diff --git a/DDC/Core/Eval.hs b/DDC/Core/Eval.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Eval.hs @@ -0,0 +1,15 @@ + +-- | Single step evaluator for the Disciple Core language. +-- +-- 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 +-- 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 (..) + , force + , step) +where +import DDC.Core.Eval.Step + diff --git a/DDC/Core/Eval/Check.hs b/DDC/Core/Eval/Check.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Eval/Check.hs @@ -0,0 +1,204 @@ + +module DDC.Core.Eval.Check + ( checkCapsX + , Error(..)) +where +import DDC.Core.Eval.Compounds +import DDC.Core.Eval.Name +import DDC.Core.Exp +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 + +type CheckM a = G.CheckM Error + +-- | Check for conflicting store capabilities in the program. +checkCapsX :: Exp a Name -> Maybe Error +checkCapsX xx + = case result $ checkCapsXM xx of + Left err -> Just err + Right ws + -> let caps = foldr mustInsertCap emptyCapSet ws + in checkCapSet caps + + +-- CapSet -------------------------------------------------------------------- +data CapSet + = CapSet + { capsGlobal :: Set Rgn + , capsConst :: Set Rgn + , capsMutable :: Set Rgn + , capsLazy :: Set Rgn + , capsManifest :: Set Rgn } + deriving Show + +-- | An empty capability set +emptyCapSet :: CapSet +emptyCapSet + = CapSet + { capsGlobal = Set.empty + , capsConst = Set.empty + , capsMutable = Set.empty + , capsLazy = Set.empty + , capsManifest = Set.empty } + + +-- | Insert a capability, or `error` if this isn't one. +mustInsertCap :: Witness Name -> CapSet -> CapSet +mustInsertCap ww caps + | WApp (WCon (WiConBound (UPrim nc _))) + (WType (TCon (TyConBound (UPrim nh _)))) <- ww + , NameCap c <- nc + , NameRgn r <- nh + = case c of + CapGlobal -> caps { capsGlobal = Set.insert r (capsGlobal caps) } + CapConst -> caps { capsConst = Set.insert r (capsConst caps) } + CapMutable -> caps { capsMutable = Set.insert r (capsMutable caps) } + CapLazy -> caps { capsLazy = Set.insert r (capsLazy caps) } + CapManifest -> caps { capsManifest = Set.insert r (capsManifest caps)} + + | otherwise + = error "mustInsertCap: not a capability" + + +-- | Check a capability set for conflicts between the capabilities. +checkCapSet :: CapSet -> Maybe Error +checkCapSet cs + | r : _ <- Set.toList + $ Set.intersection (capsConst cs) (capsMutable cs) + = Just $ ErrorConflict r CapConst CapMutable + + | r : _ <- Set.toList + $ Set.intersection (capsLazy cs) (capsManifest cs) + = Just $ ErrorConflict r CapLazy CapManifest + + | otherwise + = Nothing + + +-- Error ---------------------------------------------------------------------- +-- | Things that can go wrong with the capabilities in a program. +data Error + -- | Conflicting capabilities in program. + = ErrorConflict + { errorRegions :: Rgn + , errorCap1 :: Cap + , errorCap2 :: Cap } + + -- | A partially applied capability constructor. + -- In the formal semantics, capabilities are atomic, so this isn't + -- a problem. However, as we're representing them with general witness + -- appliction we need to ensure the constructors aren't partially + -- applied. + | ErrorPartial + { 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 } + + +instance Pretty Error where + ppr err + = case err of + ErrorConflict r c1 c2 + -> vcat [ text "Conflicting capabilities in core program." + , text " region: " <> ppr r + , text " can't be both: " <> ppr c1 + , text " and: " <> ppr c2 ] + + ErrorPartial w1 + -> vcat [ text "Partially applied capability constructor." + , text "with: " <> ppr w1] + + ErrorNonHandle w1 + -> vcat [ text "Capability constructor applied to a non-region handle." + , text "with: " <> ppr w1] + + +------------------------------------------------------------------------------- +-- | Collect the list of capabilities in an expression, +-- and check that they are well-formed. +checkCapsXM :: Exp a Name -> CheckM a [Witness Name] +checkCapsXM xx + = let none = return [] + in case xx of + XVar{} -> none + XCon{} -> none + XLAM _ _ x -> checkCapsXM x + XLam _ _ x -> checkCapsXM x + XApp _ x1 x2 -> liftM2 (++) (checkCapsXM x1) (checkCapsXM x2) + XLet _ lts x1 -> liftM2 (++) (checkCapsLM lts) (checkCapsXM x1) + XCase _ x1 alts -> liftM2 (++) (checkCapsXM x1) + (liftM concat $ mapM checkCapsAM alts) + XCast _ cc x1 -> liftM2 (++) (checkCapsCM cc) (checkCapsXM x1) + XType{} -> none + XWitness w -> checkCapsWM w + + +checkCapsCM :: Cast Name -> CheckM a [Witness Name] +checkCapsCM cc + = let none = return [] + in case cc of + CastWeakenEffect{} -> none + CastWeakenClosure{} -> none + CastPurify w -> checkCapsWM w + CastForget w -> checkCapsWM w + + +checkCapsLM :: Lets a Name -> CheckM a [Witness Name] +checkCapsLM ll + = let none = return [] + in case ll of + LLet m _ x -> liftM2 (++) (checkCapsMM m) (checkCapsXM x) + LRec bxs -> liftM concat (mapM checkCapsXM $ map snd bxs) + LLetRegion{} -> 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 aa + = case aa of + AAlt _ x -> checkCapsXM x + + +checkCapsWM :: Witness Name -> CheckM a [Witness Name] +checkCapsWM ww + = let none = return [] + in case ww of + WVar{} -> none + + WCon{} + | isCapConW ww -> throw $ ErrorPartial ww + | otherwise -> none + + + WApp w1@WCon{} w2@(WType tR) + | isCapConW w1 + -> if isJust $ takeHandleT tR + then return [ww] + else throw $ ErrorNonHandle 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 + diff --git a/DDC/Core/Eval/Compounds.hs b/DDC/Core/Eval/Compounds.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Eval/Compounds.hs @@ -0,0 +1,162 @@ + +-- | Utilities for constructing and destructing compound types and +-- expressions. +module DDC.Core.Eval.Compounds + ( -- * Types + tUnit + , tInt + , tList + + -- * Witnesses + , wGlobal + , wConst, wMutable + , wLazy, wManifest + , wcGlobal + , wcConst, wcMutable + , wcLazy, wcManifest + , isCapConW + + -- * Expressions + , isUnitX + , takeHandleT + , takeHandleX + , takeLocX, stripLocX + , takeMutableX) +where +import DDC.Core.Eval.Name +import DDC.Type.Compounds +import DDC.Core.Exp + + +-- Type ----------------------------------------------------------------------- +-- | Application of the Unit data type constructor. +tUnit :: Type Name +tUnit = TCon (TyConBound (UPrim (NamePrimCon PrimTyConUnit) kData)) + + +-- | Application of the Int data type constructor. +tInt :: Region Name -> Type Name +tInt r1 = TApp (TCon (TyConBound (UPrim (NamePrimCon PrimTyConInt) + (kFun kRegion kData)))) + r1 + +-- | Application of the List data 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] + + +-- Witness -------------------------------------------------------------------- +wGlobal :: Region Name -> Witness Name +wGlobal r = WApp (WCon wcGlobal) (WType r) + +wConst :: Region Name -> Witness Name +wConst r = WApp (WCon wcConst) (WType r) + +wMutable :: Region Name -> Witness Name +wMutable r = WApp (WCon wcMutable) (WType r) + +wLazy :: Region Name -> Witness Name +wLazy r = WApp (WCon wcLazy) (WType r) + +wManifest :: Region Name -> Witness Name +wManifest r = WApp (WCon wcManifest) (WType r) + + +-- Just the Constructors +wcGlobal :: WiCon Name +wcGlobal = WiConBound + $ UPrim (NameCap CapGlobal) (tForall kRegion $ \r -> tGlobal r) + +wcConst :: WiCon Name +wcConst = WiConBound + $ UPrim (NameCap CapConst) (tForall kRegion $ \r -> tConst r) + +wcMutable :: WiCon Name +wcMutable = WiConBound + $ UPrim (NameCap CapMutable) (tForall kRegion $ \r -> tMutable r) + +wcLazy :: WiCon Name +wcLazy = WiConBound + $ UPrim (NameCap CapLazy) (tForall kRegion $ \r -> tLazy r) + +wcManifest :: WiCon Name +wcManifest = WiConBound + $ UPrim (NameCap CapManifest) (tForall kRegion $ \r -> tManifest r) + + +-- | Check whether a witness is a capability constructor. +isCapConW :: Witness Name -> Bool +isCapConW ww + = case ww of + WCon WiConBound{} -> True + _ -> False + + + +-- Exp ------------------------------------------------------------------------ +-- | Check whether an expression is the unit constructor. +isUnitX :: Exp a Name -> Bool +isUnitX xx + = case xx of + XCon _ (UPrim (NamePrimCon PrimDaConUnit) _) + -> True + _ -> False + + +-- | Take a region handle from a type. +takeHandleT :: Type Name -> Maybe Rgn +takeHandleT tt + = case tt of + TCon (TyConBound (UPrim (NameRgn r1) _)) + -> Just r1 + _ -> Nothing + + +-- | Take a region handle from an expression. +takeHandleX :: Exp a Name -> Maybe Rgn +takeHandleX xx + = case xx of + XType t -> takeHandleT t + _ -> Nothing + + +-- | 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 + + +-- | 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 + + +-- | 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 + -> takeHandleT tR1 + _ -> Nothing + + + diff --git a/DDC/Core/Eval/Env.hs b/DDC/Core/Eval/Env.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Eval/Env.hs @@ -0,0 +1,204 @@ + +-- | Primitive types and operators for the core language evaluator. +-- +-- These are only a subset of the primitives supported by the real compiler, there's just +-- enough to experiment with the core language. +-- +module DDC.Core.Eval.Env + ( -- * Data Type Definitions. + primDataDefs + + -- * Kind environment. + , primKindEnv + , kindOfPrimName + + -- * Type Environment. + , primTypeEnv + , typeOfPrimName + , arityOfName) +where +import DDC.Core.Eval.Compounds +import DDC.Core.Eval.Name +import DDC.Core.DataDef +import DDC.Type.Exp +import DDC.Type.Compounds +import DDC.Type.Env (Env) +import qualified DDC.Type.Env as Env + + +-- DataDefs ------------------------------------------------------------------- +-- | Data type definitions for: +-- +-- @ Type Constructors +-- ---- ------------ +-- Unit () +-- Int 0 1 2 3 ... +-- List Nil Cons +-- @ +primDataDefs :: DataDefs Name +primDataDefs + = fromListDataDefs + -- Unit + [ DataDef + (NamePrimCon PrimTyConUnit) + [] + (Just [ (NamePrimCon PrimDaConUnit, []) ]) + + -- Int + , DataDef + (NamePrimCon PrimTyConInt) + [kRegion] + Nothing + + -- List + , DataDef + (NamePrimCon PrimTyConList) + [kRegion, kData] + (Just [ (NamePrimCon PrimDaConNil, []) + , (NamePrimCon PrimDaConCons, [tList (tIx kRegion 1) (tIx kData 0)])]) + ] + + +-- Kinds ---------------------------------------------------------------------- +-- | Kind environment containing kinds of primitive data types. +primKindEnv :: Env Name +primKindEnv = Env.setPrimFun kindOfPrimName Env.empty + + +-- | Take the kind of a primitive name. +-- +-- Returns `Nothing` if the name isn't primitive. +-- +kindOfPrimName :: Name -> Maybe (Kind Name) +kindOfPrimName nn + = case nn of + NameRgn _ + -> Just $ kRegion + + -- Unit + NamePrimCon PrimTyConUnit + -> Just $ kData + + -- List + NamePrimCon PrimTyConList + -> Just $ kRegion `kFun` kData `kFun` kData + + -- Int + NamePrimCon PrimTyConInt + -> Just $ kFun kRegion kData + + _ -> Nothing + + + + +-- Types ---------------------------------------------------------------------- +-- | Type environment containing types of primitive data constructors as well +-- as the following primitive operators: +-- +-- @negInt, addInt, subInt, mulInt, divInt, eqInt, updateInt@ +-- +-- It also contains types for the primitive capability constructors: +-- +-- @Global\#, Const\#, Mutable\#, Lazy\#, Manifest\#@ +-- +primTypeEnv :: Env Name +primTypeEnv = Env.setPrimFun typeOfPrimName Env.empty + + +-- | Take the type of a primitive name. +-- +-- Returns `Nothing` if the name isn't primitive. +-- +typeOfPrimName :: Name -> Maybe (Type Name) +typeOfPrimName nn + = case nn of + -- Unit + NamePrimCon PrimDaConUnit + -> Just $ tUnit + + + -- List + NamePrimCon PrimDaConNil + -> Just $ tForalls [kRegion, kData] $ \[tR, tA] + -> tFun tUnit (tAlloc tR) + (tBot kClosure) + $ tList tR tA + + NamePrimCon PrimDaConCons + -> Just $ tForalls [kRegion, kData] $ \[tR, tA] + -> tFun tA (tBot kEffect) + (tBot kClosure) + $ tFun (tList tR tA) (tSum kEffect [tAlloc tR]) + (tSum kClosure [tDeepUse tA]) + $ tList tR tA + + -- Int + NameInt _ + -> Just $ tForall kRegion + $ \r -> tFun 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]) + (tBot kClosure) + $ (tInt r0) + + -- add, sub, mul, div, eq + NamePrimOp p + | elem p [PrimOpAddInt, PrimOpSubInt, PrimOpMulInt, PrimOpDivInt, PrimOpEqInt] + -> Just $ tForalls [kRegion, kRegion, kRegion] $ \[r2, r1, r0] + -> tFun (tInt r2) (tBot kEffect) + (tBot kClosure) + $ tFun (tInt r1) (tSum kEffect [tRead r2, tRead r1, tAlloc r0]) + (tSum kClosure [tUse r2]) + $ tInt r0 + + -- update :: [r1 r2 : %]. Mutable r1 => Int r1 -> Int r2 -(Write r1 + Read r2 | Share r1)> () + NamePrimOp PrimOpUpdateInt + -> Just $ tForalls [kRegion, kRegion] $ \[r1, r2] + -> tImpl (tMutable r1) + $ tFun (tInt r1) (tBot kEffect) + (tBot kClosure) + $ tFun (tInt r2) (tSum kEffect [tWrite r1, tRead r2]) + (tSum kClosure [tUse r1]) + $ tUnit + + 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 + + _ -> Nothing + + + +-- | Take the arity of a primitive name. +--- +-- TODO: determine this from the type. +arityOfName :: Name -> Maybe Int +arityOfName n + = case n of + NameLoc{} -> Just 0 + NameRgn{} -> Just 0 + NameInt{} -> Just 2 + + NamePrimCon PrimDaConUnit -> Just 0 + NamePrimCon PrimDaConNil -> Just 3 + + NamePrimCon PrimDaConCons -> Just 4 + + NamePrimOp p + | elem p [ PrimOpAddInt, PrimOpSubInt, PrimOpMulInt, PrimOpDivInt + , PrimOpEqInt] + -> Just 5 + + NamePrimOp PrimOpUpdateInt + -> Just 5 + + _ -> Nothing + diff --git a/DDC/Core/Eval/Name.hs b/DDC/Core/Eval/Name.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Eval/Name.hs @@ -0,0 +1,245 @@ + +module DDC.Core.Eval.Name + ( Name (..) + , PrimCon (..) + , PrimOp (..) + , Loc (..) + , Rgn (..) + , Cap (..) + , readName + , lexString) +where +import DDC.Base.Pretty +import DDC.Base.Lexer +import DDC.Core.Parser.Lexer +import DDC.Core.Parser.Tokens +import Data.Char +import Data.Maybe + + +-- | Names of things recognised by the evaluator. +-- +data Name + -- Names whose types are bound in the environments. + = NameVar String -- ^ User variables. + | NameCon String -- ^ User constructors. + + -- Names whose types are baked in, and should be attached to + -- the `Bound` constructor that they appear in. + | NameInt Integer -- ^ Integer literals (which data constructors). + | NamePrimCon PrimCon -- ^ Primitive constructors (eg @List, Nil@). + | NamePrimOp PrimOp -- ^ Primitive operators (eg @addInt, subInt@). + + | NameLoc Loc -- ^ Store locations. + | NameRgn Rgn -- ^ Region handles. + | NameCap Cap -- ^ Store capabilities. + + deriving (Show, Eq, Ord) + + +instance Pretty Name where + ppr nn + = case nn of + NameVar v -> text v + NameCon c -> text c + NameInt i -> text (show i) + NamePrimCon c -> ppr c + NamePrimOp op -> ppr op + NameLoc l -> ppr l + NameRgn r -> ppr r + NameCap p -> ppr p + + +-- Locations ------------------------------------------------------------------ +-- | A store location. +-- +-- These are pretty printed like @L4#@. +data Loc + = Loc Int + deriving (Eq, Ord, Show) + +instance Pretty Loc where + ppr (Loc l) + = text "L" <> text (show l) <> text "#" + + +-- Regions -------------------------------------------------------------------- +-- | A region handle. +-- +-- These are pretty printed like @R5#@. +data Rgn + = Rgn Int + deriving (Eq, Ord, Show) + +instance Pretty Rgn where + ppr (Rgn r) + = text "R" <> text (show r) <> text "#" + + +-- Capabilities -------------------------------------------------------------- +-- | These are primitive witnesses that guarantee the associated property +-- of the program. Ostensibly, they are only introduced by the system +-- at runtime, but for testing purposes we can also inject them into +-- the source program. +data Cap + -- | Witness that a region is global. + -- Global regions live for the duration of the program and are not + -- 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 + + -- | 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 + + -- | 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 + + -- | 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 + + -- | 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 + deriving (Eq, Ord, Show) + + +instance Pretty Cap where + ppr cp + = case cp of + CapGlobal -> text "Global#" + CapConst -> text "Const#" + CapMutable -> text "Mutable#" + CapLazy -> text "Lazy#" + CapManifest -> text "Manifest#" + + +-- PrimCons ------------------------------------------------------------------- +-- | A primitive constructor. +data PrimCon + = PrimTyConUnit -- ^ Unit type constructor (@Unit@). + | PrimDaConUnit -- ^ Unit data constructor (@()@). + | PrimTyConInt -- ^ @Int@ type constructor. + + -- Implement lists as primitives until we have data decls working + | PrimTyConList -- ^ @List@ data type constructor. + | PrimDaConNil -- ^ @Nil@ data constructor. + | PrimDaConCons -- ^ @Cons@ data constructor. + deriving (Show, Eq, Ord) + + +instance Pretty PrimCon where + ppr con + = case con of + PrimTyConUnit -> text "Unit" + PrimDaConUnit -> text "()" + PrimTyConInt -> text "Int" + PrimTyConList -> text "List" + PrimDaConNil -> text "Nil" + PrimDaConCons -> text "Cons" + + +-- PrimOps -------------------------------------------------------------------- +-- | A primitive operator. +data PrimOp + = PrimOpNegInt + | PrimOpAddInt + | PrimOpSubInt + | PrimOpMulInt + | PrimOpDivInt + | PrimOpEqInt + | PrimOpUpdateInt + deriving (Show, Eq, Ord) + + +instance Pretty PrimOp where + ppr op + = case op of + PrimOpNegInt -> text "negInt" + PrimOpAddInt -> text "addInt" + PrimOpSubInt -> text "subInt" + PrimOpMulInt -> text "mulInt" + PrimOpDivInt -> text "divInt" + PrimOpEqInt -> text "eqInt" + PrimOpUpdateInt -> text "updateInt" + + +-- Parsing -------------------------------------------------------------------- +-- | Read a primitive name. +readName :: String -> Maybe Name +readName [] = Nothing +readName str@(c:rest) + -- primops + | isLower c + = case (c:rest) of + "negInt" -> Just $ NamePrimOp PrimOpNegInt + "addInt" -> Just $ NamePrimOp PrimOpAddInt + "subInt" -> Just $ NamePrimOp PrimOpSubInt + "mulInt" -> Just $ NamePrimOp PrimOpMulInt + "divInt" -> Just $ NamePrimOp PrimOpDivInt + "eqInt" -> Just $ NamePrimOp PrimOpEqInt + "updateInt" -> Just $ NamePrimOp PrimOpUpdateInt + _ -> 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) + + -- implement lists as primitive until we have data type decls implemented + | 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 + + -- other constructors + | isUpper c + = Just $ NameCon str + + | 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. +lexString :: Int -> String -> [Token (Tok Name)] +lexString lineStart str + = map rn $ lexExp lineStart str + where rn (Token t sp) = Token (renameTok readName_ t) sp + diff --git a/DDC/Core/Eval/Prim.hs b/DDC/Core/Eval/Prim.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Eval/Prim.hs @@ -0,0 +1,177 @@ + +-- | Single step evaluation of primitive operators and constructors. +--- +-- This should implements the proper operational semantics of the core language, +-- so we're careful to check all premises of the evaluation rules are satisfied. +module DDC.Core.Eval.Prim + ( stepPrimCon + , stepPrimOp + , primNewRegion + , primDelRegion) +where +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. + -> [Exp () Name] -- ^ Arguments to constructor. + -> Store -- ^ Current store. + -> Maybe ( Store + , Exp () Name) -- ^ New store and result expression, + -- if the operator steps, otherwise `Nothing`. + +-- Alloction of Ints. +stepPrimCon (NameInt i) [xR, xUnit] store + -- unpack the args + | XType tR <- xR + , Just rgn <- takeHandleT tR + , isUnitX 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 + + = Just ( store1 + , XCon () (UPrim (NameLoc l) (tInt tR))) + + +-- Handle Nil and Cons specially until we have general data types. +stepPrimCon n@(NamePrimCon PrimDaConNil) [xR, xA, xUnit] store + -- unpack the args + | XType tR <- xR + , Just rgn <- takeHandleT tR + , XType tA <- xA + , isUnitX 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 + + = Just ( store1 + , XCon () (UPrim (NameLoc l) (tList tR tA))) + + +stepPrimCon n@(NamePrimCon PrimDaConCons) [xR, xA, xHead, xTail] store + -- unpack the args + | XType tR <- xR + , Just rgn <- takeHandleT tR + , XType tA <- xA + , Just lHead <- takeLocX xHead + , Just lTail <- takeLocX xTail + + -- 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 [lHead, lTail]) store + + = Just ( store1 + , XCon () (UPrim (NameLoc l) (tList tR tA))) + +stepPrimCon _ _ _ + = Nothing + + +------------------------------------------------------------------------------- +-- | Step a primitive operator. +stepPrimOp + :: Name -- ^ Name of operator to evaluate. + -> [Exp () Name] -- ^ Arguments to operator. + -> Store -- ^ Current store. + -> Maybe ( Store + , Exp () Name) -- ^ New store and result expression, + -- if the operator steps, otherwise `Nothing`. + +-- Binary integer primop. +stepPrimOp (NamePrimOp op) [xR1, xR2, xR3, xL1, xL2] store + -- unpack the args + | Just fOp <- lookup op + [ (PrimOpAddInt, (+)) + , (PrimOpSubInt, (-)) + , (PrimOpMulInt, (*)) + , (PrimOpDivInt, div) + , (PrimOpEqInt, (\x y -> if x == y then 1 else 0))] + , Just r1 <- takeHandleX xR1 + , Just r2 <- takeHandleX xR2 + , 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 + + -- the locations must be in the regions the args said they were in + , r1' == r1 + , r2' == r2 + + -- the destination region must exist + , Store.hasRgn store r3 + + -- do the actual computation + , 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 + + = Just ( store1 + , XCon () (UPrim (NameLoc l3) (tInt tR3))) + + +-- Update integer primop. +stepPrimOp (NamePrimOp PrimOpUpdateInt) [xR1, xR2, xMutR1, xL1, xL2] store + -- unpack the args + | Just r1 <- takeHandleX xR1 + , Just r2 <- takeHandleX xR2 + , Just r1W <- takeMutableX xMutR1 + , Just l1 <- stripLocX xL1 + , Just l2 <- stripLocX xL2 + + -- the witness must be for the destination region + , 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 + + -- 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 + + = Just ( store1 + , XCon () (UPrim (NamePrimCon PrimDaConUnit) tUnit)) + +stepPrimOp _ _ _ + = Nothing + + +-- Store ---------------------------------------------------------------------- +-- | Like `Store.newRgn` but return the region handle wrapped in a `Bound`. +primNewRegion :: Store -> (Store, Bound Name) +primNewRegion store + = let (store', rgn) = Store.newRgn store + u = UPrim (NameRgn rgn) kRegion + in (store', u) + + +-- | Like `Store.delRgn` but accept a region handle wrapped in a `Bound`. +primDelRegion :: Bound Name -> Store -> Maybe Store +primDelRegion uu store + = case uu of + UPrim (NameRgn rgn) _ -> Just $ Store.delRgn rgn store + _ -> Nothing + diff --git a/DDC/Core/Eval/Step.hs b/DDC/Core/Eval/Step.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Eval/Step.hs @@ -0,0 +1,545 @@ + +-- | Single step evalation for the Disciple Core language. +module DDC.Core.Eval.Step + ( StepResult(..) + , force + , step + , isValue + , isWeakValue) +where +import DDC.Core.Eval.Store +import DDC.Core.Eval.Name +import DDC.Core.Eval.Prim +import DDC.Core.Eval.Env +import DDC.Core.Eval.Compounds +import DDC.Core.Transform.SubstituteWX +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 Data.Set as Set + + +-- StepResult ----------------------------------------------------------------- +-- | The result of stepping some expression. +data StepResult + -- | Expression progressed to a new state. + = StepProgress Store (Exp () Name) + + -- | Expression cannot step and is a (weak) value. + -- We're done already. + | StepDone + + + -- | Expression cannot step, and is not a (weak) value. + -- The original expression was mistyped, + -- or something is wrong with the interpreter. + | StepStuck + + -- | Expression is stuck, and we know for sure it's mistyped. + | StepStuckMistyped (Error () Name) + deriving (Show) + + +-- force ---------------------------------------------------------------------- +-- | Single step a core expression to a value. +-- +-- As opposed to `step`, if the provided expression is the location of a +-- Thunk, then the thunk will be forced. +-- +force :: Store -- ^ Current store. + -> Exp () Name -- ^ Expression to force. + -> StepResult -- ^ Result of forcing it. + +force store xx + | (casts, xx') <- unwrapCasts xx + , XCon _ (UPrim (NameLoc l) _) <- xx' + , Just (rgn, t, SThunk x) <- lookupRegionTypeBind l store + = case force store x of + StepProgress store' x' + -> let store2 = addBind l rgn t (SThunk x') store' + in StepProgress store2 (wrapCasts casts xx) + + StepDone + -> StepProgress store x + + err -> err + + | otherwise + = step store xx + + +-- step ----------------------------------------------------------------------- +-- | Single step a code expression to a weak value. +-- +-- As opposed to `force`, if the provided expression is the location of a +-- Thunk, then the thunk is not forced. +-- +step :: Store -- ^ Current store. + -> Exp () Name -- ^ Expression to step. + -> StepResult -- ^ Result of stepping it. + + +-- (EvLam) +-- Add abstractions to the heap. +-- We need the type of the expression to attach to the location +-- This fakes the store typing from the formal typing rules. +step store xx + | (casts, xp) <- unwrapCasts xx + , isLambdaX xp + = case typeOfExp primDataDefs xp of + Left err -> StepStuckMistyped 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)) + + +-- (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 PrimDaConUnit) _ -> False + UPrim NamePrimCon{} _ -> True + UPrim NameInt{} _ -> True + UPrim NameCon{} _ -> True + _ -> False + + , UPrim n _ <- u + , Just arity <- arityOfName n + , length xs == arity + , and $ map (isWeakValue store) xs + , Just (store', x') <- stepPrimCon n 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 + = let + -- TODO: we're not allowing over-applied primops + stepArg i _acc [] + | i == arity + , Just (store', x') <- stepPrimOp p xs store + = Right (store', x') + + -- The arguments are all values, but the primop didn't step. + | otherwise + = Left StepStuck + + stepArg i acc (ax:axs) + = case force store ax of + StepProgress store' x' + -> Right (store', makeXApps () x1 (reverse acc ++ (x' : axs))) + + StepDone + -> case stepArg (i + 1) (ax : acc) axs of + Left err -> Left err + result -> result + + err -> Left err + + in case stepArg 0 [] xs of + Left err -> err + Right (store', x') -> StepProgress store' x' + + +-- (EvAppArgs) +-- Step the left-most non-wnf argument of a lambda. +step store xx + | 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. + , arity <- length bs + , wnfs <- map (isWeakValue store) xsArgs + , or (take arity $ map not wnfs) + + = let -- Step the first non-wnf argument. + -- This should never error, as we took as many args + -- as we had wnf flags. + stepArg _ [] + = error "stepArg: no more args" + + stepArg [] xs + = Right (store, xs) + + stepArg (True:ws) (x:xs) + = case stepArg ws xs of + Right (store', xs') -> Right (store', x : xs') + Left err -> Left err + + stepArg (False:_) (x:xs) + = case step store x of + StepProgress store' x' -> Right (store', x' : xs) + err -> Left err + + in case stepArg wnfs xsArgs of + Left err -> err + Right (store2, xsArgs') + -> StepProgress store2 (makeXApps () 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 (Rgn 0, _, SLams fbs xBody) <- lookupRegionTypeBind l1 store + + -- Take as many wnfs as possible to satisfy binders. + , arity <- length fbs + , (wnfs, nonWnfs) <- span (isWeakValue store) xsArgs + + -- If we have any wnfs at all, then we can do a substitution. + , not $ null wnfs + + = let argsToSubst = take arity wnfs + argsOverApplied = drop (length argsToSubst) wnfs + argsLeftover = argsOverApplied ++ nonWnfs + + bs = map snd fbs + bsToSubst = take (length argsToSubst) bs + bsLeftover = drop (length bsToSubst) fbs + + xResult = substituteXArgs (zip bsToSubst argsToSubst) + $ makeXLamFlags () bsLeftover xBody + + in StepProgress store + $ wrapCasts casts (makeXApps () xResult argsLeftover) + + +-- (EvApp1 / EvApp2) +-- Evaluate the components of an application. +step store (XApp a x1 x2) + | (casts, x1p) <- unwrapCasts x1 + = case force store x1p of + StepProgress store' x1p' + -> StepProgress store' (XApp a (wrapCasts casts x1p') x2) + + StepDone + -> case step store x2 of + StepProgress store' x2' + -> StepProgress store' (XApp a x1 x2') + + err -> err + + err -> err + + +-- (EvLetStrictStep / EvLetStrictSubst) +-- Substitute in a bound value in a let expression. +step store (XLet a (LLet LetStrict b x1) x2) + = case step store x1 of + StepProgress store' x1' + -> StepProgress store' (XLet a (LLet LetStrict b x1') x2) + + StepDone + -> StepProgress store (substituteXX b x1 x2) + + 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) + = let (bs, xs) = unzip bxs + 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] + + -- 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 + _ -> Nothing) + xs' + + -- If this fails then some of the bindings did not have lambdas out the + -- front. We don't support plain value recursion yet. + in case sequence mos of + Nothing -> StepStuck + Just os + -> let -- Add all the objects to the store. + store2 = foldr (\(l, t, o) -> addBind l (Rgn 0) t o) store1 + $ zip3 ls ts os + + -- Substitute locations into the body expression. + x2' = substituteXXs (zip bs xls) x2 + + in StepProgress store2 x2' + + +-- (EvCreateRegion) +-- Create a new region. +step store (XLet a (LLetRegion bRegion bws) x) + | Just uRegion <- takeSubstBoundOfBind bRegion + + -- Allocate a new region handle for the bound region. + , (store1, uHandle@(UPrim (NameRgn rgn) _)) + <- primNewRegion store + , tHandle <- TCon $ TyConBound uHandle + + -- Substitute handle into the witness types. + , bws' <- map (substituteBoundTX uRegion tHandle) bws + + -- 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 typeOfBind bws' + + = let -- Substitute handle and witnesses into body. + x' = substituteBoundTX uRegion tHandle + $ substituteWXs (zip bws' wits) x + + isGlobalBind b + = case typeOfBind b of + TApp (TCon (TyConWitness TwConGlobal)) _ + -> True + _ -> False + + -- Set region to global if there is a witness for it. + store2 = if or $ map isGlobalBind bws + then setGlobal rgn store1 + else store1 + + 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 + -- to reference the region variable. Just create a dummy region in the + -- store to simulate what would happen if there was a real binder. + | otherwise + = let (store', _) = primNewRegion store + in StepProgress store' x + + +-- (EvEjectRegion) +-- Eject completed value from the region context, and delete the region. +step store (XLet _ (LWithRegion r@(UPrim (NameRgn rgn) _)) x) + | isWeakValue store x + , Set.member rgn (storeGlobal store) + = StepProgress store x + + | isWeakValue store x + , Just store' <- primDelRegion r store + = StepProgress store' x + + +-- (EvWithRegion) +-- Reduction within a region context. +step store (XLet a (LWithRegion uRegion) x) + = case step store x of + StepProgress store' x' + -> StepProgress store' (XLet a (LWithRegion uRegion) x') + err -> err + + +-- (EvCaseStep / EvCaseMatch) +-- Case branching. +step store (XCase a xDiscrim alts) + = case force store xDiscrim of + StepProgress store' xDiscrim' + -> StepProgress store' (XCase a xDiscrim' alts) + + StepDone + | (casts, xDiscrim') <- unwrapCasts xDiscrim + , Just lDiscrim <- takeLocX xDiscrim' + , Just (SObj nTag lsArgs) <- lookupBind lDiscrim store + , Just tsArgs <- sequence $ map (\l -> lookupTypeOfLoc l store) lsArgs + , AAlt pat xBody : _ <- filter (tagMatchesAlt nTag) alts + -> case pat of + PDefault + -> StepProgress store xBody + + PData _ bsArgs + | bxsArgs <- [ (b, wrapCasts casts (XCon a (UPrim (NameLoc l) t))) + | l <- lsArgs + | t <- tsArgs + | b <- bsArgs] + -> StepProgress store + (substituteXXs bxsArgs xBody) + + | otherwise + -> StepStuck + + err -> err + + +-- (EvPurifyEject) +-- Eject values from purify casts as there are no more effects to be had. +step store (XCast _ (CastPurify _) x) + | isWeakValue store x + = StepProgress store x + + +-- (EvCast) +-- Evaluate under casts. +step store (XCast a cc x) + = case step store x of + StepProgress store' x' + -> StepProgress store' (XCast a cc x') + err -> err + + +-- (Done/Stuck) +-- Either already a value, or expression is stuck. +step store xx + | isWeakValue store xx = StepDone + | otherwise = StepStuck + + +-- Casts ---------------------------------------------------------------------- +-- Unwrap casts from the front of an expression. +unwrapCasts :: Exp () n -> ([Cast n], Exp () n) +unwrapCasts xx + = case xx of + XCast _ c x + -> let (cs, x') = unwrapCasts x + in (c : cs, x') + + _ -> ([], xx) + + +-- Wrap casts around an expression. +wrapCasts :: [Cast n] -> Exp () n -> Exp () n +wrapCasts cc xx + = case cc of + [] -> xx + c : cs -> XCast () c (wrapCasts cs xx) + + +-- Alternatives --------------------------------------------------------------- +-- | See if a constructor tag matches a case alternative. +tagMatchesAlt :: Name -> Alt a Name -> Bool +tagMatchesAlt n (AAlt p _) + = tagMatchesPat n p + + +-- | See if a constructor tag matches a pattern. +tagMatchesPat :: Name -> Pat Name -> Bool +tagMatchesPat _ PDefault = True +tagMatchesPat n (PData u' _) + = case takeNameOfBound u' of + Just n' -> n == n' + _ -> False + + +-- isValue ---------------------------------------------------------------- +-- | Check if an expression is a value. +-- Values can't be progressed any further, with either `force` or `step`. +isValue :: Store -> Exp a Name -> Bool +isValue store xx + = isSomeValue False store xx + + +-- | Check if an expression is a weak values. +-- 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 + + + +-- | Check if an expression is a weak value. +isSomeValue :: Bool -> Store -> Exp a Name -> Bool +isSomeValue weak store xx + = case xx of + XVar{} -> True + + XCon _ (UPrim (NameLoc l) _) + | Just SThunk{} <- lookupBind l store + -> weak + + XCon{} -> True + + -- Plain lambdas aren't weak values because we always add them + -- to the store. The resulting store location is then a value. + XLAM{} -> False + XLam{} -> False + + XLet{} -> False + XCase{} -> False + + XCast _ (CastPurify _) _ + -> False + + XCast _ _ x + -> isSomeValue weak store x + + XType{} -> True + XWitness{} -> True + + XApp _ x1 x2 + + -- Application if a primop to enough args is not wnf. + | Just (n, xs) <- takeXPrimApps xx + , and $ map (isSomeValue weak store) xs + , 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 + -> False + + -- Application of a data constructor to enough args is not wnf. + | Just (u, xs) <- takeXConApps xx + , and $ map (isSomeValue weak store) xs + , UPrim n _ <- u + , Just a <- arityOfName n + , length xs >= a + -> False + + -- Application of some other expression, + -- maybe an under-applied primop or data constructor. + | otherwise + -> isSomeValue weak store x1 + && isSomeValue weak store x2 + + +-- | 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 + _ -> Nothing + diff --git a/DDC/Core/Eval/Store.hs b/DDC/Core/Eval/Store.hs new file mode 100644 --- /dev/null +++ b/DDC/Core/Eval/Store.hs @@ -0,0 +1,239 @@ + +-- | Definition of the store. +--- +-- This implements the store in terms of the operational semantics of the +-- core language, and isn't intended to be efficient in a practical sense. +-- If we cared about runtime performance we'd want to use an IOArray or +-- some other mutable structure to hold the bindings, instead of a Data.Map. +-- +module DDC.Core.Eval.Store + ( Store (..) + , Loc (..) + , Rgn (..) + , SBind (..) + + -- * Operators + , empty + , newLoc, newLocs + , newRgn, newRgns + , delRgn + , hasRgn + , setGlobal + , addBind + , allocBind, allocBinds + , lookupBind + , lookupTypeOfLoc + , lookupRegionTypeBind) +where +import DDC.Core.Exp +import DDC.Core.Eval.Name +import Control.Monad +import DDC.Core.Pretty hiding (empty) +import Data.Map (Map) +import Data.Set (Set) +import qualified Data.Map as Map +import qualified Data.Set as Set + + +data Store + = Store + { -- | Next store location to allocate. + storeNextLoc :: Int + + -- | Next region handle to allocate. + , storeNextRgn :: Int + + -- | Region handles already allocated. + , storeRegions :: Set Rgn + + -- | Regions that are marked as global, and are not + -- deallocated with a stack discipline. + , storeGlobal :: Set Rgn + + -- | Map of locations to store bindings, + -- their types, + -- and the handle for the regions they're in. + , storeBinds :: Map Loc (Rgn, Type Name, SBind) } + deriving Show + + +-- | Store binding. +-- These are naked objects that can be allocated directly into the heap. +data SBind + -- | An algebraic data constructor. + = SObj + { sbindDataTag :: Name + , sbindDataArgs :: [Loc] } + + -- | Lambda abstraction, used for recursive bindings. + -- The flag indicates whether each binder is level-1 (True) or level-0 (False). + | SLams + { sbindLamBinds :: [(Bool, Bind Name)] + , sbindLamBody :: Exp () Name } + + -- | A thunk, used for lazy evaluation. + | SThunk + { sbindThunkExp :: Exp () Name } + deriving (Eq, Show) + + +-- Pretty --------------------------------------------------------------------- +instance Pretty Store where + ppr (Store nextLoc nextRgn regions global binds) + = vcat + [ text "* STORE" + , text " NextLoc: " <> text (show nextLoc) + , text " NextRgn: " <> text (show nextRgn) + + , text " Regions: " <> braces (sep $ punctuate comma + $ map ppr $ Set.toList regions) + + , text " Global: " <> braces (sep $ punctuate comma + $ map ppr $ Set.toList global) + , text "" + , text " Binds:" + , vcat $ [ text " " <> ppr l <> colon <> ppr r <> text " -> " <> ppr sbind + <> line + <> text " :: " <> ppr t + | (l, (r, t, sbind)) <- Map.toList binds] ] + + +instance Pretty SBind where + ppr (SObj tag []) + = text "OBJ" <+> ppr tag + + ppr (SObj tag svs) + = text "OBJ" <+> ppr tag + <+> (sep $ map ppr svs) + + ppr (SLams fbs x) + = text "LAMS" <+> sep (map (parens . ppr) fbs) + <> text "." + <> text (renderPlain $ ppr x) + + ppr (SThunk x) + = text "THUNK" <+> text (renderPlain $ ppr x) + + +-- Constructors --------------------------------------------------------------- +-- | An empty store, with no bindings or regions. +empty :: Store +empty = Store + { storeNextLoc = 1 + , storeNextRgn = 1 + , storeRegions = Set.empty + , storeGlobal = Set.empty + , storeBinds = Map.empty } + + +-- Locations ------------------------------------------------------------------ +-- | Create a new location in the store. +newLoc :: Store -> (Store, Loc) +newLoc store + = let loc = storeNextLoc store + store' = store { storeNextLoc = loc + 1 } + in (store', Loc loc) + + +-- | Create several new locations in the store. +newLocs :: Int -> Store -> (Store, [Loc]) +newLocs n store + = let lFirst = storeNextLoc store + lLast = lFirst + n + + locs = [lFirst .. lLast] + store' = store { storeNextLoc = lLast + 1 } + in (store', map Loc locs) + + +-- Regions ------------------------------------------------------------------- +-- | Create a new region in the store. +newRgn :: Store -> (Store, Rgn) +newRgn store + = let rgn = storeNextRgn store + store' = store { storeNextRgn = rgn + 1 + , storeRegions = Set.insert (Rgn rgn) (storeRegions store) } + in (store', Rgn rgn) + + +-- | Create several new regions in the store +newRgns :: Int -> Store -> (Store, [Rgn]) +newRgns 0 store = (store, []) +newRgns count store + = let rgns = map Rgn $ [ storeNextRgn store .. storeNextRgn store + count - 1] + store' = store { storeNextRgn = storeNextRgn store + count + , storeRegions = Set.union (Set.fromList rgns) (storeRegions store) } + in (store', rgns) + + +-- | Delete a region, removing all its bindings. +delRgn :: Rgn -> Store -> Store +delRgn rgn store + = let binds' = [x | x@(_, (r, _, _)) <- Map.toList $ storeBinds store + , r /= rgn ] + in store { storeBinds = Map.fromList binds' + , storeRegions = Set.delete rgn (storeRegions store) + , storeGlobal = Set.delete rgn (storeGlobal store) } + + +-- | Check whether a store contains the given region. +hasRgn :: Store -> Rgn -> Bool +hasRgn store rgn + = Set.member rgn (storeRegions store) + + +-- | Set a region as being global. +setGlobal :: Rgn -> Store -> Store +setGlobal rgn store + = store + { storeGlobal = Set.insert rgn (storeGlobal store) } + + +-- Bindings ------------------------------------------------------------------- +-- | Add a store binding to the store, at the given location. +addBind :: Loc -> Rgn -> Type Name -> SBind -> Store -> Store +addBind loc rgn t sbind store + = store + { storeBinds = Map.insert loc (rgn, t, sbind) (storeBinds store) } + + +-- | Allocate a new binding into the given region, +-- returning the new location. +allocBind :: Rgn -> Type Name -> SBind -> Store -> (Store, Loc) +allocBind rgn t sbind store + = let (store1, loc) = newLoc 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 + rgnBinds = map (\mk -> mk locs) mkSBinds + store2 = foldr (\(l, (r, t, b)) -> addBind l r t b) store1 + $ zip locs rgnBinds + in (store2, locs) + + +-- | Lookup a the binding for a location. +lookupBind :: Loc -> Store -> Maybe SBind +lookupBind loc store + = liftM (\(_, _, sb) -> sb) + $ Map.lookup loc (storeBinds store) + + +-- | Lookup the type of a store location. +lookupTypeOfLoc :: Loc -> Store -> Maybe (Type Name) +lookupTypeOfLoc loc store + = 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) +lookupRegionTypeBind loc store + = Map.lookup loc (storeBinds store) + diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,20 @@ +-------------------------------------------------------------------------------- +The Disciplined Disciple Compiler License (MIT style) + +Copyright (c) 2008-2011 Benjamin Lippmeier + +Permission is hereby granted, free of charge, to any person obtaining a copy +of this software and associated documentation files (the "Software"), to deal +in the Software without restriction, including without limitation the rights +to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in +all copies or substantial portions of the Software. + +-------------------------------------------------------------------------------- +Redistributions of libraries in ./external are governed by their own licenses: + + - TinyPTC GNU Lesser General Public License + diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/ddc-core-eval.cabal b/ddc-core-eval.cabal new file mode 100644 --- /dev/null +++ b/ddc-core-eval.cabal @@ -0,0 +1,60 @@ +Name: ddc-core-eval +Version: 0.2.0.1 +License: MIT +License-file: LICENSE +Author: Ben Lippmeier +Maintainer: benl@ouroborus.net +Build-Type: Simple +Cabal-Version: >=1.6 +Stability: experimental +Category: Compilers/Interpreters +Homepage: http://disciple.ouroborus.net +Bug-reports: disciple@ouroborus.net +Synopsis: Disciple Core language semantic evaluator. +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 + 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. + +Library + Build-Depends: + base == 4.5.*, + containers == 0.4.*, + array == 0.4.*, + transformers == 0.2.*, + mtl == 2.0.*, + ddc-base == 0.2.0.*, + ddc-core == 0.2.0.* + + Exposed-modules: + DDC.Core.Eval.Check + DDC.Core.Eval.Compounds + DDC.Core.Eval.Env + DDC.Core.Eval.Name + DDC.Core.Eval.Prim + DDC.Core.Eval.Step + DDC.Core.Eval.Store + DDC.Core.Eval + + GHC-options: + -Wall + -fno-warn-orphans + -fno-warn-missing-signatures + -fno-warn-unused-do-bind + + Extensions: + ParallelListComp + PatternGuards + RankNTypes + FlexibleContexts + FlexibleInstances + MultiParamTypeClasses + UndecidableInstances + KindSignatures + NoMonomorphismRestriction + ScopedTypeVariables + StandaloneDeriving + DoAndIfThenElse +