diff options
| -rw-r--r-- | dev/printers.mllib | 1 | ||||
| -rw-r--r-- | library/keys.ml | 124 | ||||
| -rw-r--r-- | library/keys.mli | 9 | ||||
| -rw-r--r-- | library/library.mllib | 2 | ||||
| -rw-r--r-- | pretyping/unification.ml | 26 |
5 files changed, 116 insertions, 46 deletions
diff --git a/dev/printers.mllib b/dev/printers.mllib index 4afa9d4fc..1d09ce105 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -109,6 +109,7 @@ Goptions Decls Heads Assumptions +Keys Locusops Miscops Universes diff --git a/library/keys.ml b/library/keys.ml index 5c295a385..c661e67fb 100644 --- a/library/keys.ml +++ b/library/keys.ml @@ -2,45 +2,125 @@ open Globnames open Term open Libobject + +type key = + | KGlob of global_reference + | KLam + | KLet + | KProd + | KSort + | KEvar + | KCase + | KFix + | KCoFix + | KRel + | KMeta + +module KeyOrdered = struct + type t = key + + let hash gr = + match gr with + | KGlob gr -> 10 + RefOrdered.hash gr + | KLam -> 0 + | KLet -> 1 + | KProd -> 2 + | KSort -> 3 + | KEvar -> 4 + | KCase -> 5 + | KFix -> 6 + | KCoFix -> 7 + | KRel -> 8 + | KMeta -> 9 + + let compare gr1 gr2 = + match gr1, gr2 with + | KGlob gr1, KGlob gr2 -> RefOrdered.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 -> RefOrdered.equal gr1 gr2 + | _, KGlob _ -> false + | KGlob _, _ -> false + | k, k' -> k == k' +end + +module Keymap = HMap.Make(KeyOrdered) +module Keyset = Keymap.Set + (* Union-find structure for references to be considered equivalent *) -module RefUF = Unionfind.Make(Refset)(Refmap) +module KeyUF = Unionfind.Make(Keyset)(Keymap) -let keys = (* Summary.ref ( *)RefUF.create ()(* ) ~name:"Keys_decl" *) +let keys = (* Summary.ref ( *)KeyUF.create ()(* ) ~name:"Keys_decl" *) -let add_key k v = RefUF.union k v keys +let add_keys k v = KeyUF.union k v keys -let equiv_keys k k' = RefUF.find k keys == RefUF.find k' keys +let equiv_keys k k' = + k == k' || KeyUF.find k keys == KeyUF.find k' keys (** Registration of keys as an object *) -let load_key _ (_,(ref,ref')) = - add_key ref ref' +let load_keys _ (_,(ref,ref')) = + add_keys ref ref' + +let cache_keys o = + load_keys 1 o -let cache_key o = - load_key 1 o +let subst_key subst k = + match k with + | KGlob gr -> KGlob (subst_global_reference subst gr) + | _ -> k -let subst_key (subst,(ref,ref')) = - (subst_global_reference subst ref, - subst_global_reference subst ref') +let subst_keys (subst,(k,k')) = + (subst_key subst k, subst_key subst k') -let discharge_key (_,refs) = - match refs with - | VarRef _, _ | _, VarRef _ -> None - | ref, ref' -> Some (pop_global_reference ref, pop_global_reference ref') +let discharge_key = function + | KGlob (VarRef _) -> None + | KGlob g -> Some (KGlob (pop_global_reference g)) + | x -> Some x -let rebuild_key (ref,ref') = (ref, ref') +let discharge_keys (_,(k,k')) = + match discharge_key k, discharge_key k' with + | Some x, Some y -> Some (x, y) + | _ -> None -type key_obj = global_reference * global_reference +let rebuild_keys (ref,ref') = (ref, ref') + +type key_obj = key * key let inKeys : key_obj -> obj = declare_object {(default_object "KEYS") with - cache_function = cache_key; - load_function = load_key; - subst_function = subst_key; + cache_function = cache_keys; + load_function = load_keys; + subst_function = subst_keys; classify_function = (fun x -> Substitute x); - discharge_function = discharge_key; - rebuild_function = rebuild_key } + discharge_function = discharge_keys; + rebuild_function = rebuild_keys } let declare_keys ref ref' = Lib.add_anonymous_leaf (inKeys (ref,ref')) + +let rec constr_key c = + let open Globnames in + match kind_of_term c with + | Const (c, _) -> KGlob (ConstRef c) + | Ind (i, u) -> KGlob (IndRef i) + | Construct (c,u) -> KGlob (ConstructRef c) + | Var id -> KGlob (VarRef id) + | App (f, _) -> constr_key f + | Proj (p, _) -> KGlob (ConstRef p) + | Cast (p, _, _) -> constr_key p + | Lambda _ -> KLam + | Prod _ -> KProd + | Case _ -> KCase + | Fix _ -> KFix + | CoFix _ -> KCoFix + | Rel _ -> KRel + | Meta _ -> KMeta + | Evar _ -> KEvar + | Sort _ -> KSort + | LetIn _ -> KLet diff --git a/library/keys.mli b/library/keys.mli index 4e6a803e4..87ba45558 100644 --- a/library/keys.mli +++ b/library/keys.mli @@ -8,8 +8,13 @@ open Globnames -val declare_keys : global_reference -> global_reference -> unit +type key + +val declare_keys : key -> key -> unit (** Declare two keys as being equivalent. *) -val equiv_keys : global_reference -> global_reference -> bool +val equiv_keys : key -> key -> bool (** Check equivalence of keys. *) + +val constr_key : Term.constr -> key +(** Compute the head key of a term. *) diff --git a/library/library.mllib b/library/library.mllib index 04244160b..eca28c822 100644 --- a/library/library.mllib +++ b/library/library.mllib @@ -17,4 +17,4 @@ Goptions Decls Heads Assumptions - +Keys diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 1a1143fe7..efa64ca1e 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1457,38 +1457,22 @@ let make_abstraction env evd ccl abs = make_abstraction_core name (make_eq_test env evd c) (evd,c) ty occs check_occs env ccl -let rec constr_key c = - let open Globnames in - match kind_of_term c with - | Const (c, _) -> ConstRef c - | Ind (i, u) -> IndRef i - | Construct (c,u) -> ConstructRef c - | Var id -> VarRef id - | App (f, _) -> constr_key f - | Proj (p, _) -> ConstRef p - | Cast (p, _, _) -> constr_key p - | Lambda _ - | Prod _ - | Case _ - | Fix _ | CoFix _ - | Rel _ | Meta _ | Evar _ | Sort _ | LetIn _ -> raise Not_found - -let keyed_unify env evd op cl = +let keyed_unify env evd kop cl = if not !keyed_unification then true else - let k1 = constr_key op in - let k2 = constr_key cl in - Globnames.eq_gr k1 k2 || Keys.equiv_keys k1 k2 + let k2 = Keys.constr_key cl in + Keys.equiv_keys kop k2 (* Tries to find an instance of term [cl] in term [op]. Unifies [cl] to every subterm of [op] until it finds a match. Fails if no match is found *) let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) = let bestexn = ref None in + let kop = Keys.constr_key op in let rec matchrec cl = let cl = strip_outer_cast cl in (try - if closed0 cl && not (isEvar cl) && keyed_unify env evd op cl then + if closed0 cl && not (isEvar cl) && keyed_unify env evd kop cl then (try w_typed_unify env evd CONV flags op cl,cl with ex when Pretype_errors.unsatisfiable_exception ex -> bestexn := Some ex; error "Unsat") |