Mercurial > urweb
comparison lib/ur/monad.ur @ 2272:b49d22a4eda8
Merge.
author | Ziv Scully <ziv@mit.edu> |
---|---|
date | Sat, 31 Oct 2015 23:35:42 -0400 |
parents | cbd294994c69 |
children |
comparison
equal
deleted
inserted
replaced
2271:85f91c7452b0 | 2272:b49d22a4eda8 |
---|---|
79 (acc : $(map tr rest)) => | 79 (acc : $(map tr rest)) => |
80 v' <- f [nm] [t] v1 v2; | 80 v' <- f [nm] [t] v1 v2; |
81 return (acc ++ {nm = v'})) | 81 return (acc ++ {nm = v'})) |
82 {} | 82 {} |
83 | 83 |
84 fun mapR3 [K] [m] (_ : monad m) [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type] [tr :: K -> Type] | |
85 (f : nm :: Name -> t :: K -> tf1 t -> tf2 t -> tf3 t -> m (tr t)) = | |
86 @@foldR3 [m] _ [tf1] [tf2] [tf3] [fn r => $(map tr r)] | |
87 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] (v1 : tf1 t) (v2 : tf2 t) (v3 : tf3 t) | |
88 (acc : $(map tr rest)) => | |
89 v' <- f [nm] [t] v1 v2 v3; | |
90 return (acc ++ {nm = v'})) | |
91 {} | |
92 | |
84 fun foldMapR [K] [m] (_ : monad m) [tf :: K -> Type] [tf' :: K -> Type] [tr :: {K} -> Type] | 93 fun foldMapR [K] [m] (_ : monad m) [tf :: K -> Type] [tf' :: K -> Type] [tr :: {K} -> Type] |
85 (f : nm :: Name -> t :: K -> rest :: {K} | 94 (f : nm :: Name -> t :: K -> rest :: {K} |
86 -> [[nm] ~ rest] => | 95 -> [[nm] ~ rest] => |
87 tf t -> tr rest -> m (tf' t * tr ([nm = t] ++ rest))) | 96 tf t -> tr rest -> m (tf' t * tr ([nm = t] ++ rest))) |
88 (i : tr []) [r ::: {K}] (fl : folder r) = | 97 (i : tr []) [r ::: {K}] (fl : folder r) = |