Mercurial > urweb

annotate lib/ur/monad.ur @ 2282:19b233bb3176

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Make cache flushes safe for transactions (not sure about LRU bump on read).
author Ziv Scully <ziv@mit.edu>
date Thu, 12 Nov 2015 09:47:20 -0500
parents cbd294994c69
children
rev   line source
adamc@834 1 fun exec [m ::: Type -> Type] (_ : monad m) [ts ::: {Type}] r (fd : folder ts) =
adamc@1093 2 @foldR [m] [fn ts => m $ts]
adamc@1093 3 (fn [nm :: Name] [v :: Type] [rest :: {Type}] [[nm] ~ rest] action acc =>
adamc@1093 4 this <- action;
adamc@1093 5 others <- acc;
adamc@1093 6 return ({nm = this} ++ others))
adamc@1093 7 (return {}) fd r
adamc@898 8
adamc@898 9 fun ignore [m ::: Type -> Type] (_ : monad m) [t] (v : m t) = x <- v; return ()
adamc@905 10
adamc@917 11 fun mp [m] (_ : monad m) [a] [b] f m =
adamc@917 12 v <- m;
adamc@917 13 return (f v)
adamc@917 14
adam@1768 15 val liftM = @@mp
adam@1768 16
adamc@905 17 fun foldR [K] [m] (_ : monad m) [tf :: K -> Type] [tr :: {K} -> Type]
adamc@905 18 (f : nm :: Name -> t :: K -> rest :: {K}
adamc@905 19 -> [[nm] ~ rest] =>
adamc@905 20 tf t -> tr rest -> m (tr ([nm = t] ++ rest)))
adamc@1093 21 (i : tr []) [r ::: {K}] (fl : folder r) =
adamc@1093 22 @Top.fold [fn r :: {K} => $(map tf r) -> m (tr r)]
adamc@1093 23 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest]
adamc@1093 24 (acc : _ -> m (tr rest)) r =>
adamc@1093 25 acc' <- acc (r -- nm);
adam@1472 26 f [nm] [t] [rest] r.nm acc')
adamc@1093 27 (fn _ => return i)
adamc@1093 28 fl
adamc@905 29
adamc@905 30 fun foldR2 [K] [m] (_ : monad m) [tf1 :: K -> Type] [tf2 :: K -> Type] [tr :: {K} -> Type]
adamc@905 31 (f : nm :: Name -> t :: K -> rest :: {K}
adamc@905 32 -> [[nm] ~ rest] =>
adamc@905 33 tf1 t -> tf2 t -> tr rest -> m (tr ([nm = t] ++ rest)))
adamc@1093 34 (i : tr []) [r ::: {K}] (fl : folder r) =
adamc@1093 35 @Top.fold [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> m (tr r)]
adamc@1093 36 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest]
adamc@1093 37 (acc : _ -> _ -> m (tr rest)) r1 r2 =>
adamc@1093 38 acc' <- acc (r1 -- nm) (r2 -- nm);
adam@1472 39 f [nm] [t] [rest] r1.nm r2.nm acc')
adamc@1093 40 (fn _ _ => return i)
adamc@1093 41 fl
adamc@905 42
adamc@910 43 fun foldR3 [K] [m] (_ : monad m) [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type] [tr :: {K} -> Type]
adamc@910 44 (f : nm :: Name -> t :: K -> rest :: {K}
adamc@910 45 -> [[nm] ~ rest] =>
adamc@910 46 tf1 t -> tf2 t -> tf3 t -> tr rest -> m (tr ([nm = t] ++ rest)))
adamc@1093 47 (i : tr []) [r ::: {K}] (fl : folder r) =
adamc@1093 48 @Top.fold [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> m (tr r)]
adamc@1093 49 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest]
adamc@1093 50 (acc : _ -> _ -> _ -> m (tr rest)) r1 r2 r3 =>
adamc@1093 51 acc' <- acc (r1 -- nm) (r2 -- nm) (r3 -- nm);
adam@1472 52 f [nm] [t] [rest] r1.nm r2.nm r3.nm acc')
adamc@1093 53 (fn _ _ _ => return i)
adamc@1093 54 fl
adamc@910 55
adamc@1172 56 fun mapR0 [K] [m] (_ : monad m) [tr :: K -> Type]
adamc@1172 57 (f : nm :: Name -> t :: K -> m (tr t)) [r ::: {K}] (fl : folder r) =
adamc@1172 58 @Top.fold [fn r => m ($(map tr r))]
adamc@1172 59 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] (acc : m ($(map tr rest))) =>
adamc@1172 60 v <- f [nm] [t];
adamc@1172 61 vs <- acc;
adamc@1172 62 return (vs ++ {nm = v}))
adamc@1172 63 (return {})
adamc@1172 64 fl
adamc@1172 65
adamc@905 66 fun mapR [K] [m] (_ : monad m) [tf :: K -> Type] [tr :: K -> Type]
adamc@905 67 (f : nm :: Name -> t :: K -> tf t -> m (tr t)) =
adamc@905 68 @@foldR [m] _ [tf] [fn r => $(map tr r)]
adamc@905 69 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] (v : tf t)
adamc@905 70 (acc : $(map tr rest)) =>
adamc@905 71 v' <- f [nm] [t] v;
adamc@905 72 return (acc ++ {nm = v'}))
adamc@905 73 {}
adamc@937 74
adamc@937 75 fun mapR2 [K] [m] (_ : monad m) [tf1 :: K -> Type] [tf2 :: K -> Type] [tr :: K -> Type]
adamc@937 76 (f : nm :: Name -> t :: K -> tf1 t -> tf2 t -> m (tr t)) =
adamc@937 77 @@foldR2 [m] _ [tf1] [tf2] [fn r => $(map tr r)]
adamc@937 78 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] (v1 : tf1 t) (v2 : tf2 t)
adamc@937 79 (acc : $(map tr rest)) =>
adamc@937 80 v' <- f [nm] [t] v1 v2;
adamc@937 81 return (acc ++ {nm = v'}))
adamc@937 82 {}
adamc@1175 83
adam@2185 84 fun mapR3 [K] [m] (_ : monad m) [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type] [tr :: K -> Type]
adam@2185 85 (f : nm :: Name -> t :: K -> tf1 t -> tf2 t -> tf3 t -> m (tr t)) =
adam@2185 86 @@foldR3 [m] _ [tf1] [tf2] [tf3] [fn r => $(map tr r)]
adam@2185 87 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] (v1 : tf1 t) (v2 : tf2 t) (v3 : tf3 t)
adam@2185 88 (acc : $(map tr rest)) =>
adam@2185 89 v' <- f [nm] [t] v1 v2 v3;
adam@2185 90 return (acc ++ {nm = v'}))
adam@2185 91 {}
adam@2185 92
adamc@1175 93 fun foldMapR [K] [m] (_ : monad m) [tf :: K -> Type] [tf' :: K -> Type] [tr :: {K} -> Type]
adamc@1175 94 (f : nm :: Name -> t :: K -> rest :: {K}
adamc@1175 95 -> [[nm] ~ rest] =>
adamc@1175 96 tf t -> tr rest -> m (tf' t * tr ([nm = t] ++ rest)))
adamc@1175 97 (i : tr []) [r ::: {K}] (fl : folder r) =
adamc@1175 98 @Top.fold [fn r :: {K} => $(map tf r) -> m ($(map tf' r) * tr r)]
adamc@1175 99 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest]
adamc@1175 100 (acc : _ -> m ($(map tf' rest) * tr rest)) r =>
adamc@1175 101 p <- acc (r -- nm);
adam@1472 102 p' <- f [nm] [t] [rest] r.nm p.2;
adamc@1175 103 return ({nm = p'.1} ++ p.1, p'.2))
adamc@1175 104 (fn _ => return ({}, i))
adamc@1175 105 fl
adamc@1257 106
adam@1312 107 fun appR [K] [m] (_ : monad m) [tf :: K -> Type]
adam@1312 108 (f : nm :: Name -> t :: K -> tf t -> m unit)
adam@1312 109 [r ::: {K}] (fl : folder r) =
adam@1312 110 @Top.fold [fn r :: {K} => $(map tf r) -> m unit]
adam@1312 111 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] acc r =>
adam@1312 112 acc (r -- nm);
adam@1312 113 f [nm] [t] r.nm)
adam@1312 114 (fn _ => return ())
adam@1312 115 fl
adam@1312 116
adamc@1257 117 fun appR2 [K] [m] (_ : monad m) [tf1 :: K -> Type] [tf2 :: K -> Type]
adam@1310 118 (f : nm :: Name -> t :: K -> tf1 t -> tf2 t -> m unit)
adamc@1257 119 [r ::: {K}] (fl : folder r) =
adamc@1257 120 @Top.fold [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> m unit]
adamc@1257 121 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] acc r1 r2 =>
adamc@1257 122 acc (r1 -- nm) (r2 -- nm);
adam@1310 123 f [nm] [t] r1.nm r2.nm)
adamc@1257 124 (fn _ _ => return ())
adamc@1257 125 fl
adam@1313 126
adam@1313 127 fun appR3 [K] [m] (_ : monad m) [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type]
adam@1313 128 (f : nm :: Name -> t :: K -> tf1 t -> tf2 t -> tf3 t -> m unit)
adam@1313 129 [r ::: {K}] (fl : folder r) =
adam@1313 130 @Top.fold [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> m unit]
adam@1313 131 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] acc r1 r2 r3 =>
adam@1313 132 acc (r1 -- nm) (r2 -- nm) (r3 -- nm);
adam@1313 133 f [nm] [t] r1.nm r2.nm r3.nm)
adam@1313 134 (fn _ _ _ => return ())
adam@1313 135 fl
adam@1768 136
adam@1768 137 fun liftM2 [m ::: Type -> Type] (_ : monad m) [a] [b] [c] (f : a -> b -> c) (mx : m a) (my : m b) : m c =
adam@1768 138 x <- mx;
adam@1768 139 y <- my;
adam@1768 140 return (f x y)