Mercurial > meta
comparison eq.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 | 799f43bce62b |
children |
comparison
equal
deleted
inserted
replaced
13:d05943db55e8 | 14:744bf911dcc6 |
---|---|
16 (i : tf []) (fl : folder r) : tf r = | 16 (i : tf []) (fl : folder r) : tf r = |
17 @@Top.fold [fn post => pre :: {K} -> [pre ~ post] => eq r (pre ++ post) -> tf post] | 17 @@Top.fold [fn post => pre :: {K} -> [pre ~ post] => eq r (pre ++ post) -> tf post] |
18 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] | 18 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] |
19 (acc : pre :: {K} -> [pre ~ rest] => eq r (pre ++ rest) -> tf rest) | 19 (acc : pre :: {K} -> [pre ~ rest] => eq r (pre ++ rest) -> tf rest) |
20 [pre :: {K}] [pre ~ [nm = t] ++ rest] pf => | 20 [pre :: {K}] [pre ~ [nm = t] ++ rest] pf => |
21 f [pre] [nm] [t] [rest] ! ! pf (acc [[nm = t] ++ pre] ! pf)) | 21 f [pre] [nm] [t] [rest] pf (acc [[nm = t] ++ pre] pf)) |
22 (fn [pre :: {K}] [pre ~ []] _ => i) [r] fl [[]] ! refl | 22 (fn [pre :: {K}] [pre ~ []] _ => i) [r] fl [[]] ! refl |
23 | 23 |
24 fun foldUR [tr :: Type] [tf :: {Unit} -> Type] [r ::: {Unit}] | 24 fun foldUR [tr :: Type] [tf :: {Unit} -> Type] [r ::: {Unit}] |
25 (f : pre :: {Unit} -> nm :: Name -> post :: {Unit} -> [pre ~ post] => [[nm] ~ pre ++ post] => | 25 (f : pre :: {Unit} -> nm :: Name -> post :: {Unit} -> [pre ~ post] => [[nm] ~ pre ++ post] => |
26 eq r (pre ++ [nm] ++ post) -> tr -> tf post -> tf ([nm] ++ post)) | 26 eq r (pre ++ [nm] ++ post) -> tr -> tf post -> tf ([nm] ++ post)) |
27 (i : tf []) (fl : folder r) (r : $(mapU tr r)) : tf r = | 27 (i : tf []) (fl : folder r) (r : $(mapU tr r)) : tf r = |
28 @@fold [fn r' => $(mapU tr r') -> tf r'] [r] | 28 @@fold [fn r' => $(mapU tr r') -> tf r'] [r] |
29 (fn [pre :: {Unit}] [nm :: Name] [u :: Unit] [post :: {Unit}] [pre ~ post] [[nm] ~ pre ++ post] pf acc r => | 29 (fn [pre :: {Unit}] [nm :: Name] [u :: Unit] [post :: {Unit}] [pre ~ post] [[nm] ~ pre ++ post] pf acc r => |
30 f [pre] [nm] [post] ! ! pf r.nm (acc (r -- nm))) | 30 f [pre] [nm] [post] pf r.nm (acc (r -- nm))) |
31 (fn _ => i) fl r | 31 (fn _ => i) fl r |
32 | 32 |
33 fun foldR [K] [tr :: K -> Type] [tf :: {K} -> Type] [r ::: {K}] | 33 fun foldR [K] [tr :: K -> Type] [tf :: {K} -> Type] [r ::: {K}] |
34 (f : pre :: {K} -> nm :: Name -> t :: K -> post :: {K} -> [pre ~ post] => [[nm] ~ pre ++ post] => | 34 (f : pre :: {K} -> nm :: Name -> t :: K -> post :: {K} -> [pre ~ post] => [[nm] ~ pre ++ post] => |
35 eq r (pre ++ [nm = t] ++ post) -> tr t -> tf post -> tf ([nm = t] ++ post)) | 35 eq r (pre ++ [nm = t] ++ post) -> tr t -> tf post -> tf ([nm = t] ++ post)) |
36 (i : tf []) (fl : folder r) (r : $(map tr r)) : tf r = | 36 (i : tf []) (fl : folder r) (r : $(map tr r)) : tf r = |
37 @@fold [fn r' => $(map tr r') -> tf r'] [r] | 37 @@fold [fn r' => $(map tr r') -> tf r'] [r] |
38 (fn [pre :: {K}] [nm :: Name] [t :: K] [post :: {K}] [pre ~ post] [[nm] ~ pre ++ post] pf acc r => | 38 (fn [pre :: {K}] [nm :: Name] [t :: K] [post :: {K}] [pre ~ post] [[nm] ~ pre ++ post] pf acc r => |
39 f [pre] [nm] [t] [post] ! ! pf r.nm (acc (r -- nm))) | 39 f [pre] [nm] [t] [post] pf r.nm (acc (r -- nm))) |
40 (fn _ => i) fl r | 40 (fn _ => i) fl r |
41 | 41 |
42 fun foldR2 [K] [tr1 :: K -> Type] [tr2 :: K -> Type] [tf :: {K} -> Type] [r ::: {K}] | 42 fun foldR2 [K] [tr1 :: K -> Type] [tr2 :: K -> Type] [tf :: {K} -> Type] [r ::: {K}] |
43 (f : pre :: {K} -> nm :: Name -> t :: K -> post :: {K} -> [pre ~ post] => [[nm] ~ pre ++ post] => | 43 (f : pre :: {K} -> nm :: Name -> t :: K -> post :: {K} -> [pre ~ post] => [[nm] ~ pre ++ post] => |
44 eq r (pre ++ [nm = t] ++ post) -> tr1 t -> tr2 t -> tf post -> tf ([nm = t] ++ post)) | 44 eq r (pre ++ [nm = t] ++ post) -> tr1 t -> tr2 t -> tf post -> tf ([nm = t] ++ post)) |
45 (i : tf []) (fl : folder r) (r1 : $(map tr1 r)) (r2 : $(map tr2 r)) : tf r = | 45 (i : tf []) (fl : folder r) (r1 : $(map tr1 r)) (r2 : $(map tr2 r)) : tf r = |
46 @@fold [fn r' => $(map tr1 r') -> $(map tr2 r') -> tf r'] [r] | 46 @@fold [fn r' => $(map tr1 r') -> $(map tr2 r') -> tf r'] [r] |
47 (fn [pre :: {K}] [nm :: Name] [t :: K] [post :: {K}] [pre ~ post] [[nm] ~ pre ++ post] pf acc r1 r2 => | 47 (fn [pre :: {K}] [nm :: Name] [t :: K] [post :: {K}] [pre ~ post] [[nm] ~ pre ++ post] pf acc r1 r2 => |
48 f [pre] [nm] [t] [post] ! ! pf r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm))) | 48 f [pre] [nm] [t] [post] pf r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm))) |
49 (fn _ _ => i) fl r1 r2 | 49 (fn _ _ => i) fl r1 r2 |
50 | 50 |
51 fun foldR3 [K] [tr1 :: K -> Type] [tr2 :: K -> Type] [tr3 :: K -> Type] [tf :: {K} -> Type] [r ::: {K}] | 51 fun foldR3 [K] [tr1 :: K -> Type] [tr2 :: K -> Type] [tr3 :: K -> Type] [tf :: {K} -> Type] [r ::: {K}] |
52 (f : pre :: {K} -> nm :: Name -> t :: K -> post :: {K} -> [pre ~ post] => [[nm] ~ pre ++ post] => | 52 (f : pre :: {K} -> nm :: Name -> t :: K -> post :: {K} -> [pre ~ post] => [[nm] ~ pre ++ post] => |
53 eq r (pre ++ [nm = t] ++ post) -> tr1 t -> tr2 t -> tr3 t -> tf post -> tf ([nm = t] ++ post)) | 53 eq r (pre ++ [nm = t] ++ post) -> tr1 t -> tr2 t -> tr3 t -> tf post -> tf ([nm = t] ++ post)) |
54 (i : tf []) (fl : folder r) (r1 : $(map tr1 r)) (r2 : $(map tr2 r)) (r3 : $(map tr3 r)) : tf r = | 54 (i : tf []) (fl : folder r) (r1 : $(map tr1 r)) (r2 : $(map tr2 r)) (r3 : $(map tr3 r)) : tf r = |
55 @@fold [fn r' => $(map tr1 r') -> $(map tr2 r') -> $(map tr3 r') -> tf r'] [r] | 55 @@fold [fn r' => $(map tr1 r') -> $(map tr2 r') -> $(map tr3 r') -> tf r'] [r] |
56 (fn [pre :: {K}] [nm :: Name] [t :: K] [post :: {K}] [pre ~ post] [[nm] ~ pre ++ post] pf acc r1 r2 r3 => | 56 (fn [pre :: {K}] [nm :: Name] [t :: K] [post :: {K}] [pre ~ post] [[nm] ~ pre ++ post] pf acc r1 r2 r3 => |
57 f [pre] [nm] [t] [post] ! ! pf r1.nm r2.nm r3.nm (acc (r1 -- nm) (r2 -- nm) (r3 -- nm))) | 57 f [pre] [nm] [t] [post] pf r1.nm r2.nm r3.nm (acc (r1 -- nm) (r2 -- nm) (r3 -- nm))) |
58 (fn _ _ _ => i) fl r1 r2 r3 | 58 (fn _ _ _ => i) fl r1 r2 r3 |
59 | 59 |
60 fun foldR4 [K] [tr1 :: K -> Type] [tr2 :: K -> Type] [tr3 :: K -> Type] [tr4 :: K -> Type] [tf :: {K} -> Type] [r ::: {K}] | 60 fun foldR4 [K] [tr1 :: K -> Type] [tr2 :: K -> Type] [tr3 :: K -> Type] [tr4 :: K -> Type] [tf :: {K} -> Type] [r ::: {K}] |
61 (f : pre :: {K} -> nm :: Name -> t :: K -> post :: {K} -> [pre ~ post] => [[nm] ~ pre ++ post] => | 61 (f : pre :: {K} -> nm :: Name -> t :: K -> post :: {K} -> [pre ~ post] => [[nm] ~ pre ++ post] => |
62 eq r (pre ++ [nm = t] ++ post) -> tr1 t -> tr2 t -> tr3 t -> tr4 t -> tf post -> tf ([nm = t] ++ post)) | 62 eq r (pre ++ [nm = t] ++ post) -> tr1 t -> tr2 t -> tr3 t -> tr4 t -> tf post -> tf ([nm = t] ++ post)) |
63 (i : tf []) (fl : folder r) (r1 : $(map tr1 r)) (r2 : $(map tr2 r)) (r3 : $(map tr3 r)) (r4 : $(map tr4 r)) : tf r = | 63 (i : tf []) (fl : folder r) (r1 : $(map tr1 r)) (r2 : $(map tr2 r)) (r3 : $(map tr3 r)) (r4 : $(map tr4 r)) : tf r = |
64 @@fold [fn r' => $(map tr1 r') -> $(map tr2 r') -> $(map tr3 r') -> $(map tr4 r') -> tf r'] [r] | 64 @@fold [fn r' => $(map tr1 r') -> $(map tr2 r') -> $(map tr3 r') -> $(map tr4 r') -> tf r'] [r] |
65 (fn [pre :: {K}] [nm :: Name] [t :: K] [post :: {K}] [pre ~ post] [[nm] ~ pre ++ post] pf acc r1 r2 r3 r4 => | 65 (fn [pre :: {K}] [nm :: Name] [t :: K] [post :: {K}] [pre ~ post] [[nm] ~ pre ++ post] pf acc r1 r2 r3 r4 => |
66 f [pre] [nm] [t] [post] ! ! pf r1.nm r2.nm r3.nm r4.nm (acc (r1 -- nm) (r2 -- nm) (r3 -- nm) (r4 -- nm))) | 66 f [pre] [nm] [t] [post] pf r1.nm r2.nm r3.nm r4.nm (acc (r1 -- nm) (r2 -- nm) (r3 -- nm) (r4 -- nm))) |
67 (fn _ _ _ _ => i) fl r1 r2 r3 r4 | 67 (fn _ _ _ _ => i) fl r1 r2 r3 r4 |
68 | 68 |
69 fun mp [K] [tr :: K -> Type] [tf :: K -> Type] [r ::: {K}] | 69 fun mp [K] [tr :: K -> Type] [tf :: K -> Type] [r ::: {K}] |
70 (f : nm :: Name -> t :: K -> rest :: {K} -> [[nm] ~ rest] => | 70 (f : nm :: Name -> t :: K -> rest :: {K} -> [[nm] ~ rest] => |
71 eq r ([nm = t] ++ rest) -> tr t -> tf t) | 71 eq r ([nm = t] ++ rest) -> tr t -> tf t) |
72 (fl : folder r) (r : $(map tr r)) : $(map tf r) = | 72 (fl : folder r) (r : $(map tr r)) : $(map tf r) = |
73 @@foldR [tr] [fn r => $(map tf r)] [r] | 73 @@foldR [tr] [fn r => $(map tf r)] [r] |
74 (fn [pre :: {K}] [nm :: Name] [t :: K] [post :: {K}] [pre ~ post] [[nm] ~ pre ++ post] pf r acc => | 74 (fn [pre :: {K}] [nm :: Name] [t :: K] [post :: {K}] [pre ~ post] [[nm] ~ pre ++ post] pf r acc => |
75 {nm = f [nm] [t] [pre ++ post] ! pf r} ++ acc) | 75 {nm = f [nm] [t] [pre ++ post] pf r} ++ acc) |
76 {} fl r | 76 {} fl r |