ddc-core-eval 0.2.1.2 → 0.4.1.3
raw patch · 11 files changed
Files
- DDC/Core/Eval.hs +4/−1
- DDC/Core/Eval/Check.hs +75/−48
- DDC/Core/Eval/Compounds.hs +112/−67
- DDC/Core/Eval/Env.hs +37/−49
- DDC/Core/Eval/Name.hs +112/−55
- DDC/Core/Eval/Prim.hs +72/−50
- DDC/Core/Eval/Profile.hs +43/−0
- DDC/Core/Eval/Step.hs +89/−86
- DDC/Core/Eval/Store.hs +22/−21
- LICENSE +1/−15
- ddc-core-eval.cabal +12/−10
DDC/Core/Eval.hs view
@@ -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
DDC/Core/Eval/Check.hs view
@@ -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
DDC/Core/Eval/Compounds.hs view
@@ -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
DDC/Core/Eval/Env.hs view
@@ -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
DDC/Core/Eval/Name.hs view
@@ -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+
DDC/Core/Eval/Prim.hs view
@@ -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
+ DDC/Core/Eval/Profile.hs view
@@ -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 }+
DDC/Core/Eval/Step.hs view
@@ -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
DDC/Core/Eval/Store.hs view
@@ -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)
LICENSE view
@@ -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-
ddc-core-eval.cabal view
@@ -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