class Prolog with rewriting and eval (old) [1002862]

!752

static final class Prolog {
  boolean upperCaseVariables = false; // true for SNL, false for NL
  long varCount;
  boolean showStuff;
  new L<Entry> stack;
  Trail sofar = null;
  new L<Clause> program;
  new L<L<Clause>> programByArity;
  long steps;
  new L<Native> natives;
  L<S> log;
  int maxLogSize = 1000; // lines
  int maxLevel = 10000; // max stack size
  int timeLimit = 20; // 20 seconds
  long startTime;
  boolean allowEval = true;
  
  // stats
  int maxLevelSeen; // maximum stack level reached during computation
  long topUnifications, exceptions;

  static interface Native {
    public boolean yo(Prolog p, Lisp term);
  }

  boolean headeq(S a, S b) {
    ret isQuoted (a) ? eq(a, b) : eqic(a, b);
  }
  
  static class Var extends Lisp {
    long id;
    Lisp instance;
    
    *(S name) {
      super(name);
      instance = this;
    }
    
    *(long id) {
      super("___");
      this.id = id;
      instance = this;
    }
    
    void reset() { instance = this; }
    
    public String toString() {
      if (instance != this)
        ret instance.toString();
      ret isUserVar() ? getName() : "_" + id;
    }
    
    boolean isUserVar() {
      ret id == 0;
    }
    
    S getName() {
      ret head;
    }
    
    Lisp getValue() {
      Lisp l = instance;
      while (l instanceof Var) {
        Var v = cast l;
        if (v.instance == v)
          ret v;
        l = v.instance;
      }
      ret l;
    }
  }
  
  class Clause {
    Lisp head;
    
    // Either body or nat will be set (or none)
    Native nat;
    Goal body;
    
    *(Lisp *head, Native *nat) {}
    *(Lisp *head, Goal *body) {}
    *(Lisp *head, Goal *body, Native *nat) {}
    *(Lisp *head) {}
    
    Clause copy() {
      ret new Clause(Prolog.this.copy(head), body == null ? null : body.copy(), nat);
    }
    
    public String toString() {
      //ret head + " :- " + (body == null ? "true" : body);
      ret nat != null ? head + " :- native" :
        (body == null ? head.toString() : head + " :- " + body);
    }
  }
  
  class Trail {
    Var tcar;
    Trail tcdr;
    
    *(Var *tcar, Trail *tcdr) {}
  }
  
  Trail Trail_Note() { return sofar; }
  void Trail_Push(Var x) { sofar = new Trail(x, sofar); }
  void Trail_Undo(Trail whereto) {
    for (; sofar != whereto; sofar = sofar.tcdr)
      sofar.tcar.reset();
  }
  
  static class TermVarMapping {
    new L<Var> vars;
    
    *(L<Var> *vars) {}
    *(Var... vars) { this.vars.addAll(asList(vars)); }
    
    void showanswer() {
      print("TRUE.");
      for (Var v : vars)
        print("  " + v.getName() + " = " + v);
    }
  }
      
  class Goal {
    Lisp car;
    Goal cdr;
    
    *(Lisp *car, Goal *cdr) {}
    *(Lisp *car) {}
    
    public String toString() {
      ret cdr == null ? car.toString() : car + "; " + cdr;
    }
    
    Goal copy() {
      return new Goal(Prolog.this.copy(car),
        cdr == null ? null : cdr.copy());
    }
    
    Goal append(Goal l) {
      return new Goal(car, cdr == null ? l : cdr.append(l));
    }
    
  } // class Goal
  
  boolean unifyOrRollback(Lisp a, Lisp b) {
    Trail t = Trail_Note();
    if (unify(a, b)) ret true;
    Trail_Undo(t);
    ret false;
  }
  
  boolean unify(Lisp thiz, Lisp t) {
    if (thiz == null) fail("thiz=null");
    if (t == null) fail("t=null");
    
    if (thiz instanceof Var) { // TermVar::unify
      Var v = cast thiz;
      if (v.instance != v)
        return unify(v.instance, t);
      Trail_Push(v);
      v.instance = t;
      return true;
    }
    
    // TermCons::unify
    return unify2(t, thiz);
  }
  
  boolean unify2(Lisp thiz, Lisp t) { 
    if (thiz instanceof Var)
      return unify(thiz, t);
   
    int arity = thiz.size();
    if (!headeq(thiz.head, t.head) || arity != t.size())
      return false;
    for (int i = 0; i < arity; i++)
      if (!unify(thiz.get(i), t.get(i)))
        return false;
    return true;
  }
  
  Lisp copy(Lisp thiz) {
    if (thiz instanceof Var) {
      Var v = cast thiz;
      if (v.instance == v) {
        Trail_Push(v);
        v.instance = newVar();
      }
      return v.instance;
    }
    
    // copy2 (copy non-var)
    Lisp l = new Lisp(thiz.head);
    for (Lisp arg : thiz)
      l.add(copy(arg));
    ret l;
  }
  
  Var newVar() {
    ret new Var(++varCount);
  }
  
  Var newVar(S name) {
    ret new Var(name);
  }
  
  Clause clause(Lisp head, Goal body) {
    ret prologify(new Clause(head, body));
  }
  
  // primarey processor for freshly parsed rules
  
  Clause clause(Lisp rule) {
    if (allowEval)
      rule = new EvalTransform().evalTransformRule(rule);
      
    L<Lisp> ops = snlSplitOps(rule);
    /*if (showStuff)
      log("clause(Lisp): " + rule + " => " + structure(ops)); */
      
    if (!empty(ops) && last(ops).is("say *"))
      ops.set(l(ops)-1, lisp("then *", lisp("[]", "say", last(ops).get(0))));

    if (!empty(ops) && last(ops).is("then *")) {
      Lisp head = last(ops).get(0);
      Goal goal = null;
      
      // TODO: check the actual words (if/and/...)
      for (int i = l(ops)-2; i >= 0; i--)
        goal = new Goal(ops.get(i).get(0), goal);
        
      ret clause(head, goal);
    } else
      ret clause(rule, (Lisp) null);
  }
  
  Clause clause(Lisp head, Lisp body) {
    ret clause(head, body == null ? null : new Goal(body));
  }
  
  Lisp prologify(Lisp term) {
    ret prologify(term, new HashMap);
  }
  
  Clause prologify(Clause c) {
    new HashMap vars;
    c = new Clause(
      prologify(c.head, vars),
      prologify(c.body, vars),
      c.nat);
    /*if (showStuff)
      log("Clause made: " + structure_seen(c));*/
    ret c;
  }
  
  Goal prologify(Goal goal, Map<S, Var> vars) {
    if (goal == null) ret null;
    ret new Goal(
      prologify(goal.car, vars),
      prologify(goal.cdr, vars));
  }
  
  boolean isVar(Lisp term) {
    ret upperCaseVariables ? snlIsVar(term) : nlIsVar(term);
  }
  
  Lisp prologify(Lisp term, Map<S, Var> vars) {
    if (term == null) ret null;
    if (isVar(term)) {
      Var v = vars.get(term.head);
      if (v == null)
        vars.put(term.head, v = newVar(term.head));
      ret v;
    } else {
      Lisp l = new Lisp(term.head);
      for (Lisp arg : term)
        l.add(prologify(arg, vars));
      ret l;
    }
  }
  
  L<Var> findVars(Goal g) {
    new IdentityHashMap<Var, Boolean> map;
    while (g != null) {
      findVars(g.car, map);
      g = g.cdr;
    }
    ret asList(map.keySet());
  }
  
  L<Var> findVars(Lisp term) {
    new IdentityHashMap<Var, Boolean> map;
    findVars(term, map);
    ret asList(map.keySet());
  }
  
  void findVars(Lisp term, IdentityHashMap<Var, Boolean> map) {
    if (term instanceof Var)
      map.put((Var) term, Boolean.TRUE);
    else
      for (Lisp arg : term)
        findVars(arg, map);
  }
  
  static Map<S, Var> makeVarMap(L<Var> vars) {
    new HashMap<S, Var> map;
    for (Var v : vars)
      map.put(v.getName(), v);
    ret map;
  }
  
  new L<Clause> emptyProgram;
  
  // Executor stack entry
  class Entry {
    Goal goal;
    L<Clause> program; // full program or filtered by arity
    int programIdx = -1; // -1 is natives
    Trail trail;
    boolean trailSet;

    *(Goal *goal) {
      Lisp car = resolve1(goal.car);
      if (car instanceof Var) {
        if (showStuff)
          log("Weird: Goal is variable: " + car);
        program = Prolog.this.program;
      } else {
        int arity = car.size();
        if (showStuff)
          log("Goal arity " + arity + ": " + car);
        program = arity >= l(programByArity) ? emptyProgram : programByArity.get(arity);
      }
    }
  }
  
  void start(Lisp goal) {
    start(new Goal(prologify(goal)));
  }
  
  // warning: doesn't prologify the goal
  void start(Goal goal) {
    if (showStuff)
      log("Starting on goal: " + structure_seen(goal));
    steps = 0;
    stack = new L;
    Trail_Undo(null);
    stackAdd(new Entry(goal));
    startTime = now();
  }
  
  void log(S s) {
    if (log != null) {
      if (l(log) == maxLogSize)
        log.add("[Log overflow]");
      else if (l(log) < maxLogSize)
        log.add(s);
    } else if (showStuff)
      print("prolog: " + s);
  }
    
  int level() {
    ret l(stack)-1;
  }
  
  boolean done() {
    boolean result = empty(stack);
    if (showStuff && result)
      log("Done with goal!");
    ret result;
  }

  boolean gnext(Goal g) {  
    Goal gdash = g.cdr;
    if (gdash == null) {
      if (showStuff)
        log("gnext true");
      ret true;
    } else {
      stackAdd(new Entry(gdash));
      ret false;
    }
  }
  
  void stackPop() {
    Entry e = popLast(stack);
    if (e.trailSet)
      Trail_Undo(e.trail);
  }
  
  void backToCutPoint(int n) {
    if (showStuff)
      log("back to cut point " + n);
    while (l(stack) >= n) {
      if (showStuff)
        log("cut: dropping " + structure(last(stack).goal));
      stackPop();
    }
  }

  boolean step() {
    if (done()) fail("done!"); // safety
    if (now() >= startTime+timeLimit*1000)
      fail("time limit reached: " + timeLimit + " s");
    
    ++steps;
    Entry e = last(stack);
    
    if (e.trailSet) {
      Trail_Undo(e.trail);
      e.trailSet = false;
    }
    
    e.trail = Trail_Note();
    e.trailSet = true;
    
    // cut operator - suceeds first time
    if (e.goal.car.is("!", 1)) {
      if (showStuff)
        log("cut " + e.programIdx + ". " + structure(e.goal));
      if (e.programIdx == -1) {
        ++e.programIdx;
        ret gnext(e.goal);
      } else if (e.programIdx == 0) {
        ++e.programIdx;
        // fails 2nd time and cuts
        //e.goal.car.head = "false"; // super-hack :D
        backToCutPoint(parseInt(e.goal.car.get(0).raw()));
        ret false;
      } else {
        stackPop();
        ret false;
      }
    }

    if (e.programIdx >= l(e.program)) { // program loop ends
      removeLast(stack);
      ret false;
    }
      
    if (e.programIdx == -1) {
      ++e.programIdx;
        
      // try native functions
      if (goNative(e.goal.car)) {
        if (showStuff)
          log(indent(level()) + "native!");
          
        ret gnext(e.goal);
      }
      
      ret false;
    }
      
    // now in program loop
    
    Clause c = e.program.get(e.programIdx).copy();
    ++e.programIdx;
    Trail_Undo(e.trail);
    S text = null;
    if (showStuff)
      text = "  Goal: " + e.goal + ". Got clause: " + c;
    ++topUnifications;
    if (unify(e.goal.car, c.head)) {
      if (showStuff) {
        log(indent(level()) + text);
        log(indent(level()) + "  Clause unifies to: " + c);
      }
      Goal gdash;
      if (c.nat != null) {
        if (showStuff)
          log(indent(level()) + " Clause is native.");
        if (!c.nat.yo(this, c.head)) {
          if (showStuff)
            log(indent(level()) + "Native clause fails");
          ret false;
        }
        gdash = e.goal.cdr;
      } else
        gdash = c.body == null ? e.goal.cdr : resolveCut(c.body).append(e.goal.cdr);
      if (showStuff)
        log(indent(level()) + "  gdash: " + gdash);
        
      if (gdash == null) {
        if (showStuff)
          log("SUCCESS!");
        ret true;
      } else {
        Entry e2 = new Entry(gdash);
        if (showStuff)
          log(indent(level()) + "New goal: " + gdash);
        stackAdd(e2);
        ret false;
      }
    } /*else
      if (showStuff)
        log(indent(level()) + "No match for clause.");*/
        
    ret false;
  }
  
  // resolve cut in clause body
  Goal resolveCut(Goal g) {
    if (g.car.is("!", 0))
      ret fixCut(g);
    if (g.cdr == null)
      ret g;
    ret new Goal(g.car, resolveCut(g.cdr));
  }
  
  // note stack length in cut
  Goal fixCut(Goal g) {
    ret new Goal(lisp("!", lstr(stack)), g.cdr); // max. one cut per clause
  }
  
  void stackAdd(Entry e) {
    stack.add(e);
    int n = l(stack);
    if (n > maxLevel) fail("Maximum stack level reached: " + n);
    if (n > maxLevelSeen) maxLevelSeen = n;
  }
  
  void addClause(S text) {
    addClause(nlParse(text));
  }
  
  void addClause(Lisp c) {
    addClause(clause(c));
  }
  
  void addClause(Clause c) {
    program.add(c);
    int arity = c.head.size();
    while (arity >= l(programByArity))
      programByArity.add(new L);
    programByArity.get(arity).add(c);
  }
  
  boolean canSolve(Lisp goal) {
    ret canSolve(new Goal(prologify(goal)));
  }
  
  boolean canSolve(Goal goal) {
    start(goal);
    while (!done())
      if (step())
        ret true;
    ret false;
  }
  
  // return variable map or null if unsolved
  Map<S, Lisp> solve(Lisp goal) {
    start(new Goal(prologify(goal)));
    ret nextSolution();
  }
  
  Map<S, Lisp> solve(S text) {
    ret solve(nlParse(text));
  }
  
  Map<S, Lisp> getUserVarMap() {
    Goal g = stack.get(0).goal;
    new HashMap<S, Lisp> map;
    for (Var v : findVars(g))
      if (v.isUserVar())
        map.put(v.getName(), resolve(v));
    ret map;
  }
  
  Map<S, Lisp> nextSolution() {
    if (showStuff)
      log("nextSolution");
    int n = 0;
    while (!done()) {
      ++n;
      if (step()) {
        if (showStuff)
          log("  solution found in step " + n);
        ret getUserVarMap();
      }
    }
    if (showStuff)
      log("No solution");
    ret null;
  }
  
  void addTheory(S text) {
    for (Clause c : parseProgram(text))
      addClause(c);
  }
    
  L<Clause> parseProgram(S text) {
    new L<Clause> l;
    Lisp tree = nlParse(text);
    if (nlIsMultipleStatements(text))
      for (Lisp part : tree)
        l.add(clause(part));
    else
      l.add(clause(tree));
    ret l;
  }
  
  boolean goNative(Lisp term) {
    term = resolve(term);
    
    for (Native n : natives) {
      Trail t = Trail_Note();
      boolean result;
      try {
        result = n.yo(this, term);
      } catch (Exception e) {
        Trail_Undo(t);
        continue;
      }
      if (!result) {
        Trail_Undo(t);
        continue;
      }
      ret true;
    }

    if (term.is("nativeTest", 0))
      ret true;
      
    if (term.is("isQuoted", 1)) {
      Lisp x = term.get(0);
      ret !(x instanceof Var) && x.isLeaf() && isQuoted(x.head);
    }
      
    ret false;
  }
  
  // Resolve top-level only
  Lisp resolve1(Lisp term) {
    if (term instanceof Var)
      ret ((Var) term).getValue();
    ret term;
  }
  
  // resolve all variables
  Lisp resolve(Lisp term) {
    term = resolve1(term);
      
    // smart recurse
    for (int i = 0; i < term.size(); i++) {
      Lisp l = term.get(i);
      Lisp r = resolve(l);
      if (l != r) {
        Lisp x = new Lisp(term.head);
        for (int j = 0; j < i; j++)
          x.add(term.get(j));
        x.add(r);
        for (i++; i < term.size(); i++)
          x.add(resolve(term.get(i)));
        ret x;
      }
    }
    
    ret term;
  }
  
  // looks for a bodyless rule in the program that matches the term
   // todo: eqic
  boolean containsStatement(Lisp term) {
    for (Clause c : program)
      if (c.body == null && c.nat == null && eq(c.head, term))
        ret true;
    ret false;
  }
  
  // closed == contains no variables
  boolean isClosedTerm(Lisp term) {
    if (term instanceof Var)
      ret false;
    else
      for (Lisp arg : term)
        if (!isClosedTerm(arg))
          ret false;
    ret true;
  }
  
  void addNative(Native n) {
    if (n instanceof BaseNative)
      addNative(((BaseNative) n).pat, n);
    else
      natives.add(n);
  }
  
  void addNatives(Native... l) {
    for (Native n : l)
      addNative(n);
  }
    
  void addNatives(L<Native> l) {
    for (Native n : l)
      addNative(n);
  }
  
  void addNative(S text, Native n) {
    addClause(prologify(new Clause(nlParse(text), n)));
  }
  
  L<Lisp> getStackTerms() {
    new L<Lisp> l;
    for (Entry e : stack)
      l.add(e.goal.car);
    ret l;
  }
  
  void logOn() {
    log = new L;
    showStuff = true;
  }

  static abstract class BaseNative implements Native {
    S pat;
    Prolog p;
    Map<S, Lisp> m;
    
    *(S *pat) {}
    
    abstract boolean yo();
    
    public boolean yo(Prolog p, Lisp term) {
      m = new HashMap;
      this.p = p;
      try {
        ret nlMatch(pat, p.resolve(term), m) && yo();
      } catch (Exception e) {
        ++p.exceptions;
        if (p.showStuff)
          p.log("Exception in native: " + e);
        ret false;
      } finally {
        this.p = null;
      }
    }
    
    boolean unify(S var, Lisp term) {
      Lisp v = m.get(var);
      if (v == null)
        fail("Variable " + var + " not found");
      ret p.unify(v, term);
    }
  } // BaseNative
  
  // Prolog constructor
  *() {
    addClause(lisp("true"));
  }
  
  L<Lisp> rewriteWith(L<Clause> rewriteTheory) {
    new L<Lisp> result;
    
    for (Prolog.Clause clause : rewriteTheory) {
      if (clause.body == null) continue; // need conditions to rewrite anything
      
      // todo: trail
      Prolog.Clause c = clause.copy();
      start(c.body);
      while (!done()) {
        if (step()) {
          Lisp term = resolve(c.head);
          if (!isClosedTerm(term)) {
            print("Not a closed term, skipping: " + term);
            continue;
          }
          
          if (containsStatement(term)) {
            print("Statement exists, skipping: " + term);
            continue;
          }
          
          if (result.contains(term))
            continue;
            
          print("Found new statement: " + term);
          result.add(term);
        }
      }
    }
    
    ret result;
  }
} // class Prolog

Travelled to 13 computer(s): aoiabmzegqzx, bhatertpkbcr, cbybwowwnfue, cfunsshuasjs, gwrvuhgaqvyk, ishqpsrjomds, lpdgvwnxivlt, mqqgnosmbjvj, pyentgdyhuwx, pzhvpgtvlbxg, tslmcundralx, tvejysmllsmz, vouqrxazstgt

Snippet ID:	#1002862
Snippet name:	class Prolog with rewriting and eval (old)
Eternal ID of this version:	#1002862/1
Text MD5:	bd68ccfd36dae3f9add95ea97749bc78
Author:	stefan
Category:	javax
Type:	JavaX fragment (include)
Public (visible to everyone):	Yes
Archived (hidden from active list):	No
Created/modified:	2016-03-10 00:40:12
Source code size:	18351 bytes / 787 lines
Pitched / IR pitched:	No / No
Views / Downloads:	606 / 558
Referenced in:	[show references]

< > BotCompany Repo | #1002862 // class Prolog with rewriting and eval (old)

JavaX fragment (include)

Author comment

1	!752
2
3	static final class Prolog {
4	boolean upperCaseVariables = false; // true for SNL, false for NL
5	long varCount;
6	boolean showStuff;
7	new L<Entry> stack;
8	Trail sofar = null;
9	new L<Clause> program;
10	new L<L<Clause>> programByArity;
11	long steps;
12	new L<Native> natives;
13	L<S> log;
14	int maxLogSize = 1000; // lines
15	int maxLevel = 10000; // max stack size
16	int timeLimit = 20; // 20 seconds
17	long startTime;
18	boolean allowEval = true;
19
20	// stats
21	int maxLevelSeen; // maximum stack level reached during computation
22	long topUnifications, exceptions;
23
24	static interface Native {
25	public boolean yo(Prolog p, Lisp term);
26	}
27
28	boolean headeq(S a, S b) {
29	ret isQuoted (a) ? eq(a, b) : eqic(a, b);
30	}
31
32	static class Var extends Lisp {
33	long id;
34	Lisp instance;
35
36	*(S name) {
37	super(name);
38	instance = this;
39	}
40
41	*(long id) {
42	super("___");
43	this.id = id;
44	instance = this;
45	}
46
47	void reset() { instance = this; }
48
49	public String toString() {
50	if (instance != this)
51	ret instance.toString();
52	ret isUserVar() ? getName() : "_" + id;
53	}
54
55	boolean isUserVar() {
56	ret id == 0;
57	}
58
59	S getName() {
60	ret head;
61	}
62
63	Lisp getValue() {
64	Lisp l = instance;
65	while (l instanceof Var) {
66	Var v = cast l;
67	if (v.instance == v)
68	ret v;
69	l = v.instance;
70	}
71	ret l;
72	}
73	}
74
75	class Clause {
76	Lisp head;
77
78	// Either body or nat will be set (or none)
79	Native nat;
80	Goal body;
81
82	(Lisp head, Native *nat) {}
83	(Lisp head, Goal *body) {}
84	(Lisp head, Goal body, Native nat) {}
85	(Lisp head) {}
86
87	Clause copy() {
88	ret new Clause(Prolog.this.copy(head), body == null ? null : body.copy(), nat);
89	}
90
91	public String toString() {
92	//ret head + " :- " + (body == null ? "true" : body);
93	ret nat != null ? head + " :- native" :
94	(body == null ? head.toString() : head + " :- " + body);
95	}
96	}
97
98	class Trail {
99	Var tcar;
100	Trail tcdr;
101
102	(Var tcar, Trail *tcdr) {}
103	}
104
105	Trail Trail_Note() { return sofar; }
106	void Trail_Push(Var x) { sofar = new Trail(x, sofar); }
107	void Trail_Undo(Trail whereto) {
108	for (; sofar != whereto; sofar = sofar.tcdr)
109	sofar.tcar.reset();
110	}
111
112	static class TermVarMapping {
113	new L<Var> vars;
114
115	(L<Var> vars) {}
116	*(Var... vars) { this.vars.addAll(asList(vars)); }
117
118	void showanswer() {
119	print("TRUE.");
120	for (Var v : vars)
121	print(" " + v.getName() + " = " + v);
122	}
123	}
124
125	class Goal {
126	Lisp car;
127	Goal cdr;
128
129	(Lisp car, Goal *cdr) {}
130	(Lisp car) {}
131
132	public String toString() {
133	ret cdr == null ? car.toString() : car + "; " + cdr;
134	}
135
136	Goal copy() {
137	return new Goal(Prolog.this.copy(car),
138	cdr == null ? null : cdr.copy());
139	}
140
141	Goal append(Goal l) {
142	return new Goal(car, cdr == null ? l : cdr.append(l));
143	}
144
145	} // class Goal
146
147	boolean unifyOrRollback(Lisp a, Lisp b) {
148	Trail t = Trail_Note();
149	if (unify(a, b)) ret true;
150	Trail_Undo(t);
151	ret false;
152	}
153
154	boolean unify(Lisp thiz, Lisp t) {
155	if (thiz == null) fail("thiz=null");
156	if (t == null) fail("t=null");
157
158	if (thiz instanceof Var) { // TermVar::unify
159	Var v = cast thiz;
160	if (v.instance != v)
161	return unify(v.instance, t);
162	Trail_Push(v);
163	v.instance = t;
164	return true;
165	}
166
167	// TermCons::unify
168	return unify2(t, thiz);
169	}
170
171	boolean unify2(Lisp thiz, Lisp t) {
172	if (thiz instanceof Var)
173	return unify(thiz, t);
174
175	int arity = thiz.size();
176	if (!headeq(thiz.head, t.head) \|\| arity != t.size())
177	return false;
178	for (int i = 0; i < arity; i++)
179	if (!unify(thiz.get(i), t.get(i)))
180	return false;
181	return true;
182	}
183
184	Lisp copy(Lisp thiz) {
185	if (thiz instanceof Var) {
186	Var v = cast thiz;
187	if (v.instance == v) {
188	Trail_Push(v);
189	v.instance = newVar();
190	}
191	return v.instance;
192	}
193
194	// copy2 (copy non-var)
195	Lisp l = new Lisp(thiz.head);
196	for (Lisp arg : thiz)
197	l.add(copy(arg));
198	ret l;
199	}
200
201	Var newVar() {
202	ret new Var(++varCount);
203	}
204
205	Var newVar(S name) {
206	ret new Var(name);
207	}
208
209	Clause clause(Lisp head, Goal body) {
210	ret prologify(new Clause(head, body));
211	}
212
213	// primarey processor for freshly parsed rules
214
215	Clause clause(Lisp rule) {
216	if (allowEval)
217	rule = new EvalTransform().evalTransformRule(rule);
218
219	L<Lisp> ops = snlSplitOps(rule);
220	/*if (showStuff)
221	log("clause(Lisp): " + rule + " => " + structure(ops)); */
222
223	if (!empty(ops) && last(ops).is("say *"))
224	ops.set(l(ops)-1, lisp("then *", lisp("[]", "say", last(ops).get(0))));
225
226	if (!empty(ops) && last(ops).is("then *")) {
227	Lisp head = last(ops).get(0);
228	Goal goal = null;
229
230	// TODO: check the actual words (if/and/...)
231	for (int i = l(ops)-2; i >= 0; i--)
232	goal = new Goal(ops.get(i).get(0), goal);
233
234	ret clause(head, goal);
235	} else
236	ret clause(rule, (Lisp) null);
237	}
238
239	Clause clause(Lisp head, Lisp body) {
240	ret clause(head, body == null ? null : new Goal(body));
241	}
242
243	Lisp prologify(Lisp term) {
244	ret prologify(term, new HashMap);
245	}
246
247	Clause prologify(Clause c) {
248	new HashMap vars;
249	c = new Clause(
250	prologify(c.head, vars),
251	prologify(c.body, vars),
252	c.nat);
253	/*if (showStuff)
254	log("Clause made: " + structure_seen(c));*/
255	ret c;
256	}
257
258	Goal prologify(Goal goal, Map<S, Var> vars) {
259	if (goal == null) ret null;
260	ret new Goal(
261	prologify(goal.car, vars),
262	prologify(goal.cdr, vars));
263	}
264
265	boolean isVar(Lisp term) {
266	ret upperCaseVariables ? snlIsVar(term) : nlIsVar(term);
267	}
268
269	Lisp prologify(Lisp term, Map<S, Var> vars) {
270	if (term == null) ret null;
271	if (isVar(term)) {
272	Var v = vars.get(term.head);
273	if (v == null)
274	vars.put(term.head, v = newVar(term.head));
275	ret v;
276	} else {
277	Lisp l = new Lisp(term.head);
278	for (Lisp arg : term)
279	l.add(prologify(arg, vars));
280	ret l;
281	}
282	}
283
284	L<Var> findVars(Goal g) {
285	new IdentityHashMap<Var, Boolean> map;
286	while (g != null) {
287	findVars(g.car, map);
288	g = g.cdr;
289	}
290	ret asList(map.keySet());
291	}
292
293	L<Var> findVars(Lisp term) {
294	new IdentityHashMap<Var, Boolean> map;
295	findVars(term, map);
296	ret asList(map.keySet());
297	}
298
299	void findVars(Lisp term, IdentityHashMap<Var, Boolean> map) {
300	if (term instanceof Var)
301	map.put((Var) term, Boolean.TRUE);
302	else
303	for (Lisp arg : term)
304	findVars(arg, map);
305	}
306
307	static Map<S, Var> makeVarMap(L<Var> vars) {
308	new HashMap<S, Var> map;
309	for (Var v : vars)
310	map.put(v.getName(), v);
311	ret map;
312	}
313
314	new L<Clause> emptyProgram;
315
316	// Executor stack entry
317	class Entry {
318	Goal goal;
319	L<Clause> program; // full program or filtered by arity
320	int programIdx = -1; // -1 is natives
321	Trail trail;
322	boolean trailSet;
323
324	(Goal goal) {
325	Lisp car = resolve1(goal.car);
326	if (car instanceof Var) {
327	if (showStuff)
328	log("Weird: Goal is variable: " + car);
329	program = Prolog.this.program;
330	} else {
331	int arity = car.size();
332	if (showStuff)
333	log("Goal arity " + arity + ": " + car);
334	program = arity >= l(programByArity) ? emptyProgram : programByArity.get(arity);
335	}
336	}
337	}
338
339	void start(Lisp goal) {
340	start(new Goal(prologify(goal)));
341	}
342
343	// warning: doesn't prologify the goal
344	void start(Goal goal) {
345	if (showStuff)
346	log("Starting on goal: " + structure_seen(goal));
347	steps = 0;
348	stack = new L;
349	Trail_Undo(null);
350	stackAdd(new Entry(goal));
351	startTime = now();
352	}
353
354	void log(S s) {
355	if (log != null) {
356	if (l(log) == maxLogSize)
357	log.add("[Log overflow]");
358	else if (l(log) < maxLogSize)
359	log.add(s);
360	} else if (showStuff)
361	print("prolog: " + s);
362	}
363
364	int level() {
365	ret l(stack)-1;
366	}
367
368	boolean done() {
369	boolean result = empty(stack);
370	if (showStuff && result)
371	log("Done with goal!");
372	ret result;
373	}
374
375	boolean gnext(Goal g) {
376	Goal gdash = g.cdr;
377	if (gdash == null) {
378	if (showStuff)
379	log("gnext true");
380	ret true;
381	} else {
382	stackAdd(new Entry(gdash));
383	ret false;
384	}
385	}
386
387	void stackPop() {
388	Entry e = popLast(stack);
389	if (e.trailSet)
390	Trail_Undo(e.trail);
391	}
392
393	void backToCutPoint(int n) {
394	if (showStuff)
395	log("back to cut point " + n);
396	while (l(stack) >= n) {
397	if (showStuff)
398	log("cut: dropping " + structure(last(stack).goal));
399	stackPop();
400	}
401	}
402
403	boolean step() {
404	if (done()) fail("done!"); // safety
405	if (now() >= startTime+timeLimit*1000)
406	fail("time limit reached: " + timeLimit + " s");
407
408	++steps;
409	Entry e = last(stack);
410
411	if (e.trailSet) {
412	Trail_Undo(e.trail);
413	e.trailSet = false;
414	}
415
416	e.trail = Trail_Note();
417	e.trailSet = true;
418
419	// cut operator - suceeds first time
420	if (e.goal.car.is("!", 1)) {
421	if (showStuff)
422	log("cut " + e.programIdx + ". " + structure(e.goal));
423	if (e.programIdx == -1) {
424	++e.programIdx;
425	ret gnext(e.goal);
426	} else if (e.programIdx == 0) {
427	++e.programIdx;
428	// fails 2nd time and cuts
429	//e.goal.car.head = "false"; // super-hack :D
430	backToCutPoint(parseInt(e.goal.car.get(0).raw()));
431	ret false;
432	} else {
433	stackPop();
434	ret false;
435	}
436	}
437
438	if (e.programIdx >= l(e.program)) { // program loop ends
439	removeLast(stack);
440	ret false;
441	}
442
443	if (e.programIdx == -1) {
444	++e.programIdx;
445
446	// try native functions
447	if (goNative(e.goal.car)) {
448	if (showStuff)
449	log(indent(level()) + "native!");
450
451	ret gnext(e.goal);
452	}
453
454	ret false;
455	}
456
457	// now in program loop
458
459	Clause c = e.program.get(e.programIdx).copy();
460	++e.programIdx;
461	Trail_Undo(e.trail);
462	S text = null;
463	if (showStuff)
464	text = " Goal: " + e.goal + ". Got clause: " + c;
465	++topUnifications;
466	if (unify(e.goal.car, c.head)) {
467	if (showStuff) {
468	log(indent(level()) + text);
469	log(indent(level()) + " Clause unifies to: " + c);
470	}
471	Goal gdash;
472	if (c.nat != null) {
473	if (showStuff)
474	log(indent(level()) + " Clause is native.");
475	if (!c.nat.yo(this, c.head)) {
476	if (showStuff)
477	log(indent(level()) + "Native clause fails");
478	ret false;
479	}
480	gdash = e.goal.cdr;
481	} else
482	gdash = c.body == null ? e.goal.cdr : resolveCut(c.body).append(e.goal.cdr);
483	if (showStuff)
484	log(indent(level()) + " gdash: " + gdash);
485
486	if (gdash == null) {
487	if (showStuff)
488	log("SUCCESS!");
489	ret true;
490	} else {
491	Entry e2 = new Entry(gdash);
492	if (showStuff)
493	log(indent(level()) + "New goal: " + gdash);
494	stackAdd(e2);
495	ret false;
496	}
497	} /*else
498	if (showStuff)
499	log(indent(level()) + "No match for clause.");*/
500
501	ret false;
502	}
503
504	// resolve cut in clause body
505	Goal resolveCut(Goal g) {
506	if (g.car.is("!", 0))
507	ret fixCut(g);
508	if (g.cdr == null)
509	ret g;
510	ret new Goal(g.car, resolveCut(g.cdr));
511	}
512
513	// note stack length in cut
514	Goal fixCut(Goal g) {
515	ret new Goal(lisp("!", lstr(stack)), g.cdr); // max. one cut per clause
516	}
517
518	void stackAdd(Entry e) {
519	stack.add(e);
520	int n = l(stack);
521	if (n > maxLevel) fail("Maximum stack level reached: " + n);
522	if (n > maxLevelSeen) maxLevelSeen = n;
523	}
524
525	void addClause(S text) {
526	addClause(nlParse(text));
527	}
528
529	void addClause(Lisp c) {
530	addClause(clause(c));
531	}
532
533	void addClause(Clause c) {
534	program.add(c);
535	int arity = c.head.size();
536	while (arity >= l(programByArity))
537	programByArity.add(new L);
538	programByArity.get(arity).add(c);
539	}
540
541	boolean canSolve(Lisp goal) {
542	ret canSolve(new Goal(prologify(goal)));
543	}
544
545	boolean canSolve(Goal goal) {
546	start(goal);
547	while (!done())
548	if (step())
549	ret true;
550	ret false;
551	}
552
553	// return variable map or null if unsolved
554	Map<S, Lisp> solve(Lisp goal) {
555	start(new Goal(prologify(goal)));
556	ret nextSolution();
557	}
558
559	Map<S, Lisp> solve(S text) {
560	ret solve(nlParse(text));
561	}
562
563	Map<S, Lisp> getUserVarMap() {
564	Goal g = stack.get(0).goal;
565	new HashMap<S, Lisp> map;
566	for (Var v : findVars(g))
567	if (v.isUserVar())
568	map.put(v.getName(), resolve(v));
569	ret map;
570	}
571
572	Map<S, Lisp> nextSolution() {
573	if (showStuff)
574	log("nextSolution");
575	int n = 0;
576	while (!done()) {
577	++n;
578	if (step()) {
579	if (showStuff)
580	log(" solution found in step " + n);
581	ret getUserVarMap();
582	}
583	}
584	if (showStuff)
585	log("No solution");
586	ret null;
587	}
588
589	void addTheory(S text) {
590	for (Clause c : parseProgram(text))
591	addClause(c);
592	}
593
594	L<Clause> parseProgram(S text) {
595	new L<Clause> l;
596	Lisp tree = nlParse(text);
597	if (nlIsMultipleStatements(text))
598	for (Lisp part : tree)
599	l.add(clause(part));
600	else
601	l.add(clause(tree));
602	ret l;
603	}
604
605	boolean goNative(Lisp term) {
606	term = resolve(term);
607
608	for (Native n : natives) {
609	Trail t = Trail_Note();
610	boolean result;
611	try {
612	result = n.yo(this, term);
613	} catch (Exception e) {
614	Trail_Undo(t);
615	continue;
616	}
617	if (!result) {
618	Trail_Undo(t);
619	continue;
620	}
621	ret true;
622	}
623
624	if (term.is("nativeTest", 0))
625	ret true;
626
627	if (term.is("isQuoted", 1)) {
628	Lisp x = term.get(0);
629	ret !(x instanceof Var) && x.isLeaf() && isQuoted(x.head);
630	}
631
632	ret false;
633	}
634
635	// Resolve top-level only
636	Lisp resolve1(Lisp term) {
637	if (term instanceof Var)
638	ret ((Var) term).getValue();
639	ret term;
640	}
641
642	// resolve all variables
643	Lisp resolve(Lisp term) {
644	term = resolve1(term);
645
646	// smart recurse
647	for (int i = 0; i < term.size(); i++) {
648	Lisp l = term.get(i);
649	Lisp r = resolve(l);
650	if (l != r) {
651	Lisp x = new Lisp(term.head);
652	for (int j = 0; j < i; j++)
653	x.add(term.get(j));
654	x.add(r);
655	for (i++; i < term.size(); i++)
656	x.add(resolve(term.get(i)));
657	ret x;
658	}
659	}
660
661	ret term;
662	}
663
664	// looks for a bodyless rule in the program that matches the term
665	// todo: eqic
666	boolean containsStatement(Lisp term) {
667	for (Clause c : program)
668	if (c.body == null && c.nat == null && eq(c.head, term))
669	ret true;
670	ret false;
671	}
672
673	// closed == contains no variables
674	boolean isClosedTerm(Lisp term) {
675	if (term instanceof Var)
676	ret false;
677	else
678	for (Lisp arg : term)
679	if (!isClosedTerm(arg))
680	ret false;
681	ret true;
682	}
683
684	void addNative(Native n) {
685	if (n instanceof BaseNative)
686	addNative(((BaseNative) n).pat, n);
687	else
688	natives.add(n);
689	}
690
691	void addNatives(Native... l) {
692	for (Native n : l)
693	addNative(n);
694	}
695
696	void addNatives(L<Native> l) {
697	for (Native n : l)
698	addNative(n);
699	}
700
701	void addNative(S text, Native n) {
702	addClause(prologify(new Clause(nlParse(text), n)));
703	}
704
705	L<Lisp> getStackTerms() {
706	new L<Lisp> l;
707	for (Entry e : stack)
708	l.add(e.goal.car);
709	ret l;
710	}
711
712	void logOn() {
713	log = new L;
714	showStuff = true;
715	}
716
717	static abstract class BaseNative implements Native {
718	S pat;
719	Prolog p;
720	Map<S, Lisp> m;
721
722	(S pat) {}
723
724	abstract boolean yo();
725
726	public boolean yo(Prolog p, Lisp term) {
727	m = new HashMap;
728	this.p = p;
729	try {
730	ret nlMatch(pat, p.resolve(term), m) && yo();
731	} catch (Exception e) {
732	++p.exceptions;
733	if (p.showStuff)
734	p.log("Exception in native: " + e);
735	ret false;
736	} finally {
737	this.p = null;
738	}
739	}
740
741	boolean unify(S var, Lisp term) {
742	Lisp v = m.get(var);
743	if (v == null)
744	fail("Variable " + var + " not found");
745	ret p.unify(v, term);
746	}
747	} // BaseNative
748
749	// Prolog constructor
750	*() {
751	addClause(lisp("true"));
752	}
753
754	L<Lisp> rewriteWith(L<Clause> rewriteTheory) {
755	new L<Lisp> result;
756
757	for (Prolog.Clause clause : rewriteTheory) {
758	if (clause.body == null) continue; // need conditions to rewrite anything
759
760	// todo: trail
761	Prolog.Clause c = clause.copy();
762	start(c.body);
763	while (!done()) {
764	if (step()) {
765	Lisp term = resolve(c.head);
766	if (!isClosedTerm(term)) {
767	print("Not a closed term, skipping: " + term);
768	continue;
769	}
770
771	if (containsStatement(term)) {
772	print("Statement exists, skipping: " + term);
773	continue;
774	}
775
776	if (result.contains(term))
777	continue;
778
779	print("Found new statement: " + term);
780	result.add(term);
781	}
782	}
783	}
784
785	ret result;
786	}
787	} // class Prolog