diff --git a/DDC/Source/Tetra/Compounds.hs b/DDC/Source/Tetra/Compounds.hs --- a/DDC/Source/Tetra/Compounds.hs +++ b/DDC/Source/Tetra/Compounds.hs @@ -1,4 +1,6 @@ +{-# LANGUAGE TypeFamilies #-} +-- | Utilities for constructing and destructing Source Tetra expressions. module DDC.Source.Tetra.Compounds ( module DDC.Type.Compounds , takeAnnotOfExp @@ -21,6 +23,10 @@ , takeXConApps , takeXPrimApps + -- * Casts + , xBox + , xRun + -- * Data Constructors , dcUnit , takeNameOfDaCon @@ -28,17 +34,24 @@ -- * Patterns , bindsOfPat + , pTrue + , pFalse -- * Witnesses , wApp , wApps , takeXWitness , takeWAppsAsList - , takePrimWiConApps) + , takePrimWiConApps + + -- * Primitives + , xErrorDefault) where import DDC.Source.Tetra.Exp +import DDC.Source.Tetra.Prim import DDC.Type.Compounds -import DDC.Core.Compounds +import Data.Text (Text) +import DDC.Core.Exp.Annot.Compounds ( dcUnit , takeNameOfDaCon , takeTypeOfDaCon @@ -51,13 +64,15 @@ , takeWAppsAsList , takePrimWiConApps) + -- Annotations ---------------------------------------------------------------- -- | Take the outermost annotation from an expression, -- or Nothing if this is an `XType` or `XWitness` without an annotation. -takeAnnotOfExp :: Exp a n -> Maybe a +takeAnnotOfExp :: GExp l -> Maybe (GAnnot l) takeAnnotOfExp xx = case xx of XVar a _ -> Just a + XPrim a _ -> Just a XCon a _ -> Just a XLAM a _ _ -> Just a XLam a _ _ -> Just a @@ -74,20 +89,20 @@ -- Lambdas --------------------------------------------------------------------- -- | Make some nested type lambdas. -xLAMs :: a -> [Bind n] -> Exp a n -> Exp a n +xLAMs :: GAnnot l -> [GBind l] -> GExp l -> GExp l xLAMs a bs x = foldr (XLAM a) x bs -- | Make some nested value or witness lambdas. -xLams :: a -> [Bind n] -> Exp a n -> Exp a n +xLams :: GAnnot l -> [GBind l] -> GExp l -> GExp l xLams a bs x = foldr (XLam a) x bs -- | Split type lambdas from the front of an expression, -- or `Nothing` if there aren't any. -takeXLAMs :: Exp a n -> Maybe ([Bind n], Exp a n) +takeXLAMs :: GExp l -> Maybe ([GBind l], GExp l) takeXLAMs xx = let go bs (XLAM _ b x) = go (b:bs) x go bs x = (reverse bs, x) @@ -98,7 +113,7 @@ -- | Split nested value or witness lambdas from the front of an expression, -- or `Nothing` if there aren't any. -takeXLams :: Exp a n -> Maybe ([Bind n], Exp a n) +takeXLams :: GExp l -> Maybe ([GBind l], GExp l) takeXLams xx = let go bs (XLam _ b x) = go (b:bs) x go bs x = (reverse bs, x) @@ -110,7 +125,7 @@ -- | Make some nested lambda abstractions, -- using a flag to indicate whether the lambda is a -- level-1 (True), or level-0 (False) binder. -makeXLamFlags :: a -> [(Bool, Bind n)] -> Exp a n -> Exp a n +makeXLamFlags :: GAnnot l -> [(Bool, GBind l)] -> GExp l -> GExp l makeXLamFlags a fbs x = foldr (\(f, b) x' -> if f then XLAM a b x' @@ -121,7 +136,7 @@ -- | Split nested lambdas from the front of an expression, -- with a flag indicating whether the lambda was a level-1 (True), -- or level-0 (False) binder. -takeXLamFlags :: Exp a n -> Maybe ([(Bool, Bind n)], Exp a n) +takeXLamFlags :: GExp l -> Maybe ([(Bool, GBind l)], GExp l) takeXLamFlags xx = let go bs (XLAM _ b x) = go ((True, b):bs) x go bs (XLam _ b x) = go ((False, b):bs) x @@ -133,14 +148,14 @@ -- Applications --------------------------------------------------------------- -- | Build sequence of value applications. -xApps :: a -> Exp a n -> [Exp a n] -> Exp a n +xApps :: GAnnot l -> GExp l -> [GExp l] -> GExp l xApps a t1 ts = foldl (XApp a) t1 ts -- | Build sequence of applications. -- Similar to `xApps` but also takes list of annotations for -- the `XApp` constructors. -makeXAppsWithAnnots :: Exp a n -> [(Exp a n, a)] -> Exp a n +makeXAppsWithAnnots :: GExp l -> [(GExp l, GAnnot l)] -> GExp l makeXAppsWithAnnots f xas = case xas of [] -> f @@ -150,7 +165,7 @@ -- | Flatten an application into the function part and its arguments. -- -- Returns `Nothing` if there is no outer application. -takeXApps :: Exp a n -> Maybe (Exp a n, [Exp a n]) +takeXApps :: GExp l -> Maybe (GExp l, [GExp l]) takeXApps xx = case takeXAppsAsList xx of (x1 : xsArgs) -> Just (x1, xsArgs) @@ -160,7 +175,7 @@ -- | Flatten an application into the function part and its arguments. -- -- This is like `takeXApps` above, except we know there is at least one argument. -takeXApps1 :: Exp a n -> Exp a n -> (Exp a n, [Exp a n]) +takeXApps1 :: GExp l -> GExp l -> (GExp l, [GExp l]) takeXApps1 x1 x2 = case takeXApps x1 of Nothing -> (x1, [x2]) @@ -168,7 +183,7 @@ -- | Flatten an application into the function parts and arguments, if any. -takeXAppsAsList :: Exp a n -> [Exp a n] +takeXAppsAsList :: GExp l -> [GExp l] takeXAppsAsList xx = case xx of XApp _ x1 x2 -> takeXAppsAsList x1 ++ [x2] @@ -177,7 +192,7 @@ -- | Destruct sequence of applications. -- Similar to `takeXAppsAsList` but also keeps annotations for later. -takeXAppsWithAnnots :: Exp a n -> (Exp a n, [(Exp a n, a)]) +takeXAppsWithAnnots :: GExp l -> (GExp l, [(GExp l, GAnnot l)]) takeXAppsWithAnnots xx = case xx of XApp a f arg @@ -191,18 +206,39 @@ -- and its arguments. -- -- Returns `Nothing` if the expression isn't a primop application. -takeXPrimApps :: Exp a n -> Maybe (n, [Exp a n]) +takeXPrimApps :: GExp l -> Maybe (GPrim l, [GExp l]) takeXPrimApps xx = case takeXAppsAsList xx of - XVar _ (UPrim p _) : xs -> Just (p, xs) - _ -> Nothing + XPrim _ p : xs -> Just (p, xs) + _ -> Nothing -- | Flatten an application of a data constructor into the constructor -- and its arguments. -- -- Returns `Nothing` if the expression isn't a constructor application. -takeXConApps :: Exp a n -> Maybe (DaCon n, [Exp a n]) +takeXConApps :: GExp l -> Maybe (DaCon (GName l), [GExp l]) takeXConApps xx = case takeXAppsAsList xx of XCon _ dc : xs -> Just (dc, xs) _ -> Nothing + + +-- Casts ---------------------------------------------------------------------- +xBox a x = XCast a CastBox x +xRun a x = XCast a CastRun x + + +-- Primitives ----------------------------------------------------------------- +xErrorDefault :: (GPrim l ~ PrimVal, GName l ~ Name) + => GAnnot l -> Text -> Integer -> GExp l +xErrorDefault a name n + = xApps a + (XPrim a (PrimValError OpErrorDefault)) + [ XCon a (DaConPrim (NameLitTextLit name) (tBot kData)) + , XCon a (DaConPrim (NameLitNat n) (tBot kData))] + +-- Patterns ------------------------------------------------------------------- +pTrue = PData (DaConPrim (NameLitBool True) tBool) [] +pFalse = PData (DaConPrim (NameLitBool False) tBool) [] + + diff --git a/DDC/Source/Tetra/Convert.hs b/DDC/Source/Tetra/Convert.hs new file mode 100644 --- /dev/null +++ b/DDC/Source/Tetra/Convert.hs @@ -0,0 +1,515 @@ +{-# LANGUAGE TypeFamilies #-} + +-- | Source Tetra conversion to Disciple Core Tetra language. +module DDC.Source.Tetra.Convert + ( ConvertM + , ErrorConvert (..) + , coreOfSourceModule + , runConvertM) +where +import DDC.Source.Tetra.Convert.Error +import DDC.Data.SourcePos + +import qualified DDC.Source.Tetra.Transform.Guards as S +import qualified DDC.Source.Tetra.Module as S +import qualified DDC.Source.Tetra.DataDef as S +import qualified DDC.Source.Tetra.Env as S +import qualified DDC.Source.Tetra.Compounds as S +import qualified DDC.Source.Tetra.Exp.Annot as S +import qualified DDC.Source.Tetra.Prim as S + +import qualified DDC.Core.Tetra.Prim as C +import qualified DDC.Core.Module as C +import qualified DDC.Core.Exp.Annot as C +import qualified DDC.Type.DataDef as C + +import qualified DDC.Type.Exp as T +import qualified DDC.Type.Sum as Sum +import qualified Data.Text as Text +import Data.Maybe + + +import DDC.Core.Module + ( ExportSource (..) + , ImportType (..) + , ImportCap (..) + , ImportValue (..)) + + +--------------------------------------------------------------------------------------------------- +type ConvertM a x + = Either (ErrorConvert a) x + +type SP = SourcePos + + +-- | Run a conversion computation. +runConvertM :: ConvertM a x -> Either (ErrorConvert a) x +runConvertM cc = cc + +-- | Convert a Source Tetra module to Core Tetra. +coreOfSourceModule + :: SP + -> S.Module (S.Annot SP) + -> Either (ErrorConvert SP) (C.Module SP C.Name) + +coreOfSourceModule a mm + = runConvertM + $ coreOfSourceModuleM a mm + + +-- Module ----------------------------------------------------------------------------------------- +-- | Convert a Source Tetra module to Core Tetra. +-- +-- The Source code needs to already have been desugared and cannot contain, +-- and `XDefix`, `XInfixOp`, or `XInfixVar` nodes, else `error`. +-- +-- We use the map of core headers to add imports for all the names that this +-- module uses from its environment. +-- +coreOfSourceModuleM + :: SP + -> S.Module (S.Annot SP) + -> ConvertM SP (C.Module SP C.Name) + +coreOfSourceModuleM a mm + = do + -- Exported types and values. + exportTypes' <- sequence + $ fmap (\n + -> (,) <$> (pure $ toCoreN n) + <*> (pure $ ExportSourceLocalNoType (toCoreN n))) + $ S.moduleExportTypes mm + + exportValues' <- sequence + $ fmap (\n + -> (,) <$> (pure $ toCoreN n) + <*> (pure $ ExportSourceLocalNoType (toCoreN n))) + $ S.moduleExportValues mm + + -- Imported types and values. + importTypes' <- sequence + $ fmap (\(n, it) + -> (,) <$> (pure $ toCoreN n) <*> (toCoreImportType it)) + $ S.moduleImportTypes mm + + importCaps' <- sequence + $ fmap (\(n, iv) + -> (,) <$> (pure $ toCoreN n) <*> (toCoreImportCap iv)) + $ S.moduleImportCaps mm + + importValues' <- sequence + $ fmap (\(n, iv) + -> (,) <$> (pure $ toCoreN n) <*> (toCoreImportValue iv)) + $ S.moduleImportValues mm + + -- Data type definitions. + dataDefsLocal <- sequence $ fmap toCoreDataDef + $ [ def | S.TopData _ def <- S.moduleTops mm ] + + -- Top level bindings. + ltsTops <- letsOfTops $ S.moduleTops mm + + return + $ C.ModuleCore + { C.moduleName = S.moduleName mm + , C.moduleIsHeader = False + + , C.moduleExportTypes = exportTypes' + + , C.moduleExportValues + = exportValues' + ++ (if C.isMainModuleName (S.moduleName mm) + && (not $ elem (S.NameVar "main") $ S.moduleExportValues mm) + then [ ( C.NameVar "main" + , ExportSourceLocalNoType (C.NameVar "main"))] + else []) + + , C.moduleImportTypes = importTypes' + , C.moduleImportCaps = importCaps' + , C.moduleImportValues = importValues' + , C.moduleImportDataDefs = [] + , C.moduleDataDefsLocal = dataDefsLocal + , C.moduleBody = C.XLet a ltsTops (C.xUnit a) } + + +-- | Extract the top-level bindings from some source definitions. +letsOfTops :: [S.Top (S.Annot SP)] + -> ConvertM SP (C.Lets SP C.Name) +letsOfTops tops + = C.LRec <$> (sequence $ mapMaybe bindOfTop tops) + + +-- | Try to convert a `TopBind` to a top-level binding, +-- or `Nothing` if it isn't one. +bindOfTop + :: S.Top (S.Annot SP) + -> Maybe (ConvertM SP (T.Bind C.Name, C.Exp SP C.Name)) + +bindOfTop (S.TopClause _ (S.SLet _ b [] [S.GExp x])) + = Just ((,) <$> toCoreB b <*> toCoreX x) + +bindOfTop _ + = Nothing + + +-- ImportType ------------------------------------------------------------------------------------- +toCoreImportType :: ImportType S.Name -> ConvertM a (ImportType C.Name) +toCoreImportType src + = case src of + ImportTypeAbstract t + -> ImportTypeAbstract <$> toCoreT t + + ImportTypeBoxed t + -> ImportTypeBoxed <$> toCoreT t + + +-- ImportCap -------------------------------------------------------------------------------------- +toCoreImportCap :: ImportCap S.Name -> ConvertM a (ImportCap C.Name) +toCoreImportCap src + = case src of + ImportCapAbstract t + -> ImportCapAbstract <$> toCoreT t + + +-- ImportValue ------------------------------------------------------------------------------------ +toCoreImportValue :: ImportValue S.Name -> ConvertM a (ImportValue C.Name) +toCoreImportValue src + = case src of + ImportValueModule mn n t mA + -> ImportValueModule + <$> (pure mn) <*> (pure $ toCoreN n) <*> toCoreT t <*> pure mA + + ImportValueSea v t + -> ImportValueSea + <$> pure v <*> toCoreT t + + +-- Type ------------------------------------------------------------------------------------------- +toCoreT :: T.Type S.Name -> ConvertM a (T.Type C.Name) +toCoreT tt + = case tt of + T.TVar u + -> T.TVar <$> toCoreU u + + T.TCon tc + -> T.TCon <$> toCoreTC tc + + T.TForall b t + -> T.TForall <$> toCoreB b <*> toCoreT t + + T.TApp t1 t2 + -> T.TApp <$> toCoreT t1 <*> toCoreT t2 + + T.TSum ts + -> do k' <- toCoreT $ Sum.kindOfSum ts + + tss' <- fmap (Sum.fromList k') + $ sequence $ fmap toCoreT $ Sum.toList ts + + return $ T.TSum tss' + + +-- TyCon ------------------------------------------------------------------------------------------ +toCoreTC :: T.TyCon S.Name -> ConvertM a (T.TyCon C.Name) +toCoreTC tc + = case tc of + T.TyConSort sc + -> pure $ T.TyConSort sc + + T.TyConKind kc + -> pure $ T.TyConKind kc + + T.TyConWitness wc + -> pure $ T.TyConWitness wc + + T.TyConSpec sc + -> pure $ T.TyConSpec sc + + T.TyConBound u k + -> T.TyConBound <$> toCoreU u <*> toCoreT k + + T.TyConExists n k + -> T.TyConExists <$> pure n <*> toCoreT k + + +-- DataDef ---------------------------------------------------------------------------------------- +toCoreDataDef :: S.DataDef S.Name -> ConvertM a (C.DataDef C.Name) +toCoreDataDef def + = do + defParams <- sequence $ fmap toCoreB $ S.dataDefParams def + + defCtors <- sequence $ fmap (\(ctor, tag) -> toCoreDataCtor def tag ctor) + $ [(ctor, tag) | ctor <- S.dataDefCtors def + | tag <- [0..]] + + return $ C.DataDef + { C.dataDefTypeName = toCoreN $ S.dataDefTypeName def + , C.dataDefParams = defParams + , C.dataDefCtors = Just $ defCtors + , C.dataDefIsAlgebraic = True } + + +-- DataCtor --------------------------------------------------------------------------------------- +toCoreDataCtor + :: S.DataDef S.Name + -> Integer + -> S.DataCtor S.Name + -> ConvertM a (C.DataCtor C.Name) + +toCoreDataCtor dataDef tag ctor + = do typeParams <- sequence $ fmap toCoreB $ S.dataDefParams dataDef + fieldTypes <- sequence $ fmap toCoreT $ S.dataCtorFieldTypes ctor + resultType <- toCoreT (S.dataCtorResultType ctor) + + return $ C.DataCtor + { C.dataCtorName = toCoreN (S.dataCtorName ctor) + , C.dataCtorTag = tag + , C.dataCtorFieldTypes = fieldTypes + , C.dataCtorResultType = resultType + , C.dataCtorTypeName = toCoreN (S.dataDefTypeName dataDef) + , C.dataCtorTypeParams = typeParams } + + +-- Exp -------------------------------------------------------------------------------------------- +toCoreX :: S.Exp SP -> ConvertM SP (C.Exp SP C.Name) +toCoreX xx + = case xx of + S.XVar a u + -> C.XVar <$> pure a <*> toCoreU u + + -- Wrap text literals into Text during conversion to Core. + -- The 'textLit' variable refers to whatever is in scope. + S.XCon a dc@(C.DaConPrim (S.NameLitTextLit{}) _) + -> C.XApp <$> pure a + <*> (C.XVar <$> pure a <*> (pure $ C.UName (C.NameVar "textLit"))) + <*> (C.XCon <$> pure a <*> (toCoreDC dc)) + + S.XPrim a p + -> C.XVar <$> pure a <*> toCoreU (C.UPrim (S.NameVal p) (S.typeOfPrimVal p)) + + S.XCon a dc + -> C.XCon <$> pure a <*> toCoreDC dc + + S.XLAM a b x + -> C.XLAM <$> pure a <*> toCoreB b <*> toCoreX x + + S.XLam a b x + -> C.XLam <$> pure a <*> toCoreB b <*> toCoreX x + + -- We don't want to wrap the source file path passed to the default# prim + -- in a Text constructor, so detect this case separately. + S.XApp a0 _ _ + | Just ( p@(S.PrimValError S.OpErrorDefault) + , [S.XCon a1 dc1, S.XCon a2 dc2]) + <- S.takeXPrimApps xx + -> do xPrim' <- toCoreX (S.XPrim a0 p) + dc1' <- toCoreDC dc1 + dc2' <- toCoreDC dc2 + return $ C.xApps a0 xPrim' [C.XCon a1 dc1', C.XCon a2 dc2'] + + S.XApp a x1 x2 + -> C.XApp <$> pure a <*> toCoreX x1 <*> toCoreX x2 + + S.XLet a lts x + -> C.XLet <$> pure a <*> toCoreLts lts <*> toCoreX x + + S.XCase a x alts + -> C.XCase <$> pure a <*> toCoreX x <*> (sequence $ map (toCoreA a) alts) + + S.XCast a c x + -> C.XCast <$> pure a <*> toCoreC c <*> toCoreX x + + S.XType a t + -> C.XType <$> pure a <*> toCoreT t + + S.XWitness a w + -> C.XWitness <$> pure a <*> toCoreW w + + -- These shouldn't exist in the desugared source tetra code. + S.XDefix{} -> Left $ ErrorConvertCannotConvertSugarExp xx + S.XInfixOp{} -> Left $ ErrorConvertCannotConvertSugarExp xx + S.XInfixVar{} -> Left $ ErrorConvertCannotConvertSugarExp xx + + +-- Lets ------------------------------------------------------------------------------------------- +toCoreLts :: S.Lets SP -> ConvertM SP (C.Lets SP C.Name) +toCoreLts lts + = case lts of + S.LLet b x + -> C.LLet <$> toCoreB b <*> toCoreX x + + S.LRec bxs + -> C.LRec <$> (sequence $ map (\(b, x) -> (,) <$> toCoreB b <*> toCoreX x) bxs) + + S.LPrivate bks Nothing bts + -> C.LPrivate <$> (sequence $ fmap toCoreB bks) + <*> pure Nothing + <*> (sequence $ fmap toCoreB bts) + + S.LPrivate bks (Just tParent) bts + -> C.LPrivate <$> (sequence $ fmap toCoreB bks) + <*> (fmap Just $ toCoreT tParent) + <*> (sequence $ fmap toCoreB bts) + + S.LGroup{} + -> Left $ ErrorConvertCannotConvertSugarLets lts + + +-- Cast ------------------------------------------------------------------------------------------- +toCoreC :: S.Cast a -> ConvertM a (C.Cast a C.Name) +toCoreC cc + = case cc of + S.CastWeakenEffect eff + -> C.CastWeakenEffect <$> toCoreT eff + + S.CastPurify w + -> C.CastPurify <$> toCoreW w + + S.CastBox + -> pure C.CastBox + + S.CastRun + -> pure C.CastRun + + +-- Alt -------------------------------------------------------------------------------------------- +toCoreA :: SP -> S.Alt SP -> ConvertM SP (C.Alt SP C.Name) +toCoreA sp (S.AAlt w gxs) + = C.AAlt <$> toCoreP w + <*> (toCoreX $ S.desugarGuards sp gxs + $ S.xErrorDefault sp + (Text.pack $ sourcePosSource sp) + (fromIntegral $ sourcePosLine sp)) + + +-- Pat -------------------------------------------------------------------------------------------- +toCoreP :: S.Pat a -> ConvertM a (C.Pat C.Name) +toCoreP pp + = case pp of + S.PDefault + -> pure C.PDefault + + S.PData dc bs + -> C.PData <$> toCoreDC dc <*> (sequence $ fmap toCoreB bs) + + +-- DaCon ------------------------------------------------------------------------------------------ +toCoreDC :: S.DaCon S.Name -> ConvertM a (C.DaCon C.Name) +toCoreDC dc + = case dc of + S.DaConUnit + -> pure $ C.DaConUnit + + S.DaConPrim n t + -> C.DaConPrim <$> (pure $ toCoreN n) <*> toCoreT t + + S.DaConBound n + -> C.DaConBound <$> (pure $ toCoreN n) + + +-- Witness ---------------------------------------------------------------------------------------- +toCoreW :: S.Witness a -> ConvertM a (C.Witness a C.Name) +toCoreW ww + = case ww of + S.WVar a u + -> C.WVar <$> pure a <*> toCoreU u + + S.WCon a wc + -> C.WCon <$> pure a <*> toCoreWC wc + + S.WApp a w1 w2 + -> C.WApp <$> pure a <*> toCoreW w1 <*> toCoreW w2 + + S.WType a t + -> C.WType <$> pure a <*> toCoreT t + + +-- WiCon ------------------------------------------------------------------------------------------ +toCoreWC :: S.WiCon a -> ConvertM a (C.WiCon C.Name) +toCoreWC wc + = case wc of + S.WiConBound u t + -> C.WiConBound <$> toCoreU u <*> toCoreT t + + +-- Bind ------------------------------------------------------------------------------------------- +toCoreB :: S.Bind -> ConvertM a (C.Bind C.Name) +toCoreB bb + = case bb of + T.BName n t + -> T.BName <$> (pure $ toCoreN n) <*> toCoreT t + + T.BAnon t + -> T.BAnon <$> toCoreT t + + T.BNone t + -> T.BNone <$> toCoreT t + + +-- Bound ------------------------------------------------------------------------------------------ +toCoreU :: S.Bound -> ConvertM a (C.Bound C.Name) +toCoreU uu + = case uu of + T.UName n + -> T.UName <$> (pure $ toCoreN n) + + T.UIx i + -> T.UIx <$> (pure i) + + T.UPrim n t + -> T.UPrim <$> (pure $ toCoreN n) <*> toCoreT t + + +-- Name ------------------------------------------------------------------------------------------- +toCoreN :: S.Name -> C.Name +toCoreN nn + = case nn of + S.NameVar str + -> C.NameVar str + + S.NameCon str + -> C.NameCon str + + S.NamePrim (S.PrimNameType (S.PrimTypeTyConTetra tc)) + -> C.NameTyConTetra (toCoreTyConTetra tc) + + S.NamePrim (S.PrimNameType (S.PrimTypeTyCon p)) + -> C.NamePrimTyCon p + + S.NamePrim (S.PrimNameVal (S.PrimValLit lit)) + -> case lit of + S.PrimLitBool x -> C.NameLitBool x + S.PrimLitNat x -> C.NameLitNat x + S.PrimLitInt x -> C.NameLitInt x + S.PrimLitSize x -> C.NameLitSize x + S.PrimLitWord x s -> C.NameLitWord x s + S.PrimLitFloat x s -> C.NameLitFloat x s + S.PrimLitTextLit x -> C.NameLitTextLit x + + S.NamePrim (S.PrimNameVal (S.PrimValArith p)) + -> C.NamePrimArith p False + + S.NamePrim (S.PrimNameVal (S.PrimValVector p)) + -> C.NameOpVector p False + + S.NamePrim (S.PrimNameVal (S.PrimValFun p)) + -> C.NameOpFun p + + S.NamePrim (S.PrimNameVal (S.PrimValError p)) + -> C.NameOpError p False + + S.NameHole + -> C.NameHole + + +-- | Convert a Tetra specific type constructor to core. +toCoreTyConTetra :: S.PrimTyConTetra -> C.TyConTetra +toCoreTyConTetra tc + = case tc of + S.PrimTyConTetraTuple n -> C.TyConTetraTuple n + S.PrimTyConTetraVector -> C.TyConTetraVector + S.PrimTyConTetraF -> C.TyConTetraF + S.PrimTyConTetraC -> C.TyConTetraC + S.PrimTyConTetraU -> C.TyConTetraU + diff --git a/DDC/Source/Tetra/Convert/Error.hs b/DDC/Source/Tetra/Convert/Error.hs new file mode 100644 --- /dev/null +++ b/DDC/Source/Tetra/Convert/Error.hs @@ -0,0 +1,27 @@ + +module DDC.Source.Tetra.Convert.Error + (ErrorConvert (..)) +where +import DDC.Source.Tetra.Pretty +import qualified DDC.Source.Tetra.Exp.Annot as S + + +data ErrorConvert a + -- | Cannot convert sugar expression to core. + = ErrorConvertCannotConvertSugarExp (S.Exp a) + + -- | Cannot convert sugar let bindings to core. + | ErrorConvertCannotConvertSugarLets (S.Lets a) + + +instance Pretty a => Pretty (ErrorConvert a) where + ppr err + = case err of + ErrorConvertCannotConvertSugarExp xx + -> vcat [ text "Cannot desugar expression" + , indent 2 $ ppr xx ] + + ErrorConvertCannotConvertSugarLets xx + -> vcat [ text "Cannot desugar let-bindings" + , indent 2 $ ppr xx ] + diff --git a/DDC/Source/Tetra/DataDef.hs b/DDC/Source/Tetra/DataDef.hs --- a/DDC/Source/Tetra/DataDef.hs +++ b/DDC/Source/Tetra/DataDef.hs @@ -1,4 +1,5 @@ +-- | Source Tetra data type definitions. module DDC.Source.Tetra.DataDef ( -- * Data Type Definition. DataDef (..) @@ -29,9 +30,11 @@ , dataDefCtors :: [DataCtor n] } deriving Show -instance NFData (DataDef n) +instance NFData (DataDef n) where + rnf !_ = () + -- | Take the types of data constructors from a data type definition. typeEnvOfDataDef :: Ord n => DataDef n -> TypeEnv n typeEnvOfDataDef def @@ -56,7 +59,8 @@ deriving Show -instance NFData (DataCtor n) +instance NFData (DataCtor n) where + rnf !_ = () -- | Get the type of a data constructor. diff --git a/DDC/Source/Tetra/Env.hs b/DDC/Source/Tetra/Env.hs --- a/DDC/Source/Tetra/Env.hs +++ b/DDC/Source/Tetra/Env.hs @@ -1,10 +1,21 @@ +-- | Source Tetra primitive type and kind environments. module DDC.Source.Tetra.Env - ( primKindEnv - , primTypeEnv ) + ( -- * Primitive kind environment. + primKindEnv + , kindOfPrimName + + -- * Primitive type environment. + , primTypeEnv + , typeOfPrimName + , typeOfPrimVal + , typeOfPrimLit + + , dataDefBool) where import DDC.Source.Tetra.Prim import DDC.Source.Tetra.Exp +import DDC.Type.DataDef import DDC.Type.Env (Env) import qualified DDC.Type.Env as Env @@ -22,7 +33,7 @@ kindOfPrimName :: Name -> Maybe (Kind Name) kindOfPrimName nn = case nn of - NamePrimTyCon tc -> Just $ kindPrimTyCon tc + NameTyCon tc -> Just $ kindPrimTyCon tc _ -> Nothing @@ -35,13 +46,41 @@ -- | Take the type of a name, -- or `Nothing` if this is not a value name. typeOfPrimName :: Name -> Maybe (Type Name) -typeOfPrimName dc +typeOfPrimName nn + = case nn of + NameVal n -> Just $ typeOfPrimVal n + _ -> Nothing + + +-- | Take the type of a primitive name. +typeOfPrimVal :: PrimVal -> Type Name +typeOfPrimVal dc = case dc of - NamePrimArith p -> Just $ typePrimArith p + PrimValLit l -> typeOfPrimLit l + PrimValArith p -> typePrimArith p + PrimValError p -> typeOpError p + PrimValVector p -> typeOpVector p + PrimValFun p -> typeOpFun p - NameLitBool _ -> Just $ tBool - NameLitNat _ -> Just $ tNat - NameLitInt _ -> Just $ tInt - NameLitWord _ bits -> Just $ tWord bits - _ -> Nothing +-- | Take the type of a primitive literal. +typeOfPrimLit :: PrimLit -> Type Name +typeOfPrimLit pl + = case pl of + PrimLitBool _ -> tBool + PrimLitNat _ -> tNat + PrimLitInt _ -> tInt + PrimLitSize _ -> tSize + PrimLitFloat _ bits -> tFloat bits + PrimLitWord _ bits -> tWord bits + PrimLitTextLit _ -> tTextLit + + +-- | Data type definition for `Bool`. +dataDefBool :: DataDef Name +dataDefBool + = makeDataDefAlg (NameTyCon PrimTyConBool) + [] + (Just [ (NameLitBool True, []) + , (NameLitBool False, []) ]) + diff --git a/DDC/Source/Tetra/Exp.hs b/DDC/Source/Tetra/Exp.hs --- a/DDC/Source/Tetra/Exp.hs +++ b/DDC/Source/Tetra/Exp.hs @@ -1,23 +1,31 @@ +-- | Definition of Source Tetra Expressions. module DDC.Source.Tetra.Exp ( module DDC.Type.Exp -- * Expressions - , Exp (..) - , Lets (..) - , Alt (..) - , Pat (..) - , Cast (..) + , GName + , GAnnot + , GBind + , GBound + , GPrim + , GExp (..) + , GLets (..) + , GAlt (..) + , GPat (..) + , GClause (..) + , GGuardedExp (..) + , GGuard (..) + , GCast (..) + , DaCon (..) -- * Witnesses - , Witness (..) - - -- * Data Constructors - , DaCon (..) + , GWitness (..) + , GWiCon (..) - -- * Witness Constructors - , WiCon (..) - , WbCon (..)) + -- * Dictionaries + , ShowLanguage + , NFDataLanguage) where import DDC.Type.Exp -import DDC.Source.Tetra.Exp.Base +import DDC.Source.Tetra.Exp.Generic diff --git a/DDC/Source/Tetra/Exp/Annot.hs b/DDC/Source/Tetra/Exp/Annot.hs new file mode 100644 --- /dev/null +++ b/DDC/Source/Tetra/Exp/Annot.hs @@ -0,0 +1,54 @@ +{-# LANGUAGE TypeFamilies #-} +module DDC.Source.Tetra.Exp.Annot + ( module DDC.Source.Tetra.Exp.Generic + , Annot + , HasAnonBind (..) + + -- * Expressions + , Name + , Bound + , Bind + , Exp + , Lets + , Alt + , Pat + , Clause + , GuardedExp + , Guard + , Cast + , DaCon (..) + + -- * Witnesses + , Witness + , WiCon) +where +import DDC.Source.Tetra.Exp.Generic +import DDC.Source.Tetra.Prim +import qualified DDC.Type.Exp as T + + +-- | Type index for annotated expression type. +data Annot a + +instance HasAnonBind (Annot a) where + isAnon _ (T.BAnon _) = True + isAnon _ _ = False + +type instance GName (Annot a) = Name +type instance GAnnot (Annot a) = a +type instance GBind (Annot a) = T.Bind Name +type instance GBound (Annot a) = T.Bound Name +type instance GPrim (Annot a) = PrimVal + +type Bound = T.Bound Name +type Bind = T.Bind Name +type Exp a = GExp (Annot a) +type Lets a = GLets (Annot a) +type Alt a = GAlt (Annot a) +type Pat a = GPat (Annot a) +type Clause a = GClause (Annot a) +type GuardedExp a = GGuardedExp (Annot a) +type Guard a = GGuard (Annot a) +type Cast a = GCast (Annot a) +type Witness a = GWitness (Annot a) +type WiCon a = GWiCon (Annot a) diff --git a/DDC/Source/Tetra/Exp/Base.hs b/DDC/Source/Tetra/Exp/Base.hs deleted file mode 100644 --- a/DDC/Source/Tetra/Exp/Base.hs +++ /dev/null @@ -1,168 +0,0 @@ - -module DDC.Source.Tetra.Exp.Base - ( module DDC.Type.Exp - - -- * Expressions - , Exp (..) - , Lets (..) - , Alt (..) - , Pat (..) - , Cast (..) - - -- * Witnesses - , Witness (..) - - -- * Data Constructors - , DaCon (..) - - -- * Witness Constructors - , WiCon (..) - , WbCon (..)) -where -import DDC.Type.Exp -import DDC.Type.Sum () -import Control.DeepSeq -import DDC.Core.Exp - ( Witness (..) - , WiCon (..) - , WbCon (..) - , Pat (..) - , DaCon (..)) - - --- | Well-typed expressions have types of kind `Data`. -data Exp a n - --------------------------------------------------- - -- Core Language Constructs. - -- These are also in the core language, and after desugaring only - -- these constructs are used. - -- - -- | Value variable or primitive operation. - = XVar !a !(Bound n) - - -- | Data constructor or literal. - | XCon !a !(DaCon n) - - -- | Type abstraction (level-1). - | XLAM !a !(Bind n) !(Exp a n) - - -- | Value and Witness abstraction (level-0). - | XLam !a !(Bind n) !(Exp a n) - - -- | Application. - | XApp !a !(Exp a n) !(Exp a n) - - -- | Possibly recursive bindings. - | XLet !a !(Lets a n) !(Exp a n) - - -- | Case branching. - | XCase !a !(Exp a n) ![Alt a n] - - -- | Type cast. - | XCast !a !(Cast a n) !(Exp a n) - - -- | Type can appear as the argument of an application. - | XType !a !(Type n) - - -- | Witness can appear as the argument of an application. - | XWitness !a !(Witness a n) - - - --------------------------------------------------- - -- Sugar Constructs. - -- These constructs are eliminated by the desugarer. - -- - -- | Some expressions and infix operators that need to be resolved into - -- proper function applications. - | XDefix !a [Exp a n] - - -- | Use of a naked infix operator, like in 1 + 2. - -- INVARIANT: only appears in the list of an XDefix node. - | XInfixOp !a String - - -- | Use of an infix operator as a plain variable, like in (+) 1 2. - -- INVARIANT: only appears in the list of an XDefix node. - | XInfixVar !a String - deriving (Show, Eq) - - --- | Possibly recursive bindings. -data Lets a n - -- | Non-recursive let-binding. - = LLet !(Bind n) !(Exp a n) - - -- | Recursive let bindings. - | LRec ![(Bind n, Exp a n)] - - -- | Bind a local region variable, - -- and witnesses to its properties. - | LPrivate ![Bind n] !(Maybe (Type n)) ![Bind n] - deriving (Show, Eq) - - --- | Case alternatives. -data Alt a n - = AAlt !(Pat n) !(Exp a n) - deriving (Show, Eq) - - --- | Type casts. -data Cast a n - -- | Weaken the effect of an expression. - -- The given effect is added to the effect - -- of the body. - = CastWeakenEffect !(Effect n) - - -- | Purify the effect (action) of an expression. - | CastPurify !(Witness a n) - - -- | Box a computation, - -- capturing its effects in the S computation type. - | CastBox - - -- | Run a computation, - -- releasing its effects into the environment. - | CastRun - deriving (Show, Eq) - - --- NFData --------------------------------------------------------------------- -instance (NFData a, NFData n) => NFData (Exp a n) where - rnf xx - = case xx of - XVar a u -> rnf a `seq` rnf u - XCon a dc -> rnf a `seq` rnf dc - XLAM a b x -> rnf a `seq` rnf b `seq` rnf x - XLam a b x -> rnf a `seq` rnf b `seq` rnf x - XApp a x1 x2 -> rnf a `seq` rnf x1 `seq` rnf x2 - XLet a lts x -> rnf a `seq` rnf lts `seq` rnf x - XCase a x alts -> rnf a `seq` rnf x `seq` rnf alts - XCast a c x -> rnf a `seq` rnf c `seq` rnf x - XType a t -> rnf a `seq` rnf t - XWitness a w -> rnf a `seq` rnf w - XDefix a xs -> rnf a `seq` rnf xs - XInfixOp a s -> rnf a `seq` rnf s - XInfixVar a s -> rnf a `seq` rnf s - - -instance (NFData a, NFData n) => NFData (Cast a n) where - rnf cc - = case cc of - CastWeakenEffect e -> rnf e - CastPurify w -> rnf w - CastBox -> () - CastRun -> () - - -instance (NFData a, NFData n) => NFData (Lets a n) where - rnf lts - = case lts of - LLet b x -> rnf b `seq` rnf x - LRec bxs -> rnf bxs - LPrivate bs1 mR bs2 -> rnf bs1 `seq` rnf mR `seq` rnf bs2 - - -instance (NFData a, NFData n) => NFData (Alt a n) where - rnf aa - = case aa of - AAlt w x -> rnf w `seq` rnf x diff --git a/DDC/Source/Tetra/Exp/Generic.hs b/DDC/Source/Tetra/Exp/Generic.hs new file mode 100644 --- /dev/null +++ b/DDC/Source/Tetra/Exp/Generic.hs @@ -0,0 +1,322 @@ +{-# LANGUAGE TypeFamilies, UndecidableInstances #-} + +-- | Abstract syntax for Tetra Source expressions. +module DDC.Source.Tetra.Exp.Generic + ( -- * Classes + HasAnonBind (..) + + -- * Expressions + , GName + , GAnnot + , GBind + , GBound + , GPrim + , GExp (..) + , GLets (..) + , GAlt (..) + , GPat (..) + , GClause (..) + , GGuardedExp (..) + , GGuard (..) + , GCast (..) + , DaCon (..) + + -- * Witnesses + , GWitness (..) + , GWiCon (..) + + -- * Dictionaries + , ShowLanguage + , NFDataLanguage) +where +import DDC.Type.Exp +import qualified DDC.Type.Exp as T +import DDC.Type.Sum () +import Control.DeepSeq +import DDC.Core.Exp + ( DaCon (..)) + + +--------------------------------------------------------------------------------------------------- +-- | Type functions associated with the language AST. +type family GName l +type family GAnnot l +type family GBind l +type family GBound l +type family GPrim l + +class HasAnonBind l where + isAnon :: l -> GBind l -> Bool + + +--------------------------------------------------------------------------------------------------- +-- | Well-typed expressions have types of kind `Data`. +data GExp l + --------------------------------------------------- + -- Core Language Constructs. + -- These are also in the core language, and after desugaring only + -- these constructs are used. + -- + -- | Value variable or primitive operation. + = XVar !(GAnnot l) !(GBound l) + + -- | Primitive values. + | XPrim !(GAnnot l) !(GPrim l) + + -- | Data constructor or literal. + | XCon !(GAnnot l) !(DaCon (GName l)) + + -- | Type abstraction (level-1). + | XLAM !(GAnnot l) !(GBind l) !(GExp l) + + -- | Value and Witness abstraction (level-0). + | XLam !(GAnnot l) !(GBind l) !(GExp l) + + -- | Application. + | XApp !(GAnnot l) !(GExp l) !(GExp l) + + -- | A non-recursive let-binding. + | XLet !(GAnnot l) !(GLets l) !(GExp l) + + -- | Case branching. + | XCase !(GAnnot l) !(GExp l) ![GAlt l] + + -- | Type cast. + | XCast !(GAnnot l) !(GCast l) !(GExp l) + + -- | Type can appear as the argument of an application. + | XType !(GAnnot l) !(Type (GName l)) + + -- | Witness can appear as the argument of an application. + | XWitness !(GAnnot l) !(GWitness l) + + + --------------------------------------------------- + -- Sugar Constructs. + -- These constructs are eliminated by the desugarer. + -- + -- | Some expressions and infix operators that need to be resolved into + -- proper function applications. + | XDefix !(GAnnot l) [GExp l] + + -- | Use of a naked infix operator, like in 1 + 2. + -- INVARIANT: only appears in the list of an XDefix node. + | XInfixOp !(GAnnot l) String + + -- | Use of an infix operator as a plain variable, like in (+) 1 2. + -- INVARIANT: only appears in the list of an XDefix node. + | XInfixVar !(GAnnot l) String + + +-- | Possibly recursive bindings. +-- Whether these are taken as recursive depends on whether they appear +-- in an XLet or XLetrec group. +data GLets l + --------------------------------------------------- + -- Core Language Constructs + -- | Non-recursive expression binding. + = LLet !(GBind l) !(GExp l) + + -- | Recursive binding of lambda abstractions. + | LRec ![(GBind l, GExp l)] + + -- | Bind a local region variable, + -- and witnesses to its properties. + | LPrivate ![GBind l] !(Maybe (Type (GName l))) ![GBind l] + + --------------------------------------------------- + -- Sugar Constructs + -- | A possibly recursive group of binding clauses. + -- + -- Multiple clauses in the group may be part of the same function. + | LGroup ![GClause l] + + +-- | Binding clause +data GClause l + -- | A separate type signature. + = SSig !(GAnnot l) !(GBind l) !(Type (GName l)) + + -- | A function binding using pattern matching and guards. + | SLet !(GAnnot l) !(GBind l) ![GPat l] ![GGuardedExp l] + + +-- | Case alternatives. +data GAlt l + = AAlt !(GPat l) ![GGuardedExp l] + + +-- | Patterns. +data GPat l + -- | The default pattern always succeeds. + = PDefault + + -- | Match a data constructor and bind its arguments. + | PData !(DaCon (GName l)) ![GBind l] + + +-- | An expression with some guards. +data GGuardedExp l + = GGuard !(GGuard l) !(GGuardedExp l) + | GExp !(GExp l) + + +-- | Expression guards. +data GGuard l + = GPat !(GPat l) !(GExp l) + | GPred !(GExp l) + | GDefault + + +-- | Type casts. +data GCast l + -- | Weaken the effect of an expression. + -- The given effect is added to the effect + -- of the body. + = CastWeakenEffect !(Effect (GName l)) + + -- | Purify the effect (action) of an expression. + | CastPurify !(GWitness l) + + -- | Box a computation, + -- capturing its effects in the S computation type. + | CastBox + + -- | Run a computation, + -- releasing its effects into the environment. + | CastRun + + +-- | Witnesses. +data GWitness l + -- | Witness variable. + = WVar !(GAnnot l) !(GBound l) + + -- | Witness constructor. + | WCon !(GAnnot l) !(GWiCon l) + + -- | Witness application. + | WApp !(GAnnot l) !(GWitness l) !(GWitness l) + + -- | Type can appear as an argument of a witness application. + | WType !(GAnnot l) !(T.Type (GName l)) + + +-- | Witness constructors. +data GWiCon l + -- | Witness constructors defined in the environment. + -- In the interpreter we use this to hold runtime capabilities. + -- The attached type must be closed. + = WiConBound !(GBound l) !(T.Type (GName l)) + + +--------------------------------------------------------------------------------------------------- +type ShowLanguage l + = ( Show l + , Show (GName l), Show (GAnnot l) + , Show (GBind l), Show (GBound l), Show (GPrim l)) + +deriving instance ShowLanguage l => Show (GExp l) +deriving instance ShowLanguage l => Show (GLets l) +deriving instance ShowLanguage l => Show (GClause l) +deriving instance ShowLanguage l => Show (GAlt l) +deriving instance ShowLanguage l => Show (GGuardedExp l) +deriving instance ShowLanguage l => Show (GGuard l) +deriving instance ShowLanguage l => Show (GPat l) +deriving instance ShowLanguage l => Show (GCast l) +deriving instance ShowLanguage l => Show (GWitness l) +deriving instance ShowLanguage l => Show (GWiCon l) + + +--------------------------------------------------------------------------------------------------- +type NFDataLanguage l + = ( NFData l + , NFData (GAnnot l), NFData (GName l) + , NFData (GBind l), NFData (GBound l), NFData (GPrim l)) + +instance NFDataLanguage l => NFData (GExp l) where + rnf xx + = case xx of + XVar a u -> rnf a `seq` rnf u + XPrim a p -> rnf a `seq` rnf p + XCon a dc -> rnf a `seq` rnf dc + XLAM a b x -> rnf a `seq` rnf b `seq` rnf x + XLam a b x -> rnf a `seq` rnf b `seq` rnf x + XApp a x1 x2 -> rnf a `seq` rnf x1 `seq` rnf x2 + XLet a lts x -> rnf a `seq` rnf lts `seq` rnf x + XCase a x alts -> rnf a `seq` rnf x `seq` rnf alts + XCast a c x -> rnf a `seq` rnf c `seq` rnf x + XType a t -> rnf a `seq` rnf t + XWitness a w -> rnf a `seq` rnf w + XDefix a xs -> rnf a `seq` rnf xs + XInfixOp a s -> rnf a `seq` rnf s + XInfixVar a s -> rnf a `seq` rnf s + + +instance NFDataLanguage l => NFData (GClause l) where + rnf cc + = case cc of + SSig a b t -> rnf a `seq` rnf b `seq` rnf t + SLet a b ps gxs -> rnf a `seq` rnf b `seq` rnf ps `seq` rnf gxs + + +instance NFDataLanguage l => NFData (GLets l) where + rnf lts + = case lts of + LLet b x -> rnf b `seq` rnf x + LRec bxs -> rnf bxs + LPrivate bs1 mR bs2 -> rnf bs1 `seq` rnf mR `seq` rnf bs2 + LGroup cs -> rnf cs + + +instance NFDataLanguage l => NFData (GAlt l) where + rnf aa + = case aa of + AAlt w gxs -> rnf w `seq` rnf gxs + + +instance NFDataLanguage l => NFData (GPat l) where + rnf pp + = case pp of + PDefault -> () + PData dc bs -> rnf dc `seq` rnf bs + + +instance NFDataLanguage l => NFData (GGuardedExp l) where + rnf gx + = case gx of + GGuard g gx' -> rnf g `seq` rnf gx' + GExp x -> rnf x + + +instance NFDataLanguage l => NFData (GGuard l) where + rnf gg + = case gg of + GPred x -> rnf x + GPat p x -> rnf p `seq` rnf x + GDefault -> () + + +instance NFDataLanguage l => NFData (GCast l) where + rnf cc + = case cc of + CastWeakenEffect e -> rnf e + CastPurify w -> rnf w + CastBox -> () + CastRun -> () + + +instance NFDataLanguage l => NFData (GWitness l) where + rnf ww + = case ww of + WVar a u -> rnf a `seq` rnf u + WCon a c -> rnf a `seq` rnf c + WApp a w1 w2 -> rnf a `seq` rnf w1 `seq` rnf w2 + WType a t -> rnf a `seq` rnf t + + +instance NFDataLanguage l => NFData (GWiCon l) where + rnf wc + = case wc of + WiConBound u t -> rnf u `seq` rnf t + diff --git a/DDC/Source/Tetra/Lexer.hs b/DDC/Source/Tetra/Lexer.hs --- a/DDC/Source/Tetra/Lexer.hs +++ b/DDC/Source/Tetra/Lexer.hs @@ -1,4 +1,5 @@ +-- | Lexer for Source Tetra tokens. module DDC.Source.Tetra.Lexer (lexModuleString) where @@ -10,10 +11,16 @@ -- | Lex a string to tokens, using primitive names. -- -- The first argument gives the starting source line number. +-- +-- We're currently re-using the lexer for the core language, which has +-- *mostly* the same lexical structure as Source Tetra. +-- There are a few tokens accepted by one language but not the other, +-- but it'll do for now. +-- lexModuleString :: String -> Int -> String -> [Token (Tok Name)] lexModuleString sourceName lineStart str = map rn $ lexModuleWithOffside sourceName lineStart str - where rn (Token strTok sp) + where rn (Token strTok sp) = case renameTok readName strTok of Just t' -> Token t' sp - Nothing -> Token (KJunk "lexical error") sp + Nothing -> Token (KErrorJunk "lexical error") sp diff --git a/DDC/Source/Tetra/Lexer/Lit.hs b/DDC/Source/Tetra/Lexer/Lit.hs deleted file mode 100644 --- a/DDC/Source/Tetra/Lexer/Lit.hs +++ /dev/null @@ -1,85 +0,0 @@ - -module DDC.Source.Tetra.Lexer.Lit - ( readLitInteger - , readLitNat - , readLitInt - , readLitWordOfBits) -where -import Data.List -import Data.Char - - --- | Read a signed integer. -readLitInteger :: String -> Maybe Integer -readLitInteger [] = Nothing -readLitInteger str@(c:cs) - | '-' <- c - , all isDigit cs - = Just $ read str - - | all isDigit str - = Just $ read str - - | otherwise - = Nothing - - --- | Read a natural number like @1234@. -readLitNat :: String -> Maybe Integer -readLitNat str1 - | (ds, "") <- span isDigit str1 - , not $ null ds - = Just $ read ds - - | otherwise - = Nothing - - --- | Read an integer with an explicit format specifier like @1234i@. -readLitInt :: String -> Maybe Integer -readLitInt str1 - | '-' : str2 <- str1 - , (ds, "i") <- span isDigit str2 - , not $ null ds - = Just $ read ds - - | (ds, "i") <- span isDigit str1 - , not $ null ds - = Just $ read ds - - | otherwise - = Nothing - - --- | Read a word with an explicit format speficier. -readLitWordOfBits :: String -> Maybe (Integer, Int) -readLitWordOfBits str1 - -- binary like 0b01001w32 - | Just str2 <- stripPrefix "0b" str1 - , (ds, str3) <- span (\c -> c == '0' || c == '1') str2 - , not $ null ds - , Just str4 <- stripPrefix "w" str3 - , (bs, "") <- span isDigit str4 - , not $ null bs - , bits <- read bs - , length ds <= bits - = Just (readBinary ds, bits) - - -- decimal like 1234w32 - | (ds, str2) <- span isDigit str1 - , not $ null ds - , Just str3 <- stripPrefix "w" str2 - , (bs, "") <- span isDigit str3 - , not $ null bs - = Just (read ds, read bs) - - | otherwise - = Nothing - - --- | Read a binary string as a number. -readBinary :: (Num a, Read a) => String -> a -readBinary digits - = foldl' (\ acc b -> if b then 2 * acc + 1 else 2 * acc) 0 - $ map (/= '0') digits - diff --git a/DDC/Source/Tetra/Module.hs b/DDC/Source/Tetra/Module.hs --- a/DDC/Source/Tetra/Module.hs +++ b/DDC/Source/Tetra/Module.hs @@ -1,10 +1,14 @@ +{-# LANGUAGE UndecidableInstances #-} +-- | Definition of Source Tetra modules. module DDC.Source.Tetra.Module ( -- * Modules Module (..) , isMainModule , ExportSource (..) - , ImportSource (..) + , ImportType (..) + , ImportCap (..) + , ImportValue (..) -- * Module Names , QualName (..) @@ -26,74 +30,79 @@ , ModuleName (..) , isMainModuleName , ExportSource (..) - , ImportSource (..)) + , ImportType (..) + , ImportCap (..) + , ImportValue (..)) -- Module --------------------------------------------------------------------- -data Module a n +data Module l = Module { -- | Name of this module moduleName :: !ModuleName -- Exports ---------------------------- -- | Names of exported types (level-1). - , moduleExportTypes :: [n] + , moduleExportTypes :: [GName l] -- | Names of exported values (level-0). - , moduleExportValues :: [n] + , moduleExportValues :: [GName l] -- Imports ---------------------------- -- | Imported modules. , moduleImportModules :: [ModuleName] -- | Kinds of imported foreign types. - , moduleImportTypes :: [(n, ImportSource n)] + , moduleImportTypes :: [(GName l, ImportType (GName l))] + -- | Types of imported capabilities. + , moduleImportCaps :: [(GName l, ImportCap (GName l))] + -- | Types of imported foreign values. - , moduleImportValues :: [(n, ImportSource n)] + , moduleImportValues :: [(GName l, ImportValue (GName l))] -- Local ------------------------------ -- | Top-level things - , moduleTops :: [Top a n] } - deriving Show + , moduleTops :: [Top l] } +deriving instance ShowLanguage l => Show (Module l) -instance (NFData a, NFData n) => NFData (Module a n) where + +instance NFDataLanguage l => NFData (Module l) where rnf !mm - = rnf (moduleName mm) - `seq` rnf (moduleExportTypes mm) - `seq` rnf (moduleExportValues mm) - `seq` rnf (moduleImportModules mm) - `seq` rnf (moduleImportTypes mm) - `seq` rnf (moduleImportValues mm) - `seq` rnf (moduleTops mm) + = rnf (moduleName mm) + `seq` rnf (moduleExportTypes mm) + `seq` rnf (moduleExportValues mm) + `seq` rnf (moduleImportModules mm) + `seq` rnf (moduleImportTypes mm) + `seq` rnf (moduleImportCaps mm) + `seq` rnf (moduleImportValues mm) + `seq` rnf (moduleTops mm) -- | Check if this is the `Main` module. -isMainModule :: Module a n -> Bool +isMainModule :: Module l -> Bool isMainModule mm - = isMainModuleName - $ moduleName mm + = isMainModuleName $ moduleName mm -- Top Level Thing ------------------------------------------------------------ -data Top a n - -- | Top-level, possibly recursive binding. - = TopBind a (Bind n) (Exp a n) +data Top l + -- | Some top-level, possibly recursive clauses. + = TopClause + { topAnnot :: GAnnot l + , topClause :: GClause l } -- | Data type definition. | TopData - { topAnnot :: a - , topDataDef :: DataDef n } - deriving Show + { topAnnot :: GAnnot l + , topDataDef :: DataDef (GName l) } +deriving instance ShowLanguage l => Show (Top l) -instance (NFData a, NFData n) => NFData (Top a n) where +instance NFDataLanguage l => NFData (Top l) where rnf !top = case top of - TopBind a b x - -> rnf a `seq` rnf b `seq` rnf x - - TopData a def - -> rnf a `seq` rnf def + TopClause a c -> rnf a `seq` rnf c + TopData a def -> rnf a `seq` rnf def diff --git a/DDC/Source/Tetra/Parser.hs b/DDC/Source/Tetra/Parser.hs --- a/DDC/Source/Tetra/Parser.hs +++ b/DDC/Source/Tetra/Parser.hs @@ -1,7 +1,9 @@ +-- | Parser for the Source Tetra language. module DDC.Source.Tetra.Parser ( Parser , Context (..) + , context -- * Modules , pModule diff --git a/DDC/Source/Tetra/Parser/Atom.hs b/DDC/Source/Tetra/Parser/Atom.hs new file mode 100644 --- /dev/null +++ b/DDC/Source/Tetra/Parser/Atom.hs @@ -0,0 +1,28 @@ + +module DDC.Source.Tetra.Parser.Atom + ( pPrimValSP + , pVarStringSP) +where +import DDC.Source.Tetra.Prim +import DDC.Core.Lexer.Tokens +import DDC.Base.Parser ((), SourcePos) +import qualified DDC.Base.Parser as P + +import DDC.Core.Parser + (Parser) + + +-- | Parse a variable, with source position. +pPrimValSP :: Parser Name (PrimVal, SourcePos) +pPrimValSP = P.pTokMaybeSP f + "a variable" + where f (KN (KVar (NameVal p))) = Just p + f _ = Nothing + + +-- | Parse a variable, with source position. +pVarStringSP :: Parser Name (String, SourcePos) +pVarStringSP = P.pTokMaybeSP f + "a variable" + where f (KN (KVar (NameVar s))) = Just s + f _ = Nothing diff --git a/DDC/Source/Tetra/Parser/Exp.hs b/DDC/Source/Tetra/Parser/Exp.hs --- a/DDC/Source/Tetra/Parser/Exp.hs +++ b/DDC/Source/Tetra/Parser/Exp.hs @@ -1,81 +1,108 @@ --- | Core language parser. +-- | Parser for Source Tetra expressions. module DDC.Source.Tetra.Parser.Exp - ( pExp + ( context + , pExp , pExpApp , pExpAtom, pExpAtomSP - , pLetsSP, pLetBinding + , pLetsSP, pClauseSP , pType , pTypeApp , pTypeAtom) where -import DDC.Source.Tetra.Exp +import DDC.Source.Tetra.Transform.Guards +import DDC.Source.Tetra.Parser.Witness import DDC.Source.Tetra.Parser.Param +import DDC.Source.Tetra.Parser.Atom import DDC.Source.Tetra.Compounds +import DDC.Source.Tetra.Prim +import DDC.Source.Tetra.Exp.Annot +import DDC.Core.Lexer.Tokens +import Control.Monad.Except +import DDC.Base.Parser ((), SourcePos(..)) +import qualified DDC.Base.Parser as P +import qualified DDC.Type.Exp as T +import qualified DDC.Type.Compounds as T +import qualified Data.Text as Text import DDC.Core.Parser ( Parser - , Context(..) + , Context (..) , pBinder - , pWitness - , pWitnessAtom , pType , pTypeAtom , pTypeApp - , pCon - , pConSP - , pLit - , pLitSP + , pCon, pConSP + , pLit, pLitSP + , pStringSP , pIndexSP - , pOpSP - , pOpVarSP - , pVarSP + , pOpSP, pOpVarSP , pTok , pTokSP) -import DDC.Core.Lexer.Tokens -import DDC.Base.Parser ((), SourcePos) -import qualified DDC.Base.Parser as P -import qualified DDC.Type.Compounds as T -import Control.Monad.Error +type SP = SourcePos +-- | Starting context for the parser. +-- Holds flags about what language features we should accept. +context :: Context Name +context = Context + { contextTrackedEffects = True + , contextTrackedClosures = True + , contextFunctionalEffects = False + , contextFunctionalClosures = False + , contextMakeStringName = Just (\_ tx -> NameLitTextLit tx) } + -- Exp -------------------------------------------------------------------------------------------- --- | Parse a core language expression. -pExp :: Ord n => Context -> Parser n (Exp SourcePos n) +-- | Parse a Tetra Source language expression. +pExp :: Context Name -> Parser Name (Exp SP) pExp c = P.choice + -- Level-0 lambda abstractions - -- \(x1 x2 ... : Type) (y1 y2 ... : Type) ... . Exp - [ do sp <- pTokSP KBackSlash + -- \(x1 x2 ... : Type) (y1 y2 ... : Type) ... . Exp + -- \x1 x2 : Type. Exp + [ do sp <- P.choice [ pTokSP KLambda, pTokSP KBackSlash ] - bs <- liftM concat - $ P.many1 - $ do pTok KRoundBra + bs <- P.choice + [ fmap concat $ P.many1 + $ do pTok KRoundBra bs' <- P.many1 pBinder pTok (KOp ":") t <- pType c pTok KRoundKet return (map (\b -> T.makeBindFromBinder b t) bs') + , do bs' <- P.many1 pBinder + pTok (KOp ":") + t <- pType c + return (map (\b -> T.makeBindFromBinder b t) bs') + ] + pTok KDot xBody <- pExp c return $ foldr (XLam sp) xBody bs -- Level-1 lambda abstractions. -- /\(x1 x2 ... : Type) (y1 y2 ... : Type) ... . Exp - , do sp <- pTokSP KBigLambda + , do sp <- P.choice [ pTokSP KBigLambda, pTokSP KBigLambdaSlash ] - bs <- liftM concat - $ P.many1 - $ do pTok KRoundBra + bs <- P.choice + [ fmap concat $ P.many1 + $ do pTok KRoundBra bs' <- P.many1 pBinder pTok (KOp ":") t <- pType c pTok KRoundKet return (map (\b -> T.makeBindFromBinder b t) bs') + , do bs' <- P.many1 pBinder + pTok (KOp ":") + t <- pType c + return (map (\b -> T.makeBindFromBinder b t) bs') + ] + pTok KDot xBody <- pExp c return $ foldr (XLAM sp) xBody bs @@ -103,17 +130,25 @@ pTok KBraceKet return $ XCase sp x alts - -- match Pat <- Exp else Exp in Exp - -- Sugar for a case-expression. + -- match { | EXP = EXP | EXP = EXP ... } + -- Sugar for cascaded case expressions case-expression. , do sp <- pTokSP KMatch - p <- pPat c - pTok KArrowDashLeft + pTok KBraceBra + x <- pMatchGuardsAsCase sp c + pTok KBraceKet + return x + + , do -- if-then-else + -- Sugar for a case-expression. + sp <- pTokSP KIf x1 <- pExp c - pTok KElse + pTok KThen x2 <- pExp c - pTok KIn + pTok KElse x3 <- pExp c - return $ XCase sp x1 [AAlt p x3, AAlt PDefault x2] + return $ XCase sp x1 + [ AAlt pTrue [GExp x2] + , AAlt PDefault [GExp x3]] -- weakeff [Type] in Exp , do sp <- pTokSP KWeakEff @@ -149,7 +184,7 @@ -- Applications. -pExpApp :: Ord n => Context -> Parser n (Exp SourcePos n) +pExpApp :: Context Name -> Parser Name (Exp SP) pExpApp c = do xps <- liftM concat $ P.many1 (pArgSPs c) let (xs, sps) = unzip xps @@ -163,7 +198,7 @@ -- Comp, Witness or Spec arguments. -pArgSPs :: Ord n => Context -> Parser n [(Exp SourcePos n, SourcePos)] +pArgSPs :: Context Name -> Parser Name [(Exp SP, SP)] pArgSPs c = P.choice -- [Type] @@ -198,7 +233,7 @@ -- | Parse a variable, constructor or parenthesised expression. -pExpAtom :: Ord n => Context -> Parser n (Exp SourcePos n) +pExpAtom :: Context Name -> Parser Name (Exp SP) pExpAtom c = do (x, _) <- pExpAtomSP c return x @@ -206,11 +241,7 @@ -- | Parse a variable, constructor or parenthesised expression, -- also returning source position. -pExpAtomSP - :: Ord n - => Context - -> Parser n (Exp SourcePos n, SourcePos) - +pExpAtomSP :: Context Name -> Parser Name (Exp SP, SP) pExpAtomSP c = P.choice [ -- ( Exp2 ) @@ -243,13 +274,23 @@ , do (lit, sp) <- pLitSP return (XCon sp (DaConPrim lit (T.tBot T.kData)), sp) + , do (tx, sp) <- pStringSP + let Just mkString = contextMakeStringName c + let lit = mkString sp tx + return (XCon sp (DaConPrim lit (T.tBot T.kData)), sp) + + -- Primitive names. + , do (nPrim, sp) <- pPrimValSP + return (XPrim sp nPrim, sp) + + -- Named variables. + , do (sVar, sp) <- pVarStringSP + return (XVar sp (T.UName (NameVar sVar)), sp) + -- Debruijn indices , do (i, sp) <- pIndexSP - return (XVar sp (UIx i), sp) + return (XVar sp (T.UIx i), sp) - -- Variables - , do (var, sp) <- pVarSP - return (XVar sp (UName var), sp) ] "a variable, constructor, or parenthesised type" @@ -257,17 +298,22 @@ -- Alternatives ----------------------------------------------------------------------------------- -- Case alternatives. -pAlt :: Ord n => Context -> Parser n (Alt SourcePos n) +pAlt :: Context Name -> Parser Name (Alt SP) pAlt c = do p <- pPat c - pTok KArrowDash - x <- pExp c - return $ AAlt p x + P.choice + [ do -- Desugar case guards while we're here. + spgxs <- P.many1 (pGuardedExpSP c (pTokSP KArrowDash)) + let gxs = map snd spgxs + return $ AAlt p gxs + + , do pTok KArrowDash + x <- pExp c + return $ AAlt p [GExp x] ] -- Patterns. -pPat :: Ord n - => Context -> Parser n (Pat n) +pPat :: Context Name -> Parser Name (Pat SP) pPat c = P.choice [ -- Wildcard @@ -290,9 +336,7 @@ -- Binds in patterns can have no type annotation, -- or can have an annotation if the whole thing is in parens. -pBindPat - :: Ord n - => Context -> Parser n (Bind n) +pBindPat :: Context Name -> Parser Name Bind pBindPat c = P.choice -- Plain binder. @@ -309,22 +353,100 @@ ] +-- Guards ----------------------------------------------------------------------------------------- +-- | Parse some guards and auto-desugar them to a case-expression. +pBindGuardsAsCaseSP + :: Context Name + -> Parser Name (SP, Exp SP) + +pBindGuardsAsCaseSP c + = do + (sp, g) : spgs + <- P.many1 (pGuardedExpSP c (pTokSP KEquals)) + + -- Desugar guards. + -- If none match then raise a runtime error. + let xx' = desugarGuards sp (g : map snd spgs) + $ xErrorDefault sp + (Text.pack $ sourcePosSource sp) + (fromIntegral $ sourcePosLine sp) + + return (sp, xx') + + +pMatchGuardsAsCase + :: SP -> Context Name + -> Parser Name (Exp SP) + +pMatchGuardsAsCase sp c + = do gg <- liftM (map snd) + $ P.sepEndBy1 (pGuardedExpSP c (pTokSP KEquals)) + (pTok KSemiColon) + + -- Desugar guards. + -- If none match then raise a runtime error. + let xx' = desugarGuards sp gg + $ xErrorDefault sp + (Text.pack $ sourcePosSource sp) + (fromIntegral $ sourcePosLine sp) + + return xx' + + +-- | An guarded expression, +-- like | EXP1 = EXP2. +pGuardedExpSP + :: Context Name -- ^ Parser context. + -> Parser Name SP -- ^ Parser for char between and of guards and exp. + -- usually -> or = + -> Parser Name (SP, GuardedExp SP) + +pGuardedExpSP c pTermSP + = pGuardExp (pTokSP KBar) + + where pGuardExp pSepSP + = P.choice + [ do sp <- pSepSP + g <- pGuard + gx <- liftM snd $ pGuardExp (pTokSP KComma) + return (sp, GGuard g gx) + + , do sp <- pTermSP + x <- pExp c + return (sp, GExp x) ] + + pGuard + = P.choice + [ P.try $ + do p <- pPat c + pTok KArrowDashLeft + x <- pExp c + return $ GPat p x + + , do g <- pExp c + return $ GPred g + + + , do pTok KOtherwise + return GDefault ] + + -- Bindings --------------------------------------------------------------------------------------- -pLetsSP :: Ord n - => Context -> Parser n (Lets SourcePos n, SourcePos) +pLetsSP :: Context Name -> Parser Name (Lets SP, SP) pLetsSP c = P.choice [ -- non-recursive let do sp <- pTokSP KLet - (b1, x1) <- pLetBinding c - return (LLet b1 x1, sp) + l <- liftM fst $ pClauseSP c + return (LGroup [l], sp) -- recursive let , do sp <- pTokSP KLetRec pTok KBraceBra - lets <- P.sepEndBy1 (pLetBinding c) (pTok KSemiColon) + ls <- liftM (map fst) + $ P.sepEndBy1 (pClauseSP c) (pTok KSemiColon) pTok KBraceKet - return (LRec lets, sp) + return (LGroup ls, sp) -- Private region binding. -- private Binder+ (with { Binder : Type ... })? in Exp @@ -361,11 +483,9 @@ ] -pLetWits - :: Ord n - => Context - -> [Bind n] -> Maybe (Type n) - -> Parser n (Lets SourcePos n) +pLetWits :: Context Name + -> [Bind] -> Maybe (T.Type Name) + -> Parser Name (Lets SP) pLetWits c bs mParent = P.choice @@ -380,7 +500,7 @@ -- Ambient witness binding, used for capabilities. , do t <- pTypeApp c - return $ BNone t + return $ T.BNone t ]) (pTok KSemiColon) pTok KBraceKet @@ -391,34 +511,26 @@ -- | A binding for let expression. -pLetBinding - :: Ord n - => Context - -> Parser n ( Bind n - , Exp SourcePos n) -pLetBinding c +pClauseSP :: Context Name + -> Parser Name (Clause SP, SP) + +pClauseSP c = do b <- pBinder P.choice [ do -- Binding with full type signature. - -- Binder : Type = Exp - pTok (KOp ":") - t <- pType c - pTok (KOp "=") - xBody <- pExp c - - return $ (T.makeBindFromBinder b t, xBody) - + sp <- pTokSP (KOp ":") + t <- pType c + (_, xBody) <- pBindGuardsAsCaseSP c + return ( SLet sp (T.makeBindFromBinder b t) [] [GExp xBody] + , sp) , do -- Non-function binding with no type signature. - -- This form can't be used with letrec as we can't use it - -- to build the full type sig for the let-bound variable. - -- Binder = Exp - pTok (KOp "=") + sp <- pTokSP KEquals xBody <- pExp c let t = T.tBot T.kData - return $ (T.makeBindFromBinder b t, xBody) - + return ( SLet sp (T.makeBindFromBinder b t) [] [GExp xBody] + , sp) , do -- Binding using function syntax. ps <- liftM concat @@ -429,37 +541,38 @@ -- We can make the full type sig for the let-bound variable. -- Binder Param1 Param2 .. ParamN : Type = Exp pTok (KOp ":") - tBody <- pType c - sp <- pTokSP (KOp "=") - xBody <- pExp c + tBody <- pType c + (sp, xBody) <- pBindGuardsAsCaseSP c let x = expOfParams sp ps xBody let t = funTypeOfParams c ps tBody - return (T.makeBindFromBinder b t, x) + return ( SLet sp (T.makeBindFromBinder b t) [] [GExp x] + , sp) -- Function syntax with no return type. -- We can't make the type sig for the let-bound variable, -- but we can create lambda abstractions with the given -- parameter types. -- Binder Param1 Param2 .. ParamN = Exp - , do sp <- pTokSP (KOp "=") - xBody <- pExp c + , do (sp, xBody) <- pBindGuardsAsCaseSP c let x = expOfParams sp ps xBody let t = T.tBot T.kData - return (T.makeBindFromBinder b t, x) ] + return ( SLet sp (T.makeBindFromBinder b t) [] [GExp x] + , sp) + ] ] -- Statements ------------------------------------------------------------------------------------- data Stmt n - = StmtBind SourcePos (Bind n) (Exp SourcePos n) - | StmtMatch SourcePos (Pat n) (Exp SourcePos n) (Exp SourcePos n) - | StmtNone SourcePos (Exp SourcePos n) + = StmtBind SP Bind (Exp SP) + | StmtMatch SP (Pat SP) (Exp SP) (Exp SP) + | StmtNone SP (Exp SP) -- | Parse a single statement. -pStmt :: Ord n => Context -> Parser n (Stmt n) +pStmt :: Context Name -> Parser Name (Stmt Name) pStmt c = P.choice [ -- Binder = Exp ; @@ -468,7 +581,7 @@ -- P.try $ do br <- pBinder - sp <- pTokSP (KOp "=") + sp <- pTokSP KEquals x1 <- pExp c let t = T.tBot T.kData let b = T.makeBindFromBinder br t @@ -498,7 +611,7 @@ -- | Parse some statements. -pStmts :: Ord n => Context -> Parser n (Exp SourcePos n) +pStmts :: Context Name -> Parser Name (Exp SP) pStmts c = do stmts <- P.sepEndBy1 (pStmt c) (pTok KSemiColon) case makeStmts stmts of @@ -507,7 +620,7 @@ -- | Make an expression from some statements. -makeStmts :: [Stmt n] -> Maybe (Exp SourcePos n) +makeStmts :: [Stmt Name] -> Maybe (Exp SP) makeStmts ss = case ss of [StmtNone _ x] @@ -515,7 +628,7 @@ StmtNone sp x1 : rest | Just x2 <- makeStmts rest - -> Just $ XLet sp (LLet (BNone (T.tBot T.kData)) x1) x2 + -> Just $ XLet sp (LLet (T.BNone (T.tBot T.kData)) x1) x2 StmtBind sp b x1 : rest | Just x2 <- makeStmts rest @@ -524,8 +637,8 @@ StmtMatch sp p x1 x2 : rest | Just x3 <- makeStmts rest -> Just $ XCase sp x1 - [ AAlt p x3 - , AAlt PDefault x2] + [ AAlt p [GExp x3] + , AAlt PDefault [GExp x2] ] _ -> Nothing diff --git a/DDC/Source/Tetra/Parser/Module.hs b/DDC/Source/Tetra/Parser/Module.hs --- a/DDC/Source/Tetra/Parser/Module.hs +++ b/DDC/Source/Tetra/Parser/Module.hs @@ -1,4 +1,5 @@ +-- | Parser for Source Tetra modules. module DDC.Source.Tetra.Parser.Module ( -- * Modules pModule @@ -11,11 +12,14 @@ import DDC.Source.Tetra.Compounds import DDC.Source.Tetra.DataDef import DDC.Source.Tetra.Module -import DDC.Source.Tetra.Exp +import DDC.Source.Tetra.Prim +import DDC.Source.Tetra.Exp.Annot import DDC.Core.Lexer.Tokens import DDC.Base.Pretty import Control.Monad +import qualified DDC.Type.Exp as T import qualified DDC.Base.Parser as P +import DDC.Base.Parser (()) import DDC.Core.Parser ( Parser @@ -25,15 +29,16 @@ , pVar , pTok, pTokSP) +type SP = P.SourcePos --- Module --------------------------------------------------------------------- + +-- Module ----------------------------------------------------------------------------------------- -- | Parse a source tetra module. -pModule :: (Ord n, Pretty n) - => Context - -> Parser n (Module P.SourcePos n) +pModule :: Context Name -> Parser Name (Module (Annot SP)) pModule c - = do _sp <- pTokSP KModule - name <- pModuleName + = do + _sp <- pTokSP KModule + name <- pModuleName "a module name" -- export { VAR;+ } tExports @@ -50,14 +55,21 @@ tImports <- liftM concat $ P.many (pImportSpecs c) - pTok KWhere - pTok KBraceBra + -- top-level declarations. + tops + <- P.choice + [do pTok KWhere + pTok KBraceBra - -- TOP;+ - tops <- P.sepEndBy (pTop c) (pTok KSemiColon) + -- TOP;+ + tops <- P.sepEndBy (pTop c) (pTok KSemiColon) - pTok KBraceKet + pTok KBraceKet + return tops + ,do return [] ] + + -- ISSUE #295: Check for duplicate exported names in module parser. -- The names are added to a unique map, so later ones with the same -- name will replace earlier ones. @@ -65,17 +77,15 @@ { moduleName = name , moduleExportTypes = [] , moduleExportValues = tExports - , moduleImportModules = [] + , moduleImportModules = [mn | ImportModule mn <- tImports] , moduleImportTypes = [(n, s) | ImportType n s <- tImports] + , moduleImportCaps = [(n, s) | ImportCap n s <- tImports] , moduleImportValues = [(n, s) | ImportValue n s <- tImports] , moduleTops = tops } -- | Parse a type signature. -pTypeSig - :: Ord n - => Context -> Parser n (n, Type n) - +pTypeSig :: Context Name -> Parser Name (Name, T.Type Name) pTypeSig c = do var <- pVar pTokSP (KOp ":") @@ -83,61 +93,94 @@ return (var, t) -------------------------------------------------------------------------------- +--------------------------------------------------------------------------------------------------- -- | An imported foreign type or foreign value. data ImportSpec n - = ImportType n (ImportSource n) - | ImportValue n (ImportSource n) + = ImportModule ModuleName + | ImportType n (ImportType n) + | ImportCap n (ImportCap n) + | ImportValue n (ImportValue n) + deriving Show -- | Parse some import specs. -pImportSpecs - :: (Ord n, Pretty n) - => Context -> Parser n [ImportSpec n] - +pImportSpecs :: Context Name -> Parser Name [ImportSpec Name] pImportSpecs c = do pTok KImport - pTok KForeign - src <- liftM (renderIndent . ppr) pName P.choice - [ -- imports foreign X type (NAME :: TYPE)+ - do pTok KType - pTok KBraceBra + -- import foreign ... + [ do pTok KForeign + src <- liftM (renderIndent . ppr) pName - sigs <- P.sepEndBy1 (pImportType c src) (pTok KSemiColon) - pTok KBraceKet - return sigs + P.choice + [ -- import foreign X type (NAME :: TYPE)+ + do pTok KType + pTok KBraceBra - -- imports foreign X value (NAME :: TYPE)+ - , do pTok KValue - pTok KBraceBra + sigs <- P.sepEndBy1 (pImportType c src) (pTok KSemiColon) + pTok KBraceKet + return sigs - sigs <- P.sepEndBy1 (pImportValue c src) (pTok KSemiColon) + -- import foreign X capability (NAME :: TYPE)+ + , do pTok KCapability + pTok KBraceBra + + sigs <- P.sepEndBy1 (pImportCapability c src) (pTok KSemiColon) + pTok KBraceKet + return sigs + + -- import foreign X value (NAME :: TYPE)+ + , do pTok KValue + pTok KBraceBra + + sigs <- P.sepEndBy1 (pImportValue c src) (pTok KSemiColon) + pTok KBraceKet + return sigs + ] + + , do pTok KBraceBra + names <- P.sepEndBy1 pModuleName (pTok KSemiColon) + "module names" pTok KBraceKet - return sigs + return [ImportModule n | n <- names] ] -- | Parse a type import spec. -pImportType - :: (Ord n, Pretty n) - => Context -> String -> Parser n (ImportSpec n) +pImportType :: Context Name -> String -> Parser Name (ImportSpec Name) pImportType c src | "abstract" <- src = do n <- pName pTokSP (KOp ":") k <- pType c - return (ImportType n (ImportSourceAbstract k)) + return (ImportType n (ImportTypeAbstract k)) + | "boxed" <- src + = do n <- pName + pTokSP (KOp ":") + k <- pType c + return (ImportType n (ImportTypeBoxed k)) + | otherwise = P.unexpected "import mode for foreign type" +-- | Parse a capability import. +pImportCapability :: Context Name -> String -> Parser Name (ImportSpec Name) +pImportCapability c src + | "abstract" <- src + = do n <- pName + pTokSP (KOp ":") + t <- pType c + return (ImportCap n (ImportCapAbstract t)) + + | otherwise + = P.unexpected "import mode for foreign capability" + + -- | Parse a value import spec. -pImportValue - :: (Ord n, Pretty n) - => Context -> String -> Parser n (ImportSpec n) +pImportValue :: Context Name -> String -> Parser Name (ImportSpec Name) pImportValue c src | "c" <- src = do n <- pName @@ -148,32 +191,28 @@ -- with foreign C imports and exports. let symbol = renderIndent (ppr n) - return (ImportValue n (ImportSourceSea symbol k)) + return (ImportValue n (ImportValueSea symbol k)) | otherwise = P.unexpected "import mode for foreign value" --- Top Level ----------------------------------------------------------------- -pTop :: Ord n - => Context -> Parser n (Top P.SourcePos n) +-- Top Level -------------------------------------------------------------------------------------- +pTop :: Context Name -> Parser Name (Top (Annot SP)) pTop c = P.choice [ do -- A top-level, possibly recursive binding. - (b, x) <- pLetBinding c - let Just sp = takeAnnotOfExp x - return $ TopBind sp b x + (l, sp) <- pClauseSP c + return $ TopClause sp l -- A data type declaration , do pData c ] --- Data ----------------------------------------------------------------------- +-- Data ------------------------------------------------------------------------------------------- -- | Parse a data type declaration. -pData :: Ord n - => Context -> Parser n (Top P.SourcePos n) - +pData :: Context Name -> Parser Name (Top (Annot SP)) pData c = do sp <- pTokSP KData n <- pName @@ -193,18 +232,18 @@ -- | Parse a type parameter to a data type. -pDataParam :: Ord n => Context -> Parser n [Bind n] +pDataParam :: Context Name -> Parser Name [Bind] pDataParam c = do pTok KRoundBra ns <- P.many1 pName pTokSP (KOp ":") k <- pType c pTok KRoundKet - return [BName n k | n <- ns] + return [T.BName n k | n <- ns] -- | Parse a data constructor declaration. -pDataCtor :: Ord n => Context -> Parser n (DataCtor n) +pDataCtor :: Context Name -> Parser Name (DataCtor Name) pDataCtor c = do n <- pName pTokSP (KOp ":") diff --git a/DDC/Source/Tetra/Parser/Param.hs b/DDC/Source/Tetra/Parser/Param.hs --- a/DDC/Source/Tetra/Parser/Param.hs +++ b/DDC/Source/Tetra/Parser/Param.hs @@ -1,11 +1,12 @@ +-- | Desugaring of function parameter syntax in Source Tetra. module DDC.Source.Tetra.Parser.Param ( ParamSpec (..) , funTypeOfParams , pBindParamSpec , expOfParams) where -import DDC.Source.Tetra.Exp +import DDC.Source.Tetra.Exp.Annot import DDC.Core.Parser ( ParamSpec(..) , funTypeOfParams @@ -16,9 +17,9 @@ -- and the expression for the body. expOfParams :: a - -> [ParamSpec n] -- ^ Spec of parameters. - -> Exp a n -- ^ Body of function. - -> Exp a n -- ^ Expression of whole function. + -> [ParamSpec Name] -- ^ Spec of parameters. + -> Exp a -- ^ Body of function. + -> Exp a -- ^ Expression of whole function. expOfParams _ [] xBody = xBody expOfParams a (p:ps) xBody diff --git a/DDC/Source/Tetra/Parser/Witness.hs b/DDC/Source/Tetra/Parser/Witness.hs new file mode 100644 --- /dev/null +++ b/DDC/Source/Tetra/Parser/Witness.hs @@ -0,0 +1,100 @@ + +module DDC.Source.Tetra.Parser.Witness + ( pWitness + , pWitnessApp + , pWitnessAtom) +where +import DDC.Source.Tetra.Prim +import DDC.Source.Tetra.Exp.Annot +import DDC.Core.Parser + ( Parser + , Context (..) + , pType + , pConSP + , pIndexSP + , pVarSP + , pTok + , pTokSP) + +import DDC.Core.Lexer.Tokens +import DDC.Base.Parser ((), SourcePos) +import qualified DDC.Base.Parser as P +import qualified DDC.Type.Exp as T +import qualified DDC.Type.Compounds as T +import Control.Monad.Except + +type SP = SourcePos + + +-- | Parse a witness expression. +pWitness :: Context Name -> Parser Name (Witness SP) +pWitness c = pWitnessJoin c + + +-- | Parse a witness join. +pWitnessJoin :: Context Name -> Parser Name (Witness SP) +pWitnessJoin c + -- WITNESS or WITNESS & WITNESS + = do w1 <- pWitnessApp c + P.choice + [ do return w1 ] + + +-- | Parse a witness application. +pWitnessApp :: Context Name -> Parser Name (Witness SP) +pWitnessApp c + = do (x:xs) <- P.many1 (pWitnessArgSP c) + let x' = fst x + let sp = snd x + let xs' = map fst xs + return $ foldl (WApp sp) x' xs' + + "a witness expression or application" + + +-- | Parse a witness argument. +pWitnessArgSP :: Context Name -> Parser Name (Witness SP, SP) +pWitnessArgSP c + = P.choice + [ -- [TYPE] + do sp <- pTokSP KSquareBra + t <- pType c + pTok KSquareKet + return (WType sp t, sp) + + -- WITNESS + , do pWitnessAtomSP c ] + + + +-- | Parse a variable, constructor or parenthesised witness. +pWitnessAtom :: Context Name -> Parser Name (Witness SP) +pWitnessAtom c + = liftM fst (pWitnessAtomSP c) + + +-- | Parse a variable, constructor or parenthesised witness, +-- also returning source position. +pWitnessAtomSP :: Context Name -> Parser Name (Witness SP, SP) +pWitnessAtomSP c + = P.choice + -- (WITNESS) + [ do sp <- pTokSP KRoundBra + w <- pWitness c + pTok KRoundKet + return (w, sp) + + -- Named constructors + , do (con, sp) <- pConSP + return (WCon sp (WiConBound (T.UName con) (T.tBot T.kWitness)), sp) + + -- Debruijn indices + , do (i, sp) <- pIndexSP + return (WVar sp (T.UIx i), sp) + + -- Variables + , do (var, sp) <- pVarSP + return (WVar sp (T.UName var), sp) ] + + "a witness" + diff --git a/DDC/Source/Tetra/Predicates.hs b/DDC/Source/Tetra/Predicates.hs --- a/DDC/Source/Tetra/Predicates.hs +++ b/DDC/Source/Tetra/Predicates.hs @@ -1,4 +1,5 @@ +-- | Simple predicates on Source Tetra things. module DDC.Source.Tetra.Predicates ( module DDC.Type.Predicates @@ -23,13 +24,13 @@ -- * Patterns , isPDefault) where -import DDC.Source.Tetra.Exp +import DDC.Source.Tetra.Exp.Generic import DDC.Type.Predicates -- Atoms ---------------------------------------------------------------------- -- | Check whether an expression is a variable. -isXVar :: Exp a n -> Bool +isXVar :: GExp l -> Bool isXVar xx = case xx of XVar{} -> True @@ -37,7 +38,7 @@ -- | Check whether an expression is a constructor. -isXCon :: Exp a n -> Bool +isXCon :: GExp l -> Bool isXCon xx = case xx of XCon{} -> True @@ -46,7 +47,7 @@ -- | Check whether an expression is a `XVar` or an `XCon`, -- or some type or witness atom. -isAtomX :: Exp a n -> Bool +isAtomX :: GExp l -> Bool isAtomX xx = case xx of XVar{} -> True @@ -57,7 +58,7 @@ -- | Check whether a witness is a `WVar` or `WCon`. -isAtomW :: Witness a n -> Bool +isAtomW :: GWitness l -> Bool isAtomW ww = case ww of WVar{} -> True @@ -67,7 +68,7 @@ -- Lambdas -------------------------------------------------------------------- -- | Check whether an expression is a spec abstraction (level-1). -isXLAM :: Exp a n -> Bool +isXLAM :: GExp l -> Bool isXLAM xx = case xx of XLAM{} -> True @@ -75,7 +76,7 @@ -- | Check whether an expression is a value or witness abstraction (level-0). -isXLam :: Exp a n -> Bool +isXLam :: GExp l -> Bool isXLam xx = case xx of XLam{} -> True @@ -83,14 +84,14 @@ -- | Check whether an expression is a spec, value, or witness abstraction. -isLambdaX :: Exp a n -> Bool +isLambdaX :: GExp l -> Bool isLambdaX xx = isXLAM xx || isXLam xx -- Applications --------------------------------------------------------------- -- | Check whether an expression is an `XApp`. -isXApp :: Exp a n -> Bool +isXApp :: GExp l -> Bool isXApp xx = case xx of XApp{} -> True @@ -99,7 +100,7 @@ -- Let Bindings --------------------------------------------------------------- -- | Check whether an expression is a `XLet`. -isXLet :: Exp a n -> Bool +isXLet :: GExp l -> Bool isXLet xx = case xx of XLet{} -> True @@ -108,7 +109,7 @@ -- Type and Witness ----------------------------------------------------------- -- | Check whether an expression is an `XType` -isXType :: Exp a n -> Bool +isXType :: GExp l -> Bool isXType xx = case xx of XType{} -> True @@ -116,7 +117,7 @@ -- | Check whether an expression is an `XWitness` -isXWitness :: Exp a n -> Bool +isXWitness :: GExp l -> Bool isXWitness xx = case xx of XWitness{} -> True @@ -125,6 +126,7 @@ -- Patterns ------------------------------------------------------------------- -- | Check whether an alternative is a `PDefault`. -isPDefault :: Pat n -> Bool +isPDefault :: GPat l -> Bool isPDefault PDefault = True isPDefault _ = False + diff --git a/DDC/Source/Tetra/Pretty.hs b/DDC/Source/Tetra/Pretty.hs --- a/DDC/Source/Tetra/Pretty.hs +++ b/DDC/Source/Tetra/Pretty.hs @@ -1,20 +1,28 @@ +{-# LANGUAGE TypeFamilies, UndecidableInstances #-} -- | Pretty printing for Tetra modules and expressions. module DDC.Source.Tetra.Pretty ( module DDC.Core.Pretty - , module DDC.Base.Pretty ) + , module DDC.Base.Pretty + , PrettyLanguage) where -import DDC.Source.Tetra.Compounds import DDC.Source.Tetra.Predicates import DDC.Source.Tetra.DataDef import DDC.Source.Tetra.Module import DDC.Source.Tetra.Exp import DDC.Core.Pretty import DDC.Base.Pretty +import Prelude hiding ((<$>)) +type PrettyLanguage l + = ( Eq (GName l) + , Pretty (GAnnot l), Pretty (GName l) + , Pretty (GBound l), Pretty (GBind l), Pretty (GPrim l)) + + -- Module ----------------------------------------------------------------------------------------- -instance (Pretty n, Eq n) => Pretty (Module a n) where +instance PrettyLanguage l => Pretty (Module l) where ppr Module { moduleName = name , moduleExportTypes = _exportedTypes @@ -47,20 +55,15 @@ -- Top -------------------------------------------------------------------------------------------- -instance (Pretty n, Eq n) => Pretty (Top a n) where - ppr (TopBind _ b x) - = let dBind = if isBot (typeOfBind b) - then ppr (binderOfBind b) - else ppr b - in align ( dBind - <> nest 2 ( breakWhen (not $ isSimpleX x) - <> text "=" <+> align (ppr x))) +instance PrettyLanguage l => Pretty (Top l) where + ppr (TopClause _ c) = ppr c ppr (TopData _ (DataDef name params ctors)) - = hsep - ( [ text "data", ppr name] - ++ [parens $ ppr b | b <- params] - ++ [text "where" <+> lbrace]) + = (text "data" + <+> hsep ( ppr name + : map (parens . ppr) params) + <+> text "where" + <+> lbrace) <$> indent 8 (vcat [ ppr (dataCtorName ctor) <+> text ":" @@ -72,30 +75,28 @@ <> line <> rbrace + -- Exp -------------------------------------------------------------------------------------------- -instance (Pretty n, Eq n) => Pretty (Exp a n) where +instance PrettyLanguage l => Pretty (GExp l) where pprPrec d xx = {-# SCC "ppr[Exp]" #-} case xx of XVar _ u -> ppr u XCon _ dc -> ppr dc + XPrim _ u -> ppr u - XLAM{} - -> let Just (bs, xBody) = takeXLAMs xx - groups = partitionBindsByType bs - in pprParen' (d > 1) - $ (cat $ map (pprBinderGroup (text "/\\")) groups) + XLAM _ b xBody + -> pprParen' (d > 1) + $ text "/\\" <> ppr b <> text "." <> (if isXLAM xBody then empty else if isXLam xBody then line <> space else if isSimpleX xBody then space else line) <> ppr xBody - XLam{} - -> let Just (bs, xBody) = takeXLams xx - groups = partitionBindsByType bs - in pprParen' (d > 1) - $ (cat $ map (pprBinderGroup (text "\\")) groups) + XLam _ b xBody + -> pprParen' (d > 1) + $ text "\\" <> ppr b <> text "." <> breakWhen (not $ isSimpleX xBody) <> ppr xBody @@ -110,14 +111,6 @@ $ ppr lts <+> text "in" <$> ppr x - XCase _ x1 [AAlt p x2] - -> pprParen' (d > 2) - $ text "caselet" <+> ppr p - <+> nest 2 (breakWhen (not $ isSimpleX x1) - <> text "=" <+> align (ppr x1)) - <+> text "in" - <$> ppr x2 - XCase _ x alts -> pprParen' (d > 2) $ (nest 2 $ text "case" <+> ppr x <+> text "of" <+> lbrace <> line @@ -142,8 +135,7 @@ XWitness _ w -> text "<" <> ppr w <> text ">" XDefix _ xs - -> pprParen' (d > 2) - $ text "DEFIX" <+> hsep (map (pprPrec 11) xs) + -> text "[" <> text "DEFIX|" <+> hsep (map (pprPrec 11) xs) <+> text "]" XInfixOp _ str -> parens $ text "INFIXOP" <+> text "\"" <> text str <> text "\"" @@ -152,46 +144,18 @@ -> parens $ text "INFIXVAR" <+> text "\"" <> text str <> text "\"" --- Alt -------------------------------------------------------------------------------------------- -instance (Pretty n, Eq n) => Pretty (Alt a n) where - ppr (AAlt p x) - = ppr p <+> nest 1 (line <> nest 3 (text "->" <+> ppr x)) - - --- Cast ------------------------------------------------------------------------------------------- -instance (Pretty n, Eq n) => Pretty (Cast a n) where - ppr cc - = case cc of - CastWeakenEffect eff - -> text "weakeff" <+> brackets (ppr eff) - - CastPurify w - -> text "purify" <+> angles (ppr w) - - CastBox - -> text "box" - - CastRun - -> text "run" - - -- Lets ------------------------------------------------------------------------------------------- -instance (Pretty n, Eq n) => Pretty (Lets a n) where +instance PrettyLanguage l => Pretty (GLets l) where ppr lts = case lts of LLet b x - -> let dBind = if isBot (typeOfBind b) - then ppr (binderOfBind b) - else ppr b - in text "let" - <+> align ( dBind + -> text "let" + <+> align ( ppr b <> nest 2 ( breakWhen (not $ isSimpleX x) <> text "=" <+> align (ppr x))) LRec bxs -> let pprLetRecBind (b, x) - = ppr (binderOfBind b) - <+> text ":" - <+> ppr (typeOfBind b) + = ppr b <> nest 2 ( breakWhen (not $ isSimpleX x) <> text "=" <+> align (ppr x)) @@ -204,11 +168,11 @@ LPrivate bs Nothing [] -> text "private" - <+> (hcat $ punctuate space (map (ppr . binderOfBind) bs)) + <+> (hcat $ punctuate space (map ppr bs)) LPrivate bs Nothing bsWit -> text "private" - <+> (hcat $ punctuate space (map (ppr . binderOfBind) bs)) + <+> (hcat $ punctuate space (map ppr bs)) <+> text "with" <+> braces (cat $ punctuate (text "; ") $ map ppr bsWit) @@ -216,42 +180,107 @@ -> text "extend" <+> ppr parent <+> text "using" - <+> (hcat $ punctuate space (map (ppr . binderOfBind) bs)) + <+> (hcat $ punctuate space (map ppr bs)) LPrivate bs (Just parent) bsWit -> text "extend" <+> ppr parent <+> text "using" - <+> (hcat $ punctuate space (map (ppr . binderOfBind) bs)) + <+> (hcat $ punctuate space (map ppr bs)) <+> text "with" <+> braces (cat $ punctuate (text "; ") $ map ppr bsWit) + LGroup cs + -> vcat $ map ppr cs --- Binder ----------------------------------------------------------------------------------------- -pprBinder :: Pretty n => Binder n -> Doc -pprBinder bb - = case bb of - RName v -> ppr v - RAnon -> text "^" - RNone -> text "_" +-- Clause ----------------------------------------------------------------------------------------- +instance PrettyLanguage l => Pretty (GClause l) where + ppr (SSig _ b t) + = ppr b <+> text ":" <+> ppr t --- | Print a group of binders with the same type. -pprBinderGroup - :: (Pretty n, Eq n) - => Doc -> ([Binder n], Type n) -> Doc + ppr (SLet _ b ps [GExp x]) + = ppr b <+> hsep (map ppr ps) + <> nest 2 ( breakWhen (not $ isSimpleX x) + <> text "=" <+> align (ppr x)) -pprBinderGroup lam (rs, t) - = lam <> parens ((hsep $ map pprBinder rs) <+> text ":" <+> ppr t) <> dot + ppr (SLet _ b ps gxs) + = ppr b <+> hsep (map ppr ps) + <> nest 2 (line <> vcat (map (pprGuardedExp "=") gxs)) +-- Alt -------------------------------------------------------------------------------------------- +instance PrettyLanguage l => Pretty (GAlt l) where + ppr (AAlt p gxs) + = ppr p <> nest 2 (line <> vcat (map (pprGuardedExp "->") gxs)) + + +-- Pat -------------------------------------------------------------------------------------------- +instance PrettyLanguage l => Pretty (GPat l) where + ppr pp + = case pp of + PDefault -> text "_" + PData u bs -> ppr u <+> sep (map ppr bs) + + +-- GuardedExp ------------------------------------------------------------------------------------- +pprGuardedExp :: PrettyLanguage l => String -> GGuardedExp l -> Doc +pprGuardedExp sTerm gx + = pprGs "|" gx + where + pprGs _c (GExp x) + = text sTerm <+> ppr x + + pprGs c (GGuard g gs) + = pprG c g <> line <> pprGs "," gs + + pprG c (GPat p x) + = text c <+> ppr p <+> text "<-" <+> ppr x + + pprG c (GPred x) + = text c <+> ppr x + + pprG c GDefault + = text c <+> text "otherwise" + + +-- Guard ------------------------------------------------------------------------------------------ +instance PrettyLanguage l => Pretty (GGuard l) where + + +-- Cast ------------------------------------------------------------------------------------------- +instance PrettyLanguage l => Pretty (GCast l) where + ppr cc + = case cc of + CastWeakenEffect eff -> text "weakeff" <+> brackets (ppr eff) + CastPurify w -> text "purify" <+> angles (ppr w) + CastBox -> text "box" + CastRun -> text "run" + + +-- Witness ---------------------------------------------------------------------------------------- +instance PrettyLanguage l => Pretty (GWitness l) where + pprPrec d ww + = case ww of + WVar _ n -> ppr n + WCon _ wc -> ppr wc + WApp _ w1 w2 -> pprParen (d > 10) (ppr w1 <+> pprPrec 11 w2) + WType _ t -> text "[" <> ppr t <> text "]" + + +instance PrettyLanguage l => Pretty (GWiCon l) where + ppr wc + = case wc of + WiConBound u _ -> ppr u + + -- Utils ------------------------------------------------------------------------------------------ breakWhen :: Bool -> Doc breakWhen True = line breakWhen False = space -isSimpleX :: Exp a n -> Bool +isSimpleX :: GExp l -> Bool isSimpleX xx = case xx of XVar{} -> True diff --git a/DDC/Source/Tetra/Prim.hs b/DDC/Source/Tetra/Prim.hs --- a/DDC/Source/Tetra/Prim.hs +++ b/DDC/Source/Tetra/Prim.hs @@ -1,121 +1,294 @@ +-- | Definitions of Source Tetra primitive names and operators. module DDC.Source.Tetra.Prim - ( Name (..) - , TyConTetra (..) - , kindTyConTetra + ( -- * Names + Name (..) - , OpStore (..) - , typeOpStore + -- * Primitive Names + , PrimName (..) + , pattern NameType + , pattern NameVal + , readName + -- * Primitive Types + , PrimType (..) + , pattern NameTyCon + , pattern NameTyConTetra + + -- ** Primitive machine type constructors. , PrimTyCon (..) , kindPrimTyCon , tBool , tNat , tInt + , tSize , tWord + , tFloat + , tTextLit + -- ** Primitive tetra type constructors. + , PrimTyConTetra(..) + , pattern NameTyConTetraTuple + , pattern NameTyConTetraF + , pattern NameTyConTetraC + , pattern NameTyConTetraU + , kindPrimTyConTetra + + -- * Primitive values + , PrimVal (..) + , pattern NameLit + , pattern NameArith + , pattern NameVector + , pattern NameFun + , pattern NameError + + -- ** Primitive arithmetic operators. , PrimArith (..) , typePrimArith - , readName) + + -- ** Primitive vector operators. + , OpVector (..) + , typeOpVector + + -- ** Primitive function operators. + , OpFun (..) + , typeOpFun + + -- ** Primitive error handling + , OpError (..) + , typeOpError + + -- ** Primitive literals + , PrimLit (..) + , pattern NameLitBool + , pattern NameLitNat + , pattern NameLitInt + , pattern NameLitSize + , pattern NameLitWord + , pattern NameLitFloat + , pattern NameLitTextLit) where -import DDC.Source.Tetra.Lexer.Lit import DDC.Source.Tetra.Prim.Base import DDC.Source.Tetra.Prim.TyConPrim import DDC.Source.Tetra.Prim.TyConTetra -import DDC.Source.Tetra.Prim.OpStore import DDC.Source.Tetra.Prim.OpArith +import DDC.Source.Tetra.Prim.OpFun +import DDC.Source.Tetra.Prim.OpVector +import DDC.Source.Tetra.Prim.OpError +import DDC.Core.Lexer.Names (isVarStart) import DDC.Base.Pretty import Control.DeepSeq import Data.Char +import qualified Data.Text as T import DDC.Core.Tetra ( readPrimTyCon - , readPrimArith - , readOpStore) + , readPrimArithFlag + , readOpFun + , readOpErrorFlag + , readOpVectorFlag) +import DDC.Core.Salt.Name + ( readLitNat + , readLitInt + , readLitSize + , readLitWordOfBits + , readLitFloatOfBits) + +--------------------------------------------------------------------------------------------------- +instance Pretty Name where + ppr nn + = case nn of + NameVar v -> text v + NameCon c -> text c + NamePrim p -> ppr p + NameHole -> text "?" + + instance NFData Name where rnf nn = case nn of NameVar s -> rnf s NameCon s -> rnf s + NamePrim p -> rnf p + NameHole -> () - NameTyConTetra p -> rnf p - NameOpStore p -> rnf p - NamePrimTyCon p -> rnf p - NamePrimArith p -> rnf p - NameLitBool b -> rnf b - NameLitNat n -> rnf n - NameLitInt i -> rnf i - NameLitWord i bits -> rnf i `seq` rnf bits +-- | Read the name of a variable, constructor or literal. +readName :: String -> Maybe Name +readName str + -- Primitive names. + | Just n <- readPrimName str + = Just $ NamePrim n - NameHole -> () + -- Constructors. + | c : _ <- str + , isUpper c + = Just $ NameCon str + -- Variables. + | c : _ <- str + , isVarStart c + = Just $ NameVar str -instance Pretty Name where + | otherwise + = Nothing + + +--------------------------------------------------------------------------------------------------- +instance Pretty PrimName where ppr nn = case nn of - NameVar v -> text v - NameCon c -> text c + PrimNameType p -> ppr p + PrimNameVal p -> ppr p - NameTyConTetra p -> ppr p - NameOpStore p -> ppr p - NamePrimTyCon p -> ppr p - NamePrimArith p -> ppr p - NameLitBool True -> text "True#" - NameLitBool False -> text "False#" - NameLitNat i -> integer i - NameLitInt i -> integer i <> text "i" - NameLitWord i bits -> integer i <> text "w" <> int bits +instance NFData PrimName where + rnf nn + = case nn of + PrimNameType p -> rnf p + PrimNameVal p -> rnf p - NameHole -> text "?" +readPrimName :: String -> Maybe PrimName +readPrimName str + | Just t <- readPrimType str + = Just $ PrimNameType t --- | Read the name of a variable, constructor or literal. -readName :: String -> Maybe Name -readName str - -- Baked-in names - | Just p <- readTyConTetra str - = Just $ NameTyConTetra p + | Just v <- readPrimVal str + = Just $ PrimNameVal v - | Just p <- readOpStore str - = Just $ NameOpStore p + | otherwise + = Nothing - -- Primitive names. - | Just p <- readPrimTyCon str - = Just $ NamePrimTyCon p - | Just p <- readPrimArith str - = Just $ NamePrimArith p +--------------------------------------------------------------------------------------------------- +instance Pretty PrimType where + ppr t + = case t of + PrimTypeTyConTetra p -> ppr p + PrimTypeTyCon p -> ppr p + +instance NFData PrimType where + rnf t + = case t of + PrimTypeTyConTetra p -> rnf p + PrimTypeTyCon p -> rnf p + + +-- | Read the name of a primitive type. +readPrimType :: String -> Maybe PrimType +readPrimType str + | Just p <- readPrimTyConTetra str + = Just $ PrimTypeTyConTetra p + + | Just p <- readPrimTyCon str + = Just $ PrimTypeTyCon p + + | otherwise + = Nothing + + +--------------------------------------------------------------------------------------------------- +instance Pretty PrimVal where + ppr val + = case val of + PrimValError p -> ppr p + PrimValLit lit -> ppr lit + PrimValArith p -> ppr p + PrimValVector p -> ppr p + PrimValFun p -> ppr p + + +instance NFData PrimVal where + rnf val + = case val of + PrimValError p -> rnf p + PrimValLit lit -> rnf lit + PrimValArith p -> rnf p + PrimValVector p -> rnf p + PrimValFun p -> rnf p + + +-- | Read the name of a primtive value. +readPrimVal :: String -> Maybe PrimVal +readPrimVal str + | Just (p, False) <- readOpErrorFlag str + = Just $ PrimValError p + + | Just lit <- readPrimLit str + = Just $ PrimValLit lit + + | Just (p, False) <- readPrimArithFlag str + = Just $ PrimValArith p + + | Just (p, False) <- readOpVectorFlag str + = Just $ PrimValVector p + + | Just p <- readOpFun str + = Just $ PrimValFun p + + | otherwise + = Nothing + + +--------------------------------------------------------------------------------------------------- +instance Pretty PrimLit where + ppr lit + = case lit of + PrimLitBool True -> text "True" + PrimLitBool False -> text "False" + PrimLitNat i -> integer i + PrimLitInt i -> integer i <> text "i" + PrimLitSize s -> integer s <> text "s" + PrimLitWord i bits -> integer i <> text "w" <> int bits + PrimLitFloat f bits -> double f <> text "f" <> int bits + PrimLitTextLit tx -> text (show $ T.unpack tx) + + +instance NFData PrimLit where + rnf lit + = case lit of + PrimLitBool b -> rnf b + PrimLitNat n -> rnf n + PrimLitInt i -> rnf i + PrimLitSize s -> rnf s + PrimLitWord i bits -> rnf i `seq` rnf bits + PrimLitFloat d bits -> rnf d `seq` rnf bits + PrimLitTextLit bs -> rnf bs + + +-- | Read the name of a primitive literal. +readPrimLit :: String -> Maybe PrimLit +readPrimLit str -- Literal Bools - | str == "True#" = Just $ NameLitBool True - | str == "False#" = Just $ NameLitBool False + | str == "True" = Just $ PrimLitBool True + | str == "False" = Just $ PrimLitBool False -- Literal Nat | Just val <- readLitNat str - = Just $ NameLitNat val + = Just $ PrimLitNat val -- Literal Ints | Just val <- readLitInt str - = Just $ NameLitInt val + = Just $ PrimLitInt val + -- Literal Sizes + | Just val <- readLitSize str + = Just $ PrimLitSize val + -- Literal Words | Just (val, bits) <- readLitWordOfBits str , elem bits [8, 16, 32, 64] - = Just $ NameLitWord val bits - - -- Constructors. - | c : _ <- str - , isUpper c - = Just $ NameCon str + = Just $ PrimLitWord val bits - -- Variables. - | c : _ <- str - , isLower c - = Just $ NameVar str + -- Literal Floats + | Just (val, bits) <- readLitFloatOfBits str + , elem bits [32, 64] + = Just $ PrimLitFloat val bits | otherwise = Nothing + diff --git a/DDC/Source/Tetra/Prim/Base.hs b/DDC/Source/Tetra/Prim/Base.hs --- a/DDC/Source/Tetra/Prim/Base.hs +++ b/DDC/Source/Tetra/Prim/Base.hs @@ -1,67 +1,199 @@ +-- | Definition of names used in Source Tetra language. module DDC.Source.Tetra.Prim.Base - ( Name (..) - , TyConTetra (..) - , OpStore (..) + ( -- * Names + Name (..) + + -- * Primitive Names + , PrimName (..) + , pattern NameType + , pattern NameVal + + -- * Primitive Types + , PrimType (..) + , pattern NameTyCon + , pattern NameTyConTetra + + -- ** Primitive machine type constructors. , PrimTyCon (..) - , PrimArith (..)) + + -- ** Primitive Tetra specific type constructors. + , PrimTyConTetra(..) + , pattern NameTyConTetraTuple + , pattern NameTyConTetraVector + , pattern NameTyConTetraF + , pattern NameTyConTetraC + , pattern NameTyConTetraU + + -- * Primitive Values + , PrimVal (..) + , pattern NameLit + , pattern NameArith + , pattern NameVector + , pattern NameFun + , pattern NameError + + -- ** Primitive arithmetic operators. + , PrimArith (..) + + -- ** Primitive vector operators. + , OpVector (..) + + -- ** Primitive function operators. + , OpFun (..) + + -- ** Primitive error handling. + , OpError (..) + + -- ** Primitive literals. + , PrimLit (..) + , pattern NameLitBool + , pattern NameLitNat + , pattern NameLitInt + , pattern NameLitSize + , pattern NameLitWord + , pattern NameLitFloat + , pattern NameLitTextLit) where import DDC.Core.Tetra - ( OpStore (..) + ( OpFun (..) + , OpVector (..) + , OpError (..) , PrimTyCon (..) , PrimArith (..)) +import Data.Text (Text) + +--------------------------------------------------------------------------------------------------- -- | Names of things used in Disciple Source Tetra. data Name -- | A user defined variable. - = NameVar String + = NameVar !String -- | A user defined constructor. - | NameCon String + | NameCon !String - -- Baked in things ---------------------- - -- | Baked in data type constructors. - | NameTyConTetra TyConTetra + -- | Primitive names. + | NamePrim !PrimName - -- | Baked in store operators. - | NameOpStore OpStore + -- Inference ---------------------------- + -- | A hole used during type inference. + | NameHole + deriving (Eq, Ord, Show) - -- Machine primitives ------------------- - -- | Primitive type cosntructors. - | NamePrimTyCon PrimTyCon - -- | Primitive arithmetic, logic and comparison. - | NamePrimArith PrimArith +--------------------------------------------------------------------------------------------------- +-- | Primitive names. +data PrimName + = PrimNameType !PrimType + | PrimNameVal !PrimVal + deriving (Eq, Ord, Show) - -- Literals ----------------------------- - -- | A boolean literal. - | NameLitBool Bool +pattern NameType p = NamePrim (PrimNameType p) +pattern NameVal p = NamePrim (PrimNameVal p) - -- | A natural literal. - | NameLitNat Integer - -- | An integer literal. - | NameLitInt Integer - - -- | A word literal. - | NameLitWord Integer Int +--------------------------------------------------------------------------------------------------- +-- | Primitive types. +data PrimType + -- | Primitive machine type constructors. + = PrimTypeTyCon !PrimTyCon - -- Inference ---------------------------- - -- | A hole used during type inference. - | NameHole + -- | Primtiive type constructors specific to the Tetra fragment. + | PrimTypeTyConTetra !PrimTyConTetra deriving (Eq, Ord, Show) +pattern NameTyCon tc = NamePrim (PrimNameType (PrimTypeTyCon tc)) +pattern NameTyConTetra tc = NamePrim (PrimNameType (PrimTypeTyConTetra tc)) --- TyConTetra ---------------------------------------------------------------- --- | Baked-in type constructors. -data TyConTetra - -- | @Ref#@. Mutable reference. - = TyConTetraRef +--------------------------------------------------------------------------------------------------- +-- | Primitive type constructors specific to the Tetra language fragment. +data PrimTyConTetra -- | @TupleN#@. Tuples. - | TyConTetraTuple Int + = PrimTyConTetraTuple !Int + + -- | @Vector#@. Vectors. + | PrimTyConTetraVector + + -- | @F#@. Reified function values. + | PrimTyConTetraF + + -- | @C#@. Reified function closures. + | PrimTyConTetraC + + -- | @U#@. Explicitly unboxed values. + | PrimTyConTetraU deriving (Eq, Ord, Show) +pattern NameTyConTetraTuple i = NameTyConTetra (PrimTyConTetraTuple i) +pattern NameTyConTetraVector = NameTyConTetra PrimTyConTetraVector +pattern NameTyConTetraF = NameTyConTetra PrimTyConTetraF +pattern NameTyConTetraC = NameTyConTetra PrimTyConTetraC +pattern NameTyConTetraU = NameTyConTetra PrimTyConTetraU + +--------------------------------------------------------------------------------------------------- +-- | Primitive values. +data PrimVal + -- | Primitive literals. + = PrimValLit !PrimLit + + -- | Primitive arithmetic operators. + | PrimValArith !PrimArith + + -- | Primitive error handling. + | PrimValError !OpError + + -- | Primitive vector operators. + | PrimValVector !OpVector + + -- | Primitive function operators. + | PrimValFun !OpFun + deriving (Eq, Ord, Show) + +pattern NameLit p = NamePrim (PrimNameVal (PrimValLit p)) +pattern NameArith p = NamePrim (PrimNameVal (PrimValArith p)) +pattern NameError p = NamePrim (PrimNameVal (PrimValError p)) +pattern NameVector p = NamePrim (PrimNameVal (PrimValVector p)) +pattern NameFun p = NamePrim (PrimNameVal (PrimValFun p)) + + +--------------------------------------------------------------------------------------------------- +data PrimLit + -- | A boolean literal. + = PrimLitBool !Bool + + -- | A natural literal, + -- with enough precision to count every heap object. + | PrimLitNat !Integer + + -- | An integer literal, + -- with enough precision to count every heap object. + | PrimLitInt !Integer + + -- | An unsigned size literal, + -- with enough precision to count every addressable byte of memory. + | PrimLitSize !Integer + + -- | A word literal, + -- with the given number of bits precison. + | PrimLitWord !Integer !Int + + -- | A floating point literal, + -- with the given number of bits precision. + | PrimLitFloat !Double !Int + + -- | Text literals (UTF-8 encoded) + | PrimLitTextLit !Text + deriving (Eq, Ord, Show) + +pattern NameLitBool x = NameLit (PrimLitBool x) +pattern NameLitNat x = NameLit (PrimLitNat x) +pattern NameLitInt x = NameLit (PrimLitInt x) +pattern NameLitSize x = NameLit (PrimLitSize x) +pattern NameLitWord x s = NameLit (PrimLitWord x s) +pattern NameLitFloat x s = NameLit (PrimLitFloat x s) +pattern NameLitTextLit x = NameLit (PrimLitTextLit x) diff --git a/DDC/Source/Tetra/Prim/OpArith.hs b/DDC/Source/Tetra/Prim/OpArith.hs --- a/DDC/Source/Tetra/Prim/OpArith.hs +++ b/DDC/Source/Tetra/Prim/OpArith.hs @@ -1,4 +1,5 @@ +-- | Types of primitive Source Tetra arithmetic operators. module DDC.Source.Tetra.Prim.OpArith (typePrimArith) where diff --git a/DDC/Source/Tetra/Prim/OpError.hs b/DDC/Source/Tetra/Prim/OpError.hs new file mode 100644 --- /dev/null +++ b/DDC/Source/Tetra/Prim/OpError.hs @@ -0,0 +1,19 @@ + +module DDC.Source.Tetra.Prim.OpError + ( typeOpError) +where +import DDC.Source.Tetra.Prim.TyConPrim +import DDC.Source.Tetra.Prim.Base +import DDC.Type.Compounds +import DDC.Type.Exp + + + +-- | Take the type of a primitive error function. +typeOpError :: OpError -> Type Name +typeOpError err + = case err of + OpErrorDefault + -> tForall kData $ \t -> tTextLit `tFun` tNat `tFun` t + + diff --git a/DDC/Source/Tetra/Prim/OpFun.hs b/DDC/Source/Tetra/Prim/OpFun.hs new file mode 100644 --- /dev/null +++ b/DDC/Source/Tetra/Prim/OpFun.hs @@ -0,0 +1,69 @@ + +-- | Types of primitive Source Tetra function operators. +module DDC.Source.Tetra.Prim.OpFun + (typeOpFun) +where +import DDC.Source.Tetra.Prim.TyConTetra +import DDC.Source.Tetra.Prim.Base +import DDC.Type.Compounds +import DDC.Type.Exp + + +-- | Take the type of a primitive function operator. +typeOpFun :: OpFun -> Type Name +typeOpFun op + = case op of + OpFunCurry n + -> tForalls (replicate (n + 1) kData) + $ \ts -> + let Just tF = tFunOfList ts + Just result = tFunOfList (tF : ts) + in result + + OpFunApply n + -> tForalls (replicate (n + 1) kData) + $ \ts -> + let Just tF = tFunOfList ts + Just result = tFunOfList (tF : ts) + in result + + OpFunCReify + -> tForalls [kData, kData] + $ \[tA, tB] -> (tA `tFun` tB) `tFun` tFunValue (tA `tFun` tB) + + OpFunCCurry n + -> tForalls (replicate (n + 1) kData) + $ \ts -> + let tLast : tsFront' = reverse ts + tsFront = reverse tsFront' + Just tF = tFunOfList ts + Just result + = tFunOfList + ( tFunValue tF + : tsFront ++ [tCloValue tLast]) + in result + + OpFunCExtend n + -> tForalls (replicate (n + 1) kData) + $ \ts -> + let tLast : tsFront' = reverse ts + tsFront = reverse tsFront' + Just tF = tFunOfList ts + Just result + = tFunOfList + ( tCloValue tF + : tsFront ++ [tCloValue tLast]) + in result + + OpFunCApply n + -> tForalls (replicate (n + 1) kData) + $ \ts -> + let tLast : tsFront' = reverse ts + tsFront = reverse tsFront' + Just tF = tFunOfList ts + Just result + = tFunOfList + ( tCloValue tF + : tsFront ++ [tLast]) + in result + diff --git a/DDC/Source/Tetra/Prim/OpStore.hs b/DDC/Source/Tetra/Prim/OpStore.hs deleted file mode 100644 --- a/DDC/Source/Tetra/Prim/OpStore.hs +++ /dev/null @@ -1,13 +0,0 @@ - -module DDC.Source.Tetra.Prim.OpStore - (typeOpStore) -where -import DDC.Source.Tetra.Prim.Base -import DDC.Source.Tetra.Exp - - --- | Take the type of a primitive arithmetic operator. -typeOpStore :: OpStore -> Maybe (Type Name) -typeOpStore op - = case op of - _ -> Nothing diff --git a/DDC/Source/Tetra/Prim/OpVector.hs b/DDC/Source/Tetra/Prim/OpVector.hs new file mode 100644 --- /dev/null +++ b/DDC/Source/Tetra/Prim/OpVector.hs @@ -0,0 +1,32 @@ + +-- Types of primitive Source Tetra vector operators. +module DDC.Source.Tetra.Prim.OpVector + (typeOpVector) +where +import DDC.Source.Tetra.Prim.TyConPrim +import DDC.Source.Tetra.Prim.TyConTetra +import DDC.Source.Tetra.Prim.Base +import DDC.Type.Compounds +import DDC.Type.Exp + + +-- | Take the type of a primitive vector operator. +typeOpVector :: OpVector -> Type Name +typeOpVector op + = case op of + OpVectorAlloc + -> tForalls [kRegion, kData] + $ \[tR, tA] -> tNat `tFun` tSusp (tAlloc tR) (tVector tR tA) + + OpVectorLength + -> tForalls [kRegion, kData] + $ \[tR, tA] -> tVector tR tA `tFun` tNat + + OpVectorRead + -> tForalls [kRegion, kData] + $ \[tR, tA] -> tVector tR tA `tFun` tNat `tFun` tSusp (tRead tR) tA + + OpVectorWrite + -> tForalls [kRegion, kData] + $ \[tR, tA] -> tVector tR tA `tFun` tNat `tFun` tA `tFun` tSusp (tWrite tR) tVoid + diff --git a/DDC/Source/Tetra/Prim/TyConPrim.hs b/DDC/Source/Tetra/Prim/TyConPrim.hs --- a/DDC/Source/Tetra/Prim/TyConPrim.hs +++ b/DDC/Source/Tetra/Prim/TyConPrim.hs @@ -1,7 +1,9 @@ +-- | Definitions of primitive types for Source Tetra language. module DDC.Source.Tetra.Prim.TyConPrim ( kindPrimTyCon - , tBool, tNat, tInt, tWord) + , tVoid, tBool, tNat, tInt, tSize, tWord, tFloat + , tTextLit) where import DDC.Source.Tetra.Prim.Base import DDC.Type.Compounds @@ -13,36 +15,58 @@ kindPrimTyCon tc = case tc of PrimTyConVoid -> kData - PrimTyConPtr -> (kRegion `kFun` kData `kFun` kData) - PrimTyConAddr -> kData PrimTyConBool -> kData PrimTyConNat -> kData PrimTyConInt -> kData + PrimTyConSize -> kData PrimTyConWord _ -> kData PrimTyConFloat _ -> kData + PrimTyConVec _ -> kData `kFun` kData + PrimTyConAddr -> kData + PrimTyConPtr -> kRegion `kFun` kData `kFun` kData + PrimTyConTextLit -> kData PrimTyConTag -> kData - PrimTyConVec _ -> kData `kFun` kData - PrimTyConString -> kData -- Compounds ------------------------------------------------------------------ +-- | Primitive `Void` type. +tVoid :: Type Name +tVoid = TCon (TyConBound (UPrim (NameTyCon PrimTyConVoid) kData) kData) + + -- | Primitive `Bool` type. tBool :: Type Name -tBool = TCon (TyConBound (UPrim (NamePrimTyCon PrimTyConBool) kData) kData) +tBool = TCon (TyConBound (UPrim (NameTyCon PrimTyConBool) kData) kData) -- | Primitive `Nat` type. -tNat :: Type Name -tNat = TCon (TyConBound (UPrim (NamePrimTyCon PrimTyConNat) kData) kData) +tNat :: Type Name +tNat = TCon (TyConBound (UPrim (NameTyCon PrimTyConNat) kData) kData) -- | Primitive `Int` type. -tInt :: Type Name -tInt = TCon (TyConBound (UPrim (NamePrimTyCon PrimTyConInt) kData) kData) +tInt :: Type Name +tInt = TCon (TyConBound (UPrim (NameTyCon PrimTyConInt) kData) kData) +-- | Primitive `Size` type. +tSize :: Type Name +tSize = TCon (TyConBound (UPrim (NameTyCon PrimTyConSize) kData) kData) + + -- | Primitive `WordN` type of the given width. tWord :: Int -> Type Name tWord bits - = TCon (TyConBound (UPrim (NamePrimTyCon (PrimTyConWord bits)) kData) kData) + = TCon (TyConBound (UPrim (NameTyCon (PrimTyConWord bits)) kData) kData) + +-- | Primitive `FloatN` type of the given width. +tFloat :: Int -> Type Name +tFloat bits + = TCon (TyConBound (UPrim (NameTyCon (PrimTyConFloat bits)) kData) kData) + + +-- | Primitive `TextLit` type. +tTextLit :: Type Name +tTextLit + = TCon (TyConBound (UPrim (NameTyCon PrimTyConTextLit) kData) kData) diff --git a/DDC/Source/Tetra/Prim/TyConTetra.hs b/DDC/Source/Tetra/Prim/TyConTetra.hs --- a/DDC/Source/Tetra/Prim/TyConTetra.hs +++ b/DDC/Source/Tetra/Prim/TyConTetra.hs @@ -1,8 +1,11 @@ +-- | Definitions of primitive type constructors for Source Tetra language. module DDC.Source.Tetra.Prim.TyConTetra - ( kindTyConTetra - , readTyConTetra - , tRef) + ( kindPrimTyConTetra + , readPrimTyConTetra + , tVector + , tFunValue + , tCloValue) where import DDC.Source.Tetra.Prim.Base import DDC.Type.Compounds @@ -12,43 +15,67 @@ import Data.List import Control.DeepSeq -instance NFData TyConTetra -instance Pretty TyConTetra where +instance NFData PrimTyConTetra where + rnf !_ = () + + +instance Pretty PrimTyConTetra where ppr tc = case tc of - TyConTetraRef -> text "Ref#" - TyConTetraTuple n -> text "Tuple" <> int n <> text "#" + PrimTyConTetraTuple n -> text "Tuple" <> int n + PrimTyConTetraVector -> text "Vector" + PrimTyConTetraF -> text "F#" + PrimTyConTetraC -> text "C#" + PrimTyConTetraU -> text "U#" -- | Read the name of a baked-in type constructor. -readTyConTetra :: String -> Maybe TyConTetra -readTyConTetra str +readPrimTyConTetra :: String -> Maybe PrimTyConTetra +readPrimTyConTetra str | Just rest <- stripPrefix "Tuple" str - , (ds, "#") <- span isDigit rest + , (ds, "") <- span isDigit rest , not $ null ds , arity <- read ds - = Just $ TyConTetraTuple arity + = Just $ PrimTyConTetraTuple arity | otherwise = case str of - "Ref#" -> Just TyConTetraRef + "Vector#" -> Just PrimTyConTetraVector + "F#" -> Just PrimTyConTetraF + "C#" -> Just PrimTyConTetraC + "U#" -> Just PrimTyConTetraU _ -> Nothing -- | Take the kind of a baked-in data constructor. -kindTyConTetra :: TyConTetra -> Type Name -kindTyConTetra tc +kindPrimTyConTetra :: PrimTyConTetra -> Type Name +kindPrimTyConTetra tc = case tc of - TyConTetraRef -> kRegion `kFun` kData `kFun` kData - TyConTetraTuple n -> foldr kFun kData (replicate n kData) + PrimTyConTetraTuple n -> foldr kFun kData (replicate n kData) + PrimTyConTetraVector -> kRegion `kFun` kData `kFun` kData + PrimTyConTetraF -> kData `kFun` kData + PrimTyConTetraC -> kData `kFun` kData + PrimTyConTetraU -> kData `kFun` kData -- Compounds ------------------------------------------------------------------ --- | Primitive `Ref` type. -tRef :: Region Name -> Type Name -> Type Name -tRef tR tA - = tApps (TCon (TyConBound (UPrim (NameTyConTetra TyConTetraRef) k) k)) - [tR, tA] +-- | Primitive `Vector` type. +tVector :: Region Name -> Type Name -> Type Name +tVector tR tA + = tApps (TCon (TyConBound (UPrim (NameTyConTetra PrimTyConTetraVector) k) k)) + [tR, tA] where k = kRegion `kFun` kData `kFun` kData + + +tFunValue :: Type Name -> Type Name +tFunValue tA + = tApps (TCon (TyConBound (UPrim (NameTyConTetra PrimTyConTetraF) k) k)) [tA] + where k = kData `kFun` kData + + +tCloValue :: Type Name -> Type Name +tCloValue tA + = tApps (TCon (TyConBound (UPrim (NameTyConTetra PrimTyConTetraC) k) k)) [tA] + where k = kData `kFun` kData diff --git a/DDC/Source/Tetra/ToCore.hs b/DDC/Source/Tetra/ToCore.hs deleted file mode 100644 --- a/DDC/Source/Tetra/ToCore.hs +++ /dev/null @@ -1,306 +0,0 @@ - -module DDC.Source.Tetra.ToCore - (toCoreModule) -where -import qualified DDC.Source.Tetra.Module as S -import qualified DDC.Source.Tetra.DataDef as S -import qualified DDC.Source.Tetra.Exp as S -import qualified DDC.Source.Tetra.Prim as S - -import qualified DDC.Core.Tetra.Prim as C -import qualified DDC.Core.Compounds as C -import qualified DDC.Core.Module as C -import qualified DDC.Core.Exp as C -import qualified DDC.Type.DataDef as C - -import qualified DDC.Type.Sum as Sum -import Data.Maybe - --- Things shared between both Source and Core languages. -import DDC.Core.Exp - ( Bind (..) - , Bound (..) - , Type (..) - , TyCon (..) - , Pat (..) - , DaCon (..) - , Witness (..) - , WiCon (..)) - -import DDC.Core.Module - ( ExportSource (..) - , ImportSource (..)) - - --- Module --------------------------------------------------------------------- --- | Convert a Source Tetra module to Core Tetra. --- --- The Source code needs to already have been desugared and cannot contain, --- and `XDefix`, `XInfixOp`, or `XInfixVar` nodes, else `error`. --- -toCoreModule :: a -> S.Module a S.Name -> C.Module a C.Name -toCoreModule a mm - = C.ModuleCore - { C.moduleName = S.moduleName mm - - , C.moduleExportTypes - = [ (toCoreN n, ExportSourceLocalNoType (toCoreN n)) - | n <- S.moduleExportTypes mm ] - - , C.moduleExportValues - = [ (toCoreN n, ExportSourceLocalNoType (toCoreN n)) - | n <- S.moduleExportValues mm ] - - , C.moduleImportTypes - = [ (toCoreN n, toCoreImportSource isrc) - | (n, isrc) <- S.moduleImportTypes mm ] - - , C.moduleImportValues - = [ (toCoreN n, toCoreImportSource isrc) - | (n, isrc) <- S.moduleImportValues mm ] - - , C.moduleDataDefsLocal - = [ toCoreDataDef def - | S.TopData _ def <- S.moduleTops mm ] - - , C.moduleBody - = C.XLet a (letsOfTops (S.moduleTops mm)) - (C.xUnit a) } - - --- | Extract the top-level bindings from some source definitions. -letsOfTops :: [S.Top a S.Name] -> C.Lets a C.Name -letsOfTops tops - = C.LRec $ mapMaybe bindOfTop tops - - --- | Try to convert a `TopBind` to a top-level binding, --- or `Nothing` if it isn't one. -bindOfTop - :: S.Top a S.Name - -> Maybe (Bind C.Name, C.Exp a C.Name) - -bindOfTop (S.TopBind _ b x) - = Just (toCoreB b, toCoreX x) -bindOfTop _ = Nothing - - --- ImportSource --------------------------------------------------------------- -toCoreImportSource :: ImportSource S.Name -> ImportSource C.Name -toCoreImportSource src - = case src of - ImportSourceAbstract t - -> ImportSourceAbstract (toCoreT t) - - ImportSourceModule mn n t - -> ImportSourceModule mn (toCoreN n) (toCoreT t) - - ImportSourceSea v t - -> ImportSourceSea v (toCoreT t) - - --- Type ----------------------------------------------------------------------- -toCoreT :: Type S.Name -> Type C.Name -toCoreT tt - = case tt of - TVar u -> TVar (toCoreU u) - TCon tc -> TCon (toCoreTC tc) - TForall b t -> TForall (toCoreB b) (toCoreT t) - TApp t1 t2 -> TApp (toCoreT t1) (toCoreT t2) - TSum ts -> TSum $ Sum.fromList (toCoreT (Sum.kindOfSum ts)) - $ map toCoreT - $ Sum.toList ts - - --- TyCon ---------------------------------------------------------------------- -toCoreTC :: TyCon S.Name -> TyCon C.Name -toCoreTC tc - = case tc of - TyConSort sc -> TyConSort sc - TyConKind kc -> TyConKind kc - TyConWitness wc -> TyConWitness wc - TyConSpec sc -> TyConSpec sc - TyConBound u k -> TyConBound (toCoreU u) (toCoreT k) - TyConExists n k -> TyConExists n (toCoreT k) - - --- DataDef -------------------------------------------------------------------- -toCoreDataDef :: S.DataDef S.Name -> C.DataDef C.Name -toCoreDataDef def - = C.DataDef - { C.dataDefTypeName - = toCoreN $ S.dataDefTypeName def - - , C.dataDefParams - = map toCoreB $ S.dataDefParams def - - , C.dataDefCtors - = Just - $ [ toCoreDataCtor def tag ctor - | ctor <- S.dataDefCtors def - | tag <- [0..] ] - - , C.dataDefIsAlgebraic - = True - } - - --- DataCtor ------------------------------------------------------------------- -toCoreDataCtor - :: S.DataDef S.Name - -> Integer - -> S.DataCtor S.Name - -> C.DataCtor C.Name - -toCoreDataCtor dataDef tag ctor - = C.DataCtor - { C.dataCtorName = toCoreN (S.dataCtorName ctor) - , C.dataCtorTag = tag - , C.dataCtorFieldTypes = map toCoreT (S.dataCtorFieldTypes ctor) - , C.dataCtorResultType = toCoreT (S.dataCtorResultType ctor) - , C.dataCtorTypeName = toCoreN (S.dataDefTypeName dataDef) - , C.dataCtorTypeParams = map toCoreB (S.dataDefParams dataDef) } - - --- Exp ------------------------------------------------------------------------ -toCoreX :: S.Exp a S.Name -> C.Exp a C.Name -toCoreX xx - = case xx of - S.XVar a u -> C.XVar a (toCoreU u) - S.XCon a dc -> C.XCon a (toCoreDC dc) - S.XLAM a b x -> C.XLAM a (toCoreB b) (toCoreX x) - S.XLam a b x -> C.XLam a (toCoreB b) (toCoreX x) - S.XApp a x1 x2 -> C.XApp a (toCoreX x1) (toCoreX x2) - S.XLet a lts x -> C.XLet a (toCoreLts lts) (toCoreX x) - S.XCase a x alts -> C.XCase a (toCoreX x) (map toCoreA alts) - S.XCast a c x -> C.XCast a (toCoreC c) (toCoreX x) - S.XType a t -> C.XType a (toCoreT t) - S.XWitness a w -> C.XWitness a (toCoreW w) - - -- These shouldn't exist in the desugared source tetra code. - S.XDefix{} -> error "source-tetra.toCoreX: found XDefix node" - S.XInfixOp{} -> error "source-tetra.toCoreX: found XInfixOp node" - S.XInfixVar{} -> error "source-tetra.toCoreX: found XInfixVar node" - - --- Lets ----------------------------------------------------------------------- -toCoreLts :: S.Lets a S.Name -> C.Lets a C.Name -toCoreLts lts - = case lts of - S.LLet b x - -> C.LLet (toCoreB b) (toCoreX x) - - S.LRec bxs - -> C.LRec [(toCoreB b, toCoreX x) | (b, x) <- bxs ] - - S.LPrivate bks Nothing bts - -> C.LPrivate (map toCoreB bks) Nothing (map toCoreB bts) - - S.LPrivate bks (Just tParent) bts - -> C.LPrivate (map toCoreB bks) - (Just $ toCoreT tParent) (map toCoreB bts) - - - --- Cast ----------------------------------------------------------------------- -toCoreC :: S.Cast a S.Name -> C.Cast a C.Name -toCoreC cc - = case cc of - S.CastWeakenEffect eff -> C.CastWeakenEffect (toCoreT eff) - S.CastPurify w -> C.CastPurify (toCoreW w) - S.CastBox -> C.CastBox - S.CastRun -> C.CastRun - - --- Alt ------------------------------------------------------------------------ -toCoreA :: S.Alt a S.Name -> C.Alt a C.Name -toCoreA aa - = case aa of - S.AAlt w x -> C.AAlt (toCoreP w) (toCoreX x) - - --- Pat ------------------------------------------------------------------------ -toCoreP :: Pat S.Name -> Pat C.Name -toCoreP pp - = case pp of - PDefault -> PDefault - PData dc bs -> PData (toCoreDC dc) (map toCoreB bs) - - --- DaCon ---------------------------------------------------------------------- -toCoreDC :: DaCon S.Name -> DaCon C.Name -toCoreDC dc - = case dc of - DaConUnit - -> DaConUnit - - DaConPrim n t - -> DaConPrim - { daConName = toCoreN n - , daConType = toCoreT t } - - DaConBound n - -> DaConBound (toCoreN n) - - - --- Witness -------------------------------------------------------------------- -toCoreW :: Witness a S.Name -> Witness a C.Name -toCoreW ww - = case ww of - S.WVar a u -> C.WVar a (toCoreU u) - S.WCon a wc -> C.WCon a (toCoreWC wc) - S.WApp a w1 w2 -> C.WApp a (toCoreW w1) (toCoreW w2) - S.WJoin a w1 w2 -> C.WJoin a (toCoreW w1) (toCoreW w2) - S.WType a t -> C.WType a (toCoreT t) - - --- WiCon ---------------------------------------------------------------------- -toCoreWC :: WiCon S.Name -> WiCon C.Name -toCoreWC wc - = case wc of - WiConBuiltin wb -> WiConBuiltin wb - WiConBound u t -> WiConBound (toCoreU u) (toCoreT t) - - --- Bind ----------------------------------------------------------------------- -toCoreB :: Bind S.Name -> Bind C.Name -toCoreB bb - = case bb of - BName n t -> BName (toCoreN n) (toCoreT t) - BAnon t -> BAnon (toCoreT t) - BNone t -> BNone (toCoreT t) - - --- Bound ---------------------------------------------------------------------- -toCoreU :: Bound S.Name -> Bound C.Name -toCoreU uu - = case uu of - UName n -> UName (toCoreN n) - UIx i -> UIx i - UPrim n t -> UPrim (toCoreN n) (toCoreT t) - - --- Name ----------------------------------------------------------------------- -toCoreN :: S.Name -> C.Name -toCoreN nn - = case nn of - S.NameVar str -> C.NameVar str - S.NameCon str -> C.NameCon str - S.NameTyConTetra tc -> C.NameTyConTetra (toCoreTyConTetra tc) - S.NameOpStore tc -> C.NameOpStore tc - S.NamePrimTyCon p -> C.NamePrimTyCon p - S.NamePrimArith p -> C.NamePrimArith p - S.NameLitBool b -> C.NameLitBool b - S.NameLitNat n -> C.NameLitNat n - S.NameLitInt i -> C.NameLitInt i - S.NameLitWord w b -> C.NameLitWord w b - S.NameHole -> C.NameHole - - -toCoreTyConTetra :: S.TyConTetra -> C.TyConTetra -toCoreTyConTetra tc - = case tc of - S.TyConTetraRef -> C.TyConTetraRef - S.TyConTetraTuple n -> C.TyConTetraTuple n - diff --git a/DDC/Source/Tetra/Transform/BoundX.hs b/DDC/Source/Tetra/Transform/BoundX.hs new file mode 100644 --- /dev/null +++ b/DDC/Source/Tetra/Transform/BoundX.hs @@ -0,0 +1,215 @@ +{-# LANGUAGE TypeFamilies #-} +-- | Lifting and lowering level-0 deBruijn indices in source expressions. +-- +-- Level-0 indices are used for both value and witness variables. +-- +module DDC.Source.Tetra.Transform.BoundX + ( liftX, liftAtDepthX +-- , lowerX, lowerAtDepthX + , MapBoundX (..) + , HasAnonBind (..)) +where +import DDC.Source.Tetra.Exp.Generic +import DDC.Type.Exp + +--------------------------------------------------------------------------------------------------- +class HasAnonBind l => MapBoundX (c :: * -> *) l where + mapBoundAtDepthX + :: l -- Proxy for language index, not inspected. + -> (Int -> GBound l -> GBound l) -- Function to apply to current bound occ. + -> Int -- Current binding depth. + -> c l -- Map across bounds in this thing. + -> c l -- Result thing. + + +-- Lift ------------------------------------------------------------------------------------------- +-- | Lift debruijn indices less than or equal to the given depth. +liftAtDepthX + :: (MapBoundX c l, GBound l ~ Bound n) + => l + -> Int -- ^ Number of levels to lift. + -> Int -- ^ Current binding depth. + -> c l -- ^ Lift expression indices in this thing. + -> c l + +liftAtDepthX l n d + = mapBoundAtDepthX l liftU d + where + liftU d' u + = case u of + UName{} -> u + UPrim{} -> u + UIx i + | d' <= i -> UIx (i + n) + | otherwise -> u + + +-- | Wrapper for `liftAtDepthX` that starts at depth 0. +liftX :: (MapBoundX c l, GBound l ~ Bound n) + => Int -> c l -> c l + +liftX n xx + = let lProxy :: l + lProxy = error "ddc-source-tetra.lProxy" + in liftAtDepthX lProxy n 0 xx + + +--------------------------------------------------------------------------------------------------- +instance HasAnonBind l => MapBoundX GExp l where + mapBoundAtDepthX = downX + +downX l f d xx + = case xx of + XVar a u -> XVar a (f d u) + XCon{} -> xx + XPrim{} -> xx + XApp a x1 x2 -> XApp a (downX l f d x1) (downX l f d x2) + XLAM a b x -> XLAM a b (downX l f d x) + + XLam a b x + -> let d' = d + countBAnons l [b] + in XLam a b (mapBoundAtDepthX l f d' x) + + XLet a lets x + -> let (lets', levels) = mapBoundAtDepthXLets l f d lets + in XLet a lets' (mapBoundAtDepthX l f (d + levels) x) + + XCase a x alts -> XCase a (downX l f d x) (map (downA l f d) alts) + XCast a cc x -> XCast a (downC l f d cc) (downX l f d x) + XType{} -> xx + XWitness a w -> XWitness a (downW l f d w) + + XDefix a xs -> XDefix a (map (downX l f d) xs) + XInfixOp{} -> xx + XInfixVar{} -> xx + + +--------------------------------------------------------------------------------------------------- +instance HasAnonBind l => MapBoundX GClause l where + mapBoundAtDepthX = downCL + +downCL l f d cc + = case cc of + SSig{} -> cc + SLet a b p gs -> SLet a b p (map (downGX l f d) gs) + + +--------------------------------------------------------------------------------------------------- +instance HasAnonBind l => MapBoundX GAlt l where + mapBoundAtDepthX = downA + +downA l f d (AAlt p gxs) + = case p of + PDefault + -> AAlt PDefault (map (downGX l f d) gxs) + + PData _ bs + -> let d' = d + countBAnons l bs + in AAlt p (map (downGX l f d') gxs) + + +--------------------------------------------------------------------------------------------------- +instance HasAnonBind l => MapBoundX GGuardedExp l where + mapBoundAtDepthX = downGX + +downGX l f d gx + = case gx of + GGuard g gxs + -> let d' = d + countBAnonsG l g + in GGuard (downG l f d g) (downGX l f d' gxs) + + GExp x + -> GExp (downX l f d x) + + +--------------------------------------------------------------------------------------------------- +instance HasAnonBind l => MapBoundX GGuard l where + mapBoundAtDepthX = downG + +downG l f d g + = case g of + GPat p x -> GPat p (downX l f d x) + GPred x -> GPred (downX l f d x) + GDefault -> GDefault + + +--------------------------------------------------------------------------------------------------- +instance HasAnonBind l => MapBoundX GCast l where + mapBoundAtDepthX = downC + +downC _l _f _d cc + = case cc of + CastWeakenEffect{} -> cc + CastPurify w -> CastPurify w + CastBox -> CastBox + CastRun -> CastRun + +--------------------------------------------------------------------------------------------------- +instance HasAnonBind l => MapBoundX GWitness l where + mapBoundAtDepthX = downW + +downW l f d ww + = case ww of + WVar a u -> WVar a (f d u) + WCon{} -> ww + WApp a w1 w2 -> WApp a (downW l f d w1) (downW l f d w2) + WType{} -> ww + + +--------------------------------------------------------------------------------------------------- +mapBoundAtDepthXLets + :: forall l + . HasAnonBind l + => l + -> (Int -> GBound l -> GBound l) + -- ^ Function given number of levels to lift. + -> Int -- ^ Current binding depth. + -> GLets l -- ^ Lift exp indices in this thing. + -> (GLets l, Int) -- ^ Lifted, and how much to increase depth by + +mapBoundAtDepthXLets l f d lts + = case lts of + LLet b x + -> let inc = countBAnons l [b] + x' = mapBoundAtDepthX l f d x + in (LLet b x', inc) + + LRec bs + -> let inc = countBAnons l (map fst bs) + bs' = map (\(b,e) -> (b, mapBoundAtDepthX l f (d + inc) e)) bs + in (LRec bs', inc) + + LPrivate _b _ bs + -> (lts, countBAnons l bs) + + LGroup cs + -> let inc = sum (map (countBAnonsC l) cs) + cs' = map (mapBoundAtDepthX l f (d + inc)) cs + in (LGroup cs', inc) + + +--------------------------------------------------------------------------------------------------- +countBAnons :: HasAnonBind l => l -> [GBind l] -> Int +countBAnons l = length . filter (isAnon l) + + +countBAnonsC :: HasAnonBind l => l -> GClause l -> Int +countBAnonsC l c + = case c of + SSig _ b _ -> countBAnons l [b] + SLet _ b _ _ -> countBAnons l [b] + + +countBAnonsG :: HasAnonBind l => l -> GGuard l -> Int +countBAnonsG l g + = case g of + GPat p _ -> countBAnonsP l p + GPred _ -> 0 + GDefault -> 0 + +countBAnonsP :: HasAnonBind l => l -> GPat l -> Int +countBAnonsP l p + = case p of + PData _ bs -> countBAnons l bs + PDefault -> 0 + diff --git a/DDC/Source/Tetra/Transform/Defix.hs b/DDC/Source/Tetra/Transform/Defix.hs --- a/DDC/Source/Tetra/Transform/Defix.hs +++ b/DDC/Source/Tetra/Transform/Defix.hs @@ -1,4 +1,21 @@ +-- | Convert infix expressions to prefix form. +-- +-- The parser packs up sequences of expressions and operators into an +-- XDefix node, but does not convert them to standard prefix applications. +-- That is the job of this module. +-- +-- The parsed code will contain XDefix, XInfixOp and XInfixVar nodes, +-- which are pretty-printed like this: +-- +-- @ [DEFIX| Cons start [DEFIX| enumFromTo [DEFIX| start (INFIXOP "+") 1 ] end ] +-- @ +-- +-- After applying the transform in this module, all function applications +-- will be in prefix form: +-- +-- @ Cons start (enumFromTo ((+) start 1) end)@ +-- module DDC.Source.Tetra.Transform.Defix ( FixTable (..) , FixDef (..) @@ -19,32 +36,33 @@ -- Defix ---------------------------------------------------------------------- -class Defix (c :: * -> * -> *) where +class Defix (c :: * -> *) l where -- | Resolve infix expressions in a thing. - defix :: FixTable a n - -> c a n - -> Either (Error a n) (c a n) + defix :: FixTable l + -> c l + -> Either (Error l) (c l) -instance Defix Module where +instance Defix Module l where defix table mm = do tops' <- mapM (defix table) (moduleTops mm) return $ mm { moduleTops = tops' } -instance Defix Top where +instance Defix Top l where defix table tt = case tt of - TopBind a b x -> liftM (TopBind a b) (defix table x) + TopClause a c -> liftM (TopClause a) (defix table c) _ -> return tt -instance Defix Exp where +instance Defix GExp l where defix table xx = let down = defix table in case xx of XVar{} -> return xx XCon{} -> return xx + XPrim{} -> return xx XLAM a b x -> liftM (XLAM a b) (down x) XLam a b x -> liftM (XLam a b) (down x) XApp a x1 x2 -> liftM2 (XApp a) (down x1) (down x2) @@ -67,7 +85,7 @@ Nothing -> Left $ ErrorNoInfixDef a str -instance Defix Lets where +instance Defix GLets l where defix table lts = let down = defix table in case lts of @@ -80,14 +98,41 @@ LPrivate{} -> return lts + LGroup cs -> liftM LGroup (mapM down cs) -instance Defix Alt where + +instance Defix GClause l where + defix table cc + = let down = defix table + in case cc of + SSig{} -> return cc + SLet a b ps gs -> liftM (SLet a b ps) (mapM down gs) + + +instance Defix GAlt l where defix table aa = let down = defix table in case aa of - AAlt p x -> liftM (AAlt p) (down x) + AAlt p x -> liftM (AAlt p) (mapM down x) +instance Defix GGuardedExp l where + defix table gg + = let down = defix table + in case gg of + GGuard g x -> liftM2 GGuard (down g) (down x) + GExp x -> liftM GExp (down x) + + +instance Defix GGuard l where + defix table gg + = let down = defix table + in case gg of + GPat p x -> liftM (GPat p) (down x) + GPred x -> liftM GPred (down x) + GDefault -> return GDefault + + ------------------------------------------------------------------------------- -- | Preprocess the body of an XDefix node to insert applications. -- @@ -95,10 +140,10 @@ -- and produces (f a) + (g b) with three nodes in the XDefix list. -- defixApps - :: a - -> FixTable a n - -> [Exp a n] - -> Either (Error a n) [Exp a n] + :: GAnnot l + -> FixTable l + -> [GExp l] + -> Either (Error l) [GExp l] defixApps a table xx = start xx @@ -148,10 +193,10 @@ -- The input needs to have already been preprocessed by defixApps above. -- defixExps - :: a -- ^ Annotation from original XDefix node. - -> FixTable a n -- ^ Table of infix defs. - -> [Exp a n] -- ^ Body of the XDefix node. - -> Either (Error a n) (Exp a n) + :: GAnnot l -- ^ Annotation from original XDefix node. + -> FixTable l -- ^ Table of infix defs. + -> [GExp l] -- ^ Body of the XDefix node. + -> Either (Error l) (GExp l) defixExps a table xx = case xx of @@ -178,10 +223,10 @@ -- | Try to defix a sequence of expressions and XInfixOp nodes. defixInfix - :: a -- ^ Annotation from original XDefix node. - -> FixTable a n -- ^ Table of infix defs. - -> [Exp a n] -- ^ Body of the XDefix node. - -> Either (Error a n) (Maybe [Exp a n]) + :: GAnnot l -- ^ Annotation from original XDefix node. + -> FixTable l -- ^ Table of infix defs. + -> [GExp l] -- ^ Body of the XDefix node. + -> Either (Error l) (Maybe [GExp l]) defixInfix a table xs -- Get the list of infix ops in the expression. @@ -214,6 +259,9 @@ defsHigh <- mapM (getInfixDefOfSymbol sp table) opsHigh let assocsHigh = map fixDefAssoc defsHigh + -- All operators at the current precedence level must have the + -- same associativity, otherwise the implied order-of-operations is + -- ambiguous. case nub assocsHigh of [InfixLeft] -> do xs' <- defixInfixLeft sp table precHigh xs @@ -232,8 +280,8 @@ -- | Defix some left associative ops. defixInfixLeft - :: a -> FixTable a n -> Int - -> [Exp a n] -> Either (Error a n) [Exp a n] + :: GAnnot l -> FixTable l -> Int + -> [GExp l] -> Either (Error l) [GExp l] defixInfixLeft sp table precHigh (x1 : XInfixOp spo op : x2 : xs) | Just def <- lookupDefInfixOfSymbol table op @@ -252,8 +300,8 @@ -- The input expression list is reversed, so we can eat the operators left -- to right. However, be careful to build the App node the right way around. defixInfixRight - :: a -> FixTable a n -> Int - -> [Exp a n] -> Either (Error a n) [Exp a n] + :: GAnnot l -> FixTable l -> Int + -> [GExp l] -> Either (Error l) [GExp l] defixInfixRight sp table precHigh (x2 : XInfixOp spo op : x1 : xs) | Just def <- lookupDefInfixOfSymbol table op @@ -270,8 +318,8 @@ -- | Defix non-associative ops. defixInfixNone - :: a -> FixTable a n -> Int - -> [Exp a n] -> Either (Error a n) [Exp a n] + :: GAnnot l -> FixTable l -> Int + -> [GExp l] -> Either (Error l) [GExp l] defixInfixNone sp table precHigh xx -- If there are two ops in a row that are non-associative and have diff --git a/DDC/Source/Tetra/Transform/Defix/Error.hs b/DDC/Source/Tetra/Transform/Defix/Error.hs --- a/DDC/Source/Tetra/Transform/Defix/Error.hs +++ b/DDC/Source/Tetra/Transform/Defix/Error.hs @@ -1,64 +1,67 @@ +{-# LANGUAGE TypeFamilies, UndecidableInstances #-} +-- | Things that can go wrong when resolving infix expressions. module DDC.Source.Tetra.Transform.Defix.Error (Error (..)) where -import DDC.Source.Tetra.Exp -import DDC.Base.Pretty -import qualified DDC.Data.SourcePos as BP +import DDC.Source.Tetra.Exp.Generic +import DDC.Source.Tetra.Pretty -- | Things that can go wrong when defixing code. -data Error a n +data Error l -- | Infix operator symbol has no infix definition. = ErrorNoInfixDef - { errorAnnot :: a + { errorAnnot :: GAnnot l , errorSymbol :: String } -- | Two non-associative operators with the same precedence. | ErrorDefixNonAssoc { errorOp1 :: String - , errorAnnot1 :: a + , errorAnnot1 :: GAnnot l , errorOp2 :: String - , errorAnnot2 :: a } + , errorAnnot2 :: GAnnot l } -- | Two operators of different associativies with same precedence. | ErrorDefixMixedAssoc - { errorAnnot :: a + { errorAnnot :: GAnnot l , errorOps :: [String] } -- | Infix expression is malformed. -- Eg "+ 3" or "2 + + 2" | ErrorMalformed - { errorAnnot :: a - , errorExp :: Exp a n } - deriving Show + { errorAnnot :: GAnnot l + , errorExp :: GExp l } +deriving instance ShowLanguage l => Show (Error l) --- Pretty --------------------------------------------------------------------- -instance (Pretty n) - => Pretty (Error BP.SourcePos n) where + +instance PrettyLanguage l => Pretty (Error l) where ppr err = case err of ErrorNoInfixDef{} -> vcat [ ppr $ errorAnnot err - , text "No infix definition for symbol: " <> ppr (errorSymbol err) ] + , text "No infix definition for symbol: " + <> ppr (errorSymbol err) ] ErrorDefixNonAssoc{} -> vcat [ ppr $ errorAnnot1 err , text "Ambiguous infix expression." - , text " Operator '" <> text (errorOp1 err) - <> text "' at " <> ppr (errorAnnot1 err) - <+> text "is non associative," + , text " Operator '" + <> text (errorOp1 err) + <> text "' at " <> ppr (errorAnnot1 err) + <+> text "is non associative," , text " but the same precedence as" - , text " operator '" <> text (errorOp2 err) - <> text "' at " <> ppr (errorAnnot2 err) - <> text "."] + , text " operator '" + <> text (errorOp2 err) + <> text "' at " <> ppr (errorAnnot2 err) + <> text "."] ErrorDefixMixedAssoc{} -> vcat [ ppr $ errorAnnot err , text "Ambiguous infix expression." , text " operators " <> hsep (map ppr (errorOps err)) - <> text "have different associativities but same precedence." ] + <> text "have different associativities but same precedence." ] ErrorMalformed{} -> vcat [ ppr $ errorAnnot err diff --git a/DDC/Source/Tetra/Transform/Defix/FixTable.hs b/DDC/Source/Tetra/Transform/Defix/FixTable.hs --- a/DDC/Source/Tetra/Transform/Defix/FixTable.hs +++ b/DDC/Source/Tetra/Transform/Defix/FixTable.hs @@ -1,4 +1,8 @@ - +{-# LANGUAGE TypeFamilies #-} +-- | Defines the table that tracks what precedence and associativity +-- infix operators have. The config for common operators is currently +-- hard-coded, rather than being configurable in the source language. +-- module DDC.Source.Tetra.Transform.Defix.FixTable ( FixTable (..) , FixDef (..) @@ -9,19 +13,19 @@ , defaultFixTable) where import DDC.Source.Tetra.Transform.Defix.Error +import DDC.Source.Tetra.Exp.Generic import DDC.Source.Tetra.Prim -import DDC.Source.Tetra.Exp import Data.List -import qualified DDC.Data.SourcePos as BP +import qualified DDC.Type.Exp as T -- | Table of infix operator definitions. -data FixTable a n - = FixTable [FixDef a n] +data FixTable l + = FixTable [FixDef l] -- | Infix operator definition. -data FixDef a n +data FixDef l -- A prefix operator = FixDefPrefix { -- String of the operator @@ -29,7 +33,7 @@ -- Expression to rewrite the operator to, -- given the annotation of the original symbol. - , fixDefExp :: a -> Exp a n } + , fixDefExp :: GAnnot l -> GExp l } -- An infix operator. | FixDefInfix @@ -38,7 +42,7 @@ -- Expression to rewrite the operator to, -- given the annotation of the original symbol. - , fixDefExp :: a -> Exp a n + , fixDefExp :: GAnnot l -> GExp l -- Associativity of infix operator. , fixDefAssoc :: InfixAssoc @@ -47,7 +51,6 @@ , fixDefPrec :: Int } - -- | Infix associativity. data InfixAssoc -- | Left associative. @@ -68,7 +71,7 @@ -- | Lookup the `FixDefInfix` corresponding to a symbol name, if any. -lookupDefInfixOfSymbol :: FixTable a n -> String -> Maybe (FixDef a n) +lookupDefInfixOfSymbol :: FixTable l -> String -> Maybe (FixDef l) lookupDefInfixOfSymbol (FixTable defs) str = find (\def -> case def of FixDefInfix{} -> fixDefSymbol def == str @@ -77,7 +80,7 @@ -- | Lookup the `FixDefPrefix` corresponding to a symbol name, if any. -lookupDefPrefixOfSymbol :: FixTable a n -> String -> Maybe (FixDef a n) +lookupDefPrefixOfSymbol :: FixTable l -> String -> Maybe (FixDef l) lookupDefPrefixOfSymbol (FixTable defs) str = find (\def -> case def of FixDefPrefix{} -> fixDefSymbol def == str @@ -87,10 +90,10 @@ -- | Get the precedence of an infix symbol, else Error. getInfixDefOfSymbol - :: a - -> FixTable a n + :: GAnnot l + -> FixTable l -> String - -> Either (Error a n) (FixDef a n) + -> Either (Error l) (FixDef l) getInfixDefOfSymbol a table str = case lookupDefInfixOfSymbol table str of @@ -99,17 +102,46 @@ -- | Default fixity table for infix operators. -defaultFixTable :: FixTable BP.SourcePos Name +defaultFixTable :: GBound l ~ T.Bound Name => FixTable l defaultFixTable = FixTable - [ FixDefPrefix "-" (\sp -> XVar sp (UName (NameVar "neg"))) - , FixDefInfix "*" (\sp -> XVar sp (UName (NameVar "mul"))) InfixLeft 7 - , FixDefInfix "+" (\sp -> XVar sp (UName (NameVar "add"))) InfixLeft 6 - , FixDefInfix "-" (\sp -> XVar sp (UName (NameVar "sub"))) InfixLeft 6 - , FixDefInfix "==" (\sp -> XVar sp (UName (NameVar "eq" ))) InfixNone 5 - , FixDefInfix "/=" (\sp -> XVar sp (UName (NameVar "neq"))) InfixNone 5 - , FixDefInfix "<" (\sp -> XVar sp (UName (NameVar "lt" ))) InfixNone 5 - , FixDefInfix "<=" (\sp -> XVar sp (UName (NameVar "le" ))) InfixNone 5 - , FixDefInfix ">" (\sp -> XVar sp (UName (NameVar "gt" ))) InfixNone 5 - , FixDefInfix ">=" (\sp -> XVar sp (UName (NameVar "ge" ))) InfixNone 5 - , FixDefInfix "$" (\sp -> XVar sp (UName (NameVar "app"))) InfixRight 1 ] + [ FixDefPrefix "-" (xvar "neg") + , FixDefPrefix "¬" (xvar "not") + + -- Operators defined in the Haskell Prelude. + , FixDefInfix "∘" (xvar "compose") InfixRight 9 + + , FixDefInfix "*" (xvar "mul") InfixLeft 7 + + , FixDefInfix "+" (xvar "add") InfixLeft 6 + , FixDefInfix "-" (xvar "sub") InfixLeft 6 + + , FixDefInfix "∪" (xvar "intersect") InfixLeft 6 + , FixDefInfix "∩" (xvar "union") InfixLeft 6 + + , FixDefInfix "==" (xvar "eq") InfixNone 4 + , FixDefInfix "/=" (xvar "neq") InfixNone 4 + , FixDefInfix "<" (xvar "lt") InfixNone 4 + , FixDefInfix "<=" (xvar "le") InfixNone 4 + , FixDefInfix ">" (xvar "gt") InfixNone 4 + , FixDefInfix ">=" (xvar "ge") InfixNone 4 + + , FixDefInfix "/\\" (xvar "and") InfixRight 3 + , FixDefInfix "∧" (xvar "and") InfixRight 3 + + , FixDefInfix "\\/" (xvar "or") InfixRight 3 + , FixDefInfix "∨" (xvar "or") InfixRight 3 + + , FixDefInfix "$" (xvar "apply") InfixRight 1 + + -- String pasting. + -- These associate to the right so that when text objects are formed by + -- pasting several together, then spine of the data structure leans to + -- the right, as do cons lists. + , FixDefInfix "%" (xvar "paste") InfixRight 6 + , FixDefInfix "%%" (xvar "pastes") InfixRight 6 + ] + + where xvar str sp + = XVar sp (T.UName (NameVar str)) + diff --git a/DDC/Source/Tetra/Transform/Expand.hs b/DDC/Source/Tetra/Transform/Expand.hs --- a/DDC/Source/Tetra/Transform/Expand.hs +++ b/DDC/Source/Tetra/Transform/Expand.hs @@ -1,4 +1,26 @@ +{-# LANGUAGE TypeFamilies, UndecidableInstances #-} +-- | Look at type signatures and add quantifiers to bind any free type +-- variables. Also add holes for missing type arguments. +-- +-- Given +-- +-- @ +-- mapS (f : a -> S e b) (xx : List a) : S e (List b) +-- = box case xx of +-- Nil -> Nil +-- Cons x xs -> Cons (run f x) (run mapS f xs) +-- @ +-- +-- We get: +-- +-- @ +-- mapS [a e b : ?] (f : a -> S e b) (xx : List a) : S e (List b) +-- = /\(a e b : ?). box case xx of +-- Nil -> Nil +-- Cons x xs -> Cons (run f x) (run mapS [?] [?] [?] f xs) +-- @ +-- module DDC.Source.Tetra.Transform.Expand ( Config (..) , configDefault @@ -16,34 +38,42 @@ import qualified Data.Set as Set -------------------------------------------------------------------------------- +--------------------------------------------------------------------------------------------------- -- | Expander configuration. -data Config a n +data Config l = Config { -- | Make a type hole of the given kind. - configMakeTypeHole :: Kind n -> Type n } + configMakeTypeHole :: Kind (GName l) -> Type (GName l) } -- | Default expander configuration. -configDefault :: Config a Name +configDefault :: GName l ~ Name => Config l configDefault = Config { configMakeTypeHole = \k -> TVar (UPrim NameHole k)} -------------------------------------------------------------------------------- -class Expand (c :: * -> * -> *) where +--------------------------------------------------------------------------------------------------- +type ExpandLanguage l + = ( Ord (GName l) + , GBind l ~ Bind (GName l) + , GBound l ~ Bound (GName l)) + +class ExpandLanguage l => Expand (c :: * -> *) l where -- | Add quantifiers to the types of binders. Also add holes for missing -- type arguments. expand - :: Ord n - => Config a n - -> KindEnv n -> TypeEnv n - -> c a n -> c a n + :: Ord (GName l) + => Config l + -> KindEnv (GName l) -> TypeEnv (GName l) + -> c l -> c l -instance Expand Module where - expand config kenv tenv mm +--------------------------------------------------------------------------------------------------- +instance ExpandLanguage l => Expand Module l where + expand = expandM + +expandM config kenv tenv mm = let -- Add quantifiers to the types of bindings, and also slurp -- out the contribution to the top-level environment from each binding. @@ -51,13 +81,17 @@ -- thing is in-scope of all the others. preTop p = case p of - TopBind a b x + TopClause a (SLet _ b [] [GExp x]) -> let (b', x') = expandQuant a config kenv (b, x) - in (TopBind a b' x', Env.singleton b') + in ( TopClause a (SLet a b' [] [GExp x']) + , Env.singleton b') TopData _ def -> (p, typeEnvOfDataDef def) + -- Clauses should have already desugared. + _ -> error "source-tetra.expand: can't expand sugared TopClause." + (tops_quant, tenvs) = unzip $ map preTop $ moduleTops mm @@ -71,23 +105,30 @@ in mm { moduleTops = tops' } -instance Expand Top where - expand config kenv tenv top +--------------------------------------------------------------------------------------------------- +instance ExpandLanguage l => Expand Top l where + expand = expandT + +expandT config kenv tenv top = case top of - TopBind a b x + TopClause a1 (SLet a2 b [] [GExp x]) -> let tenv' = Env.extend b tenv x' = expand config kenv tenv' x - in TopBind a b x' + in TopClause a1 (SLet a2 b [] [GExp x']) - TopData{} - -> top + TopData{} -> top + -- Clauses should have already been desugared. + _ -> error "source-tetra.expand: can't expand sugared TopClause." -instance Expand Exp where - expand config kenv tenv xx - = let down = expand config kenv tenv - in case xx of +--------------------------------------------------------------------------------------------------- +instance ExpandLanguage l => Expand GExp l where + expand = downX + +downX config kenv tenv xx + = case xx of + -- Invoke the expander -------- XVar{} -> expandApp config kenv tenv xx [] @@ -95,6 +136,9 @@ XCon{} -> expandApp config kenv tenv xx [] + XPrim{} + -> expandApp config kenv tenv xx [] + XApp{} | (x1, xas) <- takeXAppsWithAnnots xx -> if isXVar x1 || isXCon x1 @@ -130,7 +174,17 @@ x2' = expand config kenv tenv' x2 in XLet a (LRec (zip bs_quant xs')) x2' + -- LGroups need to be desugared first because any quantifiers + -- we add to the front of a function binding need to scope over + -- all the clauses related to that binding. + XLet a (LGroup [SLet _ b [] [GExp x1]]) x2 + -> expand config kenv tenv (XLet a (LLet b x1) x2) + -- This should have already been desugared. + XLet _ (LGroup{}) _ + -> error $ "ddc-source-tetra.expand: can't expand sugared LGroup." + + -- Boilerplate ---------------- XLAM a b x -> let kenv' = Env.extend b kenv @@ -148,41 +202,95 @@ x2' = expand config kenv' tenv' x2 in XLet a (LPrivate bts mR bxs) x2' - XCase a x alts -> XCase a (down x) (map down alts) - XCast a c x -> XCast a c (down x) + XCase a x alts -> XCase a (downX config kenv tenv x) + (map (downA config kenv tenv) alts) + XCast a c x -> XCast a c (downX config kenv tenv x) XType{} -> xx XWitness{} -> xx - XDefix a xs -> XDefix a (map down xs) + XDefix a xs -> XDefix a (map (downX config kenv tenv) xs) XInfixOp{} -> xx XInfixVar{} -> xx -instance Expand Alt where - expand config kenv tenv alt +--------------------------------------------------------------------------------------------------- +instance ExpandLanguage l => Expand GAlt l where + expand = downA + +downA config kenv tenv alt = case alt of - AAlt PDefault x2 - -> let x2' = expand config kenv tenv x2 - in AAlt PDefault x2' + AAlt p gsx + -> let tenv' = extendPat p tenv + gsx' = map (expand config kenv tenv') gsx + in AAlt p gsx' - AAlt (PData dc bs) x2 - -> let tenv' = Env.extends bs tenv - x2' = expand config kenv tenv' x2 - in AAlt (PData dc bs) x2' +--------------------------------------------------------------------------------------------------- +instance ExpandLanguage l => Expand GGuardedExp l where + expand = downGX -------------------------------------------------------------------------------- +downGX config kenv tenv (GGuard g x) + = let g' = expand config kenv tenv g + tenv' = extendGuard g' tenv + in GGuard g' (expand config kenv tenv' x) + +downGX config kenv tenv (GExp x) + = let x' = expand config kenv tenv x + in GExp x' + + +--------------------------------------------------------------------------------------------------- +instance ExpandLanguage l => Expand GGuard l where + expand = downG + +downG config kenv tenv gg + = case gg of + GPat p x + -> let tenv' = extendPat p tenv + x' = expand config kenv tenv' x + in GPat p x' + + GPred x + -> let x' = expand config kenv tenv x + in GPred x' + + GDefault + -> GDefault + + +--------------------------------------------------------------------------------------------------- +-- | Extend a type environment with the variables bound by the given pattern. +extendPat + :: ExpandLanguage l + => GPat l -> TypeEnv (GName l) -> TypeEnv (GName l) +extendPat ww tenv + = case ww of + PDefault -> tenv + PData _ bs -> Env.extends bs tenv + + +-- | Extend a type environment with the variables bound by the given guard. +extendGuard + :: ExpandLanguage l + => GGuard l -> TypeEnv (GName l) -> TypeEnv (GName l) +extendGuard gg tenv + = case gg of + GPat w _ -> extendPat w tenv + _ -> tenv + + +--------------------------------------------------------------------------------------------------- -- | Expand missing quantifiers in types of bindings. -- -- If a binding mentions type variables that are not in scope then add new -- quantifiers to its type, as well as matching type lambdas. -- expandQuant - :: Ord n - => a -- ^ Annotation to use on new type lambdas. - -> Config a n -- ^ Expander configuration. - -> KindEnv n -- ^ Current kind environment. - -> (Bind n, Exp a n) -- ^ Binder and expression of binding. - -> (Bind n, Exp a n) + :: ExpandLanguage l + => GAnnot l -- ^ Annotation to use on new type lambdas. + -> Config l -- ^ Expander configuration. + -> KindEnv (GName l) -- ^ Current kind environment. + -> (GBind l, GExp l) -- ^ Binder and expression of binding. + -> (GBind l, GExp l) expandQuant a config kenv (b, x) | fvs <- freeVarsT kenv (typeOfBind b) @@ -213,7 +321,7 @@ = (b, x) -------------------------------------------------------------------------------- +--------------------------------------------------------------------------------------------------- -- | Expand missing type arguments in applications. -- -- The thing being applied needs to be a variable or data constructor @@ -222,13 +330,13 @@ -- the expression is missing them. -- expandApp - :: Ord n - => Config a n -- ^ Expander configuration. - -> KindEnv n -- ^ Current kind environment. - -> TypeEnv n -- ^ Current type environment. - -> Exp a n -- ^ Functional expression being applied. - -> [(Exp a n, a)] -- ^ Function arguments. - -> Exp a n + :: ExpandLanguage l + => Config l -- ^ Expander configuration. + -> KindEnv (GName l) -- ^ Current kind environment. + -> TypeEnv (GName l) -- ^ Current type environment. + -> GExp l -- ^ Functional expression being applied. + -> [(GExp l, GAnnot l)] -- ^ Function arguments. + -> GExp l expandApp config _kenv tenv x0 xas0 | Just (a, u) <- slurpVarConBound x0 @@ -259,7 +367,10 @@ -- | Slurp a `Bound` from and `XVar` or `XCon`. -- Named data constructors are converted to `UName`s. -slurpVarConBound :: Exp a n -> Maybe (a, Bound n) +slurpVarConBound + :: GBound l ~ Bound (GName l) + => GExp l + -> Maybe (GAnnot l, GBound l) slurpVarConBound xx = case xx of XVar a u -> Just (a, u) diff --git a/DDC/Source/Tetra/Transform/Guards.hs b/DDC/Source/Tetra/Transform/Guards.hs new file mode 100644 --- /dev/null +++ b/DDC/Source/Tetra/Transform/Guards.hs @@ -0,0 +1,68 @@ +{-# LANGUAGE TypeFamilies #-} + +-- | Desugaring Source Tetra guards to simple case-expressions. +module DDC.Source.Tetra.Transform.Guards + ( desugarGuards ) +where +import DDC.Source.Tetra.Transform.BoundX +import DDC.Source.Tetra.Compounds +import DDC.Source.Tetra.Exp.Annot +import DDC.Type.Exp + + +-- | Desugar some guards to a case-expression. +-- At runtime, if none of the guards match then run the provided fail action. +desugarGuards + :: forall a + . GAnnot (Annot a) -- ^ Annotation. + -> [GGuardedExp (Annot a)] -- ^ Guarded expressions to desugar. + -> GExp (Annot a) -- ^ Failure action. + -> GExp (Annot a) + +desugarGuards a gs0 fail0 + = go gs0 fail0 + where + -- Desugar list of guarded expressions. + go [] cont + = cont + + go [g] cont + = go1 g cont + + go (g : gs) cont + = go1 g (go gs cont) + + -- Desugar single guarded expression. + go1 (GExp x1) _ + = x1 + + go1 (GGuard GDefault gs) cont + = go1 gs cont + + -- Simple cases where we can avoid introducing the continuation. + go1 (GGuard (GPred g1) (GExp x1)) cont + = XCase a g1 + [ AAlt pTrue [GExp x1] + , AAlt PDefault [GExp cont] ] + + go1 (GGuard (GPat p1 g1) (GExp x1)) cont + = XCase a g1 + [ AAlt p1 [GExp x1] + , AAlt PDefault [GExp cont]] + + -- Cases that use a continuation function as a join point. + -- We need this when desugaring general pattern alternatives, + -- as each group of guards can be reached from multiple places. + go1 (GGuard (GPred x1) gs) cont + = XLet a (LLet (BAnon (tBot kData)) (xBox a cont)) + $ XCase a (liftX 1 x1) + [ AAlt pTrue [GExp (go1 (liftX 1 gs) (xRun a (XVar a (UIx 0))))] + , AAlt PDefault [GExp (xRun a (XVar a (UIx 0))) ]] + + go1 (GGuard (GPat p1 x1) gs) cont + = XLet a (LLet (BAnon (tBot kData)) (xBox a cont)) + $ XCase a (liftX 1 x1) + [ AAlt p1 [GExp (go1 (liftX 1 gs) (xRun a (XVar a (UIx 0))))] + , AAlt PDefault [GExp (xRun a (XVar a (UIx 0))) ]] + + diff --git a/ddc-source-tetra.cabal b/ddc-source-tetra.cabal --- a/ddc-source-tetra.cabal +++ b/ddc-source-tetra.cabal @@ -1,5 +1,5 @@ Name: ddc-source-tetra -Version: 0.4.1.3 +Version: 0.4.2.1 License: MIT License-file: LICENSE Author: The Disciplined Disciple Compiler Strike Force @@ -17,22 +17,29 @@ Library Build-Depends: - base >= 4.6 && < 4.8, - array >= 0.4 && < 0.6, - deepseq == 1.3.*, + base >= 4.6 && < 4.9, + array >= 0.4 && < 0.6, + deepseq >= 1.3 && < 1.5, containers == 0.5.*, + text >= 1.0 && < 1.3, transformers == 0.4.*, - mtl == 2.2.*, - ddc-base == 0.4.1.*, - ddc-core == 0.4.1.*, - ddc-core-salt == 0.4.1.*, - ddc-core-tetra == 0.4.1.* + mtl == 2.2.1.*, + ddc-base == 0.4.2.*, + ddc-core == 0.4.2.*, + ddc-core-salt == 0.4.2.*, + ddc-core-tetra == 0.4.2.* Exposed-modules: - DDC.Source.Tetra.Transform.Expand + DDC.Source.Tetra.Exp.Annot + DDC.Source.Tetra.Exp.Generic + + DDC.Source.Tetra.Transform.BoundX DDC.Source.Tetra.Transform.Defix - + DDC.Source.Tetra.Transform.Expand + DDC.Source.Tetra.Transform.Guards + DDC.Source.Tetra.Compounds + DDC.Source.Tetra.Convert DDC.Source.Tetra.DataDef DDC.Source.Tetra.Env DDC.Source.Tetra.Exp @@ -42,22 +49,26 @@ DDC.Source.Tetra.Predicates DDC.Source.Tetra.Pretty DDC.Source.Tetra.Prim - DDC.Source.Tetra.ToCore Other-modules: - DDC.Source.Tetra.Exp.Base - DDC.Source.Tetra.Lexer.Lit + DDC.Source.Tetra.Convert.Error + + DDC.Source.Tetra.Parser.Atom DDC.Source.Tetra.Parser.Exp DDC.Source.Tetra.Parser.Module DDC.Source.Tetra.Parser.Param + DDC.Source.Tetra.Parser.Witness + DDC.Source.Tetra.Prim.Base DDC.Source.Tetra.Prim.OpArith - DDC.Source.Tetra.Prim.OpStore + DDC.Source.Tetra.Prim.OpError + DDC.Source.Tetra.Prim.OpFun + DDC.Source.Tetra.Prim.OpVector DDC.Source.Tetra.Prim.TyConPrim DDC.Source.Tetra.Prim.TyConTetra + DDC.Source.Tetra.Transform.Defix.Error DDC.Source.Tetra.Transform.Defix.FixTable - GHC-options: -Wall @@ -67,13 +78,18 @@ -fno-warn-unused-do-bind Extensions: - KindSignatures NoMonomorphismRestriction + MultiParamTypeClasses ScopedTypeVariables - PatternGuards - FlexibleContexts + StandaloneDeriving FlexibleInstances - RankNTypes - BangPatterns + FlexibleContexts ParallelListComp - + ConstraintKinds + PatternSynonyms + EmptyDataDecls + KindSignatures + PatternGuards + BangPatterns + RankNTypes +