Safe Haskell | None |
---|---|
Language | Haskell98 |
Documentation
Effect [*] State | |
type Unit [*] State = [] * | |
type Plus [*] State s t = UnionS s t | |
type Inv [*] State s t = (IsSet s, IsSet (Reads s), IsSet (Writes s), IsSet t, IsSet (Reads t), IsSet (Writes t), (~) [*] (Reads (Reads t)) (Reads t), (~) [*] (Writes (Writes s)) (Writes s), Split (Reads s) (Reads t) (Reads (UnionS s t)), Unionable (Writes s) (Writes t), IntersectR (Writes s) (Reads t), (~) [*] (Writes (UnionS s t)) (UnionS (Writes s) (Writes t))) |
(Show (Var k), Show v) => Show ((:->) k v) | |
Chooser (CmpSymbol j k) => OrdH ((:->) j u) ((:->) k v) | |
(Monoid u, Nubable ((:) * ((:->) k u) s)) => Nubable ((:) * ((:->) k u) ((:) * ((:->) k u) s)) | |
Update ((:) * ((:->) j ((:!) b s)) as) as' => Update ((:) * ((:->) k ((:!) a W)) ((:) * ((:->) j ((:!) b s)) as)) as' | |
Update ((:) * ((:->) k ((:!) a R)) as) as' => Update ((:) * ((:->) k ((:!) a W)) ((:) * ((:->) k ((:!) b R)) as)) as' | |
Update ((:) * ((:->) k ((:!) b R)) as) as' => Update ((:) * ((:->) k ((:!) a s)) ((:) * ((:->) k ((:!) b s)) as)) as' | |
Update ((:) * ((:->) j ((:!) b s)) as) as' => Update ((:) * ((:->) k ((:!) a R)) ((:) * ((:->) j ((:!) b s)) as)) ((:) * ((:->) k ((:!) a R)) as') | |
type Max ((:->) j u) ((:->) k v) = (:->) (Select Symbol j k k j) (Select * j k v u) | |
type Min ((:->) j u) ((:->) k v) = (:->) (Select Symbol j k j k) (Select * j k u v) |
(Show (Action f), Show a) => Show ((:!) a f) | |
Update ((:) * ((:->) j ((:!) b s)) as) as' => Update ((:) * ((:->) k ((:!) a W)) ((:) * ((:->) j ((:!) b s)) as)) as' | |
Update ((:) * ((:->) k ((:!) a R)) as) as' => Update ((:) * ((:->) k ((:!) a W)) ((:) * ((:->) k ((:!) b R)) as)) as' | |
Update ((:) * ((:->) k ((:!) b R)) as) as' => Update ((:) * ((:->) k ((:!) a s)) ((:) * ((:->) k ((:!) b s)) as)) as' | |
Update ((:) * ((:->) j ((:!) b s)) as) as' => Update ((:) * ((:->) k ((:!) a R)) ((:) * ((:->) j ((:!) b s)) as)) ((:) * ((:->) k ((:!) a R)) as') |
type Unionable s t = (Sortable (Append s t), Nubable (Sort (Append s t)) (Nub (Sort (Append s t))), Split s t (Union s t)) Source
type StateSet f = (StateSetProperties f, StateSetProperties (Reads f), StateSetProperties (Writes f)) Source
update
Update xs ([] *) | |
Update ((:) * ((:->) j ((:!) b s)) as) as' => Update ((:) * ((:->) k ((:!) a W)) ((:) * ((:->) j ((:!) b s)) as)) as' | |
Update ((:) * ((:->) k ((:!) a R)) as) as' => Update ((:) * ((:->) k ((:!) a W)) ((:) * ((:->) k ((:!) b R)) as)) as' | |
Update ((:) * ((:->) k ((:!) b R)) as) as' => Update ((:) * ((:->) k ((:!) a s)) ((:) * ((:->) k ((:!) b s)) as)) as' | |
Update ((:) * e ([] *)) ((:) * e ([] *)) | |
Update ((:) * ((:->) j ((:!) b s)) as) as' => Update ((:) * ((:->) k ((:!) a R)) ((:) * ((:->) j ((:!) b s)) as)) ((:) * ((:->) k ((:!) a R)) as') |