""" Describe an otterlang formula (or KB) using RDF triples $Id: describe.py,v 1.6 2002/08/09 02:16:21 sandro Exp $ """ import parse import sys, types # where to find these? look up! sys.path.append('..') sys.path.append('.') # or maybe we're run from up here? import rdf import pt scope = {} # varPrefix = "http://www.w3.org/2002/05/positive-triples/var#" varPrefix = "#" prefixTable = { "default": "#", "rdf": "http://www.w3.org/1999/02/22-rdf-syntax-ns#", "pt": "http://www.w3.org/2002/05/positive-triples/v2", } def addTriple(t): global scope print rdf.asNTriples([t], scope), def varns(s): # @@ assume it's short, pretty, etc.... global varPrefix return varPrefix+s def describeTermList(t, sink, sym="New", vars="New"): if vars == "New": vars = {} if t == []: if sym!="New": raise RuntimeError, 'Cannot describe empty list with given symbol' else: return rdf.nil if sym == "New": sym = rdf.Ident() sink([sym, rdf.first, describeTerm(t[0], sink, vars=vars)]) sink([sym, rdf.rest, describeTermList(t[1:], sink, vars=vars)]) return sym def describeTerm(t, sink, sym="New", vars="New"): if sym == "New": sym = rdf.Ident() if vars == "New": vars = {} if isinstance(t, types.StringType): if vars.has_key(t): sym.setURI(varns(t)) return sym if t[0] == "'": if t[0:2] == "'<" and t[-2:] == ">'": uri = t[2:-2] else: raise RuntimeError, 'Bad syntax symbol: "%s"' % t else: prefix = "default" try: (prefix, main) = t.split("_", 1) except ValueError: main = t try: expanded = prefixTable[prefix] uri = expanded+main except KeyError: raise (RuntimeError,'No expanstion defined for prefix ("%s"), ' 'used in symbol: "%s"' % (prefix, t)) # BUG: check uri syntax on main? constant = rdf.Ident().setURI(uri) sink([sym, pt.denotation, constant]) sink([sym, rdf.type, pt.Constant]) else: sink([sym, pt.args, describeTermList(t, sink, vars=vars)]) return sym def describeFormula(t, sink, sym="New", vars="New"): if sym == "New": sym = rdf.Ident() if vars == "New": vars = {} if isinstance(t, types.StringType): raise RuntimeError, ("describeFormula called with a string ('%s')" % t) if t[0] == 'rdf': sink([sym, rdf.type, pt.Triple]) sink([sym, pt.subjectTerm, describeTerm(t[1], sink, vars=vars)]) sink([sym, pt.predicateTerm, describeTerm(t[2], sink, vars=vars)]) sink([sym, pt.objectTerm, describeTerm(t[3], sink, vars=vars)]) elif t[0] == '&': left = rdf.Ident() right = rdf.Ident() sink([sym, rdf.type, pt.Conjunction]) sink([sym, pt.conjLeft, left]) sink([sym, pt.conjRight, right]) describeFormula(t[1], sink, left, vars) describeFormula(t[2], sink, right, vars) elif t[0] == '|': left = rdf.Ident() right = rdf.Ident() sink([sym, rdf.type, pt.Disjunction]) sink([sym, pt.disjLeft, left]) sink([sym, pt.disjRight, right]) describeFormula(t[1], sink, left, vars) describeFormula(t[2], sink, right, vars) elif t[0] == '->': left = rdf.Ident() right = rdf.Ident() sink([sym, rdf.type, pt.Conditional]) sink([sym, pt.condLeft, left]) sink([sym, pt.condRight, right]) describeFormula(t[1], sink, left, vars) describeFormula(t[2], sink, right, vars) elif t[0] == '<->': left = rdf.Ident() right = rdf.Ident() sink([sym, rdf.type, pt.Biconditional]) sink([sym, pt.bicondLeft, left]) sink([sym, pt.bicondRight, right]) describeFormula(t[1], sink, left, vars) describeFormula(t[2], sink, right, vars) elif t[0] == '-': negated = rdf.Ident() sink([sym, rdf.type, pt.Negation]) sink([sym, pt.negated, negated]) describeFormula(t[1], sink, negated, vars) elif t[0] == '$Quantified': varList = t[1:-1] opList = [] for v in varList: if v == "all": universal = 1; continue if v == "exists": universal = 0; continue; # @@@ switch to a local copy of vars vars[v] = vars.get(v, 0) + 1 opList = [[universal, v]]+ opList sf = describeFormula(t[-1], sink, vars=vars) for op in opList: if op == opList[-1]: f = sym else: f = rdf.Ident() sink([f, rdf.type, pt.Quantification]) v = describeTerm(op[1], sink, vars=vars) sink([f, pt.var, v]) if op[0]: sink([v, rdf.type, pt.UniVar]) else: sink([v, rdf.type, pt.ExiVar]) sink([f, pt.subformula, sf]) sf = f else: sink([sym, rdf.type, pt.AtomicFormula]) sink([sym, pt.terms, describeTermList(t, sink, vars=vars)]) #else: # raise RuntimeError, 'Unknown FOL Construct Tag: '+t[0] return sym # assertKB? def describeContentsOfKB(kb, sink): for f in kb: # skip over otter syntactic hacks, if we get any if f[0] in ['formula_list', 'end_of_list', 'set']: continue fsym = rdf.Ident() sink([fsym, rdf.type, pt.TrueSentence]) describeFormula(f, sink, fsym) if __name__ == "__main__": kb = parse.parse("inputDocument", sys.stdin.read()) if kb == None: raise RuntimeError, 'syntax error' else: print "@prefix var: <%s>."%varPrefix print "@prefix pt: <%s>."%pt.ptns describeContentsOfKB(kb, addTriple) # $Log: describe.py,v $ # Revision 1.6 2002/08/09 02:16:21 sandro # can now describe arbitrary predicates and functions # # Revision 1.5 2002/08/08 20:02:04 sandro # added handling for uris in formulas, added single-stage loopback testing for canonical samples # # Revision 1.4 2002/08/07 19:58:53 sandro # library for interacting with otter # # Revision 1.3 2002/08/02 20:34:38 sandro # started adding support for arbitrary predicates # # Revision 1.2 2002/08/01 19:31:26 sandro # passes syntactic loopback tests # # Revision 1.1 2002/08/01 19:08:51 sandro # early versions, some moved from parent dir in re-organization # # Revision 1.2 2002/08/01 15:04:22 sandro # work with less whitespace, and disjunction; test case: (a | b) and (a&b). # # Revision 1.1 2002/07/29 20:37:40 sandro # Turn otter FOL into PTL triples saying the same thing #