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@1016
|
34 structure IS = IntBinarySet
|
adamc@508
|
35 structure IM = IntBinaryMap
|
adamc@20
|
36
|
adamc@908
|
37 structure E = CoreEnv
|
adamc@908
|
38
|
adamc@908
|
39 fun multiLiftExpInExp n e =
|
adamc@908
|
40 if n = 0 then
|
adamc@908
|
41 e
|
adamc@908
|
42 else
|
adamc@908
|
43 multiLiftExpInExp (n - 1) (E.liftExpInExp 0 e)
|
adamc@908
|
44
|
adamc@909
|
45 val dangling =
|
adamc@909
|
46 CoreUtil.Exp.existsB {kind = fn _ => false,
|
adamc@909
|
47 con = fn _ => false,
|
adamc@909
|
48 exp = fn (n, e) =>
|
adamc@909
|
49 case e of
|
adamc@909
|
50 ERel n' => n' >= n
|
adamc@909
|
51 | _ => false,
|
adamc@909
|
52 bind = fn (n, b) =>
|
adamc@909
|
53 case b of
|
adamc@909
|
54 CoreUtil.Exp.RelE _ => n + 1
|
adamc@909
|
55 | _ => n}
|
adamc@909
|
56
|
adamc@508
|
57 datatype env_item =
|
adamc@626
|
58 UnknownK
|
adamc@626
|
59 | KnownK of kind
|
adamc@626
|
60
|
adamc@626
|
61 | UnknownC
|
adamc@508
|
62 | KnownC of con
|
adamc@21
|
63
|
adamc@508
|
64 | UnknownE
|
adamc@508
|
65 | KnownE of exp
|
adamc@20
|
66
|
adamc@626
|
67 | Lift of int * int * int
|
adamc@20
|
68
|
adamc@909
|
69 val edepth = foldl (fn (UnknownE, n) => n + 1
|
adamc@909
|
70 | (KnownE _, n) => n + 1
|
adamc@909
|
71 | (_, n) => n) 0
|
adamc@909
|
72
|
adamc@909
|
73 val edepth' = foldl (fn (UnknownE, n) => n + 1
|
adamc@909
|
74 | (KnownE _, n) => n + 1
|
adamc@909
|
75 | (Lift (_, _, n'), n) => n + n'
|
adamc@909
|
76 | (_, n) => n) 0
|
adamc@909
|
77
|
adamc@508
|
78 type env = env_item list
|
adamc@20
|
79
|
adamc@510
|
80 fun ei2s ei =
|
adamc@510
|
81 case ei of
|
adamc@626
|
82 UnknownK => "UK"
|
adamc@626
|
83 | KnownK _ => "KK"
|
adamc@626
|
84 | UnknownC => "UC"
|
adamc@510
|
85 | KnownC _ => "KC"
|
adamc@510
|
86 | UnknownE => "UE"
|
adamc@510
|
87 | KnownE _ => "KE"
|
adamc@626
|
88 | Lift (_, n1, n2) => "(" ^ Int.toString n1 ^ ", " ^ Int.toString n2 ^ ")"
|
adamc@510
|
89
|
adamc@510
|
90 fun e2s env = String.concatWith " " (map ei2s env)
|
adamc@510
|
91
|
adamc@909
|
92 (*val deKnown = List.filter (fn KnownC _ => false
|
adamc@510
|
93 | KnownE _ => false
|
adamc@626
|
94 | KnownK _ => false
|
adamc@909
|
95 | _ => true)*)
|
adamc@909
|
96
|
adamc@909
|
97 val deKnown = ListUtil.mapConcat (fn KnownC _ => []
|
adamc@909
|
98 | KnownE _ => []
|
adamc@909
|
99 | KnownK _ => []
|
adamc@909
|
100 | Lift (nk, nc, ne) => List.tabulate (nk, fn _ => UnknownK)
|
adamc@909
|
101 @ List.tabulate (nc, fn _ => UnknownC)
|
adamc@909
|
102 @ List.tabulate (ne, fn _ => UnknownE)
|
adamc@909
|
103 | x => [x])
|
adamc@510
|
104
|
adamc@930
|
105 datatype result = Yes of env | No | Maybe
|
adamc@930
|
106
|
adamc@930
|
107 fun match (env, p : pat, e : exp) =
|
adamc@942
|
108 let
|
adamc@942
|
109 val baseline = length env
|
adamc@930
|
110
|
adamc@942
|
111 fun match (env, p, e) =
|
adamc@942
|
112 case (#1 p, #1 e) of
|
adamc@942
|
113 (PWild, _) => Yes env
|
adamc@942
|
114 | (PVar (x, t), _) => Yes (KnownE (multiLiftExpInExp (length env - baseline) e) :: env)
|
adamc@930
|
115
|
adamc@942
|
116 | (PPrim p, EPrim p') =>
|
adamc@942
|
117 if Prim.equal (p, p') then
|
adamc@942
|
118 Yes env
|
adamc@942
|
119 else
|
adamc@942
|
120 No
|
adamc@930
|
121
|
adamc@942
|
122 | (PCon (_, PConVar n1, _, NONE), ECon (_, PConVar n2, _, NONE)) =>
|
adamc@942
|
123 if n1 = n2 then
|
adamc@942
|
124 Yes env
|
adamc@942
|
125 else
|
adamc@942
|
126 No
|
adamc@930
|
127
|
adamc@942
|
128 | (PCon (_, PConVar n1, _, SOME p), ECon (_, PConVar n2, _, SOME e)) =>
|
adamc@942
|
129 if n1 = n2 then
|
adamc@942
|
130 match (env, p, e)
|
adamc@942
|
131 else
|
adamc@942
|
132 No
|
adamc@930
|
133
|
adamc@942
|
134 | (PCon (_, PConFfi {mod = m1, con = con1, ...}, _, NONE),
|
adamc@942
|
135 ECon (_, PConFfi {mod = m2, con = con2, ...}, _, NONE)) =>
|
adamc@942
|
136 if m1 = m2 andalso con1 = con2 then
|
adamc@942
|
137 Yes env
|
adamc@942
|
138 else
|
adamc@942
|
139 No
|
adamc@930
|
140
|
adamc@942
|
141 | (PCon (_, PConFfi {mod = m1, con = con1, ...}, _, SOME ep),
|
adamc@942
|
142 ECon (_, PConFfi {mod = m2, con = con2, ...}, _, SOME e)) =>
|
adamc@942
|
143 if m1 = m2 andalso con1 = con2 then
|
adamc@942
|
144 match (env, p, e)
|
adamc@942
|
145 else
|
adamc@942
|
146 No
|
adamc@930
|
147
|
adamc@942
|
148 | (PRecord xps, ERecord xes) =>
|
adamc@942
|
149 if List.exists (fn ((CName _, _), _, _) => false
|
adamc@942
|
150 | _ => true) xes then
|
adamc@942
|
151 Maybe
|
adamc@942
|
152 else
|
adamc@942
|
153 let
|
adamc@942
|
154 fun consider (xps, env) =
|
adamc@942
|
155 case xps of
|
adamc@942
|
156 [] => Yes env
|
adamc@942
|
157 | (x, p, _) :: rest =>
|
adamc@942
|
158 case List.find (fn ((CName x', _), _, _) => x' = x
|
adamc@942
|
159 | _ => false) xes of
|
adamc@942
|
160 NONE => No
|
adamc@942
|
161 | SOME (_, e, _) =>
|
adamc@942
|
162 case match (env, p, e) of
|
adamc@942
|
163 No => No
|
adamc@942
|
164 | Maybe => Maybe
|
adamc@942
|
165 | Yes env => consider (rest, env)
|
adamc@942
|
166 in
|
adamc@942
|
167 consider (xps, env)
|
adamc@942
|
168 end
|
adamc@942
|
169
|
adamc@942
|
170 | _ => Maybe
|
adamc@942
|
171 in
|
adamc@942
|
172 match (env, p, e)
|
adamc@942
|
173 end
|
adamc@930
|
174
|
adamc@626
|
175 fun kindConAndExp (namedC, namedE) =
|
adamc@508
|
176 let
|
adamc@626
|
177 fun kind env (all as (k, loc)) =
|
adamc@626
|
178 case k of
|
adamc@626
|
179 KType => all
|
adamc@626
|
180 | KArrow (k1, k2) => (KArrow (kind env k1, kind env k2), loc)
|
adamc@626
|
181 | KName => all
|
adamc@626
|
182 | KRecord k => (KRecord (kind env k), loc)
|
adamc@626
|
183 | KUnit => all
|
adamc@626
|
184 | KTuple ks => (KTuple (map (kind env) ks), loc)
|
adamc@626
|
185
|
adamc@626
|
186 | KRel n =>
|
adamc@626
|
187 let
|
adamc@626
|
188 fun find (n', env, nudge, lift) =
|
adamc@626
|
189 case env of
|
adamc@626
|
190 [] => raise Fail "Reduce.kind: KRel"
|
adamc@626
|
191 | UnknownC :: rest => find (n', rest, nudge, lift)
|
adamc@626
|
192 | KnownC _ :: rest => find (n', rest, nudge, lift)
|
adamc@626
|
193 | UnknownE :: rest => find (n', rest, nudge, lift)
|
adamc@626
|
194 | KnownE _ :: rest => find (n', rest, nudge, lift)
|
adamc@626
|
195 | Lift (lift', _, _) :: rest => find (n', rest, nudge + lift', lift + lift')
|
adamc@626
|
196 | UnknownK :: rest =>
|
adamc@626
|
197 if n' = 0 then
|
adamc@626
|
198 (KRel (n + nudge), loc)
|
adamc@626
|
199 else
|
adamc@626
|
200 find (n' - 1, rest, nudge, lift + 1)
|
adamc@626
|
201 | KnownK k :: rest =>
|
adamc@626
|
202 if n' = 0 then
|
adamc@626
|
203 kind (Lift (lift, 0, 0) :: rest) k
|
adamc@626
|
204 else
|
adamc@626
|
205 find (n' - 1, rest, nudge - 1, lift)
|
adamc@626
|
206 in
|
adamc@626
|
207 find (n, env, 0, 0)
|
adamc@626
|
208 end
|
adamc@626
|
209 | KFun (x, k) => (KFun (x, kind (UnknownK :: env) k), loc)
|
adamc@626
|
210
|
adamc@508
|
211 fun con env (all as (c, loc)) =
|
adamc@510
|
212 ((*Print.prefaces "con" [("c", CorePrint.p_con CoreEnv.empty all)];*)
|
adamc@508
|
213 case c of
|
adamc@508
|
214 TFun (c1, c2) => (TFun (con env c1, con env c2), loc)
|
adamc@626
|
215 | TCFun (x, k, c2) => (TCFun (x, kind env k, con (UnknownC :: env) c2), loc)
|
adamc@626
|
216 | TKFun (x, c2) => (TKFun (x, con (UnknownK :: env) c2), loc)
|
adamc@508
|
217 | TRecord c => (TRecord (con env c), loc)
|
adamc@215
|
218
|
adamc@508
|
219 | CRel n =>
|
adamc@508
|
220 let
|
adamc@626
|
221 fun find (n', env, nudge, liftK, liftC) =
|
adamc@510
|
222 case env of
|
adamc@510
|
223 [] => raise Fail "Reduce.con: CRel"
|
adamc@626
|
224 | UnknownK :: rest => find (n', rest, nudge, liftK + 1, liftC)
|
adamc@626
|
225 | KnownK _ :: rest => find (n', rest, nudge, liftK, liftC)
|
adamc@626
|
226 | UnknownE :: rest => find (n', rest, nudge, liftK, liftC)
|
adamc@626
|
227 | KnownE _ :: rest => find (n', rest, nudge, liftK, liftC)
|
adamc@626
|
228 | Lift (liftK', liftC', _) :: rest => find (n', rest, nudge + liftC',
|
adamc@626
|
229 liftK + liftK', liftC + liftC')
|
adamc@510
|
230 | UnknownC :: rest =>
|
adamc@510
|
231 if n' = 0 then
|
adamc@510
|
232 (CRel (n + nudge), loc)
|
adamc@510
|
233 else
|
adamc@626
|
234 find (n' - 1, rest, nudge, liftK, liftC + 1)
|
adamc@510
|
235 | KnownC c :: rest =>
|
adamc@510
|
236 if n' = 0 then
|
adamc@626
|
237 con (Lift (liftK, liftC, 0) :: rest) c
|
adamc@510
|
238 else
|
adamc@626
|
239 find (n' - 1, rest, nudge - 1, liftK, liftC)
|
adamc@508
|
240 in
|
adamc@510
|
241 (*print (Int.toString n ^ ": " ^ e2s env ^ "\n");*)
|
adamc@626
|
242 find (n, env, 0, 0, 0)
|
adamc@508
|
243 end
|
adamc@508
|
244 | CNamed n =>
|
adamc@508
|
245 (case IM.find (namedC, n) of
|
adamc@508
|
246 NONE => all
|
adamc@508
|
247 | SOME c => c)
|
adamc@508
|
248 | CFfi _ => all
|
adamc@508
|
249 | CApp (c1, c2) =>
|
adamc@508
|
250 let
|
adamc@508
|
251 val c1 = con env c1
|
adamc@508
|
252 val c2 = con env c2
|
adamc@508
|
253 in
|
adamc@508
|
254 case #1 c1 of
|
adamc@508
|
255 CAbs (_, _, b) =>
|
adamc@510
|
256 con (KnownC c2 :: deKnown env) b
|
adamc@215
|
257
|
adamc@621
|
258 | CApp ((CMap (dom, ran), _), f) =>
|
adamc@508
|
259 (case #1 c2 of
|
adamc@626
|
260 CRecord (_, []) => (CRecord (kind env ran, []), loc)
|
adamc@621
|
261 | CRecord (_, (x, c) :: rest) =>
|
adamc@510
|
262 con (deKnown env)
|
adamc@621
|
263 (CConcat ((CRecord (ran, [(x, (CApp (f, c), loc))]), loc),
|
adamc@626
|
264 (CApp (c1, (CRecord (kind env dom, rest), loc)), loc)), loc)
|
adamc@508
|
265 | _ => (CApp (c1, c2), loc))
|
adamc@20
|
266
|
adamc@508
|
267 | _ => (CApp (c1, c2), loc)
|
adamc@508
|
268 end
|
adamc@626
|
269 | CAbs (x, k, b) => (CAbs (x, kind env k, con (UnknownC :: env) b), loc)
|
adamc@626
|
270
|
adamc@626
|
271 | CKApp (c1, k) =>
|
adamc@626
|
272 let
|
adamc@626
|
273 val c1 = con env c1
|
adamc@626
|
274 in
|
adamc@626
|
275 case #1 c1 of
|
adamc@626
|
276 CKAbs (_, b) =>
|
adamc@626
|
277 con (KnownK k :: deKnown env) b
|
adamc@626
|
278
|
adamc@626
|
279 | _ => (CKApp (c1, kind env k), loc)
|
adamc@626
|
280 end
|
adamc@626
|
281 | CKAbs (x, b) => (CKAbs (x, con (UnknownK :: env) b), loc)
|
adamc@20
|
282
|
adamc@508
|
283 | CName _ => all
|
adamc@21
|
284
|
adamc@626
|
285 | CRecord (k, xcs) => (CRecord (kind env k, map (fn (x, c) => (con env x, con env c)) xcs), loc)
|
adamc@508
|
286 | CConcat (c1, c2) =>
|
adamc@508
|
287 let
|
adamc@508
|
288 val c1 = con env c1
|
adamc@508
|
289 val c2 = con env c2
|
adamc@508
|
290 in
|
adamc@508
|
291 case (#1 c1, #1 c2) of
|
adamc@508
|
292 (CRecord (k, xcs1), CRecord (_, xcs2)) =>
|
adamc@626
|
293 (CRecord (kind env k, xcs1 @ xcs2), loc)
|
adamc@508
|
294 | _ => (CConcat (c1, c2), loc)
|
adamc@508
|
295 end
|
adamc@626
|
296 | CMap (dom, ran) => (CMap (kind env dom, kind env ran), loc)
|
adamc@74
|
297
|
adamc@508
|
298 | CUnit => all
|
adamc@21
|
299
|
adamc@508
|
300 | CTuple cs => (CTuple (map (con env) cs), loc)
|
adamc@508
|
301 | CProj (c, n) =>
|
adamc@508
|
302 let
|
adamc@508
|
303 val c = con env c
|
adamc@508
|
304 in
|
adamc@508
|
305 case #1 c of
|
adamc@508
|
306 CTuple cs => List.nth (cs, n - 1)
|
adamc@508
|
307 | _ => (CProj (c, n), loc)
|
adamc@510
|
308 end)
|
adamc@22
|
309
|
adamc@509
|
310 fun patCon pc =
|
adamc@509
|
311 case pc of
|
adamc@509
|
312 PConVar _ => pc
|
adamc@509
|
313 | PConFfi {mod = m, datatyp, params, con = c, arg, kind} =>
|
adamc@509
|
314 PConFfi {mod = m, datatyp = datatyp, params = params, con = c,
|
adamc@509
|
315 arg = Option.map (con (map (fn _ => UnknownC) params)) arg,
|
adamc@509
|
316 kind = kind}
|
adamc@509
|
317
|
adamc@509
|
318
|
adamc@509
|
319 val k = (KType, ErrorMsg.dummySpan)
|
adamc@509
|
320 fun doPart e (this as (x, t), rest) =
|
adamc@509
|
321 ((x, (EField (e, x, {field = t, rest = (CRecord (k, rest), #2 t)}), #2 t), t),
|
adamc@509
|
322 this :: rest)
|
adamc@509
|
323
|
adamc@509
|
324 fun exp env (all as (e, loc)) =
|
adamc@909
|
325 let
|
adamc@909
|
326 (*val () = Print.prefaces "exp" [("e", CorePrint.p_exp CoreEnv.empty all),
|
adamc@909
|
327 ("env", Print.PD.string (e2s env))]*)
|
adamc@910
|
328 val () = if dangling (edepth env) all then
|
adamc@909
|
329 (Print.prefaces "exp" [("e", CorePrint.p_exp CoreEnv.empty all),
|
adamc@909
|
330 ("env", Print.PD.string (e2s env))];
|
adamc@909
|
331 raise Fail "!")
|
adamc@909
|
332 else
|
adamc@910
|
333 ()
|
adamc@509
|
334
|
adamc@909
|
335 val r = case e of
|
adamc@909
|
336 EPrim _ => all
|
adamc@909
|
337 | ERel n =>
|
adamc@909
|
338 let
|
adamc@909
|
339 fun find (n', env, nudge, liftK, liftC, liftE) =
|
adamc@909
|
340 case env of
|
adamc@909
|
341 [] => raise Fail ("Reduce.exp: ERel (" ^ ErrorMsg.spanToString loc ^ ")")
|
adamc@909
|
342 | UnknownK :: rest => find (n', rest, nudge, liftK + 1, liftC, liftE)
|
adamc@909
|
343 | KnownK _ :: rest => find (n', rest, nudge, liftK, liftC, liftE)
|
adamc@909
|
344 | UnknownC :: rest => find (n', rest, nudge, liftK, liftC + 1, liftE)
|
adamc@909
|
345 | KnownC _ :: rest => find (n', rest, nudge, liftK, liftC, liftE)
|
adamc@909
|
346 | Lift (liftK', liftC', liftE') :: rest =>
|
adamc@909
|
347 find (n', rest, nudge + liftE',
|
adamc@909
|
348 liftK + liftK', liftC + liftC', liftE + liftE')
|
adamc@909
|
349 | UnknownE :: rest =>
|
adamc@909
|
350 if n' = 0 then
|
adamc@909
|
351 (ERel (n + nudge), loc)
|
adamc@909
|
352 else
|
adamc@909
|
353 find (n' - 1, rest, nudge, liftK, liftC, liftE + 1)
|
adamc@909
|
354 | KnownE e :: rest =>
|
adamc@909
|
355 if n' = 0 then
|
adamc@909
|
356 ((*print "SUBSTITUTING\n";*)
|
adamc@909
|
357 exp (Lift (liftK, liftC, liftE) :: rest) e)
|
adamc@909
|
358 else
|
adamc@909
|
359 find (n' - 1, rest, nudge - 1, liftK, liftC, liftE)
|
adamc@909
|
360 in
|
adamc@909
|
361 (*print (Int.toString n ^ ": " ^ e2s env ^ "\n");*)
|
adamc@909
|
362 find (n, env, 0, 0, 0, 0)
|
adamc@909
|
363 end
|
adamc@909
|
364 | ENamed n =>
|
adamc@909
|
365 (case IM.find (namedE, n) of
|
adamc@909
|
366 NONE => all
|
adamc@909
|
367 | SOME e => e)
|
adamc@909
|
368 | ECon (dk, pc, cs, eo) => (ECon (dk, patCon pc,
|
adamc@909
|
369 map (con env) cs, Option.map (exp env) eo), loc)
|
adamc@909
|
370 | EFfi _ => all
|
adamc@909
|
371 | EFfiApp (m, f, es) => (EFfiApp (m, f, map (exp env) es), loc)
|
adamc@908
|
372
|
adamc@909
|
373 (*| EApp (
|
adamc@909
|
374 (EApp
|
adamc@909
|
375 ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), loc), _), _), t1), _), t2), _),
|
adamc@909
|
376 (EFfi ("Basis", "transaction_monad"), _)), _),
|
adamc@909
|
377 (ECase (ed, pes, {disc, ...}), _)), _),
|
adamc@909
|
378 trans2) =>
|
adamc@909
|
379 let
|
adamc@909
|
380 val e' = (EFfi ("Basis", "bind"), loc)
|
adamc@909
|
381 val e' = (ECApp (e', (CFfi ("Basis", "transaction"), loc)), loc)
|
adamc@909
|
382 val e' = (ECApp (e', t1), loc)
|
adamc@909
|
383 val e' = (ECApp (e', t2), loc)
|
adamc@909
|
384 val e' = (EApp (e', (EFfi ("Basis", "transaction_monad"), loc)), loc)
|
adamc@908
|
385
|
adamc@909
|
386 val pes = map (fn (p, e) =>
|
adamc@909
|
387 let
|
adamc@909
|
388 val e' = (EApp (e', e), loc)
|
adamc@909
|
389 val e' = (EApp (e',
|
adamc@909
|
390 multiLiftExpInExp (E.patBindsN p)
|
adamc@909
|
391 trans2), loc)
|
adamc@909
|
392 val e' = exp env e'
|
adamc@909
|
393 in
|
adamc@909
|
394 (p, e')
|
adamc@909
|
395 end) pes
|
adamc@909
|
396 in
|
adamc@909
|
397 (ECase (exp env ed,
|
adamc@909
|
398 pes,
|
adamc@909
|
399 {disc = con env disc,
|
adamc@909
|
400 result = (CApp ((CFfi ("Basis", "transaction"), loc), con env t2), loc)}),
|
adamc@909
|
401 loc)
|
adamc@909
|
402 end*)
|
adamc@908
|
403
|
adamc@909
|
404 | EApp (e1, e2) =>
|
adamc@909
|
405 let
|
adamc@910
|
406 val env' = deKnown env
|
adamc@910
|
407
|
adamc@910
|
408 fun reassoc e =
|
adamc@910
|
409 case #1 e of
|
adamc@910
|
410 EApp
|
adamc@910
|
411 ((EApp
|
adamc@910
|
412 ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), loc), _), _),
|
adamc@910
|
413 t1),
|
adamc@910
|
414 _), t2), _),
|
adamc@910
|
415 (EFfi ("Basis", "transaction_monad"), _)), _),
|
adamc@910
|
416 (EServerCall (n, es, (EAbs (_, _, _, ke), _), dom, ran), _)), _),
|
adamc@910
|
417 trans3) =>
|
adamc@910
|
418 let
|
adamc@910
|
419 val e' = (EFfi ("Basis", "bind"), loc)
|
adamc@910
|
420 val e' = (ECApp (e', (CFfi ("Basis", "transaction"), loc)), loc)
|
adamc@910
|
421 val e' = (ECApp (e', dom), loc)
|
adamc@910
|
422 val e' = (ECApp (e', t2), loc)
|
adamc@910
|
423 val e' = (EApp (e', (EFfi ("Basis", "transaction_monad"), loc)), loc)
|
adamc@910
|
424 val e' = (EApp (e', ke), loc)
|
adamc@910
|
425 val e' = (EApp (e', E.liftExpInExp 0 trans3), loc)
|
adamc@910
|
426 val e' = reassoc e'
|
adamc@910
|
427 val e' = (EAbs ("x", dom, t2, e'), loc)
|
adamc@910
|
428 val e' = (EServerCall (n, es, e', dom, t2), loc)
|
adamc@910
|
429 in
|
adamc@910
|
430 e'
|
adamc@910
|
431 end
|
adamc@910
|
432
|
adamc@910
|
433 | EApp
|
adamc@910
|
434 ((EApp
|
adamc@910
|
435 ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), loc), _), _),
|
adamc@910
|
436 t1),
|
adamc@910
|
437 _), t2), _),
|
adamc@910
|
438 (EFfi ("Basis", "transaction_monad"), _)), _),
|
adamc@910
|
439 (EServerCall (n, es, ke, dom, ran), _)), _),
|
adamc@910
|
440 trans3) =>
|
adamc@910
|
441 let
|
adamc@910
|
442 val e' = (EFfi ("Basis", "bind"), loc)
|
adamc@910
|
443 val e' = (ECApp (e', (CFfi ("Basis", "transaction"), loc)), loc)
|
adamc@910
|
444 val e' = (ECApp (e', dom), loc)
|
adamc@910
|
445 val e' = (ECApp (e', t2), loc)
|
adamc@910
|
446 val e' = (EApp (e', (EFfi ("Basis", "transaction_monad"), loc)), loc)
|
adamc@910
|
447 val e' = (EApp (e', exp (UnknownE :: env')
|
adamc@910
|
448 (EApp (E.liftExpInExp 0 ke, (ERel 0, loc)), loc)),
|
adamc@910
|
449 loc)
|
adamc@910
|
450 val e' = (EApp (e', E.liftExpInExp 0 trans3), loc)
|
adamc@910
|
451 val e' = reassoc e'
|
adamc@910
|
452 val e' = (EAbs ("x", dom, t2, e'), loc)
|
adamc@910
|
453 val e' = (EServerCall (n, es, e', dom, t2), loc)
|
adamc@910
|
454 in
|
adamc@910
|
455 e'
|
adamc@910
|
456 end
|
adamc@910
|
457
|
adamc@910
|
458 | EApp
|
adamc@910
|
459 ((EApp
|
adamc@955
|
460 ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), loc), _), _),
|
adamc@955
|
461 t1),
|
adamc@955
|
462 _), t2), _),
|
adamc@955
|
463 (EFfi ("Basis", "transaction_monad"), _)), _),
|
adamc@955
|
464 (ETailCall (n, es, (EAbs (_, _, _, ke), _), dom, ran), _)), _),
|
adamc@955
|
465 trans3) =>
|
adamc@955
|
466 let
|
adamc@955
|
467 val e' = (EFfi ("Basis", "bind"), loc)
|
adamc@955
|
468 val e' = (ECApp (e', (CFfi ("Basis", "transaction"), loc)), loc)
|
adamc@955
|
469 val e' = (ECApp (e', dom), loc)
|
adamc@955
|
470 val e' = (ECApp (e', t2), loc)
|
adamc@955
|
471 val e' = (EApp (e', (EFfi ("Basis", "transaction_monad"), loc)), loc)
|
adamc@955
|
472 val e' = (EApp (e', ke), loc)
|
adamc@955
|
473 val e' = (EApp (e', E.liftExpInExp 0 trans3), loc)
|
adamc@955
|
474 val e' = reassoc e'
|
adamc@955
|
475 val e' = (EAbs ("x", dom, t2, e'), loc)
|
adamc@955
|
476 val e' = (ETailCall (n, es, e', dom, t2), loc)
|
adamc@955
|
477 in
|
adamc@955
|
478 e'
|
adamc@955
|
479 end
|
adamc@955
|
480
|
adamc@955
|
481 | EApp
|
adamc@955
|
482 ((EApp
|
adamc@955
|
483 ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), loc), _), _),
|
adamc@955
|
484 t1),
|
adamc@955
|
485 _), t2), _),
|
adamc@955
|
486 (EFfi ("Basis", "transaction_monad"), _)), _),
|
adamc@955
|
487 (ETailCall (n, es, ke, dom, ran), _)), _),
|
adamc@955
|
488 trans3) =>
|
adamc@955
|
489 let
|
adamc@955
|
490 val e' = (EFfi ("Basis", "bind"), loc)
|
adamc@955
|
491 val e' = (ECApp (e', (CFfi ("Basis", "transaction"), loc)), loc)
|
adamc@955
|
492 val e' = (ECApp (e', dom), loc)
|
adamc@955
|
493 val e' = (ECApp (e', t2), loc)
|
adamc@955
|
494 val e' = (EApp (e', (EFfi ("Basis", "transaction_monad"), loc)), loc)
|
adamc@955
|
495 val e' = (EApp (e', exp (UnknownE :: env')
|
adamc@955
|
496 (EApp (E.liftExpInExp 0 ke, (ERel 0, loc)), loc)),
|
adamc@955
|
497 loc)
|
adamc@955
|
498 val e' = (EApp (e', E.liftExpInExp 0 trans3), loc)
|
adamc@955
|
499 val e' = reassoc e'
|
adamc@955
|
500 val e' = (EAbs ("x", dom, t2, e'), loc)
|
adamc@955
|
501 val e' = (ETailCall (n, es, e', dom, t2), loc)
|
adamc@955
|
502 in
|
adamc@955
|
503 e'
|
adamc@955
|
504 end
|
adamc@955
|
505
|
adamc@955
|
506 | EApp
|
adamc@955
|
507 ((EApp
|
adamc@910
|
508 ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), loc), mt),
|
adamc@910
|
509 _), _), _), t3), _),
|
adamc@910
|
510 me), _),
|
adamc@910
|
511 (EApp ((EApp
|
adamc@910
|
512 ((EApp ((ECApp ((ECApp ((ECApp (
|
adamc@910
|
513 (EFfi ("Basis", "bind"), _), _), _),
|
adamc@910
|
514 t1), _), t2), _),
|
adamc@910
|
515 _), _),
|
adamc@910
|
516 trans1), _), (EAbs (_, _, _, trans2), _)), _)), _),
|
adamc@910
|
517 trans3) =>
|
adamc@910
|
518 let
|
adamc@910
|
519 val e'' = (EFfi ("Basis", "bind"), loc)
|
adamc@910
|
520 val e'' = (ECApp (e'', mt), loc)
|
adamc@910
|
521 val e'' = (ECApp (e'', t2), loc)
|
adamc@910
|
522 val e'' = (ECApp (e'', t3), loc)
|
adamc@910
|
523 val e'' = (EApp (e'', me), loc)
|
adamc@910
|
524 val e'' = (EApp (e'', trans2), loc)
|
adamc@910
|
525 val e'' = (EApp (e'', E.liftExpInExp 0 trans3), loc)
|
adamc@910
|
526 val e'' = reassoc e''
|
adamc@910
|
527 val e'' = (EAbs ("xb", t1, (CApp (mt, t3), loc), e''), loc)
|
adamc@910
|
528
|
adamc@910
|
529 val e' = (EFfi ("Basis", "bind"), loc)
|
adamc@910
|
530 val e' = (ECApp (e', mt), loc)
|
adamc@910
|
531 val e' = (ECApp (e', t1), loc)
|
adamc@910
|
532 val e' = (ECApp (e', t3), loc)
|
adamc@910
|
533 val e' = (EApp (e', me), loc)
|
adamc@910
|
534 val e' = (EApp (e', trans1), loc)
|
adamc@910
|
535 val e' = (EApp (e', e''), loc)
|
adamc@910
|
536 in
|
adamc@910
|
537 e'
|
adamc@910
|
538 end
|
adamc@910
|
539
|
adamc@910
|
540 | EApp
|
adamc@910
|
541 ((EApp
|
adamc@910
|
542 ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), loc), mt),
|
adamc@910
|
543 _), _), _), t3), _),
|
adamc@910
|
544 me), _),
|
adamc@910
|
545 (EApp ((EApp
|
adamc@910
|
546 ((EApp ((ECApp ((ECApp ((ECApp (
|
adamc@910
|
547 (EFfi ("Basis", "bind"), _), _), _),
|
adamc@910
|
548 t1), _), t2), _),
|
adamc@910
|
549 _), _),
|
adamc@910
|
550 trans1), _), trans2), _)), _),
|
adamc@910
|
551 trans3) =>
|
adamc@910
|
552 let
|
adamc@910
|
553 val e'' = (EFfi ("Basis", "bind"), loc)
|
adamc@910
|
554 val e'' = (ECApp (e'', mt), loc)
|
adamc@910
|
555 val e'' = (ECApp (e'', t2), loc)
|
adamc@910
|
556 val e'' = (ECApp (e'', t3), loc)
|
adamc@910
|
557 val e'' = (EApp (e'', me), loc)
|
adamc@910
|
558 val () = print "In2\n"
|
adamc@910
|
559 val e'' = (EApp (e'', exp (UnknownE :: env')
|
adamc@910
|
560 (EApp (E.liftExpInExp 0 trans2, (ERel 0, loc)),
|
adamc@910
|
561 loc)),
|
adamc@910
|
562 loc)
|
adamc@910
|
563 val () = print "Out2\n"
|
adamc@910
|
564 val e'' = (EApp (e'', E.liftExpInExp 0 trans3), loc)
|
adamc@910
|
565 val e'' = reassoc e''
|
adamc@910
|
566 val e'' = (EAbs ("xb", t1, (CApp (mt, t3), loc), e''), loc)
|
adamc@910
|
567
|
adamc@910
|
568 val e' = (EFfi ("Basis", "bind"), loc)
|
adamc@910
|
569 val e' = (ECApp (e', mt), loc)
|
adamc@910
|
570 val e' = (ECApp (e', t1), loc)
|
adamc@910
|
571 val e' = (ECApp (e', t3), loc)
|
adamc@910
|
572 val e' = (EApp (e', me), loc)
|
adamc@910
|
573 val e' = (EApp (e', trans1), loc)
|
adamc@910
|
574 val e' = (EApp (e', e''), loc)
|
adamc@910
|
575 in
|
adamc@910
|
576 e'
|
adamc@910
|
577 end
|
adamc@910
|
578
|
adamc@931
|
579 | EApp
|
adamc@931
|
580 ((EApp
|
adamc@931
|
581 ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), loc), _), _),
|
adamc@931
|
582 t1),
|
adamc@931
|
583 _), t2), _),
|
adamc@931
|
584 (EFfi ("Basis", "transaction_monad"), _)), _),
|
adamc@931
|
585 (ECase (e, pes, {disc, ...}), _)), _), trans) =>
|
adamc@931
|
586 let
|
adamc@931
|
587 val e' = (EFfi ("Basis", "bind"), loc)
|
adamc@931
|
588 val e' = (ECApp (e', (CFfi ("Basis", "transaction"), loc)), loc)
|
adamc@931
|
589 val e' = (ECApp (e', t1), loc)
|
adamc@931
|
590 val e' = (ECApp (e', t2), loc)
|
adamc@931
|
591 val e' = (EApp (e', (EFfi ("Basis", "transaction_monad"), loc)), loc)
|
adamc@931
|
592
|
adamc@931
|
593 fun doCase (p, e) =
|
adamc@931
|
594 let
|
adamc@931
|
595 val e' = (EApp (e', e), loc)
|
adamc@931
|
596 val e' = (EApp (e',
|
adamc@931
|
597 multiLiftExpInExp (E.patBindsN p)
|
adamc@931
|
598 trans), loc)
|
adamc@931
|
599 in
|
adamc@931
|
600 (p, reassoc e')
|
adamc@931
|
601 end
|
adamc@931
|
602 in
|
adamc@931
|
603 (ECase (e, map doCase pes,
|
adamc@931
|
604 {disc = disc,
|
adamc@931
|
605 result = (CApp ((CFfi ("Basis", "transaction"), loc),
|
adamc@931
|
606 t2), loc)}), loc)
|
adamc@931
|
607 end
|
adamc@931
|
608
|
adamc@910
|
609 | _ => e
|
adamc@910
|
610
|
adamc@909
|
611 val e1 = exp env e1
|
adamc@909
|
612 val e2 = exp env e2
|
adamc@910
|
613 val e12 = reassoc (EApp (e1, e2), loc)
|
adamc@909
|
614 in
|
adamc@910
|
615 case #1 e12 of
|
adamc@910
|
616 EApp ((EAbs (_, _, _, b), _), e2) =>
|
adamc@931
|
617 exp (KnownE e2 :: env') b
|
adamc@910
|
618 | _ => e12
|
adamc@909
|
619 end
|
adamc@509
|
620
|
adamc@909
|
621 | EAbs (x, dom, ran, e) => (EAbs (x, con env dom, con env ran, exp (UnknownE :: env) e), loc)
|
adamc@509
|
622
|
adamc@909
|
623 | ECApp (e, c) =>
|
adamc@909
|
624 let
|
adamc@909
|
625 val e = exp env e
|
adamc@909
|
626 val c = con env c
|
adamc@909
|
627 in
|
adamc@909
|
628 case #1 e of
|
adamc@909
|
629 ECAbs (_, _, b) => exp (KnownC c :: deKnown env) b
|
adamc@909
|
630 | _ => (ECApp (e, c), loc)
|
adamc@909
|
631 end
|
adamc@626
|
632
|
adamc@909
|
633 | ECAbs (x, k, e) => (ECAbs (x, kind env k, exp (UnknownC :: env) e), loc)
|
adamc@626
|
634
|
adamc@909
|
635 | EKApp (e, k) =>
|
adamc@909
|
636 let
|
adamc@909
|
637 val e = exp env e
|
adamc@909
|
638 in
|
adamc@909
|
639 case #1 e of
|
adamc@909
|
640 EKAbs (_, b) => exp (KnownK k :: deKnown env) b
|
adamc@909
|
641 | _ => (EKApp (e, kind env k), loc)
|
adamc@909
|
642 end
|
adamc@509
|
643
|
adamc@909
|
644 | EKAbs (x, e) => (EKAbs (x, exp (UnknownK :: env) e), loc)
|
adamc@509
|
645
|
adamc@909
|
646 | ERecord xcs => (ERecord (map (fn (x, e, t) => (con env x, exp env e, con env t)) xcs), loc)
|
adamc@909
|
647 | EField (e, c, {field, rest}) =>
|
adamc@909
|
648 let
|
adamc@909
|
649 val e = exp env e
|
adamc@909
|
650 val c = con env c
|
adamc@509
|
651
|
adamc@909
|
652 fun default () = (EField (e, c, {field = con env field, rest = con env rest}), loc)
|
adamc@909
|
653 in
|
adamc@909
|
654 case (#1 e, #1 c) of
|
adamc@909
|
655 (ERecord xcs, CName x) =>
|
adamc@909
|
656 (case List.find (fn ((CName x', _), _, _) => x' = x | _ => false) xcs of
|
adamc@909
|
657 NONE => default ()
|
adamc@909
|
658 | SOME (_, e, _) => e)
|
adamc@909
|
659 | _ => default ()
|
adamc@909
|
660 end
|
adamc@509
|
661
|
adamc@909
|
662 | EConcat (e1, c1, e2, c2) =>
|
adamc@909
|
663 let
|
adamc@909
|
664 val e1 = exp env e1
|
adamc@909
|
665 val e2 = exp env e2
|
adamc@909
|
666 in
|
adamc@909
|
667 case (#1 e1, #1 e2) of
|
adamc@909
|
668 (ERecord xes1, ERecord xes2) => (ERecord (xes1 @ xes2), loc)
|
adamc@909
|
669 | _ =>
|
adamc@909
|
670 let
|
adamc@909
|
671 val c1 = con env c1
|
adamc@909
|
672 val c2 = con env c2
|
adamc@909
|
673 in
|
adamc@909
|
674 case (#1 c1, #1 c2) of
|
adamc@909
|
675 (CRecord (k, xcs1), CRecord (_, xcs2)) =>
|
adamc@909
|
676 let
|
adamc@909
|
677 val (xes1, rest) = ListUtil.foldlMap (doPart e1) [] xcs1
|
adamc@909
|
678 val (xes2, _) = ListUtil.foldlMap (doPart e2) rest xcs2
|
adamc@909
|
679 in
|
adamc@909
|
680 exp (deKnown env) (ERecord (xes1 @ xes2), loc)
|
adamc@909
|
681 end
|
adamc@909
|
682 | _ => (EConcat (e1, c1, e2, c2), loc)
|
adamc@909
|
683 end
|
adamc@909
|
684 end
|
adamc@509
|
685
|
adamc@909
|
686 | ECut (e, c, {field, rest}) =>
|
adamc@909
|
687 let
|
adamc@909
|
688 val e = exp env e
|
adamc@909
|
689 val c = con env c
|
adamc@509
|
690
|
adamc@909
|
691 fun default () =
|
adamc@909
|
692 let
|
adamc@909
|
693 val rest = con env rest
|
adamc@909
|
694 in
|
adamc@909
|
695 case #1 rest of
|
adamc@909
|
696 CRecord (k, xcs) =>
|
adamc@909
|
697 let
|
adamc@909
|
698 val (xes, _) = ListUtil.foldlMap (doPart e) [] xcs
|
adamc@909
|
699 in
|
adamc@909
|
700 exp (deKnown env) (ERecord xes, loc)
|
adamc@909
|
701 end
|
adamc@909
|
702 | _ => (ECut (e, c, {field = con env field, rest = rest}), loc)
|
adamc@909
|
703 end
|
adamc@909
|
704 in
|
adamc@909
|
705 case (#1 e, #1 c) of
|
adamc@909
|
706 (ERecord xes, CName x) =>
|
adamc@909
|
707 if List.all (fn ((CName _, _), _, _) => true | _ => false) xes then
|
adamc@909
|
708 (ERecord (List.filter (fn ((CName x', _), _, _) => x' <> x
|
adamc@909
|
709 | _ => raise Fail "Reduce: ECut") xes), loc)
|
adamc@909
|
710 else
|
adamc@909
|
711 default ()
|
adamc@909
|
712 | _ => default ()
|
adamc@909
|
713 end
|
adamc@509
|
714
|
adamc@909
|
715 | ECutMulti (e, c, {rest}) =>
|
adamc@909
|
716 let
|
adamc@909
|
717 val e = exp env e
|
adamc@909
|
718 val c = con env c
|
adamc@509
|
719
|
adamc@909
|
720 fun default () =
|
adamc@909
|
721 let
|
adamc@909
|
722 val rest = con env rest
|
adamc@909
|
723 in
|
adamc@909
|
724 case #1 rest of
|
adamc@909
|
725 CRecord (k, xcs) =>
|
adamc@909
|
726 let
|
adamc@909
|
727 val (xes, _) = ListUtil.foldlMap (doPart e) [] xcs
|
adamc@909
|
728 in
|
adamc@909
|
729 exp (deKnown env) (ERecord xes, loc)
|
adamc@909
|
730 end
|
adamc@909
|
731 | _ => (ECutMulti (e, c, {rest = rest}), loc)
|
adamc@909
|
732 end
|
adamc@909
|
733 in
|
adamc@909
|
734 case (#1 e, #1 c) of
|
adamc@909
|
735 (ERecord xes, CRecord (_, xcs)) =>
|
adamc@909
|
736 if List.all (fn ((CName _, _), _, _) => true | _ => false) xes
|
adamc@909
|
737 andalso List.all (fn ((CName _, _), _) => true | _ => false) xcs then
|
adamc@909
|
738 (ERecord (List.filter (fn ((CName x', _), _, _) =>
|
adamc@909
|
739 List.all (fn ((CName x, _), _) => x' <> x
|
adamc@909
|
740 | _ => raise Fail "Reduce: ECutMulti [1]") xcs
|
adamc@909
|
741 | _ => raise Fail "Reduce: ECutMulti [2]") xes), loc)
|
adamc@909
|
742 else
|
adamc@909
|
743 default ()
|
adamc@909
|
744 | _ => default ()
|
adamc@909
|
745 end
|
adamc@823
|
746
|
adamc@909
|
747 | ECase (_, [((PRecord [], _), e)], _) => exp env e
|
adamc@909
|
748 | ECase (_, [((PWild, _), e)], _) => exp env e
|
adamc@509
|
749
|
adamc@909
|
750 | ECase (e, pes, {disc, result}) =>
|
adamc@909
|
751 let
|
adamc@909
|
752 fun patBinds (p, _) =
|
adamc@909
|
753 case p of
|
adamc@909
|
754 PWild => 0
|
adamc@909
|
755 | PVar _ => 1
|
adamc@909
|
756 | PPrim _ => 0
|
adamc@909
|
757 | PCon (_, _, _, NONE) => 0
|
adamc@909
|
758 | PCon (_, _, _, SOME p) => patBinds p
|
adamc@909
|
759 | PRecord xpts => foldl (fn ((_, p, _), n) => n + patBinds p) 0 xpts
|
adamc@509
|
760
|
adamc@909
|
761 fun pat (all as (p, loc)) =
|
adamc@909
|
762 case p of
|
adamc@909
|
763 PWild => all
|
adamc@909
|
764 | PVar (x, t) => (PVar (x, con env t), loc)
|
adamc@909
|
765 | PPrim _ => all
|
adamc@909
|
766 | PCon (dk, pc, cs, po) =>
|
adamc@909
|
767 (PCon (dk, patCon pc, map (con env) cs, Option.map pat po), loc)
|
adamc@909
|
768 | PRecord xpts => (PRecord (map (fn (x, p, t) => (x, pat p, con env t)) xpts), loc)
|
adamc@930
|
769
|
adamc@930
|
770 fun push () =
|
adamc@930
|
771 (ECase (exp env e,
|
adamc@930
|
772 map (fn (p, e) => (pat p,
|
adamc@930
|
773 exp (List.tabulate (patBinds p,
|
adamc@930
|
774 fn _ => UnknownE) @ env) e))
|
adamc@930
|
775 pes, {disc = con env disc, result = con env result}), loc)
|
adamc@930
|
776
|
adamc@930
|
777 fun search pes =
|
adamc@930
|
778 case pes of
|
adamc@930
|
779 [] => push ()
|
adamc@930
|
780 | (p, body) :: pes =>
|
adamc@930
|
781 case match (env, p, e) of
|
adamc@930
|
782 No => search pes
|
adamc@930
|
783 | Maybe => push ()
|
adamc@930
|
784 | Yes env' => exp env' body
|
adamc@909
|
785 in
|
adamc@930
|
786 search pes
|
adamc@909
|
787 end
|
adamc@509
|
788
|
adamc@909
|
789 | EWrite e => (EWrite (exp env e), loc)
|
adamc@909
|
790 | EClosure (n, es) => (EClosure (n, map (exp env) es), loc)
|
adamc@607
|
791
|
adamc@910
|
792 | ELet (x, t, e1, e2) =>
|
adamc@910
|
793 (ELet (x, con env t, exp env e1, exp (UnknownE :: env) e2), loc)
|
adamc@909
|
794
|
adamc@909
|
795 | EServerCall (n, es, e, t1, t2) => (EServerCall (n, map (exp env) es, exp env e,
|
adamc@909
|
796 con env t1, con env t2), loc)
|
adamc@954
|
797 | ETailCall (n, es, e, t1, t2) => (ETailCall (n, map (exp env) es, exp env e,
|
adamc@954
|
798 con env t1, con env t2), loc)
|
adamc@909
|
799 in
|
adamc@909
|
800 (*if dangling (edepth' (deKnown env)) r then
|
adamc@909
|
801 (Print.prefaces "exp" [("e", CorePrint.p_exp CoreEnv.empty all),
|
adamc@909
|
802 ("r", CorePrint.p_exp CoreEnv.empty r)];
|
adamc@909
|
803 raise Fail "!!")
|
adamc@909
|
804 else
|
adamc@909
|
805 ();*)
|
adamc@909
|
806 r
|
adamc@909
|
807 end
|
adamc@417
|
808 in
|
adamc@626
|
809 {kind = kind, con = con, exp = exp}
|
adamc@417
|
810 end
|
adamc@21
|
811
|
adamc@626
|
812 fun kind namedC env k = #kind (kindConAndExp (namedC, IM.empty)) env k
|
adamc@626
|
813 fun con namedC env c = #con (kindConAndExp (namedC, IM.empty)) env c
|
adamc@626
|
814 fun exp (namedC, namedE) env e = #exp (kindConAndExp (namedC, namedE)) env e
|
adamc@20
|
815
|
adamc@508
|
816 fun reduce file =
|
adamc@508
|
817 let
|
adamc@1016
|
818 val uses = CoreUtil.File.fold {kind = fn (_, m) => m,
|
adamc@1016
|
819 con = fn (_, m) => m,
|
adamc@1016
|
820 exp = fn (e, m) =>
|
adamc@1016
|
821 case e of
|
adamc@1016
|
822 ENamed n => IM.insert (m, n, 1 + Option.getOpt (IM.find (m, n), 0))
|
adamc@1016
|
823 | _ => m,
|
adamc@1016
|
824 decl = fn (_, m) => m}
|
adamc@1016
|
825 IM.empty file
|
adamc@1016
|
826
|
adamc@1016
|
827 fun isPoly names = CoreUtil.Con.exists {kind = fn _ => false,
|
adamc@1016
|
828 con = fn TCFun _ => true
|
adamc@1016
|
829 | TKFun _ => true
|
adamc@1016
|
830 | CNamed n => IS.member (names, n)
|
adamc@1016
|
831 | _ => false}
|
adamc@1016
|
832
|
adamc@1016
|
833 val size = CoreUtil.Exp.fold {kind = fn (_, n) => n,
|
adamc@1016
|
834 con = fn (_, n) => n,
|
adamc@1016
|
835 exp = fn (_, n) => n + 1} 0
|
adamc@1016
|
836
|
adamc@1016
|
837 fun mayInline (polyC, n, t, e) =
|
adamc@1016
|
838 case IM.find (uses, n) of
|
adamc@1016
|
839 NONE => false
|
adamc@1016
|
840 | SOME count => count <= 1
|
adamc@1016
|
841 orelse isPoly polyC t
|
adamc@1016
|
842 orelse size e <= Settings.getCoreInline ()
|
adamc@1016
|
843
|
adamc@1016
|
844 fun doDecl (d as (_, loc), st as (polyC, namedC, namedE)) =
|
adamc@508
|
845 case #1 d of
|
adamc@508
|
846 DCon (x, n, k, c) =>
|
adamc@508
|
847 let
|
adamc@626
|
848 val k = kind namedC [] k
|
adamc@509
|
849 val c = con namedC [] c
|
adamc@508
|
850 in
|
adamc@508
|
851 ((DCon (x, n, k, c), loc),
|
adamc@1016
|
852 (if isPoly polyC c then
|
adamc@1016
|
853 IS.add (polyC, n)
|
adamc@1016
|
854 else
|
adamc@1016
|
855 polyC,
|
adamc@1016
|
856 IM.insert (namedC, n, c),
|
adamc@1016
|
857 namedE))
|
adamc@508
|
858 end
|
adamc@807
|
859 | DDatatype dts =>
|
adamc@807
|
860 ((DDatatype (map (fn (x, n, ps, cs) =>
|
adamc@807
|
861 let
|
adamc@807
|
862 val env = map (fn _ => UnknownC) ps
|
adamc@807
|
863 in
|
adamc@807
|
864 (x, n, ps, map (fn (x, n, co) => (x, n, Option.map (con namedC env) co)) cs)
|
adamc@807
|
865 end) dts), loc),
|
adamc@1016
|
866 (if List.exists (fn (_, _, _, cs) => List.exists (fn (_, _, co) => case co of
|
adamc@1016
|
867 NONE => false
|
adamc@1016
|
868 | SOME c => isPoly polyC c) cs)
|
adamc@1016
|
869 dts then
|
adamc@1016
|
870 foldl (fn ((_, n, _, _), polyC) => IS.add (polyC, n)) polyC dts
|
adamc@1016
|
871 else
|
adamc@1016
|
872 polyC,
|
adamc@1016
|
873 namedC,
|
adamc@1016
|
874 namedE))
|
adamc@508
|
875 | DVal (x, n, t, e, s) =>
|
adamc@508
|
876 let
|
adamc@509
|
877 val t = con namedC [] t
|
adamc@509
|
878 val e = exp (namedC, namedE) [] e
|
adamc@508
|
879 in
|
adamc@508
|
880 ((DVal (x, n, t, e, s), loc),
|
adamc@1016
|
881 (polyC,
|
adamc@1016
|
882 namedC,
|
adamc@1016
|
883 if mayInline (polyC, n, t, e) then
|
adamc@1016
|
884 IM.insert (namedE, n, e)
|
adamc@1016
|
885 else
|
adamc@1016
|
886 namedE))
|
adamc@508
|
887 end
|
adamc@508
|
888 | DValRec vis =>
|
adamc@910
|
889 ((DValRec (map (fn (x, n, t, e, s) => (x, n, con namedC [] t,
|
adamc@910
|
890 exp (namedC, namedE) [] e, s)) vis), loc),
|
adamc@508
|
891 st)
|
adamc@508
|
892 | DExport _ => (d, st)
|
adamc@707
|
893 | DTable (s, n, c, s', pe, pc, ce, cc) => ((DTable (s, n, con namedC [] c, s',
|
adamc@707
|
894 exp (namedC, namedE) [] pe,
|
adamc@707
|
895 con namedC [] pc,
|
adamc@707
|
896 exp (namedC, namedE) [] ce,
|
adamc@707
|
897 con namedC [] cc), loc), st)
|
adamc@508
|
898 | DSequence _ => (d, st)
|
adamc@754
|
899 | DView (s, n, s', e, c) => ((DView (s, n, s', exp (namedC, namedE) [] e, con namedC [] c), loc), st)
|
adamc@508
|
900 | DDatabase _ => (d, st)
|
adamc@509
|
901 | DCookie (s, n, c, s') => ((DCookie (s, n, con namedC [] c, s'), loc), st)
|
adamc@720
|
902 | DStyle (s, n, s') => ((DStyle (s, n, s'), loc), st)
|
adamc@20
|
903
|
adamc@1016
|
904 val (file, _) = ListUtil.foldlMap doDecl (IS.empty, IM.empty, IM.empty) file
|
adamc@508
|
905 in
|
adamc@508
|
906 file
|
adamc@508
|
907 end
|
adamc@20
|
908
|
adamc@20
|
909 end
|