comparison lib/ur/monad.ur @ 1312:726f0caeea3f

Monad.appR
author Adam Chlipala <adam@chlipala.net>
date Tue, 19 Oct 2010 11:51:53 -0400
parents f0909fb3848f
children 0bf73c3e4563
comparison
equal deleted inserted replaced
1311:5337adf33a4a 1312:726f0caeea3f
91 p' <- f [nm] [t] [rest] ! r.nm p.2; 91 p' <- f [nm] [t] [rest] ! r.nm p.2;
92 return ({nm = p'.1} ++ p.1, p'.2)) 92 return ({nm = p'.1} ++ p.1, p'.2))
93 (fn _ => return ({}, i)) 93 (fn _ => return ({}, i))
94 fl 94 fl
95 95
96 fun appR [K] [m] (_ : monad m) [tf :: K -> Type]
97 (f : nm :: Name -> t :: K -> tf t -> m unit)
98 [r ::: {K}] (fl : folder r) =
99 @Top.fold [fn r :: {K} => $(map tf r) -> m unit]
100 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] acc r =>
101 acc (r -- nm);
102 f [nm] [t] r.nm)
103 (fn _ => return ())
104 fl
105
96 fun appR2 [K] [m] (_ : monad m) [tf1 :: K -> Type] [tf2 :: K -> Type] 106 fun appR2 [K] [m] (_ : monad m) [tf1 :: K -> Type] [tf2 :: K -> Type]
97 (f : nm :: Name -> t :: K -> tf1 t -> tf2 t -> m unit) 107 (f : nm :: Name -> t :: K -> tf1 t -> tf2 t -> m unit)
98 [r ::: {K}] (fl : folder r) = 108 [r ::: {K}] (fl : folder r) =
99 @Top.fold [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> m unit] 109 @Top.fold [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> m unit]
100 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] acc r1 r2 => 110 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] acc r1 r2 =>