|
adam@6
|
1 con eq = K ==> fn (t1 :: K) (t2 :: K) => f :: (K -> Type) -> f t1 -> f t2
|
|
adam@6
|
2
|
|
adam@6
|
3 val refl [K] [t ::: K] : eq t t = fn [f :: (K -> Type)] x => x
|
|
adam@6
|
4
|
|
adam@6
|
5 fun sym [K] [t1 ::: K] [t2 ::: K] (e : eq t1 t2) : eq t2 t1 =
|
|
adam@6
|
6 e [fn t => eq t t1] refl
|
|
adam@6
|
7
|
|
adam@6
|
8 fun trans [K] [t1 ::: K] [t2 ::: K] [t3 ::: K] (e1 : eq t1 t2) (e2 : eq t2 t3) : eq t1 t3 =
|
|
adam@6
|
9 (sym e1) [fn t => eq t t3] e2
|
|
adam@6
|
10
|
|
adam@6
|
11 fun cast [K] [t1 ::: K] [t2 ::: K] (e : eq t1 t2) = e
|
|
adam@6
|
12
|
|
adam@6
|
13 fun fold [K] [tf :: {K} -> Type] [r ::: {K}]
|
|
adam@6
|
14 (f : pre :: {K} -> nm :: Name -> v :: K -> post :: {K} -> [pre ~ post] => [[nm] ~ pre ++ post] =>
|
|
adam@6
|
15 eq r (pre ++ [nm = v] ++ post) -> tf post -> tf ([nm = v] ++ post))
|
|
adam@6
|
16 (i : tf []) (fl : folder r) : tf r =
|
|
adam@6
|
17 @@Top.fold [fn post => pre :: {K} -> [pre ~ post] => eq r (pre ++ post) -> tf post]
|
|
adam@6
|
18 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest]
|
|
adam@6
|
19 (acc : pre :: {K} -> [pre ~ rest] => eq r (pre ++ rest) -> tf rest)
|
|
adam@6
|
20 [pre :: {K}] [pre ~ [nm = t] ++ rest] pf =>
|
|
adam@6
|
21 f [pre] [nm] [t] [rest] ! ! pf (acc [[nm = t] ++ pre] ! pf))
|
|
adam@6
|
22 (fn [pre :: {K}] [pre ~ []] _ => i) [r] fl [[]] ! refl
|
|
adam@6
|
23
|
|
adam@6
|
24 fun foldUR [tr :: Type] [tf :: {Unit} -> Type] [r ::: {Unit}]
|
|
adam@6
|
25 (f : pre :: {Unit} -> nm :: Name -> post :: {Unit} -> [pre ~ post] => [[nm] ~ pre ++ post] =>
|
|
adam@6
|
26 eq r (pre ++ [nm] ++ post) -> tr -> tf post -> tf ([nm] ++ post))
|
|
adam@6
|
27 (i : tf []) (fl : folder r) (r : $(mapU tr r)) : tf r =
|
|
adam@6
|
28 @@fold [fn r' => $(mapU tr r') -> tf r'] [r]
|
|
adam@6
|
29 (fn [pre :: {Unit}] [nm :: Name] [u :: Unit] [post :: {Unit}] [pre ~ post] [[nm] ~ pre ++ post] pf acc r =>
|
|
adam@6
|
30 f [pre] [nm] [post] ! ! pf r.nm (acc (r -- nm)))
|
|
adam@6
|
31 (fn _ => i) fl r
|
|
adam@6
|
32
|
|
adam@6
|
33 fun foldR [K] [tr :: K -> Type] [tf :: {K} -> Type] [r ::: {K}]
|
|
adam@6
|
34 (f : pre :: {K} -> nm :: Name -> t :: K -> post :: {K} -> [pre ~ post] => [[nm] ~ pre ++ post] =>
|
|
adam@6
|
35 eq r (pre ++ [nm = t] ++ post) -> tr t -> tf post -> tf ([nm = t] ++ post))
|
|
adam@6
|
36 (i : tf []) (fl : folder r) (r : $(map tr r)) : tf r =
|
|
adam@6
|
37 @@fold [fn r' => $(map tr r') -> tf r'] [r]
|
|
adam@6
|
38 (fn [pre :: {K}] [nm :: Name] [t :: K] [post :: {K}] [pre ~ post] [[nm] ~ pre ++ post] pf acc r =>
|
|
adam@6
|
39 f [pre] [nm] [t] [post] ! ! pf r.nm (acc (r -- nm)))
|
|
adam@6
|
40 (fn _ => i) fl r
|
|
adam@6
|
41
|
|
adam@6
|
42 fun foldR2 [K] [tr1 :: K -> Type] [tr2 :: K -> Type] [tf :: {K} -> Type] [r ::: {K}]
|
|
adam@6
|
43 (f : pre :: {K} -> nm :: Name -> t :: K -> post :: {K} -> [pre ~ post] => [[nm] ~ pre ++ post] =>
|
|
adam@6
|
44 eq r (pre ++ [nm = t] ++ post) -> tr1 t -> tr2 t -> tf post -> tf ([nm = t] ++ post))
|
|
adam@6
|
45 (i : tf []) (fl : folder r) (r1 : $(map tr1 r)) (r2 : $(map tr2 r)) : tf r =
|
|
adam@6
|
46 @@fold [fn r' => $(map tr1 r') -> $(map tr2 r') -> tf r'] [r]
|
|
adam@6
|
47 (fn [pre :: {K}] [nm :: Name] [t :: K] [post :: {K}] [pre ~ post] [[nm] ~ pre ++ post] pf acc r1 r2 =>
|
|
adam@6
|
48 f [pre] [nm] [t] [post] ! ! pf r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm)))
|
|
adam@6
|
49 (fn _ _ => i) fl r1 r2
|
|
adam@6
|
50
|
|
adam@6
|
51 fun foldR3 [K] [tr1 :: K -> Type] [tr2 :: K -> Type] [tr3 :: K -> Type] [tf :: {K} -> Type] [r ::: {K}]
|
|
adam@6
|
52 (f : pre :: {K} -> nm :: Name -> t :: K -> post :: {K} -> [pre ~ post] => [[nm] ~ pre ++ post] =>
|
|
adam@6
|
53 eq r (pre ++ [nm = t] ++ post) -> tr1 t -> tr2 t -> tr3 t -> tf post -> tf ([nm = t] ++ post))
|
|
adam@6
|
54 (i : tf []) (fl : folder r) (r1 : $(map tr1 r)) (r2 : $(map tr2 r)) (r3 : $(map tr3 r)) : tf r =
|
|
adam@6
|
55 @@fold [fn r' => $(map tr1 r') -> $(map tr2 r') -> $(map tr3 r') -> tf r'] [r]
|
|
adam@6
|
56 (fn [pre :: {K}] [nm :: Name] [t :: K] [post :: {K}] [pre ~ post] [[nm] ~ pre ++ post] pf acc r1 r2 r3 =>
|
|
adam@6
|
57 f [pre] [nm] [t] [post] ! ! pf r1.nm r2.nm r3.nm (acc (r1 -- nm) (r2 -- nm) (r3 -- nm)))
|
|
adam@6
|
58 (fn _ _ _ => i) fl r1 r2 r3
|
|
adam@6
|
59
|
|
adam@6
|
60 fun foldR4 [K] [tr1 :: K -> Type] [tr2 :: K -> Type] [tr3 :: K -> Type] [tr4 :: K -> Type] [tf :: {K} -> Type] [r ::: {K}]
|
|
adam@6
|
61 (f : pre :: {K} -> nm :: Name -> t :: K -> post :: {K} -> [pre ~ post] => [[nm] ~ pre ++ post] =>
|
|
adam@6
|
62 eq r (pre ++ [nm = t] ++ post) -> tr1 t -> tr2 t -> tr3 t -> tr4 t -> tf post -> tf ([nm = t] ++ post))
|
|
adam@6
|
63 (i : tf []) (fl : folder r) (r1 : $(map tr1 r)) (r2 : $(map tr2 r)) (r3 : $(map tr3 r)) (r4 : $(map tr4 r)) : tf r =
|
|
adam@6
|
64 @@fold [fn r' => $(map tr1 r') -> $(map tr2 r') -> $(map tr3 r') -> $(map tr4 r') -> tf r'] [r]
|
|
adam@6
|
65 (fn [pre :: {K}] [nm :: Name] [t :: K] [post :: {K}] [pre ~ post] [[nm] ~ pre ++ post] pf acc r1 r2 r3 r4 =>
|
|
adam@6
|
66 f [pre] [nm] [t] [post] ! ! pf r1.nm r2.nm r3.nm r4.nm (acc (r1 -- nm) (r2 -- nm) (r3 -- nm) (r4 -- nm)))
|
|
adam@6
|
67 (fn _ _ _ _ => i) fl r1 r2 r3 r4
|
|
adam@6
|
68
|
|
adam@6
|
69 fun mp [K] [tr :: K -> Type] [tf :: K -> Type] [r ::: {K}]
|
|
adam@6
|
70 (f : nm :: Name -> t :: K -> rest :: {K} -> [[nm] ~ rest] =>
|
|
adam@6
|
71 eq r ([nm = t] ++ rest) -> tr t -> tf t)
|
|
adam@6
|
72 (fl : folder r) (r : $(map tr r)) : $(map tf r) =
|
|
adam@6
|
73 @@foldR [tr] [fn r => $(map tf r)] [r]
|
|
adam@6
|
74 (fn [pre :: {K}] [nm :: Name] [t :: K] [post :: {K}] [pre ~ post] [[nm] ~ pre ++ post] pf r acc =>
|
|
adam@6
|
75 {nm = f [nm] [t] [pre ++ post] ! pf r} ++ acc)
|
|
adam@6
|
76 {} fl r
|
