// do NOT initialize in static field 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; L<S> log; int maxLogSize = 1000; // lines int maxLevel = 10000; // max stack size int timeLimit = 20; // 20 seconds long startTime; boolean allowEval = true; int defaultRewriteMax = 100; // name of theory to memorize stuff to S outTheory; // stats int maxLevelSeen; // maximum stack level reached during computation long topUnifications, exceptions; static interface INative { public boolean yo(Prolog p, Lisp term); } // CENTRAL method for comparing terms // change for modifying case-sensitivity. 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 prettyName(); } S prettyName() { 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; } } static class LCollector extends Lisp { new L<Lisp> solutions; *() { super("___"); } public S toString() { ret "<collector>"; } } static class Clause { Lisp head; S loadedFrom; // theory name boolean used; // Either body or nat will be set (or none) INative nat; Goal body; *(Lisp *head, INative *nat) {} *(Lisp *head, Goal *body) {} *(Lisp *head, Goal *body, INative *nat) {} *(Lisp *head) {} Clause copy(Prolog p) { ret new Clause(p.copy(head), body == null ? null : body.copy(p), nat); } public String toString() { //ret head + " :- " + (body == null ? "true" : body); ret nat != null ? head + " :- native" : (body == null ? head.toString() : head + " :- " + body); } // fails if clause is a rule Lisp getStatement() { if (nat != null || body != null) fail("Not a statement: " + this); ret head; } } class Trail { Var tcar; Trail tcdr; *(Var *tcar, Trail *tcdr) {} } Trail Trail_Note() { return sofar; } void Trail_Set(Var x, Lisp value) { sofar = new Trail(x, sofar); x.instance = value; /*if (showStuff) log(indent(level()) + " Push " + x.prettyName() + " (" + x + ")");*/ } void Trail_Undo(Trail whereto) { for (; sofar != whereto; sofar = sofar.tcdr) { /*if (showStuff) log(indent(level()) + " Resetting variable " + sofar.tcar.prettyName() + " (" + sofar.tcar + ")");*/ 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.prettyName() + " = " + v); } } static class Goal { Lisp car; Goal cdr; *(Lisp *car, Goal *cdr) {} *(Lisp *car) {} public String toString() { ret cdr == null ? car.toString() : car + "; " + cdr; } Goal copy(Prolog p) { return new Goal(p.copy(car), cdr == null ? null : cdr.copy(p)); } 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_Set(v, 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_Set(v, 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)); } // primary processor for freshly parsed rules Clause clause(Lisp rule) { L<Lisp> ops = snlSplitOps(rule); /*if (showStuff) log("clause(Lisp): " + rule + " => " + structure(ops)); */ // expand rule shortcuts (say/memorize/...) for (int i = 0; i < l(ops)-1; i++) if (ops.get(i).is("memorize *")) ops.set(i, lisp("and *", lisp("[]", "memorize", ops.get(i)))); if (!empty(ops) && last(ops).is("say *")) ops.set(l(ops)-1, lisp("then *", lisp("[]", "say", last(ops).get(0)))); rule = empty(ops) ? rule : snlJoinOps(ops); if (allowEval) rule = new EvalTransform().evalTransformRule(rule); ops = snlSplitOps(rule); 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)); } // Note: only for un-prologified boolean isVar(Lisp term) { ret upperCaseVariables ? snlIsVar(term) : nlIsVar(term); } // for prologified (e.g. in native clauses) boolean isLiveVar(Lisp term) { ret term instanceof Var; } 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 = 0; 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(); program = arity >= l(programByArity) ? emptyProgram : programByArity.get(arity); if (showStuff) log(indent(level()) + "Goal arity " + arity + ": " + render(car) + ", have " + n2(program, "fact") + " of this arity"); } } } void start(S goal) { start(nlParse(goal)); } void start(Lisp goal) { start(new Goal(prologify(goal))); } S render(Lisp term) { ret nlUnparse(resolve(term)); } S render(Goal goal) { ret goal == null ? "-" : render(goal.car); } S render(Clause c) { ret c == null ? "-" : render(c.head); } // warning: doesn't prologify the goal void start(Goal goal) { if (showStuff) log("Starting on goal: " + render(goal)); steps = 0; stack = new L; Trail_Undo(null); stackAdd(new Entry(goal)); startTime = sysNow(); } void log(S s) { if (log != null) { if (l(log) == maxLogSize) { log.add("[Log overflow]"); showStuff = false; } 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() { ping(); if (done()) fail("done!"); // safety if (sysNow() >= 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; } // now in program loop - get next clause to try Clause cc = e.program.get(e.programIdx); ++e.programIdx; // copy the clause; synchronize on it because it may come // from a shared Prolog interpreter Clause c; synchronized(cc) { c = cc.copy(this); Trail_Undo(e.trail); } S text = null; if (showStuff) //text = " Goal: " + e.goal + ". Got clause: " + c; text = "Got clause: " + render(c); ++topUnifications; if (unify(e.goal.car, c.head)) { cc.used = true; // mark clause used if (showStuff) { log(indent(level()) + text); log(indent(level()) + " Clause unifies to: " + render(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: " + render(gdash)); if (gdash == null) { if (showStuff) log("SUCCESS!"); ret true; } else { Entry e2 = new Entry(gdash); /*if (showStuff) log(indent(level()) + "New goal: " + render(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 addClauses(L<Lisp> l) { for (Lisp clause : unnull(l)) addClause(clause); } // synonym of addClause void addStatement(S text) { addClause(text); } void addClause(Lisp c) { addClause(clause(c)); } void addClause(Lisp c, S name) { addClause(clause(c), name); } void addClause(Clause c) { addClause(c, null); } void addClause(Clause c, S name) { c.loadedFrom = name; program.add(c); if (c.head instanceof Var) { if (showStuff) log("WARNING: Clause is variable, will not be executed right now: " + c); ret; } int arity = c.head.size(); growArityList(arity); programByArity.get(arity).add(c); } void growArityList(int arity) { while (arity >= l(programByArity)) programByArity.add(new L); } boolean canSolve(Lisp goal) { ret canSolve(new Goal(prologify(goal))); } boolean canSolve(S goal) { ret canSolve(nlParse(goal)); } boolean canSolve(Goal goal) { start(goal); while (!done()) if (step()) ret true; ret false; } S solveAsText(S goal, S var) { Map<S, Lisp> solution = solve(goal); ret solution == null ? null : nlUnparse(solution.get(addPrefix("$", var))); } // return variable map or null if unsolved Map<S, Lisp> solve(Lisp goal) { start(goal); ret nextSolution(); } Map<S, Lisp> solve(S text) { ret solve(nlParse(text)); } Map<S, Lisp> getUserVarMap() { Goal g = stack.get(0).goal; if (showStuff) log("UserVarMap goal: " + g); new HashMap<S, Lisp> map; for (Var v : findVars(g)) if (v.isUserVar()) { Lisp term = resolve(v); boolean ok = !(term instanceof Var) || (term != v && ((Var) term).isUserVar()); if (showStuff) log("UserVarMap var " + v + " ok: " + ok); if (ok) map.put(v.getName(), term); } 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("\nNo solution"); ret null; } void code(S text) { addTheory(text, "ad hoc"); } void addTheory(S text, S name) { for (Clause c : parseProgram(text)) addClause(c, name); } void addTheory(S text, Lisp tree) { addTheory(text, tree, null); } void addTheory(S text, Lisp tree, S name) { for (Clause c : parseProgram(text, tree)) addClause(c, name); } L<Clause> parseProgram(S text) { ret parseProgram(text, nlParse(text)); } L<Clause> parseProgram(S text, Lisp tree) { new L<Clause> l; if (nlIsMultipleStatements(text)) for (Lisp part : tree) l.add(clause(part)); else l.add(clause(tree)); ret l; } L<Lisp> parseStatements(S text) { ret map(func(Clause c) { c.getStatement() }, parseProgram(text)); } // 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(BaseNative n) { addClause(prologify(new Clause(nlParse(n.pat), n)), "nat"); } void addNatives(BaseNative... l) { for (BaseNative n : l) addNative(n); } void addNatives(L<BaseNative> l) { for (BaseNative n : l) addNative(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 INative { 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 { // Terms are always resolved for native code! ret nlMatch(pat, p.resolve(term), m) && yo(); } catch (Exception e) { ++p.exceptions; if (p.showStuff) p.log("Exception in native class " + getClass().getName() + ": " + getStackTrace(e)); ret false; } finally { this.p = null; } } boolean unify(S var, Lisp term) { ret set(var, term); } boolean set(S var, Lisp term) { Lisp v = m.get(var); if (v == null) fail("Variable " + var + " not found"); ret p.unify(v, term); } boolean unifyForeign(IdentityHashMap<Lisp, S> varMap, Map<S, Lisp> solution) { if (p.showStuff) p.log("unifyForeign with: " + structure(solution)); for (Lisp v : varMap.keySet()) { S name = varMap.get(v); Lisp value = solution.get(name); if (value == null) continue; if (!p.unify(v, escapeVariables(value))) { ret false; // rollback? } } ret true; } // fills varMap Lisp exportVars(Lisp tree, IdentityHashMap<Lisp, S> varMap) { if (tree instanceof Var) { S name = varMap.get(tree); if (name == null) { name = "$_" + (varMap.size()+1); varMap.put(tree, name); } ret lisp(name); } Lisp lisp = new Lisp(tree.head); for (Lisp sub : tree) lisp.add(exportVars(sub, varMap)); ret lisp; } // var = without $ Lisp get(S var) { ret m.get(var); } S unq(S var) { ret m.get(var).unq(); } } // BaseNative // Prolog constructor *() { addClause(lisp("true")); addBaseNatives(); } *(Prolog p) { copyProgramFrom(p); } static class State { Trail trail; L<Entry> stack; } State saveState() { new State s; s.trail = sofar; s.stack = stack; sofar = null; ret s; } void restoreState(State s) { sofar = s.trail; stack = s.stack; } // auto-rewrite with all clauses in DB L<Lisp> rewrite() { ret rewriteWith(program, defaultRewriteMax); } L<Lisp> rewrite(int max) { ret rewriteWith(program, max); } // Note: rewriteTheory is not searched for facts (only rules) L<Lisp> rewriteWith(Prolog rewriteTheory) { ret rewriteWith(rewriteTheory.program()); } L<Lisp> rewriteWith(L<Clause> rewriteTheory) { ret rewriteWith(rewriteTheory, defaultRewriteMax); } L<Lisp> rewriteWith(L<Clause> rewriteTheory, int max) { new L<Lisp> l; rewriteWithInto(rewriteTheory, limitedListCollector(l, max)); ret l; } void rewriteInto(Collector<Lisp> collector) { rewriteWithInto(program, collector); } void rewriteWithInto(L<Clause> rewriteTheory, Collector<Lisp> collector) { if (collector.full()) ret; for (Prolog.Clause clause : rewriteTheory) { if (clause.body == null) continue; // need conditions to rewrite anything // usual safe clause copying Trail t = Trail_Note(); Clause c; synchronized(clause) { c = clause.copy(this); Trail_Undo(t); } State state = saveState(); try { start(c.body); while (!done()) { if (step()) { Lisp term = resolve(c.head); if (!isClosedTerm(term)) { if (showStuff) log("Not a closed term, skipping: " + term); continue; } if (containsStatement(term)) { if (showStuff) log("Statement exists, skipping: " + term); continue; } if (collector.contains(term)) continue; if (showStuff) log("Found new statement: " + term); collector.add(term); if (collector.full()) { log("Collector full"); break; } } } } finally { restoreState(state); } } } static class NewCollector extends BaseNative { *() { super("$x = new collector"); } boolean yo() { ret set("x", new LCollector); } } class Save extends BaseNative { *() { super("saveTo($x, $collector)"); } boolean yo() { LCollector collector = (LCollector) get("collector"); Lisp x = get("x"); collector.solutions.add(resolve(x)); ret true; } } static class Retrieve extends BaseNative { *() { super("$x = retrieve($collector)"); } boolean yo() { print("Retrieve: collector = " + get("collector")); LCollector collector = (LCollector) get("collector"); ret set("x", nlList(collector.solutions)); } } void addBaseNatives() { addNatives(new NewCollector, new Save, new Retrieve); } static Lisp escapeVariables(Lisp tree) { if (tree instanceof Var) { S name = ((Var) tree).prettyName(); ret lisp("[]", "var", name); } Lisp lisp = new Lisp(tree.head); for (Lisp sub : tree) lisp.add(escapeVariables(sub)); ret lisp; } boolean addClauseIfNew(Lisp clause, S name) { if (containsStatement(clause)) ret false; addClause(clause, name); ret true; } L<Clause> getUsedClauses() { new L<Clause> l; for (Clause c : program) if (c.used) l.add(c); ret l; } L<S> getUsedTheories() { new TreeSet<S> theories; for (Clause c : getUsedClauses()) theories.add(or(c.loadedFrom, "?")); ret asList(theories); } void think(Lisp x) { addClauseIfNew(x, "thought"); // TODO: vars and stuff? } L<Lisp> getMemorizedStatements() { new L<Lisp> l; for (Clause c : program) if (c.body == null && c.nat == null && c.head.is("[]", 2) && c.head.get(0).is("memorized")) l.add(c.head); ret l; } S showClause(Clause c) { ret nlUnparse(c.head) + (c.body == null ? "" : " :- ..."); } S showProgram() { new L<S> l; for (Clause c : program) l.add(showClause(c)); ret n(l(program), "statement") + " " + slackSnippet(joinLines(l )); } void copyProgramFrom(Prolog p) { program.addAll(p.program); growArityList(l(p.programByArity)); for (int i = 0; i < l(p.programByArity); i++) programByArity.get(i).addAll(p.programByArity.get(i)); } void addProgram(L<Clause> clauses, S loadedFrom) { for (Clause c : clauses) addClause(c, loadedFrom); } void addClauses(S text) { addTheory(text, fsI(programID())); } L<S> statementsAsText() { ret statementsAsText(0); } L<S> statementsAsText(int startingFromIndex) { new L<S> l; for (int i = startingFromIndex; i < l(program); i++) { Clause c = program.get(i); if (c.nat == null) { if (c.body != null) l.add("[if ? then " + nlUnparse(c.head, false) + "]"); // TODO else l.add(nlUnparse(c.head, false)); } } ret l; } int mark() { ret l(program); } L<Clause> program() { ret program; } L<Lisp> rewriteAndSave() { L<Lisp> l = rewrite(); addClauses(l); ret l; } } // class Prolog
Began life as a copy of #1002868
download show line numbers debug dex old transpilations
Travelled to 14 computer(s): aoiabmzegqzx, bhatertpkbcr, cbybwowwnfue, cfunsshuasjs, gwrvuhgaqvyk, ishqpsrjomds, lpdgvwnxivlt, mqqgnosmbjvj, onxytkatvevr, pyentgdyhuwx, pzhvpgtvlbxg, tslmcundralx, tvejysmllsmz, vouqrxazstgt
No comments. add comment