support Restart

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

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 =

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;

language-server/tests/interactive/restart.v

@@ -0,0 +1,9 @@
+Goal True.
+Proof.
+    exact I.
+Restart.
+    auto.
+Restart.
+    cut False.
+Restart.
+