#!/usr/bin/env python

# Sergio Antoy
# Wed 20 Nov 2019 02:54:15 PM PST

# Object code to head normalize expressions made up of
# lists of colors and the function append according to
# http://web.cecs.pdx.edu/~antoy/homepage/publications/termgraph14/final.pdf

class Symbol:
    def __init__(self, name): self._name = name
    def name(self): return self._name

class Constructor(Symbol):
    pass

class Operation(Symbol):
    def __init__(self, name, hnf):
        Symbol.__init__(self, name)
        self._hnf = hnf
    def hnf(self): return self._hnf

# representation of expressions:
# a node has a root (symbol) and arguments (list of nodes)
class Node:
    def __init__(self, root, arguments = []):
        self._root = root
        self._arguments = arguments
    def root(self): return self._root
    def argn(self,i): return self._arguments[i]
    def tostring(self):
        t = self._root.name()
        if self._arguments != []:
            t += '('
            for i, x in enumerate(self._arguments):
                if i > 0: t += ','
                t += x.tostring()
            t += ')'
        return t
    def hnf(self): return self._root.hnf()(self)

# ---------------- user program, compiled ----------------

# signature constructors

red = Constructor('red')
green = Constructor('green')
blue = Constructor('blue')
nil = Constructor('[]')
cons = Constructor(':')

# signature operations

def hnf_append(expr):
    a0r = expr.argn(0).root()
    if a0r == nil:
        a1 = expr.argn(1)
        a1r = a1.root()
        if a1r == nil:
            return a1
        elif a1r == cons:
            return a1
        else:
            return a1.hnf()
    elif a0r == cons:
        return Node(cons,[expr.argn(0).argn(0),Node(append,[expr.argn(0).argn(1),expr.argn(1)])])
    else:
        return Node(expr.root(),[expr.argn(0).hnf(), expr.argn(1)]).hnf()

append = Operation('++', hnf_append)