Correctly display terms

package.yaml

@@ -15,6 +15,7 @@ dependencies:
 - base >= 4.7 && < 5
 - containers
 - text
+- transformers
 
 library:
   source-dirs: src

props.cabal

@@ -4,7 +4,7 @@ cabal-version: 1.18
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: 5a5ea1f94c0aefd4530bcfe91d7e5265b092b9e1b361d21bef695382fe4422a5
+-- hash: 03958e185b40527fc635759af663a90da5cd82cead9a9fd30ce5ab3e91b53f83
 
 name:           props
 version:        0.1.0.0
@@ -32,6 +32,7 @@ library
       base >=4.7 && <5
     , containers
     , text
+    , transformers
   default-language: Haskell2010
 
 executable props
@@ -46,4 +47,5 @@ executable props
     , containers
     , props
     , text
+    , transformers
   default-language: Haskell2010

src/Props/Lambda/Display.hs

@@ -5,11 +5,14 @@ module Props.Lambda.Display
   , makeVarNamesUnique
   , findVarNames
   , displayTerm
+  , displayTerm'
   ) where
 
 import           Data.Maybe
 import           Numeric.Natural
 
+import           Control.Monad.Trans.State
+import qualified Data.Set                  as Set
 import qualified Data.Text                 as T
 
 import           Props.Lambda.Term
@@ -26,18 +29,58 @@ constNames = chars ++ (mappend <$> constNames <*> chars)
   where
     chars = map T.singleton ['A'..'Z']
 
+chooseUnique :: (Ord a) => Set.Set a -> [a] -> a
+chooseUnique taken = head . dropWhile (`Set.member` taken)
+
+makeNameUnique :: Set.Set Name -> Name -> Name
+makeNameUnique taken name
+  = chooseUnique taken
+  $ zipWith (<>) (repeat name)
+  $ "" : map (T.pack . show) [(2::Integer) ..]
+
 findConstNames :: Term e (Maybe Name) v -> Term e Name v
-findConstNames = mapConsts (fromMaybe "[]") -- TODO implement
+findConstNames term = evalState (helper term) (Set.fromList $ catMaybes $ consts term)
+  where
+    helper (Var i) = pure $ Var i
+    helper (Const c) = do
+      taken <- get
+      let name = fromMaybe (chooseUnique taken constNames) c
+      put $ Set.insert name taken
+      pure $ Const name
+    helper (Lambda v t) = Lambda v <$> helper t
+    helper (App l r) = App <$> helper l <*> helper r
+    helper (Ext e) = pure $ Ext e
 
-makeVarNamesUnique :: Term e c (Maybe Name) -> Term e c (Maybe Name)
+makeVarNamesUnique :: Term e Name (Maybe Name) -> Term e Name (Maybe Name)
-makeVarNamesUnique = id -- TODO implement
+makeVarNamesUnique term = helper (Set.fromList $ consts term) term
+  where
+    helper _     (Var i) = Var i
+    helper _     (Const c) = Const c
+    helper taken (Lambda v t) = case v of
+      Nothing -> Lambda Nothing $ helper taken t
+      Just name ->
+        let newName = makeNameUnique taken name
+        in  Lambda (Just newName) $ helper (Set.insert name taken) t
+    helper taken (App l r) = App (helper taken l) (helper taken r)
+    helper _     (Ext e) = Ext e
 
-findVarNames :: Term e c (Maybe Name) -> Term e c Name
+findVarNames :: Term e Name (Maybe Name) -> Term e Name Name
-findVarNames = mapVars (fromMaybe "[]") -- TODO implement
+findVarNames term = helper (Set.fromList $ consts term) term
+  where
+    helper _     (Var i) = Var i
+    helper _     (Const c) = Const c
+    helper taken (Lambda v t) =
+      let name = fromMaybe (chooseUnique taken varNames) v
+      in  Lambda name $ helper (Set.insert name taken) t
+    helper taken (App l r) = App (helper taken l) (helper taken r)
+    helper _     (Ext e) = Ext e
 
 displayTerm :: (e -> T.Text) -> Term e Name Name -> T.Text
 displayTerm f = dTerm f []
 
+displayTerm' :: (e -> T.Text) -> Term e (Maybe Name) (Maybe Name) -> T.Text
+displayTerm' f = displayTerm f . findVarNames . makeVarNamesUnique . findConstNames
+
 nth :: [a] -> Natural -> Maybe a
 nth []     _ = Nothing
 nth (x:_)  0 = Just x