Mercurial > hg > Members > atton > delta_monad
diff agda/deltaM.agda @ 104:ebd0d6e2772c
Trying redenition Delta with length constraints
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 26 Jan 2015 23:00:05 +0900 |
parents | a271f3ff1922 |
children | 5bd5f4a7ce8d |
line wrap: on
line diff
--- a/agda/deltaM.agda Mon Jan 26 14:08:46 2015 +0900 +++ b/agda/deltaM.agda Mon Jan 26 23:00:05 2015 +0900 @@ -4,6 +4,7 @@ open import delta open import delta.functor open import nat +open import revision open import laws module deltaM where @@ -15,83 +16,76 @@ {functorM : {l' : Level} -> Functor {l'} M} {monadM : {l' : Level} {A : Set l'} -> Monad {l'} M functorM} (A : Set l) - : Set l where - deltaM : Delta (M A) -> DeltaM M {functorM} {monadM} A + : (Rev -> Set l) where + deltaM : {v : Rev} -> Delta (M A) v -> DeltaM M {functorM} {monadM} A v -- DeltaM utils -headDeltaM : {l : Level} {A : Set l} +headDeltaM : {l : Level} {A : Set l} {v : Rev} {M : {l' : Level} -> Set l' -> Set l'} {functorM : {l' : Level} -> Functor {l'} M} {monadM : {l' : Level} -> Monad {l'} M functorM} - -> DeltaM M {functorM} {monadM} A -> M A + -> DeltaM M {functorM} {monadM} A v -> M A headDeltaM (deltaM d) = headDelta d -tailDeltaM : {l : Level} {A : Set l} - {M : {l' : Level} -> Set l' -> Set l'} - {functorM : {l' : Level} -> Functor {l'} M} - {monadM : {l' : Level} -> Monad {l'} M functorM} - -> DeltaM M {functorM} {monadM} A -> DeltaM M {functorM} {monadM} A -tailDeltaM (deltaM d) = deltaM (tailDelta d) - - -appendDeltaM : {l : Level} {A : Set l} +tailDeltaM : {l : Level} {A : Set l} {v : Rev} {M : {l' : Level} -> Set l' -> Set l'} {functorM : {l' : Level} -> Functor {l'} M} {monadM : {l' : Level} -> Monad {l'} M functorM} - -> DeltaM M {functorM} {monadM} A -> DeltaM M {functorM} {monadM} A -> DeltaM M {functorM} {monadM} A -appendDeltaM (deltaM d) (deltaM dd) = deltaM (deltaAppend d dd) + -> DeltaM {l} M {functorM} {monadM} A (commit v) -> DeltaM M {functorM} {monadM} A v +tailDeltaM {_} {n} (deltaM d) = deltaM (tailDelta d) -checkOut : {l : Level} {A : Set l} - {M : {l' : Level} -> Set l' -> Set l'} - {functorM : {l' : Level} -> Functor {l'} M} - {monadM : {l' : Level} -> Monad {l'} M functorM} - -> Nat -> DeltaM M {functorM} {monadM} A -> M A -checkOut O (deltaM (mono x)) = x -checkOut O (deltaM (delta x _)) = x -checkOut (S n) (deltaM (mono x)) = x -checkOut {l} {A} {M} {functorM} {monadM} (S n) (deltaM (delta _ d)) = checkOut {l} {A} {M} {functorM} {monadM} n (deltaM d) +appendDeltaM : {l : Level} {A : Set l} {n m : Rev} + {M : {l' : Level} -> Set l' -> Set l'} + {functorM : {l' : Level} -> Functor {l'} M} + {monadM : {l' : Level} -> Monad {l'} M functorM} + -> DeltaM M {functorM} {monadM} A n -> DeltaM M {functorM} {monadM} A m -> DeltaM M {functorM} {monadM} A (merge n m) +appendDeltaM (deltaM d) (deltaM dd) = deltaM (deltaAppend d dd) + -- functor definitions open Functor -deltaM-fmap : {l : Level} {A B : Set l} +deltaM-fmap : {l : Level} {A B : Set l} {n : Rev} {M : {l' : Level} -> Set l' -> Set l'} {functorM : {l' : Level} -> Functor {l'} M} {monadM : {l' : Level} -> Monad {l'} M functorM} - -> (A -> B) -> DeltaM M {functorM} {monadM} A -> DeltaM M {functorM} {monadM} B -deltaM-fmap {l} {A} {B} {M} {functorM} f (deltaM d) = deltaM (fmap delta-is-functor (fmap functorM f) d) + -> (A -> B) -> DeltaM M {functorM} {monadM} A n -> DeltaM M {functorM} {monadM} B n +deltaM-fmap {l} {A} {B} {n} {M} {functorM} f (deltaM d) = deltaM (fmap delta-is-functor (fmap functorM f) d) + + + -- monad definitions open Monad -deltaM-eta : {l : Level} {A : Set l} {M : {l' : Level} -> Set l' -> Set l'} - {functorM : {l' : Level} -> Functor {l'} M} - {monadM : {l' : Level} -> Monad {l'} M functorM} - -> A -> (DeltaM M {functorM} {monadM} A) -deltaM-eta {_} {A} {_} {_} {monadM} x = deltaM (mono (eta monadM x)) -deltaM-mu : {l : Level} {A : Set l} {M : {l' : Level} -> Set l' -> Set l'} - {functorM : {l' : Level} -> Functor {l'} M} - {monadM : {l' : Level} -> Monad {l'} M functorM} - -> (DeltaM M {functorM} {monadM} (DeltaM M {functorM} {monadM} A)) -> DeltaM M {functorM} {monadM} A -deltaM-mu {l} {A} {M} {functorM} {monadM} (deltaM (mono x)) = deltaM (mono (mu monadM (fmap functorM headDeltaM x))) -deltaM-mu {l} {A} {M} {functorM} {monadM} (deltaM (delta x (mono xx))) = appendDeltaM (deltaM (mono (bind monadM x headDeltaM))) - (deltaM-mu (deltaM (mono xx))) -deltaM-mu {l} {A} {M} {functorM} {monadM} (deltaM (delta x (delta xx d))) = appendDeltaM (deltaM (mono (bind {l} monadM x headDeltaM))) - (deltaM-mu (deltaM d)) --- original deltaM-mu definitions. but it's cannot termination checking. --- manually expand nested delta for delete tailDelta in argument to recursive deltaM-mu. -{- -deltaM-mu {l} {A} {M} {functorM} {monadM} (deltaM (delta x d)) = appendDeltaM (deltaM (mono (bind monadM x headDeltaM))) - (deltaM-mu (deltaM (tailDelta d))) --} +deltaM-eta : {l : Level} {A : Set l} {v : Rev} + {M : {l' : Level} -> Set l' -> Set l'} + {functorM : {l' : Level} -> Functor {l'} M} + {monadM : {l' : Level} -> Monad {l'} M functorM} + -> A -> (DeltaM M {functorM} {monadM} A v) +deltaM-eta {v = init} {monadM = mm} x = deltaM (mono (eta mm x)) +deltaM-eta {v = (commit v)} {monadM = mm} x = appendDeltaM (deltaM (mono (eta mm x))) + (deltaM-eta {v = v} x) -deltaM-bind : {l : Level} {A B : Set l} {M : {l' : Level} -> Set l' -> Set l'} + +deltaM-bind : {l : Level} {A B : Set l} {v : Rev} + {M : {l' : Level} -> Set l' -> Set l'} {functorM : {l' : Level} -> Functor {l'} M} {monadM : {l' : Level} -> Monad {l'} M functorM} - -> (DeltaM M {functorM} {monadM} A) -> (A -> DeltaM M {functorM} {monadM} B) -> DeltaM M {functorM} {monadM} B -deltaM-bind {l} {A} {B} {M} {functorM} {monadM} d f = deltaM-mu (deltaM-fmap f d) + -> (DeltaM M {functorM} {monadM} A v) -> (A -> DeltaM M {functorM} {monadM} B v) -> DeltaM M {functorM} {monadM} B v +deltaM-bind {v = init} {monadM = mm} (deltaM (mono x)) f = deltaM (mono (bind mm x (headDeltaM ∙ f))) +deltaM-bind {v = commit v} {monadM = mm} (deltaM (delta x d)) f = appendDeltaM (deltaM (mono (bind mm x (headDeltaM ∙ f)))) + (deltaM-bind (deltaM d) (tailDeltaM ∙ f)) + + +deltaM-mu : {l : Level} {A : Set l} {v : Rev} + {M : {l' : Level} -> Set l' -> Set l'} + {functorM : {l' : Level} -> Functor {l'} M} + {monadM : {l' : Level} -> Monad {l'} M functorM} + -> (DeltaM M {functorM} {monadM} (DeltaM M {functorM} {monadM} A v) v) -> DeltaM M {functorM} {monadM} A v +deltaM-mu d = deltaM-bind d id