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 =

| TType
| Prop
| Term
| Rat
| Int
| Real

val pp_builtin : builtin CCFormat.printer

val builtin_conv : builtin -> Builtin.t

type view = private

| Builtin of builtin
| Var of t HVar.t
| DB of int
| App of ID.t * t list
(*
parametrized type
*)
| Fun of t list * t
(*
Function type (left to right, no left-nesting)
*)
| Forall of t
(*
explicit quantification using De Bruijn index
*)

val view : t -> view

Type-centric view of the head of this type.

raises Assert_failure
if the argument is not a 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 =

| Def_unin of int
| 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

raises Not_found
if not a proper constant

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 =

| Arity of int * int
| 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.

raises ApplyError
if the types do not match

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.

raises ApplyError
if types do not match

raises Assert_failure
if the arguments are not proper types

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 pp : t CCFormat.printer

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

val pp_in : Output_format.t -> t CCFormat.printer

Conversions

module Conv : sig ... end

Install

Dune Dependency

Authors

Maintainers

Sources

doc/logtk/Logtk/Type/index.html

Module `Logtk.Type`

Types

Main Type representation

Constructors

Definition

Containers

Utils

IO

TPTP-specific printer and types

Conversions

package logtk

Install

Dune Dependency

Authors

Maintainers

Sources

doc/logtk/Logtk/Type/index.html

Module Logtk.Type

Types

Main Type representation

Constructors

Definition

Containers

Utils

IO

TPTP-specific printer and types

Conversions

Module `Logtk.Type`