package logtk

  1. Overview
  2. Docs
Core types and algorithms for logic

Install 

dune-project
 Dependency

github.com Readme Changelog Edit opam file Versions (4)

Authors

  1. S
    Simon Cruanes
  2. P
    Petar Vukmirovic
  3. A
    Alexander Bentkamp
  4. S
    Sophie Tourret
  5. V
    Visa Nummelin

Maintainers

  1. S
    simon.cruanes.2.17@m4x.org

Sources

2.1.tar.gz
md5=e72de75e9f0f87da9e6e8c0a4d4c89f9
sha512=81becfc9badd686ab3692cd9312172aa4c4e3581b110e81770bb01e0ffbc1eb8495d0dd6d43b98f3d06e6b8c8a338174c13ebafb4e9849a3ddf89f9a3a72c287

doc/logtk/Logtk/Type/index.html

Module Logtk.Type

Types

Main Type representation

Types are represented using InnerTerm, with kind Type. 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 TypeInference for inferring types from terms and formulas, and Signature to associate types with symbols.

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

type t = private InnerTerm.t

Type is a subtype of the term structure (itself a subtype of InnerTerm.t), with explicit conversion

type ty = t
type builtin =
  1. | TType
  2. | Prop
  3. | Term
  4. | Rat
  5. | Int
  6. | Real
val pp_builtin : builtin CCFormat.printer
val builtin_conv : builtin -> Builtin.t
type view = private
  1. | Builtin of builtin
  2. | Var of t HVar.t
  3. | DB of int
  4. | App of ID.t * t list
    (*

    parametrized type

    *)
  5. | Fun of t list * t
    (*

    Function type (left to right, no left-nesting)

    *)
  6. | Forall of t
    (*

    explicit quantification using De Bruijn index

    *)
val view : t -> view

Type-centric view of the head of this type.

include Interfaces.HASH with type t := t
include Interfaces.EQ with type t := t
val equal : t -> t -> bool
val hash : t -> int
include Interfaces.ORD with type t := t
val compare : t -> t -> int
val is_tType : t -> bool
val is_var : t -> bool
val is_bvar : t -> bool
val is_app : t -> bool
val is_const : t -> bool
val is_fun : t -> bool
val is_forall : t -> bool
val is_prop : t -> bool
val as_var_exn : t -> t HVar.t
val hash_mod_alpha : t -> int

Hash invariant w.r.t variable renaming

Constructors

val tType : t
val prop : t
val term : t
val int : t
val rat : t
val real : t
val var : t HVar.t -> t
val var_of_int : int -> t

Build a type variable.

val app : ID.t -> t list -> t

Parametrized type

val builtin : builtin -> t
val const : ID.t -> t

Constant sort

val arrow : t list -> t -> t

arrow l r is the type l -> r.

val forall : t -> t

Quantify over one type variable. Careful with the De Bruijn indices!

val forall_n : int -> t -> t

Quantify over n type variable. Careful with the De Bruijn indices!

val forall_fvars : t HVar.t list -> t -> t

forall_fvars vars body makes the De Bruijn conversion before quantifying on vars

val bvar : int -> t

bound variable

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

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

val of_term_unsafe : InnerTerm.t -> t

NOTE: this can break the invariants and make view fail. Only use with caution.

val of_terms_unsafe : InnerTerm.t list -> t list
val cast_var_unsafe : InnerTerm.t HVar.t -> t HVar.t

Definition

type def =
  1. | Def_unin of int
  2. | Def_data of int * ty list
val def : ID.t -> def option

Access the definition of a type

val def_exn : ID.t -> def

Unsafe version of def

val set_def : ID.t -> def -> unit

Set definition of an ID

Containers

module Set : CCSet.S with type elt = t
module Map : CCMap.S with type key = t
module Tbl : CCHashtbl.S with type key = t
module Seq : sig ... end

Utils

module VarSet : CCSet.S with type elt = t HVar.t
module VarMap : CCMap.S with type key = t HVar.t
module VarTbl : CCHashtbl.S with type key = t HVar.t
val vars_set : VarSet.t -> t -> VarSet.t

Add the free variables to the given set

val vars : t -> t HVar.t list

List of free variables

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

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

val expected_ty_vars : t -> int

Number of type parameters expected. 0 for monomorphic types.

val needs_args : t -> bool

needs_args ty iff expected_ty_vars ty>0 || expected_args ty<>[]

val order : t -> int

Number of left-nested function types (1 for constant and variables). order (a->b) = 1 order ((a->b)->c) = 2 order (((a->b)->c)->d) = 2

val contains_prop : t -> bool
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_poly_fun : t -> int * t list * t

open_poly_fun ty "unrolls" polymorphic function arrows from the left, so that open_poly_fun (forall a b. f a -> (g b -> (c -> d))) returns 2; [f a;g b;c], d.

  • returns

    the return type, the number of type variables, and the list of all its arguments

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 returns : t -> t

returned type (going through foralls and arrows). returns a is like let _, _, ret = open_poly_fun a in ret NOTE caution, not always closed

val returns_prop : t -> bool
val returns_tType : t -> bool
exception ApplyError of string

Error raised when apply fails

val apply : t -> t list -> t

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

val apply1 : t -> t -> t

apply1 a b is short for apply a [b].

val apply_unsafe : t -> InnerTerm.t list -> t

Similar to apply, but assumes its arguments are well-formed types without more ado.

val is_unifiable : t -> bool

Are terms of this type syntactically unifiable? See InnerTerm.type_is_unifiable

IO

include Interfaces.PRINT_DE_BRUIJN with type term := t and type t := t
type print_hook = int -> t CCFormat.printer -> Format.formatter -> 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 -> t CCFormat.printer
include Interfaces.PRINT with type t := t
val to_string : t -> string
val pp_surrounded : t CCFormat.printer
val pp_typed_var : t HVar.t CCFormat.printer
val mangle : t -> string
val pp_mangle : t CCFormat.printer

TPTP-specific printer and types

module TPTP : sig ... end
module ZF : sig ... end

Conversions

module Conv : sig ... end