module TypeInference:sig
..end
This module is used for two things that overlap:
Signature
.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)
.
f : list(A) -> list(A)
(for all A
).f : list($i) -> list($i)
.
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 ]
typetype_ =
TypedSTerm.t
typeuntyped =
STerm.t
typetyped =
TypedSTerm.t
typeloc =
ParseLocation.t
exception Error of string
val section : Util.Section.t
module TyBuiltin:sig
..end
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
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_
TypeInference.untyped
.val infer_ty : Ctx.t ->
untyped -> type_ or_error
TypeInference.untyped
.val infer_exn : Ctx.t -> untyped -> typed
Error
if the types are inconsistentval infer : Ctx.t ->
untyped -> typed or_error
TypeInference.infer_exn
. It returns `Error s
rather
than raising TypeInference.Error
if the typechecking fails.val infer_prop_exn : Ctx.t -> untyped -> typed
val infer_clause_exn : Ctx.t -> untyped list -> typed list
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
Error
if an inconsistency is detectedval constrain_term_type_exn : ?loc:loc ->
Ctx.t -> untyped -> type_ -> unit
Error
if an inconsistency is detectedval constrain_term_term : ?loc:loc ->
Ctx.t ->
untyped -> untyped -> unit or_error
TypeInference.constrain_term_term_exn
val constrain_term_type : ?loc:loc ->
Ctx.t ->
untyped -> type_ -> unit or_error
TypeInference.constrain_term_type_exn
typetyped_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
val infer_statements : ?ctx:Ctx.t ->
UntypedAST.statement Sequence.t ->
typed_statement CCVector.ro_vector or_error