diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index b5cad5e..939bca8 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -15,8 +15,8 @@ jobs: steps: - uses: actions/checkout@v7 - uses: fabasoad/setup-prolog-action@v1 - - name: Rewrite test - run: test/hash_consing_rewrite.sh | diff - test/hash_consing_rewrite_baseline.txt + - name: Tests + run: swipl -p library=prolog --stack-limit=32m --table-space=32m -g run_tests -t halt test/hash_consing.plt - name: The pack installs and loads run: | mkdir -p "$RUNNER_TEMP/packs" diff --git a/README.md b/README.md index 9e81b10..1f33fba 100644 --- a/README.md +++ b/README.md @@ -4,9 +4,11 @@ Hash-consed terms for SWI-Prolog, and a load-time rewrite that makes a program use them. A file is written as the program that does not intern and -names the constructors to intern; every clause read after that directive -refers to their instances by Ids, each wrapping a node handle of one trie, -and the store is canonical: the same term has the same Id. +names, by templates, the terms to intern: a term is interned when a template +of its constructor matches it, and stays a plain term otherwise. Every clause +read after the directive refers to the interned terms by Ids, each wrapping a +node handle of one trie, and the store is canonical: the same term has the +same Id. ## Install @@ -19,7 +21,7 @@ and the store is canonical: the same term has the same Id. ```prolog :- module(steps, [step/2, built/2]). :- use_module(library(hash_consing), []). -:- hash_consing:rewritten([apply(*, _), lambda(_), variable(_)]). +:- hash_consing:rewritten([apply(lambda(_), _), lambda(_), variable(_)]). step(apply(lambda(Body), Argument), beta(Body, Argument)). @@ -27,20 +29,83 @@ built(Function, Applied) :- Applied = apply(Function, variable(0)). ``` -A term that did not come through the rewrite crosses the boundary with -`hash_consing:internalized/3`, and `hash_consing:externalized/2` turns Ids back -into terms. The module comment of [`prolog/hash_consing.pl`](prolog/hash_consing.pl) -is the reference: the relation `intern/2`, the Id and its shape, the -templates, the rewrite of a clause, the two rules for a file that opts in, -and the known defects. +Here an application is interned when its first argument is a lambda; any +other application stays a plain compound whose arguments are represented in +turn. A term that did not come through the rewrite crosses the boundary with +`hash_consing:internalized/3`, `hash_consing:externalized/2` turns Ids back +into terms, and `hash_consing:declared/1` declares templates at run time, for +constructors a program makes as it runs. The module comment of +[`prolog/hash_consing.pl`](prolog/hash_consing.pl) is the reference: the +relation `intern/2`, the Id and its shape, the templates, the rewrite of a +clause, the two rules for a file that opts in, and the known defects. + +## Templates are patterns + +What is interned is chosen by patterns, not by constructors. A template is +written like the clause heads it serves: a constructor applied, at each +argument position, to `_` (any argument), `*` (any argument, its root +constructor recorded) or a nested template (an argument with the nested +template's constructor, whose arguments match the nested template's). A +constructor may have several templates. They are tried in the order of the +list, the first that matches a term is its template, and a term that none +matches is not interned. From +[`test/hash_consing_fixtures/patterns.pl`](test/hash_consing_fixtures/patterns.pl): + +```prolog +:- hash_consing:rewritten([app(abs(_), _), app(app(*, _), _), app(_, ref(_)), abs(_), ref(_)]). + +% Must intern, every instance taking the first template: the shape `abs/1` +% is written into the head. +kind(app(abs(_), _), redex). +% Must intern, every instance taking the second template: `app/2(abs/1)`. +kind(app(app(abs(_), _), _), redex_under_an_application). +% Must intern, every instance taking the third template: `ref/1`. +kind(app(ref(_), ref(_)), stuck). +% Must not intern: no template matches any instance, so the head keeps the +% plain application. +kind(app(ref(_), abs(_)), plain). +``` + +The Id of an interned application is `'__hash_consed_app/2'(Shape, Handle)`: +the root constructor is in the Id's name, and the shape, one atom, spells what +the term's template records below the root, `app/2(abs/1)` for the two layers +of the second template. SWI-Prolog's deep indexing then tells the first three +heads apart without looking the terms up. `app(abs(ref(0)), ref(1))` matches +the first template and the third; the first gives its shape, `abs/1`. +`app(ref(0), abs(ref(1)))` matches none, stays a plain compound, and meets the +plain head of the last clause. + +A head that does not decide whether its argument is interned, such as +`size(app(Function, Argument), Size)` in the same file, gets a variable in +that position, related to the term by `hash_consing:represented/2`; the clause +keeps its meaning and loses the first argument index there. A body goal hands +such an occurrence over decided: what is bound of it must settle whether a +template matches, or the call raises an instantiation error. + +## Incompatible changes in 0.2.0 + +- A nested template requires its constructor: `apply(apply(*, _), _)` matches + only applications whose first argument is an application, where 0.1.0 + recorded the second layer when it was there and one layer otherwise. +- A constructor may have several templates, tried in order; `;` no longer + writes alternatives inside a template. +- A term that no template of its constructor matches is not interned: it + stays a plain compound, and `intern/2` fails on it. +- `intern/2` raises `existence_error(templates, Name/Arity)` on a constructor + without templates, where 0.1.0 declared it on first use. +- A rewritten body goal raises an instantiation error when it is handed an + occurrence whose interning is still undecided. +- `*` records the root constructor of any compound or atom, where 0.1.0 wrote + `-` for an argument that was not an Id. +- New predicates: `declared/1`, `is_id/1` and `represented/2`. ## Test ```sh -test/hash_consing_rewrite.sh | diff - test/hash_consing_rewrite_baseline.txt +swipl -p library=prolog --stack-limit=32m --table-space=32m -g run_tests -t halt test/hash_consing.plt ``` -prints nothing when the rewrite and `intern/2` behave as specified. +Run from the root of the pack, it exits with status 0 when every test passes. ## Contributing and releases diff --git a/pack.pl b/pack.pl index 5e51f93..6962cb1 100644 --- a/pack.pl +++ b/pack.pl @@ -1,5 +1,5 @@ name(hash_consing). -version('0.1.0'). +version('0.2.0'). title('Hash-consed terms by clause rewriting'). keywords([interning, 'hash-consing', trie, term_expansion]). author('Yang, Bo', 'yang-bo@yang-bo.com'). diff --git a/prolog/hash_consing.pl b/prolog/hash_consing.pl index e55adc0..1eb5cd1 100644 --- a/prolog/hash_consing.pl +++ b/prolog/hash_consing.pl @@ -1,32 +1,39 @@ :- module(hash_consing, [ intern/2, % ?Term, ?Id + represented/2, % ?Layer, ?Representation + is_id/1, % +Value externalized/2, % +TermWithIds, -External - internalized/3, % +Constructors, +External, -TermWithIds - rewritten/1 % +Constructors + internalized/3, % +Templates, +External, -TermWithIds + declared/1, % +Templates + rewritten/1 % +Templates ]). -/** hash_consing: hash-consed terms whose Ids record a configurable shape, and a term rewrite that makes a program use them +/** hash_consing: hash-consed terms selected by templates, whose Ids record a shape, and a term rewrite that makes a program use them A GENERIC LIBRARY: it knows no constructor of any calculus and keeps no -configuration but the templates files declare. +configuration but the templates that files and `declared/1` declare. HOW TO USE IT. A file is written as the program that does not intern, loads -this library and names the constructors to intern, each by a template: +this library and names, by templates, the terms to intern: :- module(steps, [step/2, built/2]). :- use_module(library(hash_consing), []). - :- hash_consing:rewritten([apply(*, _), lambda(_), variable(_)]). + :- hash_consing:rewritten([apply(lambda(_), _), lambda(_), variable(_)]). step(apply(lambda(Body), Argument), beta(Body, Argument)). built(Function, Applied) :- Applied = apply(Function, variable(0)). -Files that hand such terms to each other declare the same templates, most -simply by including one file that holds the directive. Code that did not go -through the rewrite crosses the boundary explicitly: +A term is interned when a template of its constructor matches it (TEMPLATES +ARE PATTERNS, below); here an application is interned when its first +argument is a lambda, and any other application stays a plain compound whose +arguments are represented in turn. Files that hand such terms to each other +declare the same templates, most simply by including one file that holds the +directive. Code that did not go through the rewrite crosses the boundary +explicitly: - ?- hash_consing:internalized([apply(*, _), lambda(_), variable(_)], + ?- hash_consing:internalized([apply(lambda(_), _), lambda(_), variable(_)], apply(lambda(variable(0)), variable(1)), Id), steps:step(Id, Result), hash_consing:externalized(Result, External). @@ -34,23 +41,29 @@ External = beta(variable(0), variable(1)). With the list `[]` the file loads unchanged, which is the program without -interning. The test `test/hash_consing_rewrite.sh` prints what the rewrite -makes of its fixtures, `test/hash_consing_fixtures/`, and is the place to -read exact rewritten clauses. +interning. The test `test/hash_consing.plt` loads the fixtures in +`test/hash_consing_fixtures/` and compares what the rewrite makes of them +with the snapshots in `test/hash_consing_snapshots/`, the place to read +exact rewritten clauses. `intern(?Term, ?Id)` IS ONE RELATION WITH TWO DIRECTIONS (user, 2026-09-17: a binary predicate that upserts forwards and looks up backwards). Term is a -ground term whose rewritten subterms are Ids already. Called with Id bound it +ground term whose subterms are represented already. Called with Id bound it looks the term up (and with Term bound as well it is a check that inserts nothing); called with Id unbound, or bound to an Id pattern whose Handle is -unbound, it inserts Term unless it is there and answers its Id; a value that -is no Id matches nothing and the call fails, as a pattern that does not match -fails without interning (user ruling, 2026-09-17: an uninterned instance at -an Id position fails to unify rather than raising). The store is canonical -(the same term, the same Id), idempotent and monotone (it only grows and -backtracking does not shrink it), so an answer once given is never -contradicted. An Id is abstract: only `==`, `intern/2` and the two boundary -predicates look at it. +unbound, it inserts Term unless it is there and answers its Id. It fails, +inserting nothing, when no template of Term's constructor matches Term (user, +2026-09-26: a term that matches no template is not interned, even when its +constructor has templates), and raises `existence_error(templates, +Name/Arity)` when the constructor has no template in this process, which is +most likely a missing declaration (user, 2026-09-26, approving the change). A +value that is no Id matches nothing and the call fails, as a pattern that +does not match fails without interning (user ruling, 2026-09-17: an +uninterned instance at an Id position fails to unify rather than raising). +The store is canonical (the same term, the same Id), idempotent and monotone +(it only grows and backtracking does not shrink it), so an answer once given +is never contradicted. An Id is abstract: only `==`, `intern/2`, +`represented/2`, `is_id/1` and the two boundary predicates look at it. AN ID IS `'__hash_consed_Name/Arity'(Handle)` OR `'__hash_consed_Name/Arity'(Shape, Handle)`. Name/Arity is the root constructor @@ -67,16 +80,16 @@ THE SHAPE is there for clauses told apart by an INNER constructor, step(apply(lambda(Body), Argument)) :- ... - step(apply(closure_a(Capture), Argument)) :- ... + step(apply(closure(Capture), Argument)) :- ... whose heads would otherwise be one Id pattern, every candidate clause paying a lookup before it fails. Shape is ONE ATOM that spells the constructors -found below the root, as far as the constructor's template says (user, -2026-09-20: the Id keeps one layer, the shape may have several; the layers -are joined into one atom, not kept as several shapes; how deep is -configurable). The heads above become -`step('__hash_consed_apply/2'('lambda/1', Handle))` and -`step('__hash_consed_apply/2'('closure_a/1', Handle))`, and the deep index +found below the root, as far as the term's template says (user, 2026-09-20: +the Id keeps one layer, the shape may have several; the layers are joined +into one atom, not kept as several shapes; how deep is configurable). Under +the templates `apply(lambda(_), _)` and `apply(closure(_), _)` the heads above +become `step('__hash_consed_apply/2'('lambda/1', Handle))` and +`step('__hash_consed_apply/2'('closure/1', Handle))`, and the deep index SWI-Prolog builds on the first argument of the first argument tells them apart without a lookup (benchmark, 2026-09-20: 1000 calls over 2000 such clauses, 621 ms without the shape and 3 ms with it; upserts 46 percent @@ -86,52 +99,65 @@ shallow pattern `apply(F, X)` has to match the Ids of every shape and the set of inner constructors is open across files; and the Id holds no Id of a subterm, because a truncation would give one term two spellings and split -`==` and the table keys. A shape is a function of the content and the -template, so the Handle determines it and the store stays canonical. - -THE CONFIGURATION IS A TEMPLATE, one syntax for every constructor (user, -2026-09-20: one syntax, not three; the template names the constructor, so no -indicator beside it; a depth of zero is another feature and is not offered). -An element of the directive's list is the constructor applied to one of these -at each argument position (a constructor of arity zero is its atom): - - _ nothing is recorded about the argument - * the root constructor of the argument is recorded - a nested template the root constructor is recorded and, when it is the - template's constructor, the template goes on below - it; alternatives are joined by `;` - -`lambda(_)` records the root only and its Ids are -`'__hash_consed_lambda/1'(Handle)`. `apply(*, _)` -gives `apply(lambda(B), X)` the shape `'lambda/1'`; with -`apply(apply(*, _), _)`, `apply(apply(lambda(B), Y), X)` has the shape -`'apply/2(lambda/1)'` and `apply(lambda(B), X)` still `'lambda/1'`. An -argument that is no Id is written `-`. The reading has a precedent in -SWI-Prolog's mode-directed tabling, `:- table path(_, _, min)`. - -THE SHAPE IS A FUNCTION OF THE TERM AND OF ITS OWN TEMPLATE, and of nothing -else: at a `*` the root is read off the functor name of the argument's Id, -with no lookup; each nested template costs an upsert one `trie_term/2` on the -argument's Id. The spelling of a shape is remembered in a trie keyed by its -structure, so an atom is built once per structure; the atoms are finitely -many, bounded by the templates and the constructors. - -AT COMPILE TIME a pattern that determines everything its template records -gets the atom written into the head; a pattern that determines only part of -it gets an unbound shape, which is correct (the constructors of the pattern -are still checked by the lookups of the body) and unindexed. A nested -template reads the argument's own arguments off the occurrence of that -argument in the same clause, or off the store when its Id was baked. A -partial pattern is NOT expanded into one clause per completion: a file loaded -later brings new shapes, which the expanded clauses would silently miss. So -the deeper a template, the fewer patterns determine it. - -ONE CONFIGURATION PER CONSTRUCTOR, PER PROCESS: a second declaration of a -constructor with another template raises while the file loads, because two -shapes of one term would not be `==` (agent design decision, 2026-09-20, not -objected to by the user; between files the library checks nothing else, by -the user's ruling of 2026-09-17: which files list which constructors is the -user's to arrange, for instance with one included file). +`==` and the table keys. A shape is a function of the content and of the +constructor's templates, so the Handle determines it and the store stays +canonical. + +TEMPLATES ARE PATTERNS, in one syntax for every constructor (user, +2026-09-20: one syntax, not three; user, 2026-09-26: hash_consing is based on +patterns, not on constructors). An element of a list of templates is a +constructor applied to one of these at each argument position (a +constructor of arity zero is its atom): + + _ any argument; nothing is recorded + * any argument; its root constructor is recorded + a nested template an argument whose root constructor is the template's + and whose arguments match the template's arguments; + its root is recorded, and what the template records + below it + +`*` records the root constructor of the term the argument stands for, +`Name/Arity`, whether that term is interned or not, and `-` for a number or a +string. There is no alternative inside a template, and `;` is an ordinary +constructor: the alternatives of a constructor are several templates in the +list, because Prolog's `;` is a disjunction whose two sides can both hold, +and templates are not predicates (user, 2026-09-26). + +A CONSTRUCTOR'S TEMPLATES ARE TRIED IN ORDER, the order of the list, and the +first that matches a term is the term's template; the templates after it are +not looked at, and a term has one template or none (user, 2026-09-26: the +parts where templates overlap use the first matching template; matching +several templates at once has no meaning). The shape is what that template +records, spelled as the recorded descriptions joined by commas, `''` when it +records nothing. Under `apply(apply(*, _), _)` then `apply(*, _)`, the term +`apply(apply(lambda(B), Y), X)` has the shape `'apply/2(lambda/1)'` and +`apply(lambda(B), X)` the shape `'lambda/1'`; under `apply(apply(*, _), _)` +alone the second is not interned. A template that one earlier template +always takes first raises while it is declared, so a constructor whose +templates record nothing has the one template `Name(_, ..., _)`, and its Ids +have no shape; the Ids of any other constructor have one. Two templates that +record different positions can spell the same atom for different terms, +which only keeps the index from telling their clauses apart. + +MATCHING AND RECORDING READ THE TERM, not how its subterms are represented: +an argument that is an Id is read through the store and an argument that is +a plain compound as it is, and both give the same root and arguments. At a +`*` the root of an Id is read off its functor name, with no lookup; a nested +template costs one `trie_term/2` on an argument that is an Id. The spelling +of a shape is remembered in a trie keyed by its structure, so an atom is +built once per structure; the atoms are finitely many, bounded by the +templates and the constructors. + +ONE LIST OF TEMPLATES PER CONSTRUCTOR, PER PROCESS: the first declaration of +a constructor, by `rewritten/1`, `declared/1` or `internalized/3`, fixes its +list, and another declaration with other templates or another order raises +`permission_error(reconfigure, interned_constructor, Name/Arity)`, because +whether a term is interned and what its shape is must agree wherever it is +handed (agent design decision, 2026-09-20, for one template, and 2026-09-26 +for a list, in plans the user approved; between files the library checks +nothing else, by the user's ruling of 2026-09-17: which files list which +constructors is the user's to arrange, for instance with one included file). +A constructor is never declared by being met. THE STORE IS ONE TRIE, used through SWI-Prolog's trie API directly (user, 2026-09-17, after a benchmark of four candidate stores: "use the trie"). Its @@ -141,40 +167,83 @@ key with a different value raises instead of failing. It lives outside the table space and `trie_property(Trie, value_count(Count))` counts it. -`externalized/2` AND `internalized/3` ARE THE BOUNDARY: the first replaces -every Id by its term, recursively, for printing, for writing a file and for a -content address; the second interns, bottom up, the instances of the -constructors whose templates it is given, for a term that did not come through the rewrite -(a toplevel query, `read_term/2`, a module that did not opt in, a term built -by `=..`). +A TERM THAT IS NOT INTERNED STAYS AS IT IS (user, 2026-09-26): a plain +compound of its constructor, whose arguments are represented in turn. The +REPRESENTATION of a term is its Id when a template of its constructor +matches it, and the term itself, with represented arguments, otherwise. + +THE BOUNDARY: `externalized/2` replaces every Id by its term, recursively, +for printing, for writing a file and for a content address. +`internalized/3` declares the templates it is given and represents, bottom +up, the instances of their constructors, for a term that did not come +through the rewrite (a toplevel query, `read_term/2`, a module that did not +opt in, a term built by `=..`). `declared/1` only declares templates, for a +program whose constructors are made at run time. `is_id/1` tells an Id from +any other value. `represented(?Layer, ?Representation)` relates one layer, a +constructor applied to represented arguments, to its representation. `:- hash_consing:rewritten(Templates).` OPTS A FILE IN (user ruling, 2026-09-17: opt-in per file, the constructors passed to the directive, no -setting). Every clause read after it in that file, included files counted, -has each occurrence of a listed constructor turned into an -Id pattern and a call of `intern/2`, the direction of each call decided at -run time, so the file is written as the program that does not intern and -needs no mode declaration. Several directives in one file add up. An empty -list rewrites nothing. The library checks no consistency between files: -files that pass one constructor to each other must both list it, which the -user arranges, for instance with one included file (user ruling, -2026-09-17). +setting). It declares the templates as `declared/1` does, and every clause +read after it in that file, included files counted, has each occurrence of a +constructor of the list rewritten as below, the direction of each call +decided at run time, so the file is written as the program that does not +intern and needs no mode declaration. Several directives in one file add up, +each declaring whole lists. An empty list rewrites nothing. The library +checks no consistency between files: files that pass one constructor to each +other must both list it, which the user arranges, for instance with one +included file (user ruling, 2026-09-17). + +AN OCCURRENCE IS CLASSIFIED while the file loads, by comparing its source +pattern with each template of its constructor: every instance of the pattern +matches the template, none does, or some do. + + must intern a template matches every instance: an Id pattern and + a call of `intern/2`; the shape is written in when the + first template that some instance matches matches them + all and each root it records is in the pattern + must not intern no template matches any instance: the layer itself, + written where the occurrence stood + undetermined otherwise: a fresh variable where the occurrence + stood, and a call of `represented/2` + +A pattern whose variables are all filled with an atom no template names is +taken by a template only when that template has `_` or `*` there, and such a +template takes every instance, so no occurrence is missed as must intern. +The other two tests treat each occurrence of a variable apart, so a pattern +with a repeated variable can be classified undetermined, or left without its +shape, although its instances decide it; that is correct and unindexed. An +undetermined occurrence at the top of a head costs its clause the first +argument indexing of that argument: the clause is a candidate for every +call, so a call that a clause before it answers leaves a choice point on it +(measured 2026-09-26: with such a clause first in its predicate, calls on an +Id, a plain term and the other constructors' Ids were deterministic; with it +last, each of them left a choice point). Such a clause is not split into an +Id version and a plain version: called with that argument unbound, both +would run the body, and a cut in the first would prune the second. THE REWRITE OF A CLAUSE: - head fast path when the Handle of every top-level head occurrence - is bound: look them up top down, then run the body, which - keeps the last call; otherwise look up the bound ones top - down, insert the ground ones bottom up, run the body, insert - the rest bottom up (an instantiation error when a term is - still not ground) - body goal when the variables of its terms are bound: insert bottom up - and call; otherwise insert the ground ones, call, and then - settle every occurrence top down (a lookup when the call - bound the Id, an insertion when it made the term ground, an - instantiation error when neither) - ground an occurrence that is ground in the source is interned while - the file loads and its Id is written into the clause + head fast path when every top-level occurrence is given (the + handle of an Id pattern bound; the variable of an undetermined + occurrence bound, and not to an Id pattern whose handle is + unbound): relate them to their layers top down, then run the + body, which keeps the last call; otherwise relate the given + ones top down, represent the ground ones bottom up, run the + body, represent the rest bottom up (an instantiation error + when a term that must be interned is still not ground, or an + undetermined one is still undecided) + body goal when the variables of its layers are bound: represent bottom + up and call; otherwise intern the ground ones and decide each + undetermined one (its Id, an Id pattern whose handle is + unbound, or the layer itself; an instantiation error when + still undecided), call, and then settle every occurrence top + down (a lookup when the call bound the Id, an insertion when + it made the term ground, an instantiation error when + neither) + ground an occurrence that is ground in the source is represented + while the file loads, and its Id or its layer is written into + the clause Control constructs (`,`, `;`, `->`, `*->`, `\+`, `call/1`, `forall/2`, the goal of `findall/3` and of `catch/3`, a module-qualified goal) are rewritten @@ -182,16 +251,33 @@ in the catcher of `catch/3`, or in a DCG rule raises while the file loads. Directives are not rewritten. -TWO RULES FOR A FILE THAT OPTS IN. (1) An instance of a listed constructor is -settled, ground or its Id bound, by the end of the goal it is handed to; a -term handed over half built and filled in later raises an instantiation -error. (2) Reflection sees Ids: `=..`, `functor/3`, `arg/3`, `write/1`, +TWO RULES FOR A FILE THAT OPTS IN. (1) An instance of a listed constructor +whose interning is undetermined is decided when it is handed to a goal: what +is bound of it settles whether a template matches every completion or none +does, or the call raises an instantiation error; and every instance is +settled, ground or its Id bound, by the end of the goal it is handed to. The +first half is a DOWNGRADE of the rule before 0.2.0, which asked only for the +second: a term that matches no template stays as it is (user, 2026-09-26), +and a callee could not otherwise tell whether to receive an Id or a plain +term. (2) Reflection sees Ids: `=..`, `functor/3`, `arg/3`, `write/1`, `variant_sha1/2`, `term_hash/2` and ordering whose result depends on the order see `'__hash_consed_Name/Arity'(Handle)`. Code that reads structure calls `externalized/2` first, and code that builds an instance with them calls -`internalized/3` after; an instance left uninterned fails to unify at every -rewritten position. Using an Id as an opaque key, whose result does not -depend on the order (an assoc key, a sort to remove duplicates), is fine. +`internalized/3` after; an instance that must be interned and is left +uninterned fails to unify at every rewritten position. Using an Id as an +opaque key, whose result does not depend on the order (an assoc key, a sort +to remove duplicates), is fine. + +THREADS SHARE THE STORE WHEN THEY INSTALL IT. The store and the spellings +of the shapes are tries in two global variables of the thread that loaded +this module, `hash_consing_store` and `hash_consing_spellings`, and a +thread made later starts without them; a thread that sets both to the +loading thread's tries (read there with `nb_getval/2`, set with +`nb_setval/2`) declares, interns and looks up alongside the others, with +the answers one thread would give. A lookup that finds its key takes no +lock. A declaration, an insertion into the store and a new spelling each +take a mutex (`hash_consing_templates`, `hash_consing_store`, +`hash_consing_spellings`) and look again under it before they write. THIS MODULE REFLECTS ON SOURCE CLAUSES with `=..` while a file loads, a mechanical boundary; nothing here chooses behaviour at run time by @@ -227,7 +313,7 @@ */ :- use_module(library(error), [must_be/2]). -:- use_module(library(lists), [reverse/2, append/3]). +:- use_module(library(lists), [reverse/2, member/2]). :- initialization(stores_created). @@ -256,42 +342,150 @@ intern(Term, Id) :- upserted(Term, Id). -%! upserted(+Term, ?Id) insert Term unless it is stored, and answer its Id. +%! upserted(+Term, ?Id) when a template of Term's constructor matches it, +% insert Term unless it is stored, and answer its Id; fail, inserting +% nothing, when none does. upserted(Term, Id) :- ( ground(Term) -> true ; throw(error(instantiation_error, context(hash_consing:intern/2, Term-Id))) ), + functor(Term, Name, Arity), + templates_known(Name, Arity, hash_consing:intern/2, Templates, Kind), + first_template_recorded(Templates, Term, Structure), nb_getval(hash_consing_store, Trie), - ( trie_lookup(Trie, Term, Handle) - -> true - ; trie_insert(Trie, Term, pending, Handle), - trie_update(Trie, Term, Handle) + ( trie_lookup(Trie, Term, Found) + -> settled_handle(Trie, Term, Found, Handle) + ; with_mutex(hash_consing_store, handle_inserted(Trie, Term, Handle)) ), - functor(Term, Name, Arity), - configuration_of(Name, Arity, Configuration), - id_of(Configuration, Term, Name, Arity, Handle, Id). + id_built(Name, Arity, Kind, Structure, Handle, Id). + +% handle_inserted(+Trie, +Term, -Handle): Term looked up again and, when it +% is still absent, inserted, under the mutex `hash_consing_store`. Two +% threads that share the store and both miss Term would otherwise both +% insert it, and the second trie_insert/4 raises +% `permission_error(modify, trie_key, Term)` (measured 2026-09-30: eight +% threads interning the same 20000 terms raised in 5 of 5 runs). A lookup +% that finds Term takes no mutex. + +handle_inserted(Trie, Term, Handle) :- + ( trie_lookup(Trie, Term, Found) + -> settled_handle(Trie, Term, Found, Handle) + ; sig_atomic(inserted(Trie, Term, Handle)) + ). -id_of(root_only, _, Name, Arity, Handle, Id) :- - id_name(Name, Arity, IdName), - compound_name_arguments(Id, IdName, [Handle]). -id_of(shaped(Records), Term, Name, Arity, Handle, Id) :- - id_name(Name, Arity, IdName), - ( term_shape(Term, Records, [], Shape) - -> true - ; throw(error(instantiation_error, context(hash_consing:intern/2, Term))) +% inserted(+Trie, +Term, -Handle): the insertion and the write-back of the +% key's own handle as its value, run under `sig_atomic/1` by +% handle_inserted/3, so +% that a signal (a `call_with_time_limit/2` expiring) waits until both are +% done. `call_with_inference_limit/3` is no signal: its limit can still +% fall between the two and leave the value `pending` (measured 2026-09-27: +% interning a fresh two-argument term under a limit of 9 inferences left it +% `pending`, and the next lookup handed `pending` to `trie_term/2`, which +% raised `type_error(address, pending)`). settled_handle/4 repairs such a +% key at its next lookup. + +inserted(Trie, Term, Handle) :- + trie_insert(Trie, Term, pending, Handle), + trie_update(Trie, Term, Handle). + +% settled_handle(+Trie, +Term, +Found, -Handle): the handle of Term's node, +% Found when the value was written back, and otherwise, when an +% interrupted insertion left `pending`, the node's own handle, read with +% `'$trie_gen_node'/3` (SWI-Prolog's generator of a trie's keys with their +% nodes, here with the key bound) and written back. The repair may itself +% be interrupted between its two steps; the key then stays `pending` and +% is repaired at its next lookup. + +settled_handle(Trie, Term, pending, Handle) :- + !, + '$trie_gen_node'(Trie, Term, Handle), + trie_update(Trie, Term, Handle). +settled_handle(_, _, Handle, Handle). + +%! represented(?Layer, ?Representation) Representation represents Layer, a +% constructor applied to represented arguments: its Id when a template of +% the constructor matches it, Layer itself otherwise. +% +% Given an Id of the constructor, Layer is its stored term, or, when the +% handle is unbound, Layer is interned into it and must be ground. Given +% a plain term of the constructor, it is Layer, and no template may match +% any completion of it: it is then not the representation of a term that +% must be interned. Given nothing, Layer is represented as far as what is +% bound of it decides: its Id when it is ground and a template matches it, +% an Id pattern whose handle is unbound when every completion must be +% interned, Layer itself when none may be, and an instantiation error when +% what is bound does not decide. Any other value fails. + +represented(Layer, Representation) :- + ( var(Layer) + -> throw(error(instantiation_error, + context(hash_consing:represented/2, Layer-Representation))) + ; true ), - compound_name_arguments(Id, IdName, [Shape, Handle]). + functor(Layer, Name, Arity), + templates_known(Name, Arity, hash_consing:represented/2, Templates, Kind), + id_name(Name, Arity, IdName), + ( var(Representation) + -> representation_made(Templates, Kind, Name, Arity, Layer, Representation) + ; id_parts(Representation, IdName, _, Handle) + -> ( nonvar(Handle) + -> trie_term(Handle, Stored), + Layer = Stored + ; ground(Layer) + -> upserted(Layer, Representation) + ; throw(error(instantiation_error, context(hash_consing:represented/2, Layer))) + ) + ; functor(Representation, Name, Arity) + -> Layer = Representation, + value_classified(Templates, Layer, Class, _), + Class == must_not_intern + ). + +representation_made(Templates, Kind, Name, Arity, Layer, Representation) :- + value_classified(Templates, Layer, Class, Structure), + ( Class == must_intern + -> ( ground(Layer) + -> upserted(Layer, Representation) + ; id_built(Name, Arity, Kind, Structure, _, Representation) + ) + ; Class == must_not_intern + -> Representation = Layer + ; throw(error(instantiation_error, context(hash_consing:represented/2, Layer))) + ). + +%! represented_settled(+Layer, ?Representation) represented/2 at the end of +% a rewritten head, where rule (1) of the module comment leaves no Id +% pattern with an unbound handle: such a pattern raises an instantiation +% error. + +represented_settled(Layer, Representation) :- + represented(Layer, Representation), + ( id_parts(Representation, _, _, Handle), + var(Handle) + -> throw(error(instantiation_error, context(hash_consing:represented/2, Layer))) + ; true + ). + +%! is_id(+Value) Value is an Id: an Id functor this process made, applied +% to a bound handle. + +is_id(Value) :- + id_parts(Value, _, _, Handle), + nonvar(Handle). %! id_parts(+Value, -IdName, -Shape, -Handle) Value is an Id or an Id -% pattern; Shape is `none` for a constructor without a shape. Fails on any -% other value. +% pattern: its functor is one id_name/3 made, which the first argument +% index of id_constructor/3 finds without scanning the name (the prefix +% test it replaces took 30 percent of a lambda_jit read, 2026-09-26). +% Shape is `none` for a constructor without a shape. Fails on any other +% value. id_parts(Value, IdName, Shape, Handle) :- compound(Value), compound_name_arity(Value, IdName, Arity), - sub_atom(IdName, 0, _, _, '__hash_consed_'), + id_constructor(IdName, _, _), id_arguments(Arity, Value, Shape, Handle). id_arguments(1, Value, none, Handle) :- @@ -300,15 +494,19 @@ arg(1, Value, Shape), arg(2, Value, Handle). -%! id_pattern(+Name, +Arity, -Id, -Handle) an Id pattern of the constructor -% as it is configured, its Handle and, if it has one, its shape unbound. +%! id_built(+Name, +Arity, +Kind, +Structure, ?Handle, -Id) the Id, or +% the Id pattern, of the constructor with the handle Handle: no shape when +% Kind is `root_only`, an unbound shape when Structure is `unknown`, and +% otherwise the spelling of Structure. -id_pattern(Name, Arity, Id, Handle) :- +id_built(Name, Arity, Kind, Structure, Handle, Id) :- id_name(Name, Arity, IdName), - configuration_of(Name, Arity, Configuration), - ( Configuration == root_only + ( Kind == root_only -> compound_name_arguments(Id, IdName, [Handle]) - ; compound_name_arguments(Id, IdName, [_, Handle]) + ; Structure == unknown + -> compound_name_arguments(Id, IdName, [_, Handle]) + ; structure_spelled(Structure, Shape), + compound_name_arguments(Id, IdName, [Shape, Handle]) ). %! id_name(+Name, +Arity, -IdName) the functor name of the Ids of the @@ -318,67 +516,160 @@ :- dynamic id_constructor/3. % id_constructor(IdName, Name, Arity) id_name(Name, Arity, IdName) :- + ( known_id_name(Name, Arity, Known) + -> IdName = Known + ; with_mutex(hash_consing_templates, id_name_made(Name, Arity, IdName)) + ). + +% id_name_made(+Name, +Arity, -IdName): the name looked up again under the +% mutex `hash_consing_templates`, and made when it is still unknown. +% id_constructor/3 is asserted before known_id_name/3, so a thread that +% finds the name without the mutex also finds the fact id_parts/4 reads. + +id_name_made(Name, Arity, IdName) :- ( known_id_name(Name, Arity, Known) -> IdName = Known ; format(atom(Made), '__hash_consed_~w/~d', [Name, Arity]), - assertz(known_id_name(Name, Arity, Made)), assertz(id_constructor(Made, Name, Arity)), + assertz(known_id_name(Name, Arity, Made)), IdName = Made ). -% ---- the configuration of a constructor ---- +% ---- the templates of a constructor ---- -:- dynamic constructor_configuration/3. % constructor_configuration(Name, Arity, Configuration) +% A TEMPLATE IS KEPT PARSED, `template(Name/Arity, Arguments)` with one of +% `ignored` (for `_`), `root` (for `*`) or a nested template per argument, +% ground, so that two declarations of a constructor compare with `==`. -%! configuration_of(+Name, +Arity, -Configuration) `root_only`, or -% `shaped(Records)` with one record per argument, `ignored` or -% `root(Templates)`, Templates a list of `below(Name/Arity, Records)` for -% the nested templates; a constructor met without a declaration is -% registered as `root_only`. +:- dynamic constructor_templates/4. % constructor_templates(Name, Arity, Templates, Kind) -configuration_of(Name, Arity, Configuration) :- - ( constructor_configuration(Name, Arity, Known) - -> Configuration = Known - ; assertz(constructor_configuration(Name, Arity, root_only)), - Configuration = root_only - ). +%! declared(+Templates) the constructors of the list declared for this +% process, each with its templates in the order of the list. -%! configuration_registered(+Name, +Arity, +Configuration) the one -% configuration of the constructor in this process; another raises. +declared(Templates) :- + templates_declared(Templates, hash_consing:declared/1, _). -configuration_registered(Name, Arity, Configuration) :- - ( constructor_configuration(Name, Arity, Known) - -> ( Known == Configuration - -> true - ; throw(error(permission_error(reconfigure, interned_constructor, Name/Arity), - context(hash_consing:rewritten/1, - configured(Known)-declared(Configuration)))) - ) - ; assertz(constructor_configuration(Name, Arity, Configuration)) +%! templates_known(+Name, +Arity, +Context, -Templates, -Kind) the declared +% templates of the constructor, and `root_only` or `shaped`; raises when +% the constructor has none. + +templates_known(Name, Arity, Context, Templates, Kind) :- + ( constructor_templates(Name, Arity, Templates, Kind) + -> true + ; throw(error(existence_error(templates, Name/Arity), context(Context, _))) ). -%! specification(+Template, -Name, -Arity, -Configuration) an element of a -% constructor list, a template, in the form the library keeps: ground, so -% that two declarations of one constructor compare with `==`. +%! templates_declared(+Templates, +Context, -Constructors) the list parsed +% and grouped by constructor, in the order of first appearance; every group +% checked before any is registered; Constructors the `Name/Arity` of the +% groups. Raises, registering nothing, on a malformed or unreachable +% template and on a constructor already declared with another list. + +templates_declared(Templates, Context, Constructors) :- + must_be(list, Templates), + templates_parsed(Templates, Context, Parsed), + parsed_constructors(Parsed, [], Reversed), + reverse(Reversed, Constructors), + constructors_groups(Constructors, Parsed, Groups), + with_mutex(hash_consing_templates, groups_declared(Groups, Context)). + +% groups_declared(+Groups, +Context): the groups checked against the lists +% already declared, then registered, as one step under the mutex +% `hash_consing_templates`. Two threads declaring a constructor at once +% would otherwise both find it undeclared and both register it (measured +% 2026-09-30: eight threads declaring the same 2000 constructors left 3924 +% registrations and 3631 Id names, and is_id/1 answered once for each Id +% name of its constructor, since id_parts/4 reads them). + +groups_declared(Groups, Context) :- + groups_checked(Groups, Context), + groups_registered(Groups). + +parsed_constructors([], Constructors, Constructors). +parsed_constructors([_-template(Constructor, _) | Parsed], Seen, Constructors) :- + ( memberchk(Constructor, Seen) + -> parsed_constructors(Parsed, Seen, Constructors) + ; parsed_constructors(Parsed, [Constructor | Seen], Constructors) + ). -specification(Template, _, _, _) :- - var(Template), - !, - throw(error(instantiation_error, context(hash_consing:rewritten/1, _))). -specification(Template, Name, Arity, Configuration) :- - callable(Template), - Template \== (*), - Template \= (_ ; _), - !, - compound_name_arguments_or_atom(Template, Name, Arguments), - length(Arguments, Arity), - arguments_records(Arguments, Records), - ( all_ignored(Records) - -> Configuration = root_only - ; Configuration = shaped(Records) +% A GROUP is `group(Name/Arity, Written, Templates)`: the templates of one +% constructor as written and as parsed, in the order of the list. + +constructors_groups([], _, []). +constructors_groups([Constructor | Constructors], Parsed, [group(Constructor, Written, Templates) | Groups]) :- + constructor_templates_parsed(Parsed, Constructor, Written, Templates), + constructors_groups(Constructors, Parsed, Groups). + +constructor_templates_parsed([], _, [], []). +constructor_templates_parsed([Template-Parsed | Pairs], Constructor, Written, Templates) :- + ( Parsed = template(Constructor, _) + -> Written = [Template | WrittenRest], + Templates = [Parsed | TemplatesRest] + ; Written = WrittenRest, + Templates = TemplatesRest + ), + constructor_templates_parsed(Pairs, Constructor, WrittenRest, TemplatesRest). + +groups_checked([], _). +groups_checked([group(Name/Arity, Written, Templates) | Groups], Context) :- + templates_reachable(Written, Templates, [], Context), + ( constructor_templates(Name, Arity, Known, _), + Known \== Templates + -> templates_written(Known, KnownWritten), + throw(error(permission_error(reconfigure, interned_constructor, Name/Arity), + context(Context, configured(KnownWritten)-declared(Written)))) + ; true + ), + groups_checked(Groups, Context). + +%! templates_reachable(+Written, +Templates, +Earlier, +Context) no +% template is always taken first by one template before it. + +templates_reachable([], [], _, _). +templates_reachable([Template | Written], [Parsed | Templates], Earlier, Context) :- + ( member(EarlierTemplate, Earlier), + template_covers(EarlierTemplate, Parsed) + -> throw(error(domain_error(reachable_template, Template), context(Context, _))) + ; templates_reachable(Written, Templates, [Parsed | Earlier], Context) ). -specification(Template, _, _, _) :- - throw(error(type_error(constructor_template, Template), _)). + +%! template_covers(+Covering, +Covered) every term Covered matches, +% Covering matches too. + +template_covers(template(Constructor, Coverings), template(Constructor, Covereds)) :- + arguments_cover(Coverings, Covereds). + +arguments_cover([], []). +arguments_cover([Covering | Coverings], [Covered | Covereds]) :- + argument_covers(Covering, Covered), + arguments_cover(Coverings, Covereds). + +argument_covers(ignored, _). +argument_covers(root, _). +argument_covers(template(Constructor, Coverings), template(Constructor, Covereds)) :- + arguments_cover(Coverings, Covereds). + +groups_registered([]). +groups_registered([group(Name/Arity, _, Templates) | Groups]) :- + ( constructor_templates(Name, Arity, _, _) + -> true + ; templates_kind(Templates, Kind), + id_name(Name, Arity, _), + assertz(constructor_templates(Name, Arity, Templates, Kind)) + ), + groups_registered(Groups). + +% A constructor whose one template records nothing has Ids without a +% shape; any other list has a template that records something. + +templates_kind([template(_, Arguments)], root_only) :- + all_ignored(Arguments), + !. +templates_kind(_, shaped). + +all_ignored([]). +all_ignored([ignored | Arguments]) :- + all_ignored(Arguments). compound_name_arguments_or_atom(Term, Name, Arguments) :- ( atom(Term) @@ -387,112 +678,261 @@ ; compound_name_arguments(Term, Name, Arguments) ). -arguments_records([], []). -arguments_records([Argument | Arguments], [Record | Records]) :- - argument_record(Argument, Record), - arguments_records(Arguments, Records). +%! templates_parsed(+Templates, +Context, -Pairs) each template paired with +% its parsed form, `Template-Parsed`. -argument_record(Argument, ignored) :- +templates_parsed([], _, []). +templates_parsed([Template | Templates], Context, [Template-Parsed | Pairs]) :- + template_parsed(Template, Context, Parsed), + templates_parsed(Templates, Context, Pairs). + +template_parsed(Template, Context, _) :- + var(Template), + !, + throw(error(instantiation_error, context(Context, _))). +template_parsed(Template, Context, template(Name/Arity, Arguments)) :- + callable(Template), + Template \== (*), + !, + compound_name_arguments_or_atom(Template, Name, TemplateArguments), + length(TemplateArguments, Arity), + arguments_parsed(TemplateArguments, Context, Arguments). +template_parsed(Template, Context, _) :- + throw(error(type_error(constructor_template, Template), context(Context, _))). + +arguments_parsed([], _, []). +arguments_parsed([Argument | Arguments], Context, [Parsed | Parseds]) :- + argument_parsed(Argument, Context, Parsed), + arguments_parsed(Arguments, Context, Parseds). + +argument_parsed(Argument, _, ignored) :- var(Argument), !. -argument_record(*, root([])) :- +argument_parsed(*, _, root) :- !. -argument_record(Alternatives, root(Templates)) :- - alternatives_list(Alternatives, List), - templates_below(List, Templates). - -alternatives_list(Alternatives, List) :- - ( nonvar(Alternatives), - Alternatives = (Left ; Right) - -> alternatives_list(Left, LeftList), - alternatives_list(Right, RightList), - append(LeftList, RightList, List) - ; List = [Alternatives] +argument_parsed(Argument, Context, Parsed) :- + template_parsed(Argument, Context, Parsed). + +%! templates_written(+Templates, -Written) parsed templates written back as +% a user writes them, for an error to show. + +templates_written([], []). +templates_written([Template | Templates], [Written | Writtens]) :- + template_written(Template, Written), + templates_written(Templates, Writtens). + +template_written(template(Name/_, Arguments), Written) :- + arguments_written(Arguments, WrittenArguments), + ( WrittenArguments == [] + -> Written = Name + ; compound_name_arguments(Written, Name, WrittenArguments) ). -% A nested template whose own arguments are all ignored records nothing -% below the root, which the root already says, and is left out. -templates_below([], []). -templates_below([Template | Templates], Belows) :- - specification(Template, Name, Arity, Configuration), - ( Configuration = shaped(Records) - -> Belows = [below(Name/Arity, Records) | Rest] - ; Belows = Rest - ), - templates_below(Templates, Rest), - ( memberchk(below(Name/Arity, _), Rest) - -> throw(error(domain_error(one_template_per_constructor, Template), _)) - ; true - ). +arguments_written([], []). +arguments_written([Argument | Arguments], [Written | Writtens]) :- + argument_written(Argument, Written), + arguments_written(Arguments, Writtens). -all_ignored([]). -all_ignored([ignored | Records]) :- - all_ignored(Records). +argument_written(ignored, _). +argument_written(root, *). +argument_written(template(Constructor, Arguments), Written) :- + template_written(template(Constructor, Arguments), Written). % ---- shapes ---- % A STRUCTURE is what a shape atom spells: a list, one description per -% recorded argument, `other` for an argument that is no Id and -% `constructor(Name/Arity, Structure)` otherwise, the inner structure being -% `none` where no nested template goes on. - -%! term_shape(+Term, +Records, +Occurrences, -Atom) the shape atom of Term -% under its template. Fails when the term does not determine it: a -% recorded argument is an unbound variable, or a nested template needs the -% arguments of an Id pattern that is neither among Occurrences, the -% `occurrence(Term, Id, Handle)` of the clause being rewritten, nor stored. -% A ground Term always determines its shape. - -term_shape(Term, Records, Occurrences, Atom) :- - compound_name_arguments_or_atom(Term, _, Arguments), - arguments_descriptions(Records, Arguments, Occurrences, Structure), - nb_getval(hash_consing_spellings, Spellings), - ( trie_lookup(Spellings, Structure, Known) - -> Atom = Known - ; structure_atom(Structure, Atom), - trie_insert(Spellings, Structure, Atom) +% recorded argument, `other` for an argument that stands for a number or a +% string and `constructor(Name/Arity, Inner)` otherwise, Inner being `none` +% where nothing is recorded below and the list of the descriptions below +% otherwise. While a value leaves a recorded root open its description is +% `unknown`, and a structure holding one is not spelled. +% +% THE SAME COMPARISON serves the rewrite, on the source pattern of an +% occurrence, and the store, on a term whose arguments are represented: a +% value's root and arguments are read off a plain term or a pattern as they +% are and off an Id through the store, and a variable, or the arguments of +% an Id pattern whose handle is unbound, are open. + +%! value_classified(+Templates, +Value, -Class, -Structure) Class is +% `must_intern` when a template matches every term Value stands for, +% `must_not_intern` when no template matches any, `undetermined` +% otherwise. Structure is what the first template that matches some such +% term records, when that template matches them all and every root it +% records is known; `unknown` otherwise. + +value_classified(Templates, Value, Class, Structure) :- + templates_relations(Templates, Value, Relations), + relations_class(Relations, Class), + relations_structure(Relations, Structure). + +templates_relations([], _, []). +templates_relations([Template | Templates], Value, [Relation-Descriptions | Relations]) :- + template_relation(Template, Value, Relation, Descriptions), + templates_relations(Templates, Value, Relations). + +relations_class(Relations, must_intern) :- + memberchk(instance-_, Relations), + !. +relations_class(Relations, must_not_intern) :- + \+ memberchk(overlap-_, Relations), + !. +relations_class(_, undetermined). + +relations_structure([], unknown). +relations_structure([Relation-Descriptions | Relations], Structure) :- + ( Relation == disjoint + -> relations_structure(Relations, Structure) + ; Relation == instance, + descriptions_known(Descriptions) + -> Structure = Descriptions + ; Structure = unknown ). -arguments_descriptions([], [], _, []). -arguments_descriptions([ignored | Records], [_ | Arguments], Occurrences, Descriptions) :- - !, - arguments_descriptions(Records, Arguments, Occurrences, Descriptions). -arguments_descriptions([root(Templates) | Records], [Argument | Arguments], Occurrences, - [Description | Descriptions]) :- - argument_description(Argument, Templates, Occurrences, Description), - arguments_descriptions(Records, Arguments, Occurrences, Descriptions). +descriptions_known([]). +descriptions_known([Description | Descriptions]) :- + description_known(Description), + descriptions_known(Descriptions). -argument_description(Argument, _, _, _) :- - var(Argument), +description_known(other). +description_known(constructor(_, Inner)) :- + ( Inner == none + -> true + ; is_list(Inner), + descriptions_known(Inner) + ). + +%! first_template_recorded(+Templates, +Term, -Structure) what the first +% template that matches the ground Term records; fails when none does. + +first_template_recorded([Template | Templates], Term, Structure) :- + template_relation(Template, Term, Relation, Descriptions), + ( Relation == instance + -> Structure = Descriptions + ; first_template_recorded(Templates, Term, Structure) + ). + +%! template_relation(+Template, +Value, -Relation, -Descriptions) whether +% every term Value stands for matches the template (`instance`), none does +% (`disjoint`) or some do (`overlap`), and what the template records on +% them. Value's own root is the template's constructor. + +template_relation(template(_, TemplateArguments), Value, Relation, Descriptions) :- + compound_name_arguments_or_atom(Value, _, Arguments), + arguments_relation(TemplateArguments, Arguments, instance, Relation, [], Reversed), + reverse(Reversed, Descriptions). + +arguments_relation([], [], Relation, Relation, Descriptions, Descriptions). +arguments_relation([TemplateArgument | TemplateArguments], [Argument | Arguments], + Relation0, Relation, Descriptions0, Descriptions) :- + argument_relation(TemplateArgument, Argument, ArgumentRelation, Descriptions0, Descriptions1), + relation_combined(Relation0, ArgumentRelation, Relation1), + arguments_relation(TemplateArguments, Arguments, Relation1, Relation, Descriptions1, Descriptions). + +argument_relation(ignored, _, instance, Descriptions, Descriptions). +argument_relation(root, Argument, instance, Descriptions, [Description | Descriptions]) :- + value_root(Argument, Root), + root_description(Root, Description). +argument_relation(template(Name/Arity, TemplateArguments), Argument, Relation, + Descriptions, [Description | Descriptions]) :- + value_view(Argument, View), + nested_relation(View, Name, Arity, TemplateArguments, Relation, Description). + +nested_relation(open, Name, Arity, _, overlap, constructor(Name/Arity, unknown)). +nested_relation(other, Name, Arity, _, disjoint, constructor(Name/Arity, unknown)). +nested_relation(layer(ViewName/ViewArity, Arguments), Name, Arity, TemplateArguments, + Relation, constructor(Name/Arity, Inner)) :- + ( ViewName/ViewArity == Name/Arity + -> arguments_relation(TemplateArguments, Arguments, instance, Relation, [], Reversed), + reverse(Reversed, Descriptions), + ( Descriptions == [] + -> Inner = none + ; Inner = Descriptions + ) + ; Relation = disjoint, + Inner = unknown + ). + +relation_combined(disjoint, _, disjoint) :- + !. +relation_combined(_, disjoint, disjoint) :- + !. +relation_combined(instance, instance, instance) :- + !. +relation_combined(_, _, overlap). + +root_description(open, unknown). +root_description(other, other). +root_description(Name/Arity, constructor(Name/Arity, none)). + +%! value_root(+Value, -Root) the root constructor of the term Value stands +% for, `Name/Arity`, read off an Id's functor name without a lookup; +% `open` for a variable, `other` for a number or a string. + +value_root(Value, open) :- + var(Value), + !. +value_root(Value, Name/Arity) :- + id_parts(Value, IdName, _, _), !, - fail. -argument_description(Argument, Templates, Occurrences, constructor(Name/Arity, Inner)) :- - id_parts(Argument, IdName, _, _), + id_constructor(IdName, Name, Arity). +value_root(Value, Name/Arity) :- + compound(Value), + !, + compound_name_arity(Value, Name, Arity). +value_root(Value, Value/0) :- + atom(Value), + !. +value_root(_, other). + +%! value_view(+Value, -View) `layer(Name/Arity, Arguments)`, the root and +% the arguments of the term Value stands for, an Id's read from the store +% and open while its handle is unbound; `open` for a variable; `other` for +% a number or a string. + +value_view(Value, open) :- + var(Value), + !. +value_view(Value, layer(Name/Arity, Arguments)) :- + id_parts(Value, IdName, _, Handle), !, id_constructor(IdName, Name, Arity), - ( memberchk(below(Name/Arity, Records), Templates) - -> id_term(Argument, Occurrences, Below), - compound_name_arguments_or_atom(Below, _, BelowArguments), - arguments_descriptions(Records, BelowArguments, Occurrences, Inner) - ; Inner = none + ( nonvar(Handle) + -> trie_term(Handle, Stored), + compound_name_arguments_or_atom(Stored, _, Arguments) + ; length(Arguments, Arity) ). -argument_description(_, _, _, other). +value_view(Value, layer(Name/Arity, Arguments)) :- + compound(Value), + !, + compound_name_arguments(Value, Name, Arguments), + length(Arguments, Arity). +value_view(Value, layer(Value/0, [])) :- + atom(Value), + !. +value_view(_, other). -%! id_term(+Id, +Occurrences, -Term) the term of an Id: stored, when its -% Handle is bound; the occurrence's, when it is a pattern of the clause -% being rewritten; fails otherwise. +%! structure_spelled(+Structure, -Atom) the shape atom of a structure, +% remembered in the trie of spellings so that it is built once. -id_term(Id, Occurrences, Term) :- - id_parts(Id, _, _, Handle), - ( nonvar(Handle) - -> trie_term(Handle, Term) - ; occurrence_term(Occurrences, Id, Term) +structure_spelled(Structure, Atom) :- + nb_getval(hash_consing_spellings, Spellings), + ( trie_lookup(Spellings, Structure, Known) + -> Atom = Known + ; with_mutex(hash_consing_spellings, spelling_inserted(Spellings, Structure, Atom)) ). -occurrence_term([occurrence(Candidate, CandidateId, _) | Occurrences], Id, Term) :- - ( CandidateId == Id - -> Term = Candidate - ; occurrence_term(Occurrences, Id, Term) +% spelling_inserted(+Spellings, +Structure, -Atom): the spelling looked up +% again and, when it is still absent, made and inserted, under the mutex +% `hash_consing_spellings`. Two threads that both miss a structure would +% otherwise both insert it, and the second trie_insert/3 fails, which +% fails its interning (measured 2026-09-30: eight threads spelling the +% same 2000 shapes). + +spelling_inserted(Spellings, Structure, Atom) :- + ( trie_lookup(Spellings, Structure, Known) + -> Atom = Known + ; structure_atom(Structure, Atom), + trie_insert(Spellings, Structure, Atom) ). %! structure_atom(+Structure, -Atom) the spelling: descriptions joined by @@ -545,21 +985,14 @@ externalized(Argument, External), arguments_externalized(Arguments, Externals). -%! internalized(+Constructors, +External, -TermWithIds) every instance of a -% constructor in Constructors interned, bottom up; an Id is kept as it is. -% The list's elements are templates, as in the directive, and register the -% same configurations. +%! internalized(+Templates, +External, -TermWithIds) the templates declared +% as declared/1 declares them, then every instance of their constructors +% represented, bottom up: its Id when a template matches it, the plain +% term otherwise; an Id is kept as it is. -internalized(Constructors, External, TermWithIds) :- - must_be(list, Constructors), - specifications_indicators(Constructors, Indicators), - term_internalized(External, Indicators, TermWithIds). - -specifications_indicators([], []). -specifications_indicators([Element | Elements], [Name/Arity | Indicators]) :- - specification(Element, Name, Arity, Configuration), - configuration_registered(Name, Arity, Configuration), - specifications_indicators(Elements, Indicators). +internalized(Templates, External, TermWithIds) :- + templates_declared(Templates, hash_consing:internalized/3, Constructors), + term_internalized(External, Constructors, TermWithIds). term_internalized(Term, _, Internal) :- var(Term), @@ -588,10 +1021,22 @@ term_internalized(Argument, Indicators, Internal), arguments_internalized(Arguments, Indicators, Internals). -instance_internalized(Indicator, Indicators, Term, Internal) :- - ( memberchk(Indicator, Indicators) - -> intern(Term, Internal) - ; Internal = Term +% An instance whose templates were given is represented; one that is not +% ground stays plain when no completion of it can match, and raises +% otherwise, as intern/2 does on a term that is not ground. + +instance_internalized(Name/Arity, Constructors, Layer, Internal) :- + ( memberchk(Name/Arity, Constructors) + -> ( ground(Layer) + -> represented(Layer, Internal) + ; constructor_templates(Name, Arity, Templates, _), + value_classified(Templates, Layer, Class, _), + ( Class == must_not_intern + -> Internal = Layer + ; throw(error(instantiation_error, context(hash_consing:internalized/3, Layer))) + ) + ) + ; Internal = Layer ). % ---- the directive ---- @@ -601,24 +1046,22 @@ :- dynamic registered_constructor/3. % registered_constructor(SourceFile, Name, Arity) -rewritten(Constructors) :- - must_be(list, Constructors), +rewritten(Templates) :- + must_be(list, Templates), ( prolog_load_context(source, File) -> true ; throw(error(context_error(nodirective, hash_consing:rewritten/1), _)) ), + templates_declared(Templates, hash_consing:rewritten/1, Constructors), constructors_registered(Constructors, File). constructors_registered([], _). -constructors_registered([Element | Elements], File) :- - specification(Element, Name, Arity, Configuration), - configuration_registered(Name, Arity, Configuration), - id_name(Name, Arity, _), +constructors_registered([Name/Arity | Constructors], File) :- ( registered_constructor(File, Name, Arity) -> true ; assertz(registered_constructor(File, Name, Arity)) ), - constructors_registered(Elements, File). + constructors_registered(Constructors, File). % ---- the rewrite ---- @@ -674,8 +1117,13 @@ %! arguments_of_abstracted(+Callable0, +File, -Callable, -Occurrences) the % arguments of a head or a goal abstracted (its own functor is a predicate -% and is left alone), the ground occurrences interned now, and the others -% listed bottom up as `occurrence(Term, Id, Handle)`. +% and is left alone), the ground occurrences represented now, and the +% others listed bottom up as `occurrence(Class, Layer, Representation, +% Handle)`: Class `id` for an occurrence that must be interned, its +% Representation an Id pattern and Handle that pattern's handle, and +% `undetermined(IdName)` for an undetermined one, its Representation and +% its Handle the fresh variable written where it stood. An occurrence that +% must not be interned is its layer, written in place, and is not listed. arguments_of_abstracted(Callable0, File, Callable, Occurrences) :- compound(Callable0), @@ -684,8 +1132,7 @@ arguments_abstracted(Arguments0, File, Arguments, [], Reversed), compound_name_arguments(Callable, Name, Arguments), reverse(Reversed, BottomUp), - occurrences_baked(BottomUp, Occurrences), - shapes_determined(Occurrences). + occurrences_baked(BottomUp, Occurrences). arguments_of_abstracted(Callable, _, Callable, []). arguments_abstracted([], _, [], Reversed, Reversed). @@ -694,8 +1141,8 @@ arguments_abstracted(Arguments0, File, Arguments, Reversed1, Reversed). %! abstracted(+Term0, +File, -Term, +Reversed0, -Reversed) each occurrence -% of a listed constructor replaced by an Id pattern, its subterms first, -% the occurrences prepended as they are met. +% of a listed constructor replaced by its representation in the clause, +% its subterms first, the listed occurrences prepended as they are met. abstracted(Term, _, Term, Reversed, Reversed) :- var(Term), @@ -707,58 +1154,55 @@ arguments_abstracted(Arguments0, File, Arguments, Reversed0, Reversed1), compound_name_arguments(Layer, Name, Arguments), compound_name_arity(Term0, Name, Arity), - occurrence_abstracted(Name, Arity, Layer, File, Term, Reversed1, Reversed). + occurrence_abstracted(Name, Arity, Term0, Layer, File, Term, Reversed1, Reversed). abstracted(Term0, File, Term, Reversed0, Reversed) :- atom(Term0), !, - occurrence_abstracted(Term0, 0, Term0, File, Term, Reversed0, Reversed). + occurrence_abstracted(Term0, 0, Term0, Term0, File, Term, Reversed0, Reversed). abstracted(Term, _, Term, Reversed, Reversed). -occurrence_abstracted(Name, Arity, Layer, File, Term, Reversed0, Reversed) :- +%! occurrence_abstracted(+Name, +Arity, +Source, +Layer, +File, +% -Representation, +Reversed0, -Reversed) AN OCCURRENCE IS CLASSIFIED +% (above) by its source pattern Source, and written as an Id pattern, as +% its layer, or as a fresh variable. + +occurrence_abstracted(Name, Arity, Source, Layer, File, Representation, Reversed0, Reversed) :- ( registered_constructor(File, Name, Arity) - -> id_pattern(Name, Arity, Term, Handle), - Reversed = [occurrence(Layer, Term, Handle) | Reversed0] - ; Term = Layer, + -> constructor_templates(Name, Arity, Templates, Kind), + value_classified(Templates, Source, Class, Structure), + occurrence_represented(Class, Name, Arity, Kind, Structure, Layer, Representation, + Reversed0, Reversed) + ; Representation = Layer, Reversed = Reversed0 ). -%! occurrences_baked(+BottomUp, -Remaining) an occurrence -% whose term is ground is interned while the file loads, which binds its -% Id in the clause; bottom up, so a parent of baked occurrences may become -% ground in turn. +occurrence_represented(must_intern, Name, Arity, Kind, Structure, Layer, Id, + Reversed, [occurrence(id, Layer, Id, Handle) | Reversed]) :- + id_built(Name, Arity, Kind, Structure, Handle, Id). +occurrence_represented(must_not_intern, _, _, _, _, Layer, Layer, Reversed, Reversed). +occurrence_represented(undetermined, Name, Arity, _, _, Layer, Variable, + Reversed, [occurrence(undetermined(IdName), Layer, Variable, Variable) | Reversed]) :- + id_name(Name, Arity, IdName). + +%! occurrences_baked(+BottomUp, -Remaining) an occurrence whose layer is +% ground is represented while the file loads, which binds its Id in the +% clause; bottom up, so a parent of baked occurrences may become ground in +% turn. occurrences_baked([], []). -occurrences_baked([occurrence(Term, Id, Handle) | Occurrences], Remaining) :- - ( ground(Term) - -> intern(Term, Id), +occurrences_baked([Occurrence | Occurrences], Remaining) :- + Occurrence = occurrence(Class, Layer, Representation, _), + ( ground(Layer) + -> occurrence_represented_now(Class, Layer, Representation), occurrences_baked(Occurrences, Remaining) - ; Remaining = [occurrence(Term, Id, Handle) | Rest], + ; Remaining = [Occurrence | Rest], occurrences_baked(Occurrences, Rest) ). -%! shapes_determined(+BottomUp) AT COMPILE TIME (above): an -% occurrence of a shaped constructor whose pattern determines the whole -% configured shape gets the shape atom written into its Id pattern, bottom -% up so that a determined inner occurrence can determine an outer one; an -% occurrence that determines only part of it keeps an unbound shape, which -% matches every shape, and its constructors are still checked by the -% lookups of the body. - -shapes_determined(Occurrences) :- - shapes_determined(Occurrences, Occurrences). - -shapes_determined([], _). -shapes_determined([occurrence(Term, Id, _) | Rest], Occurrences) :- - ( id_parts(Id, _, Shape, _), - var(Shape), - compound_name_arguments_or_atom(Term, Name, Arguments), - length(Arguments, Arity), - constructor_configuration(Name, Arity, shaped(Records)), - term_shape(Term, Records, Occurrences, Atom) - -> Shape = Atom - ; true - ), - shapes_determined(Rest, Occurrences). +occurrence_represented_now(id, Layer, Id) :- + intern(Layer, Id). +occurrence_represented_now(undetermined(_), Layer, Variable) :- + represented(Layer, Variable). %! head_scheduled(+BottomUp, +Body0, -Body) the head row of THE REWRITE % OF A CLAUSE (above). @@ -768,11 +1212,11 @@ head_scheduled(BottomUp, Body0, (Condition -> Fast ; General)) :- reverse(BottomUp, TopDown), top_level_occurrences(BottomUp, BottomUp, TopLevel), - handles_bound(TopLevel, Condition), - occurrences_goal(TopDown, intern, Lookups), - occurrences_goal(TopDown, intern_if_bound, Settled), - occurrences_goal(BottomUp, intern_if_unbound_and_ground, Inserted), - occurrences_goal(BottomUp, intern_if_unbound, Finished), + occurrences_given(TopLevel, Condition), + occurrences_goal(TopDown, related, Lookups), + occurrences_goal(TopDown, related_if_given, Settled), + occurrences_goal(BottomUp, represented_if_ground, Inserted), + occurrences_goal(BottomUp, settled_unless_given, Finished), conjoined([Lookups, Body0], Fast), conjoined([Settled, Inserted, Body0, Finished], General). @@ -796,17 +1240,21 @@ kept_conjoined([Goal | Goals], (Goal, Conjunction)) :- kept_conjoined(Goals, Conjunction). +% An occurrence is at the top when its handle is in the layer of no other +% listed occurrence; the layer of an occurrence that must not be interned +% is written in place and does not hide what it holds. + top_level_occurrences([], _, []). top_level_occurrences([Occurrence | Occurrences], All, TopLevel) :- - Occurrence = occurrence(_, _, Handle), + Occurrence = occurrence(_, _, _, Handle), ( nested_in_another(Handle, All) -> TopLevel = Rest ; TopLevel = [Occurrence | Rest] ), top_level_occurrences(Occurrences, All, Rest). -nested_in_another(Handle, [occurrence(Term, _, _) | Occurrences]) :- - ( term_variables(Term, Variables), +nested_in_another(Handle, [occurrence(_, Layer, _, _) | Occurrences]) :- + ( term_variables(Layer, Variables), variable_member(Handle, Variables) -> true ; nested_in_another(Handle, Occurrences) @@ -818,10 +1266,25 @@ ; variable_member(Variable, Candidates) ). -handles_bound([occurrence(_, _, Handle)], nonvar(Handle)) :- - !. -handles_bound([occurrence(_, _, Handle) | Occurrences], (nonvar(Handle), Condition)) :- - handles_bound(Occurrences, Condition). +%! occurrences_given(+TopLevel, -Condition) the condition of the fast path +% of a head: every top-level occurrence is given. + +occurrences_given([Occurrence], Condition) :- + !, + occurrence_given(Occurrence, Condition). +occurrences_given([Occurrence | Occurrences], (Condition, Conditions)) :- + occurrence_given(Occurrence, Condition), + occurrences_given(Occurrences, Conditions). + +% An Id pattern is given when its handle is bound; an undetermined +% occurrence when its variable is bound and not to an Id pattern of its +% constructor whose handle is unbound. The Ids of a constructor whose +% interning can be undetermined always have a shape. + +occurrence_given(occurrence(id, _, _, Handle), nonvar(Handle)). +occurrence_given(occurrence(undetermined(IdName), _, Variable, _), + (nonvar(Variable), (Variable = Id -> nonvar(Handle) ; true))) :- + compound_name_arguments(Id, IdName, [_, Handle]). %! occurrences_goal(+Occurrences, +Step, -Goal) the conjunction of one step % over the occurrences, in the order given. @@ -834,16 +1297,39 @@ occurrence_goal(Step, Occurrence, Goal), occurrences_goal(Occurrences, Step, Goals). -occurrence_goal(intern, occurrence(Term, Id, _), - hash_consing:intern(Term, Id)). -occurrence_goal(intern_if_bound, occurrence(Term, Id, Handle), - (nonvar(Handle) -> hash_consing:intern(Term, Id) ; true)). -occurrence_goal(intern_if_unbound, occurrence(Term, Id, Handle), - (var(Handle) -> hash_consing:intern(Term, Id) ; true)). -occurrence_goal(intern_if_unbound_and_ground, occurrence(Term, Id, Handle), - ((var(Handle), ground(Term)) -> hash_consing:intern(Term, Id) ; true)). -occurrence_goal(intern_if_ground, occurrence(Term, Id, _), - (ground(Term) -> hash_consing:intern(Term, Id) ; true)). +% The steps: `related` relates an occurrence to its layer; `related_if_given` +% does so when it is given; `represented_if_ground` represents it when it is +% not given and its layer is ground; `settled_unless_given` represents it at +% the end of a head, where it must be settled; `represented_before_call` +% interns a ground one and decides an undetermined one before a goal is +% called. + +occurrence_goal(related, occurrence(id, Layer, Id, _), + hash_consing:intern(Layer, Id)). +occurrence_goal(related, occurrence(undetermined(_), Layer, Variable, _), + hash_consing:represented(Layer, Variable)). +occurrence_goal(related_if_given, occurrence(id, Layer, Id, Handle), + (nonvar(Handle) -> hash_consing:intern(Layer, Id) ; true)). +occurrence_goal(related_if_given, Occurrence, + (Given -> hash_consing:represented(Layer, Variable) ; true)) :- + Occurrence = occurrence(undetermined(_), Layer, Variable, _), + occurrence_given(Occurrence, Given). +occurrence_goal(represented_if_ground, occurrence(id, Layer, Id, Handle), + ((var(Handle), ground(Layer)) -> hash_consing:intern(Layer, Id) ; true)). +occurrence_goal(represented_if_ground, Occurrence, + ((\+ Given, ground(Layer)) -> hash_consing:represented(Layer, Variable) ; true)) :- + Occurrence = occurrence(undetermined(_), Layer, Variable, _), + occurrence_given(Occurrence, Given). +occurrence_goal(settled_unless_given, occurrence(id, Layer, Id, Handle), + (var(Handle) -> hash_consing:intern(Layer, Id) ; true)). +occurrence_goal(settled_unless_given, Occurrence, + (Given -> true ; hash_consing:represented_settled(Layer, Variable))) :- + Occurrence = occurrence(undetermined(_), Layer, Variable, _), + occurrence_given(Occurrence, Given). +occurrence_goal(represented_before_call, occurrence(id, Layer, Id, _), + (ground(Layer) -> hash_consing:intern(Layer, Id) ; true)). +occurrence_goal(represented_before_call, occurrence(undetermined(_), Layer, Variable, _), + hash_consing:represented(Layer, Variable)). %! body_rewritten(+Body0, +File, -Body) the control constructs rewritten % inside, every other goal by `goal_rewritten/3`. @@ -904,14 +1390,14 @@ goal_scheduled(BottomUp, Called, (ground(Variables) -> Fast ; General)) :- reverse(BottomUp, TopDown), terms_variables(BottomUp, Variables), - occurrences_goal(BottomUp, intern, Inserts), - occurrences_goal(BottomUp, intern_if_ground, Settled), - occurrences_goal(TopDown, intern, Finished), + occurrences_goal(BottomUp, related, Inserts), + occurrences_goal(BottomUp, represented_before_call, Settled), + occurrences_goal(TopDown, related, Finished), conjoined([Inserts, Called], Fast), conjoined([Settled, Called, Finished], General). %! terms_variables(+Occurrences, -Variables) the variables of the -% occurrences' terms other than their own Handles. +% occurrences' layers other than their own Handles. terms_variables(Occurrences, Variables) :- occurrences_terms(Occurrences, Terms), @@ -920,11 +1406,11 @@ variables_without(All, Handles, Variables). occurrences_terms([], []). -occurrences_terms([occurrence(Term, _, _) | Occurrences], [Term | Terms]) :- +occurrences_terms([occurrence(_, Layer, _, _) | Occurrences], [Layer | Terms]) :- occurrences_terms(Occurrences, Terms). occurrences_handles([], []). -occurrences_handles([occurrence(_, _, Handle) | Occurrences], [Handle | Handles]) :- +occurrences_handles([occurrence(_, _, _, Handle) | Occurrences], [Handle | Handles]) :- occurrences_handles(Occurrences, Handles). variables_without([], _, []). @@ -939,13 +1425,25 @@ % Term, a place the rewrite does not schedule; raises otherwise. listed_absent(Term, File, Place) :- - abstracted(Term, File, _, [], Occurrences), - ( Occurrences == [] - -> true - ; throw(error(domain_error(term_without_rewritten_constructor, Term), + ( listed_occurs(Term, File) + -> throw(error(domain_error(term_without_rewritten_constructor, Term), context(hash_consing:rewritten/1, Place))) + ; true ). +listed_occurs(Term, File) :- + compound(Term), + !, + compound_name_arity(Term, Name, Arity), + ( registered_constructor(File, Name, Arity) + -> true + ; arg(_, Term, Argument), + listed_occurs(Argument, File) + ). +listed_occurs(Term, File) :- + atom(Term), + registered_constructor(File, Term, 0). + % ---- the hook, last, so that this file's own clauses are read before it % is active ---- diff --git a/test/hash_consing.plt b/test/hash_consing.plt new file mode 100644 index 0000000..83bffa2 --- /dev/null +++ b/test/hash_consing.plt @@ -0,0 +1,760 @@ +% THE TEST OF THE HASH_CONSING LIBRARY, run from the root of the pack as +% swipl -p library=prolog --stack-limit=32m --table-space=32m \ +% -g run_tests -t halt test/hash_consing.plt +% Ten plunit units, 65 tests. One unit per fixture file of +% `hash_consing_fixtures/`, whose setup loads the fixture: its test +% `snapshot` requires the errors the load raised, then the clauses the +% load produced, rendered as text, to be byte for byte the file of +% `hash_consing_snapshots/` named after the fixture, and each other test is +% one query. The unit `library` checks that the library under test is this +% checkout's, the unit `declarations` how lists of templates are declared, +% the unit `interrupted_intern` that an interning interrupted by a limit +% leaves no key that fails to answer its term, and the unit `concurrency` +% that threads sharing the store declare, intern and spell shapes as one +% thread would. Failing it is a defect by definition: what a rewrite +% produces +% and how `intern/2` answers are fixed by the module comment of +% prolog/hash_consing.pl, not measured. +% +% A CLAUSE IS RENDERED WITH ITS BAKED IDS EXTERNALIZED, `baked(Term)` in +% place of the Id, because a handle is an address of this process and would +% make the rendering differ from run to run. An Id pattern whose handle is a +% variable is rendered as it is, its shape atom included. +% +% AN ERROR WHILE LOADING IS RECORDED, not thrown: the fixtures that must be +% refused raise inside term expansion, which SWI-Prolog reports as a +% message and does not propagate, so a message hook records, under the +% fixture being loaded, the formal term of each error and the warning that +% a directive failed. The rendering cuts an absolute file name in them +% down to its base name. +% +% ALL FIXTURES SHARE THIS PROCESS, and a constructor has one list of +% templates per process (module comment of prolog/hash_consing.pl): +% `steps`, `inner_dispatch`, `reconfigured` and `calculus/1` declare +% `apply/2` with `apply(*, _)`, so `spines` and `deep_calculus/1`, whose +% template for applications is nested, name them `application/2`, and +% `patterns` names its own `app/2`, `abs/1` and `ref/1`. The unit +% `declarations` names constructors no other unit uses. The store and the +% spellings of the shapes are shared too, so a count of either is only +% compared before and after. +% +% This file does not opt in; it reaches Ids through the library's +% boundary predicates. The budget of each test is ONE SECOND, the +% `timeout(1)` of its unit. + +% A WARNING OR AN ERROR PRINTED ANYWHERE FAILS THE RUN. plunit drops what +% a unit's setup or a test prints when it succeeds, so a message that the +% hook below does not record would otherwise pass unseen. Under these +% flags plunit fails a test that prints a warning or an error, and `halt` +% exits with status 1 once one was printed anywhere, a unit's setup +% included; a message the hook records is not printed and does not count. +:- set_prolog_flag(on_warning, status). +:- set_prolog_flag(on_error, status). + +:- use_module(library(plunit)). +:- use_module(library(hash_consing), + [intern/2, represented/2, is_id/1, externalized/2, internalized/3, declared/1]). +:- use_module(library(aggregate), [aggregate_all/3]). +:- use_module(library(lists), [member/2]). +:- use_module(library(readutil), [read_file_to_string/3]). +:- use_module(library(listing), [portray_clause/1]). +:- use_module(library(settings), [set_setting/2]). +:- use_module(library(time), [call_with_time_limit/2]). +:- use_module(library(thread), [concurrent_maplist/2, concurrent_maplist/3]). +:- use_module(library(apply), [maplist/3]). + +% A GOAL IS NEVER WRAPPED: `portray_clause/1` otherwise breaks a goal that +% does not fit in the listing's line width, 78 columns, and a rendering +% would then depend on the length of a constructor's name. Width 0 is the +% setting's infinite width. +:- set_setting(listing:line_width, 0). + +%! test_directory(-Directory) the directory of this file, against which +% the fixtures and the snapshots are found. + +:- dynamic test_directory/1. +:- prolog_load_context(directory, Directory), + assertz(test_directory(Directory)). + +%! test_file(+Relative, -File) Relative resolved against the directory of +% this file. + +test_file(Relative, File) :- + test_directory(Directory), + directory_file_path(Directory, Relative, File). + +% ---- loading a fixture ---- + +:- dynamic load_error/2. % load_error(Fixture, Formal) +:- dynamic loading/1. % loading(Fixture) + +:- multifile user:message_hook/3. +user:message_hook(error(Formal, _), error, _) :- + loading(Fixture), + assertz(load_error(Fixture, Formal)). +user:message_hook(goal_failed(directive, _), warning, _) :- + loading(Fixture), + assertz(load_error(Fixture, directive_failed)). + +%! fixture_loaded(+Fixture) the setup of a fixture's unit: the fixture +% file loaded, each error of the load recorded as +% `load_error(Fixture, Formal)`. Nothing is imported: the fixtures export +% predicates of the same name (`kind/2` in `inner_dispatch` and `patterns`), +% which one module could not import from both, and the tests call them +% qualified. + +fixture_loaded(Fixture) :- + fixture(Fixture, Relative, _, _), + test_file(Relative, File), + assertz(loading(Fixture)), + catch(load_files(File, [if(true), imports([])]), Error, + assertz(load_error(Fixture, thrown(Error)))), + retractall(loading(Fixture)). + +% ---- rendering a fixture ---- + +%! fixture_rendered(+Fixture, -Rendered) the errors recorded while the +% fixture loaded, one `load_error(Formal)` line each, then each predicate +% of the fixture's list with the clauses the load produced, as one string. + +fixture_rendered(Fixture, Rendered) :- + fixture(Fixture, _, Module, Predicates), + with_output_to(string(Rendered), + ( load_errors_printed(Fixture), + forall(member(Predicate, Predicates), + predicate_printed(Module, Predicate)) + )). + +load_errors_printed(Fixture) :- + forall(load_error(Fixture, Formal0), + \+ \+ ( paths_shortened(Formal0, Formal), + numbervars(Formal, 0, _), + format('load_error(~W)~n', [Formal, [quoted(true), numbervars(true)]]) + )). + +%! paths_shortened(+Term, -Shortened) every absolute file name in Term as +% its base name, so that the rendering does not depend on where the +% repository is checked out. + +paths_shortened(Term, Term) :- + var(Term), + !. +paths_shortened(Term, Shortened) :- + atom(Term), + is_absolute_file_name(Term), + !, + file_base_name(Term, Shortened). +paths_shortened(Term, Shortened) :- + compound(Term), + !, + compound_name_arguments(Term, Name, Arguments), + arguments_paths_shortened(Arguments, ShortenedArguments), + compound_name_arguments(Shortened, Name, ShortenedArguments). +paths_shortened(Term, Term). + +arguments_paths_shortened([], []). +arguments_paths_shortened([Argument | Arguments], [Shortened | Shorteneds]) :- + paths_shortened(Argument, Shortened), + arguments_paths_shortened(Arguments, Shorteneds). + +%! predicate_printed(+Module, +Name/Arity) the clauses as loaded. + +predicate_printed(Module, Name/Arity) :- + functor(Head, Name, Arity), + format('predicate(~q)~n', [Name/Arity]), + forall(clause(Module:Head, Body), + ( baked_externalized((Head :- Body), Printed), + portray_clause(Printed) + )). + +baked_externalized(Term, Printed) :- + var(Term), + !, + Printed = Term. +baked_externalized(Term, Printed) :- + compound(Term), + compound_name_arity(Term, Name, Arity), + sub_atom(Name, 0, _, _, '__hash_consed_'), + arg(Arity, Term, Handle), + nonvar(Handle), + !, + externalized(Term, External), + Printed = baked(External). +baked_externalized(Term, Printed) :- + compound(Term), + !, + compound_name_arguments(Term, Name, Arguments), + arguments_baked_externalized(Arguments, PrintedArguments), + compound_name_arguments(Printed, Name, PrintedArguments). +baked_externalized(Term, Term). + +arguments_baked_externalized([], []). +arguments_baked_externalized([Argument | Arguments], [Printed | Printeds]) :- + baked_externalized(Argument, Printed), + arguments_baked_externalized(Arguments, Printeds). + +%! snapshot_read(+Fixture, -Snapshot) the text of the fixture's file in +% `hash_consing_snapshots/`. + +snapshot_read(Fixture, Snapshot) :- + format(atom(Relative), 'hash_consing_snapshots/~w.txt', [Fixture]), + test_file(Relative, File), + read_file_to_string(File, Snapshot, []). + +% ---- the queries' helpers ---- + +%! store_count(-Count) how many terms the store holds. +store_count(Count) :- + nb_getval(hash_consing_store, Trie), + trie_property(Trie, value_count(Count)). + +%! spelling_count(-Count) how many shape atoms the library has spelled. +spelling_count(Count) :- + nb_getval(hash_consing_spellings, Trie), + trie_property(Trie, value_count(Count)). + +%! shape_indexed(+Head) the just in time indexer built an index on the +% first argument of the first argument, which is the shape. +shape_indexed(Head) :- + predicate_property(Head, indexed(Indexes)), + member(Index, Indexes), + get_dict(arguments, Index, [1]), + get_dict(position, Index, [1]), + get_dict(realised, Index, true), + !. + +called_repeatedly(Goal) :- + forall(between(1, 20, _), ( call(Goal) -> true ; true )). + +%! answers_its_term(+Term) Term interns to an Id that externalizes back to +% Term. +answers_its_term(Term) :- + intern(Term, Id), + externalized(Id, Back), + Back == Term. + +%! interned_forever(+Round, +Index) interns `time_probe(Round, Index, +% leaf)` and the probes after it until a limit stops it, recording in +% the global variable `interrupted_intern_count` the last Index interned. +interned_forever(Round, Index) :- + intern(time_probe(Round, Index, leaf), _), + nb_setval(interrupted_intern_count, Index), + Next is Index + 1, + interned_forever(Round, Next). + +%! numbered_template(+Prefix, +Number, -Template) the template +% `Prefix_Number(_)`. +numbered_template(Prefix, Number, Template) :- + format(atom(Name), '~w_~d', [Prefix, Number]), + functor(Template, Name, 1). + +%! templates_declared_one_by_one(+Templates, +Worker) each template +% declared alone, in the order of the list. +templates_declared_one_by_one(Templates, _) :- + forall(member(Template, Templates), declared([Template])). + +%! thread_stores(-Stores) the store and the spellings of this thread, the +% two global variables of prolog/hash_consing.pl. +thread_stores(stores(Store, Spellings)) :- + nb_getval(hash_consing_store, Store), + nb_getval(hash_consing_spellings, Spellings). + +%! thread_stores_installed(+Stores) Stores installed in this thread, which +% then interns into the same tries. +thread_stores_installed(stores(Store, Spellings)) :- + nb_setval(hash_consing_store, Store), + nb_setval(hash_consing_spellings, Spellings). + +%! terms_interned_with_stores(+Stores, +Numbers, +Worker, -Ids) the Id of +% `concurrently_interned(Number)` for each of Numbers, interned by this +% thread into Stores. +terms_interned_with_stores(Stores, Numbers, _, Ids) :- + thread_stores_installed(Stores), + maplist(number_interned, Numbers, Ids). + +number_interned(Number, Id) :- + intern(concurrently_interned(Number), Id). + +%! shapes_interned_with_stores(+Stores, +Numbers, +Worker, -Ids) the Id of +% `concurrently_shaped(shape_Number, Worker)` for each of Numbers: a term +% of this thread's own, whose shape every thread spells alike. +shapes_interned_with_stores(Stores, Numbers, Worker, Ids) :- + thread_stores_installed(Stores), + maplist(shape_interned(Worker), Numbers, Ids). + +shape_interned(Worker, Number, Id) :- + atom_concat(shape_, Number, Root), + intern(concurrently_shaped(Root, Worker), Id). + +% ---- the fixtures ---- + +%! fixture(?Fixture, ?File, ?Module, ?Predicates) a fixture file, relative +% to this file's directory, the module it defines, and the predicates its +% rendering shows. + +fixture(steps, 'hash_consing_fixtures/steps.pl', steps, + [step/2, callee/2, built/2, constant/1]). +fixture(spines, 'hash_consing_fixtures/spines.pl', spines, + [head/2, inner/2]). +fixture(plain, 'hash_consing_fixtures/plain.pl', plain, + [doubled/2, swapped/2]). +fixture(inner_dispatch, 'hash_consing_fixtures/inner_dispatch.pl', inner_dispatch, []). +fixture(reconfigured, 'hash_consing_fixtures/reconfigured.pl', reconfigured, []). +fixture(patterns, 'hash_consing_fixtures/patterns.pl', patterns, + [kind/2, size/2, wrapped/2, first/2, built/2, unbound_built/1]). + +calculus([apply(*, _), lambda(_), variable(_), closure_a(_), closure_b]). +deep_calculus([application(application(*, _), _), lambda(_), variable(_), closure(_)]). +patterns_templates([app(abs(_), _), app(app(*, _), _), app(_, ref(_)), abs(_), ref(_)]). + +% ---- the units ---- + +:- begin_tests(library, [timeout(1)]). + +% The module under test is this checkout's, not a pack of the same name +% installed elsewhere. +test(loaded_from_this_checkout, [true(File == Expected)]) :- + module_property(hash_consing, file(File)), + test_directory(Directory), + file_directory_name(Directory, PackDirectory), + directory_file_path(PackDirectory, 'prolog/hash_consing.pl', Expected). + +:- end_tests(library). + +:- begin_tests(steps, [setup(fixture_loaded(steps)), timeout(1)]). + +test(snapshot, [true(Rendered == Snapshot)]) :- + fixture_rendered(steps, Rendered), + snapshot_read(steps, Snapshot). + +test(shape_of_an_id, [nondet]) :- + calculus(Templates), + internalized(Templates, apply(lambda(variable(0)), variable(1)), Application), + Application = '__hash_consed_apply/2'(Shape, _), Shape == 'lambda/1'. + +test(shape_of_a_zero_arity_callee, [nondet]) :- + calculus(Templates), + internalized(Templates, apply(closure_b, variable(1)), Application), + Application = '__hash_consed_apply/2'(Shape, _), Shape == 'closure_b/0'. + +test(dispatch_lambda, [nondet]) :- + calculus(Templates), + internalized(Templates, apply(lambda(variable(0)), variable(1)), Application), + steps:step(Application, Result), externalized(Result, External), + External == beta(variable(0), variable(1)). + +test(dispatch_closure, [nondet]) :- + calculus(Templates), + internalized(Templates, apply(closure_a(variable(7)), closure_b), Application), + steps:step(Application, Result), externalized(Result, External), + External == compiled(variable(7), closure_b). + +test(dispatch_zero_arity, [nondet]) :- + calculus(Templates), + internalized(Templates, apply(closure_b, variable(3)), Application), + steps:step(Application, Result), externalized(Result, External), + External == constant(variable(3)). + +test(dispatch_spine, [nondet]) :- + calculus(Templates), + internalized(Templates, apply(apply(closure_b, variable(1)), variable(2)), Application), + steps:step(Application, Result), externalized(Result, External), + External == spine(closure_b, variable(1), variable(2)). + +test(one_answer_per_term, [nondet]) :- + calculus(Templates), + internalized(Templates, apply(lambda(variable(0)), variable(1)), Application), + aggregate_all(count, steps:step(Application, _), Count), Count == 1. + +test(partial_pattern_matches_every_shape, [nondet]) :- + calculus(Templates), + internalized(Templates, apply(closure_a(variable(7)), closure_b), Application), + steps:callee(Application, Function), externalized(Function, External), + External == closure_a(variable(7)). + +test(body_goal_builds_the_shape, [nondet]) :- + calculus(Templates), internalized(Templates, lambda(variable(0)), Function), + steps:built(Function, Built), + Built = '__hash_consed_apply/2'(Shape, _), Shape == 'lambda/1', + internalized(Templates, apply(lambda(variable(0)), variable(0)), Application), + Built == Application. + +test(ground_occurrence_baked, [nondet]) :- + steps:constant(Constant), externalized(Constant, External), + External == apply(lambda(variable(0)), closure_b), + calculus(Templates), internalized(Templates, External, Application), + Constant == Application. + +test(same_content_same_id, [nondet]) :- + intern(variable(5), Variable), intern(lambda(Variable), Function), + intern(apply(Function, Variable), First), intern(apply(Function, Variable), Second), + First == Second. + +test(backward, [nondet]) :- + intern(variable(6), Variable), intern(lambda(Variable), Function), + intern(apply(Function, Variable), Id), + intern(Term, Id), Term == apply(Function, Variable). + +test(wrong_shape_does_not_unify, [nondet]) :- + calculus(Templates), + internalized(Templates, apply(lambda(variable(0)), variable(1)), Application), + \+ Application = '__hash_consed_apply/2'('closure_a/1', _). + +test(spelling_remembered_once, [nondet]) :- + intern(variable(8), FirstVariable), intern(closure_a(FirstVariable), FirstFunction), + spelling_count(Before), + intern(apply(FirstFunction, FirstVariable), _), spelling_count(Middle), + intern(variable(9), SecondVariable), intern(closure_a(SecondVariable), SecondFunction), + intern(apply(SecondFunction, SecondVariable), _), + spelling_count(After), + Middle >= Before, After =:= Middle. + +test(argument_that_is_no_id, [nondet]) :- + intern(apply(3, 4), Id), Id = '__hash_consed_apply/2'(Shape, _), Shape == '-'. + +test(unground_term_raises, [error(instantiation_error)]) :- + intern(apply(_, _), _). + +test(externalized_internalized_inverse, [nondet]) :- + calculus(Templates), + External = f(apply(lambda(variable(0)), apply(closure_b, closure_b)), [variable(1)]), + internalized(Templates, External, Internal), externalized(Internal, Back), + Back == External. + +:- end_tests(steps). + +:- begin_tests(spines, [setup(fixture_loaded(spines)), timeout(1)]). + +test(snapshot, [true(Rendered == Snapshot)]) :- + fixture_rendered(spines, Rendered), + snapshot_read(spines, Snapshot). + +test(two_layers_in_the_shape, [nondet]) :- + deep_calculus(Templates), + internalized(Templates, + application(application(lambda(variable(0)), variable(1)), variable(2)), + Application), + Application = '__hash_consed_application/2'(Shape, _), + Shape == 'application/2(lambda/1)'. + +test(template_ends_the_shape, [nondet]) :- + deep_calculus(Templates), + internalized(Templates, + application(application(application(lambda(variable(0)), variable(1)), + variable(2)), + variable(3)), + Application), + Application = '__hash_consed_application/2'(Shape, _), + Shape == 'application/2(application/2)'. + +test(dispatch_two_layers, [nondet]) :- + deep_calculus(Templates), + internalized(Templates, + application(application(closure(variable(0)), variable(1)), variable(2)), + Application), + findall(Kind, spines:head(Application, Kind), Kinds), + Kinds == [compiled_redex_under_an_application]. + +test(dispatch_one_layer, [nondet]) :- + deep_calculus(Templates), + internalized(Templates, application(lambda(variable(0)), variable(1)), Application), + findall(Kind, spines:head(Application, Kind), Kinds), Kinds == [redex]. + +test(partial_pattern_still_right, [nondet]) :- + deep_calculus(Templates), + internalized(Templates, + application(application(closure(variable(0)), variable(1)), variable(2)), + Application), + spines:inner(Application, Function), externalized(Function, External), + External == closure(variable(0)). + +test(partial_pattern_rejects_a_redex, [nondet]) :- + deep_calculus(Templates), + internalized(Templates, application(lambda(variable(0)), variable(1)), Application), + \+ spines:inner(Application, _). + +:- end_tests(spines). + +:- begin_tests(plain, [setup(fixture_loaded(plain)), timeout(1)]). + +test(snapshot, [true(Rendered == Snapshot)]) :- + fixture_rendered(plain, Rendered), + snapshot_read(plain, Snapshot). + +test(upsert_then_externalize, [nondet]) :- + plain:doubled(a, Doubled), externalized(Doubled, External), External == pair(a, a). + +test(same_content_same_id, [nondet]) :- + plain:doubled(a, Doubled), plain:swapped(Doubled, Swapped), Doubled == Swapped. + +test(value_that_is_no_id_fails, [fail]) :- + plain:doubled(_, foo). + +test(uninterned_instance_fails, [fail]) :- + plain:doubled(_, pair(a, a)). + +test(both_sides_unknown_raises, [error(instantiation_error)]) :- + plain:swapped(_, _). + +:- end_tests(plain). + +:- begin_tests(inner_dispatch, [setup(fixture_loaded(inner_dispatch)), timeout(1)]). + +test(snapshot, [true(Rendered == Snapshot)]) :- + fixture_rendered(inner_dispatch, Rendered), + snapshot_read(inner_dispatch, Snapshot). + +test(dispatch_by_inner_constructor, [nondet]) :- + internalized([apply(*, _), closure_39(_)], apply(closure_39(x), y), Application), + findall(Kind, inner_dispatch:kind(Application, Kind), Kinds), Kinds == [closure_39]. + +test(shape_indexed, [nondet]) :- + internalized([apply(*, _), closure_39(_)], apply(closure_39(x), y), Application), + called_repeatedly(inner_dispatch:kind(Application, _)), + shape_indexed(inner_dispatch:kind(_, _)). + +:- end_tests(inner_dispatch). + +:- begin_tests(reconfigured, [setup(fixture_loaded(reconfigured)), timeout(1)]). + +test(snapshot, [true(Rendered == Snapshot)]) :- + fixture_rendered(reconfigured, Rendered), + snapshot_read(reconfigured, Snapshot). + +:- end_tests(reconfigured). + +:- begin_tests(patterns, [setup(fixture_loaded(patterns)), timeout(1)]). + +test(snapshot, [true(Rendered == Snapshot)]) :- + fixture_rendered(patterns, Rendered), + snapshot_read(patterns, Snapshot). + +% `app(abs(ref(0)), ref(1))` matches the first template and the third; the +% first gives the shape. +test(first_template_gives_the_shape, [nondet]) :- + patterns_templates(Templates), + internalized(Templates, app(abs(ref(0)), ref(1)), Application), + Application = '__hash_consed_app/2'(Shape, _), Shape == 'abs/1'. + +test(second_template_records_two_layers, [nondet]) :- + patterns_templates(Templates), + internalized(Templates, app(app(abs(ref(0)), ref(1)), ref(2)), Application), + Application = '__hash_consed_app/2'(Shape, _), Shape == 'app/2(abs/1)'. + +test(third_template_records_the_second_argument, [nondet]) :- + patterns_templates(Templates), + internalized(Templates, app(ref(0), ref(1)), Application), + Application = '__hash_consed_app/2'(Shape, _), Shape == 'ref/1'. + +test(no_template_stays_plain, [nondet]) :- + patterns_templates(Templates), + internalized(Templates, ref(0), Function), + internalized(Templates, abs(ref(1)), Argument), + store_count(Before), + internalized(Templates, app(ref(0), abs(ref(1))), Application), + store_count(After), + Application == app(Function, Argument), + After =:= Before. + +test(intern_fails_on_a_term_no_template_matches, [fail]) :- + patterns_templates(Templates), + internalized(Templates, ref(0), Function), + internalized(Templates, abs(ref(1)), Argument), + intern(app(Function, Argument), _). + +test(intern_raises_without_templates, + [error(existence_error(templates, undeclared_constructor/1))]) :- + intern(undeclared_constructor(1), _). + +test(is_id_tells_ids, [nondet]) :- + patterns_templates(Templates), + internalized(Templates, app(abs(ref(0)), ref(1)), Interned), + internalized(Templates, app(ref(0), abs(ref(1))), Plain), + is_id(Interned), + \+ is_id(Plain), + \+ is_id('__hash_consed_app/2'(_, _)). + +test(kinds, [nondet, true(Kinds == [redex, redex_under_an_application, stuck, plain])]) :- + patterns_templates(Templates), + findall(Kind, + ( member(External, [app(abs(ref(0)), ref(1)), + app(app(abs(ref(0)), ref(1)), ref(2)), + app(ref(0), ref(1)), + app(ref(0), abs(ref(1)))]), + internalized(Templates, External, Application), + patterns:kind(Application, Kind) ), + Kinds). + +test(undetermined_head_given_an_id, [nondet, true(Size == 4)]) :- + patterns_templates(Templates), + internalized(Templates, app(abs(ref(0)), ref(1)), Application), + patterns:size(Application, Size). + +test(undetermined_head_given_a_plain_term, [nondet, true(Size == 4)]) :- + patterns_templates(Templates), + internalized(Templates, app(ref(0), abs(ref(1))), Application), + patterns:size(Application, Size). + +test(undetermined_output_interned, [nondet]) :- + patterns_templates(Templates), + internalized(Templates, abs(ref(0)), Function), + patterns:wrapped(Function, Wrapped), + is_id(Wrapped), + externalized(Wrapped, External), External == app(abs(ref(0)), abs(ref(0))). + +test(undetermined_output_plain, [nondet]) :- + patterns_templates(Templates), + internalized(Templates, ref(0), Function), + patterns:wrapped(Function, Wrapped), + \+ is_id(Wrapped), + externalized(Wrapped, External), External == app(ref(0), abs(ref(0))). + +% The program without interning answers `app(ref(1), abs(ref(0)))`; a clause +% split into an Id version and a plain version would cut away the plain one. +test(cut_after_undetermined_occurrence, [nondet]) :- + patterns_templates(Templates), + internalized(Templates, ref(1), Function), + internalized(Templates, abs(ref(0)), Argument), + patterns:first([Function-Argument], First), + externalized(First, External), External == app(ref(1), abs(ref(0))). + +test(body_goal_decided_at_the_call, [nondet]) :- + patterns_templates(Templates), + internalized(Templates, abs(ref(1)), Lambda), + internalized(Templates, ref(1), Reference), + patterns:built(Lambda, Interned), + patterns:built(Reference, Plain), + is_id(Interned), + Plain = app(Reference, _). + +test(body_goal_undecided_raises, [error(instantiation_error)]) :- + patterns:unbound_built(_). + +test(represented_rejects_a_plain_term_that_must_be_interned, [fail]) :- + patterns_templates(Templates), + internalized(Templates, abs(ref(0)), Function), + internalized(Templates, ref(1), Argument), + represented(app(Function, Argument), app(Function, Argument)). + +test(represented_decides_a_partial_layer, [nondet]) :- + patterns_templates(Templates), + internalized(Templates, abs(ref(0)), Function), + represented(app(Function, _), Interned), + Interned = '__hash_consed_app/2'(Shape, Handle), Shape == 'abs/1', var(Handle), + internalized(Templates, ref(0), Reference), + Layer = app(Reference, '__hash_consed_abs/1'(_)), + represented(Layer, Plain), + Plain == Layer. + +test(represented_raises_when_undecided, [error(instantiation_error)]) :- + represented(app(_, _), _). + +:- end_tests(patterns). + +:- begin_tests(declarations, [timeout(1)]). + +test(declared_twice_the_same) :- + declared([declared_pair(abs(_), _), declared_pair(_, _)]), + declared([declared_pair(abs(_), _), declared_pair(_, _)]). + +test(declared_again_otherwise_raises, + [error(permission_error(reconfigure, interned_constructor, declared_single/1))]) :- + declared([declared_single(abs(_))]), + declared([declared_single(ref(_))]). + +test(unreachable_template_raises, [error(domain_error(reachable_template, _))]) :- + declared([unreachable(_, _), unreachable(abs(_), _)]). + +test(a_raising_declaration_registers_nothing, + [error(existence_error(templates, unreachable_after_star/2))]) :- + catch(declared([unreachable_after_star(*, _), unreachable_after_star(abs(_), _)]), + error(domain_error(reachable_template, _), _), + true), + intern(unreachable_after_star(a, b), _). + +% `;` is a constructor like any other: the template requires a `;/2` term. +test(semicolon_is_a_constructor, [nondet]) :- + Templates = [pick((abs(_) ; ref(_))), abs(_), ref(_)], + internalized(Templates, pick(abs(ref(0))), Picked), + \+ is_id(Picked), + internalized(Templates, pick((abs(ref(0)) ; ref(1))), Chosen), + is_id(Chosen). + +:- end_tests(declarations). + +% AN INTERRUPTED INSERTION: `intern/2` interrupted between its insertion +% and the write-back of the node's handle, by `call_with_inference_limit/3` +% or by `call_with_time_limit/2`, leaves a store whose every key still +% answers its own term (settled_handle/4 of prolog/hash_consing.pl). The +% probes' constructors are declared in the unit's setup, every argument +% `_`. + +:- begin_tests(interrupted_intern, + [setup(declared([inference_probe(_, _), time_probe(_, _, _)])), timeout(1)]). + +% Every inference limit from 1 to 300 on the interning of a fresh term: +% one of them falls between the insertion and the write-back. +test(an_inference_limit_between_insertion_and_write_back) :- + forall(between(1, 300, Limit), + call_with_inference_limit(intern(inference_probe(Limit, leaf), _), Limit, _)), + forall(between(1, 300, Limit), + assertion(answers_its_term(inference_probe(Limit, leaf)))). + +% Time limits of a millisecond on a loop interning fresh terms: each +% expires somewhere in an interning; the terms interned so far, and the +% one being interned, still answer themselves. +test(a_time_limit_during_interning) :- + forall(between(1, 50, Round), + ( nb_setval(interrupted_intern_count, 0), + catch(call_with_time_limit(0.001, interned_forever(Round, 1)), + time_limit_exceeded, + true), + nb_getval(interrupted_intern_count, Count), + Last is Count + 1, + forall(between(1, Last, Index), + assertion(answers_its_term(time_probe(Round, Index, leaf)))) )). + +:- end_tests(interrupted_intern). + +% THREADS SHARE ONE STORE: a thread that installs the store and the +% spellings of the loading thread declares, interns and spells shapes +% while other threads do the same. Eight workers do each thing at once; +% what they leave is then read in one thread. + +:- begin_tests(concurrency, [timeout(1)]). + +% Every constructor that the workers declared at once is registered once: +% is_id/1 and intern/2 answer once on an Id of it. +test(a_constructor_declared_by_many_threads_is_registered_once) :- + numlist(1, 2000, Numbers), + maplist(numbered_template(concurrently_declared), Numbers, Templates), + numlist(1, 8, Workers), + concurrent_maplist(templates_declared_one_by_one(Templates), Workers), + forall(member(Template, Templates), + ( functor(Template, Name, 1), + functor(Term, Name, 1), + arg(1, Term, leaf), + intern(Term, Id), + aggregate_all(count, is_id(Id), 1), + aggregate_all(count, intern(_, Id), 1) )). + +% A term that the workers intern at once has one Id, and no worker raises. +test(a_term_interned_by_many_threads_has_one_id) :- + declared([concurrently_interned(_)]), + numlist(1, 20000, Numbers), + thread_stores(Stores), + numlist(1, 8, Workers), + concurrent_maplist(terms_interned_with_stores(Stores, Numbers), Workers, IdLists), + IdLists = [Ids | OtherIdLists], + forall(member(OtherIds, OtherIdLists), OtherIds == Ids). + +% A shape that the workers spell at once, each for a term of its own, is +% spelled without failing any of them. +test(a_shape_spelled_by_many_threads_fails_no_interning) :- + declared([concurrently_shaped(*, _)]), + numlist(1, 2000, Numbers), + thread_stores(Stores), + numlist(1, 8, Workers), + concurrent_maplist(shapes_interned_with_stores(Stores, Numbers), Workers, _). + +:- end_tests(concurrency). diff --git a/test/hash_consing_fixtures/inner_dispatch.pl b/test/hash_consing_fixtures/inner_dispatch.pl index 17e2327..4a8c8fb 100644 --- a/test/hash_consing_fixtures/inner_dispatch.pl +++ b/test/hash_consing_fixtures/inner_dispatch.pl @@ -1,8 +1,8 @@ -% Fixture of test/hash_consing_rewrite.pl: forty clauses told apart by +% Fixture of test/hash_consing.plt: forty clauses told apart by % the INNER constructor of an application, enough for SWI-Prolog to build a % deep index on the shape, the first argument of the Id. :- module(inner_dispatch, [kind/2]). -:- use_module('../../prolog/hash_consing', []). +:- use_module(library(hash_consing), []). :- hash_consing:rewritten([apply(*, _), closure_00(_), closure_01(_), closure_02(_), closure_03(_), closure_04(_), closure_05(_), closure_06(_), closure_07(_), closure_08(_), closure_09(_), closure_10(_), closure_11(_), closure_12(_), closure_13(_), closure_14(_), closure_15(_), closure_16(_), closure_17(_), closure_18(_), closure_19(_), closure_20(_), closure_21(_), closure_22(_), closure_23(_), closure_24(_), closure_25(_), closure_26(_), closure_27(_), closure_28(_), closure_29(_), closure_30(_), closure_31(_), closure_32(_), closure_33(_), closure_34(_), closure_35(_), closure_36(_), closure_37(_), closure_38(_), closure_39(_)]). kind(apply(closure_00(_), _), closure_00). diff --git a/test/hash_consing_fixtures/patterns.pl b/test/hash_consing_fixtures/patterns.pl new file mode 100644 index 0000000..d850625 --- /dev/null +++ b/test/hash_consing_fixtures/patterns.pl @@ -0,0 +1,46 @@ +% Fixture of test/hash_consing.plt: templates as patterns. The constructor +% `app/2` has three templates, tried in order, and an application that none +% of them matches stays a plain compound; the occurrences below fall in the +% three classes of the rewrite. +:- module(patterns, [kind/2, size/2, wrapped/2, first/2, built/2, unbound_built/1]). +:- use_module(library(hash_consing), []). +:- hash_consing:rewritten([app(abs(_), _), app(app(*, _), _), app(_, ref(_)), abs(_), ref(_)]). + +% Must intern, every instance taking the first template: the shape `abs/1` +% is written into the head. +kind(app(abs(_), _), redex). +% Must intern, every instance taking the second template: `app/2(abs/1)`. +kind(app(app(abs(_), _), _), redex_under_an_application). +% Must intern, every instance taking the third template: `ref/1`. +kind(app(ref(_), ref(_)), stuck). +% Must not intern: no template matches any instance, so the head keeps the +% plain application. +kind(app(ref(_), abs(_)), plain). + +% Undetermined at the top of a head: a fresh variable there, related to the +% layer by represented/2. +size(app(Function, Argument), Size) :- + size(Function, FunctionSize), + size(Argument, ArgumentSize), + Size is FunctionSize + ArgumentSize + 1. +size(abs(Body), Size) :- + size(Body, BodySize), + Size is BodySize + 1. +size(ref(_), 1). + +% Undetermined in an output position of a head. +wrapped(Function, app(Function, abs(ref(0)))). + +% Undetermined, with a cut after the body has bound it: the answer is the +% one of the program without interning, whichever representation it gets. +first(Pairs, app(Function, Argument)) :- + member(Function-Argument, Pairs), + !. + +% Undetermined in a body goal, decided when the goal is called. +built(Function, Built) :- + Built = app(Function, abs(ref(0))). + +% Undetermined in a body goal and still undecided when it is called. +unbound_built(Built) :- + Built = app(_, abs(ref(0))). diff --git a/test/hash_consing_fixtures/plain.pl b/test/hash_consing_fixtures/plain.pl index d63249d..e8556bc 100644 --- a/test/hash_consing_fixtures/plain.pl +++ b/test/hash_consing_fixtures/plain.pl @@ -1,7 +1,7 @@ -% Fixture of test/hash_consing_rewrite.pl: no constructor has a shape, +% Fixture of test/hash_consing.plt: no constructor has a shape, % so every Id records its root constructor only. :- module(plain, [doubled/2, swapped/2]). -:- use_module('../../prolog/hash_consing', []). +:- use_module(library(hash_consing), []). :- hash_consing:rewritten([pair(_, _)]). doubled(X, pair(X, X)). diff --git a/test/hash_consing_fixtures/reconfigured.pl b/test/hash_consing_fixtures/reconfigured.pl index e1eaa35..939eb0c 100644 --- a/test/hash_consing_fixtures/reconfigured.pl +++ b/test/hash_consing_fixtures/reconfigured.pl @@ -1,7 +1,7 @@ -% Fixture of test/hash_consing_rewrite.pl: a constructor declared +% Fixture of test/hash_consing.plt: a constructor declared % twice with different templates, which raises while the file loads. :- module(reconfigured, [first/1]). -:- use_module('../../prolog/hash_consing', []). +:- use_module(library(hash_consing), []). :- hash_consing:rewritten([apply(*, _)]). :- hash_consing:rewritten([apply(*, *)]). diff --git a/test/hash_consing_fixtures/spines.pl b/test/hash_consing_fixtures/spines.pl index 8b24acc..a8ba85e 100644 --- a/test/hash_consing_fixtures/spines.pl +++ b/test/hash_consing_fixtures/spines.pl @@ -1,14 +1,14 @@ -% Fixture of test/hash_consing_rewrite.pl: a nested template, so that +% Fixture of test/hash_consing.plt: a nested template, so that % the shape of an application spells two layers of its first argument when % that argument is an application too. :- module(spines, [head/2, inner/2]). -:- use_module('../../prolog/hash_consing', []). -:- hash_consing:rewritten([apply(apply(*, _), _), lambda(_), variable(_), closure_a(_)]). +:- use_module(library(hash_consing), []). +:- hash_consing:rewritten([application(application(*, _), _), lambda(_), variable(_), closure(_)]). % Determined: two layers of the first argument are in the pattern. -head(apply(apply(lambda(_), _), _), redex_under_an_application). -head(apply(apply(closure_a(_), _), _), compiled_redex_under_an_application). +head(application(application(lambda(_), _), _), redex_under_an_application). +head(application(application(closure(_), _), _), compiled_redex_under_an_application). % Determined: the template goes on only below an application. -head(apply(lambda(_), _), redex). +head(application(lambda(_), _), redex). % Not determined: the inner application's own callee is unknown. -inner(apply(apply(Function, _), _), Function). +inner(application(application(Function, _), _), Function). diff --git a/test/hash_consing_fixtures/steps.pl b/test/hash_consing_fixtures/steps.pl index 4e2641f..948bab8 100644 --- a/test/hash_consing_fixtures/steps.pl +++ b/test/hash_consing_fixtures/steps.pl @@ -1,8 +1,8 @@ -% Fixture of test/hash_consing_rewrite.pl: clauses told apart by an +% Fixture of test/hash_consing.plt: clauses told apart by an % inner constructor; the template apply(*, _) records the root constructor % of an application's first argument. :- module(steps, [step/2, callee/2, built/2, constant/1]). -:- use_module('../../prolog/hash_consing', []). +:- use_module(library(hash_consing), []). :- hash_consing:rewritten([apply(*, _), lambda(_), variable(_), closure_a(_), closure_b]). % The shape is determined: the atom goes into the head. diff --git a/test/hash_consing_rewrite.pl b/test/hash_consing_rewrite.pl deleted file mode 100644 index 829e707..0000000 --- a/test/hash_consing_rewrite.pl +++ /dev/null @@ -1,298 +0,0 @@ -#!/usr/bin/env swipl -% THE TEST OF THE HASH_CONSING LIBRARY: ONE PROCESS PER FIXTURE, launched -% by hash_consing_rewrite.sh as -% swipl -q --stack-limit=32m --table-space=32m \ -% hash_consing_rewrite.pl -- --fixture=Name -% It loads the fixture file of `hash_consing_fixtures/`, prints the -% clauses the load produced and the outcome of the fixture's -% queries, and hash_consing_rewrite.sh's output is compared with -% hash_consing_rewrite_baseline.txt. Failing it is a defect by definition: -% what a rewrite produces and how `intern/2` answers are fixed by the -% module comment of prolog/hash_consing.pl, not measured. -% -% A CLAUSE IS PRINTED WITH ITS BAKED IDS EXTERNALIZED, `baked(Term)` in -% place of the Id, because a handle is an address of this process and would -% make the baseline differ from run to run. An Id pattern whose handle is a -% variable is printed as it is, its shape atom included. -% -% AN ERROR WHILE LOADING IS PRINTED, not thrown: the fixtures that must be -% refused raise inside term expansion, which SWI-Prolog reports as a -% message and does not propagate, so a message hook records the formal -% term of each error, an absolute file name in it cut down to its base -% name, and the warning that a directive failed. -% -% This file does not opt in; it reaches Ids through the library's -% boundary predicates. The in-process budget is ONE SECOND. - -:- use_module('../prolog/hash_consing', [intern/2, externalized/2, internalized/3]). -:- use_module(library(main), [argv_options/3]). -:- use_module(library(time), [call_with_time_limit/2]). -:- use_module(library(aggregate), [aggregate_all/3]). -:- initialization(main, main). - -:- dynamic load_error/1. - -:- multifile user:message_hook/3. -user:message_hook(error(Formal, _), error, _) :- - loading_fixture, - assertz(load_error(Formal)). -user:message_hook(goal_failed(directive, _), warning, _) :- - loading_fixture, - assertz(load_error(directive_failed)). - -:- dynamic loading/0. - -loading_fixture :- - loading. - -gate_time_limit(1). - -main :- - current_prolog_flag(argv, Arguments), - argv_options(Arguments, _, Options), - ( memberchk(fixture(Name), Options) - -> true - ; throw(error(existence_error(option, fixture), _)) - ), - fixture(Name, File, Module, Predicates, Queries), - format('fixture(~q)~n', [Name]), - fixture_loaded(File), - forall(member(Predicate, Predicates), - predicate_printed(Module, Predicate)), - forall(member(query(QueryName, Goal), Queries), - query_printed(QueryName, Goal)). - -fixture_loaded(File) :- - assertz(loading), - catch(load_files(File, [if(true)]), Error, assertz(load_error(thrown(Error)))), - retractall(loading), - forall(load_error(Formal0), - \+ \+ ( paths_shortened(Formal0, Formal), - numbervars(Formal, 0, _), - format('load_error(~W)~n', [Formal, [quoted(true), numbervars(true)]]) - )). - -%! paths_shortened(+Term, -Shortened) every absolute file name in Term as -% its base name, so that the output does not depend on where the -% repository is checked out. - -paths_shortened(Term, Term) :- - var(Term), - !. -paths_shortened(Term, Shortened) :- - atom(Term), - is_absolute_file_name(Term), - !, - file_base_name(Term, Shortened). -paths_shortened(Term, Shortened) :- - compound(Term), - !, - compound_name_arguments(Term, Name, Arguments), - arguments_paths_shortened(Arguments, ShortenedArguments), - compound_name_arguments(Shortened, Name, ShortenedArguments). -paths_shortened(Term, Term). - -arguments_paths_shortened([], []). -arguments_paths_shortened([Argument | Arguments], [Shortened | Shorteneds]) :- - paths_shortened(Argument, Shortened), - arguments_paths_shortened(Arguments, Shorteneds). - -%! predicate_printed(+Module, +Name/Arity) the clauses as loaded. - -predicate_printed(Module, Name/Arity) :- - functor(Head, Name, Arity), - format('predicate(~q)~n', [Name/Arity]), - forall(clause(Module:Head, Body), - ( baked_externalized((Head :- Body), Printed), - portray_clause(Printed) - )). - -baked_externalized(Term, Printed) :- - var(Term), - !, - Printed = Term. -baked_externalized(Term, Printed) :- - compound(Term), - compound_name_arity(Term, Name, Arity), - sub_atom(Name, 0, _, _, '__hash_consed_'), - arg(Arity, Term, Handle), - nonvar(Handle), - !, - externalized(Term, External), - Printed = baked(External). -baked_externalized(Term, Printed) :- - compound(Term), - !, - compound_name_arguments(Term, Name, Arguments), - arguments_baked_externalized(Arguments, PrintedArguments), - compound_name_arguments(Printed, Name, PrintedArguments). -baked_externalized(Term, Term). - -arguments_baked_externalized([], []). -arguments_baked_externalized([Argument | Arguments], [Printed | Printeds]) :- - baked_externalized(Argument, Printed), - arguments_baked_externalized(Arguments, Printeds). - -%! query_printed(+Name, +Goal) `query(Name, true)`, `query(Name, false)`, -% or `query(Name, error(Formal))`. - -query_printed(Name, Goal) :- - gate_time_limit(Limit), - catch(( call_with_time_limit(Limit, Goal) - -> Outcome = true - ; Outcome = false - ), - Error, - error_outcome(Error, Outcome)), - format('query(~q, ~q)~n', [Name, Outcome]). - -error_outcome(error(Formal, _), error(Formal)) :- !. -error_outcome(Error, thrown(Error)). - -% ---- the queries' helpers ---- - -store_count(Count) :- - nb_getval(hash_consing_store, Trie), - trie_property(Trie, value_count(Count)). - -%! spelling_count(-Count) how many shape atoms the library has spelled. -spelling_count(Count) :- - nb_getval(hash_consing_spellings, Trie), - trie_property(Trie, value_count(Count)). - -%! check_inserts_nothing(+Term, +Id) `intern(Term, Id)` with both bound -% leaves the store's count as it was. -check_inserts_nothing(Term, Id) :- - store_count(Before), - ( intern(Term, Id) - -> Answered = true - ; Answered = false - ), - store_count(After), - Before =:= After, - Answered == false. - -%! shape_indexed(+Head) the just in time indexer built an index on the -% first argument of the first argument, which is the shape. -shape_indexed(Head) :- - predicate_property(Head, indexed(Indexes)), - member(Index, Indexes), - get_dict(arguments, Index, [1]), - get_dict(position, Index, [1]), - get_dict(realised, Index, true), - !. - -called_repeatedly(Goal) :- - forall(between(1, 20, _), ( call(Goal) -> true ; true )). - -% ---- the fixtures ---- - -calculus([apply(*, _), lambda(_), variable(_), closure_a(_), closure_b]). -deep_calculus([apply(apply(*, _), _), lambda(_), variable(_), closure_a(_)]). - -fixture(steps, 'hash_consing_fixtures/steps.pl', steps, - [step/2, callee/2, built/2, constant/1], - [ query(shape_of_an_id, - ( calculus(L), internalized(L, apply(lambda(variable(0)), variable(1)), T), - T = '__hash_consed_apply/2'(Shape, _), Shape == 'lambda/1' )), - query(shape_of_a_zero_arity_callee, - ( calculus(L), internalized(L, apply(closure_b, variable(1)), T), - T = '__hash_consed_apply/2'(Shape, _), Shape == 'closure_b/0' )), - query(dispatch_lambda, - ( calculus(L), internalized(L, apply(lambda(variable(0)), variable(1)), T), - steps:step(T, R), externalized(R, E), E == beta(variable(0), variable(1)) )), - query(dispatch_closure, - ( calculus(L), internalized(L, apply(closure_a(variable(7)), closure_b), T), - steps:step(T, R), externalized(R, E), E == compiled(variable(7), closure_b) )), - query(dispatch_zero_arity, - ( calculus(L), internalized(L, apply(closure_b, variable(3)), T), - steps:step(T, R), externalized(R, E), E == constant(variable(3)) )), - query(dispatch_spine, - ( calculus(L), internalized(L, apply(apply(closure_b, variable(1)), variable(2)), T), - steps:step(T, R), externalized(R, E), - E == spine(closure_b, variable(1), variable(2)) )), - query(one_answer_per_term, - ( calculus(L), internalized(L, apply(lambda(variable(0)), variable(1)), T), - aggregate_all(count, steps:step(T, _), Count), Count == 1 )), - query(partial_pattern_matches_every_shape, - ( calculus(L), internalized(L, apply(closure_a(variable(7)), closure_b), T), - steps:callee(T, F), externalized(F, E), E == closure_a(variable(7)) )), - query(body_goal_builds_the_shape, - ( calculus(L), internalized(L, lambda(variable(0)), F), - steps:built(F, B), B = '__hash_consed_apply/2'(Shape, _), Shape == 'lambda/1', - internalized(L, apply(lambda(variable(0)), variable(0)), T), B == T )), - query(ground_occurrence_baked, - ( steps:constant(C), externalized(C, E), E == apply(lambda(variable(0)), closure_b), - calculus(L), internalized(L, E, T), C == T )), - query(same_content_same_id, - ( intern(variable(5), V), intern(lambda(V), F), - intern(apply(F, V), First), intern(apply(F, V), Second), First == Second )), - query(backward, - ( intern(variable(6), V), intern(lambda(V), F), intern(apply(F, V), Id), - intern(Term, Id), Term == apply(F, V) )), - query(wrong_shape_does_not_unify, - ( calculus(L), internalized(L, apply(lambda(variable(0)), variable(1)), T), - \+ T = '__hash_consed_apply/2'('closure_a/1', _) )), - query(spelling_remembered_once, - ( intern(variable(8), V), intern(closure_a(V), F), - spelling_count(Before), - intern(apply(F, V), _), spelling_count(Middle), - intern(variable(9), W), intern(closure_a(W), G), intern(apply(G, W), _), - spelling_count(After), - Middle >= Before, After =:= Middle )), - query(argument_that_is_no_id, - ( intern(apply(3, 4), Id), Id = '__hash_consed_apply/2'(Shape, _), Shape == '-' )), - query(unground_term_raises, - intern(apply(_, _), _) ), - query(externalized_internalized_inverse, - ( calculus(L), External = f(apply(lambda(variable(0)), apply(closure_b, closure_b)), [variable(1)]), - internalized(L, External, Internal), externalized(Internal, Back), Back == External )) - ]). -fixture(spines, 'hash_consing_fixtures/spines.pl', spines, - [head/2, inner/2], - [ query(two_layers_in_the_shape, - ( deep_calculus(L), - internalized(L, apply(apply(lambda(variable(0)), variable(1)), variable(2)), T), - T = '__hash_consed_apply/2'(Shape, _), Shape == 'apply/2(lambda/1)' )), - query(template_ends_the_shape, - ( deep_calculus(L), - internalized(L, apply(apply(apply(lambda(variable(0)), variable(1)), variable(2)), variable(3)), T), - T = '__hash_consed_apply/2'(Shape, _), Shape == 'apply/2(apply/2)' )), - query(dispatch_two_layers, - ( deep_calculus(L), - internalized(L, apply(apply(closure_a(variable(0)), variable(1)), variable(2)), T), - findall(K, spines:head(T, K), Ks), Ks == [compiled_redex_under_an_application] )), - query(dispatch_one_layer, - ( deep_calculus(L), internalized(L, apply(lambda(variable(0)), variable(1)), T), - findall(K, spines:head(T, K), Ks), Ks == [redex] )), - query(partial_pattern_still_right, - ( deep_calculus(L), - internalized(L, apply(apply(closure_a(variable(0)), variable(1)), variable(2)), T), - spines:inner(T, F), externalized(F, E), E == closure_a(variable(0)) )), - query(partial_pattern_rejects_a_redex, - ( deep_calculus(L), internalized(L, apply(lambda(variable(0)), variable(1)), T), - \+ spines:inner(T, _) )) - ]). -fixture(plain, 'hash_consing_fixtures/plain.pl', plain, - [doubled/2, swapped/2], - [ query(upsert_then_externalize, - ( plain:doubled(a, D), externalized(D, E), E == pair(a, a) )), - query(same_content_same_id, - ( plain:doubled(a, D), plain:swapped(D, S), D == S )), - query(value_that_is_no_id_fails, - plain:doubled(_, foo) ), - query(uninterned_instance_fails, - plain:doubled(_, pair(a, a)) ), - query(both_sides_unknown_raises, - plain:swapped(_, _) ) - ]). -fixture(inner_dispatch, 'hash_consing_fixtures/inner_dispatch.pl', inner_dispatch, [], - [ query(dispatch_by_inner_constructor, - ( internalized([apply(*, _), closure_39(_)], apply(closure_39(x), y), T), - findall(K, inner_dispatch:kind(T, K), Ks), Ks == [closure_39] )), - query(shape_indexed, - ( internalized([apply(*, _), closure_39(_)], apply(closure_39(x), y), T), - called_repeatedly(inner_dispatch:kind(T, _)), - shape_indexed(inner_dispatch:kind(_, _)) )) - ]). -fixture(reconfigured, 'hash_consing_fixtures/reconfigured.pl', reconfigured, [], []). diff --git a/test/hash_consing_rewrite.sh b/test/hash_consing_rewrite.sh deleted file mode 100755 index 2f9c241..0000000 --- a/test/hash_consing_rewrite.sh +++ /dev/null @@ -1,15 +0,0 @@ -#!/bin/sh -# The test of the hash_consing library: every -# fixture in its own process at the day-to-day budget, -# --stack-limit=32m --table-space=32m outside, call_with_time_limit(1) -# around each query inside, `timeout 20` around process startup. -# -# Usage: ./hash_consing_rewrite.sh | diff - hash_consing_rewrite_baseline.txt -# must print nothing. -SELF_DIRECTORY="$(cd "$(dirname "$0")" && pwd)" -cd "$SELF_DIRECTORY" || exit 1 -for FIXTURE in steps spines plain inner_dispatch reconfigured; do - LANG=C.UTF-8 LC_ALL=C.UTF-8 timeout 20 \ - swipl -q --stack-limit=32m --table-space=32m hash_consing_rewrite.pl -- --fixture="$FIXTURE" 2>&1 \ - || echo "fixture($FIXTURE, process_exit($?))" -done diff --git a/test/hash_consing_rewrite_baseline.txt b/test/hash_consing_rewrite_baseline.txt deleted file mode 100644 index 95de4c8..0000000 --- a/test/hash_consing_rewrite_baseline.txt +++ /dev/null @@ -1,385 +0,0 @@ -fixture(steps) -predicate(step/2) -step('__hash_consed_apply/2'('lambda/1', A), beta(B, C)) :- - ( nonvar(A) - -> hash_consing:intern(apply('__hash_consed_lambda/1'(D), C), '__hash_consed_apply/2'('lambda/1', A)), - hash_consing:intern(lambda(B), '__hash_consed_lambda/1'(D)) - ; ( nonvar(A) - -> hash_consing:intern(apply('__hash_consed_lambda/1'(D), C), '__hash_consed_apply/2'('lambda/1', A)) - ; true - ), - ( nonvar(D) - -> hash_consing:intern(lambda(B), '__hash_consed_lambda/1'(D)) - ; true - ), - ( var(D), - ground(lambda(B)) - -> hash_consing:intern(lambda(B), '__hash_consed_lambda/1'(D)) - ; true - ), - ( var(A), - ground(apply('__hash_consed_lambda/1'(D), C)) - -> hash_consing:intern(apply('__hash_consed_lambda/1'(D), C), '__hash_consed_apply/2'('lambda/1', A)) - ; true - ), - ( var(D) - -> hash_consing:intern(lambda(B), '__hash_consed_lambda/1'(D)) - ; true - ), - ( var(A) - -> hash_consing:intern(apply('__hash_consed_lambda/1'(D), C), '__hash_consed_apply/2'('lambda/1', A)) - ; true - ) - ). -step('__hash_consed_apply/2'('closure_a/1', A), compiled(B, C)) :- - ( nonvar(A) - -> hash_consing:intern(apply('__hash_consed_closure_a/1'(D), C), '__hash_consed_apply/2'('closure_a/1', A)), - hash_consing:intern(closure_a(B), '__hash_consed_closure_a/1'(D)) - ; ( nonvar(A) - -> hash_consing:intern(apply('__hash_consed_closure_a/1'(D), C), '__hash_consed_apply/2'('closure_a/1', A)) - ; true - ), - ( nonvar(D) - -> hash_consing:intern(closure_a(B), '__hash_consed_closure_a/1'(D)) - ; true - ), - ( var(D), - ground(closure_a(B)) - -> hash_consing:intern(closure_a(B), '__hash_consed_closure_a/1'(D)) - ; true - ), - ( var(A), - ground(apply('__hash_consed_closure_a/1'(D), C)) - -> hash_consing:intern(apply('__hash_consed_closure_a/1'(D), C), '__hash_consed_apply/2'('closure_a/1', A)) - ; true - ), - ( var(D) - -> hash_consing:intern(closure_a(B), '__hash_consed_closure_a/1'(D)) - ; true - ), - ( var(A) - -> hash_consing:intern(apply('__hash_consed_closure_a/1'(D), C), '__hash_consed_apply/2'('closure_a/1', A)) - ; true - ) - ). -step('__hash_consed_apply/2'('closure_b/0', A), constant(B)) :- - ( nonvar(A) - -> hash_consing:intern(apply(baked(closure_b), B), '__hash_consed_apply/2'('closure_b/0', A)) - ; ( nonvar(A) - -> hash_consing:intern(apply(baked(closure_b), B), '__hash_consed_apply/2'('closure_b/0', A)) - ; true - ), - ( var(A), - ground(apply(baked(closure_b), B)) - -> hash_consing:intern(apply(baked(closure_b), B), '__hash_consed_apply/2'('closure_b/0', A)) - ; true - ), - ( var(A) - -> hash_consing:intern(apply(baked(closure_b), B), '__hash_consed_apply/2'('closure_b/0', A)) - ; true - ) - ). -step('__hash_consed_apply/2'('apply/2', A), spine(B, C, D)) :- - ( nonvar(A) - -> hash_consing:intern(apply('__hash_consed_apply/2'(E, F), D), '__hash_consed_apply/2'('apply/2', A)), - hash_consing:intern(apply(B, C), '__hash_consed_apply/2'(E, F)) - ; ( nonvar(A) - -> hash_consing:intern(apply('__hash_consed_apply/2'(E, F), D), '__hash_consed_apply/2'('apply/2', A)) - ; true - ), - ( nonvar(F) - -> hash_consing:intern(apply(B, C), '__hash_consed_apply/2'(E, F)) - ; true - ), - ( var(F), - ground(apply(B, C)) - -> hash_consing:intern(apply(B, C), '__hash_consed_apply/2'(E, F)) - ; true - ), - ( var(A), - ground(apply('__hash_consed_apply/2'(E, F), D)) - -> hash_consing:intern(apply('__hash_consed_apply/2'(E, F), D), '__hash_consed_apply/2'('apply/2', A)) - ; true - ), - ( var(F) - -> hash_consing:intern(apply(B, C), '__hash_consed_apply/2'(E, F)) - ; true - ), - ( var(A) - -> hash_consing:intern(apply('__hash_consed_apply/2'(E, F), D), '__hash_consed_apply/2'('apply/2', A)) - ; true - ) - ). -predicate(callee/2) -callee('__hash_consed_apply/2'(A, B), C) :- - ( nonvar(B) - -> hash_consing:intern(apply(C, D), '__hash_consed_apply/2'(A, B)) - ; ( nonvar(B) - -> hash_consing:intern(apply(C, D), '__hash_consed_apply/2'(A, B)) - ; true - ), - ( var(B), - ground(apply(C, D)) - -> hash_consing:intern(apply(C, D), '__hash_consed_apply/2'(A, B)) - ; true - ), - ( var(B) - -> hash_consing:intern(apply(C, D), '__hash_consed_apply/2'(A, B)) - ; true - ) - ). -predicate(built/2) -built(A, B) :- - ( ground([A]) - -> hash_consing:intern(apply(A, baked(variable(0))), '__hash_consed_apply/2'(C, D)), - B='__hash_consed_apply/2'(C, D) - ; ( ground(apply(A, baked(variable(0)))) - -> hash_consing:intern(apply(A, baked(variable(0))), '__hash_consed_apply/2'(C, D)) - ; true - ), - B='__hash_consed_apply/2'(C, D), - hash_consing:intern(apply(A, baked(variable(0))), '__hash_consed_apply/2'(C, D)) - ). -predicate(constant/1) -constant(baked(apply(lambda(variable(0)), closure_b))). -query(shape_of_an_id, true) -query(shape_of_a_zero_arity_callee, true) -query(dispatch_lambda, true) -query(dispatch_closure, true) -query(dispatch_zero_arity, true) -query(dispatch_spine, true) -query(one_answer_per_term, true) -query(partial_pattern_matches_every_shape, true) -query(body_goal_builds_the_shape, true) -query(ground_occurrence_baked, true) -query(same_content_same_id, true) -query(backward, true) -query(wrong_shape_does_not_unify, true) -query(spelling_remembered_once, true) -query(argument_that_is_no_id, true) -query(unground_term_raises, error(instantiation_error)) -query(externalized_internalized_inverse, true) -fixture(spines) -predicate(head/2) -head('__hash_consed_apply/2'('apply/2(lambda/1)', A), redex_under_an_application) :- - ( nonvar(A) - -> hash_consing:intern(apply('__hash_consed_apply/2'('lambda/1', B), C), '__hash_consed_apply/2'('apply/2(lambda/1)', A)), - hash_consing:intern(apply('__hash_consed_lambda/1'(D), E), '__hash_consed_apply/2'('lambda/1', B)), - hash_consing:intern(lambda(F), '__hash_consed_lambda/1'(D)) - ; ( nonvar(A) - -> hash_consing:intern(apply('__hash_consed_apply/2'('lambda/1', B), C), '__hash_consed_apply/2'('apply/2(lambda/1)', A)) - ; true - ), - ( nonvar(B) - -> hash_consing:intern(apply('__hash_consed_lambda/1'(D), E), '__hash_consed_apply/2'('lambda/1', B)) - ; true - ), - ( nonvar(D) - -> hash_consing:intern(lambda(F), '__hash_consed_lambda/1'(D)) - ; true - ), - ( var(D), - ground(lambda(F)) - -> hash_consing:intern(lambda(F), '__hash_consed_lambda/1'(D)) - ; true - ), - ( var(B), - ground(apply('__hash_consed_lambda/1'(D), E)) - -> hash_consing:intern(apply('__hash_consed_lambda/1'(D), E), '__hash_consed_apply/2'('lambda/1', B)) - ; true - ), - ( var(A), - ground(apply('__hash_consed_apply/2'('lambda/1', B), C)) - -> hash_consing:intern(apply('__hash_consed_apply/2'('lambda/1', B), C), '__hash_consed_apply/2'('apply/2(lambda/1)', A)) - ; true - ), - ( var(D) - -> hash_consing:intern(lambda(F), '__hash_consed_lambda/1'(D)) - ; true - ), - ( var(B) - -> hash_consing:intern(apply('__hash_consed_lambda/1'(D), E), '__hash_consed_apply/2'('lambda/1', B)) - ; true - ), - ( var(A) - -> hash_consing:intern(apply('__hash_consed_apply/2'('lambda/1', B), C), '__hash_consed_apply/2'('apply/2(lambda/1)', A)) - ; true - ) - ). -head('__hash_consed_apply/2'('apply/2(closure_a/1)', A), compiled_redex_under_an_application) :- - ( nonvar(A) - -> hash_consing:intern(apply('__hash_consed_apply/2'('closure_a/1', B), C), '__hash_consed_apply/2'('apply/2(closure_a/1)', A)), - hash_consing:intern(apply('__hash_consed_closure_a/1'(D), E), '__hash_consed_apply/2'('closure_a/1', B)), - hash_consing:intern(closure_a(F), '__hash_consed_closure_a/1'(D)) - ; ( nonvar(A) - -> hash_consing:intern(apply('__hash_consed_apply/2'('closure_a/1', B), C), '__hash_consed_apply/2'('apply/2(closure_a/1)', A)) - ; true - ), - ( nonvar(B) - -> hash_consing:intern(apply('__hash_consed_closure_a/1'(D), E), '__hash_consed_apply/2'('closure_a/1', B)) - ; true - ), - ( nonvar(D) - -> hash_consing:intern(closure_a(F), '__hash_consed_closure_a/1'(D)) - ; true - ), - ( var(D), - ground(closure_a(F)) - -> hash_consing:intern(closure_a(F), '__hash_consed_closure_a/1'(D)) - ; true - ), - ( var(B), - ground(apply('__hash_consed_closure_a/1'(D), E)) - -> hash_consing:intern(apply('__hash_consed_closure_a/1'(D), E), '__hash_consed_apply/2'('closure_a/1', B)) - ; true - ), - ( var(A), - ground(apply('__hash_consed_apply/2'('closure_a/1', B), C)) - -> hash_consing:intern(apply('__hash_consed_apply/2'('closure_a/1', B), C), '__hash_consed_apply/2'('apply/2(closure_a/1)', A)) - ; true - ), - ( var(D) - -> hash_consing:intern(closure_a(F), '__hash_consed_closure_a/1'(D)) - ; true - ), - ( var(B) - -> hash_consing:intern(apply('__hash_consed_closure_a/1'(D), E), '__hash_consed_apply/2'('closure_a/1', B)) - ; true - ), - ( var(A) - -> hash_consing:intern(apply('__hash_consed_apply/2'('closure_a/1', B), C), '__hash_consed_apply/2'('apply/2(closure_a/1)', A)) - ; true - ) - ). -head('__hash_consed_apply/2'('lambda/1', A), redex) :- - ( nonvar(A) - -> hash_consing:intern(apply('__hash_consed_lambda/1'(B), C), '__hash_consed_apply/2'('lambda/1', A)), - hash_consing:intern(lambda(D), '__hash_consed_lambda/1'(B)) - ; ( nonvar(A) - -> hash_consing:intern(apply('__hash_consed_lambda/1'(B), C), '__hash_consed_apply/2'('lambda/1', A)) - ; true - ), - ( nonvar(B) - -> hash_consing:intern(lambda(D), '__hash_consed_lambda/1'(B)) - ; true - ), - ( var(B), - ground(lambda(D)) - -> hash_consing:intern(lambda(D), '__hash_consed_lambda/1'(B)) - ; true - ), - ( var(A), - ground(apply('__hash_consed_lambda/1'(B), C)) - -> hash_consing:intern(apply('__hash_consed_lambda/1'(B), C), '__hash_consed_apply/2'('lambda/1', A)) - ; true - ), - ( var(B) - -> hash_consing:intern(lambda(D), '__hash_consed_lambda/1'(B)) - ; true - ), - ( var(A) - -> hash_consing:intern(apply('__hash_consed_lambda/1'(B), C), '__hash_consed_apply/2'('lambda/1', A)) - ; true - ) - ). -predicate(inner/2) -inner('__hash_consed_apply/2'(A, B), C) :- - ( nonvar(B) - -> hash_consing:intern(apply('__hash_consed_apply/2'(D, E), F), '__hash_consed_apply/2'(A, B)), - hash_consing:intern(apply(C, G), '__hash_consed_apply/2'(D, E)) - ; ( nonvar(B) - -> hash_consing:intern(apply('__hash_consed_apply/2'(D, E), F), '__hash_consed_apply/2'(A, B)) - ; true - ), - ( nonvar(E) - -> hash_consing:intern(apply(C, G), '__hash_consed_apply/2'(D, E)) - ; true - ), - ( var(E), - ground(apply(C, G)) - -> hash_consing:intern(apply(C, G), '__hash_consed_apply/2'(D, E)) - ; true - ), - ( var(B), - ground(apply('__hash_consed_apply/2'(D, E), F)) - -> hash_consing:intern(apply('__hash_consed_apply/2'(D, E), F), '__hash_consed_apply/2'(A, B)) - ; true - ), - ( var(E) - -> hash_consing:intern(apply(C, G), '__hash_consed_apply/2'(D, E)) - ; true - ), - ( var(B) - -> hash_consing:intern(apply('__hash_consed_apply/2'(D, E), F), '__hash_consed_apply/2'(A, B)) - ; true - ) - ). -query(two_layers_in_the_shape, true) -query(template_ends_the_shape, true) -query(dispatch_two_layers, true) -query(dispatch_one_layer, true) -query(partial_pattern_still_right, true) -query(partial_pattern_rejects_a_redex, true) -fixture(plain) -predicate(doubled/2) -doubled(A, '__hash_consed_pair/2'(B)) :- - ( nonvar(B) - -> hash_consing:intern(pair(A, A), '__hash_consed_pair/2'(B)) - ; ( nonvar(B) - -> hash_consing:intern(pair(A, A), '__hash_consed_pair/2'(B)) - ; true - ), - ( var(B), - ground(pair(A, A)) - -> hash_consing:intern(pair(A, A), '__hash_consed_pair/2'(B)) - ; true - ), - ( var(B) - -> hash_consing:intern(pair(A, A), '__hash_consed_pair/2'(B)) - ; true - ) - ). -predicate(swapped/2) -swapped('__hash_consed_pair/2'(A), '__hash_consed_pair/2'(B)) :- - ( nonvar(A), - nonvar(B) - -> hash_consing:intern(pair(C, D), '__hash_consed_pair/2'(B)), - hash_consing:intern(pair(D, C), '__hash_consed_pair/2'(A)) - ; ( nonvar(B) - -> hash_consing:intern(pair(C, D), '__hash_consed_pair/2'(B)) - ; true - ), - ( nonvar(A) - -> hash_consing:intern(pair(D, C), '__hash_consed_pair/2'(A)) - ; true - ), - ( var(A), - ground(pair(D, C)) - -> hash_consing:intern(pair(D, C), '__hash_consed_pair/2'(A)) - ; true - ), - ( var(B), - ground(pair(C, D)) - -> hash_consing:intern(pair(C, D), '__hash_consed_pair/2'(B)) - ; true - ), - ( var(A) - -> hash_consing:intern(pair(D, C), '__hash_consed_pair/2'(A)) - ; true - ), - ( var(B) - -> hash_consing:intern(pair(C, D), '__hash_consed_pair/2'(B)) - ; true - ) - ). -query(upsert_then_externalize, true) -query(same_content_same_id, true) -query(value_that_is_no_id_fails, false) -query(uninterned_instance_fails, false) -query(both_sides_unknown_raises, error(instantiation_error)) -fixture(inner_dispatch) -query(dispatch_by_inner_constructor, true) -query(shape_indexed, true) -fixture(reconfigured) -load_error(permission_error(reconfigure,interned_constructor,apply/2)) -load_error(directive_failed) diff --git a/test/hash_consing_snapshots/inner_dispatch.txt b/test/hash_consing_snapshots/inner_dispatch.txt new file mode 100644 index 0000000..e69de29 diff --git a/test/hash_consing_snapshots/patterns.txt b/test/hash_consing_snapshots/patterns.txt new file mode 100644 index 0000000..6b36d57 --- /dev/null +++ b/test/hash_consing_snapshots/patterns.txt @@ -0,0 +1,325 @@ +predicate(kind/2) +kind('__hash_consed_app/2'('abs/1', A), redex) :- + ( nonvar(A) + -> hash_consing:intern(app('__hash_consed_abs/1'(B), C), '__hash_consed_app/2'('abs/1', A)), + hash_consing:intern(abs(D), '__hash_consed_abs/1'(B)) + ; ( nonvar(A) + -> hash_consing:intern(app('__hash_consed_abs/1'(B), C), '__hash_consed_app/2'('abs/1', A)) + ; true + ), + ( nonvar(B) + -> hash_consing:intern(abs(D), '__hash_consed_abs/1'(B)) + ; true + ), + ( var(B), + ground(abs(D)) + -> hash_consing:intern(abs(D), '__hash_consed_abs/1'(B)) + ; true + ), + ( var(A), + ground(app('__hash_consed_abs/1'(B), C)) + -> hash_consing:intern(app('__hash_consed_abs/1'(B), C), '__hash_consed_app/2'('abs/1', A)) + ; true + ), + ( var(B) + -> hash_consing:intern(abs(D), '__hash_consed_abs/1'(B)) + ; true + ), + ( var(A) + -> hash_consing:intern(app('__hash_consed_abs/1'(B), C), '__hash_consed_app/2'('abs/1', A)) + ; true + ) + ). +kind('__hash_consed_app/2'('app/2(abs/1)', A), redex_under_an_application) :- + ( nonvar(A) + -> hash_consing:intern(app('__hash_consed_app/2'('abs/1', B), C), '__hash_consed_app/2'('app/2(abs/1)', A)), + hash_consing:intern(app('__hash_consed_abs/1'(D), E), '__hash_consed_app/2'('abs/1', B)), + hash_consing:intern(abs(F), '__hash_consed_abs/1'(D)) + ; ( nonvar(A) + -> hash_consing:intern(app('__hash_consed_app/2'('abs/1', B), C), '__hash_consed_app/2'('app/2(abs/1)', A)) + ; true + ), + ( nonvar(B) + -> hash_consing:intern(app('__hash_consed_abs/1'(D), E), '__hash_consed_app/2'('abs/1', B)) + ; true + ), + ( nonvar(D) + -> hash_consing:intern(abs(F), '__hash_consed_abs/1'(D)) + ; true + ), + ( var(D), + ground(abs(F)) + -> hash_consing:intern(abs(F), '__hash_consed_abs/1'(D)) + ; true + ), + ( var(B), + ground(app('__hash_consed_abs/1'(D), E)) + -> hash_consing:intern(app('__hash_consed_abs/1'(D), E), '__hash_consed_app/2'('abs/1', B)) + ; true + ), + ( var(A), + ground(app('__hash_consed_app/2'('abs/1', B), C)) + -> hash_consing:intern(app('__hash_consed_app/2'('abs/1', B), C), '__hash_consed_app/2'('app/2(abs/1)', A)) + ; true + ), + ( var(D) + -> hash_consing:intern(abs(F), '__hash_consed_abs/1'(D)) + ; true + ), + ( var(B) + -> hash_consing:intern(app('__hash_consed_abs/1'(D), E), '__hash_consed_app/2'('abs/1', B)) + ; true + ), + ( var(A) + -> hash_consing:intern(app('__hash_consed_app/2'('abs/1', B), C), '__hash_consed_app/2'('app/2(abs/1)', A)) + ; true + ) + ). +kind('__hash_consed_app/2'('ref/1', A), stuck) :- + ( nonvar(A) + -> hash_consing:intern(app('__hash_consed_ref/1'(B), '__hash_consed_ref/1'(C)), '__hash_consed_app/2'('ref/1', A)), + hash_consing:intern(ref(D), '__hash_consed_ref/1'(C)), + hash_consing:intern(ref(E), '__hash_consed_ref/1'(B)) + ; ( nonvar(A) + -> hash_consing:intern(app('__hash_consed_ref/1'(B), '__hash_consed_ref/1'(C)), '__hash_consed_app/2'('ref/1', A)) + ; true + ), + ( nonvar(C) + -> hash_consing:intern(ref(D), '__hash_consed_ref/1'(C)) + ; true + ), + ( nonvar(B) + -> hash_consing:intern(ref(E), '__hash_consed_ref/1'(B)) + ; true + ), + ( var(B), + ground(ref(E)) + -> hash_consing:intern(ref(E), '__hash_consed_ref/1'(B)) + ; true + ), + ( var(C), + ground(ref(D)) + -> hash_consing:intern(ref(D), '__hash_consed_ref/1'(C)) + ; true + ), + ( var(A), + ground(app('__hash_consed_ref/1'(B), '__hash_consed_ref/1'(C))) + -> hash_consing:intern(app('__hash_consed_ref/1'(B), '__hash_consed_ref/1'(C)), '__hash_consed_app/2'('ref/1', A)) + ; true + ), + ( var(B) + -> hash_consing:intern(ref(E), '__hash_consed_ref/1'(B)) + ; true + ), + ( var(C) + -> hash_consing:intern(ref(D), '__hash_consed_ref/1'(C)) + ; true + ), + ( var(A) + -> hash_consing:intern(app('__hash_consed_ref/1'(B), '__hash_consed_ref/1'(C)), '__hash_consed_app/2'('ref/1', A)) + ; true + ) + ). +kind(app('__hash_consed_ref/1'(A), '__hash_consed_abs/1'(B)), plain) :- + ( nonvar(A), + nonvar(B) + -> hash_consing:intern(abs(C), '__hash_consed_abs/1'(B)), + hash_consing:intern(ref(D), '__hash_consed_ref/1'(A)) + ; ( nonvar(B) + -> hash_consing:intern(abs(C), '__hash_consed_abs/1'(B)) + ; true + ), + ( nonvar(A) + -> hash_consing:intern(ref(D), '__hash_consed_ref/1'(A)) + ; true + ), + ( var(A), + ground(ref(D)) + -> hash_consing:intern(ref(D), '__hash_consed_ref/1'(A)) + ; true + ), + ( var(B), + ground(abs(C)) + -> hash_consing:intern(abs(C), '__hash_consed_abs/1'(B)) + ; true + ), + ( var(A) + -> hash_consing:intern(ref(D), '__hash_consed_ref/1'(A)) + ; true + ), + ( var(B) + -> hash_consing:intern(abs(C), '__hash_consed_abs/1'(B)) + ; true + ) + ). +predicate(size/2) +size(A, B) :- + ( nonvar(A), + ( A='__hash_consed_app/2'(_, C) + -> nonvar(C) + ; true + ) + -> hash_consing:represented(app(D, E), A), + size(D, F), + size(E, G), + B is F+G+1 + ; ( nonvar(A), + ( A='__hash_consed_app/2'(_, H) + -> nonvar(H) + ; true + ) + -> hash_consing:represented(app(D, E), A) + ; true + ), + ( \+ ( nonvar(A), + ( A='__hash_consed_app/2'(_, I) + -> nonvar(I) + ; true + ) + ), + ground(app(D, E)) + -> hash_consing:represented(app(D, E), A) + ; true + ), + size(D, F), + size(E, G), + B is F+G+1, + ( nonvar(A), + ( A='__hash_consed_app/2'(_, J) + -> nonvar(J) + ; true + ) + -> true + ; hash_consing:represented_settled(app(D, E), A) + ) + ). +size('__hash_consed_abs/1'(A), B) :- + ( nonvar(A) + -> hash_consing:intern(abs(C), '__hash_consed_abs/1'(A)), + size(C, D), + B is D+1 + ; ( nonvar(A) + -> hash_consing:intern(abs(C), '__hash_consed_abs/1'(A)) + ; true + ), + ( var(A), + ground(abs(C)) + -> hash_consing:intern(abs(C), '__hash_consed_abs/1'(A)) + ; true + ), + size(C, D), + B is D+1, + ( var(A) + -> hash_consing:intern(abs(C), '__hash_consed_abs/1'(A)) + ; true + ) + ). +size('__hash_consed_ref/1'(A), 1) :- + ( nonvar(A) + -> hash_consing:intern(ref(B), '__hash_consed_ref/1'(A)) + ; ( nonvar(A) + -> hash_consing:intern(ref(B), '__hash_consed_ref/1'(A)) + ; true + ), + ( var(A), + ground(ref(B)) + -> hash_consing:intern(ref(B), '__hash_consed_ref/1'(A)) + ; true + ), + ( var(A) + -> hash_consing:intern(ref(B), '__hash_consed_ref/1'(A)) + ; true + ) + ). +predicate(wrapped/2) +wrapped(A, B) :- + ( nonvar(B), + ( B='__hash_consed_app/2'(_, C) + -> nonvar(C) + ; true + ) + -> hash_consing:represented(app(A, baked(abs(ref(0)))), B) + ; ( nonvar(B), + ( B='__hash_consed_app/2'(_, D) + -> nonvar(D) + ; true + ) + -> hash_consing:represented(app(A, baked(abs(ref(0)))), B) + ; true + ), + ( \+ ( nonvar(B), + ( B='__hash_consed_app/2'(_, E) + -> nonvar(E) + ; true + ) + ), + ground(app(A, baked(abs(ref(0))))) + -> hash_consing:represented(app(A, baked(abs(ref(0)))), B) + ; true + ), + ( nonvar(B), + ( B='__hash_consed_app/2'(_, F) + -> nonvar(F) + ; true + ) + -> true + ; hash_consing:represented_settled(app(A, baked(abs(ref(0)))), B) + ) + ). +predicate(first/2) +first(A, B) :- + ( nonvar(B), + ( B='__hash_consed_app/2'(_, C) + -> nonvar(C) + ; true + ) + -> hash_consing:represented(app(D, E), B), + member(D-E, A), + ! + ; ( nonvar(B), + ( B='__hash_consed_app/2'(_, F) + -> nonvar(F) + ; true + ) + -> hash_consing:represented(app(D, E), B) + ; true + ), + ( \+ ( nonvar(B), + ( B='__hash_consed_app/2'(_, G) + -> nonvar(G) + ; true + ) + ), + ground(app(D, E)) + -> hash_consing:represented(app(D, E), B) + ; true + ), + member(D-E, A), + !, + ( nonvar(B), + ( B='__hash_consed_app/2'(_, H) + -> nonvar(H) + ; true + ) + -> true + ; hash_consing:represented_settled(app(D, E), B) + ) + ). +predicate(built/2) +built(A, B) :- + ( ground([A]) + -> hash_consing:represented(app(A, baked(abs(ref(0)))), C), + B=C + ; hash_consing:represented(app(A, baked(abs(ref(0)))), C), + B=C, + hash_consing:represented(app(A, baked(abs(ref(0)))), C) + ). +predicate(unbound_built/1) +unbound_built(A) :- + ( ground([B]) + -> hash_consing:represented(app(B, baked(abs(ref(0)))), C), + A=C + ; hash_consing:represented(app(B, baked(abs(ref(0)))), C), + A=C, + hash_consing:represented(app(B, baked(abs(ref(0)))), C) + ). diff --git a/test/hash_consing_snapshots/plain.txt b/test/hash_consing_snapshots/plain.txt new file mode 100644 index 0000000..af3cea4 --- /dev/null +++ b/test/hash_consing_snapshots/plain.txt @@ -0,0 +1,51 @@ +predicate(doubled/2) +doubled(A, '__hash_consed_pair/2'(B)) :- + ( nonvar(B) + -> hash_consing:intern(pair(A, A), '__hash_consed_pair/2'(B)) + ; ( nonvar(B) + -> hash_consing:intern(pair(A, A), '__hash_consed_pair/2'(B)) + ; true + ), + ( var(B), + ground(pair(A, A)) + -> hash_consing:intern(pair(A, A), '__hash_consed_pair/2'(B)) + ; true + ), + ( var(B) + -> hash_consing:intern(pair(A, A), '__hash_consed_pair/2'(B)) + ; true + ) + ). +predicate(swapped/2) +swapped('__hash_consed_pair/2'(A), '__hash_consed_pair/2'(B)) :- + ( nonvar(A), + nonvar(B) + -> hash_consing:intern(pair(C, D), '__hash_consed_pair/2'(B)), + hash_consing:intern(pair(D, C), '__hash_consed_pair/2'(A)) + ; ( nonvar(B) + -> hash_consing:intern(pair(C, D), '__hash_consed_pair/2'(B)) + ; true + ), + ( nonvar(A) + -> hash_consing:intern(pair(D, C), '__hash_consed_pair/2'(A)) + ; true + ), + ( var(A), + ground(pair(D, C)) + -> hash_consing:intern(pair(D, C), '__hash_consed_pair/2'(A)) + ; true + ), + ( var(B), + ground(pair(C, D)) + -> hash_consing:intern(pair(C, D), '__hash_consed_pair/2'(B)) + ; true + ), + ( var(A) + -> hash_consing:intern(pair(D, C), '__hash_consed_pair/2'(A)) + ; true + ), + ( var(B) + -> hash_consing:intern(pair(C, D), '__hash_consed_pair/2'(B)) + ; true + ) + ). diff --git a/test/hash_consing_snapshots/reconfigured.txt b/test/hash_consing_snapshots/reconfigured.txt new file mode 100644 index 0000000..2aa9d29 --- /dev/null +++ b/test/hash_consing_snapshots/reconfigured.txt @@ -0,0 +1,2 @@ +load_error(permission_error(reconfigure,interned_constructor,apply/2)) +load_error(directive_failed) diff --git a/test/hash_consing_snapshots/spines.txt b/test/hash_consing_snapshots/spines.txt new file mode 100644 index 0000000..759fb73 --- /dev/null +++ b/test/hash_consing_snapshots/spines.txt @@ -0,0 +1,125 @@ +predicate(head/2) +head('__hash_consed_application/2'('application/2(lambda/1)', A), redex_under_an_application) :- + ( nonvar(A) + -> hash_consing:intern(application(application('__hash_consed_lambda/1'(B), C), D), '__hash_consed_application/2'('application/2(lambda/1)', A)), + hash_consing:intern(lambda(E), '__hash_consed_lambda/1'(B)) + ; ( nonvar(A) + -> hash_consing:intern(application(application('__hash_consed_lambda/1'(B), C), D), '__hash_consed_application/2'('application/2(lambda/1)', A)) + ; true + ), + ( nonvar(B) + -> hash_consing:intern(lambda(E), '__hash_consed_lambda/1'(B)) + ; true + ), + ( var(B), + ground(lambda(E)) + -> hash_consing:intern(lambda(E), '__hash_consed_lambda/1'(B)) + ; true + ), + ( var(A), + ground(application(application('__hash_consed_lambda/1'(B), C), D)) + -> hash_consing:intern(application(application('__hash_consed_lambda/1'(B), C), D), '__hash_consed_application/2'('application/2(lambda/1)', A)) + ; true + ), + ( var(B) + -> hash_consing:intern(lambda(E), '__hash_consed_lambda/1'(B)) + ; true + ), + ( var(A) + -> hash_consing:intern(application(application('__hash_consed_lambda/1'(B), C), D), '__hash_consed_application/2'('application/2(lambda/1)', A)) + ; true + ) + ). +head('__hash_consed_application/2'('application/2(closure/1)', A), compiled_redex_under_an_application) :- + ( nonvar(A) + -> hash_consing:intern(application(application('__hash_consed_closure/1'(B), C), D), '__hash_consed_application/2'('application/2(closure/1)', A)), + hash_consing:intern(closure(E), '__hash_consed_closure/1'(B)) + ; ( nonvar(A) + -> hash_consing:intern(application(application('__hash_consed_closure/1'(B), C), D), '__hash_consed_application/2'('application/2(closure/1)', A)) + ; true + ), + ( nonvar(B) + -> hash_consing:intern(closure(E), '__hash_consed_closure/1'(B)) + ; true + ), + ( var(B), + ground(closure(E)) + -> hash_consing:intern(closure(E), '__hash_consed_closure/1'(B)) + ; true + ), + ( var(A), + ground(application(application('__hash_consed_closure/1'(B), C), D)) + -> hash_consing:intern(application(application('__hash_consed_closure/1'(B), C), D), '__hash_consed_application/2'('application/2(closure/1)', A)) + ; true + ), + ( var(B) + -> hash_consing:intern(closure(E), '__hash_consed_closure/1'(B)) + ; true + ), + ( var(A) + -> hash_consing:intern(application(application('__hash_consed_closure/1'(B), C), D), '__hash_consed_application/2'('application/2(closure/1)', A)) + ; true + ) + ). +head(application('__hash_consed_lambda/1'(A), _), redex) :- + ( nonvar(A) + -> hash_consing:intern(lambda(B), '__hash_consed_lambda/1'(A)) + ; ( nonvar(A) + -> hash_consing:intern(lambda(B), '__hash_consed_lambda/1'(A)) + ; true + ), + ( var(A), + ground(lambda(B)) + -> hash_consing:intern(lambda(B), '__hash_consed_lambda/1'(A)) + ; true + ), + ( var(A) + -> hash_consing:intern(lambda(B), '__hash_consed_lambda/1'(A)) + ; true + ) + ). +predicate(inner/2) +inner('__hash_consed_application/2'(A, B), C) :- + ( nonvar(B) + -> hash_consing:intern(application(D, E), '__hash_consed_application/2'(A, B)), + hash_consing:represented(application(C, F), D) + ; ( nonvar(B) + -> hash_consing:intern(application(D, E), '__hash_consed_application/2'(A, B)) + ; true + ), + ( nonvar(D), + ( D='__hash_consed_application/2'(_, G) + -> nonvar(G) + ; true + ) + -> hash_consing:represented(application(C, F), D) + ; true + ), + ( \+ ( nonvar(D), + ( D='__hash_consed_application/2'(_, H) + -> nonvar(H) + ; true + ) + ), + ground(application(C, F)) + -> hash_consing:represented(application(C, F), D) + ; true + ), + ( var(B), + ground(application(D, E)) + -> hash_consing:intern(application(D, E), '__hash_consed_application/2'(A, B)) + ; true + ), + ( nonvar(D), + ( D='__hash_consed_application/2'(_, I) + -> nonvar(I) + ; true + ) + -> true + ; hash_consing:represented_settled(application(C, F), D) + ), + ( var(B) + -> hash_consing:intern(application(D, E), '__hash_consed_application/2'(A, B)) + ; true + ) + ). diff --git a/test/hash_consing_snapshots/steps.txt b/test/hash_consing_snapshots/steps.txt new file mode 100644 index 0000000..dfbe8bd --- /dev/null +++ b/test/hash_consing_snapshots/steps.txt @@ -0,0 +1,143 @@ +predicate(step/2) +step('__hash_consed_apply/2'('lambda/1', A), beta(B, C)) :- + ( nonvar(A) + -> hash_consing:intern(apply('__hash_consed_lambda/1'(D), C), '__hash_consed_apply/2'('lambda/1', A)), + hash_consing:intern(lambda(B), '__hash_consed_lambda/1'(D)) + ; ( nonvar(A) + -> hash_consing:intern(apply('__hash_consed_lambda/1'(D), C), '__hash_consed_apply/2'('lambda/1', A)) + ; true + ), + ( nonvar(D) + -> hash_consing:intern(lambda(B), '__hash_consed_lambda/1'(D)) + ; true + ), + ( var(D), + ground(lambda(B)) + -> hash_consing:intern(lambda(B), '__hash_consed_lambda/1'(D)) + ; true + ), + ( var(A), + ground(apply('__hash_consed_lambda/1'(D), C)) + -> hash_consing:intern(apply('__hash_consed_lambda/1'(D), C), '__hash_consed_apply/2'('lambda/1', A)) + ; true + ), + ( var(D) + -> hash_consing:intern(lambda(B), '__hash_consed_lambda/1'(D)) + ; true + ), + ( var(A) + -> hash_consing:intern(apply('__hash_consed_lambda/1'(D), C), '__hash_consed_apply/2'('lambda/1', A)) + ; true + ) + ). +step('__hash_consed_apply/2'('closure_a/1', A), compiled(B, C)) :- + ( nonvar(A) + -> hash_consing:intern(apply('__hash_consed_closure_a/1'(D), C), '__hash_consed_apply/2'('closure_a/1', A)), + hash_consing:intern(closure_a(B), '__hash_consed_closure_a/1'(D)) + ; ( nonvar(A) + -> hash_consing:intern(apply('__hash_consed_closure_a/1'(D), C), '__hash_consed_apply/2'('closure_a/1', A)) + ; true + ), + ( nonvar(D) + -> hash_consing:intern(closure_a(B), '__hash_consed_closure_a/1'(D)) + ; true + ), + ( var(D), + ground(closure_a(B)) + -> hash_consing:intern(closure_a(B), '__hash_consed_closure_a/1'(D)) + ; true + ), + ( var(A), + ground(apply('__hash_consed_closure_a/1'(D), C)) + -> hash_consing:intern(apply('__hash_consed_closure_a/1'(D), C), '__hash_consed_apply/2'('closure_a/1', A)) + ; true + ), + ( var(D) + -> hash_consing:intern(closure_a(B), '__hash_consed_closure_a/1'(D)) + ; true + ), + ( var(A) + -> hash_consing:intern(apply('__hash_consed_closure_a/1'(D), C), '__hash_consed_apply/2'('closure_a/1', A)) + ; true + ) + ). +step('__hash_consed_apply/2'('closure_b/0', A), constant(B)) :- + ( nonvar(A) + -> hash_consing:intern(apply(baked(closure_b), B), '__hash_consed_apply/2'('closure_b/0', A)) + ; ( nonvar(A) + -> hash_consing:intern(apply(baked(closure_b), B), '__hash_consed_apply/2'('closure_b/0', A)) + ; true + ), + ( var(A), + ground(apply(baked(closure_b), B)) + -> hash_consing:intern(apply(baked(closure_b), B), '__hash_consed_apply/2'('closure_b/0', A)) + ; true + ), + ( var(A) + -> hash_consing:intern(apply(baked(closure_b), B), '__hash_consed_apply/2'('closure_b/0', A)) + ; true + ) + ). +step('__hash_consed_apply/2'('apply/2', A), spine(B, C, D)) :- + ( nonvar(A) + -> hash_consing:intern(apply('__hash_consed_apply/2'(E, F), D), '__hash_consed_apply/2'('apply/2', A)), + hash_consing:intern(apply(B, C), '__hash_consed_apply/2'(E, F)) + ; ( nonvar(A) + -> hash_consing:intern(apply('__hash_consed_apply/2'(E, F), D), '__hash_consed_apply/2'('apply/2', A)) + ; true + ), + ( nonvar(F) + -> hash_consing:intern(apply(B, C), '__hash_consed_apply/2'(E, F)) + ; true + ), + ( var(F), + ground(apply(B, C)) + -> hash_consing:intern(apply(B, C), '__hash_consed_apply/2'(E, F)) + ; true + ), + ( var(A), + ground(apply('__hash_consed_apply/2'(E, F), D)) + -> hash_consing:intern(apply('__hash_consed_apply/2'(E, F), D), '__hash_consed_apply/2'('apply/2', A)) + ; true + ), + ( var(F) + -> hash_consing:intern(apply(B, C), '__hash_consed_apply/2'(E, F)) + ; true + ), + ( var(A) + -> hash_consing:intern(apply('__hash_consed_apply/2'(E, F), D), '__hash_consed_apply/2'('apply/2', A)) + ; true + ) + ). +predicate(callee/2) +callee('__hash_consed_apply/2'(A, B), C) :- + ( nonvar(B) + -> hash_consing:intern(apply(C, D), '__hash_consed_apply/2'(A, B)) + ; ( nonvar(B) + -> hash_consing:intern(apply(C, D), '__hash_consed_apply/2'(A, B)) + ; true + ), + ( var(B), + ground(apply(C, D)) + -> hash_consing:intern(apply(C, D), '__hash_consed_apply/2'(A, B)) + ; true + ), + ( var(B) + -> hash_consing:intern(apply(C, D), '__hash_consed_apply/2'(A, B)) + ; true + ) + ). +predicate(built/2) +built(A, B) :- + ( ground([A]) + -> hash_consing:intern(apply(A, baked(variable(0))), '__hash_consed_apply/2'(C, D)), + B='__hash_consed_apply/2'(C, D) + ; ( ground(apply(A, baked(variable(0)))) + -> hash_consing:intern(apply(A, baked(variable(0))), '__hash_consed_apply/2'(C, D)) + ; true + ), + B='__hash_consed_apply/2'(C, D), + hash_consing:intern(apply(A, baked(variable(0))), '__hash_consed_apply/2'(C, D)) + ). +predicate(constant/1) +constant(baked(apply(lambda(variable(0)), closure_b))).