diff --git a/DDC/Core/Eval.hs b/DDC/Core/Eval.hs --- a/DDC/Core/Eval.hs +++ b/DDC/Core/Eval.hs @@ -6,10 +6,13 @@ -- evaluator will have an asymptotic complexity much worse than if they were -- compiled. This evaluator is intended for experimenting with the language -- semantics, and not running actual programs. +-- module DDC.Core.Eval - ( StepResult (..) + ( evalProfile + , StepResult (..) , force , step) where +import DDC.Core.Eval.Profile import DDC.Core.Eval.Step diff --git a/DDC/Core/Eval/Check.hs b/DDC/Core/Eval/Check.hs --- a/DDC/Core/Eval/Check.hs +++ b/DDC/Core/Eval/Check.hs @@ -1,25 +1,39 @@ +-- | Check for conflicting store capabilities in the initial program. module DDC.Core.Eval.Check - ( checkCapsX + ( checkCapsModule + , checkCapsX , Error(..)) where import DDC.Core.Eval.Compounds import DDC.Core.Eval.Name +import DDC.Core.Module import DDC.Core.Exp +import DDC.Core.Transform.Reannotate import DDC.Base.Pretty import Control.Monad import Data.Maybe -import DDC.Type.Check.Monad (throw, result) -import Data.Set (Set) -import qualified DDC.Type.Check.Monad as G -import qualified Data.Set as Set +import Data.Set (Set) +import DDC.Control.Monad.Check (evalCheck, throw) +import qualified DDC.Control.Monad.Check as G +import qualified Data.Set as Set -type CheckM a = G.CheckM Error --- | Check for conflicting store capabilities in the program. -checkCapsX :: Exp a Name -> Maybe Error +-- | Capability Checking monad. +type CheckM a x + = G.CheckM () (Error a) x + + +-- | Check for conflicting store capabilities in a module. +checkCapsModule :: Module a Name -> Maybe (Error a) +checkCapsModule mm + = checkCapsX $ moduleBody mm + + +-- | Check for conflicting store capabilities in an expression. +checkCapsX :: Exp a Name -> Maybe (Error a) checkCapsX xx - = case result $ checkCapsXM xx of + = case evalCheck () $ checkCapsXM xx of Left err -> Just err Right ws -> let caps = foldr mustInsertCap emptyCapSet ws @@ -27,15 +41,18 @@ -- CapSet -------------------------------------------------------------------- +-- | Set of used capabilities. data CapSet = CapSet { capsGlobal :: Set Rgn , capsConst :: Set Rgn , capsMutable :: Set Rgn + , capsDistinct :: Set [Rgn] , capsLazy :: Set Rgn , capsManifest :: Set Rgn } deriving Show + -- | An empty capability set emptyCapSet :: CapSet emptyCapSet @@ -43,15 +60,16 @@ { capsGlobal = Set.empty , capsConst = Set.empty , capsMutable = Set.empty + , capsDistinct = Set.empty , capsLazy = Set.empty , capsManifest = Set.empty } -- | Insert a capability, or `error` if this isn't one. -mustInsertCap :: Witness Name -> CapSet -> CapSet +mustInsertCap :: Witness a Name -> CapSet -> CapSet mustInsertCap ww caps - | WApp (WCon (WiConBound (UPrim nc _))) - (WType (TCon (TyConBound (UPrim nh _)))) <- ww + | WApp _ (WCon _ (WiConBound (UPrim nc _) _)) + (WType _ (TVar (UPrim nh _))) <- ww , NameCap c <- nc , NameRgn r <- nh = case c of @@ -60,13 +78,25 @@ CapMutable -> caps { capsMutable = Set.insert r (capsMutable caps) } CapLazy -> caps { capsLazy = Set.insert r (capsLazy caps) } CapManifest -> caps { capsManifest = Set.insert r (capsManifest caps)} - + _ -> error "mustInsertCap: invalid witness application" + + | Just (NameCap (CapDistinct _), ws) <- takePrimWiConApps ww + , ws' <- map takeNameRgn ws + , all isJust ws' + = caps { capsDistinct = Set.insert (catMaybes ws') (capsDistinct caps) } + | otherwise - = error "mustInsertCap: not a capability" + = error "ddc-core-eval.mustInsertCap: not a capability" +-- | Take a region name from a witness argument. +takeNameRgn :: Witness a Name -> Maybe Rgn +takeNameRgn (WType _ (TVar (UPrim (NameRgn r) _))) = Just r +takeNameRgn _ = Nothing + + -- | Check a capability set for conflicts between the capabilities. -checkCapSet :: CapSet -> Maybe Error +checkCapSet :: CapSet -> Maybe (Error a) checkCapSet cs | r : _ <- Set.toList $ Set.intersection (capsConst cs) (capsMutable cs) @@ -82,7 +112,7 @@ -- Error ---------------------------------------------------------------------- -- | Things that can go wrong with the capabilities in a program. -data Error +data Error a -- | Conflicting capabilities in program. = ErrorConflict { errorRegions :: Rgn @@ -95,17 +125,17 @@ -- appliction we need to ensure the constructors aren't partially -- applied. | ErrorPartial - { errorWitness :: Witness Name } + { errorWitness :: Witness () Name } -- | A capability constructor applied to a non-region handle. -- As with `ErrorPartial` we only need to check for this because we're -- using general witness application to represent capabilities, instead -- of having an atomic form. | ErrorNonHandle - { errorWitness :: Witness Name } + { errorWitness :: Witness () Name } -instance Pretty Error where +instance Pretty (Error a) where ppr err = case err of ErrorConflict r c1 c2 @@ -126,7 +156,7 @@ ------------------------------------------------------------------------------- -- | Collect the list of capabilities in an expression, -- and check that they are well-formed. -checkCapsXM :: Exp a Name -> CheckM a [Witness Name] +checkCapsXM :: Exp a Name -> CheckM a [Witness a Name] checkCapsXM xx = let none = return [] in case xx of @@ -140,65 +170,62 @@ (liftM concat $ mapM checkCapsAM alts) XCast _ cc x1 -> liftM2 (++) (checkCapsCM cc) (checkCapsXM x1) XType{} -> none - XWitness w -> checkCapsWM w + XWitness _ w -> checkCapsWM w -checkCapsCM :: Cast Name -> CheckM a [Witness Name] +checkCapsCM :: Cast a Name -> CheckM a [Witness a Name] checkCapsCM cc = let none = return [] in case cc of - CastWeakenEffect{} -> none - CastWeakenClosure{} -> none - CastPurify w -> checkCapsWM w - CastForget w -> checkCapsWM w + CastWeakenEffect{} + -> none + CastWeakenClosure xs + -> liftM concat $ mapM checkCapsXM xs -checkCapsLM :: Lets a Name -> CheckM a [Witness Name] + CastPurify w -> checkCapsWM w + CastForget w -> checkCapsWM w + CastBox -> none + CastRun -> none + + +checkCapsLM :: Lets a Name -> CheckM a [Witness a Name] checkCapsLM ll = let none = return [] in case ll of - LLet m _ x -> liftM2 (++) (checkCapsMM m) (checkCapsXM x) + LLet _ x -> checkCapsXM x LRec bxs -> liftM concat (mapM checkCapsXM $ map snd bxs) - LLetRegion{} -> none + LPrivate{} -> none LWithRegion{} -> none -checkCapsMM :: LetMode Name -> CheckM a [Witness Name] -checkCapsMM mm - = let none = return [] - in case mm of - LetStrict -> none - LetLazy (Just w) -> checkCapsWM w - LetLazy Nothing -> none - - -checkCapsAM :: Alt a Name -> CheckM a [Witness Name] +checkCapsAM :: Alt a Name -> CheckM a [Witness a Name] checkCapsAM aa = case aa of AAlt _ x -> checkCapsXM x -checkCapsWM :: Witness Name -> CheckM a [Witness Name] +checkCapsWM :: Witness a Name -> CheckM a [Witness a Name] checkCapsWM ww = let none = return [] in case ww of - WVar{} -> none + WVar{} -> none WCon{} - | isCapConW ww -> throw $ ErrorPartial ww - | otherwise -> none + | isCapConW ww -> throw $ ErrorPartial (reannotate (const ()) ww) + | otherwise -> none - WApp w1@WCon{} w2@(WType tR) + WApp _ w1@WCon{} w2@(WType _ tR) | isCapConW w1 -> if isJust $ takeHandleT tR then return [ww] - else throw $ ErrorNonHandle ww + else throw $ ErrorNonHandle (reannotate (const ()) ww) | otherwise -> liftM2 (++) (checkCapsWM w1) (checkCapsWM w2) - WApp w1 w2 -> liftM2 (++) (checkCapsWM w1) (checkCapsWM w2) - WJoin w1 w2 -> liftM2 (++) (checkCapsWM w1) (checkCapsWM w2) - WType{} -> none + WApp _ w1 w2 -> liftM2 (++) (checkCapsWM w1) (checkCapsWM w2) + WJoin _ w1 w2 -> liftM2 (++) (checkCapsWM w1) (checkCapsWM w2) + WType{} -> none diff --git a/DDC/Core/Eval/Compounds.hs b/DDC/Core/Eval/Compounds.hs --- a/DDC/Core/Eval/Compounds.hs +++ b/DDC/Core/Eval/Compounds.hs @@ -2,107 +2,116 @@ -- | Utilities for constructing and destructing compound types and -- expressions. module DDC.Core.Eval.Compounds - ( -- * Types - tUnit - , tInt + ( module DDC.Core.Compounds + + -- * Types , tPair , tList -- * Witnesses , wGlobal , wConst, wMutable + , wDistinct , wLazy, wManifest , wcGlobal , wcConst, wcMutable + , wcDistinct , wcLazy, wcManifest , isCapConW -- * Expressions + , takeMutableX + + -- * Units , isUnitX + + -- * Region Handles , takeHandleT , takeHandleX - , takeLocX, stripLocX - , takeMutableX) + + -- * Store Locations. + , xLoc, takeLocX, stripLocX + + -- * Integers + , tInt, tcInt + , dcInt + , takeIntDC, takeIntX) where import DDC.Core.Eval.Name import DDC.Type.Compounds +import DDC.Core.Compounds import DDC.Core.Exp -- Type ----------------------------------------------------------------------- --- | Application of the Unit type constructor. -tUnit :: Type Name -tUnit = TCon (TyConBound (UPrim (NamePrimCon PrimTyConUnit) kData)) - - --- | Application of the Int type constructor. -tInt :: Region Name -> Type Name -tInt r1 = TApp (TCon (TyConBound (UPrim (NamePrimCon PrimTyConInt) - (kFun kRegion kData)))) - r1 - -- | Application of the Pair type constructor. tPair :: Region Name -> Type Name -> Type Name -> Type Name tPair tR tA tB - = tApps (TCon (TyConBound (UPrim (NamePrimCon PrimTyConPair) - (kFuns [kRegion, kData, kData] kData)))) - [tR, tA, tB] + = tApps (TCon tcPair) [tR, tA, tB] + where tcPair = TyConBound (UPrim (NamePrimCon PrimTyConPair) kPair) kPair + kPair = kFuns [kRegion, kData, kData] kData -- | Application of the List type constructor. tList :: Region Name -> Type Name -> Type Name tList tR tA - = tApps (TCon (TyConBound (UPrim (NamePrimCon PrimTyConList) - (kRegion `kFun` kData `kFun` kData)))) - [tR, tA] + = tApps (TCon tcList) [tR, tA] + where tcList = TyConBound (UPrim (NamePrimCon PrimTyConList) kList) kList + kList = kRegion `kFun` kData `kFun` kData -- Witness -------------------------------------------------------------------- -wGlobal :: Region Name -> Witness Name -wGlobal r = WApp (WCon wcGlobal) (WType r) +wGlobal :: a -> Region Name -> Witness a Name +wGlobal a r = WApp a (WCon a wcGlobal) (WType a r) -wConst :: Region Name -> Witness Name -wConst r = WApp (WCon wcConst) (WType r) +wConst :: a -> Region Name -> Witness a Name +wConst a r = WApp a (WCon a wcConst) (WType a r) -wMutable :: Region Name -> Witness Name -wMutable r = WApp (WCon wcMutable) (WType r) +wMutable :: a -> Region Name -> Witness a Name +wMutable a r = WApp a (WCon a wcMutable) (WType a r) -wLazy :: Region Name -> Witness Name -wLazy r = WApp (WCon wcLazy) (WType r) +wLazy :: a -> Region Name -> Witness a Name +wLazy a r = WApp a (WCon a wcLazy) (WType a r) -wManifest :: Region Name -> Witness Name -wManifest r = WApp (WCon wcManifest) (WType r) +wManifest :: a -> Region Name -> Witness a Name +wManifest a r = WApp a (WCon a wcManifest) (WType a r) +wDistinct :: a -> Int -> [Region Name] -> Witness a Name +wDistinct a n rs + = wApps a (WCon a (wcDistinct n)) (map (WType a) rs) -- Just the Constructors wcGlobal :: WiCon Name -wcGlobal = WiConBound - $ UPrim (NameCap CapGlobal) (tForall kRegion $ \r -> tGlobal r) +wcGlobal = WiConBound (UPrim (NameCap CapGlobal) t) t + where t = tForall kRegion $ \r -> tGlobal r wcConst :: WiCon Name -wcConst = WiConBound - $ UPrim (NameCap CapConst) (tForall kRegion $ \r -> tConst r) +wcConst = WiConBound (UPrim (NameCap CapConst) t) t + where t = tForall kRegion $ \r -> tConst r wcMutable :: WiCon Name -wcMutable = WiConBound - $ UPrim (NameCap CapMutable) (tForall kRegion $ \r -> tMutable r) - +wcMutable = WiConBound (UPrim (NameCap CapMutable) t) t + where t = tForall kRegion $ \r -> tMutable r + wcLazy :: WiCon Name -wcLazy = WiConBound - $ UPrim (NameCap CapLazy) (tForall kRegion $ \r -> tLazy r) +wcLazy = WiConBound (UPrim (NameCap CapLazy) t) t + where t = tForall kRegion $ \r -> tLazy r wcManifest :: WiCon Name -wcManifest = WiConBound - $ UPrim (NameCap CapManifest) (tForall kRegion $ \r -> tManifest r) +wcManifest = WiConBound (UPrim (NameCap CapManifest) t) t + where t = tForall kRegion $ \r -> tManifest r +wcDistinct :: Int -> WiCon Name +wcDistinct n = WiConBound (UPrim (NameCap (CapDistinct n)) t) t + where t = tForalls (replicate n kRegion) $ \ts -> tDistinct n ts + -- | Check whether a witness is a capability constructor. -isCapConW :: Witness Name -> Bool +isCapConW :: Witness a Name -> Bool isCapConW ww = case ww of - WCon WiConBound{} -> True - _ -> False - + WCon _ WiConBound{} -> True + _ -> False -- Exp ------------------------------------------------------------------------ @@ -110,15 +119,19 @@ isUnitX :: Exp a Name -> Bool isUnitX xx = case xx of - XCon _ (UPrim (NamePrimCon PrimDaConUnit) _) -> True - _ -> False + XCon _ dc + -> case dc of + DaConUnit -> True + _ -> False + _ -> False +-- Handles -------------------------------------- -- | Take a region handle from a type. takeHandleT :: Type Name -> Maybe Rgn takeHandleT tt = case tt of - TCon (TyConBound (UPrim (NameRgn r1) _)) + TVar (UPrim (NameRgn r1) _) -> Just r1 _ -> Nothing @@ -127,44 +140,76 @@ takeHandleX :: Exp a Name -> Maybe Rgn takeHandleX xx = case xx of - XType t -> takeHandleT t - _ -> Nothing + XType _ t -> takeHandleT t + _ -> Nothing +-- Locations ------------------------------------ +-- | Make a location expression. +xLoc :: Loc -> Type Name -> Exp () Name +xLoc l t + = XVar () (UPrim (NameLoc l) t) + + -- | Take a store location from an expression. -- We strip off 'forget' casts along the way takeLocX :: Exp a Name -> Maybe Loc takeLocX xx = case xx of - XCast _ (CastForget _) x - -> takeLocX x - - XCon _ (UPrim (NameLoc l) _) - -> Just l - _ -> Nothing + XCast _ (CastForget _) x -> takeLocX x + XVar _ (UPrim (NameLoc l) _) -> Just l + _ -> Nothing -- | Take a store location from an expression, reaching under any 'forget' casts. stripLocX :: Exp a Name -> Maybe Loc stripLocX xx = case xx of - XCast _ (CastForget _) x - -> stripLocX x - - XCon _ (UPrim (NameLoc l) _) - -> Just l - - _ -> Nothing + XCast _ (CastForget _) x -> stripLocX x + XVar _ (UPrim (NameLoc l) _) -> Just l + _ -> Nothing +-- Witnesses ------------------------------------ -- | Take a witness of mutability from an expression. takeMutableX :: Exp a Name -> Maybe Rgn takeMutableX xx = case xx of - XWitness (WApp (WCon wc) (WType tR1)) - | WiConBound (UPrim (NameCap CapMutable) _) <- wc + XWitness _ (WApp _ (WCon _ wc) (WType _ tR1)) + | WiConBound (UPrim (NameCap CapMutable) _) _ <- wc -> takeHandleT tR1 _ -> Nothing +-- Integers ------------------------------------- +-- | Application of the Int type constructor. +tInt :: Region Name -> Type Name +tInt r1 + = TApp (TCon tcInt) r1 + +-- | The integer type constructor +tcInt :: TyCon Name +tcInt = TyConBound (UPrim (NamePrimCon PrimTyConInt) kInt) kInt + where kInt = kFun kRegion kData + + +-- | Make an integer data constructor. +dcInt :: Integer -> DaCon Name +dcInt i = DaConPrim (NameInt i) (TCon tcInt) + + +-- | Take an integer literal from an data constructor. +takeIntDC :: DaCon Name -> Maybe Integer +takeIntDC dc + = case takeNameOfDaCon dc of + Just (NameInt i) -> Just i + _ -> Nothing + + +-- | Take an integer literal from an expression. +takeIntX :: Exp a Name -> Maybe Integer +takeIntX xx + = case xx of + XCon _ dc -> takeIntDC dc + _ -> Nothing diff --git a/DDC/Core/Eval/Env.hs b/DDC/Core/Eval/Env.hs --- a/DDC/Core/Eval/Env.hs +++ b/DDC/Core/Eval/Env.hs @@ -19,9 +19,8 @@ where import DDC.Core.Eval.Compounds import DDC.Core.Eval.Name -import DDC.Core.DataDef +import DDC.Type.DataDef import DDC.Type.Exp -import DDC.Type.Compounds import DDC.Type.Env (Env) import qualified DDC.Type.Env as Env @@ -31,38 +30,33 @@ -- -- @ Type Constructors -- ---- ------------ --- Unit () -- Int 0 1 2 3 ... +-- Pair Pr -- List Nil Cons -- @ primDataDefs :: DataDefs Name primDataDefs = fromListDataDefs - -- Unit - [ DataDef - (NamePrimCon PrimTyConUnit) - [] - (Just [ (NamePrimCon PrimDaConUnit, []) ]) - - -- Int - , DataDef + [ -- Int + makeDataDefAlg (NamePrimCon PrimTyConInt) - [kRegion] + [BAnon kRegion] Nothing - -- Pair - , DataDef + -- Pair + , makeDataDefAlg (NamePrimCon PrimTyConPair) - [kRegion, kData, kData] + [BAnon kRegion, BAnon kData, BAnon kData] (Just [ ( NamePrimCon PrimDaConPr , [tIx kData 1, tIx kData 0]) ]) - -- List - , DataDef + -- List + , makeDataDefAlg (NamePrimCon PrimTyConList) - [kRegion, kData] + [BAnon kRegion, BAnon kData] (Just [ (NamePrimCon PrimDaConNil, []) - , (NamePrimCon PrimDaConCons, [tList (tIx kRegion 1) (tIx kData 0)])]) + , (NamePrimCon PrimDaConCons, + [tList (tIx kRegion 1) (tIx kData 0)])]) ] @@ -82,10 +76,6 @@ NameRgn _ -> Just $ kRegion - -- Unit - NamePrimCon PrimTyConUnit - -> Just $ kData - -- Int NamePrimCon PrimTyConInt -> Just $ kFun kRegion kData @@ -102,8 +92,6 @@ _ -> Nothing - - -- Types ---------------------------------------------------------------------- -- | Type environment containing types of primitive data constructors as well -- as the following primitive operators: @@ -125,45 +113,41 @@ typeOfPrimName :: Name -> Maybe (Type Name) typeOfPrimName nn = case nn of - -- Unit - NamePrimCon PrimDaConUnit - -> Just $ tUnit - -- Pair NamePrimCon PrimDaConPr -> Just $ tForalls [kRegion, kData, kData] $ \[tR, tA, tB] - -> tFun tA (tBot kEffect) + -> tFunEC tA (tBot kEffect) (tBot kClosure) - $ tFun tB (tSum kEffect [tAlloc tR]) + $ tFunEC tB (tSum kEffect [tAlloc tR]) (tSum kClosure [tDeepUse tA]) $ tPair tR tA tB -- List NamePrimCon PrimDaConNil -> Just $ tForalls [kRegion, kData] $ \[tR, tA] - -> tFun tUnit (tAlloc tR) - (tBot kClosure) + -> tFunEC tUnit (tAlloc tR) + (tBot kClosure) $ tList tR tA NamePrimCon PrimDaConCons -> Just $ tForalls [kRegion, kData] $ \[tR, tA] - -> tFun tA (tBot kEffect) + -> tFunEC tA (tBot kEffect) (tBot kClosure) - $ tFun (tList tR tA) (tSum kEffect [tAlloc tR]) + $ tFunEC (tList tR tA) (tSum kEffect [tAlloc tR]) (tSum kClosure [tDeepUse tA]) $ tList tR tA -- Int NameInt _ -> Just $ tForall kRegion - $ \r -> tFun tUnit (tAlloc r) + $ \r -> tFunEC tUnit (tAlloc r) (tBot kClosure) $ tInt r -- negInt NamePrimOp PrimOpNegInt -> Just $ tForalls [kRegion, kRegion] $ \[r1, r0] - -> tFun (tInt r1) (tSum kEffect [tRead r1, tAlloc r0]) + -> tFunEC (tInt r1) (tSum kEffect [tRead r1, tAlloc r0]) (tBot kClosure) $ (tInt r0) @@ -171,9 +155,9 @@ NamePrimOp p | elem p [PrimOpAddInt, PrimOpSubInt, PrimOpMulInt, PrimOpDivInt, PrimOpEqInt] -> Just $ tForalls [kRegion, kRegion, kRegion] $ \[r2, r1, r0] - -> tFun (tInt r2) (tBot kEffect) + -> tFunEC (tInt r2) (tBot kEffect) (tBot kClosure) - $ tFun (tInt r1) (tSum kEffect [tRead r2, tRead r1, tAlloc r0]) + $ tFunEC (tInt r1) (tSum kEffect [tRead r2, tRead r1, tAlloc r0]) (tSum kClosure [tUse r2]) $ tInt r0 @@ -181,32 +165,37 @@ NamePrimOp PrimOpUpdateInt -> Just $ tForalls [kRegion, kRegion] $ \[r1, r2] -> tImpl (tMutable r1) - $ tFun (tInt r1) (tBot kEffect) + $ tFunEC (tInt r1) (tBot kEffect) (tBot kClosure) - $ tFun (tInt r2) (tSum kEffect [tWrite r1, tRead r2]) + $ tFunEC (tInt r2) (tSum kEffect [tWrite r1, tRead r2]) (tSum kClosure [tUse r1]) $ tUnit -- copy :: [r1 r0 : %]. Int r1 -(Read r1 + Alloc r0 | $0)> Int r0 NamePrimOp PrimOpCopyInt -> Just $ tForalls [kRegion, kRegion] $ \[r1, r0] - -> tFun (tInt r1) (tSum kEffect [tRead r1, tAlloc r0]) + -> tFunEC (tInt r1) (tSum kEffect [tRead r1, tAlloc r0]) (tBot kClosure) $ (tInt r0) - NameCap CapGlobal -> Just $ tForall kRegion $ \r -> tGlobal r - NameCap CapConst -> Just $ tForall kRegion $ \r -> tConst r - NameCap CapMutable -> Just $ tForall kRegion $ \r -> tMutable r - NameCap CapLazy -> Just $ tForall kRegion $ \r -> tLazy r - NameCap CapManifest -> Just $ tForall kRegion $ \r -> tManifest r + NameCap CapGlobal -> Just $ tForall kRegion $ \r -> tGlobal r + NameCap CapConst -> Just $ tForall kRegion $ \r -> tConst r + NameCap CapMutable -> Just $ tForall kRegion $ \r -> tMutable r + NameCap CapLazy -> Just $ tForall kRegion $ \r -> tLazy r + NameCap CapManifest -> Just $ tForall kRegion $ \r -> tManifest r + NameCap (CapDistinct n) -> Just $ tForalls (replicate n kRegion) + $ \rs -> tDistinct n rs + NameLoc (Loc _ t) -> Just t + _ -> Nothing -- | Take the arity of a primitive name. --- --- TODO: determine this from the type. +-- We could take this from the type of the primitive instead, +-- but doing it this way is easy enough. arityOfName :: Name -> Maybe Int arityOfName n = case n of @@ -214,7 +203,6 @@ NameRgn{} -> Just 0 NameInt{} -> Just 2 - NamePrimCon PrimDaConUnit -> Just 0 NamePrimCon PrimDaConPr -> Just 5 NamePrimCon PrimDaConNil -> Just 3 NamePrimCon PrimDaConCons -> Just 4 diff --git a/DDC/Core/Eval/Name.hs b/DDC/Core/Eval/Name.hs --- a/DDC/Core/Eval/Name.hs +++ b/DDC/Core/Eval/Name.hs @@ -7,14 +7,18 @@ , Rgn (..) , Cap (..) , readName - , lexString) + , lexModuleString + , lexExpString) where +import DDC.Core.Lexer import DDC.Base.Pretty -import DDC.Base.Lexer -import DDC.Core.Parser.Lexer -import DDC.Core.Parser.Tokens +import DDC.Data.Token +import DDC.Type.Exp +import DDC.Type.Compounds +import Control.DeepSeq +import Data.Typeable import Data.Char -import Data.Maybe +import Data.List -- | Names of things recognised by the evaluator. @@ -33,10 +37,22 @@ | NameLoc Loc -- ^ Store locations. | NameRgn Rgn -- ^ Region handles. | NameCap Cap -- ^ Store capabilities. + deriving (Show, Eq, Ord, Typeable) - deriving (Show, Eq, Ord) - +instance NFData Name where + rnf nn + = case nn of + NameVar s -> rnf s + NameCon s -> rnf s + NameInt i -> rnf i + NamePrimCon pc -> rnf pc + NamePrimOp po -> rnf po + NameLoc l -> rnf l + NameRgn r -> rnf r + NameCap c -> rnf c + + instance Pretty Name where ppr nn = case nn of @@ -51,29 +67,43 @@ -- Locations ------------------------------------------------------------------ --- | A store location. +-- | A store location, +-- tagged with the type of the value contained at that location. -- --- These are pretty printed like @L4#@. +-- These are pretty printed like @l4#@. data Loc - = Loc Int - deriving (Eq, Ord, Show) + = Loc Int (Type Name) + deriving Show + +instance NFData Loc where + rnf (Loc i t) = rnf i `seq` rnf t + instance Pretty Loc where - ppr (Loc l) - = text "L" <> text (show l) <> text "#" - + ppr (Loc l _) = text "l" <> text (show l) <> text "#" +instance Eq Loc where + (==) (Loc l1 _) (Loc l2 _) + = l1 == l2 + +instance Ord Loc where + compare (Loc l1 _) (Loc l2 _) + = compare l1 l2 + + -- Regions -------------------------------------------------------------------- -- | A region handle. -- --- These are pretty printed like @R5#@. +-- These are pretty printed like @r5#@. data Rgn = Rgn Int deriving (Eq, Ord, Show) +instance NFData Rgn where + rnf (Rgn i) = rnf i + instance Pretty Rgn where - ppr (Rgn r) - = text "R" <> text (show r) <> text "#" + ppr (Rgn r) = text "r" <> text (show r) <> text "#" -- Capabilities -------------------------------------------------------------- @@ -87,36 +117,48 @@ -- deallocated in a stack like manner. This lets us hide the use of -- such regions, and rely on the garbage collector to reclaim the -- space. - = CapGlobal -- global :: [r: %]. Global r + = CapGlobal -- Global# :: [r: %]. Global r -- | Witness that a region is constant. -- This lets us purify read and allocation effects on it, -- and prevents it from being Mutable. - | CapConst -- const :: [r: %]. Const r + | CapConst -- Const# :: [r: %]. Const r -- | Witness that a region is mutable. -- This lets us update objects in the region, -- and prevents it from being Constant. - | CapMutable -- mutable :: [r: %]. Mutable r + | CapMutable -- Mutable# :: [r: %]. Mutable r + -- | Witness that some regions are distinct + -- This lets us perform aliasing based optimisations. + | CapDistinct Int -- Distinct2# :: [r1 r2 : %]. Distinct2 r1 r2 + -- | Witness that a region is lazy. -- This lets is allocate thunks into the region, -- and prevents it from being Manifest. - | CapLazy -- lazy :: [r: %].Lazy r + | CapLazy -- Lazy# :: [r: %].Lazy r -- | Witness that a region is manifest. -- This ensures there are no thunks in the region, -- which prevents it from being Lazy. - | CapManifest -- manifest :: [r: %]. Manifest r + | CapManifest -- Manifest# :: [r: %]. Manifest r deriving (Eq, Ord, Show) +instance NFData Cap where + rnf cap + = case cap of + CapDistinct i -> rnf i + _ -> () + + instance Pretty Cap where ppr cp = case cp of CapGlobal -> text "Global#" CapConst -> text "Const#" CapMutable -> text "Mutable#" + CapDistinct n -> text "Distinct" <> ppr n <> text "#" CapLazy -> text "Lazy#" CapManifest -> text "Manifest#" @@ -125,27 +167,25 @@ -- | A primitive constructor. data PrimCon -- Type constructors - = PrimTyConUnit -- ^ Unit type constructor (@Unit@). - | PrimTyConInt -- ^ @Int@ type constructor. + = PrimTyConInt -- ^ @Int@ type constructor. | PrimTyConPair -- ^ @Pair@ type constructor. | PrimTyConList -- ^ @List@ type constructor. -- Implement lists as primitives until we have data decls working - | PrimDaConUnit -- ^ Unit data constructor (@()@). | PrimDaConPr -- ^ @P@ data construct (pairs). | PrimDaConNil -- ^ @Nil@ data constructor. | PrimDaConCons -- ^ @Cons@ data constructor. deriving (Show, Eq, Ord) +instance NFData PrimCon + instance Pretty PrimCon where ppr con = case con of - PrimTyConUnit -> text "Unit" PrimTyConInt -> text "Int" PrimTyConPair -> text "Pair" PrimTyConList -> text "List" - PrimDaConUnit -> text "()" PrimDaConPr -> text "Pr" PrimDaConNil -> text "Nil" PrimDaConCons -> text "Cons" @@ -164,6 +204,7 @@ | PrimOpCopyInt deriving (Show, Eq, Ord) +instance NFData PrimOp instance Pretty PrimOp where ppr op @@ -183,7 +224,19 @@ readName :: String -> Maybe Name readName [] = Nothing readName str@(c:rest) - -- primops + -- region handles + | c == 'r' + , (ds, "#") <- span isDigit rest + , not $ null ds + = Just $ NameRgn (Rgn $ read ds) + + -- store locations + | c == 'l' + , (ds, "#") <- span isDigit rest + , not $ null ds + = Just $ NameLoc (Loc (read ds) (tBot kData)) + + -- primops and variables. | isLower c = case (c:rest) of "negInt" -> Just $ NamePrimOp PrimOpNegInt @@ -196,16 +249,16 @@ "copyInt" -> Just $ NamePrimOp PrimOpCopyInt _ -> Just $ NameVar str - -- units - | str == "Unit" = Just $ NamePrimCon PrimTyConUnit - | str == "()" = Just $ NamePrimCon PrimDaConUnit - -- integers | str == "Int" = Just $ NamePrimCon PrimTyConInt - | (ds, "") <- span isDigit str - = Just $ NameInt (read ds) + | c == '-' + , all isDigit rest + = Just $ NameInt (read str) + | all isDigit str + = Just $ NameInt (read str) + -- pairs | str == "Pair" = Just $ NamePrimCon PrimTyConPair | str == "Pr" = Just $ NamePrimCon PrimDaConPr @@ -214,25 +267,16 @@ | str == "List" = Just $ NamePrimCon PrimTyConList | str == "Nil" = Just $ NamePrimCon PrimDaConNil | str == "Cons" = Just $ NamePrimCon PrimDaConCons - - -- region handles - | c == 'R' - , (ds, "#") <- span isDigit rest - , not $ null ds - = Just $ NameRgn (Rgn $ read ds) - - -- store locations - | c == 'L' - , (ds, "#") <- span isDigit rest - , not $ null ds - = Just $ NameLoc (Loc $ read ds) - + -- store capabilities | str == "Global#" = Just $ NameCap CapGlobal | str == "Const#" = Just $ NameCap CapConst | str == "Mutable#" = Just $ NameCap CapMutable | str == "Lazy#" = Just $ NameCap CapLazy | str == "Manifest#" = Just $ NameCap CapManifest + | Just n <- stripPrefix "Distinct" str + , n' <- read $ takeWhile ('#' /=) n + = Just $ NameCap (CapDistinct n') -- other constructors | isUpper c @@ -241,17 +285,30 @@ | otherwise = Nothing -readName_ :: String -> Name -readName_ str - = fromMaybe (error $ "can't rename token " ++ str) - $ readName str +-- | Lex a string to tokens, using primitive names. +-- +-- The first argument gives the starting source line number. +-- +lexModuleString :: String -> Int -> String -> [Token (Tok Name)] +lexModuleString sourceName lineStart str + = map rn $ lexModuleWithOffside sourceName lineStart str + where rn (Token strTok sp) + = case renameTok readName strTok of + Just t' -> Token t' sp + Nothing -> Token (KJunk "lexical error") sp + -- | Lex a string to tokens, using primitive names. -- -- The first argument gives the starting source line number. -lexString :: Int -> String -> [Token (Tok Name)] -lexString lineStart str - = map rn $ lexExp lineStart str - where rn (Token t sp) = Token (renameTok readName_ t) sp +-- +lexExpString :: String -> Int -> String -> [Token (Tok Name)] +lexExpString sourceName lineStart str + = map rn $ lexExp sourceName lineStart str + where rn (Token strTok sp) + = case renameTok readName strTok of + Just t' -> Token t' sp + Nothing -> Token (KJunk "lexical error") sp + diff --git a/DDC/Core/Eval/Prim.hs b/DDC/Core/Eval/Prim.hs --- a/DDC/Core/Eval/Prim.hs +++ b/DDC/Core/Eval/Prim.hs @@ -12,88 +12,101 @@ import DDC.Core.Eval.Compounds import DDC.Core.Eval.Store import DDC.Core.Eval.Name -import DDC.Type.Compounds import DDC.Core.Exp import qualified DDC.Core.Eval.Store as Store + ------------------------------------------------------------------------------- -- | Step a primitive constructor, which allocates an object in the store. stepPrimCon - :: Name -- ^ Name of constructor to allocate. + :: DaCon Name -- ^ Data constructor to evaluate. -> [Exp () Name] -- ^ Arguments to constructor. -> Store -- ^ Current store. -> Maybe ( Store , Exp () Name) -- ^ New store and result expression, -- if the operator steps, otherwise `Nothing`. - -- Redirect the unit constructor. -- All unit values point to the same object in the store. -stepPrimCon (NamePrimCon PrimDaConUnit) [] store +stepPrimCon dc xsArgs store + | DaConUnit <- dc + , [] <- xsArgs = Just ( store - , XCon () (UPrim (NameLoc locUnit) tUnit) ) + , xLoc locUnit tUnit ) --- Alloction of Ints. -stepPrimCon (NameInt i) [xR, xUnit] store +stepPrimCon dc xsArgs store + + ------ Alloction of Ints ---------------------------------------- + | Just _ <- takeIntDC dc + , [xR, xUnit'] <- xsArgs + -- unpack the args - | XType tR <- xR + , XType _ tR <- xR , Just rgn <- takeHandleT tR - , isUnitOrLocX xUnit + , isUnitOrLocX xUnit' -- the store must contain the region we're going to allocate into. , Store.hasRgn store rgn -- add the binding to the store. - , (store1, l) <- Store.allocBind rgn (tInt tR) (SObj (NameInt i) []) store + , (store1, l) <- Store.allocBind rgn + (tInt tR) (SObj dc []) store = Just ( store1 - , XCon () (UPrim (NameLoc l) (tInt tR))) + , xLoc l (tInt tR)) --- Handle Pair specially until we have general data types. -stepPrimCon n@(NamePrimCon PrimDaConPr) [xR, xA, xB, x1, x2] store + ------ Handle Pair specially until we have general data types -- + | Just (NamePrimCon PrimDaConPr) <- takeNameOfDaCon dc + , [xR, xA, xB, x1, x2] <- xsArgs + -- unpack the args - | XType tR <- xR - , Just rgn <- takeHandleT tR - , XType tA <- xA - , XType tB <- xB - , Just l1 <- takeLocX x1 - , Just l2 <- takeLocX x2 + , XType _ tR <- xR + , Just rgn <- takeHandleT tR + , XType _ tA <- xA + , XType _ tB <- xB + , Just l1 <- takeLocX x1 + , Just l2 <- takeLocX x2 -- the store must contain the region we're going to allocate into. , Store.hasRgn store rgn -- add the binding to the store - , (store1, l) <- Store.allocBind rgn (tPair tR tA tB) (SObj n [l1, l2]) store + , (store1, l) <- Store.allocBind rgn + (tPair tR tA tB) (SObj dc [l1, l2]) store = Just ( store1 - , XCon () (UPrim (NameLoc l) (tPair tR tA tB))) + , xLoc l (tPair tR tA tB)) --- Handle Nil and Cons specially until we have general data types. -stepPrimCon n@(NamePrimCon PrimDaConNil) [xR, xA, xUnit] store + ---- Handle Nil and Cons specially until we have general data types. + | Just (NamePrimCon PrimDaConNil) <- takeNameOfDaCon dc + , [xR, xA, xUnit'] <- xsArgs + -- unpack the args - | XType tR <- xR - , Just rgn <- takeHandleT tR - , XType tA <- xA - , isUnitOrLocX xUnit + , XType _ tR <- xR + , Just rgn <- takeHandleT tR + , XType _ tA <- xA + , isUnitOrLocX xUnit' -- the store must contain the region we're going to allocate into. , Store.hasRgn store rgn -- add the binding to the store - , (store1, l) <- Store.allocBind rgn (tList tR tA) (SObj n []) store - + , (store1, l) <- Store.allocBind rgn + (tList tR tA) (SObj dc []) store = Just ( store1 - , XCon () (UPrim (NameLoc l) (tList tR tA))) + , xLoc l (tList tR tA)) -stepPrimCon n@(NamePrimCon PrimDaConCons) [xR, xA, xHead, xTail] store + | Just (NamePrimCon PrimDaConCons) <- takeNameOfDaCon dc + , [xR, xA, xHead, xTail] <- xsArgs + -- unpack the args - | XType tR <- xR + , XType _ tR <- xR , Just rgn <- takeHandleT tR - , XType tA <- xA + , XType _ tA <- xA , Just lHead <- takeLocX xHead , Just lTail <- takeLocX xTail @@ -101,10 +114,11 @@ , Store.hasRgn store rgn -- add the binding to the store - , (store1, l) <- Store.allocBind rgn (tList tR tA) (SObj n [lHead, lTail]) store + , (store1, l) <- Store.allocBind rgn + (tList tR tA) (SObj dc [lHead, lTail]) store = Just ( store1 - , XCon () (UPrim (NameLoc l) (tList tR tA))) + , xLoc l (tList tR tA)) stepPrimCon _ _ _ = Nothing @@ -131,14 +145,17 @@ , (PrimOpEqInt, (\x y -> if x == y then 1 else 0))] , Just r1 <- takeHandleX xR1 , Just r2 <- takeHandleX xR2 - , XType tR3 <- xR3 + , XType _ tR3 <- xR3 , Just r3 <- takeHandleX xR3 , Just l1 <- stripLocX xL1 , Just l2 <- stripLocX xL2 -- get the regions and values of each location - , Just (r1', _, SObj (NameInt i1) []) <- Store.lookupRegionTypeBind l1 store - , Just (r2', _, SObj (NameInt i2) []) <- Store.lookupRegionTypeBind l2 store + , Just (r1', _, SObj dc1 []) <- Store.lookupRegionTypeBind l1 store + , Just i1 <- takeIntDC dc1 + + , Just (r2', _, SObj dc2 []) <- Store.lookupRegionTypeBind l2 store + , Just i2 <- takeIntDC dc2 -- the locations must be in the regions the args said they were in , r1' == r1 @@ -151,10 +168,12 @@ , i3 <- i1 `fOp` i2 -- write the result to a new location in the store - , (store1, l3) <- Store.allocBind r3 (tInt tR3) (SObj (NameInt i3) []) store + , (store1, l3) <- Store.allocBind r3 (tInt tR3) + (SObj (dcInt i3) []) + store = Just ( store1 - , XCon () (UPrim (NameLoc l3) (tInt tR3))) + , xLoc l3 (tInt tR3)) -- Update integer primop. @@ -170,18 +189,20 @@ , r1W == r1 -- get the regions and values of each location - , Just (r1L, tX1, SObj (NameInt _) []) <- Store.lookupRegionTypeBind l1 store - , Just (r2L, _, SObj (NameInt i2) []) <- Store.lookupRegionTypeBind l2 store + , Just (r1L, tX1, SObj dc1 []) <- Store.lookupRegionTypeBind l1 store + , Just _i1 <- takeIntDC dc1 + , Just (r2L, _, SObj dc2 []) <- Store.lookupRegionTypeBind l2 store + , Just i2 <- takeIntDC dc2 + -- the locations must be in the regions the args said they were in , r1L == r1 , r2L == r2 -- update the destination - , store1 <- Store.addBind l1 r1 tX1 (SObj (NameInt i2) []) store - + , store1 <- Store.addBind l1 r1 tX1 (SObj (dcInt i2) []) store = Just ( store1 - , XCon () (UPrim (NamePrimCon PrimDaConUnit) tUnit)) + , xUnit ()) -- Unary integer operations stepPrimOp (NamePrimOp op) [xR1, xR2, xL1] store @@ -190,12 +211,13 @@ [ (PrimOpCopyInt, id) , (PrimOpNegInt, negate) ] , Just r1 <- takeHandleX xR1 - , XType tR2 <- xR2 + , XType _ tR2 <- xR2 , Just r2 <- takeHandleX xR2 , Just l1 <- stripLocX xL1 -- get the region and value of the int - , Just (r1L, _, SObj (NameInt i1) []) <- Store.lookupRegionTypeBind l1 store + , Just (r1L, _, SObj dc1 []) <- Store.lookupRegionTypeBind l1 store + , Just i1 <- takeIntDC dc1 -- the locations must be in the regions the args said they were in , r1L == r1 @@ -204,13 +226,13 @@ , Store.hasRgn store r2 -- calculate - , i2 <- fOp i1 + , i2 <- fOp i1 -- write the result to a new location in the store - , (store1, l2) <- Store.allocBind r2 (tInt tR2) (SObj (NameInt i2) []) store + , (store1, l2) <- Store.allocBind r2 (tInt tR2) (SObj (dcInt i2) []) store = Just ( store1 - , XCon () (UPrim (NameLoc l2) (tInt tR2))) + , xLoc l2 (tInt tR2)) stepPrimOp _ _ _ = Nothing diff --git a/DDC/Core/Eval/Profile.hs b/DDC/Core/Eval/Profile.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Eval/Profile.hs @@ -0,0 +1,43 @@ + +-- | Core language profile for the evaluator. +module DDC.Core.Eval.Profile + (evalProfile) +where +import DDC.Core.Fragment +import DDC.Core.Eval.Env +import DDC.Core.Eval.Name + + +-- | Core language fragment that can be directly evaluated. +evalProfile :: Profile Name +evalProfile + = Profile + { profileName = "Eval" + , profileFeatures = evalFeatures + , profilePrimDataDefs = primDataDefs + , profilePrimKinds = primKindEnv + , profilePrimTypes = primTypeEnv + , profileTypeIsUnboxed = const False + , profileNameIsHole = Nothing } + + +-- | Language features used by the eval fragment. +evalFeatures :: Features +evalFeatures + = Features + { featuresTrackedEffects = True + , featuresTrackedClosures = True + , featuresFunctionalEffects = True + , featuresFunctionalClosures = True + , featuresEffectCapabilities = False + , featuresPartialPrims = False + , featuresPartialApplication = True + , featuresGeneralApplication = True + , featuresNestedFunctions = True + , featuresDebruijnBinders = True + , featuresUnboundLevel0Vars = False + , featuresUnboxedInstantiation = True + , featuresNameShadowing = True + , featuresUnusedBindings = True + , featuresUnusedMatches = True } + diff --git a/DDC/Core/Eval/Step.hs b/DDC/Core/Eval/Step.hs --- a/DDC/Core/Eval/Step.hs +++ b/DDC/Core/Eval/Step.hs @@ -7,6 +7,7 @@ , isValue , isWeakValue) where +import DDC.Core.Eval.Profile import DDC.Core.Eval.Store import DDC.Core.Eval.Name import DDC.Core.Eval.Prim @@ -16,10 +17,9 @@ import DDC.Core.Transform.SubstituteXX import DDC.Core.Transform.SubstituteTX import DDC.Core.Check -import DDC.Core.Compounds import DDC.Core.Predicates import DDC.Core.Exp -import DDC.Type.Compounds +import qualified DDC.Core.Fragment as C import qualified Data.Set as Set @@ -40,7 +40,7 @@ | StepStuck -- | Expression is stuck, and we know for sure it's mistyped. - | StepStuckMistyped (Error () Name) + | StepMistyped (Error () Name) deriving (Show) @@ -56,7 +56,7 @@ force store xx | (casts, xx') <- unwrapCasts xx - , XCon _ (UPrim (NameLoc l) _) <- xx' + , XVar _ (UPrim (NameLoc l) _) <- xx' , Just (rgn, t, SThunk x) <- lookupRegionTypeBind l store = case force store x of StepProgress store' x' @@ -90,40 +90,38 @@ step store xx | (casts, xp) <- unwrapCasts xx , isLambdaX xp - = case typeOfExp primDataDefs xp of - Left err -> StepStuckMistyped err + = case typeOfExp + (configOfProfile evalProfile) + (C.profilePrimKinds evalProfile) + (C.profilePrimTypes evalProfile) + xp + of Left err -> StepMistyped err Right t - -> let Just (bs, xBody) = takeXLamFlags xp - (store', l) = allocBind (Rgn 0) t (SLams bs xBody) store - in StepProgress store' (wrapCasts casts $ XCon () (UPrim (NameLoc l) t)) + -> let Just (bs, xBody) = takeXLamFlags xp + (store', l) = allocBind (Rgn 0) t (SLams bs xBody) store + x' = xLoc l t + in StepProgress store' (wrapCasts casts x') -- (EvAlloc) -- Construct some data in the heap. step store xx - | Just (u, xs) <- takeXConApps xx - , case u of - -- Unit constructors are not allocated into the store. - UPrim NamePrimCon{} _ -> True - UPrim NameInt{} _ -> True - UPrim NameCon{} _ -> True - _ -> False - - , UPrim n _ <- u - , Just arity <- arityOfName n - , length xs == arity + | Just (dc, xs) <- takeXConApps xx , and $ map (isWeakValue store) xs - , Just (store', x') <- stepPrimCon n xs store + , Just (store', x') <- stepPrimCon dc xs store = StepProgress store' x' -- (EvPrim) -- Step a primitive operator or constructor defined by the client. step store xx - | x1@(XVar _ (UPrim p _)) : xs <- takeXApps xx - , Just arity <- arityOfName p + | Just (x1@(XVar _ (UPrim p _)), xs) <- takeXApps xx + , Nothing <- takeLocX x1 + , Just arity <- arityOfName p = let - -- TODO: we're not allowing over-applied primops + -- ISSUE #296: Evaluator doesn't support over-applied primops. + -- This would be a problem if we read a reference to a function + -- and then apply it directly. stepArg i _acc [] | i == arity , Just (store', x') <- stepPrimOp p xs store @@ -136,7 +134,8 @@ stepArg i acc (ax:axs) = case force store ax of StepProgress store' x' - -> Right (store', makeXApps () x1 (reverse acc ++ (x' : axs))) + -> Right ( store' + , xApps () x1 (reverse acc ++ (x' : axs))) StepDone -> case stepArg (i + 1) (ax : acc) axs of @@ -153,8 +152,8 @@ -- (EvAppArgs) -- Step the left-most non-wnf argument of a lambda. step store xx - | x1 : xsArgs <- takeXApps xx - , Just l1 <- takeLocX x1 + | Just (x1, xsArgs) <- takeXApps xx + , Just l1 <- takeLocX x1 , Just (Rgn 0, _, SLams bs _xBody) <- lookupRegionTypeBind l1 store -- See if an arg to any of the lambdas needs to be stepped. @@ -166,7 +165,7 @@ -- This should never error, as we took as many args -- as we had wnf flags. stepArg _ [] - = error "stepArg: no more args" + = error "ddc-core-eval.stepArg: no more args" stepArg [] xs = Right (store, xs) @@ -184,15 +183,15 @@ in case stepArg wnfs xsArgs of Left err -> err Right (store2, xsArgs') - -> StepProgress store2 (makeXApps () x1 xsArgs') + -> StepProgress store2 (xApps () x1 xsArgs') -- (EvAppSubst) -- Substitute wnf arguments into an abstraction. step store xx - | x1 : xsArgs <- takeXApps xx - , (casts, xL1) <- unwrapCasts x1 - , Just l1 <- takeLocX xL1 + | Just (x1, xsArgs) <- takeXApps xx + , (casts, xL1) <- unwrapCasts x1 + , Just l1 <- takeLocX xL1 , Just (Rgn 0, _, SLams fbs xBody) <- lookupRegionTypeBind l1 store @@ -215,7 +214,7 @@ $ makeXLamFlags () bsLeftover xBody in StepProgress store - $ wrapCasts casts (makeXApps () xResult argsLeftover) + $ wrapCasts casts (xApps () xResult argsLeftover) -- (EvApp1 / EvApp2) @@ -236,12 +235,12 @@ err -> err --- (EvLetStrictStep / EvLetStrictSubst) +-- (EvLetStep / EvLetSubst) -- Substitute in a bound value in a let expression. -step store (XLet a (LLet LetStrict b x1) x2) +step store (XLet a (LLet b x1) x2) = case step store x1 of StepProgress store' x1' - -> StepProgress store' (XLet a (LLet LetStrict b x1') x2) + -> StepProgress store' (XLet a (LLet b x1') x2) StepDone -> StepProgress store (substituteXX b x1 x2) @@ -249,19 +248,6 @@ err -> err --- (EvLetLazyAlloc) --- Allocate a lazy binding in the heap. -step store (XLet _ (LLet (LetLazy _w) b x1) x2) - -- We need the type of the expression to attach to the location - -- This fakes the store typing from the formal typing rules. - = case typeOfExp primDataDefs x1 of - Left err -> StepStuckMistyped err - Right t1 - -> let (store1, l) = allocBind (Rgn 0) t1 (SThunk x1) store - x1' = XCon () (UPrim (NameLoc l) t1) - in StepProgress store1 (substituteXX b x1' x2) - - -- (EvLetRec) -- Add recursive bindings to the store. step store (XLet _ (LRec bxs) x2) @@ -269,13 +255,12 @@ ts = map typeOfBind bs -- Allocate new locations in the store to hold the expressions. - (store1, ls) = newLocs (length bs) store - xls = [XCon () (UPrim (NameLoc l) t) | (l, t) <- zip ls ts] + (store1, ls) = newLocs (map (typeOfBind . fst) bxs) store + xls = [xLoc l t | (l, t) <- zip ls ts] -- Substitute locations into all the bindings. xs' = map (substituteXXs (zip bs xls)) xs - -- Create store objects for each of the bindings. mos = map (\x -> case takeXLamFlags x of Just (fbs', xBody) -> Just $ SLams fbs' xBody @@ -299,26 +284,31 @@ -- (EvCreateRegion) -- Create a new region. -step store (XLet a (LLetRegion bRegion bws) x) - | Just uRegion <- takeSubstBoundOfBind bRegion +step store (XLet a (LPrivate bRegions _mt bws) x) + | uRegions <- takeSubstBoundsOfBinds bRegions -- Allocate a new region handle for the bound region. , (store1, uHandle@(UPrim (NameRgn rgn) _)) <- primNewRegion store - , tHandle <- TCon $ TyConBound uHandle + , tHandle <- TVar uHandle -- Substitute handle into the witness types. - , bws' <- map (substituteBoundTX uRegion tHandle) bws + , bws' <- concatMap + (\uRegion -> map (substituteBoundTX uRegion tHandle) bws) + uRegions -- Build witnesses for each of the witness types. -- This can fail if the set of witness signatures is malformed. , Just wits <- sequence - $ map regionWitnessOfType + $ map (regionWitnessOfType ()) $ map typeOfBind bws' = let -- Substitute handle and witnesses into body. - x' = substituteBoundTX uRegion tHandle - $ substituteWXs (zip bws' wits) x + substituteBoundTX' xx u + = substituteBoundTX u tHandle xx + + x' = substituteWXs (zip bws' wits) x + x'' = foldl substituteBoundTX' x' uRegions isGlobalBind b = case typeOfBind b of @@ -331,7 +321,7 @@ then setGlobal rgn store1 else store1 - in StepProgress store2 (XLet a (LWithRegion uHandle) x') + in StepProgress store2 (XLet a (LWithRegion uHandle) x'') -- Region binder was a wildcard, so we can't create the region handle. -- No witness sigs can be in the set, because any sig would need @@ -373,7 +363,8 @@ StepDone | (casts, xDiscrim') <- unwrapCasts xDiscrim , Just lDiscrim <- takeLocX xDiscrim' - , Just (SObj nTag lsArgs) <- lookupBind lDiscrim store + , Just (SObj dc lsArgs) <- lookupBind lDiscrim store + , Just nTag <- takeNameOfDaCon dc , Just tsArgs <- sequence $ map (\l -> lookupTypeOfLoc l store) lsArgs , AAlt pat xBody : _ <- filter (tagMatchesAlt nTag) alts -> case pat of @@ -381,7 +372,7 @@ -> StepProgress store xBody PData _ bsArgs - | bxsArgs <- [ (b, wrapCasts casts (XCon a (UPrim (NameLoc l) t))) + | bxsArgs <- [ (b, wrapCasts casts (xLoc l t)) | l <- lsArgs | t <- tsArgs | b <- bsArgs] @@ -407,6 +398,17 @@ = case step store x of StepProgress store' x' -> StepProgress store' (XCast a cc x') + + -- Strip out any weakens, so we can evaluate further. + -- XXX this should probably be elsewhere + StepDone + -> case cc of + CastWeakenEffect _ + -> StepProgress store x + CastWeakenClosure _ + -> StepProgress store x + _ -> StepDone + err -> err @@ -419,7 +421,7 @@ -- Casts ---------------------------------------------------------------------- -- Unwrap casts from the front of an expression. -unwrapCasts :: Exp () n -> ([Cast n], Exp () n) +unwrapCasts :: Exp () n -> ([Cast () n], Exp () n) unwrapCasts xx = case xx of XCast _ c x @@ -430,7 +432,7 @@ -- Wrap casts around an expression. -wrapCasts :: [Cast n] -> Exp () n -> Exp () n +wrapCasts :: [Cast () n] -> Exp () n -> Exp () n wrapCasts cc xx = case cc of [] -> xx @@ -447,8 +449,8 @@ -- | See if a constructor tag matches a pattern. tagMatchesPat :: Name -> Pat Name -> Bool tagMatchesPat _ PDefault = True -tagMatchesPat n (PData u' _) - = case takeNameOfBound u' of +tagMatchesPat n (PData dc _) + = case takeNameOfDaCon dc of Just n' -> n == n' _ -> False @@ -465,6 +467,7 @@ -- These are all the values, and locations that point to thunks. -- -- Weak values can be progressed with `force`, but not `step`. +-- isWeakValue :: Store -> Exp a Name -> Bool isWeakValue store xx = isSomeValue True store xx @@ -475,11 +478,11 @@ isSomeValue :: Bool -> Store -> Exp a Name -> Bool isSomeValue weak store xx = case xx of - XVar{} -> True + XVar _ (UPrim (NameLoc l) _) + | Just SThunk{} <- lookupBind l store -> weak + | otherwise -> True - XCon _ (UPrim (NameLoc l) _) - | Just SThunk{} <- lookupBind l store - -> weak + XVar{} -> True XCon{} -> True @@ -503,23 +506,22 @@ XApp _ x1 x2 -- Application if a primop to enough args is not wnf. - | Just (n, xs) <- takeXPrimApps xx + | Just (n, xs) <- takeXPrimApps xx , and $ map (isSomeValue weak store) xs - , Just a <- arityOfName n + , Just a <- arityOfName n , length xs >= a -> False -- Application of a lambda in the store is not wnf. - | Just (u, _xs) <- takeXConApps xx - , UPrim (NameLoc l) _ <- u - , Just SLams{} <- lookupBind l store + | Just (NameLoc l, _xs) <- takeXPrimApps xx + , Just SLams{} <- lookupBind l store -> False -- Application of a data constructor to enough args is not wnf. - | Just (u, xs) <- takeXConApps xx + | Just (dc, xs) <- takeXConApps xx , and $ map (isSomeValue weak store) xs - , UPrim n _ <- u - , Just a <- arityOfName n + , Just n <- takeNameOfDaCon dc + , Just a <- arityOfName n , length xs >= a -> False @@ -532,13 +534,14 @@ -- | Get the region witness corresponding to one of the witness types that are -- permitted in a letregion. -regionWitnessOfType :: Type Name -> Maybe (Witness Name) -regionWitnessOfType tt - = case tt of - TApp (TCon (TyConWitness TwConGlobal)) r -> Just $ wGlobal r - TApp (TCon (TyConWitness TwConMutable)) r -> Just $ wMutable r - TApp (TCon (TyConWitness TwConConst)) r -> Just $ wConst r - TApp (TCon (TyConWitness TwConLazy)) r -> Just $ wLazy r - TApp (TCon (TyConWitness TwConManifest)) r -> Just $ wManifest r +regionWitnessOfType :: a -> Type Name -> Maybe (Witness a Name) +regionWitnessOfType a tt + = case takeTyConApps tt of + Just (TyConWitness TwConGlobal , [r]) -> Just $ wGlobal a r + Just (TyConWitness TwConMutable , [r]) -> Just $ wMutable a r + Just (TyConWitness TwConConst , [r]) -> Just $ wConst a r + Just (TyConWitness TwConLazy , [r]) -> Just $ wLazy a r + Just (TyConWitness TwConManifest , [r]) -> Just $ wManifest a r + Just (TyConWitness (TwConDistinct n), rs) -> Just $ wDistinct a n rs _ -> Nothing diff --git a/DDC/Core/Eval/Store.hs b/DDC/Core/Eval/Store.hs --- a/DDC/Core/Eval/Store.hs +++ b/DDC/Core/Eval/Store.hs @@ -64,7 +64,7 @@ data SBind -- | An algebraic data constructor. = SObj - { sbindDataTag :: Name + { sbindDataTag :: DaCon Name , sbindDataArgs :: [Loc] } -- | Lambda abstraction, used for recursive bindings. @@ -87,10 +87,10 @@ , text " NextLoc: " <> text (show nextLoc) , text " NextRgn: " <> text (show nextRgn) - , text " Regions: " <> braces (sep $ punctuate comma + , text " Regions: " <> braces (sep $ punctuate comma $ map ppr $ Set.toList regions) - , text " Global: " <> braces (sep $ punctuate comma + , text " Global: " <> braces (sep $ punctuate comma $ map ppr $ Set.toList global) , text "" , text " Binds:" @@ -132,42 +132,43 @@ , storeBinds = Map.fromList - [ (Loc 0, (Rgn 0, tUnit, SObj (NamePrimCon PrimDaConUnit) []))] + [ (Loc 0 tUnit, (Rgn 0, tUnit, SObj dcUnit []))] } -- | Location of the static unit object. locUnit :: Loc -locUnit = Loc 0 +locUnit = Loc 0 tUnit -- | Check whether an expression is the unit constructor, -- or its static heap location. -isUnitOrLocX :: Exp a Name -> Bool +isUnitOrLocX :: Show a => Exp a Name -> Bool isUnitOrLocX xx = case xx of - XCon _ (UPrim (NamePrimCon PrimDaConUnit) _) -> True - XCon _ (UPrim (NameLoc l) _) -> l == locUnit - _ -> False + XCon _ DaConUnit -> True + XVar _ (UPrim (NameLoc (Loc 0 _)) _) -> True + _ -> False -- Locations ------------------------------------------------------------------ -- | Create a new location in the store. -newLoc :: Store -> (Store, Loc) -newLoc store +newLoc :: Type Name -> Store -> (Store, Loc) +newLoc t store = let loc = storeNextLoc store store' = store { storeNextLoc = loc + 1 } - in (store', Loc loc) + in (store', Loc loc t) -- | Create several new locations in the store. -newLocs :: Int -> Store -> (Store, [Loc]) -newLocs n store - = let lFirst = storeNextLoc store +newLocs :: [Type Name] -> Store -> (Store, [Loc]) +newLocs ts store + = let n = length ts + lFirst = storeNextLoc store lLast = lFirst + n locs = [lFirst .. lLast] store' = store { storeNextLoc = lLast + 1 } - in (store', map Loc locs) + in (store', [Loc l t | l <- locs | t <- ts]) -- Regions ------------------------------------------------------------------- @@ -225,17 +226,16 @@ -- returning the new location. allocBind :: Rgn -> Type Name -> SBind -> Store -> (Store, Loc) allocBind rgn t sbind store - = let (store1, loc) = newLoc store + = let (store1, loc) = newLoc t store store2 = addBind loc rgn t sbind store1 in (store2, loc) -- | Alloc some recursive bindings into the given region, -- returning the new locations. -allocBinds :: ([[Loc] -> (Rgn, Type Name, SBind)]) -> Store -> (Store, [Loc]) -allocBinds mkSBinds store - = let n = length mkSBinds - (store1, locs) = newLocs n store +allocBinds :: [[Loc] -> (Rgn, Type Name, SBind)] -> [Type Name] -> Store -> (Store, [Loc]) +allocBinds mkSBinds ts store + = let (store1, locs) = newLocs ts store rgnBinds = map (\mk -> mk locs) mkSBinds store2 = foldr (\(l, (r, t, b)) -> addBind l r t b) store1 $ zip locs rgnBinds @@ -255,6 +255,7 @@ = case Map.lookup loc (storeBinds store) of Nothing -> Nothing Just (_, t, _) -> Just t + -- | Lookup the region handle, type and binding for a location. lookupRegionTypeBind :: Loc -> Store -> Maybe (Rgn, Type Name, SBind) diff --git a/LICENSE b/LICENSE --- a/LICENSE +++ b/LICENSE @@ -1,7 +1,7 @@ -------------------------------------------------------------------------------- The Disciplined Disciple Compiler License (MIT style) -Copyrite (K) 2007-2012 The Disciplined Disciple Compiler Strike Force +Copyrite (K) 2007-2014 The Disciplined Disciple Compiler Strike Force All rights reversed. Permission is hereby granted, free of charge, to any person obtaining a copy @@ -13,18 +13,4 @@ The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software. - -------------------------------------------------------------------------------- -Under Australian law copyright is free and automatic. -By contributing to DDC authors grant all rights they have regarding their -contributions to the other members of the Disciplined Disciple Compiler Strike -Force, past, present and future, as well as placing their contributions under -the above license. - -Use "darcs show authors" to get a list of Strike Force members. - -------------------------------------------------------------------------------- -Redistributions of libraries in ./external are governed by their own licenses: - - - TinyPTC GNU Lesser General Public License - diff --git a/ddc-core-eval.cabal b/ddc-core-eval.cabal --- a/ddc-core-eval.cabal +++ b/ddc-core-eval.cabal @@ -1,5 +1,5 @@ Name: ddc-core-eval -Version: 0.2.1.2 +Version: 0.4.1.3 License: MIT License-file: LICENSE Author: The Disciplined Disciple Compiler Strike Force @@ -9,8 +9,7 @@ Stability: experimental Category: Compilers/Interpreters Homepage: http://disciple.ouroborus.net -Bug-reports: disciple@ouroborus.net -Synopsis: Disciple Core language semantic evaluator. +Synopsis: Disciplined Disciple Compiler semantic evaluator for the core language. Description: This is a direct implementation of the operational semantics and is by no means fast, or a substitute for a real interpreter. Programs run with this @@ -20,13 +19,14 @@ Library Build-Depends: - base == 4.6.*, + base >= 4.6 && < 4.8, + array >= 0.4 && < 0.6, + deepseq == 1.3.*, containers == 0.5.*, - array == 0.4.*, - transformers == 0.3.*, - mtl == 2.1.*, - ddc-base == 0.2.1.*, - ddc-core == 0.2.1.* + transformers == 0.4.*, + mtl == 2.2.*, + ddc-base == 0.4.1.*, + ddc-core == 0.4.1.* Exposed-modules: DDC.Core.Eval.Check @@ -34,6 +34,7 @@ DDC.Core.Eval.Env DDC.Core.Eval.Name DDC.Core.Eval.Prim + DDC.Core.Eval.Profile DDC.Core.Eval.Step DDC.Core.Eval.Store DDC.Core.Eval @@ -42,6 +43,7 @@ -Wall -fno-warn-orphans -fno-warn-missing-signatures + -fno-warn-missing-methods -fno-warn-unused-do-bind Extensions: @@ -57,4 +59,4 @@ ScopedTypeVariables StandaloneDeriving DoAndIfThenElse - + DeriveDataTypeable