Mercurial > meta
comparison 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 |
comparison
equal
deleted
inserted
replaced
13:d05943db55e8 | 14:744bf911dcc6 |
---|---|
5 con mem = K ==> fn (nm :: Name) (t :: K) (r :: {K}) => | 5 con mem = K ==> fn (nm :: Name) (t :: K) (r :: {K}) => |
6 tp :: Type -> (r' :: {K} -> [[nm] ~ r'] => mem' nm t r r' -> tp) -> tp | 6 tp :: Type -> (r' :: {K} -> [[nm] ~ r'] => mem' nm t r r' -> tp) -> tp |
7 | 7 |
8 fun mem [K] [nm :: Name] [t :: K] [r :: {K}] [[nm] ~ r] = | 8 fun mem [K] [nm :: Name] [t :: K] [r :: {K}] [[nm] ~ r] = |
9 fn [tp :: Type] (f : r' :: {K} -> [[nm] ~ r'] => mem' nm t ([nm = t] ++ r) r' -> tp) => | 9 fn [tp :: Type] (f : r' :: {K} -> [[nm] ~ r'] => mem' nm t ([nm = t] ++ r) r' -> tp) => |
10 f [r] ! (fn [[nm] ~ r] => {Expose = fn [f :: {K} -> Type] x => x, | 10 f [r] (fn [[nm] ~ r] => {Expose = fn [f :: {K} -> Type] x => x, |
11 Hide = fn [f :: {K} -> Type] x => x}) | 11 Hide = fn [f :: {K} -> Type] x => x}) |
12 | 12 |
13 fun mp [K] [K2] [f :: K -> K2] [nm ::: Name] [t ::: K] [r ::: {K}] (m : mem nm t r) = | 13 fun mp [K] [K2] [f :: K -> K2] [nm ::: Name] [t ::: K] [r ::: {K}] (m : mem nm t r) = |
14 m [mem nm (f t) (map f r)] (fn [r' :: {K}] [[nm] ~ r'] (m' : mem' nm t r r') => | 14 m [mem nm (f t) (map f r)] (fn [r' :: {K}] [[nm] ~ r'] (m' : mem' nm t r r') => |
15 fn [tp :: Type] (f : r' :: {K2} -> [[nm] ~ r'] => | 15 fn [tp :: Type] (f : r' :: {K2} -> [[nm] ~ r'] => |
16 mem' nm (f t) (map f r) r' -> tp) => | 16 mem' nm (f t) (map f r) r' -> tp) => |
17 f [map f r'] ! (fn [[nm] ~ map f r'] => | 17 f [map f r'] (fn [[nm] ~ map f r'] => |
18 {Expose = fn [f' :: {K2} -> Type] x => | 18 {Expose = fn [f' :: {K2} -> Type] x => |
19 m'.Expose [fn r => f' (map f r)] x, | 19 m'.Expose [fn r => f' (map f r)] x, |
20 Hide = fn [f' :: {K2} -> Type] x => | 20 Hide = fn [f' :: {K2} -> Type] x => |
21 m'.Hide [fn r => f' (map f r)] x})) | 21 m'.Hide [fn r => f' (map f r)] x})) |
22 | 22 |
23 fun proj [nm ::: Name] [t ::: Type] [r ::: {Type}] (m : mem nm t r) (r : $r) = | 23 fun proj [nm ::: Name] [t ::: Type] [r ::: {Type}] (m : mem nm t r) (r : $r) = |
24 m [t] (fn [r' :: {Type}] [[nm] ~ r'] (m' : mem' nm t r r') => | 24 m [t] (fn [r' :: {Type}] [[nm] ~ r'] (m' : mem' nm t r r') => |
25 (m'.Expose [fn r => $r] r).nm) | 25 (m'.Expose [fn r => $r] r).nm) |
26 | 26 |
32 (f : nm :: Name -> v :: K -> r' :: {K} -> [[nm] ~ r'] | 32 (f : nm :: Name -> v :: K -> r' :: {K} -> [[nm] ~ r'] |
33 => mem nm v r -> tf r' -> tf ([nm = v] ++ r')) | 33 => mem nm v r -> tf r' -> tf ([nm = v] ++ r')) |
34 (i : tf []) (fl : folder r) = | 34 (i : tf []) (fl : folder r) = |
35 @@Incl.fold [tf] [r] | 35 @@Incl.fold [tf] [r] |
36 (fn [nm :: Name] [v :: K] [r' :: {K}] [[nm] ~ r'] (i : Incl.incl ([nm = v] ++ r') r) acc => | 36 (fn [nm :: Name] [v :: K] [r' :: {K}] [[nm] ~ r'] (i : Incl.incl ([nm = v] ++ r') r) acc => |
37 f [nm] [v] [r'] ! (Incl.inv1 [nm] [v] [r'] [r] [mem] i mem) acc) | 37 f [nm] [v] [r'] (Incl.inv1 [nm] [v] [r'] [r] [mem] i mem) acc) |
38 i fl | 38 i fl |