Mercurial > urweb

annotate lib/ur/monad.ur @ 1651:dfc854e478bb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Error messages about applying 'dynClass' to tags that don't like it
author Adam Chlipala <adam@chlipala.net>
date Sat, 31 Dec 2011 13:31:00 -0500
parents 18d18a70821e
children a613cae954ca
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
adamc@905 15 fun foldR [K] [m] (_ : monad m) [tf :: K -> Type] [tr :: {K} -> Type]
adamc@905 16 (f : nm :: Name -> t :: K -> rest :: {K}
adamc@905 17 -> [[nm] ~ rest] =>
adamc@905 18 tf t -> tr rest -> m (tr ([nm = t] ++ rest)))
adamc@1093 19 (i : tr []) [r ::: {K}] (fl : folder r) =
adamc@1093 20 @Top.fold [fn r :: {K} => $(map tf r) -> m (tr r)]
adamc@1093 21 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest]
adamc@1093 22 (acc : _ -> m (tr rest)) r =>
adamc@1093 23 acc' <- acc (r -- nm);
adam@1472 24 f [nm] [t] [rest] r.nm acc')
adamc@1093 25 (fn _ => return i)
adamc@1093 26 fl
adamc@905 27
adamc@905 28 fun foldR2 [K] [m] (_ : monad m) [tf1 :: K -> Type] [tf2 :: K -> Type] [tr :: {K} -> Type]
adamc@905 29 (f : nm :: Name -> t :: K -> rest :: {K}
adamc@905 30 -> [[nm] ~ rest] =>
adamc@905 31 tf1 t -> tf2 t -> tr rest -> m (tr ([nm = t] ++ rest)))
adamc@1093 32 (i : tr []) [r ::: {K}] (fl : folder r) =
adamc@1093 33 @Top.fold [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> m (tr r)]
adamc@1093 34 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest]
adamc@1093 35 (acc : _ -> _ -> m (tr rest)) r1 r2 =>
adamc@1093 36 acc' <- acc (r1 -- nm) (r2 -- nm);
adam@1472 37 f [nm] [t] [rest] r1.nm r2.nm acc')
adamc@1093 38 (fn _ _ => return i)
adamc@1093 39 fl
adamc@905 40
adamc@910 41 fun foldR3 [K] [m] (_ : monad m) [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type] [tr :: {K} -> Type]
adamc@910 42 (f : nm :: Name -> t :: K -> rest :: {K}
adamc@910 43 -> [[nm] ~ rest] =>
adamc@910 44 tf1 t -> tf2 t -> tf3 t -> tr rest -> m (tr ([nm = t] ++ rest)))
adamc@1093 45 (i : tr []) [r ::: {K}] (fl : folder r) =
adamc@1093 46 @Top.fold [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> m (tr r)]
adamc@1093 47 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest]
adamc@1093 48 (acc : _ -> _ -> _ -> m (tr rest)) r1 r2 r3 =>
adamc@1093 49 acc' <- acc (r1 -- nm) (r2 -- nm) (r3 -- nm);
adam@1472 50 f [nm] [t] [rest] r1.nm r2.nm r3.nm acc')
adamc@1093 51 (fn _ _ _ => return i)
adamc@1093 52 fl
adamc@910 53
adamc@1172 54 fun mapR0 [K] [m] (_ : monad m) [tr :: K -> Type]
adamc@1172 55 (f : nm :: Name -> t :: K -> m (tr t)) [r ::: {K}] (fl : folder r) =
adamc@1172 56 @Top.fold [fn r => m ($(map tr r))]
adamc@1172 57 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] (acc : m ($(map tr rest))) =>
adamc@1172 58 v <- f [nm] [t];
adamc@1172 59 vs <- acc;
adamc@1172 60 return (vs ++ {nm = v}))
adamc@1172 61 (return {})
adamc@1172 62 fl
adamc@1172 63
adamc@905 64 fun mapR [K] [m] (_ : monad m) [tf :: K -> Type] [tr :: K -> Type]
adamc@905 65 (f : nm :: Name -> t :: K -> tf t -> m (tr t)) =
adamc@905 66 @@foldR [m] _ [tf] [fn r => $(map tr r)]
adamc@905 67 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] (v : tf t)
adamc@905 68 (acc : $(map tr rest)) =>
adamc@905 69 v' <- f [nm] [t] v;
adamc@905 70 return (acc ++ {nm = v'}))
adamc@905 71 {}
adamc@937 72
adamc@937 73 fun mapR2 [K] [m] (_ : monad m) [tf1 :: K -> Type] [tf2 :: K -> Type] [tr :: K -> Type]
adamc@937 74 (f : nm :: Name -> t :: K -> tf1 t -> tf2 t -> m (tr t)) =
adamc@937 75 @@foldR2 [m] _ [tf1] [tf2] [fn r => $(map tr r)]
adamc@937 76 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] (v1 : tf1 t) (v2 : tf2 t)
adamc@937 77 (acc : $(map tr rest)) =>
adamc@937 78 v' <- f [nm] [t] v1 v2;
adamc@937 79 return (acc ++ {nm = v'}))
adamc@937 80 {}
adamc@1175 81
adamc@1175 82 fun foldMapR [K] [m] (_ : monad m) [tf :: K -> Type] [tf' :: K -> Type] [tr :: {K} -> Type]
adamc@1175 83 (f : nm :: Name -> t :: K -> rest :: {K}
adamc@1175 84 -> [[nm] ~ rest] =>
adamc@1175 85 tf t -> tr rest -> m (tf' t * tr ([nm = t] ++ rest)))
adamc@1175 86 (i : tr []) [r ::: {K}] (fl : folder r) =
adamc@1175 87 @Top.fold [fn r :: {K} => $(map tf r) -> m ($(map tf' r) * tr r)]
adamc@1175 88 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest]
adamc@1175 89 (acc : _ -> m ($(map tf' rest) * tr rest)) r =>
adamc@1175 90 p <- acc (r -- nm);
adam@1472 91 p' <- f [nm] [t] [rest] r.nm p.2;
adamc@1175 92 return ({nm = p'.1} ++ p.1, p'.2))
adamc@1175 93 (fn _ => return ({}, i))
adamc@1175 94 fl
adamc@1257 95
adam@1312 96 fun appR [K] [m] (_ : monad m) [tf :: K -> Type]
adam@1312 97 (f : nm :: Name -> t :: K -> tf t -> m unit)
adam@1312 98 [r ::: {K}] (fl : folder r) =
adam@1312 99 @Top.fold [fn r :: {K} => $(map tf r) -> m unit]
adam@1312 100 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] acc r =>
adam@1312 101 acc (r -- nm);
adam@1312 102 f [nm] [t] r.nm)
adam@1312 103 (fn _ => return ())
adam@1312 104 fl
adam@1312 105
adamc@1257 106 fun appR2 [K] [m] (_ : monad m) [tf1 :: K -> Type] [tf2 :: K -> Type]
adam@1310 107 (f : nm :: Name -> t :: K -> tf1 t -> tf2 t -> m unit)
adamc@1257 108 [r ::: {K}] (fl : folder r) =
adamc@1257 109 @Top.fold [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> m unit]
adamc@1257 110 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] acc r1 r2 =>
adamc@1257 111 acc (r1 -- nm) (r2 -- nm);
adam@1310 112 f [nm] [t] r1.nm r2.nm)
adamc@1257 113 (fn _ _ => return ())
adamc@1257 114 fl
adam@1313 115
adam@1313 116 fun appR3 [K] [m] (_ : monad m) [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type]
adam@1313 117 (f : nm :: Name -> t :: K -> tf1 t -> tf2 t -> tf3 t -> m unit)
adam@1313 118 [r ::: {K}] (fl : folder r) =
adam@1313 119 @Top.fold [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> m unit]
adam@1313 120 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] acc r1 r2 r3 =>
adam@1313 121 acc (r1 -- nm) (r2 -- nm) (r3 -- nm);
adam@1313 122 f [nm] [t] r1.nm r2.nm r3.nm)
adam@1313 123 (fn _ _ _ => return ())
adam@1313 124 fl