Previous  Up  Next

Module TypeInference

module TypeInference: sig .. end

Type Inference

This module is used for two things that overlap:

In this context, generalizing type variables means that if some ID.t whose type was unknown and its type still contains variables after the type inference, those variables are quantified instead of being bound to a default type (typically .Type.i).

For instance: say f is not declared and occurs in the term f(f(nil)) with the declared constructor nil : list(A). The inferred type for f should be something like list(B) -> list(B).

Here we use a single scope when we unify and substitute type variables, the scope 0.

Many functions will use an Error monad to make errors explicit. The error type is TypeInference.or_error. The module CCError in containers can be used to deal with errors (including monadic operators).

type 'a or_error = [ `Error of string | `Ok of 'a ] 
type type_ = TypedSTerm.t 
type untyped = STerm.t
untyped term
type typed = TypedSTerm.t
typed term
type loc = ParseLocation.t 
exception Error of string
val section : Util.Section.t

Types for Builtins


module TyBuiltin: sig .. end

Typing context

This module provides a typing context, with an applicative interface. The context is used to map terms to types locally during type inference. It also keeps and updates a signature when symbols' types are inferred.

This module is quite low-level, and shouldn't be used in simple cases (see the following modules)

module Ctx: sig .. end
val unify : ?loc:loc -> type_ -> type_ -> unit

Hindley-Milner Type Inference

This module, abstract in the exact kind of term it types, takes as input a signature and an untyped term, and updates the typing context so that the untyped term can be converted into a typed term.

val infer_ty_exn : Ctx.t -> untyped -> type_
Type conversion from TypeInference.untyped.
val infer_ty : Ctx.t ->
       untyped -> type_ or_error
Type conversion from TypeInference.untyped.
val infer_exn : Ctx.t -> untyped -> typed
Infer the type of this term under the given signature. This updates the context's typing environment!
Raises Error if the types are inconsistent
val infer : Ctx.t ->
       untyped -> typed or_error
Safe version of TypeInference.infer_exn. It returns `Error s rather than raising TypeInference.Error if the typechecking fails.
val infer_prop_exn : Ctx.t -> untyped -> typed
Same as TypeInference.infer_exn but forces the type of its result to be TypedSTerm.prop
val infer_clause_exn : Ctx.t -> untyped list -> typed list
Convert a clause. Free variables in each of the list's elements are shared

Constraining types

This section is mostly useful for inferring a signature without converting untyped_terms into typed_terms.

val constrain_term_term_exn : ?loc:loc ->
       Ctx.t -> untyped -> untyped -> unit
Force the two terms to have the same type in this context
Raises Error if an inconsistency is detected
val constrain_term_type_exn : ?loc:loc ->
       Ctx.t -> untyped -> type_ -> unit
Force the term's type and the given type to be the same.
Raises Error if an inconsistency is detected
val constrain_term_term : ?loc:loc ->
       Ctx.t ->
       untyped -> untyped -> unit or_error
Safe version of TypeInference.constrain_term_term_exn
val constrain_term_type : ?loc:loc ->
       Ctx.t ->
       untyped -> type_ -> unit or_error
Safe version of TypeInference.constrain_term_type_exn

Statements


type typed_statement = (typed, typed, type_,
        UntypedAST.attrs)
       Statement.t 
val infer_statement_exn : Ctx.t ->
       UntypedAST.statement ->
       typed_statement * typed_statement list
infer_statement ctx ~f st checks and convert st into a typed statements, and a list of auxiliary type declarations for symbols that were inferred implicitely.
val infer_statements_exn : ?ctx:Ctx.t ->
       UntypedAST.statement Sequence.t ->
       typed_statement CCVector.ro_vector
Infer all statements
val infer_statements : ?ctx:Ctx.t ->
       UntypedAST.statement Sequence.t ->
       typed_statement CCVector.ro_vector or_error