ddc-core 0.2.1.2 → 0.3.1.1

raw patch · 81 files changed

+8778/−4705 lines, 81 filesdep +deepseqdep +directorydep ~ddc-basePVP ok

version bump matches the API change (PVP)

Dependencies added: deepseq, directory

Dependency ranges changed: ddc-base

API changes (from Hackage documentation)

Files

• DDC/Core/Check.hs +19/−3
• DDC/Core/Check/CheckDaCon.hs +50/−0
• DDC/Core/Check/CheckExp.hs +1120/−946
• DDC/Core/Check/CheckModule.hs +159/−0
• DDC/Core/Check/CheckWitness.hs +99/−92
• DDC/Core/Check/Error.hs +90/−50
• DDC/Core/Check/ErrorMessage.hs +100/−62
• DDC/Core/Check/TaggedClosure.hs +27/−21
• DDC/Core/Collect.hs +12/−247
• DDC/Core/Collect/Free.hs +128/−0
• DDC/Core/Collect/Support.hs +208/−0
• DDC/Core/Compounds.hs +239/−79
• DDC/Core/DaCon.hs +100/−0
• DDC/Core/DataDef.hs +0/−135
• DDC/Core/Exp.hs +5/−178
• DDC/Core/Exp/Base.hs +186/−0
• DDC/Core/Exp/NFData.hs +82/−0
• DDC/Core/Fragment.hs +65/−0
• DDC/Core/Fragment/Compliance.hs +388/−0
• DDC/Core/Fragment/Error.hs +59/−0
• DDC/Core/Fragment/Feature.hs +63/−0
• DDC/Core/Fragment/Profile.hs +111/−0
• DDC/Core/Lexer.hs +215/−0
• DDC/Core/Lexer/Comments.hs +64/−0
• DDC/Core/Lexer/Names.hs +226/−0
• DDC/Core/Lexer/Offside.hs +265/−0
• DDC/Core/Lexer/Tokens.hs +347/−0
• DDC/Core/Load.hs +240/−0
• DDC/Core/Module.hs +147/−0
• DDC/Core/Parser.hs +32/−619
• DDC/Core/Parser/Base.hs +98/−0
• DDC/Core/Parser/Exp.hs +547/−0
• DDC/Core/Parser/Lexer.hs +0/−293
• DDC/Core/Parser/Module.hs +125/−0
• DDC/Core/Parser/Param.hs +122/−0
• DDC/Core/Parser/Tokens.hs +0/−263
• DDC/Core/Parser/Type.hs +209/−0
• DDC/Core/Parser/Witness.hs +84/−0
• DDC/Core/Predicates.hs +35/−12
• DDC/Core/Pretty.hs +119/−30
• DDC/Core/Transform/LiftT.hs +107/−0
• DDC/Core/Transform/LiftW.hs +0/−116
• DDC/Core/Transform/LiftX.hs +133/−49
• DDC/Core/Transform/Reannotate.hs +68/−0
• DDC/Core/Transform/Rename.hs +41/−0
• DDC/Core/Transform/SpreadX.hs +62/−24
• DDC/Core/Transform/SubstituteTX.hs +18/−21
• DDC/Core/Transform/SubstituteWX.hs +25/−27
• DDC/Core/Transform/SubstituteXX.hs +25/−12
• DDC/Core/Transform/Trim.hs +112/−0
• DDC/Type/Bind.hs +31/−0
• DDC/Type/Check.hs +24/−57
• DDC/Type/Check/CheckCon.hs +22/−19
• DDC/Type/Check/CheckError.hs +0/−141
• DDC/Type/Check/Error.hs +71/−0
• DDC/Type/Check/ErrorMessage.hs +75/−0
• DDC/Type/Check/Monad.hs +0/−28
• DDC/Type/Collect.hs +185/−0
• DDC/Type/Collect/FreeT.hs +47/−0
• DDC/Type/Compounds.hs +138/−60
• DDC/Type/DataDef.hs +142/−0
• DDC/Type/Env.hs +58/−23
• DDC/Type/Equiv.hs +62/−83
• DDC/Type/Exp.hs +7/−259
• DDC/Type/Exp/Base.hs +267/−0
• DDC/Type/Exp/NFData.hs +81/−0
• DDC/Type/Parser.hs +0/−236
• DDC/Type/Predicates.hs +157/−10
• DDC/Type/Pretty.hs +7/−8
• DDC/Type/Rewrite.hs +0/−264
• DDC/Type/Sum.hs +94/−48
• DDC/Type/Transform/Crush.hs +48/−15
• DDC/Type/Transform/Instantiate.hs +12/−2
• DDC/Type/Transform/LiftT.hs +87/−41
• DDC/Type/Transform/LowerT.hs +0/−63
• DDC/Type/Transform/Rename.hs +246/−0
• DDC/Type/Transform/SpreadT.hs +18/−14
• DDC/Type/Transform/SubstituteT.hs +5/−5
• DDC/Type/Transform/Trim.hs +6/−3
• DDC/Type/Universe.hs +43/−24
• ddc-core.cabal +69/−23

@@ -1,17 +1,33 @@ --- | Type checker for the Disciple core language.+-- | Type checker for the Disciple Core language.+-- +--   The functions in this module do not check for language fragment compliance.+--   This needs to be done separately via "DDC.Core.Fragment".+-- module DDC.Core.Check-        ( -- * Checking Expressions-          checkExp,     typeOfExp+        ( -- * Configuration+          Config(..)+        , configOfProfile +          -- * Checking Modules+        , checkModule++          -- * Checking Expressions+        , checkExp,     typeOfExp+           -- * Checking Witnesses         , checkWitness, typeOfWitness         , typeOfWiCon +          -- * Annotations+        , AnTEC(..)+           -- * Error messages         , Error(..)) where import DDC.Core.Check.Error import DDC.Core.Check.ErrorMessage      ()+import DDC.Core.Check.CheckModule import DDC.Core.Check.CheckExp import DDC.Core.Check.CheckWitness+                

@@ -0,0 +1,50 @@++module DDC.Core.Check.CheckDaCon+        (checkDaConM)+where+import DDC.Core.Check.Error+import DDC.Core.Check.CheckWitness+import DDC.Core.DaCon+import DDC.Core.Exp+import DDC.Type.Compounds+import DDC.Type.DataDef+import DDC.Control.Monad.Check  (throw)+import Control.Monad+import Prelude                  as L+import qualified Data.Map       as Map+++-- | Check a data constructor.+--   The data constructor must be in the set of data type declarations.+checkDaConM+        :: (Ord n, Eq n, Show n)+        => Config n+        -> Exp a n              -- ^ The full expression for error messages.+        -> DaCon n              -- ^ Data constructor to check.+        -> CheckM a n ()++checkDaConM _ _ dc+ | DaConUnit    <- daConName dc+ = return ()++checkDaConM config xx dc+ | DaConNamed nCtor <- daConName dc+ , daConIsAlgebraic dc+ = let  tResult = snd $ takeTFunArgResult $ eraseTForalls $ typeOfDaCon dc+        defs    = configPrimDataDefs config+   in   case liftM fst $ takeTyConApps tResult of+         Just (TyConBound u _)+           | Just nType         <- takeNameOfBound u+           , Just dataType      <- Map.lookup nType (dataDefsTypes defs)+           -> case dataTypeMode dataType of+                DataModeSmall nsCtors+                 | L.elem nCtor nsCtors  -> return ()+                 | otherwise    -> throw $ ErrorUndefinedCtor xx++                DataModeLarge   -> return ()++         _ -> throw $ ErrorUndefinedCtor xx++checkDaConM _ _ _+ = return ()+

@@ -1,946 +1,1120 @@---- | Type checker for the Disciple Core language.-module DDC.Core.Check.CheckExp-        ( checkExp-        , typeOfExp-        , CheckM-        , checkExpM-        , TaggedClosure(..))-where-import DDC.Core.DataDef-import DDC.Core.Predicates-import DDC.Core.Compounds-import DDC.Core.Exp-import DDC.Core.Pretty-import DDC.Core.Collect-import DDC.Core.Check.Error-import DDC.Core.Check.CheckWitness-import DDC.Core.Check.TaggedClosure-import DDC.Type.Transform.SubstituteT-import DDC.Type.Transform.Crush-import DDC.Type.Transform.Trim-import DDC.Type.Transform.Instantiate-import DDC.Type.Transform.LiftT-import DDC.Type.Transform.LowerT-import DDC.Type.Equiv-import DDC.Type.Universe-import DDC.Type.Compounds-import DDC.Type.Predicates-import DDC.Type.Sum                     as Sum-import DDC.Type.Env                     (Env)-import DDC.Type.Check.Monad             (result, throw)-import DDC.Base.Pretty                  ()-import Data.Set                         (Set)-import qualified DDC.Type.Env           as Env-import qualified DDC.Type.Check         as T-import qualified Data.Set               as Set-import qualified Data.Map               as Map-import Control.Monad-import Data.List                        as L-import Data.Maybe----- Wrappers ---------------------------------------------------------------------- | Type check an expression. ------   If it's good, you get a new version with types attached to all the bound---   variables, as well its the type, effect and closure. ------   If it's bad, you get a description of the error.------   The returned expression has types attached to all variable occurrences, ---   so you can call `typeOfExp` on any open subterm.-checkExp -        :: (Ord n, Pretty n)-        => DataDefs n           -- ^ Data type definitions.-        -> Env n                -- ^ Kind environment.-        -> Env n                -- ^ Type environment.-        -> Exp a n              -- ^ Expression to check.-        -> Either (Error a n)-                  ( Exp a n-                  , Type n-                  , Effect n-                  , Closure n)--checkExp defs kenv tenv xx - = result- $ do   (xx', t, effs, clos) <- checkExpM defs kenv tenv xx-        return  ( xx'-                , t-                , TSum effs-                , closureOfTaggedSet clos)----- | Like `checkExp`, but check in an empty environment,---   and only return the value type of an expression.------   As this function is not given an environment, the types of free variables---   must be attached directly to the bound occurrences.---   This attachment is performed by `checkExp` above.----typeOfExp -        :: (Ord n, Pretty n)-        => DataDefs n-        -> Exp a n-        -> Either (Error a n) (Type n)-typeOfExp defs xx - = case checkExp defs Env.empty Env.empty xx of-        Left err           -> Left err-        Right (_, t, _, _) -> Right t----- checkExp ---------------------------------------------------------------------- | Like `checkExp` but using the `CheckM` monad to handle errors.-checkExpM -        :: (Ord n, Pretty n)-        => DataDefs n           -- ^ Data type definitions.-        -> Env n                -- ^ Kind environment.-        -> Env n                -- ^ Type environment.-        -> Exp a n              -- ^ Expression to check.-        -> CheckM a n -                ( Exp a n-                , Type n-                , TypeSum n-                , Set (TaggedClosure n))--checkExpM defs kenv tenv xx- = checkExpM' defs kenv tenv xx-{-} = do (xx', t, eff, clo) <- checkExpM' defs kenv tenv xx-      trace (pretty $ vcat -                [ text "checkExpM:  " <+> ppr xx -                , text "        ::  " <+> ppr t -                , text "        :!: " <+> ppr eff-                , text "        :$: " <+> ppr clo-                , text ""])-         $ return (xx', t, eff, clo)--}---- variables -------------------------------------checkExpM' _defs _kenv tenv (XVar a u)- = do   let tBound      = typeOfBound u-        let mtEnv       = Env.lookup u tenv--        let mkResult-             -- When annotation on the bound is bot,-             --  then use the type from the environment.-             | Just tEnv    <- mtEnv-             , isBot tBound-             = return tEnv--             -- The bound has an explicit type annotation,-             --  which matches the one from the environment.-             -- -             --  When the bound is a deBruijn index we need to lift the-             --  annotation on the original binder through any lambdas-             --  between the binding occurrence and the use.-             | Just tEnv    <- mtEnv-             , UIx i _      <- u-             , equivT tBound (liftT (i + 1) tEnv) -             = return tBound--             -- The bound has an explicit type annotation,-             --  which matches the one from the environment.-             | Just tEnv    <- mtEnv-             , equivT tBound tEnv-             = return tEnv--             -- The bound has an explicit type annotation,-             --  which does not match the one from the environment.-             --  This shouldn't happen because the parser doesn't add non-bot-             --  annotations to bound variables.-             | Just tEnv    <- mtEnv-             = throw $ ErrorVarAnnotMismatch u tEnv--             -- Variable not in environment, so use annotation.-             --  This happens when checking open terms.-             | otherwise-             = return tBound-        -        tResult  <- mkResult--        return  ( XVar a u -                , tResult-                , Sum.empty kEffect-                , Set.singleton -                        $ taggedClosureOfValBound -                        $ replaceTypeOfBound tResult u)----- constructors ----------------------------------checkExpM' defs _kenv _tenv xx@(XCon a u)-        | UName n _     <- u-        = case Map.lookup n (dataDefsCtors defs) of-           Nothing -> throw $ ErrorUndefinedCtor xx-           Just _  -            -> return  -                  ( XCon a u-                  , typeOfBound u-                  , Sum.empty kEffect-                  , Set.empty)--        | UPrim{}       <- u-        = return  ( XCon a u-                  , typeOfBound u-                  , Sum.empty kEffect-                  , Set.empty)--        -- Constructors can't be locally bound.-        | otherwise-        = throw $ ErrorMalformedExp xx----- application --------------------------------------- value-type application.-checkExpM' defs kenv tenv xx@(XApp a x1 (XType t2))- = do   (x1', t1, effs1, clos1) <- checkExpM  defs kenv tenv x1-        k2                      <- checkTypeM defs kenv t2-        case t1 of-         TForall b11 t12-          | typeOfBind b11 == k2-          -> return ( XApp a x1' (XType t2)  -                    , substituteT b11 t2 t12-                    , substituteT b11 t2 effs1-                    , clos1 `Set.union` taggedClosureOfTyArg t2)--          | otherwise   -> throw $ ErrorAppMismatch xx (typeOfBind b11) t2-         _              -> throw $ ErrorAppNotFun   xx t1 t2----- value-witness application.-checkExpM' defs kenv tenv xx@(XApp a x1 (XWitness w2))- = do   (x1', t1, effs1, clos1) <- checkExpM     defs kenv tenv x1-        t2                      <- checkWitnessM defs kenv tenv w2-        case t1 of-         TApp (TApp (TCon (TyConWitness TwConImpl)) t11) t12-          | t11 `equivT` t2   -          -> return ( XApp a x1' (XWitness w2)-                    , t12-                    , effs1-                    , clos1)--          | otherwise   -> throw $ ErrorAppMismatch xx t11 t2-         _              -> throw $ ErrorAppNotFun   xx t1 t2-                 ---- value-value application.-checkExpM' defs kenv tenv xx@(XApp a x1 x2)- = do   (x1', t1, effs1, clos1)    <- checkExpM defs kenv tenv x1-        (x2', t2, effs2, clos2)    <- checkExpM defs 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-          | t11 `equivT` t2   -          , effs    <- Sum.fromList kEffect  [eff]-          -> return ( XApp a x1' x2'-                    , t12-                    , effs1 `Sum.union` effs2 `Sum.union` effs-                    , clos1 `Set.union` clos2)--          | otherwise   -> throw $ ErrorAppMismatch xx t11 t2-         _              -> throw $ ErrorAppNotFun xx t1 t2----- spec abstraction ------------------------------checkExpM' defs kenv tenv xx@(XLAM a b1 x2)- = do   let t1          = typeOfBind b1-        _               <- checkTypeM defs kenv t1--        -- Check the body-        let kenv'         = Env.extend b1 kenv-        let tenv'         = Env.lift   1  tenv-        (x2', t2, e2, c2) <- checkExpM  defs kenv' tenv' x2-        k2                <- checkTypeM defs kenv' t2--        when (Env.memberBind b1 kenv)-         $ throw $ ErrorLamShadow xx b1--        -- The body of a spec abstraction must be pure.-        when (e2 /= Sum.empty kEffect)-         $ throw $ ErrorLamNotPure xx (TSum e2)--        -- The body of a spec abstraction must have data kind.-        when (not $ isDataKind k2)-         $ throw $ ErrorLamBodyNotData xx b1 t2 k2--        -- Mask closure terms due to locally bound region vars.-        let c2_cut      = Set.fromList-                        $ mapMaybe (cutTaggedClosureT b1)-                        $ Set.toList c2--        return ( XLAM a b1 x2'-               , TForall b1 t2-               , Sum.empty kEffect-               , c2_cut)-         ---- function abstractions -------------------------checkExpM' defs kenv tenv xx@(XLam a b1 x2)- = do   let t1               =  typeOfBind b1-        k1                   <- checkTypeM defs kenv t1--        -- Check the body.-        let tenv'            =  Env.extend b1 tenv-        (x2', t2, e2, c2)    <- checkExpM  defs kenv tenv' x2   -        k2                   <- checkTypeM defs kenv t2--        -- The form of the function constructor depends on what universe the -        -- binder is in.-        case universeFromType2 k1 of-         Just UniverseData-          |  not $ isDataKind k1     -> throw $ ErrorLamBindNotData xx t1 k1-          |  not $ isDataKind k2     -> throw $ ErrorLamBodyNotData xx b1 t2 k2 -          |  otherwise-          -> let -                 -- Cut closure terms due to locally bound value vars.-                 -- This also lowers deBruijn indices in un-cut closure terms.-                 c2_cut  = Set.fromList-                         $ mapMaybe (cutTaggedClosureX b1)-                         $ Set.toList c2--                 -- Trim the closure before we annotate the returned function-                 -- type with it. -                 --  This should always succeed because trimClosure only returns-                 --  Nothing if the closure is miskinded, and we've already-                 --  allready checked that.-                 Just c2_captured-                  = trimClosure $ closureOfTaggedSet c2_cut--             in  return ( XLam a b1 x2'-                        , tFun t1 (TSum e2) c2_captured t2-                        , Sum.empty kEffect-                        , c2_cut) --         Just UniverseWitness-          | e2 /= Sum.empty kEffect  -> throw $ ErrorLamNotPure     xx (TSum e2)-          | not $ isDataKind k2      -> throw $ ErrorLamBodyNotData xx b1 t2 k2-          | otherwise                -          -> return ( XLam a b1 x2'-                    , tImpl t1 t2-                    , Sum.empty kEffect-                    , c2)--         _ -> throw $ ErrorMalformedType xx k1----- let ---------------------------------------------checkExpM' defs kenv tenv xx@(XLet a (LLet mode b11 x12) x2)- = do   -- Check the right of the binding.-        (x12', t12, effs12, clo12)  -         <- checkExpM defs kenv tenv x12--        -- Check binder annotation against the type we inferred for the right.-        (b11', k11')    -         <- checkLetBindOfTypeM xx defs kenv tenv t12 b11--        -- The right of the binding should have data kind.-        when (not $ isDataKind k11')-         $ throw $ ErrorLetBindingNotData xx b11' k11'-          -        -- Check the body expression.-        let tenv1  = Env.extend b11' tenv-        (x2', t2, effs2, c2)    <- checkExpM defs kenv tenv1 x2--        -- The body should have data kind.-        k2 <- checkTypeM defs kenv t2-        when (not $ isDataKind k2)-         $ throw $ ErrorLetBodyNotData xx t2 k2--        -- Mask closure terms due to locally bound value vars.-        let c2_cut      = Set.fromList-                        $ mapMaybe (cutTaggedClosureX b11')-                        $ Set.toList c2--        -- 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 defs 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 defs 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 ( XLet a (LLet mode b11' x12') x2'-               , t2-               , effs12 `Sum.union` effs2-               , clo12  `Set.union` c2_cut)----- letrec ------------------------------------------checkExpM' defs kenv tenv xx@(XLet a (LRec bxs) xBody)- = do   -        let (bs, xs)    = unzip bxs--        -- Check all the annotations.-        ks              <- mapM (checkTypeM defs kenv) -                        $  map typeOfBind bs--        -- Check all the annots have data kind.-        zipWithM_ (\b k-         -> when (not $ isDataKind k)-                $ throw $ ErrorLetBindingNotData xx b k)-                bs ks--        -- All right hand sides need to be lambdas.-        forM_ xs $ \x -         -> when (not $ (isXLam x || isXLAM x))-                $ throw $ ErrorLetrecBindingNotLambda xx x--        -- All variables are in scope in all right hand sides.-        let tenv'       = Env.extends bs tenv--        -- Check the right hand sides.-        (xsRight', tsRight, _effssBinds, clossBinds) -                <- liftM unzip4 $ mapM (checkExpM defs kenv tenv') xs--        -- Check annots on binders against inferred types of the bindings.-        zipWithM_ (\b t-                -> if not $ equivT (typeOfBind b) t-                        then throw $ ErrorLetMismatch xx b t-                        else return ())-                bs tsRight--        -- Check the body expression.-        (xBody', tBody, effsBody, closBody) -                <- checkExpM defs kenv tenv' xBody--        -- The body type must have data kind.-        kBody   <- checkTypeM defs kenv tBody-        when (not $ isDataKind kBody)-         $ throw $ ErrorLetBodyNotData xx tBody kBody--        -- Cut closure terms due to locally bound value vars.-        -- This also lowers deBruijn indices in un-cut closure terms.-        let clos_cut -                = Set.fromList-                $ mapMaybe (cutTaggedClosureXs bs)-                $ Set.toList -                $ Set.unions (closBody : clossBinds)--        return  ( XLet a (LRec (zip bs xsRight')) xBody'-                , tBody-                , effsBody-                , clos_cut)----- letregion ---------------------------------------checkExpM' defs kenv tenv xx@(XLet a (LLetRegion b bs) x)- = case takeSubstBoundOfBind b of-     Nothing     -> checkExpM defs kenv tenv x-     Just u-      -> do-        -- Check the type on the region binder.-        let k   = typeOfBind b-        checkTypeM defs kenv k--        -- The binder must have region kind.-        when (not $ isRegionKind k)-         $ throw $ ErrorLetRegionNotRegion xx b k--        -- We can't shadow region binders because we might have witnesses-        -- in the environment that conflict with the ones created here.-        when (Env.memberBind b kenv)-         $ throw $ ErrorLetRegionRebound xx b-        -        -- Check the witness types.-        let kenv'       = Env.extend b kenv-        let tenv'       = Env.lift 1 tenv-        mapM_ (checkTypeM defs kenv') $ map typeOfBind bs--        -- Check that the witnesses bound here are for the region,-        -- and they don't conflict with each other.-        checkWitnessBindsM xx u bs--        -- Check the body expression.-        let tenv2       = Env.extends bs tenv'-        (xBody', tBody, effs, clo)  <- checkExpM defs kenv' tenv2 x--        -- The body type must have data kind.-        kBody           <- checkTypeM defs kenv' tBody-        when (not $ isDataKind kBody)-         $ throw $ ErrorLetBodyNotData xx tBody kBody--        -- The bound region variable cannot be free in the body type.-        let fvsT         = freeT Env.empty tBody-        when (Set.member u fvsT)-         $ throw $ ErrorLetRegionFree xx b tBody-        -        -- Delete effects on the bound region from the result.-        let effs'       = Sum.delete (tRead  (TVar u))-                        $ Sum.delete (tWrite (TVar u))-                        $ Sum.delete (tAlloc (TVar u))-                        $ effs--        -- Delete the bound region variable from the closure.-        -- Mask closure terms due to locally bound region vars.-        let c2_cut      = Set.fromList-                        $ mapMaybe (cutTaggedClosureT b)-                        $ Set.toList clo--        return  ( XLet a (LLetRegion b bs) xBody'-                , lowerT 1 tBody-                , lowerT 1 effs'-                , c2_cut)----- withregion ------------------------------------checkExpM' defs kenv tenv xx@(XLet a (LWithRegion u) x)- = do   -- Check the type on the region handle.-        let k   = typeOfBound u-        checkTypeM defs kenv k--        -- The handle must have region kind.-        when (not $ isRegionKind k)-         $ throw $ ErrorWithRegionNotRegion xx u k-        -        -- Check the body expression.-        (xBody', tBody, effs, clo) -               <- checkExpM defs kenv tenv x--        -- The body type must have data kind.-        kBody  <- checkTypeM defs kenv tBody-        when (not $ isDataKind kBody)-         $ throw $ ErrorLetBodyNotData xx tBody kBody-        -        -- Delete effects on the bound region from the result.-        let tu          = TCon $ TyConBound u-        let effs'       = Sum.delete (tRead  tu)-                        $ Sum.delete (tWrite tu)-                        $ Sum.delete (tAlloc tu)-                        $ effs-        -        -- Delete the bound region handle from the closure.-        let clo_masked  = Set.delete (GBoundRgnCon u) clo--        return  ( XLet a (LWithRegion u) xBody'-                , tBody-                , effs'-                , clo_masked)-                ---- case expression -------------------------------checkExpM' defs kenv tenv xx@(XCase a xDiscrim alts)- = do-        -- Check the discriminant.-        (xDiscrim', tDiscrim, effsDiscrim, closDiscrim) -         <- checkExpM defs kenv tenv xDiscrim--        -- Split the type into the type constructor names and type parameters.-        -- Also check that it's algebraic data, and not a function or effect-        -- type etc. -        (nTyCon, tsArgs)-         <- case takeTyConApps tDiscrim of-                Just (tc, ts)-                 | TyConBound (UName n t) <- tc-                 , takeResultKind t == kData-                 -> return (n, ts)-                      -                 | TyConBound (UPrim n t) <- tc-                 , takeResultKind t == kData-                 -> return (n, ts)--                _ -> throw $ ErrorCaseDiscrimNotAlgebraic xx tDiscrim--        -- Get the mode of the data type, -        --   this tells us how many constructors there are.-        mode    -         <- case lookupModeOfDataType nTyCon defs of-             Nothing -> throw $ ErrorCaseDiscrimTypeUndeclared xx tDiscrim-             Just m  -> return m--        -- Check the alternatives.-        (alts', ts, effss, closs)     -                <- liftM unzip4-                $  mapM (checkAltM xx defs kenv tenv tDiscrim tsArgs) alts--        -- There must be at least one alternative-        when (null ts)-         $ throw $ ErrorCaseNoAlternatives xx--        -- All alternative result types must be identical.-        let (tAlt : _)  = ts-        forM_ ts $ \tAlt' -         -> when (not $ equivT tAlt tAlt') -             $ throw $ ErrorCaseAltResultMismatch xx tAlt tAlt'--        -- Check for overlapping alternatives.-        let pats                = [p | AAlt p _ <- alts]-        let psDefaults          = filter isPDefault pats-        let nsCtorsMatched      = mapMaybe takeCtorNameOfAlt alts--        -- Alts overlapping because there are multiple defaults.-        when (length psDefaults > 1)-         $ throw $ ErrorCaseOverlapping xx--        -- Alts overlapping because the same ctor is used multiple times.-        when (length (nub nsCtorsMatched) /= length nsCtorsMatched )-         $ throw $ ErrorCaseOverlapping xx--        -- Check for alts overlapping because a default is not last.-        -- Also check there is at least one alternative.-        (case pats of-          [] -> throw $ ErrorCaseNoAlternatives xx--          _  |  or $ map isPDefault $ init pats -             -> throw $ ErrorCaseOverlapping xx--             |  otherwise-             -> return ())--        -- Check the alternatives are exhaustive.-        (case mode of--          -- Small types have some finite number of constructors.-          DataModeSmall nsCtors-           -- If there is a default alternative then we've covered all the-           -- possibiliies. We know this we've also checked for overlap.-           | any isPDefault [p | AAlt p _ <- alts]-           -> return ()--           -- Look for unmatched constructors.-           | nsCtorsMissing <- nsCtors \\ nsCtorsMatched-           , not $ null nsCtorsMissing-           -> throw $ ErrorCaseNonExhaustive xx nsCtorsMissing--           -- All constructors were matched.-           | otherwise -           -> return ()--          -- Large types have an effectively infinite number of constructors-          -- (like integer literals), so there needs to be a default alt.-          DataModeLarge -           | any isPDefault [p | AAlt p _ <- alts] -> return ()-           | otherwise  -           -> throw $ ErrorCaseNonExhaustiveLarge xx)--        let effsMatch    -                = Sum.singleton kEffect -                $ crushEffect $ tHeadRead tDiscrim--        return  ( XCase a xDiscrim' alts'-                , tAlt-                , Sum.unions kEffect (effsDiscrim : effsMatch : effss)-                , Set.unions         (closDiscrim : closs) )----- type cast ---------------------------------------- Weaken an effect, adding in the given terms.-checkExpM' defs kenv tenv xx@(XCast a c@(CastWeakenEffect eff) x1)- = do   -        -- Check the effect term.-        kEff    <- checkTypeM defs kenv eff-        when (not $ isEffectKind kEff)-         $ throw $ ErrorMaxeffNotEff xx eff kEff--        -- Check the body.-        (x1', t1, effs, clo)    <- checkExpM defs kenv tenv x1--        return  ( XCast a c x1'-                , t1-                , Sum.insert eff effs-                , clo)----- Weaken a closure, adding in the given terms.-checkExpM' defs kenv tenv xx@(XCast a c@(CastWeakenClosure clo2) x1)- = do   -        -- Check the closure term.-        kClo    <- checkTypeM defs kenv clo2-        when (not $ isClosureKind kClo)-         $ throw $ ErrorMaxcloNotClo xx clo2 kClo--        -- The closure supplied to weakclo can only contain Use terms-        -- of region variables.-        clos2-         <- case taggedClosureOfWeakClo clo2 of-             Nothing     -> throw $ ErrorMaxcloMalformed xx clo2-             Just clos2' -> return clos2'--        -- Check the body.-        (x1', t1, effs, clos)   <- checkExpM defs kenv tenv x1--        return  ( XCast a c x1'-                , t1-                , effs-                , Set.union clos clos2)----- Purify an effect, given a witness that it is pure.-checkExpM' defs kenv tenv xx@(XCast a c@(CastPurify w) x1)- = do   tW                   <- checkWitnessM defs kenv tenv w-        (x1', t1, effs, clo) <- checkExpM     defs kenv tenv x1-                -        effs' <- case tW of-                  TApp (TCon (TyConWitness TwConPure)) effMask-                    -> return $ Sum.delete effMask effs-                  _ -> throw  $ ErrorWitnessNotPurity xx w tW--        return  ( XCast a c x1'-                , t1-                , effs'-                , clo)----- Forget a closure, given a witness that it is empty.-checkExpM' defs kenv tenv xx@(XCast a c@(CastForget w) x1)- = do   tW                    <- checkWitnessM defs kenv tenv w-        (x1', t1, effs, clos) <- checkExpM     defs kenv tenv x1--        clos' <- case tW of-                  TApp (TCon (TyConWitness TwConEmpty)) cloMask-                    -> return $ maskFromTaggedSet -                                        (Sum.singleton kClosure cloMask)-                                        clos--                  _ -> throw $ ErrorWitnessNotEmpty xx w tW--        return  ( XCast a c x1'-                , t1-                , effs-                , clos')----- Type and witness expressions can only appear as the arguments --- to  applications.-checkExpM' _defs _kenv _tenv xx@(XType _)-        = throw $ ErrorNakedType xx --checkExpM' _defs _kenv _tenv xx@(XWitness _)-        = throw $ ErrorNakedWitness xx------------------------------------------------------------------------------------- | Check a case alternative.-checkAltM -        :: (Pretty n, Ord n) -        => Exp a n              -- ^ Whole case expression, for error messages.-        -> DataDefs n           -- ^ Data type definitions.-        -> Env n                -- ^ Kind environment.-        -> Env n                -- ^ Type environment.-        -> Type n               -- ^ Type of discriminant.-        -> [Type n]             -- ^ Args to type constructor of discriminant.-        -> Alt a n              -- ^ Alternative to check.-        -> CheckM a n -                ( Alt a n-                , Type n-                , TypeSum n-                , Set (TaggedClosure n))--checkAltM _xx defs kenv tenv _tDiscrim _tsArgs (AAlt PDefault xBody)- = do   (xBody', tBody, effBody, cloBody)-                <- checkExpM defs kenv tenv xBody--        return  ( AAlt PDefault xBody'-                , tBody-                , effBody-                , cloBody)--checkAltM xx defs kenv tenv tDiscrim tsArgs (AAlt (PData uCon bsArg) xBody)- = do   -        -- Take the type of the constructor and instantiate it with the -        -- type arguments we got from the discriminant. -        -- If the ctor type doesn't instantiate then it won't have enough foralls -        -- on the front, which should have been checked by the def checker.-        let tCtor       = typeOfBound uCon-        tCtor_inst      -         <- case instantiateTs tCtor tsArgs of-             Nothing -> throw $ ErrorCaseCannotInstantiate xx tDiscrim tCtor-             Just t  -> return t-        -        -- Split the constructor type into the field and result types.-        let (tsFields_ctor, tResult) -                        = takeTFunArgResult tCtor_inst--        -- The result type of the constructor must match the discriminant type.-        --  If it doesn't then the constructor in the pattern probably isn't for-        --  the discriminant type.-        when (not $ equivT tDiscrim tResult)-         $ throw $ ErrorCaseDiscrimTypeMismatch xx tDiscrim tResult--        -- There must be at least as many fields as variables in the pattern.-        -- It's ok to bind less fields than provided by the constructor.-        when (length tsFields_ctor < length bsArg)-         $ throw $ ErrorCaseTooManyBinders xx uCon -                        (length tsFields_ctor)-                        (length bsArg)--        -- Merge the field types we get by instantiating the constructor-        -- type with possible annotations from the source program.-        -- If the annotations don't match, then we throw an error.-        tsFields        <- zipWithM (mergeAnnot xx)-                            (map typeOfBind bsArg)-                            tsFields_ctor        --        -- Extend the environment with the field types.-        let bsArg'      = zipWith replaceTypeOfBind tsFields bsArg-        let tenv'       = Env.extends bsArg' tenv-        -        -- Check the body in this new environment.-        (xBody', tBody, effsBody, closBody)-                <- checkExpM defs kenv tenv' xBody--        -- Cut closure terms due to locally bound value vars.-        -- This also lowers deBruijn indices in un-cut closure terms.-        let closBody_cut -                = Set.fromList-                $ mapMaybe (cutTaggedClosureXs bsArg')-                $ Set.toList closBody--        return  ( AAlt (PData uCon bsArg') xBody'-                , tBody-                , effsBody-                , closBody_cut)----- | Merge a type annotation on a pattern field with a type we get by---   instantiating the constructor type.-mergeAnnot :: Eq n => Exp a n -> Type n -> Type n -> CheckM a n (Type n)-mergeAnnot xx tAnnot tActual-        -- Annotation is bottom, so just use the real type.-        | isBot tAnnot      = return tActual--        -- Annotation matches actual type, all good.-        | tAnnot == tActual = return tActual--        -- Annotation does not match actual type.-        | otherwise       -        = throw $ ErrorCaseFieldTypeMismatch xx tAnnot tActual------------------------------------------------------------------------------------- | Check the set of witness bindings bound in a letregion for conflicts.-checkWitnessBindsM :: Ord n => Exp a n -> Bound n -> [Bind n] -> CheckM a n ()-checkWitnessBindsM xx nRegion bsWits- = mapM_ (checkWitnessBindM xx nRegion bsWits) bsWits---checkWitnessBindM -        :: Ord n -        => Exp a n-        -> Bound n              -- ^ Region variable bound in the letregion.-        -> [Bind n]             -- ^ Other witness bindings in the same set.-        -> Bind  n              -- ^ The witness binding to check.-        -> CheckM a n ()--checkWitnessBindM xx uRegion bsWit bWit- = let btsWit   -        = [(typeOfBind b, b) | b <- bsWit]--       -- Check the argument of a witness type is for the region we're-       -- introducing here.-       checkWitnessArg t-        = case t of-            TVar u'-             | uRegion /= u'    -> throw $ ErrorLetRegionWitnessOther xx uRegion bWit-             | otherwise        -> return ()--            TCon (TyConBound u')-             | uRegion /= u'    -> throw $ ErrorLetRegionWitnessOther xx uRegion bWit-             | otherwise        -> return ()--            -- The parser should ensure the right of a witness is a -            -- constructor or variable.-            _ -> throw $ ErrorLetRegionWitnessInvalid xx bWit--   in  case typeOfBind bWit of-        TApp (TCon (TyConWitness TwConGlobal))  t2-         -> checkWitnessArg t2--        TApp (TCon (TyConWitness TwConConst))   t2-         | Just bConflict <- L.lookup (tMutable t2) btsWit-         -> throw $ ErrorLetRegionWitnessConflict xx bWit bConflict-         | otherwise    -> checkWitnessArg t2--        TApp (TCon (TyConWitness TwConMutable)) t2-         | Just bConflict <- L.lookup (tConst t2)   btsWit-         -> throw $ ErrorLetRegionWitnessConflict xx bWit bConflict-         | otherwise    -> checkWitnessArg t2--        TApp (TCon (TyConWitness TwConLazy))    t2-         | Just bConflict <- L.lookup (tManifest t2)  btsWit-         -> throw $ ErrorLetRegionWitnessConflict xx bWit bConflict-         | otherwise    -> checkWitnessArg t2--        TApp (TCon (TyConWitness TwConManifest))  t2-         | Just bConflict <- L.lookup (tLazy t2)    btsWit-         -> throw $ ErrorLetRegionWitnessConflict xx bWit bConflict-         | otherwise    -> checkWitnessArg t2--        _ -> throw $ ErrorLetRegionWitnessInvalid xx bWit------------------------------------------------------------------------------------- | Check a type in the exp checking monad.-checkTypeM :: (Ord n, Pretty n) -           => DataDefs n -           -> Env n -           -> Type n -           -> CheckM a n (Kind n)--checkTypeM defs kenv tt- = case T.checkType defs kenv tt of-        Left err        -> throw $ ErrorType err-        Right k         -> return k------------------------------------------------------------------------------------- | Check the type annotation of a let bound variable against the type---   inferred for the right of the binding.---   If the annotation is Bot then we just replace the annotation,---   otherwise it must match that for the right of the binding.-checkLetBindOfTypeM -        :: (Eq n, Ord n, Pretty n) -        => Exp a n -        -> DataDefs n           -- Data type definitions.-        -> Env n                -- Kind environment. -        -> Env n                -- Type environment.-        -> Type n -        -> Bind n -        -> CheckM a n (Bind n, Kind n)--checkLetBindOfTypeM xx defs kenv _tenv tRight b-        -- If the annotation is Bot then just replace it.-        | isBot (typeOfBind b)-        = do    k       <- checkTypeM defs kenv tRight-                return  ( replaceTypeOfBind tRight b -                        , k)--        -- The type of the binder must match that of the right of the binding.-        | not $ equivT (typeOfBind b) tRight-        = throw $ ErrorLetMismatch xx b tRight--        | otherwise-        = do    k       <- checkTypeM defs kenv (typeOfBind b)-                return (b, k)-+-- | Type checker for the Disciple Core language.+module DDC.Core.Check.CheckExp+        ( Config (..)+        , AnTEC  (..)+        , checkExp+        , typeOfExp+        , CheckM+        , checkExpM+        , TaggedClosure(..))+where+import DDC.Core.Predicates+import DDC.Core.Compounds+import DDC.Core.Collect+import DDC.Core.Pretty+import DDC.Core.Exp+import DDC.Core.Check.Error+import DDC.Core.Check.CheckDaCon+import DDC.Core.Check.CheckWitness+import DDC.Core.Check.TaggedClosure+import DDC.Type.Transform.SubstituteT+import DDC.Type.Transform.Crush+import DDC.Type.Transform.Trim+import DDC.Type.Transform.Instantiate+import DDC.Type.Transform.LiftT+import DDC.Type.DataDef+import DDC.Type.Equiv+import DDC.Type.Universe+import DDC.Type.Sum                     as Sum+import DDC.Type.Env                     (Env, KindEnv, TypeEnv)+import DDC.Control.Monad.Check          (throw, result)+import Data.Set                         (Set)+import qualified DDC.Type.Env           as Env+import qualified Data.Set               as Set+import Control.Monad+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. +--+--   If it's good, you get a new version with types attached to all the bound+--   variables, as well its the type, effect and closure. +--+--   If it's bad, you get a description of the error.+--+--   The returned expression has types attached to all variable occurrences, +--   so you can call `typeOfExp` on any open subterm.+--+--   The kinds and types of primitives are added to the environments +--   automatically, you don't need to supply these as part of the +--   starting environments.+--+checkExp +        :: (Ord n, Show n, Pretty n)+        => Config n             -- ^ Static configuration.+        -> KindEnv n            -- ^ Starting Kind environment.+        -> TypeEnv n            -- ^ Strating Type environment.+        -> Exp a n              -- ^ Expression to check.+        -> Either (Error a n)+                  ( Exp (AnTEC a n) n+                  , Type n+                  , Effect n+                  , Closure n)++checkExp !config !kenv !tenv !xx + = result+ $ do   (xx', t, effs, clos) +                <- checkExpM config +                        (Env.union kenv (configPrimKinds config))+                        (Env.union tenv (configPrimTypes config))+                        xx+        return  ( xx'+                , t+                , TSum effs+                , closureOfTaggedSet clos)+++-- | Like `checkExp`, but only return the value type of an expression.+typeOfExp +        :: (Ord n, Pretty n, Show n)+        => Config n             -- ^ Static configuration.+        -> KindEnv n            -- ^ Starting Kind environment+        -> TypeEnv n            -- ^ Starting Type environment.+        -> Exp a n              -- ^ Expression to check.+        -> Either (Error a n) (Type n)+typeOfExp !config !kenv !tenv !xx + = case checkExp config kenv tenv xx of+        Left err           -> Left err+        Right (_, t, _, _) -> Right t+++-- checkExp -------------------------------------------------------------------+-- | Like `checkExp` but using the `CheckM` monad to handle errors.+checkExpM +        :: (Show n, Pretty n, Ord n)+        => Config n             -- ^ Static config.+        -> Env n                -- ^ Kind environment.+        -> Env n                -- ^ Type environment.+        -> Exp a n              -- ^ Expression to check.+        -> CheckM a n +                ( Exp (AnTEC a n) n+                , Type n+                , TypeSum n+                , Set (TaggedClosure n))++checkExpM !config !kenv !tenv !xx+ = {-# SCC checkExpM #-}+   checkExpM' config kenv tenv xx++-- variables ------------------------------------+checkExpM' !_config !_kenv !tenv (XVar a u)+ = case Env.lookup u tenv of+        Nothing -> throw $ ErrorUndefinedVar u UniverseData+        Just t  +         -> returnX a +                (\z -> XVar z u)+                t+                (Sum.empty kEffect)+                (Set.singleton $ taggedClosureOfValBound t u)+++-- constructors ---------------------------------+checkExpM' !config !_kenv !_tenv xx@(XCon a dc)+ = do   +        -- All data constructors need to have valid type annotations.+        when (isBot $ daConType dc)+         $ throw $ ErrorUndefinedCtor xx++        -- Check that the constructor is in the data type declarations.+        checkDaConM config xx dc++        -- Type of the data constructor.+        let tResult     +                = typeOfDaCon dc++        returnX a+                (\z -> XCon z dc)+                tResult+                (Sum.empty kEffect)+                Set.empty+++-- application ------------------------------------+-- value-type application.+--+-- Note: We don't need to substitute into the effect of x1 (effs1)+--       because the body of a type abstraction is required to be pure.+-- +--       We don't need to substitute into the closure either, because+--       the bound type variable is not visible outside the abstraction.+--       thus we can't be sharing objects that have it in its type.+--+checkExpM' !config !kenv !tenv xx@(XApp a x1 (XType t2))+ = do   (x1', t1, effs1, clos1) <- checkExpM  config kenv tenv x1++        -- Check the type argument.+        k2                      <- checkTypeM config kenv t2++        -- Take any Use annots from a region arg.+        --   This always matches because we just checked 't2'+        let Just t2_clo         = taggedClosureOfTyArg kenv t2++        case t1 of+         TForall b11 t12+          | typeOfBind b11 == k2+          -> returnX a+                (\z -> XApp z x1' (XType t2))+                (substituteT b11 t2 t12)+                effs1   +                (clos1 `Set.union` t2_clo)++          | otherwise   -> throw $ ErrorAppMismatch xx (typeOfBind b11) t2+         _              -> throw $ ErrorAppNotFun   xx t1 t2+++-- 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+        case t1 of+         TApp (TApp (TCon (TyConWitness TwConImpl)) t11) t12+          | t11 `equivT` t2   +          -> returnX a+                (\z -> XApp z x1' (XWitness w2))+                t12 effs1 clos1++          | otherwise   -> throw $ ErrorAppMismatch xx t11 t2+         _              -> throw $ ErrorAppNotFun   xx t1 t2+                 ++-- value-value application.+checkExpM' !config !kenv !tenv xx@(XApp a x1 x2)+ = 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+          | t11 `equivT` t2   +          , effs    <- Sum.fromList kEffect  [eff]+          -> returnX a+                (\z -> XApp z x1' x2')+                t12+                (effs1 `Sum.union` effs2 `Sum.union` effs)+                (clos1 `Set.union` clos2)++          | otherwise   -> throw $ ErrorAppMismatch xx t11 t2+         _              -> throw $ ErrorAppNotFun xx t1 t2+++-- spec abstraction -----------------------------+checkExpM' !config !kenv !tenv xx@(XLAM a b1 x2)+ = do   let t1            = typeOfBind b1+        _                 <- checkTypeM config kenv t1++        -- Check the body+        let kenv'         = Env.extend b1 kenv+        let tenv'         = Env.lift   1  tenv+        (x2', t2, e2, c2) <- checkExpM  config kenv' tenv' x2+        k2                <- checkTypeM config kenv' t2++        when (Env.memberBind b1 kenv)+         $ throw $ ErrorLamShadow xx b1++        -- The body of a spec abstraction must be pure.+        when (e2 /= Sum.empty kEffect)+         $ throw $ ErrorLamNotPure xx True (TSum e2)++        -- The body of a spec abstraction must have data kind.+        when (not $ isDataKind k2)+         $ throw $ ErrorLamBodyNotData xx b1 t2 k2++        -- Mask closure terms due to locally bound region vars.+        let c2_cut      = Set.fromList+                        $ mapMaybe (cutTaggedClosureT b1)+                        $ Set.toList c2++        returnX a+                (\z -> XLAM z b1 x2')+                (TForall b1 t2)+                (Sum.empty kEffect)+                c2_cut+         ++-- function abstraction -------------------------+checkExpM' !config !kenv !tenv xx@(XLam a b1 x2)+ = do   +        -- Check the type of the binder.+        let t1  =  typeOfBind b1+        k1      <- checkTypeM config kenv t1++        -- Check the body.+        let tenv'            =  Env.extend b1 tenv+        (x2', t2, e2, c2)    <- checkExpM  config kenv tenv' x2   ++        -- The typing rules guarantee that the checked type of an +        -- expression is well kinded, but we need to check it again+        -- to find out what that kind is.+        k2      <- checkTypeM config kenv t2++        -- The form of the function constructor depends on what universe the +        -- binder is in.+        case universeFromType2 k1 of++         -- This is a data abstraction.+         Just UniverseData++          -- The body of a data abstraction must accept data.+          |  not $ isDataKind k1+          -> throw $ ErrorLamBindNotData xx t1 k1++          -- The body of a data abstraction must produce data.+          |  not $ isDataKind k2+          -> throw $ ErrorLamBodyNotData xx b1 t2 k2 ++          -- Looks good.+          |  otherwise+          -> let +                 -- Cut closure terms due to locally bound value vars.+                 -- This also lowers deBruijn indices in un-cut closure terms.+                 c2_cut  = Set.fromList+                         $ mapMaybe (cutTaggedClosureX b1)+                         $ Set.toList c2++                 -- Trim the closure before we annotate the returned function+                 -- type with it. This should always succeed because trimClosure+                 -- only returns Nothing if the closure is miskinded, and we've+                 -- 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+                  = Just $ tBot kClosure++                  | otherwise+                  = trimClosure $ closureOfTaggedSet c2_cut++             in  returnX a+                        (\z -> XLam z b1 x2')+                        (tFun t1 (TSum e2) c2_captured t2)+                        (Sum.empty kEffect)+                        c2_cut++         -- 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)++          -- The body of a witness abstraction must produce data.+          | not $ isDataKind k2      +          -> throw $ ErrorLamBodyNotData xx b1 t2 k2++          -- Looks good.+          | otherwise                +          ->    returnX a+                        (\z -> XLam z b1 x2')+                        (tImpl t1 t2)+                        (Sum.empty kEffect)+                        c2++         _ -> throw $ ErrorMalformedType xx k1+++-- let --------------------------------------------+checkExpM' !config !kenv !tenv xx@(XLet a lts x2)+ | case lts of+        LLet{}  -> True+        LRec{}  -> True+        _       -> False++ = do+        -- Check the bindings+        (lts', bs', effs12, clo12)+                <- checkLetsM xx config kenv tenv lts++        -- Check the body expression.+        let tenv1  = Env.extends bs' tenv+        (x2', t2, effs2, c2)    <- checkExpM config kenv tenv1 x2++        -- The body should have data kind.+        k2       <- checkTypeM config kenv t2+        when (not $ isDataKind k2)+         $ throw $ ErrorLetBodyNotData xx t2 k2++        -- Mask closure terms due to locally bound value vars.+        let c2_cut      = Set.fromList+                        $ mapMaybe (cutTaggedClosureXs bs')+                        $ Set.toList c2++        returnX a+                (\z -> XLet z lts' x2')+                t2+                (effs12 `Sum.union` effs2)+                (clo12  `Set.union` c2_cut)+++-- letregion --------------------------------------+checkExpM' !config !kenv !tenv xx@(XLet a (LLetRegions bsRgn bsWit) x)+ = case takeSubstBoundsOfBinds bsRgn of+    []   -> checkExpM config kenv tenv x     +    us   -> do+        -- +        let depth = length $ map isBAnon bsRgn++        -- Check the type on the region binders.+        let ks    = map typeOfBind bsRgn+        mapM_ (checkTypeM config kenv) ks++        -- The binders must have region kind.+        when (any (not . isRegionKind) ks) +         $ throw $ ErrorLetRegionsNotRegion xx bsRgn ks++        -- We can't shadow region binders because we might have witnesses+        -- in the environment that conflict with the ones created here.+        let rebounds = filter (flip Env.memberBind kenv) bsRgn+        when (not $ null rebounds)+         $ throw $ ErrorLetRegionsRebound xx rebounds+        +        -- Check the witness types.+        let kenv'       = Env.extends bsRgn kenv+        let tenv'       = Env.lift depth tenv+        mapM_ (checkTypeM config kenv') $ map typeOfBind bsWit++        -- Check that the witnesses bound here are for the region,+        -- and they don't conflict with each other.+        checkWitnessBindsM kenv xx us bsWit++        -- Check the body expression.+        let tenv2       = Env.extends bsWit tenv'+        (xBody', tBody, effs, clo)  <- checkExpM config kenv' tenv2 x++        -- The body type must have data kind.+        kBody           <- checkTypeM config kenv' tBody+        when (not $ isDataKind kBody)+         $ throw $ ErrorLetBodyNotData xx tBody kBody++        -- The bound region variable cannot be free in the body type.+        let fvsT         = freeT Env.empty tBody+        when (any (flip Set.member fvsT) us)+         $ throw $ ErrorLetRegionFree xx bsRgn tBody+        +        -- Delete effects on the bound region from the result.+        let delEff es u = Sum.delete (tRead  (TVar u))+                        $ Sum.delete (tWrite (TVar u))+                        $ Sum.delete (tAlloc (TVar u))+                        $ es+        let effs'       = foldl delEff effs us ++        -- Delete the bound region variable from the closure.+        -- Mask closure terms due to locally bound region vars.+        let cutClo c r  = mapMaybe (cutTaggedClosureT r) c+        let c2_cut      = Set.fromList +                        $ foldl cutClo (Set.toList clo) bsRgn++        returnX a+                (\z -> XLet z (LLetRegions bsRgn bsWit) xBody')+                (lowerT depth tBody)+                (lowerT depth effs')+                c2_cut+++-- withregion -----------------------------------+checkExpM' !config !kenv !tenv xx@(XLet a (LWithRegion u) x)+ = do+        -- The handle must have region kind.+        (case Env.lookup u kenv of+          Nothing -> throw $ ErrorUndefinedVar u UniverseSpec++          Just k  |  not $ isRegionKind k+                  -> throw $ ErrorWithRegionNotRegion xx u k++          _       -> return ())+        +        -- Check the body expression.+        (xBody', tBody, effs, clo) +               <- checkExpM config kenv tenv x++        -- The body type must have data kind.+        kBody  <- checkTypeM config kenv tBody+        when (not $ isDataKind kBody)+         $ throw $ ErrorLetBodyNotData xx tBody kBody+        +        -- The bound region variable cannot be free in the body type.+        let tcs         = supportTyCon+                        $ support Env.empty Env.empty tBody+        when (Set.member u tcs)+         $ throw $ ErrorWithRegionFree xx u tBody++        -- Delete effects on the bound region from the result.+        let tu          = TCon $ TyConBound u kRegion+        let effs'       = Sum.delete (tRead  tu)+                        $ Sum.delete (tWrite tu)+                        $ Sum.delete (tAlloc tu)+                        $ effs+        +        -- Delete the bound region handle from the closure.+        let clo_masked  = Set.delete (GBoundRgnCon u) clo++        returnX a+                (\z -> XLet z (LWithRegion u) xBody')+                tBody+                effs'+                clo_masked+                ++-- case expression ------------------------------+checkExpM' !config !kenv !tenv xx@(XCase a xDiscrim alts)+ = do   +        -- Check the discriminant.+        (xDiscrim', tDiscrim, effsDiscrim, closDiscrim) +         <- checkExpM config kenv tenv xDiscrim++        -- Split the type into the type constructor names and type parameters.+        -- Also check that it's algebraic data, and not a function or effect+        -- type etc. +        (mmode, tsArgs)+         <- case takeTyConApps tDiscrim of+                Just (tc, ts)+                 | TyConSpec TcConUnit         <- tc+                 -> return ( Just (DataModeSmall [])+                           , [] )+                        -- ISSUE #269: Refactor DataModeSmall to hold DaCons instead of names.+                        --  The DataModeSmall should hold DaCons instead of+                        --  names, as we don't have a name for Unit.++                 | TyConBound (UName nTyCon) k <- tc+                 , takeResultKind k == kData+                 -> return ( lookupModeOfDataType nTyCon (configPrimDataDefs config)+                           , ts )+                      +                 | TyConBound (UPrim nTyCon _) k <- tc+                 , takeResultKind k == kData+                 -> return ( lookupModeOfDataType nTyCon (configPrimDataDefs config)+                           , ts )++                _ -> throw $ ErrorCaseScrutineeNotAlgebraic xx tDiscrim++        -- Get the mode of the data type, +        --   this tells us how many constructors there are.+        mode    +         <- case mmode of+             Nothing -> throw $ ErrorCaseScrutineeTypeUndeclared xx tDiscrim+             Just m  -> return m++        -- Check the alternatives.+        (alts', ts, effss, closs)     +                <- liftM unzip4+                $  mapM (checkAltM xx config kenv tenv tDiscrim tsArgs) alts++        -- There must be at least one alternative+        when (null ts)+         $ throw $ ErrorCaseNoAlternatives xx++        -- All alternative result types must be identical.+        let (tAlt : _)  = ts+        forM_ ts $ \tAlt' +         -> when (not $ equivT tAlt tAlt') +             $ throw $ ErrorCaseAltResultMismatch xx tAlt tAlt'++        -- Check for overlapping alternatives.+        let pats                = [p | AAlt p _ <- alts]+        let psDefaults          = filter isPDefault pats+        let nsCtorsMatched      = mapMaybe takeCtorNameOfAlt alts++        -- Alts overlapping because there are multiple defaults.+        when (length psDefaults > 1)+         $ throw $ ErrorCaseOverlapping xx++        -- Alts overlapping because the same ctor is used multiple times.+        when (length (nub nsCtorsMatched) /= length nsCtorsMatched )+         $ throw $ ErrorCaseOverlapping xx++        -- Check for alts overlapping because a default is not last.+        -- Also check there is at least one alternative.+        (case pats of+          [] -> throw $ ErrorCaseNoAlternatives xx++          _  |  Just patsInit <- takeInit pats+             ,  or $ map isPDefault $ patsInit+             -> throw $ ErrorCaseOverlapping xx++             |  otherwise+             -> return ())++        -- Check the alternatives are exhaustive.+        (case mode of++          -- Small types have some finite number of constructors.+          DataModeSmall nsCtors+           -- If there is a default alternative then we've covered all the+           -- possibiliies. We know this we've also checked for overlap.+           | any isPDefault [p | AAlt p _ <- alts]+           -> return ()++           -- Look for unmatched constructors.+           | nsCtorsMissing <- nsCtors \\ nsCtorsMatched+           , not $ null nsCtorsMissing+           -> throw $ ErrorCaseNonExhaustive xx nsCtorsMissing++           -- All constructors were matched.+           | otherwise +           -> return ()++          -- Large types have an effectively infinite number of constructors+          -- (like integer literals), so there needs to be a default alt.+          DataModeLarge +           | any isPDefault [p | AAlt p _ <- alts] -> return ()+           | otherwise  +           -> throw $ ErrorCaseNonExhaustiveLarge xx)++        let effsMatch    +                = Sum.singleton kEffect +                $ crushEffect $ tHeadRead tDiscrim++        returnX a+                (\z -> XCase z xDiscrim' alts')+                tAlt+                (Sum.unions kEffect (effsDiscrim : effsMatch : effss))+                (Set.unions         (closDiscrim : closs))+++-- type cast -------------------------------------+-- Weaken an effect, adding in the given terms.+checkExpM' !config !kenv !tenv xx@(XCast a (CastWeakenEffect eff) x1)+ = do+        -- Check the effect term.+        kEff    <- checkTypeM config kenv eff+        when (not $ isEffectKind kEff)+         $ throw $ ErrorWeakEffNotEff xx eff kEff++        -- Check the body.+        (x1', t1, effs, clo)    <- checkExpM config kenv tenv x1+        let c'                  = CastWeakenEffect eff++        returnX a+                (\z -> XCast z c' x1')+                t1+                (Sum.insert eff effs)+                clo+++-- Weaken a closure, adding in the given terms.+checkExpM' !config !kenv !tenv (XCast a (CastWeakenClosure xs) x1)+ = do+        -- Check the contained expressions.+        (xs', closs)+                <- liftM unzip+                $ mapM (checkArgM config kenv tenv) xs++        -- Check the body.+        (x1', t1, effs, clos)   <- checkExpM config kenv tenv x1+        let c'                  = CastWeakenClosure xs'++        returnX a+                (\z -> XCast z c' x1')+                t1+                effs+                (Set.unions (clos : closs))+++-- 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+        (x1', t1, effs, clo) <- checkExpM     config kenv tenv x1+                +        effs' <- case tW of+                  TApp (TCon (TyConWitness TwConPure)) effMask+                    -> return $ Sum.delete effMask effs+                  _ -> throw  $ ErrorWitnessNotPurity xx w tW++        let c'  = CastPurify w++        returnX a+                (\z -> XCast z c' x1')+                t1 effs' clo+++-- 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++        clos' <- case tW of+                  TApp (TCon (TyConWitness TwConEmpty)) cloMask+                    -> return $ maskFromTaggedSet +                                        (Sum.singleton kClosure cloMask)+                                        clos++                  _ -> throw $ ErrorWitnessNotEmpty xx w tW++        let c'  = CastForget w++        returnX a+                (\z -> XCast z c' x1')+                t1 effs clos'+++-- Type and witness expressions can only appear as the arguments +-- to  applications.+checkExpM' !_config !_kenv !_tenv xx@(XType _)+        = throw $ ErrorNakedType xx ++checkExpM' !_config !_kenv !_tenv xx@(XWitness _)+        = throw $ ErrorNakedWitness xx++checkExpM' _ _ _ _+        = error "checkExpM: bogus warning killer"+++-- | Like `checkExp` but we allow naked types and witnesses.+checkArgM +        :: (Show n, Pretty n, Ord n)+        => Config n             -- ^ Static config.+        -> Env n                -- ^ Kind environment.+        -> Env n                -- ^ Type environment.+        -> Exp a n              -- ^ Expression to check.+        -> CheckM a n +                ( Exp (AnTEC a n) n+                , Set (TaggedClosure n))++checkArgM !config !kenv !tenv !xx+ = case xx of+        XType t+         -> do  checkTypeM config kenv t+                let Just clo = taggedClosureOfTyArg kenv t++                return  ( XType t+                        , clo)++        XWitness w+         -> do  checkWitnessM config kenv tenv w+                return  ( XWitness w+                        , Set.empty)++        _ -> do+                (xx', _, _, clos) <- checkExpM config kenv tenv xx+                return  ( xx'+                        , clos)+++-- | Helper function for building the return value of checkExpM'+--   It builts the AnTEC annotation and attaches it to the new AST node,+--   as well as returning the current effect and closure in the appropriate+--   form as part of the tuple.+returnX :: Ord n +        => a+        -> (AnTEC a n -> Exp (AnTEC a n) n)+        -> Type n +        -> TypeSum n+        -> Set (TaggedClosure n)+        -> CheckM a n +                ( Exp (AnTEC a n) n+                , Type n+                , TypeSum n+                , Set (TaggedClosure n))++returnX !a !f !t !es !cs+ = let  e       = TSum es+        c       = closureOfTaggedSet cs+   in   return  (f (AnTEC t e c a)+                , t, es, cs)+{-# INLINE returnX #-}++-------------------------------------------------------------------------------+-- | Check some let bindings.+checkLetsM +        :: (Show n, Pretty n, Ord n)+        => Exp a n              -- ^ Enclosing expression, for error messages.+        -> Config n             -- ^ Static config.+        -> Env n                -- ^ Kind environment.+        -> Env n                -- ^ Type environment.+        -> Lets a n+        -> CheckM a n+                ( Lets (AnTEC a n) n+                , [Bind n]+                , TypeSum n+                , Set (TaggedClosure n))++checkLetsM !xx !config !kenv !tenv (LLet mode b11 x12)+ = do   +        -- Check the right of the binding.+        (x12', t12, effs12, clo12)  +         <- checkExpM config kenv tenv x12++        -- Check binder annotation against the type we inferred for the right.+        (b11', k11')    +         <- checkLetBindOfTypeM xx config kenv tenv t12 b11++        -- The right of the binding should have data kind.+        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'+                , [b11']+                , effs12+                , clo12)++-- letrec ---------------------------------------+checkLetsM !xx !config !kenv !tenv (LRec bxs)+ = do   +        let (bs, xs)    = unzip bxs++        -- No named binders can be multiply defined.+        (case duplicates $ filter isBName bs of+          []    -> return ()+          b : _ -> throw $ ErrorLetrecRebound xx b)++        -- Check the types on all the binders.+        ks              <- mapM (checkTypeM config kenv) +                        $  map typeOfBind bs++        -- Check all the binders have data kind.+        zipWithM_ (\b k+         -> when (not $ isDataKind k)+                $ throw $ ErrorLetBindingNotData xx b k)+                bs ks++        -- All right hand sides need to be lambdas.+        forM_ xs $ \x +         -> when (not $ (isXLam x || isXLAM x))+                $ throw $ ErrorLetrecBindingNotLambda xx x++        -- All variables are in scope in all right hand sides.+        let tenv'       = Env.extends bs tenv++        -- Check the right hand sides.+        (xsRight', tsRight, _effssBinds, clossBinds) +                <- liftM unzip4 $ mapM (checkExpM config kenv tenv') xs++        -- Check annots on binders against inferred types of the bindings.+        zipWithM_ (\b t+                -> if not $ equivT (typeOfBind b) t+                        then throw $ ErrorLetMismatch xx b t+                        else return ())+                bs tsRight++        -- Cut closure terms due to locally bound value vars.+        let clos_cut +                = Set.fromList+                $ mapMaybe (cutTaggedClosureXs bs)+                $ Set.toList +                $ Set.unions clossBinds++        return  ( LRec (zip bs xsRight')+                , zipWith replaceTypeOfBind tsRight bs+                , Sum.empty kEffect+                , clos_cut)++checkLetsM _xx _config _kenv _tenv _lts+        = error "checkLetsM: case should have been handled in checkExpM"+++-- | Take elements of a list that have more than once occurrence.+duplicates :: Eq a => [a] -> [a]+duplicates []           = []+duplicates (x : xs)+        | L.elem x xs   = x : duplicates (filter (/= x) xs)+        | otherwise     = duplicates xs+++-------------------------------------------------------------------------------+-- | Check a case alternative.+checkAltM +        :: (Show n, Pretty n, Ord n) +        => Exp a n              -- ^ Whole case expression, for error messages.+        -> Config n             -- ^ Data type definitions.+        -> Env n                -- ^ Kind environment.+        -> Env n                -- ^ Type environment.+        -> Type n               -- ^ Type of discriminant.+        -> [Type n]             -- ^ Args to type constructor of discriminant.+        -> Alt a n              -- ^ Alternative to check.+        -> CheckM a n +                ( Alt (AnTEC a n) n+                , Type n+                , TypeSum n+                , Set (TaggedClosure n))++checkAltM !_xx !config !kenv !tenv !_tDiscrim !_tsArgs (AAlt PDefault xBody)+ = do   (xBody', tBody, effBody, cloBody)+                <- checkExpM config kenv tenv xBody++        return  ( AAlt PDefault xBody'+                , tBody+                , effBody+                , cloBody)++checkAltM !xx !config !kenv !tenv !tDiscrim !tsArgs (AAlt (PData dc bsArg) xBody)+ = do   +        let Just aCase  = takeAnnotOfExp xx++        -- If the data constructor isn't defined then the spread +        --  transform won't have given it a proper type.+        --  Note that we can't simply check whether the constructor is in the+        --  environment because literals like 42# never are.+        (if isBot (daConType dc)+                then throw $ ErrorUndefinedCtor $ XCon aCase dc+                else return ())++        -- Take the type of the constructor and instantiate it with the +        -- type arguments we got from the discriminant. +        -- If the ctor type doesn't instantiate then it won't have enough foralls +        -- on the front, which should have been checked by the def checker.+        let tCtor = daConType dc++        tCtor_inst      +         <- case instantiateTs tCtor tsArgs of+             Nothing -> throw $ ErrorCaseCannotInstantiate xx tDiscrim tCtor+             Just t  -> return t+        +        -- Split the constructor type into the field and result types.+        let (tsFields_ctor, tResult) +                        = takeTFunArgResult tCtor_inst++        -- The result type of the constructor must match the discriminant type.+        --  If it doesn't then the constructor in the pattern probably isn't for+        --  the discriminant type.+        when (not $ equivT tDiscrim tResult)+         $ throw $ ErrorCaseScrutineeTypeMismatch xx tDiscrim tResult++        -- There must be at least as many fields as variables in the pattern.+        -- It's ok to bind less fields than provided by the constructor.+        when (length tsFields_ctor < length bsArg)+         $ throw $ ErrorCaseTooManyBinders xx dc+                        (length tsFields_ctor)+                        (length bsArg)++        -- Merge the field types we get by instantiating the constructor+        -- type with possible annotations from the source program.+        -- If the annotations don't match, then we throw an error.+        tsFields        <- zipWithM (mergeAnnot xx)+                            (map typeOfBind bsArg)+                            tsFields_ctor        ++        -- Extend the environment with the field types.+        let bsArg'      = zipWith replaceTypeOfBind tsFields bsArg+        let tenv'       = Env.extends bsArg' tenv+        +        -- Check the body in this new environment.+        (xBody', tBody, effsBody, closBody)+                <- checkExpM config kenv tenv' xBody++        -- Cut closure terms due to locally bound value vars.+        -- This also lowers deBruijn indices in un-cut closure terms.+        let closBody_cut +                = Set.fromList+                $ mapMaybe (cutTaggedClosureXs bsArg')+                $ Set.toList closBody++        return  ( AAlt (PData dc bsArg') xBody'+                , tBody+                , effsBody+                , closBody_cut)+++-- | Merge a type annotation on a pattern field with a type we get by+--   instantiating the constructor type.+mergeAnnot :: Eq n => Exp a n -> Type n -> Type n -> CheckM a n (Type n)+mergeAnnot !xx !tAnnot !tActual+        -- Annotation is bottom, so just use the real type.+        | isBot tAnnot      = return tActual++        -- Annotation matches actual type, all good.+        | tAnnot == tActual = return tActual++        -- Annotation does not match actual type.+        | otherwise       +        = throw $ ErrorCaseFieldTypeMismatch xx tAnnot tActual+++-------------------------------------------------------------------------------+-- | Check the set of witness bindings bound in a letregion for conflicts.+checkWitnessBindsM +        :: (Show n, Ord n) +        => KindEnv n +        -> Exp a n +        -> [Bound n] +        -> [Bind n] +        -> CheckM a n ()++checkWitnessBindsM !kenv !xx !nRegions !bsWits+ = mapM_ (checkWitnessBindM kenv xx nRegions bsWits) bsWits+++checkWitnessBindM +        :: (Show n, Ord n)+        => Env n+        -> Exp a n+        -> [Bound n]            -- ^ Region variables bound in the letregion.+        -> [Bind n]             -- ^ Other witness bindings in the same set.+        -> Bind  n              -- ^ The witness binding to check.+        -> CheckM a n ()++checkWitnessBindM !kenv !xx !uRegions !bsWit !bWit+ = let btsWit   +        = [(typeOfBind b, b) | b <- bsWit]++       -- Check the argument of a witness type is for the region we're+       -- introducing here.+       checkWitnessArg t+        = case t of+            TVar u'+             | all (/= u') uRegions -> throw $ ErrorLetRegionsWitnessOther xx uRegions bWit+             | otherwise            -> return ()++            TCon (TyConBound u' _)+             | all (/= u') uRegions -> throw $ ErrorLetRegionsWitnessOther xx uRegions bWit+             | otherwise            -> return ()+            +            -- The parser should ensure the right of a witness is a +            -- constructor or variable.+            _ -> throw $ ErrorLetRegionWitnessInvalid xx bWit+            +       inEnv t+        = case t of+            TVar u'                | Env.member u' kenv -> True+            TCon (TyConBound u' _) | Env.member u' kenv -> True+            _                                           -> False +       +   in  case typeOfBind bWit of+        TApp (TCon (TyConWitness TwConGlobal))  t2+         -> checkWitnessArg t2++        TApp (TCon (TyConWitness TwConConst))   t2+         | Just bConflict <- L.lookup (tMutable t2) btsWit+         -> throw $ ErrorLetRegionWitnessConflict xx bWit bConflict+         | otherwise    -> checkWitnessArg t2++        TApp (TCon (TyConWitness TwConMutable)) t2+         | Just bConflict <- L.lookup (tConst t2)   btsWit+         -> throw $ ErrorLetRegionWitnessConflict xx bWit bConflict+         | otherwise    -> checkWitnessArg t2++        TApp (TCon (TyConWitness TwConLazy))    t2+         | Just bConflict <- L.lookup (tManifest t2)  btsWit+         -> throw $ ErrorLetRegionWitnessConflict xx bWit bConflict+         | otherwise    -> checkWitnessArg t2++        TApp (TCon (TyConWitness TwConManifest))  t2+         | Just bConflict <- L.lookup (tLazy t2)    btsWit+         -> throw $ ErrorLetRegionWitnessConflict xx bWit bConflict+         | otherwise    -> checkWitnessArg t2+         +        (takeTyConApps -> Just (TyConWitness (TwConDistinct 2), [t1, t2]))+         | inEnv t1  -> checkWitnessArg t2+         | inEnv t2  -> checkWitnessArg t1+         | t1 /= t2  -> mapM_ checkWitnessArg [t1, t2]+         | otherwise -> throw $ ErrorLetRegionWitnessInvalid xx bWit++        (takeTyConApps -> Just (TyConWitness (TwConDistinct _), ts))+          -> mapM_ checkWitnessArg ts++        _ -> throw $ ErrorLetRegionWitnessInvalid xx bWit+++-------------------------------------------------------------------------------+-- | Check the type annotation of a let bound variable against the type+--   inferred for the right of the binding.+--   If the annotation is Bot then we just replace the annotation,+--   otherwise it must match that for the right of the binding.+checkLetBindOfTypeM +        :: (Ord n, Show n, Pretty n) +        => Exp a n +        -> Config n             -- Data type definitions.+        -> Env n                -- Kind environment. +        -> Env n                -- Type environment.+        -> Type n +        -> Bind n +        -> CheckM a n (Bind n, Kind n)++checkLetBindOfTypeM !xx !config !kenv !_tenv !tRight b+        -- If the annotation is Bot then just replace it.+        | isBot (typeOfBind b)+        = do    k       <- checkTypeM config kenv tRight+                return  ( replaceTypeOfBind tRight b +                        , k)++        -- The type of the binder must match that of the right of the binding.+        | not $ equivT (typeOfBind b) tRight+        = throw $ ErrorLetMismatch xx b tRight++        | otherwise+        = do    k       <- checkTypeM config kenv (typeOfBind b)+                return (b, k)

@@ -0,0 +1,159 @@++module DDC.Core.Check.CheckModule+        ( checkModule+        , checkModuleM)+where+import DDC.Core.Module+import DDC.Core.Exp+import DDC.Core.Check.CheckExp+import DDC.Core.Check.Error+import DDC.Type.Compounds+import DDC.Base.Pretty+import DDC.Type.Equiv+import DDC.Type.Env             (KindEnv, TypeEnv)+import DDC.Control.Monad.Check  (result, throw)+import Data.Map                 (Map)+import qualified DDC.Type.Check as T+import qualified DDC.Type.Env   as Env+import qualified Data.Map       as Map+++-- Wrappers -------------------------------------------------------------------+-- | Type check a module.+--+--   If it's good, you get a new version with types attached to all the bound+--   variables+--+--   If it's bad, you get a description of the error.+checkModule+        :: (Ord n, Show n, Pretty n)+        => Config n             -- ^ Static configuration.+        -> Module a n           -- ^ Module to check.+        -> Either (Error a n) (Module (AnTEC a n) n)++checkModule !config !xx +        = result +        $ checkModuleM +                config +                (configPrimKinds config)+                (configPrimTypes config)+                xx+++-- checkModule ----------------------------------------------------------------+-- | Like `checkModule` but using the `CheckM` monad to handle errors.+checkModuleM +        :: (Ord n, Show n, Pretty n)+        => Config n             -- ^ Static configuration.+        -> KindEnv n            -- ^ Starting kind environment.+        -> TypeEnv n            -- ^ Starting type environment.+        -> Module a n           -- ^ Module to check.+        -> CheckM a n (Module (AnTEC a n) n)++checkModuleM !config !kenv !tenv mm@ModuleCore{}+ = do   +        -- Convert the imported kind and type map to a list of binds.+        let bksImport  = [BName n k |  (n, (_, k)) <- Map.toList $ moduleImportKinds mm]+        let btsImport  = [BName n t |  (n, (_, t)) <- Map.toList $ moduleImportTypes mm]++        -- Check the imported kinds and types.+        --  The imported types are in scope in both imported and exported signatures.+        mapM_ (checkTypeM config kenv) $ map typeOfBind bksImport+        let kenv' = Env.union kenv $ Env.fromList bksImport++        mapM_ (checkTypeM config kenv') $ map typeOfBind btsImport+        let tenv' = Env.union tenv $ Env.fromList btsImport++        -- Check the sigs for exported things.+        mapM_ (checkTypeM config kenv') $ Map.elems $ moduleExportKinds mm+        mapM_ (checkTypeM config kenv') $ Map.elems $ moduleExportTypes mm+                +        -- Check our let bindings.+        (x', _, _effs, _) <- checkExpM config kenv' tenv' (moduleBody mm)++        -- Check that each exported signature matches the type of its binding.+        envDef  <- checkModuleBinds (moduleExportKinds mm) (moduleExportTypes mm) x'++        -- Check that all exported bindings are defined by the module.+        mapM_ (checkBindDefined envDef) $ Map.keys $ moduleExportTypes mm++        -- Return the checked bindings as they have explicit type annotations.+        let mm'         = mm { moduleBody = x' }+        return mm'+++-- | Check that the exported signatures match the types of their bindings.+checkModuleBinds +        :: Ord n+        => Map n (Kind n)               -- ^ Kinds of exported types.+        -> Map n (Type n)               -- ^ Types of exported values.+        -> Exp (AnTEC a n) n+        -> CheckM a n (TypeEnv n)       -- ^ Environment of top-level bindings+                                        --   defined by the module++checkModuleBinds !ksExports !tsExports !xx+ = case xx of+        XLet _ (LLet _ b _) x2     +         -> do  checkModuleBind  ksExports tsExports b+                env     <- checkModuleBinds ksExports tsExports x2+                return  $ Env.extend b env++        XLet _ (LRec bxs) x2+         -> do  mapM_ (checkModuleBind ksExports tsExports) $ map fst bxs+                env     <- checkModuleBinds ksExports tsExports x2+                return  $ Env.extends (map fst bxs) env++        XLet _ (LLetRegions _ _) x2+         ->     checkModuleBinds ksExports tsExports x2++        _ ->    return Env.empty+++-- | If some bind is exported, then check that it matches the exported version.+checkModuleBind +        :: Ord n+        => Map n (Kind n)       -- ^ Kinds of exported types.+        -> Map n (Type n)       -- ^ Types of exported values.+        -> Bind n+        -> CheckM a n ()++checkModuleBind !_ksExports !tsExports !b+ | BName n tDef <- b+ = case Map.lookup n tsExports of+        Nothing                 -> return ()+        Just tExport +         | equivT tDef tExport  -> return ()+         | otherwise            -> throw $ ErrorExportMismatch n tExport tDef++ -- Only named bindings can be exported, + --  so we don't need to worry about non-named ones.+ | otherwise+ = return ()+++-- | Check that a top-level binding is actually defined by the module.+checkBindDefined +        :: Ord n+        => TypeEnv n            -- ^ Types defined by the module.+        -> n                    -- ^ Name of an exported binding.+        -> CheckM a n ()++checkBindDefined env n+ = case Env.lookup (UName n) env of+        Just _  -> return ()+        _       -> throw $ ErrorExportUndefined n+++-------------------------------------------------------------------------------+-- | Check a type in the exp checking monad.+checkTypeM :: (Ord n, Show n, Pretty n) +           => Config n +           -> KindEnv n +           -> Type n +           -> CheckM a n (Kind n)++checkTypeM !config !kenv !tt+ = case T.checkType (configPrimDataDefs config) kenv tt of+        Left err        -> throw $ ErrorType err+        Right k         -> return k+

@@ -1,31 +1,34 @@- -- | Type checker for witness expressions. module DDC.Core.Check.CheckWitness-        ( checkWitness+        ( Config(..)+        , configOfProfile++        , checkWitness         , typeOfWitness         , typeOfWiCon         , typeOfWbCon          , CheckM-        , checkWitnessM)+        , checkWitnessM++        , checkTypeM) where-import DDC.Core.DataDef import DDC.Core.Exp import DDC.Core.Pretty import DDC.Core.Check.Error-import DDC.Core.Check.ErrorMessage      ()+import DDC.Core.Check.ErrorMessage              ()+import DDC.Type.DataDef import DDC.Type.Transform.SubstituteT import DDC.Type.Compounds-import DDC.Type.Predicates-import DDC.Type.Equiv-import DDC.Type.Transform.LiftT-import DDC.Type.Sum                     as Sum-import DDC.Type.Env                     (Env)-import DDC.Type.Check.Monad             (result, throw)-import DDC.Base.Pretty                  ()-import qualified DDC.Type.Env           as Env-import qualified DDC.Type.Check         as T-import qualified DDC.Type.Check.Monad   as G+import DDC.Type.Universe+import DDC.Type.Sum                             as Sum+import DDC.Type.Env                             (KindEnv, TypeEnv)+import DDC.Control.Monad.Check                  (throw, result)+import DDC.Base.Pretty                          ()+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. @@ -33,6 +36,46 @@ 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. --   @@ -44,16 +87,20 @@ --   The returned expression has types attached to all variable occurrences,  --   so you can call `typeOfWitness` on any open subterm. --+--   The kinds and types of primitives are added to the environments +--   automatically, you don't need to supply these as part of the +--   starting environments.+-- checkWitness-        :: (Ord n, Pretty n)-        => DataDefs n           -- ^ Data type definitions.-        -> Env n                -- ^ Kind Environment.-        -> Env n                -- ^ Type Environment.+        :: (Ord n, Show n, Pretty n)+        => 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) -checkWitness defs kenv tenv xx-        = result $ checkWitnessM defs kenv tenv xx+checkWitness config kenv tenv xx+        = result $ checkWitnessM config kenv tenv xx   -- | Like `checkWitness`, but check in an empty environment.@@ -63,78 +110,38 @@ --   This attachment is performed by `checkWitness` above. -- typeOfWitness -        :: (Ord n, Pretty n) -        => DataDefs n+        :: (Ord n, Show n, Pretty n) +        => Config n         -> Witness n          -> Either (Error a n) (Type n) -typeOfWitness defs ww +typeOfWitness config ww          = result -        $ checkWitnessM defs Env.empty Env.empty ww+        $ checkWitnessM config Env.empty Env.empty ww   ------------------------------------------------------------------------------ -- | Like `checkWitness` but using the `CheckM` monad to manage errors. checkWitnessM -        :: (Ord n, Pretty n)-        => DataDefs n           -- ^ Data type definitions.-        -> Env n                -- ^ Kind environment.-        -> Env n                -- ^ Type environment.+        :: (Ord n, Show n, Pretty n)+        => Config n             -- ^ Data type definitions.+        -> KindEnv n            -- ^ Kind environment.+        -> TypeEnv n            -- ^ Type environment.         -> Witness n            -- ^ Witness to check.         -> CheckM a n (Type n) -checkWitnessM _defs _kenv tenv (WVar u)- = do   let tBound      = typeOfBound u-        let mtEnv       = Env.lookup u tenv--        let mkResult-             -- When annotation on the bound is bot,-             --  then use the type from the environment.-             | Just tEnv    <- mtEnv-             , isBot tBound-             = return tEnv--             -- The bound has an explicit type annotation,-             --  which matches the one from the environment.-             -- -             --  When the bound is a deBruijn index we need to lift the-             --  annotation on the original binder through any lambdas-             --  between the binding occurrence and the use.-             | Just tEnv    <- mtEnv-             , UIx i _      <- u-             , equivT tBound (liftT (i + 1) tEnv) -             = return tBound--             -- The bound has an explicit type annotation,-             --  which matches the one from the environment.-             | Just tEnv    <- mtEnv-             , equivT tBound tEnv-             = return tEnv--             -- The bound has an explicit type annotation,-             --  which does not match the one from the environment.-             --  This shouldn't happen because the parser doesn't add non-bot-             --  annotations to bound variables.-             | Just tEnv    <- mtEnv-             = throw $ ErrorVarAnnotMismatch u tEnv--             -- Variable not in environment, so use annotation.-             --  This happens when checking open terms.-             | otherwise-             = return tBound-        -        tResult  <- mkResult-        return tResult-+checkWitnessM !_config !_kenv !tenv (WVar u)+ = case Env.lookup u tenv of+        Nothing -> throw $ ErrorUndefinedVar u UniverseWitness+        Just t  -> return t -checkWitnessM _defs _kenv _tenv (WCon wc)+checkWitnessM !_config !_kenv !_tenv (WCon wc)  = return $ typeOfWiCon wc-   --- value-type application-checkWitnessM defs kenv tenv ww@(WApp w1 (WType t2))- = do   t1      <- checkWitnessM  defs kenv tenv w1-        k2      <- checkTypeM     defs kenv t2+-- witness-type application+checkWitnessM !config !kenv !tenv ww@(WApp w1 (WType t2))+ = do   t1      <- checkWitnessM  config kenv tenv w1+        k2      <- checkTypeM     config kenv t2         case t1 of          TForall b11 t12           |  typeOfBind b11 == k2@@ -144,9 +151,9 @@          _              -> throw $ ErrorWAppNotCtor  ww t1 t2  -- witness-witness application-checkWitnessM defs kenv tenv ww@(WApp w1 w2)- = do   t1      <- checkWitnessM defs kenv tenv w1-        t2      <- checkWitnessM defs kenv tenv w2+checkWitnessM !config !kenv !tenv ww@(WApp w1 w2)+ = do   t1      <- checkWitnessM config kenv tenv w1+        t2      <- checkWitnessM config kenv tenv w2         case t1 of          TApp (TApp (TCon (TyConWitness TwConImpl)) t11) t12           |  t11 == t2   @@ -156,9 +163,9 @@          _              -> throw $ ErrorWAppNotCtor  ww t1 t2  -- witness joining-checkWitnessM defs kenv tenv ww@(WJoin w1 w2)- = do   t1      <- checkWitnessM defs kenv tenv w1-        t2      <- checkWitnessM defs kenv tenv w2+checkWitnessM !config !kenv !tenv ww@(WJoin w1 w2)+ = do   t1      <- checkWitnessM config kenv tenv w1+        t2      <- checkWitnessM config kenv tenv w2         case (t1, t2) of          (  TApp (TCon (TyConWitness TwConPure)) eff1           , TApp (TCon (TyConWitness TwConPure)) eff2)@@ -173,8 +180,8 @@          _ -> throw $ ErrorCannotJoin ww w1 t1 w2 t2  -- embedded types-checkWitnessM defs kenv _tenv (WType t)- = checkTypeM defs kenv t+checkWitnessM !config !kenv !_tenv (WType t)+ = checkTypeM config kenv t           -- | Take the type of a witness constructor.@@ -182,7 +189,7 @@ typeOfWiCon wc  = case wc of     WiConBuiltin wb -> typeOfWbCon wb-    WiConBound u    -> typeOfBound u+    WiConBound _ t  -> t   -- | Take the type of a builtin witness constructor.@@ -199,14 +206,14 @@ -- checkType ------------------------------------------------------------------ -- | Check a type in the exp checking monad. checkTypeM -        :: (Ord n, Pretty n) -        => DataDefs n -        -> Env n +        :: (Ord n, Show n, Pretty n) +        => Config n +        -> KindEnv n          -> Type n          -> CheckM a n (Kind n) -checkTypeM defs kenv tt- = case T.checkType defs kenv tt of+checkTypeM config kenv tt+ = case T.checkType (configPrimDataDefs config) kenv tt of         Left err        -> throw $ ErrorType err         Right k         -> return k 

@@ -3,47 +3,65 @@         (Error(..)) where import DDC.Core.Exp+import DDC.Type.Universe import qualified DDC.Type.Check as T   -- | All the things that can go wrong when type checking an expression --   or witness. data Error a n+        -- Type -------------------------------------------         -- | Found a kind error when checking a type.         = ErrorType         { errorTypeError        :: T.Error n } -        -- | Found a malformed expression, -        --   and we don't have a more specific diagnosis.-        | ErrorMalformedExp-        { errorChecking         :: Exp a n }-         -- | Found a malformed type,         --   and we don't have a more specific diagnosis.         | ErrorMalformedType         { errorChecking         :: Exp a n         , errorType             :: Type n } -        -- | Found a naked `XType` that wasn't the argument of an application.-        | ErrorNakedType-        { errorChecking         :: Exp a n } -        -- | Found a naked `XWitness` that wasn't the argument of an application.-        | ErrorNakedWitness+        -- Module -----------------------------------------+        -- | Exported value is undefined.+        | ErrorExportUndefined+        { errorName             :: n }++        -- | Type signature of exported binding does not match the type at+        --   the definition site.+        | ErrorExportMismatch+        { errorName             :: n+        , errorExportType       :: Type n+        , errorDefType          :: Type n }+++        -- Exp --------------------------------------------+        -- | Found a malformed expression, +        --   and we don't have a more specific diagnosis.+        | ErrorMalformedExp         { errorChecking         :: Exp a n } +         -- Var ---------------------------------------------        -- | A bound occurrence of a variable who's type annotation does not match+        -- | An undefined type variable.+        | ErrorUndefinedVar+        { errorBound            :: Bound n +        , errorUniverse         :: Universe }++        -- | A bound occurrence of a variable whose type annotation does not match         --   the corresponding annotation in the environment.         | ErrorVarAnnotMismatch         { errorBound            :: Bound n+        , errorTypeAnnot        :: Type n         , errorTypeEnv          :: Type n } +         -- Con --------------------------------------------         -- | A data constructor that wasn't in the set of data definitions.         | ErrorUndefinedCtor         { errorChecking         :: Exp a n } +         -- Application ------------------------------------         -- | A function application where the parameter and argument don't match.         | ErrorAppMismatch@@ -68,6 +86,7 @@         -- | A type or witness abstraction where the body has a visible side effect.         | ErrorLamNotPure         { errorChecking         :: Exp a n+        , errorSpecOrWit        :: Bool         , errorEffect           :: Effect n }          -- | A value function where the parameter does not have data kind.@@ -140,26 +159,32 @@         { errorChecking         :: Exp a n          , errorExp              :: Exp a n } +        -- | A recursive let-expression that has more than one binding+        --   with the same name.+        | ErrorLetrecRebound+        { errorChecking         :: Exp a n+        , errorBind             :: Bind n } +         -- Letregion ---------------------------------------        -- | A letregion-expression where the bound variable does not have-        --   region kind.-        | ErrorLetRegionNotRegion+        -- | A letregion-expression where the some of the bound variables do not+        --   have region kind.+        | ErrorLetRegionsNotRegion         { errorChecking         :: Exp a n-        , errorBind             :: Bind n-        , errorKind             :: Kind n }+        , errorBinds            :: [Bind n]+        , errorKinds            :: [Kind n] } -        -- | A letregion-expression that tried to shadow a pre-existing named-        --   region variable.-        | ErrorLetRegionRebound+        -- | A letregion-expression that tried to shadow some pre-existing named+        --   region variables.+        | ErrorLetRegionsRebound         { errorChecking         :: Exp a n-        , errorBind             :: Bind n }+        , errorBinds            :: [Bind n] } -        -- | A letregion-expression where the bound region variable is free in-        --  the type of the body.+        -- | A letregion-expression where some of the the bound region variables+        --   are free in the type of the body.         | ErrorLetRegionFree         { errorChecking         :: Exp a n-        , errorBind             :: Bind n+        , errorBinds            :: [Bind n]         , errorType             :: Type n }          -- | A letregion-expression that tried to create a witness with an @@ -176,18 +201,33 @@          -- | A letregion-expression where a bound witnesses was not for the         --   the region variable being introduced.-        | ErrorLetRegionWitnessOther+        | ErrorLetRegionsWitnessOther         { errorChecking         :: Exp a n-        , errorBoundRegion      :: Bound n+        , errorBoundRegions     :: [Bound n]         , errorBindWitness      :: Bind  n } +        -- | A letregion-expression where the witness binding references some+        --   free region variable that is not the one being introduced.+        | ErrorLetRegionWitnessFree+        { errorChecking         :: Exp a n+        , errorBindWitness      :: Bind n }+        ++        -- Withregion -------------------------------------         -- | A withregion-expression where the handle does not have region kind.         | ErrorWithRegionNotRegion         { errorChecking         :: Exp a n         , errorBound            :: Bound n         , errorKind             :: Kind n } +        -- | A letregion-expression where some of the the bound region variables+        --   are free in the type of the body.+        | ErrorWithRegionFree+        { errorChecking         :: Exp a n+        , errorBound            :: Bound n+        , errorType             :: Type n } +         -- Witnesses --------------------------------------         -- | A witness application where the argument type does not match         --   the parameter type.@@ -224,16 +264,16 @@           -- Case Expressions --------------------------------        -- | A case-expression where the discriminant type is not algebraic.-        | ErrorCaseDiscrimNotAlgebraic+        -- | A case-expression where the scrutinee type is not algebraic.+        | ErrorCaseScrutineeNotAlgebraic         { errorChecking         :: Exp a n-        , errorTypeDiscrim      :: Type n }+        , errorTypeScrutinee    :: Type n } -        -- | A case-expression where the discriminant type is not in our set+        -- | A case-expression where the scrutinee type is not in our set         --   of data type declarations.-        | ErrorCaseDiscrimTypeUndeclared+        | ErrorCaseScrutineeTypeUndeclared         { errorChecking         :: Exp a n -        , errorTypeDiscrim      :: Type n }+        , errorTypeScrutinee    :: Type n }          -- | A case-expression with no alternatives.         | ErrorCaseNoAlternatives@@ -258,22 +298,22 @@         -- | A case-expression where one of the patterns has too many binders.         | ErrorCaseTooManyBinders         { errorChecking         :: Exp a n-        , errorCtorBound        :: Bound n+        , errorCtorDaCon        :: DaCon n         , errorCtorFields       :: Int         , errorPatternFields    :: Int }          -- | A case-expression where the pattern types could not be instantiated-        --   with the arguments of the discriminant type.+        --   with the arguments of the scrutinee type.         | ErrorCaseCannotInstantiate         { errorChecking         :: Exp a n-        , errorTypeCtor         :: Type n-        , errorTypeDiscrim      :: Type n }+        , errorTypeScrutinee    :: Type n +        , errorTypeCtor         :: Type n } -        -- | A case-expression where the type of the discriminant does not match+        -- | A case-expression where the type of the scrutinee does not match         --   the type of the pattern.-        | ErrorCaseDiscrimTypeMismatch+        | ErrorCaseScrutineeTypeMismatch         { errorChecking         :: Exp a n-        , errorTypeDiscrim      :: Type n+        , errorTypeScrutinee    :: Type n         , errorTypePattern      :: Type n }          -- | A case-expression where the annotation on a pattern variable binder@@ -292,22 +332,22 @@           -- Casts -------------------------------------------        -- | A maxeff-cast where the type provided does not have effect kind.-        | ErrorMaxeffNotEff+        -- | A weakeff-cast where the type provided does not have effect kind.+        | ErrorWeakEffNotEff         { errorChecking         :: Exp a n         , errorEffect           :: Effect n         , errorKind             :: Kind n } -        -- | A maxclo-cast where the type provided does not have closure kind.-        | ErrorMaxcloNotClo-        { errorChecking         :: Exp a n-        , errorClosure          :: Closure n-        , errorKind             :: Kind n } -        -- | A maxclo-case where the closure provided is malformed. -        --   It can only contain `Use` terms.-        | ErrorMaxcloMalformed-        { errorChecking         :: Exp a n -        , errorClosure          :: Closure n }+        -- Types ------------------------------------------+        -- | Found a naked `XType` that wasn't the argument of an application.+        | ErrorNakedType+        { errorChecking         :: Exp a n }+++        -- Witnesses --------------------------------------+        -- | Found a naked `XWitness` that wasn't the argument of an application.+        | ErrorNakedWitness+        { errorChecking         :: Exp a n }         deriving (Show) 

@@ -1,4 +1,3 @@-{-# OPTIONS_HADDOCK hide #-} -- | Errors produced when checking core expressions. module DDC.Core.Check.ErrorMessage         (Error(..))@@ -6,9 +5,11 @@ import DDC.Core.Pretty import DDC.Core.Check.Error import DDC.Type.Compounds+import DDC.Type.Universe  -instance (Pretty n, Eq n) => Pretty (Error a n) where+instance (Show n, Eq n, Pretty n) +       => Pretty (Error a n) where  ppr err   = case err of         ErrorType err'  -> ppr err'@@ -21,22 +22,38 @@                  , empty                  , text "with: "                        <> align (ppr xx) ] -        ErrorNakedType xx-         -> vcat [ text "Found naked type in core program."-                 , empty-                 , text "with: "                        <> align (ppr xx) ]+        -- Modules ---------------------------------------+        ErrorExportUndefined n+         -> vcat [ text "Exported value '" <> ppr n <> text "' is undefined." ] -        ErrorNakedWitness xx-         -> vcat [ text "Found naked witness in core program."-                 , empty-                 , text "with: "                        <> align (ppr xx) ]+        ErrorExportMismatch n tExport tDef+         -> vcat [ text "Type of exported value does not match type of definition."+                 , text "             with binding: "   <> ppr n+                 , text "           type of export: "   <> ppr tExport+                 , text "       type of definition: "   <> ppr tDef ] +         -- Variable ----------------------------------------        ErrorVarAnnotMismatch u t+        ErrorUndefinedVar  u universe+         -> case universe of+             UniverseSpec+               -> vcat [ text "Undefined spec variable: "  <> ppr u ]++             UniverseData+               -> vcat [ text "Undefined value variable: " <> ppr u ]++             UniverseWitness+               -> vcat [ text "Undefined witness variable: " <> ppr u ]++             -- Universes other than the above don't have variables,+             -- but let's not worry about that here.+             _ -> vcat [ text "Undefined variable: "    <> ppr u ]++        ErrorVarAnnotMismatch u tEnv tAnnot          -> vcat [ text "Type mismatch in annotation."                  , text "             Variable: "       <> ppr u-                 , text "       has annotation: "       <> (ppr $ typeOfBound u)-                 , text " which conflicts with: "       <> ppr t+                 , text "       has annotation: "       <> ppr tAnnot+                 , text " which conflicts with: "       <> ppr tEnv                  , text "     from environment." ]  @@ -68,11 +85,14 @@                  , text "  is already in the environment."                  , text "with: "                        <> align (ppr xx) ] -        ErrorLamNotPure xx eff-         -> vcat [ text "Impure type abstraction"-                 , text "           has effect: "       <> ppr eff-                 , empty-                 , 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"+                , text "           has effect: "       <> ppr eff+                , empty+                , text "with: "                        <> align (ppr xx) ]                                    ErrorLamBindNotData xx t1 k1@@ -158,29 +178,33 @@                  , empty                  , text "with: "                        <> align (ppr xx) ] +        ErrorLetrecRebound xx b+         -> vcat [ text "Redefined binder '" <> ppr b <> text "' in letrec."+                 , empty+                 , text "with: "                        <> align (ppr xx) ]          -- Letregion ---------------------------------------        ErrorLetRegionNotRegion xx b k-         -> vcat [ text "Letregion binder does not have region kind."-                 , text "        Region binder: "       <> ppr b-                 , text "             has kind: "       <> ppr k-                 , text "       but is must be: %" +        ErrorLetRegionsNotRegion xx bs ks+         -> vcat [ text "Letregion binders do not have region kind."+                 , text "        Region binders: "       <> (hcat $ map ppr bs)+                 , text "             has kinds: "       <> (hcat $ map ppr ks)+                 , text "       but they must all be: %"                   , empty-                 , text "with: "                        <> align (ppr xx) ]+                 , text "with: "                         <> align (ppr xx) ] -        ErrorLetRegionRebound xx b-         -> vcat [ text "Region variable shadows existing one."-                 , text "           Region variable: "  <> ppr b-                 , text "     is already in environment"+        ErrorLetRegionsRebound xx bs+         -> vcat [ text "Region variables shadow existing ones."+                 , text "           Region variables: "  <> (hcat $ map ppr bs)+                 , text "     are already in environment"                  , empty-                 , text "with: "                        <> align (ppr xx) ]+                 , text "with: "                         <> align (ppr xx) ] -        ErrorLetRegionFree xx b t-         -> vcat [ text "Region variable escapes scope of letregion."-                 , text "       The region variable: "  <> ppr b-                 , text "  is free in the body type: "  <> ppr t+        ErrorLetRegionFree xx bs t+         -> vcat [ text "Region variables escape scope of letregion."+                 , text "       The region variables: "  <> (hcat $ map ppr bs)+                 , text "  is free in the body type: "   <> ppr t                  , empty-                 , text "with: "                        <> align (ppr xx) ]+                 , text "with: "                         <> align (ppr xx) ]                  ErrorLetRegionWitnessInvalid xx b          -> vcat [ text "Invalid witness type with letregion."@@ -196,12 +220,27 @@                  , empty                  , text "with: "                        <> align (ppr xx) ] -        ErrorLetRegionWitnessOther xx b1 b2-         -> vcat [ text "Witness type is not for bound region."-                 , text "      letregion binds: "       <> ppr b1+        ErrorLetRegionsWitnessOther xx bs1 b2+         -> vcat [ text "Witness type is not for bound regions."+                 , text "      letregion binds: "       <> (hsep $ map ppr bs1)                  , text "  but witness type is: "       <> ppr b2                  , empty                  , text "with: "                        <> align (ppr xx) ]+                 +        ErrorLetRegionWitnessFree xx b+         -> vcat [ text "Witness type references a free region variable."+                 , text "  the binding: "               <> ppr b +                 , text "  contains free region variables."+                 , empty+                 , text "with: "                        <> align (ppr xx) ]+                 +        -- Withregion -------------------------------------+        ErrorWithRegionFree xx u t+         -> vcat [ text "Region handle escapes scope of withregion."+                 , text "         The region handle: "   <> ppr u+                 , text "  is used in the body type: "   <> ppr t+                 , empty+                 , text "with: "                         <> align (ppr xx) ]          ErrorWithRegionNotRegion xx u k          -> vcat [ text "Withregion handle does not have region kind."@@ -251,15 +290,15 @@           -- Case Expressions --------------------------------        ErrorCaseDiscrimNotAlgebraic xx tDiscrim-         -> vcat [ text "Discriminant of case expression is not algebraic data."-                 , text "     Discriminant type: "      <> ppr tDiscrim+        ErrorCaseScrutineeNotAlgebraic xx tScrutinee+         -> vcat [ text "Scrutinee of case expression is not algebraic data."+                 , text "     Scrutinee type: "         <> ppr tScrutinee                  , empty                  , text "with: "                        <> align (ppr xx) ]         -        ErrorCaseDiscrimTypeUndeclared xx tDiscrim-         -> vcat [ text "Type of discriminant does not have a data declaration."-                 , text "     Discriminant type: "      <> ppr tDiscrim+        ErrorCaseScrutineeTypeUndeclared xx tScrutinee+         -> vcat [ text "Type of scrutinee does not have a data declaration."+                 , text "     Scrutinee type: "         <> ppr tScrutinee                  , empty                  , text "with: "                        <> align (ppr xx) ] @@ -295,18 +334,18 @@                  , empty                  , text "with: "                        <> align (ppr xx) ] -        ErrorCaseCannotInstantiate xx tCtor tDiscrim-         -> vcat [ text "Cannot instantiate constructor type with discriminant type args."+        ErrorCaseCannotInstantiate xx tScrutinee tCtor+         -> vcat [ text "Cannot instantiate constructor type with scrutinee type args."                  , text " Either the constructor has an invalid type,"-                 , text " or the type of the discriminant does not match the type of the pattern."+                 , text " or the type of the scrutinee does not match the type of the pattern."+                 , text "        Scrutinee type: "      <> ppr tScrutinee                  , text "      Constructor type: "      <> ppr tCtor-                 , text "     Discriminant type: "      <> ppr tDiscrim                  , empty                  , text "with: "                        <> align (ppr xx) ] -        ErrorCaseDiscrimTypeMismatch xx tDiscrim tPattern-         -> vcat [ text "Discriminant type does not match result of pattern type."-                 , text "     Discriminant type: "      <> ppr tDiscrim+        ErrorCaseScrutineeTypeMismatch xx tScrutinee tPattern+         -> vcat [ text "Scrutinee type does not match result of pattern type."+                 , text "        Scrutinee type: "      <> ppr tScrutinee                  , text "          Pattern type: "      <> ppr tPattern                  , empty                  , text "with: "                        <> align (ppr xx) ]@@ -327,24 +366,23 @@           -- Casts -------------------------------------------        ErrorMaxeffNotEff xx eff k-         -> vcat [ text "Type provided for a 'maxeff' does not have effect kind."+        ErrorWeakEffNotEff xx eff k+         -> vcat [ text "Type provided for a 'weakeff' does not have effect kind."                  , text "           Type: "             <> ppr eff                  , text "       has kind: "             <> ppr k                  , empty                  , text "with: "                        <> align (ppr xx) ]--        ErrorMaxcloNotClo xx clo k-         -> vcat [ text "Type provided for a 'maxclo' does not have closure kind."-                 , text "           Type: "             <> ppr clo-                 , text "       has kind: "             <> ppr k+       +        -- Type -------------------------------------------+        ErrorNakedType xx+         -> vcat [ text "Found naked type in core program."                  , empty                  , text "with: "                        <> align (ppr xx) ] -        ErrorMaxcloMalformed xx clo-         -> vcat [ text "Type provided for a 'maxclo' is malformed."-                 , text "        Closure: "             <> ppr clo-                 , text " can only contain 'Use' terms."+        -- Witness ----------------------------------------+        ErrorNakedWitness xx+         -> vcat [ text "Found naked witness in core program."                  , empty                  , text "with: "                        <> align (ppr xx) ]-       ++

@@ -11,7 +11,7 @@         , cutTaggedClosureXs         , cutTaggedClosureT) where-import DDC.Type.Transform.LowerT+import DDC.Type.Transform.LiftT import DDC.Type.Transform.Trim import DDC.Type.Compounds import DDC.Type.Predicates@@ -20,6 +20,8 @@ import Control.Monad import Data.Maybe import Data.Set                 (Set)+import DDC.Type.Env             (Env)+import qualified DDC.Type.Env   as Env import qualified DDC.Type.Sum   as Sum import qualified Data.Set       as Set @@ -62,9 +64,9 @@         GBoundRgnCon u      -> text "CLORGNCON" <+> ppr u  -instance LowerT TaggedClosure where- lowerAtDepthT n d cc-  = let down = lowerAtDepthT n d+instance Ord n => MapBoundT TaggedClosure n where+ mapBoundAtDepthT f d cc+  = let down = mapBoundAtDepthT f d     in case cc of         GBoundVal u ts    -> GBoundVal (down u) (down ts)         GBoundRgnVar u1   -> GBoundRgnVar (down u1)@@ -77,7 +79,7 @@  = case gg of         GBoundVal _ clos  -> TSum $ clos         GBoundRgnVar u    -> tUse (TVar u)-        GBoundRgnCon u    -> tUse (TCon (TyConBound u))+        GBoundRgnCon u    -> tUse (TCon (TyConBound u kRegion))   -- | Convert a set of tagged closures to a regular closure by dropping the@@ -92,31 +94,35 @@ -- | Yield the tagged closure of a value variable. taggedClosureOfValBound          :: (Ord n, Pretty n) -        => Bound n  -> TaggedClosure n+        => Type n -> Bound n  -> TaggedClosure n -taggedClosureOfValBound u+taggedClosureOfValBound t u          = GBoundVal u          $ Sum.singleton kClosure -        $ (let clo = tDeepUse $ typeOfBound u+        $ (let clo = tDeepUse t            in  fromMaybe clo (trimClosure clo))  --- | Yield the tagged closure of a type argument.+-- | Yield the tagged closure of a type argument,+--   or `Nothing` for out-of-scope type vars. taggedClosureOfTyArg          :: (Ord n, Pretty n) -        => Type n -> Set (TaggedClosure n)+        => Env n -> Type n -> Maybe (Set (TaggedClosure n)) -taggedClosureOfTyArg tt+taggedClosureOfTyArg kenv tt  = case tt of         TVar u-         |   isRegionKind (typeOfBound u)-         ->  Set.singleton $ GBoundRgnVar u--        TCon (TyConBound u)-         |   isRegionKind (typeOfBound u)-         ->  Set.singleton $ GBoundRgnCon u+         -> case Env.lookup u kenv of+                Nothing           -> Nothing+                Just k  +                 | isRegionKind k -> Just $ Set.singleton $ GBoundRgnVar u+                 | otherwise      -> Just Set.empty+                                                    +        TCon (TyConBound u k)+         |   isRegionKind k+         ->  Just $ Set.singleton $ GBoundRgnCon u -        _ -> Set.empty+        _ -> Just $ Set.empty   -- | Convert the closure provided as a 'weakclo' to tagged form.@@ -136,8 +142,8 @@             Just (TyConSpec TcConUse, [TVar u])               -> Just $ GBoundRgnVar u -            Just (TyConSpec TcConUse, [TCon (TyConBound u)])-              -> Just $ GBoundRgnVar u+            Just (TyConSpec TcConUse, [TCon (TyConBound u _)])+              -> Just $ GBoundRgnCon u              _ -> Nothing @@ -163,7 +169,7 @@             | otherwise         -> Just gg             GBoundRgnCon u-            | Sum.elem (tUse (TCon (TyConBound u))) ts1     +            | Sum.elem (tUse (TCon (TyConBound u kRegion))) ts1                                      -> Nothing             | otherwise         -> Just gg 

@@ -1,253 +1,18 @@  -- | Collecting sets of variables and constructors. module DDC.Core.Collect-        ( freeT+        ( -- * Free Variables+          freeT         , freeX-        , collectBound-        , collectSpecBinds)-where-import DDC.Type.Compounds-import DDC.Core.Exp-import DDC.Type.Env                     (Env)-import qualified DDC.Type.Env           as Env-import qualified DDC.Type.Sum           as Sum-import qualified Data.Set               as Set-import Data.Set                         (Set) ---- freeT ------------------------------------------------------------------------- | Collect the free Spec variables in a thing (level-1).-freeT   :: (BindStruct c, Ord n) -        => Env n -> c n -> Set (Bound n)-freeT tenv xx = Set.unions $ map (freeOfTreeT tenv) $ slurpBindTree xx--freeOfTreeT :: Ord n => Env n -> BindTree n -> Set (Bound n)-freeOfTreeT kenv tt- = case tt of-        BindDef way bs ts-         |  BoundSpec   <- boundLevelOfBindWay way-         ,  kenv'       <- Env.extends bs kenv-         -> Set.unions $ map (freeOfTreeT kenv') ts--        BindDef _ _ ts-         -> Set.unions $ map (freeOfTreeT kenv) ts--        BindUse BoundSpec u-         | Env.member u kenv -> Set.empty-         | otherwise         -> Set.singleton u-        _                    -> Set.empty----- freeX ------------------------------------------------------------------------- | Collect the free Data and Witness variables in a thing (level-0).-freeX   :: (BindStruct c, Ord n) -        => Env n -> c n -> Set (Bound n)-freeX tenv xx = Set.unions $ map (freeOfTreeX tenv) $ slurpBindTree xx--freeOfTreeX :: Ord n => Env n -> BindTree n -> Set (Bound n)-freeOfTreeX tenv tt- = case tt of-        BindDef way bs ts-         |  BoundExpWit <- boundLevelOfBindWay way-         ,  tenv'       <- Env.extends bs tenv-         -> Set.unions $ map (freeOfTreeX tenv') ts--        BindDef _ _ ts-         -> Set.unions $ map (freeOfTreeX  tenv) ts--        BindUse BoundExpWit u-         | Env.member u tenv -> Set.empty-         | otherwise         -> Set.singleton u-        _                    -> Set.empty----- collectBound ------------------------------------------------------------------ | Collect all the bound variables in a thing, ---   independent of whether they are free or not.-collectBound :: (BindStruct c, Ord n) => c n -> Set (Bound n)-collectBound -        = Set.unions . map collectBoundOfTree . slurpBindTree --collectBoundOfTree :: Ord n => BindTree n -> Set (Bound n)-collectBoundOfTree tt- = case tt of-        BindDef _ _ ts  -> Set.unions $ map collectBoundOfTree ts-        BindUse _ u     -> Set.singleton u-        BindCon _ u     -> Set.singleton u----- collectSpecBinds -------------------------------------------------------------- | Collect all the Spec binders in a thing.-collectSpecBinds :: (BindStruct c, Ord n) => c n -> [Bind n]-collectSpecBinds -        = concatMap collectSpecBindsOfTree . slurpBindTree-        --collectSpecBindsOfTree :: Ord n => BindTree n -> [Bind n]-collectSpecBindsOfTree tt- = case tt of-        BindDef way bs ts-         |   BoundSpec <- boundLevelOfBindWay way-         ->  concat ( bs-                    : map collectSpecBindsOfTree ts)--         | otherwise-         ->  concatMap collectSpecBindsOfTree ts--        _ -> []------------------------------------------------------------------------------------- | A description of the binding structure of some type or expression.-data BindTree n-        -- | An abstract binding expression.-        = BindDef BindWay    [Bind n] [BindTree n]--        -- | Use of a variable.-        | BindUse BoundLevel (Bound n)--        -- | Use of a constructor.-        | BindCon BoundLevel (Bound n)-        deriving (Eq, Show)----- | Describes how a variable was bound.-data BindWay-        = BindForall-        | BindLAM-        | BindLam-        | BindLet-        | BindLetRec-        | BindLetRegion-        | BindLetRegionWith-        | BindCasePat-        deriving (Eq, Show)----- | What level this binder is at.-data BoundLevel-        = BoundSpec-        | BoundExpWit-        deriving (Eq, Show)----- | Get the `BoundLevel` corresponding to a `BindWay`.-boundLevelOfBindWay :: BindWay -> BoundLevel-boundLevelOfBindWay way- = case way of-        BindForall              -> BoundSpec-        BindLAM                 -> BoundSpec-        BindLam                 -> BoundExpWit-        BindLet                 -> BoundExpWit-        BindLetRec              -> BoundExpWit-        BindLetRegion           -> BoundSpec-        BindLetRegionWith       -> BoundExpWit-        BindCasePat             -> BoundExpWit----- BindStruct ------------------------------------------------------------------class BindStruct (c :: * -> *) where- slurpBindTree :: c n -> [BindTree n]---instance BindStruct Type where- slurpBindTree tt-  = case tt of-        TVar u          -> [BindUse BoundSpec u]-        TCon tc         -> slurpBindTree tc-        TForall b t     -> [bindDefT BindForall [b] [t]]-        TApp t1 t2      -> slurpBindTree t1 ++ slurpBindTree t2-        TSum ts         -> concatMap slurpBindTree $ Sum.toList ts---instance BindStruct TyCon where- slurpBindTree tc-  = case tc of-        TyConBound u    -> [BindCon BoundSpec u]-        _               -> []---instance BindStruct (Exp a) where- slurpBindTree xx-  = case xx of-        XVar _ u        -> [BindUse BoundExpWit u]-        XCon _ u        -> [BindCon BoundExpWit u]-        XApp _ x1 x2    -> slurpBindTree x1 ++ slurpBindTree x2-        XLAM _ b x      -> [bindDefT BindLAM [b] [x]]-        XLam _ b x      -> [bindDefX BindLam [b] [x]]      --        XLet _ (LLet m b x1) x2-         -> slurpBindTree m-         ++ slurpBindTree x1-         ++ [bindDefX BindLet [b] [x2]]--        XLet _ (LRec bxs) x2-         -> [bindDefX BindLetRec -                     (map fst bxs) -                     (map snd bxs ++ [x2])]-        -        XLet _ (LLetRegion b bs) x2-         -> [ BindDef  BindLetRegion [b]-             [bindDefX BindLetRegionWith bs [x2]]]--        XLet _ (LWithRegion u) x2-         -> BindUse BoundExpWit u : slurpBindTree x2--        XCase _ x alts  -> slurpBindTree x ++ concatMap slurpBindTree alts-        XCast _ c x     -> slurpBindTree c ++ slurpBindTree x-        XType t         -> slurpBindTree t-        XWitness w      -> slurpBindTree w---instance BindStruct LetMode where- slurpBindTree mm-  = case mm of-        LetLazy (Just w) -> slurpBindTree w-        _                -> []---instance BindStruct Cast where- slurpBindTree cc-  = case cc of-        CastWeakenEffect eff    -> slurpBindTree eff-        CastWeakenClosure clo   -> slurpBindTree clo-        CastPurify w            -> slurpBindTree w-        CastForget w            -> slurpBindTree w---instance BindStruct (Alt a) where- slurpBindTree alt-  = case alt of-        AAlt PDefault x-         -> slurpBindTree x--        AAlt (PData _ bs) x-         -> [bindDefX BindCasePat bs [x]]---instance BindStruct Witness where- slurpBindTree ww-  = case ww of-        WVar u          -> [BindUse BoundExpWit u]-        WCon{}          -> []-        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.-bindDefX :: BindStruct c -         => BindWay -> [Bind n] -> [c n] -> BindTree n-bindDefX way bs xs-        = BindDef way bs-        $   concatMap (slurpBindTree . typeOfBind) bs-        ++  concatMap slurpBindTree xs----- | Helper for constructing the `BindTree` for a type binder.-bindDefT :: BindStruct c-         => BindWay -> [Bind n] -> [c n] -> BindTree n-bindDefT way bs xs-        = BindDef way bs $ concatMap slurpBindTree xs-+          -- * Bounds and Binds+        , collectBound+        , collectBinds +          -- * Support+        , Support       (..)+        , SupportX      (..))+where+import DDC.Core.Collect.Free+import DDC.Core.Collect.Support+import DDC.Type.Collect

@@ -0,0 +1,128 @@+-- | Collecting sets of variables and constructors.+module DDC.Core.Collect.Free+        (freeX)+where+import DDC.Type.Collect+import DDC.Type.Compounds+import DDC.Core.Module+import DDC.Core.Exp+import DDC.Type.Env                     (Env)+import qualified DDC.Type.Env           as Env+import qualified Data.Set               as Set+import Data.Set                         (Set)+++-- freeX ----------------------------------------------------------------------+-- | Collect the free Data and Witness variables in a thing (level-0).+freeX   :: (BindStruct c, Ord n) +        => Env n -> c n -> Set (Bound n)+freeX tenv xx = Set.unions $ map (freeOfTreeX tenv) $ slurpBindTree xx++freeOfTreeX :: Ord n => Env n -> BindTree n -> Set (Bound n)+freeOfTreeX tenv tt+ = {-# SCC freeOfTreeX #-}+   case tt of+        BindDef way bs ts+         |  isBoundExpWit $ boundLevelOfBindWay way+         ,  tenv'        <- Env.extends bs tenv+         -> Set.unions $ map (freeOfTreeX tenv') ts++        BindDef _ _ ts+         -> Set.unions $ map (freeOfTreeX  tenv) ts++        BindUse bl u+         | isBoundExpWit bl+         , Env.member u tenv -> Set.empty+         | isBoundExpWit bl  -> Set.singleton u+        _                    -> Set.empty+++-- Module ---------------------------------------------------------------------+instance BindStruct (Module a) where+ slurpBindTree mm+        = slurpBindTree $ moduleBody mm+++-- Exp ------------------------------------------------------------------------+instance BindStruct (Exp a) where+ slurpBindTree xx+  = case xx of+        XVar _ u+         -> [BindUse BoundExp u]++        XCon _ dc+         -> case daConName dc of+                DaConUnit               -> []+                DaConNamed n            -> [BindCon BoundExp (UName n) Nothing]++        XApp _ x1 x2            -> slurpBindTree x1 ++ slurpBindTree x2+        XLAM _ b x              -> [bindDefT BindLAM [b] [x]]+        XLam _ b x              -> [bindDefX BindLam [b] [x]]      ++        XLet _ (LLet m b x1) x2+         -> slurpBindTree m+         ++ slurpBindTree x1+         ++ [bindDefX BindLet [b] [x2]]++        XLet _ (LRec bxs) x2+         -> [bindDefX BindLetRec +                     (map fst bxs) +                     (map snd bxs ++ [x2])]+        +        XLet _ (LLetRegions b bs) x2+         -> [ BindDef  BindLetRegions b+             [bindDefX BindLetRegionWith bs [x2]]]++        XLet _ (LWithRegion u) x2+         -> BindUse BoundExp u : slurpBindTree x2++        XCase _ x alts  -> slurpBindTree x ++ concatMap slurpBindTree alts+        XCast _ c x     -> slurpBindTree c ++ slurpBindTree x+        XType t         -> slurpBindTree t+        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+        CastWeakenEffect  eff   -> slurpBindTree eff+        CastWeakenClosure xs    -> concatMap slurpBindTree xs+        CastPurify w            -> slurpBindTree w+        CastForget w            -> slurpBindTree w+++instance BindStruct (Alt a) where+ slurpBindTree alt+  = case alt of+        AAlt PDefault x+         -> slurpBindTree x++        AAlt (PData _ bs) x+         -> [bindDefX BindCasePat bs [x]]+++instance BindStruct Witness where+ slurpBindTree ww+  = case ww of+        WVar u          -> [BindUse BoundWit u]+        WCon{}          -> []+        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.+bindDefX :: BindStruct c +         => BindWay -> [Bind n] -> [c n] -> BindTree n+bindDefX way bs xs+        = BindDef way bs+        $   concatMap (slurpBindTree . typeOfBind) bs+        ++  concatMap slurpBindTree xs

@@ -0,0 +1,208 @@++module DDC.Core.Collect.Support+        ( Support       (..)+        , SupportX      (..))+where+import DDC.Core.Compounds+import DDC.Core.Exp+import DDC.Type.Collect.FreeT+import Data.Set                 (Set)+import DDC.Type.Env             (KindEnv, TypeEnv)+import qualified DDC.Type.Env   as Env+import qualified Data.Set       as Set+import Data.Monoid+++data Support n+        = Support+        { -- | Type constructors used in the expression.+          supportTyCon          :: Set (Bound n)++          -- | Type constructors used in the argument of a value-type application.+        , supportTyConXArg      :: Set (Bound n)++          -- | Free spec variables in an expression.+        , supportSpVar          :: Set (Bound n)++          -- | Type constructors used in the argument of a value-type application.+        , supportSpVarXArg      :: Set (Bound n)++          -- | Free witness variables in an expression.+          --   (from the Witness universe)+        , supportWiVar          :: Set (Bound n)++          -- | Free value variables in an expression.+          --   (from the Data universe)+        , supportDaVar          :: Set (Bound n) }+        deriving Show+++instance Ord n => Monoid (Support n) where+ mempty = Support+        { supportTyCon          = Set.empty+        , supportTyConXArg      = Set.empty+        , supportSpVar          = Set.empty+        , supportSpVarXArg      = Set.empty+        , supportWiVar          = Set.empty+        , supportDaVar          = Set.empty }++ mappend sp1 sp2+        = Support+        { supportTyCon          = Set.unions [supportTyCon sp1,     supportTyCon sp2]+        , supportTyConXArg      = Set.unions [supportTyConXArg sp1, supportTyConXArg sp2]+        , supportSpVar          = Set.unions [supportSpVar sp1,     supportSpVar sp2]+        , supportSpVarXArg      = Set.unions [supportSpVarXArg sp1, supportSpVarXArg sp2]+        , supportWiVar          = Set.unions [supportWiVar sp1,     supportWiVar sp2]+        , supportDaVar          = Set.unions [supportDaVar sp1,     supportDaVar sp2] }+++class SupportX (c :: * -> *) where+ support+        :: Ord n+        => KindEnv n -> TypeEnv n+        -> c n+        -> Support n+++instance SupportX Type where+ support kenv _tenv t+  = let (fvs1, tcs)     = freeVarConT kenv t+    in  mempty  { supportTyCon  = tcs+                , supportSpVar  = fvs1 }+++instance SupportX Bind where+ support kenv tenv b+  = support kenv tenv +  $ typeOfBind b+++instance SupportX (Exp a) where+ support kenv tenv xx+  = case xx of+        XVar _ u        +         | Env.member u tenv    -> mempty+         | otherwise            -> mempty { supportDaVar = Set.singleton u}++        XCon{}                  +         -> mempty++        XLAM _ b x+         -> support kenv tenv b +         <> support (Env.extend b kenv) tenv x++        XLam _ b x+         -> support kenv tenv b+         <> support kenv (Env.extend b tenv) x++        XApp _ x1 x2+         -> let s1              = support kenv tenv x1 +                s2              = support kenv tenv x2+            in  mappend s1 s2++        XLet _a lts x2+         -> let s1              = support kenv tenv lts+                (bs1, bs0)      = bindsOfLets lts+                kenv'           = Env.extends bs1 kenv+                tenv'           = Env.extends bs0 tenv+                s2              = support kenv' tenv' x2+            in  mappend s1 s2++        XCase _ x1 alts+         -> let s1              = support kenv tenv x1+                ss              = mconcat $ map (support kenv tenv) alts+            in  mappend s1 ss++        XCast _ c1 x2+         -> let s1              = support kenv tenv c1+                s2              = support kenv tenv x2+            in  mappend s1 s2++        XType t +         -> let sup = support kenv tenv t+            in  sup { supportTyConXArg  = supportTyCon sup+                    , supportSpVarXArg  = supportSpVar sup }++        XWitness w      -> support kenv tenv w+++instance SupportX (Alt a) where+ support kenv tenv aa+  = case aa of+        AAlt PDefault x+         -> support kenv tenv x++        AAlt (PData _dc bs0) x+         -> let tenv'   = Env.extends bs0 tenv+            in  support kenv tenv' x+++instance SupportX Witness where+ support kenv tenv ww+  = case ww of+        WVar u+         | Env.member u tenv    -> mempty+         | otherwise            -> mempty { supportWiVar = Set.singleton u }++        WCon{}+         -> mempty++        WApp w1 w2+         -> support kenv tenv w1+         <> support kenv tenv w2++        WJoin w1 w2+         -> support kenv tenv w1+         <> support kenv tenv w2++        WType t+         -> support kenv tenv t+++instance SupportX (Cast a) where+ support kenv tenv cc+  = case cc of+        CastWeakenEffect eff+         -> support kenv tenv eff++        CastWeakenClosure xs+         -> mconcat $ map (support kenv tenv) xs++        CastPurify w+         -> support kenv tenv w++        CastForget w+         -> support kenv tenv w+         ++instance SupportX (Lets a) where+ support kenv tenv lts+  = case lts of+        LLet m b x+         -> support kenv tenv m+         <> support kenv tenv b+         <> support kenv (Env.extend b tenv) x++        LRec bxs+         -> (mconcat $ map (support kenv tenv) $ map fst bxs)+         <> (let tenv' = Env.extends (map fst bxs) tenv+             in  mconcat $ map (support kenv tenv') $ map snd bxs)++        LLetRegions bs ws+         -> (mconcat $ map (support kenv tenv) bs)+         <> (let kenv' = Env.extends bs kenv+             in  mconcat $ map (support kenv' tenv) ws)++        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,79 +1,93 @@  -- | Utilities for constructing and destructing compound expressions. module DDC.Core.Compounds -        ( -- * Lets-          bindsOfLets-        , specBindsOfLets-        , valwitBindsOfLets+        ( module DDC.Type.Compounds+        , module DDC.Core.DaCon -          -- * Patterns-        , bindsOfPat+          -- * Annotations+        , takeAnnotOfExp            -- * Lambdas-        , makeXLAMs, takeXLAMs-        , makeXLams, takeXLams-        , takeXLamFlags+        , xLAMs+        , xLams         , makeXLamFlags+        , takeXLAMs+        , takeXLams+        , takeXLamFlags            -- * Applications-        , makeXApps+        , xApps+        , makeXAppsWithAnnots         , takeXApps+        , takeXApps1+        , takeXAppsAsList+        , takeXAppsWithAnnots         , takeXConApps         , takeXPrimApps -          -- * Alternatives-        , takeCtorNameOfAlt)-where-import DDC.Type.Compounds-import DDC.Core.Exp-+          -- * Lets+        , xLets+        , splitXLets +        , bindsOfLets+        , specBindsOfLets+        , valwitBindsOfLets --- | Take the binds of a `Lets`.-bindsOfLets :: Lets a n -> [Bind n]-bindsOfLets ll- = case ll of-        LLet _ b _        -> [b]-        LRec bxs          -> map fst bxs-        LLetRegion   b bs -> b : bs-        LWithRegion{}     -> []+          -- * Patterns+        , bindsOfPat +          -- * Alternatives+        , takeCtorNameOfAlt --- | Like `bindsOfLets` but only take the type binders.-specBindsOfLets :: Lets a n -> [Bind n]-specBindsOfLets ll- = case ll of-        LLet _ _ _       -> []-        LRec _           -> []-        LLetRegion b _   -> [b]-        LWithRegion{}    -> []+          -- * Witnesses+        , wApp+        , wApps+        , takeXWitness+        , takeWAppsAsList+        , takePrimWiConApps +          -- * Types+        , takeXType --- | Like `bindsOfLets` but only take the value and witness binders.-valwitBindsOfLets :: Lets a n -> [Bind n]-valwitBindsOfLets ll- = case ll of-        LLet _ b _       -> [b]-        LRec bxs         -> map fst bxs-        LLetRegion _ bs  -> bs-        LWithRegion{}    -> []+          -- * Units+        , xUnit)+where+import DDC.Type.Compounds+import DDC.Core.Exp+import DDC.Core.DaCon  --- | Take the binds of a `Pat`.-bindsOfPat :: Pat n -> [Bind n]-bindsOfPat pp- = case pp of-        PDefault          -> []-        PData _ bs        -> bs+-- 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 lambda abstractions.-makeXLAMs :: a -> [Bind n] -> Exp a n -> Exp a n-makeXLAMs a bs x+-- | 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)  --- | Split nested value and witness lambdas from the front of an expression,+-- | 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@@ -84,12 +98,6 @@          (bs, body)     -> Just (bs, body)  --- | Make some nested value or witness lambda abstractions.-makeXLams :: a -> [Bind n] -> Exp a n -> Exp a n-makeXLams a bs x-        = foldr (XLam a) x (reverse bs)-- -- | 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)@@ -101,6 +109,17 @@          (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.@@ -114,59 +133,200 @@          (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+-- 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  --- Applications ------------------------------------------------------------------ | Build sequence of type applications.-makeXApps   :: a -> Exp a n -> [Exp a n] -> Exp a n-makeXApps 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 parts and arguments, if any.-takeXApps   :: Exp a n -> [Exp a n]+-- | 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    -> takeXApps x1 ++ [x2]+        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 takeXApps xx of-        XVar _ (UPrim p _) : xs  -> Just (p, xs)-        _                        -> Nothing+ = 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 (Bound n, [Exp a n])+takeXConApps :: Exp a n -> Maybe (DaCon n, [Exp a n]) takeXConApps xx- = case takeXApps xx of-        XCon _ u : xs   -> Just (u, xs)+ = 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 u _) _      -> takeNameOfBound u+        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 

@@ -0,0 +1,100 @@++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,135 +0,0 @@---- | Algebraic data type definitions.-module DDC.Core.DataDef-        ( DataDef    (..)--        -- * Data type definition table-        , DataDefs   (..)-        , DataMode   (..)-        , DataType   (..)-        , DataCtor   (..)--        , emptyDataDefs-        , insertDataDef-        , fromListDataDefs-        , lookupModeOfDataType)-where-import DDC.Type.Exp-import Data.Map                 (Map)-import qualified Data.Map       as Map-import Data.Maybe-import Control.Monad----- | The definition of a single data type.-data DataDef n-        = DataDef-        { -- | Name of the data type.-          dataDefTypeName       :: n--          -- | Kinds of type parameters.-        , dataDefParamKinds     :: [Kind n]--          -- | Constructors of the data type, or Nothing if there are-          --   too many to list (like with `Int`).-        , dataDefCtors          :: Maybe [(n, [Type n])] }------ DataDefs ---------------------------------------------------------------------- | A table of data type definitions,---   unpacked into type and data constructors so we can find them easily.-data DataDefs n-        = DataDefs-        { dataDefsTypes :: Map n (DataType n)-        , dataDefsCtors :: Map n (DataCtor n) }----- | The mode of a data type records how many data constructors there are.---   This can be set to 'Large' for large primitive types like Int and Float.---   In this case we don't ever expect them all to be enumerated---   as case alternatives.-data DataMode n-        = DataModeSmall [n]-        | DataModeLarge----- | Describes a data type constructor, used in the `DataDefs` table.-data DataType n-        = DataType -        { -- | Name of data type constructor.-          dataTypeName       :: n--          -- | Kinds of type parameters to constructor.-        , dataTypeParamKinds :: [Kind n]--          -- | Names of data constructors of this data type,-          --   or `Nothing` if it has infinitely many constructors.-        , dataTypeMode       :: DataMode n }----- | Describes a data constructor, used in the `DataDefs` table.-data DataCtor n-        = DataCtor-        { -- | Name of data constructor.-          dataCtorName       :: n--          -- | Field types of constructor.-        , dataCtorFieldTypes :: [Type n]--          -- | Name of result type of constructor.-        , dataCtorTypeName   :: n }------ | An empty table of data type definitions.-emptyDataDefs :: DataDefs n-emptyDataDefs-        = DataDefs-        { dataDefsTypes = Map.empty-        , dataDefsCtors = Map.empty }----- | Insert a data type definition into some DataDefs.-insertDataDef  :: Ord n => DataDef  n -> DataDefs n -> DataDefs n-insertDataDef (DataDef nType ks mCtors) dataDefs- = let  defType = DataType-                { dataTypeName       = nType-                , dataTypeParamKinds = ks-                , dataTypeMode       = defMode }--        defMode = case mCtors of-                   Nothing    -> DataModeLarge-                   Just ctors -> DataModeSmall (map fst ctors)--        makeDefCtor (nCtor, tsFields)-                = DataCtor-                { dataCtorName       = nCtor-                , dataCtorFieldTypes = tsFields-                , dataCtorTypeName   = nType }--        defCtors = case mCtors of-                    Nothing  -> Nothing-                    Just cs  -> Just $ map makeDefCtor cs--   in   dataDefs-         { dataDefsTypes = Map.insert nType defType (dataDefsTypes dataDefs)-         , dataDefsCtors = Map.union (dataDefsCtors dataDefs)-                         $ Map.fromList [(n, def) | def@(DataCtor n _ _) -                                          <- concat $ maybeToList defCtors] }----- | Build a `DataDefs` table from a list of `DataDef`-fromListDataDefs :: Ord n => [DataDef n] -> DataDefs n-fromListDataDefs defs-        = foldr insertDataDef emptyDataDefs defs------ | Yield the list of data constructor names for some data type, ---   or `Nothing` for large types with too many constructors to list.-lookupModeOfDataType :: Ord n => n -> DataDefs n -> Maybe (DataMode n)-lookupModeOfDataType n defs-        = liftM dataTypeMode $ Map.lookup n (dataDefsTypes defs)--

@@ -5,6 +5,8 @@            -- * Computation expressions         , Exp     (..)+        , DaCon   (..)+        , DaConName(..)         , Cast    (..)         , Lets    (..)         , LetMode (..)@@ -16,183 +18,8 @@         , WiCon   (..)         , WbCon   (..)) where+import DDC.Core.Exp.Base+import DDC.Core.Exp.NFData      ()+import DDC.Core.DaCon import DDC.Type.Exp-import DDC.Type.Sum             ()----- Values ------------------------------------------------------------------------ | Well-typed expressions live in the Data universe, and their types always---   have kind '*'. --- ---   Expressions do something useful at runtime, and might diverge or cause---   side effects.-data Exp a n-        -- | Value variable   or primitive operation.-        = XVar  a  (Bound n)--        -- | Data constructor or literal.-        | XCon  a  (Bound 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 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)----- | Type casts.-data Cast n-        -- | Weaken the effect of an expression.-        = CastWeakenEffect  (Effect n)-        -        -- | Weaken the closure of an expression.-        | CastWeakenClosure (Closure n)--        -- | Purify the effect of an expression.-        | CastPurify (Witness n)--        -- | Hide sharing of the closure 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.-        | LLetRegion  (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 (Bound 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.-        | WiConBound (Bound 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,186 @@++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,82 @@++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,65 @@++-- | The ambient Disciple Core language is specialised to concrete languages+--   by adding primitive operations and optionally restricting the set of +--   available language features. This specialisation results in user-facing+--   language fragments such as @Disciple Core Lite@ and @Disciple Core Salt@.+module DDC.Core.Fragment+        ( -- * Langauge fragments+          Fragment      (..)+        , Profile       (..)+        , zeroProfile++          -- * Fragment features+        , Feature       (..)+        , Features      (..)+        , zeroFeatures++        -- * Compliance+        , complies+        , compliesWithEnvs+        , Complies+        , Error         (..))+where+import DDC.Core.Fragment.Feature+import DDC.Core.Fragment.Compliance+import DDC.Core.Fragment.Error+import DDC.Core.Fragment.Profile+import DDC.Core.Module+import DDC.Core.Exp+import DDC.Core.Lexer+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 :: * -> *)+        = Fragment+        { -- | Language profile for this fragment.+          fragmentProfile       :: Profile n++          -- | File extension to use when dumping modules in this fragment.+        , fragmentExtension     :: String++          -- | Read a name.+        , fragmentReadName      :: String -> Maybe n+        +          -- | Lex module source into tokens,+          --   given the source name and starting line number. +        , fragmentLexModule     :: String -> Int -> String -> [Token (Tok n)]++          -- | Lex expression source into tokens,+          --   given the source name and starting line number.+        , fragmentLexExp        :: String -> Int -> String -> [Token (Tok n)]++          -- | Perform language fragment specific checks on a module.+        , fragmentCheckModule   :: forall a. Module a n -> Maybe (err a)++          -- | Perform language fragment specific checks on an expression.+        , fragmentCheckExp      :: forall a. Exp a n    -> Maybe (err a) }+++instance Show (Fragment n err) where+ show frag+  = profileName $ fragmentProfile frag+

@@ -0,0 +1,388 @@++module DDC.Core.Fragment.Compliance+        ( complies+	, compliesWithEnvs+        , Complies)+where+import DDC.Core.Fragment.Feature+import DDC.Core.Fragment.Profile+import DDC.Core.Fragment.Error+import DDC.Core.Compounds+import DDC.Core.Predicates+import DDC.Core.Module+import DDC.Core.Exp+import Control.Monad+import Data.Maybe+import DDC.Type.Env                     (Env)+import Data.Set                         (Set)+import qualified DDC.Type.Env           as Env+import qualified Data.Set               as Set+import qualified Data.Map.Strict        as Map+++-- | Check whether a core thing complies with a language fragment profile.+complies +        :: (Ord n, Show n, Complies c)+        => Profile n            -- ^ Fragment profile giving the supported+                                --   language features and primitive operators.+        -> c a n                -- ^ The thing to check.+        -> Maybe (Error n)++complies profile thing+ = compliesWithEnvs profile+        (profilePrimKinds profile)+        (profilePrimTypes profile)+        thing+++-- | Like `complies` but with some starting environments.+compliesWithEnvs+        :: (Ord n, Show n, Complies c)+        => Profile n            -- ^ Fragment profile giving the supported+                                --   language features and primitive operators.+	-> Env.KindEnv n        -- ^ Starting kind environment.+	-> Env.TypeEnv n        -- ^ Starting type environment.+	-> c a n                -- ^ The thing to check.+	-> Maybe (Error n)++compliesWithEnvs profile kenv tenv thing+ = let  merr    = result +                $ compliesX profile +                        kenv tenv+                        contextTop thing+   in   case merr of+         Left err -> Just err+         Right _  -> Nothing++++-- Complies -------------------------------------------------------------------+-- | Class of things we can check language fragment compliance for.+class Complies (c :: * -> * -> *) where+ -- Check compliance of a well typed term with a language profile.+ -- If it is not well typed then this can return a bad result.+ compliesX+        :: (Ord n, Show n)+        => Profile n            -- ^ Fragment profile giving the supported+                                --   language features and primitive operators.+        -> Env n                -- ^ Starting Kind environment.+        -> Env n                -- ^ Starting Type environment.+        -> Context+        -> c a n +        -> CheckM n+                (Set n, Set n)  -- Used type and value names.+++instance Complies Module where+ compliesX profile kenv tenv context mm+  = do  let bs          = [ BName n t +                                | (n, (_, t)) <- Map.toList $ moduleImportTypes mm ]+        let tenv'       = Env.extends bs tenv+        compliesX profile kenv tenv' context (moduleBody mm)+++-- We'll mark type vars that only appear in types of binders as unused.+instance Complies Exp where+ compliesX profile kenv tenv context xx+  = let has f   = f $ profileFeatures profile+        ok      = return (Set.empty, Set.empty)+    in case xx of++        -- variables ----------------------------+        XVar _ u@(UName n)+         |  not $ Env.member u tenv+         ,  not $ has featuresUnboundLevel0Vars +         -> throw $ ErrorUndefinedVar n++         |  args        <- fromMaybe 0 $ contextFunArgs context+         ,  Just t      <- Env.lookup u tenv+         ,  arity       <- arityOfType t+         ,  args < arity+         ,  not $ has featuresPartialApplication+         -> throw $ ErrorUnsupported PartialApplication++         | otherwise+         ->     return (Set.empty, Set.singleton n)++        XVar _ u@(UPrim n t)+         |  not $ Env.member u (profilePrimTypes profile)+         -> throw $ ErrorUndefinedPrim n++         |  args        <- fromMaybe 0 $ contextFunArgs context+         ,  arity       <- arityOfType t+         ,  args < arity+         ,  not $ has featuresPartialPrims+         -> throw $ ErrorUnsupported PartialPrims++         | otherwise+         -> return (Set.empty, Set.empty)++        XVar{}          -> ok++        -- constructors -------------------------+        XCon{}          -> ok++        -- spec binders -------------------------+        XLAM _ b x+         | contextAbsBody context+         , not $ has featuresNestedFunctions+         -> throw $ ErrorUnsupported NestedFunctions++         | otherwise+         -> do  +                -- If the body isn't another lambda then remember+                -- that we've entered into a function.+                let context'+                     | isXLAM x || isXLam x = context+                     | otherwise            = setBody context++                (tUsed, vUsed)  <- compliesX profile +                                        (Env.extend b kenv) tenv +                                        context' x++                tUsed'          <- checkBind profile kenv b tUsed+                return (tUsed', vUsed)++        -- value and witness abstraction --------+        XLam _ b x+         | contextAbsBody context+         , not $ has featuresNestedFunctions+         -> throw $ ErrorUnsupported NestedFunctions++         | otherwise+         -> do  +                -- If the body isn't another lambda then remember+                -- that we've entered into a function.+                let context'+                     | isXLAM x || isXLam x = context+                     | otherwise            = setBody context++                (tUsed, vUsed)  <- compliesX profile +                                        kenv (Env.extend b tenv)+                                        context' x++                vUsed'          <- checkBind profile tenv b vUsed+                return (tUsed, vUsed')+       +        -- application --------------------------+        XApp _ x1 (XType t2)+         | profileTypeIsUnboxed profile t2+         , Nothing      <- takeXPrimApps xx+         -> throw $ ErrorUnsupported UnboxedInstantiation++         | otherwise+         -> do  checkFunction profile x1+                compliesX     profile kenv tenv (addArg context) x1++        XApp _ x1 XWitness{}+         -> do  checkFunction profile x1+                compliesX     profile kenv tenv (addArg context) x1++        XApp _ x1 x2+         -> do  checkFunction profile x1+                (tUsed1, vUsed1) <- compliesX profile kenv tenv (addArg context) x1+                (tUsed2, vUsed2) <- compliesX profile kenv tenv context x2+                return  ( Set.union tUsed1 tUsed2+                        , Set.union vUsed1 vUsed2)++        -- let ----------------------------------+        XLet _ (LLet mode 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')++        XLet _ (LRec bxs) x2+         -> do  let (bs, xs)    = unzip bxs+                let tenv'       = Env.extends bs tenv++                (tUseds1, vUseds1) +                 <- liftM unzip+                 $  mapM (compliesX profile kenv tenv' (reset context)) +                         xs++                (tUsed2,  vUsed2) <- compliesX profile kenv tenv' (reset context) x2+                let tUseds        = Set.unions (tUsed2 : tUseds1)+                let vUseds        = Set.unions (vUsed2 : vUseds1)++                vUseds'           <- checkBinds profile tenv bs vUseds+                return (tUseds, vUseds')+++        XLet _ (LLetRegions rs bs) x2+         -> do  (tUsed2, vUsed2) +                 <- compliesX profile   (Env.extends rs  kenv) +                                        (Env.extends bs tenv) +                                        (reset context) x2+                return (tUsed2, vUsed2)++        XLet _ (LWithRegion _) x2+         -> do  (tUsed2, vUsed2) <- compliesX profile kenv tenv +                                        (reset context) x2+                return (tUsed2, vUsed2)++        -- case ---------------------------------+        XCase _ x1 alts+         -> do  (tUsed1,  vUsed1)  +                 <- compliesX profile kenv tenv (reset context) x1++                (tUseds2, vUseds2) <- liftM unzip +                                   $  mapM (compliesX profile kenv tenv (reset context)) alts++                return  ( Set.unions $ tUsed1 : tUseds2+                        , Set.unions $ vUsed1 : vUseds2)+++        -- cast ---------------------------------+        XCast _ _ x     -> compliesX profile kenv tenv (reset context) x++        -- type and witness ---------------------+        XType t         -> throw $ ErrorNakedType    t+        XWitness w      -> throw $ ErrorNakedWitness w+++instance Complies Alt where+ compliesX profile kenv tenv context aa+  = case aa of+        AAlt PDefault x+         -> do  (tUsed1, vUsed1)  <- compliesX profile kenv tenv +                                        (reset context) x+                return  (tUsed1, vUsed1)++        AAlt (PData _ bs) x+         -> do  (tUsed1, vUsed1) <- compliesX profile kenv (Env.extends bs tenv) +                                        (reset context) x+                vUsed1'          <- checkBinds profile tenv bs vUsed1 +                return (tUsed1, vUsed1')+++-- Bind -----------------------------------------------------------------------+-- | Check for compliance violations at a binding site.+checkBind +        :: Ord n +        => Profile n            -- ^ The current language profile.+        -> 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.++checkBind profile env bb used+ = let has f   = f $ profileFeatures profile+   in case bb of+        BName n _+         | not $ Set.member n used+         , not $ has featuresUnusedBindings +         -> throw $ ErrorUnusedBind n++         | Env.memberBind bb env+         , not $ has featuresNameShadowing +         -> throw $ ErrorShadowedBind n++         | otherwise+         -> return $ Set.delete n used++        BAnon{}+         | not $ has featuresDebruijnBinders+         -> throw $ ErrorUnsupported DebruijnBinders++        _ -> return used+++-- | Check for compliance violations at a binding site.+--   The binders must all be at the same level.+checkBinds +        :: Ord n  +        => Profile n +        -> Env n  -> [Bind n] -> Set n +        -> CheckM n (Set n)++checkBinds profile env bs used+ = case bs of+        []              -> return used+        (b : bs')        +         -> do  used'   <- checkBinds profile env bs' used+                checkBind profile env b used'+++-- Function -------------------------------------------------------------------+-- | Check the function part of an application.+checkFunction :: Profile n -> Exp a n -> CheckM n ()+checkFunction profile xx + = let  has f   = f $ profileFeatures profile+        ok       = return ()+   in case xx of+        XVar{}  -> ok+        XCon{}  -> ok+        XApp{}  -> ok+        XCast{} -> ok+        _+         | has featuresGeneralApplication -> return ()+         | otherwise    -> throw $ ErrorUnsupported GeneralApplication+++-- Context --------------------------------------------------------------------+data Context+        = Context+        { contextAbsBody        :: Bool +        , contextFunArgs        :: Maybe Int }+        deriving (Eq, Show)+++-- | The top level context, used at the top-level scope of a module.+contextTop :: Context+contextTop+        = Context+        { contextAbsBody        = False+        , contextFunArgs        = Nothing }+++-- | Record that we've entered into an abstraction body.+setBody :: Context -> Context+setBody context = context { contextAbsBody = True }+++-- | Record that the expression is being directly applied to an argument.+addArg  :: Context -> Context+addArg context+ = case contextFunArgs context of+        Nothing         -> context { contextFunArgs = Just 1 }+        Just args       -> context { contextFunArgs = Just (args + 1) }+++-- | Reset the argument counter of a context.+reset   :: Context -> Context+reset context   = context { contextFunArgs = Nothing } +++-- Monad ----------------------------------------------------------------------+-- | Compliance checking monad.+data CheckM n x+        = CheckM (Either (Error n) x)++instance Monad (CheckM n) where+ return x   = CheckM (Right x)+ (>>=) m f  +  = case m of+          CheckM (Left err)     -> CheckM (Left err)+          CheckM (Right x)      -> f x+++-- | Throw an error in the monad.+throw :: Error n -> CheckM n x+throw e       = CheckM $ Left e+++-- | Take the result from a check monad.+result :: CheckM n x -> Either (Error n) x+result (CheckM r)       = r

@@ -0,0 +1,59 @@++module DDC.Core.Fragment.Error+        (Error(..))+where+import DDC.Core.Fragment.Feature+import DDC.Core.Exp+import DDC.Core.Pretty+++-- | Language fragment compliance violations.+data Error n+        -- | Found an unsupported language feature.+        = ErrorUnsupported      !Feature++        -- | Found an undefined primitive operator.+        | ErrorUndefinedPrim    !n ++        -- | Found an unbound variable.+        | ErrorUndefinedVar     !n++        -- | Found a variable binder that shadows another one at a higher scope,+        --   but the profile doesn't permit this.+        | ErrorShadowedBind     !n++        -- | Found a bound variable with no uses,+        --   but the profile doesn't permit this.+        | ErrorUnusedBind       !n++        -- | Found a naked type that isn't used as a function argument.+        | ErrorNakedType        !(Type    n)++        -- | Found a naked witness that isn't used as a function argument.+        | ErrorNakedWitness     !(Witness n)+        deriving (Eq, Show)+++instance (Pretty n, Eq n) => Pretty (Error n) where+ ppr err+  = case err of+        ErrorUnsupported feature+         -> vcat [ text "Unsupported feature: " <> text (show feature) ]++        ErrorUndefinedPrim n+         -> vcat [ text "Undefined primitive: " <> ppr n ]++        ErrorUndefinedVar n+         -> vcat [ text "Undefined variable: " <> ppr n ]++        ErrorShadowedBind n+         -> vcat [ text "Binding shadows existing name: " <> ppr n ]++        ErrorUnusedBind n+         -> vcat [ text "Bound name is not used: " <> ppr n ]++        ErrorNakedType t+         -> vcat [ text "Naked type is not a function argument: " <> ppr t]++        ErrorNakedWitness w+         -> vcat [ text "Naked witness is not a function argument: " <> ppr w ]

@@ -0,0 +1,63 @@++module DDC.Core.Fragment.Feature+        (Feature(..))+where+++-- | 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++        -- | Assume all functions share data invisibly,+        --   and don't generate closure terms in types.+        | UntrackedClosures++        -- General features -------------------------------+        -- | Partially applied primitive operators.+        | PartialPrims++        -- | Partially applied functions+        | PartialApplication++        -- | Function application where the thing being applied+        --   is not a variable.+        --   Most backend languages (like LLVM) don't support this.+        | GeneralApplication++        -- | 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+        --   binders.+        | DebruijnBinders++        -- | Allow data and witness vars without binding occurrences if+        --   they are annotated directly with their types. This lets+        --   us work with open terms.+        | UnboundLevel0Vars++        -- | Allow non-primitive functions to be instantiated at unboxed types.+        --   Our existing backends can't handle this, because boxed and unboxed+        --   objects have different representations.+        | UnboxedInstantiation++        -- Sanity -----------------------------------------+        -- | Allow name shadowing.+        | NameShadowing++        -- | Allow unused named data and witness bindings.+        | UnusedBindings++        -- | Allow unused named matches.+        | UnusedMatches+        deriving (Eq, Ord, Show)

@@ -0,0 +1,111 @@++-- | A fragment profile determines what features a program can use.+module DDC.Core.Fragment.Profile+        ( Profile (..)+        , zeroProfile++        , Features(..)+        , zeroFeatures+        , setFeature)+where+import DDC.Core.Fragment.Feature+import DDC.Type.DataDef+import DDC.Type.Exp+import DDC.Type.Env                     (KindEnv, TypeEnv)+import qualified DDC.Type.Env           as Env+++-- | The fragment profile describes the language features and +--   primitive operators available in the language.+data Profile n+        = Profile+        { -- | The name of this profile.+          profileName                   :: !String++          -- | Permitted language features.+        , profileFeatures               :: !Features++          -- | Primitive data type declarations.+        , profilePrimDataDefs           :: !(DataDefs n)++          -- | Kinds of primitive types.+        , profilePrimKinds              :: !(KindEnv n)++          -- | Types of primitive operators.+        , profilePrimTypes              :: !(TypeEnv n)++          -- | Check whether a type is an unboxed type.+          --   Some fragments limit how these can be used.+        , profileTypeIsUnboxed          :: !(Type n -> Bool) }+++-- | A language profile with no features or primitive operators.+--+--   This provides a simple first-order language.+zeroProfile :: Profile n+zeroProfile+        = Profile+        { profileName                   = "Zero"+        , profileFeatures               = zeroFeatures+        , profilePrimDataDefs           = emptyDataDefs+        , profilePrimKinds              = Env.empty+        , profilePrimTypes              = Env.empty+        , profileTypeIsUnboxed          = const False }+++-- | A flattened set of features, for easy lookup.+data Features +        = Features+        { featuresUntrackedEffects      :: Bool+        , featuresUntrackedClosures     :: Bool+        , featuresPartialPrims          :: Bool+        , featuresPartialApplication    :: Bool+        , featuresGeneralApplication    :: Bool+        , featuresNestedFunctions       :: Bool+        , featuresLazyBindings          :: Bool+        , featuresDebruijnBinders       :: Bool+        , featuresUnboundLevel0Vars     :: Bool+        , featuresUnboxedInstantiation  :: Bool+        , featuresNameShadowing         :: Bool+        , featuresUnusedBindings        :: Bool+        , featuresUnusedMatches         :: Bool+        }+++-- | An emtpy feature set, with all flags set to `False`.+zeroFeatures :: Features+zeroFeatures+        = Features+        { featuresUntrackedEffects      = False+        , featuresUntrackedClosures     = False+        , featuresPartialPrims          = False+        , featuresPartialApplication    = False+        , featuresGeneralApplication    = False+        , featuresNestedFunctions       = False+        , featuresLazyBindings          = False+        , featuresDebruijnBinders       = False+        , featuresUnboundLevel0Vars     = False+        , featuresUnboxedInstantiation  = False+        , featuresNameShadowing         = False+        , featuresUnusedBindings        = False+        , featuresUnusedMatches         = False }+++-- | Set a language `Flag` in the `Profile`.+setFeature :: Feature -> Bool -> Features -> Features+setFeature feature val features+ = case feature of+        UntrackedEffects        -> features { featuresUntrackedEffects     = val }+        UntrackedClosures       -> features { featuresUntrackedClosures    = 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 }+        NameShadowing           -> features { featuresNameShadowing        = val }+        UnusedBindings          -> features { featuresUnusedBindings       = val }+        UnusedMatches           -> features { featuresUnusedMatches        = val }+

@@ -0,0 +1,215 @@++-- | Reference lexer for core langauge parser. Slow but Simple.+--+--   The lexers here all use 'String' in place of a real name type.+--   After applying these functions to the program text, we need+--   to use `renameTok` tok convert the strings in `TokNamed` tokens+--   into the name type specific to the langauge fragment to be parsed.+--+module DDC.Core.Lexer+        ( module DDC.Core.Lexer.Tokens+        , module DDC.Core.Lexer.Names++          -- * Lexer+        , lexModuleWithOffside+        , lexExp)+where+import DDC.Core.Lexer.Offside+import DDC.Core.Lexer.Comments+import DDC.Core.Lexer.Names+import DDC.Core.Lexer.Tokens+import DDC.Data.SourcePos+import DDC.Data.Token+import Data.Char+++-- Module ---------------------------------------------------------------------+-- | Lex a module and apply the offside rule.+--+--   Automatically drop comments from the token stream along the way.+--+lexModuleWithOffside +        :: FilePath     -- ^ Path to source file, for error messages.+        -> Int          -- ^ Starting line number.+        -> String       -- ^ String containing program text.+        -> [Token (Tok String)]++lexModuleWithOffside sourceName lineStart str+ = {-# SCC lexWithOffside #-}+        applyOffside [] +        $ addStarts+        $ dropComments +        $ lexString sourceName lineStart str+++-- Exp ------------------------------------------------------------------------+-- | Lex a string into tokens.+--+--   Automatically drop comments from the token stream along the way.+--+lexExp  :: FilePath     -- ^ Path to source file, for error messages.+        -> Int          -- ^ Starting line number.+        -> String       -- ^ String containing program text.+        -> [Token (Tok String)]++lexExp sourceName lineStart str+ = {-# SCC lexExp #-}+        dropNewLines+        $ dropComments+        $ lexString sourceName lineStart str+++-- Generic --------------------------------------------------------------------+lexString :: String -> Int -> String -> [Token (Tok String)]+lexString sourceName lineStart str+        = lexWord lineStart 1 str+ where +  lexWord :: Int -> Int -> String -> [Token (Tok String)]+  lexWord line column w+   = let  tok t = Token t (SourcePos sourceName line column)+          tokM  = tok . KM+          tokA  = tok . KA+          tokN  = tok . KN++          lexMore n rest+           = lexWord line (column + n) rest++     in case w of+        []               -> []        ++        -- Whitespace+        ' '  : w'        -> lexMore 1 w'+        '\t' : w'        -> lexMore 8 w'++        -- Literal values+        -- This needs to come before the rule for '-'+        c : cs+         | isDigit c+         , (body, rest)         <- span isLitBody cs+         -> 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++        -- 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'+++        -- The unit data constructor+        '(' : ')' : w'   -> tokA KDaConUnit      : lexMore 2 w'++        -- Compound Parens+        '['  : ':' : w'  -> tokA KSquareColonBra : lexMore 2 w'+        ':'  : ']' : w'  -> tokA KSquareColonKet : lexMore 2 w'+        '<'  : ':' : w'  -> tokA KAngleColonBra  : lexMore 2 w'+        ':'  : '>' : w'  -> tokA KAngleColonKet  : lexMore 2 w'++        -- Function Constructors+        '~'  : '>'  : w' -> tokA KArrowTilde     : lexMore 2 w'+        '-'  : '>'  : w' -> tokA KArrowDash      : lexMore 2 w'+        '<'  : '-'  : w' -> tokA KArrowDashLeft  : lexMore 2 w'+        '='  : '>'  : w' -> tokA KArrowEquals    : lexMore 2 w'++        -- Compound symbols+        ':'  : ':'  : w' -> tokA KColonColon     : lexMore 2 w'+        '/'  : '\\' : w' -> tokA KBigLambda      : lexMore 2 w'++        -- Debruijn indices+        '^'  : cs+         |  (ds, rest)   <- span isDigit cs+         ,  length ds >= 1+         -> tokA (KIndex (read ds))              : lexMore (1 + length ds) rest         ++        -- Parens+        '('  : w'       -> tokA KRoundBra        : lexMore 1 w'+        ')'  : w'       -> tokA KRoundKet        : lexMore 1 w'+        '['  : w'       -> tokA KSquareBra       : lexMore 1 w'+        ']'  : w'       -> tokA KSquareKet       : lexMore 1 w'+        '{'  : w'       -> tokA KBraceBra        : lexMore 1 w'+        '}'  : w'       -> tokA KBraceKet        : lexMore 1 w'+        '<'  : w'       -> tokA KAngleBra        : lexMore 1 w'+        '>'  : w'       -> tokA KAngleKet        : lexMore 1 w'            ++        -- Punctuation+        '.'  : w'       -> tokA KDot             : lexMore 1 w'+        '|'  : w'       -> tokA KBar             : lexMore 1 w'+        '^'  : w'       -> tokA KHat             : lexMore 1 w'+        '+'  : w'       -> tokA KPlus            : lexMore 1 w'+        ':'  : w'       -> tokA KColon           : lexMore 1 w'+        ','  : w'       -> tokA KComma           : lexMore 1 w'+        '\\' : w'       -> tokA KBackSlash       : lexMore 1 w'+        ';'  : w'       -> tokA KSemiColon       : lexMore 1 w'+        '_'  : w'       -> tokA KUnderscore      : lexMore 1 w'+        '='  : w'       -> tokA KEquals          : lexMore 1 w'+        '&'  : w'       -> tokA KAmpersand       : lexMore 1 w'+        '-'  : 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'+        ++        -- Named Constructors+        c : cs+         | isConStart c+         , (body,  rest)        <- span isConBody cs+         , (body', rest')       <- case rest of+                                        '#' : rest'     -> (body ++ "#", rest')+                                        _               -> (body, rest)+         -> let readNamedCon s+                 | Just twcon   <- readTwConBuiltin s+                 = tokA (KTwConBuiltin twcon)    : lexMore (length s) rest'+                 +                 | Just tccon   <- readTcConBuiltin s+                 = tokA (KTcConBuiltin tccon)    : lexMore (length s) rest'+                 +                 | Just con     <- readCon s+                 = tokN (KCon con)               : lexMore (length s) rest'+               +                 | otherwise    +                 = [tok (KJunk [c])]+                 +            in  readNamedCon (c : body')++        -- Keywords, Named Variables and Witness constructors+        c : cs+         | isVarStart c+         , (body,  rest)        <- span isVarBody cs+         , (body', rest')       <- case rest of+                                        '#' : rest'     -> (body ++ "#", rest')+                                        _               -> (body, rest)+         -> let readNamedVar s+                 | Just t <- lookup s keywords+                 = tok t                   : lexMore (length s) rest'++                 | Just wc      <- readWbConBuiltin s+                 = tokA (KWbConBuiltin wc) : lexMore (length s) rest'+         +                 | Just v       <- readVar s+                 = tokN (KVar v)           : lexMore (length s) rest'++                 | otherwise+                 = [tok (KJunk [c])]++            in  readNamedVar (c : body')++        -- Some unrecognised character.+        -- We still need to keep lexing as this may be in a comment.+        c : cs   -> (tok $ KJunk [c]) : lexMore 1 cs+

@@ -0,0 +1,64 @@++module DDC.Core.Lexer.Comments+        ( dropComments+        , dropNewLines)+where+import DDC.Core.Lexer.Tokens+import DDC.Data.Token+import DDC.Data.SourcePos+++-- | Drop all the comments and newline tokens in this stream.+dropComments +        :: Eq n => [Token (Tok n)] -> [Token (Tok n)]++dropComments []      = []+dropComments (t@(Token tok sourcePos) : xs)+ = case tok of+        KM KCommentLineStart +         -> dropComments $ dropWhile (\t' -> not $ isToken t' (KM KNewLine)) xs++        KM KCommentBlockStart +         -> dropComments $ dropCommentBlock sourcePos xs t++        _ -> t : dropComments xs+++-- | Drop block comments form a token stream.+dropCommentBlock +        :: Eq n+        => SourcePos            -- ^ Position of outer-most block comment start.+        -> [Token (Tok n)] +        -> Token (Tok n) +        -> [Token (Tok n)]++dropCommentBlock spStart [] _terr+        = [Token (KM KCommentUnterminated) spStart]++dropCommentBlock spStart (t@(Token tok _) : xs) terr+ = case tok of+        -- enter into nested block comments.+        KM KCommentBlockStart+         -> dropCommentBlock spStart (dropCommentBlock spStart xs t) terr++        -- outer-most block comment has ended.+        KM KCommentBlockEnd+         -> xs++        _ -> dropCommentBlock spStart xs terr+++-- | Drop newline tokens from this list.+dropNewLines :: Eq n => [Token (Tok n)] -> [Token (Tok n)]+dropNewLines [] = []+dropNewLines (t:ts)+        | isToken t (KM KNewLine)+        = dropNewLines ts++        | otherwise+        = t : dropNewLines ts+++isToken :: Eq n => Token (Tok n) -> Tok n -> Bool+isToken (Token tok _) tok2 = tok == tok2+

@@ -0,0 +1,226 @@++module DDC.Core.Lexer.Names+        ( -- * Keywords+          keywords++          -- * Builtin constructors+        , readTwConBuiltin+        , readTcConBuiltin+        , readWbConBuiltin++          -- * Variable names+        , isVarName+        , isVarStart+        , isVarBody+        , readVar++          -- * Constructor names+        , isConName+        , isConStart+        , isConBody+        , readCon++          -- * Literal names+        , isLitName+        , isLitStart+        , isLitBody)+where+import DDC.Core.Exp+import DDC.Core.Lexer.Tokens+import DDC.Data.ListUtils+import Data.Char+import Data.List+++-- | Textual keywords in the core language.+keywords :: [(String, Tok n)]+keywords+ =      [ ("module",     KA KModule)+        , ("imports",    KA KImports)+        , ("exports",    KA KExports)+        , ("in",         KA KIn)+        , ("of",         KA KOf) +        , ("letrec",     KA KLetRec)+        , ("letregions", KA KLetRegions)+        , ("letregion",  KA KLetRegion)+        , ("withregion", KA KWithRegion)+        , ("let",        KA KLet)+        , ("lazy",       KA KLazy)+        , ("case",       KA KCase)+        , ("purify",     KA KPurify)+        , ("forget",     KA KForget)+        , ("type",       KA KType)+        , ("weakeff",    KA KWeakEff)+        , ("weakclo",    KA KWeakClo)+        , ("with",       KA KWith)+        , ("where",      KA KWhere) +        , ("do",         KA KDo)+        , ("match",      KA KMatch)+        , ("else",       KA KElse) ]+++-- | Read a named `TwCon`. +readTwConBuiltin :: String -> Maybe TwCon+readTwConBuiltin ss+ = case ss of+        "Global"        -> Just TwConGlobal+        "DeepGlobal"    -> Just TwConDeepGlobal+        "Const"         -> Just TwConConst+        "DeepConst"     -> Just TwConDeepConst+        "Mutable"       -> Just TwConMutable+        "DeepMutable"   -> Just TwConDeepMutable+        "Lazy"          -> Just TwConLazy+        "HeadLazy"      -> Just TwConHeadLazy+        "Manifest"      -> Just TwConManifest+        "Pure"          -> Just TwConPure+        "Empty"         -> Just TwConEmpty+        "Disjoint"      -> Just TwConDisjoint+        "Distinct"      -> Just (TwConDistinct 2)+        _               -> readTwConWithArity ss+++readTwConWithArity :: String -> Maybe TwCon+readTwConWithArity ss+ | Just n <- stripPrefix "Distinct" ss + , all isDigit n+ = Just (TwConDistinct $ read n)+ | otherwise = Nothing+ + +-- | Read a builtin `TcCon` with a non-symbolic name, +--   ie not '->'.+readTcConBuiltin :: String -> Maybe TcCon+readTcConBuiltin ss+ = case ss of+        "Unit"          -> Just TcConUnit+        "Read"          -> Just TcConRead+        "HeadRead"      -> Just TcConHeadRead+        "DeepRead"      -> Just TcConDeepRead+        "Write"         -> Just TcConWrite+        "DeepWrite"     -> Just TcConDeepWrite+        "Alloc"         -> Just TcConAlloc+        "DeepAlloc"     -> Just TcConDeepAlloc+        "Use"           -> Just TcConUse+        "DeepUse"       -> Just TcConDeepUse+        _               -> Nothing+++-- | Read a `WbCon`.+readWbConBuiltin :: String -> Maybe WbCon+readWbConBuiltin ss+ = case ss of+        "pure"          -> Just WbConPure+        "empty"         -> Just WbConEmpty+        "use"           -> Just WbConUse+        "read"          -> Just WbConRead+        "alloc"         -> Just WbConAlloc+        _               -> Nothing+++-- Variable names -------------------------------------------------------------+-- | String is a variable name+isVarName :: String -> Bool+isVarName str+ = case str of+     []          -> False+     c : cs +        | isVarStart c +        , and (map isVarBody cs)+        -> True+        +        | _ : _         <- cs+        , Just initCs   <- takeInit cs+        , isVarStart c+        , and (map isVarBody initCs)+        , last cs == '#'+        -> True++        | otherwise+        -> False+++-- | Charater can start a variable name.+isVarStart :: Char -> Bool+isVarStart = isLower+        ++-- | Character can be part of a variable body.+isVarBody  :: Char -> Bool+isVarBody c+        = isUpper c || isLower c || isDigit c || c == '_' || c == '\''+++-- | Read a named, user defined variable.+readVar :: String -> Maybe String+readVar ss+        | isVarName ss  = Just ss+        | otherwise     = Nothing+++-- Constructor names ----------------------------------------------------------+-- | String is a constructor name.+isConName :: String -> Bool+isConName str+ = case str of+     []          -> False+     c : cs +        | isConStart c +        , and (map isConBody cs)+        -> True+        +        | _ : _         <- cs+        , Just initCs   <- takeInit cs+        , isConStart c+        , and (map isConBody initCs)+        , last cs == '#'+        -> True++        | otherwise+        -> False++-- | Character can start a constructor name.+isConStart :: Char -> Bool+isConStart = isUpper+++-- | Charater can be part of a constructor body.+isConBody  :: Char -> Bool+isConBody c           = isUpper c || isLower c || isDigit c || c == '_'+        +++-- | Read a named, user defined `TcCon`.+readCon :: String -> Maybe String+readCon ss+        | isConName ss  = Just ss+        | otherwise     = Nothing+++-- Literal names --------------------------------------------------------------+-- | String is the name of a literal.+isLitName :: String -> Bool+isLitName str+ = case str of+        []      -> False+        c : cs+         | isLitStart c+         , and (map isLitBody cs)+         -> True++         | otherwise+         -> False++-- | Character can start a literal.+isLitStart :: Char -> Bool+isLitStart c+        =   isDigit c+        ||  c == '-'++-- | Character can be part of a literal body.+isLitBody :: Char -> Bool+isLitBody c+        =  isDigit c+        || c == 'b' || c == 'o' || c == 'x'+        || c == 'w' || c == 'i' +        || c == '#'+

@@ -0,0 +1,265 @@++-- | Apply the offside rule to a token stream to add braces.+module DDC.Core.Lexer.Offside+        ( Lexeme        (..)+        , applyOffside+        , addStarts)+where+import DDC.Core.Lexer.Tokens+import DDC.Data.SourcePos+import DDC.Data.Token+++-- | Holds a real token or start symbol which is used to apply the offside rule.+data Lexeme n+        = LexemeToken           (Token (Tok n))+        | LexemeStartLine       Int++        -- | Signal that we're starting a block in this column.+        | LexemeStartBlock      Int+        deriving (Eq, Show)++type Context+        = Int++-- | Apply the offside rule to this token stream.+--   It should have been processed with addStarts first to add the+--   LexemeStartLine/LexemeStartLine tokens.+--+applyOffside +        :: (Eq n, Show n) +        => [Context] +        -> [Lexeme n] +        -> [Token (Tok n)]++-- Wait for the module header before we start applying the real offside rule. +-- This allows us to write 'module Name with letrec' all on the same line.+applyOffside [] (LexemeToken t : ts) +        |   isToken t (KA KModule)+         || isKNToken t+        = t : applyOffside [] ts++-- When we see the top-level letrec then enter into the outer-most context.+applyOffside [] (LexemeToken t1 : (LexemeStartBlock n) : ls)+        |   isToken t1 (KA KLetRec)+         || isToken t1 (KA KExports)+         || isToken t1 (KA KImports)+        = t1 : newCBra ls : applyOffside [n] ls ++-- At top level without a context.+-- Skip over everything until we get the 'with' in 'module Name with ...''+applyOffside [] (LexemeStartLine _  : ts)+        = applyOffside [] ts ++applyOffside [] (LexemeStartBlock _ : ts)+        = applyOffside [] ts+++-- line start+applyOffside mm@(m : ms) (t@(LexemeStartLine n) : ts)+        -- add semicolon to get to the next statement in this block+        | m == n+        = newSemiColon ts : applyOffside mm ts++        -- end a block+        -- we keep the StartLine token in the recursion in case we're ending+        -- multiple blocks difference from Haskell98: add a semicolon as well+        | n < m +        = newSemiColon ts : newCKet ts : applyOffside ms (t : ts)++        -- indented continuation of this statement+        | otherwise+        = applyOffside mm ts+++-- block start+applyOffside mm@(m : ms) (LexemeStartBlock n : ts)+        -- enter into a nested context+        | n > m+        = newCBra ts : applyOffside (n : m : ms) ts ++        -- new context starts less than the current one.+        --   This should never happen, +        --     provided addStarts works.+        | tNext : _    <- dropNewLinesLexeme ts+        = error $ "DDC.Core.Lexer.Tokens.Offside: layout error on " ++ show tNext ++ "."++        -- new context cannot be less indented than outer one+        --   This should never happen,+        --      as there is no lexeme to start a new context at the end of the file+        | []            <- dropNewLinesLexeme ts+        = error "DDC.Core.Lexer.Tokens.Offside: tried to start new context at end of file."++        -- an empty block+        | otherwise+        = newCBra ts : newCKet ts : applyOffside mm (LexemeStartLine n : ts)+++-- pop contexts from explicit close braces+applyOffside mm (LexemeToken t@Token { tokenTok = KA KBraceKet } : ts) ++        -- make sure that explict open braces match explicit close braces+        | 0 : ms        <- mm+        = t : applyOffside ms ts++        -- nup+        | _tNext : _     <- dropNewLinesLexeme ts+        = [newOffsideClosingBrace ts]+++-- push contexts for explicit open braces+applyOffside ms (LexemeToken t@Token { tokenTok = KA KBraceBra } : ts)+        = t : applyOffside (0 : ms) ts++applyOffside ms (LexemeToken t : ts) +        = t : applyOffside ms ts++applyOffside [] []          = []++-- close off remaining contexts once we've reached the end of the stream.+applyOffside (_ : ms) []    = newCKet [] : applyOffside ms []+++-- addStarts ------------------------------------------------------------------+-- | Add block and line start tokens to this stream.+--      This is lifted straight from the Haskell98 report.+addStarts :: Eq n => [Token (Tok n)] -> [Lexeme n]+addStarts ts+ = case dropNewLines ts of++        -- If the first lexeme of a module is not '{' then start a new block.+        (t1 : tsRest)+          |  not $ or $ map (isToken t1) [KA KBraceBra]+          -> LexemeStartBlock (tokenColumn t1) : addStarts' (t1 : tsRest)++          | otherwise+          -> addStarts' (t1 : tsRest)++        -- empty file+        []      -> []+++addStarts'  :: Eq n => [Token (Tok n)] -> [Lexeme n]+addStarts' []           = []+addStarts' (t1 : ts) ++        -- We're starting a block+        | isBlockStart t1+        , []            <- dropNewLines ts+        = LexemeToken t1    : [LexemeStartBlock 0]++        | isBlockStart t1+        , t2 : tsRest   <- dropNewLines ts+        , not $ isToken t2 (KA KBraceBra)+        = LexemeToken t1    : LexemeStartBlock (tokenColumn t2)+                            : addStarts' (t2 : tsRest)++        -- check for start of list+        | isToken t1 (KA KBraceBra)+        = LexemeToken t1    : addStarts' ts++        -- check for end of list+        | isToken t1 (KA KBraceKet)+        = LexemeToken t1    : addStarts' ts++        -- check for start of new line+        | isToken t1 (KM KNewLine)+        , t2 : tsRest   <- dropNewLines ts+        , not $ isToken t2 (KA KBraceBra)+        = LexemeStartLine (tokenColumn t2) +                : addStarts' (t2 : tsRest)++        -- eat up trailine newlines+        | isToken t1 (KM KNewLine)+        = addStarts' ts++        -- a regular token+        | otherwise+        = LexemeToken t1    : addStarts' ts+++-- | Drop newline tokens at the front fo this stream.+dropNewLines :: Eq n => [Token (Tok n)] -> [Token (Tok n)]+dropNewLines []              = []+dropNewLines (t1:ts)+        | isToken t1 (KM KNewLine)+        = dropNewLines ts++        | otherwise+        = t1 : ts+++-- | Drop newline tokens at the front fo this stream.+dropNewLinesLexeme :: Eq n => [Lexeme n] -> [Lexeme n]+dropNewLinesLexeme ll+ = case ll of+        []                      -> []+        LexemeToken t1 : ts+         |  isToken t1 (KM KNewLine)+         -> dropNewLinesLexeme ts++        l : ls+         -> l : dropNewLinesLexeme ls+++-- | Check if a token is one that starts a block of statements.+isBlockStart :: Token (Tok n) -> Bool+isBlockStart Token { tokenTok = tok }+ = case tok of+        KA KDo          -> True+        KA KOf          -> True+        KA KLetRec      -> True+        KA KWhere       -> True+        KA KExports     -> True+        KA KImports     -> True+        _               -> False+++-- Utils ----------------------------------------------------------------------+-- | Test whether this wrapper token matches.+isToken :: Eq n => Token (Tok n) -> Tok n -> Bool+isToken (Token tok _) tok2 = tok == tok2+++-- | Test whether this wrapper token matches.+isKNToken :: Eq n => Token (Tok n) -> Bool+isKNToken (Token (KN _) _)      = True+isKNToken _                     = False+++-- | When generating new source tokens, take the position from the first+--   non-newline token in this list+newCBra :: [Lexeme n] -> Token (Tok n)+newCBra ts+        = (takeTok ts) { tokenTok = KA KBraceBra }+++newCKet :: [Lexeme n] -> Token (Tok n)+newCKet ts+        = (takeTok ts) { tokenTok = KA KBraceKet }+++newSemiColon :: [Lexeme n] -> Token (Tok n)+newSemiColon ts +        = (takeTok ts) { tokenTok = KA KSemiColon }+++-- | This is injected by `applyOffside` when it finds an explit close+--   brace in a position where it would close a synthetic one.+newOffsideClosingBrace :: [Lexeme n] -> Token (Tok n)+newOffsideClosingBrace ts+        = (takeTok ts) { tokenTok = KM KOffsideClosingBrace }+++takeTok :: [Lexeme n] -> Token (Tok n)+takeTok []      + = Token (KJunk "") (SourcePos "" 0 0)++takeTok (l : ls)+ = case l of+        LexemeToken (Token { tokenTok = KM KNewLine })+         -> takeTok ls++        LexemeToken t           -> t+        LexemeStartLine  _      -> takeTok ls+        LexemeStartBlock _      -> takeTok ls

@@ -0,0 +1,347 @@++module DDC.Core.Lexer.Tokens+        ( -- * Tokens+          Tok      (..)+        , renameTok+        , describeTok++          -- * Meta Tokens+        , TokMeta  (..)+        , describeTokMeta++          -- * Atomic Tokens+        , TokAtom  (..)+        , describeTokAtom++          -- * Named Tokens+        , TokNamed (..)+        , describeTokNamed)+where+import DDC.Core.Pretty+import DDC.Core.Exp+import Control.Monad+++-- TokenFamily ----------------------------------------------------------------+-- | The family of a token.+--   This is used to help generate parser error messages,+--   so we can say ''the constructor Cons''+--             and ''the keyword case'' etc.+data TokenFamily+        = Symbol+        | Keyword+        | Constructor+        | Index+        | Variable+++-- | Describe a token family, for parser error messages.+describeTokenFamily :: TokenFamily -> String+describeTokenFamily tf+ = case tf of+        Symbol          -> "symbol"+        Keyword         -> "keyword"+        Constructor     -> "constructor"+        Index           -> "index"+        Variable        -> "variable"+++-- Tok ------------------------------------------------------------------------+-- | Tokens accepted by the core language parser.+data Tok n+        -- | Some junk symbol that isn't part of the language.+        = KJunk String++        -- | Meta tokens contain out-of-band information that is eliminated+        --   before parsing proper.+        | KM    !TokMeta++        -- | Atomic tokens are keywords, punctuation and baked-in +        --   constructor names.+        | KA    !TokAtom ++        -- | A named token that is specific to the language fragment +        --   (maybe it's a primop), or a user defined name.+        | KN    !(TokNamed n)+        deriving (Eq, Show)+++-- | Apply a function to all the names in a `Tok`.+renameTok+        :: Ord n2+        => (n1 -> Maybe n2) +        -> Tok n1 +        -> Maybe (Tok n2)++renameTok f kk+ = case kk of+        KJunk s -> Just $ KJunk s+        KM t    -> Just $ KM t+        KA t    -> Just $ KA t+        KN t    -> liftM KN $ renameTokNamed f t+++-- | Describe a token for parser error messages.+describeTok :: Pretty n => Tok n -> String+describeTok kk+ = case kk of+        KJunk c         -> "character " ++ show c+        KM tm           -> describeTokMeta  tm+        KA ta           -> describeTokAtom  ta+        KN tn           -> describeTokNamed tn+++-- TokMeta --------------------------------------------------------------------+-- | Meta tokens contain out-of-band information that is +--   eliminated before parsing proper.+data TokMeta+        = KNewLine+        | KCommentLineStart+        | KCommentBlockStart+        | KCommentBlockEnd++        -- | This is injected by `dropCommentBlock` when it finds+        --   an unterminated block comment.+        | KCommentUnterminated++        -- | This is injected by `applyOffside` when it finds an explit close+        --   brace in a position where it would close a synthetic one.+        | KOffsideClosingBrace+        deriving (Eq, Show)+++-- | Describe a TokMeta, for lexer error messages.+describeTokMeta :: TokMeta -> String+describeTokMeta tm+ = case tm of+        KNewLine                -> "new line"+        KCommentLineStart       -> "comment start"+        KCommentBlockStart      -> "block comment start"+        KCommentBlockEnd        -> "block comment end"+        KCommentUnterminated    -> "unterminated block comment"+        KOffsideClosingBrace    -> "closing brace"+++-- TokAtom --------------------------------------------------------------------+-- | Atomic tokens are keywords, punctuation and baked-in constructor names.+--   They don't contain user-defined names or primops specific to the +--   language fragment.+data TokAtom+        -- parens+        = KRoundBra+        | KRoundKet+        | KSquareBra+        | KSquareKet+        | KBraceBra+        | KBraceKet+        | KAngleBra+        | KAngleKet++        -- compound parens+        | KSquareColonBra+        | KSquareColonKet+        | KAngleColonBra+        | KAngleColonKet++        -- punctuation+        | KDot+        | KBar+        | KHat+        | KPlus+        | KColon+        | KComma+        | KBackSlash+        | KSemiColon+        | KUnderscore+        | KEquals+        | KAmpersand+        | KDash+        | KColonColon+        | KBigLambda++        -- symbolic constructors+        | KSortComp+        | KSortProp+        | KKindValue+        | KKindRegion+        | KKindEffect+        | KKindClosure+        | KKindWitness+        | KArrowTilde+        | KArrowDash+        | KArrowDashLeft+        | KArrowEquals++        -- bottoms+        | KBotEffect+        | KBotClosure++        -- core keywords+        | KModule+        | KImports+        | KExports+        | KWith+        | KWhere+        | KIn+        | KLet+        | KLazy+        | KLetRec+        | KLetRegions+        | KLetRegion+        | KWithRegion+        | KCase+        | KOf+        | KType+        | KWeakEff+        | KWeakClo+        | KPurify+        | KForget++        -- sugar keywords+        | KDo+        | KMatch+        | KElse++        -- debruijn indices+        | KIndex Int++        -- builtin names ------------+        --   the unit data constructor.+        | KDaConUnit++        --   witness type constructors.+        | KTwConBuiltin TwCon++        --   witness constructors.+        | KWbConBuiltin WbCon++        --   other builtin spec constructors.+        | KTcConBuiltin TcCon+        deriving (Eq, Show)+++-- | Describe a `TokAtom`, for parser error messages.+describeTokAtom  :: TokAtom -> String+describeTokAtom ta+ = let  (family, str)           = describeTokAtom' ta+   in   describeTokenFamily family ++ " " ++ show str++describeTokAtom' :: TokAtom -> (TokenFamily, String)+describeTokAtom' ta+ = case ta of+        -- parens+        KRoundBra               -> (Symbol, "(")+        KRoundKet               -> (Symbol, ")")+        KSquareBra              -> (Symbol, "[")+        KSquareKet              -> (Symbol, "]")+        KBraceBra               -> (Symbol, "{")+        KBraceKet               -> (Symbol, "}")+        KAngleBra               -> (Symbol, "<")+        KAngleKet               -> (Symbol, ">")++        -- compound parens+        KSquareColonBra         -> (Symbol, "[:")+        KSquareColonKet         -> (Symbol, ":]")+        KAngleColonBra          -> (Symbol, "<:")+        KAngleColonKet          -> (Symbol, ":>")++        -- punctuation+        KDot                    -> (Symbol, ".")+        KBar                    -> (Symbol, "|")+        KHat                    -> (Symbol, "^")+        KPlus                   -> (Symbol, "+")+        KColon                  -> (Symbol, ":")+        KComma                  -> (Symbol, ",")+        KBackSlash              -> (Symbol, "\\")+        KSemiColon              -> (Symbol, ";")+        KUnderscore             -> (Symbol, "_")+        KEquals                 -> (Symbol, "=")+        KAmpersand              -> (Symbol, "&")+        KDash                   -> (Symbol, "-")+        KColonColon             -> (Symbol, "::")+        KBigLambda              -> (Symbol, "/\\")++        -- symbolic constructors+        KSortComp               -> (Constructor, "**")+        KSortProp               -> (Constructor, "@@")+        KKindValue              -> (Constructor, "*")+        KKindRegion             -> (Constructor, "%")+        KKindEffect             -> (Constructor, "!")+        KKindClosure            -> (Constructor, "$")+        KKindWitness            -> (Constructor, "@")+        KArrowTilde             -> (Constructor, "~>")+        KArrowDash              -> (Constructor, "->")+        KArrowDashLeft          -> (Constructor, "<-")+        KArrowEquals            -> (Constructor, "=>")++        -- bottoms+        KBotEffect              -> (Constructor, "!0")+        KBotClosure             -> (Constructor, "!$")++        -- expression keywords+        KModule                 -> (Keyword, "module")+        KImports                -> (Keyword, "imports")+        KExports                -> (Keyword, "exports")+        KWith                   -> (Keyword, "with")+        KWhere                  -> (Keyword, "where")+        KIn                     -> (Keyword, "in")+        KLet                    -> (Keyword, "let")+        KLazy                   -> (Keyword, "lazy")+        KLetRec                 -> (Keyword, "letrec")+        KLetRegions             -> (Keyword, "letregions")+        KLetRegion              -> (Keyword, "letregion")+        KWithRegion             -> (Keyword, "withregion")+        KCase                   -> (Keyword, "case")+        KOf                     -> (Keyword, "of")+        KType                   -> (Keyword, "type")+        KWeakEff                -> (Keyword, "weakeff")+        KWeakClo                -> (Keyword, "weakclo")+        KPurify                 -> (Keyword, "purify")+        KForget                 -> (Keyword, "forget")++        -- sugar keywords+        KDo                     -> (Keyword, "do")+        KMatch                  -> (Keyword, "match")+        KElse                   -> (Keyword, "else")++        -- debruijn indices+        KIndex i                -> (Index,   "^" ++ show i)++        -- builtin names+        KDaConUnit              -> (Constructor, "()")+        KTwConBuiltin tw        -> (Constructor, renderPlain $ ppr tw)+        KWbConBuiltin wi        -> (Constructor, renderPlain $ ppr wi)+        KTcConBuiltin tc        -> (Constructor, renderPlain $ ppr tc)+++-- TokNamed -------------------------------------------------------------------+-- | A token with a user-defined name.+data TokNamed n+        = KCon n+        | KVar n+        | KLit n+        deriving (Eq, Show)+++-- | Describe a `TokNamed`, for parser error messages.+describeTokNamed :: Pretty n => TokNamed n -> String+describeTokNamed tn+ = case tn of+        KCon n  -> renderPlain $ text "constructor" <+> (dquotes $ ppr n)+        KVar n  -> renderPlain $ text "variable"    <+> (dquotes $ ppr n)+        KLit n  -> renderPlain $ text "literal"     <+> (dquotes $ ppr n)+++-- | Apply a function to all the names in a `TokNamed`.+renameTokNamed +        :: Ord n2+        => (n1 -> Maybe n2) +        -> TokNamed n1 +        -> Maybe (TokNamed n2)++renameTokNamed f kk+  = case kk of+        KCon c           -> liftM KCon $ f c+        KVar c           -> liftM KVar $ f c+        KLit c           -> liftM KLit $ f c+