"""n3absyn.py -- exploring Notation3 (N3) abstract syntax
Part 1: convert to lisp-ish JSON structure
Part 2: generate ACL2 lisp s-expression from JSON structure
in progress: IKL s-expressions
Part 3: generate XML from JSON structure, following RIF design sketches
Part 4: generate MathML from JSON structure
So far, we handle just the N3-rules subset of N3;
we deal with:
{ ... } => { ... }
but not other occurrences of {}.
References:
AI: A Modern Approach by Stuart Russell and Peter Norvig
AIMA Python file: logic.py Jul 18, 2005
http://aima.cs.berkeley.edu/python/logic.html
ACL 2 seminar at U.T. Austin: Toward proof exchange in the Semantic Web
Submitted by connolly on Sat, 2006-09-16
http://dig.csail.mit.edu/breadcrumbs/node/160
[RIF] Extensible Design: Horn semantics and syntax actions completed
Boley, Harold (Thursday, 14 September)
http://lists.w3.org/Archives/Public/public-rif-wg/2006Sep/thread.html#msg35
N3 Syntax and Semantics
a sketch by Dan Connolly
http://dig.csail.mit.edu/2006/Papers/TPLP/n3absyn.html
Notation 3 Logic
a draft by TimBL and others
http://www.w3.org/DesignIssues/N3Logic
MathML musings...
import functions and operators from MathML rather than XPath/XQuery? (valueTesting)
02 Jun 2005
http://lists.w3.org/Archives/Public/public-rdf-dawg/2005AprJun/0304
-> http://www.w3.org/2001/sw/DataAccess/mathml-rules.xml
inference rule markup?
12 Feb 2001
http://lists.w3.org/Archives/Public/spec-prod/2001JanMar/0024.html
Note HELM seems to be still going...
http://helm.cs.unibo.it/software/index.html
inference rule markup in W3C specs?
11 Apr 2002
http://lists.w3.org/Archives/Public/www-math/2002Apr/0044.html
"""
__version__ = '$Id: n3absyn.py,v 1.15 2007/06/26 02:36:15 syosi Exp $'
import sys
from swap import uripath, llyn, formula, term
def main(argv):
"""Usage: n3absyn.py foo.n3 --pprint | --lisp | --rif | --mathml
--pprint to print the JSON structure using python's pretty printer
--lisp to print a lisp s-expression for use with ACL2
--rif for Rule Interchange Format (RIF)
--mathml for MathML
"""
path = argv[1]
addr = uripath.join(uripath.base(), path)
kb = llyn.RDFStore()
f = kb.load(addr)
j = json_formula(f)
if '--pprint' in argv:
import pprint
pprint.pprint(j)
elif '--lisp' in argv:
for s in lisp_form(j):
sys.stdout.write(s)
elif '--ikl' in argv:
for s in ikl_sentence(j, []):
sys.stdout.write(s)
elif '--rif' in argv:
for s in xml_form(j):
sys.stdout.write(s)
elif '--mathml' in argv:
for s in mathml_top():
sys.stdout.write(s)
for s in mathml_form(j):
sys.stdout.write(s)
elif '--defns' in argv:
# split top-level N3 constructs
assert(j[0]) == 'forall'
assert(j[2][0]) == 'and'
for s in mathml_top():
sys.stdout.write(s)
sys.stdout.write('\n')
sys.stdout.write('
defns\n')
sys.stdout.write('\n')
sys.stdout.write("\n")
for expr in j[2][1:]:
sys.stdout.write("- \n")
for s in mathml_form(expr):
sys.stdout.write(s)
sys.stdout.write("
\n")
sys.stdout.write("
\n")
sys.stdout.write("\n")
sys.stdout.write("\n")
def json_formula(fmla, vars={}):
"""reduce a swap.formula.Formula to a JSON structure,
i.e. strings, ints, lists, and dictionaries
"""
varnames = {}
varnames.update(vars)
# find distinct names for each variable
for v in fmla.existentials() | fmla.universals():
try:
vn = v.uri
if '#' in vn: vn = vn.split('#')[1]
except AttributeError:
try:
vn = "g%d" % v.serial
except AttributeError:
vn = v.fragid
i = 0
while vn in varnames.values():
i += 1
vn = vn + `i`
varnames[v] = vn
parts = [] # conjuncts
for s in fmla: # iterate over statements. hmm.
# this is the N3rules subset, for now...
# when we get n3-quote figured out, we can take this special-case out.
if s.predicate().uriref() == 'http://www.w3.org/2000/10/swap/log#implies':
parts.append({'op': 'implies',
'parts': [json_formula(s.subject(), varnames), #@@
json_formula(s.object(), varnames)]
})
else:
parts.append({'op': 'holds',
'parts': [json_term(s.predicate(), varnames),
json_term(s.subject(), varnames),
json_term(s.object(), varnames)]})
if len(parts) == 1:
ret = parts[0]
else:
ret = {'op': 'and', 'parts': parts}
if fmla.universals():
ret = {'Q': 'forall',
'Vars': [varnames[v] for v in fmla.universals()],
'f': ret}
if fmla.existentials():
ret = {'Q':'exists',
'Vars': [varnames[v] for v in fmla.existentials()],
'f': ret}
return ret
def json_term(t, varmap):
"""reduce a swap.term to a JSON structure,
i.e. strings, ints, lists, and dictionaries
"""
if t in varmap:
return {'var': varmap[t]}
elif isinstance(t, term.Literal):
if t.datatype:
dt = t.datatype.uriref()
if dt in(DT.integer,
DT.nonNegativeInteger):
return int(t.string)
if dt == DT.double:
return float(t.string)
return {'op': 'data', 'parts': [{'op': dt}, t.string]}
else:
return t.string
elif isinstance(t, term.LabelledNode): # ugh.
return {'op': t.uriref()}
# hmm... are lists part of the N3 abstract syntax?
elif isinstance(t, term.List):
return [json_term(i, varmap) for i in t]
elif isinstance(t, term.N3Set):
return {'op': 'n3-set', 'parts': [json_term(i, varmap) for i in t]}
elif isinstance(t, formula.Formula):
return {'op': 'n3-quote', 'parts': [json_formula(t, varmap)]}
else:
raise RuntimeError, "huh? + %s %s" % (t, t.__class__)
def lisp_form(f):
"""generate an s-expression from a formula JSON structure.
"""
# integer
if type(f) is type(1):
yield "%d " % f
elif type(f) is type(1.1):
yield "%f " % f
# string
elif type(f) in (type(''), type(u'')):
if "\\" in f or '"' in f:
raise RuntimeError, 'commonlisp string quoting TODO: %s' % f
# @@ hmm... non-ascii chars?
yield '"%s" ' % f
# list
elif type(f) is type([]):
yield '(list '
for expr in f:
for s in lisp_form(expr):
yield s
yield ')\n'
elif type(f) is type({}):
# variable
if 'var' in f:
yield f['var'] #@@ quoting?
yield ' '
return
elif 'op' in f:
head = f['op']
# URI, i.e. a 0-ary function symbol
if ':' in head:
if '|' in head:
raise RuntimeError, \
"quoting | in symbols not yet implemented"
yield '(URI::|%s|' % head
rest = f.get('parts', [])
assert(len(rest) == 0)
# function symbols
#@@ interaction of n3-quote with variables needs work.
elif head in ('holds', 'data', 'n3-quote'):
yield '('
yield head
yield ' '
rest = f['parts']
# connectives
elif head in ('and', 'implies'):
yield '('
yield head
yield ' '
rest = f['parts']
# quantifiers
elif 'Q' in f:
head = f['Q']
yield '('
yield head
yield ' ('
for v in f['Vars']:
yield v
yield ' '
yield ')\n'
rest = [f['f']]
else:
raise RuntimeError, 'unimplemented list head: %s' % head
for expr in rest:
for s in lisp_form(expr):
yield s
yield ')\n'
else:
raise RuntimeError, 'unimplemented syntactic type: %s %s' % (f, type(f))
def ikl_sentence(f, subscripts):
"""generate an IKL s-expression from a formula JSON structure.
IKL Specification Document
Pat Hayes, IHMC & Chris Menzel, TAMU
On behalf of the IKRIS Interoperability Group
rev July 20 2006
http://www.ihmc.us/users/phayes/IKL/SPEC/SPEC.html
"""
if 'op' in f:
head = f['op']
if head == 'holds':
yield '('
yield head
yield ' '
for t in f['parts']:
for s in ikl_term(t, subscripts):
yield s
yield ')\n'
return
# connectives
elif head in ('and', 'implies'):
if head == 'implies': head = 'if'
yield '('
yield head
yield ' '
rest = f['parts']
# quantifiers
elif 'Q' in f:
head = f['Q']
yield '('
yield head
yield ' ('
for v in f['Vars']:
yield v
yield ' '
yield ')\n'
rest = [f['f']]
else:
raise RuntimeError, 'unimplemented IKL sentence head: %s' % head
for expr in rest:
for s in ikl_sentence(expr, subscripts):
yield s
yield ')\n'
def ikl_term(f, subscripts):
"""generate an IKL term s-expression from a formula JSON structure.
"""
# integer
if type(f) is type(1):
yield "%d " % f
elif type(f) is type(1.1):
#@@refactor ikl_data()?
yield "(xsd:double %f)" % f #@@long uri form
# string
elif type(f) in (type(''), type(u'')):
if "\\" in f or '"' in f:
raise RuntimeError, 'string quoting TODO: %s' % f
if subscripts:
yield "('%s' " % f # string
sub = subscripts[0]
s2 = subscripts[1:]
if s2:
for s in ikl_term(sub, s2):
yield s
yield ") "
else:
yield "%s) " % sub
else:
yield "'%s' " % f
# list
elif type(f) is type([]):
yield '(list '
for expr in f:
for s in ikl_term(expr, subscripts):
yield s
yield ')\n'
elif type(f) is type({}):
# variable.
if 'var' in f:
yield f['var'] #@@ quoting?
yield ' '
return
elif 'op' in f:
head = f['op']
# URI, i.e. a 0-ary function symbol
if ':' in head:
if '"' in head:
raise RuntimeError, \
"quoting \" in IKL names not yet implemented"
if subscripts:
for s in ikl_term(head, subscripts):
yield s
else:
yield '"%s" ' % head
rest = f.get('parts', [])
assert(len(rest) == 0)
return
# function symbols
# data
elif head == 'data':
ty, lit = f['args']
yield '("%s" \'%s\') ' % (ty['op'], lit) #@@ escaping
return
elif head == 'n3-set':
yield '(n3-set '
rest = f['parts']
elif head == 'n3-quote':
yield '(that '
for s in ikl_sentence(f['parts'][0],
['c%d' % id(f)] + subscripts):
yield s
yield ') '
return
else:
raise RuntimeError, 'unimplemented IKL term head: %s' % head
for expr in rest:
for s in ikl_term(expr):
yield s
yield ')\n'
else:
raise RuntimeError, 'unimplemented syntactic type: %s %s' % (f, type(f))
from xml.sax.saxutils import escape
def xml_form(f):
"""generate XML version of JSON formula f
see http://www.w3.org/2005/rules/wg/wiki/CORE
and http://www.w3.org/2005/rules/wg/wiki/B.1_Horn_Rules
"""
# integer
if type(f) is type(1):
#@@ I'm making up type; I don't see it in the draft
yield '%d\n' % (DT.integer, f)
elif type(f) is type(1.1):
yield '%f\n' % (DT.double, f)
# string
elif type(f) in (type(''), type(u'')):
yield ''
yield escape(f)
yield '\n'
# list function symbol
elif type(f) is type([]):
yield "list\n"
for part in f:
for s in xml_form(part):
yield s
yield "\n"
elif type(f) is type({}):
# variable
if 'var' in f:
yield "%s\n" % f['var']
elif 'op' in f:
head = f['op']
# URI, i.e. a 0-ary function symbol
if ':' in head:
assert(len(f.get('args', [])) == 0)
yield '\n'
# data
elif head == 'data':
ty, lit = f['args']
yield '' % ty['op']
yield escape(lit)
yield ""
elif head == 'n3-quote':
raise RuntimeError, 'n3-quote not yet implemented'
# Atomic formula
elif head == 'holds':
yield "holds\n"
for part in f.get('parts', []):
for s in xml_form(part):
yield s
yield "\n"
# connectives
elif head in ('and', 'implies'):
tagname = {'and': 'And',
'implies': 'Implies'}[head]
yield "<%s>\n" % tagname
for part in f.get('parts', []):
for s in xml_form(part):
yield s
yield "%s>\n" % tagname
# quantifiers
elif 'Q' in f:
tagname = {'exists': 'Exists',
'forall': 'Forall', #@@
}[f['Q']]
if tagname == 'Forall':
#@@hmm... treat other vars as implicitly universally quanitified?
#@@how to assert that we're at the top level?
for s in xml_form(f['f']):
yield s
else:
yield "<%s>\n" % tagname
for v in f['Vars']:
yield "%s" % v
yield '\n'
for s in xml_form(f['f']):
yield s
yield "%s>\n" % tagname
else:
raise RuntimeError, 'unimplemented list head: %s' % head
else:
raise RuntimeError, 'unimplemented syntactic type: %s %s' % (f, type(f))
def mathml_top():
yield ''
# hmm... local or global link?
#yield '\n'
yield '\n'
def mathml_form(f):
"""generate MathML version of JSON formula
"""
yield '\n"
def mathml_fmla(f):
"""generate MathML version of JSON formula
"""
if type(f) is type([]):
yield "\n"
for part in f:
for s in mathml_fmla(part):
yield s
yield "
\n"
elif type(f) is type({}):
if 'Q' in f:
q = f['Q']
yield "\n" \
"<%s/>\n" % q
for v in f['Vars']:
# per 5 Using definitionURL for Bound Variable Identification.
# http://www.w3.org/TR/mathml-bvar/#proposal
yield '%s\n' % (v, v)
for s in mathml_fmla(f['f']):
yield s
yield "\n"
elif 'op' in f:
head = f['op']
if head == 'holds':
# Not only are we not using a holds predicate,
# but we're going classes as unary predicates.
if f['parts'][0]['op'] == RDF.type:
args = [f['parts'][2], f['parts'][1]]
else: args = f['parts']
yield "\n"
for part in args:
for s in mathml_fmla(part):
yield s
yield "\n"
elif ':' in head:
assert(len(f.get('parts', [])) == 0)
u = f['op']
try:
ln = u.split("#")[1]
except IndexError:
ln = u
yield ''
yield escape(ln)
yield '\n'
else:
#hmm... n3-quote...
yield "<%s/>\n" % head
for part in f.get('parts', []):
for s in mathml_fmla(part):
yield s
yield "\n"
# variable
elif 'var' in f:
v = f['var']
yield '%s\n' % (v, v)
# integer
elif type(f) is type(1):
yield '%d\n' % f
elif type(f) is type(1.1):
yield '%f\n' % f
# string
elif type(f) in (type(''), type(u'')):
yield ''
yield escape(f)
yield '\n'
else:
raise RuntimeError, 'unimplemented syntactic type: %s %s' % (f, type(f))
class Namespace(object):
def __init__(self, nsname):
self._ns = nsname
def __getattr__(self, ln):
return self._ns + ln
DT = Namespace('http://www.w3.org/2001/XMLSchema#')
RDF = Namespace('http://www.w3.org/1999/02/22-rdf-syntax-ns#')
if __name__ == '__main__':
main(sys.argv)