module MiniTypingEnvironment: sig .. end
TypingEnvironment implements two mappings used during the constraint
generation.
The first one associates a kind, a flexible variable and an optional
list of data constructor to a type name.
The second one records the scheme of the data constructors.
type (MiniAst.dname * MultiEquation.variable) list
An algebraic datatype is characterized by a list of data constructors.
type MiniKindInferencer.t * MultiEquation.variable *
algebraic_datatype option Pervasives.ref
A type is characterized by a kind, a variable and an optional set of
algebraic data constructors.
type int * MultiEquation.variable list * MultiEquation.crterm
A data constructor's type is denoted by an ML scheme.
type
The type of the typing environement.
val empty_environment : environment
The empty environment.
val fold_type_info : ('a -> MiniAst.tname * type_info -> 'a) ->
'a -> environment -> 'a
fold_type_info folds over the environment focusing on type's
information.
val add_type_variables : (MiniAst.tname * type_info) list ->
environment -> environment
Add a set of type variables into the environment, associating a
name to each.
val add_type_constructor : environment ->
MiniAst.tname ->
type_info -> environment
Add a type constructor into the environment.
val add_data_constructor : environment ->
MiniAst.dname ->
data_constructor -> environment
Add a data constructor into the environment.
val is_regular_datacon_scheme : environment ->
MultiEquation.variable list -> MultiEquation.crterm -> bool
is_regular_datacon_scheme env vs ty checks that forall vs.ty is
a valid scheme for a data constructor that is to say following the
shape:
K :: forall a1 .. an. tau_1 -> ... -> tau_n -> eps a1 ... an
val lookup_datacon : ?pos:Positions.position ->
environment ->
MiniAst.dname -> data_constructor
lookup_datacon env k gives access to the typing information
related to the data constructor k in env.
val lookup_type_variable : ?pos:Positions.position ->
environment ->
MiniAst.tname -> MultiEquation.variable CoreAlgebra.arterm
Looks for a type constructor given its name.
val typcon_kind : environment -> MiniAst.tname -> MiniKindInferencer.t
Accessor to the kind of a type.
val typcon_variable : environment ->
MiniAst.tname -> MultiEquation.variable CoreAlgebra.arterm
Accessor the unification variable of a type.
val as_fun : environment ->
MiniAst.tname -> MultiEquation.variable CoreAlgebra.arterm
as_fun env provides a view of
env as function from names to
variable. This is used to abstract the environment when it is
given to the
MiniAlgebra module
(see
MiniAlgebra.type_of_primitive for instance).
val as_kind_env : environment ->
(MiniAst.tname -> MiniKindInferencer.t) *
(MiniAst.tname -> MiniKindInferencer.t -> unit)
as_kind env provides a view of env as kind environment.
val fresh_datacon_scheme : Positions.position ->
environment ->
MiniAst.dname -> MultiEquation.variable list * MultiEquation.crterm
fresh_datacon_scheme env dname vs retrieves the type scheme
of dname in env and alpha convert it using vs as a set
of names to use preferentially when printing.
val fresh_flexible_vars : Positions.position ->
environment ->
MiniAst.tname list ->
MultiEquation.variable list *
(MiniAst.tname * type_info) list
fresh_flexible_vars pos env vs returns a list of fresh flexible
variables whose visible names are vs and an environment fragment.
val fresh_rigid_vars : Positions.position ->
environment ->
MiniAst.tname list ->
MultiEquation.variable list *
(MiniAst.tname * type_info) list
fresh_flexible_vars pos env vs returns a list of fresh rigid
variables whose visible names are vs and an environment fragment.
val fresh_unnamed_rigid_vars : Positions.position ->
environment ->
'a list ->
MultiEquation.variable list * ('a * type_info) list
fresh_flexible_vars pos env returns a list of fresh rigid
variables without visible names and an environment fragment.
val add_type_and_kind_variables : (MiniAst.tname * MultiEquation.variable) list ->
environment -> environment
Merge a environment fragment with an environment.