diff options
| author | gareuselesinge | 2013-08-08 18:51:35 +0000 |
|---|---|---|
| committer | gareuselesinge | 2013-08-08 18:51:35 +0000 |
| commit | b2f2727670853183bfbcbafb9dc19f0f71494a7b (patch) | |
| tree | 8d9cea5ed2713ab2bfe3b142816a48c5ba615758 /toplevel | |
| parent | 1f48326c7edf7f6e7062633494d25b254a6db82c (diff) | |
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
Diffstat (limited to 'toplevel')
31 files changed, 1644 insertions, 838 deletions
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index 82445a0fde..e63c22bf88 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -178,23 +178,30 @@ let build_beq_scheme kn = let rec aux c = let (c,a) = Reductionops.whd_betaiota_stack Evd.empty c in match kind_of_term c with - | Rel x -> mkRel (x-nlist+ndx) - | Var x -> mkVar (Id.of_string ("eq_"^(Id.to_string x))) + | Rel x -> mkRel (x-nlist+ndx), Declareops.no_seff + | Var x -> mkVar (id_of_string ("eq_"^(string_of_id x))), Declareops.no_seff | Cast (x,_,_) -> aux (applist (x,a)) | App _ -> assert false - | Ind (kn',i as ind') -> if eq_mind kn kn' then mkRel(eqA-nlist-i+nb_ind-1) - else ( try - let a = Array.of_list a in - let eq = mkConst (find_scheme (!beq_scheme_kind_aux()) (kn',i)) - and eqa = Array.map aux a - in - let args = Array.append - (Array.map (fun x->lift lifti x) a) eqa - in if Array.equal eq_constr args [||] then eq - else mkApp (eq,Array.append - (Array.map (fun x->lift lifti x) a) eqa) - with Not_found -> raise(EqNotFound (ind',ind)) - ) + | Ind (kn',i as ind') -> + if eq_mind kn kn' then mkRel(eqA-nlist-i+nb_ind-1), Declareops.no_seff + else begin + try + let eq, eff = + let c, eff = find_scheme (!beq_scheme_kind_aux()) (kn',i) in + mkConst c, eff in + let eqa, eff = + let eqa, effs = List.split (List.map aux a) in + Array.of_list eqa, + Declareops.union_side_effects + (Declareops.flatten_side_effects (List.rev effs)) + eff in + let args = + Array.append + (Array.of_list (List.map (fun x -> lift lifti x) a)) eqa in + if Int.equal (Array.length args) 0 then eq, eff + else mkApp (eq, args), eff + with Not_found -> raise(EqNotFound (ind',ind)) + end | Sort _ -> raise InductiveWithSort | Prod _ -> raise InductiveWithProduct | Lambda _-> raise (EqUnknown "Lambda") @@ -229,6 +236,7 @@ let build_beq_scheme kn = let constrsi = constrs (3+nparrec) in let n = Array.length constrsi in let ar = Array.make n ff in + let eff = ref Declareops.no_seff in for i=0 to n-1 do let nb_cstr_args = List.length constrsi.(i).cs_args in let ar2 = Array.make n ff in @@ -240,12 +248,13 @@ let build_beq_scheme kn = | _ -> let eqs = Array.make nb_cstr_args tt in for ndx = 0 to nb_cstr_args-1 do let _,_,cc = List.nth constrsi.(i).cs_args ndx in - let eqA = compute_A_equality rel_list + let eqA, eff' = compute_A_equality rel_list nparrec (nparrec+3+2*nb_cstr_args) (nb_cstr_args+ndx+1) cc in + eff := Declareops.union_side_effects eff' !eff; Array.set eqs ndx (mkApp (eqA, [|mkRel (ndx+1+nb_cstr_args);mkRel (ndx+1)|] @@ -271,23 +280,28 @@ let build_beq_scheme kn = done; mkNamedLambda (Id.of_string "X") (mkFullInd ind (nb_ind-1+1)) ( mkNamedLambda (Id.of_string "Y") (mkFullInd ind (nb_ind-1+2)) ( - mkCase (ci, do_predicate rel_list 0,mkVar (Id.of_string "X"),ar))) + mkCase (ci, do_predicate rel_list 0,mkVar (Id.of_string "X"),ar))), + !eff in (* build_beq_scheme *) let names = Array.make nb_ind Anonymous and types = Array.make nb_ind mkSet and cores = Array.make nb_ind mkSet in + let eff = ref Declareops.no_seff in for i=0 to (nb_ind-1) do names.(i) <- Name (Id.of_string (rec_name i)); types.(i) <- mkArrow (mkFullInd (kn,i) 0) (mkArrow (mkFullInd (kn,i) 1) bb); - cores.(i) <- make_one_eq i + let c, eff' = make_one_eq i in + cores.(i) <- c; + eff := Declareops.union_side_effects eff' !eff done; Array.init nb_ind (fun i -> let kelim = Inductive.elim_sorts (mib,mib.mind_packets.(i)) in if not (List.mem InSet kelim) then raise (NonSingletonProp (kn,i)); let fix = mkFix (((Array.make nb_ind 0),i),(names,types,cores)) in - create_input fix) + create_input fix), + !eff let beq_scheme_kind = declare_mutual_scheme_object "_beq" build_beq_scheme @@ -338,8 +352,10 @@ let do_replace_lb lb_scheme_key aavoid narg gls p q = in let type_of_pq = pf_type_of gls p in let u,v = destruct_ind type_of_pq - in let lb_type_of_p = - try mkConst (find_scheme lb_scheme_key u) + in let lb_type_of_p, eff = + try + let c, eff = find_scheme lb_scheme_key u in + mkConst c, eff with Not_found -> (* spiwack: the format of this error message should probably be improved. *) @@ -357,7 +373,9 @@ let do_replace_lb lb_scheme_key aavoid narg gls p q = (Array.map (fun x -> do_arg x 2) v) in let app = if Array.equal eq_constr lb_args [||] then lb_type_of_p else mkApp (lb_type_of_p,lb_args) - in [Equality.replace p q ; apply app ; Auto.default_auto] + in + [Tactics.emit_side_effects eff; + Equality.replace p q ; apply app ; Auto.default_auto] (* used in the bool -> leib side *) let do_replace_bl bl_scheme_key ind gls aavoid narg lft rgt = @@ -396,8 +414,10 @@ let do_replace_bl bl_scheme_key ind gls aavoid narg lft rgt = in if eq_ind u ind then (Equality.replace t1 t2)::(Auto.default_auto)::(aux q1 q2) else ( - let bl_t1 = - try mkConst (find_scheme bl_scheme_key u) + let bl_t1, eff = + try + let c, eff = find_scheme bl_scheme_key u in + mkConst c, eff with Not_found -> (* spiwack: the format of this error message should probably be improved. *) @@ -418,6 +438,7 @@ let do_replace_bl bl_scheme_key ind gls aavoid narg lft rgt = let app = if Array.equal eq_constr bl_args [||] then bl_t1 else mkApp (bl_t1,bl_args) in + (Tactics.emit_side_effects eff):: (Equality.replace_by t1 t2 (tclTHEN (apply app) (Auto.default_auto)))::(aux q1 q2) ) @@ -463,16 +484,17 @@ let eqI ind l = let list_id = list_id l in let eA = Array.of_list((List.map (fun (s,_,_,_) -> mkVar s) list_id)@ (List.map (fun (_,seq,_,_)-> mkVar seq) list_id )) - and e = try mkConst (find_scheme beq_scheme_kind ind) with - Not_found -> error + and e, eff = + try let c, eff = find_scheme beq_scheme_kind ind in mkConst c, eff + with Not_found -> error ("The boolean equality on "^(string_of_mind (fst ind))^" is needed."); - in (if Array.equal eq_constr eA [||] then e else mkApp(e,eA)) + in (if Array.equal eq_constr eA [||] then e else mkApp(e,eA)), eff (**********************************************************************) (* Boolean->Leibniz *) let compute_bl_goal ind lnamesparrec nparrec = - let eqI = eqI ind lnamesparrec in + let eqI, eff = eqI ind lnamesparrec in let list_id = list_id lnamesparrec in let create_input c = let x = Id.of_string "x" and @@ -506,7 +528,7 @@ let compute_bl_goal ind lnamesparrec nparrec = mkArrow (mkApp(eq,[|bb;mkApp(eqI,[|mkVar n;mkVar m|]);tt|])) (mkApp(eq,[|mkFullInd ind (nparrec+3);mkVar n;mkVar m|])) - ))) + ))), eff let compute_bl_tact bl_scheme_key ind lnamesparrec nparrec gsig = let list_id = list_id lnamesparrec in @@ -590,9 +612,10 @@ let make_bl_scheme mind = let nparrec = mib.mind_nparams_rec in let lnonparrec,lnamesparrec = context_chop (nparams-nparrec) mib.mind_params_ctxt in - [|Pfedit.build_by_tactic (Global.env()) - (compute_bl_goal ind lnamesparrec nparrec) - (compute_bl_tact (!bl_scheme_kind_aux()) ind lnamesparrec nparrec)|] + let bl_goal, eff = compute_bl_goal ind lnamesparrec nparrec in + [|Pfedit.build_by_tactic (Global.env()) bl_goal + (compute_bl_tact (!bl_scheme_kind_aux()) ind lnamesparrec nparrec)|], + eff let bl_scheme_kind = declare_mutual_scheme_object "_dec_bl" make_bl_scheme @@ -603,7 +626,7 @@ let _ = bl_scheme_kind_aux := fun () -> bl_scheme_kind let compute_lb_goal ind lnamesparrec nparrec = let list_id = list_id lnamesparrec in - let eqI = eqI ind lnamesparrec in + let eqI, eff = eqI ind lnamesparrec in let create_input c = let x = Id.of_string "x" and y = Id.of_string "y" in @@ -636,7 +659,7 @@ let compute_lb_goal ind lnamesparrec nparrec = mkArrow (mkApp(eq,[|mkFullInd ind (nparrec+2);mkVar n;mkVar m|])) (mkApp(eq,[|bb;mkApp(eqI,[|mkVar n;mkVar m|]);tt|])) - ))) + ))), eff let compute_lb_tact lb_scheme_key ind lnamesparrec nparrec gsig = let list_id = list_id lnamesparrec in @@ -702,9 +725,10 @@ let make_lb_scheme mind = let nparrec = mib.mind_nparams_rec in let lnonparrec,lnamesparrec = context_chop (nparams-nparrec) mib.mind_params_ctxt in - [|Pfedit.build_by_tactic (Global.env()) - (compute_lb_goal ind lnamesparrec nparrec) - (compute_lb_tact (!lb_scheme_kind_aux()) ind lnamesparrec nparrec)|] + let lb_goal, eff = compute_lb_goal ind lnamesparrec nparrec in + [|Pfedit.build_by_tactic (Global.env()) lb_goal + (compute_lb_tact (!lb_scheme_kind_aux()) ind lnamesparrec nparrec)|], + eff let lb_scheme_kind = declare_mutual_scheme_object "_dec_lb" make_lb_scheme @@ -771,7 +795,7 @@ let compute_dec_goal ind lnamesparrec nparrec = let compute_dec_tact ind lnamesparrec nparrec gsig = let list_id = list_id lnamesparrec in - let eqI = eqI ind lnamesparrec in + let eqI, eff = eqI ind lnamesparrec in let avoid = ref [] in let eqtrue x = mkApp(eq,[|bb;x;tt|]) in let eqfalse x = mkApp(eq,[|bb;x;ff|]) in @@ -793,17 +817,22 @@ let compute_dec_tact ind lnamesparrec nparrec gsig = avoid := freshH::(!avoid); let arfresh = Array.of_list fresh_first_intros in let xargs = Array.sub arfresh 0 (2*nparrec) in - let blI = try mkConst (find_scheme bl_scheme_kind ind) with + let blI, eff' = + try let c, eff = find_scheme bl_scheme_kind ind in mkConst c, eff with Not_found -> error ( "Error during the decidability part, boolean to leibniz"^ " equality is required.") in - let lbI = try mkConst (find_scheme lb_scheme_kind ind) with + let lbI, eff'' = + try let c, eff = find_scheme lb_scheme_kind ind in mkConst c, eff with Not_found -> error ( "Error during the decidability part, leibniz to boolean"^ " equality is required.") in tclTHENSEQ [ + Tactics.emit_side_effects + (Declareops.union_side_effects eff'' + (Declareops.union_side_effects eff' eff)); intros_using fresh_first_intros; intros_using [freshn;freshm]; (*we do this so we don't have to prove the same goal twice *) @@ -859,7 +888,7 @@ let make_eq_decidability mind = context_chop (nparams-nparrec) mib.mind_params_ctxt in [|Pfedit.build_by_tactic (Global.env()) (compute_dec_goal ind lnamesparrec nparrec) - (compute_dec_tact ind lnamesparrec nparrec)|] + (compute_dec_tact ind lnamesparrec nparrec)|], Declareops.no_seff let eq_dec_scheme_kind = declare_mutual_scheme_object "_eq_dec" make_eq_decidability diff --git a/toplevel/auto_ind_decl.mli b/toplevel/auto_ind_decl.mli index b05f94c3c6..660f6f7e72 100644 --- a/toplevel/auto_ind_decl.mli +++ b/toplevel/auto_ind_decl.mli @@ -30,17 +30,17 @@ exception ParameterWithoutEquality of constant exception NonSingletonProp of inductive val beq_scheme_kind : mutual scheme_kind -val build_beq_scheme : mutual_inductive -> constr array +val build_beq_scheme : mutual_inductive -> constr array * Declareops.side_effects (** {6 Build equivalence between boolean equality and Leibniz equality } *) val lb_scheme_kind : mutual scheme_kind -val make_lb_scheme : mutual_inductive -> constr array +val make_lb_scheme : mutual_inductive -> constr array * Declareops.side_effects val bl_scheme_kind : mutual scheme_kind -val make_bl_scheme : mutual_inductive -> constr array +val make_bl_scheme : mutual_inductive -> constr array * Declareops.side_effects (** {6 Build decidability of equality } *) val eq_dec_scheme_kind : mutual scheme_kind -val make_eq_decidability : mutual_inductive -> constr array +val make_eq_decidability : mutual_inductive -> constr array * Declareops.side_effects diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml index 049d631bf8..e9601c1232 100644 --- a/toplevel/autoinstance.ml +++ b/toplevel/autoinstance.ml @@ -187,7 +187,7 @@ let declare_record_instance gr ctx params = let ident = make_instance_ident gr in let def = it_mkLambda_or_LetIn (applistc (constr_of_global gr) params) ctx in let def = deep_refresh_universes def in - let ce = { const_entry_body= def; + let ce = { const_entry_body= Future.from_val (def,Declareops.no_seff); const_entry_secctx = None; const_entry_type=None; const_entry_opaque=false; @@ -204,9 +204,9 @@ let declare_class_instance gr ctx params = let def = deep_refresh_universes def in let typ = deep_refresh_universes typ in let ce = Entries.DefinitionEntry - { const_entry_type = Some typ; + { const_entry_type= Some typ; + const_entry_body= Future.from_val (def,Declareops.no_seff); const_entry_secctx = None; - const_entry_body = def; const_entry_opaque = false; const_entry_inline_code = false } in try diff --git a/toplevel/backtrack.ml b/toplevel/backtrack.ml deleted file mode 100644 index e259da7af0..0000000000 --- a/toplevel/backtrack.ml +++ /dev/null @@ -1,234 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Util -open Names -open Vernacexpr - -(** Command history stack - - We maintain a stack of the past states of the system. Each - successfully interpreted command adds an [info] element - to this stack, storing what were the (label / current proof / ...) - just _after_ the interpretation of this command. - - - A label is just an integer, starting from Lib.first_command_label - initially, and incremented at each new successful command. - - If some proofs are opened, we have their number in [nproofs], - the name of the current proof in [prfname], the current depth in - [prfdepth]. - - Otherwise, [nproofs = 0], [prfname = None], [prfdepth = 0] - - The text of the command is stored (for Show Script currently). - - A command can be tagged later as non-"reachable" when the current proof - at the time of this command has been ended by Qed/Abort/Restart, - meaning we can't backtrack there. -*) - -type info = { - label : int; - nproofs : int; - prfname : Id.t option; - prfdepth : int; - ngoals : int; - cmd : vernac_expr; - mutable reachable : bool; -} - -let history : info Stack.t = Stack.create () - -(** Is this stack active (i.e. nonempty) ? - The stack is currently inactive when compiling files (coqc). *) - -let is_active () = not (Stack.is_empty history) - -(** For debug purpose, a dump of the history *) - -let dump_history () = - let l = ref [] in - Stack.iter (fun i -> l:=i::!l) history; - !l - -(** Basic manipulation of the command history stack *) - -exception Invalid - -let pop () = ignore (Stack.pop history) - -let npop n = - (* Since our history stack always contains an initial entry, - it's invalid to try to completely empty it *) - if n < 0 || n >= Stack.length history then raise Invalid - else for _i = 1 to n do pop () done - -let top () = - try Stack.top history with Stack.Empty -> raise Invalid - -(** Search the history stack for a suitable location. We perform first - a non-destructive search: in case of search failure, the stack is - unchanged. *) - -exception Found of info - -let search test = - try - Stack.iter (fun i -> if test i then raise (Found i)) history; - raise Invalid - with Found i -> - while i != Stack.top history do pop () done - -(** An auxiliary function to retrieve the number of remaining subgoals *) - -let get_ngoals () = - try - let prf = Proof_global.give_me_the_proof () in - List.length (Evd.sig_it (Proof.V82.background_subgoals prf)) - with Proof_global.NoCurrentProof -> 0 - -(** Register the end of a command and store the current state *) - -let mark_command ast = - Lib.add_frozen_state(); - Lib.mark_end_of_command(); - Stack.push - { label = Lib.current_command_label (); - nproofs = List.length (Pfedit.get_all_proof_names ()); - prfname = - (try Some (Pfedit.get_current_proof_name ()) - with Proof_global.NoCurrentProof -> None); - prfdepth = max 0 (Pfedit.current_proof_depth ()); - reachable = true; - ngoals = get_ngoals (); - cmd = ast } - history - -(** Backtrack by aborting [naborts] proofs, then setting proof-depth back to - [pnum] and finally going to state number [snum]. *) - -let raw_backtrack snum pnum naborts = - for _i = 1 to naborts do Pfedit.delete_current_proof () done; - Pfedit.undo_todepth pnum; - Lib.reset_label snum - -(** Re-sync the state of the system (label, proofs) with the top - of the history stack. We may end on some earlier state to avoid - re-opening proofs. This function will return the final label - and the number of extra backtracking steps performed. *) - -let sync nb_opened_proofs = - (* Backtrack by enough additional steps to avoid re-opening proofs. - Typically, when a Qed has been crossed, we backtrack to the proof start. - NB: We cannot reach the empty stack, since the first entry in the - stack has no opened proofs and is tagged as reachable. - *) - let extra = ref 0 in - while not (top()).reachable do incr extra; pop () done; - let target = top () - in - (* Now the opened proofs at target is a subset of the opened proofs before - the backtrack, we simply abort the extra proofs (if any). - NB: It is critical here that proofs are nested in a regular way - (i.e. no more Resume or Suspend commands as earlier). This way, we can - simply count the extra proofs to abort instead of taking care of their - names. - *) - let naborts = nb_opened_proofs - target.nproofs in - (* We are now ready to do a low-level backtrack *) - raw_backtrack target.label target.prfdepth naborts; - (target.label, !extra) - -(** Backtracking by a certain number of (non-state-preserving) commands. - This is used by Coqide. - It may actually undo more commands than asked : for instance instead - of jumping back in the middle of a finished proof, we jump back before - this proof. The number of extra backtracked command is returned at - the end. *) - -let back count = - if Int.equal count 0 then 0 - else - let nb_opened_proofs = List.length (Pfedit.get_all_proof_names ()) in - npop count; - snd (sync nb_opened_proofs) - -(** Backtracking to a certain state number, and reset proofs accordingly. - We may end on some earlier state if needed to avoid re-opening proofs. - Return the final state number. *) - -let backto snum = - if Int.equal snum (Lib.current_command_label ()) then snum - else - let nb_opened_proofs = List.length (Pfedit.get_all_proof_names ()) in - search (fun i -> Int.equal i.label snum); - fst (sync nb_opened_proofs) - -(** Old [Backtrack] code with corresponding update of the history stack. - [Backtrack] is now deprecated (in favor of [BackTo]) but is kept for - compatibility with ProofGeneral. It's completely up to ProofGeneral - to decide where to go and how to adapt proofs. Note that the choices - of ProofGeneral are currently not always perfect (for instance when - backtracking an Undo). *) - -let backtrack snum pnum naborts = - raw_backtrack snum pnum naborts; - search (fun i -> Int.equal i.label snum) - -(** [reset_initial] resets the system and clears the command history - stack, only pushing back the initial entry. It should be equivalent - to [backto n0] where [n0] is the first label stored in the history. - Note that there might be other labels before [n0] in the libstack, - created during evaluation of .coqrc or initial Load's. *) - -let reset_initial () = - let n = Stack.length history in - npop (n-1); - Pfedit.delete_all_proofs (); - Lib.reset_label (top ()).label - -(** Reset to the last known state just before defining [id] *) - -let reset_name id = - let lbl = - try Lib.label_before_name id with Not_found -> raise Invalid - in - ignore (backto lbl) - -(** When a proof is ended (via either Qed/Admitted/Restart/Abort), - old proof steps should be marked differently to avoid jumping back - to them: - - either this proof isn't there anymore in the proof engine - - either it's there but it's a more recent attempt after a Restart, - so we shouldn't mix the two. - We also mark as unreachable the proof steps cancelled via a Undo. *) - -let mark_unreachable ?(after=0) prf_lst = - let fix i = match i.prfname with - | None -> raise Not_found (* stop hacking the history outside of proofs *) - | Some p -> - if List.mem p prf_lst && i.prfdepth > after - then i.reachable <- false - in - try Stack.iter fix history with Not_found -> () - -(** Parse the history stack for printing the script of a proof *) - -let get_script prf = - let script = ref [] in - let select i = match i.prfname with - | None -> raise Not_found - | Some p when Id.equal p prf && i.reachable -> script := i :: !script - | _ -> () - in - (try Stack.iter select history with Not_found -> ()); - (* Get rid of intermediate commands which don't grow the proof depth *) - let rec filter n = function - | [] -> [] - | {prfdepth=d; cmd=c; ngoals=ng}::l when n < d -> (c,ng) :: filter d l - | {prfdepth=d}::l -> filter d l - in - (* initial proof depth (after entering the lemma statement) is 1 *) - filter 1 !script diff --git a/toplevel/backtrack.mli b/toplevel/backtrack.mli deleted file mode 100644 index d4ac7cc619..0000000000 --- a/toplevel/backtrack.mli +++ /dev/null @@ -1,101 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(** Command history stack - - We maintain a stack of the past states of the system after each - (non-state-preserving) interpreted commands -*) - -(** [mark_command ast] marks the end of a command: - - it stores a frozen state and a end of command in the Lib stack, - - it stores the current state information in the command history - stack *) - -val mark_command : Vernacexpr.vernac_expr -> unit - -(** Is this history stack active (i.e. nonempty) ? - The stack is currently inactive when compiling files (coqc). *) - -val is_active : unit -> bool - -(** The [Invalid] exception is raised when one of the following function - tries to empty the history stack, or reach an unknown states, etc. - The stack is preserved in these cases. *) - -exception Invalid - -(** Nota Bene: it is critical for the following functions that proofs - are nested in a regular way (i.e. no more Resume or Suspend commands - as earlier). *) - -(** Backtracking by a certain number of (non-state-preserving) commands. - This is used by Coqide. - It may actually undo more commands than asked : for instance instead - of jumping back in the middle of a finished proof, we jump back before - this proof. The number of extra backtracked command is returned at - the end. *) - -val back : int -> int - -(** Backtracking to a certain state number, and reset proofs accordingly. - We may end on some earlier state if needed to avoid re-opening proofs. - Return the state number on which we finally end. *) - -val backto : int -> int - -(** Old [Backtrack] code with corresponding update of the history stack. - [Backtrack] is now deprecated (in favor of [BackTo]) but is kept for - compatibility with ProofGeneral. It's completely up to ProofGeneral - to decide where to go and how to adapt proofs. Note that the choices - of ProofGeneral are currently not always perfect (for instance when - backtracking an Undo). *) - -val backtrack : int -> int -> int -> unit - -(** [reset_initial] resets the system and clears the command history - stack, only pushing back the initial entry. It should be equivalent - to [backto n0] where [n0] is the first label stored in the history. - Note that there might be other labels before [n0] in the libstack, - created during evaluation of .coqrc or initial Load's. *) - -val reset_initial : unit -> unit - -(** Reset to the last known state just before defining [id] *) - -val reset_name : Names.Id.t Loc.located -> unit - -(** When a proof is ended (via either Qed/Admitted/Restart/Abort), - old proof steps should be marked differently to avoid jumping back - to them: - - either this proof isn't there anymore in the proof engine - - either a proof with the same name is there, but it's a more recent - attempt after a Restart/Abort, we shouldn't mix the two. - We also mark as unreachable the proof steps cancelled via a Undo. -*) - -val mark_unreachable : ?after:int -> Names.Id.t list -> unit - -(** Parse the history stack for printing the script of a proof *) - -val get_script : Names.Id.t -> (Vernacexpr.vernac_expr * int) list - - -(** For debug purpose, a dump of the history *) - -type info = { - label : int; - nproofs : int; - prfname : Names.Id.t option; - prfdepth : int; - ngoals : int; - cmd : Vernacexpr.vernac_expr; - mutable reachable : bool; -} - -val dump_history : unit -> info list diff --git a/toplevel/class.ml b/toplevel/class.ml index 14473e46f8..f9ce75bba7 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -217,7 +217,8 @@ let build_id_coercion idf_opt source = in let constr_entry = (* Cast is necessary to express [val_f] is identity *) DefinitionEntry - { const_entry_body = mkCast (val_f, DEFAULTcast, typ_f); + { const_entry_body = Future.from_val + (mkCast (val_f, DEFAULTcast, typ_f),Declareops.no_seff); const_entry_secctx = None; const_entry_type = Some typ_f; const_entry_opaque = false; diff --git a/toplevel/classes.ml b/toplevel/classes.ml index e4064049eb..a217abbba0 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -103,7 +103,7 @@ let instance_hook k pri global imps ?hook cst = let declare_instance_constant k pri global imps ?hook id term termtype = let kind = IsDefinition Instance in let entry = { - const_entry_body = term; + const_entry_body = Future.from_val term; const_entry_secctx = None; const_entry_type = Some termtype; const_entry_opaque = false; @@ -273,7 +273,8 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props let evm = Evarutil.nf_evar_map_undefined !evars in let evm = undefined_evars evm in if Evd.is_empty evm && not (Option.is_empty term) then - declare_instance_constant k pri global imps ?hook id (Option.get term) termtype + declare_instance_constant k pri global imps ?hook id + (Option.get term,Declareops.no_seff) termtype else begin let kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Instance in if Flags.is_program_mode () then diff --git a/toplevel/classes.mli b/toplevel/classes.mli index 1d9ae6ec42..5a0dc97c24 100644 --- a/toplevel/classes.mli +++ b/toplevel/classes.mli @@ -42,7 +42,7 @@ val declare_instance_constant : Impargs.manual_explicitation list -> (** implicits *) ?hook:(Globnames.global_reference -> unit) -> Id.t -> (** name *) - Term.constr -> (** body *) + Entries.proof_output -> (** body *) Term.types -> (** type *) Names.Id.t diff --git a/toplevel/command.ml b/toplevel/command.ml index 369abd3f87..d730d8ef11 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -67,9 +67,11 @@ let rec complete_conclusion a cs = function let red_constant_entry n ce = function | None -> ce | Some red -> - let body = ce.const_entry_body in - { ce with const_entry_body = - under_binders (Global.env()) (fst (reduction_of_red_expr red)) n body } + let proof_out = ce.const_entry_body in + { ce with const_entry_body = Future.chain ~id:"red_constant_entry" + proof_out (fun (body,eff) -> + under_binders (Global.env()) + (fst (reduction_of_red_expr red)) n body,eff) } let interp_definition bl red_option c ctypopt = let env = Global.env() in @@ -82,7 +84,7 @@ let interp_definition bl red_option c ctypopt = let c, imps2 = interp_constr_evars_impls ~impls evdref env_bl c in let body = nf_evar !evdref (it_mkLambda_or_LetIn c ctx) in imps1@(Impargs.lift_implicits nb_args imps2), - { const_entry_body = body; + { const_entry_body = Future.from_val (body,Declareops.no_seff); const_entry_secctx = None; const_entry_type = None; const_entry_opaque = false; @@ -100,7 +102,7 @@ let interp_definition bl red_option c ctypopt = then msg_warning (strbrk "Implicit arguments declaration relies on type." ++ spc () ++ strbrk "The term declares more implicits than the type here."); imps1@(Impargs.lift_implicits nb_args impsty), - { const_entry_body = body; + { const_entry_body = Future.from_val(body,Declareops.no_seff); const_entry_secctx = None; const_entry_type = Some typ; const_entry_opaque = false; @@ -135,7 +137,7 @@ let declare_definition_hook = ref ignore let set_declare_definition_hook = (:=) declare_definition_hook let get_declare_definition_hook () = !declare_definition_hook -let declare_definition ident (local, k) ce imps hook = +let declare_definition ident (local,k) ce imps hook = let () = !declare_definition_hook ce in let r = match local with | Discharge when Lib.sections_are_opened () -> @@ -158,7 +160,8 @@ let do_definition ident k bl red_option c ctypopt hook = let (ce, evd, imps as def) = interp_definition bl red_option c ctypopt in if Flags.is_program_mode () then let env = Global.env () in - let c = ce.const_entry_body in + let c,sideff = Future.force ce.const_entry_body in + assert(sideff = Declareops.no_seff); let typ = match ce.const_entry_type with | Some t -> t | None -> Retyping.get_type_of env evd c @@ -173,7 +176,7 @@ let do_definition ident k bl red_option c ctypopt hook = (* 2| Variable/Hypothesis/Parameter/Axiom declarations *) -let declare_assumption is_coe (local,kind) c imps impl nl (_,ident) = match local with +let declare_assumption is_coe (local, kind) c imps impl nl (_,ident) = match local with | Discharge when Lib.sections_are_opened () -> let decl = (Lib.cwd(), SectionLocalAssum (c,impl), IsAssumption kind) in let _ = declare_variable ident decl in @@ -521,7 +524,7 @@ let build_fix_type (_,ctx) ccl = it_mkProd_or_LetIn ccl ctx let declare_fix kind f def t imps = let ce = { - const_entry_body = def; + const_entry_body = Future.from_val def; const_entry_secctx = None; const_entry_type = Some t; const_entry_opaque = false; @@ -712,7 +715,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation = let body = it_mkLambda_or_LetIn (mkApp (constr_of_global gr, [|make|])) binders_rel in let ty = it_mkProd_or_LetIn top_arity binders_rel in let ce = - { const_entry_body = Evarutil.nf_evar !evdref body; + { const_entry_body = Future.from_val (Evarutil.nf_evar !evdref body,Declareops.no_seff); const_entry_secctx = None; const_entry_type = Some ty; const_entry_opaque = false; @@ -824,10 +827,12 @@ let declare_fixpoint local ((fixnames,fixdefs,fixtypes),fiximps) indexes ntns = (* We shortcut the proof process *) let fixdefs = List.map Option.get fixdefs in let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in - let indexes = search_guard Loc.ghost (Global.env()) indexes fixdecls in + let env = Global.env() in + let indexes = search_guard Loc.ghost env indexes fixdecls in let fiximps = List.map (fun (n,r,p) -> r) fiximps in let fixdecls = List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in + let fixdecls = List.map (fun c -> c, Declareops.no_seff) fixdecls in ignore (List.map4 (declare_fix (local, Fixpoint)) fixnames fixdecls fixtypes fiximps); (* Declare the recursive definitions *) fixpoint_message (Some indexes) fixnames; @@ -850,6 +855,7 @@ let declare_cofixpoint local ((fixnames,fixdefs,fixtypes),fiximps) ntns = let fixdefs = List.map Option.get fixdefs in let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in + let fixdecls = List.map (fun c-> c,Declareops.no_seff) fixdecls in let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in ignore (List.map4 (declare_fix (local, CoFixpoint)) fixnames fixdecls fixtypes fiximps); (* Declare the recursive definitions *) diff --git a/toplevel/command.mli b/toplevel/command.mli index 71eec32958..76a3c58027 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -150,4 +150,4 @@ val do_cofixpoint : val check_mutuality : Environ.env -> bool -> (Id.t * types) list -> unit val declare_fix : definition_kind -> Id.t -> - constr -> types -> Impargs.manual_implicits -> global_reference + Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index cb587a6efa..1dba380016 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -282,7 +282,7 @@ let parse_args arglist = | "-debug" :: rem -> set_debug (); parse rem - | "-time" :: rem -> Vernac.time := true; parse rem + | "-time" :: rem -> Flags.time := true; parse rem | "-compat" :: v :: rem -> Flags.compat_version := get_compat_version v; parse rem @@ -390,6 +390,7 @@ let init arglist = load_vernac_obj (); require (); load_rcfile(); + Stm.init (); load_vernacular (); compile_files (); outputstate () @@ -407,9 +408,7 @@ let init arglist = Pp.ppnl (with_option raw_print Prettyp.print_full_pure_context ()); Profile.print_profile (); exit 0 - end; - (* We initialize the command history stack with a first entry *) - Backtrack.mark_command Vernacexpr.VernacNop + end let init_toplevel = init diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml index 709062f1f6..8218302038 100644 --- a/toplevel/ide_slave.ml +++ b/toplevel/ide_slave.ml @@ -104,10 +104,8 @@ let coqide_cmd_checks (loc,ast) = if is_debug ast then user_error "Debug mode not available within CoqIDE"; if is_known_option ast then - user_error "Use CoqIDE display menu instead"; - if Vernac.is_navigation_vernac ast then - user_error "Use CoqIDE navigation instead"; - if is_undo ast then + msg_warning (strbrk"This will not work. Use CoqIDE display menu instead"); + if Vernac.is_navigation_vernac ast || is_undo ast then msg_warning (strbrk "Rather use CoqIDE navigation instead"); if is_query ast then msg_warning (strbrk "Query commands should not be inserted in scripts") @@ -120,10 +118,14 @@ let interp (id,raw,verbosely,s) = let loc_ast = Vernac.parse_sentence (pa,None) in if not raw then coqide_cmd_checks loc_ast; Flags.make_silent (not verbosely); - Vernac.eval_expr ~preserving:raw loc_ast; + if id = 0 then Vernac.eval_expr (loc, VernacStm (Command ast)) + else Vernac.eval_expr loc_ast; Flags.make_silent true; - Pp.feedback Interface.Processed; - read_stdout () + Stm.get_current_state (), read_stdout () + +let backto id = + Vernac.eval_expr (Loc.ghost, + VernacStm (Command (VernacBackTo (Stateid.int_of_state_id id)))) (** Goal display *) @@ -252,7 +254,7 @@ let status () = Interface.status_proofname = proof; Interface.status_allproofs = allproofs; Interface.status_statenum = Lib.current_command_label (); - Interface.status_proofnum = Pfedit.current_proof_depth (); + Interface.status_proofnum = Stm.current_proof_depth (); } let search flags = Search.interface_search flags @@ -277,6 +279,17 @@ let about () = { Interface.compile_date = Coq_config.compile_date; } +let handle_exn e = + let dummy = Stateid.dummy_state_id in + let loc_of e = match Loc.get_loc e with + | Some loc when not (Loc.is_ghost loc) -> Some (Loc.unloc loc) + | _ -> None in + let mk_msg e = read_stdout ()^"\n"^string_of_ppcmds (Errors.print e) in + match e with + | Errors.Drop -> dummy, None, "Drop is not allowed by coqide!" + | Errors.Quit -> dummy, None, "Quit is not allowed by coqide!" + | e -> dummy, loc_of e, mk_msg e + (** When receiving the Quit call, we don't directly do an [exit 0], but rather set this reference, in order to send a final answer before exiting. *) @@ -307,7 +320,7 @@ let eval_call c = in let handler = { Interface.interp = interruptible interp; - Interface.rewind = interruptible Backtrack.back; + Interface.rewind = interruptible (fun _ -> 0); Interface.goals = interruptible goals; Interface.evars = interruptible evars; Interface.hints = interruptible hints; diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml index f55a12f9d4..0a5f7d25f9 100644 --- a/toplevel/ind_tables.ml +++ b/toplevel/ind_tables.ml @@ -27,8 +27,8 @@ open Decl_kinds (**********************************************************************) (* Registering schemes in the environment *) -type mutual_scheme_object_function = mutual_inductive -> constr array -type individual_scheme_object_function = inductive -> constr +type mutual_scheme_object_function = mutual_inductive -> constr array * Declareops.side_effects +type individual_scheme_object_function = inductive -> constr * Declareops.side_effects type 'a scheme_kind = string @@ -67,8 +67,8 @@ type individual type mutual type scheme_object_function = - | MutualSchemeFunction of (mutual_inductive -> constr array) - | IndividualSchemeFunction of (inductive -> constr) + | MutualSchemeFunction of (mutual_inductive -> constr array * Declareops.side_effects) + | IndividualSchemeFunction of (inductive -> constr * Declareops.side_effects) let scheme_object_table = (Hashtbl.create 17 : (string, string * scheme_object_function) Hashtbl.t) @@ -113,7 +113,7 @@ let define internal id c = let fd = declare_constant ~internal in let id = compute_name internal id in let entry = { - const_entry_body = c; + const_entry_body = Future.from_val (c,Declareops.no_seff); const_entry_secctx = None; const_entry_type = None; const_entry_opaque = false; @@ -127,14 +127,14 @@ let define internal id c = kn let define_individual_scheme_base kind suff f internal idopt (mind,i as ind) = - let c = f ind in + let c, eff = f ind in let mib = Global.lookup_mind mind in let id = match idopt with | Some id -> id | None -> add_suffix mib.mind_packets.(i).mind_typename suff in let const = define internal id c in declare_scheme kind [|ind,const|]; - const + const, Declareops.cons_side_effects (Safe_typing.sideff_of_con (Global.safe_env()) const) eff let define_individual_scheme kind internal names (mind,i as ind) = match Hashtbl.find scheme_object_table kind with @@ -143,14 +143,19 @@ let define_individual_scheme kind internal names (mind,i as ind) = define_individual_scheme_base kind s f internal names ind let define_mutual_scheme_base kind suff f internal names mind = - let cl = f mind in + let cl, eff = f mind in let mib = Global.lookup_mind mind in let ids = Array.init (Array.length mib.mind_packets) (fun i -> try List.assoc i names with Not_found -> add_suffix mib.mind_packets.(i).mind_typename suff) in let consts = Array.map2 (define internal) ids cl in declare_scheme kind (Array.mapi (fun i cst -> ((mind,i),cst)) consts); - consts + consts, + Declareops.union_side_effects eff + (Declareops.side_effects_of_list + (List.map + (fun x -> Safe_typing.sideff_of_con (Global.safe_env()) x) + (Array.to_list consts))) let define_mutual_scheme kind internal names mind = match Hashtbl.find scheme_object_table kind with @@ -159,13 +164,16 @@ let define_mutual_scheme kind internal names mind = define_mutual_scheme_base kind s f internal names mind let find_scheme kind (mind,i as ind) = - try String.Map.find kind (Indmap.find ind !scheme_map) + try + let s = String.Map.find kind (Indmap.find ind !scheme_map) in + s, Declareops.no_seff with Not_found -> match Hashtbl.find scheme_object_table kind with | s,IndividualSchemeFunction f -> define_individual_scheme_base kind s f KernelSilent None ind | s,MutualSchemeFunction f -> - (define_mutual_scheme_base kind s f KernelSilent [] mind).(i) + let ca, eff = define_mutual_scheme_base kind s f KernelSilent [] mind in + ca.(i), eff let check_scheme kind ind = try let _ = String.Map.find kind (Indmap.find ind !scheme_map) in true diff --git a/toplevel/ind_tables.mli b/toplevel/ind_tables.mli index 9dd25c63e2..c5e82e2e2f 100644 --- a/toplevel/ind_tables.mli +++ b/toplevel/ind_tables.mli @@ -22,8 +22,10 @@ type mutual type individual type 'a scheme_kind -type mutual_scheme_object_function = mutual_inductive -> constr array -type individual_scheme_object_function = inductive -> constr +type mutual_scheme_object_function = + mutual_inductive -> constr array * Declareops.side_effects +type individual_scheme_object_function = + inductive -> constr * Declareops.side_effects (** Main functions to register a scheme builder *) @@ -31,7 +33,8 @@ val declare_mutual_scheme_object : string -> ?aux:string -> mutual_scheme_object_function -> mutual scheme_kind val declare_individual_scheme_object : string -> ?aux:string -> - individual_scheme_object_function -> individual scheme_kind + individual_scheme_object_function -> + individual scheme_kind (* val declare_scheme : 'a scheme_kind -> (inductive * constant) array -> unit @@ -41,12 +44,12 @@ val declare_scheme : 'a scheme_kind -> (inductive * constant) array -> unit val define_individual_scheme : individual scheme_kind -> Declare.internal_flag (** internal *) -> - Id.t option -> inductive -> constant + Id.t option -> inductive -> constant * Declareops.side_effects val define_mutual_scheme : mutual scheme_kind -> Declare.internal_flag (** internal *) -> - (int * Id.t) list -> mutual_inductive -> constant array + (int * Id.t) list -> mutual_inductive -> constant array * Declareops.side_effects (** Main function to retrieve a scheme in the cache or to generate it *) -val find_scheme : 'a scheme_kind -> inductive -> constant +val find_scheme : 'a scheme_kind -> inductive -> constant * Declareops.side_effects val check_scheme : 'a scheme_kind -> inductive -> bool diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index 8551c2038d..bf07156f73 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -355,7 +355,8 @@ let do_mutual_induction_scheme lnamedepindsort = let declare decl fi lrecref = let decltype = Retyping.get_type_of env0 Evd.empty decl in let decltype = refresh_universes decltype in - let cst = define fi UserVerbose decl (Some decltype) in + let proof_output = Future.from_val (decl,Declareops.no_seff) in + let cst = define fi UserVerbose proof_output (Some decltype) in ConstRef cst :: lrecref in let _ = List.fold_right2 declare listdecl lrecnames [] in @@ -449,8 +450,10 @@ let do_combined_scheme name schemes = with Not_found -> error ((string_of_qualid (snd qualid))^" is not declared.")) schemes in - let body,typ = build_combined_scheme (Global.env ()) csts in - ignore (define (snd name) UserVerbose body (Some typ)); + let env = Global.env () in + let body,typ = build_combined_scheme env csts in + let proof_output = Future.from_val (body,Declareops.no_seff) in + ignore (define (snd name) UserVerbose proof_output (Some typ)); fixpoint_message None [snd name] (**********************************************************************) diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml index 695426d56a..6876483a05 100644 --- a/toplevel/lemmas.ml +++ b/toplevel/lemmas.ml @@ -48,17 +48,22 @@ let adjust_guardness_conditions const = function | [] -> const (* Not a recursive statement *) | possible_indexes -> (* Try all combinations... not optimal *) - match kind_of_term const.const_entry_body with - | Fix ((nv,0),(_,_,fixdefs as fixdecls)) -> + (* XXX bug ignore(Future.join const.const_entry_body); *) + { const with const_entry_body = + Future.chain ~id:"adjust_guardness_conditions" const.const_entry_body + (fun (body, eff) -> + match kind_of_term body with + | Fix ((nv,0),(_,_,fixdefs as fixdecls)) -> (* let possible_indexes = List.map2 (fun i c -> match i with Some i -> i | None -> List.interval 0 (List.length ((lam_assum c)))) lemma_guard (Array.to_list fixdefs) in *) - let indexes = - search_guard Loc.ghost (Global.env()) possible_indexes fixdecls in - { const with const_entry_body = mkFix ((indexes,0),fixdecls) } - | c -> const + let indexes = + search_guard Loc.ghost (Global.env()) + possible_indexes fixdecls in + mkFix ((indexes,0),fixdecls), eff + | _ -> body, eff) } let find_mutually_recursive_statements thms = let n = List.length thms in @@ -159,7 +164,7 @@ let look_for_possibly_mutual_statements = function (* Saving a goal *) -let save id const do_guard (locality,kind) hook = +let save ?proof id const do_guard (locality,kind) hook = let const = adjust_guardness_conditions const do_guard in let k = Kindops.logical_kind_of_goal_kind kind in let l,r = match locality with @@ -175,7 +180,8 @@ let save id const do_guard (locality,kind) hook = let kn = declare_constant id ~local (DefinitionEntry const, k) in Autoinstance.search_declaration (ConstRef kn); (locality, ConstRef kn) in - Pfedit.delete_current_proof (); + (* if the proof is given explicitly, nothing has to be deleted *) + if proof = None then Pfedit.delete_current_proof (); definition_message id; hook l r @@ -220,7 +226,8 @@ let save_remaining_recthms (locality,kind) body opaq i (id,(t_i,(_,imps))) = | _ -> anomaly (Pp.str "Not a proof by induction") in match locality with | Discharge -> - let const = { const_entry_body = body_i; + let const = { const_entry_body = + Future.from_val (body_i,Declareops.no_seff); const_entry_secctx = None; const_entry_type = Some t_i; const_entry_opaque = opaq; @@ -235,7 +242,8 @@ let save_remaining_recthms (locality,kind) body opaq i (id,(t_i,(_,imps))) = | Global -> false | Discharge -> assert false in - let const = { const_entry_body = body_i; + let const = { const_entry_body = + Future.from_val (body_i,Declareops.no_seff); const_entry_secctx = None; const_entry_type = Some t_i; const_entry_opaque = opaq; @@ -247,37 +255,32 @@ let save_remaining_recthms (locality,kind) body opaq i (id,(t_i,(_,imps))) = let save_hook = ref ignore let set_save_hook f = save_hook := f -let get_proof opacity = - let id,(const,do_guard,persistence,hook) = Pfedit.cook_proof !save_hook in +let get_proof ?proof opacity = + let id,(const,do_guard,persistence,hook) = + match proof with + | None -> Pfedit.cook_proof !save_hook + | Some p -> Pfedit.cook_this_proof !save_hook p in id,{const with const_entry_opaque = opacity},do_guard,persistence,hook -let save_named opacity = - let p = Proof_global.give_me_the_proof () in - Proof.transaction p begin fun () -> - let id,const,do_guard,persistence,hook = get_proof opacity in - save id const do_guard persistence hook - end +let save_named ?proof opacity = + let id,const,do_guard,persistence,hook = get_proof ?proof opacity in + save ?proof id const do_guard persistence hook let check_anonymity id save_ident = if not (String.equal (atompart_of_id id) (Id.to_string (default_thm_id))) then error "This command can only be used for unnamed theorem." -let save_anonymous opacity save_ident = - let p = Proof_global.give_me_the_proof () in - Proof.transaction p begin fun () -> - let id,const,do_guard,persistence,hook = get_proof opacity in - check_anonymity id save_ident; - save save_ident const do_guard persistence hook - end -let save_anonymous_with_strength kind opacity save_ident = - let p = Proof_global.give_me_the_proof () in - Proof.transaction p begin fun () -> - let id,const,do_guard,_,hook = get_proof opacity in - check_anonymity id save_ident; - (* we consider that non opaque behaves as local for discharge *) - save save_ident const do_guard (Global, Proof kind) hook - end +let save_anonymous ?proof opacity save_ident = + let id,const,do_guard,persistence,hook = get_proof ?proof opacity in + check_anonymity id save_ident; + save ?proof save_ident const do_guard persistence hook + +let save_anonymous_with_strength ?proof kind opacity save_ident = + let id,const,do_guard,_,hook = get_proof ?proof opacity in + check_anonymity id save_ident; + (* we consider that non opaque behaves as local for discharge *) + save ?proof save_ident const do_guard (Global, Proof kind) hook (* Starting a goal *) diff --git a/toplevel/lemmas.mli b/toplevel/lemmas.mli index d6bc90bc37..e8998d6089 100644 --- a/toplevel/lemmas.mli +++ b/toplevel/lemmas.mli @@ -35,22 +35,24 @@ val start_proof_with_initialization : val set_save_hook : (Proof.proof -> unit) -> unit (** {6 ... } *) -(** [save_named b] saves the current completed proof under the name it -was started; boolean [b] tells if the theorem is declared opaque; it -fails if the proof is not completed *) +(** [save_named b] saves the current completed (or the provided) proof + under the name it was started; boolean [b] tells if the theorem is + declared opaque; it fails if the proof is not completed *) -val save_named : bool -> unit +val save_named : ?proof:Proof_global.closed_proof -> bool -> unit (** [save_anonymous b name] behaves as [save_named] but declares the theorem under the name [name] and respects the strength of the declaration *) -val save_anonymous : bool -> Id.t -> unit +val save_anonymous : + ?proof:Proof_global.closed_proof -> bool -> Id.t -> unit (** [save_anonymous_with_strength s b name] behaves as [save_anonymous] but declares the theorem under the name [name] and gives it the strength [strength] *) -val save_anonymous_with_strength : theorem_kind -> bool -> Id.t -> unit +val save_anonymous_with_strength : + ?proof:Proof_global.closed_proof -> theorem_kind -> bool -> Id.t -> unit (** [admit ()] aborts the current goal and save it as an assmumption *) diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 44ff40f24d..9e7ddd5a66 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -502,14 +502,15 @@ let subst_body expand prg = let declare_definition prg = let body, typ = subst_body true prg in let ce = - { const_entry_body = body; + { const_entry_body = Future.from_val (body,Declareops.no_seff); const_entry_secctx = None; const_entry_type = Some typ; const_entry_opaque = false; const_entry_inline_code = false} in progmap_remove prg; - !declare_definition_ref prg.prg_name prg.prg_kind ce prg.prg_implicits + !declare_definition_ref prg.prg_name + prg.prg_kind ce prg.prg_implicits (fun local gr -> prg.prg_hook local gr; gr) open Pp @@ -550,27 +551,35 @@ let declare_mutual_definition l = let fixkind = Option.get first.prg_fixkind in let arrrec, recvec = Array.of_list fixtypes, Array.of_list fixdefs in let fixdecls = (Array.of_list (List.map (fun x -> Name x.prg_name) l), arrrec, recvec) in - let (local,kind) = first.prg_kind in let fixnames = first.prg_deps in - let kind = if fixkind != IsCoFixpoint then Fixpoint else CoFixpoint in + let kind = + fst first.prg_kind, + if fixkind != IsCoFixpoint then Fixpoint else CoFixpoint in let indexes, fixdecls = match fixkind with | IsFixpoint wfl -> let possible_indexes = - List.map3 compute_possible_guardness_evidences wfl fixdefs fixtypes in - let indexes = Pretyping.search_guard Loc.ghost (Global.env ()) possible_indexes fixdecls in - Some indexes, List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 l + List.map3 compute_possible_guardness_evidences + wfl fixdefs fixtypes in + let indexes = + Pretyping.search_guard Loc.ghost (Global.env()) + possible_indexes fixdecls in + Some indexes, + List.map_i (fun i _ -> + mkFix ((indexes,i),fixdecls),Declareops.no_seff) 0 l | IsCoFixpoint -> - None, List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 l + None, + List.map_i (fun i _ -> + mkCoFix (i,fixdecls),Declareops.no_seff) 0 l in (* Declare the recursive definitions *) - let kns = List.map4 (!declare_fix_ref (local, kind)) fixnames fixdecls fixtypes fiximps in + let kns = List.map4 (!declare_fix_ref kind) fixnames fixdecls fixtypes fiximps in (* Declare notations *) List.iter Metasyntax.add_notation_interpretation first.prg_notations; Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames; let gr = List.hd kns in let kn = match gr with ConstRef kn -> kn | _ -> assert false in - first.prg_hook local gr; + first.prg_hook (fst first.prg_kind) gr; List.iter progmap_remove l; kn let shrink_body c = @@ -594,7 +603,7 @@ let declare_obligation prg obl body = if get_shrink_obligations () then shrink_body body else [], body, [||] in let ce = - { const_entry_body = body; + { const_entry_body = Future.from_val(body,Declareops.no_seff); const_entry_secctx = None; const_entry_type = if ctx = [] then Some ty else None; const_entry_opaque = opaque; @@ -610,7 +619,7 @@ let declare_obligation prg obl body = definition_message obl.obl_name; { obl with obl_body = Some (it_mkLambda_or_LetIn (mkApp (mkConst constant, args)) ctx) } -let init_prog_info n b t deps fixkind notations obls impls kind reduce hook = +let init_prog_info n b t deps fixkind notations obls impls k reduce hook = let obls', b = match b with | None -> @@ -632,7 +641,8 @@ let init_prog_info n b t deps fixkind notations obls impls kind reduce hook = { prg_name = n ; prg_body = b; prg_type = reduce t; prg_obligations = (obls', Array.length obls'); prg_deps = deps; prg_fixkind = fixkind ; prg_notations = notations ; - prg_implicits = impls; prg_kind = kind; prg_reduce = reduce; prg_hook = hook; } + prg_implicits = impls; prg_kind = k; prg_reduce = reduce; + prg_hook = hook; } let get_prog name = let prg_infos = !from_prg in @@ -645,7 +655,11 @@ let get_prog name = match n with 0 -> raise (NoObligations None) | 1 -> map_first prg_infos - | _ -> error "More than one program with unsolved obligations") + | _ -> + error ("More than one program with unsolved obligations: "^ + String.concat ", " + (List.map string_of_id + (ProgMap.fold (fun k _ s -> k::s) prg_infos [])))) let get_any_prog () = let prg_infos = !from_prg in @@ -737,19 +751,14 @@ let rec string_of_list sep f = function (* Solve an obligation using tactics, return the corresponding proof term *) let solve_by_tac evi t = let id = Id.of_string "H" in - try - Pfedit.start_proof id goal_kind evi.evar_hyps evi.evar_concl - (fun _ _ -> ()); - Pfedit.by (tclCOMPLETE t); - let _,(const,_,_,_) = Pfedit.cook_proof ignore in - Pfedit.delete_current_proof (); - Inductiveops.control_only_guard (Global.env ()) - const.Entries.const_entry_body; - const.Entries.const_entry_body - with reraise -> - let reraise = Errors.push reraise in - Pfedit.delete_current_proof(); - raise reraise + let entry = Pfedit.build_constant_by_tactic + id ~goal_kind evi.evar_hyps evi.evar_concl (tclCOMPLETE t) in + let env = Global.env () in + let entry = Term_typing.handle_side_effects env entry in + let body, eff = Future.force entry.Entries.const_entry_body in + assert(eff = Declareops.no_seff); + Inductiveops.control_only_guard (Global.env ()) body; + body let rec solve_obligation prg num tac = let user_num = succ num in diff --git a/toplevel/obligations.mli b/toplevel/obligations.mli index bc092a1ce1..ddc99a96cb 100644 --- a/toplevel/obligations.mli +++ b/toplevel/obligations.mli @@ -22,7 +22,7 @@ open Tacexpr (** Forward declaration. *) val declare_fix_ref : (definition_kind -> Id.t -> - constr -> types -> Impargs.manual_implicits -> global_reference) ref + Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference) ref val declare_definition_ref : (Id.t -> definition_kind -> diff --git a/toplevel/record.ml b/toplevel/record.ml index ff918293b5..476da3d0e0 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -189,7 +189,8 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls let kn = try let cie = { - const_entry_body = proj; + const_entry_body = + Future.from_val (proj,Declareops.no_seff); const_entry_secctx = None; const_entry_type = Some projtyp; const_entry_opaque = false; @@ -293,7 +294,8 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls let class_body = it_mkLambda_or_LetIn field params in let class_type = Option.map (fun ar -> it_mkProd_or_LetIn ar params) arity in let class_entry = - { const_entry_body = class_body; + { const_entry_body = + Future.from_val (class_body,Declareops.no_seff); const_entry_secctx = None; const_entry_type = class_type; const_entry_opaque = false; @@ -306,7 +308,8 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls let proj_type = it_mkProd_or_LetIn (mkProd(Name (snd id), inst_type, lift 1 field)) params in let proj_body = it_mkLambda_or_LetIn (mkLambda (Name (snd id), inst_type, mkRel 1)) params in let proj_entry = - { const_entry_body = proj_body; + { const_entry_body = + Future.from_val (proj_body,Declareops.no_seff); const_entry_secctx = None; const_entry_type = Some proj_type; const_entry_opaque = false; diff --git a/toplevel/stm.ml b/toplevel/stm.ml new file mode 100644 index 0000000000..004ac94289 --- /dev/null +++ b/toplevel/stm.ml @@ -0,0 +1,952 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2013 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +let prerr_endline s = if !Flags.debug then prerr_endline s else () + +open Stateid +open Vernacexpr +open Errors +open Pp +open Names +open Util +open Ppvernac +open Vernac_classifier + +(* During interactive use we cache more states so that Undoing is fast *) +let interactive () = + !Flags.ide_slave || !Flags.print_emacs || not !Flags.batch_mode + +(* Wrap interp to set the feedback id *) +let interp ?proof id (verbosely, loc, expr) = + let internal_command = function + | VernacResetName _ | VernacResetInitial | VernacBack _ + | VernacBackTo _ | VernacRestart | VernacUndo _ | VernacUndoTo _ + | VernacBacktrack _ | VernacAbortAll | VernacAbort _ -> true | _ -> false in + if internal_command expr then () + else begin + Pp.set_id_for_feedback (Interface.State id); + try Vernacentries.interp ~verbosely ?proof (loc, expr) + with e -> raise (Errors.push (Cerrors.process_vernac_interp_error e)) + end + +type ast = bool * Loc.t * vernac_expr +let pr_ast (_, _, v) = pr_vernac v + +module Vcs_ = Vcs.Make(StateidOrderedType) + +type branch_type = [ `Master | `Proof of string * int ] +type cmd_t = ast +type fork_t = ast * Vcs_.branch_name * Names.Id.t list +type qed_t = + ast * vernac_qed_type * (Vcs_.branch_name * branch_type Vcs_.branch_info) +type seff_t = ast option +type alias_t = state_id +type transaction = + | Cmd of cmd_t + | Fork of fork_t + | Qed of qed_t + | Sideff of seff_t + | Alias of alias_t + | Noop +type step = + [ `Cmd of cmd_t + | `Fork of fork_t + | `Qed of qed_t * state_id + | `Sideff of [ `Ast of ast * state_id | `Id of state_id ] + | `Alias of alias_t ] +type visit = { step : step; next : state_id } + +type state = States.state * Proof_global.state +type state_info = { (* Make private *) + mutable n_reached : int; + mutable n_goals : int; + mutable state : state option; +} +let default_info () = { n_reached = 0; n_goals = 0; state = None } + +(* Functions that work on a Vcs with a specific branch type *) +module Vcs_aux : sig + + val proof_nesting : (branch_type, 't,'i) Vcs_.t -> int + val find_proof_at_depth : + (branch_type, 't, 'i) Vcs_.t -> int -> + Vcs_.branch_name * branch_type Vcs_.branch_info + +end = struct (* {{{ *) + + let proof_nesting vcs = + List.fold_left max 0 + (List.map_filter + (function { Vcs_.kind = `Proof (_,n) } -> Some n | _ -> None) + (List.map (Vcs_.get_branch vcs) (Vcs_.branches vcs))) + + let find_proof_at_depth vcs pl = + try List.find (function + | _, { Vcs_.kind = `Proof(m, n) } -> n = pl + | _ -> false) + (List.map (fun h -> h, Vcs_.get_branch vcs h) (Vcs_.branches vcs)) + with Not_found -> failwith "find_proof_at_depth" + +end (* }}} *) + +(* Imperative wrap around VCS to obtain _the_ VCS *) +module VCS : sig + + type id = state_id + type branch_name = Vcs_.branch_name + type 'branch_type branch_info = 'branch_type Vcs_.branch_info = { + kind : [> `Master] as 'branch_type; + root : id; + pos : id; + } + + type vcs = (branch_type, transaction, state_info) Vcs_.t + + val init : id -> unit + + val string_of_branch_name : branch_name -> string + + val current_branch : unit -> branch_name + val checkout : branch_name -> unit + val master : branch_name + val branches : unit -> branch_name list + val get_branch : branch_name -> branch_type branch_info + val get_branch_pos : branch_name -> id + val new_node : unit -> id + val merge : id -> ours:transaction -> ?into:branch_name -> branch_name -> unit + val delete_branch : branch_name -> unit + val commit : id -> transaction -> unit + val mk_branch_name : ast -> branch_name + val branch : branch_name -> branch_type -> unit + + val get_info : id -> state_info + val reached : id -> bool -> unit + val goals : id -> int -> unit + val set_state : id -> state -> unit + val forget_state : id -> unit + + val create_cluster : id list -> unit + + val proof_nesting : unit -> int + val checkout_shallowest_proof_branch : unit -> unit + val propagate_sideff : ast option -> unit + + val visit : id -> visit + + val print : unit -> unit + + val backup : unit -> vcs + val restore : vcs -> unit + +end = struct (* {{{ *) + + include Vcs_ + + module StateidSet = Set.Make(StateidOrderedType) + open Printf + + let print_dag vcs () = (* {{{ *) + let fname = "stm" in + let string_of_transaction = function + | Cmd t | Fork (t, _, _) -> + (try string_of_ppcmds (pr_ast t) with _ -> "ERR") + | Sideff (Some t) -> + sprintf "Sideff(%s)" + (try string_of_ppcmds (pr_ast t) with _ -> "ERR") + | Sideff None -> "EnvChange" + | Noop -> " " + | Alias id -> sprintf "Alias(%s)" (string_of_state_id id) + | Qed (a,_,_) -> string_of_ppcmds (pr_ast a) in + let is_green id = + match get_info vcs id with + | Some { state = Some _ } -> true + | _ -> false in + let is_red id = + match get_info vcs id with + | Some s -> s.n_reached = ~-1 + | _ -> false in + let head = current_branch vcs in + let heads = + List.map (fun x -> x, (get_branch vcs x).pos) (branches vcs) in + let graph = dag vcs in + let quote s = + Str.global_replace (Str.regexp "\n") "<BR/>" + (Str.global_replace (Str.regexp "<") "<" + (Str.global_replace (Str.regexp ">") ">" + (Str.global_replace (Str.regexp "\"") """ + (Str.global_replace (Str.regexp "&") "&" + (String.sub s 0 (min (String.length s) 20)))))) in + let fname_dot, fname_ps = + let f = "/tmp/" ^ Filename.basename fname in + f ^ ".dot", f ^ ".pdf" in + let node id = "s" ^ string_of_state_id id in + let edge tr = + sprintf "<<FONT POINT-SIZE=\"12\" FACE=\"sans\">%s</FONT>>" + (quote (string_of_transaction tr)) in + let ids = ref StateidSet.empty in + let clus = Hashtbl.create 13 in + let node_info id = + match get_info vcs id with + | None -> "" + | Some info -> + sprintf "<<FONT POINT-SIZE=\"12\">%s</FONT>" (string_of_state_id id) ^ + sprintf " <FONT POINT-SIZE=\"11\">r:%d g:%d</FONT>>" + info.n_reached info.n_goals in + let color id = + if is_red id then "red" else if is_green id then "green" else "white" in + let nodefmt oc id = + fprintf oc "%s [label=%s,style=filled,fillcolor=%s];\n" + (node id) (node_info id) (color id) in + let add_to_clus_or_ids from cf = + match cf with + | None -> ids := StateidSet.add from !ids; false + | Some c -> Hashtbl.replace clus c + (try let n = Hashtbl.find clus c in from::n + with Not_found -> [from]); true in + let oc = open_out fname_dot in + output_string oc "digraph states {\nsplines=ortho\n"; + Dag.iter graph (fun from cf _ l -> + let c1 = add_to_clus_or_ids from cf in + List.iter (fun (dest, trans) -> + let c2 = add_to_clus_or_ids dest (Dag.cluster_of graph dest) in + fprintf oc "%s -> %s [label=%s,labelfloat=%b];\n" + (node from) (node dest) (edge trans) (c1 && c2)) l + ); + StateidSet.iter (nodefmt oc) !ids; + Hashtbl.iter (fun c nodes -> + fprintf oc "subgraph cluster_%s {\n" (Dag.string_of_cluster_id c); + List.iter (nodefmt oc) nodes; + fprintf oc "color=blue; }\n" + ) clus; + List.iteri (fun i (b,id) -> + let shape = if head = b then "box3d" else "box" in + fprintf oc "b%d -> %s;\n" i (node id); + fprintf oc "b%d [shape=%s,label=\"%s\"];\n" i shape + (string_of_branch_name b); + ) heads; + output_string oc "}\n"; + close_out oc; + ignore(Sys.command + ("dot -Tpdf -Gcharset=latin1 " ^ fname_dot ^ " -o" ^ fname_ps)) + (* }}} *) + + type vcs = (branch_type, transaction, state_info) t + let vcs : vcs ref = ref (empty dummy_state_id) + + let init id = + vcs := empty id; + vcs := set_info !vcs id (default_info ()) + + let current_branch () = current_branch !vcs + + let checkout head = vcs := checkout !vcs head + let master = master + let branches () = branches !vcs + let get_branch head = get_branch !vcs head + let get_branch_pos head = (get_branch head).pos + let new_node () = + let id = Stateid.fresh_state_id () in + vcs := set_info !vcs id (default_info ()); + id + let merge id ~ours ?into branch = + vcs := merge !vcs id ~ours ~theirs:Noop ?into branch + let delete_branch branch = vcs := delete_branch !vcs branch + let commit id t = vcs := commit !vcs id t + let mk_branch_name (_, _, x) = mk_branch_name + (match x with + | VernacDefinition (_,(_,i),_) -> string_of_id i + | VernacStartTheoremProof (_,[Some (_,i),_],_) -> string_of_id i + | _ -> "branch") + let branch name kind = vcs := branch !vcs name kind + let get_info id = + match get_info !vcs id with + | Some x -> x + | None -> assert false + let set_state id s = (get_info id).state <- Some s + let forget_state id = (get_info id).state <- None + let reached id b = + let info = get_info id in + if b then info.n_reached <- info.n_reached + 1 + else info.n_reached <- -1 + let goals id n = (get_info id).n_goals <- n + let create_cluster l = vcs := create_cluster !vcs l + + let proof_nesting () = Vcs_aux.proof_nesting !vcs + + let checkout_shallowest_proof_branch () = + let pl = proof_nesting () in + try + let branch, mode = match Vcs_aux.find_proof_at_depth !vcs pl with + | h, { Vcs_.kind = `Proof (m, _) } -> h, m | _ -> assert false in + checkout branch; + Proof_global.activate_proof_mode mode + with Failure _ -> + checkout master; + Proof_global.disactivate_proof_mode "Classic" (* XXX *) + + (* copies the transaction on every open branch *) + let propagate_sideff t = + List.iter (fun b -> + checkout b; + let id = new_node () in + merge id ~ours:(Sideff t) ~into:b master) + (List.filter ((<>) master) (branches ())) + + let visit id = + match Dag.from_node (dag !vcs) id with + | [n, Cmd x] -> { step = `Cmd x; next = n } + | [n, Alias x] -> { step = `Alias x; next = n } + | [n, Fork x] -> { step = `Fork x; next = n } + | [n, Qed x; p, Noop] + | [p, Noop; n, Qed x] -> { step = `Qed (x,p); next = n } + | [n, Sideff None; p, Noop] + | [p, Noop; n, Sideff None]-> { step = `Sideff (`Id p); next = n } + | [n, Sideff (Some x); p, Noop] + | [p, Noop; n, Sideff (Some x)]-> { step = `Sideff (`Ast (x,p)); next = n } + | _ -> anomaly (str "Malformed VCS, or visiting the root") + + module NB : sig + + val command : (unit -> unit) -> unit + + end = struct + + let m = Mutex.create () + let c = Condition.create () + let job = ref None + let worker = ref None + + let set_last_job j = + Mutex.lock m; + job := Some j; + Condition.signal c; + Mutex.unlock m + + let get_last_job () = + Mutex.lock m; + while !job = None do Condition.wait c m; done; + match !job with + | None -> assert false + | Some x -> job := None; Mutex.unlock m; x + + let run_command () = + while true do get_last_job () () done + + let command job = + set_last_job job; + if !worker = None then worker := Some (Thread.create run_command ()) + + end + + let print () = + if not !Flags.debug then () else NB.command (print_dag !vcs) + + let backup () = !vcs + let restore v = vcs := v + +end (* }}} *) + +(* Fills in the nodes of the VCS *) +module State : sig + + (** The function is from unit, so it uses the current state to define + a new one. I.e. one may been to install the right state before + defining a new one. + + Warning: an optimization requires that state modifying functions + are always executed using this wrapper. *) + val define : ?cache:bool -> (unit -> unit) -> state_id -> unit + + val install_cached : state_id -> unit + val is_cached : state_id -> bool + + val exn_on : state_id -> ?valid:state_id -> exn -> exn + +end = struct (* {{{ *) + + (* cur_id holds dummy_state_id in case the last attempt to define a state + * failed, so the global state may contain garbage *) + let cur_id = ref dummy_state_id + + (* helpers *) + let freeze_global_state () = + States.freeze ~marshallable:false, Proof_global.freeze () + let unfreeze_global_state (s,p) = + States.unfreeze s; Proof_global.unfreeze p + + (* hack to make futures functional *) + let in_t, out_t = Dyn.create "state4future" + let () = Future.set_freeze + (fun () -> in_t (freeze_global_state (), !cur_id)) + (fun t -> let s,i = out_t t in unfreeze_global_state s; cur_id := i) + + let is_cached id = + id = !cur_id || + match VCS.get_info id with + | { state = Some _ } -> true + | _ -> false + + let install_cached id = + if id = !cur_id then () else (* optimization *) + let s = + match VCS.get_info id with + | { state = Some s } -> s + | _ -> anomaly (str "unfreezing a non existing state") in + unfreeze_global_state s; cur_id := id + + let freeze id = VCS.set_state id (freeze_global_state ()) + + let exn_on id ?valid e = + Stateid.add_state_id e ?valid id + + let define ?(cache=false) f id = + if is_cached id then + anomaly (str"defining state "++str(string_of_state_id id)++str" twice"); + try + prerr_endline ("defining " ^ + string_of_state_id id ^ " (cache=" ^ string_of_bool cache ^ ")"); + f (); + if cache then freeze id; + cur_id := id; + feedback ~state_id:id Interface.Processed; + VCS.reached id true; + if Proof_global.there_are_pending_proofs () then + VCS.goals id (Proof_global.get_open_goals ()); + with e -> + let e = Errors.push e in + let good_id = !cur_id in + cur_id := dummy_state_id; + VCS.reached id false; + match Stateid.get_state_id e with + | Some _ -> raise e + | None -> raise (exn_on id ~valid:good_id e) + +end +(* }}} *) + + +(* Runs all transactions needed to reach a state *) +module Reach : sig + + val known_state : cache:bool -> state_id -> unit + +end = struct (* {{{ *) + +let pstate = ["meta counter"; "evar counter"; "program-tcc-table"] + +let collect_proof cur hd id = + let rec collect last accn id = + let view = VCS.visit id in + match last, view.step with + | _, `Cmd x -> collect (Some (id,x)) (id::accn) view.next + | _, `Alias _ -> collect None (id::accn) view.next + | Some (parent, (_,_,VernacExactProof _)), `Fork _ -> + `NotOptimizable `Immediate + | Some (parent, (_,_,VernacProof(_,Some _) as v)), `Fork (_, hd', _) -> + assert( hd = hd' ); + `Optimizable (parent, Some v, accn) + | Some (parent, _), `Fork (_, hd', _) -> + assert( hd = hd' ); + `MaybeOptimizable (parent, accn) + | _, `Sideff se -> collect None (id::accn) view.next + | _ -> `NotOptimizable `Unknown in + if State.is_cached id then `NotOptimizable `Unknown + else collect (Some cur) [] id + +let known_state ~cache id = + + (* ugly functions to process nested lemmas, i.e. hard to reproduce + * side effects *) + let cherry_pick_non_pstate () = + Summary.freeze_summary ~marshallable:false ~complement:true pstate, + Lib.freeze ~marshallable:false in + let inject_non_pstate (s,l) = Summary.unfreeze_summary s; Lib.unfreeze l in + + let rec pure_cherry_pick_non_pstate id = Future.purify (fun id -> + prerr_endline ("cherry-pick non pstate " ^ string_of_state_id id); + reach id; + cherry_pick_non_pstate ()) id + + (* traverses the dag backward from nodes being already calculated *) + and reach ?(cache=cache) id = + prerr_endline ("reaching: " ^ string_of_state_id id); + if State.is_cached id then begin + State.install_cached id; + feedback ~state_id:id Interface.Processed; + prerr_endline ("reached (cache)") + end else + let step, cache_step = + let view = VCS.visit id in + match view.step with + | `Alias id -> + (fun () -> + reach view.next; reach id; Vernacentries.try_print_subgoals ()), + cache + | `Cmd (x,_) -> (fun () -> reach view.next; interp id x), cache + | `Fork (x,_,_) -> (fun () -> reach view.next; interp id x), true + | `Qed ((x,keep,(hd,_)), eop) -> + let rec aux = function + | `Optimizable (start, proof_using_ast, nodes) -> + (fun () -> + prerr_endline ("Optimizable " ^ string_of_state_id id); + VCS.create_cluster nodes; + begin match keep with + | KeepProof -> + let f = Future.create (fun () -> reach eop) in + reach start; + let proof = + Proof_global.close_future_proof + ~fix_exn:(State.exn_on id ~valid:eop) f in + reach view.next; + interp id ~proof x; + | DropProof -> + reach view.next; + Option.iter (interp start) proof_using_ast; + interp id x + end; + Proof_global.discard_all ()) + | `NotOptimizable `Immediate -> assert (view.next = eop); + (fun () -> reach eop; interp id x; Proof_global.discard_all ()) + | `NotOptimizable `Unknown -> + (fun () -> + prerr_endline ("NotOptimizable " ^ string_of_state_id id); + reach eop; + begin match keep with + | KeepProof -> + let proof = Proof_global.close_proof () in + reach view.next; + interp id ~proof x + | DropProof -> + reach view.next; + interp id x + end; + Proof_global.discard_all ()) + | `MaybeOptimizable (start, nodes) -> + (fun () -> + prerr_endline ("MaybeOptimizable " ^ string_of_state_id id); + reach ~cache:true start; + (* no sections and no modules *) + if Environ.named_context (Global.env ()) = [] && + Safe_typing.is_curmod_library (Global.safe_env ()) then + aux (`Optimizable (start, None, nodes)) () + else + aux (`NotOptimizable `Unknown) ()) + in + aux (collect_proof (view.next, x) hd eop), true + | `Sideff (`Ast (x,_)) -> + (fun () -> reach view.next; interp id x), cache + | `Sideff (`Id origin) -> + (fun () -> + let s = pure_cherry_pick_non_pstate origin in + reach view.next; + inject_non_pstate s), + cache + in + State.define ~cache:cache_step step id; + prerr_endline ("reached: "^ string_of_state_id id) in + reach id + +end (* }}} *) + +(* The backtrack module simulates the classic behavior of a linear document *) +module Backtrack : sig + + val record : unit -> unit + val backto : state_id -> unit + val cur : unit -> state_id + + (* we could navigate the dag, but this ways easy *) + val branches_of : state_id -> VCS.branch_name list + + (* To be installed during initialization *) + val undo_vernac_classifier : vernac_expr -> vernac_classification + +end = struct (* {{{ *) + + module S = Searchstack + + type hystory_elt = { + id : state_id ; + vcs : VCS.vcs; + label : Names.Id.t list; (* To implement a limited form of reset *) + } + + let history : hystory_elt S.t = S.create () + + let cur () = + if S.is_empty history then anomaly (str "Empty history"); + (S.top history).id + + let record () = + let id = VCS.get_branch_pos (VCS.current_branch ()) in + S.push { + id = id; + vcs = VCS.backup (); + label = + if id = initial_state_id || id = dummy_state_id then [] else + match VCS.visit id with + | { step = `Fork (_,_,l) } -> l + | { step = `Cmd (_,_, VernacFixpoint (_,l)) } -> + List.map (fun (((_,id),_,_,_,_),_) -> id) l + | { step = `Cmd (_,_, VernacCoFixpoint (_,l)) } -> + List.map (fun (((_,id),_,_,_),_) -> id) l + | { step = `Cmd (_,_, VernacAssumption (_,_,l)) } -> + List.flatten (List.map (fun (_,(lid,_)) -> List.map snd lid) l) + | { step = `Cmd (_,_, VernacInductive (_,_,l)) } -> + List.map (fun (((_,(_,id)),_,_,_,_),_) -> id) l + | { step = `Cmd (_,_, (VernacDefinition (_,(_,id),DefineBody _) | + VernacDeclareModuleType ((_,id),_,_,_) | + VernacDeclareModule (_,(_,id),_,_) | + VernacDefineModule (_,(_,id),_,_,_))) } -> [id] + | _ -> [] } + history + + let backto oid = + assert(not (S.is_empty history)); + let rec pop_until_oid () = + let id = (S.top history).id in + if id = initial_state_id || id = oid then () + else begin ignore (S.pop history); pop_until_oid (); end in + pop_until_oid (); + let backup = S.top history in + VCS.restore backup.vcs; + if backup.id <> oid then anomaly (str "Backto an unknown state") + + let branches_of id = + try + let s = S.find (fun n s -> + if s.id = id then `Stop s else `Cont ()) () history in + Vcs_.branches s.vcs + with Not_found -> assert false + + let undo_vernac_classifier = function + | VernacResetInitial -> + VtStm (VtBack initial_state_id, true), VtNow + | VernacResetName (_,name) -> + msg_warning + (str"Reset not implemented for automatically generated constants"); + (try + let s = + S.find (fun b s -> + if b then `Stop s else `Cont (List.mem name s.label)) + false history in + VtStm (VtBack s.id, true), VtNow + with Not_found -> + VtStm (VtBack (S.top history).id, true), VtNow) + | VernacBack n -> + let s = S.find (fun n s -> + if n = 0 then `Stop s else `Cont (n-1)) n history in + VtStm (VtBack s.id, true), VtNow + | VernacUndo n -> + let s = S.find (fun n s -> + if n = 0 then `Stop s else `Cont (n-1)) n history in + VtStm (VtBack s.id, true), VtLater + | VernacUndoTo _ + | VernacRestart as e -> + let m = match e with VernacUndoTo m -> m | _ -> 0 in + let vcs = (S.top history).vcs in + let cb, _ = + Vcs_aux.find_proof_at_depth vcs (Vcs_aux.proof_nesting vcs) in + let n = S.find (fun n { vcs } -> + if List.mem cb (Vcs_.branches vcs) then `Cont (n+1) else `Stop n) + 0 history in + let s = S.find (fun n s -> + if n = 0 then `Stop s else `Cont (n-1)) (n-m-1) history in + VtStm (VtBack s.id, true), VtLater + | VernacAbortAll -> + let s = S.find (fun () s -> + if List.length (Vcs_.branches s.vcs) = 1 then `Stop s else `Cont ()) + () history in + VtStm (VtBack s.id, true), VtLater + | VernacBacktrack (id,_,_) + | VernacBackTo id -> + VtStm (VtBack (Stateid.state_id_of_int id), true), VtNow + | _ -> VtUnknown, VtNow + +end (* }}} *) + +let init () = + VCS.init initial_state_id; + declare_vernac_classifier "Stm" Backtrack.undo_vernac_classifier; + State.define ~cache:true (fun () -> ()) initial_state_id; + Backtrack.record () + +let observe id = + let vcs = VCS.backup () in + try + Reach.known_state ~cache:(interactive ()) id; + VCS.print () + with e -> + let e = Errors.push e in + VCS.print (); + VCS.restore vcs; + raise e + +let finish () = + observe (VCS.get_branch_pos (VCS.current_branch ())); + VCS.print () + +let join_aborted_proofs () = + let rec aux id = + if id = initial_state_id then () else + let view = VCS.visit id in + match view.step with + | `Qed ((_,DropProof,_),eop) -> observe eop; aux view.next + | `Sideff _ | `Alias _ | `Cmd _ | `Fork _ | `Qed _ -> aux view.next + in + aux (VCS.get_branch_pos VCS.master) + +let join () = + finish (); + VCS.print (); + prerr_endline "Joining the environment"; + Global.join_safe_environment (); + VCS.print (); + prerr_endline "Joining the aborted proofs"; + join_aborted_proofs (); + VCS.print () + +let merge_proof_branch x keep branch = + if branch = VCS.master then + raise(State.exn_on dummy_state_id Proof_global.NoCurrentProof); + let info = VCS.get_branch branch in + VCS.checkout VCS.master; + let id = VCS.new_node () in + VCS.merge id ~ours:(Qed (x,keep,(branch, info))) branch; + VCS.delete_branch branch; + if keep = KeepProof then VCS.propagate_sideff None + +let process_transaction verbosely (loc, expr) = + let warn_if_pos a b = + if b then msg_warning(pr_ast a ++ str" should not be part of a script") in + let v, x = expr, (verbosely && Flags.is_verbose(), loc, expr) in + prerr_endline ("{{{ execute: "^ string_of_ppcmds (pr_ast x)); + let vcs = VCS.backup () in + try + let head = VCS.current_branch () in + VCS.checkout head; + begin + let c = classify_vernac v in + prerr_endline (" classified as: " ^ string_of_vernac_classification c); + match c with + (* Joining various parts of the document *) + | VtStm (VtJoinDocument, b), VtNow -> warn_if_pos x b; join () + | VtStm (VtFinish, b), VtNow -> warn_if_pos x b; finish () + | VtStm (VtObserve id, b), VtNow -> warn_if_pos x b; observe id + | VtStm ((VtObserve _ | VtFinish | VtJoinDocument), _), VtLater -> + anomaly(str"classifier: join actions cannot be classified as VtLater") + + (* Back *) + | VtStm (VtBack oid, true), w -> + let id = VCS.new_node () in + let bl = Backtrack.branches_of oid in + List.iter (fun branch -> + if not (List.mem branch bl) then + merge_proof_branch + (false,Loc.ghost,VernacAbortAll) DropProof branch) + (VCS.branches ()); + VCS.checkout_shallowest_proof_branch (); + VCS.commit id (Alias oid); + Backtrack.record (); if w = VtNow then finish () + | VtStm (VtBack id, false), VtNow -> + prerr_endline ("undo to state " ^ string_of_state_id id); + Backtrack.backto id; + VCS.checkout_shallowest_proof_branch (); + Reach.known_state ~cache:(interactive ()) id; + | VtStm (VtBack id, false), VtLater -> + anomaly(str"classifier: VtBack + VtLater must imply part_of_script") + + (* Query *) + | VtQuery false, VtNow -> + finish (); + (try Future.purify (interp dummy_state_id) (true,loc,expr) + with e when Errors.noncritical e -> + let e = Errors.push e in + raise(State.exn_on dummy_state_id e)) + | VtQuery true, w -> + let id = VCS.new_node () in + VCS.commit id (Cmd x); + Backtrack.record (); if w = VtNow then finish () + | VtQuery false, VtLater -> + anomaly(str"classifier: VtQuery + VtLater must imply part_of_script") + + (* Proof *) + | VtStartProof (mode, names), w -> + let id = VCS.new_node () in + let bname = VCS.mk_branch_name x in + VCS.checkout VCS.master; + VCS.commit id (Fork (x, bname, names)); + VCS.branch bname (`Proof (mode, VCS.proof_nesting () + 1)); + Proof_global.activate_proof_mode mode; + Backtrack.record (); if w = VtNow then finish () + | VtProofStep, w -> + let id = VCS.new_node () in + VCS.commit id (Cmd x); + Backtrack.record (); if w = VtNow then finish () + | VtQed keep, w -> + merge_proof_branch x keep head; + VCS.checkout_shallowest_proof_branch (); + Backtrack.record (); if w = VtNow then finish () + + (* Side effect on all branches *) + | VtSideff, w -> + let id = VCS.new_node () in + VCS.checkout VCS.master; + VCS.commit id (Cmd x); + VCS.propagate_sideff (Some x); + VCS.checkout_shallowest_proof_branch (); + Backtrack.record (); if w = VtNow then finish () + + (* Unknown: we execute it, check for open goals and propagate sideeff *) + | VtUnknown, VtNow -> + let id = VCS.new_node () in + let step () = + VCS.checkout VCS.master; + let mid = VCS.get_branch_pos VCS.master in + Reach.known_state ~cache:(interactive ()) mid; + interp id x; + (* Vernac x may or may not start a proof *) + if head = VCS.master && + Proof_global.there_are_pending_proofs () + then begin + let bname = VCS.mk_branch_name x in + VCS.commit id (Fork (x,bname,[])); + VCS.branch bname (`Proof ("Classic", VCS.proof_nesting () + 1)) + end else begin + VCS.commit id (Cmd x); + VCS.propagate_sideff (Some x); + VCS.checkout_shallowest_proof_branch (); + end in + State.define ~cache:true step id; + Backtrack.record () + + | VtUnknown, VtLater -> + anomaly(str"classifier: VtUnknown must imply VtNow") + end; + prerr_endline "executed }}}"; + VCS.print () + with e -> + match Stateid.get_state_id e with + | None -> + VCS.restore vcs; + VCS.print (); + anomaly (str ("execute: "^ + string_of_ppcmds (Errors.print_no_report e) ^ "}}}")) + | Some (_, id) -> + let e = Errors.push e in + prerr_endline ("Failed at state " ^ Stateid.string_of_state_id id); + VCS.restore vcs; + VCS.print (); + raise e + +(* Query API *) + +let get_current_state () = Backtrack.cur () + +let current_proof_depth () = + let head = VCS.current_branch () in + match VCS.get_branch head with + | { VCS.kind = `Master } -> 0 + | { VCS.pos = cur; VCS.kind = `Proof (_,n); VCS.root = root } -> + let rec distance cur = + if cur = root then 0 + else 1 + distance (VCS.visit cur).next in + distance cur + +let unmangle n = + let n = VCS.string_of_branch_name n in + let idx = String.index n '_' + 1 in + Names.id_of_string (String.sub n idx (String.length n - idx)) + +let proofname b = match VCS.get_branch b with + | { VCS.kind = `Proof _ } -> Some b + | _ -> None + +let get_all_proof_names () = + List.map unmangle (List.map_filter proofname (VCS.branches ())) + +let get_current_proof_name () = + Option.map unmangle (proofname (VCS.current_branch ())) + +let get_script prf = + let rec find acc id = + if id = initial_state_id || id = dummy_state_id then acc else + let view = VCS.visit id in + match view.step with + | `Fork (_,_,ns) when List.mem prf ns -> acc + | `Qed ((x,_,_), proof) -> find [pi3 x, (VCS.get_info id).n_goals] proof + | `Sideff (`Ast (x,id)) -> find ((pi3 x, (VCS.get_info id).n_goals)::acc) id + | `Sideff (`Id id) -> find acc id + | `Cmd x -> find ((pi3 x, (VCS.get_info id).n_goals)::acc) view.next + | `Alias id -> find acc id + | `Fork _ -> find acc view.next + in + find [] (VCS.get_branch_pos VCS.master) + +(* indentation code for Show Script, initially contributed + by D. de Rauglaudre *) + +let indent_script_item ((ng1,ngl1),nl,beginend,ppl) (cmd,ng) = + (* ng1 : number of goals remaining at the current level (before cmd) + ngl1 : stack of previous levels with their remaining goals + ng : number of goals after the execution of cmd + beginend : special indentation stack for { } *) + let ngprev = List.fold_left (+) ng1 ngl1 in + let new_ngl = + if ng > ngprev then + (* We've branched *) + (ng - ngprev + 1, ng1 - 1 :: ngl1) + else if ng < ngprev then + (* A subgoal have been solved. Let's compute the new current level + by discarding all levels with 0 remaining goals. *) + let _ = assert (Int.equal ng (ngprev - 1)) in + let rec loop = function + | (0, ng2::ngl2) -> loop (ng2,ngl2) + | p -> p + in loop (ng1-1, ngl1) + else + (* Standard case, same goal number as before *) + (ng1, ngl1) + in + (* When a subgoal have been solved, separate this block by an empty line *) + let new_nl = (ng < ngprev) + in + (* Indentation depth *) + let ind = List.length ngl1 + in + (* Some special handling of bullets and { }, to get a nicer display *) + let pred n = max 0 (n-1) in + let ind, nl, new_beginend = match cmd with + | VernacSubproof _ -> pred ind, nl, (pred ind)::beginend + | VernacEndSubproof -> List.hd beginend, false, List.tl beginend + | VernacBullet _ -> pred ind, nl, beginend + | _ -> ind, nl, beginend + in + let pp = + (if nl then fnl () else mt ()) ++ + (hov (ind+1) (str (String.make ind ' ') ++ Ppvernac.pr_vernac cmd)) + in + (new_ngl, new_nl, new_beginend, pp :: ppl) + +let show_script ?proof () = + try + let prf = + match proof with + | None -> Pfedit.get_current_proof_name () + | Some (id,_) -> id in + let cmds = get_script prf in + let _,_,_,indented_cmds = + List.fold_left indent_script_item ((1,[]),false,[],[]) cmds + in + let indented_cmds = List.rev (indented_cmds) in + msg_notice (v 0 (Pp.prlist_with_sep Pp.fnl (fun x -> x) indented_cmds)) + with Proof_global.NoCurrentProof -> () + +let () = Vernacentries.show_script := show_script + +(* vim:set foldmethod=marker: *) diff --git a/toplevel/stm.mli b/toplevel/stm.mli new file mode 100644 index 0000000000..d4898b30f3 --- /dev/null +++ b/toplevel/stm.mli @@ -0,0 +1,27 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Add a transaction (an edit that adds a new line to the script). + The bool is there for -compile-verbose *) +val process_transaction : bool -> Vernacexpr.located_vernac_expr -> unit + +(* Evaluates the tip of the current branch *) +val finish : unit -> unit + +(* Evaluates a particular state id (does not move the current tip) *) +val observe : Stateid.state_id -> unit + +(* Joins the entire document. Implies finish, but also checks proofs *) +val join : unit -> unit + +val get_current_state : unit -> Stateid.state_id +val current_proof_depth : unit -> int +val get_all_proof_names : unit -> Names.identifier list +val get_current_proof_name : unit -> Names.identifier option + +val init : unit -> unit diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index 9a2b8840c7..dcf2b0b3d7 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -213,9 +213,9 @@ let make_prompt () = "n |lem1|lem2|lem3| p < " *) let make_emacs_prompt() = - let statnum = string_of_int (Lib.current_command_label ()) in - let dpth = Pfedit.current_proof_depth() in - let pending = Pfedit.get_all_proof_names() in + let statnum = Stateid.string_of_state_id (Stm.get_current_state ()) in + let dpth = Stm.current_proof_depth() in + let pending = Stm.get_all_proof_names() in let pendingprompt = List.fold_left (fun acc x -> acc ^ (if String.is_empty acc then "" else "|") ^ Names.Id.to_string x) @@ -306,14 +306,24 @@ let do_vernac () = msgerrnl (mt ()); if !print_emacs then msgerr (str (top_buffer.prompt())); resynch_buffer top_buffer; - try ignore (Vernac.eval_expr (read_sentence ())) + try Vernac.eval_expr (read_sentence ()); Stm.finish () with | End_of_input | Errors.Quit -> msgerrnl (mt ()); pp_flush(); raise Errors.Quit | Errors.Drop -> (* Last chance *) if Mltop.is_ocaml_top() then raise Errors.Drop else ppnl (str"Error: There is no ML toplevel." ++ fnl ()) - | any -> ppnl (print_toplevel_error any) + | any -> + Format.set_formatter_out_channel stdout; + ppnl (print_toplevel_error any); + pp_flush (); + match Stateid.get_state_id any with + | Some (valid_id,_) -> + let valid = Stateid.int_of_state_id valid_id in + Vernac.eval_expr (Loc.ghost, + (Vernacexpr.VernacStm (Vernacexpr.Command + (Vernacexpr.VernacBackTo valid)))) + | _ -> () (** Main coq loop : read vernacular expressions until Drop is entered. Ctrl-C is handled internally as Sys.Break instead of aborting Coq. @@ -330,5 +340,7 @@ let rec loop () = | Errors.Drop -> () | Errors.Quit -> exit 0 | any -> - msgerrnl (str"Anomaly: main loop exited. Please report."); - loop () + msgerrnl (str"Anomaly: main loop exited with exception: " ++ + str (Printexc.to_string any) ++ + fnl() ++ str"Please report."); + loop () diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib index b27c7588dd..d58df57f2b 100644 --- a/toplevel/toplevel.mllib +++ b/toplevel/toplevel.mllib @@ -2,6 +2,9 @@ Himsg Cerrors Class Locality +Vernacexpr +Ppextra +Ppvernac Metasyntax Auto_ind_decl Search @@ -13,11 +16,12 @@ Command Classes Record Ppvernac -Backtrack Vernacinterp Mltop Vernacentries Whelp +Vernac_classifier +Stm Vernac Ide_slave Toplevel diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index fcffb343ee..e05ced2b8d 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -116,53 +116,6 @@ let disable_drop = function let user_error loc s = Errors.user_err_loc (loc,"_",str s) -(** Timeout handling *) - -(** A global default timeout, controled by option "Set Default Timeout n". - Use "Unset Default Timeout" to deactivate it (or set it to 0). *) - -let default_timeout = ref None - -let _ = - Goptions.declare_int_option - { Goptions.optsync = true; - Goptions.optdepr = false; - Goptions.optname = "the default timeout"; - Goptions.optkey = ["Default";"Timeout"]; - Goptions.optread = (fun () -> !default_timeout); - Goptions.optwrite = ((:=) default_timeout) } - -(** When interpreting a command, the current timeout is initially - the default one, but may be modified locally by a Timeout command. *) - -let current_timeout = ref None - -(** Installing and de-installing a timer. - Note: according to ocaml documentation, Unix.alarm isn't available - for native win32. *) - -let timeout_handler _ = raise Timeout - -let set_timeout n = - let psh = - Sys.signal Sys.sigalrm (Sys.Signal_handle timeout_handler) in - ignore (Unix.alarm n); - Some psh - -let default_set_timeout () = - match !current_timeout with - | Some n -> set_timeout n - | None -> None - -let restore_timeout = function - | None -> () - | Some psh -> - (* stop alarm *) - ignore(Unix.alarm 0); - (* restore handler *) - Sys.set_signal Sys.sigalrm psh - - (* Open an utf-8 encoded file and skip the byte-order mark if any *) let open_utf8_file_in fname = @@ -262,7 +215,30 @@ let restore_translator_coqdoc (ch,cl,cs,coqdocstate) = Lexer.restore_com_state cs; Lexer.restore_location_table coqdocstate -let rec vernac_com interpfun checknav (loc,com) = +(* For coqtop -time, we display the position in the file, + and a glimpse of the executed command *) + +let display_cmd_header loc com = + let shorten s = try (String.sub s 0 30)^"..." with _ -> s in + let noblank s = + for i = 0 to String.length s - 1 do + match s.[i] with + | ' ' | '\n' | '\t' | '\r' -> s.[i] <- '~' + | _ -> () + done; + s + in + let (start,stop) = Loc.unloc loc in + let safe_pr_vernac x = + try Ppvernac.pr_vernac x + with e -> str (Printexc.to_string e) in + let cmd = noblank (shorten (string_of_ppcmds (safe_pr_vernac com))) + in + Pp.pp (str "Chars " ++ int start ++ str " - " ++ int stop ++ + str (" ["^cmd^"] ")); + Pp.flush_all () + +let rec vernac_com verbosely checknav (loc,com) = let rec interp = function | VernacLoad (verbosely, fname) -> let fname = Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) fname in @@ -286,39 +262,10 @@ let rec vernac_com interpfun checknav (loc,com) = raise reraise end - | VernacList l -> - List.iter (fun (_,v) -> interp v) l - | v when !just_parsing -> () - | VernacFail v -> - begin - try - (* If the command actually works, ignore its effects on the state *) - States.with_state_protection - (fun v -> ignore (interp v); raise HasNotFailed) v - with - | HasNotFailed -> - errorlabstrm "Fail" (str "The command has not failed !") - | e when Errors.noncritical e -> (* In particular e is no anomaly *) - if_verbose msg_info - (str "The command has indeed failed with message:" ++ - fnl () ++ str "=> " ++ hov 0 (Errors.print e)) - end - - | VernacTime v -> - let tstart = System.get_time() in - interp v; - let tend = System.get_time() in - let msg = if !time then "" else "Finished transaction in " in - msg_info (str msg ++ System.fmt_time_difference tstart tend) - - | VernacTimeout(n,v) -> - current_timeout := Some n; - interp v - - | v -> - let rollback = + | v -> Stm.process_transaction verbosely (loc,v) + (* FIXME elsewhere let rollback = if !Flags.batch_mode then States.without_rollback else States.with_heavy_rollback in @@ -330,12 +277,12 @@ let rec vernac_com interpfun checknav (loc,com) = let reraise = Errors.push reraise in restore_timeout psh; raise reraise + *) in try checknav loc com; - current_timeout := !default_timeout; if do_beautify () then pr_new_syntax loc (Some com); - if !time then display_cmd_header loc com; + if !Flags.time then display_cmd_header loc com; let com = if !time then VernacTime com else com in interp com with reraise -> @@ -347,20 +294,10 @@ let rec vernac_com interpfun checknav (loc,com) = and read_vernac_file verbosely s = Flags.make_warn verbosely; - let interpfun = - if verbosely then Vernacentries.interp - else Flags.silently Vernacentries.interp - in let checknav loc cmd = if is_navigation_vernac cmd && not (is_reset cmd) then user_error loc "Navigation commands forbidden in files" in - let end_inner_command cmd = - if !atomic_load || is_reset cmd then - Lib.mark_end_of_command () (* for Reset in coqc or coqtop -l *) - else - Backtrack.mark_command cmd; (* for Show Script, cf bug #2820 *) - in let (in_chan, fname, input) = open_file_twice_if verbosely s in try @@ -368,8 +305,7 @@ and read_vernac_file verbosely s = * raised, which means that we raised the end of the file being loaded *) while true do let loc_ast = parse_sentence input in - vernac_com interpfun checknav loc_ast; - end_inner_command (snd loc_ast); + vernac_com verbosely checknav loc_ast; pp_flush () done with any -> (* whatever the exception *) @@ -378,6 +314,7 @@ and read_vernac_file verbosely s = close_input in_chan input; (* we must close the file first *) match e with | End_of_input -> + Stm.join (); if do_beautify () then pr_new_syntax (Loc.make_loc (max_int,max_int)) None | _ -> raise_with_file fname (disable_drop e) @@ -393,10 +330,7 @@ let checknav loc ast = if is_deep_navigation_vernac ast then user_error loc "Navigation commands forbidden in nested commands" -let eval_expr ?(preserving=false) loc_ast = - vernac_com Vernacentries.interp checknav loc_ast; - if not preserving && not (is_navigation_vernac (snd loc_ast)) then - Backtrack.mark_command (snd loc_ast) +let eval_expr loc_ast = vernac_com true checknav loc_ast (* XML output hooks *) let (f_xml_start_library, xml_start_library) = Hook.make ~default:ignore () @@ -407,7 +341,6 @@ let load_vernac verb file = chan_beautify := if !Flags.beautify_file then open_out (file^beautify_suffix) else stdout; try - Lib.mark_end_of_command (); (* in case we're still in coqtop init *) read_vernac_file verb file; if !Flags.beautify_file then close_out !chan_beautify; with any -> @@ -428,3 +361,4 @@ let compile verbosely f = if !Flags.xml_export then Hook.get f_xml_end_library (); Library.save_library_to ldir (long_f_dot_v ^ "o"); Dumpglob.end_dump_glob () + diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli index bda42dfa62..d185719909 100644 --- a/toplevel/vernac.mli +++ b/toplevel/vernac.mli @@ -21,12 +21,7 @@ exception End_of_input val just_parsing : bool ref -(** [eval_expr] executes one vernacular command. By default the command is - considered as non-state-preserving, in which case we add it to the - Backtrack stack (triggering a save of a frozen state and the generation - of a new state label). An example of state-preserving command is one coming - from the query panel of Coqide. *) -val eval_expr : ?preserving:bool -> Loc.t * Vernacexpr.vernac_expr -> unit +val eval_expr : Loc.t * Vernacexpr.vernac_expr -> unit (** Set XML hooks *) val xml_start_library : (unit -> unit) Hook.t @@ -42,7 +37,6 @@ val load_vernac : bool -> string -> unit val compile : bool -> string -> unit - val is_navigation_vernac : Vernacexpr.vernac_expr -> bool (** Should we display timings for each command ? *) diff --git a/toplevel/vernac_classifier.ml b/toplevel/vernac_classifier.ml new file mode 100644 index 0000000000..d7b9553a0a --- /dev/null +++ b/toplevel/vernac_classifier.ml @@ -0,0 +1,164 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Stateid +open Vernacexpr +open Errors +open Pp + +let string_of_in_script b = if b then " (inside script)" else "" + +let string_of_vernac_type = function + | VtUnknown -> "Unknown" + | VtStartProof _ -> "StartProof" + | VtSideff -> "Sideff" + | VtQed _ -> "Qed" + | VtProofStep -> "ProofStep" + | VtQuery b -> "Query" ^ string_of_in_script b + | VtStm ((VtFinish|VtJoinDocument|VtObserve _), b) -> + "Stm" ^ string_of_in_script b + | VtStm (VtBack _, b) -> "Stm Back" ^ string_of_in_script b + +let string_of_vernac_when = function + | VtLater -> "Later" + | VtNow -> "Now" + +let string_of_vernac_classification (t,w) = + string_of_vernac_type t ^ " " ^ string_of_vernac_when w + +(* Since the set of vernaculars is extensible, also the classification function + has to be. *) +let classifiers = Summary.ref ~name:"vernac_classifier" [] +let declare_vernac_classifier s (f : vernac_expr -> vernac_classification) = + classifiers := !classifiers @ [s,f] + +let elide_part_of_script_and_now (a, _) = + match a with + | VtQuery _ -> VtQuery false, VtNow + | VtStm (x, _) -> VtStm (x, false), VtNow + | x -> x, VtNow + +let rec classify_vernac e = + let static_classifier e = match e with + (* Stm *) + | VernacStm Finish -> VtStm (VtFinish, true), VtNow + | VernacStm JoinDocument -> VtStm (VtJoinDocument, true), VtNow + | VernacStm (Observe id) -> VtStm (VtObserve id, true), VtNow + | VernacStm (Command x) -> elide_part_of_script_and_now (classify_vernac x) + (* Impossible, Vernac handles these *) + | VernacList _ -> anomaly (str "VernacList not handled by Vernac") + | VernacLoad _ -> anomaly (str "VernacLoad not handled by Vernac") + (* Nested vernac exprs *) + | VernacProgram e -> classify_vernac e + | VernacLocal (_,e) -> classify_vernac e + | VernacTimeout (_,e) -> classify_vernac e + | VernacTime e -> classify_vernac e + | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *) + (match classify_vernac e with + | (VtQuery _ | VtProofStep _ | VtSideff _ | VtStm _), _ as x -> x + | VtQed _, _ -> VtProofStep, VtNow + | (VtStartProof _ | VtUnknown), _ -> VtUnknown, VtNow) + (* Qed *) + | VernacEndProof Admitted | VernacAbort _ -> VtQed DropProof, VtLater + | VernacEndProof _ | VernacExactProof _ -> VtQed KeepProof, VtLater + (* Query *) + | VernacShow _ | VernacPrint _ | VernacSearch _ | VernacLocate _ + | VernacCheckMayEval _ -> VtQuery true, VtLater + (* ProofStep *) + | VernacProof _ + | VernacBullet _ + | VernacFocus _ | VernacUnfocus _ + | VernacSubproof _ | VernacEndSubproof _ + | VernacSolve _ + | VernacCheckGuard _ + | VernacUnfocused _ + | VernacSolveExistential _ -> VtProofStep, VtLater + (* StartProof *) + | VernacDefinition (_,(_,i),ProveBody _) -> + VtStartProof("Classic",[i]), VtLater + | VernacStartTheoremProof (_,l,_) -> + let names = + CList.map_filter (function (Some(_,i), _) -> Some i | _ -> None) l in + VtStartProof ("Classic", names), VtLater + | VernacGoal _ -> VtStartProof ("Classic",[]), VtLater + | VernacFixpoint (_,l) + when List.exists (fun ((_,_,_,_,p),_) -> p = None) l -> + VtStartProof ("Classic", + List.map (fun (((_,id),_,_,_,_),_) -> id) l), VtLater + | VernacCoFixpoint (_,l) + when List.exists (fun ((_,_,_,p),_) -> p = None) l -> + VtStartProof ("Classic", + List.map (fun (((_,id),_,_,_),_) -> id) l), VtLater + (* Sideff: apply to all open branches. usually run on master only *) + | VernacAssumption _ + | VernacDefinition (_,_,DefineBody _) + | VernacFixpoint _ | VernacCoFixpoint _ + | VernacInductive _ + | VernacScheme _ | VernacCombinedScheme _ + | VernacBeginSection _ + | VernacCanonical _ | VernacCoercion _ | VernacIdentityCoercion _ + | VernacAddLoadPath _ | VernacRemoveLoadPath _ | VernacAddMLPath _ + | VernacChdir _ + | VernacCreateHintDb _ | VernacRemoveHints _ | VernacHints _ + | VernacDeclareImplicits _ | VernacArguments _ | VernacArgumentsScope _ + | VernacReserve _ + | VernacGeneralizable _ + | VernacSetOpacity _ | VernacSetStrategy _ + | VernacUnsetOption _ | VernacSetOption _ + | VernacAddOption _ | VernacRemoveOption _ + | VernacMemOption _ | VernacPrintOption _ + | VernacGlobalCheck _ + | VernacDeclareReduction _ + | VernacDeclareClass _ | VernacDeclareInstances _ + | VernacComments _ -> VtSideff, VtLater + (* (Local) Notations have to disappear *) + | VernacEndSegment _ -> VtSideff, VtNow + (* Modules with parameters have to be executed: can import notations *) + | VernacDeclareModule (_,_,bl,_) + | VernacDefineModule (_,_,bl,_,_) + | VernacDeclareModuleType (_,bl,_,_) -> + VtSideff, if bl = [] then VtLater else VtNow + (* These commands alter the parser *) + | VernacOpenCloseScope _ | VernacDelimiters _ | VernacBindScope _ + | VernacInfix _ | VernacNotation _ | VernacSyntaxExtension _ + | VernacSyntacticDefinition _ + | VernacDeclareTacticDefinition _ | VernacTacticNotation _ + | VernacRequire _ | VernacImport _ | VernacInclude _ + | VernacDeclareMLModule _ + | VernacContext _ (* TASSI: unsure *) + | VernacProofMode _ + | VernacRequireFrom _ -> VtSideff, VtNow + (* These are ambiguous *) + | VernacInstance _ -> VtUnknown, VtNow + (* Stm will install a new classifier to handle these *) + | VernacBack _ | VernacAbortAll + | VernacUndoTo _ | VernacUndo _ + | VernacResetName _ | VernacResetInitial _ + | VernacBacktrack _ | VernacBackTo _ | VernacRestart -> !undo_classifier e + (* What are these? *) + | VernacNop + | VernacToplevelControl _ + | VernacRestoreState _ + | VernacWriteState _ -> VtUnknown, VtNow + (* Plugins should classify their commands *) + | VernacExtend _ -> VtUnknown, VtNow in + let rec extended_classifier = function + | [] -> static_classifier e + | (name,f)::fs -> + try + match f e with + | VtUnknown, _ -> extended_classifier fs + | x -> x + with e when Errors.noncritical e -> + let e = Errors.push e in + msg_warning(str"Exception raised by classifier: " ++ str name); + raise e + + in + extended_classifier !classifiers + diff --git a/toplevel/vernac_classifier.mli b/toplevel/vernac_classifier.mli new file mode 100644 index 0000000000..06535d5123 --- /dev/null +++ b/toplevel/vernac_classifier.mli @@ -0,0 +1,20 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2013 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Stateid +open Vernacexpr + +val string_of_vernac_classification : vernac_classification -> string + +(** What does a vernacular do *) +val classify_vernac : vernac_expr -> vernac_classification + +(** Install an additional vernacular classifier (that has precedence over + all classifiers already installed) *) +val declare_vernac_classifier : + string -> (vernac_expr -> vernac_classification) -> unit diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 88da26e83e..706b757db4 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -34,6 +34,10 @@ open Declaremods open Misctypes open Locality +let debug = false +let prerr_endline = + if debug then prerr_endline else fun _ -> () + (* Misc *) let cl_of_qualid = function @@ -58,60 +62,6 @@ let show_node () = could, possibly, be cleaned away. (Feb. 2010) *) () -(* indentation code for Show Script, initially contributed - by D. de Rauglaudre *) - -let indent_script_item ((ng1,ngl1),nl,beginend,ppl) (cmd,ng) = - (* ng1 : number of goals remaining at the current level (before cmd) - ngl1 : stack of previous levels with their remaining goals - ng : number of goals after the execution of cmd - beginend : special indentation stack for { } *) - let ngprev = List.fold_left (+) ng1 ngl1 in - let new_ngl = - if ng > ngprev then - (* We've branched *) - (ng - ngprev + 1, ng1 - 1 :: ngl1) - else if ng < ngprev then - (* A subgoal have been solved. Let's compute the new current level - by discarding all levels with 0 remaining goals. *) - let _ = assert (Int.equal ng (ngprev - 1)) in - let rec loop = function - | (0, ng2::ngl2) -> loop (ng2,ngl2) - | p -> p - in loop (ng1-1, ngl1) - else - (* Standard case, same goal number as before *) - (ng1, ngl1) - in - (* When a subgoal have been solved, separate this block by an empty line *) - let new_nl = (ng < ngprev) - in - (* Indentation depth *) - let ind = List.length ngl1 - in - (* Some special handling of bullets and { }, to get a nicer display *) - let pred n = max 0 (n-1) in - let ind, nl, new_beginend = match cmd with - | VernacSubproof _ -> pred ind, nl, (pred ind)::beginend - | VernacEndSubproof -> List.hd beginend, false, List.tl beginend - | VernacBullet _ -> pred ind, nl, beginend - | _ -> ind, nl, beginend - in - let pp = - (if nl then fnl () else mt ()) ++ - (hov (ind+1) (str (String.make ind ' ') ++ Ppvernac.pr_vernac cmd)) - in - (new_ngl, new_nl, new_beginend, pp :: ppl) - -let show_script () = - let prf = Pfedit.get_current_proof_name () in - let cmds = Backtrack.get_script prf in - let _,_,_,indented_cmds = - List.fold_left indent_script_item ((1,[]),false,[],[]) cmds - in - let indented_cmds = List.rev (indented_cmds) in - msg_notice (v 0 (Pp.prlist_with_sep Pp.fnl (fun x -> x) indented_cmds)) - let show_thesis () = msg_error (anomaly (Pp.str "TODO") ) @@ -130,7 +80,9 @@ let enable_goal_printing = ref true let print_subgoals () = if !enable_goal_printing && is_verbose () - then msg_notice (pr_open_subgoals ()) + then begin + msg_notice (pr_open_subgoals ()) + end let try_print_subgoals () = Pp.flush_all(); @@ -141,8 +93,8 @@ let try_print_subgoals () = let show_intro all = let pf = get_pftreestate() in - let {Evd.it=gls ; sigma=sigma} = Proof.V82.subgoals pf in - let gl = {Evd.it=List.hd gls ; sigma = sigma} in + let {Evd.it=gls ; sigma=sigma; eff=eff} = Proof.V82.subgoals pf in + let gl = {Evd.it=List.hd gls ; sigma = sigma; eff=eff} in let l,_= decompose_prod_assum (strip_outer_cast (pf_concl gl)) in if all then @@ -502,21 +454,20 @@ let vernac_start_proof kind l lettop = start_proof_and_print (Global, Proof kind) l no_hook let qed_display_script = ref true +let show_script = ref (fun ?proof () -> ()) -let vernac_end_proof = function +let vernac_end_proof ?proof = function | Admitted -> - Backtrack.mark_unreachable [Pfedit.get_current_proof_name ()]; admit (); Pp.feedback Interface.AddedAxiom | Proved (is_opaque,idopt) -> - let prf = Pfedit.get_current_proof_name () in - if is_verbose () && !qed_display_script then show_script (); + if is_verbose () && !qed_display_script then !show_script ?proof (); begin match idopt with - | None -> save_named is_opaque - | Some ((_,id),None) -> save_anonymous is_opaque id - | Some ((_,id),Some kind) -> save_anonymous_with_strength kind is_opaque id - end; - Backtrack.mark_unreachable [prf] + | None -> save_named ?proof is_opaque + | Some ((_,id),None) -> save_anonymous ?proof is_opaque id + | Some ((_,id),Some kind) -> + save_anonymous_with_strength ?proof kind is_opaque id + end (* A stupid macro that should be replaced by ``Exact c. Save.'' all along the theories [??] *) @@ -524,10 +475,8 @@ let vernac_end_proof = function let vernac_exact_proof c = (* spiwack: for simplicity I do not enforce that "Proof proof_term" is called only at the begining of a proof. *) - let prf = Pfedit.get_current_proof_name () in by (Tactics.exact_proof c); - save_named true; - Backtrack.mark_unreachable [prf] + save_named true let vernac_assumption locality (local, kind) l nl = let local = enforce_locality_exp locality local in @@ -800,9 +749,10 @@ let vernac_identity_coercion locality local id qids qidt = (* Type classes *) let vernac_instance abst locality sup inst props pri = - let glob = not (make_section_locality locality) in + let global = not (make_section_locality locality) in Dumpglob.dump_constraint inst false "inst"; - ignore(Classes.new_instance ~abstract:abst ~global:glob sup inst props pri) + ignore(Classes.new_instance + ~abstract:abst ~global sup inst props pri) let vernac_context l = if not (Classes.context l) then Pp.feedback Interface.AddedAxiom @@ -824,15 +774,15 @@ let focus_command_cond = Proof.no_cond command_focus let vernac_solve n tcom b = if not (refining ()) then error "Unknown command of the non proof-editing mode."; - let p = Proof_global.give_me_the_proof () in - Proof.transaction p begin fun () -> - solve_nth n (Tacinterp.hide_interp tcom None) ~with_end_tac:b; + Proof_global.with_current_proof (fun etac p -> + let with_end_tac = if b then Some etac else None in + let p = solve_nth n (Tacinterp.hide_interp tcom None) ?with_end_tac p in (* in case a strict subtree was completed, go back to the top of the prooftree *) - Proof_global.maximal_unfocus command_focus p; + let p = Proof.maximal_unfocus command_focus p in + p); print_subgoals() - end - +;; (* A command which should be a tactic. It has been added by Christine to patch an error in the design of the proof @@ -1532,126 +1482,23 @@ let vernac_register id r = match r with | RegisterInline -> Global.register_inline kn -(****************) -(* Backtracking *) - -(** NB: these commands are now forbidden in non-interactive use, - e.g. inside VernacLoad, VernacList, ... *) - -let vernac_backto lbl = - try - let lbl' = Backtrack.backto lbl in - if not (Int.equal lbl lbl') then - Pp.msg_warning - (str "Actually back to state "++ Pp.int lbl' ++ str "."); - try_print_subgoals () - with Backtrack.Invalid -> error "Invalid backtrack." - -let vernac_back n = - try - let extra = Backtrack.back n in - if not (Int.equal extra 0) then - Pp.msg_warning - (str "Actually back by " ++ Pp.int (extra+n) ++ str " steps."); - try_print_subgoals () - with Backtrack.Invalid -> error "Invalid backtrack." - -let vernac_reset_name id = - try - let globalized = - try - let gr = Smartlocate.global_with_alias (Ident id) in - Dumpglob.add_glob (fst id) gr; - true - with e when Errors.noncritical e -> false in - - if not globalized then begin - try begin match Lib.find_opening_node (snd id) with - | Lib.OpenedSection _ -> Dumpglob.dump_reference (fst id) - (DirPath.to_string (Lib.current_dirpath true)) "<>" "sec"; - (* Might be nice to implement module cases, too.... *) - | _ -> () - end with UserError _ -> () - end; - - if Backtrack.is_active () then - (Backtrack.reset_name id; try_print_subgoals ()) - else - (* When compiling files, Reset is now allowed again - as asked by A. Chlipala. we emulate a simple reset, - that discards all proofs. *) - let lbl = Lib.label_before_name id in - Pfedit.delete_all_proofs (); - Pp.msg_warning (str "Reset command occurred in non-interactive mode."); - Lib.reset_label lbl - with Backtrack.Invalid | Not_found -> error "Invalid Reset." - - -let vernac_reset_initial () = - if Backtrack.is_active () then - Backtrack.reset_initial () - else begin - Pp.msg_warning (str "Reset command occurred in non-interactive mode."); - Lib.raw_reset_initial () - end - -(* For compatibility with ProofGeneral: *) - -let vernac_backtrack snum pnum naborts = - Backtrack.backtrack snum pnum naborts; - try_print_subgoals () - - (********************) (* Proof management *) -let vernac_abort = function - | None -> - Backtrack.mark_unreachable [Pfedit.get_current_proof_name ()]; - delete_current_proof (); - if_verbose msg_info (str "Current goal aborted") - | Some id -> - Backtrack.mark_unreachable [snd id]; - delete_proof id; - let s = Id.to_string (snd id) in - if_verbose msg_info (str ("Goal "^s^" aborted")) - -let vernac_abort_all () = - if refining() then begin - Backtrack.mark_unreachable (Pfedit.get_all_proof_names ()); - delete_all_proofs (); - msg_info (str "Current goals aborted") - end else - error "No proof-editing in progress." - -let vernac_restart () = - Backtrack.mark_unreachable [Pfedit.get_current_proof_name ()]; - restart_proof(); print_subgoals () - -let vernac_undo n = - let d = Pfedit.current_proof_depth () - n in - Backtrack.mark_unreachable ~after:d [Pfedit.get_current_proof_name ()]; - Pfedit.undo n; print_subgoals () - -let vernac_undoto n = - Backtrack.mark_unreachable ~after:n [Pfedit.get_current_proof_name ()]; - Pfedit.undo_todepth n; - print_subgoals () - let vernac_focus gln = - let p = Proof_global.give_me_the_proof () in - let n = match gln with None -> 1 | Some n -> n in - if Int.equal n 0 then - Errors.error "Invalid goal number: 0. Goal numbering starts with 1." - else - try Proof.focus focus_command_cond () n p; print_subgoals () - with Proofview.IndexOutOfRange -> - Errors.error "No such unproven subgoal." + Proof_global.with_current_proof (fun _ p -> + match gln with + | None -> Proof.focus focus_command_cond () 1 p + | Some 0 -> + Errors.error "Invalid goal number: 0. Goal numbering starts with 1." + | Some n -> + Proof.focus focus_command_cond () n p); + print_subgoals () (* Unfocuses one step in the focus stack. *) let vernac_unfocus () = - let p = Proof_global.give_me_the_proof () in - Proof.unfocus command_focus p; print_subgoals () + Proof_global.with_current_proof (fun _ p -> Proof.unfocus command_focus p ()); + print_subgoals () (* Checks that a proof is fully unfocused. Raises an error if not. *) let vernac_unfocused () = @@ -1672,22 +1519,20 @@ let subproof_kind = Proof.new_focus_kind () let subproof_cond = Proof.done_cond subproof_kind let vernac_subproof gln = - let p = Proof_global.give_me_the_proof () in - begin match gln with - | None -> Proof.focus subproof_cond () 1 p - | Some n -> Proof.focus subproof_cond () n p - end ; + Proof_global.with_current_proof (fun _ p -> + match gln with + | None -> Proof.focus subproof_cond () 1 p + | Some n -> Proof.focus subproof_cond () n p); print_subgoals () let vernac_end_subproof () = - let p = Proof_global.give_me_the_proof () in - Proof.unfocus subproof_kind p ; print_subgoals () + Proof_global.with_current_proof (fun _ p -> Proof.unfocus subproof_kind p ()); + print_subgoals () let vernac_bullet (bullet:Proof_global.Bullet.t) = - let p = Proof_global.give_me_the_proof () in - Proof.transaction p - (fun () -> Proof_global.Bullet.put p bullet); + Proof_global.with_current_proof (fun _ p -> + Proof_global.Bullet.put p bullet); (* Makes the focus visible in emacs by re-printing the goal. *) if !Flags.print_emacs then print_subgoals () @@ -1706,7 +1551,7 @@ let vernac_show = function Constrextern.with_implicits msg_notice (pr_nth_open_subgoal n) | ShowProof -> show_proof () | ShowNode -> show_node () - | ShowScript -> show_script () + | ShowScript -> !show_script () | ShowExistentials -> show_top_evars () | ShowTree -> show_prooftree () | ShowProofNames -> @@ -1733,10 +1578,17 @@ let vernac_check_guard () = (* "locality" is the prefix "Local" attribute, while the "local" component * is the outdated/deprecated "Local" attribute of some vernacular commands * still parsed as the obsolete_locality grammar entry for retrocompatibility *) -let interp locality c = match c with - (* Control (done in vernac) *) - | (VernacTime _|VernacList _|VernacLoad _|VernacTimeout _|VernacFail _) -> - assert false +let interp ?proof locality c = + prerr_endline ("interpreting: " ^ Pp.string_of_ppcmds (Ppvernac.pr_vernac c)); + match c with + (* Done in vernac *) + | (VernacList _|VernacLoad _) -> assert false + + (* Done later in this file *) + | VernacFail _ -> assert false + | VernacTime _ -> assert false + | VernacTimeout _ -> assert false + | VernacStm _ -> assert false (* Syntax *) | VernacTacticNotation (n,r,e) -> @@ -1754,7 +1606,7 @@ let interp locality c = match c with (* Gallina *) | VernacDefinition (k,lid,d) -> vernac_definition locality k lid d | VernacStartTheoremProof (k,l,top) -> vernac_start_proof k l top - | VernacEndProof e -> vernac_end_proof e + | VernacEndProof e -> vernac_end_proof ?proof e | VernacExactProof c -> vernac_exact_proof c | VernacAssumption (stre,nl,l) -> vernac_assumption locality stre l nl | VernacInductive (finite,infer,l) -> vernac_inductive finite infer l @@ -1808,10 +1660,10 @@ let interp locality c = match c with | VernacRestoreState s -> vernac_restore_state s (* Resetting *) - | VernacResetName id -> vernac_reset_name id - | VernacResetInitial -> vernac_reset_initial () - | VernacBack n -> vernac_back n - | VernacBackTo n -> vernac_backto n + | VernacResetName _ -> anomaly (str "VernacResetName not handled by Stm") + | VernacResetInitial -> anomaly (str "VernacResetInitial not handled by Stm") + | VernacBack _ -> anomaly (str "VernacBack not handled by Stm") + | VernacBackTo _ -> anomaly (str "VernacBackTo not handled by Stm") (* Commands *) | VernacDeclareTacticDefinition def -> @@ -1848,12 +1700,12 @@ let interp locality c = match c with (* Proof management *) | VernacGoal t -> vernac_start_proof Theorem [None,([],t,None)] false - | VernacAbort id -> vernac_abort id - | VernacAbortAll -> vernac_abort_all () - | VernacRestart -> vernac_restart () - | VernacUndo n -> vernac_undo n - | VernacUndoTo n -> vernac_undoto n - | VernacBacktrack (snum,pnum,naborts) -> vernac_backtrack snum pnum naborts + | VernacAbort id -> anomaly (str "VernacAbort not handled by Stm") + | VernacAbortAll -> anomaly (str "VernacAbortAll not handled by Stm") + | VernacRestart -> anomaly (str "VernacRestart not handled by Stm") + | VernacUndo _ -> anomaly (str "VernacUndo not handled by Stm") + | VernacUndoTo _ -> anomaly (str "VernacUndoTo not handled by Stm") + | VernacBacktrack _ -> anomaly (str "VernacBacktrack not handled by Stm") | VernacFocus n -> vernac_focus n | VernacUnfocus -> vernac_unfocus () | VernacUnfocused -> vernac_unfocused () @@ -1902,24 +1754,119 @@ let check_vernac_supports_locality c l = | VernacExtend _ ) -> () | Some _, _ -> Errors.error "This command does not support Locality" -let interp c = +(** A global default timeout, controled by option "Set Default Timeout n". + Use "Unset Default Timeout" to deactivate it (or set it to 0). *) + +let default_timeout = ref None + +let _ = + Goptions.declare_int_option + { Goptions.optsync = true; + Goptions.optdepr = false; + Goptions.optname = "the default timeout"; + Goptions.optkey = ["Default";"Timeout"]; + Goptions.optread = (fun () -> !default_timeout); + Goptions.optwrite = ((:=) default_timeout) } + +(** When interpreting a command, the current timeout is initially + the default one, but may be modified locally by a Timeout command. *) + +let current_timeout = ref None + +(** Installing and de-installing a timer. + Note: according to ocaml documentation, Unix.alarm isn't available + for native win32. *) + +let timeout_handler _ = raise Timeout + +let set_timeout n = + let psh = + Sys.signal Sys.sigalrm (Sys.Signal_handle timeout_handler) in + ignore (Unix.alarm n); + Some psh + +let default_set_timeout () = + match !current_timeout with + | Some n -> set_timeout n + | None -> None + +let restore_timeout = function + | None -> () + | Some psh -> + (* stop alarm *) + ignore(Unix.alarm 0); + (* restore handler *) + Sys.set_signal Sys.sigalrm psh + +let locate_if_not_already loc exn = + match Loc.get_loc exn with + | None -> Loc.add_loc exn loc + | Some l -> if Loc.is_ghost l then Loc.add_loc exn loc else exn + +exception HasNotFailed +exception HasFailed of string + +let interp ?(verbosely=true) ?proof (loc,c) = let orig_program_mode = Flags.is_program_mode () in let rec aux ?locality isprogcmd = function | VernacProgram c when not isprogcmd -> aux ?locality true c | VernacProgram _ -> Errors.error "Program mode specified twice" | VernacLocal (b, c) when locality = None -> aux ~locality:b isprogcmd c | VernacLocal _ -> Errors.error "Locality specified twice" + | VernacStm (Command c) -> aux ?locality isprogcmd c + | VernacStm _ -> assert false (* Done by Stm *) + | VernacFail v -> + begin try + (* If the command actually works, ignore its effects on the state. + * Note that error has to be printed in the right state, hence + * within the purified function *) + Future.purify + (fun v -> + try + aux ?locality isprogcmd v; + raise HasNotFailed + with + | HasNotFailed as e -> raise e + | e -> raise (HasFailed (Pp.string_of_ppcmds + (Errors.print (Cerrors.process_vernac_interp_error e))))) + v + with e when Errors.noncritical e -> + let e = Errors.push e in + match e with + | HasNotFailed -> + errorlabstrm "Fail" (str "The command has not failed!") + | HasFailed msg -> + if_verbose msgnl + (str "The command has indeed failed with message:" ++ + fnl () ++ str "=> " ++ hov 0 (str msg)) + | _ -> assert false + end + | VernacTimeout (n,v) -> + current_timeout := Some n; + aux ?locality isprogcmd v + | VernacTime v -> + let tstart = System.get_time() in + aux ?locality isprogcmd v; + let tend = System.get_time() in + let msg = if !Flags.time then "" else "Finished transaction in " in + msg_info (str msg ++ System.fmt_time_difference tstart tend) | c -> check_vernac_supports_locality c locality; Obligations.set_program_mode isprogcmd; + let psh = default_set_timeout () in try - interp locality c; + if verbosely then Flags.verbosely (interp ?proof locality) c + else Flags.silently (interp ?proof locality) c; + restore_timeout psh; if orig_program_mode || not !Flags.program_mode || isprogcmd then Flags.program_mode := orig_program_mode with - | reraise -> + | reraise when Errors.noncritical reraise -> let e = Errors.push reraise in + let e = locate_if_not_already loc e in + restore_timeout psh; Flags.program_mode := orig_program_mode; raise e in aux false c + diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli index 5a6550d56e..3f6d45a049 100644 --- a/toplevel/vernacentries.mli +++ b/toplevel/vernacentries.mli @@ -17,7 +17,7 @@ val dump_global : Libnames.reference or_by_notation -> unit (** Vernacular entries *) -val show_script : unit -> unit +val show_script : (?proof:Proof_global.closed_proof -> unit -> unit) ref val show_prooftree : unit -> unit val show_node : unit -> unit @@ -27,12 +27,16 @@ val show_node : unit -> unit val get_current_context_of_args : int option -> Evd.evar_map * Environ.env (** The main interpretation function of vernacular expressions *) -val interp : Vernacexpr.vernac_expr -> unit +val interp : + ?verbosely:bool -> + ?proof:Proof_global.closed_proof -> + Loc.t * Vernacexpr.vernac_expr -> unit (** Print subgoals when the verbose flag is on. Meant to be used inside vernac commands from plugins. *) val print_subgoals : unit -> unit +val try_print_subgoals : unit -> unit (** The printing of goals via [print_subgoals] or during [interp] can be controlled by the following flag. @@ -53,3 +57,6 @@ val qed_display_script : bool ref a known inductive type. *) val make_cases : string -> string list list + +val vernac_end_proof : + ?proof:Proof_global.closed_proof -> Vernacexpr.proof_end -> unit diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4 index 8929fb32cf..8185e5702c 100644 --- a/toplevel/whelp.ml4 +++ b/toplevel/whelp.ml4 @@ -192,8 +192,8 @@ let whelp_elim ind = send_whelp "elim" (make_string uri_of_global (IndRef ind)) let on_goal f = - let { Evd.it=goals ; sigma=sigma } = Proof.V82.subgoals (get_pftreestate ()) in - let gls = { Evd.it=List.hd goals ; sigma = sigma } in + let gls = Proof.V82.subgoals (get_pftreestate ()) in + let gls = { gls with Evd.it = List.hd gls.Evd.it } in f (Termops.it_mkNamedProd_or_LetIn (pf_concl gls) (pf_hyps gls)) type whelp_request = |