rename prettily
This commit is contained in:
@@ -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
|
||||||
|
|||||||
@@ -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'] ]
|
||||||
|
|||||||
Reference in New Issue
Block a user