new grammar and adapted renamer

Grammar.cf

@@ -1,50 +1,91 @@
+--------------------------------------------------------------------------------
+-- * PROGRAM
+--------------------------------------------------------------------------------
 
 Program. Program ::= [Def] ;
 
+--------------------------------------------------------------------------------
+-- * TOP-LEVEL
+--------------------------------------------------------------------------------
+
 DBind. Def ::= Bind ;
+DSig.  Def ::= Sig ;
 DData. Def ::= Data ;
-separator Def ";" ;
 
-Bind. Bind ::= Ident ":" Type ";"
+Sig. Sig ::= LIdent ":" Type ;
-               Ident [Ident] "=" Exp ;
 
-Data. Data ::= "data" Constr "where" "{" [Constructor] "}" ;
+Bind. Bind ::= LIdent [LIdent] "=" Exp ;
 
-Constructor. Constructor ::= Ident ":" Type ;
+--------------------------------------------------------------------------------
-separator nonempty Constructor "" ;
+-- * TYPES
+--------------------------------------------------------------------------------
 
-TMono.   Type1 ::= "_" Ident ;
+         TLit.     Type2 ::= UIdent ;
-TPol.    Type1 ::= "'" Ident ;
+         TVar.     Type2 ::= TVar ;
-TConstr. Type1 ::= Constr ;
+         TAll.     Type1 ::= "forall" TVar "." Type ;
-TArr.    Type  ::= Type1 "->" Type ;
+         TIndexed. Type1 ::= Indexed ;
+internal TEVar.    Type1 ::= TEVar ;
+         TFun.     Type  ::= Type1 "->" Type ;
 
-Constr.  Constr ::= Ident "(" [Type] ")" ;
+         MkTVar.  TVar  ::= LIdent ;
+internal MkTEVar. TEVar ::= LIdent ;
+
+--------------------------------------------------------------------------------
+-- * DATA TYPES
+--------------------------------------------------------------------------------
+
+Constructor. Constructor ::= UIdent ":" Type ;
+
+Indexed. Indexed ::= UIdent "(" [Type] ")" ;
+
+Data. Data ::= "data" Indexed "where" "{" [Constructor] "}" ;
+
+--------------------------------------------------------------------------------
+-- * EXPRESSIONS
+--------------------------------------------------------------------------------
 
--- TODO: Move literal to its own thing since it's reused in Init as well.
 EAnn.   Exp5 ::= "(" Exp ":" Type ")" ;
-EId.    Exp4 ::= Ident ;
+EId.    Exp4 ::= LIdent ;
-ELit.   Exp4 ::= Literal ;
+ELit.   Exp4 ::= Lit ;
 EApp.   Exp3 ::= Exp3 Exp4 ;
 EAdd.   Exp1 ::= Exp1 "+" Exp2 ;
-ELet.   Exp  ::= "let" Ident "=" Exp "in" Exp ; 
+ELet.   Exp  ::= "let" LIdent "=" Exp "in" Exp ; 
-EAbs.   Exp  ::= "\\" Ident "." Exp ;
+EAbs.   Exp  ::= "\\" LIdent "." Exp ;
 ECase.  Exp  ::= "case" Exp "of" "{" [Inj] "}";
 
-LInt. Literal ::= Integer ;
+--------------------------------------------------------------------------------
+-- * LITERALS
+--------------------------------------------------------------------------------
+
+LInt. Lit ::= Integer ;
+LChar. Lit ::= Char ;
+
+--------------------------------------------------------------------------------
+-- * CASE
+--------------------------------------------------------------------------------
 
 Inj. Inj ::= Init "=>" Exp ;
-separator nonempty Inj ";" ;
 
-InitLit. Init    ::= Literal ;
+InitLit. Init         ::= Lit ;
-InitConstr. Init ::= Ident [Ident] ;
+InitConstructor. Init ::= UIdent [LIdent] ;
-InitCatch. Init  ::= "_" ;
+InitCatch. Init       ::= "_" ;
 
+--------------------------------------------------------------------------------
+-- * AUX
+--------------------------------------------------------------------------------
+
+separator Def ";" ;
+separator nonempty Constructor "" ;
 separator Type " " ;
-coercions Type 2 ;
+separator nonempty Inj ";" ;
-
 separator Ident " ";
+separator LIdent " ";
 
 coercions Exp 5 ;
+coercions Type 2 ;
+
+token UIdent (upper (letter | digit | '_')*) ;
+token LIdent (lower (letter | digit | '_')*) ;
 
 comment "--" ;
 comment "{-" "-}" ;

sample-programs/basic-1

@@ -1,2 +1,2 @@
-f : _Int -> _Int ;
+f : Int -> Int ;
 f = \x. x+1 ;

sample-programs/basic-2

@@ -1,5 +1,5 @@
-add : _Int -> _Int -> _Int ;
+add : Int -> Int -> Int ;
 add x = \y. x+y;
 
-main : _Int ;
+main : Int ;
 main = (\z. z+z) ((add 4) 6) ;

sample-programs/basic-3

@@ -1,2 +1,2 @@
-main : _Int ;
+main : Int ;
 main = (\x. x+x+3) ((\x. x) 2) ;

sample-programs/basic-4

@@ -1,2 +1,2 @@
-f : _Int -> _Int ;
+f : Int -> Int ;
 f x = let g = (\y. y+1) in g (g x)

sample-programs/basic-5

@@ -1,8 +1,8 @@
-double : _Int -> _Int ;
+double : Int -> Int ;
 double n = n + n;
 
-id : 'a -> 'a ;
+id : forall a. a -> a ;
 id x = x ;
 
-main : _Int ;
+main : Int ;
 main = id double 5;

sample-programs/basic-6

@@ -3,7 +3,7 @@ data Bool () where {
     False : Bool ()
 };
 
-main : Bool () -> _Int ;
+main : Bool () -> Int ;
 main b = case b of {
     False => 0;
     True => 0

sample-programs/basic-7

@@ -3,7 +3,7 @@ data Bool () where {
     False : Bool ()
 };
 
-ifThenElse : Bool () -> 'a -> 'a -> 'a;
+ifThenElse : forall a. Bool () -> a -> a -> a;
 ifThenElse b if else = case b of {
         True => if;
         False => else

sample-programs/basic-8

@@ -1,22 +1,22 @@
-data Maybe ('a) where {
+data Maybe (a) where {
-    Nothing : Maybe ('a)
+    Nothing : Maybe (a)
-    Just : 'a -> Maybe ('a)
+    Just : forall a. a -> Maybe (a)
 };
 
-fromJust : Maybe ('a) -> 'a ;
+fromJust : Maybe (a) -> a ;
 fromJust a =
     case a of {
         Just a => a
     };
 
-fromMaybe : 'a -> Maybe ('a) -> 'a ;
+fromMaybe : a -> Maybe (a) -> a ;
 fromMaybe a b =
     case b of {
         Just a => a;
         Nothing => a
     };
 
-maybe : 'b -> ('a -> 'b) -> Maybe ('a) -> 'b;
+maybe : b -> (a -> b) -> Maybe (a) -> b;
 maybe b f ma =
     case ma of {
         Just a => f a;

src/Main.hs

@@ -11,7 +11,8 @@ import Grammar.Print (printTree)
 import Renamer.Renamer (rename)
 import System.Environment (getArgs)
 import System.Exit (exitFailure, exitSuccess)
-import TypeChecker.TypeChecker (typecheck)
+
+-- import TypeChecker.TypeChecker (typecheck)
 
 main :: IO ()
 main =
@@ -28,12 +29,12 @@ main' s = do
     putStrLn $ printTree parsed
 
     putStrLn "\n-- Renamer --"
-    let renamed = rename parsed
+    renamed <- fromRenamerErr . rename $ parsed
     putStrLn $ printTree renamed
 
-    putStrLn "\n-- TypeChecker --"
+    -- putStrLn "\n-- TypeChecker --"
-    typechecked <- fromTypeCheckerErr $ typecheck renamed
+    -- typechecked <- fromTypeCheckerErr $ typecheck renamed
-    putStrLn $ show typechecked
+    -- putStrLn $ show typechecked
 
     -- putStrLn "\n-- Lambda Lifter --"
     -- let lifted = lambdaLift typechecked
@@ -55,6 +56,16 @@ fromCompilerErr =
         )
         pure
 
+fromRenamerErr :: Err a -> IO a
+fromRenamerErr =
+    either
+        ( \err -> do
+            putStrLn "\nRENAME ERROR"
+            putStrLn err
+            exitFailure
+        )
+        pure
+
 fromSyntaxErr :: Err a -> IO a
 fromSyntaxErr =
     either

src/Renamer/Renamer.hs

@@ -1,56 +1,101 @@
 {-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE OverloadedRecordDot #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE PatternSynonyms #-}
 
-module Renamer.Renamer where
+module Renamer.Renamer (rename) where
 
 import Auxiliary (mapAccumM)
+import Control.Applicative (Applicative (liftA2))
+import Control.Monad.Except (ExceptT, runExceptT)
+import Control.Monad.Identity (Identity, runIdentity)
 import Control.Monad.State (
     MonadState,
-    State,
+    StateT,
-    evalState,
+    evalStateT,
     gets,
     modify,
  )
-import Data.List (foldl')
+import Data.Function (on)
 import Data.Map (Map)
 import Data.Map qualified as Map
 import Data.Maybe (fromMaybe)
 import Data.Tuple.Extra (dupe)
-import Debug.Trace (trace)
 import Grammar.Abs
 
 -- | Rename all variables and local binds
-rename :: Program -> Program
+rename :: Program -> Either String Program
-rename (Program bs) = Program $ evalState (runRn $ mapM (renameSc initNames) bs) 0
+rename (Program defs) = Program <$> renameDefs defs
+
+renameDefs :: [Def] -> Either String [Def]
+renameDefs defs = runIdentity $ runExceptT $ evalStateT (runRn $ mapM renameDef defs) initCxt
   where
-    -- initNames = Map.fromList $ map (\(Bind name _ _ _ _) -> dupe name) bs
+    initNames = Map.fromList [dupe name | DBind (Bind name _ _) <- defs]
-    initNames = Map.fromList $ foldl' saveIfBind [] bs
+
-    saveIfBind acc (DBind (Bind name _ _ _ _)) = dupe name : acc
+    renameDef :: Def -> Rn Def
-    saveIfBind acc _ = acc
+    renameDef = \case
-    renameSc :: Names -> Def -> Rn Def
+        DSig (Sig name typ) -> DSig . Sig name <$> renameTVars typ
-    renameSc old_names (DBind (Bind name t _ parms rhs)) = do
+        DBind (Bind name vars rhs) -> do
-        (new_names, parms') <- newNames old_names parms
+            (new_names, vars') <- newNames initNames vars
-        rhs' <- snd <$> renameExp new_names rhs
+            rhs' <- snd <$> renameExp new_names rhs
-        pure . DBind $ Bind name t name parms' rhs'
+            pure . DBind $ Bind name vars' rhs'
-    renameSc _ def = pure def
+        DData (Data (Indexed cname types) constrs) -> do
+            tvars' <- mapM nextNameTVar tvars
+            let tvars_lt = zip tvars tvars'
+                typ' = map (substituteTVar tvars_lt) types
+                constrs' = map (renameConstr tvars_lt) constrs
+            pure . DData $ Data (Indexed cname typ') constrs'
+          where
+            tvars = concatMap (collectTVars []) types
+            collectTVars tvars = \case
+                TAll tvar t -> collectTVars (tvar : tvars) t
+                TIndexed _ -> tvars
+                -- Should be monad error
+                TVar v -> [v]
+                _ -> error ("Bad data type definition: " ++ show types)
+
+    renameConstr :: [(TVar, TVar)] -> Constructor -> Constructor
+    renameConstr new_types (Constructor name typ) =
+        Constructor name $ substituteTVar new_types typ
+
+substituteTVar :: [(TVar, TVar)] -> Type -> Type
+substituteTVar new_names typ = case typ of
+    TLit _ -> typ
+    TVar tvar
+        | Just tvar' <- lookup tvar new_names ->
+            TVar tvar'
+        | otherwise ->
+            typ
+    TFun t1 t2 -> on TFun substitute' t1 t2
+    TAll tvar t
+        | Just tvar' <- lookup tvar new_names ->
+            TAll tvar' $ substitute' t
+        | otherwise ->
+            TAll tvar $ substitute' t
+    TIndexed (Indexed name typs) -> TIndexed . Indexed name $ map substitute' typs
+    _ -> error ("Impossible " ++ show typ)
+  where
+    substitute' = substituteTVar new_names
+
+initCxt :: Cxt
+initCxt = Cxt 0 0
+
+data Cxt = Cxt
+    { var_counter :: Int
+    , tvar_counter :: Int
+    }
 
 -- | Rename monad. State holds the number of renamed names.
-newtype Rn a = Rn {runRn :: State Int a}
+newtype Rn a = Rn {runRn :: StateT Cxt (ExceptT String Identity) a}
-    deriving (Functor, Applicative, Monad, MonadState Int)
+    deriving (Functor, Applicative, Monad, MonadState Cxt)
 
 -- | Maps old to new name
-type Names = Map Ident Ident
+type Names = Map LIdent LIdent
-
-renameLocalBind :: Names -> Bind -> Rn (Names, Bind)
-renameLocalBind old_names (Bind name t _ parms rhs) = do
-    (new_names, name') <- newName old_names name
-    (new_names', parms') <- newNames new_names parms
-    (new_names'', rhs') <- renameExp new_names' rhs
-    pure (new_names'', Bind name' t name' parms' rhs')
 
 renameExp :: Names -> Exp -> Rn (Names, Exp)
 renameExp old_names = \case
     EId n -> pure (old_names, EId . fromMaybe n $ Map.lookup n old_names)
-    ELit (LInt i1) -> pure (old_names, ELit (LInt i1))
+    ELit lit -> pure (old_names, ELit lit)
     EApp e1 e2 -> do
         (env1, e1') <- renameExp old_names e1
         (env2, e2') <- renameExp old_names e2
@@ -59,17 +104,21 @@ renameExp old_names = \case
         (env1, e1') <- renameExp old_names e1
         (env2, e2') <- renameExp old_names e2
         pure (Map.union env1 env2, EAdd e1' e2')
-    ELet i e1 e2 -> do
+
-        (new_names, e1') <- renameExp old_names e1
+    -- TODO fix shadowing
-        (new_names', e2') <- renameExp new_names e2
+    ELet name rhs e -> do
-        pure (new_names', ELet i e1' e2')
+        (new_names, name') <- newName old_names name
+        (new_names', rhs') <- renameExp new_names rhs
+        (new_names'', e') <- renameExp new_names' e
+        pure (new_names'', ELet name' rhs' e')
     EAbs par e -> do
         (new_names, par') <- newName old_names par
         (new_names', e') <- renameExp new_names e
         pure (new_names', EAbs par' e')
     EAnn e t -> do
         (new_names, e') <- renameExp old_names e
-        pure (new_names, EAnn e' t)
+        t' <- renameTVars t
+        pure (new_names, EAnn e' t')
     ECase e injs -> do
         (new_names, e') <- renameExp old_names e
         (new_names', injs') <- renameInjs new_names injs
@@ -88,21 +137,58 @@ renameInj ns (Inj init e) = do
 
 renameInit :: Names -> Init -> Rn (Names, Init)
 renameInit ns i = case i of
-    InitConstr cs vars -> do
+    InitConstructor cs vars -> do
         (ns_new, vars') <- newNames ns vars
-        return (ns_new, InitConstr cs vars')
+        return (ns_new, InitConstructor cs vars')
     rest -> return (ns, rest)
 
+renameTVars :: Type -> Rn Type
+renameTVars typ = case typ of
+    TAll tvar t -> do
+        tvar' <- nextNameTVar tvar
+        t' <- renameTVars $ substitute tvar tvar' t
+        pure $ TAll tvar' t'
+    TFun t1 t2 -> liftA2 TFun (renameTVars t1) (renameTVars t2)
+    _ -> pure typ
+
+substitute ::
+    TVar -> -- α
+    TVar -> -- α_n
+    Type -> -- A
+    Type -- [α_n/α]A
+substitute tvar1 tvar2 typ = case typ of
+    TLit _ -> typ
+    TVar tvar'
+        | tvar' == tvar1 -> TVar tvar2
+        | otherwise -> typ
+    TFun t1 t2 -> on TFun substitute' t1 t2
+    TAll tvar t -> TAll tvar $ substitute' t
+    TIndexed (Indexed name typs) -> TIndexed . Indexed name $ map substitute' typs
+    _ -> error "Impossible"
+  where
+    substitute' = substitute tvar1 tvar2
+
 -- | Create a new name and add it to name environment.
-newName :: Names -> Ident -> Rn (Names, Ident)
+newName :: Names -> LIdent -> Rn (Names, LIdent)
 newName env old_name = do
     new_name <- makeName old_name
     pure (Map.insert old_name new_name env, new_name)
 
 -- | Create multiple names and add them to the name environment
-newNames :: Names -> [Ident] -> Rn (Names, [Ident])
+newNames :: Names -> [LIdent] -> Rn (Names, [LIdent])
 newNames = mapAccumM newName
 
 -- | Annotate name with number and increment the number @prefix ⇒ prefix_number@.
-makeName :: Ident -> Rn Ident
+makeName :: LIdent -> Rn LIdent
-makeName (Ident prefix) = gets (\i -> Ident $ prefix ++ "_" ++ show i) <* modify succ
+makeName (LIdent prefix) = do
+    i <- gets var_counter
+    let name = LIdent $ prefix ++ "_" ++ show i
+    modify $ \cxt -> cxt{var_counter = succ cxt.var_counter}
+    pure name
+
+nextNameTVar :: TVar -> Rn TVar
+nextNameTVar (MkTVar (LIdent s)) = do
+    i <- gets tvar_counter
+    let tvar = MkTVar . LIdent $ s ++ "_" ++ show i
+    modify $ \cxt -> cxt{tvar_counter = succ cxt.tvar_counter}
+    pure tvar

src/TypeChecker/Bugs.md

@@ -1,83 +0,0 @@
-## Bugs
-
-None known at this moment
-
-main\_bug should not typecheck
-
-```hs
-apply : ('a -> 'b -> 'c) -> 'a -> 'b -> 'c ;
-apply f x = \y. f x y ;
-
-id : 'a -> 'a ;
-id x = x ;
-
-add : _Int -> _Int -> _Int ;
-add x y = x + y ;
-
-main_bug : _Int -> _Int -> _Int ;
-main_bug= (apply id) add ;
-
-idadd : _Int -> _Int -> _Int ;
-idadd = id add ;
-```
-
-main\_bug should typecheck
-
-```hs
-apply : ('a -> 'b -> 'c) -> 'a -> 'b -> 'c ;
-apply f x = \y. f x y ;
-
-id : 'a -> 'a ;
-id x = x ;
-
-add : _Int -> _Int -> _Int ;
-add x y = x + y ;
-
-main_bug : _Int -> _Int -> _Int ;
-main_bug = apply (id add) ;
-
-idadd : _Int -> _Int -> _Int ;
-idadd = id add ;
-```
-
-## Fixed bugs
-
-* 1
-
-```hs
-fmap : ('a -> 'b) -> Maybe ('a) -> Maybe ('b) ;
-fmap f x =
-    case x of {
-        Just x => Just (f x) ;
-        Nothing => Nothing
-    }
-```
-
-* 2
-
-```hs
-data Maybe ('a) where {
-    Nothing : Maybe ('a)
-    Just : 'a -> Maybe ('a)
-};
-
-id : 'a -> 'a ;
-id x = x ;
-
-main : Maybe ('a -> 'a) ; 
-main = Just id;
-```
-
-But this does
-```hs
-data Maybe ('a) where {
-    Nothing : Maybe ('a)
-    Just : 'a -> Maybe ('a)
-};
-
-id : 'b -> 'b ;
-id x = x ;
-
-main : Maybe ('a -> 'a) ; 
-main = Just id;
-```

src/TypeChecker/TypeCheckerIr.hs

@@ -2,178 +2,178 @@
 
 module TypeChecker.TypeCheckerIr where
 
-import Control.Monad.Except
+-- import Control.Monad.Except
-import Control.Monad.Reader
+-- import Control.Monad.Reader
-import Control.Monad.State
+-- import Control.Monad.State
-import Data.Functor.Identity (Identity)
+-- import Data.Functor.Identity (Identity)
-import Data.Map (Map)
+-- import Data.Map (Map)
-import Grammar.Abs (
+-- import Grammar.Abs (
-    Data (..),
+--     Data (..),
-    Ident (..),
+--     Ident (..),
-    Init (..),
+--     Init (..),
-    Literal (..),
+--     Literal (..),
-    Type (..),
+--     Type (..),
- )
+--  )
-import Grammar.Print
+-- import Grammar.Print
-import Prelude
+-- import Prelude
-import Prelude qualified as C (Eq, Ord, Read, Show)
+-- import Prelude qualified as C (Eq, Ord, Read, Show)
 
--- | A data type representing type variables
+-- -- | A data type representing type variables
-data Poly = Forall [Ident] Type
+-- data Poly = Forall [Ident] Type
-    deriving (Show)
+--     deriving (Show)
 
-newtype Ctx = Ctx {vars :: Map Ident Poly}
+-- newtype Ctx = Ctx {vars :: Map Ident Poly}
-    deriving Show
+--     deriving Show
 
-data Env = Env
+-- data Env = Env
-    { count :: Int
+--     { count :: Int
-    , sigs :: Map Ident Type
+--     , sigs :: Map Ident Type
-    , constructors :: Map Ident Type
+--     , constructors :: Map Ident Type
-    } deriving Show
+--     } deriving Show
 
-type Error = String
+-- type Error = String
-type Subst = Map Ident Type
+-- type Subst = Map Ident Type
 
-type Infer = StateT Env (ReaderT Ctx (ExceptT Error Identity))
+-- type Infer = StateT Env (ReaderT Ctx (ExceptT Error Identity))
 
-newtype Program = Program [Def]
+-- newtype Program = Program [Def]
-    deriving (C.Eq, C.Ord, C.Show, C.Read)
+--     deriving (C.Eq, C.Ord, C.Show, C.Read)
 
-data Exp
+-- data Exp
-    = EId Id
+--     = EId Id
-    | ELit Type Literal
+--     | ELit Type Literal
-    | ELet Bind Exp
+--     | ELet Bind Exp
-    | EApp Type Exp Exp
+--     | EApp Type Exp Exp
-    | EAdd Type Exp Exp
+--     | EAdd Type Exp Exp
-    | EAbs Type Id Exp
+--     | EAbs Type Id Exp
-    | ECase Type Exp [Inj]
+--     | ECase Type Exp [Inj]
-    deriving (C.Eq, C.Ord, C.Read, C.Show)
+--     deriving (C.Eq, C.Ord, C.Read, C.Show)
 
-data Inj = Inj (Init, Type) Exp
+-- data Inj = Inj (Init, Type) Exp
-    deriving (C.Eq, C.Ord, C.Read, C.Show)
+--     deriving (C.Eq, C.Ord, C.Read, C.Show)
 
-data Def = DBind Bind | DData Data
+-- data Def = DBind Bind | DData Data
-    deriving (C.Eq, C.Ord, C.Read, C.Show)
+--     deriving (C.Eq, C.Ord, C.Read, C.Show)
 
-type Id = (Ident, Type)
+-- type Id = (Ident, Type)
 
-data Bind = Bind Id Exp
+-- data Bind = Bind Id Exp
-    deriving (C.Eq, C.Ord, C.Show, C.Read)
+--     deriving (C.Eq, C.Ord, C.Show, C.Read)
 
-instance Print [Def] where
+-- instance Print [Def] where
-    prt _ [] = concatD []
+--     prt _ [] = concatD []
-    prt _ (x : xs) = concatD [prt 0 x, doc (showString "\n"), prt 0 xs]
+--     prt _ (x : xs) = concatD [prt 0 x, doc (showString "\n"), prt 0 xs]
 
-instance Print Def where
+-- instance Print Def where
-    prt i (DBind bind) = prt i bind
+--     prt i (DBind bind) = prt i bind
-    prt i (DData d) = prt i d
+--     prt i (DData d) = prt i d
 
-instance Print Program where
+-- instance Print Program where
-    prt i (Program sc) = prPrec i 0 $ prt 0 sc
+--     prt i (Program sc) = prPrec i 0 $ prt 0 sc
 
-instance Print Bind where
+-- instance Print Bind where
-    prt i (Bind (t, name) rhs) =
+--     prt i (Bind (t, name) rhs) =
-        prPrec i 0 $
+--         prPrec i 0 $
-            concatD
+--             concatD
-                [ prt 0 name
+--                 [ prt 0 name
-                , doc $ showString ":"
+--                 , doc $ showString ":"
-                , prt 0 t
+--                 , prt 0 t
-                , doc $ showString "\n"
+--                 , doc $ showString "\n"
-                , prt 0 name
+--                 , prt 0 name
-                , doc $ showString "="
+--                 , doc $ showString "="
-                , prt 0 rhs
+--                 , prt 0 rhs
-                ]
+--                 ]
 
-instance Print [Bind] where
+-- instance Print [Bind] where
-    prt _ [] = concatD []
+--     prt _ [] = concatD []
-    prt _ [x] = concatD [prt 0 x]
+--     prt _ [x] = concatD [prt 0 x]
-    prt _ (x : xs) = concatD [prt 0 x, doc (showString ";"), doc (showString "\n"), prt 0 xs]
+--     prt _ (x : xs) = concatD [prt 0 x, doc (showString ";"), doc (showString "\n"), prt 0 xs]
 
-prtIdPs :: Int -> [Id] -> Doc
+-- prtIdPs :: Int -> [Id] -> Doc
-prtIdPs i = prPrec i 0 . concatD . map (prtIdP i)
+-- prtIdPs i = prPrec i 0 . concatD . map (prtIdP i)
 
-prtId :: Int -> Id -> Doc
+-- prtId :: Int -> Id -> Doc
-prtId i (name, t) =
+-- prtId i (name, t) =
-    prPrec i 0 $
+--     prPrec i 0 $
-        concatD
+--         concatD
-            [ prt 0 name
+--             [ prt 0 name
-            , doc $ showString ":"
+--             , doc $ showString ":"
-            , prt 0 t
+--             , prt 0 t
-            ]
+--             ]
 
-prtIdP :: Int -> Id -> Doc
+-- prtIdP :: Int -> Id -> Doc
-prtIdP i (name, t) =
+-- prtIdP i (name, t) =
-    prPrec i 0 $
+--     prPrec i 0 $
-        concatD
+--         concatD
-            [ doc $ showString "("
+--             [ doc $ showString "("
-            , prt 0 name
+--             , prt 0 name
-            , doc $ showString ":"
+--             , doc $ showString ":"
-            , prt 0 t
+--             , prt 0 t
-            , doc $ showString ")"
+--             , doc $ showString ")"
-            ]
+--             ]
 
-instance Print Exp where
+-- instance Print Exp where
-    prt i = \case
+--     prt i = \case
-        EId n -> prPrec i 3 $ concatD [prtId 0 n, doc $ showString "\n"]
+--         EId n -> prPrec i 3 $ concatD [prtId 0 n, doc $ showString "\n"]
-        ELit _ (LInt i1) -> prPrec i 3 $ concatD [prt 0 i1, doc $ showString "\n"]
+--         ELit _ (LInt i1) -> prPrec i 3 $ concatD [prt 0 i1, doc $ showString "\n"]
-        ELet bs e ->
+--         ELet bs e ->
-            prPrec i 3 $
+--             prPrec i 3 $
-                concatD
+--                 concatD
-                    [ doc $ showString "let"
+--                     [ doc $ showString "let"
-                    , prt 0 bs
+--                     , prt 0 bs
-                    , doc $ showString "in"
+--                     , doc $ showString "in"
-                    , prt 0 e
+--                     , prt 0 e
-                    , doc $ showString "\n"
+--                     , doc $ showString "\n"
-                    ]
+--                     ]
-        EApp _ e1 e2 ->
+--         EApp _ e1 e2 ->
-            prPrec i 2 $
+--             prPrec i 2 $
-                concatD
+--                 concatD
-                    [ prt 2 e1
+--                     [ prt 2 e1
-                    , prt 3 e2
+--                     , prt 3 e2
-                    ]
+--                     ]
-        EAdd t e1 e2 ->
+--         EAdd t e1 e2 ->
-            prPrec i 1 $
+--             prPrec i 1 $
-                concatD
+--                 concatD
-                    [ doc $ showString "@"
+--                     [ doc $ showString "@"
-                    , prt 0 t
+--                     , prt 0 t
-                    , prt 1 e1
+--                     , prt 1 e1
-                    , doc $ showString "+"
+--                     , doc $ showString "+"
-                    , prt 2 e2
+--                     , prt 2 e2
-                    , doc $ showString "\n"
+--                     , doc $ showString "\n"
-                    ]
+--                     ]
-        EAbs t n e ->
+--         EAbs t n e ->
-            prPrec i 0 $
+--             prPrec i 0 $
-                concatD
+--                 concatD
-                    [ doc $ showString "@"
+--                     [ doc $ showString "@"
-                    , prt 0 t
+--                     , prt 0 t
-                    , doc $ showString "\\"
+--                     , doc $ showString "\\"
-                    , prtId 0 n
+--                     , prtId 0 n
-                    , doc $ showString "."
+--                     , doc $ showString "."
-                    , prt 0 e
+--                     , prt 0 e
-                    , doc $ showString "\n"
+--                     , doc $ showString "\n"
-                    ]
+--                     ]
-        ECase t exp injs ->
+--         ECase t exp injs ->
-            prPrec
+--             prPrec
-                i
+--                 i
-                0
+--                 0
-                ( concatD
+--                 ( concatD
-                    [ doc (showString "case")
+--                     [ doc (showString "case")
-                    , prt 0 exp
+--                     , prt 0 exp
-                    , doc (showString "of")
+--                     , doc (showString "of")
-                    , doc (showString "{")
+--                     , doc (showString "{")
-                    , prt 0 injs
+--                     , prt 0 injs
-                    , doc (showString "}")
+--                     , doc (showString "}")
-                    , doc (showString ":")
+--                     , doc (showString ":")
-                    , prt 0 t
+--                     , prt 0 t
-                    , doc $ showString "\n"
+--                     , doc $ showString "\n"
-                    ]
+--                     ]
-                )
+--                 )
 
-instance Print Inj where
+-- instance Print Inj where
-    prt i = \case
+--     prt i = \case
-        Inj (init, t) exp -> prPrec i 0 (concatD [prt 0 init, doc (showString ":"), prt 0 t, doc (showString "=>"), prt 0 exp])
+--         Inj (init, t) exp -> prPrec i 0 (concatD [prt 0 init, doc (showString ":"), prt 0 t, doc (showString "=>"), prt 0 exp])
 
-instance Print [Inj] where
+-- instance Print [Inj] where
-    prt _ [] = concatD []
+--     prt _ [] = concatD []
-    prt _ [x] = concatD [prt 0 x]
+--     prt _ [x] = concatD [prt 0 x]
-    prt _ (x : xs) = concatD [prt 0 x, doc (showString ";"), prt 0 xs]
+--     prt _ (x : xs) = concatD [prt 0 x, doc (showString ";"), prt 0 xs]

test_program

@@ -1,24 +1,4 @@
-data Maybe ('a) where {
+data Maybe (a) where {
-    Nothing : Maybe ('a)
+    Nothing : Maybe (a)
-    Just : 'a -> Maybe ('a)
+    Just : a -> Maybe (a)
-};
+}
-
-fromJust : Maybe ('a) -> 'a ;
-fromJust a =
-    case a of {
-        Just a => a
-    };
-
-fromMaybe : 'a -> Maybe ('a) -> 'a ;
-fromMaybe a b =
-    case b of {
-        Just a => a;
-        Nothing => a
-    };
-
-maybe : 'b -> ('a -> 'b) -> Maybe ('a) -> 'b;
-maybe b f ma =
-    case ma of {
-        Just a => f a;
-        Nothing => b
-    }