Mercurial > urweb
comparison lib/ur/monad.ur @ 1175:79f487f51d9f
Monad.foldMapR
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Tue, 02 Mar 2010 10:33:49 -0500 |
parents | ad15700272f6 |
children | fd1a49b51db5 |
comparison
equal
deleted
inserted
replaced
1174:9df124fcab3d | 1175:79f487f51d9f |
---|---|
76 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] (v1 : tf1 t) (v2 : tf2 t) | 76 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] (v1 : tf1 t) (v2 : tf2 t) |
77 (acc : $(map tr rest)) => | 77 (acc : $(map tr rest)) => |
78 v' <- f [nm] [t] v1 v2; | 78 v' <- f [nm] [t] v1 v2; |
79 return (acc ++ {nm = v'})) | 79 return (acc ++ {nm = v'})) |
80 {} | 80 {} |
81 | |
82 fun foldMapR [K] [m] (_ : monad m) [tf :: K -> Type] [tf' :: K -> Type] [tr :: {K} -> Type] | |
83 (f : nm :: Name -> t :: K -> rest :: {K} | |
84 -> [[nm] ~ rest] => | |
85 tf t -> tr rest -> m (tf' t * tr ([nm = t] ++ rest))) | |
86 (i : tr []) [r ::: {K}] (fl : folder r) = | |
87 @Top.fold [fn r :: {K} => $(map tf r) -> m ($(map tf' r) * tr r)] | |
88 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] | |
89 (acc : _ -> m ($(map tf' rest) * tr rest)) r => | |
90 p <- acc (r -- nm); | |
91 p' <- f [nm] [t] [rest] ! r.nm p.2; | |
92 return ({nm = p'.1} ++ p.1, p'.2)) | |
93 (fn _ => return ({}, i)) | |
94 fl |