reg.py

#!/usr/bin/env nix-shell
#! nix-shell -p python27Packages.attrs -i python

import attr

@attr.s
class Term(object):
    predicate = attr.ib()
    arguments = attr.ib()

def parseTerm(text):
    pred, argPile = text.split("(", 1)
    # Hack!
    args = [t.strip(" )") for t in argPile.split(",")]
    return Term(predicate=pred.strip(), arguments=args)

@attr.s
class Decl(object):
    name = attr.ib()
    ty = attr.ib()

def parseDecl(t):
    name, ty = t
    return Decl(name=name.strip(), ty=ty.strip())

def parseBody(text):
    conj = []
    while "&" in text:
        t, text = text.split("&", 1)
        conj.append(t.strip())
    conj.append(text)
    return [parseTerm(t.strip()) for t in conj]

@attr.s
class Formula(object):
    context = attr.ib()
    terms = attr.ib()

@attr.s
class Rule(object):
    context = attr.ib()
    assume = attr.ib()
    conclude = attr.ib()

def parse(text):
    head, body = text.split("|", 1)
    headTerms = head.split(",")
    context = [parseDecl(t.split(":", 1)) for t in headTerms]
    if "=>" in body:
        before, after = body.split("=>", 1)
        return Rule(context=context, assume=parseBody(before), conclude=parseBody(after))
    else:
        bodyTerms = parseBody(body)
        return Formula(context=context, terms=bodyTerms)

def gismuType(g, i):
    if i == 0:
        return "lo " + g
    else:
        return "lo " + ["se ", "te ", "ve ", "xe "][i - 1] + g

def gismu(g, arity):
    names = [g[0] + str(i + 1) for i in range(arity)]
    decls = [Decl(name=n, ty=gismuType(g, i)) for i, n in enumerate(names)]
    term = Term(predicate=g, arguments=names)
    return Formula(context=decls, terms=[term])

arities = {
    # danlu
    "cinfo": 2,
    "mlatu": 2,
    # skari
    "blabi": 1,
}
basis = {g: gismu(g, arity) for g, arity in arities.iteritems()}

if __name__ == "__main__":
    import sys
    import pprint
    text = sys.argv[-1]
    f = parse(text)
    print f
    pprint.pprint(basis)

Try something like 'x :lo mlatu, y :lo se mlatu | mlatu(x, y) & xunre(x)'.