comparison lib/ur/top.ur @ 905:7a4b026e45dd

Library improvements; proper list [un]urlification; remove server-side ServerCalls; eta reduction in type inference
author Adam Chlipala <adamc@hcoop.net>
date Sun, 09 Aug 2009 16:13:27 -0400
parents d1d0b18afd3d
children 8e540df3294d
comparison
equal deleted inserted replaced
904:6d9538ce94d8 905:7a4b026e45dd
96 fl [fn r :: {K} => $(map tf1 r) -> $(map tf2 r)] 96 fl [fn r :: {K} => $(map tf1 r) -> $(map tf2 r)]
97 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] acc r => 97 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] acc r =>
98 acc (r -- nm) ++ {nm = f r.nm}) 98 acc (r -- nm) ++ {nm = f r.nm})
99 (fn _ => {}) 99 (fn _ => {})
100 100
101 fun map2 [K1] [K2] [tf1 :: K1 -> Type] [tf2 :: K2 -> Type] [tf :: K1 -> K2] 101 fun map2 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type]
102 (f : t ::: K1 -> tf1 t -> tf2 (tf t)) [r :: {K1}] (fl : folder r) = 102 (f : t ::: K -> tf1 t -> tf2 t -> tf3 t) [r :: {K}] (fl : folder r) =
103 fl [fn r :: {K1} => $(map tf1 r) -> $(map tf2 (map tf r))] 103 fl [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r)]
104 (fn [nm :: Name] [t :: K1] [rest :: {K1}] [[nm] ~ rest] acc r => 104 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] acc r1 r2 =>
105 acc (r -- nm) ++ {nm = f r.nm}) 105 acc (r1 -- nm) (r2 -- nm) ++ {nm = f r1.nm r2.nm})
106 (fn _ => {}) 106 (fn _ _ => {})
107 107
108 fun foldUR [tf :: Type] [tr :: {Unit} -> Type] 108 fun foldUR [tf :: Type] [tr :: {Unit} -> Type]
109 (f : nm :: Name -> rest :: {Unit} 109 (f : nm :: Name -> rest :: {Unit}
110 -> [[nm] ~ rest] => 110 -> [[nm] ~ rest] =>
111 tf -> tr rest -> tr ([nm] ++ rest)) 111 tf -> tr rest -> tr ([nm] ++ rest))