Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
41 changes: 38 additions & 3 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -18,20 +18,47 @@ same Id.

## Use

Keep the directive that names the terms to intern in a file of its own:

```prolog
:- module(steps, [step/2, built/2]).
% calculus_templates.pl
:- use_module(library(hash_consing), []).
:- hash_consing:rewritten([apply(lambda(_), _), lambda(_), variable(_)]).
```

and include it in every file that uses these terms:

```prolog
:- module(steps, [step/2, built/2]).
:- include(calculus_templates).

step(apply(lambda(Body), Argument), beta(Body, Argument)).

built(Function, Applied) :-
Applied = apply(Function, variable(0)).
```

```prolog
:- module(redexes, [is_redex/1]).
:- include(calculus_templates).

is_redex(apply(lambda(_), _)).
```

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
turn. The included directive opts in the file that includes it, so both
modules rewrite the same terms: when `built/2` in `steps` applies a lambda,
the application it makes is the Id that the head of `is_redex/1` in
`redexes` expects.

**Warning:** the rewrite is per file. A file rewrites only the terms its own
directive names, and the library checks nothing between files. A file that
receives interned terms without including the directive keeps plain terms
in its clauses, so its heads never unify with the Ids: the call fails,
silently, with no error. Write the directive once and include it everywhere.

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
Expand All @@ -49,10 +76,18 @@ 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):
[`test/hash_consing_fixtures/patterns_templates.pl`](test/hash_consing_fixtures/patterns_templates.pl):

```prolog
:- use_module(library(hash_consing), []).
:- hash_consing:rewritten([app(abs(_), _), app(app(*, _), _), app(_, ref(_)), abs(_), ref(_)]).
```

and [`test/hash_consing_fixtures/patterns.pl`](test/hash_consing_fixtures/patterns.pl),
which includes it:

```prolog
:- include(patterns_templates).

% Must intern, every instance taking the first template: the shape `abs/1`
% is written into the head.
Expand Down
2 changes: 1 addition & 1 deletion pack.pl
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
name(hash_consing).
version('0.2.0').
version('0.2.1').
title('Hash-consed terms by clause rewriting').
keywords([interning, 'hash-consing', trie, term_expansion]).
author('Yang, Bo', 'yang-bo@yang-bo.com').
Expand Down
Loading
Loading