diff options
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 82445a0fd..e63c22bf8 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 b05f94c3c..660f6f7e7 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 049d631bf..e9601c123 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 e259da7af..000000000 --- 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 d4ac7cc61..000000000 --- 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 14473e46f..f9ce75bba 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 e4064049e..a217abbba 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 1d9ae6ec4..5a0dc97c2 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 369abd3f8..d730d8ef1 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 71eec3295..76a3c5802 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 cb587a6ef..1dba38001 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 709062f1f..821830203 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 f55a12f9d..0a5f7d25f 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 9dd25c63e..c5e82e2e2 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 8551c2038..bf07156f7 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 695426d56..6876483a0 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 d6bc90bc3..e8998d608 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 44ff40f24..9e7ddd5a6 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 bc092a1ce..ddc99a96c 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 ff918293b..476da3d0e 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 000000000..004ac9428 --- /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 000000000..d4898b30f --- /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 9a2b8840c..dcf2b0b3d 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 b27c7588d..d58df57f2 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 fcffb343e..e05ced2b8 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 bda42dfa6..d18571990 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 000000000..d7b9553a0 --- /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 000000000..06535d512 --- /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 88da26e83..706b757db 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 5a6550d56..3f6d45a04 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 8929fb32c..8185e5702 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 = |