Module Sidekick_base.Term

include module type of struct include Sidekick_core.Term end
include module type of struct include Sidekick_core_logic.Term end
type t

A term, in the calculus of constructions

The store for terms.

The store is responsible for allocating unique IDs to terms, and enforcing their hashconsing (so that syntactic equality is just a pointer comparison).

type view =
  1. | E_type of int
  2. | E_var of var
  3. | E_bound_var of bvar
  4. | E_app of t * t
  5. | E_lam of string * t * t
  6. | E_pi of string * t * t

View.

A view is the shape of the root node of a term.

include Sidekick_sigs.EQ_ORD_HASH with type t := t
include Sidekick_sigs.EQ with type t := t
val equal : t -> t -> bool
include Sidekick_sigs.ORD with type t := t
val compare : t -> t -> int
include Sidekick_sigs.HASH with type t := t
val hash : t -> int
val pp_debug : t Sidekick_util.Fmt.printer
val pp_debug_with_ids : t Sidekick_util.Fmt.printer

Containers

include Sidekick_sigs.WITH_SET_MAP_TBL with type t := t
include Sidekick_sigs.WITH_WEAK with type t := t
module Weak_set = Sidekick_core.Term.Weak_set
module Weak_map = Sidekick_core.Term.Weak_map

Utils

val view : t -> view
val unfold_app : t -> t * t list
val is_app : t -> bool
val is_const : t -> bool
val is_pi : t -> bool
val iter_dag : ?seen:unit Tbl.t -> iter_ty:bool -> f:(t -> unit) -> t -> unit

iter_dag t ~f calls f once on each subterm of t, t included. It must not traverse t as a tree, but rather as a perfectly shared DAG.

For example, in:

let x = 2 in
let y = f x x in
let z = g y x in
z = z

the DAG has the following nodes:

n1: 2
n2: f n1 n1
n3: g n2 n1
n4: = n3 n3
val iter_shallow : f:(bool -> t -> unit) -> t -> unit

iter_shallow f e iterates on immediate subterms of e, calling f trdb e' for each subterm e', with trdb = true iff e' is directly under a binder.

val map_shallow : store -> f:(bool -> t -> t) -> t -> t
val exists_shallow : f:(bool -> t -> bool) -> t -> bool
val for_all_shallow : f:(bool -> t -> bool) -> t -> bool
val contains : t -> sub:t -> bool
val free_vars_iter : t -> var Iter.t
val free_vars : ?init:Sidekick_core_logic__.Var.Set.t -> t -> Sidekick_core_logic__.Var.Set.t
val is_type : t -> bool

is_type t is true iff view t is Type _

val is_a_type : t -> bool

is_a_type t is true if is_ty (ty t)

val is_closed : t -> bool

Is the term closed (all bound variables are paired with a binder)? time: O(1)

val has_fvars : t -> bool

Does the term contain free variables? time: O(1)

val ty : t -> t

Return the type of this term.

Creation

val type_ : store -> t
val type_of_univ : store -> int -> t
val var : store -> var -> t
val var_str : store -> string -> ty:t -> t
val bvar : store -> bvar -> t
val bvar_i : store -> int -> ty:t -> t
val const : store -> Sidekick_core_logic__.Types_.const -> t
val app : store -> t -> t -> t
val app_l : store -> t -> t list -> t
val app_fold : store -> f:t -> acc0:t -> t list -> t
val lam : store -> var -> t -> t
val pi : store -> var -> t -> t
val arrow : store -> t -> t -> t
val arrow_l : store -> t list -> t -> t
val open_lambda : store -> t -> (var * t) option
val open_lambda_exn : store -> t -> var * t

De bruijn indices

include module type of struct include Sidekick_core_logic.T_builtins end
type Sidekick_core_logic__.Types_.const_view +=
  1. | C_bool
  2. | C_eq
  3. | C_ite
  4. | C_not
  5. | C_true
  6. | C_false
  7. | C_proof
val true_ : Sidekick_core_logic.Term.store -> Sidekick_core_logic.Term.t
val false_ : Sidekick_core_logic.Term.store -> Sidekick_core_logic.Term.t

eq a b is a = b

ite a b c is if a then b else c

val is_eq : Sidekick_core_logic.Term.t -> bool
val is_bool : Sidekick_core_logic.Term.t -> bool

abs t returns an "absolute value" for the term, along with the sign of t.

The idea is that we want to turn not a into (false, a), or (a != b) into (false, a=b). For terms without a negation this should return (true, t).

val as_bool_val : Sidekick_core_logic.Term.t -> bool option

open_eq (a=b) returns Some (a,b), None for other terms.

type hook = recurse:term Sidekick_util.Fmt.printer -> Sidekick_util.Fmt.t -> term -> bool

Printing hook, responsible for printing certain subterms

val default_hooks : Hooks.t Stdlib.ref
val pp_with : Hooks.t -> term Sidekick_util.Fmt.printer

Print using the hooks

val pp : term Sidekick_util.Fmt.printer

Print using default_hooks

val pp_limit : max_depth:int -> max_nodes:int -> term Sidekick_util.Fmt.printer

Print with a limit on the number of nodes printed. An ellipsis is displayed otherwise.

module Trace_reader = Sidekick_core.Term.Trace_reader