refactoring

6 files changed, 49 insertions, 30 deletions

diff --git a/src/LambdaCube/Compiler.hs b/src/LambdaCube/Compiler.hs
index ecb33167..bc1f615b 100644
--- a/src/LambdaCube/Compiler.hs
+++ b/src/LambdaCube/Compiler.hs
@@ -188,8 +188,8 @@ loadModule ex imp mname_ = do
     filterImports (ImportJust ns) = (`elem` map sName ns)
 
 -- used in runTests
-getDef :: MonadMask m => FilePath -> SName -> Maybe Exp -> MMT m Infos (Infos, Either Doc (FilePath, Either Doc (Exp, Exp)))
-getDef = getDef_ fst
+getDef :: MonadMask m => FilePath -> SName -> Maybe Exp -> MMT m (Infos, [Stmt]) ((Infos, [Stmt]), Either Doc (FilePath, Either Doc (Exp, Exp)))
+getDef = getDef_ id
 
 getDef_ ex m d ty = loadModule ex Nothing (Left m) <&> \case
     Left err -> (mempty, Left err)
diff --git a/src/LambdaCube/Compiler/DesugaredSource.hs b/src/LambdaCube/Compiler/DesugaredSource.hs
index 6c4ff0e0..8f92f18a 100644
--- a/src/LambdaCube/Compiler/DesugaredSource.hs
+++ b/src/LambdaCube/Compiler/DesugaredSource.hs
@@ -79,7 +79,6 @@ instance Eq FileInfo where (==) = (==) `on` fileId
 instance Ord FileInfo where compare = compare `on` fileId
 
 instance PShow FileInfo where pShow = text . filePath
-instance Show FileInfo where show = ppShow
 
 showPos :: FileInfo -> SPos -> Doc
 showPos n p = pShow n <> ":" <> pShow p
@@ -117,7 +116,7 @@ instance NFData SI where
         NoSI x -> rnf x
         RangeSI r -> rnf r
 
-instance Show SI where show _ = "SI"
+--instance Show SI where show _ = "SI"
 instance Eq SI where _ == _ = True
 instance Ord SI where _ `compare` _ = EQ
 
@@ -149,7 +148,7 @@ pattern SIName si n <- SIName_ si _ n
 
 instance Eq SIName where (==) = (==) `on` sName
 instance Ord SIName where compare = compare `on` sName
-instance Show SIName where show = sName
+--instance Show SIName where show = sName
 instance PShow SIName
   where
     pShow (SIName si n) = expand (text n) $ case si of
@@ -210,10 +209,10 @@ data Binder
     = BPi  Visibility
     | BLam Visibility
     | BMeta      -- a metavariable is like a floating hidden lambda
-  deriving (Eq, Show)
+  deriving (Eq)
 
 data Visibility = Hidden | Visible
-  deriving (Eq, Show)
+  deriving (Eq)
 
 dummyName s = SIName (debugSI s) ("v_" ++ s)
 dummyName' = SData . dummyName
@@ -380,10 +379,11 @@ trSExp' = trSExp elimVoid
 
 instance (Up a, PShow a) => PShow (SExp' a) where
     pShow = \case
+        SGlobal op | Just p <- getFixity op -> DOp0 (sName op) p
         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)
+        TyType a        -> text "tyType" `dApp` pShow a
+        SAppV a b       -> pShow a `dApp` 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)
@@ -427,8 +427,8 @@ showLam x (DFreshName True d) = DFreshName True $ showLam (DUp 0 x) d
 showLam x (DLam xs y) = DLam (DSep (InfixR 11) x xs) y
 showLam x y = DLam x y
 
-shLet i a b = showLam (DLet (blue $ shVar i) $ DUp i a) (DUp i b)
-shLet_ a b = DFreshName True $ showLam (DLet (shVar 0) $ DUp 0 a) b
+shLet i a b = showLam (DLet ":=" (blue $ shVar i) $ DUp i a) (DUp i b)
+shLet_ a b = DFreshName True $ showLam (DLet ":=" (shVar 0) $ DUp 0 a) b
 
 -------------------------------------------------------------------------------- statement
 
@@ -441,9 +441,10 @@ pattern Primitive n t = Let n (Just t) (SBuiltin "undefined")
 
 instance PShow Stmt where
     pShow = \case
-        Let n ty e -> text (sName n) </> "=" <+> maybe (pShow e) (\ty -> pShow e </> "::" <+> pShow ty) ty 
+        Primitive n t -> shAnn False (pShow n) (pShow t)
+        Let n ty e -> DLet "=" (pShow n) $ maybe (pShow e) (\ty -> shAnn False (pShow e) (pShow ty)) ty 
         Data n ps ty cs -> "data" <+> text (sName n)
-        PrecDef n i -> "precedence" <+> text (sName n) <+> text (show i)
+        PrecDef n i -> pShow i <+> DOp0 (sName n) i
 
 instance DeBruijnify SIName Stmt where
     deBruijnify_ k v = \case
diff --git a/src/LambdaCube/Compiler/Infer.hs b/src/LambdaCube/Compiler/Infer.hs
index ad7eeae6..88860d62 100644
--- a/src/LambdaCube/Compiler/Infer.hs
+++ b/src/LambdaCube/Compiler/Infer.hs
@@ -63,7 +63,7 @@ data Exp
     | Neut Neutral
 
 data Freq = CompileTime | RunTime
-  deriving (Eq, Show)
+  deriving (Eq)
 
 pattern TType = TType_ CompileTime
 
@@ -756,7 +756,7 @@ instance Monoid MaxDB where
         max 0 x = x
         max _ _ = 1 --
 
-instance Show MaxDB where show _ = "MaxDB"
+--instance Show MaxDB where show _ = "MaxDB"
 
 varDB i = MaxDB 1 --
 
diff --git a/src/LambdaCube/Compiler/Lexer.hs b/src/LambdaCube/Compiler/Lexer.hs
index 46c44086..e10ac817 100644
--- a/src/LambdaCube/Compiler/Lexer.hs
+++ b/src/LambdaCube/Compiler/Lexer.hs
@@ -181,7 +181,7 @@ commaSep1 p = sepBy1 p $ symbol ","
 -------------------------------------------------------------------------------- namespace handling
 
 data Namespace = TypeNS | ExpNS
-  deriving (Eq, Show)
+  deriving (Eq)
 
 tick c = f <$> asks namespace
   where
diff --git a/src/LambdaCube/Compiler/Pretty.hs b/src/LambdaCube/Compiler/Pretty.hs
index 2059e530..1d0e07dd 100644
--- a/src/LambdaCube/Compiler/Pretty.hs
+++ b/src/LambdaCube/Compiler/Pretty.hs
@@ -35,7 +35,7 @@ data Fixity
     = Infix  !Int
     | InfixL !Int
     | InfixR !Int
-    deriving (Eq, Show)
+    deriving (Eq)
 
 instance PShow Fixity where
     pShow = \case
@@ -64,6 +64,7 @@ data Doc
 
     | DAtom DocAtom
     | DInfix Fixity Doc DocAtom Doc
+    | DPreOp Int DocAtom Doc
 
     | DFreshName Bool{-used-} Doc
     | DVar Int
@@ -120,6 +121,7 @@ renderDoc
         DDocOp x d -> DDocOp x $ expand full <$> d
         DAtom s -> DAtom $ mapDocAtom (\_ _ -> noexpand) s
         DInfix pr x op y -> DInfix pr (noexpand x) (mapDocAtom (\_ _ -> noexpand) op) (noexpand y)
+        DPreOp pr op y -> DPreOp pr (mapDocAtom (\_ _ -> noexpand) op) (noexpand y)
         DVar i -> DVar i
         DFreshName b x -> DFreshName b $ noexpand x
         DUp i x -> DUp i $ noexpand x
@@ -129,6 +131,7 @@ renderDoc
         DFormat c x -> DFormat c <$> showVars x
         DDocOp x d -> DDocOp x <$> traverse showVars d
         DInfix pr x op y -> DInfix pr <$> showVars x <*> showVarA op <*> showVars y
+        DPreOp pr op y -> DPreOp pr <$> showVarA op <*> showVars y
         DVar i -> asks $ text . (!! i)
         DFreshName True x -> gets head >>= \n -> modify tail >> local (n:) (showVars x)
         DFreshName False x -> local ("_":) $ showVars x
@@ -140,8 +143,13 @@ renderDoc
     addPar :: Int -> Doc -> Doc
     addPar pr x = case x of
         DAtom x -> DAtom $ addParA x
+        DOp0 s f -> DParen $ DOp0 s f
+        DOpL s f x -> DParen $ DOpL s f $ addPar (leftPrecedence f) x
+        DOpR s f x -> DParen $ DOpR s f $ addPar (rightPrecedence f) x
         DInfix pr' x op y -> (if protect then DParen else id)
                        $ DInfix pr' (addPar (leftPrecedence pr') x) (addParA op) (addPar (rightPrecedence pr') y)
+        DPreOp pr' op y -> (if protect then DParen else id)
+                       $ DPreOp pr' (addParA op) (addPar pr' y)
         DFormat c x -> DFormat c $ addPar pr x
         DDocOp x d -> DDocOp x $ addPar (-10) <$> d
       where
@@ -149,6 +157,7 @@ renderDoc
 
         protect = case x of
             DInfix f _ _ _ -> precedence f < pr
+            DPreOp f _ _ -> f < pr
             _ -> False
 
     render :: Doc -> P.Doc
@@ -159,6 +168,7 @@ renderDoc
             DDocOp f d -> (('\0', '\0'), f $ render <$> d)
             DAtom x -> renderA x
             DInfix _ x op y -> render' x <++> renderA op <++> render' y
+            DPreOp _ op y -> renderA op <++> render' y
 
         renderA (SimpleAtom s) = rtext s
         renderA (ComplexAtom s _ d a) = rtext s <++> render' d <++> renderA a
@@ -220,40 +230,50 @@ shVar = DVar
 shortForm d = DPar "" d ""
 expand = DExpand
 
-pattern DPar l d r = DAtom (ComplexAtom l (-20) d (SimpleAtom r))
+pattern DAt x       = DGlue     (InfixR   20) (DText "@") x
+pattern DApp x y    = DSep      (InfixL   10)  x y
+pattern DArr_ s x y = DOp s     (InfixR  (-1)) x y      -- -> => .
+pattern DCstr x y   = DOp "~"   (Infix   (-2)) x y
+pattern DAnn x y    = DOp "::"  (Infix   (-3)) x y
+pattern DLet s x y  = DOp s     (Infix   (-4)) x y      -- := =
+pattern DComma a b  = DOp ","   (InfixR (-20)) a b
+pattern DPar l d r  = DAtom (ComplexAtom l (-20) d (SimpleAtom r))
+
 pattern DParen x = DPar "(" x ")"
 pattern DBrace x = DPar "{" x "}"
 pattern DOp s f l r = DInfix f l (SimpleAtom s) r
+pattern DOp0 s f = DOp s f (DText "") (DText "")
+pattern DOpL s f x = DOp s f x (DText "")
+pattern DOpR s f x = DOp s f (DText "") x
 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
-pattern DAnn x y = DOp "::" (InfixR (-3)) x y
-pattern DApp x y = DSep (InfixL 10) x y
-pattern DComma a b = DOp "," (InfixR (-20)) a b
 
 braces = DBrace
 parens = DParen
 
+dApp (DOp0 s f) x = DOpL s f x
+dApp (DOpL s f x) y = DOp s f x y
+dApp x y = DApp x y
+
+shCstr = DCstr
+
 shTuple [] = "()"
 shTuple [x] = DParen $ DParen x
 shTuple xs = DParen $ foldr1 DComma xs
 
-pattern DLet x y = DOp ":=" (Infix (-4)) x y
-
 shAnn True x (strip -> DText "Type") = x
-shAnn _ x y = DOp "::" (InfixR (-3)) x y
+shAnn True x (strip -> DText "'Type") = x
+shAnn _ x y = DAnn x y
 
 shArr = DArr
 
-shCstr = DOp "~" (Infix (-2))
 
 pattern DForall s vs e = DArr_ s (DSep (Infix 10) (DText "forall") vs) e
 pattern DContext vs e = DArr_ "=>" vs e
 pattern DParContext vs e = DContext (DParen vs) e
-pattern DLam vs e = DSep (InfixR (-10)) (DAtom (ComplexAtom "\\" 11 vs (SimpleAtom "->"))) e
+pattern DLam vs e = DPreOp (-10) (ComplexAtom "\\" 11 vs (SimpleAtom "->")) e
 
 --------------------------------------------------------------------------------
 
diff --git a/src/LambdaCube/Compiler/Utils.hs b/src/LambdaCube/Compiler/Utils.hs
index 8e5dbee5..78872b04 100644
--- a/src/LambdaCube/Compiler/Utils.hs
+++ b/src/LambdaCube/Compiler/Utils.hs
@@ -36,7 +36,6 @@ unfoldNat z s n | n > 0 = s $ unfoldNat z s (n-1)
 
 data Void
 
-instance Show Void where show = elimVoid
 instance Eq Void where x == y = elimVoid x
 
 elimVoid :: Void -> a
@@ -47,7 +46,6 @@ elimVoid v = case v of
 -- supplementary data: data with no semantic relevance
 newtype SData a = SData a
 
-instance Show (SData a) where show _ = "SData"
 instance Eq (SData a) where _ == _ = True
 instance Ord (SData a) where _ `compare` _ = EQ