definition module PView import StdEnv import Data.Void, Data.Error, Data.Either, Text.JSON :: *MyWorld createMyWorld :: *World -> *MyWorld getWorld :: *MyWorld -> *World // ----------------------------------------------------------------------- :: IFun p :== p -> Bool :: Source p r w *env = { get :: p env -> *(MaybeErrorString r, env) , put :: p w env -> *(MaybeErrorString (IFun p), env) } :: PView p` r` w` *env = Source (Source p` r` w` env) | E.r w: Projection (PView p` r w env) (Lens r w r` w`) | E.p: Translation (PView p r` w` env) (p` -> p) & TC p | E.p1 p2: Split (PView p1 r` w` env) (Split p2 r` w`) (p` -> (p1,p2)) & TC p1 & TC p2 | E.p1 r1 w1 p2 r2 w2: Join (PView p1 r1 w1 env) (PView p2 r2 w2 env) (p` -> (p1,p2)) (w` -> (w1,w2)) (r1 r2 -> r`) & TC p1 & TC p2 | E.p1 p2: Union (PView p1 r` w` env) (PView p2 r` w` env) (p` -> Either p1 p2) (p1 r` w` -> IFun p2) (p2 r` w` -> IFun p1) & TC p1 & TC p2 | E.a r w p: PSeq (PView p` a a env) (PView p r w env) (a -> p) (w` -> (a,w)) (a r -> r`) & TC p :: View r w *env :== PView Void r w env :: Lens r w r` w` = { lget :: r -> r` , lput :: r w` -> w } :: Split p r w = { sget :: p r -> r , sput :: p r w -> (w, IFun p) } fixP :: (PView p r w *env) p -> View r w *env | TC p applyLens :: (PView p a a *env) (Lens a a r` w`) -> PView p r` w` *env applySplit :: (PView p1 r w *env) (Split p2 r w) (p->(p1,p2)) -> (PView p r w *env) | TC p1 & TC p2 applyTranslation :: (PView p1 r w *env) (p2 -> p1) -> (PView p2 r w *env) | TC p1 & TC p2 join :: (PView p1 r1 w1 *env) (PView p2 r2 w2 *env) -> (PView (p1,p2) (r1,r2) (w1,w2) *env) | TC p1 & TC p2 union :: (PView p1 r w *env) (PView p2 r w *env) (p1 r w -> IFun p2) (p2 r w -> IFun p1) -> (PView (Either p1 p2) r w *env) | TC p1 & TC p2 pseq :: (PView p a a *env) (PView p` r2 w2 *env) (a -> p`) (w -> (a,w2)) (a r2 -> r) -> (PView p r w *env) | TC p` tr1 :: a -> (Void, a) tr2 :: (a,b) -> (a,b) tr3 :: (a,b,c) -> ((a,b),c) tr4 :: (a,b,c,d) -> (((a,b),c),d) // ----------------------------------------------------------------------- get :: (View r w *MyWorld) *MyWorld -> *(MaybeErrorString r, *MyWorld) put :: (View r w *MyWorld) w *MyWorld -> *(MaybeErrorString Void, *MyWorld) class registerForNotification env :: (PView p r w *env) p String *env -> *env | TC p instance registerForNotification MyWorld // ----------------------------------------------------------------------- createMemoryView :: a *MyWorld -> *(PView Void a a MyWorld, *MyWorld) | JSONEncode{|*|} a & JSONDecode{|*|} a createStoreView :: String a -> (PView Void a a MyWorld) | JSONEncode{|*|} a & JSONDecode{|*|} a