Mercurial > urweb
comparison lib/ur/monad.ur @ 1472:18d18a70821e
Implicit argument insertion for local variables
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Tue, 14 Jun 2011 08:54:45 -0400 |
parents | 0bf73c3e4563 |
children | a613cae954ca |
comparison
equal
deleted
inserted
replaced
1471:67ebd30a2283 | 1472:18d18a70821e |
---|---|
19 (i : tr []) [r ::: {K}] (fl : folder r) = | 19 (i : tr []) [r ::: {K}] (fl : folder r) = |
20 @Top.fold [fn r :: {K} => $(map tf r) -> m (tr r)] | 20 @Top.fold [fn r :: {K} => $(map tf r) -> m (tr r)] |
21 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] | 21 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] |
22 (acc : _ -> m (tr rest)) r => | 22 (acc : _ -> m (tr rest)) r => |
23 acc' <- acc (r -- nm); | 23 acc' <- acc (r -- nm); |
24 f [nm] [t] [rest] ! r.nm acc') | 24 f [nm] [t] [rest] r.nm acc') |
25 (fn _ => return i) | 25 (fn _ => return i) |
26 fl | 26 fl |
27 | 27 |
28 fun foldR2 [K] [m] (_ : monad m) [tf1 :: K -> Type] [tf2 :: K -> Type] [tr :: {K} -> Type] | 28 fun foldR2 [K] [m] (_ : monad m) [tf1 :: K -> Type] [tf2 :: K -> Type] [tr :: {K} -> Type] |
29 (f : nm :: Name -> t :: K -> rest :: {K} | 29 (f : nm :: Name -> t :: K -> rest :: {K} |
32 (i : tr []) [r ::: {K}] (fl : folder r) = | 32 (i : tr []) [r ::: {K}] (fl : folder r) = |
33 @Top.fold [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> m (tr r)] | 33 @Top.fold [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> m (tr r)] |
34 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] | 34 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] |
35 (acc : _ -> _ -> m (tr rest)) r1 r2 => | 35 (acc : _ -> _ -> m (tr rest)) r1 r2 => |
36 acc' <- acc (r1 -- nm) (r2 -- nm); | 36 acc' <- acc (r1 -- nm) (r2 -- nm); |
37 f [nm] [t] [rest] ! r1.nm r2.nm acc') | 37 f [nm] [t] [rest] r1.nm r2.nm acc') |
38 (fn _ _ => return i) | 38 (fn _ _ => return i) |
39 fl | 39 fl |
40 | 40 |
41 fun foldR3 [K] [m] (_ : monad m) [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type] [tr :: {K} -> Type] | 41 fun foldR3 [K] [m] (_ : monad m) [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type] [tr :: {K} -> Type] |
42 (f : nm :: Name -> t :: K -> rest :: {K} | 42 (f : nm :: Name -> t :: K -> rest :: {K} |
45 (i : tr []) [r ::: {K}] (fl : folder r) = | 45 (i : tr []) [r ::: {K}] (fl : folder r) = |
46 @Top.fold [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> m (tr r)] | 46 @Top.fold [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> m (tr r)] |
47 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] | 47 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] |
48 (acc : _ -> _ -> _ -> m (tr rest)) r1 r2 r3 => | 48 (acc : _ -> _ -> _ -> m (tr rest)) r1 r2 r3 => |
49 acc' <- acc (r1 -- nm) (r2 -- nm) (r3 -- nm); | 49 acc' <- acc (r1 -- nm) (r2 -- nm) (r3 -- nm); |
50 f [nm] [t] [rest] ! r1.nm r2.nm r3.nm acc') | 50 f [nm] [t] [rest] r1.nm r2.nm r3.nm acc') |
51 (fn _ _ _ => return i) | 51 (fn _ _ _ => return i) |
52 fl | 52 fl |
53 | 53 |
54 fun mapR0 [K] [m] (_ : monad m) [tr :: K -> Type] | 54 fun mapR0 [K] [m] (_ : monad m) [tr :: K -> Type] |
55 (f : nm :: Name -> t :: K -> m (tr t)) [r ::: {K}] (fl : folder r) = | 55 (f : nm :: Name -> t :: K -> m (tr t)) [r ::: {K}] (fl : folder r) = |
86 (i : tr []) [r ::: {K}] (fl : folder r) = | 86 (i : tr []) [r ::: {K}] (fl : folder r) = |
87 @Top.fold [fn r :: {K} => $(map tf r) -> m ($(map tf' r) * tr 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] | 88 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] |
89 (acc : _ -> m ($(map tf' rest) * tr rest)) r => | 89 (acc : _ -> m ($(map tf' rest) * tr rest)) r => |
90 p <- acc (r -- nm); | 90 p <- acc (r -- nm); |
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] | 96 fun appR [K] [m] (_ : monad m) [tf :: K -> Type] |