diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/keys.ml | 162 | ||||
| -rw-r--r-- | pretyping/keys.mli | 23 | ||||
| -rw-r--r-- | pretyping/pretyping.mllib | 1 | ||||
| -rw-r--r-- | pretyping/unification.ml | 32 | ||||
| -rw-r--r-- | pretyping/unification.mli | 6 |
5 files changed, 212 insertions, 12 deletions
diff --git a/pretyping/keys.ml b/pretyping/keys.ml new file mode 100644 index 0000000000..f8eecd80d4 --- /dev/null +++ b/pretyping/keys.ml @@ -0,0 +1,162 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \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) *) +(************************************************************************) + +(** Keys for unification and indexing *) + +open Names +open Constr +open Libobject +open Globnames + +type key = + | KGlob of GlobRef.t + | KLam + | KLet + | KProd + | KSort + | KCase + | KFix + | KCoFix + | KRel + | KInt + +module KeyOrdered = struct + type t = key + + let hash gr = + match gr with + | KGlob gr -> 9 + GlobRef.Ordered.hash gr + | KLam -> 0 + | KLet -> 1 + | KProd -> 2 + | KSort -> 3 + | KCase -> 4 + | KFix -> 5 + | KCoFix -> 6 + | KRel -> 7 + | KInt -> 8 + + let compare gr1 gr2 = + match gr1, gr2 with + | KGlob gr1, KGlob gr2 -> GlobRef.Ordered.compare gr1 gr2 + | _, KGlob _ -> -1 + | KGlob _, _ -> 1 + | k, k' -> Int.compare (hash k) (hash k') + + let equal k1 k2 = + match k1, k2 with + | KGlob gr1, KGlob gr2 -> GlobRef.Ordered.equal gr1 gr2 + | _, KGlob _ -> false + | KGlob _, _ -> false + | k, k' -> k == k' +end + +module Keymap = HMap.Make(KeyOrdered) +module Keyset = Keymap.Set + +(* Mapping structure for references to be considered equivalent *) + +let keys = Summary.ref Keymap.empty ~name:"Keys_decl" + +let add_kv k v m = + try Keymap.modify k (fun k' vs -> Keyset.add v vs) m + with Not_found -> Keymap.add k (Keyset.singleton v) m + +let add_keys k v = + keys := add_kv k v (add_kv v k !keys) + +let equiv_keys k k' = + k == k' || KeyOrdered.equal k k' || + try Keyset.mem k' (Keymap.find k !keys) + with Not_found -> false + +(** Registration of keys as an object *) + +let load_keys _ (_,(ref,ref')) = + add_keys ref ref' + +let cache_keys o = + load_keys 1 o + +let subst_key subst k = + match k with + | KGlob gr -> KGlob (subst_global_reference subst gr) + | _ -> k + +let subst_keys (subst,(k,k')) = + (subst_key subst k, subst_key subst k') + +let discharge_key = function + | KGlob (GlobRef.VarRef _ as g) when Lib.is_in_section g -> None + | x -> Some x + +let discharge_keys (_,(k,k')) = + match discharge_key k, discharge_key k' with + | Some x, Some y -> Some (x, y) + | _ -> None + +type key_obj = key * key + +let inKeys : key_obj -> obj = + declare_object @@ superglobal_object "KEYS" + ~cache:cache_keys + ~subst:(Some subst_keys) + ~discharge:discharge_keys + +let declare_equiv_keys ref ref' = + Lib.add_anonymous_leaf (inKeys (ref,ref')) + +let constr_key kind c = + try + let rec aux k = + match kind k with + | Const (c, _) -> KGlob (GlobRef.ConstRef c) + | Ind (i, u) -> KGlob (GlobRef.IndRef i) + | Construct (c,u) -> KGlob (GlobRef.ConstructRef c) + | Var id -> KGlob (GlobRef.VarRef id) + | App (f, _) -> aux f + | Proj (p, _) -> KGlob (GlobRef.ConstRef (Projection.constant p)) + | Cast (p, _, _) -> aux p + | Lambda _ -> KLam + | Prod _ -> KProd + | Case _ -> KCase + | Fix _ -> KFix + | CoFix _ -> KCoFix + | Rel _ -> KRel + | Meta _ -> raise Not_found + | Evar _ -> raise Not_found + | Sort _ -> KSort + | LetIn _ -> KLet + | Int _ -> KInt + in Some (aux c) + with Not_found -> None + +open Pp + +let pr_key pr_global = function + | KGlob gr -> pr_global gr + | KLam -> str"Lambda" + | KLet -> str"Let" + | KProd -> str"Product" + | KSort -> str"Sort" + | KCase -> str"Case" + | KFix -> str"Fix" + | KCoFix -> str"CoFix" + | KRel -> str"Rel" + | KInt -> str"Int" + +let pr_keyset pr_global v = + prlist_with_sep spc (pr_key pr_global) (Keyset.elements v) + +let pr_mapping pr_global k v = + pr_key pr_global k ++ str" <-> " ++ pr_keyset pr_global v + +let pr_keys pr_global = + Keymap.fold (fun k v acc -> pr_mapping pr_global k v ++ fnl () ++ acc) !keys (mt()) diff --git a/pretyping/keys.mli b/pretyping/keys.mli new file mode 100644 index 0000000000..a7adf7791b --- /dev/null +++ b/pretyping/keys.mli @@ -0,0 +1,23 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \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) *) +(************************************************************************) + +type key + +val declare_equiv_keys : key -> key -> unit +(** Declare two keys as being equivalent. *) + +val equiv_keys : key -> key -> bool +(** Check equivalence of keys. *) + +val constr_key : ('a -> ('a, 't, 'u, 'i) Constr.kind_of_term) -> 'a -> key option +(** Compute the head key of a term. *) + +val pr_keys : (Names.GlobRef.t -> Pp.t) -> Pp.t +(** Pretty-print the mapping *) diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index 34a6cecc95..0ca39f0404 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -35,4 +35,5 @@ Indrec GlobEnv Cases Pretyping +Keys Unification diff --git a/pretyping/unification.ml b/pretyping/unification.ml index a9eb43e573..4d34139ec0 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -254,6 +254,10 @@ let unify_r2l x = x let sort_eqns = unify_r2l *) +type allowed_evars = +| AllowAll +| AllowFun of (Evar.t -> bool) + type core_unify_flags = { modulo_conv_on_closed_terms : TransparentState.t option; (* What this flag controls was activated with all constants transparent, *) @@ -287,8 +291,8 @@ type core_unify_flags = { (* This allowed for instance to unify "forall x:?A, ?B x" with "A' -> B'" *) (* when ?B is a Meta. *) - frozen_evars : Evar.Set.t; - (* Evars of this set are considered axioms and never instantiated *) + allowed_evars : allowed_evars; + (* Evars that are allowed to be instantiated *) (* Useful e.g. for autorewrite *) restrict_conv_on_strict_subterms : bool; @@ -339,7 +343,7 @@ let default_core_unify_flags () = check_applied_meta_types = true; use_pattern_unification = true; use_meta_bound_pattern_unification = true; - frozen_evars = Evar.Set.empty; + allowed_evars = AllowAll; restrict_conv_on_strict_subterms = false; modulo_betaiota = true; modulo_eta = true; @@ -417,6 +421,10 @@ let default_no_delta_unify_flags ts = resolve_evars = false } +let allow_new_evars sigma = + let undefined = Evd.undefined_map sigma in + AllowFun (fun evk -> not (Evar.Map.mem evk undefined)) + (* Default flags for looking for subterms in elimination tactics *) (* Not used in practice at the current date, to the exception of *) (* allow_K) because only closed terms are involved in *) @@ -424,9 +432,7 @@ let default_no_delta_unify_flags ts = (* call w_unify for induction/destruct/case/elim (13/6/2011) *) let elim_core_flags sigma = { (default_core_unify_flags ()) with modulo_betaiota = false; - frozen_evars = - fold_undefined (fun evk _ evars -> Evar.Set.add evk evars) - sigma Evar.Set.empty; + allowed_evars = allow_new_evars sigma; } let elim_flags_evars sigma = @@ -600,8 +606,12 @@ let do_reduce ts (env, nb) sigma c = Stack.zip sigma (whd_betaiota_deltazeta_for_iota_state ts env sigma (c, Stack.empty)) +let is_evar_allowed flags evk = match flags.allowed_evars with +| AllowAll -> true +| AllowFun f -> f evk + let isAllowedEvar sigma flags c = match EConstr.kind sigma c with - | Evar (evk,_) -> not (Evar.Set.mem evk flags.frozen_evars) + | Evar (evk,_) -> is_evar_allowed flags evk | _ -> false @@ -749,7 +759,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e evarsubst) else error_cannot_unify_local curenv sigma (m,n,cM) | Evar (evk,_ as ev), Evar (evk',_) - when not (Evar.Set.mem evk flags.frozen_evars) + when is_evar_allowed flags evk && Evar.equal evk evk' -> begin match constr_cmp cv_pb env sigma flags cM cN with | Some sigma -> @@ -758,14 +768,14 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e sigma,metasubst,((curenv,ev,cN)::evarsubst) end | Evar (evk,_ as ev), _ - when not (Evar.Set.mem evk flags.frozen_evars) + when is_evar_allowed flags evk && not (occur_evar sigma evk cN) -> let cmvars = free_rels sigma cM and cnvars = free_rels sigma cN in if Int.Set.subset cnvars cmvars then sigma,metasubst,((curenv,ev,cN)::evarsubst) else error_cannot_unify_local curenv sigma (m,n,cN) | _, Evar (evk,_ as ev) - when not (Evar.Set.mem evk flags.frozen_evars) + when is_evar_allowed flags evk && not (occur_evar sigma evk cM) -> let cmvars = free_rels sigma cM and cnvars = free_rels sigma cN in if Int.Set.subset cmvars cnvars then @@ -1554,7 +1564,7 @@ let default_matching_core_flags sigma = check_applied_meta_types = true; use_pattern_unification = false; use_meta_bound_pattern_unification = false; - frozen_evars = Evar.Map.domain (Evd.undefined_map sigma); + allowed_evars = allow_new_evars sigma; restrict_conv_on_strict_subterms = false; modulo_betaiota = false; modulo_eta = false; diff --git a/pretyping/unification.mli b/pretyping/unification.mli index 0ee71246d8..d7ddbcb721 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -13,6 +13,10 @@ open EConstr open Environ open Evd +type allowed_evars = +| AllowAll +| AllowFun of (Evar.t -> bool) + type core_unify_flags = { modulo_conv_on_closed_terms : TransparentState.t option; use_metas_eagerly_in_conv_on_closed_terms : bool; @@ -22,7 +26,7 @@ type core_unify_flags = { check_applied_meta_types : bool; use_pattern_unification : bool; use_meta_bound_pattern_unification : bool; - frozen_evars : Evar.Set.t; + allowed_evars : allowed_evars; restrict_conv_on_strict_subterms : bool; modulo_betaiota : bool; modulo_eta : bool; |