ddc-source-tetra (empty) → 0.4.1.1
raw patch · 28 files changed
+3453/−0 lines, 28 filesdep +arraydep +basedep +containerssetup-changed
Dependencies added: array, base, containers, ddc-base, ddc-core, ddc-core-salt, ddc-core-tetra, deepseq, mtl, transformers
Files
- DDC/Source/Tetra/Compounds.hs +208/−0
- DDC/Source/Tetra/DataDef.hs +68/−0
- DDC/Source/Tetra/Env.hs +47/−0
- DDC/Source/Tetra/Exp.hs +23/−0
- DDC/Source/Tetra/Exp/Base.hs +168/−0
- DDC/Source/Tetra/Lexer.hs +19/−0
- DDC/Source/Tetra/Lexer/Lit.hs +85/−0
- DDC/Source/Tetra/Module.hs +99/−0
- DDC/Source/Tetra/Parser.hs +54/−0
- DDC/Source/Tetra/Parser/Exp.hs +531/−0
- DDC/Source/Tetra/Parser/Module.hs +219/−0
- DDC/Source/Tetra/Parser/Param.hs +33/−0
- DDC/Source/Tetra/Predicates.hs +130/−0
- DDC/Source/Tetra/Pretty.hs +273/−0
- DDC/Source/Tetra/Prim.hs +121/−0
- DDC/Source/Tetra/Prim/Base.hs +67/−0
- DDC/Source/Tetra/Prim/OpArith.hs +41/−0
- DDC/Source/Tetra/Prim/OpStore.hs +13/−0
- DDC/Source/Tetra/Prim/TyConPrim.hs +48/−0
- DDC/Source/Tetra/Prim/TyConTetra.hs +54/−0
- DDC/Source/Tetra/ToCore.hs +306/−0
- DDC/Source/Tetra/Transform/Defix.hs +299/−0
- DDC/Source/Tetra/Transform/Defix/Error.hs +65/−0
- DDC/Source/Tetra/Transform/Defix/FixTable.hs +115/−0
- DDC/Source/Tetra/Transform/Expand.hs +270/−0
- LICENSE +16/−0
- Setup.hs +2/−0
- ddc-source-tetra.cabal +79/−0
+ DDC/Source/Tetra/Compounds.hs view
@@ -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
+ DDC/Source/Tetra/DataDef.hs view
@@ -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)
+ DDC/Source/Tetra/Env.hs view
@@ -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
+ DDC/Source/Tetra/Exp.hs view
@@ -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
+ DDC/Source/Tetra/Exp/Base.hs view
@@ -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
+ DDC/Source/Tetra/Lexer.hs view
@@ -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
+ DDC/Source/Tetra/Lexer/Lit.hs view
@@ -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+
+ DDC/Source/Tetra/Module.hs view
@@ -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 +
+ DDC/Source/Tetra/Parser.hs view
@@ -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)+
+ DDC/Source/Tetra/Parser/Exp.hs view
@@ -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+
+ DDC/Source/Tetra/Parser/Module.hs view
@@ -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 }+
+ DDC/Source/Tetra/Parser/Param.hs view
@@ -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
+ DDC/Source/Tetra/Predicates.hs view
@@ -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
+ DDC/Source/Tetra/Pretty.hs view
@@ -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
+ DDC/Source/Tetra/Prim.hs view
@@ -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
+ DDC/Source/Tetra/Prim/Base.hs view
@@ -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)+++
+ DDC/Source/Tetra/Prim/OpArith.hs view
@@ -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
+ DDC/Source/Tetra/Prim/OpStore.hs view
@@ -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
+ DDC/Source/Tetra/Prim/TyConPrim.hs view
@@ -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)+
+ DDC/Source/Tetra/Prim/TyConTetra.hs view
@@ -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+
+ DDC/Source/Tetra/ToCore.hs view
@@ -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+
+ DDC/Source/Tetra/Transform/Defix.hs view
@@ -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)+
+ DDC/Source/Tetra/Transform/Defix/Error.hs view
@@ -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." ]
+ DDC/Source/Tetra/Transform/Defix/FixTable.hs view
@@ -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 ]
+ DDC/Source/Tetra/Transform/Expand.hs view
@@ -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+
+ LICENSE view
@@ -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.+--------------------------------------------------------------------------------
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ ddc-source-tetra.cabal view
@@ -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 <benl@ouroborus.net>+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+