adamc@20
|
1 (* Copyright (c) 2008, Adam Chlipala
|
adamc@20
|
2 * All rights reserved.
|
adamc@20
|
3 *
|
adamc@20
|
4 * Redistribution and use in source and binary forms, with or without
|
adamc@20
|
5 * modification, are permitted provided that the following conditions are met:
|
adamc@20
|
6 *
|
adamc@20
|
7 * - Redistributions of source code must retain the above copyright notice,
|
adamc@20
|
8 * this list of conditions and the following disclaimer.
|
adamc@20
|
9 * - Redistributions in binary form must reproduce the above copyright notice,
|
adamc@20
|
10 * this list of conditions and the following disclaimer in the documentation
|
adamc@20
|
11 * and/or other materials provided with the distribution.
|
adamc@20
|
12 * - The names of contributors may not be used to endorse or promote products
|
adamc@20
|
13 * derived from this software without specific prior written permission.
|
adamc@20
|
14 *
|
adamc@20
|
15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
|
adamc@20
|
16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
|
adamc@20
|
17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
|
adamc@20
|
18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
|
adamc@20
|
19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
|
adamc@20
|
20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
|
adamc@20
|
21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
|
adamc@20
|
22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
|
adamc@20
|
23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
|
adamc@20
|
24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
|
adamc@20
|
25 * POSSIBILITY OF SUCH DAMAGE.
|
adamc@20
|
26 *)
|
adamc@20
|
27
|
adamc@20
|
28 (* Simplify a Core program algebraically *)
|
adamc@20
|
29
|
adamc@20
|
30 structure Reduce :> REDUCE = struct
|
adamc@20
|
31
|
adamc@20
|
32 open Core
|
adamc@20
|
33
|
adamc@508
|
34 structure IM = IntBinaryMap
|
adamc@20
|
35
|
adamc@508
|
36 datatype env_item =
|
adamc@626
|
37 UnknownK
|
adamc@626
|
38 | KnownK of kind
|
adamc@626
|
39
|
adamc@626
|
40 | UnknownC
|
adamc@508
|
41 | KnownC of con
|
adamc@21
|
42
|
adamc@508
|
43 | UnknownE
|
adamc@508
|
44 | KnownE of exp
|
adamc@20
|
45
|
adamc@626
|
46 | Lift of int * int * int
|
adamc@20
|
47
|
adamc@508
|
48 type env = env_item list
|
adamc@20
|
49
|
adamc@510
|
50 fun ei2s ei =
|
adamc@510
|
51 case ei of
|
adamc@626
|
52 UnknownK => "UK"
|
adamc@626
|
53 | KnownK _ => "KK"
|
adamc@626
|
54 | UnknownC => "UC"
|
adamc@510
|
55 | KnownC _ => "KC"
|
adamc@510
|
56 | UnknownE => "UE"
|
adamc@510
|
57 | KnownE _ => "KE"
|
adamc@626
|
58 | Lift (_, n1, n2) => "(" ^ Int.toString n1 ^ ", " ^ Int.toString n2 ^ ")"
|
adamc@510
|
59
|
adamc@510
|
60 fun e2s env = String.concatWith " " (map ei2s env)
|
adamc@510
|
61
|
adamc@510
|
62 val deKnown = List.filter (fn KnownC _ => false
|
adamc@510
|
63 | KnownE _ => false
|
adamc@626
|
64 | KnownK _ => false
|
adamc@510
|
65 | _ => true)
|
adamc@510
|
66
|
adamc@626
|
67 fun kindConAndExp (namedC, namedE) =
|
adamc@508
|
68 let
|
adamc@626
|
69 fun kind env (all as (k, loc)) =
|
adamc@626
|
70 case k of
|
adamc@626
|
71 KType => all
|
adamc@626
|
72 | KArrow (k1, k2) => (KArrow (kind env k1, kind env k2), loc)
|
adamc@626
|
73 | KName => all
|
adamc@626
|
74 | KRecord k => (KRecord (kind env k), loc)
|
adamc@626
|
75 | KUnit => all
|
adamc@626
|
76 | KTuple ks => (KTuple (map (kind env) ks), loc)
|
adamc@626
|
77
|
adamc@626
|
78 | KRel n =>
|
adamc@626
|
79 let
|
adamc@626
|
80 fun find (n', env, nudge, lift) =
|
adamc@626
|
81 case env of
|
adamc@626
|
82 [] => raise Fail "Reduce.kind: KRel"
|
adamc@626
|
83 | UnknownC :: rest => find (n', rest, nudge, lift)
|
adamc@626
|
84 | KnownC _ :: rest => find (n', rest, nudge, lift)
|
adamc@626
|
85 | UnknownE :: rest => find (n', rest, nudge, lift)
|
adamc@626
|
86 | KnownE _ :: rest => find (n', rest, nudge, lift)
|
adamc@626
|
87 | Lift (lift', _, _) :: rest => find (n', rest, nudge + lift', lift + lift')
|
adamc@626
|
88 | UnknownK :: rest =>
|
adamc@626
|
89 if n' = 0 then
|
adamc@626
|
90 (KRel (n + nudge), loc)
|
adamc@626
|
91 else
|
adamc@626
|
92 find (n' - 1, rest, nudge, lift + 1)
|
adamc@626
|
93 | KnownK k :: rest =>
|
adamc@626
|
94 if n' = 0 then
|
adamc@626
|
95 kind (Lift (lift, 0, 0) :: rest) k
|
adamc@626
|
96 else
|
adamc@626
|
97 find (n' - 1, rest, nudge - 1, lift)
|
adamc@626
|
98 in
|
adamc@626
|
99 find (n, env, 0, 0)
|
adamc@626
|
100 end
|
adamc@626
|
101 | KFun (x, k) => (KFun (x, kind (UnknownK :: env) k), loc)
|
adamc@626
|
102
|
adamc@508
|
103 fun con env (all as (c, loc)) =
|
adamc@510
|
104 ((*Print.prefaces "con" [("c", CorePrint.p_con CoreEnv.empty all)];*)
|
adamc@508
|
105 case c of
|
adamc@508
|
106 TFun (c1, c2) => (TFun (con env c1, con env c2), loc)
|
adamc@626
|
107 | TCFun (x, k, c2) => (TCFun (x, kind env k, con (UnknownC :: env) c2), loc)
|
adamc@626
|
108 | TKFun (x, c2) => (TKFun (x, con (UnknownK :: env) c2), loc)
|
adamc@508
|
109 | TRecord c => (TRecord (con env c), loc)
|
adamc@215
|
110
|
adamc@508
|
111 | CRel n =>
|
adamc@508
|
112 let
|
adamc@626
|
113 fun find (n', env, nudge, liftK, liftC) =
|
adamc@510
|
114 case env of
|
adamc@510
|
115 [] => raise Fail "Reduce.con: CRel"
|
adamc@626
|
116 | UnknownK :: rest => find (n', rest, nudge, liftK + 1, liftC)
|
adamc@626
|
117 | KnownK _ :: rest => find (n', rest, nudge, liftK, liftC)
|
adamc@626
|
118 | UnknownE :: rest => find (n', rest, nudge, liftK, liftC)
|
adamc@626
|
119 | KnownE _ :: rest => find (n', rest, nudge, liftK, liftC)
|
adamc@626
|
120 | Lift (liftK', liftC', _) :: rest => find (n', rest, nudge + liftC',
|
adamc@626
|
121 liftK + liftK', liftC + liftC')
|
adamc@510
|
122 | UnknownC :: rest =>
|
adamc@510
|
123 if n' = 0 then
|
adamc@510
|
124 (CRel (n + nudge), loc)
|
adamc@510
|
125 else
|
adamc@626
|
126 find (n' - 1, rest, nudge, liftK, liftC + 1)
|
adamc@510
|
127 | KnownC c :: rest =>
|
adamc@510
|
128 if n' = 0 then
|
adamc@626
|
129 con (Lift (liftK, liftC, 0) :: rest) c
|
adamc@510
|
130 else
|
adamc@626
|
131 find (n' - 1, rest, nudge - 1, liftK, liftC)
|
adamc@508
|
132 in
|
adamc@510
|
133 (*print (Int.toString n ^ ": " ^ e2s env ^ "\n");*)
|
adamc@626
|
134 find (n, env, 0, 0, 0)
|
adamc@508
|
135 end
|
adamc@508
|
136 | CNamed n =>
|
adamc@508
|
137 (case IM.find (namedC, n) of
|
adamc@508
|
138 NONE => all
|
adamc@508
|
139 | SOME c => c)
|
adamc@508
|
140 | CFfi _ => all
|
adamc@508
|
141 | CApp (c1, c2) =>
|
adamc@508
|
142 let
|
adamc@508
|
143 val c1 = con env c1
|
adamc@508
|
144 val c2 = con env c2
|
adamc@508
|
145 in
|
adamc@508
|
146 case #1 c1 of
|
adamc@508
|
147 CAbs (_, _, b) =>
|
adamc@510
|
148 con (KnownC c2 :: deKnown env) b
|
adamc@215
|
149
|
adamc@621
|
150 | CApp ((CMap (dom, ran), _), f) =>
|
adamc@508
|
151 (case #1 c2 of
|
adamc@626
|
152 CRecord (_, []) => (CRecord (kind env ran, []), loc)
|
adamc@621
|
153 | CRecord (_, (x, c) :: rest) =>
|
adamc@510
|
154 con (deKnown env)
|
adamc@621
|
155 (CConcat ((CRecord (ran, [(x, (CApp (f, c), loc))]), loc),
|
adamc@626
|
156 (CApp (c1, (CRecord (kind env dom, rest), loc)), loc)), loc)
|
adamc@508
|
157 | _ => (CApp (c1, c2), loc))
|
adamc@20
|
158
|
adamc@508
|
159 | _ => (CApp (c1, c2), loc)
|
adamc@508
|
160 end
|
adamc@626
|
161 | CAbs (x, k, b) => (CAbs (x, kind env k, con (UnknownC :: env) b), loc)
|
adamc@626
|
162
|
adamc@626
|
163 | CKApp (c1, k) =>
|
adamc@626
|
164 let
|
adamc@626
|
165 val c1 = con env c1
|
adamc@626
|
166 in
|
adamc@626
|
167 case #1 c1 of
|
adamc@626
|
168 CKAbs (_, b) =>
|
adamc@626
|
169 con (KnownK k :: deKnown env) b
|
adamc@626
|
170
|
adamc@626
|
171 | _ => (CKApp (c1, kind env k), loc)
|
adamc@626
|
172 end
|
adamc@626
|
173 | CKAbs (x, b) => (CKAbs (x, con (UnknownK :: env) b), loc)
|
adamc@20
|
174
|
adamc@508
|
175 | CName _ => all
|
adamc@21
|
176
|
adamc@626
|
177 | CRecord (k, xcs) => (CRecord (kind env k, map (fn (x, c) => (con env x, con env c)) xcs), loc)
|
adamc@508
|
178 | CConcat (c1, c2) =>
|
adamc@508
|
179 let
|
adamc@508
|
180 val c1 = con env c1
|
adamc@508
|
181 val c2 = con env c2
|
adamc@508
|
182 in
|
adamc@508
|
183 case (#1 c1, #1 c2) of
|
adamc@508
|
184 (CRecord (k, xcs1), CRecord (_, xcs2)) =>
|
adamc@626
|
185 (CRecord (kind env k, xcs1 @ xcs2), loc)
|
adamc@508
|
186 | _ => (CConcat (c1, c2), loc)
|
adamc@508
|
187 end
|
adamc@626
|
188 | CMap (dom, ran) => (CMap (kind env dom, kind env ran), loc)
|
adamc@74
|
189
|
adamc@508
|
190 | CUnit => all
|
adamc@21
|
191
|
adamc@508
|
192 | CTuple cs => (CTuple (map (con env) cs), loc)
|
adamc@508
|
193 | CProj (c, n) =>
|
adamc@508
|
194 let
|
adamc@508
|
195 val c = con env c
|
adamc@508
|
196 in
|
adamc@508
|
197 case #1 c of
|
adamc@508
|
198 CTuple cs => List.nth (cs, n - 1)
|
adamc@508
|
199 | _ => (CProj (c, n), loc)
|
adamc@510
|
200 end)
|
adamc@22
|
201
|
adamc@509
|
202 fun patCon pc =
|
adamc@509
|
203 case pc of
|
adamc@509
|
204 PConVar _ => pc
|
adamc@509
|
205 | PConFfi {mod = m, datatyp, params, con = c, arg, kind} =>
|
adamc@509
|
206 PConFfi {mod = m, datatyp = datatyp, params = params, con = c,
|
adamc@509
|
207 arg = Option.map (con (map (fn _ => UnknownC) params)) arg,
|
adamc@509
|
208 kind = kind}
|
adamc@509
|
209
|
adamc@509
|
210
|
adamc@509
|
211 val k = (KType, ErrorMsg.dummySpan)
|
adamc@509
|
212 fun doPart e (this as (x, t), rest) =
|
adamc@509
|
213 ((x, (EField (e, x, {field = t, rest = (CRecord (k, rest), #2 t)}), #2 t), t),
|
adamc@509
|
214 this :: rest)
|
adamc@509
|
215
|
adamc@509
|
216 fun exp env (all as (e, loc)) =
|
adamc@510
|
217 ((*Print.prefaces "exp" [("e", CorePrint.p_exp CoreEnv.empty all),
|
adamc@510
|
218 ("env", Print.PD.string (e2s env))];*)
|
adamc@509
|
219 case e of
|
adamc@509
|
220 EPrim _ => all
|
adamc@509
|
221 | ERel n =>
|
adamc@509
|
222 let
|
adamc@626
|
223 fun find (n', env, nudge, liftK, liftC, liftE) =
|
adamc@510
|
224 case env of
|
adamc@510
|
225 [] => raise Fail "Reduce.exp: ERel"
|
adamc@626
|
226 | UnknownK :: rest => find (n', rest, nudge, liftK + 1, liftC, liftE)
|
adamc@626
|
227 | KnownK _ :: rest => find (n', rest, nudge, liftK, liftC, liftE)
|
adamc@626
|
228 | UnknownC :: rest => find (n', rest, nudge, liftK, liftC + 1, liftE)
|
adamc@626
|
229 | KnownC _ :: rest => find (n', rest, nudge, liftK, liftC, liftE)
|
adamc@626
|
230 | Lift (liftK', liftC', liftE') :: rest =>
|
adamc@626
|
231 find (n', rest, nudge + liftE',
|
adamc@626
|
232 liftK + liftK', liftC + liftC', liftE + liftE')
|
adamc@510
|
233 | UnknownE :: rest =>
|
adamc@510
|
234 if n' = 0 then
|
adamc@510
|
235 (ERel (n + nudge), loc)
|
adamc@510
|
236 else
|
adamc@626
|
237 find (n' - 1, rest, nudge, liftK, liftC, liftE + 1)
|
adamc@510
|
238 | KnownE e :: rest =>
|
adamc@510
|
239 if n' = 0 then
|
adamc@510
|
240 ((*print "SUBSTITUTING\n";*)
|
adamc@626
|
241 exp (Lift (liftK, liftC, liftE) :: rest) e)
|
adamc@510
|
242 else
|
adamc@626
|
243 find (n' - 1, rest, nudge - 1, liftK, liftC, liftE)
|
adamc@509
|
244 in
|
adamc@510
|
245 (*print (Int.toString n ^ ": " ^ e2s env ^ "\n");*)
|
adamc@626
|
246 find (n, env, 0, 0, 0, 0)
|
adamc@509
|
247 end
|
adamc@509
|
248 | ENamed n =>
|
adamc@509
|
249 (case IM.find (namedE, n) of
|
adamc@509
|
250 NONE => all
|
adamc@509
|
251 | SOME e => e)
|
adamc@509
|
252 | ECon (dk, pc, cs, eo) => (ECon (dk, patCon pc,
|
adamc@509
|
253 map (con env) cs, Option.map (exp env) eo), loc)
|
adamc@509
|
254 | EFfi _ => all
|
adamc@509
|
255 | EFfiApp (m, f, es) => (EFfiApp (m, f, map (exp env) es), loc)
|
adamc@509
|
256
|
adamc@509
|
257 | EApp (e1, e2) =>
|
adamc@509
|
258 let
|
adamc@509
|
259 val e1 = exp env e1
|
adamc@509
|
260 val e2 = exp env e2
|
adamc@509
|
261 in
|
adamc@509
|
262 case #1 e1 of
|
adamc@510
|
263 EAbs (_, _, _, b) => exp (KnownE e2 :: deKnown env) b
|
adamc@509
|
264 | _ => (EApp (e1, e2), loc)
|
adamc@509
|
265 end
|
adamc@509
|
266
|
adamc@509
|
267 | EAbs (x, dom, ran, e) => (EAbs (x, con env dom, con env ran, exp (UnknownE :: env) e), loc)
|
adamc@509
|
268
|
adamc@509
|
269 | ECApp (e, c) =>
|
adamc@509
|
270 let
|
adamc@509
|
271 val e = exp env e
|
adamc@509
|
272 val c = con env c
|
adamc@509
|
273 in
|
adamc@509
|
274 case #1 e of
|
adamc@510
|
275 ECAbs (_, _, b) => exp (KnownC c :: deKnown env) b
|
adamc@509
|
276 | _ => (ECApp (e, c), loc)
|
adamc@509
|
277 end
|
adamc@509
|
278
|
adamc@626
|
279 | ECAbs (x, k, e) => (ECAbs (x, kind env k, exp (UnknownC :: env) e), loc)
|
adamc@626
|
280
|
adamc@626
|
281 | EKApp (e, k) =>
|
adamc@626
|
282 let
|
adamc@626
|
283 val e = exp env e
|
adamc@626
|
284 in
|
adamc@626
|
285 case #1 e of
|
adamc@626
|
286 EKAbs (_, b) => exp (KnownK k :: deKnown env) b
|
adamc@626
|
287 | _ => (EKApp (e, kind env k), loc)
|
adamc@626
|
288 end
|
adamc@626
|
289
|
adamc@626
|
290 | EKAbs (x, e) => (EKAbs (x, exp (UnknownK :: env) e), loc)
|
adamc@509
|
291
|
adamc@509
|
292 | ERecord xcs => (ERecord (map (fn (x, e, t) => (con env x, exp env e, con env t)) xcs), loc)
|
adamc@509
|
293 | EField (e, c, {field, rest}) =>
|
adamc@509
|
294 let
|
adamc@509
|
295 val e = exp env e
|
adamc@509
|
296 val c = con env c
|
adamc@509
|
297
|
adamc@509
|
298 fun default () = (EField (e, c, {field = con env field, rest = con env rest}), loc)
|
adamc@509
|
299 in
|
adamc@509
|
300 case (#1 e, #1 c) of
|
adamc@509
|
301 (ERecord xcs, CName x) =>
|
adamc@509
|
302 (case List.find (fn ((CName x', _), _, _) => x' = x | _ => false) xcs of
|
adamc@509
|
303 NONE => default ()
|
adamc@509
|
304 | SOME (_, e, _) => e)
|
adamc@509
|
305 | _ => default ()
|
adamc@509
|
306 end
|
adamc@509
|
307
|
adamc@509
|
308 | EConcat (e1, c1, e2, c2) =>
|
adamc@509
|
309 let
|
adamc@509
|
310 val e1 = exp env e1
|
adamc@509
|
311 val e2 = exp env e2
|
adamc@509
|
312 in
|
adamc@509
|
313 case (#1 e1, #1 e2) of
|
adamc@509
|
314 (ERecord xes1, ERecord xes2) => (ERecord (xes1 @ xes2), loc)
|
adamc@509
|
315 | _ =>
|
adamc@509
|
316 let
|
adamc@509
|
317 val c1 = con env c1
|
adamc@509
|
318 val c2 = con env c2
|
adamc@509
|
319 in
|
adamc@509
|
320 case (#1 c1, #1 c2) of
|
adamc@509
|
321 (CRecord (k, xcs1), CRecord (_, xcs2)) =>
|
adamc@509
|
322 let
|
adamc@509
|
323 val (xes1, rest) = ListUtil.foldlMap (doPart e1) [] xcs1
|
adamc@509
|
324 val (xes2, _) = ListUtil.foldlMap (doPart e2) rest xcs2
|
adamc@509
|
325 in
|
adamc@510
|
326 exp (deKnown env) (ERecord (xes1 @ xes2), loc)
|
adamc@509
|
327 end
|
adamc@509
|
328 | _ => (EConcat (e1, c1, e2, c2), loc)
|
adamc@509
|
329 end
|
adamc@509
|
330 end
|
adamc@509
|
331
|
adamc@509
|
332 | ECut (e, c, {field, rest}) =>
|
adamc@509
|
333 let
|
adamc@509
|
334 val e = exp env e
|
adamc@509
|
335 val c = con env c
|
adamc@509
|
336
|
adamc@509
|
337 fun default () =
|
adamc@509
|
338 let
|
adamc@509
|
339 val rest = con env rest
|
adamc@509
|
340 in
|
adamc@509
|
341 case #1 rest of
|
adamc@509
|
342 CRecord (k, xcs) =>
|
adamc@509
|
343 let
|
adamc@509
|
344 val (xes, _) = ListUtil.foldlMap (doPart e) [] xcs
|
adamc@509
|
345 in
|
adamc@510
|
346 exp (deKnown env) (ERecord xes, loc)
|
adamc@509
|
347 end
|
adamc@509
|
348 | _ => (ECut (e, c, {field = con env field, rest = rest}), loc)
|
adamc@509
|
349 end
|
adamc@509
|
350 in
|
adamc@509
|
351 case (#1 e, #1 c) of
|
adamc@509
|
352 (ERecord xes, CName x) =>
|
adamc@509
|
353 if List.all (fn ((CName _, _), _, _) => true | _ => false) xes then
|
adamc@509
|
354 (ERecord (List.filter (fn ((CName x', _), _, _) => x' <> x
|
adamc@509
|
355 | _ => raise Fail "Reduce: ECut") xes), loc)
|
adamc@509
|
356 else
|
adamc@509
|
357 default ()
|
adamc@509
|
358 | _ => default ()
|
adamc@509
|
359 end
|
adamc@509
|
360
|
adamc@509
|
361 | ECutMulti (e, c, {rest}) =>
|
adamc@509
|
362 let
|
adamc@509
|
363 val e = exp env e
|
adamc@509
|
364 val c = con env c
|
adamc@509
|
365
|
adamc@509
|
366 fun default () =
|
adamc@509
|
367 let
|
adamc@509
|
368 val rest = con env rest
|
adamc@509
|
369 in
|
adamc@509
|
370 case #1 rest of
|
adamc@509
|
371 CRecord (k, xcs) =>
|
adamc@509
|
372 let
|
adamc@509
|
373 val (xes, _) = ListUtil.foldlMap (doPart e) [] xcs
|
adamc@509
|
374 in
|
adamc@510
|
375 exp (deKnown env) (ERecord xes, loc)
|
adamc@509
|
376 end
|
adamc@509
|
377 | _ => (ECutMulti (e, c, {rest = rest}), loc)
|
adamc@509
|
378 end
|
adamc@509
|
379 in
|
adamc@509
|
380 case (#1 e, #1 c) of
|
adamc@509
|
381 (ERecord xes, CRecord (_, xcs)) =>
|
adamc@509
|
382 if List.all (fn ((CName _, _), _, _) => true | _ => false) xes
|
adamc@509
|
383 andalso List.all (fn ((CName _, _), _) => true | _ => false) xcs then
|
adamc@509
|
384 (ERecord (List.filter (fn ((CName x', _), _, _) =>
|
adamc@509
|
385 List.all (fn ((CName x, _), _) => x' <> x
|
adamc@509
|
386 | _ => raise Fail "Reduce: ECutMulti [1]") xcs
|
adamc@509
|
387 | _ => raise Fail "Reduce: ECutMulti [2]") xes), loc)
|
adamc@509
|
388 else
|
adamc@509
|
389 default ()
|
adamc@509
|
390 | _ => default ()
|
adamc@509
|
391 end
|
adamc@509
|
392
|
adamc@509
|
393 | ECase (e, pes, {disc, result}) =>
|
adamc@509
|
394 let
|
adamc@509
|
395 fun patBinds (p, _) =
|
adamc@509
|
396 case p of
|
adamc@509
|
397 PWild => 0
|
adamc@509
|
398 | PVar _ => 1
|
adamc@509
|
399 | PPrim _ => 0
|
adamc@509
|
400 | PCon (_, _, _, NONE) => 0
|
adamc@509
|
401 | PCon (_, _, _, SOME p) => patBinds p
|
adamc@509
|
402 | PRecord xpts => foldl (fn ((_, p, _), n) => n + patBinds p) 0 xpts
|
adamc@509
|
403
|
adamc@509
|
404 fun pat (all as (p, loc)) =
|
adamc@509
|
405 case p of
|
adamc@509
|
406 PWild => all
|
adamc@509
|
407 | PVar (x, t) => (PVar (x, con env t), loc)
|
adamc@509
|
408 | PPrim _ => all
|
adamc@509
|
409 | PCon (dk, pc, cs, po) =>
|
adamc@509
|
410 (PCon (dk, patCon pc, map (con env) cs, Option.map pat po), loc)
|
adamc@509
|
411 | PRecord xpts => (PRecord (map (fn (x, p, t) => (x, pat p, con env t)) xpts), loc)
|
adamc@509
|
412 in
|
adamc@509
|
413 (ECase (exp env e,
|
adamc@509
|
414 map (fn (p, e) => (pat p,
|
adamc@509
|
415 exp (List.tabulate (patBinds p, fn _ => UnknownE) @ env) e))
|
adamc@509
|
416 pes, {disc = con env disc, result = con env result}), loc)
|
adamc@509
|
417 end
|
adamc@509
|
418
|
adamc@509
|
419 | EWrite e => (EWrite (exp env e), loc)
|
adamc@509
|
420 | EClosure (n, es) => (EClosure (n, map (exp env) es), loc)
|
adamc@509
|
421
|
adamc@607
|
422 | ELet (x, t, e1, e2) => (ELet (x, con env t, exp env e1, exp (UnknownE :: env) e2), loc)
|
adamc@607
|
423
|
adamc@609
|
424 | EServerCall (n, es, e, t) => (EServerCall (n, map (exp env) es, exp env e, con env t), loc))
|
adamc@417
|
425 in
|
adamc@626
|
426 {kind = kind, con = con, exp = exp}
|
adamc@417
|
427 end
|
adamc@21
|
428
|
adamc@626
|
429 fun kind namedC env k = #kind (kindConAndExp (namedC, IM.empty)) env k
|
adamc@626
|
430 fun con namedC env c = #con (kindConAndExp (namedC, IM.empty)) env c
|
adamc@626
|
431 fun exp (namedC, namedE) env e = #exp (kindConAndExp (namedC, namedE)) env e
|
adamc@20
|
432
|
adamc@508
|
433 fun reduce file =
|
adamc@508
|
434 let
|
adamc@508
|
435 fun doDecl (d as (_, loc), st as (namedC, namedE)) =
|
adamc@508
|
436 case #1 d of
|
adamc@508
|
437 DCon (x, n, k, c) =>
|
adamc@508
|
438 let
|
adamc@626
|
439 val k = kind namedC [] k
|
adamc@509
|
440 val c = con namedC [] c
|
adamc@508
|
441 in
|
adamc@508
|
442 ((DCon (x, n, k, c), loc),
|
adamc@508
|
443 (IM.insert (namedC, n, c), namedE))
|
adamc@508
|
444 end
|
adamc@508
|
445 | DDatatype (x, n, ps, cs) =>
|
adamc@509
|
446 let
|
adamc@509
|
447 val env = map (fn _ => UnknownC) ps
|
adamc@509
|
448 in
|
adamc@509
|
449 ((DDatatype (x, n, ps, map (fn (x, n, co) => (x, n, Option.map (con namedC env) co)) cs), loc),
|
adamc@509
|
450 st)
|
adamc@509
|
451 end
|
adamc@508
|
452 | DVal (x, n, t, e, s) =>
|
adamc@508
|
453 let
|
adamc@509
|
454 val t = con namedC [] t
|
adamc@509
|
455 val e = exp (namedC, namedE) [] e
|
adamc@508
|
456 in
|
adamc@508
|
457 ((DVal (x, n, t, e, s), loc),
|
adamc@508
|
458 (namedC, IM.insert (namedE, n, e)))
|
adamc@508
|
459 end
|
adamc@508
|
460 | DValRec vis =>
|
adamc@509
|
461 ((DValRec (map (fn (x, n, t, e, s) => (x, n, con namedC [] t, exp (namedC, namedE) [] e, s)) vis), loc),
|
adamc@508
|
462 st)
|
adamc@508
|
463 | DExport _ => (d, st)
|
adamc@509
|
464 | DTable (s, n, c, s') => ((DTable (s, n, con namedC [] c, s'), loc), st)
|
adamc@508
|
465 | DSequence _ => (d, st)
|
adamc@508
|
466 | DDatabase _ => (d, st)
|
adamc@509
|
467 | DCookie (s, n, c, s') => ((DCookie (s, n, con namedC [] c, s'), loc), st)
|
adamc@20
|
468
|
adamc@508
|
469 val (file, _) = ListUtil.foldlMap doDecl (IM.empty, IM.empty) file
|
adamc@508
|
470 in
|
adamc@508
|
471 file
|
adamc@508
|
472 end
|
adamc@20
|
473
|
adamc@20
|
474 end
|