package vscoq-language-server
- Overview
- No Docs
You can search for identifiers within the package.
in-package search v0.2.0
VSCoq language server
Install
Dune Dependency
Authors
Maintainers
Sources
vscoq-language-server-2.2.6.tar.gz
md5=f528c1760966ac10d48b5f1c5531411a
sha512=1f69538ae5f78854b34e3f1a9d408714843e899bb96d063c2bfac410339b6a13ee5f30d5e7b3cd2bbd673169bcfdb550153ba741092cdc3ee3a8ca6446cc2240
doc/src/vscoq-language-server.dm/scheduler.ml.html
Source file scheduler.ml
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291
(**************************************************************************) (* *) (* VSCoq *) (* *) (* Copyright INRIA and contributors *) (* (see version control and README file for authors & dates) *) (* *) (**************************************************************************) (* *) (* This file is distributed under the terms of the MIT License. *) (* See LICENSE file. *) (* *) (**************************************************************************) open Types let Log log = Log.mk_log "scheduler" module SM = CMap.Make (Stateid) type error_recovery_strategy = | RSkip | RAdmitted type executable_sentence = { id : sentence_id; ast : Synterp.vernac_control_entry; classif : Vernacextend.vernac_classification; synterp : Vernacstate.Synterp.t; error_recovery : error_recovery_strategy; } type task = | Skip of { id: sentence_id; error: Pp.t option } | Block of { id: sentence_id; error: Pp.t Loc.located } | Exec of executable_sentence | OpaqueProof of { terminator: executable_sentence; opener_id: sentence_id; proof_using: Vernacexpr.section_subset_expr; tasks : executable_sentence list; (* non empty list *) } | Query of executable_sentence (* | SubProof of ast list | ModuleWithSignature of ast list *) type proof_block = { proof_sentences : executable_sentence list; opener_id : sentence_id; } type state = { document_scope : sentence_id list; (* List of sentences whose effect scope is the document that follows them *) proof_blocks : proof_block list; (* List of sentences whose effect scope ends with the Qed *) section_depth : int; (* Statically computed section nesting *) } let initial_state = { document_scope = []; proof_blocks = []; section_depth = 0; } type schedule = { tasks : (sentence_id option * task) SM.t; dependencies : Stateid.Set.t SM.t; } let initial_schedule = { tasks = SM.empty; dependencies = SM.empty; } let push_executable_proof_sentence ex_sentence block = { block with proof_sentences = ex_sentence :: block.proof_sentences } let push_ex_sentence ex_sentence st = match st.proof_blocks with | [] -> { st with document_scope = ex_sentence.id :: st.document_scope } | l::q -> { st with proof_blocks = push_executable_proof_sentence ex_sentence l :: q } (* Not sure what the base_id for nested lemmas should be, e.g. Lemma foo : X. Proof. Definition x := True. intros ... Lemma bar : Y. <- What should the base_id be for this command? -> 83 *) let base_id st = let rec aux = function | [] -> (match st.document_scope with hd :: _ -> Some hd | [] -> None) | block :: l -> begin match block.proof_sentences with | [] -> aux l | ex_sentence :: _ -> Some ex_sentence.id end in aux st.proof_blocks let open_proof_block ex_sentence st = let st = push_ex_sentence ex_sentence st in let block = { proof_sentences = []; opener_id = ex_sentence.id } in { st with proof_blocks = block :: st.proof_blocks } let extrude_side_effect ex_sentence st = let document_scope = ex_sentence.id :: st.document_scope in let proof_blocks = List.map (push_executable_proof_sentence ex_sentence) st.proof_blocks in { st with document_scope; proof_blocks } let flatten_proof_block st = match st.proof_blocks with | [] -> st | [block] -> let document_scope = CList.uniquize @@ List.map (fun x -> x.id) block.proof_sentences @ st.document_scope in { st with document_scope; proof_blocks = [] } | block1 :: block2 :: tl -> (* Nested proofs. TODO check if we want to extrude one level or directly to document scope *) let proof_sentences = CList.uniquize @@ block1.proof_sentences @ block2.proof_sentences in let block2 = { block2 with proof_sentences } in { st with proof_blocks = block2 :: tl } (* [1] Lemma foo : XX. [2] Proof. [3] Definition y := True. [4] Lemma bar : y. [5] Proof. [6] exact I. [7] Qed. [8] apply bar. [9] Qed. -> We don't delegate 8: Exec(127, Qed) 2: Exec(1, Lemma foo : XX) --> We delegate only pure proofs *) (* FIXME handle commands with side effects followed by `Abort` *) let find_proof_using (ast : Synterp.vernac_control_entry) = match ast.CAst.v.expr with | VernacSynPure(VernacProof(_,Some e)) -> Some e | _ -> log (fun () -> "no ast for proof using, looking at a default"); Proof_using.get_default_proof_using () (* TODO: There is also a #[using] annotation on the proof opener we should take into account (but it is not on a proof sentence, but rather on the proof opener). Ask maxime if the attribute is processed during synterp, and if so where its value is stored. *) let find_proof_using_annotation { proof_sentences } = match List.rev proof_sentences with | ex_sentence :: _ -> find_proof_using ex_sentence.ast | _ -> None let is_opaque_flat_proof terminator section_depth block = let open Vernacextend in let has_side_effect { classif } = match classif with | VtStartProof _ | VtSideff _ | VtQed _ | VtProofMode _ | VtMeta -> true | VtProofStep _ | VtQuery -> false in if List.exists has_side_effect block.proof_sentences then None else match terminator with | VtDrop -> Some Vernacexpr.SsEmpty | VtKeep VtKeepDefined -> None | VtKeep (VtKeepAxiom | VtKeepOpaque) -> if section_depth = 0 then Some Vernacexpr.SsEmpty else find_proof_using_annotation block let push_state id ast synterp classif st = let open Vernacextend in let ex_sentence = { id; ast; classif; synterp; error_recovery = RSkip } in match classif with | VtStartProof _ -> base_id st, open_proof_block ex_sentence st, Exec ex_sentence | VtQed terminator_type -> log (fun () -> "scheduling a qed"); begin match st.proof_blocks with | [] -> (* can happen on ill-formed documents *) base_id st, push_ex_sentence ex_sentence st, Exec ex_sentence | block :: pop -> (* TODO do not delegate if command with side effect inside the proof or nested lemmas *) match is_opaque_flat_proof terminator_type st.section_depth block with | Some proof_using -> log (fun () -> "opaque proof"); let terminator = { ex_sentence with error_recovery = RAdmitted } in let tasks = List.rev block.proof_sentences in let st = { st with proof_blocks = pop } in base_id st, push_ex_sentence ex_sentence st, OpaqueProof { terminator; opener_id = block.opener_id; tasks; proof_using } | None -> log (fun () -> "not an opaque proof"); let st = flatten_proof_block st in base_id st, push_ex_sentence ex_sentence st, Exec ex_sentence end | VtQuery -> (* queries have no impact, we don't push them *) base_id st, push_ex_sentence ex_sentence st, Query ex_sentence | VtProofStep _ -> base_id st, push_ex_sentence ex_sentence st, Exec ex_sentence | VtSideff _ -> base_id st, extrude_side_effect ex_sentence st, Exec ex_sentence | VtMeta -> base_id st, push_ex_sentence ex_sentence st, Skip { id; error = Some (Pp.str "Unsupported command") } | VtProofMode _ -> base_id st, push_ex_sentence ex_sentence st, Skip { id; error = Some (Pp.str "Unsupported command") } let string_of_task (task_id,(base_id,task)) = let s = match task with | Skip { id } -> Format.sprintf "Skip %s" (Stateid.to_string id) | Exec { id } -> Format.sprintf "Exec %s" (Stateid.to_string id) | OpaqueProof { terminator; tasks } -> Format.sprintf "OpaqueProof [%s | %s]" (Stateid.to_string terminator.id) (String.concat "," (List.map (fun task -> Stateid.to_string task.id) tasks)) | Query { id } -> Format.sprintf "Query %s" (Stateid.to_string id) | Block { id } -> Format.sprintf "Block %s" (Stateid.to_string id) in Format.sprintf "[%s] : [%s] -> %s" (Stateid.to_string task_id) (Option.cata Stateid.to_string "init" base_id) s let _string_of_state st = let scopes = (List.map (fun b -> List.map (fun x -> x.id) b.proof_sentences) st.proof_blocks) @ [st.document_scope] in String.concat "|" (List.map (fun l -> String.concat " " (List.map Stateid.to_string l)) scopes) let schedule_errored_sentence id error schedule = let task = Block {id; error} in let tasks = SM.add id (None, task) schedule.tasks in let dependencies = SM.add id Stateid.Set.empty schedule.dependencies in {tasks; dependencies} let schedule_sentence (id, (ast, classif, synterp_st)) st schedule = let base, st, task = let open Vernacexpr in let (base, st, task) = push_state id ast synterp_st classif st in begin match ast.CAst.v.expr with | VernacSynterp (EVernacBeginSection _) -> (base, { st with section_depth = st.section_depth + 1 }, task) | VernacSynterp (EVernacEndSegment _) -> (base, { st with section_depth = max 0 (st.section_depth - 1) }, task) | _ -> (base, st, task) end in (* log (fun () -> "Scheduled " ^ (Stateid.to_string id) ^ " based on " ^ (match base with Some id -> Stateid.to_string id | None -> "no state")); log (fun () -> "New scheduler state: " ^ string_of_state st); *) let tasks = SM.add id (base, task) schedule.tasks in let add_dep deps x id = let upd = function | Some deps -> Some (Stateid.Set.add id deps) | None -> Some (Stateid.Set.singleton id) in SM.update x upd deps in let dependencies = Option.cata (fun x -> add_dep schedule.dependencies x id) schedule.dependencies base in (* This new sentence impacts no sentence (yet) *) let dependencies = SM.add id Stateid.Set.empty dependencies in st, { tasks; dependencies } let task_for_sentence schedule id = match SM.find_opt id schedule.tasks with | Some x -> x | None -> CErrors.anomaly Pp.(str "cannot find schedule for sentence " ++ Stateid.print id) let dependents schedule id = match SM.find_opt id schedule.dependencies with | Some x -> x | None -> CErrors.anomaly Pp.(str "cannot find dependents for sentence " ++ Stateid.print id) (** Dependency computation algo *) (* {} 1. Definition y := ... {{1}} 2. Lemma x : T. {{},{1,2}} 3. Proof using v. {{3},{1,2}} 4. tac1. {{3,4},{1,2}} 5. Definition f := Type. {{3,4,5},{1,2,5}} 6. Defined. || 6. Qed. {{1,2,3,4,5,6}} || {{1,2,5,6}} 7. Check x. *) let string_of_schedule schedule = "Task\n" ^ String.concat "\n" @@ List.map string_of_task @@ SM.bindings schedule.tasks
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>