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 Logtk.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 -> Logtk.Builtin.t
type view = private
| Builtin of builtin
| Var of t Logtk.HVar.t
| DB of int
| App of Logtk.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 Logtk.Interfaces.HASH with type t := t
include Logtk.Interfaces.EQ
type t
val equal : t -> t -> bool
val hash : t -> int
include Logtk.Interfaces.ORD with type t := t
type 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 Logtk.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 Logtk.HVar.t -> t
val var_of_int : int -> t

Build a type variable.

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

Parametrized type

val builtin : builtin -> t
val const : Logtk.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 Logtk.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 : Logtk.InnerTerm.t -> t

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

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

Definition

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

Access the definition of a type

val def_exn : Logtk.ID.t -> def

Unsafe version of def

raises Not_found

if not a proper constant

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

Set definition of an ID

Containers

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

Utils

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

Add the free variables to the given set

val vars : t -> t Logtk.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 -> Logtk.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 Logtk.Interfaces.PRINT_DE_BRUIJN with type term := t and type t := t
type t
type term
type print_hook = int -> term CCFormat.printer -> Stdlib.Format.formatter -> term -> 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 Logtk.Interfaces.PRINT with type t := t
type t
val pp : t CCFormat.printer
val to_string : t -> string
val pp_surrounded : t CCFormat.printer
val pp_typed_var : t Logtk.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 : Logtk.Output_format.t -> t CCFormat.printer

Conversions

module Conv : sig ... end