package logtk

  1. Overview
  2. Docs
package logtk
Legend:
Library
Module
Module type
Parameter
Class
Class type

LogtkType Inference

This module is used for two things that overlap:

  • inferring the types of symbols that have not been declared (e.g. in "fof" or "cnf" TPTP statements) so as to enrich a Logtk.LogtkSignature.t
  • converting untyped terms or formulas into typed formulas, by inferring the exact type of each subterm (and possibly inferring type parameters).

In this context, generalizing type variables means that if some symbol whose type was unknown and its type still contains variables after the type inference, those variables are quantified instead of being bound to a default type (typically Logtk.LogtkType.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).

  • If we generalize, we declare that f : list(A) -> list(A) (for all A).
  • If we don't, we declare that f : list($i) -> list($i).

Here we use a single scope when we unify and substitute type variables, the scope 0.

Many functions will use an Error monad to make errors explicit. The error type is or_error. The module CCError in containers can be used to deal with errors (including monadic operators).

type 'a or_error = [
  1. | `Error of string
  2. | `Ok of 'a
]

Default LogtkTypes

type default_types = {
  1. default_i : LogtkType.t;
  2. default_prop : LogtkType.t;
  3. default_int : LogtkType.t;
  4. default_rat : LogtkType.t;
}
val tptp_default : default_types

Default TPTP types for ints, rats, etc.

Typing context

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

Closures

A closure is a function that returns a 'a value if provided with a proper type inference context. It is useful to delay the translation from untyped terms to typed terms, because locally we don't have applied all the type constraints resulting from the context yet. Therefore, when inferring the type of a subterm, we apply local constraints, and return a closure that, given the final environment, converts the subterm into a typed term.

For instance, if we infer the type of nil in the terms cons(1, nil) and cons("foo", nil), we can't infer the most specialized type for nil unless we also take its context (cons(_,_)) into account. The same closure will therefore be used to build nil:$int and nil:$string respectively.

module Closure : sig ... end

Hindley-Milner LogtkType Inference

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.

module type S = sig ... end
val map_error_seq : ('a -> 'b or_error) -> 'a Sequence.t -> 'b Sequence.t or_error

map_error_seq f seq maps f over the sequence seq, and returns the (persistent) sequence of result if all calls to f succeed. Otherwise it returns the first encountered error.

module FO : sig ... end
module HO : sig ... end