3 files changed, 187 insertions, 187 deletions

diff --git a/src/LambdaCube/Compiler/DesugaredSource.hs b/src/LambdaCube/Compiler/DesugaredSource.hs
index 60807cc6..0511988a 100644
--- a/src/LambdaCube/Compiler/DesugaredSource.hs
+++ b/src/LambdaCube/Compiler/DesugaredSource.hs
@@ -8,7 +8,10 @@
 {-# LANGUAGE DeriveFunctor #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
-module LambdaCube.Compiler.DesugaredSource where
+module LambdaCube.Compiler.DesugaredSource
+    ( module LambdaCube.Compiler.DesugaredSource
+    , FixityDir(..), Fixity(..)
+    )where
 
 import Data.Monoid
 import Data.Maybe
@@ -19,8 +22,6 @@ import Data.Bits
 import qualified Data.Map as Map
 import qualified Data.Set as Set
 import qualified Data.IntMap as IM
-import Control.Monad.Reader
-import Control.Monad.State
 import Control.Arrow hiding ((<+>))
 import Control.DeepSeq
 
@@ -53,14 +54,6 @@ pattern MatchName :: SName -> SName
 pattern MatchName cs <- 'm':'a':'t':'c':'h':cs where MatchName cs = "match" ++ cs
 
 
--------------------------------------------------------------------------------- fixity
-
-data FixityDir = Infix | InfixL | InfixR
-    deriving (Eq, Show)
-
-data Fixity = Fixity !FixityDir !Int
-    deriving (Eq, Show)
-
 -------------------------------------------------------------------------------- file position
 
 -- source position without file name
@@ -392,6 +385,39 @@ trSExp f = g where
 trSExp' :: SExp -> SExp' a
 trSExp' = trSExp elimVoid
 
+instance Up a => PShow (SExp' a) where
+    pShowPrec _ = showDoc_ . sExpDoc
+
+sExpDoc :: Up a => SExp' a -> NDoc
+sExpDoc = \case
+    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)-}  -> shAtom "<<>>" -- todo: expDoc e
+    SVar _ i        -> shVar i
+    SLit _ l        -> shAtom $ show l
+
+shLam usedVar h a b = DFreshName usedVar $ lam (p $ DUp 0 a) b
+  where
+    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
+
 -------------------------------------------------------------------------------- statement
 
 data Stmt
@@ -474,174 +500,3 @@ data Extension
 extensionMap :: Map.Map String Extension
 extensionMap = Map.fromList $ map (show &&& id) [toEnum 0 .. ]
 
--------------------------------------------------------------------------------- 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
-        DFreshName True x -> gets head >>= \n -> modify tail >> local (n:) (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 = xs !! i
-        lookupVarName i _ = ((\s n -> n: '_': s) <$> iterate ('\'':) "" <*> ['a'..'z']) !! i
-
-    addPar :: Int -> NDoc -> NDoc
-    addPar pr x = case x of
-        DAtom{} -> x
-        DColor c x -> DColor c $ addPar pr x
-        DPar l x r -> DPar l (addPar (-20) x) r
-        DOp pr' x s y -> paren $ DOp pr' (addPar (precL pr') x) s (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 
-
-        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
-
--- name De Bruijn indices
-type NameDB a = StateT [String] (Reader [String]) a
-
-showDoc :: NDoc -> String
-showDoc = show . renderDocX
-
-showDoc_ :: NDoc -> Doc
-showDoc_ = renderDocX
-
-sExpDoc :: Up a => SExp' a -> NDoc
-sExpDoc = \case
-    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)-}  -> shAtom "<<>>" -- todo: expDoc e
-    SVar _ i        -> shVar i
-    SLit _ l        -> shAtom $ show l
-
-shVar = DVar
-
-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 usedVar $ lam (p $ DUp 0 a) b
-  where
-    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/Parser.hs b/src/LambdaCube/Compiler/Parser.hs
index 8a9e56c1..fd2cdbfd 100644
--- a/src/LambdaCube/Compiler/Parser.hs
+++ b/src/LambdaCube/Compiler/Parser.hs
@@ -146,18 +146,14 @@ mkDesugarInfo ss = DesugarInfo
 
 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/Pretty.hs b/src/LambdaCube/Compiler/Pretty.hs
index e1d41fc1..5044eecf 100644
--- a/src/LambdaCube/Compiler/Pretty.hs
+++ b/src/LambdaCube/Compiler/Pretty.hs
@@ -21,9 +21,14 @@ import qualified Data.Set as Set
 import Data.Map (Map)
 import qualified Data.Map as Map
 import Control.Monad.Except
+import Control.Monad.Reader
+import Control.Monad.State
+import Control.Arrow hiding ((<+>))
 import Debug.Trace
 
-import Text.PrettyPrint.Leijen
+import Text.PrettyPrint.Leijen hiding ((<$>))
+
+import LambdaCube.Compiler.Utils
 
 --------------------------------------------------------------------------------
 
@@ -150,3 +155,147 @@ error_ = error . correctEscs
 trace_ = trace . correctEscs
 throwError_ = throwError . correctEscs
 
+
+-------------------------------------------------------------------------------- fixity
+
+data FixityDir = Infix | InfixL | InfixR
+    deriving (Eq, Show)
+
+data Fixity = Fixity !FixityDir !Int
+    deriving (Eq, Show)
+
+-------------------------------------------------------------------------------- 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
+        DFreshName True x -> gets head >>= \n -> modify tail >> local (n:) (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 = xs !! i
+        lookupVarName i _ = ((\s n -> n: '_': s) <$> iterate ('\'':) "" <*> ['a'..'z']) !! i
+
+    addPar :: Int -> NDoc -> NDoc
+    addPar pr x = case x of
+        DAtom{} -> x
+        DColor c x -> DColor c $ addPar pr x
+        DPar l x r -> DPar l (addPar (-20) x) r
+        DOp pr' x s y -> paren $ DOp pr' (addPar (precL pr') x) s (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 
+
+        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
+        
+showDoc :: NDoc -> String
+showDoc = show . renderDocX
+
+showDoc_ :: NDoc -> Doc
+showDoc_ = renderDocX
+
+shVar = DVar
+
+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
+
+-----------------------------------------
+
+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
+
+