Mercurial > urweb

comparison lib/ur/top.ur @ 630:6a6eb9882d57

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Top.Fold.mp
author Adam Chlipala <adamc@hcoop.net>
date Tue, 24 Feb 2009 13:50:39 -0500
parents e68de2a5506b
children effa7d43aac3
comparison
equal deleted inserted replaced
629:e68de2a5506b 630:6a6eb9882d57
27 f1 [fn r1' => [r1' ~ r2] => tf (r1' ++ r2)] 27 f1 [fn r1' => [r1' ~ r2] => tf (r1' ++ r2)]
28 (fn (nm :: Name) (v :: K) (r1' :: {K}) (acc : [r1' ~ r2] => tf (r1' ++ r2)) 28 (fn (nm :: Name) (v :: K) (r1' :: {K}) (acc : [r1' ~ r2] => tf (r1' ++ r2))
29 [[nm] ~ r1'] [[nm = v] ++ r1' ~ r2] => 29 [[nm] ~ r1'] [[nm = v] ++ r1' ~ r2] =>
30 f [nm] [v] [r1' ++ r2] acc !) 30 f [nm] [v] [r1' ++ r2] acc !)
31 (fn [[] ~ r2] => f2 [tf] f i) ! 31 (fn [[] ~ r2] => f2 [tf] f i) !
32
33 fun mp K1 K2 (f ::: K1 -> K2) (r ::: {K1})
34 (fold : folder r)
35 (tf :: {K2} -> Type)
36 (f : nm :: Name -> v :: K2 -> r :: {K2} -> tf r
37 -> [[nm] ~ r] => tf ([nm = v] ++ r))
38 (i : tf []) =
39 fold [fn r => tf (map f r)]
40 (fn (nm :: Name) (v :: K1) (rest :: {K1}) (acc : tf (map f rest)) [[nm] ~ rest] =>
41 f [nm] [f v] [map f rest] acc !)
42 i
32 end 43 end
33 44
34 45
35 fun not b = if b then False else True 46 fun not b = if b then False else True
36 47