Vernac classification: allow for commands which start proofs but must be synchrone.

The previous heuristic is to check whether the proof ends with Qed or not. This modification allows for commands which start proof but may produce transparent term even when the function ends with Qed.

6 files changed, 26 insertions, 21 deletions

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index d1ed1d4ab..4f666a801 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -441,7 +441,7 @@ type vernac_type =
   | VtStm of vernac_control * vernac_part_of_script
   | VtUnknown
 and vernac_qed_type = VtKeep | VtDrop (* Qed/Admitted, Abort *)
-and vernac_start = string * Id.t list
+and vernac_start = string * opacity_guarantee * Id.t list
 and vernac_sideff_type = Id.t list
 and vernac_is_alias = bool
 and vernac_part_of_script = bool
@@ -453,6 +453,9 @@ and vernac_control =
   | VtObserve of Stateid.t
   | VtBack of Stateid.t
   | VtPG
+and opacity_guarantee =
+  | GuaranteesOpacity (** Only generates opaque terms at [Qed] *)
+  | Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*)
 type vernac_when =
   | VtNow
   | VtLater
diff --git a/parsing/g_obligations.ml4 b/parsing/g_obligations.ml4
index a0d4771f1..fe024d409 100644
--- a/parsing/g_obligations.ml4
+++ b/parsing/g_obligations.ml4
@@ -60,7 +60,7 @@ let wit_withtac : Tacexpr.raw_tactic_expr option Genarg.uniform_genarg_type =
 
 open Obligations
 
-let classify_obbl _ = Vernacexpr.VtStartProof ("Classic",[]), Vernacexpr.VtLater
+let classify_obbl _ = Vernacexpr.(VtStartProof ("Classic",GuaranteesOpacity,[]), VtLater)
 
 VERNAC COMMAND EXTEND Obligations CLASSIFIED BY classify_obbl
 | [ "Obligation" integer(num) "of" ident(name) ":" lconstr(t) withtac(tac) ] ->
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index b317cec0d..3e4f67498 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -167,7 +167,7 @@ VERNAC COMMAND EXTEND Function
              (Vernacexpr.VernacFixpoint(None, List.map snd recsl))
          with
          | Vernacexpr.VtSideff ids, _ when hard ->
-             Vernacexpr.VtStartProof ("Classic", ids), Vernacexpr.VtLater
+             Vernacexpr.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater)
          | x -> x ]
     -> [ do_generate_principle false (List.map snd recsl) ]
 END
diff --git a/tactics/g_rewrite.ml4 b/tactics/g_rewrite.ml4
index 846bba1d4..31defcafb 100644
--- a/tactics/g_rewrite.ml4
+++ b/tactics/g_rewrite.ml4
@@ -244,11 +244,11 @@ VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF
     => [ Vernacexpr.VtUnknown, Vernacexpr.VtNow ]
     -> [ add_morphism_infer (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) m n ]
   | [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ]
-    => [ Vernacexpr.VtStartProof("Classic",[n]), Vernacexpr.VtLater ]
+    => [ Vernacexpr.(VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater) ]
     -> [ add_morphism (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) [] m s n ]
   | [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m)
         "with" "signature" lconstr(s) "as" ident(n) ]
-    => [ Vernacexpr.VtStartProof("Classic",[n]), Vernacexpr.VtLater ]
+    => [ Vernacexpr.(VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater) ]
     -> [ add_morphism (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) binders m s n ]
 END
 
diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index 0730c08ee..d8f905256 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -67,7 +67,7 @@ type branch_type =
   | `Proof of proof_mode * depth
   | `Edit of proof_mode * Stateid.t * Stateid.t ]
 type cmd_t = ast * Id.t list
-type fork_t = ast * Vcs_.Branch.t * Id.t list
+type fork_t = ast * Vcs_.Branch.t * Vernacexpr.opacity_guarantee * Id.t list
 type qed_t = {
   qast : ast;
   keep : vernac_qed_type;
@@ -232,7 +232,7 @@ end = struct (* {{{ *)
   let print_dag vcs () = (* {{{ *)
     let fname = "stm" ^ string_of_int (max 0 !Flags.coq_slave_mode) in
     let string_of_transaction = function
-      | Cmd (t, _) | Fork (t, _,_) ->
+      | Cmd (t, _) | Fork (t, _,_,_) ->
           (try string_of_ppcmds (pr_ast t) with _ -> "ERR")
       | Sideff (Some t) ->
           sprintf "Sideff(%s)"
@@ -1014,13 +1014,14 @@ let collect_proof cur hd id =
     match last, view.step with
     | _, `Cmd (x, _) -> collect (Some (id,x)) (id::accn) view.next
     | _, `Alias _ -> `NotOptimizable `Alias
-    | _, `Fork(_,_,_::_::_)->
+    | _, `Fork(_,_,_,_::_::_)->
         `NotOptimizable `MutualProofs (* TODO: enderstand where we need that *)
-    | Some (parent, (_,_,VernacProof(_,Some _) as v)), `Fork (_, hd', ids) ->
+    | _, `Fork(_,_,Doesn'tGuaranteeOpacity,_) -> `NotOptimizable `Doesn'tGuaranteeOpacity
+    | Some (parent, (_,_,VernacProof(_,Some _) as v)), `Fork (_, hd', GuaranteesOpacity, ids) ->
         assert (VCS.Branch.equal hd hd' || VCS.Branch.equal hd VCS.edit_branch);
         if delegate_policy_check accn then `Optimizable (parent,Some v,accn,ids)
         else `NotOptimizable `TooShort
-    | Some (parent, _), `Fork (_, hd', ids) ->
+    | Some (parent, _), `Fork (_, hd', GuaranteesOpacity, ids) ->
         assert (VCS.Branch.equal hd hd' || VCS.Branch.equal hd VCS.edit_branch);
         if delegate_policy_check accn then `MaybeOptimizable (parent, accn,ids)
         else `NotOptimizable `TooShort
@@ -1042,6 +1043,7 @@ let string_of_reason = function
   | `NestedProof -> "NestedProof"
   | `Immediate -> "Immediate"
   | `Alias -> "Alias"
+  | `Doesn'tGuaranteeOpacity -> "Doesn'tGuaranteeOpacity"
   | _ -> "Unknown Reason"
 
 let known_state ?(redefine_qed=false) ~cache id =
@@ -1075,7 +1077,7 @@ let known_state ?(redefine_qed=false) ~cache id =
       | `Cmd (x,_) -> (fun () ->
             reach view.next; vernac_interp id x
           ), cache
-      | `Fork (x,_,_) -> (fun () ->
+      | `Fork (x,_,_,_) -> (fun () ->
             reach view.next; vernac_interp id x
           ), `Yes
       | `Qed ({ qast = x; keep; brinfo; brname } as qed, eop) ->
@@ -1212,7 +1214,7 @@ end = struct (* {{{ *)
         let ids =
           if id = Stateid.initial || id = Stateid.dummy then [] else
           match VCS.visit id with
-          | { step = `Fork (_,_,l) } -> l
+          | { step = `Fork (_,_,_,l) } -> l
           | { step = `Cmd (_,l) } -> l
           | _ -> [] in
         match f acc (id, vcs, ids) with
@@ -1470,11 +1472,11 @@ let process_transaction ~tty verbose c (loc, expr) =
           anomaly(str"classifier: VtQuery + VtLater must imply part_of_script")
 
       (* Proof *)
-      | VtStartProof (mode, names), w ->
+      | VtStartProof (mode, guarantee, names), w ->
           let id = VCS.new_node () in
           let bname = VCS.mk_branch_name x in
           VCS.checkout VCS.Branch.master;
-          VCS.commit id (Fork (x, bname, names));
+          VCS.commit id (Fork (x, bname, guarantee, names));
           VCS.branch bname (`Proof (mode, VCS.proof_nesting () + 1));
           Proof_global.activate_proof_mode mode;
           Backtrack.record (); if w == VtNow then finish (); `Ok
@@ -1531,7 +1533,7 @@ let process_transaction ~tty verbose c (loc, expr) =
                Proof_global.there_are_pending_proofs ()
             then begin
               let bname = VCS.mk_branch_name x in
-              VCS.commit id (Fork (x,bname,[]));
+              VCS.commit id (Fork (x,bname,Doesn'tGuaranteeOpacity,[]));
               VCS.branch bname (`Proof ("Classic", VCS.proof_nesting () + 1));
               Proof_global.activate_proof_mode "Classic";
             end else begin
@@ -1742,7 +1744,7 @@ let get_script prf =
     if Stateid.equal id Stateid.initial || Stateid.equal id Stateid.dummy then acc else
     let view = VCS.visit id in
     match view.step with
-    | `Fork (_,_,ns) when List.mem prf ns -> acc
+    | `Fork (_,_,_,ns) when List.mem prf ns -> acc
     | `Qed (qed, proof) -> find [pi3 qed.qast, (VCS.get_info id).n_goals] proof
     | `Sideff (`Ast (x,_)) ->
          find ((pi3 x, (VCS.get_info id).n_goals)::acc) view.next
diff --git a/toplevel/vernac_classifier.ml b/toplevel/vernac_classifier.ml
index 2e04d1430..4ef157a64 100644
--- a/toplevel/vernac_classifier.ml
+++ b/toplevel/vernac_classifier.ml
@@ -94,23 +94,23 @@ let rec classify_vernac e =
     | VernacSolveExistential _ -> VtProofStep, VtLater
     (* StartProof *)
     | VernacDefinition (_,(_,i),ProveBody _) ->
-        VtStartProof("Classic",[i]), VtLater
+        VtStartProof("Classic",GuaranteesOpacity,[i]), VtLater
     | VernacStartTheoremProof (_,l,_) ->
         let ids = 
           CList.map_filter (function (Some(_,i), _) -> Some i | _ -> None) l in
-        VtStartProof ("Classic", ids), VtLater
-    | VernacGoal _ -> VtStartProof ("Classic",[]), VtLater
+        VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater
+    | VernacGoal _ -> VtStartProof ("Classic",GuaranteesOpacity,[]), VtLater
     | VernacFixpoint (_,l) ->
         let ids, open_proof =
           List.fold_left (fun (l,b) (((_,id),_,_,_,p),_) ->
             id::l, b || p = None) ([],false) l in
-        if open_proof then VtStartProof ("Classic",ids), VtLater
+        if open_proof then VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater
         else VtSideff ids, VtLater
     | VernacCoFixpoint (_,l) ->
         let ids, open_proof =
           List.fold_left (fun (l,b) (((_,id),_,_,p),_) ->
             id::l, b || p = None) ([],false) l in
-        if open_proof then VtStartProof ("Classic",ids), VtLater
+        if open_proof then VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater
         else VtSideff ids, VtLater
     (* Sideff: apply to all open branches. usually run on master only *)
     | VernacAssumption (_,_,l) ->