From 17058d3f8cd7b3a749a6f8a1513509bd94c2f9fc Mon Sep 17 00:00:00 2001 From: crumbtoo Date: Thu, 8 Feb 2024 18:40:46 -0700 Subject: [PATCH] letrec + typechecking core --- src/Control/Monad/Errorful.hs | 4 ++++ src/Core/HindleyMilner.hs | 20 +++++++++++------- src/Rlp/Lex.x | 2 ++ src/Rlp/Parse.y | 4 +++- src/Rlp/Parse/Types.hs | 2 ++ src/Rlp/Syntax.hs | 39 +++++++++++++++++++++-------------- 6 files changed, 47 insertions(+), 24 deletions(-) diff --git a/src/Control/Monad/Errorful.hs b/src/Control/Monad/Errorful.hs index f788aaf..1d46e91 100644 --- a/src/Control/Monad/Errorful.hs +++ b/src/Control/Monad/Errorful.hs @@ -8,6 +8,7 @@ module Control.Monad.Errorful , errorful , runErrorful , mapErrorful + , hoistErrorfulT , MonadErrorful(..) ) where @@ -74,6 +75,9 @@ mapErrorful f (ErrorfulT m) = ErrorfulT $ -- mapErrorful f = coerced . mapped . _2 . mapped %~ f -- lol +hoistErrorfulT :: (forall a. m a -> n a) -> ErrorfulT e m a -> ErrorfulT e n a +hoistErrorfulT nt (ErrorfulT m) = ErrorfulT (nt m) + -------------------------------------------------------------------------------- -- daily dose of n^2 instances diff --git a/src/Core/HindleyMilner.hs b/src/Core/HindleyMilner.hs index 7dcc4c6..9fa3208 100644 --- a/src/Core/HindleyMilner.hs +++ b/src/Core/HindleyMilner.hs @@ -22,9 +22,13 @@ import Data.Maybe (fromMaybe) import Data.Text qualified as T import Data.HashMap.Strict qualified as H import Data.Foldable (traverse_) +import Data.Functor +import Data.Functor.Identity import Compiler.RLPC +import Compiler.Types +import Compiler.RlpcError import Control.Monad (foldM, void, forM) -import Control.Monad.Errorful (Errorful, addFatal) +import Control.Monad.Errorful import Control.Monad.State import Control.Monad.Utils (mapAccumLM) import Text.Printf @@ -38,8 +42,6 @@ type Context b = [(b, Type)] -- | Unannotated typing context, AKA our beloved Γ. type Context' = Context Name --- TODO: Errorful monad? - -- | Type error enum. data TypeError -- | Two types could not be unified @@ -93,7 +95,7 @@ check g t1 e = do -- in the mean time all top-level binders must have a type annotation. checkCoreProg :: Program' -> HMError () checkCoreProg p = scDefs - & traverse_ k + & traverse_ k where scDefs = p ^. programScDefs g = gatherTypeSigs p @@ -105,10 +107,14 @@ checkCoreProg p = scDefs where scname = sc ^. _lhs._1 -- | @checkCoreProgR p@ returns @p@ if @p@ successfully typechecks. -checkCoreProgR :: (Applicative m) => Program' -> RLPCT m Program' -checkCoreProgR p = undefined +checkCoreProgR :: forall m. (Monad m) => Program' -> RLPCT m Program' +checkCoreProgR p = (hoistRlpcT generalise . liftE . checkCoreProg $ p) + $> p + where + liftE = liftErrorful . mapErrorful (errorMsg (SrcSpan 0 0 0 0)) -{-# WARNING checkCoreProgR "unimpl" #-} + generalise :: forall a. Identity a -> m a + generalise (Identity a) = pure a -- | Infer the type of an expression under some context. -- diff --git a/src/Rlp/Lex.x b/src/Rlp/Lex.x index f5e7e34..7b2e75b 100644 --- a/src/Rlp/Lex.x +++ b/src/Rlp/Lex.x @@ -85,6 +85,7 @@ $white_no_nl+ ; <0> { "let" { constToken TokenLet `thenBeginPush` layout_let } + "letrec" { constToken TokenLet `thenBeginPush` layout_let } "of" { constToken TokenOf `thenBeginPush` layout_of } } @@ -155,6 +156,7 @@ lexReservedName = \case "case" -> TokenCase "of" -> TokenOf "let" -> TokenLet + "letrec" -> TokenLetrec "in" -> TokenIn "infix" -> TokenInfix "infixl" -> TokenInfixL diff --git a/src/Rlp/Parse.y b/src/Rlp/Parse.y index d8c0ff4..652fccc 100644 --- a/src/Rlp/Parse.y +++ b/src/Rlp/Parse.y @@ -62,6 +62,7 @@ import Compiler.Types infixr { Located _ TokenInfixR } infix { Located _ TokenInfix } let { Located _ TokenLet } + letrec { Located _ TokenLetrec } in { Located _ TokenIn } %nonassoc '=' @@ -190,7 +191,8 @@ AppExpr :: { RlpExpr' RlpcPs } | AppExpr Expr1 { AppE <<~ $1 <~> $2 } LetExpr :: { RlpExpr' RlpcPs } - : let layout1(Binding) in Expr { $1 \$> LetE $2 $4 } + : let layout1(Binding) in Expr { $1 \$> LetE $2 $4 } + | letrec layout1(Binding) in Expr { $1 \$> LetrecE $2 $4 } CaseExpr :: { RlpExpr' RlpcPs } : case Expr of layout0(CaseAlt) diff --git a/src/Rlp/Parse/Types.hs b/src/Rlp/Parse/Types.hs index 244b7e1..1f71d2b 100644 --- a/src/Rlp/Parse/Types.hs +++ b/src/Rlp/Parse/Types.hs @@ -64,6 +64,7 @@ type instance XTySigD RlpcPs = () type instance XXDeclD RlpcPs = () type instance XLetE RlpcPs = () +type instance XLetrecE RlpcPs = () type instance XVarE RlpcPs = () type instance XLamE RlpcPs = () type instance XCaseE RlpcPs = () @@ -127,6 +128,7 @@ data RlpToken | TokenCase | TokenOf | TokenLet + | TokenLetrec | TokenIn | TokenInfixL | TokenInfixR diff --git a/src/Rlp/Syntax.hs b/src/Rlp/Syntax.hs index 55146e0..6ef26fb 100644 --- a/src/Rlp/Syntax.hs +++ b/src/Rlp/Syntax.hs @@ -26,15 +26,15 @@ module Rlp.Syntax -- *** Decl , XFunD, XTySigD, XInfixD, XDataD, XXDeclD -- *** RlpExpr - , XLetE, XVarE, XLamE, XCaseE, XIfE, XAppE, XLitE + , XLetE, XLetrecE, XVarE, XLamE, XCaseE, XIfE, XAppE, XLitE , XParE, XOAppE, XXRlpExprE -- ** Pattern synonyms -- *** Decl , pattern FunD, pattern TySigD, pattern InfixD, pattern DataD , pattern FunD'', pattern TySigD'', pattern InfixD'', pattern DataD'' -- *** RlpExpr - , pattern LetE, pattern VarE, pattern LamE, pattern CaseE, pattern IfE - , pattern AppE, pattern LitE, pattern ParE, pattern OAppE + , pattern LetE, pattern LetrecE, pattern VarE, pattern LamE, pattern CaseE + , pattern IfE , pattern AppE, pattern LitE, pattern ParE, pattern OAppE , pattern XRlpExprE -- *** RlpType , pattern FunConT'', pattern FunT'', pattern AppT'', pattern VarT'' @@ -165,19 +165,21 @@ data ConAlt p = ConAlt (IdP p) [RlpType' p] deriving instance (Show (IdP p), Show (XRec p (RlpType p))) => Show (ConAlt p) -data RlpExpr p = LetE' (XLetE p) [Binding' p] (RlpExpr' p) - | VarE' (XVarE p) (IdP p) - | LamE' (XLamE p) [Pat p] (RlpExpr' p) - | CaseE' (XCaseE p) (RlpExpr' p) [(Alt p, Where p)] - | IfE' (XIfE p) (RlpExpr' p) (RlpExpr' p) (RlpExpr' p) - | AppE' (XAppE p) (RlpExpr' p) (RlpExpr' p) - | LitE' (XLitE p) (Lit p) - | ParE' (XParE p) (RlpExpr' p) - | OAppE' (XOAppE p) (IdP p) (RlpExpr' p) (RlpExpr' p) +data RlpExpr p = LetE' (XLetE p) [Binding' p] (RlpExpr' p) + | LetrecE' (XLetrecE p) [Binding' p] (RlpExpr' p) + | VarE' (XVarE p) (IdP p) + | LamE' (XLamE p) [Pat p] (RlpExpr' p) + | CaseE' (XCaseE p) (RlpExpr' p) [(Alt p, Where p)] + | IfE' (XIfE p) (RlpExpr' p) (RlpExpr' p) (RlpExpr' p) + | AppE' (XAppE p) (RlpExpr' p) (RlpExpr' p) + | LitE' (XLitE p) (Lit p) + | ParE' (XParE p) (RlpExpr' p) + | OAppE' (XOAppE p) (IdP p) (RlpExpr' p) (RlpExpr' p) | XRlpExprE' !(XXRlpExprE p) deriving (Generic) type family XLetE p +type family XLetrecE p type family XVarE p type family XLamE p type family XCaseE p @@ -189,6 +191,7 @@ type family XOAppE p type family XXRlpExprE p pattern LetE :: (XLetE p ~ ()) => [Binding' p] -> RlpExpr' p -> RlpExpr p +pattern LetrecE :: (XLetrecE p ~ ()) => [Binding' p] -> RlpExpr' p -> RlpExpr p pattern VarE :: (XVarE p ~ ()) => IdP p -> RlpExpr p pattern LamE :: (XLamE p ~ ()) => [Pat p] -> RlpExpr' p -> RlpExpr p pattern CaseE :: (XCaseE p ~ ()) => RlpExpr' p -> [(Alt p, Where p)] -> RlpExpr p @@ -200,6 +203,7 @@ pattern OAppE :: (XOAppE p ~ ()) => IdP p -> RlpExpr' p -> RlpExpr' p -> RlpExpr pattern XRlpExprE :: (XXRlpExprE p ~ ()) => RlpExpr p pattern LetE bs e = LetE' () bs e +pattern LetrecE bs e = LetrecE' () bs e pattern VarE n = VarE' () n pattern LamE as e = LamE' () as e pattern CaseE e as = CaseE' () e as @@ -211,10 +215,10 @@ pattern OAppE n a b = OAppE' () n a b pattern XRlpExprE = XRlpExprE' () deriving instance - ( Show (XLetE p), Show (XVarE p), Show (XLamE p) - , Show (XCaseE p), Show (XIfE p), Show (XAppE p) - , Show (XLitE p), Show (XParE p), Show (XOAppE p) - , Show (XXRlpExprE p) + ( Show (XLetE p), Show (XLetrecE p), Show (XVarE p) + , Show (XLamE p), Show (XCaseE p), Show (XIfE p) + , Show (XAppE p), Show (XLitE p), Show (XParE p) + , Show (XOAppE p), Show (XXRlpExprE p) , PhaseShow p ) => Show (RlpExpr p) @@ -308,6 +312,7 @@ makePrisms ''Pat -------------------------------------------------------------------------------- data RlpExprF p a = LetE'F (XLetE p) [Binding' p] a + | LetrecE'F (XLetrecE p) [Binding' p] a | VarE'F (XVarE p) (IdP p) | LamE'F (XLamE p) [Pat p] a | CaseE'F (XCaseE p) a [(Alt p, Where p)] @@ -324,6 +329,7 @@ type instance Base (RlpExpr p) = RlpExprF p instance (UnXRec p) => Recursive (RlpExpr p) where project = \case LetE' xx bs e -> LetE'F xx bs (unXRec e) + LetrecE' xx bs e -> LetrecE'F xx bs (unXRec e) VarE' xx n -> VarE'F xx n LamE' xx ps e -> LamE'F xx ps (unXRec e) CaseE' xx e as -> CaseE'F xx (unXRec e) as @@ -337,6 +343,7 @@ instance (UnXRec p) => Recursive (RlpExpr p) where instance (WrapXRec p) => Corecursive (RlpExpr p) where embed = \case LetE'F xx bs e -> LetE' xx bs (wrapXRec e) + LetrecE'F xx bs e -> LetrecE' xx bs (wrapXRec e) VarE'F xx n -> VarE' xx n LamE'F xx ps e -> LamE' xx ps (wrapXRec e) CaseE'F xx e as -> CaseE' xx (wrapXRec e) as