Previous  Up  Next

Module Lang_types


module Lang_types: sig .. end
Positions
type pos = Lexing.position * Lexing.position 
val print_single_pos : Lexing.position -> string
val print_pos : ?prefix:string -> pos -> string

type variance =
| Covariant
| Contravariant
| Invariant

type ground =
| Unit
| Bool
| Int
| String
| Float 
val print_ground : ground -> string

type constr =
| Num
| Ord
| Getter of ground
| Dtools
| Arity_fixed
| Arity_any 
type constraints = constr list 
val print_constr : constr -> string

type t = {
   pos : pos option;
   mutable level : int;
   mutable descr : descr;
}
Every type gets a level annotation. This is useful in order to know what can or cannot be generalized: you need to compare the level of an abstraction and those of a ref or source.

type constructed = {
   name : string;
   params : (variance * t) list;
}
type 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
These two exceptions can be raised when attempting to assign a variable.
val occur_check : t -> t -> unit
Check that a (a dereferenced type variable) does not occur in b, and prepare the instantiation a<-b by adjusting the levels.
exception Unsatisfied_constraint of constr * t
val bind : t -> t -> unit
val deref : t -> t
Dereferencing gives you the meaning of a term, going through links created by instantiations. One should (almost) never work on a non-dereferenced type.
val filter_vars : (t -> bool) -> t -> (int * constraints) list
val copy_with : ((int * constraints) * t) list ->
       t -> t
Copy a term, substituting some EVars as indicated by a list of associations. Other EVars are not copied, so sharing is preserved.
val instantiate : level:int ->
       generalized:(int * constraints) list ->
       t -> t
Instantiate a type scheme, given as a type together with a list of generalized variables. Fresh variables are created with the given (current) level, and attached to the appropriate constraints. This erases position information, since they usually become irrelevant.
val generalizable : level:int -> t -> (int * constraints) list
Return a list of generalizable variables in a type. This is performed after type inference on the left-hand side of a let-in, with level being the level of that let-in. Uses the simple method of ML, to be associated with a value restriction.
type 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
Simplified version of existential variable generation, without constraints. This is used when parsing to annotate the AST.
val fresh_evar : level:int -> pos:pos option -> t
val iter_constr : (bool -> constructed -> unit) -> t -> bool * bool
Iterate over all constructed types, giving info about their positivity, and return true if there is a var, because it might be instantiated by a ground type later.