Episteme.Term (Episteme v0.1.0)

Copy Markdown View Source

Episteme's term representation: atoms and numbers are plain Elixir atoms/integers/floats, 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

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.

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

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

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

Functions

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.

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

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.

to_text(list)

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

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