diff options
| -rw-r--r-- | dev/base_include | 1 | ||||
| -rw-r--r-- | plugins/ltac/leminv.ml | 2 | ||||
| -rw-r--r-- | proofs/clenv.ml | 119 | ||||
| -rw-r--r-- | proofs/clenv.mli | 8 | ||||
| -rw-r--r-- | proofs/clenvtac.ml | 135 | ||||
| -rw-r--r-- | proofs/clenvtac.mli | 22 | ||||
| -rw-r--r-- | proofs/proofs.mllib | 1 | ||||
| -rw-r--r-- | tactics/auto.ml | 2 | ||||
| -rw-r--r-- | tactics/class_tactics.ml | 6 | ||||
| -rw-r--r-- | tactics/eauto.ml | 4 | ||||
| -rw-r--r-- | tactics/equality.ml | 8 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 10 |
13 files changed, 144 insertions, 176 deletions
diff --git a/dev/base_include b/dev/base_include index 45e79147c1..efbd156758 100644 --- a/dev/base_include +++ b/dev/base_include @@ -66,7 +66,6 @@ open Pretyping open Cbv open Coercionops open Clenv -open Clenvtac open Constr_matching open Glob_term open Glob_ops diff --git a/plugins/ltac/leminv.ml b/plugins/ltac/leminv.ml index 5a8ec404ee..0024d1a4ba 100644 --- a/plugins/ltac/leminv.ml +++ b/plugins/ltac/leminv.ml @@ -261,7 +261,7 @@ let lemInv id c = try let clause = mk_clenv_from_env (pf_env gls) (project gls) None (c, pf_get_type_of gls c) in let clause = clenv_constrain_last_binding (EConstr.mkVar id) clause in - Clenvtac.res_pf clause ~flags:(Unification.elim_flags ()) ~with_evars:false + Clenv.res_pf clause ~flags:(Unification.elim_flags ()) ~with_evars:false with | NoSuchBinding -> user_err diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 87b4255b88..4f19f943a8 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -28,6 +28,7 @@ open Pretype_errors open Evarutil open Unification open Tactypes +open Logic (******************************************************************) (* Clausal environments *) @@ -598,6 +599,124 @@ let clenv_constrain_dep_args hyps_only bl clenv = else error_not_right_number_missing_arguments (List.length occlist) + +(* This function put casts around metavariables whose type could not be + * inferred by the refiner, that is head of applications, predicates and + * subject of Cases. + * Does check that the casted type is closed. Anyway, the refiner would + * fail in this case... *) + +let clenv_cast_meta clenv = + let rec crec u = + match EConstr.kind clenv.evd u with + | App _ | Case _ -> crec_hd u + | Cast (c,_,_) when isMeta clenv.evd c -> u + | Proj (p, c) -> mkProj (p, crec_hd c) + | _ -> EConstr.map clenv.evd crec u + + and crec_hd u = + match EConstr.kind clenv.evd (strip_outer_cast clenv.evd u) with + | Meta mv -> + (try + let b = Typing.meta_type clenv.env clenv.evd mv in + assert (not (occur_meta clenv.evd b)); + if occur_meta clenv.evd b then u + else mkCast (mkMeta mv, DEFAULTcast, b) + with Not_found -> u) + | App(f,args) -> mkApp (crec_hd f, Array.map crec args) + | Case(ci,p,c,br) -> + mkCase (ci, crec_hd p, crec_hd c, Array.map crec br) + | Proj (p, c) -> mkProj (p, crec_hd c) + | _ -> u + in + crec + +let clenv_value_cast_meta clenv = + clenv_cast_meta clenv (clenv_value clenv) + +let clenv_pose_dependent_evars ?(with_evars=false) clenv = + let dep_mvs = clenv_dependent clenv in + let env, sigma = clenv.env, clenv.evd in + if not (List.is_empty dep_mvs) && not with_evars then + raise + (RefinerError (env, sigma, UnresolvedBindings (List.map (meta_name clenv.evd) dep_mvs))); + clenv_pose_metas_as_evars clenv dep_mvs + +let clenv_refine ?(with_evars=false) ?(with_classes=true) clenv = + Proofview.Goal.enter begin fun gl -> + let clenv, evars = clenv_pose_dependent_evars ~with_evars clenv in + let evd' = + if with_classes then + let evd' = + Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars + ~fail:(not with_evars) clenv.env clenv.evd + in + (* After an apply, all the subgoals including those dependent shelved ones are in + the hands of the user and resolution won't be called implicitely on them. *) + Typeclasses.make_unresolvables (fun x -> true) evd' + else clenv.evd + in + let clenv = { clenv with evd = evd' } in + Proofview.tclTHEN + (Proofview.Unsafe.tclEVARS (Evd.clear_metas evd')) + (refiner ~check:false EConstr.Unsafe.(to_constr (clenv_cast_meta clenv (clenv_value clenv)))) + end + +let clenv_pose_dependent_evars ?(with_evars=false) clenv = + fst (clenv_pose_dependent_evars ~with_evars clenv) + +open Unification + +let dft = default_unify_flags + +let res_pf ?with_evars ?(with_classes=true) ?(flags=dft ()) clenv = + Proofview.Goal.enter begin fun gl -> + let clenv = clenv_unique_resolver ~flags clenv gl in + clenv_refine ?with_evars ~with_classes clenv + end + +(* [unifyTerms] et [unify] ne semble pas gérer les Meta, en + particulier ne semblent pas vérifier que des instances différentes + d'une même Meta sont compatibles. D'ailleurs le "fst" jette les metas + provenant de w_Unify. (Utilisé seulement dans prolog.ml) *) + +let fail_quick_core_unif_flags = { + modulo_conv_on_closed_terms = Some TransparentState.full; + use_metas_eagerly_in_conv_on_closed_terms = false; + use_evars_eagerly_in_conv_on_closed_terms = false; + modulo_delta = TransparentState.empty; + modulo_delta_types = TransparentState.full; + check_applied_meta_types = false; + use_pattern_unification = false; + use_meta_bound_pattern_unification = true; (* ? *) + allowed_evars = AllowAll; + restrict_conv_on_strict_subterms = false; (* ? *) + modulo_betaiota = false; + modulo_eta = true; +} + +let fail_quick_unif_flags = { + core_unify_flags = fail_quick_core_unif_flags; + merge_unify_flags = fail_quick_core_unif_flags; + subterm_unify_flags = fail_quick_core_unif_flags; + allow_K_in_toplevel_higher_order_unification = false; + resolve_evars = false +} + +(* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *) +let unify ?(flags=fail_quick_unif_flags) m = + Proofview.Goal.enter begin fun gl -> + let env = Tacmach.New.pf_env gl in + let n = Tacmach.New.pf_concl gl in + let evd = clear_metas (Tacmach.New.project gl) in + try + let evd' = w_unify env evd CONV ~flags m n in + Proofview.Unsafe.tclEVARSADVANCE evd' + with e when CErrors.noncritical e -> + let info = Exninfo.reify () in + Proofview.tclZERO ~info e + end + (****************************************************************) (* Clausal environment for an application *) diff --git a/proofs/clenv.mli b/proofs/clenv.mli index 4279ab4768..492fca3963 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -109,6 +109,14 @@ val make_clenv_binding : exception NotExtensibleClause val clenv_push_prod : clausenv -> clausenv +(** {6 Clenv tactics} *) + +val unify : ?flags:unify_flags -> constr -> unit Proofview.tactic +val res_pf : ?with_evars:bool -> ?with_classes:bool -> ?flags:unify_flags -> clausenv -> unit Proofview.tactic + +val clenv_pose_dependent_evars : ?with_evars:bool -> clausenv -> clausenv +val clenv_value_cast_meta : clausenv -> constr + (** {6 Pretty-print (debug only) } *) val pr_clenv : clausenv -> Pp.t diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml deleted file mode 100644 index 007d53f911..0000000000 --- a/proofs/clenvtac.ml +++ /dev/null @@ -1,135 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Util -open Constr -open Termops -open Evd -open EConstr -open Logic -open Reduction -open Clenv - -(* This function put casts around metavariables whose type could not be - * inferred by the refiner, that is head of applications, predicates and - * subject of Cases. - * Does check that the casted type is closed. Anyway, the refiner would - * fail in this case... *) - -let clenv_cast_meta clenv = - let rec crec u = - match EConstr.kind clenv.evd u with - | App _ | Case _ -> crec_hd u - | Cast (c,_,_) when isMeta clenv.evd c -> u - | Proj (p, c) -> mkProj (p, crec_hd c) - | _ -> EConstr.map clenv.evd crec u - - and crec_hd u = - match EConstr.kind clenv.evd (strip_outer_cast clenv.evd u) with - | Meta mv -> - (try - let b = Typing.meta_type clenv.env clenv.evd mv in - assert (not (occur_meta clenv.evd b)); - if occur_meta clenv.evd b then u - else mkCast (mkMeta mv, DEFAULTcast, b) - with Not_found -> u) - | App(f,args) -> mkApp (crec_hd f, Array.map crec args) - | Case(ci,p,c,br) -> - mkCase (ci, crec_hd p, crec_hd c, Array.map crec br) - | Proj (p, c) -> mkProj (p, crec_hd c) - | _ -> u - in - crec - -let clenv_value_cast_meta clenv = - clenv_cast_meta clenv (clenv_value clenv) - -let clenv_pose_dependent_evars ?(with_evars=false) clenv = - let dep_mvs = clenv_dependent clenv in - let env, sigma = clenv.env, clenv.evd in - if not (List.is_empty dep_mvs) && not with_evars then - raise - (RefinerError (env, sigma, UnresolvedBindings (List.map (meta_name clenv.evd) dep_mvs))); - clenv_pose_metas_as_evars clenv dep_mvs - -let clenv_refine ?(with_evars=false) ?(with_classes=true) clenv = - Proofview.Goal.enter begin fun gl -> - let clenv, evars = clenv_pose_dependent_evars ~with_evars clenv in - let evd' = - if with_classes then - let evd' = - Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars - ~fail:(not with_evars) clenv.env clenv.evd - in - (* After an apply, all the subgoals including those dependent shelved ones are in - the hands of the user and resolution won't be called implicitely on them. *) - Typeclasses.make_unresolvables (fun x -> true) evd' - else clenv.evd - in - let clenv = { clenv with evd = evd' } in - Proofview.tclTHEN - (Proofview.Unsafe.tclEVARS (Evd.clear_metas evd')) - (refiner ~check:false EConstr.Unsafe.(to_constr (clenv_cast_meta clenv (clenv_value clenv)))) - end - -let clenv_pose_dependent_evars ?(with_evars=false) clenv = - fst (clenv_pose_dependent_evars ~with_evars clenv) - -open Unification - -let dft = default_unify_flags - -let res_pf ?with_evars ?(with_classes=true) ?(flags=dft ()) clenv = - Proofview.Goal.enter begin fun gl -> - let clenv = clenv_unique_resolver ~flags clenv gl in - clenv_refine ?with_evars ~with_classes clenv - end - -(* [unifyTerms] et [unify] ne semble pas gérer les Meta, en - particulier ne semblent pas vérifier que des instances différentes - d'une même Meta sont compatibles. D'ailleurs le "fst" jette les metas - provenant de w_Unify. (Utilisé seulement dans prolog.ml) *) - -let fail_quick_core_unif_flags = { - modulo_conv_on_closed_terms = Some TransparentState.full; - use_metas_eagerly_in_conv_on_closed_terms = false; - use_evars_eagerly_in_conv_on_closed_terms = false; - modulo_delta = TransparentState.empty; - modulo_delta_types = TransparentState.full; - check_applied_meta_types = false; - use_pattern_unification = false; - use_meta_bound_pattern_unification = true; (* ? *) - allowed_evars = AllowAll; - restrict_conv_on_strict_subterms = false; (* ? *) - modulo_betaiota = false; - modulo_eta = true; -} - -let fail_quick_unif_flags = { - core_unify_flags = fail_quick_core_unif_flags; - merge_unify_flags = fail_quick_core_unif_flags; - subterm_unify_flags = fail_quick_core_unif_flags; - allow_K_in_toplevel_higher_order_unification = false; - resolve_evars = false -} - -(* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *) -let unify ?(flags=fail_quick_unif_flags) m = - Proofview.Goal.enter begin fun gl -> - let env = Tacmach.New.pf_env gl in - let n = Tacmach.New.pf_concl gl in - let evd = clear_metas (Tacmach.New.project gl) in - try - let evd' = w_unify env evd CONV ~flags m n in - Proofview.Unsafe.tclEVARSADVANCE evd' - with e when CErrors.noncritical e -> - let info = Exninfo.reify () in - Proofview.tclZERO ~info e - end diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli deleted file mode 100644 index a34ec0e5be..0000000000 --- a/proofs/clenvtac.mli +++ /dev/null @@ -1,22 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -(** Legacy components of the previous proof engine. *) - -open Clenv -open EConstr -open Unification - -(** Tactics *) -val unify : ?flags:unify_flags -> constr -> unit Proofview.tactic -val res_pf : ?with_evars:bool -> ?with_classes:bool -> ?flags:unify_flags -> clausenv -> unit Proofview.tactic - -val clenv_pose_dependent_evars : ?with_evars:bool -> clausenv -> clausenv -val clenv_value_cast_meta : clausenv -> constr diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib index 756fef0511..790a9dd2cc 100644 --- a/proofs/proofs.mllib +++ b/proofs/proofs.mllib @@ -9,4 +9,3 @@ Proof_bullet Refiner Tacmach Clenv -Clenvtac diff --git a/tactics/auto.ml b/tactics/auto.ml index 4f7bb7ee1e..3287c1c354 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -99,7 +99,7 @@ let connect_hint_clenv h gl = let unify_resolve flags (h : hint) = Proofview.Goal.enter begin fun gl -> let clenv, c = connect_hint_clenv h gl in - Clenvtac.res_pf ~flags clenv + Clenv.res_pf ~flags clenv end let unify_resolve_nodelta h = unify_resolve auto_unif_flags h diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 56d6f7f09a..5ad21c2a5b 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -158,17 +158,17 @@ let e_give_exact flags h = in let (sigma, t1) = Typing.type_of (pf_env gl) sigma c in Proofview.Unsafe.tclEVARS sigma <*> - Clenvtac.unify ~flags t1 <*> exact_no_check c + Clenv.unify ~flags t1 <*> exact_no_check c end let unify_e_resolve flags = begin fun gls (h, _) -> let clenv', c = connect_hint_clenv h gls in - Clenvtac.res_pf ~with_evars:true ~with_classes:false ~flags clenv' + Clenv.res_pf ~with_evars:true ~with_classes:false ~flags clenv' end let unify_resolve flags = begin fun gls (h, _) -> let clenv', _ = connect_hint_clenv h gls in - Clenvtac.res_pf ~with_evars:false ~with_classes:false ~flags clenv' + Clenv.res_pf ~with_evars:false ~with_classes:false ~flags clenv' end (** Application of a lemma using [refine] instead of the old [w_unify] *) diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 7269228485..d275e15255 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -37,7 +37,7 @@ let e_give_exact ?(flags=eauto_unif_flags) c = if occur_existential sigma t1 || occur_existential sigma t2 then Tacticals.New.tclTHENLIST [Proofview.Unsafe.tclEVARS sigma; - Clenvtac.unify ~flags t1; + Clenv.unify ~flags t1; exact_no_check c] else exact_check c end @@ -68,7 +68,7 @@ open Auto let unify_e_resolve flags h = Proofview.Goal.enter begin fun gl -> let clenv', c = connect_hint_clenv h gl in - Clenvtac.res_pf ~with_evars:true ~with_classes:true ~flags clenv' + Clenv.res_pf ~with_evars:true ~with_classes:true ~flags clenv' end let hintmap_of sigma secvars concl = diff --git a/tactics/equality.ml b/tactics/equality.ml index 79b6dfe920..39017c946f 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -154,7 +154,7 @@ let instantiate_lemma_all frzevars gl c ty l l2r concl = let c1 = args.(arglen - 2) in let c2 = args.(arglen - 1) in let try_occ (evd', c') = - Clenvtac.clenv_pose_dependent_evars ~with_evars:true {eqclause with evd = evd'} + Clenv.clenv_pose_dependent_evars ~with_evars:true {eqclause with evd = evd'} in let flags = make_flags frzevars (Tacmach.New.project gl) rewrite_unif_flags eqclause in let occs = @@ -1045,7 +1045,7 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn = discrimination_pf e (t,t1,t2) discriminator lbeq false_kind >>= fun pf -> let pf_ty = mkArrow eqn Sorts.Relevant false_0 in let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in - let pf = Clenvtac.clenv_value_cast_meta absurd_clause in + let pf = Clenv.clenv_value_cast_meta absurd_clause in tclTHENS (assert_after Anonymous false_0) [onLastHypId gen_absurdity; (Refiner.refiner ~check:true EConstr.Unsafe.(to_constr pf))] @@ -1067,7 +1067,7 @@ let onEquality with_evars tac (c,lbindc) = let t = pf_get_type_of gl c in let t' = try snd (reduce_to_quantified_ind t) with UserError _ -> t in let eq_clause = pf_apply make_clenv_binding gl (c,t') lbindc in - let eq_clause' = Clenvtac.clenv_pose_dependent_evars ~with_evars eq_clause in + let eq_clause' = Clenv.clenv_pose_dependent_evars ~with_evars eq_clause in let eqn = clenv_type eq_clause' in (* FIXME evar leak *) let (eq,u,eq_args) = pf_apply find_this_eq_data_decompose gl eqn in @@ -1397,7 +1397,7 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac = let pf = applist(congr,[t;resty;injfun;t1;t2]) in let sigma, pf_typ = Typing.type_of env sigma pf in let inj_clause = apply_on_clause (pf,pf_typ) eq_clause in - let pf = Clenvtac.clenv_value_cast_meta inj_clause in + let pf = Clenv.clenv_value_cast_meta inj_clause in let ty = simplify_args env sigma (clenv_type inj_clause) in evdref := sigma; Some (pf, ty) diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 483d8a726b..22c5bbe73f 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -695,7 +695,7 @@ module New = struct in let branchtacs = List.init (Array.length branchsigns) after_tac in Proofview.tclTHEN - (Clenvtac.res_pf ~flags elimclause') + (Clenv.res_pf ~flags elimclause') (Proofview.tclEXTEND [] tclIDTAC branchtacs) end) end diff --git a/tactics/tactics.ml b/tactics/tactics.ml index fd9fd81500..3133f9be1e 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1373,7 +1373,7 @@ let do_replace id = function [id] is replaced by P using the proof given by [tac] *) let clenv_refine_in ?err with_evars targetid id sigma0 clenv tac = - let clenv = Clenvtac.clenv_pose_dependent_evars ~with_evars clenv in + let clenv = Clenv.clenv_pose_dependent_evars ~with_evars clenv in let clenv = { clenv with evd = Typeclasses.resolve_typeclasses ~fail:(not with_evars) clenv.env clenv.evd } @@ -1475,7 +1475,7 @@ let general_elim_clause with_evars flags where indclause elim = match where with | None -> let elimclause = clenv_fchain ~flags indmv elimclause indclause in - Clenvtac.res_pf elimclause ~with_evars ~with_classes:true ~flags + Clenv.res_pf elimclause ~with_evars ~with_classes:true ~flags | Some id -> let hypmv = match List.remove Int.equal indmv (clenv_independent elimclause) with @@ -1737,7 +1737,7 @@ let general_apply ?(respect_opaque=false) with_delta with_destruct with_evars let n = nb_prod_modulo_zeta sigma thm_ty - nprod in if n<0 then error "Applied theorem does not have enough premises."; let clause = make_clenv_binding_apply env sigma (Some n) (c,thm_ty) lbind in - Clenvtac.res_pf clause ~with_evars ~flags + Clenv.res_pf clause ~with_evars ~flags with exn when noncritical exn -> let exn, info = Exninfo.capture exn in Proofview.tclZERO ~info exn @@ -4371,7 +4371,7 @@ let induction_tac with_evars params indvars elim = (* elimclause' is built from elimclause by instantiating all args and params. *) let elimclause' = recolle_clenv i params indvars elimclause gl in (* one last resolution (useless?) *) - Clenvtac.res_pf ~with_evars ~flags:(elim_flags ()) elimclause' + Clenv.res_pf ~with_evars ~flags:(elim_flags ()) elimclause' end (* Apply induction "in place" taking into account dependent @@ -4812,7 +4812,7 @@ let elim_scheme_type elim t = (* t is inductive, then CUMUL or CONV is irrelevant *) clenv_unify ~flags:(elim_flags ()) Reduction.CUMUL t (clenv_meta_type clause mv) clause in - Clenvtac.res_pf clause' ~flags:(elim_flags ()) ~with_evars:false + Clenv.res_pf clause' ~flags:(elim_flags ()) ~with_evars:false | _ -> anomaly (Pp.str "elim_scheme_type.") end |