adamc@16
|
1 (* Copyright (c) 2008, Adam Chlipala
|
adamc@16
|
2 * All rights reserved.
|
adamc@16
|
3 *
|
adamc@16
|
4 * Redistribution and use in source and binary forms, with or without
|
adamc@16
|
5 * modification, are permitted provided that the following conditions are met:
|
adamc@16
|
6 *
|
adamc@16
|
7 * - Redistributions of source code must retain the above copyright notice,
|
adamc@16
|
8 * this list of conditions and the following disclaimer.
|
adamc@16
|
9 * - Redistributions in binary form must reproduce the above copyright notice,
|
adamc@16
|
10 * this list of conditions and the following disclaimer in the documentation
|
adamc@16
|
11 * and/or other materials provided with the distribution.
|
adamc@16
|
12 * - The names of contributors may not be used to endorse or promote products
|
adamc@16
|
13 * derived from this software without specific prior written permission.
|
adamc@16
|
14 *
|
adamc@16
|
15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
|
adamc@16
|
16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
|
adamc@16
|
17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
|
adamc@16
|
18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
|
adamc@16
|
19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
|
adamc@16
|
20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
|
adamc@16
|
21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
|
adamc@16
|
22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
|
adamc@16
|
23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
|
adamc@16
|
24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
|
adamc@16
|
25 * POSSIBILITY OF SUCH DAMAGE.
|
adamc@16
|
26 *)
|
adamc@16
|
27
|
adamc@16
|
28 structure CoreEnv :> CORE_ENV = struct
|
adamc@16
|
29
|
adamc@16
|
30 open Core
|
adamc@16
|
31
|
adamc@16
|
32 structure U = CoreUtil
|
adamc@16
|
33
|
adamc@16
|
34 structure IM = IntBinaryMap
|
adamc@16
|
35
|
adamc@16
|
36
|
adamc@16
|
37 (* AST utility functions *)
|
adamc@16
|
38
|
adamc@626
|
39 val liftKindInKind =
|
adamc@626
|
40 U.Kind.mapB {kind = fn bound => fn k =>
|
adamc@626
|
41 case k of
|
adamc@626
|
42 KRel xn =>
|
adamc@626
|
43 if xn < bound then
|
adamc@626
|
44 k
|
adamc@626
|
45 else
|
adamc@626
|
46 KRel (xn + 1)
|
adamc@626
|
47 | _ => k,
|
adamc@626
|
48 bind = fn (bound, _) => bound + 1}
|
adamc@626
|
49
|
adamc@626
|
50 val liftKindInCon =
|
adamc@626
|
51 U.Con.mapB {kind = fn bound => fn k =>
|
adamc@626
|
52 case k of
|
adamc@626
|
53 KRel xn =>
|
adamc@626
|
54 if xn < bound then
|
adamc@626
|
55 k
|
adamc@626
|
56 else
|
adamc@626
|
57 KRel (xn + 1)
|
adamc@626
|
58 | _ => k,
|
adamc@626
|
59 con = fn _ => fn c => c,
|
adamc@626
|
60 bind = fn (bound, U.Con.RelK _) => bound + 1
|
adamc@626
|
61 | (bound, _) => bound}
|
adamc@626
|
62
|
adamc@626
|
63 val liftKindInExp =
|
adamc@626
|
64 U.Exp.mapB {kind = fn bound => fn k =>
|
adamc@626
|
65 case k of
|
adamc@626
|
66 KRel xn =>
|
adamc@626
|
67 if xn < bound then
|
adamc@626
|
68 k
|
adamc@626
|
69 else
|
adamc@626
|
70 KRel (xn + 1)
|
adamc@626
|
71 | _ => k,
|
adamc@626
|
72 con = fn _ => fn c => c,
|
adamc@626
|
73 exp = fn _ => fn e => e,
|
adamc@626
|
74 bind = fn (bound, U.Exp.RelK _) => bound + 1
|
adamc@626
|
75 | (bound, _) => bound}
|
adamc@626
|
76
|
adamc@16
|
77 val liftConInCon =
|
adamc@626
|
78 U.Con.mapB {kind = fn _ => fn k => k,
|
adamc@16
|
79 con = fn bound => fn c =>
|
adamc@16
|
80 case c of
|
adamc@16
|
81 CRel xn =>
|
adamc@16
|
82 if xn < bound then
|
adamc@16
|
83 c
|
adamc@16
|
84 else
|
adamc@16
|
85 CRel (xn + 1)
|
adamc@16
|
86 | _ => c,
|
adamc@626
|
87 bind = fn (bound, U.Con.RelC _) => bound + 1
|
adamc@16
|
88 | (bound, _) => bound}
|
adamc@16
|
89
|
adamc@16
|
90 val lift = liftConInCon 0
|
adamc@16
|
91
|
adamc@193
|
92 val subConInCon =
|
adamc@626
|
93 U.Con.mapB {kind = fn _ => fn k => k,
|
adamc@193
|
94 con = fn (xn, rep) => fn c =>
|
adamc@193
|
95 case c of
|
adamc@193
|
96 CRel xn' =>
|
adamc@193
|
97 (case Int.compare (xn', xn) of
|
adamc@193
|
98 EQUAL => #1 rep
|
adamc@193
|
99 | GREATER => CRel (xn' - 1)
|
adamc@193
|
100 | LESS => c)
|
adamc@193
|
101 | _ => c,
|
adamc@626
|
102 bind = fn ((xn, rep), U.Con.RelC _) => (xn+1, liftConInCon 0 rep)
|
adamc@193
|
103 | (ctx, _) => ctx}
|
adamc@193
|
104
|
adamc@16
|
105
|
adamc@315
|
106 val liftConInExp =
|
adamc@626
|
107 U.Exp.mapB {kind = fn _ => fn k => k,
|
adamc@315
|
108 con = fn bound => fn c =>
|
adamc@315
|
109 case c of
|
adamc@315
|
110 CRel xn =>
|
adamc@315
|
111 if xn < bound then
|
adamc@315
|
112 c
|
adamc@315
|
113 else
|
adamc@315
|
114 CRel (xn + 1)
|
adamc@315
|
115 | _ => c,
|
adamc@315
|
116 exp = fn _ => fn e => e,
|
adamc@315
|
117 bind = fn (bound, U.Exp.RelC _) => bound + 1
|
adamc@315
|
118 | (bound, _) => bound}
|
adamc@315
|
119
|
adamc@315
|
120 val subConInExp =
|
adamc@626
|
121 U.Exp.mapB {kind = fn _ => fn k => k,
|
adamc@315
|
122 con = fn (xn, rep) => fn c =>
|
adamc@417
|
123 case c of
|
adamc@417
|
124 CRel xn' =>
|
adamc@417
|
125 (case Int.compare (xn', xn) of
|
adamc@417
|
126 EQUAL => #1 rep
|
adamc@417
|
127 | GREATER => CRel (xn' - 1)
|
adamc@417
|
128 | LESS => c)
|
adamc@417
|
129 | _ => c,
|
adamc@315
|
130 exp = fn _ => fn e => e,
|
adamc@315
|
131 bind = fn ((xn, rep), U.Exp.RelC _) => (xn+1, liftConInCon 0 rep)
|
adamc@315
|
132 | (ctx, _) => ctx}
|
adamc@315
|
133
|
adamc@443
|
134 val liftExpInExp =
|
adamc@626
|
135 U.Exp.mapB {kind = fn _ => fn k => k,
|
adamc@443
|
136 con = fn _ => fn c => c,
|
adamc@443
|
137 exp = fn bound => fn e =>
|
adamc@443
|
138 case e of
|
adamc@443
|
139 ERel xn =>
|
adamc@443
|
140 if xn < bound then
|
adamc@443
|
141 e
|
adamc@443
|
142 else
|
adamc@443
|
143 ERel (xn + 1)
|
adamc@443
|
144 | _ => e,
|
adamc@443
|
145 bind = fn (bound, U.Exp.RelE _) => bound + 1
|
adamc@443
|
146 | (bound, _) => bound}
|
adamc@443
|
147
|
adamc@443
|
148 val subExpInExp =
|
adamc@626
|
149 U.Exp.mapB {kind = fn _ => fn k => k,
|
adamc@443
|
150 con = fn _ => fn c => c,
|
adamc@443
|
151 exp = fn (xn, rep) => fn e =>
|
adamc@443
|
152 case e of
|
adamc@443
|
153 ERel xn' =>
|
adamc@443
|
154 (case Int.compare (xn', xn) of
|
adamc@443
|
155 EQUAL => #1 rep
|
adamc@443
|
156 | GREATER=> ERel (xn' - 1)
|
adamc@443
|
157 | LESS => e)
|
adamc@443
|
158 | _ => e,
|
adamc@443
|
159 bind = fn ((xn, rep), U.Exp.RelE _) => (xn+1, liftExpInExp 0 rep)
|
adamc@443
|
160 | ((xn, rep), U.Exp.RelC _) => (xn, liftConInExp 0 rep)
|
adamc@443
|
161 | (ctx, _) => ctx}
|
adamc@443
|
162
|
adamc@16
|
163 (* Back to environments *)
|
adamc@16
|
164
|
adamc@16
|
165 exception UnboundRel of int
|
adamc@16
|
166 exception UnboundNamed of int
|
adamc@16
|
167
|
adamc@16
|
168 type env = {
|
adamc@626
|
169 relK : string list,
|
adamc@626
|
170
|
adamc@16
|
171 relC : (string * kind) list,
|
adamc@16
|
172 namedC : (string * kind * con option) IM.map,
|
adamc@16
|
173
|
adamc@192
|
174 datatypes : (string * string list * (string * int * con option) list) IM.map,
|
adamc@192
|
175 constructors : (string * string list * con option * int) IM.map,
|
adamc@168
|
176
|
adamc@16
|
177 relE : (string * con) list,
|
adamc@109
|
178 namedE : (string * con * exp option * string) IM.map
|
adamc@16
|
179 }
|
adamc@16
|
180
|
adamc@16
|
181 val empty = {
|
adamc@626
|
182 relK = [],
|
adamc@626
|
183
|
adamc@16
|
184 relC = [],
|
adamc@16
|
185 namedC = IM.empty,
|
adamc@16
|
186
|
adamc@168
|
187 datatypes = IM.empty,
|
adamc@177
|
188 constructors = IM.empty,
|
adamc@168
|
189
|
adamc@16
|
190 relE = [],
|
adamc@16
|
191 namedE = IM.empty
|
adamc@16
|
192 }
|
adamc@16
|
193
|
adamc@626
|
194 fun pushKRel (env : env) x =
|
adamc@626
|
195 {relK = x :: #relK env,
|
adamc@626
|
196
|
adamc@626
|
197 relC = map (fn (x, k) => (x, liftKindInKind 0 k)) (#relC env),
|
adamc@626
|
198 namedC = #namedC env,
|
adamc@626
|
199
|
adamc@626
|
200 relE = map (fn (x, c) => (x, liftKindInCon 0 c)) (#relE env),
|
adamc@626
|
201 namedE = #namedE env,
|
adamc@626
|
202
|
adamc@626
|
203 datatypes = #datatypes env,
|
adamc@626
|
204 constructors = #constructors env
|
adamc@626
|
205 }
|
adamc@626
|
206
|
adamc@626
|
207 fun lookupKRel (env : env) n =
|
adamc@626
|
208 (List.nth (#relK env, n))
|
adamc@626
|
209 handle Subscript => raise UnboundRel n
|
adamc@626
|
210
|
adamc@16
|
211 fun pushCRel (env : env) x k =
|
adamc@626
|
212 {relK = #relK env,
|
adamc@626
|
213
|
adamc@626
|
214 relC = (x, k) :: #relC env,
|
adamc@16
|
215 namedC = IM.map (fn (x, k, co) => (x, k, Option.map lift co)) (#namedC env),
|
adamc@16
|
216
|
adamc@168
|
217 datatypes = #datatypes env,
|
adamc@177
|
218 constructors = #constructors env,
|
adamc@168
|
219
|
adamc@16
|
220 relE = map (fn (x, c) => (x, lift c)) (#relE env),
|
adamc@109
|
221 namedE = IM.map (fn (x, c, eo, s) => (x, lift c, eo, s)) (#namedE env)}
|
adamc@16
|
222
|
adamc@16
|
223 fun lookupCRel (env : env) n =
|
adamc@16
|
224 (List.nth (#relC env, n))
|
adamc@16
|
225 handle Subscript => raise UnboundRel n
|
adamc@16
|
226
|
adamc@16
|
227 fun pushCNamed (env : env) x n k co =
|
adamc@626
|
228 {relK = #relK env,
|
adamc@626
|
229
|
adamc@626
|
230 relC = #relC env,
|
adamc@16
|
231 namedC = IM.insert (#namedC env, n, (x, k, co)),
|
adamc@16
|
232
|
adamc@168
|
233 datatypes = #datatypes env,
|
adamc@177
|
234 constructors = #constructors env,
|
adamc@168
|
235
|
adamc@16
|
236 relE = #relE env,
|
adamc@16
|
237 namedE = #namedE env}
|
adamc@16
|
238
|
adamc@16
|
239 fun lookupCNamed (env : env) n =
|
adamc@16
|
240 case IM.find (#namedC env, n) of
|
adamc@16
|
241 NONE => raise UnboundNamed n
|
adamc@16
|
242 | SOME x => x
|
adamc@16
|
243
|
adamc@192
|
244 fun pushDatatype (env : env) x n xs xncs =
|
adamc@626
|
245 {relK = #relK env,
|
adamc@626
|
246
|
adamc@626
|
247 relC = #relC env,
|
adamc@168
|
248 namedC = #namedC env,
|
adamc@168
|
249
|
adamc@192
|
250 datatypes = IM.insert (#datatypes env, n, (x, xs, xncs)),
|
adamc@182
|
251 constructors = foldl (fn ((x, n', to), constructors) =>
|
adamc@192
|
252 IM.insert (constructors, n', (x, xs, to, n)))
|
adamc@177
|
253 (#constructors env) xncs,
|
adamc@168
|
254
|
adamc@168
|
255 relE = #relE env,
|
adamc@168
|
256 namedE = #namedE env}
|
adamc@168
|
257
|
adamc@168
|
258 fun lookupDatatype (env : env) n =
|
adamc@168
|
259 case IM.find (#datatypes env, n) of
|
adamc@168
|
260 NONE => raise UnboundNamed n
|
adamc@168
|
261 | SOME x => x
|
adamc@168
|
262
|
adamc@177
|
263 fun lookupConstructor (env : env) n =
|
adamc@177
|
264 case IM.find (#constructors env, n) of
|
adamc@177
|
265 NONE => raise UnboundNamed n
|
adamc@177
|
266 | SOME x => x
|
adamc@177
|
267
|
adamc@16
|
268 fun pushERel (env : env) x t =
|
adamc@626
|
269 {relK = #relK env,
|
adamc@626
|
270
|
adamc@626
|
271 relC = #relC env,
|
adamc@16
|
272 namedC = #namedC env,
|
adamc@16
|
273
|
adamc@168
|
274 datatypes = #datatypes env,
|
adamc@177
|
275 constructors = #constructors env,
|
adamc@168
|
276
|
adamc@16
|
277 relE = (x, t) :: #relE env,
|
adamc@16
|
278 namedE = #namedE env}
|
adamc@16
|
279
|
adamc@16
|
280 fun lookupERel (env : env) n =
|
adamc@16
|
281 (List.nth (#relE env, n))
|
adamc@16
|
282 handle Subscript => raise UnboundRel n
|
adamc@16
|
283
|
adamc@109
|
284 fun pushENamed (env : env) x n t eo s =
|
adamc@626
|
285 {relK = #relK env,
|
adamc@626
|
286
|
adamc@626
|
287 relC = #relC env,
|
adamc@16
|
288 namedC = #namedC env,
|
adamc@16
|
289
|
adamc@168
|
290 datatypes = #datatypes env,
|
adamc@177
|
291 constructors = #constructors env,
|
adamc@168
|
292
|
adamc@16
|
293 relE = #relE env,
|
adamc@109
|
294 namedE = IM.insert (#namedE env, n, (x, t, eo, s))}
|
adamc@16
|
295
|
adamc@16
|
296 fun lookupENamed (env : env) n =
|
adamc@16
|
297 case IM.find (#namedE env, n) of
|
adamc@16
|
298 NONE => raise UnboundNamed n
|
adamc@16
|
299 | SOME x => x
|
adamc@16
|
300
|
adamc@163
|
301 fun declBinds env (d, loc) =
|
adamc@16
|
302 case d of
|
adamc@16
|
303 DCon (x, n, k, c) => pushCNamed env x n k (SOME c)
|
adamc@192
|
304 | DDatatype (x, n, xs, xncs) =>
|
adamc@163
|
305 let
|
adamc@192
|
306 val env = pushDatatype env x n xs xncs
|
adamc@163
|
307 val env = pushCNamed env x n (KType, loc) NONE
|
adamc@163
|
308 in
|
adamc@163
|
309 foldl (fn ((x', n', NONE), env) => pushENamed env x' n' (CNamed n, loc) NONE ""
|
adamc@163
|
310 | ((x', n', SOME t), env) => pushENamed env x' n' (TFun (t, (CNamed n, loc)), loc) NONE "")
|
adamc@163
|
311 env xncs
|
adamc@163
|
312 end
|
adamc@109
|
313 | DVal (x, n, t, e, s) => pushENamed env x n t (SOME e) s
|
adamc@126
|
314 | DValRec vis => foldl (fn ((x, n, t, e, s), env) => pushENamed env x n t NONE s) env vis
|
adamc@109
|
315 | DExport _ => env
|
adamc@707
|
316 | DTable (x, n, c, s, _, pc, _, cc) =>
|
adamc@247
|
317 let
|
adamc@705
|
318 val ct = (CFfi ("Basis", "sql_table"), loc)
|
adamc@705
|
319 val ct = (CApp (ct, c), loc)
|
adamc@707
|
320 val ct = (CApp (ct, (CConcat (pc, cc), loc)), loc)
|
adamc@338
|
321 in
|
adamc@705
|
322 pushENamed env x n ct NONE s
|
adamc@338
|
323 end
|
adamc@338
|
324 | DSequence (x, n, s) =>
|
adamc@338
|
325 let
|
adamc@338
|
326 val t = (CFfi ("Basis", "sql_sequence"), loc)
|
adamc@247
|
327 in
|
adamc@247
|
328 pushENamed env x n t NONE s
|
adamc@247
|
329 end
|
adamc@271
|
330 | DDatabase _ => env
|
adamc@461
|
331 | DCookie (x, n, c, s) =>
|
adamc@461
|
332 let
|
adamc@461
|
333 val t = (CApp ((CFfi ("Basis", "http_cookie"), loc), c), loc)
|
adamc@461
|
334 in
|
adamc@461
|
335 pushENamed env x n t NONE s
|
adamc@461
|
336 end
|
adamc@718
|
337 | DStyle (x, n, c, s) =>
|
adamc@718
|
338 let
|
adamc@718
|
339 val t = (CApp ((CFfi ("Basis", "css_class"), loc), c), loc)
|
adamc@718
|
340 in
|
adamc@718
|
341 pushENamed env x n t NONE s
|
adamc@718
|
342 end
|
adamc@16
|
343
|
adamc@193
|
344 fun patBinds env (p, loc) =
|
adamc@193
|
345 case p of
|
adamc@193
|
346 PWild => env
|
adamc@193
|
347 | PVar (x, t) => pushERel env x t
|
adamc@193
|
348 | PPrim _ => env
|
adamc@193
|
349 | PCon (_, _, _, NONE) => env
|
adamc@193
|
350 | PCon (_, _, _, SOME p) => patBinds env p
|
adamc@193
|
351 | PRecord xps => foldl (fn ((_, p, _), env) => patBinds env p) env xps
|
adamc@193
|
352
|
adamc@642
|
353 fun patBindsN (p, loc) =
|
adamc@642
|
354 case p of
|
adamc@642
|
355 PWild => 0
|
adamc@642
|
356 | PVar _ => 1
|
adamc@642
|
357 | PPrim _ => 0
|
adamc@642
|
358 | PCon (_, _, _, NONE) => 0
|
adamc@642
|
359 | PCon (_, _, _, SOME p) => patBindsN p
|
adamc@642
|
360 | PRecord xps => foldl (fn ((_, p, _), count) => count + patBindsN p) 0 xps
|
adamc@642
|
361
|
adamc@16
|
362 end
|