From 703c91af7525838dff97f88245bf7482745e771e Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 28 Feb 2010 13:06:10 -0500 Subject: Changing foldRX to mapX --- demo/batchFun.ur | 6 +++--- demo/crud.ur | 4 ++-- demo/more/grid.ur | 8 ++++---- lib/ur/monad.ur | 10 ++++++++++ lib/ur/monad.urs | 5 +++++ lib/ur/top.ur | 13 ++++++++++--- lib/ur/top.urs | 43 ++++++++++++++++++++++++------------------- 7 files changed, 58 insertions(+), 31 deletions(-) diff --git a/demo/batchFun.ur b/demo/batchFun.ur index 3f0317a8..f665b132 100644 --- a/demo/batchFun.ur +++ b/demo/batchFun.ur @@ -72,7 +72,7 @@ functor Make(M : sig | Cons (r, ls) => {[r.Id]} - {@foldRX2 [colMeta] [fst] [_] + {@mapX2 [colMeta] [fst] [_] (fn [nm :: Name] [p :: (Type * Type)] [rest :: {(Type * Type)}] [[nm] ~ rest] m v => {m.Show v}) @@ -88,7 +88,7 @@ functor Make(M : sig - {@foldRX [colMeta] [_] + {@mapX [colMeta] [_] (fn [nm :: Name] [p :: (Type * Type)] [rest :: {(Type * Type)}] [[nm] ~ rest] m => ) @@ -144,7 +144,7 @@ functor Make(M : sig
Id{[m.Nam]}
- {@foldRX2 [colMeta] [snd] [_] + {@mapX2 [colMeta] [snd] [_] (fn [nm :: Name] [p :: (Type * Type)] [rest :: {(Type * Type)}] [[nm] ~ rest] m s => ) diff --git a/demo/crud.ur b/demo/crud.ur index bccc3822..7850e656 100644 --- a/demo/crud.ur +++ b/demo/crud.ur @@ -50,7 +50,7 @@ functor Make(M : sig (fn (fs : {T : $([Id = int] ++ map fst M.cols)}) => - {@foldRX2 [fst] [colMeta] [tr] + {@mapX2 [fst] [colMeta] [tr] (fn [nm :: Name] [t :: (Type * Type)] [rest :: {(Type * Type)}] [[nm] ~ rest] v col => @@ -66,7 +66,7 @@ functor Make(M : sig
Id:
{[m.Nam]}: {m.Widget s}
{[fs.T.Id]}{col.Show v}
- {@foldRX [colMeta] [tr] + {@mapX [colMeta] [tr] (fn [nm :: Name] [t :: (Type * Type)] [rest :: {(Type * Type)}] [[nm] ~ rest] col => diff --git a/demo/more/grid.ur b/demo/more/grid.ur index 7540ca27..d560c556 100644 --- a/demo/more/grid.ur +++ b/demo/more/grid.ur @@ -123,7 +123,7 @@ functor Make(M : sig
ID{cdata col.Nam}
- {@foldRX2 [fst3] [colMeta M.row] [_] + {@mapX2 [fst3] [colMeta M.row] [_] (fn [nm :: Name] [p :: (Type * Type * Type)] [rest :: {(Type * Type * Type)}] [[nm] ~ rest] data (meta : colMeta M.row p) => - {@foldRX2 [aggregateMeta M.row] [id] [_] + {@mapX2 [aggregateMeta M.row] [id] [_] (fn [nm :: Name] [t :: Type] [rest :: {Type}] [[nm] ~ rest] meta acc => ) M.aggFolder M.aggregates rows} }/> - {@foldRX3 [colMeta M.row] [fst3] [thd3] [_] + {@mapX3 [colMeta M.row] [fst3] [thd3] [_] (fn [nm :: Name] [p :: (Type * Type * Type)] [rest :: {(Type * Type * Type)}] [[nm] ~ rest] meta state filter => ) M.folder M.cols grid.Cols grid.Filters} diff --git a/lib/ur/monad.ur b/lib/ur/monad.ur index e15da523..689e6b26 100644 --- a/lib/ur/monad.ur +++ b/lib/ur/monad.ur @@ -51,6 +51,16 @@ fun foldR3 [K] [m] (_ : monad m) [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K (fn _ _ _ => return i) fl +fun mapR0 [K] [m] (_ : monad m) [tr :: K -> Type] + (f : nm :: Name -> t :: K -> m (tr t)) [r ::: {K}] (fl : folder r) = + @Top.fold [fn r => m ($(map tr r))] + (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] (acc : m ($(map tr rest))) => + v <- f [nm] [t]; + vs <- acc; + return (vs ++ {nm = v})) + (return {}) + fl + fun mapR [K] [m] (_ : monad m) [tf :: K -> Type] [tr :: K -> Type] (f : nm :: Name -> t :: K -> tf t -> m (tr t)) = @@foldR [m] _ [tf] [fn r => $(map tr r)] diff --git a/lib/ur/monad.urs b/lib/ur/monad.urs index 698a4b5b..05f201e0 100644 --- a/lib/ur/monad.urs +++ b/lib/ur/monad.urs @@ -34,6 +34,11 @@ val foldR3 : K --> m ::: (Type -> Type) -> monad m -> tr [] -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> m (tr r) +val mapR0 : K --> m ::: (Type -> Type) -> monad m + -> tr :: (K -> Type) + -> (nm :: Name -> t :: K -> m (tr t)) + -> r ::: {K} -> folder r -> m ($(map tr r)) + val mapR : K --> m ::: (Type -> Type) -> monad m -> tf :: (K -> Type) -> tr :: (K -> Type) diff --git a/lib/ur/top.ur b/lib/ur/top.ur index 613f5ec5..703c7bae 100644 --- a/lib/ur/top.ur +++ b/lib/ur/top.ur @@ -179,7 +179,14 @@ fun foldR3 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type] [tr :: { f [nm] [t] [rest] ! r1.nm r2.nm r3.nm (acc (r1 -- nm) (r2 -- nm) (r3 -- nm))) (fn _ _ _ => i) -fun foldRX [K] [tf :: K -> Type] [ctx :: {Unit}] +fun mapUX [tf :: Type] [ctx :: {Unit}] + (f : nm :: Name -> rest :: {Unit} -> [[nm] ~ rest] => tf -> xml ctx [] []) = + @@foldR [fn _ => tf] [fn _ => xml ctx [] []] + (fn [nm :: Name] [u :: Unit] [rest :: {Unit}] [[nm] ~ rest] r acc => + {f [nm] [rest] ! r}{acc}) + + +fun mapX [K] [tf :: K -> Type] [ctx :: {Unit}] (f : nm :: Name -> t :: K -> rest :: {K} -> [[nm] ~ rest] => tf t -> xml ctx [] []) = @@ -188,7 +195,7 @@ fun foldRX [K] [tf :: K -> Type] [ctx :: {Unit}] {f [nm] [t] [rest] ! r}{acc}) -fun foldRX2 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [ctx :: {Unit}] +fun mapX2 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [ctx :: {Unit}] (f : nm :: Name -> t :: K -> rest :: {K} -> [[nm] ~ rest] => tf1 t -> tf2 t -> xml ctx [] []) = @@ -198,7 +205,7 @@ fun foldRX2 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [ctx :: {Unit}] {f [nm] [t] [rest] ! r1 r2}{acc}) -fun foldRX3 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type] [ctx :: {Unit}] +fun mapX3 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type] [ctx :: {Unit}] (f : nm :: Name -> t :: K -> rest :: {K} -> [[nm] ~ rest] => tf1 t -> tf2 t -> tf3 t -> xml ctx [] []) = diff --git a/lib/ur/top.urs b/lib/ur/top.urs index 743669ce..de2ac03b 100644 --- a/lib/ur/top.urs +++ b/lib/ur/top.urs @@ -98,25 +98,30 @@ val foldR3 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type -> tr [] -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> tr r -val foldRX : K --> tf :: (K -> Type) -> ctx :: {Unit} - -> (nm :: Name -> t :: K -> rest :: {K} - -> [[nm] ~ rest] => - tf t -> xml ctx [] []) - -> r ::: {K} -> folder r -> $(map tf r) -> xml ctx [] [] - -val foldRX2 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> ctx :: {Unit} - -> (nm :: Name -> t :: K -> rest :: {K} - -> [[nm] ~ rest] => - tf1 t -> tf2 t -> xml ctx [] []) - -> r ::: {K} -> folder r - -> $(map tf1 r) -> $(map tf2 r) -> xml ctx [] [] - -val foldRX3 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type) -> ctx :: {Unit} - -> (nm :: Name -> t :: K -> rest :: {K} - -> [[nm] ~ rest] => - tf1 t -> tf2 t -> tf3 t -> xml ctx [] []) - -> r ::: {K} -> folder r - -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> xml ctx [] [] +val mapUX : tf :: Type -> ctx :: {Unit} + -> (nm :: Name -> rest :: {Unit} -> [[nm] ~ rest] => + tf -> xml ctx [] []) + -> r ::: {Unit} -> folder r -> $(mapU tf r) -> xml ctx [] [] + +val mapX : K --> tf :: (K -> Type) -> ctx :: {Unit} + -> (nm :: Name -> t :: K -> rest :: {K} + -> [[nm] ~ rest] => + tf t -> xml ctx [] []) + -> r ::: {K} -> folder r -> $(map tf r) -> xml ctx [] [] + +val mapX2 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> ctx :: {Unit} + -> (nm :: Name -> t :: K -> rest :: {K} + -> [[nm] ~ rest] => + tf1 t -> tf2 t -> xml ctx [] []) + -> r ::: {K} -> folder r + -> $(map tf1 r) -> $(map tf2 r) -> xml ctx [] [] + +val mapX3 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type) -> ctx :: {Unit} + -> (nm :: Name -> t :: K -> rest :: {K} + -> [[nm] ~ rest] => + tf1 t -> tf2 t -> tf3 t -> xml ctx [] []) + -> r ::: {K} -> folder r + -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> xml ctx [] [] val queryL : tables ::: {{Type}} -> exps ::: {Type} -> [tables ~ exps] => -- cgit v1.2.3
@@ -208,7 +208,7 @@ functor Make(M : sig @@ -260,14 +260,14 @@ functor Make(M : sig M.aggFolder M.aggregates) grid.Rows; return
Aggregates{meta.Display acc}
Filters{(meta.Handlers state).DisplayFilter filter}