Mercurial > hg > Members > atton > delta_monad

annotate agda/delta.agda @ 146:57601209eff3 default tip

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add an example used multi types on Delta
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 24 Mar 2015 17:04:00 +0900
parents 2bf1fa6d2006
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
131
d205ff1e406f Cleanup proofs
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 105
diff changeset
1 open import Level
d205ff1e406f Cleanup proofs
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 105
diff changeset
2 open import Relation.Binary.PropositionalEquality
d205ff1e406f Cleanup proofs
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 105
diff changeset
3 open ≡-Reasoning
d205ff1e406f Cleanup proofs
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 105
diff changeset
4
26
5ba82f107a95 Define Similar in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 open import list
28
6e6d646d7722 Split basic functions to file
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 27
diff changeset
6 open import basic
76
c7076f9bbaed Refactors
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
7 open import nat
87
6789c65a75bc Split functor-proofs into delta.functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 80
diff changeset
8 open import laws
29
e0ba1bf564dd Apply level to some functions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
9
43
90b171e3a73e Rename to Delta from Similar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
10 module delta where
26
5ba82f107a95 Define Similar in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11
105
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
12 data Delta {l : Level} (A : Set l) : (Nat -> (Set l)) where
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
13 mono : A -> Delta A (S O)
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
14 delta : {n : Nat} -> A -> Delta A (S n) -> Delta A (S (S n))
54
9bb7c9bee94f Trying redefine delta for infinite changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 43
diff changeset
15
105
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
16 deltaAppend : {l : Level} {A : Set l} {n m : Nat} -> Delta A (S n) -> Delta A (S m) -> Delta A ((S n) + (S m))
57
dfcd72dc697e ReDefine Delta used non-empty-list for infinite changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
17 deltaAppend (mono x) d = delta x d
dfcd72dc697e ReDefine Delta used non-empty-list for infinite changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
18 deltaAppend (delta x d) ds = delta x (deltaAppend d ds)
54
9bb7c9bee94f Trying redefine delta for infinite changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 43
diff changeset
19
105
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
20 headDelta : {l : Level} {A : Set l} {n : Nat} -> Delta A (S n) -> A
70
18a20a14c4b2 Change prove method. use Int ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
21 headDelta (mono x) = x
18a20a14c4b2 Change prove method. use Int ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
22 headDelta (delta x _) = x
54
9bb7c9bee94f Trying redefine delta for infinite changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 43
diff changeset
23
105
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
24 tailDelta : {l : Level} {A : Set l} {n : Nat} -> Delta A (S (S n)) -> Delta A (S n)
79
7307e43a3c76 Prove monad-law-4
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 78
diff changeset
25 tailDelta (delta _ d) = d
26
5ba82f107a95 Define Similar in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26
76
c7076f9bbaed Refactors
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
27
38
6ce83b2c9e59 Proof Functor-laws
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 36
diff changeset
28
6ce83b2c9e59 Proof Functor-laws
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 36
diff changeset
29 -- Functor
105
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
30 delta-fmap : {l : Level} {A B : Set l} {n : Nat} -> (A -> B) -> (Delta A (S n)) -> (Delta B (S n))
89
5411ce26d525 Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 88
diff changeset
31 delta-fmap f (mono x) = mono (f x)
5411ce26d525 Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 88
diff changeset
32 delta-fmap f (delta x d) = delta (f x) (delta-fmap f d)
57
dfcd72dc697e ReDefine Delta used non-empty-list for infinite changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
33
26
5ba82f107a95 Define Similar in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34
38
6ce83b2c9e59 Proof Functor-laws
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 36
diff changeset
35
40
a7cd7740f33e Add Haskell style Monad-laws and Proof Monad-laws-h-1
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 39
diff changeset
36 -- Monad (Category)
105
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
37 delta-eta : {l : Level} {A : Set l} {n : Nat} -> A -> Delta A (S n)
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
38 delta-eta {n = O} x = mono x
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
39 delta-eta {n = (S n)} x = delta x (delta-eta {n = n} x)
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
40
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
41 delta-mu : {l : Level} {A : Set l} {n : Nat} -> (Delta (Delta A (S n)) (S n)) -> Delta A (S n)
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
42 delta-mu (mono x) = x
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
43 delta-mu (delta x d) = delta (headDelta x) (delta-mu (delta-fmap tailDelta d))
59
46b15f368905 Define bind and mu for Infinite Delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 57
diff changeset
44
105
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
45 delta-bind : {l : Level} {A B : Set l} {n : Nat} -> (Delta A (S n)) -> (A -> Delta B (S n)) -> Delta B (S n)
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
46 delta-bind d f = delta-mu (delta-fmap f d)
26
5ba82f107a95 Define Similar in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
47
104
ebd0d6e2772c Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 96
diff changeset
48 {-
40
a7cd7740f33e Add Haskell style Monad-laws and Proof Monad-laws-h-1
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 39
diff changeset
49 -- Monad (Haskell)
104
ebd0d6e2772c Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 96
diff changeset
50 delta-return : {l : Level} {A : Set l} -> A -> Delta A (S O)
94
bcd4fe52a504 Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 90
diff changeset
51 delta-return = delta-eta
40
a7cd7740f33e Add Haskell style Monad-laws and Proof Monad-laws-h-1
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 39
diff changeset
52
104
ebd0d6e2772c Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 96
diff changeset
53 _>>=_ : {l : Level} {A B : Set l} {n : Nat} ->
ebd0d6e2772c Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 96
diff changeset
54 (x : Delta A n) -> (f : A -> (Delta B n)) -> (Delta B n)
ebd0d6e2772c Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 96
diff changeset
55 d >>= f = delta-bind d f
40
a7cd7740f33e Add Haskell style Monad-laws and Proof Monad-laws-h-1
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 39
diff changeset
56
137
2bf1fa6d2006 Adjust codes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 131
diff changeset
57 -}