ddc-core (empty) → 0.2.0.1
raw patch · 46 files changed
+8620/−0 lines, 46 filesdep +arraydep +basedep +containerssetup-changed
Dependencies added: array, base, containers, ddc-base, mtl, transformers
Files
- DDC/Core/Check.hs +17/−0
- DDC/Core/Check/CheckExp.hs +916/−0
- DDC/Core/Check/CheckWitness.hs +201/−0
- DDC/Core/Check/Error.hs +308/−0
- DDC/Core/Check/ErrorMessage.hs +345/−0
- DDC/Core/Check/TaggedClosure.hs +223/−0
- DDC/Core/Collect.hs +253/−0
- DDC/Core/Compounds.hs +172/−0
- DDC/Core/DataDef.hs +135/−0
- DDC/Core/Exp.hs +198/−0
- DDC/Core/Parser.hs +621/−0
- DDC/Core/Parser/Lexer.hs +293/−0
- DDC/Core/Parser/Tokens.hs +263/−0
- DDC/Core/Predicates.hs +97/−0
- DDC/Core/Pretty.hs +237/−0
- DDC/Core/Transform/LiftW.hs +116/−0
- DDC/Core/Transform/LiftX.hs +96/−0
- DDC/Core/Transform/SpreadX.hs +152/−0
- DDC/Core/Transform/SubstituteTX.hs +172/−0
- DDC/Core/Transform/SubstituteWX.hs +182/−0
- DDC/Core/Transform/SubstituteXX.hs +176/−0
- DDC/Type/Check.hs +178/−0
- DDC/Type/Check/CheckCon.hs +73/−0
- DDC/Type/Check/CheckError.hs +134/−0
- DDC/Type/Check/Monad.hs +28/−0
- DDC/Type/Compounds.hs +425/−0
- DDC/Type/Env.hs +153/−0
- DDC/Type/Equiv.hs +149/−0
- DDC/Type/Exp.hs +271/−0
- DDC/Type/Parser.hs +236/−0
- DDC/Type/Predicates.hs +98/−0
- DDC/Type/Pretty.hs +191/−0
- DDC/Type/Rewrite.hs +264/−0
- DDC/Type/Subsumes.hs +32/−0
- DDC/Type/Sum.hs +304/−0
- DDC/Type/Transform/Crush.hs +152/−0
- DDC/Type/Transform/Instantiate.hs +27/−0
- DDC/Type/Transform/LiftT.hs +63/−0
- DDC/Type/Transform/LowerT.hs +63/−0
- DDC/Type/Transform/SpreadT.hs +67/−0
- DDC/Type/Transform/SubstituteT.hs +138/−0
- DDC/Type/Transform/Trim.hs +163/−0
- DDC/Type/Universe.hs +116/−0
- LICENSE +20/−0
- Setup.hs +2/−0
- ddc-core.cabal +100/−0
+ DDC/Core/Check.hs view
@@ -0,0 +1,17 @@++-- | Type checker for the Disciple core language.+module DDC.Core.Check+ ( -- * Checking Expressions+ checkExp, typeOfExp++ -- * Checking Witnesses+ , checkWitness, typeOfWitness+ , typeOfWiCon++ -- * Error messages+ , Error(..))+where+import DDC.Core.Check.Error+import DDC.Core.Check.ErrorMessage ()+import DDC.Core.Check.CheckExp+import DDC.Core.Check.CheckWitness
+ DDC/Core/Check/CheckExp.hs view
@@ -0,0 +1,916 @@++-- | Type checker for the Disciple Core language.+module DDC.Core.Check.CheckExp+ ( checkExp+ , typeOfExp+ , CheckM+ , checkExpM+ , TaggedClosure(..))+where+import DDC.Core.DataDef+import DDC.Core.Predicates+import DDC.Core.Compounds+import DDC.Core.Exp+import DDC.Core.Pretty+import DDC.Core.Collect+import DDC.Core.Check.Error+import DDC.Core.Check.CheckWitness+import DDC.Core.Check.TaggedClosure+import DDC.Type.Transform.SubstituteT+import DDC.Type.Transform.Crush+import DDC.Type.Transform.Trim+import DDC.Type.Transform.Instantiate+import DDC.Type.Transform.LiftT+import DDC.Type.Equiv+import DDC.Type.Universe+import DDC.Type.Compounds+import DDC.Type.Predicates+import DDC.Type.Sum as Sum+import DDC.Type.Env (Env)+import DDC.Type.Check.Monad (result, throw)+import DDC.Base.Pretty ()+import Data.Set (Set)+import qualified DDC.Type.Env as Env+import qualified DDC.Type.Check as T+import qualified Data.Set as Set+import Control.Monad+import Data.List as L+import Data.Maybe+++-- Wrappers -------------------------------------------------------------------+-- | Type check an expression. +--+-- If it's good, you get a new version with types attached to all the bound+-- variables, as well its the type, effect and closure. +--+-- If it's bad, you get a description of the error.+--+-- The returned expression has types attached to all variable occurrences, +-- so you can call `typeOfExp` on any open subterm.+checkExp + :: (Ord n, Pretty n)+ => DataDefs n -- ^ Data type definitions.+ -> Env n -- ^ Kind environment.+ -> Env n -- ^ Type environment.+ -> Exp a n -- ^ Expression to check.+ -> Either (Error a n)+ ( Exp a n+ , Type n+ , Effect n+ , Closure n)++checkExp defs kenv tenv xx + = result+ $ do (xx', t, effs, clos) <- checkExpM defs kenv tenv xx+ return ( xx'+ , t+ , TSum effs+ , closureOfTaggedSet clos)+++-- | Like `checkExp`, but check in an empty environment,+-- and only return the value type of an expression.+--+-- As this function is not given an environment, the types of free variables+-- must be attached directly to the bound occurrences.+-- This attachment is performed by `checkExp` above.+--+typeOfExp + :: (Ord n, Pretty n)+ => DataDefs n+ -> Exp a n+ -> Either (Error a n) (Type n)+typeOfExp defs xx + = case checkExp defs Env.empty Env.empty xx of+ Left err -> Left err+ Right (_, t, _, _) -> Right t+++-- checkExp -------------------------------------------------------------------+-- | Like `checkExp` but using the `CheckM` monad to handle errors.+checkExpM + :: (Ord n, Pretty n)+ => DataDefs n -- ^ Data type definitions.+ -> Env n -- ^ Kind environment.+ -> Env n -- ^ Type environment.+ -> Exp a n -- ^ Expression to check.+ -> CheckM a n + ( Exp a n+ , Type n+ , TypeSum n+ , Set (TaggedClosure n))++checkExpM defs kenv tenv xx+ = checkExpM' defs kenv tenv xx+{-} = do (xx', t, eff, clo) <- checkExpM' defs kenv tenv xx+ trace (pretty $ vcat + [ text "checkExpM: " <+> ppr xx + , text " :: " <+> ppr t + , text " :!: " <+> ppr eff+ , text " :$: " <+> ppr clo+ , text ""])+ $ return (xx', t, eff, clo)+-}++-- variables ------------------------------------+checkExpM' _defs _kenv tenv (XVar a u)+ = do let tBound = typeOfBound u+ let mtEnv = Env.lookup u tenv++ let mkResult+ -- When annotation on the bound is bot,+ -- then use the type from the environment.+ | Just tEnv <- mtEnv+ , isBot tBound+ = return tEnv++ -- The bound has an explicit type annotation,+ -- which matches the one from the environment.+ -- + -- When the bound is a deBruijn index we need to lift the+ -- annotation on the original binder through any lambdas+ -- between the binding occurrence and the use.+ | Just tEnv <- mtEnv+ , UIx i _ <- u+ , equivT tBound (liftT (i + 1) tEnv) + = return tBound++ -- The bound has an explicit type annotation,+ -- which matches the one from the environment.+ | Just tEnv <- mtEnv+ , equivT tBound tEnv+ = return tEnv++ -- The bound has an explicit type annotation,+ -- which does not match the one from the environment.+ -- This shouldn't happen because the parser doesn't add non-bot+ -- annotations to bound variables.+ | Just tEnv <- mtEnv+ = throw $ ErrorVarAnnotMismatch u tEnv++ -- Variable not in environment, so use annotation.+ -- This happens when checking open terms.+ | otherwise+ = return tBound+ + tResult <- mkResult++ return ( XVar a u + , tResult+ , Sum.empty kEffect+ , Set.singleton + $ taggedClosureOfValBound + $ replaceTypeOfBound tResult u)+++-- constructors ---------------------------------+checkExpM' _defs _kenv _tenv (XCon a u)+ = return ( XCon a u+ , typeOfBound u+ , Sum.empty kEffect+ , Set.empty)+++-- application ------------------------------------+-- value-type application.+checkExpM' defs kenv tenv xx@(XApp a x1 (XType t2))+ = do (x1', t1, effs1, clos1) <- checkExpM defs kenv tenv x1+ k2 <- checkTypeM kenv t2+ case t1 of+ TForall b11 t12+ | typeOfBind b11 == k2+ -> return ( XApp a x1' (XType t2) + , substituteT b11 t2 t12+ , substituteT b11 t2 effs1+ , clos1 `Set.union` taggedClosureOfTyArg t2)++ | otherwise -> throw $ ErrorAppMismatch xx (typeOfBind b11) t2+ _ -> throw $ ErrorAppNotFun xx t1 t2+++-- value-witness application.+checkExpM' defs kenv tenv xx@(XApp a x1 (XWitness w2))+ = do (x1', t1, effs1, clos1) <- checkExpM defs kenv tenv x1+ t2 <- checkWitnessM kenv tenv w2+ case t1 of+ TApp (TApp (TCon (TyConWitness TwConImpl)) t11) t12+ | t11 `equivT` t2 + -> return ( XApp a x1' (XWitness w2)+ , t12+ , effs1+ , clos1)++ | otherwise -> throw $ ErrorAppMismatch xx t11 t2+ _ -> throw $ ErrorAppNotFun xx t1 t2+ ++-- value-value application.+checkExpM' defs kenv tenv xx@(XApp a x1 x2)+ = do (x1', t1, effs1, clos1) <- checkExpM defs kenv tenv x1+ (x2', t2, effs2, clos2) <- checkExpM defs kenv tenv x2+ case t1 of+ TApp (TApp (TApp (TApp (TCon (TyConSpec TcConFun)) t11) eff) _clo) t12+ | t11 `equivT` t2 + , effs <- Sum.fromList kEffect [eff]+ -> return ( XApp a x1' x2'+ , t12+ , effs1 `Sum.union` effs2 `Sum.union` effs+ , clos1 `Set.union` clos2)++ | otherwise -> throw $ ErrorAppMismatch xx t11 t2+ _ -> throw $ ErrorAppNotFun xx t1 t2+++-- spec abstraction -----------------------------+checkExpM' defs kenv tenv xx@(XLAM a b1 x2)+ = do let t1 = typeOfBind b1+ _ <- checkTypeM kenv t1++ -- Check the body+ let kenv' = Env.extend b1 kenv+ (x2', t2, e2, c2) <- checkExpM defs kenv' tenv x2+ k2 <- checkTypeM kenv' t2++ when (Env.memberBind b1 kenv)+ $ throw $ ErrorLamShadow xx b1++ -- The body of a spec abstraction must be pure.+ when (e2 /= Sum.empty kEffect)+ $ throw $ ErrorLamNotPure xx (TSum e2)++ -- The body of a spec abstraction must have data kind.+ when (not $ isDataKind k2)+ $ throw $ ErrorLamBodyNotData xx b1 t2 k2++ -- Mask closure terms due to locally bound region vars.+ let c2_cut = Set.fromList+ $ mapMaybe (cutTaggedClosureT b1)+ $ Set.toList c2++ return ( XLAM a b1 x2'+ , TForall b1 t2+ , Sum.empty kEffect+ , c2_cut)+ ++-- function abstractions ------------------------+checkExpM' defs kenv tenv xx@(XLam a b1 x2)+ = do let t1 = typeOfBind b1+ k1 <- checkTypeM kenv t1++ -- Check the body.+ let tenv' = Env.extend b1 tenv+ (x2', t2, e2, c2) <- checkExpM defs kenv tenv' x2 + k2 <- checkTypeM kenv t2++ -- The form of the function constructor depends on what universe the + -- binder is in.+ case universeFromType2 k1 of+ Just UniverseData+ | not $ isDataKind k1 -> throw $ ErrorLamBindNotData xx t1 k1+ | not $ isDataKind k2 -> throw $ ErrorLamBodyNotData xx b1 t2 k2 + | otherwise+ -> let + -- Cut closure terms due to locally bound value vars.+ -- This also lowers deBruijn indices in un-cut closure terms.+ c2_cut = Set.fromList+ $ mapMaybe (cutTaggedClosureX b1)+ $ Set.toList c2++ -- Trim the closure before we annotate the returned function+ -- type with it. + -- This should always succeed because trimClosure only returns+ -- Nothing if the closure is miskinded, and we've already+ -- allready checked that.+ Just c2_captured+ = trimClosure $ closureOfTaggedSet c2_cut++ in return ( XLam a b1 x2'+ , tFun t1 (TSum e2) c2_captured t2+ , Sum.empty kEffect+ , c2_cut) ++ Just UniverseWitness+ | e2 /= Sum.empty kEffect -> throw $ ErrorLamNotPure xx (TSum e2)+ | not $ isDataKind k2 -> throw $ ErrorLamBodyNotData xx b1 t2 k2+ | otherwise + -> return ( XLam a b1 x2'+ , tImpl t1 t2+ , Sum.empty kEffect+ , c2)++ _ -> throw $ ErrorMalformedType xx k1+++-- let --------------------------------------------+checkExpM' defs kenv tenv xx@(XLet a (LLet mode b11 x12) x2)+ = do -- Check the right of the binding.+ (x12', t12, effs12, clo12) + <- checkExpM defs kenv tenv x12++ -- Check binder annotation against the type we inferred for the right.+ (b11', k11') + <- checkLetBindOfTypeM xx kenv tenv t12 b11++ -- The right of the binding should have data kind.+ when (not $ isDataKind k11')+ $ throw $ ErrorLetBindingNotData xx b11' k11'+ + -- Check the body expression.+ let tenv1 = Env.extend b11' tenv+ (x2', t2, effs2, c2) <- checkExpM defs kenv tenv1 x2++ -- The body should have data kind.+ k2 <- checkTypeM kenv t2+ when (not $ isDataKind k2)+ $ throw $ ErrorLetBodyNotData xx t2 k2++ -- Mask closure terms due to locally bound value vars.+ let c2_cut = Set.fromList+ $ mapMaybe (cutTaggedClosureX b11')+ $ Set.toList c2++ -- Check purity and emptiness for lazy bindings.+ (case mode of+ LetStrict -> return ()+ LetLazy _+ -> do let eff12' = TSum effs12+ when (not $ isBot eff12')+ $ throw $ ErrorLetLazyNotPure xx b11 eff12'++ let clo12' = closureOfTaggedSet clo12+ when (not $ isBot clo12')+ $ throw $ ErrorLetLazyNotEmpty xx b11 clo12')++ -- Check region witness for lazy bindings.+ (case mode of+ LetStrict -> return ()++ -- Type of lazy binding has no head region, like Unit and (->).+ LetLazy Nothing+ -> do case takeDataTyConApps t12 of+ Just (_tc, t1 : _)+ -> do k1 <- checkTypeM 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 kenv tenv wit+ let tWitExp = case takeDataTyConApps t12 of+ Just (_tc, tR : _ts) -> tLazy tR+ _ -> tHeadLazy t12++ when (not $ equivT tWit tWitExp)+ $ throw $ ErrorLetLazyWitnessTypeMismatch + xx b11 tWit t12 tWitExp)+ ++ return ( XLet a (LLet mode b11' x12') x2'+ , t2+ , effs12 `Sum.union` effs2+ , clo12 `Set.union` c2_cut)+++-- letrec -----------------------------------------+checkExpM' defs kenv tenv xx@(XLet a (LRec bxs) xBody)+ = do + let (bs, xs) = unzip bxs++ -- Check all the annotations.+ ks <- mapM (checkTypeM kenv) $ map typeOfBind bs++ -- Check all the annots have data kind.+ zipWithM_ (\b k+ -> when (not $ isDataKind k)+ $ throw $ ErrorLetBindingNotData xx b k)+ bs ks++ -- All right hand sides need to be lambdas.+ forM_ xs $ \x + -> when (not $ (isXLam x || isXLAM x))+ $ throw $ ErrorLetrecBindingNotLambda xx x++ -- All variables are in scope in all right hand sides.+ let tenv' = Env.extends bs tenv++ -- Check the right hand sides.+ (xsRight', tsRight, _effssBinds, clossBinds) + <- liftM unzip4 $ mapM (checkExpM defs kenv tenv') xs++ -- Check annots on binders against inferred types of the bindings.+ zipWithM_ (\b t+ -> if not $ equivT (typeOfBind b) t+ then throw $ ErrorLetMismatch xx b t+ else return ())+ bs tsRight++ -- Check the body expression.+ (xBody', tBody, effsBody, closBody) + <- checkExpM defs kenv tenv' xBody++ -- The body type must have data kind.+ kBody <- checkTypeM kenv tBody+ when (not $ isDataKind kBody)+ $ throw $ ErrorLetBodyNotData xx tBody kBody++ -- Cut closure terms due to locally bound value vars.+ -- This also lowers deBruijn indices in un-cut closure terms.+ let clos_cut + = Set.fromList+ $ mapMaybe (cutTaggedClosureXs bs)+ $ Set.toList + $ Set.unions (closBody : clossBinds)++ return ( XLet a (LRec (zip bs xsRight')) xBody'+ , tBody+ , effsBody+ , clos_cut)+++-- letregion --------------------------------------+checkExpM' defs kenv tenv xx@(XLet a (LLetRegion b bs) x)+ = case takeSubstBoundOfBind b of+ Nothing -> checkExpM defs kenv tenv x+ Just u+ -> do+ -- Check the type on the region binder.+ let k = typeOfBind b+ checkTypeM kenv k++ -- The binder must have region kind.+ when (not $ isRegionKind k)+ $ throw $ ErrorLetRegionNotRegion xx b k++ -- We can't shadow region binders because we might have witnesses+ -- in the environment that conflict with the ones created here.+ when (Env.memberBind b kenv)+ $ throw $ ErrorLetRegionRebound xx b+ + -- Check the witness types.+ let kenv' = Env.extend b kenv+ mapM_ (checkTypeM kenv') $ map typeOfBind bs++ -- Check that the witnesses bound here are for the region,+ -- and they don't conflict with each other.+ checkWitnessBindsM xx u bs++ -- Check the body expression.+ let tenv' = Env.extends bs tenv+ (xBody', tBody, effs, clo) <- checkExpM defs kenv' tenv' x++ -- The body type must have data kind.+ kBody <- checkTypeM kenv' tBody+ when (not $ isDataKind kBody)+ $ throw $ ErrorLetBodyNotData xx tBody kBody++ -- The bound region variable cannot be free in the body type.+ let fvsT = freeT Env.empty tBody+ when (Set.member u fvsT)+ $ throw $ ErrorLetRegionFree xx b tBody+ + -- Delete effects on the bound region from the result.+ let effs' = Sum.delete (tRead (TVar u))+ $ Sum.delete (tWrite (TVar u))+ $ Sum.delete (tAlloc (TVar u))+ $ effs++ -- Delete the bound region variable from the closure.+ let clo_masked = Set.delete (GBoundRgnVar u) + $ clo+ + return ( XLet a (LLetRegion b bs) xBody'+ , tBody+ , effs'+ , clo_masked)+++-- withregion -----------------------------------+checkExpM' defs kenv tenv xx@(XLet a (LWithRegion u) x)+ = do -- Check the type on the region handle.+ let k = typeOfBound u+ checkTypeM kenv k++ -- The handle must have region kind.+ when (not $ isRegionKind k)+ $ throw $ ErrorWithRegionNotRegion xx u k+ + -- Check the body expression.+ (xBody', tBody, effs, clo) + <- checkExpM defs kenv tenv x++ -- The body type must have data kind.+ kBody <- checkTypeM kenv tBody+ when (not $ isDataKind kBody)+ $ throw $ ErrorLetBodyNotData xx tBody kBody+ + -- Delete effects on the bound region from the result.+ let tu = TCon $ TyConBound u+ let effs' = Sum.delete (tRead tu)+ $ Sum.delete (tWrite tu)+ $ Sum.delete (tAlloc tu)+ $ effs+ + -- Delete the bound region handle from the closure.+ let clo_masked = Set.delete (GBoundRgnCon u) clo++ return ( XLet a (LWithRegion u) xBody'+ , tBody+ , effs'+ , clo_masked)+ ++-- case expression ------------------------------+checkExpM' defs kenv tenv xx@(XCase a xDiscrim alts)+ = do+ -- Check the discriminant.+ (xDiscrim', tDiscrim, effsDiscrim, closDiscrim) + <- checkExpM defs kenv tenv xDiscrim++ -- Split the type into the type constructor names and type parameters.+ -- Also check that it's algebraic data, and not a function or effect+ -- type etc. + (nTyCon, tsArgs)+ <- case takeTyConApps tDiscrim of+ Just (tc, ts)+ | TyConBound (UName n t) <- tc+ , takeResultKind t == kData+ -> return (n, ts)+ + | TyConBound (UPrim n t) <- tc+ , takeResultKind t == kData+ -> return (n, ts)++ _ -> throw $ ErrorCaseDiscrimNotAlgebraic xx tDiscrim++ -- Get the mode of the data type, + -- this tells us how many constructors there are.+ mode + <- case lookupModeOfDataType nTyCon defs of+ Nothing -> throw $ ErrorCaseDiscrimTypeUndeclared xx tDiscrim+ Just m -> return m++ -- Check the alternatives.+ (alts', ts, effss, closs) + <- liftM unzip4+ $ mapM (checkAltM xx defs kenv tenv tDiscrim tsArgs) alts++ -- There must be at least one alternative+ when (null ts)+ $ throw $ ErrorCaseNoAlternatives xx++ -- All alternative result types must be identical.+ let (tAlt : _) = ts+ forM_ ts $ \tAlt' + -> when (not $ equivT tAlt tAlt') + $ throw $ ErrorCaseAltResultMismatch xx tAlt tAlt'++ -- Check for overlapping alternatives.+ let pats = [p | AAlt p _ <- alts]+ let psDefaults = filter isPDefault pats+ let nsCtorsMatched = mapMaybe takeCtorNameOfAlt alts++ -- Alts overlapping because there are multiple defaults.+ when (length psDefaults > 1)+ $ throw $ ErrorCaseOverlapping xx++ -- Alts overlapping because the same ctor is used multiple times.+ when (length (nub nsCtorsMatched) /= length nsCtorsMatched )+ $ throw $ ErrorCaseOverlapping xx++ -- Check for alts overlapping because a default is not last.+ -- Also check there is at least one alternative.+ (case pats of+ [] -> throw $ ErrorCaseNoAlternatives xx++ _ | or $ map isPDefault $ init pats + -> throw $ ErrorCaseOverlapping xx++ | otherwise+ -> return ())++ -- Check the alternatives are exhaustive.+ (case mode of++ -- Small types have some finite number of constructors.+ DataModeSmall nsCtors+ -- If there is a default alternative then we've covered all the+ -- possibiliies. We know this we've also checked for overlap.+ | any isPDefault [p | AAlt p _ <- alts]+ -> return ()++ -- Look for unmatched constructors.+ | nsCtorsMissing <- nsCtors \\ nsCtorsMatched+ , not $ null nsCtorsMissing+ -> throw $ ErrorCaseNonExhaustive xx nsCtorsMissing++ -- All constructors were matched.+ | otherwise + -> return ()++ -- Large types have an effectively infinite number of constructors+ -- (like integer literals), so there needs to be a default alt.+ DataModeLarge + | any isPDefault [p | AAlt p _ <- alts] -> return ()+ | otherwise + -> throw $ ErrorCaseNonExhaustiveLarge xx)++ let effsMatch + = Sum.singleton kEffect + $ crushEffect $ tHeadRead tDiscrim++ return ( XCase a xDiscrim' alts'+ , tAlt+ , Sum.unions kEffect (effsDiscrim : effsMatch : effss)+ , Set.unions (closDiscrim : closs) )+++-- type cast -------------------------------------+-- Weaken an effect, adding in the given terms.+checkExpM' defs kenv tenv xx@(XCast a c@(CastWeakenEffect eff) x1)+ = do + -- Check the effect term.+ kEff <- checkTypeM kenv eff+ when (not $ isEffectKind kEff)+ $ throw $ ErrorMaxeffNotEff xx eff kEff++ -- Check the body.+ (x1', t1, effs, clo) <- checkExpM defs kenv tenv x1++ return ( XCast a c x1'+ , t1+ , Sum.insert eff effs+ , clo)+++-- Weaken a closure, adding in the given terms.+checkExpM' defs kenv tenv xx@(XCast a c@(CastWeakenClosure clo2) x1)+ = do + -- Check the closure term.+ kClo <- checkTypeM kenv clo2+ when (not $ isClosureKind kClo)+ $ throw $ ErrorMaxcloNotClo xx clo2 kClo++ -- The closure supplied to weakclo can only contain Use terms+ -- of region variables.+ clos2+ <- case taggedClosureOfWeakClo clo2 of+ Nothing -> throw $ ErrorMaxcloMalformed xx clo2+ Just clos2' -> return clos2'++ -- Check the body.+ (x1', t1, effs, clos) <- checkExpM defs kenv tenv x1++ return ( XCast a c x1'+ , t1+ , effs+ , Set.union clos clos2)+++-- Purify an effect, given a witness that it is pure.+checkExpM' defs kenv tenv xx@(XCast a c@(CastPurify w) x1)+ = do tW <- checkWitnessM kenv tenv w+ (x1', t1, effs, clo) <- checkExpM defs kenv tenv x1+ + effs' <- case tW of+ TApp (TCon (TyConWitness TwConPure)) effMask+ -> return $ Sum.delete effMask effs+ _ -> throw $ ErrorWitnessNotPurity xx w tW++ return ( XCast a c x1'+ , t1+ , effs'+ , clo)+++-- Forget a closure, given a witness that it is empty.+checkExpM' defs kenv tenv xx@(XCast a c@(CastForget w) x1)+ = do tW <- checkWitnessM kenv tenv w+ (x1', t1, effs, clos) <- checkExpM defs kenv tenv x1++ clos' <- case tW of+ TApp (TCon (TyConWitness TwConEmpty)) cloMask+ -> return $ maskFromTaggedSet + (Sum.singleton kClosure cloMask)+ clos++ _ -> throw $ ErrorWitnessNotEmpty xx w tW++ return ( XCast a c x1'+ , t1+ , effs+ , clos')+++-- Type and witness expressions can only appear as the arguments +-- to applications.+checkExpM' _defs _kenv _tenv xx@(XType _)+ = throw $ ErrorNakedType xx ++checkExpM' _defs _kenv _tenv xx@(XWitness _)+ = throw $ ErrorNakedWitness xx+++-------------------------------------------------------------------------------+-- | Check a case alternative.+checkAltM + :: (Pretty n, Ord n) + => Exp a n -- ^ Whole case expression, for error messages.+ -> DataDefs n -- ^ Data type definitions.+ -> Env n -- ^ Kind environment.+ -> Env n -- ^ Type environment.+ -> Type n -- ^ Type of discriminant.+ -> [Type n] -- ^ Args to type constructor of discriminant.+ -> Alt a n -- ^ Alternative to check.+ -> CheckM a n + ( Alt a n+ , Type n+ , TypeSum n+ , Set (TaggedClosure n))++checkAltM _xx defs kenv tenv _tDiscrim _tsArgs (AAlt PDefault xBody)+ = do (xBody', tBody, effBody, cloBody)+ <- checkExpM defs kenv tenv xBody++ return ( AAlt PDefault xBody'+ , tBody+ , effBody+ , cloBody)++checkAltM xx defs kenv tenv tDiscrim tsArgs (AAlt (PData uCon bsArg) xBody)+ = do + -- Take the type of the constructor and instantiate it with the + -- type arguments we got from the discriminant. + -- If the ctor type doesn't instantiate then it won't have enough foralls + -- on the front, which should have been checked by the def checker.+ let tCtor = typeOfBound uCon+ tCtor_inst + <- case instantiateTs tCtor tsArgs of+ Nothing -> throw $ ErrorCaseCannotInstantiate xx tDiscrim tCtor+ Just t -> return t+ + -- Split the constructor type into the field and result types.+ let (tsFields_ctor, tResult) + = takeTFunArgResult tCtor_inst++ -- The result type of the constructor must match the discriminant type.+ -- If it doesn't then the constructor in the pattern probably isn't for+ -- the discriminant type.+ when (not $ equivT tDiscrim tResult)+ $ throw $ ErrorCaseDiscrimTypeMismatch xx tDiscrim tResult++ -- There must be at least as many fields as variables in the pattern.+ -- It's ok to bind less fields than provided by the constructor.+ when (length tsFields_ctor < length bsArg)+ $ throw $ ErrorCaseTooManyBinders xx uCon + (length tsFields_ctor)+ (length bsArg)++ -- Merge the field types we get by instantiating the constructor+ -- type with possible annotations from the source program.+ -- If the annotations don't match, then we throw an error.+ tsFields <- zipWithM (mergeAnnot xx)+ (map typeOfBind bsArg)+ tsFields_ctor ++ -- Extend the environment with the field types.+ let bsArg' = zipWith replaceTypeOfBind tsFields bsArg+ let tenv' = Env.extends bsArg' tenv+ + -- Check the body in this new environment.+ (xBody', tBody, effsBody, closBody)+ <- checkExpM defs kenv tenv' xBody++ -- Cut closure terms due to locally bound value vars.+ -- This also lowers deBruijn indices in un-cut closure terms.+ let closBody_cut + = Set.fromList+ $ mapMaybe (cutTaggedClosureXs bsArg')+ $ Set.toList closBody++ return ( AAlt (PData uCon bsArg') xBody'+ , tBody+ , effsBody+ , closBody_cut)+++-- | Merge a type annotation on a pattern field with a type we get by+-- instantiating the constructor type.+mergeAnnot :: Eq n => Exp a n -> Type n -> Type n -> CheckM a n (Type n)+mergeAnnot xx tAnnot tActual+ -- Annotation is bottom, so just use the real type.+ | isBot tAnnot = return tActual++ -- Annotation matches actual type, all good.+ | tAnnot == tActual = return tActual++ -- Annotation does not match actual type.+ | otherwise + = throw $ ErrorCaseFieldTypeMismatch xx tAnnot tActual+++-------------------------------------------------------------------------------+-- | Check the set of witness bindings bound in a letregion for conflicts.+checkWitnessBindsM :: Ord n => Exp a n -> Bound n -> [Bind n] -> CheckM a n ()+checkWitnessBindsM xx nRegion bsWits+ = mapM_ (checkWitnessBindM xx nRegion bsWits) bsWits+++checkWitnessBindM + :: Ord n + => Exp a n+ -> Bound n -- ^ Region variable bound in the letregion.+ -> [Bind n] -- ^ Other witness bindings in the same set.+ -> Bind n -- ^ The witness binding to check.+ -> CheckM a n ()++checkWitnessBindM xx uRegion bsWit bWit+ = let btsWit + = [(typeOfBind b, b) | b <- bsWit]++ -- Check the argument of a witness type is for the region we're+ -- introducing here.+ checkWitnessArg t+ = case t of+ TVar u'+ | uRegion /= u' -> throw $ ErrorLetRegionWitnessOther xx uRegion bWit+ | otherwise -> return ()++ TCon (TyConBound u')+ | uRegion /= u' -> throw $ ErrorLetRegionWitnessOther xx uRegion bWit+ | otherwise -> return ()++ -- The parser should ensure the right of a witness is a + -- constructor or variable.+ _ -> throw $ ErrorLetRegionWitnessInvalid xx bWit++ in case typeOfBind bWit of+ TApp (TCon (TyConWitness TwConGlobal)) t2+ -> checkWitnessArg t2++ TApp (TCon (TyConWitness TwConConst)) t2+ | Just bConflict <- L.lookup (tMutable t2) btsWit+ -> throw $ ErrorLetRegionWitnessConflict xx bWit bConflict+ | otherwise -> checkWitnessArg t2++ TApp (TCon (TyConWitness TwConMutable)) t2+ | Just bConflict <- L.lookup (tConst t2) btsWit+ -> throw $ ErrorLetRegionWitnessConflict xx bWit bConflict+ | otherwise -> checkWitnessArg t2++ TApp (TCon (TyConWitness TwConLazy)) t2+ | Just bConflict <- L.lookup (tManifest t2) btsWit+ -> throw $ ErrorLetRegionWitnessConflict xx bWit bConflict+ | otherwise -> checkWitnessArg t2++ TApp (TCon (TyConWitness TwConManifest)) t2+ | Just bConflict <- L.lookup (tLazy t2) btsWit+ -> throw $ ErrorLetRegionWitnessConflict xx bWit bConflict+ | otherwise -> checkWitnessArg t2++ _ -> throw $ ErrorLetRegionWitnessInvalid xx bWit+++-------------------------------------------------------------------------------+-- | Check a type in the exp checking monad.+checkTypeM :: (Ord n, Pretty n) => Env n -> Type n -> CheckM a n (Kind n)++checkTypeM kenv tt+ = case T.checkType kenv tt of+ Left err -> throw $ ErrorType err+ Right k -> return k+++-------------------------------------------------------------------------------+-- | Check the type annotation of a let bound variable against the type+-- inferred for the right of the binding.+-- If the annotation is Bot then we just replace the annotation,+-- otherwise it must match that for the right of the binding.+checkLetBindOfTypeM + :: (Eq n, Ord n, Pretty n) + => Exp a n + -> Env n -- Kind environment. + -> Env n -- Type environment.+ -> Type n + -> Bind n + -> CheckM a n (Bind n, Kind n)++checkLetBindOfTypeM xx kenv _tenv tRight b+ -- If the annotation is Bot then just replace it.+ | isBot (typeOfBind b)+ = do k <- checkTypeM kenv tRight+ return ( replaceTypeOfBind tRight b + , k)++ -- The type of the binder must match that of the right of the binding.+ | not $ equivT (typeOfBind b) tRight+ = throw $ ErrorLetMismatch xx b tRight++ | otherwise+ = do k <- checkTypeM kenv (typeOfBind b)+ return (b, k)+
+ DDC/Core/Check/CheckWitness.hs view
@@ -0,0 +1,201 @@++-- | Type checker for witness expressions.+module DDC.Core.Check.CheckWitness+ ( checkWitness+ , typeOfWitness+ , typeOfWiCon+ , typeOfWbCon++ , CheckM+ , checkWitnessM)+where+import DDC.Core.Exp+import DDC.Core.Pretty+import DDC.Core.Check.Error+import DDC.Core.Check.ErrorMessage ()+import DDC.Type.Transform.SubstituteT+import DDC.Type.Compounds+import DDC.Type.Predicates+import DDC.Type.Equiv+import DDC.Type.Transform.LiftT+import DDC.Type.Sum as Sum+import DDC.Type.Env (Env)+import DDC.Type.Check.Monad (result, throw)+import DDC.Base.Pretty ()+import qualified DDC.Type.Env as Env+import qualified DDC.Type.Check as T+import qualified DDC.Type.Check.Monad as G+++-- | Type checker monad. +-- Used to manage type errors.+type CheckM a n = G.CheckM (Error a n)+++-- Wrappers --------------------------------------------------------------------+-- | Check a witness.+-- +-- If it's good, you get a new version with types attached to all the bound+-- variables, as well as the type of the overall witness.+--+-- If it's bad, you get a description of the error.+--+-- The returned expression has types attached to all variable occurrences, +-- so you can call `typeOfWitness` on any open subterm.+--+checkWitness+ :: (Ord n, Pretty n)+ => Env n -- ^ Kind Environment.+ -> Env n -- ^ Type Environment.+ -> Witness n -- ^ Witness to check.+ -> Either (Error a n) (Type n)++checkWitness kenv tenv xx+ = result $ checkWitnessM kenv tenv xx+++-- | Like `checkWitness`, but check in an empty environment.+--+-- As this function is not given an environment, the types of free variables+-- must be attached directly to the bound occurrences.+-- This attachment is performed by `checkWitness` above.+--+typeOfWitness + :: (Ord n, Pretty n) + => Witness n + -> Either (Error a n) (Type n)+typeOfWitness ww + = result + $ checkWitnessM Env.empty Env.empty ww+++------------------------------------------------------------------------------+-- | Like `checkWitness` but using the `CheckM` monad to manage errors.+checkWitnessM + :: (Ord n, Pretty n)+ => Env n -- ^ Kind environment.+ -> Env n -- ^ Type environment.+ -> Witness n -- ^ Witness to check.+ -> CheckM a n (Type n)++checkWitnessM _kenv tenv (WVar u)+ = do let tBound = typeOfBound u+ let mtEnv = Env.lookup u tenv++ let mkResult+ -- When annotation on the bound is bot,+ -- then use the type from the environment.+ | Just tEnv <- mtEnv+ , isBot tBound+ = return tEnv++ -- The bound has an explicit type annotation,+ -- which matches the one from the environment.+ -- + -- When the bound is a deBruijn index we need to lift the+ -- annotation on the original binder through any lambdas+ -- between the binding occurrence and the use.+ | Just tEnv <- mtEnv+ , UIx i _ <- u+ , equivT tBound (liftT (i + 1) tEnv) + = return tBound++ -- The bound has an explicit type annotation,+ -- which matches the one from the environment.+ | Just tEnv <- mtEnv+ , equivT tBound tEnv+ = return tEnv++ -- The bound has an explicit type annotation,+ -- which does not match the one from the environment.+ -- This shouldn't happen because the parser doesn't add non-bot+ -- annotations to bound variables.+ | Just tEnv <- mtEnv+ = throw $ ErrorVarAnnotMismatch u tEnv++ -- Variable not in environment, so use annotation.+ -- This happens when checking open terms.+ | otherwise+ = return tBound+ + tResult <- mkResult+ return tResult+++checkWitnessM _kenv _tenv (WCon wc)+ = return $ typeOfWiCon wc++ +-- value-type application+checkWitnessM kenv tenv ww@(WApp w1 (WType t2))+ = do t1 <- checkWitnessM kenv tenv w1+ k2 <- checkTypeM kenv t2+ case t1 of+ TForall b11 t12+ | typeOfBind b11 == k2+ -> return $ substituteT b11 t2 t12++ | otherwise -> throw $ ErrorWAppMismatch ww (typeOfBind b11) k2+ _ -> throw $ ErrorWAppNotCtor ww t1 t2++-- witness-witness application+checkWitnessM kenv tenv ww@(WApp w1 w2)+ = do t1 <- checkWitnessM kenv tenv w1+ t2 <- checkWitnessM kenv tenv w2+ case t1 of+ TApp (TApp (TCon (TyConWitness TwConImpl)) t11) t12+ | t11 == t2 + -> return t12++ | otherwise -> throw $ ErrorWAppMismatch ww t11 t2+ _ -> throw $ ErrorWAppNotCtor ww t1 t2++-- witness joining+checkWitnessM kenv tenv ww@(WJoin w1 w2)+ = do t1 <- checkWitnessM kenv tenv w1+ t2 <- checkWitnessM 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])++ ( TApp (TCon (TyConWitness TwConEmpty)) clo1+ , TApp (TCon (TyConWitness TwConEmpty)) clo2)+ -> return $ TApp (TCon (TyConWitness TwConEmpty))+ (TSum $ Sum.fromList kClosure [clo1, clo2])++ _ -> throw $ ErrorCannotJoin ww w1 t1 w2 t2++-- embedded types+checkWitnessM kenv _tenv (WType t)+ = checkTypeM kenv t+ ++-- | Take the type of a witness constructor.+typeOfWiCon :: WiCon n -> Type n+typeOfWiCon wc+ = case wc of+ WiConBuiltin wb -> typeOfWbCon wb+ WiConBound u -> typeOfBound u+++-- | Take the type of a builtin witness constructor.+typeOfWbCon :: WbCon -> Type n+typeOfWbCon wb+ = case wb of+ WbConPure -> tPure (tBot kEffect)+ WbConEmpty -> tEmpty (tBot kClosure)+ WbConUse -> tForall kRegion $ \r -> tGlobal r `tImpl` (tEmpty $ tUse r)+ WbConRead -> tForall kRegion $ \r -> tConst r `tImpl` (tPure $ tRead r)+ WbConAlloc -> tForall kRegion $ \r -> tConst r `tImpl` (tPure $ tAlloc r)+++-- checkType ------------------------------------------------------------------+-- | Check a type in the exp checking monad.+checkTypeM :: (Ord n, Pretty n) => Env n -> Type n -> CheckM a n (Kind n)+checkTypeM kenv tt+ = case T.checkType kenv tt of+ Left err -> throw $ ErrorType err+ Right k -> return k+
+ DDC/Core/Check/Error.hs view
@@ -0,0 +1,308 @@+-- | Errors produced when checking core expressions.+module DDC.Core.Check.Error+ (Error(..))+where+import DDC.Core.Exp+import qualified DDC.Type.Check as T+++-- | All the things that can go wrong when type checking an expression+-- or witness.+data Error a n+ -- | Found a kind error when checking a type.+ = ErrorType+ { errorTypeError :: T.Error n }++ -- | Found a malformed expression, + -- and we don't have a more specific diagnosis.+ | ErrorMalformedExp+ { errorChecking :: Exp a n }++ -- | Found a malformed type,+ -- and we don't have a more specific diagnosis.+ | ErrorMalformedType+ { errorChecking :: Exp a n+ , errorType :: Type n }++ -- | Found a naked `XType` that wasn't the argument of an application.+ | ErrorNakedType+ { errorChecking :: Exp a n }++ -- | Found a naked `XWitness` that wasn't the argument of an application.+ | ErrorNakedWitness+ { errorChecking :: Exp a n }++ -- Var --------------------------------------------+ -- | A bound occurrence of a variable who's type annotation does not match+ -- the corresponding annotation in the environment.+ | ErrorVarAnnotMismatch+ { errorBound :: Bound n+ , errorTypeEnv :: Type n }++ -- Application ------------------------------------+ -- | A function application where the parameter and argument don't match.+ | ErrorAppMismatch+ { errorChecking :: Exp a n+ , errorParamType :: Type n+ , errorArgType :: Type n }++ -- | Tried to apply something that is not a function.+ | ErrorAppNotFun+ { errorChecking :: Exp a n+ , errorNotFunType :: Type n+ , errorArgType :: Type n }+++ -- Lambda -----------------------------------------+ -- | A type abstraction that tries to shadow a type variable that is+ -- already in the environment.+ | ErrorLamShadow+ { errorChecking :: Exp a n + , errorBind :: Bind n }++ -- | A type or witness abstraction where the body has a visible side effect.+ | ErrorLamNotPure+ { errorChecking :: Exp a n+ , errorEffect :: Effect n }++ -- | A value function where the parameter does not have data kind.+ | ErrorLamBindNotData+ { errorChecking :: Exp a n + , errorType :: Type n+ , errorKind :: Kind n }++ -- | An abstraction where the body does not have data kind.+ | ErrorLamBodyNotData+ { errorChecking :: Exp a n+ , errorBind :: Bind n+ , errorType :: Type n+ , errorKind :: Kind n }+++ -- Let --------------------------------------------+ -- | A let-expression where the type of the binder does not match the right+ -- of the binding.+ | ErrorLetMismatch+ { errorChecking :: Exp a n+ , errorBind :: Bind n+ , errorType :: Type n }++ -- | A let-expression where the right of the binding does not have data kind.+ | ErrorLetBindingNotData+ { errorChecking :: Exp a n+ , errorBind :: Bind n+ , errorKind :: Kind n }++ -- | A let-expression where the body does not have data kind.+ | ErrorLetBodyNotData+ { errorChecking :: Exp a n+ , errorType :: Type n+ , 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.+ | ErrorLetrecBindingNotLambda+ { errorChecking :: Exp a n + , errorExp :: Exp a n }+++ -- Letregion --------------------------------------+ -- | A letregion-expression where the bound variable does not have+ -- region kind.+ | ErrorLetRegionNotRegion+ { errorChecking :: Exp a n+ , errorBind :: Bind n+ , errorKind :: Kind n }++ -- | A letregion-expression that tried to shadow a pre-existing named+ -- region variable.+ | ErrorLetRegionRebound+ { errorChecking :: Exp a n+ , errorBind :: Bind n }++ -- | A letregion-expression where the bound region variable is free in+ -- the type of the body.+ | ErrorLetRegionFree+ { errorChecking :: Exp a n+ , errorBind :: Bind n+ , errorType :: Type n }++ -- | A letregion-expression that tried to create a witness with an + -- invalid type.+ | ErrorLetRegionWitnessInvalid+ { errorChecking :: Exp a n+ , errorBind :: Bind n }++ -- | A letregion-expression that tried to create conflicting witnesses.+ | ErrorLetRegionWitnessConflict+ { errorChecking :: Exp a n+ , errorBindWitness1 :: Bind n+ , errorBindWitness2 :: Bind n }++ -- | A letregion-expression where a bound witnesses was not for the+ -- the region variable being introduced.+ | ErrorLetRegionWitnessOther+ { errorChecking :: Exp a n+ , errorBoundRegion :: Bound n+ , errorBindWitness :: Bind n }++ -- | A withregion-expression where the handle does not have region kind.+ | ErrorWithRegionNotRegion+ { errorChecking :: Exp a n+ , errorBound :: Bound n+ , errorKind :: Kind n }+++ -- Witnesses --------------------------------------+ -- | A witness application where the argument type does not match+ -- the parameter type.+ | ErrorWAppMismatch+ { errorWitness :: Witness n+ , errorParamType :: Type n+ , errorArgType :: Type n }++ -- | Tried to perform a witness application with a non-witness.+ | ErrorWAppNotCtor+ { errorWitness :: Witness n+ , errorNotFunType :: Type n+ , errorArgType :: Type n }++ -- | An invalid witness join.+ | ErrorCannotJoin+ { errorWitness :: Witness n+ , errorWitnessLeft :: Witness n+ , errorTypeLeft :: Type n+ , errorWitnessRight :: Witness n+ , errorTypeRight :: Type n }++ -- | A witness provided for a purify cast that does not witness purity.+ | ErrorWitnessNotPurity+ { errorChecking :: Exp a n+ , errorWitness :: Witness n+ , errorType :: Type n }++ -- | A witness provided for a forget cast that does not witness emptiness.+ | ErrorWitnessNotEmpty+ { errorChecking :: Exp a n+ , errorWitness :: Witness n+ , errorType :: Type n }+++ -- Case Expressions -------------------------------+ -- | A case-expression where the discriminant type is not algebraic.+ | ErrorCaseDiscrimNotAlgebraic+ { errorChecking :: Exp a n+ , errorTypeDiscrim :: Type n }++ -- | A case-expression where the discriminant type is not in our set+ -- of data type declarations.+ | ErrorCaseDiscrimTypeUndeclared+ { errorChecking :: Exp a n + , errorTypeDiscrim :: Type n }++ -- | A case-expression with no alternatives.+ | ErrorCaseNoAlternatives+ { errorChecking :: Exp a n }++ -- | A case-expression where the alternatives don't cover all the+ -- possible data constructors.+ | ErrorCaseNonExhaustive+ { errorChecking :: Exp a n+ , errorCtorNamesMissing :: [n] }++ -- | A case-expression where the alternatives don't cover all the+ -- possible constructors, and the type has too many data constructors+ -- to list.+ | ErrorCaseNonExhaustiveLarge+ { errorChecking :: Exp a n }++ -- | A case-expression with overlapping alternatives.+ | ErrorCaseOverlapping+ { errorChecking :: Exp a n }++ -- | A case-expression where one of the patterns has too many binders.+ | ErrorCaseTooManyBinders+ { errorChecking :: Exp a n+ , errorCtorBound :: Bound n+ , errorCtorFields :: Int+ , errorPatternFields :: Int }++ -- | A case-expression where the pattern types could not be instantiated+ -- with the arguments of the discriminant type.+ | ErrorCaseCannotInstantiate+ { errorChecking :: Exp a n+ , errorTypeCtor :: Type n+ , errorTypeDiscrim :: Type n }++ -- | A case-expression where the type of the discriminant does not match+ -- the type of the pattern.+ | ErrorCaseDiscrimTypeMismatch+ { errorChecking :: Exp a n+ , errorTypeDiscrim :: Type n+ , errorTypePattern :: Type n }++ -- | A case-expression where the annotation on a pattern variable binder+ -- does not match the field type of the constructor.+ | ErrorCaseFieldTypeMismatch+ { errorChecking :: Exp a n+ , errorTypeAnnot :: Type n+ , errorTypeField :: Type n }++ -- | A case-expression where the result types of the alternatives are not+ -- identical.+ | ErrorCaseAltResultMismatch+ { errorChecking :: Exp a n+ , errorAltType1 :: Type n+ , errorAltType2 :: Type n }+++ -- Casts ------------------------------------------+ -- | A maxeff-cast where the type provided does not have effect kind.+ | ErrorMaxeffNotEff+ { errorChecking :: Exp a n+ , errorEffect :: Effect n+ , errorKind :: Kind n }++ -- | A maxclo-cast where the type provided does not have closure kind.+ | ErrorMaxcloNotClo+ { errorChecking :: Exp a n+ , errorClosure :: Closure n+ , errorKind :: Kind n }++ -- | A maxclo-case where the closure provided is malformed. + -- It can only contain `Use` terms.+ | ErrorMaxcloMalformed+ { errorChecking :: Exp a n + , errorClosure :: Closure n }+ deriving (Show)+
+ DDC/Core/Check/ErrorMessage.hs view
@@ -0,0 +1,345 @@+{-# OPTIONS_HADDOCK hide #-}+-- | Errors produced when checking core expressions.+module DDC.Core.Check.ErrorMessage+ (Error(..))+where+import DDC.Core.Pretty+import DDC.Core.Check.Error+import DDC.Type.Compounds+++instance (Pretty n, Eq n) => Pretty (Error a n) where+ ppr err+ = case err of+ ErrorType err' -> ppr err'++ ErrorMalformedExp xx+ -> vcat [ text "Malformed expression: " <> align (ppr xx) ]+ + ErrorMalformedType xx tt+ -> vcat [ text "Found malformed type: " <> ppr tt+ , empty+ , text "with: " <> align (ppr xx) ]++ ErrorNakedType xx+ -> vcat [ text "Found naked type in core program."+ , empty+ , text "with: " <> align (ppr xx) ]++ ErrorNakedWitness xx+ -> vcat [ text "Found naked witness in core program."+ , empty+ , text "with: " <> align (ppr xx) ]++ -- Variable ---------------------------------------+ ErrorVarAnnotMismatch u t+ -> vcat [ text "Type mismatch in annotation."+ , text " Variable: " <> ppr u+ , text " has annotation: " <> (ppr $ typeOfBound u)+ , text " which conflicts with: " <> ppr t+ , text " from environment." ]+++ -- Application ------------------------------------+ ErrorAppMismatch xx t1 t2+ -> vcat [ text "Type mismatch in application." + , text " Function expects: " <> ppr t1+ , text " but argument is: " <> ppr t2+ , empty+ , text "with: " <> align (ppr xx) ]+ + ErrorAppNotFun xx t1 t2+ -> vcat [ text "Cannot apply non-function"+ , text " of type: " <> ppr t1+ , text " to argument of type: " <> ppr t2 + , empty+ , text "with: " <> align (ppr xx) ]+++ -- Lambda -----------------------------------------+ ErrorLamShadow xx b+ -> vcat [ text "Cannot shadow named spec variable."+ , text " binder: " <> ppr b+ , text " is already in the environment."+ , text "with: " <> align (ppr xx) ]++ ErrorLamNotPure xx eff+ -> vcat [ text "Impure type abstraction"+ , text " has effect: " <> ppr eff+ , empty+ , text "with: " <> align (ppr xx) ]+ + + ErrorLamBindNotData xx t1 k1+ -> vcat [ text "Function parameter does not have data kind."+ , text " The function parameter:" <> ppr t1+ , text " has kind: " <> ppr k1+ , text " but it must be: *"+ , empty+ , text "with: " <> align (ppr xx) ]++ ErrorLamBodyNotData xx b1 t2 k2+ -> vcat [ text "Result of function does not have data kind."+ , text " In function with binder: " <> ppr b1+ , text " the result has type: " <> ppr t2+ , text " with kind: " <> ppr k2+ , text " but it must be: *"+ , empty+ , text "with: " <> align (ppr xx) ]+++ -- Let --------------------------------------------+ ErrorLetMismatch xx b t+ -> vcat [ text "Type mismatch in let-binding."+ , text " The binder: " <> ppr (binderOfBind b)+ , text " has type: " <> ppr (typeOfBind b)+ , text " but the body has type: " <> ppr t+ , empty+ , text "with: " <> align (ppr xx) ]++ ErrorLetBindingNotData xx b k+ -> vcat [ text "Let binding does not have data kind."+ , text " The binding for: " <> ppr (binderOfBind b)+ , text " has type: " <> ppr (typeOfBind b)+ , text " with kind: " <> ppr k+ , text " but it must be: * "+ , empty+ , text "with: " <> align (ppr xx) ]++ ErrorLetBodyNotData xx t k+ -> vcat [ text "Let body does not have data kind."+ , text " Body of let has type: " <> ppr t+ , text " with kind: " <> ppr k+ , text " but it must be: * "+ , empty+ , 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."+ , text " This is not one: " <> ppr x+ , empty+ , text "with: " <> align (ppr xx) ]+++ -- Letregion --------------------------------------+ ErrorLetRegionNotRegion xx b k+ -> vcat [ text "Letregion binder does not have region kind."+ , text " Region binder: " <> ppr b+ , text " has kind: " <> ppr k+ , text " but is must be: %" + , empty+ , text "with: " <> align (ppr xx) ]++ ErrorLetRegionRebound xx b+ -> vcat [ text "Region variable shadows existing one."+ , text " Region variable: " <> ppr b+ , text " is already in environment"+ , empty+ , text "with: " <> align (ppr xx) ]++ ErrorLetRegionFree xx b t+ -> vcat [ text "Region variable escapes scope of letregion."+ , text " The region variable: " <> ppr b+ , text " is free in the body type: " <> ppr t+ , empty+ , text "with: " <> align (ppr xx) ]+ + ErrorLetRegionWitnessInvalid xx b+ -> vcat [ text "Invalid witness type with letregion."+ , text " The witness: " <> ppr b+ , text " cannot be created with a letregion"+ , empty+ , text "with: " <> align (ppr xx) ]++ ErrorLetRegionWitnessConflict xx b1 b2+ -> vcat [ text "Conflicting witness types with letregion."+ , text " Witness binding: " <> ppr b1+ , text " conflicts with: " <> ppr b2 + , empty+ , text "with: " <> align (ppr xx) ]++ ErrorLetRegionWitnessOther xx b1 b2+ -> vcat [ text "Witness type is not for bound region."+ , text " letregion binds: " <> ppr b1+ , text " but witness type is: " <> ppr b2+ , empty+ , text "with: " <> align (ppr xx) ]++ ErrorWithRegionNotRegion xx u k+ -> vcat [ text "Withregion handle does not have region kind."+ , text " Region var or ctor: " <> ppr u+ , text " has kind: " <> ppr k+ , text " but it must be: %"+ , empty+ , text "with: " <> align (ppr xx) ]++ -- Witnesses --------------------------------------+ ErrorWAppMismatch ww t1 t2+ -> vcat [ text "Type mismatch in witness application."+ , text " Constructor expects: " <> ppr t1+ , text " but argument is: " <> ppr t2+ , empty+ , text "with: " <> align (ppr ww) ]++ ErrorWAppNotCtor ww t1 t2+ -> vcat [ text "Type cannot apply non-constructor witness"+ , text " of type: " <> ppr t1+ , text " to argument of type: " <> ppr t2+ , empty+ , text "with: " <> align (ppr ww) ]++ ErrorCannotJoin ww w1 t1 w2 t2+ -> vcat [ text "Cannot join witnesses."+ , text " Cannot join: " <> ppr w1+ , text " of type: " <> ppr t1+ , text " with witness: " <> ppr w2+ , text " of type: " <> ppr t2+ , empty+ , text "with: " <> align (ppr ww) ]++ ErrorWitnessNotPurity xx w t+ -> vcat [ text "Witness for a purify does not witness purity."+ , text " Witness: " <> ppr w+ , text " has type: " <> ppr t+ , empty+ , text "with: " <> align (ppr xx) ]++ ErrorWitnessNotEmpty xx w t+ -> vcat [ text "Witness for a forget does not witness emptiness."+ , text " Witness: " <> ppr w+ , text " has type: " <> ppr t+ , empty+ , text "with: " <> align (ppr xx) ]+++ -- Case Expressions -------------------------------+ ErrorCaseDiscrimNotAlgebraic xx tDiscrim+ -> vcat [ text "Discriminant of case expression is not algebraic data."+ , text " Discriminant type: " <> ppr tDiscrim+ , empty+ , text "with: " <> align (ppr xx) ]+ + ErrorCaseDiscrimTypeUndeclared xx tDiscrim+ -> vcat [ text "Type of discriminant does not have a data declaration."+ , text " Discriminant type: " <> ppr tDiscrim+ , empty+ , text "with: " <> align (ppr xx) ]++ ErrorCaseNoAlternatives xx+ -> vcat [ text "Case expression does not have any alternatives."+ , empty+ , text "with: " <> align (ppr xx) ]++ ErrorCaseNonExhaustive xx ns+ -> vcat [ text "Case alternatives are non-exhaustive."+ , text " Constructors not matched: " + <> (sep $ punctuate comma $ map ppr ns)+ , empty+ , text "with: " <> align (ppr xx) ]++ ErrorCaseNonExhaustiveLarge xx+ -> vcat [ text "Case alternatives are non-exhaustive."+ , empty+ , text "with: " <> align (ppr xx) ]++ ErrorCaseOverlapping xx+ -> vcat [ text "Case alternatives are overlapping."+ , empty+ , text "with: " <> align (ppr xx) ]++ ErrorCaseTooManyBinders xx uCtor iCtorFields iPatternFields+ -> vcat [ text "Pattern has more binders than there are fields in the constructor."+ , text " Contructor: " <> ppr uCtor+ , text " has: " <> ppr iCtorFields + <+> text "fields"+ , text " but there are: " <> ppr iPatternFields + <+> text "binders in the pattern" + , empty+ , text "with: " <> align (ppr xx) ]++ ErrorCaseCannotInstantiate xx tCtor tDiscrim+ -> vcat [ text "Cannot instantiate constructor type with discriminant type args."+ , text " Either the constructor has an invalid type,"+ , text " or the type of the discriminant does not match the type of the pattern."+ , text " Constructor type: " <> ppr tCtor+ , text " Discriminant type: " <> ppr tDiscrim+ , empty+ , text "with: " <> align (ppr xx) ]++ ErrorCaseDiscrimTypeMismatch xx tDiscrim tPattern+ -> vcat [ text "Discriminant type does not match result of pattern type."+ , text " Discriminant type: " <> ppr tDiscrim+ , text " Pattern type: " <> ppr tPattern+ , empty+ , text "with: " <> align (ppr xx) ]++ ErrorCaseFieldTypeMismatch xx tAnnot tField+ -> vcat [ text "Annotation on pattern variable does not match type of field."+ , text " Annotation type: " <> ppr tAnnot+ , text " Field type: " <> ppr tField+ , empty+ , text "with: " <> align (ppr xx) ]++ ErrorCaseAltResultMismatch xx t1 t2+ -> vcat [ text "Mismatch in alternative result types."+ , text " Type of alternative: " <> ppr t1+ , text " does not match: " <> ppr t2+ , empty+ , text "with: " <> align (ppr xx) ]+++ -- Casts ------------------------------------------+ ErrorMaxeffNotEff xx eff k+ -> vcat [ text "Type provided for a 'maxeff' does not have effect kind."+ , text " Type: " <> ppr eff+ , text " has kind: " <> ppr k+ , empty+ , text "with: " <> align (ppr xx) ]++ ErrorMaxcloNotClo xx clo k+ -> vcat [ text "Type provided for a 'maxclo' does not have closure kind."+ , text " Type: " <> ppr clo+ , text " has kind: " <> ppr k+ , empty+ , text "with: " <> align (ppr xx) ]++ ErrorMaxcloMalformed xx clo+ -> vcat [ text "Type provided for a 'maxclo' is malformed."+ , text " Closure: " <> ppr clo+ , text " can only contain 'Use' terms."+ , empty+ , text "with: " <> align (ppr xx) ]+
+ DDC/Core/Check/TaggedClosure.hs view
@@ -0,0 +1,223 @@++module DDC.Core.Check.TaggedClosure+ ( TaggedClosure(..)+ , closureOfTagged+ , closureOfTaggedSet+ , taggedClosureOfValBound+ , taggedClosureOfTyArg+ , taggedClosureOfWeakClo+ , maskFromTaggedSet+ , cutTaggedClosureX+ , cutTaggedClosureXs+ , cutTaggedClosureT)+where+import DDC.Type.Transform.LowerT+import DDC.Type.Transform.Trim+import DDC.Type.Compounds+import DDC.Type.Predicates+import DDC.Type.Pretty+import DDC.Type.Exp+import Control.Monad+import Data.Maybe+import Data.Set (Set)+import qualified DDC.Type.Sum as Sum+import qualified Data.Set as Set+++-- | A closure-term tagged with the bound variable that the term is due to.+data TaggedClosure n+ -- | Term due to a free value variable.+ = GBoundVal (Bound n) (TypeSum n)++ -- | Term due to a free region variable.+ | GBoundRgnVar (Bound n)++ -- | Term due to a region handle.+ | GBoundRgnCon (Bound n)+ deriving Show+++instance Eq n => Eq (TaggedClosure n) where+ (==) (GBoundVal u1 _) (GBoundVal u2 _) = u1 == u2+ (==) (GBoundRgnVar u1) (GBoundRgnVar u2) = u1 == u2+ (==) (GBoundRgnCon u1) (GBoundRgnCon u2) = u1 == u2+ (==) _ _ = False+ ++instance Ord n => Ord (TaggedClosure n) where+ compare g1 g2 = compare (ordify g1) (ordify g2)+ where + ordify gg+ = case gg of+ GBoundVal u _ -> (0, u) :: (Int, Bound n)+ GBoundRgnVar u -> (1, u)+ GBoundRgnCon u -> (2, u)+++instance (Eq n, Pretty n) => Pretty (TaggedClosure n) where+ ppr cc+ = case cc of+ GBoundVal u clos -> text "CLOVAL " <+> ppr u <+> text ":" <+> ppr clos+ GBoundRgnVar u -> text "CLORGNVAR" <+> ppr u+ GBoundRgnCon u -> text "CLORGNCON" <+> ppr u+++instance LowerT TaggedClosure where+ lowerAtDepthT n d cc+ = let down = lowerAtDepthT n d+ in case cc of+ GBoundVal u ts -> GBoundVal (down u) (down ts)+ GBoundRgnVar u1 -> GBoundRgnVar (down u1)+ GBoundRgnCon u2 -> GBoundRgnCon u2+++-- | Convert a tagged clousure to a regular closure by dropping the tag variables.+closureOfTagged :: TaggedClosure n -> Closure n+closureOfTagged gg+ = case gg of+ GBoundVal _ clos -> TSum $ clos+ GBoundRgnVar u -> tUse (TVar u)+ GBoundRgnCon u -> tUse (TCon (TyConBound u))+++-- | Convert a set of tagged closures to a regular closure by dropping the+-- tag variables.+closureOfTaggedSet :: Ord n => Set (TaggedClosure n) -> Closure n+closureOfTaggedSet clos+ = TSum $ Sum.fromList kClosure + $ map closureOfTagged + $ Set.toList clos+++-- | Yield the tagged closure of a value variable.+taggedClosureOfValBound + :: (Ord n, Pretty n) + => Bound n -> TaggedClosure n++taggedClosureOfValBound u+ = GBoundVal u + $ Sum.singleton kClosure + $ (let clo = tDeepUse $ typeOfBound u+ in fromMaybe clo (trimClosure clo))+++-- | Yield the tagged closure of a type argument.+taggedClosureOfTyArg + :: (Ord n, Pretty n) + => Type n -> Set (TaggedClosure n)++taggedClosureOfTyArg tt+ = case tt of+ TVar u+ | isRegionKind (typeOfBound u)+ -> Set.singleton $ GBoundRgnVar u++ TCon (TyConBound u)+ | isRegionKind (typeOfBound u)+ -> Set.singleton $ GBoundRgnCon u++ _ -> Set.empty+++-- | Convert the closure provided as a 'weakclo' to tagged form.+-- Only terms of form `Use r` can be converted.+taggedClosureOfWeakClo + :: (Ord n, Pretty n)+ => Closure n -> Maybe (Set (TaggedClosure n))++taggedClosureOfWeakClo clo+ = liftM Set.fromList+ $ sequence+ $ map convert + $ Sum.toList $ Sum.singleton kClosure clo++ where convert c+ = case takeTyConApps c of+ Just (TyConSpec TcConUse, [TVar u])+ -> Just $ GBoundRgnVar u++ Just (TyConSpec TcConUse, [TCon (TyConBound u)])+ -> Just $ GBoundRgnVar u++ _ -> Nothing+++-- | Mask a closure term from a tagged closure.+--+-- This is used for the `forget` cast.+maskFromTaggedSet + :: Ord n + => TypeSum n + -> Set (TaggedClosure n) -> Set (TaggedClosure n)+maskFromTaggedSet ts1 set+ = Set.fromList $ mapMaybe mask $ Set.toList set++ where mask gg+ = case gg of+ GBoundVal u ts2 + -> Just $ GBoundVal u $ ts2 `Sum.difference` ts1++ GBoundRgnVar u+ | Sum.elem (tUse (TVar u)) ts1+ -> Nothing+ | otherwise -> Just gg++ GBoundRgnCon u+ | Sum.elem (tUse (TCon (TyConBound u))) ts1 + -> Nothing+ | otherwise -> Just gg+++-- | Cut the terms due to the outermost binder from a tagged closure.+cutTaggedClosureT + :: (Eq n, Ord n) + => Bind n + -> TaggedClosure n + -> Maybe (TaggedClosure n)++cutTaggedClosureT b1 cc+ = let lower = case b1 of+ BAnon{} -> lowerT 1+ _ -> id+ in case cc of+ GBoundVal u2 ts -> Just $ GBoundVal u2 (lower ts)++ GBoundRgnVar u2 + | boundMatchesBind u2 b1 -> Nothing+ | otherwise -> Just $ GBoundRgnVar (lower u2)++ GBoundRgnCon u2 -> Just $ GBoundRgnCon (lower u2)+++-- | Like `cutTaggedClosureX` but cut terms due to several binders.+cutTaggedClosureXs + :: (Eq n, Ord n)+ => [Bind n]+ -> TaggedClosure n -> Maybe (TaggedClosure n)++cutTaggedClosureXs bb c + = case bb of+ [] -> Just c+ (b:bs) -> case cutTaggedClosureX b c of+ Nothing -> Nothing+ Just c' -> cutTaggedClosureXs bs c'+++-- | Cut the terms due to the outermost binder from a tagged closure.+cutTaggedClosureX+ :: (Eq n, Ord n) + => Bind n + -> TaggedClosure n + -> Maybe (TaggedClosure n)++cutTaggedClosureX b1 cc+ = let lower = case b1 of+ BAnon{} -> lowerT 1+ _ -> id+ in case cc of+ GBoundVal u2 ts+ | boundMatchesBind u2 b1 -> Nothing+ | otherwise -> Just $ GBoundVal (lower u2) ts++ GBoundRgnVar u2 -> Just $ GBoundRgnVar u2+ GBoundRgnCon u2 -> Just $ GBoundRgnCon u2
+ DDC/Core/Collect.hs view
@@ -0,0 +1,253 @@++-- | Collecting sets of variables and constructors.+module DDC.Core.Collect+ ( freeT+ , freeX+ , collectBound+ , collectSpecBinds)+where+import DDC.Type.Compounds+import DDC.Core.Exp+import DDC.Type.Env (Env)+import qualified DDC.Type.Env as Env+import qualified DDC.Type.Sum as Sum+import qualified Data.Set as Set+import Data.Set (Set)+++-- freeT ----------------------------------------------------------------------+-- | Collect the free Spec variables in a thing (level-1).+freeT :: (BindStruct c, Ord n) + => Env n -> c n -> Set (Bound n)+freeT tenv xx = Set.unions $ map (freeOfTreeT tenv) $ slurpBindTree xx++freeOfTreeT :: Ord n => Env n -> BindTree n -> Set (Bound n)+freeOfTreeT kenv tt+ = case tt of+ BindDef way bs ts+ | BoundSpec <- boundLevelOfBindWay way+ , kenv' <- Env.extends bs kenv+ -> Set.unions $ map (freeOfTreeT kenv') ts++ BindDef _ _ ts+ -> Set.unions $ map (freeOfTreeT kenv) ts++ BindUse BoundSpec u+ | Env.member u kenv -> Set.empty+ | otherwise -> Set.singleton u+ _ -> Set.empty+++-- freeX ----------------------------------------------------------------------+-- | Collect the free Data and Witness variables in a thing (level-0).+freeX :: (BindStruct c, Ord n) + => Env n -> c n -> Set (Bound n)+freeX tenv xx = Set.unions $ map (freeOfTreeX tenv) $ slurpBindTree xx++freeOfTreeX :: Ord n => Env n -> BindTree n -> Set (Bound n)+freeOfTreeX tenv tt+ = case tt of+ BindDef way bs ts+ | BoundExpWit <- boundLevelOfBindWay way+ , tenv' <- Env.extends bs tenv+ -> Set.unions $ map (freeOfTreeX tenv') ts++ BindDef _ _ ts+ -> Set.unions $ map (freeOfTreeX tenv) ts++ BindUse BoundExpWit u+ | Env.member u tenv -> Set.empty+ | otherwise -> Set.singleton u+ _ -> Set.empty+++-- collectBound ---------------------------------------------------------------+-- | Collect all the bound variables in a thing, +-- independent of whether they are free or not.+collectBound :: (BindStruct c, Ord n) => c n -> Set (Bound n)+collectBound + = Set.unions . map collectBoundOfTree . slurpBindTree ++collectBoundOfTree :: Ord n => BindTree n -> Set (Bound n)+collectBoundOfTree tt+ = case tt of+ BindDef _ _ ts -> Set.unions $ map collectBoundOfTree ts+ BindUse _ u -> Set.singleton u+ BindCon _ u -> Set.singleton u+++-- collectSpecBinds -----------------------------------------------------------+-- | Collect all the Spec binders in a thing.+collectSpecBinds :: (BindStruct c, Ord n) => c n -> [Bind n]+collectSpecBinds + = concatMap collectSpecBindsOfTree . slurpBindTree+ ++collectSpecBindsOfTree :: Ord n => BindTree n -> [Bind n]+collectSpecBindsOfTree tt+ = case tt of+ BindDef way bs ts+ | BoundSpec <- boundLevelOfBindWay way+ -> concat ( bs+ : map collectSpecBindsOfTree ts)++ | otherwise+ -> concatMap collectSpecBindsOfTree ts++ _ -> []+++-------------------------------------------------------------------------------+-- | A description of the binding structure of some type or expression.+data BindTree n+ -- | An abstract binding expression.+ = BindDef BindWay [Bind n] [BindTree n]++ -- | Use of a variable.+ | BindUse BoundLevel (Bound n)++ -- | Use of a constructor.+ | BindCon BoundLevel (Bound n)+ deriving (Eq, Show)+++-- | Describes how a variable was bound.+data BindWay+ = BindForall+ | BindLAM+ | BindLam+ | BindLet+ | BindLetRec+ | BindLetRegion+ | BindLetRegionWith+ | BindCasePat+ deriving (Eq, Show)+++-- | What level this binder is at.+data BoundLevel+ = BoundSpec+ | BoundExpWit+ deriving (Eq, Show)+++-- | Get the `BoundLevel` corresponding to a `BindWay`.+boundLevelOfBindWay :: BindWay -> BoundLevel+boundLevelOfBindWay way+ = case way of+ BindForall -> BoundSpec+ BindLAM -> BoundSpec+ BindLam -> BoundExpWit+ BindLet -> BoundExpWit+ BindLetRec -> BoundExpWit+ BindLetRegion -> BoundSpec+ BindLetRegionWith -> BoundExpWit+ BindCasePat -> BoundExpWit+++-- BindStruct -----------------------------------------------------------------+class BindStruct (c :: * -> *) where+ slurpBindTree :: c n -> [BindTree n]+++instance BindStruct Type where+ slurpBindTree tt+ = case tt of+ TVar u -> [BindUse BoundSpec u]+ TCon tc -> slurpBindTree tc+ TForall b t -> [bindDefT BindForall [b] [t]]+ TApp t1 t2 -> slurpBindTree t1 ++ slurpBindTree t2+ TSum ts -> concatMap slurpBindTree $ Sum.toList ts+++instance BindStruct TyCon where+ slurpBindTree tc+ = case tc of+ TyConBound u -> [BindCon BoundSpec u]+ _ -> []+++instance BindStruct (Exp a) where+ slurpBindTree xx+ = case xx of+ XVar _ u -> [BindUse BoundExpWit u]+ XCon _ u -> [BindCon BoundExpWit u]+ XApp _ x1 x2 -> slurpBindTree x1 ++ slurpBindTree x2+ XLAM _ b x -> [bindDefT BindLAM [b] [x]]+ XLam _ b x -> [bindDefX BindLam [b] [x]] ++ XLet _ (LLet m b x1) x2+ -> slurpBindTree m+ ++ slurpBindTree x1+ ++ [bindDefX BindLet [b] [x2]]++ XLet _ (LRec bxs) x2+ -> [bindDefX BindLetRec + (map fst bxs) + (map snd bxs ++ [x2])]+ + XLet _ (LLetRegion b bs) x2+ -> [ BindDef BindLetRegion [b]+ [bindDefX BindLetRegionWith bs [x2]]]++ XLet _ (LWithRegion u) x2+ -> BindUse BoundExpWit u : slurpBindTree x2++ XCase _ x alts -> slurpBindTree x ++ concatMap slurpBindTree alts+ XCast _ c x -> slurpBindTree c ++ slurpBindTree x+ XType t -> slurpBindTree t+ XWitness w -> slurpBindTree w+++instance BindStruct LetMode where+ slurpBindTree mm+ = case mm of+ LetLazy (Just w) -> slurpBindTree w+ _ -> []+++instance BindStruct Cast where+ slurpBindTree cc+ = case cc of+ CastWeakenEffect eff -> slurpBindTree eff+ CastWeakenClosure clo -> slurpBindTree clo+ CastPurify w -> slurpBindTree w+ CastForget w -> slurpBindTree w+++instance BindStruct (Alt a) where+ slurpBindTree alt+ = case alt of+ AAlt PDefault x+ -> slurpBindTree x++ AAlt (PData _ bs) x+ -> [bindDefX BindCasePat bs [x]]+++instance BindStruct Witness where+ slurpBindTree ww+ = case ww of+ WVar u -> [BindUse BoundExpWit u]+ WCon{} -> []+ WApp w1 w2 -> slurpBindTree w1 ++ slurpBindTree w2+ WJoin w1 w2 -> slurpBindTree w1 ++ slurpBindTree w2+ WType t -> slurpBindTree t+++-- | Helper for constructing the `BindTree` for an expression or witness binder.+bindDefX :: BindStruct c + => BindWay -> [Bind n] -> [c n] -> BindTree n+bindDefX way bs xs+ = BindDef way bs+ $ concatMap (slurpBindTree . typeOfBind) bs+ ++ concatMap slurpBindTree xs+++-- | Helper for constructing the `BindTree` for a type binder.+bindDefT :: BindStruct c+ => BindWay -> [Bind n] -> [c n] -> BindTree n+bindDefT way bs xs+ = BindDef way bs $ concatMap slurpBindTree xs++
+ DDC/Core/Compounds.hs view
@@ -0,0 +1,172 @@++-- | Utilities for constructing and destructing compound expressions.+module DDC.Core.Compounds + ( -- * Lets+ bindsOfLets+ , specBindsOfLets+ , valwitBindsOfLets++ -- * Patterns+ , bindsOfPat++ -- * Lambdas+ , makeXLAMs, takeXLAMs+ , makeXLams, takeXLams+ , takeXLamFlags+ , makeXLamFlags++ -- * Applications+ , makeXApps+ , takeXApps+ , takeXConApps+ , takeXPrimApps++ -- * Alternatives+ , takeCtorNameOfAlt)+where+import DDC.Type.Compounds+import DDC.Core.Exp+++-- | Take the binds of a `Lets`.+bindsOfLets :: Lets a n -> [Bind n]+bindsOfLets ll+ = case ll of+ LLet _ b _ -> [b]+ LRec bxs -> map fst bxs+ LLetRegion b bs -> b : bs+ LWithRegion{} -> []+++-- | Like `bindsOfLets` but only take the type binders.+specBindsOfLets :: Lets a n -> [Bind n]+specBindsOfLets ll+ = case ll of+ LLet _ _ _ -> []+ LRec _ -> []+ LLetRegion b _ -> [b]+ LWithRegion{} -> []+++-- | Like `bindsOfLets` but only take the value and witness binders.+valwitBindsOfLets :: Lets a n -> [Bind n]+valwitBindsOfLets ll+ = case ll of+ LLet _ b _ -> [b]+ LRec bxs -> map fst bxs+ LLetRegion _ bs -> bs+ LWithRegion{} -> []+++-- | Take the binds of a `Pat`.+bindsOfPat :: Pat n -> [Bind n]+bindsOfPat pp+ = case pp of+ PDefault -> []+ PData _ bs -> bs+++-- Lambdas ---------------------------------------------------------------------+-- | Make some nested type lambda abstractions.+makeXLAMs :: a -> [Bind n] -> Exp a n -> Exp a n+makeXLAMs a bs x+ = foldr (XLAM a) x (reverse bs)+++-- | Split nested value and 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 value or witness lambda abstractions.+makeXLams :: a -> [Bind n] -> Exp a n -> Exp a n+makeXLams a bs x+ = foldr (XLam a) x (reverse bs)+++-- | Split nested value or witness lambdas from the front of an expression,+-- or `Nothing` if there aren't any.+takeXLams :: Exp a n -> Maybe ([Bind n], Exp a n)+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 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)+++-- | 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 (reverse fbs)+++-- Applications ---------------------------------------------------------------+-- | Build sequence of type applications.+makeXApps :: a -> Exp a n -> [Exp a n] -> Exp a n+makeXApps a t1 ts = foldl (XApp a) t1 ts+++-- | Flatten an application into the function parts and arguments, if any.+takeXApps :: Exp a n -> [Exp a n]+takeXApps xx+ = case xx of+ XApp _ x1 x2 -> takeXApps 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 takeXApps xx of+ XVar _ (UPrim p _) : xs -> Just (p, xs)+ _ -> Nothing++-- | Flatten an application of a data constructor into the constructor+-- and its arguments. +--+-- Returns `Nothing` if the expression isn't a constructor application.+takeXConApps :: Exp a n -> Maybe (Bound n, [Exp a n])+takeXConApps xx+ = case takeXApps xx of+ XCon _ u : xs -> Just (u, xs)+ _ -> Nothing+++-- Alternatives ---------------------------------------------------------------+-- | Take the constructor name of an alternative, if there is one.+takeCtorNameOfAlt :: Alt a n -> Maybe n+takeCtorNameOfAlt aa+ = case aa of+ AAlt (PData u _) _ -> takeNameOfBound u+ _ -> Nothing+++
+ DDC/Core/DataDef.hs view
@@ -0,0 +1,135 @@++-- | Algebraic data type definitions.+module DDC.Core.DataDef+ ( DataDef (..)++ -- * Data type definition table+ , DataDefs (..)+ , DataMode (..)+ , DataType (..)+ , DataCtor (..)++ , emptyDataDefs+ , insertDataDef+ , fromListDataDefs+ , lookupModeOfDataType)+where+import DDC.Type.Exp+import Data.Map (Map)+import qualified Data.Map as Map+import Data.Maybe+import Control.Monad+++-- | The definition of a single data type.+data DataDef n+ = DataDef+ { -- | Name of the data type.+ dataDefTypeName :: n++ -- | Kinds of type parameters.+ , dataDefParamKinds :: [Kind n]++ -- | Constructors of is data type, or Nothing if there are+ -- too many to list (like with `Int`).+ , dataDefCtors :: Maybe [(n, [Type n])] }++++-- DataDefs -------------------------------------------------------------------+-- | A table of data type definitions,+-- unpacked into type and data constructors so we can find them easily.+data DataDefs n+ = DataDefs+ { dataDefsTypes :: Map n (DataType n)+ , dataDefsCtors :: Map n (DataCtor n) }+++-- | The mode of a data type records how many data constructors there are.+-- This can be set to 'Large' for large primitive types like Int and Float.+-- In this case we don't ever expect them all to be enumerated+-- as case alternatives.+data DataMode n+ = DataModeSmall [n]+ | DataModeLarge+++-- | Describes a data type constructor, used in the `DataDefs` table.+data DataType n+ = DataType + { -- | Name of data type constructor.+ dataTypeName :: n++ -- | Kinds of type parameters to constructor.+ , dataTypeParamKinds :: [Kind n]++ -- | Names of data constructors of this data type,+ -- or `Nothing` if it has infinitely many constructors.+ , dataTypeMode :: DataMode n }+++-- | Describes a data constructor, used in the `DataDefs` table.+data DataCtor n+ = DataCtor+ { -- | Name of data constructor.+ dataCtorName :: n++ -- | Field types of constructor.+ , dataCtorFieldTypes :: [Type n]++ -- | Name of result type of constructor.+ , dataCtorTypeName :: n }++++-- | An empty table of data type definitions.+emptyDataDefs :: DataDefs n+emptyDataDefs+ = DataDefs+ { dataDefsTypes = Map.empty+ , dataDefsCtors = Map.empty }+++-- | Insert a data type definition into some DataDefs.+insertDataDef :: Ord n => DataDef n -> DataDefs n -> DataDefs n+insertDataDef (DataDef nType ks mCtors) dataDefs+ = let defType = DataType+ { dataTypeName = nType+ , dataTypeParamKinds = ks+ , dataTypeMode = defMode }++ defMode = case mCtors of+ Nothing -> DataModeLarge+ Just ctors -> DataModeSmall (map fst ctors)++ makeDefCtor (nCtor, tsFields)+ = DataCtor+ { dataCtorName = nCtor+ , dataCtorFieldTypes = tsFields+ , dataCtorTypeName = nType }++ defCtors = case mCtors of+ Nothing -> Nothing+ Just cs -> Just $ map makeDefCtor cs++ in dataDefs+ { dataDefsTypes = Map.insert nType defType (dataDefsTypes dataDefs)+ , dataDefsCtors = Map.union (dataDefsCtors dataDefs)+ $ Map.fromList [(n, def) | def@(DataCtor n _ _) + <- concat $ maybeToList defCtors] }+++-- | Build a `DataDefs` table from a list of `DataDef`+fromListDataDefs :: Ord n => [DataDef n] -> DataDefs n+fromListDataDefs defs+ = foldr insertDataDef emptyDataDefs defs++++-- | Yield the list of data constructor names for some data type, +-- or `Nothing` for large types with too many constructors to list.+lookupModeOfDataType :: Ord n => n -> DataDefs n -> Maybe (DataMode n)+lookupModeOfDataType n defs+ = liftM dataTypeMode $ Map.lookup n (dataDefsTypes defs)++
+ DDC/Core/Exp.hs view
@@ -0,0 +1,198 @@++-- | Abstract syntax for the Disciple core language.+module DDC.Core.Exp + ( module DDC.Type.Exp++ -- * Computation expressions+ , Exp (..)+ , Cast (..)+ , Lets (..)+ , LetMode (..)+ , Alt (..)+ , Pat (..)+ + -- * Witnesses expressions+ , Witness (..)+ , WiCon (..)+ , WbCon (..))+where+import DDC.Type.Exp+import DDC.Type.Sum ()+++-- Values ---------------------------------------------------------------------+-- | Well-typed expressions live in the Data universe, and their types always+-- have kind '*'. +-- +-- Expressions do something useful at runtime, and might diverge or cause+-- side effects.+data Exp a n+ -- | Value variable or primitive operation.+ = XVar a (Bound n)++ -- | Data constructor or literal.+ | XCon a (Bound n)++ -- | Type abstraction (level-1).+ | XLAM a (Bind n) (Exp a n)++ -- | Value and Witness abstraction (level-0).+ | XLam a (Bind n) (Exp a n)++ -- | Application.+ | XApp a (Exp a n) (Exp a n)++ -- | Possibly recursive bindings.+ | XLet a (Lets a n) (Exp a n)++ -- | Case branching.+ | XCase a (Exp a n) [Alt a n]++ -- | Type cast.+ | XCast a (Cast n) (Exp a n)++ -- | Type can appear as the argument of an application.+ | XType (Type n)++ -- | Witness can appear as the argument of an application.+ | XWitness (Witness n)+ deriving (Eq, Show)+++-- | Type casts.+data Cast n+ -- | Weaken the effect of an expression.+ = CastWeakenEffect (Effect n)+ + -- | Weaken the closure of an expression.+ | CastWeakenClosure (Closure n)++ -- | Purify the effect of an expression.+ | CastPurify (Witness n)++ -- | Hide sharing of the closure of an expression.+ | CastForget (Witness n)+ deriving (Eq, Show)+++-- | Possibly recursive bindings.+data Lets a n+ -- | Non-recursive expression binding.+ = LLet (LetMode n) (Bind n) (Exp a n)++ -- | Recursive binding of lambda abstractions.+ | LRec [(Bind n, Exp a n)]++ -- | Bind a local region variable,+ -- and witnesses to its properties.+ | LLetRegion (Bind n) [Bind n]+ + -- | Holds a region handle during evaluation.+ | LWithRegion (Bound n)+ deriving (Eq, Show)+++-- | Describes how a let binding should be evaluated.+data LetMode n+ -- | Evaluate binding before substituting the result.+ = LetStrict++ -- | Use lazy evaluation. + -- The witness shows that the head region of the bound expression+ -- can contain thunks (is lazy), or Nothing if there is no head region.+ | LetLazy (Maybe (Witness n))+ deriving (Eq, Show)+++-- | Case alternatives.+data Alt a n+ = AAlt (Pat n) (Exp a n)+ deriving (Eq, Show)+++-- | Pattern matching.+data Pat n+ -- | The default pattern always succeeds.+ = PDefault+ + -- | Match a data constructor and bind its arguments.+ | PData (Bound n) [Bind n]+ deriving (Eq, Show)+ ++-- Witness --------------------------------------------------------------------+-- | When a witness exists in the program it guarantees that a+-- certain property of the program is true.+data Witness n+ -- | Witness variable.+ = WVar (Bound n)+ + -- | Witness constructor.+ | WCon (WiCon n)+ + -- | Witness application.+ | WApp (Witness n) (Witness n)++ -- | Joining of witnesses.+ | WJoin (Witness n) (Witness n)++ -- | Type can appear as the argument of an application.+ | WType (Type n)+ deriving (Eq, Show)+++-- | Witness constructors.+data WiCon n+ -- | Witness constructors baked into the language.+ = WiConBuiltin WbCon++ -- | Witness constructors defined in the environment.+ -- In the interpreter we use this to hold runtime capabilities.+ | WiConBound (Bound n)+ deriving (Eq, Show)+++-- | Built-in witness constructors.+--+-- These are used to convert a runtime capability into a witness that+-- the corresponding property is true.+data WbCon+ -- | (axiom) The pure effect is pure.+ -- + -- @pure :: Pure !0@+ = WbConPure ++ -- | (axiom) The empty closure is empty.+ --+ -- @empty :: Empty $0@+ | WbConEmpty++ -- | Convert a capability guaranteeing that a region is in the global+ -- heap into a witness that a closure using this region is empty.+ -- This lets us rely on the garbage collector to reclaim objects+ -- in the region. It is needed when we suspend the evaluation of + -- expressions that have a region in their closure, because the+ -- type of the returned thunk may not reveal that it references+ -- objects in that region.+ -- + -- @use :: [r: %]. Global r => Empty (Use r)@+ | WbConUse ++ -- | Convert a capability guaranteeing the constancy of a region into+ -- a witness that a read from that region is pure.+ -- This lets us suspend applications that read constant objects,+ -- because it doesn't matter if the read is delayed, we'll always+ -- get the same result.+ --+ -- @read :: [r: %]. Const r => Pure (Read r)@+ | WbConRead ++ -- | Convert a capability guaranteeing the constancy of a region into+ -- a witness that allocation into that region is pure.+ -- This lets us increase the sharing of constant objects,+ -- because we can't tell constant objects of the same value apart.+ -- + -- @alloc :: [r: %]. Const r => Pure (Alloc r)@+ | WbConAlloc+ deriving (Eq, Show)+
+ DDC/Core/Parser.hs view
@@ -0,0 +1,621 @@+-- | Core language parser.+module DDC.Core.Parser+ ( module DDC.Base.Parser+ , Parser+ , pExp+ , pWitness)+ +where+import DDC.Core.Exp+import DDC.Core.Parser.Tokens+import DDC.Base.Parser ((<?>))+import DDC.Type.Parser (pTok)+import qualified DDC.Base.Parser as P+import qualified DDC.Type.Compounds as T+import qualified DDC.Type.Parser as T+import Control.Monad.Error+++-- | A parser of core language tokens.+type Parser n a+ = P.Parser (Tok n) a+++-- Expressions ----------------------------------------------------------------+-- | Parse a core language expression.+pExp :: Ord n => Parser n (Exp () n)+pExp + = P.choice+ -- Level-0 lambda abstractions+ -- \(x1 x2 ... : TYPE) (y1 y2 ... : TYPE) ... . EXP+ [ do pTok KBackSlash++ bs <- liftM concat+ $ P.many1 + $ do pTok KRoundBra+ bs' <- P.many1 T.pBinder+ pTok KColon+ t <- T.pType+ pTok KRoundKet+ return (map (\b -> T.makeBindFromBinder b t) bs')++ pTok KDot+ xBody <- pExp+ return $ foldr (XLam ()) xBody bs++ -- Level-1 lambda abstractions.+ -- /\(x1 x2 ... : TYPE) (y1 y2 ... : TYPE) ... . EXP+ , do pTok KBigLambda++ bs <- liftM concat+ $ P.many1 + $ do pTok KRoundBra+ bs' <- P.many1 T.pBinder+ pTok KColon+ t <- T.pType+ pTok KRoundKet+ return (map (\b -> T.makeBindFromBinder b t) bs')++ pTok KDot+ xBody <- pExp+ return $ foldr (XLAM ()) xBody bs+++ -- let expression+ , do pTok KLet+ (mode1, b1, x1) <- pLetBinding+ pTok KIn+ x2 <- pExp+ return $ XLet () (LLet mode1 b1 x1) x2++ -- letrec expression+ , do pTok KLetRec+ pTok KBraceBra+ lets <- P.sepEndBy1 pLetRecBinding (pTok KSemiColon)+ pTok KBraceKet+ pTok KIn+ x <- pExp++ return $ XLet () (LRec lets) x+++ -- Local region binding.+ -- letregion BINDER with { BINDER : TYPE ... } in EXP+ -- letregion BINDER in EXP+ , do pTok KLetRegion+ br <- T.pBinder+ let b = T.makeBindFromBinder br T.kRegion++ P.choice + [ do pTok KWith+ pTok KBraceBra+ wits <- P.sepBy+ (do w <- pVar+ pTok KColon+ t <- T.pTypeApp+ return (BName w t))+ (pTok KSemiColon)+ pTok KBraceKet+ pTok KIn+ x <- pExp + return $ XLet () (LLetRegion b wits) x ++ , do pTok KIn+ x <- pExp+ return $ XLet () (LLetRegion b []) x ]+++ -- withregion CON in EXP+ , do pTok KWithRegion+ n <- pVar+ pTok KIn+ x <- pExp+ let u = UName n (T.tBot T.kRegion)+ return $ XLet () (LWithRegion u) x+++ -- case EXP of { ALTS }+ , do pTok KCase+ x <- pExp+ pTok KOf + pTok KBraceBra+ alts <- P.sepEndBy1 pAlt (pTok KSemiColon)+ pTok KBraceKet+ return $ XCase () x alts+++ -- weakeff [TYPE] in EXP+ , do pTok KWeakEff+ pTok KSquareBra+ t <- T.pType+ pTok KSquareKet+ pTok KIn+ x <- pExp+ return $ XCast () (CastWeakenEffect t) x+++ -- weakclo [TYPE] in EXP+ , do pTok KWeakClo+ pTok KSquareBra+ t <- T.pType+ pTok KSquareKet+ pTok KIn+ x <- pExp+ return $ XCast () (CastWeakenClosure t) x+++ -- purify <WITNESS> in EXP+ , do pTok KPurify+ pTok KAngleBra+ w <- pWitness+ pTok KAngleKet+ pTok KIn+ x <- pExp+ return $ XCast () (CastPurify w) x+++ -- forget <WITNESS> in EXP+ , do pTok KForget+ pTok KAngleBra+ w <- pWitness+ pTok KAngleKet+ pTok KIn+ x <- pExp+ return $ XCast () (CastForget w) x++ -- APP+ , do pExpApp+ ]++ <?> "an expression"+++-- Applications.+pExpApp :: Ord n => Parser n (Exp () n)+pExpApp + = do x1 <- pExp0+ + P.choice+ [ do xs <- liftM concat $ P.many1 pArgs+ return $ foldl (XApp ()) x1 xs++ , return x1]++ <?> "an expression or application"+++-- Comp, Witness or Spec arguments.+pArgs :: Ord n => Parser n [Exp () n]+pArgs + = P.choice+ -- [TYPE]+ [ do pTok KSquareBra+ t <- T.pType + pTok KSquareKet+ return [XType t]++ -- [: TYPE0 TYPE0 ... :]+ , do pTok KSquareColonBra+ ts <- P.many1 T.pTypeAtom+ pTok KSquareColonKet+ return $ map XType ts+ + -- <WITNESS>+ , do pTok KAngleBra+ w <- pWitness+ pTok KAngleKet+ return [XWitness w]+ + -- <: WITNESS0 WITNESS0 ... :>+ , do pTok KAngleColonBra+ ws <- P.many1 pWitnessAtom+ pTok KAngleColonKet+ return $ map XWitness ws+ + -- EXP0+ , do x <- pExp0+ return [x]+ ]+ <?> "a type, witness or expression argument"+++-- Atomics+pExp0 :: Ord n => Parser n (Exp () n)+pExp0 + = P.choice+ -- (EXP2)+ [ do pTok KRoundBra+ t <- pExp+ pTok KRoundKet+ return $ t+ + -- Named constructors+ , do con <- pCon+ return $ XCon () (UName con (T.tBot T.kData)) ++ -- Literals+ , do lit <- pLit+ return $ XCon () (UName lit (T.tBot T.kData))++ -- Debruijn indices+ , do i <- T.pIndex+ return $ XVar () (UIx i (T.tBot T.kData))++ -- Variables+ , do var <- pVar+ return $ XVar () (UName var (T.tBot T.kData)) + ]++ <?> "a variable, constructor, or parenthesised type"+++-- Case alternatives.+pAlt :: Ord n => Parser n (Alt () n)+pAlt+ = do p <- pPat+ pTok KArrowDash+ x <- pExp+ return $ AAlt p x+++-- Patterns.+pPat :: Ord n => Parser n (Pat n)+pPat+ = P.choice+ [ -- Wildcard+ do pTok KUnderscore+ return $ PDefault++ -- LIT+ , do nLit <- pLit+ return $ PData (UName nLit (T.tBot T.kData)) []++ -- CON BIND BIND ...+ , do nCon <- pCon + bs <- P.many pBindPat+ return $ PData (UName 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 + = P.choice+ -- Plain binder.+ [ do b <- T.pBinder+ return $ T.makeBindFromBinder b (T.tBot T.kData)++ -- Binder with type, wrapped in parens.+ , do pTok KRoundBra+ b <- T.pBinder+ pTok KColon+ t <- T.pType+ pTok KRoundKet+ return $ T.makeBindFromBinder b t+ ]+++-- Bindings -------------------------------------------------------------------+-- | A binding for let expression.+pLetBinding :: Ord n => Parser n (LetMode n, Bind n, Exp () n)+pLetBinding + = do b <- T.pBinder++ P.choice+ [ do -- Binding with full type signature.+ -- BINDER : TYPE = EXP+ pTok KColon+ t <- T.pType+ mode <- pLetMode+ pTok KEquals+ xBody <- pExp++ return $ (mode, 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+ let t = T.tBot T.kData+ return $ (mode, T.makeBindFromBinder b t, xBody)+++ , do -- Binding using function syntax.+ ps <- liftM concat + $ P.many pBindParamSpec + + 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 <- T.pType+ mode <- pLetMode+ pTok KEquals+ xBody <- pExp++ let x = expOfParams () ps xBody+ let t = funTypeOfParams ps tBody+ return (mode, 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++ let x = expOfParams () ps xBody+ let t = T.tBot T.kData+ return (mode, T.makeBindFromBinder b t, x) ]+ ]++-- | Parse a let mode specifier.+-- Only allow the lazy specifier with non-recursive bindings.+-- We don't support value recursion, so the right of all recursive+-- bindings must be explicit lambda abstractions anyway, so there's +-- no point suspending them.+pLetMode :: Ord n => Parser n (LetMode n)+pLetMode+ = do P.choice+ -- lazy <WITNESS>+ [ do pTok KLazy++ P.choice+ [ do pTok KAngleBra+ w <- pWitness+ pTok KAngleKet+ return $ LetLazy (Just w)+ + , do return $ LetLazy Nothing ]++ , do return $ LetStrict ]+++-- | Letrec bindings must have a full type signature, +-- or use function syntax with a return type so that we can make one.+pLetRecBinding :: Ord n => Parser n (Bind n, Exp () n)+pLetRecBinding + = do b <- T.pBinder++ P.choice+ [ do -- Binding with full type signature.+ -- BINDER : TYPE = EXP+ pTok KColon+ t <- T.pType+ pTok KEquals+ xBody <- pExp++ return $ (T.makeBindFromBinder b t, xBody) +++ , do -- Binding using function syntax.+ -- BINDER PARAM1 PARAM2 .. PARAMN : TYPE = EXP+ ps <- liftM concat + $ P.many pBindParamSpec + + pTok KColon+ tBody <- T.pType+ let t = funTypeOfParams ps tBody++ pTok KEquals+ xBody <- pExp+ let x = expOfParams () ps xBody++ return (T.makeBindFromBinder b t, x) ]+++-- | Parse a parameter specification.+--+-- [BIND1 BIND2 .. BINDN : TYPE]+-- or (BIND : TYPE)+-- or (BIND : TYPE) { EFFECT | CLOSURE }+--+pBindParamSpec :: Ord n => Parser n [ParamSpec n]+pBindParamSpec+ = P.choice+ -- Type parameter+ -- [BIND1 BIND2 .. BINDN : TYPE]+ [ do pTok KSquareBra+ bs <- P.many1 T.pBinder+ pTok KColon+ t <- T.pType+ pTok KSquareKet+ return [ ParamType b + | b <- zipWith T.makeBindFromBinder bs (repeat t)]+++ -- Witness parameter+ -- <BIND : TYPE>+ , do pTok KAngleBra+ b <- T.pBinder+ pTok KColon+ t <- T.pType+ pTok KAngleKet+ return [ ParamWitness $ T.makeBindFromBinder b t]++ -- Value parameter+ -- (BIND : TYPE) + -- (BIND : TYPE) { TYPE | TYPE }+ , do pTok KRoundBra+ b <- T.pBinder+ pTok KColon+ t <- T.pType+ pTok KRoundKet++ (eff, clo) + <- P.choice+ [ do pTok KBraceBra+ eff' <- T.pType+ pTok KBar+ clo' <- T.pType+ pTok KBraceKet+ return (eff', clo')+ + , do return (T.tBot T.kEffect, T.tBot T.kClosure) ]+ ++ return $ [ParamValue (T.makeBindFromBinder b t) eff clo]+ ]+++-- | Specification of a function parameter.+-- We can determine the contribution to the type of the function, +-- as well as its expression based on the parameter.+data ParamSpec n+ = ParamType (Bind n)+ | ParamWitness (Bind n)+ | 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 + :: a+ -> [ParamSpec n] -- ^ Spec of parameters.+ -> Exp a n -- ^ Body of function.+ -> Exp a n -- ^ Expression of whole function.++expOfParams _ [] xBody = xBody+expOfParams a (p:ps) xBody+ = case p of+ ParamType b + -> XLAM a b $ expOfParams a ps xBody+ + ParamWitness b+ -> XLam a b $ expOfParams a ps xBody++ ParamValue b _ _+ -> XLam a b $ expOfParams a ps xBody++++-- Witnesses ------------------------------------------------------------------+-- | Parse a witness expression.+pWitness :: Ord n => Parser n (Witness n)+pWitness = pWitnessJoin+++-- Witness Joining+pWitnessJoin :: Ord n => Parser n (Witness n)+pWitnessJoin + -- WITNESS or WITNESS & WITNESS+ = do w1 <- pWitnessApp+ P.choice + [ do pTok KAmpersand+ w2 <- pWitnessJoin+ return (WJoin w1 w2)++ , do return w1 ]+++-- Applications+pWitnessApp :: Ord n => Parser n (Witness n)+pWitnessApp + = do (x:xs) <- P.many1 pWitnessArg+ return $ foldl WApp x xs++ <?> "a witness expression or application"+++-- Function argument+pWitnessArg :: Ord n => Parser n (Witness n)+pWitnessArg + = P.choice+ [ -- [TYPE]+ do pTok KSquareBra+ t <- T.pType+ pTok KSquareKet+ return $ WType t++ -- WITNESS+ , do pWitnessAtom ]+++-- Atomics+pWitnessAtom :: Ord n => Parser n (Witness n)+pWitnessAtom + = P.choice+ -- (WITNESS)+ [ do pTok KRoundBra+ w <- pWitness+ pTok KRoundKet+ return $ w++ -- Named constructors+ , do con <- pCon+ return $ WCon (WiConBound $ UName con (T.tBot T.kWitness)) ++ -- Baked-in witness constructors.+ , do wb <- pWbCon+ return $ WCon (WiConBuiltin wb)++ + -- Debruijn indices+ , do i <- T.pIndex+ return $ WVar (UIx i (T.tBot T.kWitness))++ -- Variables+ , do var <- pVar+ return $ WVar (UName var (T.tBot T.kWitness)) ]++ <?> "a witness"+++-------------------------------------------------------------------------------+-- | Parse a builtin named `WiCon`+pWbCon :: Parser n WbCon+pWbCon = P.pTokMaybe f+ where f (KA (KWbConBuiltin wb)) = Just wb+ f _ = Nothing+++-- | Parse a variable name+pVar :: Parser n n+pVar = P.pTokMaybe f+ where f (KN (KVar n)) = Just n+ f _ = Nothing+++-- | Parse a constructor name+pCon :: Parser n n+pCon = P.pTokMaybe f+ where f (KN (KCon n)) = Just n+ f _ = Nothing+++-- | Parse a literal+pLit :: Parser n n+pLit = P.pTokMaybe f+ where f (KN (KLit n)) = Just n+ f _ = Nothing+
+ DDC/Core/Parser/Lexer.hs view
@@ -0,0 +1,293 @@++-- | Reference lexer for core langauge parser. Slow but Simple.+module DDC.Core.Parser.Lexer+ ( -- * Constructors+ isConName, isConStart, isConBody+ , readTwConBuiltin+ , readTcConBuiltin+ , readWbConBuiltin+ , readCon+ + -- * Variables+ , isVarName, isVarStart, isVarBody+ , readVar++ -- * Lexer+ , lexExp)+where+import DDC.Base.Lexer+import DDC.Core.Exp+import DDC.Core.Parser.Tokens+import Data.Char+++-- WbCon names ----------------------------------------------------------------+-- | Read a `WbCon`.+readWbConBuiltin :: String -> Maybe WbCon+readWbConBuiltin ss+ = case ss of+ "pure" -> Just WbConPure+ "empty" -> Just WbConEmpty+ "use" -> Just WbConUse+ "read" -> Just WbConRead+ "alloc" -> Just WbConAlloc+ _ -> Nothing+++-- | Textual keywords in the core language.+keywords :: [(String, Tok n)]+keywords+ = [ ("in", KA KIn)+ , ("of", KA KOf) + , ("letrec", KA KLetRec)+ , ("letregion", KA KLetRegion)+ , ("withregion", KA KWithRegion)+ , ("let", KA KLet)+ , ("lazy", KA KLazy)+ , ("case", KA KCase)+ , ("purify", KA KPurify)+ , ("forget", KA KForget)+ , ("weakeff", KA KWeakEff)+ , ("weakclo", KA KWeakClo)+ , ("with", KA KWith)+ , ("where", KA KWhere) ]+++-------------------------------------------------------------------------------+-- | Lex a string into tokens.+--+lexExp :: Int -> String -> [Token (Tok String)]+lexExp lineStart str+ = lexWord lineStart 1 str+ where ++ lexWord :: Int -> Int -> String -> [Token (Tok String)]+ lexWord line column w+ = let tok t = Token t (SourcePos Nothing line column)+ tokA = tok . KA+ tokN = tok . KN++ lexMore n rest+ = lexWord line (column + n) rest++ in case w of+ [] -> [] ++ ' ' : w' -> lexMore 1 w'+ '\t' : w' -> lexMore 8 w'+ '\n' : w' -> lexWord (line + 1) 1 w'+++ -- The unit data constructor+ '(' : ')' : w' -> tokN (KCon "()") : lexMore 2 w'++ -- Compound Parens+ '[' : ':' : w' -> tokA KSquareColonBra : lexMore 2 w'+ ':' : ']' : w' -> tokA KSquareColonKet : lexMore 2 w'+ '<' : ':' : w' -> tokA KAngleColonBra : lexMore 2 w'+ ':' : '>' : w' -> tokA KAngleColonKet : lexMore 2 w'++ -- Function Constructors+ '~' : '>' : w' -> tokA KArrowTilde : lexMore 2 w'+ '-' : '>' : w' -> tokA KArrowDash : lexMore 2 w'+ '=' : '>' : w' -> tokA KArrowEquals : lexMore 2 w'++ -- Compound symbols+ ':' : ':' : w' -> tokA KColonColon : lexMore 2 w'+ '/' : '\\' : w' -> tokA KBigLambda : lexMore 2 w'++ -- Debruijn indices+ '^' : cs+ | (ds, rest) <- span isDigit cs+ , length ds >= 1+ -> tokA (KIndex (read ds)) : lexMore (1 + length ds) rest ++ -- Parens+ '(' : w' -> tokA KRoundBra : lexMore 1 w'+ ')' : w' -> tokA KRoundKet : lexMore 1 w'+ '[' : w' -> tokA KSquareBra : lexMore 1 w'+ ']' : w' -> tokA KSquareKet : lexMore 1 w'+ '{' : w' -> tokA KBraceBra : lexMore 1 w'+ '}' : w' -> tokA KBraceKet : lexMore 1 w'+ '<' : w' -> tokA KAngleBra : lexMore 1 w'+ '>' : w' -> tokA KAngleKet : lexMore 1 w' ++ -- Punctuation+ '.' : w' -> tokA KDot : lexMore 1 w'+ '|' : w' -> tokA KBar : lexMore 1 w'+ '^' : w' -> tokA KHat : lexMore 1 w'+ '+' : w' -> tokA KPlus : lexMore 1 w'+ ':' : w' -> tokA KColon : lexMore 1 w'+ ',' : w' -> tokA KComma : lexMore 1 w'+ '\\' : w' -> tokA KBackSlash : lexMore 1 w'+ ';' : w' -> tokA KSemiColon : lexMore 1 w'+ '_' : w' -> tokA KUnderscore : lexMore 1 w'+ '=' : w' -> tokA KEquals : lexMore 1 w'+ '&' : w' -> tokA KAmpersand : lexMore 1 w'+ '-' : w' -> tokA KDash : lexMore 1 w'+ + -- Bottoms+ '!' : '0' : w' -> tokA KBotEffect : lexMore 2 w'+ '$' : '0' : w' -> tokA KBotClosure : lexMore 2 w'++ -- Sort Constructors+ '*' : '*' : w' -> tokA KSortComp : lexMore 2 w'+ '@' : '@' : w' -> tokA KSortProp : lexMore 2 w' ++ -- Kind Constructors+ '*' : w' -> tokA KKindValue : lexMore 1 w'+ '%' : w' -> tokA KKindRegion : lexMore 1 w'+ '!' : w' -> tokA KKindEffect : lexMore 1 w'+ '$' : w' -> tokA KKindClosure : lexMore 1 w'+ '@' : w' -> tokA KKindWitness : lexMore 1 w'+ + -- Literal values+ c : cs+ | isDigit c+ , (body, rest) <- span isDigit cs+ -> tokN (KLit (c:body)) : lexMore (length (c:body)) rest+ + -- Named Constructors+ c : cs+ | isConStart c+ , (body, rest) <- span isConBody cs+ , (body', rest') <- case rest of+ '#' : rest' -> (body ++ "#", rest')+ _ -> (body, rest)+ -> let readNamedCon s+ | Just twcon <- readTwConBuiltin s+ = tokA (KTwConBuiltin twcon) : lexMore (length s) rest'+ + | Just tccon <- readTcConBuiltin s+ = tokA (KTcConBuiltin tccon) : lexMore (length s) rest'+ + | Just con <- readCon s+ = tokN (KCon con) : lexMore (length s) rest'+ + | otherwise + = [tok (KJunk c)]+ + in readNamedCon (c : body')++ -- Keywords, Named Variables and Witness constructors+ c : cs+ | isVarStart c+ , (body, rest) <- span isVarBody cs+ -> let readNamedVar s+ | Just t <- lookup s keywords+ = tok t : lexMore (length s) rest++ | Just wc <- readWbConBuiltin s+ = tokA (KWbConBuiltin wc) : lexMore (length s) rest+ + | Just v <- readVar s+ = tokN (KVar v) : lexMore (length s) rest++ | otherwise+ = [tok (KJunk c)]++ in readNamedVar (c : body)++ -- Error+ c : _ -> [tok $ KJunk c]+ ++-- TyCon names ----------------------------------------------------------------+-- | String is a constructor name.+isConName :: String -> Bool+isConName str+ = case str of+ [] -> False+ (c:cs) + | isConStart c + , and (map isConBody cs)+ -> True+ + | _ : _ <- cs+ , isConStart c+ , and (map isConBody (init cs))+ , last cs == '#'+ -> True++ | otherwise+ -> False++-- | Character can start a constructor name.+isConStart :: Char -> Bool+isConStart = isUpper+++-- | Charater can be part of a constructor body.+isConBody :: Char -> Bool+isConBody c = isUpper c || isLower c || isDigit c || c == '_'+ ++-- | Read a named `TwCon`. +readTwConBuiltin :: String -> Maybe TwCon+readTwConBuiltin ss+ = case ss of+ "Global" -> Just TwConGlobal+ "DeepGlobal" -> Just TwConDeepGlobal+ "Const" -> Just TwConConst+ "DeepConst" -> Just TwConDeepConst+ "Mutable" -> Just TwConMutable+ "DeepMutable" -> Just TwConDeepMutable+ "Lazy" -> Just TwConLazy+ "HeadLazy" -> Just TwConHeadLazy+ "Manifest" -> Just TwConManifest+ "Pure" -> Just TwConPure+ "Empty" -> Just TwConEmpty+ _ -> Nothing+++-- | Read a builtin `TcCon` with a non-symbolic name, +-- ie not '->'.+readTcConBuiltin :: String -> Maybe TcCon+readTcConBuiltin ss+ = case ss of+ "Read" -> Just TcConRead+ "HeadRead" -> Just TcConHeadRead+ "DeepRead" -> Just TcConDeepRead+ "Write" -> Just TcConWrite+ "DeepWrite" -> Just TcConDeepWrite+ "Alloc" -> Just TcConAlloc+ "DeepAlloc" -> Just TcConDeepAlloc+ "Use" -> Just TcConUse+ "DeepUse" -> Just TcConDeepUse+ _ -> Nothing+++-- | Read a named, user defined `TcCon`.+--+-- We won't know its kind, so fill this in with the Bottom element for +-- computatation kinds (**0).+readCon :: String -> Maybe String+readCon ss+ | isConName ss = Just ss+ | otherwise = Nothing+++-- TyVar names ----------------------------------------------------------------+-- | String is a variable name.+isVarName :: String -> Bool+isVarName [] = False+isVarName (c:cs) = isVarStart c && (and $ map isVarBody cs)+++-- | Charater can start a variable name.+isVarStart :: Char -> Bool+isVarStart = isLower+ ++-- | Character can be part of a variable body.+isVarBody :: Char -> Bool+isVarBody c+ = isUpper c || isLower c || isDigit c || c == '_' || c == '\''+++-- | Read a named, user defined variable.+readVar :: String -> Maybe String+readVar ss+ | isVarName ss = Just ss+ | otherwise = Nothing+
+ DDC/Core/Parser/Tokens.hs view
@@ -0,0 +1,263 @@++module DDC.Core.Parser.Tokens+ ( Tok (..)+ , describeTok+ , renameTok++ , TokAtom (..)+ , describeTokAtom++ , TokNamed (..)+ , describeTokNamed)+where+import DDC.Core.Pretty+import DDC.Core.Exp+++-- TokenFamily ----------------------------------------------------------------+-- | The family of a token.+-- This is used to help generate parser error messages,+-- so we can say ''the constructor Cons''+-- and ''the keyword case'' etc.+data TokenFamily+ = Symbol+ | Keyword+ | Constructor+ | Index+ | Variable+++-- | Describe a token family, for parser error messages.+describeTokenFamily :: TokenFamily -> String+describeTokenFamily tf+ = case tf of+ Symbol -> "symbol"+ Keyword -> "keyword"+ Constructor -> "constructor"+ Index -> "index"+ Variable -> "variable"+++-- Tok ------------------------------------------------------------------------+-- | Tokens accepted by the core language parser.+data Tok n+ -- Some junk symbol that isn't part of the language.+ = KJunk Char++ -- An atomic token.+ | KA !TokAtom ++ -- A named token.+ | KN !(TokNamed n)+ deriving (Eq, Show)+++-- | Describe a token for parser error messages.+describeTok :: Pretty n => Tok n -> String+describeTok kk+ = case kk of+ KJunk c -> "character " ++ show c+ KA ta -> describeTokAtom ta+ KN tn -> describeTokNamed tn+++-- | Apply a function to all the names in a `Tok`.+renameTok+ :: Ord n2+ => (n1 -> n2) -> Tok n1 -> Tok n2++renameTok f kk+ = case kk of+ KJunk s -> KJunk s+ KA t -> KA t+ KN t -> KN $ renameTokNamed f t+++-- TokAtom --------------------------------------------------------------------+-- | Atomic tokens, that don't contain user-defined names.+data TokAtom+ -- parens+ = KRoundBra+ | KRoundKet+ | KSquareBra+ | KSquareKet+ | KBraceBra+ | KBraceKet+ | KAngleBra+ | KAngleKet++ -- compound parens+ | KSquareColonBra+ | KSquareColonKet+ | KAngleColonBra+ | KAngleColonKet++ -- punctuation+ | KDot+ | KBar+ | KHat+ | KPlus+ | KColon+ | KComma+ | KBackSlash+ | KSemiColon+ | KUnderscore+ | KEquals+ | KAmpersand+ | KDash+ | KColonColon+ | KBigLambda++ -- symbolic constructors+ | KSortComp+ | KSortProp+ | KKindValue+ | KKindRegion+ | KKindEffect+ | KKindClosure+ | KKindWitness+ | KArrowTilde+ | KArrowDash+ | KArrowEquals++ -- bottoms+ | KBotEffect+ | KBotClosure++ -- expression keywords+ | KWith+ | KWhere+ | KIn+ | KLet+ | KLazy+ | KLetRec+ | KLetRegion+ | KWithRegion+ | KCase+ | KOf+ | KWeakEff+ | KWeakClo+ | KPurify+ | KForget++ -- debruijn indices+ | KIndex Int++ -- builtin names+ | KTwConBuiltin TwCon+ | KWbConBuiltin WbCon+ | KTcConBuiltin TcCon+ deriving (Eq, Show)+++-- | Describe a `TokAtom`, for parser error messages.+describeTokAtom :: TokAtom -> String+describeTokAtom ta+ = let (family, str) = describeTokAtom' ta+ in describeTokenFamily family ++ " " ++ show str++describeTokAtom' :: TokAtom -> (TokenFamily, String)+describeTokAtom' ta+ = case ta of+ -- parens+ KRoundBra -> (Symbol, "(")+ KRoundKet -> (Symbol, ")")+ KSquareBra -> (Symbol, "[")+ KSquareKet -> (Symbol, "]")+ KBraceBra -> (Symbol, "{")+ KBraceKet -> (Symbol, "}")+ KAngleBra -> (Symbol, "<")+ KAngleKet -> (Symbol, ">")++ -- compound parens+ KSquareColonBra -> (Symbol, "[:")+ KSquareColonKet -> (Symbol, ":]")+ KAngleColonBra -> (Symbol, "<:")+ KAngleColonKet -> (Symbol, ":>")++ -- punctuation+ KDot -> (Symbol, ".")+ KBar -> (Symbol, "|")+ KHat -> (Symbol, "^")+ KPlus -> (Symbol, "+")+ KColon -> (Symbol, ":")+ KComma -> (Symbol, ",")+ KBackSlash -> (Symbol, "\\")+ KSemiColon -> (Symbol, ";")+ KUnderscore -> (Symbol, "_")+ KEquals -> (Symbol, "=")+ KAmpersand -> (Symbol, "&")+ KDash -> (Symbol, "-")+ KColonColon -> (Symbol, "::")+ KBigLambda -> (Symbol, "/\\")++ -- symbolic constructors+ KSortComp -> (Constructor, "**")+ KSortProp -> (Constructor, "@@")+ KKindValue -> (Constructor, "*")+ KKindRegion -> (Constructor, "%")+ KKindEffect -> (Constructor, "!")+ KKindClosure -> (Constructor, "$")+ KKindWitness -> (Constructor, "@")+ KArrowTilde -> (Constructor, "~>")+ KArrowDash -> (Constructor, "->")+ KArrowEquals -> (Constructor, "=>")++ -- bottoms+ KBotEffect -> (Constructor, "!0")+ KBotClosure -> (Constructor, "!$")++ -- expression keywords+ KWith -> (Keyword, "with")+ KWhere -> (Keyword, "where")+ KIn -> (Keyword, "in")+ KLet -> (Keyword, "let")+ KLazy -> (Keyword, "lazy")+ KLetRec -> (Keyword, "letrec")+ KLetRegion -> (Keyword, "letregion")+ KWithRegion -> (Keyword, "withregion")+ KCase -> (Keyword, "case")+ KOf -> (Keyword, "of")+ KWeakEff -> (Keyword, "weakeff")+ KWeakClo -> (Keyword, "weakclo")+ KPurify -> (Keyword, "purify")+ KForget -> (Keyword, "forget")+ + -- debruijn indices+ KIndex i -> (Index, "^" ++ show i)++ -- builtin names+ KTwConBuiltin tw -> (Constructor, renderPlain $ ppr tw)+ KWbConBuiltin wi -> (Constructor, renderPlain $ ppr wi)+ KTcConBuiltin tc -> (Constructor, renderPlain $ ppr tc)+++-- TokNamed -------------------------------------------------------------------+-- | A token witn a user-defined name.+data TokNamed n+ = KCon n+ | KVar n+ | KLit n+ deriving (Eq, Show)+++-- | Describe a `TokNamed`, for parser error messages.+describeTokNamed :: Pretty n => TokNamed n -> String+describeTokNamed tn+ = case tn of+ KCon n -> renderPlain $ text "constructor" <+> (dquotes $ ppr n)+ KVar n -> renderPlain $ text "variable" <+> (dquotes $ ppr n)+ KLit n -> renderPlain $ text "literal" <+> (dquotes $ ppr n)+++-- | Apply a function to all the names in a `TokNamed`.+renameTokNamed + :: Ord n2+ => (n1 -> n2) -> TokNamed n1 -> TokNamed n2++renameTokNamed f kk+ = case kk of+ KCon c -> KCon $ f c+ KVar c -> KVar $ f c+ KLit c -> KLit $ f c+
+ DDC/Core/Predicates.hs view
@@ -0,0 +1,97 @@++-- | Simple predicates on core expressions.+module DDC.Core.Predicates+ ( -- * Atoms+ isXVar, isXCon+ , isAtomW, isAtomX++ -- * Lambdas+ , isXLAM, isXLam+ , isLambdaX++ -- * Applications+ , isXApp++ -- * Patterns+ , isPDefault)+where+import DDC.Core.Exp+import DDC.Type.Predicates+++-- Atoms ----------------------------------------------------------------------+-- | Check whether an expression is a variable.+isXVar :: Exp a n -> Bool+isXVar xx+ = case xx of+ XVar{} -> True+ _ -> False+++-- | Check whether an expression is a constructor.+isXCon :: Exp a n -> Bool+isXCon xx+ = case xx of+ XCon{} -> True+ _ -> False+++-- | Check whether a witness is a `WVar` or `WCon`.+isAtomW :: Witness n -> Bool+isAtomW ww+ = case ww of+ WVar{} -> True+ WCon{} -> True+ _ -> False+++-- | Check whether an expression is a `XVar` or an `XCon`, +-- or some type or witness atom.+isAtomX :: Exp a n -> Bool+isAtomX xx+ = case xx of+ XVar{} -> True+ XCon{} -> True+ XType t -> isAtomT t+ XWitness w -> isAtomW w+ _ -> False+++-- Lambdas --------------------------------------------------------------------+-- | Check whether an expression is a spec abstraction (level-1).+isXLAM :: Exp a n -> Bool+isXLAM xx+ = case xx of+ XLAM{} -> True+ _ -> False+++-- | Check whether an expression is a value or witness abstraction (level-0).+isXLam :: Exp a n -> Bool+isXLam xx+ = case xx of+ XLam{} -> True+ _ -> False+++-- | Check whether an expression is a spec, value, or witness abstraction.+isLambdaX :: Exp a n -> Bool+isLambdaX xx+ = isXLAM xx || isXLam xx+++-- Applications ---------------------------------------------------------------+-- | Check whether an expression is an `XApp`.+isXApp :: Exp a n -> Bool+isXApp xx+ = case xx of+ XApp{} -> True+ _ -> False+++-- Patterns -------------------------------------------------------------------+-- | Check whether an alternative is a `PDefault`.+isPDefault :: Pat n -> Bool+isPDefault PDefault = True+isPDefault _ = False+
+ DDC/Core/Pretty.hs view
@@ -0,0 +1,237 @@+-- | Pretty printing for core expressions.+module DDC.Core.Pretty + ( module DDC.Type.Pretty+ , module DDC.Base.Pretty)+where+import DDC.Core.Exp+import DDC.Core.Compounds+import DDC.Core.Predicates+import DDC.Type.Pretty+import DDC.Type.Compounds+import DDC.Type.Predicates+import DDC.Base.Pretty+++-- Binder ---------------------------------------------------------------------+-- | Pretty print a binder, adding spaces after names.+-- The RAnon and None binders don't need spaces, as they're single symbols.+pprBinderSep :: Pretty n => Binder n -> Doc+pprBinderSep bb+ = case bb of+ RName v -> ppr v+ RAnon -> text "^"+ RNone -> text "_"+++-- | Print a group of binders with the same type.+pprBinderGroup + :: (Pretty n, Eq n) + => Doc -> ([Binder n], Type n) -> Doc++pprBinderGroup lam (rs, t)+ = lam <> parens ((cat $ map pprBinderSep rs) <+> text ":" <+> ppr t) <> dot+++-- Exp ------------------------------------------------------------------------+instance (Pretty n, Eq n) => Pretty (Exp a n) where+ pprPrec d xx+ = case xx of+ XVar _ u -> ppr u+ XCon _ tc -> ppr tc+ + XLAM{}+ -> let Just (bs, xBody) = takeXLAMs xx+ groups = partitionBindsByType bs+ in pprParen' (d > 1)+ $ (cat $ map (pprBinderGroup (text "/\\")) groups)+ <> (if isXLAM xBody then empty+ else if isXLam xBody then line <> space+ else if isSimpleX xBody then space+ else line)+ <> ppr xBody++ XLam{}+ -> let Just (bs, xBody) = takeXLams xx+ groups = partitionBindsByType bs+ in pprParen' (d > 1)+ $ (cat $ map (pprBinderGroup (text "\\")) groups) + <> breakWhen (not $ isSimpleX xBody)+ <> ppr xBody++ XApp _ x1 x2+ -> pprParen' (d > 10)+ $ pprPrec 10 x1 + <> nest 4 (breakWhen (not $ isSimpleX x2) + <> pprPrec 11 x2)++ XLet _ lts x+ -> pprParen' (d > 2)+ $ ppr lts <+> text "in"+ <$> ppr x++ XCase _ x alts+ -> pprParen' (d > 2) + $ (nest 2 $ text "case" <+> ppr x <+> text "of" <+> lbrace <> line+ <> (vcat $ punctuate semi $ map ppr alts))+ <> line + <> rbrace++ XCast _ cc x+ -> pprParen' (d > 2)+ $ ppr cc <+> text "in"+ <$> ppr x++ XType t -> text "[" <> ppr t <> text "]"+ XWitness w -> text "<" <> ppr w <> text ">"+++-- Pat ------------------------------------------------------------------------+instance (Pretty n, Eq n) => Pretty (Pat n) where+ ppr pp+ = case pp of+ PDefault -> text "_"+ PData u bs -> ppr u <+> sep (map pprPatBind bs)+++-- | Pretty print a binder, +-- showing its type annotation only if it's not bottom.+pprPatBind :: (Eq n, Pretty n) => Bind n -> Doc+pprPatBind b+ | isBot (typeOfBind b) = ppr $ binderOfBind b+ | otherwise = parens $ ppr b+++-- Alt ------------------------------------------------------------------------+instance (Pretty n, Eq n) => Pretty (Alt a n) where+ ppr (AAlt p x)+ = ppr p <+> nest 1 (line <> nest 3 (text "->" <+> ppr x))+++-- Cast -----------------------------------------------------------------------+instance (Pretty n, Eq n) => Pretty (Cast n) where+ ppr cc+ = case cc of+ CastWeakenEffect eff + -> text "weakeff" <+> brackets (ppr eff)++ CastWeakenClosure clo+ -> text "weakclo" <+> brackets (ppr clo)++ CastPurify w+ -> text "purify" <+> angles (ppr w)++ CastForget w+ -> text "forget" <+> angles (ppr w)+++-- Lets -----------------------------------------------------------------------+instance (Pretty n, Eq n) => Pretty (Lets a n) where+ ppr lts+ = case lts of+ LLet m b x+ -> let dBind = if isBot (typeOfBind b)+ then ppr (binderOfBind b)+ else ppr b+ in text "let"+ <+> align ( dBind <> ppr m+ <> nest 2 ( breakWhen (not $ isSimpleX x)+ <> text "=" <+> align (ppr x)))++ LRec bxs+ -> let pprLetRecBind (b, x)+ = ppr (binderOfBind b)+ <+> text ":"+ <+> ppr (typeOfBind b)+ <> nest 2 ( breakWhen (not $ isSimpleX x)+ <> text "=" <+> align (ppr x))+ + in (nest 2 $ text "letrec"+ <+> lbrace + <> ( line + <> (vcat $ punctuate (semi <> line)+ $ map pprLetRecBind bxs)))+ <$> rbrace+++ LLetRegion b []+ -> text "letregion"+ <+> ppr (binderOfBind b)++ LLetRegion b bs+ -> text "letregion"+ <+> ppr (binderOfBind b)+ <+> text "with"+ <+> braces (cat $ punctuate (text "; ") $ map ppr bs)++ LWithRegion b+ -> text "withregion"+ <+> 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+ pprPrec d ww+ = case ww of+ WVar n -> ppr n+ WCon wc -> ppr wc++ WApp w1 w2+ -> pprParen (d > 10) (ppr w1 <+> pprPrec 11 w2)+ + WJoin w1 w2+ -> pprParen (d > 9) (ppr w1 <+> text "&" <+> ppr w2)++ WType t -> text "[" <> ppr t <> text "]"+++instance (Pretty n, Eq n) => Pretty (WiCon n) where+ ppr wc+ = case wc of+ WiConBuiltin wb -> ppr wb+ WiConBound u -> ppr u+++instance Pretty WbCon where+ ppr wb+ = case wb of+ WbConPure -> text "pure"+ WbConEmpty -> text "empty"+ WbConUse -> text "use"+ WbConRead -> text "read"+ WbConAlloc -> text "alloc"+++-- Utils ----------------------------------------------------------------------+breakWhen :: Bool -> Doc+breakWhen True = line+breakWhen False = space+++isSimpleX :: Exp a n -> Bool+isSimpleX xx+ = case xx of+ XVar{} -> True+ XCon{} -> True+ XType{} -> True+ XWitness{} -> True+ XApp _ x1 x2 -> isSimpleX x1 && isAtomX x2+ _ -> False+++parens' :: Doc -> Doc+parens' d = lparen <> nest 1 d <> rparen+++-- | Wrap a `Doc` in parens if the predicate is true.+pprParen' :: Bool -> Doc -> Doc+pprParen' b c+ = if b then parens' c+ else c
+ DDC/Core/Transform/LiftW.hs view
@@ -0,0 +1,116 @@++-- | Lift deBruijn indices in witnesses.+module DDC.Core.Transform.LiftW+ (LiftW(..))+where+import DDC.Core.Exp+++class LiftW (c :: * -> *) where+ -- | Lift indices that are at least a the given depth by some number+ -- of levels+ liftAtDepthW+ :: forall n. Ord n+ => Int -- ^ Number of levels to lift.+ -> Int -- ^ Current binding depth.+ -> c n -- ^ Lift witness variable indices in this thing.+ -> c n+ + -- | Wrapper for `liftAtDepthX` that starts at depth 0. + liftW :: forall n. Ord n+ => Int -- ^ Number of levels to lift.+ -> c n -- ^ Lift witness variable indices in this thing.+ -> c n+ + liftW n xx = liftAtDepthW n 0 xx+ ++instance LiftW Bound where+ liftAtDepthW n d uu+ = case uu of+ UName{} -> uu+ UPrim{} -> uu+ UIx i t + | d <= i -> UIx (i + n) t+ | otherwise -> uu+++instance LiftW (Exp a) where+ liftAtDepthW n d xx+ = let down = liftAtDepthW n d+ in case xx of+ XVar{} -> xx+ XCon{} -> xx+ XApp a x1 x2 -> XApp a (down x1) (down x2)+ XLAM a b x -> XLAM a b (down x)+ XLam a b x -> XLam a b (liftAtDepthW n (d + 1) x)+ + XLet a lets x + -> let (lets', levels) = liftAtDepthXLets n d lets + in XLet a lets' (liftAtDepthW n (d + levels) x)++ XCase a x alts -> XCase a (down x) (map down alts)+ XCast a cc x -> XCast a cc (down x)+ XType{} -> xx+ XWitness w -> XWitness (down w)+ ++instance LiftW LetMode where+ liftAtDepthW n d m+ = case m of+ LetStrict -> m+ LetLazy Nothing -> m+ LetLazy (Just w) -> LetLazy (Just $ liftAtDepthW n d w)+++instance LiftW (Alt a) where+ liftAtDepthW n d (AAlt p x)+ = case p of+ PDefault + -> AAlt PDefault (liftAtDepthW n d x)++ PData _ bs + -> let d' = d + countBAnons bs+ in AAlt p (liftAtDepthW n d' x)+++instance LiftW Witness where+ liftAtDepthW n d ww+ = let down = liftAtDepthW n 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+ ++liftAtDepthXLets+ :: forall a n. Ord n+ => Int -- ^ Number of levels to lift.+ -> Int -- ^ Current binding depth.+ -> Lets a n -- ^ Lift exp indices in this thing.+ -> (Lets a n, Int) -- ^ Lifted, and how much to increase depth by++liftAtDepthXLets n d lts+ = case lts of+ LLet m b x+ -> let m' = liftAtDepthW n d m+ inc = countBAnons [b]+ x' = liftAtDepthW n (d+inc) x+ in (LLet m' b x', inc)++ LRec bs+ -> let inc = countBAnons (map fst bs)+ bs' = map (\(b,e) -> (b, liftAtDepthW n (d+inc) e)) bs+ in (LRec bs', inc)++ LLetRegion _b bs -> (lts, countBAnons bs)+ LWithRegion _ -> (lts, 0)+++countBAnons = length . filter isAnon+ where isAnon (BAnon _) = True+ isAnon _ = False++
+ DDC/Core/Transform/LiftX.hs view
@@ -0,0 +1,96 @@++-- | Lift deBruijn indices in expressions.+module DDC.Core.Transform.LiftX+ (LiftX(..))+where+import DDC.Core.Exp+++class LiftX (c :: * -> *) where+ -- | Lift indices that are at least the given depth by some number+ -- of levels.+ liftAtDepthX+ :: forall n. Ord n+ => Int -- ^ Number of levels to lift.+ -> Int -- ^ Current binding depth.+ -> c n -- ^ Lift expression indices in this thing.+ -> c n+ + -- | Wrapper for `liftAtDepthX` that starts at depth 0. + liftX :: forall n. Ord n+ => Int -- ^ Number of levels to lift.+ -> c n -- ^ Lift expression indices in this thing.+ -> c n+ + liftX n xx = liftAtDepthX n 0 xx+ ++instance LiftX Bound where+ liftAtDepthX n d uu+ = case uu of+ UName{} -> uu+ UPrim{} -> uu+ UIx i t + | d <= i -> UIx (i + n) t+ | otherwise -> uu+++instance LiftX (Exp a) where+ liftAtDepthX n d xx+ = let down = liftAtDepthX n d+ in case xx of+ XVar a u -> XVar a (down u)+ XCon{} -> xx+ XApp a x1 x2 -> XApp a (down x1) (down x2)+ XLAM a b x -> XLAM a b (down x)+ XLam a b x -> XLam a b (liftAtDepthX n (d + 1) x)+ + XLet a lets x + -> let (lets', levels) = liftAtDepthXLets n d lets + in XLet a lets' (liftAtDepthX n (d + levels) x)++ XCase a x alts -> XCase a (down x) (map down alts)+ XCast a cc x -> XCast a cc (down x)+ XType{} -> xx+ XWitness{} -> xx+ ++instance LiftX (Alt a) where+ liftAtDepthX n d (AAlt p x)+ = case p of+ PDefault + -> AAlt PDefault (liftAtDepthX n d x)++ PData _ bs + -> let d' = d + countBAnons bs+ in AAlt p (liftAtDepthX n d' x)+ ++liftAtDepthXLets+ :: forall a n. Ord n+ => Int -- ^ Number of levels to lift.+ -> Int -- ^ Current binding depth.+ -> Lets a n -- ^ Lift exp indices in this thing.+ -> (Lets a n, Int) -- ^ Lifted, and how much to increase depth by++liftAtDepthXLets n d lts+ = case lts of+ LLet m b x+ -> let inc = countBAnons [b]+ x' = liftAtDepthX n (d+inc) x+ in (LLet m b x', inc)++ LRec bs+ -> let inc = countBAnons (map fst bs)+ bs' = map (\(b,e) -> (b, liftAtDepthX n (d+inc) e)) bs+ in (LRec bs', inc)++ LLetRegion _b bs -> (lts, countBAnons bs)+ LWithRegion _ -> (lts, 0)+++countBAnons = length . filter isAnon+ where isAnon (BAnon _) = True+ isAnon _ = False++
+ DDC/Core/Transform/SpreadX.hs view
@@ -0,0 +1,152 @@++-- | Spread type annotations from binders and the environment into bound+-- occurrences of variables and constructors.+module DDC.Core.Transform.SpreadX+ (SpreadX(..))+where+import DDC.Core.Exp+import DDC.Core.Compounds+import DDC.Type.Transform.SpreadT+import DDC.Type.Env (Env)+import qualified DDC.Type.Env as Env+++class SpreadX (c :: * -> *) where++ -- | Spread type annotations from binders and the environment into bound+ -- occurrences of variables and constructors.+ --+ -- Also convert `Bound`s to `UPrim` form if the environment says that+ -- they are primitive.+ spreadX :: forall n. Ord n+ => Env n -> Env n -> c n -> c n+++instance SpreadX (Exp a) where+ spreadX kenv tenv xx + = let down = spreadX kenv tenv + in case xx of+ XVar a u -> XVar a (down u)+ XCon a u -> XCon a (down u)+ XApp a x1 x2 -> XApp a (down x1) (down x2)++ XLAM a b x+ -> let b' = spreadT kenv b+ in XLAM a b' (spreadX (Env.extend b' kenv) tenv x)++ XLam a b x + -> let b' = down b+ in XLam a b' (spreadX kenv (Env.extend b' tenv) x)+ + XLet a lts x+ -> let lts' = down lts+ kenv' = Env.extends (specBindsOfLets lts') kenv+ tenv' = Env.extends (valwitBindsOfLets lts') tenv+ in XLet a lts' (spreadX kenv' tenv' x)+ + XCase a x alts -> XCase a (down x) (map down alts)+ XCast a c x -> XCast a (down c) (down x)+ XType t -> XType (spreadT kenv t)+ XWitness w -> XWitness (down w)+++instance SpreadX Cast where+ spreadX kenv tenv cc+ = let down = spreadX kenv tenv + in case cc of+ CastWeakenEffect eff -> CastWeakenEffect (spreadT kenv eff)+ CastWeakenClosure clo -> CastWeakenClosure (spreadT kenv clo)+ CastPurify w -> CastPurify (down w)+ CastForget w -> CastForget (down w)+++instance SpreadX Pat where+ spreadX kenv tenv pat+ = let down = spreadX kenv tenv+ in case pat of+ PDefault -> PDefault+ PData u bs -> PData (down u) (map down bs)+++instance SpreadX (Alt a) where+ spreadX kenv tenv alt+ = case alt of+ AAlt p x+ -> let p' = spreadX kenv tenv p+ tenv' = Env.extends (bindsOfPat p') tenv+ in AAlt p' (spreadX kenv tenv' x)+++instance SpreadX (Lets a) where+ spreadX kenv tenv lts+ = let down = spreadX kenv tenv+ in case lts of+ LLet m b x -> LLet (down m) (down b) (down x)+ + LRec bxs+ -> let (bs, xs) = unzip bxs+ bs' = map (spreadX kenv tenv) bs+ tenv' = Env.extends bs' tenv+ xs' = map (spreadX kenv tenv') xs+ in LRec (zip bs' xs')++ LLetRegion b bs+ -> let b' = spreadT kenv b+ kenv' = Env.extend b' kenv+ bs' = map (spreadX kenv' tenv) bs+ in LLetRegion b' bs'++ LWithRegion b+ -> 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+ 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)+++instance SpreadX WiCon where+ spreadX kenv tenv wc+ = let down = spreadX kenv tenv+ in case wc of+ WiConBound u -> WiConBound (down u)+ WiConBuiltin{} -> wc+++instance SpreadX Bind where+ spreadX kenv _tenv bb+ = case bb of+ BName n t -> BName n (spreadT kenv t)+ BAnon t -> BAnon (spreadT kenv t)+ BNone t -> BNone (spreadT kenv t)+++instance SpreadX Bound where+ spreadX kenv tenv uu+ | Just t' <- Env.lookup uu tenv+ = case uu of+ UIx ix _ -> UIx ix t'+ UPrim n _ -> UPrim n t'++ UName n _+ -> if Env.isPrim tenv n + then UPrim n (spreadT kenv t')+ else UName n (spreadT kenv t')++ | otherwise = uu ++
+ DDC/Core/Transform/SubstituteTX.hs view
@@ -0,0 +1,172 @@++-- | Capture avoiding substitution of types in expressions. +--+-- If a binder would capture a variable then it is anonymized+-- to deBruijn form.+module DDC.Core.Transform.SubstituteTX+ ( substituteTX+ , substituteTXs+ , substituteBoundTX+ , SubstituteTX(..))+where+import DDC.Core.Collect+import DDC.Core.Exp+import DDC.Type.Compounds+import DDC.Type.Transform.SubstituteT+import DDC.Type.Rewrite+import Data.Maybe+import qualified Data.Set as Set+import qualified DDC.Type.Env as Env+++-- | Substitute a `Type` for the `Bound` corresponding to some `Bind` in a thing.+substituteTX :: (SubstituteTX c, Ord n) => Bind n -> Type n -> c n -> c n+substituteTX b t x+ = case takeSubstBoundOfBind b of+ Just u -> substituteBoundTX u t x+ _ -> x+++-- | Wrapper for `substituteT` to substitute multiple types.+substituteTXs :: (SubstituteTX c, Ord n) => [(Bind n, Type n)] -> c n -> c n+substituteTXs bts x+ = foldr (uncurry substituteTX) x bts+++-- | Substitute a `Type` for a `Bound` in some thing.+substituteBoundTX :: (SubstituteTX c, Ord n) => Bound n -> Type n -> c n -> c n+substituteBoundTX u tArg xx+ = substituteWithTX tArg+ ( Sub + { subBound = u++ -- Rewrite level-1 binders that have the same name as any+ -- of the free variables in the expression to substitute.+ , subConflict1 + = Set.fromList+ $ (mapMaybe takeNameOfBound $ Set.toList $ freeT Env.empty tArg) ++ -- Rewrite level-0 binders that have the same name as any+ -- of the free variables in the expression to substitute.+ , subConflict0 = Set.empty+ , subStack1 = BindStack [] [] 0 0+ , subStack0 = BindStack [] [] 0 0+ , subShadow0 = False })+ xx+++-------------------------------------------------------------------------------+class SubstituteTX (c :: * -> *) where+ substituteWithTX+ :: forall n. Ord n+ => Type n -> Sub n -> c n -> c n+++instance SubstituteTX (Exp a) where + substituteWithTX tArg sub xx+ = let down = substituteWithTX tArg+ in case xx of+ XVar a u -> XVar a (down sub u)+ XCon{} -> xx+ XApp a x1 x2 -> XApp a (down sub x1) (down sub x2)++ XLAM a b x+ -> let (sub1, b') = bind1 sub b+ x' = down sub1 x+ in XLAM a b' x'++ XLam a b x+ -> let (sub1, b') = bind0 sub (down sub b)+ 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+ (sub1, b') = bind0 sub (down sub b)+ x2' = down sub1 x2+ in XLet a (LLet m' b' x1') x2'++ XLet a (LRec bxs) x2+ -> let (bs, xs) = unzip bxs+ (sub1, bs') = bind0s sub (map (down sub) bs)+ xs' = map (down sub1) xs+ x2' = down sub1 x2+ in XLet a (LRec (zip bs' xs')) x2'++ XLet a (LLetRegion b bs) x2+ -> let (sub1, b') = bind1 sub b+ (sub2, bs') = bind0s sub1 (map (down sub1) bs)+ x2' = down sub2 x2+ in XLet a (LLetRegion b' bs') x2'++ XLet a (LWithRegion uR) x2+ -> XLet a (LWithRegion uR) (down sub x2)++ XCase a x1 alts -> XCase a (down sub x1) (map (down sub) alts)+ XCast a cc x1 -> XCast a (down sub cc) (down sub x1)+ XType t -> XType (down sub t)+ XWitness w -> XWitness (down sub w)+++instance SubstituteTX LetMode where+ substituteWithTX tArg sub lm+ = let down = substituteWithTX tArg+ 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 = substituteWithTX tArg+ in case aa of+ AAlt PDefault xBody+ -> AAlt PDefault $ down sub xBody+ + AAlt (PData uCon bs) x+ -> let (sub1, bs') = bind0s sub (map (down sub) bs)+ x' = down sub1 x+ in AAlt (PData uCon bs') x'+++instance SubstituteTX Cast where+ substituteWithTX tArg sub cc+ = let down = substituteWithTX tArg+ in case cc of+ CastWeakenEffect eff -> CastWeakenEffect (down sub eff)+ CastWeakenClosure clo -> CastWeakenClosure (down sub clo)+ CastPurify w -> CastPurify (down sub w)+ CastForget w -> CastForget (down sub w)+++instance SubstituteTX Witness where+ substituteWithTX tArg sub ww+ = let down = substituteWithTX tArg+ in case ww of+ WVar u -> WVar (down 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)+++instance SubstituteTX Bind where+ substituteWithTX tArg sub bb+ = replaceTypeOfBind (substituteWithTX tArg sub (typeOfBind bb)) bb+++instance SubstituteTX Bound where+ substituteWithTX tArg sub uu+ = replaceTypeOfBound (substituteWithTX tArg sub (typeOfBound uu)) uu+++instance SubstituteTX Type where+ substituteWithTX tArg sub tt+ = substituteWithT+ (subBound sub)+ tArg+ (subConflict1 sub)+ (subStack1 sub)+ tt
+ DDC/Core/Transform/SubstituteWX.hs view
@@ -0,0 +1,182 @@++-- | Capture avoiding substitution of witnesses in expressions.+--+-- If a binder would capture a variable then it is anonymized+-- to deBruijn form.+module DDC.Core.Transform.SubstituteWX+ ( SubstituteWX(..)+ , substituteWX+ , substituteWXs)+where+import DDC.Core.Exp+import DDC.Core.Collect+import DDC.Core.Transform.LiftW+import DDC.Type.Compounds+import DDC.Type.Rewrite+import Data.Maybe+import qualified DDC.Type.Env as Env+import qualified Data.Set as Set+++-- | Wrapper for `substituteWithW` that determines the set of free names in the+-- type being substituted, and starts with an empty binder stack.+substituteWX + :: (Ord n, SubstituteWX c) + => Bind n -> Witness n -> c n -> c n++substituteWX b wArg xx+ | Just u <- takeSubstBoundOfBind b+ = substituteWithWX wArg+ ( Sub + { subBound = u++ -- Rewrite level-1 binders that have the same name as any+ -- of the free variables in the expression to substitute.+ , subConflict1 + = Set.fromList+ $ (mapMaybe takeNameOfBound $ Set.toList $ freeT Env.empty wArg) ++ -- Rewrite level-0 binders that have the same name as any+ -- of the free variables in the expression to substitute.+ , subConflict0+ = Set.fromList+ $ mapMaybe takeNameOfBound + $ Set.toList + $ freeX Env.empty wArg+ + , subStack1 = BindStack [] [] 0 0+ , subStack0 = BindStack [] [] 0 0+ , subShadow0 = False })+ xx++ | otherwise = xx+ ++-- | Wrapper for `substituteW` to substitute multiple things.+substituteWXs + :: (Ord n, SubstituteWX c) + => [(Bind n, Witness n)] -> c n -> c n+substituteWXs bts x+ = foldr (uncurry substituteWX) x bts+++class SubstituteWX (c :: * -> *) where++ -- | Substitute a witness into some thing.+ -- In the target, if we find a named binder that would capture a free variable+ -- in the type to substitute, then we rewrite that binder to anonymous form,+ -- avoiding the capture.+ substituteWithWX+ :: forall n. Ord n+ => Witness n -> Sub n -> c n -> c n+++instance SubstituteWX (Exp a) where + substituteWithWX wArg sub xx+ = let down = substituteWithWX wArg+ into = rewriteWith+ in case xx of+ XVar a u -> XVar a (into sub u)+ XCon{} -> xx+ XApp a x1 x2 -> XApp a (down sub x1) (down sub x2)++ XLAM a b x+ -> let (sub1, b') = bind1 sub b+ x' = down sub1 x+ in XLAM a b' x'++ XLam a b x+ -> let (sub1, b') = bind0 sub b+ 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+ (sub1, b') = bind0 sub b+ x2' = down sub1 x2+ in XLet a (LLet m' b' x1') x2'++ XLet a (LRec bxs) x2+ -> let (bs, xs) = unzip bxs+ (sub1, bs') = bind0s sub bs+ xs' = map (down sub1) xs+ x2' = down sub1 x2+ in XLet a (LRec (zip bs' xs')) x2'++ XLet a (LLetRegion b bs) x2+ -> let (sub1, b') = bind1 sub b+ (sub2, bs') = bind0s sub1 bs+ x2' = down sub2 x2+ in XLet a (LLetRegion b' bs') x2'++ XLet a (LWithRegion uR) x2+ -> XLet a (LWithRegion uR) (down sub x2)++ XCase a x1 alts -> XCase a (down sub x1) (map (down sub) alts)+ XCast a cc x1 -> XCast a (down sub cc) (down sub x1)+ XType t -> XType (into sub t)+ XWitness w -> XWitness (down sub w)++++instance SubstituteWX LetMode where+ substituteWithWX wArg sub lm+ = let down = substituteWithWX wArg+ in case lm of+ LetStrict -> lm+ LetLazy Nothing -> LetLazy Nothing+ LetLazy (Just w) -> LetLazy (Just (down sub w))+++instance SubstituteWX (Alt a) where+ substituteWithWX wArg sub aa+ = let down = substituteWithWX wArg+ in case aa of+ AAlt PDefault xBody+ -> AAlt PDefault $ down sub xBody+ + AAlt (PData uCon bs) x+ -> let (sub1, bs') = bind0s sub bs+ x' = down sub1 x+ in AAlt (PData uCon bs') x'+++instance SubstituteWX Cast where+ substituteWithWX wArg sub cc+ = let down = substituteWithWX wArg+ into = rewriteWith+ in case cc of+ CastWeakenEffect eff -> CastWeakenEffect (into sub eff)+ CastWeakenClosure clo -> CastWeakenClosure (into sub clo)+ CastPurify w -> CastPurify (down sub w)+ CastForget w -> CastForget (down sub w)+++instance SubstituteWX Witness where+ substituteWithWX wArg sub ww+ = let down = substituteWithWX wArg+ into = rewriteWith+ in case ww of+ WVar u+ -> case substW wArg sub u of+ Left u' -> WVar (into sub 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)+++-- | Rewrite or substitute into a witness variable.+substW :: Ord n => Witness n -> Sub n -> Bound n + -> Either (Bound n) (Witness n)++substW wArg sub u+ = case substBound (subStack0 sub) (subBound sub) u of+ Left u' -> Left (rewriteWith sub u')+ Right n + | not $ subShadow0 sub -> Right (liftW n wArg)+ | otherwise -> Left (rewriteWith sub u)+
+ DDC/Core/Transform/SubstituteXX.hs view
@@ -0,0 +1,176 @@++-- | Capture avoiding substitution of expressions in expressions.+--+-- If a binder would capture a variable then it is anonymized+-- to deBruijn form.+module DDC.Core.Transform.SubstituteXX+ ( SubstituteXX(..)+ , substituteXX+ , substituteXXs+ , substituteXArg+ , substituteXArgs)+where+import DDC.Core.Exp+import DDC.Core.Collect+import DDC.Core.Transform.LiftX+import DDC.Type.Compounds+import DDC.Core.Transform.SubstituteWX+import DDC.Core.Transform.SubstituteTX+import DDC.Type.Transform.SubstituteT+import DDC.Type.Rewrite+import Data.Maybe+import qualified DDC.Type.Env as Env+import qualified Data.Set as Set+++-- | Wrapper for `substituteWithX` that determines the set of free names in the+-- expression being substituted, and starts with an empty binder stack.+substituteXX + :: (Ord n, SubstituteXX c)+ => Bind n -> Exp a n -> c a n -> c a n++substituteXX b xArg xx+ | Just u <- takeSubstBoundOfBind b+ = substituteWithXX xArg+ ( Sub + { subBound = u++ -- Rewrite level-1 binders that have the same name as any+ -- of the free variables in the expression to substitute, + -- or any level-1 binders that expression binds itself.+ , subConflict1 + = Set.fromList+ $ (mapMaybe takeNameOfBound $ Set.toList $ freeT Env.empty xArg) + ++ (mapMaybe takeNameOfBind $ collectSpecBinds xArg)++ -- Rewrite level-0 binders that have the same name as any+ -- of the free variables in the expression to substitute.+ , subConflict0+ = Set.fromList+ $ mapMaybe takeNameOfBound + $ Set.toList + $ freeX Env.empty xArg+ + , subStack1 = BindStack [] [] 0 0+ , subStack0 = BindStack [] [] 0 0+ , subShadow0 = False })+ xx++ | otherwise = xx+++-- | Wrapper for `substituteX` to substitute multiple expressions.+substituteXXs + :: (Ord n, SubstituteXX c)+ => [(Bind n, Exp a n)] -> c a n -> c a n+substituteXXs bts x+ = foldr (uncurry substituteXX) x bts+++-- | Substitute the argument of an application into an expression.+-- Perform type substitution for an `XType` +-- and witness substitution for an `XWitness`+substituteXArg + :: (Ord n, SubstituteXX c, SubstituteWX (c a), SubstituteTX (c a))+ => Bind n -> Exp a n -> c a n -> c a n++substituteXArg b arg x+ = case arg of+ XType t -> substituteTX b t x+ XWitness w -> substituteWX b w x+ _ -> substituteXX b arg x+++-- | Wrapper for `substituteXArgs` to substitute multiple arguments.+substituteXArgs+ :: (Ord n, SubstituteXX c, SubstituteWX (c a), SubstituteTX (c a))+ => [(Bind n, Exp a n)] -> c a n -> c a n++substituteXArgs bas x+ = foldr (uncurry substituteXArg) x bas+++-------------------------------------------------------------------------------+class SubstituteXX (c :: * -> * -> *) where+ substituteWithXX + :: forall a n. Ord n + => Exp a n -> Sub n -> c a n -> c a n +++instance SubstituteXX Exp where + substituteWithXX xArg sub xx+ = let down = substituteWithXX xArg+ into = rewriteWith+ in case xx of+ XVar a u+ -> case substX xArg sub u of+ Left u' -> XVar a (into sub u')+ Right x -> x++ XCon{} -> xx+ XApp a x1 x2 -> XApp a (down sub x1) (down sub x2)++ XLAM a b x+ -> let (sub1, b') = bind1 sub b+ x' = down sub1 x+ in XLAM a b' x'++ XLam a b x+ -> let (sub1, b') = bind0 sub b+ 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+ (sub1, b') = bind0 sub b+ x2' = down sub1 x2+ in XLet a (LLet m' b' x1') x2'++ XLet a (LRec bxs) x2+ -> let (bs, xs) = unzip bxs+ (sub1, bs') = bind0s sub bs+ xs' = map (down sub1) xs+ x2' = down sub1 x2+ in XLet a (LRec (zip bs' xs')) x2'++ XLet a (LLetRegion b bs) x2+ -> let (sub1, b') = bind1 sub b+ (sub2, bs') = bind0s sub1 bs+ x2' = down sub2 x2+ in XLet a (LLetRegion b' bs') x2'++ XLet a (LWithRegion uR) x2+ -> XLet a (LWithRegion uR) (down sub x2)++ XCase a x1 alts -> XCase a (down sub x1) (map (down sub) alts)+ XCast a cc x1 -> XCast a (into sub cc) (down sub x1)+ XType t -> XType (into sub t)+ XWitness w -> XWitness (into sub w)+ ++instance SubstituteXX Alt where+ substituteWithXX xArg sub aa+ = let down = substituteWithXX xArg+ in case aa of+ AAlt PDefault xBody+ -> AAlt PDefault $ down sub xBody+ + AAlt (PData uCon bs) x+ -> let (sub1, bs') = bind0s sub bs+ x' = down sub1 x+ in AAlt (PData uCon bs') x'+++-- | Rewrite or substitute into an expression variable.+substX :: Ord n => Exp a n -> Sub n -> Bound n + -> Either (Bound n) (Exp a n)++substX xArg sub u+ = case substBound (subStack0 sub) (subBound sub) u of+ Left u' -> Left (rewriteWith sub u')+ Right n + | not $ subShadow0 sub -> Right (liftX n xArg)+ | otherwise -> Left (rewriteWith sub u)++
+ DDC/Type/Check.hs view
@@ -0,0 +1,178 @@+-- | Check the kind of a type.+module DDC.Type.Check+ ( -- * Kinds of Types+ checkType+ , kindOfType++ -- * Kinds of Constructors+ , takeSortOfKiCon+ , kindOfTwCon+ , kindOfTcCon+ + -- * Errors+ , Error(..))+where+import DDC.Type.Check.CheckError+import DDC.Type.Check.CheckCon+import DDC.Type.Compounds+import DDC.Type.Predicates+import DDC.Type.Transform.LiftT+import DDC.Type.Exp+import DDC.Base.Pretty+import Data.List+import Control.Monad+import DDC.Type.Check.Monad (throw, result)+import DDC.Type.Pretty ()+import DDC.Type.Env (Env)+import qualified DDC.Type.Sum as TS+import qualified DDC.Type.Env as Env+import qualified DDC.Type.Check.Monad as G+++-- | The type checker monad.+type CheckM n = G.CheckM (Error n)+++-- Wrappers -------------------------------------------------------------------+-- | Check a type in the given environment, returning an error or its kind.+checkType :: (Ord n, Pretty n) => Env n -> Type n -> Either (Error n) (Kind n)+checkType env tt = result $ checkTypeM env tt+++-- | Check a type in an empty environment, returning an error or its kind.+kindOfType :: (Ord n, Pretty n) => Type n -> Either (Error n) (Kind n)+kindOfType tt = result $ checkTypeM Env.empty tt+++-- checkType ------------------------------------------------------------------+-- | Check a type, returning its kind.+---+-- Note that when comparing kinds, we can just use plain equality+-- (==) instead of equivT. This is because kinds do not contain quantifiers+-- that need to be compared up to alpha-equivalence, nor do they contain+-- crushable components terms.+checkTypeM :: (Ord n, Pretty n) => Env n -> Type n -> CheckM n (Kind n)+checkTypeM env tt+ = -- trace (pretty $ text "checkTypeM:" <+> ppr tt) $+ checkTypeM' env tt++-- Variables ------------------+checkTypeM' env (TVar u)+ = do let tBound = typeOfBound u+ let mtEnv = Env.lookup u env++ let mkResult+ -- If the annot is Bot then just use the type+ -- from the environment.+ | Just tEnv <- mtEnv+ , isBot tBound+ = return tEnv++ -- The bound has an explicit type annotation,+ -- which matches the one from the environment.+ -- + -- When the bound is a deBruijn index we need to lift the+ -- annotation on the original binder through any lambdas+ -- between the binding occurrence and the use.+ | Just tEnv <- mtEnv+ , UIx i _ <- u+ , tBound == liftT (i + 1) tEnv+ = return tBound++ -- The bound has an explicit type annotation,+ -- that matches the one from the environment.+ | Just tEnv <- mtEnv+ , tBound == tEnv+ = return tBound++ -- The bound has an explicit type annotation,+ -- that does not match the one from the environment. + | Just tEnv <- mtEnv+ = throw $ ErrorVarAnnotMismatch u tEnv++ -- Type variables must be in the environment.+ | _ <- mtEnv+ = throw $ ErrorUndefined u++ mkResult++-- Constructors ---------------+checkTypeM' _env tt@(TCon tc)+ = case tc of+ -- Sorts don't have a higher classification.+ TyConSort _ -> throw $ ErrorNakedSort tt++ -- Can't sort check a naked kind function+ -- because the sort depends on the argument kinds.+ TyConKind kc+ -> case takeSortOfKiCon kc of+ Just s -> return s+ Nothing -> throw $ ErrorUnappliedKindFun++ TyConWitness tcw -> return $ kindOfTwCon tcw+ TyConSpec tcc -> return $ kindOfTcCon tcc+ TyConBound u -> return $ typeOfBound u+++-- Quantifiers ----------------+checkTypeM' env tt@(TForall b1 t2)+ = do _ <- checkTypeM env (typeOfBind b1)+ k2 <- checkTypeM (Env.extend b1 env) t2++ -- The body must have data or witness kind.+ when ( (not $ isDataKind k2)+ && (not $ isWitnessKind k2))+ $ throw $ ErrorForallKindInvalid tt t2 k2++ return k2++-- Applications ---------------+-- Applications of the kind function constructor are handled directly+-- because the constructor doesn't have a sort by itself.+checkTypeM' env (TApp (TApp (TCon (TyConKind KiConFun)) k1) k2)+ = do _ <- checkTypeM env k1+ s2 <- checkTypeM env k2+ return s2++-- The implication constructor is overloaded and can have the+-- following kinds:+-- (=>) :: @ ~> @ ~> @, for witness implication.+-- (=>) :: @ ~> * ~> *, for a context.+checkTypeM' env tt@(TApp (TApp (TCon (TyConWitness TwConImpl)) t1) t2)+ = do k1 <- checkTypeM env t1+ k2 <- checkTypeM env t2+ if isWitnessKind k1 && isWitnessKind k2+ then return kWitness+ else if isWitnessKind k1 && isDataKind k2+ then return kData+ else throw $ ErrorWitnessImplInvalid tt t1 k1 t2 k2++-- Type application.+checkTypeM' env tt@(TApp t1 t2)+ = do k1 <- checkTypeM env t1+ k2 <- checkTypeM env t2+ case k1 of+ TApp (TApp (TCon (TyConKind KiConFun)) k11) k12+ | k11 == k2 -> return k12+ | otherwise -> throw $ ErrorAppArgMismatch tt k1 k2+ + _ -> throw $ ErrorAppNotFun tt t1 k1 t2 k2++-- Sums -----------------------+checkTypeM' env (TSum ts)+ = do ks <- mapM (checkTypeM env) $ TS.toList ts++ -- Check that all the types in the sum have a single kind, + -- and return that kind.+ k <- case nub ks of + [] -> return $ TS.kindOfSum ts+ [k] -> return k+ _ -> throw $ ErrorSumKindMismatch + (TS.kindOfSum ts) ts ks+ + -- Check that the kind of the elements is a valid one.+ -- Only effects and closures can be summed.+ if (k == kEffect || k == kClosure)+ then return k+ else throw $ ErrorSumKindInvalid ts k+
+ DDC/Type/Check/CheckCon.hs view
@@ -0,0 +1,73 @@+{-# OPTIONS_HADDOCK hide #-}+module DDC.Type.Check.CheckCon+ ( takeKindOfTyCon+ , takeSortOfKiCon+ , kindOfTwCon+ , kindOfTcCon)+where+import DDC.Type.Exp+import DDC.Type.Compounds+++-- | Take the kind of a `TyCon`, if there is one.+takeKindOfTyCon :: TyCon n -> Maybe (Kind n)+takeKindOfTyCon tt+ = case tt of + -- Sorts don't have a higher classification.+ TyConSort _ -> Nothing+ + TyConKind kc -> takeSortOfKiCon kc+ TyConWitness tc -> Just $ kindOfTwCon tc+ TyConSpec tc -> Just $ kindOfTcCon tc+ TyConBound u -> Just $ typeOfBound u+++-- | Take the superkind of an atomic kind constructor.+--+-- * Yields `Nothing` for the kind function (~>) as it doesn't have a sort+-- without being fully applied.+takeSortOfKiCon :: KiCon -> Maybe (Sort n)+takeSortOfKiCon kc+ = case kc of+ KiConFun -> Nothing+ KiConData -> Just sComp+ KiConRegion -> Just sComp+ KiConEffect -> Just sComp+ KiConClosure -> Just sComp+ KiConWitness -> Just sProp+++-- | Take the kind of a witness type constructor.+kindOfTwCon :: TwCon -> Kind n+kindOfTwCon tc+ = case tc of+ TwConImpl -> kWitness `kFun` (kWitness `kFun` kWitness)+ TwConPure -> kEffect `kFun` kWitness+ TwConEmpty -> kClosure `kFun` kWitness+ TwConGlobal -> kRegion `kFun` kWitness+ TwConDeepGlobal -> kData `kFun` kWitness+ TwConConst -> kRegion `kFun` kWitness+ TwConDeepConst -> kData `kFun` kWitness+ TwConMutable -> kRegion `kFun` kWitness+ TwConDeepMutable-> kData `kFun` kWitness+ TwConLazy -> kRegion `kFun` kWitness+ TwConHeadLazy -> kData `kFun` kWitness+ TwConManifest -> kRegion `kFun` kWitness+++-- | Take the kind of a computation type constructor.+kindOfTcCon :: TcCon -> Kind n+kindOfTcCon tc+ = case tc of+ TcConFun -> [kData, kEffect, kClosure, kData] `kFuns` kData+ TcConRead -> kRegion `kFun` kEffect+ TcConHeadRead -> kData `kFun` kEffect+ TcConDeepRead -> kData `kFun` kEffect+ TcConWrite -> kRegion `kFun` kEffect+ TcConDeepWrite -> kData `kFun` kEffect+ TcConAlloc -> kRegion `kFun` kEffect+ TcConDeepAlloc -> kData `kFun` kEffect+ TcConUse -> kRegion `kFun` kClosure+ TcConDeepUse -> kData `kFun` kClosure++
+ DDC/Type/Check/CheckError.hs view
@@ -0,0 +1,134 @@+{-# OPTIONS_HADDOCK hide #-}+-- | Errors produced when checking types.+module DDC.Type.Check.CheckError+ (Error(..))+where+import DDC.Type.Exp+import DDC.Type.Compounds+import DDC.Type.Pretty+++-- Error ------------------------------------------------------------------------------------------+-- | Type errors.+data Error n++ -- | An undefined type variable.+ = ErrorUndefined + { errorBound :: Bound n }++ -- | The kind annotation on the variables does not match the one in the environment.+ | ErrorVarAnnotMismatch+ { errorBound :: Bound n+ , errorTypeEnv :: Type n }++ -- | Found a naked sort constructor.+ | ErrorNakedSort+ { errorSort :: Sort n }++ -- | Found an unapplied kind function constructor.+ | ErrorUnappliedKindFun ++ -- | A type application where the parameter and argument kinds don't match.+ | ErrorAppArgMismatch + { errorChecking :: Type n+ , errorParamKind :: Kind n+ , errorArgKind :: Kind n }++ -- | A type application where the thing being applied is not a function.+ | ErrorAppNotFun+ { errorChecking :: Type n+ , errorFunType :: Type n+ , errorFunTypeKind :: Kind n+ , errorArgType :: Type n+ , errorArgTypeKind :: Kind n }++ -- | A type sum where the components have differing kinds.+ | ErrorSumKindMismatch+ { errorKindExpected :: Kind n+ , errorTypeSum :: TypeSum n+ , errorKinds :: [Kind n] }+ + -- | A type sum that does not have effect or closure kind.+ | ErrorSumKindInvalid+ { errorCheckingSum :: TypeSum n+ , errorKind :: Kind n }++ -- | A forall where the body does not have data or witness kind.+ | ErrorForallKindInvalid+ { errorChecking :: Type n+ , errorBody :: Type n+ , errorKind :: Kind n }++ -- | A witness implication where the premise or conclusion has an invalid kind.+ | ErrorWitnessImplInvalid+ { errorChecking :: Type n+ , errorLeftType :: Type n+ , errorLeftKind :: Kind n+ , errorRightType :: Type n+ , errorRightKind :: Kind n }+ deriving Show+++instance (Eq n, Pretty n) => Pretty (Error n) where+ ppr err+ = case err of+ ErrorUnappliedKindFun + -> text "Can't take sort of unapplied kind function constructor."+ + ErrorNakedSort s+ -> text "Can't check a naked sort: " <> ppr s++ ErrorUndefined u+ -> text "Undefined type variable: " <> ppr u+ + ErrorVarAnnotMismatch u t+ -> vcat [ text "Type mismatch in annotation."+ , text " Variable: " <> ppr u+ , text " has annotation: " <> (ppr $ typeOfBound u)+ , text " which conflicts with: " <> ppr t+ , text " from environment." ]+ + ErrorAppArgMismatch tt t1 t2+ -> vcat [ text "Core type mismatch in application."+ , text " type: " <> ppr t1+ , text " does not match: " <> ppr t2+ , text " in application: " <> ppr tt ]+ + ErrorAppNotFun tt t1 k1 t2 k2+ -> vcat [ text "Core type mismatch in application."+ , text " cannot apply type: " <> ppr t2+ , text " of kind: " <> ppr k2+ , text " to non-function type: " <> ppr t1+ , text " of kind: " <> ppr k1+ , text " in appliction: " <> ppr tt]+ + ErrorSumKindMismatch k ts ks+ -> vcat + $ [ text "Core type mismatch in sum."+ , text " found multiple types: " <> ppr ts+ , text " with differing kinds: " <> ppr ks ]+ ++ (if k /= tBot sComp+ then [text " expected kind: " <> ppr k ]+ else [])+ + ErrorSumKindInvalid ts k+ -> vcat [ text "Invalid kind for type sum."+ , text " the type sum: " <> ppr ts+ , text " has kind: " <> ppr k+ , text " but it must be ! or $" ]++ ErrorForallKindInvalid tt t k+ -> vcat [ text "Invalid kind for body of quantified type."+ , text " the body type: " <> ppr t+ , text " has kind: " <> ppr k+ , text " but it must be * or @" + , text " when checking: " <> ppr tt ]+ + ErrorWitnessImplInvalid tt t1 k1 t2 k2+ -> vcat [ text "Invalid args for witness implication."+ , text " left type: " <> ppr t1+ , text " has kind: " <> ppr k1+ , text " right type: " <> ppr t2+ , text " has kind: " <> ppr k2 + , text " when checking: " <> ppr tt ]+
+ DDC/Type/Check/Monad.hs view
@@ -0,0 +1,28 @@++module DDC.Type.Check.Monad+ ( CheckM (..)+ , throw+ , result)+where++-- | Type checking monad.+data CheckM err a+ = CheckM (Either err a)++instance Monad (CheckM err) where+ return x = CheckM (Right x)+ (>>=) m f + = case m of+ CheckM (Left err) -> CheckM (Left err)+ CheckM (Right x) -> f x++ +-- | Throw a type error in the monad.+throw :: err -> CheckM err a+throw e = CheckM $ Left e+++-- | Take the result from a check monad.+result :: CheckM err a -> Either err a+result (CheckM r) = r+
+ DDC/Type/Compounds.hs view
@@ -0,0 +1,425 @@+{-# OPTIONS -fno-warn-missing-signatures #-}+module DDC.Type.Compounds+ ( -- * Binds+ takeNameOfBind+ , typeOfBind+ , replaceTypeOfBind+ + -- * Binders+ , binderOfBind+ , makeBindFromBinder+ , partitionBindsByType+ + -- * Bounds+ , typeOfBound+ , takeNameOfBound+ , replaceTypeOfBound+ , boundMatchesBind+ , namedBoundMatchesBind+ , takeSubstBoundOfBind++ -- * Type structure+ , tIx+ , tApp, ($:)+ , tApps, takeTApps+ , takeTyConApps, takeDataTyConApps+ , tForall+ , tForalls, takeTForalls+ , tBot+ , tSum++ -- * Function type construction+ , kFun+ , kFuns, takeKFun+ , takeKFuns, takeKFuns', takeResultKind+ , tFun, takeTFun, takeTFunArgResult+ , tFunPE+ , tImpl++ -- * Sort construction+ , sComp, sProp++ -- * Kind construction+ , kData, kRegion, kEffect, kClosure, kWitness++ -- * Effect type constructors+ , tRead, tDeepRead, tHeadRead+ , tWrite, tDeepWrite+ , tAlloc, tDeepAlloc++ -- * Closure type constructors.+ , tUse, tDeepUse++ -- * Witness type constructors.+ , tPure+ , tEmpty+ , tGlobal, tDeepGlobal+ , tConst, tDeepConst+ , tMutable, tDeepMutable+ , tLazy, tHeadLazy+ , tManifest+ , tConData0, tConData1)+where+import DDC.Type.Exp+import qualified DDC.Type.Sum as Sum+++-- Binds ----------------------------------------------------------------------+-- | Take the variable name of a bind.+-- If this is an anonymous binder then there won't be a name.+takeNameOfBind :: Bind n -> Maybe n+takeNameOfBind bb+ = case bb of+ BName n _ -> Just n+ BAnon _ -> Nothing+ BNone _ -> Nothing+++-- | Take the type of a bind.+typeOfBind :: Bind n -> Type n+typeOfBind bb+ = case bb of+ BName _ t -> t+ BAnon t -> t+ BNone t -> t+++-- | Replace the type of a bind with a new one.+replaceTypeOfBind :: Type n -> Bind n -> Bind n+replaceTypeOfBind t bb+ = case bb of+ BName n _ -> BName n t+ BAnon _ -> BAnon t+ BNone _ -> BNone t+++-- Binders --------------------------------------------------------------------+-- | Take the binder of a bind.+binderOfBind :: Bind n -> Binder n+binderOfBind bb+ = case bb of+ BName n _ -> RName n+ BAnon _ -> RAnon+ BNone _ -> RNone+++-- | Make a bind from a binder and its type.+makeBindFromBinder :: Binder n -> Type n -> Bind n+makeBindFromBinder bb t+ = case bb of+ RName n -> BName n t+ RAnon -> BAnon t+ RNone -> BNone t+++-- | Make lists of binds that have the same type.+partitionBindsByType :: Eq n => [Bind n] -> [([Binder n], Type n)]+partitionBindsByType [] = []+partitionBindsByType (b:bs)+ = let t = typeOfBind b+ bsSame = takeWhile (\b' -> typeOfBind b' == t) bs+ rs = map binderOfBind (b:bsSame)+ in (rs, t) : partitionBindsByType (drop (length bsSame) bs)+++-- Bounds ---------------------------------------------------------------------+-- | Take the type of a bound variable.+typeOfBound :: Bound n -> Type n+typeOfBound uu+ = case uu of+ UName _ t -> t+ UPrim _ t -> t+ UIx _ t -> t+++-- | Take the name of bound variable.+-- If this is a deBruijn index then there won't be a name.+takeNameOfBound :: Bound n -> Maybe n+takeNameOfBound uu+ = case uu of+ UName n _ -> Just n+ UPrim n _ -> Just n+ UIx _ _ -> Nothing+++-- | Replace the type of a bound with a new one.+replaceTypeOfBound :: Type n -> Bound n -> Bound n+replaceTypeOfBound t uu+ = case uu of+ UName n _ -> UName n t+ UPrim n _ -> UPrim n t+ UIx i _ -> UIx i t+++-- | Check whether a bound maches a bind.+-- `UName` and `BName` match if they have the same name.+-- @UIx 0 _@ and @BAnon _@ always match.+-- Yields `False` for other combinations of bounds and binds.+boundMatchesBind :: Eq n => Bound n -> Bind n -> Bool+boundMatchesBind u b+ = case (u, b) of+ (UName n1 _, BName n2 _) -> n1 == n2+ (UIx 0 _, BAnon _ ) -> True+ _ -> False+++-- | Check whether a named bound matches a named bind. +-- Yields `False` if they are not named or have different names.+namedBoundMatchesBind :: Eq n => Bound n -> Bind n -> Bool+namedBoundMatchesBind u b+ = case (u, b) of+ (UName n1 _, BName n2 _) -> n1 == n2+ _ -> False++++-- | Convert a `Bound` to a `Bind`, ready for substitution.+-- +-- Returns `UName` for `BName`, @UIx 0@ for `BAnon` +-- and `Nothing` for `BNone`, because there's nothing to substitute.+takeSubstBoundOfBind :: Bind n -> Maybe (Bound n)+takeSubstBoundOfBind bb+ = case bb of+ BName n t -> Just $ UName n t+ BAnon t -> Just $ UIx 0 t+ BNone _ -> Nothing+++-- Variables ------------------------------------------------------------------+-- | Construct a deBruijn index.+tIx :: Kind n -> Int -> Type n+tIx k i = TVar (UIx i k)+++-- Applications ---------------------------------------------------------------+-- | Construct an empty type sum.+tBot :: Kind n -> Type n+tBot k = TSum $ Sum.empty k+++-- | Construct a type application.+tApp, ($:) :: Type n -> Type n -> Type n+tApp = TApp+($:) = TApp++-- | Construct a sequence of type applications.+tApps :: Type n -> [Type n] -> Type n+tApps t1 ts = foldl TApp t1 ts+++-- | Flatten a sequence ot type applications into the function part and+-- arguments, if any.+takeTApps :: Type n -> [Type n]+takeTApps tt+ = case tt of+ TApp t1 t2 -> takeTApps t1 ++ [t2]+ _ -> [tt]+++-- | Flatten a sequence of type applications, returning the type constructor+-- and arguments, if there is one.+takeTyConApps :: Type n -> Maybe (TyCon n, [Type n])+takeTyConApps tt+ = case takeTApps tt of+ TCon tc : args -> Just $ (tc, args)+ _ -> Nothing+++-- | Flatten a sequence of type applications, returning the type constructor+-- and arguments, if there is one. Only accept data type constructors.+takeDataTyConApps :: Type n -> Maybe (TyCon n, [Type n])+takeDataTyConApps tt+ = case takeTApps tt of+ TCon tc : args + | TyConBound (UName _ t) <- tc+ , TCon (TyConKind KiConData) <- takeResultKind t+ -> Just (tc, args)++ | TyConBound (UPrim _ t) <- tc+ , TCon (TyConKind KiConData) <- takeResultKind t+ -> Just (tc, args)++ _ -> Nothing+++-- Foralls --------------------------------------------------------------------+-- | Build an anonymous type abstraction, with a single parameter.+tForall :: Kind n -> (Type n -> Type n) -> Type n+tForall k f+ = TForall (BAnon k) (f (TVar (UIx 0 k)))+++-- | Build an anonymous type abstraction, with several parameters.+tForalls :: [Kind n] -> ([Type n] -> Type n) -> Type n+tForalls ks f+ = let bs = [BAnon k | k <- ks]+ us = reverse [TVar (UIx n k) | k <- ks | n <- [0..]]+ in foldr TForall (f 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)+takeTForalls tt+ = let go bs (TForall b t) = go (b:bs) t+ go bs t = (reverse bs, t)+ in case go [] tt of+ ([], _) -> Nothing+ (bs, body) -> Just (bs, body)+++-- Sums -----------------------------------------------------------------------+tSum :: Ord n => Kind n -> [Type n] -> Type n+tSum k ts+ = TSum (Sum.fromList k ts)+++-- Function Constructors ------------------------------------------------------+-- | Construct a kind function.+kFun :: Kind n -> Kind n -> Kind n+kFun k1 k2 = ((TCon $ TyConKind KiConFun)`TApp` k1) `TApp` k2++infixr `kFun`+++-- | Construct some kind functions.+kFuns :: [Kind n] -> Kind n -> Kind n+kFuns [] k1 = k1+kFuns (k:ks) k1 = k `kFun` kFuns ks k1+++-- | Destruct a kind function+takeKFun :: Kind n -> Maybe (Kind n, Kind n)+takeKFun kk+ = case kk of+ TApp (TApp (TCon (TyConKind KiConFun)) k1) k2 + -> Just (k1, k2)+ _ -> Nothing+++-- | Destruct a chain of kind functions into the arguments+takeKFuns :: Kind n -> ([Kind n], Kind n)+takeKFuns kk+ = case kk of+ TApp (TApp (TCon (TyConKind KiConFun)) k1) k2+ | (ks, k2') <- takeKFuns k2+ -> (k1 : ks, k2')++ _ -> ([], kk)+++-- | Like `takeKFuns`, but return argument and return kinds in the same list.+takeKFuns' :: Kind n -> [Kind n]+takeKFuns' kk + | (ks, k1) <- takeKFuns kk+ = ks ++ [k1]+++-- | Take the result kind of a kind function, or return the same kind+-- unharmed if it's not a kind function.+takeResultKind :: Kind n -> Kind n+takeResultKind kk+ = case kk of+ TApp (TApp (TCon (TyConKind KiConFun)) _) k2+ -> takeResultKind k2+ _ -> kk+++-- | 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`+++-- | Destruct the type of a value function.+takeTFun :: Type n -> Maybe (Type n, Effect n, Closure n, Type n)+takeTFun tt+ = case tt of+ TApp (TApp (TApp (TApp (TCon (TyConSpec TcConFun)) t1) eff) clo) t2+ -> Just (t1, eff, clo, t2)+ _ -> Nothing+++-- | Destruct the type of a value function, returning just the argument+-- and result types.+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)++ _ -> ([], tt)+++-- | 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+++-- | Construct a witness implication type.+tImpl :: Type n -> Type n -> Type n+tImpl t1 t2 + = ((TCon $ TyConWitness TwConImpl) `tApp` t1) `tApp` t2++infixr `tImpl`+++-- Level 3 constructors (sorts) -----------------------------------------------+sComp = TCon $ TyConSort SoConComp+sProp = TCon $ TyConSort SoConProp+++-- Level 2 constructors (kinds) -----------------------------------------------+kData = TCon $ TyConKind KiConData+kRegion = TCon $ TyConKind KiConRegion+kEffect = TCon $ TyConKind KiConEffect+kClosure = TCon $ TyConKind KiConClosure+kWitness = TCon $ TyConKind KiConWitness+++-- Level 1 constructors (witness and computation types) -----------------------++-- Effect type constructors+tRead = tcCon1 TcConRead+tHeadRead = tcCon1 TcConHeadRead+tDeepRead = tcCon1 TcConDeepRead+tWrite = tcCon1 TcConWrite+tDeepWrite = tcCon1 TcConDeepWrite+tAlloc = tcCon1 TcConAlloc+tDeepAlloc = tcCon1 TcConDeepAlloc++-- Closure type constructors.+tUse = tcCon1 TcConUse+tDeepUse = tcCon1 TcConDeepUse++-- Witness type constructors.+tPure = twCon1 TwConPure+tEmpty = twCon1 TwConEmpty+tGlobal = twCon1 TwConGlobal+tDeepGlobal = twCon1 TwConDeepGlobal+tConst = twCon1 TwConConst+tDeepConst = twCon1 TwConDeepConst+tMutable = twCon1 TwConMutable+tDeepMutable = twCon1 TwConDeepMutable+tLazy = twCon1 TwConLazy+tHeadLazy = twCon1 TwConHeadLazy+tManifest = twCon1 TwConManifest++tcCon1 tc t = (TCon $ TyConSpec tc) `tApp` t+twCon1 tc t = (TCon $ TyConWitness tc) `tApp` t+++-- | Build a nullary type constructor of the given kind.+tConData0 :: n -> Kind n -> Type n+tConData0 n k = TCon (TyConBound (UName n k))+++-- | 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++
+ DDC/Type/Env.hs view
@@ -0,0 +1,153 @@++-- | Type environments.+--+-- An environment contains the types +-- named bound variables,+-- named primitives, +-- and a deBruijn stack for anonymous variables.+--+module DDC.Type.Env+ ( Env(..)+ , empty+ , extend, extends+ , setPrimFun, isPrim+ , fromList+ , union+ , member, memberBind+ , lookup, lookupName+ , depth+ , wrapTForalls)+where+import DDC.Type.Exp+import Data.Maybe+import Data.Map (Map)+import Prelude hiding (lookup)+import qualified Data.Map as Map+import qualified Prelude as P+import Control.Monad+++-- | A type environment.+data Env n+ = Env+ { -- | Types of named binders.+ envMap :: Map n (Type n)++ -- | Types of anonymous deBruijn binders.+ , envStack :: [Type n] + + -- | The length of the above stack.+ , envStackLength :: Int++ -- | Types of baked in, primitive names.+ , envPrimFun :: n -> Maybe (Type n) }+++-- | An empty environment.+empty :: Env n+empty = Env+ { envMap = Map.empty+ , envStack = [] + , envStackLength = 0+ , envPrimFun = \_ -> Nothing }+++-- | Extend an environment with a new binding.+-- Replaces bindings with the same name already in the environment.+extend :: Ord n => Bind n -> Env n -> Env n+extend bb env+ = case bb of+ BName n k -> env { envMap = Map.insert n k (envMap env) }+ BAnon k -> env { envStack = k : envStack env + , envStackLength = envStackLength env + 1 }+ BNone{} -> env+++-- | Extend an environment with a list of new bindings.+-- Replaces bindings with the same name already in the environment.+extends :: Ord n => [Bind n] -> Env n -> Env n+extends bs env+ = foldl (flip extend) env bs+++-- | Set the function that knows the types of primitive things.+setPrimFun :: (n -> Maybe (Type n)) -> Env n -> Env n+setPrimFun f env+ = env { envPrimFun = f }+++-- | Check if the type of a name is defined by the `envPrimFun`.+isPrim :: Env n -> n -> Bool+isPrim env n+ = isJust $ envPrimFun env n+++-- | Convert a list of `Bind`s to an environment.+fromList :: Ord n => [Bind n] -> Env n+fromList bs+ = foldr extend empty bs+++-- | Combine two environments.+-- If both environments have a binding with the same name,+-- then the one in the second environment takes preference.+union :: Ord n => Env n -> Env n -> Env n+union env1 env2+ = Env + { envMap = envMap env1 `Map.union` envMap env2+ , envStack = envStack env2 ++ envStack env1+ , envStackLength = envStackLength env2 + envStackLength env1+ , envPrimFun = \n -> envPrimFun env2 n `mplus` envPrimFun env1 n }+++-- | Check whether a bound variable is present in an environment.+member :: Ord n => Bound n -> Env n -> Bool+member uu env+ = isJust $ lookup uu env+++-- | Check whether a binder is already present in the an environment.+-- This can only return True for named binders, not anonymous or primitive ones.+memberBind :: Ord n => Bind n -> Env n -> Bool+memberBind uu env+ = case uu of+ BName n _ -> Map.member n (envMap env)+ _ -> False+++-- | Lookup a bound variable from an environment.+lookup :: Ord n => Bound n -> Env n -> Maybe (Type n)+lookup uu env+ = case uu of+ UName n _+ -> Map.lookup n (envMap env) + `mplus` envPrimFun env n++ UIx i _ + -> P.lookup i (zip [0..] (envStack env))++ UPrim n _+ -> envPrimFun env n+++-- | Lookup a bound name from an environment.+lookupName :: Ord n => n -> Env n -> Maybe (Type n)+lookupName n env+ = Map.lookup n (envMap env)+++-- | Yield the total depth of the deBruijn stack.+depth :: Env n -> Int+depth env = envStackLength env+++-- | Wrap locally bound (non primitive) variables defined in an environment+-- around a type as new foralls.+wrapTForalls :: Ord n => Env n -> Type n -> Type n+wrapTForalls env tBody+ = let bsNamed = [BName b t | (b, t) <- Map.toList $ envMap env ]+ bsAnon = [BAnon t | t <- envStack env]+ + tInner = foldr TForall tBody (reverse bsAnon)+ in foldr TForall tInner bsNamed+
+ DDC/Type/Equiv.hs view
@@ -0,0 +1,149 @@++module DDC.Type.Equiv+ (equivT)+where+import DDC.Type.Exp+import DDC.Type.Compounds+import DDC.Type.Transform.Crush+import DDC.Type.Transform.Trim+import DDC.Base.Pretty+import Data.Maybe+import qualified DDC.Type.Sum as Sum+++-- | Check equivalence of types.+--+-- Checks equivalence up to alpha-renaming, as well as crushing of effects+-- and trimming of closures.+-- +-- * Return `False` if we find any free variables.+--+-- * We assume the types are well-kinded, so that the type annotations on+-- bound variables match the binders. If this is not the case then you get+-- an indeterminate result.+--+equivT :: (Ord n, Pretty n) => Type n -> Type n -> Bool+equivT t1 t2+ = equivT' [] 0 [] 0 t1 t2+++equivT' :: (Ord n, Pretty n)+ => [Bind n] -> Int+ -> [Bind n] -> Int+ -> Type n -> Type n+ -> Bool++equivT' stack1 depth1 stack2 depth2 t1 t2+ = let t1' = unpackSumT $ crushSomeT t1+ t2' = unpackSumT $ crushSomeT t2+ in case (t1', t2') of+ (TVar u1, TVar u2)+ -- Bound variables are name-equivalent.+ | u1 == u2 -> True++ -- Variables aren't name equivalent, + -- but would be equivalent if we renamed them.+ | depth1 == depth2+ , Just (ix1, t1a) <- getBindType stack1 u1+ , Just (ix2, t2a) <- getBindType stack2 u2+ , ix1 == ix2+ -> equivT' stack1 depth1 stack2 depth2 t1a t2a++ -- Constructor names must be equal.+ (TCon tc1, TCon tc2)+ -> tc1 == tc2++ -- Push binders on the stack as we enter foralls.+ (TForall b11 t12, TForall b21 t22)+ | equivT (typeOfBind b11) (typeOfBind b21)+ -> equivT' (b11 : stack1) (depth1 + 1) + (b21 : stack2) (depth2 + 1) + t12 t22++ -- Decend into applications.+ (TApp t11 t12, TApp t21 t22)+ -> equivT' stack1 depth1 stack2 depth2 t11 t21+ && equivT' stack1 depth1 stack2 depth2 t12 t22+ + -- Sums are equivalent if all of their components are.+ (TSum ts1, TSum ts2)+ -> let ts1' = Sum.toList ts1+ ts2' = Sum.toList ts2+ equiv = equivT' stack1 depth1 stack2 depth2++ -- If all the components of the sum were in the element+ -- arrays then they come out of Sum.toList sorted+ -- and we can compare corresponding pairs.+ checkFast = and $ zipWith equiv ts1' ts2'++ -- If any of the components use a higher kinded type variable+ -- like (c : % ~> !) then they won't nessesarally be sorted,+ -- so we need to do this slower O(n^2) check.+ checkSlow = and [ or (map (equiv t1c) ts2') | t1c <- ts1' ]+ && and [ or (map (equiv t2c) ts1') | t2c <- ts2' ]++ in (length ts1' == length ts2')+ && (checkFast || checkSlow)++ (_, _) -> False+++-- | Unpack single element sums into plain types.+unpackSumT :: Type n -> Type n+unpackSumT (TSum ts)+ | [t] <- Sum.toList ts = t+unpackSumT tt = tt+++-- | Crush compound effects and closure terms.+-- We check for a crushable term before calling crushT because that function+-- will recursively crush the components. +-- As equivT is already recursive, we don't want a doubly-recursive function+-- that tries to re-crush the same non-crushable type over and over.+--+crushSomeT :: (Ord n, Pretty n) => Type n -> Type n+crushSomeT tt+ = case tt of+ (TApp (TCon tc) _)+ -> case tc of+ TyConSpec TcConDeepRead -> crushEffect tt+ TyConSpec TcConDeepWrite -> crushEffect tt+ TyConSpec TcConDeepAlloc -> crushEffect tt++ -- If a closure is miskinded then 'trimClosure' + -- can return Nothing, so we just leave the term untrimmed.+ TyConSpec TcConDeepUse -> fromMaybe tt (trimClosure tt)++ TyConWitness TwConDeepGlobal -> crushEffect tt+ _ -> tt++ _ -> tt+++-- | Lookup the type of a bound thing from the binder stack.+-- The binder stack contains the binders of all the `TForall`s we've+-- entered under so far.+getBindType :: Eq n => [Bind n] -> Bound n -> Maybe (Int, Type n)+getBindType bs' u+ = go 0 bs'+ where go n (BName n1 t : bs)+ | UName n2 _ <- u+ , n1 == n2 = Just (n, t)+ | otherwise = go (n + 1) bs+++ go n (BAnon t : bs)+ | UIx i _ <- u+ , i == 0 = Just (n, t)++ | UIx i _ <- u+ , i < 0 = Nothing++ | otherwise = go (n + 1) bs+++ go n (BNone _ : bs)+ = go (n + 1) bs++ go _ [] = Nothing+
+ DDC/Type/Exp.hs view
@@ -0,0 +1,271 @@++module DDC.Type.Exp+ ( -- * Types, Kinds, and Sorts+ Binder (..)+ , Bind (..)+ , Bound (..)+ , Type (..)+ , Kind, Sort+ , Region, Effect, Closure+ , TypeSum (..), TyConHash(..), TypeSumVarCon(..)+ , TyCon (..)+ , SoCon (..)+ , KiCon (..)+ , TwCon (..)+ , TcCon (..))+where+import Data.Array+import Data.Map (Map)+import Data.Set (Set)+++-- Bind -----------------------------------------------------------------------+-- | A variable binder.+data Binder n+ = RNone+ | RAnon+ | RName n+ deriving Show+++-- | A variable binder with its type.+data Bind n+ -- | A variable with no uses in the body doesn't need a name.+ = BNone (Type n)++ -- | Nameless variable on the deBruijn stack.+ | BAnon (Type n)++ -- | Named variable in the environment.+ | BName n (Type n)+ deriving Show++++-- | A bound occurrence of a variable, with its type.+--+-- If variable hasn't been annotated with its real type then this +-- can be `tBot` (an empty sum).++data Bound n+ -- | Nameless variable that should be on the deBruijn stack.+ = UIx Int (Type n) ++ -- | Named variable that should be in the environment.+ | UName n (Type n)++ -- | Named primitive that is not bound in the environment.+ -- Prims aren't every counted as being free.+ | UPrim n (Type n) + deriving Show+++-- Types ----------------------------------------------------------------------+-- | A value type, kind, or sort.+--+-- We use the same data type to represent all three universes, as they have+-- a similar algebraic structure.+--+data Type n+ -- | Variable.+ = TVar (Bound n)++ -- | Constructor.+ | TCon (TyCon n)++ -- | Abstraction.+ | TForall (Bind n) (Type n)+ + -- | Application.+ | TApp (Type n) (Type n)++ -- | Least upper bound.+ | TSum (TypeSum n)+ deriving Show+++type Sort n = Type n+type Kind n = Type n+type Region n = Type n+type Effect n = Type n+type Closure n = Type n+++-- Type Sums ------------------------------------------------------------------+-- | A least upper bound of several types.+-- +-- We keep type sums in this normalised format instead of joining them+-- together with a binary operator (like @(+)@). This makes sums easier to work+-- with, as a given sum type often only has a single physical representation.+data TypeSum n+ = TypeSum+ { -- | The kind of the elements in this sum.+ typeSumKind :: Kind n++ -- | Where we can see the outer constructor of a type, its argument+ -- is inserted into this array. This handles common cases like+ -- Read, Write, Alloc effects.+ , typeSumElems :: Array TyConHash (Set (TypeSumVarCon n))++ -- | A map for named type variables.+ , typeSumBoundNamed :: Map n (Kind n)++ -- | A map for anonymous type variables.+ , typeSumBoundAnon :: Map Int (Kind n)++ -- | Types that can't be placed in the other fields go here.+ -- + -- INVARIANT: this list doesn't contain more `TSum`s.+ , typeSumSpill :: [Type n] }+ deriving (Show)+ ++-- | Hash value used to insert types into the `typeSumElems` array of a `TypeSum`.+data TyConHash + = TyConHash !Int+ deriving (Eq, Show, Ord, Ix)+++-- | Wraps a variable or constructor that can be added the `typeSumElems` array.+data TypeSumVarCon n+ = TypeSumVar (Bound n)+ | TypeSumCon (Bound n)+ deriving Show+++-- TyCon ----------------------------------------------------------------------+-- | Kind, type and witness constructors.+--+-- These are grouped to make it easy to determine the universe that they+-- belong to.+-- +data TyCon n+ -- | (level 3) Builtin Sort constructors.+ = TyConSort SoCon++ -- | (level 2) Builtin Kind constructors.+ | TyConKind KiCon++ -- | (level 1) Builtin Spec constructors for the types of witnesses.+ | TyConWitness TwCon++ -- | (level 1) Builtin Spec constructors for types of other kinds.+ | TyConSpec TcCon++ -- | User defined and primitive constructors.+ | TyConBound (Bound n)+ deriving Show+++-- | Sort constructor.+data SoCon+ -- | Sort of witness kinds.+ = SoConProp -- '@@'++ -- | Sort of computation kinds.+ | SoConComp -- '**'+ deriving (Eq, Show)+++-- | Kind constructor.+data KiCon+ -- | Function kind constructor.+ -- This is only well formed when it is fully applied.+ = KiConFun -- (~>)++ -- Witness kinds ------------------------+ -- | Kind of witnesses.+ | KiConWitness -- '@ :: @@'++ -- Computation kinds ---------------------+ -- | Kind of data values.+ | KiConData -- '* :: **'++ -- | Kind of regions.+ | KiConRegion -- '% :: **'++ -- | Kind of effects.+ | KiConEffect -- '! :: **'++ -- | Kind of closures.+ | KiConClosure -- '$ :: **'+ deriving (Eq, Show)+++-- | Witness type constructors.+data TwCon+ -- Witness implication.+ = TwConImpl -- :: '(=>) :: * ~> *'++ -- | Purity of some effect.+ | TwConPure -- :: ! ~> @++ -- | Emptiness of some closure.+ | TwConEmpty -- :: $ ~> @++ -- | Globalness of some region.+ | TwConGlobal -- :: % ~> @++ -- | Globalness of material regions in some type.+ | TwConDeepGlobal -- :: * ~> @+ + -- | Constancy of some region.+ | TwConConst -- :: % ~> @++ -- | Constancy of material regions in some type+ | TwConDeepConst -- :: * ~> @++ -- | Mutability of some region.+ | TwConMutable -- :: % ~> @++ -- | Mutability of material regions in some type.+ | TwConDeepMutable -- :: * ~> @++ -- | Laziness of some region.+ | TwConLazy -- :: % ~> @++ -- | Laziness of the primary region in some type.+ | TwConHeadLazy -- :: * ~> @++ -- | Manifestness of some region (not lazy).+ | TwConManifest -- :: % ~> @+ deriving (Eq, Show)+++-- | Other constructors at the spec level.+data TcCon+ -- Data type constructors ---------------+ -- | The function type constructor is baked in so we + -- represent it separately.+ = TcConFun -- '(->) :: * ~> * ~> ! ~> $ ~> *'++ -- Effect type constructors -------------+ -- | Read of some region.+ | TcConRead -- :: '% ~> !'++ -- | Read the head region in a data type.+ | TcConHeadRead -- :: '* ~> !'++ -- | Read of all material regions in a data type.+ | TcConDeepRead -- :: '* ~> !'+ + -- | Write of some region.+ | TcConWrite -- :: '% ~> !'++ -- | Write to all material regions in some data type.+ | TcConDeepWrite -- :: '* ~> !'+ + -- | Allocation into some region.+ | TcConAlloc -- :: '% ~> !'++ -- | Allocation into all material regions in some data type.+ | TcConDeepAlloc -- :: '* ~> !'+ + -- Closure type constructors ------------+ -- | Region is captured in a closure.+ | TcConUse -- :: '% ~> $'+ + -- | All material regions in a data type are captured in a closure.+ | TcConDeepUse -- :: '* ~> $'+ deriving (Eq, Show)+
+ DDC/Type/Parser.hs view
@@ -0,0 +1,236 @@++-- | Parser for type expressions.+module DDC.Type.Parser+ ( module DDC.Base.Parser+ , Parser+ , pType, pTypeAtom, pTypeApp+ , pBinder+ , pIndex+ , pTok, pTokAs)+where+import DDC.Core.Parser.Tokens +import DDC.Type.Exp+import DDC.Type.Compounds+import DDC.Base.Parser ((<?>))+import qualified DDC.Base.Parser as P+import qualified DDC.Type.Sum as TS+++-- | Parser of type tokens.+type Parser n a+ = P.Parser (Tok n) a+++-- | Top level parser for types.+pType :: Ord n => Parser n (Type n)+pType = pTypeSum+ <?> "a type"+++-- | Parse a type sum.+pTypeSum :: Ord n => Parser n (Type n)+pTypeSum + = do t1 <- pTypeForall+ P.choice + [ -- Type sums.+ -- T2 + T3+ do pTok KPlus+ t2 <- pTypeSum+ return $ TSum $ TS.fromList (tBot sComp) [t1, t2]+ + , do return t1 ]+ <?> "a type"+++-- | Parse a binder.+pBinder :: Ord n => Parser n (Binder n)+pBinder+ = P.choice+ -- Named binders.+ [ do v <- pVar+ return $ RName v+ + -- Anonymous binders.+ , do pTok KHat+ return $ RAnon + + -- Vacant binders.+ , do pTok KUnderscore+ return $ RNone ]+ <?> "a binder"+++-- | Parse a quantified type.+pTypeForall :: Ord n => Parser n (Type n)+pTypeForall+ = P.choice+ [ -- Universal quantification.+ -- [v1 v1 ... vn : T1]. T2+ do pTok KSquareBra+ bs <- P.many1 pBinder+ pTok KColon+ k <- pTypeSum+ pTok KSquareKet+ pTok KDot++ body <- pTypeForall++ return $ foldr TForall body + $ map (\b -> makeBindFromBinder b k) bs++ -- Body type+ , do pTypeFun]+ <?> "a type"+++-- | Parse a function type.+pTypeFun :: Ord n => Parser n (Type n)+pTypeFun+ = do t1 <- pTypeApp+ P.choice + [ -- T1 ~> T2+ do pTok KArrowTilde+ t2 <- pTypeFun+ return $ TApp (TApp (TCon (TyConKind KiConFun)) t1) t2++ -- T1 => T2+ , do pTok KArrowEquals+ t2 <- pTypeFun+ return $ TApp (TApp (TCon (TyConWitness TwConImpl)) t1) t2++ -- T1 -> T2+ , do pTok KArrowDash+ t2 <- pTypeFun+ return $ t1 `tFunPE` t2++ -- T1 -(TSUM | TSUM)> t2+ , do pTok KDash+ pTok KRoundBra+ eff <- pTypeSum+ pTok KBar+ clo <- pTypeSum+ pTok KRoundKet+ pTok KAngleKet+ t2 <- pTypeFun+ return $ tFun t1 eff clo t2+++ -- Body type+ , do return t1 ]+ <?> "an atomic type or type application"+++-- | Parse a type application.+pTypeApp :: Ord n => Parser n (Type n)+pTypeApp + = do (t:ts) <- P.many1 pTypeAtom+ 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 + = P.choice+ -- (~>) and (=>) and (->) and (TYPE2)+ [ do pTok KRoundBra+ P.choice+ [ do pTok KArrowTilde+ pTok KRoundKet+ return (TCon $ TyConKind KiConFun)++ , do pTok KArrowEquals+ pTok KRoundKet+ return (TCon $ TyConWitness TwConImpl)++ , do pTok KArrowDash+ pTok KRoundKet+ return (TCon $ TyConSpec TcConFun)++ , do t <- pTypeSum+ pTok KRoundKet+ return t + ]++ -- Named type constructors+ , do tc <- pTcCon+ return $ TCon (TyConSpec tc)++ , do tc <- pTwCon+ return $ TCon (TyConWitness tc)++ , 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)+ , do pTokAs KBotClosure (tBot kClosure)+ + -- Bound occurrence of a variable.+ -- We don't know the kind of this variable yet, so fill in the+ -- field with the bottom element of computation kinds. This isn't+ -- really part of the language, but makes sense implentation-wise.+ , do v <- pVar+ return $ TVar (UName v (tBot sComp))++ , do i <- pIndex+ return $ TVar (UIx (fromIntegral i) (tBot sComp))+ ]+ <?> "an atomic type"+++-------------------------------------------------------------------------------+-- | Parse a builtin `TcCon`+pTcCon :: Parser n TcCon+pTcCon = P.pTokMaybe f+ <?> "a type constructor"+ where f (KA (KTcConBuiltin c)) = Just c+ f _ = Nothing ++-- | Parse a builtin `TwCon`+pTwCon :: Parser n TwCon+pTwCon = P.pTokMaybe f+ <?> "a witness constructor"+ where f (KA (KTwConBuiltin c)) = Just c+ f _ = Nothing++-- | Parse a user `TcCon`+pTyConNamed :: Parser n (TyCon n)+pTyConNamed + = P.pTokMaybe f+ <?> "a type constructor"+ where f (KN (KCon n)) = Just (TyConBound (UName n (tBot kData)))+ f _ = Nothing++-- | Parse a variable.+pVar :: Parser n n+pVar = P.pTokMaybe f+ <?> "a variable"+ where f (KN (KVar n)) = Just n+ f _ = Nothing++-- | Parse a deBruijn index+pIndex :: Parser n Int+pIndex = P.pTokMaybe 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 and return some value.+pTokAs :: TokAtom -> a -> Parser n a+pTokAs k x = P.pTokAs (KA k) x+
+ DDC/Type/Predicates.hs view
@@ -0,0 +1,98 @@++-- | Predicates on type expressions.+module DDC.Type.Predicates+ ( isBot+ , isAtomT+ , isDataKind+ , isRegionKind+ , isEffectKind+ , isClosureKind+ , isWitnessKind+ , isAlgDataType)+where+import DDC.Type.Exp+import DDC.Type.Compounds+import qualified DDC.Type.Sum as T+++-- Atoms ----------------------------------------------------------------------+-- | Test if some type is an empty TSum+isBot :: Type n -> Bool+isBot tt+ | TSum ss <- tt+ , [] <- T.toList ss+ = True+ + | otherwise = False+++-- | Check whether a type is a `TVar`, `TCon` or is Bottom.+isAtomT :: Type n -> Bool+isAtomT tt+ = case tt of+ TVar{} -> True+ TCon{} -> True+ _ -> isBot tt+++-- Kinds ----------------------------------------------------------------------+-- | Check if some kind is the data kind.+isDataKind :: Kind n -> Bool+isDataKind tt+ = case tt of+ TCon (TyConKind KiConData) -> True+ _ -> False+++-- | Check if some kind is the region kind.+isRegionKind :: Region n -> Bool+isRegionKind tt+ = case tt of+ TCon (TyConKind KiConRegion) -> True+ _ -> False+++-- | Check if some kind is the effect kind.+isEffectKind :: Kind n -> Bool+isEffectKind tt+ = case tt of+ TCon (TyConKind KiConEffect) -> True+ _ -> False+++-- | Check if some kind is the closure kind.+isClosureKind :: Kind n -> Bool+isClosureKind tt+ = case tt of+ TCon (TyConKind KiConClosure) -> True+ _ -> False+++-- | Check if some kind is the witness kind.+isWitnessKind :: Kind n -> Bool+isWitnessKind tt+ = case tt of+ TCon (TyConKind KiConWitness) -> True+ _ -> False+++-- Data Types -----------------------------------------------------------------+-- | Check whether this type is that of algebraic data.+--+-- It needs to have an explicit data constructor out the front,+-- and not a type variable. The constructor must not be the function+-- constructor, and must return a value of kind '*'.++-- Algebraic data types are all built from constructors+-- that have '*' as their result kind.+-- The function constructor (->) also has this result kind,+-- but it is in `TyConComp`, so is easy to ignore.+isAlgDataType :: Eq n => Type n -> Bool+isAlgDataType tt+ | Just (tc, _) <- takeTyConApps tt+ , TyConBound u <- tc+ = takeResultKind (typeOfBound u) == kData++ | otherwise+ = False+
+ DDC/Type/Pretty.hs view
@@ -0,0 +1,191 @@+{-# OPTIONS_HADDOCK hide #-}+module DDC.Type.Pretty + (module DDC.Base.Pretty)+where+import DDC.Type.Exp+import DDC.Type.Predicates+import DDC.Type.Compounds+import DDC.Base.Pretty+import qualified DDC.Type.Sum as Sum++stage = "DDC.Type.Pretty"++-- Bind -----------------------------------------------------------------------+instance (Pretty n, Eq n) => Pretty (Bind n) where+ ppr bb+ = case bb of+ BName v t -> ppr v <+> text ":" <+> ppr t+ BAnon t -> text "^" <+> text ":" <+> ppr t+ BNone t -> text "_" <+> text ":" <+> ppr t+++-- Binder ---------------------------------------------------------------------+instance Pretty n => Pretty (Binder n) where+ ppr bb+ = case bb of+ RName v -> ppr v+ RAnon -> text "^"+ RNone -> text "_"+++-- | Pretty print a binder, adding spaces after names.+-- The RAnon and None binders don't need spaces, as they're single symbols.+pprBinderSep :: Pretty n => Binder n -> Doc+pprBinderSep bb+ = case bb of+ RName v -> ppr v+ RAnon -> text "^"+ RNone -> text "_"+++-- | Print a group of binders with the same type.+pprBinderGroup :: (Pretty n, Eq n) => ([Binder n], Type n) -> Doc+pprBinderGroup (rs, t)+ = (brackets $ (sep $ map pprBinderSep rs) <+> text ":" <+> ppr t) + <> dot+++-- Bound ----------------------------------------------------------------------+instance (Pretty n, Eq n) => Pretty (Bound n) where+ ppr nn+ = case nn of+-- UName n t -> parens (ppr n <> text ":" <> ppr t)+ UName n _ -> ppr n+++ UPrim n _ -> ppr n+-- UIx i t -> parens (text "^" <> ppr i <> text ":" <> ppr t)+ UIx i _ -> text "^" <> ppr i+++-- Type -----------------------------------------------------------------------+instance (Pretty n, Eq n) => Pretty (Type n) where+ pprPrec d tt+ = case tt of+ -- Full application of function constructors are printed infix.+ TApp (TApp (TCon (TyConKind KiConFun)) k1) k2+ -> pprParen (d > 5)+ $ ppr k1 <+> text "~>" <+> ppr k2++ TApp (TApp (TCon (TyConWitness TwConImpl)) k1) k2+ -> pprParen (d > 5)+ $ ppr k1 <+> text "=>" </> pprPrec 6 k2++ TApp (TApp (TApp (TApp (TCon (TyConSpec TcConFun)) t1) eff) clo) t2+ | isBot eff, isBot clo+ -> pprParen (d > 5)+ $ (if isTFun t1 then pprPrec 6 t1 else pprPrec 5 t1)+ <+> text "->" </> ppr t2++ | otherwise+ -> pprParen (d > 5)+ $ (if isTFun t1 then pprPrec 6 t1 else pprPrec 5 t1)+ <+> text "-(" <> ppr eff <> text " | " <> ppr clo <> text ")>" + </> ppr t2+ + -- Standard types.+ TCon tc -> ppr tc+ TVar b -> ppr b++ TForall b t+ | Just (bsMore, tBody) <- takeTForalls t+ -> let groups = partitionBindsByType (b:bsMore)+ in pprParen (d > 1) + $ (cat $ map pprBinderGroup groups) <> ppr tBody+ + | otherwise+ -> pprParen (d > 1)+ $ brackets (ppr b) <> dot <> ppr t++ TApp t1 t2+ -> pprParen (d > 10)+ $ ppr t1 <+> pprPrec 11 t2++ TSum ts+ | isBot tt + -> ppr (Sum.kindOfSum ts) <> text "0"+ + | otherwise+ -> pprParen (d > 9) $ ppr ts+++isTFun :: Type n -> Bool+isTFun tt+ = case tt of+ TApp (TApp (TApp (TApp (TCon (TyConSpec TcConFun)) _) _) _) _+ -> True+ _ -> False+++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"+ | otherwise -> error $ stage ++ ": malformed sum"+ + ts -> sep $ punctuate (text " +") (map ppr ts)+++-- TyCon ----------------------------------------------------------------------+instance (Eq n, Pretty n) => Pretty (TyCon n) where+ ppr tt+ = case tt of+ TyConSort sc -> ppr sc+ TyConKind kc -> ppr kc+ TyConWitness tc -> ppr tc+ TyConSpec tc -> ppr tc+ TyConBound u -> ppr u+++instance Pretty SoCon where+ ppr sc + = case sc of+ SoConComp -> text "**"+ SoConProp -> text "@@"+++instance Pretty KiCon where+ ppr kc+ = case kc of+ KiConFun -> text "(~>)"+ KiConData -> text "*"+ KiConRegion -> text "%"+ KiConEffect -> text "!"+ KiConClosure -> text "$"+ KiConWitness -> text "@"+++instance Pretty TwCon where+ ppr tw+ = case tw of+ TwConImpl -> text "(=>)"+ TwConPure -> text "Pure"+ TwConEmpty -> text "Empty"+ TwConGlobal -> text "Global"+ TwConDeepGlobal -> text "DeepGlobal"+ TwConConst -> text "Const"+ TwConDeepConst -> text "DeepConst"+ TwConMutable -> text "Mutable"+ TwConDeepMutable-> text "DeepMutable"+ TwConLazy -> text "Lazy"+ TwConHeadLazy -> text "HeadLazy"+ TwConManifest -> text "Manifest"+ ++instance Pretty TcCon where+ ppr tc + = case tc of+ TcConFun -> text "(->)"+ TcConRead -> text "Read"+ TcConHeadRead -> text "HeadRead"+ TcConDeepRead -> text "DeepRead"+ TcConWrite -> text "Write"+ TcConDeepWrite -> text "DeepWrite"+ TcConAlloc -> text "Alloc"+ TcConDeepAlloc -> text "DeepAlloc"+ TcConUse -> text "Use"+ TcConDeepUse -> text "DeepUse"++
+ DDC/Type/Rewrite.hs view
@@ -0,0 +1,264 @@++-- | Rewriting of variable binders to anonymous form to avoid capture.+module DDC.Type.Rewrite+ ( Rewrite(..)+ , Sub(..)+ , BindStack(..)+ , pushBind+ , pushBinds+ , substBound++ , bind1, bind0, bind0s+ , use1, use0)+where+import DDC.Core.Exp+import DDC.Type.Compounds+import Data.List+import Data.Set (Set)+import qualified DDC.Type.Sum as Sum+import qualified Data.Set as Set+++-- | Substitution state.+-- Keeps track of the binders in the environment that have been rewrittten+-- to avoid variable capture or spec binder shadowing.+data Sub n+ = Sub+ { -- | Bound variable that we're substituting for.+ subBound :: Bound n++ -- | We've decended past a binder that shadows the one that we're+ -- substituting for. We're no longer substituting, but still may+ -- need to anonymise variables in types. + -- This can only happen for level-0 named binders.+ , subShadow0 :: Bool ++ -- | Level-1 names that need to be rewritten to avoid capture.+ , subConflict1 :: Set n++ -- | Level-0 names that need to be rewritten to avoid capture.+ , subConflict0 :: Set n ++ -- | Rewriting stack for level-1 names.+ , subStack1 :: BindStack n++ -- | Rewriting stack for level-0 names.+ , subStack0 :: BindStack n }+++-- | Stack of anonymous binders that we've entered under during substitution. +data BindStack n+ = BindStack+ { -- | Holds anonymous binders that were already in the program,+ -- as well as named binders that are being rewritten to anonymous ones.+ -- In the resulting expression all these binders will be anonymous.+ stackBinds :: [Bind n]++ -- | Holds all binders, independent of whether they are being rewritten or not.+ , stackAll :: [Bind n] ++ -- | Number of `BAnon` in `stackBinds`.+ , stackAnons :: Int++ -- | Number of `BName` in `stackBinds`.+ , stackNamed :: Int }+++-- | Push several binds onto the bind stack,+-- anonymyzing them if need be to avoid variable capture.+pushBinds :: Ord n => Set n -> BindStack n -> [Bind n] -> (BindStack n, [Bind n])+pushBinds fns stack bs+ = mapAccumL (pushBind fns) stack bs+++-- | Push a bind onto a bind stack, +-- anonymizing it if need be to avoid variable capture.+pushBind+ :: Ord n+ => Set n -- ^ Names that need to be rewritten.+ -> BindStack n -- ^ Current bind stack.+ -> Bind n -- ^ Bind to push.+ -> (BindStack n, Bind n) -- ^ New stack and possibly anonymised bind.++pushBind fns bs@(BindStack stack env dAnon dName) bb+ = case bb of+ -- Push already anonymous bind on stack.+ BAnon t + -> ( BindStack (BAnon t : stack) (BAnon t : env) (dAnon + 1) dName+ , BAnon t)+ + -- If the binder needs to be rewritten then push the original name on the+ -- 'stackBinds' to remember this.+ BName n t+ | Set.member n fns + -> ( BindStack (BName n t : stack) (BAnon t : env) dAnon (dName + 1)+ , BAnon t)++ | otherwise+ -> ( BindStack stack (BName n t : env) dAnon dName+ , bb)++ -- Binder was a wildcard.+ _ -> (bs, bb)++++-- | Compare a `Bound` against the one we're substituting for.+substBound+ :: Ord n+ => BindStack n -- ^ Current Bind stack during substitution.+ -> Bound n -- ^ Bound we're substituting for.+ -> Bound n -- ^ Bound we're looking at now.+ -> Either + (Bound n) -- Bound doesn't match, but replace with this one.+ Int -- Bound matches, drop the thing being substituted and + -- and lift indices this many steps.++substBound (BindStack binds _ dAnon dName) u u'+ -- Bound name matches the one that we're substituting for.+ | UName n1 _ <- u+ , UName n2 _ <- u'+ , n1 == n2+ = Right (dAnon + dName)++ -- Bound index matches the one that we're substituting for.+ | UIx i1 _ <- u+ , UIx i2 _ <- u'+ , i1 + dAnon == i2 + = Right (dAnon + dName)++ -- The Bind for this name was rewritten to avoid variable capture,+ -- so we also have to update the bound occurrence.+ | UName _ t <- u'+ , Just ix <- findIndex (boundMatchesBind u') binds+ = Left $ UIx ix t++ -- Bound index doesn't match, but lower this index by one to account+ -- for the removal of the outer binder.+ | UIx i2 t <- u'+ , i2 > dAnon+ , cutOffset <- case u of+ UIx{} -> 1+ _ -> 0+ = Left $ UIx (i2 + dName - cutOffset) t++ -- Some name that didn't match.+ | otherwise+ = Left u'+++-------------------------------------------------------------------------------+-- | Push a level-1 binder on the rewrite stack.+bind1 :: Ord n => Sub n -> Bind n -> (Sub n, Bind n)+bind1 sub b + = let (stackT', b') = pushBind (subConflict1 sub) (subStack1 sub) b+ in (sub { subStack1 = stackT' }, b')+++-- | Push a level-0 binder on the rewrite stack.+bind0 :: Ord n => Sub n -> Bind n -> (Sub n, Bind n)+bind0 sub b + = let b1 = rewriteWith sub b+ (stackX', b2) = pushBind (subConflict0 sub) (subStack0 sub) b1+ in ( sub { subStack0 = stackX'+ , subShadow0 = subShadow0 sub + || namedBoundMatchesBind (subBound sub) b2 }+ , b2)+++-- | Push some level-0 binders on the rewrite stack.+bind0s :: Ord n => Sub n -> [Bind n] -> (Sub n, [Bind n])+bind0s = mapAccumL bind0+++-- | Rewrite a use of a level-1 binder if need be.+use1 :: Ord n => Sub n -> Bound n -> Bound n+use1 sub u+ | UName _ t <- u+ , BindStack binds _ _ _ <- subStack1 sub+ , Just ix <- findIndex (boundMatchesBind u) binds+ = UIx ix t++ | otherwise+ = u+++-- | Rewrite the use of a level-0 binder if need be.+use0 :: Ord n => Sub n -> Bound n -> Bound n+use0 sub u+ | UName _ t <- u+ , BindStack binds _ _ _ <- subStack0 sub+ , Just ix <- findIndex (boundMatchesBind u) binds+ = UIx ix (rewriteWith sub t)++ | otherwise+ = rewriteWith sub u+++-------------------------------------------------------------------------------+class Rewrite (c :: * -> *) where+ -- | Rewrite names in some thing to anonymous form if they conflict with+-- any names in the `Sub` state.+ rewriteWith :: Ord n => Sub n -> c n -> c n +++instance Rewrite Bind where+ rewriteWith sub bb+ = replaceTypeOfBind (rewriteWith sub (typeOfBind bb)) bb+++instance Rewrite Bound where+ rewriteWith sub uu+ = replaceTypeOfBound (rewriteWith sub (typeOfBound uu)) uu+++instance Rewrite LetMode where+ rewriteWith sub lm+ = case lm of+ LetStrict -> lm+ LetLazy (Just t) -> LetLazy (Just $ rewriteWith sub t) + LetLazy Nothing -> LetLazy Nothing+++instance Rewrite Cast where+ rewriteWith sub cc+ = let down = rewriteWith sub + in case cc of+ CastWeakenEffect eff -> CastWeakenEffect (down eff)+ CastWeakenClosure clo -> CastWeakenClosure (down clo)+ CastPurify w -> CastPurify (down w)+ CastForget w -> CastForget (down w)+++instance Rewrite Type where+ rewriteWith sub tt + = let down = rewriteWith + in case tt of+ TVar u -> TVar (use1 sub u)+ TCon{} -> tt++ TForall b t+ -> let (sub1, b') = bind1 sub b+ t' = down sub1 t+ in TForall b' t'++ TApp t1 t2 -> TApp (down sub t1) (down sub t2)+ TSum ts -> TSum (down sub ts)+++instance Rewrite TypeSum where+ rewriteWith sub ts+ = Sum.fromList (Sum.kindOfSum ts)+ $ map (rewriteWith sub)+ $ Sum.toList ts+++instance Rewrite Witness where+ rewriteWith sub ww+ = let down = rewriteWith + 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)
+ DDC/Type/Subsumes.hs view
@@ -0,0 +1,32 @@+module DDC.Type.Subsumes+ (subsumesT)+where+import DDC.Type.Exp+import DDC.Type.Predicates+import DDC.Type.Transform.Crush+import DDC.Type.Transform.Trim+import qualified DDC.Type.Sum as Sum+import Control.Monad+++-- | Check whether the first type subsumes the second.+--+-- Both arguments are converted to sums, and we check that every+-- element of the second sum is equivalent to an element in the first.+--+-- This only works for well formed types of effect and closure kind.+-- Other types will yield `False`.+subsumesT :: Ord n => Kind n -> Type n -> Type n -> Bool+subsumesT k t1 t2+ | isEffectKind k+ , ts1 <- Sum.singleton k $ crushEffect t1+ , ts2 <- Sum.singleton k $ crushEffect t2+ = and $ [ Sum.elem t ts1 | t <- Sum.toList ts2 ]++ | isClosureKind k+ , Just ts1 <- liftM (Sum.singleton k) $ trimClosure t1+ , Just ts2 <- liftM (Sum.singleton k) $ trimClosure t2+ = and $ [ Sum.elem t ts1 | t <- Sum.toList ts2 ]++ | otherwise+ = False
+ DDC/Type/Sum.hs view
@@ -0,0 +1,304 @@++-- | Utilities for working with `TypeSum`s.+--+module DDC.Type.Sum + ( empty+ , singleton+ , elem+ , insert+ , delete+ , union+ , unions+ , difference+ , kindOfSum+ , toList, fromList+ , hashTyCon, hashTyConRange+ , unhashTyCon+ , takeSumArrayElem+ , makeSumArrayElem)+where+import DDC.Type.Exp+import Data.Array+import qualified Data.List as L+import qualified Data.Map as Map+import qualified Data.Set as Set+import Prelude hiding (elem)+++-- | Construct an empty type sum of the given kind.+empty :: Kind n -> TypeSum n+empty k = TypeSum+ { typeSumKind = k+ , typeSumElems = listArray hashTyConRange (repeat Set.empty)+ , typeSumBoundNamed = Map.empty+ , typeSumBoundAnon = Map.empty+ , typeSumSpill = [] }+++-- | Construct a type sum containing a single element.+singleton :: Ord n => Kind n -> Type n -> TypeSum n+singleton k t+ = insert t (empty k)+++-- | Check whether an element is a member of a sum.+--+-- * Returns True when the first argument is $0 or !0.+--+-- * Returns False when the first argument is another sum.+--+-- * May return False if the first argument is miskinded but still+-- alpha-equivalent to some component of the sum.+elem :: (Eq n, Ord n) => Type n -> TypeSum n -> Bool+elem t ts + = case t of+ TVar (UName n _) -> Map.member n (typeSumBoundNamed ts)+ TVar (UPrim n _) -> Map.member n (typeSumBoundNamed ts)+ TVar (UIx i _) -> Map.member i (typeSumBoundAnon ts)+ TCon{} -> L.elem t (typeSumSpill ts)++ -- Foralls can't be a part of well-kinded sums.+ -- Just check whether the types are strucutrally equal+ -- without worring about alpha-equivalence.+ TForall{} -> L.elem t (typeSumSpill ts)++ TApp (TCon _) _+ | Just (h, vc) <- takeSumArrayElem t+ , tsThere <- typeSumElems ts ! h+ -> Set.member vc tsThere++ TApp{} -> L.elem t (typeSumSpill ts) ++ -- Treat bottom effect and closures as always+ -- being part of the sum.+ TSum ts1+ -> case toList ts1 of+ [] | TCon (TyConKind KiConEffect) <- typeSumKind ts1 + , TCon (TyConKind KiConEffect) <- typeSumKind ts+ -> True++ | TCon (TyConKind KiConClosure) <- typeSumKind ts1+ , TCon (TyConKind KiConClosure) <- typeSumKind ts+ -> True++ _ -> False+++-- | Insert a new element into a sum.+insert :: Ord n => Type n -> TypeSum n -> TypeSum n+insert t ts+ = case t of+ TVar (UName n k) -> ts { typeSumBoundNamed = Map.insert n k (typeSumBoundNamed ts) }+ TVar (UPrim n k) -> ts { typeSumBoundNamed = Map.insert n k (typeSumBoundNamed ts) }+ TVar (UIx i k) -> ts { typeSumBoundAnon = Map.insert i k (typeSumBoundAnon ts) }+ TCon{} -> ts { typeSumSpill = t : typeSumSpill ts }++ -- Foralls can't be part of well-kinded sums.+ -- Just add them to the splill lists so that we can still+ -- pretty print such mis-kinded types.+ TForall{} -> ts { typeSumSpill = t : typeSumSpill ts }++ TApp (TCon _) _+ | Just (h, vc) <- takeSumArrayElem t+ , tsThere <- typeSumElems ts ! h+ -> if Set.member vc tsThere+ then ts+ else ts { typeSumElems = (typeSumElems ts) // [(h, Set.insert vc tsThere)] }+ + TApp{} -> ts { typeSumSpill = t : typeSumSpill ts }+ + TSum ts' -> foldr insert ts (toList ts')+++-- | Delete an element from a sum.+delete :: Ord n => Type n -> TypeSum n -> TypeSum n+delete t ts+ = case t of+ TVar (UName n _) -> ts { typeSumBoundNamed = Map.delete n (typeSumBoundNamed ts) }+ TVar (UPrim n _) -> ts { typeSumBoundNamed = Map.delete n (typeSumBoundNamed ts) }+ TVar (UIx i _) -> ts { typeSumBoundAnon = Map.delete i (typeSumBoundAnon ts) }+ TCon{} -> ts { typeSumSpill = L.delete t (typeSumSpill ts) }+ TForall{} -> ts { typeSumSpill = L.delete t (typeSumSpill ts) }+ + TApp (TCon _) _+ | Just (h, vc) <- takeSumArrayElem t+ , tsThere <- typeSumElems ts ! h+ -> ts { typeSumElems = (typeSumElems ts) // [(h, Set.delete vc tsThere)] }+ + TApp{} -> ts { typeSumSpill = L.delete t (typeSumSpill ts) }+ + TSum ts' -> foldr delete ts (toList ts')+++-- | Add two type sums.+union :: Ord n => TypeSum n -> TypeSum n -> TypeSum n+union ts1 ts2 + = foldr insert ts2 (toList ts1)+++-- | Union a list of `TypeSum`s together.+unions :: Ord n => Kind n -> [TypeSum n] -> TypeSum n+unions k [] = empty k+unions _ (t:ts) = foldr union t ts++++-- | Delete all members of the second sum from the first one.+difference :: Ord n => TypeSum n -> TypeSum n -> TypeSum n+difference ts1 ts2+ = foldr delete ts1 (toList ts2)+++-- | Take the kind of a sum.+kindOfSum :: TypeSum n -> Kind n+kindOfSum ts+ = typeSumKind ts+++-- | Flatten out a sum, yielding a list of individual terms.+toList :: TypeSum n -> [Type n]+toList TypeSum+ { typeSumKind = _kind+ , typeSumElems = sumElems+ , typeSumBoundNamed = named+ , typeSumBoundAnon = anon+ , typeSumSpill = spill}++ = [ makeSumArrayElem h vc+ | (h, ts) <- assocs sumElems, vc <- Set.toList ts] + ++ [TVar $ UName n k | (n, k) <- Map.toList named]+ ++ [TVar $ UIx i k | (i, k) <- Map.toList anon]+ ++ spill+ ++-- | Convert a list of types to a `TypeSum`+fromList :: Ord n => Kind n -> [Type n] -> TypeSum n+fromList k ts+ = foldr insert (empty k) ts+++-- | Yield the `TyConHash` of a `TyCon`, or `Nothing` if there isn't one.+hashTyCon :: TyCon n -> Maybe TyConHash+hashTyCon tc+ = case tc of+ TyConSpec tc' -> hashTcCon tc'+ _ -> Nothing+ ++-- | Yield the `TyConHash` of a `TyConBuiltin`, or `Nothing` if there isn't one.+hashTcCon :: TcCon -> Maybe TyConHash+hashTcCon tc+ = case tc of+ TcConRead -> Just $ TyConHash 0+ TcConDeepRead -> Just $ TyConHash 1+ TcConWrite -> Just $ TyConHash 2+ TcConDeepWrite -> Just $ TyConHash 3+ TcConAlloc -> Just $ TyConHash 4+ TcConUse -> Just $ TyConHash 5+ TcConDeepUse -> Just $ TyConHash 6+ _ -> Nothing+++-- | The range of hashes that can be produced by `hashTyCon`.+hashTyConRange :: (TyConHash, TyConHash)+hashTyConRange+ = ( TyConHash 0+ , TyConHash 6)+ ++-- | Yield the `TyCon` corresponding to a `TyConHash`, or `error` if there isn't one.+unhashTyCon :: TyConHash -> TyCon n+unhashTyCon (TyConHash i)+ = TyConSpec+ $ case i of+ 0 -> TcConRead+ 1 -> TcConDeepRead+ 2 -> TcConWrite+ 3 -> TcConDeepWrite+ 4 -> TcConAlloc+ 5 -> TcConUse+ 6 -> TcConDeepUse++ -- This should never happen, because we only produce hashes+ -- with the above 'hashTyCon' function.+ _ -> error $ "DDC.Type.Sum: bad TyConHash " ++ show i+++-- | If this type can be put in one of our arrays then split it+-- into the hash and the argument.+takeSumArrayElem :: Type n -> Maybe (TyConHash, TypeSumVarCon n)+takeSumArrayElem (TApp (TCon tc) t2)+ | Just h <- hashTyCon tc+ = case t2 of+ TVar u -> Just (h, TypeSumVar u)+ TCon (TyConBound u) -> Just (h, TypeSumCon u)+ _ -> Nothing+ +takeSumArrayElem _ = Nothing+++-- | Inverse of `takeSumArrayElem`.+makeSumArrayElem :: TyConHash -> TypeSumVarCon n -> Type n+makeSumArrayElem h vc+ = let tc = unhashTyCon h+ in case vc of+ TypeSumVar u -> TApp (TCon tc) (TVar u)+ TypeSumCon u -> TApp (TCon tc) (TCon (TyConBound u))+++-- Type Equality --------------------------------------------------------------+-- Code for type equality is in this module because we need to normalise sums+-- when deciding if two types are equal.++deriving instance Eq n => Eq (TyCon n)+deriving instance Eq n => Eq (Bound n)+deriving instance Eq n => Eq (Bind n)+++instance Eq n => Eq (Type n) where+ (==) t1 t2+ = case (normalise t1, normalise t2) of+ (TVar u1, TVar u2) -> u1 == u2+ (TCon tc1, TCon tc2) -> tc1 == tc2+ (TForall b1 t11, TForall b2 t22) -> b1 == b2 && t11 == t22+ (TApp t11 t12, TApp t21 t22) -> t11 == t21 && t12 == t22+ (TSum ts1, TSum ts2) -> ts1 == ts2+ (_, _) -> False++ -- Unwrap single element sums into plain types.+ where normalise (TSum ts)+ | [t'] <- toList ts = t'++ normalise t' = t'+++instance Eq n => Eq (TypeSum n) where+ (==) ts1 ts2++ -- If the sum is empty, then just compare the kinds.+ | [] <- toList ts1 + , [] <- toList ts2+ = typeSumKind ts1 == typeSumKind ts2++ -- If the sum has elements, then compare them directly and ignore the+ -- kind. This allows us to use (tBot sComp) as the typeSumKind field+ -- when we want to compute the real kind based on the elements. + | otherwise+ = typeSumElems ts1 == typeSumElems ts2+ && typeSumBoundNamed ts1 == typeSumBoundNamed ts2+ && typeSumBoundAnon ts1 == typeSumBoundAnon ts2+ && typeSumSpill ts1 == typeSumSpill ts2+++instance Ord n => Ord (Bound n) where+ compare (UName n1 _) (UName n2 _) = compare n1 n2+ compare (UIx i1 _) (UIx i2 _) = compare i1 i2+ compare (UPrim n1 _) (UPrim n2 _) = compare n1 n2+ compare (UIx _ _) _ = LT+ compare (UName _ _) (UIx _ _) = GT+ compare (UName _ _) (UPrim _ _) = LT+ compare (UPrim _ _) _ = GT++deriving instance Eq n => Eq (TypeSumVarCon n)+deriving instance Ord n => Ord (TypeSumVarCon n)+
+ DDC/Type/Transform/Crush.hs view
@@ -0,0 +1,152 @@+module DDC.Type.Transform.Crush+ (crushEffect)+where+import DDC.Type.Predicates+import DDC.Type.Compounds+import DDC.Type.Exp+import qualified DDC.Type.Sum as Sum+++-- | Crush compound effect terms into their components.+--+-- This is like `trimClosure` but for effects instead of closures.+-- +-- For example, crushing @DeepRead (List r1 (Int r2))@ yields @(Read r1 + Read r2)@.+--+crushEffect :: Ord n => Effect n -> Effect n+crushEffect tt+ = case tt of+ TVar{} -> tt+ TCon{} -> tt+ TForall b t+ -> TForall b (crushEffect t)++ TSum ts + -> TSum+ $ Sum.fromList (Sum.kindOfSum ts) + $ map crushEffect+ $ Sum.toList ts++ TApp t1 t2+ -- Head Read.+ | Just (TyConSpec TcConHeadRead, [t]) <- takeTyConApps tt+ -> case takeTyConApps t of++ -- Type has a head region.+ Just (TyConBound u, (tR : _)) + | (k1 : _, _) <- takeKFuns (typeOfBound u)+ , isRegionKind k1+ -> tRead tR++ -- Type has no head region.+ -- This happens with case () of { ... }+ Just (TyConBound _, []) -> tBot kEffect++ _ -> tt++ -- Deep Read.+ -- See Note: Crushing with higher kinded type vars.+ | Just (TyConSpec TcConDeepRead, [t]) <- takeTyConApps tt+ -> case takeTyConApps t of+ Just (TyConBound u, ts)+ | (ks, _) <- takeKFuns (typeOfBound u)+ , length ks == length ts+ , Just effs <- sequence $ zipWith makeDeepRead ks ts+ -> crushEffect $ TSum $ Sum.fromList kEffect effs++ _ -> tt++ -- Deep Write+ -- See Note: Crushing with higher kinded type vars.+ | Just (TyConSpec TcConDeepWrite, [t]) <- takeTyConApps tt+ -> case takeTyConApps t of+ Just (TyConBound u, ts)+ | (ks, _) <- takeKFuns (typeOfBound u)+ , length ks == length ts+ , Just effs <- sequence $ zipWith makeDeepWrite ks ts+ -> crushEffect $ TSum $ Sum.fromList kEffect effs++ _ -> tt ++ -- Deep Alloc+ -- See Note: Crushing with higher kinded type vars.+ | Just (TyConSpec TcConDeepAlloc, [t]) <- takeTyConApps tt+ -> case takeTyConApps t of+ Just (TyConBound u, ts)+ | (ks, _) <- takeKFuns (typeOfBound u)+ , length ks == length ts+ , Just effs <- sequence $ zipWith makeDeepAlloc ks ts+ -> crushEffect $ TSum $ Sum.fromList kEffect effs++ _ -> tt++ -- TODO: we're hijacking crushEffect to work on witnesses as well.+ -- we should split this into another function.+ -- Deep Global+ -- See Note: Crushing with higher kinded type vars.+ | Just (TyConWitness TwConDeepGlobal, [t]) <- takeTyConApps tt+ -> case takeTyConApps t of+ Just (TyConBound u, ts)+ | (ks, _) <- takeKFuns (typeOfBound u)+ , length ks == length ts+ , Just props <- sequence $ zipWith makeDeepGlobal ks ts+ -> crushEffect $ TSum $ Sum.fromList kWitness props++ _ -> tt ++ | otherwise+ -> TApp (crushEffect t1) (crushEffect t2)+++-- | If this type has first order kind then wrap with the +-- appropriate read effect.+makeDeepRead :: Kind n -> Type n -> Maybe (Effect n)+makeDeepRead k t+ | isRegionKind k = Just $ tRead t+ | isDataKind k = Just $ tDeepRead t+ | isClosureKind k = Just $ tBot kEffect+ | isEffectKind k = Just $ tBot kEffect+ | otherwise = Nothing+++-- | If this type has first order kind then wrap with the +-- appropriate read effect.+makeDeepWrite :: Kind n -> Type n -> Maybe (Effect n)+makeDeepWrite k t+ | isRegionKind k = Just $ tWrite t+ | isDataKind k = Just $ tDeepWrite t+ | isClosureKind k = Just $ tBot kEffect+ | isEffectKind k = Just $ tBot kEffect+ | otherwise = Nothing+++-- | If this type has first order kind then wrap with the +-- appropriate read effect.+makeDeepAlloc :: Kind n -> Type n -> Maybe (Effect n)+makeDeepAlloc k t+ | isRegionKind k = Just $ tAlloc t+ | isDataKind k = Just $ tDeepAlloc t+ | isClosureKind k = Just $ tBot kEffect+ | isEffectKind k = Just $ tBot kEffect+ | otherwise = Nothing+++-- | If this type has first order kind then wrap with the +-- appropriate read effect.+makeDeepGlobal :: Kind n -> Type n -> Maybe (Type n)+makeDeepGlobal k t+ | isRegionKind k = Just $ tGlobal t+ | isDataKind k = Just $ tDeepGlobal t+ | isClosureKind k = Nothing+ | isEffectKind k = Just $ tBot kEffect+ | otherwise = Nothing+++{- [Note: Crushing with higher kinded type vars]+ ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~+ We can't just look at the free variables here and wrap Read and DeepRead constructors+ around them, as the type may contain higher kinded type variables such as: (t a).+ Instead, we'll only crush the effect when all variable have first-order kind.+ When comparing types with higher order variables, we'll have to use the type+ equivalence checker, instead of relying on the effects to be pre-crushed.+-}
+ DDC/Type/Transform/Instantiate.hs view
@@ -0,0 +1,27 @@++module DDC.Type.Transform.Instantiate+ ( instantiateT+ , instantiateTs)+where+import DDC.Type.Exp+import DDC.Type.Transform.SubstituteT+import DDC.Base.Pretty (Pretty)+++-- | Instantiate a type with an argument.+-- The type to be instantiated must have an outer forall, else `Nothing`.+instantiateT :: (Ord n, Pretty n) => Type n -> Type n -> Maybe (Type n)+instantiateT (TForall b tBody) t2 = Just $ substituteT b t2 tBody+instantiateT _ _ = Nothing+++-- | Instantiate a type with several arguments.+-- The type to be instantiated must have at least as many outer foralls +-- as provided type arguments, else `Nothing`.+instantiateTs :: (Ord n, Pretty n) => Type n -> [Type n] -> Maybe (Type n)+instantiateTs t [] = Just t+instantiateTs t (tArg:tsArgs)+ = case instantiateT t tArg of+ Nothing -> Nothing+ Just t' -> instantiateTs t' tsArgs+
+ DDC/Type/Transform/LiftT.hs view
@@ -0,0 +1,63 @@++-- | Lifting of deBruijn indices in a type.+---+-- TODO: merge this code with LowerT+module DDC.Type.Transform.LiftT+ (LiftT(..))+where+import DDC.Type.Exp+import DDC.Type.Compounds+import qualified DDC.Type.Sum as Sum+++class LiftT (c :: * -> *) where++ -- | Lift type indices that are at least a certain depth by the given number of levels.+ liftAtDepthT + :: forall n. Ord n+ => Int -- ^ Number of levels to lift.+ -> Int -- ^ Current binding depth.+ -> c n -- ^ Lift type indices in this thing.+ -> c n+ + -- | Wrapper for `liftAtDepthT` that starts at depth 0. + liftT :: forall n. Ord n+ => Int -- ^ Number of levels to lift+ -> c n -- ^ Lift type indices in this thing.+ -> c n+ + liftT n xx = liftAtDepthT n 0 xx+ ++instance LiftT Bind where+ liftAtDepthT n d bb+ = replaceTypeOfBind (liftAtDepthT n d $ typeOfBind bb) bb+ ++instance LiftT Bound where+ liftAtDepthT n d uu+ = case uu of+ UName{} -> uu+ UPrim{} -> uu+ UIx i t + | d <= i -> UIx (i + n) t+ | otherwise -> uu+ ++instance LiftT Type where+ liftAtDepthT n d tt+ = let down = liftAtDepthT n+ in case tt of+ TVar u -> TVar (down d u)+ TCon{} -> tt+ TForall b t -> TForall (down d b) (down (d + 1) t)+ TApp t1 t2 -> TApp (down d t1) (down d t2)+ TSum ss -> TSum (down d ss)+++instance LiftT TypeSum where+ liftAtDepthT n d ss+ = Sum.fromList (liftAtDepthT n d $ Sum.kindOfSum ss)+ $ map (liftAtDepthT n d)+ $ Sum.toList ss+
+ DDC/Type/Transform/LowerT.hs view
@@ -0,0 +1,63 @@++-- | Lowering of deBruijn indices in a type.+---+-- TODO: merge this code with LiftT.+module DDC.Type.Transform.LowerT+ (LowerT(..))+where+import DDC.Type.Exp+import DDC.Type.Compounds+import qualified DDC.Type.Sum as Sum+++class LowerT (c :: * -> *) where++ -- | Lower type indices that are at least a certain depth by the given number of levels.+ lowerAtDepthT + :: forall n. Ord n+ => Int -- ^ Number of levels to lower.+ -> Int -- ^ Current binding depth.+ -> c n -- ^ Lower type indices in this thing.+ -> c n+ + -- | Wrapper for `lowerAtDepthT` that starts at depth 0. + lowerT :: forall n. Ord n+ => Int -- ^ Number of levels to lower.+ -> c n -- ^ Lower type indices in this thing.+ -> c n+ + lowerT n xx = lowerAtDepthT n 0 xx+ ++instance LowerT Bind where+ lowerAtDepthT n d bb+ = replaceTypeOfBind (lowerAtDepthT n d $ typeOfBind bb) bb+ ++instance LowerT Bound where+ lowerAtDepthT n d uu+ = case uu of+ UName{} -> uu+ UPrim{} -> uu+ UIx i t + | d <= i -> UIx (i - n) t+ | otherwise -> uu+ ++instance LowerT Type where+ lowerAtDepthT n d tt+ = let down = lowerAtDepthT n + in case tt of+ TVar uu -> TVar (down d uu)+ TCon{} -> tt+ TForall b t -> TForall (down d b) (down (d + 1) t)+ TApp t1 t2 -> TApp (down d t1) (down d t2)+ TSum ss -> TSum (down d ss)+++instance LowerT TypeSum where+ lowerAtDepthT n d ss+ = Sum.fromList (lowerAtDepthT n d $ Sum.kindOfSum ss)+ $ map (lowerAtDepthT n d)+ $ Sum.toList ss+
+ DDC/Type/Transform/SpreadT.hs view
@@ -0,0 +1,67 @@+ +module DDC.Type.Transform.SpreadT+ (SpreadT(..))+where+import DDC.Type.Exp+import DDC.Type.Env (Env)+import qualified DDC.Type.Env as Env+import qualified DDC.Type.Sum as T+++class SpreadT (c :: * -> *) where++ -- | Spread type annotations from variable binders in to the bound+ -- occurrences.+ spreadT :: forall n. Ord n + => Env n -> c n -> c n+ ++instance SpreadT Type where+ spreadT kenv tt+ = case tt of+ TVar u -> TVar $ spreadT kenv u+ TCon tc -> TCon $ spreadT kenv tc++ TForall b t+ -> let b' = spreadT kenv b+ in TForall b' $ spreadT (Env.extend b' kenv) t++ TApp t1 t2 -> TApp (spreadT kenv t1) (spreadT kenv t2)+ TSum ss -> TSum (spreadT kenv ss)+ ++instance SpreadT TypeSum where+ spreadT kenv ss+ = T.fromList (spreadT kenv $ T.kindOfSum ss)+ $ map (spreadT kenv)+ $ T.toList ss+++instance SpreadT Bind where+ spreadT kenv bb+ = case bb of+ BName n t -> BName n (spreadT kenv t)+ BAnon t -> BAnon (spreadT kenv t)+ BNone t -> BNone (spreadT kenv t)+++instance SpreadT Bound where+ spreadT kenv uu+ | Just t' <- Env.lookup uu kenv+ = case uu of+ UIx ix _ -> UIx ix t'+ UPrim n _ -> UPrim n t'+ UName n _+ -> if Env.isPrim kenv n + then UPrim n t'+ else UName n t'+ + | otherwise = uu+++instance SpreadT TyCon where+ spreadT kenv tc+ = case tc of+ TyConBound u -> TyConBound (spreadT kenv u)+ _ -> tc+
+ DDC/Type/Transform/SubstituteT.hs view
@@ -0,0 +1,138 @@++-- | Capture avoiding substitution of types in types.+module DDC.Type.Transform.SubstituteT+ ( SubstituteT(..)+ , substituteT+ , substituteTs+ , substituteBoundT++ , BindStack(..)+ , pushBind+ , pushBinds+ , substBound)+where+import DDC.Type.Exp+import DDC.Type.Compounds+import DDC.Core.Collect+import DDC.Type.Transform.LiftT+import DDC.Type.Transform.Crush+import DDC.Type.Transform.Trim+import DDC.Type.Rewrite+import Data.Maybe+import qualified DDC.Type.Sum as Sum+import qualified DDC.Type.Env as Env+import qualified Data.Set as Set+import Data.Set (Set)+++-- | Substitute a `Type` for the `Bound` corresponding to some `Bind` in a thing.+substituteT :: (SubstituteT c, Ord n) => Bind n -> Type n -> c n -> c n+substituteT b t x+ = case takeSubstBoundOfBind b of+ Just u -> substituteBoundT u t x+ _ -> x+++-- | Wrapper for `substituteT` to substitute multiple things.+substituteTs :: (SubstituteT c, Ord n) => [(Bind n, Type n)] -> c n -> c n+substituteTs bts x+ = foldr (uncurry substituteT) x bts+++-- | Substitute a `Type` for `Bound` in some thing.+substituteBoundT :: (SubstituteT c, Ord n) => Bound n -> Type n -> c n -> c n+substituteBoundT u t x+ = let -- Determine the free names in the type we're subsituting.+ -- We'll need to rename binders with the same names as these+ freeNames = Set.fromList+ $ mapMaybe takeNameOfBound + $ Set.toList + $ freeT Env.empty t++ stack = BindStack [] [] 0 0+ + in substituteWithT u t freeNames stack x+++-- SubstituteT ----------------------------------------------------------------+class SubstituteT (c :: * -> *) where++ -- | Substitute a type into some thing.+ -- In the target, if we find a named binder that would capture a free variable+ -- in the type to substitute, then we rewrite that binder to anonymous form,+ -- avoiding the capture.+ substituteWithT+ :: forall n. Ord n+ => Bound n -- ^ Bound variable that we're subsituting into.+ -> Type n -- ^ Type to substitute.+ -> Set n -- ^ Names of free varaibles in the type to substitute.+ -> BindStack n -- ^ Bind stack.+ -> c n -> c n+++-- Instances ------------------------------------------------------------------+instance SubstituteT Bind where+ substituteWithT u fvs t stack bb+ = let k' = substituteWithT u fvs t stack $ typeOfBind bb+ in replaceTypeOfBind k' bb+ + +instance SubstituteT Type where+ substituteWithT u t fns stack tt+ = let down = substituteWithT u t fns stack+ in case tt of+ TCon{} -> tt++ -- Crush out compound effects and closures as we substitute them.+ TApp t1 t2+ -> case t1 of+ TCon (TyConSpec TcConHeadRead) + -> crushEffect (TApp t1 (down t2))++ TCon (TyConSpec TcConDeepRead) + -> crushEffect (TApp t1 (down t2))++ TCon (TyConSpec TcConDeepWrite) + -> crushEffect (TApp t1 (down t2))++ TCon (TyConSpec TcConDeepAlloc) + -> crushEffect (TApp t1 (down t2))++ -- If the closure is miskinded then trimClosure can + -- return Nothing, so we leave it untrimmed.+ TCon (TyConSpec TcConDeepUse)+ -> fromMaybe tt (trimClosure (TApp t1 (down t2)))++ _ -> TApp (down t1) (down t2)++ TSum ss + -> TSum (down ss)++ TForall b tBody+ | namedBoundMatchesBind u b -> tt+ | otherwise+ -> let -- Substitute into the annotation on the binder.+ bSub = down b++ -- Push bind onto stack, and anonymise to avoid capture if needed+ (stack', b') = pushBind fns stack bSub+ + -- Substitute into body.+ tBody' = substituteWithT u t fns stack' tBody++ in TForall b' tBody'++ TVar u'+ -> case substBound stack u u' of+ Left u'' -> TVar u''+ Right n -> liftT n t+ ++instance SubstituteT TypeSum where+ substituteWithT u n fns stack ss+ = let k = substituteWithT u n fns stack+ $ Sum.kindOfSum ss+ in Sum.fromList k + $ map (substituteWithT u n fns stack)+ $ Sum.toList ss+
+ DDC/Type/Transform/Trim.hs view
@@ -0,0 +1,163 @@++module DDC.Type.Transform.Trim + (trimClosure)+where+import DDC.Core.Collect+import DDC.Type.Check.CheckCon+import DDC.Type.Exp+import DDC.Type.Compounds+import DDC.Type.Predicates+import Control.Monad+import Data.Set (Set)+import qualified DDC.Type.Env as Env+import qualified DDC.Type.Sum as Sum+import qualified Data.Set as Set+++-- | Trim compound closures into their components. +--+-- This is like `crushEffect`, but for closures instead of effects.+--+-- For example, trimming @Int r2 -(Read r1 | Use r1)> Int r2@ yields just @Use r1@. +-- Only @r1@ might contain an actual store object that is reachable from a function+-- closure with such a type.+--+-- This function assumes the closure is well-kinded, and may return `Nothing` if+-- this is not the case.+trimClosure + :: Ord n+ => Closure n + -> Maybe (Closure n)++trimClosure cc+ = liftM TSum $ trimToSumC cc+++-- | Trim a closure down to a closure sum.+-- May return 'Nothing' if the closure is mis-kinded.+trimToSumC + :: forall n. Ord n+ => Closure n -> Maybe (TypeSum n)++trimToSumC cc+ = case cc of+ -- Keep closure variables.+ TVar{} -> Just $ Sum.singleton kClosure cc++ -- There aren't any naked constructors of closure type.+ -- If we find a constructor the closure is miskinded.+ TCon{} -> Nothing+ + -- The body of a forall should have data or witness kind.+ -- If we find a forall then the closure is miskinded.+ TForall{} -> Nothing++ -- Keep use constructor applied to a region.+ TApp (TCon (TyConSpec TcConUse)) _+ -> Just $ Sum.singleton kClosure cc+ + -- Trim DeepUse constructor applied to a data type.+ TApp (TCon (TyConSpec TcConDeepUse)) t2 + -> Just $ trimDeepUsedD t2++ -- Some other constructor we don't know about,+ -- perhaps using a type variable of higher kind.+ TApp{} -> Just $ Sum.singleton kClosure cc++ -- Trim components of a closure sum and rebuild the sum.+ TSum ts+ -> case sequence $ map trimToSumC $ Sum.toList ts of+ Nothing -> Nothing+ Just sums -> Just $ Sum.fromList kClosure+ $ concatMap Sum.toList sums+++-- | Trim the argument of a DeepUsed constructor down to a closure sum.+-- The argument is of data kind.+trimDeepUsedD + :: forall n. Ord n+ => Type n -> TypeSum n++trimDeepUsedD tt+ = case tt of+ -- Keep type variables.+ TVar{} -> Sum.singleton kClosure $ tDeepUse tt++ -- Naked data constructors like 'Unit' don't contain region variables,+ -- but the interpreter uses constructors of region kind to encode+ -- region handes, that we need to keep.+ TCon tc+ | Just k <- takeKindOfTyCon tc+ , isRegionKind k+ -> Sum.singleton kClosure $ tDeepUse tt++ | otherwise+ -> Sum.empty kClosure++ -- Add locally bound variable to the environment.+ -- See Note: Trimming Foralls. + TForall{}+ -> let ns = freeT Env.empty tt :: Set (Bound n)+ in if Set.size ns == 0+ then Sum.empty kClosure+ else Sum.singleton kClosure $ tDeepUse tt++ -- Trim function constructors.+ -- See Note: Material variables and the interpreter+ TApp (TApp (TApp (TApp (TCon (TyConSpec TcConFun)) _t1) _eff) clo) _t2+ -> Sum.singleton kClosure clo++ -- Trim a type application.+ -- See Note: Trimming with higher kinded type vars.+ TApp{}+ -> case takeTyConApps tt of+ Just (tc, args) + | Just k <- takeKindOfTyCon tc+ , Just cs <- sequence $ zipWith makeUsed (takeKFuns' k) args+ -> Sum.fromList kClosure cs++ _ -> Sum.singleton kClosure $ tDeepUse tt++ -- We shouldn't get sums of data types in regular code, + -- but the (tBot kData) form might appear in debugging. + TSum{} -> Sum.singleton kClosure $ tDeepUse tt+++-- | Make the appropriate Use term for a type of the given kind, or `Nothing` if+-- there isn't one. Also recursively trim types of data kind.+makeUsed :: (Eq n, Ord n) => Kind n -> Type n -> Maybe (Closure n)+makeUsed k t+ | isRegionKind k = Just $ tUse t+ | isDataKind k = Just $ TSum $ trimDeepUsedD t+ | isEffectKind k = Just $ tBot kClosure+ | isClosureKind k = Just $ t+ | otherwise = Nothing +++{- [Note: Trimming with higher kinded type vars]+ ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~+ We can't just look at the free variables here and wrap Use and DeepUse constructors+ around them, as the type may contain higher kinded type variables such as: (t a).+ We cannot simply drop such variables, as they may be substituted for types that+ contain components that we must keep in the closure. To handle this, when we see+ higher kinded type varibles we preserve the entire type application, which is+ DeepUse (t a) in this example.++ [Note: Trimming Foralls]+ ~~~~~~~~~~~~~~~~~~~~~~~~+ For now we just drop the forall if the free vars list is empty. This is ok because+ we only do this at top-level, so don't need to lower debruijn indices to account for+ deleted intermediate quantifiers.++ [Note: Material variables and the interpreter]+ ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~+ Even though we're not tracking material vars properly yet, + for the interpreter we need to ignore the non-material parameters of the+ function constructor so that we can treat store location constructors as+ having an empty closure. For example:++ L2# :: Int R1# -> Int R1#+ + This does not capture the R1# region, even the handle for it is in its type.+-}+
+ DDC/Type/Universe.hs view
@@ -0,0 +1,116 @@++-- | Universes of the Disciple Core language.+module DDC.Type.Universe+ ( Universe(..)+ , universeFromType3+ , universeFromType2+ , universeFromType1+ , universeOfType)+where+import DDC.Type.Exp+import DDC.Type.Compounds+import qualified DDC.Type.Sum as T+++-- | Universes of the Disciple Core language.+data Universe + -- | (level 3). The universe of sorts.+ -- Sorts classify kinds.+ = UniverseSort++ -- | (level 2). The universe of kinds.+ -- Kinds classify specifications.+ | UniverseKind++ -- | (level 1). The universe of specifications.+ -- Specifications classify both witnesses and data values.+ -- In the vanilla Haskell world \"specifications\" are known as+ -- \"types\", but here we use the former term because we overload+ -- the word \"type\" to refer to kinds and sorts as well.+ | UniverseSpec++ -- | (level 0). The universe of witnesses.+ -- The existence of a witness in the program guarantees that some+ -- property about how it operates at runtime. For example, a witness+ -- of constancy of some region guarantees objects in that region will+ -- not be updated. This is like the @Prop@ universe in constructive+ -- logic.+ | UniverseWitness++ -- | (level 0). The universe of data values.+ -- These are physical data objects that take up space at runtime.+ -- This is like the @Set@ universe in constructive logic, but the + -- expressions may diverge or cause side effects.+ | UniverseData+ deriving (Show, Eq) +++-- | Given the type of the type of the type of some thing (up three levels),+-- yield the universe of the original thing, or `Nothing` it was badly formed.+universeFromType3 :: Type n -> Maybe Universe+universeFromType3 ss+ = case ss of+ TCon (TyConSort SoConProp) -> Just UniverseWitness+ TCon (TyConSort SoConComp) -> Just UniverseData+ _ -> Nothing+++-- | Given the type of the type of some thing (up two levels),+-- yield the universe of the original thing, or `Nothing` if it was badly formed.+universeFromType2 :: Type n -> Maybe Universe+universeFromType2 tt+ = case tt of+ TVar _ -> Nothing+ TCon (TyConSort _) -> Just UniverseSpec++ TCon (TyConKind kc) + -> case kc of+ KiConWitness -> Just UniverseWitness+ KiConData -> Just UniverseData+ _ -> Nothing++ TCon (TyConWitness _) -> Nothing+ TCon (TyConSpec _) -> Nothing+ TCon (TyConBound _) -> Nothing+ TForall _ _ -> Nothing+ TApp _ t2 -> universeFromType2 t2+ TSum _ -> Nothing+++-- | Given the type of some thing (up one level),+-- yield the universe of the original thing, or `Nothing` if it was badly formed.+universeFromType1 :: Type n -> Maybe Universe+universeFromType1 tt+ = case tt of+ TVar u -> universeFromType2 (typeOfBound u)+ TCon (TyConSort _) -> Just UniverseKind+ TCon (TyConKind _) -> Just UniverseSpec+ TCon (TyConWitness _) -> Just UniverseWitness+ TCon (TyConSpec TcConFun) -> Just UniverseData+ TCon (TyConSpec _) -> Nothing+ TCon (TyConBound u) -> universeFromType2 (typeOfBound u)+ TForall _ t2 -> universeFromType1 t2+ TApp _ t2 -> universeFromType1 t2+ TSum _ -> Nothing+++-- | Yield the universe of some type.+--+-- @ universeOfType (tBot kEffect) = UniverseSpec+-- universeOfType kRegion = UniverseKind+-- @+--+universeOfType :: Type n -> Maybe Universe+universeOfType tt+ = case tt of+ TVar u -> universeFromType1 (typeOfBound u)+ TCon (TyConSort _) -> Just UniverseSort+ TCon (TyConKind _) -> Just UniverseKind+ TCon (TyConWitness _) -> Just UniverseSpec+ TCon (TyConSpec _) -> Just UniverseSpec+ TCon (TyConBound u) -> universeFromType1 (typeOfBound u)+ TForall _ t2 -> universeOfType t2+ TApp _ t2 -> universeOfType t2+ TSum ss -> universeFromType1 (T.kindOfSum ss)++
+ LICENSE view
@@ -0,0 +1,20 @@+--------------------------------------------------------------------------------+The Disciplined Disciple Compiler License (MIT style)++Copyright (c) 2008-2011 Benjamin Lippmeier++Permission is hereby granted, free of charge, to any person obtaining a copy+of this software and associated documentation files (the "Software"), to deal+in the Software without restriction, including without limitation the rights+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell+copies of the Software, and to permit persons to whom the Software is+furnished to do so, subject to the following conditions:++The above copyright notice and this permission notice shall be included in+all copies or substantial portions of the Software.++--------------------------------------------------------------------------------+Redistributions of libraries in ./external are governed by their own licenses:++ - TinyPTC GNU Lesser General Public License+
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ ddc-core.cabal view
@@ -0,0 +1,100 @@+Name: ddc-core+Version: 0.2.0.1+License: MIT+License-file: LICENSE+Author: Ben Lippmeier+Maintainer: benl@ouroborus.net+Build-Type: Simple+Cabal-Version: >=1.6+Stability: experimental+Category: Compilers/Interpreters+Homepage: http://disciple.ouroborus.net+Bug-reports: disciple@ouroborus.net+Synopsis: Disciple 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 features 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 also 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.++ See the @ddci-core@ package for a user-facing interpreter.++Library+ Build-Depends: + base == 4.5.*,+ containers == 0.4.*,+ array == 0.4.*,+ transformers == 0.2.*,+ mtl == 2.0.*,+ ddc-base == 0.2.0.*++ Exposed-modules:+ DDC.Core.Check.CheckExp+ DDC.Core.Check.CheckWitness+ DDC.Core.Check.Error+ DDC.Core.Check.TaggedClosure+ DDC.Core.Parser.Lexer+ DDC.Core.Parser.Tokens+ DDC.Core.Transform.LiftW+ DDC.Core.Transform.LiftX+ DDC.Core.Transform.SpreadX+ DDC.Core.Transform.SubstituteTX+ DDC.Core.Transform.SubstituteWX+ DDC.Core.Transform.SubstituteXX+ DDC.Core.Check+ DDC.Core.Collect+ DDC.Core.Compounds+ DDC.Core.DataDef+ DDC.Core.Exp+ DDC.Core.Pretty+ DDC.Core.Predicates+ DDC.Core.Parser+ DDC.Type.Check.CheckCon+ DDC.Type.Check.CheckError+ DDC.Type.Check.Monad+ DDC.Type.Transform.Crush+ DDC.Type.Transform.Instantiate+ DDC.Type.Transform.LiftT+ DDC.Type.Transform.LowerT+ DDC.Type.Transform.SpreadT+ DDC.Type.Transform.SubstituteT+ DDC.Type.Transform.Trim+ DDC.Type.Check+ DDC.Type.Compounds+ DDC.Type.Env+ DDC.Type.Equiv+ DDC.Type.Exp+ DDC.Type.Parser+ DDC.Type.Predicates+ DDC.Type.Rewrite+ DDC.Type.Subsumes+ DDC.Type.Sum+ DDC.Type.Universe++ Other-modules:+ DDC.Core.Check.ErrorMessage+ DDC.Type.Pretty+ + GHC-options:+ -Wall+ -fno-warn-orphans+ -fno-warn-missing-signatures+ -fno-warn-unused-do-bind++ Extensions:+ ParallelListComp+ PatternGuards+ RankNTypes+ FlexibleContexts+ FlexibleInstances+ MultiParamTypeClasses+ UndecidableInstances+ KindSignatures+ NoMonomorphismRestriction+ ScopedTypeVariables+ StandaloneDeriving+ DoAndIfThenElse+