// $Id: EulerProof.cs 93 2003-07-01 07:28:40Z mdupont $
using System;
using System.Collections;
using System.IO;
using System.Net;
using System.Net.Sockets;
using System.Text;
using DotGNU.Rdf;
/*
MainProofLoop(elrEp) --> rewrite
CheckLogForSome
LOGForSomeProof
*/
/// proofs a conjunction with that proof engine
/// of the RDF resource
/// proof
/// Euler proof mechanism
/// hacked by mdupont
/// Jos De Roo
/// James Michael DuPont
public class Euler {
public Euler subj = null; // RDF subject
public String verb = null; // RDF predicate as absoluteized verb
public Euler obj = null; // RDF object
public String cverb = null; // compact verb
public int varid = - 1; // variable id
public bool bound = false; // variable binding state
internal bool vv = false; // variable verb state, set in load, used in proof, eval
public Euler refr = null; java-mode // to be dereferenced
public Euler premis = null; // to attach the premis
public Euler near = null; // to construct a conjunction
public Euler far; // to remember last/root clause
// needed for URI resolving
// RENAMED:internal Hashtable ns = null; // to table namespaces
public Hashtable hshtNs = null; // to table namespaces
// RENAMED:internal Hashtable nsp = null; // to table namespace prefixes
public Hashtable hshtNsp = null; // to table namespace prefixes
// RENAMED:internal Hashtable syn = null; // to table synonyms
public Hashtable hshtSyn; // to table synonyms in parent
//REMOVED TO PROOF:internal Hashtable dds = null; // to table log:definitiveDocument and Service properties
public int varmax = 0; // maximum variable count
public String baseURI = null; // URI of base process
// public String uri; // the uri of the proof engine
public Hashtable loaded = null; // to table document/engine pairs
public static long engine = 0;
// public long eng = engine; // engine number
public const String version = "R3338";
// internal const String IW = "constructs a proof engine
public Euler() {
r = new Report();
hshtNs = new Hashtable();
hshtSyn = new Hashtable();
RegisterNamespaces();
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);
StringBuilder stbldGen = new StringBuilder("data:,");
r.Load(engine, uri);
while (true) {
far.near = np.Parse(); // ok start the parsing!a
if (far.near == null) break; // and break unless it is ok
while (far.near != null) {
if (CheckFirstPass()) // has been removed
{
// check the register classes
// TODO :FIRSTPASS
}
else
{
// @@ rule generation
Euler s = far.near.subj;
String p = far.near.verb;
Euler o = far.near.obj;
// TODO : SECOND PASS!
CheckSecondPass(far.near);
r.Assert(far.near);
far = far.near;
}
}
syno(this);
String gener = stbldGen.ToString();
if (!gener.Equals("data:,")) this.Load(gener); // line 249
if (vt.Count > varmax) varmax = vt.Count;
doc++;
} // end of while true
} // end of Lock
}
/// prepares that proof engine
public virtual void Prepare() {
Console.Error.WriteLine("prepare!");
lock(this) {
bool ot = think; //
long os = step;
think = true;
{
// r.Prepare(engine,baseURI);
}
Console.Error.WriteLine("prepare call proof.");
String p = Proof("data:,?s = ?o.");
Console.Error.WriteLine("prepare return from proof.");
step = os;
think = ot;
Console.Error.WriteLine("syno");
syno(this);
Console.Error.WriteLine("~syno");
}
Console.Error.WriteLine("prepare");
}
public virtual String Proof(String auri) {
Console.Error.WriteLine("EulerProof!");
r.Proof(engine,auri);
Console.Error.WriteLine("EulerProof2!");
// uri = auri;
r.Proof(engine,auri);
String cj = fromWeb(auri);
String u = baseURI;
r.Proof(engine,auri);
long query = 0;
Console.Error.WriteLine("Before Loop");
Proof theProof = new Proof(this,auri,u,cj);
return theProof.DoProof();
}
// int tab = 0; // i made this global
public virtual bool SameAs(String s)
{
return false;//TODO :
}
public virtual void RegisterNamespaces()
{
hshtNs["log:"] = LOG + "#>";
hshtNs["rdfs:"] = RDFS + "#>";
hshtNs["iw:"] = IW + "#>";
}
public virtual int Indent(StringBuilder stbldPp, int tab)
{
if (stbldPp.Length > 0 &&
stbldPp[stbldPp.Length - 1] == '.')
{
stbldPp.Append('\n');
for (int i = tab; i > 0; i--)
{
stbldPp.Append(" ");
}
}
return tab;
}
// .method /*0600000D*/ public virtual hidebysig newslot instance void 'ReportSteps'(class 'System'.'String'/*00000000*/ 'uri', class 'Euler'/*02000002*/ 'elrGoal') cil managed
public virtual void ReportSteps(String uri, Euler e)
{
if (e !=null)
{
if (e.verb != null) {
step++;
if (debug && step % 1000000 == 0) {
r.ReportSteps(step,uri);
}
}
}
}
/// loads all facts and rules acquired from the RDF URI in that proof engine
/// of the RDF resource
public virtual bool CheckFirstPass()
{
return false;
}
public virtual bool CheckSecondPass(Euler far_near)
{
return false;
}
public bool unify(Euler t, Euler r, EStack 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 (IfCompareNumeric( t,r,s))
{
CompareNumeric(t,r,s);
}
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;
return true;
}
if (bound)
{
// unify this with t?
return t.unify(this, r, s);
}
if (s != null) {
if (t.varid != varid && t.oc(varid)) return false;
// recurse into subject
if (subj != null && !subj.unify(t.subj, r, s)) return false;
// recurse into object
if (obj != null && !obj.unify(t.obj, r, s)) return false;
// deref the object
if (t != deref()) {
deref().refr = t;
}
//
bound = true;
// push this object
s.push(this, 0);
}
return true;
}
public 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);
}
public void syno(Euler t) {
for (Euler elrEl = t; elrEl != null; elrEl = elrEl.near) synt(elrEl);
}
public void synt(Euler t) {
if (t.subj != null) syno(t.subj);
if (t.verb != null) {
Object o = hshtSyn[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);
}
public 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);
}
public 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);
}
public void synon(Euler t) {
String s = t.subj.deref().verb;
String o = t.obj.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)) hshtSyn[s] = o;
for (IEnumerator e = (IEnumerator) ((Hashtable)hshtSyn.Clone()).Keys.GetEnumerator(); e.MoveNext(); ) {
String k = (String) e.Current;
if (hshtSyn[k].Equals(s)) {
if (!k.Equals(o)) hshtSyn[k] = o;
else hshtSyn.Remove(k);
}
}
}
else if (t.subj != null && t.obj == null && t.subj.subj == null && t.subj.obj == null) hshtSyn[s] = t;
else if (t.subj == null && t.obj != null && t.obj.subj == null && t.obj.obj == null) hshtSyn[o] = t;
}
public Euler copy() {
Euler elrEl = new Euler();
if (subj != null) elrEl.subj = subj.copy();
elrEl.verb = verb;
if (obj != null) elrEl.obj = obj.copy();
elrEl.cverb = cverb;
elrEl.varid = varid;
elrEl.bound = bound;
if (refr != elrEl) elrEl.refr = refr;
elrEl.premis = premis;
if (near != null) elrEl.near = near.copy();
elrEl.far = far;
return elrEl;
}
public void copyAttributes(Euler elrEl, Euler gr)
{
elrEl.subj = gr.subj;
elrEl.verb = gr.verb;
elrEl.obj = gr.obj;
elrEl.cverb = gr.cverb;
elrEl.varid = gr.varid;
elrEl.bound = gr.bound;
elrEl.near = gr.near;
}
public Euler eval(Euler[] v, EStack s) {
// evals the current euler, pushes the new one onto the stack
// also binds the variables if not done into the refr field, and sets the bound flag
// uses obj, subj, varid, refr, bound
if (refr != null && obj == null)
{
return refr.eval(v, s);
}
if (bound && varid == - 1 && obj == null)
{
return this;
}
if (varid != - 1 && v[varid] == null) {
v[varid] = new Euler();
v[varid].verb = verb;
v[varid].cverb = cverb;
v[varid].varid = varid;
}
// if the obj is not null, the do somethign with it!
if (obj != null) {
Euler t = new Euler();
// set the subject of the t to be the eval of the subj
if (subj != null)
{
// eval the subject into the new object
t.subj = subj.eval(v, s); // recurse
}
// we have done this already
// if (obj != null)
t.obj = obj.eval(v, s); // recurse
// copy these variables
t.verb = verb;
t.cverb = cverb;
t.varid = varid;
// if the variable array v is not empty,
// and this is not bound
// and the varid is not null
if (v != null && !bound && varid != - 1) {
// and t is not stored in the variable already
if (v[varid] != t){
// now copy the reference to the varible into refr
t.refr = v[varid]; // lookup the variable
}
t.bound = true; // now it is bound
// now push the t onto the stack
s.push(t, 0); // push the new t on the stack
}
else t.bound = true; // it has been bound already
// obj and near are set, eval near!
if (subj == null && obj != null && near != null) {
t.near = near.eval(v, s);
}
else{
// copy near, it is null anyway
t.near = near;
}
return t;
}
return v[varid];
}
public void prove(Euler elrEl, Parser np) {
// see the EulerProof.cs
}
//# Node
//# elrEl [subject[s.subject s.predicate s.object] elrEl.predicate elrEl.object].
public Euler rewriteHelper(Euler elrEl, Parser np, Euler targetFieldRef)
{
Euler targetField = targetFieldRef.copy();
// Euler targetField = targetFieldRef.copy();
// parse this thing, ?v + Hash of Target Field
// gets you the value of the hash object in memory.
Euler gv = np.parse(false, "?v" + targetField.GetHashCode());
// store the Target
targetField = gv; // assign the value of the data to the field object. first step in the rewrite
// here we have an atomic operation, take the targetField, parse it, and store results in
// this meahshtNs : subj = a variable with the same hash code as the subject
// an iterator through the values of the RdfData
Euler gl = targetField;
// CHAINON gl.near { swap gl, where gl.subj=RdfData about subject or object}
// does this mean we replace the subject with an interpretation of the
while (true) {
// here we store the value in the subject
gl.subj = gv; // get the hash value of the subject, and store it in there
np.swap(gl); // tell the parser to swap this object gl
if (gl.near == null) break; // CHAINON?
gl = gl.near; // CHAINON
}
// Append : add to Global chain :
// gl is basically targetField
// 1. This = global.next
// 2. Global next = this
gl.near = elrEl.near; // store the next in
elrEl.near = targetField; // add this object to the end of the chain,
return targetField; // returns the updated field
}
// public void rewrite(Euler elrEl, Parser np) ;
public void rewrite(Euler elrEl, Parser np) {
if (elrEl.subj != null &&
elrEl.subj.subj == null &&
elrEl.subj.obj != null
//TODO && elrEl.subj.getFirst() == null
) {
Euler gr = rewriteHelper(elrEl,np,elrEl.subj);
// now process the verb
if (elrEl.verb.Equals("")) {
// copy all the attributes this i guess expands the subject to be
// the whole statement, if there is no predicate
elrEl.copyAttributes(elrEl,gr);
}
}
// second, process the type of object
if (elrEl.obj != null && elrEl.obj.subj == null && elrEl.obj.obj != null) {
rewriteHelper(elrEl,np, elrEl.obj);
}
}
public bool IfCompareNumeric(Euler t, Euler r,EStack s)
{
if (verb == "^^" && t.verb == "^^" && subj.bound && t.subj.bound &&
(obj.unify(t.obj, r, s) || Datatype.IsNumeric(obj.deref().verb) &&
Datatype.IsNumeric(t.obj.deref().verb)))
{
return true;
}
return false;
}
public bool CompareNumeric(Euler t, Euler r,EStack s)
{
return false;
// return Datatype.Compare(obj.deref().verb, r.getLit(this), r.getLit(t)) == 0;
}
public Euler deref() {
if (refr != null) return refr.deref();
else return this;
}
public String stringf(bool f, int n) {
if (refr != null && obj == null) return refr.stringf(f, n);
String cv = deref().cverb;
if (cv != null && cv.Equals("^^")) return subj + "^^" + obj;
if (f && subj.varid == - 1 || obj == null) {
if (cv == null) return "[]";
//TODO: if (cv.Equals(RDFnil)) return "( )";
return cv;
}
Euler elrEl = 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;
// MATCH6 part of math proofcount
// calls Implies::stringf
if (r.Length > 0 && (r[r.Length - 1] == '.' || r[r.Length - 1] == ';')) {
if (r[0] != ' ') {
r.Insert(0, '{');
r[r.Length - 1] = '}';
}
else {
r.Insert(0, '[');
r[r.Length - 1] = ']';
}
}
r.Append(' ');
r.Append(deref().cverb);
if (n % 2 == 0) {
r.Append('\n');
for (int i = n; i >= 0; i--) r.Append(" ");
n++;
}
else r.Append(' ');
int i2 = r.Length;
// see Implies::stringf2);
if (!sv && subj != null) r.Append('.');
else {
r.Append(';');
elrEl = near;
while (elrEl != null) {
r.Append(' ').Append(elrEl.deref().cverb).Append(' ');
bool test = true ;
if ((elrEl.subj.ToString() != null))
{
test = test && true;
}
else
{
test = false;
}
if (elrEl.obj.ToString() != null)
{
test = test && true;
}
else
{
test = false;
}
r.Append(
elrEl.obj.stringf(
test
,
n++
)
);
r.Append(';');
elrEl = elrEl.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, 0);
}
public String CheckPrefixes(String s)
{
return ""; // here we should look up in all the models, what the prefix might be and expand it.
/*
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";
*/
}
public String toURI(Euler elrEl) {
if (elrEl.verb == "^^") elrEl = elrEl.subj;
if (elrEl.obj != null) {
StringBuilder sb = new StringBuilder("data:,");
for (IEnumerator en = (IEnumerator) hshtNs.Keys.GetEnumerator(); en.MoveNext(); ) {
Object nsx = en.Current;
sb.Append("@prefix ").Append(nsx).Append(' ').Append(hshtNs[nsx]).Append(".\n");
}
for (Euler eu = elrEl; eu != null; eu = eu.near) sb.Append(eu);
return sb.ToString();
}
else if (elrEl.verb.Equals("this")) return baseURI;
else {
String p = CheckPrefixes(elrEl.verb);
if (p != "")
{
return p;
}
else
{
String s = elrEl.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;
}
}
}
public 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();
}
public String fromWeb(String uri) {
r.Debug ("fromweb uri called" + uri);
try
{
StringBuilder sb = new StringBuilder();
String rl = null;
// could be data
if (uri.StartsWith("data:")) return uri.Substring(uri.IndexOf(',') + 1);
else if (uri.StartsWith("http:")) {
try {
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;
}
Console.Error.WriteLine("Going to open TCP CLIENT!");
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 {
r.Debug("Goint to open some reader!");
StreamReader br = new StreamReader(uri.Substring(6));
while ((rl = br.ReadLine()) != null) {
sb.Append(rl);
sb.Append('\n');
}
}
}
catch (Exception) {
if (uri.StartsWith("http://localhost")) throw new SystemException(uri);
return uri; // # TODO : this is a problem
//#fromWeb("http://localhost/AskJena?fromWeb=" + (!local?uri:uri.Substring(6)));
}
}
else {
r.Debug("Goint to open some file!");
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] != '/'?path:"") + uri;
StreamReader br = new StreamReader(uri);
while ((rl = br.ReadLine()) != null) {
sb.Append(rl);
sb.Append('\n');
}
}
catch (Exception) {
return uri;
// fromWeb("http://localhost/AskJena?fromWeb=" + uri); TODO!
}
}
return sb.ToString();
}
catch (Exception e) {
Report.StackTrace(e.StackTrace);
}
return "error:unresolvedUri"; // this is into the error namespace!
}
/// Main method invoked via Euler
/// [-think] [-trace] axiom ... lemma
[STAThread]
public static void Main(String[] args) {
if (args.Length == 0)
{
Report.Args();
}
else {
try {
step = 1;
trace = false;
think = false;
bool twice = false;
TextWriter outp = Console.Out;
Euler e = new Euler();
engine = 1;
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("-step")) mstep = Int64.Parse(args[++j]);
else if (args[j].EndsWith("-local")) local = true;
else if (args[j].EndsWith("-twice")) twice = 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] + '>'))); // line 1108
}
e.Prepare();
{
Report.Parse(engine,args[n]);
}
// Here the proof mechanism is called
if (twice) e.Proof(e.toURI(np.Parse('<' + args[n] + '>')));
outp.WriteLine(e.Proof(e.toURI(np.Parse('<' + args[n] + '>'))));
if (outp != Console.Out) outp.Close();
}
catch (Exception e) {
Report.StackTrace(e.StackTrace);
}
}
}
} // end of the class Euler,
public class RdfNode
{
public RdfNode copy(){ return this; }
};
public class RdfFieldRef
{
};
public class EulerCollection
{
public RdfNodeIterator getFirst(){return new RdfNodeIterator();}
public virtual RdfNode append(RdfNode rNew){return rNew;}
};
public class RdfNodeIterator
{
// public virtual RdfNode getNext(){ TODO }
public RdfNodeIterator()
{
}
}
public class RdfData
{
};
public class EulerProver
{
};