Module Sidekick_base.Ty

include module type of struct include Types_.Term end
include module type of struct include Sidekick_core_logic.Term end
type nonrec var
type nonrec bvar

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 =
| E_type of int
| E_var of var
| 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

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 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 +=
| C_bool
| C_eq
| C_ite
| C_not
| C_true
| C_false
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
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

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