From a0cfa4f118023d35b767a999d5a2ac4b082857b4 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 25 Jul 2008 15:12:53 +0200 Subject: Imported Upstream version 8.2~beta3+dfsg --- proofs/clenvtac.ml | 48 ++++++++++++------ proofs/clenvtac.mli | 15 ++++-- proofs/decl_expr.mli | 3 +- proofs/decl_mode.ml | 26 ++++++---- proofs/decl_mode.mli | 22 ++++---- proofs/evar_refiner.ml | 22 ++++---- proofs/logic.ml | 40 +++++++++------ proofs/logic.mli | 5 +- proofs/pfedit.ml | 16 +++--- proofs/pfedit.mli | 17 ++++--- proofs/proof_trees.ml | 3 +- proofs/proof_type.ml | 8 +-- proofs/proof_type.mli | 8 +-- proofs/redexpr.ml | 103 ++++++++++++++++++++++++++++--------- proofs/redexpr.mli | 16 +++--- proofs/refiner.ml | 124 ++++++++++++++++++++++++++++----------------- proofs/refiner.mli | 24 +++++++-- proofs/tacexpr.ml | 135 ++++++++++++++++++++++++++----------------------- proofs/tacmach.ml | 21 +++----- proofs/tacmach.mli | 11 ++-- proofs/tactic_debug.ml | 2 + 21 files changed, 414 insertions(+), 255 deletions(-) (limited to 'proofs') diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 71538614..92794ac3 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: clenvtac.ml 8023 2006-02-10 18:34:51Z coq $ *) +(* $Id: clenvtac.ml 11166 2008-06-22 13:23:35Z herbelin $ *) open Pp open Util @@ -49,7 +49,7 @@ let clenv_cast_meta clenv = match kind_of_term (strip_outer_cast u) with | Meta mv -> (try - let b = Typing.meta_type clenv.env mv in + let b = Typing.meta_type clenv.evd mv in if occur_meta b then u else mkCast (mkMeta mv, DEFAULTcast, b) with Not_found -> u) @@ -60,25 +60,35 @@ let clenv_cast_meta clenv = in crec -let clenv_refine clenv gls = +let clenv_value_cast_meta clenv = + clenv_cast_meta clenv (clenv_value clenv) + +let clenv_pose_dependent_evars with_evars clenv = + let dep_mvs = clenv_dependent false clenv in + if dep_mvs <> [] & not with_evars then + raise + (RefinerError (UnresolvedBindings (List.map (meta_name clenv.evd) dep_mvs))); + clenv_pose_metas_as_evars clenv dep_mvs + + +let clenv_refine with_evars clenv gls = + let clenv = clenv_pose_dependent_evars with_evars clenv in tclTHEN - (tclEVARS (evars_of clenv.env)) + (tclEVARS (evars_of clenv.evd)) (refine (clenv_cast_meta clenv (clenv_value clenv))) gls +let dft = Unification.default_unify_flags -let res_pf clenv ?(allow_K=false) gls = - clenv_refine (clenv_unique_resolver allow_K clenv gls) gls +let res_pf clenv ?(with_evars=false) ?(allow_K=false) ?(flags=dft) gls = + clenv_refine with_evars + (clenv_unique_resolver allow_K ~flags:flags clenv gls) gls -let elim_res_pf_THEN_i clenv tac gls = +let elim_res_pf_THEN_i clenv tac gls = let clenv' = (clenv_unique_resolver true clenv gls) in - tclTHENLASTn (clenv_refine clenv') (tac clenv') gls - - -let e_res_pf clenv gls = - clenv_refine (evar_clenv_unique_resolver clenv gls) gls - + tclTHENLASTn (clenv_refine false clenv') (tac clenv') gls +let e_res_pf clenv = res_pf clenv ~with_evars:true ~allow_K:false ~flags:dft (* [unifyTerms] et [unify] ne semble pas gérer les Meta, en @@ -86,11 +96,19 @@ let e_res_pf clenv gls = d'une même Meta sont compatibles. D'ailleurs le "fst" jette les metas provenant de w_Unify. (Utilisé seulement dans prolog.ml) *) +open Unification + +let fail_quick_unif_flags = { + modulo_conv_on_closed_terms = Some full_transparent_state; + use_metas_eagerly = false; + modulo_delta = empty_transparent_state; +} + (* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *) let unifyTerms m n gls = let env = pf_env gls in - let evd = create_evar_defs (project gls) in - let evd' = Unification.w_unify false env CONV m n evd in + let evd = create_goal_evar_defs (project gls) in + let evd' = w_unify false env CONV ~flags:fail_quick_unif_flags m n evd in tclIDTAC {it = gls.it; sigma = evars_of evd'} let unify m gls = diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli index 505826fa..29442ded 100644 --- a/proofs/clenvtac.mli +++ b/proofs/clenvtac.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: clenvtac.mli 6099 2004-09-12 11:38:09Z barras $ i*) +(*i $Id: clenvtac.mli 11166 2008-06-22 13:23:35Z herbelin $ i*) (*i*) open Util @@ -16,11 +16,18 @@ open Sign open Evd open Clenv open Proof_type +open Tacexpr +open Unification (*i*) (* Tactics *) val unify : constr -> tactic -val clenv_refine : clausenv -> tactic -val res_pf : clausenv -> ?allow_K:bool -> tactic -val e_res_pf : clausenv -> tactic +val clenv_refine : evars_flag -> clausenv -> tactic +val res_pf : clausenv -> ?with_evars:evars_flag -> ?allow_K:bool -> ?flags:unify_flags -> tactic val elim_res_pf_THEN_i : clausenv -> (clausenv -> tactic array) -> tactic + +val clenv_pose_dependent_evars : evars_flag -> clausenv -> clausenv +val clenv_value_cast_meta : clausenv -> constr + +(* Compatibility, use res_pf ?with_evars:true instead *) +val e_res_pf : clausenv -> tactic diff --git a/proofs/decl_expr.mli b/proofs/decl_expr.mli index a8b7c0d6..22752eda 100644 --- a/proofs/decl_expr.mli +++ b/proofs/decl_expr.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: decl_expr.mli 10739 2008-04-01 14:45:20Z herbelin $ *) open Names open Util @@ -18,7 +18,6 @@ type 'it statement = type thesis_kind = Plain - | Sub of int | For of identifier type 'this or_thesis = diff --git a/proofs/decl_mode.ml b/proofs/decl_mode.ml index 8d8fb745..f8fc4e87 100644 --- a/proofs/decl_mode.ml +++ b/proofs/decl_mode.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(*i $Id: decl_mode.ml 10739 2008-04-01 14:45:20Z herbelin $ i*) open Names open Term @@ -41,16 +41,19 @@ let check_not_proof_mode str = error str type split_tree= - Push of (Idset.t * split_tree) - | Split of (Idset.t * inductive * (Idset.t * split_tree) option array) - | Pop of split_tree - | End_of_branch of (identifier * int) + Skip_patt of Idset.t * split_tree + | Split_patt of Idset.t * inductive * + (bool array * (Idset.t * split_tree) option) array + | Close_patt of split_tree + | End_patt of (identifier * int) type elim_kind = EK_dep of split_tree | EK_nodep | EK_unknown +type recpath = int option*Declarations.wf_paths + type per_info = {per_casee:constr; per_ctype:types; @@ -58,7 +61,8 @@ type per_info = per_pred:constr; per_args:constr list; per_params:constr list; - per_nparams:int} + per_nparams:int; + per_wf:recpath} type stack_info = Per of Decl_expr.elim_type * per_info * elim_kind * identifier list @@ -67,10 +71,7 @@ type stack_info = | Focus_claim type pm_info = - { pm_last: (Names.identifier * bool) option (* anonymous if none *); - pm_partial_goal : constr; (* partial goal construction *) - pm_subgoals : (metavariable*constr) list; - pm_stack : stack_info list} + { pm_stack : stack_info list} let pm_in,pm_out = Dyn.create "pm_info" @@ -118,3 +119,8 @@ let get_end_command pts = end | Mode_none -> error "no proof in progress" + +let get_last env = + try + let (id,_,_) = List.hd (Environ.named_context env) in id + with Invalid_argument _ -> error "no previous statement to use" diff --git a/proofs/decl_mode.mli b/proofs/decl_mode.mli index 81fab168..77bee313 100644 --- a/proofs/decl_mode.mli +++ b/proofs/decl_mode.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: decl_mode.mli 10739 2008-04-01 14:45:20Z herbelin $ *) open Names open Term @@ -29,16 +29,18 @@ val get_current_mode : unit -> command_mode val check_not_proof_mode : string -> unit type split_tree= - Push of (Idset.t * split_tree) - | Split of (Idset.t * inductive * (Idset.t*split_tree) option array) - | Pop of split_tree - | End_of_branch of (identifier * int) + Skip_patt of Idset.t * split_tree + | Split_patt of Idset.t * inductive * + (bool array * (Idset.t * split_tree) option) array + | Close_patt of split_tree + | End_patt of (identifier * int) type elim_kind = EK_dep of split_tree | EK_nodep | EK_unknown +type recpath = int option*Declarations.wf_paths type per_info = {per_casee:constr; @@ -47,7 +49,8 @@ type per_info = per_pred:constr; per_args:constr list; per_params:constr list; - per_nparams:int} + per_nparams:int; + per_wf:recpath} type stack_info = Per of Decl_expr.elim_type * per_info * elim_kind * Names.identifier list @@ -56,10 +59,7 @@ type stack_info = | Focus_claim type pm_info = - { pm_last: (Names.identifier * bool) option (* anonymous if none *); - pm_partial_goal : constr ; (* partial goal construction *) - pm_subgoals : (metavariable*constr) list; - pm_stack : stack_info list } + {pm_stack : stack_info list } val pm_in : pm_info -> Dyn.t @@ -70,3 +70,5 @@ val get_end_command : pftreestate -> string option val get_stack : pftreestate -> stack_info list val get_top_stack : pftreestate -> stack_info list + +val get_last: Environ.env -> identifier diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index 132fa2b9..99ab7ef1 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: evar_refiner.ml 9583 2007-02-01 19:35:03Z notin $ *) +(* $Id: evar_refiner.ml 11047 2008-06-03 23:08:00Z msozeau $ *) open Util open Names @@ -28,8 +28,8 @@ let w_refine ev rawc evd = let e_info = Evd.find (evars_of evd) ev in let env = Evd.evar_env e_info in let sigma,typed_c = - try Pretyping.Default.understand_tcc (evars_of evd) env - ~expected_type:e_info.evar_concl rawc + try Pretyping.Default.understand_tcc ~resolve_classes:false + (evars_of evd) env ~expected_type:e_info.evar_concl rawc with _ -> error ("The term is not well-typed in the environment of " ^ string_of_existential ev) in @@ -41,12 +41,16 @@ let instantiate_pf_com n com pfts = let gls = top_goal_of_pftreestate pfts in let sigma = gls.sigma in let (sp,evi) (* as evc *) = - try - List.nth (Evarutil.non_instantiated sigma) (n-1) - with Failure _ -> - error "not so many uninstantiated existential variables" in + let evl = Evarutil.non_instantiated sigma in + if (n <= 0) then + error "incorrect existential variable index" + else if List.length evl < n then + error "not so many uninstantiated existential variables" + else + List.nth evl (n-1) + in let env = Evd.evar_env evi in let rawc = Constrintern.intern_constr sigma env com in - let evd = create_evar_defs sigma in + let evd = create_goal_evar_defs sigma in let evd' = w_refine sp rawc evd in - change_constraints_pftreestate (evars_of evd') pfts + change_constraints_pftreestate (evars_of evd') pfts diff --git a/proofs/logic.ml b/proofs/logic.ml index 0846997e..6e78f134 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: logic.ml 9805 2007-04-28 21:28:37Z herbelin $ *) +(* $Id: logic.ml 10877 2008-04-30 21:58:41Z herbelin $ *) open Pp open Util @@ -32,8 +32,7 @@ type refiner_error = (* Errors raised by the refiner *) | BadType of constr * constr * constr - | OccurMeta of constr - | OccurMetaGoal of constr + | UnresolvedBindings of name list | CannotApply of constr * constr | NotWellTyped of constr | NonLinearProof of constr @@ -52,14 +51,15 @@ let rec catchable_exception = function | RefinerError _ | Indrec.RecursionSchemeError _ | Nametab.GlobalizationError _ | PretypeError (_,VarNotFound _) (* unification errors *) - | PretypeError(_,(CannotUnify _|CannotGeneralize _|NoOccurrenceFound _| - CannotUnifyBindingType _|NotClean _)) -> true + | PretypeError(_,(CannotUnify _|CannotUnifyLocal _|CannotGeneralize _ + |NoOccurrenceFound _|CannotUnifyBindingType _|NotClean _ + |CannotFindWellTypedAbstraction _)) -> true | _ -> false (* Tells if the refiner should check that the submitted rules do not produce invalid subgoals *) let check = ref false -let with_check = Options.with_option check +let with_check = Flags.with_option check (************************************************************************) (************************************************************************) @@ -69,10 +69,12 @@ let with_check = Options.with_option check (* The Clear tactic: it scans the context for hypotheses to be removed (instead of iterating on the list of identifier to be removed, which forces the user to give them in order). *) + let clear_hyps sigma ids gl = - let evd = ref (Evd.create_evar_defs sigma) in - let ngl = Evarutil.clear_hyps_in_evi evd gl ids in - (ngl, evars_of !evd) + let evdref = ref (Evd.create_goal_evar_defs sigma) in + let (hyps,concl) = + Evarutil.clear_hyps_in_evi evdref gl.evar_hyps gl.evar_concl ids in + (mk_goal hyps concl gl.evar_extra, evars_of !evdref) (* The ClearBody tactic *) @@ -264,8 +266,8 @@ let rec mk_refgoals sigma goal goalacc conclty trm = *) match kind_of_term trm with | Meta _ -> - if occur_meta conclty then - raise (RefinerError (OccurMetaGoal conclty)); + if !check && occur_meta conclty then + anomaly "refined called with a dependent meta"; (mk_goal hyps (nf_betaiota conclty))::goalacc, conclty | Cast (t,_, ty) -> @@ -276,8 +278,10 @@ let rec mk_refgoals sigma goal goalacc conclty trm = | App (f,l) -> let (acc',hdty) = match kind_of_term f with - | (Ind _ (* needed if defs in Type are polymorphic: | Const _*)) - when not (array_exists occur_meta l) (* we could be finer *) -> + | Ind _ | Const _ + when not (array_exists occur_meta l) (* we could be finer *) + & (isInd f or has_polymorphic_type (destConst f)) + -> (* Sort-polymorphism of definition and inductive types *) goalacc, type_of_global_reference_knowing_parameters env sigma f l @@ -300,7 +304,8 @@ let rec mk_refgoals sigma goal goalacc conclty trm = (acc'',conclty') | _ -> - if occur_meta trm then raise (RefinerError (OccurMeta trm)); + if occur_meta trm then + anomaly "refiner called with a meta in non app/case subterm"; let t'ty = goal_type_of env sigma trm in check_conv_leq_goal env sigma trm t'ty conclty; (goalacc,t'ty) @@ -340,7 +345,10 @@ and mk_hdgoals sigma goal goalacc trm = in (acc'',conclty') - | _ -> goalacc, goal_type_of env sigma trm + | _ -> + if !check && occur_meta trm then + anomaly "refined called with a dependent meta"; + goalacc, goal_type_of env sigma trm and mk_arggoals sigma goal goalacc funty = function | [] -> goalacc,funty @@ -378,7 +386,7 @@ let convert_hyp sign sigma (id,b,bt as d) = let env = Global.env_of_context sign in if !check && not (is_conv env sigma bt ct) then error ("Incorrect change of the type of "^(string_of_id id)); - if !check && not (option_compare (is_conv env sigma) b c) then + if !check && not (Option.Misc.compare (is_conv env sigma) b c) then error ("Incorrect change of the body of "^(string_of_id id)); d) diff --git a/proofs/logic.mli b/proofs/logic.mli index 2b6c6b4a..def02c8c 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: logic.mli 9573 2007-01-31 20:18:18Z notin $ i*) +(*i $Id: logic.mli 10785 2008-04-13 21:41:54Z herbelin $ i*) (*i*) open Names @@ -50,8 +50,7 @@ type refiner_error = (*i Errors raised by the refiner i*) | BadType of constr * constr * constr - | OccurMeta of constr - | OccurMetaGoal of constr + | UnresolvedBindings of name list | CannotApply of constr * constr | NotWellTyped of constr | NonLinearProof of constr diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 565c9547..6d8f09ea 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: pfedit.ml 9154 2006-09-20 17:18:18Z corbinea $ *) +(* $Id: pfedit.ml 10850 2008-04-25 18:07:44Z herbelin $ *) open Pp open Util @@ -33,6 +33,7 @@ open Safe_typing type proof_topstate = { mutable top_end_tac : tactic option; + top_init_tac : tactic option; top_goal : goal; top_strength : Decl_kinds.goal_kind; top_hook : declaration_hook } @@ -118,8 +119,6 @@ let delete_proof (loc,id) = user_err_loc (loc,"Pfedit.delete_proof",str"No such proof" ++ msg_proofs false) -let init_proofs () = Edit.clear proof_edits - let mutate f = try Edit.mutate proof_edits (fun _ pfs -> f pfs) @@ -128,7 +127,8 @@ let mutate f = (str"No focused proof" ++ msg_proofs true) let start (na,ts) = - let pfs = mk_pftreestate ts.top_goal in + let pfs = mk_pftreestate ts.top_goal in + let pfs = Option.fold_right solve_pftreestate ts.top_init_tac pfs in add_proof(na,pfs,ts) let restart_proof () = @@ -204,13 +204,14 @@ let current_proof_depth() = let xml_cook_proof = ref (fun _ -> ()) let set_xml_cook_proof f = xml_cook_proof := f -let cook_proof () = +let cook_proof k = let (pfs,ts) = get_state() and ident = get_current_proof_name () in let {evar_concl=concl} = ts.top_goal and strength = ts.top_strength in let pfterm = extract_pftreestate pfs in !xml_cook_proof (strength,pfs); + k pfs; (ident, ({ const_entry_body = pfterm; const_entry_type = Some concl; @@ -237,7 +238,7 @@ let check_no_pending_proofs () = let delete_current_proof () = delete_proof_gen (get_current_proof_name ()) -let delete_all_proofs = init_proofs +let delete_all_proofs () = Edit.clear proof_edits (*********************************************************************) (* Modifying the end tactic of the current profftree *) @@ -250,10 +251,11 @@ let set_end_tac tac = (* Modifying the current prooftree *) (*********************************************************************) -let start_proof na str sign concl hook = +let start_proof na str sign concl ?init_tac hook = let top_goal = mk_goal sign concl None in let ts = { top_end_tac = None; + top_init_tac = init_tac; top_goal = top_goal; top_strength = str; top_hook = hook} diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 8c0c7f55..42c24081 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: pfedit.mli 9154 2006-09-20 17:18:18Z corbinea $ i*) +(*i $Id: pfedit.mli 10850 2008-04-25 18:07:44Z herbelin $ i*) (*i*) open Util @@ -71,13 +71,16 @@ val current_proof_depth: unit -> int val set_undo : int option -> unit val get_undo : unit -> int option -(*s [start_proof s str env t hook] starts a proof of name [s] and conclusion - [t]; [hook] is optionally a function to be applied at proof end (e.g. to - declare the built constructions as a coercion or a setoid morphism) *) +(*s [start_proof s str env t hook tac] starts a proof of name [s] and + conclusion [t]; [hook] is optionally a function to be applied at + proof end (e.g. to declare the built constructions as a coercion + or a setoid morphism); init_tac is possibly a tactic to + systematically apply at initialization time (e.g. to start the + proof of mutually dependent theorems) *) val start_proof : - identifier -> goal_kind -> named_context_val -> constr - -> declaration_hook -> unit + identifier -> goal_kind -> named_context_val -> constr -> + ?init_tac:tactic -> declaration_hook -> unit (* [restart_proof ()] restarts the current focused proof from the beginning or fails if no proof is focused *) @@ -103,7 +106,7 @@ val suspend_proof : unit -> unit a constant with its name, kind and possible hook (see [start_proof]); it fails if there is no current proof of if it is not completed *) -val cook_proof : unit -> +val cook_proof : (Refiner.pftreestate -> unit) -> identifier * (Entries.definition_entry * goal_kind * declaration_hook) (* To export completed proofs to xml *) diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml index 9d70d012..99a1e506 100644 --- a/proofs/proof_trees.ml +++ b/proofs/proof_trees.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: proof_trees.ml 9154 2006-09-20 17:18:18Z corbinea $ *) +(* $Id: proof_trees.ml 10124 2007-09-17 18:40:21Z herbelin $ *) open Closure open Util @@ -35,6 +35,7 @@ let is_bind = function let mk_goal hyps cl extra = { evar_hyps = hyps; evar_concl = cl; + evar_filter = List.map (fun _ -> true) (named_context_of_val hyps); evar_body = Evar_empty; evar_extra = extra } (* Functions on proof trees *) diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index 6f8b0686..dbe40780 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: proof_type.ml 9573 2007-01-31 20:18:18Z notin $ *) +(*i $Id: proof_type.ml 9842 2007-05-20 17:44:23Z herbelin $ *) (*i*) open Environ @@ -63,7 +63,7 @@ and tactic = goal sigma -> (goal list sigma * validation) and validation = (proof_tree list -> proof_tree) and tactic_expr = - (constr, + (open_constr, constr_pattern, evaluable_global_reference, inductive, @@ -73,7 +73,7 @@ and tactic_expr = Tacexpr.gen_tactic_expr and atomic_tactic_expr = - (constr, + (open_constr, constr_pattern, evaluable_global_reference, inductive, @@ -83,7 +83,7 @@ and atomic_tactic_expr = Tacexpr.gen_atomic_tactic_expr and tactic_arg = - (constr, + (open_constr, constr_pattern, evaluable_global_reference, inductive, diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index 26d9eb2e..4fbcda4c 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: proof_type.mli 9573 2007-01-31 20:18:18Z notin $ i*) +(*i $Id: proof_type.mli 9842 2007-05-20 17:44:23Z herbelin $ i*) (*i*) open Environ @@ -98,7 +98,7 @@ and tactic = goal sigma -> (goal list sigma * validation) and validation = (proof_tree list -> proof_tree) and tactic_expr = - (constr, + (open_constr, constr_pattern, evaluable_global_reference, inductive, @@ -108,7 +108,7 @@ and tactic_expr = Tacexpr.gen_tactic_expr and atomic_tactic_expr = - (constr, + (open_constr, constr_pattern, evaluable_global_reference, inductive, @@ -118,7 +118,7 @@ and atomic_tactic_expr = Tacexpr.gen_atomic_tactic_expr and tactic_arg = - (constr, + (open_constr, constr_pattern, evaluable_global_reference, inductive, diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index ad277caa..072a38b6 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: redexpr.ml 9058 2006-07-22 17:42:45Z bgregoir $ *) +(* $Id: redexpr.ml 11094 2008-06-10 19:35:23Z herbelin $ *) open Pp open Util @@ -19,7 +19,7 @@ open Reductionops open Tacred open Closure open RedFlags - +open Libobject (* call by value normalisation function using the virtual machine *) let cbv_vm env _ c = @@ -27,22 +27,79 @@ let cbv_vm env _ c = Vnorm.cbv_vm env c ctyp -let set_opaque_const sp = - Conv_oracle.set_opaque_const sp; - Csymtable.set_opaque_const sp - -let set_transparent_const sp = - let cb = Global.lookup_constant sp in - if cb.const_body <> None & cb.const_opaque then - errorlabstrm "set_transparent_const" - (str "Cannot make" ++ spc () ++ - Nametab.pr_global_env Idset.empty (ConstRef sp) ++ - spc () ++ str "transparent because it was declared opaque."); - Conv_oracle.set_transparent_const sp; - Csymtable.set_transparent_const sp - -let set_opaque_var = Conv_oracle.set_opaque_var -let set_transparent_var = Conv_oracle.set_transparent_var +let set_strategy_one ref l = + let k = + match ref with + | EvalConstRef sp -> ConstKey sp + | EvalVarRef id -> VarKey id in + Conv_oracle.set_strategy k l; + match k,l with + ConstKey sp, Conv_oracle.Opaque -> + Csymtable.set_opaque_const sp + | ConstKey sp, _ -> + let cb = Global.lookup_constant sp in + if cb.const_body <> None & cb.const_opaque then + errorlabstrm "set_transparent_const" + (str "Cannot make" ++ spc () ++ + Nametab.pr_global_env Idset.empty (ConstRef sp) ++ + spc () ++ str "transparent because it was declared opaque."); + Csymtable.set_transparent_const sp + | _ -> () + +let cache_strategy str = + List.iter + (fun (lev,ql) -> List.iter (fun q -> set_strategy_one q lev) ql) + str + +let subst_strategy (_,subs,obj) = + list_smartmap + (fun (k,ql as entry) -> + let ql' = list_smartmap (Mod_subst.subst_evaluable_reference subs) ql in + if ql==ql' then entry else (k,ql')) + obj + + +let map_strategy f l = + let l' = List.fold_right + (fun (lev,ql) str -> + let ql' = List.fold_right + (fun q ql -> + match f q with + Some q' -> q' :: ql + | None -> ql) ql [] in + if ql'=[] then str else (lev,ql')::str) l [] in + if l'=[] then None else Some l' + +let export_strategy obj = + map_strategy (function + EvalVarRef _ -> None + | EvalConstRef _ as q -> Some q) obj + +let classify_strategy (_,obj) = Substitute obj + +let disch_ref ref = + match ref with + EvalConstRef c -> + let c' = Lib.discharge_con c in + if c==c' then Some ref else Some (EvalConstRef c') + | _ -> Some ref + +let discharge_strategy (_,obj) = + map_strategy disch_ref obj + +let (inStrategy,outStrategy) = + declare_object {(default_object "STRATEGY") with + cache_function = (fun (_,obj) -> cache_strategy obj); + load_function = (fun _ (_,obj) -> cache_strategy obj); + subst_function = subst_strategy; + discharge_function = discharge_strategy; + classify_function = classify_strategy; + export_function = export_strategy } + + +let set_strategy local str = + if local then cache_strategy str + else Lib.add_anonymous_leaf (inStrategy str) let _ = Summary.declare_summary "Transparent constants and variables" @@ -70,7 +127,7 @@ let make_flag f = let red = if f.rDelta then (* All but rConst *) let red = red_add red fDELTA in - let red = red_add_transparent red (Conv_oracle.freeze ()) in + let red = red_add_transparent red (Conv_oracle.get_transp_state()) in List.fold_right (fun v red -> red_sub red (make_flag_constant v)) f.rConst red @@ -97,8 +154,8 @@ let out_arg = function | ArgVar _ -> anomaly "Unevaluated or_var variable" | ArgArg x -> x -let out_with_occurrences (l,c) = - (List.map out_arg l, c) +let out_with_occurrences ((b,l),c) = + ((b,List.map out_arg l), c) let reduction_of_red_expr = function | Red internal -> @@ -106,8 +163,8 @@ let reduction_of_red_expr = function else (red_product,DEFAULTcast) | Hnf -> (hnf_constr,DEFAULTcast) | Simpl (Some (_,c as lp)) -> - (contextually (is_reference c) (out_with_occurrences lp) nf,DEFAULTcast) - | Simpl None -> (nf,DEFAULTcast) + (contextually (is_reference c) (out_with_occurrences lp) simpl,DEFAULTcast) + | Simpl None -> (simpl,DEFAULTcast) | Cbv f -> (cbv_norm_flags (make_flag f),DEFAULTcast) | Lazy f -> (clos_norm_flags (make_flag f),DEFAULTcast) | Unfold ubinds -> (unfoldn (List.map out_with_occurrences ubinds),DEFAULTcast) diff --git a/proofs/redexpr.mli b/proofs/redexpr.mli index cbac180a..d72ff182 100644 --- a/proofs/redexpr.mli +++ b/proofs/redexpr.mli @@ -6,18 +6,19 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: redexpr.mli 8878 2006-05-30 16:44:25Z herbelin $ i*) +(*i $Id: redexpr.mli 11094 2008-06-10 19:35:23Z herbelin $ i*) open Names open Term open Closure open Rawterm open Reductionops +open Termops type red_expr = (constr, evaluable_global_reference) red_expr_gen -val out_with_occurrences : 'a with_occurrences -> int list * 'a +val out_with_occurrences : 'a with_occurrences -> occurrences * 'a val reduction_of_red_expr : red_expr -> reduction_function * cast_kind (* [true] if we should use the vm to verify the reduction *) @@ -25,13 +26,12 @@ val reduction_of_red_expr : red_expr -> reduction_function * cast_kind val declare_red_expr : string -> reduction_function -> unit (* Opaque and Transparent commands. *) -val set_opaque_const : constant -> unit -val set_transparent_const : constant -> unit - -val set_opaque_var : identifier -> unit -val set_transparent_var : identifier -> unit - +(* Sets the expansion strategy of a constant. When the boolean is + true, the effect is non-synchronous (i.e. it does not survive + section and module closure). *) +val set_strategy : + bool -> (Conv_oracle.level * evaluable_global_reference list) list -> unit (* call by value normalisation function using the virtual machine *) val cbv_vm : reduction_function diff --git a/proofs/refiner.ml b/proofs/refiner.ml index a1d7e011..172a7d70 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: refiner.ml 9573 2007-01-31 20:18:18Z notin $ *) +(* $Id: refiner.ml 11021 2008-05-29 16:48:18Z barras $ *) open Pp open Util @@ -108,13 +108,23 @@ let rec frontier p = open_subgoals = and_status (List.map pf_status pfl'); ref = Some(r,pfl')})) +(* TODO LEM: I might have to make sure that these hooks are called + only when called from solve_nth_pftreestate; I can build the hook + call into the "f", then. + *) +let solve_hook = ref ignore +let set_solve_hook = (:=) solve_hook let rec frontier_map_rec f n p = if n < 1 || n > p.open_subgoals then p else match p.ref with | None -> let p' = f p in - if Evd.eq_evar_info p'.goal p.goal then p' + if Evd.eq_evar_info p'.goal p.goal then + begin + !solve_hook p'; + p' + end else errorlabstrm "Refiner.frontier_map" (str"frontier_map was handed back a ill-formed proof.") @@ -140,7 +150,11 @@ let rec frontier_mapi_rec f i p = match p.ref with | None -> let p' = f i p in - if Evd.eq_evar_info p'.goal p.goal then p' + if Evd.eq_evar_info p'.goal p.goal then + begin + !solve_hook p'; + p' + end else errorlabstrm "Refiner.frontier_mapi" (str"frontier_mapi was handed back a ill-formed proof.") @@ -223,9 +237,7 @@ let refiner = function ref = Some(Daimon,[])}) -let local_Constraints gl = refiner (Prim Change_evars) gl - -let norm_evar_tac = local_Constraints +let norm_evar_tac gl = refiner (Prim Change_evars) gl let norm_evar_proof sigma pf = let nf_subgoal i sgl = @@ -312,6 +324,9 @@ let idtac_valid = function (* [goal_goal_list : goal sigma -> goal list sigma] *) let goal_goal_list gls = {it=[gls.it];sigma=gls.sigma} +(* forces propagation of evar constraints *) +let tclNORMEVAR = norm_evar_tac + (* identity tactic without any message *) let tclIDTAC gls = (goal_goal_list gls, idtac_valid) @@ -334,29 +349,25 @@ let start_tac gls = let finish_tac (sigr,gl,p) = (repackage sigr gl, p) -(* Apply [taci.(i)] on the first n-th subgoals and [tac] on the others *) -let thensf_tac taci tac (sigr,gs,p) = - let n = Array.length taci in - let nsg = List.length gs in - if nsg apply_sig_tac sigr (if i + apply_sig_tac sigr (if i=ng-nl then tacli.(nl-ng+i) else tac)) 0 gs) in (sigr, List.flatten gll, compose p (mapshape (List.map List.length gll) pl)) -(* Apply [taci.(i)] on the last n-th subgoals and [tac] on the others *) -let thensl_tac tac taci (sigr,gs,p) = - let n = Array.length taci in - let nsg = List.length gs in - if nsg apply_sig_tac sigr (if i<0 then tac else taci.(i))) - (n-nsg) gs) in - (sigr, List.flatten gll, - compose p (mapshape (List.map List.length gll) pl)) +(* Apply [taci.(i)] on the first n subgoals and [tac] on the others *) +let thensf_tac taci tac = thens3parts_tac taci tac [||] + +(* Apply [taci.(i)] on the last n subgoals and [tac] on the others *) +let thensl_tac tac taci = thens3parts_tac [||] tac taci (* Apply [tac i] on the ith subgoal (no subgoals number check) *) let thensi_tac tac (sigr,gs,p) = @@ -382,19 +393,25 @@ let theni_tac i tac ((_,gl,_) as subgoals) = subgoals else non_existent_goal k +(* [tclTHENS3PARTS tac1 [|t1 ; ... ; tn|] tac2 [|t'1 ; ... ; t'm|] gls] + applies the tactic [tac1] to [gls] then, applies [t1], ..., [tn] to + the first [n] resulting subgoals, [t'1], ..., [t'm] to the last [m] + subgoals and [tac2] to the rest of the subgoals in the middle. Raises an + error if the number of resulting subgoals is strictly less than [n+m] *) +let tclTHENS3PARTS tac1 tacfi tac tacli gls = + finish_tac (thens3parts_tac tacfi tac tacli (then_tac tac1 (start_tac gls))) + (* [tclTHENSFIRSTn tac1 [|t1 ; ... ; tn|] tac2 gls] applies the tactic [tac1] - to [gls] and applies [t1], ..., [tn] to the [n] first resulting + to [gls] and applies [t1], ..., [tn] to the first [n] resulting subgoals, and [tac2] to the others subgoals. Raises an error if the number of resulting subgoals is strictly less than [n] *) -let tclTHENSFIRSTn tac1 taci tac gls = - finish_tac (thensf_tac taci tac (then_tac tac1 (start_tac gls))) +let tclTHENSFIRSTn tac1 taci tac = tclTHENS3PARTS tac1 taci tac [||] (* [tclTHENSLASTn tac1 tac2 [|t1 ;...; tn|] gls] applies the tactic [tac1] - to [gls] and applies [t1], ..., [tn] to the [n] last resulting + to [gls] and applies [t1], ..., [tn] to the last [n] resulting subgoals, and [tac2] to the other subgoals. Raises an error if the number of resulting subgoals is strictly less than [n] *) -let tclTHENSLASTn tac1 tac taci gls = - finish_tac (thensl_tac tac taci (then_tac tac1 (start_tac gls))) +let tclTHENSLASTn tac1 tac taci = tclTHENS3PARTS tac1 [||] tac taci (* [tclTHEN_i tac taci gls] applies the tactic [tac] to [gls] and applies [(taci i)] to the i_th resulting subgoal (starting from 1), whatever the @@ -407,13 +424,13 @@ let tclTHENFIRSTn tac1 taci = tclTHENSFIRSTn tac1 taci tclIDTAC (* [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies [tac2] to every resulting subgoals *) -let tclTHEN tac1 tac2 = tclTHENSFIRSTn tac1 [||] tac2 +let tclTHEN tac1 tac2 = tclTHENS3PARTS tac1 [||] tac2 [||] (* [tclTHENSV tac1 [t1 ; ... ; tn] gls] applies the tactic [tac1] to [gls] and applies [t1],..., [tn] to the [n] resulting subgoals. Raises an error if the number of resulting subgoals is not [n] *) let tclTHENSV tac1 tac2v = - tclTHENSFIRSTn tac1 tac2v (tclFAIL_s "Wrong number of tactics.") + tclTHENS3PARTS tac1 tac2v (tclFAIL_s "Wrong number of tactics.") [||] let tclTHENS tac1 tac2l = tclTHENSV tac1 (Array.of_list tac2l) @@ -425,7 +442,6 @@ let tclTHENLAST tac1 tac2 = tclTHENSLASTn tac1 tclIDTAC [|tac2|] to the first resulting subgoal *) let tclTHENFIRST tac1 tac2 = tclTHENSFIRSTn tac1 [|tac2|] tclIDTAC - (* [tclTHENLIST [t1;..;tn]] applies [t1] then [t2] ... then [tn]. More convenient than [tclTHEN] when [n] is large. *) let rec tclTHENLIST = function @@ -437,18 +453,17 @@ let rec tclTHENLIST = function (* various progress criterions *) let same_goal gl subgoal = - eq_named_context_val (hypotheses subgoal) (hypotheses gl) && - eq_constr (conclusion subgoal) (conclusion gl) + eq_constr (conclusion subgoal) (conclusion gl) && + eq_named_context_val (hypotheses subgoal) (hypotheses gl) let weak_progress gls ptree = - (List.length gls.it <> 1) or + (List.length gls.it <> 1) || (not (same_goal (List.hd gls.it) ptree.it)) -(* Il y avait ici un ts_eq ........ *) let progress gls ptree = - (weak_progress gls ptree) or - (not (ptree.sigma == gls.sigma)) + (not (ptree.sigma == gls.sigma)) || + (weak_progress gls ptree) (* PROGRESS tac ptree applies tac to the goal ptree and fails if tac leaves @@ -476,24 +491,39 @@ let tclNOTSAMEGOAL (tac : tactic) goal = (str"Tactic generated a subgoal identical to the original goal.") else rslt - +let catch_failerror = function + | e when catchable_exception e -> check_for_interrupt () + | FailError (0,_) | Stdpp.Exc_located(_, FailError (0,_)) -> + check_for_interrupt () + | FailError (lvl,s) -> raise (FailError (lvl - 1, s)) + | Stdpp.Exc_located (s,FailError (lvl,s')) -> + raise (Stdpp.Exc_located (s,FailError (lvl - 1, s'))) + | e -> raise e (* ORELSE0 t1 t2 tries to apply t1 and if it fails, applies t2 *) let tclORELSE0 t1 t2 g = try t1 g with (* Breakpoint *) - | e when catchable_exception e -> check_for_interrupt (); t2 g - | FailError (0,_) | Stdpp.Exc_located(_, FailError (0,_)) -> - check_for_interrupt (); t2 g - | FailError (lvl,s) -> raise (FailError (lvl - 1, s)) - | Stdpp.Exc_located (s,FailError (lvl,s')) -> - raise (Stdpp.Exc_located (s,FailError (lvl - 1, s'))) + | e -> catch_failerror e; t2 g (* ORELSE t1 t2 tries to apply t1 and if it fails or does not progress, then applies t2 *) let tclORELSE t1 t2 = tclORELSE0 (tclPROGRESS t1) t2 +(* applies t1;t2then if t1 succeeds or t2else if t1 fails + t2* are called in terminal position (unless t1 produces more than + 1 subgoal!) *) +let tclORELSE_THEN t1 t2then t2else gls = + match + try Some(tclPROGRESS t1 gls) + with e -> catch_failerror e; None + with + | None -> t2else gls + | Some (sgl,v) -> + let (sigr,gl) = unpackage sgl in + finish_tac (then_tac t2then (sigr,gl,v)) + (* TRY f tries to apply f, and if it fails, leave the goal unchanged *) let tclTRY f = (tclORELSE0 f tclIDTAC) @@ -558,9 +588,10 @@ let tclDO n t = in dorec n + (* Beware: call by need of CAML, g is needed *) let rec tclREPEAT t g = - (tclORELSE (tclTHEN t (tclREPEAT t)) tclIDTAC) g + tclORELSE_THEN t (tclREPEAT t) tclIDTAC g let tclAT_LEAST_ONCE t = (tclTHEN t (tclREPEAT t)) @@ -847,6 +878,7 @@ let prev_unproven pts = let rec top_of_tree pts = if is_top_pftreestate pts then pts else top_of_tree(traverse 0 pts) +(* FIXME: cette fonction n'est (as of October 2007) appelée nulle part *) let change_rule f pts = let mark_top _ pt = match pt.ref with diff --git a/proofs/refiner.mli b/proofs/refiner.mli index d8b13dba..95130ac5 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: refiner.mli 9244 2006-10-16 17:11:44Z barras $ i*) +(*i $Id: refiner.mli 10879 2008-05-01 22:14:20Z msozeau $ i*) (*i*) open Term @@ -28,7 +28,7 @@ val pf_hyps : goal sigma -> named_context val unpackage : 'a sigma -> evar_map ref * 'a val repackage : evar_map ref -> 'a -> 'a sigma val apply_sig_tac : - evar_map ref -> ('a sigma -> 'b sigma * 'c) -> 'a -> 'b * 'c + evar_map ref -> (goal sigma -> (goal list) sigma * validation) -> goal -> (goal list) * validation type transformation_tactic = proof_tree -> (goal list * validation) @@ -40,15 +40,16 @@ val abstract_operation : compound_rule -> tactic -> tactic val abstract_tactic : ?dflt:bool -> atomic_tactic_expr -> tactic -> tactic val abstract_tactic_expr : ?dflt:bool -> tactic_expr -> tactic -> tactic val abstract_extended_tactic : - ?dflt:bool -> string -> closed_generic_argument list -> tactic -> tactic + ?dflt:bool -> string -> typed_generic_argument list -> tactic -> tactic val refiner : rule -> tactic val frontier : transformation_tactic val list_pf : proof_tree -> goal list val unTAC : tactic -> goal sigma -> proof_tree sigma -val local_Constraints : tactic +(* Install a hook frontier_map and frontier_mapi call on the new node they create *) +val set_solve_hook : (Proof_type.proof_tree -> unit) -> unit (* [frontier_map f n p] applies f on the n-th open subgoal of p and rebuilds proof-tree. n=1 for first goal, n negative counts from the right *) @@ -61,6 +62,9 @@ val frontier_mapi : (*s Tacticals. *) +(* [tclNORMEVAR] forces propagation of evar constraints *) +val tclNORMEVAR : tactic + (* [tclIDTAC] is the identity tactic without message printing*) val tclIDTAC : tactic val tclIDTAC_MESSAGE : Pp.std_ppcmds -> tactic @@ -100,6 +104,13 @@ val tclTHENS : tactic -> tactic list -> tactic val tclTHENST : tactic -> tactic array -> tactic -> tactic *) +(* [tclTHENS3PARTS tac1 [|t1 ; ... ; tn|] tac2 [|t'1 ; ... ; t'm|] gls] + applies the tactic [tac1] to [gls] then, applies [t1], ..., [tn] to + the first [n] resulting subgoals, [t'1], ..., [t'm] to the last [m] + subgoals and [tac2] to the rest of the subgoals in the middle. Raises an + error if the number of resulting subgoals is strictly less than [n+m] *) +val tclTHENS3PARTS : tactic -> tactic array -> tactic -> tactic array -> tactic + (* [tclTHENSLASTn tac1 [t1 ; ... ; tn] tac2 gls] applies [t1],...,[tn] on the last [n] resulting subgoals and [tac2] on the remaining first subgoals *) val tclTHENSLASTn : tactic -> tactic -> tactic array -> tactic @@ -122,6 +133,10 @@ val tclTHENFIRSTn : tactic -> tactic array -> tactic (* A special exception for levels for the Fail tactic *) exception FailError of int * Pp.std_ppcmds +(* Takes an exception and either raise it at the next + level or do nothing. *) +val catch_failerror : exn -> unit + val tclORELSE : tactic -> tactic -> tactic val tclREPEAT : tactic -> tactic val tclREPEAT_MAIN : tactic -> tactic @@ -189,6 +204,7 @@ val solve_pftreestate : tactic -> pftreestate -> pftreestate val weak_undo_pftreestate : pftreestate -> pftreestate val mk_pftreestate : goal -> pftreestate +val extract_open_proof : evar_map -> proof_tree -> constr * (int * types) list val extract_open_pftreestate : pftreestate -> constr * Termops.metamap val extract_pftreestate : pftreestate -> constr val first_unproven : pftreestate -> pftreestate diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml index 0bcc7d16..d0789980 100644 --- a/proofs/tacexpr.ml +++ b/proofs/tacexpr.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: tacexpr.ml 9551 2007-01-29 15:13:35Z bgregoir $ i*) +(*i $Id: tacexpr.ml 11100 2008-06-11 11:10:31Z herbelin $ i*) open Names open Topconstr @@ -16,18 +16,25 @@ open Rawterm open Util open Genarg open Pattern +open Decl_kinds type 'a or_metaid = AI of 'a | MetaId of loc * string type direction_flag = bool (* true = Left-to-right false = right-to-right *) type lazy_flag = bool (* true = lazy false = eager *) +type evars_flag = bool (* true = pose evars false = fail on evars *) +type rec_flag = bool (* true = recursive false = not recursive *) +type advanced_flag = bool (* true = advanced false = basic *) +type split_flag = bool (* true = exists false = split *) +type hidden_flag = bool (* true = internal use false = user-level *) +type letin_flag = bool (* true = use local def false = use Leibniz *) type raw_red_flag = | FBeta | FIota | FZeta - | FConst of reference list - | FDeltaBut of reference list + | FConst of reference or_by_notation list + | FDeltaBut of reference or_by_notation list let make_red_flag = let rec add_flag red = function @@ -87,15 +94,23 @@ type 'id gsimple_clause = ('id raw_hyp_location) option [Some l] means on hypothesis belonging to l *) type 'id gclause = { onhyps : 'id raw_hyp_location list option; - onconcl : bool; - concl_occs : int or_var list } + concl_occs : bool * int or_var list } -let nowhere = {onhyps=Some[]; onconcl=false; concl_occs=[]} +let nowhere = {onhyps=Some[]; concl_occs=no_occurrences_expr} let simple_clause_of = function - { onhyps = Some[scl]; onconcl = false } -> Some scl - | { onhyps = Some []; onconcl = true; concl_occs=[] } -> None - | _ -> error "not a simple clause (one hypothesis or conclusion)" +| { onhyps = Some [scl]; concl_occs = occs } when occs = no_occurrences_expr -> + Some scl +| { onhyps = Some []; concl_occs = occs } when occs = all_occurrences_expr -> + None +| _ -> + error "not a simple clause (one hypothesis or conclusion)" + +type multi = + | Precisely of int + | UpTo of int + | RepeatStar + | RepeatPlus type pattern_expr = constr_expr @@ -122,29 +137,30 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr = | TacExact of 'constr | TacExactNoCheck of 'constr | TacVmCastNoCheck of 'constr - | TacApply of 'constr with_bindings - | TacElim of 'constr with_bindings * 'constr with_bindings option + | TacApply of advanced_flag * evars_flag * 'constr with_bindings + | TacElim of evars_flag * 'constr with_bindings * + 'constr with_bindings option | TacElimType of 'constr - | TacCase of 'constr with_bindings + | TacCase of evars_flag * 'constr with_bindings | TacCaseType of 'constr | TacFix of identifier option * int - | TacMutualFix of identifier * int * (identifier * int * 'constr) list + | TacMutualFix of hidden_flag * identifier * int * (identifier * int * + 'constr) list | TacCofix of identifier option - | TacMutualCofix of identifier * (identifier * 'constr) list + | TacMutualCofix of hidden_flag * identifier * (identifier * 'constr) list | TacCut of 'constr | TacAssert of 'tac option * intro_pattern_expr * 'constr - | TacGeneralize of 'constr list + | TacGeneralize of ('constr with_occurrences * name) list | TacGeneralizeDep of 'constr - | TacLetTac of name * 'constr * 'id gclause -(* | TacInstantiate of int * 'constr * (('id * hyp_location_flag,unit) location) *) + | TacLetTac of name * 'constr * 'id gclause * letin_flag (* Derived basic tactics *) | TacSimpleInduction of quantified_hypothesis - | TacNewInduction of 'constr induction_arg list * 'constr with_bindings option - * intro_pattern_expr + | TacNewInduction of evars_flag * 'constr with_bindings induction_arg list * + 'constr with_bindings option * intro_pattern_expr * 'id gclause option | TacSimpleDestruct of quantified_hypothesis - | TacNewDestruct of 'constr induction_arg list * 'constr with_bindings option - * intro_pattern_expr + | TacNewDestruct of evars_flag * 'constr with_bindings induction_arg list * + 'constr with_bindings option * intro_pattern_expr * 'id gclause option | TacDoubleInduction of quantified_hypothesis * quantified_hypothesis | TacDecomposeAnd of 'constr @@ -160,20 +176,21 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr = | TacDestructHyp of (bool * identifier located) | TacDestructConcl | TacSuperAuto of (int option * reference list * bool * bool) - | TacDAuto of int or_var option * int option + | TacDAuto of int or_var option * int option * 'constr list (* Context management *) | TacClear of bool * 'id list | TacClearBody of 'id list | TacMove of bool * 'id * 'id - | TacRename of 'id * 'id + | TacRename of ('id *'id) list + | TacRevert of 'id list (* Constructors *) - | TacLeft of 'constr bindings - | TacRight of 'constr bindings - | TacSplit of bool * 'constr bindings - | TacAnyConstructor of 'tac option - | TacConstructor of int or_metaid * 'constr bindings + | TacLeft of evars_flag * 'constr bindings + | TacRight of evars_flag * 'constr bindings + | TacSplit of evars_flag * split_flag * 'constr bindings + | TacAnyConstructor of evars_flag * 'tac option + | TacConstructor of evars_flag * int or_metaid * 'constr bindings (* Conversion *) | TacReduce of ('constr,'cst) red_expr_gen * 'id gclause @@ -185,21 +202,26 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr = | TacTransitivity of 'constr (* Equality and inversion *) - | TacRewrite of bool * 'constr with_bindings * 'id gclause + | TacRewrite of + evars_flag * (bool * multi * 'constr with_bindings) list * 'id gclause * 'tac option | TacInversion of ('constr,'id) inversion_strength * quantified_hypothesis (* For ML extensions *) - | TacExtend of loc * string * ('constr,'tac) generic_argument list + | TacExtend of loc * string * 'constr generic_argument list (* For syntax extensions *) | TacAlias of loc * string * - (identifier * ('constr,'tac) generic_argument) list + (identifier * 'constr generic_argument) list * (dir_path * glob_tactic_expr) and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr = | TacAtom of loc * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr - | TacThen of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr - | TacThens of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr list + | TacThen of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr * + ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr array * + ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr * + ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr array + | TacThens of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr * + ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr list | TacFirst of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr list | TacComplete of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr | TacSolve of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr list @@ -212,8 +234,7 @@ and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr = | TacId of 'id message_token list | TacFail of int or_var * 'id message_token list | TacInfo of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr - | TacLetRecIn of (identifier located * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_fun_ast) list * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr - | TacLetIn of (identifier located * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr option * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg) list * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr + | TacLetIn of rec_flag * (identifier located * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg) list * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr | TacMatch of lazy_flag * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr * ('pat,('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr) match_rule list | TacMatchContext of lazy_flag * direction_flag * ('pat,('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr) match_rule list | TacFun of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_fun_ast @@ -222,11 +243,11 @@ and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr = and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_fun_ast = identifier option list * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr - (* These are possible arguments of a tactic definition *) + (* These are the possible arguments of a tactic definition *) and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg = | TacDynamic of loc * Dyn.t | TacVoid - | MetaIdArg of loc * string + | MetaIdArg of loc * bool * string | ConstrMayEval of ('constr,'cst) may_eval | IntroPattern of intro_pattern_expr | Reference of 'ref @@ -251,8 +272,8 @@ and glob_tactic_expr = type raw_tactic_expr = (constr_expr, pattern_expr, - reference, - reference, + reference or_by_notation, + reference or_by_notation, reference, identifier located or_metaid, raw_tactic_expr) gen_tactic_expr @@ -260,8 +281,8 @@ type raw_tactic_expr = type raw_atomic_tactic_expr = (constr_expr, (* constr *) pattern_expr, (* pattern *) - reference, (* evaluable reference *) - reference, (* inductive *) + reference or_by_notation, (* evaluable reference *) + reference or_by_notation, (* inductive *) reference, (* ltac reference *) identifier located or_metaid, (* identifier *) raw_tactic_expr) gen_atomic_tactic_expr @@ -269,16 +290,15 @@ type raw_atomic_tactic_expr = type raw_tactic_arg = (constr_expr, pattern_expr, - reference, - reference, + reference or_by_notation, + reference or_by_notation, reference, identifier located or_metaid, raw_tactic_expr) gen_tactic_arg -type raw_generic_argument = - (constr_expr,raw_tactic_expr) generic_argument +type raw_generic_argument = constr_expr generic_argument -type raw_red_expr = (constr_expr, reference) red_expr_gen +type raw_red_expr = (constr_expr, reference or_by_notation) red_expr_gen type glob_atomic_tactic_expr = (rawconstr_and_expr, @@ -298,28 +318,17 @@ type glob_tactic_arg = identifier located, glob_tactic_expr) gen_tactic_arg -type glob_generic_argument = - (rawconstr_and_expr,glob_tactic_expr) generic_argument +type glob_generic_argument = rawconstr_and_expr generic_argument type glob_red_expr = (rawconstr_and_expr, evaluable_global_reference or_var) red_expr_gen -type closed_raw_generic_argument = - (constr_expr,raw_tactic_expr) generic_argument - -type 'a raw_abstract_argument_type = - ('a,rlevel,raw_tactic_expr) abstract_argument_type - -type 'a glob_abstract_argument_type = - ('a,glevel,glob_tactic_expr) abstract_argument_type +type typed_generic_argument = Evd.open_constr generic_argument -type open_generic_argument = - (Term.constr,glob_tactic_expr) generic_argument +type 'a raw_abstract_argument_type = ('a,rlevel) abstract_argument_type -type closed_generic_argument = - (Term.constr,glob_tactic_expr) generic_argument +type 'a glob_abstract_argument_type = ('a,glevel) abstract_argument_type -type 'a closed_abstract_argument_type = - ('a,Term.constr,glob_tactic_expr) abstract_argument_type +type 'a typed_abstract_argument_type = ('a,tlevel) abstract_argument_type -type declaration_hook = Decl_kinds.strength -> global_reference -> unit +type declaration_hook = locality -> global_reference -> unit diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index baf8c859..213cc13f 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tacmach.ml 9511 2007-01-22 08:27:31Z herbelin $ *) +(* $Id: tacmach.ml 10544 2008-02-09 11:31:35Z herbelin $ *) open Util open Names @@ -205,8 +205,11 @@ let thin_body_no_check ids gl = let move_hyp_no_check with_dep id1 id2 gl = refiner (Prim (Move (with_dep,id1,id2))) gl -let rename_hyp_no_check id1 id2 gl = - refiner (Prim (Rename (id1,id2))) gl +let rec rename_hyp_no_check l gl = match l with + | [] -> tclIDTAC gl + | (id1,id2)::l -> + tclTHEN (refiner (Prim (Rename (id1,id2)))) + (rename_hyp_no_check l) gl let mutual_fix f n others gl = with_check (refiner (Prim (FixRule (f,n,others)))) gl @@ -214,14 +217,6 @@ let mutual_fix f n others gl = let mutual_cofix f others gl = with_check (refiner (Prim (Cofix (f,others)))) gl -let rename_bound_var_goal gls = - let { evar_hyps = sign; evar_concl = cl } = sig_it gls in - let ids = ids_of_named_context (named_context_of_val sign) in - convert_concl_no_check - (rename_bound_var (Global.env()) ids cl) DEFAULTcast gls - - - (* Versions with consistency checks *) let introduction id = with_check (introduction_no_check id) @@ -234,8 +229,8 @@ let convert_hyp d = with_check (convert_hyp_no_check d) let thin l = with_check (thin_no_check l) let thin_body c = with_check (thin_body_no_check c) let move_hyp b id id' = with_check (move_hyp_no_check b id id') -let rename_hyp id id' = with_check (rename_hyp_no_check id id') - +let rename_hyp l = with_check (rename_hyp_no_check l) + (* Pretty-printers *) open Pp diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 9352cb5d..8b0053a4 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: tacmach.mli 7639 2005-12-02 10:01:15Z gregoire $ i*) +(*i $Id: tacmach.mli 11094 2008-06-10 19:35:23Z herbelin $ i*) (*i*) open Names @@ -37,7 +37,7 @@ val re_sig : 'a -> evar_map -> 'a sigma val unpackage : 'a sigma -> evar_map ref * 'a val repackage : evar_map ref -> 'a -> 'a sigma val apply_sig_tac : - evar_map ref -> ('a sigma -> 'b sigma * 'c) -> 'a -> 'b * 'c + evar_map ref -> (goal sigma -> (goal list) sigma * validation) -> goal -> (goal list) * validation val pf_concl : goal sigma -> types val pf_env : goal sigma -> env @@ -79,7 +79,7 @@ val pf_nf_betaiota : goal sigma -> constr -> constr val pf_reduce_to_quantified_ind : goal sigma -> types -> inductive * types val pf_reduce_to_atomic_ind : goal sigma -> types -> inductive * types val pf_compute : goal sigma -> constr -> constr -val pf_unfoldn : (int list * evaluable_global_reference) list +val pf_unfoldn : (Termops.occurrences * evaluable_global_reference) list -> goal sigma -> constr -> constr val pf_const_value : goal sigma -> constant -> constr @@ -132,11 +132,10 @@ val convert_hyp_no_check : named_declaration -> tactic val thin_no_check : identifier list -> tactic val thin_body_no_check : identifier list -> tactic val move_hyp_no_check : bool -> identifier -> identifier -> tactic -val rename_hyp_no_check : identifier -> identifier -> tactic +val rename_hyp_no_check : (identifier*identifier) list -> tactic val mutual_fix : identifier -> int -> (identifier * int * constr) list -> tactic val mutual_cofix : identifier -> (identifier * constr) list -> tactic -val rename_bound_var_goal : tactic (*s The most primitive tactics with consistency and type checking *) @@ -150,7 +149,7 @@ val convert_hyp : named_declaration -> tactic val thin : identifier list -> tactic val thin_body : identifier list -> tactic val move_hyp : bool -> identifier -> identifier -> tactic -val rename_hyp : identifier -> identifier -> tactic +val rename_hyp : (identifier*identifier) list -> tactic (*s Tactics handling a list of goals. *) diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml index 96df8f64..2e19011f 100644 --- a/proofs/tactic_debug.ml +++ b/proofs/tactic_debug.ml @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(*i $Id: tactic_debug.ml 10739 2008-04-01 14:45:20Z herbelin $ i*) + open Names open Constrextern open Pp -- cgit v1.2.3