package logtk

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

LogtkTypes

Main LogtkType representation

LogtkTypes are represented using LogtkScopedTerm, with kind LogtkType. Therefore, they are hashconsed and scoped.

Common representation of types, including higher-order and polymorphic types. All type variables are assumed to be universally quantified in the outermost possible scope (outside any other quantifier).

See LogtkTypeInference for inferring types from terms and formulas, and LogtkSignature to associate types with symbols.

TODO: think of a good way of representating AC operators (+, ...)

exception Error of string

Generic error on types.

Main signature

type symbol = LogtkSymbol.t
type t = private LogtkScopedTerm.t

LogtkType is a subtype of the general structure LogtkScopedTerm.t, with explicit conversion

type ty = t
type view = private
  1. | Var of int
    (*

    LogtkType variable

    *)
  2. | BVar of int
    (*

    Bound variable (De Bruijn index)

    *)
  3. | App of symbol * t list
    (*

    parametrized type

    *)
  4. | Fun of t * t
    (*

    Function type (left to right)

    *)
  5. | Record of (string * t) list * t option
    (*

    Record type

    *)
  6. | Forall of t
    (*

    explicit quantification using De Bruijn index

    *)
val view : t -> view

LogtkType-centric view of the head of this type.

  • raises Invalid_argument

    if the argument is not a type.

include LogtkInterfaces.HASH with type t := t
include LogtkInterfaces.EQ with type t := t
val eq : t -> t -> bool
val hash_fun : t CCHash.hash_fun
val hash : t -> int
include LogtkInterfaces.ORD with type t := t
val cmp : t -> t -> int
val is_var : t -> bool
val is_bvar : t -> bool
val is_app : t -> bool
val is_fun : t -> bool
val is_forall : t -> bool

Constructors

val var : int -> t

Build a type variable.

val app : symbol -> t list -> t

Parametrized type

val const : symbol -> t

Constant sort

val arrow : t -> t -> t

arrow l r is the type l -> r.

val arrow_list : t list -> t -> t

n-ary version of arrow

val forall : t list -> t -> t

forall vars ty quantifies ty over vars. If vars is the empty list, returns ty.

  • raises Invalid_argument

    if some element of vars is not a variable

val record : (string * t) list -> rest:t option -> t

Record type, with an optional extension

val __forall : t -> t

not documented.

val __bvar : int -> t

not documented.

val (@@) : symbol -> t list -> t

s @@ args applies the sort s to arguments args.

val (<==) : t -> t list -> t

General function type. x <== l is the same as x if l is empty. Invariant: the return type is never a function type.

val (<=.) : t -> t -> t

Unary function type. x <=. y is the same as x <== [y].

val multiset : t -> t

LogtkType of multiset

val of_term : LogtkScopedTerm.t -> t option

Conversion from a term, if structure matches

val of_term_exn : LogtkScopedTerm.t -> t

Same as of_term, but without option

  • raises Invalid_argument

    if the term is not a type

val is_type : LogtkScopedTerm.t -> bool

Is the term a representation of a type?

Containers

module Set : Sequence.Set.S with type elt = t
module Map : Sequence.Map.S with type key = t
module Tbl : Hashtbl.S with type key = t
module Seq : sig ... end

LogtkUtils

val vars_set : Set.t -> t -> Set.t

Add the free variables to the given set

val vars : t -> t list

List of free variables (Var)

val close_forall : t -> t

bind free variables

type arity_result =
  1. | Arity of int * int
  2. | NoArity
val arity : t -> arity_result

Number of arguments the type expects. If arity ty returns Arity (a, b) that means that it expects a arguments to be used as arguments of Forall, and b arguments to be used for function application. If it returns NoArity then the arity is unknown (variable)

val expected_args : t -> t list

LogtkTypes expected as function argument by ty. The length of the list expected_args ty is the same as snd (arity ty).

val is_ground : t -> bool

Is the type ground? (means that no Var not BVar occurs in it)

val size : t -> int

Size of type, in number of "nodes"

val depth : t -> int

Depth of the type (length of the longest path to some leaf)

  • since 0.5.3
val open_fun : t -> t list * t

open_fun ty "unrolls" function arrows from the left, so that open_fun (a -> (b -> (c -> d))) returns [a;b;c], d.

  • returns

    the return type and the list of all its arguments

val apply : t -> t -> t

Given a function/forall type, and an argument, return the type that results from applying the function/forall to the arguments. No unification is done, types must check exactly.

  • raises Error

    if the types do not match

val apply_list : t -> t list -> t

List version of apply

  • raises Error

    if the types do not match

IO

include LogtkInterfaces.PRINT_DE_BRUIJN with type term := t and type t := t
type print_hook = int -> (Buffer.t -> t -> unit) -> Buffer.t -> t -> bool

User-provided hook that can be used to print terms (for composite cases) before the default printing occurs. The int argument is the De Bruijn depth in the term. A hook takes as arguments the depth and the recursive printing function that it can use to print subterms. A hook should return true if it fired, false to fall back on the default printing.

val pp_depth : ?hooks:print_hook list -> int -> Buffer.t -> t -> unit
include LogtkInterfaces.PRINT with type t := t
val pp : Buffer.t -> t -> unit
val to_string : t -> string
val fmt : Format.formatter -> t -> unit
val pp_surrounded : Buffer.t -> t -> unit

TPTP

specific printer and types

module TPTP : sig ... end

Conversions

module Conv : sig ... end

Misc

val fresh_var : unit -> t

Fresh var, with negative index