package logtk
-
logtk
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
package logtk
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
val create : ?default:default_types -> LogtkSignature.t -> tNew context with a signature and default types.
val clear : t -> unitReset totally the context
val exit_scope : t -> unitExit the current scope (formula, clause), meaning that all free variables' types are forgotten.
val add_signature : t -> LogtkSignature.t -> unitSpecify the type of some symbols
val declare : t -> LogtkSymbol.t -> LogtkType.t -> unitDeclare the type of a symbol. The type must be equal to the current type of the symbol, if any.
val ty_of_prolog : t -> LogtkPrologTerm.t -> LogtkType.t optionLogtkType conversion from LogtkPrologTerm
val bind_to_default : t -> unitFree constructor variables are bound to the default type provided at creation of the context.
val generalize : t -> unitFree constructor variables will be generalized, i.e., kept as variables
val to_signature : t -> LogtkSignature.tObtain 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 -> unitConstrain the two types to be equal