Module type LogtkTypeInference.S

module type S = sig .. end

type untyped 
untyped term
type typed 
typed term
val infer_exn : LogtkTypeInference.Ctx.t ->
untyped ->
LogtkType.t * typed LogtkTypeInference.Closure.t
Infer the type of this term under the given signature. This updates the context's typing environment!
Raises LogtkType.Error if the types are inconsistent
Returns the inferred type of the untyped term (possibly a type var) along with a closure to produce a typed term once every constraint has been solved
val infer : LogtkTypeInference.Ctx.t ->
untyped ->
(LogtkType.t * typed LogtkTypeInference.Closure.t)
Safe version of LogtkTypeInference.S.infer_exn. It returns `Error s rather than raising LogtkType.Error if the typechecking fails.

Constraining types

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

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