Up  Next

Module InnerTerm

module InnerTerm: sig .. end

Scoped 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, FOTerm, ...

type t
Abstract type of term
type term = t 
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
*) 
val view : t -> view
View on the term's head form
type type_result =
| NoType
| HasType of t 
val ty : t -> type_result
Type of the term, if any
val ty_exn : t -> t
Same as InnerTerm.ty, but fails if the term has no type
Raises Invalid_argument if the type is NoType
include Interfaces.HASH
include Interfaces.ORD
val same_l : t list -> t list -> bool

Constructors

Some constructors, such as record, may raise InnerTerm.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 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 hashcons_stats : unit -> int * int * int * int * int * int

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.

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

IO


val print_hashconsing_ids : bool Pervasives.ref
if enabled, every term will be printed with its unique ID
include Interfaces.PRINT
include Interfaces.PRINT_DE_BRUIJN
val add_default_hook : print_hook -> unit
Add a print hook that will be used from now on
val debugf : t CCFormat.printer