diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/lemmas.ml | 557 | ||||
| -rw-r--r-- | stm/lemmas.mli | 69 | ||||
| -rw-r--r-- | stm/stm.ml | 59 | ||||
| -rw-r--r-- | stm/stm.mli | 5 | ||||
| -rw-r--r-- | stm/stm.mllib | 1 |
5 files changed, 32 insertions, 659 deletions
diff --git a/stm/lemmas.ml b/stm/lemmas.ml deleted file mode 100644 index 55f33be399..0000000000 --- a/stm/lemmas.ml +++ /dev/null @@ -1,557 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(* Created by Hugo Herbelin from contents related to lemma proofs in - file command.ml, Aug 2009 *) - -open CErrors -open Util -open Flags -open Pp -open Names -open Term -open Declarations -open Declareops -open Entries -open Environ -open Nameops -open Globnames -open Decls -open Decl_kinds -open Declare -open Pretyping -open Termops -open Namegen -open Reductionops -open Constrexpr -open Constrintern -open Impargs -open Context.Rel.Declaration - -module RelDecl = Context.Rel.Declaration -module NamedDecl = Context.Named.Declaration - -type 'a declaration_hook = Decl_kinds.locality -> Globnames.global_reference -> 'a -let mk_hook hook = hook -let call_hook fix_exn hook l c = - try hook l c - with e when CErrors.noncritical e -> - let e = CErrors.push e in - iraise (fix_exn e) - -(* Support for mutually proved theorems *) - -let retrieve_first_recthm = function - | VarRef id -> - (NamedDecl.get_value (Global.lookup_named id),variable_opacity id) - | ConstRef cst -> - let cb = Global.lookup_constant cst in - (Global.body_of_constant_body cb, is_opaque cb) - | _ -> assert false - -let adjust_guardness_conditions const = function - | [] -> const (* Not a recursive statement *) - | possible_indexes -> - (* Try all combinations... not optimal *) - let env = Global.env() in - { const with const_entry_body = - Future.chain ~greedy:true ~pure:true const.const_entry_body - (fun ((body, ctx), 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 add c cb e = - let exists c e = - try ignore(Environ.lookup_constant c e); true - with Not_found -> false in - if exists c e then e else Environ.add_constant c cb e in - let env = List.fold_left (fun env { eff } -> - match eff with - | SEsubproof (c, cb,_) -> add c cb env - | SEscheme (l,_) -> - List.fold_left (fun e (_,c,cb,_) -> add c cb e) env l) - env (Safe_typing.side_effects_of_private_constants eff) in - let indexes = - search_guard Loc.ghost env - possible_indexes fixdecls in - (mkFix ((indexes,0),fixdecls), ctx), eff - | _ -> (body, ctx), eff) } - -let find_mutually_recursive_statements thms = - let n = List.length thms in - let inds = List.map (fun (id,(t,impls,annot)) -> - let (hyps,ccl) = decompose_prod_assum t in - let x = (id,(t,impls)) in - match annot with - (* Explicit fixpoint decreasing argument is given *) - | Some (Some (_,id),CStructRec) -> - let i,b,typ = lookup_rel_id id hyps in - (match kind_of_term t with - | Ind ((kn,_ as ind), u) when - let mind = Global.lookup_mind kn in - mind.mind_finite == Decl_kinds.Finite && Option.is_empty b -> - [ind,x,i],[] - | _ -> - error "Decreasing argument is not an inductive assumption.") - (* Unsupported cases *) - | Some (_,(CWfRec _|CMeasureRec _)) -> - error "Only structural decreasing is supported for mutual statements." - (* Cofixpoint or fixpoint w/o explicit decreasing argument *) - | None | Some (None, CStructRec) -> - let whnf_hyp_hds = map_rel_context_in_env - (fun env c -> fst (whd_all_stack env Evd.empty c)) - (Global.env()) hyps in - let ind_hyps = - List.flatten (List.map_i (fun i decl -> - let t = RelDecl.get_type decl in - match kind_of_term t with - | Ind ((kn,_ as ind),u) when - let mind = Global.lookup_mind kn in - mind.mind_finite <> Decl_kinds.CoFinite && is_local_assum decl -> - [ind,x,i] - | _ -> - []) 0 (List.rev whnf_hyp_hds)) in - let ind_ccl = - let cclenv = push_rel_context hyps (Global.env()) in - let whnf_ccl,_ = whd_all_stack cclenv Evd.empty ccl in - match kind_of_term whnf_ccl with - | Ind ((kn,_ as ind),u) when - let mind = Global.lookup_mind kn in - Int.equal mind.mind_ntypes n && mind.mind_finite == Decl_kinds.CoFinite -> - [ind,x,0] - | _ -> - [] in - ind_hyps,ind_ccl) thms in - let inds_hyps,ind_ccls = List.split inds in - let of_same_mutind ((kn,_),_,_) = function ((kn',_),_,_) -> eq_mind kn kn' in - (* Check if all conclusions are coinductive in the same type *) - (* (degenerated cartesian product since there is at most one coind ccl) *) - let same_indccl = - List.cartesians_filter (fun hyp oks -> - if List.for_all (of_same_mutind hyp) oks - then Some (hyp::oks) else None) [] ind_ccls in - let ordered_same_indccl = - List.filter (List.for_all_i (fun i ((kn,j),_,_) -> Int.equal i j) 0) same_indccl in - (* Check if some hypotheses are inductive in the same type *) - let common_same_indhyp = - List.cartesians_filter (fun hyp oks -> - if List.for_all (of_same_mutind hyp) oks - then Some (hyp::oks) else None) [] inds_hyps in - let ordered_inds,finite,guard = - match ordered_same_indccl, common_same_indhyp with - | indccl::rest, _ -> - assert (List.is_empty rest); - (* One occ. of common coind ccls and no common inductive hyps *) - if not (List.is_empty common_same_indhyp) then - if_verbose Feedback.msg_info (str "Assuming mutual coinductive statements."); - flush_all (); - indccl, true, [] - | [], _::_ -> - let () = match same_indccl with - | ind :: _ -> - if List.distinct_f ind_ord (List.map pi1 ind) - then - if_verbose Feedback.msg_info - (strbrk - ("Coinductive statements do not follow the order of "^ - "definition, assuming the proof to be by induction.")); - flush_all () - | _ -> () - in - let possible_guards = List.map (List.map pi3) inds_hyps in - (* assume the largest indices as possible *) - List.last common_same_indhyp, false, possible_guards - | _, [] -> - error - ("Cannot find common (mutual) inductive premises or coinductive" ^ - " conclusions in the statements.") - in - (finite,guard,None), ordered_inds - -let look_for_possibly_mutual_statements = function - | [id,(t,impls,None)] -> - (* One non recursively proved theorem *) - None,[id,(t,impls)],None - | _::_ as thms -> - (* More than one statement and/or an explicit decreasing mark: *) - (* we look for a common inductive hyp or a common coinductive conclusion *) - let recguard,ordered_inds = find_mutually_recursive_statements thms in - let thms = List.map pi2 ordered_inds in - Some recguard,thms, Some (List.map (fun (_,_,i) -> succ i) ordered_inds) - | [] -> anomaly (Pp.str "Empty list of theorems.") - -(* Saving a goal *) - -let save ?export_seff id const cstrs pl do_guard (locality,poly,kind) hook = - let fix_exn = Future.fix_exn_of const.Entries.const_entry_body in - try - 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 - | Discharge when Lib.sections_are_opened () -> - let c = SectionLocalDef const in - let _ = declare_variable id (Lib.cwd(), c, k) in - (Local, VarRef id) - | Local | Global | Discharge -> - let local = match locality with - | Local | Discharge -> true - | Global -> false - in - let kn = - declare_constant ?export_seff id ~local (DefinitionEntry const, k) in - (locality, ConstRef kn) in - definition_message id; - Option.iter (Universes.register_universe_binders r) pl; - call_hook (fun exn -> exn) hook l r - with e when CErrors.noncritical e -> - let e = CErrors.push e in - iraise (fix_exn e) - -let default_thm_id = Id.of_string "Unnamed_thm" - -let compute_proof_name locality = function - | Some ((loc,id),pl) -> - (* We check existence here: it's a bit late at Qed time *) - if Nametab.exists_cci (Lib.make_path id) || is_section_variable id || - locality == Global && Nametab.exists_cci (Lib.make_path_except_section id) - then - user_err ~loc (pr_id id ++ str " already exists."); - id, pl - | None -> - next_global_ident_away default_thm_id (Pfedit.get_all_proof_names ()), None - -let save_remaining_recthms (locality,p,kind) norm ctx body opaq i ((id,pl),(t_i,(_,imps))) = - let t_i = norm t_i in - match body with - | None -> - (match locality with - | Discharge -> - let impl = false in (* copy values from Vernacentries *) - let k = IsAssumption Conjectural in - let c = SectionLocalAssum ((t_i,ctx),p,impl) in - let _ = declare_variable id (Lib.cwd(),c,k) in - (Discharge, VarRef id,imps) - | Local | Global -> - let k = IsAssumption Conjectural in - let local = match locality with - | Local -> true - | Global -> false - | Discharge -> assert false - in - let ctx = Univ.ContextSet.to_context ctx in - let decl = (ParameterEntry (None,p,(t_i,ctx),None), k) in - let kn = declare_constant id ~local decl in - (locality,ConstRef kn,imps)) - | Some body -> - let body = norm body in - let k = Kindops.logical_kind_of_goal_kind kind in - let rec body_i t = match kind_of_term t with - | Fix ((nv,0),decls) -> mkFix ((nv,i),decls) - | CoFix (0,decls) -> mkCoFix (i,decls) - | LetIn(na,t1,ty,t2) -> mkLetIn (na,t1,ty, body_i t2) - | Lambda(na,ty,t) -> mkLambda(na,ty,body_i t) - | App (t, args) -> mkApp (body_i t, args) - | _ -> anomaly Pp.(str "Not a proof by induction: " ++ Printer.pr_constr body) in - let body_i = body_i body in - match locality with - | Discharge -> - let const = definition_entry ~types:t_i ~opaque:opaq ~poly:p - ~univs:(Univ.ContextSet.to_context ctx) body_i in - let c = SectionLocalDef const in - let _ = declare_variable id (Lib.cwd(), c, k) in - (Discharge,VarRef id,imps) - | Local | Global -> - let ctx = Univ.ContextSet.to_context ctx in - let local = match locality with - | Local -> true - | Global -> false - | Discharge -> assert false - in - let const = - Declare.definition_entry ~types:t_i ~poly:p ~univs:ctx ~opaque:opaq body_i - in - let kn = declare_constant id ~local (DefinitionEntry const, k) in - (locality,ConstRef kn,imps) - -let save_hook = ref ignore -let set_save_hook f = save_hook := f - -let save_named ?export_seff proof = - let id,const,(cstrs,pl),do_guard,persistence,hook = proof in - save ?export_seff id const cstrs pl 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 ?export_seff proof save_ident = - let id,const,(cstrs,pl),do_guard,persistence,hook = proof in - check_anonymity id save_ident; - save ?export_seff save_ident const cstrs pl do_guard persistence hook - -let save_anonymous_with_strength ?export_seff proof kind save_ident = - let id,const,(cstrs,pl),do_guard,_,hook = proof in - check_anonymity id save_ident; - (* we consider that non opaque behaves as local for discharge *) - save ?export_seff save_ident const cstrs pl do_guard - (Global, const.const_entry_polymorphic, Proof kind) hook - -(* Admitted *) - -let warn_let_as_axiom = - CWarnings.create ~name:"let-as-axiom" ~category:"vernacular" - (fun id -> strbrk "Let definition" ++ spc () ++ pr_id id ++ - spc () ++ strbrk "declared as an axiom.") - -let admit (id,k,e) pl hook () = - let kn = declare_constant id (ParameterEntry e, IsAssumption Conjectural) in - let () = match k with - | Global, _, _ -> () - | Local, _, _ | Discharge, _, _ -> warn_let_as_axiom id - in - let () = assumption_message id in - Option.iter (Universes.register_universe_binders (ConstRef kn)) pl; - call_hook (fun exn -> exn) hook Global (ConstRef kn) - -(* Starting a goal *) - -let start_hook = ref ignore -let set_start_hook = (:=) start_hook - - -let get_proof proof do_guard hook opacity = - let (id,(const,univs,persistence)) = - Pfedit.cook_this_proof proof - in - id,{const with const_entry_opaque = opacity},univs,do_guard,persistence,hook - -let check_exist = - List.iter (fun (loc,id) -> - if not (Nametab.exists_cci (Lib.make_path id)) then - user_err ~loc (pr_id id ++ str " does not exist.") - ) - -let universe_proof_terminator compute_guard hook = - let open Proof_global in - make_terminator begin function - | Admitted (id,k,pe,(ctx,pl)) -> - admit (id,k,pe) pl (hook (Some ctx)) (); - Feedback.feedback Feedback.AddedAxiom - | Proved (opaque,idopt,proof) -> - let is_opaque, export_seff, exports = match opaque with - | Vernacexpr.Transparent -> false, true, [] - | Vernacexpr.Opaque None -> true, false, [] - | Vernacexpr.Opaque (Some l) -> true, true, l in - let proof = get_proof proof compute_guard - (hook (Some (fst proof.Proof_global.universes))) is_opaque in - begin match idopt with - | None -> save_named ~export_seff proof - | Some ((_,id),None) -> save_anonymous ~export_seff proof id - | Some ((_,id),Some kind) -> - save_anonymous_with_strength ~export_seff proof kind id - end; - check_exist exports - end - -let standard_proof_terminator compute_guard hook = - universe_proof_terminator compute_guard (fun _ -> hook) - -let start_proof id ?pl kind sigma ?terminator ?sign c ?init_tac ?(compute_guard=[]) hook = - let terminator = match terminator with - | None -> standard_proof_terminator compute_guard hook - | Some terminator -> terminator compute_guard hook - in - let sign = - match sign with - | Some sign -> sign - | None -> initialize_named_context_for_proof () - in - !start_hook c; - Pfedit.start_proof id ?pl kind sigma sign c ?init_tac terminator - -let start_proof_univs id ?pl kind sigma ?terminator ?sign c ?init_tac ?(compute_guard=[]) hook = - let terminator = match terminator with - | None -> universe_proof_terminator compute_guard hook - | Some terminator -> terminator compute_guard hook - in - let sign = - match sign with - | Some sign -> sign - | None -> initialize_named_context_for_proof () - in - !start_hook c; - Pfedit.start_proof id ?pl kind sigma sign c ?init_tac terminator - -let rec_tac_initializer finite guard thms snl = - if finite then - match List.map (fun ((id,_),(t,_)) -> (id,t)) thms with - | (id,_)::l -> Tactics.mutual_cofix id l 0 - | _ -> assert false - else - (* nl is dummy: it will be recomputed at Qed-time *) - let nl = match snl with - | None -> List.map succ (List.map List.last guard) - | Some nl -> nl - in match List.map2 (fun ((id,_),(t,_)) n -> (id,n,t)) thms nl with - | (id,n,_)::l -> Tactics.mutual_fix id n l 0 - | _ -> assert false - -let start_proof_with_initialization kind ctx recguard thms snl hook = - let intro_tac (_, (_, (ids, _))) = - Tacticals.New.tclMAP (function - | Name id -> Tactics.intro_mustbe_force id - | Anonymous -> Tactics.intro) (List.rev ids) in - let init_tac,guard = match recguard with - | Some (finite,guard,init_tac) -> - let rec_tac = rec_tac_initializer finite guard thms snl in - Some (match init_tac with - | None -> - if Flags.is_auto_intros () then - Tacticals.New.tclTHENS rec_tac (List.map intro_tac thms) - else - rec_tac - | Some tacl -> - Tacticals.New.tclTHENS rec_tac - (if Flags.is_auto_intros () then - List.map2 (fun tac thm -> Tacticals.New.tclTHEN tac (intro_tac thm)) tacl thms - else - tacl)),guard - | None -> - let () = match thms with [_] -> () | _ -> assert false in - (if Flags.is_auto_intros () then Some (intro_tac (List.hd thms)) else None), [] in - match thms with - | [] -> anomaly (Pp.str "No proof to start") - | ((id,pl),(t,(_,imps)))::other_thms -> - let hook ctx strength ref = - let ctx = match ctx with - | None -> Evd.empty_evar_universe_context - | Some ctx -> ctx - in - let other_thms_data = - if List.is_empty other_thms then [] else - (* there are several theorems defined mutually *) - let body,opaq = retrieve_first_recthm ref in - let subst = Evd.evar_universe_context_subst ctx in - let norm c = Universes.subst_opt_univs_constr subst c in - let ctx = UState.context_set (*FIXME*) ctx in - let body = Option.map norm body in - List.map_i (save_remaining_recthms kind norm ctx body opaq) 1 other_thms in - let thms_data = (strength,ref,imps)::other_thms_data in - List.iter (fun (strength,ref,imps) -> - maybe_declare_manual_implicits false ref imps; - call_hook (fun exn -> exn) hook strength ref) thms_data in - start_proof_univs id ?pl kind ctx t ?init_tac (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard - -let start_proof_com ?inference_hook kind thms hook = - let env0 = Global.env () in - let levels = Option.map snd (fst (List.hd thms)) in - let evdref = ref (match levels with - | None -> Evd.from_env env0 - | Some l -> Evd.from_ctx (Evd.make_evar_universe_context env0 l)) - in - let thms = List.map (fun (sopt,(bl,t,guard)) -> - let impls, ((env, ctx), imps) = interp_context_evars env0 evdref bl in - let t', imps' = interp_type_evars_impls ~impls env evdref t in - let flags = all_and_fail_flags in - let flags = { flags with use_hook = inference_hook } in - evdref := solve_remaining_evars flags env !evdref (Evd.empty,!evdref); - let ids = List.map RelDecl.get_name ctx in - (compute_proof_name (pi1 kind) sopt, - (nf_evar !evdref (it_mkProd_or_LetIn t' ctx), - (ids, imps @ lift_implicits (List.length ids) imps'), - guard))) - thms in - let recguard,thms,snl = look_for_possibly_mutual_statements thms in - let evd, nf = Evarutil.nf_evars_and_universes !evdref in - let thms = List.map (fun (n, (t, info)) -> (n, (nf t, info))) thms in - let () = - match levels with - | None -> () - | Some l -> ignore (Evd.universe_context evd ?names:l) - in - let evd = - if pi2 kind then evd - else (* We fix the variables to ensure they won't be lowered to Set *) - Evd.fix_undefined_variables evd - in - start_proof_with_initialization kind evd recguard thms snl hook - - -(* Saving a proof *) - -let keep_admitted_vars = ref true - -let _ = - let open Goptions in - declare_bool_option - { optsync = true; - optdepr = false; - optname = "keep section variables in admitted proofs"; - optkey = ["Keep"; "Admitted"; "Variables"]; - optread = (fun () -> !keep_admitted_vars); - optwrite = (fun b -> keep_admitted_vars := b) } - -let save_proof ?proof = function - | Vernacexpr.Admitted -> - let pe = - let open Proof_global in - match proof with - | Some ({ id; entries; persistence = k; universes }, _) -> - if List.length entries <> 1 then - error "Admitted does not support multiple statements"; - let { const_entry_secctx; const_entry_type } = List.hd entries in - if const_entry_type = None then - error "Admitted requires an explicit statement"; - let typ = Option.get const_entry_type in - let ctx = Evd.evar_context_universe_context (fst universes) in - let sec_vars = if !keep_admitted_vars then const_entry_secctx else None in - Admitted(id, k, (sec_vars, pi2 k, (typ, ctx), None), universes) - | None -> - let pftree = Pfedit.get_pftreestate () in - let id, k, typ = Pfedit.current_proof_statement () in - let universes = Proof.initial_euctx pftree in - (* This will warn if the proof is complete *) - let pproofs, _univs = - Proof_global.return_proof ~allow_partial:true () in - let sec_vars = - if not !keep_admitted_vars then None - else match Pfedit.get_used_variables(), pproofs with - | Some _ as x, _ -> x - | None, (pproof, _) :: _ -> - let env = Global.env () in - let ids_typ = Environ.global_vars_set env typ in - let ids_def = Environ.global_vars_set env pproof in - Some (Environ.keep_hyps env (Idset.union ids_typ ids_def)) - | _ -> None in - let names = Pfedit.get_universe_binders () in - let evd = Evd.from_ctx universes in - let binders, ctx = Evd.universe_context ?names evd in - Admitted(id,k,(sec_vars, pi2 k, (typ, ctx), None), - (universes, Some binders)) - in - Proof_global.apply_terminator (Proof_global.get_terminator ()) pe - | Vernacexpr.Proved (is_opaque,idopt) -> - let (proof_obj,terminator) = - match proof with - | None -> - Proof_global.close_proof ~keep_body_ucst_separate:false (fun x -> x) - | Some proof -> proof - in - (* if the proof is given explicitly, nothing has to be deleted *) - if Option.is_empty proof then Pfedit.delete_current_proof (); - Proof_global.(apply_terminator terminator (Proved (is_opaque,idopt,proof_obj))) - -(* Miscellaneous *) - -let get_current_context () = - Pfedit.get_current_context () - diff --git a/stm/lemmas.mli b/stm/lemmas.mli deleted file mode 100644 index 39c089be9f..0000000000 --- a/stm/lemmas.mli +++ /dev/null @@ -1,69 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Names -open Term -open Decl_kinds -open Pfedit - -type 'a declaration_hook -val mk_hook : - (Decl_kinds.locality -> Globnames.global_reference -> 'a) -> 'a declaration_hook - -val call_hook : - Future.fix_exn -> 'a declaration_hook -> Decl_kinds.locality -> Globnames.global_reference -> 'a - -(** A hook start_proof calls on the type of the definition being started *) -val set_start_hook : (types -> unit) -> unit - -val start_proof : Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map -> - ?terminator:(lemma_possible_guards -> unit declaration_hook -> Proof_global.proof_terminator) -> - ?sign:Environ.named_context_val -> types -> - ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> - unit declaration_hook -> unit - -val start_proof_univs : Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map -> - ?terminator:(lemma_possible_guards -> (Evd.evar_universe_context option -> unit declaration_hook) -> Proof_global.proof_terminator) -> - ?sign:Environ.named_context_val -> types -> - ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> - (Evd.evar_universe_context option -> unit declaration_hook) -> unit - -val start_proof_com : - ?inference_hook:Pretyping.inference_hook -> - goal_kind -> Vernacexpr.proof_expr list -> - unit declaration_hook -> unit - -val start_proof_with_initialization : - goal_kind -> Evd.evar_map -> - (bool * lemma_possible_guards * unit Proofview.tactic list option) option -> - ((Id.t * universe_binders option) * - (types * (Name.t list * Impargs.manual_explicitation list))) list - -> int list option -> unit declaration_hook -> unit - -val universe_proof_terminator : - Proof_global.lemma_possible_guards -> - (Evd.evar_universe_context option -> unit declaration_hook) -> - Proof_global.proof_terminator - -val standard_proof_terminator : - Proof_global.lemma_possible_guards -> unit declaration_hook -> - Proof_global.proof_terminator - -(** {6 ... } *) - -(** A hook the next three functions pass to cook_proof *) -val set_save_hook : (Proof.proof -> unit) -> unit - -val save_proof : ?proof:Proof_global.closed_proof -> Vernacexpr.proof_end -> unit - - -(** [get_current_context ()] returns the evar context and env of the - current open proof if any, otherwise returns the empty evar context - and the current global env *) - -val get_current_context : unit -> Evd.evar_map * Environ.env diff --git a/stm/stm.ml b/stm/stm.ml index 6f34c8dbc3..be3e841cb9 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -24,11 +24,13 @@ open Ppvernac open Vernac_classifier open Feedback +let execution_error state_id loc msg = + feedback ~id:(State state_id) + (Message (Error, Some loc, pp_to_richpp msg)) + module Hooks = struct let process_error, process_error_hook = Hook.make () -let interp, interp_hook = Hook.make () -let with_fail, with_fail_hook = Hook.make () let state_computed, state_computed_hook = Hook.make ~default:(fun state_id ~in_cache -> @@ -48,10 +50,6 @@ let parse_error, parse_error_hook = Hook.make ~default:(fun id loc msg -> feedback ~id (Message(Error, Some loc, pp_to_richpp msg))) () -let execution_error, execution_error_hook = Hook.make - ~default:(fun state_id loc msg -> - feedback ~id:(State state_id) (Message(Error, Some loc, pp_to_richpp msg))) () - let unreachable_state, unreachable_state_hook = Hook.make ~default:(fun _ _ -> ()) () @@ -106,24 +104,36 @@ let may_pierce_opaque = function | _ -> false (* Wrapper for Vernacentries.interp to set the feedback id *) -let vernac_interp ?proof id ?route { verbose; loc; expr } = - let rec internal_command = function - | VernacResetName _ | VernacResetInitial | VernacBack _ - | VernacBackTo _ | VernacRestart | VernacUndo _ | VernacUndoTo _ - | VernacBacktrack _ | VernacAbortAll | VernacAbort _ -> true - | VernacTime (_,e) | VernacTimeout (_,e) | VernacRedirect (_,(_,e)) -> internal_command e - | _ -> false in - if internal_command expr then begin +(* It is currently called 19 times, this number should be certainly + reduced... *) +let stm_vernac_interp ?proof id ?route { verbose; loc; expr } = + (* The Stm will gain the capability to interpret commmads affecting + the whole document state, such as backtrack, etc... so we start + to design the stm command interpreter now *) + set_id_for_feedback ?route (State id); + Aux_file.record_in_aux_set_at loc; + (* We need to check if a command should be filtered from + * vernac_entries, as it cannot handle it. This should go away in + * future refactorings. + *) + let rec is_filtered_command = function + | VernacResetName _ | VernacResetInitial | VernacBack _ + | VernacBackTo _ | VernacRestart | VernacUndo _ | VernacUndoTo _ + | VernacBacktrack _ | VernacAbortAll | VernacAbort _ -> true + | VernacTime (_,e) | VernacTimeout (_,e) | VernacRedirect (_,(_,e)) -> is_filtered_command e + | _ -> false + in + let aux_interp cmd = + if is_filtered_command cmd then prerr_endline (fun () -> "ignoring " ^ Pp.string_of_ppcmds(pr_vernac expr)) - end else begin - set_id_for_feedback ?route (State id); - Aux_file.record_in_aux_set_at loc; + else match cmd with + | expr -> prerr_endline (fun () -> "interpreting " ^ Pp.string_of_ppcmds(pr_vernac expr)); - try Hooks.(call interp ?verbosely:(Some verbose) ?proof (loc, expr)) + try Vernacentries.interp ?verbosely:(Some verbose) ?proof (loc, expr) with e -> let e = CErrors.push e in iraise Hooks.(call_process_error_once e) - end + in aux_interp expr (* Wrapper for Vernac.parse_sentence to set the feedback id *) let indentation_of_string s = @@ -860,7 +870,7 @@ end = struct (* {{{ *) | None -> let loc = Option.default Loc.ghost (Loc.get_loc info) in let (e, info) = Hooks.(call_process_error_once (e, info)) in - Hooks.(call execution_error id loc (iprint (e, info))); + execution_error id loc (iprint (e, info)); (e, Stateid.add info ~valid id) let same_env { system = s1 } { system = s2 } = @@ -910,7 +920,6 @@ end = struct (* {{{ *) end (* }}} *) - (****************************** CRUFT *****************************************) (******************************************************************************) @@ -1287,7 +1296,7 @@ end = struct (* {{{ *) let info = Stateid.add ~valid:start Exninfo.null start in let e = (RemoteException (strbrk s), info) in t_assign (`Exn e); - Hooks.(call execution_error start Loc.ghost (strbrk s)); + execution_error start Loc.ghost (strbrk s); feedback (InProgress ~-1) let build_proof_here ~drop_pt (id,valid) loc eop = @@ -1750,7 +1759,7 @@ end = struct (* {{{ *) | VernacTime (_,e) | VernacRedirect (_,(_,e)) -> find true fail e | VernacFail e -> find time true e | _ -> e, time, fail in find false false e in - Hooks.call Hooks.with_fail fail (fun () -> + Vernacentries.with_fail fail (fun () -> (if time then System.with_time false else (fun x -> x)) (fun () -> ignore(TaskQueue.with_n_workers nworkers (fun queue -> Proof_global.with_current_proof (fun _ p -> @@ -2946,12 +2955,8 @@ let show_script ?proof () = let state_computed_hook = Hooks.state_computed_hook let state_ready_hook = Hooks.state_ready_hook let parse_error_hook = Hooks.parse_error_hook -let execution_error_hook = Hooks.execution_error_hook let forward_feedback_hook = Hooks.forward_feedback_hook let process_error_hook = Hooks.process_error_hook -let interp_hook = Hooks.interp_hook -let with_fail_hook = Hooks.with_fail_hook let unreachable_state_hook = Hooks.unreachable_state_hook -let get_fix_exn () = !State.fix_exn_ref let tactic_being_run_hook = Hooks.tactic_being_run_hook (* vim:set foldmethod=marker: *) diff --git a/stm/stm.mli b/stm/stm.mli index b8a2a38596..36341a5d51 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -184,7 +184,6 @@ val register_proof_block_delimiter : val state_computed_hook : (Stateid.t -> in_cache:bool -> unit) Hook.t val parse_error_hook : (Feedback.edit_or_state_id -> Loc.t -> Pp.std_ppcmds -> unit) Hook.t -val execution_error_hook : (Stateid.t -> Loc.t -> Pp.std_ppcmds -> unit) Hook.t val unreachable_state_hook : (Stateid.t -> Exninfo.iexn -> unit) Hook.t (* ready means that master has it at hand *) val state_ready_hook : (Stateid.t -> unit) Hook.t @@ -218,7 +217,3 @@ val show_script : ?proof:Proof_global.closed_proof -> unit -> unit (* Hooks to be set by other Coq components in order to break file cycles *) val process_error_hook : Future.fix_exn Hook.t -val interp_hook : (?verbosely:bool -> ?proof:Proof_global.closed_proof -> - Loc.t * Vernacexpr.vernac_expr -> unit) Hook.t -val with_fail_hook : (bool -> (unit -> unit) -> unit) Hook.t -val get_fix_exn : unit -> (Exninfo.iexn -> Exninfo.iexn) diff --git a/stm/stm.mllib b/stm/stm.mllib index 939ee187ae..4b254e8113 100644 --- a/stm/stm.mllib +++ b/stm/stm.mllib @@ -4,7 +4,6 @@ Vcs TQueue WorkerPool Vernac_classifier -Lemmas CoqworkmgrApi AsyncTaskQueue Stm |