improve pretty printing & try to fix local function handling

5 files changed, 74 insertions, 56 deletions

diff --git a/src/LambdaCube/Compiler/Core.hs b/src/LambdaCube/Compiler/Core.hs
index 5e2b4136..a75beb60 100644
--- a/src/LambdaCube/Compiler/Core.hs
+++ b/src/LambdaCube/Compiler/Core.hs
@@ -21,7 +21,7 @@ import Control.Arrow hiding ((<+>))
 --import LambdaCube.Compiler.Utils
 import LambdaCube.Compiler.DeBruijn
 import LambdaCube.Compiler.Pretty hiding (braces, parens)
-import LambdaCube.Compiler.DesugaredSource hiding (getList)
+import LambdaCube.Compiler.DesugaredSource
 
 -------------------------------------------------------------------------------- De-Bruijn limit
 
@@ -509,8 +509,7 @@ instance MkDoc Exp where
             Pi h TType b    -> shLam_ (usedVar 0 b) (BPi h) Nothing (f b)
             Pi h a b        -> shLam (usedVar 0 b) (BPi h) (f a) (f b)
             ENat n          -> pShow n
-            (getTTup -> Just xs) -> shTuple $ f <$> xs
-            (getTup -> Just xs)  -> shTuple $ f <$> xs
+            ConN FHCons [_, _, x, xs] -> foldl DApp (text "HCons") (f <$> [x, xs])
             Con s _ xs      -> foldl DApp (pShow s) (f <$> xs)
             TyConN s xs     -> foldl DApp (pShow s) (f <$> xs)
             TType           -> text "Type"
@@ -533,17 +532,6 @@ instance MkDoc Neutral where
             TyCaseFun_ s [m, t, f] n  -> foldl DApp (pShow s) (g <$> [m, t, Neut n, f])
             TyCaseFun_ s _ n -> error $ "mkDoc TyCaseFun"
 
-getTup (hnf -> ConN FHCons [_, _, x, xs]) = (x:) <$> getTup xs
-getTup (hnf -> ConN FHNil []) = Just []
-getTup _ = Nothing
-
-getTTup (hnf -> TyConN FHList [xs]) = getList xs
-getTTup _ = Nothing
-
-getList (hnf -> ConN FCons [x, xs]) = (x:) <$> getList xs
-getList (hnf -> ConN FNil []) = Just []
-getList _ = Nothing
-
 -------------------------------------------------------------------------------- reduction
 
 {- todo: generate
@@ -686,7 +674,7 @@ cstr = f []
 
     f_ [] typ a@Neut{} a' = CstrT typ a a'
     f_ [] typ a a'@Neut{} = CstrT typ a a'
-    f_ ns typ a a' = CEmpty $ unlines [ "can not unify", ppShow a, "with", ppShow a' ]
+    f_ ns typ a a' = CEmpty $ simpleShow $ nest 2 ("can not unify" <$$> DTypeNamespace True (pShow a)) <$$> nest 2 ("with" <$$> DTypeNamespace True (pShow a'))
 
     ff _ _ [] = CUnit
     ff ns tt@(Pi v t _) ((t1, t2'): ts) = t2 (f ns t t1 t2') $ ff ns (appTy tt t1) ts
diff --git a/src/LambdaCube/Compiler/CoreToIR.hs b/src/LambdaCube/Compiler/CoreToIR.hs
index 303f1156..f65b543d 100644
--- a/src/LambdaCube/Compiler/CoreToIR.hs
+++ b/src/LambdaCube/Compiler/CoreToIR.hs
@@ -865,7 +865,7 @@ mkLam _ = Nothing
 
 mkCon (ExpTV (I.Con s n xs) et vs) = Just (untick $ show s, chain vs (I.conType et s) $ I.mkConPars n et ++ xs)
 mkCon (ExpTV (I.TyCon s xs) et vs) = Just (untick $ show s, chain vs (nType s) xs)
-mkCon (ExpTV (I.Neut (I.Fun s (reverse -> xs) def)) et vs) = Just (untick $ show s, chain vs (nType s) xs)
+mkCon (ExpTV (I.Neut (I.Fun s@(I.FunName _ 0 _{-I.DeltaDef{}-} _) (reverse -> xs) def)) et vs) = Just (untick $ show s, chain vs (nType s) xs)
 mkCon (ExpTV (I.CaseFun s xs n) et vs) = Just (untick $ show s, chain vs (nType s) $ makeCaseFunPars' (mkEnv vs) n ++ xs ++ [I.Neut n])
 mkCon (ExpTV (I.TyCaseFun s [m, t, f] n) et vs) = Just (untick $ show s, chain vs (nType s) [m, t, I.Neut n, f])
 mkCon _ = Nothing
@@ -874,7 +874,13 @@ mkApp (ExpTV (I.Neut (I.App_ a b)) et vs) = Just (ExpTV (I.Neut a) t vs, head $
   where t = neutType' (mkEnv vs) a
 mkApp _ = Nothing
 
-mkFunc r@(ExpTV (IFunc (show -> n) def nt xs) ty vs) | all (supType . tyOf) (r: xs') && n `notElem` ["typeAnn"] && all validChar n
+removeRHS 0 (I.RHS x) = Just x
+removeRHS n (I.Lam x) | n > 0 = I.Lam <$> removeRHS (n-1) x
+removeRHS _ _ = Nothing
+
+mkFunc r@(ExpTV (I.Neut (I.Fun (I.FunName (show -> n) 0 (I.ExpDef def_) nt) xs I.RHS{})) ty vs)
+    | Just def <- removeRHS (length xs) def_
+    , all (supType . tyOf) (r: xs') && n `notElem` ["typeAnn"] && all validChar n
     = Just (untick n +++ intercalate "_" (filter (/="TT") $ map (filter isAlphaNum . plainShow) hs), toExp $ I.ET (foldl I.app_ def hs) (foldl I.appTy nt hs), tyOf r, xs')
   where
     a +++ [] = a
@@ -897,21 +903,10 @@ unLab' (I.RHS x) = unLab' x   -- TODO: remove
 unLab' x = x
 
 unFunc' (I.Reduced x) = unFunc' x   -- todo: remove?
-unFunc' (UFL x) = unFunc' x
+unFunc' (I.Neut (I.Fun (I.FunName _ _ I.ExpDef{} _) _ y)) = unFunc' y
 unFunc' (I.RHS x) = unFunc' x   -- TODO: remove
 unFunc' x = x
 
-pattern UFL y <- I.Neut (I.Fun (I.FunName _ _ I.ExpDef{} _) _ y)
-
-pattern IFunc n def ty xs <- (mkIFunc -> Just (n, def, ty, xs))
-
-mkIFunc (I.Neut (I.Fun (I.FunName n 0 (I.ExpDef def) ty) xs I.RHS{})) | Just def' <- removeRHS (length xs) def = Just (n, def', ty, xs)
-mkIFunc _ = Nothing
-
-removeRHS 0 (I.RHS x) = Just x
-removeRHS n (I.Lam x) | n > 0 = I.Lam <$> removeRHS (n-1) x
-removeRHS _ _ = Nothing
-
 instance Subst I.Exp ExpTV where
     subst_ i0 dx x (ExpTV a at vs) = ExpTV (subst_ i0 dx x a) (subst_ i0 dx x at) (zipWith (\i -> subst_ (i0+i) (I.upDB i dx) $ up i x{-todo: review-}) [1..] vs)
 
diff --git a/src/LambdaCube/Compiler/DesugaredSource.hs b/src/LambdaCube/Compiler/DesugaredSource.hs
index 271c678e..074e0299 100644
--- a/src/LambdaCube/Compiler/DesugaredSource.hs
+++ b/src/LambdaCube/Compiler/DesugaredSource.hs
@@ -235,7 +235,6 @@ instance PShow FName where
     pShow (CFName _ (SData s)) = pShow s
     pShow s = maybe (error "show") text' $ lookup s $ map (\(a, b) -> (b, a)) fntable
       where
-        text' "Nil" = "[]"
         text' ":" = pShow ConsName
         text' s = text s
 
@@ -468,7 +467,10 @@ shApp Hidden a b = DApp a (DAt b)
 
 shLam usedVar h a b = shLam_ usedVar h (Just a) b
 
-shLam_ False (BPi Hidden) (Just (DText "'CW" `DApp` a)) b = DFreshName False $ showContext (DUp 0 a) b
+simpleFo (DExpand x _) = x
+simpleFo x = x
+
+shLam_ False (BPi Hidden) (Just ((simpleFo -> DText "'CW") `DApp` a)) b = DFreshName False $ showContext (DUp 0 a) b
   where
     showContext x (DFreshName u d) = DFreshName u $ showContext (DUp 0 x) d
     showContext x (DParContext xs y) = DParContext (DComma x xs) y
@@ -500,18 +502,19 @@ shLam_ usedVar h a b = DFreshName usedVar $ lam (p $ DUp 0 <$> a) b
     showForall s x (DForall s' xs y) | s == s' = DForall s (DSep (InfixR 11) x xs) y
     showForall s x y = DForall s x y
 
-    -- TODO: use other sign instead of (=>)
-    showContext x (DFreshName u d) = DFreshName u $ showContext (DUp 0 x) d
-    showContext x (DParContext xs y) = DParContext (DComma x xs) y
-    showContext x (DContext xs y) = DParContext (DComma x xs) y
-    showContext x y = DContext x y
+    showContext x y = DContext' x y
 
 showLam x (DFreshName u d) = DFreshName u $ 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 = DLet' (DLet "=" (blue $ shVar i) $ DUp i a) (DUp i b)
-shLet_ a b = DFreshName True $ DLet' (DLet "=" (shVar 0) $ DUp 0 a) b
+
+showLet x (DFreshName u d) = DFreshName u $ showLet (DUp 0 x) d
+showLet x (DLet' xs y) = DLet' (DSemi x xs) y
+showLet x y = DLet' x y
+
+shLet_ a b = DFreshName True $ showLet (DLet "=" (shVar 0) $ DUp 0 a) b
 
 -------------------------------------------------------------------------------- statement
 
diff --git a/src/LambdaCube/Compiler/Infer.hs b/src/LambdaCube/Compiler/Infer.hs
index b511d9c0..1cb528ea 100644
--- a/src/LambdaCube/Compiler/Infer.hs
+++ b/src/LambdaCube/Compiler/Infer.hs
@@ -51,17 +51,21 @@ varType err n_ env = f n_ env where
 
 mkELet n x xt env = {-(if null vs then id else trace_ $ "mkELet " ++ show (length vs) ++ " " ++ show n)-} term
   where
-    vs = sort $ Set.toList $ join grow $ free x <> free xt
+    vs = sort $ Set.toList $ grow mempty $ free x <> free xt
     nloc = length vs
-    fn = FunName (mkFName n) nloc (ExpDef $ addLams 0 vs x) (addPis 0 vs xt)
+    fn = FunName (mkFName n) nloc (ExpDef $ addLams vs x) (addPis vs xt)
 
     term = mkFun fn (Var <$> reverse vs) $ getFix x 0
 
-    addLams l [] x = x
-    addLams l (v: vs) x = Lam $ rMove v l $ addLams (l+1) vs x
+    getFix (Lam z) i = Lam $ getFix z (i+1)
+    getFix (DFun FprimFix _ [t, Lam f]) i = subst 0 (foldl app_ term (downTo 0 i)) f
+    getFix x _ = x
 
-    addPis l [] x = x
-    addPis l (v: vs) x = Pi Visible (snd $ varType "mkELet" v env) $ rMove v l $ addPis (l+1) vs x
+    addLams [] x = x
+    addLams (v: vs) x = Lam $ rMove v 0 $ addLams vs x
+
+    addPis [] x = x
+    addPis (v: vs) x = Pi Visible (snd $ varType "mkELet" v env) $ rMove v 0 $ addPis vs x
 
     grow acc s
         | Set.null s = acc
@@ -69,12 +73,6 @@ mkELet n x xt env = {-(if null vs then id else trace_ $ "mkELet " ++ show (lengt
       where
         s' = mconcat (free . snd . flip (varType "mkELet2") env <$> Set.toList s)
 
-    getFix (Lam z) i = Lam $ getFix z (i+1)
-    getFix (DFun FprimFix _ [t, Lam f]) i = subst 0 (foldl app_ term (downTo 0 i)) f
-    getFix x _ = x
-
-
-
 instance PShow (CEnv Exp) where
     pShow = mkDoc False
 
diff --git a/src/LambdaCube/Compiler/Pretty.hs b/src/LambdaCube/Compiler/Pretty.hs
index f9702b94..db31ee2e 100644
--- a/src/LambdaCube/Compiler/Pretty.hs
+++ b/src/LambdaCube/Compiler/Pretty.hs
@@ -16,6 +16,7 @@ module LambdaCube.Compiler.Pretty
 import Data.Maybe
 import Data.String
 import Data.Char
+import Data.Monoid
 --import qualified Data.Set as Set
 --import qualified Data.Map as Map
 import Control.Applicative
@@ -153,8 +154,22 @@ renderDoc
         showVarA (SimpleAtom s) = pure $ SimpleAtom s
         showVarA (ComplexAtom s i d a) = ComplexAtom s i <$> showVars d <*> showVarA a
 
+    getTup (DText "HCons" `DApp` x `DApp` (getTup -> Just xs)) = Just $ x: xs
+    getTup (DText "HNil") = Just []
+    getTup _ = Nothing
+
+    getList (DOp0 ":" _ `DApp` x `DApp` (getList -> Just xs)) = Just $ x: xs
+    getList (DText "Nil") = Just []
+    getList _ = Nothing
+
+    shTick True = DPreOp 20 (SimpleAtom "'")
+    shTick False = id
+
     namespace :: Bool -> Doc -> Doc
     namespace tn x = case x of
+        (getTup -> Just xs) -> shTick tn $ namespace tn $ shTuple xs
+        (getList -> Just xs) -> shTick tn $ namespace tn $ shList xs
+        DText "'HList" `DApp` (getList -> Just xs) -> shTick (not tn) $ namespace tn $ shTuple xs
         DAtom x -> DAtom $ namespaceA x
         DText "'List" `DApp` x -> namespace tn $ DBracket x
         DInfix pr' x op y -> DInfix pr' (namespace tn x) (namespaceA op) (namespace tn y)
@@ -198,25 +213,39 @@ renderDoc
     getApps (DApp (getApps -> (n, xs)) x) = (n, x: xs)
     getApps x = (x, [])
 
+    getSemis (DSemi x (getSemis -> (xs, n))) = (x: xs, n)
+    getSemis x = ([], x)
+
+    getCommas (DComma x (getCommas -> xs)) = x: xs
+    getCommas x = [x]
+
     render :: Doc -> P.Doc
     render = snd . render'
       where
         render' = \case
-            DText "Nil" -> rtext "[]"
-            DText "'Nil" -> rtext "'[]"
             DAtom x -> renderA x
             DFormat c x -> second c $ render' x
             DDocOp f d -> (('\0', '\0'), f $ render <$> d)
-            DPreOp _ op y -> renderA op <++> render' y
+            DPreOp _ op y -> renderA' op <++> render' y
             DSep (InfixR 11) a b -> gr $ render' a <+++> render' b
             x@DApp{} -> case getApps x of
                 (n, reverse -> xs) -> ((\xs -> (fst $ head xs, snd $ last xs)) *** P.nest 2 . P.sep) (unzip $ render' n: (render' <$> xs))
+            x@DComma{} -> case getCommas x of
+                x: xs -> ((\xs -> (fst $ head xs, snd $ last xs)) *** P.cat) (unzip $ render' x: (second ("," P.<+>) . render' <$> xs))
+            x@DSemi{} -> case getSemis x of
+                (xs, n) -> ((\xs -> (fst $ head xs, snd $ last xs)) *** P.sep) (unzip $ (second (<> ";") . render' <$> xs) ++ [render' n])
             DInfix _ x op y -> gr $ render' x <+++> renderA op <++> render' y
 
+        renderA' (SimpleAtom s) = rtext s
+        renderA' x = gr $ renderA'' x
+
+        renderA'' (SimpleAtom s) = rtext s
+        renderA'' (ComplexAtom s _ d a) = rtext s <+++> render' d <+++> renderA'' a
+
         renderA (SimpleAtom s) = rtext s
         renderA (ComplexAtom s _ d a) = rtext s <++> render' d <++> renderA a
 
-        gr = second (P.nest 2. P.group)
+        gr = second (P.nest 2 . P.group)
 
         rtext "" = (('\0', '\0'), mempty)
         rtext s@(h:_) = ((h, last s), P.text s)
@@ -224,12 +253,12 @@ renderDoc
         ((lx, rx), x) <++> ((ly, ry), y) = ((lx, ry), z)
           where
             z | sep rx ly = x P.<+> y
-              | otherwise = x P.<> y
+              | otherwise = x <> y
 
         ((lx, rx), x) <+++> ((ly, ry), y) = ((lx, ry), z)
           where
-            z | sep rx ly = x P.<> P.line P.<> y
-              | otherwise = x P.<> y
+            z | sep rx ly = x <> P.line <> y
+              | otherwise = x <> y
 
         sep x y
             | x == '\0' || y == '\0' = False
@@ -291,6 +320,7 @@ infixl 4 `DApp`
 
 pattern DAt x       = DGlue     (InfixR   20) (DText "@") x
 pattern DApp x y    = DSep      (InfixL   10)  x y
+pattern DSemi x y   = DOp ";"   (InfixR (-19)) 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 (DTypeNamespace True y)
@@ -317,12 +347,16 @@ shTuple [] = "()"
 shTuple [x] = DParen $ DParen x
 shTuple xs = DParen $ foldr1 DComma xs
 
+shList [] = "[]"
+shList xs = DBracket $ foldr1 DComma xs
+
 shAnn = DAnn
 
 shArr = DArr
 
 
 pattern DForall s vs e = DArr_ s (DPreOp 10 (SimpleAtom "forall") vs) e
+pattern DContext' vs e = DArr_ "->" (DAt vs) e
 pattern DContext vs e = DArr_ "=>" vs e
 pattern DParContext vs e = DContext (DParen vs) e
 pattern DLam vs e = DPreOp (-10) (ComplexAtom "\\" 11 vs (SimpleAtom "->")) e