# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1423989860 -32400
# Node ID 957496efbe5d7841e3656d219cb6659a6aab7e4b
# Parent  160a86e97a54a19024e4683b8a34ae32ab429a6f# Parent  1f218e2d9de01b323b759eb78d16ddeacd65471e
Merge some commits

diff -r 160a86e97a54 -r 957496efbe5d agda/delta.agda
--- a/agda/delta.agda	Sun Feb 15 17:42:58 2015 +0900
+++ b/agda/delta.agda	Sun Feb 15 17:44:20 2015 +0900
@@ -54,4 +54,4 @@
         (x : Delta A n) -> (f : A -> (Delta B n)) -> (Delta B n)
 d >>= f = delta-bind d f
 
--}
\ No newline at end of file
+-}
diff -r 160a86e97a54 -r 957496efbe5d agda/delta/monad.agda
--- a/agda/delta/monad.agda	Sun Feb 15 17:42:58 2015 +0900
+++ b/agda/delta/monad.agda	Sun Feb 15 17:44:20 2015 +0900
@@ -10,11 +10,6 @@
 
 module delta.monad where
 
-tailDelta-is-nt : {l : Level} {A B : Set l} {n : Nat}
-                  (f : A -> B) -> (d : Delta A (S (S n))) ->
-                  (tailDelta {n = n} ∙ (delta-fmap f)) d ≡ ((delta-fmap f) ∙ tailDelta {n = n}) d
-tailDelta-is-nt f (delta x d) = refl
-
 
 tailDelta-to-tail-nt : {l : Level} {A B : Set l} (n m  : Nat)
                        (f : A -> B) (d : Delta (Delta A (S (S m))) (S n)) ->
@@ -40,7 +35,6 @@
 delta-eta-is-nt : {l : Level} {A B : Set l} -> {n : Nat}
                   (f : A -> B) -> (x : A) -> (delta-eta {n = n} ∙ f) x ≡ delta-fmap f (delta-eta x)
 delta-eta-is-nt {n = O}   f x = refl
-delta-eta-is-nt {n = S O} f x = refl
 delta-eta-is-nt {n = S n} f x = begin
   (delta-eta ∙ f) x                        ≡⟨ refl ⟩
   delta-eta (f x)                          ≡⟨ refl ⟩
@@ -75,10 +69,10 @@
     (delta-fmap delta-mu
      (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta ds)))
   ∎
-delta-fmap-mu-to-tail (S n) (S n₁) (delta (delta (delta x (delta xx d)) (delta (delta dx (delta dxx dd)) ds)) dds) = begin
+delta-fmap-mu-to-tail (S n) (S m) (delta (delta (delta x (delta xx d)) (delta (delta dx (delta dxx dd)) ds)) dds) = begin
   delta (delta dxx (delta-mu (delta-fmap tailDelta (delta-fmap tailDelta ds))))
     (delta-fmap tailDelta (delta-fmap delta-mu dds))
-  ≡⟨ cong (\de -> delta (delta dxx (delta-mu (delta-fmap tailDelta (delta-fmap tailDelta ds)))) de) (delta-fmap-mu-to-tail n (S n₁) dds) ⟩
+  ≡⟨ cong (\de -> delta (delta dxx (delta-mu (delta-fmap tailDelta (delta-fmap tailDelta ds)))) de) (delta-fmap-mu-to-tail n (S m) dds) ⟩
   delta (delta dxx (delta-mu (delta-fmap tailDelta (delta-fmap tailDelta ds))))
     (delta-fmap delta-mu (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta dds)))
   ∎
@@ -89,7 +83,7 @@
 -- association-law : join . delta-fmap join = join . join
 delta-association-law : {l : Level} {A : Set l} {n : Nat} (d : Delta (Delta (Delta A (S n)) (S n)) (S n)) ->
               ((delta-mu ∙ (delta-fmap delta-mu)) d) ≡ ((delta-mu ∙ delta-mu) d)
-delta-association-law {n =       O} (mono d)                          = refl
+delta-association-law {n =   O} (mono d)                          = refl
 delta-association-law {n = S n} (delta (delta (delta x d) dd) ds) = begin
   delta x (delta-mu (delta-fmap tailDelta (delta-fmap delta-mu ds)))
   ≡⟨ cong (\de -> delta x (delta-mu de)) (delta-fmap-mu-to-tail n n ds) ⟩
diff -r 160a86e97a54 -r 957496efbe5d haskell/Example/Delta.hs
--- a/haskell/Example/Delta.hs	Sun Feb 15 17:42:58 2015 +0900
+++ b/haskell/Example/Delta.hs	Sun Feb 15 17:44:20 2015 +0900
@@ -3,34 +3,20 @@
 import Data.Numbers.Primes
 import Delta
 
--- samples
+-- examples
 
 generator :: Int -> Delta [Int]
 generator x = let intList = [1..x] in
                   return intList
 
-primeFilter :: [Int] -> Delta [Int]
-primeFilter xs = let primeList    = filter isPrime xs
-                     refactorList = filter even xs    in
-                 deltaFromList [ primeList, refactorList]
+numberFilter :: [Int] -> Delta [Int]
+numberFilter xs = let primeList = filter isPrime xs
+                      evenList  = filter even xs    in
+                  Delta evenList (Mono primeList)
 
 count :: [Int] -> Delta Int
 count xs = let primeCount = length xs in
            return primeCount
 
-primeCount :: Int -> Delta Int
-primeCount x = generator x >>= primeFilter >>= count
-
-bubbleSort :: [Int] -> Delta [Int]
-bubbleSort [] = return []
-bubbleSort xs = bubbleSort remainValue >>= (\xs -> deltaFromList [ (sortedValueL : xs),
-                                                                   (sortedValueR ++ xs)] )
-    where
-        maximumValue = maximum xs
-        sortedValueL = maximumValue
-        sortedValueR = replicate (length $ filter (== maximumValue) xs) maximumValue
-        remainValue  = filter (/= maximumValue) xs
-
-
-
-
+numberCount :: Int -> Delta Int
+numberCount x = generator x >>= numberFilter >>= count
diff -r 160a86e97a54 -r 957496efbe5d haskell/Example/DeltaM.hs
--- a/haskell/Example/DeltaM.hs	Sun Feb 15 17:42:58 2015 +0900
+++ b/haskell/Example/DeltaM.hs	Sun Feb 15 17:44:20 2015 +0900
@@ -25,22 +25,22 @@
 
 
 -- example : prime filter
--- usage   : runWriter $ checkOut 0 $ primeCountM 30  -- run specific version
---         : dmap runWriter $ primeCountM 30          -- run all version
+-- usage   : runWriter $ checkOut 0 $ numberCountM 30  -- run specific version
+--         : dmap runWriter $ numberCountM 30          -- run all version
 
 generatorM :: Int -> DeltaWithLog [Int]
 generatorM x = let intList = [1..x] in
                              DeltaM $ deltaFromList $ fmap returnW $ replicate 2 intList
 
-primeFilterM :: [Int] -> DeltaWithLog [Int]
-primeFilterM xs = let primeList    = filter isPrime xs
-                      refactorList = filter even xs    in
-                      DeltaM $ deltaFromList $ fmap returnW [primeList, refactorList]
+numberFilterM :: [Int] -> DeltaWithLog [Int]
+numberFilterM xs = let primeList = filter isPrime xs
+                       evenList  = filter even xs    in
+                      DeltaM $ deltaFromList $ fmap returnW [primeList, evenList]
 
 
 countM :: [Int] -> DeltaWithLog Int
-countM xs = let primeCount = length xs in
-                DeltaM $ deltaFromList $ fmap returnW $ replicate 2 primeCount
+countM xs = let numberCount = length xs in
+                DeltaM $ deltaFromList $ fmap returnW $ replicate 2 numberCount
 
-primeCountM :: Int -> DeltaWithLog Int
-primeCountM x = generatorM x >>= primeFilterM >>= countM
+numberCountM :: Int -> DeltaWithLog Int
+numberCountM x = generatorM x >>= numberFilterM >>= countM