implementation module PView import StdEnv, StdDebug import Data.Void, Data.Tuple, Data.Error, Data.Func, Data.Either, Text.JSON, Data.List import System.File, System.Time, Crypto.Hash.MD5 import graph_to_sapl_string from Data.Map import :: Map from Data.Set import :: Set import qualified Data.Map as Map import qualified Data.Set as Set println :: !a !*MyWorld -> *MyWorld | toString a println msg iw=:{world} # (console,world) = stdio world # console = fwrites (toString msg) console # console = fwrites "\n" console # (_,world) = fclose console world = {iw & world = world} getDescriptor :: !a -> VIEWID getDescriptor a = md5 (graph_to_sapl_string a) geq a b = graph_to_sapl_string a == graph_to_sapl_string b gt a b = trace_n (graph_to_sapl_string a) b genID world=:{nextid} = (nextid, {world & nextid = nextid + 1}) // ----------------------------------------------------------------------- :: VIEWID :== String // Notificication request :: NRequest = { nreqid :: Int , target :: VIEWID , param :: Dynamic , handler :: *MyWorld -> *MyWorld } /* eventsource: The id of the source node of the write (top layer) origin: The id of the node of the original notification request target: The id of the node the notification is attached For the node you reqest for a notification "target == origin". But there are many request generated automatically for the lower layers. For those "target <> origin" A notification must be triggered: viewid: the node we are currently processing 1. if the origin and eventsource is the same: ----- | 1 | | 2 | <- eventsource, origin | 3 | | 4 | | 5 | ----- trigger: target == viewid && target == origin 2. if the origin is below eventsource in the graph ----- | 1 | | 2 | <- eventsource | 3 | | 4 | <- origin | 5 | ----- trigger: target == viewid && target == origin 3. if eventsource is below the origin ----- | 1 | | 2 | <- origin | 3 | | 4 | <- eventsource | 5 | ----- trigger: target == viewid && target == eventsource UPDATE: counterexample (origin and eventsource are in two different branches) ----- | 1 | | 2 | <- origin | 3 | --- | 4 |--------|6] <- eventsource | 5 | --- ----- */ :: *MyWorld = { sdsmem :: Map Int JSONNode , sdsstore :: Map String JSONNode , notification :: [NRequest] , nextid :: Int , world :: *World } createMyWorld :: *World -> *MyWorld createMyWorld world = {MyWorld | sdsmem = 'Map'.newMap, sdsstore = 'Map'.newMap, notification = [], nextid = 1, world = world} getWorld :: *MyWorld -> *World getWorld {world} = world // ----------------------------------------------------------------------- :: IFun p :== p -> Bool :: IFunIO p *env :== p env -> *(Bool, env) :: Source p r w *env = { get :: p env -> *(MaybeErrorString r, env) , put :: p w env -> *(MaybeErrorString (IFun p), 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) } applyLens :: (PView p a a *env) (Lens a a r` w`) -> PView p r` w` *env applyLens pview lens = Projection pview lens fixP :: (PView p r w *env) p -> View r w *env | TC p fixP pview p = Translation pview (const p) applySplit :: (PView p1 r w *env) (Split p2 r w) (p->(p1,p2)) -> (PView p r w *env) | TC p1 & TC p2 applySplit pview split tr = Split pview split tr applyTranslation :: (PView p1 r w *env) (p2 -> p1) -> (PView p2 r w *env) | TC p1 & TC p2 applyTranslation pview tr = Translation pview tr join :: (PView p1 r1 w1 *env) (PView p2 r2 w2 *env) -> (PView (p1,p2) (r1,r2) (w1,w2) *env) | TC p1 & TC p2 join pview1 pview2 = Join pview1 pview2 id id tuple 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 union pview1 pview2 ifun1 ifun2 = Union pview1 pview2 id ifun1 ifun2 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` pseq pview1 pview2 trp trw trr = PSeq pview1 pview2 trp trw trr // These can be encoded as a type class if we have functional dependencies... tr1 :: a -> (Void, a) tr1 a = (Void, a) tr2 :: (a,b) -> (a,b) tr2 (a,b) = (a,b) tr3 :: (a,b,c) -> ((a,b),c) tr3 (a,b,c) = ((a,b), c) tr4 :: (a,b,c,d) -> (((a,b),c),d) tr4 (a,b,c,d) = (((a,b), c),d) // ----------------------------------------------------------------------- get :: (View r w *MyWorld) *MyWorld -> *(MaybeErrorString r, *MyWorld) get pview env = get` pview Void env // TODO: return "read cache" get` :: (PView p r w *env) p *env -> *(MaybeErrorString r, *env) get` (Source {get}) p env = get p env get` (Projection pview` {lget}) p env # (ret, env) = get` pview` p env = (fmap lget ret, env) get` (Translation pview` tr) p env = get` pview` (tr p) env get` (Split pview` {sget} tr) p env # (p1, p2) = tr p # (ret, env) = get` pview` p1 env = (fmap (sget p2) ret, env) get` (Join pview1 pview2 trp trw trr) p env # (p1, p2) = trp p # (ret1, env) = get` pview1 p1 env | isError ret1 = (Error (fromError ret1), env) # (ret2, env) = get` pview2 p2 env | isError ret2 = (Error (fromError ret2), env) = (Ok (trr (fromOk ret1) (fromOk ret2)), env) get` (Union pview1 pview2 trp _ _) p env = case trp p of Left p1 = get` pview1 p1 env Right p2 = get` pview2 p2 env get` (PSeq pview1 pview2 trp trw trr) p env = case get` pview1 p env of (Error msg, env) = (Error msg, env) (Ok r1, env) = case get` pview2 (trp r1) env of (Error msg, env) = (Error msg, env) (Ok r2, env) = (Ok (trr r1 r2), env) put :: (View r w *MyWorld) w *MyWorld -> *(MaybeErrorString Void, *MyWorld) put pview w env = case put` pview Void w env of (Error msg, _, myworld) = (Error msg, myworld) (Ok _, ns, myworld) # myworld = notificateAll ns myworld = (Ok Void, myworld) // Notification event :: NEvent = E.p: NEvent VIEWID (IFunIO p *MyWorld) & TC p nevent d ifun = NEvent (getDescriptor d) ifun wrapIO ifun p env = (ifun p, env) put` :: (PView p r w *MyWorld) p w *MyWorld -> (MaybeErrorString (IFunIO p *MyWorld), [NEvent], *MyWorld) | TC p put` d=:(Source pview) p wval myworld = case pview.put p wval myworld of (Error msg, myworld) = (Error msg, [], myworld) (Ok ifun, myworld) # ifun` = wrapIO ifun = (Ok ifun`, [nevent d ifun`], myworld) put` d=:(Projection pview {lput}) p wval env = case get` pview p env of (Error msg, env) = (Error msg, [], env) (Ok rval, env) = case put` pview p (lput rval wval) env of (Error msg, _, env) = (Error msg, [], env) (Ok ifun, ns, env) = (Ok ifun, [nevent d ifun: ns], env) put` d=:(Translation pview tr) p wval env = case put` pview (tr p) wval env of (Error msg, _, env) = (Error msg, [], env) (Ok ifun, ns, env) # ifun` = \p env -> ifun (tr p) env = (Ok ifun`, [nevent d ifun`: ns], env) put` d=:(Split pview {sput} trp) p wval env = case get` pview p1 env of (Error msg, env) = (Error msg, [], env) (Ok rval, env) # (wval, ifun2) = sput p2 rval wval = case put` pview p1 wval env of (Error msg, _, env) = (Error msg, [], env) (Ok ifun1, ns, env) # ifun` = genifun ifun1 (wrapIO ifun2) = (Ok ifun`, [nevent d ifun`: ns], env) where genifun ifun1 ifun2 p env = genifun` ifun1 ifun2 (trp p) env // TODO: verify notification condition genifun` ifun1 ifun2 (p1`,p2`) env | geq p1 p1` = ifun2 p2` env = ifun1 p1` env (p1, p2) = trp p put` d=:(Join pview1 pview2 trp trw _) p wval env = case put` pview1 p1 w1 env of (Error msg, _, env) = (Error msg, [], env) (Ok ifun1, ns1, env) = case put` pview2 p2 w2 env of (Error msg, _, env) = (Error msg, [], env) (Ok ifun2, ns2, env) # ifun` = genifun ifun1 ifun2 = (Ok ifun`, [nevent d ifun`: ns1++ns2], env) where genifun ifun1 ifun2 p env = genifun` ifun1 ifun2 (trp p) env genifun` ifun1 ifun2 (p1,p2) env = case ifun1 p1 env of (False, env) = ifun2 p2 env (True, env) = (True, env) (p1, p2) = trp p (w1, w2) = trw wval put` d=:(Union pview1 pview2 trp ifunl ifunr) p wval env = case trp p of Left p1 = case get` pview1 p1 env of (Error msg, env) = (Error msg, [], env) (Ok rval, env) = case put` pview1 p1 wval env of (Error msg, _, env) = (Error msg, [], env) (Ok ifun, ns, env) # ifun` = genifun (wrapIO (ifunl p1 rval wval)) ifun = (Ok ifun`, [nevent d ifun`: ns], env) Right p2 = case get` pview2 p2 env of (Error msg, env) = (Error msg, [], env) (Ok rval, env) = case put` pview2 p2 wval env of (Error msg, _, env) = (Error msg, [], env) (Ok ifun, ns, env) # ifun` = genifun ifun (wrapIO (ifunr p2 rval wval)) = (Ok ifun`, [nevent d ifun`: ns], env) where genifun ifun1 ifun2 p env = case trp p of (Left p1) = ifun2 p1 env (Right p2) = ifun1 p2 env put` d=:(PSeq pview1 pview2 trp trw trr) p wval env # (w1, w2) = trw wval = case put` pview1 p w1 env of (Error msg, _, env) = (Error msg, [], env) (Ok ifun1, ns1, env) = case put` pview2 (trp w1) w2 env of (Error msg, _, env) = (Error msg, [], env) (Ok ifun2, ns2, env) # ifun` = genifun ifun1 ifun2 = (Ok ifun`, [nevent d ifun`: ns1++ns2], env) where genifun ifun1 ifun2 p env = case ifun1 p env of (False, env) = case get` pview1 p env of (Error msg, env) = (True, env) (Ok rval, env) = ifun2 (trp rval) env (True, env) = (True, env) notificateAll :: [NEvent] *MyWorld -> *MyWorld notificateAll ns myworld=:{MyWorld|notification} # (myworld,_,ds) = foldl notificate (myworld,'Set'.newSet,[]) ns = {myworld & notification = filter (\{nreqid} -> not (isMember nreqid ds)) notification} where notificate st (NEvent viewid invalidator) = foldl geninv st notification where geninv (myworld,s,ds) {nreqid, target, handler, param} | target == viewid && 'Set'.notMember nreqid s = case param of (qr :: qr^) = case invalidator qr myworld of (False, myworld) = (myworld, 'Set'.insert nreqid s, ds) (True, myworld) = (handler myworld, 'Set'.insert nreqid s, [nreqid:ds]) = (myworld, 'Set'.insert nreqid s, ds) geninv a _ = a class registerForNotification env :: (PView p r w *env) p String *env -> *env | TC p instance registerForNotification MyWorld where registerForNotification pview p msg myworld=:{MyWorld|notification} # (nreqid, myworld) = genID myworld # (lowerids, myworld) = collectIds pview p myworld # lowerLayers = [createRequest viewid dynparam nreqid \\ (viewid, dynparam) <- lowerids] = {MyWorld | myworld & notification = [createRequest (getDescriptor pview) (dynamic p) nreqid:tl lowerLayers ++ notification]} where createRequest target param nreqid = { nreqid = nreqid , target = target , param = param , handler = println ("Notification: "+++msg) } collectIds :: (PView p r w *MyWorld) p *MyWorld -> *([(VIEWID, Dynamic)], *MyWorld) | TC p collectIds d=:(Source _) p myworld = ([(getDescriptor d, dynamic p)], myworld) collectIds d=:(Projection pview _) p myworld = let (ids, myworld`) = collectIds pview p myworld in ([(getDescriptor d, dynamic p):ids], myworld`) collectIds d=:(Translation pview tr) p myworld = let (ids, myworld`) = collectIds pview (tr p) myworld in ([(getDescriptor d, dynamic p):ids], myworld`) collectIds d=:(Split pview split trp) p myworld = let (ids, myworld`) = collectIds pview (fst (trp p)) myworld in ([(getDescriptor d, dynamic p):ids], myworld`) collectIds d=:(Join pview1 pview2 trp _ _) p myworld # (ids1, myworld) = collectIds pview1 p1 myworld # (ids2, myworld) = collectIds pview2 p2 myworld = ([(getDescriptor d, dynamic p):ids1 ++ ids2], myworld) where (p1, p2) = trp p collectIds d=:(Union pview1 pview2 trp _ _) p myworld = case trp p of Left p1 = let (ids, myworld`) = collectIds pview1 p1 myworld in ([(getDescriptor d, dynamic p):ids], myworld`) Right p2 = let (ids, myworld`) = collectIds pview2 p2 myworld in ([(getDescriptor d, dynamic p):ids], myworld`) collectIds d=:(PSeq pview1 pview2 trp _ _) p myworld # (ids1, myworld) = collectIds pview1 p myworld # (Ok rval, myworld) = get` pview1 p myworld # (ids2, myworld) = collectIds pview2 (trp rval) myworld = ([(getDescriptor d, dynamic p):ids1 ++ ids2], myworld) // ----------------------------------------------------------------------- createMemoryView :: a *MyWorld -> *(PView Void a a MyWorld, *MyWorld) | JSONEncode{|*|} a & JSONDecode{|*|} a createMemoryView val myworld=:{sdsmem} # (memid, myworld) = genID myworld # sds = Source {Source | get = get` memid, put = put` memid} = (sds, {myworld & sdsmem = 'Map'.put memid (toJSON val) sdsmem}) where get` memid Void myworld=:{sdsmem} = case 'Map'.get memid sdsmem of (Just json) = case fromJSON json of (Just val) = (Ok val, myworld) Nothing = (Error "E2", myworld) Nothing = (Error "E1", myworld) put` memid Void val myworld=:{sdsmem} = (Ok (const True), {myworld & sdsmem = 'Map'.put memid (toJSON val) sdsmem}) createStoreView :: String a -> (PView Void a a MyWorld) | JSONEncode{|*|} a & JSONDecode{|*|} a createStoreView name def = Source {Source | get = get` name def, put = put` name} where get` name def Void myworld=:{sdsstore} = case 'Map'.get name sdsstore of (Just json) = case fromJSON json of (Just val) = (Ok val, myworld) Nothing = (Error "E2", myworld) Nothing = (Ok def, myworld) put` name Void val myworld=:{sdsstore} = (Ok (const True), {myworld & sdsstore = 'Map'.put name (toJSON val) sdsstore})