diff --git a/DDC/Core/Annot/AnT.hs b/DDC/Core/Annot/AnT.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Annot/AnT.hs @@ -0,0 +1,35 @@ + +module DDC.Core.Annot.AnT + (AnT (..)) +where +import DDC.Type.Exp +import DDC.Base.Pretty +import Control.DeepSeq +import Data.Typeable + + +-- Annot ---------------------------------------------------------------------- +-- | The type checker for witnesses adds this annotation to every node in the, +-- giving the type of each component of the witness. +--- +-- NOTE: We want to leave the components lazy so that the checker +-- doesn't actualy need to produce the type components if they're +-- not needed. +data AnT a n + = AnT + { annotType :: (Type n) + , annotTail :: a } + deriving (Show, Typeable) + + +instance (NFData a, NFData n) => NFData (AnT a n) where + rnf !an + = rnf (annotType an) + `seq` rnf (annotTail an) + + +instance Pretty (AnT a n) where + ppr _ = text "AnT" + + + diff --git a/DDC/Core/Annot/AnTEC.hs b/DDC/Core/Annot/AnTEC.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Annot/AnTEC.hs @@ -0,0 +1,50 @@ + +module DDC.Core.Annot.AnTEC + ( AnTEC (..) + , fromAnT) +where +import DDC.Type.Compounds +import DDC.Type.Exp +import DDC.Base.Pretty +import Control.DeepSeq +import Data.Typeable +import DDC.Core.Annot.AnT (AnT) +import qualified DDC.Core.Annot.AnT as AnT + + +-- Annot ---------------------------------------------------------------------- +-- | The type checker adds this annotation to every node in the AST, +-- giving its type, effect and closure. +--- +-- NOTE: We want to leave the components lazy so that the checker +-- doesn't actualy need to produce the type components if they're +-- not needed. +data AnTEC a n + = AnTEC + { annotType :: (Type n) + , annotEffect :: (Effect n) + , annotClosure :: (Closure n) + , annotTail :: a } + deriving (Show, Typeable) + + +-- | Promote an `AnT` to an `AnTEC` by filling in the effect and closure +-- portions with bottoms. +fromAnT :: AnT a n -> AnTEC a n +fromAnT (AnT.AnT t a) + = (AnTEC t (tBot kEffect) (tBot kClosure) a) + + +instance (NFData a, NFData n) => NFData (AnTEC a n) where + rnf !an + = rnf (annotType an) + `seq` rnf (annotEffect an) + `seq` rnf (annotClosure an) + `seq` rnf (annotTail an) + + +instance Pretty (AnTEC a n) where + ppr _ = text "AnTEC" + + + diff --git a/DDC/Core/Check/CheckDaCon.hs b/DDC/Core/Check/CheckDaCon.hs --- a/DDC/Core/Check/CheckDaCon.hs +++ b/DDC/Core/Check/CheckDaCon.hs @@ -4,7 +4,7 @@ where import DDC.Core.Check.Error import DDC.Core.Check.CheckWitness -import DDC.Core.DaCon +import DDC.Core.Exp.DaCon import DDC.Core.Exp import DDC.Type.Compounds import DDC.Type.DataDef diff --git a/DDC/Core/Check/CheckExp.hs b/DDC/Core/Check/CheckExp.hs --- a/DDC/Core/Check/CheckExp.hs +++ b/DDC/Core/Check/CheckExp.hs @@ -13,10 +13,12 @@ import DDC.Core.Collect import DDC.Core.Pretty import DDC.Core.Exp +import DDC.Core.Annot.AnTEC import DDC.Core.Check.Error import DDC.Core.Check.CheckDaCon import DDC.Core.Check.CheckWitness import DDC.Core.Check.TaggedClosure +import DDC.Core.Transform.Reannotate import DDC.Type.Transform.SubstituteT import DDC.Type.Transform.Crush import DDC.Type.Transform.Trim @@ -35,39 +37,8 @@ import DDC.Data.ListUtils import Data.List as L import Data.Maybe -import Data.Typeable -import Control.DeepSeq --- Annot ---------------------------------------------------------------------- --- | The type checker adds this annotation to every node in the AST, --- giving its type, effect and closure. ---- --- NOTE: We wwant to leave the components lazy so that the checker --- doesn't actualy need to produce the type components if they're --- not needed. -data AnTEC a n - = AnTEC - { annotType :: (Type n) - , annotEffect :: (Effect n) - , annotClosure :: (Closure n) - , annotTail :: a } - deriving (Show, Typeable) - - -instance (NFData a, NFData n) => NFData (AnTEC a n) where - rnf !an - = rnf (annotType an) - `seq` rnf (annotEffect an) - `seq` rnf (annotClosure an) - `seq` rnf (annotTail an) - - -instance Pretty (AnTEC a n) where - ppr _ = text "AnTEC" - - - -- Wrappers ------------------------------------------------------------------- -- | Type check an expression. -- @@ -87,7 +58,7 @@ :: (Ord n, Show n, Pretty n) => Config n -- ^ Static configuration. -> KindEnv n -- ^ Starting Kind environment. - -> TypeEnv n -- ^ Strating Type environment. + -> TypeEnv n -- ^ Starting Type environment. -> Exp a n -- ^ Expression to check. -> Either (Error a n) ( Exp (AnTEC a n) n @@ -209,12 +180,16 @@ -- value-witness application. checkExpM' !config !kenv !tenv xx@(XApp a x1 (XWitness w2)) = do (x1', t1, effs1, clos1) <- checkExpM config kenv tenv x1 - t2 <- checkWitnessM config kenv tenv w2 + + (w2', t2) <- checkWitnessM config kenv tenv w2 + let w2TEC = reannotate fromAnT w2' + + case t1 of TApp (TApp (TCon (TyConWitness TwConImpl)) t11) t12 | t11 `equivT` t2 -> returnX a - (\z -> XApp z x1' (XWitness w2)) + (\z -> XApp z x1' (XWitness w2TEC)) t12 effs1 clos1 | otherwise -> throw $ ErrorAppMismatch xx t11 t2 @@ -226,10 +201,22 @@ = do (x1', t1, effs1, clos1) <- checkExpM config kenv tenv x1 (x2', t2, effs2, clos2) <- checkExpM config kenv tenv x2 - -- Note: we don't need to use the closure of the function because - -- all of its components will already be part of clos1 above. case t1 of - TApp (TApp (TApp (TApp (TCon (TyConSpec TcConFun)) t11) eff) _clo) t12 + -- Oblivious application of a pure function. + -- Computation of the function and argument may themselves have + -- an effect, but the function application does not. + TApp (TApp (TCon (TyConSpec TcConFun)) t11) t12 + | t11 `equivT` t2 + -> returnX a + (\z -> XApp z x1' x2') + t12 + (effs1 `Sum.union` effs2) + (clos1 `Set.union` clos2) + + -- Function with latent effect and closure. + -- Note: we don't need to use the closure of the function because + -- all of its components will already be part of clos1 above. + TApp (TApp (TApp (TApp (TCon (TyConSpec TcConFunEC)) t11) eff) _clo) t12 | t11 `equivT` t2 , effs <- Sum.fromList kEffect [eff] -> returnX a @@ -258,7 +245,7 @@ -- The body of a spec abstraction must be pure. when (e2 /= Sum.empty kEffect) - $ throw $ ErrorLamNotPure xx True (TSum e2) + $ throw $ ErrorLamNotPure xx UniverseSpec (TSum e2) -- The body of a spec abstraction must have data kind. when (not $ isDataKind k2) @@ -322,26 +309,65 @@ -- already already checked that. Just c2_captured - -- If we're suppressing closures then just drop them on the - -- floor. The consumer of this core program doesn't care. - | configSuppressClosures config + -- If we're not tracking closure information then just drop it + -- on the floor. + | not $ configTrackedClosures config = Just $ tBot kClosure | otherwise = trimClosure $ closureOfTaggedSet c2_cut - in returnX a + -- If we're not tracking effect information then just drop it + -- on the floor. + e2_captured + | not $ configTrackedEffects config + = tBot kEffect + + | otherwise + = TSum e2 + + -- If the function type for the current fragment supports + -- latent effects and closures then just use that. + fun_result + | configFunctionalEffects config + , configFunctionalClosures config + = returnX a (\z -> XLam z b1 x2') - (tFun t1 (TSum e2) c2_captured t2) + (tFunEC t1 e2_captured c2_captured t2) (Sum.empty kEffect) c2_cut + -- If the function type for the current fragment does not + -- support latent effects, then the body expression needs + -- to be pure. + | e2_captured == tBot kEffect + , c2_captured == tBot kClosure + = returnX a + (\z -> XLam z b1 x2') + (tFun t1 t2) + (Sum.empty kEffect) + Set.empty + + | e2_captured /= tBot kEffect + = throw $ ErrorLamNotPure xx UniverseData e2_captured + + | c2_captured /= tBot kClosure + = throw $ ErrorLamNotEmpty xx UniverseData c2_captured + + -- One of the above error cases is supposed to fire, + -- so we should never hit this error. + | otherwise + = error "checkExpM': can't build function type." + + in fun_result + + -- This is a witness abstraction. Just UniverseWitness -- The body of a witness abstraction must be pure. | e2 /= Sum.empty kEffect - -> throw $ ErrorLamNotPure xx False (TSum e2) + -> throw $ ErrorLamNotPure xx UniverseWitness (TSum e2) -- The body of a witness abstraction must produce data. | not $ isDataKind k2 @@ -658,7 +684,9 @@ -- Purify an effect, given a witness that it is pure. checkExpM' !config !kenv !tenv xx@(XCast a (CastPurify w) x1) = do - tW <- checkWitnessM config kenv tenv w + (w', tW) <- checkWitnessM config kenv tenv w + let wTEC = reannotate fromAnT w' + (x1', t1, effs, clo) <- checkExpM config kenv tenv x1 effs' <- case tW of @@ -666,7 +694,7 @@ -> return $ Sum.delete effMask effs _ -> throw $ ErrorWitnessNotPurity xx w tW - let c' = CastPurify w + let c' = CastPurify wTEC returnX a (\z -> XCast z c' x1') @@ -676,9 +704,11 @@ -- Forget a closure, given a witness that it is empty. checkExpM' !config !kenv !tenv xx@(XCast a (CastForget w) x1) = do - tW <- checkWitnessM config kenv tenv w - (x1', t1, effs, clos) <- checkExpM config kenv tenv x1 + (w', tW) <- checkWitnessM config kenv tenv w + let wTEC = reannotate fromAnT w' + (x1', t1, effs, clos) <- checkExpM config kenv tenv x1 + clos' <- case tW of TApp (TCon (TyConWitness TwConEmpty)) cloMask -> return $ maskFromTaggedSet @@ -687,13 +717,44 @@ _ -> throw $ ErrorWitnessNotEmpty xx w tW - let c' = CastForget w + let c' = CastForget wTEC returnX a (\z -> XCast z c' x1') t1 effs clos' +-- Suspend a computation, +-- capturing its effects in a computation type. +checkExpM' !config !kenv !tenv (XCast a CastSuspend x1) + = do + (x1', t1, effs, clos) <- checkExpM config kenv tenv x1 + + let tS = tApps (TCon (TyConSpec TcConSusp)) + [TSum effs, t1] + + returnX a + (\z -> XCast z CastSuspend x1') + tS (Sum.empty kEffect) clos + + +-- Run a suspended computation, +-- releasing its effects into the environment. +checkExpM' !config !kenv !tenv xx@(XCast a CastRun x1) + = do + (x1', t1, effs, clos) <- checkExpM config kenv tenv x1 + + case t1 of + TApp (TApp (TCon (TyConSpec TcConSusp)) eff2) tA + -> returnX a + (\z -> XCast z CastRun x1') + tA + (Sum.union effs (Sum.singleton kEffect eff2)) + clos + + _ -> throw $ ErrorRunNotSuspension xx t1 + + -- Type and witness expressions can only appear as the arguments -- to applications. checkExpM' !_config !_kenv !_tenv xx@(XType _) @@ -702,8 +763,9 @@ checkExpM' !_config !_kenv !_tenv xx@(XWitness _) = throw $ ErrorNakedWitness xx +-- This shouldn't happen. checkExpM' _ _ _ _ - = error "checkExpM: bogus warning killer" + = error "checkExpM: can't check this expression" -- | Like `checkExp` but we allow naked types and witnesses. @@ -727,8 +789,8 @@ , clo) XWitness w - -> do checkWitnessM config kenv tenv w - return ( XWitness w + -> do (w', _) <- checkWitnessM config kenv tenv w + return ( XWitness (reannotate fromAnT w') , Set.empty) _ -> do @@ -760,6 +822,7 @@ , t, es, cs) {-# INLINE returnX #-} + ------------------------------------------------------------------------------- -- | Check some let bindings. checkLetsM @@ -775,7 +838,7 @@ , TypeSum n , Set (TaggedClosure n)) -checkLetsM !xx !config !kenv !tenv (LLet mode b11 x12) +checkLetsM !xx !config !kenv !tenv (LLet b11 x12) = do -- Check the right of the binding. (x12', t12, effs12, clo12) @@ -789,45 +852,7 @@ when (not $ isDataKind k11') $ throw $ ErrorLetBindingNotData xx b11' k11' - -- Check purity and emptiness for lazy bindings. - (case mode of - LetStrict -> return () - LetLazy _ - -> do let eff12' = TSum effs12 - when (not $ isBot eff12') - $ throw $ ErrorLetLazyNotPure xx b11 eff12' - - let clo12' = closureOfTaggedSet clo12 - when (not $ isBot clo12') - $ throw $ ErrorLetLazyNotEmpty xx b11 clo12') - - -- Check region witness for lazy bindings. - (case mode of - LetStrict -> return () - - -- Type of lazy binding has no head region, like Unit and (->). - LetLazy Nothing - -> do case takeDataTyConApps t12 of - Just (_tc, t1 : _) - -> do k1 <- checkTypeM config kenv t1 - when (isRegionKind k1) - $ throw $ ErrorLetLazyNoWitness xx b11 t12 - - _ -> return () - - -- Type of lazy binding might have a head region, - -- so we need a Lazy witness for it. - LetLazy (Just wit) - -> do tWit <- checkWitnessM config kenv tenv wit - let tWitExp = case takeDataTyConApps t12 of - Just (_tc, tR : _ts) -> tLazy tR - _ -> tHeadLazy t12 - - when (not $ equivT tWit tWitExp) - $ throw $ ErrorLetLazyWitnessTypeMismatch - xx b11 tWit t12 tWitExp) - - return ( LLet mode b11' x12' + return ( LLet b11' x12' , [b11'] , effs12 , clo12) diff --git a/DDC/Core/Check/CheckModule.hs b/DDC/Core/Check/CheckModule.hs --- a/DDC/Core/Check/CheckModule.hs +++ b/DDC/Core/Check/CheckModule.hs @@ -93,7 +93,7 @@ checkModuleBinds !ksExports !tsExports !xx = case xx of - XLet _ (LLet _ b _) x2 + XLet _ (LLet b _) x2 -> do checkModuleBind ksExports tsExports b env <- checkModuleBinds ksExports tsExports x2 return $ Env.extend b env @@ -153,7 +153,7 @@ -> CheckM a n (Kind n) checkTypeM !config !kenv !tt - = case T.checkType (configPrimDataDefs config) kenv tt of + = case T.checkType config kenv tt of Left err -> throw $ ErrorType err Right k -> return k diff --git a/DDC/Core/Check/CheckWitness.hs b/DDC/Core/Check/CheckWitness.hs --- a/DDC/Core/Check/CheckWitness.hs +++ b/DDC/Core/Check/CheckWitness.hs @@ -14,10 +14,11 @@ , checkTypeM) where import DDC.Core.Exp +import DDC.Core.Annot.AnT import DDC.Core.Pretty import DDC.Core.Check.Error import DDC.Core.Check.ErrorMessage () -import DDC.Type.DataDef +import DDC.Type.Check (Config (..), configOfProfile) import DDC.Type.Transform.SubstituteT import DDC.Type.Compounds import DDC.Type.Universe @@ -28,7 +29,6 @@ import qualified DDC.Control.Monad.Check as G import qualified DDC.Type.Env as Env import qualified DDC.Type.Check as T -import qualified DDC.Core.Fragment as F -- | Type checker monad. @@ -36,46 +36,6 @@ type CheckM a n = G.CheckM (Error a n) --- Config --------------------------------------------------------------------- --- | Static configuration for the type checker. --- These fields don't change as we decend into the tree. --- --- The starting configuration should be converted from the profile that --- defines the language fragment you are checking. --- See "DDC.Core.Fragment" and use `configOfProfile` below. -data Config n - = Config - { -- | Data type definitions. - configPrimDataDefs :: DataDefs n - - -- | Kinds of primitive types. - , configPrimKinds :: KindEnv n - - -- | Types of primitive operators. - , configPrimTypes :: TypeEnv n - - -- | Suppress all closure information, - -- annotating all functions with an empty closure. - -- - -- This is used when checking the Disciple Core Salt fragment, - -- as transforms in this language don't use the closure - -- information. - , configSuppressClosures :: Bool } - - --- | Convert a langage profile to a type checker configuration. -configOfProfile :: F.Profile n -> Config n -configOfProfile profile - = Config - { configPrimDataDefs = F.profilePrimDataDefs profile - , configPrimKinds = F.profilePrimKinds profile - , configPrimTypes = F.profilePrimTypes profile - - , configSuppressClosures - = F.featuresUntrackedClosures - $ F.profileFeatures profile } - - -- Wrappers -------------------------------------------------------------------- -- | Check a witness. -- @@ -96,8 +56,10 @@ => Config n -- ^ Static configuration. -> KindEnv n -- ^ Starting Kind Environment. -> TypeEnv n -- ^ Strating Type Environment. - -> Witness n -- ^ Witness to check. - -> Either (Error a n) (Type n) + -> Witness a n -- ^ Witness to check. + -> Either (Error a n) + ( Witness (AnT a n) n + , Type n) checkWitness config kenv tenv xx = result $ checkWitnessM config kenv tenv xx @@ -112,12 +74,13 @@ typeOfWitness :: (Ord n, Show n, Pretty n) => Config n - -> Witness n + -> Witness a n -> Either (Error a n) (Type n) typeOfWitness config ww - = result - $ checkWitnessM config Env.empty Env.empty ww + = case checkWitness config Env.empty Env.empty ww of + Left err -> Left err + Right (_, t) -> Right t ------------------------------------------------------------------------------ @@ -127,61 +90,75 @@ => Config n -- ^ Data type definitions. -> KindEnv n -- ^ Kind environment. -> TypeEnv n -- ^ Type environment. - -> Witness n -- ^ Witness to check. - -> CheckM a n (Type n) + -> Witness a n -- ^ Witness to check. + -> CheckM a n + ( Witness (AnT a n) n + , Type n) -checkWitnessM !_config !_kenv !tenv (WVar u) +checkWitnessM !_config !_kenv !tenv (WVar a u) = case Env.lookup u tenv of Nothing -> throw $ ErrorUndefinedVar u UniverseWitness - Just t -> return t + Just t -> return ( WVar (AnT t a) u + , t) -checkWitnessM !_config !_kenv !_tenv (WCon wc) - = return $ typeOfWiCon wc +checkWitnessM !_config !_kenv !_tenv (WCon a wc) + = let t' = typeOfWiCon wc + in return ( WCon (AnT t' a) wc + , t') -- witness-type application -checkWitnessM !config !kenv !tenv ww@(WApp w1 (WType t2)) - = do t1 <- checkWitnessM config kenv tenv w1 - k2 <- checkTypeM config kenv t2 +checkWitnessM !config !kenv !tenv ww@(WApp a1 w1 (WType a2 t2)) + = do (w1', t1) <- checkWitnessM config kenv tenv w1 + k2 <- checkTypeM config kenv t2 case t1 of TForall b11 t12 | typeOfBind b11 == k2 - -> return $ substituteT b11 t2 t12 + -> let t' = substituteT b11 t2 t12 + in return ( WApp (AnT t' a1) w1' (WType (AnT k2 a2) t2) + , t') | otherwise -> throw $ ErrorWAppMismatch ww (typeOfBind b11) k2 _ -> throw $ ErrorWAppNotCtor ww t1 t2 -- witness-witness application -checkWitnessM !config !kenv !tenv ww@(WApp w1 w2) - = do t1 <- checkWitnessM config kenv tenv w1 - t2 <- checkWitnessM config kenv tenv w2 +checkWitnessM !config !kenv !tenv ww@(WApp a w1 w2) + = do (w1', t1) <- checkWitnessM config kenv tenv w1 + (w2', t2) <- checkWitnessM config kenv tenv w2 case t1 of TApp (TApp (TCon (TyConWitness TwConImpl)) t11) t12 | t11 == t2 - -> return t12 - + -> return ( WApp (AnT t12 a) w1' w2' + , t12) + | otherwise -> throw $ ErrorWAppMismatch ww t11 t2 _ -> throw $ ErrorWAppNotCtor ww t1 t2 -- witness joining -checkWitnessM !config !kenv !tenv ww@(WJoin w1 w2) - = do t1 <- checkWitnessM config kenv tenv w1 - t2 <- checkWitnessM config kenv tenv w2 +checkWitnessM !config !kenv !tenv ww@(WJoin a w1 w2) + = do (w1', t1) <- checkWitnessM config kenv tenv w1 + (w2', t2) <- checkWitnessM config kenv tenv w2 case (t1, t2) of ( TApp (TCon (TyConWitness TwConPure)) eff1 , TApp (TCon (TyConWitness TwConPure)) eff2) - -> return $ TApp (TCon (TyConWitness TwConPure)) - (TSum $ Sum.fromList kEffect [eff1, eff2]) + -> let t' = TApp (TCon (TyConWitness TwConPure)) + (TSum $ Sum.fromList kEffect [eff1, eff2]) + in return ( WJoin (AnT t' a) w1' w2' + , t') ( TApp (TCon (TyConWitness TwConEmpty)) clo1 , TApp (TCon (TyConWitness TwConEmpty)) clo2) - -> return $ TApp (TCon (TyConWitness TwConEmpty)) - (TSum $ Sum.fromList kClosure [clo1, clo2]) + -> let t' = TApp (TCon (TyConWitness TwConEmpty)) + (TSum $ Sum.fromList kClosure [clo1, clo2]) + in return ( WJoin (AnT t' a) w1' w2' + , t') _ -> throw $ ErrorCannotJoin ww w1 t1 w2 t2 -- embedded types -checkWitnessM !config !kenv !_tenv (WType t) - = checkTypeM config kenv t +checkWitnessM !config !kenv !_tenv (WType a t) + = do k <- checkTypeM config kenv t + return ( WType (AnT k a) t + , k) -- | Take the type of a witness constructor. @@ -213,7 +190,7 @@ -> CheckM a n (Kind n) checkTypeM config kenv tt - = case T.checkType (configPrimDataDefs config) kenv tt of + = case T.checkType config kenv tt of Left err -> throw $ ErrorType err Right k -> return k diff --git a/DDC/Core/Check/Error.hs b/DDC/Core/Check/Error.hs --- a/DDC/Core/Check/Error.hs +++ b/DDC/Core/Check/Error.hs @@ -83,12 +83,20 @@ { errorChecking :: Exp a n , errorBind :: Bind n } - -- | A type or witness abstraction where the body has a visible side effect. + -- | An abstraction where the body has a visible side effect that + -- is not supported by the current language fragment. | ErrorLamNotPure { errorChecking :: Exp a n - , errorSpecOrWit :: Bool + , errorUniverse :: Universe , errorEffect :: Effect n } + -- | An abstraction where the body has a visible closure that + -- is not supported by the current language fragment. + | ErrorLamNotEmpty + { errorChecking :: Exp a n + , errorUniverse :: Universe + , errorClosure :: Closure n } + -- | A value function where the parameter does not have data kind. | ErrorLamBindNotData { errorChecking :: Exp a n @@ -124,34 +132,6 @@ , errorKind :: Kind n } - -- Let Lazy --------------------------------------- - -- | A lazy let binding that has a visible side effect. - | ErrorLetLazyNotPure - { errorChecking :: Exp a n - , errorBind :: Bind n - , errorEffect :: Effect n } - - -- | A lazy let binding with a non-empty closure. - | ErrorLetLazyNotEmpty - { errorChecking :: Exp a n - , errorBind :: Bind n - , errorClosure :: Closure n } - - -- | A lazy let binding without a witness that binding is in a lazy region. - | ErrorLetLazyNoWitness - { errorChecking :: Exp a n - , errorBind :: Bind n - , errorType :: Type n } - - -- | A lazy let binding where the witness has the wrong type. - | ErrorLetLazyWitnessTypeMismatch - { errorChecking :: Exp a n - , errorBind :: Bind n - , errorWitnessTypeHave :: Type n - , errorBindType :: Type n - , errorWitnessTypeExpect :: Type n } - - -- Letrec ----------------------------------------- -- | A recursive let-expression where the right of the binding is not -- a lambda abstraction. @@ -232,34 +212,34 @@ -- | A witness application where the argument type does not match -- the parameter type. | ErrorWAppMismatch - { errorWitness :: Witness n + { errorWitness :: Witness a n , errorParamType :: Type n , errorArgType :: Type n } -- | Tried to perform a witness application with a non-witness. | ErrorWAppNotCtor - { errorWitness :: Witness n + { errorWitness :: Witness a n , errorNotFunType :: Type n , errorArgType :: Type n } -- | An invalid witness join. | ErrorCannotJoin - { errorWitness :: Witness n - , errorWitnessLeft :: Witness n + { errorWitness :: Witness a n + , errorWitnessLeft :: Witness a n , errorTypeLeft :: Type n - , errorWitnessRight :: Witness n + , errorWitnessRight :: Witness a n , errorTypeRight :: Type n } -- | A witness provided for a purify cast that does not witness purity. | ErrorWitnessNotPurity { errorChecking :: Exp a n - , errorWitness :: Witness n + , errorWitness :: Witness a n , errorType :: Type n } -- | A witness provided for a forget cast that does not witness emptiness. | ErrorWitnessNotEmpty { errorChecking :: Exp a n - , errorWitness :: Witness n + , errorWitness :: Witness a n , errorType :: Type n } @@ -337,6 +317,11 @@ { errorChecking :: Exp a n , errorEffect :: Effect n , errorKind :: Kind n } + + -- | A run cast applied to a non-suspension. + | ErrorRunNotSuspension + { errorChecking :: Exp a n + , errorType :: Type n } -- Types ------------------------------------------ diff --git a/DDC/Core/Check/ErrorMessage.hs b/DDC/Core/Check/ErrorMessage.hs --- a/DDC/Core/Check/ErrorMessage.hs +++ b/DDC/Core/Check/ErrorMessage.hs @@ -85,16 +85,20 @@ , text " is already in the environment." , text "with: " <> align (ppr xx) ] - ErrorLamNotPure xx spec eff - -> let universe' = if spec then text "spec" - else text "witness" - in vcat - [ text "Impure" <+> universe' <+> text "abstraction" + ErrorLamNotPure xx universe eff + -> vcat + [ text "Impure" <+> ppr universe <+> text "abstraction" , text " has effect: " <> ppr eff , empty , text "with: " <> align (ppr xx) ] + + ErrorLamNotEmpty xx universe eff + -> vcat + [ text "Non-empty" <+> ppr universe <+> text "abstraction" + , text " has closure: " <> ppr eff + , empty + , text "with: " <> align (ppr xx) ] - ErrorLamBindNotData xx t1 k1 -> vcat [ text "Function parameter does not have data kind." , text " The function parameter:" <> ppr t1 @@ -140,37 +144,6 @@ , text "with: " <> align (ppr xx) ] - -- Let Lazy --------------------------------------- - ErrorLetLazyNotEmpty xx b clo - -> vcat [ text "Lazy let binding is not empty." - , text " The binding for: " <> ppr (binderOfBind b) - , text " has closure: " <> ppr clo - , empty - , text "with: " <> align (ppr xx) ] - - ErrorLetLazyNotPure xx b eff - -> vcat [ text "Lazy let binding is not pure." - , text " The binding for: " <> ppr (binderOfBind b) - , text " has effect: " <> ppr eff - , empty - , text "with: " <> align (ppr xx) ] - - ErrorLetLazyNoWitness xx b t - -> vcat [ text "Lazy let binding has no witness but the bound value may have a head region." - , text " The binding for: " <> ppr (binderOfBind b) - , text " Has type: " <> ppr t - , empty - , text "with: " <> align (ppr xx) ] - - ErrorLetLazyWitnessTypeMismatch xx b tWitGot tBind tWitExp - -> vcat [ text "Unexpected witness type in lazy let binding." - , text " The binding for: " <> ppr (binderOfBind b) - , text " has a witness of type: " <> ppr tWitGot - , text " but is type is: " <> ppr tBind - , text " so the witness should be: " <> ppr tWitExp - , empty - , text "with: " <> align (ppr xx) ] - -- Letrec ----------------------------------------- ErrorLetrecBindingNotLambda xx x -> vcat [ text "Letrec can only bind lambda abstractions." @@ -373,6 +346,13 @@ , empty , text "with: " <> align (ppr xx) ] + ErrorRunNotSuspension xx t + -> vcat [ text "Expression to run is not a suspension." + , text " Type: " <> ppr t + , empty + , text "with: " <> align (ppr xx) ] + + -- Type ------------------------------------------- ErrorNakedType xx -> vcat [ text "Found naked type in core program." diff --git a/DDC/Core/Collect/Free.hs b/DDC/Core/Collect/Free.hs --- a/DDC/Core/Collect/Free.hs +++ b/DDC/Core/Collect/Free.hs @@ -59,9 +59,8 @@ XLAM _ b x -> [bindDefT BindLAM [b] [x]] XLam _ b x -> [bindDefX BindLam [b] [x]] - XLet _ (LLet m b x1) x2 - -> slurpBindTree m - ++ slurpBindTree x1 + XLet _ (LLet b x1) x2 + -> slurpBindTree x1 ++ [bindDefX BindLet [b] [x2]] XLet _ (LRec bxs) x2 @@ -82,14 +81,6 @@ XWitness w -> slurpBindTree w -instance BindStruct LetMode where - slurpBindTree mode - = case mode of - LetStrict -> [] - LetLazy Nothing -> [] - LetLazy (Just ww) -> slurpBindTree ww - - instance BindStruct (Cast a) where slurpBindTree cc = case cc of @@ -97,6 +88,8 @@ CastWeakenClosure xs -> concatMap slurpBindTree xs CastPurify w -> slurpBindTree w CastForget w -> slurpBindTree w + CastSuspend -> [] + CastRun -> [] instance BindStruct (Alt a) where @@ -109,14 +102,14 @@ -> [bindDefX BindCasePat bs [x]] -instance BindStruct Witness where +instance BindStruct (Witness a) where slurpBindTree ww = case ww of - WVar u -> [BindUse BoundWit u] + WVar _ u -> [BindUse BoundWit u] WCon{} -> [] - WApp w1 w2 -> slurpBindTree w1 ++ slurpBindTree w2 - WJoin w1 w2 -> slurpBindTree w1 ++ slurpBindTree w2 - WType t -> slurpBindTree t + WApp _ w1 w2 -> slurpBindTree w1 ++ slurpBindTree w2 + WJoin _ w1 w2 -> slurpBindTree w1 ++ slurpBindTree w2 + WType _ t -> slurpBindTree t -- | Helper for constructing the `BindTree` for an expression or witness binder. diff --git a/DDC/Core/Collect/Support.hs b/DDC/Core/Collect/Support.hs --- a/DDC/Core/Collect/Support.hs +++ b/DDC/Core/Collect/Support.hs @@ -137,25 +137,25 @@ in support kenv tenv' x -instance SupportX Witness where +instance SupportX (Witness a) where support kenv tenv ww = case ww of - WVar u + WVar _ u | Env.member u tenv -> mempty | otherwise -> mempty { supportWiVar = Set.singleton u } WCon{} -> mempty - WApp w1 w2 + WApp _ w1 w2 -> support kenv tenv w1 <> support kenv tenv w2 - WJoin w1 w2 + WJoin _ w1 w2 -> support kenv tenv w1 <> support kenv tenv w2 - WType t + WType _ t -> support kenv tenv t @@ -173,14 +173,19 @@ CastForget w -> support kenv tenv w + + CastSuspend + -> mempty + + CastRun + -> mempty instance SupportX (Lets a) where support kenv tenv lts = case lts of - LLet m b x - -> support kenv tenv m - <> support kenv tenv b + LLet b x + -> support kenv tenv b <> support kenv (Env.extend b tenv) x LRec bxs @@ -196,13 +201,4 @@ LWithRegion u | Env.member u kenv -> mempty | otherwise -> mempty { supportSpVar = Set.singleton u } - - -instance SupportX LetMode where - support kenv tenv mm - = case mm of - LetStrict -> mempty - LetLazy Nothing -> mempty - LetLazy (Just w) -> support kenv tenv w - diff --git a/DDC/Core/Compounds.hs b/DDC/Core/Compounds.hs --- a/DDC/Core/Compounds.hs +++ b/DDC/Core/Compounds.hs @@ -1,332 +1,7 @@ -- | Utilities for constructing and destructing compound expressions. module DDC.Core.Compounds - ( module DDC.Type.Compounds - , module DDC.Core.DaCon - - -- * Annotations - , takeAnnotOfExp - - -- * Lambdas - , xLAMs - , xLams - , makeXLamFlags - , takeXLAMs - , takeXLams - , takeXLamFlags - - -- * Applications - , xApps - , makeXAppsWithAnnots - , takeXApps - , takeXApps1 - , takeXAppsAsList - , takeXAppsWithAnnots - , takeXConApps - , takeXPrimApps - - -- * Lets - , xLets - , splitXLets - , bindsOfLets - , specBindsOfLets - , valwitBindsOfLets - - -- * Patterns - , bindsOfPat - - -- * Alternatives - , takeCtorNameOfAlt - - -- * Witnesses - , wApp - , wApps - , takeXWitness - , takeWAppsAsList - , takePrimWiConApps - - -- * Types - , takeXType - - -- * Units - , xUnit) + ( module DDC.Core.Compounds.Annot ) where -import DDC.Type.Compounds -import DDC.Core.Exp -import DDC.Core.DaCon - - --- Annotations ---------------------------------------------------------------- --- | Take the outermost annotation from an expression, --- or Nothing if this is an `XType` or `XWitness` without an annotation. -takeAnnotOfExp :: Exp a n -> Maybe a -takeAnnotOfExp xx - = case xx of - XVar a _ -> Just a - XCon a _ -> Just a - XLAM a _ _ -> Just a - XLam a _ _ -> Just a - XApp a _ _ -> Just a - XLet a _ _ -> Just a - XCase a _ _ -> Just a - XCast a _ _ -> Just a - XType{} -> Nothing - XWitness{} -> Nothing - - --- Lambdas --------------------------------------------------------------------- --- | Make some nested type lambdas. -xLAMs :: a -> [Bind n] -> Exp a n -> Exp a n -xLAMs a bs x - = foldr (XLAM a) x (reverse bs) - - --- | Make some nested value or witness lambdas. -xLams :: a -> [Bind n] -> Exp a n -> Exp a n -xLams a bs x - = foldr (XLam a) x (reverse bs) - - --- | Split type lambdas from the front of an expression, --- or `Nothing` if there aren't any. -takeXLAMs :: Exp a n -> Maybe ([Bind n], Exp a n) -takeXLAMs xx - = let go bs (XLAM _ b x) = go (b:bs) x - go bs x = (reverse bs, x) - in case go [] xx of - ([], _) -> Nothing - (bs, body) -> Just (bs, body) - - --- | Split nested value or witness lambdas from the front of an expression, --- or `Nothing` if there aren't any. -takeXLams :: Exp a n -> Maybe ([Bind n], Exp a n) -takeXLams xx - = let go bs (XLam _ b x) = go (b:bs) x - go bs x = (reverse bs, x) - in case go [] xx of - ([], _) -> Nothing - (bs, body) -> Just (bs, body) - - --- | Make some nested lambda abstractions, --- using a flag to indicate whether the lambda is a --- level-1 (True), or level-0 (False) binder. -makeXLamFlags :: a -> [(Bool, Bind n)] -> Exp a n -> Exp a n -makeXLamFlags a fbs x - = foldr (\(f, b) x' - -> if f then XLAM a b x' - else XLam a b x') - x fbs - - --- | Split nested lambdas from the front of an expression, --- with a flag indicating whether the lambda was a level-1 (True), --- or level-0 (False) binder. -takeXLamFlags :: Exp a n -> Maybe ([(Bool, Bind n)], Exp a n) -takeXLamFlags xx - = let go bs (XLAM _ b x) = go ((True, b):bs) x - go bs (XLam _ b x) = go ((False, b):bs) x - go bs x = (reverse bs, x) - in case go [] xx of - ([], _) -> Nothing - (bs, body) -> Just (bs, body) - - --- Applications --------------------------------------------------------------- --- | Build sequence of value applications. -xApps :: a -> Exp a n -> [Exp a n] -> Exp a n -xApps a t1 ts = foldl (XApp a) t1 ts - - --- | Build sequence of applications. --- Similar to `xApps` but also takes list of annotations for --- the `XApp` constructors. -makeXAppsWithAnnots :: Exp a n -> [(Exp a n, a)] -> Exp a n -makeXAppsWithAnnots f xas - = case xas of - [] -> f - (arg,a ) : as -> makeXAppsWithAnnots (XApp a f arg) as - - --- | Flatten an application into the function part and its arguments. --- --- Returns `Nothing` if there is no outer application. -takeXApps :: Exp a n -> Maybe (Exp a n, [Exp a n]) -takeXApps xx - = case takeXAppsAsList xx of - (x1 : xsArgs) -> Just (x1, xsArgs) - _ -> Nothing - - --- | Flatten an application into the function part and its arguments. --- --- This is like `takeXApps` above, except we know there is at least one argument. -takeXApps1 :: Exp a n -> Exp a n -> (Exp a n, [Exp a n]) -takeXApps1 x1 x2 - = case takeXApps x1 of - Nothing -> (x1, [x2]) - Just (x11, x12s) -> (x11, x12s ++ [x2]) - - --- | Flatten an application into the function parts and arguments, if any. -takeXAppsAsList :: Exp a n -> [Exp a n] -takeXAppsAsList xx - = case xx of - XApp _ x1 x2 -> takeXAppsAsList x1 ++ [x2] - _ -> [xx] - - --- | Destruct sequence of applications. --- Similar to `takeXAppsAsList` but also keeps annotations for later. -takeXAppsWithAnnots :: Exp a n -> (Exp a n, [(Exp a n, a)]) -takeXAppsWithAnnots xx - = case xx of - XApp a f arg - -> let (f', args') = takeXAppsWithAnnots f - in (f', args' ++ [(arg,a)]) - - _ -> (xx, []) - - --- | Flatten an application of a primop into the variable --- and its arguments. --- --- Returns `Nothing` if the expression isn't a primop application. -takeXPrimApps :: Exp a n -> Maybe (n, [Exp a n]) -takeXPrimApps xx - = case takeXAppsAsList xx of - XVar _ (UPrim p _) : xs -> Just (p, xs) - _ -> Nothing - --- | Flatten an application of a data constructor into the constructor --- and its arguments. --- --- Returns `Nothing` if the expression isn't a constructor application. -takeXConApps :: Exp a n -> Maybe (DaCon n, [Exp a n]) -takeXConApps xx - = case takeXAppsAsList xx of - XCon _ dc : xs -> Just (dc, xs) - _ -> Nothing - - --- Lets ----------------------------------------------------------------------- --- | Wrap some let-bindings around an expression. -xLets :: a -> [Lets a n] -> Exp a n -> Exp a n -xLets a lts x - = foldr (XLet a) x lts - - --- | Split let-bindings from the front of an expression, if any. -splitXLets :: Exp a n -> ([Lets a n], Exp a n) -splitXLets xx - = case xx of - XLet _ lts x - -> let (lts', x') = splitXLets x - in (lts : lts', x') - - _ -> ([], xx) - --- | Take the binds of a `Lets`. --- --- The level-1 and level-0 binders are returned separately. -bindsOfLets :: Lets a n -> ([Bind n], [Bind n]) -bindsOfLets ll - = case ll of - LLet _ b _ -> ([], [b]) - LRec bxs -> ([], map fst bxs) - LLetRegions bs bbs -> (bs, bbs) - LWithRegion{} -> ([], []) - - --- | Like `bindsOfLets` but only take the spec (level-1) binders. -specBindsOfLets :: Lets a n -> [Bind n] -specBindsOfLets ll - = case ll of - LLet _ _ _ -> [] - LRec _ -> [] - LLetRegions bs _ -> bs - LWithRegion{} -> [] - - --- | Like `bindsOfLets` but only take the value and witness (level-0) binders. -valwitBindsOfLets :: Lets a n -> [Bind n] -valwitBindsOfLets ll - = case ll of - LLet _ b _ -> [b] - LRec bxs -> map fst bxs - LLetRegions _ bs -> bs - LWithRegion{} -> [] - - --- Alternatives --------------------------------------------------------------- --- | Take the constructor name of an alternative, if there is one. -takeCtorNameOfAlt :: Alt a n -> Maybe n -takeCtorNameOfAlt aa - = case aa of - AAlt (PData dc _) _ -> takeNameOfDaCon dc - _ -> Nothing - - --- Patterns ------------------------------------------------------------------- --- | Take the binds of a `Pat`. -bindsOfPat :: Pat n -> [Bind n] -bindsOfPat pp - = case pp of - PDefault -> [] - PData _ bs -> bs - - --- Witnesses ------------------------------------------------------------------ --- | Construct a witness application -wApp :: Witness n -> Witness n -> Witness n -wApp = WApp - - --- | Construct a sequence of witness applications -wApps :: Witness n -> [Witness n] -> Witness n -wApps = foldl wApp - - --- | Take the witness from an `XWitness` argument, if any. -takeXWitness :: Exp a n -> Maybe (Witness n) -takeXWitness xx - = case xx of - XWitness t -> Just t - _ -> Nothing - - --- | Flatten an application into the function parts and arguments, if any. -takeWAppsAsList :: Witness n -> [Witness n] -takeWAppsAsList ww - = case ww of - WApp w1 w2 -> takeWAppsAsList w1 ++ [w2] - _ -> [ww] - - --- | Flatten an application of a witness into the witness constructor --- name and its arguments. --- --- Returns nothing if there is no witness constructor in head position. -takePrimWiConApps :: Witness n -> Maybe (n, [Witness n]) -takePrimWiConApps ww - = case takeWAppsAsList ww of - WCon wc : args | WiConBound (UPrim n _) _ <- wc - -> Just (n, args) - _ -> Nothing - - --- Types ---------------------------------------------------------------------- --- | Take the type from an `XType` argument, if any. -takeXType :: Exp a n -> Maybe (Type n) -takeXType xx - = case xx of - XType t -> Just t - _ -> Nothing - - --- Units ----------------------------------------------------------------------- --- | Construct a value of unit type. -xUnit :: a -> Exp a n -xUnit a = XCon a dcUnit +import DDC.Core.Compounds.Annot diff --git a/DDC/Core/Compounds/Annot.hs b/DDC/Core/Compounds/Annot.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Compounds/Annot.hs @@ -0,0 +1,342 @@ + +-- | Utilities for constructing and destructing compound expressions. +-- +-- For the annotated version of the AST. +module DDC.Core.Compounds.Annot + ( module DDC.Type.Compounds + + -- * Annotations + , takeAnnotOfExp + + -- * Lambdas + , xLAMs + , xLams + , makeXLamFlags + , takeXLAMs + , takeXLams + , takeXLamFlags + + -- * Applications + , xApps + , makeXAppsWithAnnots + , takeXApps + , takeXApps1 + , takeXAppsAsList + , takeXAppsWithAnnots + , takeXConApps + , takeXPrimApps + + -- * Lets + , xLets, xLetsAnnot + , splitXLets + , bindsOfLets + , specBindsOfLets + , valwitBindsOfLets + + -- * Patterns + , bindsOfPat + + -- * Alternatives + , takeCtorNameOfAlt + + -- * Witnesses + , wApp + , wApps + , takeXWitness + , takeWAppsAsList + , takePrimWiConApps + + -- * Types + , takeXType + + -- * Data Constructors + , xUnit, dcUnit + , mkDaConAlg + , mkDaConSolid + , takeNameOfDaCon + , typeOfDaCon) +where +import DDC.Type.Compounds +import DDC.Core.Exp +import DDC.Core.Exp.DaCon + + +-- Annotations ---------------------------------------------------------------- +-- | Take the outermost annotation from an expression, +-- or Nothing if this is an `XType` or `XWitness` without an annotation. +takeAnnotOfExp :: Exp a n -> Maybe a +takeAnnotOfExp xx + = case xx of + XVar a _ -> Just a + XCon a _ -> Just a + XLAM a _ _ -> Just a + XLam a _ _ -> Just a + XApp a _ _ -> Just a + XLet a _ _ -> Just a + XCase a _ _ -> Just a + XCast a _ _ -> Just a + XType{} -> Nothing + XWitness{} -> Nothing + + +-- Lambdas --------------------------------------------------------------------- +-- | Make some nested type lambdas. +xLAMs :: a -> [Bind n] -> Exp a n -> Exp a n +xLAMs a bs x + = foldr (XLAM a) x bs + + +-- | Make some nested value or witness lambdas. +xLams :: a -> [Bind n] -> Exp a n -> Exp a n +xLams a bs x + = foldr (XLam a) x bs + + +-- | Split type lambdas from the front of an expression, +-- or `Nothing` if there aren't any. +takeXLAMs :: Exp a n -> Maybe ([Bind n], Exp a n) +takeXLAMs xx + = let go bs (XLAM _ b x) = go (b:bs) x + go bs x = (reverse bs, x) + in case go [] xx of + ([], _) -> Nothing + (bs, body) -> Just (bs, body) + + +-- | Split nested value or witness lambdas from the front of an expression, +-- or `Nothing` if there aren't any. +takeXLams :: Exp a n -> Maybe ([Bind n], Exp a n) +takeXLams xx + = let go bs (XLam _ b x) = go (b:bs) x + go bs x = (reverse bs, x) + in case go [] xx of + ([], _) -> Nothing + (bs, body) -> Just (bs, body) + + +-- | Make some nested lambda abstractions, +-- using a flag to indicate whether the lambda is a +-- level-1 (True), or level-0 (False) binder. +makeXLamFlags :: a -> [(Bool, Bind n)] -> Exp a n -> Exp a n +makeXLamFlags a fbs x + = foldr (\(f, b) x' + -> if f then XLAM a b x' + else XLam a b x') + x fbs + + +-- | Split nested lambdas from the front of an expression, +-- with a flag indicating whether the lambda was a level-1 (True), +-- or level-0 (False) binder. +takeXLamFlags :: Exp a n -> Maybe ([(Bool, Bind n)], Exp a n) +takeXLamFlags xx + = let go bs (XLAM _ b x) = go ((True, b):bs) x + go bs (XLam _ b x) = go ((False, b):bs) x + go bs x = (reverse bs, x) + in case go [] xx of + ([], _) -> Nothing + (bs, body) -> Just (bs, body) + + +-- Applications --------------------------------------------------------------- +-- | Build sequence of value applications. +xApps :: a -> Exp a n -> [Exp a n] -> Exp a n +xApps a t1 ts = foldl (XApp a) t1 ts + + +-- | Build sequence of applications. +-- Similar to `xApps` but also takes list of annotations for +-- the `XApp` constructors. +makeXAppsWithAnnots :: Exp a n -> [(Exp a n, a)] -> Exp a n +makeXAppsWithAnnots f xas + = case xas of + [] -> f + (arg,a ) : as -> makeXAppsWithAnnots (XApp a f arg) as + + +-- | Flatten an application into the function part and its arguments. +-- +-- Returns `Nothing` if there is no outer application. +takeXApps :: Exp a n -> Maybe (Exp a n, [Exp a n]) +takeXApps xx + = case takeXAppsAsList xx of + (x1 : xsArgs) -> Just (x1, xsArgs) + _ -> Nothing + + +-- | Flatten an application into the function part and its arguments. +-- +-- This is like `takeXApps` above, except we know there is at least one argument. +takeXApps1 :: Exp a n -> Exp a n -> (Exp a n, [Exp a n]) +takeXApps1 x1 x2 + = case takeXApps x1 of + Nothing -> (x1, [x2]) + Just (x11, x12s) -> (x11, x12s ++ [x2]) + + +-- | Flatten an application into the function parts and arguments, if any. +takeXAppsAsList :: Exp a n -> [Exp a n] +takeXAppsAsList xx + = case xx of + XApp _ x1 x2 -> takeXAppsAsList x1 ++ [x2] + _ -> [xx] + + +-- | Destruct sequence of applications. +-- Similar to `takeXAppsAsList` but also keeps annotations for later. +takeXAppsWithAnnots :: Exp a n -> (Exp a n, [(Exp a n, a)]) +takeXAppsWithAnnots xx + = case xx of + XApp a f arg + -> let (f', args') = takeXAppsWithAnnots f + in (f', args' ++ [(arg,a)]) + + _ -> (xx, []) + + +-- | Flatten an application of a primop into the variable +-- and its arguments. +-- +-- Returns `Nothing` if the expression isn't a primop application. +takeXPrimApps :: Exp a n -> Maybe (n, [Exp a n]) +takeXPrimApps xx + = case takeXAppsAsList xx of + XVar _ (UPrim p _) : xs -> Just (p, xs) + _ -> Nothing + +-- | Flatten an application of a data constructor into the constructor +-- and its arguments. +-- +-- Returns `Nothing` if the expression isn't a constructor application. +takeXConApps :: Exp a n -> Maybe (DaCon n, [Exp a n]) +takeXConApps xx + = case takeXAppsAsList xx of + XCon _ dc : xs -> Just (dc, xs) + _ -> Nothing + + +-- Lets ----------------------------------------------------------------------- +-- | Wrap some let-bindings around an expression. +xLets :: a -> [Lets a n] -> Exp a n -> Exp a n +xLets a lts x + = foldr (XLet a) x lts + + +-- | Wrap some let-bindings around an expression, with individual annotations. +xLetsAnnot :: [(Lets a n, a)] -> Exp a n -> Exp a n +xLetsAnnot lts x + = foldr (\(l, a) x' -> XLet a l x') x lts + + +-- | Split let-bindings from the front of an expression, if any. +splitXLets :: Exp a n -> ([Lets a n], Exp a n) +splitXLets xx + = case xx of + XLet _ lts x + -> let (lts', x') = splitXLets x + in (lts : lts', x') + + _ -> ([], xx) + +-- | Take the binds of a `Lets`. +-- +-- The level-1 and level-0 binders are returned separately. +bindsOfLets :: Lets a n -> ([Bind n], [Bind n]) +bindsOfLets ll + = case ll of + LLet b _ -> ([], [b]) + LRec bxs -> ([], map fst bxs) + LLetRegions bs bbs -> (bs, bbs) + LWithRegion{} -> ([], []) + + +-- | Like `bindsOfLets` but only take the spec (level-1) binders. +specBindsOfLets :: Lets a n -> [Bind n] +specBindsOfLets ll + = case ll of + LLet _ _ -> [] + LRec _ -> [] + LLetRegions bs _ -> bs + LWithRegion{} -> [] + + +-- | Like `bindsOfLets` but only take the value and witness (level-0) binders. +valwitBindsOfLets :: Lets a n -> [Bind n] +valwitBindsOfLets ll + = case ll of + LLet b _ -> [b] + LRec bxs -> map fst bxs + LLetRegions _ bs -> bs + LWithRegion{} -> [] + + +-- Alternatives --------------------------------------------------------------- +-- | Take the constructor name of an alternative, if there is one. +takeCtorNameOfAlt :: Alt a n -> Maybe n +takeCtorNameOfAlt aa + = case aa of + AAlt (PData dc _) _ -> takeNameOfDaCon dc + _ -> Nothing + + +-- Patterns ------------------------------------------------------------------- +-- | Take the binds of a `Pat`. +bindsOfPat :: Pat n -> [Bind n] +bindsOfPat pp + = case pp of + PDefault -> [] + PData _ bs -> bs + + +-- Witnesses ------------------------------------------------------------------ +-- | Construct a witness application +wApp :: a -> Witness a n -> Witness a n -> Witness a n +wApp = WApp + + +-- | Construct a sequence of witness applications +wApps :: a -> Witness a n -> [Witness a n] -> Witness a n +wApps a = foldl (wApp a) + + +-- | Take the witness from an `XWitness` argument, if any. +takeXWitness :: Exp a n -> Maybe (Witness a n) +takeXWitness xx + = case xx of + XWitness t -> Just t + _ -> Nothing + + +-- | Flatten an application into the function parts and arguments, if any. +takeWAppsAsList :: Witness a n -> [Witness a n] +takeWAppsAsList ww + = case ww of + WApp _ w1 w2 -> takeWAppsAsList w1 ++ [w2] + _ -> [ww] + + +-- | Flatten an application of a witness into the witness constructor +-- name and its arguments. +-- +-- Returns nothing if there is no witness constructor in head position. +takePrimWiConApps :: Witness a n -> Maybe (n, [Witness a n]) +takePrimWiConApps ww + = case takeWAppsAsList ww of + WCon _ wc : args | WiConBound (UPrim n _) _ <- wc + -> Just (n, args) + _ -> Nothing + + +-- Types ---------------------------------------------------------------------- +-- | Take the type from an `XType` argument, if any. +takeXType :: Exp a n -> Maybe (Type n) +takeXType xx + = case xx of + XType t -> Just t + _ -> Nothing + + +-- Units ----------------------------------------------------------------------- +-- | Construct a value of unit type. +xUnit :: a -> Exp a n +xUnit a = XCon a dcUnit diff --git a/DDC/Core/Compounds/Simple.hs b/DDC/Core/Compounds/Simple.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Compounds/Simple.hs @@ -0,0 +1,293 @@ + +-- | Utilities for constructing and destructing compound expressions. +-- +-- For the Simple version of the AST. +module DDC.Core.Compounds.Simple + ( module DDC.Type.Compounds + + -- * Lambdas + , xLAMs + , xLams + , makeXLamFlags + , takeXLAMs + , takeXLams + , takeXLamFlags + + -- * Applications + , xApps + , takeXApps + , takeXApps1 + , takeXAppsAsList + , takeXConApps + , takeXPrimApps + + -- * Lets + , xLets + , splitXLets + , bindsOfLets + , specBindsOfLets + , valwitBindsOfLets + + -- * Patterns + , bindsOfPat + + -- * Alternatives + , takeCtorNameOfAlt + + -- * Witnesses + , wApp + , wApps + , takeXWitness + , takeWAppsAsList + , takePrimWiConApps + + -- * Types + , takeXType + + -- * Data Constructors + , xUnit, dcUnit + , mkDaConAlg + , mkDaConSolid + , takeNameOfDaCon + , typeOfDaCon) +where +import DDC.Type.Exp +import DDC.Core.Exp.Simple +import DDC.Core.Exp.DaCon +import DDC.Type.Compounds + + +-- Lambdas --------------------------------------------------------------------- +-- | Make some nested type lambdas. +xLAMs :: [Bind n] -> Exp a n -> Exp a n +xLAMs bs x + = foldr XLAM x bs + + +-- | Make some nested value or witness lambdas. +xLams :: [Bind n] -> Exp a n -> Exp a n +xLams bs x + = foldr XLam x bs + + +-- | Split type lambdas from the front of an expression, +-- or `Nothing` if there aren't any. +takeXLAMs :: Exp a n -> Maybe ([Bind n], Exp a n) +takeXLAMs xx + = let go bs (XLAM b x) = go (b:bs) x + go bs x = (reverse bs, x) + in case go [] xx of + ([], _) -> Nothing + (bs, body) -> Just (bs, body) + + +-- | Split nested value or witness lambdas from the front of an expression, +-- or `Nothing` if there aren't any. +takeXLams :: Exp a n -> Maybe ([Bind n], Exp a n) +takeXLams xx + = let go bs (XLam b x) = go (b:bs) x + go bs x = (reverse bs, x) + in case go [] xx of + ([], _) -> Nothing + (bs, body) -> Just (bs, body) + + +-- | Make some nested lambda abstractions, +-- using a flag to indicate whether the lambda is a +-- level-1 (True), or level-0 (False) binder. +makeXLamFlags :: [(Bool, Bind n)] -> Exp a n -> Exp a n +makeXLamFlags fbs x + = foldr (\(f, b) x' + -> if f then XLAM b x' + else XLam b x') + x fbs + + +-- | Split nested lambdas from the front of an expression, +-- with a flag indicating whether the lambda was a level-1 (True), +-- or level-0 (False) binder. +takeXLamFlags :: Exp a n -> Maybe ([(Bool, Bind n)], Exp a n) +takeXLamFlags xx + = let go bs (XLAM b x) = go ((True, b):bs) x + go bs (XLam b x) = go ((False, b):bs) x + go bs x = (reverse bs, x) + in case go [] xx of + ([], _) -> Nothing + (bs, body) -> Just (bs, body) + + +-- Applications --------------------------------------------------------------- +-- | Build sequence of value applications. +xApps :: Exp a n -> [Exp a n] -> Exp a n +xApps t1 ts = foldl XApp t1 ts + + +-- | Flatten an application into the function part and its arguments. +-- +-- Returns `Nothing` if there is no outer application. +takeXApps :: Exp a n -> Maybe (Exp a n, [Exp a n]) +takeXApps xx + = case takeXAppsAsList xx of + (x1 : xsArgs) -> Just (x1, xsArgs) + _ -> Nothing + + +-- | Flatten an application into the function part and its arguments. +-- +-- This is like `takeXApps` above, except we know there is at least one argument. +takeXApps1 :: Exp a n -> Exp a n -> (Exp a n, [Exp a n]) +takeXApps1 x1 x2 + = case takeXApps x1 of + Nothing -> (x1, [x2]) + Just (x11, x12s) -> (x11, x12s ++ [x2]) + + +-- | Flatten an application into the function parts and arguments, if any. +takeXAppsAsList :: Exp a n -> [Exp a n] +takeXAppsAsList xx + = case xx of + XApp x1 x2 -> takeXAppsAsList x1 ++ [x2] + _ -> [xx] + + +-- | Flatten an application of a primop into the variable +-- and its arguments. +-- +-- Returns `Nothing` if the expression isn't a primop application. +takeXPrimApps :: Exp a n -> Maybe (n, [Exp a n]) +takeXPrimApps xx + = case takeXAppsAsList xx of + XVar (UPrim p _) : xs -> Just (p, xs) + _ -> Nothing + +-- | Flatten an application of a data constructor into the constructor +-- and its arguments. +-- +-- Returns `Nothing` if the expression isn't a constructor application. +takeXConApps :: Exp a n -> Maybe (DaCon n, [Exp a n]) +takeXConApps xx + = case takeXAppsAsList xx of + XCon dc : xs -> Just (dc, xs) + _ -> Nothing + + +-- Lets ----------------------------------------------------------------------- +-- | Wrap some let-bindings around an expression. +xLets :: [Lets a n] -> Exp a n -> Exp a n +xLets lts x + = foldr XLet x lts + + +-- | Split let-bindings from the front of an expression, if any. +splitXLets :: Exp a n -> ([Lets a n], Exp a n) +splitXLets xx + = case xx of + XLet lts x + -> let (lts', x') = splitXLets x + in (lts : lts', x') + + _ -> ([], xx) + + +-- | Take the binds of a `Lets`. +-- +-- The level-1 and level-0 binders are returned separately. +bindsOfLets :: Lets a n -> ([Bind n], [Bind n]) +bindsOfLets ll + = case ll of + LLet b _ -> ([], [b]) + LRec bxs -> ([], map fst bxs) + LLetRegions bs bbs -> (bs, bbs) + LWithRegion{} -> ([], []) + + +-- | Like `bindsOfLets` but only take the spec (level-1) binders. +specBindsOfLets :: Lets a n -> [Bind n] +specBindsOfLets ll + = case ll of + LLet _ _ -> [] + LRec _ -> [] + LLetRegions bs _ -> bs + LWithRegion{} -> [] + + +-- | Like `bindsOfLets` but only take the value and witness (level-0) binders. +valwitBindsOfLets :: Lets a n -> [Bind n] +valwitBindsOfLets ll + = case ll of + LLet b _ -> [b] + LRec bxs -> map fst bxs + LLetRegions _ bs -> bs + LWithRegion{} -> [] + + +-- Alternatives --------------------------------------------------------------- +-- | Take the constructor name of an alternative, if there is one. +takeCtorNameOfAlt :: Alt a n -> Maybe n +takeCtorNameOfAlt aa + = case aa of + AAlt (PData dc _) _ -> takeNameOfDaCon dc + _ -> Nothing + + +-- Patterns ------------------------------------------------------------------- +-- | Take the binds of a `Pat`. +bindsOfPat :: Pat n -> [Bind n] +bindsOfPat pp + = case pp of + PDefault -> [] + PData _ bs -> bs + + +-- Witnesses ------------------------------------------------------------------ +-- | Construct a witness application +wApp :: Witness a n -> Witness a n -> Witness a n +wApp = WApp + + +-- | Construct a sequence of witness applications +wApps :: Witness a n -> [Witness a n] -> Witness a n +wApps = foldl wApp + + +-- | Take the witness from an `XWitness` argument, if any. +takeXWitness :: Exp a n -> Maybe (Witness a n) +takeXWitness xx + = case xx of + XWitness t -> Just t + _ -> Nothing + + +-- | Flatten an application into the function parts and arguments, if any. +takeWAppsAsList :: Witness a n -> [Witness a n] +takeWAppsAsList ww + = case ww of + WApp w1 w2 -> takeWAppsAsList w1 ++ [w2] + _ -> [ww] + + +-- | Flatten an application of a witness into the witness constructor +-- name and its arguments. +-- +-- Returns nothing if there is no witness constructor in head position. +takePrimWiConApps :: Witness a n -> Maybe (n, [Witness a n]) +takePrimWiConApps ww + = case takeWAppsAsList ww of + WCon wc : args | WiConBound (UPrim n _) _ <- wc + -> Just (n, args) + _ -> Nothing + + +-- Types ---------------------------------------------------------------------- +-- | Take the type from an `XType` argument, if any. +takeXType :: Exp a n -> Maybe (Type n) +takeXType xx + = case xx of + XType t -> Just t + _ -> Nothing + + +-- Units ----------------------------------------------------------------------- +-- | Construct a value of unit type. +xUnit :: Exp a n +xUnit = XCon dcUnit diff --git a/DDC/Core/DaCon.hs b/DDC/Core/DaCon.hs deleted file mode 100644 --- a/DDC/Core/DaCon.hs +++ /dev/null @@ -1,100 +0,0 @@ - -module DDC.Core.DaCon - ( DaCon (..) - , DaConName (..) - - , dcUnit - , mkDaConAlg - , mkDaConSolid - , takeNameOfDaCon - , typeOfDaCon) -where -import DDC.Type.Compounds -import DDC.Type.Exp -import Control.DeepSeq - - -------------------------------------------------------------------------------- --- | Data constructor names. -data DaConName n - -- | The unit data constructor is builtin. - = DaConUnit - - -- | Data constructor name defined by the client. - | DaConNamed n - deriving (Eq, Show) - - -instance NFData n => NFData (DaConName n) where - rnf dcn - = case dcn of - DaConUnit -> () - DaConNamed n -> rnf n - - -------------------------------------------------------------------------------- --- | Data constructors. -data DaCon n - = DaCon - { -- | Name of the data constructor. - daConName :: !(DaConName n) - - -- | Type of the data constructor. - -- The type must be closed. - , daConType :: !(Type n) - - -- | Algebraic constructors can be deconstructed with case-expressions, - -- and must have a data type declaration. - -- - -- Non-algebraic types like 'Float' can't be inspected with - -- case-expressions. - , daConIsAlgebraic :: !Bool } - deriving Show - - -instance NFData n => NFData (DaCon n) where - rnf !dc - = rnf (daConName dc) - `seq` rnf (daConType dc) - `seq` rnf (daConIsAlgebraic dc) - - --- | Take the name of data constructor. -takeNameOfDaCon :: DaCon n -> Maybe n -takeNameOfDaCon dc - = case daConName dc of - DaConUnit -> Nothing - DaConNamed n -> Just n - - --- | Take the type annotation of a data constructor. -typeOfDaCon :: DaCon n -> Type n -typeOfDaCon dc = daConType dc - - --- | The unit data constructor. -dcUnit :: DaCon n -dcUnit = DaCon - { daConName = DaConUnit - , daConType = tUnit - , daConIsAlgebraic = True } - - --- | Make an algebraic data constructor. -mkDaConAlg :: n -> Type n -> DaCon n -mkDaConAlg n t - = DaCon - { daConName = DaConNamed n - , daConType = t - , daConIsAlgebraic = True } - - --- | Make a non-algebraic (solid) constructor. --- These are used for location values in the interpreter, --- and for floating point literals in the main compiler. -mkDaConSolid :: n -> Type n -> DaCon n -mkDaConSolid n t - = DaCon - { daConName = DaConNamed n - , daConType = t - , daConIsAlgebraic = False } diff --git a/DDC/Core/Exp.hs b/DDC/Core/Exp.hs --- a/DDC/Core/Exp.hs +++ b/DDC/Core/Exp.hs @@ -1,25 +1,6 @@ -- | Abstract syntax for the Disciple core language. module DDC.Core.Exp - ( module DDC.Type.Exp - - -- * Computation expressions - , Exp (..) - , DaCon (..) - , DaConName(..) - , Cast (..) - , Lets (..) - , LetMode (..) - , Alt (..) - , Pat (..) - - -- * Witnesses expressions - , Witness (..) - , WiCon (..) - , WbCon (..)) + ( module DDC.Core.Exp.Annot ) where -import DDC.Core.Exp.Base -import DDC.Core.Exp.NFData () -import DDC.Core.DaCon -import DDC.Type.Exp - +import DDC.Core.Exp.Annot diff --git a/DDC/Core/Exp/Annot.hs b/DDC/Core/Exp/Annot.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Exp/Annot.hs @@ -0,0 +1,202 @@ + +-- | Core language AST that includes an annotation on every node of +-- an expression. +-- +-- This is the default representation for Disciple Core, and should be preferred +-- over the 'Simple' version of the AST in most cases. +-- +-- * Local transformations on this AST should propagate the annotations in a way that +-- would make sense if they were source position identifiers that tracked the provenance +-- of each code snippet. If the specific annotations attached to the AST would not make +-- sense after such a transformation, then the client should erase them to @()@ beforehand +-- using the `reannotate` transform. +-- +-- * Global transformations that drastically change the provenance of code snippets should +-- accept an AST with an arbitrary annotation type, but produce one with the annotations +-- set to @()@. +-- +module DDC.Core.Exp.Annot + ( module DDC.Type.Exp + + -- * Expressions + , Exp (..) + , Lets (..) + , Alt (..) + , Pat (..) + , Cast (..) + + -- * Witnesses + , Witness (..) + + -- * Data Constructors + , DaCon (..) + , DaConName (..) + + -- * Witness Constructors + , WiCon (..) + , WbCon (..)) +where +import DDC.Core.Exp.WiCon +import DDC.Core.Exp.DaCon +import DDC.Core.Exp.Pat +import DDC.Type.Exp +import DDC.Type.Sum () +import Control.DeepSeq + + +-- Values --------------------------------------------------------------------- +-- | Well-typed expressions have types of kind `Data`. +data Exp a n + -- | Value variable or primitive operation. + = XVar !a !(Bound n) + + -- | Data constructor or literal. + | XCon !a !(DaCon n) + + -- | Type abstraction (level-1). + | XLAM !a !(Bind n) !(Exp a n) + + -- | Value and Witness abstraction (level-0). + | XLam !a !(Bind n) !(Exp a n) + + -- | Application. + | XApp !a !(Exp a n) !(Exp a n) + + -- | Possibly recursive bindings. + | XLet !a !(Lets a n) !(Exp a n) + + -- | Case branching. + | XCase !a !(Exp a n) ![Alt a n] + + -- | Type cast. + | XCast !a !(Cast a n) !(Exp a n) + + -- | Type can appear as the argument of an application. + | XType !(Type n) + + -- | Witness can appear as the argument of an application. + | XWitness !(Witness a n) + deriving (Show, Eq) + + +-- | Possibly recursive bindings. +data Lets a n + -- | Non-recursive expression binding. + = LLet !(Bind n) !(Exp a n) + + -- | Recursive binding of lambda abstractions. + | LRec ![(Bind n, Exp a n)] + + -- | Bind a local region variable, + -- and witnesses to its properties. + | LLetRegions ![Bind n] ![Bind n] + + -- | Holds a region handle during evaluation. + | LWithRegion !(Bound n) + deriving (Show, Eq) + + +-- | Case alternatives. +data Alt a n + = AAlt !(Pat n) !(Exp a n) + deriving (Show, Eq) + + +-- | Type casts. +data Cast a n + -- | Weaken the effect of an expression. + -- The given effect is added to the effect + -- of the body. + = CastWeakenEffect !(Effect n) + + -- | Weaken the closure of an expression. + -- The closures of these expressions are added to the closure + -- of the body. + | CastWeakenClosure ![Exp a n] + + -- | Purify the effect (action) of an expression. + | CastPurify !(Witness a n) + + -- | Forget about the closure (sharing) of an expression. + | CastForget !(Witness a n) + + -- | Suspend a computation, + -- capturing its effects in the S computation type. + | CastSuspend + + -- | Run a computation, + -- releasing its effects into the environment. + | CastRun + deriving (Show, Eq) + + +-- | When a witness exists in the program it guarantees that a +-- certain property of the program is true. +data Witness a n + -- | Witness variable. + = WVar a !(Bound n) + + -- | Witness constructor. + | WCon a !(WiCon n) + + -- | Witness application. + | WApp a !(Witness a n) !(Witness a n) + + -- | Joining of witnesses. + | WJoin a !(Witness a n) !(Witness a n) + + -- | Type can appear as the argument of an application. + | WType a !(Type n) + deriving (Show, Eq) + + +-- NFData --------------------------------------------------------------------- +instance (NFData a, NFData n) => NFData (Exp a n) where + rnf xx + = case xx of + XVar a u -> rnf a `seq` rnf u + XCon a dc -> rnf a `seq` rnf dc + XLAM a b x -> rnf a `seq` rnf b `seq` rnf x + XLam a b x -> rnf a `seq` rnf b `seq` rnf x + XApp a x1 x2 -> rnf a `seq` rnf x1 `seq` rnf x2 + XLet a lts x -> rnf a `seq` rnf lts `seq` rnf x + XCase a x alts -> rnf a `seq` rnf x `seq` rnf alts + XCast a c x -> rnf a `seq` rnf c `seq` rnf x + XType t -> rnf t + XWitness w -> rnf w + + +instance (NFData a, NFData n) => NFData (Cast a n) where + rnf cc + = case cc of + CastWeakenEffect e -> rnf e + CastWeakenClosure xs -> rnf xs + CastPurify w -> rnf w + CastForget w -> rnf w + CastSuspend -> () + CastRun -> () + + +instance (NFData a, NFData n) => NFData (Lets a n) where + rnf lts + = case lts of + LLet b x -> rnf b `seq` rnf x + LRec bxs -> rnf bxs + LLetRegions bs1 bs2 -> rnf bs1 `seq` rnf bs2 + LWithRegion u -> rnf u + + +instance (NFData a, NFData n) => NFData (Alt a n) where + rnf aa + = case aa of + AAlt w x -> rnf w `seq` rnf x + + +instance (NFData a, NFData n) => NFData (Witness a n) where + rnf ww + = case ww of + WVar a u -> rnf a `seq` rnf u + WCon a c -> rnf a `seq` rnf c + WApp a w1 w2 -> rnf a `seq` rnf w1 `seq` rnf w2 + WJoin a w1 w2 -> rnf a `seq` rnf w1 `seq` rnf w2 + WType a tt -> rnf a `seq` rnf tt diff --git a/DDC/Core/Exp/Base.hs b/DDC/Core/Exp/Base.hs deleted file mode 100644 --- a/DDC/Core/Exp/Base.hs +++ /dev/null @@ -1,186 +0,0 @@ - -module DDC.Core.Exp.Base where -import DDC.Core.DaCon -import DDC.Type.Exp -import DDC.Type.Sum () - - --- Values --------------------------------------------------------------------- --- | Well-typed expressions produce `Data` values when evaluated, --- and their types aways have kind '*' (Data) -data Exp a n - -- | Value variable or primitive operation. - = XVar !a !(Bound n) - - -- | Data constructor or literal. - | XCon !a !(DaCon n) - - -- | Type abstraction (level-1). - | XLAM !a !(Bind n) !(Exp a n) - - -- | Value and Witness abstraction (level-0). - | XLam !a !(Bind n) !(Exp a n) - - -- | Application. - | XApp !a !(Exp a n) !(Exp a n) - - -- | Possibly recursive bindings. - | XLet !a !(Lets a n) !(Exp a n) - - -- | Case branching. - | XCase !a !(Exp a n) ![Alt a n] - - -- | Type cast. - | XCast !a !(Cast a n) !(Exp a n) - - -- | Type can appear as the argument of an application. - | XType !(Type n) - - -- | Witness can appear as the argument of an application. - | XWitness !(Witness n) - deriving (Eq, Show) - -deriving instance Eq n => Eq (DaCon n) - - --- | Type casts. -data Cast a n - -- | Weaken the effect of an expression. - -- The given effect is added to the effect - -- of the body. - = CastWeakenEffect !(Effect n) - - -- | Weaken the closure of an expression. - -- The closures of these expressions are added to the closure - -- of the body. - | CastWeakenClosure ![Exp a n] - - -- | Purify the effect (action) of an expression. - | CastPurify !(Witness n) - - -- | Forget about the closure (sharing) of an expression. - | CastForget !(Witness n) - deriving (Eq, Show) - - --- | Possibly recursive bindings. -data Lets a n - -- | Non-recursive expression binding. - = LLet !(LetMode n) !(Bind n) !(Exp a n) - - -- | Recursive binding of lambda abstractions. - | LRec ![(Bind n, Exp a n)] - - -- | Bind a local region variable, - -- and witnesses to its properties. - | LLetRegions ![Bind n] ![Bind n] - - -- | Holds a region handle during evaluation. - | LWithRegion !(Bound n) - deriving (Eq, Show) - - --- | Describes how a let binding should be evaluated. -data LetMode n - -- | Evaluate binding before substituting the result. - = LetStrict - - -- | Use lazy evaluation. - -- The witness shows that the head region of the bound expression - -- can contain thunks (is lazy), or Nothing if there is no head region. - | LetLazy !(Maybe (Witness n)) - deriving (Eq, Show) - - --- | Case alternatives. -data Alt a n - = AAlt !(Pat n) !(Exp a n) - deriving (Eq, Show) - - --- | Pattern matching. -data Pat n - -- | The default pattern always succeeds. - = PDefault - - -- | Match a data constructor and bind its arguments. - | PData !(DaCon n) ![Bind n] - deriving (Eq, Show) - - --- Witness -------------------------------------------------------------------- --- | When a witness exists in the program it guarantees that a --- certain property of the program is true. -data Witness n - -- | Witness variable. - = WVar !(Bound n) - - -- | Witness constructor. - | WCon !(WiCon n) - - -- | Witness application. - | WApp !(Witness n) !(Witness n) - - -- | Joining of witnesses. - | WJoin !(Witness n) !(Witness n) - - -- | Type can appear as the argument of an application. - | WType !(Type n) - deriving (Eq, Show) - - --- | Witness constructors. -data WiCon n - -- | Witness constructors baked into the language. - = WiConBuiltin !WbCon - - -- | Witness constructors defined in the environment. - -- In the interpreter we use this to hold runtime capabilities. - -- The attached type must be closed. - | WiConBound !(Bound n) !(Type n) - deriving (Eq, Show) - - --- | Built-in witness constructors. --- --- These are used to convert a runtime capability into a witness that --- the corresponding property is true. -data WbCon - -- | (axiom) The pure effect is pure. - -- - -- @pure :: Pure !0@ - = WbConPure - - -- | (axiom) The empty closure is empty. - -- - -- @empty :: Empty $0@ - | WbConEmpty - - -- | Convert a capability guaranteeing that a region is in the global - -- heap, into a witness that a closure using this region is empty. - -- This lets us rely on the garbage collector to reclaim objects - -- in the region. It is needed when we suspend the evaluation of - -- expressions that have a region in their closure, because the - -- type of the returned thunk may not reveal that it references - -- objects in that region. - -- - -- @use :: [r : %]. Global r => Empty (Use r)@ - | WbConUse - - -- | Convert a capability guaranteeing the constancy of a region, into - -- a witness that a read from that region is pure. - -- This lets us suspend applications that read constant objects, - -- because it doesn't matter if the read is delayed, we'll always - -- get the same result. - -- - -- @read :: [r : %]. Const r => Pure (Read r)@ - | WbConRead - - -- | Convert a capability guaranteeing the constancy of a region, into - -- a witness that allocation into that region is pure. - -- This lets us increase the sharing of constant objects, - -- because we can't tell constant objects of the same value apart. - -- - -- @alloc :: [r : %]. Const r => Pure (Alloc r)@ - | WbConAlloc - deriving (Eq, Show) diff --git a/DDC/Core/Exp/DaCon.hs b/DDC/Core/Exp/DaCon.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Exp/DaCon.hs @@ -0,0 +1,101 @@ + +module DDC.Core.Exp.DaCon + ( DaCon (..) + , DaConName (..) + + -- * Compounds + , dcUnit + , mkDaConAlg + , mkDaConSolid + , takeNameOfDaCon + , typeOfDaCon) +where +import DDC.Type.Compounds +import DDC.Type.Exp +import Control.DeepSeq + + +------------------------------------------------------------------------------- +-- | Data constructor names. +data DaConName n + -- | The unit data constructor is builtin. + = DaConUnit + + -- | Data constructor name defined by the client. + | DaConNamed n + deriving (Eq, Show) + + +instance NFData n => NFData (DaConName n) where + rnf dcn + = case dcn of + DaConUnit -> () + DaConNamed n -> rnf n + + +------------------------------------------------------------------------------- +-- | Data constructors. +data DaCon n + = DaCon + { -- | Name of the data constructor. + daConName :: !(DaConName n) + + -- | Type of the data constructor. + -- The type must be closed. + , daConType :: !(Type n) + + -- | Algebraic constructors can be deconstructed with case-expressions, + -- and must have a data type declaration. + -- + -- Non-algebraic types like 'Float' can't be inspected with + -- case-expressions. + , daConIsAlgebraic :: !Bool } + deriving (Show, Eq) + + +instance NFData n => NFData (DaCon n) where + rnf !dc + = rnf (daConName dc) + `seq` rnf (daConType dc) + `seq` rnf (daConIsAlgebraic dc) + + +-- | Take the name of data constructor. +takeNameOfDaCon :: DaCon n -> Maybe n +takeNameOfDaCon dc + = case daConName dc of + DaConUnit -> Nothing + DaConNamed n -> Just n + + +-- | Take the type annotation of a data constructor. +typeOfDaCon :: DaCon n -> Type n +typeOfDaCon dc = daConType dc + + +-- | The unit data constructor. +dcUnit :: DaCon n +dcUnit = DaCon + { daConName = DaConUnit + , daConType = tUnit + , daConIsAlgebraic = True } + + +-- | Make an algebraic data constructor. +mkDaConAlg :: n -> Type n -> DaCon n +mkDaConAlg n t + = DaCon + { daConName = DaConNamed n + , daConType = t + , daConIsAlgebraic = True } + + +-- | Make a non-algebraic (solid) constructor. +-- These are used for location values in the interpreter, +-- and for floating point literals in the main compiler. +mkDaConSolid :: n -> Type n -> DaCon n +mkDaConSolid n t + = DaCon + { daConName = DaConNamed n + , daConType = t + , daConIsAlgebraic = False } diff --git a/DDC/Core/Exp/NFData.hs b/DDC/Core/Exp/NFData.hs deleted file mode 100644 --- a/DDC/Core/Exp/NFData.hs +++ /dev/null @@ -1,82 +0,0 @@ - -module DDC.Core.Exp.NFData where -import DDC.Core.Exp.Base -import Control.DeepSeq - - -instance (NFData a, NFData n) => NFData (Exp a n) where - rnf xx - = case xx of - XVar a u -> rnf a `seq` rnf u - XCon a dc -> rnf a `seq` rnf dc - XLAM a b x -> rnf a `seq` rnf b `seq` rnf x - XLam a b x -> rnf a `seq` rnf b `seq` rnf x - XApp a x1 x2 -> rnf a `seq` rnf x1 `seq` rnf x2 - XLet a lts x -> rnf a `seq` rnf lts `seq` rnf x - XCase a x alts -> rnf a `seq` rnf x `seq` rnf alts - XCast a c x -> rnf a `seq` rnf c `seq` rnf x - XType t -> rnf t - XWitness w -> rnf w - - -instance (NFData a, NFData n) => NFData (Cast a n) where - rnf cc - = case cc of - CastWeakenEffect e -> rnf e - CastWeakenClosure xs -> rnf xs - CastPurify w -> rnf w - CastForget w -> rnf w - - -instance (NFData a, NFData n) => NFData (Lets a n) where - rnf lts - = case lts of - LLet mode b x -> rnf mode `seq` rnf b `seq` rnf x - LRec bxs -> rnf bxs - LLetRegions bs1 bs2 -> rnf bs1 `seq` rnf bs2 - LWithRegion u -> rnf u - - -instance NFData n => NFData (LetMode n) where - rnf mode - = case mode of - LetStrict -> () - LetLazy mw -> rnf mw - - -instance (NFData a, NFData n) => NFData (Alt a n) where - rnf aa - = case aa of - AAlt w x -> rnf w `seq` rnf x - - -instance NFData n => NFData (Pat n) where - rnf pp - = case pp of - PDefault -> () - PData dc bs -> rnf dc `seq` rnf bs - - -instance NFData n => NFData (Witness n) where - rnf ww - = case ww of - WVar u -> rnf u - WCon c -> rnf c - WApp w1 w2 -> rnf w1 `seq` rnf w2 - WJoin w1 w2 -> rnf w1 `seq` rnf w2 - WType tt -> rnf tt - - -instance NFData n => NFData (WiCon n) where - rnf wi - = case wi of - WiConBuiltin wb -> rnf wb - WiConBound u t -> rnf u `seq` rnf t - -instance NFData WbCon - - - - - - diff --git a/DDC/Core/Exp/Pat.hs b/DDC/Core/Exp/Pat.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Exp/Pat.hs @@ -0,0 +1,26 @@ + +module DDC.Core.Exp.Pat + ( Pat (..)) +where +import DDC.Core.Exp.DaCon +import DDC.Type.Exp +import Control.DeepSeq + + +-- | Pattern matching. +data Pat n + -- | The default pattern always succeeds. + = PDefault + + -- | Match a data constructor and bind its arguments. + | PData !(DaCon n) ![Bind n] + deriving (Show, Eq) + + +instance NFData n => NFData (Pat n) where + rnf pp + = case pp of + PDefault -> () + PData dc bs -> rnf dc `seq` rnf bs + + diff --git a/DDC/Core/Exp/Simple.hs b/DDC/Core/Exp/Simple.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Exp/Simple.hs @@ -0,0 +1,202 @@ + +-- | Core language AST with a separate node to hold annotations. +-- +-- This version of the AST is used when generating code where most or all +-- of the annotations would be empty. General purpose transformations should +-- deal with the fully annotated version of the AST instead. +-- +module DDC.Core.Exp.Simple + ( module DDC.Type.Exp + + -- * Expressions + , Exp (..) + , Cast (..) + , Lets (..) + , Alt (..) + , Pat (..) + + -- * Witnesses + , Witness (..) + + -- * Data Constructors + , DaCon (..) + , DaConName (..) + + -- * Witness Constructors + , WiCon (..) + , WbCon (..)) +where +import DDC.Core.Exp.WiCon +import DDC.Core.Exp.DaCon +import DDC.Core.Exp.Pat +import DDC.Type.Exp +import DDC.Type.Sum () +import Control.DeepSeq + + +-- Values --------------------------------------------------------------------- +-- | Well-typed expressions have types of kind `Data`. +data Exp a n + -- | Annotation. + = XAnnot a (Exp a n) + + -- | Value variable or primitive operation. + | XVar !(Bound n) + + -- | Data constructor or literal. + | XCon !(DaCon n) + + -- | Type abstraction (level-1). + | XLAM !(Bind n) !(Exp a n) + + -- | Value and Witness abstraction (level-0). + | XLam !(Bind n) !(Exp a n) + + -- | Application. + | XApp !(Exp a n) !(Exp a n) + + -- | Possibly recursive bindings. + | XLet !(Lets a n) !(Exp a n) + + -- | Case branching. + | XCase !(Exp a n) ![Alt a n] + + -- | Type cast. + | XCast !(Cast a n) !(Exp a n) + + -- | Type can appear as the argument of an application. + | XType !(Type n) + + -- | Witness can appear as the argument of an application. + | XWitness !(Witness a n) + deriving (Show, Eq) + + +-- | Possibly recursive bindings. +data Lets a n + -- | Non-recursive expression binding. + = LLet !(Bind n) !(Exp a n) + + -- | Recursive binding of lambda abstractions. + | LRec ![(Bind n, Exp a n)] + + -- | Bind a local region variable, + -- and witnesses to its properties. + | LLetRegions ![Bind n] ![Bind n] + + -- | Holds a region handle during evaluation. + | LWithRegion !(Bound n) + deriving (Show, Eq) + + +-- | Case alternatives. +data Alt a n + = AAlt !(Pat n) !(Exp a n) + deriving (Show, Eq) + + +-- | When a witness exists in the program it guarantees that a +-- certain property of the program is true. +data Witness a n + = WAnnot a (Witness a n) + + -- | Witness variable. + | WVar !(Bound n) + + -- | Witness constructor. + | WCon !(WiCon n) + + -- | Witness application. + | WApp !(Witness a n) !(Witness a n) + + -- | Joining of witnesses. + | WJoin !(Witness a n) !(Witness a n) + + -- | Type can appear as the argument of an application. + | WType !(Type n) + deriving (Show, Eq) + + +-- | Type casts. +data Cast a n + -- | Weaken the effect of an expression. + -- The given effect is added to the effect + -- of the body. + = CastWeakenEffect !(Effect n) + + -- | Weaken the closure of an expression. + -- The closures of these expressions are added to the closure + -- of the body. + | CastWeakenClosure ![Exp a n] + + -- | Purify the effect (action) of an expression. + | CastPurify !(Witness a n) + + -- | Forget about the closure (sharing) of an expression. + | CastForget !(Witness a n) + + -- | Suspend a computation, + -- capturing its effects in the S computation type. + | CastSuspend + + -- | Run a computation, + -- releasing its effects into the environment. + | CastRun + deriving (Show, Eq) + + + + +-- NFData --------------------------------------------------------------------- +instance (NFData a, NFData n) => NFData (Exp a n) where + rnf xx + = case xx of + XAnnot a x -> rnf a `seq` rnf x + XVar u -> rnf u + XCon dc -> rnf dc + XLAM b x -> rnf b `seq` rnf x + XLam b x -> rnf b `seq` rnf x + XApp x1 x2 -> rnf x1 `seq` rnf x2 + XLet lts x -> rnf lts `seq` rnf x + XCase x alts -> rnf x `seq` rnf alts + XCast c x -> rnf c `seq` rnf x + XType t -> rnf t + XWitness w -> rnf w + + +instance (NFData a, NFData n) => NFData (Cast a n) where + rnf cc + = case cc of + CastWeakenEffect e -> rnf e + CastWeakenClosure xs -> rnf xs + CastPurify w -> rnf w + CastForget w -> rnf w + CastSuspend -> () + CastRun -> () + + +instance (NFData a, NFData n) => NFData (Lets a n) where + rnf lts + = case lts of + LLet b x -> rnf b `seq` rnf x + LRec bxs -> rnf bxs + LLetRegions bs1 bs2 -> rnf bs1 `seq` rnf bs2 + LWithRegion u -> rnf u + + +instance (NFData a, NFData n) => NFData (Alt a n) where + rnf aa + = case aa of + AAlt w x -> rnf w `seq` rnf x + + +instance (NFData a, NFData n) => NFData (Witness a n) where + rnf ww + = case ww of + WAnnot a w -> rnf a `seq` rnf w + WVar u -> rnf u + WCon c -> rnf c + WApp w1 w2 -> rnf w1 `seq` rnf w2 + WJoin w1 w2 -> rnf w1 `seq` rnf w2 + WType t -> rnf t + diff --git a/DDC/Core/Exp/WiCon.hs b/DDC/Core/Exp/WiCon.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Exp/WiCon.hs @@ -0,0 +1,75 @@ + +module DDC.Core.Exp.WiCon + ( WiCon (..) + , WbCon (..)) +where +import DDC.Type.Exp +import DDC.Type.Sum () +import Control.DeepSeq + + +-- | Witness constructors. +data WiCon n + -- | Witness constructors baked into the language. + = WiConBuiltin !WbCon + + -- | Witness constructors defined in the environment. + -- In the interpreter we use this to hold runtime capabilities. + -- The attached type must be closed. + | WiConBound !(Bound n) !(Type n) + deriving (Show, Eq) + + +-- | Built-in witness constructors. +-- +-- These are used to convert a runtime capability into a witness that +-- the corresponding property is true. +data WbCon + -- | (axiom) The pure effect is pure. + -- + -- @pure :: Pure !0@ + = WbConPure + + -- | (axiom) The empty closure is empty. + -- + -- @empty :: Empty $0@ + | WbConEmpty + + -- | Convert a capability guaranteeing that a region is in the global + -- heap, into a witness that a closure using this region is empty. + -- This lets us rely on the garbage collector to reclaim objects + -- in the region. It is needed when we suspend the evaluation of + -- expressions that have a region in their closure, because the + -- type of the returned thunk may not reveal that it references + -- objects in that region. + -- + -- @use :: [r : %]. Global r => Empty (Use r)@ + | WbConUse + + -- | Convert a capability guaranteeing the constancy of a region, into + -- a witness that a read from that region is pure. + -- This lets us suspend applications that read constant objects, + -- because it doesn't matter if the read is delayed, we'll always + -- get the same result. + -- + -- @read :: [r : %]. Const r => Pure (Read r)@ + | WbConRead + + -- | Convert a capability guaranteeing the constancy of a region, into + -- a witness that allocation into that region is pure. + -- This lets us increase the sharing of constant objects, + -- because we can't tell constant objects of the same value apart. + -- + -- @alloc :: [r : %]. Const r => Pure (Alloc r)@ + | WbConAlloc + deriving (Show, Eq) + + +-- NFData --------------------------------------------------------------------- +instance NFData n => NFData (WiCon n) where + rnf wi + = case wi of + WiConBuiltin wb -> rnf wb + WiConBound u t -> rnf u `seq` rnf t + +instance NFData WbCon diff --git a/DDC/Core/Fragment.hs b/DDC/Core/Fragment.hs --- a/DDC/Core/Fragment.hs +++ b/DDC/Core/Fragment.hs @@ -30,7 +30,6 @@ import DDC.Data.Token --- Fragment ------------------------------------------------------------------- -- | Carries all the information we need to work on a particular -- fragment of the Disciple Core language. data Fragment n (err :: * -> *) diff --git a/DDC/Core/Fragment/Compliance.hs b/DDC/Core/Fragment/Compliance.hs --- a/DDC/Core/Fragment/Compliance.hs +++ b/DDC/Core/Fragment/Compliance.hs @@ -26,7 +26,7 @@ => Profile n -- ^ Fragment profile giving the supported -- language features and primitive operators. -> c a n -- ^ The thing to check. - -> Maybe (Error n) + -> Maybe (Error a n) complies profile thing = compliesWithEnvs profile @@ -43,7 +43,7 @@ -> Env.KindEnv n -- ^ Starting kind environment. -> Env.TypeEnv n -- ^ Starting type environment. -> c a n -- ^ The thing to check. - -> Maybe (Error n) + -> Maybe (Error a n) compliesWithEnvs profile kenv tenv thing = let merr = result @@ -69,7 +69,7 @@ -> Env n -- ^ Starting Type environment. -> Context -> c a n - -> CheckM n + -> CheckM a n (Set n, Set n) -- Used type and value names. @@ -186,20 +186,12 @@ , Set.union vUsed1 vUsed2) -- let ---------------------------------- - XLet _ (LLet mode b1 x1) x2 + XLet _ (LLet b1 x1) x2 -> do let tenv' = Env.extend b1 tenv (tUsed1, vUsed1) <- compliesX profile kenv tenv (reset context) x1 (tUsed2, vUsed2) <- compliesX profile kenv tenv' (reset context) x2 vUsed2' <- checkBind profile tenv b1 vUsed2 - -- Check for unsupported lazy bindings. - (case mode of - LetStrict -> return () - LetLazy _ - | has featuresLazyBindings -> return () - | otherwise - -> throw $ ErrorUnsupported LazyBindings) - return ( Set.union tUsed1 tUsed2 , Set.union vUsed1 vUsed2') @@ -275,7 +267,7 @@ -> Env n -- ^ The current environment -> Bind n -- ^ The binder at this site. -> Set n -- ^ Names used under the binder. - -> CheckM n (Set n) -- ^ Names used above the binder. + -> CheckM a n (Set n) -- ^ Names used above the binder. checkBind profile env bb used = let has f = f $ profileFeatures profile @@ -305,7 +297,7 @@ :: Ord n => Profile n -> Env n -> [Bind n] -> Set n - -> CheckM n (Set n) + -> CheckM a n (Set n) checkBinds profile env bs used = case bs of @@ -317,7 +309,7 @@ -- Function ------------------------------------------------------------------- -- | Check the function part of an application. -checkFunction :: Profile n -> Exp a n -> CheckM n () +checkFunction :: Profile n -> Exp a n -> CheckM a n () checkFunction profile xx = let has f = f $ profileFeatures profile ok = return () @@ -367,10 +359,10 @@ -- Monad ---------------------------------------------------------------------- -- | Compliance checking monad. -data CheckM n x - = CheckM (Either (Error n) x) +data CheckM a n x + = CheckM (Either (Error a n) x) -instance Monad (CheckM n) where +instance Monad (CheckM a n) where return x = CheckM (Right x) (>>=) m f = case m of @@ -379,10 +371,10 @@ -- | Throw an error in the monad. -throw :: Error n -> CheckM n x +throw :: Error a n -> CheckM a n x throw e = CheckM $ Left e -- | Take the result from a check monad. -result :: CheckM n x -> Either (Error n) x +result :: CheckM a n x -> Either (Error a n) x result (CheckM r) = r diff --git a/DDC/Core/Fragment/Error.hs b/DDC/Core/Fragment/Error.hs --- a/DDC/Core/Fragment/Error.hs +++ b/DDC/Core/Fragment/Error.hs @@ -8,7 +8,7 @@ -- | Language fragment compliance violations. -data Error n +data Error a n -- | Found an unsupported language feature. = ErrorUnsupported !Feature @@ -30,11 +30,11 @@ | ErrorNakedType !(Type n) -- | Found a naked witness that isn't used as a function argument. - | ErrorNakedWitness !(Witness n) - deriving (Eq, Show) + | ErrorNakedWitness !(Witness a n) + deriving Show -instance (Pretty n, Eq n) => Pretty (Error n) where +instance (Pretty n, Eq n) => Pretty (Error a n) where ppr err = case err of ErrorUnsupported feature diff --git a/DDC/Core/Fragment/Feature.hs b/DDC/Core/Fragment/Feature.hs --- a/DDC/Core/Fragment/Feature.hs +++ b/DDC/Core/Fragment/Feature.hs @@ -7,14 +7,18 @@ -- | Language feature supported by a fragment. data Feature -- Type system features --------------------------- - -- | Assume all functions perform global side effects, - -- and don't generate effect terms in types. - = UntrackedEffects + -- | Track effect type information. + = TrackedEffects - -- | Assume all functions share data invisibly, - -- and don't generate closure terms in types. - | UntrackedClosures + -- | Track closure type information. + | TrackedClosures + -- | Attach latent effects to function types. + | FunctionalEffects + + -- | Attach latent closures to function types. + | FunctionalClosures + -- General features ------------------------------- -- | Partially applied primitive operators. | PartialPrims @@ -30,11 +34,6 @@ -- | Nested function bindings. -- The output of the lambda-lifter should not contain these. | NestedFunctions - - -- | Lazy let-bindings. - -- Turning this off means the runtime system won't need to build - -- suspensions. - | LazyBindings -- | Debruijn binders. -- Most backends will want to use real names, instead of indexed diff --git a/DDC/Core/Fragment/Profile.hs b/DDC/Core/Fragment/Profile.hs --- a/DDC/Core/Fragment/Profile.hs +++ b/DDC/Core/Fragment/Profile.hs @@ -11,7 +11,7 @@ import DDC.Core.Fragment.Feature import DDC.Type.DataDef import DDC.Type.Exp -import DDC.Type.Env (KindEnv, TypeEnv) +import DDC.Type.Env (SuperEnv, KindEnv, TypeEnv) import qualified DDC.Type.Env as Env @@ -28,6 +28,9 @@ -- | Primitive data type declarations. , profilePrimDataDefs :: !(DataDefs n) + -- | Supers of primitive kinds. + , profilePrimSupers :: !(SuperEnv n) + -- | Kinds of primitive types. , profilePrimKinds :: !(KindEnv n) @@ -48,6 +51,7 @@ { profileName = "Zero" , profileFeatures = zeroFeatures , profilePrimDataDefs = emptyDataDefs + , profilePrimSupers = Env.empty , profilePrimKinds = Env.empty , profilePrimTypes = Env.empty , profileTypeIsUnboxed = const False } @@ -56,13 +60,14 @@ -- | A flattened set of features, for easy lookup. data Features = Features - { featuresUntrackedEffects :: Bool - , featuresUntrackedClosures :: Bool + { featuresTrackedEffects :: Bool + , featuresTrackedClosures :: Bool + , featuresFunctionalEffects :: Bool + , featuresFunctionalClosures :: Bool , featuresPartialPrims :: Bool , featuresPartialApplication :: Bool , featuresGeneralApplication :: Bool , featuresNestedFunctions :: Bool - , featuresLazyBindings :: Bool , featuresDebruijnBinders :: Bool , featuresUnboundLevel0Vars :: Bool , featuresUnboxedInstantiation :: Bool @@ -76,13 +81,14 @@ zeroFeatures :: Features zeroFeatures = Features - { featuresUntrackedEffects = False - , featuresUntrackedClosures = False + { featuresTrackedEffects = False + , featuresTrackedClosures = False + , featuresFunctionalEffects = False + , featuresFunctionalClosures = False , featuresPartialPrims = False , featuresPartialApplication = False , featuresGeneralApplication = False , featuresNestedFunctions = False - , featuresLazyBindings = False , featuresDebruijnBinders = False , featuresUnboundLevel0Vars = False , featuresUnboxedInstantiation = False @@ -95,13 +101,14 @@ setFeature :: Feature -> Bool -> Features -> Features setFeature feature val features = case feature of - UntrackedEffects -> features { featuresUntrackedEffects = val } - UntrackedClosures -> features { featuresUntrackedClosures = val } + TrackedEffects -> features { featuresTrackedEffects = val } + TrackedClosures -> features { featuresTrackedClosures = val } + FunctionalEffects -> features { featuresFunctionalEffects = val } + FunctionalClosures -> features { featuresFunctionalClosures = val } PartialPrims -> features { featuresPartialPrims = val } PartialApplication -> features { featuresPartialApplication = val } GeneralApplication -> features { featuresGeneralApplication = val } NestedFunctions -> features { featuresNestedFunctions = val } - LazyBindings -> features { featuresLazyBindings = val } DebruijnBinders -> features { featuresDebruijnBinders = val } UnboundLevel0Vars -> features { featuresUnboundLevel0Vars = val } UnboxedInstantiation -> features { featuresUnboxedInstantiation = val } diff --git a/DDC/Core/Lexer.hs b/DDC/Core/Lexer.hs --- a/DDC/Core/Lexer.hs +++ b/DDC/Core/Lexer.hs @@ -21,6 +21,7 @@ import DDC.Data.SourcePos import DDC.Data.Token import Data.Char +import Data.List -- Module --------------------------------------------------------------------- @@ -86,20 +87,27 @@ c : cs | isDigit c , (body, rest) <- span isLitBody cs - -> tokN (KLit (c:body)) : lexMore (length (c:body)) rest + -> tokN (KLit (c:body)) : lexMore (length (c:body)) rest '-' : c : cs | isDigit c , (body, rest) <- span isLitBody cs - -> tokN (KLit ('-':c:body)) : lexMore (length (c:body)) rest + -> tokN (KLit ('-':c:body)) : lexMore (length (c:body)) rest -- Meta tokens - '{' : '-' : w' -> tokM KCommentBlockStart : lexMore 2 w' - '-' : '}' : w' -> tokM KCommentBlockEnd : lexMore 2 w' - '-' : '-' : w' -> tokM KCommentLineStart : lexMore 2 w' - '\n' : w' -> tokM KNewLine : lexWord (line + 1) 1 w' + -- ISSUE #302: Don't try to lex body of a block comment. + '{' : '-' : w' + -> tokM KCommentBlockStart : lexMore 2 w' + '-' : '}' : w' + -> tokM KCommentBlockEnd : lexMore 2 w' + '-' : '-' : w' + -> let (_junk, w'') = span (/= '\n') w' + in tokM KCommentLineStart : lexMore 2 w'' + + '\n' : w' -> tokM KNewLine : lexWord (line + 1) 1 w' + -- The unit data constructor '(' : ')' : w' -> tokA KDaConUnit : lexMore 2 w' @@ -150,29 +158,28 @@ '-' : w' -> tokA KDash : lexMore 1 w' -- Bottoms - '!' : '0' : w' -> tokA KBotEffect : lexMore 2 w' - '$' : '0' : w' -> tokA KBotClosure : lexMore 2 w' - - -- Sort Constructors - '*' : '*' : w' -> tokA KSortComp : lexMore 2 w' - '@' : '@' : w' -> tokA KSortProp : lexMore 2 w' - - -- Kind Constructors - '*' : w' -> tokA KKindValue : lexMore 1 w' - '%' : w' -> tokA KKindRegion : lexMore 1 w' - '!' : w' -> tokA KKindEffect : lexMore 1 w' - '$' : w' -> tokA KKindClosure : lexMore 1 w' - '@' : w' -> tokA KKindWitness : lexMore 1 w' - + name + | Just w' <- stripPrefix "Pure" name + -> tokA KBotEffect : lexMore 2 w' + + | Just w' <- stripPrefix "Empty" name + -> tokA KBotClosure : lexMore 2 w' -- Named Constructors c : cs | isConStart c , (body, rest) <- span isConBody cs , (body', rest') <- case rest of - '#' : rest' -> (body ++ "#", rest') + '\'' : rest' -> (body ++ "'", rest') + '#' : rest' -> (body ++ "#", rest') _ -> (body, rest) -> let readNamedCon s + | Just socon <- readSoConBuiltin s + = tokA (KSoConBuiltin socon) : lexMore (length s) rest' + + | Just kicon <- readKiConBuiltin s + = tokA (KKiConBuiltin kicon) : lexMore (length s) rest' + | Just twcon <- readTwConBuiltin s = tokA (KTwConBuiltin twcon) : lexMore (length s) rest' @@ -195,13 +202,13 @@ '#' : rest' -> (body ++ "#", rest') _ -> (body, rest) -> let readNamedVar s - | Just t <- lookup s keywords + | Just t <- lookup s keywords = tok t : lexMore (length s) rest' - | Just wc <- readWbConBuiltin s + | Just wc <- readWbConBuiltin s = tokA (KWbConBuiltin wc) : lexMore (length s) rest' - | Just v <- readVar s + | Just v <- readVar s = tokN (KVar v) : lexMore (length s) rest' | otherwise diff --git a/DDC/Core/Lexer/Names.hs b/DDC/Core/Lexer/Names.hs --- a/DDC/Core/Lexer/Names.hs +++ b/DDC/Core/Lexer/Names.hs @@ -4,6 +4,8 @@ keywords -- * Builtin constructors + , readSoConBuiltin + , readKiConBuiltin , readTwConBuiltin , readTcConBuiltin , readWbConBuiltin @@ -49,6 +51,8 @@ , ("case", KA KCase) , ("purify", KA KPurify) , ("forget", KA KForget) + , ("suspend", KA KSuspend) + , ("run", KA KRun) , ("type", KA KType) , ("weakeff", KA KWeakEff) , ("weakclo", KA KWeakClo) @@ -59,7 +63,28 @@ , ("else", KA KElse) ] --- | Read a named `TwCon`. +-- | Read a named sort constructor. +readSoConBuiltin :: String -> Maybe SoCon +readSoConBuiltin ss + = case ss of + "Prop" -> Just SoConProp + "Comp" -> Just SoConComp + _ -> Nothing + + +-- | Read a named kind constructor. +readKiConBuiltin :: String -> Maybe KiCon +readKiConBuiltin ss + = case ss of + "Witness" -> Just KiConWitness + "Data" -> Just KiConData + "Region" -> Just KiConRegion + "Effect" -> Just KiConEffect + "Closure" -> Just KiConClosure + _ -> Nothing + + +-- | Read a named witness type constructor. readTwConBuiltin :: String -> Maybe TwCon readTwConBuiltin ss = case ss of @@ -72,8 +97,8 @@ "Lazy" -> Just TwConLazy "HeadLazy" -> Just TwConHeadLazy "Manifest" -> Just TwConManifest - "Pure" -> Just TwConPure - "Empty" -> Just TwConEmpty + "Purify" -> Just TwConPure + "Emptify" -> Just TwConEmpty "Disjoint" -> Just TwConDisjoint "Distinct" -> Just (TwConDistinct 2) _ -> readTwConWithArity ss @@ -87,12 +112,13 @@ | otherwise = Nothing --- | Read a builtin `TcCon` with a non-symbolic name, +-- | Read a builtin type constructor with a non-symbolic name. -- ie not '->'. readTcConBuiltin :: String -> Maybe TcCon readTcConBuiltin ss = case ss of "Unit" -> Just TcConUnit + "S" -> Just TcConSusp "Read" -> Just TcConRead "HeadRead" -> Just TcConHeadRead "DeepRead" -> Just TcConDeepRead @@ -105,7 +131,7 @@ _ -> Nothing --- | Read a `WbCon`. +-- | Read a witness constructor. readWbConBuiltin :: String -> Maybe WbCon readWbConBuiltin ss = case ss of @@ -147,7 +173,12 @@ -- | Character can be part of a variable body. isVarBody :: Char -> Bool isVarBody c - = isUpper c || isLower c || isDigit c || c == '_' || c == '\'' + = isUpper c + || isLower c + || isDigit c + || c == '_' + || c == '\'' + || c == '$' -- | Read a named, user defined variable. @@ -185,10 +216,13 @@ -- | Charater can be part of a constructor body. isConBody :: Char -> Bool -isConBody c = isUpper c || isLower c || isDigit c || c == '_' +isConBody c + = isUpper c + || isLower c + || isDigit c + || c == '_' - -- | Read a named, user defined `TcCon`. readCon :: String -> Maybe String readCon ss @@ -223,4 +257,5 @@ || c == 'b' || c == 'o' || c == 'x' || c == 'w' || c == 'i' || c == '#' + || c == '\'' diff --git a/DDC/Core/Lexer/Tokens.hs b/DDC/Core/Lexer/Tokens.hs --- a/DDC/Core/Lexer/Tokens.hs +++ b/DDC/Core/Lexer/Tokens.hs @@ -160,13 +160,6 @@ | KBigLambda -- symbolic constructors - | KSortComp - | KSortProp - | KKindValue - | KKindRegion - | KKindEffect - | KKindClosure - | KKindWitness | KArrowTilde | KArrowDash | KArrowDashLeft @@ -196,6 +189,8 @@ | KWeakClo | KPurify | KForget + | KSuspend + | KRun -- sugar keywords | KDo @@ -206,9 +201,12 @@ | KIndex Int -- builtin names ------------ - -- the unit data constructor. - | KDaConUnit + -- sort constructors. + | KSoConBuiltin SoCon + -- kind constructors. + | KKiConBuiltin KiCon + -- witness type constructors. | KTwConBuiltin TwCon @@ -217,6 +215,9 @@ -- other builtin spec constructors. | KTcConBuiltin TcCon + + -- the unit data constructor. + | KDaConUnit deriving (Eq, Show) @@ -262,13 +263,6 @@ KBigLambda -> (Symbol, "/\\") -- symbolic constructors - KSortComp -> (Constructor, "**") - KSortProp -> (Constructor, "@@") - KKindValue -> (Constructor, "*") - KKindRegion -> (Constructor, "%") - KKindEffect -> (Constructor, "!") - KKindClosure -> (Constructor, "$") - KKindWitness -> (Constructor, "@") KArrowTilde -> (Constructor, "~>") KArrowDash -> (Constructor, "->") KArrowDashLeft -> (Constructor, "<-") @@ -298,6 +292,8 @@ KWeakClo -> (Keyword, "weakclo") KPurify -> (Keyword, "purify") KForget -> (Keyword, "forget") + KSuspend -> (Keyword, "suspend") + KRun -> (Keyword, "run") -- sugar keywords KDo -> (Keyword, "do") @@ -308,11 +304,13 @@ KIndex i -> (Index, "^" ++ show i) -- builtin names - KDaConUnit -> (Constructor, "()") + KSoConBuiltin so -> (Constructor, renderPlain $ ppr so) + KKiConBuiltin ki -> (Constructor, renderPlain $ ppr ki) KTwConBuiltin tw -> (Constructor, renderPlain $ ppr tw) KWbConBuiltin wi -> (Constructor, renderPlain $ ppr wi) KTcConBuiltin tc -> (Constructor, renderPlain $ ppr tc) - + KDaConUnit -> (Constructor, "()") + -- TokNamed ------------------------------------------------------------------- -- | A token with a user-defined name. diff --git a/DDC/Core/Load.hs b/DDC/Core/Load.hs --- a/DDC/Core/Load.hs +++ b/DDC/Core/Load.hs @@ -16,6 +16,7 @@ import DDC.Core.Fragment.Profile import DDC.Core.Lexer.Tokens import DDC.Core.Exp +import DDC.Core.Annot.AnT (AnT) import DDC.Type.Transform.SpreadT import DDC.Core.Module import DDC.Base.Pretty @@ -24,6 +25,7 @@ import qualified DDC.Core.Parser as C import qualified DDC.Core.Check as C import qualified DDC.Type.Check as T +import qualified DDC.Type.Env as Env import qualified DDC.Base.Parser as BP import Data.Map.Strict (Map) import System.Directory @@ -34,8 +36,8 @@ = ErrorRead !String | ErrorParser !BP.ParseError | ErrorCheckType !(T.Error n) - | ErrorCheckExp !(C.Error () n) - | ErrorCompliance !(I.Error n) + | ErrorCheckExp !(C.Error BP.SourcePos n) + | ErrorCompliance !(I.Error (C.AnTEC BP.SourcePos n) n) deriving Show @@ -72,7 +74,7 @@ -> (String -> [Token (Tok n)]) -- ^ Function to lex the source file. -> FilePath -- ^ File containing source code. -> IO (Either (Error n) - (Module (C.AnTEC () n) n)) + (Module (C.AnTEC BP.SourcePos n) n)) loadModuleFromFile profile lexSource filePath = do @@ -89,6 +91,7 @@ return $ loadModuleFromTokens profile filePath toks + -- | Parse and type check a core module from a string. loadModuleFromString :: (Eq n, Ord n, Show n, Pretty n) @@ -96,7 +99,8 @@ -> (String -> [Token (Tok n)]) -- ^ Function to lex the source file. -> FilePath -- ^ Path to source file for error messages. -> String -- ^ Program text. - -> Either (Error n) (Module (C.AnTEC () n) n) + -> Either (Error n) + (Module (C.AnTEC BP.SourcePos n) n) loadModuleFromString profile lexSource filePath src = loadModuleFromTokens profile filePath (lexSource src) @@ -108,7 +112,8 @@ => Profile n -- ^ Language fragment profile. -> FilePath -- ^ Path to source file for error messages. -> [Token (Tok n)] -- ^ Source tokens. - -> Either (Error n) (Module (C.AnTEC () n) n) + -> Either (Error n) + (Module (C.AnTEC BP.SourcePos n) n) loadModuleFromTokens profile sourceName toks' = goParse toks' @@ -120,7 +125,9 @@ -- Parse the tokens. goParse toks - = case BP.runTokenParser describeTok sourceName C.pModule toks of + = case BP.runTokenParser describeTok sourceName + (C.pModule (C.contextOfProfile profile)) + toks of Left err -> Left (ErrorParser err) Right mm -> goCheckType (spreadX kenv tenv mm) @@ -149,7 +156,7 @@ -> FilePath -- ^ Path to source file for error messages. -> [Token (Tok n)] -- ^ Source tokens. -> Either (Error n) - (Exp (C.AnTEC () n) n) + (Exp (C.AnTEC BP.SourcePos n) n) loadExp profile modules sourceName toks' = goParse toks' @@ -161,7 +168,9 @@ -- Parse the tokens. goParse toks - = case BP.runTokenParser describeTok sourceName C.pExp toks of + = case BP.runTokenParser describeTok sourceName + (C.pExp (C.contextOfProfile profile)) + toks of Left err -> Left (ErrorParser err) Right t -> goCheckType (spreadX kenv tenv t) @@ -191,18 +200,18 @@ loadType profile sourceName toks' = goParse toks' - where defs = profilePrimDataDefs profile - kenv = profilePrimKinds profile - + where -- Parse the tokens. goParse toks - = case BP.runTokenParser describeTok sourceName C.pType toks of + = case BP.runTokenParser describeTok sourceName + (C.pType (C.contextOfProfile profile)) + toks of Left err -> Left (ErrorParser err) - Right t -> goCheckType (spreadT kenv t) + Right t -> goCheckType (spreadT (profilePrimKinds profile) t) -- Check the kind of the type. goCheckType t - = case T.checkType defs kenv t of + = case T.checkType (T.configOfProfile profile) Env.empty t of Left err -> Left (ErrorCheckType err) Right k -> Right (t, k) @@ -217,7 +226,7 @@ -> FilePath -- ^ Path to source file for error messages. -> [Token (Tok n)] -- ^ Source tokens. -> Either (Error n) - (Witness n, Type n) + (Witness (AnT BP.SourcePos n) n, Type n) loadWitness profile sourceName toks' = goParse toks' @@ -228,13 +237,15 @@ -- Parse the tokens. goParse toks - = case BP.runTokenParser describeTok sourceName C.pWitness toks of + = case BP.runTokenParser describeTok sourceName + (C.pWitness (C.contextOfProfile profile)) + toks of Left err -> Left (ErrorParser err) Right t -> goCheckType (spreadX kenv tenv t) -- Check the kind of the type. goCheckType w = case C.checkWitness config kenv tenv w of - Left err -> Left (ErrorCheckExp err) - Right k -> Right (w, k) + Left err -> Left (ErrorCheckExp err) + Right (w', t) -> Right (w', t) diff --git a/DDC/Core/Parser.hs b/DDC/Core/Parser.hs --- a/DDC/Core/Parser.hs +++ b/DDC/Core/Parser.hs @@ -1,6 +1,8 @@ -- | Core language parser. module DDC.Core.Parser ( Parser + , Context (..) + , contextOfProfile -- * Modules , pModule @@ -36,9 +38,9 @@ where import DDC.Core.Parser.Base +import DDC.Core.Parser.Context import DDC.Core.Parser.Witness import DDC.Core.Parser.Type import DDC.Core.Parser.Exp import DDC.Core.Parser.Module - diff --git a/DDC/Core/Parser/Base.hs b/DDC/Core/Parser/Base.hs --- a/DDC/Core/Parser/Base.hs +++ b/DDC/Core/Parser/Base.hs @@ -1,22 +1,22 @@ module DDC.Core.Parser.Base ( Parser - , pWbCon , pModuleName , pQualName , pName - , pCon - , pLit - , pIndex - , pVar - , pTok - , pTokAs) + , pWbCon, pWbConSP + , pCon, pConSP + , pLit, pLitSP + , pIndex, pIndexSP + , pVar, pVarSP + , pTok, pTokSP + , pTokAs, pTokAsSP) where import DDC.Base.Pretty import DDC.Core.Module import DDC.Core.Exp import DDC.Core.Lexer.Tokens -import DDC.Base.Parser (()) +import DDC.Base.Parser ((), SourcePos) import qualified DDC.Base.Parser as P @@ -25,13 +25,6 @@ = P.Parser (Tok n) a --- | Parse a builtin named `WiCon` -pWbCon :: Parser n WbCon -pWbCon = P.pTokMaybe f - where f (KA (KWbConBuiltin wb)) = Just wb - f _ = Nothing - - -- | Parse a module name. -- --- ISSUE #273: Handle hierarchical module names. @@ -57,13 +50,34 @@ pName = P.choice [pCon, pVar] +-- | Parse a builtin named `WbCon` +pWbCon :: Parser n WbCon +pWbCon = P.pTokMaybe f + where f (KA (KWbConBuiltin wb)) = Just wb + f _ = Nothing + + +-- | Parse a builtin named `WbCon` +pWbConSP :: Parser n (WbCon, SourcePos) +pWbConSP = P.pTokMaybeSP f + where f (KA (KWbConBuiltin wb)) = Just wb + f _ = Nothing + + -- | Parse a constructor name. -pCon :: Parser n n +pCon :: Parser n n pCon = P.pTokMaybe f where f (KN (KCon n)) = Just n f _ = Nothing +-- | Parse a constructor name. +pConSP :: Parser n (n, SourcePos) +pConSP = P.pTokMaybeSP f + where f (KN (KCon n)) = Just n + f _ = Nothing + + -- | Parse a literal pLit :: Parser n n pLit = P.pTokMaybe f @@ -71,6 +85,13 @@ f _ = Nothing +-- | Parse a literal, with source position. +pLitSP :: Parser n (n, SourcePos) +pLitSP = P.pTokMaybeSP f + where f (KN (KLit n)) = Just n + f _ = Nothing + + -- | Parse a variable. pVar :: Parser n n pVar = P.pTokMaybe f @@ -79,6 +100,14 @@ f _ = Nothing +-- | Parse a variable, with source position. +pVarSP :: Parser n (n, SourcePos) +pVarSP = P.pTokMaybeSP f + "a variable" + where f (KN (KVar n)) = Just n + f _ = Nothing + + -- | Parse a deBruijn index pIndex :: Parser n Int pIndex = P.pTokMaybe f @@ -87,12 +116,29 @@ f _ = Nothing +-- | Parse a deBruijn index, with source position. +pIndexSP :: Parser n (Int, SourcePos) +pIndexSP = P.pTokMaybeSP f + "an index" + where f (KA (KIndex i)) = Just i + f _ = Nothing + + -- | Parse an atomic token. pTok :: TokAtom -> Parser n () pTok k = P.pTok (KA k) +-- | Parse an atomic token, yielding its source position. +pTokSP :: TokAtom -> Parser n SourcePos +pTokSP k = P.pTokSP (KA k) + + -- | Parse an atomic token and return some value. pTokAs :: TokAtom -> a -> Parser n a pTokAs k x = P.pTokAs (KA k) x + +-- | Parse an atomic token and return source position and value. +pTokAsSP :: TokAtom -> a -> Parser n (a, SourcePos) +pTokAsSP k x = P.pTokAsSP (KA k) x diff --git a/DDC/Core/Parser/Context.hs b/DDC/Core/Parser/Context.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Parser/Context.hs @@ -0,0 +1,34 @@ + +module DDC.Core.Parser.Context + ( Context (..) + , contextOfProfile) +where +import DDC.Core.Fragment + + +-- | Configuration and information from the context. +-- Used for context sensitive parsing. +data Context + = Context + { contextTrackedEffects :: Bool + , contextTrackedClosures :: Bool + , contextFunctionalEffects :: Bool + , contextFunctionalClosures :: Bool } + + +-- | Slurp an initital Context from a Profile +contextOfProfile :: Profile n -> Context +contextOfProfile profile + = Context + { contextTrackedEffects = featuresTrackedEffects + $ profileFeatures profile + + , contextTrackedClosures = featuresTrackedClosures + $ profileFeatures profile + + , contextFunctionalEffects = featuresFunctionalEffects + $ profileFeatures profile + + , contextFunctionalClosures = featuresFunctionalClosures + $ profileFeatures profile + } diff --git a/DDC/Core/Parser/Exp.hs b/DDC/Core/Parser/Exp.hs --- a/DDC/Core/Parser/Exp.hs +++ b/DDC/Core/Parser/Exp.hs @@ -3,8 +3,8 @@ module DDC.Core.Parser.Exp ( pExp , pExpApp - , pExpAtom - , pLets + , pExpAtom, pExpAtomSP + , pLetsSP , pType , pTypeApp , pTypeAtom) @@ -13,10 +13,11 @@ import DDC.Core.Parser.Witness import DDC.Core.Parser.Param import DDC.Core.Parser.Type +import DDC.Core.Parser.Context import DDC.Core.Parser.Base import DDC.Core.Lexer.Tokens import DDC.Core.Compounds -import DDC.Base.Parser (()) +import DDC.Base.Parser ((), SourcePos) import qualified DDC.Base.Parser as P import qualified DDC.Type.Compounds as T import Control.Monad.Error @@ -24,62 +25,62 @@ -- Expressions ---------------------------------------------------------------- -- | Parse a core language expression. -pExp :: Ord n => Parser n (Exp () n) -pExp +pExp :: Ord n => Context -> Parser n (Exp SourcePos n) +pExp c = P.choice -- Level-0 lambda abstractions -- \(x1 x2 ... : TYPE) (y1 y2 ... : TYPE) ... . EXP - [ do pTok KBackSlash + [ do sp <- pTokSP KBackSlash bs <- liftM concat $ P.many1 $ do pTok KRoundBra bs' <- P.many1 pBinder pTok KColon - t <- pType + t <- pType c pTok KRoundKet return (map (\b -> T.makeBindFromBinder b t) bs') pTok KDot - xBody <- pExp - return $ foldr (XLam ()) xBody bs + xBody <- pExp c + return $ foldr (XLam sp) xBody bs -- Level-1 lambda abstractions. -- /\(x1 x2 ... : TYPE) (y1 y2 ... : TYPE) ... . EXP - , do pTok KBigLambda + , do sp <- pTokSP KBigLambda bs <- liftM concat $ P.many1 $ do pTok KRoundBra bs' <- P.many1 pBinder pTok KColon - t <- pType + t <- pType c pTok KRoundKet return (map (\b -> T.makeBindFromBinder b t) bs') pTok KDot - xBody <- pExp - return $ foldr (XLAM ()) xBody bs + xBody <- pExp c + return $ foldr (XLAM sp) xBody bs -- let expression - , do lts <- pLets + , do (lts, sp) <- pLetsSP c pTok KIn - x2 <- pExp - return $ XLet () lts x2 + x2 <- pExp c + return $ XLet sp lts x2 -- do { STMTS } -- Sugar for a let-expression. , do pTok KDo pTok KBraceBra - xx <- pStmts + xx <- pStmts c pTok KBraceKet return $ xx -- withregion CON in EXP - , do pTok KWithRegion + , do sp <- pTokSP KWithRegion u <- P.choice [ do n <- pVar return $ UName n @@ -87,87 +88,98 @@ , do n <- pCon return $ UPrim n kRegion] pTok KIn - x <- pExp - return $ XLet () (LWithRegion u) x + x <- pExp c + return $ XLet sp (LWithRegion u) x -- case EXP of { ALTS } - , do pTok KCase - x <- pExp + , do sp <- pTokSP KCase + x <- pExp c pTok KOf pTok KBraceBra - alts <- P.sepEndBy1 pAlt (pTok KSemiColon) + alts <- P.sepEndBy1 (pAlt c) (pTok KSemiColon) pTok KBraceKet - return $ XCase () x alts + return $ XCase sp x alts -- match PAT <- EXP else EXP in EXP -- Sugar for a case-expression. - , do pTok KMatch - p <- pPat + , do sp <- pTokSP KMatch + p <- pPat c pTok KArrowDashLeft - x1 <- pExp + x1 <- pExp c pTok KElse - x2 <- pExp + x2 <- pExp c pTok KIn - x3 <- pExp - return $ XCase () x1 [AAlt p x3, AAlt PDefault x2] + x3 <- pExp c + return $ XCase sp x1 [AAlt p x3, AAlt PDefault x2] -- weakeff [TYPE] in EXP - , do pTok KWeakEff + , do sp <- pTokSP KWeakEff pTok KSquareBra - t <- pType + t <- pType c pTok KSquareKet pTok KIn - x <- pExp - return $ XCast () (CastWeakenEffect t) x + x <- pExp c + return $ XCast sp (CastWeakenEffect t) x -- weakclo {EXP;+} in EXP - , do pTok KWeakClo + , do sp <- pTokSP KWeakClo pTok KBraceBra - xs <- liftM concat $ P.sepEndBy1 pArgs (pTok KSemiColon) + xs <- liftM (map fst . concat) + $ P.sepEndBy1 (pArgSPs c) (pTok KSemiColon) pTok KBraceKet pTok KIn - x <- pExp - return $ XCast () (CastWeakenClosure xs) x + x <- pExp c + return $ XCast sp (CastWeakenClosure xs) x -- purify in EXP - , do pTok KPurify + , do sp <- pTokSP KPurify pTok KAngleBra - w <- pWitness + w <- pWitness c pTok KAngleKet pTok KIn - x <- pExp - return $ XCast () (CastPurify w) x + x <- pExp c + return $ XCast sp (CastPurify w) x -- forget in EXP - , do pTok KForget + , do sp <- pTokSP KForget pTok KAngleBra - w <- pWitness + w <- pWitness c pTok KAngleKet pTok KIn - x <- pExp - return $ XCast () (CastForget w) x + x <- pExp c + return $ XCast sp (CastForget w) x + -- suspend EXP + , do sp <- pTokSP KSuspend + x <- pExp c + return $ XCast sp CastSuspend x + + -- run EXP + , do sp <- pTokSP KRun + x <- pExp c + return $ XCast sp CastRun x + -- APP - , do pExpApp + , do pExpApp c ] "an expression" -- Applications. -pExpApp :: Ord n => Parser n (Exp () n) -pExpApp - = do x1 <- pExpAtom +pExpApp :: Ord n => Context -> Parser n (Exp SourcePos n) +pExpApp c + = do (x1, _) <- pExpAtomSP c P.choice - [ do xs <- liftM concat $ P.many1 pArgs - return $ foldl (XApp ()) x1 xs + [ do xs <- liftM concat $ P.many1 (pArgSPs c) + return $ foldl (\x (x', sp) -> XApp sp x x') x1 xs , return x1] @@ -175,75 +187,87 @@ -- Comp, Witness or Spec arguments. -pArgs :: Ord n => Parser n [Exp () n] -pArgs +pArgSPs :: Ord n => Context -> Parser n [(Exp SourcePos n, SourcePos)] +pArgSPs c = P.choice -- [TYPE] - [ do pTok KSquareBra - t <- pType + [ do sp <- pTokSP KSquareBra + t <- pType c pTok KSquareKet - return [XType t] + return [(XType t, sp)] -- [: TYPE0 TYPE0 ... :] - , do pTok KSquareColonBra - ts <- P.many1 pTypeAtom + , do sp <- pTokSP KSquareColonBra + ts <- P.many1 (pTypeAtom c) pTok KSquareColonKet - return $ map XType ts + return [(XType t, sp) | t <- ts] -- - , do pTok KAngleBra - w <- pWitness + , do sp <- pTokSP KAngleBra + w <- pWitness c pTok KAngleKet - return [XWitness w] + return [(XWitness w, sp)] -- <: WITNESS0 WITNESS0 ... :> - , do pTok KAngleColonBra - ws <- P.many1 pWitnessAtom + , do sp <- pTokSP KAngleColonBra + ws <- P.many1 (pWitnessAtom c) pTok KAngleColonKet - return $ map XWitness ws + return [(XWitness w, sp) | w <- ws] -- EXP0 - , do x <- pExpAtom - return [x] + , do (x, sp) <- pExpAtomSP c + return [(x, sp)] ] "a type, witness or expression argument" -- | Parse a variable, constructor or parenthesised expression. -pExpAtom :: Ord n => Parser n (Exp () n) -pExpAtom +pExpAtom :: Ord n => Context -> Parser n (Exp SourcePos n) +pExpAtom c + = do (x, _) <- pExpAtomSP c + return x + + +-- | Parse a variable, constructor or parenthesised expression, +-- also returning source position. +pExpAtomSP + :: Ord n + => Context + -> Parser n (Exp SourcePos n, SourcePos) + +pExpAtomSP c = P.choice -- (EXP2) - [ do pTok KRoundBra - t <- pExp + [ do sp <- pTokSP KRoundBra + t <- pExp c pTok KRoundKet - return $ t + return (t, sp) -- The unit data constructor. - , do pTok KDaConUnit - return $ XCon () dcUnit + , do sp <- pTokSP KDaConUnit + return (XCon sp dcUnit, sp) -- Named algebraic constructors. -- We just fill-in the type with tBot for now, and leave it to -- the spreader to attach the real type. - , do con <- pCon - return $ XCon () (mkDaConAlg con (T.tBot T.kData)) + , do (con, sp) <- pConSP + return (XCon sp (mkDaConAlg con (T.tBot T.kData)), sp) -- Literals. -- We just fill-in the type with tBot for now, and leave it to -- the spreader to attach the real type. -- We also set the literal as being algebraic, which may not be -- true (as for Floats). The spreader also needs to fix this. - , do lit <- pLit - return $ XCon () (mkDaConAlg lit (T.tBot T.kData)) + , do (lit, sp) <- pLitSP + return (XCon sp (mkDaConAlg lit (T.tBot T.kData)), sp) -- Debruijn indices - , do i <- pIndex - return $ XVar () (UIx i) + , do (i, sp) <- pIndexSP + return (XVar sp (UIx i), sp) -- Variables - , do var <- pVar - return $ XVar () (UName var) + , do (var, sp) <- pVarSP + return (XVar sp (UName var), sp) ] "a variable, constructor, or parenthesised type" @@ -251,17 +275,18 @@ -- Alternatives --------------------------------------------------------------- -- Case alternatives. -pAlt :: Ord n => Parser n (Alt () n) -pAlt - = do p <- pPat +pAlt :: Ord n => Context -> Parser n (Alt SourcePos n) +pAlt c + = do p <- pPat c pTok KArrowDash - x <- pExp + x <- pExp c return $ AAlt p x -- Patterns. -pPat :: Ord n => Parser n (Pat n) -pPat +pPat :: Ord n + => Context -> Parser n (Pat n) +pPat c = P.choice [ -- Wildcard do pTok KUnderscore @@ -277,14 +302,16 @@ -- CON BIND BIND ... , do nCon <- pCon - bs <- P.many pBindPat + bs <- P.many (pBindPat c) return $ PData (mkDaConAlg nCon (T.tBot T.kData)) bs] -- Binds in patterns can have no type annotation, -- or can have an annotation if the whole thing is in parens. -pBindPat :: Ord n => Parser n (Bind n) pBindPat + :: Ord n + => Context -> Parser n (Bind n) +pBindPat c = P.choice -- Plain binder. [ do b <- pBinder @@ -294,60 +321,65 @@ , do pTok KRoundBra b <- pBinder pTok KColon - t <- pType + t <- pType c pTok KRoundKet return $ T.makeBindFromBinder b t ] -- Bindings ------------------------------------------------------------------- -pLets :: Ord n => Parser n (Lets () n) -pLets +pLetsSP :: Ord n + => Context -> Parser n (Lets SourcePos n, SourcePos) +pLetsSP c = P.choice [ -- non-recursive let. - do pTok KLet - (mode1, b1, x1) <- pLetBinding - return $ LLet mode1 b1 x1 + do sp <- pTokSP KLet + (b1, x1) <- pLetBinding c + return (LLet b1 x1, sp) -- recursive let. - , do pTok KLetRec + , do sp <- pTokSP KLetRec P.choice -- Multiple bindings in braces [ do pTok KBraceBra - lets <- P.sepEndBy1 pLetRecBinding (pTok KSemiColon) + lets <- P.sepEndBy1 (pLetRecBinding c) (pTok KSemiColon) pTok KBraceKet - return $ LRec lets + return (LRec lets, sp) -- A single binding without braces. - , do ll <- pLetRecBinding - return $ LRec [ll] + , do ll <- pLetRecBinding c + return (LRec [ll], sp) ] -- Local region binding. -- letregions [BINDER] with { BINDER : TYPE ... } in EXP -- letregions [BINDER] in EXP - , do pTok KLetRegions + , do sp <- pTokSP KLetRegions brs <- P.manyTill pBinder (P.try $ P.lookAhead $ P.choice [pTok KIn, pTok KWith]) let bs = map (flip T.makeBindFromBinder T.kRegion) brs - pLetWits bs + r <- pLetWits c bs + return (r, sp) - , do pTok KLetRegion + , do sp <- pTokSP KLetRegion br <- pBinder let b = T.makeBindFromBinder br T.kRegion - pLetWits [b] + r <- pLetWits c [b] + return (r, sp) ] -pLetWits :: Ord n => [Bind n] -> Parser n (Lets () n) -pLetWits bs +pLetWits :: Ord n + => Context -> [Bind n] -> Parser n (Lets SourcePos n) + +pLetWits c bs = P.choice [ do pTok KWith pTok KBraceBra wits <- P.sepBy (do b <- pBinder pTok KColon - t <- pTypeApp + t <- pTypeApp c return $ T.makeBindFromBinder b t) (pTok KSemiColon) pTok KBraceKet @@ -358,100 +390,82 @@ -- | A binding for let expression. -pLetBinding :: Ord n => Parser n (LetMode n, Bind n, Exp () n) pLetBinding + :: Ord n + => Context + -> Parser n ( Bind n + , Exp SourcePos n) +pLetBinding c = do b <- pBinder P.choice [ do -- Binding with full type signature. -- BINDER : TYPE = EXP pTok KColon - t <- pType - mode <- pLetMode + t <- pType c pTok KEquals - xBody <- pExp + xBody <- pExp c - return $ (mode, T.makeBindFromBinder b t, xBody) + return $ (T.makeBindFromBinder b t, xBody) , do -- Non-function binding with no type signature. -- This form can't be used with letrec as we can't use it -- to build the full type sig for the let-bound variable. -- BINDER = EXP - mode <- pLetMode pTok KEquals - xBody <- pExp + xBody <- pExp c let t = T.tBot T.kData - return $ (mode, T.makeBindFromBinder b t, xBody) + return $ (T.makeBindFromBinder b t, xBody) , do -- Binding using function syntax. ps <- liftM concat - $ P.many pBindParamSpec + $ P.many (pBindParamSpec c) P.choice [ do -- Function syntax with a return type. -- We can make the full type sig for the let-bound variable. -- BINDER PARAM1 PARAM2 .. PARAMN : TYPE = EXP pTok KColon - tBody <- pType - mode <- pLetMode - pTok KEquals - xBody <- pExp + tBody <- pType c + sp <- pTokSP KEquals + xBody <- pExp c - let x = expOfParams () ps xBody - let t = funTypeOfParams ps tBody - return (mode, T.makeBindFromBinder b t, x) + let x = expOfParams sp ps xBody + let t = funTypeOfParams c ps tBody + return (T.makeBindFromBinder b t, x) -- Function syntax with no return type. -- We can't make the type sig for the let-bound variable, -- but we can create lambda abstractions with the given -- parameter types. -- BINDER PARAM1 PARAM2 .. PARAMN = EXP - , do mode <- pLetMode - pTok KEquals - xBody <- pExp + , do sp <- pTokSP KEquals + xBody <- pExp c - let x = expOfParams () ps xBody + let x = expOfParams sp ps xBody let t = T.tBot T.kData - return (mode, T.makeBindFromBinder b t, x) ] + return (T.makeBindFromBinder b t, x) ] ] --- | Parse a let mode specifier. --- Only allow the lazy specifier with non-recursive bindings. --- We don't support value recursion, so the right of all recursive --- bindings must be explicit lambda abstractions anyway, so there's --- no point suspending them. -pLetMode :: Ord n => Parser n (LetMode n) -pLetMode - = do P.choice - -- lazy - [ do pTok KLazy - - P.choice - [ do pTok KAngleBra - w <- pWitness - pTok KAngleKet - return $ LetLazy (Just w) - - , do return $ LetLazy Nothing ] - - , do return $ LetStrict ] - - -- | Letrec bindings must have a full type signature, -- or use function syntax with a return type so that we can make one. -pLetRecBinding :: Ord n => Parser n (Bind n, Exp () n) pLetRecBinding + :: Ord n + => Context + -> Parser n (Bind n, Exp SourcePos n) + +pLetRecBinding c = do b <- pBinder P.choice [ do -- Binding with full type signature. -- BINDER : TYPE = EXP pTok KColon - t <- pType + t <- pType c pTok KEquals - xBody <- pExp + xBody <- pExp c return $ (T.makeBindFromBinder b t, xBody) @@ -459,29 +473,29 @@ , do -- Binding using function syntax. -- BINDER PARAM1 PARAM2 .. PARAMN : TYPE = EXP ps <- liftM concat - $ P.many pBindParamSpec + $ P.many (pBindParamSpec c) pTok KColon - tBody <- pType - let t = funTypeOfParams ps tBody + tBody <- pType c + let t = funTypeOfParams c ps tBody - pTok KEquals - xBody <- pExp - let x = expOfParams () ps xBody + sp <- pTokSP KEquals + xBody <- pExp c + let x = expOfParams sp ps xBody return (T.makeBindFromBinder b t, x) ] -- Statements ----------------------------------------------------------------- data Stmt n - = StmtBind (Bind n) (Exp () n) - | StmtMatch (Pat n) (Exp () n) (Exp () n) - | StmtNone (Exp () n) + = StmtBind SourcePos (Bind n) (Exp SourcePos n) + | StmtMatch SourcePos (Pat n) (Exp SourcePos n) (Exp SourcePos n) + | StmtNone SourcePos (Exp SourcePos n) -- | Parse a single statement. -pStmt :: Ord n => Parser n (Stmt n) -pStmt +pStmt :: Ord n => Context -> Parser n (Stmt n) +pStmt c = P.choice [ -- BINDER = EXP ; -- We need the 'try' because a VARIABLE binders can also be parsed @@ -489,57 +503,62 @@ -- P.try $ do br <- pBinder - pTok KEquals - x1 <- pExp + sp <- pTokSP KEquals + x1 <- pExp c let t = T.tBot T.kData let b = T.makeBindFromBinder br t - return $ StmtBind b x1 + return $ StmtBind sp b x1 -- PAT <- EXP else EXP; -- Sugar for a case-expression. -- We need the 'try' because the PAT can also be parsed -- as a function name in a non-binding statement. , P.try $ - do p <- pPat - pTok KArrowDashLeft - x1 <- pExp + do p <- pPat c + sp <- pTokSP KArrowDashLeft + x1 <- pExp c pTok KElse - x2 <- pExp - return $ StmtMatch p x1 x2 + x2 <- pExp c + return $ StmtMatch sp p x1 x2 -- EXP - , do x <- pExp - return $ StmtNone x + , do x <- pExp c + + -- This should always succeed because pExp doesn't + -- parse plain types or witnesses + let Just sp = takeAnnotOfExp x + + return $ StmtNone sp x ] -- | Parse some statements. -pStmts :: Ord n => Parser n (Exp () n) -pStmts - = do stmts <- P.sepEndBy1 pStmt (pTok KSemiColon) +pStmts :: Ord n => Context -> Parser n (Exp SourcePos n) +pStmts c + = do stmts <- P.sepEndBy1 (pStmt c) (pTok KSemiColon) case makeStmts stmts of Nothing -> P.unexpected "do-block must end with a statement" Just x -> return x -- | Make an expression from some statements. -makeStmts :: [Stmt n] -> Maybe (Exp () n) +makeStmts :: [Stmt n] -> Maybe (Exp SourcePos n) makeStmts ss = case ss of - [StmtNone x] + [StmtNone _ x] -> Just x - StmtNone x1 : rest + StmtNone sp x1 : rest | Just x2 <- makeStmts rest - -> Just $ XLet () (LLet LetStrict (BNone (T.tBot T.kData)) x1) x2 + -> Just $ XLet sp (LLet (BNone (T.tBot T.kData)) x1) x2 - StmtBind b x1 : rest + StmtBind sp b x1 : rest | Just x2 <- makeStmts rest - -> Just $ XLet () (LLet LetStrict b x1) x2 + -> Just $ XLet sp (LLet b x1) x2 - StmtMatch p x1 x2 : rest + StmtMatch sp p x1 x2 : rest | Just x3 <- makeStmts rest - -> Just $ XCase () x1 + -> Just $ XCase sp x1 [ AAlt p x3 , AAlt PDefault x2] diff --git a/DDC/Core/Parser/Module.hs b/DDC/Core/Parser/Module.hs --- a/DDC/Core/Parser/Module.hs +++ b/DDC/Core/Parser/Module.hs @@ -6,6 +6,7 @@ import DDC.Core.Exp import DDC.Core.Parser.Type import DDC.Core.Parser.Exp +import DDC.Core.Parser.Context import DDC.Core.Parser.Base import DDC.Core.Lexer.Tokens import DDC.Core.Compounds @@ -17,9 +18,10 @@ -- Module --------------------------------------------------------------------- -- | Parse a core module. pModule :: (Ord n, Pretty n) - => Parser n (Module () n) -pModule - = do pTok KModule + => Context + -> Parser n (Module P.SourcePos n) +pModule c + = do sp <- pTokSP KModule name <- pModuleName -- exports { SIG;+ } @@ -27,7 +29,7 @@ <- P.choice [do pTok KExports pTok KBraceBra - sigs <- P.sepEndBy1 pTypeSig (pTok KSemiColon) + sigs <- P.sepEndBy1 (pTypeSig c) (pTok KSemiColon) pTok KBraceKet return sigs @@ -38,8 +40,8 @@ <- P.choice [do pTok KImports pTok KBraceBra - importKinds <- P.sepEndBy pImportKindSpec (pTok KSemiColon) - importTypes <- P.sepEndBy pImportTypeSpec (pTok KSemiColon) + importKinds <- P.sepEndBy (pImportKindSpec c) (pTok KSemiColon) + importTypes <- P.sepEndBy (pImportTypeSpec c) (pTok KSemiColon) pTok KBraceKet return (importKinds, importTypes) @@ -51,11 +53,11 @@ pTok KWith -- LET;+ - lts <- P.sepBy1 pLets (pTok KIn) + lts <- P.sepBy1 (pLetsSP c) (pTok KIn) -- The body of the module consists of the top-level bindings wrapped -- around a unit constructor place-holder. - let body = xLets () lts (xUnit ()) + let body = xLetsAnnot lts (xUnit sp) -- ISSUE #295: Check for duplicate exported names in module parser. -- The names are added to a unique map, so later ones with the same @@ -70,20 +72,23 @@ -- | Parse a type signature. -pTypeSig :: Ord n => Parser n (n, Type n) -pTypeSig +pTypeSig + :: Ord n + => Context -> Parser n (n, Type n) + +pTypeSig c = do var <- pVar pTok KColonColon - t <- pType + t <- pType c return (var, t) -- | Parse the type signature of an imported variable. pImportKindSpec :: (Ord n, Pretty n) - => Parser n (n, (QualName n, Kind n)) + => Context -> Parser n (n, (QualName n, Kind n)) -pImportKindSpec +pImportKindSpec c = pTok KType >> P.choice [ -- Import with an explicit external name. @@ -92,12 +97,12 @@ pTok KWith n <- pName pTok KColonColon - k <- pType + k <- pType c return (n, (qn, k)) , do n <- pName pTok KColonColon - k <- pType + k <- pType c return (n, (QualName (ModuleName []) n, k)) ] @@ -105,9 +110,9 @@ -- | Parse the type signature of an imported variable. pImportTypeSpec :: (Ord n, Pretty n) - => Parser n (n, (QualName n, Type n)) + => Context -> Parser n (n, (QualName n, Type n)) -pImportTypeSpec +pImportTypeSpec c = P.choice [ -- Import with an explicit external name. -- Module.varExternal with varLocal @@ -115,11 +120,11 @@ pTok KWith n <- pName pTok KColonColon - t <- pType + t <- pType c return (n, (qn, t)) , do n <- pName pTok KColonColon - t <- pType + t <- pType c return (n, (QualName (ModuleName []) n, t)) ] diff --git a/DDC/Core/Parser/Param.hs b/DDC/Core/Parser/Param.hs --- a/DDC/Core/Parser/Param.hs +++ b/DDC/Core/Parser/Param.hs @@ -7,6 +7,7 @@ where import DDC.Core.Exp import DDC.Core.Parser.Type +import DDC.Core.Parser.Context import DDC.Core.Parser.Base (Parser) import DDC.Core.Lexer.Tokens import qualified DDC.Base.Parser as P @@ -22,29 +23,6 @@ | ParamValue (Bind n) (Type n) (Type n) --- | Build the type of a function from specifications of its parameters, --- and the type of the body. -funTypeOfParams - :: [ParamSpec n] -- ^ Spec of parameters. - -> Type n -- ^ Type of body. - -> Type n -- ^ Type of whole function. - -funTypeOfParams [] tBody = tBody -funTypeOfParams (p:ps) tBody - = case p of - ParamType b - -> TForall b - $ funTypeOfParams ps tBody - - ParamWitness b - -> T.tImpl (T.typeOfBind b) - $ funTypeOfParams ps tBody - - ParamValue b eff clo - -> T.tFun (T.typeOfBind b) eff clo - $ funTypeOfParams ps tBody - - -- | Build the expression of a function from specifications of its parameters, -- and the expression for the body. expOfParams @@ -66,21 +44,56 @@ -> XLam a b $ expOfParams a ps xBody +-- | Build the type of a function from specifications of its parameters, +-- and the type of the body. +funTypeOfParams + :: Context + -> [ParamSpec n] -- ^ Spec of parameters. + -> Type n -- ^ Type of body. + -> Type n -- ^ Type of whole function. + +funTypeOfParams _ [] tBody + = tBody + +funTypeOfParams c (p:ps) tBody + = case p of + ParamType b + -> TForall b + $ funTypeOfParams c ps tBody + + ParamWitness b + -> T.tImpl (T.typeOfBind b) + $ funTypeOfParams c ps tBody + + ParamValue b eff clo + | contextFunctionalEffects c + , contextFunctionalClosures c + -> T.tFunEC (T.typeOfBind b) eff clo + $ funTypeOfParams c ps tBody + + | otherwise + -> T.tFun (T.typeOfBind b) + $ funTypeOfParams c ps tBody + + -- | Parse a parameter specification. -- -- [BIND1 BIND2 .. BINDN : TYPE] -- or (BIND : TYPE) -- or (BIND : TYPE) { EFFECT | CLOSURE } -- -pBindParamSpec :: Ord n => Parser n [ParamSpec n] -pBindParamSpec +pBindParamSpec + :: Ord n + => Context -> Parser n [ParamSpec n] + +pBindParamSpec c = P.choice -- Type parameter -- [BIND1 BIND2 .. BINDN : TYPE] [ do pTok KSquareBra bs <- P.many1 pBinder pTok KColon - t <- pType + t <- pType c pTok KSquareKet return [ ParamType b | b <- zipWith T.makeBindFromBinder bs (repeat t)] @@ -91,7 +104,7 @@ , do pTok KAngleBra b <- pBinder pTok KColon - t <- pType + t <- pType c pTok KAngleKet return [ ParamWitness $ T.makeBindFromBinder b t] @@ -101,15 +114,15 @@ , do pTok KRoundBra b <- pBinder pTok KColon - t <- pType + t <- pType c pTok KRoundKet (eff, clo) <- P.choice [ do pTok KBraceBra - eff' <- pType + eff' <- pType c pTok KBar - clo' <- pType + clo' <- pType c pTok KBraceKet return (eff', clo') @@ -118,5 +131,4 @@ return $ [ParamValue (T.makeBindFromBinder b t) eff clo] ] - diff --git a/DDC/Core/Parser/Type.hs b/DDC/Core/Parser/Type.hs --- a/DDC/Core/Parser/Type.hs +++ b/DDC/Core/Parser/Type.hs @@ -9,6 +9,7 @@ , pTok , pTokAs) where +import DDC.Core.Parser.Context import DDC.Core.Parser.Base import DDC.Core.Lexer.Tokens import DDC.Type.Exp @@ -19,20 +20,25 @@ -- | Parse a type. -pType :: Ord n => Parser n (Type n) -pType = pTypeSum +pType :: Ord n + => Context -> Parser n (Type n) + +pType c + = pTypeSum c "a type" -- | Parse a type sum. -pTypeSum :: Ord n => Parser n (Type n) pTypeSum - = do t1 <- pTypeForall + :: Ord n + => Context -> Parser n (Type n) +pTypeSum c + = do t1 <- pTypeForall c P.choice [ -- Type sums. -- T2 + T3 do pTok KPlus - t2 <- pTypeSum + t2 <- pTypeSum c return $ TSum $ TS.fromList (tBot sComp) [t1, t2] , do return t1 ] @@ -55,60 +61,69 @@ , do pTok KUnderscore return $ RNone ] "a binder" - + + -- | Parse a quantified type. -pTypeForall :: Ord n => Parser n (Type n) -pTypeForall +pTypeForall + :: Ord n + => Context -> Parser n (Type n) +pTypeForall c = P.choice [ -- Universal quantification. -- [v1 v1 ... vn : T1]. T2 do pTok KSquareBra bs <- P.many1 pBinder pTok KColon - k <- pTypeSum + k <- pTypeSum c pTok KSquareKet pTok KDot - body <- pTypeForall + body <- pTypeForall c return $ foldr TForall body $ map (\b -> makeBindFromBinder b k) bs -- Body type - , do pTypeFun] + , do pTypeFun c] "a type" -- | Parse a function type. -pTypeFun :: Ord n => Parser n (Type n) -pTypeFun - = do t1 <- pTypeApp +pTypeFun + :: Ord n + => Context -> Parser n (Type n) + +pTypeFun c + = do t1 <- pTypeApp c P.choice [ -- T1 ~> T2 do pTok KArrowTilde - t2 <- pTypeFun + t2 <- pTypeFun c return $ TApp (TApp (TCon (TyConKind KiConFun)) t1) t2 -- T1 => T2 , do pTok KArrowEquals - t2 <- pTypeFun + t2 <- pTypeFun c return $ TApp (TApp (TCon (TyConWitness TwConImpl)) t1) t2 -- T1 -> T2 , do pTok KArrowDash - t2 <- pTypeFun - return $ t1 `tFunPE` t2 + t2 <- pTypeFun c + if ( contextFunctionalEffects c + && contextFunctionalClosures c) + then return $ t1 `tFunPE` t2 + else return $ t1 `tFun` t2 -- T1 -(TSUM | TSUM)> t2 , do pTok KDash pTok KRoundBra - eff <- pTypeSum + eff <- pTypeSum c pTok KBar - clo <- pTypeSum + clo <- pTypeSum c pTok KRoundKet pTok KAngleKet - t2 <- pTypeFun - return $ tFun t1 eff clo t2 + t2 <- pTypeFun c + return $ tFunEC t1 eff clo t2 -- Body type @@ -117,16 +132,20 @@ -- | Parse a type application. -pTypeApp :: Ord n => Parser n (Type n) -pTypeApp - = do (t:ts) <- P.many1 pTypeAtom +pTypeApp + :: Ord n + => Context -> Parser n (Type n) +pTypeApp c + = do (t:ts) <- P.many1 (pTypeAtom c) return $ foldl TApp t ts "an atomic type or type application" -- | Parse a variable, constructor or parenthesised type. -pTypeAtom :: Ord n => Parser n (Type n) -pTypeAtom +pTypeAtom + :: Ord n + => Context -> Parser n (Type n) +pTypeAtom c = P.choice -- (~>) and (=>) and (->) and (TYPE2) [ do pTok KRoundBra @@ -141,14 +160,27 @@ , do pTok KArrowDash pTok KRoundKet - return (TCon $ TyConSpec TcConFun) - , do t <- pTypeSum + -- Decide what type constructor to use for the (->) token. + -- Only use the function constructor with latent effects + -- and closures if the language fragment supports both. + if ( contextFunctionalEffects c + && contextFunctionalClosures c) + then return (TCon $ TyConSpec TcConFunEC) + else return (TCon $ TyConSpec TcConFun) + + , do t <- pTypeSum c pTok KRoundKet return t ] -- Named type constructors + , do so <- pSoCon + return $ TCon (TyConSort so) + + , do ki <- pKiCon + return $ TCon (TyConKind ki) + , do tc <- pTcCon return $ TCon (TyConSpec tc) @@ -157,15 +189,6 @@ , do tc <- pTyConNamed return $ TCon tc - - -- Symbolic constructors. - , do pTokAs KSortComp (TCon $ TyConSort SoConComp) - , do pTokAs KSortProp (TCon $ TyConSort SoConProp) - , do pTokAs KKindValue (TCon $ TyConKind KiConData) - , do pTokAs KKindRegion (TCon $ TyConKind KiConRegion) - , do pTokAs KKindEffect (TCon $ TyConKind KiConEffect) - , do pTokAs KKindClosure (TCon $ TyConKind KiConClosure) - , do pTokAs KKindWitness (TCon $ TyConKind KiConWitness) -- Bottoms. , do pTokAs KBotEffect (tBot kEffect) @@ -185,21 +208,39 @@ ------------------------------------------------------------------------------- --- | Parse a builtin `TcCon` +-- | Parse a builtin sort constructor. +pSoCon :: Parser n SoCon +pSoCon = P.pTokMaybe f + "a sort constructor" + where f (KA (KSoConBuiltin c)) = Just c + f _ = Nothing + + +-- | Parse a builtin kind constructor. +pKiCon :: Parser n KiCon +pKiCon = P.pTokMaybe f + "a kind constructor" + where f (KA (KKiConBuiltin c)) = Just c + f _ = Nothing + + +-- | Parse a builtin type constructor. pTcCon :: Parser n TcCon pTcCon = P.pTokMaybe f "a type constructor" where f (KA (KTcConBuiltin c)) = Just c f _ = Nothing --- | Parse a builtin `TwCon` + +-- | Parse a builtin witness type constructor. pTwCon :: Parser n TwCon pTwCon = P.pTokMaybe f "a witness constructor" where f (KA (KTwConBuiltin c)) = Just c f _ = Nothing --- | Parse a user `TcCon` + +-- | Parse a user defined type constructor. pTyConNamed :: Parser n (TyCon n) pTyConNamed = P.pTokMaybe f diff --git a/DDC/Core/Parser/Witness.hs b/DDC/Core/Parser/Witness.hs --- a/DDC/Core/Parser/Witness.hs +++ b/DDC/Core/Parser/Witness.hs @@ -5,80 +5,109 @@ , pWitnessAtom) where import DDC.Core.Parser.Type +import DDC.Core.Parser.Context import DDC.Core.Parser.Base import DDC.Core.Lexer.Tokens import DDC.Core.Exp -import DDC.Base.Parser (()) +import DDC.Base.Parser ((), SourcePos) import qualified DDC.Base.Parser as P import qualified DDC.Type.Compounds as T - +import Control.Monad + -- | Parse a witness expression. -pWitness :: Ord n => Parser n (Witness n) -pWitness = pWitnessJoin +pWitness + :: Ord n + => Context -> Parser n (Witness SourcePos n) +pWitness c = pWitnessJoin c -- | Parse a witness join. -pWitnessJoin :: Ord n => Parser n (Witness n) pWitnessJoin + :: Ord n + => Context -> Parser n (Witness SourcePos n) +pWitnessJoin c -- WITNESS or WITNESS & WITNESS - = do w1 <- pWitnessApp + = do w1 <- pWitnessApp c P.choice - [ do pTok KAmpersand - w2 <- pWitnessJoin - return (WJoin w1 w2) + [ do sp <- pTokSP KAmpersand + w2 <- pWitnessJoin c + return (WJoin sp w1 w2) , do return w1 ] -- | Parse a witness application. -pWitnessApp :: Ord n => Parser n (Witness n) pWitnessApp - = do (x:xs) <- P.many1 pWitnessArg - return $ foldl WApp x xs + :: Ord n + => Context -> Parser n (Witness SourcePos n) +pWitnessApp c + = do (x:xs) <- P.many1 (pWitnessArgSP c) + let x' = fst x + let sp = snd x + let xs' = map fst xs + return $ foldl (WApp sp) x' xs' + "a witness expression or application" -- | Parse a witness argument. -pWitnessArg :: Ord n => Parser n (Witness n) -pWitnessArg +pWitnessArgSP + :: Ord n + => Context -> Parser n (Witness SourcePos n, SourcePos) + +pWitnessArgSP c = P.choice [ -- [TYPE] - do pTok KSquareBra - t <- pType + do sp <- pTokSP KSquareBra + t <- pType c pTok KSquareKet - return $ WType t + return (WType sp t, sp) -- WITNESS - , do pWitnessAtom ] + , do pWitnessAtomSP c ] + -- | Parse a variable, constructor or parenthesised witness. -pWitnessAtom :: Ord n => Parser n (Witness n) -pWitnessAtom +pWitnessAtom + :: Ord n + => Context -> Parser n (Witness SourcePos n) + +pWitnessAtom c + = liftM fst (pWitnessAtomSP c) + + +-- | Parse a variable, constructor or parenthesised witness, +-- also returning source position. +pWitnessAtomSP + :: Ord n + => Context -> Parser n (Witness SourcePos n, SourcePos) + +pWitnessAtomSP c = P.choice -- (WITNESS) - [ do pTok KRoundBra - w <- pWitness - pTok KRoundKet - return $ w + [ do sp <- pTokSP KRoundBra + w <- pWitness c + pTok KRoundKet + return (w, sp) -- Named constructors - , do con <- pCon - return $ WCon (WiConBound (UName con) (T.tBot T.kWitness)) + , do (con, sp) <- pConSP + return (WCon sp (WiConBound (UName con) (T.tBot T.kWitness)), sp) -- Baked-in witness constructors. - , do wb <- pWbCon - return $ WCon (WiConBuiltin wb) + , do (wb, sp) <- pWbConSP + return (WCon sp (WiConBuiltin wb), sp) -- Debruijn indices - , do i <- pIndex - return $ WVar (UIx i) + , do (i, sp) <- pIndexSP + return (WVar sp (UIx i), sp) -- Variables - , do var <- pVar - return $ WVar (UName var) ] + , do (var, sp) <- pVarSP + return (WVar sp (UName var), sp) ] "a witness" diff --git a/DDC/Core/Predicates.hs b/DDC/Core/Predicates.hs --- a/DDC/Core/Predicates.hs +++ b/DDC/Core/Predicates.hs @@ -14,6 +14,9 @@ -- * Applications , isXApp + -- * Let bindings + , isXLet + -- * Types and Witnesses , isXType , isXWitness @@ -55,7 +58,7 @@ -- | Check whether a witness is a `WVar` or `WCon`. -isAtomW :: Witness n -> Bool +isAtomW :: Witness a n -> Bool isAtomW ww = case ww of WVar{} -> True @@ -94,6 +97,14 @@ XApp{} -> True _ -> False + +-- Let Bindings --------------------------------------------------------------- +isXLet :: Exp a n -> Bool +isXLet xx + = case xx of + XLet{} -> True + _ -> False + -- Type and Witness ----------------------------------------------------------- -- | Check whether an expression is an `XType` diff --git a/DDC/Core/Pretty.hs b/DDC/Core/Pretty.hs --- a/DDC/Core/Pretty.hs +++ b/DDC/Core/Pretty.hs @@ -120,6 +120,14 @@ $ ppr lts <+> text "in" <$> ppr x + XCase _ x1 [AAlt p x2] + -> pprParen' (d > 2) + $ text "caselet" <+> ppr p + <+> nest 2 (breakWhen (not $ isSimpleX x1) + <> text "=" <+> align (ppr x1)) + <+> text "in" + <$> ppr x2 + XCase _ x alts -> pprParen' (d > 2) $ (nest 2 $ text "case" <+> ppr x <+> text "of" <+> lbrace <> line @@ -127,6 +135,14 @@ <> line <> rbrace + XCast _ CastSuspend x + -> pprParen' (d > 2) + $ text "suspend" <$> ppr x + + XCast _ CastRun x + -> pprParen' (d > 2) + $ text "run" <+> ppr x + XCast _ cc x -> pprParen' (d > 2) $ ppr cc <+> text "in" @@ -184,17 +200,23 @@ CastForget w -> text "forget" <+> angles (ppr w) + CastSuspend + -> text "suspend" + CastRun + -> text "run" + + -- Lets ----------------------------------------------------------------------- instance (Pretty n, Eq n) => Pretty (Lets a n) where ppr lts = case lts of - LLet m b x + LLet b x -> let dBind = if isBot (typeOfBind b) then ppr (binderOfBind b) else ppr b in text "let" - <+> align ( dBind <> ppr m + <+> align ( dBind <> nest 2 ( breakWhen (not $ isSimpleX x) <> text "=" <+> align (ppr x))) @@ -239,28 +261,20 @@ <+> ppr b -instance (Pretty n, Eq n) => Pretty (LetMode n) where - ppr lm - = case lm of - LetStrict -> empty - LetLazy Nothing -> text " lazy" - LetLazy (Just w) -> text " lazy <" <> ppr w <> text ">" - - -- Witness -------------------------------------------------------------------- -instance (Pretty n, Eq n) => Pretty (Witness n) where +instance (Pretty n, Eq n) => Pretty (Witness a n) where pprPrec d ww = case ww of - WVar n -> ppr n - WCon wc -> ppr wc + WVar _ n -> ppr n + WCon _ wc -> ppr wc - WApp w1 w2 + WApp _ w1 w2 -> pprParen (d > 10) (ppr w1 <+> pprPrec 11 w2) - WJoin w1 w2 + WJoin _ w1 w2 -> pprParen (d > 9) (ppr w1 <+> text "&" <+> ppr w2) - WType t -> text "[" <> ppr t <> text "]" + WType _ t -> text "[" <> ppr t <> text "]" instance (Pretty n, Eq n) => Pretty (WiCon n) where diff --git a/DDC/Core/Transform/Annotate.hs b/DDC/Core/Transform/Annotate.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Transform/Annotate.hs @@ -0,0 +1,92 @@ + +module DDC.Core.Transform.Annotate + (Annotate (..)) +where +import qualified DDC.Core.Exp.Annot as A +import qualified DDC.Core.Exp.Simple as S + + +-- | Convert the `Simple` version of the AST to the `Annot` version, +-- using a the provided default annotation value. +class Annotate + (c1 :: * -> * -> *) + (c2 :: * -> * -> *) | c1 -> c2 + where + annotate :: a -> c1 a n -> c2 a n + + +instance Annotate S.Exp A.Exp where + annotate def xx + = let down = annotate def + in case xx of + S.XAnnot _ (S.XAnnot a x) -> down (S.XAnnot a x) + S.XAnnot a (S.XVar u) -> A.XVar a u + S.XAnnot a (S.XCon dc) -> A.XCon a dc + S.XAnnot a (S.XLAM b x) -> A.XLAM a b (down x) + S.XAnnot a (S.XLam b x) -> A.XLam a b (down x) + S.XAnnot a (S.XApp x1 x2) -> A.XApp a (down x1) (down x2) + S.XAnnot a (S.XLet lts x) -> A.XLet a (down lts) (down x) + S.XAnnot a (S.XCase x alts) -> A.XCase a (down x) (map down alts) + S.XAnnot a (S.XCast c x) -> A.XCast a (down c) (down x) + S.XAnnot _ (S.XType t) -> A.XType t + S.XAnnot _ (S.XWitness w) -> A.XWitness (down w) + + S.XVar u -> A.XVar def u + S.XCon dc -> A.XCon def dc + S.XLAM b x -> A.XLAM def b (down x) + S.XLam b x -> A.XLam def b (down x) + S.XApp x1 x2 -> A.XApp def (down x1) (down x2) + S.XLet lts x -> A.XLet def (down lts) (down x) + S.XCase x alts -> A.XCase def (down x) (map down alts) + S.XCast c x -> A.XCast def (down c) (down x) + S.XType t -> A.XType t + S.XWitness w -> A.XWitness (down w) + + +instance Annotate S.Cast A.Cast where + annotate def cc + = let down = annotate def + in case cc of + S.CastWeakenEffect eff -> A.CastWeakenEffect eff + S.CastWeakenClosure clo -> A.CastWeakenClosure (map down clo) + S.CastPurify w -> A.CastPurify (down w) + S.CastForget w -> A.CastForget (down w) + S.CastSuspend -> A.CastSuspend + S.CastRun -> A.CastRun + + +instance Annotate S.Lets A.Lets where + annotate def lts + = let down = annotate def + in case lts of + S.LLet b x -> A.LLet b (down x) + S.LRec bxs -> A.LRec [(b, down x) | (b, x) <- bxs] + S.LLetRegions bks bts -> A.LLetRegions bks bts + S.LWithRegion u -> A.LWithRegion u + + +instance Annotate S.Alt A.Alt where + annotate def alt + = let down = annotate def + in case alt of + S.AAlt w x -> A.AAlt w (down x) + + +instance Annotate S.Witness A.Witness where + annotate def wit + = let down = annotate def + in case wit of + S.WAnnot _ (S.WAnnot a x) -> down (S.WAnnot a x) + S.WAnnot a (S.WVar u) -> A.WVar a u + S.WAnnot a (S.WCon wc) -> A.WCon a wc + S.WAnnot a (S.WApp w1 w2) -> A.WApp a (down w1) (down w2) + S.WAnnot a (S.WJoin w1 w2) -> A.WJoin a (down w1) (down w2) + S.WAnnot a (S.WType t) -> A.WType a t + + S.WVar u -> A.WVar def u + S.WCon dc -> A.WCon def dc + S.WApp x1 x2 -> A.WApp def (down x1) (down x2) + S.WJoin x1 x2 -> A.WJoin def (down x1) (down x2) + S.WType t -> A.WType def t + + diff --git a/DDC/Core/Transform/Deannotate.hs b/DDC/Core/Transform/Deannotate.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Transform/Deannotate.hs @@ -0,0 +1,78 @@ + +module DDC.Core.Transform.Deannotate + (Deannotate(..)) +where +import qualified DDC.Core.Exp.Annot as A +import qualified DDC.Core.Exp.Simple as S + + +-- | Convert the `Annot` version of the AST to the `Simple` version, +-- using the provided function to decide when to keep the annotation. +class Deannotate + (c1 :: * -> * -> *) + (c2 :: * -> * -> *) | c1 -> c2 + where + deannotate :: (a -> Maybe a) -> c1 a n -> c2 a n + + +instance Deannotate A.Exp S.Exp where + deannotate f xx + = let down = deannotate f + wrap a x = case f a of + Nothing -> x + Just a' -> S.XAnnot a' x + in case xx of + A.XVar a u -> wrap a (S.XVar u) + A.XCon a dc -> wrap a (S.XCon dc) + A.XLAM a b x -> wrap a (S.XLAM b (down x)) + A.XLam a b x -> wrap a (S.XLam b (down x)) + A.XApp a x1 x2 -> wrap a (S.XApp (down x1) (down x2)) + A.XLet a lts x2 -> wrap a (S.XLet (down lts) (down x2)) + A.XCase a x alts -> wrap a (S.XCase (down x) (map down alts)) + A.XCast a cc x -> wrap a (S.XCast (down cc) (down x)) + A.XType t -> S.XType t + A.XWitness w -> S.XWitness (down w) + + +instance Deannotate A.Lets S.Lets where + deannotate f lts + = let down = deannotate f + in case lts of + A.LLet b x -> S.LLet b (down x) + A.LRec bxs -> S.LRec [(b, down x) | (b, x) <- bxs] + A.LLetRegions bks bts -> S.LLetRegions bks bts + A.LWithRegion u -> S.LWithRegion u + + +instance Deannotate A.Alt S.Alt where + deannotate f aa + = case aa of + A.AAlt w x -> S.AAlt w (deannotate f x) + + +instance Deannotate A.Witness S.Witness where + deannotate f ww + = let down = deannotate f + wrap a x = case f a of + Nothing -> x + Just a' -> S.WAnnot a' x + in case ww of + A.WVar a u -> wrap a (S.WVar u) + A.WCon a wc -> wrap a (S.WCon wc) + A.WApp a w1 w2 -> wrap a (S.WApp (down w1) (down w2)) + A.WJoin a w1 w2 -> wrap a (S.WJoin (down w1) (down w2)) + A.WType a t -> wrap a (S.WType t) + + +instance Deannotate A.Cast S.Cast where + deannotate f cc + = let down = deannotate f + in case cc of + A.CastWeakenEffect e -> S.CastWeakenEffect e + A.CastWeakenClosure xs -> S.CastWeakenClosure (map down xs) + A.CastPurify w -> S.CastPurify (down w) + A.CastForget w -> S.CastForget (down w) + A.CastSuspend -> S.CastSuspend + A.CastRun -> S.CastRun + + diff --git a/DDC/Core/Transform/LiftT.hs b/DDC/Core/Transform/LiftT.hs --- a/DDC/Core/Transform/LiftT.hs +++ b/DDC/Core/Transform/LiftT.hs @@ -11,67 +11,51 @@ mapBoundAtDepthT f d xx = let down = mapBoundAtDepthT f d in case xx of - XVar a u -> XVar a u - XCon{} -> xx - XApp a x1 x2 -> XApp a (down x1) (down x2) - XLAM a b x -> XLAM a b (mapBoundAtDepthT f (d + countBAnons [b]) x) - XLam a b x -> XLam a (down b) (down x) + XVar a u -> XVar a u + XCon{} -> xx + XApp a x1 x2 -> XApp a (down x1) (down x2) + XLAM a b x -> XLAM a b (mapBoundAtDepthT f (d + countBAnons [b]) x) + XLam a b x -> XLam a (down b) (down x) XLet a lets x -> let (lets', levels) = mapBoundAtDepthTLets f d lets in XLet a lets' (mapBoundAtDepthT f (d + levels) x) - XCase a x alts -> XCase a (down x) (map down alts) - XCast a cc x -> XCast a (down cc) (down x) - XType t -> XType (down t) - XWitness w -> XWitness (down w) - - -instance Ord n => MapBoundT LetMode n where - mapBoundAtDepthT f d m - = case m of - LetStrict -> m - LetLazy Nothing -> m - LetLazy (Just w) -> LetLazy (Just $ mapBoundAtDepthT f d w) + XCase a x alts -> XCase a (down x) (map down alts) + XCast a cc x -> XCast a (down cc) (down x) + XType t -> XType (down t) + XWitness w -> XWitness (down w) -instance Ord n => MapBoundT Witness n where +instance Ord n => MapBoundT (Witness a) n where mapBoundAtDepthT f d ww = let down = mapBoundAtDepthT f d in case ww of - WVar u -> WVar (down u) - WCon _ -> ww - WApp w1 w2 -> WApp (down w1) (down w2) - WJoin w1 w2 -> WJoin (down w1) (down w2) - WType t -> WType (down t) + WVar a u -> WVar a (down u) + WCon _ _ -> ww + WApp a w1 w2 -> WApp a (down w1) (down w2) + WJoin a w1 w2 -> WJoin a (down w1) (down w2) + WType a t -> WType a (down t) instance Ord n => MapBoundT (Cast a) n where mapBoundAtDepthT f d cc = let down = mapBoundAtDepthT f d in case cc of - CastWeakenEffect t - -> CastWeakenEffect (down t) - - CastWeakenClosure xs - -> CastWeakenClosure (map down xs) - - CastPurify w - -> CastPurify (down w) - - CastForget w - -> CastForget (down w) + CastWeakenEffect t -> CastWeakenEffect (down t) + CastWeakenClosure xs -> CastWeakenClosure (map down xs) + CastPurify w -> CastPurify (down w) + CastForget w -> CastForget (down w) + CastSuspend -> CastSuspend + CastRun -> CastRun instance Ord n => MapBoundT (Alt a) n where mapBoundAtDepthT f d (AAlt p x) = let down = mapBoundAtDepthT f d in case p of - PDefault - -> AAlt PDefault (down x) - - PData dc bs - -> AAlt (PData dc (map down bs)) (down x) + PDefault -> AAlt PDefault (down x) + PData dc bs -> AAlt (PData dc (map down bs)) (down x) mapBoundAtDepthTLets @@ -84,8 +68,8 @@ mapBoundAtDepthTLets f d lts = let down = mapBoundAtDepthT f d in case lts of - LLet m b x - -> ( LLet (down m) (down b) (down x) + LLet b x + -> ( LLet (down b) (down x) , 0) LRec bs diff --git a/DDC/Core/Transform/LiftX.hs b/DDC/Core/Transform/LiftX.hs --- a/DDC/Core/Transform/LiftX.hs +++ b/DDC/Core/Transform/LiftX.hs @@ -102,39 +102,30 @@ XWitness w -> XWitness (down w) -instance MapBoundX LetMode n where - mapBoundAtDepthX f d m - = case m of - LetStrict -> m - LetLazy Nothing -> m - LetLazy (Just w) -> LetLazy (Just $ mapBoundAtDepthX f d w) - - -instance MapBoundX Witness n where +instance MapBoundX (Witness a) n where mapBoundAtDepthX f d ww = let down = mapBoundAtDepthX f d in case ww of - WVar u -> WVar (down u) - WCon _ -> ww - WApp w1 w2 -> WApp (down w1) (down w2) - WJoin w1 w2 -> WJoin (down w1) (down w2) - WType _ -> ww + WVar a u -> WVar a (down u) + WCon _ _ -> ww + WApp a w1 w2 -> WApp a (down w1) (down w2) + WJoin a w1 w2 -> WJoin a (down w1) (down w2) + WType _ _ -> ww instance MapBoundX (Cast a) n where mapBoundAtDepthX f d cc = case cc of - CastWeakenEffect{} + CastWeakenEffect{} -> cc CastWeakenClosure xs -> CastWeakenClosure (map (mapBoundAtDepthX f d) xs) - CastPurify w - -> CastPurify w - - CastForget w - -> CastForget w + CastPurify w -> CastPurify w + CastForget w -> CastForget w + CastSuspend -> CastSuspend + CastRun -> CastRun instance MapBoundX (Alt a) n where @@ -156,13 +147,12 @@ mapBoundAtDepthXLets f d lts = case lts of - LLet m b x + LLet b x -> let inc = countBAnons [b] - m' = mapBoundAtDepthX f d m - + -- non-recursive binding: do not increase x's depth x' = mapBoundAtDepthX f d x - in (LLet m' b x', inc) + in (LLet b x', inc) LRec bs -> let inc = countBAnons (map fst bs) diff --git a/DDC/Core/Transform/Reannotate.hs b/DDC/Core/Transform/Reannotate.hs --- a/DDC/Core/Transform/Reannotate.hs +++ b/DDC/Core/Transform/Reannotate.hs @@ -25,35 +25,34 @@ instance Reannotate Exp where reannotate f xx - = {-# SCC reannotate #-} - let down x = reannotate f x + = let down x = reannotate f x in case xx of - XVar a u -> XVar (f a) u - XCon a u -> XCon (f a) u - XLAM a b x -> XLAM (f a) b (down x) - XLam a b x -> XLam (f a) b (down x) - XApp a x1 x2 -> XApp (f a) (down x1) (down x2) - XLet a lts x -> XLet (f a) (down lts) (down x) - XCase a x alts -> XCase (f a) (down x) (map down alts) - XCast a c x -> XCast (f a) (down c) (down x) - XType t -> XType t - XWitness w -> XWitness w + XVar a u -> XVar (f a) u + XCon a u -> XCon (f a) u + XLAM a b x -> XLAM (f a) b (down x) + XLam a b x -> XLam (f a) b (down x) + XApp a x1 x2 -> XApp (f a) (down x1) (down x2) + XLet a lts x -> XLet (f a) (down lts) (down x) + XCase a x alts -> XCase (f a) (down x) (map down alts) + XCast a c x -> XCast (f a) (down c) (down x) + XType t -> XType t + XWitness w -> XWitness (down w) instance Reannotate Lets where reannotate f xx = let down x = reannotate f x in case xx of - LLet m b x -> LLet m b (down x) - LRec bxs -> LRec [(b, down x) | (b, x) <- bxs] - LLetRegions b bs -> LLetRegions b bs - LWithRegion b -> LWithRegion b + LLet b x -> LLet b (down x) + LRec bxs -> LRec [(b, down x) | (b, x) <- bxs] + LLetRegions b bs -> LLetRegions b bs + LWithRegion b -> LWithRegion b instance Reannotate Alt where reannotate f aa = case aa of - AAlt w x -> AAlt w (reannotate f x) + AAlt w x -> AAlt w (reannotate f x) instance Reannotate Cast where @@ -62,7 +61,19 @@ in case cc of CastWeakenEffect eff -> CastWeakenEffect eff CastWeakenClosure xs -> CastWeakenClosure (map down xs) - CastPurify w -> CastPurify w - CastForget w -> CastForget w + CastPurify w -> CastPurify (down w) + CastForget w -> CastForget (down w) + CastSuspend -> CastSuspend + CastRun -> CastRun + +instance Reannotate Witness where + reannotate f ww + = let down x = reannotate f x + in case ww of + WVar a u -> WVar (f a) u + WCon a c -> WCon (f a) c + WApp a w1 w2 -> WApp (f a) (down w1) (down w2) + WJoin a w1 w2 -> WJoin (f a) (down w1) (down w2) + WType a t -> WType (f a) t diff --git a/DDC/Core/Transform/Rename.hs b/DDC/Core/Transform/Rename.hs --- a/DDC/Core/Transform/Rename.hs +++ b/DDC/Core/Transform/Rename.hs @@ -21,21 +21,13 @@ import DDC.Type.Transform.Rename -instance Rename LetMode where - renameWith sub lm - = case lm of - LetStrict -> lm - LetLazy (Just t) -> LetLazy (Just $ renameWith sub t) - LetLazy Nothing -> LetLazy Nothing - - -instance Rename Witness where +instance Rename (Witness a) where renameWith sub ww = let down x = renameWith x in case ww of - WVar u -> WVar (use0 sub u) - WCon{} -> ww - WApp w1 w2 -> WApp (down sub w1) (down sub w2) - WJoin w1 w2 -> WJoin (down sub w1) (down sub w2) - WType t -> WType (down sub t) + WVar a u -> WVar a (use0 sub u) + WCon a c -> WCon a c + WApp a w1 w2 -> WApp a (down sub w1) (down sub w2) + WJoin a w1 w2 -> WJoin a (down sub w1) (down sub w2) + WType a t -> WType a (down sub t) diff --git a/DDC/Core/Transform/SpreadX.hs b/DDC/Core/Transform/SpreadX.hs --- a/DDC/Core/Transform/SpreadX.hs +++ b/DDC/Core/Transform/SpreadX.hs @@ -10,6 +10,7 @@ import qualified DDC.Type.Env as Env import qualified Data.Map as Map + class SpreadX (c :: * -> *) where -- | Spread type annotations from binders and the environment into bound @@ -90,6 +91,8 @@ CastWeakenClosure xs -> CastWeakenClosure (map down xs) CastPurify w -> CastPurify (down w) CastForget w -> CastForget (down w) + CastSuspend -> CastSuspend + CastRun -> CastRun instance SpreadX Pat where @@ -113,7 +116,8 @@ spreadX kenv tenv lts = let down x = spreadX kenv tenv x in case lts of - LLet m b x -> LLet (down m) (down b) (down x) + LLet b x + -> LLet (down b) (down x) LRec bxs -> let (bs, xs) = unzip bxs @@ -132,23 +136,15 @@ -> LWithRegion (spreadX kenv tenv b) -instance SpreadX LetMode where - spreadX kenv tenv lm - = case lm of - LetStrict -> LetStrict - LetLazy Nothing -> LetLazy Nothing - LetLazy (Just w) -> LetLazy (Just $ spreadX kenv tenv w) - - -instance SpreadX Witness where +instance SpreadX (Witness a) where spreadX kenv tenv ww = let down = spreadX kenv tenv in case ww of - WCon wc -> WCon (down wc) - WVar u -> WVar (down u) - WApp w1 w2 -> WApp (down w1) (down w2) - WJoin w1 w2 -> WJoin (down w1) (down w2) - WType t1 -> WType (spreadT kenv t1) + WCon a wc -> WCon a (down wc) + WVar a u -> WVar a (down u) + WApp a w1 w2 -> WApp a (down w1) (down w2) + WJoin a w1 w2 -> WJoin a (down w1) (down w2) + WType a t1 -> WType a (spreadT kenv t1) instance SpreadX WiCon where diff --git a/DDC/Core/Transform/SubstituteTX.hs b/DDC/Core/Transform/SubstituteTX.hs --- a/DDC/Core/Transform/SubstituteTX.hs +++ b/DDC/Core/Transform/SubstituteTX.hs @@ -82,12 +82,11 @@ x' = down sub1 x in XLam a b' x' - XLet a (LLet m b x1) x2 - -> let m' = down sub m - x1' = down sub x1 + XLet a (LLet b x1) x2 + -> let x1' = down sub x1 (sub1, b') = bind0 sub (down sub b) x2' = down sub1 x2 - in XLet a (LLet m' b' x1') x2' + in XLet a (LLet b' x1') x2' XLet a (LRec bxs) x2 -> let (bs, xs) = unzip bxs @@ -111,15 +110,6 @@ XWitness w -> XWitness (down sub w) -instance SubstituteTX LetMode where - substituteWithTX tArg sub lm - = let down x = substituteWithTX tArg x - in case lm of - LetStrict -> lm - LetLazy Nothing -> lm - LetLazy (Just w) -> LetLazy (Just $ down sub w) - - instance SubstituteTX (Alt a) where substituteWithTX tArg sub aa = let down x = substituteWithTX tArg x @@ -141,17 +131,19 @@ CastWeakenClosure clo -> CastWeakenClosure (map (down sub) clo) CastPurify w -> CastPurify (down sub w) CastForget w -> CastForget (down sub w) + CastSuspend -> CastSuspend + CastRun -> CastRun -instance SubstituteTX Witness where +instance SubstituteTX (Witness a) where substituteWithTX tArg sub ww = let down x = substituteWithTX tArg x in case ww of - WVar u -> WVar u + WVar a u -> WVar a u WCon{} -> ww - WApp w1 w2 -> WApp (down sub w1) (down sub w2) - WJoin w1 w2 -> WJoin (down sub w1) (down sub w2) - WType t -> WType (down sub t) + WApp a w1 w2 -> WApp a (down sub w1) (down sub w2) + WJoin a w1 w2 -> WJoin a (down sub w1) (down sub w2) + WType a t -> WType a (down sub t) instance SubstituteTX Bind where diff --git a/DDC/Core/Transform/SubstituteWX.hs b/DDC/Core/Transform/SubstituteWX.hs --- a/DDC/Core/Transform/SubstituteWX.hs +++ b/DDC/Core/Transform/SubstituteWX.hs @@ -23,7 +23,7 @@ -- type being substituted, and starts with an empty binder stack. substituteWX :: (Ord n, SubstituteWX c) - => Bind n -> Witness n -> c n -> c n + => Bind n -> Witness a n -> c a n -> c a n substituteWX b wArg xx | Just u <- takeSubstBoundOfBind b @@ -56,19 +56,19 @@ -- | Wrapper for `substituteWithWX` to substitute multiple things. substituteWXs :: (Ord n, SubstituteWX c) - => [(Bind n, Witness n)] -> c n -> c n + => [(Bind n, Witness a n)] -> c a n -> c a n substituteWXs bts x = foldr (uncurry substituteWX) x bts ------------------------------------------------------------------------------- -class SubstituteWX (c :: * -> *) where +class SubstituteWX (c :: * -> * -> *) where substituteWithWX - :: forall n. Ord n - => Witness n -> Sub n -> c n -> c n + :: forall a n. Ord n + => Witness a n -> Sub n -> c a n -> c a n -instance SubstituteWX (Exp a) where +instance SubstituteWX Exp where substituteWithWX wArg sub xx = {-# SCC substituteWithWX #-} let down s x = substituteWithWX wArg s x @@ -88,12 +88,11 @@ x' = down sub1 x in XLam a b' x' - XLet a (LLet m b x1) x2 - -> let m' = down sub m - x1' = down sub x1 + XLet a (LLet b x1) x2 + -> let x1' = down sub x1 (sub1, b') = bind0 sub b x2' = down sub1 x2 - in XLet a (LLet m' b' x1') x2' + in XLet a (LLet b' x1') x2' XLet a (LRec bxs) x2 -> let (bs, xs) = unzip bxs @@ -117,17 +116,7 @@ XWitness w -> XWitness (down sub w) - -instance SubstituteWX LetMode where - substituteWithWX wArg sub lm - = let down s x = substituteWithWX wArg s x - in case lm of - LetStrict -> lm - LetLazy Nothing -> LetLazy Nothing - LetLazy (Just w) -> LetLazy (Just (down sub w)) - - -instance SubstituteWX (Alt a) where +instance SubstituteWX Alt where substituteWithWX wArg sub aa = let down s x = substituteWithWX wArg s x in case aa of @@ -140,7 +129,7 @@ in AAlt (PData uCon bs') x' -instance SubstituteWX (Cast a) where +instance SubstituteWX Cast where substituteWithWX wArg sub cc = let down s x = substituteWithWX wArg s x into s x = renameWith s x @@ -149,6 +138,8 @@ CastWeakenClosure xs -> CastWeakenClosure (map (down sub) xs) CastPurify w -> CastPurify (down sub w) CastForget w -> CastForget (down sub w) + CastSuspend -> CastSuspend + CastRun -> CastRun instance SubstituteWX Witness where @@ -156,20 +147,20 @@ = let down s x = substituteWithWX wArg s x into s x = renameWith s x in case ww of - WVar u + WVar a u -> case substW wArg sub u of - Left u' -> WVar u' + Left u' -> WVar a u' Right w -> w WCon{} -> ww - WApp w1 w2 -> WApp (down sub w1) (down sub w2) - WJoin w1 w2 -> WJoin (down sub w1) (down sub w2) - WType t -> WType (into sub t) + WApp a w1 w2 -> WApp a (down sub w1) (down sub w2) + WJoin a w1 w2 -> WJoin a (down sub w1) (down sub w2) + WType a t -> WType a (into sub t) -- | Rewrite or substitute into a witness variable. -substW :: Ord n => Witness n -> Sub n -> Bound n - -> Either (Bound n) (Witness n) +substW :: Ord n => Witness a n -> Sub n -> Bound n + -> Either (Bound n) (Witness a n) substW wArg sub u = case substBound (subStack0 sub) (subBound sub) u of diff --git a/DDC/Core/Transform/SubstituteXX.hs b/DDC/Core/Transform/SubstituteXX.hs --- a/DDC/Core/Transform/SubstituteXX.hs +++ b/DDC/Core/Transform/SubstituteXX.hs @@ -72,7 +72,7 @@ -- Perform type substitution for an `XType` -- and witness substitution for an `XWitness` substituteXArg - :: (Ord n, SubstituteXX c, SubstituteWX (c a), SubstituteTX (c a)) + :: (Ord n, SubstituteXX c, SubstituteWX c, SubstituteTX (c a)) => Bind n -> Exp a n -> c a n -> c a n substituteXArg b arg x @@ -84,7 +84,7 @@ -- | Wrapper for `substituteXArgs` to substitute multiple arguments. substituteXArgs - :: (Ord n, SubstituteXX c, SubstituteWX (c a), SubstituteTX (c a)) + :: (Ord n, SubstituteXX c, SubstituteWX c, SubstituteTX (c a)) => [(Bind n, Exp a n)] -> c a n -> c a n substituteXArgs bas x @@ -122,12 +122,11 @@ x' = down sub1 x in XLam a b' x' - XLet a (LLet m b x1) x2 - -> let m' = into sub m - x1' = down sub x1 + XLet a (LLet b x1) x2 + -> let x1' = down sub x1 (sub1, b') = bind0 sub b x2' = down sub1 x2 - in XLet a (LLet m' b' x1') x2' + in XLet a (LLet b' x1') x2' XLet a (LRec bxs) x2 -> let (bs, xs) = unzip bxs @@ -173,6 +172,8 @@ CastWeakenClosure xs -> CastWeakenClosure (map (down sub) xs) CastPurify w -> CastPurify (into sub w) CastForget w -> CastForget (into sub w) + CastSuspend -> CastSuspend + CastRun -> CastRun -- | Rewrite or substitute into an expression variable. diff --git a/DDC/Core/Transform/Trim.hs b/DDC/Core/Transform/Trim.hs --- a/DDC/Core/Transform/Trim.hs +++ b/DDC/Core/Transform/Trim.hs @@ -98,7 +98,7 @@ BindUse BoundWit u | member u tenv -> [] - | otherwise -> [XWitness (WVar u)] + | otherwise -> [XWitness (WVar a u)] BindUse BoundSpec u | member u kenv -> [] diff --git a/DDC/Type/Check.hs b/DDC/Type/Check.hs --- a/DDC/Type/Check.hs +++ b/DDC/Type/Check.hs @@ -1,7 +1,10 @@ -- | Check the kind of a type. module DDC.Type.Check - ( -- * Kinds of Types - checkType + ( Config (..) + , configOfProfile + + -- * Kinds of Types + , checkType , kindOfType -- * Kinds of Constructors @@ -16,6 +19,7 @@ import DDC.Type.Check.Error import DDC.Type.Check.ErrorMessage () import DDC.Type.Check.CheckCon +import DDC.Type.Check.Config import DDC.Type.Compounds import DDC.Type.Predicates import DDC.Type.Exp @@ -30,7 +34,6 @@ import qualified DDC.Type.Env as Env import qualified Data.Map as Map - -- | The type checker monad. type CheckM n = G.CheckM (Error n) @@ -38,7 +41,7 @@ -- Wrappers ------------------------------------------------------------------- -- | Check a type in the given environment, returning an error or its kind. checkType :: (Ord n, Show n, Pretty n) - => DataDefs n + => Config n -> KindEnv n -> Type n -> Either (Error n) (Kind n) @@ -49,7 +52,7 @@ -- | Check a type in an empty environment, returning an error or its kind. kindOfType :: (Ord n, Show n, Pretty n) - => DataDefs n + => Config n -> Type n -> Either (Error n) (Kind n) @@ -66,24 +69,24 @@ -- crushable components terms. checkTypeM :: (Ord n, Show n, Pretty n) - => DataDefs n + => Config n -> KindEnv n -> Type n -> CheckM n (Kind n) -checkTypeM defs env tt - = -- trace (pretty $ text "checkTypeM:" <+> ppr tt) $ +checkTypeM config env tt + = -- trace (renderPlain $ text "checkTypeM:" <+> text (show tt)) $ {-# SCC checkTypeM #-} - checkTypeM' defs env tt + checkTypeM' config env tt -- Variables ------------------ -checkTypeM' _defs env (TVar u) +checkTypeM' _config env (TVar u) = case Env.lookup u env of Just t -> return t Nothing -> throw $ ErrorUndefined u -- Constructors --------------- -checkTypeM' defs _env tt@(TCon tc) +checkTypeM' config env tt@(TCon tc) = case tc of -- Sorts don't have a higher classification. TyConSort _ -> throw $ ErrorNakedSort tt @@ -99,12 +102,20 @@ TyConSpec tcc -> return $ kindOfTcCon tcc -- User defined type constructors need to be in the set of data defs. - TyConBound u k + TyConBound u k -> case u of UName n - | Just _ <- Map.lookup n (dataDefsTypes defs) + | Just _ <- Map.lookup n + $ dataDefsTypes $ configPrimDataDefs config -> return k + | Just s <- Env.lookupName n + $ configPrimSupers config + -> return s + + | Just s <- Env.lookupName n env + -> return s + | otherwise -> throw $ ErrorUndefinedCtor u @@ -113,9 +124,9 @@ -- Quantifiers ---------------- -checkTypeM' defs env tt@(TForall b1 t2) - = do _ <- checkTypeM defs env (typeOfBind b1) - k2 <- checkTypeM defs (Env.extend b1 env) t2 +checkTypeM' config env tt@(TForall b1 t2) + = do _ <- checkTypeM config env (typeOfBind b1) + k2 <- checkTypeM config (Env.extend b1 env) t2 -- The body must have data or witness kind. when ( (not $ isDataKind k2) @@ -127,18 +138,18 @@ -- Applications --------------- -- Applications of the kind function constructor are handled directly -- because the constructor doesn't have a sort by itself. -checkTypeM' defs env (TApp (TApp (TCon (TyConKind KiConFun)) k1) k2) - = do _ <- checkTypeM defs env k1 - s2 <- checkTypeM defs env k2 +checkTypeM' config env (TApp (TApp (TCon (TyConKind KiConFun)) k1) k2) + = do _ <- checkTypeM config env k1 + s2 <- checkTypeM config env k2 return s2 -- The implication constructor is overloaded and can have the -- following kinds: -- (=>) :: @ ~> @ ~> @, for witness implication. -- (=>) :: @ ~> * ~> *, for a context. -checkTypeM' defs env tt@(TApp (TApp (TCon (TyConWitness TwConImpl)) t1) t2) - = do k1 <- checkTypeM defs env t1 - k2 <- checkTypeM defs env t2 +checkTypeM' config env tt@(TApp (TApp (TCon (TyConWitness TwConImpl)) t1) t2) + = do k1 <- checkTypeM config env t1 + k2 <- checkTypeM config env t2 if isWitnessKind k1 && isWitnessKind k2 then return kWitness else if isWitnessKind k1 && isDataKind k2 @@ -146,9 +157,9 @@ else throw $ ErrorWitnessImplInvalid tt t1 k1 t2 k2 -- Type application. -checkTypeM' defs env tt@(TApp t1 t2) - = do k1 <- checkTypeM defs env t1 - k2 <- checkTypeM defs env t2 +checkTypeM' config env tt@(TApp t1 t2) + = do k1 <- checkTypeM config env t1 + k2 <- checkTypeM config env t2 case k1 of TApp (TApp (TCon (TyConKind KiConFun)) k11) k12 | k11 == k2 -> return k12 @@ -157,8 +168,8 @@ _ -> throw $ ErrorAppNotFun tt t1 k1 t2 k2 -- Sums ----------------------- -checkTypeM' defs env (TSum ts) - = do ks <- mapM (checkTypeM defs env) $ TS.toList ts +checkTypeM' config env (TSum ts) + = do ks <- mapM (checkTypeM config env) $ TS.toList ts -- Check that all the types in the sum have a single kind, -- and return that kind. diff --git a/DDC/Type/Check/CheckCon.hs b/DDC/Type/Check/CheckCon.hs --- a/DDC/Type/Check/CheckCon.hs +++ b/DDC/Type/Check/CheckCon.hs @@ -53,7 +53,7 @@ TwConLazy -> kRegion `kFun` kWitness TwConHeadLazy -> kData `kFun` kWitness TwConManifest -> kRegion `kFun` kWitness - TwConDisjoint -> kEffect `kFun` kEffect `kFun` kWitness + TwConDisjoint -> kEffect `kFun` kEffect `kFun` kWitness TwConDistinct n -> (replicate n kRegion) `kFuns` kWitness @@ -62,7 +62,9 @@ kindOfTcCon tc = case tc of TcConUnit -> kData - TcConFun -> [kData, kEffect, kClosure, kData] `kFuns` kData + TcConFun -> kData `kFun` kData `kFun` kData + TcConFunEC -> [kData, kEffect, kClosure, kData] `kFuns` kData + TcConSusp -> kEffect `kFun` kData `kFun` kData TcConRead -> kRegion `kFun` kEffect TcConHeadRead -> kData `kFun` kEffect TcConDeepRead -> kData `kFun` kEffect diff --git a/DDC/Type/Check/Config.hs b/DDC/Type/Check/Config.hs new file mode 100644 --- /dev/null +++ b/DDC/Type/Check/Config.hs @@ -0,0 +1,66 @@ + +module DDC.Type.Check.Config + ( Config (..) + , configOfProfile) +where +import DDC.Type.DataDef +import DDC.Type.Env (SuperEnv, KindEnv, TypeEnv) +import qualified DDC.Core.Fragment as F + + +-- Config --------------------------------------------------------------------- +-- | Static configuration for the type checker. +-- These fields don't change as we decend into the tree. +-- +-- The starting configuration should be converted from the profile that +-- defines the language fragment you are checking. +-- See "DDC.Core.Fragment" and use `configOfProfile` below. +data Config n + = Config + { -- | Data type definitions. + configPrimDataDefs :: DataDefs n + + -- | Super kinds of primitive kinds. + , configPrimSupers :: SuperEnv n + + -- | Kinds of primitive types. + , configPrimKinds :: KindEnv n + + -- | Types of primitive operators. + , configPrimTypes :: TypeEnv n + + -- | Track effect type information. + , configTrackedEffects :: Bool + + -- | Track closure type information. + , configTrackedClosures :: Bool + + -- | Attach effect information to function types. + , configFunctionalEffects :: Bool + + -- | Attach closure information to function types. + , configFunctionalClosures :: Bool } + + + +-- | Convert a langage profile to a type checker configuration. +configOfProfile :: F.Profile n -> Config n +configOfProfile profile + = Config + { configPrimDataDefs = F.profilePrimDataDefs profile + , configPrimSupers = F.profilePrimSupers profile + , configPrimKinds = F.profilePrimKinds profile + , configPrimTypes = F.profilePrimTypes profile + + , configTrackedEffects = F.featuresTrackedEffects + $ F.profileFeatures profile + + , configTrackedClosures = F.featuresTrackedClosures + $ F.profileFeatures profile + + , configFunctionalEffects = F.featuresFunctionalEffects + $ F.profileFeatures profile + + , configFunctionalClosures = F.featuresFunctionalClosures + $ F.profileFeatures profile } + diff --git a/DDC/Type/Check/ErrorMessage.hs b/DDC/Type/Check/ErrorMessage.hs --- a/DDC/Type/Check/ErrorMessage.hs +++ b/DDC/Type/Check/ErrorMessage.hs @@ -11,10 +11,10 @@ ppr err = case err of ErrorUndefined u - -> text "Undefined type variable: " <> ppr u + -> text "Undefined type variable: " <> ppr u ErrorUndefinedCtor u - -> text "Undefined type constructor: " <> ppr u + -> text "Undefined type constructor: " <> ppr u ErrorUnappliedKindFun -> text "Can't take sort of unapplied kind function constructor." diff --git a/DDC/Type/Compounds.hs b/DDC/Type/Compounds.hs --- a/DDC/Type/Compounds.hs +++ b/DDC/Type/Compounds.hs @@ -16,6 +16,7 @@ , namedBoundMatchesBind , takeSubstBoundOfBind , takeSubstBoundsOfBinds + , replaceTypeOfBound -- * Kinds , kFun @@ -26,8 +27,9 @@ , takeResultKind -- * Quantifiers - , tForall - , tForalls, takeTForalls, eraseTForalls + , tForall, tForall' + , tForalls, tForalls' + , takeTForalls, eraseTForalls -- * Sums , tBot @@ -42,13 +44,18 @@ , takePrimeRegion -- * Functions - , tFun - , tFunPE - , takeTFun + , tFun, tFunOfList + , tFunPE, tFunOfListPE + , tFunEC + , takeTFun, takeTFunEC , takeTFunArgResult , takeTFunWitArgResult + , takeTFunAllArgResult , arityOfType + -- * Suspensions + , tSusp + -- * Implications , tImpl @@ -198,7 +205,17 @@ go level (BAnon _ : bs') = UIx level : go (level + 1) bs' go level (BNone _ : bs') = go level bs' - + +-- | If this `Bound` is a `UPrim` then replace it's embedded type with a new +-- one, otherwise return it unharmed. +replaceTypeOfBound :: Type n -> Bound n -> Bound n +replaceTypeOfBound t uu + = case uu of + UName{} -> uu + UPrim n _ -> UPrim n t + UIx{} -> uu + + -- Variables ------------------------------------------------------------------ -- | Construct a deBruijn index. tIx :: Kind n -> Int -> Type n @@ -285,15 +302,31 @@ tForall k f = TForall (BAnon k) (f (TVar (UIx 0))) +-- | Build an anonymous type abstraction, with a single parameter. +-- Starting the next index from the given value. +tForall' :: Int -> Kind n -> (Type n -> Type n) -> Type n +tForall' ix k f + = TForall (BAnon k) (f (TVar (UIx ix))) + -- | Build an anonymous type abstraction, with several parameters. +-- Starting the next index from the given value. tForalls :: [Kind n] -> ([Type n] -> Type n) -> Type n tForalls ks f = let bs = [BAnon k | k <- ks] - us = map (\i -> TVar (UIx i)) [0.. (length ks - 1)] + us = map (\i -> TVar (UIx i)) [0 .. (length ks - 1)] in foldr TForall (f $ reverse us) bs +-- | Build an anonymous type abstraction, with several parameters. +-- Starting the next index from the given value. +tForalls' :: Int -> [Kind n] -> ([Type n] -> Type n) -> Type n +tForalls' ix ks f + = let bs = [BAnon k | k <- ks] + us = map (\i -> TVar (UIx i)) [ix .. ix + (length ks - 1)] + in foldr TForall (f $ reverse us) bs + + -- | Split nested foralls from the front of a type, -- or `Nothing` if there was no outer forall. takeTForalls :: Type n -> Maybe ([Bind n], Type n) @@ -378,38 +411,101 @@ _ -> kk +-- Function types ------------------------------------------------------------- +-- | Construct a pure function type. +tFun :: Type n -> Type n -> Type n +tFun t1 t2 + = (TCon $ TyConSpec TcConFun) `tApps` [t1, t2] +infixr `tFun` + + -- | Construct a value type function, -- with the provided effect and closure. -tFun :: Type n -> Effect n -> Closure n -> Type n -> Type n -tFun t1 eff clo t2 - = (TCon $ TyConSpec TcConFun) `tApps` [t1, eff, clo, t2] -infixr `tFun` +tFunEC :: Type n -> Effect n -> Closure n -> Type n -> Type n +tFunEC t1 eff clo t2 + = (TCon $ TyConSpec TcConFunEC) `tApps` [t1, eff, clo, t2] +infixr `tFunEC` --- | Destruct the type of a value function. -takeTFun :: Type n -> Maybe (Type n, Effect n, Closure n, Type n) +-- | Construct a pure and empty value type function. +tFunPE :: Type n -> Type n -> Type n +tFunPE t1 t2 = tFunEC t1 (tBot kEffect) (tBot kClosure) t2 +infixr `tFunPE` + + +-- | Construct a pure and empty function from a list containing the +-- parameter and return type. Yields `Nothing` if the list is empty. +tFunOfList :: [Type n] -> Maybe (Type n) +tFunOfList ts + = case reverse ts of + [] -> Nothing + (t : tsArgs) + -> let tFuns' [] = t + tFuns' (t' : ts') = t' `tFun` tFuns' ts' + in Just $ tFuns' (reverse tsArgs) + + +-- | Construct a pure and empty function from a list containing the +-- parameter and return type. Yields `Nothing` if the list is empty. +tFunOfListPE :: [Type n] -> Maybe (Type n) +tFunOfListPE ts + = case reverse ts of + [] -> Nothing + (t : tsArgs) + -> let tFunPEs' [] = t + tFunPEs' (t' : ts') = t' `tFunPE` tFunPEs' ts' + in Just $ tFunPEs' (reverse tsArgs) + + +-- | Yield the argument and result type of a function type. +-- +-- Works for both `TcConFun` and `TcConFunEC`. +takeTFun :: Type n -> Maybe (Type n, Type n) takeTFun tt = case tt of - TApp (TApp (TApp (TApp (TCon (TyConSpec TcConFun)) t1) eff) clo) t2 + TApp (TApp (TCon (TyConSpec TcConFun)) t1) t2 + -> Just (t1, t2) + + TApp (TApp (TApp (TApp (TCon (TyConSpec TcConFunEC)) t1) _eff) _clo) t2 + -> Just (t1, t2) + + _ -> Nothing + + +-- | Yield the argument and result type of a function type. +takeTFunEC :: Type n -> Maybe (Type n, Effect n, Closure n, Type n) +takeTFunEC tt + = case tt of + TApp (TApp (TApp (TApp (TCon (TyConSpec TcConFunEC)) t1) eff) clo) t2 -> Just (t1, eff, clo, t2) + _ -> Nothing --- | Destruct the type of a function, --- returning just the argument and result types. +-- | Destruct the type of a function, returning just the argument and result types. +-- +-- Works for both `TcConFun` and `TcConFunEC`. takeTFunArgResult :: Type n -> ([Type n], Type n) takeTFunArgResult tt = case tt of - TApp (TApp (TApp (TApp (TCon (TyConSpec TcConFun)) t1) _eff) _clo) t2 - -> let (tsMore, tResult) = takeTFunArgResult t2 - in (t1 : tsMore, tResult) + TApp (TApp (TCon (TyConSpec TcConFun)) t1) t2 + -> let (tsMore, tResult) = takeTFunArgResult t2 + in (t1 : tsMore, tResult) + TApp (TApp (TApp (TApp (TCon (TyConSpec TcConFunEC)) t1) _eff) _clo) t2 + -> let (tsMore, tResult) = takeTFunArgResult t2 + in (t1 : tsMore, tResult) + _ -> ([], tt) + -- | Destruct the type of a function, -- returning the witness argument, value argument and result types. -- The function type must have the witness implications before -- the value arguments, eg @T1 => T2 -> T3 -> T4 -> T5@. +-- +-- Works for both `TcConFun` and `TcConFunEC`. +-- takeTFunWitArgResult :: Type n -> ([Type n], [Type n], Type n) takeTFunWitArgResult tt = case tt of @@ -421,6 +517,35 @@ in ([], tvsMore, tResult) +-- | Destruct the type of a possibly polymorphic function +-- returning all kinds of quantifiers, witness arguments, +-- and value arguments in the order they appear, along with +-- the type of the result. +takeTFunAllArgResult :: Type n -> ([Type n], Type n) +takeTFunAllArgResult tt + = case tt of + TVar{} -> ([], tt) + TCon{} -> ([], tt) + + TForall b t + -> let (tsMore, tResult) = takeTFunAllArgResult t + in (typeOfBind b : tsMore, tResult) + + TApp (TApp (TCon (TyConSpec TcConFun)) t1) t2 + -> let (tsMore, tResult) = takeTFunAllArgResult t2 + in (t1 : tsMore, tResult) + + TApp (TApp (TApp (TApp (TCon (TyConSpec TcConFunEC)) t1) _eff) _clo) t2 + -> let (tsMore, tResult) = takeTFunAllArgResult t2 + in (t1 : tsMore, tResult) + + TApp (TApp (TCon (TyConWitness TwConImpl)) t1) t2 + -> let (tsMore, tResult) = takeTFunAllArgResult t2 + in (t1 : tsMore, tResult) + + _ -> ([], tt) + + -- | Determine the arity of an expression by looking at its type. -- Count all the function arrows, and foralls. arityOfType :: Type n -> Int @@ -430,12 +555,7 @@ t -> length $ fst $ takeTFunArgResult t --- | Construct a pure and empty value type function. -tFunPE :: Type n -> Type n -> Type n -tFunPE t1 t2 = tFun t1 (tBot kEffect) (tBot kClosure) t2 -infixr `tFunPE` - - +-- Implications --------------------------------------------------------------- -- | Construct a witness implication type. tImpl :: Type n -> Type n -> Type n tImpl t1 t2 @@ -443,6 +563,12 @@ infixr `tImpl` +-- Suspensions ---------------------------------------------------------------- +tSusp :: Effect n -> Type n -> Type n +tSusp tE tA + = (TCon $ TyConSpec TcConSusp) `tApp` tE `tApp` tA + + -- Level 3 constructors (sorts) ----------------------------------------------- sComp = TCon $ TyConSort SoConComp sProp = TCon $ TyConSort SoConProp @@ -485,10 +611,10 @@ tHeadLazy = twCon1 TwConHeadLazy tManifest = twCon1 TwConManifest -tcCon1 tc t = (TCon $ TyConSpec tc) `tApp` t -twCon1 tc t = (TCon $ TyConWitness tc) `tApp` t +tcCon1 tc t = (TCon $ TyConSpec tc) `tApp` t +twCon1 tc t = (TCon $ TyConWitness tc) `tApp` t -twCon2 tc ts = tApps (TCon $ TyConWitness tc) ts +twCon2 tc ts = tApps (TCon $ TyConWitness tc) ts -- | Build a nullary type constructor of the given kind. @@ -499,5 +625,4 @@ -- | Build a type constructor application of one argumnet. tConData1 :: n -> Kind n -> Type n -> Type n tConData1 n k t1 = TApp (TCon (TyConBound (UName n) k)) t1 - diff --git a/DDC/Type/Env.hs b/DDC/Type/Env.hs --- a/DDC/Type/Env.hs +++ b/DDC/Type/Env.hs @@ -8,6 +8,7 @@ -- module DDC.Type.Env ( Env(..) + , SuperEnv , KindEnv , TypeEnv @@ -21,7 +22,7 @@ , fromList , fromTypeMap - -- * Projetions + -- * Projections , depth , member , memberBind @@ -65,8 +66,10 @@ -- | Type synonym to improve readability. -type KindEnv n = Env n +type SuperEnv n = Env n +-- | Type synonym to improve readability. +type KindEnv n = Env n -- | Type synonym to improve readability. type TypeEnv n = Env n diff --git a/DDC/Type/Exp/Base.hs b/DDC/Type/Exp/Base.hs --- a/DDC/Type/Exp/Base.hs +++ b/DDC/Type/Exp/Base.hs @@ -106,7 +106,7 @@ -- -- INVARIANT: this list doesn't contain more `TSum`s. , typeSumSpill :: ![Type n] } - deriving (Show) + deriving Show -- | Hash value used to insert types into the `typeSumElems` array of a `TypeSum`. @@ -142,17 +142,17 @@ | TyConSpec !TcCon -- | User defined and primitive constructors. - | TyConBound !(Bound n) !(Kind n) + | TyConBound !(Bound n) !(Type n) deriving Show -- | Sort constructor. data SoCon -- | Sort of witness kinds. - = SoConProp -- '@@' + = SoConProp -- 'Prop' -- | Sort of computation kinds. - | SoConComp -- '**' + | SoConComp -- 'Comp' deriving (Eq, Show) @@ -164,66 +164,66 @@ -- Witness kinds ------------------------ -- | Kind of witnesses. - | KiConWitness -- '@ :: @@' + | KiConWitness -- 'Witness :: Prop' -- Computation kinds --------------------- -- | Kind of data values. - | KiConData -- '* :: **' + | KiConData -- 'Data :: Comp' -- | Kind of regions. - | KiConRegion -- '% :: **' + | KiConRegion -- 'Region :: Comp' -- | Kind of effects. - | KiConEffect -- '! :: **' + | KiConEffect -- 'Effect :: Comp' -- | Kind of closures. - | KiConClosure -- '$ :: **' + | KiConClosure -- 'Closure :: Comp' deriving (Eq, Show) -- | Witness type constructors. data TwCon -- Witness implication. - = TwConImpl -- :: '(=>) :: @ ~> *' + = TwConImpl -- :: '(=>) :: Witness ~> Data' -- | Purity of some effect. - | TwConPure -- :: ! ~> @ + | TwConPure -- :: Effect ~> Witness -- | Emptiness of some closure. - | TwConEmpty -- :: $ ~> @ + | TwConEmpty -- :: Closure ~> Witness -- | Globalness of some region. - | TwConGlobal -- :: % ~> @ + | TwConGlobal -- :: Region ~> Witness -- | Globalness of material regions in some type. - | TwConDeepGlobal -- :: * ~> @ + | TwConDeepGlobal -- :: Data ~> Witness -- | Constancy of some region. - | TwConConst -- :: % ~> @ + | TwConConst -- :: Region ~> Witness -- | Constancy of material regions in some type - | TwConDeepConst -- :: * ~> @ + | TwConDeepConst -- :: Data ~> Witness -- | Mutability of some region. - | TwConMutable -- :: % ~> @ + | TwConMutable -- :: Region ~> Witness -- | Mutability of material regions in some type. - | TwConDeepMutable -- :: * ~> @ + | TwConDeepMutable -- :: Data ~> Witness -- | Distinctness of some n regions - | TwConDistinct Int -- :: * ~> [%] ~> @ + | TwConDistinct Int -- :: Data ~> [Region] ~> Witness -- | Laziness of some region. - | TwConLazy -- :: % ~> @ + | TwConLazy -- :: Region ~> Witness -- | Laziness of the primary region in some type. - | TwConHeadLazy -- :: * ~> @ + | TwConHeadLazy -- :: Data ~> Witness -- | Manifestness of some region (not lazy). - | TwConManifest -- :: % ~> @ + | TwConManifest -- :: Region ~> Witness -- | Non-interfering effects are disjoint. Used for rewrite rules. - | TwConDisjoint -- :: ! ~> ! ~> @ + | TwConDisjoint -- :: Effect ~> Effect ~> Witness deriving (Eq, Show) @@ -231,37 +231,43 @@ data TcCon -- Data type constructors --------------- -- | The unit data type constructor is baked in. - = TcConUnit -- 'Unit :: *' + = TcConUnit -- 'Unit :: Data' - -- | The function type constructor is baked in. - | TcConFun -- '(->) :: * ~> * ~> ! ~> $ ~> *' + -- | Pure function. + | TcConFun -- '(->)' :: Data ~> Data ~> Data + -- | Function with a latent effect and closure. + | TcConFunEC -- '(->) :: Data ~> Data ~> Effect ~> Closure ~> Data' + + -- | A suspended computation. + | TcConSusp -- 'S :: Effect ~> Data ~> Data' + -- Effect type constructors ------------- -- | Read of some region. - | TcConRead -- :: '% ~> !' + | TcConRead -- :: 'Region ~> Effect' -- | Read the head region in a data type. - | TcConHeadRead -- :: '* ~> !' + | TcConHeadRead -- :: 'Data ~> Effect' -- | Read of all material regions in a data type. - | TcConDeepRead -- :: '* ~> !' + | TcConDeepRead -- :: 'Data ~> Effect' -- | Write of some region. - | TcConWrite -- :: '% ~> !' + | TcConWrite -- :: 'Region ~> Effect' -- | Write to all material regions in some data type. - | TcConDeepWrite -- :: '* ~> !' + | TcConDeepWrite -- :: 'Data ~> Effect' -- | Allocation into some region. - | TcConAlloc -- :: '% ~> !' + | TcConAlloc -- :: 'Region ~> Effect' -- | Allocation into all material regions in some data type. - | TcConDeepAlloc -- :: '* ~> !' + | TcConDeepAlloc -- :: 'Data ~> Effect' -- Closure type constructors ------------ -- | Region is captured in a closure. - | TcConUse -- :: '% ~> $' + | TcConUse -- :: 'Region ~> Closure' -- | All material regions in a data type are captured in a closure. - | TcConDeepUse -- :: '* ~> $' + | TcConDeepUse -- :: 'Data ~> Closure' deriving (Eq, Show) diff --git a/DDC/Type/Pretty.hs b/DDC/Type/Pretty.hs --- a/DDC/Type/Pretty.hs +++ b/DDC/Type/Pretty.hs @@ -67,7 +67,13 @@ -> pprParen (d > 5) $ pprPrec 6 t1 <+> text "=>" pprPrec 5 t2 - TApp (TApp (TApp (TApp (TCon (TyConSpec TcConFun)) t1) eff) clo) t2 + -- Pure function. + TApp (TApp (TCon (TyConSpec TcConFun)) t1) t2 + -> pprParen (d > 5) + $ pprPrec 6 t1 <+> text "->" pprPrec 5 t2 + + -- Function with a latent effect and closure. + TApp (TApp (TApp (TApp (TCon (TyConSpec TcConFunEC)) t1) eff) clo) t2 | isBot eff, isBot clo -> pprParen (d > 5) $ pprPrec 6 t1 <+> text "->" pprPrec 5 t2 @@ -97,8 +103,17 @@ $ ppr t1 <+> pprPrec 11 t2 TSum ts - | isBot tt - -> ppr (Sum.kindOfSum ts) <> text "0" + | isBot tt, isEffectKind $ Sum.kindOfSum ts + -> text "Pure" + + | isBot tt, isClosureKind $ Sum.kindOfSum ts + -> text "Empty" + + | isBot tt, isDataKind $ Sum.kindOfSum ts + -> text "Bot" + + | isBot tt, otherwise + -> error $ stage ++ ": malformed sum" | otherwise -> pprParen (d > 9) $ ppr ts @@ -107,9 +122,9 @@ instance (Pretty n, Eq n) => Pretty (TypeSum n) where ppr ss = case Sum.toList ss of - [] | isEffectKind $ Sum.kindOfSum ss -> text "!0" - | isClosureKind $ Sum.kindOfSum ss -> text "$0" - | isDataKind $ Sum.kindOfSum ss -> text "*0" + [] | isEffectKind $ Sum.kindOfSum ss -> text "Pure" + | isClosureKind $ Sum.kindOfSum ss -> text "Empty" + | isDataKind $ Sum.kindOfSum ss -> text "Bot" | otherwise -> error $ stage ++ ": malformed sum" ts -> sep $ punctuate (text " +") (map ppr ts) @@ -129,27 +144,27 @@ instance Pretty SoCon where ppr sc = case sc of - SoConComp -> text "**" - SoConProp -> text "@@" + SoConComp -> text "Comp" + SoConProp -> text "Prop" instance Pretty KiCon where ppr kc = case kc of KiConFun -> text "(~>)" - KiConData -> text "*" - KiConRegion -> text "%" - KiConEffect -> text "!" - KiConClosure -> text "$" - KiConWitness -> text "@" + KiConData -> text "Data" + KiConRegion -> text "Region" + KiConEffect -> text "Effect" + KiConClosure -> text "Closure" + KiConWitness -> text "Witness" instance Pretty TwCon where ppr tw = case tw of TwConImpl -> text "(=>)" - TwConPure -> text "Pure" - TwConEmpty -> text "Empty" + TwConPure -> text "Purify" + TwConEmpty -> text "Emptify" TwConGlobal -> text "Global" TwConDeepGlobal -> text "DeepGlobal" TwConConst -> text "Const" @@ -168,6 +183,8 @@ = case tc of TcConUnit -> text "Unit" TcConFun -> text "(->)" + TcConFunEC -> text "(->)" + TcConSusp -> text "S" TcConRead -> text "Read" TcConHeadRead -> text "HeadRead" TcConDeepRead -> text "DeepRead" diff --git a/DDC/Type/Transform/Trim.hs b/DDC/Type/Transform/Trim.hs --- a/DDC/Type/Transform/Trim.hs +++ b/DDC/Type/Transform/Trim.hs @@ -107,7 +107,7 @@ -- Trim function constructors. -- See Note: Material variables and the interpreter - TApp (TApp (TApp (TApp (TCon (TyConSpec TcConFun)) _t1) _eff) clo) _t2 + TApp (TApp (TApp (TApp (TCon (TyConSpec TcConFunEC)) _t1) _eff) clo) _t2 -> Sum.singleton kClosure clo -- Trim a type application. diff --git a/DDC/Type/Universe.hs b/DDC/Type/Universe.hs --- a/DDC/Type/Universe.hs +++ b/DDC/Type/Universe.hs @@ -100,7 +100,7 @@ TCon (TyConSort _) -> Just UniverseKind TCon (TyConKind _) -> Just UniverseSpec TCon (TyConWitness _) -> Just UniverseWitness - TCon (TyConSpec TcConFun) -> Just UniverseData + TCon (TyConSpec TcConFunEC)-> Just UniverseData TCon (TyConSpec TcConUnit) -> Just UniverseData TCon (TyConSpec _) -> Nothing TCon (TyConBound _ k) -> universeFromType2 k diff --git a/LICENSE b/LICENSE --- a/LICENSE +++ b/LICENSE @@ -1,7 +1,7 @@ -------------------------------------------------------------------------------- The Disciplined Disciple Compiler License (MIT style) -Copyrite (K) 2007-2012 The Disciplined Disciple Compiler Strike Force +Copyrite (K) 2007-2013 The Disciplined Disciple Compiler Strike Force All rights reversed. Permission is hereby granted, free of charge, to any person obtaining a copy diff --git a/ddc-core.cabal b/ddc-core.cabal --- a/ddc-core.cabal +++ b/ddc-core.cabal @@ -1,5 +1,5 @@ Name: ddc-core -Version: 0.3.1.1 +Version: 0.3.2.1 License: MIT License-file: LICENSE Author: The Disciplined Disciple Compiler Strike Force @@ -9,16 +9,14 @@ Stability: experimental Category: Compilers/Interpreters Homepage: http://disciple.ouroborus.net -Bug-reports: disciple@ouroborus.net Synopsis: Disciplined Disciple Compiler core language and type checker. Description: Disciple Core is an explicitly typed language based on System-F2, intended as an intermediate representation for a compiler. In addition to the polymorphism of System-F2 it supports region, effect and closure typing. Evaluation order is - left-to-right call-by-value by default, but explicit lazy evaluation is also supported. - There is a capability system to track whether objects are mutable or constant, - and to ensure that computations that perform visible side effects are not suspended with - lazy evaluation. + left-to-right call-by-value by default. There is a capability system to track whether + objects are mutable or constant, and to ensure that computations that perform visible + side effects are not reordered inappropriately. See the @ddc-tools@ package for a user-facing interpreter and compiler. @@ -31,12 +29,33 @@ directory == 1.2.*, transformers == 0.3.*, mtl == 2.1.*, - ddc-base == 0.3.1.* + ddc-base == 0.3.2.* Exposed-modules: + DDC.Core.Annot.AnT + DDC.Core.Annot.AnTEC + + DDC.Core.Check + DDC.Core.Collect + + DDC.Core.Compounds.Annot + DDC.Core.Compounds.Simple + DDC.Core.Compounds + + DDC.Core.Exp.Simple + DDC.Core.Exp.Annot + DDC.Core.Exp + + DDC.Core.Fragment + DDC.Core.Lexer.Names DDC.Core.Lexer.Tokens + DDC.Core.Lexer + DDC.Core.Parser + + DDC.Core.Transform.Annotate + DDC.Core.Transform.Deannotate DDC.Core.Transform.LiftT DDC.Core.Transform.LiftX DDC.Core.Transform.Reannotate @@ -47,16 +66,8 @@ DDC.Core.Transform.SubstituteXX DDC.Core.Transform.Trim - DDC.Core.Check - DDC.Core.Collect - DDC.Core.Compounds - DDC.Core.DaCon - DDC.Core.Exp - DDC.Core.Fragment - DDC.Core.Lexer DDC.Core.Load DDC.Core.Module - DDC.Core.Parser DDC.Core.Predicates DDC.Core.Pretty @@ -93,8 +104,9 @@ DDC.Core.Collect.Support DDC.Core.Collect.Free - DDC.Core.Exp.Base - DDC.Core.Exp.NFData + DDC.Core.Exp.WiCon + DDC.Core.Exp.DaCon + DDC.Core.Exp.Pat DDC.Core.Fragment.Compliance DDC.Core.Fragment.Error @@ -105,6 +117,7 @@ DDC.Core.Lexer.Offside DDC.Core.Parser.Base + DDC.Core.Parser.Context DDC.Core.Parser.Exp DDC.Core.Parser.Module DDC.Core.Parser.Param @@ -114,6 +127,7 @@ DDC.Type.Check.CheckCon DDC.Type.Check.Error DDC.Type.Check.ErrorMessage + DDC.Type.Check.Config DDC.Type.Collect.FreeT @@ -143,4 +157,5 @@ DoAndIfThenElse DeriveDataTypeable ViewPatterns + FunctionalDependencies