From fc942fb8dfaad7614567f2dcbd9a911ffd474a06 Mon Sep 17 00:00:00 2001 From: Tom Smeding Date: Tue, 27 Feb 2024 22:17:03 +0100 Subject: Trees that explode --- src/HSVIS/AST.hs | 310 +++++++++++++++++++++++++++++++++++++++++-------- src/HSVIS/Parser.hs | 168 +++++++++++++++++---------- src/HSVIS/Typecheck.hs | 120 ++++++++++++++++--- 3 files changed, 467 insertions(+), 131 deletions(-) (limited to 'src/HSVIS') diff --git a/src/HSVIS/AST.hs b/src/HSVIS/AST.hs index f606d22..7b05e19 100644 --- a/src/HSVIS/AST.hs +++ b/src/HSVIS/AST.hs @@ -1,75 +1,162 @@ +{-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-} +{-# LANGUAGE PolyKinds #-} {-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE LambdaCase #-} module HSVIS.AST where +import Data.Bifunctor (bimap, second) +import qualified Data.Kind as DK import Data.List.NonEmpty (NonEmpty) +import Data.Proxy import HSVIS.Pretty +-- | An AST type has a single stage argument. +type ASTType = DK.Type -> DK.Type + +-- | Trees that Grow extension type family +type family X (f :: ASTType) s + +-- | Additional constructors +data family E (f :: ASTType) s + +class HasExt f where + type HasXField f :: Bool + type HasECon f :: Bool + type ContainsData f :: [ASTType] + extOf :: f s -> X f s + extMap :: Proxy f -> Proxy s1 -> Proxy s2 + -> XMapperTelescope (TransitiveContainsData '[f]) s1 s2 + (EMapperTelescope (TransitiveContainsData '[f]) s1 s2 + (f s1 -> f s2)) + +type family If c a b where + If 'True a b = a + If 'False a b = b + +type family ASTShowPrereqs f s :: DK.Constraint where + ASTShowPrereqs f s = + (If (HasXField f) (Show (X f s)) (() :: DK.Constraint) + ,If (HasECon f) (Show (E f s)) (() :: DK.Constraint) + ,ASTShowPrereqsC (ContainsData f) s) + +type family ASTShowPrereqsC l s :: DK.Constraint where + ASTShowPrereqsC '[] s = () + ASTShowPrereqsC (f ': fs) s = (Show (f s), ASTShowPrereqsC fs s) + +type family a && b where + 'False && b = 'False + 'True && b = b + +type family In x l where + In x '[] = 'False + In x (x ': ys) = 'True + In x (_ ': ys) = In x ys + +type family Sublist l1 l2 where + Sublist '[] l = 'True + Sublist (x ': xs) l = In x l && Sublist xs l + +type family Union l1 l2 where + Union '[] l = l + Union (x ': xs) l = If (In x l) (Union xs l) (x ': Union xs l) + +type family MapContainsData l where + MapContainsData '[] = '[] + MapContainsData (f ': fs) = Union (ContainsData f) (MapContainsData fs) + +type family TransitiveContainsData fs where + TransitiveContainsData fs = TransitiveContainsData' fs (Sublist (Union fs (MapContainsData fs)) fs) + +type family TransitiveContainsData' fs isfull where + TransitiveContainsData' fs 'True = fs + TransitiveContainsData' fs 'False = TransitiveContainsData (Union fs (MapContainsData fs)) + +type family XMapperTelescope fs s1 s2 a where + XMapperTelescope '[] s1 s2 a = a + XMapperTelescope (f ': fs) s1 s2 a = + If (HasXField f) + ((X f s1 -> X f s2) -> XMapperTelescope fs s1 s2 a) + (XMapperTelescope fs s1 s2 a) + +type family EMapperTelescope fs s1 s2 a where + EMapperTelescope '[] s1 s2 a = a + EMapperTelescope (f ': fs) s1 s2 a = + If (HasECon f) + ((X f s1 -> E f s1 -> f s2) -> EMapperTelescope fs s1 s2 a) + (EMapperTelescope fs s1 s2 a) + + newtype Name = Name String deriving (Show, Eq) -data Program t = Program [DataDef] [FunDef t] - deriving (Show) +data Program s = Program [DataDef s] [FunDef s] +deriving instance (Show (DataDef s), Show (FunDef s)) => Show (Program s) -data DataDef = DataDef Name [Name] [(Name, [Type])] - deriving (Show) +data DataDef s = DataDef (X DataDef s) Name [Name] [(Name, [Type s])] +deriving instance ASTShowPrereqs DataDef s => Show (DataDef s) -data FunDef t = FunDef Name (Maybe Type) (NonEmpty (FunEq t)) - deriving (Show) +data FunDef s = FunDef (X FunDef s) Name (Maybe (Type s)) (NonEmpty (FunEq s)) +deriving instance ASTShowPrereqs FunDef s => Show (FunDef s) -data FunEq t = FunEq t Name [Pattern t] (RHS t) - deriving (Show) +data FunEq s = FunEq (X FunEq s) Name [Pattern s] (RHS s) +deriving instance ASTShowPrereqs FunEq s => Show (FunEq s) -data TypeStage = TSTC | TSNormal - deriving (Show) +data Kind s + = KType (X Kind s) + | KFun (X Kind s) (Kind s) (Kind s) +deriving instance ASTShowPrereqs Kind s => Show (Kind s) -data GType (stage :: TypeStage) where - TApp :: GType s -> [GType s] -> GType s - TTup :: [GType s] -> GType s - TList :: GType s -> GType s - TFun :: GType s -> GType s -> GType s - TCon :: Name -> GType s - TVar :: Name -> GType s - - -- Type constructor used only while type checking - TUniVar :: Int -> GType 'TSTC -deriving instance Show (GType stage) - -type TCType = GType 'TSTC -type Type = GType 'TSNormal - -data Pattern t - = PWildcard t - | PVar t Name - | PAs t Name (Pattern t) - | PCon t Name [Pattern t] - | POp t (Pattern t) Operator (Pattern t) - | PList t [Pattern t] - | PTup t [Pattern t] - deriving (Show) +data Type s + = TApp (X Type s) (Type s) [Type s] + | TTup (X Type s) [Type s] + | TList (X Type s) (Type s) + | TFun (X Type s) (Type s) (Type s) + | TCon (X Type s) Name + | TVar (X Type s) Name -data RHS t - = Guarded [(Expr t, Expr t)] -- currently not parsed - | Plain (Expr t) - deriving (Show) + -- extension point + | TExt (X Type s) !(E Type s) +deriving instance ASTShowPrereqs Type s => Show (Type s) -data Expr t - = ELit t Literal - | EVar t Name - | ECon t Name - | EList t [Expr t] - | ETup t [Expr t] - | EApp t (Expr t) [Expr t] - | EOp t (Expr t) Operator (Expr t) - | EIf t (Expr t) (Expr t) (Expr t) - | ECase t (Expr t) [(Pattern t, RHS t)] - | ELet t [FunDef t] (Expr t) - | EParseError - deriving (Show) +data Pattern s + = PWildcard (X Pattern s) + | PVar (X Pattern s) Name + | PAs (X Pattern s) Name (Pattern s) + | PCon (X Pattern s) Name [Pattern s] + | POp (X Pattern s) (Pattern s) Operator (Pattern s) + | PList (X Pattern s) [Pattern s] + | PTup (X Pattern s) [Pattern s] +deriving instance ASTShowPrereqs Pattern s => Show (Pattern s) + +data RHS s + = Guarded (X RHS s) [(Expr s, Expr s)] -- currently not parsed + | Plain (X RHS s) (Expr s) +deriving instance ASTShowPrereqs RHS s => Show (RHS s) + +data Expr s + = ELit (X Expr s) Literal + | EVar (X Expr s) Name + | ECon (X Expr s) Name + | EList (X Expr s) [Expr s] + | ETup (X Expr s) [Expr s] + | EApp (X Expr s) (Expr s) [Expr s] + | EOp (X Expr s) (Expr s) Operator (Expr s) + | EIf (X Expr s) (Expr s) (Expr s) (Expr s) + | ECase (X Expr s) (Expr s) [(Pattern s, RHS s)] + | ELet (X Expr s) [FunDef s] (Expr s) + | EError (X Expr s) +deriving instance ASTShowPrereqs Expr s => Show (Expr s) data Literal = LInt Integer | LFloat Rational | LChar Char | LString String deriving (Show) @@ -80,3 +167,124 @@ data Operator = OAdd | OSub | OMul | ODiv | OMod | OEqu | OPow instance Pretty Name where prettysPrec _ (Name n) = showString ("\"" ++ n ++ "\"") + +instance HasExt DataDef where + type HasXField DataDef = 'True + type HasECon DataDef = 'False + type ContainsData DataDef = '[Type] + extOf (DataDef x _ _ _) = x + extMap _ ps1 ps2 fdd fty gty (DataDef x n ps cs) = + DataDef (fdd x) n ps (map (second (map (extMap (Proxy @Type) ps1 ps2 fty gty))) cs) + +instance HasExt FunDef where + type HasXField FunDef = 'True + type HasECon FunDef = 'False + type ContainsData FunDef = '[Type, FunEq] + extOf (FunDef x _ _ _) = x + extMap _ ps1 ps2 ffd ffe frh fty fpa fex gty (FunDef x n msig es) = + FunDef (ffd x) n (extMap (Proxy @Type) ps1 ps2 fty gty <$> msig) + (fmap (extMap (Proxy @FunEq) ps1 ps2 frh ffd fpa fex fty ffe gty) es) + +instance HasExt FunEq where + type HasXField FunEq = 'True + type HasECon FunEq = 'False + type ContainsData FunEq = '[Pattern, RHS] + extOf (FunEq x _ _ _) = x + extMap _ ps1 ps2 frh ffd fpa fex fty ffe gty (FunEq x n ps rhs) = + FunEq (ffe x) n (map (extMap (Proxy @Pattern) ps1 ps2 fpa) ps) + (extMap (Proxy @RHS) ps1 ps2 frh ffd fpa fex fty ffe gty rhs) + +instance HasExt Kind where + type HasXField Kind = 'True + type HasECon Kind = 'False + type ContainsData Kind = '[Kind] + extOf (KType x) = x + extOf (KFun x _ _) = x + extMap _ _ _ f (KType x) = KType (f x) + extMap p ps1 ps2 f (KFun x a b) = KFun (f x) (extMap p ps1 ps2 f a) (extMap p ps1 ps2 f b) + +instance HasExt Type where + type HasXField Type = 'True + type HasECon Type = 'True + type ContainsData Type = '[Type] + extOf (TApp x _ _) = x + extOf (TTup x _) = x + extOf (TList x _) = x + extOf (TFun x _ _) = x + extOf (TCon x _) = x + extOf (TVar x _) = x + extOf (TExt x _) = x + + extMap p ps1 ps2 f g (TApp x a b) = TApp (f x) (extMap p ps1 ps2 f g a) (map (extMap p ps1 ps2 f g) b) + extMap p ps1 ps2 f g (TTup x as) = TTup (f x) (map (extMap p ps1 ps2 f g) as) + extMap p ps1 ps2 f g (TList x a) = TList (f x) (extMap p ps1 ps2 f g a) + extMap p ps1 ps2 f g (TFun x a b) = TFun (f x) (extMap p ps1 ps2 f g a) (extMap p ps1 ps2 f g b) + extMap _ _ _ f _ (TCon x n) = TCon (f x) n + extMap _ _ _ f _ (TVar x n) = TVar (f x) n + extMap _ _ _ _ g (TExt x e) = g x e + +instance HasExt Pattern where + type HasXField Pattern = 'True + type HasECon Pattern = 'False + type ContainsData Pattern = '[Pattern] + extOf (PWildcard x) = x + extOf (PVar x _) = x + extOf (PAs x _ _) = x + extOf (PCon x _ _) = x + extOf (POp x _ _ _) = x + extOf (PList x _) = x + extOf (PTup x _) = x + + extMap _ _ _ f (PWildcard x) = PWildcard (f x) + extMap _ _ _ f (PVar x n) = PVar (f x) n + extMap p ps1 ps2 f (PAs x n a) = PAs (f x) n (extMap p ps1 ps2 f a) + extMap p ps1 ps2 f (PCon x n as) = PCon (f x) n (map (extMap p ps1 ps2 f) as) + extMap p ps1 ps2 f (POp x a n b) = POp (f x) (extMap p ps1 ps2 f a) n (extMap p ps1 ps2 f b) + extMap p ps1 ps2 f (PList x as) = PList (f x) (map (extMap p ps1 ps2 f) as) + extMap p ps1 ps2 f (PTup x as) = PTup (f x) (map (extMap p ps1 ps2 f) as) + +instance HasExt RHS where + type HasXField RHS = 'True + type HasECon RHS = 'False + type ContainsData RHS = '[Expr] + extOf (Guarded x _) = x + extOf (Plain x _) = x + + extMap _ ps1 ps2 frh ffd fpa fex fty ffe gty (Guarded x l) = + Guarded (frh x) (map (bimap (extMap (Proxy @Expr) ps1 ps2 frh ffd fpa fex fty ffe gty) + (extMap (Proxy @Expr) ps1 ps2 frh ffd fpa fex fty ffe gty)) + l) + extMap _ ps1 ps2 frh ffd fpa fex fty ffe gty (Plain x e) = + Plain (frh x) (extMap (Proxy @Expr) ps1 ps2 frh ffd fpa fex fty ffe gty e) + +instance HasExt Expr where + type HasXField Expr = 'True + type HasECon Expr = 'False + type ContainsData Expr = '[Expr, Pattern, RHS, FunDef] + extOf (ELit x _) = x + extOf (EVar x _) = x + extOf (ECon x _) = x + extOf (EList x _) = x + extOf (ETup x _) = x + extOf (EApp x _ _) = x + extOf (EOp x _ _ _) = x + extOf (EIf x _ _ _) = x + extOf (ECase x _ _) = x + extOf (ELet x _ _) = x + extOf (EError x) = x + + extMap p ps1 ps2 frh ffd fpa fex fty ffe gty = \case + ELit x l -> ELit (fex x) l + EVar x n -> EVar (fex x) n + ECon x n -> ECon (fex x) n + EList x es -> EList (fex x) (map (extMap p ps1 ps2 frh ffd fpa fex fty ffe gty) es) + ETup x es -> ETup (fex x) (map (extMap p ps1 ps2 frh ffd fpa fex fty ffe gty) es) + EApp x a es -> EApp (fex x) (extMap p ps1 ps2 frh ffd fpa fex fty ffe gty a) (map (extMap p ps1 ps2 frh ffd fpa fex fty ffe gty) es) + EOp x a n b -> EOp (fex x) (extMap p ps1 ps2 frh ffd fpa fex fty ffe gty a) n (extMap p ps1 ps2 frh ffd fpa fex fty ffe gty b) + EIf x a b c -> EIf (fex x) (extMap p ps1 ps2 frh ffd fpa fex fty ffe gty a) (extMap p ps1 ps2 frh ffd fpa fex fty ffe gty b) (extMap p ps1 ps2 frh ffd fpa fex fty ffe gty c) + ECase x a l -> ECase (fex x) (extMap p ps1 ps2 frh ffd fpa fex fty ffe gty a) + (map (bimap (extMap (Proxy @Pattern) ps1 ps2 fpa) + (extMap (Proxy @RHS) ps1 ps2 frh ffd fpa fex fty ffe gty)) + l) + ELet x as b -> ELet (fex x) (map (extMap (Proxy @FunDef) ps1 ps2 ffd ffe frh fty fpa fex gty) as) (extMap p ps1 ps2 frh ffd fpa fex fty ffe gty b) + EError x -> EError (fex x) diff --git a/src/HSVIS/Parser.hs b/src/HSVIS/Parser.hs index 04e6a63..eba78d8 100644 --- a/src/HSVIS/Parser.hs +++ b/src/HSVIS/Parser.hs @@ -12,11 +12,15 @@ {-# LANGUAGE TypeApplications #-} {-# LANGUAGE ViewPatterns #-} {-# LANGUAGE InstanceSigs #-} +{-# LANGUAGE EmptyDataDeriving #-} -- I don't want a warning for 'head' and 'tail' in this file. But I also don't -- want GHCs before 9.8 to complain that they don't know the x-partial warning. {-# OPTIONS_GHC -Wno-unrecognised-warning-flags -Wno-x-partial #-} module HSVIS.Parser ( + StageParsed, parse, + -- * Staged AST synonyms + PProgram, PDataDef, PFunDef, PFunEq, PType, PPattern, PRHS, PExpr, ) where -- import Control.Applicative @@ -34,11 +38,36 @@ import Data.These import Control.FAlternative import Data.Bag +import Data.List.NonEmpty.Util import HSVIS.AST import HSVIS.Diagnostic import HSVIS.Pretty +-- | The stage for the parser +data StageParsed + +type instance X DataDef StageParsed = Range +type instance X FunDef StageParsed = Range +type instance X FunEq StageParsed = Range +type instance X Type StageParsed = Range +type instance X Pattern StageParsed = Range +type instance X RHS StageParsed = Range +type instance X Expr StageParsed = Range + +data instance E Type StageParsed + deriving (Show) + +type PProgram = Program StageParsed +type PDataDef = DataDef StageParsed +type PFunDef = FunDef StageParsed +type PFunEq = FunEq StageParsed +type PType = Type StageParsed +type PPattern = Pattern StageParsed +type PRHS = RHS StageParsed +type PExpr = Expr StageParsed + + -- Positions are zero-based in both dimensions. -- See 'isInsideBlock' and 'isAtBlockLeft' for the two relevant "inside the -- block" conditions. @@ -145,7 +174,7 @@ instance KnownFallible fail => MonadChronicle (Bag Diagnostic) (Parser fail) whe That res -> Parser (\_ ps kok _ _ -> kok ps mempty res) These errs res -> Parser (\_ ps kok _ _ -> kok ps errs res) -parse :: FilePath -> String -> ([Diagnostic], Maybe (Program Range)) +parse :: FilePath -> String -> ([Diagnostic], Maybe PProgram) parse fp source = runParser pProgram (Context fp (lines source) []) (PS (Pos 0 0) (Pos 0 0) source) (\_ errs res -> case errs of @@ -154,7 +183,7 @@ parse fp source = (\errs -> (toList errs, Nothing)) () -- the program parser cannot fail! :D -pProgram :: IParser (Program Range) +pProgram :: IParser PProgram pProgram = do defs <- pTopDefs let (datadefs, fundefs) = partitionEithers defs @@ -162,7 +191,7 @@ pProgram = do assertEOF Error return (Program datadefs fundefs) -pTopDefs :: IParser [Either DataDef (FunDef Range)] +pTopDefs :: IParser [Either PDataDef PFunDef] pTopDefs = do faoptional pTopDef >>= \case Nothing -> do @@ -177,7 +206,7 @@ pTopDefs = do defs2 <- pTopDefs return (defs ++ defs2) -pTopDef :: FParser [Either DataDef (FunDef Range)] +pTopDef :: FParser [Either PDataDef PFunDef] pTopDef = do noFail skipWhiteComment noFail isAtBlockLeft >>= \case @@ -187,8 +216,9 @@ pTopDef = do noFail $ readWhileInline (const True) pTopDef -pDataDef0 :: FParser [DataDef] +pDataDef0 :: FParser [PDataDef] pDataDef0 = do + pos1 <- gets psCur pKeyword "data" noFail $ do inlineWhite @@ -199,9 +229,10 @@ pDataDef0 = do Just name -> do params <- famany (inlineWhite >> pIdentifier0 InBlock Lowercase WCBacktrack) cons <- pDatacons "=" - return [DataDef name params cons] + pos2 <- gets psCur + return [DataDef (Range pos1 pos2) name params cons] where - pDatacons :: String -> IParser [(Name, [Type])] + pDatacons :: String -> IParser [(Name, [PType])] pDatacons leader = do inlineWhite facatch (return []) $ do @@ -218,31 +249,34 @@ data FunEqContext | Continue Name deriving (Show) -pFunDef0 :: FParser [FunDef Range] +pFunDef0 :: FParser [PFunDef] pFunDef0 = faasum' - [do (name, typ) <- pStandaloneTypesig0 + [do (sigrange, (name, typ)) <- ranged pStandaloneTypesig0 noFail $ do faoptional (pFunEq (TypeSig name)) >>= \case - Nothing -> do - raise Error $ "Expected function equation for " ++ pretty name ++ - " after type signature" - return [] - Just [] -> do - pos <- gets psCur - return [FunDef name (Just typ) - (FunEq (Range pos pos) name [] (Plain EParseError) :| [])] Just (clause1 : clauses1) -> do clauses <- concat <$> famany (pFunEq (Continue name)) - return [FunDef name (Just typ) (clause1 :| clauses1 ++ clauses)] + let clauses' = clause1 :| clauses1 ++ clauses + let rng = sigrange <> foldMapne extOf clauses' + return [FunDef rng name (Just typ) clauses'] + _ -> do + pos <- gets psCur + raise Error $ "Expected function equation for " ++ pretty name ++ + " after type signature" + let rng = Range pos pos + return [FunDef sigrange name (Just typ) + (FunEq rng name [] (Plain rng (EError rng)) :| [])] ,do pFunEq FirstLine >>= \case clause1@(FunEq _ name _ _) : clauses1 -> noFail $ do clauses <- concat <$> famany (pFunEq (Continue name)) - return [FunDef name Nothing (clause1 :| clauses1 ++ clauses)] + let clauses' = clause1 :| clauses1 ++ clauses + let rng = foldMapne extOf clauses' + return [FunDef rng name Nothing clauses'] [] -> faempty] -- | Given the name from the type signature or a previous clause, if any. -pFunEq :: FunEqContext -> FParser [FunEq Range] +pFunEq :: FunEqContext -> FParser [PFunEq] pFunEq fectx = do noFail skipWhiteComment faguardM isAtBlockLeft @@ -275,24 +309,24 @@ pFunEq fectx = do else return [] -- | Pass "=" for function definitions and "->" for case clauses. -pRHS :: String -> IParser (RHS Range) +pRHS :: String -> IParser PRHS pRHS sepsym = do -- TODO: parse guards inlineWhite pKeySym0 sepsym <|>> raise Error ("Expected " ++ show sepsym) expr <- pExpr <|>> expectedExpression - return (Plain expr) + return (Plain (extOf expr) expr) -pPattern :: Int -> FParser (Pattern Range) +pPattern :: Int -> FParser PPattern pPattern d = inlineWhite >> pPattern0 d -pPattern0 :: Int -> FParser (Pattern Range) +pPattern0 :: Int -> FParser PPattern pPattern0 d = do pos1 <- gets psCur p0 <- pPatExprAtom0 (max 10 d) climbRight pPattern (pInfixOp Uppercase) POp d pos1 p0 Nothing -pExpr :: FParser (Expr Range) +pExpr :: FParser PExpr pExpr = do inlineWhite -- basics: lit, list, var, con, tup @@ -305,7 +339,7 @@ pExpr = do ,pEIf0 ,pExprOpExpr0 0] -pPatExprAtom0 :: Int -> FParser (Pattern Range) +pPatExprAtom0 :: Int -> FParser PPattern pPatExprAtom0 d = faasum' [pPatWildcard0 ,pPatVarOrAs0 @@ -362,7 +396,7 @@ pPatExprAtom0 d = pos2 <- gets psCur return (PTup (Range pos1 pos2) (p : ps))]] -pELet0 :: FParser (Expr Range) +pELet0 :: FParser PExpr pELet0 = do pos1 <- gets psCur pKeyword "let" @@ -388,7 +422,7 @@ pELet0 = do inlineWhite facatch (do pos2 <- gets psCur raise Error "Expected 'in' after 'let'" - return (ELet (Range pos1 pos2) defs EParseError)) $ do + return (ELet (Range pos1 pos2) defs (EError (Range pos2 pos2)))) $ do pKeyword "in" noFail $ do inlineWhite @@ -396,7 +430,7 @@ pELet0 = do pos2 <- gets psCur return (ELet (Range pos1 pos2) defs body) -pECase0 :: FParser (Expr Range) +pECase0 :: FParser PExpr pECase0 = do pos1 <- gets psCur pKeyword "case" @@ -423,7 +457,7 @@ pECase0 = do pos2 <- gets psCur return (ECase (Range pos1 pos2) e clauses) -pEIf0 :: FParser (Expr Range) +pEIf0 :: FParser PExpr pEIf0 = do pos1 <- gets psCur pKeyword "if" @@ -432,24 +466,26 @@ pEIf0 = do inlineWhite facatch (do pos2 <- gets psCur raise Error "Expected 'then' after 'if'" - return (EIf (Range pos1 pos2) e1 EParseError EParseError)) $ do + let rng = Range pos2 pos2 + return (EIf (Range pos1 pos2) e1 (EError rng) (EError rng))) $ do pKeyword "then" noFail $ do e2 <- pExpr <|>> expectedExpression inlineWhite facatch (do pos2 <- gets psCur raise Error "Expected else after 'then'" - return (EIf (Range pos1 pos2) e1 e2 EParseError)) $ do + let rng = Range pos2 pos2 + return (EIf (Range pos1 pos2) e1 e2 (EError rng))) $ do pKeyword "else" noFail $ do e3 <- pExpr <|>> expectedExpression pos2 <- gets psCur return (EIf (Range pos1 pos2) e1 e2 e3) -pExprOpExpr :: Int -> FParser (Expr Range) +pExprOpExpr :: Int -> FParser PExpr pExprOpExpr d = inlineWhite >> pExprOpExpr0 d -pExprOpExpr0 :: Int -> FParser (Expr Range) +pExprOpExpr0 :: Int -> FParser PExpr pExprOpExpr0 d = do pos1 <- gets psCur e0 <- pEApp0 @@ -478,7 +514,7 @@ climbRight pExpr' pOper makeOp d lhspos lhs mlhsop = pos2 <- gets psCur climbRight pExpr' pOper makeOp d lhspos (makeOp (Range lhspos pos2) lhs op rhs) (Just paop) -pEApp0 :: FParser (Expr Range) +pEApp0 :: FParser PExpr pEApp0 = do pos1 <- gets psCur e1 <- pEAtom0 @@ -488,7 +524,7 @@ pEApp0 = do [] -> return e1 _ -> return (EApp (Range pos1 pos2) e1 es) -pEAtom0 :: FParser (Expr Range) +pEAtom0 :: FParser PExpr pEAtom0 = faasum' [uncurry ELit <$> ranged pLiteral0 ,pEList0 @@ -550,7 +586,7 @@ pStringChar = faasum' return '?' ,do satisfy (\c -> c `notElem` "\n\r\\\'")] -pEList0 :: FParser (Expr Range) +pEList0 :: FParser PExpr pEList0 = do pos1 <- gets psCur char '[' -- special syntax, no need for pKeySym @@ -561,13 +597,13 @@ pEList0 = do pos2 <- gets psCur return (EList (Range pos1 pos2) es) -pEVarOrCon0 :: FParser (Expr Range) +pEVarOrCon0 :: FParser PExpr pEVarOrCon0 = ranged (pIdentifier0 InBlock Don'tCare ()) >>= \case (rng, (Lowercase, name)) -> return (EVar rng name) (rng, (Uppercase, name)) -> return (ECon rng name) -pEParens0 :: FParser (Expr Range) +pEParens0 :: FParser PExpr pEParens0 = do char '(' noFail $ do @@ -576,8 +612,11 @@ pEParens0 = do char ')' <|>> raise Error "Expected closing ')'" return e -expectedExpression :: IParser (Expr Range) -expectedExpression = raise Error "Expected expression" >> return EParseError +expectedExpression :: IParser PExpr +expectedExpression = do + pos <- gets psCur + raise Error "Expected expression" + return (EError (Range pos pos)) data Associativity = AssocLeft | AssocRight | AssocNone deriving (Show, Eq) @@ -609,65 +648,72 @@ pUpperInfixOp0 :: FParser ParsedOperator pUpperInfixOp0 = faasum' [PaOp OCons 5 AssocRight <$> ranged' (pKeySym0 ":")] -pStandaloneTypesig0 :: FParser (Name, Type) +pStandaloneTypesig0 :: FParser (Name, PType) pStandaloneTypesig0 = do name <- pIdentifier0 AtLeft Lowercase WCBacktrack inlineWhite pKeySym0 "::" - noFail $ pushContext ("type signature for " ++ pretty name) $ do - ty <- pType <|>> (raise Error "Expected type" >> return (TTup [])) - return (name, ty) + ty <- pType <|>> (raise Error "Expected type" >> faempty) + return (name, ty) -pType :: FParser Type +pType :: FParser PType pType = do + pos1 <- gets psCur ty1 <- pTypeApp facatch (return ty1) $ do inlineWhite pKeySym0 "->" noFail $ do - ty2 <- pType <|>> (raise Error "Expected type" >> return (TTup [])) - return (TFun ty1 ty2) + pos2 <- gets psCur + ty2 <- pType <|>> (raise Error "Expected type" >> return (TTup (Range pos2 pos2) [])) + return (TFun (Range pos1 pos2) ty1 ty2) -pTypeApp :: FParser Type +pTypeApp :: FParser PType pTypeApp = fasome pTypeAtom >>= \case t :| [] -> return t - t :| ts -> return (TApp t ts) + t :| ts -> return (TApp (foldMapne extOf (t :| ts)) t ts) -pTypeAtom :: FParser Type +pTypeAtom :: FParser PType pTypeAtom = faasum' [pTypeParens, pTypeList, pTypeName] where pTypeParens = do inlineWhite + pos1 <- gets psCur char '(' faasum' [do inlineWhite char ')' - return (TTup []) + pos2 <- gets psCur + return (TTup (Range pos1 pos2) []) ,do ty1 <- pType noFail $ do ty2s <- famany $ do inlineWhite char ',' - noFail $ pType <|>> (raise Error "Expected type" >> return (TTup [])) + pos <- gets psCur + noFail $ pType <|>> (raise Error "Expected type" >> return (TTup (Range pos pos) [])) inlineWhite char ')' <|>> raise Error "Expected closing ')'" + pos2 <- gets psCur case ty2s of [] -> return ty1 - _ -> return (TTup (ty1 : ty2s))] + _ -> return (TTup (Range pos1 pos2) (ty1 : ty2s))] pTypeList = do inlineWhite + pos1 <- gets psCur char '[' ty <- pType - noFail $ char ']' <|>> raise Error "Expecte closing ']'" - return (TList ty) + noFail $ char ']' <|>> raise Error "Expected closing ']'" + pos2 <- gets psCur + return (TList (Range pos1 pos2) ty) pTypeName = do inlineWhite - (cs, name) <- pIdentifier0 InBlock Don'tCare () + (rng, (cs, name)) <- ranged $ pIdentifier0 InBlock Don'tCare () case cs of - Uppercase -> return (TCon name) - Lowercase -> return (TVar name) + Uppercase -> return (TCon rng name) + Lowercase -> return (TVar rng name) -- | Parse the given name-like keyword, ensuring that it is the entire word. pKeyword :: String -> FParser () @@ -702,10 +748,6 @@ type family WithCaseOutput care a where WithCaseOutput 'True a = a WithCaseOutput 'False a = (Case 'True, a) -type family If c a b where - If 'True a b = a - If 'False a b = b - data WrongCaseBacktrack = WCBacktrack -- ^ If a word was found but it had the wrong case, fail and backtrack. | WCAssume -- ^ Be certain that this case is expected here, and assume incorrect diff --git a/src/HSVIS/Typecheck.hs b/src/HSVIS/Typecheck.hs index b1ffbb9..23fb961 100644 --- a/src/HSVIS/Typecheck.hs +++ b/src/HSVIS/Typecheck.hs @@ -1,5 +1,8 @@ {-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE EmptyDataDeriving #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE TypeFamilies #-} module HSVIS.Typecheck where import Control.Monad @@ -7,17 +10,69 @@ import Control.Monad.Reader import Control.Monad.State import Control.Monad.Writer.CPS import Data.Foldable (toList) -import qualified Data.List.NonEmpty as NE +import Data.Map.Strict (Map) import Data.Bag +import Data.List.NonEmpty.Util import HSVIS.AST +import HSVIS.Parser import HSVIS.Diagnostic -typecheck :: FilePath -> String -> Program Range -> ([Diagnostic], Program Type) +data StageTC + +type instance X DataDef StageTC = CType +type instance X FunDef StageTC = CType +type instance X FunEq StageTC = CType +type instance X Kind StageTC = () +type instance X Type StageTC = CKind +type instance X Pattern StageTC = CType +type instance X RHS StageTC = CType +type instance X Expr StageTC = CType + +data instance E Type StageTC = TUniVar Int + deriving (Show) + +type CProgram = Program StageTC +type CDataDef = DataDef StageTC +type CFunDef = FunDef StageTC +type CFunEq = FunEq StageTC +type CKind = Kind StageTC +type CType = Type StageTC +type CPattern = Pattern StageTC +type CRHS = RHS StageTC +type CExpr = Expr StageTC + +data StageTyped + +type instance X DataDef StageTyped = TType +type instance X FunDef StageTyped = TType +type instance X FunEq StageTyped = TType +type instance X Kind StageTyped = () +type instance X Type StageTyped = TKind +type instance X Pattern StageTyped = TType +type instance X RHS StageTyped = TType +type instance X Expr StageTyped = TType + +data instance E t StageTyped + deriving (Show) + +type TProgram = Program StageTyped +type TDataDef = DataDef StageTyped +type TFunDef = FunDef StageTyped +type TFunEq = FunEq StageTyped +type TKind = Kind StageTyped +type TType = Type StageTyped +type TPattern = Pattern StageTyped +type TRHS = RHS StageTyped +type TExpr = Expr StageTyped + + +typecheck :: FilePath -> String -> Program Range -> ([Diagnostic], Program TType) typecheck fp source prog = let (progtc, (ds1, cs)) = runWriter + . flip evalStateT (Env mempty mempty) . flip evalStateT 1 . flip runReaderT (fp, source) . runTCM @@ -26,9 +81,18 @@ typecheck fp source prog = in (toList (ds1 <> ds2), substProg sub progtc) data Constr = - CEq Type Type Range -- ^ These types must be equal because of the expression here + CEq CType CType Range -- ^ These types must be equal because of the expression here + deriving (Show) + +data Env = Env (Map Name CKind) (Map Name CType) + deriving (Show) -newtype TCM a = TCM { runTCM :: ReaderT (FilePath, String) (StateT Int (Writer (Bag Diagnostic, Bag Constr))) a } +newtype TCM a = TCM { runTCM :: + ReaderT (FilePath, String) + (StateT Int + (StateT Env + (Writer (Bag Diagnostic, Bag Constr)))) + a } deriving newtype (Functor, Applicative, Monad) raise :: Range -> String -> TCM () @@ -36,28 +100,50 @@ raise rng@(Range (Pos y _) _) msg = do (fp, source) <- ask TCM $ lift $ lift $ tell (pure (Diagnostic fp rng [] (source !! y) msg), mempty) -tcProgram :: Program Range -> TCM (Program TCType) -tcProgram (Program ddefs fdefs) = Program ddefs <$> traverse tcFunDef fdefs +modifyTEnv :: (Map Name CKind -> Map Name CKind) -> TCM () +modifyTEnv f = TCM $ lift $ lift $ modify (\(Env a b) -> Env (f a) b) -tcFunDef :: FunDef Range -> TCM (FunDef TCType) -tcFunDef (FunDef name msig eqs) = do +modifyVEnv :: (Map Name CType -> Map Name CType) -> TCM () +modifyVEnv f = TCM $ lift $ lift $ modify (\(Env a b) -> Env a (f b)) + +genUniVar :: CKind -> TCM CType +genUniVar k = TCM $ lift $ state (\i -> (TExt k (TUniVar i), i + 1)) + +tcProgram :: PProgram -> TCM CProgram +tcProgram (Program ddefs fdefs) = do + -- TODO: add preliminary kinds for the data definitions to the environment, + -- then solve for the kind variables in checkDataDef + + Program <$> traverse checkDataDef ddefs <*> traverse tcFunDef fdefs + +checkDataDef :: PDataDef -> TCM CDataDef +checkDataDef (DataDef rng name params cons) = do + _ + +tcFunDef :: PFunDef -> TCM CFunDef +tcFunDef (FunDef rng name msig eqs) = do when (not $ allEq (fmap (length . funeqPats) eqs)) $ - raise (sconcatne (fmap funeqRange eqs)) "Function equations have differing numbers of arguments" + raise (sconcatne (fmap extOf eqs)) "Function equations have differing numbers of arguments" + + typ <- case msig of + Just sig -> checkType sig + Nothing -> genUniVar (KType ()) _ +checkType :: PType -> TCM CType +checkType = \case + TApp r t ts -> _ + TTup r ts -> _ + TList r t -> _ + TFun r s t -> _ + TCon r n -> _ + TVar r n -> _ + allEq :: (Eq a, Foldable t) => t a -> Bool allEq l = case toList l of [] -> True x : xs -> all (== x) xs -funeqRange :: FunEq t -> t -funeqRange (FunEq rng _ _ _) = rng - funeqPats :: FunEq t -> [Pattern t] funeqPats (FunEq _ _ pats _) = pats - -sconcatne :: Semigroup a => NE.NonEmpty a -> a -sconcatne = \(x NE.:| xs) -> go x xs - where go a [] = a - go a (x : xs) = go (a <> x) xs -- cgit v1.2.3-70-g09d2