Mercurial > urweb

comparison lib/top.ur @ 367:28d3d7210687

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Improving indentation of XML after antiquote
author Adam Chlipala <adamc@hcoop.net>
date Thu, 16 Oct 2008 13:30:40 -0400
parents c1e96b387115
children 8084fa9216de
comparison
equal deleted inserted replaced
366:3004f8843e36 367:28d3d7210687
32 [[nm] ~ rest] r => 32 [[nm] ~ rest] r =>
33 f [nm] [t] [rest] r.nm (acc (r -- nm))) 33 f [nm] [t] [rest] r.nm (acc (r -- nm)))
34 (fn _ => i) 34 (fn _ => i)
35 35
36 fun foldT2R (tf :: (Type * Type) -> Type) (tr :: {(Type * Type)} -> Type) 36 fun foldT2R (tf :: (Type * Type) -> Type) (tr :: {(Type * Type)} -> Type)
37 (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} 37 (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)}
38 -> fn [[nm] ~ rest] => 38 -> fn [[nm] ~ rest] =>
39 tf t -> tr rest -> tr ([nm = t] ++ rest)) 39 tf t -> tr rest -> tr ([nm = t] ++ rest))
40 (i : tr []) = 40 (i : tr []) =
41 fold [fn r :: {(Type * Type)} => $(mapT2T tf r) -> tr r] 41 fold [fn r :: {(Type * Type)} => $(mapT2T tf r) -> tr r]
42 (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)}) 42 (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)})
43 (acc : _ -> tr rest) [[nm] ~ rest] r => 43 (acc : _ -> tr rest) [[nm] ~ rest] r =>
44 f [nm] [t] [rest] r.nm (acc (r -- nm))) 44 f [nm] [t] [rest] r.nm (acc (r -- nm)))
45 (fn _ => i) 45 (fn _ => i)
46 46
47 fun foldTR2 (tf1 :: Type -> Type) (tf2 :: Type -> Type) (tr :: {Type} -> Type) 47 fun foldTR2 (tf1 :: Type -> Type) (tf2 :: Type -> Type) (tr :: {Type} -> Type)
48 (f : nm :: Name -> t :: Type -> rest :: {Type} 48 (f : nm :: Name -> t :: Type -> rest :: {Type}
49 -> fn [[nm] ~ rest] => 49 -> fn [[nm] ~ rest] =>
50 tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) 50 tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
51 (i : tr []) = 51 (i : tr []) =
52 fold [fn r :: {Type} => $(mapTT tf1 r) -> $(mapTT tf2 r) -> tr r] 52 fold [fn r :: {Type} => $(mapTT tf1 r) -> $(mapTT tf2 r) -> tr r]
53 (fn (nm :: Name) (t :: Type) (rest :: {Type}) 53 (fn (nm :: Name) (t :: Type) (rest :: {Type})
54 (acc : _ -> _ -> tr rest) [[nm] ~ rest] r1 r2 => 54 (acc : _ -> _ -> tr rest) [[nm] ~ rest] r1 r2 =>
55 f [nm] [t] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm))) 55 f [nm] [t] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm)))
56 (fn _ _ => i) 56 (fn _ _ => i)