Module LogtkTypeInference.Ctx

module Ctx: sig .. end

type t 
val create : ?default:LogtkTypeInference.default_types ->
LogtkSignature.t -> t
New context with a signature and default types.
default : which types are inferred by default (if not provided then LogtkTypeInference.tptp_default will be used)
val clear : t -> unit
Reset totally the context
val copy : t -> t
Copy of the context
val exit_scope : t -> unit
Exit the current scope (formula, clause), meaning that all free variables' types are forgotten.
val add_signature : t -> LogtkSignature.t -> unit
Specify the type of some symbols
val declare : t -> LogtkSymbol.t -> LogtkType.t -> unit
Declare the type of a symbol. The type must be equal to the current type of the symbol, if any.
Raises LogtkType.Error if an inconsistency (with inferred types) is detected.
val ty_of_prolog : t -> LogtkPrologTerm.t -> LogtkType.t option
LogtkType conversion from LogtkPrologTerm
val bind_to_default : t -> unit
Free constructor variables are bound to the default type provided at creation of the context.
val generalize : t -> unit
Free constructor variables will be generalized, i.e., kept as variables
val to_signature : t -> LogtkSignature.t
Obtain the type of all symbols whose type has been inferred. If some instantiated variables remain, they are bound to the context's default parameter.
val constrain_type_type : t -> LogtkType.t -> LogtkType.t -> unit
Constrain the two types to be equal
Raises LogtkType.Error if it is not possible