1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149
(************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) open Util open Names open Term open Termops open Evd open EConstr open Refiner open Logic open Reduction open Tacmach open Clenv (* This function put casts around metavariables whose type could not be * infered 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.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 clenv = let dep_mvs = clenv_dependent clenv in if not (List.is_empty 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 (** Use our own fast path, more informative than from Typeclasses *) let check_tc evd = let has_resolvable = ref false in let check _ evi = let res = Typeclasses.is_resolvable evi in if res then let () = has_resolvable := true in Typeclasses.is_class_evar evd evi else false in let has_typeclass = Evar.Map.exists check (Evd.undefined_map evd) in (has_typeclass, !has_resolvable) let clenv_refine with_evars ?(with_classes=true) clenv = (** ppedrot: a Goal.enter here breaks things, because the tactic below may solve goals by side effects, while the compatibility layer keeps those useless goals. That deserves a FIXME. *) Proofview.V82.tactic begin fun gl -> let clenv = clenv_pose_dependent_evars with_evars clenv in let evd' = if with_classes then let (has_typeclass, has_resolvable) = check_tc clenv.evd in let evd' = if has_typeclass then Typeclasses.resolve_typeclasses ~fast_path:false ~filter:Typeclasses.all_evars ~fail:(not with_evars) clenv.env clenv.evd else clenv.evd in if has_resolvable then Typeclasses.mark_unresolvables ~filter:Typeclasses.all_goals evd' else evd' else clenv.evd in let clenv = { clenv with evd = evd' } in tclTHEN (tclEVARS (Evd.clear_metas evd')) (refine_no_check (clenv_cast_meta clenv (clenv_value clenv))) gl end open Unification let dft = default_unify_flags let res_pf ?(with_evars=false) ?(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 full_transparent_state; use_metas_eagerly_in_conv_on_closed_terms = false; use_evars_eagerly_in_conv_on_closed_terms = false; modulo_delta = empty_transparent_state; modulo_delta_types = full_transparent_state; check_applied_meta_types = false; use_pattern_unification = false; use_meta_bound_pattern_unification = true; (* ? *) frozen_evars = Evar.Set.empty; 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 (Proofview.Goal.assume 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 -> Proofview.tclZERO e end