# HG changeset patch # User Adam Chlipala # Date 1267380370 18000 # Node ID ad15700272f6bf0bd3c079638daa55d4a4c9de06 # Parent 7a2a7a8f9cab3d249e5fc6cf39ed6740bdc0b0b1 Changing foldRX to mapX diff -r 7a2a7a8f9cab -r ad15700272f6 demo/batchFun.ur --- a/demo/batchFun.ur Sat Feb 27 16:49:11 2010 -0500 +++ b/demo/batchFun.ur Sun Feb 28 13:06:10 2010 -0500 @@ -72,7 +72,7 @@ | 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 @@ - {@foldRX [colMeta] [_] + {@mapX [colMeta] [_] (fn [nm :: Name] [p :: (Type * Type)] [rest :: {(Type * Type)}] [[nm] ~ rest] m => ) @@ -144,7 +144,7 @@
Id{[m.Nam]}
- {@foldRX2 [colMeta] [snd] [_] + {@mapX2 [colMeta] [snd] [_] (fn [nm :: Name] [p :: (Type * Type)] [rest :: {(Type * Type)}] [[nm] ~ rest] m s => ) diff -r 7a2a7a8f9cab -r ad15700272f6 demo/crud.ur --- a/demo/crud.ur Sat Feb 27 16:49:11 2010 -0500 +++ b/demo/crud.ur Sun Feb 28 13:06:10 2010 -0500 @@ -50,7 +50,7 @@ (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 @@
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 -r 7a2a7a8f9cab -r ad15700272f6 demo/more/grid.ur --- a/demo/more/grid.ur Sat Feb 27 16:49:11 2010 -0500 +++ b/demo/more/grid.ur Sun Feb 28 13:06:10 2010 -0500 @@ -123,7 +123,7 @@
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 -r 7a2a7a8f9cab -r ad15700272f6 lib/ur/monad.ur --- a/lib/ur/monad.ur Sat Feb 27 16:49:11 2010 -0500 +++ b/lib/ur/monad.ur Sun Feb 28 13:06:10 2010 -0500 @@ -51,6 +51,16 @@ (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 -r 7a2a7a8f9cab -r ad15700272f6 lib/ur/monad.urs --- a/lib/ur/monad.urs Sat Feb 27 16:49:11 2010 -0500 +++ b/lib/ur/monad.urs Sun Feb 28 13:06:10 2010 -0500 @@ -34,6 +34,11 @@ -> 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 -r 7a2a7a8f9cab -r ad15700272f6 lib/ur/top.ur --- a/lib/ur/top.ur Sat Feb 27 16:49:11 2010 -0500 +++ b/lib/ur/top.ur Sun Feb 28 13:06:10 2010 -0500 @@ -179,7 +179,14 @@ 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 @@ {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 @@ {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 -r 7a2a7a8f9cab -r ad15700272f6 lib/ur/top.urs --- a/lib/ur/top.urs Sat Feb 27 16:49:11 2010 -0500 +++ b/lib/ur/top.urs Sun Feb 28 13:06:10 2010 -0500 @@ -98,25 +98,30 @@ -> 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 mapUX : tf :: Type -> ctx :: {Unit} + -> (nm :: Name -> rest :: {Unit} -> [[nm] ~ rest] => + tf -> xml ctx [] []) + -> r ::: {Unit} -> folder r -> $(mapU 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 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 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 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] =>
@@ -208,7 +208,7 @@ @@ -260,14 +260,14 @@ M.aggFolder M.aggregates) grid.Rows; return
Aggregates{meta.Display acc}
Filters{(meta.Handlers state).DisplayFilter filter}