changeset 54:9bb7c9bee94f

Trying redefine delta for infinite changes
author Yasutaka Higa Wed, 19 Nov 2014 14:01:17 +0900 1e6fecb54f1f 9c8c09334e32 agda/delta.agda 1 files changed, 27 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
```--- a/agda/delta.agda	Wed Nov 19 13:35:58 2014 +0900
+++ b/agda/delta.agda	Wed Nov 19 14:01:17 2014 +0900
@@ -7,19 +7,42 @@

module delta where

+DeltaLog : Set
+DeltaLog = List String
+
data Delta {l : Level} (A : Set l) : (Set (suc l)) where
-  similar : List String -> A -> List String -> A -> Delta A
+  mono    : DeltaLog -> A -> Delta A
+  delta   : DeltaLog -> A -> Delta A -> Delta A
+
+logAppend : {l : Level} {A : Set l} -> DeltaLog -> Delta A -> Delta A
+logAppend l (mono lx x)    = mono  (l ++ lx) x
+logAppend l (delta lx x d) = delta (l ++ lx) x (logAppend l d)
+
+deltaAppend : {l : Level} {A : Set l} -> Delta A -> Delta A -> Delta A
+deltaAppend (mono lx x) d     = delta lx x d
+deltaAppend (delta lx x d) ds = delta lx x (deltaAppend d ds)
+
+headDelta : {l : Level} {A : Set l} -> Delta A -> Delta A
+headDelta (mono lx x)    = mono lx x
+headDelta (delta lx x _) = mono lx x
+
+tailDelta : {l : Level} {A : Set l} -> Delta A -> Delta A
+tailDelta (mono lx x)   = mono lx x
+tailDelta (delta _ _ d) = d

-- Functor
fmap : {l ll : Level} {A : Set l} {B : Set ll} -> (A -> B) -> (Delta A) -> (Delta B)
-fmap f (similar xs x ys y) = similar xs (f x) ys (f y)
+fmap f (mono lx x)    = mono lx (f x)
+fmap f (delta lx x d) = delta lx (f x) (fmap f d)

mu : {l : Level} {A : Set l} -> Delta (Delta A) -> Delta A
-mu (similar lx (similar llx x _ _) ly (similar _ _ lly y)) = similar (lx ++ llx) x (ly ++ lly) y
+mu (mono ld d)     = logAppend ld d
+mu (delta ld d ds) = deltaAppend (logAppend ld (headDelta d)) (mu (fmap tailDelta ds))

+{-
eta : {l : Level} {A : Set l} -> A -> Delta A
eta x = similar [] x [] x

@@ -164,3 +187,4 @@
≡⟨ refl ⟩
((similar lx x ly y) >>= k) >>= h
∎
+-}```