|
adam@6
|
1 fun read [r ::: {Unit}] [t ::: Type] (fl : folder r) (r : $(mapU t r)) (v : variant (mapU {} r)) : t =
|
|
adam@6
|
2 match v
|
|
adam@6
|
3 (@fold [fn r => r' :: {Unit} -> [r ~ r'] => $(mapU t (r ++ r')) -> $(mapU ({} -> t) r)]
|
|
adam@6
|
4 (fn [nm :: Name] [u::_] [us::_] [[nm] ~ us] (cs : r' :: {Unit} -> [us ~ r'] => $(mapU t (us ++ r')) -> _) [r'::_] [[nm = u] ++ us ~ r'] r =>
|
|
adam@14
|
5 {nm = fn () => r.nm} ++ cs [[nm = u] ++ r'] r)
|
|
adam@6
|
6 (fn [r'::_] [[] ~ r'] _ => {}) fl [[]] ! r)
|
|
adam@6
|
7
|
|
adam@6
|
8 fun write [r ::: {Unit}] [t ::: Type] (fl : folder r) (r : $(mapU t r)) (v : variant (mapU {} r)) (x : t) : $(mapU t r) =
|
|
adam@6
|
9 match v
|
|
adam@6
|
10 (@fold [fn r => r' :: {Unit} -> [r ~ r'] => $(mapU t (r ++ r')) -> $(mapU ({} -> $(mapU t (r ++ r'))) r)]
|
|
adam@6
|
11 (fn [nm :: Name] [u::_] [us::_] [[nm] ~ us]
|
|
adam@6
|
12 (cs : r' :: {Unit} -> [us ~ r'] => $(mapU t (us ++ r')) -> $(mapU ({} -> $(mapU t (us ++ r'))) us))
|
|
adam@6
|
13 [r'::_] [[nm = u] ++ us ~ r'] r =>
|
|
adam@14
|
14 {nm = fn () => r -- nm ++ {nm = x}} ++ cs [[nm = u] ++ r'] r)
|
|
adam@6
|
15 (fn [r'::_] [[] ~ r'] _ => {}) fl [[]] ! r)
|
|
adam@6
|
16
|
|
adam@6
|
17 fun search [r] [t] (f : variant (mapU {} r) -> option t) (fl : folder r) : option t =
|
|
adam@6
|
18 @fold [fn r => r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> option t) -> option t]
|
|
adam@6
|
19 (fn [nm :: Name] [u ::_] [r ::_] [[nm] ~ r]
|
|
adam@6
|
20 (acc : r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> option t) -> option t)
|
|
adam@6
|
21 [r' ::_] [[nm] ++ r ~ r'] f' =>
|
|
adam@6
|
22 case f' (make [nm] {}) of
|
|
adam@14
|
23 None => acc [[nm] ++ r'] f'
|
|
adam@6
|
24 | v => v)
|
|
adam@6
|
25 (fn [r' ::_] [[] ~ r'] _ => None) fl [[]] ! f
|
|
adam@6
|
26
|
|
adam@6
|
27 fun find [r] (f : variant (mapU {} r) -> bool) (fl : folder r) : option (variant (mapU {} r)) =
|
|
adam@6
|
28 @search (fn v => if f v then Some v else None) fl
|
|
adam@6
|
29
|
|
adam@6
|
30 fun test [nm :: Name] [t ::: Type] [ts ::: {Type}] [[nm] ~ ts] (fl : folder ([nm = t] ++ ts))
|
|
adam@6
|
31 (v : variant ([nm = t] ++ ts)) : option t =
|
|
adam@6
|
32 match v ({nm = Some}
|
|
adam@6
|
33 ++ (@map0 [fn t' => t' -> option t] (fn [t' :: Type] _ => None) fl -- nm))
|
|
adam@6
|
34
|
|
adam@6
|
35 fun testLess [nm :: Name] [t ::: Type] [ts ::: {Type}] [[nm] ~ ts] (fl : folder ts) (v : variant ([nm = t] ++ ts)) : option t =
|
|
adam@6
|
36 match v ({nm = Some}
|
|
adam@6
|
37 ++ @map0 [fn t' => t' -> option t] (fn [t' :: Type] _ => None) fl)
|
|
adam@6
|
38
|
|
adam@21
|
39 fun weaken [r1 ::: {Type}] [r2 ::: {Type}] [r1 ~ r2] (fl : folder r1) (v : variant r1) : variant (r1 ++ r2) =
|
|
adam@21
|
40 match v
|
|
adam@21
|
41 (@fold [fn r => r' :: {Type} -> [r ~ r'] => $(map (fn t => t -> variant (r ++ r')) r)]
|
|
adam@21
|
42 (fn [nm :: Name] [t ::_] [r ::_] [[nm] ~ r] (acc : r' :: {Type} -> [r ~ r'] => $(map (fn t => t -> variant (r ++ r')) r)) [r'::_] [[nm = t] ++ r ~ r'] =>
|
|
adam@21
|
43 {nm = make [nm]} ++ acc [[nm = t] ++ r'])
|
|
adam@21
|
44 (fn [r'::_] [[] ~ r'] => {}) fl [r2] !)
|
|
adam@21
|
45
|
|
adam@6
|
46 fun eq [r] (fl : folder r) (v1 : variant (mapU {} r)) (v2 : variant (mapU {} r)) : bool =
|
|
adam@6
|
47 match v1
|
|
adam@6
|
48 (@fold [fn r => r' :: {Unit} -> [r ~ r'] => folder (r ++ r') -> variant (mapU {} (r ++ r')) -> $(mapU ({} -> bool) r)]
|
|
adam@6
|
49 (fn [nm ::_] [u ::_] [r ::_] [[nm] ~ r]
|
|
adam@6
|
50 (acc : r' :: {Unit} -> [r ~ r'] => folder (r ++ r') -> variant (mapU {} (r ++ r')) -> $(mapU ({} -> bool) r))
|
|
adam@6
|
51 [r' ::_] [[nm] ++ r ~ r'] (fl' : folder ([nm] ++ r ++ r')) v =>
|
|
adam@6
|
52 {nm = fn () => Option.isSome (@test [nm] ! (@Folder.mp fl') v)}
|
|
adam@14
|
53 ++ @acc [[nm] ++ r'] ! fl' v)
|
|
adam@6
|
54 (fn [r' ::_] [[] ~ r'] _ _ => {}) fl [[]] ! fl v2)
|
|
adam@6
|
55
|
|
adam@6
|
56 fun fold [r] [t] (fl : folder r) (f : variant (mapU {} r) -> t -> t) : t -> t =
|
|
adam@6
|
57 @Top.fold [fn r => r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> t -> t) -> t -> t]
|
|
adam@6
|
58 (fn [nm :: Name] [u ::_] [r ::_] [[nm] ~ r]
|
|
adam@6
|
59 (acc : r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> t -> t) -> t -> t)
|
|
adam@6
|
60 [r' ::_] [[nm] ++ r ~ r'] f' acc' =>
|
|
adam@14
|
61 f' (make [nm] {}) (acc [[nm] ++ r'] f' acc'))
|
|
adam@6
|
62 (fn [r' ::_] [[] ~ r'] _ x => x) fl [[]] ! f
|
|
adam@6
|
63
|
|
adam@21
|
64 fun mp [r ::: {Unit}] [t ::: Type] (fl : folder r) (f : variant (mapU {} r) -> t) : $(mapU t r) =
|
|
adam@21
|
65 @Top.fold [fn r => r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> t) -> $(mapU t r)]
|
|
adam@21
|
66 (fn [nm :: Name] [u ::_] [r ::_] [[nm] ~ r]
|
|
adam@21
|
67 (acc : r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> t) -> $(mapU t r))
|
|
adam@21
|
68 [r' ::_] [[nm] ++ r ~ r'] f' =>
|
|
adam@21
|
69 {nm = f' (make [nm] {})} ++ acc [[nm] ++ r'] f')
|
|
adam@21
|
70 (fn [r' ::_] [[] ~ r'] _ => {}) fl [[]] ! f
|
|
adam@21
|
71
|
|
adam@20
|
72 fun foldR [tr] [r] [t] (fl : folder r) (f : variant (mapU {} r) -> tr -> t -> t) (record : $(mapU tr r)) : t -> t =
|
|
adam@20
|
73 @Top.foldUR [tr] [fn r => r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> tr -> t -> t) -> t -> t]
|
|
adam@20
|
74 (fn [nm :: Name] [r ::_] [[nm] ~ r] (v : tr)
|
|
adam@20
|
75 (acc : r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> tr -> t -> t) -> t -> t)
|
|
adam@20
|
76 [r' ::_] [[nm] ++ r ~ r'] f' acc' =>
|
|
adam@20
|
77 f' (make [nm] {}) v (acc [[nm] ++ r'] f' acc'))
|
|
adam@20
|
78 (fn [r' ::_] [[] ~ r'] _ x => x) fl record [[]] ! f
|
|
adam@20
|
79
|
|
adam@20
|
80 fun appR [m] (_ : monad m) [tr] [r] (fl : folder r) (f : variant (mapU {} r) -> tr -> m {}) (record : $(mapU tr r)) : m {} =
|
|
adam@20
|
81 @foldR fl (fn var this acc => f var this; acc) record (return ())
|
|
adam@20
|
82
|
|
adam@21
|
83 fun mapR [tr] [t] [r] (fl : folder r) (f : variant (mapU {} r) -> tr -> t) (record : $(mapU tr r)) : $(mapU t r) =
|
|
adam@21
|
84 @Top.fold [fn r => r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> tr -> t) -> $(mapU tr r) -> $(mapU t r)]
|
|
adam@21
|
85 (fn [nm :: Name] [u ::_] [r ::_] [[nm] ~ r]
|
|
adam@21
|
86 (acc : r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> tr -> t) -> $(mapU tr r) -> $(mapU t r))
|
|
adam@21
|
87 [r' ::_] [[nm] ++ r ~ r'] f' vs =>
|
|
adam@21
|
88 {nm = f' (make [nm] {}) vs.nm} ++ acc [[nm] ++ r'] f' (vs -- nm))
|
|
adam@21
|
89 (fn [r' ::_] [[] ~ r'] _ _ => {}) fl [[]] ! f record
|
|
adam@21
|
90
|
|
adam@6
|
91 fun destrR [K] [f :: K -> Type] [fr :: K -> Type] [t ::: Type]
|
|
adam@6
|
92 (f : p :: K -> f p -> fr p -> t)
|
|
adam@6
|
93 [r ::: {K}] (fl : folder r) (v : variant (map f r)) (r : $(map fr r)) : t =
|
|
adam@6
|
94 match v
|
|
adam@6
|
95 (@Top.mp [fr] [fn p => f p -> t]
|
|
adam@6
|
96 (fn [p] (m : fr p) (v : f p) => f [p] v m)
|
|
adam@6
|
97 fl r)
|
|
adam@6
|
98
|
|
adam@6
|
99 fun destr2R [K] [f1 :: K -> Type] [f2 :: K -> Type] [fr :: K -> Type] [t ::: Type]
|
|
adam@6
|
100 (f : p :: K -> f1 p -> f2 p -> fr p -> t)
|
|
adam@6
|
101 [r ::: {K}] (fl : folder r) (v1 : variant (map f1 r)) (v2 : variant (map f2 r)) (r : $(map fr r)) : option t =
|
|
adam@6
|
102 match v1
|
|
adam@20
|
103 (@Top.foldR [fr] [fn r => others :: {K} -> [others ~ r] =>
|
|
adam@6
|
104 folder (r ++ others)
|
|
adam@6
|
105 -> variant (map f2 (r ++ others))
|
|
adam@6
|
106 -> $(map (fn p => f1 p -> option t) r)]
|
|
adam@6
|
107 (fn [nm ::_] [p ::_] [r ::_] [[nm] ~ r] (meta : fr p)
|
|
adam@6
|
108 (acc : others :: {K} -> [others ~ r] =>
|
|
adam@6
|
109 folder (r ++ others)
|
|
adam@6
|
110 -> variant (map f2 (r ++ others))
|
|
adam@6
|
111 -> $(map (fn p => f1 p -> option t) r))
|
|
adam@6
|
112 [others :: {K}] [others ~ [nm = p] ++ r]
|
|
adam@6
|
113 (fl : folder ([nm = p] ++ r ++ others))
|
|
adam@6
|
114 (v2 : variant (map f2 ([nm = p] ++ r ++ others))) =>
|
|
adam@6
|
115 {nm = fn x1 => match v2
|
|
adam@6
|
116 ({nm = fn x2 => Some (f [p] x1 x2 meta)}
|
|
adam@6
|
117 ++ (@map0 [fn p => f2 p -> option t] (fn [p' ::_] _ => None) fl -- nm))}
|
|
adam@14
|
118 ++ @acc [[nm = p] ++ others] ! fl v2)
|
|
adam@6
|
119 (fn [others ::_] [others ~ []] _ _ => {})
|
|
adam@6
|
120 fl r [[]] ! fl v2)
|
|
adam@6
|
121
|
|
adam@6
|
122 fun testEq [K] [f :: K -> Type] [nm :: Name] [t ::: K] [ts ::: {K}] [r ::: {K}] [[nm] ~ ts]
|
|
adam@6
|
123 (pf : Eq.eq r ([nm = t] ++ ts)) (fl : folder r) (v : variant (map f r)) : option (f t) =
|
|
adam@6
|
124 @test [nm] ! (@Folder.mp (@Eq.cast pf [folder] fl))
|
|
adam@6
|
125 (Eq.cast pf [fn r => variant (map f r)] v)
|
|
adam@6
|
126
|
|
adam@6
|
127 fun makeEq [K] [f :: K -> Type] [nm :: Name] [t ::: K] [ts ::: {K}] [r ::: {K}] [[nm] ~ ts]
|
|
adam@6
|
128 (pf : Eq.eq r ([nm = t] ++ ts)) (x : f t) : variant (map f r) =
|
|
adam@6
|
129 Eq.cast (Eq.sym pf) [fn r => variant (map f r)] (make [nm] x)
|
|
ezyang@27
|
130
|
|
ezyang@27
|
131 con variantMake ts' ts = $(map (fn t => t -> variant ts') ts)
|
|
ezyang@27
|
132 con mkLabelsAccum r = s :: {Type} -> [r ~ s] => variantMake (r ++ s) r
|
|
ezyang@27
|
133 fun mkLabels [ts ::: {Type}] (fl : folder ts) : variantMake ts ts
|
|
ezyang@27
|
134 = @Top.fold [mkLabelsAccum]
|
|
ezyang@27
|
135 (fn [nm::_] [v::_] [r::_] [[nm] ~ r]
|
|
ezyang@27
|
136 (k : mkLabelsAccum r)
|
|
ezyang@27
|
137 [s::_] [[nm = v] ++ r ~ s] => k [[nm = v] ++ s] ++ {nm = make [nm]})
|
|
ezyang@27
|
138 (fn [s::_] [[] ~ s] => {}) fl [[]] !
|
|
ezyang@27
|
139
|
|
ezyang@27
|
140 class type_case = fn ts t a => (a -> variant ts) -> a -> t
|
|
ezyang@27
|
141
|
|
ezyang@27
|
142 fun declareCase [ts] [t] [a] (f : (a -> variant ts) -> a -> t) : type_case ts t a = f
|
|
ezyang@27
|
143 fun typeCase [ts] [t] (v : variant ts) (dstrs : $(map (type_case ts t) ts)) (fl : folder ts) : t
|
|
ezyang@27
|
144 (* Ur/Web not clever enough to calculate these folders, it seems *)
|
|
ezyang@27
|
145 = match v (@ap [fn a => a -> variant ts] [fn a => a -> t] fl dstrs (@mkLabels fl))
|
