ddc-source-tetra 0.4.1.3 → 0.4.2.1

raw patch · 37 files changed

+2929/−1196 lines, 37 filesdep +textdep ~basedep ~ddc-basedep ~ddc-corePVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: text

Dependency ranges changed: base, ddc-base, ddc-core, ddc-core-salt, ddc-core-tetra, deepseq, mtl

API changes (from Hackage documentation)

Files

• DDC/Source/Tetra/Compounds.hs +55/−19
• DDC/Source/Tetra/Convert.hs +515/−0
• DDC/Source/Tetra/Convert/Error.hs +27/−0
• DDC/Source/Tetra/DataDef.hs +6/−2
• DDC/Source/Tetra/Env.hs +49/−10
• DDC/Source/Tetra/Exp.hs +21/−13
• DDC/Source/Tetra/Exp/Annot.hs +54/−0
• DDC/Source/Tetra/Exp/Base.hs +0/−168
• DDC/Source/Tetra/Exp/Generic.hs +322/−0
• DDC/Source/Tetra/Lexer.hs +9/−2
• DDC/Source/Tetra/Lexer/Lit.hs +0/−85
• DDC/Source/Tetra/Module.hs +41/−32
• DDC/Source/Tetra/Parser.hs +2/−0
• DDC/Source/Tetra/Parser/Atom.hs +28/−0
• DDC/Source/Tetra/Parser/Exp.hs +220/−107
• DDC/Source/Tetra/Parser/Module.hs +97/−58
• DDC/Source/Tetra/Parser/Param.hs +5/−4
• DDC/Source/Tetra/Parser/Witness.hs +100/−0
• DDC/Source/Tetra/Predicates.hs +15/−13
• DDC/Source/Tetra/Pretty.hs +115/−86
• DDC/Source/Tetra/Prim.hs +232/−59
• DDC/Source/Tetra/Prim/Base.hs +168/−36
• DDC/Source/Tetra/Prim/OpArith.hs +1/−0
• DDC/Source/Tetra/Prim/OpError.hs +19/−0
• DDC/Source/Tetra/Prim/OpFun.hs +69/−0
• DDC/Source/Tetra/Prim/OpStore.hs +0/−13
• DDC/Source/Tetra/Prim/OpVector.hs +32/−0
• DDC/Source/Tetra/Prim/TyConPrim.hs +35/−11
• DDC/Source/Tetra/Prim/TyConTetra.hs +48/−21
• DDC/Source/Tetra/ToCore.hs +0/−306
• DDC/Source/Tetra/Transform/BoundX.hs +215/−0
• DDC/Source/Tetra/Transform/Defix.hs +77/−29
• DDC/Source/Tetra/Transform/Defix/Error.hs +25/−22
• DDC/Source/Tetra/Transform/Defix/FixTable.hs +58/−26
• DDC/Source/Tetra/Transform/Expand.hs +163/−52
• DDC/Source/Tetra/Transform/Guards.hs +68/−0
• ddc-source-tetra.cabal +38/−22

@@ -1,4 +1,6 @@+{-# LANGUAGE TypeFamilies #-} +-- | Utilities for constructing and destructing Source Tetra expressions. module DDC.Source.Tetra.Compounds         ( module DDC.Type.Compounds         , takeAnnotOfExp@@ -21,6 +23,10 @@         , takeXConApps         , takeXPrimApps +          -- * Casts+        , xBox+        , xRun+           -- * Data Constructors         , dcUnit         , takeNameOfDaCon@@ -28,17 +34,24 @@            -- * Patterns         , bindsOfPat+        , pTrue+        , pFalse            -- * Witnesses         , wApp         , wApps         , takeXWitness         , takeWAppsAsList-        , takePrimWiConApps)+        , takePrimWiConApps++          -- * Primitives+        , xErrorDefault) where import DDC.Source.Tetra.Exp+import DDC.Source.Tetra.Prim import DDC.Type.Compounds-import DDC.Core.Compounds+import Data.Text                        (Text)+import DDC.Core.Exp.Annot.Compounds         ( dcUnit         , takeNameOfDaCon         , takeTypeOfDaCon@@ -51,13 +64,15 @@         , takeWAppsAsList         , takePrimWiConApps)         + -- Annotations ---------------------------------------------------------------- -- | Take the outermost annotation from an expression, --   or Nothing if this is an `XType` or `XWitness` without an annotation.-takeAnnotOfExp :: Exp a n -> Maybe a+takeAnnotOfExp :: GExp l -> Maybe (GAnnot l) takeAnnotOfExp xx  = case xx of         XVar  a _       -> Just a+        XPrim a _       -> Just a         XCon  a _       -> Just a         XLAM  a _ _     -> Just a         XLam  a _ _     -> Just a@@ -74,20 +89,20 @@  -- Lambdas --------------------------------------------------------------------- -- | Make some nested type lambdas.-xLAMs :: a -> [Bind n] -> Exp a n -> Exp a n+xLAMs :: GAnnot l -> [GBind l] -> GExp l -> GExp l xLAMs a bs x         = foldr (XLAM a) x bs   -- | Make some nested value or witness lambdas.-xLams :: a -> [Bind n] -> Exp a n -> Exp a n+xLams :: GAnnot l -> [GBind l] -> GExp l -> GExp l xLams a bs x         = foldr (XLam a) x bs   -- | Split type lambdas from the front of an expression, --   or `Nothing` if there aren't any.-takeXLAMs :: Exp a n -> Maybe ([Bind n], Exp a n)+takeXLAMs :: GExp l -> Maybe ([GBind l], GExp l) takeXLAMs xx  = let  go bs (XLAM _ b x) = go (b:bs) x         go bs x            = (reverse bs, x)@@ -98,7 +113,7 @@  -- | Split nested value or witness lambdas from the front of an expression, --   or `Nothing` if there aren't any.-takeXLams :: Exp a n -> Maybe ([Bind n], Exp a n)+takeXLams :: GExp l -> Maybe ([GBind l], GExp l) takeXLams xx  = let  go bs (XLam _ b x) = go (b:bs) x         go bs x            = (reverse bs, x)@@ -110,7 +125,7 @@ -- | Make some nested lambda abstractions, --   using a flag to indicate whether the lambda is a --   level-1 (True), or level-0 (False) binder.-makeXLamFlags :: a -> [(Bool, Bind n)] -> Exp a n -> Exp a n+makeXLamFlags :: GAnnot l -> [(Bool, GBind l)] -> GExp l -> GExp l makeXLamFlags a fbs x  = foldr (\(f, b) x'            -> if f then XLAM a b x'@@ -121,7 +136,7 @@ -- | Split nested lambdas from the front of an expression,  --   with a flag indicating whether the lambda was a level-1 (True),  --   or level-0 (False) binder.-takeXLamFlags :: Exp a n -> Maybe ([(Bool, Bind n)], Exp a n)+takeXLamFlags :: GExp l -> Maybe ([(Bool, GBind l)], GExp l) takeXLamFlags xx  = let  go bs (XLAM _ b x) = go ((True,  b):bs) x         go bs (XLam _ b x) = go ((False, b):bs) x@@ -133,14 +148,14 @@  -- Applications --------------------------------------------------------------- -- | Build sequence of value applications.-xApps   :: a -> Exp a n -> [Exp a n] -> Exp a n+xApps   :: GAnnot l -> GExp l -> [GExp l] -> GExp l xApps a t1 ts     = foldl (XApp a) t1 ts   -- | Build sequence of applications. --   Similar to `xApps` but also takes list of annotations for  --   the `XApp` constructors.-makeXAppsWithAnnots :: Exp a n -> [(Exp a n, a)] -> Exp a n+makeXAppsWithAnnots :: GExp l -> [(GExp l, GAnnot l)] -> GExp l makeXAppsWithAnnots f xas  = case xas of         []              -> f@@ -150,7 +165,7 @@ -- | Flatten an application into the function part and its arguments. -- --   Returns `Nothing` if there is no outer application.-takeXApps :: Exp a n -> Maybe (Exp a n, [Exp a n])+takeXApps :: GExp l -> Maybe (GExp l, [GExp l]) takeXApps xx  = case takeXAppsAsList xx of         (x1 : xsArgs)   -> Just (x1, xsArgs)@@ -160,7 +175,7 @@ -- | Flatten an application into the function part and its arguments. -- --   This is like `takeXApps` above, except we know there is at least one argument.-takeXApps1 :: Exp a n -> Exp a n -> (Exp a n, [Exp a n])+takeXApps1 :: GExp l -> GExp l -> (GExp l, [GExp l]) takeXApps1 x1 x2  = case takeXApps x1 of         Nothing          -> (x1,  [x2])@@ -168,7 +183,7 @@   -- | Flatten an application into the function parts and arguments, if any.-takeXAppsAsList  :: Exp a n -> [Exp a n]+takeXAppsAsList  :: GExp l -> [GExp l] takeXAppsAsList xx  = case xx of         XApp _ x1 x2    -> takeXAppsAsList x1 ++ [x2]@@ -177,7 +192,7 @@  -- | Destruct sequence of applications. --   Similar to `takeXAppsAsList` but also keeps annotations for later.-takeXAppsWithAnnots :: Exp a n -> (Exp a n, [(Exp a n, a)])+takeXAppsWithAnnots :: GExp l -> (GExp l, [(GExp l, GAnnot l)]) takeXAppsWithAnnots xx  = case xx of         XApp a f arg@@ -191,18 +206,39 @@ --   and its arguments. --    --   Returns `Nothing` if the expression isn't a primop application.-takeXPrimApps :: Exp a n -> Maybe (n, [Exp a n])+takeXPrimApps :: GExp l -> Maybe (GPrim l, [GExp l]) takeXPrimApps xx  = case takeXAppsAsList xx of-        XVar _ (UPrim p _) : xs -> Just (p, xs)-        _                       -> Nothing+        XPrim _ p : xs  -> Just (p, xs)+        _               -> Nothing  -- | Flatten an application of a data constructor into the constructor --   and its arguments.  -- --   Returns `Nothing` if the expression isn't a constructor application.-takeXConApps :: Exp a n -> Maybe (DaCon n, [Exp a n])+takeXConApps :: GExp l -> Maybe (DaCon (GName l), [GExp l]) takeXConApps xx  = case takeXAppsAsList xx of         XCon _ dc : xs  -> Just (dc, xs)         _               -> Nothing+++-- Casts ----------------------------------------------------------------------+xBox a x = XCast a CastBox x+xRun a x = XCast a CastRun x+++-- Primitives -----------------------------------------------------------------+xErrorDefault :: (GPrim l ~ PrimVal, GName l ~ Name)+              => GAnnot l -> Text -> Integer -> GExp l+xErrorDefault a name n+ = xApps a+        (XPrim a  (PrimValError OpErrorDefault))+        [ XCon a (DaConPrim (NameLitTextLit name) (tBot kData))+        , XCon a (DaConPrim (NameLitNat     n)    (tBot kData))]++-- Patterns -------------------------------------------------------------------+pTrue    = PData (DaConPrim (NameLitBool True)  tBool) []+pFalse   = PData (DaConPrim (NameLitBool False) tBool) []++

@@ -0,0 +1,515 @@+{-# LANGUAGE TypeFamilies #-}++-- | Source Tetra conversion to Disciple Core Tetra language.+module DDC.Source.Tetra.Convert+        ( ConvertM+        , ErrorConvert (..)+        , coreOfSourceModule+        , runConvertM)+where+import DDC.Source.Tetra.Convert.Error+import DDC.Data.SourcePos++import qualified DDC.Source.Tetra.Transform.Guards      as S+import qualified DDC.Source.Tetra.Module                as S+import qualified DDC.Source.Tetra.DataDef               as S+import qualified DDC.Source.Tetra.Env                   as S+import qualified DDC.Source.Tetra.Compounds             as S+import qualified DDC.Source.Tetra.Exp.Annot             as S+import qualified DDC.Source.Tetra.Prim                  as S++import qualified DDC.Core.Tetra.Prim                    as C+import qualified DDC.Core.Module                        as C+import qualified DDC.Core.Exp.Annot                     as C+import qualified DDC.Type.DataDef                       as C++import qualified DDC.Type.Exp                           as T+import qualified DDC.Type.Sum                           as Sum+import qualified Data.Text                              as Text+import Data.Maybe+++import DDC.Core.Module +        ( ExportSource  (..)+        , ImportType    (..)+        , ImportCap     (..)+        , ImportValue   (..))+++---------------------------------------------------------------------------------------------------+type ConvertM a x+        = Either (ErrorConvert a) x++type SP = SourcePos+++-- | Run a conversion computation.+runConvertM :: ConvertM a x -> Either (ErrorConvert a) x+runConvertM cc = cc++-- | Convert a Source Tetra module to Core Tetra.+coreOfSourceModule +        :: SP+        -> S.Module (S.Annot SP)+        -> Either (ErrorConvert SP) (C.Module SP C.Name)++coreOfSourceModule a mm+        = runConvertM +        $ coreOfSourceModuleM a mm+++-- Module -----------------------------------------------------------------------------------------+-- | Convert a Source Tetra module to Core Tetra.+--+--   The Source code needs to already have been desugared and cannot contain,+--   and `XDefix`, `XInfixOp`, or `XInfixVar` nodes, else `error`.+--+--   We use the map of core headers to add imports for all the names that this+--   module uses from its environment.+-- +coreOfSourceModuleM+        :: SP+        -> S.Module (S.Annot SP)+        -> ConvertM SP (C.Module SP C.Name)++coreOfSourceModuleM a mm+ = do   +        -- Exported types and values.+        exportTypes'    <- sequence+                        $  fmap (\n +                                -> (,)  <$> (pure $ toCoreN n) +                                        <*> (pure $ ExportSourceLocalNoType (toCoreN n)))+                        $  S.moduleExportTypes mm++        exportValues'   <- sequence+                        $  fmap (\n+                                -> (,)  <$> (pure $ toCoreN n)+                                        <*> (pure $ ExportSourceLocalNoType (toCoreN n)))+                        $  S.moduleExportValues mm++        -- Imported types and values.+        importTypes'    <- sequence+                        $  fmap (\(n, it) +                                -> (,)  <$> (pure $ toCoreN n) <*> (toCoreImportType it))+                        $  S.moduleImportTypes  mm++        importCaps'     <- sequence +                        $  fmap (\(n, iv) +                                -> (,)  <$> (pure $ toCoreN n) <*> (toCoreImportCap iv))+                        $  S.moduleImportCaps   mm++        importValues'   <- sequence +                        $  fmap (\(n, iv) +                                -> (,)  <$> (pure $ toCoreN n) <*> (toCoreImportValue iv))+                        $  S.moduleImportValues mm++        -- Data type definitions.+        dataDefsLocal   <- sequence $ fmap toCoreDataDef +                        $  [ def | S.TopData _ def <- S.moduleTops mm ]++        -- Top level bindings.+        ltsTops         <- letsOfTops $  S.moduleTops mm++        return+         $ C.ModuleCore+                { C.moduleName          = S.moduleName mm+                , C.moduleIsHeader      = False++                , C.moduleExportTypes   = exportTypes'++                , C.moduleExportValues+                   =  exportValues'+                   ++ (if C.isMainModuleName (S.moduleName mm)+                        && (not $ elem (S.NameVar "main") $ S.moduleExportValues mm)+                        then [ ( C.NameVar "main"+                             , ExportSourceLocalNoType (C.NameVar "main"))]+                        else [])++                , C.moduleImportTypes    = importTypes'+                , C.moduleImportCaps     = importCaps'+                , C.moduleImportValues   = importValues'+                , C.moduleImportDataDefs = []+                , C.moduleDataDefsLocal  = dataDefsLocal+                , C.moduleBody           = C.XLet  a ltsTops (C.xUnit a) }+++-- | Extract the top-level bindings from some source definitions.+letsOfTops :: [S.Top (S.Annot SP)] +           -> ConvertM SP (C.Lets SP C.Name)+letsOfTops tops+ = C.LRec <$> (sequence $ mapMaybe bindOfTop tops)+++-- | Try to convert a `TopBind` to a top-level binding, +--   or `Nothing` if it isn't one.+bindOfTop  +        :: S.Top (S.Annot SP) +        -> Maybe (ConvertM SP (T.Bind C.Name, C.Exp SP C.Name))++bindOfTop (S.TopClause _ (S.SLet _ b [] [S.GExp x]))+ = Just ((,) <$> toCoreB b <*> toCoreX x)++bindOfTop _     + = Nothing+++-- ImportType -------------------------------------------------------------------------------------+toCoreImportType :: ImportType S.Name -> ConvertM a (ImportType C.Name)+toCoreImportType src+ = case src of+        ImportTypeAbstract t    +         -> ImportTypeAbstract <$> toCoreT t++        ImportTypeBoxed t+         -> ImportTypeBoxed    <$> toCoreT t+++-- ImportCap --------------------------------------------------------------------------------------+toCoreImportCap :: ImportCap S.Name -> ConvertM a (ImportCap C.Name)+toCoreImportCap src+ = case src of+        ImportCapAbstract t+         -> ImportCapAbstract   <$> toCoreT t+++-- ImportValue ------------------------------------------------------------------------------------+toCoreImportValue :: ImportValue S.Name -> ConvertM a (ImportValue C.Name)+toCoreImportValue src+ = case src of+        ImportValueModule mn n t mA+         ->  ImportValueModule +         <$> (pure mn) <*> (pure $ toCoreN n) <*> toCoreT t <*> pure mA++        ImportValueSea v t+         -> ImportValueSea +         <$> pure v    <*> toCoreT t+++-- Type -------------------------------------------------------------------------------------------+toCoreT :: T.Type S.Name -> ConvertM a (T.Type C.Name)+toCoreT tt+ = case tt of+        T.TVar u+         -> T.TVar <$> toCoreU  u++        T.TCon tc+         -> T.TCon <$> toCoreTC tc++        T.TForall b t+         -> T.TForall <$> toCoreB b  <*> toCoreT t++        T.TApp t1 t2+         -> T.TApp    <$> toCoreT t1 <*> toCoreT t2++        T.TSum ts+         -> do  k'      <- toCoreT $ Sum.kindOfSum ts++                tss'    <- fmap (Sum.fromList k') +                        $  sequence $ fmap toCoreT $ Sum.toList ts++                return  $ T.TSum tss'+++-- TyCon ------------------------------------------------------------------------------------------+toCoreTC :: T.TyCon S.Name -> ConvertM a (T.TyCon C.Name)+toCoreTC tc+ = case tc of+        T.TyConSort sc    +         -> pure $ T.TyConSort sc++        T.TyConKind kc+         -> pure $ T.TyConKind kc++        T.TyConWitness wc+         -> pure $ T.TyConWitness wc++        T.TyConSpec sc+         -> pure $ T.TyConSpec sc++        T.TyConBound u k+         -> T.TyConBound  <$> toCoreU u <*> toCoreT k++        T.TyConExists n k+         -> T.TyConExists <$> pure n    <*> toCoreT k+++-- DataDef ----------------------------------------------------------------------------------------+toCoreDataDef :: S.DataDef S.Name -> ConvertM a (C.DataDef C.Name)+toCoreDataDef def+ = do+        defParams       <- sequence $ fmap toCoreB $ S.dataDefParams def++        defCtors        <- sequence $ fmap (\(ctor, tag) -> toCoreDataCtor def tag ctor)+                                    $ [(ctor, tag) | ctor <- S.dataDefCtors def+                                                   | tag  <- [0..]]++        return $ C.DataDef+         { C.dataDefTypeName    = toCoreN     $ S.dataDefTypeName def+         , C.dataDefParams      = defParams+         , C.dataDefCtors       = Just $ defCtors+         , C.dataDefIsAlgebraic = True }+++-- DataCtor ---------------------------------------------------------------------------------------+toCoreDataCtor +        :: S.DataDef S.Name +        -> Integer+        -> S.DataCtor S.Name +        -> ConvertM a (C.DataCtor C.Name)++toCoreDataCtor dataDef tag ctor+ = do   typeParams      <- sequence $ fmap toCoreB $ S.dataDefParams dataDef+        fieldTypes      <- sequence $ fmap toCoreT $ S.dataCtorFieldTypes ctor+        resultType      <- toCoreT (S.dataCtorResultType ctor)++        return $ C.DataCtor+         { C.dataCtorName        = toCoreN (S.dataCtorName ctor)+         , C.dataCtorTag         = tag+         , C.dataCtorFieldTypes  = fieldTypes+         , C.dataCtorResultType  = resultType+         , C.dataCtorTypeName    = toCoreN (S.dataDefTypeName dataDef) +         , C.dataCtorTypeParams  = typeParams }+++-- Exp --------------------------------------------------------------------------------------------+toCoreX :: S.Exp SP -> ConvertM SP (C.Exp SP C.Name)+toCoreX xx+ = case xx of+        S.XVar a u      +         -> C.XVar  <$> pure a <*> toCoreU  u++        -- Wrap text literals into Text during conversion to Core.+        -- The 'textLit' variable refers to whatever is in scope.+        S.XCon a dc@(C.DaConPrim (S.NameLitTextLit{}) _)+         -> C.XApp  <$> pure a +                    <*> (C.XVar <$> pure a <*> (pure $ C.UName (C.NameVar "textLit")))+                    <*> (C.XCon <$> pure a <*> (toCoreDC dc))++        S.XPrim a p+         -> C.XVar  <$> pure a <*> toCoreU (C.UPrim (S.NameVal p) (S.typeOfPrimVal p))++        S.XCon a dc+         -> C.XCon  <$> pure a <*> toCoreDC dc++        S.XLAM a b x+         -> C.XLAM  <$> pure a <*> toCoreB b  <*> toCoreX x++        S.XLam a b x+         -> C.XLam  <$> pure a <*> toCoreB b  <*> toCoreX x++        -- We don't want to wrap the source file path passed to the default# prim+        -- in a Text constructor, so detect this case separately.+        S.XApp a0 _ _+         |  Just ( p@(S.PrimValError S.OpErrorDefault)+                 , [S.XCon a1 dc1, S.XCon a2 dc2])+                 <- S.takeXPrimApps xx+         -> do  xPrim'  <- toCoreX (S.XPrim a0 p)+                dc1'    <- toCoreDC dc1+                dc2'    <- toCoreDC dc2+                return  $  C.xApps a0 xPrim' [C.XCon a1 dc1', C.XCon a2 dc2']++        S.XApp a x1 x2+         -> C.XApp  <$> pure a <*> toCoreX x1 <*> toCoreX x2++        S.XLet a lts x+         -> C.XLet  <$> pure a <*> toCoreLts lts <*> toCoreX x++        S.XCase a x alts+         -> C.XCase <$> pure a <*> toCoreX x <*> (sequence $ map (toCoreA a) alts)++        S.XCast a c x+         -> C.XCast <$> pure a <*> toCoreC c <*> toCoreX x++        S.XType a t+         -> C.XType    <$> pure a <*> toCoreT t++        S.XWitness a w+         -> C.XWitness <$> pure a <*> toCoreW w++        -- These shouldn't exist in the desugared source tetra code.+        S.XDefix{}      -> Left $ ErrorConvertCannotConvertSugarExp xx+        S.XInfixOp{}    -> Left $ ErrorConvertCannotConvertSugarExp xx+        S.XInfixVar{}   -> Left $ ErrorConvertCannotConvertSugarExp xx+++-- Lets -------------------------------------------------------------------------------------------+toCoreLts :: S.Lets SP -> ConvertM SP (C.Lets SP C.Name)+toCoreLts lts+ = case lts of+        S.LLet b x+         -> C.LLet <$> toCoreB b <*> toCoreX x+        +        S.LRec bxs+         -> C.LRec <$> (sequence $ map (\(b, x) -> (,) <$> toCoreB b <*> toCoreX x) bxs)++        S.LPrivate bks Nothing bts+         -> C.LPrivate <$> (sequence $ fmap toCoreB bks) +                       <*>  pure Nothing +                       <*> (sequence $ fmap toCoreB bts)++        S.LPrivate bks (Just tParent) bts+         -> C.LPrivate <$> (sequence $ fmap toCoreB bks) +                       <*> (fmap Just $ toCoreT tParent)+                       <*> (sequence $ fmap toCoreB bts)++        S.LGroup{}+         -> Left $ ErrorConvertCannotConvertSugarLets lts+++-- Cast -------------------------------------------------------------------------------------------+toCoreC :: S.Cast a -> ConvertM a (C.Cast a C.Name)+toCoreC cc+ = case cc of+        S.CastWeakenEffect eff+         -> C.CastWeakenEffect <$> toCoreT eff++        S.CastPurify w+         -> C.CastPurify       <$> toCoreW w++        S.CastBox+         -> pure C.CastBox++        S.CastRun+         -> pure C.CastRun+++-- Alt --------------------------------------------------------------------------------------------+toCoreA  :: SP -> S.Alt SP -> ConvertM SP (C.Alt SP C.Name)+toCoreA sp (S.AAlt w gxs)+ = C.AAlt <$> toCoreP w+          <*> (toCoreX  $ S.desugarGuards sp gxs +                        $ S.xErrorDefault sp+                                (Text.pack    $ sourcePosSource sp)+                                (fromIntegral $ sourcePosLine   sp))+++-- Pat --------------------------------------------------------------------------------------------+toCoreP  :: S.Pat a -> ConvertM a (C.Pat C.Name)+toCoreP pp+ = case pp of+        S.PDefault        +         -> pure C.PDefault+        +        S.PData dc bs+         -> C.PData <$> toCoreDC dc <*> (sequence $ fmap toCoreB bs)+++-- DaCon ------------------------------------------------------------------------------------------+toCoreDC :: S.DaCon S.Name -> ConvertM a (C.DaCon C.Name)+toCoreDC dc+ = case dc of+        S.DaConUnit+         -> pure $ C.DaConUnit++        S.DaConPrim n t +         -> C.DaConPrim  <$> (pure $ toCoreN n) <*> toCoreT t++        S.DaConBound n+         -> C.DaConBound <$> (pure $ toCoreN n)+++-- Witness ----------------------------------------------------------------------------------------+toCoreW :: S.Witness a -> ConvertM a (C.Witness a C.Name)+toCoreW ww+ = case ww of+        S.WVar a u+         -> C.WVar  <$> pure a <*> toCoreU  u++        S.WCon a wc+         -> C.WCon  <$> pure a <*> toCoreWC wc++        S.WApp a w1 w2+         -> C.WApp  <$> pure a <*> toCoreW  w1 <*> toCoreW w2++        S.WType a t+         -> C.WType <$> pure a <*> toCoreT  t+++-- WiCon ------------------------------------------------------------------------------------------+toCoreWC :: S.WiCon a -> ConvertM a (C.WiCon C.Name)+toCoreWC wc+ = case wc of+        S.WiConBound u t+         -> C.WiConBound <$> toCoreU u <*> toCoreT t+++-- Bind -------------------------------------------------------------------------------------------+toCoreB :: S.Bind -> ConvertM a (C.Bind C.Name)+toCoreB bb+ = case bb of+        T.BName n t+         -> T.BName <$> (pure $ toCoreN n) <*> toCoreT t++        T.BAnon t+         -> T.BAnon <$> toCoreT t++        T.BNone t+         -> T.BNone <$> toCoreT t+++-- Bound ------------------------------------------------------------------------------------------+toCoreU :: S.Bound -> ConvertM a (C.Bound C.Name)+toCoreU uu+ = case uu of+        T.UName n+         -> T.UName <$> (pure $ toCoreN n)++        T.UIx   i+         -> T.UIx   <$> (pure i)++        T.UPrim n t+         -> T.UPrim <$> (pure $ toCoreN n) <*> toCoreT t+++-- Name -------------------------------------------------------------------------------------------+toCoreN :: S.Name -> C.Name+toCoreN nn+ = case nn of+        S.NameVar str+         -> C.NameVar str++        S.NameCon str+         -> C.NameCon str++        S.NamePrim (S.PrimNameType (S.PrimTypeTyConTetra tc))+         -> C.NameTyConTetra (toCoreTyConTetra tc)++        S.NamePrim (S.PrimNameType (S.PrimTypeTyCon p))+         -> C.NamePrimTyCon  p++        S.NamePrim (S.PrimNameVal (S.PrimValLit lit))+         -> case lit of+                S.PrimLitBool    x   -> C.NameLitBool    x+                S.PrimLitNat     x   -> C.NameLitNat     x+                S.PrimLitInt     x   -> C.NameLitInt     x+                S.PrimLitSize    x   -> C.NameLitSize    x+                S.PrimLitWord    x s -> C.NameLitWord    x s+                S.PrimLitFloat   x s -> C.NameLitFloat   x s+                S.PrimLitTextLit x   -> C.NameLitTextLit x++        S.NamePrim (S.PrimNameVal (S.PrimValArith p))+         -> C.NamePrimArith p False++        S.NamePrim (S.PrimNameVal (S.PrimValVector p))+         -> C.NameOpVector  p False++        S.NamePrim (S.PrimNameVal (S.PrimValFun   p))+         -> C.NameOpFun     p++        S.NamePrim (S.PrimNameVal (S.PrimValError p))+         -> C.NameOpError   p False++        S.NameHole+         -> C.NameHole+++-- | Convert a Tetra specific type constructor to core.+toCoreTyConTetra :: S.PrimTyConTetra -> C.TyConTetra+toCoreTyConTetra tc+ = case tc of+        S.PrimTyConTetraTuple n -> C.TyConTetraTuple n+        S.PrimTyConTetraVector  -> C.TyConTetraVector+        S.PrimTyConTetraF       -> C.TyConTetraF+        S.PrimTyConTetraC       -> C.TyConTetraC+        S.PrimTyConTetraU       -> C.TyConTetraU+

@@ -0,0 +1,27 @@++module DDC.Source.Tetra.Convert.Error+        (ErrorConvert (..))+where+import DDC.Source.Tetra.Pretty+import qualified DDC.Source.Tetra.Exp.Annot   as S+++data ErrorConvert a+        -- | Cannot convert sugar expression to core.+        = ErrorConvertCannotConvertSugarExp  (S.Exp a)++        -- | Cannot convert sugar let bindings to core.+        | ErrorConvertCannotConvertSugarLets (S.Lets a)+++instance Pretty a => Pretty (ErrorConvert a) where+ ppr err+  = case err of+        ErrorConvertCannotConvertSugarExp xx+         -> vcat [ text "Cannot desugar expression"+                 , indent 2 $ ppr xx ]++        ErrorConvertCannotConvertSugarLets xx+         -> vcat [ text "Cannot desugar let-bindings"+                 , indent 2 $ ppr xx ]+

@@ -1,4 +1,5 @@ +-- | Source Tetra data type definitions. module DDC.Source.Tetra.DataDef         ( -- * Data Type Definition.           DataDef  (..)@@ -29,9 +30,11 @@         , dataDefCtors          :: [DataCtor n] }         deriving Show -instance NFData (DataDef n) +instance NFData (DataDef n) where+ rnf !_ = () + -- | Take the types of data constructors from a data type definition. typeEnvOfDataDef :: Ord n => DataDef n -> TypeEnv n typeEnvOfDataDef def @@ -56,7 +59,8 @@         deriving Show  -instance NFData (DataCtor n)+instance NFData (DataCtor n) where+ rnf !_ = ()   -- | Get the type of a data constructor.

@@ -1,10 +1,21 @@ +-- | Source Tetra primitive type and kind environments. module DDC.Source.Tetra.Env-        ( primKindEnv-        , primTypeEnv )+        ( -- * Primitive kind environment.+          primKindEnv+        , kindOfPrimName++          -- * Primitive type environment.+        , primTypeEnv +        , typeOfPrimName+        , typeOfPrimVal+        , typeOfPrimLit++        , dataDefBool) where import DDC.Source.Tetra.Prim import DDC.Source.Tetra.Exp+import DDC.Type.DataDef import DDC.Type.Env             (Env) import qualified DDC.Type.Env   as Env @@ -22,7 +33,7 @@ kindOfPrimName :: Name -> Maybe (Kind Name) kindOfPrimName nn  = case nn of-        NamePrimTyCon tc        -> Just $ kindPrimTyCon tc+        NameTyCon tc            -> Just $ kindPrimTyCon tc         _                       -> Nothing  @@ -35,13 +46,41 @@ -- | Take the type of a name, --   or `Nothing` if this is not a value name. typeOfPrimName :: Name -> Maybe (Type Name)-typeOfPrimName dc+typeOfPrimName nn+ = case nn of+        NameVal n       -> Just $ typeOfPrimVal n+        _               -> Nothing+++-- | Take the type of a primitive name.+typeOfPrimVal  :: PrimVal -> Type Name+typeOfPrimVal dc  = case dc of-        NamePrimArith   p       -> Just $ typePrimArith p+        PrimValLit    l         -> typeOfPrimLit l+        PrimValArith  p         -> typePrimArith p+        PrimValError  p         -> typeOpError   p+        PrimValVector p         -> typeOpVector  p+        PrimValFun    p         -> typeOpFun     p -        NameLitBool     _       -> Just $ tBool-        NameLitNat      _       -> Just $ tNat-        NameLitInt      _       -> Just $ tInt-        NameLitWord     _ bits  -> Just $ tWord bits -        _                       -> Nothing+-- | Take the type of a primitive literal.+typeOfPrimLit   :: PrimLit -> Type Name+typeOfPrimLit pl+ = case pl of+        PrimLitBool     _       -> tBool+        PrimLitNat      _       -> tNat+        PrimLitInt      _       -> tInt+        PrimLitSize     _       -> tSize+        PrimLitFloat    _ bits  -> tFloat bits+        PrimLitWord     _ bits  -> tWord  bits+        PrimLitTextLit  _       -> tTextLit+++-- | Data type definition for `Bool`.+dataDefBool :: DataDef Name+dataDefBool+ = makeDataDefAlg (NameTyCon PrimTyConBool) +        [] +        (Just   [ (NameLitBool True,  []) +                , (NameLitBool False, []) ])+

@@ -1,23 +1,31 @@ +-- | Definition of Source Tetra Expressions. module DDC.Source.Tetra.Exp         ( module DDC.Type.Exp          -- * Expressions-        , Exp           (..)-        , Lets          (..)-        , Alt           (..)-        , Pat           (..)-        , Cast          (..)+        , GName+        , GAnnot+        , GBind+        , GBound+        , GPrim+        , GExp          (..)+        , GLets         (..)+        , GAlt          (..)+        , GPat          (..)+        , GClause       (..)+        , GGuardedExp   (..)+        , GGuard        (..)+        , GCast         (..)+        , DaCon         (..)          -- * Witnesses-        , Witness       (..)--        -- * Data Constructors-        , DaCon         (..)+        , GWitness      (..)+        , GWiCon        (..) -        -- * Witness Constructors-        , WiCon         (..)-        , WbCon         (..))+        -- * Dictionaries+        , ShowLanguage+        , NFDataLanguage) where import DDC.Type.Exp-import DDC.Source.Tetra.Exp.Base+import DDC.Source.Tetra.Exp.Generic

@@ -0,0 +1,54 @@+{-# LANGUAGE TypeFamilies #-}+module DDC.Source.Tetra.Exp.Annot+        ( module DDC.Source.Tetra.Exp.Generic+        , Annot+        , HasAnonBind   (..)++        -- * Expressions+        , Name       +        , Bound+        , Bind+        , Exp        +        , Lets       +        , Alt        +        , Pat        +        , Clause     +        , GuardedExp +        , Guard      +        , Cast+        , DaCon         (..)++        -- * Witnesses+        , Witness+        , WiCon)+where+import DDC.Source.Tetra.Exp.Generic+import DDC.Source.Tetra.Prim+import qualified DDC.Type.Exp           as T+++-- | Type index for annotated expression type.+data Annot a++instance HasAnonBind (Annot a) where+ isAnon _ (T.BAnon _)   = True+ isAnon _ _             = False++type instance GName  (Annot a) = Name+type instance GAnnot (Annot a) = a+type instance GBind  (Annot a) = T.Bind  Name+type instance GBound (Annot a) = T.Bound Name+type instance GPrim  (Annot a) = PrimVal++type Bound              = T.Bound Name+type Bind               = T.Bind  Name+type Exp        a       = GExp          (Annot a)+type Lets       a       = GLets         (Annot a)+type Alt        a       = GAlt          (Annot a)+type Pat        a       = GPat          (Annot a)+type Clause     a       = GClause       (Annot a)+type GuardedExp a       = GGuardedExp   (Annot a)+type Guard      a       = GGuard        (Annot a)+type Cast       a       = GCast         (Annot a)+type Witness    a       = GWitness      (Annot a)+type WiCon      a       = GWiCon        (Annot a)

@@ -1,168 +0,0 @@--module DDC.Source.Tetra.Exp.Base-        ( module DDC.Type.Exp--        -- * Expressions-        , Exp           (..)-        , Lets          (..)-        , Alt           (..)-        , Pat           (..)-        , Cast          (..)--        -- * Witnesses-        , Witness       (..)--        -- * Data Constructors-        , DaCon         (..)--        -- * Witness Constructors-        , WiCon         (..)-        , WbCon         (..))-where-import DDC.Type.Exp-import DDC.Type.Sum     ()-import Control.DeepSeq-import DDC.Core.Exp     -        ( Witness       (..)-        , WiCon         (..)-        , WbCon         (..)-        , Pat           (..)-        , DaCon         (..))----- | Well-typed expressions have types of kind `Data`.-data Exp a n-        ----------------------------------------------------        -- Core Language Constructs.-        --   These are also in the core language, and after desugaring only-        --   these constructs are used.-        ---        -- | Value variable   or primitive operation.-        = XVar      !a !(Bound n)--        -- | Data constructor or literal.-        | XCon      !a !(DaCon n)--        -- | Type abstraction (level-1).-        | XLAM      !a !(Bind n)   !(Exp a n)--        -- | Value and Witness abstraction (level-0).-        | XLam      !a !(Bind n)   !(Exp a n)--        -- | Application.-        | XApp      !a !(Exp a n)  !(Exp a n)--        -- | Possibly recursive bindings.-        | XLet      !a !(Lets a n) !(Exp a n)--        -- | Case branching.-        | XCase     !a !(Exp a n)  ![Alt a n]--        -- | Type cast.-        | XCast     !a !(Cast a n) !(Exp a n)--        -- | Type can appear as the argument of an application.-        | XType     !a !(Type n)--        -- | Witness can appear as the argument of an application.-        | XWitness  !a !(Witness a n)---        ----------------------------------------------------        -- Sugar Constructs.-        --  These constructs are eliminated by the desugarer.-        ---        -- | Some expressions and infix operators that need to be resolved into-        --   proper function applications.-        | XDefix    !a [Exp a n]--        -- | Use of a naked infix operator, like in 1 + 2.-        --   INVARIANT: only appears in the list of an XDefix node.-        | XInfixOp  !a String--        -- | Use of an infix operator as a plain variable, like in (+) 1 2.-        --   INVARIANT: only appears in the list of an XDefix node.-        | XInfixVar !a String-        deriving (Show, Eq)----- | Possibly recursive bindings.-data Lets a n-        -- | Non-recursive let-binding.-        = LLet     !(Bind n) !(Exp a n)--        -- | Recursive let bindings.-        | LRec     ![(Bind n, Exp a n)]--        -- | Bind a local region variable,-        --   and witnesses to its properties.-        | LPrivate ![Bind n] !(Maybe (Type n)) ![Bind n]-        deriving (Show, Eq)----- | Case alternatives.-data Alt a n-        = AAlt !(Pat n) !(Exp a n)-        deriving (Show, Eq)----- | Type casts.-data Cast a n-        -- | Weaken the effect of an expression.-        --   The given effect is added to the effect-        --   of the body.-        = CastWeakenEffect  !(Effect n)-        -        -- | Purify the effect (action) of an expression.-        | CastPurify !(Witness a n)--        -- | Box a computation, -        --   capturing its effects in the S computation type.-        | CastBox--        -- | Run a computation,-        --   releasing its effects into the environment.-        | CastRun-        deriving (Show, Eq)--        --- NFData ----------------------------------------------------------------------instance (NFData a, NFData n) => NFData (Exp a n) where- rnf xx-  = case xx of-        XVar      a u      -> rnf a `seq` rnf u-        XCon      a dc     -> rnf a `seq` rnf dc-        XLAM      a b x    -> rnf a `seq` rnf b   `seq` rnf x-        XLam      a b x    -> rnf a `seq` rnf b   `seq` rnf x-        XApp      a x1 x2  -> rnf a `seq` rnf x1  `seq` rnf x2-        XLet      a lts x  -> rnf a `seq` rnf lts `seq` rnf x-        XCase     a x alts -> rnf a `seq` rnf x   `seq` rnf alts-        XCast     a c x    -> rnf a `seq` rnf c   `seq` rnf x-        XType     a t      -> rnf a `seq` rnf t-        XWitness  a w      -> rnf a `seq` rnf w-        XDefix    a xs     -> rnf a `seq` rnf xs-        XInfixOp  a s      -> rnf a `seq` rnf s-        XInfixVar a s      -> rnf a `seq` rnf s---instance (NFData a, NFData n) => NFData (Cast a n) where- rnf cc-  = case cc of-        CastWeakenEffect e      -> rnf e-        CastPurify w            -> rnf w-        CastBox                 -> ()-        CastRun                 -> ()---instance (NFData a, NFData n) => NFData (Lets a n) where- rnf lts-  = case lts of-        LLet b x                -> rnf b `seq` rnf x-        LRec bxs                -> rnf bxs-        LPrivate bs1 mR bs2     -> rnf bs1  `seq` rnf mR `seq` rnf bs2---instance (NFData a, NFData n) => NFData (Alt a n) where- rnf aa-  = case aa of-        AAlt w x                -> rnf w `seq` rnf x

@@ -0,0 +1,322 @@+{-# LANGUAGE TypeFamilies, UndecidableInstances #-}++-- | Abstract syntax for Tetra Source expressions.+module DDC.Source.Tetra.Exp.Generic+        ( -- * Classes+          HasAnonBind   (..)++          -- * Expressions+        , GName+        , GAnnot+        , GBind+        , GBound+        , GPrim+        , GExp          (..)+        , GLets         (..)+        , GAlt          (..)+        , GPat          (..)+        , GClause       (..)+        , GGuardedExp   (..)+        , GGuard        (..)+        , GCast         (..)+        , DaCon         (..)++          -- * Witnesses+        , GWitness      (..)+        , GWiCon        (..)++          -- * Dictionaries+        , ShowLanguage+        , NFDataLanguage)+where+import DDC.Type.Exp     +import qualified DDC.Type.Exp           as T+import DDC.Type.Sum                     ()+import Control.DeepSeq+import DDC.Core.Exp+        ( DaCon         (..))+++---------------------------------------------------------------------------------------------------+-- | Type functions associated with the language AST.+type family GName  l+type family GAnnot l+type family GBind  l+type family GBound l+type family GPrim  l++class HasAnonBind l where+ isAnon :: l -> GBind l -> Bool+++---------------------------------------------------------------------------------------------------+-- | Well-typed expressions have types of kind `Data`.+data GExp l+        ---------------------------------------------------+        -- Core Language Constructs.+        --   These are also in the core language, and after desugaring only+        --   these constructs are used.+        --+        -- | Value variable   or primitive operation.+        = XVar      !(GAnnot l) !(GBound l)++        -- | Primitive values.+        | XPrim     !(GAnnot l) !(GPrim  l)++        -- | Data constructor or literal.+        | XCon      !(GAnnot l) !(DaCon (GName l))++        -- | Type abstraction (level-1).+        | XLAM      !(GAnnot l) !(GBind l) !(GExp l)++        -- | Value and Witness abstraction (level-0).+        | XLam      !(GAnnot l) !(GBind l) !(GExp l)++        -- | Application.+        | XApp      !(GAnnot l) !(GExp  l) !(GExp l)++        -- | A non-recursive let-binding.+        | XLet      !(GAnnot l) !(GLets l) !(GExp l)++        -- | Case branching.+        | XCase     !(GAnnot l) !(GExp  l) ![GAlt l]++        -- | Type cast.+        | XCast     !(GAnnot l) !(GCast l) !(GExp l)++        -- | Type can appear as the argument of an application.+        | XType     !(GAnnot l) !(Type  (GName l))++        -- | Witness can appear as the argument of an application.+        | XWitness  !(GAnnot l) !(GWitness l)+++        ---------------------------------------------------+        -- Sugar Constructs.+        --  These constructs are eliminated by the desugarer.+        --+        -- | Some expressions and infix operators that need to be resolved into+        --   proper function applications.+        | XDefix    !(GAnnot l) [GExp l]++        -- | Use of a naked infix operator, like in 1 + 2.+        --   INVARIANT: only appears in the list of an XDefix node.+        | XInfixOp  !(GAnnot l) String++        -- | Use of an infix operator as a plain variable, like in (+) 1 2.+        --   INVARIANT: only appears in the list of an XDefix node.+        | XInfixVar !(GAnnot l) String+++-- | Possibly recursive bindings.+--   Whether these are taken as recursive depends on whether they appear+--   in an XLet or XLetrec group.+data GLets l+        ---------------------------------------------------+        -- Core Language Constructs+        -- | Non-recursive expression binding.+        = LLet     !(GBind l) !(GExp l)++        -- | Recursive binding of lambda abstractions.+        | LRec     ![(GBind l, GExp l)]++        -- | Bind a local region variable,+        --   and witnesses to its properties.+        | LPrivate ![GBind l] !(Maybe (Type (GName l))) ![GBind l]++        ---------------------------------------------------+        -- Sugar Constructs+        -- | A possibly recursive group of binding clauses.+        -- +        --   Multiple clauses in the group may be part of the same function.+        | LGroup   ![GClause l]+++-- | Binding clause+data GClause l+        -- | A separate type signature.+        = SSig   !(GAnnot l) !(GBind l) !(Type (GName l))++        -- | A function binding using pattern matching and guards.+        | SLet   !(GAnnot l) !(GBind l) ![GPat l]  ![GGuardedExp l]+++-- | Case alternatives.+data GAlt l+        = AAlt   !(GPat l) ![GGuardedExp l]+++-- | Patterns.+data GPat l+        -- | The default pattern always succeeds.+        = PDefault++        -- | Match a data constructor and bind its arguments.+        | PData !(DaCon (GName l)) ![GBind l]+++-- | An expression with some guards.+data GGuardedExp l+        = GGuard !(GGuard l) !(GGuardedExp l)+        | GExp   !(GExp   l)+++-- | Expression guards.+data GGuard l+        = GPat  !(GPat l) !(GExp l)+        | GPred !(GExp l)+        | GDefault+++-- | Type casts.+data GCast l+        -- | Weaken the effect of an expression.+        --   The given effect is added to the effect+        --   of the body.+        = CastWeakenEffect  !(Effect (GName l))+        +        -- | Purify the effect (action) of an expression.+        | CastPurify !(GWitness l)++        -- | Box a computation, +        --   capturing its effects in the S computation type.+        | CastBox++        -- | Run a computation,+        --   releasing its effects into the environment.+        | CastRun+++-- | Witnesses.+data GWitness l+        -- | Witness variable.+        = WVar  !(GAnnot l) !(GBound l)++        -- | Witness constructor.+        | WCon  !(GAnnot l) !(GWiCon l)++        -- | Witness application.+        | WApp  !(GAnnot l) !(GWitness l) !(GWitness l)++        -- | Type can appear as an argument of a witness application.+        | WType !(GAnnot l) !(T.Type (GName l))+++-- | Witness constructors.+data GWiCon l+        -- | Witness constructors defined in the environment.+        --   In the interpreter we use this to hold runtime capabilities.+        --   The attached type must be closed.+        = WiConBound   !(GBound l) !(T.Type (GName l))+++---------------------------------------------------------------------------------------------------+type ShowLanguage l+        = ( Show l+          , Show (GName l), Show (GAnnot l)+          , Show (GBind l), Show (GBound l), Show (GPrim l))++deriving instance ShowLanguage l => Show (GExp        l)+deriving instance ShowLanguage l => Show (GLets       l)+deriving instance ShowLanguage l => Show (GClause     l)+deriving instance ShowLanguage l => Show (GAlt        l)+deriving instance ShowLanguage l => Show (GGuardedExp l)+deriving instance ShowLanguage l => Show (GGuard      l)+deriving instance ShowLanguage l => Show (GPat        l)+deriving instance ShowLanguage l => Show (GCast       l)+deriving instance ShowLanguage l => Show (GWitness    l)+deriving instance ShowLanguage l => Show (GWiCon      l)+++---------------------------------------------------------------------------------------------------+type NFDataLanguage l+        = ( NFData l+          , NFData (GAnnot l), NFData (GName l)+          , NFData (GBind l),  NFData (GBound l), NFData (GPrim l))++instance NFDataLanguage l => NFData (GExp l) where+ rnf xx+  = case xx of+        XVar      a u           -> rnf a `seq` rnf u+        XPrim     a p           -> rnf a `seq` rnf p+        XCon      a dc          -> rnf a `seq` rnf dc+        XLAM      a b x         -> rnf a `seq` rnf b   `seq` rnf x+        XLam      a b x         -> rnf a `seq` rnf b   `seq` rnf x+        XApp      a x1 x2       -> rnf a `seq` rnf x1  `seq` rnf x2+        XLet      a lts x       -> rnf a `seq` rnf lts `seq` rnf x+        XCase     a x alts      -> rnf a `seq` rnf x   `seq` rnf alts+        XCast     a c x         -> rnf a `seq` rnf c   `seq` rnf x+        XType     a t           -> rnf a `seq` rnf t+        XWitness  a w           -> rnf a `seq` rnf w+        XDefix    a xs          -> rnf a `seq` rnf xs+        XInfixOp  a s           -> rnf a `seq` rnf s+        XInfixVar a s           -> rnf a `seq` rnf s+++instance NFDataLanguage l => NFData (GClause l) where+ rnf cc+  = case cc of+        SSig a b t              -> rnf a `seq` rnf b `seq` rnf t+        SLet a b ps gxs         -> rnf a `seq` rnf b `seq` rnf ps `seq` rnf gxs+++instance NFDataLanguage l => NFData (GLets l) where+ rnf lts+  = case lts of+        LLet b x                -> rnf b `seq` rnf x+        LRec bxs                -> rnf bxs+        LPrivate bs1 mR bs2     -> rnf bs1  `seq` rnf mR `seq` rnf bs2+        LGroup cs               -> rnf cs+++instance NFDataLanguage l => NFData (GAlt l) where+ rnf aa+  = case aa of+        AAlt w gxs              -> rnf w `seq` rnf gxs+++instance NFDataLanguage l => NFData (GPat l) where+ rnf pp+  = case pp of+        PDefault                -> ()+        PData dc bs             -> rnf dc `seq` rnf bs+++instance NFDataLanguage l => NFData (GGuardedExp l) where+ rnf gx+  = case gx of+        GGuard g gx'            -> rnf g `seq` rnf gx'+        GExp x                  -> rnf x+++instance NFDataLanguage l => NFData (GGuard l) where+ rnf gg+  = case gg of+        GPred x                 -> rnf x+        GPat  p x               -> rnf p `seq` rnf x+        GDefault                -> ()+++instance NFDataLanguage l => NFData (GCast l) where+ rnf cc+  = case cc of+        CastWeakenEffect e      -> rnf e+        CastPurify w            -> rnf w+        CastBox                 -> ()+        CastRun                 -> ()+++instance NFDataLanguage l => NFData (GWitness l) where+ rnf ww+  = case ww of+        WVar  a u               -> rnf a `seq` rnf u+        WCon  a c               -> rnf a `seq` rnf c+        WApp  a w1 w2           -> rnf a `seq` rnf w1 `seq` rnf w2+        WType a t               -> rnf a `seq` rnf t+++instance NFDataLanguage l => NFData (GWiCon l) where+ rnf wc+  = case wc of+        WiConBound u t          -> rnf u `seq` rnf t+

@@ -1,4 +1,5 @@ +-- | Lexer for Source Tetra tokens. module DDC.Source.Tetra.Lexer         (lexModuleString) where@@ -10,10 +11,16 @@ -- | Lex a string to tokens, using primitive names. -- --   The first argument gives the starting source line number.+--+--   We're currently re-using the lexer for the core language, which has+--   *mostly* the same lexical structure as Source Tetra.+--   There are a few tokens accepted by one language but not the other,+--   but it'll do for now.+-- lexModuleString :: String -> Int -> String -> [Token (Tok Name)] lexModuleString sourceName lineStart str  = map rn $ lexModuleWithOffside sourceName lineStart str- where rn (Token strTok sp) + where rn (Token strTok sp)         = case renameTok readName strTok of                 Just t' -> Token t' sp-                Nothing -> Token (KJunk "lexical error") sp+                Nothing -> Token (KErrorJunk "lexical error") sp

@@ -1,85 +0,0 @@--module DDC.Source.Tetra.Lexer.Lit-        ( readLitInteger-        , readLitNat-        , readLitInt-        , readLitWordOfBits)-where-import Data.List-import Data.Char----- | Read a signed integer.-readLitInteger :: String -> Maybe Integer-readLitInteger []       = Nothing-readLitInteger str@(c:cs)-        | '-'   <- c-        , all isDigit cs-        = Just $ read str--        | all isDigit str-        = Just $ read str-        -        | otherwise-        = Nothing-        ---- | Read a natural number like @1234@.-readLitNat :: String -> Maybe Integer-readLitNat str1-        | (ds, "")      <- span isDigit str1-        , not  $ null ds-        = Just $ read ds--        | otherwise-        = Nothing----- | Read an integer with an explicit format specifier like @1234i@.-readLitInt :: String -> Maybe Integer-readLitInt str1-        | '-' : str2    <- str1-        , (ds, "i")     <- span isDigit str2-        , not $ null ds-        = Just $ read ds--        | (ds, "i")     <- span isDigit str1-        , not $ null ds-        = Just $ read ds--        | otherwise-        = Nothing----- | Read a word with an explicit format speficier.-readLitWordOfBits :: String -> Maybe (Integer, Int)-readLitWordOfBits str1-        -- binary like 0b01001w32-        | Just str2     <- stripPrefix "0b" str1-        , (ds, str3)    <- span (\c -> c == '0' || c == '1') str2-        , not $ null ds-        , Just str4     <- stripPrefix "w" str3-        , (bs, "")      <- span isDigit str4-        , not $ null bs-        , bits          <- read bs-        , length ds     <= bits-        = Just (readBinary ds, bits)--        -- decimal like 1234w32-        | (ds, str2)    <- span isDigit str1-        , not $ null ds-        , Just str3     <- stripPrefix "w" str2-        , (bs, "")      <- span isDigit str3-        , not $ null bs-        = Just (read ds, read bs)--        | otherwise-        = Nothing----- | Read a binary string as a number.-readBinary :: (Num a, Read a) => String -> a-readBinary digits-        = foldl' (\ acc b -> if b then 2 * acc + 1 else 2 * acc) 0-        $ map (/= '0') digits-

@@ -1,10 +1,14 @@+{-# LANGUAGE UndecidableInstances #-} +-- | Definition of Source Tetra modules. module DDC.Source.Tetra.Module         ( -- * Modules           Module        (..)         , isMainModule         , ExportSource  (..)-        , ImportSource  (..)+        , ImportType    (..)+        , ImportCap     (..)+        , ImportValue   (..)            -- * Module Names         , QualName      (..)@@ -26,74 +30,79 @@         , ModuleName    (..)         , isMainModuleName         , ExportSource  (..)-        , ImportSource  (..))+        , ImportType    (..)+        , ImportCap     (..)+        , ImportValue   (..))           -- Module ----------------------------------------------------------------------data Module a n+data Module l         = Module         { -- | Name of this module           moduleName            :: !ModuleName            -- Exports ----------------------------           -- | Names of exported types  (level-1).-        , moduleExportTypes     :: [n]+        , moduleExportTypes     :: [GName l]            -- | Names of exported values (level-0).-        , moduleExportValues    :: [n]+        , moduleExportValues    :: [GName l]            -- Imports ----------------------------           -- | Imported modules.         , moduleImportModules   :: [ModuleName]            -- | Kinds of imported foreign types.-        , moduleImportTypes     :: [(n, ImportSource n)]+        , moduleImportTypes     :: [(GName l, ImportType  (GName l))] +          -- | Types of imported capabilities.+        , moduleImportCaps      :: [(GName l, ImportCap   (GName l))]+           -- | Types of imported foreign values.-        , moduleImportValues    :: [(n, ImportSource n)]+        , moduleImportValues    :: [(GName l, ImportValue (GName l))]            -- Local ------------------------------           -- | Top-level things-        , moduleTops            :: [Top a n] }-        deriving Show+        , moduleTops            :: [Top l] } +deriving instance ShowLanguage l => Show (Module l) -instance (NFData a, NFData n) => NFData (Module a n) where++instance NFDataLanguage l => NFData (Module l) where  rnf !mm-        =     rnf (moduleName mm)-        `seq` rnf (moduleExportTypes   mm)-        `seq` rnf (moduleExportValues  mm)-        `seq` rnf (moduleImportModules mm)-        `seq` rnf (moduleImportTypes   mm)-        `seq` rnf (moduleImportValues  mm)-        `seq` rnf (moduleTops          mm)+        =     rnf (moduleName           mm)+        `seq` rnf (moduleExportTypes    mm)+        `seq` rnf (moduleExportValues   mm)+        `seq` rnf (moduleImportModules  mm)+        `seq` rnf (moduleImportTypes    mm)+        `seq` rnf (moduleImportCaps     mm)+        `seq` rnf (moduleImportValues   mm)+        `seq` rnf (moduleTops           mm)           -- | Check if this is the `Main` module.-isMainModule :: Module a n -> Bool+isMainModule :: Module l -> Bool isMainModule mm-        = isMainModuleName-        $ moduleName mm+        = isMainModuleName $ moduleName mm   -- Top Level Thing -------------------------------------------------------------data Top a n-        -- | Top-level, possibly recursive binding.-        = TopBind a (Bind n) (Exp a n)+data Top l+        -- | Some top-level, possibly recursive clauses.+        = TopClause  +        { topAnnot      :: GAnnot l+        , topClause     :: GClause l }          -- | Data type definition.         | TopData -        { topAnnot      :: a-        , topDataDef    :: DataDef n }-        deriving Show+        { topAnnot      :: GAnnot l+        , topDataDef    :: DataDef (GName l) } +deriving instance ShowLanguage l => Show (Top l) -instance (NFData a, NFData n) => NFData (Top a n) where+instance NFDataLanguage l => NFData (Top l) where  rnf !top   = case top of-        TopBind a b x   -         -> rnf a `seq` rnf b  `seq` rnf x-                 -        TopData a def-         -> rnf a `seq` rnf def +        TopClause a c   -> rnf a `seq` rnf c+        TopData   a def -> rnf a `seq` rnf def 

@@ -1,7 +1,9 @@ +-- | Parser for the Source Tetra language. module DDC.Source.Tetra.Parser         ( Parser         , Context       (..)+        , context          -- * Modules         , pModule

@@ -0,0 +1,28 @@++module DDC.Source.Tetra.Parser.Atom+        ( pPrimValSP+        , pVarStringSP)+where+import DDC.Source.Tetra.Prim+import DDC.Core.Lexer.Tokens+import DDC.Base.Parser                  ((<?>), SourcePos)+import qualified DDC.Base.Parser        as P++import DDC.Core.Parser+        (Parser)+++-- | Parse a variable, with source position.+pPrimValSP :: Parser Name (PrimVal, SourcePos)+pPrimValSP =  P.pTokMaybeSP f+        <?> "a variable"+ where  f (KN (KVar (NameVal p)))      = Just p+        f _                            = Nothing+++-- | Parse a variable, with source position.+pVarStringSP :: Parser Name (String, SourcePos)+pVarStringSP =  P.pTokMaybeSP f+        <?> "a variable"+ where  f (KN (KVar (NameVar s)))       = Just s+        f _                             = Nothing

@@ -1,81 +1,108 @@ --- | Core language parser.+-- | Parser for Source Tetra expressions. module DDC.Source.Tetra.Parser.Exp-        ( pExp+        ( context+        , pExp         , pExpApp         , pExpAtom,     pExpAtomSP-        , pLetsSP,      pLetBinding+        , pLetsSP,      pClauseSP         , pType         , pTypeApp         , pTypeAtom) where-import DDC.Source.Tetra.Exp+import DDC.Source.Tetra.Transform.Guards+import DDC.Source.Tetra.Parser.Witness import DDC.Source.Tetra.Parser.Param+import DDC.Source.Tetra.Parser.Atom import DDC.Source.Tetra.Compounds+import DDC.Source.Tetra.Prim+import DDC.Source.Tetra.Exp.Annot+import DDC.Core.Lexer.Tokens+import Control.Monad.Except+import DDC.Base.Parser                  ((<?>), SourcePos(..))+import qualified DDC.Base.Parser        as P+import qualified DDC.Type.Exp           as T+import qualified DDC.Type.Compounds     as T+import qualified Data.Text              as Text  import DDC.Core.Parser         ( Parser-        , Context(..)+        , Context (..)         , pBinder-        , pWitness-        , pWitnessAtom         , pType         , pTypeAtom         , pTypeApp-        , pCon-        , pConSP-        , pLit-        , pLitSP+        , pCon,         pConSP+        , pLit,         pLitSP+        ,               pStringSP         , pIndexSP-        , pOpSP-        , pOpVarSP-        , pVarSP+        , pOpSP,        pOpVarSP         , pTok         , pTokSP)  -import DDC.Core.Lexer.Tokens-import DDC.Base.Parser                  ((<?>), SourcePos)-import qualified DDC.Base.Parser        as P-import qualified DDC.Type.Compounds     as T-import Control.Monad.Error+type SP = SourcePos +-- | Starting context for the parser.+--   Holds flags about what language features we should accept.+context :: Context Name+context = Context+        { contextTrackedEffects         = True+        , contextTrackedClosures        = True+        , contextFunctionalEffects      = False+        , contextFunctionalClosures     = False +        , contextMakeStringName         = Just (\_ tx -> NameLitTextLit tx) } + -- Exp ----------------------------------------------------------------------------------------------- | Parse a core language expression.-pExp    :: Ord n => Context -> Parser n (Exp SourcePos n)+-- | Parse a Tetra Source language expression.+pExp    :: Context Name -> Parser Name (Exp SP) pExp c  = P.choice+         -- Level-0 lambda abstractions-        -- \(x1 x2 ... : Type) (y1 y2 ... : Type) ... . Exp- [ do   sp      <- pTokSP KBackSlash+        --  \(x1 x2 ... : Type) (y1 y2 ... : Type) ... . Exp+        --  \x1 x2 : Type. Exp+ [ do   sp      <- P.choice [ pTokSP KLambda, pTokSP KBackSlash ] -        bs      <- liftM concat-                $  P.many1 -                $  do   pTok KRoundBra+        bs      <- P.choice+                [ fmap concat $ P.many1 +                   $ do pTok KRoundBra                         bs'     <- P.many1 pBinder                         pTok (KOp ":")                         t       <- pType c                         pTok KRoundKet                         return (map (\b -> T.makeBindFromBinder b t) bs') +                , do    bs'     <- P.many1 pBinder+                        pTok (KOp ":")+                        t       <- pType c+                        return (map (\b -> T.makeBindFromBinder b t) bs') +                ]+         pTok KDot         xBody   <- pExp c         return  $ foldr (XLam sp) xBody bs          -- Level-1 lambda abstractions.         -- /\(x1 x2 ... : Type) (y1 y2 ... : Type) ... . Exp- , do   sp      <- pTokSP KBigLambda+ , do   sp      <- P.choice [ pTokSP KBigLambda, pTokSP KBigLambdaSlash ] -        bs      <- liftM concat-                $  P.many1 -                $  do   pTok KRoundBra+        bs      <- P.choice+                [ fmap concat $ P.many1+                   $ do pTok KRoundBra                         bs'     <- P.many1 pBinder                         pTok (KOp ":")                         t       <- pType c                         pTok KRoundKet                         return (map (\b -> T.makeBindFromBinder b t) bs') +                , do    bs'     <- P.many1 pBinder+                        pTok (KOp ":")+                        t       <- pType c+                        return (map (\b -> T.makeBindFromBinder b t) bs')+                ]+         pTok KDot         xBody   <- pExp c         return  $ foldr (XLAM sp) xBody bs@@ -103,17 +130,25 @@         pTok KBraceKet         return  $ XCase sp x alts -        -- match Pat <- Exp else Exp in Exp-        --  Sugar for a case-expression.+        -- match { | EXP = EXP | EXP = EXP ... }+        --  Sugar for cascaded case expressions case-expression.  , do   sp      <- pTokSP KMatch-        p       <- pPat c-        pTok KArrowDashLeft+        pTok KBraceBra+        x       <- pMatchGuardsAsCase sp c+        pTok KBraceKet+        return x++ , do   -- if-then-else+        --  Sugar for a case-expression.+        sp      <- pTokSP KIf         x1      <- pExp c-        pTok KElse+        pTok KThen         x2      <- pExp c-        pTok KIn+        pTok KElse         x3      <- pExp c-        return  $ XCase sp x1 [AAlt p x3, AAlt PDefault x2]+        return  $ XCase sp x1 +                        [ AAlt pTrue    [GExp x2]+                        , AAlt PDefault [GExp x3]]          -- weakeff [Type] in Exp  , do   sp      <- pTokSP KWeakEff@@ -149,7 +184,7 @@   -- Applications.-pExpApp :: Ord n => Context -> Parser n (Exp SourcePos n)+pExpApp :: Context Name -> Parser Name (Exp SP) pExpApp c   = do  xps     <- liftM concat $ P.many1 (pArgSPs c)         let (xs, sps)   = unzip xps@@ -163,7 +198,7 @@   -- Comp, Witness or Spec arguments.-pArgSPs :: Ord n => Context -> Parser n [(Exp SourcePos n, SourcePos)]+pArgSPs :: Context Name -> Parser Name [(Exp SP, SP)] pArgSPs c  = P.choice         -- [Type]@@ -198,7 +233,7 @@   -- | Parse a variable, constructor or parenthesised expression.-pExpAtom   :: Ord n => Context -> Parser n (Exp SourcePos n)+pExpAtom   :: Context Name -> Parser Name (Exp SP) pExpAtom c  = do   (x, _) <- pExpAtomSP c         return x@@ -206,11 +241,7 @@  -- | Parse a variable, constructor or parenthesised expression, --   also returning source position.-pExpAtomSP -        :: Ord n -        => Context -        -> Parser n (Exp SourcePos n, SourcePos)-+pExpAtomSP :: Context Name -> Parser Name (Exp SP, SP) pExpAtomSP c  = P.choice  [      -- ( Exp2 )@@ -243,13 +274,23 @@  , do   (lit, sp)       <- pLitSP         return  (XCon sp (DaConPrim lit (T.tBot T.kData)), sp) + , do   (tx, sp)        <- pStringSP+        let Just mkString = contextMakeStringName c +        let lit           = mkString sp tx+        return  (XCon sp (DaConPrim lit (T.tBot T.kData)), sp)++        -- Primitive names.+ , do   (nPrim, sp)     <- pPrimValSP+        return  (XPrim sp nPrim, sp)++        -- Named variables.+ , do   (sVar,  sp)     <- pVarStringSP+        return  (XVar  sp (T.UName (NameVar sVar)), sp)+         -- Debruijn indices  , do   (i, sp)         <- pIndexSP-        return  (XVar sp (UIx   i), sp)+        return  (XVar  sp (T.UIx   i), sp) -        -- Variables- , do   (var, sp)       <- pVarSP-        return  (XVar sp (UName var), sp)  ]   <?> "a variable, constructor, or parenthesised type"@@ -257,17 +298,22 @@  -- Alternatives ----------------------------------------------------------------------------------- -- Case alternatives.-pAlt    :: Ord n => Context -> Parser n (Alt SourcePos n)+pAlt    :: Context Name -> Parser Name (Alt SP) pAlt c  = do   p       <- pPat c-        pTok KArrowDash-        x       <- pExp c-        return  $ AAlt p x+        P.choice+         [ do   -- Desugar case guards while we're here.+                spgxs     <- P.many1 (pGuardedExpSP c (pTokSP KArrowDash))+                let gxs  = map snd spgxs+                return  $ AAlt p gxs +                +         , do   pTok KArrowDash+                x       <- pExp c+                return  $ AAlt p [GExp x] ]   -- Patterns.-pPat    :: Ord n -        => Context -> Parser n (Pat n)+pPat    :: Context Name -> Parser Name (Pat SP) pPat c  = P.choice  [      -- Wildcard@@ -290,9 +336,7 @@  -- Binds in patterns can have no type annotation, -- or can have an annotation if the whole thing is in parens.-pBindPat -        :: Ord n -        => Context -> Parser n (Bind n)+pBindPat :: Context Name -> Parser Name Bind pBindPat c  = P.choice         -- Plain binder.@@ -309,22 +353,100 @@  ]  +-- Guards -----------------------------------------------------------------------------------------+-- | Parse some guards and auto-desugar them to a case-expression.+pBindGuardsAsCaseSP+        :: Context Name+        -> Parser Name (SP, Exp SP)++pBindGuardsAsCaseSP c+ = do   +        (sp, g) : spgs  +                <- P.many1 (pGuardedExpSP c (pTokSP KEquals))++        -- Desugar guards.+        -- If none match then raise a runtime error.+        let xx' = desugarGuards sp (g : map snd spgs)  +                $ xErrorDefault sp +                        (Text.pack    $ sourcePosSource sp) +                        (fromIntegral $ sourcePosLine   sp)++        return  (sp, xx')+++pMatchGuardsAsCase+        :: SP -> Context Name+        -> Parser Name (Exp SP)++pMatchGuardsAsCase sp c+ = do   gg      <- liftM (map snd)+                $  P.sepEndBy1  (pGuardedExpSP c (pTokSP KEquals)) +                                (pTok KSemiColon)++        -- Desugar guards.+        -- If none match then raise a runtime error.+        let xx' = desugarGuards sp gg+                $ xErrorDefault sp +                        (Text.pack    $ sourcePosSource sp) +                        (fromIntegral $ sourcePosLine   sp)++        return  xx'+++-- | An guarded expression,+--   like | EXP1 = EXP2.+pGuardedExpSP +        :: Context Name         -- ^ Parser context.+        -> Parser  Name SP      -- ^ Parser for char between and of guards and exp.+                                --   usually -> or =+        -> Parser  Name (SP, GuardedExp SP)++pGuardedExpSP c pTermSP+ = pGuardExp (pTokSP KBar)++ where  pGuardExp pSepSP+         = P.choice+         [ do   sp      <- pSepSP+                g       <- pGuard+                gx      <- liftM snd $ pGuardExp (pTokSP KComma)+                return  (sp, GGuard g gx)++         , do   sp      <- pTermSP+                x       <- pExp c+                return  (sp, GExp x) ]++        pGuard+         = P.choice +         [ P.try $+           do   p       <- pPat c+                pTok KArrowDashLeft+                x       <- pExp c+                return $ GPat p x++         , do   g       <- pExp c+                return $ GPred g+++         , do   pTok KOtherwise+                return GDefault ]++ -- Bindings ----------------------------------------------------------------------------------------pLetsSP :: Ord n -        => Context -> Parser n (Lets SourcePos n, SourcePos)+pLetsSP :: Context Name -> Parser Name (Lets SP, SP) pLetsSP c  = P.choice     [ -- non-recursive let       do sp       <- pTokSP KLet-         (b1, x1) <- pLetBinding c-         return (LLet b1 x1, sp)+         l        <- liftM fst $ pClauseSP c+         return (LGroup [l], sp)        -- recursive let     , do sp       <- pTokSP KLetRec          pTok KBraceBra-         lets     <- P.sepEndBy1 (pLetBinding c) (pTok KSemiColon)+         ls       <- liftM (map fst)+                  $  P.sepEndBy1 (pClauseSP c) (pTok KSemiColon)          pTok KBraceKet-         return (LRec lets, sp)+         return (LGroup ls, sp)        -- Private region binding.       --   private Binder+ (with { Binder : Type ... })? in Exp@@ -361,11 +483,9 @@     ]          -pLetWits -        :: Ord n -        => Context -        -> [Bind n] -> Maybe (Type n)-        -> Parser n (Lets SourcePos n)+pLetWits :: Context Name+         -> [Bind] -> Maybe (T.Type Name)+         -> Parser Name (Lets SP)  pLetWits c bs mParent  = P.choice @@ -380,7 +500,7 @@                          -- Ambient witness binding, used for capabilities.                       , do t    <- pTypeApp c-                           return  $ BNone t+                           return  $ T.BNone t                       ])                       (pTok KSemiColon)            pTok KBraceKet@@ -391,34 +511,26 @@   -- | A binding for let expression.-pLetBinding -        :: Ord n -        => Context-        -> Parser n ( Bind n-                    , Exp SourcePos n)-pLetBinding c+pClauseSP :: Context Name+          -> Parser Name (Clause SP, SP)++pClauseSP c  = do   b       <- pBinder          P.choice          [ do   -- Binding with full type signature.-                --  Binder : Type = Exp-                pTok (KOp ":")-                t       <- pType c-                pTok (KOp "=")-                xBody   <- pExp c--                return  $ (T.makeBindFromBinder b t, xBody) -+                sp         <- pTokSP (KOp ":")+                t          <- pType c+                (_, xBody) <- pBindGuardsAsCaseSP c+                return  ( SLet sp (T.makeBindFromBinder b t) [] [GExp xBody]+                        , sp)           , do   -- Non-function binding with no type signature.-                -- This form can't be used with letrec as we can't use it-                -- to build the full type sig for the let-bound variable.-                --   Binder = Exp-                pTok (KOp "=")+                sp      <- pTokSP KEquals                 xBody   <- pExp c                 let t   = T.tBot T.kData-                return  $ (T.makeBindFromBinder b t, xBody)-+                return  ( SLet sp (T.makeBindFromBinder b t) [] [GExp xBody]+                        , sp)           , do   -- Binding using function syntax.                 ps      <- liftM concat @@ -429,37 +541,38 @@                         -- We can make the full type sig for the let-bound variable.                         --   Binder Param1 Param2 .. ParamN : Type = Exp                         pTok (KOp ":")-                        tBody   <- pType c-                        sp      <- pTokSP (KOp "=")-                        xBody   <- pExp c+                        tBody       <- pType c+                        (sp, xBody) <- pBindGuardsAsCaseSP c                          let x   = expOfParams sp ps xBody                         let t   = funTypeOfParams c ps tBody-                        return  (T.makeBindFromBinder b t, x)+                        return  ( SLet sp (T.makeBindFromBinder b t) [] [GExp x]+                                , sp)                          -- Function syntax with no return type.                         -- We can't make the type sig for the let-bound variable,                         -- but we can create lambda abstractions with the given                          -- parameter types.                         --   Binder Param1 Param2 .. ParamN = Exp-                 , do   sp      <- pTokSP (KOp "=")-                        xBody   <- pExp c+                 , do   (sp, xBody) <- pBindGuardsAsCaseSP c                          let x   = expOfParams sp ps xBody                         let t   = T.tBot T.kData-                        return  (T.makeBindFromBinder b t, x) ]+                        return  ( SLet sp (T.makeBindFromBinder b t) [] [GExp x]+                                , sp)+                 ]          ]   -- Statements ------------------------------------------------------------------------------------- data Stmt n-        = StmtBind  SourcePos (Bind n) (Exp SourcePos n)-        | StmtMatch SourcePos (Pat n)  (Exp SourcePos n) (Exp SourcePos n)-        | StmtNone  SourcePos (Exp SourcePos n)+        = StmtBind  SP Bind (Exp SP)+        | StmtMatch SP (Pat SP) (Exp SP) (Exp SP)+        | StmtNone  SP (Exp SP)   -- | Parse a single statement.-pStmt :: Ord n => Context -> Parser n (Stmt n)+pStmt :: Context Name -> Parser Name (Stmt Name) pStmt c  = P.choice  [ -- Binder = Exp ;@@ -468,7 +581,7 @@    --      P.try $      do  br      <- pBinder-        sp      <- pTokSP (KOp "=")+        sp      <- pTokSP KEquals         x1      <- pExp c         let t   = T.tBot T.kData         let b   = T.makeBindFromBinder br t@@ -498,7 +611,7 @@   -- | Parse some statements.-pStmts :: Ord n => Context -> Parser n (Exp SourcePos n)+pStmts :: Context Name -> Parser Name (Exp SP) pStmts c  = do   stmts   <- P.sepEndBy1 (pStmt c) (pTok KSemiColon)         case makeStmts stmts of@@ -507,7 +620,7 @@   -- | Make an expression from some statements.-makeStmts :: [Stmt n] -> Maybe (Exp SourcePos n)+makeStmts :: [Stmt Name] -> Maybe (Exp SP) makeStmts ss  = case ss of         [StmtNone _ x]    @@ -515,7 +628,7 @@          StmtNone sp x1 : rest          | Just x2      <- makeStmts rest-         -> Just $ XLet sp (LLet (BNone (T.tBot T.kData)) x1) x2+         -> Just $ XLet sp (LLet (T.BNone (T.tBot T.kData)) x1) x2          StmtBind sp b x1 : rest          | Just x2      <- makeStmts rest@@ -524,8 +637,8 @@         StmtMatch sp p x1 x2 : rest          | Just x3      <- makeStmts rest          -> Just $ XCase sp x1 -                 [ AAlt p x3-                 , AAlt PDefault x2]+                 [ AAlt p        [GExp x3]+                 , AAlt PDefault [GExp x2] ]          _ -> Nothing 

@@ -1,4 +1,5 @@ +-- | Parser for Source Tetra modules. module DDC.Source.Tetra.Parser.Module         ( -- * Modules           pModule@@ -11,11 +12,14 @@ import DDC.Source.Tetra.Compounds import DDC.Source.Tetra.DataDef import DDC.Source.Tetra.Module-import DDC.Source.Tetra.Exp+import DDC.Source.Tetra.Prim+import DDC.Source.Tetra.Exp.Annot import DDC.Core.Lexer.Tokens import DDC.Base.Pretty import Control.Monad+import qualified DDC.Type.Exp           as T import qualified DDC.Base.Parser        as P+import DDC.Base.Parser                  ((<?>))  import DDC.Core.Parser         ( Parser@@ -25,15 +29,16 @@         , pVar         , pTok,         pTokSP) +type SP = P.SourcePos --- Module ---------------------------------------------------------------------++-- Module ----------------------------------------------------------------------------------------- -- | Parse a source tetra module.-pModule :: (Ord n, Pretty n) -        => Context-        -> Parser n (Module P.SourcePos n)+pModule :: Context Name -> Parser Name (Module (Annot SP)) pModule c- = do   _sp     <- pTokSP KModule-        name    <- pModuleName+ = do   +        _sp     <- pTokSP KModule+        name    <- pModuleName <?> "a module name"          -- export { VAR;+ }         tExports @@ -50,14 +55,21 @@         tImports          <- liftM concat $ P.many (pImportSpecs c) -        pTok KWhere-        pTok KBraceBra+        -- top-level declarations.+        tops    +         <- P.choice+            [do pTok KWhere+                pTok KBraceBra -        -- TOP;+-        tops    <- P.sepEndBy (pTop c) (pTok KSemiColon)+                -- TOP;++                tops    <- P.sepEndBy (pTop c) (pTok KSemiColon) -        pTok KBraceKet+                pTok KBraceKet+                return tops +            ,do return [] ]++         -- ISSUE #295: Check for duplicate exported names in module parser.         --  The names are added to a unique map, so later ones with the same         --  name will replace earlier ones.@@ -65,17 +77,15 @@                 { moduleName            = name                 , moduleExportTypes     = []                 , moduleExportValues    = tExports-                , moduleImportModules   = []+                , moduleImportModules   = [mn     | ImportModule mn  <- tImports]                 , moduleImportTypes     = [(n, s) | ImportType  n s  <- tImports]+                , moduleImportCaps      = [(n, s) | ImportCap   n s  <- tImports]                 , moduleImportValues    = [(n, s) | ImportValue n s  <- tImports]                 , moduleTops            = tops }   -- | Parse a type signature.-pTypeSig -        :: Ord n -        => Context -> Parser n (n, Type n)        -+pTypeSig :: Context Name -> Parser Name (Name, T.Type Name) pTypeSig c  = do   var     <- pVar         pTokSP (KOp ":")@@ -83,61 +93,94 @@         return  (var, t)  --------------------------------------------------------------------------------+--------------------------------------------------------------------------------------------------- -- | An imported foreign type or foreign value. data ImportSpec n-        = ImportType    n (ImportSource n)-        | ImportValue   n (ImportSource n)+        = ImportModule  ModuleName+        | ImportType    n (ImportType  n)+        | ImportCap     n (ImportCap   n)+        | ImportValue   n (ImportValue n)+        deriving Show           -- | Parse some import specs.-pImportSpecs-        :: (Ord n, Pretty n)-        => Context -> Parser n [ImportSpec n]-+pImportSpecs :: Context Name -> Parser Name [ImportSpec Name] pImportSpecs c  = do   pTok KImport-        pTok KForeign-        src    <- liftM (renderIndent . ppr) pName          P.choice-         [      -- imports foreign X type (NAME :: TYPE)+ -          do    pTok KType-                pTok KBraceBra+                -- import foreign ...+         [ do   pTok KForeign+                src    <- liftM (renderIndent . ppr) pName -                sigs <- P.sepEndBy1 (pImportType c src) (pTok KSemiColon)-                pTok KBraceKet-                return sigs+                P.choice+                 [      -- import foreign X type (NAME :: TYPE)+ +                  do    pTok KType+                        pTok KBraceBra -                -- imports foreign X value (NAME :: TYPE)+-         , do   pTok KValue-                pTok KBraceBra+                        sigs <- P.sepEndBy1 (pImportType c src) (pTok KSemiColon)+                        pTok KBraceKet+                        return sigs -                sigs <- P.sepEndBy1 (pImportValue c src) (pTok KSemiColon)+                        -- import foreign X capability (NAME :: TYPE)++                 , do   pTok KCapability+                        pTok KBraceBra++                        sigs <- P.sepEndBy1 (pImportCapability c src) (pTok KSemiColon)+                        pTok KBraceKet+                        return sigs++                        -- import foreign X value (NAME :: TYPE)++                 , do   pTok KValue+                        pTok KBraceBra++                        sigs <- P.sepEndBy1 (pImportValue c src) (pTok KSemiColon)+                        pTok KBraceKet+                        return sigs+                 ]++         , do   pTok KBraceBra+                names   <- P.sepEndBy1 pModuleName (pTok KSemiColon) +                                <?> "module names"                 pTok KBraceKet-                return sigs+                return  [ImportModule n | n <- names]          ]   -- | Parse a type import spec.-pImportType-        :: (Ord n, Pretty n)-        => Context -> String -> Parser n (ImportSpec n)+pImportType :: Context Name -> String -> Parser Name (ImportSpec Name) pImportType c src         | "abstract"    <- src         = do    n       <- pName                 pTokSP (KOp ":")                 k       <- pType c-                return  (ImportType n (ImportSourceAbstract k))+                return  (ImportType n (ImportTypeAbstract k)) +        | "boxed"        <- src+        = do    n       <- pName+                pTokSP (KOp ":")+                k       <- pType c+                return  (ImportType n (ImportTypeBoxed k))+         | otherwise         = P.unexpected "import mode for foreign type"  +-- | Parse a capability import.+pImportCapability :: Context Name -> String -> Parser Name (ImportSpec Name)+pImportCapability c src+        | "abstract"    <- src+        = do    n       <- pName+                pTokSP (KOp ":")+                t       <- pType c+                return  (ImportCap n (ImportCapAbstract t))++        | otherwise+        = P.unexpected "import mode for foreign capability"++ -- | Parse a value import spec.-pImportValue -        :: (Ord n, Pretty n)-        => Context -> String -> Parser n (ImportSpec n)+pImportValue :: Context Name -> String -> Parser Name (ImportSpec Name) pImportValue c src         | "c"           <- src         = do    n       <- pName@@ -148,32 +191,28 @@                 --             with foreign C imports and exports.                 let symbol = renderIndent (ppr n) -                return  (ImportValue n (ImportSourceSea symbol k))+                return  (ImportValue n (ImportValueSea symbol k))          | otherwise         = P.unexpected "import mode for foreign value"  --- Top Level ------------------------------------------------------------------pTop    :: Ord n -        => Context -> Parser n (Top P.SourcePos n)+-- Top Level --------------------------------------------------------------------------------------+pTop    :: Context Name -> Parser Name (Top (Annot SP)) pTop c  = P.choice  [ do   -- A top-level, possibly recursive binding.-        (b, x)          <- pLetBinding c-        let Just sp     = takeAnnotOfExp x-        return  $ TopBind sp b x+        (l, sp)         <- pClauseSP c+        return  $ TopClause sp l           -- A data type declaration  , do   pData c  ]  --- Data -----------------------------------------------------------------------+-- Data ------------------------------------------------------------------------------------------- -- | Parse a data type declaration.-pData   :: Ord n-        => Context -> Parser n (Top P.SourcePos n)-+pData   :: Context Name -> Parser Name (Top (Annot SP)) pData c  = do   sp      <- pTokSP KData         n       <- pName@@ -193,18 +232,18 @@   -- | Parse a type parameter to a data type.-pDataParam :: Ord n => Context -> Parser n [Bind n]+pDataParam :: Context Name -> Parser Name [Bind] pDataParam c   = do   pTok KRoundBra         ns      <- P.many1 pName         pTokSP (KOp ":")         k       <- pType c         pTok KRoundKet-        return  [BName n k | n <- ns]+        return  [T.BName n k | n <- ns]   -- | Parse a data constructor declaration.-pDataCtor :: Ord n => Context -> Parser n (DataCtor n)+pDataCtor :: Context Name -> Parser Name (DataCtor Name) pDataCtor c  = do   n       <- pName         pTokSP (KOp ":")

@@ -1,11 +1,12 @@ +-- | Desugaring of function parameter syntax in Source Tetra. module DDC.Source.Tetra.Parser.Param         ( ParamSpec     (..)         , funTypeOfParams         , pBindParamSpec         , expOfParams) where-import DDC.Source.Tetra.Exp+import DDC.Source.Tetra.Exp.Annot import DDC.Core.Parser         ( ParamSpec(..)         , funTypeOfParams@@ -16,9 +17,9 @@ --   and the expression for the body. expOfParams          :: a-        -> [ParamSpec n]        -- ^ Spec of parameters.-        -> Exp a n              -- ^ Body of function.-        -> Exp a n              -- ^ Expression of whole function.+        -> [ParamSpec Name]     -- ^ Spec of parameters.+        -> Exp a                -- ^ Body of function.+        -> Exp a                -- ^ Expression of whole function.  expOfParams _ [] xBody            = xBody expOfParams a (p:ps) xBody

@@ -0,0 +1,100 @@++module DDC.Source.Tetra.Parser.Witness+        ( pWitness+        , pWitnessApp+        , pWitnessAtom) +where+import DDC.Source.Tetra.Prim+import DDC.Source.Tetra.Exp.Annot+import DDC.Core.Parser+        ( Parser+        , Context (..)+        , pType+        , pConSP+        , pIndexSP+        , pVarSP+        , pTok+        , pTokSP)++import DDC.Core.Lexer.Tokens+import DDC.Base.Parser                  ((<?>), SourcePos)+import qualified DDC.Base.Parser        as P+import qualified DDC.Type.Exp           as T+import qualified DDC.Type.Compounds     as T+import Control.Monad.Except++type SP = SourcePos+++-- | Parse a witness expression.+pWitness      :: Context Name -> Parser Name (Witness SP)+pWitness c = pWitnessJoin c+++-- | Parse a witness join.+pWitnessJoin  :: Context Name -> Parser Name (Witness SP)+pWitnessJoin c+   -- WITNESS  or  WITNESS & WITNESS+ = do   w1      <- pWitnessApp c+        P.choice +         [ do   return w1 ]+++-- | Parse a witness application.+pWitnessApp   :: Context Name -> Parser Name (Witness SP)+pWitnessApp c+  = do  (x:xs)  <- P.many1 (pWitnessArgSP c)+        let x'  = fst x+        let sp  = snd x+        let xs' = map fst xs+        return  $ foldl (WApp sp) x' xs'++ <?> "a witness expression or application"+++-- | Parse a witness argument.+pWitnessArgSP :: Context Name -> Parser Name (Witness SP, SP)+pWitnessArgSP c+ = P.choice+ [ -- [TYPE]+   do   sp      <- pTokSP KSquareBra+        t       <- pType c+        pTok KSquareKet+        return  (WType sp t, sp)++   -- WITNESS+ , do   pWitnessAtomSP c ]++++-- | Parse a variable, constructor or parenthesised witness.+pWitnessAtom   :: Context Name -> Parser Name (Witness SP)+pWitnessAtom c   +        = liftM fst (pWitnessAtomSP c)+++-- | Parse a variable, constructor or parenthesised witness,+--   also returning source position.+pWitnessAtomSP :: Context Name -> Parser Name (Witness SP, SP)+pWitnessAtomSP c+ = P.choice+   -- (WITNESS)+ [ do   sp      <- pTokSP KRoundBra+        w       <- pWitness c+        pTok KRoundKet+        return  (w, sp)++   -- Named constructors+ , do   (con, sp) <- pConSP+        return  (WCon sp (WiConBound (T.UName con) (T.tBot T.kWitness)), sp)+                +   -- Debruijn indices+ , do   (i, sp) <- pIndexSP+        return  (WVar sp (T.UIx   i), sp)++   -- Variables+ , do   (var, sp) <- pVarSP+        return  (WVar sp (T.UName var), sp) ]++ <?> "a witness"+

@@ -1,4 +1,5 @@ +-- | Simple predicates on Source Tetra things. module DDC.Source.Tetra.Predicates         ( module DDC.Type.Predicates @@ -23,13 +24,13 @@           -- * Patterns         , isPDefault) where-import DDC.Source.Tetra.Exp+import DDC.Source.Tetra.Exp.Generic import DDC.Type.Predicates   -- Atoms ---------------------------------------------------------------------- -- | Check whether an expression is a variable.-isXVar :: Exp a n -> Bool+isXVar :: GExp l -> Bool isXVar xx  = case xx of         XVar{}  -> True@@ -37,7 +38,7 @@   -- | Check whether an expression is a constructor.-isXCon :: Exp a n -> Bool+isXCon :: GExp l -> Bool isXCon xx  = case xx of         XCon{}  -> True@@ -46,7 +47,7 @@  -- | Check whether an expression is a `XVar` or an `XCon`,  --   or some type or witness atom.-isAtomX :: Exp a n -> Bool+isAtomX :: GExp l -> Bool isAtomX xx  = case xx of         XVar{}          -> True@@ -57,7 +58,7 @@   -- | Check whether a witness is a `WVar` or `WCon`.-isAtomW :: Witness a n -> Bool+isAtomW :: GWitness l -> Bool isAtomW ww  = case ww of         WVar{}          -> True@@ -67,7 +68,7 @@  -- Lambdas -------------------------------------------------------------------- -- | Check whether an expression is a spec abstraction (level-1).-isXLAM :: Exp a n -> Bool+isXLAM :: GExp l -> Bool isXLAM xx  = case xx of         XLAM{}  -> True@@ -75,7 +76,7 @@   -- | Check whether an expression is a value or witness abstraction (level-0).-isXLam :: Exp a n -> Bool+isXLam :: GExp l -> Bool isXLam xx  = case xx of         XLam{}  -> True@@ -83,14 +84,14 @@   -- | Check whether an expression is a spec, value, or witness abstraction.-isLambdaX :: Exp a n -> Bool+isLambdaX :: GExp l -> Bool isLambdaX xx         = isXLAM xx || isXLam xx   -- Applications --------------------------------------------------------------- -- | Check whether an expression is an `XApp`.-isXApp :: Exp a n -> Bool+isXApp :: GExp l -> Bool isXApp xx  = case xx of         XApp{}  -> True@@ -99,7 +100,7 @@  -- Let Bindings --------------------------------------------------------------- -- | Check whether an expression is a `XLet`.-isXLet :: Exp a n -> Bool+isXLet :: GExp l -> Bool isXLet xx  = case xx of         XLet{}  -> True@@ -108,7 +109,7 @@  -- Type and Witness ----------------------------------------------------------- -- | Check whether an expression is an `XType`-isXType :: Exp a n -> Bool+isXType :: GExp l -> Bool isXType xx  = case xx of         XType{}         -> True@@ -116,7 +117,7 @@   -- | Check whether an expression is an `XWitness`-isXWitness :: Exp a n -> Bool+isXWitness :: GExp l -> Bool isXWitness xx  = case xx of         XWitness{}      -> True@@ -125,6 +126,7 @@  -- Patterns ------------------------------------------------------------------- -- | Check whether an alternative is a `PDefault`.-isPDefault :: Pat n -> Bool+isPDefault :: GPat l -> Bool isPDefault PDefault     = True isPDefault _            = False+

@@ -1,20 +1,28 @@+{-# LANGUAGE TypeFamilies, UndecidableInstances #-}  -- | Pretty printing for Tetra modules and expressions. module DDC.Source.Tetra.Pretty         ( module DDC.Core.Pretty-        , module DDC.Base.Pretty )+        , module DDC.Base.Pretty +        , PrettyLanguage) where-import DDC.Source.Tetra.Compounds import DDC.Source.Tetra.Predicates import DDC.Source.Tetra.DataDef import DDC.Source.Tetra.Module import DDC.Source.Tetra.Exp import DDC.Core.Pretty import DDC.Base.Pretty+import Prelude                  hiding ((<$>))  +type PrettyLanguage l +        = ( Eq     (GName l)+          , Pretty (GAnnot l), Pretty (GName l)+          , Pretty (GBound l), Pretty (GBind l), Pretty (GPrim l))++ -- Module ------------------------------------------------------------------------------------------instance (Pretty n, Eq n) => Pretty (Module a n) where+instance PrettyLanguage l => Pretty (Module l) where  ppr Module         { moduleName            = name         , moduleExportTypes     = _exportedTypes@@ -47,20 +55,15 @@   -- Top ---------------------------------------------------------------------------------------------instance (Pretty n, Eq n) => Pretty (Top a n) where- ppr (TopBind _ b x)-  = let dBind = if isBot (typeOfBind b)-                          then ppr (binderOfBind b)-                          else ppr b-    in  align (  dBind-                <> nest 2 ( breakWhen (not $ isSimpleX x)-                          <> text "=" <+> align (ppr x)))+instance PrettyLanguage l => Pretty (Top l) where+ ppr (TopClause _ c) = ppr c   ppr (TopData _ (DataDef name params ctors))-  = hsep-        (  [ text "data", ppr name]-        ++ [parens $ ppr b | b <- params]-        ++ [text "where" <+> lbrace])+  = (text "data"+        <+> hsep ( ppr name+                 : map (parens . ppr) params)+        <+> text "where"+        <+> lbrace)   <$> indent 8         (vcat [ ppr (dataCtorName ctor)                  <+> text ":" @@ -72,30 +75,28 @@   <> line   <> rbrace + -- Exp ---------------------------------------------------------------------------------------------instance (Pretty n, Eq n) => Pretty (Exp a n) where+instance PrettyLanguage l => Pretty (GExp l) where  pprPrec d xx   = {-# SCC "ppr[Exp]" #-}     case xx of         XVar  _ u       -> ppr u         XCon  _ dc      -> ppr dc+        XPrim _ u       -> ppr u         -        XLAM{}-         -> let Just (bs, xBody) = takeXLAMs xx-                groups = partitionBindsByType bs-            in  pprParen' (d > 1)-                 $  (cat $ map (pprBinderGroup (text "/\\")) groups)+        XLAM _ b xBody+         -> pprParen' (d > 1)+                 $   text "/\\" <>  ppr b <> text "."                  <>  (if      isXLAM    xBody then empty                       else if isXLam    xBody then line <> space                       else if isSimpleX xBody then space                       else    line)                  <>  ppr xBody -        XLam{}-         -> let Just (bs, xBody) = takeXLams xx-                groups = partitionBindsByType bs-            in  pprParen' (d > 1)-                 $  (cat $ map (pprBinderGroup (text "\\")) groups) +        XLam _ b xBody+         -> pprParen' (d > 1)+                 $  text "\\" <> ppr b <> text "."                  <> breakWhen (not $ isSimpleX xBody)                  <> ppr xBody @@ -110,14 +111,6 @@          $   ppr lts <+> text "in"          <$> ppr x -        XCase _ x1 [AAlt p x2]-         ->  pprParen' (d > 2)-         $   text "caselet" <+> ppr p -                <+> nest 2 (breakWhen (not $ isSimpleX x1)-                            <> text "=" <+> align (ppr x1))-                <+> text "in"-         <$> ppr x2-         XCase _ x alts          -> pprParen' (d > 2)           $  (nest 2 $ text "case" <+> ppr x <+> text "of" <+> lbrace <> line@@ -142,8 +135,7 @@         XWitness _ w    -> text "<" <> ppr w <> text ">"          XDefix _ xs-         -> pprParen' (d > 2)-         $  text "DEFIX" <+> hsep (map (pprPrec 11) xs)+         -> text "[" <> text "DEFIX|" <+> hsep (map (pprPrec 11) xs) <+> text "]"          XInfixOp _ str          -> parens $ text "INFIXOP"  <+> text "\"" <> text str <> text "\""@@ -152,46 +144,18 @@          -> parens $ text "INFIXVAR" <+> text "\"" <> text str <> text "\""  --- Alt ---------------------------------------------------------------------------------------------instance (Pretty n, Eq n) => Pretty (Alt a n) where- ppr (AAlt p x)-  = ppr p <+> nest 1 (line <> nest 3 (text "->" <+> ppr x))----- Cast --------------------------------------------------------------------------------------------instance (Pretty n, Eq n) => Pretty (Cast a n) where- ppr cc-  = case cc of-        CastWeakenEffect  eff   -         -> text "weakeff" <+> brackets (ppr eff)--        CastPurify w-         -> text "purify"  <+> angles   (ppr w)--        CastBox-         -> text "box"--        CastRun-         -> text "run"-- -- Lets --------------------------------------------------------------------------------------------instance (Pretty n, Eq n) => Pretty (Lets a n) where+instance PrettyLanguage l => Pretty (GLets l) where  ppr lts   = case lts of         LLet b x-         -> let dBind = if isBot (typeOfBind b)-                          then ppr (binderOfBind b)-                          else ppr b-            in  text "let"-                 <+> align (  dBind+         -> text "let"+                 <+> align (  ppr b                            <> nest 2 ( breakWhen (not $ isSimpleX x)                                      <> text "=" <+> align (ppr x)))         LRec bxs          -> let pprLetRecBind (b, x)-                 =   ppr (binderOfBind b)-                 <+> text ":"-                 <+> ppr (typeOfBind b)+                 =   ppr b                  <>  nest 2 (  breakWhen (not $ isSimpleX x)                             <> text "=" <+> align (ppr x))         @@ -204,11 +168,11 @@          LPrivate bs Nothing []          -> text "private"-                <+> (hcat $ punctuate space (map (ppr . binderOfBind) bs))+                <+> (hcat $ punctuate space (map ppr bs))                  LPrivate bs Nothing bsWit          -> text "private"-                <+> (hcat $ punctuate space (map (ppr . binderOfBind) bs))+                <+> (hcat $ punctuate space (map ppr bs))                 <+> text "with"                 <+> braces (cat $ punctuate (text "; ") $ map ppr bsWit) @@ -216,42 +180,107 @@          -> text "extend"                 <+> ppr parent                 <+> text "using"-                <+> (hcat $ punctuate space (map (ppr . binderOfBind) bs))+                <+> (hcat $ punctuate space (map ppr bs))          LPrivate bs (Just parent) bsWit          -> text "extend"                 <+> ppr parent                 <+> text "using"-                <+> (hcat $ punctuate space (map (ppr . binderOfBind) bs))+                <+> (hcat $ punctuate space (map ppr bs))                 <+> text "with"                 <+> braces (cat $ punctuate (text "; ") $ map ppr bsWit) +        LGroup cs+         -> vcat $ map ppr cs --- Binder ------------------------------------------------------------------------------------------pprBinder   :: Pretty n => Binder n -> Doc-pprBinder bb- = case bb of-        RName v         -> ppr v-        RAnon           -> text "^"-        RNone           -> text "_" +-- Clause -----------------------------------------------------------------------------------------+instance PrettyLanguage l => Pretty (GClause l) where+ ppr (SSig _ b t)+  = ppr b <+> text ":" <+> ppr t --- | Print a group of binders with the same type.-pprBinderGroup -        :: (Pretty n, Eq n) -        => Doc -> ([Binder n], Type n) -> Doc+ ppr (SLet _ b ps [GExp x])+  = ppr b       <+> hsep (map ppr ps) +                <>  nest 2 ( breakWhen (not $ isSimpleX x)+                           <> text "=" <+> align (ppr x)) -pprBinderGroup lam (rs, t)-        = lam <> parens ((hsep $ map pprBinder rs) <+> text ":" <+> ppr t) <> dot+ ppr (SLet _ b ps gxs)+  = ppr b       <+> hsep (map ppr ps) +                <>  nest 2 (line <> vcat (map (pprGuardedExp "=") gxs))  +-- Alt --------------------------------------------------------------------------------------------+instance PrettyLanguage l => Pretty (GAlt l) where+ ppr (AAlt p gxs)+  =  ppr p <> nest 2 (line <> vcat (map (pprGuardedExp "->") gxs))+++-- Pat --------------------------------------------------------------------------------------------+instance PrettyLanguage l => Pretty (GPat l) where+ ppr pp+  = case pp of+        PDefault        -> text "_"+        PData u bs      -> ppr u <+> sep (map ppr bs)+++-- GuardedExp -------------------------------------------------------------------------------------+pprGuardedExp :: PrettyLanguage l => String -> GGuardedExp l -> Doc+pprGuardedExp sTerm gx+  = pprGs "|" gx+  where+        pprGs _c (GExp x)+         = text sTerm <+> ppr x++        pprGs c (GGuard g gs)+         = pprG c g <> line <> pprGs "," gs++        pprG  c (GPat p x)+         = text c <+> ppr p  <+> text "<-" <+> ppr x++        pprG  c (GPred x)+         = text c <+> ppr x++        pprG  c GDefault+         = text c <+> text "otherwise"+        ++-- Guard ------------------------------------------------------------------------------------------+instance PrettyLanguage l => Pretty (GGuard l) where+++-- Cast -------------------------------------------------------------------------------------------+instance PrettyLanguage l => Pretty (GCast l) where+ ppr cc+  = case cc of+        CastWeakenEffect  eff -> text "weakeff" <+> brackets (ppr eff)+        CastPurify w    -> text "purify"  <+> angles   (ppr w)+        CastBox         -> text "box"+        CastRun         -> text "run"+++-- Witness ----------------------------------------------------------------------------------------+instance PrettyLanguage l => Pretty (GWitness l) where+ pprPrec d ww+  = case ww of+        WVar _ n        -> ppr n+        WCon _ wc       -> ppr wc+        WApp _ w1 w2    -> pprParen (d > 10) (ppr w1 <+> pprPrec 11 w2)+        WType _ t       -> text "[" <> ppr t <> text "]"+++instance PrettyLanguage l => Pretty (GWiCon l) where+ ppr wc+  = case wc of+        WiConBound   u  _ -> ppr u++ -- Utils ------------------------------------------------------------------------------------------ breakWhen :: Bool -> Doc breakWhen True   = line breakWhen False  = space  -isSimpleX :: Exp a n -> Bool+isSimpleX :: GExp l -> Bool isSimpleX xx  = case xx of         XVar{}          -> True

@@ -1,121 +1,294 @@ +-- | Definitions of Source Tetra primitive names and operators. module DDC.Source.Tetra.Prim-        ( Name          (..)-        , TyConTetra    (..)-        , kindTyConTetra+        ( -- * Names+          Name          (..) -        , OpStore       (..)-        , typeOpStore+          -- * Primitive Names+        , PrimName      (..)+        , pattern NameType+        , pattern NameVal+        , readName +          -- * Primitive Types+        , PrimType      (..)+        , pattern NameTyCon+        , pattern NameTyConTetra++          -- ** Primitive machine type constructors.         , PrimTyCon     (..)         , kindPrimTyCon         , tBool         , tNat         , tInt+        , tSize         , tWord+        , tFloat+        , tTextLit +          -- ** Primitive tetra type constructors.+        , PrimTyConTetra(..)+        , pattern NameTyConTetraTuple+        , pattern NameTyConTetraF+        , pattern NameTyConTetraC+        , pattern NameTyConTetraU+        , kindPrimTyConTetra++          -- * Primitive values+        , PrimVal (..)+        , pattern NameLit+        , pattern NameArith+        , pattern NameVector+        , pattern NameFun+        , pattern NameError++          -- ** Primitive arithmetic operators.         , PrimArith     (..)         , typePrimArith-        , readName)++          -- ** Primitive vector operators.+        , OpVector      (..)+        , typeOpVector++          -- ** Primitive function operators.+        , OpFun         (..)+        , typeOpFun++          -- ** Primitive error handling+        , OpError (..)+        , typeOpError++          -- ** Primitive literals+        , PrimLit (..)+        , pattern NameLitBool+        , pattern NameLitNat+        , pattern NameLitInt+        , pattern NameLitSize+        , pattern NameLitWord+        , pattern NameLitFloat+        , pattern NameLitTextLit) where-import DDC.Source.Tetra.Lexer.Lit import DDC.Source.Tetra.Prim.Base import DDC.Source.Tetra.Prim.TyConPrim import DDC.Source.Tetra.Prim.TyConTetra-import DDC.Source.Tetra.Prim.OpStore import DDC.Source.Tetra.Prim.OpArith+import DDC.Source.Tetra.Prim.OpFun+import DDC.Source.Tetra.Prim.OpVector+import DDC.Source.Tetra.Prim.OpError+import DDC.Core.Lexer.Names             (isVarStart) import DDC.Base.Pretty import Control.DeepSeq import Data.Char+import qualified Data.Text              as T  import DDC.Core.Tetra            ( readPrimTyCon-        , readPrimArith-        , readOpStore)+        , readPrimArithFlag+        , readOpFun+        , readOpErrorFlag+        , readOpVectorFlag) +import DDC.Core.Salt.Name+        ( readLitNat+        , readLitInt+        , readLitSize+        , readLitWordOfBits+        , readLitFloatOfBits) ++---------------------------------------------------------------------------------------------------+instance Pretty Name where+ ppr nn+  = case nn of+        NameVar  v              -> text v+        NameCon  c              -> text c+        NamePrim p              -> ppr p+        NameHole                -> text "?"++ instance NFData Name where  rnf nn   = case nn of         NameVar s               -> rnf s         NameCon s               -> rnf s+        NamePrim p              -> rnf p+        NameHole                -> () -        NameTyConTetra p        -> rnf p-        NameOpStore    p        -> rnf p-        NamePrimTyCon  p        -> rnf p-        NamePrimArith  p        -> rnf p -        NameLitBool b           -> rnf b-        NameLitNat  n           -> rnf n-        NameLitInt  i           -> rnf i-        NameLitWord i bits      -> rnf i `seq` rnf bits+-- | Read the name of a variable, constructor or literal.+readName :: String -> Maybe Name+readName str+        -- Primitive names.+        | Just n        <- readPrimName str+        = Just $ NamePrim n -        NameHole                -> ()+        -- Constructors.+        | c : _         <- str+        , isUpper c+        = Just $ NameCon str +        -- Variables.+        | c : _         <- str+        , isVarStart c      +        = Just $ NameVar str -instance Pretty Name where+        | otherwise+        = Nothing+++---------------------------------------------------------------------------------------------------+instance Pretty PrimName where  ppr nn   = case nn of-        NameVar  v              -> text v-        NameCon  c              -> text c+        PrimNameType p          -> ppr p+        PrimNameVal p           -> ppr p -        NameTyConTetra p        -> ppr p-        NameOpStore   p         -> ppr p-        NamePrimTyCon p         -> ppr p-        NamePrimArith p         -> ppr p -        NameLitBool True        -> text "True#"-        NameLitBool False       -> text "False#"-        NameLitNat  i           -> integer i-        NameLitInt  i           -> integer i <> text "i"-        NameLitWord i bits      -> integer i <> text "w" <> int bits+instance NFData PrimName where+ rnf nn+  = case nn of+        PrimNameType p          -> rnf p+        PrimNameVal p           -> rnf p -        NameHole                -> text "?" +readPrimName :: String -> Maybe PrimName+readPrimName str+        | Just t <- readPrimType str+        = Just $ PrimNameType t --- | Read the name of a variable, constructor or literal.-readName :: String -> Maybe Name-readName str-        -- Baked-in names-        | Just p <- readTyConTetra   str  -        = Just $ NameTyConTetra p+        | Just v <- readPrimVal str+        = Just $ PrimNameVal  v -        | Just p <- readOpStore   str  -        = Just $ NameOpStore   p+        | otherwise+        = Nothing -        -- Primitive names.-        | Just p <- readPrimTyCon   str  -        = Just $ NamePrimTyCon p -        | Just p <- readPrimArith str  -        = Just $ NamePrimArith p+---------------------------------------------------------------------------------------------------+instance Pretty PrimType where+ ppr t+  = case t of+        PrimTypeTyConTetra p    -> ppr p+        PrimTypeTyCon  p        -> ppr p ++instance NFData PrimType where+ rnf t+  = case t of+        PrimTypeTyConTetra p    -> rnf p+        PrimTypeTyCon p         -> rnf p+++-- | Read the name of a primitive type.+readPrimType :: String -> Maybe PrimType+readPrimType str+        | Just p <- readPrimTyConTetra str  +        = Just $ PrimTypeTyConTetra p++        | Just p <- readPrimTyCon str  +        = Just $ PrimTypeTyCon p++        | otherwise+        = Nothing+++---------------------------------------------------------------------------------------------------+instance Pretty PrimVal where+ ppr val+  = case val of+        PrimValError  p         -> ppr p+        PrimValLit    lit       -> ppr lit+        PrimValArith  p         -> ppr p+        PrimValVector p         -> ppr p+        PrimValFun    p         -> ppr p+++instance NFData PrimVal where+ rnf val+  = case val of+        PrimValError  p         -> rnf p+        PrimValLit    lit       -> rnf lit+        PrimValArith  p         -> rnf p+        PrimValVector p         -> rnf p+        PrimValFun    p         -> rnf p+++-- | Read the name of a primtive value.+readPrimVal :: String -> Maybe PrimVal+readPrimVal str+        | Just (p, False) <- readOpErrorFlag str+        = Just $ PrimValError  p++        | Just lit        <- readPrimLit str+        = Just $ PrimValLit    lit++        | Just (p, False) <- readPrimArithFlag str  +        = Just $ PrimValArith  p++        | Just (p, False) <- readOpVectorFlag str+        = Just $ PrimValVector p++        | Just p          <- readOpFun str+        = Just $ PrimValFun    p++        | otherwise+        = Nothing+++---------------------------------------------------------------------------------------------------+instance Pretty PrimLit where+ ppr lit+  = case lit of+        PrimLitBool    True     -> text "True"+        PrimLitBool    False    -> text "False"+        PrimLitNat     i        -> integer i+        PrimLitInt     i        -> integer i <> text "i"+        PrimLitSize    s        -> integer s <> text "s"+        PrimLitWord    i bits   -> integer i <> text "w" <> int bits+        PrimLitFloat   f bits   -> double  f <> text "f" <> int bits+        PrimLitTextLit tx       -> text (show $ T.unpack tx)+++instance NFData PrimLit where+ rnf lit +  = case lit of+        PrimLitBool    b        -> rnf b+        PrimLitNat     n        -> rnf n+        PrimLitInt     i        -> rnf i+        PrimLitSize    s        -> rnf s+        PrimLitWord    i bits   -> rnf i `seq` rnf bits+        PrimLitFloat   d bits   -> rnf d `seq` rnf bits+        PrimLitTextLit bs       -> rnf bs       +++-- | Read the name of a primitive literal.+readPrimLit :: String -> Maybe PrimLit+readPrimLit str         -- Literal Bools-        | str == "True#"  = Just $ NameLitBool True-        | str == "False#" = Just $ NameLitBool False+        | str == "True"        = Just $ PrimLitBool True+        | str == "False"       = Just $ PrimLitBool False          -- Literal Nat         | Just val <- readLitNat str-        = Just $ NameLitNat  val+        = Just $ PrimLitNat  val          -- Literal Ints         | Just val <- readLitInt str-        = Just $ NameLitInt  val+        = Just $ PrimLitInt  val +        -- Literal Sizes+        | Just val <- readLitSize str+        = Just $ PrimLitSize val+         -- Literal Words         | Just (val, bits) <- readLitWordOfBits str         , elem bits [8, 16, 32, 64]-        = Just $ NameLitWord val bits--        -- Constructors.-        | c : _         <- str-        , isUpper c-        = Just $ NameCon str+        = Just $ PrimLitWord val bits -        -- Variables.-        | c : _         <- str-        , isLower c      -        = Just $ NameVar str+        -- Literal Floats+        | Just (val, bits) <- readLitFloatOfBits str+        , elem bits [32, 64]+        = Just $ PrimLitFloat val bits          | otherwise         = Nothing+

@@ -1,67 +1,199 @@ +-- | Definition of names used in Source Tetra language. module DDC.Source.Tetra.Prim.Base-        ( Name          (..)-        , TyConTetra    (..)-        , OpStore       (..)+        ( -- * Names+          Name          (..)++          -- * Primitive Names+        , PrimName      (..)+        , pattern NameType+        , pattern NameVal++          -- * Primitive Types+        , PrimType      (..)+        , pattern NameTyCon+        , pattern NameTyConTetra++          -- ** Primitive machine type constructors.         , PrimTyCon     (..)-        , PrimArith     (..))++          -- ** Primitive Tetra specific type constructors.+        , PrimTyConTetra(..)+        , pattern NameTyConTetraTuple+        , pattern NameTyConTetraVector+        , pattern NameTyConTetraF+        , pattern NameTyConTetraC+        , pattern NameTyConTetraU++          -- * Primitive Values+        , PrimVal       (..)+        , pattern NameLit+        , pattern NameArith+        , pattern NameVector+        , pattern NameFun+        , pattern NameError++          -- ** Primitive arithmetic operators.+        , PrimArith     (..)++          -- ** Primitive vector operators.+        , OpVector      (..)++          -- ** Primitive function operators.+        , OpFun         (..)++          -- ** Primitive error handling.+        , OpError       (..)++          -- ** Primitive literals.+        , PrimLit       (..)+        , pattern NameLitBool+        , pattern NameLitNat+        , pattern NameLitInt+        , pattern NameLitSize+        , pattern NameLitWord+        , pattern NameLitFloat+        , pattern NameLitTextLit) where import DDC.Core.Tetra    -        ( OpStore       (..)+        ( OpFun         (..)+        , OpVector      (..)+        , OpError       (..)         , PrimTyCon     (..)         , PrimArith     (..)) +import Data.Text        (Text) ++--------------------------------------------------------------------------------------------------- -- | Names of things used in Disciple Source Tetra. data Name         -- | A user defined variable.-        = NameVar               String+        = NameVar               !String          -- | A user defined constructor.-        | NameCon               String+        | NameCon               !String -        -- Baked in things -----------------------        -- | Baked in data type constructors.-        | NameTyConTetra        TyConTetra+        -- | Primitive names.+        | NamePrim              !PrimName -        -- | Baked in store operators.-        | NameOpStore           OpStore+        -- Inference ----------------------------+        -- | A hole used during type inference.+        | NameHole              +        deriving (Eq, Ord, Show) -        -- Machine primitives --------------------        -- | Primitive type cosntructors.-        | NamePrimTyCon         PrimTyCon -        -- | Primitive arithmetic, logic and comparison.-        | NamePrimArith         PrimArith+---------------------------------------------------------------------------------------------------+-- | Primitive names.+data PrimName+        = PrimNameType          !PrimType+        | PrimNameVal           !PrimVal+        deriving (Eq, Ord, Show) -        -- Literals ------------------------------        -- | A boolean literal.-        | NameLitBool           Bool+pattern NameType p              = NamePrim (PrimNameType p)+pattern NameVal  p              = NamePrim (PrimNameVal  p) -        -- | A natural literal.-        | NameLitNat            Integer -        -- | An integer literal.-        | NameLitInt            Integer--        -- | A word literal.-        | NameLitWord           Integer Int+---------------------------------------------------------------------------------------------------+-- | Primitive types.+data PrimType+        -- | Primitive machine type constructors.+        = PrimTypeTyCon         !PrimTyCon -        -- Inference -----------------------------        -- | A hole used during type inference.-        | NameHole              +        -- | Primtiive type constructors specific to the Tetra fragment.+        | PrimTypeTyConTetra    !PrimTyConTetra         deriving (Eq, Ord, Show) +pattern NameTyCon tc            = NamePrim (PrimNameType (PrimTypeTyCon tc))+pattern NameTyConTetra tc       = NamePrim (PrimNameType (PrimTypeTyConTetra tc)) --- TyConTetra ------------------------------------------------------------------- | Baked-in type constructors.-data TyConTetra-        -- | @Ref#@.    Mutable reference.-        = TyConTetraRef +---------------------------------------------------------------------------------------------------+-- | Primitive type constructors specific to the Tetra language fragment.+data PrimTyConTetra         -- | @TupleN#@. Tuples.-        | TyConTetraTuple Int+        = PrimTyConTetraTuple !Int+        +        -- | @Vector#@. Vectors.+        | PrimTyConTetraVector++        -- | @F#@.       Reified function values.+        | PrimTyConTetraF++        -- | @C#@.       Reified function closures.+        | PrimTyConTetraC++        -- | @U#@.       Explicitly unboxed values.+        | PrimTyConTetraU         deriving (Eq, Ord, Show) +pattern NameTyConTetraTuple i   = NameTyConTetra (PrimTyConTetraTuple i)+pattern NameTyConTetraVector    = NameTyConTetra PrimTyConTetraVector+pattern NameTyConTetraF         = NameTyConTetra PrimTyConTetraF+pattern NameTyConTetraC         = NameTyConTetra PrimTyConTetraC+pattern NameTyConTetraU         = NameTyConTetra PrimTyConTetraU ++---------------------------------------------------------------------------------------------------+-- | Primitive values.+data PrimVal+        -- | Primitive literals.+        = PrimValLit            !PrimLit++        -- | Primitive arithmetic operators.+        | PrimValArith          !PrimArith++        -- | Primitive error handling.+        | PrimValError          !OpError+        +        -- | Primitive vector operators.+        | PrimValVector         !OpVector++        -- | Primitive function operators.+        | PrimValFun            !OpFun+        deriving (Eq, Ord, Show)++pattern NameLit    p            = NamePrim (PrimNameVal  (PrimValLit    p))+pattern NameArith  p            = NamePrim (PrimNameVal  (PrimValArith  p))+pattern NameError  p            = NamePrim (PrimNameVal  (PrimValError  p))+pattern NameVector p            = NamePrim (PrimNameVal  (PrimValVector p))+pattern NameFun    p            = NamePrim (PrimNameVal  (PrimValFun    p))+++---------------------------------------------------------------------------------------------------+data PrimLit+        -- | A boolean literal.+        = PrimLitBool           !Bool++        -- | A natural literal,+        --   with enough precision to count every heap object.+        | PrimLitNat            !Integer++        -- | An integer literal,+        --   with enough precision to count every heap object.+        | PrimLitInt            !Integer++        -- | An unsigned size literal,+        --   with enough precision to count every addressable byte of memory.+        | PrimLitSize           !Integer++        -- | A word literal,+        --   with the given number of bits precison.+        | PrimLitWord           !Integer !Int++        -- | A floating point literal,+        --   with the given number of bits precision.+        | PrimLitFloat          !Double !Int++        -- | Text literals (UTF-8 encoded)+        | PrimLitTextLit        !Text+        deriving (Eq, Ord, Show)++pattern NameLitBool   x   = NameLit (PrimLitBool    x)+pattern NameLitNat    x   = NameLit (PrimLitNat     x)+pattern NameLitInt    x   = NameLit (PrimLitInt     x)+pattern NameLitSize   x   = NameLit (PrimLitSize    x)+pattern NameLitWord   x s = NameLit (PrimLitWord    x s)+pattern NameLitFloat  x s = NameLit (PrimLitFloat   x s)+pattern NameLitTextLit x  = NameLit (PrimLitTextLit x) 

@@ -1,4 +1,5 @@ +-- | Types of primitive Source Tetra arithmetic operators. module DDC.Source.Tetra.Prim.OpArith         (typePrimArith) where

@@ -0,0 +1,19 @@++module DDC.Source.Tetra.Prim.OpError+        ( typeOpError)+where+import DDC.Source.Tetra.Prim.TyConPrim+import DDC.Source.Tetra.Prim.Base+import DDC.Type.Compounds+import DDC.Type.Exp++++-- | Take the type of a primitive error function.+typeOpError :: OpError -> Type Name+typeOpError err+ = case err of+        OpErrorDefault    +         -> tForall kData $ \t -> tTextLit `tFun` tNat `tFun` t++

@@ -0,0 +1,69 @@++-- | Types of primitive Source Tetra function operators.+module DDC.Source.Tetra.Prim.OpFun+        (typeOpFun)+where+import DDC.Source.Tetra.Prim.TyConTetra+import DDC.Source.Tetra.Prim.Base+import DDC.Type.Compounds+import DDC.Type.Exp+++-- | Take the type of a primitive function operator.+typeOpFun :: OpFun -> Type Name+typeOpFun op+ = case op of+        OpFunCurry n+         -> tForalls (replicate (n + 1) kData)+         $  \ts -> +                let Just tF          = tFunOfList ts+                    Just result      = tFunOfList (tF : ts)+                in  result++        OpFunApply n+         -> tForalls (replicate (n + 1) kData)+         $  \ts -> +                let Just tF          = tFunOfList ts+                    Just result      = tFunOfList (tF : ts)+                in  result++        OpFunCReify+         -> tForalls [kData, kData]+         $  \[tA, tB]  -> (tA `tFun` tB) `tFun` tFunValue (tA `tFun` tB)++        OpFunCCurry n+         -> tForalls (replicate (n + 1) kData)+         $  \ts -> +                let tLast : tsFront' = reverse ts+                    tsFront          = reverse tsFront'+                    Just tF          = tFunOfList ts+                    Just result         +                        = tFunOfList +                                ( tFunValue tF+                                : tsFront ++ [tCloValue tLast])+                in result++        OpFunCExtend n+         -> tForalls (replicate (n + 1) kData)+         $  \ts -> +                let tLast : tsFront' = reverse ts+                    tsFront          = reverse tsFront'+                    Just tF          = tFunOfList ts+                    Just result+                        = tFunOfList+                                ( tCloValue tF+                                : tsFront ++ [tCloValue tLast])+                in result++        OpFunCApply n+         -> tForalls (replicate (n + 1) kData)+         $  \ts ->+                let tLast : tsFront' = reverse ts+                    tsFront          = reverse tsFront'+                    Just tF          = tFunOfList ts+                    Just result+                        = tFunOfList+                                ( tCloValue tF+                                : tsFront ++ [tLast])+                in result+

@@ -1,13 +0,0 @@--module DDC.Source.Tetra.Prim.OpStore-        (typeOpStore)-where-import DDC.Source.Tetra.Prim.Base-import DDC.Source.Tetra.Exp----- | Take the type of a primitive arithmetic operator.-typeOpStore :: OpStore -> Maybe (Type Name)-typeOpStore op- = case op of-        _       -> Nothing

@@ -0,0 +1,32 @@++-- Types of primitive Source Tetra vector operators.+module DDC.Source.Tetra.Prim.OpVector+        (typeOpVector)+where+import DDC.Source.Tetra.Prim.TyConPrim+import DDC.Source.Tetra.Prim.TyConTetra+import DDC.Source.Tetra.Prim.Base+import DDC.Type.Compounds+import DDC.Type.Exp+++-- | Take the type of a primitive vector operator.+typeOpVector :: OpVector -> Type Name+typeOpVector op+ = case op of+        OpVectorAlloc+         -> tForalls [kRegion, kData]+         $  \[tR, tA] -> tNat `tFun` tSusp (tAlloc tR) (tVector tR tA)++        OpVectorLength+         -> tForalls [kRegion, kData]+         $  \[tR, tA] -> tVector tR tA `tFun` tNat++        OpVectorRead+         -> tForalls [kRegion, kData]+         $  \[tR, tA] -> tVector tR tA `tFun` tNat `tFun` tSusp (tRead tR) tA++        OpVectorWrite+         -> tForalls [kRegion, kData]+         $  \[tR, tA] -> tVector tR tA `tFun` tNat `tFun` tA `tFun` tSusp (tWrite tR) tVoid+

@@ -1,7 +1,9 @@ +-- | Definitions of primitive types for Source Tetra language. module DDC.Source.Tetra.Prim.TyConPrim         ( kindPrimTyCon-        , tBool, tNat, tInt, tWord)+        , tVoid, tBool, tNat, tInt, tSize, tWord, tFloat+        , tTextLit) where import DDC.Source.Tetra.Prim.Base import DDC.Type.Compounds@@ -13,36 +15,58 @@ kindPrimTyCon tc  = case tc of         PrimTyConVoid    -> kData-        PrimTyConPtr     -> (kRegion `kFun` kData `kFun` kData)-        PrimTyConAddr    -> kData         PrimTyConBool    -> kData         PrimTyConNat     -> kData         PrimTyConInt     -> kData+        PrimTyConSize    -> kData         PrimTyConWord  _ -> kData         PrimTyConFloat _ -> kData+        PrimTyConVec   _ -> kData   `kFun` kData+        PrimTyConAddr    -> kData+        PrimTyConPtr     -> kRegion `kFun` kData `kFun` kData+        PrimTyConTextLit -> kData         PrimTyConTag     -> kData-        PrimTyConVec   _ -> kData `kFun` kData-        PrimTyConString  -> kData   -- Compounds ------------------------------------------------------------------+-- | Primitive `Void` type.+tVoid   :: Type Name+tVoid   = TCon (TyConBound (UPrim (NameTyCon PrimTyConVoid) kData) kData)++ -- | Primitive `Bool` type. tBool   :: Type Name-tBool   = TCon (TyConBound (UPrim (NamePrimTyCon PrimTyConBool) kData) kData)+tBool   = TCon (TyConBound (UPrim (NameTyCon PrimTyConBool) kData) kData)   -- | Primitive `Nat` type.-tNat    ::  Type Name-tNat    = TCon (TyConBound (UPrim (NamePrimTyCon PrimTyConNat) kData) kData)+tNat    :: Type Name+tNat    = TCon (TyConBound (UPrim (NameTyCon PrimTyConNat) kData) kData)   -- | Primitive `Int` type.-tInt    ::  Type Name-tInt    = TCon (TyConBound (UPrim (NamePrimTyCon PrimTyConInt) kData) kData)+tInt    :: Type Name+tInt    = TCon (TyConBound (UPrim (NameTyCon PrimTyConInt) kData) kData)  +-- | Primitive `Size` type.+tSize   :: Type Name+tSize   = TCon (TyConBound (UPrim (NameTyCon PrimTyConSize) kData) kData)++ -- | Primitive `WordN` type of the given width. tWord   :: Int -> Type Name tWord bits -        = TCon (TyConBound (UPrim (NamePrimTyCon (PrimTyConWord bits)) kData) kData)+        = TCon (TyConBound (UPrim (NameTyCon (PrimTyConWord bits)) kData) kData) ++-- | Primitive `FloatN` type of the given width.+tFloat  :: Int -> Type Name+tFloat bits+        = TCon (TyConBound (UPrim (NameTyCon (PrimTyConFloat bits)) kData) kData)+++-- | Primitive `TextLit` type.+tTextLit  :: Type Name+tTextLit+        = TCon (TyConBound (UPrim (NameTyCon PrimTyConTextLit) kData) kData)

@@ -1,8 +1,11 @@ +-- | Definitions of primitive type constructors for Source Tetra language. module DDC.Source.Tetra.Prim.TyConTetra-        ( kindTyConTetra-        , readTyConTetra-        , tRef)+        ( kindPrimTyConTetra+        , readPrimTyConTetra+        , tVector+        , tFunValue+        , tCloValue) where import DDC.Source.Tetra.Prim.Base import DDC.Type.Compounds@@ -12,43 +15,67 @@ import Data.List import Control.DeepSeq -instance NFData TyConTetra -instance Pretty TyConTetra where+instance NFData PrimTyConTetra where+ rnf !_ = ()+++instance Pretty PrimTyConTetra where  ppr tc   = case tc of-        TyConTetraRef           -> text "Ref#"-        TyConTetraTuple n       -> text "Tuple" <> int n <> text "#"+        PrimTyConTetraTuple n   -> text "Tuple" <> int n+        PrimTyConTetraVector    -> text "Vector"+        PrimTyConTetraF         -> text "F#"+        PrimTyConTetraC         -> text "C#"+        PrimTyConTetraU         -> text "U#"   -- | Read the name of a baked-in type constructor.-readTyConTetra :: String -> Maybe TyConTetra-readTyConTetra str+readPrimTyConTetra :: String -> Maybe PrimTyConTetra+readPrimTyConTetra str         | Just rest     <- stripPrefix "Tuple" str-        , (ds, "#")     <- span isDigit rest+        , (ds, "")      <- span isDigit rest         , not $ null ds         , arity         <- read ds-        = Just $ TyConTetraTuple arity+        = Just $ PrimTyConTetraTuple arity          | otherwise         = case str of-                "Ref#"          -> Just TyConTetraRef+                "Vector#"       -> Just PrimTyConTetraVector+                "F#"            -> Just PrimTyConTetraF+                "C#"            -> Just PrimTyConTetraC+                "U#"            -> Just PrimTyConTetraU                 _               -> Nothing   -- | Take the kind of a baked-in data constructor.-kindTyConTetra :: TyConTetra -> Type Name-kindTyConTetra tc+kindPrimTyConTetra :: PrimTyConTetra -> Type Name+kindPrimTyConTetra tc  = case tc of-        TyConTetraRef     -> kRegion `kFun` kData `kFun` kData-        TyConTetraTuple n -> foldr kFun kData (replicate n kData)+        PrimTyConTetraTuple n   -> foldr kFun kData (replicate n kData)+        PrimTyConTetraVector    -> kRegion `kFun` kData `kFun` kData+        PrimTyConTetraF         -> kData   `kFun` kData+        PrimTyConTetraC         -> kData   `kFun` kData+        PrimTyConTetraU         -> kData   `kFun` kData   -- Compounds --------------------------------------------------------------------- | Primitive `Ref` type.-tRef    :: Region Name -> Type Name -> Type Name-tRef tR tA   - = tApps (TCon (TyConBound (UPrim (NameTyConTetra TyConTetraRef) k) k))-                [tR, tA]+-- | Primitive `Vector` type.+tVector ::  Region Name -> Type Name -> Type Name+tVector tR tA   + = tApps (TCon (TyConBound (UPrim (NameTyConTetra PrimTyConTetraVector) k) k)) +         [tR, tA]  where k = kRegion `kFun` kData `kFun` kData+++tFunValue :: Type Name -> Type Name+tFunValue tA+ = tApps (TCon (TyConBound (UPrim (NameTyConTetra PrimTyConTetraF) k) k)) [tA]+ where k = kData `kFun` kData+++tCloValue :: Type Name -> Type Name+tCloValue tA+ = tApps (TCon (TyConBound (UPrim (NameTyConTetra PrimTyConTetraC) k) k)) [tA]+ where k = kData `kFun` kData 

@@ -1,306 +0,0 @@--module DDC.Source.Tetra.ToCore-        (toCoreModule)-where-import qualified DDC.Source.Tetra.Module        as S-import qualified DDC.Source.Tetra.DataDef       as S-import qualified DDC.Source.Tetra.Exp           as S-import qualified DDC.Source.Tetra.Prim          as S--import qualified DDC.Core.Tetra.Prim            as C-import qualified DDC.Core.Compounds             as C-import qualified DDC.Core.Module                as C-import qualified DDC.Core.Exp                   as C-import qualified DDC.Type.DataDef               as C--import qualified DDC.Type.Sum                   as Sum-import Data.Maybe---- Things shared between both Source and Core languages.-import DDC.Core.Exp-        ( Bind          (..)-        , Bound         (..)-        , Type          (..)-        , TyCon         (..)-        , Pat           (..)-        , DaCon         (..)-        , Witness       (..)-        , WiCon         (..))--import DDC.Core.Module -        ( ExportSource  (..)-        , ImportSource  (..))----- Module ------------------------------------------------------------------------ | Convert a Source Tetra module to Core Tetra.------   The Source code needs to already have been desugared and cannot contain,---   and `XDefix`, `XInfixOp`, or `XInfixVar` nodes, else `error`.----toCoreModule :: a -> S.Module a S.Name -> C.Module a C.Name-toCoreModule a mm-        = C.ModuleCore-        { C.moduleName          = S.moduleName mm--        , C.moduleExportTypes   -                = [ (toCoreN n, ExportSourceLocalNoType (toCoreN n))-                        | n <- S.moduleExportTypes mm ]--        , C.moduleExportValues-                = [ (toCoreN n, ExportSourceLocalNoType (toCoreN n))-                        | n <- S.moduleExportValues mm ]--        , C.moduleImportTypes   -                = [ (toCoreN n, toCoreImportSource isrc)-                        | (n, isrc) <- S.moduleImportTypes mm ]--        , C.moduleImportValues  -                = [ (toCoreN n, toCoreImportSource isrc)-                        | (n, isrc) <- S.moduleImportValues mm ]-        -        , C.moduleDataDefsLocal -                = [ toCoreDataDef def-                        | S.TopData _ def <- S.moduleTops mm ]--        , C.moduleBody          -                = C.XLet  a (letsOfTops (S.moduleTops mm))-                                        (C.xUnit a) }----- | Extract the top-level bindings from some source definitions.-letsOfTops :: [S.Top a S.Name] -> C.Lets a C.Name-letsOfTops tops- = C.LRec $ mapMaybe bindOfTop tops----- | Try to convert a `TopBind` to a top-level binding, ---   or `Nothing` if it isn't one.-bindOfTop  -        :: S.Top a S.Name -        -> Maybe (Bind C.Name, C.Exp a C.Name)--bindOfTop (S.TopBind _ b x) -                = Just (toCoreB b, toCoreX x)-bindOfTop _     = Nothing----- ImportSource ----------------------------------------------------------------toCoreImportSource :: ImportSource S.Name -> ImportSource C.Name-toCoreImportSource src- = case src of-        ImportSourceAbstract t    -         -> ImportSourceAbstract (toCoreT t)--        ImportSourceModule mn n t -         -> ImportSourceModule mn (toCoreN n) (toCoreT t)--        ImportSourceSea v t      -         -> ImportSourceSea v (toCoreT t)----- Type ------------------------------------------------------------------------toCoreT :: Type S.Name -> Type C.Name-toCoreT tt- = case tt of-        TVar    u       -> TVar (toCoreU  u)-        TCon    tc      -> TCon (toCoreTC tc)        -        TForall b t     -> TForall (toCoreB b) (toCoreT t)-        TApp    t1 t2   -> TApp (toCoreT t1) (toCoreT t2)-        TSum    ts      -> TSum $ Sum.fromList (toCoreT (Sum.kindOfSum ts))-                                $ map toCoreT -                                $ Sum.toList ts  ----- TyCon -----------------------------------------------------------------------toCoreTC :: TyCon S.Name -> TyCon C.Name-toCoreTC tc- = case tc of-        TyConSort sc    -> TyConSort sc-        TyConKind kc    -> TyConKind kc-        TyConWitness wc -> TyConWitness wc-        TyConSpec sc    -> TyConSpec sc-        TyConBound u k  -> TyConBound (toCoreU u) (toCoreT k)-        TyConExists n k -> TyConExists n          (toCoreT k)----- DataDef ---------------------------------------------------------------------toCoreDataDef :: S.DataDef S.Name -> C.DataDef C.Name-toCoreDataDef def-        = C.DataDef-        { C.dataDefTypeName       -                = toCoreN     $ S.dataDefTypeName def--        , C.dataDefParams-                = map toCoreB $ S.dataDefParams def--        , C.dataDefCtors          -                = Just -                $ [ toCoreDataCtor def tag ctor-                        | ctor  <- S.dataDefCtors def-                        | tag   <- [0..] ]--        , C.dataDefIsAlgebraic-                = True-        }----- DataCtor --------------------------------------------------------------------toCoreDataCtor -        :: S.DataDef S.Name -        -> Integer-        -> S.DataCtor S.Name -        -> C.DataCtor C.Name--toCoreDataCtor dataDef tag ctor-        = C.DataCtor-        { C.dataCtorName        = toCoreN (S.dataCtorName ctor)-        , C.dataCtorTag         = tag-        , C.dataCtorFieldTypes  = map toCoreT (S.dataCtorFieldTypes ctor)-        , C.dataCtorResultType  = toCoreT (S.dataCtorResultType ctor)-        , C.dataCtorTypeName    = toCoreN (S.dataDefTypeName dataDef) -        , C.dataCtorTypeParams  = map toCoreB (S.dataDefParams dataDef) }----- Exp -------------------------------------------------------------------------toCoreX :: S.Exp a S.Name -> C.Exp a C.Name-toCoreX xx- = case xx of-        S.XVar     a u      -> C.XVar     a (toCoreU  u)-        S.XCon     a dc     -> C.XCon     a (toCoreDC dc)-        S.XLAM     a b x    -> C.XLAM     a (toCoreB b)  (toCoreX x)-        S.XLam     a b x    -> C.XLam     a (toCoreB b)  (toCoreX x)-        S.XApp     a x1 x2  -> C.XApp     a (toCoreX x1) (toCoreX x2)-        S.XLet     a lts x  -> C.XLet     a (toCoreLts lts) (toCoreX x)-        S.XCase    a x alts -> C.XCase    a (toCoreX x)  (map toCoreA alts)-        S.XCast    a c x    -> C.XCast    a (toCoreC c)  (toCoreX x)-        S.XType    a t      -> C.XType    a (toCoreT t)-        S.XWitness a w      -> C.XWitness a (toCoreW w)--        -- These shouldn't exist in the desugared source tetra code.-        S.XDefix{}      -> error "source-tetra.toCoreX: found XDefix node"-        S.XInfixOp{}    -> error "source-tetra.toCoreX: found XInfixOp node"-        S.XInfixVar{}   -> error "source-tetra.toCoreX: found XInfixVar node"----- Lets ------------------------------------------------------------------------toCoreLts :: S.Lets a S.Name -> C.Lets a C.Name-toCoreLts lts- = case lts of-        S.LLet b x-         -> C.LLet (toCoreB b) (toCoreX x)-        -        S.LRec bxs-         -> C.LRec [(toCoreB b, toCoreX x) | (b, x) <- bxs ]--        S.LPrivate bks Nothing bts-         -> C.LPrivate (map toCoreB bks) Nothing (map toCoreB bts)--        S.LPrivate bks (Just tParent) bts-         -> C.LPrivate  (map toCoreB bks) -                        (Just $ toCoreT tParent) (map toCoreB bts)------ Cast ------------------------------------------------------------------------toCoreC :: S.Cast a S.Name -> C.Cast a C.Name-toCoreC cc- = case cc of-        S.CastWeakenEffect eff  -> C.CastWeakenEffect (toCoreT eff)-        S.CastPurify   w        -> C.CastPurify       (toCoreW w)-        S.CastBox               -> C.CastBox-        S.CastRun               -> C.CastRun----- Alt -------------------------------------------------------------------------toCoreA  :: S.Alt a S.Name -> C.Alt a C.Name-toCoreA aa- = case aa of-        S.AAlt w x      -> C.AAlt (toCoreP w) (toCoreX x)----- Pat -------------------------------------------------------------------------toCoreP  :: Pat S.Name -> Pat C.Name-toCoreP pp- = case pp of-        PDefault        -> PDefault-        PData dc bs     -> PData (toCoreDC dc) (map toCoreB bs)----- DaCon -----------------------------------------------------------------------toCoreDC :: DaCon S.Name -> DaCon C.Name-toCoreDC dc- = case dc of-        DaConUnit-         -> DaConUnit--        DaConPrim n t -         -> DaConPrim-                { daConName             = toCoreN n-                , daConType             = toCoreT t }--        DaConBound n-         -> DaConBound (toCoreN n)------ Witness ---------------------------------------------------------------------toCoreW :: Witness a S.Name -> Witness a C.Name-toCoreW ww- = case ww of-        S.WVar  a u     -> C.WVar  a (toCoreU  u)-        S.WCon  a wc    -> C.WCon  a (toCoreWC wc)-        S.WApp  a w1 w2 -> C.WApp  a (toCoreW  w1) (toCoreW w2)-        S.WJoin a w1 w2 -> C.WJoin a (toCoreW  w1) (toCoreW w2)-        S.WType a t     -> C.WType a (toCoreT  t)----- WiCon -----------------------------------------------------------------------toCoreWC :: WiCon S.Name -> WiCon C.Name-toCoreWC wc- = case wc of-        WiConBuiltin wb -> WiConBuiltin wb-        WiConBound u t  -> WiConBound (toCoreU u) (toCoreT t)----- Bind ------------------------------------------------------------------------toCoreB :: Bind S.Name -> Bind C.Name-toCoreB bb- = case bb of-        BName n t       -> BName (toCoreN n) (toCoreT t)-        BAnon t         -> BAnon (toCoreT t)-        BNone t         -> BNone (toCoreT t)----- Bound -----------------------------------------------------------------------toCoreU :: Bound S.Name -> Bound C.Name-toCoreU uu- = case uu of-        UName n         -> UName (toCoreN n)-        UIx   i         -> UIx   i-        UPrim n t       -> UPrim (toCoreN n) (toCoreT t)----- Name ------------------------------------------------------------------------toCoreN :: S.Name -> C.Name-toCoreN nn- = case nn of-        S.NameVar        str -> C.NameVar        str-        S.NameCon        str -> C.NameCon        str-        S.NameTyConTetra tc  -> C.NameTyConTetra (toCoreTyConTetra tc)-        S.NameOpStore    tc  -> C.NameOpStore    tc-        S.NamePrimTyCon  p   -> C.NamePrimTyCon  p-        S.NamePrimArith  p   -> C.NamePrimArith  p-        S.NameLitBool    b   -> C.NameLitBool    b-        S.NameLitNat     n   -> C.NameLitNat     n-        S.NameLitInt     i   -> C.NameLitInt     i  -        S.NameLitWord    w b -> C.NameLitWord    w b-        S.NameHole           -> C.NameHole---toCoreTyConTetra :: S.TyConTetra -> C.TyConTetra-toCoreTyConTetra tc- = case tc of-        S.TyConTetraRef      -> C.TyConTetraRef-        S.TyConTetraTuple n  -> C.TyConTetraTuple n-

@@ -0,0 +1,215 @@+{-# LANGUAGE TypeFamilies #-}+-- | Lifting and lowering level-0 deBruijn indices in source expressions.+--+--   Level-0 indices are used for both value and witness variables.+--+module DDC.Source.Tetra.Transform.BoundX+        ( liftX,        liftAtDepthX+--        , lowerX,       lowerAtDepthX+        , MapBoundX     (..)+        , HasAnonBind   (..))+where+import DDC.Source.Tetra.Exp.Generic+import DDC.Type.Exp++---------------------------------------------------------------------------------------------------+class HasAnonBind l => MapBoundX (c :: * -> *) l where+ mapBoundAtDepthX+        :: l                                    -- Proxy for language index, not inspected.+        -> (Int -> GBound l -> GBound l)        -- Function to apply to current bound occ.+        -> Int                                  -- Current binding depth.+        -> c l                                  -- Map across bounds in this thing.+        -> c l                                  -- Result thing.+++-- Lift -------------------------------------------------------------------------------------------+-- | Lift debruijn indices less than or equal to the given depth.+liftAtDepthX   +        :: (MapBoundX c l, GBound l ~ Bound n)+        => l+        -> Int          -- ^ Number of levels to lift.+        -> Int          -- ^ Current binding depth.+        -> c l          -- ^ Lift expression indices in this thing.+        -> c l++liftAtDepthX l n d+ = mapBoundAtDepthX l liftU d+ where  +        liftU d' u+         = case u of+                UName{}         -> u+                UPrim{}         -> u+                UIx i+                 | d' <= i      -> UIx (i + n)+                 | otherwise    -> u+++-- | Wrapper for `liftAtDepthX` that starts at depth 0.       +liftX   :: (MapBoundX c l, GBound l ~ Bound n)+        => Int -> c l -> c l++liftX n xx  + = let lProxy :: l+       lProxy = error "ddc-source-tetra.lProxy"+   in  liftAtDepthX lProxy n 0 xx+++---------------------------------------------------------------------------------------------------+instance HasAnonBind l => MapBoundX GExp l where+ mapBoundAtDepthX = downX ++downX l f d xx+  = case xx of+        XVar  a u       -> XVar a (f d u)+        XCon{}          -> xx+        XPrim{}         -> xx+        XApp  a x1 x2   -> XApp a   (downX l f d x1) (downX l f d x2)+        XLAM  a b x     -> XLAM a b (downX l f d x)++        XLam  a b x     +         -> let d'      = d + countBAnons l [b]+            in  XLam a b (mapBoundAtDepthX l f d' x)++        XLet  a lets x   +         -> let (lets', levels) = mapBoundAtDepthXLets l f d lets +            in  XLet a lets' (mapBoundAtDepthX l f (d + levels) x)++        XCase a x alts  -> XCase a  (downX l f d x)  (map (downA l f d) alts)+        XCast a cc x    -> XCast a  (downC l f d cc) (downX l f d x)+        XType{}         -> xx+        XWitness a w    -> XWitness a (downW l f d w)++        XDefix   a xs   -> XDefix a (map (downX l f d) xs)+        XInfixOp{}      -> xx+        XInfixVar{}     -> xx+++---------------------------------------------------------------------------------------------------+instance HasAnonBind l => MapBoundX GClause l where+ mapBoundAtDepthX = downCL++downCL l f d cc+  = case cc of+        SSig{}          -> cc+        SLet a b p gs   -> SLet a b p (map (downGX l f d) gs)+++---------------------------------------------------------------------------------------------------+instance HasAnonBind l => MapBoundX GAlt l where+ mapBoundAtDepthX = downA++downA l f d (AAlt p gxs)+  = case p of+        PDefault +         -> AAlt PDefault (map (downGX l f d)  gxs)++        PData _ bs +         -> let d' = d + countBAnons l bs+            in  AAlt p    (map (downGX l f d') gxs)+++---------------------------------------------------------------------------------------------------+instance HasAnonBind l => MapBoundX GGuardedExp l where+ mapBoundAtDepthX = downGX++downGX l f d gx+  = case gx of+        GGuard g gxs    +         -> let d' = d + countBAnonsG l g+            in  GGuard (downG l f d g) (downGX l f d' gxs)++        GExp x  +         -> GExp   (downX l f d x)+++---------------------------------------------------------------------------------------------------+instance HasAnonBind l => MapBoundX GGuard l where+ mapBoundAtDepthX = downG++downG l f d g+ = case g of+        GPat p x        -> GPat p (downX l f d x)+        GPred x         -> GPred  (downX l f d x)+        GDefault        -> GDefault+++---------------------------------------------------------------------------------------------------+instance HasAnonBind l => MapBoundX GCast l where+ mapBoundAtDepthX = downC++downC _l _f _d cc+  = case cc of+        CastWeakenEffect{} -> cc+        CastPurify w    -> CastPurify w+        CastBox         -> CastBox+        CastRun         -> CastRun++---------------------------------------------------------------------------------------------------+instance HasAnonBind l => MapBoundX GWitness l where+ mapBoundAtDepthX = downW++downW l f d ww+ = case ww of+        WVar a u        -> WVar a (f d u)+        WCon{}          -> ww+        WApp a w1 w2    -> WApp a (downW l f d w1) (downW l f d w2)+        WType{}         -> ww+++---------------------------------------------------------------------------------------------------+mapBoundAtDepthXLets+        :: forall l+        .  HasAnonBind l+        => l+        -> (Int -> GBound l -> GBound l)  +                           -- ^ Function given number of levels to lift.+        -> Int             -- ^ Current binding depth.+        -> GLets l         -- ^ Lift exp indices in this thing.+        -> (GLets l, Int)  -- ^ Lifted, and how much to increase depth by++mapBoundAtDepthXLets l f d lts+ = case lts of+        LLet b x+         -> let inc = countBAnons l [b]+                x'  = mapBoundAtDepthX l f d x+            in  (LLet b x', inc)++        LRec bs+         -> let inc = countBAnons l (map fst bs)+                bs' = map (\(b,e) -> (b, mapBoundAtDepthX l f (d + inc) e)) bs+            in  (LRec bs', inc)++        LPrivate _b _ bs +         -> (lts, countBAnons l bs)++        LGroup cs+         -> let inc = sum (map (countBAnonsC l) cs)+                cs' = map (mapBoundAtDepthX l f (d + inc)) cs+            in  (LGroup cs', inc)+++---------------------------------------------------------------------------------------------------+countBAnons  :: HasAnonBind l => l -> [GBind l] -> Int+countBAnons l = length . filter (isAnon l)+++countBAnonsC :: HasAnonBind l => l -> GClause l -> Int+countBAnonsC l c+ = case c of+        SSig _ b _   -> countBAnons l [b]+        SLet _ b _ _ -> countBAnons l [b]+++countBAnonsG :: HasAnonBind l => l -> GGuard l -> Int+countBAnonsG l g+ = case g of+        GPat p _    -> countBAnonsP l p +        GPred _     -> 0+        GDefault    -> 0++countBAnonsP :: HasAnonBind l => l -> GPat l -> Int+countBAnonsP l p+ = case p of+        PData _  bs -> countBAnons l bs+        PDefault    -> 0+

@@ -1,4 +1,21 @@ +-- | Convert infix expressions to prefix form.+--+--   The parser packs up sequences of expressions and operators into an +--   XDefix node, but does not convert them to standard prefix applications.+--   That is the job of this module.+--+--   The parsed code will contain XDefix, XInfixOp and XInfixVar nodes, +--   which are pretty-printed like this:+--+-- @ [DEFIX| Cons start [DEFIX| enumFromTo [DEFIX| start (INFIXOP "+") 1 ] end ]+-- @+--+--   After applying the transform in this module, all function applications+--   will be in prefix form:+--+-- @ Cons start (enumFromTo ((+) start 1) end)@+-- module DDC.Source.Tetra.Transform.Defix         ( FixTable      (..)         , FixDef        (..)@@ -19,32 +36,33 @@   -- Defix -----------------------------------------------------------------------class Defix (c :: * -> * -> *) where+class Defix (c :: * -> *) l where  -- | Resolve infix expressions in a thing.- defix  :: FixTable a n-        -> c a n-        -> Either (Error a n) (c a n)+ defix  :: FixTable l+        -> c l+        -> Either (Error l) (c l)  -instance Defix Module where+instance Defix Module l where  defix table mm    = do  tops'   <- mapM (defix table) (moduleTops mm)         return  $ mm { moduleTops = tops' }  -instance Defix Top where+instance Defix Top l where  defix table tt   = case tt of-        TopBind a b x   -> liftM (TopBind a b) (defix table x)+        TopClause a c   -> liftM (TopClause a) (defix table c)         _               -> return tt  -instance Defix Exp where+instance Defix GExp l where  defix table xx   = let down = defix table     in case xx of         XVar{}          -> return xx         XCon{}          -> return xx+        XPrim{}         -> return xx         XLAM  a b x     -> liftM  (XLAM  a b) (down x)         XLam  a b x     -> liftM  (XLam  a b) (down x)         XApp  a x1 x2   -> liftM2 (XApp  a)   (down x1)  (down x2)@@ -67,7 +85,7 @@                 Nothing  -> Left $ ErrorNoInfixDef a str  -instance Defix Lets where+instance Defix GLets l where  defix table lts   = let down = defix table     in case lts of@@ -80,14 +98,41 @@          LPrivate{}      -> return lts +        LGroup cs       -> liftM LGroup (mapM down cs) -instance Defix Alt where++instance Defix GClause l where+ defix table cc+  = let down = defix table+    in case cc of+        SSig{}          -> return cc+        SLet a b ps gs  -> liftM (SLet a b ps) (mapM down gs)+++instance Defix GAlt l where  defix table aa   = let down = defix table     in case aa of-        AAlt p x        -> liftM (AAlt p) (down x)+        AAlt p x        -> liftM (AAlt p) (mapM down x)  +instance Defix GGuardedExp l where+ defix table gg+  = let down = defix table+    in case gg of+        GGuard g x      -> liftM2 GGuard (down g) (down x)+        GExp x          -> liftM  GExp (down x)+++instance Defix GGuard l where+ defix table gg+  = let down = defix table+    in case gg of+        GPat p x        -> liftM  (GPat p) (down x)+        GPred x         -> liftM  GPred (down x)+        GDefault        -> return GDefault++ ------------------------------------------------------------------------------- -- | Preprocess the body of an XDefix node to insert applications. --    @@ -95,10 +140,10 @@ --   and produces (f a) + (g b) with three nodes in the XDefix list. -- defixApps -        :: a-        -> FixTable a n-        -> [Exp a n]-        -> Either (Error a n) [Exp a n]+        :: GAnnot l+        -> FixTable l+        -> [GExp l]+        -> Either (Error l) [GExp l]  defixApps a table xx  = start xx@@ -148,10 +193,10 @@ --   The input needs to have already been preprocessed by defixApps above. -- defixExps -        :: a                    -- ^ Annotation from original XDefix node.-        -> FixTable a n         -- ^ Table of infix defs.-        -> [Exp a n]            -- ^ Body of the XDefix node.-        -> Either (Error a n) (Exp a n)+        :: GAnnot l             -- ^ Annotation from original XDefix node.+        -> FixTable l           -- ^ Table of infix defs.+        -> [GExp l]             -- ^ Body of the XDefix node.+        -> Either (Error l) (GExp l)  defixExps a table xx  = case xx of@@ -178,10 +223,10 @@  -- | Try to defix a sequence of expressions and XInfixOp nodes. defixInfix-        :: a                    -- ^ Annotation from original XDefix node.-        -> FixTable a n         -- ^ Table of infix defs.-        -> [Exp a n]            -- ^ Body of the XDefix node.-        -> Either (Error a n) (Maybe [Exp a n])+        :: GAnnot l             -- ^ Annotation from original XDefix node.+        -> FixTable l           -- ^ Table of infix defs.+        -> [GExp l]             -- ^ Body of the XDefix node.+        -> Either (Error l) (Maybe [GExp l])  defixInfix a table xs         -- Get the list of infix ops in the expression.@@ -214,6 +259,9 @@         defsHigh <- mapM (getInfixDefOfSymbol sp table) opsHigh         let assocsHigh  = map fixDefAssoc defsHigh +        -- All operators at the current precedence level must have the+        -- same associativity, otherwise the implied order-of-operations is+        -- ambiguous.         case nub assocsHigh of          [InfixLeft]               -> do xs'     <- defixInfixLeft  sp table precHigh xs@@ -232,8 +280,8 @@  -- | Defix some left associative ops. defixInfixLeft -        :: a -> FixTable a n -> Int -        -> [Exp a n] -> Either (Error a n) [Exp a n]+        :: GAnnot l -> FixTable l -> Int +        -> [GExp l] -> Either (Error l) [GExp l]  defixInfixLeft sp table precHigh (x1 : XInfixOp spo op : x2 : xs)         | Just def      <- lookupDefInfixOfSymbol table op@@ -252,8 +300,8 @@ --   The input expression list is reversed, so we can eat the operators left --   to right. However, be careful to build the App node the right way around. defixInfixRight-        :: a -> FixTable a n -> Int -        -> [Exp a n] -> Either (Error a n) [Exp a n]+        :: GAnnot l  -> FixTable l -> Int +        -> [GExp l] -> Either (Error l) [GExp l]  defixInfixRight sp table precHigh (x2 : XInfixOp spo op : x1 : xs)         | Just def      <- lookupDefInfixOfSymbol table op@@ -270,8 +318,8 @@  -- | Defix non-associative ops. defixInfixNone -        :: a -> FixTable a n -> Int-        -> [Exp a n] -> Either (Error a n) [Exp a n]+        :: GAnnot l -> FixTable l -> Int+        -> [GExp l] -> Either (Error l) [GExp l]  defixInfixNone sp table precHigh xx         -- If there are two ops in a row that are non-associative and have

@@ -1,64 +1,67 @@+{-# LANGUAGE TypeFamilies, UndecidableInstances #-} +-- | Things that can go wrong when resolving infix expressions. module DDC.Source.Tetra.Transform.Defix.Error         (Error (..)) where-import DDC.Source.Tetra.Exp-import DDC.Base.Pretty-import qualified DDC.Data.SourcePos     as BP+import DDC.Source.Tetra.Exp.Generic+import DDC.Source.Tetra.Pretty   -- | Things that can go wrong when defixing code.-data Error a n+data Error l         -- | Infix operator symbol has no infix definition.         = ErrorNoInfixDef-        { errorAnnot            :: a+        { errorAnnot            :: GAnnot l         , errorSymbol           :: String }          -- | Two non-associative operators with the same precedence.         | ErrorDefixNonAssoc         { errorOp1              :: String-        , errorAnnot1           :: a+        , errorAnnot1           :: GAnnot l         , errorOp2              :: String-        , errorAnnot2           :: a }+        , errorAnnot2           :: GAnnot l }          -- | Two operators of different associativies with same precedence.         | ErrorDefixMixedAssoc -        { errorAnnot            :: a+        { errorAnnot            :: GAnnot l         , errorOps              :: [String] }          -- | Infix expression is malformed.         --   Eg "+ 3" or "2 + + 2"         | ErrorMalformed-        { errorAnnot            :: a-        , errorExp              :: Exp a n }-        deriving Show+        { errorAnnot            :: GAnnot l+        , errorExp              :: GExp l } +deriving instance ShowLanguage l => Show (Error l) --- Pretty ----------------------------------------------------------------------instance (Pretty n) -       => Pretty (Error BP.SourcePos n) where++instance PrettyLanguage l => Pretty (Error l) where  ppr err   = case err of         ErrorNoInfixDef{}          -> vcat [ ppr $ errorAnnot err-                 , text "No infix definition for symbol: " <> ppr (errorSymbol err) ]+                 , text "No infix definition for symbol: "+                        <> ppr (errorSymbol err) ]          ErrorDefixNonAssoc{}          -> vcat [ ppr $ errorAnnot1 err                  , text "Ambiguous infix expression."-                 , text " Operator  '"  <> text (errorOp1 err) -                                        <> text "' at " <> ppr (errorAnnot1 err)-                                        <+> text "is non associative,"+                 , text " Operator  '"  +                        <> text (errorOp1 err) +                        <> text "' at " <> ppr (errorAnnot1 err)+                        <+> text "is non associative,"                  , text " but the same precedence as"-                 , text "  operator '"  <> text (errorOp2 err)-                                        <> text "' at " <> ppr (errorAnnot2 err) -                                        <> text "."]+                 , text "  operator '"  +                        <> text (errorOp2 err)+                        <> text "' at " <> ppr (errorAnnot2 err) +                        <> text "."]          ErrorDefixMixedAssoc{}          -> vcat [ ppr $ errorAnnot err                  , text "Ambiguous infix expression."                  , text " operators "   <> hsep (map ppr (errorOps err))-                        <> text "have different associativities but same precedence." ]+                    <> text "have different associativities but same precedence." ]          ErrorMalformed{}          -> vcat [ ppr $ errorAnnot err

@@ -1,4 +1,8 @@-+{-# LANGUAGE TypeFamilies #-}+-- | Defines the table that tracks what precedence and associativity+--   infix operators have. The config for common operators is currently+--   hard-coded, rather than being configurable in the source language.+-- module DDC.Source.Tetra.Transform.Defix.FixTable         ( FixTable      (..)         , FixDef        (..)@@ -9,19 +13,19 @@         , defaultFixTable) where import DDC.Source.Tetra.Transform.Defix.Error+import DDC.Source.Tetra.Exp.Generic import DDC.Source.Tetra.Prim-import DDC.Source.Tetra.Exp import Data.List-import qualified DDC.Data.SourcePos     as BP+import qualified DDC.Type.Exp           as T   -- | Table of infix operator definitions.-data FixTable a n-        = FixTable [FixDef a n]+data FixTable l+        = FixTable [FixDef l]   -- | Infix operator definition.-data FixDef a n+data FixDef l         -- A prefix operator         = FixDefPrefix         { -- String of the operator@@ -29,7 +33,7 @@            -- Expression to rewrite the operator to,            -- given the annotation of the original symbol.-        , fixDefExp     :: a -> Exp a n }+        , fixDefExp     :: GAnnot l -> GExp l }          -- An infix operator.         | FixDefInfix@@ -38,7 +42,7 @@                    -- Expression to rewrite the operator to,            -- given the annotation of the original symbol.-        , fixDefExp     :: a -> Exp a n+        , fixDefExp     :: GAnnot l -> GExp l            -- Associativity of infix operator.         , fixDefAssoc   :: InfixAssoc@@ -47,7 +51,6 @@         , fixDefPrec    :: Int }  - -- | Infix associativity. data InfixAssoc         -- | Left associative.@@ -68,7 +71,7 @@   -- | Lookup the `FixDefInfix` corresponding to a symbol name, if any.-lookupDefInfixOfSymbol  :: FixTable a n -> String -> Maybe (FixDef a n)+lookupDefInfixOfSymbol  :: FixTable l -> String -> Maybe (FixDef l) lookupDefInfixOfSymbol (FixTable defs) str         = find (\def -> case def of                          FixDefInfix{}  -> fixDefSymbol def == str@@ -77,7 +80,7 @@   -- | Lookup the `FixDefPrefix` corresponding to a symbol name, if any.-lookupDefPrefixOfSymbol  :: FixTable a n -> String -> Maybe (FixDef a n)+lookupDefPrefixOfSymbol  :: FixTable l -> String -> Maybe (FixDef l) lookupDefPrefixOfSymbol (FixTable defs) str         = find (\def -> case def of                          FixDefPrefix{} -> fixDefSymbol def == str@@ -87,10 +90,10 @@  -- | Get the precedence of an infix symbol, else Error. getInfixDefOfSymbol -        :: a-        -> FixTable a n +        :: GAnnot l+        -> FixTable l         -> String -        -> Either (Error a n) (FixDef a n)+        -> Either (Error l) (FixDef l)  getInfixDefOfSymbol a table str  = case lookupDefInfixOfSymbol table str of@@ -99,17 +102,46 @@   -- | Default fixity table for infix operators.-defaultFixTable :: FixTable BP.SourcePos Name+defaultFixTable :: GBound l ~ T.Bound Name => FixTable l defaultFixTable  = FixTable -        [ FixDefPrefix "-"  (\sp -> XVar sp (UName (NameVar "neg")))-        , FixDefInfix  "*"  (\sp -> XVar sp (UName (NameVar "mul"))) InfixLeft  7-        , FixDefInfix  "+"  (\sp -> XVar sp (UName (NameVar "add"))) InfixLeft  6-        , FixDefInfix  "-"  (\sp -> XVar sp (UName (NameVar "sub"))) InfixLeft  6 -        , FixDefInfix  "==" (\sp -> XVar sp (UName (NameVar "eq" ))) InfixNone  5-        , FixDefInfix  "/=" (\sp -> XVar sp (UName (NameVar "neq"))) InfixNone  5-        , FixDefInfix  "<"  (\sp -> XVar sp (UName (NameVar "lt" ))) InfixNone  5-        , FixDefInfix  "<=" (\sp -> XVar sp (UName (NameVar "le" ))) InfixNone  5-        , FixDefInfix  ">"  (\sp -> XVar sp (UName (NameVar "gt" ))) InfixNone  5-        , FixDefInfix  ">=" (\sp -> XVar sp (UName (NameVar "ge" ))) InfixNone  5-        , FixDefInfix  "$"  (\sp -> XVar sp (UName (NameVar "app"))) InfixRight 1 ]+        [ FixDefPrefix  "-"     (xvar "neg")+        , FixDefPrefix  "¬"     (xvar "not")++        -- Operators defined in the Haskell Prelude.+        , FixDefInfix   "∘"     (xvar "compose")        InfixRight 9++        , FixDefInfix   "*"     (xvar "mul")            InfixLeft  7++        , FixDefInfix   "+"     (xvar "add")            InfixLeft  6+        , FixDefInfix   "-"     (xvar "sub")            InfixLeft  6++        , FixDefInfix   "∪"     (xvar "intersect")      InfixLeft  6+        , FixDefInfix   "∩"     (xvar "union")          InfixLeft  6++        , FixDefInfix   "=="    (xvar "eq")             InfixNone  4+        , FixDefInfix   "/="    (xvar "neq")            InfixNone  4+        , FixDefInfix   "<"     (xvar "lt")             InfixNone  4+        , FixDefInfix   "<="    (xvar "le")             InfixNone  4+        , FixDefInfix   ">"     (xvar "gt")             InfixNone  4+        , FixDefInfix   ">="    (xvar "ge")             InfixNone  4++        , FixDefInfix   "/\\"   (xvar "and")            InfixRight 3+        , FixDefInfix   "∧"     (xvar "and")            InfixRight 3++        , FixDefInfix   "\\/"   (xvar "or")             InfixRight 3+        , FixDefInfix   "∨"     (xvar "or")             InfixRight 3++        , FixDefInfix   "$"     (xvar "apply")          InfixRight 1 ++        -- String pasting.+        --   These associate to the right so that when text objects are formed by+        --   pasting several together, then spine of the data structure leans to +        --   the right, as do cons lists.+        , FixDefInfix   "%"  (xvar "paste")             InfixRight 6+        , FixDefInfix   "%%" (xvar "pastes")            InfixRight 6+        ]++ where  xvar str sp +         = XVar sp (T.UName (NameVar str))+

@@ -1,4 +1,26 @@+{-# LANGUAGE TypeFamilies, UndecidableInstances #-} +-- | Look at type signatures and add quantifiers to bind any free type+--   variables. Also add holes for missing type arguments.+--   +--   Given+--+-- @+--    mapS (f : a -> S e b) (xx : List a) : S e (List b)+--     = box case xx of+--        Nil        -> Nil+--        Cons x xs  -> Cons (run f x) (run mapS f xs)+-- @+--+--  We get:+--+-- @+--    mapS [a e b : ?] (f : a -> S e b) (xx : List a) : S e (List b)+--     = /\(a e b : ?). box case xx of+--        Nil        -> Nil+--        Cons x xs  -> Cons (run f x) (run mapS [?] [?] [?] f xs)+-- @+-- module DDC.Source.Tetra.Transform.Expand         ( Config        (..)         , configDefault@@ -16,34 +38,42 @@ import qualified Data.Set               as Set  --------------------------------------------------------------------------------+--------------------------------------------------------------------------------------------------- -- | Expander configuration.-data Config a n+data Config l         = Config         { -- | Make a type hole of the given kind.-          configMakeTypeHole    :: Kind n -> Type n }+          configMakeTypeHole    :: Kind (GName l) -> Type (GName l) }   -- | Default expander configuration.-configDefault :: Config a Name+configDefault :: GName l ~ Name => Config l configDefault          = Config         { configMakeTypeHole    = \k -> TVar (UPrim NameHole k)}  ---------------------------------------------------------------------------------class Expand (c :: * -> * -> *) where+---------------------------------------------------------------------------------------------------+type ExpandLanguage l+        = ( Ord (GName l)+          , GBind  l ~ Bind  (GName l)+          , GBound l ~ Bound (GName l))++class ExpandLanguage l => Expand (c :: * -> *) l where  -- | Add quantifiers to the types of binders. Also add holes for missing  --   type arguments.  expand-        :: Ord n -        => Config a n-        -> KindEnv n -> TypeEnv n-        -> c a n     -> c a n+        :: Ord (GName l) +        => Config l+        -> KindEnv (GName l) -> TypeEnv (GName l)+        -> c l -> c l  -instance Expand Module where- expand config kenv tenv mm+---------------------------------------------------------------------------------------------------+instance ExpandLanguage l => Expand Module l where+ expand = expandM++expandM config kenv tenv mm   = let          -- Add quantifiers to the types of bindings, and also slurp         -- out the contribution to the top-level environment from each binding.@@ -51,13 +81,17 @@         --   thing is in-scope of all the others.         preTop p          = case p of-                TopBind a b x+                TopClause a (SLet _ b [] [GExp x])                  -> let (b', x') = expandQuant a config kenv (b, x)-                    in  (TopBind a b' x', Env.singleton b')+                    in  ( TopClause a (SLet a b' [] [GExp x'])+                        , Env.singleton b')                  TopData _ def                  -> (p, typeEnvOfDataDef def) +                -- Clauses should have already desugared.+                _ -> error "source-tetra.expand: can't expand sugared TopClause."+         (tops_quant, tenvs)                 = unzip $ map preTop $ moduleTops mm @@ -71,23 +105,30 @@     in  mm { moduleTops = tops' }  -instance Expand Top where- expand config kenv tenv top+---------------------------------------------------------------------------------------------------+instance ExpandLanguage l => Expand Top l where+ expand = expandT++expandT config kenv tenv top   = case top of-        TopBind a b x   +        TopClause a1 (SLet a2 b [] [GExp x])          -> let tenv'   = Env.extend b tenv                 x'      = expand config kenv tenv' x-            in  TopBind a b x'+            in  TopClause a1 (SLet a2 b [] [GExp x']) -        TopData{}-         -> top+        TopData{} -> top +        -- Clauses should have already been desugared.+        _   -> error "source-tetra.expand: can't expand sugared TopClause." -instance Expand Exp where- expand config kenv tenv xx-  = let down = expand config kenv tenv-    in case xx of +---------------------------------------------------------------------------------------------------+instance ExpandLanguage l => Expand GExp l where+ expand = downX++downX config kenv tenv xx+  = case xx of+         -- Invoke the expander --------         XVar{}          ->     expandApp config kenv tenv xx []@@ -95,6 +136,9 @@         XCon{}          ->     expandApp config kenv tenv xx [] +        XPrim{}+         ->     expandApp config kenv tenv xx []+         XApp{}          | (x1, xas)     <- takeXAppsWithAnnots xx          -> if isXVar x1 || isXCon x1@@ -130,7 +174,17 @@                 x2'     = expand config kenv tenv' x2             in  XLet a (LRec (zip bs_quant xs')) x2' +        -- LGroups need to be desugared first because any quantifiers+        -- we add to the front of a function binding need to scope over+        -- all the clauses related to that binding.+        XLet a (LGroup [SLet _ b [] [GExp x1]]) x2+         -> expand config kenv tenv (XLet a (LLet b x1) x2) +        -- This should have already been desugared.+        XLet _ (LGroup{}) _+         -> error $ "ddc-source-tetra.expand: can't expand sugared LGroup."++         -- Boilerplate ----------------         XLAM a b x          -> let kenv'   = Env.extend b kenv@@ -148,41 +202,95 @@                 x2'     = expand config kenv' tenv' x2             in  XLet a (LPrivate bts mR bxs) x2' -        XCase a x alts  -> XCase a   (down x)   (map down alts)-        XCast a c x     -> XCast a c (down x)+        XCase a x alts  -> XCase a   (downX config kenv tenv x)   +                                     (map (downA config kenv tenv) alts)+        XCast a c x     -> XCast a c (downX config kenv tenv x)         XType{}         -> xx         XWitness{}      -> xx-        XDefix a xs     -> XDefix a  (map down xs)+        XDefix a xs     -> XDefix a  (map (downX config kenv tenv) xs)         XInfixOp{}      -> xx         XInfixVar{}     -> xx  -instance Expand Alt where- expand config kenv tenv alt+---------------------------------------------------------------------------------------------------+instance ExpandLanguage l => Expand GAlt l where+ expand = downA++downA config kenv tenv alt   = case alt of-        AAlt PDefault x2-         -> let x2'     = expand config kenv tenv x2-            in  AAlt PDefault x2'+        AAlt p gsx+         -> let tenv'   = extendPat p tenv+                gsx'    = map (expand config kenv tenv') gsx+            in  AAlt p gsx' -        AAlt (PData dc bs) x2-         -> let tenv'   = Env.extends bs tenv-                x2'     = expand config kenv tenv' x2-            in  AAlt (PData dc bs) x2' +---------------------------------------------------------------------------------------------------+instance ExpandLanguage l => Expand GGuardedExp l where+ expand = downGX --------------------------------------------------------------------------------+downGX config kenv tenv (GGuard g x)+  = let g'      = expand config kenv tenv g+        tenv'   = extendGuard g' tenv+    in  GGuard g' (expand config kenv tenv' x)++downGX config kenv tenv (GExp x)+  = let x'      = expand config kenv tenv x+    in  GExp x'+++---------------------------------------------------------------------------------------------------+instance ExpandLanguage l => Expand GGuard l where+ expand = downG++downG config kenv tenv gg+  = case gg of+        GPat p x+         -> let tenv'   = extendPat p tenv+                x'      = expand config kenv tenv' x+            in  GPat  p x'++        GPred x+         -> let x'      = expand config kenv tenv x+            in  GPred x'++        GDefault+         -> GDefault +++---------------------------------------------------------------------------------------------------+-- | Extend a type environment with the variables bound by the given pattern.+extendPat +        :: ExpandLanguage l+        => GPat l -> TypeEnv (GName l) -> TypeEnv (GName l)+extendPat ww tenv+ = case ww of+        PDefault        -> tenv+        PData _  bs     -> Env.extends bs tenv+++-- | Extend a type environment with the variables bound by the given guard.+extendGuard+        :: ExpandLanguage l+        => GGuard l -> TypeEnv (GName l) -> TypeEnv (GName l)+extendGuard gg tenv+ = case gg of+        GPat w _        -> extendPat w tenv+        _               -> tenv+++--------------------------------------------------------------------------------------------------- -- | Expand missing quantifiers in types of bindings. --   --   If a binding mentions type variables that are not in scope then add new --   quantifiers to its type, as well as matching type lambdas. -- expandQuant -        :: Ord n-        => a                    -- ^ Annotation to use on new type lambdas.-        -> Config a n           -- ^ Expander configuration.-        -> KindEnv  n           -- ^ Current kind environment.-        -> (Bind n, Exp a n)    -- ^ Binder and expression of binding.-        -> (Bind n, Exp a n)+        :: ExpandLanguage l+        => GAnnot l             -- ^ Annotation to use on new type lambdas.+        -> Config l             -- ^ Expander configuration.+        -> KindEnv  (GName l)   -- ^ Current kind environment.+        -> (GBind l, GExp l)    -- ^ Binder and expression of binding.+        -> (GBind l, GExp l)  expandQuant a config kenv (b, x)  | fvs  <- freeVarsT kenv (typeOfBind b)@@ -213,7 +321,7 @@  = (b, x)  --------------------------------------------------------------------------------+--------------------------------------------------------------------------------------------------- -- | Expand missing type arguments in applications. --    --   The thing being applied needs to be a variable or data constructor@@ -222,13 +330,13 @@ --   the expression is missing them. -- expandApp -        :: Ord n-        => Config a n           -- ^ Expander configuration.-        -> KindEnv n            -- ^ Current kind environment.-        -> TypeEnv n            -- ^ Current type environment.-        -> Exp a n              -- ^ Functional expression being applied.-        -> [(Exp a n, a)]       -- ^ Function arguments.-        -> Exp a n+        :: ExpandLanguage l+        => Config l             -- ^ Expander configuration.+        -> KindEnv (GName l)    -- ^ Current kind environment.+        -> TypeEnv (GName l)    -- ^ Current type environment.+        -> GExp l               -- ^ Functional expression being applied.+        -> [(GExp l, GAnnot l)] -- ^ Function arguments.+        -> GExp l  expandApp config _kenv tenv x0 xas0  | Just (a, u)  <- slurpVarConBound x0@@ -259,7 +367,10 @@  -- | Slurp a `Bound` from and `XVar` or `XCon`.  --   Named data constructors are converted to `UName`s.-slurpVarConBound :: Exp a n -> Maybe (a, Bound n)+slurpVarConBound +        :: GBound l ~ Bound (GName l)+        => GExp l +        -> Maybe (GAnnot l, GBound l) slurpVarConBound xx  = case xx of         XVar a u -> Just (a, u)

@@ -0,0 +1,68 @@+{-# LANGUAGE TypeFamilies #-}++-- | Desugaring Source Tetra guards to simple case-expressions.+module DDC.Source.Tetra.Transform.Guards+        ( desugarGuards )+where+import DDC.Source.Tetra.Transform.BoundX+import DDC.Source.Tetra.Compounds+import DDC.Source.Tetra.Exp.Annot+import DDC.Type.Exp+++-- | Desugar some guards to a case-expression.+--   At runtime, if none of the guards match then run the provided fail action.+desugarGuards+        :: forall a+        .  GAnnot (Annot a)         -- ^ Annotation.+        -> [GGuardedExp (Annot a)]  -- ^ Guarded expressions to desugar.+        -> GExp (Annot a)           -- ^ Failure action.+        -> GExp (Annot a)++desugarGuards a gs0 fail0+ = go gs0 fail0+ where+        -- Desugar list of guarded expressions.+        go [] cont+         = cont++        go [g]   cont+         = go1 g cont++        go (g : gs) cont+         = go1 g (go gs cont)++        -- Desugar single guarded expression.+        go1 (GExp x1) _+         = x1++        go1 (GGuard GDefault   gs) cont+         = go1 gs cont++        -- Simple cases where we can avoid introducing the continuation.+        go1 (GGuard (GPred g1)   (GExp x1)) cont+         = XCase a g1+                [ AAlt pTrue     [GExp x1]+                , AAlt PDefault  [GExp cont] ]++        go1 (GGuard (GPat p1 g1) (GExp x1)) cont+         = XCase a g1+                [ AAlt p1        [GExp x1]+                , AAlt PDefault  [GExp cont]]++        -- Cases that use a continuation function as a join point.+        -- We need this when desugaring general pattern alternatives,+        -- as each group of guards can be reached from multiple places.+        go1 (GGuard (GPred x1) gs) cont+         = XLet  a (LLet (BAnon (tBot kData)) (xBox a cont))+         $ XCase a (liftX 1 x1)+                [ AAlt pTrue     [GExp (go1 (liftX 1 gs) (xRun a (XVar a (UIx 0))))]+                , AAlt PDefault  [GExp                   (xRun a (XVar a (UIx 0))) ]]++        go1 (GGuard (GPat p1 x1) gs) cont+         = XLet a (LLet (BAnon (tBot kData)) (xBox a cont))+         $ XCase a (liftX 1 x1)+                [ AAlt p1        [GExp (go1 (liftX 1 gs) (xRun a (XVar a (UIx 0))))]+                , AAlt PDefault  [GExp                   (xRun a (XVar a (UIx 0))) ]]+        +

@@ -1,5 +1,5 @@ Name:           ddc-source-tetra-Version:        0.4.1.3+Version:        0.4.2.1 License:        MIT License-file:   LICENSE Author:         The Disciplined Disciple Compiler Strike Force@@ -17,22 +17,29 @@                  Library   Build-Depends: -        base             >= 4.6 && < 4.8,-        array            >= 0.4 && < 0.6,-        deepseq          == 1.3.*,+        base             >= 4.6   && < 4.9,+        array            >= 0.4   && < 0.6,+        deepseq          >= 1.3   && < 1.5,         containers       == 0.5.*,+        text             >= 1.0   && < 1.3,         transformers     == 0.4.*,-        mtl              == 2.2.*,-        ddc-base         == 0.4.1.*,-        ddc-core         == 0.4.1.*,-        ddc-core-salt    == 0.4.1.*,-        ddc-core-tetra   == 0.4.1.*+        mtl              == 2.2.1.*,+        ddc-base         == 0.4.2.*,+        ddc-core         == 0.4.2.*,+        ddc-core-salt    == 0.4.2.*,+        ddc-core-tetra   == 0.4.2.*    Exposed-modules:-        DDC.Source.Tetra.Transform.Expand+        DDC.Source.Tetra.Exp.Annot+        DDC.Source.Tetra.Exp.Generic++        DDC.Source.Tetra.Transform.BoundX         DDC.Source.Tetra.Transform.Defix-        +        DDC.Source.Tetra.Transform.Expand+        DDC.Source.Tetra.Transform.Guards+         DDC.Source.Tetra.Compounds+        DDC.Source.Tetra.Convert         DDC.Source.Tetra.DataDef         DDC.Source.Tetra.Env         DDC.Source.Tetra.Exp@@ -42,22 +49,26 @@         DDC.Source.Tetra.Predicates         DDC.Source.Tetra.Pretty         DDC.Source.Tetra.Prim-        DDC.Source.Tetra.ToCore    Other-modules:-        DDC.Source.Tetra.Exp.Base-        DDC.Source.Tetra.Lexer.Lit+        DDC.Source.Tetra.Convert.Error++        DDC.Source.Tetra.Parser.Atom         DDC.Source.Tetra.Parser.Exp         DDC.Source.Tetra.Parser.Module         DDC.Source.Tetra.Parser.Param+        DDC.Source.Tetra.Parser.Witness+         DDC.Source.Tetra.Prim.Base         DDC.Source.Tetra.Prim.OpArith-        DDC.Source.Tetra.Prim.OpStore+        DDC.Source.Tetra.Prim.OpError+        DDC.Source.Tetra.Prim.OpFun+        DDC.Source.Tetra.Prim.OpVector         DDC.Source.Tetra.Prim.TyConPrim         DDC.Source.Tetra.Prim.TyConTetra+         DDC.Source.Tetra.Transform.Defix.Error         DDC.Source.Tetra.Transform.Defix.FixTable-            GHC-options:         -Wall@@ -67,13 +78,18 @@         -fno-warn-unused-do-bind    Extensions:-        KindSignatures         NoMonomorphismRestriction+        MultiParamTypeClasses         ScopedTypeVariables-        PatternGuards-        FlexibleContexts+        StandaloneDeriving         FlexibleInstances-        RankNTypes-        BangPatterns+        FlexibleContexts         ParallelListComp-        +        ConstraintKinds+        PatternSynonyms+        EmptyDataDecls+        KindSignatures+        PatternGuards+        BangPatterns+        RankNTypes+