Module Logtk.InnerTerm

Inner Terms

type t = private {
term : view;
ty : type_result;
mutable id : int;
mutable payload : exn;
}

Abstract type of term

type view = private
| Var of t HVar.t

Free variable

| DB of int
| Bind of Binder.t * t * t

Type, sub-term

| Const of ID.t

Constant

| App of t * t list

Uncurried application

| AppBuiltin of Builtin.t * t list

For representing special constructors

type type_result =
| NoType
| HasType of t
type term = t
val view : t -> view

View on the term's head form

val ty : t -> type_result

Type of the term, if any

val ty_exn : t -> t

Same as ty, but fails if the term has no type

raises Invalid_argument

if the type is NoType

include Interfaces.HASH with type t := t
include Interfaces.EQ
type t
val equal : t -> t -> bool
val hash : t -> int
include Interfaces.ORD with type t := t
type t
val compare : t -> t -> int
val hash_mod_alpha : t -> int

Hash invariant w.r.t variable renaming

val same_l : t list -> t list -> bool

Physical equality on lists of terms, roughly the same as List.forall2 (==)

Constructors

Some constructors, such as record, may raise IllFormedTermif the arguments are ill-formed (several occurrences of a key), or, for variables, if the number is negative

exception IllFormedTerm of string
type nat = int
val const : ty:t -> ID.t -> t
val app : ty:t -> t -> t list -> t
val bind : ty:t -> varty:t -> Binder.t -> t -> t
val var : t HVar.t -> t
val bvar : ty:t -> nat -> t
val app_builtin : ty:t -> Builtin.t -> t list -> t
val builtin : ty:t -> Builtin.t -> t
val tType : t

The root of the type system. It doesn't have a type. It has kind Kind.Type

val arrow : t list -> t -> t

Smart constructor for arrow types

val cast : ty:t -> t -> t

Change the type

val is_var : t -> bool
val is_bvar : t -> bool
val is_const : t -> bool
val is_bind : t -> bool
val is_app : t -> bool
val is_tType : t -> bool
val is_lambda : t -> bool
val hashcons_stats : unit -> int * int * int * int * int * int

Payload

exception No_payload
val payload : t -> exn
val set_payload : t -> exn -> unit

Set payload.

raises Invalid_argument

if there is already a payload

val set_payload_erase : t -> exn -> unit

Set payload, ignoring the previous payload.

Containers

module Map : CCMap.S with type Map.key = term
module Set : CCSet.S with type Set.elt = term
module Tbl : CCHashtbl.S with type Tbl.key = term
module VarMap : CCMap.S with type VarMap.key = t HVar.t
module VarSet : CCSet.S with type VarSet.elt = t HVar.t
module VarTbl : CCHashtbl.S with type VarTbl.key = t HVar.t

De Bruijn indices handling

module DB : sig ... end

Iterators

module Seq : sig ... end

Positions

module Pos : sig ... end
val replace : t -> old:t -> by:t -> t

replace t ~old ~by syntactically replaces all occurrences of old in t by the term by.

val replace_m : t -> t Map.t -> t

Simultaneous replacement of every a->b in the map

Variables

val bind_vars : ty:t -> Binder.t -> t HVar.t list -> t -> t

bind_vars ~ty b vars t binds each v in vars with the binder b, with body t, and each intermediate result has type ty (not suitable for functions)

val close_vars : ty:t -> Binder.t -> t -> t

Close all free variables of the term using the binding symbol

val fun_ : t -> t -> t
val fun_l : t list -> t -> t
val fun_of_fvars : t HVar.t list -> t -> t

Build a function from a list of free vars + the body. This performs the De Bruijn transformation, and shifts the body.

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 open_poly_fun : t -> int * t list * t

open_poly_fun ty "unrolls" polymorphic function arrows from the left, so that open_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 expected_ty_vars : t -> int
returns

the number of type variables that a type requires.

val open_bind : Binder.t -> t -> t list * t
val open_bind_fresh : Binder.t -> t -> t HVar.t list * t

open_bind_fresh λ (λxy. F) returns [v1,v2], F[v1/x,v2/y] where v1 and v2 are fresh variables using HVar.fresh

val open_bind_fresh2 : ?⁠eq_ty:(t -> t -> bool) -> Binder.t -> t -> t -> t HVar.t list * t * t

open_bind_free2 λ (λxy. F) (λxyz. G) returns [v1,v2], F[v1/x,v2/y], λz.G[v1/x,v2/y] where v1 and v2 are fresh variables using HVar.fresh

parameter eq_ty

checks whether type of bound variables are compatible

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 open_poly_fun : t -> int * t list * t

open_poly_fun ty "unrolls" polymorphic function arrows from the left, so that open_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_bind : Binder.t -> t -> t list * t
val open_bind2 : Binder.t -> t -> t -> t list * t * t list * t
val mk_fun : ty_l:t list -> t -> t

mk_fun ~ty_l body closes over body for DB indices of type ty_l

val is_ground : t -> bool

true if the term contains no free variables

Misc

val size : t -> int
val depth : t -> int
val head : t -> ID.t option

Head symbol, or None if the term is a (bound) variable

val type_is_unifiable : t -> bool

Can we (syntactically) unify terms of this type?

val type_non_unifiable_tags : t -> Builtin.Tag.t list

Theory tags that justify this type not being unifiable

val type_is_prop : t -> bool

Is is equal to prop

val is_a_type : t -> bool

Is this a type? (i.e. its type is tType)

val as_app : t -> t * t list

as_app t decomposes t into a head (non-application) and arguments, such as (let f,l = as_app t in app f l) = t

val as_var : t -> t HVar.t option
val as_var_exn : t -> t HVar.t
val as_bvar_exn : t -> int
val is_bvar_i : int -> t -> bool

is_bvar_i n t is true iff t = bvar i

IO

val print_hashconsing_ids : bool Pervasives.ref

if enabled, every term will be printed with its unique ID

val print_all_types : bool Pervasives.ref

if enabled, print all types

val show_type_arguments : bool Pervasives.ref

Parameter for printing/hiding type arguments in terms

include Interfaces.PRINT with type t := t
type t
val pp : t CCFormat.printer
val to_string : t -> string
include Interfaces.PRINT_DE_BRUIJN with type t := t and type term := t
type t
type term
type print_hook = int -> term CCFormat.printer -> 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
val pp_var : t HVar.t CCFormat.printer
val add_default_hook : print_hook -> unit

Add a print hook that will be used from now on

val default_hooks : unit -> print_hook list
val debugf : t CCFormat.printer
val pp_zf : t CCFormat.printer
val pp_in : Output_format.t -> t CCFormat.printer