Mercurial > meta
diff variant.ur @ 20:296807a9fd50
Variant.foldR and appR
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Mon, 02 Jan 2012 17:23:31 -0500 |
parents | 744bf911dcc6 |
children | e7d64ea0f922 |
line wrap: on
line diff
--- a/variant.ur Sat Dec 31 15:49:54 2011 -0500 +++ b/variant.ur Mon Jan 02 17:23:31 2012 -0500 @@ -54,6 +54,17 @@ f' (make [nm] {}) (acc [[nm] ++ r'] f' acc')) (fn [r' ::_] [[] ~ r'] _ x => x) fl [[]] ! f +fun foldR [tr] [r] [t] (fl : folder r) (f : variant (mapU {} r) -> tr -> t -> t) (record : $(mapU tr r)) : t -> t = + @Top.foldUR [tr] [fn r => r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> tr -> t -> t) -> t -> t] + (fn [nm :: Name] [r ::_] [[nm] ~ r] (v : tr) + (acc : r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> tr -> t -> t) -> t -> t) + [r' ::_] [[nm] ++ r ~ r'] f' acc' => + f' (make [nm] {}) v (acc [[nm] ++ r'] f' acc')) + (fn [r' ::_] [[] ~ r'] _ x => x) fl record [[]] ! f + +fun appR [m] (_ : monad m) [tr] [r] (fl : folder r) (f : variant (mapU {} r) -> tr -> m {}) (record : $(mapU tr r)) : m {} = + @foldR fl (fn var this acc => f var this; acc) record (return ()) + fun destrR [K] [f :: K -> Type] [fr :: K -> Type] [t ::: Type] (f : p :: K -> f p -> fr p -> t) [r ::: {K}] (fl : folder r) (v : variant (map f r)) (r : $(map fr r)) : t = @@ -66,7 +77,7 @@ (f : p :: K -> f1 p -> f2 p -> fr p -> t) [r ::: {K}] (fl : folder r) (v1 : variant (map f1 r)) (v2 : variant (map f2 r)) (r : $(map fr r)) : option t = match v1 - (@foldR [fr] [fn r => others :: {K} -> [others ~ r] => + (@Top.foldR [fr] [fn r => others :: {K} -> [others ~ r] => folder (r ++ others) -> variant (map f2 (r ++ others)) -> $(map (fn p => f1 p -> option t) r)]