sig
type pos = Lexing.position * Lexing.position
val print_single_pos : Lexing.position -> string
val print_pos : ?prefix:string -> pos -> string
type variance = Lang_types.variance = Covariant | Contravariant | Invariant
type ground = Lang_types.ground = Unit | Bool | Int | String | Float
val print_ground : ground -> string
type constr =
Lang_types.constr =
Num
| Ord
| Getter of ground
| Dtools
| Arity_fixed
| Arity_any
type constraints = constr list
val print_constr : constr -> string
type t =
Lang_types.t = {
pos : pos option;
mutable level : int;
mutable descr : descr;
}
and constructed =
Lang_types.constructed = {
name : string;
params : (variance * t) list;
}
and descr =
Lang_types.descr =
Constr of constructed
| Ground of ground
| List of t
| Product of t * t
| Zero
| Succ of t
| Variable
| Arrow of (bool * string * t) list * t
| EVar of int * constraints
| Link of t
val make : ?pos:pos option -> ?level:int -> descr -> t
val dummy : t
val pp_type : Format.formatter -> t -> unit
val pp_type_generalized :
(int * constraints) list -> Format.formatter -> t -> unit
val print : ?generalized:(int * constraints) list -> t -> string
val doc_of_type : generalized:(int * constraints) list -> t -> Doc.item
exception Occur_check of t * t
val occur_check : t -> t -> unit
exception Unsatisfied_constraint of constr * t
val bind : t -> t -> unit
val deref : t -> t
val filter_vars : (t -> bool) -> t -> (int * constraints) list
val copy_with : ((int * constraints) * t) list -> t -> t
val instantiate :
level:int -> generalized:(int * constraints) list -> t -> t
val generalizable : level:int -> t -> (int * constraints) list
type explanation = Lang_types.explanation
exception Type_Error of explanation
val print_type_error : explanation -> unit
val ( <: ) : t -> t -> unit
val ( >: ) : t -> t -> unit
val fresh : constraints:constraints -> level:int -> pos:pos option -> t
val fresh_evar : level:int -> pos:pos option -> t
val iter_constr : (bool -> constructed -> unit) -> t -> bool * bool
end