module Types: sig .. end
This module provides a variety of functions for dealing with types, mostly
built on top of
DeBruijn and
TypeCore.
Convenient combinators.
Dealing with triples.
val fst3 : 'a * 'b * 'c -> 'a
val snd3 : 'a * 'b * 'c -> 'b
val thd3 : 'a * 'b * 'c -> 'c
Operators
val (!!) : TypeCore.typ -> TypeCore.var
Asserts that this type is actually a TyOpen.
val (!!=) : TypeCore.typ -> TypeCore.var
Asserts that this type is actually a TySingleton (TyOpen ...).
val ( !* ) : 'a Lazy.t -> 'a
This is Lazy.force.
val (>>=) : 'a option -> ('a -> 'b option) -> 'b option
bind for the option monad.
val (|||) : 'a option -> 'a option -> 'a option
either operator for the option monad
val (^=>) : bool -> bool -> bool
The standard implication connector, with the right associativity.
val (|>) : 'a -> ('a -> 'b) -> 'b
The pipe operator.
Manipulating types.
Building types.
val ty_unit : TypeCore.typ
val ty_tuple : TypeCore.typ list -> TypeCore.typ
val (@->) : TypeCore.typ -> TypeCore.typ -> TypeCore.typ
val ty_bar : TypeCore.typ -> TypeCore.typ -> TypeCore.typ
val ty_app : TypeCore.typ -> TypeCore.typ list -> TypeCore.typ
val ty_equals : TypeCore.var -> TypeCore.typ
Binding types
val bind_datacon_parameters : TypeCore.env ->
Kind.kind ->
TypeCore.unresolved_branch list ->
TypeCore.env * TypeCore.var list * TypeCore.unresolved_branch list
Instantiation
val instantiate_type : TypeCore.typ -> TypeCore.typ list -> TypeCore.typ
val instantiate_branch : TypeCore.unresolved_branch -> TypeCore.typ list -> TypeCore.unresolved_branch
val find_and_instantiate_branch : TypeCore.env ->
TypeCore.var -> Datacon.name -> TypeCore.typ list -> TypeCore.resolved_branch
val resolve_branch : TypeCore.var -> TypeCore.unresolved_branch -> TypeCore.resolved_branch
Folding and unfolding
val flatten_star : TypeCore.env -> TypeCore.typ -> TypeCore.typ list
val fold_star : TypeCore.typ list -> TypeCore.typ
val strip_forall : TypeCore.typ -> (TypeCore.type_binding * TypeCore.flavor) list * TypeCore.typ
val fold_forall : (TypeCore.type_binding * TypeCore.flavor) list ->
TypeCore.typ -> TypeCore.typ
val fold_exists : TypeCore.type_binding list -> TypeCore.typ -> TypeCore.typ
val expand_if_one_branch : TypeCore.env -> TypeCore.typ -> TypeCore.typ
Dealing with variables
Various getters
val get_location : TypeCore.env -> TypeCore.var -> TypeCore.location
val get_adopts_clause : TypeCore.env -> TypeCore.var -> TypeCore.typ
val get_branches : TypeCore.env -> TypeCore.var -> TypeCore.unresolved_branch list
val get_arity : TypeCore.env -> TypeCore.var -> int
val get_kind_for_type : TypeCore.env -> TypeCore.typ -> Kind.kind
val get_variance : TypeCore.env -> TypeCore.var -> TypeCore.variance list
val def_for_datacon : TypeCore.env -> TypeCore.resolved_datacon -> TypeCore.data_type_def
val def_for_branch : TypeCore.env -> TypeCore.resolved_branch -> TypeCore.data_type_def
val flavor_for_branch : TypeCore.env -> TypeCore.resolved_branch -> DataTypeFlavor.flavor
val variance : TypeCore.env -> TypeCore.var -> int -> TypeCore.variance
Get the variance of the i-th parameter of a data type.
val is_tyapp : TypeCore.typ -> (TypeCore.var * TypeCore.typ list) option
Inspecting
val is_term : TypeCore.env -> TypeCore.var -> bool
val is_perm : TypeCore.env -> TypeCore.var -> bool
val is_type : TypeCore.env -> TypeCore.var -> bool
val is_user : TypeCore.name -> bool
Miscellaneous
val fresh_auto_var : string -> TypeCore.name
val find_type_by_name : TypeCore.env -> ?mname:string -> string -> TypeCore.typ
val make_datacon_letters : TypeCore.env -> Kind.kind -> bool -> TypeCore.env * TypeCore.var list
module TypePrinter: sig .. end
Our not-so-pretty printer for types.