From 7be8d27e52c603b57d7d42dec805a291954e0b3c Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Thu, 26 Sep 2024 14:19:36 +0200
Subject: [PATCH] cleanup handling of unsupported commands (Skip)

---
 language-server/dm/executionManager.ml |   9 +--
 language-server/dm/scheduler.ml        | 103 +++++++++++++++++--------
 language-server/dm/scheduler.mli       |   4 +-
 3 files changed, 78 insertions(+), 38 deletions(-)

diff --git a/language-server/dm/executionManager.ml b/language-server/dm/executionManager.ml
index 5b7fb0b82..2fe7f846e 100644
--- a/language-server/dm/executionManager.ml
+++ b/language-server/dm/executionManager.ml
@@ -104,7 +104,7 @@ 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
@@ -657,11 +657,8 @@ let execute st (vs, events, interrupted) task =
   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, exec_error_id_of_outcome v id)
       | PExec { id; ast; synterp; error_recovery } ->
diff --git a/language-server/dm/scheduler.ml b/language-server/dm/scheduler.ml
index 78e72f469..4a50952a0 100644
--- a/language-server/dm/scheduler.ml
+++ b/language-server/dm/scheduler.ml
@@ -24,6 +24,8 @@ type error_recovery_strategy =
 
 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;
@@ -33,7 +35,7 @@ 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;
@@ -48,12 +50,17 @@ type task =
   | ModuleWithSignature of ast list
 *)
 
-type executable_sentence_or_restart =
+(* 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_or_restart list;
+  proof_sentences : proof_command list;
   opener_id : sentence_id;
 }
 
@@ -79,19 +86,29 @@ let initial_schedule = {
   dependencies = SM.empty;
 }
 
-let push_executable_proof_sentence ex_sentence block =
+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_command id to_ block = { block with proof_sentences = R { id; to_ } :: block.proof_sentences }
-let push_restart id st =
+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 = Some (Pp.str "Restart can only be used inside a proof.")}
-  | l::q -> { st with proof_blocks = push_restart_command id l.opener_id l :: q }, Restart { id; to_ = l.opener_id }
+  | [] -> 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.
@@ -106,6 +123,7 @@ let base_id st =
   | block :: l ->
     begin match block.proof_sentences with
     | [] -> aux l
+    | S { id } :: _ -> Some id
     | E { id } :: _ -> Some id
     | R { to_ } :: _ -> Some to_
     end
@@ -113,20 +131,20 @@ let base_id st =
   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 (function E { id } -> id | R { id } -> 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
@@ -176,7 +194,7 @@ let find_proof_using_annotation { proof_sentences } =
 let is_opaque_flat_proof terminator section_depth block =
   let open Vernacextend in
   let has_side_effect = function
-   | R _ -> true
+   | R _ | S _ -> true
    | E { classif } -> match classif with
     | VtStartProof _ | VtSideff _ | VtQed _ | VtProofMode _ | VtMeta -> true
     | VtProofStep _ | VtQuery -> false
@@ -194,41 +212,64 @@ 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_map (function E x -> x | R _ -> assert false) 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
+    let base = base_id st in
+    let st, task = extrude_side_effect ex_sentence st in
+    base, st, task
   | VtMeta ->
-      begin match ast.CAst.v.expr with
-      | Vernacexpr.(VernacSynPure VernacRestart) ->
+      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, 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") }
+          let st, task = push_Skip st id (Pp.str "Unsupported navigation command") in
+          base, st, task
       end  
-  | VtProofMode _ -> base_id st, push_ex_sentence ex_sentence st, Skip { id; error = Some (Pp.str "Unsupported command") }
+  | 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
@@ -241,7 +282,7 @@ let string_of_task (task_id,(base_id,task)) =
   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 (function E { id } -> id | R { id } -> 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 =
diff --git a/language-server/dm/scheduler.mli b/language-server/dm/scheduler.mli
index bc4f9611a..617b9c14f 100644
--- a/language-server/dm/scheduler.mli
+++ b/language-server/dm/scheduler.mli
@@ -29,6 +29,8 @@ type error_recovery_strategy =
 
 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;
@@ -38,7 +40,7 @@ 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;