fix codegen bug (marking terms in rules too eagerly)

This commit is contained in:
Mark Thom
2017-02-24 17:54:33 -07:00
parent 2fccbb09c6
commit f47a161376
2 changed files with 50 additions and 11 deletions

View File

@@ -57,15 +57,15 @@ no
l2> p(f(X), h(Y, f(a)), Y).
l2> ?- p(Z, h(Z, W), f(W)).
yes
W = f(a)
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
Y = t
X = q
Y = t
l2> ?- p(q, t).
yes
l2> ?- p(t, q).
@@ -80,27 +80,63 @@ 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).
l2> ?- p(X, Y).
yes
X = _0
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
X = s
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> quit
```
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 uniscore.
## Occurs check
There's no occurs check, but there probably should be. Currently,
attempting to unify on a cyclic term causes an infinite loop:
There's no occurs check, but there soon will be. Currently, attempting
unification on a cyclic term causes an infinite loop:
```
l2> p(W, W).

View File

@@ -237,7 +237,7 @@ impl<'a> TermMarker<'a> {
}
fn advance(&mut self, term: &'a Term) {
self.arg_c = 1;
self.arg_c = 1;
self.temp_c = term.subterms() + 1;
}
}
@@ -329,8 +329,6 @@ impl<'a> CodeGenerator<'a> {
let iter = Target::iter(term);
let mut target = Vec::new();
self.marker.advance(term);
for term in iter {
match term {
TermRef::Atom(lvl, term, atom) =>
@@ -411,13 +409,18 @@ impl<'a> CodeGenerator<'a> {
let mut body = Vec::new();
self.marker.advance(p0);
body.push(Line::Control(ControlInstruction::Allocate(perm_vars)));
body.push(Line::Fact(self.compile_target(p0)));
body.append(&mut self.compile_query(p1));
body = clauses.iter()
.map(|ref term| self.compile_query(term))
.map(|ref term| {
self.marker.advance(term);
self.compile_query(term)
})
.fold(body, |mut body, ref mut cqs| {
body.append(cqs);
body