Warning: session_start(): open(/var/lib/php/sessions/sess_sm3i4n416ldlb2u8rnnhn5hqi1, O_RDWR) failed: No space left on device (28) in /var/www/tb-usercake/models/config.php on line 51
Warning: session_start(): Failed to read session data: files (path: /var/lib/php/sessions) in /var/www/tb-usercake/models/config.php on line 51
!752
static class Prolog {
boolean upperCaseVariables = false; // true for SNL, false for NL
long varCount;
boolean showStuff;
new L stack;
Trail sofar = null;
new L program;
long steps;
new L 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(copy2(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 vars;
*(L *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(/* XXX copy2(car) XXX */ 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;
}
ret copy2(thiz);
}
Lisp newTermCons(Lisp t) {
Lisp l = new Lisp(t.head);
for (Lisp arg : t)
l.add(copy(arg));
ret l;
}
Lisp copy2(Lisp thiz) {
return newTermCons(thiz);
}
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 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 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 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 findVars(Goal g) {
new IdentityHashMap map;
while (g != null) {
findVars(g.car, map);
g = g.cdr;
}
ret asList(map.keySet());
}
L findVars(Lisp term) {
new IdentityHashMap map;
findVars(term, map);
ret asList(map.keySet());
}
void findVars(Lisp term, IdentityHashMap map) {
if (term instanceof Var)
map.put((Var) term, Boolean.TRUE);
else
for (Lisp arg : term)
findVars(arg, map);
}
static Map makeVarMap(L vars) {
new HashMap 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) {
program.add(clause(c));
}
void addClause(Clause c) {
program.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 solve(Lisp goal) {
Goal g = new Goal(prologify(goal));
if (!canSolve(g))
ret null;
ret getUserVarMap();
}
Map getUserVarMap() {
Goal g = stack.get(0).goal;
new HashMap map;
for (Var v : findVars(g))
if (v.isUserVar())
map.put(v.getName(), v.getValue());
ret map;
}
Map nextSolution() {
while (!done())
if (step())
ret getUserVarMap();
ret null;
}
void addClauses(Lisp tree) {
if (nlIsMultipleStatements(tree))
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;
}
// 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 getStackTerms() {
new L l;
for (Entry e : stack)
l.add(e.goal.car);
ret l;
}
} // class Prolog