transition to l3
This commit is contained in:
161
README.md
161
README.md
@@ -8,135 +8,56 @@ pure Prolog.
|
||||
|
||||
## Progress
|
||||
|
||||
The language L2 is implemented as a simple REPL. It supports
|
||||
unification on queries without backtracking, where rules and facts are
|
||||
limited to a single name/arity pairing, in the familiar Prolog
|
||||
syntax. No data types apart from atoms are currently supported.
|
||||
The language L3 is implemented as a simple REPL. L3 is pure Prolog --
|
||||
Prolog without cuts, meta- or extra-logical operators, or side effects
|
||||
of any kind. No data types apart from atoms are currently supported.
|
||||
|
||||
An example of the level of interaction currently supported is:
|
||||
## Tutorial
|
||||
To enter a multi-clause predicate, the brackets ":{" and "}:" are used
|
||||
as delimiters. They must be entirely contained with their own lines.
|
||||
|
||||
For example,
|
||||
```
|
||||
l2> p(Z, Z).
|
||||
l2> ?- p(Z, Z).
|
||||
l3> :{
|
||||
p(f(f(X)), h(W), Y) :- g(W), h(W), f(X).
|
||||
p(X, Y, Z) :- h(Y), z(Z).
|
||||
}:
|
||||
l3> :{
|
||||
h(x).
|
||||
h(y).
|
||||
h(z).
|
||||
}:
|
||||
```
|
||||
|
||||
Single clause predicates can entered without brackets, as in
|
||||
```
|
||||
l3> p(X) :- q(X).
|
||||
l3> f(s).
|
||||
l3> z(Z).
|
||||
```
|
||||
|
||||
Queries are issued as
|
||||
```
|
||||
l3> ?- p(X, Y, Z).
|
||||
```
|
||||
|
||||
Given the above work, the result of the query will be
|
||||
```
|
||||
l3> ?- p(X, Y, Z).
|
||||
yes
|
||||
Z = _0
|
||||
l2> ?- p(Z, z).
|
||||
yes
|
||||
Z = z
|
||||
l2> ?- p(Z, w).
|
||||
yes
|
||||
Z = w
|
||||
l2> clouds(are, nice).
|
||||
l2> ?- p(z, w).
|
||||
no
|
||||
l2> ?- p(w, w).
|
||||
yes
|
||||
l2> ?- clouds(Z, Z).
|
||||
no
|
||||
l2> ?- clouds(are, W).
|
||||
yes
|
||||
W = nice
|
||||
l2> ?- clouds(W, nice).
|
||||
yes
|
||||
W = are
|
||||
l2> ?- p(Z, h(Z, W), f(W)).
|
||||
no
|
||||
l2> p(Z, h(Z, W), f(W)).
|
||||
l2> ?- p(z, h(z, z), f(w)).
|
||||
no
|
||||
l2> ?- p(z, h(z, w), f(w)).
|
||||
yes
|
||||
l2> ?- p(z, h(z, W), f(w)).
|
||||
yes
|
||||
W = w
|
||||
l2> ?- p(Z, h(Z, w), f(Z)).
|
||||
yes
|
||||
Z = w
|
||||
l2> ?- p(z, h(Z, w), f(Z)).
|
||||
no
|
||||
l2> p(f(X), h(Y, f(a)), Y).
|
||||
l2> ?- p(Z, h(Z, W), f(W)).
|
||||
yes
|
||||
Z = f(f(a))
|
||||
W = f(a)
|
||||
l2> p(X, Y) :- q(X, Z), r(Z, Y).
|
||||
l2> q(q, s).
|
||||
l2> r(s, t).
|
||||
l2> ?- p(X, Y).
|
||||
yes
|
||||
X = q
|
||||
Y = t
|
||||
l2> ?- p(q, t).
|
||||
yes
|
||||
l2> ?- p(t, q).
|
||||
no
|
||||
l2> ?- p(q, T).
|
||||
yes
|
||||
T = t
|
||||
l2> ?- p(Q, t).
|
||||
yes
|
||||
Q = q
|
||||
l2> ?- p(t, t).
|
||||
no
|
||||
l2> p(X, Y) :- q(f(f(X)), R), r(S, T).
|
||||
l2> q(f(f(X)), r).
|
||||
l2> ?- p(X, Y).
|
||||
yes
|
||||
Y = _1
|
||||
X = _0
|
||||
l2> q(f(f(x)), r).
|
||||
l2> ?- p(X, Y).
|
||||
yes
|
||||
Y = _1
|
||||
X = x
|
||||
l2> p(X, Y) :- q(X, Y), r(X, Y).
|
||||
l2> q(s, t).
|
||||
l2> r(X, Y) :- r(a).
|
||||
l2> r(a).
|
||||
l2> ?- p(X, Y).
|
||||
yes
|
||||
Y = t
|
||||
X = s
|
||||
l2> ?- p(t, S).
|
||||
no
|
||||
l2> ?- p(t, s).
|
||||
no
|
||||
l2> ?- p(s, T).
|
||||
yes
|
||||
T = t
|
||||
l2> ?- p(S, t).
|
||||
yes
|
||||
S = s
|
||||
l2> p(f(f(a), g(b), X), g(b), h) :- q(X, Y).
|
||||
l2> q(X, Y).
|
||||
l2> ?- p(f(X, Y, Z), g(b), h).
|
||||
yes
|
||||
Z = _4
|
||||
X = f(a)
|
||||
Y = g(b)
|
||||
l2> ?- p(f(X, g(Y), c), g(Z), X).
|
||||
no
|
||||
l2> ?- p(f(X, g(Y), c), g(Z), h).
|
||||
yes
|
||||
Z = b
|
||||
Y = b
|
||||
X = f(a)
|
||||
l2> ?- p(Z, Y, X).
|
||||
yes
|
||||
X = h
|
||||
Z = f(f(a), g(b), _7)
|
||||
Y = g(b)
|
||||
l2> ?- p(f(X, Y, Z), Y, h).
|
||||
yes
|
||||
X = f(a)
|
||||
Z = _4
|
||||
Y = g(b)
|
||||
l2> quit
|
||||
Y = x
|
||||
Z = _2
|
||||
Press ; to continue or A to abort.
|
||||
```
|
||||
|
||||
Pressing ; will backtrack through other possible answers, if any exist.
|
||||
Pressing A will abort the search and return to the prompt.
|
||||
|
||||
Note that the values of variables belonging to successful queries are
|
||||
printed out, on one line each. Uninstantiated variables are denoted by
|
||||
a number preceded by an underscore.
|
||||
a number preceded by an underscore (X = _0 is an example in the
|
||||
above).
|
||||
|
||||
## Occurs check
|
||||
|
||||
|
||||
Reference in New Issue
Block a user