Module MiniTypes (.ml)

module MiniTypes: sig .. end

This module transforms types from the user's syntax to the internal representation of the inference engine.

val extract_type : MiniAst.expression -> MiniAst.typ * MiniAst.expression

extract_type examines an expression and looks for a sufficiently explicit type annotation. If it finds one, it returns the type annotation, together with the expression (deprived of its annotation). Otherwise, it raises Not_found.

type recursive_value_definition_kind =

`\|`	`Implicit of MiniAst.name * MiniAst.expression`
`\|`	`Explicit of MiniAst.name * MiniAst.typ * MiniAst.expression`
`\|`	`NotPVar`

recursive_value_definition_kind tests if a recursive definition is annotated or not.

val explicit_or_implicit : MiniAst.pattern ->
       MiniAst.expression -> recursive_value_definition_kind

explicit_or_implicit p e tests if a definition is annotated or not and normalizes it such that type constraint can be found at the top of the term. For instance: \(x:int). (x : int) is normalized into (\x.x : int -> int).

val variables_of_typ : MiniAst.typ -> Misc.StringSet.t

variables_of_typ ty returns the type variables of ty.

val arrow : MiniTypingEnvironment.environment ->
       Constraint.variable CoreAlgebra.arterm ->
       Constraint.variable CoreAlgebra.arterm ->
       Constraint.variable CoreAlgebra.arterm

arrow env x1 x2 builds the internal representation of the type x1 -> x2.

val arity : MiniAst.typ -> int

arity (t1 -> ... -> tn) returns n.

val tycon : MiniTypingEnvironment.environment ->
       MultiEquation.tname ->
       Constraint.variable CoreAlgebra.arterm list ->
       Constraint.variable CoreAlgebra.arterm

tycon t xs builds the internal representation of the type t xs.

val intern : Positions.position ->
       MiniTypingEnvironment.environment -> MiniAst.typ -> Constraint.crterm

intern env ty converts ty into its internal representation.

val intern_let_env : Positions.position ->
       MiniTypingEnvironment.environment ->
       MultiEquation.tname list ->
       MultiEquation.tname list ->
       Constraint.variable list * Constraint.variable list *
       MiniTypingEnvironment.environment

internal_let_env env fqs rqs internalizes the flexible variables fqs and the rigid variables rqs into env.

val intern_scheme : Positions.position ->
       MiniTypingEnvironment.environment ->
       string ->
       MultiEquation.tname list ->
       MiniAst.typ -> (Constraint.crterm, Constraint.variable) Constraint.scheme

intern_scheme env x fqs ty returns the internal representation of the type scheme forall fqs.ty and the binding of x to it.