Mercurial > hg > Members > atton > delta_monad
changeset 140:957496efbe5d
Merge some commits
| author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 15 Feb 2015 17:44:20 +0900 |
| parents | 160a86e97a54 (current diff) 1f218e2d9de0 (diff) |
| children | 861e35665469 |
| files | |
| diffstat | 4 files changed, 21 insertions(+), 41 deletions(-) [+] |
line wrap: on
line diff
--- 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 +-}
--- 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) ⟩
--- 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
--- 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