Not logged in.  Login/Logout/Register | List snippets | | Create snippet | Upload image | Upload data

744
LINES

< > BotCompany Repo | #1002857 // class Prolog (arity optimization, older)

JavaX fragment (include)

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

Author comment

Began life as a copy of #1002855

download  show line numbers  debug dex  old transpilations   

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

No comments. add comment

Snippet ID: #1002857
Snippet name: class Prolog (arity optimization, older)
Eternal ID of this version: #1002857/1
Text MD5: 9211e3d39b07158b821fcbe889bf76a4
Author: stefan
Category: javax
Type: JavaX fragment (include)
Public (visible to everyone): Yes
Archived (hidden from active list): No
Created/modified: 2016-03-14 01:11:54
Source code size: 17238 bytes / 744 lines
Pitched / IR pitched: No / No
Views / Downloads: 627 / 597
Referenced in: [show references]