Mercurial > urweb
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)) => |