Module Logtk.InnerTerm

Inner Terms

Those terms are not designed to be used directly, but rather to provide a generic backend (implementing De Bruijn indices, subterms, substitutions, etc.) for other more specific representations like Type.t and Term.t.

The point is that we only have to do substitution, hashconsing, and De Bruijn indices manipulation in one place; it also makes it easy to make terms and types occur in one another (types as parameters to terms, etc.)

NOTE: this should be used with a lot of caution. Few checks are performed (even typing checks) and it is easy to obtain non-closed terms or ill-typed terms by manipulating this carelessly.

module I = Int32
type t = private {
  1. term : view;
  2. ty : type_result;
  3. mutable id : int;
  4. mutable payload : exn;
  5. props : I.t;
  6. ho_weight : int lazy_t;
}

Abstract type of term

and view = private
  1. | Var of t HVar.t
    (*

    Free variable

    *)
  2. | DB of int
  3. | Bind of Binder.t * t * t
    (*

    Type, sub-term

    *)
  4. | Const of ID.t
    (*

    Constant

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

    Uncurried application

    *)
  6. | AppBuiltin of Builtin.t * t list
    (*

    For representing special constructors

    *)
and type_result =
  1. | NoType
  2. | 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

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 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(==)

val same_l_gen : t list -> t list -> bool

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

val ho_weight : t -> int

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
val is_beta_reducible : t -> bool
val has_lambda : t -> bool

Payload

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

Set payload.

val set_payload_erase : t -> exn -> unit

Set payload, ignoring the previous payload.

Containers

module Map : CCMap.S with type key = term
module Set : CCSet.S with type elt = term
module Tbl : CCHashtbl.S with type key = term
module VarMap : CCMap.S with type key = t HVar.t
module VarSet : CCSet.S with type elt = t HVar.t
module VarTbl : CCHashtbl.S with type 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 expected_ty_vars : t -> int
  • returns

    the number of type variables that a type requires.

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_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_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_const : t -> ID.t option
val as_const_exn : t -> ID.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 ref

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

val print_all_types : bool ref

if enabled, print all types

val show_type_arguments : bool ref

Parameter for printing/hiding type arguments in terms

include Interfaces.PRINT with type t := t
val to_string : t -> string
include Interfaces.PRINT_DE_BRUIJN with type t := t and type term := 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 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