// $Id: Euler.cs,v 1.25 2003/09/29 23:24:21 jderoo Exp $
// PxButton | build | csc /o /doc:Euler.xml *.cs |
// PxButton | builddll | csc /o /doc:Euler.xml /t:library /out:EulerSharp.dll *.cs |
// PxButton | build2 | cscc -g *.cs -l /PNET/lib/cscc/lib/System.dll -l /PNET/lib/cscc/lib/System.Xml.dll && del Euler.exe && ren a.out.exe Euler.exe |
using System;
using System.Collections;
using System.IO;
using System.Net.Sockets;
using System.Text;
using System.Xml;
/// Euler proof mechanism
/// Jos De Roo
public class Euler {
internal Euler subj = null; // RDF subject
internal String verb = null; // RDF predicate as absoluteized verb
internal Euler obj = null; // RDF object
internal String cverb = null; // compact verb
internal int varid = - 1; // variable id
internal bool bound = false; // variable binding state
internal bool vv = false; // variable verb state
internal Euler refr = null; // to be dereferenced
internal Euler premis = null; // to attach the premis
internal Euler near = null; // to construct a conjunction
internal Euler far; // to remember last clause
internal Hashtable ns = null; // to table namespaces
internal Hashtable nsp = null; // to table namespace prefixes
internal Hashtable syn = null; // to table synonyms
internal Hashtable dds = null; // to table log:definitiveDocument and Service properties
internal int varmax = 0; // maximum variable count
internal String baseURI = ""; // URI of base process
internal Hashtable loaded = null; // to table document/engine pairs
internal long engine = 1; // number of engines
internal const String version = "R3588";
internal const String Elabel = "label";
internal const String Etrace = "trace";
internal const String IW = "constructs a proof engine
public Euler() {
far = this;
}
/// loads all facts and rules acquired from the RDF URI in that proof engine
/// of the RDF resource
public virtual void Load(String uri) {
lock(this) {
root = this;
if (loaded == null) loaded = new Hashtable();
if (loaded['<' + uri + '>'] != null) return;
String rk = fromWeb(uri);
String u = baseURI;
if (!uri.StartsWith("data:")) loaded['<' + baseURI + '>'] = this;
ArrayList vt = new ArrayList();
Parser np = new Parser(rk, vt, this, u);
if (ns == null) {
ns = new Hashtable();
nsp = new Hashtable();
syn = new Hashtable();
dds = new Hashtable();
ns["rdfs:"] = RDFS + "#>";
ns["log:"] = LOG + "#>";
ns["iw:"] = IW + "#>";
}
StringBuilder gen = new StringBuilder("data:,");
if (debug || trace) Console.Error.WriteLine("load " + uri);
while (true) {
far.near = np.Parse();
if (far.near == null) break;
while (far.near != null) {
if (far.near.verb.Equals(LOGforAll)) {
if (far.near.subj.subj == null && far.near.subj.obj == null) {
if (!vt.Contains(far.near.obj.verb)) vt.Add(far.near.obj.verb);
far.near = far.near.near;
continue;
}
else {
Euler fn = far.near;
ArrayList wt = new ArrayList();
for (IEnumerator e = vt.GetEnumerator(); e.MoveNext(); wt.Add(e.Current));
while (fn != null && fn.verb.Equals(LOGforAll)) {
if (!wt.Contains(fn.obj.verb)) wt.Add(fn.obj.verb);
fn = fn.near;
}
if (wt.Count > varmax) varmax = wt.Count;
far.near.subj.near = fn;
far.near = far.near.subj;
far.near.forX(false, wt);
}
}
rewrite(true, far.near, np);
if (far.near.verb.Equals(LOGimplies)) {
rewrite(false, far.near.subj, np);
far.near.obj.premis = far.near.subj;
if (far.near.obj.varid != -1) {
Euler er = far.near.subj;
while (er.verb.Equals(RDFSfyi) || er.verb.Equals("") || er.verb.Equals(Etrace)) er = er.near;
er.vv = true;
}
Euler fn = far.near;
while (fn.obj.near != null) {
fn.near = np.parse(false, LOGimplies);
fn.near.subj = fn.subj;
fn.near.obj = fn.obj.near;
fn = fn.near;
}
}
else if (far.near.verb.Equals(OWLequivalentClass))
gen.Append(far.near.subj + " " + RDFSsubClassOf + " " + far.near.obj + ". ")
.Append(far.near.obj + " " + RDFSsubClassOf + " " + far.near.subj + ". ");
else if (far.near.verb.Equals(OWLequivalentProperty))
gen.Append(far.near.subj + " " + RDFSsubPropertyOf + " " + far.near.obj + ". ")
.Append(far.near.obj + " " + RDFSsubPropertyOf + " " + far.near.subj + ". ");
else if (far.near.verb.StartsWith(RDF + "#_"))
gen.Append(far.near.verb + " " + RDFSsubPropertyOf + " " + RDFSmember + ". ");
else if (far.near.verb.Equals(LOGdefinitiveDocument) || far.near.verb.Equals(LOGdefinitiveService))
dds[far.near.subj.verb] = far.near.obj.verb;
if (debug || trace) Console.Error.WriteLine("@@ assert " + far.near);
far = far.near;
}
}
syno(this);
String gener = gen.ToString();
if (!gener.Equals("data:,")) this.Load(gener);
if (vt.Count > varmax) varmax = vt.Count;
doc++;
}
}
/// "no proof explanation" mode
public bool Nope
{
get
{
return nope;
}
set
{
nope = value;
}
}
/// "think" mode
public bool Think
{
get
{
return think;
}
set
{
think = value;
}
}
/// prepares that proof engine
public virtual void Prepare() {
lock(this) {
bool ot = think;
long os = step;
think = true;
if (debug || trace) Console.Error.WriteLine("prepare " + baseURI);
Proof("data:,?s " + OWLsameAs + " ?o. ");
step = os;
think = ot;
syno(this);
}
}
/// proofs a conjunction with that proof engine
/// of the RDF resource
/// proof
public virtual String Proof(String uri) {
lock(this) {
root = this;
if (loaded == null) loaded = new Hashtable();
String cj = fromWeb(uri);
String u = baseURI;
ArrayList vt = new ArrayList();
Parser np = new Parser(cj, vt, this, u);
if (ns == null) {
ns = new Hashtable();
this.nsp = new Hashtable();
syn = new Hashtable();
dds = new Hashtable();
ns["rdfs:"] = RDFS + "#>";
ns["log:"] = LOG + "#>";
ns["iw:"] = IW + "#>";
}
StringBuilder gen = new StringBuilder("data:,");
Euler goal = new Euler();
Euler g = goal;
if (debug || trace) Console.Error.WriteLine("proof " + uri);
while (true) {
g.near = np.Parse();
if (g.near == null) break;
while (g.near != null && g.near.verb != null) {
rewrite(true, g.near, np);
if (g.near.verb.Equals(LOGforSome) || g.near.verb.Equals(LOGforAll) || g.near.obj.verb != null && g.near.obj.verb.Equals(LOGTruth)) {
if (g.near.subj.subj == null && g.near.subj.obj == null) {
if (g.near.obj != null && !vt.Contains(g.near.obj.verb)) vt.Add(g.near.obj.verb);
}
else {
Euler fn = g.near;
ArrayList wt = new ArrayList();
for (IEnumerator e = vt.GetEnumerator(); e.MoveNext(); wt.Add(e.Current));
while (fn != null && (fn.verb.Equals(LOGforSome) || fn.verb.Equals(LOGforAll) || fn.obj.verb.Equals(LOGTruth))) {
if ((fn.verb.Equals(LOGforSome) || fn.verb.Equals(LOGforAll)) && !wt.Contains(fn.obj.verb))
wt.Add(fn.obj.verb);
fn = fn.near;
}
if (wt.Count > varmax) varmax = wt.Count;
g.near = g.near.subj;
Euler gn = g;
while (gn.near != null) {
gn.near.forX(false, wt);
gn = gn.near;
}
gn.near = fn;
}
g = g.near;
}
else {
g.near.getX(false, vt);
g.near.forX(false, vt);
if (vt.Count > varmax) varmax = vt.Count;
if (debug || trace) Console.Error.WriteLine("@@ query " + g.near);
g = g.near;
}
if (g.subj.varid != -1 && // @@ comprehension
(g.verb.Equals(RDFtype) && g.obj.verb.Equals(RDFList) ||
g.verb.Equals(RDFfirst) ||
g.verb.Equals(RDFrest) ||
g.verb.Equals(RDFtype) && g.obj.verb.Equals(OWLOntology) ||
g.verb.Equals(RDFtype) && g.obj.verb.Equals(OWLClass) ||
g.verb.Equals(OWLintersectionOf) ||
g.verb.Equals(OWLunionOf) ||
g.verb.Equals(OWLcomplementOf) ||
g.verb.Equals(OWLoneOf) ||
g.verb.Equals(RDFtype) && g.obj.verb.Equals(OWLRestriction) ||
g.verb.Equals(OWLonProperty) ||
g.verb.Equals(OWLallValuesFrom) ||
g.verb.Equals(OWLsomeValuesFrom) ||
g.verb.Equals(OWLhasValue) ||
g.verb.Equals(OWLminCardinality) ||
g.verb.Equals(OWLmaxCardinality) ||
g.verb.Equals(OWLcardinality))) {
if (g.verb.Equals(RDFtype)) g.vv = true;
gen.Append(g);
}
}
}
reorder(goal);
syno(goal);
String gener = gen.ToString();
if (!gener.Equals("data:,")) this.Load(gener);
if (vt.Count > varmax) varmax = vt.Count;
StringBuilder nsp = new StringBuilder(256);
IEnumerator en = (IEnumerator) ns.Keys.GetEnumerator();
while (en.MoveNext()) {
Object nsx = en.Current;
nsp.Append("@prefix ").Append(nsx).Append(' ').Append(ns[nsx]).Append(".\n");
}
nsp.Append('\n');
int tab = 0;
Euler[] vars = new Euler[varmax];
Euler lr = goal.near;
Euler ts = null;
Euler tsb = null;
Euler ts1 = null;
Euler ts2 = null;
Stack stack = new Stack();
bool not = false;
long istep = step;
StringBuilder proof = new StringBuilder(4096);
proof.Append("# Generated with http://www.agfa.com/w3c/euler/#").Append(version);
proof.Append(" on ").Append(DateTime.UtcNow.ToString()).Append("\n");
int pn = 0;
if (!nope) {
proof.Append("{\n (\n");
IEnumerator enu = (IEnumerator) loaded.Keys.GetEnumerator();
while (enu.MoveNext())
proof.Append(' ').Append(enu.Current).Append('.').Append(LOGsemantics).Append("\n");
proof.Append(" ).").Append(LOGconjunction).Append(" =>\n");
proof.Append(" <").Append(baseURI).Append(">.").Append(LOGsemantics).Append("\n}\n");
pn = proof.Length;
proof.Append(WHYbecause).Append("\n{\n");
}
proof.Append(nsp);
int pns = proof.Length;
proof.EnsureCapacity(proof.Length * 2);
StringBuilder pp = new StringBuilder(4096);
StringBuilder pc = new StringBuilder(4096);
StringBuilder pm = new StringBuilder(4096);
Hashtable pct = new Hashtable();
Euler te = goal;
while (te.near != null) {
te.near = te.near.eval(false, vars, stack);
te = te.near;
}
goal = goal.near;
if (trace) Console.Error.WriteLine("[" + step + "]CALL: " + goal);
long t = DateTime.Now.Ticks;
while (true) {
if (goal == null) {
t = DateTime.Now.Ticks - t;
if (proof.Length == pns) {
if (!nope) {
proof.Length = pn;
proof.Append(WHYunknownBecause).Append("\n{\n");
}
proof.Append("# No proof found for ");
}
else {
IEnumerator sen = (IEnumerator) syn.Keys.GetEnumerator();
while (sen.MoveNext()) {
Object sne = sen.Current;
if (sne.Equals(syn[sne])) continue;
proof.Append(sne);
proof.Append(' ');
proof.Append(OWLsameAs);
proof.Append(' ');
proof.Append(syn[sne]);
proof.Append(" .\n");
}
proof.Append("# Proof found for ");
}
proof.Append(u);
proof.Append(" in ").Append(step-istep).Append(step-istep==1?" step":" steps");
proof.Append(" (").Append((long)((step-istep)*10000000L/(t+100))).Append(" steps/sec)"); // @@ 100ns
proof.Append(" using ").Append(engine).Append(engine==1?" engine":" engines");
if (!nope) proof.Append("\n}.\n");
conc = pct;
return proof.ToString();
}
not = false;
try {
if (goal.varid != - 1 && goal.subj != null && goal.obj != null) {
Euler gn = goal.eval(false, vars, stack);
goal.verb = gn.verb;
goal.cverb = gn.cverb;
}
if (goal.verb == null) {
if (goal.obj.verb == OWLsameAs) synon(goal.obj);
tab--;
if (goal.obj.subj.varid != -1 || goal.obj.varid != -1 || goal.obj.obj.varid != -1) {
pp.Append('\n');
for (int i = tab; i >= 0; i--) pp.Append(" ");
goal.obj.whysubst(pp, tab); }
if (pp[pp.Length - 2] == '.' && pp[pp.Length - 1] == ' ') pp[pp.Length - 2] = '}';
else pp.Append('}');
pp.Append(" =>\n");
for (int i = tab; i > 0; i--) pp.Append(" ");
pp.Append('{').Append(goal.obj);
if (pp[pp.Length - 2] == '.' && pp[pp.Length - 1] == ' ') pp.Insert(pp.Length - 2, '}');
else pp.Append("}. ");
if (tab == 0) pc.Append(goal.obj).Append('\n');
}
else if (goal.verb == "" && goal.subj.deref().bound) { // @@ single
pp.Append('\n');
for (int i = tab; i > 0; i--) pp.Append(" ");
pp.Append(getLit(goal.subj)).Append(". ");
}
else if (goal.verb == Etrace) Console.Error.WriteLine("[" + step + "] " + goal);
else if (goal.verb == STRconcatenation) {
Euler el = goal.subj.deref();
StringBuilder sb = new StringBuilder("\"");
while (el.getFirst() != null) {
sb.Append(getLit(el.getFirst().deref()));
el = el.getRest();
}
sb.Append("\"");
Euler er = np.Parse(String.Intern(sb.ToString()));
if (goal.obj.unify(er, this, stack)) {
pp.Append('\n');
for (int i = tab; i > 0; i--) pp.Append(" ");
goal.whysub(pp, tab);
if (tab == 0) pc.Append(goal).Append('\n');;
}
else not = true;
}
else if (goal.verb == STRequalIgnoringCase)
{
String sv = getLit(goal.subj.deref());
String ov = getLit(goal.obj.deref());
if (sv.ToLower().Equals(ov.ToLower()))
{
pp.Append('\n');
for (int i = tab; i > 0; i--) pp.Append(" ");
goal.whysub(pp, tab);
if (tab == 0) pc.Append(goal).Append('\n');
}
else not = true;
}
else if (goal.verb == STRnotEqualIgnoringCase)
{
String sv = getLit(goal.subj.deref());
String ov = getLit(goal.obj.deref());
if (!sv.ToLower().Equals(ov.ToLower()))
{
pp.Append('\n');
for (int i = tab; i > 0; i--) pp.Append(" ");
goal.whysub(pp, tab);
if (tab == 0) pc.Append(goal).Append('\n');
}
else not = true;
}
else if (goal.verb == STRgreaterThan) {
String sv = getLit(goal.subj.deref());
String ov = getLit(goal.obj.deref());
if (sv.CompareTo(ov) > 0) {
pp.Append('\n');
for (int i = tab; i > 0; i--) pp.Append(" ");
goal.whysub(pp, tab);
if (tab == 0) pc.Append(goal).Append('\n');;
}
else not = true;
}
else if (goal.verb == STRnotGreaterThan) {
String sv = getLit(goal.subj.deref());
String ov = getLit(goal.obj.deref());
if (sv.CompareTo(ov) <= 0) {
pp.Append('\n');
for (int i = tab; i > 0; i--) pp.Append(" ");
goal.whysub(pp, tab);
if (tab == 0) pc.Append(goal).Append('\n');
}
else not = true;
}
else if (goal.verb == STRlessThan) {
String sv = getLit(goal.subj.deref());
String ov = getLit(goal.obj.deref());
if (sv.CompareTo(ov) < 0) {
pp.Append('\n');
for (int i = tab; i > 0; i--) pp.Append(" ");
goal.whysub(pp, tab);
if (tab == 0) pc.Append(goal).Append('\n');
}
else not = true;
}
else if (goal.verb == STRnotLessThan) {
String sv = getLit(goal.subj.deref());
String ov = getLit(goal.obj.deref());
if (sv.CompareTo(ov) >= 0) {
pp.Append('\n');
for (int i = tab; i > 0; i--) pp.Append(" ");
goal.whysub(pp, tab);
if (tab == 0) pc.Append(goal).Append('\n');
}
else not = true;
}
else if (goal.verb == STRstartsWith) {
String sv = getLit(goal.subj.deref());
String ov = getLit(goal.obj.deref());
if (sv.StartsWith(ov)) {
pp.Append('\n');
for (int i = tab; i > 0; i--) pp.Append(" ");
goal.whysub(pp, tab);
if (tab == 0) pc.Append(goal).Append('\n');
}
else not = true;
}
else if (goal.verb == STRendsWith) {
String sv = getLit(goal.subj.deref());
String ov = getLit(goal.obj.deref());
if (sv.EndsWith(ov)) {
pp.Append('\n');
for (int i = tab; i > 0; i--) pp.Append(" ");
goal.whysub(pp, tab);
if (tab == 0) pc.Append(goal).Append('\n');
}
else not = true;
}
else if (goal.verb == STRcontains) {
String sv = getLit(goal.subj.deref());
String ov = getLit(goal.obj.deref());
if (sv.IndexOf(ov) != -1) {
pp.Append('\n');
for (int i = tab; i > 0; i--) pp.Append(" ");
goal.whysub(pp, tab);
if (tab == 0) pc.Append(goal).Append('\n');
}
else not = true;
}
else if (goal.verb == STRcontainsIgnoringCase) {
String sv = getLit(goal.subj.deref());
String ov = getLit(goal.obj.deref());
if (sv.ToLower().IndexOf(ov.ToLower()) != -1) {
pp.Append('\n');
for (int i = tab; i > 0; i--) pp.Append(" ");
goal.whysub(pp, tab);
if (tab == 0) pc.Append(goal).Append('\n');
}
else not = true;
}
else if (goal.verb == MATHsum) {
Euler el = goal.subj.deref();
double d = 0;
while (el.getFirst() != null) {
d += Double.Parse(getLit(el.getFirst().deref()));
el = el.getRest();
}
StringBuilder sb = new StringBuilder().Append(nat(goal.subj.deref(), d));
obj = np.Parse(String.Intern(sb.ToString()));
if (goal.obj.unify(obj, this, stack)) {
pp.Append('\n');
for (int i = tab; i > 0; i--) pp.Append(" ");
goal.whysub(pp, tab);
if (tab == 0) pc.Append(goal).Append('\n');
}
else not = true;
}
else if (goal.verb == MATHdifference) {
Euler el = goal.subj.deref();
double d = Double.Parse(getLit(el.getFirst().deref()));
el = el.getRest();
while (el.getFirst() != null) {
d -= Double.Parse(getLit(el.getFirst().deref()));
el = el.getRest();
}
StringBuilder sb = new StringBuilder().Append(nat(goal.subj.deref(), d));
obj = np.Parse(String.Intern(sb.ToString()));
if (goal.obj.unify(obj, this, stack)) {
pp.Append('\n');
for (int i = tab; i > 0; i--) pp.Append(" ");
goal.whysub(pp, tab);
if (tab == 0) pc.Append(goal).Append('\n');
}
else not = true;
}
else if (goal.verb == MATHproduct) {
Euler el = goal.subj.deref();
double d = 1;
while (el.getFirst() != null) {
d *= Double.Parse(getLit(el.getFirst().deref()));
el = el.getRest();
}
StringBuilder sb = new StringBuilder().Append(nat(goal.subj.deref(), d));
obj = np.Parse(String.Intern(sb.ToString()));
if (goal.obj.unify(obj, this, stack)) {
pp.Append('\n');
for (int i = tab; i > 0; i--) pp.Append(" ");
goal.whysub(pp, tab);
if (tab == 0) pc.Append(goal).Append('\n');
}
else not = true;
}
else if (goal.verb == MATHquotient) {
Euler el = goal.subj.deref();
double d = Double.Parse(getLit(el.getFirst().deref()));
el = el.near.obj;
while (el.getFirst() != null) {
d /= Double.Parse(getLit(el.getFirst().deref()));
el = el.getRest();
}
StringBuilder sb = new StringBuilder().Append(d);
obj = np.Parse(String.Intern(sb.ToString()));
if (goal.obj.unify(obj, this, stack)) {
pp.Append('\n');
for (int i = tab; i > 0; i--) pp.Append(" ");
goal.whysub(pp, tab);
if (tab == 0) pc.Append(goal).Append('\n');
}
else not = true;
}
else if (goal.verb == MATHintegerQuotient) {
Euler el = goal.subj.deref();
double d = Double.Parse(getLit(el.getFirst().deref()));
el = el.near.obj;
while (el.getFirst() != null) {
d /= Double.Parse(getLit(el.getFirst().deref()));
el = el.getRest();
}
StringBuilder sb = new StringBuilder().Append(((int)d).ToString());
obj = np.Parse(String.Intern(sb.ToString()));
if (goal.obj.unify(obj, this, stack)) {
pp.Append('\n');
for (int i = tab; i > 0; i--) pp.Append(" ");
goal.whysub(pp, tab);
if (tab == 0) pc.Append(goal).Append('\n');
}
else not = true;
}
else if (goal.verb == MATHremainder) {
Euler el = goal.subj.deref();
double d = Double.Parse(getLit(el.getFirst().deref()));
el = el.getRest();
while (el.getFirst() != null) {
d %= Double.Parse(getLit(el.getFirst().deref()));
el = el.getRest();
}
StringBuilder sb = new StringBuilder().Append(nat(goal.subj.deref(), d));
obj = np.Parse(String.Intern(sb.ToString()));
if (goal.obj.unify(obj, this, stack)) {
pp.Append('\n');
for (int i = tab; i > 0; i--) pp.Append(" ");
goal.whysub(pp, tab);
if (tab == 0) pc.Append(goal).Append('\n');
}
else not = true;
}
else if (goal.verb == MATHnegation && goal.subj.bound) {
double d = Double.Parse(getLit(goal.subj.deref()));
StringBuilder sb = new StringBuilder().Append(nat(goal.subj.deref(), -d));
obj = np.Parse(String.Intern(sb.ToString()));
if (goal.obj.unify(obj, this, stack)) {
pp.Append('\n');
for (int i = tab; i > 0; i--) pp.Append(" ");
goal.whysub(pp, tab);
if (tab == 0) pc.Append(goal).Append('\n');
}
else not = true;
}
else if (goal.verb == MATHabsoluteValue) {
double d = Double.Parse(getLit(goal.subj.deref()));
StringBuilder sb = new StringBuilder().Append(nat(goal.subj.deref(), d<0?-d:d));
obj = np.Parse(String.Intern(sb.ToString()));
if (goal.obj.unify(obj, this, stack)) {
pp.Append('\n');
for (int i = tab; i > 0; i--) pp.Append(" ");
goal.whysub(pp, tab);
if (tab == 0) pc.Append(goal).Append('\n');
}
else not = true;
}
else if (goal.verb == MATHrounded) {
double d = Double.Parse(getLit(goal.subj.deref()));
StringBuilder sb = new StringBuilder().Append(Math.Round(d));
obj = np.Parse(String.Intern(sb.ToString()));
if (goal.obj.unify(obj, this, stack)) {
pp.Append('\n');
for (int i = tab; i > 0; i--) pp.Append(" ");
goal.whysub(pp, tab);
if (tab == 0) pc.Append(goal).Append('\n');
}
else not = true;
}
else if (goal.verb == MATHexponentiation) {
Euler el = goal.subj.deref();
double d = (double) Double.Parse(getLit(el.getFirst().deref()));
el = el.getRest();
while (el.getFirst() != null) {
d = Math.Pow(d, (double) Double.Parse(getLit(el.getFirst().deref())));
el = el.getRest();
}
StringBuilder sb = new StringBuilder().Append(nat(goal.subj.deref(), d));
obj = np.Parse(String.Intern(sb.ToString()));
if (goal.obj.unify(obj, this, stack)) {
pp.Append('\n');
for (int i = tab; i > 0; i--) pp.Append(" ");
goal.whysub(pp, tab);
if (tab == 0) pc.Append(goal).Append('\n');
}
else not = true;
}
else if (goal.verb == MATHgreaterThan) {
if (mathCompare(goal) > 0) {
pp.Append('\n');
for (int i = tab; i > 0; i--) pp.Append(" ");
goal.whysub(pp, tab);
if (tab == 0) pc.Append(goal).Append('\n');
}
else not = true;
}
else if (goal.verb == MATHnotGreaterThan) {
if (mathCompare(goal) <= 0) {
pp.Append('\n');
for (int i = tab; i > 0; i--) pp.Append(" ");
goal.whysub(pp, tab);
if (tab == 0) pc.Append(goal).Append('\n');
}
else not = true;
}
else if (goal.verb == MATHlessThan) {
if (mathCompare(goal) < 0) {
pp.Append('\n');
for (int i = tab; i > 0; i--) pp.Append(" ");
goal.whysub(pp, tab);
if (tab == 0) pc.Append(goal).Append('\n');
}
else not = true;
}
else if (goal.verb == MATHnotLessThan) {
if (mathCompare(goal) >= 0) {
pp.Append('\n');
for (int i = tab; i > 0; i--) pp.Append(" ");
goal.whysub(pp, tab);
if (tab == 0) pc.Append(goal).Append('\n');
}
else not = true;
}
else if (goal.verb == MATHequalTo) {
if (mathCompare(goal) == 0) {
pp.Append('\n');
for (int i = tab; i > 0; i--) pp.Append(" ");
goal.whysub(pp, tab);
if (tab == 0) pc.Append(goal).Append('\n');
}
else not = true;
}
else if (goal.verb == MATHnotEqualTo) {
if (mathCompare(goal) != 0) {
pp.Append('\n');
for (int i = tab; i > 0; i--) pp.Append(" ");
goal.whysub(pp, tab);
if (tab == 0) pc.Append(goal).Append('\n');
}
else not = true;
}
else if (goal.verb == MATHmemberCount) {
int n = 0;
Euler el = goal.subj.deref();
while (el.getFirst() != null) {
n++;
el = el.getRest();
}
StringBuilder sb = new StringBuilder().Append(n);
Euler er = np.Parse(String.Intern(sb.ToString()));
if (goal.obj.unify(er, this, stack)) {
pp.Append('\n');
for (int i = tab; i > 0; i--) pp.Append(" ");
goal.whysub(pp, tab);
if (tab == 0) pc.Append(goal).Append('\n');
}
else not = true;
}
else if (goal.verb == MATHproofCount) {
bool ot = think;
think = true;
String p = this.Proof(toURI(goal.subj));
think = ot;
StringBuilder sb = new StringBuilder().Append(conc.Count);
Euler er = np.Parse(String.Intern(sb.ToString()));
if (goal.obj.unify(er, this, stack)) {
pp.Append('\n');
for (int i = tab; i > 0; i--) pp.Append(" ");
goal.whysub(pp, tab);
if (tab == 0) pc.Append(goal).Append('\n');
}
else not = true;
}
else if (goal.verb == LOGequalTo) {
if (goal.subj.deref().verb == goal.obj.deref().verb) {
pp.Append('\n');
for (int i = tab; i > 0; i--) pp.Append(" ");
goal.whysub(pp, tab);
if (tab == 0) pc.Append(goal).Append('\n');
}
else not = true;
}
else if (goal.verb == LOGnotEqualTo) {
if (goal.subj.deref().verb != goal.obj.deref().verb) {
pp.Append('\n');
for (int i = tab; i > 0; i--) pp.Append(" ");
goal.whysub(pp, tab);
if (tab == 0) pc.Append(goal).Append('\n');
}
else not = true;
}
else if (goal.verb == LOGincludes) {
Euler e = new Euler();
engine++;
e.Load(toURI(goal.subj.deref()));
String p = e.Proof(toURI(goal.obj.deref()));
if (p.IndexOf("# Proof found") != - 1) {
pp.Append('\n');
for (int i = tab; i > 0; i--) pp.Append(" ");
goal.whysub(pp, tab);
if (tab == 0) pc.Append(goal).Append('\n');
}
else not = true;
}
else if (goal.verb == LOGnotIncludes) {
Euler e = new Euler();
engine++;
e.Load(toURI(goal.subj.deref()));
String p = e.Proof(toURI(goal.obj.deref()));
if (p.IndexOf("# Proof found") == - 1) {
pp.Append('\n');
for (int i = tab; i > 0; i--) pp.Append(" ");
goal.whysub(pp, tab);
if (tab == 0) pc.Append(goal).Append('\n');
}
else not = true;
}
else if (goal.verb == LOGsemantics) {
Euler e = np.parse(false, "^^");
e.subj = goal.subj.deref().copy();
e.obj = np.parse(false, LOGsemantics);
if (goal.obj.deref().unify(e, this, stack)) {
pp.Append('\n');
for (int i = tab; i > 0; i--) pp.Append(" ");
goal.whysub(pp, tab);
if (tab == 0) pc.Append(goal).Append('\n');
}
else not = true;
}
else if (goal.verb == LOGracine) {
String gsv = goal.subj.deref().verb;
Euler er = goal.subj.deref();
if (gsv.IndexOf('#') != -1)
er = np.Parse(String.Intern(gsv.Substring(0, gsv.IndexOf('#')) + '>'));
if (goal.obj.deref().unify(er, this, stack)) {
pp.Append('\n');
for (int i = tab; i > 0; i--) pp.Append(" ");
goal.whysub(pp, tab);
if (tab == 0) pc.Append(goal).Append('\n');
}
else not = true;
}
else if (goal.verb == LOGimplies && (goal.subj.subj == null || goal.subj.verb == "^^" || goal.subj.verb == ".")) {
Euler e = new Euler();
engine++;
bool ot = think;
Euler el = goal.subj.deref();
while (el.getFirst() != null) {
if (el.getFirst().getFirst() != null) think = true;
else e.Load(toURI(el.getFirst().deref()));
el = el.getRest();
}
e.Prepare();
if (!tr) {
Console.Out.WriteLine(
"@prefix r: .\n" +
"@prefix xsd: .\n" +
"@prefix : <#>.\n");
tr = true;
}
if (goal.obj.ToString().IndexOf("Manifest") == -1 && goal.subj.deref().getFirst() != null)
Console.Out.Write("[ r:test " + (goal.subj.getFirst().verb=="."?goal.subj.getFirst().subj:goal.subj.getFirst()) + ";" +
" r:begins \"" + now() + "\"^^xsd:dateTime; r:ends \"");
String p = e.Proof(toURI(goal.obj.deref()));
bool pass = p.IndexOf("# Proof found") != -1;
if (pass) {
pp.Append('\n');
for (int i = tab; i > 0; i--) pp.Append(" ");
pp.Append(p);
if (tab == 0) pc.Append(p).Append('\n');
}
if (goal.obj.ToString().IndexOf("Manifest") == -1 && goal.subj.deref().getFirst() != null)
Console.Out.WriteLine(now() + "\"^^xsd:dateTime; r:system :euler; " +
"a " + (pass?"r:PassingRun":"r:IncompleteRun") + ", r:TestRun].");
think = ot;
}
else if ((goal.verb == RDFSsubClassOf || goal.verb == RDFSsubPropertyOf ||
goal.verb == OWLequivalentClass || goal.verb == OWLequivalentProperty ||
goal.verb == OWLsameAs) &&
goal.subj.deref().obj == null && goal.obj.deref().obj == null &&
goal.subj.deref().bound && goal.obj.deref().bound &&
goal.subj.deref().verb == goal.obj.deref().verb) {
pp.Append('\n');
for (int i = tab; i > 0; i--) pp.Append(" ");
goal.whysub(pp, tab);
if (tab == 0) pc.Append(goal).Append('\n');
}
else if (goal.verb == RDFSfyi ||
goal.verb == RDFtype && goal.obj.deref().verb == RDFSContainerMembershipProperty
&& goal.subj.deref().verb.StartsWith(RDF + "#_") ||
goal.verb == RDFtype && goal.obj.deref().verb == RDFSLiteral
&& (goal.subj.deref().verb.StartsWith("\"") ||
goal.subj.deref().verb == "^^" && goal.subj.deref().subj.deref().verb.StartsWith("\"") ||
goal.subj.deref().isNumeral()) ||
goal.verb == RDFtype && goal.obj.deref().verb == XSDstring
&& goal.subj.deref().verb.StartsWith("\"")
&& goal.subj.deref().verb.EndsWith("\"") ||
goal.verb.EndsWith(Xrcsid + '>')) {
pp.Append('\n');
for (int i = tab; i > 0; i--) pp.Append(" ");
goal.whysub(pp, tab);
if (tab == 0) pc.Append(goal).Append('\n');
}
else {
Euler gd = goal.deref();
bool b = mstep == -1 || step-istep < mstep*engine;
bool d = dds[goal.verb] != null;
if (ts == null) {
lr = this.near;
while (lr != null) {
ts = lr;
if (b && !gd.vv && ts.verb == LOGimplies &&
(ts.obj.verb == gd.verb || !ts.obj.bound && gd.bound) &&
(!d || ts.subj.subj.verb.IndexOf("log-rules#log1d") != -1)) {
ts = ts.obj;
break;
}
if (b && !d && ts.verb == gd.verb) break;
else lr = lr.near;
ts = null;
}
}
if (ts != null) {
Euler n = lr.near;
tsb = null;
while (n != null) {
tsb = n;
if (b && !gd.vv && tsb.verb == LOGimplies &&
(tsb.obj.verb == gd.verb || !tsb.obj.bound && gd.bound) &&
(!d || tsb.subj.subj.verb.IndexOf("log-rules#log1d") != -1)) {
tsb = tsb.obj;
break;
}
if (b && !d && tsb.verb == gd.verb) break;
else n = n.near;
tsb = null;
}
if (tsb != null) {
stack.push(goal, 0);
stack.push(tsb, 0);
stack.push(n, 0);
stack.push(null, pp.Length);
stack.push(null, pc.Length);
stack.push(null, tab);
}
int hc = ts.GetHashCode();
for (int i = 0; i < varmax; i++) vars[i] = null;
if (ts.eval(false, vars, stack).unify(goal, this, stack)) {
if (ts.varid != -1) {
vars[ts.varid].verb = gd.verb;
vars[ts.varid].cverb = gd.cverb;
vars[ts.varid].varid = gd.varid;
vars[ts.varid].bound = true;
vars[ts.varid].vv = true;
}
Euler ep = goal.near; // @@ euler paths
while (ep != null) {
if (ep.verb == null && hc == ep.varid && ep.obj.unify(goal, this, null)) break;
ep = ep.near;
}
if (ep != null) {
if (trace) Console.Error.WriteLine("@@ cycle " + ep);
not = true;
}
else {
ts = ts.premis;
if (ts != null) {
ts2 = new Euler();
ts1 = ts2;
while (ts != null) {
ts1.near = ts.eval(false, vars, stack);
ts1 = ts1.near;
ts = ts.near;
}
ts1.near = new Euler();
ts1 = ts1.near;
ts1.cverb = "[" + step + "]";
ts1.obj = goal;
ts1.bound = true;
ts1.varid = hc;
ts1.near = goal.near;
ts1.far = goal.far;
goal = ts2;
if (pp.Length > 1 && pp[pp.Length - 2] == '.' && pp[pp.Length - 1] == ' ') {
pp.Append('\n');
for (int i = tab; i > 0; i--) pp.Append(" ");
}
if (pp.Length == 0) pp.Append(' ');
else if (pp.Length > 0 && pp[pp.Length - 1] != '{') pp.Append(' ');
pp.Append('{');
tab++;
}
else {
if (goal.verb == OWLsameAs) synon(goal);
if (pp.Length > 1 && pp[pp.Length - 2] == '.' && pp[pp.Length - 1] == ' ') {
pp.Append('\n');
for (int i = tab; i > 0; i--) pp.Append(" ");
}
goal.whysub(pp, tab);
if (tab == 0) pc.Append(goal).Append('\n');
}
}
}
else not = true;
}
else not = true;
}
}
catch (Exception exc) {
if (debug || trace) Console.Error.WriteLine(exc);
not = true;
}
if (trace) {
if (!not && goal.verb != null) Console.Error.WriteLine("[" + step + "]EXIT: " + goal);
else if (!not && goal.cverb != null) Console.Error.WriteLine(goal.cverb + "EXIT: " + goal.obj);
else if (not && goal.verb != null) Console.Error.WriteLine("[" + step + "]FAIL: " + goal);
else if (not && goal.cverb != null) Console.Error.WriteLine(goal.cverb + "FAIL: " + goal.obj);
}
if (goal.verb != null) {
step++;
if (debug && step % 1000000 == 0) Console.Error.WriteLine(step + " steps for " + u);
}
goal = goal.near;
if (trace && !not && goal != null && goal.verb != null)
Console.Error.WriteLine("[" + step + "]CALL: " + goal);
if (!not && goal == null) {
if (pm.Length != 0) proof.Append(pm);
else if (nope) proof.Append(pc);
else proof.Append(pp);
proof.Append("\n");
if (trace) Console.Error.WriteLine("@@ continue");
pct[pc.ToString()] = this;
}
if (not || think && goal == null) {
goal = null;
Euler b = null;
while ((b = stack.pop()) != null) {
if (b.bound) {
b.bound = false;
b.refr = null;
}
else {
tab = b.varid;
pc.Length = stack.pop().varid;
pp.Length = stack.pop().varid;
lr = stack.pop();
ts = stack.pop();
goal = stack.pop();
if (trace) Console.Error.WriteLine("[" + step + "]REDO: " + goal);
break;
}
}
}
}
}
}
internal Euler eval(bool f, Euler[] v, Stack s) {
if (refr != null && obj == null) return refr.eval(f, v, s);
if (bound && varid == - 1 && obj == null) return this;
if (varid != - 1 && v[varid] == null) v[varid] = new Euler();
if (varid != -1 && v[varid] != null && v[varid].vv) {
Euler t = new Euler();
if (subj != null) t.subj = subj.eval(true, v, s);
if (obj != null) t.obj = obj.eval(true, v, s);
t.verb = v[varid].verb;
t.cverb = v[varid].cverb;
t.varid = v[varid].varid;
t.bound = true;
return t;
}
else if (obj != null) {
Euler t = new Euler();
if (subj != null) t.subj = subj.eval(true, v, s);
if (obj != null) t.obj = obj.eval(true, v, s);
t.verb = verb;
t.cverb = cverb;
t.varid = varid;
if (v != null && !bound && varid != - 1) {
if (v[varid] != t) t.refr = v[varid];
t.bound = true;
s.push(t, 0);
}
else t.bound = true;
t.vv = vv;
if (f && near != null) t.near = near.eval(true, v, s);
else t.near = near;
return t;
}
v[varid].verb = verb;
v[varid].cverb = cverb;
v[varid].varid = varid;
return v[varid];
}
internal bool unify(Euler t, Euler r, Stack s) {
if (t == null) return false;
if (refr != null && obj == null) return refr.unify(t, r, s);
if (t.refr != null && t.obj == null) return unify(t.refr, r, s);
if (bound && t.bound) {
if (obj != null && verb == "^^" && t.verb == "^^" && subj.bound && t.subj.bound &&
(obj.unify(t.obj, r, s) || Datatype.IsNumeric(r.getType(this)) && Datatype.IsNumeric(r.getType(t))) ||
(verb == "^^" && subj.bound && obj.bound && t.obj == null || obj == null && t.verb == "^^" && t.subj.bound && t.obj.bound) &&
(r.getType(this) == r.getType(t) || Datatype.IsNumeric(r.getType(this)) && Datatype.IsNumeric(r.getType(t))))
return Datatype.Compare(r.getType(this), r.getLit(this), r.getType(t), r.getLit(t)) == 0;
if (varid == - 1 && verb != null && t.verb != null && deref().verb != t.deref().verb) return false;
if (subj != null && !subj.unify(t.subj, r, s)) return false;
if (obj != null && !obj.unify(t.obj, r, s)) return false;
if (near != null && near.verb == RDFrest && t.near.verb == RDFrest && !near.unify(t.near, r, s)) return false;
return true;
}
if (bound) return t.unify(this, r, s);
if (s != null) {
if (t.varid != -1 && t.varid != varid && t.oc(varid)) return false;
if (subj != null && !subj.unify(t.subj, r, s)) return false;
if (obj != null && !obj.unify(t.obj, r, s)) return false;
if (near != null && near.verb == RDFrest && t.near.verb == RDFrest && !near.unify(t.near, r, s)) return false;
if (t != deref()) deref().refr = t;
bound = true;
s.push(this, 0);
}
return true;
}
internal bool oc(int vi) {
if (refr != null) return refr.oc(vi);
if (bound) {
if (subj != null && subj.oc(vi)) return true;
if (obj != null && obj.oc(vi)) return true;
return false;
}
else return (varid == vi);
}
internal void rewrite(bool eu, Euler el, Parser np) {
if (el.subj != null && el.subj.cverb == null)
el.subj.verb = el.subj.cverb = (eu?"_:":"?v") + el.subj.GetHashCode() + "_" + doc;
if (el.obj != null && el.obj.cverb == null)
el.obj.verb = el.obj.cverb = (eu?"_:":"?v") + el.obj.GetHashCode() + "_" + doc;
if (eu && el.subj != null && el.subj.cverb.StartsWith("?"))
el.subj.verb = el.subj.cverb = "_:" + el.subj.cverb.Substring(1) + "_" + doc;
if (eu && el.obj != null && el.obj.cverb.StartsWith("?"))
el.obj.verb = el.obj.cverb = "_:" + el.obj.cverb.Substring(1) + "_" + doc;
if (el.subj != null && el.subj.subj == null && el.subj.obj != null && el.subj.getFirst() == null) {
Euler gr = el.subj.copy();
Euler gv = np.parse(false, (eu?"_:":"?v") + gr.GetHashCode() + "_" + doc);
el.subj = gv;
Euler gl = gr;
while (true) {
gl.subj = gv;
np.swap(gl);
if (gl.near == null) break;
gl = gl.near;
}
gl.near = el.near;
el.near = gr;
if (el.verb.Equals("")) {
el.subj = gr.subj;
el.verb = gr.verb;
el.obj = gr.obj;
el.cverb = gr.cverb;
el.varid = gr.varid;
el.bound = gr.bound;
el.near = gr.near;
}
}
if (el.obj != null && el.obj.subj == null && el.obj.obj != null) {
Euler gr = el.obj.copy();
Euler gv = np.parse(false, (eu?"_:":"?v") + gr.GetHashCode() + "_" + doc);
el.obj = gv;
Euler gl = gr;
while (true) {
gl.subj = gv;
np.swap(gl);
if (gl.near == null) break;
gl = gl.near;
}
gl.near = el.near;
el.near = gr;
}
if (el.subj != null && el.subj.verb == "^" && el.verb != LOGimplies) {
Euler gr = el.subj.copy();
rewrite(eu, gr, np);
Euler gv = np.parse(false, (eu?"_:":"?v") + gr.GetHashCode() + "_" + doc);
el.subj = gv;
Euler gl = gr;
gl.verb = gl.obj.verb;
gl.cverb = gl.obj.cverb;
gl.varid = gl.obj.varid;
gl.bound = gl.obj.bound;
gl.obj = gl.subj.copy();
gl.subj = gv;
np.swap(gl);
while (gl.near != null) gl = gl.near;
gl.near = el.near;
el.near = gr;
}
if (el.obj != null && el.obj.verb == "^" && el.verb != LOGimplies) {
Euler gr = el.obj.copy();
rewrite(eu, gr, np);
Euler gv = np.parse(false, (eu?"_:":"?v") + gr.GetHashCode() + "_" + doc);
el.obj = gv;
Euler gl = gr;
gl.verb = gl.obj.verb;
gl.cverb = gl.obj.cverb;
gl.varid = gl.obj.varid;
gl.bound = gl.obj.bound;
gl.obj = gl.subj.copy();
gl.subj = gv;
np.swap(gl);
while (gl.near != null) gl = gl.near;
gl.near = el.near;
el.near = gr;
}
if (el.subj != null && el.subj.verb == "." && el.verb != LOGimplies) {
Euler gr = el.subj.copy();
rewrite(eu, gr, np);
Euler gv = np.parse(false, (eu?"_:":"?v") + gr.GetHashCode() + "_" + doc);
el.subj = gv;
Euler gl = gr;
gl.verb = gl.obj.verb;
gl.cverb = gl.obj.cverb;
gl.varid = gl.obj.varid;
gl.bound = gl.obj.bound;
gl.obj = gv;
np.swap(gl);
while (gl.near != null) gl = gl.near;
gl.near = el.near;
el.near = gr;
}
if (el.obj != null && el.obj.verb == "." && el.verb != LOGimplies) {
Euler gr = el.obj.copy();
rewrite(eu, gr, np);
Euler gv = np.parse(false, (eu?"_:":"?v") + gr.GetHashCode() + "_" + doc);
el.obj = gv;
Euler gl = gr;
gl.verb = gl.obj.verb;
gl.cverb = gl.obj.cverb;
gl.varid = gl.obj.varid;
gl.bound = gl.obj.bound;
gl.obj = gv;
np.swap(gl);
while (gl.near != null) gl = gl.near;
gl.near = el.near;
el.near = gr;
}
}
internal Euler copy() {
Euler el = new Euler();
if (subj != null) el.subj = subj.copy();
el.verb = verb;
if (obj != null) el.obj = obj.copy();
el.cverb = cverb;
el.varid = varid;
el.bound = bound;
if (refr != el) el.refr = refr;
el.premis = premis;
if (near != null) el.near = near.copy();
el.far = far;
return el;
}
internal void getX(bool f, ArrayList wt) {
if (subj != null) subj.getX(true, wt);
if (verb != null && (verb.StartsWith("_:") || verb.StartsWith("?")) && !wt.Contains(verb))
wt.Add(verb);
if (obj != null) obj.getX(true, wt);
if (f && near != null) near.getX(f, wt);
}
internal void forX(bool f, ArrayList wt) {
if (subj != null) subj.forX(true, wt);
if (verb != null && wt.Count > 0 && wt.IndexOf(verb) != - 1) {
varid = wt.IndexOf(verb);
bound = false;
}
if (obj != null) obj.forX(true, wt);
if (f && near != null) near.forX(f, wt);
}
internal void reorder(Euler er) {
Euler el = er.near;
Euler elc = null, elcp = null, elv = null, elvp = null;
while (el != null) {
if (el.varid != -1 || el.verb.Equals(RDFtype)) {
if (elv == null) elvp = elv = el;
else elvp = elvp.near = el;
}
else {
if (elc == null) elcp = elc = el;
else elcp = elcp.near = el;
}
el = el.near;
}
if (elvp != null) elvp.near = null;
if (elcp != null) elcp.near = elv;
if (elc != null) er.near = elc;
}
internal void synon(Euler t) {
if (t.subj.deref().verb.Equals("^^") || t.obj.deref().verb.Equals("^^")) return;
bool w = !t.subj.deref().verb.StartsWith(W3C);
String s = w?t.subj.deref().verb:t.obj.deref().verb;
String o = w?t.obj.deref().verb:t.subj.deref().verb;
if (o == null || s == null) return;
if (t.subj != null && t.obj != null && t.subj.subj == null &&
t.subj.obj == null && t.obj.subj == null && t.obj.obj == null) {
if (!s.Equals(o)) syn[s] = o;
for (IEnumerator e = (IEnumerator) ((Hashtable)syn.Clone()).Keys.GetEnumerator(); e.MoveNext(); ) {
String k = (String) e.Current;
if (syn[k] != null && syn[k].Equals(s)) {
if (!k.Equals(o)) syn[k] = o;
else syn.Remove(k);
}
}
}
else if (t.subj != null && t.obj == null && t.subj.subj == null && t.subj.obj == null) syn[s] = t;
else if (t.subj == null && t.obj != null && t.obj.subj == null && t.obj.obj == null) syn[o] = t;
}
internal void syno(Euler t) {
for (Euler el = t; el != null; el = el.near) synt(el);
}
internal void synt(Euler t) {
if (t.subj != null) syno(t.subj);
if (t.verb != null) {
Object o = this.syn[t.verb];
if (o != null) {
if (o is String) t.verb = (String) o;
else t.verb = o.ToString();
}
t.verb = String.Intern(t.verb);
}
if (t.obj != null) syno(t.obj);
}
internal Euler deref() {
if (refr != null) return refr.deref();
else return this;
}
internal String stringf(bool f) {
if (refr != null && obj == null) return refr.stringf(f);
String cv = debug?deref().verb:deref().cverb;
if (cv != null && cv.Equals("^^")) return subj + "^^" + obj;
if (cv != null && cv.Equals("^")) return subj + "^" + obj;
if (cv != null && cv.Equals(".")) {
if (!root.getLit(deref()).Equals(deref().verb)) return root.getLit(deref());
else return subj + "." + obj;
}
if (f && subj != null && subj.varid == -1 || obj == null) {
if (cv == null) return deref().verb;
return cv;
}
Euler el = deref();
Euler en = null;
StringBuilder r = new StringBuilder(64);
bool sv = subj != null && subj.refr == null && subj.subj == null &&
subj.cverb != null && subj.cverb.Equals("[]") && subj.obj == null;
bool ov = obj != null && obj.refr == null && obj.subj == null &&
obj.cverb != null && obj.cverb.Equals("[]") && obj.obj == null;
bool b = verb != null && !verb.Equals(LOGimplies) &&
!verb.Equals(LOGincludes) && !verb.Equals(LOGnotIncludes) &&
!verb.Equals(LOGinconsistentWith) && !verb.Equals(MATHproofCount) &&
!verb.Equals(OWLsameAs);
if (el.verb != null && el.verb.Equals(RDFfirst) && el.subj == null && el.obj != null) {
r.Append("(");
while (el != null && el.obj != null) {
int i = r.Length;
r.Append(el.obj.deref().stringf(b && el.obj.subj != null && el.obj.obj != null));
if (r.Length > 1 && (r[r.Length - 2] == '.' && r[r.Length - 1] == ' ' || r[r.Length - 1] == ';')) {
if (r[i] != ' ') {
r.Insert(i, '{');
r[r.Length - 2] = '}';
}
else {
r.Insert(i, '[');
r[r.Length - 1] = ']';
}
}
en = el.near.obj.deref();
if (en.verb.Equals(RDFnil)) break;
else if (!en.verb.Equals(RDFfirst)) {
r.Append("/ ");
r.Append(en.stringf(b && en.subj != null && en.obj != null));
break;
}
r.Append(' ');
el = en;
}
r.Append(')');
return r.ToString();
}
if (!sv && subj != null && verb != null && !b && subj.verb != ".") {
el = subj.deref();
while (el != null) {
r.Append(el.stringf(b && el.subj != null && el.obj != null));
el = el.near;
}
}
else if (!sv && subj != null || !sv && subj != null && subj.deref().subj == null) {
el = subj.deref();
r.Append(el.stringf(b && el.subj != null && el.obj != null));
}
if (r.Length > 1 && (r[r.Length - 2] == '.' && r[r.Length - 1] == ' ' || r[r.Length - 1] == ';')) {
if (r[0] != ' ') {
r.Insert(0, '{');
r[r.Length - 2] = '}';
}
else {
r.Insert(0, '[');
r[r.Length - 1] = ']';
}
}
if (r.Length > 0 && r[r.Length - 1] != ' ') r.Append(' ');
r.Append(debug?deref().verb:deref().cverb);
r.Append(' ');
int i2 = r.Length;
if (!ov && obj != null && verb != null && !b ||
!ov && obj != null && obj.deref().subj == null) {
el = obj.deref();
while (el != null) {
r.Append(el.stringf(b && el.subj != null && el.obj != null));
el = el.near;
}
}
else if (!ov && obj != null) r.Append(obj.stringf(b && obj.subj != null && obj.obj != null));
if (r.Length > 1 && (r[r.Length - 2] == '.' && r[r.Length - 1] == ' ' || r[r.Length - 1] == ';')) {
if (r[i2] != ' ') {
r.Insert(i2, '{');
r[r.Length - 2] = '}';
}
else {
r.Insert(i2, '[');
r[r.Length - 1] = ']';
}
}
if (!sv && subj != null && r[r.Length - 1] == ' ') r.Insert(r.Length - 1, '.');
else if (!sv && subj != null && r[r.Length - 1] != ' ') r.Append(". ");
else {
r.Append(';');
el = near;
while (el != null) {
r.Append(' ').Append(debug?el.deref().verb:el.deref().cverb).Append(' ');
r.Append(el.obj.stringf(b && el.subj != null && el.obj != null));
r.Append(';');
el = el.near;
}
r.Insert(0, '[');
r[r.Length - 1] = ']';
}
return r.ToString();
}
/// string represention of this Euler object
/// string
public override String ToString() {
return stringf(false);
}
internal Euler getFirst() {
Euler er = this;
if (verb == "^^" || verb == "^" || verb == ".") er = subj;
while (er != null) {
if (er.verb == RDFfirst) return er.obj;
else er = er.near;
}
return null;
}
internal Euler getRest() {
Euler er = this;
if (verb == "^^" ||verb == "^" || verb == ".") er = subj;
while (er != null) {
if (er.verb == RDFrest) return er.obj;
else er = er.near;
}
return null;
}
internal String getLit(Euler el) {
String s = el.verb;
if (s == "." && el.obj.verb.StartsWith(MATH)) {
Proof("data:," + el.subj + " " + el.obj + " ?x. ");
if (obj != null) s = obj.cverb;
}
if (s == "^^") return getLit(el.subj.deref());
if (s.StartsWith("\"\"\"")) return s.Substring(3, s.Length - 6);
if (s.IndexOf('"') != -1) return s.Substring(s.IndexOf('"') + 1, s.LastIndexOf('"') - s.IndexOf('"') - 1);
return s;
}
internal String getType(Euler el) {
if (el.obj == null) {
if (el.isNumeral()) return XSDdouble;
else return XSDstring;
}
else return el.obj.deref().verb;
}
internal double mathCompare(Euler el) {
Euler s = el.subj.deref();
Euler o = el.obj.deref();
if ((s.verb == "^^" || o.verb == "^^") &&
(getType(s) == getType(o) || Datatype.IsNumeric(getType(s)) && Datatype.IsNumeric(getType(o))))
return Datatype.Compare(getType(s), getLit(s), getType(o), getLit(o));
return Double.Parse(getLit(s)) - Double.Parse(getLit(o));
}
internal void whysub(StringBuilder sb, int tab) {
if (subj.varid != -1 || varid != -1 || obj.varid != -1) {
sb.Append(" {");
whysubst(sb, tab);
sb.Append("} =>\n");
for (int i = tab; i > 0; i--) sb.Append(" ");
sb.Append("{").Append(this);
if (sb[sb.Length - 2] == '.' && sb[sb.Length - 1] == ' ') sb.Insert(sb.Length - 2, '}');
else sb.Append("}. ");
}
else sb.Append(this);
}
internal void whysubst(StringBuilder sb, int tab) {
Parser np = new Parser();
Euler el = np.parse(false, "=");
el.subj = np.parse(false, IWV);
if (subj.varid != -1) {
el.subj.obj = np.parse(false, "\"" + subj.cf() + "\"");
el.obj = subj.deref();
sb.Append(el).Append('\n');
for (int i = tab; i >= 0; i--) sb.Append(" ");
}
if (varid != -1) {
sb.Append("[").Append(IWV).Append(" \"").Append(cf()).Append("\"] = ").Append(deref().cverb).Append(".\n");
for (int i = tab; i >= 0; i--) sb.Append(" ");
}
if (obj.varid != -1) {
el.subj.obj = np.parse(false, "\"" + obj.cf() + "\"");
el.obj = obj.deref();
sb.Append(el).Append('\n');
for (int i = tab; i >= 0; i--) sb.Append(" ");
}
if (subj.varid != -1) sb.Append("[").Append(IWV).Append(" \"").Append(subj.cf()).Append("\"] ");
else sb.Append(subj.cf()).Append(" ");
if (varid != -1) sb.Append("[").Append(IWV).Append(" \"").Append(cf()).Append("\"] ");
else sb.Append(cf()).Append(" ");
if (obj.varid != -1) sb.Append("[").Append(IWV).Append(" \"").Append(obj.cf()).Append("\"]");
else sb.Append(obj.cf());
}
internal String cf() {
if (subj == null && verb == RDFfirst) return this.ToString();
if (cverb == "^^") return subj + "^^" + obj;
else return cverb;
}
internal String fromWeb(String uri) {
StringBuilder sb = new StringBuilder();
String rl = null;
if (uri.StartsWith("data:")) {
baseURI = "";
return uri.Substring(uri.IndexOf(',') + 1);
}
else if (uri.StartsWith("http:")) {
try {
if (!uri.StartsWith("http://localhost/AskJena?fromWeb=")) baseURI = uri;
if (!local || uri.StartsWith("http://localhost")) {
Uri r = new Uri(uri);
String p = r.PathAndQuery;
String hp = Environment.GetEnvironmentVariable("http_proxy");
if (hp != null && !hp.Equals("") && !hp.Equals("%http_proxy%") && !uri.StartsWith("http://localhost")) {
r = new Uri(hp);
p = uri;
}
TcpClient so = new TcpClient(r.Host, r.Port == - 1?80:r.Port);
//so.NoDelay.Enabled = true;
StreamWriter pw = new StreamWriter((Stream) so.GetStream());
pw.WriteLine("GET " + p + " HTTP/1.0");
pw.WriteLine("Host: " + r.Host);
pw.WriteLine("");
pw.Flush();
StreamReader br = new StreamReader((Stream) so.GetStream());
if ((rl = br.ReadLine()).IndexOf("200") == - 1) throw new SystemException(rl);
while (!br.ReadLine().Equals(""));
while ((rl = br.ReadLine()) != null) {
sb.Append(rl);
sb.Append('\n');
}
so.Close();
}
else {
StreamReader br = new StreamReader(uri.Substring(6));
while ((rl = br.ReadLine()) != null) {
sb.Append(rl);
sb.Append('\n');
}
br.Close();
}
}
catch (Exception) {
if (uri.StartsWith("http://localhost")) throw new SystemException(uri);
return fromWeb("http://localhost/AskJena?fromWeb=" + (!local?uri:uri.Substring(6)));
}
}
else {
if (uri.StartsWith("file:")) uri = uri.Substring(uri.IndexOf(':') + 1);
if (uri.IndexOf('#') != - 1) uri = uri.Substring(0, uri.LastIndexOf('#'));
try {
String path = Directory.GetCurrentDirectory().Replace(Path.DirectorySeparatorChar, '/');
path = path.Substring(path.IndexOf('/')) + "/";
baseURI = "file:" + ((uri[0] == '/' || uri[1] ==':') ? "" : path) + uri;
StreamReader br = new StreamReader(uri);
while ((rl = br.ReadLine()) != null) {
sb.Append(rl);
sb.Append('\n');
}
br.Close();
}
catch (Exception) {
return fromWeb("http://localhost/AskJena?fromWeb=" + uri);
}
}
return sb.ToString();
}
internal String toURI(Euler el) {
if (el.verb == "^^" || el.verb == "^" || el.verb == ".") el = el.subj;
if (el.obj != null) {
StringBuilder sb = new StringBuilder("data:,");
for (IEnumerator en = (IEnumerator) ns.Keys.GetEnumerator(); en.MoveNext(); ) {
Object nsx = en.Current;
sb.Append("@prefix ").Append(nsx).Append(' ').Append(ns[nsx]).Append(".\n");
}
for (Euler eu = el; eu != null; eu = eu.near) sb.Append(eu);
return sb.ToString();
}
else if (el.verb.Equals("this")) return baseURI;
else if (el.verb.StartsWith(RDF)) return "http://www.agfa.com/w3c/euler/rdf-rules.n3";
else if (el.verb.StartsWith(RDFS)) return "http://www.agfa.com/w3c/euler/rdfs-rules.n3";
else if (el.verb.StartsWith(XSD)) return "http://www.agfa.com/w3c/euler/xsd-rules.n3";
else if (el.verb.StartsWith(OWL)) return "http://www.agfa.com/w3c/euler/owl-rules.n3";
else {
String s = el.verb;
if (s[0] == '<') s = s.Substring(1, s.Length - 2);
if (s[s.Length - 1] == '#') s = s.Substring(0, s.Length - 1);
if (s.EndsWith(".rdf")) s = s.Substring(0, s.Length - 4) + ".n3";
else if (!s.EndsWith(".n3") && !s.EndsWith(".nt")) s = s + ".n3";
return s;
}
}
internal String nat(Euler el, double d) {
if (el.getFirst() == null && getLit(el.deref()).IndexOf('.') != -1) return d.ToString();
while (el.getFirst() != null) {
if (getLit(el.getFirst().deref()).IndexOf('.') != -1) return d.ToString();
el = el.getRest();
}
return ((int)d).ToString();
}
internal bool isNumeral() {
try {
Double.Parse(verb);
return true;
}
catch (Exception) {
return false;
}
}
internal String now() {
DateTime d = DateTime.UtcNow;
StringBuilder sb = new StringBuilder();
sb.Append(d.Year).Append('-')
.Append(d.Month<10?"0":"").Append(d.Month).Append('-')
.Append(d.Day<10?"0":"").Append(d.Day).Append('T')
.Append(d.Hour<10?"0":"").Append(d.Hour).Append(':')
.Append(d.Minute<10?"0":"").Append(d.Minute).Append(':')
.Append(d.Second<10?"0":"").Append(d.Second).Append('Z');
return sb.ToString();
}
internal String toHex(String s) {
StringBuilder sb = new StringBuilder();
for (int i = 0; i < s.Length; i++) sb.Append(Convert.ToString(s[i], 16));
return sb.ToString();
}
/// Main method invoked via Euler
/// [--think] [--nope] [--step count] [--debug] [--trace] axiom ... lemma
[STAThread]
public static void Main(String[] args) {
if (args.Length == 0) Console.Error.WriteLine("Euler [--think] [--nope] [--step count] [--debug] [--trace] axiom ... lemma");
else {
try {
step = 1;
trace = false;
think = false;
TextWriter outp = Console.Out;
Euler e = new Euler();
Parser np = new Parser();
int n = args.Length - 1;
if (args[n].StartsWith(">")) {
outp = new StreamWriter(new FileStream(new FileInfo(args[n].Substring(1)).FullName, FileMode.Create));
n--;
}
for (int j = 0; j < n; j++) {
if (args[j].EndsWith("-think")) think = true;
else if (args[j].EndsWith("-nope")) nope = true;
else if (args[j].EndsWith("-step")) mstep = Int64.Parse(args[++j]);
else if (args[j].EndsWith("-local")) local = true;
else if (args[j].EndsWith("-debug")) debug = true;
else if (args[j].EndsWith("-trace")) trace = true;
else if (!args[j].StartsWith("-")) e.Load(e.toURI(np.Parse('<' + args[j] + '>')));
}
e.Prepare();
outp.WriteLine(e.Proof(e.toURI(np.Parse('<' + args[n] + '>'))));
if (outp != Console.Out) outp.Close();
}
catch (Exception e) {
Console.Error.WriteLine(e);
}
}
}
}