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