adamc@443
|
1 (* Copyright (c) 2008, Adam Chlipala
|
adamc@443
|
2 * All rights reserved.
|
adamc@443
|
3 *
|
adamc@443
|
4 * Redistribution and use in source and binary forms, with or without
|
adamc@443
|
5 * modification, are permitted provided that the following conditions are met:
|
adamc@443
|
6 *
|
adamc@443
|
7 * - Redistributions of source code must retain the above copyright notice,
|
adamc@443
|
8 * this list of conditions and the following disclaimer.
|
adamc@443
|
9 * - Redistributions in binary form must reproduce the above copyright notice,
|
adamc@443
|
10 * this list of conditions and the following disclaimer in the documentation
|
adamc@443
|
11 * and/or other materials provided with the distribution.
|
adamc@443
|
12 * - The names of contributors may not be used to endorse or promote products
|
adamc@443
|
13 * derived from this software without specific prior written permission.
|
adamc@443
|
14 *
|
adamc@443
|
15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
|
adamc@443
|
16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
|
adamc@443
|
17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
|
adamc@443
|
18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
|
adamc@443
|
19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
|
adamc@443
|
20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
|
adamc@443
|
21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
|
adamc@443
|
22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
|
adamc@443
|
23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
|
adamc@443
|
24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
|
adamc@443
|
25 * POSSIBILITY OF SUCH DAMAGE.
|
adamc@443
|
26 *)
|
adamc@443
|
27
|
adamc@443
|
28 structure ESpecialize :> ESPECIALIZE = struct
|
adamc@443
|
29
|
adamc@443
|
30 open Core
|
adamc@443
|
31
|
adamc@443
|
32 structure E = CoreEnv
|
adamc@443
|
33 structure U = CoreUtil
|
adamc@443
|
34
|
adamc@443
|
35 structure ILK = struct
|
adamc@443
|
36 type ord_key = int list
|
adamc@443
|
37 val compare = Order.joinL Int.compare
|
adamc@443
|
38 end
|
adamc@443
|
39
|
adamc@443
|
40 structure ILM = BinaryMapFn(ILK)
|
adamc@443
|
41 structure IM = IntBinaryMap
|
adamc@443
|
42
|
adamc@443
|
43 type func = {
|
adamc@443
|
44 name : string,
|
adamc@443
|
45 args : int ILM.map,
|
adamc@443
|
46 body : exp,
|
adamc@443
|
47 typ : con,
|
adamc@443
|
48 tag : string
|
adamc@443
|
49 }
|
adamc@443
|
50
|
adamc@443
|
51 type state = {
|
adamc@443
|
52 maxName : int,
|
adamc@443
|
53 funcs : func IM.map,
|
adamc@443
|
54 decls : (string * int * con * exp * string) list
|
adamc@443
|
55 }
|
adamc@443
|
56
|
adamc@443
|
57 fun kind (k, st) = (k, st)
|
adamc@443
|
58 fun con (c, st) = (c, st)
|
adamc@443
|
59
|
adamc@443
|
60 fun exp (e, st : state) =
|
adamc@443
|
61 let
|
adamc@443
|
62 fun getApp e =
|
adamc@443
|
63 case e of
|
adamc@443
|
64 ENamed f => SOME (f, [], [])
|
adamc@443
|
65 | EApp (e1, (ENamed x, _)) =>
|
adamc@443
|
66 (case getApp (#1 e1) of
|
adamc@443
|
67 NONE => NONE
|
adamc@443
|
68 | SOME (f, xs, xs') => SOME (f, xs @ [x], xs'))
|
adamc@443
|
69 | EApp (e1, e2) =>
|
adamc@443
|
70 (case getApp (#1 e1) of
|
adamc@443
|
71 NONE => NONE
|
adamc@443
|
72 | SOME (f, xs, xs') => SOME (f, xs, xs' @ [e2]))
|
adamc@443
|
73 | _ => NONE
|
adamc@443
|
74 in
|
adamc@443
|
75 case getApp e of
|
adamc@443
|
76 NONE => (e, st)
|
adamc@443
|
77 | SOME (_, [], _) => (e, st)
|
adamc@443
|
78 | SOME (f, xs, xs') =>
|
adamc@443
|
79 case IM.find (#funcs st, f) of
|
adamc@443
|
80 NONE => (e, st)
|
adamc@443
|
81 | SOME {name, args, body, typ, tag} =>
|
adamc@443
|
82 case ILM.find (args, xs) of
|
adamc@443
|
83 SOME f' => (#1 (foldl (fn (e, arg) => (EApp (e, arg), ErrorMsg.dummySpan))
|
adamc@443
|
84 (ENamed f', ErrorMsg.dummySpan) xs'),
|
adamc@443
|
85 st)
|
adamc@443
|
86 | NONE =>
|
adamc@443
|
87 let
|
adamc@443
|
88 fun subBody (body, typ, xs) =
|
adamc@443
|
89 case (#1 body, #1 typ, xs) of
|
adamc@443
|
90 (_, _, []) => SOME (body, typ)
|
adamc@443
|
91 | (EAbs (_, _, _, body'), TFun (_, typ'), x :: xs) =>
|
adamc@443
|
92 subBody (E.subExpInExp (0, (ENamed x, ErrorMsg.dummySpan)) body',
|
adamc@443
|
93 typ',
|
adamc@443
|
94 xs)
|
adamc@443
|
95 | _ => NONE
|
adamc@443
|
96 in
|
adamc@443
|
97 case subBody (body, typ, xs) of
|
adamc@443
|
98 NONE => (e, st)
|
adamc@443
|
99 | SOME (body', typ') =>
|
adamc@443
|
100 let
|
adamc@443
|
101 val f' = #maxName st
|
adamc@443
|
102 val funcs = IM.insert (#funcs st, f, {name = name,
|
adamc@443
|
103 args = ILM.insert (args, xs, f'),
|
adamc@443
|
104 body = body,
|
adamc@443
|
105 typ = typ,
|
adamc@443
|
106 tag = tag})
|
adamc@443
|
107 val st = {
|
adamc@443
|
108 maxName = f' + 1,
|
adamc@443
|
109 funcs = funcs,
|
adamc@443
|
110 decls = #decls st
|
adamc@443
|
111 }
|
adamc@443
|
112
|
adamc@443
|
113 val (body', st) = specExp st body'
|
adamc@443
|
114 val e' = foldl (fn (e, arg) => (EApp (e, arg), ErrorMsg.dummySpan))
|
adamc@443
|
115 (ENamed f', ErrorMsg.dummySpan) xs'
|
adamc@443
|
116 in
|
adamc@443
|
117 (#1 e',
|
adamc@443
|
118 {maxName = #maxName st,
|
adamc@443
|
119 funcs = #funcs st,
|
adamc@443
|
120 decls = (name, f', typ', body', tag ^ "_espec") :: #decls st})
|
adamc@443
|
121 end
|
adamc@443
|
122 end
|
adamc@443
|
123 end
|
adamc@443
|
124
|
adamc@443
|
125 and specExp st = U.Exp.foldMap {kind = kind, con = con, exp = exp} st
|
adamc@443
|
126
|
adamc@443
|
127 fun decl (d, st) = (d, st)
|
adamc@443
|
128
|
adamc@443
|
129 val specDecl = U.Decl.foldMap {kind = kind, con = con, exp = exp, decl = decl}
|
adamc@443
|
130
|
adamc@443
|
131 fun specialize file =
|
adamc@443
|
132 let
|
adamc@443
|
133 fun doDecl (d, st) =
|
adamc@443
|
134 let
|
adamc@443
|
135 val (d', st) = specDecl st d
|
adamc@443
|
136
|
adamc@443
|
137 val funcs = #funcs st
|
adamc@443
|
138 val funcs =
|
adamc@443
|
139 case #1 d of
|
adamc@443
|
140 DVal (x, n, c, e as (EAbs _, _), tag) =>
|
adamc@443
|
141 IM.insert (funcs, n, {name = x,
|
adamc@443
|
142 args = ILM.empty,
|
adamc@443
|
143 body = e,
|
adamc@443
|
144 typ = c,
|
adamc@443
|
145 tag = tag})
|
adamc@443
|
146 | DValRec vis =>
|
adamc@443
|
147 foldl (fn ((x, n, c, e, tag), funcs) =>
|
adamc@443
|
148 IM.insert (funcs, n, {name = x,
|
adamc@443
|
149 args = ILM.empty,
|
adamc@443
|
150 body = e,
|
adamc@443
|
151 typ = c,
|
adamc@443
|
152 tag = tag}))
|
adamc@443
|
153 funcs vis
|
adamc@443
|
154 | _ => funcs
|
adamc@443
|
155
|
adamc@443
|
156 val ds =
|
adamc@443
|
157 case #decls st of
|
adamc@443
|
158 [] => [d']
|
adamc@443
|
159 | vis => [(DValRec vis, ErrorMsg.dummySpan), d']
|
adamc@443
|
160 in
|
adamc@443
|
161 (ds, {maxName = #maxName st,
|
adamc@443
|
162 funcs = funcs,
|
adamc@443
|
163 decls = []})
|
adamc@443
|
164 end
|
adamc@443
|
165
|
adamc@443
|
166 val (ds, _) = ListUtil.foldlMapConcat doDecl
|
adamc@443
|
167 {maxName = U.File.maxName file + 1,
|
adamc@443
|
168 funcs = IM.empty,
|
adamc@443
|
169 decls = []}
|
adamc@443
|
170 file
|
adamc@443
|
171 in
|
adamc@443
|
172 ds
|
adamc@443
|
173 end
|
adamc@443
|
174
|
adamc@443
|
175
|
adamc@443
|
176 end
|