Mercurial > urweb

comparison lib/ur/top.ur @ 1172:ad15700272f6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Changing foldRX to mapX
author Adam Chlipala <adamc@hcoop.net>
date Sun, 28 Feb 2010 13:06:10 -0500
parents 7fc4e0087e50
children 983d9b38abc7
comparison
equal deleted inserted replaced
1171:7a2a7a8f9cab 1172:ad15700272f6
177 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] 177 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest]
178 (acc : _ -> _ -> _ -> tr rest) r1 r2 r3 => 178 (acc : _ -> _ -> _ -> tr rest) r1 r2 r3 =>
179 f [nm] [t] [rest] ! r1.nm r2.nm r3.nm (acc (r1 -- nm) (r2 -- nm) (r3 -- nm))) 179 f [nm] [t] [rest] ! r1.nm r2.nm r3.nm (acc (r1 -- nm) (r2 -- nm) (r3 -- nm)))
180 (fn _ _ _ => i) 180 (fn _ _ _ => i)
181 181
182 fun foldRX [K] [tf :: K -> Type] [ctx :: {Unit}] 182 fun mapUX [tf :: Type] [ctx :: {Unit}]
183 (f : nm :: Name -> rest :: {Unit} -> [[nm] ~ rest] => tf -> xml ctx [] []) =
184 @@foldR [fn _ => tf] [fn _ => xml ctx [] []]
185 (fn [nm :: Name] [u :: Unit] [rest :: {Unit}] [[nm] ~ rest] r acc =>
186 <xml>{f [nm] [rest] ! r}{acc}</xml>)
187 <xml/>
188
189 fun mapX [K] [tf :: K -> Type] [ctx :: {Unit}]
183 (f : nm :: Name -> t :: K -> rest :: {K} 190 (f : nm :: Name -> t :: K -> rest :: {K}
184 -> [[nm] ~ rest] => 191 -> [[nm] ~ rest] =>
185 tf t -> xml ctx [] []) = 192 tf t -> xml ctx [] []) =
186 @@foldR [tf] [fn _ => xml ctx [] []] 193 @@foldR [tf] [fn _ => xml ctx [] []]
187 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] r acc => 194 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] r acc =>
188 <xml>{f [nm] [t] [rest] ! r}{acc}</xml>) 195 <xml>{f [nm] [t] [rest] ! r}{acc}</xml>)
189 <xml/> 196 <xml/>
190 197
191 fun foldRX2 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [ctx :: {Unit}] 198 fun mapX2 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [ctx :: {Unit}]
192 (f : nm :: Name -> t :: K -> rest :: {K} 199 (f : nm :: Name -> t :: K -> rest :: {K}
193 -> [[nm] ~ rest] => 200 -> [[nm] ~ rest] =>
194 tf1 t -> tf2 t -> xml ctx [] []) = 201 tf1 t -> tf2 t -> xml ctx [] []) =
195 @@foldR2 [tf1] [tf2] [fn _ => xml ctx [] []] 202 @@foldR2 [tf1] [tf2] [fn _ => xml ctx [] []]
196 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] 203 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest]
197 r1 r2 acc => 204 r1 r2 acc =>
198 <xml>{f [nm] [t] [rest] ! r1 r2}{acc}</xml>) 205 <xml>{f [nm] [t] [rest] ! r1 r2}{acc}</xml>)
199 <xml/> 206 <xml/>
200 207
201 fun foldRX3 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type] [ctx :: {Unit}] 208 fun mapX3 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type] [ctx :: {Unit}]
202 (f : nm :: Name -> t :: K -> rest :: {K} 209 (f : nm :: Name -> t :: K -> rest :: {K}
203 -> [[nm] ~ rest] => 210 -> [[nm] ~ rest] =>
204 tf1 t -> tf2 t -> tf3 t -> xml ctx [] []) = 211 tf1 t -> tf2 t -> tf3 t -> xml ctx [] []) =
205 @@foldR3 [tf1] [tf2] [tf3] [fn _ => xml ctx [] []] 212 @@foldR3 [tf1] [tf2] [tf3] [fn _ => xml ctx [] []]
206 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] 213 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest]