package logtk
Install
Dune Dependency
Authors
Maintainers
Sources
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
val pp_builtin : builtin CCFormat.printer
include Interfaces.ORD with type t := t
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 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_of_int : int -> t
Build a type variable.
forall_fvars vars body
makes the De Bruijn conversion before quantifying on vars
val bvar : int -> t
bound variable
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
Containers
module Tbl : CCHashtbl.S with type key = t
module Seq : sig ... end
Utils
module VarTbl : CCHashtbl.S with type key = t HVar.t
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)
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 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)
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
.
open_fun ty
"unrolls" function arrows from the left, so that open_fun (a -> (b -> (c -> d)))
returns [a;b;c], d
.
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
Error raised when apply
fails
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 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
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