refactoring

10 files changed, 111 insertions, 120 deletions

diff --git a/src/LambdaCube/Compiler/CoreToIR.hs b/src/LambdaCube/Compiler/CoreToIR.hs
index 0c8b8006..7e4a938e 100644
--- a/src/LambdaCube/Compiler/CoreToIR.hs
+++ b/src/LambdaCube/Compiler/CoreToIR.hs
@@ -576,7 +576,7 @@ genGLSLs backend
     reds x = error $ "red: " ++ ppShow x
     genGLSL' err vertOuts (ps, o)
         | length ps == length vertOuts = genGLSL (reverse vertOuts) o
-        | otherwise = error $ "makeSubst illegal input " ++ err ++ "  " ++ show ps ++ "\n" ++ show vertOuts
+        | otherwise = error $ "makeSubst illegal input " ++ err ++ "  " ++ ppShow ps ++ "\n" ++ ppShow vertOuts
 
     noUnit TTuple0 = False
     noUnit _ = True
@@ -623,7 +623,6 @@ data Uniform
     = UUniform
     | UTexture2DSlot
     | UTexture2D Integer Integer ExpTV
-    deriving (Show)
 
 type Uniforms = Map String (Uniform, IR.InputType)
 
@@ -638,7 +637,7 @@ simpleExpr = \case
 genGLSL :: [SName] -> ExpTV -> WriterT (Uniforms, Map.Map SName (ExpTV, ExpTV, [ExpTV])) (State [String]) Doc
 genGLSL dns e = case e of
 
-  ELit a -> pure $ text $ show a
+  ELit a -> pure $ pShow a
   Var i _ -> pure $ text $ dns !! i
 
   Func fn def ty xs | not (simpleExpr def) -> tell (mempty, Map.singleton fn (def, ty, map tyOf xs)) >> call fn xs
@@ -822,7 +821,7 @@ genGLSL dns e = case e of
 
 -- expression + type + type of local variables
 data ExpTV = ExpTV_ Exp Exp [Exp]
-  deriving (Show, Eq)
+  deriving (Eq)
 
 pattern ExpTV a b c <- ExpTV_ a b c where ExpTV a b c = ExpTV_ (a) (unLab' b) c
 
@@ -888,7 +887,7 @@ chain vs t xs = map snd $ chain' vs t xs
 
 chain' vs t [] = []
 chain' vs t@(I.Pi b at y) (a: as) = (b, ExpTV a at vs): chain' vs (appTy t a) as
-chain' vs t _ = error $ "chain: " ++ show t
+chain' vs t _ = error $ "chain: " ++ ppShow t
 
 mkTVar i (ExpTV t _ vs) = ExpTV (I.Var i) t vs
 
@@ -1001,7 +1000,7 @@ getTuple _ = Nothing
 genHLSL :: [SName] -> ExpTV -> WriterT (Uniforms, Map.Map SName (ExpTV, ExpTV, [ExpTV])) (State [String]) Doc
 genHLSL dns e = case e of
 
-  ELit a -> pure $ text $ show a
+  ELit a -> pure $ pShow a
   Var i _ -> pure $ text $ dns !! i
 
   Func fn def ty xs | not (simpleExpr def) -> tell (mempty, Map.singleton fn (def, ty, map tyOf xs)) >> call fn xs
@@ -1288,7 +1287,7 @@ genHLSLs backend
     reds x = error $ "red: " ++ ppShow x
     genHLSL' err vertOuts (ps, o)
         | length ps == length vertOuts = genHLSL (reverse vertOuts) o
-        | otherwise = error $ "makeSubst illegal input " ++ err ++ "  " ++ show ps ++ "\n" ++ show vertOuts
+        | otherwise = error $ "makeSubst illegal input " ++ err ++ "  " ++ ppShow ps ++ "\n" ++ ppShow vertOuts
 
     noUnit TTuple0 = False
     noUnit _ = True
diff --git a/src/LambdaCube/Compiler/DeBruijn.hs b/src/LambdaCube/Compiler/DeBruijn.hs
index 4cf286fc..c0fce31e 100644
--- a/src/LambdaCube/Compiler/DeBruijn.hs
+++ b/src/LambdaCube/Compiler/DeBruijn.hs
@@ -46,13 +46,14 @@ instance Rearrange Void where
 
 -------------------------------------------------------------------------------- fold De Bruijn indices
 
-class Up a where
+class Up{-TODO: rename-} a where
 
     foldVar :: Monoid e => (Int{-level-} -> Int{-index-} -> e) -> Int -> a -> e
 
     usedVar :: Int -> a -> Bool
     usedVar = (getAny .) . foldVar ((Any .) . (==))
 
+    -- TODO: remove
     closedExp :: a -> a
     closedExp a = a
 
diff --git a/src/LambdaCube/Compiler/DesugaredSource.hs b/src/LambdaCube/Compiler/DesugaredSource.hs
index b3880a3d..4c52d5f1 100644
--- a/src/LambdaCube/Compiler/DesugaredSource.hs
+++ b/src/LambdaCube/Compiler/DesugaredSource.hs
@@ -24,7 +24,7 @@ import qualified Data.Set as Set
 import qualified Data.IntMap as IM
 import Control.Arrow hiding ((<+>))
 import Control.DeepSeq
-import Debug.Trace
+--import Debug.Trace
 
 import LambdaCube.Compiler.Utils
 import LambdaCube.Compiler.DeBruijn
@@ -92,7 +92,6 @@ data Range = Range !FileInfo !SPos !SPos
 instance NFData Range where
     rnf Range{} = ()
 
--- short version
 instance PShow Range
   where
     pShow (Range n b@(SPos r c) e@(SPos r' c')) = expand (pShow n <+> pShow b <> "-" <> pShow e)
@@ -100,8 +99,6 @@ instance PShow Range
              : map text (drop (r - 1) $ take r' $ lines $ fileContent n)
             ++ [text $ replicate (c - 1) ' ' ++ replicate (c' - c) '^' | r' == r]
 
-instance Show Range where show = ppShow
-
 joinRange :: Range -> Range -> Range
 joinRange (Range n b e) (Range n' b' e') {- | n == n' -} = Range n (min b b') (max e e')
 
@@ -142,7 +139,9 @@ debugSI a = NoSI (Set.singleton a)
 si@(RangeSI r) `validate` xs | r `notElem` [r | RangeSI r <- xs]  = si
 _ `validate` _ = mempty
 
-data SIName = SIName_ SI (Maybe Fixity) SName
+-------------------------------------------------------------------------------- name with source info
+
+data SIName = SIName_ { siName :: SI, getFixity :: Maybe Fixity, sName :: SName }
 
 pattern SIName si n <- SIName_ si _ n
   where SIName si n =  SIName_ si Nothing n
@@ -156,13 +155,6 @@ instance PShow SIName
         NoSI{} -> text n
         _ -> pShow si
 
-sName (SIName _ s) = s
-
---appName f (SIName si n) = SIName si $ f n
-
-getFixity_ (SIName_ _ f _) = f
---getFixity (SIName_ _ f _) = fromMaybe (InfixL 9) f
-
 -------------
 
 class SourceInfo a where
@@ -192,12 +184,12 @@ data Lit
     | LString String
   deriving (Eq)
 
-instance Show Lit where
-    show = \case
-        LFloat x  -> show x
-        LString x -> show x
-        LInt x    -> show x
-        LChar x   -> show x
+instance PShow Lit where
+    pShow = \case
+        LFloat x  -> pShow x
+        LString x -> text $ show x
+        LInt x    -> pShow x
+        LChar x   -> pShow x
 
 -------------------------------------------------------------------------------- expression
 
@@ -209,7 +201,7 @@ data SExp' a
     | SVar_   (SData SIName) !Int
     | SLet_   SI (SData SIName) (SExp' a) (SExp' a)    -- let x = e in f   -->  SLet e f{-x is Var 0-}
     | STyped  a
-  deriving (Eq, Show)
+  deriving (Eq)
 
 type SExp = SExp' Void
 
@@ -385,25 +377,22 @@ trSExp f = g where
 trSExp' :: SExp -> SExp' a
 trSExp' = trSExp elimVoid
 
-instance Up a => PShow (SExp' a) where
-    pShow = sExpDoc
-
-sExpDoc :: Up a => SExp' a -> Doc
-sExpDoc = \case
-    SGlobal ns      -> text $ sName ns
-    SAnn a b        -> shAnn False (sExpDoc a) (sExpDoc b)
-    TyType a        -> shApp Visible (text "tyType") (sExpDoc a)
-    SGlobal op `SAppV` a `SAppV` b | Just p <- getFixity_ op -> DOp (sName op) p (pShow a) (pShow b)
-    SApp h a b      -> shApp h (sExpDoc a) (sExpDoc b)
-    Wildcard t      -> shAnn True (text "_") (sExpDoc t)
-    SBind_ _ h _ a b -> shLam (usedVar 0 b) h (sExpDoc a) (sExpDoc b)
-    SLet _ a b      -> shLet_ (sExpDoc a) (sExpDoc b)
-    STyped _{-(e,t)-}  -> text "<<>>" -- todo: expDoc e
-    SVar _ i        -> shVar i
-    SLit _ l        -> text $ show l
+instance (Up a, PShow a) => PShow (SExp' a) where
+    pShow = \case
+        SGlobal ns      -> pShow ns
+        SAnn a b        -> shAnn False (pShow a) (pShow b)
+        TyType a        -> text "tyType" `DApp` pShow a
+        SGlobal op `SAppV` a `SAppV` b | Just p <- getFixity op -> DOp (sName op) p (pShow a) (pShow b)
+        SApp h a b      -> shApp h (pShow a) (pShow b)
+        Wildcard t      -> shAnn True (text "_") (pShow t)
+        SBind_ _ h _ a b -> shLam (usedVar 0 b) h (pShow a) (pShow b)
+        SLet _ a b      -> shLet_ (pShow a) (pShow b)
+        STyped a        -> pShow a
+        SVar _ i        -> shVar i
+        SLit _ l        -> pShow l
 
 shApp Visible a b = DApp a b
-shApp Hidden a b = DApp a (DGlue (InfixR 20) "@" b)
+shApp Hidden a b = DApp a (DAt b)
 
 shLam True (BPi Hidden) a b = DFreshName True $ showForall (shAnn True (DVar 0) $ DUp 0 a) b
 shLam False (BPi Hidden) a b = showContext a $ DFreshName False b
@@ -418,7 +407,7 @@ shLam usedVar h a b = DFreshName usedVar $ lam (p $ DUp 0 a) b
         BLam h -> vpar h
         BPi h -> vpar h
 
-    vpar Hidden = (\p -> DBrace p) . shAnn True (green $ DVar 0)
+    vpar Hidden = DAt . ann (green $ DVar 0)
     vpar Visible = ann (green $ DVar 0)
 
     ann | usedVar = shAnn False
@@ -432,7 +421,6 @@ data Stmt
     = Let SIName (Maybe SExp) SExp
     | Data SIName [(Visibility, SExp)]{-parameters-} SExp{-type-} [(SIName, SExp)]{-constructor names and types-}
     | PrecDef SIName Fixity
-    deriving (Show)
 
 pattern Primitive n t = Let n (Just t) (SBuiltin "undefined")
 
@@ -445,7 +433,7 @@ instance PShow Stmt where
 instance DeBruijnify SIName Stmt where
     deBruijnify_ k v = \case
         Let sn mt e -> Let sn (deBruijnify_ k v <$> mt) (deBruijnify_ k v e)
-        x -> error $ "deBruijnify @ " ++ show x
+        x -> error $ "deBruijnify @ " ++ ppShow x
 
 -------------------------------------------------------------------------------- statement with dependencies
 
diff --git a/src/LambdaCube/Compiler/Infer.hs b/src/LambdaCube/Compiler/Infer.hs
index ef490fc7..ad7eeae6 100644
--- a/src/LambdaCube/Compiler/Infer.hs
+++ b/src/LambdaCube/Compiler/Infer.hs
@@ -61,7 +61,6 @@ data Exp
     | Pi_  !MaxDB Visibility Exp Exp
     | Lam_ !MaxDB Exp
     | Neut Neutral
-  deriving (Show)
 
 data Freq = CompileTime | RunTime
   deriving (Eq, Show)
@@ -78,7 +77,6 @@ data Neutral
     | Var_ !Int                 -- De Bruijn variable
     | LabelEnd_ Exp                 -- not neut?
     | Delta (SData ([Exp] -> Exp))  -- not neut?
-  deriving (Show)
 
 data ConName = ConName FName Int{-ordinal number, e.g. Zero:0, Succ:1-} Type
 
@@ -95,14 +93,19 @@ type ExpType = (Exp, Type)
 type SExp2 = SExp' ExpType
 
 instance Show ConName where show (ConName n _ _) = show n
+instance PShow ConName where pShow (ConName n _ _) = pShow n
 instance Eq ConName where ConName _ n _ == ConName _ n' _ = n == n'
 instance Show TyConName where show (TyConName n _ _ _ _) = show n
+instance PShow TyConName where pShow (TyConName n _ _ _ _) = pShow n
 instance Eq TyConName where TyConName n _ _ _ _ == TyConName n' _ _ _ _ = n == n'
 instance Show FunName where show (FunName n _ _) = show n
+instance PShow FunName where pShow (FunName n _ _) = pShow n
 instance Eq FunName where FunName n _ _ == FunName n' _ _ = n == n'
 instance Show CaseFunName where show (CaseFunName n _ _) = CaseName $ show n
+instance PShow CaseFunName where pShow (CaseFunName n _ _) = text $ CaseName $ ppShow n
 instance Eq CaseFunName where CaseFunName n _ _ == CaseFunName n' _ _ = n == n'
 instance Show TyCaseFunName where show (TyCaseFunName n _) = MatchName $ show n
+instance PShow TyCaseFunName where pShow (TyCaseFunName n _) = text $ MatchName $ ppShow n
 instance Eq TyCaseFunName where TyCaseFunName n _ == TyCaseFunName n' _ = n == n'
 
 data FName
@@ -195,7 +198,10 @@ fntable =
 
 instance Show FName where
   show (CFName _ (SData s)) = s
-  show s = fromMaybe (error "show") $ lookup s $ map (\(a, b) -> (b, a)) fntable
+  show s = maybe (error "show") id $ lookup s $ map (\(a, b) -> (b, a)) fntable
+instance PShow FName where
+  pShow (CFName _ (SData s)) = text s
+  pShow s = maybe (error "show") text $ lookup s $ map (\(a, b) -> (b, a)) fntable
 
 -------------------------------------------------------------------------------- auxiliary functions and patterns
 
@@ -328,7 +334,7 @@ pattern LabelEnd x = Neut (LabelEnd_ x)
 --pmLabel' :: FunName -> [Exp] -> Int -> [Exp] -> Exp -> Exp
 pmLabel' _ (FunName _ _ _) _ 0 as (Neut (Delta (SData f))) = f $ reverse as
 pmLabel' md f vs i xs (unfixlabel -> Neut y) = Neut $ Fun_ md f vs i xs y
-pmLabel' _ f _ i xs y = error $ "pmLabel: " ++ show (f, i, length xs, y)
+pmLabel' _ f _ i xs y = error $ "pmLabel: " ++ ppShow f --show (f, i, length xs, y)
 
 pmLabel :: FunName -> [Exp] -> Int -> [Exp] -> Exp -> Exp
 pmLabel f vs i xs e = pmLabel' (foldMap maxDB_ vs <> foldMap maxDB_ xs) f vs (i + numLams e) xs (Neut $ dropLams e)
@@ -536,11 +542,11 @@ evalCaseFun a ps (Con n@(ConName _ i _) _ vs)
     | i /= (-1) = foldl app_ (ps !!! (i + 1)) vs
     | otherwise = error "evcf"
   where
-    xs !!! i | i >= length xs = error $ "!!! " ++ show a ++ " " ++ show i ++ " " ++ show n ++ "\n" ++ ppShow ps
+    xs !!! i | i >= length xs = error $ "!!! " ++ ppShow a ++ " " ++ show i ++ " " ++ ppShow n ++ "\n" ++ ppShow ps
     xs !!! i = xs !! i
 evalCaseFun a b (FL c) = evalCaseFun a b c
 evalCaseFun a b (Neut c) = CaseFun a b c
-evalCaseFun a b x = error $ "evalCaseFun: " ++ show (a, x)
+evalCaseFun a b x = error $ "evalCaseFun: " ++ ppShow (a, x)
 
 evalTyCaseFun a b (FL c) = evalTyCaseFun a b c
 evalTyCaseFun a b (Neut c) = TyCaseFun a b c
@@ -705,7 +711,7 @@ data CEnv a
     = MEnd a
     | Meta Exp (CEnv a)
     | Assign !Int ExpType (CEnv a)       -- De Bruijn index decreasing assign reservedOp, only for metavariables (non-recursive)
-  deriving (Show, Functor)
+  deriving (Functor)
 
 instance (Subst Exp a, Up a) => Up (CEnv a) where
     usedVar i a = error "usedVar @(CEnv _)"
@@ -822,7 +828,6 @@ data Env
     | CheckIType SExp2 Env
 --    | CheckSame Exp Env
     | CheckAppType SI Visibility Type Env SExp2   --pattern CheckAppType _ h t te b = EApp1 _ h (CheckType t te) b
-  deriving Show
 
 pattern EBind2 b e env <- EBind2_ _ b e env where EBind2 b e env = EBind2_ (debugSI "6") b e env
 pattern CheckType e env <- CheckType_ _ e env where CheckType e env = CheckType_ (debugSI "7") e env
@@ -877,7 +882,7 @@ mkExpTypes t [] = []
 mkExpTypes t@(Pi _ a _) (x: xs) = (x, t): mkExpTypes (appTy t x) xs
 
 appTy (Pi _ a b) x = subst 0 x b
-appTy t x = error $ "appTy: " ++ show t
+appTy t x = error $ "appTy: " ++ ppShow t
 
 -------------------------------------------------------------------------------- error messages
 
@@ -981,7 +986,7 @@ inferN_ tellTrace = infer  where
         | SLam h a b <- e, Pi h' x y <- t, h == h'  = do
             tellType e t
             let same = checkSame te a x
-            if same then checkN (EBind2 (BLam h) x te) b y else error $ "checkSame:\n" ++ show a ++ "\nwith\n" ++ showEnvExp te (x, TType)
+            if same then checkN (EBind2 (BLam h) x te) b y else error $ "checkSame:\n" ++ ppShow a ++ "\nwith\n" ++ showEnvExp te (x, TType)
         | Pi Hidden a b <- t = do
             bb <- notHiddenLam e
             if bb then checkN (EBind2 (BLam Hidden) a te) (up1 e) b
@@ -1008,7 +1013,7 @@ inferN_ tellTrace = infer  where
     checkSame te (SGlobal (sName -> "'Type")) TType = True
     checkSame te SType TType = True
     checkSame te (SBind_ _ BMeta _ SType (STyped (Var 0, _))) a = True
-    checkSame te a b = error $ "checkSame: " ++ show (a, b)
+    checkSame te a b = error $ "checkSame: " ++ ppShow (a, b)
 
     hArgs (Pi Hidden _ b) = 1 + hArgs b
     hArgs _ = 0
@@ -1177,10 +1182,10 @@ recheck' msg' e (x, xt) = (recheck_ "main" (checkEnv e) (x, xt), xt)
         (Neut (App__ md a b), zt)
             | (Neut a', at) <- recheck'' "app1" te (Neut a, neutType te a)
             -> checkApps "a" [] zt (Neut . App__ md a' . head) te at [b]
-        (Con_ md s n as, zt)      -> checkApps (show s) [] zt (Con_ md s n . drop (conParams s)) te (conType zt s) $ mkConPars n zt ++ as
-        (TyCon_ md s as, zt)      -> checkApps (show s) [] zt (TyCon_ md s) te (nType s) as
-        (CaseFun s@(CaseFunName _ t pars) as n, zt) -> checkApps (show s) [] zt (\xs -> evalCaseFun s (init $ drop pars xs) (last xs)) te (nType s) (makeCaseFunPars te n ++ as ++ [Neut n])
-        (TyCaseFun s [m, t, f] n, zt)  -> checkApps (show s) [] zt (\[m, t, n, f] -> evalTyCaseFun s [m, t, f] n) te (nType s) [m, t, Neut n, f]
+        (Con_ md s n as, zt)      -> checkApps (ppShow s) [] zt (Con_ md s n . drop (conParams s)) te (conType zt s) $ mkConPars n zt ++ as
+        (TyCon_ md s as, zt)      -> checkApps (ppShow s) [] zt (TyCon_ md s) te (nType s) as
+        (CaseFun s@(CaseFunName _ t pars) as n, zt) -> checkApps (ppShow s) [] zt (\xs -> evalCaseFun s (init $ drop pars xs) (last xs)) te (nType s) (makeCaseFunPars te n ++ as ++ [Neut n])
+        (TyCaseFun s [m, t, f] n, zt)  -> checkApps (ppShow s) [] zt (\[m, t, n, f] -> evalTyCaseFun s [m, t, f] n) te (nType s) [m, t, Neut n, f]
         (Neut (Fun_ md f vs@[] i a x), zt) -> checkApps "lab" [] zt (\xs -> Neut $ Fun_ md f vs i (reverse xs) x) te (nType f) $ reverse a   -- TODO: recheck x
         -- TODO
         (r@(Neut (Fun' f vs i a x)), zt) -> r
@@ -1200,7 +1205,7 @@ recheck' msg' e (x, xt) = (recheck_ "main" (checkEnv e) (x, xt), xt)
 ambiguityCheck :: String -> Exp -> Maybe String
 ambiguityCheck s ty = case ambigVars ty of
     [] -> Nothing
-    err -> Just $ s ++ " has ambiguous type:\n" ++ ppShow ty ++ "\nproblematic vars:\n" ++ show err
+    err -> Just $ s ++ " has ambiguous type:\n" ++ ppShow ty ++ "\nproblematic vars:\n" ++ ppShow err
 
 ambigVars :: Exp -> [(Int, Exp)]
 ambigVars ty = [(n, c) | (n, c) <- hid, not $ any (`Set.member` defined) $ Set.insert n $ free c]
@@ -1383,7 +1388,7 @@ handleStmt = \case
     e3 <- addToEnv (SIName (sourceInfo s) $ MatchName (sName s)) (lamify t $ \[m, tr, n, f] -> evalTyCaseFun (TyCaseFunName sint t) [m, tr, f] n, t)
     return (e1 <> e2 <> e3 <> es)
 
-  stmt -> error $ "handleStmt: " ++ show stmt
+  stmt -> error $ "handleStmt: " ++ ppShow stmt
 
 withEnv e = local $ second (<> e)
 
@@ -1464,21 +1469,21 @@ instance PShow Env where
 showEnvExp :: Env -> ExpType -> String
 showEnvExp e c = show $ envDoc e $ underline $ mkDoc False False c
 
-showEnvSExp :: Up a => Env -> SExp' a -> String
-showEnvSExp e c = show $ envDoc e $ underline $ sExpDoc c
+showEnvSExp :: (PShow a, Up a) => Env -> SExp' a -> String
+showEnvSExp e c = show $ envDoc e $ underline $ pShow c
 
-showEnvSExpType :: Up a => Env -> SExp' a -> Exp -> String
-showEnvSExpType e c t = show $ envDoc e $ underline $ (shAnn False (sExpDoc c) (mkDoc False False (t, TType)))
+showEnvSExpType :: (PShow a, Up a) => Env -> SExp' a -> Exp -> String
+showEnvSExpType e c t = show $ envDoc e $ underline $ (shAnn False (pShow c) (mkDoc False False (t, TType)))
 
 envDoc :: Env -> Doc -> Doc
 envDoc x m = case x of
     EGlobal{}           -> m
-    EBind1 _ h ts b     -> envDoc ts $ shLam (usedVar 0 b) h m (sExpDoc b)
+    EBind1 _ h ts b     -> envDoc ts $ shLam (usedVar 0 b) h m (pShow b)
     EBind2 h a ts       -> envDoc ts $ shLam True h (mkDoc False ts' (a, TType)) m
-    EApp1 _ h ts b      -> envDoc ts $ shApp h m (sExpDoc b)
+    EApp1 _ h ts b      -> envDoc ts $ shApp h m (pShow b)
     EApp2 _ h (Lam (Var 0), Pi Visible TType _) ts -> envDoc ts $ shApp h (text "tyType") m
     EApp2 _ h a ts      -> envDoc ts $ shApp h (mkDoc False ts' a) m
-    ELet1 _ ts b        -> envDoc ts $ shLet_ m (sExpDoc b)
+    ELet1 _ ts b        -> envDoc ts $ shLet_ m (pShow b)
     ELet2 _ x ts        -> envDoc ts $ shLet_ (mkDoc False ts' x) m
     EAssign i x ts      -> envDoc ts $ shLet i (mkDoc False ts' x) m
     CheckType t ts      -> envDoc ts $ shAnn False m $ mkDoc False ts' (t, TType)
@@ -1486,7 +1491,7 @@ envDoc x m = case x of
 --    CheckSame t ts      -> envDoc ts $ shCstr <$> m <*> mkDoc ts' t
     CheckAppType si h t te b -> envDoc (EApp1 si h (CheckType_ (sourceInfo b) t te) b) m
     ELabelEnd ts        -> envDoc ts $ shApp Visible (text "labEnd") m
-    x   -> error $ "envDoc: " ++ show x
+    x   -> error $ "envDoc: " ++ ppShow x
   where
     ts' = False
 
@@ -1503,13 +1508,13 @@ instance MkDoc Exp where
 --            Lam h a b       -> join $ shLam (usedVar 0 b) (BLam h) <$> f a <*> pure (f b)
             Lam b           -> shLam True (BLam Visible) (f TType{-todo!-}) (f b)
             Pi h a b        -> shLam (usedVar 0 b) (BPi h) (f a) (f b)
-            ENat' n         -> text $ show n
+            ENat' n         -> text $ ppShow n
             (getTTup -> Just xs) -> shTuple $ f <$> xs
             (getTup -> Just xs)  -> shTuple $ f <$> xs
-            Con s _ xs      -> foldl (shApp Visible) (text_ $ show s) (f <$> xs)
-            TyConN s xs     -> foldl (shApp Visible) (text_ $ show s) (f <$> xs)
+            Con s _ xs      -> foldl (shApp Visible) (text_ $ ppShow s) (f <$> xs)
+            TyConN s xs     -> foldl (shApp Visible) (text_ $ ppShow s) (f <$> xs)
             TType           -> text "Type"
-            ELit l          -> text $ show l
+            ELit l          -> pShow l
             Neut x          -> mkDoc pr ts x
 
         text_ = text . if ts then switchTick else id
@@ -1521,11 +1526,11 @@ instance MkDoc Neutral where
         f = \case
             CstrT' t a b     -> shCstr (g (a, t)) (g (b, t))
             FL' a | pr -> g a
-            Fun' s vs i (mkExpTypes (nType s) . reverse -> xs) _ -> foldl (shApp Visible) (text_ $ show s) (g <$> xs)
+            Fun' s vs i (mkExpTypes (nType s) . reverse -> xs) _ -> foldl (shApp Visible) (text_ $ ppShow s) (g <$> xs)
             Var_ k           -> shVar k
             App_ a b         -> shApp Visible (g a) (g b)
-            CaseFun_ s xs n  -> foldl (shApp Visible) (text_ $ show s) (map g $ {-mkExpTypes (nType s) $ makeCaseFunPars te n ++ -} xs ++ [Neut n])
-            TyCaseFun_ s [m, t, f] n  -> foldl (shApp Visible) (text_ $ show s) (g <$> mkExpTypes (nType s) [m, t, Neut n, f])
+            CaseFun_ s xs n  -> foldl (shApp Visible) (text_ $ ppShow s) (map g $ {-mkExpTypes (nType s) $ makeCaseFunPars te n ++ -} xs ++ [Neut n])
+            TyCaseFun_ s [m, t, f] n  -> foldl (shApp Visible) (text_ $ ppShow s) (g <$> mkExpTypes (nType s) [m, t, Neut n, f])
             TyCaseFun_ s _ n -> error $ "mkDoc TyCaseFun"
             LabelEnd_ x      -> shApp Visible (text "labend") (g x)
             Delta{}          -> text "^delta"
diff --git a/src/LambdaCube/Compiler/Lexer.hs b/src/LambdaCube/Compiler/Lexer.hs
index fcbd356d..46c44086 100644
--- a/src/LambdaCube/Compiler/Lexer.hs
+++ b/src/LambdaCube/Compiler/Lexer.hs
@@ -22,7 +22,6 @@ import Control.Applicative
 
 import Text.Megaparsec hiding (State)
 import qualified Text.Megaparsec as P
-import qualified Text.Megaparsec.Prim as P
 import Text.Megaparsec as ParseUtils hiding (try, Message, State)
 import Text.Megaparsec.Lexer hiding (lexeme, symbol, negate)
 
@@ -35,22 +34,6 @@ import LambdaCube.Compiler.DesugaredSource
 -- see http://blog.ezyang.com/2014/05/parsec-try-a-or-b-considered-harmful/comment-page-1/#comment-6602
 try_ s m = try m <?> s
 
-instance (Monoid w, P.MonadParsec st m t) => P.MonadParsec st (RWST r w s m) t where
-  failure                    = lift . failure
-  label n       (RWST m) = RWST $ \r s -> label n $ m r s
-  try           (RWST m) = RWST $ \r s -> try $ m r s
-  lookAhead     (RWST m) = RWST $ \r s ->
-    (\(a, _, _) -> (a, s, mempty)) <$> lookAhead (m r s)
-  notFollowedBy (RWST m) = RWST $ \r s ->
-    notFollowedBy ((\(a, _, _) -> a) <$> m r s) >> return ((), s, mempty)
-  withRecovery rec (RWST m) = RWST $ \r s ->
-    withRecovery (\e -> runRWST (rec e) r s) (m r s)
-  eof                        = lift eof
-  token  f e                 = lift $ token  f e
-  tokens f e ts              = lift $ tokens f e ts
-  getParserState             = lift getParserState
-  updateParserState f        = lift $ updateParserState f
-
 toSPos :: SourcePos -> SPos
 toSPos p = SPos (sourceLine p) (sourceColumn p)
 
diff --git a/src/LambdaCube/Compiler/Parser.hs b/src/LambdaCube/Compiler/Parser.hs
index bc2cbbd4..633368f8 100644
--- a/src/LambdaCube/Compiler/Parser.hs
+++ b/src/LambdaCube/Compiler/Parser.hs
@@ -71,7 +71,7 @@ instance PShow LCParseError where
     pShow = \case
         MultiplePatternVars xs -> vcat $ "multiple pattern vars:":
             concat [(shortForm (pShow $ head ns) <+> "is defined at"): map pShow ns | ns <- xs]
-        OperatorMismatch op op' -> "Operator precedences don't match:" <$$> pShow (fromJust $ getFixity_ op) <+> "at" <+> pShow op <$$> pShow (fromJust $ getFixity_ op') <+> "at" <+> pShow op'
+        OperatorMismatch op op' -> "Operator precedences don't match:" <$$> pShow (fromJust $ getFixity op) <+> "at" <+> pShow op <$$> pShow (fromJust $ getFixity op') <+> "at" <+> pShow op'
         UndefinedConstructor n -> "Constructor" <+> shortForm (pShow n) <+> "is not defined at" <+> pShow n
         ParseError p -> text $ show p
 
@@ -275,7 +275,7 @@ calculatePrecs = go where
     waitOp lsec e acc []            = calcPrec' e acc
     waitOp lsec e acc _             = error "impossible @ Parser 488"
 
-    calcPrec' e = postponedCheck id . calcPrec (\op x y -> SGlobal op `SAppV` x `SAppV` y) (fromJust . getFixity_) e . reverse
+    calcPrec' e = postponedCheck id . calcPrec (\op x y -> SGlobal op `SAppV` x `SAppV` y) (fromJust . getFixity) e . reverse
 
 generator, letdecl, boolExpression :: BodyParser (SExp -> ErrorFinder SExp)
 generator = do
@@ -354,7 +354,7 @@ mkTup ps = foldr cHCons cHNil ps
 patType p (Wildcard SType) = p
 patType p t = PatTypeSimp p t
 
-calculatePatPrecs e xs = postponedCheck fst $ calcPrec (\op x y -> PConSimp op [x, y]) (fromJust . getFixity_ . fst) e xs
+calculatePatPrecs e xs = postponedCheck fst $ calcPrec (\op x y -> PConSimp op [x, y]) (fromJust . getFixity . fst) e xs
 
 longPattern = setR parsePatAnn <&> (reverse . getPVars &&& id)
 
diff --git a/src/LambdaCube/Compiler/Patterns.hs b/src/LambdaCube/Compiler/Patterns.hs
index 9a986fd6..a2bc3831 100644
--- a/src/LambdaCube/Compiler/Patterns.hs
+++ b/src/LambdaCube/Compiler/Patterns.hs
@@ -42,13 +42,11 @@ data Pat_ c
     | PCon_ SI (SIName, c) [ParPat_ c]
     | ViewPat_ SI SExp (ParPat_ c)
     | PatType_ SI (ParPat_ c) SExp
-  deriving Show
 
 type ParPat = ParPat_ ConsInfo
 
 -- parallel patterns like  v@(f -> [])@(Just x)
 data ParPat_ c = ParPat_ SI [Pat_ c]
-  deriving Show
 
 pattern ParPat ps <- ParPat_ _ ps
   where ParPat ps =  ParPat_ (foldMap sourceInfo ps) ps
@@ -198,7 +196,6 @@ data Lets a
     = LLet SIName SExp (Lets a)
     | LTypeAnn SExp (Lets a)        -- TODO: eliminate if not used
     | In a
-  deriving Show
 
 lLet sn (SVar sn' i) l = rSubst 0 i l
 lLet sn e l = LLet sn e l
@@ -223,7 +220,6 @@ data GuardTree
     = GuardNode SExp (SIName, ConsInfo) [SIName] GuardTrees GuardTrees
     | GTSuccess SExp
     | GTFailure
-  deriving Show
 
 instance DeBruijnify SIName GuardTree where
     deBruijnify_ l ns = mapGT (`deBruijnify_` ns) (`deBruijnify_` ns) l
diff --git a/src/LambdaCube/Compiler/Pretty.hs b/src/LambdaCube/Compiler/Pretty.hs
index 4b266fea..511e57f6 100644
--- a/src/LambdaCube/Compiler/Pretty.hs
+++ b/src/LambdaCube/Compiler/Pretty.hs
@@ -13,7 +13,7 @@ module LambdaCube.Compiler.Pretty
     ( module LambdaCube.Compiler.Pretty
     ) where
 
-import Data.Monoid
+--import Data.Monoid
 import Data.String
 import Data.Char
 --import qualified Data.Set as Set
@@ -39,9 +39,9 @@ data Fixity
 
 instance PShow Fixity where
     pShow = \case
-        Infix  i -> "infix"  `DApp` pShow i
-        InfixL i -> "infixl" `DApp` pShow i
-        InfixR i -> "infixr" `DApp` pShow i
+        Infix  i -> "infix"  <+> pShow i
+        InfixL i -> "infixl" <+> pShow i
+        InfixR i -> "infixr" <+> pShow i
 
 precedence, leftPrecedence, rightPrecedence :: Fixity -> Int
 
@@ -98,12 +98,6 @@ strip = \case
     DFreshName _ x -> strip x
     x              -> x
 
-simple :: Doc -> Bool
-simple x = case strip x of
-    DAtom{} -> True
-    DVar{} -> True
-    _ -> False
-
 instance Show Doc where
     show = show . renderDoc
 
@@ -232,6 +226,7 @@ pattern DBrace x = DPar "{" x "}"
 pattern DOp s f l r = DInfix f l (SimpleAtom s) r
 pattern DSep p a b = DOp " " p a b
 pattern DGlue p a b = DOp "" p a b
+pattern DAt x = DGlue (InfixR 20) (DText "@") x
 
 pattern DArr_ s x y = DOp s (InfixR (-1)) x y
 pattern DArr x y = DArr_ "->" x y
@@ -246,9 +241,9 @@ shTuple [] = "()"
 shTuple [x] = DParen $ DParen x
 shTuple xs = DParen $ foldr1 DComma xs
 
-shLet i a b = shLam' (shLet' (blue $ shVar i) $ DUp i a) (DUp i b)
-shLet_ a b = DFreshName True $ shLam' (shLet' (shVar 0) $ DUp 0 a) b
-shLet' = DOp ":=" (Infix (-4))
+shLet i a b = shLam' (DLet (blue $ shVar i) $ DUp i a) (DUp i b)
+shLet_ a b = DFreshName True $ shLam' (DLet (shVar 0) $ DUp 0 a) b
+pattern DLet x y = DOp ":=" (Infix (-4)) x y
 
 shAnn True x (strip -> DText "Type") = x
 shAnn _ x y = DOp "::" (InfixR (-3)) x y
@@ -293,6 +288,9 @@ instance PShow ()      where pShow _ = "()"
 instance PShow Bool where
     pShow b = if b then "True" else "False"
 
+instance PShow Void where
+    pShow = elimVoid
+
 instance (PShow a, PShow b) => PShow (Either a b) where
    pShow = either (("Left" `DApp`) . pShow) (("Right" `DApp`) . pShow)
 
diff --git a/src/LambdaCube/Compiler/Statements.hs b/src/LambdaCube/Compiler/Statements.hs
index 6a0ac767..2112dd69 100644
--- a/src/LambdaCube/Compiler/Statements.hs
+++ b/src/LambdaCube/Compiler/Statements.hs
@@ -35,12 +35,14 @@ data PreStmt
     | FunAlt SIName [(Visibility, SExp)]{-TODO: remove-} GuardTrees
     | Class SIName [SExp]{-parameters-} [(SIName, SExp)]{-method names and types-}
     | Instance SIName [ParPat]{-parameter patterns-} [SExp]{-constraints-} [Stmt]{-method definitions-}
-    deriving (Show)
+
+instance PShow PreStmt where
+    pShow _ = text "PreStmt - TODO"
 
 instance DeBruijnify SIName PreStmt where
     deBruijnify_ k v = \case
         FunAlt n ts gue -> FunAlt n (map (second $ deBruijnify_ k v) ts) $ deBruijnify_ k v gue
-        x -> error $ "deBruijnify @ " ++ show x
+        x -> error $ "deBruijnify @ " ++ ppShow x
 
 mkLets :: [Stmt]{-where block-} -> SExp{-main expression-} -> SExp{-big let with lambdas; replaces global names with de bruijn indices-}
 mkLets = mkLets_ SLet
@@ -52,7 +54,7 @@ mkLets_ mkLet = mkLets' . sortDefs where
       where
         x' = if usedS n x then SBuiltin "primFix" `SAppV` SLamV (deBruijnify [n] x) else x
     mkLets' (PrecDef{}: ds) e = mkLets' ds e
-    mkLets' (x: ds) e = error $ "mkLets: " ++ show x
+    mkLets' (x: ds) e = error $ "mkLets: " ++ ppShow x
 
 type DefinedSet = Set.Set SName
 
diff --git a/src/LambdaCube/Compiler/Utils.hs b/src/LambdaCube/Compiler/Utils.hs
index 36dbe050..8e5dbee5 100644
--- a/src/LambdaCube/Compiler/Utils.hs
+++ b/src/LambdaCube/Compiler/Utils.hs
@@ -1,6 +1,9 @@
 {-# LANGUAGE NoMonomorphismRestriction #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
 module LambdaCube.Compiler.Utils where
 
 import qualified Data.IntSet as IS
@@ -8,8 +11,11 @@ import qualified Data.Text as T
 import qualified Text.Show.Pretty as PP
 import Control.Monad.Catch
 import Control.Monad.Except
+import Control.Monad.RWS
 import System.Directory
 import qualified Data.Text.IO as TIO
+import qualified Text.Megaparsec as P
+import qualified Text.Megaparsec.Prim as P
 
 ------------------------------------------------------- general functions
 
@@ -106,10 +112,23 @@ readFileIfExists fname = do
     b <- doesFileExist fname
     return $ if b then Just $ readFileStrict fname else Nothing
 
-------------------------------------------------------- misc
+------------------------------------------------------- missing instances
 
 instance MonadMask m => MonadMask (ExceptT e m) where
     mask f = ExceptT $ mask $ \u -> runExceptT $ f (mapExceptT u)
     uninterruptibleMask = error "not implemented: uninterruptibleMask for ExcpetT"
 
+instance (Monoid w, P.MonadParsec st m t) => P.MonadParsec st (RWST r w s m) t where
+    failure                     = lift . P.failure
+    label                       = mapRWST . P.label
+    try                         = mapRWST P.try
+    lookAhead          (RWST m) = RWST $ \r s -> (\(a, _, _) -> (a, s, mempty)) <$> P.lookAhead (m r s)
+    notFollowedBy      (RWST m) = RWST $ \r s -> P.notFollowedBy ((\(a, _, _) -> a) <$> m r s) >> return ((), s, mempty)
+    withRecovery rec   (RWST m) = RWST $ \r s -> P.withRecovery (\e -> runRWST (rec e) r s) (m r s)
+    eof                         = lift P.eof
+    token  f e                  = lift $ P.token  f e
+    tokens f e ts               = lift $ P.tokens f e ts
+    getParserState              = lift P.getParserState
+    updateParserState f         = lift $ P.updateParserState f
+