diff options
Diffstat (limited to 'kernel/constr.mli')
| -rw-r--r-- | kernel/constr.mli | 47 |
1 files changed, 27 insertions, 20 deletions
diff --git a/kernel/constr.mli b/kernel/constr.mli index f7e4eecba..98c0eaa28 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -402,31 +402,38 @@ val iter : (constr -> unit) -> constr -> unit val iter_with_binders : ('a -> 'a) -> ('a -> constr -> unit) -> 'a -> constr -> unit +type 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 -> constr -> bool) -> constr -> constr -> bool +val compare_head : constr_compare_fn -> 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 = global_reference -> int -> + Univ.Instance.t -> Univ.Instance.t -> 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 (the first boolean tells if they belong to a Constant.t), [s] to - compare sorts; Cast's, binders name and Cases annotations are not taken - into account *) +(** [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 : (bool -> Univ.Instance.t -> Univ.Instance.t -> bool) -> +val compare_head_gen : instance_compare_fn -> (Sorts.t -> Sorts.t -> bool) -> - (constr -> constr -> bool) -> - constr -> constr -> bool + constr_compare_fn -> + 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) -> - (bool -> Univ.Instance.t -> Univ.Instance.t -> bool) -> + instance_compare_fn -> (Sorts.t -> Sorts.t -> bool) -> - (constr -> constr -> bool) -> - (constr -> constr -> bool) -> - constr -> constr -> bool + constr_compare_fn -> + constr_compare_fn -> + 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]) @@ -435,10 +442,10 @@ val compare_head_gen_leq_with : 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) -> - (bool -> Univ.Instance.t -> Univ.Instance.t -> bool) -> + instance_compare_fn -> (Sorts.t -> Sorts.t -> bool) -> - (constr -> constr -> bool) -> - constr -> constr -> bool + constr_compare_fn -> + 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 @@ -447,11 +454,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 : (bool -> Univ.Instance.t -> Univ.Instance.t -> bool) -> +val compare_head_gen_leq : instance_compare_fn -> (Sorts.t -> Sorts.t -> bool) -> - (constr -> constr -> bool) -> - (constr -> constr -> bool) -> - constr -> constr -> bool + constr_compare_fn -> + constr_compare_fn -> + constr_compare_fn (** {6 Hashconsing} *) |