From 45a660915261da303b587729e2419b63a5ea8dd2 Mon Sep 17 00:00:00 2001 From: crumbtoo Date: Thu, 22 Feb 2024 14:05:24 -0700 Subject: [PATCH] things --- src/Core/HindleyMilner.hs | 9 ++ src/Core/Parse.y | 109 +++++++++---------- src/Core/Syntax.hs | 224 ++++++++++++++++++++++++-------------- src/Core/SystemF.hs | 2 + 4 files changed, 207 insertions(+), 137 deletions(-) create mode 100644 src/Core/SystemF.hs diff --git a/src/Core/HindleyMilner.hs b/src/Core/HindleyMilner.hs index 1aaeb2d..ecee654 100644 --- a/src/Core/HindleyMilner.hs +++ b/src/Core/HindleyMilner.hs @@ -35,6 +35,12 @@ import Text.Printf import Core.Syntax ---------------------------------------------------------------------------------- +infer = undefined +check = undefined +checkCoreProg = undefined +checkCoreProgR = undefined +checkCoreExprR = undefined + -- | Annotated typing context -- I have a feeling we're going to want this in the -- future. type Context b = [(b, Type)] @@ -74,6 +80,8 @@ instance IsRlpcError TypeError where -- throw any number of fatal or nonfatal errors. Run with @runErrorful@. type HMError = Errorful TypeError +{-- + -- | Assert that an expression unifies with a given type -- -- >>> let e = [coreProg|3|] @@ -276,3 +284,4 @@ demoContext = , ("False", TyCon "Bool") ] +--} diff --git a/src/Core/Parse.y b/src/Core/Parse.y index 91bfe68..f432479 100644 --- a/src/Core/Parse.y +++ b/src/Core/Parse.y @@ -12,7 +12,6 @@ module Core.Parse , parseCoreProgR , module Core.Lex -- temp convenience , SrcError - , Module ) where @@ -34,7 +33,6 @@ import Data.Text qualified as T import Data.HashMap.Strict qualified as H } -%name parseCore Module %name parseCoreExpr StandaloneExpr %name parseCoreProg StandaloneProgram %tokentype { Located CoreToken } @@ -44,7 +42,6 @@ import Data.HashMap.Strict qualified as H %token let { Located _ TokenLet } letrec { Located _ TokenLetrec } - module { Located _ TokenModule } where { Located _ TokenWhere } case { Located _ TokenCase } of { Located _ TokenOf } @@ -73,18 +70,14 @@ import Data.HashMap.Strict qualified as H %% -Module :: { Module Name } -Module : module conname where Program Eof { Module (Just ($2, [])) $4 } - | Program Eof { Module Nothing $1 } - Eof :: { () } Eof : eof { () } | error { () } -StandaloneProgram :: { Program Name } +StandaloneProgram :: { Program Var } StandaloneProgram : Program eof { $1 } -Program :: { Program Name } +Program :: { Program Var } Program : ScTypeSig ';' Program { insTypeSig $1 $3 } | ScTypeSig OptSemi { singletonTypeSig $1 } | ScDef ';' Program { insScDef $1 $3 } @@ -104,97 +97,99 @@ OptSemi : ';' { () } | {- epsilon -} { () } ScTypeSig :: { (Name, Type) } -ScTypeSig : Var '::' Type { ($1,$3) } +ScTypeSig : Id '::' Type { ($1, $3 TyKindType) } -ScDefs :: { [ScDef Name] } +ScDefs :: { [ScDef PsName] } ScDefs : ScDef ';' ScDefs { $1 : $3 } | ScDef ';' { [$1] } | ScDef { [$1] } -ScDef :: { ScDef Name } -ScDef : Var ParList '=' Expr { ScDef $1 $2 $4 } - -- hack to allow constructors to be compiled into scs - | Con ParList '=' Expr { ScDef $1 $2 $4 } +ScDef :: { ScDef PsName } +ScDef : Id ParList '=' Expr { ScDef ($1,Nothing) $2 $4 } -Type :: { Type } -Type : Type1 { $1 } +Type :: { [(Name, Kind)] -> Kind -> Type } + : Type1 '->' Type { \cases + g TyKindType -> + $1 g TyKindType :-> $3 g TyKindType + _ _ -> error "kind mismatch" } + | Type1 { $1 } -Type1 :: { Type } +-- do we want to allow symbolic names for tyvars and tycons? + +Type1 :: { [(Name, Kind)] -> Kind -> Type } Type1 : '(' Type ')' { $2 } - | Type1 '->' Type { $1 :-> $3 } - -- do we want to allow symbolic names for tyvars and tycons? - | varname { TyVar $1 } - | conname { TyCon $1 } + | varname { \k -> TyVar $ MkVar $1 k } + | conname { \k -> TyCon $ MkTyCon $1 k } -ParList :: { [Name] } -ParList : Var ParList { $1 : $2 } +ParList :: { [PsName] } +ParList : varname ParList { ($1, Nothing) : $2 } | {- epsilon -} { [] } -StandaloneExpr :: { Expr Name } +StandaloneExpr :: { Expr Var } StandaloneExpr : Expr eof { $1 } -Expr :: { Expr Name } +Expr :: { Expr Var } Expr : LetExpr { $1 } | 'λ' Binders '->' Expr { Lam $2 $4 } | Application { $1 } | CaseExpr { $1 } | Expr1 { $1 } -LetExpr :: { Expr Name } +LetExpr :: { Expr Var } LetExpr : let '{' Bindings '}' in Expr { Let NonRec $3 $6 } | letrec '{' Bindings '}' in Expr { Let Rec $3 $6 } -Binders :: { [Name] } +Binders :: { [Var] } Binders : Var Binders { $1 : $2 } | Var { [$1] } -Application :: { Expr Name } -Application : Expr1 AppArgs { foldl' App $1 $2 } +Application :: { Expr Var } +Application : Application AppArg { App $1 $2 } + | Expr1 AppArg { App $1 $2 } -AppArgs :: { [Expr Name] } -AppArgs : Expr1 AppArgs { $1 : $2 } - | Expr1 { [$1] } +AppArg :: { Expr Var } + : '@' Type1 { Type ($2 [] TyKindInferred) } + | Expr1 { $1 } -CaseExpr :: { Expr Name } +CaseExpr :: { Expr Var } CaseExpr : case Expr of '{' Alters '}' { Case $2 $5 } -Alters :: { [Alter Name] } +Alters :: { [Alter Var] } Alters : Alter ';' Alters { $1 : $3 } | Alter ';' { [$1] } | Alter { [$1] } -Alter :: { Alter Name } -Alter : alttag ParList '->' Expr { Alter (AltTag $1) $2 $4 } - | Con ParList '->' Expr { Alter (AltData $1) $2 $4 } +Alter :: { Alter Var } +Alter : alttag AltParList '->' Expr { Alter (AltTag $1) $2 $4 } + | conname AltParList '->' Expr { Alter (AltData $1) $2 $4 } -Expr1 :: { Expr Name } +AltParList :: { [Var] } + : Var AltParList { $1 : $2 } + | {- epsilon -} { [] } + +Expr1 :: { Expr Var } Expr1 : litint { Lit $ IntL $1 } | Id { Var $1 } | PackCon { $1 } | '(' Expr ')' { $2 } -PackCon :: { Expr Name } +PackCon :: { Expr Var } PackCon : pack '{' litint litint '}' { Con $3 $4 } -Bindings :: { [Binding Name] } +Bindings :: { [Binding Var] } Bindings : Binding ';' Bindings { $1 : $3 } | Binding ';' { [$1] } | Binding { [$1] } -Binding :: { Binding Name } +Binding :: { Binding Var } Binding : Var '=' Expr { $1 := $3 } Id :: { Name } -Id : Var { $1 } - | Con { $1 } + : varname { $1 } + | conname { $1 } -Var :: { Name } -Var : varname { $1 } - | varsym { $1 } - -Con :: { Name } -Con : conname { $1 } - | consym { $1 } +Var :: { Var } +Var : '(' varname '::' Type ')' { MkVar $2 ($4 [] TyKindType) } { @@ -205,13 +200,13 @@ parseError (Located _ t : _) = {-# WARNING parseError "unimpl" #-} -exprPragma :: [String] -> RLPC (Expr Name) +exprPragma :: [String] -> RLPC (Expr Var) exprPragma ("AST" : e) = undefined exprPragma _ = undefined {-# WARNING exprPragma "unimpl" #-} -astPragma :: [String] -> RLPC (Expr Name) +astPragma :: [String] -> RLPC (Expr Var) astPragma _ = undefined {-# WARNING astPragma "unimpl" #-} @@ -228,13 +223,13 @@ insScDef sc = programScDefs %~ (sc:) singletonScDef :: (Hashable b) => ScDef b -> Program b singletonScDef sc = insScDef sc mempty -parseCoreExprR :: (Monad m) => [Located CoreToken] -> RLPCT m Expr' +parseCoreExprR :: (Monad m) => [Located CoreToken] -> RLPCT m (Expr Var) parseCoreExprR = hoistRlpcT generalise . parseCoreExpr -parseCoreProgR :: forall m. (Monad m) => [Located CoreToken] -> RLPCT m Program' +parseCoreProgR :: forall m. (Monad m) => [Located CoreToken] -> RLPCT m (Program Var) parseCoreProgR = ddumpast <=< (hoistRlpcT generalise . parseCoreProg) where - ddumpast :: Program' -> RLPCT m Program' + ddumpast :: (Program Var) -> RLPCT m (Program Var) ddumpast p = do addDebugMsg "dump-parsed-core" . show $ p pure p @@ -257,5 +252,7 @@ doTLPragma (Pragma pr) p = case pr of readt :: (Read a) => Text -> a readt = read . T.unpack +type PsName = (Name, Maybe Type) + } diff --git a/src/Core/Syntax.hs b/src/Core/Syntax.hs index db4a4d7..e125fa0 100644 --- a/src/Core/Syntax.hs +++ b/src/Core/Syntax.hs @@ -8,38 +8,31 @@ Description : Core ASTs and the like -- for recursion-schemes {-# LANGUAGE DeriveTraversable, TypeFamilies #-} module Core.Syntax - ( Expr(..) - , ExprF(..) - , ExprF'(..) - , Type(..) - , pattern TyInt - , Lit(..) - , pattern (:$) - , pattern (:@) - , pattern (:->) - , Binding(..) - , AltCon(..) - , pattern (:=) - , Rec(..) - , Alter(..) - , Name - , Tag - , ScDef(..) - , Module(..) - , Program(..) - , Program' + ( + -- * Core AST + ExprF(..), ExprF' + , ScDef(..), ScDef' + , Program(..), Program' + , Type(..), Kind, pattern (:->), pattern TyInt + , Alter(..), Alter', AltCon(..) + , Rec(..), Lit(..) , Pragma(..) - , unliftScDef - , programScDefs - , programTypeSigs - , programDataTags - , Expr' - , ScDef' - , Alter' - , Binding' - , HasRHS(_rhs) - , HasLHS(_lhs) + -- ** Variables and identifiers + , Name, Var(..), TyCon(..), Tag + , Binding(..), pattern (:=) + , type Binding' + -- ** Working with the fixed point of ExprF + , Expr, Expr' + , pattern Con, pattern Var, pattern App, pattern Lam, pattern Let + , pattern Case, pattern Type, pattern Lit + + -- * Misc , Pretty(pretty) + + -- * Optics + , programScDefs, programTypeSigs, programDataTags + , formalising + , HasRHS(_rhs), HasLHS(_lhs) ) where ---------------------------------------------------------------------------------- @@ -47,8 +40,6 @@ import Data.Coerce import Data.Pretty import Data.List (intersperse) import Data.Function ((&)) -import Data.Functor.Foldable -import Data.Functor.Foldable.TH (makeBaseFunctor) import Data.String import Data.HashMap.Strict (HashMap) import Data.HashMap.Strict qualified as H @@ -56,40 +47,74 @@ import Data.Hashable import Data.Text qualified as T import Data.Char import Data.These -import Data.Bifoldable (bifoldr) import GHC.Generics (Generic, Generically(..)) +import Text.Show.Deriving + +import Data.Fix hiding (cata, ana) +import Data.Bifoldable (bifoldr) +import Data.Functor.Foldable +import Data.Functor.Foldable.TH (makeBaseFunctor) + -- Lift instances for the Core quasiquoters -import Language.Haskell.TH.Syntax (Lift) +import Misc.Lift1 import Control.Lens ---------------------------------------------------------------------------------- -data Expr b = Var Name - | Con Tag Int -- ^ Con Tag Arity - | Case (Expr b) [Alter b] - | Lam [b] (Expr b) - | Let Rec [Binding b] (Expr b) - | App (Expr b) (Expr b) - | Lit Lit - deriving (Show, Read, Lift) +data ExprF b a = VarF Name + | ConF Tag Int -- ^ Con Tag Arity + | CaseF a [Alter b] + | LamF [b] a + | LetF Rec [Binding b] a + | AppF a a + | LitF Lit + | TypeF Type + deriving (Functor, Foldable, Traversable) -deriving instance (Eq b) => Eq (Expr b) +type Expr b = Fix (ExprF b) data Type = TyFun - | TyVar Name + | TyVar Var | TyApp Type Type - | TyCon Name - deriving (Show, Read, Lift, Eq) + | TyCon TyCon + | TyForall Var Type + | TyKindType + | TyKindInferred + deriving (Show, Eq, Lift) + +type Kind = Type + +data TyCon = MkTyCon Name Kind + deriving (Eq, Show, Lift) + +data Var = MkVar Name Type + deriving (Eq, Show, Lift) + +pattern Con :: Tag -> Int -> Expr b +pattern Con t a = Fix (ConF t a) + +pattern Var :: Name -> Expr b +pattern Var b = Fix (VarF b) + +pattern App :: Expr b -> Expr b -> Expr b +pattern App f x = Fix (AppF f x) + +pattern Lam :: [b] -> Expr b -> Expr b +pattern Lam bs e = Fix (LamF bs e) + +pattern Let :: Rec -> [Binding b] -> Expr b -> Expr b +pattern Let r bs e = Fix (LetF r bs e) + +pattern Case :: Expr b -> [Alter b] -> Expr b +pattern Case e as = Fix (CaseF e as) + +pattern Type :: Type -> Expr b +pattern Type t = Fix (TypeF t) + +pattern Lit :: Lit -> Expr b +pattern Lit t = Fix (LitF t) pattern TyInt :: Type -pattern TyInt = TyCon "Int#" - -infixl 2 :$ -pattern (:$) :: Expr b -> Expr b -> Expr b -pattern f :$ x = App f x - -infixl 2 :@ -pattern (:@) :: Type -> Type -> Type -pattern f :@ x = TyApp f x +pattern TyInt = TyCon (MkTyCon "Int#" TyKindType) infixr 1 :-> pattern (:->) :: Type -> Type -> Type @@ -97,46 +122,39 @@ pattern a :-> b = TyApp (TyApp TyFun a) b {-# COMPLETE Binding :: Binding #-} {-# COMPLETE (:=) :: Binding #-} -data Binding b = Binding b (Expr b) - deriving (Show, Read, Lift) -deriving instance (Eq b) => Eq (Binding b) +data Binding b = Binding b (Expr b) infixl 1 := pattern (:=) :: b -> Expr b -> Binding b pattern k := v = Binding k v data Alter b = Alter AltCon [b] (Expr b) - deriving (Show, Read, Lift) - -deriving instance (Eq b) => Eq (Alter b) newtype Pragma = Pragma [T.Text] data Rec = Rec | NonRec - deriving (Show, Read, Eq, Lift) + deriving (Show, Eq, Lift) data AltCon = AltData Name | AltTag Tag | AltLit Lit | AltDefault - deriving (Show, Read, Eq, Lift) + deriving (Show, Eq, Lift) newtype Lit = IntL Int - deriving (Show, Read, Eq, Lift) + deriving (Show, Eq, Lift) type Name = T.Text type Tag = Int data ScDef b = ScDef b [b] (Expr b) - deriving (Show, Lift) unliftScDef :: ScDef b -> Expr b unliftScDef (ScDef _ as e) = Lam as e data Module b = Module (Maybe (Name, [Name])) (Program b) - deriving (Show, Lift) data Program b = Program { _programScDefs :: [ScDef b] @@ -144,12 +162,12 @@ data Program b = Program , _programDataTags :: HashMap b (Tag, Int) -- ^ map constructors to their tag and arity } - deriving (Show, Lift, Generic) + deriving (Generic) deriving (Semigroup, Monoid) via Generically (Program b) makeLenses ''Program -makeBaseFunctor ''Expr +-- makeBaseFunctor ''Expr pure [] -- this is a weird optic, stronger than Lens and Prism, but weaker than Iso. @@ -169,13 +187,6 @@ type Binding' = Binding Name instance IsString (Expr b) where fromString = Var . fromString -instance IsString Type where - fromString "" = error "IsString Type string may not be empty" - fromString s - | isUpper c = TyCon . fromString $ s - | otherwise = TyVar . fromString $ s - where (c:_) = s - ---------------------------------------------------------------------------------- class HasRHS s t a b | s -> a, t -> b, s b -> t, t a -> s where @@ -214,14 +225,39 @@ instance HasLHS (Binding b) (Binding b) b b where (\ (k := _) -> k) (\ (_ := e) k' -> k' := e) +-- | This is not a valid isomorphism for expressions containing lambdas whose +-- bodies are themselves lambdas with multiple arguments: +-- +-- >>> [coreExpr|\x -> \y z -> x|] ^. from (from formalising) +-- Lam ["x"] (Lam ["y"] (Lam ["z"] (Var "x"))) +-- >>> [coreExpr|\x -> \y z -> x|] +-- Lam ["x"] (Lam ["y","z"] (Var "x")) +-- +-- For this reason, it's best to consider 'formalising' as if it were two +-- unrelated unidirectional getters. + +formalising :: Iso (Expr a) (Expr b) (Expr a) (Expr b) +formalising = iso sa bt where + sa :: Expr a -> Expr a + sa = ana \case + Lam [b] e -> LamF [b] e + Lam (b:bs) e -> LamF [b] (Lam bs e) + x -> project x + + bt :: Expr b -> Expr b + bt = cata \case + LamF [b] (Lam bs e) -> Lam (b:bs) e + x -> embed x + -------------------------------------------------------------------------------- --- TODO: print type sigs with corresponding scdefs --- TODO: emit pragmas for datatags instance (Hashable b, Pretty b) => Pretty (Program b) where - pretty p = ifoldrOf (programDataTags . ifolded) cataDataTag mempty p - $+$ vlinesOf (programJoinedDefs . to prettyGroup) p + pretty p = (datatags <> "\n") + $+$ defs where + datatags = ifoldrOf (programDataTags . ifolded) cataDataTag mempty p + defs = vlinesOf (programJoinedDefs . to prettyGroup) p + programJoinedDefs :: Fold (Program b) (These (b, Type) (ScDef b)) programJoinedDefs = folding $ \p -> foldMapOf programTypeSigs thisTs p @@ -234,7 +270,10 @@ instance (Hashable b, Pretty b) => Pretty (Program b) where H.singleton (sc ^. _lhs . _1) (That sc) prettyGroup :: These (b, Type) (ScDef b) -> Doc - prettyGroup = bifoldr ($$) ($$) mempty . bimap prettyTySig pretty + prettyGroup = bifoldr vcatWithSemi vcatWithSemi mempty + . bimap prettyTySig pretty + + vcatWithSemi a b = (a <+> ";") $$ b prettyTySig (n,t) = hsep [ttext n, "::", pretty t] @@ -257,7 +296,7 @@ instance Pretty Type where prettyPrec 1 f <+> prettyPrec 2 x instance (Pretty b) => Pretty (ScDef b) where - pretty sc = hsep [name, as, "=", hang empty 1 e, ";"] + pretty sc = hsep [name, as, "=", hang empty 1 e] where name = ttext $ sc ^. _lhs . _1 as = sc & hsepOf (_lhs . _2 . each . to ttext) @@ -298,3 +337,26 @@ explicitLayout as = vcat inner <+> "}" where inner = zipWith (<+>) delims (pretty <$> as) delims = "{" : repeat ";" +instance Pretty TyCon +instance Pretty Var + +-------------------------------------------------------------------------------- + +deriveShow1 ''ExprF + +instance Lift b => Lift1 (ExprF b) where + lift1 (VarF k) = liftCon 'VarF (lift k) + lift1 (AppF f x) = liftCon2 'AppF (lift f) (lift x) + lift1 (LamF b e) = liftCon2 'LamF (lift b) (lift e) + lift1 (LetF r bs e) = liftCon3 'LetF (lift r) (lift bs) (lift e) + lift1 (CaseF e as) = liftCon2 'CaseF (lift e) (lift as) + lift1 (TypeF t) = liftCon 'TypeF (lift t) + lift1 (LitF l) = liftCon 'LitF (lift l) + +deriving instance (Show b, Show a) => Show (ExprF b a) +deriving instance Show b => Show (Binding b) +deriving instance Show b => Show (Alter b) + +deriving instance Lift b => Lift (Binding b) +deriving instance Lift b => Lift (Alter b) + diff --git a/src/Core/SystemF.hs b/src/Core/SystemF.hs new file mode 100644 index 0000000..a7c7414 --- /dev/null +++ b/src/Core/SystemF.hs @@ -0,0 +1,2 @@ +module Core.SystemF where +