Skip to content

Commit

Permalink
split module for CESK store
Browse files Browse the repository at this point in the history
  • Loading branch information
kostmo committed Jan 16, 2024
1 parent 3d87e71 commit f6e8bf0
Show file tree
Hide file tree
Showing 4 changed files with 86 additions and 64 deletions.
65 changes: 1 addition & 64 deletions src/swarm-engine/Swarm/Game/CESK.hs
Original file line number Diff line number Diff line change
Expand Up @@ -73,7 +73,6 @@ module Swarm.Game.CESK (
initMachine,
initMachine',
cancel,
resetBlackholes,

-- ** Extracting information
finalValue,
Expand All @@ -85,10 +84,9 @@ import Control.Lens ((^.))
import Control.Lens.Combinators (pattern Empty)
import Data.Aeson (FromJSON, ToJSON)
import Data.Int (Int64)
import Data.IntMap.Strict (IntMap)
import Data.IntMap.Strict qualified as IM
import GHC.Generics (Generic)
import Prettyprinter (Doc, Pretty (..), encloseSep, hsep, (<+>))
import Swarm.Game.CESK.Store
import Swarm.Game.Entity (Count, Entity)
import Swarm.Game.Exception
import Swarm.Game.World (WorldUpdate (..))
Expand Down Expand Up @@ -198,58 +196,6 @@ data Frame
-- | A continuation is just a stack of frames.
type Cont = [Frame]

------------------------------------------------------------
-- Store
------------------------------------------------------------

type Addr = Int

-- | 'Store' represents a store, /i.e./ memory, indexing integer
-- locations to 'MemCell's.
data Store = Store {next :: Addr, mu :: IntMap MemCell}
deriving (Show, Eq, Generic, FromJSON, ToJSON)

-- | A memory cell can be in one of three states.
data MemCell
= -- | A cell starts out life as an unevaluated term together with
-- its environment.
E Term Env
| -- | When the cell is 'Force'd, it is set to a 'Blackhole' while
-- being evaluated. If it is ever referenced again while still
-- a 'Blackhole', that means it depends on itself in a way that
-- would trigger an infinite loop, and we can signal an error.
-- (Of course, we
-- <http://www.lel.ed.ac.uk/~gpullum/loopsnoop.html cannot
-- detect /all/ infinite loops this way>.)
--
-- A 'Blackhole' saves the original 'Term' and 'Env' that are
-- being evaluated; if Ctrl-C is used to cancel a computation
-- while we are in the middle of evaluating a cell, the
-- 'Blackhole' can be reset to 'E'.
Blackhole Term Env
| -- | Once evaluation is complete, we cache the final 'Value' in
-- the 'MemCell', so that subsequent lookups can just use it
-- without recomputing anything.
V Value
deriving (Show, Eq, Generic, FromJSON, ToJSON)

emptyStore :: Store
emptyStore = Store 0 IM.empty

-- | Allocate a new memory cell containing an unevaluated expression
-- with the current environment. Return the index of the allocated
-- cell.
allocate :: Env -> Term -> Store -> (Addr, Store)
allocate e t (Store n m) = (n, Store (n + 1) (IM.insert n (E t e) m))

-- | Look up the cell at a given index.
lookupStore :: Addr -> Store -> Maybe MemCell
lookupStore n = IM.lookup n . mu

-- | Set the cell at a given index.
setStore :: Addr -> MemCell -> Store -> Store
setStore n c (Store nxt m) = Store nxt (IM.insert n c m)

------------------------------------------------------------
-- CESK machine
------------------------------------------------------------
Expand Down Expand Up @@ -337,15 +283,6 @@ cancel cesk = Out VUnit s' []
getStore (Up _ s _) = s
getStore (Waiting _ c) = getStore c

-- | Reset any 'Blackhole's in the 'Store'. We need to use this any
-- time a running computation is interrupted, either by an exception
-- or by a Ctrl+C.
resetBlackholes :: Store -> Store
resetBlackholes (Store n m) = Store n (IM.map resetBlackhole m)
where
resetBlackhole (Blackhole t e) = E t e
resetBlackhole c = c

------------------------------------------------------------
-- Pretty printing CESK machine states
------------------------------------------------------------
Expand Down
82 changes: 82 additions & 0 deletions src/swarm-engine/Swarm/Game/CESK/Store.hs
Original file line number Diff line number Diff line change
@@ -0,0 +1,82 @@
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}

-- |
-- SPDX-License-Identifier: BSD-3-Clause
-- Description: Store for Swarm's CESK interpreter
module Swarm.Game.CESK.Store (
Store,
Addr,
emptyStore,
MemCell (..),
allocate,
lookupStore,
setStore,
resetBlackholes,
) where

import Data.Aeson (FromJSON, ToJSON)
import Data.IntMap.Strict (IntMap)
import Data.IntMap.Strict qualified as IM
import GHC.Generics (Generic)

import Swarm.Language.Syntax
import Swarm.Language.Value as V

type Addr = Int

-- | 'Store' represents a store, /i.e./ memory, indexing integer
-- locations to 'MemCell's.
data Store = Store {next :: Addr, mu :: IntMap MemCell}
deriving (Show, Eq, Generic, FromJSON, ToJSON)

-- | A memory cell can be in one of three states.
data MemCell
= -- | A cell starts out life as an unevaluated term together with
-- its environment.
E Term Env
| -- | When the cell is 'Force'd, it is set to a 'Blackhole' while
-- being evaluated. If it is ever referenced again while still
-- a 'Blackhole', that means it depends on itself in a way that
-- would trigger an infinite loop, and we can signal an error.
-- (Of course, we
-- <http://www.lel.ed.ac.uk/~gpullum/loopsnoop.html cannot
-- detect /all/ infinite loops this way>.)
--
-- A 'Blackhole' saves the original 'Term' and 'Env' that are
-- being evaluated; if Ctrl-C is used to cancel a computation
-- while we are in the middle of evaluating a cell, the
-- 'Blackhole' can be reset to 'E'.
Blackhole Term Env
| -- | Once evaluation is complete, we cache the final 'Value' in
-- the 'MemCell', so that subsequent lookups can just use it
-- without recomputing anything.
V Value
deriving (Show, Eq, Generic, FromJSON, ToJSON)

emptyStore :: Store
emptyStore = Store 0 IM.empty

-- | Allocate a new memory cell containing an unevaluated expression
-- with the current environment. Return the index of the allocated
-- cell.
allocate :: Env -> Term -> Store -> (Addr, Store)
allocate e t (Store n m) = (n, Store (n + 1) (IM.insert n (E t e) m))

-- | Look up the cell at a given index.
lookupStore :: Addr -> Store -> Maybe MemCell
lookupStore n = IM.lookup n . mu

-- | Set the cell at a given index.
setStore :: Addr -> MemCell -> Store -> Store
setStore n c (Store nxt m) = Store nxt (IM.insert n c m)

-- | Reset any 'Blackhole's in the 'Store'. We need to use this any
-- time a running computation is interrupted, either by an exception
-- or by a Ctrl+C.
resetBlackholes :: Store -> Store
resetBlackholes (Store n m) = Store n (IM.map resetBlackhole m)
where
resetBlackhole (Blackhole t e) = E t e
resetBlackhole c = c
1 change: 1 addition & 0 deletions src/swarm-engine/Swarm/Game/Step.hs
Original file line number Diff line number Diff line change
Expand Up @@ -45,6 +45,7 @@ import Prettyprinter (pretty)
import Swarm.Effect as Effect (Time, getNow)
import Swarm.Game.Achievement.Definitions
import Swarm.Game.CESK
import Swarm.Game.CESK.Store
import Swarm.Game.Display
import Swarm.Game.Entity hiding (empty, lookup, singleton, union)
import Swarm.Game.Exception
Expand Down
2 changes: 2 additions & 0 deletions swarm.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -166,6 +166,7 @@ library swarm-engine
Swarm.Game.Achievement.Description
Swarm.Game.Achievement.Persistence
Swarm.Game.CESK
Swarm.Game.CESK.Store
Swarm.Game.Display
Swarm.Game.Entity
Swarm.Game.Entity.Cosmetic
Expand Down Expand Up @@ -431,6 +432,7 @@ library
, Swarm.Game.Achievement.Description
, Swarm.Game.Achievement.Persistence
, Swarm.Game.CESK
, Swarm.Game.CESK.Store
, Swarm.Game.Display
, Swarm.Game.Entity
, Swarm.Game.Entity.Cosmetic
Expand Down

0 comments on commit f6e8bf0

Please sign in to comment.