Module Compare

Comparison on types, terms and ordis

General function

val eq_assoc : ('b -> 'b -> bool) -> ('a * 'b) list -> ('a * 'b) list -> bool
val eq_option : ('a -> 'a -> bool) -> 'a option -> 'a option -> bool
val eq_strict : bool Stdlib.ref

this boolean control the fact that an equality is strict: i.e. it can not instanciate unification variables

val strict : ('a -> bool) -> 'a -> bool

make a function strict by changing and restoring eq_strict

val constant_mbind : int -> 'a -> (Ast.ordi, 'a) LibTools.Bindlib.mbinder
val mbind_assoc : (('a * 'b LibTools.Bindlib.box) list -> 'c LibTools.Bindlib.box) -> int -> ('a * (Ast.ordi, 'b) LibTools.Bindlib.mbinder) list -> (Ast.ordi, 'c) LibTools.Bindlib.mbinder
val set_kuvar : (Ast.kind, 'a) Ast.uvar -> (Ast.ordi, Ast.kind) LibTools.Bindlib.mbinder -> unit

function to set type variables (a more complex function safe_set_kuvar exists)

val set_ouvar : ?msg:string -> (Ast.ordi, 'a) Ast.uvar -> (Ast.ordi, Ast.ordi) LibTools.Bindlib.mbinder -> unit

function to set ordi variables

val fbind_ordis : (Ast.ordi array -> Ast.kind -> Ast.kind Ast.from_ordis) Stdlib.ref

TODO: reorder the definition to minimize mutual recursion

val fobind_ordis : (Ast.ordi array -> Ast.ordi -> Ast.ordi Ast.from_ordis) Stdlib.ref

Ordinal comparisons

val eq_ordis : Ast.ordi list -> Ast.ordi array -> Ast.ordi array -> bool
val optpr : Stdlib.Format.formatter -> Ast.ordi option -> unit

try to set OUVar(p,os) with o. Return true in case of success.

val safe_set_ouvar : Ast.ordi list -> Ast.ouvar -> Ast.ordi array -> Ast.ordi -> bool
val is_positive : Ast.ordi list -> Ast.ordi -> bool
val eq_schema : Ast.schema -> Ast.schema -> bool
val eq_term_or_kind : Ast.ordi list -> Ast.term_or_kind -> Ast.term_or_kind -> bool
val leqi_ordi : Ast.ordi list -> Ast.ordi -> int -> Ast.ordi -> bool

Equality on kinds

Equality on terms

Strict equalities

val strict_eq_kind : Ast.kind -> Ast.kind -> bool
val strict_eq_term : Ast.term -> Ast.term -> bool
val strict_eq_ordi : Ast.ordi -> Ast.ordi -> bool
val strict_eq_ord_wit : Ast.ord_wit -> Ast.ord_wit -> bool
val strict_leq_ordi : Ast.ordi -> Ast.ordi -> bool
val gen_occur : ?safe_ordis:Ast.ordi array -> ?kuvar:(Ast.kuvar -> bool) -> ?ouvar:(Ast.ouvar -> bool) -> unit -> (Ast.kind -> Ast.occur) * (Ast.ordi -> Ast.occur)
val ouvar_occur : ?safe_ordis:Ast.ordi array -> Ast.ouvar -> Ast.ordi -> bool
val ouvar_kind_occur : ?safe_ordis:Ast.ordi array -> Ast.ouvar -> Ast.kind -> bool
val kuvar_occur : ?safe_ordis:Ast.ordi array -> Ast.kuvar -> Ast.kind -> Ast.occur
val kuvar_ord_occur : ?safe_ordis:Ast.ordi array -> Ast.kuvar -> Ast.ordi -> bool
val ouvar_mbind_occur : Ast.ouvar -> Ast.ordi Ast.from_ordis -> Ast.ordi array -> bool

Protection of tests

val eq_kind : Ast.ordi list -> Ast.kind -> Ast.kind -> bool
val eq_term : Ast.ordi list -> Ast.term -> Ast.term -> bool
val eq_ordi : Ast.ordi list -> Ast.ordi -> Ast.ordi -> bool
val eq_ord_wit : Ast.ordi list -> Ast.ord_wit -> Ast.ord_wit -> bool
val leq_ordi : Ast.ordi list -> Ast.ordi -> Ast.ordi -> bool
val less_ordi : Ast.ordi list -> Ast.ordi -> Ast.ordi -> bool
val less_opt_ordi : Ast.ordi list -> Ast.ordi -> (Ast.ordi Ast.from_ordis option * Ast.ordi Ast.from_ordis option) -> Ast.ordi array -> bool

Searching functions

val assoc_ordi : Ast.ordi -> (Ast.ordi * 'a) list -> 'a
val assoc_kind : Ast.kind -> (Ast.kind * 'a) list -> 'a
val assoc_term : Ast.term -> (Ast.term * 'a) list -> 'a
val assoc_kkind : (Ast.kind, Ast.kind) LibTools.Bindlib.binder -> ((Ast.kind, Ast.kind) LibTools.Bindlib.binder * 'a) list -> 'a