Episteme's term representation: atoms and numbers are plain Elixir
atoms/integers/floats, a real Prolog string is a plain Elixir binary
-- a genuinely new atomic term
class, not a list of codes, but still no dedicated struct, the same
"raw host-language value" pattern atoms/integers/floats already use --
lists are native Elixir lists, variables and compounds get dedicated
structs. This module is the
Ichor.Backtrack.Term implementation passed explicitly to every
Ichor.Backtrack.Bindings call, plus the handful of whole-term
operations (deep resolve, rename-apart) built on
Ichor.Toolkit.TermWalk that unification itself doesn't need but the
engine does.
Summary
Functions
ISO's standard order of terms: Var < Number < Atom < Compound.
Both arguments should already be resolved (see resolve_deep/2) --
an unresolved variable bound to, say, a compound would otherwise
sort as a variable instead of by what it's actually bound to.
A non-empty native Elixir list decomposes as ISO's own ./2 cons
functor ([H|T] <-> .(H, T)) -- the encoding that lets
Ichor.Backtrack.Bindings.unify/4 recurse into list structure at all
(without this, [H|T] vs [1,2,3] would only ever compare via plain
==/2, never binding H/T). [] is the atomic empty-list atom,
same as real Prolog -- not a ./2 cell, so it stays out of
compound?/1 above.
Renames every distinct variable in term apart to a brand new one,
preserving sharing (two occurrences of the same variable become two
occurrences of the same fresh variable) -- the "discover names, build
a fresh-ref map, rewrite" shape. Used both for copy_term/2 and to
instantiate a stored clause fresh on every call.
True iff term contains no unbound variable anywhere -- resolve deeply first (see resolve_deep/2) if term may still hold bindings.
A fresh variable, optionally named for display.
Fully dereferences term and every subterm reachable through it under
bindings -- unlike Ichor.Backtrack.Bindings.resolve/3, which only
chases the outermost variable one level deep, this also resolves
inside compound-term arguments (and, since rewrite/3 re-examines a
freshly resolved variable's own value, transitively through however
many bindings a chain passes through).
Sorts list by compare_order/2 -- the shared basis for msort/2 and, deduped, sort/2/setof/3.
Like sort_by_order/1, but also drops every term that standard-order-
compares :eq to its predecessor once sorted -- not plain Elixir
==, which would wrongly conflate 1 and 1.0 (equal by ==, but
never :eq in standard order -- see compare_order/2's own
float-before-integer tie-break). Shared by sort/2 and setof/3.
Structural equality (==/2) on two already-resolved terms -- same shape, same variable identity, and (unlike plain Elixir ==) an integer never equals a float.
Every distinct variable in term, in first-occurrence order (real
Prolog's own term_variables/2, though not itself exposed as a
callable goal yet) -- Episteme.Engine's own building block for
bagof/3/setof/3's free-variable grouping: which of a Goal's
variables aren't mentioned in Template and aren't existentially
quantified via Var^Goal.
Canonical functor(args) text for an already fully-resolved term -- no operator-aware pretty-printing.
Functions
ISO's standard order of terms: Var < Number < Atom < Compound.
Both arguments should already be resolved (see resolve_deep/2) --
an unresolved variable bound to, say, a compound would otherwise
sort as a variable instead of by what it's actually bound to.
Within a class: variables order by reference identity (a total,
consistent order within one run, not meaningful across runs, and not
the same thing as creation order); numbers by value, with a float
sorting before an integer of equal value (1.0 before 1); atoms
alphabetically by character code ([], the empty-list atom, sorts
as if its name were the two characters [ ], same as any other
atom); strings alphabetically by byte value, same comparator as
atoms; compounds (a non-empty list
decomposes via the same ./2 cons functor compound?/1 uses
everywhere else) by arity first, then functor name alphabetically,
then arguments left to right, recursively.
Classes order Var < Number < Atom < String < Compound -- a real
string is its own class, distinct from atoms, matching SWI-Prolog's
own convention (ISO itself has no strings to place, since its own
double-quoted syntax is just a code-list).
A non-empty native Elixir list decomposes as ISO's own ./2 cons
functor ([H|T] <-> .(H, T)) -- the encoding that lets
Ichor.Backtrack.Bindings.unify/4 recurse into list structure at all
(without this, [H|T] vs [1,2,3] would only ever compare via plain
==/2, never binding H/T). [] is the atomic empty-list atom,
same as real Prolog -- not a ./2 cell, so it stays out of
compound?/1 above.
Renames every distinct variable in term apart to a brand new one,
preserving sharing (two occurrences of the same variable become two
occurrences of the same fresh variable) -- the "discover names, build
a fresh-ref map, rewrite" shape. Used both for copy_term/2 and to
instantiate a stored clause fresh on every call.
True iff term contains no unbound variable anywhere -- resolve deeply first (see resolve_deep/2) if term may still hold bindings.
@spec new_var(String.t()) :: Episteme.Term.Var.t()
A fresh variable, optionally named for display.
@spec resolve_deep(term(), Ichor.Backtrack.Bindings.t()) :: term()
Fully dereferences term and every subterm reachable through it under
bindings -- unlike Ichor.Backtrack.Bindings.resolve/3, which only
chases the outermost variable one level deep, this also resolves
inside compound-term arguments (and, since rewrite/3 re-examines a
freshly resolved variable's own value, transitively through however
many bindings a chain passes through).
Sorts list by compare_order/2 -- the shared basis for msort/2 and, deduped, sort/2/setof/3.
Like sort_by_order/1, but also drops every term that standard-order-
compares :eq to its predecessor once sorted -- not plain Elixir
==, which would wrongly conflate 1 and 1.0 (equal by ==, but
never :eq in standard order -- see compare_order/2's own
float-before-integer tie-break). Shared by sort/2 and setof/3.
Structural equality (==/2) on two already-resolved terms -- same shape, same variable identity, and (unlike plain Elixir ==) an integer never equals a float.
@spec term_variables(term()) :: [Episteme.Term.Var.t()]
Every distinct variable in term, in first-occurrence order (real
Prolog's own term_variables/2, though not itself exposed as a
callable goal yet) -- Episteme.Engine's own building block for
bagof/3/setof/3's free-variable grouping: which of a Goal's
variables aren't mentioned in Template and aren't existentially
quantified via Var^Goal.
Canonical functor(args) text for an already fully-resolved term -- no operator-aware pretty-printing.