From b2f2727670853183bfbcbafb9dc19f0f71494a7b Mon Sep 17 00:00:00 2001 From: gareuselesinge Date: Thu, 8 Aug 2013 18:51:35 +0000 Subject: State Transaction Machine The process_transaction function adds a new edge to the Dag without executing the transaction (when possible). The observe id function runs the transactions necessary to reach to the state id. Transaction being on a merged branch are not executed but stored into a future. The finish function calls observe on the tip of the current branch. Imperative modifications to the environment made by some tactics are now explicitly declared by the tactic and modeled as let-in/beta-redexes at the root of the proof term. An example is the abstract tactic. This is the work described in the Coq Workshop 2012 paper. Coq is compile with thread support from now on. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16674 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/decl_mode/decl_mode.ml | 8 +++-- plugins/decl_mode/decl_mode.mli | 4 +-- plugins/decl_mode/decl_proof_instr.ml | 43 ++++++++++++++------------- plugins/decl_mode/g_decl_mode.ml4 | 14 ++++++--- plugins/extraction/extraction.ml | 4 +-- plugins/funind/functional_principles_types.ml | 8 +++-- plugins/funind/invfun.ml | 17 +++-------- plugins/funind/recdef.ml | 15 ++++------ plugins/setoid_ring/newring.ml4 | 18 ++++++----- 9 files changed, 66 insertions(+), 65 deletions(-) (limited to 'plugins') diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml index 8c5aec38bf..0cbd263168 100644 --- a/plugins/decl_mode/decl_mode.ml +++ b/plugins/decl_mode/decl_mode.ml @@ -99,11 +99,13 @@ let proof_cond = Proof.no_cond proof_focus let focus p = let inf = get_stack p in - Proof.focus proof_cond inf 1 p + Proof_global.with_current_proof (fun _ -> Proof.focus proof_cond inf 1) -let unfocus = Proof.unfocus proof_focus +let unfocus () = + Proof_global.with_current_proof (fun _ p -> Proof.unfocus proof_focus p ()) -let maximal_unfocus = Proof_global.maximal_unfocus proof_focus +let maximal_unfocus () = + Proof_global.with_current_proof (fun _ -> Proof.maximal_unfocus proof_focus) let get_top_stack pts = try diff --git a/plugins/decl_mode/decl_mode.mli b/plugins/decl_mode/decl_mode.mli index c54dcdc281..8e691f508f 100644 --- a/plugins/decl_mode/decl_mode.mli +++ b/plugins/decl_mode/decl_mode.mli @@ -75,6 +75,6 @@ val get_last: Environ.env -> Id.t val focus : Proof.proof -> unit -val unfocus : Proof.proof -> unit +val unfocus : unit -> unit -val maximal_unfocus : Proof.proof -> unit +val maximal_unfocus : unit -> unit diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index a06b44083d..e3ef0671c0 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -51,12 +51,13 @@ let _ = let tcl_change_info_gen info_gen = (fun gls -> + let it, eff = sig_it gls, sig_eff gls in let concl = pf_concl gls in - let hyps = Goal.V82.hyps (project gls) (sig_it gls) in - let extra = Goal.V82.extra (project gls) (sig_it gls) in + let hyps = Goal.V82.hyps (project gls) it in + let extra = Goal.V82.extra (project gls) it in let (gl,ev,sigma) = Goal.V82.mk_goal (project gls) hyps concl (info_gen extra) in - let sigma = Goal.V82.partial_solution sigma (sig_it gls) ev in - { it = [gl] ; sigma= sigma } ) + let sigma = Goal.V82.partial_solution sigma it ev in + { it = [gl] ; sigma= sigma; eff = eff } ) let tcl_change_info info gls = let info_gen s = Store.set s Decl_mode.info info in @@ -128,34 +129,34 @@ let go_to_proof_mode () = let daimon_tac gls = set_daimon_flag (); - {it=[];sigma=sig_sig gls} + {it=[];sigma=sig_sig gls;eff=gls.eff} (* post-instruction focus management *) (* spiwack: This used to fail if there was no focusing command above, but I don't think it ever happened. I hope it doesn't mess things up*) -let goto_current_focus pts = - Decl_mode.maximal_unfocus pts +let goto_current_focus () = + Decl_mode.maximal_unfocus () -let goto_current_focus_or_top pts = - goto_current_focus pts +let goto_current_focus_or_top () = + goto_current_focus () (* return *) -let close_tactic_mode pts = - try goto_current_focus pts +let close_tactic_mode () = + try goto_current_focus () with Not_found -> error "\"return\" cannot be used outside of Declarative Proof Mode." let return_from_tactic_mode () = - close_tactic_mode (Proof_global.give_me_the_proof ()) + close_tactic_mode () (* end proof/claim *) let close_block bt pts = if Proof.no_focused_goal pts then - goto_current_focus pts + goto_current_focus () else let stack = if Proof.is_done pts then @@ -165,7 +166,7 @@ let close_block bt pts = in match bt,stack with B_claim, Claim::_ | B_focus, Focus_claim::_ | B_proof, [] -> - (goto_current_focus pts) + (goto_current_focus ()) | _, Claim::_ -> error "\"end claim\" expected." | _, Focus_claim::_ -> @@ -190,13 +191,13 @@ let close_previous_case pts = match get_top_stack pts with Per (et,_,_,_) :: _ -> anomaly (Pp.str "Weird case occured ...") | Suppose_case :: Per (et,_,_,_) :: _ -> - goto_current_focus (pts) + goto_current_focus () | _ -> error "Not inside a proof per cases or induction." else match get_stack pts with Per (et,_,_,_) :: _ -> () | Suppose_case :: Per (et,_,_,_) :: _ -> - goto_current_focus ((pts)) + goto_current_focus () | _ -> error "Not inside a proof per cases or induction." (* Proof instructions *) @@ -1443,21 +1444,21 @@ let rec postprocess pts instr = in try Inductiveops.control_only_guard env pfterm; - goto_current_focus_or_top pts + goto_current_focus_or_top () with Type_errors.TypeError(env, Type_errors.IllFormedRecBody(_,_,_,_,_)) -> anomaly (Pp.str "\"end induction\" generated an ill-formed fixpoint") end | Pend _ -> - goto_current_focus_or_top (pts) + goto_current_focus_or_top () let do_instr raw_instr pts = let has_tactic = preprocess pts raw_instr.instr in begin if has_tactic then - let { it=gls ; sigma=sigma } = Proof.V82.subgoals pts in - let gl = { it=List.hd gls ; sigma=sigma } in + let { it=gls ; sigma=sigma; eff=eff } = Proof.V82.subgoals pts in + let gl = { it=List.hd gls ; sigma=sigma; eff=eff } in let env= pf_env gl in let ist = {ltacvars = Id.Set.empty; ltacrecvars = Id.Map.empty; gsigma = sigma; genv = env} in @@ -1469,7 +1470,7 @@ let do_instr raw_instr pts = postprocess pts raw_instr.instr; (* spiwack: this should restore a compatible semantics with v8.3 where we never stayed focused on 0 goal. *) - Decl_mode.maximal_unfocus pts + Decl_mode.maximal_unfocus () let proof_instr raw_instr = let p = Proof_global.give_me_the_proof () in diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index 8f570af7e2..072737dab2 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -65,7 +65,7 @@ let vernac_decl_proof () = if Proof.is_done pf then Errors.error "Nothing left to prove here." else - Proof.transaction pf begin fun () -> + begin Decl_proof_instr.go_to_proof_mode () ; Proof_global.set_proof_mode "Declarative" ; Vernacentries.print_subgoals () @@ -73,14 +73,14 @@ let vernac_decl_proof () = (* spiwack: some bureaucracy is not performed here *) let vernac_return () = - Proof.transaction (Proof_global.give_me_the_proof ()) begin fun () -> + begin Decl_proof_instr.return_from_tactic_mode () ; Proof_global.set_proof_mode "Declarative" ; Vernacentries.print_subgoals () end let vernac_proof_instr instr = - Proof.transaction (Proof_global.give_me_the_proof ()) begin fun () -> + begin Decl_proof_instr.proof_instr instr; Vernacentries.print_subgoals () end @@ -397,4 +397,10 @@ GLOBAL: proof_instr; ; END;; - +open Vernacexpr + +let () = + Vernac_classifier.declare_vernac_classifier "decl_mode" (function + | VernacExtend (("DeclProof"|"DeclReturn"), _) -> VtProofStep, VtNow + | VernacExtend ("ProofInstr", _) -> VtProofStep, VtLater + | _ -> VtUnknown, VtNow) diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 5c67c33b6a..68f832997c 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -993,7 +993,7 @@ let extract_constant env kn cb = | OpaqueDef c -> add_opaque r; if access_opaque () then - mk_typ (Lazyconstr.force_opaque c) + mk_typ (Lazyconstr.force_opaque (Future.force c)) else mk_typ_ax ()) | (Info,Default) -> (match cb.const_body with @@ -1002,7 +1002,7 @@ let extract_constant env kn cb = | OpaqueDef c -> add_opaque r; if access_opaque () then - mk_def (Lazyconstr.force_opaque c) + mk_def (Lazyconstr.force_opaque (Future.force c)) else mk_ax ()) let extract_constant_spec env kn cb = diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index f70ce00924..efed9a8560 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -339,7 +339,8 @@ let generate_functional_principle let value = change_property_sort s new_principle_type new_princ_name in (* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *) let ce = - { const_entry_body = value; + { const_entry_body = + Future.from_val (value,Declareops.no_seff); const_entry_secctx = None; const_entry_type = None; const_entry_opaque = false; @@ -556,7 +557,7 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis List.map (compute_new_princ_type_from_rel funs sorts) other_princ_types in let first_princ_body,first_princ_type = const.Entries.const_entry_body, const.Entries.const_entry_type in - let ctxt,fix = decompose_lam_assum first_princ_body in (* the principle has for forall ...., fix .*) + let ctxt,fix = decompose_lam_assum (fst(Future.force first_princ_body)) in (* the principle has for forall ...., fix .*) let (idxs,_),(_,ta,_ as decl) = destFix fix in let other_result = List.map (* we can now compute the other principles *) @@ -598,7 +599,8 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis Termops.it_mkLambda_or_LetIn (mkFix((idxs,i),decl)) ctxt in {const with - Entries.const_entry_body = princ_body; + Entries.const_entry_body = + (Future.from_val (princ_body,Declareops.no_seff)); Entries.const_entry_type = Some scheme_type } ) diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index fd074386ec..7d14d1408c 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -1013,10 +1013,9 @@ let do_save () = Lemmas.save_named false *) let derive_correctness make_scheme functional_induction (funs: constant list) (graphs:inductive list) = - let previous_state = States.freeze ~marshallable:false in let funs = Array.of_list funs and graphs = Array.of_list graphs in let funs_constr = Array.map mkConst funs in - try + States.with_state_protection (fun () -> let graphs_constr = Array.map mkInd graphs in let lemmas_types_infos = Util.Array.map2_i @@ -1044,7 +1043,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g Array.of_list (List.map (fun entry -> - (entry.Entries.const_entry_body, Option.get entry.Entries.const_entry_type ) + (fst(Future.force entry.Entries.const_entry_body), Option.get entry.Entries.const_entry_type ) ) (make_scheme (Array.map_to_list (fun const -> const,GType None) funs)) ) @@ -1122,16 +1121,8 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g let lem_cst = destConst (Constrintern.global_reference lem_id) in update_Function {finfo with completeness_lemma = Some lem_cst} ) - funs; - with reraise -> - (* In case of problem, we reset all the lemmas *) - Pfedit.delete_all_proofs (); - States.unfreeze previous_state; - raise reraise - - - - + funs) + () (***********************************************) diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 4b9704c2c9..68b291ff96 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -57,7 +57,8 @@ let find_reference sl s = let (declare_fun : Id.t -> logical_kind -> constr -> global_reference) = fun f_id kind value -> - let ce = {const_entry_body = value; + let ce = {const_entry_body = Future.from_val + (value, Declareops.no_seff); const_entry_secctx = None; const_entry_type = None; const_entry_opaque = false; @@ -1261,7 +1262,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_ ref_ := Some lemma ; let lid = ref [] in let h_num = ref (-1) in - ignore (Flags.silently Vernacentries.interp (Vernacexpr.VernacAbort None)); + ignore (Flags.silently Vernacentries.interp (Loc.ghost,Vernacexpr.VernacAbort None)); build_proof ( fun gls -> let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in @@ -1443,7 +1444,6 @@ let (com_eqn : int -> Id.t -> let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num eq generate_induction_principle using_lemmas : unit = - let previous_label = Lib.current_command_label () in let function_type = interp_constr Evd.empty (Global.env()) type_of_f in let env = push_named (function_name,None,function_type) (Global.env()) in (* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type); *) @@ -1513,7 +1513,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num spc () ++ str"is defined" ) ) in - try + States.with_state_protection (fun () -> com_terminate tcc_lemma_name tcc_lemma_constr @@ -1523,9 +1523,6 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num term_id using_lemmas (List.length res_vars) - hook - with reraise -> - ignore (Backtrack.backto previous_label); - (* anomaly (Pp.str "Cannot create termination Lemma") *) - raise reraise + hook) + () diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index aecbbfe856..be661587ad 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -176,7 +176,7 @@ let carg c = TacDynamic(Loc.ghost,Pretyping.constr_in c) let dummy_goal env = let (gl,_,sigma) = Goal.V82.mk_goal Evd.empty (named_context_val env) mkProp Evd.Store.empty in - {Evd.it = gl; + {Evd.it = gl; Evd.eff=Declareops.no_seff; Evd.sigma = sigma} let exec_tactic env n f args = @@ -679,8 +679,10 @@ let add_theory name rth eqth morphth cst_tac (pre,post) power sign div = let lemma1 = constr_of params.(3) in let lemma2 = constr_of params.(4) in - let lemma1 = decl_constant (Id.to_string name^"_ring_lemma1") lemma1 in - let lemma2 = decl_constant (Id.to_string name^"_ring_lemma2") lemma2 in + let lemma1 = + decl_constant (Id.to_string name^"_ring_lemma1") (Future.from_val ( lemma1,Declareops.no_seff)) in + let lemma2 = + decl_constant (Id.to_string name^"_ring_lemma2") (Future.from_val ( lemma2,Declareops.no_seff)) in let cst_tac = interp_cst_tac env sigma morphth kind (zero,one,add,mul,opp) cst_tac in let pretac = @@ -1030,11 +1032,11 @@ let add_field_theory name fth eqth morphth cst_tac inj (pre,post) power sign odi match inj with | Some thm -> mkApp(constr_of params.(8),[|thm|]) | None -> constr_of params.(7) in - let lemma1 = decl_constant (Id.to_string name^"_field_lemma1") lemma1 in - let lemma2 = decl_constant (Id.to_string name^"_field_lemma2") lemma2 in - let lemma3 = decl_constant (Id.to_string name^"_field_lemma3") lemma3 in - let lemma4 = decl_constant (Id.to_string name^"_field_lemma4") lemma4 in - let cond_lemma = decl_constant (Id.to_string name^"_lemma5") cond_lemma in + let lemma1 = decl_constant (Id.to_string name^"_field_lemma1") (Future.from_val (lemma1,Declareops.no_seff)) in + let lemma2 = decl_constant (Id.to_string name^"_field_lemma2") (Future.from_val (lemma2,Declareops.no_seff)) in + let lemma3 = decl_constant (Id.to_string name^"_field_lemma3") (Future.from_val (lemma3,Declareops.no_seff)) in + let lemma4 = decl_constant (Id.to_string name^"_field_lemma4") (Future.from_val (lemma4,Declareops.no_seff)) in + let cond_lemma = decl_constant (Id.to_string name^"_lemma5") (Future.from_val (cond_lemma,Declareops.no_seff)) in let cst_tac = interp_cst_tac env sigma morphth kind (zero,one,add,mul,opp) cst_tac in let pretac = -- cgit v1.2.3