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 | // name of theory to memorize stuff to |
21 | S outTheory; |
22 | |
23 | // stats |
24 | int maxLevelSeen; // maximum stack level reached during computation |
25 | long topUnifications, exceptions; |
26 | |
27 | static interface Native { |
28 | public boolean yo(Prolog p, Lisp term); |
29 | } |
30 | |
31 | boolean headeq(S a, S b) { |
32 | ret isQuoted (a) ? eq(a, b) : eqic(a, b); |
33 | } |
34 | |
35 | static class Var extends Lisp { |
36 | long id; |
37 | Lisp instance; |
38 | |
39 | *(S name) { |
40 | super(name); |
41 | instance = this; |
42 | } |
43 | |
44 | *(long id) { |
45 | super("___"); |
46 | this.id = id; |
47 | instance = this; |
48 | } |
49 | |
50 | void reset() { instance = this; } |
51 | |
52 | public String toString() { |
53 | if (instance != this) |
54 | ret instance.toString(); |
55 | ret prettyName(); |
56 | } |
57 | |
58 | S prettyName() { |
59 | ret isUserVar() ? getName() : "_" + id; |
60 | } |
61 | |
62 | boolean isUserVar() { |
63 | ret id == 0; |
64 | } |
65 | |
66 | S getName() { |
67 | ret head; |
68 | } |
69 | |
70 | Lisp getValue() { |
71 | Lisp l = instance; |
72 | while (l instanceof Var) { |
73 | Var v = cast l; |
74 | if (v.instance == v) |
75 | ret v; |
76 | l = v.instance; |
77 | } |
78 | ret l; |
79 | } |
80 | } |
81 | |
82 | static class Collector extends Lisp { |
83 | new L<Lisp> solutions; |
84 | |
85 | *() { super("___"); } |
86 | |
87 | public S toString() { |
88 | ret "<collector>"; |
89 | } |
90 | } |
91 | |
92 | class Clause { |
93 | Lisp head; |
94 | S loadedFrom; // theory name |
95 | boolean used; |
96 | |
97 | // Either body or nat will be set (or none) |
98 | Native nat; |
99 | Goal body; |
100 | |
101 | *(Lisp *head, Native *nat) {} |
102 | *(Lisp *head, Goal *body) {} |
103 | *(Lisp *head, Goal *body, Native *nat) {} |
104 | *(Lisp *head) {} |
105 | |
106 | Clause copy() { |
107 | ret new Clause(Prolog.this.copy(head), body == null ? null : body.copy(), nat); |
108 | } |
109 | |
110 | public String toString() { |
111 | //ret head + " :- " + (body == null ? "true" : body); |
112 | ret nat != null ? head + " :- native" : |
113 | (body == null ? head.toString() : head + " :- " + body); |
114 | } |
115 | } |
116 | |
117 | class Trail { |
118 | Var tcar; |
119 | Trail tcdr; |
120 | |
121 | *(Var *tcar, Trail *tcdr) {} |
122 | } |
123 | |
124 | Trail Trail_Note() { return sofar; } |
125 | void Trail_Set(Var x, Lisp value) { |
126 | sofar = new Trail(x, sofar); |
127 | x.instance = value; |
128 | /*if (showStuff) |
129 | log(indent(level()) + " Push " + x.prettyName() + " (" + x + ")");*/ |
130 | } |
131 | void Trail_Undo(Trail whereto) { |
132 | for (; sofar != whereto; sofar = sofar.tcdr) { |
133 | /*if (showStuff) |
134 | log(indent(level()) + " Resetting variable " + sofar.tcar.prettyName() + " (" + sofar.tcar + ")");*/ |
135 | sofar.tcar.reset(); |
136 | } |
137 | } |
138 | |
139 | static class TermVarMapping { |
140 | new L<Var> vars; |
141 | |
142 | *(L<Var> *vars) {} |
143 | *(Var... vars) { this.vars.addAll(asList(vars)); } |
144 | |
145 | void showanswer() { |
146 | print("TRUE."); |
147 | for (Var v : vars) |
148 | print(" " + v.prettyName() + " = " + v); |
149 | } |
150 | } |
151 | |
152 | class Goal { |
153 | Lisp car; |
154 | Goal cdr; |
155 | |
156 | *(Lisp *car, Goal *cdr) {} |
157 | *(Lisp *car) {} |
158 | |
159 | public String toString() { |
160 | ret cdr == null ? car.toString() : car + "; " + cdr; |
161 | } |
162 | |
163 | Goal copy() { |
164 | return new Goal(Prolog.this.copy(car), |
165 | cdr == null ? null : cdr.copy()); |
166 | } |
167 | |
168 | Goal append(Goal l) { |
169 | return new Goal(car, cdr == null ? l : cdr.append(l)); |
170 | } |
171 | |
172 | } // class Goal |
173 | |
174 | boolean unifyOrRollback(Lisp a, Lisp b) { |
175 | Trail t = Trail_Note(); |
176 | if (unify(a, b)) ret true; |
177 | Trail_Undo(t); |
178 | ret false; |
179 | } |
180 | |
181 | boolean unify(Lisp thiz, Lisp t) { |
182 | if (thiz == null) fail("thiz=null"); |
183 | if (t == null) fail("t=null"); |
184 | |
185 | if (thiz instanceof Var) { // TermVar::unify |
186 | Var v = cast thiz; |
187 | if (v.instance != v) |
188 | return unify(v.instance, t); |
189 | Trail_Set(v, t); |
190 | return true; |
191 | } |
192 | |
193 | // TermCons::unify |
194 | return unify2(t, thiz); |
195 | } |
196 | |
197 | boolean unify2(Lisp thiz, Lisp t) { |
198 | if (thiz instanceof Var) |
199 | return unify(thiz, t); |
200 | |
201 | int arity = thiz.size(); |
202 | if (!headeq(thiz.head, t.head) || arity != t.size()) |
203 | return false; |
204 | for (int i = 0; i < arity; i++) |
205 | if (!unify(thiz.get(i), t.get(i))) |
206 | return false; |
207 | return true; |
208 | } |
209 | |
210 | Lisp copy(Lisp thiz) { |
211 | if (thiz instanceof Var) { |
212 | Var v = cast thiz; |
213 | if (v.instance == v) { |
214 | Trail_Set(v, newVar()); |
215 | } |
216 | return v.instance; |
217 | } |
218 | |
219 | // copy2 (copy non-var) |
220 | Lisp l = new Lisp(thiz.head); |
221 | for (Lisp arg : thiz) |
222 | l.add(copy(arg)); |
223 | ret l; |
224 | } |
225 | |
226 | Var newVar() { |
227 | ret new Var(++varCount); |
228 | } |
229 | |
230 | Var newVar(S name) { |
231 | ret new Var(name); |
232 | } |
233 | |
234 | Clause clause(Lisp head, Goal body) { |
235 | ret prologify(new Clause(head, body)); |
236 | } |
237 | |
238 | // primary processor for freshly parsed rules |
239 | |
240 | Clause clause(Lisp rule) { |
241 | L<Lisp> ops = snlSplitOps(rule); |
242 | /*if (showStuff) |
243 | log("clause(Lisp): " + rule + " => " + structure(ops)); */ |
244 | |
245 | if (!empty(ops) && last(ops).is("say *")) |
246 | ops.set(l(ops)-1, lisp("then *", lisp("[]", "say", last(ops).get(0)))); |
247 | |
248 | rule = empty(ops) ? rule : snlJoinOps(ops); |
249 | |
250 | if (allowEval) |
251 | rule = new EvalTransform().evalTransformRule(rule); |
252 | |
253 | ops = snlSplitOps(rule); |
254 | if (!empty(ops) && last(ops).is("then *")) { |
255 | Lisp head = last(ops).get(0); |
256 | Goal goal = null; |
257 | |
258 | // TODO: check the actual words (if/and/...) |
259 | for (int i = l(ops)-2; i >= 0; i--) |
260 | goal = new Goal(ops.get(i).get(0), goal); |
261 | |
262 | ret clause(head, goal); |
263 | } else |
264 | ret clause(rule, (Lisp) null); |
265 | } |
266 | |
267 | Clause clause(Lisp head, Lisp body) { |
268 | ret clause(head, body == null ? null : new Goal(body)); |
269 | } |
270 | |
271 | Lisp prologify(Lisp term) { |
272 | ret prologify(term, new HashMap); |
273 | } |
274 | |
275 | Clause prologify(Clause c) { |
276 | new HashMap vars; |
277 | c = new Clause( |
278 | prologify(c.head, vars), |
279 | prologify(c.body, vars), |
280 | c.nat); |
281 | /*if (showStuff) |
282 | log("Clause made: " + structure_seen(c));*/ |
283 | ret c; |
284 | } |
285 | |
286 | Goal prologify(Goal goal, Map<S, Var> vars) { |
287 | if (goal == null) ret null; |
288 | ret new Goal( |
289 | prologify(goal.car, vars), |
290 | prologify(goal.cdr, vars)); |
291 | } |
292 | |
293 | // Note: only for un-prologified |
294 | boolean isVar(Lisp term) { |
295 | ret upperCaseVariables ? snlIsVar(term) : nlIsVar(term); |
296 | } |
297 | |
298 | // for prologified (e.g. in native clauses) |
299 | boolean isLiveVar(Lisp term) { |
300 | ret term instanceof Var; |
301 | } |
302 | |
303 | Lisp prologify(Lisp term, Map<S, Var> vars) { |
304 | if (term == null) ret null; |
305 | if (isVar(term)) { |
306 | Var v = vars.get(term.head); |
307 | if (v == null) |
308 | vars.put(term.head, v = newVar(term.head)); |
309 | ret v; |
310 | } else { |
311 | Lisp l = new Lisp(term.head); |
312 | for (Lisp arg : term) |
313 | l.add(prologify(arg, vars)); |
314 | ret l; |
315 | } |
316 | } |
317 | |
318 | L<Var> findVars(Goal g) { |
319 | new IdentityHashMap<Var, Boolean> map; |
320 | while (g != null) { |
321 | findVars(g.car, map); |
322 | g = g.cdr; |
323 | } |
324 | ret asList(map.keySet()); |
325 | } |
326 | |
327 | L<Var> findVars(Lisp term) { |
328 | new IdentityHashMap<Var, Boolean> map; |
329 | findVars(term, map); |
330 | ret asList(map.keySet()); |
331 | } |
332 | |
333 | void findVars(Lisp term, IdentityHashMap<Var, Boolean> map) { |
334 | if (term instanceof Var) |
335 | map.put((Var) term, Boolean.TRUE); |
336 | else |
337 | for (Lisp arg : term) |
338 | findVars(arg, map); |
339 | } |
340 | |
341 | static Map<S, Var> makeVarMap(L<Var> vars) { |
342 | new HashMap<S, Var> map; |
343 | for (Var v : vars) |
344 | map.put(v.getName(), v); |
345 | ret map; |
346 | } |
347 | |
348 | new L<Clause> emptyProgram; |
349 | |
350 | // Executor stack entry |
351 | class Entry { |
352 | Goal goal; |
353 | L<Clause> program; // full program or filtered by arity |
354 | int programIdx = -1; // -1 is natives |
355 | Trail trail; |
356 | boolean trailSet; |
357 | |
358 | *(Goal *goal) { |
359 | Lisp car = resolve1(goal.car); |
360 | if (car instanceof Var) { |
361 | if (showStuff) |
362 | log("Weird: Goal is variable: " + car); |
363 | program = Prolog.this.program; |
364 | } else { |
365 | int arity = car.size(); |
366 | if (showStuff) |
367 | log(indent(level()) + "Goal arity " + arity + ": " + render(car)); |
368 | program = arity >= l(programByArity) ? emptyProgram : programByArity.get(arity); |
369 | } |
370 | } |
371 | } |
372 | |
373 | void start(S goal) { |
374 | start(nlParse(goal)); |
375 | } |
376 | |
377 | void start(Lisp goal) { |
378 | start(new Goal(prologify(goal))); |
379 | } |
380 | |
381 | S render(Lisp term) { |
382 | ret nlUnparse(resolve(term)); |
383 | } |
384 | |
385 | S render(Goal goal) { |
386 | ret goal == null ? "-" : render(goal.car); |
387 | } |
388 | |
389 | S render(Clause c) { |
390 | ret c == null ? "-" : render(c.head); |
391 | } |
392 | |
393 | // warning: doesn't prologify the goal |
394 | void start(Goal goal) { |
395 | if (showStuff) |
396 | log("Starting on goal: " + render(goal)); |
397 | steps = 0; |
398 | stack = new L; |
399 | Trail_Undo(null); |
400 | stackAdd(new Entry(goal)); |
401 | startTime = now(); |
402 | } |
403 | |
404 | void log(S s) { |
405 | if (log != null) { |
406 | if (l(log) == maxLogSize) { |
407 | log.add("[Log overflow]"); |
408 | showStuff = false; |
409 | } |
410 | else if (l(log) < maxLogSize) |
411 | log.add(s); |
412 | } else if (showStuff) |
413 | print("prolog: " + s); |
414 | } |
415 | |
416 | int level() { |
417 | ret l(stack)-1; |
418 | } |
419 | |
420 | boolean done() { |
421 | boolean result = empty(stack); |
422 | /*if (showStuff && result) |
423 | log("Done with goal!");*/ |
424 | ret result; |
425 | } |
426 | |
427 | boolean gnext(Goal g) { |
428 | Goal gdash = g.cdr; |
429 | if (gdash == null) { |
430 | if (showStuff) |
431 | log("gnext true"); |
432 | ret true; |
433 | } else { |
434 | stackAdd(new Entry(gdash)); |
435 | ret false; |
436 | } |
437 | } |
438 | |
439 | void stackPop() { |
440 | Entry e = popLast(stack); |
441 | if (e.trailSet) |
442 | Trail_Undo(e.trail); |
443 | } |
444 | |
445 | void backToCutPoint(int n) { |
446 | if (showStuff) |
447 | log("back to cut point " + n); |
448 | while (l(stack) >= n) { |
449 | if (showStuff) |
450 | log("cut: dropping " + structure(last(stack).goal)); |
451 | stackPop(); |
452 | } |
453 | } |
454 | |
455 | boolean step() { |
456 | if (done()) fail("done!"); // safety |
457 | if (now() >= startTime+timeLimit*1000) |
458 | fail("time limit reached: " + timeLimit + " s"); |
459 | |
460 | ++steps; |
461 | Entry e = last(stack); |
462 | |
463 | if (e.trailSet) { |
464 | Trail_Undo(e.trail); |
465 | e.trailSet = false; |
466 | } |
467 | |
468 | e.trail = Trail_Note(); |
469 | e.trailSet = true; |
470 | |
471 | // cut operator - suceeds first time |
472 | if (e.goal.car.is("!", 1)) { |
473 | if (showStuff) |
474 | log("cut " + e.programIdx + ". " + structure(e.goal)); |
475 | if (e.programIdx == -1) { |
476 | ++e.programIdx; |
477 | ret gnext(e.goal); |
478 | } else if (e.programIdx == 0) { |
479 | ++e.programIdx; |
480 | // fails 2nd time and cuts |
481 | //e.goal.car.head = "false"; // super-hack :D |
482 | backToCutPoint(parseInt(e.goal.car.get(0).raw())); |
483 | ret false; |
484 | } else { |
485 | stackPop(); |
486 | ret false; |
487 | } |
488 | } |
489 | |
490 | if (e.programIdx >= l(e.program)) { // program loop ends |
491 | removeLast(stack); |
492 | ret false; |
493 | } |
494 | |
495 | if (e.programIdx == -1) { |
496 | ++e.programIdx; |
497 | |
498 | // try native functions |
499 | if (goNative(e.goal.car)) { |
500 | if (showStuff) |
501 | log(indent(level()) + "native!"); |
502 | |
503 | ret gnext(e.goal); |
504 | } |
505 | |
506 | ret false; |
507 | } |
508 | |
509 | // now in program loop |
510 | |
511 | Clause cc = e.program.get(e.programIdx); |
512 | Clause c = cc.copy(); |
513 | ++e.programIdx; |
514 | Trail_Undo(e.trail); |
515 | S text = null; |
516 | if (showStuff) |
517 | //text = " Goal: " + e.goal + ". Got clause: " + c; |
518 | text = "Got clause: " + render(c); |
519 | ++topUnifications; |
520 | if (unify(e.goal.car, c.head)) { |
521 | cc.used = true; // mark clause used |
522 | if (showStuff) { |
523 | log(indent(level()) + text); |
524 | log(indent(level()) + " Clause unifies to: " + render(c)); |
525 | } |
526 | Goal gdash; |
527 | if (c.nat != null) { |
528 | if (showStuff) |
529 | log(indent(level()) + " Clause is native."); |
530 | if (!c.nat.yo(this, c.head)) { |
531 | if (showStuff) |
532 | log(indent(level()) + "Native clause fails"); |
533 | ret false; |
534 | } |
535 | gdash = e.goal.cdr; |
536 | } else |
537 | gdash = c.body == null ? e.goal.cdr : resolveCut(c.body).append(e.goal.cdr); |
538 | if (showStuff) |
539 | log(indent(level()) + " gdash: " + render(gdash)); |
540 | |
541 | if (gdash == null) { |
542 | if (showStuff) |
543 | log("SUCCESS!"); |
544 | ret true; |
545 | } else { |
546 | Entry e2 = new Entry(gdash); |
547 | /*if (showStuff) |
548 | log(indent(level()) + "New goal: " + render(gdash));*/ |
549 | stackAdd(e2); |
550 | ret false; |
551 | } |
552 | } /*else |
553 | if (showStuff) |
554 | log(indent(level()) + "No match for clause.");*/ |
555 | |
556 | ret false; |
557 | } |
558 | |
559 | // resolve cut in clause body |
560 | Goal resolveCut(Goal g) { |
561 | if (g.car.is("!", 0)) |
562 | ret fixCut(g); |
563 | if (g.cdr == null) |
564 | ret g; |
565 | ret new Goal(g.car, resolveCut(g.cdr)); |
566 | } |
567 | |
568 | // note stack length in cut |
569 | Goal fixCut(Goal g) { |
570 | ret new Goal(lisp("!", lstr(stack)), g.cdr); // max. one cut per clause |
571 | } |
572 | |
573 | void stackAdd(Entry e) { |
574 | stack.add(e); |
575 | int n = l(stack); |
576 | if (n > maxLevel) fail("Maximum stack level reached: " + n); |
577 | if (n > maxLevelSeen) maxLevelSeen = n; |
578 | } |
579 | |
580 | void addClause(S text) { |
581 | addClause(nlParse(text)); |
582 | } |
583 | |
584 | void addClause(Lisp c) { |
585 | addClause(clause(c)); |
586 | } |
587 | |
588 | void addClause(Lisp c, S name) { |
589 | addClause(clause(c), name); |
590 | } |
591 | |
592 | void addClause(Clause c) { |
593 | addClause(c, null); |
594 | } |
595 | |
596 | void addClause(Clause c, S name) { |
597 | c.loadedFrom = name; |
598 | program.add(c); |
599 | if (c.head instanceof Var) { |
600 | if (showStuff) |
601 | log("WARNING: Clause is variable, will not be executed right now: " + c); |
602 | ret; |
603 | } |
604 | int arity = c.head.size(); |
605 | while (arity >= l(programByArity)) |
606 | programByArity.add(new L); |
607 | programByArity.get(arity).add(c); |
608 | } |
609 | |
610 | boolean canSolve(Lisp goal) { |
611 | ret canSolve(new Goal(prologify(goal))); |
612 | } |
613 | |
614 | boolean canSolve(Goal goal) { |
615 | start(goal); |
616 | while (!done()) |
617 | if (step()) |
618 | ret true; |
619 | ret false; |
620 | } |
621 | |
622 | // return variable map or null if unsolved |
623 | Map<S, Lisp> solve(Lisp goal) { |
624 | start(goal); |
625 | |
626 | ret nextSolution(); |
627 | } |
628 | |
629 | Map<S, Lisp> solve(S text) { |
630 | ret solve(nlParse(text)); |
631 | } |
632 | |
633 | Map<S, Lisp> getUserVarMap() { |
634 | Goal g = stack.get(0).goal; |
635 | if (showStuff) |
636 | log("UserVarMap goal: " + g); |
637 | new HashMap<S, Lisp> map; |
638 | for (Var v : findVars(g)) |
639 | if (v.isUserVar()) { |
640 | Lisp term = resolve(v); |
641 | boolean ok = !(term instanceof Var) || (term != v && ((Var) term).isUserVar()); |
642 | if (showStuff) |
643 | log("UserVarMap var " + v + " ok: " + ok); |
644 | if (ok) |
645 | map.put(v.getName(), term); |
646 | } |
647 | ret map; |
648 | } |
649 | |
650 | Map<S, Lisp> nextSolution() { |
651 | if (showStuff) |
652 | log("nextSolution"); |
653 | int n = 0; |
654 | while (!done()) { |
655 | ++n; |
656 | if (step()) { |
657 | if (showStuff) |
658 | log(" solution found in step " + n); |
659 | ret getUserVarMap(); |
660 | } |
661 | } |
662 | if (showStuff) |
663 | log("\nNo solution"); |
664 | ret null; |
665 | } |
666 | |
667 | void addTheory(S text, S name) { |
668 | for (Clause c : parseProgram(text)) |
669 | addClause(c, name); |
670 | } |
671 | |
672 | void addTheory(S text, Lisp tree) { |
673 | addTheory(text, tree, null); |
674 | } |
675 | |
676 | void addTheory(S text, Lisp tree, S name) { |
677 | for (Clause c : parseProgram(text, tree)) |
678 | addClause(c, name); |
679 | } |
680 | |
681 | L<Clause> parseProgram(S text) { |
682 | ret parseProgram(text, nlParse(text)); |
683 | } |
684 | |
685 | L<Clause> parseProgram(S text, Lisp tree) { |
686 | new L<Clause> l; |
687 | if (nlIsMultipleStatements(text)) |
688 | for (Lisp part : tree) |
689 | l.add(clause(part)); |
690 | else |
691 | l.add(clause(tree)); |
692 | ret l; |
693 | } |
694 | |
695 | // shouldn't use anymore |
696 | boolean goNative(Lisp term) { |
697 | term = resolve(term); |
698 | |
699 | for (Native n : natives) { |
700 | Trail t = Trail_Note(); |
701 | boolean result; |
702 | try { |
703 | result = n.yo(this, term); |
704 | } catch (Exception e) { |
705 | Trail_Undo(t); |
706 | continue; |
707 | } |
708 | if (!result) { |
709 | Trail_Undo(t); |
710 | continue; |
711 | } |
712 | ret true; |
713 | } |
714 | |
715 | ret false; |
716 | } |
717 | |
718 | // Resolve top-level only |
719 | Lisp resolve1(Lisp term) { |
720 | if (term instanceof Var) |
721 | ret ((Var) term).getValue(); |
722 | ret term; |
723 | } |
724 | |
725 | // resolve all variables |
726 | Lisp resolve(Lisp term) { |
727 | term = resolve1(term); |
728 | |
729 | // smart recurse |
730 | for (int i = 0; i < term.size(); i++) { |
731 | Lisp l = term.get(i); |
732 | Lisp r = resolve(l); |
733 | if (l != r) { |
734 | Lisp x = new Lisp(term.head); |
735 | for (int j = 0; j < i; j++) |
736 | x.add(term.get(j)); |
737 | x.add(r); |
738 | for (i++; i < term.size(); i++) |
739 | x.add(resolve(term.get(i))); |
740 | ret x; |
741 | } |
742 | } |
743 | |
744 | ret term; |
745 | } |
746 | |
747 | // looks for a bodyless rule in the program that matches the term |
748 | // todo: eqic |
749 | boolean containsStatement(Lisp term) { |
750 | for (Clause c : program) |
751 | if (c.body == null && c.nat == null && eq(c.head, term)) |
752 | ret true; |
753 | ret false; |
754 | } |
755 | |
756 | // closed == contains no variables |
757 | boolean isClosedTerm(Lisp term) { |
758 | if (term instanceof Var) |
759 | ret false; |
760 | else |
761 | for (Lisp arg : term) |
762 | if (!isClosedTerm(arg)) |
763 | ret false; |
764 | ret true; |
765 | } |
766 | |
767 | void addNative(Native n) { |
768 | if (n instanceof BaseNative) |
769 | addNative(((BaseNative) n).pat, n); |
770 | else |
771 | natives.add(n); |
772 | } |
773 | |
774 | void addNatives(Native... l) { |
775 | for (Native n : l) |
776 | addNative(n); |
777 | } |
778 | |
779 | void addNatives(L<Native> l) { |
780 | for (Native n : l) |
781 | addNative(n); |
782 | } |
783 | |
784 | void addNative(S text, Native n) { |
785 | addClause(prologify(new Clause(nlParse(text), n)), "nat"); |
786 | } |
787 | |
788 | L<Lisp> getStackTerms() { |
789 | new L<Lisp> l; |
790 | for (Entry e : stack) |
791 | l.add(e.goal.car); |
792 | ret l; |
793 | } |
794 | |
795 | void logOn() { |
796 | log = new L; |
797 | showStuff = true; |
798 | } |
799 | |
800 | static abstract class BaseNative implements Native { |
801 | S pat; |
802 | Prolog p; |
803 | Map<S, Lisp> m; |
804 | |
805 | *(S *pat) {} |
806 | |
807 | abstract boolean yo(); |
808 | |
809 | public boolean yo(Prolog p, Lisp term) { |
810 | m = new HashMap; |
811 | this.p = p; |
812 | try { |
813 | // Terms are always resolved for native code! |
814 | ret nlMatch(pat, p.resolve(term), m) && yo(); |
815 | } catch (Exception e) { |
816 | ++p.exceptions; |
817 | if (p.showStuff) |
818 | p.log("Exception in native class " + getClass().getName() + ": " + getStackTrace(e)); |
819 | ret false; |
820 | } finally { |
821 | this.p = null; |
822 | } |
823 | } |
824 | |
825 | boolean unify(S var, Lisp term) { |
826 | ret set(var, term); |
827 | } |
828 | |
829 | boolean set(S var, Lisp term) { |
830 | Lisp v = m.get(var); |
831 | if (v == null) |
832 | fail("Variable " + var + " not found"); |
833 | ret p.unify(v, term); |
834 | } |
835 | |
836 | boolean unifyForeign(IdentityHashMap<Lisp, S> varMap, Map<S, Lisp> solution) { |
837 | if (p.showStuff) |
838 | p.log("unifyForeign with: " + structure(solution)); |
839 | for (Lisp v : varMap.keySet()) { |
840 | S name = varMap.get(v); |
841 | Lisp value = solution.get(name); |
842 | if (value == null) continue; |
843 | if (!p.unify(v, escapeVariables(value))) { |
844 | ret false; // rollback? |
845 | } |
846 | } |
847 | ret true; |
848 | } |
849 | |
850 | // fills varMap |
851 | Lisp exportVars(Lisp tree, IdentityHashMap<Lisp, S> varMap) { |
852 | if (tree instanceof Var) { |
853 | S name = varMap.get(tree); |
854 | if (name == null) { |
855 | name = "$_" + (varMap.size()+1); |
856 | varMap.put(tree, name); |
857 | } |
858 | ret lisp(name); |
859 | } |
860 | |
861 | Lisp lisp = new Lisp(tree.head); |
862 | for (Lisp sub : tree) |
863 | lisp.add(exportVars(sub, varMap)); |
864 | ret lisp; |
865 | } |
866 | |
867 | // var = without $ |
868 | Lisp get(S var) { |
869 | ret m.get(var); |
870 | } |
871 | |
872 | S unq(S var) { |
873 | ret m.get(var).unq(); |
874 | } |
875 | } // BaseNative |
876 | |
877 | // Prolog constructor |
878 | *() { |
879 | addClause(lisp("true")); |
880 | addBaseNatives(); |
881 | } |
882 | |
883 | static class State { |
884 | Trail trail; |
885 | L<Entry> stack; |
886 | } |
887 | |
888 | State saveState() { |
889 | new State s; |
890 | s.trail = sofar; |
891 | s.stack = stack; |
892 | sofar = null; |
893 | ret s; |
894 | } |
895 | |
896 | void restoreState(State s) { |
897 | sofar = s.trail; |
898 | stack = s.stack; |
899 | } |
900 | |
901 | L<Lisp> rewriteWith(L<Clause> rewriteTheory) { |
902 | new L<Lisp> result; |
903 | |
904 | for (Prolog.Clause clause : rewriteTheory) { |
905 | if (clause.body == null) continue; // need conditions to rewrite anything |
906 | Prolog.Clause c = clause.copy(); |
907 | State state = saveState(); |
908 | try { |
909 | start(c.body); |
910 | while (!done()) { |
911 | if (step()) { |
912 | Lisp term = resolve(c.head); |
913 | if (!isClosedTerm(term)) { |
914 | if (showStuff) |
915 | log("Not a closed term, skipping: " + term); |
916 | continue; |
917 | } |
918 | |
919 | if (containsStatement(term)) { |
920 | if (showStuff) |
921 | log("Statement exists, skipping: " + term); |
922 | continue; |
923 | } |
924 | |
925 | if (result.contains(term)) |
926 | continue; |
927 | |
928 | if (showStuff) |
929 | log("Found new statement: " + term); |
930 | result.add(term); |
931 | } |
932 | } |
933 | } finally { |
934 | restoreState(state); |
935 | } |
936 | } |
937 | |
938 | ret result; |
939 | } |
940 | |
941 | static class NewCollector extends BaseNative { |
942 | *() { super("$x = new collector"); } |
943 | |
944 | boolean yo() { |
945 | ret set("x", new Collector); |
946 | } |
947 | } |
948 | |
949 | class Save extends BaseNative { |
950 | *() { super("saveTo($x, $collector)"); } |
951 | |
952 | boolean yo() { |
953 | Collector collector = (Collector) get("collector"); |
954 | Lisp x = get("x"); |
955 | collector.solutions.add(resolve(x)); |
956 | ret true; |
957 | } |
958 | } |
959 | |
960 | static class Retrieve extends BaseNative { |
961 | *() { super("$x = retrieve($collector)"); } |
962 | |
963 | boolean yo() { |
964 | print("Retrieve: collector = " + get("collector")); |
965 | Collector collector = (Collector) get("collector"); |
966 | ret set("x", nlList(collector.solutions)); |
967 | } |
968 | } |
969 | |
970 | void addBaseNatives() { |
971 | addNatives(new NewCollector, new Save, new Retrieve); |
972 | } |
973 | |
974 | static Lisp escapeVariables(Lisp tree) { |
975 | if (tree instanceof Var) { |
976 | S name = ((Var) tree).prettyName(); |
977 | ret lisp("[]", "var", name); |
978 | } |
979 | |
980 | Lisp lisp = new Lisp(tree.head); |
981 | for (Lisp sub : tree) |
982 | lisp.add(escapeVariables(sub)); |
983 | ret lisp; |
984 | } |
985 | |
986 | boolean addClauseIfNew(Lisp clause, S name) { |
987 | if (containsStatement(clause)) ret false; |
988 | addClause(clause, name); |
989 | ret true; |
990 | } |
991 | |
992 | L<Clause> getUsedClauses() { |
993 | new L<Clause> l; |
994 | for (Clause c : program) |
995 | if (c.used) |
996 | l.add(c); |
997 | ret l; |
998 | } |
999 | |
1000 | L<S> getUsedTheories() { |
1001 | new TreeSet<S> theories; |
1002 | for (Clause c : getUsedClauses()) |
1003 | theories.add(or(c.loadedFrom, "?")); |
1004 | ret asList(theories); |
1005 | } |
1006 | |
1007 | void think(Lisp x) { |
1008 | addClauseIfNew(x, "thought"); // TODO: vars and stuff? |
1009 | } |
1010 | |
1011 | L<Lisp> getMemorizedStatements() { |
1012 | new L<Lisp> l; |
1013 | for (Clause c : program) |
1014 | if (c.body == null && c.nat == null && c.head.is("[]", 2) && c.head.get(0).is("memorized")) |
1015 | l.add(c.head); |
1016 | ret l; |
1017 | } |
1018 | |
1019 | S showClause(Clause c) { |
1020 | ret nlUnparse(c.head) + (c.body == null ? "" : " :- ..."); |
1021 | } |
1022 | |
1023 | S showProgram() { |
1024 | new L<S> l; |
1025 | for (Clause c : program) |
1026 | l.add(showClause(c)); |
1027 | ret n(l(program), "statement") + " " + slackSnippet(joinLines(l )); |
1028 | } |
1029 | } // class Prolog |
Began life as a copy of #1002862
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: | #1002868 |
Snippet name: | class Prolog with list comprehensions (LIVE) |
Eternal ID of this version: | #1002868/1 |
Text MD5: | 4e206c7a59296de7dd40ddb7f5b957e9 |
Author: | stefan |
Category: | javax |
Type: | JavaX fragment (include) |
Public (visible to everyone): | Yes |
Archived (hidden from active list): | No |
Created/modified: | 2016-03-14 17:31:06 |
Source code size: | 24361 bytes / 1029 lines |
Pitched / IR pitched: | No / No |
Views / Downloads: | 715 / 693 |
Referenced in: | [show references] |