main :: IO ()
main = print $ match 0 us qs Error
    where
        us = [makeVar 2, makeVar 3]
        qs = [ ([PCon "Nil" [], PVar "ys"], (App (App (Var "A") (Var "u1")) (Var "ys")))
             , ([PVar "xs", PCon "Nil" [] ], (App (App (Var "B") (Var "u1")) (Var "xs")))
             , ( [ PCon "Cons" [ PVar "x", PVar "xs" ], PCon "Cons" [ PVar "y", PVar "ys"] ],
                 (App (App (App (App (App (Var "C") (Var "u1")) (Var "x")) (Var "xs")) (Var "y")) (Var "ys")) )
             ]

type Name = String

type Constructor = String

data Expr = Var Name
          | App Expr Expr
          | Case Name [Clause]
          | Fatbar Expr Expr
          | Error
          deriving (Show)

data Clause = Clause Constructor [Name] Expr deriving (Show)

data Pattern = PVar Name
             | PCon Name [Pattern]
             deriving (Show)

type Equation = ([Pattern], Expr)

arity :: Constructor -> Int
arity c =
        case c of
            "Cons" -> 2
            "Nil" -> 0
            _ -> 0

constructors :: Constructor -> [Constructor]
constructors c =
        case c of
            "Cons" -> ["Cons", "Nil"]
            "Nil"  -> ["Cons", "Nil"]
            _ -> []

subst :: Expr -> Name -> Name -> Expr
subst e@(Var n) before after = if n == before then Var after else Var n
subst (App e1 e2) before after = App (subst e1 before after) (subst e2 before after)
subst (Fatbar e1 e2) before after = Fatbar (subst e1 before after) (subst e2 before after)
subst (Case var clauses) before after = Case var (map (\c -> substClause c before after) clauses)

substClause :: Clause -> Name -> Name -> Clause
substClause (Clause c us e) before after = Clause c us (subst e before after)

isPVar :: Equation -> Bool
isPVar (PVar _: _, _) = True
isPVar _ = False

isPCon :: Equation -> Bool
isPCon q = not $ isPVar q

getCon :: Equation -> Constructor
getCon (PCon c _ : _, _) = c
getCon _ = ""

makeVar :: Int -> Name
makeVar i = "_u" ++ show i

partition :: Eq b => (a -> b) -> [a] -> [[a]]
partition _ [] = []
partition _ [x] = [[x]]
partition f (x:x':xs)
    | f x == f x' = tack x (partition f (x':xs))
    | otherwise = [x] : partition f (x':xs)

tack :: a -> [[a]] -> [[a]]
tack x xss = (x : head xss) : tail xss

match :: Int -> [Name] -> [Equation] -> Expr -> Expr
match _ [] qs def = foldr Fatbar def [e | ([], e) <- qs]
match k (u:us) qs def = foldr (matchVarCon k (u:us)) def (partition isPVar qs)

matchVarCon :: Int -> [Name] -> [Equation] -> Expr -> Expr
matchVarCon k us qs def | isPVar (head qs) = matchVar k us qs def
                        | isPCon (head qs) = matchCon k us qs def


matchVar :: Int -> [Name] -> [Equation] -> Expr -> Expr
matchVar k (u:us) qs def = match k us [(ps, subst e v u) | (PVar v : ps, e) <- qs ] def

matchCon :: Int -> [Name] -> [Equation] -> Expr -> Expr
matchCon k (u:us) qs def = Case u [matchClause c k (u:us) (choose c qs) def | c <- cs ]
    where
        cs = constructors (getCon (head qs))

matchClause :: Constructor -> Int -> [Name] -> [Equation] -> Expr -> Clause
matchClause c k (u:us) qs def =
        Clause c us' (match (k' + k) (us' ++ us) [(ps' ++ ps, e) | (PCon c ps' : ps, e) <- qs ] def)
        where
            k' = arity c
            us' = [makeVar (i + k) | i <- [1..k']]

choose c qs = [q | q <- qs, getCon q == c]
Case "_u2" [Clause "Cons" ["_u1","_u2"] (Case "_u3" [Clause "Cons" ["_u1","_u2"] (Case "_u2" [Clause "Cons" ["_u1","_u2"] (Case "_u3" [Clause "Cons" ["_u3","_u4"] (Fatbar (App (App (App (App (App (Var "C") (Var "u1")) (Var "_u1")) (Var "_u2")) (Var "_u3")) (Var "_u4")) Error),Clause "Nil" [] Error]),Clause "Nil" [] Error]),Clause "Nil" [] (Fatbar (App (App (Var "B") (Var "u1")) (Var "_u2")) (Case "_u2" [Clause "Cons" ["_u1","_u2"] (Case "_u3" [Clause "Cons" ["_u3","_u4"] (Fatbar (App (App (App (App (App (Var "C") (Var "u1")) (Var "_u1")) (Var "_u2")) (Var "_u3")) (Var "_u4")) Error),Clause "Nil" [] Error]),Clause "Nil" [] Error]))]),Clause "Nil" [] (Fatbar (App (App (Var "A") (Var "u1")) (Var "_u3")) (Case "_u3" [Clause "Cons" ["_u1","_u2"] (Case "_u2" [Clause "Cons" ["_u1","_u2"] (Case "_u3" [Clause "Cons" ["_u3","_u4"] (Fatbar (App (App (App (App (App (Var "C") (Var "u1")) (Var "_u1")) (Var "_u2")) (Var "_u3")) (Var "_u4")) Error),Clause "Nil" [] Error]),Clause "Nil" [] Error]),Clause "Nil" [] (Fatbar (App (App (Var "B") (Var "u1")) (Var "_u2")) (Case "_u2" [Clause "Cons" ["_u1","_u2"] (Case "_u3" [Clause "Cons" ["_u3","_u4"] (Fatbar (App (App (App (App (App (Var "C") (Var "u1")) (Var "_u1")) (Var "_u2")) (Var "_u3")) (Var "_u4")) Error),Clause "Nil" [] Error]),Clause "Nil" [] Error]))]))]

*** time: 0.34985 ***