package logtk

  1. Overview
  2. Docs
package logtk
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Logtk.InnerTermSource

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.

Sourcemodule I = Int32
Sourcetype 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

Sourceand 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

    *)
Sourceand type_result =
  1. | NoType
  2. | HasType of t
Sourcetype term = t
Sourceval view : t -> view

View on the term's head form

Sourceval ty : t -> type_result

Type of the term, if any

Sourceval 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
Sourceval equal : t -> t -> bool
Sourceval hash : t -> int
include Interfaces.ORD with type t := t
Sourceval compare : t -> t -> int
Sourceval hash_mod_alpha : t -> int

Hash invariant w.r.t variable renaming

Sourceval same_l : t list -> t list -> bool

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

Sourceval same_l_gen : t list -> t list -> bool

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

Sourceval 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

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

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

Sourceval arrow : t list -> t -> t

Smart constructor for arrow types

Sourceval cast : ty:t -> t -> t

Change the type

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

Payload

Sourceexception No_payload
Sourceval payload : t -> exn
Sourceval set_payload : t -> exn -> unit

Set payload.

Sourceval set_payload_erase : t -> exn -> unit

Set payload, ignoring the previous payload.

Containers

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

De Bruijn indices handling

Sourcemodule DB : sig ... end

Iterators

Sourcemodule Seq : sig ... end

Positions

Sourcemodule Pos : sig ... end
Sourceval replace : t -> old:t -> by:t -> t

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

Sourceval replace_m : t -> t Map.t -> t

Simultaneous replacement of every a->b in the map

Variables

Sourceval 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)

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

Close all free variables of the term using the binding symbol

Sourceval fun_ : t -> t -> t
Sourceval fun_l : t list -> t -> t
Sourceval 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.

Sourceval expected_ty_vars : t -> int
  • returns

    the number of type variables that a type requires.

Sourceval 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

Sourceval 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

Sourceval 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

Sourceval 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

Sourceval open_bind : Binder.t -> t -> t list * t
Sourceval open_bind2 : Binder.t -> t -> t -> t list * t * t list * t
Sourceval mk_fun : ty_l:t list -> t -> t

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

Sourceval is_ground : t -> bool

true if the term contains no free variables

Misc

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

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

Sourceval type_is_unifiable : t -> bool

Can we (syntactically) unify terms of this type?

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

Theory tags that justify this type not being unifiable

Sourceval type_is_prop : t -> bool

Is is equal to prop

Sourceval is_a_type : t -> bool

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

Sourceval 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

Sourceval as_var : t -> t HVar.t option
Sourceval as_var_exn : t -> t HVar.t
Sourceval as_const : t -> ID.t option
Sourceval as_const_exn : t -> ID.t
Sourceval as_bvar_exn : t -> int
Sourceval is_bvar_i : int -> t -> bool

is_bvar_i n t is true iff t = bvar i

IO

Sourceval print_hashconsing_ids : bool ref

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

Sourceval print_all_types : bool ref

if enabled, print all types

Sourceval show_type_arguments : bool ref

Parameter for printing/hiding type arguments in terms

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

Sourceval pp_depth : ?hooks:print_hook list -> int -> t CCFormat.printer
Sourceval add_default_hook : print_hook -> unit

Add a print hook that will be used from now on

Sourceval default_hooks : unit -> print_hook list