From b9762ddb10a96988403a9f1a086ed6595c76a3db Mon Sep 17 00:00:00 2001
From: Joscha <joscha@plugh.de>
Date: Thu, 26 Nov 2020 19:03:22 +0100
Subject: [PATCH] Correctly display terms

---
 package.yaml                |  1 +
 props.cabal                 |  4 ++-
 src/Props/Lambda/Display.hs | 55 +++++++++++++++++++++++++++++++++----
 3 files changed, 53 insertions(+), 7 deletions(-)

diff --git a/package.yaml b/package.yaml
index 5062cc2..b6c0015 100644
--- a/package.yaml
+++ b/package.yaml
@@ -15,6 +15,7 @@ dependencies:
 - base >= 4.7 && < 5
 - containers
 - text
+- transformers
 
 library:
   source-dirs: src
diff --git a/props.cabal b/props.cabal
index d0e1c22..ef355c2 100644
--- a/props.cabal
+++ b/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
diff --git a/src/Props/Lambda/Display.hs b/src/Props/Lambda/Display.hs
index 3197aa5..6184da4 100644
--- a/src/Props/Lambda/Display.hs
+++ b/src/Props/Lambda/Display.hs
@@ -5,12 +5,15 @@ module Props.Lambda.Display
   , makeVarNamesUnique
   , findVarNames
   , displayTerm
+  , displayTerm'
   ) where
 
 import           Data.Maybe
 import           Numeric.Natural
 
-import qualified Data.Text         as T
+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 = id -- TODO implement
+makeVarNamesUnique :: Term e Name (Maybe Name) -> Term e Name (Maybe Name)
+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 = mapVars (fromMaybe "[]") -- TODO implement
+findVarNames :: Term e Name (Maybe Name) -> Term e Name Name
+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