4 files changed, 44 insertions, 20 deletions

diff --git a/src/LambdaCube/Compiler/Core.hs b/src/LambdaCube/Compiler/Core.hs
index b6a1c1c4..181d07e8 100644
--- a/src/LambdaCube/Compiler/Core.hs
+++ b/src/LambdaCube/Compiler/Core.hs
@@ -412,9 +412,9 @@ instance MkDoc ExpType where
 
 instance MkDoc Exp where
     mkDoc pr@(reduce, body) = \case
-        Lam b           -> shLam_ (usedVar 0 b) (BLam Visible) Nothing (mkDoc pr b)
-        Pi h TType b    -> shLam_ (usedVar 0 b) (BPi h) Nothing (mkDoc pr b)
-        Pi h a b        -> shLam (usedVar 0 b) (BPi h) (mkDoc pr a) (mkDoc pr b)
+        Lam b           -> shLam_ (usedVar' 0 b "") (BLam Visible) Nothing (mkDoc pr b)
+        Pi h TType b    -> shLam_ (usedVar' 0 b "") (BPi h) Nothing (mkDoc pr b)
+        Pi h a b        -> shLam (usedVar' 0 b "") (BPi h) (mkDoc pr a) (mkDoc pr b)
         ENat n          -> pShow n
         Con s@(ConName _ i _) _ _ | body -> text $ "<<" ++ showNth i ++ " constructor of " ++ show (conTypeName s) ++ ">>"
         ConN FHCons (xs: x: _{-2-}) -> foldl DApp (text "HCons") (mkDoc pr <$> [x, xs])
diff --git a/src/LambdaCube/Compiler/DesugaredSource.hs b/src/LambdaCube/Compiler/DesugaredSource.hs
index db2c1f24..7bb5ba96 100644
--- a/src/LambdaCube/Compiler/DesugaredSource.hs
+++ b/src/LambdaCube/Compiler/DesugaredSource.hs
@@ -298,7 +298,7 @@ instance PShow Visibility where
         Hidden -> "Hidden"
         Visible -> "Visible"
 
-dummyName s = SIName (debugSI s) ("v_" ++ s)
+dummyName s = SIName (debugSI s) "" --("v_" ++ s)
 dummyName' = SData . dummyName
 sVar = SVar . dummyName
 
@@ -476,8 +476,8 @@ instance (HasFreeVars a, PShow a) => PShow (SExp' a) where
         SApp h a b      -> shApp h (pShow a) (pShow b)
         Wildcard SType  -> text "_"
         Wildcard t      -> shAnn (text "_") (pShow t)
-        SBind_ _ h _ SType b -> shLam_ (usedVar 0 b) h Nothing (pShow b)
-        SBind_ _ h _ a b -> shLam (usedVar 0 b) h (pShow a) (pShow b)
+        SBind_ _ h (SData n) SType b -> shLam_ (usedVar' 0 b $ sName n) h Nothing (pShow b)
+        SBind_ _ h (SData n) a b -> shLam (usedVar' 0 b $ sName n) h (pShow a) (pShow b)
         SLet _ a b      -> shLet_ (pShow a) (pShow b)
         SLHS n x        -> "_lhs" `DApp` pShow n `DApp` pShow x
         STyped a        -> pShow a
@@ -487,12 +487,15 @@ instance (HasFreeVars a, PShow a) => PShow (SExp' a) where
 shApp Visible a b = DApp a b
 shApp Hidden a b = DApp a (DAt b)
 
+usedVar' a b s | usedVar a b = Just s
+               | otherwise = Nothing
+
 shLam usedVar h a b = shLam_ usedVar h (Just 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
+shLam_ Nothing (BPi Hidden) (Just ((simpleFo -> DText "'CW") `DApp` a)) b = DFreshName Nothing $ 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
@@ -503,10 +506,10 @@ shLam_ usedVar h a b = DFreshName usedVar $ lam (p $ DUp 0 <$> a) b
   where
     lam = case h of
         BPi Visible
-            | usedVar   -> showForall "->"
+            | isJust usedVar   -> showForall "->"
             | otherwise -> shArr
         BPi Hidden
-            | usedVar   -> showForall "."
+            | isJust usedVar   -> showForall "."
             | otherwise -> showContext
         _ -> showLam
 
@@ -518,7 +521,7 @@ shLam_ usedVar h a b = DFreshName usedVar $ lam (p $ DUp 0 <$> a) b
         BLam Visible -> shAnn' (DVar 0)
         _ -> ann
 
-    ann | usedVar = shAnn' (DVar 0)
+    ann | isJust usedVar = shAnn' (DVar 0)
         | otherwise = fromMaybe (text "Type")
 
     showForall s x (DFreshName u d) = DFreshName u $ showForall s (DUp 0 x) d
@@ -537,7 +540,7 @@ 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
+shLet_ a b = DFreshName (Just "") $ showLet (DLet "=" (shVar 0) $ DUp 0 a) b
 
 -------------------------------------------------------------------------------- statement
 
diff --git a/src/LambdaCube/Compiler/Infer.hs b/src/LambdaCube/Compiler/Infer.hs
index 5067487c..f2889dd0 100644
--- a/src/LambdaCube/Compiler/Infer.hs
+++ b/src/LambdaCube/Compiler/Infer.hs
@@ -83,8 +83,8 @@ showEnvSExpType e c t = show $ envDoc e $ underline $ (shAnn (pShow c) (pShow t)
 envDoc :: Env -> Doc -> Doc
 envDoc x m = case x of
     EGlobal{}           -> m
-    EBind1 _ h ts b     -> envDoc ts $ shLam (usedVar 0 b) h m (pShow b)
-    EBind2 h a ts       -> envDoc ts $ shLam True h (pShow a) m
+    EBind1 _ h ts b     -> envDoc ts $ shLam (usedVar' 0 b "") h m (pShow b)
+    EBind2 h a ts       -> envDoc ts $ shLam (Just "") h (pShow a) m
     EApp1 _ h ts b      -> envDoc ts $ shApp h m (pShow b)
     EApp2 _ h (ET (Lam (Var 0)) (Pi Visible TType _)) ts -> envDoc ts $ shApp h (text "tyType") m
     EApp2 _ h a ts      -> envDoc ts $ shApp h (pShow a) m
@@ -102,7 +102,7 @@ envDoc x m = case x of
 instance MkDoc a => MkDoc (CEnv a) where
     mkDoc pr = \case
         MEnd a          -> mkDoc pr a
-        Meta a b        -> shLam True BMeta (mkDoc pr a) (mkDoc pr b)
+        Meta a b        -> shLam (Just "") BMeta (mkDoc pr a) (mkDoc pr b)
         Assign i (ET x _) e -> shLet i (mkDoc pr x) (mkDoc pr e)
 
 -------------------------------------------------------------------------------- constraints env
diff --git a/src/LambdaCube/Compiler/Pretty.hs b/src/LambdaCube/Compiler/Pretty.hs
index 12964b6b..a82f7ce6 100644
--- a/src/LambdaCube/Compiler/Pretty.hs
+++ b/src/LambdaCube/Compiler/Pretty.hs
@@ -18,7 +18,7 @@ import Data.String
 import Data.Char
 import Data.Monoid
 import qualified Data.Set as Set
---import qualified Data.Map as Map
+import qualified Data.Map.Strict as Map
 import Control.Applicative
 import Control.Monad.Identity
 import Control.Monad.Reader
@@ -71,7 +71,7 @@ data Doc
     | DInfix Fixity Doc DocAtom Doc
     | DPreOp Int DocAtom Doc
 
-    | DFreshName Bool{-used-} Doc
+    | DFreshName (Maybe String){-used-} Doc
     | DVar Int
     | DUp Int Doc
     | DResetFreshNames Doc
@@ -104,6 +104,16 @@ plainShow = ($ "") . P.displayS . P.renderPretty 0.6 150 . P.plain . renderDoc .
 simpleShow :: PShow a => a -> String
 simpleShow = ($ "") . P.displayS . P.renderPretty 0.4 200 . P.plain . renderDoc . pShow
 
+mkFreshName :: MonadState (Map.Map String Int, [String]) m => String -> m String
+mkFreshName n = state $ addIndex n
+  where
+    addIndex "" (m, (n:ns)) = add n (m, ns)
+    addIndex n (m, ns) = add n (m, ns)
+
+    add n (m, ns) = case Map.lookup n m of
+        Just i -> (n ++ (toSubscript <$> show (i+1)), (Map.insert n (i+1) m, ns))
+        Nothing -> (n, (Map.insert n 0 m, ns))
+
 renderDoc :: Doc -> P.Doc
 renderDoc
     = render
@@ -114,8 +124,8 @@ renderDoc
     . showVars
     . expand True
   where
-    freshNames = flip (:) <$> iterate ('\'':) "" <*> ['a'..'z']
-    freeNames = map ('_':) freshNames
+    freshNames = (mempty, cycle $ (:[]) <$> ['a'..'z'])
+    freeNames = map ('_':) $ flip (:) <$> iterate ('\'':) "" <*> ['a'..'z']
 
     noexpand = expand False
     expand full = \case
@@ -139,8 +149,8 @@ renderDoc
         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
+        DFreshName (Just n) x -> mkFreshName n >>= \n -> local (n:) (showVars x)
+        DFreshName Nothing x -> local ("_":) $ showVars x
         DResetFreshNames x -> do
             st <- get
             put freshNames
@@ -421,3 +431,14 @@ showNth n = show n ++ f (n `div` 10 `mod` 10) (n `mod` 10)
     f _ 3 = "rd"
     f _ _ = "th"
 
+toSubscript '0' = '₀'
+toSubscript '1' = '₁'
+toSubscript '2' = '₂'
+toSubscript '3' = '₃'
+toSubscript '4' = '₄'
+toSubscript '5' = '₅'
+toSubscript '6' = '₆'
+toSubscript '7' = '₇'
+toSubscript '8' = '₈'
+toSubscript '9' = '₉'
+toSubscript _ = error "toSubscript"