Add priv/prelude.pl: the textbook why meta-interpreter - #4
Merged
Merged
Conversation
Ships an example for MANIFOLD_PRELUDE: solve/2, the vanilla meta-circular interpreter from Sterling & Shapiro's The Art of Prolog, extended with a second argument that keeps the derivation (fact/1, rule/2, builtin/1) instead of discarding it. why/2 is solve/2 under the name a caller wants to ask for, e.g. `?- why(mortal(socrates), Proof)` in question mode. It only uses kernel-resident predicates (clause/2, predicate_property/2, call/1) since it loads ahead of the unknown=fail flag that permanently breaks autoloading for the engine's lifetime (see test/smoke/prolog_autoload_test.exs). predicate_property/2 routes true built-ins (>/2, is/2, \+/1, ...) around clause/2 before it's reached, since clause/2 raises a permission_error on those rather than failing. test/integration/why_meta_interpreter_test.exs consults the shipped file itself (not a re-typed copy) and checks the proof shape for a fact, a rule, a rule whose body calls a built-in, and the two failure paths (goal doesn't hold; predicate never heard of). Verified the Prolog-level semantics directly against a real swipl (not available as an Elixir toolchain in this environment) and cross-checked the JSON compound-term encoding against the installed library(term_to_json) source to confirm the MQI wire shapes asserted in the test.
solve/2's conjunction clause used to mirror ,/2's own right-associative shape: (ProofA, (ProofB, ProofC)) for a three-goal body. That's a proof whose structure reflects how the source text happened to associate rather than the derivation itself, and it makes a three-goal body indistinguishable in shape from "two goals, the second of which is itself two goals." conj_list/2 walks the ,/2 chain once and flattens it into [ProofA, ProofB, ProofC]. A single-goal body is unaffected — it was never a conjunction, so it stays a bare proof term rather than a one-element list. Also pins :- encoding(utf8) as the very first line: consulting the file under a non-UTF-8 locale (LC_CTYPE=POSIX, reproduced in this sandbox) otherwise misreads the em dashes in the header comment as "Illegal multibyte Sequence" — harmless today since it only corrupts comments, but not something to leave load-bearing on the deployment's locale. Re-verified both changes directly against swipl (still no Elixir toolchain in this environment): the three-goal case now prints rule(triple(widget),[fact(price(widget,150)),builtin(150>100), builtin(150<1000)]) instead of the nested-tuple shape, and consulting the file under LC_CTYPE=POSIX no longer warns.
solve/2 gets a dedicated (A ; B) clause: try the left arm, and only if that fails, the right, exactly like ;/2 itself. The proof keeps only the arm that actually fired, tagged either(left, ProofA) or either(right, ProofB), instead of `builtin((A;B))` treating the whole disjunction as one opaque call. It stays exactly as non-deterministic as plain ;/2: backtracking (findall/3 over why/2) reaches every left solution before falling through to the right, one either/2 per solution. Placement matters and is now load-bearing: the ;/2 clause has to come before the generic builtin/1 clause, or predicate_property((A;B), built_in) would claim the disjunction first and call/1 it as one step — the exact outcome either/2 exists to avoid. It also has to come before fact/1 and rule/2, since clause((A;B), true) raises the same permission_error clause(1>2, _) does. (Cond -> Then ; Else) still gets partial treatment worth documenting: the outer ;/2 now reports which side fired, but the if-then arm itself is a ->/2 term and stays one opaque builtin((Cond->Then)) leaf, since solve/2 still has no dedicated ->/2 clause. test/integration/why_meta_interpreter_test.exs: two new cases — one arm firing (plato / vegetarian) and both arms firing on backtracking (socrates satisfies both branches, checked by sorting the two either/2-tagged proofs rather than assuming solution order). Re-verified against real swipl (still no Elixir toolchain here): either/left and either/right tagging, a 3-way disjunction chain nesting either(right, either(right, ...)), disjunction embedded inside a conjunction's flattened list, the if-then-else partial-opacity case, and findall/3 backtracking giving both tagged proofs for socrates.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Ships an example for MANIFOLD_PRELUDE: solve/2, the vanilla meta-circular
interpreter from Sterling & Shapiro's The Art of Prolog, extended with a
second argument that keeps the derivation (fact/1, rule/2, builtin/1)
instead of discarding it. why/2 is solve/2 under the name a caller wants
to ask for, e.g.
?- why(mortal(socrates), Proof)in question mode.It only uses kernel-resident predicates (clause/2, predicate_property/2,
call/1) since it loads ahead of the unknown=fail flag that permanently
breaks autoloading for the engine's lifetime (see
test/smoke/prolog_autoload_test.exs). predicate_property/2 routes true
built-ins (>/2, is/2, +/1, ...) around clause/2 before it's reached,
since clause/2 raises a permission_error on those rather than failing.
test/integration/why_meta_interpreter_test.exs consults the shipped file
itself (not a re-typed copy) and checks the proof shape for a fact, a
rule, a rule whose body calls a built-in, and the two failure paths
(goal doesn't hold; predicate never heard of).
Verified the Prolog-level semantics directly against a real swipl (not
available as an Elixir toolchain in this environment) and cross-checked
the JSON compound-term encoding against the installed
library(term_to_json) source to confirm the MQI wire shapes asserted in
the test.