removing coloring from .out files

3 files changed, 36 insertions, 23 deletions

diff --git a/src/LambdaCube/Compiler/DesugaredSource.hs b/src/LambdaCube/Compiler/DesugaredSource.hs
index 33912ae3..7351f4d7 100644
--- a/src/LambdaCube/Compiler/DesugaredSource.hs
+++ b/src/LambdaCube/Compiler/DesugaredSource.hs
@@ -447,7 +447,7 @@ data Stmt
 pattern Primitive n t = Let n (Just t) (SBuiltin "undefined")
 
 instance PShow Stmt where
-    pShow = \case
+    pShow stmt = DResetFreshNames $ case stmt of
         Primitive n t -> shAnn (pShow n) (pShow t)
         Let n ty e -> DLet "=" (pShow n) $ maybe (pShow e) (\ty -> shAnn (pShow e) (pShow ty)) ty 
         Data n ps ty cs -> nest 4 $ "data" <+> shAnn (foldl dApp (DTypeNamespace True $ pShow n) [shAnn (text "_") (pShow t) | (v, t) <- ps]) (pShow ty) <+> "where" <$$> vcat [shAnn (pShow n) $ pShow t | (n, t) <- cs]
diff --git a/src/LambdaCube/Compiler/Infer.hs b/src/LambdaCube/Compiler/Infer.hs
index 61a50814..1b747e69 100644
--- a/src/LambdaCube/Compiler/Infer.hs
+++ b/src/LambdaCube/Compiler/Infer.hs
@@ -952,10 +952,10 @@ inferN_ tellTrace = infer  where
         Parens x        -> infer te x
         SAnn x t        -> checkN (CheckIType x te) t TType
         SRHS x          -> infer (ELabelEnd te) x
-        SVar sn i       -> focus_' te exp (Var i, snd $ varType "C2" i te)
-        SLit si l       -> focus_' te exp (ELit l, litType l)
-        STyped et       -> focus_' te exp et
-        SGlobal (SIName si s) -> focus_' te exp =<< getDef te si s
+        SVar sn i       -> focusTell te exp (Var i, snd $ varType "C2" i te)
+        SLit si l       -> focusTell te exp (ELit l, litType l)
+        STyped et       -> focusTell' te exp et
+        SGlobal (SIName si s) -> focusTell te exp =<< getDef te si s
         SLet le a b     -> infer (ELet1 le te b{-in-}) a{-let-} -- infer te SLamV b `SAppV` a)
         SApp_ si h a b  -> infer (EApp1 (si `validate` [sourceInfo a, sourceInfo b]) h te b) a
         SBind_ si h _ a b -> infer ((if h /= BMeta then CheckType_ (sourceInfo exp) TType else id) $ EBind1 si h te $ (if isPi h then TyType else id) b) a
@@ -984,7 +984,7 @@ inferN_ tellTrace = infer  where
         | SRHS x <- e = checkN (ELabelEnd te) x t
         | SApp_ si h a b <- e = infer (CheckAppType si h t te b) a
         | SLam h a b <- e, Pi h' x y <- t, h == h'  = do
-            tellType e t
+--            tellType e t
             let same = checkSame te a x
             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
@@ -1018,7 +1018,8 @@ inferN_ tellTrace = infer  where
     hArgs (Pi Hidden _ b) = 1 + hArgs b
     hArgs _ = 0
 
-    focus_' env si eet = tellType si (snd eet) >> focus_ env eet
+    focusTell env si eet = tellType si (snd eet) >> focus_ env eet
+    focusTell' env si eet = focus_ env eet
 
     focus_ :: Env -> ExpType -> IM m ExpType'
     focus_ env eet@(e, et) = tellTrace "focus" (showEnvExp env eet) $ case env of
@@ -1045,10 +1046,10 @@ inferN_ tellTrace = infer  where
             | hArgs et < hArgs t, Pi Hidden t1 t2 <- t
                             -> focus_ (CheckType_ si t2 $ EBind2 (BLam Hidden) t1 te) eet
             | otherwise    -> focus_ (EBind2_ si BMeta (cstr TType t et) te) $ up 1 eet
-        EApp2 si h (a, at) te    -> focus_' te si (app_ a e, appTy at e)        --  h??
+        EApp2 si h (a, at) te    -> focusTell te si (app_ a e, appTy at e)        --  h??
         EBind1 si h te b   -> infer (EBind2_ (sourceInfo b) h e te) b
         EBind2_ si (BLam h) a te -> focus_ te $ lamPi h a eet
-        EBind2_ si (BPi h) a te -> focus_' te si (Pi h a e, TType)
+        EBind2_ si (BPi h) a te -> focusTell te si (Pi h a e, TType)
         _ -> focus2 env $ MEnd eet
 
     focus2 :: Env -> CEnv ExpType -> IM m ExpType'
@@ -1065,8 +1066,8 @@ inferN_ tellTrace = infer  where
             | CstrT t a b <- tt, Just r <- cst (b, t) a -> r
             | isCstr tt, EBind2 h x te' <- te{-, h /= BMeta todo: remove-}, Just x' <- down 0 tt, x == x'
                             -> refocus te $ subst 1 (Var 0) eet
-            | EBind2 h x te' <- te, h /= BMeta, Just b' <- down 0 tt
-                            -> refocus (EBind2_ si h (up 1 x) $ EBind2_ si BMeta b' te') $ subst 2 (Var 0) $ up 1 eet
+            | EBind2_ si' h x te' <- te, h /= BMeta, Just b' <- down 0 tt
+                            -> refocus (EBind2_ si' h (up 1 x) $ EBind2_ si BMeta b' te') $ subst 2 (Var 0) $ up 1 eet
             | ELet2 le (x, xt) te' <- te, Just b' <- down 0 tt
                             -> refocus (ELet2 le (up 1 x, up 1 xt) $ EBind2_ si BMeta b' te') $ subst 2 (Var 0) $ up 1 eet
             | EBind1 si h te' x <- te -> refocus (EBind1 si h (EBind2_ si BMeta tt_ te') $ up1_ 1 x) eet
@@ -1261,7 +1262,7 @@ initEnv = Map.fromList
 -------------------------------------------------------------------------------- infos
 
 data Info
-    = Info Range String
+    = Info Range Doc
     | IType SIName Exp
     | ITrace String String
     | IError ErrorMsg
@@ -1279,7 +1280,7 @@ instance NFData Info where rnf = rnf . ppShow
 -}
 instance PShow Info where
     pShow = \case
-        Info r s -> shortForm (pShow r) <+> "" <+> text s
+        Info r s -> nest 4 $ shortForm (pShow r) <$$> s
         IType a b -> shAnn (pShow a) (pShow b)
         ITrace i s -> text i <> ": " <+> text s
         IError e -> "!" <> pShow e
@@ -1295,14 +1296,14 @@ mkInfoItem (RangeSI r) i = [Info r i]
 mkInfoItem _ _ = mempty
 
 listAllInfos m = h "trace"  (listTraceInfos m)
-             ++  h "tooltips" [ show (shortForm $ pShow r) ++ "  " ++ intercalate " | " is | (r, is) <- listTypeInfos m ]
-             ++  h "warnings" [ ppShow w | ParseWarning w <- m ]
+             ++  h "tooltips" [ nest 4 $ shortForm (pShow r) <$$> hsep (intersperse "|" is) | (r, is) <- listTypeInfos m ]
+             ++  h "warnings" [ pShow w | ParseWarning w <- m ]
   where
     h x [] = []
-    h x xs = ("------------ " ++ x) : xs
+    h x xs = ("------------" <+> x) : xs
 
-listTraceInfos m = [ppShow i | i <- m, case i of Info{} -> False; ParseWarning{} -> False; _ -> True]
-listTypeInfos m = map (second Set.toList) $ Map.toList $ Map.unionsWith (<>) [Map.singleton r $ Set.singleton i | Info r i <- m]
+listTraceInfos m = [DResetFreshNames $ pShow i | i <- m, case i of Info{} -> False; ParseWarning{} -> False; _ -> True]
+listTypeInfos m = Map.toList $ Map.unionsWith (<>) [Map.singleton r [i] | Info r i <- m]
 
 -------------------------------------------------------------------------------- inference for statements
 
@@ -1346,7 +1347,7 @@ handleStmt = \case
             | c == SGlobal s && take pnum' xs == downToS "a3" (length ctl) pnum'
             = do
                 cty <- removeHiddenUnit <$> inferType (UncurryS [(Hidden, x) | (Visible, x) <- ps] ct)
-                tellType (sourceInfo cn) cty
+--                tellType (sourceInfo cn) cty
                 let     pars = zipWith (\x -> second $ STyped . flip (,) TType . rUp (1+j) x) [0..] $ drop (length ps) $ fst $ getParams cty
                         act = length . fst . getParams $ cty
                         acts = map fst . fst . getParams $ cty
@@ -1451,7 +1452,7 @@ joinEnv e1 e2 = do
 
 downTo n m = map Var [n+m-1, n+m-2..n]
 
-tellType si t = tell $ mkInfoItem (sourceInfo si) $ plainShow $ DTypeNamespace True $ mkDoc False (t, TType)
+tellType si t = tell $ mkInfoItem (sourceInfo si) $ DTypeNamespace True $ mkDoc False (t, TType)
 
 
 -------------------------------------------------------------------------------- pretty print
diff --git a/src/LambdaCube/Compiler/Pretty.hs b/src/LambdaCube/Compiler/Pretty.hs
index 17b64c15..7aba8f77 100644
--- a/src/LambdaCube/Compiler/Pretty.hs
+++ b/src/LambdaCube/Compiler/Pretty.hs
@@ -70,6 +70,7 @@ data Doc
     | DFreshName Bool{-used-} Doc
     | DVar Int
     | DUp Int Doc
+    | DResetFreshNames Doc
 
     | DExpand Doc Doc
 
@@ -106,15 +107,21 @@ instance Show Doc where
 plainShow :: PShow a => a -> String
 plainShow = ($ "") . P.displayS . P.renderPretty 0.6 150 . P.plain . renderDoc . pShow
 
+simpleShow :: PShow a => a -> String
+simpleShow = ($ "") . P.displayS . P.renderPretty 0.4 200 . P.plain . renderDoc . pShow
+
 renderDoc :: Doc -> P.Doc
 renderDoc
     = render
     . addPar False (Infix (-10))
-    . flip runReader ((\s n -> '_': n: s) <$> iterate ('\'':) "" <*> ['a'..'z'])
-    . flip evalStateT (flip (:) <$> iterate ('\'':) "" <*> ['a'..'z'])
+    . flip runReader freeNames
+    . flip evalStateT freshNames
     . showVars
     . expand True
   where
+    freshNames = flip (:) <$> iterate ('\'':) "" <*> ['a'..'z']
+    freeNames = map ('_':) freshNames
+
     noexpand = expand False
     expand full = \case
         DExpand short long -> expand full $ if full then long else short
@@ -125,7 +132,8 @@ renderDoc
         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
+        DFreshName b x -> (if full then DResetFreshNames else id) $ DFreshName b $ noexpand x
+        DResetFreshNames x -> DResetFreshNames $ expand full x
         DUp i x -> DUp i $ noexpand x
 
     showVars = \case
@@ -138,6 +146,10 @@ renderDoc
         DVar i -> asks $ text . (!! i)
         DFreshName True x -> gets head >>= \n -> modify tail >> local (n:) (showVars x)
         DFreshName False x -> local ("_":) $ showVars x
+        DResetFreshNames x -> do
+            st <- get
+            put freshNames
+            local (const freeNames) (showVars x) <* put st
         DUp i x -> local (dropIndex i) $ showVars x
       where
         showVarA (SimpleAtom s) = pure $ SimpleAtom s