Mercurial > hg > Members > atton > delta_monad

annotate agda/deltaM.agda @ 103:a271f3ff1922

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Delte type dependencie in Monad record for escape implicit type conflict
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Mon, 26 Jan 2015 14:08:46 +0900
parents 29c54b0197fb
children ebd0d6e2772c
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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}
103
a271f3ff1922 Delte type dependencie in Monad record for escape implicit type conflict
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 101
diff changeset
16 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} M functorM}
89
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}
103
a271f3ff1922 Delte type dependencie in Monad record for escape implicit type conflict
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 101
diff changeset
27 {monadM : {l' : Level} -> Monad {l'} M functorM}
89
5411ce26d525 Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28 -> DeltaM M {functorM} {monadM} A -> M A
100
d8cd880f1d78 Redefine some functions DeltaM in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 95
diff changeset
29 headDeltaM (deltaM d) = headDelta d
d8cd880f1d78 Redefine some functions DeltaM in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 95
diff changeset
30
89
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}
103
a271f3ff1922 Delte type dependencie in Monad record for escape implicit type conflict
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 101
diff changeset
35 {monadM : {l' : Level} -> Monad {l'} M functorM}
89
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
100
d8cd880f1d78 Redefine some functions DeltaM in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 95
diff changeset
37 tailDeltaM (deltaM d) = deltaM (tailDelta d)
d8cd880f1d78 Redefine some functions DeltaM in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 95
diff changeset
38
89
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}
103
a271f3ff1922 Delte type dependencie in Monad record for escape implicit type conflict
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 101
diff changeset
43 {monadM : {l' : Level} -> Monad {l'} M functorM}
89
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}
103
a271f3ff1922 Delte type dependencie in Monad record for escape implicit type conflict
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 101
diff changeset
51 {monadM : {l' : Level} -> Monad {l'} M functorM}
89
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}
103
a271f3ff1922 Delte type dependencie in Monad record for escape implicit type conflict
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 101
diff changeset
65 {monadM : {l' : Level} -> Monad {l'} M functorM}
90
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
101
29c54b0197fb Fix bind definition on DeltaM. use mu.
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 100
diff changeset
71 deltaM-eta : {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
72 {functorM : {l' : Level} -> Functor {l'} M}
103
a271f3ff1922 Delte type dependencie in Monad record for escape implicit type conflict
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 101
diff changeset
73 {monadM : {l' : Level} -> Monad {l'} M functorM}
94
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)
103
a271f3ff1922 Delte type dependencie in Monad record for escape implicit type conflict
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 101
diff changeset
75 deltaM-eta {_} {A} {_} {_} {monadM} x = deltaM (mono (eta monadM x))
94
bcd4fe52a504 Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 90
diff changeset
76
100
d8cd880f1d78 Redefine some functions DeltaM in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 95
diff changeset
77 deltaM-mu : {l : Level} {A : Set l} {M : {l' : Level} -> Set l' -> Set l'}
d8cd880f1d78 Redefine some functions DeltaM in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 95
diff changeset
78 {functorM : {l' : Level} -> Functor {l'} M}
103
a271f3ff1922 Delte type dependencie in Monad record for escape implicit type conflict
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 101
diff changeset
79 {monadM : {l' : Level} -> Monad {l'} M functorM}
100
d8cd880f1d78 Redefine some functions DeltaM in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 95
diff changeset
80 -> (DeltaM M {functorM} {monadM} (DeltaM M {functorM} {monadM} A)) -> DeltaM M {functorM} {monadM} A
103
a271f3ff1922 Delte type dependencie in Monad record for escape implicit type conflict
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 101
diff changeset
81 deltaM-mu {l} {A} {M} {functorM} {monadM} (deltaM (mono x)) = deltaM (mono (mu monadM (fmap functorM headDeltaM x)))
a271f3ff1922 Delte type dependencie in Monad record for escape implicit type conflict
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 101
diff changeset
82 deltaM-mu {l} {A} {M} {functorM} {monadM} (deltaM (delta x (mono xx))) = appendDeltaM (deltaM (mono (bind monadM x headDeltaM)))
100
d8cd880f1d78 Redefine some functions DeltaM in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 95
diff changeset
83 (deltaM-mu (deltaM (mono xx)))
103
a271f3ff1922 Delte type dependencie in Monad record for escape implicit type conflict
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 101
diff changeset
84 deltaM-mu {l} {A} {M} {functorM} {monadM} (deltaM (delta x (delta xx d))) = appendDeltaM (deltaM (mono (bind {l} monadM x headDeltaM)))
100
d8cd880f1d78 Redefine some functions DeltaM in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 95
diff changeset
85 (deltaM-mu (deltaM d))
d8cd880f1d78 Redefine some functions DeltaM in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 95
diff changeset
86 -- original deltaM-mu definitions. but it's cannot termination checking.
d8cd880f1d78 Redefine some functions DeltaM in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 95
diff changeset
87 -- manually expand nested delta for delete tailDelta in argument to recursive deltaM-mu.
d8cd880f1d78 Redefine some functions DeltaM in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 95
diff changeset
88 {-
d8cd880f1d78 Redefine some functions DeltaM in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 95
diff changeset
89 deltaM-mu {l} {A} {M} {functorM} {monadM} (deltaM (delta x d)) = appendDeltaM (deltaM (mono (bind monadM x headDeltaM)))
d8cd880f1d78 Redefine some functions DeltaM in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 95
diff changeset
90 (deltaM-mu (deltaM (tailDelta d)))
d8cd880f1d78 Redefine some functions DeltaM in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 95
diff changeset
91 -}
d8cd880f1d78 Redefine some functions DeltaM in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 95
diff changeset
92
94
bcd4fe52a504 Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 90
diff changeset
93 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
94 {functorM : {l' : Level} -> Functor {l'} M}
103
a271f3ff1922 Delte type dependencie in Monad record for escape implicit type conflict
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 101
diff changeset
95 {monadM : {l' : Level} -> Monad {l'} M functorM}
94
bcd4fe52a504 Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 90
diff changeset
96 -> (DeltaM M {functorM} {monadM} A) -> (A -> DeltaM M {functorM} {monadM} B) -> DeltaM M {functorM} {monadM} B
100
d8cd880f1d78 Redefine some functions DeltaM in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 95
diff changeset
97 deltaM-bind {l} {A} {B} {M} {functorM} {monadM} d f = deltaM-mu (deltaM-fmap f d)