# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1424842562 -32400
# Node ID f241d521bf652a1df9dcd7a75cc5d81332bbe48e
# Parent  861e3566546904af2b2b79fb0806452a8dc97527# Parent  3bbb68f0a1e341de40b5c784f59c948e6fbca83e
Merge

diff -r 3bbb68f0a1e3 -r f241d521bf65 .hgignore
--- a/.hgignore	Sun Feb 15 17:34:52 2015 +0900
+++ b/.hgignore	Wed Feb 25 14:36:02 2015 +0900
@@ -1,5 +1,7 @@
 syntax: glob
 
+.DS_Store
+
 *.swp
 *.*~
 *.agdai
diff -r 3bbb68f0a1e3 -r f241d521bf65 agda/delta.agda
--- a/agda/delta.agda	Sun Feb 15 17:34:52 2015 +0900
+++ b/agda/delta.agda	Wed Feb 25 14:36:02 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 3bbb68f0a1e3 -r f241d521bf65 agda/delta/monad.agda
--- a/agda/delta/monad.agda	Sun Feb 15 17:34:52 2015 +0900
+++ b/agda/delta/monad.agda	Wed Feb 25 14:36:02 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 3bbb68f0a1e3 -r f241d521bf65 haskell/Delta.hs
--- a/haskell/Delta.hs	Sun Feb 15 17:34:52 2015 +0900
+++ b/haskell/Delta.hs	Wed Feb 25 14:36:02 2015 +0900
@@ -1,6 +1,7 @@
+module Delta ( Delta(..) , deltaAppend , headDelta , tailDelta , deltaFromList) where
+
 import Control.Applicative
-import Control.Monad.Writer
-import Data.Numbers.Primes -- $ cabal install primes
+
 
 -- Delta definition
 
@@ -51,127 +52,5 @@
 
 -- utils
 
-returnDD :: (Show s) => s -> s -> Delta s
-returnDD x y = (return x) `deltaAppend` (return y)
-
 deltaFromList :: [a] -> Delta a
 deltaFromList = (foldl1 deltaAppend) . (fmap return)
-
-
--- samples
-
-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
-                 returnDD primeList refactorList
-
-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 -> returnDD (sortedValueL : xs)
-                                                            (sortedValueR ++ xs))
-    where
-        maximumValue = maximum xs
-        sortedValueL = maximumValue
-        sortedValueR = replicate (length $ filter (== maximumValue) xs) maximumValue
-        remainValue  = filter (/= maximumValue) xs
-
-
-
--- DeltaM definition (Delta with Monad)
-
-data DeltaM m a = DeltaM (Delta (m a)) deriving (Show)
-
-
--- DeltaM utils
-
-unDeltaM :: DeltaM m a -> Delta (m a)
-unDeltaM (DeltaM d) = d
-
-headDeltaM :: DeltaM m a -> m a
-headDeltaM (DeltaM d) = headDelta d
-
-tailDeltaM :: DeltaM m a -> DeltaM m a
-tailDeltaM (DeltaM d) = DeltaM $ tailDelta d
-
-appendDeltaM :: DeltaM m a -> DeltaM m a -> DeltaM m a
-appendDeltaM (DeltaM d) (DeltaM dd) = DeltaM (deltaAppend d dd)
-
-checkOut :: Int -> DeltaM m a -> m a
-checkOut 0 (DeltaM (Mono x))    = x
-checkOut 0 (DeltaM (Delta x _)) = x
-checkOut n (DeltaM (Mono x))    = x
-checkOut n (DeltaM (Delta _ d)) = checkOut (n-1) (DeltaM d)
-
-
--- DeltaM instance definitions
-
-instance (Functor m) => Functor (DeltaM m) where
-    fmap f (DeltaM d) = DeltaM $ fmap (fmap f) d
-
-instance (Applicative m) => Applicative (DeltaM m) where
-    pure f                                          = DeltaM $ Mono $ pure f
-    (DeltaM (Mono f))     <*> (DeltaM (Mono x))     = DeltaM $ Mono $ f <*> x
-    df@(DeltaM (Mono f))  <*> (DeltaM (Delta x d))  = appendDeltaM (DeltaM $ Mono $ f <*> x) (df <*> (DeltaM d))
-    (DeltaM (Delta f df)) <*> dx@(DeltaM (Mono x))  = appendDeltaM (DeltaM $ Mono $ f <*> x) ((DeltaM df) <*> dx)
-    (DeltaM (Delta f df)) <*> (DeltaM (Delta x dx)) = appendDeltaM (DeltaM $ Mono $ f <*> x) ((DeltaM df) <*> (DeltaM dx))
-
-
-mu' :: (Functor m, Monad m) => DeltaM m (DeltaM m a) -> DeltaM m a
-mu' d@(DeltaM (Mono _))    = DeltaM $ Mono $ (>>= id) $ fmap headDeltaM $ headDeltaM d
-mu' d@(DeltaM (Delta _ _)) = DeltaM $ Delta ((>>= id) $ fmap headDeltaM $ headDeltaM d)
-                                            (unDeltaM (mu' (fmap tailDeltaM (tailDeltaM d))))
-
-instance (Functor m, Monad m) => Monad (DeltaM m) where
-    return x = DeltaM $ Mono $ return x
-    d >>= f  = mu' $ fmap f d
-
-
-
--- DeltaM examples
-
--- DeltaM example utils
-type DeltaLog     = Writer [String]
-type DeltaWithLog = DeltaM DeltaLog
-
-returnW :: (Show a) => a -> DeltaLog a
-returnW x = do tell $ [show x]
-               return x
-
-dmap :: (m a -> b) -> DeltaM m a -> Delta b
-dmap f (DeltaM d) = fmap f d
-
-deltaWithLogFromList :: (Show a) => [a] -> DeltaWithLog a
-deltaWithLogFromList xs = DeltaM $ deltaFromList $ fmap returnW xs
-
-
--- example : prime filter
--- usage   : runWriter $ checkOut 0 $ primeCountM 30  -- run specific version
---         : dmap runWriter $ primeCountM 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]
-
-
-countM :: [Int] -> DeltaWithLog Int
-countM xs = let primeCount = length xs in
-                DeltaM $ deltaFromList $ fmap returnW $ replicate 2 primeCount
-
-primeCountM :: Int -> DeltaWithLog Int
-primeCountM x = generatorM x >>= primeFilterM >>= countM
diff -r 3bbb68f0a1e3 -r f241d521bf65 haskell/DeltaM.hs
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/haskell/DeltaM.hs	Wed Feb 25 14:36:02 2015 +0900
@@ -0,0 +1,56 @@
+module DeltaM (DeltaM(..), unDeltaM, appendDeltaM, tailDeltaM, headDeltaM, checkOut) where
+
+import Control.Applicative
+import Delta
+
+
+-- DeltaM definition (Delta with Monad)
+
+data DeltaM m a = DeltaM (Delta (m a)) deriving (Show)
+
+
+-- DeltaM utils
+
+unDeltaM :: DeltaM m a -> Delta (m a)
+unDeltaM (DeltaM d) = d
+
+headDeltaM :: DeltaM m a -> m a
+headDeltaM (DeltaM d) = headDelta d
+
+tailDeltaM :: DeltaM m a -> DeltaM m a
+tailDeltaM (DeltaM d) = DeltaM $ tailDelta d
+
+appendDeltaM :: DeltaM m a -> DeltaM m a -> DeltaM m a
+appendDeltaM (DeltaM d) (DeltaM dd) = DeltaM (deltaAppend d dd)
+
+checkOut :: Int -> DeltaM m a -> m a
+checkOut 0 (DeltaM (Mono x))    = x
+checkOut 0 (DeltaM (Delta x _)) = x
+checkOut n (DeltaM (Mono x))    = x
+checkOut n (DeltaM (Delta _ d)) = checkOut (n-1) (DeltaM d)
+
+
+-- DeltaM instance definitions
+
+instance (Functor m) => Functor (DeltaM m) where
+    fmap f (DeltaM d) = DeltaM $ fmap (fmap f) d
+
+instance (Applicative m) => Applicative (DeltaM m) where
+    pure f                                          = DeltaM $ Mono $ pure f
+    (DeltaM (Mono f))     <*> (DeltaM (Mono x))     = DeltaM $ Mono $ f <*> x
+    df@(DeltaM (Mono f))  <*> (DeltaM (Delta x d))  = appendDeltaM (DeltaM $ Mono $ f <*> x) (df <*> (DeltaM d))
+    (DeltaM (Delta f df)) <*> dx@(DeltaM (Mono x))  = appendDeltaM (DeltaM $ Mono $ f <*> x) ((DeltaM df) <*> dx)
+    (DeltaM (Delta f df)) <*> (DeltaM (Delta x dx)) = appendDeltaM (DeltaM $ Mono $ f <*> x) ((DeltaM df) <*> (DeltaM dx))
+
+
+mu' :: (Functor m, Monad m) => DeltaM m (DeltaM m a) -> DeltaM m a
+mu' d@(DeltaM (Mono _))    = DeltaM $ Mono $ (>>= id) $ fmap headDeltaM $ headDeltaM d
+mu' d@(DeltaM (Delta _ _)) = DeltaM $ Delta ((>>= id) $ fmap headDeltaM $ headDeltaM d)
+                                            (unDeltaM (mu' (fmap tailDeltaM (tailDeltaM d))))
+
+instance (Functor m, Monad m) => Monad (DeltaM m) where
+    return x = DeltaM $ Mono $ return x
+    d >>= f  = mu' $ fmap f d
+
+
+
diff -r 3bbb68f0a1e3 -r f241d521bf65 haskell/Example/Delta.hs
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/haskell/Example/Delta.hs	Wed Feb 25 14:36:02 2015 +0900
@@ -0,0 +1,47 @@
+module Example.Delta where
+
+import Data.Numbers.Primes
+import Delta
+
+-- examples
+
+generator :: Int -> Delta [Int]
+generator x = let intList = [1..x] in
+                  return intList
+
+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
+
+numberCount :: Int -> Delta Int
+numberCount x = generator x >>= numberFilter >>= count
+
+sort :: [Int] -> Delta [Int]
+sort xs = deltaFromList [ bubbleSort  xs,
+                          singleSort  xs,
+                          swapPair    xs,
+                          identity,
+                          nil
+                        ]
+    where
+        nil = []
+        identity = xs
+
+        swapPair  []        = []
+        swapPair  [x]       = [x]
+        swapPair  (x:xx:xs) = (min x xx) : (max x xx) : xs
+
+        singleSort []        = []
+        singleSort xs        = (minimum xs) : (singleSort (filter (/= (minimum xs)) xs))
+
+        bubbleSort []       = []
+        bubbleSort xs       = let
+                minVal  = minimum xs
+                minVals = replicate (length (filter (== minVal) xs)) minVal
+            in
+                minVals ++ (bubbleSort (filter (/= (minimum xs)) xs))
diff -r 3bbb68f0a1e3 -r f241d521bf65 haskell/Example/DeltaM.hs
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/haskell/Example/DeltaM.hs	Wed Feb 25 14:36:02 2015 +0900
@@ -0,0 +1,87 @@
+module Example.DeltaM where
+
+import Control.Monad.Writer
+import Data.Numbers.Primes -- $ cabal install primes
+
+import Delta
+import DeltaM
+
+
+-- DeltaM examples
+
+-- DeltaM example utils
+type DeltaLog     = Writer [String]
+type DeltaWithLog = DeltaM DeltaLog
+
+returnW :: (Show a) => a -> DeltaLog a
+returnW x = do tell $ [show x]
+               return x
+
+dmap :: (m a -> b) -> DeltaM m a -> Delta b
+dmap f (DeltaM d) = fmap f d
+
+deltaWithLogFromList :: (Show a) => [a] -> DeltaWithLog a
+deltaWithLogFromList xs = DeltaM $ deltaFromList $ fmap returnW xs
+
+
+-- example : prime filter
+-- 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
+
+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 numberCount = length xs in
+                DeltaM $ deltaFromList $ fmap returnW $ replicate 2 numberCount
+
+numberCountM :: Int -> DeltaWithLog Int
+numberCountM x = generatorM x >>= numberFilterM >>= countM
+
+
+-- example : sort
+
+sort :: [Int] -> DeltaWithLog [Int]
+sort xs = DeltaM $ deltaFromList [ --bubbleSort xs,
+                          singleSort xs,
+                          returnW $ swapPair xs,
+                          identity,
+                          nil
+                        ]
+    where
+        nil = returnW []
+
+        identity = returnW xs
+
+        swapPair  []        = []
+        swapPair  [x]       = [x]
+        swapPair  (x:xx:xs) = (min x xx) : (max x xx) : xs
+
+        singleSort []        = returnW []
+        singleSort xs        = do
+                tell [show xs]
+                res <- do
+                    remanVals <- singleSort $ filter (/= (minimum xs)) xs
+                    return $ (minimum xs) : remanVals
+                tell [ show res ]
+                return res
+
+        bubbleSort []       = returnW []
+        bubbleSort xs       = let
+                minVal  = minimum xs
+                minVals = replicate (length (filter (== minVal) xs)) minVal
+            in
+                do
+                    tell [show xs]
+                    res <- do
+                            remainVals <- bubbleSort $ filter (/= minVal) xs
+                            return $ minVals ++ remainVals
+                    tell [show res]
+                    return res