ddc-core 0.3.1.1 → 0.3.2.1

raw patch · 64 files changed

+2950/−1747 lines, 64 filesdep ~ddc-basePVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: ddc-base

API changes (from Hackage documentation)

Files

• DDC/Core/Annot/AnT.hs +35/−0
• DDC/Core/Annot/AnTEC.hs +50/−0
• DDC/Core/Check/CheckDaCon.hs +1/−1
• DDC/Core/Check/CheckExp.hs +117/−92
• DDC/Core/Check/CheckModule.hs +2/−2
• DDC/Core/Check/CheckWitness.hs +49/−72
• DDC/Core/Check/Error.hs +22/−37
• DDC/Core/Check/ErrorMessage.hs +17/−37
• DDC/Core/Collect/Free.hs +9/−16
• DDC/Core/Collect/Support.hs +13/−17
• DDC/Core/Compounds.hs +2/−327
• DDC/Core/Compounds/Annot.hs +342/−0
• DDC/Core/Compounds/Simple.hs +293/−0
• DDC/Core/DaCon.hs +0/−100
• DDC/Core/Exp.hs +2/−21
• DDC/Core/Exp/Annot.hs +202/−0
• DDC/Core/Exp/Base.hs +0/−186
• DDC/Core/Exp/DaCon.hs +101/−0
• DDC/Core/Exp/NFData.hs +0/−82
• DDC/Core/Exp/Pat.hs +26/−0
• DDC/Core/Exp/Simple.hs +202/−0
• DDC/Core/Exp/WiCon.hs +75/−0
• DDC/Core/Fragment.hs +0/−1
• DDC/Core/Fragment/Compliance.hs +12/−20
• DDC/Core/Fragment/Error.hs +4/−4
• DDC/Core/Fragment/Feature.hs +10/−11
• DDC/Core/Fragment/Profile.hs +17/−10
• DDC/Core/Lexer.hs +31/−24
• DDC/Core/Lexer/Names.hs +43/−8
• DDC/Core/Lexer/Tokens.hs +16/−18
• DDC/Core/Load.hs +29/−18
• DDC/Core/Parser.hs +3/−1
• DDC/Core/Parser/Base.hs +62/−16
• DDC/Core/Parser/Context.hs +34/−0
• DDC/Core/Parser/Exp.hs +206/−187
• DDC/Core/Parser/Module.hs +24/−19
• DDC/Core/Parser/Param.hs +43/−31
• DDC/Core/Parser/Type.hs +82/−41
• DDC/Core/Parser/Witness.hs +61/−32
• DDC/Core/Predicates.hs +12/−1
• DDC/Core/Pretty.hs +30/−16
• DDC/Core/Transform/Annotate.hs +92/−0
• DDC/Core/Transform/Deannotate.hs +78/−0
• DDC/Core/Transform/LiftT.hs +25/−41
• DDC/Core/Transform/LiftX.hs +14/−24
• DDC/Core/Transform/Reannotate.hs +30/−19
• DDC/Core/Transform/Rename.hs +6/−14
• DDC/Core/Transform/SpreadX.hs +11/−15
• DDC/Core/Transform/SubstituteTX.hs +10/−18
• DDC/Core/Transform/SubstituteWX.hs +20/−29
• DDC/Core/Transform/SubstituteXX.hs +7/−6
• DDC/Core/Transform/Trim.hs +1/−1
• DDC/Type/Check.hs +38/−27
• DDC/Type/Check/CheckCon.hs +4/−2
• DDC/Type/Check/Config.hs +66/−0
• DDC/Type/Check/ErrorMessage.hs +2/−2
• DDC/Type/Compounds.hs +154/−29
• DDC/Type/Env.hs +5/−2
• DDC/Type/Exp/Base.hs +41/−35
• DDC/Type/Pretty.hs +32/−15
• DDC/Type/Transform/Trim.hs +1/−1
• DDC/Type/Universe.hs +1/−1
• LICENSE +1/−1
• ddc-core.cabal +32/−17

@@ -0,0 +1,35 @@++module DDC.Core.Annot.AnT+        (AnT (..))+where+import DDC.Type.Exp+import DDC.Base.Pretty+import Control.DeepSeq+import Data.Typeable+++-- Annot ----------------------------------------------------------------------+-- | The type checker for witnesses adds this annotation to every node in the,+--   giving the type of each component of the witness.+---+--   NOTE: We want to leave the components lazy so that the checker+--         doesn't actualy need to produce the type components if they're+--         not needed.+data AnT a n+        = AnT+        { annotType     :: (Type  n)+        , annotTail     :: a }+        deriving (Show, Typeable)+++instance (NFData a, NFData n) => NFData (AnT a n) where+ rnf !an+        =     rnf (annotType    an)+        `seq` rnf (annotTail    an)+++instance Pretty (AnT a n) where+ ppr _ = text "AnT"        +++

@@ -0,0 +1,50 @@++module DDC.Core.Annot.AnTEC+        ( AnTEC (..)+        , fromAnT)+where+import DDC.Type.Compounds+import DDC.Type.Exp+import DDC.Base.Pretty+import Control.DeepSeq+import Data.Typeable+import DDC.Core.Annot.AnT       (AnT)+import qualified DDC.Core.Annot.AnT as AnT+++-- Annot ----------------------------------------------------------------------+-- | The type checker adds this annotation to every node in the AST, +--   giving its type, effect and closure.+---+--   NOTE: We want to leave the components lazy so that the checker+--         doesn't actualy need to produce the type components if they're+--         not needed.+data AnTEC a n+        = AnTEC+        { annotType     :: (Type    n)+        , annotEffect   :: (Effect  n)+        , annotClosure  :: (Closure n)+        , annotTail     :: a }+        deriving (Show, Typeable)+++-- | Promote an `AnT` to an `AnTEC` by filling in the effect and closure+--   portions with bottoms.+fromAnT :: AnT a n -> AnTEC a n+fromAnT (AnT.AnT t a)+   =    (AnTEC t (tBot kEffect) (tBot kClosure) a)+++instance (NFData a, NFData n) => NFData (AnTEC a n) where+ rnf !an+        =     rnf (annotType    an)+        `seq` rnf (annotEffect  an)+        `seq` rnf (annotClosure an)+        `seq` rnf (annotTail    an)+++instance Pretty (AnTEC a n) where+ ppr _ = text "AnTEC"        +++

@@ -4,7 +4,7 @@ where import DDC.Core.Check.Error import DDC.Core.Check.CheckWitness-import DDC.Core.DaCon+import DDC.Core.Exp.DaCon import DDC.Core.Exp import DDC.Type.Compounds import DDC.Type.DataDef

@@ -13,10 +13,12 @@ import DDC.Core.Collect import DDC.Core.Pretty import DDC.Core.Exp+import DDC.Core.Annot.AnTEC import DDC.Core.Check.Error import DDC.Core.Check.CheckDaCon import DDC.Core.Check.CheckWitness import DDC.Core.Check.TaggedClosure+import DDC.Core.Transform.Reannotate import DDC.Type.Transform.SubstituteT import DDC.Type.Transform.Crush import DDC.Type.Transform.Trim@@ -35,39 +37,8 @@ import DDC.Data.ListUtils import Data.List                        as L import Data.Maybe-import Data.Typeable-import Control.DeepSeq  --- Annot ------------------------------------------------------------------------- | The type checker adds this annotation to every node in the AST, ---   giving its type, effect and closure.-------   NOTE: We wwant to leave the components lazy so that the checker---         doesn't actualy need to produce the type components if they're---         not needed.-data AnTEC a n-        = AnTEC-        { annotType     :: (Type    n)-        , annotEffect   :: (Effect  n)-        , annotClosure  :: (Closure n)-        , annotTail     :: a }-        deriving (Show, Typeable)---instance (NFData a, NFData n) => NFData (AnTEC a n) where- rnf !an-        =     rnf (annotType    an)-        `seq` rnf (annotEffect  an)-        `seq` rnf (annotClosure an)-        `seq` rnf (annotTail    an)---instance Pretty (AnTEC a n) where- ppr _ = text "AnTEC"        --- -- Wrappers ------------------------------------------------------------------- -- | Type check an expression.  --@@ -87,7 +58,7 @@         :: (Ord n, Show n, Pretty n)         => Config n             -- ^ Static configuration.         -> KindEnv n            -- ^ Starting Kind environment.-        -> TypeEnv n            -- ^ Strating Type environment.+        -> TypeEnv n            -- ^ Starting Type environment.         -> Exp a n              -- ^ Expression to check.         -> Either (Error a n)                   ( Exp (AnTEC a n) n@@ -209,12 +180,16 @@ -- value-witness application. checkExpM' !config !kenv !tenv xx@(XApp a x1 (XWitness w2))  = do   (x1', t1, effs1, clos1) <- checkExpM     config kenv tenv x1-        t2                      <- checkWitnessM config kenv tenv w2++        (w2', t2) <- checkWitnessM config kenv tenv w2+        let w2TEC = reannotate fromAnT w2'++         case t1 of          TApp (TApp (TCon (TyConWitness TwConImpl)) t11) t12           | t11 `equivT` t2              -> returnX a-                (\z -> XApp z x1' (XWitness w2))+                (\z -> XApp z x1' (XWitness w2TEC))                 t12 effs1 clos1            | otherwise   -> throw $ ErrorAppMismatch xx t11 t2@@ -226,10 +201,22 @@  = do   (x1', t1, effs1, clos1)    <- checkExpM config kenv tenv x1         (x2', t2, effs2, clos2)    <- checkExpM config kenv tenv x2 -        -- Note: we don't need to use the closure of the function because-        --       all of its components will already be part of clos1 above.         case t1 of-         TApp (TApp (TApp (TApp (TCon (TyConSpec TcConFun)) t11) eff) _clo) t12+         -- Oblivious application of a pure function.+         -- Computation of the function and argument may themselves have+         -- an effect, but the function application does not.+         TApp (TApp (TCon (TyConSpec TcConFun)) t11) t12+          | t11 `equivT` t2+          -> returnX a+                (\z -> XApp z x1' x2')+                t12+                (effs1 `Sum.union` effs2)+                (clos1 `Set.union` clos2)++         -- Function with latent effect and closure.+         -- Note: we don't need to use the closure of the function because+         --       all of its components will already be part of clos1 above.+         TApp (TApp (TApp (TApp (TCon (TyConSpec TcConFunEC)) t11) eff) _clo) t12           | t11 `equivT` t2              , effs    <- Sum.fromList kEffect  [eff]           -> returnX a@@ -258,7 +245,7 @@          -- The body of a spec abstraction must be pure.         when (e2 /= Sum.empty kEffect)-         $ throw $ ErrorLamNotPure xx True (TSum e2)+         $ throw $ ErrorLamNotPure xx UniverseSpec (TSum e2)          -- The body of a spec abstraction must have data kind.         when (not $ isDataKind k2)@@ -322,26 +309,65 @@                  -- already already checked that.                  Just c2_captured -                  -- If we're suppressing closures then just drop them on the-                  -- floor. The consumer of this core program doesn't care.-                  | configSuppressClosures config+                  -- If we're not tracking closure information then just drop it +                  -- on the floor.+                  | not  $ configTrackedClosures config                   = Just $ tBot kClosure                    | otherwise                   = trimClosure $ closureOfTaggedSet c2_cut -             in  returnX a+                 -- If we're not tracking effect information then just drop it +                 -- on the floor.+                 e2_captured+                  | not  $ configTrackedEffects config+                  = tBot kEffect++                  | otherwise+                  = TSum e2++                 -- If the function type for the current fragment supports+                 -- latent effects and closures then just use that.+                 fun_result+                  | configFunctionalEffects  config+                  , configFunctionalClosures config+                  = returnX a                         (\z -> XLam z b1 x2')-                        (tFun t1 (TSum e2) c2_captured t2)+                        (tFunEC t1 e2_captured c2_captured t2)                         (Sum.empty kEffect)                         c2_cut +                 -- If the function type for the current fragment does not+                 -- support latent effects, then the body expression needs+                 -- to be pure.+                  | e2_captured == tBot kEffect+                  , c2_captured == tBot kClosure+                  = returnX a+                        (\z -> XLam z b1 x2')+                        (tFun t1 t2)+                        (Sum.empty kEffect)+                        Set.empty++                  | e2_captured /= tBot kEffect+                  = throw $ ErrorLamNotPure  xx UniverseData e2_captured++                  | c2_captured /= tBot kClosure+                  = throw $ ErrorLamNotEmpty xx UniverseData c2_captured++                  -- One of the above error cases is supposed to fire,+                  -- so we should never hit this error.+                  | otherwise+                  = error "checkExpM': can't build function type."++             in  fun_result++          -- This is a witness abstraction.          Just UniverseWitness            -- The body of a witness abstraction must be pure.           | e2 /= Sum.empty kEffect  -          -> throw $ ErrorLamNotPure  xx False (TSum e2)+          -> throw $ ErrorLamNotPure  xx UniverseWitness (TSum e2)            -- The body of a witness abstraction must produce data.           | not $ isDataKind k2      @@ -658,7 +684,9 @@ -- Purify an effect, given a witness that it is pure. checkExpM' !config !kenv !tenv xx@(XCast a (CastPurify w) x1)  = do-        tW                   <- checkWitnessM config kenv tenv w+        (w', tW)        <- checkWitnessM config kenv tenv w+        let wTEC        = reannotate fromAnT w'+         (x1', t1, effs, clo) <- checkExpM     config kenv tenv x1                          effs' <- case tW of@@ -666,7 +694,7 @@                     -> return $ Sum.delete effMask effs                   _ -> throw  $ ErrorWitnessNotPurity xx w tW -        let c'  = CastPurify w+        let c'  = CastPurify wTEC          returnX a                 (\z -> XCast z c' x1')@@ -676,9 +704,11 @@ -- Forget a closure, given a witness that it is empty. checkExpM' !config !kenv !tenv xx@(XCast a (CastForget w) x1)  = do   -        tW                    <- checkWitnessM config kenv tenv w-        (x1', t1, effs, clos) <- checkExpM     config kenv tenv x1+        (w', tW)      <- checkWitnessM config kenv tenv w        +        let wTEC      = reannotate fromAnT w' +        (x1', t1, effs, clos)  <- checkExpM     config kenv tenv x1+         clos' <- case tW of                   TApp (TCon (TyConWitness TwConEmpty)) cloMask                     -> return $ maskFromTaggedSet @@ -687,13 +717,44 @@                    _ -> throw $ ErrorWitnessNotEmpty xx w tW -        let c'  = CastForget w+        let c'  = CastForget wTEC          returnX a                 (\z -> XCast z c' x1')                 t1 effs clos'  +-- Suspend a computation,+-- capturing its effects in a computation type.+checkExpM' !config !kenv !tenv (XCast a CastSuspend x1)+ = do   +        (x1', t1, effs, clos) <- checkExpM config kenv tenv x1++        let tS  = tApps (TCon (TyConSpec TcConSusp))+                        [TSum effs, t1]++        returnX a+                (\z -> XCast z CastSuspend x1')+                tS (Sum.empty kEffect) clos+++-- Run a suspended computation,+-- releasing its effects into the environment.+checkExpM' !config !kenv !tenv xx@(XCast a CastRun x1)+ = do   +        (x1', t1, effs, clos) <- checkExpM config kenv tenv x1++        case t1 of+         TApp (TApp (TCon (TyConSpec TcConSusp)) eff2) tA +          -> returnX a+                (\z -> XCast z CastRun x1')+                tA +                (Sum.union effs (Sum.singleton kEffect eff2))+                clos++         _ -> throw $ ErrorRunNotSuspension xx t1++ -- Type and witness expressions can only appear as the arguments  -- to  applications. checkExpM' !_config !_kenv !_tenv xx@(XType _)@@ -702,8 +763,9 @@ checkExpM' !_config !_kenv !_tenv xx@(XWitness _)         = throw $ ErrorNakedWitness xx +-- This shouldn't happen. checkExpM' _ _ _ _-        = error "checkExpM: bogus warning killer"+        = error "checkExpM: can't check this expression"   -- | Like `checkExp` but we allow naked types and witnesses.@@ -727,8 +789,8 @@                         , clo)          XWitness w-         -> do  checkWitnessM config kenv tenv w-                return  ( XWitness w+         -> do  (w', _) <- checkWitnessM config kenv tenv w+                return  ( XWitness (reannotate fromAnT w')                         , Set.empty)          _ -> do@@ -760,6 +822,7 @@                 , t, es, cs) {-# INLINE returnX #-} + ------------------------------------------------------------------------------- -- | Check some let bindings. checkLetsM @@ -775,7 +838,7 @@                 , TypeSum n                 , Set (TaggedClosure n)) -checkLetsM !xx !config !kenv !tenv (LLet mode b11 x12)+checkLetsM !xx !config !kenv !tenv (LLet b11 x12)  = do            -- Check the right of the binding.         (x12', t12, effs12, clo12)  @@ -789,45 +852,7 @@         when (not $ isDataKind k11')          $ throw $ ErrorLetBindingNotData xx b11' k11'           -        -- Check purity and emptiness for lazy bindings.-        (case mode of-          LetStrict     -> return ()-          LetLazy _-           -> do let eff12' = TSum effs12-                 when (not $ isBot eff12')-                  $ throw $ ErrorLetLazyNotPure xx b11 eff12'--                 let clo12' = closureOfTaggedSet clo12-                 when (not $ isBot clo12')-                  $ throw $ ErrorLetLazyNotEmpty xx b11 clo12')--        -- Check region witness for lazy bindings.-        (case mode of-          LetStrict     -> return ()--          -- Type of lazy binding has no head region, like Unit and (->).-          LetLazy Nothing-           -> do case takeDataTyConApps t12 of-                  Just (_tc, t1 : _)-                   ->  do k1 <- checkTypeM config kenv t1-                          when (isRegionKind k1)-                           $ throw $ ErrorLetLazyNoWitness xx b11 t12--                  _ -> return ()--          -- Type of lazy binding might have a head region,-          -- so we need a Lazy witness for it.-          LetLazy (Just wit)-           -> do tWit        <- checkWitnessM config kenv tenv wit-                 let tWitExp =  case takeDataTyConApps t12 of-                                 Just (_tc, tR : _ts) -> tLazy tR-                                 _                    -> tHeadLazy t12--                 when (not $ equivT tWit tWitExp)-                  $ throw $ ErrorLetLazyWitnessTypeMismatch -                                 xx b11 tWit t12 tWitExp)-        -        return  ( LLet mode b11' x12'+        return  ( LLet b11' x12'                 , [b11']                 , effs12                 , clo12)

@@ -93,7 +93,7 @@  checkModuleBinds !ksExports !tsExports !xx  = case xx of-        XLet _ (LLet _ b _) x2     +        XLet _ (LLet b _) x2               -> do  checkModuleBind  ksExports tsExports b                 env     <- checkModuleBinds ksExports tsExports x2                 return  $ Env.extend b env@@ -153,7 +153,7 @@            -> CheckM a n (Kind n)  checkTypeM !config !kenv !tt- = case T.checkType (configPrimDataDefs config) kenv tt of+ = case T.checkType config kenv tt of         Left err        -> throw $ ErrorType err         Right k         -> return k 

@@ -14,10 +14,11 @@         , checkTypeM) where import DDC.Core.Exp+import DDC.Core.Annot.AnT import DDC.Core.Pretty import DDC.Core.Check.Error import DDC.Core.Check.ErrorMessage              ()-import DDC.Type.DataDef+import DDC.Type.Check                           (Config (..), configOfProfile) import DDC.Type.Transform.SubstituteT import DDC.Type.Compounds import DDC.Type.Universe@@ -28,7 +29,6 @@ import qualified DDC.Control.Monad.Check        as G import qualified DDC.Type.Env                   as Env import qualified DDC.Type.Check                 as T-import qualified DDC.Core.Fragment              as F   -- | Type checker monad. @@ -36,46 +36,6 @@ type CheckM a n   = G.CheckM (Error a n)  --- Config ------------------------------------------------------------------------ | Static configuration for the type checker.---   These fields don't change as we decend into the tree.------   The starting configuration should be converted from the profile that---   defines the language fragment you are checking. ---   See "DDC.Core.Fragment" and use `configOfProfile` below.-data Config n-        = Config-        { -- | Data type definitions.-          configPrimDataDefs            :: DataDefs n --          -- | Kinds of primitive types.-        , configPrimKinds               :: KindEnv n--          -- | Types of primitive operators.-        , configPrimTypes               :: TypeEnv n--          -- | Suppress all closure information, -          --   annotating all functions with an empty closure.-          --   -          --   This is used when checking the Disciple Core Salt fragment,-          --   as transforms in this language don't use the closure-          --   information.-        , configSuppressClosures        :: Bool }----- | Convert a langage profile to a type checker configuration.-configOfProfile :: F.Profile n -> Config n-configOfProfile profile-        = Config-        { configPrimDataDefs    = F.profilePrimDataDefs profile-        , configPrimKinds       = F.profilePrimKinds profile-        , configPrimTypes       = F.profilePrimTypes profile--        , configSuppressClosures      -                = F.featuresUntrackedClosures-                $ F.profileFeatures profile }-- -- Wrappers -------------------------------------------------------------------- -- | Check a witness. --   @@ -96,8 +56,10 @@         => Config n             -- ^ Static configuration.         -> KindEnv n            -- ^ Starting Kind Environment.         -> TypeEnv n            -- ^ Strating Type Environment.-        -> Witness n            -- ^ Witness to check.-        -> Either (Error a n) (Type n)+        -> Witness a n          -- ^ Witness to check.+        -> Either (Error a n) +                  ( Witness (AnT a n) n+                  , Type n)  checkWitness config kenv tenv xx         = result $ checkWitnessM config kenv tenv xx@@ -112,12 +74,13 @@ typeOfWitness          :: (Ord n, Show n, Pretty n)          => Config n-        -> Witness n +        -> Witness a n          -> Either (Error a n) (Type n)  typeOfWitness config ww -        = result -        $ checkWitnessM config Env.empty Env.empty ww+ = case checkWitness config Env.empty Env.empty ww of+        Left  err       -> Left err+        Right (_, t)    -> Right t   ------------------------------------------------------------------------------@@ -127,61 +90,75 @@         => Config n             -- ^ Data type definitions.         -> KindEnv n            -- ^ Kind environment.         -> TypeEnv n            -- ^ Type environment.-        -> Witness n            -- ^ Witness to check.-        -> CheckM a n (Type n)+        -> Witness a n          -- ^ Witness to check.+        -> CheckM a n +                ( Witness (AnT a n) n+                , Type n) -checkWitnessM !_config !_kenv !tenv (WVar u)+checkWitnessM !_config !_kenv !tenv (WVar a u)  = case Env.lookup u tenv of         Nothing -> throw $ ErrorUndefinedVar u UniverseWitness-        Just t  -> return t+        Just t  -> return ( WVar (AnT t a) u+                          , t) -checkWitnessM !_config !_kenv !_tenv (WCon wc)- = return $ typeOfWiCon wc+checkWitnessM !_config !_kenv !_tenv (WCon a wc)+ = let  t'       = typeOfWiCon wc+   in   return  ( WCon (AnT t' a) wc+                , t')    -- witness-type application-checkWitnessM !config !kenv !tenv ww@(WApp w1 (WType t2))- = do   t1      <- checkWitnessM  config kenv tenv w1-        k2      <- checkTypeM     config kenv t2+checkWitnessM !config !kenv !tenv ww@(WApp a1 w1 (WType a2 t2))+ = do   (w1', t1)       <- checkWitnessM  config kenv tenv w1+        k2              <- checkTypeM     config kenv t2         case t1 of          TForall b11 t12           |  typeOfBind b11 == k2-          -> return $ substituteT b11 t2 t12+          -> let t'     = substituteT b11 t2 t12+             in  return ( WApp (AnT t' a1) w1' (WType (AnT k2 a2) t2)+                        , t')            | otherwise   -> throw $ ErrorWAppMismatch ww (typeOfBind b11) k2          _              -> throw $ ErrorWAppNotCtor  ww t1 t2  -- witness-witness application-checkWitnessM !config !kenv !tenv ww@(WApp w1 w2)- = do   t1      <- checkWitnessM config kenv tenv w1-        t2      <- checkWitnessM config kenv tenv w2+checkWitnessM !config !kenv !tenv ww@(WApp a w1 w2)+ = do   (w1', t1)       <- checkWitnessM config kenv tenv w1+        (w2', t2)       <- checkWitnessM config kenv tenv w2         case t1 of          TApp (TApp (TCon (TyConWitness TwConImpl)) t11) t12           |  t11 == t2   -          -> return t12-+          -> return ( WApp (AnT t12 a) w1' w2'+                    , t12)+                     | otherwise   -> throw $ ErrorWAppMismatch ww t11 t2          _              -> throw $ ErrorWAppNotCtor  ww t1 t2  -- witness joining-checkWitnessM !config !kenv !tenv ww@(WJoin w1 w2)- = do   t1      <- checkWitnessM config kenv tenv w1-        t2      <- checkWitnessM config kenv tenv w2+checkWitnessM !config !kenv !tenv ww@(WJoin a w1 w2)+ = do   (w1', t1) <- checkWitnessM config kenv tenv w1+        (w2', t2) <- checkWitnessM config kenv tenv w2         case (t1, t2) of          (  TApp (TCon (TyConWitness TwConPure)) eff1           , TApp (TCon (TyConWitness TwConPure)) eff2)-          -> return $ TApp (TCon (TyConWitness TwConPure))-                           (TSum $ Sum.fromList kEffect  [eff1, eff2])+          -> let t'     = TApp (TCon (TyConWitness TwConPure))+                               (TSum $ Sum.fromList kEffect  [eff1, eff2])+             in  return ( WJoin (AnT t' a) w1' w2'+                        , t')           (  TApp (TCon (TyConWitness TwConEmpty)) clo1           , TApp (TCon (TyConWitness TwConEmpty)) clo2)-          -> return $ TApp (TCon (TyConWitness TwConEmpty))-                           (TSum $ Sum.fromList kClosure [clo1, clo2])+          -> let t'     = TApp (TCon (TyConWitness TwConEmpty))+                               (TSum $ Sum.fromList kClosure [clo1, clo2])+             in  return ( WJoin (AnT t' a) w1' w2'+                        , t')           _ -> throw $ ErrorCannotJoin ww w1 t1 w2 t2  -- embedded types-checkWitnessM !config !kenv !_tenv (WType t)- = checkTypeM config kenv t+checkWitnessM !config !kenv !_tenv (WType a t)+ = do   k       <- checkTypeM config kenv t+        return  ( WType (AnT k a) t+                , k)           -- | Take the type of a witness constructor.@@ -213,7 +190,7 @@         -> CheckM a n (Kind n)  checkTypeM config kenv tt- = case T.checkType (configPrimDataDefs config) kenv tt of+ = case T.checkType config kenv tt of         Left err        -> throw $ ErrorType err         Right k         -> return k 

@@ -83,12 +83,20 @@         { errorChecking         :: Exp a n          , errorBind             :: Bind n } -        -- | A type or witness abstraction where the body has a visible side effect.+        -- | An abstraction where the body has a visible side effect that +        --   is not supported by the current language fragment.         | ErrorLamNotPure         { errorChecking         :: Exp a n-        , errorSpecOrWit        :: Bool+        , errorUniverse         :: Universe         , errorEffect           :: Effect n } +        -- | An abstraction where the body has a visible closure that +        --   is not supported by the current language fragment.+        | ErrorLamNotEmpty+        { errorChecking         :: Exp a n+        , errorUniverse         :: Universe+        , errorClosure          :: Closure n }+         -- | A value function where the parameter does not have data kind.         | ErrorLamBindNotData         { errorChecking         :: Exp a n @@ -124,34 +132,6 @@         , errorKind             :: Kind n }  -        -- Let Lazy ----------------------------------------        -- | A lazy let binding that has a visible side effect.-        | ErrorLetLazyNotPure-        { errorChecking         :: Exp a n-        , errorBind             :: Bind n-        , errorEffect           :: Effect n }--        -- | A lazy let binding with a non-empty closure.-        | ErrorLetLazyNotEmpty-        { errorChecking         :: Exp a n-        , errorBind             :: Bind n-        , errorClosure          :: Closure n }--        -- | A lazy let binding without a witness that binding is in a lazy region.-        | ErrorLetLazyNoWitness-        { errorChecking         :: Exp a n-        , errorBind             :: Bind n-        , errorType             :: Type n }--        -- | A lazy let binding where the witness has the wrong type.-        | ErrorLetLazyWitnessTypeMismatch -        { errorChecking          :: Exp a n-        , errorBind              :: Bind n-        , errorWitnessTypeHave   :: Type n-        , errorBindType          :: Type n-        , errorWitnessTypeExpect :: Type n }--         -- Letrec -----------------------------------------         -- | A recursive let-expression where the right of the binding is not         --   a lambda abstraction.@@ -232,34 +212,34 @@         -- | A witness application where the argument type does not match         --   the parameter type.         | ErrorWAppMismatch-        { errorWitness          :: Witness n+        { errorWitness          :: Witness a n         , errorParamType        :: Type n         , errorArgType          :: Type n }          -- | Tried to perform a witness application with a non-witness.         | ErrorWAppNotCtor-        { errorWitness          :: Witness n+        { errorWitness          :: Witness a n         , errorNotFunType       :: Type n         , errorArgType          :: Type n }          -- | An invalid witness join.         | ErrorCannotJoin-        { errorWitness          :: Witness n-        , errorWitnessLeft      :: Witness n+        { errorWitness          :: Witness a n+        , errorWitnessLeft      :: Witness a n         , errorTypeLeft         :: Type n-        , errorWitnessRight     :: Witness n+        , errorWitnessRight     :: Witness a n         , errorTypeRight        :: Type n }          -- | A witness provided for a purify cast that does not witness purity.         | ErrorWitnessNotPurity         { errorChecking         :: Exp a n-        , errorWitness          :: Witness n+        , errorWitness          :: Witness a n         , errorType             :: Type n }          -- | A witness provided for a forget cast that does not witness emptiness.         | ErrorWitnessNotEmpty         { errorChecking         :: Exp a n-        , errorWitness          :: Witness n+        , errorWitness          :: Witness a n         , errorType             :: Type n }  @@ -337,6 +317,11 @@         { errorChecking         :: Exp a n         , errorEffect           :: Effect n         , errorKind             :: Kind n }++        -- | A run cast applied to a non-suspension.+        | ErrorRunNotSuspension+        { errorChecking         :: Exp a n+        , errorType             :: Type n }           -- Types ------------------------------------------

@@ -85,16 +85,20 @@                  , text "  is already in the environment."                  , text "with: "                        <> align (ppr xx) ] -        ErrorLamNotPure xx spec eff-         -> let universe' = if spec then text "spec"-                                    else text "witness"-            in vcat -                [ text "Impure" <+> universe' <+> text "abstraction"+        ErrorLamNotPure xx universe eff+         -> vcat +                [ text "Impure" <+> ppr universe <+> text "abstraction"                 , text "           has effect: "       <> ppr eff                 , empty                 , text "with: "                        <> align (ppr xx) ]++        ErrorLamNotEmpty xx universe eff+         -> vcat +                [ text "Non-empty" <+> ppr universe <+> text "abstraction"+                , text "           has closure: "       <> ppr eff+                , empty+                , text "with: "                        <> align (ppr xx) ]                  -                 ErrorLamBindNotData xx t1 k1          -> vcat [ text "Function parameter does not have data kind."                  , text "    The function parameter:"   <> ppr t1@@ -140,37 +144,6 @@                  , text "with: "                        <> align (ppr xx) ]  -        -- Let Lazy ----------------------------------------        ErrorLetLazyNotEmpty xx b clo-         -> vcat [ text "Lazy let binding is not empty."-                 , text "      The binding for: "       <> ppr (binderOfBind b)-                 , text "          has closure: "       <> ppr clo-                 , empty-                 , text "with: "                        <> align (ppr xx) ]--        ErrorLetLazyNotPure xx b eff-         -> vcat [ text "Lazy let binding is not pure."-                 , text "      The binding for: "       <> ppr (binderOfBind b)-                 , text "           has effect: "       <> ppr eff-                 , empty-                 , text "with: "                        <> align (ppr xx) ]--        ErrorLetLazyNoWitness xx b t-         -> vcat [ text "Lazy let binding has no witness but the bound value may have a head region."-                 , text "      The binding for: "       <> ppr (binderOfBind b)-                 , text "             Has type: "       <> ppr t-                 , empty-                 , text "with: "                        <> align (ppr xx) ]--        ErrorLetLazyWitnessTypeMismatch xx b tWitGot tBind tWitExp-         -> vcat [ text "Unexpected witness type in lazy let binding."-                 , text "          The binding for: "   <> ppr (binderOfBind b)-                 , text "    has a witness of type: "   <> ppr tWitGot-                 , text "           but is type is: "   <> ppr tBind-                 , text " so the witness should be: "   <> ppr tWitExp -                 , empty-                 , text "with: "                        <> align (ppr xx) ]-         -- Letrec -----------------------------------------         ErrorLetrecBindingNotLambda xx x          -> vcat [ text "Letrec can only bind lambda abstractions."@@ -373,6 +346,13 @@                  , empty                  , text "with: "                        <> align (ppr xx) ]        +        ErrorRunNotSuspension xx t+         -> vcat [ text "Expression to run is not a suspension."+                 , text "          Type: "              <> ppr t+                 , empty+                 , text "with: "                        <> align (ppr xx) ]++         -- Type -------------------------------------------         ErrorNakedType xx          -> vcat [ text "Found naked type in core program."

@@ -59,9 +59,8 @@         XLAM _ b x              -> [bindDefT BindLAM [b] [x]]         XLam _ b x              -> [bindDefX BindLam [b] [x]]       -        XLet _ (LLet m b x1) x2-         -> slurpBindTree m-         ++ slurpBindTree x1+        XLet _ (LLet b x1) x2+         -> slurpBindTree x1          ++ [bindDefX BindLet [b] [x2]]          XLet _ (LRec bxs) x2@@ -82,14 +81,6 @@         XWitness w      -> slurpBindTree w  -instance BindStruct LetMode where- slurpBindTree mode-  = case mode of-        LetStrict               -> []-        LetLazy Nothing         -> []-        LetLazy (Just ww)       -> slurpBindTree ww-- instance BindStruct (Cast a) where  slurpBindTree cc   = case cc of@@ -97,6 +88,8 @@         CastWeakenClosure xs    -> concatMap slurpBindTree xs         CastPurify w            -> slurpBindTree w         CastForget w            -> slurpBindTree w+        CastSuspend             -> []+        CastRun                 -> []   instance BindStruct (Alt a) where@@ -109,14 +102,14 @@          -> [bindDefX BindCasePat bs [x]]  -instance BindStruct Witness where+instance BindStruct (Witness a) where  slurpBindTree ww   = case ww of-        WVar u          -> [BindUse BoundWit u]+        WVar _ u        -> [BindUse BoundWit u]         WCon{}          -> []-        WApp  w1 w2     -> slurpBindTree w1 ++ slurpBindTree w2-        WJoin w1 w2     -> slurpBindTree w1 ++ slurpBindTree w2-        WType t         -> slurpBindTree t+        WApp  _ w1 w2   -> slurpBindTree w1 ++ slurpBindTree w2+        WJoin _ w1 w2   -> slurpBindTree w1 ++ slurpBindTree w2+        WType _ t       -> slurpBindTree t   -- | Helper for constructing the `BindTree` for an expression or witness binder.

@@ -137,25 +137,25 @@             in  support kenv tenv' x  -instance SupportX Witness where+instance SupportX (Witness a) where  support kenv tenv ww   = case ww of-        WVar u+        WVar _ u          | Env.member u tenv    -> mempty          | otherwise            -> mempty { supportWiVar = Set.singleton u }          WCon{}          -> mempty -        WApp w1 w2+        WApp _ w1 w2          -> support kenv tenv w1          <> support kenv tenv w2 -        WJoin w1 w2+        WJoin _ w1 w2          -> support kenv tenv w1          <> support kenv tenv w2 -        WType t+        WType _ t          -> support kenv tenv t  @@ -173,14 +173,19 @@          CastForget w          -> support kenv tenv w++        CastSuspend+         -> mempty++        CastRun+         -> mempty            instance SupportX (Lets a) where  support kenv tenv lts   = case lts of-        LLet m b x-         -> support kenv tenv m-         <> support kenv tenv b+        LLet b x+         -> support kenv tenv b          <> support kenv (Env.extend b tenv) x          LRec bxs@@ -196,13 +201,4 @@         LWithRegion u          | Env.member u kenv    -> mempty          | otherwise            -> mempty { supportSpVar = Set.singleton u }---instance SupportX LetMode where- support kenv tenv mm-  = case mm of-        LetStrict               -> mempty-        LetLazy Nothing         -> mempty-        LetLazy (Just w)        -> support kenv tenv w- 

@@ -1,332 +1,7 @@  -- | Utilities for constructing and destructing compound expressions. module DDC.Core.Compounds -        ( module DDC.Type.Compounds-        , module DDC.Core.DaCon--          -- * Annotations-        , takeAnnotOfExp--          -- * Lambdas-        , xLAMs-        , xLams-        , makeXLamFlags-        , takeXLAMs-        , takeXLams-        , takeXLamFlags--          -- * Applications-        , xApps-        , makeXAppsWithAnnots-        , takeXApps-        , takeXApps1-        , takeXAppsAsList-        , takeXAppsWithAnnots-        , takeXConApps-        , takeXPrimApps--          -- * Lets-        , xLets-        , splitXLets -        , bindsOfLets-        , specBindsOfLets-        , valwitBindsOfLets--          -- * Patterns-        , bindsOfPat--          -- * Alternatives-        , takeCtorNameOfAlt--          -- * Witnesses-        , wApp-        , wApps-        , takeXWitness-        , takeWAppsAsList-        , takePrimWiConApps--          -- * Types-        , takeXType--          -- * Units-        , xUnit)+        ( module DDC.Core.Compounds.Annot ) where-import DDC.Type.Compounds-import DDC.Core.Exp-import DDC.Core.DaCon----- Annotations ------------------------------------------------------------------- | Take the outermost annotation from an expression,---   or Nothing if this is an `XType` or `XWitness` without an annotation.-takeAnnotOfExp :: Exp a n -> Maybe a-takeAnnotOfExp xx- = case xx of-        XVar  a _       -> Just a-        XCon  a _       -> Just a-        XLAM  a _ _     -> Just a-        XLam  a _ _     -> Just a-        XApp  a _ _     -> Just a-        XLet  a _ _     -> Just a-        XCase a _ _     -> Just a-        XCast a _ _     -> Just a-        XType{}         -> Nothing-        XWitness{}      -> Nothing----- Lambdas ------------------------------------------------------------------------ | Make some nested type lambdas.-xLAMs :: a -> [Bind n] -> Exp a n -> Exp a n-xLAMs a bs x-        = foldr (XLAM a) x (reverse bs)----- | Make some nested value or witness lambdas.-xLams :: a -> [Bind n] -> Exp a n -> Exp a n-xLams a bs x-        = foldr (XLam a) x (reverse bs)----- | Split type lambdas from the front of an expression,---   or `Nothing` if there aren't any.-takeXLAMs :: Exp a n -> Maybe ([Bind n], Exp a n)-takeXLAMs xx- = let  go bs (XLAM _ b x) = go (b:bs) x-        go bs x            = (reverse bs, x)-   in   case go [] xx of-         ([], _)        -> Nothing-         (bs, body)     -> Just (bs, body)----- | Split nested value or witness lambdas from the front of an expression,---   or `Nothing` if there aren't any.-takeXLams :: Exp a n -> Maybe ([Bind n], Exp a n)-takeXLams xx- = let  go bs (XLam _ b x) = go (b:bs) x-        go bs x            = (reverse bs, x)-   in   case go [] xx of-         ([], _)        -> Nothing-         (bs, body)     -> Just (bs, body)----- | Make some nested lambda abstractions,---   using a flag to indicate whether the lambda is a---   level-1 (True), or level-0 (False) binder.-makeXLamFlags :: a -> [(Bool, Bind n)] -> Exp a n -> Exp a n-makeXLamFlags a fbs x- = foldr (\(f, b) x'-           -> if f then XLAM a b x'-                   else XLam a b x')-                x fbs----- | Split nested lambdas from the front of an expression, ---   with a flag indicating whether the lambda was a level-1 (True), ---   or level-0 (False) binder.-takeXLamFlags :: Exp a n -> Maybe ([(Bool, Bind n)], Exp a n)-takeXLamFlags xx- = let  go bs (XLAM _ b x) = go ((True,  b):bs) x-        go bs (XLam _ b x) = go ((False, b):bs) x-        go bs x            = (reverse bs, x)-   in   case go [] xx of-         ([], _)        -> Nothing-         (bs, body)     -> Just (bs, body)----- Applications ------------------------------------------------------------------ | Build sequence of value applications.-xApps   :: a -> Exp a n -> [Exp a n] -> Exp a n-xApps a t1 ts     = foldl (XApp a) t1 ts----- | Build sequence of applications.---   Similar to `xApps` but also takes list of annotations for ---   the `XApp` constructors.-makeXAppsWithAnnots :: Exp a n -> [(Exp a n, a)] -> Exp a n-makeXAppsWithAnnots f xas- = case xas of-        []              -> f-        (arg,a ) : as   -> makeXAppsWithAnnots (XApp a f arg) as----- | Flatten an application into the function part and its arguments.------   Returns `Nothing` if there is no outer application.-takeXApps :: Exp a n -> Maybe (Exp a n, [Exp a n])-takeXApps xx- = case takeXAppsAsList xx of-        (x1 : xsArgs)   -> Just (x1, xsArgs)-        _               -> Nothing----- | Flatten an application into the function part and its arguments.------   This is like `takeXApps` above, except we know there is at least one argument.-takeXApps1 :: Exp a n -> Exp a n -> (Exp a n, [Exp a n])-takeXApps1 x1 x2- = case takeXApps x1 of-        Nothing          -> (x1,  [x2])-        Just (x11, x12s) -> (x11, x12s ++ [x2])----- | Flatten an application into the function parts and arguments, if any.-takeXAppsAsList  :: Exp a n -> [Exp a n]-takeXAppsAsList xx- = case xx of-        XApp _ x1 x2    -> takeXAppsAsList x1 ++ [x2]-        _               -> [xx]----- | Destruct sequence of applications.---   Similar to `takeXAppsAsList` but also keeps annotations for later.-takeXAppsWithAnnots :: Exp a n -> (Exp a n, [(Exp a n, a)])-takeXAppsWithAnnots xx- = case xx of-        XApp a f arg-         -> let (f', args') = takeXAppsWithAnnots f-            in  (f', args' ++ [(arg,a)])--        _ -> (xx, [])----- | Flatten an application of a primop into the variable---   and its arguments.---   ---   Returns `Nothing` if the expression isn't a primop application.-takeXPrimApps :: Exp a n -> Maybe (n, [Exp a n])-takeXPrimApps xx- = case takeXAppsAsList xx of-        XVar _ (UPrim p _) : xs -> Just (p, xs)-        _                       -> Nothing---- | Flatten an application of a data constructor into the constructor---   and its arguments. ------   Returns `Nothing` if the expression isn't a constructor application.-takeXConApps :: Exp a n -> Maybe (DaCon n, [Exp a n])-takeXConApps xx- = case takeXAppsAsList xx of-        XCon _ dc : xs  -> Just (dc, xs)-        _               -> Nothing----- Lets -------------------------------------------------------------------------- | Wrap some let-bindings around an expression.-xLets :: a -> [Lets a n] -> Exp a n -> Exp a n-xLets a lts x- = foldr (XLet a) x lts----- | Split let-bindings from the front of an expression, if any.-splitXLets :: Exp a n -> ([Lets a n], Exp a n)-splitXLets xx- = case xx of-        XLet _ lts x -         -> let (lts', x')      = splitXLets x-            in  (lts : lts', x')--        _ -> ([], xx)---- | Take the binds of a `Lets`.------   The level-1 and level-0 binders are returned separately.-bindsOfLets :: Lets a n -> ([Bind n], [Bind n])-bindsOfLets ll- = case ll of-        LLet _ b _         -> ([],  [b])-        LRec bxs           -> ([],  map fst bxs)-        LLetRegions bs bbs -> (bs, bbs)-        LWithRegion{}      -> ([],  [])----- | Like `bindsOfLets` but only take the spec (level-1) binders.-specBindsOfLets :: Lets a n -> [Bind n]-specBindsOfLets ll- = case ll of-        LLet _ _ _       -> []-        LRec _           -> []-        LLetRegions bs _ -> bs-        LWithRegion{}    -> []----- | Like `bindsOfLets` but only take the value and witness (level-0) binders.-valwitBindsOfLets :: Lets a n -> [Bind n]-valwitBindsOfLets ll- = case ll of-        LLet _ b _       -> [b]-        LRec bxs         -> map fst bxs-        LLetRegions _ bs -> bs-        LWithRegion{}    -> []----- Alternatives ------------------------------------------------------------------ | Take the constructor name of an alternative, if there is one.-takeCtorNameOfAlt :: Alt a n -> Maybe n-takeCtorNameOfAlt aa- = case aa of-        AAlt (PData dc _) _     -> takeNameOfDaCon dc-        _                       -> Nothing----- Patterns ---------------------------------------------------------------------- | Take the binds of a `Pat`.-bindsOfPat :: Pat n -> [Bind n]-bindsOfPat pp- = case pp of-        PDefault          -> []-        PData _ bs        -> bs----- Witnesses --------------------------------------------------------------------- | Construct a witness application-wApp :: Witness n -> Witness n -> Witness n-wApp = WApp----- | Construct a sequence of witness applications-wApps :: Witness n -> [Witness n] -> Witness n-wApps = foldl wApp----- | Take the witness from an `XWitness` argument, if any.-takeXWitness :: Exp a n -> Maybe (Witness n)-takeXWitness xx- = case xx of-        XWitness t -> Just t-        _          -> Nothing----- | Flatten an application into the function parts and arguments, if any.-takeWAppsAsList :: Witness n -> [Witness n]-takeWAppsAsList ww- = case ww of-        WApp w1 w2 -> takeWAppsAsList w1 ++ [w2]-        _          -> [ww]----- | Flatten an application of a witness into the witness constructor---   name and its arguments.------   Returns nothing if there is no witness constructor in head position.-takePrimWiConApps :: Witness n -> Maybe (n, [Witness n])-takePrimWiConApps ww- = case takeWAppsAsList ww of-        WCon wc : args | WiConBound (UPrim n _) _ <- wc-          -> Just (n, args)-        _ -> Nothing----- Types ------------------------------------------------------------------------- | Take the type from an `XType` argument, if any.-takeXType :: Exp a n -> Maybe (Type n)-takeXType xx- = case xx of-        XType t -> Just t-        _       -> Nothing----- Units -------------------------------------------------------------------------- | Construct a value of unit type.-xUnit   :: a -> Exp a n-xUnit a = XCon a dcUnit+import DDC.Core.Compounds.Annot 

@@ -0,0 +1,342 @@++-- | Utilities for constructing and destructing compound expressions.+--+--   For the annotated version of the AST.+module DDC.Core.Compounds.Annot+        ( module DDC.Type.Compounds++          -- * Annotations+        , takeAnnotOfExp++          -- * Lambdas+        , xLAMs+        , xLams+        , makeXLamFlags+        , takeXLAMs+        , takeXLams+        , takeXLamFlags++          -- * Applications+        , xApps+        , makeXAppsWithAnnots+        , takeXApps+        , takeXApps1+        , takeXAppsAsList+        , takeXAppsWithAnnots+        , takeXConApps+        , takeXPrimApps++          -- * Lets+        , xLets,               xLetsAnnot+        , splitXLets +        , bindsOfLets+        , specBindsOfLets+        , valwitBindsOfLets++          -- * Patterns+        , bindsOfPat++          -- * Alternatives+        , takeCtorNameOfAlt++          -- * Witnesses+        , wApp+        , wApps+        , takeXWitness+        , takeWAppsAsList+        , takePrimWiConApps++          -- * Types+        , takeXType++          -- * Data Constructors+        , xUnit, dcUnit+        , mkDaConAlg+        , mkDaConSolid+        , takeNameOfDaCon+        , typeOfDaCon)+where+import DDC.Type.Compounds+import DDC.Core.Exp+import DDC.Core.Exp.DaCon+++-- Annotations ----------------------------------------------------------------+-- | Take the outermost annotation from an expression,+--   or Nothing if this is an `XType` or `XWitness` without an annotation.+takeAnnotOfExp :: Exp a n -> Maybe a+takeAnnotOfExp xx+ = case xx of+        XVar  a _       -> Just a+        XCon  a _       -> Just a+        XLAM  a _ _     -> Just a+        XLam  a _ _     -> Just a+        XApp  a _ _     -> Just a+        XLet  a _ _     -> Just a+        XCase a _ _     -> Just a+        XCast a _ _     -> Just a+        XType{}         -> Nothing+        XWitness{}      -> Nothing+++-- Lambdas ---------------------------------------------------------------------+-- | Make some nested type lambdas.+xLAMs :: a -> [Bind n] -> Exp a n -> Exp a n+xLAMs a bs x+        = foldr (XLAM a) x bs+++-- | Make some nested value or witness lambdas.+xLams :: a -> [Bind n] -> Exp a n -> Exp a n+xLams a bs x+        = foldr (XLam a) x bs+++-- | Split type lambdas from the front of an expression,+--   or `Nothing` if there aren't any.+takeXLAMs :: Exp a n -> Maybe ([Bind n], Exp a n)+takeXLAMs xx+ = let  go bs (XLAM _ b x) = go (b:bs) x+        go bs x            = (reverse bs, x)+   in   case go [] xx of+         ([], _)        -> Nothing+         (bs, body)     -> Just (bs, body)+++-- | Split nested value or witness lambdas from the front of an expression,+--   or `Nothing` if there aren't any.+takeXLams :: Exp a n -> Maybe ([Bind n], Exp a n)+takeXLams xx+ = let  go bs (XLam _ b x) = go (b:bs) x+        go bs x            = (reverse bs, x)+   in   case go [] xx of+         ([], _)        -> Nothing+         (bs, body)     -> Just (bs, body)+++-- | Make some nested lambda abstractions,+--   using a flag to indicate whether the lambda is a+--   level-1 (True), or level-0 (False) binder.+makeXLamFlags :: a -> [(Bool, Bind n)] -> Exp a n -> Exp a n+makeXLamFlags a fbs x+ = foldr (\(f, b) x'+           -> if f then XLAM a b x'+                   else XLam a b x')+                x fbs+++-- | Split nested lambdas from the front of an expression, +--   with a flag indicating whether the lambda was a level-1 (True), +--   or level-0 (False) binder.+takeXLamFlags :: Exp a n -> Maybe ([(Bool, Bind n)], Exp a n)+takeXLamFlags xx+ = let  go bs (XLAM _ b x) = go ((True,  b):bs) x+        go bs (XLam _ b x) = go ((False, b):bs) x+        go bs x            = (reverse bs, x)+   in   case go [] xx of+         ([], _)        -> Nothing+         (bs, body)     -> Just (bs, body)+++-- Applications ---------------------------------------------------------------+-- | Build sequence of value applications.+xApps   :: a -> Exp a n -> [Exp a n] -> Exp a n+xApps a t1 ts     = foldl (XApp a) t1 ts+++-- | Build sequence of applications.+--   Similar to `xApps` but also takes list of annotations for +--   the `XApp` constructors.+makeXAppsWithAnnots :: Exp a n -> [(Exp a n, a)] -> Exp a n+makeXAppsWithAnnots f xas+ = case xas of+        []              -> f+        (arg,a ) : as   -> makeXAppsWithAnnots (XApp a f arg) as+++-- | Flatten an application into the function part and its arguments.+--+--   Returns `Nothing` if there is no outer application.+takeXApps :: Exp a n -> Maybe (Exp a n, [Exp a n])+takeXApps xx+ = case takeXAppsAsList xx of+        (x1 : xsArgs)   -> Just (x1, xsArgs)+        _               -> Nothing+++-- | Flatten an application into the function part and its arguments.+--+--   This is like `takeXApps` above, except we know there is at least one argument.+takeXApps1 :: Exp a n -> Exp a n -> (Exp a n, [Exp a n])+takeXApps1 x1 x2+ = case takeXApps x1 of+        Nothing          -> (x1,  [x2])+        Just (x11, x12s) -> (x11, x12s ++ [x2])+++-- | Flatten an application into the function parts and arguments, if any.+takeXAppsAsList  :: Exp a n -> [Exp a n]+takeXAppsAsList xx+ = case xx of+        XApp _ x1 x2    -> takeXAppsAsList x1 ++ [x2]+        _               -> [xx]+++-- | Destruct sequence of applications.+--   Similar to `takeXAppsAsList` but also keeps annotations for later.+takeXAppsWithAnnots :: Exp a n -> (Exp a n, [(Exp a n, a)])+takeXAppsWithAnnots xx+ = case xx of+        XApp a f arg+         -> let (f', args') = takeXAppsWithAnnots f+            in  (f', args' ++ [(arg,a)])++        _ -> (xx, [])+++-- | Flatten an application of a primop into the variable+--   and its arguments.+--   +--   Returns `Nothing` if the expression isn't a primop application.+takeXPrimApps :: Exp a n -> Maybe (n, [Exp a n])+takeXPrimApps xx+ = case takeXAppsAsList xx of+        XVar _ (UPrim p _) : xs -> Just (p, xs)+        _                       -> Nothing++-- | Flatten an application of a data constructor into the constructor+--   and its arguments. +--+--   Returns `Nothing` if the expression isn't a constructor application.+takeXConApps :: Exp a n -> Maybe (DaCon n, [Exp a n])+takeXConApps xx+ = case takeXAppsAsList xx of+        XCon _ dc : xs  -> Just (dc, xs)+        _               -> Nothing+++-- Lets -----------------------------------------------------------------------+-- | Wrap some let-bindings around an expression.+xLets :: a -> [Lets a n] -> Exp a n -> Exp a n+xLets a lts x+ = foldr (XLet a) x lts+++-- | Wrap some let-bindings around an expression, with individual annotations.+xLetsAnnot :: [(Lets a n, a)] -> Exp a n -> Exp a n+xLetsAnnot lts x+ = foldr (\(l, a) x' -> XLet a l x') x lts+++-- | Split let-bindings from the front of an expression, if any.+splitXLets :: Exp a n -> ([Lets a n], Exp a n)+splitXLets xx+ = case xx of+        XLet _ lts x +         -> let (lts', x')      = splitXLets x+            in  (lts : lts', x')++        _ -> ([], xx)++-- | Take the binds of a `Lets`.+--+--   The level-1 and level-0 binders are returned separately.+bindsOfLets :: Lets a n -> ([Bind n], [Bind n])+bindsOfLets ll+ = case ll of+        LLet b _           -> ([],  [b])+        LRec bxs           -> ([],  map fst bxs)+        LLetRegions bs bbs -> (bs, bbs)+        LWithRegion{}      -> ([],  [])+++-- | Like `bindsOfLets` but only take the spec (level-1) binders.+specBindsOfLets :: Lets a n -> [Bind n]+specBindsOfLets ll+ = case ll of+        LLet _ _         -> []+        LRec _           -> []+        LLetRegions bs _ -> bs+        LWithRegion{}    -> []+++-- | Like `bindsOfLets` but only take the value and witness (level-0) binders.+valwitBindsOfLets :: Lets a n -> [Bind n]+valwitBindsOfLets ll+ = case ll of+        LLet b _         -> [b]+        LRec bxs         -> map fst bxs+        LLetRegions _ bs -> bs+        LWithRegion{}    -> []+++-- Alternatives ---------------------------------------------------------------+-- | Take the constructor name of an alternative, if there is one.+takeCtorNameOfAlt :: Alt a n -> Maybe n+takeCtorNameOfAlt aa+ = case aa of+        AAlt (PData dc _) _     -> takeNameOfDaCon dc+        _                       -> Nothing+++-- Patterns -------------------------------------------------------------------+-- | Take the binds of a `Pat`.+bindsOfPat :: Pat n -> [Bind n]+bindsOfPat pp+ = case pp of+        PDefault          -> []+        PData _ bs        -> bs+++-- Witnesses ------------------------------------------------------------------+-- | Construct a witness application+wApp :: a -> Witness a n -> Witness a n -> Witness a n+wApp = WApp+++-- | Construct a sequence of witness applications+wApps :: a -> Witness a n -> [Witness a n] -> Witness a n+wApps a = foldl (wApp a)+++-- | Take the witness from an `XWitness` argument, if any.+takeXWitness :: Exp a n -> Maybe (Witness a n)+takeXWitness xx+ = case xx of+        XWitness t -> Just t+        _          -> Nothing+++-- | Flatten an application into the function parts and arguments, if any.+takeWAppsAsList :: Witness a n -> [Witness a n]+takeWAppsAsList ww+ = case ww of+        WApp _ w1 w2 -> takeWAppsAsList w1 ++ [w2]+        _          -> [ww]+++-- | Flatten an application of a witness into the witness constructor+--   name and its arguments.+--+--   Returns nothing if there is no witness constructor in head position.+takePrimWiConApps :: Witness a n -> Maybe (n, [Witness a n])+takePrimWiConApps ww+ = case takeWAppsAsList ww of+        WCon _ wc : args | WiConBound (UPrim n _) _ <- wc+          -> Just (n, args)+        _ -> Nothing+++-- Types ----------------------------------------------------------------------+-- | Take the type from an `XType` argument, if any.+takeXType :: Exp a n -> Maybe (Type n)+takeXType xx+ = case xx of+        XType t -> Just t+        _       -> Nothing+++-- Units -----------------------------------------------------------------------+-- | Construct a value of unit type.+xUnit   :: a -> Exp a n+xUnit a = XCon a dcUnit

@@ -0,0 +1,293 @@++-- | Utilities for constructing and destructing compound expressions.+--+--   For the Simple version of the AST.+module DDC.Core.Compounds.Simple+        ( module DDC.Type.Compounds++          -- * Lambdas+        , xLAMs+        , xLams+        , makeXLamFlags+        , takeXLAMs+        , takeXLams+        , takeXLamFlags++          -- * Applications+        , xApps+        , takeXApps+        , takeXApps1+        , takeXAppsAsList+        , takeXConApps+        , takeXPrimApps++          -- * Lets+        , xLets+        , splitXLets +        , bindsOfLets+        , specBindsOfLets+        , valwitBindsOfLets++          -- * Patterns+        , bindsOfPat++          -- * Alternatives+        , takeCtorNameOfAlt++          -- * Witnesses+        , wApp+        , wApps+        , takeXWitness+        , takeWAppsAsList+        , takePrimWiConApps++          -- * Types+        , takeXType++          -- * Data Constructors+        , xUnit, dcUnit+        , mkDaConAlg+        , mkDaConSolid+        , takeNameOfDaCon+        , typeOfDaCon)+where+import DDC.Type.Exp+import DDC.Core.Exp.Simple+import DDC.Core.Exp.DaCon+import DDC.Type.Compounds+++-- Lambdas ---------------------------------------------------------------------+-- | Make some nested type lambdas.+xLAMs :: [Bind n] -> Exp a n -> Exp a n+xLAMs bs x+        = foldr XLAM x bs+++-- | Make some nested value or witness lambdas.+xLams :: [Bind n] -> Exp a n -> Exp a n+xLams bs x+        = foldr XLam x bs+++-- | Split type lambdas from the front of an expression,+--   or `Nothing` if there aren't any.+takeXLAMs :: Exp a n -> Maybe ([Bind n], Exp a n)+takeXLAMs xx+ = let  go bs (XLAM b x) = go (b:bs) x+        go bs x            = (reverse bs, x)+   in   case go [] xx of+         ([], _)        -> Nothing+         (bs, body)     -> Just (bs, body)+++-- | Split nested value or witness lambdas from the front of an expression,+--   or `Nothing` if there aren't any.+takeXLams :: Exp a n -> Maybe ([Bind n], Exp a n)+takeXLams xx+ = let  go bs (XLam b x) = go (b:bs) x+        go bs x          = (reverse bs, x)+   in   case go [] xx of+         ([], _)        -> Nothing+         (bs, body)     -> Just (bs, body)+++-- | Make some nested lambda abstractions,+--   using a flag to indicate whether the lambda is a+--   level-1 (True), or level-0 (False) binder.+makeXLamFlags :: [(Bool, Bind n)] -> Exp a n -> Exp a n+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 :: Exp a n -> Maybe ([(Bool, Bind n)], Exp a n)+takeXLamFlags xx+ = let  go bs (XLAM b x)  = go ((True,  b):bs) x+        go bs (XLam b x)  = go ((False, b):bs) x+        go bs x           = (reverse bs, x)+   in   case go [] xx of+         ([], _)        -> Nothing+         (bs, body)     -> Just (bs, body)+++-- Applications ---------------------------------------------------------------+-- | Build sequence of value applications.+xApps   :: Exp a n -> [Exp a n] -> Exp a n+xApps t1 ts     = foldl XApp t1 ts+++-- | Flatten an application into the function part and its arguments.+--+--   Returns `Nothing` if there is no outer application.+takeXApps :: Exp a n -> Maybe (Exp a n, [Exp a n])+takeXApps xx+ = case takeXAppsAsList xx of+        (x1 : xsArgs)   -> Just (x1, xsArgs)+        _               -> Nothing+++-- | Flatten an application into the function part and its arguments.+--+--   This is like `takeXApps` above, except we know there is at least one argument.+takeXApps1 :: Exp a n -> Exp a n -> (Exp a n, [Exp a n])+takeXApps1 x1 x2+ = case takeXApps x1 of+        Nothing          -> (x1,  [x2])+        Just (x11, x12s) -> (x11, x12s ++ [x2])+++-- | Flatten an application into the function parts and arguments, if any.+takeXAppsAsList  :: Exp a n -> [Exp a n]+takeXAppsAsList xx+ = case xx of+        XApp x1 x2      -> takeXAppsAsList x1 ++ [x2]+        _               -> [xx]+++-- | Flatten an application of a primop into the variable+--   and its arguments.+--   +--   Returns `Nothing` if the expression isn't a primop application.+takeXPrimApps :: Exp a n -> Maybe (n, [Exp a n])+takeXPrimApps xx+ = case takeXAppsAsList xx of+        XVar (UPrim p _) : xs -> Just (p, xs)+        _                     -> Nothing++-- | Flatten an application of a data constructor into the constructor+--   and its arguments. +--+--   Returns `Nothing` if the expression isn't a constructor application.+takeXConApps :: Exp a n -> Maybe (DaCon n, [Exp a n])+takeXConApps xx+ = case takeXAppsAsList xx of+        XCon dc : xs  -> Just (dc, xs)+        _             -> Nothing+++-- Lets -----------------------------------------------------------------------+-- | Wrap some let-bindings around an expression.+xLets :: [Lets a n] -> Exp a n -> Exp a n+xLets lts x+ = foldr XLet x lts+++-- | Split let-bindings from the front of an expression, if any.+splitXLets :: Exp a n -> ([Lets a n], Exp a n)+splitXLets xx+ = case xx of+        XLet lts x +         -> let (lts', x')      = splitXLets x+            in  (lts : lts', x')++        _ -> ([], xx)+++-- | Take the binds of a `Lets`.+--+--   The level-1 and level-0 binders are returned separately.+bindsOfLets :: Lets a n -> ([Bind n], [Bind n])+bindsOfLets ll+ = case ll of+        LLet b _           -> ([],  [b])+        LRec bxs           -> ([],  map fst bxs)+        LLetRegions bs bbs -> (bs, bbs)+        LWithRegion{}      -> ([],  [])+++-- | Like `bindsOfLets` but only take the spec (level-1) binders.+specBindsOfLets :: Lets a n -> [Bind n]+specBindsOfLets ll+ = case ll of+        LLet _ _         -> []+        LRec _           -> []+        LLetRegions bs _ -> bs+        LWithRegion{}    -> []+++-- | Like `bindsOfLets` but only take the value and witness (level-0) binders.+valwitBindsOfLets :: Lets a n -> [Bind n]+valwitBindsOfLets ll+ = case ll of+        LLet b _         -> [b]+        LRec bxs         -> map fst bxs+        LLetRegions _ bs -> bs+        LWithRegion{}    -> []+++-- Alternatives ---------------------------------------------------------------+-- | Take the constructor name of an alternative, if there is one.+takeCtorNameOfAlt :: Alt a n -> Maybe n+takeCtorNameOfAlt aa+ = case aa of+        AAlt (PData dc _) _     -> takeNameOfDaCon dc+        _                       -> Nothing+++-- Patterns -------------------------------------------------------------------+-- | Take the binds of a `Pat`.+bindsOfPat :: Pat n -> [Bind n]+bindsOfPat pp+ = case pp of+        PDefault          -> []+        PData _ bs        -> bs+++-- Witnesses ------------------------------------------------------------------+-- | Construct a witness application+wApp :: Witness a n -> Witness a n -> Witness a n+wApp = WApp+++-- | Construct a sequence of witness applications+wApps :: Witness a n -> [Witness a n] -> Witness a n+wApps = foldl wApp+++-- | Take the witness from an `XWitness` argument, if any.+takeXWitness :: Exp a n -> Maybe (Witness a n)+takeXWitness xx+ = case xx of+        XWitness t -> Just t+        _          -> Nothing+++-- | Flatten an application into the function parts and arguments, if any.+takeWAppsAsList :: Witness a n -> [Witness a n]+takeWAppsAsList ww+ = case ww of+        WApp w1 w2 -> takeWAppsAsList w1 ++ [w2]+        _          -> [ww]+++-- | Flatten an application of a witness into the witness constructor+--   name and its arguments.+--+--   Returns nothing if there is no witness constructor in head position.+takePrimWiConApps :: Witness a n -> Maybe (n, [Witness a n])+takePrimWiConApps ww+ = case takeWAppsAsList ww of+        WCon wc : args | WiConBound (UPrim n _) _ <- wc+          -> Just (n, args)+        _ -> Nothing+++-- Types ----------------------------------------------------------------------+-- | Take the type from an `XType` argument, if any.+takeXType :: Exp a n -> Maybe (Type n)+takeXType xx+ = case xx of+        XType t -> Just t+        _       -> Nothing+++-- Units -----------------------------------------------------------------------+-- | Construct a value of unit type.+xUnit   :: Exp a n+xUnit = XCon dcUnit

@@ -1,100 +0,0 @@--module DDC.Core.DaCon -        ( DaCon         (..)-        , DaConName     (..)--        , dcUnit-        , mkDaConAlg-        , mkDaConSolid-        , takeNameOfDaCon-        , typeOfDaCon)-where-import DDC.Type.Compounds-import DDC.Type.Exp-import Control.DeepSeq------------------------------------------------------------------------------------- | Data constructor names.-data DaConName n-        -- | The unit data constructor is builtin.-        = DaConUnit--        -- | Data constructor name defined by the client.-        | DaConNamed n-        deriving (Eq, Show)---instance NFData n => NFData (DaConName n) where- rnf dcn-  = case dcn of-        DaConUnit       -> ()-        DaConNamed n    -> rnf n------------------------------------------------------------------------------------- | Data constructors.-data DaCon n-        = DaCon-        { -- | Name of the data constructor.-          daConName             :: !(DaConName n)--          -- | Type of the data constructor.-          --   The type must be closed.-        , daConType             :: !(Type n)--          -- | Algebraic constructors can be deconstructed with case-expressions,-          --   and must have a data type declaration.-          -- -          --   Non-algebraic types like 'Float' can't be inspected with-          --   case-expressions.-        , daConIsAlgebraic      :: !Bool }-        deriving Show---instance NFData n => NFData (DaCon n) where- rnf !dc-        =     rnf (daConName dc)-        `seq` rnf (daConType dc)-        `seq` rnf (daConIsAlgebraic dc)----- | Take the name of data constructor.-takeNameOfDaCon :: DaCon n -> Maybe n-takeNameOfDaCon dc- = case daConName dc of-        DaConUnit               -> Nothing-        DaConNamed n            -> Just n----- | Take the type annotation of a data constructor.-typeOfDaCon :: DaCon n -> Type n-typeOfDaCon dc  = daConType dc----- | The unit data constructor.-dcUnit  :: DaCon n-dcUnit  = DaCon-        { daConName             = DaConUnit-        , daConType             = tUnit-        , daConIsAlgebraic      = True }----- | Make an algebraic data constructor.-mkDaConAlg :: n -> Type n -> DaCon n-mkDaConAlg n t-        = DaCon-        { daConName             = DaConNamed n-        , daConType             = t-        , daConIsAlgebraic      = True }----- | Make a non-algebraic (solid) constructor.---   These are used for location values in the interpreter,---   and for floating point literals in the main compiler.-mkDaConSolid :: n -> Type n -> DaCon n-mkDaConSolid n t-        = DaCon-        { daConName             = DaConNamed n-        , daConType             = t-        , daConIsAlgebraic      = False }

@@ -1,25 +1,6 @@  -- | Abstract syntax for the Disciple core language. module DDC.Core.Exp -        ( module DDC.Type.Exp--          -- * Computation expressions-        , Exp     (..)-        , DaCon   (..)-        , DaConName(..)-        , Cast    (..)-        , Lets    (..)-        , LetMode (..)-        , Alt     (..)-        , Pat     (..)-                        -          -- * Witnesses expressions-        , Witness (..)-        , WiCon   (..)-        , WbCon   (..))+        ( module DDC.Core.Exp.Annot ) where-import DDC.Core.Exp.Base-import DDC.Core.Exp.NFData      ()-import DDC.Core.DaCon-import DDC.Type.Exp-+import DDC.Core.Exp.Annot

@@ -0,0 +1,202 @@++-- | Core language AST that includes an annotation on every node of +--   an expression.+--+--   This is the default representation for Disciple Core, and should be preferred+--   over the 'Simple' version of the AST in most cases. +--+--   * Local transformations on this AST should propagate the annotations in a way that+--   would make sense if they were source position identifiers that tracked the provenance+--   of each code snippet. If the specific annotations attached to the AST would not make+--   sense after such a transformation, then the client should erase them to @()@ beforehand+--   using the `reannotate` transform.+--+--   * Global transformations that drastically change the provenance of code snippets should+--     accept an AST with an arbitrary annotation type, but produce one with the annotations+--     set to @()@.+--+module DDC.Core.Exp.Annot +        ( module DDC.Type.Exp++         -- * Expressions+        , Exp           (..)+        , Lets          (..)+        , Alt           (..)+        , Pat           (..)+        , Cast          (..)++          -- * Witnesses+        , Witness       (..)++          -- * Data Constructors+        , DaCon         (..)+        , DaConName     (..)++          -- * Witness Constructors+        , WiCon         (..)+        , WbCon         (..))+where+import DDC.Core.Exp.WiCon+import DDC.Core.Exp.DaCon+import DDC.Core.Exp.Pat+import DDC.Type.Exp+import DDC.Type.Sum             ()+import Control.DeepSeq+++-- Values ---------------------------------------------------------------------+-- | Well-typed expressions have types of kind `Data`.+data Exp a n+        -- | Value variable   or primitive operation.+        = XVar  !a  !(Bound n)++        -- | Data constructor or literal.+        | XCon  !a  !(DaCon n)++        -- | Type abstraction (level-1).+        | XLAM  !a  !(Bind n)   !(Exp a n)++        -- | Value and Witness abstraction (level-0).+        | XLam  !a  !(Bind n)   !(Exp a n)++        -- | Application.+        | XApp  !a  !(Exp a n)  !(Exp a n)++        -- | Possibly recursive bindings.+        | XLet  !a  !(Lets a n) !(Exp a n)++        -- | Case branching.+        | XCase !a  !(Exp a n)  ![Alt a n]++        -- | Type cast.+        | XCast !a  !(Cast a n) !(Exp a n)++        -- | Type can appear as the argument of an application.+        | XType     !(Type n)++        -- | Witness can appear as the argument of an application.+        | XWitness  !(Witness a n)+        deriving (Show, Eq)+++-- | Possibly recursive bindings.+data Lets a n+        -- | Non-recursive expression binding.+        = LLet    !(Bind n) !(Exp a n)++        -- | Recursive binding of lambda abstractions.+        | LRec    ![(Bind n, Exp a n)]++        -- | Bind a local region variable,+        --   and witnesses to its properties.+        | LLetRegions ![Bind n] ![Bind n]+        +        -- | Holds a region handle during evaluation.+        | LWithRegion !(Bound n)+        deriving (Show, Eq)+++-- | Case alternatives.+data Alt a n+        = AAlt !(Pat n) !(Exp a n)+        deriving (Show, Eq)+++-- | Type casts.+data Cast a n+        -- | Weaken the effect of an expression.+        --   The given effect is added to the effect+        --   of the body.+        = CastWeakenEffect  !(Effect n)+        +        -- | Weaken the closure of an expression.+        --   The closures of these expressions are added to the closure+        --   of the body.+        | CastWeakenClosure ![Exp a n]++        -- | Purify the effect (action) of an expression.+        | CastPurify !(Witness a n)++        -- | Forget about the closure (sharing) of an expression.+        | CastForget !(Witness a n)++        -- | Suspend a computation, +        --   capturing its effects in the S computation type.+        | CastSuspend ++        -- | Run a computation,+        --   releasing its effects into the environment.+        | CastRun+        deriving (Show, Eq)+++-- | When a witness exists in the program it guarantees that a+--   certain property of the program is true.+data Witness a n+        -- | Witness variable.+        = WVar  a !(Bound n)+        +        -- | Witness constructor.+        | WCon  a !(WiCon n)+        +        -- | Witness application.+        | WApp  a !(Witness a n) !(Witness a n)++        -- | Joining of witnesses.+        | WJoin a !(Witness a n) !(Witness a n)++        -- | Type can appear as the argument of an application.+        | WType a !(Type n)+        deriving (Show, Eq)+++-- NFData ---------------------------------------------------------------------+instance (NFData a, NFData n) => NFData (Exp a n) where+ rnf xx+  = case xx of+        XVar  a u       -> rnf a `seq` rnf u+        XCon  a dc      -> rnf a `seq` rnf dc+        XLAM  a b x     -> rnf a `seq` rnf b   `seq` rnf x+        XLam  a b x     -> rnf a `seq` rnf b   `seq` rnf x+        XApp  a x1 x2   -> rnf a `seq` rnf x1  `seq` rnf x2+        XLet  a lts x   -> rnf a `seq` rnf lts `seq` rnf x+        XCase a x alts  -> rnf a `seq` rnf x   `seq` rnf alts+        XCast a c x     -> rnf a `seq` rnf c   `seq` rnf x+        XType t         -> rnf t+        XWitness w      -> rnf w+++instance (NFData a, NFData n) => NFData (Cast a n) where+ rnf cc+  = case cc of+        CastWeakenEffect e      -> rnf e+        CastWeakenClosure xs    -> rnf xs+        CastPurify w            -> rnf w+        CastForget w            -> rnf w+        CastSuspend             -> ()+        CastRun                 -> ()+++instance (NFData a, NFData n) => NFData (Lets a n) where+ rnf lts+  = case lts of+        LLet b x                -> rnf b `seq` rnf x+        LRec bxs                -> rnf bxs+        LLetRegions bs1 bs2     -> rnf bs1  `seq` rnf bs2+        LWithRegion u           -> rnf u+++instance (NFData a, NFData n) => NFData (Alt a n) where+ rnf aa+  = case aa of+        AAlt w x                -> rnf w `seq` rnf x+++instance (NFData a, NFData n) => NFData (Witness a n) 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+        WJoin a w1 w2             -> rnf a `seq` rnf w1 `seq` rnf w2+        WType a tt                -> rnf a `seq` rnf tt

@@ -1,186 +0,0 @@--module DDC.Core.Exp.Base where-import DDC.Core.DaCon-import DDC.Type.Exp-import DDC.Type.Sum             ()----- Values ------------------------------------------------------------------------ | Well-typed expressions produce `Data` values when evaluated, ---   and their types aways have kind '*' (Data)-data Exp a n-        -- | Value variable   or primitive operation.-        = XVar  !a  !(Bound n)--        -- | Data constructor or literal.-        | XCon  !a  !(DaCon n)--        -- | Type abstraction (level-1).-        | XLAM  !a  !(Bind n)   !(Exp a n)--        -- | Value and Witness abstraction (level-0).-        | XLam  !a  !(Bind n)   !(Exp a n)--        -- | Application.-        | XApp  !a  !(Exp a n)  !(Exp a n)--        -- | Possibly recursive bindings.-        | XLet  !a  !(Lets a n) !(Exp a n)--        -- | Case branching.-        | XCase !a  !(Exp a n)  ![Alt a n]--        -- | Type cast.-        | XCast !a  !(Cast a n) !(Exp a n)--        -- | Type can appear as the argument of an application.-        | XType    !(Type n)--        -- | Witness can appear as the argument of an application.-        | XWitness !(Witness n)-        deriving (Eq, Show)--deriving instance Eq n => Eq (DaCon n)----- | Type casts.-data Cast a n-        -- | Weaken the effect of an expression.-        --   The given effect is added to the effect-        --   of the body.-        = CastWeakenEffect  !(Effect n)-        -        -- | Weaken the closure of an expression.-        --   The closures of these expressions are added to the closure-        --   of the body.-        | CastWeakenClosure ![Exp a n]--        -- | Purify the effect (action) of an expression.-        | CastPurify !(Witness n)--        -- | Forget about the closure (sharing) of an expression.-        | CastForget !(Witness n)-        deriving (Eq, Show)----- | Possibly recursive bindings.-data Lets a n-        -- | Non-recursive expression binding.-        = LLet    !(LetMode n) !(Bind n) !(Exp a n)--        -- | Recursive binding of lambda abstractions.-        | LRec    ![(Bind n, Exp a n)]--        -- | Bind a local region variable,-        --   and witnesses to its properties.-        | LLetRegions ![Bind n] ![Bind n]-        -        -- | Holds a region handle during evaluation.-        | LWithRegion !(Bound n)-        deriving (Eq, Show)----- | Describes how a let binding should be evaluated.-data LetMode n-        -- | Evaluate binding before substituting the result.-        = LetStrict--        -- | Use lazy evaluation. -        --   The witness shows that the head region of the bound expression-        --   can contain thunks (is lazy), or Nothing if there is no head region.-        | LetLazy !(Maybe (Witness n))-        deriving (Eq, Show)----- | Case alternatives.-data Alt a n-        = AAlt !(Pat n) !(Exp a n)-        deriving (Eq, Show)----- | Pattern matching.-data Pat n-        -- | The default pattern always succeeds.-        = PDefault-        -        -- | Match a data constructor and bind its arguments.-        | PData !(DaCon n) ![Bind n]-        deriving (Eq, Show)-        ---- Witness ----------------------------------------------------------------------- | When a witness exists in the program it guarantees that a---   certain property of the program is true.-data Witness n-        -- | Witness variable.-        = WVar  !(Bound n)-        -        -- | Witness constructor.-        | WCon  !(WiCon n)-        -        -- | Witness application.-        | WApp  !(Witness n) !(Witness n)--        -- | Joining of witnesses.-        | WJoin !(Witness n) !(Witness n)--        -- | Type can appear as the argument of an application.-        | WType !(Type n)-        deriving (Eq, Show)----- | Witness constructors.-data WiCon n-        -- | Witness constructors baked into the language.-        = WiConBuiltin !WbCon--        -- | Witness constructors defined in the environment.-        --   In the interpreter we use this to hold runtime capabilities.-        --   The attached type must be closed.-        | WiConBound !(Bound n) !(Type n)-        deriving (Eq, Show)----- | Built-in witness constructors.------   These are used to convert a runtime capability into a witness that---   the corresponding property is true.-data WbCon-        -- | (axiom) The pure effect is pure.-        -- -        --   @pure     :: Pure !0@-        = WbConPure --        -- | (axiom) The empty closure is empty.-        ---        --   @empty    :: Empty $0@-        | WbConEmpty--        -- | Convert a capability guaranteeing that a region is in the global-        --   heap, into a witness that a closure using this region is empty.-        --   This lets us rely on the garbage collector to reclaim objects-        --   in the region. It is needed when we suspend the evaluation of -        --   expressions that have a region in their closure, because the-        --   type of the returned thunk may not reveal that it references-        --   objects in that region.-        -- -        --  @use      :: [r : %]. Global r => Empty (Use r)@-        | WbConUse      --        -- | Convert a capability guaranteeing the constancy of a region, into-        --   a witness that a read from that region is pure.-        --   This lets us suspend applications that read constant objects,-        --   because it doesn't matter if the read is delayed, we'll always-        --   get the same result.-        ---        --   @read     :: [r : %]. Const r  => Pure (Read r)@-        | WbConRead     --        -- | Convert a capability guaranteeing the constancy of a region, into-        --   a witness that allocation into that region is pure.-        --   This lets us increase the sharing of constant objects,-        --   because we can't tell constant objects of the same value apart.-        -- -        --  @alloc    :: [r : %]. Const r  => Pure (Alloc r)@-        | WbConAlloc-        deriving (Eq, Show)

@@ -0,0 +1,101 @@++module DDC.Core.Exp.DaCon +        ( DaCon         (..)+        , DaConName     (..)++        -- * Compounds+        , dcUnit+        , mkDaConAlg+        , mkDaConSolid+        , takeNameOfDaCon+        , typeOfDaCon)+where+import DDC.Type.Compounds+import DDC.Type.Exp+import Control.DeepSeq+++-------------------------------------------------------------------------------+-- | Data constructor names.+data DaConName n+        -- | The unit data constructor is builtin.+        = DaConUnit++        -- | Data constructor name defined by the client.+        | DaConNamed n+        deriving (Eq, Show)+++instance NFData n => NFData (DaConName n) where+ rnf dcn+  = case dcn of+        DaConUnit       -> ()+        DaConNamed n    -> rnf n+++-------------------------------------------------------------------------------+-- | Data constructors.+data DaCon n+        = DaCon+        { -- | Name of the data constructor.+          daConName             :: !(DaConName n)++          -- | Type of the data constructor.+          --   The type must be closed.+        , daConType             :: !(Type n)++          -- | Algebraic constructors can be deconstructed with case-expressions,+          --   and must have a data type declaration.+          -- +          --   Non-algebraic types like 'Float' can't be inspected with+          --   case-expressions.+        , daConIsAlgebraic      :: !Bool }+        deriving (Show, Eq)+++instance NFData n => NFData (DaCon n) where+ rnf !dc+        =     rnf (daConName dc)+        `seq` rnf (daConType dc)+        `seq` rnf (daConIsAlgebraic dc)+++-- | Take the name of data constructor.+takeNameOfDaCon :: DaCon n -> Maybe n+takeNameOfDaCon dc+ = case daConName dc of+        DaConUnit               -> Nothing+        DaConNamed n            -> Just n+++-- | Take the type annotation of a data constructor.+typeOfDaCon :: DaCon n -> Type n+typeOfDaCon dc  = daConType dc+++-- | The unit data constructor.+dcUnit  :: DaCon n+dcUnit  = DaCon+        { daConName             = DaConUnit+        , daConType             = tUnit+        , daConIsAlgebraic      = True }+++-- | Make an algebraic data constructor.+mkDaConAlg :: n -> Type n -> DaCon n+mkDaConAlg n t+        = DaCon+        { daConName             = DaConNamed n+        , daConType             = t+        , daConIsAlgebraic      = True }+++-- | Make a non-algebraic (solid) constructor.+--   These are used for location values in the interpreter,+--   and for floating point literals in the main compiler.+mkDaConSolid :: n -> Type n -> DaCon n+mkDaConSolid n t+        = DaCon+        { daConName             = DaConNamed n+        , daConType             = t+        , daConIsAlgebraic      = False }

@@ -1,82 +0,0 @@--module DDC.Core.Exp.NFData where-import DDC.Core.Exp.Base-import Control.DeepSeq---instance (NFData a, NFData n) => NFData (Exp a n) where- rnf xx-  = case xx of-        XVar  a u       -> rnf a `seq` rnf u-        XCon  a dc      -> rnf a `seq` rnf dc-        XLAM  a b x     -> rnf a `seq` rnf b   `seq` rnf x-        XLam  a b x     -> rnf a `seq` rnf b   `seq` rnf x-        XApp  a x1 x2   -> rnf a `seq` rnf x1  `seq` rnf x2-        XLet  a lts x   -> rnf a `seq` rnf lts `seq` rnf x-        XCase a x alts  -> rnf a `seq` rnf x   `seq` rnf alts-        XCast a c x     -> rnf a `seq` rnf c   `seq` rnf x-        XType t         -> rnf t-        XWitness w      -> rnf w---instance (NFData a, NFData n) => NFData (Cast a n) where- rnf cc-  = case cc of-        CastWeakenEffect e      -> rnf e-        CastWeakenClosure xs    -> rnf xs-        CastPurify w            -> rnf w-        CastForget w            -> rnf w---instance (NFData a, NFData n) => NFData (Lets a n) where- rnf lts-  = case lts of-        LLet mode b x           -> rnf mode `seq` rnf b `seq` rnf x-        LRec bxs                -> rnf bxs-        LLetRegions bs1 bs2     -> rnf bs1  `seq` rnf bs2-        LWithRegion u           -> rnf u---instance NFData n => NFData (LetMode n) where- rnf mode-  = case mode of-        LetStrict               -> ()-        LetLazy mw              -> rnf mw---instance (NFData a, NFData n) => NFData (Alt a n) where- rnf aa-  = case aa of-        AAlt w x                -> rnf w `seq` rnf x---instance NFData n => NFData (Pat n) where- rnf pp-  = case pp of-        PDefault                -> ()-        PData dc bs             -> rnf dc `seq` rnf bs---instance NFData n => NFData (Witness n) where- rnf ww-  = case ww of-        WVar  u                 -> rnf u-        WCon  c                 -> rnf c-        WApp  w1 w2             -> rnf w1 `seq` rnf w2-        WJoin w1 w2             -> rnf w1 `seq` rnf w2-        WType tt                -> rnf tt---instance NFData n => NFData (WiCon n) where- rnf wi-  = case wi of-        WiConBuiltin wb         -> rnf wb-        WiConBound   u t        -> rnf u `seq` rnf t--instance NFData WbCon------

@@ -0,0 +1,26 @@++module DDC.Core.Exp.Pat+        ( Pat (..))+where+import DDC.Core.Exp.DaCon+import DDC.Type.Exp+import Control.DeepSeq+++-- | Pattern matching.+data Pat n+        -- | The default pattern always succeeds.+        = PDefault+        +        -- | Match a data constructor and bind its arguments.+        | PData !(DaCon n) ![Bind n]+        deriving (Show, Eq)+        ++instance NFData n => NFData (Pat n) where+ rnf pp+  = case pp of+        PDefault                -> ()+        PData dc bs             -> rnf dc `seq` rnf bs++

@@ -0,0 +1,202 @@++-- | Core language AST with a separate node to hold annotations.+--+--   This version of the AST is used when generating code where most or all+--   of the annotations would be empty. General purpose transformations should+--   deal with the fully annotated version of the AST instead.+--+module DDC.Core.Exp.Simple +        ( module DDC.Type.Exp++          -- * Expressions+        , Exp           (..)+        , Cast          (..)+        , Lets          (..)+        , Alt           (..)+        , Pat           (..)++          -- * Witnesses+        , Witness       (..)++          -- * Data Constructors+        , DaCon         (..)+        , DaConName     (..)++          -- * Witness Constructors+        , WiCon         (..)+        , WbCon         (..))+where+import DDC.Core.Exp.WiCon+import DDC.Core.Exp.DaCon+import DDC.Core.Exp.Pat+import DDC.Type.Exp+import DDC.Type.Sum             ()+import Control.DeepSeq+++-- Values ---------------------------------------------------------------------+-- | Well-typed expressions have types of kind `Data`.+data Exp a n+        -- | Annotation.+        = XAnnot a (Exp a n)++        -- | Value variable   or primitive operation.+        | XVar  !(Bound n)++        -- | Data constructor or literal.+        | XCon  !(DaCon n)++        -- | Type abstraction (level-1).+        | XLAM  !(Bind n)   !(Exp a n)++        -- | Value and Witness abstraction (level-0).+        | XLam  !(Bind n)   !(Exp a n)++        -- | Application.+        | XApp  !(Exp a n)  !(Exp a n)++        -- | Possibly recursive bindings.+        | XLet  !(Lets a n) !(Exp a n)++        -- | Case branching.+        | XCase !(Exp a n)  ![Alt a n]++        -- | Type cast.+        | XCast !(Cast a n) !(Exp a n)++        -- | Type can appear as the argument of an application.+        | XType    !(Type n)++        -- | Witness can appear as the argument of an application.+        | XWitness !(Witness a n)+        deriving (Show, Eq)+++-- | Possibly recursive bindings.+data Lets a n+        -- | Non-recursive expression binding.+        = LLet        !(Bind n) !(Exp a n)++        -- | Recursive binding of lambda abstractions.+        | LRec        ![(Bind n, Exp a n)]++        -- | Bind a local region variable,+        --   and witnesses to its properties.+        | LLetRegions ![Bind n] ![Bind n]+        +        -- | Holds a region handle during evaluation.+        | LWithRegion !(Bound n)+        deriving (Show, Eq)+++-- | Case alternatives.+data Alt a n+        = AAlt !(Pat n) !(Exp a n)+        deriving (Show, Eq)+++-- | When a witness exists in the program it guarantees that a+--   certain property of the program is true.+data Witness a n+        = WAnnot a (Witness a n)++        -- | Witness variable.+        | WVar  !(Bound n)+        +        -- | Witness constructor.+        | WCon  !(WiCon n)+        +        -- | Witness application.+        | WApp  !(Witness a n) !(Witness a n)++        -- | Joining of witnesses.+        | WJoin !(Witness a n) !(Witness a n)++        -- | Type can appear as the argument of an application.+        | WType !(Type n)+        deriving (Show, Eq)+++-- | Type casts.+data Cast a n+        -- | Weaken the effect of an expression.+        --   The given effect is added to the effect+        --   of the body.+        = CastWeakenEffect  !(Effect n)+        +        -- | Weaken the closure of an expression.+        --   The closures of these expressions are added to the closure+        --   of the body.+        | CastWeakenClosure ![Exp a n]++        -- | Purify the effect (action) of an expression.+        | CastPurify        !(Witness a n)++        -- | Forget about the closure (sharing) of an expression.+        | CastForget        !(Witness a n)++        -- | Suspend a computation, +        --   capturing its effects in the S computation type.+        | CastSuspend ++        -- | Run a computation,+        --   releasing its effects into the environment.+        | CastRun+        deriving (Show, Eq)+++++-- NFData ---------------------------------------------------------------------+instance (NFData a, NFData n) => NFData (Exp a n) where+ rnf xx+  = case xx of+        XAnnot a x      -> rnf a   `seq` rnf x+        XVar   u        -> rnf u+        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+++instance (NFData a, NFData n) => NFData (Cast a n) where+ rnf cc+  = case cc of+        CastWeakenEffect e      -> rnf e+        CastWeakenClosure xs    -> rnf xs+        CastPurify w            -> rnf w+        CastForget w            -> rnf w+        CastSuspend             -> ()+        CastRun                 -> ()+++instance (NFData a, NFData n) => NFData (Lets a n) where+ rnf lts+  = case lts of+        LLet b x                -> rnf b `seq` rnf x+        LRec bxs                -> rnf bxs+        LLetRegions bs1 bs2     -> rnf bs1  `seq` rnf bs2+        LWithRegion u           -> rnf u+++instance (NFData a, NFData n) => NFData (Alt a n) where+ rnf aa+  = case aa of+        AAlt w x                -> rnf w `seq` rnf x+++instance (NFData a, NFData n) => NFData (Witness a n) 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+        WJoin  w1 w2            -> rnf w1 `seq` rnf w2+        WType  t                -> rnf t+

@@ -0,0 +1,75 @@++module DDC.Core.Exp.WiCon+        ( WiCon  (..)+        , WbCon  (..))+where+import DDC.Type.Exp+import DDC.Type.Sum     ()+import Control.DeepSeq+++-- | Witness constructors.+data WiCon n+        -- | Witness constructors baked into the language.+        = WiConBuiltin !WbCon++        -- | Witness constructors defined in the environment.+        --   In the interpreter we use this to hold runtime capabilities.+        --   The attached type must be closed.+        | WiConBound   !(Bound n) !(Type n)+        deriving (Show, Eq)+++-- | Built-in witness constructors.+--+--   These are used to convert a runtime capability into a witness that+--   the corresponding property is true.+data WbCon+        -- | (axiom) The pure effect is pure.+        -- +        --   @pure     :: Pure !0@+        = WbConPure ++        -- | (axiom) The empty closure is empty.+        --+        --   @empty    :: Empty $0@+        | WbConEmpty++        -- | Convert a capability guaranteeing that a region is in the global+        --   heap, into a witness that a closure using this region is empty.+        --   This lets us rely on the garbage collector to reclaim objects+        --   in the region. It is needed when we suspend the evaluation of +        --   expressions that have a region in their closure, because the+        --   type of the returned thunk may not reveal that it references+        --   objects in that region.+        -- +        --  @use      :: [r : %]. Global r => Empty (Use r)@+        | WbConUse      ++        -- | Convert a capability guaranteeing the constancy of a region, into+        --   a witness that a read from that region is pure.+        --   This lets us suspend applications that read constant objects,+        --   because it doesn't matter if the read is delayed, we'll always+        --   get the same result.+        --+        --   @read     :: [r : %]. Const r  => Pure (Read r)@+        | WbConRead     ++        -- | Convert a capability guaranteeing the constancy of a region, into+        --   a witness that allocation into that region is pure.+        --   This lets us increase the sharing of constant objects,+        --   because we can't tell constant objects of the same value apart.+        -- +        --  @alloc    :: [r : %]. Const r  => Pure (Alloc r)@+        | WbConAlloc+        deriving (Show, Eq)+++-- NFData ---------------------------------------------------------------------+instance NFData n => NFData (WiCon n) where+ rnf wi+  = case wi of+        WiConBuiltin wb         -> rnf wb+        WiConBound   u t        -> rnf u `seq` rnf t++instance NFData WbCon

@@ -30,7 +30,6 @@ import DDC.Data.Token  --- Fragment ------------------------------------------------------------------- -- | Carries all the information we need to work on a particular  --   fragment of the Disciple Core language. data Fragment n (err :: * -> *)

@@ -26,7 +26,7 @@         => Profile n            -- ^ Fragment profile giving the supported                                 --   language features and primitive operators.         -> c a n                -- ^ The thing to check.-        -> Maybe (Error n)+        -> Maybe (Error a n)  complies profile thing  = compliesWithEnvs profile@@ -43,7 +43,7 @@ 	-> Env.KindEnv n        -- ^ Starting kind environment. 	-> Env.TypeEnv n        -- ^ Starting type environment. 	-> c a n                -- ^ The thing to check.-	-> Maybe (Error n)+	-> Maybe (Error a n)  compliesWithEnvs profile kenv tenv thing  = let  merr    = result @@ -69,7 +69,7 @@         -> Env n                -- ^ Starting Type environment.         -> Context         -> c a n -        -> CheckM n+        -> CheckM a n                 (Set n, Set n)  -- Used type and value names.  @@ -186,20 +186,12 @@                         , Set.union vUsed1 vUsed2)          -- let -----------------------------------        XLet _ (LLet mode b1 x1) x2+        XLet _ (LLet b1 x1) x2          -> do  let tenv'        = Env.extend b1 tenv                 (tUsed1, vUsed1) <- compliesX profile kenv tenv  (reset context) x1                 (tUsed2, vUsed2) <- compliesX profile kenv tenv' (reset context) x2                 vUsed2'          <- checkBind profile tenv b1 vUsed2 -                -- Check for unsupported lazy bindings.-                (case mode of-                  LetStrict     -> return ()-                  LetLazy _     -                   | has featuresLazyBindings -> return ()-                   | otherwise          -                   -> throw $ ErrorUnsupported LazyBindings)-                 return  ( Set.union tUsed1 tUsed2                         , Set.union vUsed1 vUsed2') @@ -275,7 +267,7 @@         -> Env n                -- ^ The current environment         -> Bind n               -- ^ The binder at this site.         -> Set n                -- ^ Names used under the binder.-        -> CheckM n (Set n)     -- ^ Names used above the binder.+        -> CheckM a n (Set n)   -- ^ Names used above the binder.  checkBind profile env bb used  = let has f   = f $ profileFeatures profile@@ -305,7 +297,7 @@         :: Ord n           => Profile n          -> Env n  -> [Bind n] -> Set n -        -> CheckM n (Set n)+        -> CheckM a n (Set n)  checkBinds profile env bs used  = case bs of@@ -317,7 +309,7 @@  -- Function ------------------------------------------------------------------- -- | Check the function part of an application.-checkFunction :: Profile n -> Exp a n -> CheckM n ()+checkFunction :: Profile n -> Exp a n -> CheckM a n () checkFunction profile xx   = let  has f   = f $ profileFeatures profile         ok       = return ()@@ -367,10 +359,10 @@  -- Monad ---------------------------------------------------------------------- -- | Compliance checking monad.-data CheckM n x-        = CheckM (Either (Error n) x)+data CheckM a n x+        = CheckM (Either (Error a n) x) -instance Monad (CheckM n) where+instance Monad (CheckM a n) where  return x   = CheckM (Right x)  (>>=) m f     = case m of@@ -379,10 +371,10 @@   -- | Throw an error in the monad.-throw :: Error n -> CheckM n x+throw :: Error a n -> CheckM a n x throw e       = CheckM $ Left e   -- | Take the result from a check monad.-result :: CheckM n x -> Either (Error n) x+result :: CheckM a n x -> Either (Error a n) x result (CheckM r)       = r

@@ -8,7 +8,7 @@   -- | Language fragment compliance violations.-data Error n+data Error a n         -- | Found an unsupported language feature.         = ErrorUnsupported      !Feature @@ -30,11 +30,11 @@         | ErrorNakedType        !(Type    n)          -- | Found a naked witness that isn't used as a function argument.-        | ErrorNakedWitness     !(Witness n)-        deriving (Eq, Show)+        | ErrorNakedWitness     !(Witness a n)+        deriving Show  -instance (Pretty n, Eq n) => Pretty (Error n) where+instance (Pretty n, Eq n) => Pretty (Error a n) where  ppr err   = case err of         ErrorUnsupported feature

@@ -7,14 +7,18 @@ -- | Language feature supported by a fragment. data Feature         -- Type system features ----------------------------        -- | Assume all functions perform global side effects, -        --   and don't generate effect terms in types.-        = UntrackedEffects+        -- | Track effect type information.+        = TrackedEffects -        -- | Assume all functions share data invisibly,-        --   and don't generate closure terms in types.-        | UntrackedClosures+        -- | Track closure type information.+        | TrackedClosures +        -- | Attach latent effects to function types.+        | FunctionalEffects++        -- | Attach latent closures to function types.+        | FunctionalClosures+         -- General features -------------------------------         -- | Partially applied primitive operators.         | PartialPrims@@ -30,11 +34,6 @@         -- | Nested function bindings.         --   The output of the lambda-lifter should not contain these.         | NestedFunctions--        -- | Lazy let-bindings.-        --   Turning this off means the runtime system won't need to build-        --   suspensions.-        | LazyBindings          -- | Debruijn binders.         --   Most backends will want to use real names, instead of indexed

@@ -11,7 +11,7 @@ import DDC.Core.Fragment.Feature import DDC.Type.DataDef import DDC.Type.Exp-import DDC.Type.Env                     (KindEnv, TypeEnv)+import DDC.Type.Env                     (SuperEnv, KindEnv, TypeEnv) import qualified DDC.Type.Env           as Env  @@ -28,6 +28,9 @@           -- | Primitive data type declarations.         , profilePrimDataDefs           :: !(DataDefs n) +          -- | Supers of primitive kinds.+        , profilePrimSupers             :: !(SuperEnv n)+           -- | Kinds of primitive types.         , profilePrimKinds              :: !(KindEnv n) @@ -48,6 +51,7 @@         { profileName                   = "Zero"         , profileFeatures               = zeroFeatures         , profilePrimDataDefs           = emptyDataDefs+        , profilePrimSupers             = Env.empty         , profilePrimKinds              = Env.empty         , profilePrimTypes              = Env.empty         , profileTypeIsUnboxed          = const False }@@ -56,13 +60,14 @@ -- | A flattened set of features, for easy lookup. data Features          = Features-        { featuresUntrackedEffects      :: Bool-        , featuresUntrackedClosures     :: Bool+        { featuresTrackedEffects        :: Bool+        , featuresTrackedClosures       :: Bool+        , featuresFunctionalEffects     :: Bool+        , featuresFunctionalClosures    :: Bool         , featuresPartialPrims          :: Bool         , featuresPartialApplication    :: Bool         , featuresGeneralApplication    :: Bool         , featuresNestedFunctions       :: Bool-        , featuresLazyBindings          :: Bool         , featuresDebruijnBinders       :: Bool         , featuresUnboundLevel0Vars     :: Bool         , featuresUnboxedInstantiation  :: Bool@@ -76,13 +81,14 @@ zeroFeatures :: Features zeroFeatures         = Features-        { featuresUntrackedEffects      = False-        , featuresUntrackedClosures     = False+        { featuresTrackedEffects        = False+        , featuresTrackedClosures       = False+        , featuresFunctionalEffects     = False+        , featuresFunctionalClosures    = False         , featuresPartialPrims          = False         , featuresPartialApplication    = False         , featuresGeneralApplication    = False         , featuresNestedFunctions       = False-        , featuresLazyBindings          = False         , featuresDebruijnBinders       = False         , featuresUnboundLevel0Vars     = False         , featuresUnboxedInstantiation  = False@@ -95,13 +101,14 @@ setFeature :: Feature -> Bool -> Features -> Features setFeature feature val features  = case feature of-        UntrackedEffects        -> features { featuresUntrackedEffects     = val }-        UntrackedClosures       -> features { featuresUntrackedClosures    = val }+        TrackedEffects          -> features { featuresTrackedEffects       = val }+        TrackedClosures         -> features { featuresTrackedClosures      = val }+        FunctionalEffects       -> features { featuresFunctionalEffects    = val }+        FunctionalClosures      -> features { featuresFunctionalClosures   = val }         PartialPrims            -> features { featuresPartialPrims         = val }         PartialApplication      -> features { featuresPartialApplication   = val }         GeneralApplication      -> features { featuresGeneralApplication   = val }         NestedFunctions         -> features { featuresNestedFunctions      = val }-        LazyBindings            -> features { featuresLazyBindings         = val }         DebruijnBinders         -> features { featuresDebruijnBinders      = val }         UnboundLevel0Vars       -> features { featuresUnboundLevel0Vars    = val }         UnboxedInstantiation    -> features { featuresUnboxedInstantiation = val }

@@ -21,6 +21,7 @@ import DDC.Data.SourcePos import DDC.Data.Token import Data.Char+import Data.List   -- Module ---------------------------------------------------------------------@@ -86,20 +87,27 @@         c : cs          | isDigit c          , (body, rest)         <- span isLitBody cs-         -> tokN (KLit (c:body))                 : lexMore (length (c:body)) rest+         -> tokN (KLit (c:body))        : lexMore (length (c:body)) rest          '-' : c : cs          | isDigit c          , (body, rest)         <- span isLitBody cs-         -> tokN (KLit ('-':c:body))                 : lexMore (length (c:body)) rest+         -> tokN (KLit ('-':c:body))    : lexMore (length (c:body)) rest          -- Meta tokens-        '{'  : '-' : w'  -> tokM KCommentBlockStart : lexMore 2 w'-        '-'  : '}' : w'  -> tokM KCommentBlockEnd   : lexMore 2 w'-        '-'  : '-' : w'  -> tokM KCommentLineStart  : lexMore 2 w'-        '\n' : w'        -> tokM KNewLine           : lexWord (line + 1) 1 w'+        -- ISSUE #302: Don't try to lex body of a block comment.+        '{'  : '-' : w'  +         -> tokM KCommentBlockStart : lexMore 2 w' +        '-'  : '}' : w'  +         -> tokM KCommentBlockEnd   : lexMore 2 w' +        '-'  : '-' : w'  +         -> let  (_junk, w'') = span (/= '\n') w'+            in   tokM KCommentLineStart  : lexMore 2 w''++        '\n' : w'        -> tokM KNewLine           : lexWord (line + 1) 1 w'+         -- The unit data constructor         '(' : ')' : w'   -> tokA KDaConUnit      : lexMore 2 w' @@ -150,29 +158,28 @@         '-'  : w'       -> tokA KDash            : lexMore 1 w'                  -- Bottoms-        '!' : '0' : w'  -> tokA KBotEffect       : lexMore 2 w'-        '$' : '0' : w'  -> tokA KBotClosure      : lexMore 2 w'--        -- Sort Constructors-        '*' : '*' : w'  -> tokA KSortComp        : lexMore 2 w'-        '@' : '@' : w'  -> tokA KSortProp        : lexMore 2 w'        --        -- Kind Constructors-        '*' : w'        -> tokA KKindValue       : lexMore 1 w'-        '%' : w'        -> tokA KKindRegion      : lexMore 1 w'-        '!' : w'        -> tokA KKindEffect      : lexMore 1 w'-        '$' : w'        -> tokA KKindClosure     : lexMore 1 w'-        '@' : w'        -> tokA KKindWitness     : lexMore 1 w'-        +        name+         |  Just w'     <- stripPrefix "Pure"  name +         -> tokA KBotEffect   : lexMore 2 w'+         +         |  Just w'     <- stripPrefix "Empty" name +         -> tokA KBotClosure  : lexMore 2 w'          -- Named Constructors         c : cs          | isConStart c          , (body,  rest)        <- span isConBody cs          , (body', rest')       <- case rest of-                                        '#' : rest'     -> (body ++ "#", rest')+                                        '\'' : rest'    -> (body ++ "'", rest')+                                        '#'  : rest'    -> (body ++ "#", rest')                                         _               -> (body, rest)          -> let readNamedCon s+                 | Just socon   <- readSoConBuiltin s+                 = tokA (KSoConBuiltin socon)    : lexMore (length s) rest'++                 | Just kicon   <- readKiConBuiltin s+                 = tokA (KKiConBuiltin kicon)    : lexMore (length s) rest'+                  | Just twcon   <- readTwConBuiltin s                  = tokA (KTwConBuiltin twcon)    : lexMore (length s) rest'                  @@ -195,13 +202,13 @@                                         '#' : rest'     -> (body ++ "#", rest')                                         _               -> (body, rest)          -> let readNamedVar s-                 | Just t <- lookup s keywords+                 | Just t  <- lookup s keywords                  = tok t                   : lexMore (length s) rest' -                 | Just wc      <- readWbConBuiltin s+                 | Just wc <- readWbConBuiltin s                  = tokA (KWbConBuiltin wc) : lexMore (length s) rest'          -                 | Just v       <- readVar s+                 | Just v  <- readVar s                  = tokN (KVar v)           : lexMore (length s) rest'                   | otherwise

@@ -4,6 +4,8 @@           keywords            -- * Builtin constructors+        , readSoConBuiltin+        , readKiConBuiltin         , readTwConBuiltin         , readTcConBuiltin         , readWbConBuiltin@@ -49,6 +51,8 @@         , ("case",       KA KCase)         , ("purify",     KA KPurify)         , ("forget",     KA KForget)+        , ("suspend",    KA KSuspend)+        , ("run",        KA KRun)         , ("type",       KA KType)         , ("weakeff",    KA KWeakEff)         , ("weakclo",    KA KWeakClo)@@ -59,7 +63,28 @@         , ("else",       KA KElse) ]  --- | Read a named `TwCon`. +-- | Read a named sort constructor.+readSoConBuiltin :: String -> Maybe SoCon+readSoConBuiltin ss+ = case ss of+        "Prop"          -> Just SoConProp+        "Comp"          -> Just SoConComp+        _               -> Nothing+++-- | Read a named kind constructor.+readKiConBuiltin :: String -> Maybe KiCon+readKiConBuiltin ss+ = case ss of+        "Witness"       -> Just KiConWitness+        "Data"          -> Just KiConData+        "Region"        -> Just KiConRegion+        "Effect"        -> Just KiConEffect+        "Closure"       -> Just KiConClosure+        _               -> Nothing+++-- | Read a named witness type constructor. readTwConBuiltin :: String -> Maybe TwCon readTwConBuiltin ss  = case ss of@@ -72,8 +97,8 @@         "Lazy"          -> Just TwConLazy         "HeadLazy"      -> Just TwConHeadLazy         "Manifest"      -> Just TwConManifest-        "Pure"          -> Just TwConPure-        "Empty"         -> Just TwConEmpty+        "Purify"        -> Just TwConPure+        "Emptify"       -> Just TwConEmpty         "Disjoint"      -> Just TwConDisjoint         "Distinct"      -> Just (TwConDistinct 2)         _               -> readTwConWithArity ss@@ -87,12 +112,13 @@  | otherwise = Nothing    --- | Read a builtin `TcCon` with a non-symbolic name, +-- | Read a builtin type constructor with a non-symbolic name. --   ie not '->'. readTcConBuiltin :: String -> Maybe TcCon readTcConBuiltin ss  = case ss of         "Unit"          -> Just TcConUnit+        "S"             -> Just TcConSusp         "Read"          -> Just TcConRead         "HeadRead"      -> Just TcConHeadRead         "DeepRead"      -> Just TcConDeepRead@@ -105,7 +131,7 @@         _               -> Nothing  --- | Read a `WbCon`.+-- | Read a witness constructor. readWbConBuiltin :: String -> Maybe WbCon readWbConBuiltin ss  = case ss of@@ -147,7 +173,12 @@ -- | Character can be part of a variable body. isVarBody  :: Char -> Bool isVarBody c-        = isUpper c || isLower c || isDigit c || c == '_' || c == '\''+        =  isUpper c +        || isLower c +        || isDigit c +        || c == '_' +        || c == '\'' +        || c == '$'   -- | Read a named, user defined variable.@@ -185,10 +216,13 @@  -- | Charater can be part of a constructor body. isConBody  :: Char -> Bool-isConBody c           = isUpper c || isLower c || isDigit c || c == '_'+isConBody c     +        =  isUpper c +        || isLower c +        || isDigit c +        || c == '_'          - -- | Read a named, user defined `TcCon`. readCon :: String -> Maybe String readCon ss@@ -223,4 +257,5 @@         || c == 'b' || c == 'o' || c == 'x'         || c == 'w' || c == 'i'          || c == '#'+        || c == '\'' 

@@ -160,13 +160,6 @@         | KBigLambda          -- symbolic constructors-        | KSortComp-        | KSortProp-        | KKindValue-        | KKindRegion-        | KKindEffect-        | KKindClosure-        | KKindWitness         | KArrowTilde         | KArrowDash         | KArrowDashLeft@@ -196,6 +189,8 @@         | KWeakClo         | KPurify         | KForget+        | KSuspend+        | KRun          -- sugar keywords         | KDo@@ -206,9 +201,12 @@         | KIndex Int          -- builtin names -------------        --   the unit data constructor.-        | KDaConUnit+        --   sort constructors.+        | KSoConBuiltin SoCon +        --   kind constructors.+        | KKiConBuiltin KiCon+         --   witness type constructors.         | KTwConBuiltin TwCon @@ -217,6 +215,9 @@          --   other builtin spec constructors.         | KTcConBuiltin TcCon++        --   the unit data constructor.+        | KDaConUnit         deriving (Eq, Show)  @@ -262,13 +263,6 @@         KBigLambda              -> (Symbol, "/\\")          -- symbolic constructors-        KSortComp               -> (Constructor, "**")-        KSortProp               -> (Constructor, "@@")-        KKindValue              -> (Constructor, "*")-        KKindRegion             -> (Constructor, "%")-        KKindEffect             -> (Constructor, "!")-        KKindClosure            -> (Constructor, "$")-        KKindWitness            -> (Constructor, "@")         KArrowTilde             -> (Constructor, "~>")         KArrowDash              -> (Constructor, "->")         KArrowDashLeft          -> (Constructor, "<-")@@ -298,6 +292,8 @@         KWeakClo                -> (Keyword, "weakclo")         KPurify                 -> (Keyword, "purify")         KForget                 -> (Keyword, "forget")+        KSuspend                -> (Keyword, "suspend")+        KRun                    -> (Keyword, "run")          -- sugar keywords         KDo                     -> (Keyword, "do")@@ -308,11 +304,13 @@         KIndex i                -> (Index,   "^" ++ show i)          -- builtin names-        KDaConUnit              -> (Constructor, "()")+        KSoConBuiltin so        -> (Constructor, renderPlain $ ppr so)+        KKiConBuiltin ki        -> (Constructor, renderPlain $ ppr ki)         KTwConBuiltin tw        -> (Constructor, renderPlain $ ppr tw)         KWbConBuiltin wi        -> (Constructor, renderPlain $ ppr wi)         KTcConBuiltin tc        -> (Constructor, renderPlain $ ppr tc)-+        KDaConUnit              -> (Constructor, "()")+          -- TokNamed ------------------------------------------------------------------- -- | A token with a user-defined name.

@@ -16,6 +16,7 @@ import DDC.Core.Fragment.Profile import DDC.Core.Lexer.Tokens import DDC.Core.Exp+import DDC.Core.Annot.AnT                       (AnT) import DDC.Type.Transform.SpreadT import DDC.Core.Module import DDC.Base.Pretty@@ -24,6 +25,7 @@ import qualified DDC.Core.Parser                as C import qualified DDC.Core.Check                 as C import qualified DDC.Type.Check                 as T+import qualified DDC.Type.Env                   as Env import qualified DDC.Base.Parser                as BP import Data.Map.Strict                          (Map) import System.Directory@@ -34,8 +36,8 @@         = ErrorRead       !String         | ErrorParser     !BP.ParseError         | ErrorCheckType  !(T.Error n)      -        | ErrorCheckExp   !(C.Error () n)-        | ErrorCompliance !(I.Error n)+        | ErrorCheckExp   !(C.Error BP.SourcePos n)+        | ErrorCompliance !(I.Error (C.AnTEC BP.SourcePos n) n)         deriving Show  @@ -72,7 +74,7 @@         -> (String -> [Token (Tok n)])  -- ^ Function to lex the source file.         -> FilePath                     -- ^ File containing source code.         -> IO (Either (Error n)-                      (Module (C.AnTEC () n) n))+                      (Module (C.AnTEC BP.SourcePos n) n))  loadModuleFromFile profile lexSource filePath  = do   @@ -89,6 +91,7 @@                  return $ loadModuleFromTokens profile filePath toks + -- | Parse and type check a core module from a string. loadModuleFromString         :: (Eq n, Ord n, Show n, Pretty n)@@ -96,7 +99,8 @@         -> (String -> [Token (Tok n)])  -- ^ Function to lex the source file.         -> FilePath                     -- ^ Path to source file for error messages.         -> String                       -- ^ Program text.-        -> Either (Error n) (Module (C.AnTEC () n) n)+        -> Either (Error n) +                  (Module (C.AnTEC BP.SourcePos n) n)  loadModuleFromString profile lexSource filePath src         = loadModuleFromTokens profile filePath (lexSource src)@@ -108,7 +112,8 @@         => Profile n                    -- ^ Language fragment profile.         -> FilePath                     -- ^ Path to source file for error messages.         -> [Token (Tok n)]              -- ^ Source tokens.-        -> Either (Error n) (Module (C.AnTEC () n) n)+        -> Either (Error n) +                  (Module (C.AnTEC BP.SourcePos n) n)  loadModuleFromTokens profile sourceName toks'  = goParse toks'@@ -120,7 +125,9 @@          -- Parse the tokens.         goParse toks                -         = case BP.runTokenParser describeTok sourceName C.pModule toks of+         = case BP.runTokenParser describeTok sourceName +                        (C.pModule (C.contextOfProfile profile))+                        toks of                 Left err  -> Left (ErrorParser err)                 Right mm  -> goCheckType (spreadX kenv tenv mm) @@ -149,7 +156,7 @@         -> FilePath             -- ^ Path to source file for error messages.         -> [Token (Tok n)]      -- ^ Source tokens.         -> Either (Error n) -                  (Exp (C.AnTEC () n) n)+                  (Exp (C.AnTEC BP.SourcePos n) n)  loadExp profile modules sourceName toks'  = goParse toks'@@ -161,7 +168,9 @@          -- Parse the tokens.         goParse toks                -         = case BP.runTokenParser describeTok sourceName C.pExp toks of+         = case BP.runTokenParser describeTok sourceName +                        (C.pExp (C.contextOfProfile profile))+                        toks of                 Left err  -> Left (ErrorParser err)                 Right t   -> goCheckType (spreadX kenv tenv t) @@ -191,18 +200,18 @@  loadType profile sourceName toks'  = goParse toks'- where  defs    = profilePrimDataDefs profile-        kenv    = profilePrimKinds    profile-+ where           -- Parse the tokens.         goParse toks                -         = case BP.runTokenParser describeTok sourceName C.pType toks of+         = case BP.runTokenParser describeTok sourceName +                        (C.pType (C.contextOfProfile profile))+                        toks of                 Left err  -> Left (ErrorParser err)-                Right t   -> goCheckType (spreadT kenv t)+                Right t   -> goCheckType (spreadT (profilePrimKinds profile) t)          -- Check the kind of the type.         goCheckType t-         = case T.checkType defs kenv t of+         = case T.checkType (T.configOfProfile profile) Env.empty t of                 Left err  -> Left (ErrorCheckType err)                 Right k   -> Right (t, k)         @@ -217,7 +226,7 @@         -> FilePath             -- ^ Path to source file for error messages.         -> [Token (Tok n)]      -- ^ Source tokens.         -> Either (Error n) -                  (Witness n, Type n)+                  (Witness (AnT BP.SourcePos n) n, Type n)  loadWitness profile sourceName toks'  = goParse toks'@@ -228,13 +237,15 @@          -- Parse the tokens.         goParse toks                -         = case BP.runTokenParser describeTok sourceName C.pWitness toks of+         = case BP.runTokenParser describeTok sourceName +                (C.pWitness (C.contextOfProfile profile)) +                toks of                 Left err  -> Left (ErrorParser err)                 Right t   -> goCheckType (spreadX kenv tenv t)          -- Check the kind of the type.         goCheckType w          = case C.checkWitness config kenv tenv w of-                Left err  -> Left (ErrorCheckExp err)-                Right k   -> Right (w, k)+                Left err      -> Left (ErrorCheckExp err)+                Right (w', t) -> Right (w', t) 

@@ -1,6 +1,8 @@ -- | Core language parser. module DDC.Core.Parser         ( Parser+        , Context       (..)+        , contextOfProfile          -- * Modules         , pModule@@ -36,9 +38,9 @@  where import DDC.Core.Parser.Base+import DDC.Core.Parser.Context import DDC.Core.Parser.Witness import DDC.Core.Parser.Type import DDC.Core.Parser.Exp import DDC.Core.Parser.Module- 

@@ -1,22 +1,22 @@  module DDC.Core.Parser.Base         ( Parser-        , pWbCon         , pModuleName         , pQualName         , pName-        , pCon-        , pLit-        , pIndex-        , pVar-        , pTok-        , pTokAs)+        , pWbCon,       pWbConSP+        , pCon,         pConSP+        , pLit,         pLitSP+        , pIndex,       pIndexSP+        , pVar,         pVarSP+        , pTok,         pTokSP+        , pTokAs,       pTokAsSP) where import DDC.Base.Pretty import DDC.Core.Module import DDC.Core.Exp import DDC.Core.Lexer.Tokens-import DDC.Base.Parser                  ((<?>))+import DDC.Base.Parser                  ((<?>), SourcePos) import qualified DDC.Base.Parser        as P  @@ -25,13 +25,6 @@         = P.Parser (Tok n) a  --- | Parse a builtin named `WiCon`-pWbCon :: Parser n WbCon-pWbCon  = P.pTokMaybe f- where  f (KA (KWbConBuiltin wb)) = Just wb-        f _                       = Nothing-- -- | Parse a module name.                                --    ---  ISSUE #273: Handle hierarchical module names.@@ -57,13 +50,34 @@ pName   = P.choice [pCon, pVar]  +-- | Parse a builtin named `WbCon`+pWbCon :: Parser n WbCon+pWbCon  = P.pTokMaybe f+ where  f (KA (KWbConBuiltin wb)) = Just wb+        f _                       = Nothing+++-- | Parse a builtin named `WbCon`+pWbConSP :: Parser n (WbCon, SourcePos)+pWbConSP = P.pTokMaybeSP f+ where  f (KA (KWbConBuiltin wb)) = Just wb+        f _                       = Nothing++ -- | Parse a constructor name.-pCon  :: Parser n n+pCon    :: Parser n n pCon    = P.pTokMaybe f  where  f (KN (KCon n)) = Just n         f _             = Nothing  +-- | Parse a constructor name.+pConSP    :: Parser n (n, SourcePos)+pConSP    = P.pTokMaybeSP f+ where  f (KN (KCon n)) = Just n+        f _             = Nothing++ -- | Parse a literal pLit :: Parser n n pLit    = P.pTokMaybe f@@ -71,6 +85,13 @@         f _             = Nothing  +-- | Parse a literal, with source position.+pLitSP :: Parser n (n, SourcePos)+pLitSP  = P.pTokMaybeSP f+ where  f (KN (KLit n)) = Just n+        f _             = Nothing++ -- | Parse a variable. pVar :: Parser n n pVar    =   P.pTokMaybe f@@ -79,6 +100,14 @@         f _                     = Nothing  +-- | Parse a variable, with source position.+pVarSP :: Parser n (n, SourcePos)+pVarSP  =   P.pTokMaybeSP f+        <?> "a variable"+ where  f (KN (KVar n))         = Just n+        f _                     = Nothing++ -- | Parse a deBruijn index pIndex :: Parser n Int pIndex  =   P.pTokMaybe f@@ -87,12 +116,29 @@         f _                     = Nothing  +-- | Parse a deBruijn index, with source position.+pIndexSP :: Parser n (Int, SourcePos)+pIndexSP  =   P.pTokMaybeSP f+        <?> "an index"+ where  f (KA (KIndex i))       = Just i+        f _                     = Nothing++ -- | Parse an atomic token. pTok :: TokAtom -> Parser n () pTok k     = P.pTok (KA k)  +-- | Parse an atomic token, yielding its source position.+pTokSP :: TokAtom -> Parser n SourcePos+pTokSP k   = P.pTokSP (KA k)++ -- | Parse an atomic token and return some value. pTokAs :: TokAtom -> a -> Parser n a pTokAs k x = P.pTokAs (KA k) x ++-- | Parse an atomic token and return source position and value.+pTokAsSP :: TokAtom -> a -> Parser n (a, SourcePos)+pTokAsSP k x = P.pTokAsSP (KA k) x

@@ -0,0 +1,34 @@++module DDC.Core.Parser.Context +        ( Context (..)+        , contextOfProfile)+where+import DDC.Core.Fragment+++-- | Configuration and information from the context. +--   Used for context sensitive parsing.+data Context+        = Context+        { contextTrackedEffects         :: Bool +        , contextTrackedClosures        :: Bool+        , contextFunctionalEffects      :: Bool+        , contextFunctionalClosures     :: Bool }+++-- | Slurp an initital Context from a Profile+contextOfProfile :: Profile n -> Context+contextOfProfile profile+        = Context+        { contextTrackedEffects         = featuresTrackedEffects+                                        $ profileFeatures profile++        , contextTrackedClosures        = featuresTrackedClosures+                                        $ profileFeatures profile++        , contextFunctionalEffects      = featuresFunctionalEffects+                                        $ profileFeatures profile++        , contextFunctionalClosures     = featuresFunctionalClosures+                                        $ profileFeatures profile+        }

@@ -3,8 +3,8 @@ module DDC.Core.Parser.Exp         ( pExp         , pExpApp-        , pExpAtom-        , pLets+        , pExpAtom,     pExpAtomSP+        , pLetsSP         , pType         , pTypeApp         , pTypeAtom)@@ -13,10 +13,11 @@ import DDC.Core.Parser.Witness import DDC.Core.Parser.Param import DDC.Core.Parser.Type+import DDC.Core.Parser.Context import DDC.Core.Parser.Base import DDC.Core.Lexer.Tokens import DDC.Core.Compounds-import DDC.Base.Parser                  ((<?>))+import DDC.Base.Parser                  ((<?>), SourcePos) import qualified DDC.Base.Parser        as P import qualified DDC.Type.Compounds     as T import Control.Monad.Error@@ -24,62 +25,62 @@  -- Expressions ---------------------------------------------------------------- -- | Parse a core language expression.-pExp    :: Ord n => Parser n (Exp () n)-pExp +pExp    :: Ord n => Context -> Parser n (Exp SourcePos n)+pExp c  = P.choice         -- Level-0 lambda abstractions         -- \(x1 x2 ... : TYPE) (y1 y2 ... : TYPE) ... . EXP- [ do   pTok KBackSlash+ [ do   sp      <- pTokSP KBackSlash          bs      <- liftM concat                 $  P.many1                  $  do   pTok KRoundBra                         bs'     <- P.many1 pBinder                         pTok KColon-                        t       <- pType+                        t       <- pType c                         pTok KRoundKet                         return (map (\b -> T.makeBindFromBinder b t) bs')          pTok KDot-        xBody   <- pExp-        return  $ foldr (XLam ()) xBody bs+        xBody   <- pExp c+        return  $ foldr (XLam sp) xBody bs          -- Level-1 lambda abstractions.         -- /\(x1 x2 ... : TYPE) (y1 y2 ... : TYPE) ... . EXP- , do   pTok KBigLambda+ , do   sp      <- pTokSP KBigLambda          bs      <- liftM concat                 $  P.many1                  $  do   pTok KRoundBra                         bs'     <- P.many1 pBinder                         pTok KColon-                        t       <- pType+                        t       <- pType c                         pTok KRoundKet                         return (map (\b -> T.makeBindFromBinder b t) bs')          pTok KDot-        xBody   <- pExp-        return  $ foldr (XLAM ()) xBody bs+        xBody   <- pExp c+        return  $ foldr (XLAM sp) xBody bs           -- let expression- , do   lts     <- pLets+ , do   (lts, sp) <- pLetsSP c         pTok    KIn-        x2      <- pExp-        return  $ XLet () lts x2+        x2      <- pExp c+        return  $ XLet sp lts x2           -- do { STMTS }         --   Sugar for a let-expression.  , do   pTok    KDo         pTok    KBraceBra-        xx      <- pStmts+        xx      <- pStmts c         pTok    KBraceKet         return  $ xx           -- withregion CON in EXP- , do   pTok KWithRegion+ , do   sp      <- pTokSP KWithRegion         u       <- P.choice                  [  do   n    <- pVar                         return $ UName n@@ -87,87 +88,98 @@                 ,  do   n    <- pCon                         return $ UPrim n kRegion]         pTok KIn-        x       <- pExp-        return  $ XLet () (LWithRegion u) x+        x       <- pExp c+        return  $ XLet sp (LWithRegion u) x           -- case EXP of { ALTS }- , do   pTok KCase-        x       <- pExp+ , do   sp      <- pTokSP KCase+        x       <- pExp c         pTok KOf          pTok KBraceBra-        alts    <- P.sepEndBy1 pAlt (pTok KSemiColon)+        alts    <- P.sepEndBy1 (pAlt c) (pTok KSemiColon)         pTok KBraceKet-        return  $ XCase () x alts+        return  $ XCase sp x alts           -- match PAT <- EXP else EXP in EXP         --  Sugar for a case-expression.- , do   pTok KMatch-        p       <- pPat+ , do   sp      <- pTokSP KMatch+        p       <- pPat c         pTok KArrowDashLeft-        x1      <- pExp +        x1      <- pExp c         pTok KElse-        x2      <- pExp +        x2      <- pExp c         pTok KIn-        x3      <- pExp-        return  $ XCase () x1 [AAlt p x3, AAlt PDefault x2]+        x3      <- pExp c+        return  $ XCase sp x1 [AAlt p x3, AAlt PDefault x2]           -- weakeff [TYPE] in EXP- , do   pTok KWeakEff+ , do   sp      <- pTokSP KWeakEff         pTok KSquareBra-        t       <- pType+        t       <- pType c         pTok KSquareKet         pTok KIn-        x       <- pExp-        return  $ XCast () (CastWeakenEffect t) x+        x       <- pExp c+        return  $ XCast sp (CastWeakenEffect t) x           -- weakclo {EXP;+} in EXP- , do   pTok KWeakClo+ , do   sp      <- pTokSP KWeakClo         pTok KBraceBra-        xs       <- liftM concat $ P.sepEndBy1 pArgs (pTok KSemiColon)+        xs      <- liftM (map fst . concat) +                $  P.sepEndBy1 (pArgSPs c) (pTok KSemiColon)         pTok KBraceKet         pTok KIn-        x       <- pExp-        return  $ XCast () (CastWeakenClosure xs) x+        x       <- pExp c+        return  $ XCast sp (CastWeakenClosure xs) x           -- purify <WITNESS> in EXP- , do   pTok KPurify+ , do   sp      <- pTokSP KPurify         pTok KAngleBra-        w       <- pWitness+        w       <- pWitness c         pTok KAngleKet         pTok KIn-        x       <- pExp-        return  $ XCast () (CastPurify w) x+        x       <- pExp c+        return  $ XCast sp (CastPurify w) x           -- forget <WITNESS> in EXP- , do   pTok KForget+ , do   sp      <- pTokSP KForget         pTok KAngleBra-        w       <- pWitness+        w       <- pWitness c         pTok KAngleKet         pTok KIn-        x       <- pExp-        return  $ XCast () (CastForget w) x+        x       <- pExp c+        return  $ XCast sp (CastForget w) x +        -- suspend EXP+ , do   sp      <- pTokSP KSuspend+        x       <- pExp c+        return  $ XCast sp CastSuspend x++        -- run EXP+ , do   sp      <- pTokSP KRun+        x       <- pExp c+        return  $ XCast sp CastRun x+         -- APP- , do   pExpApp+ , do   pExpApp c  ]   <?> "an expression"   -- Applications.-pExpApp :: Ord n => Parser n (Exp () n)-pExpApp -  = do  x1      <- pExpAtom+pExpApp :: Ord n => Context -> Parser n (Exp SourcePos n)+pExpApp c+  = do  (x1, _)        <- pExpAtomSP c                  P.choice-         [ do   xs  <- liftM concat $ P.many1 pArgs-                return  $ foldl (XApp ()) x1 xs+         [ do   xs  <- liftM concat $ P.many1 (pArgSPs c)+                return  $ foldl (\x (x', sp) -> XApp sp x x') x1 xs           ,      return x1] @@ -175,75 +187,87 @@   -- Comp, Witness or Spec arguments.-pArgs   :: Ord n => Parser n [Exp () n]-pArgs +pArgSPs :: Ord n => Context -> Parser n [(Exp SourcePos n, SourcePos)]+pArgSPs c  = P.choice         -- [TYPE]- [ do   pTok KSquareBra-        t       <- pType + [ do   sp      <- pTokSP KSquareBra+        t       <- pType c         pTok KSquareKet-        return  [XType t]+        return  [(XType t, sp)]          -- [: TYPE0 TYPE0 ... :]- , do   pTok KSquareColonBra-        ts      <- P.many1 pTypeAtom+ , do   sp      <- pTokSP KSquareColonBra+        ts      <- P.many1 (pTypeAtom c)         pTok KSquareColonKet-        return  $ map XType ts+        return  [(XType t, sp) | t <- ts]                  -- <WITNESS>- , do   pTok KAngleBra-        w       <- pWitness+ , do   sp      <- pTokSP KAngleBra+        w       <- pWitness c         pTok KAngleKet-        return  [XWitness w]+        return  [(XWitness w, sp)]                          -- <: WITNESS0 WITNESS0 ... :>- , do   pTok KAngleColonBra-        ws      <- P.many1 pWitnessAtom+ , do   sp      <- pTokSP KAngleColonBra+        ws      <- P.many1 (pWitnessAtom c)         pTok KAngleColonKet-        return  $ map XWitness ws+        return  [(XWitness w, sp) | w <- ws]                          -- EXP0- , do   x       <- pExpAtom-        return  [x]+ , do   (x, sp)  <- pExpAtomSP c+        return  [(x, sp)]  ]  <?> "a type, witness or expression argument"   -- | Parse a variable, constructor or parenthesised expression.-pExpAtom   :: Ord n => Parser n (Exp () n)-pExpAtom +pExpAtom   :: Ord n => Context -> Parser n (Exp SourcePos n)+pExpAtom c+ = do   (x, _) <- pExpAtomSP c+        return x+++-- | Parse a variable, constructor or parenthesised expression,+--   also returning source position.+pExpAtomSP +        :: Ord n +        => Context +        -> Parser n (Exp SourcePos n, SourcePos)++pExpAtomSP c  = P.choice         -- (EXP2)- [ do   pTok KRoundBra-        t       <- pExp+ [ do   sp      <- pTokSP KRoundBra+        t       <- pExp c         pTok KRoundKet-        return  $ t+        return  (t, sp)           -- The unit data constructor.       - , do   pTok KDaConUnit-        return  $ XCon () dcUnit+ , do   sp              <- pTokSP KDaConUnit+        return  (XCon sp dcUnit, sp)          -- Named algebraic constructors.         --  We just fill-in the type with tBot for now, and leave it to          --  the spreader to attach the real type.- , do   con     <- pCon-        return  $ XCon () (mkDaConAlg con (T.tBot T.kData))+ , do   (con, sp)       <- pConSP+        return  (XCon sp (mkDaConAlg con (T.tBot T.kData)), 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     <- pLit-        return  $ XCon () (mkDaConAlg lit (T.tBot T.kData))+ , do   (lit, sp)       <- pLitSP+        return  (XCon sp (mkDaConAlg lit (T.tBot T.kData)), sp)          -- Debruijn indices- , do   i       <- pIndex-        return  $ XVar () (UIx   i)+ , do   (i, sp)         <- pIndexSP+        return  (XVar sp (UIx   i), sp)          -- Variables- , do   var     <- pVar-        return  $ XVar () (UName var) + , do   (var, sp)       <- pVarSP+        return  (XVar sp (UName var), sp)  ]   <?> "a variable, constructor, or parenthesised type"@@ -251,17 +275,18 @@  -- Alternatives --------------------------------------------------------------- -- Case alternatives.-pAlt    :: Ord n => Parser n (Alt () n)-pAlt- = do   p       <- pPat+pAlt    :: Ord n => Context -> Parser n (Alt SourcePos n)+pAlt c+ = do   p       <- pPat c         pTok KArrowDash-        x       <- pExp+        x       <- pExp c         return  $ AAlt p x   -- Patterns.-pPat    :: Ord n => Parser n (Pat n)-pPat+pPat    :: Ord n +        => Context -> Parser n (Pat n)+pPat c  = P.choice  [      -- Wildcard    do   pTok KUnderscore@@ -277,14 +302,16 @@          -- CON BIND BIND ...  , do   nCon    <- pCon -        bs      <- P.many pBindPat+        bs      <- P.many (pBindPat c)         return  $ PData (mkDaConAlg nCon (T.tBot T.kData)) bs]   -- Binds in patterns can have no type annotation, -- or can have an annotation if the whole thing is in parens.-pBindPat :: Ord n => Parser n (Bind n) pBindPat +        :: Ord n +        => Context -> Parser n (Bind n)+pBindPat c  = P.choice         -- Plain binder.  [ do   b       <- pBinder@@ -294,60 +321,65 @@  , do   pTok KRoundBra         b       <- pBinder         pTok KColon-        t       <- pType+        t       <- pType c         pTok KRoundKet         return  $ T.makeBindFromBinder b t  ]   -- Bindings --------------------------------------------------------------------pLets :: Ord n => Parser n (Lets () n)-pLets+pLetsSP :: Ord n +        => Context -> Parser n (Lets SourcePos n, SourcePos)+pLetsSP c  = P.choice     [ -- non-recursive let.-      do pTok KLet-         (mode1, b1, x1) <- pLetBinding-         return  $ LLet mode1 b1 x1+      do sp       <- pTokSP KLet+         (b1, x1) <- pLetBinding c+         return (LLet b1 x1, sp)        -- recursive let.-    , do pTok KLetRec+    , do sp     <- pTokSP KLetRec          P.choice           -- Multiple bindings in braces           [ do   pTok KBraceBra-                 lets    <- P.sepEndBy1 pLetRecBinding (pTok KSemiColon)+                 lets    <- P.sepEndBy1 (pLetRecBinding c) (pTok KSemiColon)                  pTok KBraceKet-                 return $ LRec lets+                 return (LRec lets, sp)            -- A single binding without braces.-          , do   ll      <- pLetRecBinding-                 return  $ LRec [ll]+          , do   ll      <- pLetRecBinding c+                 return (LRec [ll], sp)           ]              -- Local region binding.       --   letregions [BINDER] with { BINDER : TYPE ... } in EXP       --   letregions [BINDER] in EXP-    , do pTok KLetRegions+    , do sp     <- pTokSP KLetRegions          brs    <- P.manyTill pBinder (P.try $ P.lookAhead $ P.choice [pTok KIn, pTok KWith])          let bs =  map (flip T.makeBindFromBinder T.kRegion) brs-         pLetWits bs+         r      <- pLetWits c bs+         return (r, sp)           -    , do pTok KLetRegion+    , do sp     <- pTokSP KLetRegion          br    <- pBinder          let b =  T.makeBindFromBinder br T.kRegion-         pLetWits [b]+         r      <- pLetWits c [b]+         return (r, sp)               ]          -pLetWits :: Ord n => [Bind n] -> Parser n (Lets () n)-pLetWits bs+pLetWits :: Ord n +        => Context -> [Bind n] -> Parser n (Lets SourcePos n)++pLetWits c bs  = P.choice      [ do   pTok KWith            pTok KBraceBra            wits    <- P.sepBy                       (do  b    <- pBinder                            pTok KColon-                           t    <- pTypeApp+                           t    <- pTypeApp c                            return  $ T.makeBindFromBinder b t)                       (pTok KSemiColon)            pTok KBraceKet@@ -358,100 +390,82 @@   -- | A binding for let expression.-pLetBinding :: Ord n => Parser n (LetMode n, Bind n, Exp () n) pLetBinding +        :: Ord n +        => Context+        -> Parser n ( Bind n+                    , Exp SourcePos n)+pLetBinding c  = do   b       <- pBinder          P.choice          [ do   -- Binding with full type signature.                 --  BINDER : TYPE = EXP                 pTok KColon-                t       <- pType-                mode    <- pLetMode+                t       <- pType c                 pTok KEquals-                xBody   <- pExp+                xBody   <- pExp c -                return  $ (mode, T.makeBindFromBinder b t, xBody) +                return  $ (T.makeBindFromBinder b t, xBody)             , do   -- Non-function binding with no type signature.                 -- This form can't be used with letrec as we can't use it                 -- to build the full type sig for the let-bound variable.                 --  BINDER = EXP-                mode    <- pLetMode                 pTok KEquals-                xBody   <- pExp+                xBody   <- pExp c                 let t   = T.tBot T.kData-                return  $ (mode, T.makeBindFromBinder b t, xBody)+                return  $ (T.makeBindFromBinder b t, xBody)            , do   -- Binding using function syntax.                 ps      <- liftM concat -                        $  P.many pBindParamSpec +                        $  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 KColon-                        tBody   <- pType-                        mode    <- pLetMode-                        pTok KEquals-                        xBody   <- pExp+                        tBody   <- pType c+                        sp      <- pTokSP KEquals+                        xBody   <- pExp c -                        let x   = expOfParams () ps xBody-                        let t   = funTypeOfParams ps tBody-                        return  (mode, T.makeBindFromBinder b t, x)+                        let x   = expOfParams sp ps xBody+                        let t   = funTypeOfParams c ps tBody+                        return  (T.makeBindFromBinder b t, x)                          -- Function syntax with no return type.                         -- We can't make the type sig for the let-bound variable,                         -- but we can create lambda abstractions with the given                          -- parameter types.                         --  BINDER PARAM1 PARAM2 .. PARAMN = EXP-                 , do   mode    <- pLetMode-                        pTok KEquals-                        xBody   <- pExp+                 , do   sp      <- pTokSP KEquals+                        xBody   <- pExp c -                        let x   = expOfParams () ps xBody+                        let x   = expOfParams sp ps xBody                         let t   = T.tBot T.kData-                        return  (mode, T.makeBindFromBinder b t, x) ]+                        return  (T.makeBindFromBinder b t, x) ]          ] --- | Parse a let mode specifier.---   Only allow the lazy specifier with non-recursive bindings.---   We don't support value recursion, so the right of all recursive---   bindings must be explicit lambda abstractions anyway, so there's ---   no point suspending them.-pLetMode :: Ord n => Parser n (LetMode n)-pLetMode- = do   P.choice-                -- lazy <WITNESS>-         [ do   pTok KLazy--                P.choice-                 [ do   pTok KAngleBra-                        w       <- pWitness-                        pTok KAngleKet-                        return  $ LetLazy (Just w)-                 -                 , do   return  $ LetLazy Nothing ]--         , do   return  $ LetStrict ]-- -- | Letrec bindings must have a full type signature,  --   or use function syntax with a return type so that we can make one.-pLetRecBinding :: Ord n => Parser n (Bind n, Exp () n) pLetRecBinding +        :: Ord n +        => Context+        -> Parser n (Bind n, Exp SourcePos n)++pLetRecBinding  c  = do   b       <- pBinder          P.choice          [ do   -- Binding with full type signature.                 --  BINDER : TYPE = EXP                 pTok KColon-                t       <- pType+                t       <- pType c                 pTok KEquals-                xBody   <- pExp+                xBody   <- pExp c                  return  $ (T.makeBindFromBinder b t, xBody)  @@ -459,29 +473,29 @@          , do   -- Binding using function syntax.                 --  BINDER PARAM1 PARAM2 .. PARAMN : TYPE = EXP                 ps      <- liftM concat -                        $  P.many pBindParamSpec +                        $  P.many (pBindParamSpec c)                          pTok KColon-                tBody   <- pType-                let t   = funTypeOfParams ps tBody+                tBody   <- pType c+                let t   = funTypeOfParams c ps tBody -                pTok KEquals-                xBody   <- pExp-                let x   = expOfParams () ps xBody+                sp      <- pTokSP KEquals+                xBody   <- pExp c+                let x   = expOfParams sp ps xBody                  return  (T.makeBindFromBinder b t, x) ]   -- Statements ----------------------------------------------------------------- data Stmt n-        = StmtBind  (Bind n) (Exp () n)-        | StmtMatch (Pat n)  (Exp () n) (Exp () n)-        | StmtNone  (Exp () n)+        = StmtBind  SourcePos (Bind n) (Exp SourcePos n)+        | StmtMatch SourcePos (Pat n)  (Exp SourcePos n) (Exp SourcePos n)+        | StmtNone  SourcePos (Exp SourcePos n)   -- | Parse a single statement.-pStmt :: Ord n => Parser n (Stmt n)-pStmt +pStmt :: Ord n => Context -> Parser n (Stmt n)+pStmt c  = P.choice  [ -- BINDER = EXP ;    -- We need the 'try' because a VARIABLE binders can also be parsed@@ -489,57 +503,62 @@    --      P.try $      do  br      <- pBinder-        pTok    KEquals-        x1      <- pExp+        sp      <- pTokSP    KEquals+        x1      <- pExp c         let t   = T.tBot T.kData         let b   = T.makeBindFromBinder br t-        return  $ StmtBind b x1+        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-        pTok KArrowDashLeft-        x1      <- pExp +    do  p       <- pPat c+        sp      <- pTokSP KArrowDashLeft+        x1      <- pExp c         pTok KElse-        x2      <- pExp -        return  $ StmtMatch p x1 x2+        x2      <- pExp c+        return  $ StmtMatch sp p x1 x2          -- EXP- , do   x       <- pExp-        return  $ StmtNone x+ , do   x               <- pExp c++        -- This should always succeed because pExp doesn't+        -- parse plain types or witnesses+        let Just sp     = takeAnnotOfExp x+        +        return  $ StmtNone sp x  ]   -- | Parse some statements.-pStmts :: Ord n => Parser n (Exp () n)-pStmts- = do   stmts   <- P.sepEndBy1 pStmt (pTok KSemiColon)+pStmts :: Ord n => Context -> Parser n (Exp SourcePos n)+pStmts c+ = do   stmts   <- P.sepEndBy1 (pStmt c) (pTok KSemiColon)         case makeStmts stmts of          Nothing -> P.unexpected "do-block must end with a statement"          Just x  -> return x   -- | Make an expression from some statements.-makeStmts :: [Stmt n] -> Maybe (Exp () n)+makeStmts :: [Stmt n] -> Maybe (Exp SourcePos n) makeStmts ss  = case ss of-        [StmtNone x]    +        [StmtNone _ x]              -> Just x -        StmtNone x1 : rest+        StmtNone sp x1 : rest          | Just x2      <- makeStmts rest-         -> Just $ XLet () (LLet LetStrict (BNone (T.tBot T.kData)) x1) x2+         -> Just $ XLet sp (LLet (BNone (T.tBot T.kData)) x1) x2 -        StmtBind b x1 : rest+        StmtBind sp b x1 : rest          | Just x2      <- makeStmts rest-         -> Just $ XLet () (LLet LetStrict b x1) x2+         -> Just $ XLet sp (LLet b x1) x2 -        StmtMatch p x1 x2 : rest+        StmtMatch sp p x1 x2 : rest          | Just x3      <- makeStmts rest-         -> Just $ XCase () x1 +         -> Just $ XCase sp x1                   [ AAlt p x3                  , AAlt PDefault x2] 

@@ -6,6 +6,7 @@ import DDC.Core.Exp import DDC.Core.Parser.Type import DDC.Core.Parser.Exp+import DDC.Core.Parser.Context import DDC.Core.Parser.Base import DDC.Core.Lexer.Tokens import DDC.Core.Compounds@@ -17,9 +18,10 @@ -- Module --------------------------------------------------------------------- -- | Parse a core module. pModule :: (Ord n, Pretty n) -        => Parser n (Module () n)-pModule - = do   pTok KModule+        => Context+        -> Parser n (Module P.SourcePos n)+pModule c+ = do   sp      <- pTokSP KModule         name    <- pModuleName          -- exports { SIG;+ }@@ -27,7 +29,7 @@          <- P.choice             [do pTok KExports                 pTok KBraceBra-                sigs    <- P.sepEndBy1 pTypeSig (pTok KSemiColon)+                sigs    <- P.sepEndBy1 (pTypeSig c) (pTok KSemiColon)                 pTok KBraceKet                 return sigs @@ -38,8 +40,8 @@          <- P.choice             [do pTok KImports                 pTok KBraceBra-                importKinds     <- P.sepEndBy pImportKindSpec (pTok KSemiColon)-                importTypes     <- P.sepEndBy pImportTypeSpec (pTok KSemiColon)+                importKinds     <- P.sepEndBy (pImportKindSpec c) (pTok KSemiColon)+                importTypes     <- P.sepEndBy (pImportTypeSpec c) (pTok KSemiColon)                 pTok KBraceKet                 return (importKinds, importTypes) @@ -51,11 +53,11 @@         pTok KWith          -- LET;+-        lts     <- P.sepBy1 pLets (pTok KIn)+        lts     <- P.sepBy1 (pLetsSP c) (pTok KIn)          -- The body of the module consists of the top-level bindings wrapped         -- around a unit constructor place-holder.-        let body = xLets () lts (xUnit ())+        let body = xLetsAnnot lts (xUnit sp)          -- ISSUE #295: Check for duplicate exported names in module parser.         --  The names are added to a unique map, so later ones with the same@@ -70,20 +72,23 @@   -- | Parse a type signature.-pTypeSig :: Ord n => Parser n (n, Type n)        -pTypeSig+pTypeSig +        :: Ord n +        => Context -> Parser n (n, Type n)        ++pTypeSig c  = do   var     <- pVar         pTok KColonColon-        t       <- pType+        t       <- pType c         return  (var, t)   -- | Parse the type signature of an imported variable. pImportKindSpec          :: (Ord n, Pretty n) -        => Parser n (n, (QualName n, Kind n))+        => Context -> Parser n (n, (QualName n, Kind n)) -pImportKindSpec +pImportKindSpec c  =   pTok KType  >>  P.choice  [      -- Import with an explicit external name.@@ -92,12 +97,12 @@         pTok KWith         n       <- pName         pTok KColonColon-        k       <- pType+        k       <- pType c         return  (n, (qn, k))   , do   n       <- pName         pTok KColonColon-        k       <- pType+        k       <- pType c         return  (n, (QualName (ModuleName []) n, k))  ]         @@ -105,9 +110,9 @@ -- | Parse the type signature of an imported variable. pImportTypeSpec          :: (Ord n, Pretty n) -        => Parser n (n, (QualName n, Type n))+        => Context -> Parser n (n, (QualName n, Type n)) -pImportTypeSpec +pImportTypeSpec c  = P.choice  [      -- Import with an explicit external name.         -- Module.varExternal with varLocal@@ -115,11 +120,11 @@         pTok KWith         n       <- pName         pTok KColonColon-        t       <- pType+        t       <- pType c         return  (n, (qn, t))   , do   n       <- pName         pTok KColonColon-        t       <- pType+        t       <- pType c         return  (n, (QualName (ModuleName []) n, t))  ]        

@@ -7,6 +7,7 @@ where import DDC.Core.Exp import DDC.Core.Parser.Type+import DDC.Core.Parser.Context import DDC.Core.Parser.Base             (Parser) import DDC.Core.Lexer.Tokens import qualified DDC.Base.Parser        as P@@ -22,29 +23,6 @@         | ParamValue   (Bind n) (Type n) (Type n)  --- | Build the type of a function from specifications of its parameters,---   and the type of the body.-funTypeOfParams -        :: [ParamSpec n]        -- ^ Spec of parameters.-        -> Type n               -- ^ Type of body.-        -> Type n               -- ^ Type of whole function.--funTypeOfParams [] tBody        = tBody-funTypeOfParams (p:ps) tBody- = case p of-        ParamType  b    -         -> TForall b -                $ funTypeOfParams ps tBody--        ParamWitness b-         -> T.tImpl (T.typeOfBind b)-                $ funTypeOfParams ps tBody--        ParamValue b eff clo-         -> T.tFun (T.typeOfBind b) eff clo -                $ funTypeOfParams ps tBody-- -- | Build the expression of a function from specifications of its parameters, --   and the expression for the body. expOfParams @@ -66,21 +44,56 @@          -> XLam a b $ expOfParams a ps xBody  +-- | Build the type of a function from specifications of its parameters,+--   and the type of the body.+funTypeOfParams +        :: Context+        -> [ParamSpec n]        -- ^ Spec of parameters.+        -> Type n               -- ^ Type of body.+        -> Type n               -- ^ Type of whole function.++funTypeOfParams _ [] tBody        + = tBody++funTypeOfParams c (p:ps) tBody+ = case p of+        ParamType  b    +         -> TForall b +                $ funTypeOfParams c ps tBody++        ParamWitness b+         -> T.tImpl (T.typeOfBind b)+                $ funTypeOfParams c ps tBody++        ParamValue b eff clo+         | contextFunctionalEffects c+         , contextFunctionalClosures c+         -> T.tFunEC (T.typeOfBind b) eff clo +                $ funTypeOfParams c ps tBody+         +         | otherwise+         -> T.tFun (T.typeOfBind b)+                $ funTypeOfParams c ps tBody++ -- | Parse a parameter specification. -- --       [BIND1 BIND2 .. BINDN : TYPE] --   or  (BIND : TYPE) --   or  (BIND : TYPE) { EFFECT | CLOSURE } ---pBindParamSpec :: Ord n => Parser n [ParamSpec n]-pBindParamSpec+pBindParamSpec +        :: Ord n +        => Context -> Parser n [ParamSpec n]++pBindParamSpec c  = P.choice         -- Type parameter         -- [BIND1 BIND2 .. BINDN : TYPE]  [ do   pTok KSquareBra         bs      <- P.many1 pBinder         pTok KColon-        t       <- pType+        t       <- pType c         pTok KSquareKet         return  [ ParamType b                  | b <- zipWith T.makeBindFromBinder bs (repeat t)]@@ -91,7 +104,7 @@  , do   pTok KAngleBra         b       <- pBinder         pTok KColon-        t       <- pType+        t       <- pType c         pTok KAngleKet         return  [ ParamWitness $ T.makeBindFromBinder b t] @@ -101,15 +114,15 @@  , do   pTok KRoundBra         b       <- pBinder         pTok KColon-        t       <- pType+        t       <- pType c         pTok KRoundKet          (eff, clo)           <- P.choice                 [ do    pTok KBraceBra-                        eff'    <- pType+                        eff'    <- pType c                         pTok KBar-                        clo'    <- pType+                        clo'    <- pType c                         pTok KBraceKet                         return  (eff', clo')                 @@ -118,5 +131,4 @@          return  $ [ParamValue (T.makeBindFromBinder b t) eff clo]  ]- 

@@ -9,6 +9,7 @@         , pTok         , pTokAs) where+import DDC.Core.Parser.Context import DDC.Core.Parser.Base import DDC.Core.Lexer.Tokens    import DDC.Type.Exp@@ -19,20 +20,25 @@   -- | Parse a type.-pType   :: Ord n => Parser n (Type n)-pType   = pTypeSum+pType   :: Ord n +        => Context -> Parser n (Type n)++pType c  + =      pTypeSum c  <?> "a type"   --  | Parse a type sum.-pTypeSum :: Ord n => Parser n (Type n) pTypeSum - = do   t1      <- pTypeForall+        :: Ord n +        => Context -> Parser n (Type n)+pTypeSum c+ = do   t1      <- pTypeForall c         P.choice           [ -- Type sums.            -- T2 + T3            do   pTok KPlus-                t2      <- pTypeSum+                t2      <- pTypeSum c                 return  $ TSum $ TS.fromList (tBot sComp) [t1, t2]                           , do   return t1 ]@@ -55,60 +61,69 @@         , do    pTok KUnderscore                 return  $ RNone ]  <?> "a binder"-   ++ -- | Parse a quantified type.-pTypeForall :: Ord n => Parser n (Type n)-pTypeForall+pTypeForall +        :: Ord n +        => Context -> Parser n (Type n)+pTypeForall c  = P.choice          [ -- Universal quantification.            -- [v1 v1 ... vn : T1]. T2            do   pTok KSquareBra                 bs      <- P.many1 pBinder                 pTok KColon-                k       <- pTypeSum+                k       <- pTypeSum c                 pTok KSquareKet                 pTok KDot -                body    <- pTypeForall+                body    <- pTypeForall c                  return  $ foldr TForall body                          $ map (\b -> makeBindFromBinder b k) bs             -- Body type-         , do   pTypeFun]+         , do   pTypeFun c]  <?> "a type"   -- | Parse a function type.-pTypeFun :: Ord n => Parser n (Type n)-pTypeFun- = do   t1      <- pTypeApp+pTypeFun +        :: Ord n +        => Context -> Parser n (Type n)++pTypeFun c+ = do   t1      <- pTypeApp c         P.choice           [ -- T1 ~> T2            do   pTok KArrowTilde-                t2      <- pTypeFun+                t2      <- pTypeFun c                 return  $ TApp (TApp (TCon (TyConKind KiConFun)) t1) t2             -- T1 => T2          , do   pTok KArrowEquals-                t2      <- pTypeFun+                t2      <- pTypeFun c                 return  $ TApp (TApp (TCon (TyConWitness TwConImpl)) t1) t2             -- T1 -> T2          , do   pTok KArrowDash-                t2      <- pTypeFun-                return  $ t1 `tFunPE` t2+                t2      <- pTypeFun c+                if (  contextFunctionalEffects c+                   && contextFunctionalClosures c)+                   then return $ t1 `tFunPE` t2+                   else return $ t1 `tFun`   t2             -- T1 -(TSUM | TSUM)> t2          , do   pTok KDash                 pTok KRoundBra-                eff     <- pTypeSum+                eff     <- pTypeSum c                 pTok KBar-                clo     <- pTypeSum+                clo     <- pTypeSum c                 pTok KRoundKet                 pTok KAngleKet-                t2      <- pTypeFun-                return  $ tFun t1 eff clo t2+                t2      <- pTypeFun c+                return  $ tFunEC t1 eff clo t2              -- Body type@@ -117,16 +132,20 @@   -- | Parse a type application.-pTypeApp :: Ord n => Parser n (Type n)-pTypeApp  - = do   (t:ts)  <- P.many1 pTypeAtom+pTypeApp +        :: Ord n +        => Context -> Parser n (Type n)+pTypeApp c+ = do   (t:ts)  <- P.many1 (pTypeAtom c)         return  $  foldl TApp t ts  <?> "an atomic type or type application"   -- | Parse a variable, constructor or parenthesised type.-pTypeAtom :: Ord n => Parser n (Type n)-pTypeAtom  +pTypeAtom +        :: Ord n +        => Context -> Parser n (Type n)+pTypeAtom c  = P.choice         -- (~>) and (=>) and (->) and (TYPE2)         [ do    pTok KRoundBra@@ -141,14 +160,27 @@                   , do   pTok KArrowDash                         pTok KRoundKet-                        return (TCon $ TyConSpec TcConFun) -                 , do   t       <- pTypeSum+                        -- Decide what type constructor to use for the (->) token.+                        -- Only use the function constructor with latent effects+                        -- and closures if the language fragment supports both.+                        if (  contextFunctionalEffects  c +                           && contextFunctionalClosures c)+                         then return (TCon $ TyConSpec TcConFunEC)+                         else return (TCon $ TyConSpec TcConFun)++                 , do   t       <- pTypeSum c                         pTok KRoundKet                         return t                   ]          -- Named type constructors+        , do    so      <- pSoCon+                return  $ TCon (TyConSort so)++        , do    ki      <- pKiCon+                return  $ TCon (TyConKind ki)+         , do    tc      <- pTcCon                 return  $ TCon (TyConSpec tc) @@ -157,15 +189,6 @@          , do    tc      <- pTyConNamed                 return  $ TCon tc--        -- Symbolic constructors.-        , do    pTokAs KSortComp    (TCon $ TyConSort SoConComp)-        , do    pTokAs KSortProp    (TCon $ TyConSort SoConProp) -        , do    pTokAs KKindValue   (TCon $ TyConKind KiConData)-        , do    pTokAs KKindRegion  (TCon $ TyConKind KiConRegion) -        , do    pTokAs KKindEffect  (TCon $ TyConKind KiConEffect) -        , do    pTokAs KKindClosure (TCon $ TyConKind KiConClosure) -        , do    pTokAs KKindWitness (TCon $ TyConKind KiConWitness)                       -- Bottoms.         , do    pTokAs KBotEffect  (tBot kEffect)@@ -185,21 +208,39 @@   ---------------------------------------------------------------------------------- | Parse a builtin `TcCon`+-- | Parse a builtin sort constructor.+pSoCon :: Parser n SoCon+pSoCon  =   P.pTokMaybe f+        <?> "a sort constructor"+ where f (KA (KSoConBuiltin c)) = Just c+       f _                      = Nothing +++-- | Parse a builtin kind constructor.+pKiCon :: Parser n KiCon+pKiCon  =   P.pTokMaybe f+        <?> "a kind constructor"+ where f (KA (KKiConBuiltin c)) = Just c+       f _                      = Nothing +++-- | Parse a builtin type constructor. pTcCon :: Parser n TcCon pTcCon  =   P.pTokMaybe f         <?> "a type constructor"  where f (KA (KTcConBuiltin c)) = Just c        f _                      = Nothing  --- | Parse a builtin `TwCon`++-- | Parse a builtin witness type constructor. pTwCon :: Parser n TwCon pTwCon  =   P.pTokMaybe f         <?> "a witness constructor"  where f (KA (KTwConBuiltin c)) = Just c        f _                      = Nothing --- | Parse a user `TcCon`++-- | Parse a user defined type constructor. pTyConNamed :: Parser n (TyCon n) pTyConNamed           =   P.pTokMaybe f

@@ -5,80 +5,109 @@         , pWitnessAtom)  where import DDC.Core.Parser.Type+import DDC.Core.Parser.Context import DDC.Core.Parser.Base import DDC.Core.Lexer.Tokens import DDC.Core.Exp-import DDC.Base.Parser                  ((<?>))+import DDC.Base.Parser                  ((<?>), SourcePos) import qualified DDC.Base.Parser        as P import qualified DDC.Type.Compounds     as T- +import Control.Monad  + -- | Parse a witness expression.-pWitness :: Ord n  => Parser n (Witness n)-pWitness = pWitnessJoin+pWitness +        :: Ord n  +        => Context -> Parser n (Witness SourcePos n)+pWitness c = pWitnessJoin c   -- | Parse a witness join.-pWitnessJoin :: Ord n => Parser n (Witness n) pWitnessJoin +        :: Ord n +        => Context -> Parser n (Witness SourcePos n)+pWitnessJoin c    -- WITNESS  or  WITNESS & WITNESS- = do   w1      <- pWitnessApp+ = do   w1      <- pWitnessApp c         P.choice -         [ do   pTok KAmpersand-                w2      <- pWitnessJoin-                return  (WJoin w1 w2)+         [ do   sp      <- pTokSP KAmpersand+                w2      <- pWitnessJoin c+                return  (WJoin sp w1 w2)           , do   return w1 ]   -- | Parse a witness application.-pWitnessApp :: Ord n => Parser n (Witness n) pWitnessApp -  = do  (x:xs)  <- P.many1 pWitnessArg-        return  $ foldl WApp x xs+        :: Ord n +        => Context -> Parser n (Witness SourcePos n) +pWitnessApp c+  = do  (x:xs)  <- P.many1 (pWitnessArgSP c)+        let x'  = fst x+        let sp  = snd x+        let xs' = map fst xs+        return  $ foldl (WApp sp) x' xs'+  <?> "a witness expression or application"   -- | Parse a witness argument.-pWitnessArg :: Ord n => Parser n (Witness n)-pWitnessArg +pWitnessArgSP +        :: Ord n +        => Context -> Parser n (Witness SourcePos n, SourcePos)++pWitnessArgSP c  = P.choice  [ -- [TYPE]-   do   pTok KSquareBra-        t       <- pType+   do   sp      <- pTokSP KSquareBra+        t       <- pType c         pTok KSquareKet-        return  $ WType t+        return  (WType sp t, sp)     -- WITNESS- , do   pWitnessAtom ]+ , do   pWitnessAtomSP c ]  + -- | Parse a variable, constructor or parenthesised witness.-pWitnessAtom :: Ord n => Parser n (Witness n)-pWitnessAtom +pWitnessAtom   +        :: Ord n +        => Context -> Parser n (Witness SourcePos n)++pWitnessAtom c   +        = liftM fst (pWitnessAtomSP c)+++-- | Parse a variable, constructor or parenthesised witness,+--   also returning source position.+pWitnessAtomSP +        :: Ord n +        => Context -> Parser n (Witness SourcePos n, SourcePos)++pWitnessAtomSP c  = P.choice    -- (WITNESS)- [ do    pTok KRoundBra-         w       <- pWitness-         pTok KRoundKet-         return  $ w+ [ do   sp      <- pTokSP KRoundBra+        w       <- pWitness c+        pTok KRoundKet+        return  (w, sp)     -- Named constructors- , do   con     <- pCon-        return  $ WCon (WiConBound (UName con) (T.tBot T.kWitness))+ , do   (con, sp) <- pConSP+        return  (WCon sp (WiConBound (UName con) (T.tBot T.kWitness)), sp)     -- Baked-in witness constructors.- , do    wb     <- pWbCon-         return $ WCon (WiConBuiltin wb)+ , do   (wb, sp) <- pWbConSP+        return  (WCon sp (WiConBuiltin wb), sp)                      -- Debruijn indices- , do    i       <- pIndex-         return  $ WVar (UIx   i)+ , do   (i, sp) <- pIndexSP+        return  (WVar sp (UIx   i), sp)     -- Variables- , do    var     <- pVar-         return  $ WVar (UName var) ]+ , do   (var, sp) <- pVarSP+        return  (WVar sp (UName var), sp) ]   <?> "a witness"

@@ -14,6 +14,9 @@           -- * Applications         , isXApp +          -- * Let bindings+        , isXLet+           -- * Types and Witnesses         , isXType         , isXWitness@@ -55,7 +58,7 @@   -- | Check whether a witness is a `WVar` or `WCon`.-isAtomW :: Witness n -> Bool+isAtomW :: Witness a n -> Bool isAtomW ww  = case ww of         WVar{}          -> True@@ -94,6 +97,14 @@         XApp{}  -> True         _       -> False ++-- Let Bindings ---------------------------------------------------------------+isXLet :: Exp a n -> Bool+isXLet xx+ = case xx of+        XLet{}  -> True+        _       -> False+          -- Type and Witness ----------------------------------------------------------- -- | Check whether an expression is an `XType`

@@ -120,6 +120,14 @@          $   ppr lts <+> text "in"          <$> ppr x +        XCase _ x1 [AAlt p x2]+         ->  pprParen' (d > 2)+         $   text "caselet" <+> ppr p +                <+> nest 2 (breakWhen (not $ isSimpleX x1)+                            <> text "=" <+> align (ppr x1))+                <+> text "in"+         <$> ppr x2+         XCase _ x alts          -> pprParen' (d > 2)           $  (nest 2 $ text "case" <+> ppr x <+> text "of" <+> lbrace <> line@@ -127,6 +135,14 @@          <> line           <> rbrace +        XCast _ CastSuspend x+         -> pprParen' (d > 2)+         $  text "suspend" <$> ppr x++        XCast _ CastRun x+         -> pprParen' (d > 2)+         $  text "run"     <+> ppr x+         XCast _ cc x          ->  pprParen' (d > 2)          $   ppr cc <+> text "in"@@ -184,17 +200,23 @@         CastForget w          -> text "forget"  <+> angles   (ppr w) +        CastSuspend+         -> text "suspend" +        CastRun+         -> text "run"++ -- Lets ----------------------------------------------------------------------- instance (Pretty n, Eq n) => Pretty (Lets a n) where  ppr lts   = case lts of-        LLet m b x+        LLet b x          -> let dBind = if isBot (typeOfBind b)                           then ppr (binderOfBind b)                           else ppr b             in  text "let"-                 <+> align (  dBind <> ppr m+                 <+> align (  dBind                            <> nest 2 ( breakWhen (not $ isSimpleX x)                                      <> text "=" <+> align (ppr x))) @@ -239,28 +261,20 @@                 <+> ppr b  -instance (Pretty n, Eq n) => Pretty (LetMode n) where- ppr lm-  = case lm of-        LetStrict        -> empty-        LetLazy Nothing  -> text " lazy"-        LetLazy (Just w) -> text " lazy <" <> ppr w <> text ">"-- -- Witness ---------------------------------------------------------------------instance (Pretty n, Eq n) => Pretty (Witness n) where+instance (Pretty n, Eq n) => Pretty (Witness a n) where  pprPrec d ww   = case ww of-        WVar n          -> ppr n-        WCon wc         -> ppr wc+        WVar _ n         -> ppr n+        WCon _ wc        -> ppr wc -        WApp w1 w2+        WApp _ w1 w2          -> pprParen (d > 10) (ppr w1 <+> pprPrec 11 w2)          -        WJoin w1 w2+        WJoin _ w1 w2          -> pprParen (d > 9)  (ppr w1 <+> text "&" <+> ppr w2) -        WType t         -> text "[" <> ppr t <> text "]"+        WType _ t        -> text "[" <> ppr t <> text "]"   instance (Pretty n, Eq n) => Pretty (WiCon n) where

@@ -0,0 +1,92 @@++module DDC.Core.Transform.Annotate+        (Annotate (..))+where+import qualified DDC.Core.Exp.Annot     as A+import qualified DDC.Core.Exp.Simple    as S+++-- | Convert the `Simple` version of the AST to the `Annot` version,+--   using a the provided default annotation value.+class Annotate  +        (c1 :: * -> * -> *) +        (c2 :: * -> * -> *) | c1 -> c2 + where+ annotate :: a -> c1 a n -> c2 a n+++instance Annotate S.Exp A.Exp where+ annotate def xx+  = let down     = annotate def+    in case xx of+        S.XAnnot _ (S.XAnnot a x)       -> down (S.XAnnot a x)+        S.XAnnot a (S.XVar   u)         -> A.XVar      a u+        S.XAnnot a (S.XCon   dc)        -> A.XCon      a dc+        S.XAnnot a (S.XLAM   b x)       -> A.XLAM      a b   (down x)+        S.XAnnot a (S.XLam   b x)       -> A.XLam      a b   (down x)+        S.XAnnot a (S.XApp   x1 x2)     -> A.XApp      a     (down x1)  (down x2)+        S.XAnnot a (S.XLet   lts x)     -> A.XLet      a     (down lts) (down x)+        S.XAnnot a (S.XCase  x alts)    -> A.XCase     a     (down x)   (map down alts)+        S.XAnnot a (S.XCast  c x)       -> A.XCast     a     (down c)   (down x)+        S.XAnnot _ (S.XType    t)       -> A.XType     t+        S.XAnnot _ (S.XWitness w)       -> A.XWitness  (down w)++        S.XVar  u                       -> A.XVar      def u+        S.XCon  dc                      -> A.XCon      def dc+        S.XLAM  b x                     -> A.XLAM      def b (down x)+        S.XLam  b x                     -> A.XLam      def b (down x)+        S.XApp  x1 x2                   -> A.XApp      def   (down x1)  (down x2)+        S.XLet  lts x                   -> A.XLet      def   (down lts) (down x)+        S.XCase x alts                  -> A.XCase     def   (down x)   (map down alts)+        S.XCast c x                     -> A.XCast     def   (down c)   (down x)+        S.XType t                       -> A.XType     t+        S.XWitness w                    -> A.XWitness  (down w)+++instance Annotate S.Cast A.Cast where+ annotate def cc+  = let down    = annotate def+    in case cc of+        S.CastWeakenEffect eff          -> A.CastWeakenEffect  eff+        S.CastWeakenClosure clo         -> A.CastWeakenClosure (map down clo)+        S.CastPurify w                  -> A.CastPurify        (down w)+        S.CastForget w                  -> A.CastForget        (down w)+        S.CastSuspend                   -> A.CastSuspend+        S.CastRun                       -> A.CastRun+++instance Annotate S.Lets A.Lets where+ annotate def lts+  = let down    = annotate def+    in case lts of+        S.LLet b x                      -> A.LLet b (down x)+        S.LRec bxs                      -> A.LRec [(b, down x) | (b, x) <- bxs]+        S.LLetRegions bks bts           -> A.LLetRegions bks bts+        S.LWithRegion u                 -> A.LWithRegion u+++instance Annotate S.Alt A.Alt where+ annotate def alt+  = let down    = annotate def+    in case alt of+        S.AAlt w x                      -> A.AAlt w (down x)+++instance Annotate S.Witness A.Witness where+ annotate def wit+  = let down    = annotate def+    in case wit of+        S.WAnnot _ (S.WAnnot a x)       -> down (S.WAnnot a x)+        S.WAnnot a (S.WVar  u)          -> A.WVar  a u+        S.WAnnot a (S.WCon  wc)         -> A.WCon  a wc+        S.WAnnot a (S.WApp  w1 w2)      -> A.WApp  a (down w1) (down w2)+        S.WAnnot a (S.WJoin w1 w2)      -> A.WJoin a (down w1) (down w2)+        S.WAnnot a (S.WType t)          -> A.WType a t++        S.WVar  u                       -> A.WVar  def u+        S.WCon  dc                      -> A.WCon  def dc        +        S.WApp  x1 x2                   -> A.WApp  def (down x1) (down x2)+        S.WJoin x1 x2                   -> A.WJoin def (down x1) (down x2)+        S.WType t                       -> A.WType def t++

@@ -0,0 +1,78 @@++module DDC.Core.Transform.Deannotate+        (Deannotate(..))+where+import qualified DDC.Core.Exp.Annot     as A+import qualified DDC.Core.Exp.Simple    as S+++-- | Convert the `Annot` version of the AST to the `Simple` version,+--   using the provided function to decide when to keep the annotation.+class Deannotate +        (c1 :: * -> * -> *)+        (c2 :: * -> * -> *) | c1 -> c2+ where  + deannotate :: (a -> Maybe a) -> c1 a n -> c2 a n+++instance Deannotate A.Exp S.Exp where+ deannotate f xx+  = let down      = deannotate f +        wrap a x  = case f a of+                        Nothing -> x+                        Just a' -> S.XAnnot a' x+    in case xx of+        A.XVar  a u             -> wrap a (S.XVar u)+        A.XCon  a dc            -> wrap a (S.XCon dc)+        A.XLAM  a b x           -> wrap a (S.XLAM b (down x))+        A.XLam  a b x           -> wrap a (S.XLam b (down x))+        A.XApp  a x1 x2         -> wrap a (S.XApp   (down x1)  (down x2))+        A.XLet  a lts x2        -> wrap a (S.XLet   (down lts) (down x2))+        A.XCase a x alts        -> wrap a (S.XCase  (down x)   (map down alts))+        A.XCast a cc x          -> wrap a (S.XCast  (down cc)  (down x))+        A.XType t               -> S.XType t+        A.XWitness w            -> S.XWitness (down w)+++instance Deannotate A.Lets S.Lets where+ deannotate f lts+  = let down    = deannotate f+    in case lts of+        A.LLet b x              -> S.LLet b (down x)+        A.LRec bxs              -> S.LRec [(b, down x) | (b, x) <- bxs]+        A.LLetRegions bks bts   -> S.LLetRegions bks bts+        A.LWithRegion u         -> S.LWithRegion u+++instance Deannotate A.Alt S.Alt where+ deannotate f aa+  = case aa of+        A.AAlt w x              -> S.AAlt w (deannotate f x)+++instance Deannotate A.Witness S.Witness where+ deannotate f ww+  = let down     = deannotate f+        wrap a x = case f a of+                        Nothing -> x+                        Just a' -> S.WAnnot a' x+    in case ww of+        A.WVar  a u             -> wrap a (S.WVar u)+        A.WCon  a wc            -> wrap a (S.WCon wc)+        A.WApp  a w1 w2         -> wrap a (S.WApp  (down w1) (down w2))+        A.WJoin a w1 w2         -> wrap a (S.WJoin (down w1) (down w2))+        A.WType a t             -> wrap a (S.WType t)+++instance Deannotate A.Cast S.Cast where+ deannotate f cc+  = let down    = deannotate f+    in case cc of+        A.CastWeakenEffect e    -> S.CastWeakenEffect e+        A.CastWeakenClosure xs  -> S.CastWeakenClosure (map down xs)+        A.CastPurify w          -> S.CastPurify (down w)+        A.CastForget w          -> S.CastForget (down w)+        A.CastSuspend           -> S.CastSuspend+        A.CastRun               -> S.CastRun++

@@ -11,67 +11,51 @@  mapBoundAtDepthT f d xx   = let down = mapBoundAtDepthT f d     in case xx of-        XVar a u        -> XVar a   u-        XCon{}          -> xx-        XApp a x1 x2    -> XApp a   (down x1) (down x2)-        XLAM a b x      -> XLAM a b (mapBoundAtDepthT f (d + countBAnons [b]) x)-        XLam a b x      -> XLam a   (down b) (down x)+        XVar a u                -> XVar a   u+        XCon{}                  -> xx+        XApp a x1 x2            -> XApp a   (down x1) (down x2)+        XLAM a b x              -> XLAM a b (mapBoundAtDepthT f (d + countBAnons [b]) x)+        XLam a b x              -> XLam a   (down b) (down x)                   XLet a lets x             -> let (lets', levels) = mapBoundAtDepthTLets f d lets              in  XLet a lets' (mapBoundAtDepthT f (d + levels) x) -        XCase a x alts  -> XCase a  (down x)  (map down alts)-        XCast a cc x    -> XCast a  (down cc) (down x)-        XType    t      -> XType    (down t)-        XWitness w      -> XWitness (down w)---instance Ord n => MapBoundT LetMode n where- mapBoundAtDepthT f d m-  = case m of-        LetStrict        -> m-        LetLazy Nothing  -> m-        LetLazy (Just w) -> LetLazy (Just $ mapBoundAtDepthT f d w)+        XCase a x alts          -> XCase a  (down x)  (map down alts)+        XCast a cc x            -> XCast a  (down cc) (down x)+        XType    t              -> XType    (down t)+        XWitness w              -> XWitness (down w)           -instance Ord n => MapBoundT Witness n where+instance Ord n => MapBoundT (Witness a) n where  mapBoundAtDepthT f d ww   = let down = mapBoundAtDepthT f d     in case ww of-        WVar u         -> WVar  (down u)-        WCon _         -> ww-        WApp  w1 w2    -> WApp  (down w1) (down w2)-        WJoin w1 w2    -> WJoin (down w1) (down w2)-        WType t        -> WType (down t)+        WVar  a u               -> WVar  a (down u)+        WCon  _ _               -> ww+        WApp  a w1 w2           -> WApp  a (down w1) (down w2)+        WJoin a w1 w2           -> WJoin a (down w1) (down w2)+        WType a t               -> WType a (down t)   instance Ord n => MapBoundT (Cast a) n where  mapBoundAtDepthT f d cc   = let down = mapBoundAtDepthT f d     in case cc of-        CastWeakenEffect t -         -> CastWeakenEffect  (down t)--        CastWeakenClosure xs    -         -> CastWeakenClosure (map down xs)--        CastPurify w-         -> CastPurify (down w)--        CastForget w-         -> CastForget (down w)+        CastWeakenEffect t      -> CastWeakenEffect  (down t)+        CastWeakenClosure xs    -> CastWeakenClosure (map down xs)+        CastPurify w            -> CastPurify (down w)+        CastForget w            -> CastForget (down w)+        CastSuspend             -> CastSuspend+        CastRun                 -> CastRun   instance Ord n => MapBoundT (Alt a) n where  mapBoundAtDepthT f d (AAlt p x)   = let down = mapBoundAtDepthT f d     in case p of-        PDefault -         -> AAlt PDefault (down x)--        PData dc bs-         -> AAlt (PData dc (map down bs)) (down x) +        PDefault                -> AAlt PDefault (down x)+        PData dc bs             -> AAlt (PData dc (map down bs)) (down x)           mapBoundAtDepthTLets@@ -84,8 +68,8 @@ mapBoundAtDepthTLets f d lts  = let down = mapBoundAtDepthT f d    in case lts of-        LLet m b x-         ->     ( LLet (down m) (down b) (down x)+        LLet b x+         ->     ( LLet (down b) (down x)                 , 0)          LRec bs

@@ -102,39 +102,30 @@         XWitness w	-> XWitness (down w)  -instance MapBoundX LetMode n where- mapBoundAtDepthX f d m-  = case m of-        LetStrict        -> m-        LetLazy Nothing  -> m-        LetLazy (Just w) -> LetLazy (Just $ mapBoundAtDepthX f d w)--         -instance MapBoundX Witness n where+instance MapBoundX (Witness a) n where  mapBoundAtDepthX f d ww   = let down = mapBoundAtDepthX f d     in case ww of-        WVar u         -> WVar  (down u)-	WCon _         -> ww-	WApp  w1 w2    -> WApp  (down w1) (down w2)-	WJoin w1 w2    -> WJoin (down w1) (down w2)-	WType _        -> ww+        WVar  a u       -> WVar  a (down u)+	WCon  _ _       -> ww+	WApp  a w1 w2   -> WApp  a (down w1) (down w2)+	WJoin a w1 w2   -> WJoin a (down w1) (down w2)+	WType _ _       -> ww   instance MapBoundX (Cast a) n where  mapBoundAtDepthX f d cc   = case cc of-        CastWeakenEffect{}+        CastWeakenEffect{}                -> cc          CastWeakenClosure xs              -> CastWeakenClosure (map (mapBoundAtDepthX f d) xs) -        CastPurify w-         -> CastPurify w--        CastForget w-         -> CastForget w+        CastPurify w    -> CastPurify w+        CastForget w    -> CastForget w+        CastSuspend     -> CastSuspend+        CastRun         -> CastRun   instance MapBoundX (Alt a) n where@@ -156,13 +147,12 @@  mapBoundAtDepthXLets f d lts  = case lts of-        LLet m b x+        LLet b x          -> let inc = countBAnons [b]-                m'  = mapBoundAtDepthX f d m-+                 		-- non-recursive binding: do not increase x's depth                 x'  = mapBoundAtDepthX f d x-            in  (LLet m' b x', inc)+            in  (LLet b x', inc)          LRec bs          -> let inc = countBAnons (map fst bs)

@@ -25,35 +25,34 @@  instance Reannotate Exp where  reannotate f xx-  = {-# SCC reannotate #-}-    let down x   = reannotate f x+  = let down x   = reannotate f x     in case xx of-        XVar  a u       -> XVar  (f a) u-        XCon  a u       -> XCon  (f a) u-        XLAM  a b x     -> XLAM  (f a) b (down x)-        XLam  a b x     -> XLam  (f a) b (down x)-        XApp  a x1 x2   -> XApp  (f a) (down x1)  (down x2)-        XLet  a lts x   -> XLet  (f a) (down lts) (down x)-        XCase a x alts  -> XCase (f a) (down x)   (map down alts)-        XCast a c x     -> XCast (f a) (down c)   (down x)-        XType t         -> XType t-        XWitness w      -> XWitness w+        XVar  a u               -> XVar  (f a) u+        XCon  a u               -> XCon  (f a) u+        XLAM  a b x             -> XLAM  (f a) b (down x)+        XLam  a b x             -> XLam  (f a) b (down x)+        XApp  a x1 x2           -> XApp  (f a)   (down x1)  (down x2)+        XLet  a lts x           -> XLet  (f a)   (down lts) (down x)+        XCase a x alts          -> XCase (f a)   (down x)   (map down alts)+        XCast a c x             -> XCast (f a)   (down c)   (down x)+        XType t                 -> XType t+        XWitness w              -> XWitness (down w)   instance Reannotate Lets where  reannotate f xx   = let down x  = reannotate f x     in case xx of-        LLet m b x       -> LLet m b (down x)-        LRec bxs         -> LRec [(b, down x) | (b, x) <- bxs]-        LLetRegions b bs -> LLetRegions b bs-        LWithRegion b    -> LWithRegion b+        LLet b x                -> LLet b (down x)+        LRec bxs                -> LRec [(b, down x) | (b, x) <- bxs]+        LLetRegions b bs        -> LLetRegions b bs+        LWithRegion b           -> LWithRegion b   instance Reannotate Alt where  reannotate f aa   = case aa of-        AAlt w x        -> AAlt w (reannotate f x)+        AAlt w x                -> AAlt w (reannotate f x)   instance Reannotate Cast where@@ -62,7 +61,19 @@     in case cc of         CastWeakenEffect  eff   -> CastWeakenEffect eff         CastWeakenClosure xs    -> CastWeakenClosure (map down xs)-        CastPurify w            -> CastPurify w-        CastForget w            -> CastForget w+        CastPurify w            -> CastPurify (down w)+        CastForget w            -> CastForget (down w)+        CastSuspend             -> CastSuspend+        CastRun                 -> CastRun ++instance Reannotate Witness where+ reannotate f ww+  = let down x = reannotate f x+    in case ww of+        WVar  a u               -> WVar  (f a) u+        WCon  a c               -> WCon  (f a) c+        WApp  a w1 w2           -> WApp  (f a) (down w1) (down w2)+        WJoin a w1 w2           -> WJoin (f a) (down w1) (down w2)+        WType a t               -> WType (f a) t 

@@ -21,21 +21,13 @@ import DDC.Type.Transform.Rename  -instance Rename LetMode where- renameWith sub lm-  = case lm of-        LetStrict        -> lm-        LetLazy (Just t) -> LetLazy (Just $ renameWith sub t) -        LetLazy Nothing  -> LetLazy Nothing---instance Rename Witness where+instance Rename (Witness a) where  renameWith sub ww   = let down x   = renameWith x     in case ww of-        WVar u          -> WVar  (use0 sub u)-        WCon{}          -> ww-        WApp  w1 w2     -> WApp  (down sub w1) (down sub w2)-        WJoin w1 w2     -> WJoin (down sub w1) (down sub w2)-        WType t         -> WType (down sub t)+        WVar  a u       -> WVar  a (use0 sub u)+        WCon  a c       -> WCon  a c+        WApp  a w1 w2   -> WApp  a (down sub w1) (down sub w2)+        WJoin a w1 w2   -> WJoin a (down sub w1) (down sub w2)+        WType a t       -> WType a (down sub t) 

@@ -10,6 +10,7 @@ import qualified DDC.Type.Env           as Env import qualified Data.Map               as Map + class SpreadX (c :: * -> *) where   -- | Spread type annotations from binders and the environment into bound@@ -90,6 +91,8 @@         CastWeakenClosure xs    -> CastWeakenClosure (map down xs)         CastPurify w            -> CastPurify        (down w)         CastForget w            -> CastForget        (down w)+        CastSuspend             -> CastSuspend+        CastRun                 -> CastRun   instance SpreadX Pat where@@ -113,7 +116,8 @@  spreadX kenv tenv lts   = let down x = spreadX kenv tenv x     in case lts of-        LLet m b x       -> LLet (down m) (down b) (down x)+        LLet b x         +         -> LLet (down b) (down x)                  LRec bxs          -> let (bs, xs) = unzip bxs@@ -132,23 +136,15 @@          -> LWithRegion (spreadX kenv tenv b)  -instance SpreadX LetMode where- spreadX kenv tenv lm-  = case lm of-        LetStrict        -> LetStrict-        LetLazy Nothing  -> LetLazy Nothing-        LetLazy (Just w) -> LetLazy (Just $ spreadX kenv tenv w)---instance SpreadX Witness where+instance SpreadX (Witness a) where  spreadX kenv tenv ww   = let down = spreadX kenv tenv      in case ww of-        WCon  wc         -> WCon  (down wc)-        WVar  u          -> WVar  (down u)-        WApp  w1 w2      -> WApp  (down w1) (down w2)-        WJoin w1 w2      -> WJoin (down w1) (down w2)-        WType t1         -> WType (spreadT kenv t1)+        WCon  a wc       -> WCon  a (down wc)+        WVar  a u        -> WVar  a (down u)+        WApp  a w1 w2    -> WApp  a (down w1) (down w2)+        WJoin a w1 w2    -> WJoin a (down w1) (down w2)+        WType a t1       -> WType a (spreadT kenv t1)   instance SpreadX WiCon where

@@ -82,12 +82,11 @@                 x'              = down  sub1 x             in  XLam a b' x' -        XLet a (LLet m b x1) x2-         -> let m'              = down  sub  m-                x1'             = down  sub  x1+        XLet a (LLet b x1) x2+         -> let x1'             = down  sub  x1                 (sub1, b')      = bind0 sub  (down sub b)                 x2'             = down  sub1 x2-            in  XLet a (LLet m' b' x1') x2'+            in  XLet a (LLet b' x1') x2'          XLet a (LRec bxs) x2          -> let (bs, xs)        = unzip  bxs@@ -111,15 +110,6 @@         XWitness w      -> XWitness (down sub w)  -instance SubstituteTX LetMode where- substituteWithTX tArg sub lm-  = let down x   = substituteWithTX tArg x-    in case lm of-        LetStrict         -> lm-        LetLazy Nothing   -> lm-        LetLazy (Just w)  -> LetLazy (Just $ down sub w)-- instance SubstituteTX (Alt a) where  substituteWithTX tArg sub aa   = let down x = substituteWithTX tArg x@@ -141,17 +131,19 @@         CastWeakenClosure clo   -> CastWeakenClosure (map (down sub) clo)         CastPurify w            -> CastPurify        (down sub w)         CastForget w            -> CastForget        (down sub w)+        CastSuspend             -> CastSuspend+        CastRun                 -> CastRun  -instance SubstituteTX Witness where+instance SubstituteTX (Witness a) where  substituteWithTX tArg sub ww   = let down x   = substituteWithTX tArg x     in case ww of-        WVar u                  -> WVar u+        WVar  a u               -> WVar  a u         WCon{}                  -> ww-        WApp  w1 w2             -> WApp  (down sub w1) (down sub w2)-        WJoin w1 w2             -> WJoin (down sub w1) (down sub w2)-        WType t                 -> WType (down sub t)+        WApp  a w1 w2           -> WApp  a (down sub w1) (down sub w2)+        WJoin a w1 w2           -> WJoin a (down sub w1) (down sub w2)+        WType a t               -> WType a (down sub t)   instance SubstituteTX Bind where

@@ -23,7 +23,7 @@ --   type being substituted, and starts with an empty binder stack. substituteWX          :: (Ord n, SubstituteWX c) -        => Bind n -> Witness n -> c n -> c n+        => Bind n -> Witness a n -> c a n -> c a n  substituteWX b wArg xx  | Just u       <- takeSubstBoundOfBind b@@ -56,19 +56,19 @@ -- | Wrapper for `substituteWithWX` to substitute multiple things. substituteWXs          :: (Ord n, SubstituteWX c) -        => [(Bind n, Witness n)] -> c n -> c n+        => [(Bind n, Witness a n)] -> c a n -> c a n substituteWXs bts x         = foldr (uncurry substituteWX) x bts   --------------------------------------------------------------------------------class SubstituteWX (c :: * -> *) where+class SubstituteWX (c :: * -> * -> *) where  substituteWithWX-        :: forall n. Ord n-        => Witness n -> Sub n -> c n -> c n+        :: forall a n. Ord n+        => Witness a n -> Sub n -> c a n -> c a n  -instance SubstituteWX (Exp a) where +instance SubstituteWX Exp where   substituteWithWX wArg sub xx   = {-# SCC substituteWithWX #-}     let down s x   = substituteWithWX wArg s x@@ -88,12 +88,11 @@                 x'              = down  sub1 x             in  XLam a b' x' -        XLet a (LLet m b x1) x2-         -> let m'              = down  sub  m-                x1'             = down  sub  x1+        XLet a (LLet b x1) x2+         -> let x1'             = down  sub  x1                 (sub1, b')      = bind0 sub  b                 x2'             = down  sub1 x2-            in  XLet a (LLet m' b' x1') x2'+            in  XLet a (LLet b' x1') x2'          XLet a (LRec bxs) x2          -> let (bs, xs)        = unzip  bxs@@ -117,17 +116,7 @@         XWitness w      -> XWitness (down sub w)  --instance SubstituteWX LetMode where- substituteWithWX wArg sub lm-  = let down s x = substituteWithWX wArg s x-    in case lm of-        LetStrict        -> lm-        LetLazy Nothing  -> LetLazy Nothing-        LetLazy (Just w) -> LetLazy (Just (down sub w))---instance SubstituteWX (Alt a) where+instance SubstituteWX Alt where  substituteWithWX wArg sub aa   = let down s x = substituteWithWX wArg s x     in case aa of@@ -140,7 +129,7 @@             in  AAlt (PData uCon bs') x'  -instance SubstituteWX (Cast a) where+instance SubstituteWX Cast where  substituteWithWX wArg sub cc   = let down s x = substituteWithWX wArg s x         into s x = renameWith s x@@ -149,6 +138,8 @@         CastWeakenClosure xs    -> CastWeakenClosure (map (down sub) xs)         CastPurify w            -> CastPurify        (down sub w)         CastForget w            -> CastForget        (down sub w)+        CastSuspend             -> CastSuspend+        CastRun                 -> CastRun   instance SubstituteWX Witness where@@ -156,20 +147,20 @@   = let down s x = substituteWithWX wArg s x         into s x = renameWith s x     in case ww of-        WVar u+        WVar a u          -> case substW wArg sub u of-                Left u'  -> WVar u'+                Left u'  -> WVar a u'                 Right w  -> w          WCon{}                  -> ww-        WApp  w1 w2             -> WApp  (down sub w1) (down sub w2)-        WJoin w1 w2             -> WJoin (down sub w1) (down sub w2)-        WType t                 -> WType (into sub t)+        WApp  a w1 w2           -> WApp  a (down sub w1) (down sub w2)+        WJoin a w1 w2           -> WJoin a (down sub w1) (down sub w2)+        WType a t               -> WType a (into sub t)   -- | Rewrite or substitute into a witness variable.-substW  :: Ord n => Witness n -> Sub n -> Bound n -        -> Either (Bound n) (Witness n)+substW  :: Ord n => Witness a n -> Sub n -> Bound n +        -> Either (Bound n) (Witness a n)  substW wArg sub u   = case substBound (subStack0 sub) (subBound sub) u of

@@ -72,7 +72,7 @@ --   Perform type substitution for an `XType`  --    and witness substitution for an `XWitness` substituteXArg -        :: (Ord n, SubstituteXX c, SubstituteWX (c a), SubstituteTX (c a))+        :: (Ord n, SubstituteXX c, SubstituteWX c, SubstituteTX (c a))         => Bind n -> Exp a n -> c a n -> c a n  substituteXArg b arg x@@ -84,7 +84,7 @@  -- | Wrapper for `substituteXArgs` to substitute multiple arguments. substituteXArgs-        :: (Ord n, SubstituteXX c, SubstituteWX (c a), SubstituteTX (c a))+        :: (Ord n, SubstituteXX c, SubstituteWX c, SubstituteTX (c a))         => [(Bind n, Exp a n)] -> c a n -> c a n  substituteXArgs bas x@@ -122,12 +122,11 @@                 x'              = down  sub1 x             in  XLam a b' x' -        XLet a (LLet m b x1) x2-         -> let m'              = into  sub  m-                x1'             = down  sub  x1+        XLet a (LLet b x1) x2+         -> let x1'             = down  sub  x1                 (sub1, b')      = bind0 sub  b                 x2'             = down  sub1 x2-            in  XLet a (LLet m' b' x1') x2'+            in  XLet a (LLet b' x1') x2'          XLet a (LRec bxs) x2          -> let (bs, xs)        = unzip  bxs@@ -173,6 +172,8 @@         CastWeakenClosure xs    -> CastWeakenClosure (map (down sub) xs)         CastPurify w            -> CastPurify (into sub w)         CastForget w            -> CastForget (into sub w)+        CastSuspend             -> CastSuspend+        CastRun                 -> CastRun   -- | Rewrite or substitute into an expression variable.

@@ -98,7 +98,7 @@          BindUse BoundWit u          | member u tenv     -> []-         | otherwise         -> [XWitness (WVar u)]+         | otherwise         -> [XWitness (WVar a u)]          BindUse BoundSpec u          | member u kenv     -> []

@@ -1,7 +1,10 @@ -- | Check the kind of a type. module DDC.Type.Check-        ( -- * Kinds of Types-          checkType+        ( Config        (..)+        , configOfProfile++          -- * Kinds of Types+        , checkType         , kindOfType            -- * Kinds of Constructors@@ -16,6 +19,7 @@ import DDC.Type.Check.Error import DDC.Type.Check.ErrorMessage      () import DDC.Type.Check.CheckCon+import DDC.Type.Check.Config import DDC.Type.Compounds import DDC.Type.Predicates import DDC.Type.Exp@@ -30,7 +34,6 @@ import qualified DDC.Type.Env            as Env import qualified Data.Map                as Map - -- | The type checker monad. type CheckM n   = G.CheckM (Error n) @@ -38,7 +41,7 @@ -- Wrappers ------------------------------------------------------------------- -- | Check a type in the given environment, returning an error or its kind. checkType  :: (Ord n, Show n, Pretty n) -           => DataDefs n +           => Config n             -> KindEnv n             -> Type n             -> Either (Error n) (Kind n)@@ -49,7 +52,7 @@  -- | Check a type in an empty environment, returning an error or its kind. kindOfType :: (Ord n, Show n, Pretty n) -           => DataDefs n+           => Config n            -> Type n             -> Either (Error n) (Kind n) @@ -66,24 +69,24 @@ --   crushable components terms. checkTypeM          :: (Ord n, Show n, Pretty n) -        => DataDefs n+        => Config n         -> KindEnv n         -> Type n          -> CheckM n (Kind n) -checkTypeM defs env tt-        = -- trace (pretty $ text "checkTypeM:" <+> ppr tt) $+checkTypeM config env tt+        = -- trace (renderPlain $ text "checkTypeM:" <+> text (show tt)) $           {-# SCC checkTypeM #-}-          checkTypeM' defs env tt+          checkTypeM' config env tt  -- Variables -------------------checkTypeM' _defs env (TVar u)+checkTypeM' _config env (TVar u)  = case Env.lookup u env of         Just t  -> return t         Nothing -> throw $ ErrorUndefined u  -- Constructors ----------------checkTypeM' defs _env tt@(TCon tc)+checkTypeM' config env tt@(TCon tc)  = case tc of         -- Sorts don't have a higher classification.         TyConSort _      -> throw $ ErrorNakedSort tt@@ -99,12 +102,20 @@         TyConSpec    tcc -> return $ kindOfTcCon tcc          -- User defined type constructors need to be in the set of data defs.-        TyConBound   u k+        TyConBound u k          -> case u of                 UName n-                 | Just _ <- Map.lookup n (dataDefsTypes defs)+                 | Just _ <- Map.lookup n +                          $  dataDefsTypes $ configPrimDataDefs config                  -> return k +                 | Just s <- Env.lookupName n+                          $  configPrimSupers config+                 -> return s++                 | Just s <- Env.lookupName n env+                 -> return s+                  | otherwise                  -> throw $ ErrorUndefinedCtor u @@ -113,9 +124,9 @@   -- Quantifiers -----------------checkTypeM' defs env tt@(TForall b1 t2)- = do   _       <- checkTypeM defs env (typeOfBind b1)-        k2      <- checkTypeM defs (Env.extend b1 env) t2+checkTypeM' config env tt@(TForall b1 t2)+ = do   _       <- checkTypeM config env (typeOfBind b1)+        k2      <- checkTypeM config (Env.extend b1 env) t2          -- The body must have data or witness kind.         when (  (not $ isDataKind k2)@@ -127,18 +138,18 @@ -- Applications --------------- -- Applications of the kind function constructor are handled directly -- because the constructor doesn't have a sort by itself.-checkTypeM' defs env (TApp (TApp (TCon (TyConKind KiConFun)) k1) k2)- = do   _       <- checkTypeM defs env k1-        s2      <- checkTypeM defs env k2+checkTypeM' config env (TApp (TApp (TCon (TyConKind KiConFun)) k1) k2)+ = do   _       <- checkTypeM config env k1+        s2      <- checkTypeM config env k2         return  s2  -- The implication constructor is overloaded and can have the -- following kinds: --   (=>) :: @ ~> @ ~> @,  for witness implication. --   (=>) :: @ ~> * ~> *,  for a context.-checkTypeM' defs env tt@(TApp (TApp (TCon (TyConWitness TwConImpl)) t1) t2)- = do   k1      <- checkTypeM defs env t1-        k2      <- checkTypeM defs env t2+checkTypeM' config env tt@(TApp (TApp (TCon (TyConWitness TwConImpl)) t1) t2)+ = do   k1      <- checkTypeM config env t1+        k2      <- checkTypeM config env t2         if      isWitnessKind k1 && isWitnessKind k2          then     return kWitness         else if isWitnessKind k1 && isDataKind k2@@ -146,9 +157,9 @@         else    throw $ ErrorWitnessImplInvalid tt t1 k1 t2 k2  -- Type application.-checkTypeM' defs env tt@(TApp t1 t2)- = do   k1      <- checkTypeM defs env t1-        k2      <- checkTypeM defs env t2+checkTypeM' config env tt@(TApp t1 t2)+ = do   k1      <- checkTypeM config env t1+        k2      <- checkTypeM config env t2         case k1 of          TApp (TApp (TCon (TyConKind KiConFun)) k11) k12           | k11 == k2   -> return k12@@ -157,8 +168,8 @@          _              -> throw $ ErrorAppNotFun tt t1 k1 t2 k2  -- Sums ------------------------checkTypeM' defs env (TSum ts)- = do   ks      <- mapM (checkTypeM defs env) $ TS.toList ts+checkTypeM' config env (TSum ts)+ = do   ks      <- mapM (checkTypeM config env) $ TS.toList ts          -- Check that all the types in the sum have a single kind,          -- and return that kind.

@@ -53,7 +53,7 @@         TwConLazy       -> kRegion   `kFun`  kWitness         TwConHeadLazy   -> kData     `kFun`  kWitness         TwConManifest   -> kRegion   `kFun`  kWitness-        TwConDisjoint	  -> kEffect   `kFun`  kEffect  `kFun`  kWitness+        TwConDisjoint	-> kEffect   `kFun`  kEffect  `kFun`  kWitness         TwConDistinct n -> (replicate n kRegion)      `kFuns` kWitness          @@ -62,7 +62,9 @@ kindOfTcCon tc  = case tc of         TcConUnit       -> kData-        TcConFun        -> [kData, kEffect, kClosure, kData] `kFuns` kData+        TcConFun        -> kData    `kFun` kData `kFun` kData+        TcConFunEC      -> [kData, kEffect, kClosure, kData] `kFuns` kData+        TcConSusp       -> kEffect  `kFun` kData `kFun` kData         TcConRead       -> kRegion  `kFun` kEffect         TcConHeadRead   -> kData    `kFun` kEffect         TcConDeepRead   -> kData    `kFun` kEffect

@@ -0,0 +1,66 @@++module DDC.Type.Check.Config+        ( Config (..)+        , configOfProfile)+where+import DDC.Type.DataDef+import DDC.Type.Env                     (SuperEnv, KindEnv, TypeEnv)+import qualified DDC.Core.Fragment      as F+++-- Config ---------------------------------------------------------------------+-- | Static configuration for the type checker.+--   These fields don't change as we decend into the tree.+--+--   The starting configuration should be converted from the profile that+--   defines the language fragment you are checking. +--   See "DDC.Core.Fragment" and use `configOfProfile` below.+data Config n+        = Config+        { -- | Data type definitions.+          configPrimDataDefs            :: DataDefs n ++          -- | Super kinds of primitive kinds.+        , configPrimSupers              :: SuperEnv n++          -- | Kinds of primitive types.+        , configPrimKinds               :: KindEnv n++          -- | Types of primitive operators.+        , configPrimTypes               :: TypeEnv n++          -- | Track effect type information.+        , configTrackedEffects          :: Bool++          -- | Track closure type information.+        , configTrackedClosures         :: Bool ++          -- | Attach effect information to function types.+        , configFunctionalEffects       :: Bool++          -- | Attach closure information to function types.+        , configFunctionalClosures      :: Bool }++++-- | Convert a langage profile to a type checker configuration.+configOfProfile :: F.Profile n -> Config n+configOfProfile profile+        = Config+        { configPrimDataDefs       = F.profilePrimDataDefs profile+        , configPrimSupers         = F.profilePrimSupers profile+        , configPrimKinds          = F.profilePrimKinds  profile+        , configPrimTypes          = F.profilePrimTypes  profile++        , configTrackedEffects     = F.featuresTrackedEffects+                                   $ F.profileFeatures profile++        , configTrackedClosures    = F.featuresTrackedClosures+                                   $ F.profileFeatures profile++        , configFunctionalEffects  = F.featuresFunctionalEffects+                                   $ F.profileFeatures profile++        , configFunctionalClosures = F.featuresFunctionalClosures+                                   $ F.profileFeatures profile }+

@@ -11,10 +11,10 @@  ppr err   = case err of         ErrorUndefined u-         -> text "Undefined type variable:  " <> ppr u+         -> text "Undefined type variable: " <> ppr u          ErrorUndefinedCtor u-         -> text "Undefined type constructor:  " <> ppr u+         -> text "Undefined type constructor: " <> ppr u          ErrorUnappliedKindFun           -> text "Can't take sort of unapplied kind function constructor."

@@ -16,6 +16,7 @@         , namedBoundMatchesBind         , takeSubstBoundOfBind         , takeSubstBoundsOfBinds+        , replaceTypeOfBound            -- * Kinds         , kFun@@ -26,8 +27,9 @@         , takeResultKind           -- * Quantifiers-        , tForall-        , tForalls,      takeTForalls,  eraseTForalls+        , tForall,  tForall'+        , tForalls, tForalls'+        , takeTForalls,  eraseTForalls            -- * Sums         , tBot@@ -42,13 +44,18 @@         , takePrimeRegion            -- * Functions-        , tFun-        , tFunPE-        , takeTFun+        , tFun,         tFunOfList+        , tFunPE,       tFunOfListPE+        , tFunEC+        , takeTFun,     takeTFunEC         , takeTFunArgResult         , takeTFunWitArgResult+        , takeTFunAllArgResult         , arityOfType +          -- * Suspensions+        , tSusp+           -- * Implications         , tImpl @@ -198,7 +205,17 @@         go level (BAnon _   : bs') = UIx level : go (level + 1) bs'         go level (BNone _   : bs') =             go level bs' -            ++-- | If this `Bound` is a `UPrim` then replace it's embedded type with a new+--   one, otherwise return it unharmed.+replaceTypeOfBound :: Type n -> Bound n -> Bound n+replaceTypeOfBound t uu+ = case uu of+        UName{}         -> uu+        UPrim n _       -> UPrim n t+        UIx{}           -> uu++ -- Variables ------------------------------------------------------------------ -- | Construct a deBruijn index. tIx :: Kind n -> Int -> Type n@@ -285,15 +302,31 @@ tForall k f         = TForall (BAnon k) (f (TVar (UIx 0))) +-- | Build an anonymous type abstraction, with a single parameter.+--   Starting the next index from the given value.+tForall' :: Int -> Kind n -> (Type n -> Type n) -> Type n+tForall' ix k f+        = TForall (BAnon k) (f (TVar (UIx ix))) + -- | Build an anonymous type abstraction, with several parameters.+--   Starting the next index from the given value. tForalls  :: [Kind n] -> ([Type n] -> Type n) -> Type n tForalls ks f  = let  bs      = [BAnon k | k <- ks]-        us      = map (\i -> TVar (UIx i)) [0.. (length ks - 1)]+        us      = map (\i -> TVar (UIx i)) [0 .. (length ks - 1)]    in   foldr TForall (f $ reverse us) bs  +-- | Build an anonymous type abstraction, with several parameters.+--   Starting the next index from the given value.+tForalls'  :: Int -> [Kind n] -> ([Type n] -> Type n) -> Type n+tForalls' ix ks f+ = let  bs      = [BAnon k | k <- ks]+        us      = map (\i -> TVar (UIx i)) [ix .. ix + (length ks - 1)]+   in   foldr TForall (f $ reverse us) bs++ -- | Split nested foralls from the front of a type,  --   or `Nothing` if there was no outer forall. takeTForalls :: Type n -> Maybe ([Bind n], Type n)@@ -378,38 +411,101 @@         _       -> kk  +-- Function types -------------------------------------------------------------+-- | Construct a pure function type.+tFun      :: Type n -> Type n -> Type n+tFun t1 t2+        = (TCon $ TyConSpec TcConFun)  `tApps` [t1, t2]+infixr `tFun`++ -- | Construct a value type function,  --   with the provided effect and closure.-tFun    :: Type n -> Effect n -> Closure n -> Type n -> Type n-tFun t1 eff clo t2-        = (TCon $ TyConSpec TcConFun) `tApps` [t1, eff, clo, t2]-infixr `tFun`+tFunEC    :: Type n -> Effect n -> Closure n -> Type n -> Type n+tFunEC t1 eff clo t2+        = (TCon $ TyConSpec TcConFunEC) `tApps` [t1, eff, clo, t2]+infixr `tFunEC`  --- | Destruct the type of a value function.-takeTFun :: Type n -> Maybe (Type n, Effect n, Closure n, Type n)+-- | Construct a pure and empty value type function.+tFunPE  :: Type n -> Type n -> Type n+tFunPE t1 t2    = tFunEC t1 (tBot kEffect) (tBot kClosure) t2+infixr `tFunPE`+++-- | Construct a pure and empty function from a list containing the +--   parameter and return type. Yields `Nothing` if the list is empty.+tFunOfList :: [Type n] -> Maybe (Type n)+tFunOfList ts+  = case reverse ts of+        []      -> Nothing+        (t : tsArgs)       +         -> let tFuns' []             = t+                tFuns' (t' : ts')     = t' `tFun` tFuns' ts'+            in  Just $ tFuns' (reverse tsArgs)+++-- | Construct a pure and empty function from a list containing the +--   parameter and return type. Yields `Nothing` if the list is empty.+tFunOfListPE :: [Type n] -> Maybe (Type n)+tFunOfListPE ts+  = case reverse ts of+        []      -> Nothing+        (t : tsArgs)       +         -> let tFunPEs' []             = t+                tFunPEs' (t' : ts')     = t' `tFunPE` tFunPEs' ts'+            in  Just $ tFunPEs' (reverse tsArgs)+++-- | Yield the argument and result type of a function type.+--   +--   Works for both `TcConFun` and `TcConFunEC`.+takeTFun :: Type n -> Maybe (Type n, Type n) takeTFun tt  = case tt of-        TApp (TApp (TApp (TApp (TCon (TyConSpec TcConFun)) t1) eff) clo) t2+        TApp (TApp (TCon (TyConSpec TcConFun)) t1) t2+         ->  Just (t1, t2)++        TApp (TApp (TApp (TApp (TCon (TyConSpec TcConFunEC)) t1) _eff) _clo) t2+         ->  Just (t1, t2)++        _ -> Nothing+++-- | Yield the argument and result type of a function type.+takeTFunEC :: Type n -> Maybe (Type n, Effect n, Closure n, Type n)+takeTFunEC tt+ = case tt of+        TApp (TApp (TApp (TApp (TCon (TyConSpec TcConFunEC)) t1) eff) clo) t2          ->  Just (t1, eff, clo, t2)+         _ -> Nothing  --- | Destruct the type of a function,---   returning just the argument and result types.+-- | Destruct the type of a function, returning just the argument and result types.+--+--   Works for both `TcConFun` and `TcConFunEC`. takeTFunArgResult :: Type n -> ([Type n], Type n) takeTFunArgResult tt  = case tt of-        TApp (TApp (TApp (TApp (TCon (TyConSpec TcConFun)) t1) _eff) _clo) t2-          -> let (tsMore, tResult) = takeTFunArgResult t2-             in  (t1 : tsMore, tResult)+        TApp (TApp (TCon (TyConSpec TcConFun)) t1) t2+         -> let (tsMore, tResult) = takeTFunArgResult t2+            in  (t1 : tsMore, tResult) +        TApp (TApp (TApp (TApp (TCon (TyConSpec TcConFunEC)) t1) _eff) _clo) t2+         -> let (tsMore, tResult) = takeTFunArgResult t2+            in  (t1 : tsMore, tResult)+         _ -> ([], tt) + -- | Destruct the type of a function, --   returning the witness argument, value argument and result types. --   The function type must have the witness implications before  --   the value arguments, eg  @T1 => T2 -> T3 -> T4 -> T5@.+--+--   Works for both `TcConFun` and `TcConFunEC`.+-- takeTFunWitArgResult :: Type n -> ([Type n], [Type n], Type n) takeTFunWitArgResult tt  = case tt of@@ -421,6 +517,35 @@              in  ([], tvsMore, tResult)  +-- | Destruct the type of a possibly polymorphic function+--   returning all kinds of quantifiers, witness arguments, +--   and value arguments in the order they appear, along with +--   the type of the result.+takeTFunAllArgResult :: Type n -> ([Type n], Type n)+takeTFunAllArgResult tt+ = case tt of+        TVar{}          -> ([], tt)+        TCon{}          -> ([], tt)++        TForall b t     +         -> let (tsMore, tResult)       = takeTFunAllArgResult t+            in  (typeOfBind b : tsMore, tResult)++        TApp (TApp (TCon (TyConSpec TcConFun)) t1) t2+         -> let (tsMore, tResult) = takeTFunAllArgResult t2+            in  (t1 : tsMore, tResult)++        TApp (TApp (TApp (TApp (TCon (TyConSpec TcConFunEC)) t1) _eff) _clo) t2+         -> let (tsMore, tResult) = takeTFunAllArgResult t2+            in  (t1 : tsMore, tResult)++        TApp (TApp (TCon (TyConWitness TwConImpl)) t1) t2+         -> let (tsMore, tResult) = takeTFunAllArgResult t2+            in  (t1 : tsMore, tResult)++        _ -> ([], tt)++ -- | Determine the arity of an expression by looking at its type. --   Count all the function arrows, and foralls. arityOfType :: Type n -> Int@@ -430,12 +555,7 @@         t               -> length $ fst $ takeTFunArgResult t  --- | Construct a pure and empty value type function.-tFunPE  :: Type n -> Type n -> Type n-tFunPE t1 t2    = tFun t1 (tBot kEffect) (tBot kClosure) t2-infixr `tFunPE`--+-- Implications --------------------------------------------------------------- -- | Construct a witness implication type. tImpl :: Type n -> Type n -> Type n tImpl t1 t2      @@ -443,6 +563,12 @@ infixr `tImpl`  +-- Suspensions ----------------------------------------------------------------+tSusp  :: Effect n -> Type n -> Type n+tSusp tE tA+        = (TCon $ TyConSpec TcConSusp) `tApp` tE `tApp` tA++ -- Level 3 constructors (sorts) ----------------------------------------------- sComp           = TCon $ TyConSort SoConComp sProp           = TCon $ TyConSort SoConProp@@ -485,10 +611,10 @@ tHeadLazy       = twCon1 TwConHeadLazy tManifest       = twCon1 TwConManifest -tcCon1 tc t  = (TCon $ TyConSpec    tc) `tApp` t-twCon1 tc t  = (TCon $ TyConWitness tc) `tApp` t+tcCon1 tc t     = (TCon $ TyConSpec    tc) `tApp` t+twCon1 tc t     = (TCon $ TyConWitness tc) `tApp` t -twCon2 tc ts = tApps (TCon $ TyConWitness tc) ts+twCon2 tc ts    = tApps (TCon $ TyConWitness tc) ts   -- | Build a nullary type constructor of the given kind.@@ -499,5 +625,4 @@ -- | Build a type constructor application of one argumnet. tConData1 :: n -> Kind n -> Type n -> Type n tConData1 n k t1 = TApp (TCon (TyConBound (UName n) k)) t1- 

@@ -8,6 +8,7 @@ -- module DDC.Type.Env         ( Env(..)+        , SuperEnv         , KindEnv         , TypeEnv @@ -21,7 +22,7 @@         , fromList         , fromTypeMap -        -- * Projetions +        -- * Projections          , depth         , member         , memberBind@@ -65,8 +66,10 @@   -- | Type synonym to improve readability.-type KindEnv n  = Env n+type SuperEnv n = Env n +-- | Type synonym to improve readability.+type KindEnv n  = Env n  -- | Type synonym to improve readability. type TypeEnv n  = Env n

@@ -106,7 +106,7 @@           --            --   INVARIANT: this list doesn't contain more `TSum`s.         , typeSumSpill          :: ![Type n] }-        deriving (Show)+        deriving Show           -- | Hash value used to insert types into the `typeSumElems` array of a `TypeSum`.@@ -142,17 +142,17 @@         | TyConSpec     !TcCon          -- | User defined and primitive constructors.-        | TyConBound   !(Bound n) !(Kind n)+        | TyConBound   !(Bound n) !(Type n)         deriving Show   -- | Sort constructor. data SoCon         -- | Sort of witness kinds.-        = SoConProp                -- '@@'+        = SoConProp                -- 'Prop'          -- | Sort of computation kinds.-        | SoConComp                -- '**'+        | SoConComp                -- 'Comp'         deriving (Eq, Show)  @@ -164,66 +164,66 @@          -- Witness kinds ------------------------         -- | Kind of witnesses.-        | KiConWitness          -- '@ :: @@'+        | KiConWitness          -- 'Witness :: Prop'          -- Computation kinds ---------------------         -- | Kind of data values.-        | KiConData             -- '* :: **'+        | KiConData             -- 'Data    :: Comp'          -- | Kind of regions.-        | KiConRegion           -- '% :: **'+        | KiConRegion           -- 'Region  :: Comp'          -- | Kind of effects.-        | KiConEffect           -- '! :: **'+        | KiConEffect           -- 'Effect  :: Comp'          -- | Kind of closures.-        | KiConClosure          -- '$ :: **'+        | KiConClosure          -- 'Closure :: Comp'         deriving (Eq, Show)   -- | Witness type constructors. data TwCon         -- Witness implication.-        = TwConImpl             -- :: '(=>) :: @ ~> *'+        = TwConImpl             -- :: '(=>) :: Witness ~> Data'          -- | Purity of some effect.-        | TwConPure             -- :: ! ~> @+        | TwConPure             -- :: Effect  ~> Witness          -- | Emptiness of some closure.-        | TwConEmpty            -- :: $ ~> @+        | TwConEmpty            -- :: Closure ~> Witness          -- | Globalness of some region.-        | TwConGlobal           -- :: % ~> @+        | TwConGlobal           -- :: Region  ~> Witness          -- | Globalness of material regions in some type.-        | TwConDeepGlobal       -- :: * ~> @+        | TwConDeepGlobal       -- :: Data    ~> Witness                  -- | Constancy of some region.-        | TwConConst            -- :: % ~> @+        | TwConConst            -- :: Region  ~> Witness          -- | Constancy of material regions in some type-        | TwConDeepConst        -- :: * ~> @+        | TwConDeepConst        -- :: Data    ~> Witness          -- | Mutability of some region.-        | TwConMutable          -- :: % ~> @+        | TwConMutable          -- :: Region  ~> Witness          -- | Mutability of material regions in some type.-        | TwConDeepMutable      -- :: * ~> @+        | TwConDeepMutable      -- :: Data    ~> Witness          -- | Distinctness of some n regions-        | TwConDistinct Int     -- :: * ~> [%] ~> @+        | TwConDistinct Int     -- :: Data    ~> [Region] ~> Witness                  -- | Laziness of some region.-        | TwConLazy             -- :: % ~> @+        | TwConLazy             -- :: Region  ~> Witness          -- | Laziness of the primary region in some type.-        | TwConHeadLazy         -- :: * ~> @+        | TwConHeadLazy         -- :: Data    ~> Witness          -- | Manifestness of some region (not lazy).-        | TwConManifest         -- :: % ~> @+        | TwConManifest         -- :: Region  ~> Witness          -- | Non-interfering effects are disjoint. Used for rewrite rules.-        | TwConDisjoint               -- :: ! ~> ! ~> @+        | TwConDisjoint         -- :: Effect ~> Effect ~> Witness         deriving (Eq, Show)  @@ -231,37 +231,43 @@ data TcCon         -- Data type constructors ---------------         -- | The unit data type constructor is baked in.-        = TcConUnit             -- 'Unit :: *'+        = TcConUnit             -- 'Unit :: Data' -        -- | The function type constructor is baked in.-        | TcConFun              -- '(->) :: * ~> * ~> ! ~> $ ~> *'+        -- | Pure function.+        | TcConFun              -- '(->)' :: Data ~> Data ~> Data +        -- | Function with a latent effect and closure.+        | TcConFunEC            -- '(->)  :: Data ~> Data ~> Effect ~> Closure ~> Data'++        -- | A suspended computation.+        | TcConSusp             -- 'S     :: Effect ~> Data ~> Data'+         -- Effect type constructors -------------         -- | Read of some region.-        | TcConRead             -- :: '% ~> !'+        | TcConRead             -- :: 'Region ~> Effect'          -- | Read the head region in a data type.-        | TcConHeadRead         -- :: '* ~> !'+        | TcConHeadRead         -- :: 'Data   ~> Effect'          -- | Read of all material regions in a data type.-        | TcConDeepRead         -- :: '* ~> !'+        | TcConDeepRead         -- :: 'Data   ~> Effect'                  -- | Write of some region.-        | TcConWrite            -- :: '% ~> !'+        | TcConWrite            -- :: 'Region ~> Effect'          -- | Write to all material regions in some data type.-        | TcConDeepWrite        -- :: '* ~> !'+        | TcConDeepWrite        -- :: 'Data   ~> Effect'                  -- | Allocation into some region.-        | TcConAlloc            -- :: '% ~> !'+        | TcConAlloc            -- :: 'Region ~> Effect'          -- | Allocation into all material regions in some data type.-        | TcConDeepAlloc        -- :: '* ~> !'+        | TcConDeepAlloc        -- :: 'Data   ~> Effect'                  -- Closure type constructors ------------         -- | Region is captured in a closure.-        | TcConUse              -- :: '% ~> $'+        | TcConUse              -- :: 'Region ~> Closure'                  -- | All material regions in a data type are captured in a closure.-        | TcConDeepUse          -- :: '* ~> $'+        | TcConDeepUse          -- :: 'Data   ~> Closure'         deriving (Eq, Show)

@@ -67,7 +67,13 @@          -> pprParen (d > 5)          $  pprPrec 6 t1 <+> text "=>" </> pprPrec 5 t2 -        TApp (TApp (TApp (TApp (TCon (TyConSpec TcConFun)) t1) eff) clo) t2+        -- Pure function.+        TApp (TApp (TCon (TyConSpec TcConFun)) t1) t2+         -> pprParen (d > 5)+         $  pprPrec 6 t1 <+> text "->" </> pprPrec 5 t2++        -- Function with a latent effect and closure.+        TApp (TApp (TApp (TApp (TCon (TyConSpec TcConFunEC)) t1) eff) clo) t2          | isBot eff, isBot clo          -> pprParen (d > 5)          $  pprPrec 6 t1 <+> text "->"  </> pprPrec 5 t2@@ -97,8 +103,17 @@          $  ppr t1 <+> pprPrec 11 t2          TSum ts-         | isBot tt     -         -> ppr (Sum.kindOfSum ts) <> text "0"+         | isBot tt, isEffectKind  $ Sum.kindOfSum ts+         -> text "Pure"++         | isBot tt, isClosureKind $ Sum.kindOfSum ts +         -> text "Empty"++         | isBot tt, isDataKind    $ Sum.kindOfSum ts +         -> text "Bot"++         | isBot tt, otherwise  +         -> error $ stage ++ ": malformed sum"                    | otherwise          -> pprParen (d > 9) $  ppr ts@@ -107,9 +122,9 @@ instance (Pretty n, Eq n) => Pretty (TypeSum n) where  ppr ss   = case Sum.toList ss of-      [] | isEffectKind  $ Sum.kindOfSum ss -> text "!0"-         | isClosureKind $ Sum.kindOfSum ss -> text "$0"-         | isDataKind    $ Sum.kindOfSum ss -> text "*0"+      [] | isEffectKind  $ Sum.kindOfSum ss -> text "Pure"+         | isClosureKind $ Sum.kindOfSum ss -> text "Empty"+         | isDataKind    $ Sum.kindOfSum ss -> text "Bot"          | otherwise     -> error $ stage ++ ": malformed sum"                 ts  -> sep $ punctuate (text " +") (map ppr ts)@@ -129,27 +144,27 @@ instance Pretty SoCon where  ppr sc    = case sc of-        SoConComp       -> text "**"-        SoConProp       -> text "@@"+        SoConComp       -> text "Comp"+        SoConProp       -> text "Prop"   instance Pretty KiCon where  ppr kc   = case kc of         KiConFun        -> text "(~>)"-        KiConData       -> text "*"-        KiConRegion     -> text "%"-        KiConEffect     -> text "!"-        KiConClosure    -> text "$"-        KiConWitness    -> text "@"+        KiConData       -> text "Data"+        KiConRegion     -> text "Region"+        KiConEffect     -> text "Effect"+        KiConClosure    -> text "Closure"+        KiConWitness    -> text "Witness"   instance Pretty TwCon where  ppr tw   = case tw of         TwConImpl       -> text "(=>)"-        TwConPure       -> text "Pure"-        TwConEmpty      -> text "Empty"+        TwConPure       -> text "Purify"+        TwConEmpty      -> text "Emptify"         TwConGlobal     -> text "Global"         TwConDeepGlobal -> text "DeepGlobal"         TwConConst      -> text "Const"@@ -168,6 +183,8 @@   = case tc of         TcConUnit       -> text "Unit"         TcConFun        -> text "(->)"+        TcConFunEC      -> text "(->)"+        TcConSusp       -> text "S"         TcConRead       -> text "Read"         TcConHeadRead   -> text "HeadRead"         TcConDeepRead   -> text "DeepRead"

@@ -107,7 +107,7 @@          -- Trim function constructors.         -- See Note: Material variables and the interpreter-        TApp (TApp (TApp (TApp (TCon (TyConSpec TcConFun)) _t1) _eff) clo) _t2+        TApp (TApp (TApp (TApp (TCon (TyConSpec TcConFunEC)) _t1) _eff) clo) _t2          -> Sum.singleton kClosure clo          -- Trim a type application.

@@ -100,7 +100,7 @@         TCon (TyConSort _)         -> Just UniverseKind         TCon (TyConKind _)         -> Just UniverseSpec         TCon (TyConWitness _)      -> Just UniverseWitness-        TCon (TyConSpec TcConFun)  -> Just UniverseData+        TCon (TyConSpec TcConFunEC)-> Just UniverseData         TCon (TyConSpec TcConUnit) -> Just UniverseData         TCon (TyConSpec _)         -> Nothing         TCon (TyConBound _ k)      -> universeFromType2 k

@@ -1,7 +1,7 @@ -------------------------------------------------------------------------------- The Disciplined Disciple Compiler License (MIT style) -Copyrite (K) 2007-2012 The Disciplined Disciple Compiler Strike Force+Copyrite (K) 2007-2013 The Disciplined Disciple Compiler Strike Force All rights reversed.  Permission is hereby granted, free of charge, to any person obtaining a copy

@@ -1,5 +1,5 @@ Name:           ddc-core-Version:        0.3.1.1+Version:        0.3.2.1 License:        MIT License-file:   LICENSE Author:         The Disciplined Disciple Compiler Strike Force@@ -9,16 +9,14 @@ Stability:      experimental Category:       Compilers/Interpreters Homepage:       http://disciple.ouroborus.net-Bug-reports:    disciple@ouroborus.net Synopsis:       Disciplined Disciple Compiler core language and type checker. Description:             Disciple Core is an explicitly typed language based on System-F2, intended         as an intermediate representation for a compiler. In addition to the polymorphism of          System-F2 it supports region, effect and closure typing. Evaluation order is -        left-to-right call-by-value by default, but explicit lazy evaluation is also supported.-        There is a capability system to track whether objects are mutable or constant,-        and to ensure that computations that perform visible side effects are not suspended with-        lazy evaluation.+        left-to-right call-by-value by default. There is a capability system to track whether+        objects are mutable or constant, and to ensure that computations that perform visible+        side effects are not reordered inappropriately.          See the @ddc-tools@ package for a user-facing interpreter and compiler. @@ -31,12 +29,33 @@         directory       == 1.2.*,         transformers    == 0.3.*,         mtl             == 2.1.*,-        ddc-base        == 0.3.1.*+        ddc-base        == 0.3.2.*    Exposed-modules:+        DDC.Core.Annot.AnT+        DDC.Core.Annot.AnTEC++        DDC.Core.Check+        DDC.Core.Collect++        DDC.Core.Compounds.Annot+        DDC.Core.Compounds.Simple+        DDC.Core.Compounds++        DDC.Core.Exp.Simple+        DDC.Core.Exp.Annot+        DDC.Core.Exp++        DDC.Core.Fragment+         DDC.Core.Lexer.Names         DDC.Core.Lexer.Tokens+        DDC.Core.Lexer +        DDC.Core.Parser++        DDC.Core.Transform.Annotate+        DDC.Core.Transform.Deannotate         DDC.Core.Transform.LiftT         DDC.Core.Transform.LiftX         DDC.Core.Transform.Reannotate@@ -47,16 +66,8 @@         DDC.Core.Transform.SubstituteXX         DDC.Core.Transform.Trim -        DDC.Core.Check-        DDC.Core.Collect-        DDC.Core.Compounds-        DDC.Core.DaCon-        DDC.Core.Exp-        DDC.Core.Fragment-        DDC.Core.Lexer         DDC.Core.Load         DDC.Core.Module-        DDC.Core.Parser         DDC.Core.Predicates         DDC.Core.Pretty @@ -93,8 +104,9 @@         DDC.Core.Collect.Support         DDC.Core.Collect.Free -        DDC.Core.Exp.Base-        DDC.Core.Exp.NFData+        DDC.Core.Exp.WiCon+        DDC.Core.Exp.DaCon+        DDC.Core.Exp.Pat          DDC.Core.Fragment.Compliance         DDC.Core.Fragment.Error@@ -105,6 +117,7 @@         DDC.Core.Lexer.Offside          DDC.Core.Parser.Base+        DDC.Core.Parser.Context         DDC.Core.Parser.Exp         DDC.Core.Parser.Module         DDC.Core.Parser.Param@@ -114,6 +127,7 @@         DDC.Type.Check.CheckCon         DDC.Type.Check.Error         DDC.Type.Check.ErrorMessage+        DDC.Type.Check.Config          DDC.Type.Collect.FreeT @@ -143,4 +157,5 @@         DoAndIfThenElse         DeriveDataTypeable         ViewPatterns+        FunctionalDependencies