refactored pretty print framework

8 files changed, 244 insertions, 167 deletions

diff --git a/src/LambdaCube/Compiler/DesugaredSource.hs b/src/LambdaCube/Compiler/DesugaredSource.hs
index af85af65..54455fc7 100644
--- a/src/LambdaCube/Compiler/DesugaredSource.hs
+++ b/src/LambdaCube/Compiler/DesugaredSource.hs
@@ -14,13 +14,11 @@ import Data.Monoid
 import Data.Maybe
 import Data.Char
 import Data.List
-import Data.String
 import Data.Function
 import Data.Bits
 import qualified Data.Map as Map
 import qualified Data.Set as Set
 import qualified Data.IntMap as IM
-import Control.Monad.Except
 import Control.Monad.Reader
 import Control.Monad.State
 import Control.Arrow hiding ((<+>))
@@ -28,9 +26,7 @@ import Control.DeepSeq
 
 import LambdaCube.Compiler.Utils
 import LambdaCube.Compiler.DeBruijn
-
-import qualified LambdaCube.Compiler.Pretty as Parser
-import LambdaCube.Compiler.Pretty hiding (Doc, braces, parens)
+import LambdaCube.Compiler.Pretty --hiding (braces, parens)
 
 -------------------------------------------------------------------------------- simple name
 
@@ -62,7 +58,7 @@ pattern MatchName cs <- 'm':'a':'t':'c':'h':cs where MatchName cs = "match" ++ c
 data FixityDir = Infix | InfixL | InfixR
     deriving (Eq, Show)
 
-data Fixity = Fixity FixityDir Int
+data Fixity = Fixity !FixityDir !Int
     deriving (Eq, Show)
 
 -------------------------------------------------------------------------------- file position
@@ -91,7 +87,7 @@ instance Ord FileInfo where compare = compare `on` fileId
 instance PShow FileInfo where pShowPrec _ = text . filePath
 instance Show FileInfo where show = ppShow
 
-showPos :: FileInfo -> SPos -> Parser.Doc
+showPos :: FileInfo -> SPos -> Doc
 showPos n p = pShow n <> ":" <> pShow p
 
 -------------------------------------------------------------------------------- range
@@ -107,7 +103,7 @@ instance PShow Range where pShowPrec _ (Range n b e) = pShow n <+> pShow b <> "-
 instance Show Range where show = ppShow
 
 -- long version
-showRange :: Range -> Parser.Doc
+showRange :: Range -> Doc
 showRange (Range n p@(SPos r c) (SPos r' c')) = vcat
      $ (showPos n p <> ":")
      : map text (drop (r - 1) $ take r' $ lines $ fileContent n)
@@ -478,126 +474,188 @@ data Extension
 extensionMap :: Map.Map String Extension
 extensionMap = Map.fromList $ map (show &&& id) [toEnum 0 .. ]
 
--------------------------------------------------------------------------------- builtin precedences
-
-data Prec
-    = PrecAtom      --  ( _ )  ...
-    | PrecAtom'
-    | PrecAt        --  _@_                 {assoc}  -- in patterns
-    | PrecProj      --  _ ._                {left}
-    | PrecSwiz      --  _%_                 {left}
-    | PrecApp       --  _ _                 {left}
-    | PrecOp
-    | PrecArr       --  _ -> _              {right}
-    | PrecEq        --  _ ~ _
-    | PrecAnn       --  _ :: _              {right}
-    | PrecLet       --  _ := _
-    | PrecLam       --  \ _ -> _            {right} {accum}
-    deriving (Eq, Ord)
-
+-------------------------------------------------------------------------------- pretty print
+
+data NDoc
+    = DAtom String
+    | DOp Fixity NDoc String NDoc
+    | DPar String NDoc String
+    | DLam String [NDoc] String NDoc
+    | DVar Int
+    | DFreshName Bool{-False: dummy-} NDoc
+    | DUp Int NDoc
+    | DColor Color NDoc
+    -- add wl-pprint combinators as necessary here
+    deriving (Eq)
+
+pattern DParen x = DPar "(" x ")"
+pattern DBrace x = DPar "{" x "}"
+pattern DArr x y = DOp (Fixity InfixR (-1)) x "->" y
+pattern DAnn x y = DOp (Fixity InfixR (-3)) x ":" y
+
+data Color = Green | Blue | Underlined
+    deriving (Eq)
+
+inGreen' = DColor Green
+inBlue' = DColor Blue
+epar = DColor Underlined
+
+strip = \case
+    DColor _ x -> strip x
+    DUp _ x -> strip x
+    DFreshName _ x -> strip x
+    x -> x
+
+simple x = case strip x of
+    DAtom{} -> True
+    DVar{} -> True
+    DPar{} -> True
+    _ -> False
+
+renderDocX :: NDoc -> Doc
+renderDocX = render . addPar (-10) . flip runReader [] . flip evalStateT (flip (:) <$> iterate ('\'':) "" <*> ['a'..'z']) . showVars
+  where
+    showVars x = case x of
+        DAtom s -> pure x
+        DColor c x -> DColor c <$> showVars x
+        DPar l x r -> DPar l <$> showVars x <*> pure r
+        DOp pr x s y -> DOp pr <$> showVars x <*> pure s <*> showVars y
+        DVar i -> asks $ DAtom . lookupVarName i
+        -- hack, remove
+        DFreshName True (DArr (DAnn a (DUp 0 b)) y) -> do
+            b' <- showVars b
+            newName $ showVars $ DArr (DAnn a b') y
+        -- hack, remove
+        DFreshName True (DArr (DUp 0 b) y) -> do
+            b' <- showVars b
+            newName $ showVars $ DArr b' y
+        DFreshName True x -> newName $ showVars x
+        DFreshName False x -> local ("?":) $ showVars x
+        DUp i x -> local (dropNth i) $ showVars x
+        DLam lam vs arr e -> DLam lam <$> (mapM showVars vs) <*> pure arr <*> showVars e
+      where
+        lookupVarName i xs | i < length xs && i >= 0 = xs !! i
+        lookupVarName i _ = "V" ++ show i -- TODO: better names here
+
+    addPar :: Int -> NDoc -> NDoc
+    addPar pr x = case x of
+        DColor c x -> DColor c $ addPar pr x
+        DAtom{} -> x
+        DPar l x r -> DPar l (addPar (-20) x) r
+        DOp pr' x s y -> (if simple x' && simple y' && s `notElem` ["", ","] then id else paren) $ DOp pr' x' s y'
+          where
+            x' = addPar (precL pr') x
+            y' = addPar (precR pr') y
+        DLam lam vs arr e -> paren $ DLam lam (addPar 10 <$> vs) arr (addPar (-10) e)
+      where
+        paren d
+            | protect x = DParen d
+            | otherwise = d
+          where
+            protect x = case x of
+                DAtom{} -> False
+                DPar{} -> False
+                DOp (Fixity _ pr') _ _ _ -> pr' < pr
+                DLam{} -> -10 < pr 
+                DColor _ x     -> protect x
+
+        precL (Fixity Infix  i) = i+1
+        precL (Fixity InfixL i) = i
+        precL (Fixity InfixR i) = i+1
+        precR (Fixity Infix  i) = i+1
+        precR (Fixity InfixL i) = i+1
+        precR (Fixity InfixR i) = i
+
+    render x = case x of
+        DColor Green x -> text $ inGreen $ show $ render x -- TODO
+        DColor Blue x -> text $ inBlue $ show $ render x -- TODO
+        DColor Underlined x -> text $ underlined $ show $ render x -- TODO
+        DAtom s -> text s
+        DPar l x r -> text l <> render x <> text r
+        DOp _ x s y -> case s of
+            "" -> render x <+> render y
+            _ | simple x && simple y && s /= "," -> render x <> text s <> render y
+              | otherwise -> (render x <++> s) <+> render y
+        DLam lam vs arr e -> text lam <> hsep (render <$> vs) <+> text arr <+> render e
+      where
+        x <++> "," = x <> text ","
+        x <++> s = x <+> text s
+        
 instance Up a => PShow (SExp' a) where
     pShowPrec _ = showDoc_ . sExpDoc
 
-type Doc = NameDB PrecString
-
 -- name De Bruijn indices
 type NameDB a = StateT [String] (Reader [String]) a
 
-showDoc :: Doc -> String
-showDoc = str . flip runReader [] . flip evalStateT (flip (:) <$> iterate ('\'':) "" <*> ['a'..'z'])
+showDoc :: NDoc -> String
+showDoc = show . renderDocX
 
-showDoc_ :: Doc -> Parser.Doc
-showDoc_ = text . str . flip runReader [] . flip evalStateT (flip (:) <$> iterate ('\'':) "" <*> ['a'..'z'])
+showDoc_ :: NDoc -> Doc
+showDoc_ = renderDocX
 
-sExpDoc :: Up a => SExp' a -> Doc
+sExpDoc :: Up a => SExp' a -> NDoc
 sExpDoc = \case
-    SGlobal ns      -> pure $ shAtom $ sName ns
-    SAnn a b        -> shAnn ":" False <$> sExpDoc a <*> sExpDoc b
-    TyType a        -> shApp Visible (shAtom "tyType") <$> sExpDoc a
-    SApp h a b      -> shApp h <$> sExpDoc a <*> sExpDoc b
-    Wildcard t      -> shAnn ":" True (shAtom "_") <$> sExpDoc t
-    SBind_ _ h _ a b -> join $ shLam (usedVar 0 b) h <$> sExpDoc a <*> pure (sExpDoc b)
+    SGlobal ns      -> shAtom $ sName ns
+    SAnn a b        -> shAnn ":" False (sExpDoc a) (sExpDoc b)
+    TyType a        -> shApp Visible (shAtom "tyType") (sExpDoc a)
+    SApp h a b      -> shApp h (sExpDoc a) (sExpDoc b)
+    Wildcard t      -> shAnn ":" True (shAtom "_") (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)-}  -> pure $ shAtom "<<>>" -- todo: expDoc e
-    SVar _ i        -> shAtom <$> shVar i
-    SLit _ l        -> pure $ shAtom $ show l
-
-shVar i = asks lookupVarName where
-    lookupVarName xs | i < length xs && i >= 0 = xs !! i
-    lookupVarName _ = "V" ++ show i
-
-newName = gets head <* modify tail
-
-shLet i a b = shAtom <$> shVar i >>= \i' -> local (dropNth i) $ shLam' <$> (cpar . shLet' (fmap inBlue i') <$> a) <*> b
-shLet_ a b = newName >>= \i -> shLam' <$> (cpar . shLet' (shAtom i) <$> a) <*> local (i:) b
-shLam usedVar h a b = newName >>= \i ->
-    let lam = case h of
-            BPi _ -> shArr
-            _ -> shLam'
-        p = case h of
-            BMeta -> cpar . shAnn ":" True (shAtom $ inBlue i)
-            BLam h -> vpar h
-            BPi h -> vpar h
-        vpar Hidden = brace . shAnn ":" True (shAtom $ inGreen i)
-        vpar Visible = ann (shAtom $ inGreen i)
-        ann | usedVar = shAnn ":" False
-            | otherwise = const id
-    in lam (p a) <$> local (i:) b
+    STyped _{-(e,t)-}  -> shAtom "<<>>" -- todo: expDoc e
+    SVar _ i        -> shVar i
+    SLit _ l        -> shAtom $ show l
 
------------------------------------------
+shVar = DVar
+
+newName p = gets head >>= \n -> modify tail >> local (n:) p
 
-data PS a = PS Prec a deriving (Functor)
-type PrecString = PS String
-
-getPrec (PS p _) = p
-prec i s = PS i (s i)
-str (PS _ s) = s
-
-lpar, rpar :: PrecString -> Prec -> String
-lpar (PS i s) j = par (i >. j) s  where
-    PrecLam >. i = i > PrecAtom'
-    i >. PrecLam = i >= PrecArr
-    PrecApp >. PrecApp = False
-    i >. j  = i >= j
-rpar (PS i s) j = par (i >. j) s where
-    PrecLam >. PrecLam = False
-    PrecLam >. i = i > PrecAtom'
-    PrecArr >. PrecArr = False
-    PrecAnn >. PrecAnn = False
-    i >. j  = i >= j
-
-par True s = "(" ++ s ++ ")"
-par False s = s
-
-isAtom = (==PrecAtom) . getPrec
-isAtom' = (<=PrecAtom') . getPrec
-
-shAtom = PS PrecAtom
-shAtom' = PS PrecAtom'
-shTuple xs = prec PrecAtom $ \_ -> case xs of
-    [x] -> "((" ++ str x ++ "))"
-    xs -> "(" ++ intercalate ", " (map str xs) ++ ")"
-shAnn _ True x y | str y `elem` ["Type", inGreen "Type"] = x
-shAnn s simp x y | isAtom x && isAtom y = shAtom' $ str x <> s <> str y
-shAnn s simp x y = prec PrecAnn $ lpar x <> " " <> const s <> " " <> rpar y
-shApp Hidden x y = prec PrecApp $ lpar x <> " " <> const (str $ brace y)
-shApp h x y = prec PrecApp $ lpar x <> " " <> rpar y
-shArr x y | isAtom x && isAtom y = shAtom' $ str x <> "->" <> str y
-shArr x y = prec PrecArr $ lpar x <> " -> " <> rpar y
-shCstr x y | isAtom x && isAtom y = shAtom' $ str x <> "~" <> str y
-shCstr x y = prec PrecEq $ lpar x <> " ~ " <> rpar y
-shLet' x y | isAtom x && isAtom y = shAtom' $ str x <> ":=" <> str y
-shLet' x y = prec PrecLet $ lpar x <> " := " <> rpar y
-shLam' x y | PrecLam <- getPrec y = prec PrecLam $ "\\" <> lpar x <> " " <> pure (dropC $ str y)
+shLet i a b = shLam' (cpar . shLet' (inBlue' $ shVar i) $ DUp i a) (DUp i b)
+shLet_ a b = DFreshName True $ shLam' (cpar . shLet' (shVar 0) $ DUp 0 a) b
+
+shLam usedVar h a b = DFreshName True $ lam (p $ DUp 0 a) b
   where
-    dropC (ESC s (dropC -> x)) = ESC s x
-    dropC (x: xs) = xs
-shLam' x y | isAtom x && isAtom y = shAtom' $ "\\" <> str x <> "->" <> str y
-shLam' x y = prec PrecLam $ "\\" <> lpar x <> " -> " <> rpar y
-brace s = shAtom $ "{" <> str s <> "}"
-cpar s | isAtom' s = s      -- TODO: replace with lpar, rpar
-cpar s = shAtom $ par True $ str s
-epar = fmap underlined
-
-instance IsString (Prec -> String) where fromString = const
+    lam = case h of
+        BPi{} -> shArr
+        _ -> shLam'
+
+    p = case h of
+        BMeta -> cpar . shAnn ":" True (inBlue' $ DVar 0)
+        BLam h -> vpar h
+        BPi h -> vpar h
+
+    vpar Hidden = (\p -> DBrace p) . shAnn ":" True (inGreen' $ DVar 0)
+    vpar Visible = ann (inGreen' $ DVar 0)
+
+    ann | usedVar = shAnn ":" False
+        | otherwise = const id
+
+-----------------------------------------
+
+shAtom = DAtom
+
+shTuple [] = DAtom "()"
+shTuple [x] = DParen $ DParen x
+shTuple xs = DParen $ foldr1 (\x y -> DOp (Fixity InfixR (-20)) x "," y) xs
+
+shAnn _ True x y | strip y == DAtom "Type" = x
+shAnn s _ x y = DOp (Fixity InfixR (-3)) x s y
+
+shApp _ x y = DOp (Fixity InfixL 10) x "" y
+
+shArr = DArr
+
+shCstr x y = DOp (Fixity Infix (-2)) x "~" y
+
+shLet' x y = DOp (Fixity Infix (-4)) x ":=" y
+
+getFN (DFreshName True a) = first (+1) $ getFN a
+getFN a = (0, a)
+
+shLam' x (getFN -> (i, DLam "\\" xs "->" y)) = iterateN i (DFreshName True) $ DLam "\\" (iterateN i (DUp 0) x: xs) "->" y
+shLam' x y = DLam "\\" [x] "->" y
+
+cpar s | simple s = s
+cpar s = DParen s
+
 
diff --git a/src/LambdaCube/Compiler/Infer.hs b/src/LambdaCube/Compiler/Infer.hs
index 8b3b5c12..0015e364 100644
--- a/src/LambdaCube/Compiler/Infer.hs
+++ b/src/LambdaCube/Compiler/Infer.hs
@@ -47,7 +47,7 @@ import Control.DeepSeq
 
 import LambdaCube.Compiler.Utils
 import LambdaCube.Compiler.DeBruijn
-import LambdaCube.Compiler.Pretty hiding (Doc, braces, parens)
+import LambdaCube.Compiler.Pretty hiding (braces, parens)
 import LambdaCube.Compiler.DesugaredSource hiding (getList)
 import LambdaCube.Compiler.Parser (ParseWarning) -- TODO: remove
 
@@ -1457,20 +1457,22 @@ instance PShow (CEnv Exp) where
     pShowPrec _ = showDoc_ . mkDoc False False
 
 instance PShow Env where
-    pShowPrec _ e = showDoc_ $ envDoc e $ pure $ shAtom $ underlined "<<HERE>>"
+    pShowPrec _ e = showDoc_ $ envDoc e $ shAtom $ underlined "<<HERE>>"
 
 showEnvExp :: Env -> ExpType -> String
-showEnvExp e c = showDoc $ envDoc e $ epar <$> mkDoc False False c
+showEnvExp e c = showDoc $ envDoc e $ epar $ mkDoc False False c
 
 showEnvSExp :: Up a => Env -> SExp' a -> String
-showEnvSExp e c = showDoc $ envDoc e $ epar <$> sExpDoc c
+showEnvSExp e c = showDoc $ envDoc e $ epar $ sExpDoc c
 
 showEnvSExpType :: Up a => Env -> SExp' a -> Exp -> String
-showEnvSExpType e c t = showDoc $ envDoc e $ epar <$> (shAnn "::" False <$> sExpDoc c <**> mkDoc False False (t, TType))
+showEnvSExpType e c t = showDoc $ envDoc e $ epar $ (shAnn "::" False (sExpDoc c) (mkDoc False False (t, TType)))
+{-
   where
     infixl 4 <**>
     (<**>) :: NameDB (a -> b) -> NameDB a -> NameDB b
     a <**> b = get >>= \s -> lift $ evalStateT a s <*> evalStateT b s
+-}
 
 {-
 expToSExp :: Exp -> SExp
@@ -1501,75 +1503,75 @@ nameSExp = \case
     STyped_ (e, _)  -> nameSExp $ expToSExp e  -- todo: mark boundary
     SVar i          -> SGlobal <$> shVar i
 -}
-envDoc :: Env -> Doc -> Doc
+envDoc :: Env -> NDoc -> NDoc
 envDoc x m = case x of
     EGlobal{}           -> m
-    EBind1 _ h ts b     -> envDoc ts $ join $ shLam (usedVar 0 b) h <$> m <*> pure (sExpDoc b)
-    EBind2 h a ts       -> envDoc ts $ join $ shLam True h <$> mkDoc False ts' (a, TType) <*> pure m
-    EApp1 _ h ts b      -> envDoc ts $ shApp h <$> m <*> sExpDoc b
-    EApp2 _ h (Lam (Var 0), Pi Visible TType _) ts -> envDoc ts $ shApp h (shAtom "tyType") <$> m
-    EApp2 _ h a ts      -> envDoc ts $ shApp h <$> mkDoc False ts' a <*> m
+    EBind1 _ h ts b     -> envDoc ts $ shLam (usedVar 0 b) h m (sExpDoc 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)
+    EApp2 _ h (Lam (Var 0), Pi Visible TType _) ts -> envDoc ts $ shApp h (shAtom "tyType") m
+    EApp2 _ h a ts      -> envDoc ts $ shApp h (mkDoc False ts' a) m
     ELet1 _ ts b        -> envDoc ts $ shLet_ m (sExpDoc 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)
-    CheckIType t ts     -> envDoc ts $ shAnn ":" False <$> m <*> pure (shAtom "??") -- mkDoc ts' t
+    CheckType t ts      -> envDoc ts $ shAnn ":" False m $ mkDoc False ts' (t, TType)
+    CheckIType t ts     -> envDoc ts $ shAnn ":" False m (shAtom "??") -- mkDoc ts' t
 --    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 (shAtom "labEnd") <$> m
+    ELabelEnd ts        -> envDoc ts $ shApp Visible (shAtom "labEnd") m
     x   -> error $ "envDoc: " ++ show x
   where
     ts' = False
 
 class MkDoc a where
-    mkDoc :: Bool {-print reduced-} -> Bool -> a -> Doc
+    mkDoc :: Bool {-print reduced-} -> Bool -> a -> NDoc
 
 instance MkDoc ExpType where
     mkDoc pr ts e = mkDoc pr ts $ fst e
 
 instance MkDoc Exp where
-    mkDoc pr ts e = fmap inGreen <$> f e
+    mkDoc pr ts e = inGreen' $ f e
       where
         f = \case
 --            Lam h a b       -> join $ shLam (usedVar 0 b) (BLam h) <$> f a <*> pure (f b)
-            Lam b           -> join $ shLam True (BLam Visible) <$> f TType{-todo!-} <*> pure (f b)
-            Pi h a b        -> join $ shLam (usedVar 0 b) (BPi h) <$> f a <*> pure (f b)
-            ENat' n         -> pure $ shAtom $ show n
-            (getTTup -> Just xs) -> shTuple <$> mapM f xs
-            (getTup -> Just xs) -> shTuple <$> mapM f xs
-            Con s _ xs      -> foldl (shApp Visible) (shAtom_ $ show s) <$> mapM f xs
-            TyConN s xs     -> foldl (shApp Visible) (shAtom_ $ show s) <$> mapM f xs
-            TType           -> pure $ shAtom "Type"
-            ELit l          -> pure $ shAtom $ show l
+            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         -> shAtom $ show n
+            (getTTup -> Just xs) -> shTuple $ f <$> xs
+            (getTup -> Just xs)  -> shTuple $ f <$> xs
+            Con s _ xs      -> foldl (shApp Visible) (shAtom_ $ show s) (f <$> xs)
+            TyConN s xs     -> foldl (shApp Visible) (shAtom_ $ show s) (f <$> xs)
+            TType           -> shAtom "Type"
+            ELit l          -> shAtom $ show l
             Neut x          -> mkDoc pr ts x
 
         shAtom_ = shAtom . if ts then switchTick else id
 
 instance MkDoc Neutral where
-    mkDoc pr ts e = fmap inGreen <$> f e
+    mkDoc pr ts e = inGreen' $ f e
       where
         g = mkDoc pr ts
         f = \case
-            CstrT' t a b     -> shCstr <$> g (a, t) <*> g (b, t)
+            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) (shAtom_ $ show s) <$> mapM g xs
-            Var_ k           -> shAtom <$> shVar k
-            App_ a b         -> shApp Visible <$> g a <*> g b
-            CaseFun_ s xs n  -> foldl (shApp Visible) (shAtom_ $ show s) <$> mapM g ({-mkExpTypes (nType s) $ makeCaseFunPars te n ++ -} xs ++ [Neut n])
-            TyCaseFun_ s [m, t, f] n  -> foldl (shApp Visible) (shAtom_ $ show s) <$> mapM g (mkExpTypes (nType s) [m, t, Neut n, f])
-            TyCaseFun_ s _ n  -> error $ "mkDoc TyCaseFun"
-            LabelEnd_ x      -> shApp Visible (shAtom $ "labend") <$> g x
-            Delta{} -> return $ shAtom "^delta"
+            Fun' s vs i (mkExpTypes (nType s) . reverse -> xs) _ -> foldl (shApp Visible) (shAtom_ $ show s) (g <$> xs)
+            Var_ k           -> shVar k
+            App_ a b         -> shApp Visible (g a) (g b)
+            CaseFun_ s xs n  -> foldl (shApp Visible) (shAtom_ $ show s) (map g $ {-mkExpTypes (nType s) $ makeCaseFunPars te n ++ -} xs ++ [Neut n])
+            TyCaseFun_ s [m, t, f] n  -> foldl (shApp Visible) (shAtom_ $ show s) (g <$> mkExpTypes (nType s) [m, t, Neut n, f])
+            TyCaseFun_ s _ n -> error $ "mkDoc TyCaseFun"
+            LabelEnd_ x      -> shApp Visible (shAtom "labend") (g x)
+            Delta{}          -> shAtom "^delta"
 
         shAtom_ = shAtom . if ts then switchTick else id
 
 instance MkDoc (CEnv Exp) where
-    mkDoc pr ts e = fmap inGreen <$> f e
+    mkDoc pr ts e = inGreen' $ f e
       where
-        f :: CEnv Exp -> Doc
+        f :: CEnv Exp -> NDoc
         f = \case
             MEnd a          -> mkDoc pr ts a
-            Meta a b        -> join $ shLam True BMeta <$> mkDoc pr ts a <*> pure (f b)
+            Meta a b        -> shLam True BMeta (mkDoc pr ts a) (f b)
             Assign i (x, _) e -> shLet i (mkDoc pr ts x) (f e)
 
 getTup (unfixlabel -> ConN FHCons [_, _, x, xs]) = (x:) <$> getTup xs
diff --git a/src/LambdaCube/Compiler/Parser.hs b/src/LambdaCube/Compiler/Parser.hs
index 7dfcd580..8a9e56c1 100644
--- a/src/LambdaCube/Compiler/Parser.hs
+++ b/src/LambdaCube/Compiler/Parser.hs
@@ -142,6 +142,23 @@ mkDesugarInfo ss = DesugarInfo
         Data sn _ _ cs -> Set.fromList $ sName sn: map (sName . fst) cs
         PrecDef{} -> mempty
 
+-------------------------------------------------------------------------------- precedences -- TODO: remove
+
+data Prec
+    = PrecAtom      --  ( _ )  ...                                          -- 20
+    | PrecAtom'                                                             
+    | PrecAt        --  _@_                 {assoc}  -- in patterns         -- 13
+    | PrecProj      --  _ ._                {left}                          -- 12
+    | PrecSwiz      --  _%_                 {left}                          -- 11
+    | PrecApp       --  _ _                 {left}                          -- 10
+    | PrecOp                                                                -- 0 - 9
+    | PrecArr       --  _ -> _              {right}                         -- -1
+    | PrecEq        --  _ ~ _                                               -- -2
+    | PrecAnn       --  _ :: _              {right}                         -- -3
+    | PrecLet       --  _ := _                                              -- -4
+    | PrecLam       --  \ _ -> _            {right} {accum}                 -- -10
+                    --  _ , _               {right}                         -- -20
+    deriving (Eq, Ord)
 
 -------------------------------------------------------------------------------- expression parsing
 
diff --git a/src/LambdaCube/Compiler/Patterns.hs b/src/LambdaCube/Compiler/Patterns.hs
index 0ebb6a97..00626d2e 100644
--- a/src/LambdaCube/Compiler/Patterns.hs
+++ b/src/LambdaCube/Compiler/Patterns.hs
@@ -18,7 +18,7 @@ import Control.Arrow hiding ((<+>))
 
 import LambdaCube.Compiler.Utils
 import LambdaCube.Compiler.DeBruijn
-import LambdaCube.Compiler.Pretty hiding (Doc, braces, parens)
+import LambdaCube.Compiler.Pretty hiding (braces, parens)
 import LambdaCube.Compiler.DesugaredSource
 
 ---------------------------------
@@ -157,13 +157,13 @@ instance SetSourceInfo (Pat_ c) where
 
 -------------------------------------------------------------------------------- pretty print
 
-patDoc :: Pat_ a -> Doc
+patDoc :: Pat_ a -> NDoc
 patDoc = \case
-    PCon (n, _) _ -> pure $ shAtom $ sName n -- TODO
+    PCon (n, _) _ -> shAtom $ sName n -- TODO
 
-parPatDoc :: ParPat_ a -> Doc
+parPatDoc :: ParPat_ a -> NDoc
 parPatDoc = \case
-    ParPat [] -> pure $ shAtom "_"
+    ParPat [] -> shAtom "_"
     ParPat [p] -> patDoc p
     -- TODO
 -------------------------------------------------------------------------------- pattern match compilation
diff --git a/src/LambdaCube/Compiler/Pretty.hs b/src/LambdaCube/Compiler/Pretty.hs
index 2fa539a3..e1d41fc1 100644
--- a/src/LambdaCube/Compiler/Pretty.hs
+++ b/src/LambdaCube/Compiler/Pretty.hs
@@ -120,7 +120,7 @@ splitESC _ = Nothing
 
 withEsc i s = ESC (show i) $ s ++ ESC "" ""
 
-inGreen = withEsc 32
+inGreen = withEsc 32    -- TODO
 inBlue = withEsc 34
 inRed = withEsc 31
 underlined = withEsc 47
diff --git a/src/LambdaCube/Compiler/Statements.hs b/src/LambdaCube/Compiler/Statements.hs
index afb5fbc1..fa4f02bc 100644
--- a/src/LambdaCube/Compiler/Statements.hs
+++ b/src/LambdaCube/Compiler/Statements.hs
@@ -19,7 +19,7 @@ import Control.Arrow hiding ((<+>))
 --import Debug.Trace
 
 import LambdaCube.Compiler.DeBruijn
-import LambdaCube.Compiler.Pretty hiding (Doc, braces, parens)
+import LambdaCube.Compiler.Pretty hiding (braces, parens)
 import LambdaCube.Compiler.DesugaredSource
 import LambdaCube.Compiler.Patterns
 
diff --git a/testdata/instantiate2.out b/testdata/instantiate2.out
index b7d32356..1a2a8631 100644
--- a/testdata/instantiate2.out
+++ b/testdata/instantiate2.out
@@ -1 +1 @@
-(+ ('VecS 'Float 2) TT (V2 1.0 2.0) (V2 2.3 3.4), 3.0)
\ No newline at end of file
+(+ ('VecS 'Float 2) TT (V2 1.0 2.0) (V2 2.3 3.4), 3.0)
\ No newline at end of file
diff --git a/testdata/typesig.reject.out b/testdata/typesig.reject.out
index 9c2979a6..590a5d21 100644
--- a/testdata/typesig.reject.out
+++ b/testdata/typesig.reject.out
@@ -1,12 +1,12 @@
-focus checkMetas: \a -> (\b:Type -> primFix a b) (\a:=Type c:Type -> <<HERE>>)
-\(a : Type~V0) (b : V1~'X) -> typeAnn V2 (labend X)
+focus checkMetas: \a -> (\b:Type -> primFix a b) (\(a:=Type) -> \c:Type -> <<HERE>>)
+\(a : Type~V0) (b : V1~'X) -> typeAnn V2 (labend X)
 ------------ trace
 'X :: Type
 X :: 'X
 'XCase :: (b : 'X->Type) -> b X -> d:'X -> b d
 match'X :: (b : Type->Type) -> b 'X -> d:Type -> b d -> b d
-!focus checkMetas: \a -> (\b:Type -> primFix a b) (\a:=Type c:Type -> <<HERE>>)
-\(a : Type~V0) (b : V1~'X) -> typeAnn V2 (labend X)
+!focus checkMetas: \a -> (\b:Type -> primFix a b) (\(a:=Type) -> \c:Type -> <<HERE>>)
+\(a : Type~V0) (b : V1~'X) -> typeAnn V2 (labend X)
 ------------ tooltips
 testdata/typesig.reject.lc 4:6-4:7  Type
 testdata/typesig.reject.lc 4:6-4:11  Type