From dcc3b5ff7cb7ff2a087ecb10ca661079c925410a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 26 Sep 2024 00:33:00 +0200 Subject: [PATCH] support Restart --- language-server/dm/executionManager.ml | 21 ++++++++--- language-server/dm/scheduler.ml | 41 ++++++++++++++++----- language-server/dm/scheduler.mli | 3 ++ language-server/tests/interactive/restart.v | 9 +++++ 4 files changed, 60 insertions(+), 14 deletions(-) create mode 100644 language-server/tests/interactive/restart.v diff --git a/language-server/dm/executionManager.ml b/language-server/dm/executionManager.ml index 92fdf7da..1c327276 100644 --- a/language-server/dm/executionManager.ml +++ b/language-server/dm/executionManager.ml @@ -106,6 +106,7 @@ let get_options () = !options type prepared_task = | PSkip of { id: sentence_id; error: Pp.t option } | PExec of executable_sentence + | PRestart of { id : sentence_id; to_ : sentence_id } | PQuery of executable_sentence | PDelegate of { terminator_id: sentence_id; opener_id: sentence_id; @@ -306,7 +307,7 @@ let rec cut_from_range r = function let cut_overview task state document = let range = match task with | PDelegate { terminator_id } -> Document.range_of_id_with_blank_space document terminator_id - | PSkip { id } | PExec { id } | PQuery { id } -> + | PSkip { id } | PExec { id } | PQuery { id } | PRestart {id } -> Document.range_of_id_with_blank_space document id in let {prepared; processing; processed} = state.overview in @@ -379,7 +380,7 @@ let invalidate_prepared_or_processing task state document = let processing = remove_or_truncate_range range processing in let overview = {state.overview with prepared; processing} in {state with overview} - | PSkip { id } | PExec { id } | PQuery { id } -> + | PSkip { id } | PExec { id } | PQuery { id } | PRestart {id } -> let range = Document.range_of_id_with_blank_space document id in let prepared = remove_or_truncate_range range prepared in let processing = remove_or_truncate_range range processing in @@ -400,7 +401,7 @@ let update_processing task state document = let prepared = remove_or_truncate_range range prepared in let overview = {state.overview with prepared; processing} in {state with overview} - | PSkip { id } | PExec { id } | PQuery { id } -> + | PSkip { id } | PExec { id } | PQuery { id } | PRestart {id } -> let range = Document.range_of_id_with_blank_space document id in let processing = insert_or_merge_range range processing in let prepared = remove_or_truncate_range range prepared in @@ -420,7 +421,7 @@ let update_prepared task document state = let prepared = List.append prepared [ range ] in let overview = {state.overview with prepared} in {state with overview} - | PSkip { id } | PExec { id } | PQuery { id } -> + | PSkip { id } | PExec { id } | PQuery { id } | PRestart {id } -> let range = Document.range_of_id_with_blank_space document id in let prepared = insert_or_merge_range range prepared in let overview = {state.overview with prepared} in @@ -436,7 +437,7 @@ let update_overview task todo state document = let overview = update_processed_as_Done (Success None) range state.overview in let overview = {overview with prepared} in {state with overview} - | PSkip { id } | PExec { id } | PQuery { id } -> + | PSkip { id } | PExec { id } | PQuery { id } | PRestart {id } -> update_processed id state document in match todo with @@ -568,6 +569,7 @@ let prepare_task task : prepared_task list = match task with | Skip { id; error } -> [PSkip { id; error }] | Exec e -> [PExec e] + | Restart { id; to_} -> [PRestart { id; to_}] | Query e -> [PQuery e] | OpaqueProof { terminator; opener_id; tasks; proof_using} -> match !options.delegation_mode with @@ -586,6 +588,7 @@ let id_of_prepared_task = function | PSkip { id } -> id | PExec ex -> ex.id | PQuery ex -> ex.id + | PRestart { id } -> id | PDelegate { terminator_id } -> terminator_id let purge_state = function @@ -657,6 +660,14 @@ let execute st (vs, events, interrupted) task = in let st = update st id v in (st, vs, events @ ev, false, exec_error) + | PRestart { id; to_ } -> begin + match SM.find to_ st.of_sentence with + | (Done (Success (Some vs) as v), _) -> + let st = update st id v in + (st, vs, events, false, None) + | _ -> assert false + | exception Not_found -> assert false + end | PQuery { id; ast; synterp; error_recovery } -> let vs = { vs with Vernacstate.synterp } in let _, v, ev = interp_ast ~doc_id:st.doc_id ~state_id:id ~st:vs ~error_recovery ast in diff --git a/language-server/dm/scheduler.ml b/language-server/dm/scheduler.ml index c8733a70..3c029af6 100644 --- a/language-server/dm/scheduler.ml +++ b/language-server/dm/scheduler.ml @@ -22,6 +22,8 @@ type error_recovery_strategy = | RSkip | RAdmitted +type restart = { id : sentence_id; to_ : sentence_id } + type executable_sentence = { id : sentence_id; ast : Synterp.vernac_control_entry; @@ -33,6 +35,7 @@ type executable_sentence = { type task = | Skip of { id: sentence_id; error: Pp.t option } | Exec of executable_sentence + | Restart of restart | OpaqueProof of { terminator: executable_sentence; opener_id: sentence_id; proof_using: Vernacexpr.section_subset_expr; @@ -45,9 +48,12 @@ type task = | ModuleWithSignature of ast list *) +type executable_sentence_or_restart = + | E of executable_sentence + | R of restart type proof_block = { - proof_sentences : executable_sentence list; + proof_sentences : executable_sentence_or_restart list; opener_id : sentence_id; } @@ -74,13 +80,19 @@ let initial_schedule = { } let push_executable_proof_sentence ex_sentence block = - { block with proof_sentences = ex_sentence :: block.proof_sentences } + { block with proof_sentences = E 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 } +let push_restart_command id to_ block = { block with proof_sentences = R { id; to_ } :: block.proof_sentences } +let push_restart id st = + match st.proof_blocks with + | [] -> assert false (* FIXME: cannot use Restart outside proofs *) + | l::q -> { st with proof_blocks = push_restart_command id l.opener_id l :: q }, Restart { id; to_ = l.opener_id } + (* Not sure what the base_id for nested lemmas should be, e.g. Lemma foo : X. Proof. @@ -94,7 +106,8 @@ let base_id st = | block :: l -> begin match block.proof_sentences with | [] -> aux l - | ex_sentence :: _ -> Some ex_sentence.id + | E { id } :: _ -> Some id + | R { to_ } :: _ -> Some to_ end in aux st.proof_blocks @@ -113,7 +126,7 @@ 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 + let document_scope = CList.uniquize @@ List.map (function E { id } -> id | R { id } -> 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 @@ -155,14 +168,16 @@ let find_proof_using (ast : Synterp.vernac_control_entry) = 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 + | E 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 + let has_side_effect = function + | R _ -> true + | E { classif } -> match classif with | VtStartProof _ | VtSideff _ | VtQed _ | VtProofMode _ | VtMeta -> true | VtProofStep _ | VtQuery -> false in @@ -191,7 +206,7 @@ let push_state id ast synterp classif st = | Some proof_using -> log "opaque proof"; let terminator = { ex_sentence with error_recovery = RAdmitted } in - let tasks = List.rev block.proof_sentences in + let tasks = List.rev_map (function E x -> x | R _ -> assert false) 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 -> @@ -205,20 +220,28 @@ let push_state id ast synterp classif st = 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") } + | VtMeta -> + begin match ast.CAst.v.expr with + | Vernacexpr.(VernacSynPure VernacRestart) -> + let base = base_id st in + let st, t = push_restart ex_sentence.id st in + base, st, t (* TOOD: control *) + | _ -> base_id st, push_ex_sentence ex_sentence st, Skip { id; error = Some (Pp.str "Unsupported command") } + end | 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) + | Restart { id; to_ } -> Format.sprintf "Reset %s -> %s" (Stateid.to_string id) (Stateid.to_string to_) | 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) 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 + let scopes = (List.map (fun b -> List.map (function E { id } -> id | R { id } -> 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_sentence (id, (ast, classif, synterp_st)) st schedule = diff --git a/language-server/dm/scheduler.mli b/language-server/dm/scheduler.mli index 436d9384..bc4f9611 100644 --- a/language-server/dm/scheduler.mli +++ b/language-server/dm/scheduler.mli @@ -27,6 +27,8 @@ type error_recovery_strategy = | RSkip | RAdmitted +type restart = { id : sentence_id; to_ : sentence_id } + type executable_sentence = { id : sentence_id; ast : Synterp.vernac_control_entry; @@ -38,6 +40,7 @@ type executable_sentence = { type task = | Skip of { id: sentence_id; error: Pp.t option } | Exec of executable_sentence + | Restart of restart | OpaqueProof of { terminator: executable_sentence; opener_id: sentence_id; proof_using: Vernacexpr.section_subset_expr; diff --git a/language-server/tests/interactive/restart.v b/language-server/tests/interactive/restart.v new file mode 100644 index 00000000..299826b2 --- /dev/null +++ b/language-server/tests/interactive/restart.v @@ -0,0 +1,9 @@ +Goal True. +Proof. + exact I. +Restart. + auto. +Restart. + cut False. +Restart. + \ No newline at end of file