ddc-source-tetra 0.4.2.1 → 0.4.3.1

raw patch · 53 files changed

+6459/−2731 lines, 53 filesdep +pretty-showdep −ddc-basedep ~basedep ~ddc-coredep ~ddc-core-saltPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: pretty-show

Dependencies removed: ddc-base

Dependency ranges changed: base, ddc-core, ddc-core-salt, ddc-core-tetra, transformers

API changes (from Hackage documentation)

Files

• DDC/Source/Tetra/Collect/FreeVars.hs +44/−0
• DDC/Source/Tetra/Compounds.hs +0/−244
• DDC/Source/Tetra/Convert.hs +222/−300
• DDC/Source/Tetra/Convert/Base.hs +21/−0
• DDC/Source/Tetra/Convert/Clause.hs +99/−0
• DDC/Source/Tetra/Convert/Error.hs +42/−16
• DDC/Source/Tetra/Convert/Prim.hs +45/−0
• DDC/Source/Tetra/Convert/Type.hs +241/−0
• DDC/Source/Tetra/Convert/Witness.hs +41/−0
• DDC/Source/Tetra/DataDef.hs +36/−26
• DDC/Source/Tetra/Env.hs +299/−59
• DDC/Source/Tetra/Exp.hs +237/−22
• DDC/Source/Tetra/Exp/Annot.hs +0/−54
• DDC/Source/Tetra/Exp/Bind.hs +71/−0
• DDC/Source/Tetra/Exp/Compounds.hs +300/−0
• DDC/Source/Tetra/Exp/Generic.hs +173/−167
• DDC/Source/Tetra/Exp/NFData.hs +127/−0
• DDC/Source/Tetra/Exp/Predicates.hs +139/−0
• DDC/Source/Tetra/Exp/Source.hs +162/−0
• DDC/Source/Tetra/Lexer.hs +84/−7
• DDC/Source/Tetra/Module.hs +21/−11
• DDC/Source/Tetra/Parser.hs +17/−30
• DDC/Source/Tetra/Parser/Atom.hs +0/−28
• DDC/Source/Tetra/Parser/Base.hs +154/−0
• DDC/Source/Tetra/Parser/Exp.hs +777/−643
• DDC/Source/Tetra/Parser/Module.hs +125/−121
• DDC/Source/Tetra/Parser/Param.hs +110/−18
• DDC/Source/Tetra/Parser/Type.hs +205/−0
• DDC/Source/Tetra/Parser/Witness.hs +36/−47
• DDC/Source/Tetra/Predicates.hs +0/−132
• DDC/Source/Tetra/Pretty.hs +225/−40
• DDC/Source/Tetra/Prim.hs +82/−136
• DDC/Source/Tetra/Prim/Base.hs +39/−80
• DDC/Source/Tetra/Prim/OpArith.hs +29/−24
• DDC/Source/Tetra/Prim/OpCast.hs +29/−0
• DDC/Source/Tetra/Prim/OpError.hs +5/−8
• DDC/Source/Tetra/Prim/OpFun.hs +32/−46
• DDC/Source/Tetra/Prim/OpVector.hs +14/−13
• DDC/Source/Tetra/Prim/TyCon.hs +41/−0
• DDC/Source/Tetra/Prim/TyConPrim.hs +62/−47
• DDC/Source/Tetra/Prim/TyConTetra.hs +20/−32
• DDC/Source/Tetra/Transform/BoundX.hs +84/−49
• DDC/Source/Tetra/Transform/Defix.hs +33/−20
• DDC/Source/Tetra/Transform/Defix/Error.hs +5/−5
• DDC/Source/Tetra/Transform/Defix/FixTable.hs +7/−8
• DDC/Source/Tetra/Transform/Expand.hs +195/−232
• DDC/Source/Tetra/Transform/Freshen.hs +483/−0
• DDC/Source/Tetra/Transform/Freshen/State.hs +145/−0
• DDC/Source/Tetra/Transform/Guards.hs +380/−53
• DDC/Source/Tetra/Transform/Matches.hs +346/−0
• DDC/Source/Tetra/Transform/Prep.hs +342/−0
• LICENSE +1/−1
• ddc-source-tetra.cabal +32/−12

@@ -0,0 +1,44 @@++module DDC.Source.Tetra.Collect.FreeVars where+import DDC.Source.Tetra.Exp+import DDC.Source.Tetra.Env             (Env, Presence(..))+import Data.Set                         (Set)+import qualified DDC.Source.Tetra.Env   as Env+import qualified Data.Set               as Set+++-- | Collect the variables a type that do not appear in the given environment.+freeVarsT :: Env -> Type -> Set Bound+freeVarsT env tt+ = case tt of+        TAnnot _ t+         -> freeVarsT env t++        TCon{}+         -> Set.empty++        TVar u@(UName _)+         -> case Env.lookupTyVar env u of+                Present _ -> Set.empty+                Unknown   -> Set.empty+                Absent    -> Set.singleton u++        TVar u@(UIx i)+         -> case Env.lookupTyVar env u of+                Present _ -> Set.empty+                Unknown   -> Set.empty+                Absent    -> Set.singleton (UIx (i - Env.tyStackDepth env))++        TVar UHole+         -> Set.empty++        TAbs{}+         |  Just (k, b, t)       <- takeTForall tt+         -> freeVarsT (Env.extendTyVar b k env) t++         |  otherwise+         -> Set.empty++        TApp t1 t2+         -> Set.union (freeVarsT env t1) (freeVarsT env t2)+

@@ -1,244 +0,0 @@-{-# LANGUAGE TypeFamilies #-}---- | Utilities for constructing and destructing Source Tetra expressions.-module DDC.Source.Tetra.Compounds-        ( module DDC.Type.Compounds-        , takeAnnotOfExp--          -- * Lambdas-        , xLAMs-        , xLams-        , makeXLamFlags-        , takeXLAMs-        , takeXLams-        , takeXLamFlags--          -- * Applications-        , xApps-        , makeXAppsWithAnnots-        , takeXApps-        , takeXApps1-        , takeXAppsAsList-        , takeXAppsWithAnnots-        , takeXConApps-        , takeXPrimApps--          -- * Casts-        , xBox-        , xRun--          -- * Data Constructors-        , dcUnit-        , takeNameOfDaCon-        , takeTypeOfDaCon--          -- * Patterns-        , bindsOfPat-        , pTrue-        , pFalse--          -- * Witnesses-        , wApp-        , wApps-        , takeXWitness-        , takeWAppsAsList-        , takePrimWiConApps--          -- * Primitives-        , xErrorDefault)-where-import DDC.Source.Tetra.Exp-import DDC.Source.Tetra.Prim-import DDC.Type.Compounds-import Data.Text                        (Text)-import DDC.Core.Exp.Annot.Compounds-        ( dcUnit-        , takeNameOfDaCon-        , takeTypeOfDaCon--        , bindsOfPat--        , wApp-        , wApps-        , takeXWitness-        , takeWAppsAsList-        , takePrimWiConApps)-        ---- Annotations ------------------------------------------------------------------- | Take the outermost annotation from an expression,---   or Nothing if this is an `XType` or `XWitness` without an annotation.-takeAnnotOfExp :: 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-        XApp  a _ _     -> Just a-        XLet  a _ _     -> Just a-        XCase a _ _     -> Just a-        XCast a _ _     -> Just a-        XType{}         -> Nothing-        XWitness{}      -> Nothing-        XDefix a _      -> Just a-        XInfixOp  a _   -> Just a-        XInfixVar a _   -> Just a----- Lambdas ------------------------------------------------------------------------ | Make some nested type lambdas.-xLAMs :: 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 :: 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 :: 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)-   in   case go [] xx of-         ([], _)        -> Nothing-         (bs, body)     -> Just (bs, body)----- | Split nested value or witness lambdas from the front of an expression,---   or `Nothing` if there aren't any.-takeXLams :: 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)-   in   case go [] xx of-         ([], _)        -> Nothing-         (bs, body)     -> Just (bs, body)----- | Make some nested lambda abstractions,---   using a flag to indicate whether the lambda is a---   level-1 (True), or level-0 (False) binder.-makeXLamFlags :: GAnnot l -> [(Bool, GBind l)] -> GExp l -> GExp l-makeXLamFlags a fbs x- = foldr (\(f, b) x'-           -> if f then XLAM a b x'-                   else XLam a b x')-                x fbs----- | Split nested lambdas from the front of an expression, ---   with a flag indicating whether the lambda was a level-1 (True), ---   or level-0 (False) binder.-takeXLamFlags :: 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-        go bs x            = (reverse bs, x)-   in   case go [] xx of-         ([], _)        -> Nothing-         (bs, body)     -> Just (bs, body)----- Applications ------------------------------------------------------------------ | Build sequence of value applications.-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 :: GExp l -> [(GExp l, GAnnot l)] -> GExp l-makeXAppsWithAnnots f xas- = case xas of-        []              -> f-        (arg,a ) : as   -> makeXAppsWithAnnots (XApp a f arg) as----- | Flatten an application into the function part and its arguments.------   Returns `Nothing` if there is no outer application.-takeXApps :: GExp l -> Maybe (GExp l, [GExp l])-takeXApps xx- = case takeXAppsAsList xx of-        (x1 : xsArgs)   -> Just (x1, xsArgs)-        _               -> Nothing----- | Flatten an application into the function part and its arguments.------   This is like `takeXApps` above, except we know there is at least one argument.-takeXApps1 :: GExp l -> GExp l -> (GExp l, [GExp l])-takeXApps1 x1 x2- = case takeXApps x1 of-        Nothing          -> (x1,  [x2])-        Just (x11, x12s) -> (x11, x12s ++ [x2])----- | Flatten an application into the function parts and arguments, if any.-takeXAppsAsList  :: GExp l -> [GExp l]-takeXAppsAsList xx- = case xx of-        XApp _ x1 x2    -> takeXAppsAsList x1 ++ [x2]-        _               -> [xx]----- | Destruct sequence of applications.---   Similar to `takeXAppsAsList` but also keeps annotations for later.-takeXAppsWithAnnots :: GExp l -> (GExp l, [(GExp l, GAnnot l)])-takeXAppsWithAnnots xx- = case xx of-        XApp a f arg-         -> let (f', args') = takeXAppsWithAnnots f-            in  (f', args' ++ [(arg,a)])--        _ -> (xx, [])----- | Flatten an application of a primop into the variable---   and its arguments.---   ---   Returns `Nothing` if the expression isn't a primop application.-takeXPrimApps :: GExp l -> Maybe (GPrim l, [GExp l])-takeXPrimApps xx- = case takeXAppsAsList xx of-        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 :: 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) []--

@@ -8,41 +8,32 @@         , runConvertM) where import DDC.Source.Tetra.Convert.Error-import DDC.Data.SourcePos+import DDC.Source.Tetra.Convert.Witness+import DDC.Source.Tetra.Convert.Clause+import DDC.Source.Tetra.Convert.Type+import DDC.Source.Tetra.Convert.Prim+import DDC.Source.Tetra.Convert.Base -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.Source.Tetra.Exp                   as S+import qualified DDC.Source.Tetra.Env                   as Env +import qualified DDC.Core.Tetra.Compounds               as C 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 qualified Text.Show.Pretty                       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@@ -50,8 +41,8 @@ -- | Convert a Source Tetra module to Core Tetra. coreOfSourceModule          :: SP-        -> S.Module (S.Annot SP)-        -> Either (ErrorConvert SP) (C.Module SP C.Name)+        -> S.Module S.Source+        -> Either (ErrorConvert S.Source) (C.Module SP C.Name)  coreOfSourceModule a mm         = runConvertM @@ -69,46 +60,54 @@ --  coreOfSourceModuleM         :: SP-        -> S.Module (S.Annot SP)-        -> ConvertM SP (C.Module SP C.Name)+        -> S.Module S.Source+        -> ConvertM S.Source (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+        exportTypes'    +         <- sequence+         $  fmap (\n -> (,) <$> toCoreTUCN n +                            <*> (fmap ExportSourceLocalNoType $ toCoreTUCN n))+         $  S.moduleExportTypes mm -        exportValues'   <- sequence-                        $  fmap (\n-                                -> (,)  <$> (pure $ toCoreN n)-                                        <*> (pure $ ExportSourceLocalNoType (toCoreN n)))-                        $  S.moduleExportValues mm+        exportValues'   +         <- sequence+         $  fmap (\n -> (,) <$> toCoreXUVN n+                            <*> (fmap ExportSourceLocalNoType (toCoreXUVN 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+        -- Imported types, capabilities and values.+        importTypes'    +         <- sequence+         $  fmap (\(n, it) -> (,) <$> toCoreTBCN n <*> (toCoreImportType it))+         $  S.moduleImportTypes  mm -        importValues'   <- sequence -                        $  fmap (\(n, iv) -                                -> (,)  <$> (pure $ toCoreN n) <*> (toCoreImportValue iv))-                        $  S.moduleImportValues mm+        importCaps'     +         <- sequence +         $  fmap (\(n, iv) -> (,) <$> toCoreXBVN n <*> toCoreImportCap   iv)+         $  S.moduleImportCaps   mm +        importValues'+         <- sequence +         $  fmap (\(n, iv) -> (,) <$> toCoreXBVN n <*> toCoreImportValue iv)+         $  S.moduleImportValues mm+         -- Data type definitions.-        dataDefsLocal   <- sequence $ fmap toCoreDataDef -                        $  [ def | S.TopData _ def <- S.moduleTops mm ]+        dataDefsLocal +         <- sequence $ fmap toCoreDataDef +         $  [ def    | S.TopData _ def <- S.moduleTops mm ] +        -- Type equations.+        typeDefsLocal+         <- sequence $ fmap toCoreTypeDef +         $  [ (b, t) | S.TopType _ b t <- S.moduleTops mm ]+         -- Top level bindings.-        ltsTops         <- letsOfTops $  S.moduleTops mm+        ltsTops+         <- letsOfTops $  S.moduleTops mm          return          $ C.ModuleCore@@ -120,131 +119,100 @@                 , C.moduleExportValues                    =  exportValues'                    ++ (if C.isMainModuleName (S.moduleName mm)-                        && (not $ elem (S.NameVar "main") $ S.moduleExportValues mm)+                        && (not $ elem (S.UName (Text.pack "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.moduleImportTypeDefs = []                 , C.moduleDataDefsLocal  = dataDefsLocal+                , C.moduleTypeDefsLocal  = typeDefsLocal                 , 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 :: [S.Top S.Source] +           -> ConvertM S.Source (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))+ = do   +        -- Collect up the type signatures defined at top level.+        let cls         = [cl   | S.TopClause _ cl      <- tops]+        let sigs        = collectSigsFromClauses      cls+        let vals        = collectBoundVarsFromClauses cls -bindOfTop (S.TopClause _ (S.SLet _ b [] [S.GExp x]))- = Just ((,) <$> toCoreB b <*> toCoreX x)+        bxps            <- fmap catMaybes +                        $  mapM (makeBindingFromClause sigs vals) cls -bindOfTop _     - = Nothing+        let (bms, xps)  =  unzip bxps+        bs'             <- mapM (toCoreBM UniverseSpec) bms+        xs'             <- mapM (\(sp, x) -> toCoreX sp x) xps+        return $ C.LRec $ zip bs' xs'   -- ImportType --------------------------------------------------------------------------------------toCoreImportType :: ImportType S.Name -> ConvertM a (ImportType C.Name)+toCoreImportType +        :: ImportType n S.Type+        -> ConvertM a (ImportType C.Name (C.Type C.Name))+ toCoreImportType src  = case src of         ImportTypeAbstract t    -         -> ImportTypeAbstract <$> toCoreT t+         -> ImportTypeAbstract <$> toCoreT UniverseKind t          ImportTypeBoxed t-         -> ImportTypeBoxed    <$> toCoreT t+         -> ImportTypeBoxed    <$> toCoreT UniverseKind t   -- ImportCap ---------------------------------------------------------------------------------------toCoreImportCap :: ImportCap S.Name -> ConvertM a (ImportCap C.Name)+toCoreImportCap +        :: ImportCap S.Bind S.Type+        -> ConvertM a (ImportCap C.Name (C.Type C.Name))+ toCoreImportCap src  = case src of         ImportCapAbstract t-         -> ImportCapAbstract   <$> toCoreT t+         -> ImportCapAbstract   <$> toCoreT UniverseSpec t   -- ImportValue -------------------------------------------------------------------------------------toCoreImportValue :: ImportValue S.Name -> ConvertM a (ImportValue C.Name)+toCoreImportValue +        :: ImportValue S.Bind S.Type+        -> ConvertM a (ImportValue C.Name (C.Type C.Name))+ toCoreImportValue src  = case src of         ImportValueModule mn n t mA          ->  ImportValueModule -         <$> (pure mn) <*> (pure $ toCoreN n) <*> toCoreT t <*> pure mA+         <$> pure mn    <*> toCoreXBVN n +                        <*> toCoreT UniverseSpec 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+         <$> pure v     <*> toCoreT UniverseSpec t   -- DataDef -----------------------------------------------------------------------------------------toCoreDataDef :: S.DataDef S.Name -> ConvertM a (C.DataDef C.Name)+toCoreDataDef :: S.DataDef S.Source -> ConvertM a (C.DataDef C.Name) toCoreDataDef def  = do-        defParams       <- sequence $ fmap toCoreB $ S.dataDefParams def+        defParams       <- sequence $ fmap toCoreTBK $ S.dataDefParams def          defCtors        <- sequence $ fmap (\(ctor, tag) -> toCoreDataCtor def tag ctor)                                     $ [(ctor, tag) | ctor <- S.dataDefCtors def                                                    | tag  <- [0..]] +        let (S.TyConBindName txTyConName) = S.dataDefTypeName def+         return $ C.DataDef-         { C.dataDefTypeName    = toCoreN     $ S.dataDefTypeName def+         { C.dataDefTypeName    = C.NameCon (Text.unpack txTyConName)          , C.dataDefParams      = defParams          , C.dataDefCtors       = Just $ defCtors          , C.dataDefIsAlgebraic = True }@@ -252,119 +220,142 @@  -- DataCtor --------------------------------------------------------------------------------------- toCoreDataCtor -        :: S.DataDef S.Name +        :: S.DataDef  S.Source         -> Integer-        -> S.DataCtor S.Name +        -> S.DataCtor S.Source         -> 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)+ = do   typeParams      <- sequence $ fmap toCoreTBK $ S.dataDefParams dataDef+        fieldTypes      <- sequence $ fmap (toCoreT UniverseSpec)   $ S.dataCtorFieldTypes ctor+        resultType      <- toCoreT UniverseSpec (S.dataCtorResultType ctor)+        let (S.TyConBindName txTyConName) = S.dataDefTypeName dataDef          return $ C.DataCtor-         { C.dataCtorName        = toCoreN (S.dataCtorName ctor)+         { C.dataCtorName        = toCoreDaConBind (S.dataCtorName ctor)          , C.dataCtorTag         = tag          , C.dataCtorFieldTypes  = fieldTypes          , C.dataCtorResultType  = resultType-         , C.dataCtorTypeName    = toCoreN (S.dataDefTypeName dataDef) +         , C.dataCtorTypeName    = C.NameCon (Text.unpack txTyConName)          , C.dataCtorTypeParams  = typeParams }   -- Exp ---------------------------------------------------------------------------------------------toCoreX :: S.Exp SP -> ConvertM SP (C.Exp SP C.Name)-toCoreX xx+toCoreX :: SP -> S.Exp -> ConvertM S.Source (C.Exp SP C.Name)+toCoreX a xx  = case xx of-        S.XVar a u      -         -> C.XVar  <$> pure a <*> toCoreU  u+        S.XAnnot a' x+         -> toCoreX a' x +        S.XVar 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.XCon dc@(C.DaConPrim (S.DaConBoundLit (S.PrimLitTextLit{})) _)+         -> 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.XPrim p+         -> do  let p'  =  toCorePrimVal p +                t'      <- toCoreT UniverseSpec  $ Env.typeOfPrimVal p+                return  $ C.XVar a (C.UPrim p' t') -        S.XCon a dc-         -> C.XCon  <$> pure a <*> toCoreDC dc+        S.XCon  dc+         -> C.XCon      <$> pure a <*> toCoreDC dc -        S.XLAM a b x-         -> C.XLAM  <$> pure a <*> toCoreB b  <*> toCoreX x+        S.XLAM  bm x+         -> C.XLAM      <$> pure a <*> toCoreBM UniverseKind bm  <*> toCoreX a x -        S.XLam a b x-         -> C.XLam  <$> pure a <*> toCoreB b  <*> toCoreX x+        S.XLam  bm x+         -> C.XLam      <$> pure a <*> toCoreBM UniverseSpec bm  <*> toCoreX a 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 _ _+        S.XApp  _ _          |  Just ( p@(S.PrimValError S.OpErrorDefault)-                 , [S.XCon a1 dc1, S.XCon a2 dc2])+                 , [S.XCon dc1, S.XCon dc2])                  <- S.takeXPrimApps xx-         -> do  xPrim'  <- toCoreX (S.XPrim a0 p)+         -> do  xPrim'  <- toCoreX  a (S.XPrim p)                 dc1'    <- toCoreDC dc1                 dc2'    <- toCoreDC dc2-                return  $  C.xApps a0 xPrim' [C.XCon a1 dc1', C.XCon a2 dc2']+                return  $  C.xApps a xPrim' [C.XCon a dc1', C.XCon a dc2'] -        S.XApp a x1 x2-         -> C.XApp  <$> pure a <*> toCoreX x1 <*> toCoreX x2+        S.XApp x1 x2+         -> C.XApp      <$> pure a  <*> toCoreX a x1 <*> toCoreX a x2 -        S.XLet a lts x-         -> C.XLet  <$> pure a <*> toCoreLts lts <*> toCoreX x+        S.XLet lts x+         -> C.XLet      <$> pure a  <*> toCoreLts a lts <*> toCoreX a x -        S.XCase a x alts-         -> C.XCase <$> pure a <*> toCoreX x <*> (sequence $ map (toCoreA a) alts)+        S.XCase x alts+         -> C.XCase     <$> pure a  <*> toCoreX a x +                                    <*> (sequence $ map (toCoreA a) alts) -        S.XCast a c x-         -> C.XCast <$> pure a <*> toCoreC c <*> toCoreX x+        S.XCast c x+         -> C.XCast     <$> pure a  <*> toCoreC a c <*> toCoreX a x -        S.XType a t-         -> C.XType    <$> pure a <*> toCoreT t+        S.XType t+         -> C.XType     <$> pure a  <*> toCoreT UniverseSpec t -        S.XWitness a w-         -> C.XWitness <$> pure a <*> toCoreW w+        S.XWitness w+         -> C.XWitness  <$> pure a  <*> toCoreW a 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+        S.XDefix{}      -> Left $ ErrorConvertSugaredExp xx+        S.XInfixOp{}    -> Left $ ErrorConvertSugaredExp xx+        S.XInfixVar{}   -> Left $ ErrorConvertSugaredExp xx+        S.XMatch{}      -> Left $ ErrorConvertSugaredExp xx+        S.XWhere{}      -> Left $ ErrorConvertSugaredExp xx+        S.XLamPat{}     -> Left $ ErrorConvertSugaredExp xx+        S.XLamCase{}    -> Left $ ErrorConvertSugaredExp xx           -- Lets --------------------------------------------------------------------------------------------toCoreLts :: S.Lets SP -> ConvertM SP (C.Lets SP C.Name)-toCoreLts lts+toCoreLts :: SP -> S.Lets -> ConvertM S.Source (C.Lets SP C.Name)+toCoreLts a lts  = case lts of         S.LLet b x-         -> C.LLet <$> toCoreB b <*> toCoreX x+         -> C.LLet <$> toCoreBM UniverseSpec b <*> toCoreX a x                  S.LRec bxs-         -> C.LRec <$> (sequence $ map (\(b, x) -> (,) <$> toCoreB b <*> toCoreX x) bxs)+         -> C.LRec <$> (sequence +                $ map (\(b, x) -> (,) <$> toCoreBM UniverseSpec b <*> toCoreX a x) bxs) -        S.LPrivate bks Nothing bts-         -> C.LPrivate <$> (sequence $ fmap toCoreB bks) -                       <*>  pure Nothing -                       <*> (sequence $ fmap toCoreB bts)+        S.LPrivate bs Nothing bts+         -> C.LPrivate +                <$> (sequence  $ fmap (toCoreBM UniverseKind)+                               $ [S.XBindVarMT b (Just S.KRegion) | b <- bs])+                <*>  pure Nothing +                <*> (sequence  $ fmap toCoreTBK bts) -        S.LPrivate bks (Just tParent) bts-         -> C.LPrivate <$> (sequence $ fmap toCoreB bks) -                       <*> (fmap Just $ toCoreT tParent)-                       <*> (sequence $ fmap toCoreB bts)+        S.LPrivate bs (Just tParent) bts+         -> C.LPrivate +                <$> (sequence  $ fmap (toCoreBM UniverseKind)+                               $ [S.XBindVarMT b (Just S.KRegion) | b <- bs])+                <*> (fmap Just $ toCoreT UniverseKind tParent)+                <*> (sequence  $ fmap toCoreTBK bts) -        S.LGroup{}-         -> Left $ ErrorConvertCannotConvertSugarLets lts+        S.LGroup cls+         -> do  let sigs  = collectSigsFromClauses cls+                let vals  = collectBoundVarsFromClauses cls +                bxs       <- fmap catMaybes+                          $  mapM (makeBindingFromClause sigs vals) cls +                let bxs' = [(b, x) | (b, (_, x)) <- bxs]+                toCoreLts a (S.LRec bxs')++ -- Cast --------------------------------------------------------------------------------------------toCoreC :: S.Cast a -> ConvertM a (C.Cast a C.Name)-toCoreC cc+toCoreC :: SP -> S.Cast -> ConvertM S.Source (C.Cast SP C.Name)+toCoreC a cc  = case cc of         S.CastWeakenEffect eff-         -> C.CastWeakenEffect <$> toCoreT eff+         -> C.CastWeakenEffect <$> toCoreT UniverseSpec eff          S.CastPurify w-         -> C.CastPurify       <$> toCoreW w+         -> C.CastPurify       <$> toCoreW a w          S.CastBox          -> pure C.CastBox@@ -374,142 +365,73 @@   -- 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))+toCoreA  :: SP -> S.AltCase -> ConvertM S.Source (C.Alt SP C.Name)+toCoreA sp alt+ = case alt of+        S.AAltCase w [S.GExp x]+         -> C.AAlt <$> toCoreP alt w <*> toCoreX sp x +        _ -> error $ unlines+                [ "ddc-source-tetra: cannot convert sugared alt"       +                , Text.ppShow alt] + -- Pat ---------------------------------------------------------------------------------------------toCoreP  :: S.Pat a -> ConvertM a (C.Pat C.Name)-toCoreP pp+toCoreP  :: S.AltCase -> S.Pat -> ConvertM a (C.Pat C.Name)+toCoreP aa pp  = case pp of-        S.PDefault        +        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+        S.PAt{}+         -> error $ unlines+                  [ "ddc-source-tetra: cannot convert PAt pattern"+                  , Text.ppShow pp] +        S.PVar{}+         -> error $ unlines+                  [ "ddc-source-tetra: cannot convert PVar pattern"+                  , Text.ppShow aa] --- 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+        S.PData dc bs+         -> C.PData <$> toCoreDC dc <*> (sequence $ fmap toCorePasB bs)  --- 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-+-- | Convert a pattern to a core binder.+--   Only default and var patterns are supported,+--   nested patterns need to have been eliminated by the desugarer.+toCorePasB :: S.Pat -> ConvertM a (C.Bind C.Name)+toCorePasB pp+ = let  hole = C.TVar (C.UName C.NameHole)+   in   case pp of+         S.PDefault+          -> pure $ C.BAnon hole --- Bound -------------------------------------------------------------------------------------------toCoreU :: S.Bound -> ConvertM a (C.Bound C.Name)-toCoreU uu- = case uu of-        T.UName n-         -> T.UName <$> (pure $ toCoreN n)+         S.PAt{}+          -> error $ "ddc-source-tetra: cannot convert at pattern "     ++ Text.ppShow pp -        T.UIx   i-         -> T.UIx   <$> (pure i)+         S.PVar b+          -> do b'      <- toCoreB b+                return  b' -        T.UPrim n t-         -> T.UPrim <$> (pure $ toCoreN n) <*> toCoreT t+         S.PData{}+          -> error $ "ddc-source-tetra: cannot convert nested pattern " ++ Text.ppShow pp  --- 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+-- DaCon ------------------------------------------------------------------------------------------+toCoreDC :: S.DaCon S.DaConBound S.Type+         -> ConvertM a (C.DaCon C.Name (C.Type (C.Name))) -        S.NamePrim (S.PrimNameVal (S.PrimValFun   p))-         -> C.NameOpFun     p+toCoreDC dc+ = case dc of+        S.DaConUnit+         -> pure $ C.DaConUnit -        S.NamePrim (S.PrimNameVal (S.PrimValError p))-         -> C.NameOpError   p False+        S.DaConPrim  n t +         -> C.DaConPrim  <$> (pure $ toCoreDaConBound n) <*> toCoreT UniverseSpec t -        S.NameHole-         -> C.NameHole+        S.DaConBound n+         -> C.DaConBound <$> (pure $ toCoreDaConBound n)  --- | 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,21 @@++module DDC.Source.Tetra.Convert.Base+        ( ConvertM+        , SP++        , module DDC.Type.Universe+        , module DDC.Source.Tetra.Convert.Error+        , module DDC.Data.SourcePos)+where+import DDC.Type.Universe+import DDC.Source.Tetra.Convert.Error+import DDC.Data.SourcePos+++type ConvertM a x+        = Either (ErrorConvert a) x+++type SP = SourcePos++

@@ -0,0 +1,99 @@++module DDC.Source.Tetra.Convert.Clause+        ( collectSigsFromClauses+        , collectBoundVarsFromClauses+        , makeBindingFromClause)+where+import DDC.Source.Tetra.Convert.Error+import DDC.Source.Tetra.Convert.Base+import qualified DDC.Source.Tetra.Exp                   as S+++-- | Collect type signatures defined in a clause group.+collectSigsFromClauses      :: [S.Clause] -> [(S.BindVar, S.Type)]+collectSigsFromClauses cls+ = go cls+ where  go (S.SSig _ b t : cls')+                        = (b, t) : go cls'+        go (_ : cls')   = go cls'+        go []           = []+++-- | Collect binders for values defined in a clause group.+collectBoundVarsFromClauses :: [S.Clause] -> [S.BindVar]+collectBoundVarsFromClauses cls+ = go cls+ where  go (S.SLet _ (S.XBindVarMT b _) _ _ : cls') +                        = b : go cls'+        go (_ : cls')   = go cls'+        go []           = []+++-- | Strip a let-binding from a clause.+makeBindingFromClause+        :: [(S.BindVar, S.Type)]        -- ^ Type signatures in the same group. +        -> [ S.BindVar ]                -- ^ Bound values defined in the same group.+        -> S.Clause                     -- ^ Clause to consider.+        -> ConvertM S.Source +                    (Maybe (S.BindVarMT, (SP, S.Exp)))+                                        -- ^ Let-bindings with attached signatures.+makeBindingFromClause sigs vals cc+ = case cc of+        S.SLet sp bm@(S.XBindVarMT b mtHas) ps [S.GExp x]+         -- See if there was a type signature specified in the same group.+         |  Just tSig   <- lookup b sigs+         -> case mtHas of+                -- If the binder was already directly annotated with a signature+                -- then throw an error, as it might conflict with the separate+                -- signature provided in the same group.+                Just _          -> Left   $ ErrorMultipleSignatures sp b++                -- The binder was not directly annotated, +                -- so attach the provided signature.+                Nothing +                 -> case wrapParams ps x of+                        Nothing -> Left   $ ErrorConvertSugaredClause cc+                        Just x' -> return $ Just $ ( S.XBindVarMT b (Just tSig), (sp, x'))++         -- We don't have a separate signature for this binding.+         |  otherwise   +         -> case wrapParams ps x of+                Nothing         -> Left   $ ErrorConvertSugaredClause cc+                Just x'         -> return $ Just $ (bm, (sp, x'))++        -- Some let binding with an expression that should have+        -- been desugared earlier.+        S.SLet{}                -> Left   $ ErrorConvertSugaredClause cc++        -- Check that signatures in the clause group have associated bindings.+        --   If we find a signature without a binding then one or +        --   the other is probably mis-spelled.+        S.SSig sp b _ +         | elem b vals          -> return Nothing+         | otherwise            -> Left   $ ErrorTypeSignatureLacksBinding sp b+++-- | Wrap an expression with lambda abstractions for each +--   of the given parameters.+wrapParams :: [S.Param] -> S.Exp -> Maybe S.Exp+wrapParams [] x + = pure x++wrapParams (p:ps) x+ = case p of+        S.MType    b mt    +         -> S.XLAM (S.XBindVarMT b mt)       <$> wrapParams ps x++        S.MWitness b mt+         -> S.XLam (S.XBindVarMT b mt)       <$> wrapParams ps x++        S.MValue   S.PDefault mt+         -> S.XLam (S.XBindVarMT S.BNone mt) <$> wrapParams ps x++        S.MValue   (S.PVar b) mt+         -> S.XLam (S.XBindVarMT b mt)       <$> wrapParams ps x++        -- Some pattern that should have been desugared earlier.+        S.MValue   _ _+         -> Nothing+

@@ -1,27 +1,53 @@-+{-# LANGUAGE UndecidableInstances #-} module DDC.Source.Tetra.Convert.Error         (ErrorConvert (..)) where+import DDC.Data.SourcePos import DDC.Source.Tetra.Pretty-import qualified DDC.Source.Tetra.Exp.Annot   as S+import DDC.Source.Tetra.Exp.Generic  -data ErrorConvert a-        -- | Cannot convert sugar expression to core.-        = ErrorConvertCannotConvertSugarExp  (S.Exp a)+-- | Things that can go wrong when converting source to core.+data ErrorConvert l+        -- | Cannot convert sugared expression to core.+        --   This should have been desugared in a prior pass.+        = ErrorConvertSugaredExp    (GExp l) -        -- | Cannot convert sugar let bindings to core.-        | ErrorConvertCannotConvertSugarLets (S.Lets a)+        -- | Cannot convert sugared let bindings to core.+        --   This should have been desugared in a prior pass.+        | ErrorConvertSugaredLets   (GLets l) +        -- | Cannot convert sugared clause to core.+        --   This should have been desugared in a prior pass.+        | ErrorConvertSugaredClause (GClause l) -instance Pretty a => Pretty (ErrorConvert a) where- ppr err-  = case err of-        ErrorConvertCannotConvertSugarExp xx-         -> vcat [ text "Cannot desugar expression"-                 , indent 2 $ ppr xx ]+        -- | Found multiple type signatures for the same binder.+        --   This should have been desugared in a prior pass.+        | ErrorMultipleSignatures        SourcePos (GXBindVar l) -        ErrorConvertCannotConvertSugarLets xx-         -> vcat [ text "Cannot desugar let-bindings"-                 , indent 2 $ ppr xx ]+        -- | Type signature lacks associated value-level binding.+        | ErrorTypeSignatureLacksBinding SourcePos (GXBindVar l) ++instance (PrettyLanguage l) => Pretty (ErrorConvert l) where+ ppr = pprError++pprError (ErrorConvertSugaredExp xx)+ = vcat [ text "Cannot convert sugared expression"+        , indent 2 $ ppr xx ]++pprError (ErrorConvertSugaredLets xx)+ = vcat [ text "Cannot convert sugared let-bindings"+        , indent 2 $ ppr xx ]++pprError (ErrorConvertSugaredClause l)+ = vcat [ text "Cannot convert sugared let-bindings"+        , indent 2 $ ppr l ]++pprError (ErrorMultipleSignatures sp b)+ = vcat [ ppr sp+        , text "Multiple type signatures specified for " <> ppr b ]++pprError (ErrorTypeSignatureLacksBinding sp b)+ = vcat [ ppr sp+        , text "Type signature lacks associated binding " <> ppr b]

@@ -0,0 +1,45 @@++module DDC.Source.Tetra.Convert.Prim+        ( toCoreTyConTetra+        , toCorePrimVal+        , toCorePrimLit)+where+import qualified DDC.Core.Tetra.Prim    as C+import qualified DDC.Source.Tetra.Prim  as S+++-- | 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+++-- | Convert a value primtivie to a core name.+toCorePrimVal :: S.PrimVal -> C.Name+toCorePrimVal pv+ = case pv of+        S.PrimValArith  p       -> C.NamePrimArith  p False+        S.PrimValCast   p       -> C.NamePrimCast   p False+        S.PrimValError  p       -> C.NameOpError    p False+        S.PrimValVector p       -> C.NameOpVector   p False+        S.PrimValFun    p       -> C.NameOpFun      p+        S.PrimValLit    p       -> toCorePrimLit    p+++-- | Convert a primitive literal to a core name.+toCorePrimLit :: S.PrimLit -> C.Name+toCorePrimLit pl+ = case pl 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.PrimLitChar    x      -> C.NameLitChar    x+        S.PrimLitTextLit x      -> C.NameLitTextLit x

@@ -0,0 +1,241 @@++module DDC.Source.Tetra.Convert.Type+        ( toCoreTypeDef++        , toCoreT+        , toCoreTC++        , toCoreTBCN,   toCoreTUCN+        , toCoreXUVN,   toCoreXBVN++        , toCoreTBK++        , toCoreB,      toCoreBM+        , toCoreU+        , toCoreDaConBind+        , toCoreDaConBound)+where+import DDC.Source.Tetra.Convert.Prim+import DDC.Source.Tetra.Convert.Base+import DDC.Type.Universe                                (Universe (..), universeUp)++import qualified DDC.Source.Tetra.Exp                   as S+import qualified DDC.Source.Tetra.Prim                  as S++import qualified DDC.Core.Tetra.Compounds               as C+import qualified DDC.Core.Tetra.Prim                    as C+import qualified DDC.Type.Sum                           as CSum+import qualified Data.Text                              as Text+++-- TypeDef ----------------------------------------------------------------------------------------+toCoreTypeDef+        :: (S.TyConBind, S.Type)+        -> ConvertM a (C.Name, (C.Kind C.Name, C.Type C.Name))++toCoreTypeDef (b, t)+ = do   n       <- toCoreTBCN b+        t'      <- toCoreT UniverseSpec t+        let hole = C.TVar (C.UName C.NameHole)+        return  (n, (hole, t'))+++-- Type -------------------------------------------------------------------------------------------+toCoreT :: Universe -> S.Type -> ConvertM a (C.Type C.Name)+toCoreT uu tt+ = case tt of+        S.TAnnot _ t+         -> toCoreT uu t++        S.TCon (S.TyConBot k)     +         -> do  k'      <- toCoreT uu k+                return  $ C.tBot k'++        S.TCon (S.TyConVoid)+         -> do  return  $ C.tVoid++        S.TCon tc+         -> do  mtc'    <- toCoreTC uu tc+                case mtc' of+                 Nothing        -> error  $ "ddc-soure-tetra.toCoreT: " ++ show tt+                 Just tc'       -> return $ C.TCon tc'++        S.TVar u+         -> C.TVar <$> toCoreU  u++        S.TAbs b k t+         -> do  b'      <- toCoreTBK (b, k)+                t'      <- toCoreT uu  t+                return  $  C.TAbs b' t'++        S.TApp (S.TCon (S.TyConForall _)) (S.TAbs b k t)+         -> let uu'     =  universeUp uu+            in  C.TForall <$> toCoreBM uu' (S.XBindVarMT b (Just k)) <*> toCoreT uu t++        S.TApp{}+         | Just (k, ts) <- S.takeTUnions tt+         -> do  let uu' =  universeUp uu+                k'      <- toCoreT uu' k+                ts'     <- sequence $ fmap (toCoreT uu) ts+                return  $  C.TSum (CSum.fromList k' ts')++        S.TApp t1 t2+         -> C.TApp      <$> toCoreT uu t1 <*> toCoreT uu t2++++-- TyCon ------------------------------------------------------------------------------------------+-- | Convert a Source TyCon to Core, or Nothing if it cannot be converted in isolation.+toCoreTC :: Universe -> S.TyCon -> ConvertM a (Maybe (C.TyCon C.Name))+toCoreTC uu tc+ = case tc of+        S.TyConVoid             -> return Nothing+        S.TyConUnit             -> return $ Just $ C.TyConSpec C.TcConUnit++        S.TyConFun       +         -> case uu of+                UniverseSpec    -> return $ Just $ C.TyConSpec C.TcConFun+                UniverseKind    -> return $ Just $ C.TyConKind C.KiConFun+                _               -> return Nothing+++        S.TyConUnion _   -> return Nothing++        S.TyConBot _k    -> return Nothing+        S.TyConForall _k -> return Nothing+        S.TyConExists _k -> return Nothing++        -- Primitive type constructors.+        S.TyConPrim pt+         -> case pt of+                -- Ambient TyCons+                S.PrimTypeSoCon sc -> return $ Just $ C.TyConSort    sc+                S.PrimTypeKiCon kc -> return $ Just $ C.TyConKind    kc+                S.PrimTypeTwCon tw -> return $ Just $ C.TyConWitness tw+                S.PrimTypeTcCon ts -> return $ Just $ C.TyConSpec    ts++                -- Primitive TyCons+                S.PrimTypeTyCon tcy+                 -> do  k       <- toCoreT UniverseKind $ S.kindPrimTyCon tcy+                        return  $ Just $ C.TyConBound (C.UPrim (C.NamePrimTyCon tcy) k) k++                S.PrimTypeTyConTetra tct +                 -> do  k       <- toCoreT UniverseKind $ S.kindPrimTyConTetra tct+                        let tct' =  toCoreTyConTetra tct+                        return  $ Just $ C.TyConBound (C.UPrim (C.NameTyConTetra tct') k) k++        -- Bound type constructors.+        --   The embedded kind is set to Bot. We rely on the spreader+        --   to fill in the real kind before type checking.+        S.TyConBound (S.TyConBoundName tx)+         -> return $ Just +         $  C.TyConBound (C.UName (C.NameCon (Text.unpack tx))) +                                  (C.TVar (C.UName C.NameHole))+++-- Bind -------------------------------------------------------------------------------------------+-- | Convert a type constructor binding occurrence to a core name.+toCoreTBCN :: S.GTBindCon S.Source  -> ConvertM a C.Name+toCoreTBCN (S.TyConBindName n)+ = return $ C.NameCon (Text.unpack n)+++-- | Convert a type constructor bound occurrence to a core name.+toCoreTUCN :: S.GTBoundCon S.Source -> ConvertM a C.Name+toCoreTUCN (S.TyConBoundName n)+ = return $ C.NameCon (Text.unpack n)+++-- | Convert a term variable bound occurrence to a core name.+toCoreXUVN :: S.Bound -> ConvertM a C.Name+toCoreXUVN uu+ = case uu of+        S.UName n -> return $ C.NameVar (Text.unpack n)+        S.UIx  _i -> error "ddc-source-tetra.toCoreXBVN: anon bound"+        S.UHole   -> return $ C.NameHole        +++toCoreXBVN  :: S.GTBindVar S.Source -> ConvertM a C.Name+toCoreXBVN bb+ = case bb of+        S.BNone   -> error "ddc-source-tetra.toCoreXBVN: none bound"+        S.BAnon   -> error "ddc-source-tetra.toCoreXBVN: anon bound"+        S.BName n -> return $ C.NameVar (Text.unpack n)+++-- | Convert a type binder and kind to core.+toCoreTBK :: (S.GTBindVar S.Source, S.GType S.Source)+          -> ConvertM a (C.Bind C.Name)+toCoreTBK (bb, k)+ = case bb of+        S.BNone   -> C.BNone <$> (toCoreT UniverseKind k)+        S.BAnon   -> C.BAnon <$> (toCoreT UniverseKind k)+        S.BName n -> C.BName <$> (return $ C.NameVar (Text.unpack n)) +                             <*> (toCoreT UniverseKind k)+++-- | Convert an unannoted binder to core.+toCoreB  :: S.Bind -> ConvertM a (C.Bind C.Name)+toCoreB bb+ = let hole     = C.TVar (C.UName C.NameHole)+   in case bb of+        S.BNone   -> return $ C.BNone hole+        S.BAnon   -> return $ C.BAnon hole+        S.BName n -> return $ C.BName (C.NameVar (Text.unpack n)) hole+++-- | Convert a possibly annoted binding occurrence of a variable to core.+toCoreBM :: Universe -> S.GXBindVarMT S.Source -> ConvertM a (C.Bind C.Name)+toCoreBM uu bb+ = case bb of+        S.XBindVarMT S.BNone     (Just t)+         -> C.BNone <$> toCoreT uu t++        S.XBindVarMT S.BNone     Nothing+         -> C.BNone <$> (return $ C.TVar (C.UName C.NameHole))+++        S.XBindVarMT S.BAnon     (Just t)   +         -> C.BAnon <$> toCoreT uu t++        S.XBindVarMT S.BAnon     Nothing    +         -> C.BAnon <$> (return $ C.TVar (C.UName C.NameHole))+++        S.XBindVarMT (S.BName n) (Just t)+         -> C.BName <$> (return $ C.NameVar (Text.unpack n)) +                    <*> toCoreT uu t++        S.XBindVarMT (S.BName n) Nothing    +         -> C.BName <$> (return $ C.NameVar (Text.unpack n)) +                    <*> (return $ C.TVar (C.UName C.NameHole))+++-- Bound ------------------------------------------------------------------------------------------+toCoreU :: S.Bound -> ConvertM a (C.Bound C.Name)+toCoreU uu+ = case uu of+        S.UName n       -> C.UName <$> pure (C.NameVar (Text.unpack n))+        S.UIx   i       -> C.UIx   <$> (pure i)+        S.UHole         -> C.UName <$> pure (C.NameHole)+++-- Name -------------------------------------------------------------------------------------------+-- | Convert a binding occurrences of a data constructor to a core name.+toCoreDaConBind :: S.DaConBind -> C.Name+toCoreDaConBind (S.DaConBindName tx)+ = C.NameCon (Text.unpack tx)+++-- | Convert a bound occurrence of a data constructor to a core name.+toCoreDaConBound :: S.DaConBound -> C.Name+toCoreDaConBound dcb+ = case dcb of+        S.DaConBoundName tx+         -> C.NameCon (Text.unpack tx)++        S.DaConBoundLit pl+         -> toCorePrimLit pl+++

@@ -0,0 +1,41 @@++module DDC.Source.Tetra.Convert.Witness+        ( toCoreW+        , toCoreWC)+where+import DDC.Source.Tetra.Convert.Type+import DDC.Source.Tetra.Convert.Base++import qualified DDC.Source.Tetra.Exp                   as S++import qualified DDC.Core.Tetra.Prim                    as C+import qualified DDC.Core.Exp.Annot                     as C++++toCoreW :: SP -> S.Witness -> ConvertM a (C.Witness SP C.Name)+toCoreW a ww+ = case ww of+        S.WAnnot a' w   +         -> toCoreW a' w++        S.WVar  u+         -> C.WVar  <$> pure a <*> toCoreU  u++        S.WCon  wc+         -> C.WCon  <$> pure a <*> toCoreWC wc++        S.WApp  w1 w2+         -> C.WApp  <$> pure a <*> toCoreW a w1 <*> toCoreW a w2++        S.WType t+         -> C.WType <$> pure a <*> toCoreT UniverseSpec t+++toCoreWC :: S.WiCon -> ConvertM a (C.WiCon C.Name)+toCoreWC wc+ = case wc of+        S.WiConBound u t+         -> C.WiConBound <$> toCoreU u +                         <*> toCoreT UniverseSpec t+

@@ -1,72 +1,82 @@+{-# LANGUAGE TypeFamilies, UndecidableInstances #-}  -- | Source Tetra data type definitions. module DDC.Source.Tetra.DataDef         ( -- * Data Type Definition.           DataDef  (..)-        , typeEnvOfDataDef+        , envOfDataDef                      -- * Data Constructor Definition.         , DataCtor (..)         , typeOfDataCtor) where-import DDC.Type.Compounds-import DDC.Type.Exp-import DDC.Type.Env             (TypeEnv)-import qualified DDC.Type.Env   as Env+import DDC.Source.Tetra.Exp.Generic+import DDC.Source.Tetra.Exp.Source+import DDC.Source.Tetra.Env             (Env)+import qualified DDC.Source.Tetra.Env   as Env import Control.DeepSeq   -- DataDef -------------------------------------------------------------------- -- | Data type definitions.-data DataDef n+data DataDef l         = DataDef         { -- | Data type name.-          dataDefTypeName       :: !n+          dataDefTypeName       :: !(GTBindCon l) -          -- | Type parameters.-        , dataDefParams         :: [Bind n]+          -- | Type parameters and their kinds.+        , dataDefParams         :: [(GTBindVar l, GType l)]            -- | Parameters and return type of each constructor.-        , dataDefCtors          :: [DataCtor n] }-        deriving Show+        , dataDefCtors          :: [DataCtor l] } +deriving instance (ShowLanguage l, Show (DataCtor l))+ => Show (DataDef l)  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 - = Env.fromList -        [BName  (dataCtorName ctor) -                (typeOfDataCtor def ctor)-                | ctor  <- dataDefCtors def ]-                +envOfDataDef +        :: DataDef Source -> Env +envOfDataDef def +        =  Env.unions+        $ [Env.singletonDaCon (dataCtorName ctor) (typeOfDataCtor def ctor)+                | ctor  <- dataDefCtors def]+              + -- DataCtor ------------------------------------------------------------------- -- | A data type constructor definition.-data DataCtor n+data DataCtor l         = DataCtor         { -- | Name of the data constructor.-          dataCtorName          :: !n+          dataCtorName          :: !(GXBindCon l)            -- | Types of each of the fields of the constructor.-        , dataCtorFieldTypes    :: ![Type n]+        , dataCtorFieldTypes    :: ![GType l]            -- | Result type of the constructor.-        , dataCtorResultType    :: !(Type n) }-        deriving Show+        , dataCtorResultType    :: !(GType l) } +deriving instance (ShowLanguage l) + => Show (DataCtor l) ++ instance NFData (DataCtor n) where  rnf !_ = ()   -- | Get the type of a data constructor.-typeOfDataCtor :: DataDef n -> DataCtor n -> Type n+typeOfDataCtor :: DataDef l -> DataCtor l -> GType l typeOfDataCtor def ctor-        = foldr TForall-                (foldr tFun (dataCtorResultType ctor)+        = foldr (\(b, k) t -> TApp (TCon (TyConForall k)) (TAbs b k t))+                (foldr TFun (dataCtorResultType ctor)                             (dataCtorFieldTypes ctor))                 (dataDefParams def)++++

@@ -1,86 +1,326 @@  -- | Source Tetra primitive type and kind environments. module DDC.Source.Tetra.Env-        ( -- * Primitive kind environment.-          primKindEnv-        , kindOfPrimName+        ( Env           (..) -          -- * Primitive type environment.-        , primTypeEnv -        , typeOfPrimName-        , typeOfPrimVal-        , typeOfPrimLit+        , Presence      (..)+        , takePresent -        , dataDefBool)+        , empty+        , union, unions++          -- ** Type Variables+        , singletonTyVar, singletonTyVar'+        , extendTyVar+        , extendTyVar',   extendsTyVar'+        , lookupTyVar+        , tyStackDepth++          -- ** Data Constructors+        , singletonDaCon+        , extendDaCon+        , lookupDaCon++          -- ** Term Variables+        , singletonDaVar+        , singletonDaVar'+        , extendDaVar,   extendsDaVar+        , extendDaVar'+        , extendDaVarMT, extendsDaVarMT+        , lookupDaVar+        , daStackDepth++          -- * Primitive Kinds and Types.+        , kindOfPrimType+        , typeOfPrimVal+        , typeOfPrimLit) 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+import DDC.Source.Tetra.Exp.Source+import Data.Map                         (Map)+import Data.Sequence                    (Seq)+import Data.Text                        (Text)+import qualified Data.List              as List+import qualified Data.Map.Strict        as Map+import qualified Data.Sequence          as Seq  --- Kinds ------------------------------------------------------------------------- | Kind environment containing kinds of primitive data types.-primKindEnv :: Env Name-primKindEnv = Env.setPrimFun kindOfPrimName Env.empty+---------------------------------------------------------------------------------------------------+data Env+        = Env+        { -- | Map names of type constructors to their kinds.+          envTyCon      :: Map Text Type +          -- | Map names of variables to their kinds.+        , envTyVar      :: Map Text (Maybe Type) --- | Take the kind of a primitive name.------   Returns `Nothing` if the name isn't primitive. ----kindOfPrimName :: Name -> Maybe (Kind Name)-kindOfPrimName nn- = case nn of-        NameTyCon tc            -> Just $ kindPrimTyCon tc-        _                       -> Nothing+          -- | Stack of kinds of deBruijn indexed type variables.+        , envTyStack    :: Seq (Maybe Type)+          +          -- | Map names of data constructors to their types.+        , envDaCon      :: Map Text Type  +          -- | Map names of term variables to their types.+        , envDaVar      :: Map Text (Maybe Type) --- Types ------------------------------------------------------------------------- | Type environment containing types of primitive operators.-primTypeEnv :: Env Name-primTypeEnv = Env.setPrimFun typeOfPrimName Env.empty+          -- | Stack of types of deBruijn indexed term variables.+        , envDaStack    :: Seq (Maybe Type) }  --- | Take the type of a name,---   or `Nothing` if this is not a value name.-typeOfPrimName :: Name -> Maybe (Type Name)-typeOfPrimName nn- = case nn of-        NameVal n       -> Just $ typeOfPrimVal n-        _               -> Nothing+-- | Presence of a variable in the environment.+data Presence a+        -- | Variable is not present in environment.+        = Absent +        -- | Variable is present but we don't have a type for it.+        | Unknown +        -- | Variable is present in the environment with this information.+        | Present  a+        deriving Show+++-- | Yield `Just` for a `Present` and `Nothing` for the others.+takePresent :: Presence a -> Maybe a+takePresent pp+ = case pp of+        Absent          -> Nothing+        Unknown         -> Nothing+        Present x       -> Just x+++-- | An empty environment.+empty :: Env+empty +        = Env+        { envTyCon      = Map.empty+        , envTyVar      = Map.empty+        , envTyStack    = Seq.empty+        , envDaCon      = Map.empty+        , envDaVar      = Map.empty+        , envDaStack    = Seq.empty }+++-- | Take the right biased union of two environments.+union :: Env -> Env -> Env+union env1 env2+        = Env+        { envTyCon      = Map.union (envTyCon env1) (envTyCon env2)+        , envTyVar      = Map.union (envTyVar env1) (envTyVar env2)+        , envTyStack    = envTyStack env1 Seq.>< envTyStack env2++        , envDaCon      = Map.union (envDaCon env1) (envDaCon env2)+        , envDaVar      = Map.union (envDaVar env1) (envDaVar env2) +        , envDaStack    = envDaStack env1 Seq.>< envDaStack env2 }+++-- | Take the right biased union of a list of type environments.+unions :: [Env] -> Env+unions envs+        = List.foldl' union empty envs+++---------------------------------------------------------------------------------------------------+-- | Extend the environment with the kind for a type variable.+extendTyVar :: Bind -> Type -> Env -> Env+extendTyVar b k env+ = case b of+        BNone   -> env+        BAnon   -> env { envTyStack = (envTyStack env) Seq.|> (Just k) }+        BName n -> env { envTyVar   = Map.insert n (Just k) (envTyVar env) }+++-- | Extend the environment with a type variable where we don't know its kind.+extendTyVar' :: Bind -> Env -> Env+extendTyVar' b env+ = case b of+        BNone   -> env+        BAnon   -> env { envTyStack = (envTyStack env) Seq.|> Nothing }+        BName n -> env { envTyVar   = Map.insert n Nothing (envTyVar env) }+++-- | Extend the environment with some type variables where we don't know their kinds.+extendsTyVar' :: [Bind] -> Env -> Env+extendsTyVar' bs env+ = List.foldl' (flip extendTyVar') env bs+++-- | Yield an environment containing a single type variable.+singletonTyVar' :: Bind -> Env+singletonTyVar' b + = extendTyVar' b empty++-- | Yield an environment containing the kind for a single type variable.+singletonTyVar :: Bind -> Type -> Env+singletonTyVar b t+ = extendTyVar b t empty++++-- | Lookup the kind of the given type variable.+lookupTyVar :: Env -> Bound -> Presence Type+lookupTyVar env u+ = case u of+        UName tx+         -> case Map.lookup tx (envTyVar env) of+                Nothing         -> Absent+                Just Nothing    -> Unknown+                Just (Just t)   -> Present t++        UIx i+         |  i >= Seq.length (envTyStack env)  +         -> Absent++         | otherwise+         -> case Seq.index (envTyStack env) i of+                Nothing -> Unknown+                Just t  -> Present t++        UHole+         -> Unknown+        ++-- | Get the depth of the type stack.+tyStackDepth :: Env -> Int+tyStackDepth env = Seq.length (envTyStack env)+++---------------------------------------------------------------------------------------------------+-- | Extend the environment with the type of a data constructor.+extendDaCon :: DaConBind -> Type -> Env -> Env+extendDaCon (DaConBindName tx) t env+ = env { envDaCon = Map.insert tx t (envDaCon env) }+++-- | Yield an environment containing the type of a single data constructor.+singletonDaCon :: DaConBind -> Type -> Env+singletonDaCon dc t + = extendDaCon dc t empty+++-- | Lookup the type of a data constructor.+lookupDaCon :: DaConBound -> Env -> Maybe Type+lookupDaCon dc env+ = case dc of+        DaConBoundName tx       -> Map.lookup tx (envDaCon env)+        DaConBoundLit  lit      -> Just (typeOfPrimLit lit)+++---------------------------------------------------------------------------------------------------+-- | Extend the environment with the type of a term variable.+extendDaVar :: Bind -> Type -> Env -> Env+extendDaVar b t env+ = case b of+        BNone   -> env+        BAnon   -> env { envDaStack = (envDaStack env) Seq.|> (Just t) }+        BName n -> env { envDaVar   = Map.insert n (Just t) (envDaVar env) }+++-- | Extend the environment with the types of some term variables.+extendsDaVar :: [(Bind, Type)] -> Env -> Env+extendsDaVar bxs env+ = List.foldl' (\env' (b, t) -> extendDaVar b t env') env bxs+++-- | Extend the environment with a term variable where we don't know it's type.+extendDaVar' :: Bind -> Env -> Env+extendDaVar' b env+ = case b of+        BNone   -> env+        BAnon   -> env { envDaStack = (envDaStack env) Seq.|> Nothing }+        BName n -> env { envDaVar   = Map.insert n Nothing (envDaVar env) }+++-- | Like `extendDaVar` but take a `BindVarMT`+extendDaVarMT :: BindVarMT -> Env -> Env+extendDaVarMT xb env+ = case xb of+        XBindVarMT b Nothing    -> extendDaVar' b env+        XBindVarMT b (Just t)   -> extendDaVar  b t env+++-- | Like `extendDaVarMT` but take a list of `BindVarMT`+extendsDaVarMT :: [BindVarMT] -> Env -> Env+extendsDaVarMT bs env+ = List.foldl' (flip extendDaVarMT) env bs+++-- | Yield an environment containing the type for a single term variable.+singletonDaVar :: Bind -> Type -> Env+singletonDaVar b t+ = extendDaVar b t empty+++-- | Yield an environment containing a single term variable where we don't know its type.+singletonDaVar' :: Bind -> Env+singletonDaVar' b + = extendDaVar' b empty+++-- | Lookup the kind of the given type variable.+lookupDaVar :: Env -> Bound -> Presence Type+lookupDaVar env u+ = case u of+        UName tx+         -> case Map.lookup tx (envDaVar env) of+                Nothing         -> Absent+                Just Nothing    -> Unknown+                Just (Just t)   -> Present t++        UIx i+         |  i >= Seq.length (envDaStack env)  +         -> Absent++         |  otherwise    +         -> case Seq.index (envDaStack env) i of+                Nothing -> Unknown+                Just t  -> Present t++        UHole+         -> Unknown+        ++-- | Get the depth of the type stack.+daStackDepth :: Env -> Int+daStackDepth env = Seq.length (envDaStack env)+++---------------------------------------------------------------------------------------------------+-- | Take the kind of a primitive type.+kindOfPrimType :: PrimType -> Maybe Type+kindOfPrimType tt+ = case tt of+        PrimTypeSoCon _         -> Nothing+        PrimTypeKiCon _         -> Nothing+        PrimTypeTwCon _         -> Nothing+        PrimTypeTcCon _         -> Nothing+        PrimTypeTyCon tc        -> Just (kindPrimTyCon tc)+        PrimTypeTyConTetra tc   -> Just (kindPrimTyConTetra tc)++ -- | Take the type of a primitive name.-typeOfPrimVal  :: PrimVal -> Type Name+typeOfPrimVal  :: PrimVal -> Type typeOfPrimVal dc  = case dc of-        PrimValLit    l         -> typeOfPrimLit l-        PrimValArith  p         -> typePrimArith p-        PrimValError  p         -> typeOpError   p-        PrimValVector p         -> typeOpVector  p-        PrimValFun    p         -> typeOpFun     p+        PrimValLit      l       -> typeOfPrimLit l+        PrimValArith    p       -> typePrimArith Source p+        PrimValCast     p       -> typePrimCast  Source p+        PrimValError    p       -> typeOpError   Source p+        PrimValVector   p       -> typeOpVector  Source p+        PrimValFun      p       -> typeOpFun     Source p   -- | Take the type of a primitive literal.-typeOfPrimLit   :: PrimLit -> Type Name+typeOfPrimLit   :: PrimLit -> Type typeOfPrimLit pl  = case pl of-        PrimLitBool     _       -> tBool-        PrimLitNat      _       -> tNat-        PrimLitInt      _       -> tInt-        PrimLitSize     _       -> tSize-        PrimLitFloat    _ bits  -> tFloat bits-        PrimLitWord     _ bits  -> tWord  bits-        PrimLitTextLit  _       -> tTextLit-+        PrimLitBool     _       -> TBool+        PrimLitNat      _       -> TNat+        PrimLitInt      _       -> TInt+        PrimLitSize     _       -> TSize+        PrimLitFloat    _ bits  -> TFloat bits+        PrimLitWord     _ bits  -> TWord  bits+        PrimLitChar     _       -> TWord  32+        PrimLitTextLit  _       -> TTextLit --- | Data type definition for `Bool`.-dataDefBool :: DataDef Name-dataDefBool- = makeDataDefAlg (NameTyCon PrimTyConBool) -        [] -        (Just   [ (NameLitBool True,  []) -                , (NameLitBool False, []) ]) 

@@ -1,31 +1,246 @@ --- | Definition of Source Tetra Expressions.+-- | Definition of Source Tetra Abstract Syntax,+--   and utilities for working with it. module DDC.Source.Tetra.Exp-        ( module DDC.Type.Exp+        ( -- * Binding+          Name+        , Bind          (..)+        , Bound         (..)+        , takeBoundOfBind -        -- * Expressions-        , GName-        , GAnnot-        , GBind-        , GBound-        , GPrim-        , GExp          (..)-        , GLets         (..)-        , GAlt          (..)-        , GPat          (..)-        , GClause       (..)-        , GGuardedExp   (..)-        , GGuard        (..)-        , GCast         (..)-        , DaCon         (..)+          -------------------------------------------------+          -- * Types -        -- * Witnesses-        , GWitness      (..)-        , GWiCon        (..)+          -----------------------------+          -- ** Syntax+          -- *** Expressions+        , Type,         GType  (..) +          -- *** TyCons+        , TyCon,        GTyCon (..)+        , TyConBind     (..)+        , TyConBound    (..)++          -----------------------------+          -- ** Type Generics+        , Source        (..)+        , GTAnnot+        , GTBindVar,    GTBoundVar+        , GTBindCon,    GTBoundCon+        , GTPrim++          -----------------------------+          -- ** Type Constructors+        , SoCon         (..)+        , KiCon         (..)+        , TwCon         (..)+        , TcCon         (..)++          -----------------------------+          -- ** Type Primitives +        , PrimType       (..)+        , PrimTyCon      (..)+        , PrimTyConTetra (..)++          -----------------------------+          -- ** Pattern Synonyms+        , pattern TApp2, pattern TApp3+        , pattern TApp4, pattern TApp5++        , pattern TVoid, pattern TUnit+        , pattern TFun+        , pattern TBot,  pattern TUnion+        , pattern TPrim++        , pattern KData, pattern KRegion, pattern KEffect+        , pattern TImpl+        , pattern TSusp+        , pattern TRead, pattern TWrite,  pattern TAlloc++        , pattern TBool+        , pattern TNat,  pattern TInt+        , pattern TSize, pattern TWord+        , pattern TFloat+        , pattern TTextLit++          -----------------------------+          -- ** Predicates+        , isAtomT++          -----------------------------+          -- ** Compounds+        , -- *** Destructors+          takeTCon+        , takeTVar+        , takeTAbs+        , takeTApp++          -- *** Type Applications+        , makeTApps,    takeTApps++          -- *** Function Types+        , makeTFun,     makeTFuns,      makeTFuns',     (~>)+        , takeTFun,     takeTFuns,      takeTFuns'++          -- *** Forall Types+        , makeTForall,  makeTForalls +        , takeTForall++          -- *** Exists Types+        , makeTExists,  takeTExists++          -- *** Union types+        , takeTUnion+        , makeTUnions,  takeTUnions+        , splitTUnionsOfKind+        , makeTBot++          -------------------------------------------------+          -- * Terms+          -- ** Syntax+        , Annot,        GXAnnot+        , BindVar,      GXBindVar+        , BindVarMT,    GXBindVarMT (..)+        , BoundVar,     GXBoundVar+        , BindCon,      GXBindCon+        , BoundCon,     GXBoundCon+        , Prim,         GXPrim++          -- *** Expressions+        , Exp,          GExp        (..)++          -- *** Let-binding+        , Lets,         GLets       (..)++          -- *** Clauses+        , Clause,       GClause     (..)++          -- *** Parameters+        , Param,        GParam      (..)++          -- *** Patterns+        , Pat,          GPat        (..)++          -- *** Guards+        , Guard,        GGuard      (..)++          -- *** Guarded Expressions+        , GuardedExp,   GGuardedExp (..)++          -- *** Case Alternatives+        , AltCase,      GAltCase    (..)+        , AltMatch,     GAltMatch   (..)++          -- *** Casts+        , Cast,         GCast       (..)++          -- *** Witnesses+        , Witness,      GWitness    (..)++          -- *** Witness Constructors+        , WiCon,        GWiCon      (..)++          -- *** Data Constructors+        , DaCon (..)+        , DaConBind     (..)+        , DaConBound    (..)++          -----------------------------+          -- ** Term Primitives+        , PrimVal       (..)+        , PrimArith     (..)+        , OpVector      (..)+        , OpFun         (..)+        , OpError       (..)+        , PrimLit       (..)++          -----------------------------+          -- ** Pattern Synonyms+        , pattern PTrue+        , pattern PFalse++          -----------------------------+          -- ** Predicates+          -- *** Atoms+        , isXVar,       isXCon+        , isAtomX,      isAtomW++          -- *** Lambdas+        , isXLAM, isXLam+        , isLambdaX++          -- *** Applications+        , isXApp++          -- *** Let bindings+        , isXLet++          -- *** Types and Witnesses+        , isXType+        , isXWitness++          -- *** Patterns+        , isPDefault++          -----------------------------+          -- ** Compounds+        , takeAnnotOfExp++          -- *** Binds+        , bindOfBindMT+        , takeTypeOfBindMT++          -- *** Lambdas+        , makeXLAMs+        , makeXLams+        , makeXLamFlags+        , takeXLAMs+        , takeXLams+        , takeXLamFlags++          -- *** Applications+        , makeXApps+        , makeXAppsWithAnnots+        , takeXApps+        , takeXApps1+        , takeXAppsAsList+        , takeXAppsWithAnnots+        , takeXConApps+        , takeXPrimApps++          -- *** Clauses+        , bindOfClause++          -- *** Casts+        , pattern XRun+        , pattern XBox++          -- *** Data Constructors+        , dcUnit+        , takeNameOfDaCon+        , takeTypeOfDaCon++          -- *** Patterns+        , bindsOfPat++          -- *** Witnesses+        , wApp+        , wApps+        , takeXWitness+        , takeWAppsAsList+        , takePrimWiConApps++        -------------------------------------------------         -- * Dictionaries         , ShowLanguage+        , PrettyLanguage         , NFDataLanguage) where-import DDC.Type.Exp-import DDC.Source.Tetra.Exp.Generic+import DDC.Source.Tetra.Exp.Bind+import DDC.Source.Tetra.Exp.Source+import DDC.Source.Tetra.Exp.Predicates+import DDC.Source.Tetra.Exp.Compounds+import DDC.Source.Tetra.Exp.NFData+import DDC.Source.Tetra.Pretty+import DDC.Type.Exp.Generic.Compounds+

@@ -1,54 +0,0 @@-{-# 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)

@@ -0,0 +1,71 @@++module DDC.Source.Tetra.Exp.Bind+        ( Name+        , Bind          (..)+        , Bound         (..)+        , takeBoundOfBind++        , DaConBind     (..)+        , DaConBound    (..)+        , TyConBind     (..)+        , TyConBound    (..))+where+import DDC.Source.Tetra.Prim.Base+import Data.Text                (Text)++type Name = Text++-- | Binding occurrence of a variable.+data Bind+        = BNone+        | BAnon+        | BName !Text+        deriving (Eq, Ord, Show)+++-- | Bound occurrence of a variable.+data Bound +        -- A named variable.+        = UName !Text++        -- A deBruijn idex.+        | UIx   !Int++        -- A hole that we want the type checker to fill in.+        | UHole+        deriving (Eq, Ord, Show)+++-- | Take the corresponding `Bound` of a `Bind`, if there is one.+takeBoundOfBind :: Bind -> Maybe Bound+takeBoundOfBind bb+ = case bb of+        BNone    -> Nothing+        BAnon    -> Just $ UIx 0+        BName tx -> Just $ UName tx+++-- | Binding occurrence of a data constructor.+data DaConBind+        = DaConBindName  Text+        deriving (Eq, Ord, Show)+++-- | Bound occurrences of a data constructor.+data DaConBound+        = DaConBoundName Text+        | DaConBoundLit  PrimLit+        deriving (Eq, Ord, Show)+++-- | Binding occurrence of a type constructor.+data TyConBind+        = TyConBindName  Text+        deriving (Eq, Ord, Show)+++-- | Bound occurrence of a type constructor.+data TyConBound+        = TyConBoundName Text+        deriving (Eq, Ord, Show)+

@@ -0,0 +1,300 @@+{-# LANGUAGE TypeFamilies #-}++-- | Utilities for constructing and destructing Source Tetra expressions.+module DDC.Source.Tetra.Exp.Compounds+        ( takeAnnotOfExp++          -- * Binds+        , bindOfBindMT+        , takeTypeOfBindMT++          -- * Types+          -- ** Type Applications+        , T.makeTApps,   T.takeTApps++          -- ** Sum Types+        , makeTBot++          -- ** Function Types+        , T.makeTFun,    T.makeTFuns,   T.makeTFuns',   (T.~>)+        , T.takeTFun,    T.takeTFuns,   T.takeTFuns'++          -- ** Forall Types+        , T.makeTForall, T.makeTForalls+        , T.takeTForall++          -- ** Exists Types+        , T.makeTExists, T.takeTExists++          -- ** Union types+        , T.takeTUnion+        , T.makeTUnions, T.takeTUnions+        , T.splitTUnionsOfKind++          -- * Terms+          -- ** Lambdas+        , makeXLAMs+        , makeXLams+        , makeXLamFlags+        , takeXLAMs+        , takeXLams+        , takeXLamFlags++          -- ** Applications+        , makeXApps+        , makeXAppsWithAnnots+        , takeXApps+        , takeXApps1+        , takeXAppsAsList+        , takeXAppsWithAnnots+        , takeXConApps+        , takeXPrimApps++          -- ** Clauses+        , bindOfClause++          -- ** Casts+        , pattern XRun+        , pattern XBox++          -- ** Data Constructors+        , dcUnit+        , takeNameOfDaCon+        , takeTypeOfDaCon++          -- ** Patterns+        , bindsOfPat++          -- * Witnesses+        , wApp+        , wApps+        , takeXWitness+        , takeWAppsAsList+        , takePrimWiConApps)+where+import DDC.Source.Tetra.Exp.Generic+import Data.Maybe+import qualified DDC.Type.Exp.Generic.Compounds as T++import DDC.Core.Exp.Annot+        ( dcUnit+        , takeNameOfDaCon+        , takeTypeOfDaCon++        , bindsOfPat++        , wApp+        , wApps+        , takeXWitness+        , takeWAppsAsList+        , takePrimWiConApps)+        ++-- Binds ----------------------------------------------------------------------+-- | Take the `GBind` of a `GBindMT`+bindOfBindMT :: GXBindVarMT l -> GXBindVar l+bindOfBindMT (XBindVarMT g _mt) = g+++-- | Take the type of a `GBindMT`.+takeTypeOfBindMT :: GXBindVarMT l -> Maybe (GType l)+takeTypeOfBindMT (XBindVarMT _g mt) = mt+++-- Types ----------------------------------------------------------------------+-- | Make an empty union type of the given kind.+makeTBot  :: GType l -> GType l+makeTBot k = TCon (TyConUnion k)++++-- Annotations ----------------------------------------------------------------+-- | Take the outermost annotation from an expression,+--   or Nothing if this is an `XType` or `XWitness` without an annotation.+takeAnnotOfExp :: GExp l -> Maybe (GXAnnot l)+takeAnnotOfExp xx+ = case xx of+        XAnnot a _              -> Just a+        XVar{}                  -> Nothing+        XPrim{}                 -> Nothing+        XCon{}                  -> Nothing+        XLAM    _  x            -> takeAnnotOfExp x+        XLam    _  x            -> takeAnnotOfExp x+        XApp    x1 x2           -> firstJust $ map takeAnnotOfExp [x1, x2]+        XLet    _  x            -> takeAnnotOfExp x+        XCase   x  _            -> takeAnnotOfExp x+        XCast   _  x            -> takeAnnotOfExp x+        XType{}                 -> Nothing+        XWitness{}              -> Nothing+        XDefix    a _           -> Just a+        XInfixOp  a _           -> Just a+        XInfixVar a _           -> Just a+        XMatch    a _ _         -> Just a+        XWhere    a _ _         -> Just a+        XLamPat   a _ _ _       -> Just a+        XLamCase  a _           -> Just a+++firstJust = listToMaybe . catMaybes++-- Lambdas ---------------------------------------------------------------------+-- | Make some nested type lambdas.+makeXLAMs :: [GXBindVarMT l] -> GExp l -> GExp l+makeXLAMs bs x = foldr XLAM x bs+++-- | Make some nested value or witness lambdas.+makeXLams :: [GXBindVarMT l] -> GExp l -> GExp l+makeXLams bs x = foldr XLam x bs+++-- | Split type lambdas from the front of an expression,+--   or `Nothing` if there aren't any.+takeXLAMs :: GExp l -> Maybe ([GXBindVarMT l], GExp l)+takeXLAMs xx+ = let  go bs (XAnnot _ x) = go bs x+        go bs (XLAM b x)   = go (b:bs) x+        go bs x            = (reverse bs, x)++   in   case go [] xx of+         ([], _)        -> Nothing+         (bs, body)     -> Just (bs, body)+++-- | Split nested value or witness lambdas from the front of an expression,+--   or `Nothing` if there aren't any.+takeXLams :: GExp l -> Maybe ([GXBindVarMT l], GExp l)+takeXLams xx+ = let  go bs (XAnnot _ x) = go bs x+        go bs (XLam b x)   = go (b:bs) x+        go bs x            = (reverse bs, x)+   in   case go [] xx of+         ([], _)        -> Nothing+         (bs, body)     -> Just (bs, body)+++-- | Make some nested lambda abstractions,+--   using a flag to indicate whether the lambda is a+--   level-1 (True), or level-0 (False) binder.+makeXLamFlags :: [(Bool, GXBindVarMT l)] -> GExp l -> GExp l+makeXLamFlags fbs x+ = foldr (\(f, b) x'+           -> if f then XLAM b x'+                   else XLam b x')+                x fbs+++-- | Split nested lambdas from the front of an expression, +--   with a flag indicating whether the lambda was a level-1 (True), +--   or level-0 (False) binder.+takeXLamFlags +        :: GExp l +        -> Maybe ([(Bool, GXBindVarMT l)], GExp l)++takeXLamFlags xx+ = let  go bs (XAnnot _ x)  = go bs x+        go bs (XLAM b x)    = go ((True,  b):bs) x+        go bs (XLam b x)    = go ((False, b):bs) x+        go bs x             = (reverse bs, x)++   in   case go [] xx of+         ([], _)        -> Nothing+         (bs, body)     -> Just (bs, body)+++-- Applications ---------------------------------------------------------------+-- | Build sequence of value applications.+makeXApps   :: GExp l -> [GExp l] -> GExp l+makeXApps t1 ts     = foldl XApp t1 ts+++-- | Build sequence of applications.+--   Similar to `xApps` but also takes list of annotations for +--   the `XApp` constructors.+makeXAppsWithAnnots :: GExp l -> [(GExp l, Maybe (GXAnnot l))] -> GExp l+makeXAppsWithAnnots f xas+ = case xas of+        []                  -> f+        (arg, Nothing) : as -> makeXAppsWithAnnots (XApp f arg) as+        (arg, Just a)  : as -> makeXAppsWithAnnots (XAnnot a $ XApp f arg) as+++-- | Flatten an application into the function part and its arguments.+--+--   Returns `Nothing` if there is no outer application.+takeXApps :: GExp l -> Maybe (GExp l, [GExp l])+takeXApps xx+ = case takeXAppsAsList xx of+        (x1 : xsArgs)   -> Just (x1, xsArgs)+        _               -> Nothing+++-- | Flatten an application into the function part and its arguments.+--+--   This is like `takeXApps` above, except we know there is at least one argument.+takeXApps1 :: GExp l -> GExp l -> (GExp l, [GExp l])+takeXApps1 x1 x2+ = case takeXApps x1 of+        Nothing          -> (x1,  [x2])+        Just (x11, x12s) -> (x11, x12s ++ [x2])+++-- | Flatten an application into the function parts and arguments, if any.+takeXAppsAsList  :: GExp l -> [GExp l]+takeXAppsAsList xx+ = case xx of+        XAnnot _ x      -> takeXAppsAsList x+        XApp x1 x2      -> takeXAppsAsList x1 ++ [x2]+        _               -> [xx]+++-- | Destruct sequence of applications.+--   Similar to `takeXAppsAsList` but also keeps annotations for later.+takeXAppsWithAnnots :: GExp l -> (GExp l, [(GExp l, Maybe (GXAnnot l))])+takeXAppsWithAnnots xx+ = case xx of+        XAnnot a (XApp f arg)+         -> let (f', args') = takeXAppsWithAnnots f+            in  (f', args' ++ [(arg, Just a)])++        XApp f arg+         -> let (f', args') = takeXAppsWithAnnots f+            in  (f', args' ++ [(arg, Nothing)])++        _ -> (xx, [])+++-- | Flatten an application of a primop into the variable+--   and its arguments.+--   +--   Returns `Nothing` if the expression isn't a primop application.+takeXPrimApps :: GExp l -> Maybe (GXPrim l, [GExp l])+takeXPrimApps xx+ = case takeXAppsAsList xx of+        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 :: GExp l -> Maybe (DaCon (GXBoundCon l) (GType l), [GExp l])+takeXConApps xx+ = case takeXAppsAsList xx of+        XCon dc : xs    -> Just (dc, xs)+        _               -> Nothing+++-- Clauses --------------------------------------------------------------------+-- | Take the binding variable of a clause.+bindOfClause :: GClause l -> GXBindVar l+bindOfClause cc+ = case cc of+        SSig _ b _                      -> b+        SLet _ (XBindVarMT b _) _ _     -> b+++-- Casts ----------------------------------------------------------------------+pattern XBox x = XCast CastBox x+pattern XRun x = XCast CastRun x+

@@ -4,52 +4,93 @@ module DDC.Source.Tetra.Exp.Generic         ( -- * Classes           HasAnonBind   (..)+        , Anon          (..) -          -- * Expressions-        , GName-        , GAnnot-        , GBind-        , GBound-        , GPrim+          -- * Types+          -- ** Type Functions+        , GTAnnot+        , GTBindVar,    GTBoundVar+        , GTBindCon,    GTBoundCon+        , GTPrim++          -- ** Syntax+        , GType         (..)+        , GTyCon        (..)++        , pattern TApp2, pattern TApp3+        , pattern TApp4, pattern TApp5++        , pattern TVoid, pattern TUnit+        , pattern TFun+        , pattern TBot,  pattern TUnion+        , pattern TPrim++          -- ** Dictionaries+        , ShowGType++          -- * Terms+          -- ** Type Functions+        , GXAnnot+        , GXBindVar, GXBoundVar+        , GXBindCon, GXBoundCon+        , GXPrim++          -- ** Syntax+        , GXBindVarMT   (..)         , GExp          (..)         , GLets         (..)-        , GAlt          (..)         , GPat          (..)         , GClause       (..)-        , GGuardedExp   (..)+        , GParam        (..)         , GGuard        (..)+        , GGuardedExp   (..)+        , GAltMatch     (..)+        , GAltCase      (..)         , GCast         (..)-        , DaCon         (..)--          -- * Witnesses         , GWitness      (..)         , GWiCon        (..)+        , DaCon         (..)            -- * Dictionaries-        , ShowLanguage-        , NFDataLanguage)+        , ShowLanguage) where-import DDC.Type.Exp     -import qualified DDC.Type.Exp           as T-import DDC.Type.Sum                     ()-import Control.DeepSeq-import DDC.Core.Exp-        ( DaCon         (..))+import DDC.Type.Exp.Generic.Binding+import DDC.Type.Exp.Generic.Exp+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+-------------------------------------------------------------------------------+-- Type functions associated with the language AST. +-- | Yield the type of annotations.+type family GXAnnot    l++-- | Yield the type of binding occurrences of variables.+type family GXBindVar  l++-- | Yield the type of bound occurrences of variables.+type family GXBoundVar l++-- | Yield the type of binding occurrences of constructors.+type family GXBindCon  l++-- | Yield the type of bound occurrences of constructors.+type family GXBoundCon l++-- | Yield the type of primitive operator names.+type family GXPrim     l++ class HasAnonBind l where- isAnon :: l -> GBind l -> Bool+ isAnon :: l -> GXBindVar l -> Bool  ----------------------------------------------------------------------------------------------------+-- | A possibly typed binding.+data GXBindVarMT l +        = XBindVarMT (GXBindVar l) (Maybe (GType l))+++------------------------------------------------------------------------------- -- | Well-typed expressions have types of kind `Data`. data GExp l         ---------------------------------------------------@@ -57,57 +98,78 @@         --   These are also in the core language, and after desugaring only         --   these constructs are used.         --+        = XAnnot    !(GXAnnot l) !(GExp   l)+         -- | Value variable   or primitive operation.-        = XVar      !(GAnnot l) !(GBound l)+        | XVar      !(GXBoundVar l)          -- | Primitive values.-        | XPrim     !(GAnnot l) !(GPrim  l)+        | XPrim     !(GXPrim  l)          -- | Data constructor or literal.-        | XCon      !(GAnnot l) !(DaCon (GName l))+        | XCon      !(DaCon (GXBoundCon l) (GType l))          -- | Type abstraction (level-1).-        | XLAM      !(GAnnot l) !(GBind l) !(GExp l)+        | XLAM      !(GXBindVarMT l) !(GExp l)          -- | Value and Witness abstraction (level-0).-        | XLam      !(GAnnot l) !(GBind l) !(GExp l)+        | XLam      !(GXBindVarMT l) !(GExp l)          -- | Application.-        | XApp      !(GAnnot l) !(GExp  l) !(GExp l)+        | XApp      !(GExp  l)   !(GExp l)          -- | A non-recursive let-binding.-        | XLet      !(GAnnot l) !(GLets l) !(GExp l)+        | XLet      !(GLets l)   !(GExp l)          -- | Case branching.-        | XCase     !(GAnnot l) !(GExp  l) ![GAlt l]+        | XCase     !(GExp  l)   ![GAltCase l]          -- | Type cast.-        | XCast     !(GAnnot l) !(GCast l) !(GExp l)+        | XCast     !(GCast l)   !(GExp l)          -- | Type can appear as the argument of an application.-        | XType     !(GAnnot l) !(Type  (GName l))+        | XType     !(GType l)          -- | Witness can appear as the argument of an application.-        | XWitness  !(GAnnot l) !(GWitness l)+        | XWitness  !(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]+        -- | Some expressions and infix operators that need to be resolved+        --   into proper function applications.+        | XDefix    !(GXAnnot 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+        | XInfixOp  !(GXAnnot 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+        | XInfixVar !(GXAnnot l) String +        -- | Match expression with default.+        --   Similar to a case expression, except that if an alternative+        --   fails then we try the next one instead of failing.+        --   If none of the alternatives succeeds then the overall value+        --   is the value of the default expression.+        | XMatch    !(GXAnnot l) ![GAltMatch l] !(GExp l) +        -- | Where expression defines a group of recursive clauses,+        --   and is desugared to a letrec.+        | XWhere    !(GXAnnot l) !(GExp l) ![GClause l]++        -- | Lambda abstraction which matches its argument against+        --   a single pattern.+        | XLamPat   !(GXAnnot l) !(GPat l) !(Maybe (GType l)) !(GExp l)++        -- | Lambda abstraction that matches its argument against+        --   the given alternatives.+        | XLamCase  !(GXAnnot l) ![GAltCase l]++ -- | Possibly recursive bindings. --   Whether these are taken as recursive depends on whether they appear --   in an XLet or XLetrec group.@@ -115,14 +177,14 @@         ---------------------------------------------------         -- Core Language Constructs         -- | Non-recursive expression binding.-        = LLet     !(GBind l) !(GExp l)+        = LLet      !(GXBindVarMT l) !(GExp l)          -- | Recursive binding of lambda abstractions.-        | LRec     ![(GBind l, GExp l)]+        | LRec     ![(GXBindVarMT l,   GExp l)]          -- | Bind a local region variable,         --   and witnesses to its properties.-        | LPrivate ![GBind l] !(Maybe (Type (GName l))) ![GBind l]+        | LPrivate ![GXBindVar l] !(Maybe (GType l)) ![(GXBindVar l, GType l)]          ---------------------------------------------------         -- Sugar Constructs@@ -135,24 +197,38 @@ -- | Binding clause data GClause l         -- | A separate type signature.-        = SSig   !(GAnnot l) !(GBind l) !(Type (GName l))+        = SSig   !(GXAnnot l) !(GXBindVar l)   !(GType l)          -- | A function binding using pattern matching and guards.-        | SLet   !(GAnnot l) !(GBind l) ![GPat l]  ![GGuardedExp l]+        | SLet   !(GXAnnot l) !(GXBindVarMT l) ![GParam l] ![GGuardedExp l]  --- | Case alternatives.-data GAlt l-        = AAlt   !(GPat l) ![GGuardedExp l]+-- | Parameter for a binding.+data GParam l+        -- | Type parameter with optional kind.+        = MType    !(GXBindVar l) (Maybe (GType l)) +        -- | Witness parameter with optional type.+        | MWitness !(GXBindVar l) (Maybe (GType l)) +        -- | Value paatter with optional type.+        | MValue   !(GPat l)      (Maybe (GType l))++ -- | Patterns. data GPat l         -- | The default pattern always succeeds.         = PDefault +        -- | Give a name to the value matched by a pattern.+        | PAt    !(GXBindVar l) !(GPat l)++        -- | The variable pattern always succeeds and binds the value+        --   to the new variable.+        | PVar   !(GXBindVar l) +         -- | Match a data constructor and bind its arguments.-        | PData !(DaCon (GName l)) ![GBind l]+        | PData  !(DaCon (GXBoundCon l) (GType l)) ![GPat l]   -- | An expression with some guards.@@ -163,17 +239,31 @@  -- | Expression guards. data GGuard l-        = GPat  !(GPat l) !(GExp l)-        | GPred !(GExp l)+        = GPat   !(GPat l) !(GExp l)+        | GPred  !(GExp l)         | GDefault  +-- | Case alternative.+--   If the pattern matches then bind the variables then enter+--   the guarded expression.+data GAltCase l+        = AAltCase   !(GPat l) ![GGuardedExp l]+++-- | Match alternative.+--   This is like a case alternative except that the match expression+--   does not give us a head pattern.+data GAltMatch l+        = AAltMatch  !(GGuardedExp l)++ -- | 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))+        = CastWeakenEffect  !(GType l)                  -- | Purify the effect (action) of an expression.         | CastPurify !(GWitness l)@@ -189,17 +279,20 @@  -- | Witnesses. data GWitness l+        -- | Witness annotation+        = WAnnot !(GXAnnot l)  !(GWitness l)+         -- | Witness variable.-        = WVar  !(GAnnot l) !(GBound l)+        | WVar   !(GXBoundVar l)          -- | Witness constructor.-        | WCon  !(GAnnot l) !(GWiCon l)+        | WCon   !(GWiCon l)          -- | Witness application.-        | WApp  !(GAnnot l) !(GWitness l) !(GWitness l)+        | WApp   !(GWitness l) !(GWitness l)          -- | Type can appear as an argument of a witness application.-        | WType !(GAnnot l) !(T.Type (GName l))+        | WType  !(GType l)   -- | Witness constructors.@@ -207,116 +300,29 @@         -- | 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))+        = WiConBound   !(GXBoundVar l) !(GType 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-+          , ShowGType l+          , Show (GXAnnot    l)+          , Show (GXBindVar l), Show (GXBoundVar l)+          , Show (GXBindCon l), Show (GXBoundCon l)+          , Show (GXPrim l)) -instance NFDataLanguage l => NFData (GWiCon l) where- rnf wc-  = case wc of-        WiConBound u t          -> rnf u `seq` rnf t+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 (GParam       l)+deriving instance ShowLanguage l => Show (GAltCase     l)+deriving instance ShowLanguage l => Show (GAltMatch    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)+deriving instance ShowLanguage l => Show (GXBindVarMT  l) 

@@ -0,0 +1,127 @@+{-# LANGUAGE UndecidableInstances #-}+module DDC.Source.Tetra.Exp.NFData where+import DDC.Source.Tetra.Exp.Generic+import qualified DDC.Type.Exp.Generic.NFData    as T+import Control.DeepSeq++---------------------------------------------------------------------------------------------------+type NFDataLanguage l+        = ( NFData l, T.NFDataLanguage l+          , NFData (GXAnnot   l)+          , NFData (GXBindVar l),  NFData (GXBoundVar l)+          , NFData (GXBindCon l),  NFData (GXBoundCon l)+          , NFData (GXPrim    l))++instance NFDataLanguage l => NFData (GExp l) where+ rnf xx+  = case xx of+        XAnnot    a x           -> rnf a `seq` rnf x+        XVar      u             -> rnf u+        XPrim     p             -> rnf p+        XCon      dc            -> rnf dc+        XLAM      b x           -> rnf b   `seq` rnf x+        XLam      b x           -> rnf b   `seq` rnf x+        XApp      x1 x2         -> rnf x1  `seq` rnf x2+        XLet      lts x         -> rnf lts `seq` rnf x+        XCase     x alts        -> rnf x   `seq` rnf alts+        XCast     c x           -> rnf c   `seq` rnf x+        XType     t             -> rnf t+        XWitness  w             -> 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+        XMatch    a as x        -> rnf a   `seq` rnf as `seq` rnf x+        XWhere    a cl x        -> rnf a   `seq` rnf cl `seq` rnf x+        XLamPat   a w mt x      -> rnf a   `seq` rnf w  `seq` rnf mt `seq` rnf x+        XLamCase  a as          -> rnf a   `seq` rnf as+++instance NFDataLanguage l => NFData (GXBindVarMT l) where+ rnf (XBindVarMT b mt)+  = rnf b `seq` rnf mt+++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 (GParam l) where+ rnf pp+  = case pp of+        MType    b mt           -> rnf b `seq` rnf mt+        MWitness b mt           -> rnf b `seq` rnf mt+        MValue   p mt           -> rnf p `seq` rnf mt+++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 (GAltCase l) where+ rnf aa+  = case aa of+        AAltCase w gxs          -> rnf w `seq` rnf gxs+++instance NFDataLanguage l => NFData (GAltMatch l) where+ rnf aa+  = case aa of+        AAltMatch gs            -> rnf gs+++instance NFDataLanguage l => NFData (GPat l) where+ rnf pp+  = case pp of+        PDefault                -> ()+        PAt   b p               -> rnf b  `seq` rnf p+        PVar  b                 -> rnf b+        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+        WAnnot a w              -> rnf a `seq` rnf w+        WVar   u                -> rnf u+        WCon   c                -> rnf c+        WApp   w1 w2            -> rnf w1 `seq` rnf w2+        WType  t                -> rnf t+++instance NFDataLanguage l => NFData (GWiCon l) where+ rnf wc+  = case wc of+        WiConBound u t          -> rnf u `seq` rnf t+

@@ -0,0 +1,139 @@++-- | Simple predicates on Source Tetra things.+module DDC.Source.Tetra.Exp.Predicates+        ( module DDC.Type.Exp.Generic.Predicates++          -- * Atoms+        , isXVar,       isXCon+        , isAtomX,      isAtomW++          -- * Lambdas+        , isXLAM, isXLam+        , isLambdaX++          -- * Applications+        , isXApp++          -- * Let bindings+        , isXLet++          -- * Types and Witnesses+        , isXType+        , isXWitness++          -- * Patterns+        , isPDefault+        , isPVar)+where+import DDC.Source.Tetra.Exp.Generic+import DDC.Type.Exp.Generic.Predicates+++-- Atoms ----------------------------------------------------------------------+-- | Check whether an expression is a variable.+isXVar :: GExp l -> Bool+isXVar xx+ = case xx of+        XVar{}  -> True+        _       -> False+++-- | Check whether an expression is a constructor.+isXCon :: GExp l -> Bool+isXCon xx+ = case xx of+        XCon{}  -> True+        _       -> False+++-- | Check whether an expression is a `XVar` or an `XCon`, +--   or some type or witness atom.+isAtomX :: GExp l -> Bool+isAtomX xx+ = case xx of+        XVar{}          -> True+        XCon{}          -> True+        XType    t      -> isAtomT t+        XWitness w      -> isAtomW w+        _               -> False+++-- | Check whether a witness is a `WVar` or `WCon`.+isAtomW :: GWitness l -> Bool+isAtomW ww+ = case ww of+        WVar{}          -> True+        WCon{}          -> True+        _               -> False+++-- Lambdas --------------------------------------------------------------------+-- | Check whether an expression is a spec abstraction (level-1).+isXLAM :: GExp l -> Bool+isXLAM xx+ = case xx of+        XLAM{}  -> True+        _       -> False+++-- | Check whether an expression is a value or witness abstraction (level-0).+isXLam :: GExp l -> Bool+isXLam xx+ = case xx of+        XLam{}  -> True+        _       -> False+++-- | Check whether an expression is a spec, value, or witness abstraction.+isLambdaX :: GExp l -> Bool+isLambdaX xx+        = isXLAM xx || isXLam xx+++-- Applications ---------------------------------------------------------------+-- | Check whether an expression is an `XApp`.+isXApp :: GExp l -> Bool+isXApp xx+ = case xx of+        XApp{}  -> True+        _       -> False+++-- Let Bindings ---------------------------------------------------------------+-- | Check whether an expression is a `XLet`.+isXLet :: GExp l -> Bool+isXLet xx+ = case xx of+        XLet{}  -> True+        _       -> False+        ++-- Type and Witness -----------------------------------------------------------+-- | Check whether an expression is an `XType`+isXType :: GExp l -> Bool+isXType xx+ = case xx of+        XType{}         -> True+        _               -> False+++-- | Check whether an expression is an `XWitness`+isXWitness :: GExp l -> Bool+isXWitness xx+ = case xx of+        XWitness{}      -> True+        _               -> False+++-- Patterns -------------------------------------------------------------------+-- | Check whether a pattern is a `PDefault`.+isPDefault :: GPat l -> Bool+isPDefault PDefault     = True+isPDefault _            = False+++-- | Check whether a pattern is a `PVar`.+isPVar     :: GPat l -> Bool+isPVar (PVar _)         = True+isPVar _                = False+

@@ -0,0 +1,162 @@+{-# LANGUAGE TypeFamilies #-}+module DDC.Source.Tetra.Exp.Source+        ( -- * Language+          Source        (..)++          -- * Binding+        , Name+        , Bind          (..)+        , Bound         (..)++          -- * Types+          -- ** Syntax+        , GTAnnot+        , GTBindVar,    GTBoundVar+        , GTBindCon,    GTBoundCon+        , GTPrim++        , Type,         GType  (..)+        , TyCon,        GTyCon (..)++        , SoCon         (..)+        , KiCon         (..)+        , TwCon         (..)+        , TcCon         (..)++        , TyConBind     (..)+        , TyConBound    (..)++        , pattern TApp2, pattern TApp3+        , pattern TApp4, pattern TApp5++        , pattern TVoid, pattern TUnit+        , pattern TFun+        , pattern TBot,  pattern TUnion+        , pattern TPrim++          -- ** Primitives +        , PrimType       (..)+        , PrimTyCon      (..)+        , PrimTyConTetra (..)++        , pattern KData, pattern KRegion, pattern KEffect+        , pattern TImpl+        , pattern TSusp+        , pattern TRead, pattern TWrite,  pattern TAlloc++        , pattern TBool+        , pattern TNat,  pattern TInt+        , pattern TSize, pattern TWord+        , pattern TFloat+        , pattern TTextLit++          -- * Terms+          -- ** Syntax+        , Annot,        GXAnnot+        , BindVarMT,    GXBindVarMT (..)+        , BindVar,      GXBindVar+        , BoundVar,     GXBoundVar+        , BindCon,      GXBindCon+        , BoundCon,     GXBoundCon+        , Prim,         GXPrim+        , Exp,          GExp        (..)+        , Lets,         GLets       (..)+        , Clause,       GClause     (..)+        , Param,        GParam      (..)+        , Pat,          GPat        (..)+        , Guard,        GGuard      (..)+        , GuardedExp,   GGuardedExp (..)+        , AltMatch,     GAltMatch   (..)+        , AltCase,      GAltCase    (..)+        , Cast,         GCast       (..)+        , Witness,      GWitness    (..)+        , WiCon,        GWiCon      (..)+        , DaCon (..)++        , DaConBind     (..)+        , DaConBound    (..)++          -- ** Primitives+        , PrimVal       (..)+        , PrimArith     (..)+        , OpVector      (..)+        , OpFun         (..)+        , OpError       (..)+        , PrimLit       (..)++        , pattern PTrue+        , pattern PFalse++          -- ** Dictionaries+        , ShowLanguage)+where+import DDC.Source.Tetra.Exp.Generic+import DDC.Source.Tetra.Exp.Bind+import DDC.Source.Tetra.Prim+import DDC.Type.Exp.TyCon               as T+import DDC.Data.SourcePos+import DDC.Data.Pretty+++-- Language -------------------------------------------------------------------+-- | Type index for Source Tetra Language.+data Source     +        = Source+        deriving Show++instance Pretty Source where+ ppr ss = text (show ss)+++instance HasAnonBind Source where+ isAnon _ BAnon = True+ isAnon _ _     = False+++instance Anon Source where+ withBindings Source n f+  = let bs      = replicate n BAnon+        us      = reverse [UIx i | i <- [0..(n - 1)]]+    in  f bs us+++-- Type AST -------------------------------------------------------------------+type Type       = GType  Source+type TyCon      = GTyCon Source++type instance GTAnnot    Source = SourcePos+type instance GTBindVar  Source = Bind+type instance GTBoundVar Source = Bound+type instance GTBindCon  Source = TyConBind+type instance GTBoundCon Source = TyConBound+type instance GTPrim     Source = PrimType+++-- Term AST -------------------------------------------------------------------+type Annot      = GXAnnot     Source+type BindVar    = GXBindVar   Source+type BindVarMT  = GXBindVarMT Source+type BoundVar   = GXBoundVar  Source+type BindCon    = GXBoundCon  Source+type BoundCon   = GXBoundCon  Source+type Prim       = GXPrim      Source+type Exp        = GExp        Source+type Lets       = GLets       Source+type Clause     = GClause     Source+type Param      = GParam      Source+type Pat        = GPat        Source+type Guard      = GGuard      Source+type GuardedExp = GGuardedExp Source+type AltCase    = GAltCase    Source+type AltMatch   = GAltMatch   Source+type Cast       = GCast       Source+type Witness    = GWitness    Source+type WiCon      = GWiCon      Source++type instance GXAnnot    Source = SourcePos+type instance GXBindVar  Source = Bind+type instance GXBoundVar Source = Bound+type instance GXBindCon  Source = DaConBind+type instance GXBoundCon Source = DaConBound+type instance GXPrim     Source = PrimVal+

@@ -1,13 +1,87 @@  -- | Lexer for Source Tetra tokens. module DDC.Source.Tetra.Lexer-        (lexModuleString)+        ( Name (..)+        , lexModuleString) where import DDC.Source.Tetra.Prim import DDC.Core.Lexer-import DDC.Data.Token+import DDC.Data.Pretty+import Control.DeepSeq+import Data.Char+import Data.Text                (Text)+import qualified Data.Text      as Text  +---------------------------------------------------------------------------------------------------+-- | Union of all names that we detect during lexing.+data Name+        -- | A user defined variable.+        = NameVar        !Text++        -- | A user defined constructor.+        | NameCon        !Text++        -- | Primitive type names.+        | NamePrimType   !PrimType++        -- | Primitive literal values.+        | NamePrimValLit !PrimLit++        -- | Primitive operator values.+        | NamePrimValOp  !PrimVal+        deriving (Eq, Ord, Show)+++---------------------------------------------------------------------------------------------------+instance Pretty Name where+ ppr nn+  = case nn of+        NameVar  v              -> text (Text.unpack v)+        NameCon  c              -> text (Text.unpack c)+        NamePrimType p          -> ppr p+        NamePrimValLit p        -> ppr p+        NamePrimValOp  p        -> ppr p+++instance NFData Name where+ rnf nn+  = case nn of+        NameVar s               -> rnf s+        NameCon s               -> rnf s+        NamePrimType p          -> rnf p+        NamePrimValLit p        -> rnf p+        NamePrimValOp  p        -> rnf p+++-- | Read the name of a variable, constructor or literal.+readName :: String -> Maybe Name+readName str+        -- Primitive names.+        | Just n        <- readPrimType str+        = Just $ NamePrimType   n++        | Just n        <- readPrimLit str+        = Just $ NamePrimValLit n++        | Just n        <- readPrimVal str+        = Just $ NamePrimValOp  n++        -- Constructors.+        | c : _         <- str+        , isUpper c+        = Just $ NameCon (Text.pack str)++        -- Variables.+        | c : _         <- str+        , isVarStart c      +        = Just $ NameVar (Text.pack str)++        | otherwise+        = Nothing+++--------------------------------------------------------------------------------------------------- -- | Lex a string to tokens, using primitive names. -- --   The first argument gives the starting source line number.@@ -17,10 +91,13 @@ --   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 :: String -> Int -> String -> [Located (Token Name)] lexModuleString sourceName lineStart str  = map rn $ lexModuleWithOffside sourceName lineStart str- where rn (Token strTok sp)-        = case renameTok readName strTok of-                Just t' -> Token t' sp-                Nothing -> Token (KErrorJunk "lexical error") sp+ where +        rn (Located sp strTok)+         = case renameToken readName strTok of+                Just t' -> Located sp t'+                Nothing -> Located sp (KErrorJunk "lexical error")++

@@ -21,8 +21,9 @@           -- * Data type definitions         , DataDef       (..)) where-import DDC.Source.Tetra.Exp import DDC.Source.Tetra.DataDef+import DDC.Source.Tetra.Exp.Source+import DDC.Source.Tetra.Exp.NFData import Control.DeepSeq  import DDC.Core.Module          @@ -35,7 +36,7 @@         , ImportValue   (..))          --- Module ---------------------------------------------------------------------+-- Module ----------------------------------------------------------------------------------------- data Module l         = Module         { -- | Name of this module@@ -43,28 +44,29 @@            -- Exports ----------------------------           -- | Names of exported types  (level-1).-        , moduleExportTypes     :: [GName l]+        , moduleExportTypes     :: [GTBoundCon l]            -- | Names of exported values (level-0).-        , moduleExportValues    :: [GName l]+        , moduleExportValues    :: [GXBoundVar l]            -- Imports ----------------------------           -- | Imported modules.         , moduleImportModules   :: [ModuleName]            -- | Kinds of imported foreign types.-        , moduleImportTypes     :: [(GName l, ImportType  (GName l))]+        , moduleImportTypes     :: [(GTBindCon l, ImportType  (GTBindCon l) (GType l))]            -- | Types of imported capabilities.-        , moduleImportCaps      :: [(GName l, ImportCap   (GName l))]+        , moduleImportCaps      :: [(GXBindVar l, ImportCap   (GXBindVar l) (GType l))]            -- | Types of imported foreign values.-        , moduleImportValues    :: [(GName l, ImportValue (GName l))]+        , moduleImportValues    :: [(GXBindVar l, ImportValue (GXBindVar l) (GType l))]            -- Local ------------------------------           -- | Top-level things         , moduleTops            :: [Top l] } + deriving instance ShowLanguage l => Show (Module l)  @@ -86,18 +88,25 @@         = isMainModuleName $ moduleName mm  --- Top Level Thing ------------------------------------------------------------+-- Top Level Thing -------------------------------------------------------------------------------- data Top l         -- | Some top-level, possibly recursive clauses.         = TopClause  -        { topAnnot      :: GAnnot l+        { topAnnot      :: GXAnnot l         , topClause     :: GClause l }          -- | Data type definition.         | TopData -        { topAnnot      :: GAnnot l-        , topDataDef    :: DataDef (GName l) }+        { topAnnot      :: GXAnnot l+        , topDataDef    :: DataDef l } +        -- | Type binding.+        | TopType+        { topAnnot      :: GXAnnot l+        , topTypeBind   :: GTBindCon l+        , topTypeExp    :: GType l }++ deriving instance ShowLanguage l => Show (Top l)  instance NFDataLanguage l => NFData (Top l) where@@ -105,4 +114,5 @@   = case top of         TopClause a c   -> rnf a `seq` rnf c         TopData   a def -> rnf a `seq` rnf def+        TopType   a b t -> rnf a `seq` rnf b `seq` rnf t 

@@ -2,55 +2,42 @@ -- | Parser for the Source Tetra language. module DDC.Source.Tetra.Parser         ( Parser-        , Context       (..)-        , context          -- * Modules         , pModule          -- * Expressions         , pExp-        , pExpApp-        , pExpAtom+        , pExpAppSP          -- * Types         , pType         , pTypeApp-        , pTypeAtom+        , pTypeAtomSP          -- * Witnesses         , pWitness         , pWitnessApp         , pWitnessAtom -        -- * Constructors-        , pCon-        , pLit-         -- * Variables-        , pBinder-        , pIndex-        , pVar-        , pName+        , pBindNameSP+        , pBoundNameSP,         pBoundName+        , pBoundIxSP+        , pBoundNameOpSP+        , pBoundNameOpVarSP +        -- * Constructors+        , pDaConBindName+        , pDaConBoundName,      pDaConBoundNameSP+        , pDaConBoundLit,       pDaConBoundLitSP+        , pPrimValSP+         -- * Raw Tokens-        , pTok-        , pTokAs)+        , pTok) where-import DDC.Source.Tetra.Parser.Exp import DDC.Source.Tetra.Parser.Module+import DDC.Source.Tetra.Parser.Witness+import DDC.Source.Tetra.Parser.Exp+import DDC.Source.Tetra.Parser.Base -import DDC.Core.Parser-        ( Parser-        , Context       (..)-        , pWitness-        , pWitnessApp-        , pWitnessAtom-        , pVar-        , pCon-        , pName-        , pBinder-        , pIndex        -        , pLit-        , pTok, pTokAs)-        

@@ -1,28 +0,0 @@--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

@@ -0,0 +1,154 @@+{-# LANGUAGE ExplicitNamespaces #-}+module DDC.Source.Tetra.Parser.Base+        ( type Parser+        , (<?>), SourcePos(..)++          -- * Generic Token parsers+        , pSym, pKey+        , pTok, pTokSP++          -- * Term Variables+        , pBindNameSP+        , pBoundName,           pBoundNameSP+        , pBoundIxSP+        , pBoundNameOpVarSP+        , pBoundNameOpSP++          -- * TyCons+        , pTyConBindName,       pTyConBindNameSP++          -- * DaCons+        , pDaConBindName+        , pDaConBoundName,      pDaConBoundNameSP+        , pDaConBoundLit,       pDaConBoundLitSP++          -- * Primitive Operators+        , pPrimValSP)+where+import DDC.Source.Tetra.Exp.Bind        hiding (Name)+import DDC.Source.Tetra.Prim+import DDC.Source.Tetra.Lexer+import DDC.Core.Lexer.Tokens+import DDC.Control.Parser               ((<?>))+import DDC.Control.Parser               (SourcePos(..))+import qualified DDC.Control.Parser     as P+import qualified Data.Text              as Text+++import DDC.Core.Parser+        ( pSym, pKey+        , pTok, pTokSP+        , pIndexSP)++type Parser a+        = P.Parser (Token Name) a+++-- Type and Term Variables ----------------------------------------------------+-- | Parse a binding occurrence of a named variable.+pBindNameSP  :: Parser (Bind, SourcePos)+pBindNameSP = P.pTokMaybeSP f <?> "a variable"+ where  f (KN (KVar (NameVar s)))       = Just (BName s)+        f _                             = Nothing+++-- | Parse a named term variable.+pBoundName :: Parser Bound+pBoundName = P.pTokMaybe f <?> "a variable"+ where  f (KN (KVar (NameVar s)))       = Just (UName s)+        f _                             = Nothing+++-- | Parse a named term variable.+pBoundNameSP :: Parser (Bound, SourcePos)+pBoundNameSP = P.pTokMaybeSP f <?> "a variable"+ where  f (KN (KVar (NameVar s)))       = Just (UName s)+        f _                             = Nothing+++-- | Parse an indexed term variable.+pBoundIxSP   :: Parser (Bound, SourcePos)+pBoundIxSP + = do   (i, sp) <- pIndexSP+        return  $ (UIx i, sp)+++-- | Parse an infix operator used as a variable.+pBoundNameOpSP :: Parser (Bound, SourcePos)+pBoundNameOpSP = P.pTokMaybeSP f+ where  f (KA (KOp s))                  = Just (UName (Text.pack s))+        f _                             = Nothing+++-- | Parse an infix operator used as a variable.+pBoundNameOpVarSP :: Parser (Bound, SourcePos)+pBoundNameOpVarSP = P.pTokMaybeSP f+ where  f (KA (KOpVar s))               = Just (UName (Text.pack s))+        f _                             = Nothing+++-- TyCons ---------------------------------------------------------------------+-- | Parse a binding occurrences of a type constructor name.+pTyConBindName :: Parser TyConBind+pTyConBindName = P.pTokMaybe f+ where  f (KN (KCon (NameCon n)))       = Just (TyConBindName n)+        f _                             = Nothing+++-- | Parse a binding occurrences of a type constructor name.+pTyConBindNameSP :: Parser (TyConBind, SourcePos)+pTyConBindNameSP = P.pTokMaybeSP f+ where  f (KN (KCon (NameCon n)))       = Just (TyConBindName n)+        f _                             = Nothing++++-- DaCons ---------------------------------------------------------------------+-- | Parse a binding occurrence of a data constructor name.+pDaConBindName :: Parser DaConBind+pDaConBindName = P.pTokMaybe f+ where  f (KN (KCon (NameCon n)))       = Just (DaConBindName n)+        f _                             = Nothing+++-- | Parse a bound occurrence of a data constructor name.+pDaConBoundName :: Parser DaConBound+pDaConBoundName = P.pTokMaybe f+ where  f (KN (KCon (NameCon n)))       = Just (DaConBoundName n)+        f _                             = Nothing+++-- | Parse a constructor name.+pDaConBoundNameSP :: Parser (DaConBound, SourcePos)+pDaConBoundNameSP = P.pTokMaybeSP f+ where  f (KN (KCon (NameCon n)))       = Just (DaConBoundName n)+        f _                             = Nothing+++-- | Parse a literal.+--    These are numeric literals, string literals, +--    and special constructors like 'True' and 'False'.+pDaConBoundLit :: Parser DaConBound+pDaConBoundLit = P.pTokMaybe f+ where  f (KA (KLiteral lit False))      = Just (DaConBoundLit (primLitOfLiteral lit))+        f (KN (KCon (NamePrimValLit n))) = Just (DaConBoundLit n)+        f _                              = Nothing+++-- | Parse a literal, with source position.+--    These are numeric literals, string literals, +--    and special constructors like 'True' and 'False'.+pDaConBoundLitSP :: Parser (DaConBound, SourcePos)+pDaConBoundLitSP = P.pTokMaybeSP f+ where  f (KA (KLiteral lit False))      = Just (DaConBoundLit (primLitOfLiteral lit))+        f (KN (KCon (NamePrimValLit n))) = Just (DaConBoundLit n)+        f _                              = Nothing+++-- Primitive Values -----------------------------------------------------------+pPrimValSP :: Parser (PrimVal, SourcePos)+pPrimValSP =  P.pTokMaybeSP f <?> "a primitive operator"+ where  f (KN (KVar (NamePrimValOp p))) = Just p+        f _                             = Nothing++

@@ -1,644 +1,778 @@---- | Parser for Source Tetra expressions.-module DDC.Source.Tetra.Parser.Exp-        ( context-        , pExp-        , pExpApp-        , pExpAtom,     pExpAtomSP-        , pLetsSP,      pClauseSP-        , pType-        , pTypeApp-        , pTypeAtom)-where-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 (..)-        , pBinder-        , pType-        , pTypeAtom-        , pTypeApp-        , pCon,         pConSP-        , pLit,         pLitSP-        ,               pStringSP-        , pIndexSP-        , pOpSP,        pOpVarSP-        , pTok-        , pTokSP)---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 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-        --  \x1 x2 : Type. Exp- [ do   sp      <- P.choice [ pTokSP KLambda, pTokSP KBackSlash ]--        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      <- P.choice [ pTokSP KBigLambda, pTokSP KBigLambdaSlash ]--        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--        -- let expression- , do   (lts, sp) <- pLetsSP c-        pTok    KIn-        x2      <- pExp c-        return  $ XLet sp lts x2--        -- Sugar for a let-expression.-        --  do { Stmt;+ }- , do   pTok    KDo-        pTok    KBraceBra-        xx      <- pStmts c-        pTok    KBraceKet-        return  $ xx--        -- case Exp of { Alt;+ }- , do   sp      <- pTokSP KCase-        x       <- pExp c-        pTok KOf -        pTok KBraceBra-        alts    <- P.sepEndBy1 (pAlt c) (pTok KSemiColon)-        pTok KBraceKet-        return  $ XCase sp x alts--        -- match { | EXP = EXP | EXP = EXP ... }-        --  Sugar for cascaded case expressions case-expression.- , do   sp      <- pTokSP KMatch-        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 KThen-        x2      <- pExp c-        pTok KElse-        x3      <- pExp c-        return  $ XCase sp x1 -                        [ AAlt pTrue    [GExp x2]-                        , AAlt PDefault [GExp x3]]--        -- weakeff [Type] in Exp- , do   sp      <- pTokSP KWeakEff-        pTok KSquareBra-        t       <- pType c-        pTok KSquareKet-        pTok KIn-        x       <- pExp c-        return  $ XCast sp (CastWeakenEffect t) x--        -- purify Witness in Exp- , do   sp      <- pTokSP KPurify-        w       <- pWitness c-        pTok KIn-        x       <- pExp c-        return  $ XCast sp (CastPurify w) x--        -- box Exp- , do   sp      <- pTokSP KBox-        x       <- pExp c-        return  $ XCast sp CastBox x--        -- run Exp- , do   sp      <- pTokSP KRun-        x       <- pExp c-        return  $ XCast sp CastRun x--        -- APP- , do   pExpApp c- ]-- <?> "an expression"----- Applications.-pExpApp :: Context Name -> Parser Name (Exp SP)-pExpApp c-  = do  xps     <- liftM concat $ P.many1 (pArgSPs c)-        let (xs, sps)   = unzip xps-        let sp1 : _     = sps-                -        case xs of-         [x]    -> return x-         _      -> return $ XDefix sp1 xs--  <?> "an expression or application"----- Comp, Witness or Spec arguments.-pArgSPs :: Context Name -> Parser Name [(Exp SP, SP)]-pArgSPs c- = P.choice-        -- [Type]- [ do   sp      <- pTokSP KSquareBra-        t       <- pType c-        pTok KSquareKet-        return  [(XType sp t, sp)]--        -- [: Type0 Type0 ... :]- , do   sp      <- pTokSP KSquareColonBra-        ts      <- P.many1 (pTypeAtom c)-        pTok KSquareColonKet-        return  [(XType sp t, sp) | t <- ts]-        -        -- { Witness }- , do   sp      <- pTokSP KBraceBra-        w       <- pWitness c-        pTok KBraceKet-        return  [(XWitness sp w, sp)]-                -        -- {: Witness0 Witness0 ... :}- , do   sp      <- pTokSP KBraceColonBra-        ws      <- P.many1 (pWitnessAtom c)-        pTok KBraceColonKet-        return  [(XWitness sp w, sp) | w <- ws]-               -        -- Exp0- , do   (x, sp)  <- pExpAtomSP c-        return  [(x, sp)]- ]- <?> "a type, witness or expression argument"----- | Parse a variable, constructor or parenthesised expression.-pExpAtom   :: Context Name -> Parser Name (Exp SP)-pExpAtom c- = do   (x, _) <- pExpAtomSP c-        return x----- | Parse a variable, constructor or parenthesised expression,---   also returning source position.-pExpAtomSP :: Context Name -> Parser Name (Exp SP, SP)-pExpAtomSP c- = P.choice- [      -- ( Exp2 )-   do   sp      <- pTokSP KRoundBra-        t       <- pExp c-        pTok KRoundKet-        return  (t, sp)--        -- Infix operator used as a variable.- , do   (str, sp) <- pOpVarSP-        return  (XInfixVar sp str, sp)--        -- Infix operator used nekkid.- , do   (str, sp) <- pOpSP-        return  (XInfixOp sp str, sp)-  -        -- The unit data constructor.       - , do   sp              <- pTokSP KDaConUnit-        return  (XCon sp dcUnit, sp)--        -- Named algebraic constructors.- , do   (con, sp)       <- pConSP-        return  (XCon sp (DaConBound con), sp)--        -- Literals.-        --  We just fill-in the type with tBot for now, and leave it to-        --  the spreader to attach the real type.-        --  We also set the literal as being algebraic, which may not be-        --  true (as for Floats). The spreader also needs to fix this.- , do   (lit, sp)       <- pLitSP-        return  (XCon sp (DaConPrim lit (T.tBot T.kData)), sp)-- , 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 (T.UIx   i), sp)-- ]-- <?> "a variable, constructor, or parenthesised type"----- Alternatives -------------------------------------------------------------------------------------- Case alternatives.-pAlt    :: Context Name -> Parser Name (Alt SP)-pAlt c- = do   p       <- pPat c-        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    :: Context Name -> Parser Name (Pat SP)-pPat c- = P.choice- [      -- Wildcard-   do   pTok KUnderscore-        return  $ PDefault--        -- Lit- , do   nLit    <- pLit-        return  $ PData (DaConPrim nLit (T.tBot T.kData)) []--        -- 'Unit'- , do   pTok KDaConUnit-        return  $ PData  dcUnit []--        -- Con Bind Bind ...- , do   nCon    <- pCon -        bs      <- P.many (pBindPat c)-        return  $ PData (DaConBound nCon) bs]----- Binds in patterns can have no type annotation,--- or can have an annotation if the whole thing is in parens.-pBindPat :: Context Name -> Parser Name Bind-pBindPat c- = P.choice-        -- Plain binder.- [ do   b       <- pBinder-        return  $ T.makeBindFromBinder b (T.tBot T.kData)--        -- Binder with type, wrapped in parens.- , do   pTok KRoundBra-        b       <- pBinder-        pTok (KOp ":")-        t       <- pType c-        pTok KRoundKet-        return  $ T.makeBindFromBinder b t- ]----- 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 :: Context Name -> Parser Name (Lets SP, SP)-pLetsSP c- = P.choice-    [ -- non-recursive let-      do sp       <- pTokSP KLet-         l        <- liftM fst $ pClauseSP c-         return (LGroup [l], sp)--      -- recursive let-    , do sp       <- pTokSP KLetRec-         pTok KBraceBra-         ls       <- liftM (map fst)-                  $  P.sepEndBy1 (pClauseSP c) (pTok KSemiColon)-         pTok KBraceKet-         return (LGroup ls, sp)--      -- Private region binding.-      --   private Binder+ (with { Binder : Type ... })? in Exp-    , do sp     <- pTokSP KPrivate-         -        -- new private region names.-         brs    <- P.manyTill pBinder -                $  P.try $ P.lookAhead $ P.choice [pTok KIn, pTok KWith]--         let bs =  map (flip T.makeBindFromBinder T.kRegion) brs-         -         -- Witness types.-         r      <- pLetWits c bs Nothing-         return (r, sp)--      -- Extend an existing region.-      --   extend Binder+ using Type (with { Binder : Type ...})? in Exp-    , do sp     <- pTokSP KExtend--         -- parent region-         t      <- pType c-         pTok KUsing--         -- new private region names.-         brs    <- P.manyTill pBinder -                $  P.try $ P.lookAhead -                         $ P.choice [pTok KUsing, pTok KWith, pTok KIn]--         let bs =  map (flip T.makeBindFromBinder T.kRegion) brs-         -         -- witness types-         r      <- pLetWits c bs (Just t)-         return (r, sp)-    ]-    -    -pLetWits :: Context Name-         -> [Bind] -> Maybe (T.Type Name)-         -> Parser Name (Lets SP)--pLetWits c bs mParent- = P.choice -    [ do   pTok KWith-           pTok KBraceBra-           wits    <- P.sepBy (P.choice-                      [ -- Named witness binder.-                        do b    <- pBinder-                           pTok (KOp ":")-                           t    <- pTypeApp c-                           return  $ T.makeBindFromBinder b t--                        -- Ambient witness binding, used for capabilities.-                      , do t    <- pTypeApp c-                           return  $ T.BNone t-                      ])-                      (pTok KSemiColon)-           pTok KBraceKet-           return (LPrivate bs mParent wits)-    -    , do   return (LPrivate bs mParent [])-    ]----- | A binding for let expression.-pClauseSP :: Context Name-          -> Parser Name (Clause SP, SP)--pClauseSP c- = do   b       <- pBinder--        P.choice-         [ do   -- Binding with full type signature.-                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.-                sp      <- pTokSP KEquals-                xBody   <- pExp c-                let t   = T.tBot T.kData-                return  ( SLet sp (T.makeBindFromBinder b t) [] [GExp xBody]-                        , sp)--         , do   -- Binding using function syntax.-                ps      <- liftM concat -                        $  P.many (pBindParamSpec c)-        -                P.choice-                 [ do   -- Function syntax with a return type.-                        -- We can make the full type sig for the let-bound variable.-                        --   Binder Param1 Param2 .. ParamN : Type = Exp-                        pTok (KOp ":")-                        tBody       <- pType c-                        (sp, xBody) <- pBindGuardsAsCaseSP c--                        let x   = expOfParams sp ps xBody-                        let t   = funTypeOfParams c ps tBody-                        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, xBody) <- pBindGuardsAsCaseSP c--                        let x   = expOfParams sp ps xBody-                        let t   = T.tBot T.kData-                        return  ( SLet sp (T.makeBindFromBinder b t) [] [GExp x]-                                , sp)-                 ]-         ]----- Statements --------------------------------------------------------------------------------------data Stmt n-        = StmtBind  SP Bind (Exp SP)-        | StmtMatch SP (Pat SP) (Exp SP) (Exp SP)-        | StmtNone  SP (Exp SP)----- | Parse a single statement.-pStmt :: Context Name -> Parser Name (Stmt Name)-pStmt c- = P.choice- [ -- Binder = Exp ;-   -- We need the 'try' because a VARIABLE binders can also be parsed-   --   as a function name in a non-binding statement.-   --  -   P.try $ -    do  br      <- pBinder-        sp      <- pTokSP KEquals-        x1      <- pExp c-        let t   = T.tBot T.kData-        let b   = T.makeBindFromBinder br t-        return  $ StmtBind sp b x1--   -- Pat <- Exp else Exp ;-   -- Sugar for a case-expression.-   -- We need the 'try' because the PAT can also be parsed-   --  as a function name in a non-binding statement.- , P.try $-    do  p       <- pPat c-        sp      <- pTokSP KArrowDashLeft-        x1      <- pExp c-        pTok KElse-        x2      <- pExp c-        return  $ StmtMatch sp p x1 x2--        -- Exp- , do   x               <- pExp c--        -- This should always succeed because pExp doesn't-        -- parse plain types or witnesses-        let Just sp     = takeAnnotOfExp x-        -        return  $ StmtNone sp x- ]----- | Parse some statements.-pStmts :: Context Name -> Parser Name (Exp SP)-pStmts c- = do   stmts   <- P.sepEndBy1 (pStmt c) (pTok KSemiColon)-        case makeStmts stmts of-         Nothing -> P.unexpected "do-block must end with a statement"-         Just x  -> return x----- | Make an expression from some statements.-makeStmts :: [Stmt Name] -> Maybe (Exp SP)-makeStmts ss- = case ss of-        [StmtNone _ x]    -         -> Just x--        StmtNone sp x1 : rest-         | Just x2      <- makeStmts rest-         -> Just $ XLet sp (LLet (T.BNone (T.tBot T.kData)) x1) x2--        StmtBind sp b x1 : rest-         | Just x2      <- makeStmts rest-         -> Just $ XLet sp (LLet b x1) x2--        StmtMatch sp p x1 x2 : rest-         | Just x3      <- makeStmts rest-         -> Just $ XCase sp x1 -                 [ AAlt p        [GExp x3]-                 , AAlt PDefault [GExp x2] ]--        _ -> Nothing+{-# LANGUAGE TypeFamilies #-}++-- | Parser for Source Tetra expressions.+module DDC.Source.Tetra.Parser.Exp+        ( pExp+        , pExpAppSP+        , pExpAtomSP+        , pLetsSP,      pClauseSP+        , pType+        , pTypeApp+        , pTypeAtomSP)+where+import DDC.Source.Tetra.Parser.Type+import DDC.Source.Tetra.Parser.Witness+import DDC.Source.Tetra.Parser.Base+import DDC.Source.Tetra.Exp+import DDC.Source.Tetra.Prim            as S+import DDC.Core.Lexer.Tokens+import Control.Monad.Except+import Data.Maybe+import qualified DDC.Control.Parser     as P+import qualified Data.Text              as Text+++type SP = SourcePos+++-- Exp --------------------------------------------------------------------------------------------+pExp   :: Parser Exp+pExp = fmap snd pExpWhereSP+++-- An expression that may have a trailing where clause.+pExpWhereSP :: Parser (SP, Exp)+pExpWhereSP + = do   (sp1, xx) <- pExpAppSP++        P.choice+         [ do   -- x where GROUP+                sp      <- pKey EWhere+                pSym SBraceBra+                cls     <- liftM (map snd)+                        $  P.sepEndBy1 pClauseSP (pSym SSemiColon)+                pSym SBraceKet+                return  (sp1, XWhere sp xx cls)++         , do   return  (sp1, xx) ]+++-- An application of a function to its arguments,+-- or a plain expression with no arguments.+pExpAppSP :: Parser (SP, Exp)+pExpAppSP+  = do  (spF, (xF, xsArg)) <- pExpAppsSP+        case xsArg of+                []     -> return (spF, xF)+                _      -> return (spF, XDefix spF (xF : xsArg))++  <?> "an expression or application"+++-- An application of a function to its arguments,+-- or a plan expression with no arguments.+pExpAppsSP :: Parser (SP, (Exp, [Exp]))+pExpAppsSP+ = do   (spF, xFun) <- pExpFrontSP+        xsArg       <- pExpArgsSP pExpAtomSP+        return (spF, (xFun, xsArg))+++-- A list of arguments.+pExpArgsSP :: Parser (SP, Exp) -> Parser [Exp]+pExpArgsSP pX+ = P.choice+ [ do   -- After an infix operator we allow the next expression+        -- to be a compound expression rather than an atom.+        --  This allows code like (f x $ λy. g x y) as in Haskell.+        (UName txOp, sp) <- pBoundNameOpSP+        xsMore           <- pExpArgsSP pExpFrontSP+        return  (XInfixOp  sp (Text.unpack txOp) : xsMore)++        -- Some arguments.+ , do   (_, xsArg)       <- pExpArgsSpecSP pX+        xsMore           <- pExpArgsSP     pExpAtomSP+        return  (xsArg ++ xsMore)++        -- No more arguments.+ , do   return  []+ ]+++-- Comp, Witness or Spec arguments.+pExpArgsSpecSP :: Parser (SP, Exp) -> Parser (SP, [Exp])+pExpArgsSpecSP pX+ = P.choice+        -- [Type]+ [ do   sp      <- pSym SSquareBra+        t       <- pType+        pSym    SSquareKet+        return  (sp, [XType t])++        -- [: Type0 Type0 ... :]+ , do   sp      <- pSym SSquareColonBra+        ts      <- fmap (fst . unzip) $ P.many1 pTypeAtomSP+        pSym    SSquareColonKet+        return  (sp, [XType t | t <- ts])+        +        -- { Witness }+ , do   sp      <- pSym SBraceBra+        w       <- pWitness+        pSym    SBraceKet+        return  (sp, [XWitness w])+                +        -- {: Witness0 Witness0 ... :}+ , do   sp      <- pSym SBraceColonBra+        ws      <- P.many1 pWitnessAtom+        pSym    SBraceColonKet+        return  (sp, [XWitness w | w <- ws])+               +        -- Exp0+ , do   (sp, x)  <- pX+        return  (sp, [x])+ ]+ <?> "a type, witness or expression argument"+++-- | Parse a compound Source Tetra expression.+--   The first token determines the form of the expression.+pExpFrontSP :: Parser (SP, Exp)+pExpFrontSP+ = P.choice++        -- Level-0 lambda abstractions+        --  \(x1 x2 ... : Type) (y1 y2 ... : Type) ... . Exp+        --  \x1 x2 : Type. Exp+        --  \x1 x2. Exp+ [ do   sp      <- P.choice +                        [ pSym SLambda+                        , pSym SBackSlash ]++        pts     <- P.choice+                [ P.try+                   $ fmap concat $ P.many1 +                   $ do pSym SRoundBra+                        ps      <- P.many1 pPat+                        pTok (KOp ":")+                        t       <- pType+                        pSym SRoundKet+                        return  [(p, Just t) | p <- ps]++                , do    ps      <- P.many1 pPatAtom+                        return  [(p, Nothing) | p <- ps]+                ]++        pSym    SArrowDashRight+        xBody   <- pExp+        return  (sp, XAnnot sp $ foldr (\(p, mt) -> XLamPat sp p mt) xBody pts)+++        -- Level-1 lambda abstractions.+        -- /\(x1 x2 ... : Type) (y1 y2 ... : Type) ... . Exp+ , do   sp      <- P.choice +                        [ pSym SBigLambda+                        , pSym SBigLambdaSlash ]++        bs      <- P.choice+                [ fmap concat $ P.many1+                   $ do pSym SRoundBra+                        bs'     <- P.many1 pBind+                        pTok (KOp ":")+                        t       <- pType+                        pSym SRoundKet+                        return  $ map (\b -> XBindVarMT b (Just t)) bs'++                , do    bs'     <- P.many1 pBind+                        return  $ map (\b -> XBindVarMT b Nothing) bs'+                ]++        pSym    SArrowDashRight+        xBody   <- pExp+        return  (sp, XAnnot sp $ foldr XLAM xBody bs)+++        -- let expression+ , do   (lts, sp) <- pLetsSP+        pTok    (KKeyword EIn)+        x2      <- pExp+        return  (sp, XAnnot sp $ XLet lts x2)+++        -- Sugar for a let-expression.+        --  do { Stmt;+ }+ , do   sp      <- pKey EDo+        pSym    SBraceBra+        xx      <- pStmts+        pSym    SBraceKet+        return  (sp, xx)+++        -- case Exp of { Alt;+ }+ , do   sp      <- pKey ECase+        x       <- pExp+        pKey    EOf+        pSym    SBraceBra+        alts    <- P.sepEndBy1 pAltCase (pSym SSemiColon)+        pSym    SBraceKet+        return  (sp, XAnnot sp $ XCase x alts)+++        -- match { | EXP = EXP | EXP = EXP ... }+        --  Sugar for cascaded case expressions case-expression.+ , do   sp      <- pKey EMatch+        pSym SBraceBra++        gxs     <- liftM (map (AAltMatch . snd))+                $  P.sepEndBy1  (pGuardedExpSP (pSym SEquals)) +                                (pSym SSemiColon)++        let xError+                = makeXErrorDefault +                        (Text.pack    $ sourcePosSource sp) +                        (fromIntegral $ sourcePosLine   sp)++        pSym SBraceKet+        return  (sp, XAnnot sp $ XMatch sp gxs xError)+++ , do   -- if-then-else+        --  Sugar for a case-expression.+        sp      <- pTokSP (KKeyword EIf)+        x1      <- pExp+        pTok (KKeyword EThen)+        x2      <- pExp+        pTok (KKeyword EElse)+        x3      <- pExp +        return  (sp, XAnnot sp $ XCase x1 +                        [ AAltCase PTrue    [GExp x2]+                        , AAltCase PDefault [GExp x3]])+++        -- weakeff [Type] in Exp+ , do   sp      <- pTokSP (KKeyword EWeakEff)+        pSym    SSquareBra+        t       <- pType+        pSym    SSquareKet+        pKey    EIn+        x       <- pExp+        return  (sp, XAnnot sp $ XCast (CastWeakenEffect t) x)+++        -- purify Witness in Exp+ , do   sp      <- pKey EPurify+        w       <- pWitness+        pTok (KKeyword EIn)+        x       <- pExp+        return  (sp, XAnnot sp $ XCast (CastPurify w) x)+++        -- box Exp+ , do   sp      <- pKey EBox+        x       <- pExp+        return  (sp, XAnnot sp $ XCast CastBox x)+++        -- run Exp+ , do   sp      <- pKey ERun+        x       <- pExp+        return  (sp, XAnnot sp $ XCast CastRun x)++        -- ATOM+ , do   pExpAtomSP+ ]+ <?> "an expression"+++-- | Parse a variable, constructor or parenthesised expression,+--   also returning source position.+pExpAtomSP :: Parser (SP, Exp)+pExpAtomSP+ = P.choice+ [ +        -- ( Exp2 )+   do   pSym SRoundBra+        (sp, t)  <- pExpWhereSP+        pSym SRoundKet+        return  (sp, t)++        -- Infix operator used as a variable.+ , do   (UName tx, sp) <- pBoundNameOpVarSP+        return  (sp, XInfixVar sp (Text.unpack tx))++        -- Infix operator used nekkid.+ , do   (UName tx, sp) <- pBoundNameOpSP+        return  (sp, XInfixOp  sp (Text.unpack tx))+  +        -- The unit data constructor.       + , do   sp              <- pTokSP (KBuiltin BDaConUnit)+        return  (sp, XCon  dcUnit)++        -- Named algebraic constructors.+ , do   (con, sp)       <- pDaConBoundNameSP+        return  (sp, XCon  (DaConBound con))++        -- Literals.+        --  We just fill-in the type with a hole for now, and leave it to+        --  We also set the literal as being algebraic, which may not be+        --  true (as for Floats). The spreader also needs to fix this.+ , do   (lit, sp)       <- pDaConBoundLitSP+        return  (sp, XCon (DaConPrim lit (TVar UHole)))++        -- Primitive names.+ , do   (nPrim, sp)     <- pPrimValSP+        return  (sp, XPrim nPrim)++        -- Named variables.+ , do   (u,  sp)        <- pBoundNameSP+        return  (sp, XVar u)++        -- Debruijn indices+ , do   (u, sp)         <- pBoundIxSP+        return  (sp, XVar u)++ ]+ <?> "a variable, constructor, or parenthesised type"+++-- Alternatives -----------------------------------------------------------------------------------+-- Case alternatives.+pAltCase :: Parser AltCase+pAltCase+ = do   p       <- pPat+        P.choice+         [ do   -- Desugar case guards while we're here.+                spgxs     <- P.many1 (pGuardedExpSP (pSym SArrowDashRight))+                let gxs  = map snd spgxs+                return  $ AAltCase p gxs +                +         , do   pSym SArrowDashRight+                x       <- pExp+                return  $ AAltCase p [GExp x] ]+++-- Patterns.+pPat :: Parser Pat+pPat+ = P.choice+ [  -- Con Bind Bind ...+    do  nCon    <- pDaConBoundName +        ps      <- P.many pPatAtom+        return  $ PData (DaConBound nCon) ps++    -- Atom+ ,  do  p       <- pPatAtom+        return  p+ ]+ <?> "a pattern"+++pPatAtom :: Parser Pat+pPatAtom+ = P.choice+ [ do   -- ( PAT )+        pSym SRoundBra+        p       <- pPat+        pSym SRoundKet+        return  $ p++        -- Wildcard+        --   Try this case before the following one for binders+        --   so that '_' is parsed as the default pattern,+        --   rather than a wildcard binder.+ , do   pSym SUnderscore+        return  $ PDefault++        -- Var+ , do   b       <- pBind+        P.choice+         [ do   _       <- pSym SAt+                p       <- pPatAtom+                return  $  PAt b p++         , do   return  $  PVar b+         ]++        -- Lit+ , do   nLit    <- pDaConBoundLit+        return  $ PData (DaConPrim nLit (TBot S.KData)) []++        -- Named algebraic constructors.+ , do   nCon    <- pDaConBoundName+        return  $ PData (DaConBound nCon) []++        -- 'Unit'+ , do   pTok    (KBuiltin BDaConUnit)+        return  $ PData  dcUnit []+ ]+ <?> "a pattern"+++-- Bindings ---------------------------------------------------------------------------------------+pLetsSP :: Parser (Lets, SP)+pLetsSP + = P.choice+    [ -- non-recursive let+      do sp       <- pKey ELet+         l        <- liftM snd $ pClauseSP+         return (LGroup [l], sp)++      -- recursive let+    , do sp       <- pKey ELetRec+         pSym SBraceBra+         ls       <- liftM (map snd)+                  $  P.sepEndBy1 pClauseSP (pSym SSemiColon)+         pSym SBraceKet+         return (LGroup ls, sp)++      -- Private region binding.+      --   private Binder+ (with { Binder : Type ... })? in Exp+    , do sp     <- pKey EPrivate+         +        -- new private region names.+         bs     <- P.manyTill pBind+                $  P.try +                        $ P.lookAhead +                        $ P.choice [pKey EIn, pKey EWith]+         +         -- Witness types.+         r      <- pLetWits bs Nothing+         return (r, sp)++      -- Extend an existing region.+      --   extend Binder+ using Type (with { Binder : Type ...})? in Exp+    , do sp     <- pTokSP (KKeyword EExtend)++         -- parent region+         t      <- pType+         pTok (KKeyword EUsing)++         -- new private region names.+         bs     <- P.manyTill pBind+                $  P.try $ P.lookAhead +                         $ P.choice +                                [ pTok (KKeyword EUsing)+                                , pTok (KKeyword EWith)+                                , pTok (KKeyword EIn) ]+         +         -- witness types+         r      <- pLetWits bs (Just t)+         return (r, sp)+    ]+    +    +pLetWits :: [Bind] -> Maybe Type -> Parser Lets+pLetWits bs mParent+ = P.choice +    [ do   pKey EWith+           pSym SBraceBra+           wits    <- P.sepBy (P.choice+                      [ -- Named witness binder.+                        do b    <- pBind+                           pTok (KOp ":")+                           t    <- pTypeApp+                           return (b, t)++                        -- Ambient witness binding, used for capabilities.+                      , do t    <- pTypeApp+                           return (BNone, t)+                      ])+                      (pSym SSemiColon)+           pSym SBraceKet+           return (LPrivate bs mParent wits)+    +    , do   return (LPrivate bs mParent [])+    ]+++-- | A binding for let expression.+pClauseSP :: Parser (SP, Clause)+pClauseSP+ = do   -- Name of the binding.+        (b, sp0) <- pBindNameSP++        P.choice+         [ do   -- Either +                -- 1) a definition with a signature and some clauses.+                --    foo : Nat -> Nat = ...+                -- 2) foo : Nat -> Nat+                --+                _       <- pTokSP (KOp ":")+                t       <- pType+                P.choice+                 [ do   +                        gxs     <- pTermGuardedExps (pSym SEquals)+                        return  (sp0,  SLet sp0 (XBindVarMT b (Just t)) [] gxs)++                 , do   return  (sp0,  SSig sp0 b t)+                 ]++         , do   -- Non-function binding with no type signature.+                gxs     <- pTermGuardedExps (pSym SEquals)+                return  (sp0, SLet sp0 (XBindVarMT b Nothing)  [] gxs)++         , do   -- Binding using function syntax.+                ps      <- fmap concat $ P.many pParamsSP+        +                P.choice+                 [ do   -- Function syntax with a return type.+                        -- We can make the full type sig for the let-bound variable.+                        --   Binder Param1 Param2 .. ParamN : Type = Exp+                        sp      <- pTokSP (KOp ":")+                        tBody   <- pType+                        gxs     <- pTermGuardedExps (pSym SEquals)++                        let t   = funTypeOfParams     ps tBody+                        return  (sp, SLet sp (XBindVarMT b (Just t))  ps gxs)++                        -- Function syntax with no return type.+                        -- We can't make the type sig for the let-bound variable.+                 , do   gxs     <- pTermGuardedExps (pSym SEquals)+                        return  (sp0, SLet sp0 (XBindVarMT b Nothing) ps gxs)+                 ]+         ]+++-- Function parameters.+pParamsSP :: Parser [Param]+pParamsSP+ = P.choice+        -- Type parameter+        -- [BIND1 BIND2 .. BINDN : TYPE]+ [ do   pSym SSquareBra+        bs      <- P.many1 pBind+        pTok (KOp ":")+        t       <- pType+        pSym SSquareKet+        return  [ MType b (Just t) | b <- bs]++        -- Witness parameter+        -- {BIND : TYPE}+ , do   pSym  SBraceBra+        b       <- pBind+        pTok (KOp ":")+        t       <- pType+        pSym  SBraceKet+        return  [ MWitness b (Just t) ]++        -- Value pattern with type annotations.+        -- (BIND1 BIND2 .. BINDN : TYPE) + , do   pSym    SRoundBra+        ps      <- P.choice+                [  P.try $ do+                        ps      <- P.many1 pPatAtom+                        pTok (KOp ":")+                        t       <- pType+                        return  [ MValue p (Just t) | p <- ps ]++                , do    p       <- pPat+                        return  [ MValue p Nothing ]+                ]++        pSym    SRoundKet+        return ps+++ , do   -- Value parameter without a type annotation.+        p       <- pPatAtom+        return  [MValue p Nothing]+ ]+ <?> "a function parameter"+++--   and the type of the body.+funTypeOfParams +        :: [Param]      -- ^ Spec of parameters.+        -> Type         -- ^ Type of body.+        -> Type         -- ^ Type of whole function.++funTypeOfParams [] tBody        + = tBody++funTypeOfParams (p:ps) tBody+ = case p of+        MType     b mt+         -> let k       = fromMaybe (TBot S.KData) mt+            in  TApp (TCon (TyConForall k)) (TAbs b k $ funTypeOfParams ps tBody)++        MWitness  _ mt+         -> let k       = fromMaybe (TBot S.KData) mt+            in  TImpl k $ funTypeOfParams ps tBody++        MValue    _ mt+         -> let k       = fromMaybe (TBot S.KData) mt+            in  TFun k  $ funTypeOfParams ps tBody++++-- Guards -----------------------------------------------------------------------------------------+-- | Parse either the terminating char and a single expression, +--   or some guarded expressions.+pTermGuardedExps+        :: Parser SP    -- ^ Parser for char between guards and exp+        -> Parser [GuardedExp]++pTermGuardedExps pTerm+ = P.choice+ [ do   _       <- pTerm+        xBody   <- pExp+        return  [GExp xBody]++ , do   fmap (map snd)+         $ P.many1 $ pGuardedExpSP pTerm+ ]+++-- | An guarded expression,+--   like | EXP1 = EXP2.+pGuardedExpSP +        :: Parser  SP   -- ^ Parser for char between and of guards and exp.+                        --   usually -> or =+        -> Parser  (SP, GuardedExp)++pGuardedExpSP pTermSP+ = pGuardExp (pSym SBar)++ where  pGuardExp pSepSP+         = P.choice+         [ do   sp      <- pSepSP+                g       <- pGuard+                gx      <- liftM snd $ pGuardExp (pSym SComma)+                return  (sp, GGuard g gx)++         , do   sp      <- pTermSP+                x       <- pExp+                return  (sp, GExp x) ]++        pGuard+         = P.choice +         [ P.try $+           do   p       <- pPat+                pSym    SArrowDashLeft+                x       <- pExp+                return $ GPat p x++         , do   g       <- pExp+                return $ GPred g++         , do   pKey    EOtherwise+                return GDefault ]+++-- Statements -------------------------------------------------------------------------------------+-- These are statements inside a do expression.+--   +--   A 'do' block behaves much the same way as a 'let' expression,+--   except we can write effectful statements without binding the+--   result to anything.+-- +--   We currently desugar do expressions to let-expressions in the parser.+--++-- | Represent a statement inside a do block.+data Stmt+        -- | Let-binding or type signature.+        = StmtClause SP Clause++        -- | Case match.+        | StmtMatch  SP Pat Exp Exp++        -- | Plain statement without binding the result.+        | StmtNone   SP Exp+++-- | Parse a single statement.+pStmt :: Parser Stmt+pStmt+ = P.choice+ [ -- Clause;+   -- We need the 'try' because the function and argument names at the front+   -- of a clause can also be parsed as a function application in a statement.+   P.try $ +    do  (sp, c)  <- pClauseSP+        return  $ StmtClause sp c++   -- Pat <- Exp else Exp ;+   -- Sugar for a case-expression.+   -- We need the 'try' because the PAT can also be parsed+   --  as a function name in a non-binding statement.+ , P.try $+    do  p       <- pPat+        sp      <- pSym SArrowDashLeft+        x1      <- pExp+        pTok (KKeyword EElse)+        x2      <- pExp+        return  $ StmtMatch sp p x1 x2++        -- Exp+ , do   (sp, x) <- pExpWhereSP+        return  $ StmtNone sp x+ ]+++-- | Parse some statements.+pStmts :: Parser Exp+pStmts + = do   -- Parse statements in the block.+        stmts   <- P.sepEndBy1 pStmt (pSym SSemiColon)+        +        -- As in Haskell, we require do blocks to end with a statement+        -- that gives the overall value.+        case makeStmts [] stmts of+         Nothing -> P.unexpected "do-block must end with a statement"+         Just x  -> return x+++-- | Make an expression from some statements.+--   We collect consecutive clauses into the same clause group, +--   so that we can define functions with multiple clauses at the top+--   level of a 'do' expression.+makeStmts :: [Clause] -> [Stmt] -> Maybe Exp+makeStmts clsAcc ss+ = let  +        -- Wrap the clauses we're carrying around the given+        -- body expression.+        dropClauses xBody+         = case clsAcc of+                []      -> xBody+                [SLet sp bmt [] [GExp x]]+                        -> XAnnot sp $ XLet (LLet bmt x) xBody+                _       -> XLet (LGroup clsAcc) xBody+   in+      case ss of+        [StmtNone _ x]    +         -> Just $ dropClauses+                 $ x++        StmtNone sp x1 : rest+         |  Just x2     <- makeStmts [] rest+         -> Just $ XAnnot sp +                 $ dropClauses+                 $ XLet (LLet (XBindVarMT BNone Nothing) x1) x2++        StmtClause _ cl : rest+         -> case clsAcc of+                -- Start accumulating successive clauses.+                [] -> makeStmts (clsAcc ++ [cl]) rest++                (cl1 : _)+                   -- If this clause is for the same function as+                   -- the previous one then we'll collect it into+                   -- at letrec at this point.+                   |  bindOfClause cl1 == bindOfClause cl+                   -> makeStmts (clsAcc ++ [cl]) rest++                   -- Otherwise make a standard let-expression.+                _  | Just x3 <- makeStmts [] rest+                   -> case cl of+                        (SLet sp bmt [] [GExp x])+                         -> Just $ XAnnot sp +                         $  dropClauses+                         $  XLet (LLet bmt x) x3++                        _ -> Nothing++                   | otherwise+                   -> Nothing+++        StmtMatch sp p x1 x2 : rest+         |  Just x3      <- makeStmts [] rest+         -> Just $ XAnnot sp +                 $ dropClauses+                 $ XCase x1 +                 [ AAltCase p        [GExp x3]+                 , AAltCase PDefault [GExp x2] ]++        _ -> Nothing+ 

@@ -8,66 +8,58 @@           -- * Top-level things         , pTop) where-import DDC.Source.Tetra.Parser.Exp-import DDC.Source.Tetra.Compounds-import DDC.Source.Tetra.DataDef-import DDC.Source.Tetra.Module-import DDC.Source.Tetra.Prim-import DDC.Source.Tetra.Exp.Annot-import DDC.Core.Lexer.Tokens-import DDC.Base.Pretty+import DDC.Source.Tetra.Parser.Exp      as S+import DDC.Source.Tetra.Parser.Base     as S+import DDC.Source.Tetra.Module          as S+import DDC.Source.Tetra.DataDef         as S+import DDC.Source.Tetra.Exp             as S+import DDC.Core.Lexer.Tokens            as K+import DDC.Data.Pretty import Control.Monad-import qualified DDC.Type.Exp           as T-import qualified DDC.Base.Parser        as P-import DDC.Base.Parser                  ((<?>))+import qualified DDC.Control.Parser     as P+import qualified Data.Text              as Text  import DDC.Core.Parser-        ( Parser-        , Context       (..)-        , pModuleName-        , pName-        , pVar-        , pTok,         pTokSP)--type SP = P.SourcePos+        ( pModuleName+        , pName)   -- Module ----------------------------------------------------------------------------------------- -- | Parse a source tetra module.-pModule :: Context Name -> Parser Name (Module (Annot SP))-pModule c+pModule :: Parser (Module Source)+pModule   = do   -        _sp     <- pTokSP KModule+        _sp     <- pTokSP (KKeyword EModule)         name    <- pModuleName <?> "a module name"          -- export { VAR;+ }         tExports           <- P.choice-            [do pTok KExport-                pTok KBraceBra-                vars    <- P.sepEndBy1 pVar (pTok KSemiColon)-                pTok KBraceKet-                return vars+            [ do pKey EExport+                 pSym SBraceBra+                 vars <- P.sepEndBy1 pBoundName (pSym SSemiColon)+                 pSym SBraceKet+                 return vars -            ,   return []]+            ,    return []]          -- import { SIG;+ }         tImports-         <- liftM concat $ P.many (pImportSpecs c)+         <- liftM concat $ P.many pImportSpecs          -- top-level declarations.         tops              <- P.choice-            [do pTok KWhere-                pTok KBraceBra+            [ do pKey EWhere+                 pSym SBraceBra -                -- TOP;+-                tops    <- P.sepEndBy (pTop c) (pTok KSemiColon)+                 -- TOP;++                 tops <- P.sepEndBy pTop (pSym SSemiColon) -                pTok KBraceKet-                return tops+                 pSym SBraceKet+                 return tops -            ,do return [] ]+            , do return [] ]           -- ISSUE #295: Check for duplicate exported names in module parser.@@ -85,174 +77,186 @@   -- | Parse a type signature.-pTypeSig :: Context Name -> Parser Name (Name, T.Type Name)-pTypeSig c- = do   var     <- pVar+pTypeSig :: Parser (Bind, Type)+pTypeSig + = do   (b, _)  <- pBindNameSP         pTokSP (KOp ":")-        t       <- pType c-        return  (var, t)+        t       <- pType+        return  (b, t)   --------------------------------------------------------------------------------------------------- -- | An imported foreign type or foreign value.-data ImportSpec n+data ImportSpec          = ImportModule  ModuleName-        | ImportType    n (ImportType  n)-        | ImportCap     n (ImportCap   n)-        | ImportValue   n (ImportValue n)+        | ImportType    TyConBind (ImportType  TyConBind Type)+        | ImportCap     Bind      (ImportCap   Bind      Type)+        | ImportValue   Bind      (ImportValue Bind      Type)         deriving Show           -- | Parse some import specs.-pImportSpecs :: Context Name -> Parser Name [ImportSpec Name]-pImportSpecs c- = do   pTok KImport+pImportSpecs :: Parser [ImportSpec]+pImportSpecs+ = do   pTok (KKeyword EImport)          P.choice                 -- import foreign ...-         [ do   pTok KForeign+         [ do   pTok (KKeyword EForeign)                 src    <- liftM (renderIndent . ppr) pName                  P.choice                  [      -- import foreign X type (NAME :: TYPE)+ -                  do    pTok KType-                        pTok KBraceBra--                        sigs <- P.sepEndBy1 (pImportType c src) (pTok KSemiColon)-                        pTok KBraceKet+                  do    pKey EType+                        pSym SBraceBra+                        sigs <- P.sepEndBy1 (pImportType src)       (pSym SSemiColon)+                        pSym SBraceKet                         return sigs                          -- import foreign X capability (NAME :: TYPE)+-                 , do   pTok KCapability-                        pTok KBraceBra--                        sigs <- P.sepEndBy1 (pImportCapability c src) (pTok KSemiColon)-                        pTok KBraceKet+                 , do   pKey ECapability+                        pSym SBraceBra+                        sigs <- P.sepEndBy1 (pImportCapability src) (pSym SSemiColon)+                        pSym SBraceKet                         return sigs                          -- import foreign X value (NAME :: TYPE)+-                 , do   pTok KValue-                        pTok KBraceBra--                        sigs <- P.sepEndBy1 (pImportValue c src) (pTok KSemiColon)-                        pTok KBraceKet+                 , do   pKey EValue+                        pSym SBraceBra+                        sigs <- P.sepEndBy1 (pImportValue src)      (pSym SSemiColon)+                        pSym SBraceKet                         return sigs                  ] -         , do   pTok KBraceBra-                names   <- P.sepEndBy1 pModuleName (pTok KSemiColon) -                                <?> "module names"-                pTok KBraceKet+         , do   pSym SBraceBra+                names   <-  P.sepEndBy1 pModuleName (pSym SSemiColon) +                        <?> "module names"+                pSym SBraceKet                 return  [ImportModule n | n <- names]          ]   -- | Parse a type import spec.-pImportType :: Context Name -> String -> Parser Name (ImportSpec Name)-pImportType c src+pImportType :: String -> Parser ImportSpec+pImportType src         | "abstract"    <- src-        = do    n       <- pName+        = do    b       <- pTyConBindName                 pTokSP (KOp ":")-                k       <- pType c-                return  (ImportType n (ImportTypeAbstract k))+                k       <- pType+                return  (ImportType b (ImportTypeAbstract k)) -        | "boxed"        <- src-        = do    n       <- pName+        | "boxed"       <- src+        = do    b       <- pTyConBindName                 pTokSP (KOp ":")-                k       <- pType c-                return  (ImportType n (ImportTypeBoxed k))+                k       <- pType+                return  (ImportType b (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+pImportCapability :: String -> Parser ImportSpec+pImportCapability src         | "abstract"    <- src-        = do    n       <- pName+        = do    (b, _)  <- pBindNameSP                 pTokSP (KOp ":")-                t       <- pType c-                return  (ImportCap n (ImportCapAbstract t))+                t       <- pType+                return  (ImportCap b (ImportCapAbstract t))          | otherwise         = P.unexpected "import mode for foreign capability"   -- | Parse a value import spec.-pImportValue :: Context Name -> String -> Parser Name (ImportSpec Name)-pImportValue c src+pImportValue :: String -> Parser ImportSpec+pImportValue src         | "c"           <- src-        = do    n       <- pName+        = do    (b@(BName n), _)  <- pBindNameSP                 pTokSP (KOp ":")-                k       <- pType c+                k       <- pType                  -- ISSUE #327: Allow external symbol to be specified                  --             with foreign C imports and exports.-                let symbol = renderIndent (ppr n)+                let symbol = renderIndent (text $ Text.unpack n) -                return  (ImportValue n (ImportValueSea symbol k))+                return  (ImportValue b (ImportValueSea symbol k))          | otherwise         = P.unexpected "import mode for foreign value"   -- Top Level ---------------------------------------------------------------------------------------pTop    :: Context Name -> Parser Name (Top (Annot SP))-pTop c+pTop    :: Parser (Top Source)+pTop  = P.choice  [ do   -- A top-level, possibly recursive binding.-        (l, sp)         <- pClauseSP c+        (sp, l)         <- pClauseSP         return  $ TopClause sp l           -- A data type declaration- , do   pData c+ , do   pDataDef++        -- A type binding+ , do   pTypeDef  ]   -- Data ------------------------------------------------------------------------------------------- -- | Parse a data type declaration.-pData   :: Context Name -> Parser Name (Top (Annot SP))-pData c- = do   sp      <- pTokSP KData-        n       <- pName-        ps      <- liftM concat $ P.many (pDataParam c)+pDataDef :: Parser (Top Source)+pDataDef+ = do   sp      <- pTokSP (KKeyword EData)+        b       <- pTyConBindName+        ps      <- liftM concat $ P.many pTypeParam                       P.choice          [ -- Data declaration with constructors that have explicit types.-           do   pTok KWhere-                pTok KBraceBra-                ctors   <- P.sepEndBy1 (pDataCtor c) (pTok KSemiColon)-                pTok KBraceKet-                return  $ TopData sp (DataDef n ps ctors)+           do   pKey EWhere+                pSym SBraceBra+                ctors   <- P.sepEndBy1 pDataCtor (pSym SSemiColon)+                pSym SBraceKet+                return  $ TopData sp (DataDef b ps ctors)                      -- Data declaration with no data constructors.-         , do   return  $ TopData sp (DataDef n ps [])+         , do   return  $ TopData sp (DataDef b ps [])          ] ---- | Parse a type parameter to a data type.-pDataParam :: Context Name -> Parser Name [Bind]-pDataParam c - = do   pTok KRoundBra-        ns      <- P.many1 pName-        pTokSP (KOp ":")-        k       <- pType c-        pTok KRoundKet-        return  [T.BName n k | n <- ns]-- -- | Parse a data constructor declaration.-pDataCtor :: Context Name -> Parser Name (DataCtor Name)-pDataCtor c- = do   n       <- pName+pDataCtor :: Parser (DataCtor Source)+pDataCtor+ = do   n       <- pDaConBindName         pTokSP (KOp ":")-        t       <- pType c-        let (tsArg, tResult)    -                = takeTFunArgResult t+        t       <- pType+        let (tsArg, tResult) = takeTFuns t          return  $ DataCtor                 { dataCtorName          = n                 , dataCtorFieldTypes    = tsArg                 , dataCtorResultType    = tResult }+++-- Type -------------------------------------------------------------------------------------------+pTypeDef :: Parser (Top Source)+pTypeDef+ = do   sp      <- pKey EType+        bType   <- pTyConBindName+        bsParam <- liftM concat $ P.many pTypeParam+        _       <- pSym SEquals+        tBody   <- pType++        return  $  TopType sp bType +                $  foldr (\(b, k) t -> TAbs b k t) tBody bsParam+++-- | Parse a type parameter to a data type or type function.+pTypeParam :: Parser [(Bind, Type)]+pTypeParam + = do   pSym SRoundBra+        bs      <- fmap (fst . unzip) $ P.many1 pBindNameSP+        pTokSP (KOp ":")+        k       <- pType+        pSym SRoundKet+        return  [(b, k) | b <- bs]+ 

@@ -2,33 +2,125 @@ -- | Desugaring of function parameter syntax in Source Tetra. module DDC.Source.Tetra.Parser.Param         ( ParamSpec     (..)+        , expOfParams         , funTypeOfParams         , pBindParamSpec-        , expOfParams)+        , pBindParamSpecAnnot) where-import DDC.Source.Tetra.Exp.Annot-import DDC.Core.Parser-        ( ParamSpec(..)-        , funTypeOfParams-        , pBindParamSpec)+import DDC.Source.Tetra.Parser.Base+import DDC.Source.Tetra.Parser.Type+import DDC.Source.Tetra.Exp.Source+import Data.Maybe+import DDC.Core.Lexer.Tokens            as K+import qualified DDC.Control.Parser     as P  +-- | Specification of a function parameter.+--   We can determine the contribution to the type of the function, +--   as well as its expression based on the parameter.+data ParamSpec+        = ParamType    Bind (Maybe Type)+        | ParamWitness Bind (Maybe Type)+        | ParamValue   Bind (Maybe Type)++ -- | Build the expression of a function from specifications of its parameters, --   and the expression for the body. expOfParams -        :: a-        -> [ParamSpec Name]     -- ^ Spec of parameters.-        -> Exp a                -- ^ Body of function.-        -> Exp a                -- ^ Expression of whole function.+        :: [ParamSpec]  -- ^ Spec of parameters.+        -> Exp          -- ^ Body of function.+        -> Exp          -- ^ Expression of whole function. -expOfParams _ [] xBody            = xBody-expOfParams a (p:ps) xBody+expOfParams [] xBody            = xBody+expOfParams (p:ps) xBody  = case p of-        ParamType b     -         -> XLAM a b $ expOfParams a ps xBody+        ParamType    b mt+         -> XLAM (XBindVarMT b mt) $ expOfParams ps xBody         -        ParamWitness b-         -> XLam a b $ expOfParams a ps xBody+        ParamWitness b mt+         -> XLam (XBindVarMT b mt) $ expOfParams ps xBody -        ParamValue b _ _-         -> XLam a b $ expOfParams a ps xBody+        ParamValue   b mt+         -> XLam (XBindVarMT b mt) $ expOfParams ps xBody+++-- | Build the type of a function from specifications of its parameters,+--   and the type of the body.+funTypeOfParams +        :: [ParamSpec]          -- ^ Spec of parameters.+        -> Type                 -- ^ Type of body.+        -> Type                 -- ^ Type of whole function.++funTypeOfParams [] tBody        + = tBody++funTypeOfParams (p:ps) tBody+ = case p of+        ParamType     b mt+         -> let k       = fromMaybe (TBot KData) mt+            in  TApp (TCon (TyConForall k)) (TAbs b k $ funTypeOfParams ps tBody)++        ParamWitness  _ mt+         -> TImpl (fromMaybe (TBot KData) mt)+          $ funTypeOfParams ps tBody++        ParamValue    _ mt+         -> TFun  (fromMaybe (TBot KData) mt)+          $ funTypeOfParams ps tBody+++-- | Parse a function parameter specification,+--   with an optional type (or kind) annotation.+pBindParamSpec :: Parser [ParamSpec]+pBindParamSpec+ = P.choice+ [      -- Value (or type) binder with a type (or kind) annotation.+        pBindParamSpecAnnot++        -- Value binder without type annotations.+  , do  b       <- pBind+        return  $  [ ParamValue b Nothing ]+ ]+++-- | Parse a function parameter specification,+--   requiring a full type (or kind) annotation.+---+--       [BIND1 BIND2 .. BINDN : TYPE]+--   or  (BIND : TYPE)+--   or  (BIND : TYPE) { EFFECT | CLOSURE }+--+pBindParamSpecAnnot :: Parser [ParamSpec]+pBindParamSpecAnnot + = P.choice+        -- Type parameter+        -- [BIND1 BIND2 .. BINDN : TYPE]+ [ do   pSym    SSquareBra+        bs      <- P.many1 pBind+        pTok    (K.KOp ":")+        t       <- pType+        pSym    SSquareKet+        return  [ ParamType b (Just t) | b <- bs]++        -- Witness parameter+        -- {BIND : TYPE}+ , do   pSym    SBraceBra+        b       <- pBind+        pTok    (K.KOp ":")+        t       <- pType+        pSym    SBraceKet+        return  [ ParamWitness b (Just t) ]++        -- Value parameter with type annotations.+        -- (BIND1 BIND2 .. BINDN : TYPE) +        -- (BIND1 BIND2 .. BINDN : TYPE) { TYPE | TYPE }+ , do   pSym    SRoundBra+        bs      <- P.many1 pBind+        pTok    (K.KOp ":")+        t       <- pType+        pSym    SRoundKet++        return  $  [ ParamValue b (Just t) | b <- bs ]+ ]++

@@ -0,0 +1,205 @@+{-# LANGUAGE TypeFamilies #-}+module DDC.Source.Tetra.Parser.Type+        ( pBind+        , pType+        , pTypeUnion+        , pTypeApp+        , pTypeAtomSP+        , pTyConSP+        , pTyConBound)+where+import DDC.Source.Tetra.Parser.Base     as S+import DDC.Source.Tetra.Exp.Source      as S+import DDC.Source.Tetra.Prim.TyConTetra as S+import DDC.Core.Lexer.Tokens            as K+import qualified DDC.Source.Tetra.Lexer as SL++import qualified DDC.Core.Tetra         as C+import qualified DDC.Control.Parser     as P+import qualified Data.Text              as T+++-- | Parse a binder.+pBind :: Parser Bind+pBind+ = P.choice+        -- Named binders.+        [ do    (b, _)  <- pBindNameSP+                return  $  b+                +        -- Anonymous binders.+        , do    pSym SHat+                return  $  BAnon +        +        -- Vacant binders.+        , do    pSym SUnderscore+                return  $  BNone ]+ <?> "a binder"+++-- | Parse a type.+pType :: Parser Type+pType = pTypeUnion+++-- | Parse a type union.+pTypeUnion :: Parser Type+pTypeUnion+ = do   t1      <- pTypeForall+        P.choice +         [ -- Type sums.+           -- T2 + T3+           do   sp      <- pTokSP (KOp "+")+                t2      <- pTypeUnion+                return  $  TAnnot sp $ TUnion KEffect t1 t2++         , do   return t1 ]+ <?> "a type"+++-- | Parse a quantified type.+pTypeForall :: Parser Type+pTypeForall+ = P.choice+         [ -- Universal quantification.+           -- [v1 v1 ... vn : T1]. T2+           do   pSym SSquareBra+                bs      <- P.many1 pBind+                sp      <- pTokSP (KOp ":")+                kBind   <- pTypeUnion+                pSym SSquareKet+                pSym SDot++                tBody   <- pTypeForall+                return  $ foldr (\b t   -> TAnnot sp +                                        $  TApp (TCon (TyConForall kBind)) +                                                (TAbs b kBind t)) +                                tBody bs++           -- Body type+         , do   pTypeFun+         ]+ <?> "a type"+++-- | Parse a function type.+pTypeFun :: Parser Type+pTypeFun+ = do   t1      <- pTypeApp+        P.choice +         [ -- T1 ~> T2+           do   sp      <- pSym SArrowTilde+                t2      <- pTypeForall+                return  $  TAnnot sp $ TFun t1 t2++           -- T1 => T2+         , do   sp      <- pSym SArrowEquals+                t2      <- pTypeForall+                return  $  TAnnot sp $ TImpl t1 t2++           -- T1 -> T2+         , do   sp      <- pSym SArrowDashRight+                t2      <- pTypeForall+                return  $  TAnnot sp $ TFun  t1 t2++           -- Body type+         , do   return t1 +         ]+ <?> "an atomic type or type application"+++-- | Parse a type application.+pTypeApp :: Parser Type+pTypeApp+ = do   ((t, _):ts)  <- P.many1 pTypeAtomSP+        return  $  foldl (\t1 (t2, sp) -> TAnnot sp (TApp t1 t2)) t ts+ <?> "an atomic type or type application"+++-- | Parse a variable, constructor or parenthesised type.+pTypeAtomSP :: Parser (Type, SourcePos)+pTypeAtomSP+ = P.choice+        -- (~>) and (=>) and (->) and (TYPE2)+        [ -- (~>)+          do    sp      <- pTokSP $ KOpVar "~>"+                return  (TAnnot sp $ TCon  TyConFun,  sp)++          -- (=>)+        , do    sp      <- pTokSP $ KOpVar "=>"+                return  (TAnnot sp $ TCon (TyConPrim (PrimTypeTwCon TwConImpl)), sp)++          -- (->)+        , do    sp      <- pTokSP $ KOpVar "->"+                return  (TAnnot sp $ TCon TyConFun,  sp)++          -- (TYPE2)+        , do    sp      <- pSym SRoundBra+                t       <- pTypeUnion+                pSym SRoundKet+                return  (t, sp)++        -- Named type constructors+        , do    (tc, sp) <- pTyConSP +                return  (TAnnot sp $ TCon tc, sp)+            +        -- Bottoms.+        , do    sp       <- pTokSP (KBuiltin BPure)+                return  (TAnnot sp $ TBot KEffect, sp)++        -- Bound occurrence of a variable.+        --  We don't know the kind of this variable yet, so fill in the+        --  field with the bottom element of computation kinds. This isn't+        --  really part of the language, but makes sense implentation-wise.+        , do    (u, sp) <- pBoundNameSP+                return  (TAnnot sp $ TVar u, sp)++        , do    (u, sp) <- pBoundIxSP+                return  (TAnnot sp $ TVar u, sp)+        ]+ <?> "an atomic type"+++-- | Parse a type constructor.+pTyConSP :: Parser (TyCon, SourcePos)+pTyConSP  =   P.pTokMaybeSP f <?> "a type constructor"+ where f kk+        = case kk of+                -- Primitive Ambient TyCons.+                KA (KBuiltin (BSoCon c))+                 -> Just $ TyConPrim $ PrimTypeSoCon c++                KA (KBuiltin (BKiCon c))+                 -> Just $ TyConPrim $ PrimTypeKiCon c++                KA (KBuiltin (BTwCon c))+                 -> Just $ TyConPrim $ PrimTypeTwCon c++                KA (KBuiltin (BTcCon c))+                 -> Just $ TyConPrim $ PrimTypeTcCon c++                -- Primitive TyCons.+                KN (KCon (SL.NamePrimType tc))+                 -> Just $ TyConPrim tc++                -- User Bound TyCons.+                KN (KCon (SL.NameCon tx))+                 -> Just (TyConBound (TyConBoundName tx))++                _ -> Nothing+++-- | Parse a bound type constructor.+--   Known primitive type constructors do not match.+pTyConBound :: Parser TyCon+pTyConBound  +        =   P.pTokMaybe f <?> "a bound type constructor"+ where  +        f :: Token SL.Name -> Maybe TyCon+        f (KN (KCon (SL.NameCon tx)))+         |  Nothing <- C.readPrimTyCon      (T.unpack tx)+         ,  Nothing <- S.readPrimTyConTetra (T.unpack tx)+         = Just (TyConBound (TyConBoundName tx))++        f _ = Nothing+

@@ -4,97 +4,86 @@         , 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 DDC.Source.Tetra.Parser.Type+import DDC.Source.Tetra.Parser.Base+import DDC.Source.Tetra.Exp.Source import Control.Monad.Except+import DDC.Core.Lexer.Tokens            as K+import qualified DDC.Control.Parser     as P  type SP = SourcePos   -- | Parse a witness expression.-pWitness      :: Context Name -> Parser Name (Witness SP)-pWitness c = pWitnessJoin c+pWitness :: Parser Witness+pWitness = pWitnessJoin   -- | Parse a witness join.-pWitnessJoin  :: Context Name -> Parser Name (Witness SP)-pWitnessJoin c+pWitnessJoin :: Parser Witness+pWitnessJoin     -- WITNESS  or  WITNESS & WITNESS- = do   w1      <- pWitnessApp c+ = do   w1      <- pWitnessApp         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)+pWitnessApp :: Parser Witness+pWitnessApp +  = do  (x:xs)  <- P.many1 pWitnessArgSP         let x'  = fst x         let sp  = snd x         let xs' = map fst xs-        return  $ foldl (WApp sp) x' xs'+        return  $ foldl (\w1 w2 -> WAnnot sp $ WApp w1 w2) x' xs'   <?> "a witness expression or application"   -- | Parse a witness argument.-pWitnessArgSP :: Context Name -> Parser Name (Witness SP, SP)-pWitnessArgSP c+pWitnessArgSP :: Parser (Witness, SP)+pWitnessArgSP   = P.choice  [ -- [TYPE]-   do   sp      <- pTokSP KSquareBra-        t       <- pType c-        pTok KSquareKet-        return  (WType sp t, sp)+   do   sp      <- pSym SSquareBra+        t       <- pType+        pSym SSquareKet+        return  (WAnnot sp $ WType t, sp)     -- WITNESS- , do   pWitnessAtomSP c ]+ , do   pWitnessAtomSP ]    -- | Parse a variable, constructor or parenthesised witness.-pWitnessAtom   :: Context Name -> Parser Name (Witness SP)-pWitnessAtom c   -        = liftM fst (pWitnessAtomSP c)+pWitnessAtom :: Parser Witness+pWitnessAtom =  liftM fst pWitnessAtomSP   -- | Parse a variable, constructor or parenthesised witness, --   also returning source position.-pWitnessAtomSP :: Context Name -> Parser Name (Witness SP, SP)-pWitnessAtomSP c+pWitnessAtomSP :: Parser (Witness, SP)+pWitnessAtomSP   = P.choice    -- (WITNESS)- [ do   sp      <- pTokSP KRoundBra-        w       <- pWitness c-        pTok KRoundKet+ [ do   sp      <- pSym SRoundBra+        w       <- pWitness+        pSym SRoundKet         return  (w, sp)     -- Named constructors- , do   (con, sp) <- pConSP-        return  (WCon sp (WiConBound (T.UName con) (T.tBot T.kWitness)), sp)+ , do   (DaConBoundName n, sp) <- pDaConBoundNameSP+        return  ( WAnnot sp $ WCon (WiConBound (UName n) (TBot KData))+                , sp)                     -- Debruijn indices- , do   (i, sp) <- pIndexSP-        return  (WVar sp (T.UIx   i), sp)+ , do   (u, sp) <- pBoundIxSP+        return  ( WAnnot sp $ WVar u, sp)     -- Variables- , do   (var, sp) <- pVarSP-        return  (WVar sp (T.UName var), sp) ]+ , do   (u, sp) <- pBoundNameSP+        return  ( WAnnot sp $ WVar u, sp)+ ]   <?> "a witness"