ddc-core-eval (empty) → 0.2.0.1
raw patch · 11 files changed
+1873/−0 lines, 11 filesdep +arraydep +basedep +containerssetup-changed
Dependencies added: array, base, containers, ddc-base, ddc-core, mtl, transformers
Files
- DDC/Core/Eval.hs +15/−0
- DDC/Core/Eval/Check.hs +204/−0
- DDC/Core/Eval/Compounds.hs +162/−0
- DDC/Core/Eval/Env.hs +204/−0
- DDC/Core/Eval/Name.hs +245/−0
- DDC/Core/Eval/Prim.hs +177/−0
- DDC/Core/Eval/Step.hs +545/−0
- DDC/Core/Eval/Store.hs +239/−0
- LICENSE +20/−0
- Setup.hs +2/−0
- ddc-core-eval.cabal +60/−0
+ DDC/Core/Eval.hs view
@@ -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+
+ DDC/Core/Eval/Check.hs view
@@ -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+
+ DDC/Core/Eval/Compounds.hs view
@@ -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+++
+ DDC/Core/Eval/Env.hs view
@@ -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+
+ DDC/Core/Eval/Name.hs view
@@ -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+
+ DDC/Core/Eval/Prim.hs view
@@ -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+
+ DDC/Core/Eval/Step.hs view
@@ -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+
+ DDC/Core/Eval/Store.hs view
@@ -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)+
+ LICENSE view
@@ -0,0 +1,20 @@+--------------------------------------------------------------------------------+The Disciplined Disciple Compiler License (MIT style)++Copyright (c) 2008-2011 Benjamin Lippmeier++Permission is hereby granted, free of charge, to any person obtaining a copy+of this software and associated documentation files (the "Software"), to deal+in the Software without restriction, including without limitation the rights+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell+copies of the Software, and to permit persons to whom the Software is+furnished to do so, subject to the following conditions:++The above copyright notice and this permission notice shall be included in+all copies or substantial portions of the Software.++--------------------------------------------------------------------------------+Redistributions of libraries in ./external are governed by their own licenses:++ - TinyPTC GNU Lesser General Public License+
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ ddc-core-eval.cabal view
@@ -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+