support Restart

language-server/dm/executionManager.ml

@@ -104,8 +104,9 @@ let is_diagnostics_enabled () = !options.enableDiagnostics
 let get_options () = !options
 
 type prepared_task =
-  | PSkip of { id: sentence_id; error: Pp.t option }
+  | PSkip of skip
   | 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
@@ -634,34 +637,43 @@ let worker_main { ProofJob.tasks; initial_vernac_state = vs; doc_id; terminator_
     Feedback.msg_debug @@ Pp.str "==========================================================";
     exit 1
 
+let interp_Restart st id to_ =
+  match SM.find to_ st.of_sentence with
+  | (Done (Success (Some old_vs) as v), _) ->
+      let st = update st id v in
+      st, old_vs
+  | _ -> CErrors.anomaly  ~label:"vscoq" Pp.(str"Restart: to_ is incorrect")
+  | exception Not_found -> assert false
+
+let exec_error_id_of_outcome v id =
+  match v with
+  | Success _ -> None
+  | Error _ -> Some id
+
 let execute st (vs, events, interrupted) task =
   if interrupted then begin
     let st = update st (id_of_prepared_task task) (Error ((None,Pp.str "interrupted"),None,None)) in
     (st, vs, events, true, None)
   end else
     try
       match task with
-      | PSkip { id; error = err } ->
-          let v = match err with
-            | None -> success vs
-            | Some msg -> error None None msg vs
-          in
+      | PSkip { id; error = e } ->
+          let v = error None None e vs in
           let st = update st id v in
-          (st, vs, events, false, None)
+          (st, vs, events, false, exec_error_id_of_outcome v id)
       | PExec { id; ast; synterp; error_recovery } ->
           let vs = { vs with Vernacstate.synterp } in
           let vs, v, ev = interp_ast ~doc_id:st.doc_id ~state_id:id ~st:vs ~error_recovery ast in
-          let exec_error = match v with
-            | Success _ -> None
-            | Error _ -> Some id
-          in
           let st = update st id v in
-          (st, vs, events @ ev, false, exec_error)
+          (st, vs, events @ ev, false, exec_error_id_of_outcome v id)
+      | PRestart { id; to_ } -> 
+          let st, vs = interp_Restart st id to_ in
+          (st, vs, events, false, None)
       | 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
           let st = update st id v in
-          (st, vs, events @ ev, false, None)
+          (st, vs, events @ ev, false, exec_error_id_of_outcome v id)
       | PDelegate { terminator_id; opener_id; last_step_id; tasks; proof_using } ->
           begin match find_fulfilled_opt opener_id st.of_sentence with
           | Some (Success _) ->

language-server/dm/scheduler.ml

@@ -22,6 +22,10 @@ type error_recovery_strategy =
   | RSkip
   | RAdmitted
 
+type restart =  { id : sentence_id; to_ : sentence_id }
+
+type skip = { id: sentence_id; error: Pp.t }
+
 type executable_sentence = {
   id : sentence_id;
   ast : Synterp.vernac_control_entry;
@@ -31,8 +35,9 @@ type executable_sentence = {
 }
 
 type task =
-  | Skip of { id: sentence_id; error: Pp.t option }
+  | Skip of skip
   | Exec of executable_sentence
+  | Restart of restart
   | OpaqueProof of { terminator: executable_sentence;
                      opener_id: sentence_id;
                      proof_using: Vernacexpr.section_subset_expr;
@@ -45,9 +50,17 @@ type task =
   | ModuleWithSignature of ast list
 *)
 
+(* like a sub type of task, restricted what we can put in a proof *)
+type proof_command =
+  | E of executable_sentence
+  | R of restart
+  | S of skip
+
+let id_of_proof_command = function
+  | S { id } | E { id } | R { id } -> id
 
 type proof_block = {
-  proof_sentences : executable_sentence list;
+  proof_sentences : proof_command list;
   opener_id : sentence_id;
 }
 
@@ -73,13 +86,29 @@ let initial_schedule = {
   dependencies = SM.empty;
 }
 
-let push_executable_proof_sentence ex_sentence block =
-  { block with proof_sentences = ex_sentence :: block.proof_sentences }
+let push_Exec_in_block ex_sentence block =
+  { block with proof_sentences = E ex_sentence :: block.proof_sentences }
 
-let push_ex_sentence ex_sentence st =
+let push_Exec 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 }
+  | [] -> { st with document_scope = ex_sentence.id :: st.document_scope }, Exec ex_sentence
+  | l::q -> { st with proof_blocks = push_Exec_in_block ex_sentence l :: q }, Exec ex_sentence
+
+let push_Restart_in_block r block = { block with proof_sentences = R r :: block.proof_sentences }
+let push_Restart id st =
+  match st.proof_blocks with
+  | [] -> st, Skip { id; error = (Pp.str "Restart can only be used inside a proof.")}
+  | l :: q ->
+      let r = { id; to_ = l.opener_id } in
+      { st with proof_blocks = push_Restart_in_block r l :: q }, Restart r
+
+let push_Skip_in_block s block = { block with proof_sentences = S s :: block.proof_sentences }
+let push_Skip st id error =
+  let v = { id; error } in
+  match st.proof_blocks with
+  | [] -> st, Skip v
+  | l::q -> { st with proof_blocks = push_Skip_in_block v l :: q }, Skip v
+
 
 (* Not sure what the base_id for nested lemmas should be, e.g.
 Lemma foo : X.
@@ -94,26 +123,28 @@ let base_id st =
   | block :: l ->
     begin match block.proof_sentences with
     | [] -> aux l
-    | ex_sentence :: _ -> Some ex_sentence.id
+    | S { id } :: _ -> Some id
+    | E { id } :: _ -> Some id
+    | R { to_ } :: _ -> Some to_
     end
   in
   aux st.proof_blocks
 
 let open_proof_block ex_sentence st =
-  let st = push_ex_sentence ex_sentence st in
+  let st, ex = push_Exec ex_sentence st in
   let block = { proof_sentences = []; opener_id = ex_sentence.id } in
-  { st with proof_blocks = block :: st.proof_blocks }
+  { st with proof_blocks = block :: st.proof_blocks }, ex
 
 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 proof_blocks = List.map (push_Exec_in_block ex_sentence) st.proof_blocks in
+  { st with document_scope; proof_blocks }, Exec ex_sentence
 
 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 id_of_proof_command 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 +186,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 _ | S _ -> true
+   | E { classif } -> match classif with
     | VtStartProof _ | VtSideff _ | VtQed _ | VtProofMode _ | VtMeta -> true
     | VtProofStep _ | VtQuery -> false
   in
@@ -179,46 +212,77 @@ let push_state id ast synterp classif st =
   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
+    let base = base_id st in
+    let st, task = open_proof_block ex_sentence st in
+    base, st, task
   | VtQed terminator_type ->
     log "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
+      let base = base_id st in
+      let st, task = push_Exec ex_sentence st in
+      base, st, task
     | 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 "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 _ | S _ -> 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 }
+        let base = base_id st in
+        let st, _task = push_Exec ex_sentence st in
+        base, st, OpaqueProof { terminator; opener_id = block.opener_id; tasks; proof_using }
       | None ->
         log "not an opaque proof";
         let st = flatten_proof_block st in
-        base_id st, push_ex_sentence ex_sentence st, Exec ex_sentence
+        let base = base_id st in
+        let st, task = push_Exec ex_sentence st in
+        base, st, task
     end
   | VtQuery -> (* queries have no impact, we don't push them *)
     base_id st, st, Query ex_sentence
   | VtProofStep _ ->
-    base_id st, push_ex_sentence ex_sentence st, Exec ex_sentence
+    let base = base_id st in
+    let st, task = push_Exec ex_sentence st in
+    base, st, task
   | 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 base = base_id st in
+    let st, task = extrude_side_effect ex_sentence st in
+    base, st, task
+  | VtMeta ->
+      let v = ast.CAst.v in
+      begin match v.expr, v.control with
+      | Vernacexpr.(VernacSynPure VernacRestart), [] ->
+          let base = base_id st in
+          let st, task = push_Restart ex_sentence.id st in
+          base, st, task
+      | Vernacexpr.(VernacSynPure VernacRestart), _ :: _ ->
+          let base = base_id st in
+          let st, task = push_Skip st id (Pp.str "Restart cannot be decorated by controls like Time, Fail, etc...") in
+          base, st, task
+      | _ ->
+          let base = base_id st in
+          let st, task = push_Skip st id (Pp.str "Unsupported navigation command") in
+          base, st, task
+      end  
+  | VtProofMode _ ->
+      let base = base_id st in
+      let st, task = push_Skip st id (Pp.str "Unsupported command") in
+      base, st, task
 
 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 id_of_proof_command 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,10 @@ type error_recovery_strategy =
   | RSkip
   | RAdmitted
 
+type restart =  { id : sentence_id; to_ : sentence_id }
+
+type skip = { id: sentence_id; error: Pp.t }
+
 type executable_sentence = {
   id : sentence_id;
   ast : Synterp.vernac_control_entry;
@@ -36,8 +40,9 @@ type executable_sentence = {
 }
 
 type task =
-  | Skip of { id: sentence_id; error: Pp.t option }
+  | Skip of skip
   | 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.
+