adamc@484
|
1 (* Copyright (c) 2008, Adam Chlipala
|
adamc@484
|
2 * All rights reserved.
|
adamc@484
|
3 *
|
adamc@484
|
4 * Redistribution and use in source and binary forms, with or without
|
adamc@484
|
5 * modification, are permitted provided that the following conditions are met:
|
adamc@484
|
6 *
|
adamc@484
|
7 * - Redistributions of source code must retain the above copyright notice,
|
adamc@484
|
8 * this list of conditions and the following disclaimer.
|
adamc@484
|
9 * - Redistributions in binary form must reproduce the above copyright notice,
|
adamc@484
|
10 * this list of conditions and the following disclaimer in the documentation
|
adamc@484
|
11 * and/or other materials provided with the distribution.
|
adamc@484
|
12 * - The names of contributors may not be used to endorse or promote products
|
adamc@484
|
13 * derived from this software without specific prior written permission.
|
adamc@484
|
14 *
|
adamc@484
|
15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
|
adamc@484
|
16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
|
adamc@484
|
17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
|
adamc@484
|
18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
|
adamc@484
|
19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
|
adamc@484
|
20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
|
adamc@484
|
21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
|
adamc@484
|
22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
|
adamc@484
|
23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
|
adamc@484
|
24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
|
adamc@484
|
25 * POSSIBILITY OF SUCH DAMAGE.
|
adamc@484
|
26 *)
|
adamc@484
|
27
|
adamc@484
|
28 structure Defunc :> DEFUNC = struct
|
adamc@484
|
29
|
adamc@484
|
30 open Core
|
adamc@484
|
31
|
adamc@484
|
32 structure E = CoreEnv
|
adamc@484
|
33 structure U = CoreUtil
|
adamc@484
|
34
|
adamc@484
|
35 structure IS = IntBinarySet
|
adamc@484
|
36
|
adamc@484
|
37 val functionInside = U.Con.exists {kind = fn _ => false,
|
adamc@484
|
38 con = fn TFun _ => true
|
adamc@484
|
39 | CFfi ("Basis", "transaction") => true
|
adamc@484
|
40 | _ => false}
|
adamc@484
|
41
|
adamc@484
|
42 val freeVars = U.Exp.foldB {kind = fn (_, xs) => xs,
|
adamc@484
|
43 con = fn (_, _, xs) => xs,
|
adamc@484
|
44 exp = fn (bound, e, xs) =>
|
adamc@484
|
45 case e of
|
adamc@484
|
46 ERel x =>
|
adamc@484
|
47 if x >= bound then
|
adamc@484
|
48 IS.add (xs, x - bound)
|
adamc@484
|
49 else
|
adamc@484
|
50 xs
|
adamc@484
|
51 | _ => xs,
|
adamc@484
|
52 bind = fn (bound, b) =>
|
adamc@484
|
53 case b of
|
adamc@484
|
54 U.Exp.RelE _ => bound + 1
|
adamc@484
|
55 | _ => bound}
|
adamc@484
|
56 0 IS.empty
|
adamc@484
|
57
|
adamc@484
|
58 fun positionOf (v : int, ls) =
|
adamc@484
|
59 let
|
adamc@484
|
60 fun pof (pos, ls) =
|
adamc@484
|
61 case ls of
|
adamc@484
|
62 [] => raise Fail "Defunc.positionOf"
|
adamc@484
|
63 | v' :: ls' =>
|
adamc@484
|
64 if v = v' then
|
adamc@484
|
65 pos
|
adamc@484
|
66 else
|
adamc@484
|
67 pof (pos + 1, ls')
|
adamc@484
|
68 in
|
adamc@484
|
69 pof (0, ls)
|
adamc@484
|
70 end
|
adamc@484
|
71
|
adamc@484
|
72 fun squish fvs =
|
adamc@484
|
73 U.Exp.mapB {kind = fn k => k,
|
adamc@484
|
74 con = fn _ => fn c => c,
|
adamc@484
|
75 exp = fn bound => fn e =>
|
adamc@484
|
76 case e of
|
adamc@484
|
77 ERel x =>
|
adamc@484
|
78 if x >= bound then
|
adamc@484
|
79 ERel (positionOf (x - bound, fvs) + bound)
|
adamc@484
|
80 else
|
adamc@484
|
81 e
|
adamc@484
|
82 | _ => e,
|
adamc@484
|
83 bind = fn (bound, b) =>
|
adamc@484
|
84 case b of
|
adamc@484
|
85 U.Exp.RelE _ => bound + 1
|
adamc@484
|
86 | _ => bound}
|
adamc@484
|
87 0
|
adamc@484
|
88
|
adamc@484
|
89 fun default (_, x, st) = (x, st)
|
adamc@484
|
90
|
adamc@484
|
91 datatype 'a search =
|
adamc@484
|
92 Yes
|
adamc@484
|
93 | No
|
adamc@484
|
94 | Maybe of 'a
|
adamc@484
|
95
|
adamc@484
|
96 structure EK = struct
|
adamc@484
|
97 type ord_key = exp
|
adamc@484
|
98 val compare = U.Exp.compare
|
adamc@484
|
99 end
|
adamc@484
|
100
|
adamc@484
|
101 structure EM = BinaryMapFn(EK)
|
adamc@484
|
102
|
adamc@484
|
103 type state = {
|
adamc@484
|
104 maxName : int,
|
adamc@484
|
105 funcs : int EM.map,
|
adamc@484
|
106 vis : (string * int * con * exp * string) list
|
adamc@484
|
107 }
|
adamc@484
|
108
|
adamc@484
|
109 fun exp (env, e, st) =
|
adamc@484
|
110 case e of
|
adamc@484
|
111 ERecord xes =>
|
adamc@484
|
112 let
|
adamc@484
|
113 val (xes, st) =
|
adamc@484
|
114 ListUtil.foldlMap
|
adamc@484
|
115 (fn (tup as (fnam as (CName x, loc), e, xt), st) =>
|
adamc@485
|
116 if (x <> "Link" andalso x <> "Action")
|
adamc@485
|
117 orelse case #1 e of
|
adamc@485
|
118 ENamed _ => true
|
adamc@485
|
119 | _ => false then
|
adamc@484
|
120 (tup, st)
|
adamc@484
|
121 else
|
adamc@484
|
122 let
|
adamc@484
|
123 fun needsAttention (e, _) =
|
adamc@484
|
124 case e of
|
adamc@484
|
125 ENamed f => Maybe (#2 (E.lookupENamed env f))
|
adamc@484
|
126 | EApp (f, _) =>
|
adamc@484
|
127 (case needsAttention f of
|
adamc@484
|
128 No => No
|
adamc@484
|
129 | Yes => Yes
|
adamc@484
|
130 | Maybe t =>
|
adamc@484
|
131 case t of
|
adamc@484
|
132 (TFun (dom, _), _) =>
|
adamc@484
|
133 if functionInside dom then
|
adamc@484
|
134 Yes
|
adamc@484
|
135 else
|
adamc@484
|
136 No
|
adamc@484
|
137 | _ => No)
|
adamc@484
|
138 | _ => No
|
adamc@484
|
139
|
adamc@484
|
140 fun headSymbol (e, _) =
|
adamc@484
|
141 case e of
|
adamc@484
|
142 ENamed f => f
|
adamc@484
|
143 | EApp (e, _) => headSymbol e
|
adamc@484
|
144 | _ => raise Fail "Defunc: headSymbol"
|
adamc@484
|
145
|
adamc@484
|
146 fun rtype (e, _) =
|
adamc@484
|
147 case e of
|
adamc@484
|
148 ENamed f => #2 (E.lookupENamed env f)
|
adamc@484
|
149 | EApp (f, _) =>
|
adamc@484
|
150 (case rtype f of
|
adamc@484
|
151 (TFun (_, ran), _) => ran
|
adamc@484
|
152 | _ => raise Fail "Defunc: rtype [1]")
|
adamc@484
|
153 | _ => raise Fail "Defunc: rtype [2]"
|
adamc@484
|
154 in
|
adamc@484
|
155 (*Print.prefaces "Found one!"
|
adamc@484
|
156 [("e", CorePrint.p_exp env e)];*)
|
adamc@484
|
157 case needsAttention e of
|
adamc@484
|
158 Yes =>
|
adamc@484
|
159 let
|
adamc@484
|
160 (*val () = print "Yes\n"*)
|
adamc@484
|
161 val f = headSymbol e
|
adamc@484
|
162
|
adamc@484
|
163 val fvs = IS.listItems (freeVars e)
|
adamc@484
|
164
|
adamc@484
|
165 val e = squish fvs e
|
adamc@484
|
166 val (e, t) = foldl (fn (n, (e, t)) =>
|
adamc@484
|
167 let
|
adamc@484
|
168 val (x, xt) = E.lookupERel env n
|
adamc@484
|
169 in
|
adamc@484
|
170 ((EAbs (x, xt, t, e), loc),
|
adamc@484
|
171 (TFun (xt, t), loc))
|
adamc@484
|
172 end)
|
adamc@484
|
173 (e, rtype e) fvs
|
adamc@484
|
174
|
adamc@484
|
175 val (f', st) =
|
adamc@484
|
176 case EM.find (#funcs st, e) of
|
adamc@484
|
177 SOME f' => (f', st)
|
adamc@484
|
178 | NONE =>
|
adamc@484
|
179 let
|
adamc@484
|
180 val (fx, _, _, tag) = E.lookupENamed env f
|
adamc@484
|
181 val f' = #maxName st
|
adamc@484
|
182
|
adamc@484
|
183 val vi = (fx, f', t, e, tag)
|
adamc@484
|
184 in
|
adamc@484
|
185 (f', {maxName = f' + 1,
|
adamc@484
|
186 funcs = EM.insert (#funcs st, e, f'),
|
adamc@484
|
187 vis = vi :: #vis st})
|
adamc@484
|
188 end
|
adamc@484
|
189
|
adamc@484
|
190 val e = foldr (fn (n, e) =>
|
adamc@484
|
191 (EApp (e, (ERel n, loc)), loc))
|
adamc@484
|
192 (ENamed f', loc) fvs
|
adamc@484
|
193 in
|
adamc@484
|
194 (*app (fn n => Print.prefaces
|
adamc@484
|
195 "Free"
|
adamc@484
|
196 [("n", CorePrint.p_exp env (ERel n, ErrorMsg.dummySpan))])
|
adamc@484
|
197 fvs;
|
adamc@484
|
198 Print.prefaces "Squished"
|
adamc@484
|
199 [("e", CorePrint.p_exp CoreEnv.empty e)];*)
|
adamc@484
|
200
|
adamc@484
|
201 ((fnam, e, xt), st)
|
adamc@484
|
202 end
|
adamc@484
|
203 | _ => (tup, st)
|
adamc@484
|
204 end
|
adamc@484
|
205 | (tup, st) => (tup, st))
|
adamc@484
|
206 st xes
|
adamc@484
|
207 in
|
adamc@484
|
208 (ERecord xes, st)
|
adamc@484
|
209 end
|
adamc@484
|
210 | _ => (e, st)
|
adamc@484
|
211
|
adamc@484
|
212 fun bind (env, b) =
|
adamc@484
|
213 case b of
|
adamc@484
|
214 U.Decl.RelC (x, k) => E.pushCRel env x k
|
adamc@484
|
215 | U.Decl.NamedC (x, n, k, co) => E.pushCNamed env x n k co
|
adamc@484
|
216 | U.Decl.RelE (x, t) => E.pushERel env x t
|
adamc@484
|
217 | U.Decl.NamedE (x, n, t, eo, s) => E.pushENamed env x n t eo s
|
adamc@484
|
218
|
adamc@484
|
219 fun doDecl env = U.Decl.foldMapB {kind = fn x => x,
|
adamc@484
|
220 con = default,
|
adamc@484
|
221 exp = exp,
|
adamc@484
|
222 decl = default,
|
adamc@484
|
223 bind = bind}
|
adamc@484
|
224 env
|
adamc@484
|
225
|
adamc@484
|
226 fun defunc file =
|
adamc@484
|
227 let
|
adamc@484
|
228 fun doDecl' (d, (env, st)) =
|
adamc@484
|
229 let
|
adamc@484
|
230 val env = E.declBinds env d
|
adamc@484
|
231
|
adamc@484
|
232 val (d, st) = doDecl env st d
|
adamc@484
|
233
|
adamc@484
|
234 val ds =
|
adamc@484
|
235 case #vis st of
|
adamc@484
|
236 [] => [d]
|
adamc@484
|
237 | vis =>
|
adamc@484
|
238 case d of
|
adamc@484
|
239 (DValRec vis', loc) => [(DValRec (vis' @ vis), loc)]
|
adamc@484
|
240 | _ => [(DValRec vis, #2 d), d]
|
adamc@484
|
241 in
|
adamc@484
|
242 (ds,
|
adamc@484
|
243 (env,
|
adamc@484
|
244 {maxName = #maxName st,
|
adamc@484
|
245 funcs = #funcs st,
|
adamc@484
|
246 vis = []}))
|
adamc@484
|
247 end
|
adamc@484
|
248
|
adamc@484
|
249 val (file, _) = ListUtil.foldlMapConcat doDecl'
|
adamc@484
|
250 (E.empty,
|
adamc@484
|
251 {maxName = U.File.maxName file + 1,
|
adamc@484
|
252 funcs = EM.empty,
|
adamc@484
|
253 vis = []})
|
adamc@484
|
254 file
|
adamc@484
|
255 in
|
adamc@484
|
256 file
|
adamc@484
|
257 end
|
adamc@484
|
258
|
adamc@484
|
259 end
|