Mercurial > hg > Members > atton > delta_monad

comparison agda/delta.agda @ 54:9bb7c9bee94f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Trying redefine delta for infinite changes
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Wed, 19 Nov 2014 14:01:17 +0900
parents 90b171e3a73e
children 9c8c09334e32
comparison
equal deleted inserted replaced
53:1e6fecb54f1f 54:9bb7c9bee94f
5 open import Relation.Binary.PropositionalEquality 5 open import Relation.Binary.PropositionalEquality
6 open ≡-Reasoning 6 open ≡-Reasoning
7 7
8 module delta where 8 module delta where
9 9
10 DeltaLog : Set
11 DeltaLog = List String
12
10 data Delta {l : Level} (A : Set l) : (Set (suc l)) where 13 data Delta {l : Level} (A : Set l) : (Set (suc l)) where
11 similar : List String -> A -> List String -> A -> Delta A 14 mono : DeltaLog -> A -> Delta A
15 delta : DeltaLog -> A -> Delta A -> Delta A
16
17 logAppend : {l : Level} {A : Set l} -> DeltaLog -> Delta A -> Delta A
18 logAppend l (mono lx x) = mono (l ++ lx) x
19 logAppend l (delta lx x d) = delta (l ++ lx) x (logAppend l d)
20
21 deltaAppend : {l : Level} {A : Set l} -> Delta A -> Delta A -> Delta A
22 deltaAppend (mono lx x) d = delta lx x d
23 deltaAppend (delta lx x d) ds = delta lx x (deltaAppend d ds)
24
25 headDelta : {l : Level} {A : Set l} -> Delta A -> Delta A
26 headDelta (mono lx x) = mono lx x
27 headDelta (delta lx x _) = mono lx x
28
29 tailDelta : {l : Level} {A : Set l} -> Delta A -> Delta A
30 tailDelta (mono lx x) = mono lx x
31 tailDelta (delta _ _ d) = d
12 32
13 33
14 -- Functor 34 -- Functor
15 fmap : {l ll : Level} {A : Set l} {B : Set ll} -> (A -> B) -> (Delta A) -> (Delta B) 35 fmap : {l ll : Level} {A : Set l} {B : Set ll} -> (A -> B) -> (Delta A) -> (Delta B)
16 fmap f (similar xs x ys y) = similar xs (f x) ys (f y) 36 fmap f (mono lx x) = mono lx (f x)
37 fmap f (delta lx x d) = delta lx (f x) (fmap f d)
17 38
18 39
19 -- Monad (Category) 40 -- Monad (Category)
20 mu : {l : Level} {A : Set l} -> Delta (Delta A) -> Delta A 41 mu : {l : Level} {A : Set l} -> Delta (Delta A) -> Delta A
21 mu (similar lx (similar llx x _ _) ly (similar _ _ lly y)) = similar (lx ++ llx) x (ly ++ lly) y 42 mu (mono ld d) = logAppend ld d
43 mu (delta ld d ds) = deltaAppend (logAppend ld (headDelta d)) (mu (fmap tailDelta ds))
22 44
45 {-
23 eta : {l : Level} {A : Set l} -> A -> Delta A 46 eta : {l : Level} {A : Set l} -> A -> Delta A
24 eta x = similar [] x [] x 47 eta x = similar [] x [] x
25 48
26 returnS : {l : Level} {A : Set l} -> A -> Delta A 49 returnS : {l : Level} {A : Set l} -> A -> Delta A
27 returnS x = similar [[ (show x) ]] x [[ (show x) ]] x 50 returnS x = similar [[ (show x) ]] x [[ (show x) ]] x
162 ≡⟨ refl ⟩ 185 ≡⟨ refl ⟩
163 (mu (fmap k (similar lx x ly y))) >>= h 186 (mu (fmap k (similar lx x ly y))) >>= h
164 ≡⟨ refl ⟩ 187 ≡⟨ refl ⟩
165 ((similar lx x ly y) >>= k) >>= h 188 ((similar lx x ly y) >>= k) >>= h
166 ∎ 189 ∎
190 -}