continuations.py

from rpython.rlib.rstacklet import StackletThread
from rpython.rlib.objectmodel import specialize
import core

class SThread(StackletThread):
    def __init__(self, config):
        StackletThread.__init__(self, config)
        self.cont = None

def get_sthread():
    ec = core.get_ec()
    if not ec.sthread:
        ec.sthread = SThread(ec.config)
    return ec.sthread

# Continuation represents either live or empty continuation.
# It is never 'blank', assuming you call 'init' immediately after positioning the continuation.
class Continuation(object):
    def __init__(self):
        self.sthread = sthread = get_sthread()
        self.h = sthread.get_null_handle()
        self.gate = False

    def is_empty(self):
        return self.sthread.is_empty_handle(self.h) or not self.gate

    def init(self, callback):
        sthread = self.sthread
        assert sthread.cont is None
        sthread.cont = self
        self.h = sthread.new(callback)

    def switch(self):
        sthread = get_sthread()
        assert not self.is_empty(), "not so fatal error: empty switch continuation"
        self.h = sthread.switch(self.h)

    @staticmethod
    def wrapped_callback(callback):
        def _wrapped_callback(head, arg):
            sthread = get_sthread()
            this, sthread.cont = sthread.cont, None
            this.h = head
            this.gate = True
            cont = callback(this)
            assert not cont.is_empty(), "fatal error: empty return continuation"
            cont.gate = False
            return cont.h
        _wrapped_callback.__name__ = callback.__name__
        return _wrapped_callback 

core.py

from rpython.rlib.rthread import ThreadLocalReference
from continuations import Continuation

class ExecutionContext:
    def __init__(self, config):
        self.config = config
        self.sthread = None
        self.spawn_pool = []
        self.running = []
        self.scheduler = None # Start in scheduler.

class GlobalState:
    ec = ThreadLocalReference(ExecutionContext, loop_invariant=True)

g = GlobalState()

def init_executioncontext(*args):
    ec = ExecutionContext(*args)
    g.ec.set(ec)

def get_ec():
    ec = g.ec.get()
    if isinstance(ec, ExecutionContext):
        return ec
    import os
    os.write(2, "Threads don't support get_ec now.\n")
    assert False, "failure" 

goal_standalone.py

import os
import core
import interpreter
import inference
from ukanren import (walk, Term, Var, Const, var_to_const, const_to_var,
                     eq, empty, fresh, disj, conj,
                     get_constraints, constraint)
import parser

@interpreter.proc("greeting", Term("1", []), [])
def greeting(arg):
    #arg.recv()
    os.write(1, "Hello\n")

class MicroModule(object):
    def __init__(self):
        self.entries = [greeting]

    def lookup(self, name):
        for entry in reversed(self.entries):
            if entry.name == name:
                return entry

def entry_point(config):
    def __impl__(argv):
        core.init_executioncontext(config)

        module = MicroModule()
        if len(argv) == 2:
            filename = argv[1]
            fd = os.open(filename, os.O_RDONLY, 0777)
            source = os.read(fd, 64000).decode('utf-8')
            t = parser.Tokenizer(parser.Parser())
            for char in source:
                parser.read_char(t, char)
            output = parser.read_done(t)
            if output is None:
                assert False
            os.write(1, "success\n")
            output = parser.file_to_list(output, [])
            typedecls = parser.list_to_typedecls(output)
            decls = parser.list_to_decls(output)
            for name in typedecls:
                os.write(1, name + " : " + typedecls[name].to_str() + "\n")
            for name, uq, code in decls:
                os.write(1, name + " !!! " + uq.to_str() + " !!! " + code.to_str() + "\n")

            for name, uq, code in reversed(decls):
                state = empty()
                # handle self-references
                type, state = fresh(state)
                decl = interpreter.Declaration(module, name, None, type, [])
                module.entries.append(decl)

                decl.body = interpreter.decl_to_code(uq, code, module)

                expr = inference.InferCode(decl.body, [type], [])
                if name in typedecls:
                    expr = conj(expr, eq(type, typedecls[name]))

                nstates = expr.go(state)
                if len(nstates) >= 1:
                    nstate = nstates[0]
                    table = {}
                    decl.type, table = var_to_const(walk(type, nstate.subst), table)
                    typename = decl.type.to_str()
                    os.write(1, name + " : " + typename)
                    sp = " <= "
                    for cnt in get_constraints(nstate):
                        cnt, table = var_to_const(walk(cnt, nstate.subst), table)
                        decl.constraints.append(cnt)
                        os.write(1, " %s%s" % (sp, cnt.to_str()))
                        sp = " ∧ "
                    os.write(1, "\n")
                else:
                    module.entries.remove(decl)
                    os.write(2, name + " not installed due to type error\n")

        # dummy function to let inference engine figure out the pieces.
        #func1 = [
        #    i.Op("split", [[i.Op("exch", [])], [i.Op("exch", [])]]),
        #    i.Op("cur", [[i.Op("exch", [])]]),
        #    i.Op("alt", [[i.Op("exch", [])], [i.Op("exch", [])]]),
        #    i.Op("make", [[i.Op("exch", [])], [i.Op("exch", [])], [i.Op("exch", [])]]),
        #    ]
        #body = [i.Op("app", []), i.Op("exch", []), i.Op("split", [[greeting], []])]
        #inp = Term("⊗", [Term("1", []),
        #                 Term("⊸", [Term("1", []), Term("⊥", [])])])
        #outp = Term("⊥", [])

        main = module.lookup("main")
        if main is None:
            os.write(2, "main not installed\n")
            return 1

        state = empty()
        table = {}
        v = Term("+", [Term("1", []), Term("1", [])])
        t, table, state = const_to_var(main.type, table, state)
        expr = eq(v, t)
        for cnr in main.constraints:
            cnr, table, state = const_to_var(cnr, table, state)
            expr = conj(expr, constraint(cnr))
        nstates = expr.go(state)
        if len(nstates) == 1:
            nstate = nstates[0]

            retarg, arg = interpreter.port()
            interpreter.spawn(main.body, [arg], [], main)

            interpreter.scheduler_main_loop()

            if isinstance(retarg.value, interpreter.Choice):
                if retarg.value.index:
                    os.write(1, "Success\n")
                else:
                    os.write(1, "Failure\n")

        else:
            os.write(2, "'main' type does not match an entry point\n")
            os.write(2, "  %s\n" % t.to_str())
            os.write(2, "  %s\n" % v.to_str())

        exit_status = 0
        os.write(1, "Bye\n")
        return exit_status
    return __impl__

def target(driver, args):
    driver.exe_name = "lever2"
    force_config(driver.config)
    return entry_point(driver.config), None

def force_config(config):
    config.translation.continuation = True
    config.translation.thread = True

if __name__=="__main__":
    from rpython.config.translationoption import get_combined_translation_config
    import sys
    config = get_combined_translation_config(translating=True)
    force_config(config)
    sys.exit(entry_point(config)(sys.argv)) 

inference.py

from ukanren import (walk, Term, Var, Const, Combinator, const_to_var,
                     eq, empty, fresh, disj, conj, tt, ff, constraint,
                     tensor, par, plus, band, ofc, que,
                     unit, zero, top, bot, dual)
import interpreter
from interpreter import (Id, Falsum, Par, Select, Qu, Unit, Tensor,
                         Case, Ofc, Cut, Ax, Call, Impossible)

class InferCode(Combinator):
    def __init__(self, code, reg, args):
        self.code = code
        self.reg = reg
        self.args = args

    def go(self, state):
        code = self.code
        reg = self.reg
        args = self.args
        #import os
        #os.write(2, "infer: " + code.to_str() + "\n")
        if isinstance(code, Id):
            return InferCode(code.body, reg, args).go(state)
        elif isinstance(code, Falsum):
            arg = infer_lookup(reg, args, code.arg)
            return conj(
                eq(arg, bot),
                InferCode(code.body, reg, args)).go(state)
        elif isinstance(code, Par):
            arg = infer_lookup(reg, args, code.arg)
            x, state = fresh(state)
            y, state = fresh(state)
            reg = reg + [x, y]
            a = eq(arg, par(x, y))
            b = InferCode(code.body, reg, args)
            return conj(a, b).go(state)
        elif isinstance(code, Select):
            arg = infer_lookup(reg, args, code.arg)
            x, state = fresh(state)
            y, state = fresh(state)
            if code.which:
                reg = reg + [y]
            else:
                reg = reg + [x]
            return conj(
                eq(arg, plus(x, y)),
                InferCode(code.body, reg, args)).go(state)
        elif isinstance(code, Qu):
            arg = infer_lookup(reg, args, code.arg)
            x, state = fresh(state)
            args = [x] + args
            return conj(
                eq(arg, que(x)),
                InferCode(code.body, reg, args)).go(state)
        elif isinstance(code, Unit):
            arg = infer_lookup(reg, args, code.arg)
            return eq(arg, unit).go(state)
        elif isinstance(code, Tensor):
            arg = infer_lookup(reg, args, code.arg)
            x, state = fresh(state)
            y, state = fresh(state)
            reg = reg + [x, y]
            return conj(
                eq(arg, tensor(x, y)),
                conj(InferCode(code.left, reg, args),
                     InferCode(code.right, reg, args))).go(state)
        elif isinstance(code, Case):
            arg = infer_lookup(reg, args, code.arg)
            x, state = fresh(state)
            y, state = fresh(state)
            reg1 = reg + [x]
            reg2 = reg + [y]
            return conj(
                eq(arg, band(x, y)),
                conj(InferCode(code.left, reg1, args),
                     InferCode(code.right, reg2, args))).go(state)
        elif isinstance(code, Ofc):
            arg = infer_lookup(reg, args, code.arg)
            x, state = fresh(state)
            reg = [x]
            return conj(
                eq(arg, ofc(x)),
                InferCode(code.body, reg, args)).go(state)
        elif isinstance(code, Cut):
            x, state = fresh(state)
            y, state = fresh(state)
            reg = reg + [x, y]
            return conj(
                constraint(dual(x, y)),
                conj(InferCode(code.left, reg, args),
                     InferCode(code.right, reg, args))).go(state)
        elif isinstance(code, Ax):
            a = infer_lookup(reg, args, code.a)
            b = infer_lookup(reg, args, code.b)
            return constraint(dual(a, b)).go(state)
        elif isinstance(code, Call):
            arg = infer_lookup(reg, args, code.arg)
            a, table, state = const_to_var(code.decl.type, {}, state)
            expr = eq(arg, a)
            for cnr in code.decl.constraints:
                cnr, table, state = const_to_var(cnr, table, state)
                expr = conj(expr, constraint(cnr))
            return expr.go(state)
        elif isinstance(code, Impossible):
            arg = infer_lookup(reg, args, code.arg)
            return eq(arg, top).go(state)
        else:
            assert False, code

def infer_lookup(reg, args, arg):
    if arg >= 0:
        return reg[arg]
    else:
        return args[~arg] 

interpreter.py

from rpython.rlib import rvmprof
import core

def decl_to_code(uq, term, module):
    rig = [""]
    args = []
    top = bot = Id(None)
    bot = uq_to_code(0, uq, rig, args, bot)
    nq_to_code(term, rig, args, bot, module)
    full_check(top)
    return top
    
def uq_to_code(reg, uq, rig, args, bot):
    sig = uq.get_signature()
    if len(uq.args) == 0:
        if uq.name == "⊥":
            bot.body = Falsum(reg, None)
            bot = bot.body
        else:
            rig[reg] = uq.name
    elif sig == ";/2":
        bot.body = Par(reg, None)
        bot = bot.body
        x = len(rig)
        y = len(rig) + 1
        rig.append("")
        rig.append("")
        bot = uq_to_code(x, uq.args[0], rig, args, bot)
        bot = uq_to_code(y, uq.args[1], rig, args, bot)
    elif sig == "?/1":
        bot.body = Qu(reg, None)
        bot = bot.body
        args.insert(0, uq.args[0].name)
    elif sig == "↑/1":
        bot.body = Select(False, reg, None)
        bot = bot.body
        x = len(rig)
        rig.append("")
        bot = uq_to_code(x, uq.args[0], rig, args, bot)
    elif sig == "↓/1":
        bot.body = Select(True, reg, None)
        bot = bot.body
        x = len(rig)
        rig.append("")
        bot = uq_to_code(x, uq.args[0], rig, args, bot)
    else:
        assert False
    return bot

def nq_to_code(nq, rig, args, bot, module):
    sig = nq.get_signature()
    if sig == "unit/1":
        arg = lookup(nq.args[0].name, rig, args)
        bot.body = Unit(arg)
    elif sig == "tensor/5":
        uq1 = nq.args[0]
        uq2 = nq.args[1]
        src = lookup(nq.args[2].name, rig, args)
        x = len(rig)
        y = len(rig)+1
        rig.append("")
        rig.append("")
        bot.body = Tensor(src, Id(None), Id(None))
        bot = bot.body
        rig1 = list(rig)
        args1 = list(args)
        bot1 = uq_to_code(x, uq1, rig1, args1, bot.left) 
        nq_to_code(nq.args[3], rig1, args1, bot1, module)
        rig2 = list(rig)
        args2 = list(args)
        bot2 = uq_to_code(y, uq2, rig2, args2, bot.right) 
        nq_to_code(nq.args[4], rig2, args2, bot2, module)
    elif sig == "case/5":
        uq1 = nq.args[0]
        uq2 = nq.args[1]
        src = lookup(nq.args[2].name, rig, args)
        x = len(rig)
        rig.append("")
        bot.body = Case(src, Id(None), Id(None))
        bot = bot.body
        rig1 = list(rig)
        args1 = list(args)
        bot1 = uq_to_code(x, uq1, rig1, args1, bot.left)
        nq_to_code(nq.args[3], rig1, args1, bot1, module)
        rig2 = list(rig)
        args2 = list(args)
        bot2 = uq_to_code(x, uq2, rig2, args2, bot.right)
        nq_to_code(nq.args[4], rig2, args2, bot2, module)
    elif sig == "ofc/3":
        uq = nq.args[0]
        src = lookup(nq.args[1].name, rig, args)
        subrig = [""]
        bot.body = Ofc(src, None)
        bot = uq_to_code(0, uq, subrig, args, bot.body)
        nq_to_code(nq.args[2], subrig, args, bot, module)
    elif sig == "cut/4":
        uq1 = nq.args[0]
        uq2 = nq.args[1]
        x = len(rig)
        y = len(rig)+1
        rig.append("")
        rig.append("")
        bot.body = Cut(Id(None), Id(None))
        bot = bot.body
        rig1 = list(rig)
        args1 = list(args)
        bot1 = uq_to_code(x, uq1, rig1, args1, bot.left)
        nq_to_code(nq.args[2], rig1, args1, bot1, module)
        rig2 = list(rig)
        args2 = list(args)
        bot2 = uq_to_code(y, uq2, rig2, args2, bot.right)
        nq_to_code(nq.args[3], rig2, args2, bot2, module)
    elif sig == "ax/2":
        a = lookup(nq.args[0].name, rig, args)
        b = lookup(nq.args[1].name, rig, args)
        bot.body = Ax(a, b)
    elif sig == "call/2":
        a = lookup(nq.args[1].name, rig, args)
        bot.body = call = Call(nq.args[0].name, a)
        decl = module.lookup(call.name)
        assert decl is not None, ("not found %s" % call.name)
        call.decl = decl

    elif sig == "impossible/2":
        a = lookup(nq.args[0].name, rig, args)
        nargs = []
        for arg in to_list(nq.args[1]):
            nargs.append(lookup(arg.name, rig, args))
        bot.body = Impossible(a, nargs)
    else:
        #import os
        #os.write(2, "weird signature %s\n" % sig)
        assert False, sig

def lookup(name, rig, args):
    #import os
    #os.write(2, "name lookup %s\n" % name)
    if name in rig:
        #os.write(2, "name in rig %s\n" % name)
        return rig.index(name)
    if name in args:
        #os.write(2, "name in args %s\n" % name)
        return ~args.index(name)
    assert False, ("no such variable %s" % name)

def to_list(term):
    sig = term.get_signature()
    #import os
    #os.write(2, "list %s\n" % sig)
    if sig == "[]/0":
        return []
    elif sig == "::/2":
        lst = to_list(term.args[0])
        lst.append(term.args[1])
        return lst
    else:
        assert False

class Code(object):
    pass

class Id(Code):
    def __init__(self, body):
        self.body = body

    def to_str(self):
        return "id " + self.body.to_str()

class Falsum(Code):
    def __init__(self, arg, body): # ⊥ 
        self.arg = arg
        self.body = body

    def to_str(self):
        return "falsum %d %s" % (self.arg, self.body.to_str())

class Par(Code):
    def __init__(self, arg, body): # b ; c
        self.arg = arg
        self.body = body

    def to_str(self):
        return "par %d %s" % (self.arg, self.body.to_str())

class Select(Code):
    def __init__(self, which, arg, body): # b
        self.which = which
        self.arg = arg
        self.body = body

    def to_str(self):
        return "select %d %s" % (self.arg, self.body.to_str())
    
class Qu(Code):
    def __init__(self, arg, body): # ?a
        self.arg = arg
        self.body = body

    def to_str(self):
        return "qu %d %s" % (self.arg, self.body.to_str())

class Unit(Code):
    def __init__(self, arg): # ⊤ 
        self.arg = arg

    def to_str(self):
        return "unit %d" % self.arg

class Tensor(Code):
    def __init__(self, arg, left, right): # b,c
        self.arg = arg
        self.left = left
        self.right = right

    def to_str(self):
        return "tensor %d (%s ⊗ %s)" % (self.arg, self.left.to_str(), self.right.to_str())

class Case(Code):
    def __init__(self, arg, left, right): # x|y
        self.arg = arg
        self.left = left
        self.right = right

    def to_str(self):
        return "case %d (%s ⊓ %s)" % (self.arg, self.left.to_str(), self.right.to_str())

class Ofc(Code):
    def __init__(self, arg, body): # x
        self.arg = arg
        self.body = body

    def to_str(self):
        return "ofc %d (%s)" % (self.arg, self.body.to_str())

class Cut(Code):
    def __init__(self, left, right): # a,b
        self.left = left
        self.right = right

    def to_str(self):
        return "cut (%s ⊗ %s)" % (self.left.to_str(), self.right.to_str())

class Ax(Code):
    def __init__(self, a, b):
        self.a = a
        self.b = b

    def to_str(self):
        return "ax (%d=%d)" % (self.a, self.b)

class Call(Code):
    def __init__(self, name, arg):
        self.name = name
        self.arg = arg
        self.decl = None

    def to_str(self):
        return "call (%d)" % (self.arg)

class Impossible(Code):
    def __init__(self, arg, args):
        self.arg = arg
        self.args = args

    def to_str(self):
        return "impossible %d" % self.arg

# Procedures appear alone in code that's not typechecked.
class Procedure(Code):
    def __init__(self, procedure):
        self.procedure = procedure

def proc(name, type, constraints=[]):
    def __impl__(fn):
        body = Procedure(fn)
        return Declaration(None, name, body, type, constraints)
    return __impl__

def full_check(code):
    rig = check(code, [1], 0)
    assert rig == [0], rig

def check(code, rig, argc):
    #import os
    #os.write(2, "check: " + code.to_str() + "\n")
    if isinstance(code, Id):
        return check(code.body, rig, argc)
    elif isinstance(code, Falsum):
        decrement(rig, argc, code.arg)
        return check(code.body, rig, argc)
    elif isinstance(code, Par):
        decrement(rig, argc, code.arg)
        rig.append(1)
        rig.append(1)
        rig = check(code.body, rig, argc)
        assert rig.pop() == 0, "right par"
        assert rig.pop() == 0, "left par"
        return rig
    elif isinstance(code, Select):
        decrement(rig, argc, code.arg)
        rig.append(1)
        rig = check(code.body, rig, argc)
        assert rig.pop() == 0
        return rig 
    elif isinstance(code, Qu):
        decrement(rig, argc, code.arg)
        return check(code.body, rig, argc+1)
    elif isinstance(code, Unit):
        decrement(rig, argc, code.arg)
        return rig
    elif isinstance(code, Tensor):
        decrement(rig, argc, code.arg)
        x = len(rig)
        y = len(rig)+1
        rig.extend([0,0])
        rig[x] = 1
        rig = check(code.left, rig, argc)
        assert rig[x] == 0
        rig[y] = 1
        rig = check(code.right, rig, argc)
        assert rig.pop() == 0
        assert rig.pop() == 0
        return rig
    elif isinstance(code, Case):
        decrement(rig, argc, code.arg)
        x = len(rig)
        rig1 = list(rig) + [1]
        rig1 = check(code.left, rig1, argc)
        for i in range(x, len(rig1)):
            assert rig1[i] == 0
        rig2 = list(rig) + [1]
        rig2 = check(code.right, rig2, argc)
        for i in range(x, len(rig2)):
            assert rig2[i] == 0
        assert rig1[0:x] == rig2[0:x], "case conflict"
        return rig1[0:x]
    elif isinstance(code, Ofc):
        decrement(rig, argc, code.arg)
        rig1 = check(code.body, [1], argc)
        assert rig1 == [0]
        return rig
    elif isinstance(code, Cut):
        x = len(rig)
        y = len(rig)+1
        rig.extend([0,0])
        rig[x] = 1
        rig = check(code.left, rig, argc)
        assert rig[x] == 0
        rig[y] = 1
        rig = check(code.right, rig, argc)
        assert rig.pop() == 0
        assert rig.pop() == 0
        return rig
    elif isinstance(code, Ax):
        decrement(rig, argc, code.a)
        decrement(rig, argc, code.b)
        return rig
    elif isinstance(code, Call):
        decrement(rig, argc, code.arg)
        return rig
    elif isinstance(code, Impossible):
        decrement(rig, argc, code.arg)
        for arg in code.args:
            decrement(rig, argc, arg)
        return rig
    else:
        assert False, code

def decrement(rig, argc, arg):
    if 0 <= arg < len(rig):
        if rig[arg] == 1:
            rig[arg] = 0
        else:
            assert False, "refers to variable already used in rig: %d" % arg
    elif 0 <= ~arg < argc:
        return
    else:
        assert False, "arg outside rig"


class Arg(object):
    pass

class Declaration(Arg):
    def __init__(self, module, name, body, type, constraints):
        self.module = module
        self.name = name
        self.body = body
        self.type = type
        self.constraints = constraints

class Cons(Arg):
    def __init__(self, a, b):
        self.a = a
        self.b = b
        assert isinstance(a, Port)
        assert isinstance(b, Port)

class Choice(Arg):
    def __init__(self, index, a):
        self.index = index
        self.a = a
        assert isinstance(index, bool)
        assert isinstance(a, Port)

class Copier(Arg):
    def __init__(self, code, args):
        self.code = code
        self.args = args

class UnitValue(Arg):
    pass
unit = UnitValue()

def port():
    a = Port()
    b = Port()
    a.side, b.side = b, a
    return (a, b)

class Port(object):
    def __init__(self):
        self.side = None
        self.value = None
        self.waiting = None

    def send(self, value):
        self.side.value = value
        if self.side.waiting:
            ec = core.get_ec()
            ec.running.append(self.side.waiting)
            self.side.waiting = None

    def recv(self):
        if self.value is None:
            ec = core.get_ec()
            assert self.waiting is None
            this = ec.scheduler # This is soon our continuation.
            self.waiting = this
            ec.scheduler.switch()
        assert self.value is not None
        return self.value

# The evaluator
# rvmprof stuff, to see if it wakes up continuations.
def get_declaration_name(decl):
    return "py:%s" % decl.name

rvmprof.register_code_object_class(Declaration, get_declaration_name)

def get_code(code, reg, arg, declaration):
    return declaration

@rvmprof.vmprof_execute_code("pypy", get_code, Arg)
def eval(code, reg, args, decl):
    while isinstance(code, Code):
        #import os
        #os.write(2, "eval: " + code.to_str() + "\n")
        if isinstance(code, Id):
            code = code.body
        elif isinstance(code, Falsum):
            eval_lookup(reg, args, decl, code.arg).send(unit)
            code = code.body
        elif isinstance(code, Par):
            a, b = port()
            c, d = port()
            eval_lookup(reg, args, decl, code.arg).send(Cons(b, d))
            reg.append(a)
            reg.append(c)
            code = code.body
        elif isinstance(code, Select):
            a, b = port()
            eval_lookup(reg, args, decl, code.arg).send(Choice(code.which, b))
            reg.append(a)
            code = code.body
        elif isinstance(code, Qu):
            a = eval_lookup(reg, args, decl, code.arg).recv()
            assert isinstance(a, Copier)
            args.insert(0, a)
            code = code.body
        elif isinstance(code, Unit):
            a = eval_lookup(reg, args, decl, code.arg)
            a.recv()
            code = None
        elif isinstance(code, Tensor):
            cons = eval_lookup(reg, args, decl, code.arg).recv()
            assert isinstance(cons, Cons)
            reg.append(cons.a)
            reg.append(cons.b)
            spawn(code.left, reg, args, decl)
            spawn(code.right, reg, args, decl)
            code = None
        elif isinstance(code, Case):
            choice = eval_lookup(reg, args, decl, code.arg).recv()
            assert isinstance(choice, Choice)
            reg.append(choice.a)
            if choice.index:
                code = code.right
            else:
                code = code.left
        elif isinstance(code, Ofc):
            a = eval_lookup(reg, args, decl, code.arg)
            a.send(Copier(code, args))
            code = None
        elif isinstance(code, Cut):
            a, b = port()
            reg.append(a)
            reg.append(b)
            spawn(code.left, reg, args, decl)
            spawn(code.right, reg, args, decl)
            code = None
        elif isinstance(code, Ax):
            a = eval_lookup(reg, args, decl, code.a)
            b = eval_lookup(reg, args, decl, code.b)
            if a.value is not None:
                b.send(a.value)
            elif b.value is not None:
                a.send(b.value)
            else:
                c = a.side
                d = b.side 
                c.side, d.side = d, c
                a.side, b.side = b, a
            code = None
        elif isinstance(code, Call):
            a = eval_lookup(reg, args, decl, code.arg)
            spawn(code.decl.body, [a], [], code.decl)
            code = None
        elif isinstance(code, Impossible):
            assert False, "impossible to reach"
        elif isinstance(code, Procedure):
            a = eval_lookup(reg, args, decl, 0)
            code.procedure(a)
            code = None
        else:
            assert False, "options exhausted"
    assert code is None, "not none"

def eval_lookup(reg, args, decl, arg):
    if arg >= 0:
        return reg[arg]
    else:
        copier = args[~arg]
        narg, marg = port()
        spawn(copier.code, [marg], copier.args, decl)
        return narg

def spawn(code, reg, args, decl):
    ec = core.get_ec()
    ec.spawn_pool.append((code, reg, args, decl))

@core.Continuation.wrapped_callback
def launch_new_continuation(cont):
    ec = core.get_ec()
    code, reg, args, decl = ec.spawn_pool.pop()
    eval(code, reg, args, decl)
    return cont

def scheduler_main_loop():
    ec = core.get_ec()
    while len(ec.running) + len(ec.spawn_pool) > 0:
        if len(ec.spawn_pool) > 0:
            ec.scheduler = cont = core.Continuation()
            cont.init(launch_new_continuation)
        if len(ec.running) > 0:
            ec.scheduler = cont = ec.running.pop(0)
            cont.switch()

parser.py

# -*- coding: utf-8 -*-
import ukanren
from ukanren import Term

def file_to_list(term, output):
    if term.name == "__":
        output = file_to_list(term.args[0], output)
        output.append(term.args[1])
        return output
    if term.name == "[]":
        return output
    assert False

def list_to_typedecls(filelist):
    output = {}
    for term in filelist:
        if term.name == "typedecl":
            output[term.args[0].name] = term.args[1]
    return output

def list_to_decls(filelist):
    output = []
    for term in filelist:
        if term.name == "decl":
            output.append((term.args[0].name, term.args[1], term.args[2]))
    return output

# lexemes id
# 
# top: file
# 
# file: file stmt
# file:
# 
# stmt: id ":" dot
# stmt: id uq code
# 
# dot: pop "." dot
#    | pop
# 
# pop: plus "&" pop   
#    | plus
# 
# plus: par "+" plus   
#     | par
# 
# par: tensor "⅋" par
#    | tensor
# 
# tensor: shout "⊗" tensor   
#       | shout
# 
# shout: "!" shout
#      | call
# 
# call: call "(" dot ")"
#     | "(" dot ")"
#     | id
# 
# code: uq "→" id code
#     | "(" "→" id ")"                            # unit
#     | id "(" id ")"                             # call
#     | id "=" id                                 # axiom
#     | "(" uq "," uq "→" id ")" code "⊗" code    # tensor
#     | "(" uq "⊓" uq "→" id ")" code "⊓" code    # case
#     | "(" "!" uq "→" id ")" code                # ofc
#     | "(" uq "=" uq ")" code "⊗" code           # cut
#     | "impossible" id "(" ids ")"               # impossible
# 
# ids:
# ids: ids id
# 
# uq: uq1 ";" uq
#   | uq1
# 
# uq1: uq2
#    | "↑" uq1
#    | "↓" uq1
# 
# uq2: id
#    | "?" id
#    | "(" uq ")"

state = [ { u'': (1, 3), u'file': (0, 2), u'id': (1, 3), u'top': (0, 1)},
  { u'': (1, 0)},
  { u'': (1, 1), u'id': (0, 4), u'stmt': (0, 3)},
  { u'': (1, 2), u'id': (1, 2)},
  { u'"("': (0, 7),
    u'":"': (0, 9),
    u'"?"': (0, 6),
    u'"\u2191"': (0, 5),
    u'"\u2193"': (0, 13),
    u'id': (0, 12),
    u'uq': (0, 8),
    u'uq1': (0, 10),
    u'uq2': (0, 11)},
  { u'"("': (0, 7),
    u'"?"': (0, 6),
    u'"\u2191"': (0, 5),
    u'"\u2193"': (0, 13),
    u'id': (0, 12),
    u'uq1': (0, 14),
    u'uq2': (0, 11)},
  { u'id': (0, 15)},
  { u'"("': (0, 7),
    u'"?"': (0, 6),
    u'"\u2191"': (0, 5),
    u'"\u2193"': (0, 13),
    u'id': (0, 12),
    u'uq': (0, 16),
    u'uq1': (0, 10),
    u'uq2': (0, 11)},
  { u'"("': (0, 19),
    u'"?"': (0, 6),
    u'"impossible"': (0, 17),
    u'"\u2191"': (0, 5),
    u'"\u2193"': (0, 13),
    u'code': (0, 18),
    u'id': (0, 21),
    u'uq': (0, 20),
    u'uq1': (0, 10),
    u'uq2': (0, 11)},
  { u'"!"': (0, 24),
    u'"("': (0, 25),
    u'call': (0, 29),
    u'dot': (0, 31),
    u'id': (0, 30),
    u'par': (0, 22),
    u'plus': (0, 28),
    u'pop': (0, 26),
    u'shout': (0, 27),
    u'tensor': (0, 23)},
  { u'"("': (1, 33),
    u'")"': (1, 33),
    u'","': (1, 33),
    u'";"': (0, 32),
    u'"="': (1, 33),
    u'"?"': (1, 33),
    u'"impossible"': (1, 33),
    u'"\u2191"': (1, 33),
    u'"\u2192"': (1, 33),
    u'"\u2193"': (1, 33),
    u'"\u2293"': (1, 33),
    u'id': (1, 33)},
  { u'"("': (1, 34),
    u'")"': (1, 34),
    u'","': (1, 34),
    u'";"': (1, 34),
    u'"="': (1, 34),
    u'"?"': (1, 34),
    u'"impossible"': (1, 34),
    u'"\u2191"': (1, 34),
    u'"\u2192"': (1, 34),
    u'"\u2193"': (1, 34),
    u'"\u2293"': (1, 34),
    u'id': (1, 34)},
  { u'"("': (1, 37),
    u'")"': (1, 37),
    u'","': (1, 37),
    u'";"': (1, 37),
    u'"="': (1, 37),
    u'"?"': (1, 37),
    u'"impossible"': (1, 37),
    u'"\u2191"': (1, 37),
    u'"\u2192"': (1, 37),
    u'"\u2193"': (1, 37),
    u'"\u2293"': (1, 37),
    u'id': (1, 37)},
  { u'"("': (0, 7),
    u'"?"': (0, 6),
    u'"\u2191"': (0, 5),
    u'"\u2193"': (0, 13),
    u'id': (0, 12),
    u'uq1': (0, 33),
    u'uq2': (0, 11)},
  { u'"("': (1, 35),
    u'")"': (1, 35),
    u'","': (1, 35),
    u'";"': (1, 35),
    u'"="': (1, 35),
    u'"?"': (1, 35),
    u'"impossible"': (1, 35),
    u'"\u2191"': (1, 35),
    u'"\u2192"': (1, 35),
    u'"\u2193"': (1, 35),
    u'"\u2293"': (1, 35),
    u'id': (1, 35)},
  { u'"("': (1, 38),
    u'")"': (1, 38),
    u'","': (1, 38),
    u'";"': (1, 38),
    u'"="': (1, 38),
    u'"?"': (1, 38),
    u'"impossible"': (1, 38),
    u'"\u2191"': (1, 38),
    u'"\u2192"': (1, 38),
    u'"\u2193"': (1, 38),
    u'"\u2293"': (1, 38),
    u'id': (1, 38)},
  { u'")"': (0, 34)},
  { u'id': (0, 35)},
  { u'': (1, 5), u'id': (1, 5)},
  { u'"!"': (0, 38),
    u'"("': (0, 7),
    u'"?"': (0, 6),
    u'"\u2191"': (0, 5),
    u'"\u2192"': (0, 37),
    u'"\u2193"': (0, 13),
    u'id': (0, 12),
    u'uq': (0, 36),
    u'uq1': (0, 10),
    u'uq2': (0, 11)},
  { u'"\u2192"': (0, 39)},
  { u'"("': (0, 41), u'";"': (1, 37), u'"="': (0, 40)},
  { u'': (1, 11),
    u'"&"': (1, 11),
    u'")"': (1, 11),
    u'"+"': (0, 42),
    u'"."': (1, 11),
    u'id': (1, 11)},
  { u'': (1, 13),
    u'"&"': (1, 13),
    u'")"': (1, 13),
    u'"+"': (1, 13),
    u'"."': (1, 13),
    u'"\u214b"': (0, 43),
    u'id': (1, 13)},
  { u'"!"': (0, 24),
    u'"("': (0, 25),
    u'call': (0, 29),
    u'id': (0, 30),
    u'shout': (0, 44)},
  { u'"!"': (0, 24),
    u'"("': (0, 25),
    u'call': (0, 29),
    u'dot': (0, 45),
    u'id': (0, 30),
    u'par': (0, 22),
    u'plus': (0, 28),
    u'pop': (0, 26),
    u'shout': (0, 27),
    u'tensor': (0, 23)},
  { u'': (1, 7), u'")"': (1, 7), u'"."': (0, 46), u'id': (1, 7)},
  { u'': (1, 15),
    u'"&"': (1, 15),
    u'")"': (1, 15),
    u'"+"': (1, 15),
    u'"."': (1, 15),
    u'"\u214b"': (1, 15),
    u'"\u2297"': (0, 47),
    u'id': (1, 15)},
  { u'': (1, 9),
    u'"&"': (0, 48),
    u'")"': (1, 9),
    u'"."': (1, 9),
    u'id': (1, 9)},
  { u'': (1, 17),
    u'"&"': (1, 17),
    u'"("': (0, 49),
    u'")"': (1, 17),
    u'"+"': (1, 17),
    u'"."': (1, 17),
    u'"\u214b"': (1, 17),
    u'"\u2297"': (1, 17),
    u'id': (1, 17)},
  { u'': (1, 20),
    u'"&"': (1, 20),
    u'"("': (1, 20),
    u'")"': (1, 20),
    u'"+"': (1, 20),
    u'"."': (1, 20),
    u'"\u214b"': (1, 20),
    u'"\u2297"': (1, 20),
    u'id': (1, 20)},
  { u'': (1, 4), u'id': (1, 4)},
  { u'"("': (0, 7),
    u'"?"': (0, 6),
    u'"\u2191"': (0, 5),
    u'"\u2193"': (0, 13),
    u'id': (0, 12),
    u'uq': (0, 50),
    u'uq1': (0, 10),
    u'uq2': (0, 11)},
  { u'"("': (1, 36),
    u'")"': (1, 36),
    u'","': (1, 36),
    u'";"': (1, 36),
    u'"="': (1, 36),
    u'"?"': (1, 36),
    u'"impossible"': (1, 36),
    u'"\u2191"': (1, 36),
    u'"\u2192"': (1, 36),
    u'"\u2193"': (1, 36),
    u'"\u2293"': (1, 36),
    u'id': (1, 36)},
  { u'"("': (1, 39),
    u'")"': (1, 39),
    u'","': (1, 39),
    u'";"': (1, 39),
    u'"="': (1, 39),
    u'"?"': (1, 39),
    u'"impossible"': (1, 39),
    u'"\u2191"': (1, 39),
    u'"\u2192"': (1, 39),
    u'"\u2193"': (1, 39),
    u'"\u2293"': (1, 39),
    u'id': (1, 39)},
  { u'"("': (0, 51)},
  { u'")"': (0, 34), u'","': (0, 54), u'"="': (0, 52), u'"\u2293"': (0, 53)},
  { u'id': (0, 55)},
  { u'"("': (0, 7),
    u'"?"': (0, 6),
    u'"\u2191"': (0, 5),
    u'"\u2193"': (0, 13),
    u'id': (0, 12),
    u'uq': (0, 56),
    u'uq1': (0, 10),
    u'uq2': (0, 11)},
  { u'id': (0, 57)},
  { u'id': (0, 58)},
  { u'id': (0, 59)},
  { u'"!"': (0, 24),
    u'"("': (0, 25),
    u'call': (0, 29),
    u'id': (0, 30),
    u'par': (0, 22),
    u'plus': (0, 60),
    u'shout': (0, 27),
    u'tensor': (0, 23)},
  { u'"!"': (0, 24),
    u'"("': (0, 25),
    u'call': (0, 29),
    u'id': (0, 30),
    u'par': (0, 61),
    u'shout': (0, 27),
    u'tensor': (0, 23)},
  { u'': (1, 16),
    u'"&"': (1, 16),
    u'")"': (1, 16),
    u'"+"': (1, 16),
    u'"."': (1, 16),
    u'"\u214b"': (1, 16),
    u'"\u2297"': (1, 16),
    u'id': (1, 16)},
  { u'")"': (0, 62)},
  { u'"!"': (0, 24),
    u'"("': (0, 25),
    u'call': (0, 29),
    u'dot': (0, 63),
    u'id': (0, 30),
    u'par': (0, 22),
    u'plus': (0, 28),
    u'pop': (0, 26),
    u'shout': (0, 27),
    u'tensor': (0, 23)},
  { u'"!"': (0, 24),
    u'"("': (0, 25),
    u'call': (0, 29),
    u'id': (0, 30),
    u'shout': (0, 27),
    u'tensor': (0, 64)},
  { u'"!"': (0, 24),
    u'"("': (0, 25),
    u'call': (0, 29),
    u'id': (0, 30),
    u'par': (0, 22),
    u'plus': (0, 28),
    u'pop': (0, 65),
    u'shout': (0, 27),
    u'tensor': (0, 23)},
  { u'"!"': (0, 24),
    u'"("': (0, 25),
    u'call': (0, 29),
    u'dot': (0, 66),
    u'id': (0, 30),
    u'par': (0, 22),
    u'plus': (0, 28),
    u'pop': (0, 26),
    u'shout': (0, 27),
    u'tensor': (0, 23)},
  { u'"("': (1, 32),
    u'")"': (1, 32),
    u'","': (1, 32),
    u'"="': (1, 32),
    u'"?"': (1, 32),
    u'"impossible"': (1, 32),
    u'"\u2191"': (1, 32),
    u'"\u2192"': (1, 32),
    u'"\u2193"': (1, 32),
    u'"\u2293"': (1, 32),
    u'id': (1, 32)},
  { u'")"': (1, 30), u'id': (1, 30), u'ids': (0, 67)},
  { u'"("': (0, 7),
    u'"?"': (0, 6),
    u'"\u2191"': (0, 5),
    u'"\u2193"': (0, 13),
    u'id': (0, 12),
    u'uq': (0, 68),
    u'uq1': (0, 10),
    u'uq2': (0, 11)},
  { u'"("': (0, 7),
    u'"?"': (0, 6),
    u'"\u2191"': (0, 5),
    u'"\u2193"': (0, 13),
    u'id': (0, 12),
    u'uq': (0, 69),
    u'uq1': (0, 10),
    u'uq2': (0, 11)},
  { u'"("': (0, 7),
    u'"?"': (0, 6),
    u'"\u2191"': (0, 5),
    u'"\u2193"': (0, 13),
    u'id': (0, 12),
    u'uq': (0, 70),
    u'uq1': (0, 10),
    u'uq2': (0, 11)},
  { u'")"': (0, 71)},
  { u'"\u2192"': (0, 72)},
  { u'"("': (0, 19),
    u'"?"': (0, 6),
    u'"impossible"': (0, 17),
    u'"\u2191"': (0, 5),
    u'"\u2193"': (0, 13),
    u'code': (0, 73),
    u'id': (0, 21),
    u'uq': (0, 20),
    u'uq1': (0, 10),
    u'uq2': (0, 11)},
  { u'': (1, 24), u'"\u2293"': (1, 24), u'"\u2297"': (1, 24), u'id': (1, 24)},
  { u'")"': (0, 74)},
  { u'': (1, 10),
    u'"&"': (1, 10),
    u'")"': (1, 10),
    u'"."': (1, 10),
    u'id': (1, 10)},
  { u'': (1, 12),
    u'"&"': (1, 12),
    u'")"': (1, 12),
    u'"+"': (1, 12),
    u'"."': (1, 12),
    u'id': (1, 12)},
  { u'': (1, 19),
    u'"&"': (1, 19),
    u'"("': (1, 19),
    u'")"': (1, 19),
    u'"+"': (1, 19),
    u'"."': (1, 19),
    u'"\u214b"': (1, 19),
    u'"\u2297"': (1, 19),
    u'id': (1, 19)},
  { u'': (1, 6), u'")"': (1, 6), u'id': (1, 6)},
  { u'': (1, 14),
    u'"&"': (1, 14),
    u'")"': (1, 14),
    u'"+"': (1, 14),
    u'"."': (1, 14),
    u'"\u214b"': (1, 14),
    u'id': (1, 14)},
  { u'': (1, 8), u'")"': (1, 8), u'"."': (1, 8), u'id': (1, 8)},
  { u'")"': (0, 75)},
  { u'")"': (0, 76), u'id': (0, 77)},
  { u'")"': (0, 78)},
  { u'"\u2192"': (0, 79)},
  { u'"\u2192"': (0, 80)},
  { u'': (1, 22), u'"\u2293"': (1, 22), u'"\u2297"': (1, 22), u'id': (1, 22)},
  { u'id': (0, 81)},
  { u'': (1, 21), u'"\u2293"': (1, 21), u'"\u2297"': (1, 21), u'id': (1, 21)},
  { u'': (1, 23), u'"\u2293"': (1, 23), u'"\u2297"': (1, 23), u'id': (1, 23)},
  { u'': (1, 18),
    u'"&"': (1, 18),
    u'"("': (1, 18),
    u'")"': (1, 18),
    u'"+"': (1, 18),
    u'"."': (1, 18),
    u'"\u214b"': (1, 18),
    u'"\u2297"': (1, 18),
    u'id': (1, 18)},
  { u'': (1, 29), u'"\u2293"': (1, 29), u'"\u2297"': (1, 29), u'id': (1, 29)},
  { u'")"': (1, 31), u'id': (1, 31)},
  { u'"("': (0, 19),
    u'"?"': (0, 6),
    u'"impossible"': (0, 17),
    u'"\u2191"': (0, 5),
    u'"\u2193"': (0, 13),
    u'code': (0, 82),
    u'id': (0, 21),
    u'uq': (0, 20),
    u'uq1': (0, 10),
    u'uq2': (0, 11)},
  { u'id': (0, 83)},
  { u'id': (0, 84)},
  { u'")"': (0, 85)},
  { u'"\u2297"': (0, 86)},
  { u'")"': (0, 87)},
  { u'")"': (0, 88)},
  { u'"("': (0, 19),
    u'"?"': (0, 6),
    u'"impossible"': (0, 17),
    u'"\u2191"': (0, 5),
    u'"\u2193"': (0, 13),
    u'code': (0, 89),
    u'id': (0, 21),
    u'uq': (0, 20),
    u'uq1': (0, 10),
    u'uq2': (0, 11)},
  { u'"("': (0, 19),
    u'"?"': (0, 6),
    u'"impossible"': (0, 17),
    u'"\u2191"': (0, 5),
    u'"\u2193"': (0, 13),
    u'code': (0, 90),
    u'id': (0, 21),
    u'uq': (0, 20),
    u'uq1': (0, 10),
    u'uq2': (0, 11)},
  { u'"("': (0, 19),
    u'"?"': (0, 6),
    u'"impossible"': (0, 17),
    u'"\u2191"': (0, 5),
    u'"\u2193"': (0, 13),
    u'code': (0, 91),
    u'id': (0, 21),
    u'uq': (0, 20),
    u'uq1': (0, 10),
    u'uq2': (0, 11)},
  { u'"("': (0, 19),
    u'"?"': (0, 6),
    u'"impossible"': (0, 17),
    u'"\u2191"': (0, 5),
    u'"\u2193"': (0, 13),
    u'code': (0, 92),
    u'id': (0, 21),
    u'uq': (0, 20),
    u'uq1': (0, 10),
    u'uq2': (0, 11)},
  { u'': (1, 27), u'"\u2293"': (1, 27), u'"\u2297"': (1, 27), u'id': (1, 27)},
  { u'': (1, 28), u'"\u2293"': (1, 28), u'"\u2297"': (1, 28), u'id': (1, 28)},
  { u'"\u2293"': (0, 93)},
  { u'"\u2297"': (0, 94)},
  { u'"("': (0, 19),
    u'"?"': (0, 6),
    u'"impossible"': (0, 17),
    u'"\u2191"': (0, 5),
    u'"\u2193"': (0, 13),
    u'code': (0, 95),
    u'id': (0, 21),
    u'uq': (0, 20),
    u'uq1': (0, 10),
    u'uq2': (0, 11)},
  { u'"("': (0, 19),
    u'"?"': (0, 6),
    u'"impossible"': (0, 17),
    u'"\u2191"': (0, 5),
    u'"\u2193"': (0, 13),
    u'code': (0, 96),
    u'id': (0, 21),
    u'uq': (0, 20),
    u'uq1': (0, 10),
    u'uq2': (0, 11)},
  { u'': (1, 26), u'"\u2293"': (1, 26), u'"\u2297"': (1, 26), u'id': (1, 26)},
  { u'': (1, 25), u'"\u2293"': (1, 25), u'"\u2297"': (1, 25), u'id': (1, 25)}]
rstate = [ (u'', 1),
  (u'top', 1),
  (u'file', 2),
  (u'file', 0),
  (u'stmt', 3),
  (u'stmt', 3),
  (u'dot', 3),
  (u'dot', 1),
  (u'pop', 3),
  (u'pop', 1),
  (u'plus', 3),
  (u'plus', 1),
  (u'par', 3),
  (u'par', 1),
  (u'tensor', 3),
  (u'tensor', 1),
  (u'shout', 2),
  (u'shout', 1),
  (u'call', 4),
  (u'call', 3),
  (u'call', 1),
  (u'code', 4),
  (u'code', 4),
  (u'code', 4),
  (u'code', 3),
  (u'code', 10),
  (u'code', 10),
  (u'code', 7),
  (u'code', 8),
  (u'code', 5),
  (u'ids', 0),
  (u'ids', 2),
  (u'uq', 3),
  (u'uq', 1),
  (u'uq1', 1),
  (u'uq1', 2),
  (u'uq1', 2),
  (u'uq2', 1),
  (u'uq2', 2),
  (u'uq2', 3)]

keywords = [ u'!',
  u'\u2193',
  u'&',
  u')',
  u'(',
  u'+',
  u',',
  u'.',
  u'\u2191',
  u'\u2293',
  u'\u2192',
  u'\u2297',
  u'impossible',
  u';',
  u':',
  u'=',
  u'\u214b',
  u'?']

def get_action(top, sym):
    return state[top][sym]

class Tokenizer(object):
    def __init__(self, parser):
        self.state = 0
        self.text = u""
        self.parser = parser

class Parser(object):
    def __init__(self):
        self.stack = []
        self.top = 0
        self.output = None

    def step(self, name, value):
        assert isinstance(name, unicode)
        self.output = None
        if name == u'"⊥"':
            return self.step(u"id", value)
        #import os
        #os.write(2, "debug: " + name.encode('utf-8') + ": " + value.encode('utf-8') + "\n")
        arg = get_action(self.top, name)
        while arg[0] == 1:
            lhs, count = rstate[arg[1]]
            objects = []
            for _ in range(count):
                self.top, obj = self.stack.pop()
                objects.append(obj)
            objects.reverse()
            robject = reduction(arg[1], objects)
            if lhs == u"":
                self.stack = []
                self.top = 0
                self.output = robject
                return
            else:
                arg = state[self.top][lhs]
                assert arg[0] != 1
                self.stack.append((self.top, robject))
                self.top = arg[1]
                arg = get_action(self.top, name)
        self.stack.append((self.top, ukanren.Term(value.encode('utf-8'), [])))
        self.top = arg[1]

def reduction(rule, args):
    #import os
    #os.write(2, "debug-reduction: %d %s/%d\n" % (rule, rstate[rule][0].encode('utf-8'), rstate[rule][1]))
    if rule == 0: # top
        return args[0]
    if rule == 1: # top → file
        return args[0]
    if rule == 2: # file → file stmt
        return Term("__", args)
    if rule == 3: #      | ()
        return Term("[]", [])
    if rule == 4: # stmt → id : dot
        return Term("typedecl", [args[0], args[2]])
    if rule == 5: # stmt: id uq code
        return Term("decl", [args[0], args[1], args[2]])
    if rule == 6: # dot → pop . dot
        return Term(".", [args[0], args[2]])
    if rule == 7: #     | pop
        return args[0]
    if rule == 8: # pop → plus & pop   
        return Term("&", [args[0], args[2]])
    if rule == 9: #     | plus
        return args[0]
    if rule == 10: # plus: par "+" plus   
        return Term("+", [args[0], args[2]])
    if rule == 11: #     | par
        return args[0]
    if rule == 12: # par: tensor "⅋" par
        return Term("⅋", [args[0], args[2]])
    if rule == 13: #    | tensor
        return args[0]
    if rule == 14: # tensor → shout ⊗ tensor   
        return Term("⊗", [args[0], args[2]])
    if rule == 15: #        | shout
        return args[0]
    if rule == 16: # shout → ! shout
        return Term("!", [args[1]])
    if rule == 17: #      | call
        term = args[0]
        if len(term.args) == 0 and term.name.startswith("$"):
            digits = term.name[1:len(term.name)]
            if digits.isdigit():
                return ukanren.Const(int(digits))
        return term
    if rule == 18: # call → call ( dot )
        args[0].args.append(args[2])
        return args[0]
    if rule == 19: #      | ( dot )
        return args[1]
    if rule == 20: #      | id
        return args[0]
    if rule == 21: # code: uq "→" id code
        return Term("U", [args[0], args[2], args[3]])
    if rule == 22: #     | "(" "→" id ")"
        return Term("unit", [args[2]])
    if rule == 23: #     | id "(" id ")"
        return Term("call", [args[0], args[2]])
    if rule == 24: #     | id "=" id
        return Term("ax", [args[0], args[2]])
    if rule == 25: #     | "(" uq "," uq "→" id ")" code "⊗" code
        return Term("tensor", [args[1], args[3], args[5], args[7], args[9]])
    if rule == 26: #     | "(" uq "⊓" uq "→" id ")" code "⊓" code
        return Term("case", [args[1], args[3], args[5], args[7], args[9]])
    if rule == 27: #     | "(" "!" uq "→" id ")" code
        return Term("ofc", [args[2], args[4], args[6]])
    if rule == 28: #     | "(" uq "=" uq ")" code "⊗" code
        return Term("cut", [args[1], args[3], args[5], args[7]])
    if rule == 29: #     | "impossible" id "(" ids ")"
        return Term("impossible", [args[1], args[3]])
    if rule == 30: # ids:
        return Term("[]", [])
    if rule == 31: # ids: ids id
        return Term("::", [args[0], args[1]])
    if rule == 32: # uq: uq1 ";" uq
        return Term(";", [args[0], args[2]])
    if rule == 33: #   | uq1
        return args[0]
    if rule == 34: # uq1: uq2
        return args[0]
    if rule == 35: #    | "↑" uq1
        return Term("↑", [args[1]])
    if rule == 36: #    | "↓" uq1
        return Term("↓", [args[1]])
    if rule == 37: # uq2: id
        return args[0]
    if rule == 38: #    | "?" id
        return Term("?", [args[1]])
    if rule == 39: #    | "(" uq ")"
        return args[1]
    assert False

def step_text(t):
    if t.text in keywords:
        t.parser.step(u'"' + t.text + u'"', t.text)
    else:
        t.parser.step(u"id", t.text)
    t.text = u""
    t.state = 0

def read_char(t, char):
    assert isinstance(char, unicode)
    #import os
    #os.write(2, "debug-char: " + char.encode('utf-8') + "\n")
    if t.state == 0:
        if char in [u" ", u"\t", u"\n"]:
            t.state = 0
        elif char == u'#':
            t.state = 20
        elif char == u"⊗" or char == u"⊸":
            t.parser.step(u'"' + char + u'"', char)
        elif char in keywords:
            t.parser.step(u'"' + char + u'"', char)
        else:
            t.text += char
            t.state = 1
    elif t.state == 1: # retrieving characters.
        if char in [u" ", u"\t", u"\n"]:
            step_text(t)
        elif char == u'#':
            step_text(t)
            t.state = 20
        elif char == u"⊗" or char == u"⊸":
            step_text(t)
            t.parser.step(u'"' + char + u'"', char)
        elif char in keywords:
            step_text(t)
            t.parser.step(u'"' + char + u'"', char)
        else:
            t.text += char
            t.state = 1
    elif t.state == 20:
        if char == u"\n":
            t.state = 0
        else:
            t.state = 20
    else:
        raise ReadError(char)

def read_done(t):
    if t.state == 1:
        t.parser.step(u"id", t.text)
        t.state = 0
    t.parser.step(u"", u"")
    return t.parser.output

class ReadError(Exception):
    def __init__(self, char):
        self.char = char

    def rep(self):
        return "When trying to read char 0x%x" % (ord(self.char))

def to_digit(char):
    return ord(char) - ord('0')

ukanren.py

# -*- encoding: utf-8 -*-
class TermOrVar(object):
    def to_str(self, rbp=0):
        assert False

class Term(TermOrVar):
    def __init__(self, name, args):
        self.name = name
        self.args = args
        for arg in args:
            assert isinstance(arg, TermOrVar)

    def to_str(self, rbp=0):
        sig = self.get_signature()
        if rbp > get_rbp(sig):
            return "(" + self.to_str() + ")"
        elif len(self.args) == 0:
            return self.name
        elif sig == "./2":
            a = self.args[0].to_str(11)
            b = self.args[1].to_str(10)
            return a + " " + self.name + " " + b
        elif sig == "⊸/2":
            a = self.args[0].to_str(21)
            b = self.args[1].to_str(20)
            return a + " " + self.name + " " + b
        elif sig == "+/2":
            a = self.args[0].to_str(31)
            b = self.args[1].to_str(30)
            return a + " " + self.name + " " + b
        elif sig == "⅋/2":
            a = self.args[0].to_str(36)
            b = self.args[1].to_str(35)
            return a + " " + self.name + " " + b
        elif sig == "⊗/2":
            a = self.args[0].to_str(41)
            b = self.args[1].to_str(40)
            return a + " " + self.name + " " + b
        elif sig == "!/1":
            a = self.args[0].to_str(51)
            return self.name + a
        else:
            args = ""
            sp = " "
            for arg in self.args:
                args += sp + "(" + arg.to_str() + ")"
                sp = " "
            return self.name + args

    def get_signature(self):
        return self.name + "/" + str(len(self.args))

def get_rbp(sig):
    if sig == "./2":
        return 10
    if sig == "⊸/2":
        return 20
    if sig == "+/2":
        return 30
    if sig == "⅋/2":
        return 35
    if sig == "⊗/2":
        return 40
    if sig == "!/1":
        return 50
    return 60

class Var(TermOrVar):
    def __init__(self, key):
        self.key = key

    def to_str(self, rbp=0):
        return "#" + str(self.key)

class Const(TermOrVar):
    def __init__(self, key):
        self.key = key

    def to_str(self, rbp=0):
        return "$" + str(self.key)

# Pattern hole for constraint handling rule patterns.
class Hole(TermOrVar):
    def __init__(self, key):
        self.key = key

    def to_str(self, rbp=0):
        return "$HOLE{" + str(self.key) + "}"

class Storage:
    def __init__(self, rules, subst, nextvar, constraints, nextcid, notes, killed, hist):
        self.rules = rules
        self.subst = subst
        self.nextvar = nextvar
        self.constraints = constraints
        self.nextcid = nextcid
        self.notes = notes
        self.killed = killed
        self.hist = hist

default_rules = [] # Filled later.

def empty(rules=default_rules):
    return Storage(
        rules = rules,
        subst = {},
        nextvar = 0,
        constraints = {},
        nextcid = 0,
        notes = {},
        killed = {},
        hist = {})

def copy_constraints(constraints):
    nconstraints = {}
    for sig, table in constraints.items():
        nconstraints[sig] = table.copy()
    return nconstraints

def copy_notes(notes):
    nnotes = {}
    for key, table in notes.items():
        nnotes[key] = table.copy()
    return nnotes

class Constraint(object):
    def __init__(self, term, id):
        self.term = term
        self.id = id

    def to_str(self):
        return self.term.to_str() + "#" + str(self.id)

class frozenlist(object):
    def __init__(self, list):
        self.list = list

    def __hash__(self):
        return hash(self.list)

    def __iter__(self):
        return iter(self.list)

def make_constraint(term, state):
    assert isinstance(term, Term)
    c = Constraint(walk(term, state.subst), state.nextcid)
    state = Storage(state.rules,
                    state.subst,
                    state.nextvar,
                    state.constraints,
                    state.nextcid+1,
                    state.notes,
                    state.killed,
                    state.hist)
    return reactivate(c, state)

def get_constraints(state):
    out = []
    for table in state.constraints.itervalues():
        for c in table.itervalues():
            out.append(c.term)
    return out

def alive(c, state):
    if c.id in state.killed:
        return False
    return True
    # We won't access constraints outside our scope.
    #table = state.constraints.get(c.term.get_signature(), None)
    #if table is not None:
    #    if c.id in table:
    #        return True
    #return False

def kill(c, state):
    state = Storage(state.rules,
                    state.subst,
                    state.nextvar,
                    state.constraints,
                    state.nextcid,
                    state.notes,
                    state.killed.copy(),
                    state.hist)
    state.killed[c.id] = c
    #import os
    #os.write(1, "kill %s\n" % c.to_str())
    return state

def suspend(c, state):
    killed = state.killed
    state = Storage(state.rules,
                    state.subst,
                    state.nextvar,
                    copy_constraints(state.constraints),
                    state.nextcid,
                    copy_notes(state.notes),
                    {},
                    state.hist)
    if c.id not in killed:
        add_notes(c.term, state, c)
        table = state.constraints.get(c.term.get_signature(), None)
        if table is None:
            state.constraints[c.term.get_signature()] = table = {}
        table[c.id] = c
    if len(killed) > 0: # Clean propagation history
        state.hist = state.hist.copy()
        for entry in state.hist.keys():
            remove = False
            for i in entry:
                remove |= (i in killed)
            if remove:
                state.hist.pop(entry, None)
    for k in killed.itervalues():
        table = state.constraints.get(k.term.get_signature(), None)
        if table is not None:
            table.pop(c.id, None)
    return state

def add_notes(term, state, c):
    if isinstance(term, Var):
        notes = state.notes
        wakeups = notes.get(term.key, None)
        if wakeups is None:
            notes[term.key] = wakeups = {}
        wakeups[c.id] = c
    elif isinstance(term, Term):
        for arg in term.args:
            add_notes(arg, state, c)

def var_to_const(term, table):
    if isinstance(term, Var) or isinstance(term, Const):
        new_const = table.get(term.to_str(), None)
        if new_const is None:
            new_const = table[term.to_str()] = Const(len(table))
        return new_const, table
    elif isinstance(term, Term):
        nargs = []
        for arg in term.args:
            narg, table = var_to_const(arg, table)
            nargs.append(narg)
        return Term(term.name, nargs), table
    else:
        assert False

def const_to_var(term, table, state):
    if isinstance(term, Var):     # The namespace entries may contain variables.
        return term, table, state
    elif isinstance(term, Const):
        new_var = table.get(term.key, None)
        if new_var is None:
            var, state = fresh(state)
            new_var = table[term.key] = var
        return new_var, table, state
    elif isinstance(term, Term):
        nargs = []
        for arg in term.args:
            narg, table, state = const_to_var(arg, table, state)
            nargs.append(narg)
        return Term(term.name, nargs), table, state
    else:
        assert False

def walk(term, subst):
    if isinstance(term, Var):
        val = subst.get(term.key, None)
        if val is None:
            return term
        else:
            return walk(val, subst)
    elif isinstance(term, Term):
        nargs = []
        for arg in term.args:
            nargs.append(walk(arg, subst))
        return Term(term.name, nargs)
    elif isinstance(term, Const):
        return term
    else:
        assert False, term.to_str()

def extS(key, term, state):
    if occurs(key, term, state.subst):
        return None
    else:
        nnotes = state.notes
        nsubst = state.subst.copy()
        nsubst[key] = term
        if key in state.notes:
            nnotes = copy_notes(state.notes)
            wakeups = nnotes.pop(key)
        else:
            wakeups = {}
        state = Storage(state.rules,
                        nsubst,
                        state.nextvar,
                        state.constraints,
                        state.nextcid,
                        nnotes,
                        state.killed,
                        state.hist)
        states = [state]
        if len(wakeups) > 0:
            state.constraints = copy_constraints(state.constraints)
            # When waking up constraints, ideally we want to replicate
            # the situation when they were added the first time.
            for c in wakeups.values():
                state.constraints[c.term.get_signature()].pop(c.id, None)
            for c in wakeups.values():
                nstates = []
                for state in states:
                    if not alive(c, state):
                        continue
                    sts = reactivate(Constraint(walk(c.term, state.subst), c.id), state)
                    nstates.extend(sts)
                states = nstates
        return states

def fresh(state):
    v = Var(state.nextvar)
    nstate = Storage(state.rules,
                     state.subst,
                     state.nextvar+1,
                     state.constraints,
                     state.nextcid,
                     state.notes,
                     state.killed,
                     state.hist)
    return (v, nstate)

class Combinator:
    def go(self, state):
        assert False

class eq(Combinator):
    def __init__(self, t1, t2):
        self.t1 = t1
        self.t2 = t2

    def go(self, state):
        #import os
        #t1s = walk(self.t1, state.subst).to_str()
        #t2s = walk(self.t2, state.subst).to_str()
        #os.write(2, "%s = %s\n" % (t1s, t2s))
        res = unify(self.t1, self.t2, state)
        if len(res) == 0:
            #import os
            #os.write(1, "fail\n")
            #for key, term in state.subst.items():
            #    os.write(1, "%d = %s\n" % (key, walk(term,state.subst).to_str()))
            return []
        return res

def unify(t1, t2, state):
    t1 = walk(t1, state.subst)
    t2 = walk(t2, state.subst)
    #import os
    #os.write(1, t1.to_str() + " == " + t2.to_str() + "\n")
    if isinstance(t1, Var) and isinstance(t2, Var) and t1.key == t2.key:
        return [state]
    elif isinstance(t1, Var):
        return extS(t1.key, t2, state)
    elif isinstance(t2, Var):
        return extS(t2.key, t1, state)
    elif isinstance(t1, Term) and isinstance(t2, Term):
        if t1.name == t2.name and len(t1.args) == len(t2.args):
            states = [state]
            for i in range(0, len(t1.args)):
                nstates = []
                for state in states:
                    states = unify(t1.args[i], t2.args[i], state)
                    nstates.extend(states)
                states = nstates
            return states
        else:
            return []
    elif isinstance(t1, Const) and isinstance(t2, Const):
        if t1.key == t2.key:
            return [state]
        else:
            return []
    else:
        assert False

def occurs(key, term, subst):
    term = walk(term, subst)
    if isinstance(term, Var):
        return term.key == key
    elif isinstance(term, Term):
        for arg in term.args:
            if occurs(key, arg, subst):
                return True
        return False
    elif isinstance(term, Const):
        return False
    else:
        assert False

class Unit(Combinator):
    def go(self, state):
        return [state]

class Fail(Combinator):
    def go(self, state):
        return []

tt = Unit()
ff = Fail()

class disj(Combinator):
    def __init__(self, g1, g2):
        assert isinstance(g1, Combinator)
        assert isinstance(g2, Combinator)
        self.g1 = g1
        self.g2 = g2

    def go(self, state):
        return self.g1.go(state) + self.g2.go(state)

class conj(Combinator):
    def __init__(self, g1, g2):
        assert isinstance(g1, Combinator)
        assert isinstance(g2, Combinator)
        self.g1 = g1
        self.g2 = g2

    def go(self, state):
        res = []
        for nstate in self.g1.go(state):
            res.extend(self.g2.go(nstate))
        return res

class constraint(Combinator):
    def __init__(self, term):
        assert isinstance(term, Term)
        self.term = term

    def go(self, state):
        return make_constraint(self.term, state)

def match(term, pattern, table):
    if isinstance(term, Var) and isinstance(pattern, Var):
        if term.key == pattern.key:
            return table
    elif isinstance(pattern, Hole):
        other = table.get(pattern.key, None)
        if other is None:
            table = table.copy()
            table[pattern.key] = term
            return table
        else:
            return match(term, other, table)
    elif isinstance(term, Term) and isinstance(pattern, Term):
        if term.name == pattern.name and len(term.args) == len(pattern.args):
            for i in range(0, len(term.args)):
                table = match(term.args[i], pattern.args[i], table)
                if table is None:
                    return None
            return table
    return None

def lookup(sig, state):
    table = state.constraints.get(sig, None)
    if table is None:
        return {}.itervalues()
    return table.itervalues()

def reactivate(c, state):
    #import os
    #os.write(1, "reactivate %s\n" % c.to_str())
    goals = tt
    live = True
    i = 0
    for rule in state.rules:
        #os.write(1, "rule %d\n" % i)
        holes = rule.filter(c.term.get_signature())
        slots = rule.select()
        for index in holes:
            #os.write(1, "occ %d,%d\n" % (i, index))
            for table, row, kills in cartesian(slots, index, c, state):
                live = True
                for r in row.values():
                    live = live and alive(r, state)
                if not live:
                    continue
                if not len(row) == len(slots): # duplicates on row.
                    continue
                if not rule.guard(table):
                    continue
                for k in kills:
                    state = kill(k, state)
                if len(kills) == 0:
                    entry = frozenlist(row.keys() + [~i])
                    if entry in state.hist:
                        continue
                    hist = state.hist.copy()
                    hist[entry] = None
                    state = Storage(state.rules,
                                    state.subst,
                                    state.nextvar,
                                    state.constraints,
                                    state.nextcid,
                                    state.notes,
                                    state.killed,
                                    hist)
                goals = conj(goals, Handler(rule.body, table))
                live = alive(c, state)
                if not live:
                    break
            if not live:
                break
        if not live:
            break
        i += 1
    state = suspend(c, state)
    return goals.go(state)

class Handler(Combinator):
    def __init__(self, body, binding):
        self.body = body
        self.binding = binding

    def go(self, state):
        return self.body(self.binding, state)

# Cartesian match across all slots.
def cartesian(slots, index, c, state):
    if len(slots) == 0:
        return [({}, {}, [])]
    out = []
    for table, row, kills in cartesian(slots[1:len(slots)], index-1, c, state):
        #print "table"
        #for key, item in table.iteritems():
        #    print "  " + str(key) + " = " + item.to_str()
        k, sig, pat = slots[0]
        if index == 0:
            tab = match(c.term, pat, table)
            if tab is None:
                continue
            r = row.copy()
            r[c.id] = c
            if k:
                out.append((tab, r, kills + [c]))
            else:
                out.append((tab, r, kills))
        else:
            for nc in lookup(sig, state):
                if not alive(nc, state):
                    continue
                tab = match(nc.term, pat, table)
                if tab is None:
                    continue
                r = row.copy()
                r[nc.id] = nc
                if k:
                    out.append((tab, r, kills + [c]))
                else:
                    out.append((tab, r, kills))
    return out

class Rule(object):
    def __init__(self, keep, remove, guard, body):
        self.keep = keep
        self.remove = remove
        self.guard = guard
        self.body = body

    def filter(self, sig):
        top = len(self.keep) + len(self.remove) - 1
        out = []
        while top >= 0:
            if len(self.keep) <= top:
                if sig == self.remove[top-len(self.keep)].get_signature():
                    out.append(top)
            elif top < len(self.keep):
                if sig == self.keep[top].get_signature():
                    out.append(top)
            top -= 1
        return out

    def select(self):
        out = []
        for term in self.keep:
            out.append((False, term.get_signature(), term))
        for term in self.remove:
            out.append((True, term.get_signature(), term))
        return out

def dual(x, y):
    return Term("dual", [x, y])

def always_true(bindings):
    return True

# The CHR rule handler returns 'nothing' when guard doesn't pass.
def chr_rule(keep, remove, guard=always_true):
    def __decorator__(fn):
        default_rules.append(Rule(keep, remove, guard, fn))
        return fn
    return __decorator__

X = Hole(0)
Y = Hole(1)
Z = Hole(2)

@chr_rule([], [dual(X, X)])
def rule_0(bindings, state):
    return ff.go(state)

@chr_rule([dual(X, Y)], [dual(Y, Z)])
def rule_1(bindings, state):
    X = bindings[0]
    Y = bindings[1]
    Z = bindings[2]
    return eq(X, Z).go(state)

@chr_rule([dual(X, Y)], [dual(Z, Y)])
def rule_2(bindings, state):
    X = bindings[0]
    Y = bindings[1]
    Z = bindings[2]
    return eq(X, Z).go(state)

@chr_rule([dual(X, Y)], [dual(X, Z)])
def rule_3(bindings, state):
    X = bindings[0]
    Y = bindings[1]
    Z = bindings[2]
    return eq(Y, Z).go(state)

@chr_rule([dual(X, Y)], [dual(Z, X)])
def rule_4(bindings, state):
    X = bindings[0]
    Y = bindings[1]
    Z = bindings[2]
    return eq(Y, Z).go(state)

def tensor(x, y):
    return Term("⊗", [x, y])

def par(x, y):
    return Term("⅋", [x, y])

def plus(x, y):
    return Term("+", [x, y])

def band(x, y):
    return Term("&", [x, y])

def ofc(x):
    return Term("!", [x])

def que(x):
    return Term("?", [x])

unit = Term("1", [])
zero = Term("0", [])
top = Term("⊤", [])
bot = Term("⊥", [])

X = Hole(0)
Y = Hole(1)
Z = Hole(2)

@chr_rule([], [dual(tensor(X,Y),Z)])
@chr_rule([], [dual(Z,tensor(X,Y))])
def rule_5(bindings, state):
    C, state = fresh(state)
    D, state = fresh(state)
    X,Y,Z = bindings[0],bindings[1],bindings[2]
    return conj(
        eq(Z, par(C,D)),
        conj(
            constraint(dual(X,C)),
            constraint(dual(Y,D)))).go(state)

@chr_rule([], [dual(Z, par(X,Y))])
@chr_rule([], [dual(par(X,Y), Z)])
def rule_6(bindings, state):
    C, state = fresh(state)
    D, state = fresh(state)
    X,Y,Z = bindings[0],bindings[1],bindings[2]
    return conj(
        eq(Z,tensor(C,D)),
        conj(
            constraint(dual(X,C)),
            constraint(dual(Y,D)))).go(state)

@chr_rule([], [dual(Z, plus(X,Y))])
@chr_rule([], [dual(plus(X,Y), Z)])
def rule_7(bindings, state):
    C, state = fresh(state)
    D, state = fresh(state)
    X,Y,Z = bindings[0],bindings[1],bindings[2]
    return conj(
        eq(Z,band(C,D)),
        conj(
            constraint(dual(X,C)),
            constraint(dual(Y,D)))).go(state)

@chr_rule([], [dual(Z, band(X,Y))])
@chr_rule([], [dual(band(X,Y), Z)])
def rule_8(bindings, state):
    C, state = fresh(state)
    D, state = fresh(state)
    X,Y,Z = bindings[0],bindings[1],bindings[2]
    return conj(
        eq(Z,plus(C,D)),
        conj(
            constraint(dual(X,C)),
            constraint(dual(Y,D)))).go(state)

@chr_rule([], [dual(Y, ofc(X))])
@chr_rule([], [dual(ofc(X), Y)])
def rule_9(bindings, state):
    C, state = fresh(state)
    X,Y = bindings[0],bindings[1]
    return conj(
        eq(Y,que(C)),
            constraint(dual(X,C))).go(state)

@chr_rule([], [dual(Y, que(X))])
@chr_rule([], [dual(que(X), Y)])
def rule_10(bindings, state):
    C, state = fresh(state)
    X,Y = bindings[0],bindings[1]
    return conj(
        eq(Y,ofc(C)),
            constraint(dual(X,C))).go(state)

@chr_rule([], [dual(X, unit)])
@chr_rule([], [dual(unit, X)])
def rule_11(bindings, state):
    X = bindings[0]
    return eq(X,bot).go(state)

@chr_rule([], [dual(X, bot)])
@chr_rule([], [dual(bot, X)])
def rule_12(bindings, state):
    X = bindings[0]
    return eq(X,unit).go(state)

@chr_rule([], [dual(X, zero)])
@chr_rule([], [dual(zero, X)])
def rule_13(bindings, state):
    X = bindings[0]
    return eq(X,top).go(state)

@chr_rule([], [dual(X, top)])
@chr_rule([], [dual(top, X)])
def rule_13(bindings, state):
    X = bindings[0]
    return eq(X,zero).go(state)

def demonstration():
    state = empty()
    x, state = fresh(state)
    y, state = fresh(state)
    z, state = fresh(state)
    w, state = fresh(state)
    h, state = fresh(state)
    goal = conj(constraint(Term("dual", [x, y])),
                constraint(Term("dual", [tensor(unit,par(x, y)), h])))

    import os
    os.write(1, "results for\n")
    for state in goal.go(state):
        os.write(1, "result:\n")
        for var in state.subst:
            os.write(1, "  %d = %s\n" % (var, walk(state.subst[var], state.subst).to_str()))
        for cs in state.constraints.itervalues():
            for c in cs.itervalues():
                if alive(c, state):
                    os.write(1, "  %s\n" % c.term.to_str())

if __name__=="__main__":
    demonstration()