diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/constr.ml | 24 | ||||
| -rw-r--r-- | kernel/constr.mli | 53 |
2 files changed, 45 insertions, 32 deletions
diff --git a/kernel/constr.ml b/kernel/constr.ml index b25f38d630..c97969c0e0 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -237,6 +237,17 @@ let mkVar id = Var id let kind c = c +let rec kind_nocast_gen kind c = + match kind c with + | Cast (c, _, _) -> kind_nocast_gen kind c + | App (h, outer) as k -> + (match kind_nocast_gen kind h with + | App (h, inner) -> App (h, Array.append inner outer) + | _ -> k) + | k -> k + +let kind_nocast c = kind_nocast_gen kind c + (* The other way around. We treat specifically smart constructors *) let of_kind = function | App (f, a) -> mkApp (f, a) @@ -755,10 +766,10 @@ let map_with_binders g f l c0 = match kind c0 with let bl' = Array.Fun1.Smart.map f l' bl in mkCoFix (ln,(lna,tl',bl')) -type instance_compare_fn = GlobRef.t -> int -> - Univ.Instance.t -> Univ.Instance.t -> bool +type 'univs instance_compare_fn = GlobRef.t -> int -> + 'univs -> 'univs -> bool -type constr_compare_fn = int -> constr -> constr -> bool +type 'constr constr_compare_fn = int -> 'constr -> 'constr -> bool (* [compare_head_gen_evar k1 k2 u s e eq leq c1 c2] compare [c1] and [c2] (using [k1] to expose the structure of [c1] and [k2] to expose @@ -772,19 +783,16 @@ type constr_compare_fn = int -> constr -> constr -> bool calls to {!Array.equal_norefl}). *) let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq leq nargs t1 t2 = - match kind1 t1, kind2 t2 with + match kind_nocast_gen kind1 t1, kind_nocast_gen kind2 t2 with + | Cast _, _ | _, Cast _ -> assert false (* kind_nocast *) | Rel n1, Rel n2 -> Int.equal n1 n2 | Meta m1, Meta m2 -> Int.equal m1 m2 | Var id1, Var id2 -> Id.equal id1 id2 | Sort s1, Sort s2 -> leq_sorts s1 s2 - | Cast (c1, _, _), _ -> leq nargs c1 t2 - | _, Cast (c2, _, _) -> leq nargs t1 c2 | Prod (_,t1,c1), Prod (_,t2,c2) -> eq 0 t1 t2 && leq 0 c1 c2 | Lambda (_,t1,c1), Lambda (_,t2,c2) -> eq 0 t1 t2 && eq 0 c1 c2 | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> eq 0 b1 b2 && eq 0 t1 t2 && leq nargs c1 c2 (* Why do we suddenly make a special case for Cast here? *) - | App (Cast (c1, _, _), l1), _ -> leq nargs (mkApp (c1, l1)) t2 - | _, App (Cast (c2, _, _), l2) -> leq nargs t1 (mkApp (c2, l2)) | App (c1, l1), App (c2, l2) -> let len = Array.length l1 in Int.equal len (Array.length l2) && diff --git a/kernel/constr.mli b/kernel/constr.mli index ea38dabd5c..2efdae007c 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -241,6 +241,11 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term = val kind : constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term val of_kind : (constr, types, Sorts.t, Univ.Instance.t) kind_of_term -> constr +val kind_nocast_gen : ('v -> ('v, 'v, 'sort, 'univs) kind_of_term) -> + ('v -> ('v, 'v, 'sort, 'univs) kind_of_term) + +val kind_nocast : constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term + (** {6 Simple case analysis} *) val isRel : constr -> bool val isRelN : int -> constr -> bool @@ -518,50 +523,50 @@ val iter_with_binders : val fold_constr_with_binders : ('a -> 'a) -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b -type constr_compare_fn = int -> constr -> constr -> bool +type 'constr constr_compare_fn = int -> 'constr -> 'constr -> bool (** [compare_head f c1 c2] compare [c1] and [c2] using [f] to compare the immediate subterms of [c1] of [c2] if needed; Cast's, binders name and Cases annotations are not taken into account *) -val compare_head : constr_compare_fn -> constr_compare_fn +val compare_head : constr constr_compare_fn -> constr constr_compare_fn (** Convert a global reference applied to 2 instances. The int says how many arguments are given (as we can only use cumulativity for fully applied inductives/constructors) .*) -type instance_compare_fn = GlobRef.t -> int -> - Univ.Instance.t -> Univ.Instance.t -> bool +type 'univs instance_compare_fn = GlobRef.t -> int -> + 'univs -> 'univs -> bool (** [compare_head_gen u s f c1 c2] compare [c1] and [c2] using [f] to compare the immediate subterms of [c1] of [c2] if needed, [u] to compare universe instances, [s] to compare sorts; Cast's, binders name and Cases annotations are not taken into account *) -val compare_head_gen : instance_compare_fn -> +val compare_head_gen : Univ.Instance.t instance_compare_fn -> (Sorts.t -> Sorts.t -> bool) -> - constr_compare_fn -> - constr_compare_fn + constr constr_compare_fn -> + constr constr_compare_fn val compare_head_gen_leq_with : - (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) -> - (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) -> - instance_compare_fn -> - (Sorts.t -> Sorts.t -> bool) -> - constr_compare_fn -> - constr_compare_fn -> - constr_compare_fn + ('v -> ('v, 'v, 'sort, 'univs) kind_of_term) -> + ('v -> ('v, 'v, 'sort, 'univs) kind_of_term) -> + 'univs instance_compare_fn -> + ('sort -> 'sort -> bool) -> + 'v constr_compare_fn -> + 'v constr_compare_fn -> + 'v constr_compare_fn (** [compare_head_gen_with k1 k2 u s f c1 c2] compares [c1] and [c2] like [compare_head_gen u s f c1 c2], except that [k1] (resp. [k2]) is used,rather than {!kind}, to expose the immediate subterms of [c1] (resp. [c2]). *) val compare_head_gen_with : - (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) -> - (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) -> - instance_compare_fn -> - (Sorts.t -> Sorts.t -> bool) -> - constr_compare_fn -> - constr_compare_fn + ('v -> ('v, 'v, 'sort, 'univs) kind_of_term) -> + ('v -> ('v, 'v, 'sort, 'univs) kind_of_term) -> + 'univs instance_compare_fn -> + ('sort -> 'sort -> bool) -> + 'v constr_compare_fn -> + 'v constr_compare_fn (** [compare_head_gen_leq u s f fle c1 c2] compare [c1] and [c2] using [f] to compare the immediate subterms of [c1] of [c2] for @@ -570,11 +575,11 @@ val compare_head_gen_with : [s] to compare sorts for for subtyping; Cast's, binders name and Cases annotations are not taken into account *) -val compare_head_gen_leq : instance_compare_fn -> +val compare_head_gen_leq : Univ.Instance.t instance_compare_fn -> (Sorts.t -> Sorts.t -> bool) -> - constr_compare_fn -> - constr_compare_fn -> - constr_compare_fn + constr constr_compare_fn -> + constr constr_compare_fn -> + constr constr_compare_fn (** {6 Hashconsing} *) |