Mercurial > hg > Members > atton > delta_monad
annotate agda/deltaM.agda @ 95:cf372fbcebd8
Fix implicit values in deltaM-mu
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 19 Jan 2015 17:47:55 +0900 |
parents | bcd4fe52a504 |
children | d8cd880f1d78 |
rev | line source |
---|---|
89
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
1 open import Level |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
2 |
94
bcd4fe52a504
Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
90
diff
changeset
|
3 open import basic |
89
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
4 open import delta |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
5 open import delta.functor |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
6 open import nat |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
7 open import laws |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
8 |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
9 module deltaM where |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
10 |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
11 -- DeltaM definitions |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
12 |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
13 data DeltaM {l : Level} |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
14 (M : {l' : Level} -> Set l' -> Set l') |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
15 {functorM : {l' : Level} -> Functor {l'} M} |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
16 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM} |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
17 (A : Set l) |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
18 : Set l where |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
19 deltaM : Delta (M A) -> DeltaM M {functorM} {monadM} A |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
20 |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
21 |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
22 -- DeltaM utils |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
23 |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
24 headDeltaM : {l : Level} {A : Set l} |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
25 {M : {l' : Level} -> Set l' -> Set l'} |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
26 {functorM : {l' : Level} -> Functor {l'} M} |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
27 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM} |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
28 -> DeltaM M {functorM} {monadM} A -> M A |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
29 headDeltaM (deltaM (mono x)) = x |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
30 headDeltaM (deltaM (delta x _)) = x |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
31 |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
32 tailDeltaM : {l : Level} {A : Set l} |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
33 {M : {l' : Level} -> Set l' -> Set l'} |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
34 {functorM : {l' : Level} -> Functor {l'} M} |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
35 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM} |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
36 -> DeltaM M {functorM} {monadM} A -> DeltaM M {functorM} {monadM} A |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
37 tailDeltaM (deltaM (mono x)) = deltaM (mono x) |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
38 tailDeltaM (deltaM (delta _ d)) = deltaM d |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
39 |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
40 appendDeltaM : {l : Level} {A : Set l} |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
41 {M : {l' : Level} -> Set l' -> Set l'} |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
42 {functorM : {l' : Level} -> Functor {l'} M} |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
43 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM} |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
44 -> DeltaM M {functorM} {monadM} A -> DeltaM M {functorM} {monadM} A -> DeltaM M {functorM} {monadM} A |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
45 appendDeltaM (deltaM d) (deltaM dd) = deltaM (deltaAppend d dd) |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
46 |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
47 |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
48 checkOut : {l : Level} {A : Set l} |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
49 {M : {l' : Level} -> Set l' -> Set l'} |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
50 {functorM : {l' : Level} -> Functor {l'} M} |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
51 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM} |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
52 -> Nat -> DeltaM M {functorM} {monadM} A -> M A |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
53 checkOut O (deltaM (mono x)) = x |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
54 checkOut O (deltaM (delta x _)) = x |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
55 checkOut (S n) (deltaM (mono x)) = x |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
56 checkOut {l} {A} {M} {functorM} {monadM} (S n) (deltaM (delta _ d)) = checkOut {l} {A} {M} {functorM} {monadM} n (deltaM d) |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
57 |
90
55d11ce7e223
Unify levels on data type. only use suc to proofs
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
89
diff
changeset
|
58 |
94
bcd4fe52a504
Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
90
diff
changeset
|
59 |
bcd4fe52a504
Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
90
diff
changeset
|
60 -- functor definitions |
90
55d11ce7e223
Unify levels on data type. only use suc to proofs
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
89
diff
changeset
|
61 open Functor |
55d11ce7e223
Unify levels on data type. only use suc to proofs
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
89
diff
changeset
|
62 deltaM-fmap : {l : Level} {A B : Set l} |
55d11ce7e223
Unify levels on data type. only use suc to proofs
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
89
diff
changeset
|
63 {M : {l' : Level} -> Set l' -> Set l'} |
55d11ce7e223
Unify levels on data type. only use suc to proofs
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
89
diff
changeset
|
64 {functorM : {l' : Level} -> Functor {l'} M} |
55d11ce7e223
Unify levels on data type. only use suc to proofs
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
89
diff
changeset
|
65 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM} |
55d11ce7e223
Unify levels on data type. only use suc to proofs
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
89
diff
changeset
|
66 -> (A -> B) -> DeltaM M {functorM} {monadM} A -> DeltaM M {functorM} {monadM} B |
55d11ce7e223
Unify levels on data type. only use suc to proofs
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
89
diff
changeset
|
67 deltaM-fmap {l} {A} {B} {M} {functorM} f (deltaM d) = deltaM (fmap delta-is-functor (fmap functorM f) d) |
94
bcd4fe52a504
Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
90
diff
changeset
|
68 |
bcd4fe52a504
Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
90
diff
changeset
|
69 -- monad definitions |
bcd4fe52a504
Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
90
diff
changeset
|
70 open Monad |
bcd4fe52a504
Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
90
diff
changeset
|
71 deltaM-eta : {l : Level} {A B : Set l} {M : {l' : Level} -> Set l' -> Set l'} |
bcd4fe52a504
Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
90
diff
changeset
|
72 {functorM : {l' : Level} -> Functor {l'} M} |
bcd4fe52a504
Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
90
diff
changeset
|
73 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM} |
bcd4fe52a504
Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
90
diff
changeset
|
74 -> A -> (DeltaM M {functorM} {monadM} A) |
bcd4fe52a504
Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
90
diff
changeset
|
75 deltaM-eta {_} {A} {_} {_} {_} {monadM} x = deltaM (mono (eta {_} {A} monadM x)) |
bcd4fe52a504
Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
90
diff
changeset
|
76 |
bcd4fe52a504
Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
90
diff
changeset
|
77 deltaM-bind : {l : Level} {A B : Set l} {M : {l' : Level} -> Set l' -> Set l'} |
bcd4fe52a504
Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
90
diff
changeset
|
78 {functorM : {l' : Level} -> Functor {l'} M} |
bcd4fe52a504
Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
90
diff
changeset
|
79 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM} |
bcd4fe52a504
Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
90
diff
changeset
|
80 -> (DeltaM M {functorM} {monadM} A) -> (A -> DeltaM M {functorM} {monadM} B) -> DeltaM M {functorM} {monadM} B |
bcd4fe52a504
Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
90
diff
changeset
|
81 deltaM-bind {l} {A} {B} {M} {functorM} {monadM} (deltaM (mono x)) f = deltaM (mono (bind {l} {A} monadM x (headDeltaM ∙ f))) |
bcd4fe52a504
Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
90
diff
changeset
|
82 deltaM-bind {l} {A} {B} {M} {functorM} {monadM} (deltaM (delta x d)) f = appendDeltaM (deltaM (mono (bind {l} {A} monadM x (headDeltaM ∙ f)))) |
bcd4fe52a504
Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
90
diff
changeset
|
83 (deltaM-bind (deltaM d) (tailDeltaM ∙ f)) |
bcd4fe52a504
Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
90
diff
changeset
|
84 |
95
cf372fbcebd8
Fix implicit values in deltaM-mu
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
94
diff
changeset
|
85 deltaM-mu : {l : Level} {A : Set l} {M : {l' : Level} -> Set l' -> Set l'} |
94
bcd4fe52a504
Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
90
diff
changeset
|
86 {functorM : {l' : Level} -> Functor {l'} M} |
bcd4fe52a504
Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
90
diff
changeset
|
87 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM} |
bcd4fe52a504
Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
90
diff
changeset
|
88 -> (DeltaM M {functorM} {monadM} (DeltaM M {functorM} {monadM} A)) -> DeltaM M {functorM} {monadM} A |
bcd4fe52a504
Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
90
diff
changeset
|
89 deltaM-mu d = deltaM-bind d id |