rename prettily

This commit is contained in:
crumbtoo
2024-03-26 12:41:33 -06:00
parent ed353f02ab
commit f56990a59a
2 changed files with 33 additions and 9 deletions

View File

@@ -92,7 +92,9 @@ serialiseSc :: (PsName, [Pat PsName], Cofree (RlpExprF PsName) (Type PsName))
serialiseSc (n,as,e) = object serialiseSc (n,as,e) = object
[ "name" .= n [ "name" .= n
, "args" .= as , "args" .= as
, "body" .= serialiseAnnotated (e <&> renamePrettily) ] , "body" .= let root = extract e
in serialiseAnnotated (e <&> renamePrettily root)
]
serialiseAnnotated :: Cofree (RlpExprF PsName) (Type PsName) serialiseAnnotated :: Cofree (RlpExprF PsName) (Type PsName)
-> Value -> Value

View File

@@ -238,7 +238,8 @@ infer g0 e = do
pure (csa <> cs) pure (csa <> cs)
g <- unify cs' g <- unify cs'
let sub t = ifoldrOf (reversed . assocs) subst t g 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 where
-- intuitively, we'd return mgu(s,t) but the union is left-biased making `s` -- intuitively, we'd return mgu(s,t) but the union is left-biased making `s`
-- the user-specified type: prioritise her. -- the user-specified type: prioritise her.
@@ -353,24 +354,45 @@ prettyVars root = appEndo (foldMap Endo subs)
(freeVariablesLTR root) (freeVariablesLTR root)
names names
renamePrettily :: Type PsName -> Type PsName renamePrettily' :: Type PsName -> Type PsName
renamePrettily renamePrettily' = join renamePrettily
= (`evalState` alphabetNames)
. (renameFrees <=< renameForalls) renamePrettily :: Type PsName -> Type PsName -> Type PsName
renamePrettily root = (`evalState` alphabetNames) . (renameFree <=< renameBound)
where where
-- TODO: renameBound :: Type PsName -> State [PsName] (Type PsName)
renameFrees root = pure root renameBound = cata \case
renameForalls = cata \case
ForallTF x m -> do ForallTF x m -> do
n <- getName n <- getName
ForallT n <$> (subst x (VarT n) <$> m) ForallT n <$> (subst x (VarT n) <$> m)
t -> embed <$> sequenceA t 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 getName = do
n <- use _head n <- use _head
modify tail modify tail
pure n 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 :: [PsName]
alphabetNames = alphabet ++ concatMap appendAlphabet alphabetNames alphabetNames = alphabet ++ concatMap appendAlphabet alphabetNames
where alphabet = [ T.pack [c] | c <- ['a'..'z'] ] where alphabet = [ T.pack [c] | c <- ['a'..'z'] ]