Mercurial > urweb

comparison src/expl_rename.sml @ 1989:210fb3dfc483

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Some more nested functor bug-fixing, including generating fresh internal names at applications; still need to debug issues with datatype constructors
author Adam Chlipala <adam@chlipala.net>
date Thu, 20 Feb 2014 10:27:15 -0500
parents
children 7bd2ecf96bb0
comparison
equal deleted inserted replaced
1988:abb6981a2c4c 1989:210fb3dfc483
1 (* Copyright (c) 2014, Adam Chlipala
2 * All rights reserved.
3 *
4 * Redistribution and use in source and binary forms, with or without
5 * modification, are permitted provided that the following conditions are met:
6 *
7 * - Redistributions of source code must retain the above copyright notice,
8 * this list of conditions and the following disclaimer.
9 * - Redistributions in binary form must reproduce the above copyright notice,
10 * this list of conditions and the following disclaimer in the documentation
11 * and/or other materials provided with the distribution.
12 * - The names of contributors may not be used to endorse or promote products
13 * derived from this software without specific prior written permission.
14 *
15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
25 * POSSIBILITY OF SUCH DAMAGE.
26 *)
27
28 structure ExplRename :> EXPL_RENAME = struct
29
30 open Expl
31 structure E = ExplEnv
32
33 structure IM = IntBinaryMap
34
35 structure St :> sig
36 type t
37
38 val create : int -> t
39 val next : t -> int
40
41 val bind : t * int -> t * int
42 val lookup: t * int -> int option
43 end = struct
44
45 type t = {next : int,
46 renaming : int IM.map}
47
48 fun create next = {next = next,
49 renaming = IM.empty}
50
51 fun next (t : t) = #next t
52
53 fun bind ({next, renaming}, n) =
54 ({next = next + 1,
55 renaming = IM.insert (renaming, n, next)}, next)
56
57 fun lookup ({next, renaming}, n) =
58 IM.find (renaming, n)
59
60 end
61
62 fun renameCon st (all as (c, loc)) =
63 case c of
64 TFun (c1, c2) => (TFun (renameCon st c1, renameCon st c2), loc)
65 | TCFun (x, k, c) => (TCFun (x, k, renameCon st c), loc)
66 | TRecord c => (TRecord (renameCon st c), loc)
67 | CRel _ => all
68 | CNamed n =>
69 (case St.lookup (st, n) of
70 NONE => all
71 | SOME n' => (CNamed n', loc))
72 | CModProj (n, ms, x) =>
73 (case St.lookup (st, n) of
74 NONE => all
75 | SOME n' => (CModProj (n', ms, x), loc))
76 | CApp (c1, c2) => (CApp (renameCon st c1, renameCon st c2), loc)
77 | CAbs (x, k, c) => (CAbs (x, k, renameCon st c), loc)
78 | CKAbs (x, c) => (CKAbs (x, renameCon st c), loc)
79 | CKApp (c, k) => (CKApp (renameCon st c, k), loc)
80 | TKFun (x, c) => (TKFun (x, renameCon st c), loc)
81 | CName _ => all
82 | CRecord (k, xcs) => (CRecord (k, map (fn (x, c) => (renameCon st x, renameCon st c)) xcs), loc)
83 | CConcat (c1, c2) => (CConcat (renameCon st c1, renameCon st c2), loc)
84 | CMap _ => all
85 | CUnit => all
86 | CTuple cs => (CTuple (map (renameCon st) cs), loc)
87 | CProj (c, n) => (CProj (renameCon st c, n), loc)
88
89 fun renamePatCon st pc =
90 case pc of
91 PConVar n =>
92 (case St.lookup (st, n) of
93 NONE => pc
94 | SOME n' => PConVar n')
95 | PConProj (n, ms, x) =>
96 (case St.lookup (st, n) of
97 NONE => pc
98 | SOME n' => PConProj (n', ms, x))
99
100 fun renamePat st (all as (p, loc)) =
101 case p of
102 PWild => all
103 | PVar (x, c) => (PVar (x, renameCon st c), loc)
104 | PPrim _ => all
105 | PCon (dk, pc, cs, po) => (PCon (dk, renamePatCon st pc,
106 map (renameCon st) cs,
107 Option.map (renamePat st) po), loc)
108 | PRecord xpcs => (PRecord (map (fn (x, p, c) =>
109 (x, renamePat st p, renameCon st c)) xpcs), loc)
110
111 fun renameExp st (all as (e, loc)) =
112 case e of
113 EPrim _ => all
114 | ERel _ => all
115 | ENamed n =>
116 (case St.lookup (st, n) of
117 NONE => all
118 | SOME n' => (ENamed n', loc))
119 | EModProj (n, ms, x) =>
120 (case St.lookup (st, n) of
121 NONE => all
122 | SOME n' => (EModProj (n', ms, x), loc))
123 | EApp (e1, e2) => (EApp (renameExp st e1, renameExp st e2), loc)
124 | EAbs (x, dom, ran, e) => (EAbs (x, renameCon st dom, renameCon st ran, renameExp st e), loc)
125 | ECApp (e, c) => (ECApp (renameExp st e, renameCon st c), loc)
126 | ECAbs (x, k, e) => (ECAbs (x, k, renameExp st e), loc)
127 | EKAbs (x, e) => (EKAbs (x, renameExp st e), loc)
128 | EKApp (e, k) => (EKApp (renameExp st e, k), loc)
129 | ERecord xecs => (ERecord (map (fn (x, e, c) => (renameCon st x,
130 renameExp st e,
131 renameCon st c)) xecs), loc)
132 | EField (e, c, {field, rest}) => (EField (renameExp st e,
133 renameCon st c,
134 {field = renameCon st field,
135 rest = renameCon st rest}), loc)
136 | EConcat (e1, c1, e2, c2) => (EConcat (renameExp st e1,
137 renameCon st c1,
138 renameExp st e2,
139 renameCon st c2), loc)
140 | ECut (e, c, {field, rest}) => (ECut (renameExp st e,
141 renameCon st c,
142 {field = renameCon st field,
143 rest = renameCon st rest}), loc)
144 | ECutMulti (e, c, {rest}) => (ECutMulti (renameExp st e,
145 renameCon st c,
146 {rest = renameCon st rest}), loc)
147 | ECase (e, pes, {disc, result}) => (ECase (renameExp st e,
148 map (fn (p, e) => (renamePat st p, renameExp st e)) pes,
149 {disc = renameCon st disc,
150 result = renameCon st result}), loc)
151 | EWrite e => (EWrite (renameExp st e), loc)
152 | ELet (x, c1, e1, e2) => (ELet (x, renameCon st c1,
153 renameExp st e1,
154 renameExp st e2), loc)
155
156 fun renameSitem st (all as (si, loc)) =
157 case si of
158 SgiConAbs _ => all
159 | SgiCon (x, n, k, c) => (SgiCon (x, n, k, renameCon st c), loc)
160 | SgiDatatype dts => (SgiDatatype (map (fn (x, n, xs, cns) =>
161 (x, n, xs,
162 map (fn (x, n, co) =>
163 (x, n, Option.map (renameCon st) co)) cns)) dts),
164 loc)
165 | SgiDatatypeImp (x, n, n', xs, x', xs', cns) =>
166 (SgiDatatypeImp (x, n, n', xs, x', xs',
167 map (fn (x, n, co) =>
168 (x, n, Option.map (renameCon st) co)) cns), loc)
169 | SgiVal (x, n, c) => (SgiVal (x, n, renameCon st c), loc)
170 | SgiSgn (x, n, sg) => (SgiSgn (x, n, renameSgn st sg), loc)
171 | SgiStr (x, n, sg) => (SgiStr (x, n, renameSgn st sg), loc)
172
173 and renameSgn st (all as (sg, loc)) =
174 case sg of
175 SgnConst sis => (SgnConst (map (renameSitem st) sis), loc)
176 | SgnVar n =>
177 (case St.lookup (st, n) of
178 NONE => all
179 | SOME n' => (SgnVar n', loc))
180 | SgnFun (x, n, dom, ran) => (SgnFun (x, n, renameSgn st dom, renameSgn st ran), loc)
181 | SgnWhere (sg, xs, s, c) => (SgnWhere (renameSgn st sg, xs, s, renameCon st c), loc)
182 | SgnProj (n, ms, x) =>
183 (case St.lookup (st, n) of
184 NONE => all
185 | SOME n' => (SgnProj (n', ms, x), loc))
186
187 fun renameDecl st (all as (d, loc)) =
188 case d of
189 DCon (x, n, k, c) => (DCon (x, n, k, renameCon st c), loc)
190 | DDatatype dts => (DDatatype (map (fn (x, n, xs, cns) =>
191 (x, n, xs,
192 map (fn (x, n, co) =>
193 (x, n, Option.map (renameCon st) co)) cns)) dts),
194 loc)
195 | DDatatypeImp (x, n, n', xs, x', xs', cns) =>
196 (DDatatypeImp (x, n, n', xs, x', xs',
197 map (fn (x, n, co) =>
198 (x, n, Option.map (renameCon st) co)) cns), loc)
199 | DVal (x, n, c, e) => (DVal (x, n, renameCon st c, renameExp st e), loc)
200 | DValRec vis => (DValRec (map (fn (x, n, c, e) => (x, n, renameCon st c, renameExp st e)) vis), loc)
201 | DSgn (x, n, sg) => (DSgn (x, n, renameSgn st sg), loc)
202 | DStr (x, n, sg, str) => (DStr (x, n, renameSgn st sg, renameStr st str), loc)
203 | DFfiStr (x, n, sg) => (DFfiStr (x, n, renameSgn st sg), loc)
204 | DExport (n, sg, str) =>
205 (case St.lookup (st, n) of
206 NONE => all
207 | SOME n' => (DExport (n', renameSgn st sg, renameStr st str), loc))
208 | DTable (n, x, m, c1, e1, c2, e2, c3) =>
209 (DTable (n, x, m, renameCon st c1, renameExp st e1, renameCon st c2,
210 renameExp st e2, renameCon st c3), loc)
211 | DSequence _ => all
212 | DView (n, x, n', e, c) => (DView (n, x, n', renameExp st e, renameCon st c), loc)
213 | DDatabase _ => all
214 | DCookie (n, x, n', c) => (DCookie (n, x, n', renameCon st c), loc)
215 | DStyle _ => all
216 | DTask (e1, e2) => (DTask (renameExp st e1, renameExp st e2), loc)
217 | DPolicy e => (DPolicy (renameExp st e), loc)
218 | DOnError (n, xs, x) =>
219 (case St.lookup (st, n) of
220 NONE => all
221 | SOME n' => (DOnError (n', xs, x), loc))
222
223 and renameStr st (all as (str, loc)) =
224 case str of
225 StrConst ds => (StrConst (map (renameDecl st) ds), loc)
226 | StrVar n =>
227 (case St.lookup (st, n) of
228 NONE => all
229 | SOME n' => (StrVar n', loc))
230 | StrProj (str, x) => (StrProj (renameStr st str, x), loc)
231 | StrFun (x, n, dom, ran, str) => (StrFun (x, n, renameSgn st dom,
232 renameSgn st ran,
233 renameStr st str), loc)
234 | StrApp (str1, str2) => (StrApp (renameStr st str1, renameStr st str2), loc)
235
236
237
238 fun fromArity (n, loc) =
239 case n of
240 0 => (KType, loc)
241 | _ => (KArrow ((KType, loc), fromArity (n - 1, loc)), loc)
242
243 fun dupDecl (all as (d, loc), st) =
244 case d of
245 DCon (x, n, k, c) =>
246 let
247 val (st, n') = St.bind (st, n)
248 in
249 ([(DCon (x, n, k, renameCon st c), loc),
250 (DCon (x, n', k, (CNamed n, loc)), loc)],
251 st)
252 end
253 | DDatatype dts =>
254 let
255 val (dts', st) = ListUtil.foldlMap (fn ((x, n, xs, cns), st) =>
256 let
257 val (st, n') = St.bind (st, n)
258
259 val (cns', st) = ListUtil.foldlMap
260 (fn ((x, n, _), st) =>
261 let
262 val (st, n') =
263 St.bind (st, n)
264 in
265 ((x, n, n'), st)
266 end) st cns
267 in
268 ((x, n, length xs, n', cns'), st)
269 end) st dts
270
271 val d = (DDatatype (map (fn (x, n, xs, cns) =>
272 (x, n, xs,
273 map (fn (x, n, co) =>
274 (x, n, Option.map (renameCon st) co)) cns)) dts),
275 loc)
276
277 val env = E.declBinds E.empty d
278 in
279 (d
280 :: map (fn (x, n, arity, n', _) =>
281 (DCon (x, n', fromArity (arity, loc), (CNamed n, loc)), loc)) dts'
282 @ ListUtil.mapConcat (fn (_, _, _, _, cns') =>
283 map (fn (x, n, n') =>
284 (DVal (x, n', #2 (E.lookupENamed env n), (ENamed n, loc)),
285 loc)) cns') dts',
286 st)
287 end
288 | DDatatypeImp (x, n, n', xs, x', xs', cns) =>
289 let
290 val (cns', st) = ListUtil.foldlMap
291 (fn ((x, n, _), st) =>
292 let
293 val (st, n') =
294 St.bind (st, n)
295 in
296 ((x, n, n'), st)
297 end) st cns
298
299 val (st, n') = St.bind (st, n)
300
301 val d = (DDatatypeImp (x, n, n', xs, x', xs',
302 map (fn (x, n, co) =>
303 (x, n, Option.map (renameCon st) co)) cns), loc)
304
305 val env = E.declBinds E.empty d
306 in
307 (d
308 :: (DCon (x, n', fromArity (length xs, loc), (CNamed n, loc)), loc)
309 :: map (fn (x, n, n') =>
310 (DVal (x, n', #2 (E.lookupENamed env n), (ENamed n, loc)),
311 loc)) cns',
312 st)
313 end
314 | DVal (x, n, c, e) =>
315 let
316 val (st, n') = St.bind (st, n)
317 val c' = renameCon st c
318 in
319 ([(DVal (x, n, c', renameExp st e), loc),
320 (DVal (x, n', c', (ENamed n, loc)), loc)],
321 st)
322 end
323 | DValRec vis =>
324 let
325 val d = (DValRec (map (fn (x, n, c, e) => (x, n, renameCon st c, renameExp st e)) vis), loc)
326
327 val (vis', st) = ListUtil.foldlMap (fn ((x, n, _, _), st) =>
328 let
329 val (st, n') = St.bind (st, n)
330 in
331 ((x, n, n'), st)
332 end) st vis
333
334 val env = E.declBinds E.empty d
335 in
336 (d
337 :: map (fn (x, n, n') => (DVal (x, n', #2 (E.lookupENamed env n), (ENamed n, loc)), loc)) vis',
338 st)
339 end
340 | DSgn (x, n, sg) =>
341 let
342 val (st, n') = St.bind (st, n)
343 in
344 ([(DSgn (x, n, renameSgn st sg), loc),
345 (DSgn (x, n', (SgnVar n, loc)), loc)],
346 st)
347 end
348 | DStr (x, n, sg, str) =>
349 let
350 val (st, n') = St.bind (st, n)
351 val sg' = renameSgn st sg
352 in
353 ([(DStr (x, n, sg', renameStr st str), loc),
354 (DStr (x, n', sg', (StrVar n, loc)), loc)],
355 st)
356 end
357 | DFfiStr (x, n, sg) => ([(DFfiStr (x, n, renameSgn st sg), loc)], st)
358 | DExport (n, sg, str) =>
359 (case St.lookup (st, n) of
360 NONE => ([all], st)
361 | SOME n' => ([(DExport (n', renameSgn st sg, renameStr st str), loc)], st))
362 | DTable (n, x, m, c1, e1, c2, e2, c3) =>
363 let
364 val (st, m') = St.bind (st, m)
365
366 val d = (DTable (n, x, m, renameCon st c1, renameExp st e1, renameCon st c2,
367 renameExp st e2, renameCon st c3), loc)
368
369 val env = E.declBinds E.empty d
370 in
371 ([d, (DVal (x, m', #2 (E.lookupENamed env m), (ENamed m, loc)), loc)], st)
372 end
373 | DSequence (n, x, m) =>
374 let
375 val (st, m') = St.bind (st, m)
376
377 val env = E.declBinds E.empty all
378 in
379 ([all, (DVal (x, m', #2 (E.lookupENamed env m), (ENamed m, loc)), loc)], st)
380 end
381 | DView (n, x, m, e, c) =>
382 let
383 val (st, m') = St.bind (st, m)
384
385 val d = (DView (n, x, m, renameExp st e, renameCon st c), loc)
386
387 val env = E.declBinds E.empty d
388 in
389 ([d, (DVal (x, m', #2 (E.lookupENamed env m), (ENamed m, loc)), loc)], st)
390 end
391 | DDatabase _ => ([all], st)
392 | DCookie (n, x, m, c) =>
393 let
394 val (st, m') = St.bind (st, m)
395
396 val d = (DCookie (n, x, m, renameCon st c), loc)
397
398 val env = E.declBinds E.empty d
399 in
400 ([d, (DVal (x, m', #2 (E.lookupENamed env m), (ENamed m, loc)), loc)], st)
401 end
402 | DStyle (n, x, m) =>
403 let
404 val (st, m') = St.bind (st, m)
405
406 val env = E.declBinds E.empty all
407 in
408 ([all, (DVal (x, m', #2 (E.lookupENamed env m), (ENamed m, loc)), loc)], st)
409 end
410 | DTask (e1, e2) => ([(DTask (renameExp st e1, renameExp st e2), loc)], st)
411 | DPolicy e => ([(DPolicy (renameExp st e), loc)], st)
412 | DOnError (n, xs, x) =>
413 (case St.lookup (st, n) of
414 NONE => ([all], st)
415 | SOME n' => ([(DOnError (n', xs, x), loc)], st))
416
417 fun rename {NextId, FormalName, FormalId, Body = all as (str, loc)} =
418 case str of
419 StrConst ds =>
420 let
421 val st = St.create NextId
422 val (st, n) = St.bind (st, FormalId)
423
424 val (ds, st) = ListUtil.foldlMapConcat dupDecl st ds
425 val ds = (DStr (FormalName, n, (SgnConst [], loc), (StrVar FormalId, loc)), loc) :: ds
426 in
427 (St.next st, (StrConst ds, loc))
428 end
429 | _ => (NextId, all)
430
431 end