From fbd5ddbe9bacdd37e0740c1e969e1c9a6ec5d430 Mon Sep 17 00:00:00 2001
From: crumbtoo <crumb@disroot.org>
Date: Thu, 4 Apr 2024 13:23:55 -0600
Subject: [PATCH] renamePrettily

---
 src/Rlp/HindleyMilner.hs | 37 ++++++++++++++++++++++++++++++++++++-
 1 file changed, 36 insertions(+), 1 deletion(-)

diff --git a/src/Rlp/HindleyMilner.hs b/src/Rlp/HindleyMilner.hs
index 8418cfb..dd610be 100644
--- a/src/Rlp/HindleyMilner.hs
+++ b/src/Rlp/HindleyMilner.hs
@@ -285,5 +285,40 @@ programDefs k (Program ds) = Program <$> go k ds where
 
 --------------------------------------------------------------------------------
 
-renamePrettily a = id
+renamePrettily' :: Type PsName -> Type PsName
+renamePrettily' = join renamePrettily
+
+-- | for some type, compute a substitution which will rename all free variables
+-- for aesthetic purposes
+
+renamePrettily :: Type PsName -> Type PsName -> Type PsName
+renamePrettily root = (`evalState` alphabetNames) . (renameFree <=< renameBound)
+  where
+    renameBound :: Type PsName -> State [PsName] (Type PsName)
+    renameBound = cata \case
+        ForallTF x m -> do
+            n <- getName
+            ForallT n <$> (subst x (VarT n) <$> m)
+        t -> embed <$> sequenceA t
+
+    renameFree :: Type PsName -> State [PsName] (Type PsName)
+    renameFree t = do
+        subs <- forM (freeVariablesLTR root) $ \v -> do
+            n <- getName
+            pure $ Endo (subst v (VarT n))
+        pure . appEndo (fold subs) $ t
+
+    getName :: State [PsName] PsName
+    getName = state (fromJust . uncons)
+
+alphabetNames :: [PsName]
+alphabetNames = alphabet ++ concatMap appendAlphabet alphabetNames
+    where alphabet = [ T.pack [c] | c <- ['a'..'z'] ]
+          appendAlphabet c = [ c <> c' | c' <- alphabet ]
+
+freeVariablesLTR :: Type PsName -> [PsName]
+freeVariablesLTR = nub . cata \case
+    VarTF x -> [x]
+    ForallTF x m -> m \\ [x]
+    vs -> concat vs