diff --git a/DDC/Source/Tetra/Compounds.hs b/DDC/Source/Tetra/Compounds.hs new file mode 100644 --- /dev/null +++ b/DDC/Source/Tetra/Compounds.hs @@ -0,0 +1,208 @@ + +module DDC.Source.Tetra.Compounds + ( module DDC.Type.Compounds + , takeAnnotOfExp + + -- * Lambdas + , xLAMs + , xLams + , makeXLamFlags + , takeXLAMs + , takeXLams + , takeXLamFlags + + -- * Applications + , xApps + , makeXAppsWithAnnots + , takeXApps + , takeXApps1 + , takeXAppsAsList + , takeXAppsWithAnnots + , takeXConApps + , takeXPrimApps + + -- * Data Constructors + , dcUnit + , takeNameOfDaCon + , takeTypeOfDaCon + + -- * Patterns + , bindsOfPat + + -- * Witnesses + , wApp + , wApps + , takeXWitness + , takeWAppsAsList + , takePrimWiConApps) +where +import DDC.Source.Tetra.Exp +import DDC.Type.Compounds +import DDC.Core.Compounds + ( dcUnit + , takeNameOfDaCon + , takeTypeOfDaCon + + , bindsOfPat + + , wApp + , wApps + , takeXWitness + , 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 xx + = case xx of + XVar a _ -> Just a + XCon a _ -> Just a + XLAM a _ _ -> Just a + XLam a _ _ -> Just a + XApp a _ _ -> Just a + XLet a _ _ -> Just a + XCase a _ _ -> Just a + XCast a _ _ -> Just a + XType{} -> Nothing + XWitness{} -> Nothing + XDefix a _ -> Just a + XInfixOp a _ -> Just a + XInfixVar a _ -> Just a + + +-- Lambdas --------------------------------------------------------------------- +-- | Make some nested type lambdas. +xLAMs :: a -> [Bind n] -> Exp a n -> Exp a n +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 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 xx + = let go bs (XLAM _ b x) = go (b:bs) x + go bs x = (reverse bs, x) + in case go [] xx of + ([], _) -> Nothing + (bs, body) -> Just (bs, body) + + +-- | 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 xx + = let go bs (XLam _ b x) = go (b:bs) x + go bs x = (reverse bs, x) + in case go [] xx of + ([], _) -> Nothing + (bs, body) -> Just (bs, body) + + +-- | 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 a fbs x + = foldr (\(f, b) x' + -> if f then XLAM a b x' + else XLam a b x') + x fbs + + +-- | 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 xx + = let go bs (XLAM _ b x) = go ((True, b):bs) x + go bs (XLam _ b x) = go ((False, b):bs) x + go bs x = (reverse bs, x) + in case go [] xx of + ([], _) -> Nothing + (bs, body) -> Just (bs, body) + + +-- Applications --------------------------------------------------------------- +-- | Build sequence of value applications. +xApps :: a -> Exp a n -> [Exp a n] -> Exp a n +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 f xas + = case xas of + [] -> f + (arg,a ) : as -> makeXAppsWithAnnots (XApp a f arg) as + + +-- | 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 xx + = case takeXAppsAsList xx of + (x1 : xsArgs) -> Just (x1, xsArgs) + _ -> Nothing + + +-- | 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 x1 x2 + = case takeXApps x1 of + Nothing -> (x1, [x2]) + Just (x11, x12s) -> (x11, x12s ++ [x2]) + + +-- | Flatten an application into the function parts and arguments, if any. +takeXAppsAsList :: Exp a n -> [Exp a n] +takeXAppsAsList xx + = case xx of + XApp _ x1 x2 -> takeXAppsAsList x1 ++ [x2] + _ -> [xx] + + +-- | 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 xx + = case xx of + XApp a f arg + -> let (f', args') = takeXAppsWithAnnots f + in (f', args' ++ [(arg,a)]) + + _ -> (xx, []) + + +-- | Flatten an application of a primop into the variable +-- and its arguments. +-- +-- Returns `Nothing` if the expression isn't a primop application. +takeXPrimApps :: Exp a n -> Maybe (n, [Exp a n]) +takeXPrimApps xx + = case takeXAppsAsList xx of + XVar _ (UPrim 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 xx + = case takeXAppsAsList xx of + XCon _ dc : xs -> Just (dc, xs) + _ -> Nothing diff --git a/DDC/Source/Tetra/DataDef.hs b/DDC/Source/Tetra/DataDef.hs new file mode 100644 --- /dev/null +++ b/DDC/Source/Tetra/DataDef.hs @@ -0,0 +1,68 @@ + +module DDC.Source.Tetra.DataDef + ( -- * Data Type Definition. + DataDef (..) + , typeEnvOfDataDef + + -- * Data Constructor Definition. + , DataCtor (..) + , typeOfDataCtor) +where +import DDC.Type.Compounds +import DDC.Type.Exp +import DDC.Type.Env (TypeEnv) +import qualified DDC.Type.Env as Env +import Control.DeepSeq + + +-- DataDef -------------------------------------------------------------------- +-- | Data type definitions. +data DataDef n + = DataDef + { -- | Data type name. + dataDefTypeName :: !n + + -- | Type parameters. + , dataDefParams :: [Bind n] + + -- | Parameters and return type of each constructor. + , dataDefCtors :: [DataCtor n] } + deriving Show + +instance NFData (DataDef n) + + +-- | Take the types of data constructors from a data type definition. +typeEnvOfDataDef :: Ord n => DataDef n -> TypeEnv n +typeEnvOfDataDef def + = Env.fromList + [BName (dataCtorName ctor) + (typeOfDataCtor def ctor) + | ctor <- dataDefCtors def ] + + +-- DataCtor ------------------------------------------------------------------- +-- | A data type constructor definition. +data DataCtor n + = DataCtor + { -- | Name of the data constructor. + dataCtorName :: !n + + -- | Types of each of the fields of the constructor. + , dataCtorFieldTypes :: ![Type n] + + -- | Result type of the constructor. + , dataCtorResultType :: !(Type n) } + deriving Show + + +instance NFData (DataCtor n) + + +-- | Get the type of a data constructor. +typeOfDataCtor :: DataDef n -> DataCtor n -> Type n +typeOfDataCtor def ctor + = foldr TForall + (foldr tFun (dataCtorResultType ctor) + (dataCtorFieldTypes ctor)) + (dataDefParams def) diff --git a/DDC/Source/Tetra/Env.hs b/DDC/Source/Tetra/Env.hs new file mode 100644 --- /dev/null +++ b/DDC/Source/Tetra/Env.hs @@ -0,0 +1,47 @@ + +module DDC.Source.Tetra.Env + ( primKindEnv + , primTypeEnv ) +where +import DDC.Source.Tetra.Prim +import DDC.Source.Tetra.Exp +import DDC.Type.Env (Env) +import qualified DDC.Type.Env as Env + + +-- Kinds ---------------------------------------------------------------------- +-- | Kind environment containing kinds of primitive data types. +primKindEnv :: Env Name +primKindEnv = Env.setPrimFun kindOfPrimName Env.empty + + +-- | Take the kind of a primitive name. +-- +-- Returns `Nothing` if the name isn't primitive. +-- +kindOfPrimName :: Name -> Maybe (Kind Name) +kindOfPrimName nn + = case nn of + NamePrimTyCon tc -> Just $ kindPrimTyCon tc + _ -> Nothing + + +-- Types ---------------------------------------------------------------------- +-- | Type environment containing types of primitive operators. +primTypeEnv :: Env Name +primTypeEnv = Env.setPrimFun typeOfPrimName Env.empty + + +-- | Take the type of a name, +-- or `Nothing` if this is not a value name. +typeOfPrimName :: Name -> Maybe (Type Name) +typeOfPrimName dc + = case dc of + NamePrimArith p -> Just $ typePrimArith p + + NameLitBool _ -> Just $ tBool + NameLitNat _ -> Just $ tNat + NameLitInt _ -> Just $ tInt + NameLitWord _ bits -> Just $ tWord bits + + _ -> Nothing diff --git a/DDC/Source/Tetra/Exp.hs b/DDC/Source/Tetra/Exp.hs new file mode 100644 --- /dev/null +++ b/DDC/Source/Tetra/Exp.hs @@ -0,0 +1,23 @@ + +module DDC.Source.Tetra.Exp + ( 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.Source.Tetra.Exp.Base diff --git a/DDC/Source/Tetra/Exp/Base.hs b/DDC/Source/Tetra/Exp/Base.hs new file mode 100644 --- /dev/null +++ b/DDC/Source/Tetra/Exp/Base.hs @@ -0,0 +1,168 @@ + +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/Lexer.hs b/DDC/Source/Tetra/Lexer.hs new file mode 100644 --- /dev/null +++ b/DDC/Source/Tetra/Lexer.hs @@ -0,0 +1,19 @@ + +module DDC.Source.Tetra.Lexer + (lexModuleString) +where +import DDC.Source.Tetra.Prim +import DDC.Core.Lexer +import DDC.Data.Token + + +-- | Lex a string to tokens, using primitive names. +-- +-- The first argument gives the starting source line number. +lexModuleString :: String -> Int -> String -> [Token (Tok Name)] +lexModuleString sourceName lineStart str + = map rn $ lexModuleWithOffside sourceName lineStart str + where rn (Token strTok sp) + = case renameTok readName strTok of + Just t' -> Token t' sp + Nothing -> Token (KJunk "lexical error") sp diff --git a/DDC/Source/Tetra/Lexer/Lit.hs b/DDC/Source/Tetra/Lexer/Lit.hs new file mode 100644 --- /dev/null +++ b/DDC/Source/Tetra/Lexer/Lit.hs @@ -0,0 +1,85 @@ + +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 new file mode 100644 --- /dev/null +++ b/DDC/Source/Tetra/Module.hs @@ -0,0 +1,99 @@ + +module DDC.Source.Tetra.Module + ( -- * Modules + Module (..) + , isMainModule + , ExportSource (..) + , ImportSource (..) + + -- * Module Names + , QualName (..) + , ModuleName (..) + , isMainModuleName + + -- * Top-level things + , Top (..) + + -- * Data type definitions + , DataDef (..)) +where +import DDC.Source.Tetra.Exp +import DDC.Source.Tetra.DataDef +import Control.DeepSeq + +import DDC.Core.Module + ( QualName (..) + , ModuleName (..) + , isMainModuleName + , ExportSource (..) + , ImportSource (..)) + + +-- Module --------------------------------------------------------------------- +data Module a n + = Module + { -- | Name of this module + moduleName :: !ModuleName + + -- Exports ---------------------------- + -- | Names of exported types (level-1). + , moduleExportTypes :: [n] + + -- | Names of exported values (level-0). + , moduleExportValues :: [n] + + -- Imports ---------------------------- + -- | Imported modules. + , moduleImportModules :: [ModuleName] + + -- | Kinds of imported foreign types. + , moduleImportTypes :: [(n, ImportSource n)] + + -- | Types of imported foreign values. + , moduleImportValues :: [(n, ImportSource n)] + + -- Local ------------------------------ + -- | Top-level things + , moduleTops :: [Top a n] } + deriving Show + + +instance (NFData a, NFData n) => NFData (Module a n) 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) + + +-- | Check if this is the `Main` module. +isMainModule :: Module a n -> Bool +isMainModule mm + = isMainModuleName + $ moduleName mm + + +-- Top Level Thing ------------------------------------------------------------ +data Top a n + -- | Top-level, possibly recursive binding. + = TopBind a (Bind n) (Exp a n) + + -- | Data type definition. + | TopData + { topAnnot :: a + , topDataDef :: DataDef n } + deriving Show + + +instance (NFData a, NFData n) => NFData (Top a n) 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 + diff --git a/DDC/Source/Tetra/Parser.hs b/DDC/Source/Tetra/Parser.hs new file mode 100644 --- /dev/null +++ b/DDC/Source/Tetra/Parser.hs @@ -0,0 +1,54 @@ + +module DDC.Source.Tetra.Parser + ( Parser + , Context (..) + + -- * Modules + , pModule + + -- * Expressions + , pExp + , pExpApp + , pExpAtom + + -- * Types + , pType + , pTypeApp + , pTypeAtom + + -- * Witnesses + , pWitness + , pWitnessApp + , pWitnessAtom + + -- * Constructors + , pCon + , pLit + + -- * Variables + , pBinder + , pIndex + , pVar + , pName + + -- * Raw Tokens + , pTok + , pTokAs) +where +import DDC.Source.Tetra.Parser.Exp +import DDC.Source.Tetra.Parser.Module + +import DDC.Core.Parser + ( Parser + , Context (..) + , pWitness + , pWitnessApp + , pWitnessAtom + , pVar + , pCon + , pName + , pBinder + , pIndex + , pLit + , pTok, pTokAs) + diff --git a/DDC/Source/Tetra/Parser/Exp.hs b/DDC/Source/Tetra/Parser/Exp.hs new file mode 100644 --- /dev/null +++ b/DDC/Source/Tetra/Parser/Exp.hs @@ -0,0 +1,531 @@ + +-- | Core language parser. +module DDC.Source.Tetra.Parser.Exp + ( pExp + , pExpApp + , pExpAtom, pExpAtomSP + , pLetsSP, pLetBinding + , pType + , pTypeApp + , pTypeAtom) +where +import DDC.Source.Tetra.Exp +import DDC.Source.Tetra.Parser.Param +import DDC.Source.Tetra.Compounds + +import DDC.Core.Parser + ( Parser + , Context(..) + , pBinder + , pWitness + , pWitnessAtom + , pType + , pTypeAtom + , pTypeApp + , pCon + , pConSP + , pLit + , pLitSP + , pIndexSP + , pOpSP + , pOpVarSP + , pVarSP + , 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 + + +-- Exp -------------------------------------------------------------------------------------------- +-- | Parse a core language expression. +pExp :: Ord n => Context -> Parser n (Exp SourcePos n) +pExp c + = P.choice + -- Level-0 lambda abstractions + -- \(x1 x2 ... : Type) (y1 y2 ... : Type) ... . Exp + [ do sp <- pTokSP KBackSlash + + bs <- liftM 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') + + 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 + + bs <- liftM 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') + + pTok KDot + xBody <- pExp c + return $ foldr (XLAM sp) xBody bs + + -- let expression + , do (lts, sp) <- pLetsSP c + pTok KIn + x2 <- pExp c + return $ XLet sp lts x2 + + -- Sugar for a let-expression. + -- do { Stmt;+ } + , do pTok KDo + pTok KBraceBra + xx <- pStmts c + pTok KBraceKet + return $ xx + + -- case Exp of { Alt;+ } + , do sp <- pTokSP KCase + x <- pExp c + pTok KOf + pTok KBraceBra + alts <- P.sepEndBy1 (pAlt c) (pTok KSemiColon) + pTok KBraceKet + return $ XCase sp x alts + + -- match Pat <- Exp else Exp in Exp + -- Sugar for a case-expression. + , do sp <- pTokSP KMatch + p <- pPat c + pTok KArrowDashLeft + x1 <- pExp c + pTok KElse + x2 <- pExp c + pTok KIn + x3 <- pExp c + return $ XCase sp x1 [AAlt p x3, AAlt PDefault x2] + + -- weakeff [Type] in Exp + , do sp <- pTokSP KWeakEff + pTok KSquareBra + t <- pType c + pTok KSquareKet + pTok KIn + x <- pExp c + return $ XCast sp (CastWeakenEffect t) x + + -- purify Witness in Exp + , do sp <- pTokSP KPurify + w <- pWitness c + pTok KIn + x <- pExp c + return $ XCast sp (CastPurify w) x + + -- box Exp + , do sp <- pTokSP KBox + x <- pExp c + return $ XCast sp CastBox x + + -- run Exp + , do sp <- pTokSP KRun + x <- pExp c + return $ XCast sp CastRun x + + -- APP + , do pExpApp c + ] + + "an expression" + + +-- Applications. +pExpApp :: Ord n => Context -> Parser n (Exp SourcePos n) +pExpApp c + = do xps <- liftM concat $ P.many1 (pArgSPs c) + let (xs, sps) = unzip xps + let sp1 : _ = sps + + case xs of + [x] -> return x + _ -> return $ XDefix sp1 xs + + "an expression or application" + + +-- Comp, Witness or Spec arguments. +pArgSPs :: Ord n => Context -> Parser n [(Exp SourcePos n, SourcePos)] +pArgSPs c + = P.choice + -- [Type] + [ do sp <- pTokSP KSquareBra + t <- pType c + pTok KSquareKet + return [(XType sp t, sp)] + + -- [: Type0 Type0 ... :] + , do sp <- pTokSP KSquareColonBra + ts <- P.many1 (pTypeAtom c) + pTok KSquareColonKet + return [(XType sp t, sp) | t <- ts] + + -- { Witness } + , do sp <- pTokSP KBraceBra + w <- pWitness c + pTok KBraceKet + return [(XWitness sp w, sp)] + + -- {: Witness0 Witness0 ... :} + , do sp <- pTokSP KBraceColonBra + ws <- P.many1 (pWitnessAtom c) + pTok KBraceColonKet + return [(XWitness sp w, sp) | w <- ws] + + -- Exp0 + , do (x, sp) <- pExpAtomSP c + return [(x, sp)] + ] + "a type, witness or expression argument" + + +-- | Parse a variable, constructor or parenthesised expression. +pExpAtom :: Ord n => Context -> Parser n (Exp SourcePos n) +pExpAtom c + = do (x, _) <- pExpAtomSP c + return x + + +-- | Parse a variable, constructor or parenthesised expression, +-- also returning source position. +pExpAtomSP + :: Ord n + => Context + -> Parser n (Exp SourcePos n, SourcePos) + +pExpAtomSP c + = P.choice + [ -- ( Exp2 ) + do sp <- pTokSP KRoundBra + t <- pExp c + pTok KRoundKet + return (t, sp) + + -- Infix operator used as a variable. + , do (str, sp) <- pOpVarSP + return (XInfixVar sp str, sp) + + -- Infix operator used nekkid. + , do (str, sp) <- pOpSP + return (XInfixOp sp str, sp) + + -- The unit data constructor. + , do sp <- pTokSP KDaConUnit + return (XCon sp dcUnit, sp) + + -- Named algebraic constructors. + , do (con, sp) <- pConSP + return (XCon sp (DaConBound con), sp) + + -- Literals. + -- We just fill-in the type with tBot for now, and leave it to + -- the spreader to attach the real type. + -- We also set the literal as being algebraic, which may not be + -- true (as for Floats). The spreader also needs to fix this. + , do (lit, sp) <- pLitSP + return (XCon sp (DaConPrim lit (T.tBot T.kData)), sp) + + -- Debruijn indices + , do (i, sp) <- pIndexSP + return (XVar sp (UIx i), sp) + + -- Variables + , do (var, sp) <- pVarSP + return (XVar sp (UName var), sp) + ] + + "a variable, constructor, or parenthesised type" + + +-- Alternatives ----------------------------------------------------------------------------------- +-- Case alternatives. +pAlt :: Ord n => Context -> Parser n (Alt SourcePos n) +pAlt c + = do p <- pPat c + pTok KArrowDash + x <- pExp c + return $ AAlt p x + + +-- Patterns. +pPat :: Ord n + => Context -> Parser n (Pat n) +pPat c + = P.choice + [ -- Wildcard + do pTok KUnderscore + return $ PDefault + + -- Lit + , do nLit <- pLit + return $ PData (DaConPrim nLit (T.tBot T.kData)) [] + + -- 'Unit' + , do pTok KDaConUnit + return $ PData dcUnit [] + + -- Con Bind Bind ... + , do nCon <- pCon + bs <- P.many (pBindPat c) + return $ PData (DaConBound nCon) bs] + + +-- 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 c + = P.choice + -- Plain binder. + [ do b <- pBinder + return $ T.makeBindFromBinder b (T.tBot T.kData) + + -- Binder with type, wrapped in parens. + , do pTok KRoundBra + b <- pBinder + pTok (KOp ":") + t <- pType c + pTok KRoundKet + return $ T.makeBindFromBinder b t + ] + + +-- Bindings --------------------------------------------------------------------------------------- +pLetsSP :: Ord n + => Context -> Parser n (Lets SourcePos n, SourcePos) +pLetsSP c + = P.choice + [ -- non-recursive let + do sp <- pTokSP KLet + (b1, x1) <- pLetBinding c + return (LLet b1 x1, sp) + + -- recursive let + , do sp <- pTokSP KLetRec + pTok KBraceBra + lets <- P.sepEndBy1 (pLetBinding c) (pTok KSemiColon) + pTok KBraceKet + return (LRec lets, sp) + + -- Private region binding. + -- private Binder+ (with { Binder : Type ... })? in Exp + , do sp <- pTokSP KPrivate + + -- new private region names. + brs <- P.manyTill pBinder + $ P.try $ P.lookAhead $ P.choice [pTok KIn, pTok KWith] + + let bs = map (flip T.makeBindFromBinder T.kRegion) brs + + -- Witness types. + r <- pLetWits c bs Nothing + return (r, sp) + + -- Extend an existing region. + -- extend Binder+ using Type (with { Binder : Type ...})? in Exp + , do sp <- pTokSP KExtend + + -- parent region + t <- pType c + pTok KUsing + + -- new private region names. + brs <- P.manyTill pBinder + $ P.try $ P.lookAhead + $ P.choice [pTok KUsing, pTok KWith, pTok KIn] + + let bs = map (flip T.makeBindFromBinder T.kRegion) brs + + -- witness types + r <- pLetWits c bs (Just t) + return (r, sp) + ] + + +pLetWits + :: Ord n + => Context + -> [Bind n] -> Maybe (Type n) + -> Parser n (Lets SourcePos n) + +pLetWits c bs mParent + = P.choice + [ do pTok KWith + pTok KBraceBra + wits <- P.sepBy (P.choice + [ -- Named witness binder. + do b <- pBinder + pTok (KOp ":") + t <- pTypeApp c + return $ T.makeBindFromBinder b t + + -- Ambient witness binding, used for capabilities. + , do t <- pTypeApp c + return $ BNone t + ]) + (pTok KSemiColon) + pTok KBraceKet + return (LPrivate bs mParent wits) + + , do return (LPrivate bs mParent []) + ] + + +-- | A binding for let expression. +pLetBinding + :: Ord n + => Context + -> Parser n ( Bind n + , Exp SourcePos n) +pLetBinding 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) + + + , 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 "=") + xBody <- pExp c + let t = T.tBot T.kData + return $ (T.makeBindFromBinder b t, xBody) + + + , do -- Binding using function syntax. + ps <- liftM concat + $ P.many (pBindParamSpec c) + + P.choice + [ do -- Function syntax with a return type. + -- 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 + + let x = expOfParams sp ps xBody + let t = funTypeOfParams c ps tBody + return (T.makeBindFromBinder b t, x) + + -- 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 + + let x = expOfParams sp ps xBody + let t = T.tBot T.kData + return (T.makeBindFromBinder b t, x) ] + ] + + +-- 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) + + +-- | Parse a single statement. +pStmt :: Ord n => Context -> Parser n (Stmt n) +pStmt c + = P.choice + [ -- Binder = Exp ; + -- We need the 'try' because a VARIABLE binders can also be parsed + -- as a function name in a non-binding statement. + -- + P.try $ + do br <- pBinder + sp <- pTokSP (KOp "=") + x1 <- pExp c + let t = T.tBot T.kData + let b = T.makeBindFromBinder br t + return $ StmtBind sp b x1 + + -- Pat <- Exp else Exp ; + -- Sugar for a case-expression. + -- We need the 'try' because the PAT can also be parsed + -- as a function name in a non-binding statement. + , P.try $ + do p <- pPat c + sp <- pTokSP KArrowDashLeft + x1 <- pExp c + pTok KElse + x2 <- pExp c + return $ StmtMatch sp p x1 x2 + + -- Exp + , do x <- pExp c + + -- This should always succeed because pExp doesn't + -- parse plain types or witnesses + let Just sp = takeAnnotOfExp x + + return $ StmtNone sp x + ] + + +-- | Parse some statements. +pStmts :: Ord n => Context -> Parser n (Exp SourcePos n) +pStmts c + = do stmts <- P.sepEndBy1 (pStmt c) (pTok KSemiColon) + case makeStmts stmts of + Nothing -> P.unexpected "do-block must end with a statement" + Just x -> return x + + +-- | Make an expression from some statements. +makeStmts :: [Stmt n] -> Maybe (Exp SourcePos n) +makeStmts ss + = case ss of + [StmtNone _ x] + -> Just x + + StmtNone sp x1 : rest + | Just x2 <- makeStmts rest + -> Just $ XLet sp (LLet (BNone (T.tBot T.kData)) x1) x2 + + StmtBind sp b x1 : rest + | Just x2 <- makeStmts rest + -> Just $ XLet sp (LLet b x1) x2 + + StmtMatch sp p x1 x2 : rest + | Just x3 <- makeStmts rest + -> Just $ XCase sp x1 + [ AAlt p x3 + , AAlt PDefault x2] + + _ -> Nothing + diff --git a/DDC/Source/Tetra/Parser/Module.hs b/DDC/Source/Tetra/Parser/Module.hs new file mode 100644 --- /dev/null +++ b/DDC/Source/Tetra/Parser/Module.hs @@ -0,0 +1,219 @@ + +module DDC.Source.Tetra.Parser.Module + ( -- * Modules + pModule + , pTypeSig + + -- * Top-level things + , pTop) +where +import DDC.Source.Tetra.Parser.Exp +import DDC.Source.Tetra.Compounds +import DDC.Source.Tetra.DataDef +import DDC.Source.Tetra.Module +import DDC.Source.Tetra.Exp +import DDC.Core.Lexer.Tokens +import DDC.Base.Pretty +import Control.Monad +import qualified DDC.Base.Parser as P + +import DDC.Core.Parser + ( Parser + , Context (..) + , pModuleName + , pName + , pVar + , pTok, pTokSP) + + +-- Module --------------------------------------------------------------------- +-- | Parse a source tetra module. +pModule :: (Ord n, Pretty n) + => Context + -> Parser n (Module P.SourcePos n) +pModule c + = do _sp <- pTokSP KModule + name <- pModuleName + + -- export { VAR;+ } + tExports + <- P.choice + [do pTok KExport + pTok KBraceBra + vars <- P.sepEndBy1 pVar (pTok KSemiColon) + pTok KBraceKet + return vars + + , return []] + + -- import { SIG;+ } + tImports + <- liftM concat $ P.many (pImportSpecs c) + + pTok KWhere + pTok KBraceBra + + -- TOP;+ + tops <- P.sepEndBy (pTop c) (pTok KSemiColon) + + pTok KBraceKet + + -- 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. + return $ Module + { moduleName = name + , moduleExportTypes = [] + , moduleExportValues = tExports + , moduleImportModules = [] + , moduleImportTypes = [(n, s) | ImportType 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 c + = do var <- pVar + pTokSP (KOp ":") + t <- pType c + return (var, t) + + +------------------------------------------------------------------------------- +-- | An imported foreign type or foreign value. +data ImportSpec n + = ImportType n (ImportSource n) + | ImportValue n (ImportSource n) + + +-- | Parse some import specs. +pImportSpecs + :: (Ord n, Pretty n) + => Context -> Parser n [ImportSpec n] + +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 + + sigs <- P.sepEndBy1 (pImportType c src) (pTok KSemiColon) + pTok KBraceKet + return sigs + + -- imports foreign X value (NAME :: TYPE)+ + , do pTok KValue + pTok KBraceBra + + sigs <- P.sepEndBy1 (pImportValue c src) (pTok KSemiColon) + pTok KBraceKet + return sigs + ] + + +-- | Parse a type import spec. +pImportType + :: (Ord n, Pretty n) + => Context -> String -> Parser n (ImportSpec n) +pImportType c src + | "abstract" <- src + = do n <- pName + pTokSP (KOp ":") + k <- pType c + return (ImportType n (ImportSourceAbstract k)) + + | otherwise + = P.unexpected "import mode for foreign type" + + +-- | Parse a value import spec. +pImportValue + :: (Ord n, Pretty n) + => Context -> String -> Parser n (ImportSpec n) +pImportValue c src + | "c" <- src + = do n <- pName + pTokSP (KOp ":") + k <- pType c + + -- ISSUE #327: Allow external symbol to be specified + -- with foreign C imports and exports. + let symbol = renderIndent (ppr n) + + return (ImportValue n (ImportSourceSea symbol k)) + + | otherwise + = P.unexpected "import mode for foreign value" + + +-- Top Level ----------------------------------------------------------------- +pTop :: Ord n + => Context -> Parser n (Top P.SourcePos n) +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 + + -- A data type declaration + , do pData c + ] + + +-- Data ----------------------------------------------------------------------- +-- | Parse a data type declaration. +pData :: Ord n + => Context -> Parser n (Top P.SourcePos n) + +pData c + = do sp <- pTokSP KData + n <- pName + ps <- liftM concat $ P.many (pDataParam c) + + P.choice + [ -- Data declaration with constructors that have explicit types. + do pTok KWhere + pTok KBraceBra + ctors <- P.sepEndBy1 (pDataCtor c) (pTok KSemiColon) + pTok KBraceKet + return $ TopData sp (DataDef n ps ctors) + + -- Data declaration with no data constructors. + , do return $ TopData sp (DataDef n ps []) + ] + + +-- | Parse a type parameter to a data type. +pDataParam :: Ord n => Context -> Parser n [Bind n] +pDataParam c + = do pTok KRoundBra + ns <- P.many1 pName + pTokSP (KOp ":") + k <- pType c + pTok KRoundKet + return [BName n k | n <- ns] + + +-- | Parse a data constructor declaration. +pDataCtor :: Ord n => Context -> Parser n (DataCtor n) +pDataCtor c + = do n <- pName + pTokSP (KOp ":") + t <- pType c + let (tsArg, tResult) + = takeTFunArgResult t + + return $ DataCtor + { dataCtorName = n + , dataCtorFieldTypes = tsArg + , dataCtorResultType = tResult } + diff --git a/DDC/Source/Tetra/Parser/Param.hs b/DDC/Source/Tetra/Parser/Param.hs new file mode 100644 --- /dev/null +++ b/DDC/Source/Tetra/Parser/Param.hs @@ -0,0 +1,33 @@ + +module DDC.Source.Tetra.Parser.Param + ( ParamSpec (..) + , funTypeOfParams + , pBindParamSpec + , expOfParams) +where +import DDC.Source.Tetra.Exp +import DDC.Core.Parser + ( ParamSpec(..) + , funTypeOfParams + , pBindParamSpec) + + +-- | Build the expression of a function from specifications of its parameters, +-- 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. + +expOfParams _ [] xBody = xBody +expOfParams a (p:ps) xBody + = case p of + ParamType b + -> XLAM a b $ expOfParams a ps xBody + + ParamWitness b + -> XLam a b $ expOfParams a ps xBody + + ParamValue b _ _ + -> XLam a b $ expOfParams a ps xBody diff --git a/DDC/Source/Tetra/Predicates.hs b/DDC/Source/Tetra/Predicates.hs new file mode 100644 --- /dev/null +++ b/DDC/Source/Tetra/Predicates.hs @@ -0,0 +1,130 @@ + +module DDC.Source.Tetra.Predicates + ( module DDC.Type.Predicates + + -- * Atoms + , isXVar, isXCon + , isAtomX, isAtomW + + -- * Lambdas + , isXLAM, isXLam + , isLambdaX + + -- * Applications + , isXApp + + -- * Let bindings + , isXLet + + -- * Types and Witnesses + , isXType + , isXWitness + + -- * Patterns + , isPDefault) +where +import DDC.Source.Tetra.Exp +import DDC.Type.Predicates + + +-- Atoms ---------------------------------------------------------------------- +-- | Check whether an expression is a variable. +isXVar :: Exp a n -> Bool +isXVar xx + = case xx of + XVar{} -> True + _ -> False + + +-- | Check whether an expression is a constructor. +isXCon :: Exp a n -> Bool +isXCon xx + = case xx of + XCon{} -> True + _ -> False + + +-- | Check whether an expression is a `XVar` or an `XCon`, +-- or some type or witness atom. +isAtomX :: Exp a n -> Bool +isAtomX xx + = case xx of + XVar{} -> True + XCon{} -> True + XType _ t -> isAtomT t + XWitness _ w -> isAtomW w + _ -> False + + +-- | Check whether a witness is a `WVar` or `WCon`. +isAtomW :: Witness a n -> Bool +isAtomW ww + = case ww of + WVar{} -> True + WCon{} -> True + _ -> False + + +-- Lambdas -------------------------------------------------------------------- +-- | Check whether an expression is a spec abstraction (level-1). +isXLAM :: Exp a n -> Bool +isXLAM xx + = case xx of + XLAM{} -> True + _ -> False + + +-- | Check whether an expression is a value or witness abstraction (level-0). +isXLam :: Exp a n -> Bool +isXLam xx + = case xx of + XLam{} -> True + _ -> False + + +-- | Check whether an expression is a spec, value, or witness abstraction. +isLambdaX :: Exp a n -> Bool +isLambdaX xx + = isXLAM xx || isXLam xx + + +-- Applications --------------------------------------------------------------- +-- | Check whether an expression is an `XApp`. +isXApp :: Exp a n -> Bool +isXApp xx + = case xx of + XApp{} -> True + _ -> False + + +-- Let Bindings --------------------------------------------------------------- +-- | Check whether an expression is a `XLet`. +isXLet :: Exp a n -> Bool +isXLet xx + = case xx of + XLet{} -> True + _ -> False + + +-- Type and Witness ----------------------------------------------------------- +-- | Check whether an expression is an `XType` +isXType :: Exp a n -> Bool +isXType xx + = case xx of + XType{} -> True + _ -> False + + +-- | Check whether an expression is an `XWitness` +isXWitness :: Exp a n -> Bool +isXWitness xx + = case xx of + XWitness{} -> True + _ -> False + + +-- Patterns ------------------------------------------------------------------- +-- | Check whether an alternative is a `PDefault`. +isPDefault :: Pat n -> Bool +isPDefault PDefault = True +isPDefault _ = False diff --git a/DDC/Source/Tetra/Pretty.hs b/DDC/Source/Tetra/Pretty.hs new file mode 100644 --- /dev/null +++ b/DDC/Source/Tetra/Pretty.hs @@ -0,0 +1,273 @@ + +-- | Pretty printing for Tetra modules and expressions. +module DDC.Source.Tetra.Pretty + ( module DDC.Core.Pretty + , module DDC.Base.Pretty ) +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 + + +-- Module ----------------------------------------------------------------------------------------- +instance (Pretty n, Eq n) => Pretty (Module a n) where + ppr Module + { moduleName = name + , moduleExportTypes = _exportedTypes + , moduleExportValues = _exportedValues + , moduleImportModules = _importedModules + , moduleImportTypes = importedTypes + , moduleImportValues = importedValues + , moduleTops = tops } + = text "module" + <+> ppr name + <> sImportedTypes + <> sImportedValues + <> (if null importedTypes && null importedValues + then space <> text "where" + else text "where") + <$$> (vcat $ map ppr tops) + + where sImportedTypes + | null importedTypes = empty + | otherwise + = line + <> (vcat $ map pprImportType importedTypes) + <> line + + sImportedValues + | null importedValues = empty + | otherwise + = (vcat $ map pprImportValue importedValues) + <> line + + +-- 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))) + + ppr (TopData _ (DataDef name params ctors)) + = hsep + ( [ text "data", ppr name] + ++ [parens $ ppr b | b <- params] + ++ [text "where" <+> lbrace]) + <$> indent 8 + (vcat [ ppr (dataCtorName ctor) + <+> text ":" + <+> (hsep $ punctuate (text " ->") + $ ( map (pprPrec 6) (dataCtorFieldTypes ctor) + ++ [ ppr (dataCtorResultType ctor)])) + <> semi + | ctor <- ctors ]) + <> line + <> rbrace + +-- Exp -------------------------------------------------------------------------------------------- +instance (Pretty n, Eq n) => Pretty (Exp a n) where + pprPrec d xx + = {-# SCC "ppr[Exp]" #-} + case xx of + XVar _ u -> ppr u + XCon _ dc -> ppr dc + + XLAM{} + -> let Just (bs, xBody) = takeXLAMs xx + groups = partitionBindsByType bs + in pprParen' (d > 1) + $ (cat $ map (pprBinderGroup (text "/\\")) groups) + <> (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) + <> breakWhen (not $ isSimpleX xBody) + <> ppr xBody + + XApp _ x1 x2 + -> pprParen' (d > 10) + $ pprPrec 10 x1 + <> nest 4 (breakWhen (not $ isSimpleX x2) + <> pprPrec 11 x2) + + XLet _ lts x + -> pprParen' (d > 2) + $ 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 + <> (vcat $ punctuate semi $ map ppr alts)) + <> line + <> rbrace + + XCast _ CastBox x + -> pprParen' (d > 2) + $ text "box" <$> ppr x + + XCast _ CastRun x + -> pprParen' (d > 2) + $ text "run" <+> ppr x + + XCast _ cc x + -> pprParen' (d > 2) + $ ppr cc <+> text "in" + <$> ppr x + + XType _ t -> text "[" <> ppr t <> text "]" + XWitness _ w -> text "<" <> ppr w <> text ">" + + XDefix _ xs + -> pprParen' (d > 2) + $ text "DEFIX" <+> hsep (map (pprPrec 11) xs) + + XInfixOp _ str + -> parens $ text "INFIXOP" <+> text "\"" <> text str <> text "\"" + + XInfixVar _ str + -> 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 + 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 + <> nest 2 ( breakWhen (not $ isSimpleX x) + <> text "=" <+> align (ppr x))) + LRec bxs + -> let pprLetRecBind (b, x) + = ppr (binderOfBind b) + <+> text ":" + <+> ppr (typeOfBind b) + <> nest 2 ( breakWhen (not $ isSimpleX x) + <> text "=" <+> align (ppr x)) + + in (nest 2 $ text "letrec" + <+> lbrace + <> ( line + <> (vcat $ punctuate (semi <> line) + $ map pprLetRecBind bxs))) + <$> rbrace + + LPrivate bs Nothing [] + -> text "private" + <+> (hcat $ punctuate space (map (ppr . binderOfBind) bs)) + + LPrivate bs Nothing bsWit + -> text "private" + <+> (hcat $ punctuate space (map (ppr . binderOfBind) bs)) + <+> text "with" + <+> braces (cat $ punctuate (text "; ") $ map ppr bsWit) + + LPrivate bs (Just parent) [] + -> text "extend" + <+> ppr parent + <+> text "using" + <+> (hcat $ punctuate space (map (ppr . binderOfBind) bs)) + + LPrivate bs (Just parent) bsWit + -> text "extend" + <+> ppr parent + <+> text "using" + <+> (hcat $ punctuate space (map (ppr . binderOfBind) bs)) + <+> text "with" + <+> braces (cat $ punctuate (text "; ") $ map ppr bsWit) + + +-- Binder ----------------------------------------------------------------------------------------- +pprBinder :: Pretty n => Binder n -> Doc +pprBinder bb + = case bb of + RName v -> ppr v + RAnon -> text "^" + RNone -> text "_" + + +-- | Print a group of binders with the same type. +pprBinderGroup + :: (Pretty n, Eq n) + => Doc -> ([Binder n], Type n) -> Doc + +pprBinderGroup lam (rs, t) + = lam <> parens ((hsep $ map pprBinder rs) <+> text ":" <+> ppr t) <> dot + + +-- Utils ------------------------------------------------------------------------------------------ +breakWhen :: Bool -> Doc +breakWhen True = line +breakWhen False = space + + +isSimpleX :: Exp a n -> Bool +isSimpleX xx + = case xx of + XVar{} -> True + XCon{} -> True + XType{} -> True + XWitness{} -> True + XApp _ x1 x2 -> isSimpleX x1 && isAtomX x2 + _ -> False + + +parens' :: Doc -> Doc +parens' d = lparen <> nest 1 d <> rparen + + +-- | Wrap a `Doc` in parens if the predicate is true. +pprParen' :: Bool -> Doc -> Doc +pprParen' b c + = if b then parens' c + else c diff --git a/DDC/Source/Tetra/Prim.hs b/DDC/Source/Tetra/Prim.hs new file mode 100644 --- /dev/null +++ b/DDC/Source/Tetra/Prim.hs @@ -0,0 +1,121 @@ + +module DDC.Source.Tetra.Prim + ( Name (..) + , TyConTetra (..) + , kindTyConTetra + + , OpStore (..) + , typeOpStore + + , PrimTyCon (..) + , kindPrimTyCon + , tBool + , tNat + , tInt + , tWord + + , PrimArith (..) + , typePrimArith + , readName) +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.Base.Pretty +import Control.DeepSeq +import Data.Char + +import DDC.Core.Tetra + ( readPrimTyCon + , readPrimArith + , readOpStore) + + +instance NFData Name where + rnf nn + = case nn of + NameVar s -> rnf s + NameCon s -> rnf s + + 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 + + NameHole -> () + + +instance Pretty Name where + ppr nn + = case nn of + NameVar v -> text v + NameCon c -> text c + + 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 + + NameHole -> text "?" + + +-- | 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 p <- readOpStore str + = Just $ NameOpStore p + + -- Primitive names. + | Just p <- readPrimTyCon str + = Just $ NamePrimTyCon p + + | Just p <- readPrimArith str + = Just $ NamePrimArith p + + -- Literal Bools + | str == "True#" = Just $ NameLitBool True + | str == "False#" = Just $ NameLitBool False + + -- Literal Nat + | Just val <- readLitNat str + = Just $ NameLitNat val + + -- Literal Ints + | Just val <- readLitInt str + = Just $ NameLitInt 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 + + -- Variables. + | c : _ <- str + , isLower c + = Just $ NameVar str + + | otherwise + = Nothing diff --git a/DDC/Source/Tetra/Prim/Base.hs b/DDC/Source/Tetra/Prim/Base.hs new file mode 100644 --- /dev/null +++ b/DDC/Source/Tetra/Prim/Base.hs @@ -0,0 +1,67 @@ + +module DDC.Source.Tetra.Prim.Base + ( Name (..) + , TyConTetra (..) + , OpStore (..) + , PrimTyCon (..) + , PrimArith (..)) +where +import DDC.Core.Tetra + ( OpStore (..) + , PrimTyCon (..) + , PrimArith (..)) + + +-- | Names of things used in Disciple Source Tetra. +data Name + -- | A user defined variable. + = NameVar String + + -- | A user defined constructor. + | NameCon String + + -- Baked in things ---------------------- + -- | Baked in data type constructors. + | NameTyConTetra TyConTetra + + -- | Baked in store operators. + | NameOpStore OpStore + + -- Machine primitives ------------------- + -- | Primitive type cosntructors. + | NamePrimTyCon PrimTyCon + + -- | Primitive arithmetic, logic and comparison. + | NamePrimArith PrimArith + + -- Literals ----------------------------- + -- | A boolean literal. + | NameLitBool Bool + + -- | A natural literal. + | NameLitNat Integer + + -- | An integer literal. + | NameLitInt Integer + + -- | A word literal. + | NameLitWord Integer Int + + -- Inference ---------------------------- + -- | A hole used during type inference. + | NameHole + deriving (Eq, Ord, Show) + + +-- TyConTetra ---------------------------------------------------------------- +-- | Baked-in type constructors. +data TyConTetra + -- | @Ref#@. Mutable reference. + = TyConTetraRef + + -- | @TupleN#@. Tuples. + | TyConTetraTuple Int + deriving (Eq, Ord, Show) + + + diff --git a/DDC/Source/Tetra/Prim/OpArith.hs b/DDC/Source/Tetra/Prim/OpArith.hs new file mode 100644 --- /dev/null +++ b/DDC/Source/Tetra/Prim/OpArith.hs @@ -0,0 +1,41 @@ + +module DDC.Source.Tetra.Prim.OpArith + (typePrimArith) +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 arithmetic operator. +typePrimArith :: PrimArith -> Type Name +typePrimArith op + = case op of + -- Numeric + PrimArithNeg -> tForall kData $ \t -> t `tFun` t + PrimArithAdd -> tForall kData $ \t -> t `tFun` t `tFun` t + PrimArithSub -> tForall kData $ \t -> t `tFun` t `tFun` t + PrimArithMul -> tForall kData $ \t -> t `tFun` t `tFun` t + PrimArithDiv -> tForall kData $ \t -> t `tFun` t `tFun` t + PrimArithMod -> tForall kData $ \t -> t `tFun` t `tFun` t + PrimArithRem -> tForall kData $ \t -> t `tFun` t `tFun` t + + -- Comparison + PrimArithEq -> tForall kData $ \t -> t `tFun` t `tFun` tBool + PrimArithNeq -> tForall kData $ \t -> t `tFun` t `tFun` tBool + PrimArithGt -> tForall kData $ \t -> t `tFun` t `tFun` tBool + PrimArithLt -> tForall kData $ \t -> t `tFun` t `tFun` tBool + PrimArithLe -> tForall kData $ \t -> t `tFun` t `tFun` tBool + PrimArithGe -> tForall kData $ \t -> t `tFun` t `tFun` tBool + + -- Boolean + PrimArithAnd -> tBool `tFun` tBool `tFun` tBool + PrimArithOr -> tBool `tFun` tBool `tFun` tBool + + -- Bitwise + PrimArithShl -> tForall kData $ \t -> t `tFun` t `tFun` t + PrimArithShr -> tForall kData $ \t -> t `tFun` t `tFun` t + PrimArithBAnd -> tForall kData $ \t -> t `tFun` t `tFun` t + PrimArithBOr -> tForall kData $ \t -> t `tFun` t `tFun` t + PrimArithBXOr -> tForall kData $ \t -> t `tFun` t `tFun` t diff --git a/DDC/Source/Tetra/Prim/OpStore.hs b/DDC/Source/Tetra/Prim/OpStore.hs new file mode 100644 --- /dev/null +++ b/DDC/Source/Tetra/Prim/OpStore.hs @@ -0,0 +1,13 @@ + +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/TyConPrim.hs b/DDC/Source/Tetra/Prim/TyConPrim.hs new file mode 100644 --- /dev/null +++ b/DDC/Source/Tetra/Prim/TyConPrim.hs @@ -0,0 +1,48 @@ + +module DDC.Source.Tetra.Prim.TyConPrim + ( kindPrimTyCon + , tBool, tNat, tInt, tWord) +where +import DDC.Source.Tetra.Prim.Base +import DDC.Type.Compounds +import DDC.Type.Exp + + +-- | Yield the kind of a type constructor. +kindPrimTyCon :: PrimTyCon -> Kind Name +kindPrimTyCon tc + = case tc of + PrimTyConVoid -> kData + PrimTyConPtr -> (kRegion `kFun` kData `kFun` kData) + PrimTyConAddr -> kData + PrimTyConBool -> kData + PrimTyConNat -> kData + PrimTyConInt -> kData + PrimTyConWord _ -> kData + PrimTyConFloat _ -> kData + PrimTyConTag -> kData + PrimTyConVec _ -> kData `kFun` kData + PrimTyConString -> kData + + +-- Compounds ------------------------------------------------------------------ +-- | Primitive `Bool` type. +tBool :: Type Name +tBool = TCon (TyConBound (UPrim (NamePrimTyCon PrimTyConBool) kData) kData) + + +-- | Primitive `Nat` type. +tNat :: Type Name +tNat = TCon (TyConBound (UPrim (NamePrimTyCon PrimTyConNat) kData) kData) + + +-- | Primitive `Int` type. +tInt :: Type Name +tInt = TCon (TyConBound (UPrim (NamePrimTyCon PrimTyConInt) kData) kData) + + +-- | Primitive `WordN` type of the given width. +tWord :: Int -> Type Name +tWord bits + = TCon (TyConBound (UPrim (NamePrimTyCon (PrimTyConWord bits)) kData) kData) + diff --git a/DDC/Source/Tetra/Prim/TyConTetra.hs b/DDC/Source/Tetra/Prim/TyConTetra.hs new file mode 100644 --- /dev/null +++ b/DDC/Source/Tetra/Prim/TyConTetra.hs @@ -0,0 +1,54 @@ + +module DDC.Source.Tetra.Prim.TyConTetra + ( kindTyConTetra + , readTyConTetra + , tRef) +where +import DDC.Source.Tetra.Prim.Base +import DDC.Type.Compounds +import DDC.Type.Exp +import DDC.Base.Pretty +import Data.Char +import Data.List +import Control.DeepSeq + +instance NFData TyConTetra + +instance Pretty TyConTetra where + ppr tc + = case tc of + TyConTetraRef -> text "Ref#" + TyConTetraTuple n -> text "Tuple" <> int n <> text "#" + + +-- | Read the name of a baked-in type constructor. +readTyConTetra :: String -> Maybe TyConTetra +readTyConTetra str + | Just rest <- stripPrefix "Tuple" str + , (ds, "#") <- span isDigit rest + , not $ null ds + , arity <- read ds + = Just $ TyConTetraTuple arity + + | otherwise + = case str of + "Ref#" -> Just TyConTetraRef + _ -> Nothing + + +-- | Take the kind of a baked-in data constructor. +kindTyConTetra :: TyConTetra -> Type Name +kindTyConTetra tc + = case tc of + TyConTetraRef -> kRegion `kFun` kData `kFun` kData + TyConTetraTuple n -> foldr kFun kData (replicate n 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] + where k = kRegion `kFun` kData `kFun` kData + diff --git a/DDC/Source/Tetra/ToCore.hs b/DDC/Source/Tetra/ToCore.hs new file mode 100644 --- /dev/null +++ b/DDC/Source/Tetra/ToCore.hs @@ -0,0 +1,306 @@ + +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/Defix.hs b/DDC/Source/Tetra/Transform/Defix.hs new file mode 100644 --- /dev/null +++ b/DDC/Source/Tetra/Transform/Defix.hs @@ -0,0 +1,299 @@ + +module DDC.Source.Tetra.Transform.Defix + ( FixTable (..) + , FixDef (..) + , InfixAssoc (..) + , defaultFixTable + , Error (..) + , Defix (..)) +where +import DDC.Source.Tetra.Transform.Defix.FixTable +import DDC.Source.Tetra.Transform.Defix.Error +import DDC.Source.Tetra.Compounds +import DDC.Source.Tetra.Module +import DDC.Source.Tetra.Exp +import DDC.Data.ListUtils +import Control.Monad +import Data.List +import Data.Maybe + + +-- Defix ---------------------------------------------------------------------- +class Defix (c :: * -> * -> *) where + -- | Resolve infix expressions in a thing. + defix :: FixTable a n + -> c a n + -> Either (Error a n) (c a n) + + +instance Defix Module where + defix table mm + = do tops' <- mapM (defix table) (moduleTops mm) + return $ mm { moduleTops = tops' } + + +instance Defix Top where + defix table tt + = case tt of + TopBind a b x -> liftM (TopBind a b) (defix table x) + _ -> return tt + + +instance Defix Exp where + defix table xx + = let down = defix table + in case xx of + XVar{} -> return xx + XCon{} -> 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) + XLet a lts x -> liftM2 (XLet a) (down lts) (down x) + XCase a x alts -> liftM2 (XCase a) (down x) (mapM down alts) + XCast a c x -> liftM (XCast a c) (down x) + XType{} -> return xx + XWitness{} -> return xx + + XDefix a xs + -> do xs' <- mapM down xs + xs_apps <- defixApps a table xs' + defixExps a table xs_apps + + XInfixOp{} -> return xx + + XInfixVar a str + -> case lookupDefInfixOfSymbol table str of + Just def -> return (fixDefExp def a) + Nothing -> Left $ ErrorNoInfixDef a str + + +instance Defix Lets where + defix table lts + = let down = defix table + in case lts of + LLet b x -> liftM (LLet b) (down x) + + LRec bxs + -> do let (bs, xs) = unzip bxs + xs' <- mapM (defix table) xs + return $ LRec (zip bs xs') + + LPrivate{} -> return lts + + +instance Defix Alt where + defix table aa + = let down = defix table + in case aa of + AAlt p x -> liftM (AAlt p) (down x) + + +------------------------------------------------------------------------------- +-- | Preprocess the body of an XDefix node to insert applications. +-- +-- Takes f a + g b with five nodes in the XDefix list. +-- 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] + +defixApps a table xx + = start xx + where + -- No expressions, we're done. + start [] + = return [] + + -- Single element, we're done. + start [x] + = return [x] + + -- Starting operator must be prefix. + start (XInfixOp aop op : xs) + | Just def <- lookupDefPrefixOfSymbol table op + = munch (fixDefExp def aop) xs + + | otherwise + = Left $ ErrorMalformed a (XDefix a xx) + + -- Trailing infix operator is malformed. + start (_ : XInfixOp{} : []) + = Left $ ErrorMalformed a (XDefix a xx) + + -- Start accumulating an application node. + start (x1 : xs) + = munch x1 xs + + + -- Munching is done. + munch acc [] + = return [acc] + + -- We've hit an infix op, drop the accumulated expression. + munch acc (xop@XInfixOp{} : xs) + = do xs' <- start xs + return $ acc : xop : xs' + + -- Add another argument to the application. + munch acc (x1 : xs) + = munch (XApp a acc x1) xs + + +------------------------------------------------------------------------------- +-- | Defix the body of a XDefix node. +-- +-- 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) + +defixExps a table xx + = case xx of + -- If there are no elements then we're screwed. + -- Maybe the parser is wrong or defixInfix has lost them. + [] -> error "ddc-source-tetra.defixExps: no expressions" + + -- If there is only one element then we're done. + [x] -> Right x + + -- Keep calling defixInfix until we've resolved all the ops. + x : xs + -> case defixInfix a table xx of + -- Defixer found errors. + Left errs -> Left errs + + -- Defixer didn't find any infix ops, so whatever is leftover + -- is a standard prefix application. + Right Nothing -> Right $ xApps a x xs + + -- Defixer made progress, so keep calling it. + Right (Just xs') -> defixExps a table xs' + + +-- | 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]) + +defixInfix a table xs + -- Get the list of infix ops in the expression. + | spOpStrs <- mapMaybe (\x -> case x of + XInfixOp sp str -> Just (sp, str) + _ -> Nothing) + xs + = case spOpStrs of + [] -> Right Nothing + _ -> defixInfix_ops a table xs spOpStrs + +defixInfix_ops sp table xs spOpStrs + = do + let (_opSps, opStrs) = unzip spOpStrs + + -- Lookup infix info for symbols. + defs <- mapM (getInfixDefOfSymbol sp table) opStrs + let precs = map fixDefPrec defs + + -- Get the highest precedence of all symbols. + let Just precHigh = takeMaximum precs + + -- Get the list of all ops having this highest precedence. + let opsHigh = nub + $ [ op | (op, prec) <- zip opStrs precs + , prec == precHigh ] + + -- Get the list of associativities for just the ops with + -- highest precedence. + defsHigh <- mapM (getInfixDefOfSymbol sp table) opsHigh + let assocsHigh = map fixDefAssoc defsHigh + + case nub assocsHigh of + [InfixLeft] + -> do xs' <- defixInfixLeft sp table precHigh xs + return $ Just xs' + + [InfixRight] + -> do xs' <- defixInfixRight sp table precHigh (reverse xs) + return $ Just (reverse xs') + + [InfixNone] + -> do xs' <- defixInfixNone sp table precHigh xs + return $ Just (reverse xs') + + _ -> Left $ ErrorDefixMixedAssoc sp opsHigh + + +-- | Defix some left associative ops. +defixInfixLeft + :: a -> FixTable a n -> Int + -> [Exp a n] -> Either (Error a n) [Exp a n] + +defixInfixLeft sp table precHigh (x1 : XInfixOp spo op : x2 : xs) + | Just def <- lookupDefInfixOfSymbol table op + , fixDefPrec def == precHigh + = Right (XApp sp (XApp sp (fixDefExp def spo) x1) x2 : xs) + + | otherwise + = do xs' <- defixInfixLeft sp table precHigh (x2 : xs) + Right $ x1 : XInfixOp spo op : xs' + +defixInfixLeft sp _ _ xs + = Left $ ErrorMalformed sp (XDefix sp xs) + + +-- | Defix some right associative ops. +-- 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] + +defixInfixRight sp table precHigh (x2 : XInfixOp spo op : x1 : xs) + | Just def <- lookupDefInfixOfSymbol table op + , fixDefPrec def == precHigh + = Right (XApp sp (XApp sp (fixDefExp def spo) x1) x2 : xs) + + | otherwise + = do xs' <- defixInfixRight sp table precHigh (x1 : xs) + Right $ x2 : XInfixOp spo op : xs' + +defixInfixRight sp _ _ xs + = Left $ ErrorMalformed sp (XDefix sp xs) + + +-- | Defix non-associative ops. +defixInfixNone + :: a -> FixTable a n -> Int + -> [Exp a n] -> Either (Error a n) [Exp a n] + +defixInfixNone sp table precHigh xx + -- If there are two ops in a row that are non-associative and have + -- the same precedence then we don't know which one should come first. + | _ : XInfixOp sp2 op2 : _ : XInfixOp sp4 op4 : _ <- xx + , Just def2 <- lookupDefInfixOfSymbol table op2 + , Just def4 <- lookupDefInfixOfSymbol table op4 + , fixDefPrec def2 == fixDefPrec def4 + = Left $ ErrorDefixNonAssoc op2 sp2 op4 sp4 + + -- Found a use of the operator of interest. + | x1 : XInfixOp sp2 op2 : x3 : xs <- xx + , Just def2 <- lookupDefInfixOfSymbol table op2 + , fixDefPrec def2 == precHigh + = Right $ (XApp sp (XApp sp (fixDefExp def2 sp2) x1) x3) : xs + + -- Some other operator. + | x1 : x2@(XInfixOp{}) : x3 : xs <- xx + = case defixInfixNone sp table precHigh (x3 : xs) of + Right xs' -> Right (x1 : x2 : xs') + Left errs -> Left errs + + | otherwise + = Left $ ErrorMalformed sp (XDefix sp xx) + diff --git a/DDC/Source/Tetra/Transform/Defix/Error.hs b/DDC/Source/Tetra/Transform/Defix/Error.hs new file mode 100644 --- /dev/null +++ b/DDC/Source/Tetra/Transform/Defix/Error.hs @@ -0,0 +1,65 @@ + +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 + + +-- | Things that can go wrong when defixing code. +data Error a n + -- | Infix operator symbol has no infix definition. + = ErrorNoInfixDef + { errorAnnot :: a + , errorSymbol :: String } + + -- | Two non-associative operators with the same precedence. + | ErrorDefixNonAssoc + { errorOp1 :: String + , errorAnnot1 :: a + , errorOp2 :: String + , errorAnnot2 :: a } + + -- | Two operators of different associativies with same precedence. + | ErrorDefixMixedAssoc + { errorAnnot :: a + , errorOps :: [String] } + + -- | Infix expression is malformed. + -- Eg "+ 3" or "2 + + 2" + | ErrorMalformed + { errorAnnot :: a + , errorExp :: Exp a n } + deriving Show + + +-- Pretty --------------------------------------------------------------------- +instance (Pretty n) + => Pretty (Error BP.SourcePos n) where + ppr err + = case err of + ErrorNoInfixDef{} + -> vcat [ ppr $ errorAnnot 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 " but the same precedence as" + , 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." ] + + ErrorMalformed{} + -> vcat [ ppr $ errorAnnot err + , text "Malformed infix expression." ] diff --git a/DDC/Source/Tetra/Transform/Defix/FixTable.hs b/DDC/Source/Tetra/Transform/Defix/FixTable.hs new file mode 100644 --- /dev/null +++ b/DDC/Source/Tetra/Transform/Defix/FixTable.hs @@ -0,0 +1,115 @@ + +module DDC.Source.Tetra.Transform.Defix.FixTable + ( FixTable (..) + , FixDef (..) + , InfixAssoc (..) + , lookupDefInfixOfSymbol + , lookupDefPrefixOfSymbol + , getInfixDefOfSymbol + , defaultFixTable) +where +import DDC.Source.Tetra.Transform.Defix.Error +import DDC.Source.Tetra.Prim +import DDC.Source.Tetra.Exp +import Data.List +import qualified DDC.Data.SourcePos as BP + + +-- | Table of infix operator definitions. +data FixTable a n + = FixTable [FixDef a n] + + +-- | Infix operator definition. +data FixDef a n + -- A prefix operator + = FixDefPrefix + { -- String of the operator + fixDefSymbol :: String + + -- Expression to rewrite the operator to, + -- given the annotation of the original symbol. + , fixDefExp :: a -> Exp a n } + + -- An infix operator. + | FixDefInfix + { -- String of the operator. + fixDefSymbol :: String + + -- Expression to rewrite the operator to, + -- given the annotation of the original symbol. + , fixDefExp :: a -> Exp a n + + -- Associativity of infix operator. + , fixDefAssoc :: InfixAssoc + + -- Precedence of infix operator. + , fixDefPrec :: Int } + + + +-- | Infix associativity. +data InfixAssoc + -- | Left associative. + --- + -- x * y * z => * (* x y) z + = InfixLeft + + -- | Right associative. + --- + -- x * y * z => * x (* y z) + | InfixRight + + -- | Non associative. + --- + -- x * y * z => error + | InfixNone + deriving (Show, Eq) + + +-- | Lookup the `FixDefInfix` corresponding to a symbol name, if any. +lookupDefInfixOfSymbol :: FixTable a n -> String -> Maybe (FixDef a n) +lookupDefInfixOfSymbol (FixTable defs) str + = find (\def -> case def of + FixDefInfix{} -> fixDefSymbol def == str + _ -> False) + defs + + +-- | Lookup the `FixDefPrefix` corresponding to a symbol name, if any. +lookupDefPrefixOfSymbol :: FixTable a n -> String -> Maybe (FixDef a n) +lookupDefPrefixOfSymbol (FixTable defs) str + = find (\def -> case def of + FixDefPrefix{} -> fixDefSymbol def == str + _ -> False) + defs + + +-- | Get the precedence of an infix symbol, else Error. +getInfixDefOfSymbol + :: a + -> FixTable a n + -> String + -> Either (Error a n) (FixDef a n) + +getInfixDefOfSymbol a table str + = case lookupDefInfixOfSymbol table str of + Nothing -> Left (ErrorNoInfixDef a str) + Just def -> Right def + + +-- | Default fixity table for infix operators. +defaultFixTable :: FixTable BP.SourcePos Name +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 ] diff --git a/DDC/Source/Tetra/Transform/Expand.hs b/DDC/Source/Tetra/Transform/Expand.hs new file mode 100644 --- /dev/null +++ b/DDC/Source/Tetra/Transform/Expand.hs @@ -0,0 +1,270 @@ + +module DDC.Source.Tetra.Transform.Expand + ( Config (..) + , configDefault + , Expand (..)) +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.Prim +import DDC.Source.Tetra.Exp +import DDC.Type.Collect +import DDC.Type.Env (KindEnv, TypeEnv) +import qualified DDC.Type.Env as Env +import qualified Data.Set as Set + + +------------------------------------------------------------------------------- +-- | Expander configuration. +data Config a n + = Config + { -- | Make a type hole of the given kind. + configMakeTypeHole :: Kind n -> Type n } + + +-- | Default expander configuration. +configDefault :: Config a Name +configDefault + = Config + { configMakeTypeHole = \k -> TVar (UPrim NameHole k)} + + +------------------------------------------------------------------------------- +class Expand (c :: * -> * -> *) 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 + + +instance Expand Module where + expand 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. + -- We need to do this in an initial binding because each top-level + -- thing is in-scope of all the others. + preTop p + = case p of + TopBind a b x + -> let (b', x') = expandQuant a config kenv (b, x) + in (TopBind a b' x', Env.singleton b') + + TopData _ def + -> (p, typeEnvOfDataDef def) + + (tops_quant, tenvs) + = unzip $ map preTop $ moduleTops mm + + -- Build the compound top-level environment. + tenv' = Env.unions $ tenv : tenvs + + -- Expand all the top-level definitions. + tops' = map (expand config kenv tenv') + $ tops_quant + + in mm { moduleTops = tops' } + + +instance Expand Top where + expand config kenv tenv top + = case top of + TopBind a b x + -> let tenv' = Env.extend b tenv + x' = expand config kenv tenv' x + in TopBind a b x' + + TopData{} + -> top + + +instance Expand Exp where + expand config kenv tenv xx + = let down = expand config kenv tenv + in case xx of + + -- Invoke the expander -------- + XVar{} + -> expandApp config kenv tenv xx [] + + XCon{} + -> expandApp config kenv tenv xx [] + + XApp{} + | (x1, xas) <- takeXAppsWithAnnots xx + -> if isXVar x1 || isXCon x1 + -- If the function is a variable or constructor then try to expand + -- extra arguments in the application. + then let xas' = [ (expand config kenv tenv x, a) | (x, a) <- xas ] + in expandApp config kenv tenv x1 xas' + + -- Otherwise just apply the original arguments. + else let x1' = expand config kenv tenv x1 + xas' = [ (expand config kenv tenv x, a) | (x, a) <- xas ] + in makeXAppsWithAnnots x1' xas' + + XLet a (LLet b x1) x2 + -> let + -- Add missing quantifiers to the types of let-bindings. + (b_quant, x1_quant) + = expandQuant a config kenv (b, x1) + + tenv' = Env.extend b_quant tenv + x1' = expand config kenv tenv' x1_quant + x2' = expand config kenv tenv' x2 + in XLet a (LLet b x1') x2' + + XLet a (LRec bxs) x2 + -> let + (bs_quant, xs_quant) + = unzip + $ [expandQuant a config kenv (b, x) | (b, x) <- bxs] + + tenv' = Env.extends bs_quant tenv + xs' = map (expand config kenv tenv') xs_quant + x2' = expand config kenv tenv' x2 + in XLet a (LRec (zip bs_quant xs')) x2' + + + -- Boilerplate ---------------- + XLAM a b x + -> let kenv' = Env.extend b kenv + x' = expand config kenv' tenv x + in XLAM a b x' + + XLam a b x + -> let tenv' = Env.extend b tenv + x' = expand config kenv tenv' x + in XLam a b x' + + XLet a (LPrivate bts mR bxs) x2 + -> let tenv' = Env.extends bts kenv + kenv' = Env.extends bxs tenv + 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) + XType{} -> xx + XWitness{} -> xx + XDefix a xs -> XDefix a (map down xs) + XInfixOp{} -> xx + XInfixVar{} -> xx + + +instance Expand Alt where + expand config kenv tenv alt + = case alt of + AAlt PDefault x2 + -> let x2' = expand config kenv tenv x2 + in AAlt PDefault x2' + + AAlt (PData dc bs) x2 + -> let tenv' = Env.extends bs tenv + x2' = expand config kenv tenv' x2 + in AAlt (PData dc bs) x2' + + +------------------------------------------------------------------------------- +-- | 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) + +expandQuant a config kenv (b, x) + | fvs <- freeVarsT kenv (typeOfBind b) + , not $ Set.null fvs + = let + -- Make binders for each of the free type variables. + -- We set these to holes so the Core type inferencer will determine + -- their kinds for us. + kHole = configMakeTypeHole config sComp + makeBind u + = case u of + UName n -> Just $ BName n kHole + UIx{} -> Just $ BAnon kHole + _ -> Nothing + + Just bsNew = sequence $ map makeBind $ Set.toList fvs + + -- Attach quantifiers to the front of the old type. + t' = foldr TForall (typeOfBind b) bsNew + b' = replaceTypeOfBind t' b + + -- Attach type lambdas to the front of the expression. + x' = foldr (XLAM a) x bsNew + + in (b', x') + + | otherwise + = (b, x) + + +------------------------------------------------------------------------------- +-- | Expand missing type arguments in applications. +-- +-- The thing being applied needs to be a variable or data constructor +-- so we can look up its type in the environment. Given the type, look +-- at the quantifiers out the front and insert new type applications if +-- 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 + +expandApp config _kenv tenv x0 xas0 + | Just (a, u) <- slurpVarConBound x0 + , Just tt <- Env.lookup u tenv + , not $ isBot tt + = let + go t xas + = case (t, xas) of + (TForall _b t2, (x1@(XType _ _t1'), a1) : xas') + -> (x1, a1) : go t2 xas' + + (TForall b t2, xas') + -> let k = typeOfBind b + Just a0 = takeAnnotOfExp x0 + xh = XType a0 (configMakeTypeHole config k) + in (xh, a) : go t2 xas' + + _ -> xas + + xas_expanded + = go tt xas0 + + in makeXAppsWithAnnots x0 xas_expanded + + | otherwise + = makeXAppsWithAnnots x0 xas0 + + +-- | 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 xx + = case xx of + XVar a u -> Just (a, u) + XCon a dc + | DaConBound n <- dc -> Just (a, UName n) + | DaConPrim n t <- dc -> Just (a, UPrim n t) + _ -> Nothing + diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,16 @@ +-------------------------------------------------------------------------------- +The Disciplined Disciple Compiler License (MIT style) + +Copyrite (K) 2007-2014 The Disciplined Disciple Compiler Strike Force +All rights reversed. + +Permission is hereby granted, free of charge, to any person obtaining a copy +of this software and associated documentation files (the "Software"), to deal +in the Software without restriction, including without limitation the rights +to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in +all copies or substantial portions of the Software. +-------------------------------------------------------------------------------- diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/ddc-source-tetra.cabal b/ddc-source-tetra.cabal new file mode 100644 --- /dev/null +++ b/ddc-source-tetra.cabal @@ -0,0 +1,79 @@ +Name: ddc-source-tetra +Version: 0.4.1.1 +License: MIT +License-file: LICENSE +Author: The Disciplined Disciple Compiler Strike Force +Maintainer: Ben Lippmeier +Build-Type: Simple +Cabal-Version: >=1.6 +Stability: experimental +Category: Compilers/Interpreters +Homepage: http://disciple.ouroborus.net +Synopsis: Disciplined Disciple Compiler source language. +Description: Disciplined Disciple Compiler Tetra source language. + Disciple Tetra is the main source language of DDC. + The word Tetra refers to the four base kinds: + 'Data', 'Region', 'Effect' and 'Witness'. + +Library + Build-Depends: + base >= 4.6 && < 4.8, + array >= 0.4 && < 0.6, + deepseq == 1.3.*, + containers == 0.5.*, + transformers == 0.3.*, + mtl == 2.1.*, + ddc-base == 0.4.1.*, + ddc-core == 0.4.1.*, + ddc-core-salt == 0.4.1.*, + ddc-core-tetra == 0.4.1.* + + Exposed-modules: + DDC.Source.Tetra.Transform.Expand + DDC.Source.Tetra.Transform.Defix + + DDC.Source.Tetra.Compounds + DDC.Source.Tetra.DataDef + DDC.Source.Tetra.Env + DDC.Source.Tetra.Exp + DDC.Source.Tetra.Lexer + DDC.Source.Tetra.Module + DDC.Source.Tetra.Parser + 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.Parser.Exp + DDC.Source.Tetra.Parser.Module + DDC.Source.Tetra.Parser.Param + DDC.Source.Tetra.Prim.Base + DDC.Source.Tetra.Prim.OpArith + DDC.Source.Tetra.Prim.OpStore + 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 + -fno-warn-orphans + -fno-warn-missing-signatures + -fno-warn-missing-methods + -fno-warn-unused-do-bind + + Extensions: + KindSignatures + NoMonomorphismRestriction + ScopedTypeVariables + PatternGuards + FlexibleContexts + FlexibleInstances + RankNTypes + BangPatterns + ParallelListComp +