diff --git a/DDC/Core/Check.hs b/DDC/Core/Check.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Check.hs @@ -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 diff --git a/DDC/Core/Check/CheckExp.hs b/DDC/Core/Check/CheckExp.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Check/CheckExp.hs @@ -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) + diff --git a/DDC/Core/Check/CheckWitness.hs b/DDC/Core/Check/CheckWitness.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Check/CheckWitness.hs @@ -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 + diff --git a/DDC/Core/Check/Error.hs b/DDC/Core/Check/Error.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Check/Error.hs @@ -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) + diff --git a/DDC/Core/Check/ErrorMessage.hs b/DDC/Core/Check/ErrorMessage.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Check/ErrorMessage.hs @@ -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) ] + diff --git a/DDC/Core/Check/TaggedClosure.hs b/DDC/Core/Check/TaggedClosure.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Check/TaggedClosure.hs @@ -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 diff --git a/DDC/Core/Collect.hs b/DDC/Core/Collect.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Collect.hs @@ -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 + + diff --git a/DDC/Core/Compounds.hs b/DDC/Core/Compounds.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Compounds.hs @@ -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 + + + diff --git a/DDC/Core/DataDef.hs b/DDC/Core/DataDef.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/DataDef.hs @@ -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) + + diff --git a/DDC/Core/Exp.hs b/DDC/Core/Exp.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Exp.hs @@ -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) + diff --git a/DDC/Core/Parser.hs b/DDC/Core/Parser.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Parser.hs @@ -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 in EXP + , do pTok KPurify + pTok KAngleBra + w <- pWitness + pTok KAngleKet + pTok KIn + x <- pExp + return $ XCast () (CastPurify w) x + + + -- forget 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 + + -- + , 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 + [ 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 + -- + , 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 + diff --git a/DDC/Core/Parser/Lexer.hs b/DDC/Core/Parser/Lexer.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Parser/Lexer.hs @@ -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 + diff --git a/DDC/Core/Parser/Tokens.hs b/DDC/Core/Parser/Tokens.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Parser/Tokens.hs @@ -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 + diff --git a/DDC/Core/Predicates.hs b/DDC/Core/Predicates.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Predicates.hs @@ -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 + diff --git a/DDC/Core/Pretty.hs b/DDC/Core/Pretty.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Pretty.hs @@ -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 diff --git a/DDC/Core/Transform/LiftW.hs b/DDC/Core/Transform/LiftW.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Transform/LiftW.hs @@ -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 + + diff --git a/DDC/Core/Transform/LiftX.hs b/DDC/Core/Transform/LiftX.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Transform/LiftX.hs @@ -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 + + diff --git a/DDC/Core/Transform/SpreadX.hs b/DDC/Core/Transform/SpreadX.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Transform/SpreadX.hs @@ -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 + + diff --git a/DDC/Core/Transform/SubstituteTX.hs b/DDC/Core/Transform/SubstituteTX.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Transform/SubstituteTX.hs @@ -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 diff --git a/DDC/Core/Transform/SubstituteWX.hs b/DDC/Core/Transform/SubstituteWX.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Transform/SubstituteWX.hs @@ -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) + diff --git a/DDC/Core/Transform/SubstituteXX.hs b/DDC/Core/Transform/SubstituteXX.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Transform/SubstituteXX.hs @@ -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) + + diff --git a/DDC/Type/Check.hs b/DDC/Type/Check.hs new file mode 100644 --- /dev/null +++ b/DDC/Type/Check.hs @@ -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 + diff --git a/DDC/Type/Check/CheckCon.hs b/DDC/Type/Check/CheckCon.hs new file mode 100644 --- /dev/null +++ b/DDC/Type/Check/CheckCon.hs @@ -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 + + diff --git a/DDC/Type/Check/CheckError.hs b/DDC/Type/Check/CheckError.hs new file mode 100644 --- /dev/null +++ b/DDC/Type/Check/CheckError.hs @@ -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 ] + diff --git a/DDC/Type/Check/Monad.hs b/DDC/Type/Check/Monad.hs new file mode 100644 --- /dev/null +++ b/DDC/Type/Check/Monad.hs @@ -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 + diff --git a/DDC/Type/Compounds.hs b/DDC/Type/Compounds.hs new file mode 100644 --- /dev/null +++ b/DDC/Type/Compounds.hs @@ -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 + + diff --git a/DDC/Type/Env.hs b/DDC/Type/Env.hs new file mode 100644 --- /dev/null +++ b/DDC/Type/Env.hs @@ -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 + diff --git a/DDC/Type/Equiv.hs b/DDC/Type/Equiv.hs new file mode 100644 --- /dev/null +++ b/DDC/Type/Equiv.hs @@ -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 + diff --git a/DDC/Type/Exp.hs b/DDC/Type/Exp.hs new file mode 100644 --- /dev/null +++ b/DDC/Type/Exp.hs @@ -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) + diff --git a/DDC/Type/Parser.hs b/DDC/Type/Parser.hs new file mode 100644 --- /dev/null +++ b/DDC/Type/Parser.hs @@ -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 + diff --git a/DDC/Type/Predicates.hs b/DDC/Type/Predicates.hs new file mode 100644 --- /dev/null +++ b/DDC/Type/Predicates.hs @@ -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 + diff --git a/DDC/Type/Pretty.hs b/DDC/Type/Pretty.hs new file mode 100644 --- /dev/null +++ b/DDC/Type/Pretty.hs @@ -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" + + diff --git a/DDC/Type/Rewrite.hs b/DDC/Type/Rewrite.hs new file mode 100644 --- /dev/null +++ b/DDC/Type/Rewrite.hs @@ -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) diff --git a/DDC/Type/Subsumes.hs b/DDC/Type/Subsumes.hs new file mode 100644 --- /dev/null +++ b/DDC/Type/Subsumes.hs @@ -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 diff --git a/DDC/Type/Sum.hs b/DDC/Type/Sum.hs new file mode 100644 --- /dev/null +++ b/DDC/Type/Sum.hs @@ -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) + diff --git a/DDC/Type/Transform/Crush.hs b/DDC/Type/Transform/Crush.hs new file mode 100644 --- /dev/null +++ b/DDC/Type/Transform/Crush.hs @@ -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. +-} diff --git a/DDC/Type/Transform/Instantiate.hs b/DDC/Type/Transform/Instantiate.hs new file mode 100644 --- /dev/null +++ b/DDC/Type/Transform/Instantiate.hs @@ -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 + diff --git a/DDC/Type/Transform/LiftT.hs b/DDC/Type/Transform/LiftT.hs new file mode 100644 --- /dev/null +++ b/DDC/Type/Transform/LiftT.hs @@ -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 + diff --git a/DDC/Type/Transform/LowerT.hs b/DDC/Type/Transform/LowerT.hs new file mode 100644 --- /dev/null +++ b/DDC/Type/Transform/LowerT.hs @@ -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 + diff --git a/DDC/Type/Transform/SpreadT.hs b/DDC/Type/Transform/SpreadT.hs new file mode 100644 --- /dev/null +++ b/DDC/Type/Transform/SpreadT.hs @@ -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 + diff --git a/DDC/Type/Transform/SubstituteT.hs b/DDC/Type/Transform/SubstituteT.hs new file mode 100644 --- /dev/null +++ b/DDC/Type/Transform/SubstituteT.hs @@ -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 + diff --git a/DDC/Type/Transform/Trim.hs b/DDC/Type/Transform/Trim.hs new file mode 100644 --- /dev/null +++ b/DDC/Type/Transform/Trim.hs @@ -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. +-} + diff --git a/DDC/Type/Universe.hs b/DDC/Type/Universe.hs new file mode 100644 --- /dev/null +++ b/DDC/Type/Universe.hs @@ -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) + + diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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 + diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/ddc-core.cabal b/ddc-core.cabal new file mode 100644 --- /dev/null +++ b/ddc-core.cabal @@ -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 +