package logtk

  1. Overview
  2. Docs
package logtk
Legend:
Library
Module
Module type
Parameter
Class
Class type
type t
val create : ?default:default_types -> LogtkSignature.t -> t

New context with a signature and default types.

  • parameter default

    which types are inferred by default (if not provided then 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