Represents a Hol term as directed acyclic graph (DAG).
All terms contain a deterministic ID assigned by ShotDs.Stt.TermFactory.
Note that terms are in βη-normal form, i.e., fully β-reduced and η-expanded.
Besides the obvious fields :head, :args and :type, two accessor fields
are implemented for efficiency: :fvars contains all free variables
occurring in the term, :max_num represents the index of the highest bound
variable. Abstractions are identified by the :bvars field.
Summary
Types
Preliminary or dummy term IDs are assigned 0 as their ID. Those are never present in an ETS table.
Term IDs present in the global ETS table managed by ShotDs.Stt.TermFactory
are represented as positive integers.
Term IDs that are only created and consumed locally and managed in a local "scratchpad" ETS table are represented as negative integers.
The type of a term. The fields :id, :head and :type are required.
A term's id is given by an atomic positive (global) or negative (local) integer where 0 denotes a dummy.
Types
@type dummy_term_id() :: 0
Preliminary or dummy term IDs are assigned 0 as their ID. Those are never present in an ETS table.
@type global_term_id() :: pos_integer()
Term IDs present in the global ETS table managed by ShotDs.Stt.TermFactory
are represented as positive integers.
@type local_term_id() :: neg_integer()
Term IDs that are only created and consumed locally and managed in a local "scratchpad" ETS table are represented as negative integers.
@type t() :: %ShotDs.Data.Term{ args: [term_id()], bvars: [ShotDs.Data.Declaration.t()], fvars: [ShotDs.Data.Declaration.t()], head: ShotDs.Data.Declaration.t(), id: term_id(), max_num: non_neg_integer(), type: ShotDs.Data.Type.t() }
The type of a term. The fields :id, :head and :type are required.
@type term_id() :: global_term_id() | local_term_id() | dummy_term_id()
A term's id is given by an atomic positive (global) or negative (local) integer where 0 denotes a dummy.