fix codegen bug (marking terms in rules too eagerly)

diff --git a/README.md b/README.md
index 789e7e680ccd3f18934363f66ec3b016e93f6d68..899658adf57da815947615880bac7f28fdbfceef 100644 (file)
--- a/README.md
+++ b/README.md
@@ -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
+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).

diff --git a/src/l2/codegen.rs b/src/l2/codegen.rs
index 71ff300f645acd75669597938ab42a17a35df515..1ffb2e068b59f9c3a28dda7df35a9145a6cdedad 100644 (file)
--- a/src/l2/codegen.rs
+++ b/src/l2/codegen.rs
@@ -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