← Back to branch summary

~ubuntu-branches/ubuntu/wily/agda/wily-proposed

« back to all changes in this revision

Viewing changes to src/full/Agda/Utils/Update.hs

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 06:38:12 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805063812-io8e77niomivhd49
Tags: 2.4.0.2-1
* [6e140ac] Imported Upstream version 2.4.0.2
* [2049fc8] Update Build-Depends to match control
* [93dc4d4] Install the new primitives
* [e48f40f] Fix typo dev→doc

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/full/Agda/Utils/Update.hs
2
2
module Agda.Utils.Update
3
3
  ( Change
4
4
  , MonadChange(..)
 
5
  , runChange
5
6
  , Updater
6
7
  , sharing
7
8
  , runUpdater
18
19
 
19
20
import Data.Traversable (Traversable(..), traverse)
20
21
 
21
 
import Data.Monoid
 
22
import Agda.Utils.Tuple
22
23
 
23
24
-- * Change monad.
24
25
 
47
48
type EndoFun a = a -> a
48
49
type Updater a = a -> Change a
49
50
 
50
 
 
51
 
 
52
 
type Change = Identity
53
 
 
54
 
{-# INLINE sharing #-}
55
 
sharing :: Updater a -> Updater a
56
 
sharing f a = f a
57
 
 
58
 
{-# INLINE runUpdater #-}
59
 
runUpdater :: Updater a -> EndoFun a
60
 
runUpdater f a = runIdentity (f a)
61
 
 
62
 
{-# INLINE dirty #-}
63
 
dirty :: Updater a
64
 
dirty = Identity
65
 
 
66
 
{-# INLINE ifDirty #-}
67
 
ifDirty :: Identity a -> (a -> Identity b) -> (a -> Identity b) -> Identity b
68
 
ifDirty m f g = m >>= f
69
 
 
70
 
 
71
 
{- UNCOMMENT this if you want Q-combinators that do something
72
 
 
73
51
-- BEGIN REAL STUFF
74
52
 
75
53
-- | The @Change@ monad.
88
60
    (a, Any dirty) <- listen (fromChange m)
89
61
    return (a, dirty)
90
62
 
91
 
 
92
 
sharing :: Updater a -> Updater a
93
 
sharing f a = do
94
 
  (a', changed) <- listenDirty $ f a
95
 
  return $ if changed then a' else a
96
 
 
97
 
runUpdater :: Updater a -> EndoFun a
98
 
runUpdater f a = fst $ runWriter $ fromChange $ sharing f a
 
63
-- | Run a 'Change' computation, returning result plus change flag.
 
64
runChange :: Change a -> (a, Bool)
 
65
runChange = mapSnd getAny . runWriter . fromChange
 
66
 
 
67
-- | Blindly run an updater.
 
68
runUpdater :: Updater a -> a -> (a, Bool)
 
69
runUpdater f a = runChange $ f a
99
70
 
100
71
-- | Mark a computation as dirty.
101
72
dirty :: Updater a
113
81
  (a, dirty) <- listenDirty m
114
82
  if dirty then f a else g a
115
83
 
 
84
-- * Proper updater (Q-combinators)
 
85
 
 
86
-- | Replace result of updating with original input if nothing has changed.
 
87
sharing :: Updater a -> Updater a
 
88
sharing f a = do
 
89
  (a', changed) <- listenDirty $ f a
 
90
  return $ if changed then a' else a
 
91
 
 
92
-- | Eval an updater (using 'sharing').
 
93
evalUpdater :: Updater a -> EndoFun a
 
94
evalUpdater f a = fst $ runWriter $ fromChange $ sharing f a
 
95
 
116
96
-- END REAL STUFF
117
 
-}
118
97
 
119
98
-- * Updater transformer classes
120
99
 
128
107
 
129
108
  updater1   = traverse
130
109
  updates1 f = sharing $ updater1 f
131
 
  update1  f = runUpdater $ updater1 f
 
110
  update1  f = evalUpdater $ updater1 f
132
111
 
133
112
instance Updater1 Maybe where
134
113
 
145
124
  update2  :: Updater a -> Updater b -> EndoFun (f a b)
146
125
 
147
126
  updates2 f1 f2 = sharing $ updater2 f1 f2
148
 
  update2  f1 f2 = runUpdater $ updater2 f1 f2
 
127
  update2  f1 f2 = evalUpdater $ updater2 f1 f2
149
128
 
150
129
instance Updater2 (,) where
151
130
  updater2 f1 f2 (a,b) = (,) <$> sharing f1 a <*> sharing f2 b
154
133
  updater2 f1 f2 (Left a)  = Left <$> f1 a
155
134
  updater2 f1 f2 (Right b) = Right <$> f2 b
156
135
 
 
136
 
 
137
{-- BEGIN MOCK
 
138
 
 
139
-- * Mock updater
 
140
 
 
141
type Change = Identity
 
142
 
 
143
-- | Replace result of updating with original input if nothing has changed.
 
144
{-# INLINE sharing #-}
 
145
sharing :: Updater a -> Updater a
 
146
sharing f a = f a
 
147
 
 
148
-- | Run an updater.
 
149
{-# INLINE evalUpdater #-}
 
150
evalUpdater :: Updater a -> EndoFun a
 
151
evalUpdater f a = runIdentity (f a)
 
152
 
 
153
-- | Mark a computation as dirty.
 
154
{-# INLINE dirty #-}
 
155
dirty :: Updater a
 
156
dirty = Identity
 
157
 
 
158
{-# INLINE ifDirty #-}
 
159
ifDirty :: Identity a -> (a -> Identity b) -> (a -> Identity b) -> Identity b
 
160
ifDirty m f g = m >>= f
 
161
 
 
162
-- END MOCK -}