class Prolog (old 2) [1002855]

!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;
  
  // stats
  int maxLevelSeen; // maximum stack level reached during computation
  long topUnifications;

  static interface Native {
    public boolean yo(Prolog p, Lisp term);
  }
  
  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;
    Goal body;
    
    *(Lisp *head, Goal *body) {}
    *(Lisp *head) {}
    
    Clause copy() {
      return new Clause(Prolog.this.copy(head), body == null ? null : body.copy());
    }
    
    public String toString() {
      //ret head + " :- " + (body == null ? "true" : body);
      ret 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 ? null : cdr.append(l));
    }
    
  } // class Goal
  
  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 (neq(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));
  }
  
  Clause clause(Lisp rule) {
    L<Lisp> ops = snlSplitOps(rule);
    if (showStuff)
      print("clause(Lisp): " + rule + " => " + structure(ops)); 
      
    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));
    if (showStuff)
      print("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;
  }
  
  // Executor stack entry
  static class Entry {
    Goal goal;
    int programIdx = -1; // -1 is natives
    Trail trail;
    boolean trailSet;
    boolean cutPoint;
    
    *(Goal *goal) {}
  }
  
  void start(Lisp goal) {
    start(new Goal(prologify(goal)));
  }
  
  // warning: doesn't prologify the goal
  void start(Goal goal) {
    if (showStuff)
      print("start: " + structure_seen(goal));
    steps = 0;
    stack = new L;
    Trail_Undo(null);
    stackAdd(new Entry(goal));
  }
    
  int level() {
    ret l(stack)-1;
  }
  
  boolean done() {
    ret empty(stack);
  }

  boolean gnext(Goal g) {  
    Goal gdash = g.cdr;
    if (gdash == null)
      ret true;
    else {
      stackAdd(new Entry(gdash));
      ret false;
    }
  }
  
  void stackPop() {
    Entry e = popLast(stack);
    if (e.trailSet)
      Trail_Undo(e.trail);
  }
  
  void backToCutPoint() {
    if (showStuff)
      print("back to cut point.");
    while (!empty(stack) && !last(stack).cutPoint) {
      if (showStuff)
        print("cut: dropping " + structure(last(stack)));
      stackPop();
    }
    for (int i = 0; i < 2; i++) {
      if (!empty(stack)) {
        if (showStuff)
          print("cut: dropping " + i + " " + structure(last(stack)));
        stackPop();
      }
    }
  }

  boolean step() {
    if (done()) fail("done!"); // safety
    
    ++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("!", 0)) {
      if (showStuff)
        print("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();
        ret false;
      } else {
        stackPop();
        ret false;
      }
    }

    if (e.programIdx >= l(program)) { // program loop ends
      removeLast(stack);
      ret false;
    }
      
    if (e.programIdx == -1) {
      if (showStuff)
        print(indent(level()) + "solve@" + level() + ": " + e.goal);
      ++e.programIdx;
        
      // try native functions
      if (goNative(e.goal.car)) {
        if (showStuff)
          print(indent(level()) + "native!");
          
        ret gnext(e.goal);
      }
      
      ret false;
    }
      
    // now in program loop
    
    Clause c = program.get(e.programIdx).copy();
    ++e.programIdx;
    Trail_Undo(e.trail);
    if (showStuff)
      print(indent(level()) + "  try:" + c);
    ++topUnifications;
    if (unify(e.goal.car, c.head)) {
      Goal gdash = c.body == null ? e.goal.cdr : c.body.append(e.goal.cdr);
      if (gdash == null)
        ret true;
      else {
        Entry e2 = new Entry(gdash);
        if (c.body != null)
          e2.cutPoint = true;
        stackAdd(e2);
        ret false;
      }
    } else
      if (showStuff)
        print(indent(level()) + "  nomatch.");
        
    ret false;
  }
  
  void stackAdd(Entry e) {
    stack.add(e);
    int n = l(stack);
    if (n > maxLevelSeen) maxLevelSeen = n;
  }
  
  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) {
    Goal g = new Goal(prologify(goal));
    if (!canSolve(g))
      ret null;
    ret getUserVarMap();
  }
  
  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(), v.getValue());
    ret map;
  }
  
  Map<S, Lisp> nextSolution() {
    while (!done())
      if (step())
        ret getUserVarMap();
    ret null;
  }
  
  void addTheory(S text) {
    for (Lisp part : nlParseToTheory(text))
      addClause(part);
  }
  
  // shouldn't use anymore
  void addClauses(Lisp tree) {
    if (isJuxta(tree) && snlSplitOps(tree) == null)
      for (Lisp part : tree)
        addClause(part);
    else
      addClause(tree);
  }
  
  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("true", 0))
      ret true;
      
    if (term.is("isQuoted", 1)) {
      Lisp x = term.get(0);
      ret !(x instanceof Var) && x.isLeaf() && isQuoted(x.head);
    }
      
    ret false;
  }
  
  boolean unifyOrRollback(Lisp a, Lisp b) {
    Trail t = Trail_Note();
    if (unify(a, b)) ret true;
    Trail_Undo(t);
    ret false;
  }
  
  // resolve all variables
  Lisp resolve(Lisp term) {
    if (term instanceof Var)
      ret ((Var) term).getValue();
      
    // 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
  boolean containsStatement(Lisp term) {
    for (Clause c : program)
      if (c.body == 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) {
    natives.add(n);
  }
  
  L<Lisp> getStackTerms() {
    new L<Lisp> l;
    for (Entry e : stack)
      l.add(e.goal.car);
    ret l;
  }
  
} // class Prolog

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

Snippet ID:	#1002855
Snippet name:	class Prolog (old 2)
Eternal ID of this version:	#1002855/1
Text MD5:	a5b70fc1297d6502ac2412c5223baa63
Author:	stefan
Category:	javax
Type:	JavaX fragment (include)
Public (visible to everyone):	Yes
Archived (hidden from active list):	No
Created/modified:	2016-03-05 17:46:07
Source code size:	13202 bytes / 589 lines
Pitched / IR pitched:	No / No
Views / Downloads:	870 / 817
Referenced in:	[show references]

< > BotCompany Repo | #1002855 // class Prolog (old 2)

JavaX fragment (include) [tags: archive]

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
14	// stats
15	int maxLevelSeen; // maximum stack level reached during computation
16	long topUnifications;
17
18	static interface Native {
19	public boolean yo(Prolog p, Lisp term);
20	}
21
22	static class Var extends Lisp {
23	long id;
24	Lisp instance;
25
26	*(S name) {
27	super(name);
28	instance = this;
29	}
30
31	*(long id) {
32	super("___");
33	this.id = id;
34	instance = this;
35	}
36
37	void reset() { instance = this; }
38
39	public String toString() {
40	if (instance != this)
41	ret instance.toString();
42	ret isUserVar() ? getName() : "_" + id;
43	}
44
45	boolean isUserVar() {
46	ret id == 0;
47	}
48
49	S getName() {
50	ret head;
51	}
52
53	Lisp getValue() {
54	Lisp l = instance;
55	while (l instanceof Var) {
56	Var v = cast l;
57	if (v.instance == v)
58	ret v;
59	l = v.instance;
60	}
61	ret l;
62	}
63	}
64
65	class Clause {
66	Lisp head;
67	Goal body;
68
69	(Lisp head, Goal *body) {}
70	(Lisp head) {}
71
72	Clause copy() {
73	return new Clause(Prolog.this.copy(head), body == null ? null : body.copy());
74	}
75
76	public String toString() {
77	//ret head + " :- " + (body == null ? "true" : body);
78	ret body == null ? head.toString() : head + " :- " + body;
79	}
80	}
81
82	class Trail {
83	Var tcar;
84	Trail tcdr;
85
86	(Var tcar, Trail *tcdr) {}
87	}
88
89	Trail Trail_Note() { return sofar; }
90	void Trail_Push(Var x) { sofar = new Trail(x, sofar); }
91	void Trail_Undo(Trail whereto) {
92	for (; sofar != whereto; sofar = sofar.tcdr)
93	sofar.tcar.reset();
94	}
95
96	static class TermVarMapping {
97	new L<Var> vars;
98
99	(L<Var> vars) {}
100	*(Var... vars) { this.vars.addAll(asList(vars)); }
101
102	void showanswer() {
103	print("TRUE.");
104	for (Var v : vars)
105	print(" " + v.getName() + " = " + v);
106	}
107	}
108
109	class Goal {
110	Lisp car;
111	Goal cdr;
112
113	(Lisp car, Goal *cdr) {}
114	(Lisp car) {}
115
116	public String toString() {
117	ret cdr == null ? car.toString() : car + "; " + cdr;
118	}
119
120	Goal copy() {
121	return new Goal(Prolog.this.copy(car),
122	cdr == null ? null : cdr.copy());
123	}
124
125	Goal append(Goal l) {
126	return new Goal(car, cdr == null ? null : cdr.append(l));
127	}
128
129	} // class Goal
130
131	boolean unify(Lisp thiz, Lisp t) {
132	if (thiz == null) fail("thiz=null");
133	if (t == null) fail("t=null");
134
135	if (thiz instanceof Var) { // TermVar::unify
136	Var v = cast thiz;
137	if (v.instance != v)
138	return unify(v.instance, t);
139	Trail_Push(v);
140	v.instance = t;
141	return true;
142	}
143
144	// TermCons::unify
145	return unify2(t, thiz);
146	}
147
148	boolean unify2(Lisp thiz, Lisp t) {
149	if (thiz instanceof Var)
150	return unify(thiz, t);
151
152	int arity = thiz.size();
153	if (neq(thiz.head, t.head) \|\| arity != t.size())
154	return false;
155	for (int i = 0; i < arity; i++)
156	if (!unify(thiz.get(i), t.get(i)))
157	return false;
158	return true;
159	}
160
161	Lisp copy(Lisp thiz) {
162	if (thiz instanceof Var) {
163	Var v = cast thiz;
164	if (v.instance == v) {
165	Trail_Push(v);
166	v.instance = newVar();
167	}
168	return v.instance;
169	}
170
171	// copy2 (copy non-var)
172	Lisp l = new Lisp(thiz.head);
173	for (Lisp arg : thiz)
174	l.add(copy(arg));
175	ret l;
176	}
177
178	Var newVar() {
179	ret new Var(++varCount);
180	}
181
182	Var newVar(S name) {
183	ret new Var(name);
184	}
185
186	Clause clause(Lisp head, Goal body) {
187	ret prologify(new Clause(head, body));
188	}
189
190	Clause clause(Lisp rule) {
191	L<Lisp> ops = snlSplitOps(rule);
192	if (showStuff)
193	print("clause(Lisp): " + rule + " => " + structure(ops));
194
195	if (!empty(ops) && last(ops).is("then *")) {
196	Lisp head = last(ops).get(0);
197	Goal goal = null;
198
199	// TODO: check the actual words (if/and/...)
200	for (int i = l(ops)-2; i >= 0; i--)
201	goal = new Goal(ops.get(i).get(0), goal);
202
203	ret clause(head, goal);
204	} else
205	ret clause(rule, (Lisp) null);
206	}
207
208	Clause clause(Lisp head, Lisp body) {
209	ret clause(head, body == null ? null : new Goal(body));
210	}
211
212	Lisp prologify(Lisp term) {
213	ret prologify(term, new HashMap);
214	}
215
216	Clause prologify(Clause c) {
217	new HashMap vars;
218	c = new Clause(
219	prologify(c.head, vars),
220	prologify(c.body, vars));
221	if (showStuff)
222	print("Clause made: " + structure_seen(c));
223	ret c;
224	}
225
226	Goal prologify(Goal goal, Map<S, Var> vars) {
227	if (goal == null) ret null;
228	ret new Goal(
229	prologify(goal.car, vars),
230	prologify(goal.cdr, vars));
231	}
232
233	boolean isVar(Lisp term) {
234	ret upperCaseVariables ? snlIsVar(term) : nlIsVar(term);
235	}
236
237	Lisp prologify(Lisp term, Map<S, Var> vars) {
238	if (term == null) ret null;
239	if (isVar(term)) {
240	Var v = vars.get(term.head);
241	if (v == null)
242	vars.put(term.head, v = newVar(term.head));
243	ret v;
244	} else {
245	Lisp l = new Lisp(term.head);
246	for (Lisp arg : term)
247	l.add(prologify(arg, vars));
248	ret l;
249	}
250	}
251
252	L<Var> findVars(Goal g) {
253	new IdentityHashMap<Var, Boolean> map;
254	while (g != null) {
255	findVars(g.car, map);
256	g = g.cdr;
257	}
258	ret asList(map.keySet());
259	}
260
261	L<Var> findVars(Lisp term) {
262	new IdentityHashMap<Var, Boolean> map;
263	findVars(term, map);
264	ret asList(map.keySet());
265	}
266
267	void findVars(Lisp term, IdentityHashMap<Var, Boolean> map) {
268	if (term instanceof Var)
269	map.put((Var) term, Boolean.TRUE);
270	else
271	for (Lisp arg : term)
272	findVars(arg, map);
273	}
274
275	static Map<S, Var> makeVarMap(L<Var> vars) {
276	new HashMap<S, Var> map;
277	for (Var v : vars)
278	map.put(v.getName(), v);
279	ret map;
280	}
281
282	// Executor stack entry
283	static class Entry {
284	Goal goal;
285	int programIdx = -1; // -1 is natives
286	Trail trail;
287	boolean trailSet;
288	boolean cutPoint;
289
290	(Goal goal) {}
291	}
292
293	void start(Lisp goal) {
294	start(new Goal(prologify(goal)));
295	}
296
297	// warning: doesn't prologify the goal
298	void start(Goal goal) {
299	if (showStuff)
300	print("start: " + structure_seen(goal));
301	steps = 0;
302	stack = new L;
303	Trail_Undo(null);
304	stackAdd(new Entry(goal));
305	}
306
307	int level() {
308	ret l(stack)-1;
309	}
310
311	boolean done() {
312	ret empty(stack);
313	}
314
315	boolean gnext(Goal g) {
316	Goal gdash = g.cdr;
317	if (gdash == null)
318	ret true;
319	else {
320	stackAdd(new Entry(gdash));
321	ret false;
322	}
323	}
324
325	void stackPop() {
326	Entry e = popLast(stack);
327	if (e.trailSet)
328	Trail_Undo(e.trail);
329	}
330
331	void backToCutPoint() {
332	if (showStuff)
333	print("back to cut point.");
334	while (!empty(stack) && !last(stack).cutPoint) {
335	if (showStuff)
336	print("cut: dropping " + structure(last(stack)));
337	stackPop();
338	}
339	for (int i = 0; i < 2; i++) {
340	if (!empty(stack)) {
341	if (showStuff)
342	print("cut: dropping " + i + " " + structure(last(stack)));
343	stackPop();
344	}
345	}
346	}
347
348	boolean step() {
349	if (done()) fail("done!"); // safety
350
351	++steps;
352	Entry e = last(stack);
353
354	if (e.trailSet) {
355	Trail_Undo(e.trail);
356	e.trailSet = false;
357	}
358
359	e.trail = Trail_Note();
360	e.trailSet = true;
361
362	// cut operator - suceeds first time
363	if (e.goal.car.is("!", 0)) {
364	if (showStuff)
365	print("cut " + e.programIdx + ". " + structure(e.goal));
366	if (e.programIdx == -1) {
367	++e.programIdx;
368	ret gnext(e.goal);
369	} else if (e.programIdx == 0) {
370	++e.programIdx;
371	// fails 2nd time and cuts
372	//e.goal.car.head = "false"; // super-hack :D
373	backToCutPoint();
374	ret false;
375	} else {
376	stackPop();
377	ret false;
378	}
379	}
380
381	if (e.programIdx >= l(program)) { // program loop ends
382	removeLast(stack);
383	ret false;
384	}
385
386	if (e.programIdx == -1) {
387	if (showStuff)
388	print(indent(level()) + "solve@" + level() + ": " + e.goal);
389	++e.programIdx;
390
391	// try native functions
392	if (goNative(e.goal.car)) {
393	if (showStuff)
394	print(indent(level()) + "native!");
395
396	ret gnext(e.goal);
397	}
398
399	ret false;
400	}
401
402	// now in program loop
403
404	Clause c = program.get(e.programIdx).copy();
405	++e.programIdx;
406	Trail_Undo(e.trail);
407	if (showStuff)
408	print(indent(level()) + " try:" + c);
409	++topUnifications;
410	if (unify(e.goal.car, c.head)) {
411	Goal gdash = c.body == null ? e.goal.cdr : c.body.append(e.goal.cdr);
412	if (gdash == null)
413	ret true;
414	else {
415	Entry e2 = new Entry(gdash);
416	if (c.body != null)
417	e2.cutPoint = true;
418	stackAdd(e2);
419	ret false;
420	}
421	} else
422	if (showStuff)
423	print(indent(level()) + " nomatch.");
424
425	ret false;
426	}
427
428	void stackAdd(Entry e) {
429	stack.add(e);
430	int n = l(stack);
431	if (n > maxLevelSeen) maxLevelSeen = n;
432	}
433
434	void addClause(Lisp c) {
435	addClause(clause(c));
436	}
437
438	void addClause(Clause c) {
439	program.add(c);
440	int arity = c.head.size();
441	while (arity >= l(programByArity))
442	programByArity.add(new L);
443	programByArity.get(arity).add(c);
444	}
445
446	boolean canSolve(Lisp goal) {
447	ret canSolve(new Goal(prologify(goal)));
448	}
449
450	boolean canSolve(Goal goal) {
451	start(goal);
452	while (!done())
453	if (step())
454	ret true;
455	ret false;
456	}
457
458	// return variable map or null if unsolved
459	Map<S, Lisp> solve(Lisp goal) {
460	Goal g = new Goal(prologify(goal));
461	if (!canSolve(g))
462	ret null;
463	ret getUserVarMap();
464	}
465
466	Map<S, Lisp> getUserVarMap() {
467	Goal g = stack.get(0).goal;
468	new HashMap<S, Lisp> map;
469	for (Var v : findVars(g))
470	if (v.isUserVar())
471	map.put(v.getName(), v.getValue());
472	ret map;
473	}
474
475	Map<S, Lisp> nextSolution() {
476	while (!done())
477	if (step())
478	ret getUserVarMap();
479	ret null;
480	}
481
482	void addTheory(S text) {
483	for (Lisp part : nlParseToTheory(text))
484	addClause(part);
485	}
486
487	// shouldn't use anymore
488	void addClauses(Lisp tree) {
489	if (isJuxta(tree) && snlSplitOps(tree) == null)
490	for (Lisp part : tree)
491	addClause(part);
492	else
493	addClause(tree);
494	}
495
496	boolean goNative(Lisp term) {
497	term = resolve(term);
498
499	for (Native n : natives) {
500	Trail t = Trail_Note();
501	boolean result;
502	try {
503	result = n.yo(this, term);
504	} catch (Exception e) {
505	Trail_Undo(t);
506	continue;
507	}
508	if (!result) {
509	Trail_Undo(t);
510	continue;
511	}
512	ret true;
513	}
514
515	if (term.is("nativeTest", 0))
516	ret true;
517
518	if (term.is("true", 0))
519	ret true;
520
521	if (term.is("isQuoted", 1)) {
522	Lisp x = term.get(0);
523	ret !(x instanceof Var) && x.isLeaf() && isQuoted(x.head);
524	}
525
526	ret false;
527	}
528
529	boolean unifyOrRollback(Lisp a, Lisp b) {
530	Trail t = Trail_Note();
531	if (unify(a, b)) ret true;
532	Trail_Undo(t);
533	ret false;
534	}
535
536	// resolve all variables
537	Lisp resolve(Lisp term) {
538	if (term instanceof Var)
539	ret ((Var) term).getValue();
540
541	// smart recurse
542	for (int i = 0; i < term.size(); i++) {
543	Lisp l = term.get(i);
544	Lisp r = resolve(l);
545	if (l != r) {
546	Lisp x = new Lisp(term.head);
547	for (int j = 0; j < i; j++)
548	x.add(term.get(j));
549	x.add(r);
550	for (i++; i < term.size(); i++)
551	x.add(resolve(term.get(i)));
552	ret x;
553	}
554	}
555
556	ret term;
557	}
558
559	// looks for a bodyless rule in the program that matches the term
560	boolean containsStatement(Lisp term) {
561	for (Clause c : program)
562	if (c.body == null && eq(c.head, term))
563	ret true;
564	ret false;
565	}
566
567	// closed == contains no variables
568	boolean isClosedTerm(Lisp term) {
569	if (term instanceof Var)
570	ret false;
571	else
572	for (Lisp arg : term)
573	if (!isClosedTerm(arg))
574	ret false;
575	ret true;
576	}
577
578	void addNative(Native n) {
579	natives.add(n);
580	}
581
582	L<Lisp> getStackTerms() {
583	new L<Lisp> l;
584	for (Entry e : stack)
585	l.add(e.goal.car);
586	ret l;
587	}
588
589	} // class Prolog