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