!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
Began life as a copy of #1002857
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: | #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: | 604 / 555 |
Referenced in: | [show references] |