From f6c53879ff39bab242cb88a56295856448806424 Mon Sep 17 00:00:00 2001 From: crumbtoo Date: Tue, 26 Mar 2024 12:12:31 -0600 Subject: [PATCH] ppretty tyvars --- app/Server.hs | 3 +- rlp.cabal | 1 - src/Rlp/AltSyntax.hs | 2 +- src/Rlp/HindleyMilner.hs | 76 +++++++++++++++++++++++++++++----------- 4 files changed, 57 insertions(+), 25 deletions(-) diff --git a/app/Server.hs b/app/Server.hs index e38e319..08c3f49 100644 --- a/app/Server.hs +++ b/app/Server.hs @@ -92,8 +92,7 @@ serialiseSc :: (PsName, [Pat PsName], Cofree (RlpExprF PsName) (Type PsName)) serialiseSc (n,as,e) = object [ "name" .= n , "args" .= as - , "body" .= let rootType = extract e - in serialiseAnnotated (e <&> prettyVars rootType) ] + , "body" .= serialiseAnnotated (e <&> renamePrettily) ] serialiseAnnotated :: Cofree (RlpExprF PsName) (Type PsName) -> Value diff --git a/rlp.cabal b/rlp.cabal index 113af03..348b0df 100644 --- a/rlp.cabal +++ b/rlp.cabal @@ -35,7 +35,6 @@ library , Rlp.AltSyntax , Rlp.AltParse , Rlp.HindleyMilner - , Rlp.HindleyMilner2 , Rlp.HindleyMilner.Visual , Rlp.HindleyMilner.Types , Rlp.Syntax.Backstage diff --git a/src/Rlp/AltSyntax.hs b/src/Rlp/AltSyntax.hs index 2f474a2..059f4b9 100644 --- a/src/Rlp/AltSyntax.hs +++ b/src/Rlp/AltSyntax.hs @@ -181,7 +181,7 @@ instance (Out b) => Out (Type b) where outPrec appPrec f <+> outPrec appPrec1 x outPrec p FunT = maybeParens (p>0) "->" outPrec p (ForallT x m) = maybeParens (p>0) $ - hsep [ "∀", ttext x, outPrec 0 m ] + hsep [ "∀", ttext x <> ".", outPrec 0 m ] instance (Out b) => Out (Pat b) where outPrec p (VarP b) = outPrec p b diff --git a/src/Rlp/HindleyMilner.hs b/src/Rlp/HindleyMilner.hs index a0079b8..3d2a472 100644 --- a/src/Rlp/HindleyMilner.hs +++ b/src/Rlp/HindleyMilner.hs @@ -7,8 +7,7 @@ module Rlp.HindleyMilner , runHM' , liftHM , HM - , prettyVars - , prettyVars' + , renamePrettily ) where -------------------------------------------------------------------------------- @@ -98,19 +97,30 @@ gather' = \case t = foldr (:->) te tbs pure (t,j) - Finr (LetEF NonRec [VarB (VarP k) x] e) -> do - ((tx,jx),freeTvs) <- listenFreshTvNames $ gather x - let tx' = generalise freeTvs tx + Finr (LetEF NonRec bs e) -> do + let ks = bs ^.. each . singular _VarB . _1 . singular _VarP + (txs,jxs) <- unzip <$> generaliseGatherBinds bs (te,je) <- gather e - (cs,m) <- elimAssumptionsMap (je ^. assumptions) k tx' - traceM $ "m : " <> show m - let jxcs = jx ^. constraints + (cs,m) <- fmap fold . for (ks `zip` txs) $ \ (k,t) -> + elimAssumptionsMap (je ^. assumptions) k t + let jxcs = jxs ^. each . constraints & each . constraintTypes %~ substMap m - as = H.delete k (je ^. assumptions) + as = foldr H.delete (je ^. assumptions) ks j = mempty & constraints .~ (je ^. constraints <> jxcs <> cs) & assumptions .~ as - traceM $ "jxcs : " <> show jxcs - pure (te, jx <> j) + pure (te, fold jxs <> j) + + -- Finr (LetEF NonRec [VarB (VarP k) x] e) -> do + -- ((tx,jx),freeTvs) <- listenFreshTvNames $ gather x + -- let tx' = generalise freeTvs tx + -- (te,je) <- gather e + -- (cs,m) <- elimAssumptionsMap (je ^. assumptions) k tx' + -- let jxcs = jx ^. constraints + -- & each . constraintTypes %~ substMap m + -- as = H.delete k (je ^. assumptions) + -- j = mempty & constraints .~ (je ^. constraints <> jxcs <> cs) + -- & assumptions .~ as + -- pure (te, jx <> j) -- Finl (LamF [b] e) -> do -- tb <- freshTv @@ -121,6 +131,16 @@ gather' = \case -- t = tb :-> te -- pure (t,j) +generaliseGatherBinds :: [Binding PsName (RlpExpr PsName)] + -> HM [(Type PsName, PartialJudgement)] +generaliseGatherBinds = traverse \b -> + b ^. singular _VarB . _2 & generaliseGather + +generaliseGather :: RlpExpr PsName -> HM (Type PsName, PartialJudgement) +generaliseGather e = do + (a,frees) <- listenFreshTvNames $ gather e + pure $ a & _1 %~ generalise frees + generalise :: [PsName] -> Type PsName -> Type PsName generalise freeTvs t = foldr ForallT t freeTvs @@ -198,17 +218,8 @@ elimAssumptionsMap as b tb = (t',w') <- lift $ instantiateMap t writer (Equality tb' t', w <> w') -substTrace k v t = trace ("subst " <> show' k <> " " <> show' v <> " " <> show' t) - (subst k v t) - where show' a = showsPrec 11 a "" - substMap :: HashMap PsName (Type PsName) -> Type PsName -> Type PsName -substMap m t = ifoldr substTrace t m - -elimAssumptionsGen :: Assumptions -> PsName -> Type PsName -> HM [Constraint] -elimAssumptionsGen as b tb = - as ^. at b . non' _Empty & traverseOf each k - where k t = GeneralisedEquality tb <$> instantiate t +substMap m t = ifoldr subst t m elimAssumptionsG :: Context -> Assumptions -> HM [Constraint] elimAssumptionsG g as @@ -342,3 +353,26 @@ prettyVars root = appEndo (foldMap Endo subs) (freeVariablesLTR root) names +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 + + getName = do + n <- use _head + modify tail + pure n + +alphabetNames :: [PsName] +alphabetNames = alphabet ++ concatMap appendAlphabet alphabetNames + where alphabet = [ T.pack [c] | c <- ['a'..'z'] ] + appendAlphabet c = [ c <> c' | c' <- alphabet ] +