diff options
Diffstat (limited to 'proofs')
| -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 |
5 files changed, 127 insertions, 158 deletions
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 |