mirror of
https://github.com/danelahman/haskell-coop.git
synced 2024-09-19 06:17:58 +03:00
Documentation
This commit is contained in:
parent
d7911e0627
commit
97e8ac2c26
@ -124,10 +124,6 @@ intMLCoOps (Assign r x) =
|
||||
intMLRunner :: Runner '[IntMLState] sig Heap
|
||||
intMLRunner = mkRunner intMLCoOps
|
||||
|
||||
--
|
||||
-- Top-Level running of the ML-style memory.
|
||||
--
|
||||
|
||||
-- | Initialiser for the runner `intMlRunner` that
|
||||
-- initialises the heap with the empty partial map,
|
||||
-- and sets the next address to be allocated to @Z@.
|
||||
|
@ -4,69 +4,83 @@
|
||||
{-# LANGUAGE KindSignatures #-}
|
||||
{-# LANGUAGE TypeFamilies #-}
|
||||
|
||||
--
|
||||
-- Integer-valued state with scoped allocation implemented using runners.
|
||||
--
|
||||
{-|
|
||||
Module : Control.FPState
|
||||
Description : Runner for integer-valued global state, using effect typing to ensure that only a given footprint is accessed
|
||||
Copyright : (c) Danel Ahman, 2019
|
||||
License : MIT
|
||||
Maintainer : danel.ahman@eesti.ee
|
||||
Stability : experimental
|
||||
|
||||
This module implements a runner that provides access to
|
||||
integer-valued global state indexed by memory size (with
|
||||
n-many locations, all storing integers).
|
||||
|
||||
We use effect typing to ensure that only locations in a
|
||||
given footprint are allowed to be accessed. Specifically,
|
||||
the `State` effect that this module provides is indexed by
|
||||
a footprint, the size of the memory, specifying how many
|
||||
locations/addresses are present, and thus can be accessed.
|
||||
-}
|
||||
module Control.Runner.IntState (
|
||||
Nat(..), Addr(..),
|
||||
State(..), get, put,
|
||||
Memory, withNewRef, runSt
|
||||
Memory, stRunner, withNewRef, runSt
|
||||
) where
|
||||
|
||||
import Control.Runner
|
||||
import System.IO
|
||||
|
||||
--
|
||||
-- Datatypes of natural numbers (for memory size).
|
||||
--
|
||||
-- | Type of natural numbers that we use for the size of the memory.
|
||||
data Nat where
|
||||
Z :: Nat
|
||||
S :: Nat -> Nat
|
||||
|
||||
--
|
||||
-- Datatype of addresses in a memory of given size.
|
||||
--
|
||||
-- | Type of memory addresses of a given size.
|
||||
data Addr :: Nat -> * where
|
||||
AZ :: Addr (S n)
|
||||
AS :: Addr n -> Addr (S n)
|
||||
|
||||
--
|
||||
-- Signature of the state effect for 0..memsize-1 references.
|
||||
--
|
||||
-- For simplicity, storing only integers.
|
||||
--
|
||||
-- | An memory size indexed effect for reading the value stored at
|
||||
-- a given memory address, and writing a value to a given memory address.
|
||||
data State (memsize :: Nat) :: * -> * where
|
||||
-- | Algebraic operation for reading the value stored at a given memory address.
|
||||
Get :: Addr memsize -> State memsize Int
|
||||
-- | Algebraic operation for writing the value to a given memory address.
|
||||
Put :: Addr memsize -> Int -> State memsize ()
|
||||
|
||||
--
|
||||
-- Generic effects.
|
||||
--
|
||||
-- | Generic effect for reading the value stored at a given memory address.
|
||||
get :: Addr memsize -> User '[State memsize] Int
|
||||
get addr = performU (Get addr)
|
||||
|
||||
-- | Generic effect for writing the value to a given memory address.
|
||||
put :: Addr memsize -> Int -> User '[State memsize] ()
|
||||
put addr x = performU (Put addr x)
|
||||
|
||||
--
|
||||
-- ST runner for memsize-many references
|
||||
--
|
||||
-- | The type of the runtime state of the runner `stRunner`.
|
||||
type Memory = Int
|
||||
|
||||
-- | The co-operations of the runner `stRunner`.
|
||||
stCoOps :: State (S memsize) a -> Kernel '[State memsize] Memory a
|
||||
stCoOps (Get AZ) = getEnv
|
||||
stCoOps (Get (AS addr)) = performK (Get addr)
|
||||
stCoOps (Put AZ x) = setEnv x
|
||||
stCoOps (Put (AS addr) x) = performK (Put addr x)
|
||||
|
||||
-- | Runner that implements the effect @State (S memsize)@
|
||||
-- in an external context that provides the @State memsize@ effect.
|
||||
--
|
||||
-- The intuition is that every time we call `run` with `stRunner`,
|
||||
-- we allocate a new "fresh" memory address. Internally then
|
||||
-- this runner keeps only the value of the most recently
|
||||
-- allocated memory address in its runtime state, and
|
||||
-- delegates `Get` and `Put` operations to all other
|
||||
-- addresses to some enveloping runner (implementing @State memsize@).
|
||||
stRunner :: Runner '[State (S memsize)] '[State memsize] Memory
|
||||
stRunner = mkRunner stCoOps
|
||||
|
||||
--
|
||||
-- Derived with-new-ref construct, which extends the memory
|
||||
-- with a new reference initialized to the given value init.
|
||||
--
|
||||
-- | Derived programming construct for running user code that
|
||||
-- has access to one additional (freshly generated) memory address.
|
||||
withNewRef :: Int
|
||||
-> User '[State (S memsize)] a
|
||||
-> User '[State memsize] a
|
||||
|
Loading…
Reference in New Issue
Block a user