classy.hs

------------------------------------------------------------------------
-- A mini Haskell compiler with typeclasses.
-- Originally written by Ben Lynn, modified by Ben Siraphob
------------------------------------------------------------------------
-- Delete code below and uncomment the block to compile in GHC
{-
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE OverlappingInstances #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
module Compiler where
import Prelude (Char, Int, String, succ)
import Data.Char (chr, ord)
import qualified Prelude
a <= b = if a Prelude.<= b then True else False
(*) = (Prelude.*)
(+) = (Prelude.+)
(-) = (Prelude.-)
(/) = Prelude.div
(%) = Prelude.mod
class Eq a where { (==) :: a -> a -> Bool };
class Show a where { show :: a -> String };
class Functor f where { fmap :: (a -> b) -> f a -> f b };
class Applicative f where { pure :: a -> f a; (<*>) :: f (a -> b) -> f a -> f b };
class Monad m where { return :: a -> m a ; (>>=) :: m a -> (a -> m b) -> m b};
instance Eq Char where { (==) x y = if x Prelude.== y then True else False };
instance Eq Int where { (==) x y = if x Prelude.== y then True else False };
instance Show Char where { show = Prelude.show };
infixr 5 ++;
infixr 9 .;
infixl 4 <*> , <$> , <* , *>;
infixl 3 <|>, <||>;
infixr 0 $;
infixl 7 *;
infixl 6 + , -;
-}
infixr 5 :, ++;
infixr 9 .;
infixl 4 <*> , <$> , <* , *>;
infixl 3 <|>, <||>;
infixr 0 $;
infixl 7 *;
infixl 6 + , -;
(*) = (.*.);
(+) = (.+.);
(-) = (.-.);
(%) = (.%.);
(/) = (./.);
-- Delete code above and uncomment the block to compile in GHC
undefined = undefined;
($) f = f;
id x = x;
const x y = x;
flip f x y = f y x;
(&) x f = f x;
(<$>) = fmap;
liftA2 f x = (<*>) (fmap f x);
(*>) = liftA2 $ \x y -> y;
(<*) = liftA2 const;
data Bool = True | False;
data Maybe a = Nothing | Just a;
data Either a b = Left a | Right b;
data Error a = Error String | Okay a;
-- fpair = flip curry
fpair p f = case p of { (,) x y -> f x y };
fst p = case p of { (,) x y -> x };
snd p = case p of { (,) x y -> y };
first f p = fpair p $ \x y -> (f x, y);
second f p = fpair p $ \x y -> (x, f y);
ife a b c = case a of { True -> b ; False -> c };
not a = case a of { True -> False; False -> True };
(.) f g x = f (g x);
(||) f g = ife f True (ife g True False);
(&&) f g = ife f (ife g True False) False;
(<) a b = not (a == b) && (a <= b);
-- fold a list
-- flist :: [a] -> b -> (a -> [a] -> b) -> b
flst xs n c = case xs of { [] -> n; (:) h t -> c h t };
-- (==) on lists
lstEq xs ys = case xs of
  { []       -> flst ys True (\h t -> False)
  ; (:) x xt -> flst ys False (\y yt -> ife (x == y) (lstEq xt yt) False)
  };
instance Eq a => Eq [a] where { (==) = lstEq };
(/=) x y = not (x == y);
-- Append two lists
(++) xs ys = flst xs ys (\x xt -> x:xt ++ ys);
-- maybe :: b -> (a -> b) -> Maybe a -> b
maybe n j m = case m of { Nothing -> n; Just x -> j x };
-- fold a maybe
-- fmaybe :: Maybe a -> b -> (a -> b) -> b
fmaybe m n j = case m of { Nothing -> n; Just x -> j x };
instance Show a => Show (Maybe a) where
  { show = maybe "Nothing" (\x -> "Just " ++ show x) };
instance Functor Maybe where
  { fmap f = maybe Nothing (Just . f) };
instance Applicative Maybe where
  { pure = Just ; (<*>) f y = maybe Nothing (`fmap` y) f};
instance Monad Maybe where
  { return = Just ; (>>=) ma f = maybe Nothing f ma };
fromMaybe a m = fmaybe m a id;
foldr c n l = flst l n (\h t -> c h (foldr c n t));
-- TODO: foldr1 should have type 
-- foldr1 :: Monoid a => (a -> a -> a) -> [a] -> a
-- Later, when we add foldables and traversables, it should be
-- foldr1 :: (Monoid m, Foldable t) => (m -> m -> m) -> t m -> m
-- foldr1' :: (a -> a -> a) -> [a] -> Maybe a
foldr1' c l =
    flst
       l
       Nothing
       (\h t ->
          foldr
            (\x m -> Just (fmaybe m x (c x)))
            Nothing
            l);

foldl f a bs = foldr (\b g x -> g (f x b)) id bs a;
-- foldl1' :: (p -> p -> p) -> [p] -> Maybe p
-- See above comments on the status of foldr1'
foldl1' f l = flst l Nothing (\x xs -> Just (foldl f x xs));
elem k = foldr (\x t -> ife (x == k) True t) False;
find f = foldr (\x t -> ife (f x) (Just x) t) Nothing;
concat = foldr (++) [];
itemize c = [c];
map f = foldr (\x xs -> f x : xs) [];
concatMap f l = concat (map f l);
instance Functor [] where { fmap = map };
instance Monad [] where { return = itemize ; (>>=) = flip concatMap };
instance Applicative [] where
  { pure = itemize
  ; (<*>) fs xs = fs >>= \f -> xs >>= \x -> return $ f x};
prependToAll s l = flst l [] (\x xs -> s : x : prependToAll s xs);
intersperse s l = flst l [] (\x xs -> x : prependToAll s xs);

-- Show a non-empty list
intercalate d = concat . intersperse d;
unwords = intercalate " ";
showList' l = "[" ++ intercalate "," (map show l) ++ "]";
showList l = case l of {
               []       -> "[]";
               (:) x xs -> showList' l
};

mapconcat f l = concat (map f l);
escapeC c = ife (c == '\n') "\\n"
            (ife (c == '\\') "\\\\"
             [c]);
showString s = "\"" ++ mapconcat escapeC s ++ "\"";

ifz n = ife (0 == n);
showInt' n = ifz n id (showInt' (n/10) . (:) (chr (48+(n%10))));
showInt n = ifz n ('0':) (showInt' n);

-- N.B. using show on Ints will make GHC fail to compile to due GHC
-- having multiple numeric types.
instance Show Int where { show n = showInt n "" };

instance Show String where { show = showString };
instance Show a => Show [a] where { show = showList };

any f = foldr (\x t -> ife (f x) True t) False;
-- lookupWith :: (a -> b -> Bool) -> a -> [(b, a)] -> Maybe a
lookupWith eq s =
  foldr (\h t -> fpair h (\k v -> ife (eq s k) (Just v) t)) Nothing;

lstLookup = lookupWith (==);

reverse = foldl (flip (:)) [];
zipWith f xs ys =
  case xs of
  { [] -> []
  ; (:) x xt ->
    case ys of
    { [] -> []
    ; (:) y yt -> f x y : zipWith f xt yt
    }
  };
zip = zipWith (,);

-- Representation of types
--          type ctor.  type var.  type app.
data Type = TC String | TV String | TAp Type Type;
-- Representation of AST
data Ast
  = R String     -- raw combinator assembly
  | V String     -- variable
  | A Ast Ast    -- application
  | L String Ast -- lambda abstraction
  | Proof Pred;  -- proof for typeclass instantiation?

--  * instance environment
--  * definitions, including those of instances
--  * Typed ASTs, ready for compilation, including ADTs and methods,
--    e.g. (==), (Eq a => a -> a -> Bool, select-==)
data Neat =
  Neat
    [(String, [Qual])]
    [Either (String, Ast) (String, (Qual, [(String, Ast)]))]
    [(String, (Qual, Ast))];

-- Parser combinators (applicative style)
-- From the paper "Parsec: A practical parsing library"
-- Written in a contrived way for use with mini-Haskell (e.g. no
-- nested pattern matching)

-- Position is a line, column
data Pos = Pos Int Int;

data State = State String Pos;
data Parsec a = Parsec (State -> Consumed a);
data Msg = Msg Pos String [String];

data Reply a = Err Msg
             | Ok a State Msg;

data Consumed a = Empty    (Reply a)
                | Consumed (Reply a);

parens s = '(':(s ++ ")");
showPos p = case p of { Pos r c -> unwords ["row:" , show r
                                           , "col: " , show c]};
instance Show Pos where { show = showPos };
showState s = case s of { State s p -> unwords [show s, parens (show p)]};
instance Show State where { show = showState };
-- showMsg m = case m of { Msg pos s1 s2 ->
--                          unwords ["Msg", show pos, show s1, show s2]};

-- instance Show Msg where
--   { show = showMsg };

-- showReply r = case r of { Err m -> unwords ["Err", show m]
--                         ; Ok a s m -> unwords ["Ok", show a, show s, show m]};
-- instance Show a => Show (Reply a) where { show = showReply };
-- showConsumed c = case c of { Empty m    -> unwords ["Empty", show m]
--                            ; Consumed m -> unwords ["Consumed", show m] };
-- instance Show a => Show (Consumed a) where
--   { show = showConsumed };
-- fromString :: String -> State
fromString s = State s (Pos 1 1);
-- parsec :: Parsec a -> State -> Consumed a
parsec p = case p of { Parsec f -> f };
-- parse :: Parsec a -> String -> Consumed a
parse p s = parsec p (fromString s);
-- bind :: Parsec a -> (a -> Parsec b) -> Parsec b
bind p f = Parsec $
           \state -> case parsec p state of
                       { Empty m ->
                         case m of
                           { Err msg         -> Empty (Err msg)
                           ; Ok x state' msg -> parsec (f x) state' }
                       ; Consumed m ->
                         Consumed
                         (case m of
                         { Err msg -> Err msg
                         ; Ok x state' msg ->
                           case parsec (f x) state' of
                             { Empty m    -> m
                             ; Consumed m -> m}})};
-- parsecpure :: a -> Parsec a
parsecpure x = Parsec $ \state ->
                case state of
                { State s pos -> Empty (Ok x state (Msg pos [] [])) };

instance Monad Parsec where
  { return = parsecpure
  ; (>>=) = bind };
instance Functor Parsec where
  { fmap f x = x >>= \x -> parsecpure (f x) };
instance Applicative Parsec where
  { pure = parsecpure
  ; (<*>) x y = x >>= \f -> y >>= \x -> parsecpure (f x) };

-- nextPos :: Pos -> Char -> Pos
nextPos p c = case p of
  { Pos line col ->
    ife (c == '\n') (Pos (line + 1) 0) (Pos line (col + 1))};

-- sat :: (Char -> Bool) -> Parsec Char
sat test = Parsec $ \state ->
                          case state of
                          { State input pos ->
                              case input of
                              { [] -> Empty (Err (Msg pos "end of input" []))
                              ; (:) c cs ->
                                  ife (test c)
                                  (let { newPos = nextPos pos c
                                       ; newState = State cs newPos }
                                    in Consumed (Ok c newState
                                                  (Msg pos [] [])))
                                  (Empty (Err (Msg pos [c] [])))}};


mergeMsg m1 m2 = case m1 of
              { Msg pos inp exp1 ->
                  case m2 of
                    { Msg _ _ exp2 -> Msg pos inp (exp1 ++ exp2)}};

mergeOk x inp msg1 msg2 = Empty (Ok x inp (mergeMsg msg1 msg2));

mergeError msg1 msg2 = Empty (Err (mergeMsg msg1 msg2));

-- (<|>) :: Parsec a -> Parsec a -> Parsec a

-- Given two parsers p, q, run p on the input. If it fails, then
-- continue by running q. The input is not backtracked before running
-- q.
-- p <|> q ::= <p> | <q>
(<|>) p q = Parsec $
            \state ->
              case parsec p state of
              { Empty m ->
                  case m of
                  { Err msg1 ->
                      case parsec q state of
                      { Empty m ->
                        case m of
                        { Err msg2 ->
                          mergeError msg1 msg2
                        ; Ok x inp msg2 ->
                          mergeOk x inp msg1 msg2 }
                      ; Consumed m -> Consumed m }
                  ; Ok x inp msg1 ->
                    case parsec q state of
                      { Empty m ->
                        case m of
                          { Err msg2 ->
                            mergeOk x inp msg1 msg2
                          ; Ok _ _ msg2 ->
                            mergeOk x inp msg1 msg2 }
                      ; Consumed m -> Consumed m }}
              ; Consumed m -> Consumed m };

-- Run parser p, if it consumed input and failed, pretend like it
-- didn't consume anything.
try p = Parsec $ \state -> case parsec p state of
                             { Empty m -> Empty m
                             ; Consumed m ->
                               case m of
                                 { Err msg ->
                                     Empty (Err msg)
                                 ; Ok x st msg ->
                                     Consumed (Ok x st msg)}};

(<||>) p q = try p <|> q;
-- many p ::= <p>*
many p = liftA2 (:) p (many p) <||> pure [];
-- many1 p ::= <p>+
many1 p = liftA2 (:) p (many p);
expect m exp = case m of { Msg pos inp _ -> Msg pos inp [exp] };

-- (<?>) :: Parsec a -> String -> Parsec a
(<?>) p exp = Parsec $ \state ->
                         case parsec p state of
                           { Empty m ->
                               Empty
                               (case m of
                                   { Err msg ->
                                       Err (expect msg exp)
                                   ; Ok x st msg ->
                                       Ok x st (expect msg exp)})
                           ; Consumed m -> Consumed m };
item = sat (const True);
-- sepBy1 p sep ::= <p> (<sep> <p>)*
sepBy1 p sep = liftA2 (:) p (many (sep *> p));
sepBy p sep = sepBy1 p sep <||> pure [];
char c = sat (== c) <?> show c;
string s =
  case s of
  { []       -> pure []
  ; (:) c cs -> char c *> string cs *> pure s};

-- between x y p ::=  <x> <p> <y>
between x y p = x *> (p <* y);
-- Parse line comments
-- com ::= '-' '-' <char c: c != '\n'>* '\n'
com = char '-' *> between (char '-') (char '\n') (many (sat (/= '\n')));
-- Block comments
-- notComEnd ::= <char c: c != '-'> | '-' <char c: c != '}'>
notComEnd = (sat (/= '-') <|> (char '-' *> sat (/= '}'))) *> pure [];
-- blockcom ::= "{-" (<blockcom> | <notComEnd>) "-}"
blockcom = let { content = many (blockcom <||> notComEnd) }
           in between (string "{-") (string "-}") content *> pure [];
-- Parse whitespace
sp =
  many
    ((pure <$> sat (\c -> (c == ' ') || (c == '\n'))) <|> com <|> blockcom);
-- Tokenize a parser, producing a parser that consumes trailing
-- whitespace.
-- tok p ::= <p> <sp>
tok p = p <* sp;
-- Parse a character (tokenized)
tokc = tok . char;
-- wantWith :: (a -> Bool) -> String -> Parser a -> Parser a
-- TODO: Consider backtracking the input on failure (similar to sat)?
wantWith pred str p = Parsec $ \s ->
                  case parsec p s of
                  { Empty m ->
                    Empty (case m of
                      { Err m -> Err m
                      ; Ok a state' m -> ife (pred a)
                                         (Ok a state' m)
                                         (Err (expect m str)) })
                  ; Consumed m ->
                    Consumed (case m of
                                { Err m -> Err m
                                ; Ok a state' m ->
                                    ife (pred a)
                                        (Ok a state' m)
                                        (Err (expect m str))})
                  };
-- want :: Eq a => Parser a -> a -> Parser a
want f s = wantWith (== s) s f;
-- paren a ::= '(' <a> ')'
paren = between (tokc '(') (tokc ')');
-- lower ::= 'a' | 'b' | 'c' ... 'z' | '_'
lower = sat (\x -> ((x <= 'z') && ('a' <= x)) || (x == '_')) <?> "lower";
-- upper ::= 'A' | 'B' | 'C' ... 'Z'
upper = sat (\x -> (x <= 'Z') && ('A' <= x)) <?> "upper";
-- digit ::= '0' | '1' | '2' ... '9'
digit = sat (\x -> (x <= '9') && ('0' <= x)) <?> "digit";
-- alpha ::= <lower> | <upper>
alpha = (lower <|> upper) <?> "alpha";
-- varLex ::= <lower> (<alpha> | <digit> | '\'')*
varLex = liftA2 (:) lower (many (alpha <|> digit <|> char '\''));
-- Constructor identifier
conId = tok (liftA2 (:) upper (many (alpha <|> digit <|> char '\'')));
keyword s = tok (want varLex s);
varId = tok (wantWith (\s -> not ((s == "of") || (s == "where"))) "variable" varLex);
-- Operator characters
opLex = many1 (sat (`elem` ":!#$%&*+./<=>?@\\^|-~"));
-- Operators
op = tok opLex <|> between (tokc '`') (tokc '`') varId;
var = varId <|> paren (tok opLex);
anyOne = pure <$> tok (sat (const True));
-- Lambda
-- lam r ::= '\\' <varId>+ "->" <r>
lam r =
  tokc '\\' *>
  liftA2 (flip (foldr L)) (many1 varId) (char '-' *> (tokc '>' *> r));

listify = fmap (foldr (\h t -> A (A (V ":") h) t) (V "[]"));
-- Escape characters
escChar = char '\\' *> (sat (`elem` "'\"\\") <|> (const '\n' <$> char 'n'));
litOne delim = (\c -> R ('#' : pure c)) <$> (escChar <||> sat (/= delim));
-- Integer literals
litInt = R . ('(' :) . (++ ")") <$> tok (many1 digit);
-- String literals
-- Notice that we do not consume whitespace after parsing the first ",
-- hence the use of char.
litStr = listify (between (char '"') (tokc '"') (many (litOne '"')));
-- Character literals
litChar = between (char '\'') (tokc '\'') (litOne '\'');
lit = litStr <|> litChar <|> litInt;
-- sqLst r ::= '[' <sepBy r ','> ']'
sqLst r = listify (between (tokc '[') (tokc ']') (sepBy r (tokc ',')));
-- alt r ::= ((<conId> | '(' (':' | ',') ')') | "[]") <varId>* "->" r
alt r =
  (,) <$>
  (conId <||> (pure <$> paren (tokc ':' <|> tokc ',')) <||>
   liftA2 (:) (tokc '[') (pure <$> tokc ']')) <*>
  liftA2 (flip (foldr L)) (many varId) (char '-' *> (tokc '>' *> r));
-- braceSep f ::= '{' <sepBy f ';'> '}'
braceSep f = between (tokc '{') (tokc '}') (sepBy f (tokc ';'));
-- alts r ::= <braceSep <alt r>>
alts r = braceSep (alt r);
cas' x as = foldl A (V (concatMap (('|' :) . fst) as)) (x : map snd as);
-- Case expressions
-- cas r ::= "case" r "of" <alts r>
cas r = liftA2 cas' (between (keyword "case") (keyword "of") r) (alts r);
-- thenComma r ::= ',' <r>
thenComma r =
  tokc ',' *> (((\x y -> A (A (V ",") y) x) <$> r) <||> pure (A (V ",")));
-- parenExpr r ::= <r> (<op> | <thenComma r>)
parenExpr r =
  liftA2
    (&)
    r
    (((\v a -> A (V v) a) <$> op) <||> thenComma r <||> pure id);

-- rightSect r ::= (<op> | ',') <r>
rightSect r =
  ((\v a -> A (A (V "\\C") (V v)) a) <$> (op <|> (pure <$> tokc ','))) <*> r;

-- Sections
-- section ::= '(' (<parenExpr r> | <rightSect r>) ')'
section r = paren (parenExpr r <|> rightSect r);

-- isFree :: String -> Ast -> Bool
-- Checks if a string v occurs free in expr.
isFree v expr = case expr of
  { R s     -> False
  ; V s     -> s == v
  ; A x y   -> isFree v x || isFree v y
  ; L w t   -> (v /= w) && isFree v t
  ; Proof _ -> False
  };

maybeFix s x = ife (isFree s x) (A (V "\\Y") (L s x)) x;

-- Definitions
-- def r ::= <var> <varId>* '=' <r>
def r =
  liftA2 (,) var (flip (foldr L) <$> many varId <*> (tokc '=' *> r));

-- Convert a list of let bindings and the let body into a single AST.
addLets ls x =
  foldr (\p t -> fpair p (\name def -> A (L name t) $ maybeFix name def)) x ls;

-- let r ::= "let" '{' <sepBy def r> '}' "in" <r>
letin r =
  liftA2
    addLets
    (between (keyword "let") (keyword "in") (braceSep (def r)))
    r;
-- atom r ::= <letin r> | <sqLst r> | <cas r> | <lam r> | <section r>
--          | '(' ',' ')' | (<conId> | <var>) | <lit>
atom r =
  letin r                             <|>
  sqLst r                             <||>
  cas r                               <|>
  lam r                               <||>
  section r                           <||>
  (paren (tokc ',') *> pure (V ","))  <||>
  (V <$> (conId <|> var))             <||>
  lit;

aexp r = fromMaybe undefined . foldl1' A <$> many1 (atom r);
fix f = f (fix f);

-- Parse infix operators
--            infix   infixl   infixr
data Assoc = NAssoc | LAssoc | RAssoc;

instance Show Assoc where
  { show a =
     case a of
     { NAssoc -> "NAssoc"
     ; LAssoc -> "LAssoc"
     ; RAssoc -> "RAssoc" } };

eqAssoc x y = case x of
  { NAssoc -> case y of { NAssoc -> True  ; LAssoc -> False ; RAssoc -> False }
  ; LAssoc -> case y of { NAssoc -> False ; LAssoc -> True  ; RAssoc -> False }
  ; RAssoc -> case y of { NAssoc -> False ; LAssoc -> False ; RAssoc -> True }
  };
instance Eq Assoc where { (==) = eqAssoc };

precOf s precTab = fmaybe (lstLookup s precTab) 5 fst;
assocOf s precTab = fmaybe (lstLookup s precTab) LAssoc snd;
opWithPrec precTab n = wantWith (\s -> n == precOf s precTab) "precTab" op;
-- opFold'
--   :: [(String, (a, Assoc))] -> Ast -> [(String, Ast)] -> Maybe Ast
opFold' precTab e xs =
  case xs of
  { [] -> Just e
  ; (:) x xt ->
      case find
             (\y ->
                not (assocOf (fst x) precTab == assocOf (fst y) precTab))
             xt of
      { Nothing ->
          case assocOf (fst x) precTab of
          { NAssoc ->
              case xt of
              {  []       -> Just $ fpair x (\op y -> A (A (V op) e) y)
              ;  (:) y yt -> Nothing }
          ; LAssoc -> Just $ foldl (\a b -> fpair b (\op y -> A (A (V op) a) y)) e xs
          ; RAssoc ->
              Just $ foldr (\a b -> fpair a (\op y e -> A (A (V op) e) (b y))) id xs e }
      ; Just y -> Nothing }};

expr precTab =
  fix $ \r n ->
    ife
      (n <= 9)
      ((fromMaybe undefined .) . opFold' precTab <$> r (succ n) <*>
       many (liftA2 (,) (opWithPrec precTab n) (r (succ n))))
      (aexp (r 0));

data Constr = Constr String [Type];
data Pred = Pred String Type;
data Qual = Qual [Pred] Type;

data Top = Adt Type [Constr]
         | Def (String, Ast)
         | Class String Type [(String, Type)]
         | Inst String Qual [(String, Ast)];

-- arrow type constructor
arr a = TAp (TAp (TC "->") a);
-- Parse type applications
bType r = fromMaybe undefined . foldl1' TAp <$> many1 r;

-- Parse types
_type r = fromMaybe undefined . foldr1' arr <$> sepBy (bType r) (tok (want opLex "->"));
typeConstant =
  (\s -> ife (s == "String") (TAp (TC "[]") (TC "Int")) (TC s)) <$> conId;

aType =
  paren
    (liftA2
       (&)
       (_type aType)
       ((tokc ',' *> ((\a b -> TAp (TAp (TC ",") b) a) <$> _type aType)) <||>
        pure id)) <||>
  typeConstant <||>
  (TV <$> varId) <||>
  (tokc '[' *>
   (tokc ']' *> pure (TC "[]") <||>
    TAp (TC "[]") <$> (_type aType <* tokc ']')));

simpleType c vs = foldl TAp (TC c) (map TV vs);
-- Data declarations
-- TODO: Add type, newtype declarations, deriving?
-- adt ::= "data" '=' <conId> <varId>* <sepBy (<conId> | <aType>*) '|'>
adt =
  liftA2
    Adt
    (between (keyword "data") (tokc '=') (liftA2 simpleType conId (many varId)))
    (sepBy (liftA2 Constr conId (many aType)) (tokc '|'));

-- Precedence
-- prec ::= <digit> <sp>
prec = (\c -> ord c - ord '0') <$> tok digit;
fixityList a n = fmap (, (n, a));
-- Fixity declaration
-- fixityDecl "kw" a ::= "kw" <prec> <sepBy <op> ','> ';'
fixityDecl kw a =
  between
    (keyword kw)
    (tokc ';')
    (liftA2 (fixityList a) prec (sepBy op (tokc ',')));

fixity =
  fixityDecl "infixl" LAssoc <||>
  fixityDecl "infixr" RAssoc <||>
  fixityDecl "infix" NAssoc;

noQual = Qual [];
-- genDecl ::= "::" <_type aType>
genDecl = liftA2 (,) var (char ':' *> tokc ':' *> _type aType);

-- Class declarations
-- classDecl ::= "class" <conId> <varId> "where" <braceSep genDecl>
classDecl =
  keyword "class" *>
  (Class <$> conId <*> (TV <$> varId) <*> (keyword "where" *> braceSep genDecl));

-- inst ::= <_type aType>
inst = _type aType;

-- Instance declarations
-- instDecl r ::= "instance" (<conId> <inst> "=>")? <conId> <inst>
--                "where" <braceSep <def r>>
instDecl r =
  keyword "instance" *>
  ((\ps cl ty defs -> Inst cl (Qual ps ty) defs) <$>
   (liftA2 ((pure .) . Pred) conId (inst <* (char '=' *> tokc '>')) <||>
    pure []) <*>
   conId <*>
   inst <*>
   (keyword "where" *> braceSep (def r)));

-- Top level declarations
-- tops ::= <sepBy (<adt> | <def> | <classDecl> | <instDecl>) ';'>
tops precTab =
  sepBy
    (adt <||> Def <$> def (expr precTab 0) <||> classDecl <||>
     instDecl (expr precTab 0))
    (tokc ';');

-- A program consists of whitespace, followed by fixity declarations,
-- then top level declarations
-- program' ::= <sp> <fixity>* <tops>
program' = sp *> (concat <$> many fixity) >>= tops;

eqPre = case parse program' $
  "class Eq a where { (==) :: a -> a -> Bool };\n" ++
  "class Show a where { show :: a -> String };\n" ++
  "class Functor f where { fmap :: (a -> b) -> f a -> f b };\n" ++
  "class Applicative f where { pure :: a -> f a; (<*>) :: f (a -> b) -> f a -> f b };\n" ++
  "class Monad m where { return :: a -> m a ; (>>=) :: m a -> (a -> m b) -> m b};\n" ++
  "instance Eq Int where { (==) = intEq };\n" of
  { Empty m ->
    case m of
      -- TODO: replace with show msg
      { Err msg  -> undefined
      ; Ok l _ _ -> l}
  ; Consumed m ->
    case m of
      -- TODO: replace with show msg
      { Err msg  -> undefined
      ; Ok l _ _ -> l}
  };
program =
  ((eqPre ++
      -- data [] a = [] | (:) a ([] a)
    [ Adt
        (TAp (TC "[]") (TV "a"))
        [Constr "[]" [], Constr ":" [TV "a", TAp (TC "[]") (TV "a")]]
    -- data (,) a b = (,) a b
    , Adt (TAp (TAp (TC ",") (TV "a")) (TV "b")) [Constr "," [TV "a", TV "b"]]
    ]) ++) <$>
  program';


-- Primitives
-- prims :: [(String, (Qual, Ast))]
prims =
  let { ii = arr (TC "Int") (TC "Int")
      ; iii = arr (TC "Int") ii
      ; bin s = R $ "``BT`T" ++ s }
   in map (second (first noQual)) $
      [ ("\\Y", (arr (arr (TV "a") (TV "a")) (TV "a"), R "Y"))
      , ( "\\C"
        , ( arr
              (arr (TV "a") (arr (TV "b") (TV "c")))
              (arr (TV "b") (arr (TV "a") (TV "c")))
          , R "C"))
      , ("intEq", (arr (TC "Int") (arr (TC "Int") (TC "Bool")), bin "="))
      , ("<=", (arr (TC "Int") (arr (TC "Int") (TC "Bool")), bin "L"))
      , ("chr", (ii, R "I"))
      , ("ord", (ii, R "I"))
      , ("succ", (ii, R "`T`(1)+"))
      ] ++
      map (\s -> ('.':s ++ ".", (iii, bin s))) ["+", "-", "*", "/", "%"];

-- Total variant
rank ds v =
  let { loop l v c =
         case l of
         { [] -> Nothing
         ; (:) x xs ->
            ife (v == fst x) (Just ('[' : showInt c "]")) (loop xs v (succ c)) } }
   in loop ds v 0;

-- showC :: [(String, b)] -> Ast -> String
-- Total version of showC
showC ds t = case t of
  { R s     -> Just s
  ; V v     -> rank ds v
  ; A x y   -> liftA2 (\a b -> '`':a ++ b) (showC ds x) (showC ds y)
  ; L w t   -> Nothing
  ; Proof _ -> Nothing
  };

-- De Bruijn encoding of lambda calculus terms
--        z    s       lift ast   abs.   app.
data LC = Ze | Su LC | Pass Ast | La LC | App LC LC;

-- Convert the AST into a nameless representation
-- debruijn :: [String] -> Ast ->  LC
debruijn n e = case e of
  { R s     -> pure $ Pass (R s)
  ; V v     -> pure $ foldr (\h m -> ife (h == v) Ze (Su m)) (Pass (V v)) n
  ; A x y   -> App <$> debruijn n x <*> debruijn n y
  ; L s t   -> La <$> debruijn (s:n) t
  ; Proof _ -> Nothing
  };

-- See Kiselyov's paper - "Lambda to SKI, semantically", pages 10 - 11
--         V       C            N          W
data Sem = Defer | Closed Ast | Need Sem | Weak Sem;
-- ($$) algorithm

-- ($$), case Defer
-- Parameters: r == self
ldef r y = case y of
  { -- (V, V)   -> N (C S.(S $! I $! I))
    Defer    -> Need (Closed (A (A (R "S") (R "I")) (R "I")))
    -- (V, C d) -> N (C S.(kC $! kI $! d))
  ; Closed d -> Need (Closed (A (R "T") d))
    -- (V, N e) -> N (C S.(kS $! kI) $$ e)
  ; Need e   -> Need (r (Closed (A (R "S") (R "I"))) e)
    -- (V, W e) -> N (C (S.(kS $! kI)) $$ e)
  ; Weak e   -> Need (r (Closed (R "T")) e)
  };

-- ($$), case Closed
-- d is the argument to Closed (i.e. lclo r (Closed d) y = ...)
lclo r d y = case y of
  { -- (C d, V)     -> N (C d)
    Defer     -> Need (Closed d)
    -- (C d1, C d2) -> C (S.(d1 $! d2))
  ; Closed dd -> Closed (A d dd)
    -- (C d, N e)   -> N (C S.(kB $! d) $$ e)
  ; Need e    -> Need (r (Closed (A (R "B") d)) e)
    -- (C d, W e)   -> W (C d $$ e)
  ; Weak e    -> Weak (r (Closed d) e)
  };

-- ($$), case Need
-- e is the argument to Need (i.e. lnee r (Need e) y = ...)
lnee r e y = case y of
  { -- (N e, V)     -> N (C S.kS $$ e $$ C S.kI)
    Defer    -> Need (r (r (Closed (R "S")) e) (Closed (R "I")))
    -- (N e, C d)   -> N (C S.(kC $! kC $! d) $$ e)
  ; Closed d -> Need (r (Closed (A (R "R") d)) e)
    -- (N e1, N e2) -> N ((C S.kS) $$ e1 $$ e2)
  ; Need ee  -> Need (r (r (Closed (R "S")) e) ee)
    -- (N e1, W e2) -> N ((C S.kC) $$ e1 $$ e2)
  ; Weak ee  -> Need (r (r (Closed (R "C")) e) ee)
  };

-- ($$), case Weak
-- e is the argument to Weak (i.e. lweak r (Weak e) y = ...)
lwea r e y = case y of
  { -- (W e, V)     -> N e
    Defer    -> Need e
    -- (W e, C d)   -> W (e $$ C d)
  ; Closed d -> Weak (r e (Closed d))
    -- (W e1, N e2) -> N ((C S.kB) $$ e1 $$ e2)
  ; Need ee  -> Need (r (r (Closed (R "B")) e) ee)
    -- (W e1, W e2) -> W (e1 $$ e2)
  ; Weak ee  -> Weak (r e ee)
  };

-- ($$), the full thing.
babsa x y = case x of
  { Defer    -> ldef babsa y
  ; Closed d -> lclo babsa d y
  ; Need e   -> lnee babsa e y
  ; Weak e   -> lwea babsa e y
  };

-- Full bracket abstraction algorithm, from De Bruijn to combinators
-- babs :: LC -> Sem
babs t = case t of
  { -- let z : (a*y, a) repr = V
    Ze -> Defer
    -- let s: (b*y, a) repr -> (_*(b*y), a) repr = fun e -> W e
    -- Looks like this version recurs on e.
  ; Su e -> Weak (babs e)
    -- A lifted AST is closed.
  ; Pass s -> Closed s
    -- See "lam" function on page 10 of Kiselyov
    -- Lambda abstraction
  ; La t -> case babs t of
    { -- V     -> C S.kI
      Defer    -> Closed (R "I")
      -- C d   -> C S.(kK $! d)
      -- Remark: d is a closed body of a lambda abstraction, so the
      -- variable being abstracted over is not used and thus we can
      -- use the K combinator
    ; Closed d -> Closed (A (R "K") d)
      -- N e   -> e
    ; Need e   -> e
      -- W e   -> (C S.kK) $$ e
    ; Weak e   -> babsa (Closed (R "K")) e
    }
    -- Application
  ; App x y -> babsa (babs x) (babs y)
  };

-- Convert an AST into debruijn form, then perform bracket abstraction,
-- return if and only if we have a closed form.
-- nolam :: Ast -> Maybe Ast
nolam x = debruijn [] x >>= \x ->
  case babs x of
  { Defer    -> Nothing
  ; Closed d -> Just d
  ; Need e   -> Nothing
  ; Weak e   -> Nothing
  };

dump tab ds =
  case ds of
  { [] -> return []
  ; (:) h t ->
    nolam (snd h) >>= \a ->
    showC tab a   >>= \b ->
    dump tab t    >>= \c ->
    return (b ++ (';' : c)) };

asm ds = dump ds ds;

-- Apply substitutions to a tree
apply sub t = case t of
  { TC v    -> t
    -- Lookup v in the substitutions, if not found, replace it with t
  ; TV v    -> fromMaybe t (lstLookup v sub)
  ; TAp a b -> TAp (apply sub a) (apply sub b)
  };

-- Combine two substitution lists while applying the substitutions in
-- the first.
(@@) s1 s2 = map (second (apply s1)) s2 ++ s1;

-- Occurs check
-- occurs :: String -> Type -> Bool
occurs s t = case t of
  { TC v    -> False
  ; TV v    -> s == v
  ; TAp a b -> occurs s a || occurs s b
  };

-- Bind the type variable s to the type t
varBind s t = case t of
  { --         Just (pure (s, t)) is clearer
    TC v    -> pure (pure (s, t))
    -- Binding a variable with another variable
  ; TV v    -> ife (v == s) (pure []) (pure (pure (s, t)))
    -- Infinite types not allowed
  ; TAp a b -> ife (occurs s t) Nothing (pure (pure (s, t)))
  };

-- Most general unifier.  Given two type trees, possibly return the
-- assignments that make them equal.

-- We pass unify as an argument to achieve mutual recursion.
mgu unify t u = case t of
  { TC a -> case u of
    { TC b    -> ife (a == b) (pure []) Nothing
    ; TV b    -> varBind b t
    ; TAp a b -> Nothing
    }
  ; TV a -> varBind a u
  ; TAp a b -> case u of
    { TC b    -> Nothing
    ; TV b    -> varBind b t
    ; TAp c d -> unify b d (mgu unify a c)
    }
  };

unify a b =
  maybe Nothing (\s -> fmap (@@ s) (mgu unify (apply s a) (apply s b)));

-- instantiate' ::
--   Type -> Int -> [(String, Type)] -> ((Type, Int), [(String, Type)])
instantiate' t n tab = case t of
  { TC s -> ((t, n), tab)
  ; TV s -> case lstLookup s tab of
    { Nothing -> let { va = TV (s ++ '_':showInt n "") }
                 in ((va, n + 1), (s, va):tab)
    ; Just v -> ((v, n), tab)
    }
  ; TAp x y ->
    fpair (instantiate' x n tab) $ \tn1 tab1 ->
    fpair tn1 $ \t1 n1 ->
    fpair (instantiate' y n1 tab1) $ \tn2 tab2 ->
    fpair tn2 $ \t2 n2 -> ((TAp t1 t2, n2), tab2)
  };

instantiatePred pred xyz =
  case pred of
  { Pred s t ->
      fpair xyz $ \xy tab ->
        fpair xy $ \out n ->
          first (first ((: out) . Pred s)) (instantiate' t n tab) };

-- instantiate :: Qual -> Int -> (Qual, Int)
instantiate qt n =
  case qt of
  { Qual ps t ->
      fpair (foldr instantiatePred (([], n), []) ps) $ \xy tab ->
        fpair xy $ \ps1 n1 -> first (Qual ps1) (fst (instantiate' t n1 tab)) };


-- type SymTab = [(String, (Qual, Ast))];
-- type Subst = [(String, Type)];

-- infer' ::
--   [(String, (Qual, b))]
--   -> [(String, Type)]
--   -> Ast
--   -> (Maybe [(String, Type)], Int)
--   -> ((Type, Ast), (Maybe [(String, Type)], Int))
infer' typed loc ast csn =
  fpair csn $ \cs n ->
    let { va = TV ('_' : showInt n "") }
     in case ast of
        {  -- Raw code is treated as Int
           R s -> ((TC "Int", ast), csn)
        ;  V s ->
             fmaybe
               (lstLookup s loc)
               (fmaybe (lstLookup s typed) undefined $ \ta ->
                  fpair (instantiate (fst ta) n) $ \q n1 ->
                    case q of {
                      Qual preds ty ->
                        ((ty, foldl A ast (map Proof preds)), (cs, n1))
                    })
               (flip (,) csn . flip (,) ast)
        ;  A x y ->
             fpair (infer' typed loc x (cs, n + 1)) $ \tax csn1 ->
               fpair tax $ \tx ax ->
                 fpair (infer' typed loc y csn1) $ \tay csn2 ->
                   fpair tay $ \ty ay ->
                     ((va, A ax ay), first (unify tx (arr ty va)) csn2)
           -- Lambda abstraction.  Infer the body of the lambda with
           -- the substitution list extended with s := <newvar>
        ;  L s x ->
             first
               (\ta -> fpair ta $ \t a -> (arr va t, L s a))
               (infer' typed ((s, va) : loc) x (cs, n + 1))
        ;  Proof _ -> undefined };


onType f pred = case pred of { Pred s t -> Pred s (f t) };

-- typeEq :: Type -> Type -> Bool
typeEq t u = case t of
  { TC s -> case u of
    { TC t    -> t == s
    ; TV _    -> False
    ; TAp _ _ -> False
    }
  ; TV s ->  case u of
    { TC _    -> False
    ; TV t    -> t == s
    ; TAp _ _ -> False
    }
  ; TAp a b -> case u of
    { TC _    -> False
    ; TV _    -> False
    ; TAp c d -> typeEq a c && typeEq b d
    }
  };

instance Eq Type where { (==) = typeEq };
predEq p q = case p of { Pred s a -> case q of { Pred t b ->
  (s == t) && (a == b) }};

instance Eq Pred where { (==) = predEq };
predApply sub = onType (apply sub);

all f = foldr ((&&) . f) True;
filter f = foldr (\x xs -> ife (f x) (x:xs) xs) [];

intersect xs ys = filter (\x -> fmaybe (find (== x) ys) False (const True)) xs;

merge s1 s2 =
  ife
    (all (\v -> apply s1 (TV v) == apply s2 (TV v)) $
     map fst s1 `intersect` map fst s2)
    (Just $ s1 ++ s2)
    Nothing;

match h t = case h of
  { TC a -> case t of
    { TC b    -> ife (a == b) (return []) Nothing
    ; TV b    -> Nothing
    ; TAp a b -> Nothing
    }
  ; TV a -> return [(a, t)]
  ; TAp a b -> case t of
    { TC b -> Nothing
    ; TV b -> Nothing
    ; TAp c d -> match a c >>= \ac ->
                 match b d >>= \bd ->
                 merge ac bd}};

matchPred h p = case p of { Pred _ t -> match h t };

-- TODO: Add support for printing of infix type operators.
showType t = case t of
  { TC s    -> s
  ; TV s    -> s
  ; TAp a b -> concat ["(", showType a, " ", showType b, ")"]
  };

instance Show Type where { show = showType };
showPred p = case p of { Pred s t -> s ++ (' ':show t) ++ " => "};

findInst r qn p insts =
  case insts of
  {  [] ->
       fpair qn $ \q n ->
         let { v = '*' : showInt n "" }
          in (((p, v) : q, n + 1), V v)
  ;  (:) i is ->
       case i of {
         Qual ps h ->
           case matchPred h p of
             { Nothing -> findInst r qn p is
             ; Just u ->
               foldl
                 (\qnt p ->
                    fpair qnt $ \qn1 t -> second (A t) (r (predApply u p) qn1))
                 ( qn
                 , V (case p of
                       { Pred s _ -> showPred $ Pred s h }))
                 ps }}};


findProof is pred psn = fpair psn $ \ps n -> case lookupWith (==) pred ps of
  { Nothing -> case pred of { Pred s t -> case lstLookup s is of
    { Nothing    -> undefined  -- No instances!
    ; Just insts -> findInst (findProof is) psn pred insts
    }}
  ; Just s -> (psn, V s)
  };

prove' ienv sub psn a = case a of
  { R _ -> (psn, a)
  ; V _ -> (psn, a)
  ; A x y -> let { p1 = prove' ienv sub psn x } in fpair p1 $ \psn1 x1 ->
    second (A x1) (prove' ienv sub psn1 y)
  ; L s t -> second (L s) (prove' ienv sub psn t)
  ; Proof raw -> findProof ienv (predApply sub raw) psn
  };

-- prove :: [(String, [Qual])] -> (Type, Ast) -> Subst -> (Qual, Ast)
prove ienv ta sub =
  fpair ta $ \t a ->
    fpair (prove' ienv sub ([], 0) a) $ \psn x ->
      fpair psn $ \ps _ ->
        (Qual (map fst ps) (apply sub t), foldr (L . snd) x ps);

dictVars ps n =
  flst ps ([], n) $ \p pt ->
    first ((p, '*' : showInt n "") :) (dictVars pt $ n + 1);

-- qi = Qual of instance, e.g. Eq t => [t] -> [t] -> Bool
inferMethod ienv typed qi def = fpair def $ \s expr ->
  fpair (infer' typed [] expr (Just [], 0)) $ \ta msn ->
  case lstLookup s typed of
    { Nothing -> undefined -- No such method.
    -- e.g. qac = Eq a => a -> a -> Bool, some AST (product of single method)
    ; Just qac -> fpair msn $ \ms n -> case ms of
      { Nothing -> undefined  -- Type check fails.
      ; Just sub -> fpair (instantiate (fst qac) n) $ \q1 n1 -> case q1 of
        { Qual psc tc -> case psc of
        { [] -> undefined  -- Unreachable.
        ; (:) headPred shouldBeNull -> case qi of { Qual psi ti ->
          case headPred of { Pred _ headT -> case match headT ti of
          { Nothing -> undefined
          -- e.g. Eq t => [t] -> [t] -> Bool
          -- instantiate and match it against type of ta
          ; Just subc ->
            fpair (instantiate (Qual psi $ apply subc tc) n1) $ \q2 n2 ->
            case q2 of { Qual ps2 t2 -> fpair ta $ \tx ax ->
              case match (apply sub tx) t2 of
                { Nothing -> undefined  -- Class/instance type conflict.
                ; Just subx -> snd $ prove' ienv (subx @@ sub) (dictVars ps2 0) ax
              }}}}}}}}};

genProduct ds = foldr L (L "*" $ foldl A (V "*") $ map V ds) ds;

inferInst ienv typed inst = fpair inst $ \cl qds -> fpair qds $ \q ds ->
  case q of { Qual ps t -> let { s = showPred $ Pred cl t } in
  (s, (,) (noQual $ TC "DICT") $ maybeFix s $
  foldr (L . snd)
    (foldl A (genProduct $ map fst ds)
       (map (inferMethod ienv typed q) ds))
    (fst $ dictVars ps 0)
  )
  };
  
inferDefs ienv defs typed =
  flst defs (Right $ reverse typed) $ \edef rest ->
    case edef of
    { Left def ->
        fpair def $ \s expr ->
          fpair (infer' typed [] (maybeFix s expr) (Just [], 0)) $ \ta msn ->
            fpair msn $ \ms _ ->
              case fmap (prove ienv ta) ms of
              { Nothing -> Left ("bad type: " ++ s)
              ; Just qa -> inferDefs ienv rest ((s, qa) : typed)}
    ; Right inst -> inferDefs ienv rest (inferInst ienv typed inst : typed)};

conOf con = case con of { Constr s _ -> s };
mkCase t cs =
  ( concatMap (('|' :) . conOf) cs
  , ( noQual $
      arr t $
      foldr
        (arr .
         (\c ->
            case c of
            {  Constr _ ts -> foldr arr (TV "case") ts }))
        (TV "case")
        cs
    , L "x" $ V "x"));

mkStrs = snd . foldl (\p u -> fpair p (\s l -> ('*':s, s : l))) ("*", []);

-- For example, creates `Just = \x a b -> b x`.
-- Scott encoding
scottEncode vs s ts = foldr L (foldl (\a b -> A a (V b)) (V s) ts) (ts ++ vs);
scottConstr t cs c = case c of { Constr s ts -> (s,
  ( noQual $ foldr arr t ts
  , scottEncode (map conOf cs) s $ mkStrs ts)) };
mkAdtDefs t cs = mkCase t cs : map (scottConstr t cs) cs;

fneat neat f = case neat of { Neat a b c -> f a b c };

select f xs acc =
  flst xs (Nothing, acc) $ \x xt ->
    ife (f x) (Just x, xt ++ acc) (select f xt (x : acc));

addInstance s q is = fpair (select ((== s) . fst) is []) $ \m xs -> case m of
  { Nothing  -> (s, [q]):xs
  ; Just sqs -> second (q:) sqs:xs
  };

mkSel ms s = L "*" $ A (V "*") $ foldr (L . ('*' :) . fst) (V $ '*' : s) ms;

untangle = foldr (\top acc -> fneat acc $ \ienv fs typed -> case top of
  { Adt t cs -> Neat ienv fs (mkAdtDefs t cs ++ typed)
  ; Def f -> Neat ienv (Left f : fs) typed
  ; Class classId v ms -> Neat ienv fs (
    map (\st -> fpair st $ \s t -> (s, (Qual [Pred classId v] t, mkSel ms s))) ms
    ++ typed)
  ; Inst cl q ds -> Neat (addInstance cl q ienv) (Right (cl, (q, ds)):fs) typed
  }) (Neat [] [] prims);

infer prog = fneat (untangle prog) inferDefs;

showQual q = case q of { Qual ps t -> concatMap showPred ps ++ show t };

instance Show Qual where { show = showQual };
dumpTypes' m =
  case m of
    { Err msg -> "parse error"
    ; Ok prog _ _ ->
        case infer prog of
          { Left err -> err
          ; Right typed ->
              concatMap
              (\p -> fpair p $ \s qa -> s ++ " :: " ++ show (fst qa) ++ "\n")
              typed}};
dumpTypes s = case parse program s of
  { Empty m    -> dumpTypes' m
  ; Consumed m -> dumpTypes' m };

-- TODO: replace with show msg
compile' m = case m of
      { Err msg -> "parse error"
      ; Ok prog _ _ ->
          case infer prog of
            { Left err  -> err
            ; Right qas -> fromMaybe undefined (asm $ map (second snd) qas)}};

compile s = case parse program s of
  { Empty m    -> compile' m
  ; Consumed m -> compile' m };