Module Sidekick_base.Ty

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

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

View.

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

include Sidekick_sigs.EQ_ORD_HASH with type t := Sidekick_core_logic__.Types_.term
include Sidekick_sigs.EQ with type t := Sidekick_core_logic__.Types_.term
include Sidekick_sigs.ORD with type t := Sidekick_core_logic__.Types_.term
include Sidekick_sigs.HASH with type t := Sidekick_core_logic__.Types_.term
val pp_debug : Sidekick_core_logic__.Types_.term Sidekick_util.Fmt.printer
val pp_debug_with_ids : Sidekick_core_logic__.Types_.term Sidekick_util.Fmt.printer

Containers

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

Utils

val view : Sidekick_core_logic__.Types_.term -> view
val unfold_app : Sidekick_core_logic__.Types_.term -> Sidekick_core_logic__.Types_.term * Sidekick_core_logic__.Types_.term list
val is_app : Sidekick_core_logic__.Types_.term -> bool
val is_const : Sidekick_core_logic__.Types_.term -> bool
val is_pi : Sidekick_core_logic__.Types_.term -> bool
val iter_dag : ?seen:unit Tbl.t -> iter_ty:bool -> f:(Sidekick_core_logic__.Types_.term -> unit) -> Sidekick_core_logic__.Types_.term -> 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 -> Sidekick_core_logic__.Types_.term -> unit) -> Sidekick_core_logic__.Types_.term -> 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 -> Sidekick_core_logic__.Types_.term -> Sidekick_core_logic__.Types_.term) -> Sidekick_core_logic__.Types_.term -> Sidekick_core_logic__.Types_.term
val exists_shallow : f:(bool -> Sidekick_core_logic__.Types_.term -> bool) -> Sidekick_core_logic__.Types_.term -> bool
val for_all_shallow : f:(bool -> Sidekick_core_logic__.Types_.term -> bool) -> Sidekick_core_logic__.Types_.term -> bool
val contains : Sidekick_core_logic__.Types_.term -> sub:Sidekick_core_logic__.Types_.term -> bool
val free_vars_iter : Sidekick_core_logic__.Types_.term -> var Iter.t
val free_vars : ?init:Sidekick_core_logic__.Var.Set.t -> Sidekick_core_logic__.Types_.term -> Sidekick_core_logic__.Var.Set.t
val is_type : Sidekick_core_logic__.Types_.term -> bool

is_type t is true iff view t is Type _

val is_a_type : Sidekick_core_logic__.Types_.term -> bool

is_a_type t is true if is_ty (ty t)

val is_closed : Sidekick_core_logic__.Types_.term -> bool

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

val has_fvars : Sidekick_core_logic__.Types_.term -> bool

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

val ty : Sidekick_core_logic__.Types_.term -> Sidekick_core_logic__.Types_.term

Return the type of this term.

Creation

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

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_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
type t = Types_.ty
type data = Types_.data
include Sidekick_sigs.EQ_ORD_HASH_PRINT 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
include Sidekick_sigs.PRINT with type t := t
val const_decoders : Sidekick_core.Const.decoders
val bool : store -> t
val real : store -> t
val int : store -> t
val uninterpreted : store -> ID.t -> t
val uninterpreted_str : store -> string -> t
val is_uninterpreted : t -> bool
val is_real : t -> bool
val is_int : t -> bool