From 0650e1d32d5c007a484bb8399421545b5210cfda Mon Sep 17 00:00:00 2001
From: crumbtoo <crumb@disroot.org>
Date: Tue, 26 Mar 2024 12:41:33 -0600
Subject: [PATCH] rename prettily

---
 app/Server.hs            |  4 +++-
 src/Rlp/HindleyMilner.hs | 38 ++++++++++++++++++++++++++++++--------
 2 files changed, 33 insertions(+), 9 deletions(-)

diff --git a/app/Server.hs b/app/Server.hs
index 08c3f49..07402cf 100644
--- a/app/Server.hs
+++ b/app/Server.hs
@@ -92,7 +92,9 @@ serialiseSc :: (PsName, [Pat PsName], Cofree (RlpExprF PsName) (Type PsName))
 serialiseSc (n,as,e) = object
     [ "name" .= n
     , "args" .= as
-    , "body" .= serialiseAnnotated (e <&> renamePrettily) ]
+    , "body" .= let root = extract e
+                in serialiseAnnotated (e <&> renamePrettily root)
+    ]
 
 serialiseAnnotated :: Cofree (RlpExprF PsName) (Type PsName)
                    -> Value
diff --git a/src/Rlp/HindleyMilner.hs b/src/Rlp/HindleyMilner.hs
index 3d2a472..d3c0333 100644
--- a/src/Rlp/HindleyMilner.hs
+++ b/src/Rlp/HindleyMilner.hs
@@ -238,7 +238,8 @@ infer g0 e = do
         pure (csa <> cs)
     g <- unify cs'
     let sub t = ifoldrOf (reversed . assocs) subst t g
-    pure $ generaliseG g0 <$> sub . view _1 <$> e'
+    pure $ e' & fmap (sub . view _1)
+              & _extract %~ generaliseG g0
   where
     -- intuitively, we'd return mgu(s,t) but the union is left-biased making `s`
     -- the user-specified type: prioritise her.
@@ -353,24 +354,45 @@ prettyVars root = appEndo (foldMap Endo subs)
                        (freeVariablesLTR root)
                        names
 
-renamePrettily :: Type PsName -> Type PsName
-renamePrettily
-    = (`evalState` alphabetNames)
-    . (renameFrees <=< renameForalls)
+renamePrettily' :: Type PsName -> Type PsName
+renamePrettily' = join renamePrettily
+
+renamePrettily :: Type PsName -> Type PsName -> Type PsName
+renamePrettily root = (`evalState` alphabetNames) . (renameFree <=< renameBound)
   where
-    -- TODO:
-    renameFrees root = pure root
-    renameForalls = cata \case
+    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 = do
         n <- use _head
         modify tail
         pure n
 
+-- renamePrettily :: Type PsName -> Type PsName
+-- renamePrettily
+--     = (`evalState` alphabetNames)
+--     . (renameFrees <=< renameForalls)
+--   where
+--     -- TODO:
+--     renameFrees root = pure root
+--     renameForalls = cata \case
+--         ForallTF x m -> do
+--             n <- getName
+--             ForallT n <$> (subst x (VarT n) <$> m)
+--         t -> embed <$> sequenceA t
+
 alphabetNames :: [PsName]
 alphabetNames = alphabet ++ concatMap appendAlphabet alphabetNames
     where alphabet = [ T.pack [c] | c <- ['a'..'z'] ]