Mercurial > hg > Members > atton > delta_monad

comparison agda/deltaM.agda @ 100:d8cd880f1d78

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Redefine some functions DeltaM in agda
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Fri, 23 Jan 2015 17:44:53 +0900
parents cf372fbcebd8
children 29c54b0197fb
comparison
equal deleted inserted replaced
99:0580e1642477 100:d8cd880f1d78
24 headDeltaM : {l : Level} {A : Set l} 24 headDeltaM : {l : Level} {A : Set l}
25 {M : {l' : Level} -> Set l' -> Set l'} 25 {M : {l' : Level} -> Set l' -> Set l'}
26 {functorM : {l' : Level} -> Functor {l'} M} 26 {functorM : {l' : Level} -> Functor {l'} M}
27 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM} 27 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM}
28 -> DeltaM M {functorM} {monadM} A -> M A 28 -> DeltaM M {functorM} {monadM} A -> M A
29 headDeltaM (deltaM (mono x)) = x 29 headDeltaM (deltaM d) = headDelta d
30 headDeltaM (deltaM (delta x _)) = x 30
31 31
32 tailDeltaM : {l : Level} {A : Set l} 32 tailDeltaM : {l : Level} {A : Set l}
33 {M : {l' : Level} -> Set l' -> Set l'} 33 {M : {l' : Level} -> Set l' -> Set l'}
34 {functorM : {l' : Level} -> Functor {l'} M} 34 {functorM : {l' : Level} -> Functor {l'} M}
35 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM} 35 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM}
36 -> DeltaM M {functorM} {monadM} A -> DeltaM M {functorM} {monadM} A 36 -> DeltaM M {functorM} {monadM} A -> DeltaM M {functorM} {monadM} A
37 tailDeltaM (deltaM (mono x)) = deltaM (mono x) 37 tailDeltaM (deltaM d) = deltaM (tailDelta d)
38 tailDeltaM (deltaM (delta _ d)) = deltaM d 38
39 39
40 appendDeltaM : {l : Level} {A : Set l} 40 appendDeltaM : {l : Level} {A : Set l}
41 {M : {l' : Level} -> Set l' -> Set l'} 41 {M : {l' : Level} -> Set l' -> Set l'}
42 {functorM : {l' : Level} -> Functor {l'} M} 42 {functorM : {l' : Level} -> Functor {l'} M}
43 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM} 43 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM}
72 {functorM : {l' : Level} -> Functor {l'} M} 72 {functorM : {l' : Level} -> Functor {l'} M}
73 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM} 73 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM}
74 -> A -> (DeltaM M {functorM} {monadM} A) 74 -> A -> (DeltaM M {functorM} {monadM} A)
75 deltaM-eta {_} {A} {_} {_} {_} {monadM} x = deltaM (mono (eta {_} {A} monadM x)) 75 deltaM-eta {_} {A} {_} {_} {_} {monadM} x = deltaM (mono (eta {_} {A} monadM x))
76 76
77 deltaM-mu : {l : Level} {A : Set l} {M : {l' : Level} -> Set l' -> Set l'}
78 {functorM : {l' : Level} -> Functor {l'} M}
79 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM}
80 -> (DeltaM M {functorM} {monadM} (DeltaM M {functorM} {monadM} A)) -> DeltaM M {functorM} {monadM} A
81 deltaM-mu {l} {A} {M} {functorM} {monadM} (deltaM (mono x)) = deltaM (mono (bind {l} {A} monadM x headDeltaM))
82 deltaM-mu {l} {A} {M} {functorM} {monadM} (deltaM (delta x (mono xx))) = appendDeltaM (deltaM (mono (bind {l} {A} monadM x headDeltaM)))
83 (deltaM-mu (deltaM (mono xx)))
84 deltaM-mu {l} {A} {M} {functorM} {monadM} (deltaM (delta x (delta xx d))) = appendDeltaM (deltaM (mono (bind {l} {A} monadM x headDeltaM)))
85 (deltaM-mu (deltaM d))
86 -- original deltaM-mu definitions. but it's cannot termination checking.
87 -- manually expand nested delta for delete tailDelta in argument to recursive deltaM-mu.
88 {-
89 deltaM-mu {l} {A} {M} {functorM} {monadM} (deltaM (delta x d)) = appendDeltaM (deltaM (mono (bind monadM x headDeltaM)))
90 (deltaM-mu (deltaM (tailDelta d)))
91 -}
92
77 deltaM-bind : {l : Level} {A B : Set l} {M : {l' : Level} -> Set l' -> Set l'} 93 deltaM-bind : {l : Level} {A B : Set l} {M : {l' : Level} -> Set l' -> Set l'}
78 {functorM : {l' : Level} -> Functor {l'} M} 94 {functorM : {l' : Level} -> Functor {l'} M}
79 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM} 95 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM}
80 -> (DeltaM M {functorM} {monadM} A) -> (A -> DeltaM M {functorM} {monadM} B) -> DeltaM M {functorM} {monadM} B 96 -> (DeltaM M {functorM} {monadM} A) -> (A -> DeltaM M {functorM} {monadM} B) -> DeltaM M {functorM} {monadM} B
81 deltaM-bind {l} {A} {B} {M} {functorM} {monadM} (deltaM (mono x)) f = deltaM (mono (bind {l} {A} monadM x (headDeltaM ∙ f))) 97 deltaM-bind {l} {A} {B} {M} {functorM} {monadM} d f = deltaM-mu (deltaM-fmap f d)
82 deltaM-bind {l} {A} {B} {M} {functorM} {monadM} (deltaM (delta x d)) f = appendDeltaM (deltaM (mono (bind {l} {A} monadM x (headDeltaM ∙ f))))
83 (deltaM-bind (deltaM d) (tailDeltaM ∙ f))
84
85 deltaM-mu : {l : Level} {A : Set l} {M : {l' : Level} -> Set l' -> Set l'}
86 {functorM : {l' : Level} -> Functor {l'} M}
87 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM}
88 -> (DeltaM M {functorM} {monadM} (DeltaM M {functorM} {monadM} A)) -> DeltaM M {functorM} {monadM} A
89 deltaM-mu d = deltaM-bind d id