ShotDs.Data.Term (shot_ds v1.2.0)

Copy Markdown View Source

Represents a higher-order term as directed acyclic graph (DAG).

All terms contain a unique 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, several accessor fields are implemented for efficiency: :fvars contains all free variables occurring in the term, :consts contains all non-logical constants occurring in the term, :tvars records all non-instantiated type variables, :max_num represents the index of the highest bound variable. Abstractions are identified by the :bvars field.

Summary

Types

dummy_term_id()

Preliminary or dummy term IDs are assigned 0 as their ID. Those are never present in an ETS table.

global_term_id()

Term IDs present in the global ETS table managed by ShotDs.Stt.TermFactory are represented as positive integers.

local_term_id()

Term IDs that are only created and consumed locally and managed in a local "scratchpad" ETS table are represented as negative integers.

t()

The type of a term. The fields :id, :head and :type are required.

term_id()

A term's id is given by an atomic positive (global) or negative (local) integer where 0 denotes a dummy.

Types

dummy_term_id()

@type dummy_term_id() :: 0

Preliminary or dummy term IDs are assigned 0 as their ID. Those are never present in an ETS table.

global_term_id()

@type global_term_id() :: pos_integer()

Term IDs present in the global ETS table managed by ShotDs.Stt.TermFactory are represented as positive integers.

local_term_id()

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

t()

@type t() :: %ShotDs.Data.Term{
  args: [term_id()],
  bvars: [ShotDs.Data.Declaration.t()],
  consts: MapSet.t(ShotDs.Data.Declaration.const_t()),
  fvars: MapSet.t(ShotDs.Data.Declaration.t()),
  head: ShotDs.Data.Declaration.t(),
  id: term_id(),
  max_num: non_neg_integer(),
  tvars: MapSet.t(ShotDs.Data.Type.variable_id()),
  type: ShotDs.Data.Type.t()
}

The type of a term. The fields :id, :head and :type are required.

term_id()

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