diff options
Diffstat (limited to 'toplevel/stm.ml')
| -rw-r--r-- | toplevel/stm.ml | 24 |
1 files changed, 13 insertions, 11 deletions
diff --git a/toplevel/stm.ml b/toplevel/stm.ml index 0730c08ee4..d8f9052563 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 |