Episteme.Term (Episteme v0.2.0)

Copy Markdown View Source

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

compare_order(a, b)

@spec compare_order(term(), term()) :: :lt | :eq | :gt

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

deconstruct(arg1)

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.

fresh_copy(term)

@spec fresh_copy(term()) :: term()

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.

ground?(arg1)

@spec ground?(term()) :: boolean()

True iff term contains no unbound variable anywhere -- resolve deeply first (see resolve_deep/2) if term may still hold bindings.

new_var(name \\ "_")

@spec new_var(String.t()) :: Episteme.Term.Var.t()

A fresh variable, optionally named for display.

resolve_deep(term, bindings)

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

sort_by_order(list)

@spec sort_by_order([term()]) :: [term()]

Sorts list by compare_order/2 -- the shared basis for msort/2 and, deduped, sort/2/setof/3.

sort_unique(list)

@spec sort_unique([term()]) :: [term()]

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.

structurally_equal?(a, b)

@spec structurally_equal?(term(), term()) :: boolean()

Structural equality (==/2) on two already-resolved terms -- same shape, same variable identity, and (unlike plain Elixir ==) an integer never equals a float.

term_variables(term)

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

to_text(list)

@spec to_text(term()) :: String.t()

Canonical functor(args) text for an already fully-resolved term -- no operator-aware pretty-printing.