comparison src/especialize.sml @ 479:ffa18975e661

Broaden set of possible especializations
author Adam Chlipala <adamc@hcoop.net>
date Sat, 08 Nov 2008 14:42:52 -0500
parents b393c2fc80f8
children 40c737913075
comparison
equal deleted inserted replaced
478:6ee1c761818f 479:ffa18975e661
30 open Core 30 open Core
31 31
32 structure E = CoreEnv 32 structure E = CoreEnv
33 structure U = CoreUtil 33 structure U = CoreUtil
34 34
35 datatype skey = 35 type skey = exp
36 Named of int
37 | App of skey * skey
38 36
39 structure K = struct 37 structure K = struct
40 type ord_key = skey list 38 type ord_key = exp list
41 fun compare' (k1, k2) = 39 val compare = Order.joinL U.Exp.compare
42 case (k1, k2) of
43 (Named n1, Named n2) => Int.compare (n1, n2)
44 | (Named _, _) => LESS
45 | (_, Named _) => GREATER
46
47 | (App (x1, y1), App (x2, y2)) => Order.join (compare' (x1, x2), fn () => compare' (y1, y2))
48
49 val compare = Order.joinL compare'
50 end 40 end
51 41
52 structure KM = BinaryMapFn(K) 42 structure KM = BinaryMapFn(K)
53 structure IM = IntBinaryMap 43 structure IM = IntBinaryMap
54 44
55 fun skeyIn (e, _) = 45 val sizeOf = U.Exp.fold {kind = fn (_, n) => n,
46 con = fn (_, n) => n,
47 exp = fn (_, n) => n + 1}
48 0
49
50 val isOpen = U.Exp.existsB {kind = fn _ => false,
51 con = fn ((nc, _), c) =>
52 case c of
53 CRel n => n >= nc
54 | _ => false,
55 exp = fn ((_, ne), e) =>
56 case e of
57 ERel n => n >= ne
58 | _ => false,
59 bind = fn ((nc, ne), b) =>
60 case b of
61 U.Exp.RelC _ => (nc + 1, ne)
62 | U.Exp.RelE _ => (nc, ne + 1)
63 | _ => (nc, ne)}
64 (0, 0)
65
66 fun baseBad (e, _) =
56 case e of 67 case e of
57 ENamed n => SOME (Named n) 68 EAbs (_, _, _, e) => sizeOf e > 20
58 | EApp (e1, e2) => 69 | ENamed _ => false
59 (case (skeyIn e1, skeyIn e2) of 70 | _ => true
60 (SOME k1, SOME k2) => SOME (App (k1, k2)) 71
61 | _ => NONE) 72 fun isBad e =
62 | _ => NONE 73 case e of
63 74 (ERecord xes, _) =>
64 fun skeyOut (k, loc) = 75 length xes > 10
65 case k of 76 orelse List.exists (fn (_, e, _) => baseBad e) xes
66 Named n => (ENamed n, loc) 77 | _ => baseBad e
67 | App (k1, k2) => (EApp (skeyOut (k1, loc), skeyOut (k2, loc)), loc) 78
79 fun skeyIn e =
80 if isBad e orelse isOpen e then
81 NONE
82 else
83 SOME e
84
85 fun skeyOut e = e
68 86
69 type func = { 87 type func = {
70 name : string, 88 name : string,
71 args : int KM.map, 89 args : int KM.map,
72 body : exp, 90 body : exp,
124 fun subBody (body, typ, xs) = 142 fun subBody (body, typ, xs) =
125 case (#1 body, #1 typ, xs) of 143 case (#1 body, #1 typ, xs) of
126 (_, _, []) => SOME (body, typ) 144 (_, _, []) => SOME (body, typ)
127 | (EAbs (_, _, _, body'), TFun (_, typ'), x :: xs) => 145 | (EAbs (_, _, _, body'), TFun (_, typ'), x :: xs) =>
128 let 146 let
129 val body'' = E.subExpInExp (0, skeyOut (x, #2 body)) body' 147 val body'' = E.subExpInExp (0, skeyOut x) body'
130 in 148 in
131 (*Print.prefaces "espec" [("body'", CorePrint.p_exp CoreEnv.empty body'), 149 (*Print.prefaces "espec" [("body'", CorePrint.p_exp CoreEnv.empty body'),
132 ("body''", CorePrint.p_exp CoreEnv.empty body'')];*) 150 ("body''", CorePrint.p_exp CoreEnv.empty body'')];*)
133 subBody (body'', 151 subBody (body'',
134 typ', 152 typ',