Mercurial > meta
diff mem.ur @ 14:744bf911dcc6
Update to expect implicit argument insertion for local variables
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Tue, 14 Jun 2011 08:55:15 -0400 |
| parents | 943410267fad |
| children |
line wrap: on
line diff
--- a/mem.ur Mon Mar 21 10:16:12 2011 -0400 +++ b/mem.ur Tue Jun 14 08:55:15 2011 -0400 @@ -7,18 +7,18 @@ fun mem [K] [nm :: Name] [t :: K] [r :: {K}] [[nm] ~ r] = fn [tp :: Type] (f : r' :: {K} -> [[nm] ~ r'] => mem' nm t ([nm = t] ++ r) r' -> tp) => - f [r] ! (fn [[nm] ~ r] => {Expose = fn [f :: {K} -> Type] x => x, - Hide = fn [f :: {K} -> Type] x => x}) + f [r] (fn [[nm] ~ r] => {Expose = fn [f :: {K} -> Type] x => x, + Hide = fn [f :: {K} -> Type] x => x}) fun mp [K] [K2] [f :: K -> K2] [nm ::: Name] [t ::: K] [r ::: {K}] (m : mem nm t r) = m [mem nm (f t) (map f r)] (fn [r' :: {K}] [[nm] ~ r'] (m' : mem' nm t r r') => fn [tp :: Type] (f : r' :: {K2} -> [[nm] ~ r'] => mem' nm (f t) (map f r) r' -> tp) => - f [map f r'] ! (fn [[nm] ~ map f r'] => - {Expose = fn [f' :: {K2} -> Type] x => - m'.Expose [fn r => f' (map f r)] x, - Hide = fn [f' :: {K2} -> Type] x => - m'.Hide [fn r => f' (map f r)] x})) + f [map f r'] (fn [[nm] ~ map f r'] => + {Expose = fn [f' :: {K2} -> Type] x => + m'.Expose [fn r => f' (map f r)] x, + Hide = fn [f' :: {K2} -> Type] x => + m'.Hide [fn r => f' (map f r)] x})) fun proj [nm ::: Name] [t ::: Type] [r ::: {Type}] (m : mem nm t r) (r : $r) = m [t] (fn [r' :: {Type}] [[nm] ~ r'] (m' : mem' nm t r r') => @@ -34,5 +34,5 @@ (i : tf []) (fl : folder r) = @@Incl.fold [tf] [r] (fn [nm :: Name] [v :: K] [r' :: {K}] [[nm] ~ r'] (i : Incl.incl ([nm = v] ++ r') r) acc => - f [nm] [v] [r'] ! (Incl.inv1 [nm] [v] [r'] [r] [mem] i mem) acc) + f [nm] [v] [r'] (Incl.inv1 [nm] [v] [r'] [r] [mem] i mem) acc) i fl