From dd600a835133a7f53e603d6e11d37fa5e60fab26 Mon Sep 17 00:00:00 2001 From: crumbtoo Date: Wed, 20 Mar 2024 15:46:23 -0600 Subject: [PATCH] context --- .ghci | 1 + rlp.cabal | 1 + src/Core/SystemF.hs | 1 + src/Rlp/AltParse.y | 1 + src/Rlp/AltSyntax.hs | 15 ++++-- src/Rlp/HindleyMilner.hs | 99 ++++++++-------------------------- src/Rlp/HindleyMilner/Types.hs | 4 +- src/Rlp/Lex.x | 3 +- src/Rlp/Parse/Types.hs | 1 + src/Rlp2Core.hs | 70 +++++++++++++++--------- 10 files changed, 89 insertions(+), 107 deletions(-) diff --git a/.ghci b/.ghci index 75be915..91dc968 100644 --- a/.ghci +++ b/.ghci @@ -1,5 +1,6 @@ -- repl extensions :set -XOverloadedStrings +:set -XQuasiQuotes -------------------------------------------------------------------------------- diff --git a/rlp.cabal b/rlp.cabal index 66b3f5a..7e300d6 100644 --- a/rlp.cabal +++ b/rlp.cabal @@ -76,6 +76,7 @@ library , text >= 2.0.2 && < 2.2 , unordered-containers >= 0.2.20 && < 0.3 , recursion-schemes >= 5.2.2 && < 5.3 + , monadic-recursion-schemes , data-fix >= 0.3.2 && < 0.4 , utf8-string >= 1.0.2 && < 1.1 , extra >= 1.7.0 && <2 diff --git a/src/Core/SystemF.hs b/src/Core/SystemF.hs index 0e8c17d..8180dbd 100644 --- a/src/Core/SystemF.hs +++ b/src/Core/SystemF.hs @@ -2,6 +2,7 @@ {-# LANGUAGE OverloadedLists #-} module Core.SystemF ( lintCoreProgR + , kindOf ) where -------------------------------------------------------------------------------- diff --git a/src/Rlp/AltParse.y b/src/Rlp/AltParse.y index 87f3b0b..83c5f30 100644 --- a/src/Rlp/AltParse.y +++ b/src/Rlp/AltParse.y @@ -60,6 +60,7 @@ import Core.Syntax qualified as Core let { Located _ TokenLet } letrec { Located _ TokenLetrec } in { Located _ TokenIn } + forall { Located _ TokenForall } %nonassoc '=' %right '->' diff --git a/src/Rlp/AltSyntax.hs b/src/Rlp/AltSyntax.hs index 4f0529f..7207613 100644 --- a/src/Rlp/AltSyntax.hs +++ b/src/Rlp/AltSyntax.hs @@ -7,6 +7,7 @@ module Rlp.AltSyntax , DataCon(..), Type(..) , pattern IntT + , AnnotatedRlpExpr, TypedRlpExpr , TypeF(..) , Core.Name, PsName @@ -49,6 +50,10 @@ import Compiler.Types import Core.Syntax qualified as Core -------------------------------------------------------------------------------- +type AnnotatedRlpExpr b = Cofree (RlpExprF b) + +type TypedRlpExpr b = Cofree (RlpExprF b) (Type b) + type PsName = T.Text newtype Program b a = Program [Decl b a] @@ -58,15 +63,15 @@ programDecls :: Lens' (Program b a) [Decl b a] programDecls = lens (\ (Program ds) -> ds) (const Program) data Decl b a = FunD b [Pat b] a - | DataD b [b] [DataCon b] - | TySigD b (Type b) + | DataD Core.Name [Core.Name] [DataCon b] + | TySigD Core.Name (Type b) deriving (Show, Functor, Foldable, Traversable) -data DataCon b = DataCon b [Type b] +data DataCon b = DataCon Core.Name [Type b] deriving (Show, Generic) -data Type b = VarT b - | ConT b +data Type b = VarT Core.Name + | ConT Core.Name | AppT (Type b) (Type b) | FunT | ForallT b (Type b) diff --git a/src/Rlp/HindleyMilner.hs b/src/Rlp/HindleyMilner.hs index 749551e..aa1d568 100644 --- a/src/Rlp/HindleyMilner.hs +++ b/src/Rlp/HindleyMilner.hs @@ -1,7 +1,5 @@ -{-# LANGUAGE ParallelListComp #-} {-# LANGUAGE PartialTypeSignatures #-} {-# LANGUAGE OverloadedLists #-} -{-# LANGUAGE TemplateHaskell #-} module Rlp.HindleyMilner ( typeCheckRlpProgR , annotate @@ -34,7 +32,7 @@ import Data.HashSet (HashSet) import Data.HashSet qualified as S import Data.Maybe (fromMaybe) import Data.Traversable -import GHC.Generics (Generic(..), Generically(..)) +import GHC.Generics (Generic, Generically(..)) import Debug.Trace import Data.Functor @@ -89,16 +87,13 @@ gather' = \case Finl (LamF bs e) -> do tbs <- for bs (const freshTv) (te,je) <- gather e - let cs = concatMap (uncurry . equals $ je ^. assumptions) $ bs `zip` tbs + let cs = bs `zip` tbs + & concatMap (uncurry $ elimAssumptions (je ^. assumptions)) as = foldr H.delete (je ^. assumptions) bs j = mempty & constraints .~ (je ^. constraints <> cs) & assumptions .~ as t = foldr (:->) te tbs pure (t,j) - where - equals as b tb = maybe [] - (fmap $ Equality tb) - (as ^. at b) -- Finl (LamF [b] e) -> do -- tb <- freshTv @@ -109,7 +104,7 @@ gather' = \case -- t = tb :-> te -- pure (t,j) -unify :: [Constraint] -> HM Context +unify :: [Constraint] -> HM [(PsName, Type PsName)] unify [] = pure mempty @@ -122,7 +117,7 @@ unify (Equality (VarT s) (VarT t) : cs) | s == t = unify cs unify (Equality (VarT s) t : cs) | occurs s t = addFatal $ TyErrRecursiveType s t - | otherwise = unify cs' <&> contextVars . at s ?~ t + | otherwise = unify cs' <&> ((s,t):) where cs' = cs & each . constraintTypes %~ subst s t @@ -131,46 +126,10 @@ unify (Equality s (VarT t) : cs) = unify (Equality (VarT t) s : cs) unify (Equality s t : _) = addFatal $ TyErrCouldNotUnify s t -unify' :: [Constraint] -> HM [(PsName, Type PsName)] - -unify' [] = pure mempty - -unify' (Equality (sx :-> sy) (tx :-> ty) : cs) = - unify' $ Equality sx tx : Equality sy ty : cs - --- elim -unify' (Equality (ConT s) (ConT t) : cs) | s == t = unify' cs -unify' (Equality (VarT s) (VarT t) : cs) | s == t = unify' cs - -unify' (Equality (VarT s) t : cs) - | occurs s t = addFatal $ TyErrRecursiveType s t - | otherwise = unify' cs' <&> ((s,t):) - where - cs' = cs & each . constraintTypes %~ subst s t - --- swap -unify' (Equality s (VarT t) : cs) = unify' (Equality (VarT t) s : cs) - -unify' (Equality s t : _) = addFatal $ TyErrCouldNotUnify s t - annotate :: RlpExpr PsName -> HM (Cofree (RlpExprF PsName) (Type PsName, PartialJudgement)) annotate = sequenceA . fixtend (gather . wrapFix) --- infer1 :: RlpExpr PsName -> HM (Type PsName) --- infer1 = infer1' mempty - --- infer1' :: Context -> RlpExpr PsName -> HM (Type PsName) --- infer1' g1 e = do --- ((t,j) :< _) <- annotate e --- g2 <- unify (j ^. constraints) --- g <- unionContextWithKeyM unifyTypes g1 g2 --- pure $ ifoldrOf (contextVars . itraversed) subst t g --- where --- -- intuitively, we'd return mgu(s,t) but the union is left-biased making `s` --- -- the user-specified type: prioritise her. --- unifyTypes _ s t = unify [Equality s t] $> s - assocs :: IndexedTraversal k [(k,v)] [(k,v')] v v' assocs f [] = pure [] assocs f ((k,v):xs) = (\v' xs' -> (k,v') : xs') @@ -180,30 +139,32 @@ traceSubst k v t = trace ("subst " <> show' k <> " " <> show' v <> " " <> show' $ subst k v t where show' a = showsPrec 11 a mempty +elimAssumptions :: Assumptions -> PsName -> Type PsName -> [Constraint] +-- elimAssumptions b tb as = maybe [] (fmap $ Equality tb) (as ^. at b) +elimAssumptions as b tb = + as ^. at b . non' _Empty & each %~ Equality tb + +elimAssumptionsG :: Context -> Assumptions -> [Constraint] +elimAssumptionsG g as = + iconcatMapOf (contextVars . itraversed) (elimAssumptions as) g + infer :: Context -> RlpExpr PsName -> HM (Cofree (RlpExprF PsName) (Type PsName)) -infer g1 e = do +infer g0 e = do e' <- annotate e - g2 <- unify' $ concatOf (folded . _2 . constraints) e' - traceM $ "e': " <> show (view _1 <$> e') - traceM $ "g2: " <> show g2 - let sub t = ifoldrOf (reversed . assocs) traceSubst t g2 + let (as, concat -> cs) = unzip $ e' ^.. folded . _2 + . lensProduct assumptions constraints + cs' = concatMap (elimAssumptionsG g0) as <> cs + g <- unify cs' + let sub t = ifoldrOf (reversed . assocs) subst t g pure $ sub . view _1 <$> e' where -- intuitively, we'd return mgu(s,t) but the union is left-biased making `s` -- the user-specified type: prioritise her. unifyTypes _ s t = unify [Equality s t] $> s -e :: Cofree (RlpExprF PsName) (Type PsName) -e = AppT (AppT FunT (VarT "$a2")) (AppT (AppT FunT (VarT "$a3")) (VarT "$a4")) :< InL (LamF ["f","x"] (VarT "$a4" :< InL (AppF (VarT "$a5" :< InL (VarF "f")) (VarT "$a6" :< InL (AppF (VarT "$a5" :< InL (VarF "f")) (VarT "$a1" :< InL (VarF "x"))))))) - -g = Context - { _contextVars = H.fromList - [("$a1",VarT "$a6") - ,("$a3",VarT "$a4") - ,("$a2",AppT (AppT FunT (VarT "$a4")) (VarT "$a4")) - ,("$a5",AppT (AppT FunT (VarT "$a1")) (VarT "$a6")) - ,("$a6",VarT "$a4")]} +infer1 :: Context -> RlpExpr PsName -> HM (Type PsName) +infer1 g = fmap extract . infer g unionContextWithKeyM :: Monad m => (PsName -> Type PsName -> Type PsName @@ -251,13 +212,6 @@ prettyHM = over (mapped . _1) rout fixtend :: Functor f => (f (Fix f) -> b) -> Fix f -> Cofree f b fixtend c (Fix f) = c f :< fmap (fixtend c) f --- infer :: RlpExpr PsName -> HM (Cofree (RlpExprF PsName) (Type PsName)) --- infer = infer' mempty - --- infer' :: Context -> RlpExpr PsName --- -> HM (Cofree (RlpExprF PsName) (Type PsName)) --- infer' g = sequenceA . fixtend (infer1' g . wrapFix) - buildInitialContext :: Program PsName a -> Context buildInitialContext = Context . H.fromList . toListOf (programDecls . each . _TySigD) @@ -265,7 +219,7 @@ buildInitialContext = typeCheckRlpProgR :: (Monad m) => Program PsName (RlpExpr PsName) -> RLPCT m (Program PsName - (Cofree (RlpExprF PsName) (Type PsName))) + (TypedRlpExpr PsName)) typeCheckRlpProgR p = tc p where g = buildInitialContext p @@ -318,10 +272,3 @@ prettyVars root = appEndo (foldMap Endo subs) (freeVariablesLTR root) names --- test :: Type PsName -> [(PsName, PsName)] --- test root = subs --- where --- alphabetNames = [ T.pack [c] | c <- ['a'..'z'] ] --- names = alphabetNames \\ S.toList (boundVariables root) --- subs = zip (freeVariablesLTR root) names - diff --git a/src/Rlp/HindleyMilner/Types.hs b/src/Rlp/HindleyMilner/Types.hs index 95576ef..db08d19 100644 --- a/src/Rlp/HindleyMilner/Types.hs +++ b/src/Rlp/HindleyMilner/Types.hs @@ -36,9 +36,11 @@ newtype Context = Context data Constraint = Equality (Type PsName) (Type PsName) deriving (Eq, Generic, Show) +type Assumptions = HashMap PsName [Type PsName] + data PartialJudgement = PartialJudgement { _constraints :: [Constraint] - , _assumptions :: HashMap PsName [Type PsName] + , _assumptions :: Assumptions } deriving (Generic, Show) deriving (Monoid) diff --git a/src/Rlp/Lex.x b/src/Rlp/Lex.x index d8884aa..314b08e 100644 --- a/src/Rlp/Lex.x +++ b/src/Rlp/Lex.x @@ -59,7 +59,7 @@ $asciisym = [\!\#\$\%\&\*\+\.\/\<\=\>\?\@\\\^\|\-\~\:] @reservedname = case|data|do|import|in|let|letrec|module|of|where - |infixr|infixl|infix + |infixr|infixl|infix|forall @reservedop = "=" | \\ | "->" | "|" | ":" @@ -163,6 +163,7 @@ lexReservedName = \case "infix" -> TokenInfix "infixl" -> TokenInfixL "infixr" -> TokenInfixR + "forall" -> TokenForall s -> error (show s) lexReservedOp :: Text -> RlpToken diff --git a/src/Rlp/Parse/Types.hs b/src/Rlp/Parse/Types.hs index a138a77..29b546b 100644 --- a/src/Rlp/Parse/Types.hs +++ b/src/Rlp/Parse/Types.hs @@ -109,6 +109,7 @@ data RlpToken | TokenInfixL | TokenInfixR | TokenInfix + | TokenForall -- reserved ops | TokenArrow | TokenPipe diff --git a/src/Rlp2Core.hs b/src/Rlp2Core.hs index 2f3d551..9a3b3f2 100644 --- a/src/Rlp2Core.hs +++ b/src/Rlp2Core.hs @@ -12,8 +12,7 @@ import Control.Monad.Writer.CPS import Control.Monad.Utils import Control.Arrow import Control.Applicative -import Control.Comonad -import Control.Lens +import Control.Lens hiding ((:<)) import Compiler.RLPC import Data.List (mapAccumL, partition) import Data.Text (Text) @@ -22,14 +21,18 @@ import Data.HashMap.Strict qualified as H import Data.Monoid (Endo(..)) import Data.Either (partitionEithers) import Data.Foldable -import Data.Fix import Data.Maybe (fromJust, fromMaybe) -import Data.Functor.Bind import Data.Function (on) import GHC.Stack import Debug.Trace import Numeric +import Data.Fix hiding (cata, para, cataM) +import Data.Functor.Bind +import Data.Functor.Foldable +import Data.Functor.Foldable.Monadic +import Control.Comonad + import Effectful.State.Static.Local import Effectful.Labeled import Effectful @@ -59,45 +62,64 @@ deriveShow1 ''Branch -------------------------------------------------------------------------------- -desugarRlpProgR :: forall m a. (Monad m) - => Rlp.Program PsName a - -> RLPCT m Core.Program' -desugarRlpProgR p = do - let p' = desugarRlpProg p - addDebugMsg "dump-desugared" $ show (out p') - pure p' +-- desugarRlpProgR :: forall m a. (Monad m) +-- => Rlp.Program PsName (TypedRlpExpr PsName) +-- -> RLPCT m (Core.Program Var) +-- desugarRlpProgR p = do +-- let p' = desugarRlpProg p +-- addDebugMsg "dump-desugared" $ show (out p') +-- pure p' -desugarRlpProg = undefined +desugarRlpProgR = undefined + +desugarRlpProg :: Rlp.Program PsName (TypedRlpExpr PsName) -> Core.Program Var +desugarRlpProg = rlpProgToCore desugarRlpExpr = undefined +type NameSupply = Labeled "NameSupply" (State [Name]) + runNameSupply :: Text -> Eff (NameSupply ': es) a -> Eff es a -runNameSupply pre = undefined -- evalState [ pre <> "_" <> tshow name | name <- [0..] ] +runNameSupply pre = runLabeled $ evalState [ pre <> "_" <> tshow name | name <- [0..] ] + where tshow = T.pack . show -- the rl' program is desugared by desugaring each declaration as a separate -- program, and taking the monoidal product of the lot :3 -rlpProgToCore :: Rlp.Program PsName (RlpExpr PsName) -> Program' +rlpProgToCore :: Rlp.Program PsName (TypedRlpExpr PsName) -> Core.Program Var rlpProgToCore = foldMapOf (programDecls . each) declToCore -declToCore :: Rlp.Decl PsName (RlpExpr PsName) -> Program' +declToCore :: Rlp.Decl PsName (TypedRlpExpr PsName) -> Core.Program Var --- assume all arguments are VarP's for now -declToCore (FunD b as e) = mempty & programScDefs .~ [ScDef b as' e'] +-- assume full eta-expansion for now +declToCore (FunD b [] e) = mempty & programScDefs .~ [ScDef b' [] undefined] where - as' = as ^.. each . singular _VarP + b' = MkVar b (typeToCore $ extract e) e' = runPureEff . runNameSupply b . exprToCore $ e -type NameSupply = State [Name] +typeToCore :: Rlp.Type PsName -> Core.Type +typeToCore (VarT n) = TyVar n exprToCore :: (NameSupply :> es) - => RlpExpr PsName -> Eff es Core.Expr' -exprToCore = foldFixM \case - InL e -> pure $ Fix e - InR e -> rlpExprToCore e + => TypedRlpExpr PsName + -> Eff es (Cofree (Core.ExprF Var) Core.Type) +exprToCore = cataM \case + t :<$ InL e -> pure $ t' :< annotateVar t' e + where t' = typeToCore t + -- InL e -> pure . annotateVars . Fix $ e + -- InR e -> rlpExprToCore e + +annotateVar :: Core.Type -> Core.ExprF PsName a -> Core.ExprF Var a + +-- fixed points: +annotateVar _ (VarF n) = VarF n +annotateVar _ (ConF t a) = ConF t a +annotateVar _ (AppF f x) = AppF f x +annotateVar _ (LitF l) = LitF l +annotateVar _ (TypeF t) = TypeF t rlpExprToCore :: (NameSupply :> es) - => Rlp.ExprF PsName Core.Expr' -> Eff es Core.Expr' + => Rlp.ExprF PsName Core.Expr' -> Eff es Core.Expr' -- assume all binders are simple variable patterns for now rlpExprToCore (LetEF r bs e) = pure $ Let r bs' e