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

Changing foldRX to mapX
author Adam Chlipala <adamc@hcoop.net>
date Sun, 28 Feb 2010 13:06:10 -0500
parents 8d3aa6c7cee0
children 79f487f51d9f
comparison
equal deleted inserted replaced
1171:7a2a7a8f9cab 1172:ad15700272f6
49 acc' <- acc (r1 -- nm) (r2 -- nm) (r3 -- nm); 49 acc' <- acc (r1 -- nm) (r2 -- nm) (r3 -- nm);
50 f [nm] [t] [rest] ! r1.nm r2.nm r3.nm acc') 50 f [nm] [t] [rest] ! r1.nm r2.nm r3.nm acc')
51 (fn _ _ _ => return i) 51 (fn _ _ _ => return i)
52 fl 52 fl
53 53
54 fun mapR0 [K] [m] (_ : monad m) [tr :: K -> Type]
55 (f : nm :: Name -> t :: K -> m (tr t)) [r ::: {K}] (fl : folder r) =
56 @Top.fold [fn r => m ($(map tr r))]
57 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] (acc : m ($(map tr rest))) =>
58 v <- f [nm] [t];
59 vs <- acc;
60 return (vs ++ {nm = v}))
61 (return {})
62 fl
63
54 fun mapR [K] [m] (_ : monad m) [tf :: K -> Type] [tr :: K -> Type] 64 fun mapR [K] [m] (_ : monad m) [tf :: K -> Type] [tr :: K -> Type]
55 (f : nm :: Name -> t :: K -> tf t -> m (tr t)) = 65 (f : nm :: Name -> t :: K -> tf t -> m (tr t)) =
56 @@foldR [m] _ [tf] [fn r => $(map tr r)] 66 @@foldR [m] _ [tf] [fn r => $(map tr r)]
57 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] (v : tf t) 67 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] (v : tf t)
58 (acc : $(map tr rest)) => 68 (acc : $(map tr rest)) =>