Mercurial > meta
comparison incl.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 |
---|---|
1 con incl' = K ==> fn (r1 :: {K}) (r2 :: {K}) (r' :: {K}) => | 1 con incl' = K ==> fn (r1 :: {K}) (r2 :: {K}) (r' :: {K}) => |
2 [r1 ~ r'] => {Expose : f :: ({K} -> Type) -> f r2 -> f (r1 ++ r'), | 2 [r1 ~ r'] => {Expose : f :: ({K} -> Type) -> f r2 -> f (r1 ++ r'), |
3 Hide : f :: ({K} -> Type) -> f (r1 ++ r') -> f r2} | 3 Hide : f :: ({K} -> Type) -> f (r1 ++ r') -> f r2} |
4 | 4 |
5 con incl = K ==> fn (r1 :: {K}) (r2 :: {K}) => | 5 con incl = K ==> fn (r1 :: {K}) (r2 :: {K}) => |
6 tp :: Type -> (r' :: {K} -> [r1 ~ r'] => incl' r1 r2 r' -> tp) -> tp | 6 tp :: Type -> (r' :: {K} -> [r1 ~ r'] => incl' r1 r2 r' -> tp) -> tp |
7 | 7 |
8 fun incl [K] [r1 :: {K}] [r2 :: {K}] [r1 ~ r2] = | 8 fun incl [K] [r1 :: {K}] [r2 :: {K}] [r1 ~ r2] = |
9 fn [tp :: Type] (f : r' :: {K} -> [r1 ~ r'] => incl' r1 (r1 ++ r2) r' -> tp) => | 9 fn [tp :: Type] (f : r' :: {K} -> [r1 ~ r'] => incl' r1 (r1 ++ r2) r' -> tp) => |
10 f [r2] ! (fn [r1 ~ r2] => {Expose = fn [f :: ({K} -> Type)] x => x, | 10 f [r2] (fn [r1 ~ r2] => {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 proj [r1 ::: {Type}] [r2 ::: {Type}] (i : incl r1 r2) (r : $r2) = | 13 fun proj [r1 ::: {Type}] [r2 ::: {Type}] (i : incl r1 r2) (r : $r2) = |
14 i [$r1] (fn [r' :: {Type}] [r1 ~ r'] (i' : incl' r1 r2 r') => | 14 i [$r1] (fn [r' :: {Type}] [r1 ~ r'] (i' : incl' r1 r2 r') => |
15 i'.Expose [fn r => $r] r --- r') | 15 i'.Expose [fn r => $r] r --- r') |
16 | 16 |
17 fun inv1 [K] [nm :: Name] [t :: K] [r :: {K}] [r' :: {K}] [[nm] ~ r] | 17 fun inv1 [K] [nm :: Name] [t :: K] [r :: {K}] [r' :: {K}] [[nm] ~ r] |
18 [f :: Name -> K -> {K} -> Type] | 18 [f :: Name -> K -> {K} -> Type] |
19 (i : incl ([nm = t] ++ r) r') | 19 (i : incl ([nm = t] ++ r) r') |
20 (f : nm :: Name -> t :: K -> r :: {K} -> [[nm] ~ r] => f nm t ([nm = t] ++ r)) = | 20 (f : nm :: Name -> t :: K -> r :: {K} -> [[nm] ~ r] => f nm t ([nm = t] ++ r)) = |
21 i [f nm t r'] (fn [r'' :: {K}] [[nm = t] ++ r ~ r''] (i' : incl' ([nm = t] ++ r) r' r'') => | 21 i [f nm t r'] (fn [r'' :: {K}] [[nm = t] ++ r ~ r''] (i' : incl' ([nm = t] ++ r) r' r'') => |
22 i'.Hide [f nm t] (f [nm] [t] [r ++ r''] !)) | 22 i'.Hide [f nm t] (f [nm] [t] [r ++ r''])) |
23 | 23 |
24 fun inv2 [K] [nm :: Name] [t :: K] [r :: {K}] [r' :: {K}] [[nm] ~ r] | 24 fun inv2 [K] [nm :: Name] [t :: K] [r :: {K}] [r' :: {K}] [[nm] ~ r] |
25 (i : incl ([nm = t] ++ r) r') = | 25 (i : incl ([nm = t] ++ r) r') = |
26 i [incl r r'] (fn [r'' :: {K}] [[nm = t] ++ r ~ r''] (i' : incl' ([nm = t] ++ r) r' r'') => | 26 i [incl r r'] (fn [r'' :: {K}] [[nm = t] ++ r ~ r''] (i' : incl' ([nm = t] ++ r) r' r'') => |
27 fn [tp :: Type] (f : r''' :: {K} -> [r ~ r'''] => incl' r r' r''' -> tp) => | 27 fn [tp :: Type] (f : r''' :: {K} -> [r ~ r'''] => incl' r r' r''' -> tp) => |
28 f [[nm = t] ++ r''] ! (fn [r ~ [nm = t] ++ r''] => | 28 f [[nm = t] ++ r''] (fn [r ~ [nm = t] ++ r''] => |
29 {Expose = fn [f :: ({K} -> Type)] (x : f r') => i'.Expose [f] x, | 29 {Expose = fn [f :: ({K} -> Type)] (x : f r') => i'.Expose [f] x, |
30 Hide = fn [f :: ({K} -> Type)] x => i'.Hide [f] x})) | 30 Hide = fn [f :: ({K} -> Type)] x => i'.Hide [f] x})) |
31 | 31 |
32 fun fold [K] [tf :: {K} -> Type] [r ::: {K}] | 32 fun fold [K] [tf :: {K} -> Type] [r ::: {K}] |
33 (f : nm :: Name -> v :: K -> r' :: {K} | 33 (f : nm :: Name -> v :: K -> r' :: {K} |
34 -> [[nm] ~ r'] => incl ([nm = v] ++ r') r -> tf r' -> tf ([nm = v] ++ r')) | 34 -> [[nm] ~ r'] => incl ([nm = v] ++ r') r -> tf r' -> tf ([nm = v] ++ r')) |
35 (i : tf []) (fl : folder r) = | 35 (i : tf []) (fl : folder r) = |
36 @Top.fold [fn r' => incl r' r -> tf r'] | 36 @Top.fold [fn r' => incl r' r -> tf r'] |
37 (fn [nm :: Name] [v :: K] [r' :: {K}] [[nm] ~ r'] acc i => | 37 (fn [nm :: Name] [v :: K] [r' :: {K}] [[nm] ~ r'] acc i => |
38 f [nm] [v] [r'] ! i (acc (inv2 [nm] [v] [r'] [r] i))) | 38 f [nm] [v] [r'] i (acc (inv2 [nm] [v] [r'] [r] i))) |
39 (fn _ => i) | 39 (fn _ => i) |
40 fl (incl [r] [[]]) | 40 fl (incl [r] [[]]) |