adamc@1200
|
1 (* Copyright (c) 2010, Adam Chlipala
|
adamc@1200
|
2 * All rights reserved.
|
adamc@1200
|
3 *
|
adamc@1200
|
4 * Redistribution and use in source and binary forms, with or without
|
adamc@1200
|
5 * modification, are permitted provided that the following conditions are met:
|
adamc@1200
|
6 *
|
adamc@1200
|
7 * - Redistributions of source code must retain the above copyright notice,
|
adamc@1200
|
8 * this list of conditions and the following disclaimer.
|
adamc@1200
|
9 * - Redistributions in binary form must reproduce the above copyright notice,
|
adamc@1200
|
10 * this list of conditions and the following disclaimer in the documentation
|
adamc@1200
|
11 * and/or other materials provided with the distribution.
|
adamc@1200
|
12 * - The names of contributors may not be used to endorse or promote products
|
adamc@1200
|
13 * derived from this software without specific prior written permission.
|
adamc@1200
|
14 *
|
adamc@1200
|
15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
|
adamc@1200
|
16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
|
adamc@1200
|
17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
|
adamc@1200
|
18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
|
adamc@1200
|
19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
|
adamc@1200
|
20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
|
adamc@1200
|
21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
|
adamc@1200
|
22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
|
adamc@1200
|
23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
|
adamc@1200
|
24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
|
adamc@1200
|
25 * POSSIBILITY OF SUCH DAMAGE.
|
adamc@1200
|
26 *)
|
adamc@1200
|
27
|
adamc@1200
|
28 structure Iflow :> IFLOW = struct
|
adamc@1200
|
29
|
adamc@1200
|
30 open Mono
|
adamc@1200
|
31
|
adamc@1207
|
32 structure IS = IntBinarySet
|
adamc@1202
|
33 structure IM = IntBinaryMap
|
adamc@1202
|
34
|
adamc@1215
|
35 structure SK = struct
|
adamc@1215
|
36 type ord_key = string
|
adamc@1215
|
37 val compare = String.compare
|
adamc@1215
|
38 end
|
adamc@1215
|
39
|
adamc@1215
|
40 structure SS = BinarySetFn(SK)
|
adamc@1215
|
41 structure SM = BinaryMapFn(SK)
|
adamc@1200
|
42
|
adamc@1200
|
43 val writers = ["htmlifyInt_w",
|
adamc@1200
|
44 "htmlifyFloat_w",
|
adamc@1200
|
45 "htmlifyString_w",
|
adamc@1200
|
46 "htmlifyBool_w",
|
adamc@1200
|
47 "htmlifyTime_w",
|
adamc@1200
|
48 "attrifyInt_w",
|
adamc@1200
|
49 "attrifyFloat_w",
|
adamc@1200
|
50 "attrifyString_w",
|
adamc@1200
|
51 "attrifyChar_w",
|
adamc@1200
|
52 "urlifyInt_w",
|
adamc@1200
|
53 "urlifyFloat_w",
|
adamc@1200
|
54 "urlifyString_w",
|
adamc@1213
|
55 "urlifyBool_w",
|
adamc@1213
|
56 "set_cookie"]
|
adamc@1200
|
57
|
adamc@1200
|
58 val writers = SS.addList (SS.empty, writers)
|
adamc@1200
|
59
|
adamc@1200
|
60 type lvar = int
|
adamc@1200
|
61
|
adamc@1215
|
62 datatype func =
|
adamc@1215
|
63 DtCon0 of string
|
adamc@1215
|
64 | DtCon1 of string
|
adamc@1215
|
65 | UnCon of string
|
adamc@1215
|
66 | Other of string
|
adamc@1215
|
67
|
adamc@1200
|
68 datatype exp =
|
adamc@1200
|
69 Const of Prim.t
|
adamc@1200
|
70 | Var of int
|
adamc@1200
|
71 | Lvar of lvar
|
adamc@1215
|
72 | Func of func * exp list
|
adamc@1200
|
73 | Recd of (string * exp) list
|
adamc@1200
|
74 | Proj of exp * string
|
adamc@1200
|
75
|
adamc@1200
|
76 datatype reln =
|
adamc@1207
|
77 Known
|
adamc@1207
|
78 | Sql of string
|
adamc@1215
|
79 | PCon0 of string
|
adamc@1215
|
80 | PCon1 of string
|
adamc@1200
|
81 | Eq
|
adamc@1210
|
82 | Ne
|
adamc@1210
|
83 | Lt
|
adamc@1210
|
84 | Le
|
adamc@1210
|
85 | Gt
|
adamc@1210
|
86 | Ge
|
adamc@1200
|
87
|
adamc@1200
|
88 datatype prop =
|
adamc@1200
|
89 True
|
adamc@1200
|
90 | False
|
adamc@1200
|
91 | Unknown
|
adamc@1200
|
92 | And of prop * prop
|
adamc@1200
|
93 | Or of prop * prop
|
adamc@1200
|
94 | Reln of reln * exp list
|
adamc@1212
|
95 | Cond of exp * prop
|
adamc@1200
|
96
|
adamc@1200
|
97 local
|
adamc@1207
|
98 open Print
|
adamc@1207
|
99 val string = PD.string
|
adamc@1207
|
100 in
|
adamc@1207
|
101
|
adamc@1215
|
102 fun p_func f =
|
adamc@1215
|
103 string (case f of
|
adamc@1215
|
104 DtCon0 s => s
|
adamc@1215
|
105 | DtCon1 s => s
|
adamc@1215
|
106 | UnCon s => "un" ^ s
|
adamc@1215
|
107 | Other s => s)
|
adamc@1215
|
108
|
adamc@1207
|
109 fun p_exp e =
|
adamc@1207
|
110 case e of
|
adamc@1207
|
111 Const p => Prim.p_t p
|
adamc@1207
|
112 | Var n => string ("x" ^ Int.toString n)
|
adamc@1236
|
113 | Lvar n => string ("X" ^ Int.toString n)
|
adamc@1215
|
114 | Func (f, es) => box [p_func f,
|
adamc@1215
|
115 string "(",
|
adamc@1207
|
116 p_list p_exp es,
|
adamc@1207
|
117 string ")"]
|
adamc@1207
|
118 | Recd xes => box [string "{",
|
adamc@1210
|
119 p_list (fn (x, e) => box [string x,
|
adamc@1207
|
120 space,
|
adamc@1207
|
121 string "=",
|
adamc@1207
|
122 space,
|
adamc@1207
|
123 p_exp e]) xes,
|
adamc@1207
|
124 string "}"]
|
adamc@1207
|
125 | Proj (e, x) => box [p_exp e,
|
adamc@1207
|
126 string ("." ^ x)]
|
adamc@1207
|
127
|
adamc@1210
|
128 fun p_bop s es =
|
adamc@1210
|
129 case es of
|
adamc@1210
|
130 [e1, e2] => box [p_exp e1,
|
adamc@1210
|
131 space,
|
adamc@1210
|
132 string s,
|
adamc@1210
|
133 space,
|
adamc@1210
|
134 p_exp e2]
|
adamc@1210
|
135 | _ => raise Fail "Iflow.p_bop"
|
adamc@1210
|
136
|
adamc@1207
|
137 fun p_reln r es =
|
adamc@1207
|
138 case r of
|
adamc@1207
|
139 Known =>
|
adamc@1207
|
140 (case es of
|
adamc@1207
|
141 [e] => box [string "known(",
|
adamc@1207
|
142 p_exp e,
|
adamc@1207
|
143 string ")"]
|
adamc@1207
|
144 | _ => raise Fail "Iflow.p_reln: Known")
|
adamc@1207
|
145 | Sql s => box [string (s ^ "("),
|
adamc@1207
|
146 p_list p_exp es,
|
adamc@1207
|
147 string ")"]
|
adamc@1215
|
148 | PCon0 s => box [string (s ^ "("),
|
adamc@1215
|
149 p_list p_exp es,
|
adamc@1215
|
150 string ")"]
|
adamc@1215
|
151 | PCon1 s => box [string (s ^ "("),
|
adamc@1211
|
152 p_list p_exp es,
|
adamc@1211
|
153 string ")"]
|
adamc@1210
|
154 | Eq => p_bop "=" es
|
adamc@1210
|
155 | Ne => p_bop "<>" es
|
adamc@1210
|
156 | Lt => p_bop "<" es
|
adamc@1210
|
157 | Le => p_bop "<=" es
|
adamc@1210
|
158 | Gt => p_bop ">" es
|
adamc@1210
|
159 | Ge => p_bop ">=" es
|
adamc@1207
|
160
|
adamc@1207
|
161 fun p_prop p =
|
adamc@1207
|
162 case p of
|
adamc@1207
|
163 True => string "True"
|
adamc@1207
|
164 | False => string "False"
|
adamc@1207
|
165 | Unknown => string "??"
|
adamc@1207
|
166 | And (p1, p2) => box [string "(",
|
adamc@1207
|
167 p_prop p1,
|
adamc@1207
|
168 string ")",
|
adamc@1207
|
169 space,
|
adamc@1207
|
170 string "&&",
|
adamc@1207
|
171 space,
|
adamc@1207
|
172 string "(",
|
adamc@1207
|
173 p_prop p2,
|
adamc@1207
|
174 string ")"]
|
adamc@1207
|
175 | Or (p1, p2) => box [string "(",
|
adamc@1207
|
176 p_prop p1,
|
adamc@1207
|
177 string ")",
|
adamc@1207
|
178 space,
|
adamc@1207
|
179 string "||",
|
adamc@1207
|
180 space,
|
adamc@1207
|
181 string "(",
|
adamc@1207
|
182 p_prop p2,
|
adamc@1207
|
183 string ")"]
|
adamc@1207
|
184 | Reln (r, es) => p_reln r es
|
adamc@1212
|
185 | Cond (e, p) => box [string "(",
|
adamc@1212
|
186 p_exp e,
|
adamc@1212
|
187 space,
|
adamc@1212
|
188 string "==",
|
adamc@1212
|
189 space,
|
adamc@1212
|
190 p_prop p,
|
adamc@1212
|
191 string ")"]
|
adamc@1207
|
192
|
adamc@1207
|
193 end
|
adamc@1207
|
194
|
adamc@1200
|
195 fun isKnown e =
|
adamc@1200
|
196 case e of
|
adamc@1200
|
197 Const _ => true
|
adamc@1200
|
198 | Func (_, es) => List.all isKnown es
|
adamc@1200
|
199 | Recd xes => List.all (isKnown o #2) xes
|
adamc@1200
|
200 | Proj (e, _) => isKnown e
|
adamc@1200
|
201 | _ => false
|
adamc@1200
|
202
|
adamc@1236
|
203 fun simplify unif =
|
adamc@1236
|
204 let
|
adamc@1236
|
205 fun simplify e =
|
adamc@1236
|
206 case e of
|
adamc@1236
|
207 Const _ => e
|
adamc@1236
|
208 | Var _ => e
|
adamc@1236
|
209 | Lvar n =>
|
adamc@1236
|
210 (case IM.find (unif, n) of
|
adamc@1236
|
211 NONE => e
|
adamc@1236
|
212 | SOME e => simplify e)
|
adamc@1236
|
213 | Func (f, es) => Func (f, map simplify es)
|
adamc@1236
|
214 | Recd xes => Recd (map (fn (x, e) => (x, simplify e)) xes)
|
adamc@1236
|
215 | Proj (e, s) => Proj (simplify e, s)
|
adamc@1236
|
216 in
|
adamc@1236
|
217 simplify
|
adamc@1236
|
218 end
|
adamc@1200
|
219
|
adamc@1212
|
220 datatype atom =
|
adamc@1212
|
221 AReln of reln * exp list
|
adamc@1212
|
222 | ACond of exp * prop
|
adamc@1212
|
223
|
adamc@1212
|
224 fun p_atom a =
|
adamc@1212
|
225 p_prop (case a of
|
adamc@1212
|
226 AReln x => Reln x
|
adamc@1212
|
227 | ACond x => Cond x)
|
adamc@1212
|
228
|
adamc@1208
|
229 val debug = ref false
|
adamc@1211
|
230
|
adamc@1208
|
231 (* Congruence closure *)
|
adamc@1208
|
232 structure Cc :> sig
|
adamc@1215
|
233 type database
|
adamc@1215
|
234
|
adamc@1215
|
235 exception Contradiction
|
adamc@1215
|
236 exception Undetermined
|
adamc@1215
|
237
|
adamc@1215
|
238 val database : unit -> database
|
adamc@1236
|
239 val clear : database -> unit
|
adamc@1215
|
240
|
adamc@1215
|
241 val assert : database * atom -> unit
|
adamc@1215
|
242 val check : database * atom -> bool
|
adamc@1215
|
243
|
adamc@1215
|
244 val p_database : database Print.printer
|
adamc@1218
|
245
|
adamc@1238
|
246 val builtFrom : database * {UseKnown : bool, Base : exp list, Derived : exp} -> bool
|
adamc@1226
|
247
|
adamc@1226
|
248 val p_repOf : database -> exp Print.printer
|
adamc@1208
|
249 end = struct
|
adamc@1208
|
250
|
adamc@1215
|
251 exception Contradiction
|
adamc@1215
|
252 exception Undetermined
|
adamc@1208
|
253
|
adamc@1215
|
254 structure CM = BinaryMapFn(struct
|
adamc@1215
|
255 type ord_key = Prim.t
|
adamc@1215
|
256 val compare = Prim.compare
|
adamc@1215
|
257 end)
|
adamc@1208
|
258
|
adamc@1215
|
259 datatype node = Node of {Rep : node ref option ref,
|
adamc@1215
|
260 Cons : node ref SM.map ref,
|
adamc@1215
|
261 Variety : variety,
|
adamc@1215
|
262 Known : bool ref}
|
adamc@1208
|
263
|
adamc@1215
|
264 and variety =
|
adamc@1215
|
265 Dt0 of string
|
adamc@1215
|
266 | Dt1 of string * node ref
|
adamc@1215
|
267 | Prim of Prim.t
|
adamc@1221
|
268 | Recrd of node ref SM.map ref * bool
|
adamc@1215
|
269 | Nothing
|
adamc@1208
|
270
|
adamc@1215
|
271 type representative = node ref
|
adamc@1215
|
272
|
adamc@1215
|
273 type database = {Vars : representative IM.map ref,
|
adamc@1215
|
274 Consts : representative CM.map ref,
|
adamc@1215
|
275 Con0s : representative SM.map ref,
|
adamc@1215
|
276 Records : (representative SM.map * representative) list ref,
|
adamc@1229
|
277 Funcs : ((string * representative list) * representative) list ref}
|
adamc@1215
|
278
|
adamc@1215
|
279 fun database () = {Vars = ref IM.empty,
|
adamc@1215
|
280 Consts = ref CM.empty,
|
adamc@1215
|
281 Con0s = ref SM.empty,
|
adamc@1215
|
282 Records = ref [],
|
adamc@1215
|
283 Funcs = ref []}
|
adamc@1215
|
284
|
adamc@1236
|
285 fun clear (t : database) = (#Vars t := IM.empty;
|
adamc@1236
|
286 #Consts t := CM.empty;
|
adamc@1236
|
287 #Con0s t := SM.empty;
|
adamc@1236
|
288 #Records t := [];
|
adamc@1236
|
289 #Funcs t := [])
|
adamc@1236
|
290
|
adamc@1215
|
291 fun unNode n =
|
adamc@1215
|
292 case !n of
|
adamc@1215
|
293 Node r => r
|
adamc@1215
|
294
|
adamc@1215
|
295 open Print
|
adamc@1215
|
296 val string = PD.string
|
adamc@1215
|
297 val newline = PD.newline
|
adamc@1215
|
298
|
adamc@1215
|
299 fun p_rep n =
|
adamc@1215
|
300 case !(#Rep (unNode n)) of
|
adamc@1215
|
301 SOME n => p_rep n
|
adamc@1215
|
302 | NONE =>
|
adamc@1243
|
303 box [(*string (Int.toString (Unsafe.cast n) ^ ":"),
|
adamc@1243
|
304 space,*)
|
adamc@1221
|
305 case #Variety (unNode n) of
|
adamc@1221
|
306 Nothing => string "?"
|
adamc@1221
|
307 | Dt0 s => string ("Dt0(" ^ s ^ ")")
|
adamc@1221
|
308 | Dt1 (s, n) => box[string ("Dt1(" ^ s ^ ","),
|
adamc@1221
|
309 space,
|
adamc@1221
|
310 p_rep n,
|
adamc@1221
|
311 string ")"]
|
adamc@1221
|
312 | Prim p => Prim.p_t p
|
adamc@1221
|
313 | Recrd (ref m, b) => box [string "{",
|
adamc@1221
|
314 p_list (fn (x, n) => box [string x,
|
adamc@1221
|
315 space,
|
adamc@1221
|
316 string "=",
|
adamc@1221
|
317 space,
|
adamc@1221
|
318 p_rep n]) (SM.listItemsi m),
|
adamc@1221
|
319 string "}",
|
adamc@1221
|
320 if b then
|
adamc@1221
|
321 box [space,
|
adamc@1221
|
322 string "(complete)"]
|
adamc@1221
|
323 else
|
adamc@1226
|
324 box []]]
|
adamc@1215
|
325
|
adamc@1215
|
326 fun p_database (db : database) =
|
adamc@1215
|
327 box [string "Vars:",
|
adamc@1215
|
328 newline,
|
adamc@1215
|
329 p_list_sep newline (fn (i, n) => box [string ("x" ^ Int.toString i),
|
adamc@1215
|
330 space,
|
adamc@1215
|
331 string "=",
|
adamc@1215
|
332 space,
|
adamc@1218
|
333 p_rep n,
|
adamc@1218
|
334 if !(#Known (unNode n)) then
|
adamc@1218
|
335 box [space,
|
adamc@1218
|
336 string "(known)"]
|
adamc@1218
|
337 else
|
adamc@1218
|
338 box []]) (IM.listItemsi (!(#Vars db)))]
|
adamc@1215
|
339
|
adamc@1215
|
340 fun repOf (n : representative) : representative =
|
adamc@1215
|
341 case !(#Rep (unNode n)) of
|
adamc@1215
|
342 NONE => n
|
adamc@1215
|
343 | SOME r =>
|
adamc@1215
|
344 let
|
adamc@1215
|
345 val r = repOf r
|
adamc@1215
|
346 in
|
adamc@1215
|
347 #Rep (unNode n) := SOME r;
|
adamc@1215
|
348 r
|
adamc@1215
|
349 end
|
adamc@1215
|
350
|
adamc@1215
|
351 fun markKnown r =
|
adamc@1221
|
352 let
|
adamc@1221
|
353 val r = repOf r
|
adamc@1221
|
354 in
|
adamc@1221
|
355 (*Print.preface ("markKnown", p_rep r);*)
|
adamc@1221
|
356 if !(#Known (unNode r)) then
|
adamc@1221
|
357 ()(*TextIO.print "Already known\n"*)
|
adamc@1221
|
358 else
|
adamc@1221
|
359 (#Known (unNode r) := true;
|
adamc@1221
|
360 SM.app markKnown (!(#Cons (unNode r)));
|
adamc@1221
|
361 case #Variety (unNode r) of
|
adamc@1221
|
362 Dt1 (_, r) => markKnown r
|
adamc@1221
|
363 | Recrd (xes, _) => SM.app markKnown (!xes)
|
adamc@1221
|
364 | _ => ())
|
adamc@1221
|
365 end
|
adamc@1215
|
366
|
adamc@1215
|
367 fun representative (db : database, e) =
|
adamc@1208
|
368 let
|
adamc@1215
|
369 fun rep e =
|
adamc@1215
|
370 case e of
|
adamc@1215
|
371 Const p => (case CM.find (!(#Consts db), p) of
|
adamc@1215
|
372 SOME r => repOf r
|
adamc@1215
|
373 | NONE =>
|
adamc@1215
|
374 let
|
adamc@1215
|
375 val r = ref (Node {Rep = ref NONE,
|
adamc@1215
|
376 Cons = ref SM.empty,
|
adamc@1215
|
377 Variety = Prim p,
|
adamc@1219
|
378 Known = ref true})
|
adamc@1215
|
379 in
|
adamc@1215
|
380 #Consts db := CM.insert (!(#Consts db), p, r);
|
adamc@1215
|
381 r
|
adamc@1215
|
382 end)
|
adamc@1215
|
383 | Var n => (case IM.find (!(#Vars db), n) of
|
adamc@1215
|
384 SOME r => repOf r
|
adamc@1215
|
385 | NONE =>
|
adamc@1215
|
386 let
|
adamc@1215
|
387 val r = ref (Node {Rep = ref NONE,
|
adamc@1215
|
388 Cons = ref SM.empty,
|
adamc@1215
|
389 Variety = Nothing,
|
adamc@1215
|
390 Known = ref false})
|
adamc@1215
|
391 in
|
adamc@1215
|
392 #Vars db := IM.insert (!(#Vars db), n, r);
|
adamc@1215
|
393 r
|
adamc@1215
|
394 end)
|
adamc@1236
|
395 | Lvar _ => raise Undetermined
|
adamc@1215
|
396 | Func (DtCon0 f, []) => (case SM.find (!(#Con0s db), f) of
|
adamc@1215
|
397 SOME r => repOf r
|
adamc@1215
|
398 | NONE =>
|
adamc@1215
|
399 let
|
adamc@1215
|
400 val r = ref (Node {Rep = ref NONE,
|
adamc@1215
|
401 Cons = ref SM.empty,
|
adamc@1215
|
402 Variety = Dt0 f,
|
adamc@1218
|
403 Known = ref true})
|
adamc@1215
|
404 in
|
adamc@1215
|
405 #Con0s db := SM.insert (!(#Con0s db), f, r);
|
adamc@1215
|
406 r
|
adamc@1215
|
407 end)
|
adamc@1215
|
408 | Func (DtCon0 _, _) => raise Fail "Iflow.rep: DtCon0"
|
adamc@1215
|
409 | Func (DtCon1 f, [e]) =>
|
adamc@1215
|
410 let
|
adamc@1215
|
411 val r = rep e
|
adamc@1215
|
412 in
|
adamc@1215
|
413 case SM.find (!(#Cons (unNode r)), f) of
|
adamc@1215
|
414 SOME r => repOf r
|
adamc@1215
|
415 | NONE =>
|
adamc@1215
|
416 let
|
adamc@1215
|
417 val r' = ref (Node {Rep = ref NONE,
|
adamc@1215
|
418 Cons = ref SM.empty,
|
adamc@1215
|
419 Variety = Dt1 (f, r),
|
adamc@1221
|
420 Known = ref (!(#Known (unNode r)))})
|
adamc@1215
|
421 in
|
adamc@1215
|
422 #Cons (unNode r) := SM.insert (!(#Cons (unNode r)), f, r');
|
adamc@1215
|
423 r'
|
adamc@1215
|
424 end
|
adamc@1215
|
425 end
|
adamc@1215
|
426 | Func (DtCon1 _, _) => raise Fail "Iflow.rep: DtCon1"
|
adamc@1215
|
427 | Func (UnCon f, [e]) =>
|
adamc@1215
|
428 let
|
adamc@1215
|
429 val r = rep e
|
adamc@1215
|
430 in
|
adamc@1215
|
431 case #Variety (unNode r) of
|
adamc@1215
|
432 Dt1 (f', n) => if f' = f then
|
adamc@1215
|
433 repOf n
|
adamc@1215
|
434 else
|
adamc@1215
|
435 raise Contradiction
|
adamc@1215
|
436 | Nothing =>
|
adamc@1215
|
437 let
|
adamc@1215
|
438 val cons = ref SM.empty
|
adamc@1215
|
439 val r' = ref (Node {Rep = ref NONE,
|
adamc@1215
|
440 Cons = cons,
|
adamc@1215
|
441 Variety = Nothing,
|
adamc@1221
|
442 Known = ref (!(#Known (unNode r)))})
|
adamc@1215
|
443
|
adamc@1215
|
444 val r'' = ref (Node {Rep = ref NONE,
|
adamc@1215
|
445 Cons = #Cons (unNode r),
|
adamc@1215
|
446 Variety = Dt1 (f, r'),
|
adamc@1215
|
447 Known = #Known (unNode r)})
|
adamc@1215
|
448 in
|
adamc@1215
|
449 cons := SM.insert (!cons, f, r'');
|
adamc@1215
|
450 #Rep (unNode r) := SOME r'';
|
adamc@1215
|
451 r'
|
adamc@1215
|
452 end
|
adamc@1215
|
453 | _ => raise Contradiction
|
adamc@1215
|
454 end
|
adamc@1215
|
455 | Func (UnCon _, _) => raise Fail "Iflow.rep: UnCon"
|
adamc@1215
|
456 | Func (Other f, es) =>
|
adamc@1215
|
457 let
|
adamc@1215
|
458 val rs = map rep es
|
adamc@1215
|
459 in
|
adamc@1215
|
460 case List.find (fn (x : string * representative list, _) => x = (f, rs)) (!(#Funcs db)) of
|
adamc@1215
|
461 NONE =>
|
adamc@1215
|
462 let
|
adamc@1215
|
463 val r = ref (Node {Rep = ref NONE,
|
adamc@1215
|
464 Cons = ref SM.empty,
|
adamc@1215
|
465 Variety = Nothing,
|
adamc@1215
|
466 Known = ref false})
|
adamc@1215
|
467 in
|
adamc@1215
|
468 #Funcs db := ((f, rs), r) :: (!(#Funcs db));
|
adamc@1215
|
469 r
|
adamc@1215
|
470 end
|
adamc@1215
|
471 | SOME (_, r) => repOf r
|
adamc@1215
|
472 end
|
adamc@1215
|
473 | Recd xes =>
|
adamc@1215
|
474 let
|
adamc@1215
|
475 val xes = map (fn (x, e) => (x, rep e)) xes
|
adamc@1215
|
476 val len = length xes
|
adamc@1215
|
477 in
|
adamc@1215
|
478 case List.find (fn (xes', _) =>
|
adamc@1215
|
479 SM.numItems xes' = len
|
adamc@1215
|
480 andalso List.all (fn (x, n) =>
|
adamc@1215
|
481 case SM.find (xes', x) of
|
adamc@1215
|
482 NONE => false
|
adamc@1215
|
483 | SOME n' => n = repOf n') xes)
|
adamc@1215
|
484 (!(#Records db)) of
|
adamc@1215
|
485 SOME (_, r) => repOf r
|
adamc@1215
|
486 | NONE =>
|
adamc@1215
|
487 let
|
adamc@1215
|
488 val xes = foldl SM.insert' SM.empty xes
|
adamc@1215
|
489
|
adamc@1215
|
490 val r' = ref (Node {Rep = ref NONE,
|
adamc@1215
|
491 Cons = ref SM.empty,
|
adamc@1221
|
492 Variety = Recrd (ref xes, true),
|
adamc@1215
|
493 Known = ref false})
|
adamc@1215
|
494 in
|
adamc@1215
|
495 #Records db := (xes, r') :: (!(#Records db));
|
adamc@1215
|
496 r'
|
adamc@1215
|
497 end
|
adamc@1215
|
498 end
|
adamc@1215
|
499 | Proj (e, f) =>
|
adamc@1215
|
500 let
|
adamc@1215
|
501 val r = rep e
|
adamc@1215
|
502 in
|
adamc@1215
|
503 case #Variety (unNode r) of
|
adamc@1221
|
504 Recrd (xes, _) =>
|
adamc@1215
|
505 (case SM.find (!xes, f) of
|
adamc@1215
|
506 SOME r => repOf r
|
adamc@1216
|
507 | NONE => let
|
adamc@1215
|
508 val r = ref (Node {Rep = ref NONE,
|
adamc@1215
|
509 Cons = ref SM.empty,
|
adamc@1215
|
510 Variety = Nothing,
|
adamc@1221
|
511 Known = ref (!(#Known (unNode r)))})
|
adamc@1215
|
512 in
|
adamc@1215
|
513 xes := SM.insert (!xes, f, r);
|
adamc@1215
|
514 r
|
adamc@1215
|
515 end)
|
adamc@1215
|
516 | Nothing =>
|
adamc@1215
|
517 let
|
adamc@1215
|
518 val r' = ref (Node {Rep = ref NONE,
|
adamc@1215
|
519 Cons = ref SM.empty,
|
adamc@1215
|
520 Variety = Nothing,
|
adamc@1221
|
521 Known = ref (!(#Known (unNode r)))})
|
adamc@1215
|
522
|
adamc@1215
|
523 val r'' = ref (Node {Rep = ref NONE,
|
adamc@1215
|
524 Cons = #Cons (unNode r),
|
adamc@1221
|
525 Variety = Recrd (ref (SM.insert (SM.empty, f, r')), false),
|
adamc@1215
|
526 Known = #Known (unNode r)})
|
adamc@1215
|
527 in
|
adamc@1215
|
528 #Rep (unNode r) := SOME r'';
|
adamc@1215
|
529 r'
|
adamc@1215
|
530 end
|
adamc@1215
|
531 | _ => raise Contradiction
|
adamc@1215
|
532 end
|
adamc@1208
|
533 in
|
adamc@1215
|
534 rep e
|
adamc@1208
|
535 end
|
adamc@1208
|
536
|
adamc@1226
|
537 fun p_repOf db e = p_rep (representative (db, e))
|
adamc@1226
|
538
|
adamc@1215
|
539 fun assert (db, a) =
|
adamc@1243
|
540 let
|
adamc@1243
|
541 fun markEq (r1, r2) =
|
adamc@1215
|
542 let
|
adamc@1243
|
543 val r1 = repOf r1
|
adamc@1243
|
544 val r2 = repOf r2
|
adamc@1215
|
545 in
|
adamc@1243
|
546 if r1 = r2 then
|
adamc@1243
|
547 ()
|
adamc@1243
|
548 else case (#Variety (unNode r1), #Variety (unNode r2)) of
|
adamc@1243
|
549 (Prim p1, Prim p2) => if Prim.equal (p1, p2) then
|
adamc@1243
|
550 ()
|
adamc@1243
|
551 else
|
adamc@1243
|
552 raise Contradiction
|
adamc@1243
|
553 | (Dt0 f1, Dt0 f2) => if f1 = f2 then
|
adamc@1243
|
554 ()
|
adamc@1243
|
555 else
|
adamc@1243
|
556 raise Contradiction
|
adamc@1243
|
557 | (Dt1 (f1, r1), Dt1 (f2, r2)) => if f1 = f2 then
|
adamc@1243
|
558 markEq (r1, r2)
|
adamc@1243
|
559 else
|
adamc@1243
|
560 raise Contradiction
|
adamc@1243
|
561 | (Recrd (xes1, _), Recrd (xes2, _)) =>
|
adamc@1243
|
562 let
|
adamc@1243
|
563 fun unif (xes1, xes2) =
|
adamc@1243
|
564 SM.appi (fn (x, r1) =>
|
adamc@1243
|
565 case SM.find (!xes2, x) of
|
adamc@1243
|
566 NONE => xes2 := SM.insert (!xes2, x, r1)
|
adamc@1243
|
567 | SOME r2 => markEq (r1, r2)) (!xes1)
|
adamc@1243
|
568 in
|
adamc@1243
|
569 unif (xes1, xes2);
|
adamc@1243
|
570 unif (xes2, xes1)
|
adamc@1243
|
571 end
|
adamc@1243
|
572 | (Nothing, _) => mergeNodes (r1, r2)
|
adamc@1243
|
573 | (_, Nothing) => mergeNodes (r2, r1)
|
adamc@1243
|
574 | _ => raise Contradiction
|
adamc@1215
|
575 end
|
adamc@1243
|
576
|
adamc@1243
|
577 and mergeNodes (r1, r2) =
|
adamc@1243
|
578 (#Rep (unNode r1) := SOME r2;
|
adamc@1243
|
579 if !(#Known (unNode r1)) then
|
adamc@1243
|
580 markKnown r2
|
adamc@1243
|
581 else
|
adamc@1243
|
582 ();
|
adamc@1243
|
583 if !(#Known (unNode r2)) then
|
adamc@1243
|
584 markKnown r1
|
adamc@1243
|
585 else
|
adamc@1243
|
586 ();
|
adamc@1243
|
587 #Cons (unNode r2) := SM.unionWith #1 (!(#Cons (unNode r2)), !(#Cons (unNode r1)));
|
adamc@1243
|
588
|
adamc@1243
|
589 compactFuncs ())
|
adamc@1243
|
590
|
adamc@1243
|
591 and compactFuncs () =
|
adamc@1215
|
592 let
|
adamc@1243
|
593 fun loop funcs =
|
adamc@1243
|
594 case funcs of
|
adamc@1243
|
595 [] => []
|
adamc@1243
|
596 | (fr as ((f, rs), r)) :: rest =>
|
adamc@1243
|
597 let
|
adamc@1243
|
598 val rest = List.filter (fn ((f' : string, rs'), r') =>
|
adamc@1243
|
599 if f' = f
|
adamc@1243
|
600 andalso ListPair.allEq (fn (r1, r2) =>
|
adamc@1243
|
601 repOf r1 = repOf r2)
|
adamc@1243
|
602 (rs, rs') then
|
adamc@1243
|
603 (markEq (r, r');
|
adamc@1243
|
604 false)
|
adamc@1243
|
605 else
|
adamc@1243
|
606 true) rest
|
adamc@1243
|
607 in
|
adamc@1243
|
608 fr :: loop rest
|
adamc@1243
|
609 end
|
adamc@1215
|
610 in
|
adamc@1243
|
611 #Funcs db := loop (!(#Funcs db))
|
adamc@1243
|
612 end
|
adamc@1243
|
613 in
|
adamc@1243
|
614 case a of
|
adamc@1243
|
615 ACond _ => ()
|
adamc@1243
|
616 | AReln x =>
|
adamc@1243
|
617 case x of
|
adamc@1243
|
618 (Known, [e]) =>
|
adamc@1243
|
619 ((*Print.prefaces "Before" [("e", p_exp e),
|
adamc@1243
|
620 ("db", p_database db)];*)
|
adamc@1243
|
621 markKnown (representative (db, e))(*;
|
adamc@1243
|
622 Print.prefaces "After" [("e", p_exp e),
|
adamc@1243
|
623 ("db", p_database db)]*))
|
adamc@1243
|
624 | (PCon0 f, [e]) =>
|
adamc@1243
|
625 let
|
adamc@1243
|
626 val r = representative (db, e)
|
adamc@1243
|
627 in
|
adamc@1243
|
628 case #Variety (unNode r) of
|
adamc@1243
|
629 Dt0 f' => if f = f' then
|
adamc@1243
|
630 ()
|
adamc@1243
|
631 else
|
adamc@1243
|
632 raise Contradiction
|
adamc@1243
|
633 | Nothing =>
|
adamc@1243
|
634 (case SM.find (!(#Con0s db), f) of
|
adamc@1243
|
635 SOME r' => markEq (r, r')
|
adamc@1243
|
636 | NONE =>
|
adamc@1243
|
637 let
|
adamc@1243
|
638 val r' = ref (Node {Rep = ref NONE,
|
adamc@1243
|
639 Cons = ref SM.empty,
|
adamc@1243
|
640 Variety = Dt0 f,
|
adamc@1243
|
641 Known = ref false})
|
adamc@1243
|
642 in
|
adamc@1243
|
643 #Rep (unNode r) := SOME r';
|
adamc@1243
|
644 #Con0s db := SM.insert (!(#Con0s db), f, r')
|
adamc@1243
|
645 end)
|
adamc@1243
|
646 | _ => raise Contradiction
|
adamc@1243
|
647 end
|
adamc@1243
|
648 | (PCon1 f, [e]) =>
|
adamc@1243
|
649 let
|
adamc@1243
|
650 val r = representative (db, e)
|
adamc@1243
|
651 in
|
adamc@1243
|
652 case #Variety (unNode r) of
|
adamc@1243
|
653 Dt1 (f', e') => if f = f' then
|
adamc@1243
|
654 ()
|
adamc@1243
|
655 else
|
adamc@1243
|
656 raise Contradiction
|
adamc@1243
|
657 | Nothing =>
|
adamc@1243
|
658 let
|
adamc@1243
|
659 val r'' = ref (Node {Rep = ref NONE,
|
adamc@1243
|
660 Cons = ref SM.empty,
|
adamc@1243
|
661 Variety = Nothing,
|
adamc@1243
|
662 Known = ref (!(#Known (unNode r)))})
|
adamc@1214
|
663
|
adamc@1243
|
664 val r' = ref (Node {Rep = ref NONE,
|
adamc@1243
|
665 Cons = ref SM.empty,
|
adamc@1243
|
666 Variety = Dt1 (f, r''),
|
adamc@1243
|
667 Known = #Known (unNode r)})
|
adamc@1243
|
668 in
|
adamc@1243
|
669 #Rep (unNode r) := SOME r'
|
adamc@1243
|
670 end
|
adamc@1243
|
671 | _ => raise Contradiction
|
adamc@1243
|
672 end
|
adamc@1243
|
673 | (Eq, [e1, e2]) =>
|
adamc@1215
|
674 markEq (representative (db, e1), representative (db, e2))
|
adamc@1243
|
675 | _ => ()
|
adamc@1243
|
676 end
|
adamc@1214
|
677
|
adamc@1215
|
678 fun check (db, a) =
|
adamc@1215
|
679 case a of
|
adamc@1215
|
680 ACond _ => false
|
adamc@1215
|
681 | AReln x =>
|
adamc@1215
|
682 case x of
|
adamc@1221
|
683 (Known, [e]) =>
|
adamc@1221
|
684 let
|
adamc@1221
|
685 fun isKnown r =
|
adamc@1221
|
686 let
|
adamc@1221
|
687 val r = repOf r
|
adamc@1221
|
688 in
|
adamc@1221
|
689 !(#Known (unNode r))
|
adamc@1221
|
690 orelse case #Variety (unNode r) of
|
adamc@1221
|
691 Dt1 (_, r) => isKnown r
|
adamc@1221
|
692 | Recrd (xes, true) => List.all isKnown (SM.listItems (!xes))
|
adamc@1221
|
693 | _ => false
|
adamc@1221
|
694 end
|
adamc@1221
|
695
|
adamc@1221
|
696 val r = representative (db, e)
|
adamc@1221
|
697 in
|
adamc@1221
|
698 isKnown r
|
adamc@1221
|
699 end
|
adamc@1215
|
700 | (PCon0 f, [e]) =>
|
adamc@1215
|
701 (case #Variety (unNode (representative (db, e))) of
|
adamc@1215
|
702 Dt0 f' => f' = f
|
adamc@1215
|
703 | _ => false)
|
adamc@1215
|
704 | (PCon1 f, [e]) =>
|
adamc@1215
|
705 (case #Variety (unNode (representative (db, e))) of
|
adamc@1215
|
706 Dt1 (f', _) => f' = f
|
adamc@1215
|
707 | _ => false)
|
adamc@1215
|
708 | (Eq, [e1, e2]) =>
|
adamc@1214
|
709 let
|
adamc@1215
|
710 val r1 = representative (db, e1)
|
adamc@1215
|
711 val r2 = representative (db, e2)
|
adamc@1214
|
712 in
|
adamc@1215
|
713 repOf r1 = repOf r2
|
adamc@1214
|
714 end
|
adamc@1215
|
715 | _ => false
|
adamc@1212
|
716
|
adamc@1238
|
717 fun builtFrom (db, {UseKnown = uk, Base = bs, Derived = d}) =
|
adamc@1218
|
718 let
|
adamc@1218
|
719 val bs = map (fn b => representative (db, b)) bs
|
adamc@1218
|
720
|
adamc@1218
|
721 fun loop d =
|
adamc@1218
|
722 let
|
adamc@1218
|
723 val d = repOf d
|
adamc@1218
|
724 in
|
adamc@1238
|
725 (uk andalso !(#Known (unNode d)))
|
adamc@1238
|
726 orelse List.exists (fn b => repOf b = d) bs
|
adamc@1218
|
727 orelse case #Variety (unNode d) of
|
adamc@1218
|
728 Dt0 _ => true
|
adamc@1218
|
729 | Dt1 (_, d) => loop d
|
adamc@1218
|
730 | Prim _ => true
|
adamc@1221
|
731 | Recrd (xes, _) => List.all loop (SM.listItems (!xes))
|
adamc@1218
|
732 | Nothing => false
|
adamc@1218
|
733 end
|
adamc@1238
|
734
|
adamc@1238
|
735 fun decomp e =
|
adamc@1238
|
736 case e of
|
adamc@1238
|
737 Func (Other _, es) => List.all decomp es
|
adamc@1238
|
738 | _ => loop (representative (db, e))
|
adamc@1218
|
739 in
|
adamc@1238
|
740 decomp d
|
adamc@1218
|
741 end
|
adamc@1218
|
742
|
adamc@1208
|
743 end
|
adamc@1208
|
744
|
adamc@1226
|
745 val tabs = ref (SM.empty : (string list * string list list) SM.map)
|
adamc@1226
|
746
|
adamc@1231
|
747 fun ccOf hyps =
|
adamc@1231
|
748 let
|
adamc@1231
|
749 val cc = Cc.database ()
|
adamc@1231
|
750 val () = app (fn a => Cc.assert (cc, a)) hyps
|
adamc@1231
|
751
|
adamc@1231
|
752 (* Take advantage of table key information *)
|
adamc@1231
|
753 fun findKeys hyps =
|
adamc@1231
|
754 case hyps of
|
adamc@1231
|
755 [] => ()
|
adamc@1231
|
756 | AReln (Sql tab, [r1]) :: hyps =>
|
adamc@1231
|
757 (case SM.find (!tabs, tab) of
|
adamc@1231
|
758 NONE => findKeys hyps
|
adamc@1231
|
759 | SOME (_, []) => findKeys hyps
|
adamc@1231
|
760 | SOME (_, ks) =>
|
adamc@1231
|
761 let
|
adamc@1231
|
762 fun finder hyps =
|
adamc@1231
|
763 case hyps of
|
adamc@1231
|
764 [] => ()
|
adamc@1231
|
765 | AReln (Sql tab', [r2]) :: hyps =>
|
adamc@1231
|
766 (if tab' = tab andalso
|
adamc@1231
|
767 List.exists (List.all (fn f =>
|
adamc@1231
|
768 let
|
adamc@1231
|
769 val r =
|
adamc@1231
|
770 Cc.check (cc,
|
adamc@1231
|
771 AReln (Eq, [Proj (r1, f),
|
adamc@1231
|
772 Proj (r2, f)]))
|
adamc@1231
|
773 in
|
adamc@1231
|
774 (*Print.prefaces "Fs"
|
adamc@1231
|
775 [("tab",
|
adamc@1231
|
776 Print.PD.string tab),
|
adamc@1231
|
777 ("r1",
|
adamc@1231
|
778 p_exp (Proj (r1, f))),
|
adamc@1231
|
779 ("r2",
|
adamc@1231
|
780 p_exp (Proj (r2, f))),
|
adamc@1231
|
781 ("r",
|
adamc@1231
|
782 Print.PD.string
|
adamc@1231
|
783 (Bool.toString r))];*)
|
adamc@1231
|
784 r
|
adamc@1231
|
785 end)) ks then
|
adamc@1231
|
786 ((*Print.prefaces "Key match" [("tab", Print.PD.string tab),
|
adamc@1231
|
787 ("r1", p_exp r1),
|
adamc@1231
|
788 ("r2", p_exp r2),
|
adamc@1231
|
789 ("rp1", Cc.p_repOf cc r1),
|
adamc@1231
|
790 ("rp2", Cc.p_repOf cc r2)];*)
|
adamc@1231
|
791 Cc.assert (cc, AReln (Eq, [r1, r2])))
|
adamc@1231
|
792 else
|
adamc@1231
|
793 ();
|
adamc@1231
|
794 finder hyps)
|
adamc@1231
|
795 | _ :: hyps => finder hyps
|
adamc@1231
|
796 in
|
adamc@1231
|
797 finder hyps;
|
adamc@1231
|
798 findKeys hyps
|
adamc@1231
|
799 end)
|
adamc@1231
|
800 | _ :: hyps => findKeys hyps
|
adamc@1231
|
801 in
|
adamc@1231
|
802 findKeys hyps;
|
adamc@1231
|
803 cc
|
adamc@1231
|
804 end
|
adamc@1231
|
805
|
adamc@1200
|
806 fun patCon pc =
|
adamc@1200
|
807 case pc of
|
adamc@1200
|
808 PConVar n => "C" ^ Int.toString n
|
adamc@1200
|
809 | PConFfi {mod = m, datatyp = d, con = c, ...} => m ^ "." ^ d ^ "." ^ c
|
adamc@1200
|
810
|
adamc@1200
|
811 datatype chunk =
|
adamc@1200
|
812 String of string
|
adamc@1200
|
813 | Exp of Mono.exp
|
adamc@1200
|
814
|
adamc@1200
|
815 fun chunkify e =
|
adamc@1200
|
816 case #1 e of
|
adamc@1200
|
817 EPrim (Prim.String s) => [String s]
|
adamc@1207
|
818 | EStrcat (e1, e2) =>
|
adamc@1207
|
819 let
|
adamc@1207
|
820 val chs1 = chunkify e1
|
adamc@1207
|
821 val chs2 = chunkify e2
|
adamc@1207
|
822 in
|
adamc@1207
|
823 case chs2 of
|
adamc@1207
|
824 String s2 :: chs2' =>
|
adamc@1207
|
825 (case List.last chs1 of
|
adamc@1207
|
826 String s1 => List.take (chs1, length chs1 - 1) @ String (s1 ^ s2) :: chs2'
|
adamc@1207
|
827 | _ => chs1 @ chs2)
|
adamc@1207
|
828 | _ => chs1 @ chs2
|
adamc@1207
|
829 end
|
adamc@1200
|
830 | _ => [Exp e]
|
adamc@1200
|
831
|
adamc@1201
|
832 type 'a parser = chunk list -> ('a * chunk list) option
|
adamc@1201
|
833
|
adamc@1201
|
834 fun always v chs = SOME (v, chs)
|
adamc@1201
|
835
|
adamc@1202
|
836 fun parse p s =
|
adamc@1202
|
837 case p (chunkify s) of
|
adamc@1201
|
838 SOME (v, []) => SOME v
|
adamc@1201
|
839 | _ => NONE
|
adamc@1201
|
840
|
adamc@1201
|
841 fun const s chs =
|
adamc@1201
|
842 case chs of
|
adamc@1201
|
843 String s' :: chs => if String.isPrefix s s' then
|
adamc@1201
|
844 SOME ((), if size s = size s' then
|
adamc@1201
|
845 chs
|
adamc@1201
|
846 else
|
adamc@1201
|
847 String (String.extract (s', size s, NONE)) :: chs)
|
adamc@1201
|
848 else
|
adamc@1201
|
849 NONE
|
adamc@1201
|
850 | _ => NONE
|
adamc@1201
|
851
|
adamc@1201
|
852 fun follow p1 p2 chs =
|
adamc@1201
|
853 case p1 chs of
|
adamc@1201
|
854 NONE => NONE
|
adamc@1201
|
855 | SOME (v1, chs) =>
|
adamc@1201
|
856 case p2 chs of
|
adamc@1201
|
857 NONE => NONE
|
adamc@1201
|
858 | SOME (v2, chs) => SOME ((v1, v2), chs)
|
adamc@1201
|
859
|
adamc@1201
|
860 fun wrap p f chs =
|
adamc@1201
|
861 case p chs of
|
adamc@1201
|
862 NONE => NONE
|
adamc@1201
|
863 | SOME (v, chs) => SOME (f v, chs)
|
adamc@1201
|
864
|
adamc@1209
|
865 fun wrapP p f chs =
|
adamc@1209
|
866 case p chs of
|
adamc@1209
|
867 NONE => NONE
|
adamc@1209
|
868 | SOME (v, chs) =>
|
adamc@1209
|
869 case f v of
|
adamc@1209
|
870 NONE => NONE
|
adamc@1209
|
871 | SOME r => SOME (r, chs)
|
adamc@1209
|
872
|
adamc@1201
|
873 fun alt p1 p2 chs =
|
adamc@1201
|
874 case p1 chs of
|
adamc@1201
|
875 NONE => p2 chs
|
adamc@1201
|
876 | v => v
|
adamc@1201
|
877
|
adamc@1207
|
878 fun altL ps =
|
adamc@1207
|
879 case rev ps of
|
adamc@1207
|
880 [] => (fn _ => NONE)
|
adamc@1207
|
881 | p :: ps =>
|
adamc@1207
|
882 foldl (fn (p1, p2) => alt p1 p2) p ps
|
adamc@1207
|
883
|
adamc@1204
|
884 fun opt p chs =
|
adamc@1204
|
885 case p chs of
|
adamc@1204
|
886 NONE => SOME (NONE, chs)
|
adamc@1204
|
887 | SOME (v, chs) => SOME (SOME v, chs)
|
adamc@1204
|
888
|
adamc@1201
|
889 fun skip cp chs =
|
adamc@1201
|
890 case chs of
|
adamc@1201
|
891 String "" :: chs => skip cp chs
|
adamc@1201
|
892 | String s :: chs' => if cp (String.sub (s, 0)) then
|
adamc@1201
|
893 skip cp (String (String.extract (s, 1, NONE)) :: chs')
|
adamc@1201
|
894 else
|
adamc@1201
|
895 SOME ((), chs)
|
adamc@1201
|
896 | _ => SOME ((), chs)
|
adamc@1201
|
897
|
adamc@1201
|
898 fun keep cp chs =
|
adamc@1201
|
899 case chs of
|
adamc@1201
|
900 String "" :: chs => keep cp chs
|
adamc@1201
|
901 | String s :: chs' =>
|
adamc@1201
|
902 let
|
adamc@1201
|
903 val (befor, after) = Substring.splitl cp (Substring.full s)
|
adamc@1201
|
904 in
|
adamc@1201
|
905 if Substring.isEmpty befor then
|
adamc@1201
|
906 NONE
|
adamc@1201
|
907 else
|
adamc@1201
|
908 SOME (Substring.string befor,
|
adamc@1201
|
909 if Substring.isEmpty after then
|
adamc@1201
|
910 chs'
|
adamc@1201
|
911 else
|
adamc@1201
|
912 String (Substring.string after) :: chs')
|
adamc@1201
|
913 end
|
adamc@1201
|
914 | _ => NONE
|
adamc@1201
|
915
|
adamc@1204
|
916 fun ws p = wrap (follow (skip (fn ch => ch = #" "))
|
adamc@1204
|
917 (follow p (skip (fn ch => ch = #" ")))) (#1 o #2)
|
adamc@1204
|
918
|
adamc@1204
|
919 fun log name p chs =
|
adamc@1206
|
920 (if !debug then
|
adamc@1227
|
921 (print (name ^ ": ");
|
adamc@1227
|
922 app (fn String s => print s
|
adamc@1227
|
923 | _ => print "???") chs;
|
adamc@1227
|
924 print "\n")
|
adamc@1206
|
925 else
|
adamc@1206
|
926 ();
|
adamc@1204
|
927 p chs)
|
adamc@1201
|
928
|
adamc@1201
|
929 fun list p chs =
|
adamc@1207
|
930 altL [wrap (follow p (follow (ws (const ",")) (list p)))
|
adamc@1207
|
931 (fn (v, ((), ls)) => v :: ls),
|
adamc@1207
|
932 wrap (ws p) (fn v => [v]),
|
adamc@1207
|
933 always []] chs
|
adamc@1201
|
934
|
adamc@1201
|
935 val ident = keep (fn ch => Char.isAlphaNum ch orelse ch = #"_")
|
adamc@1201
|
936
|
adamc@1211
|
937 val t_ident = wrapP ident (fn s => if String.isPrefix "T_" s then
|
adamc@1211
|
938 SOME (String.extract (s, 2, NONE))
|
adamc@1201
|
939 else
|
adamc@1211
|
940 NONE)
|
adamc@1211
|
941 val uw_ident = wrapP ident (fn s => if String.isPrefix "uw_" s andalso size s >= 4 then
|
adamc@1211
|
942 SOME (str (Char.toUpper (String.sub (s, 3)))
|
adamc@1211
|
943 ^ String.extract (s, 4, NONE))
|
adamc@1211
|
944 else
|
adamc@1211
|
945 NONE)
|
adamc@1201
|
946
|
adamc@1211
|
947 val field = wrap (follow t_ident
|
adamc@1201
|
948 (follow (const ".")
|
adamc@1201
|
949 uw_ident))
|
adamc@1201
|
950 (fn (t, ((), f)) => (t, f))
|
adamc@1201
|
951
|
adamc@1206
|
952 datatype Rel =
|
adamc@1206
|
953 Exps of exp * exp -> prop
|
adamc@1206
|
954 | Props of prop * prop -> prop
|
adamc@1206
|
955
|
adamc@1204
|
956 datatype sqexp =
|
adamc@1206
|
957 SqConst of Prim.t
|
adamc@1243
|
958 | SqTrue
|
adamc@1243
|
959 | SqFalse
|
adamc@1206
|
960 | Field of string * string
|
adamc@1239
|
961 | Computed of string
|
adamc@1206
|
962 | Binop of Rel * sqexp * sqexp
|
adamc@1207
|
963 | SqKnown of sqexp
|
adamc@1207
|
964 | Inj of Mono.exp
|
adamc@1211
|
965 | SqFunc of string * sqexp
|
adamc@1211
|
966 | Count
|
adamc@1204
|
967
|
adamc@1210
|
968 fun cmp s r = wrap (const s) (fn () => Exps (fn (e1, e2) => Reln (r, [e1, e2])))
|
adamc@1210
|
969
|
adamc@1210
|
970 val sqbrel = altL [cmp "=" Eq,
|
adamc@1210
|
971 cmp "<>" Ne,
|
adamc@1210
|
972 cmp "<=" Le,
|
adamc@1210
|
973 cmp "<" Lt,
|
adamc@1210
|
974 cmp ">=" Ge,
|
adamc@1210
|
975 cmp ">" Gt,
|
adamc@1207
|
976 wrap (const "AND") (fn () => Props And),
|
adamc@1207
|
977 wrap (const "OR") (fn () => Props Or)]
|
adamc@1204
|
978
|
adamc@1204
|
979 datatype ('a, 'b) sum = inl of 'a | inr of 'b
|
adamc@1204
|
980
|
adamc@1209
|
981 fun string chs =
|
adamc@1206
|
982 case chs of
|
adamc@1209
|
983 String s :: chs =>
|
adamc@1209
|
984 if size s >= 2 andalso String.sub (s, 0) = #"'" then
|
adamc@1209
|
985 let
|
adamc@1209
|
986 fun loop (cs, acc) =
|
adamc@1209
|
987 case cs of
|
adamc@1209
|
988 [] => NONE
|
adamc@1209
|
989 | c :: cs =>
|
adamc@1209
|
990 if c = #"'" then
|
adamc@1209
|
991 SOME (String.implode (rev acc), cs)
|
adamc@1209
|
992 else if c = #"\\" then
|
adamc@1209
|
993 case cs of
|
adamc@1209
|
994 c :: cs => loop (cs, c :: acc)
|
adamc@1209
|
995 | _ => raise Fail "Iflow.string: Unmatched backslash escape"
|
adamc@1209
|
996 else
|
adamc@1209
|
997 loop (cs, c :: acc)
|
adamc@1209
|
998 in
|
adamc@1209
|
999 case loop (String.explode (String.extract (s, 1, NONE)), []) of
|
adamc@1209
|
1000 NONE => NONE
|
adamc@1209
|
1001 | SOME (s, []) => SOME (s, chs)
|
adamc@1209
|
1002 | SOME (s, cs) => SOME (s, String (String.implode cs) :: chs)
|
adamc@1209
|
1003 end
|
adamc@1209
|
1004 else
|
adamc@1209
|
1005 NONE
|
adamc@1209
|
1006 | _ => NONE
|
adamc@1206
|
1007
|
adamc@1209
|
1008 val prim =
|
adamc@1209
|
1009 altL [wrap (follow (wrapP (follow (keep Char.isDigit) (follow (const ".") (keep Char.isDigit)))
|
adamc@1209
|
1010 (fn (x, ((), y)) => Option.map Prim.Float (Real64.fromString (x ^ "." ^ y))))
|
adamc@1209
|
1011 (opt (const "::float8"))) #1,
|
adamc@1209
|
1012 wrap (follow (wrapP (keep Char.isDigit)
|
adamc@1209
|
1013 (Option.map Prim.Int o Int64.fromString))
|
adamc@1209
|
1014 (opt (const "::int8"))) #1,
|
adamc@1209
|
1015 wrap (follow (opt (const "E")) (follow string (opt (const "::text"))))
|
adamc@1209
|
1016 (Prim.String o #1 o #2)]
|
adamc@1206
|
1017
|
adamc@1207
|
1018 fun known' chs =
|
adamc@1207
|
1019 case chs of
|
adamc@1207
|
1020 Exp (EFfi ("Basis", "sql_known"), _) :: chs => SOME ((), chs)
|
adamc@1207
|
1021 | _ => NONE
|
adamc@1207
|
1022
|
adamc@1207
|
1023 fun sqlify chs =
|
adamc@1207
|
1024 case chs of
|
adamc@1207
|
1025 Exp (EFfiApp ("Basis", f, [e]), _) :: chs =>
|
adamc@1207
|
1026 if String.isPrefix "sqlify" f then
|
adamc@1207
|
1027 SOME (e, chs)
|
adamc@1207
|
1028 else
|
adamc@1207
|
1029 NONE
|
adamc@1243
|
1030 | Exp (ECase (e, [((PCon (_, PConFfi {mod = "Basis", con = "True", ...}, NONE), _),
|
adamc@1243
|
1031 (EPrim (Prim.String "TRUE"), _)),
|
adamc@1243
|
1032 ((PCon (_, PConFfi {mod = "Basis", con = "False", ...}, NONE), _),
|
adamc@1243
|
1033 (EPrim (Prim.String "FALSE"), _))], _), _) :: chs =>
|
adamc@1243
|
1034 SOME (e, chs)
|
adamc@1243
|
1035
|
adamc@1207
|
1036 | _ => NONE
|
adamc@1207
|
1037
|
adamc@1211
|
1038 fun constK s = wrap (const s) (fn () => s)
|
adamc@1211
|
1039
|
adamc@1211
|
1040 val funcName = altL [constK "COUNT",
|
adamc@1211
|
1041 constK "MIN",
|
adamc@1211
|
1042 constK "MAX",
|
adamc@1211
|
1043 constK "SUM",
|
adamc@1211
|
1044 constK "AVG"]
|
adamc@1211
|
1045
|
adamc@1204
|
1046 fun sqexp chs =
|
adamc@1206
|
1047 log "sqexp"
|
adamc@1207
|
1048 (altL [wrap prim SqConst,
|
adamc@1243
|
1049 wrap (const "TRUE") (fn () => SqTrue),
|
adamc@1243
|
1050 wrap (const "FALSE") (fn () => SqFalse),
|
adamc@1211
|
1051 wrap field Field,
|
adamc@1239
|
1052 wrap uw_ident Computed,
|
adamc@1207
|
1053 wrap known SqKnown,
|
adamc@1211
|
1054 wrap func SqFunc,
|
adamc@1211
|
1055 wrap (const "COUNT(*)") (fn () => Count),
|
adamc@1207
|
1056 wrap sqlify Inj,
|
adamc@1211
|
1057 wrap (follow (const "COALESCE(") (follow sqexp (follow (const ",")
|
adamc@1211
|
1058 (follow (keep (fn ch => ch <> #")")) (const ")")))))
|
adamc@1211
|
1059 (fn ((), (e, _)) => e),
|
adamc@1207
|
1060 wrap (follow (ws (const "("))
|
adamc@1207
|
1061 (follow (wrap
|
adamc@1207
|
1062 (follow sqexp
|
adamc@1207
|
1063 (alt
|
adamc@1207
|
1064 (wrap
|
adamc@1207
|
1065 (follow (ws sqbrel)
|
adamc@1207
|
1066 (ws sqexp))
|
adamc@1207
|
1067 inl)
|
adamc@1207
|
1068 (always (inr ()))))
|
adamc@1207
|
1069 (fn (e1, sm) =>
|
adamc@1207
|
1070 case sm of
|
adamc@1207
|
1071 inl (bo, e2) => Binop (bo, e1, e2)
|
adamc@1207
|
1072 | inr () => e1))
|
adamc@1207
|
1073 (const ")")))
|
adamc@1207
|
1074 (fn ((), (e, ())) => e)])
|
adamc@1207
|
1075 chs
|
adamc@1206
|
1076
|
adamc@1207
|
1077 and known chs = wrap (follow known' (follow (const "(") (follow sqexp (const ")"))))
|
adamc@1211
|
1078 (fn ((), ((), (e, ()))) => e) chs
|
adamc@1211
|
1079
|
adamc@1211
|
1080 and func chs = wrap (follow funcName (follow (const "(") (follow sqexp (const ")"))))
|
adamc@1211
|
1081 (fn (f, ((), (e, ()))) => (f, e)) chs
|
adamc@1211
|
1082
|
adamc@1211
|
1083 datatype sitem =
|
adamc@1211
|
1084 SqField of string * string
|
adamc@1211
|
1085 | SqExp of sqexp * string
|
adamc@1211
|
1086
|
adamc@1239
|
1087 val sitem = alt (wrap (follow sqexp (follow (const " AS ") uw_ident))
|
adamc@1239
|
1088 (fn (e, ((), s)) => SqExp (e, s)))
|
adamc@1239
|
1089 (wrap field SqField)
|
adamc@1207
|
1090
|
adamc@1207
|
1091 val select = log "select"
|
adamc@1207
|
1092 (wrap (follow (const "SELECT ") (list sitem))
|
adamc@1207
|
1093 (fn ((), ls) => ls))
|
adamc@1201
|
1094
|
adamc@1201
|
1095 val fitem = wrap (follow uw_ident
|
adamc@1201
|
1096 (follow (const " AS ")
|
adamc@1201
|
1097 t_ident))
|
adamc@1201
|
1098 (fn (t, ((), f)) => (t, f))
|
adamc@1201
|
1099
|
adamc@1207
|
1100 val from = log "from"
|
adamc@1207
|
1101 (wrap (follow (const "FROM ") (list fitem))
|
adamc@1207
|
1102 (fn ((), ls) => ls))
|
adamc@1201
|
1103
|
adamc@1204
|
1104 val wher = wrap (follow (ws (const "WHERE ")) sqexp)
|
adamc@1204
|
1105 (fn ((), ls) => ls)
|
adamc@1204
|
1106
|
adamc@1227
|
1107 type query1 = {Select : sitem list,
|
adamc@1227
|
1108 From : (string * string) list,
|
adamc@1227
|
1109 Where : sqexp option}
|
adamc@1227
|
1110
|
adamc@1227
|
1111 val query1 = log "query1"
|
adamc@1207
|
1112 (wrap (follow (follow select from) (opt wher))
|
adamc@1207
|
1113 (fn ((fs, ts), wher) => {Select = fs, From = ts, Where = wher}))
|
adamc@1201
|
1114
|
adamc@1227
|
1115 datatype query =
|
adamc@1227
|
1116 Query1 of query1
|
adamc@1227
|
1117 | Union of query * query
|
adamc@1227
|
1118
|
adamc@1239
|
1119 val orderby = log "orderby"
|
adamc@1239
|
1120 (wrap (follow (ws (const "ORDER BY "))
|
adamc@1243
|
1121 (follow (list sqexp)
|
adamc@1243
|
1122 (opt (ws (const "DESC")))))
|
adamc@1243
|
1123 ignore)
|
adamc@1239
|
1124
|
adamc@1227
|
1125 fun query chs = log "query"
|
adamc@1239
|
1126 (wrap
|
adamc@1239
|
1127 (follow
|
adamc@1239
|
1128 (alt (wrap (follow (const "((")
|
adamc@1239
|
1129 (follow query
|
adamc@1239
|
1130 (follow (const ") UNION (")
|
adamc@1239
|
1131 (follow query (const "))")))))
|
adamc@1239
|
1132 (fn ((), (q1, ((), (q2, ())))) => Union (q1, q2)))
|
adamc@1239
|
1133 (wrap query1 Query1))
|
adamc@1239
|
1134 (opt orderby))
|
adamc@1239
|
1135 #1)
|
adamc@1227
|
1136 chs
|
adamc@1227
|
1137
|
adamc@1220
|
1138 datatype dml =
|
adamc@1220
|
1139 Insert of string * (string * sqexp) list
|
adamc@1221
|
1140 | Delete of string * sqexp
|
adamc@1223
|
1141 | Update of string * (string * sqexp) list * sqexp
|
adamc@1220
|
1142
|
adamc@1220
|
1143 val insert = log "insert"
|
adamc@1220
|
1144 (wrapP (follow (const "INSERT INTO ")
|
adamc@1220
|
1145 (follow uw_ident
|
adamc@1220
|
1146 (follow (const " (")
|
adamc@1220
|
1147 (follow (list uw_ident)
|
adamc@1220
|
1148 (follow (const ") VALUES (")
|
adamc@1220
|
1149 (follow (list sqexp)
|
adamc@1220
|
1150 (const ")")))))))
|
adamc@1220
|
1151 (fn ((), (tab, ((), (fs, ((), (es, ())))))) =>
|
adamc@1221
|
1152 (SOME (tab, ListPair.zipEq (fs, es)))
|
adamc@1220
|
1153 handle ListPair.UnequalLengths => NONE))
|
adamc@1220
|
1154
|
adamc@1221
|
1155 val delete = log "delete"
|
adamc@1221
|
1156 (wrap (follow (const "DELETE FROM ")
|
adamc@1221
|
1157 (follow uw_ident
|
adamc@1221
|
1158 (follow (const " AS T_T WHERE ")
|
adamc@1221
|
1159 sqexp)))
|
adamc@1221
|
1160 (fn ((), (tab, ((), es))) => (tab, es)))
|
adamc@1221
|
1161
|
adamc@1223
|
1162 val setting = log "setting"
|
adamc@1223
|
1163 (wrap (follow uw_ident (follow (const " = ") sqexp))
|
adamc@1223
|
1164 (fn (f, ((), e)) => (f, e)))
|
adamc@1223
|
1165
|
adamc@1223
|
1166 val update = log "update"
|
adamc@1223
|
1167 (wrap (follow (const "UPDATE ")
|
adamc@1223
|
1168 (follow uw_ident
|
adamc@1223
|
1169 (follow (const " AS T_T SET ")
|
adamc@1223
|
1170 (follow (list setting)
|
adamc@1223
|
1171 (follow (ws (const "WHERE "))
|
adamc@1223
|
1172 sqexp)))))
|
adamc@1223
|
1173 (fn ((), (tab, ((), (fs, ((), e))))) =>
|
adamc@1223
|
1174 (tab, fs, e)))
|
adamc@1223
|
1175
|
adamc@1220
|
1176 val dml = log "dml"
|
adamc@1221
|
1177 (altL [wrap insert Insert,
|
adamc@1223
|
1178 wrap delete Delete,
|
adamc@1223
|
1179 wrap update Update])
|
adamc@1220
|
1180
|
adamc@1236
|
1181 type check = exp * ErrorMsg.span
|
adamc@1236
|
1182
|
adamc@1236
|
1183 structure St :> sig
|
adamc@1236
|
1184 val reset : unit -> unit
|
adamc@1236
|
1185
|
adamc@1236
|
1186 type stashed
|
adamc@1236
|
1187 val stash : unit -> stashed
|
adamc@1236
|
1188 val reinstate : stashed -> unit
|
adamc@1236
|
1189
|
adamc@1236
|
1190 val nextVar : unit -> int
|
adamc@1236
|
1191
|
adamc@1236
|
1192 val assert : atom list -> unit
|
adamc@1236
|
1193
|
adamc@1236
|
1194 val addPath : check -> unit
|
adamc@1236
|
1195
|
adamc@1236
|
1196 val allowSend : atom list * exp list -> unit
|
adamc@1238
|
1197 val send : bool -> check -> unit
|
adamc@1236
|
1198
|
adamc@1236
|
1199 val allowInsert : atom list -> unit
|
adamc@1236
|
1200 val insert : ErrorMsg.span -> unit
|
adamc@1236
|
1201
|
adamc@1236
|
1202 val allowDelete : atom list -> unit
|
adamc@1236
|
1203 val delete : ErrorMsg.span -> unit
|
adamc@1236
|
1204
|
adamc@1236
|
1205 val allowUpdate : atom list -> unit
|
adamc@1236
|
1206 val update : ErrorMsg.span -> unit
|
adamc@1236
|
1207
|
adamc@1236
|
1208 val havocReln : reln -> unit
|
adamc@1238
|
1209
|
adamc@1238
|
1210 val debug : unit -> unit
|
adamc@1236
|
1211 end = struct
|
adamc@1236
|
1212
|
adamc@1236
|
1213 val hnames = ref 1
|
adamc@1236
|
1214
|
adamc@1236
|
1215 type hyps = int * atom list
|
adamc@1236
|
1216
|
adamc@1236
|
1217 val db = Cc.database ()
|
adamc@1236
|
1218 val path = ref ([] : (hyps * check) option ref list)
|
adamc@1236
|
1219 val hyps = ref (0, [] : atom list)
|
adamc@1236
|
1220 val nvar = ref 0
|
adamc@1236
|
1221
|
adamc@1236
|
1222 fun setHyps (h as (n', hs)) =
|
adamc@1236
|
1223 let
|
adamc@1236
|
1224 val (n, _) = !hyps
|
adamc@1236
|
1225 in
|
adamc@1236
|
1226 if n' = n then
|
adamc@1236
|
1227 ()
|
adamc@1236
|
1228 else
|
adamc@1236
|
1229 (hyps := h;
|
adamc@1236
|
1230 Cc.clear db;
|
adamc@1236
|
1231 app (fn a => Cc.assert (db, a)) hs)
|
adamc@1236
|
1232 end
|
adamc@1236
|
1233
|
adamc@1236
|
1234 type stashed = int * (hyps * check) option ref list * (int * atom list)
|
adamc@1236
|
1235 fun stash () = (!nvar, !path, !hyps)
|
adamc@1236
|
1236 fun reinstate (nv, p, h) =
|
adamc@1236
|
1237 (nvar := nv;
|
adamc@1236
|
1238 path := p;
|
adamc@1236
|
1239 setHyps h)
|
adamc@1236
|
1240
|
adamc@1236
|
1241 fun nextVar () =
|
adamc@1236
|
1242 let
|
adamc@1236
|
1243 val n = !nvar
|
adamc@1236
|
1244 in
|
adamc@1236
|
1245 nvar := n + 1;
|
adamc@1236
|
1246 n
|
adamc@1236
|
1247 end
|
adamc@1236
|
1248
|
adamc@1236
|
1249 fun assert ats =
|
adamc@1236
|
1250 let
|
adamc@1236
|
1251 val n = !hnames
|
adamc@1236
|
1252 val (_, hs) = !hyps
|
adamc@1236
|
1253 in
|
adamc@1236
|
1254 hnames := n + 1;
|
adamc@1236
|
1255 hyps := (n, ats @ hs);
|
adamc@1236
|
1256 app (fn a => Cc.assert (db, a)) ats
|
adamc@1236
|
1257 end
|
adamc@1236
|
1258
|
adamc@1236
|
1259 fun addPath c = path := ref (SOME (!hyps, c)) :: !path
|
adamc@1236
|
1260
|
adamc@1236
|
1261 val sendable = ref ([] : (atom list * exp list) list)
|
adamc@1236
|
1262
|
adamc@1238
|
1263 fun checkGoals goals k =
|
adamc@1238
|
1264 let
|
adamc@1238
|
1265 fun checkGoals goals unifs =
|
adamc@1238
|
1266 case goals of
|
adamc@1238
|
1267 [] => k unifs
|
adamc@1238
|
1268 | AReln (Sql tab, [Lvar lv]) :: goals =>
|
adamc@1238
|
1269 let
|
adamc@1238
|
1270 val saved = stash ()
|
adamc@1238
|
1271 val (_, hyps) = !hyps
|
adamc@1236
|
1272
|
adamc@1238
|
1273 fun tryAll unifs hyps =
|
adamc@1238
|
1274 case hyps of
|
adamc@1238
|
1275 [] => false
|
adamc@1238
|
1276 | AReln (Sql tab', [e]) :: hyps =>
|
adamc@1238
|
1277 (tab' = tab andalso
|
adamc@1238
|
1278 checkGoals goals (IM.insert (unifs, lv, e)))
|
adamc@1238
|
1279 orelse tryAll unifs hyps
|
adamc@1238
|
1280 | _ :: hyps => tryAll unifs hyps
|
adamc@1238
|
1281 in
|
adamc@1238
|
1282 tryAll unifs hyps
|
adamc@1238
|
1283 end
|
adamc@1243
|
1284 | (g as AReln (r, es)) :: goals =>
|
adamc@1238
|
1285 Cc.check (db, AReln (r, map (simplify unifs) es))
|
adamc@1238
|
1286 andalso checkGoals goals unifs
|
adamc@1238
|
1287 | ACond _ :: _ => false
|
adamc@1238
|
1288 in
|
adamc@1238
|
1289 checkGoals goals IM.empty
|
adamc@1238
|
1290 end
|
adamc@1236
|
1291
|
adamc@1238
|
1292 fun useKeys () =
|
adamc@1236
|
1293 let
|
adamc@1238
|
1294 fun findKeys hyps =
|
adamc@1238
|
1295 case hyps of
|
adamc@1238
|
1296 [] => ()
|
adamc@1238
|
1297 | AReln (Sql tab, [r1]) :: hyps =>
|
adamc@1238
|
1298 (case SM.find (!tabs, tab) of
|
adamc@1238
|
1299 NONE => findKeys hyps
|
adamc@1238
|
1300 | SOME (_, []) => findKeys hyps
|
adamc@1238
|
1301 | SOME (_, ks) =>
|
adamc@1238
|
1302 let
|
adamc@1238
|
1303 fun finder hyps =
|
adamc@1238
|
1304 case hyps of
|
adamc@1238
|
1305 [] => ()
|
adamc@1238
|
1306 | AReln (Sql tab', [r2]) :: hyps =>
|
adamc@1238
|
1307 (if tab' = tab andalso
|
adamc@1238
|
1308 List.exists (List.all (fn f =>
|
adamc@1238
|
1309 let
|
adamc@1238
|
1310 val r =
|
adamc@1238
|
1311 Cc.check (db,
|
adamc@1238
|
1312 AReln (Eq, [Proj (r1, f),
|
adamc@1238
|
1313 Proj (r2, f)]))
|
adamc@1238
|
1314 in
|
adamc@1238
|
1315 (*Print.prefaces "Fs"
|
adamc@1238
|
1316 [("tab",
|
adamc@1238
|
1317 Print.PD.string tab),
|
adamc@1238
|
1318 ("r1",
|
adamc@1238
|
1319 p_exp (Proj (r1, f))),
|
adamc@1238
|
1320 ("r2",
|
adamc@1238
|
1321 p_exp (Proj (r2, f))),
|
adamc@1238
|
1322 ("r",
|
adamc@1238
|
1323 Print.PD.string
|
adamc@1238
|
1324 (Bool.toString r))];*)
|
adamc@1238
|
1325 r
|
adamc@1238
|
1326 end)) ks then
|
adamc@1238
|
1327 ((*Print.prefaces "Key match" [("tab", Print.PD.string tab),
|
adamc@1238
|
1328 ("r1", p_exp r1),
|
adamc@1238
|
1329 ("r2", p_exp r2),
|
adamc@1238
|
1330 ("rp1", Cc.p_repOf cc r1),
|
adamc@1238
|
1331 ("rp2", Cc.p_repOf cc r2)];*)
|
adamc@1238
|
1332 Cc.assert (db, AReln (Eq, [r1, r2])))
|
adamc@1238
|
1333 else
|
adamc@1238
|
1334 ();
|
adamc@1238
|
1335 finder hyps)
|
adamc@1238
|
1336 | _ :: hyps => finder hyps
|
adamc@1238
|
1337 in
|
adamc@1238
|
1338 finder hyps;
|
adamc@1238
|
1339 findKeys hyps
|
adamc@1238
|
1340 end)
|
adamc@1238
|
1341 | _ :: hyps => findKeys hyps
|
adamc@1238
|
1342
|
adamc@1238
|
1343 val (_, hs) = !hyps
|
adamc@1238
|
1344 in
|
adamc@1238
|
1345 (*print "findKeys\n";*)
|
adamc@1238
|
1346 findKeys hs
|
adamc@1238
|
1347 end
|
adamc@1238
|
1348
|
adamc@1238
|
1349 fun buildable uk (e, loc) =
|
adamc@1238
|
1350 let
|
adamc@1238
|
1351 fun doPols pols acc =
|
adamc@1236
|
1352 case pols of
|
adamc@1236
|
1353 [] => ((*Print.prefaces "buildable" [("Base", Print.p_list p_exp acc),
|
adamc@1236
|
1354 ("Derived", p_exp e),
|
adamc@1236
|
1355 ("Hyps", Print.p_list p_atom (#2 (!hyps)))];*)
|
adamc@1238
|
1356 Cc.builtFrom (db, {UseKnown = uk, Base = acc, Derived = e}))
|
adamc@1236
|
1357 | (goals, es) :: pols =>
|
adamc@1238
|
1358 checkGoals goals (fn unifs => doPols pols (map (simplify unifs) es @ acc))
|
adamc@1238
|
1359 orelse doPols pols acc
|
adamc@1236
|
1360 in
|
adamc@1238
|
1361 useKeys ();
|
adamc@1238
|
1362 if doPols (!sendable) [] then
|
adamc@1238
|
1363 ()
|
adamc@1238
|
1364 else
|
adamc@1238
|
1365 let
|
adamc@1238
|
1366 val (_, hs) = !hyps
|
adamc@1238
|
1367 in
|
adamc@1238
|
1368 ErrorMsg.errorAt loc "The information flow policy may be violated here.";
|
adamc@1238
|
1369 Print.prefaces "Situation" [("Hypotheses", Print.p_list p_atom hs),
|
adamc@1243
|
1370 ("User learns", p_exp e),
|
adamc@1243
|
1371 ("E-graph", Cc.p_database db)]
|
adamc@1238
|
1372 end
|
adamc@1236
|
1373 end
|
adamc@1236
|
1374
|
adamc@1236
|
1375 fun checkPaths () =
|
adamc@1236
|
1376 let
|
adamc@1236
|
1377 val hs = !hyps
|
adamc@1236
|
1378 in
|
adamc@1236
|
1379 app (fn r =>
|
adamc@1236
|
1380 case !r of
|
adamc@1236
|
1381 NONE => ()
|
adamc@1236
|
1382 | SOME (hs, e) =>
|
adamc@1236
|
1383 (r := NONE;
|
adamc@1236
|
1384 setHyps hs;
|
adamc@1238
|
1385 buildable true e)) (!path);
|
adamc@1236
|
1386 setHyps hs
|
adamc@1236
|
1387 end
|
adamc@1236
|
1388
|
adamc@1238
|
1389 fun allowSend v = ((*Print.prefaces "Allow" [("goals", Print.p_list p_atom (#1 v)),
|
adamc@1243
|
1390 ("exps", Print.p_list p_exp (#2 v))];*)
|
adamc@1238
|
1391 sendable := v :: !sendable)
|
adamc@1236
|
1392
|
adamc@1238
|
1393 fun send uk (e, loc) = ((*Print.preface ("Send", p_exp e);*)
|
adamc@1238
|
1394 checkPaths ();
|
adamc@1238
|
1395 if isKnown e then
|
adamc@1238
|
1396 ()
|
adamc@1238
|
1397 else
|
adamc@1238
|
1398 buildable uk (e, loc))
|
adamc@1236
|
1399
|
adamc@1236
|
1400 fun doable pols (loc : ErrorMsg.span) =
|
adamc@1236
|
1401 let
|
adamc@1236
|
1402 val pols = !pols
|
adamc@1236
|
1403 in
|
adamc@1236
|
1404 if List.exists (fn goals =>
|
adamc@1238
|
1405 if checkGoals goals (fn _ => true) then
|
adamc@1238
|
1406 ((*Print.prefaces "Match" [("goals", Print.p_list p_atom goals),
|
adamc@1238
|
1407 ("hyps", Print.p_list p_atom (#2 (!hyps)))];*)
|
adamc@1238
|
1408 true)
|
adamc@1238
|
1409 else
|
adamc@1238
|
1410 ((*Print.prefaces "No match" [("goals", Print.p_list p_atom goals),
|
adamc@1238
|
1411 ("hyps", Print.p_list p_atom (#2 (!hyps)))];*)
|
adamc@1238
|
1412 false)) pols then
|
adamc@1236
|
1413 ()
|
adamc@1236
|
1414 else
|
adamc@1236
|
1415 let
|
adamc@1236
|
1416 val (_, hs) = !hyps
|
adamc@1236
|
1417 in
|
adamc@1236
|
1418 ErrorMsg.errorAt loc "The database update policy may be violated here.";
|
adamc@1236
|
1419 Print.preface ("Hypotheses", Print.p_list p_atom hs)
|
adamc@1236
|
1420 end
|
adamc@1236
|
1421 end
|
adamc@1236
|
1422
|
adamc@1236
|
1423 val insertable = ref ([] : atom list list)
|
adamc@1236
|
1424 fun allowInsert v = insertable := v :: !insertable
|
adamc@1236
|
1425 val insert = doable insertable
|
adamc@1236
|
1426
|
adamc@1236
|
1427 val updatable = ref ([] : atom list list)
|
adamc@1236
|
1428 fun allowUpdate v = updatable := v :: !updatable
|
adamc@1236
|
1429 val update = doable updatable
|
adamc@1236
|
1430
|
adamc@1236
|
1431 val deletable = ref ([] : atom list list)
|
adamc@1236
|
1432 fun allowDelete v = deletable := v :: !deletable
|
adamc@1236
|
1433 val delete = doable deletable
|
adamc@1236
|
1434
|
adamc@1238
|
1435 fun reset () = (Cc.clear db;
|
adamc@1238
|
1436 path := [];
|
adamc@1238
|
1437 hyps := (0, []);
|
adamc@1238
|
1438 nvar := 0;
|
adamc@1238
|
1439 sendable := [];
|
adamc@1238
|
1440 insertable := [];
|
adamc@1238
|
1441 updatable := [];
|
adamc@1238
|
1442 deletable := [])
|
adamc@1238
|
1443
|
adamc@1236
|
1444 fun havocReln r =
|
adamc@1236
|
1445 let
|
adamc@1236
|
1446 val n = !hnames
|
adamc@1236
|
1447 val (_, hs) = !hyps
|
adamc@1236
|
1448 in
|
adamc@1236
|
1449 hnames := n + 1;
|
adamc@1236
|
1450 hyps := (n, List.filter (fn AReln (r', _) => r' <> r | _ => true) hs)
|
adamc@1236
|
1451 end
|
adamc@1236
|
1452
|
adamc@1238
|
1453 fun debug () =
|
adamc@1238
|
1454 let
|
adamc@1238
|
1455 val (_, hs) = !hyps
|
adamc@1238
|
1456 in
|
adamc@1238
|
1457 Print.preface ("Hyps", Print.p_list p_atom hs)
|
adamc@1238
|
1458 end
|
adamc@1238
|
1459
|
adamc@1236
|
1460 end
|
adamc@1236
|
1461
|
adamc@1236
|
1462
|
adamc@1215
|
1463 fun removeDups (ls : (string * string) list) =
|
adamc@1211
|
1464 case ls of
|
adamc@1211
|
1465 [] => []
|
adamc@1211
|
1466 | x :: ls =>
|
adamc@1211
|
1467 let
|
adamc@1211
|
1468 val ls = removeDups ls
|
adamc@1211
|
1469 in
|
adamc@1211
|
1470 if List.exists (fn x' => x' = x) ls then
|
adamc@1211
|
1471 ls
|
adamc@1211
|
1472 else
|
adamc@1211
|
1473 x :: ls
|
adamc@1211
|
1474 end
|
adamc@1211
|
1475
|
adamc@1241
|
1476 fun deinj env e =
|
adamc@1241
|
1477 case #1 e of
|
adamc@1241
|
1478 ERel n => SOME (List.nth (env, n))
|
adamc@1241
|
1479 | EField (e, f) =>
|
adamc@1241
|
1480 (case deinj env e of
|
adamc@1241
|
1481 NONE => NONE
|
adamc@1241
|
1482 | SOME e => SOME (Proj (e, f)))
|
adamc@1241
|
1483 | _ => NONE
|
adamc@1241
|
1484
|
adamc@1220
|
1485 fun expIn rv env rvOf =
|
adamc@1220
|
1486 let
|
adamc@1236
|
1487 fun expIn e =
|
adamc@1220
|
1488 let
|
adamc@1236
|
1489 fun default () = inl (rv ())
|
adamc@1220
|
1490 in
|
adamc@1220
|
1491 case e of
|
adamc@1236
|
1492 SqConst p => inl (Const p)
|
adamc@1243
|
1493 | SqTrue => inl (Func (DtCon0 "Basis.bool.True", []))
|
adamc@1243
|
1494 | SqFalse => inl (Func (DtCon0 "Basis.bool.False", []))
|
adamc@1236
|
1495 | Field (v, f) => inl (Proj (rvOf v, f))
|
adamc@1239
|
1496 | Computed _ => default ()
|
adamc@1220
|
1497 | Binop (bo, e1, e2) =>
|
adamc@1220
|
1498 let
|
adamc@1236
|
1499 val e1 = expIn e1
|
adamc@1236
|
1500 val e2 = expIn e2
|
adamc@1220
|
1501 in
|
adamc@1236
|
1502 inr (case (bo, e1, e2) of
|
adamc@1236
|
1503 (Exps f, inl e1, inl e2) => f (e1, e2)
|
adamc@1243
|
1504 | (Props f, v1, v2) =>
|
adamc@1243
|
1505 let
|
adamc@1243
|
1506 fun pin v =
|
adamc@1243
|
1507 case v of
|
adamc@1243
|
1508 inl e => Reln (Eq, [e, Func (DtCon0 "Basis.bool.True", [])])
|
adamc@1243
|
1509 | inr p => p
|
adamc@1243
|
1510 in
|
adamc@1243
|
1511 f (pin v1, pin v2)
|
adamc@1243
|
1512 end
|
adamc@1236
|
1513 | _ => Unknown)
|
adamc@1220
|
1514 end
|
adamc@1220
|
1515 | SqKnown e =>
|
adamc@1236
|
1516 (case expIn e of
|
adamc@1236
|
1517 inl e => inr (Reln (Known, [e]))
|
adamc@1236
|
1518 | _ => inr Unknown)
|
adamc@1220
|
1519 | Inj e =>
|
adamc@1241
|
1520 inl (case deinj env e of
|
adamc@1241
|
1521 NONE => rv ()
|
adamc@1241
|
1522 | SOME e => e)
|
adamc@1220
|
1523 | SqFunc (f, e) =>
|
adamc@1236
|
1524 (case expIn e of
|
adamc@1236
|
1525 inl e => inl (Func (Other f, [e]))
|
adamc@1220
|
1526 | _ => default ())
|
adamc@1220
|
1527
|
adamc@1220
|
1528 | Count => default ()
|
adamc@1220
|
1529 end
|
adamc@1220
|
1530 in
|
adamc@1220
|
1531 expIn
|
adamc@1220
|
1532 end
|
adamc@1216
|
1533
|
adamc@1236
|
1534 fun decomp {Save = save, Restore = restore, Add = add} =
|
adamc@1216
|
1535 let
|
adamc@1236
|
1536 fun go p k =
|
adamc@1236
|
1537 case p of
|
adamc@1238
|
1538 True => (k () handle Cc.Contradiction => ())
|
adamc@1236
|
1539 | False => ()
|
adamc@1236
|
1540 | Unknown => ()
|
adamc@1236
|
1541 | And (p1, p2) => go p1 (fn () => go p2 k)
|
adamc@1236
|
1542 | Or (p1, p2) =>
|
adamc@1236
|
1543 let
|
adamc@1236
|
1544 val saved = save ()
|
adamc@1236
|
1545 in
|
adamc@1236
|
1546 go p1 k;
|
adamc@1236
|
1547 restore saved;
|
adamc@1236
|
1548 go p2 k
|
adamc@1236
|
1549 end
|
adamc@1236
|
1550 | Reln x => (add (AReln x); k ())
|
adamc@1236
|
1551 | Cond x => (add (ACond x); k ())
|
adamc@1236
|
1552 in
|
adamc@1236
|
1553 go
|
adamc@1236
|
1554 end
|
adamc@1236
|
1555
|
adamc@1236
|
1556 datatype queryMode =
|
adamc@1238
|
1557 SomeCol of {New : (string * exp) option, Old : (string * exp) option, Outs : exp list} -> unit
|
adamc@1236
|
1558 | AllCols of exp -> unit
|
adamc@1236
|
1559
|
adamc@1236
|
1560 type 'a doQuery = {
|
adamc@1236
|
1561 Env : exp list,
|
adamc@1236
|
1562 NextVar : unit -> exp,
|
adamc@1236
|
1563 Add : atom -> unit,
|
adamc@1236
|
1564 Save : unit -> 'a,
|
adamc@1236
|
1565 Restore : 'a -> unit,
|
adamc@1241
|
1566 UsedExp : bool * exp -> unit,
|
adamc@1236
|
1567 Cont : queryMode
|
adamc@1236
|
1568 }
|
adamc@1236
|
1569
|
adamc@1241
|
1570 fun doQuery (arg : 'a doQuery) (e as (_, loc)) =
|
adamc@1236
|
1571 let
|
adamc@1241
|
1572 fun default () = ErrorMsg.errorAt loc "Information flow checker can't parse SQL query"
|
adamc@1216
|
1573 in
|
adamc@1216
|
1574 case parse query e of
|
adamc@1216
|
1575 NONE => default ()
|
adamc@1227
|
1576 | SOME q =>
|
adamc@1216
|
1577 let
|
adamc@1236
|
1578 fun doQuery q =
|
adamc@1227
|
1579 case q of
|
adamc@1227
|
1580 Query1 r =>
|
adamc@1227
|
1581 let
|
adamc@1238
|
1582 val new = ref NONE
|
adamc@1238
|
1583 val old = ref NONE
|
adamc@1238
|
1584
|
adamc@1238
|
1585 val rvs = map (fn (tab, v) =>
|
adamc@1238
|
1586 let
|
adamc@1238
|
1587 val nv = #NextVar arg ()
|
adamc@1238
|
1588 in
|
adamc@1238
|
1589 case v of
|
adamc@1238
|
1590 "New" => new := SOME (tab, nv)
|
adamc@1238
|
1591 | "Old" => old := SOME (tab, nv)
|
adamc@1238
|
1592 | _ => ();
|
adamc@1238
|
1593 (v, nv)
|
adamc@1238
|
1594 end) (#From r)
|
adamc@1214
|
1595
|
adamc@1227
|
1596 fun rvOf v =
|
adamc@1227
|
1597 case List.find (fn (v', _) => v' = v) rvs of
|
adamc@1227
|
1598 NONE => raise Fail "Iflow.queryProp: Bad table variable"
|
adamc@1227
|
1599 | SOME (_, e) => e
|
adamc@1214
|
1600
|
adamc@1236
|
1601 val expIn = expIn (#NextVar arg) (#Env arg) rvOf
|
adamc@1236
|
1602
|
adamc@1236
|
1603 val saved = #Save arg ()
|
adamc@1236
|
1604 fun addFrom () = app (fn (t, v) => #Add arg (AReln (Sql t, [rvOf v]))) (#From r)
|
adamc@1236
|
1605
|
adamc@1227
|
1606 fun usedFields e =
|
adamc@1227
|
1607 case e of
|
adamc@1227
|
1608 SqConst _ => []
|
adamc@1243
|
1609 | SqTrue => []
|
adamc@1243
|
1610 | SqFalse => []
|
adamc@1241
|
1611 | Field (v, f) => [(false, Proj (rvOf v, f))]
|
adamc@1239
|
1612 | Computed _ => []
|
adamc@1241
|
1613 | Binop (_, e1, e2) => usedFields e1 @ usedFields e2
|
adamc@1227
|
1614 | SqKnown _ => []
|
adamc@1241
|
1615 | Inj e =>
|
adamc@1241
|
1616 (case deinj (#Env arg) e of
|
adamc@1241
|
1617 NONE => (ErrorMsg.errorAt loc "Expression injected into SQL is too complicated";
|
adamc@1241
|
1618 [])
|
adamc@1241
|
1619 | SOME e => [(true, e)])
|
adamc@1227
|
1620 | SqFunc (_, e) => usedFields e
|
adamc@1227
|
1621 | Count => []
|
adamc@1214
|
1622
|
adamc@1236
|
1623 fun doUsed () = case #Where r of
|
adamc@1236
|
1624 NONE => ()
|
adamc@1236
|
1625 | SOME e =>
|
adamc@1241
|
1626 app (#UsedExp arg) (usedFields e)
|
adamc@1211
|
1627
|
adamc@1236
|
1628 fun normal' () =
|
adamc@1236
|
1629 case #Cont arg of
|
adamc@1236
|
1630 SomeCol k =>
|
adamc@1227
|
1631 let
|
adamc@1236
|
1632 val sis = map (fn si =>
|
adamc@1236
|
1633 case si of
|
adamc@1236
|
1634 SqField (v, f) => Proj (rvOf v, f)
|
adamc@1236
|
1635 | SqExp (e, f) =>
|
adamc@1236
|
1636 case expIn e of
|
adamc@1236
|
1637 inr _ => #NextVar arg ()
|
adamc@1236
|
1638 | inl e => e) (#Select r)
|
adamc@1227
|
1639 in
|
adamc@1238
|
1640 k {New = !new, Old = !old, Outs = sis}
|
adamc@1227
|
1641 end
|
adamc@1236
|
1642 | AllCols k =>
|
adamc@1227
|
1643 let
|
adamc@1236
|
1644 val (ts, es) =
|
adamc@1236
|
1645 foldl (fn (si, (ts, es)) =>
|
adamc@1227
|
1646 case si of
|
adamc@1227
|
1647 SqField (v, f) =>
|
adamc@1227
|
1648 let
|
adamc@1227
|
1649 val fs = getOpt (SM.find (ts, v), SM.empty)
|
adamc@1227
|
1650 in
|
adamc@1236
|
1651 (SM.insert (ts, v, SM.insert (fs, f, Proj (rvOf v, f))), es)
|
adamc@1227
|
1652 end
|
adamc@1227
|
1653 | SqExp (e, f) =>
|
adamc@1227
|
1654 let
|
adamc@1236
|
1655 val e =
|
adamc@1236
|
1656 case expIn e of
|
adamc@1236
|
1657 inr _ => #NextVar arg ()
|
adamc@1236
|
1658 | inl e => e
|
adamc@1227
|
1659 in
|
adamc@1236
|
1660 (ts, SM.insert (es, f, e))
|
adamc@1227
|
1661 end)
|
adamc@1236
|
1662 (SM.empty, SM.empty) (#Select r)
|
adamc@1227
|
1663 in
|
adamc@1236
|
1664 k (Recd (map (fn (t, fs) => (t, Recd (SM.listItemsi fs)))
|
adamc@1236
|
1665 (SM.listItemsi ts)
|
adamc@1236
|
1666 @ SM.listItemsi es))
|
adamc@1227
|
1667 end
|
adamc@1227
|
1668
|
adamc@1236
|
1669 fun doWhere final =
|
adamc@1236
|
1670 (addFrom ();
|
adamc@1236
|
1671 case #Where r of
|
adamc@1236
|
1672 NONE => (doUsed (); final ())
|
adamc@1236
|
1673 | SOME e =>
|
adamc@1243
|
1674 let
|
adamc@1243
|
1675 val p = case expIn e of
|
adamc@1243
|
1676 inl e => Reln (Eq, [e, Func (DtCon0 "Basis.bool.True", [])])
|
adamc@1243
|
1677 | inr p => p
|
adamc@1243
|
1678
|
adamc@1243
|
1679 val saved = #Save arg ()
|
adamc@1243
|
1680 in
|
adamc@1243
|
1681 decomp {Save = #Save arg, Restore = #Restore arg, Add = #Add arg}
|
adamc@1243
|
1682 p (fn () => (doUsed (); final ()) handle Cc.Contradiction => ());
|
adamc@1243
|
1683 #Restore arg saved
|
adamc@1243
|
1684 end)
|
adamc@1236
|
1685 handle Cc.Contradiction => ()
|
adamc@1236
|
1686
|
adamc@1236
|
1687 fun normal () = doWhere normal'
|
adamc@1227
|
1688 in
|
adamc@1236
|
1689 (case #Select r of
|
adamc@1236
|
1690 [SqExp (Binop (Exps bo, Count, SqConst (Prim.Int 0)), f)] =>
|
adamc@1236
|
1691 (case bo (Const (Prim.Int 1), Const (Prim.Int 2)) of
|
adamc@1236
|
1692 Reln (Gt, [Const (Prim.Int 1), Const (Prim.Int 2)]) =>
|
adamc@1236
|
1693 (case #Cont arg of
|
adamc@1236
|
1694 SomeCol _ => ()
|
adamc@1236
|
1695 | AllCols k =>
|
adamc@1236
|
1696 let
|
adamc@1236
|
1697 fun answer e = k (Recd [(f, e)])
|
adamc@1236
|
1698
|
adamc@1236
|
1699 val saved = #Save arg ()
|
adamc@1238
|
1700 val () = (answer (Func (DtCon0 "Basis.bool.False", [])))
|
adamc@1238
|
1701 handle Cc.Contradiction => ()
|
adamc@1236
|
1702 in
|
adamc@1238
|
1703 #Restore arg saved;
|
adamc@1238
|
1704 (*print "True time!\n";*)
|
adamc@1236
|
1705 doWhere (fn () => answer (Func (DtCon0 "Basis.bool.True", [])));
|
adamc@1236
|
1706 #Restore arg saved
|
adamc@1236
|
1707 end)
|
adamc@1236
|
1708 | _ => normal ())
|
adamc@1236
|
1709 | _ => normal ())
|
adamc@1236
|
1710 before #Restore arg saved
|
adamc@1227
|
1711 end
|
adamc@1227
|
1712 | Union (q1, q2) =>
|
adamc@1220
|
1713 let
|
adamc@1236
|
1714 val saved = #Save arg ()
|
adamc@1220
|
1715 in
|
adamc@1236
|
1716 doQuery q1;
|
adamc@1236
|
1717 #Restore arg saved;
|
adamc@1236
|
1718 doQuery q2;
|
adamc@1236
|
1719 #Restore arg saved
|
adamc@1220
|
1720 end
|
adamc@1216
|
1721 in
|
adamc@1236
|
1722 doQuery q
|
adamc@1216
|
1723 end
|
adamc@1220
|
1724 end
|
adamc@1220
|
1725
|
adamc@1211
|
1726 fun evalPat env e (pt, _) =
|
adamc@1211
|
1727 case pt of
|
adamc@1236
|
1728 PWild => env
|
adamc@1236
|
1729 | PVar _ => e :: env
|
adamc@1236
|
1730 | PPrim _ => env
|
adamc@1236
|
1731 | PCon (_, pc, NONE) => (St.assert [AReln (PCon0 (patCon pc), [e])]; env)
|
adamc@1211
|
1732 | PCon (_, pc, SOME pt) =>
|
adamc@1211
|
1733 let
|
adamc@1236
|
1734 val env = evalPat env (Func (UnCon (patCon pc), [e])) pt
|
adamc@1211
|
1735 in
|
adamc@1236
|
1736 St.assert [AReln (PCon1 (patCon pc), [e])];
|
adamc@1236
|
1737 env
|
adamc@1211
|
1738 end
|
adamc@1211
|
1739 | PRecord xpts =>
|
adamc@1236
|
1740 foldl (fn ((x, pt, _), env) => evalPat env (Proj (e, x)) pt) env xpts
|
adamc@1236
|
1741 | PNone _ => (St.assert [AReln (PCon0 "None", [e])]; env)
|
adamc@1211
|
1742 | PSome (_, pt) =>
|
adamc@1211
|
1743 let
|
adamc@1236
|
1744 val env = evalPat env (Func (UnCon "Some", [e])) pt
|
adamc@1211
|
1745 in
|
adamc@1236
|
1746 St.assert [AReln (PCon1 "Some", [e])];
|
adamc@1236
|
1747 env
|
adamc@1211
|
1748 end
|
adamc@1211
|
1749
|
adamc@1236
|
1750 fun evalExp env (e as (_, loc)) k =
|
adamc@1236
|
1751 let
|
adamc@1238
|
1752 (*val () = St.debug ()*)
|
adamc@1236
|
1753 (*val () = Print.preface ("evalExp", MonoPrint.p_exp MonoEnv.empty e)*)
|
adamc@1211
|
1754
|
adamc@1236
|
1755 fun default () = k (Var (St.nextVar ()))
|
adamc@1234
|
1756
|
adamc@1234
|
1757 fun doFfi (m, s, es) =
|
adamc@1234
|
1758 if m = "Basis" andalso SS.member (writers, s) then
|
adamc@1234
|
1759 let
|
adamc@1236
|
1760 fun doArgs es =
|
adamc@1236
|
1761 case es of
|
adamc@1236
|
1762 [] => k (Recd [])
|
adamc@1236
|
1763 | e :: es =>
|
adamc@1238
|
1764 evalExp env e (fn e => (St.send true (e, loc); doArgs es))
|
adamc@1234
|
1765 in
|
adamc@1236
|
1766 doArgs es
|
adamc@1234
|
1767 end
|
adamc@1234
|
1768 else if Settings.isEffectful (m, s) andalso not (Settings.isBenignEffectful (m, s)) then
|
adamc@1234
|
1769 default ()
|
adamc@1234
|
1770 else
|
adamc@1234
|
1771 let
|
adamc@1236
|
1772 fun doArgs (es, acc) =
|
adamc@1236
|
1773 case es of
|
adamc@1236
|
1774 [] => k (Func (Other (m ^ "." ^ s), rev acc))
|
adamc@1236
|
1775 | e :: es =>
|
adamc@1236
|
1776 evalExp env e (fn e => doArgs (es, e :: acc))
|
adamc@1234
|
1777 in
|
adamc@1236
|
1778 doArgs (es, [])
|
adamc@1234
|
1779 end
|
adamc@1200
|
1780 in
|
adamc@1200
|
1781 case #1 e of
|
adamc@1236
|
1782 EPrim p => k (Const p)
|
adamc@1236
|
1783 | ERel n => k (List.nth (env, n))
|
adamc@1200
|
1784 | ENamed _ => default ()
|
adamc@1236
|
1785 | ECon (_, pc, NONE) => k (Func (DtCon0 (patCon pc), []))
|
adamc@1236
|
1786 | ECon (_, pc, SOME e) => evalExp env e (fn e => k (Func (DtCon1 (patCon pc), [e])))
|
adamc@1236
|
1787 | ENone _ => k (Func (DtCon0 "None", []))
|
adamc@1236
|
1788 | ESome (_, e) => evalExp env e (fn e => k (Func (DtCon1 "Some", [e])))
|
adamc@1200
|
1789 | EFfi _ => default ()
|
adamc@1213
|
1790
|
adamc@1234
|
1791 | EFfiApp x => doFfi x
|
adamc@1234
|
1792 | EApp ((EFfi (m, s), _), e) => doFfi (m, s, [e])
|
adamc@1213
|
1793
|
adamc@1236
|
1794 | EApp (e1, e2) => evalExp env e1 (fn _ => evalExp env e2 (fn _ => default ()))
|
adamc@1213
|
1795
|
adamc@1200
|
1796 | EAbs _ => default ()
|
adamc@1236
|
1797 | EUnop (s, e1) => evalExp env e1 (fn e1 => k (Func (Other s, [e1])))
|
adamc@1236
|
1798 | EBinop (s, e1, e2) => evalExp env e1 (fn e1 => evalExp env e2 (fn e2 => k (Func (Other s, [e1, e2]))))
|
adamc@1200
|
1799 | ERecord xets =>
|
adamc@1200
|
1800 let
|
adamc@1236
|
1801 fun doFields (xes, acc) =
|
adamc@1236
|
1802 case xes of
|
adamc@1236
|
1803 [] => k (Recd (rev acc))
|
adamc@1236
|
1804 | (x, e, _) :: xes =>
|
adamc@1236
|
1805 evalExp env e (fn e => doFields (xes, (x, e) :: acc))
|
adamc@1200
|
1806 in
|
adamc@1236
|
1807 doFields (xets, [])
|
adamc@1200
|
1808 end
|
adamc@1236
|
1809 | EField (e, s) => evalExp env e (fn e => k (Proj (e, s)))
|
adamc@1218
|
1810 | ECase (e, pes, {result = res, ...}) =>
|
adamc@1236
|
1811 evalExp env e (fn e =>
|
adamc@1218
|
1812 let
|
adamc@1236
|
1813 val () = St.addPath (e, loc)
|
adamc@1218
|
1814 in
|
adamc@1236
|
1815 app (fn (p, pe) =>
|
adamc@1236
|
1816 let
|
adamc@1236
|
1817 val saved = St.stash ()
|
adamc@1236
|
1818 in
|
adamc@1238
|
1819 let
|
adamc@1238
|
1820 val env = evalPat env e p
|
adamc@1238
|
1821 in
|
adamc@1238
|
1822 evalExp env pe k;
|
adamc@1238
|
1823 St.reinstate saved
|
adamc@1238
|
1824 end
|
adamc@1238
|
1825 handle Cc.Contradiction => St.reinstate saved
|
adamc@1236
|
1826 end) pes
|
adamc@1238
|
1827 end)
|
adamc@1200
|
1828 | EStrcat (e1, e2) =>
|
adamc@1236
|
1829 evalExp env e1 (fn e1 =>
|
adamc@1236
|
1830 evalExp env e2 (fn e2 =>
|
adamc@1236
|
1831 k (Func (Other "cat", [e1, e2]))))
|
adamc@1238
|
1832 | EError (e, _) => evalExp env e (fn e => St.send true (e, loc))
|
adamc@1200
|
1833 | EReturnBlob {blob = b, mimeType = m, ...} =>
|
adamc@1236
|
1834 evalExp env b (fn b =>
|
adamc@1238
|
1835 (St.send true (b, loc);
|
adamc@1236
|
1836 evalExp env m
|
adamc@1238
|
1837 (fn m => St.send true (m, loc))))
|
adamc@1200
|
1838 | ERedirect (e, _) =>
|
adamc@1238
|
1839 evalExp env e (fn e => St.send true (e, loc))
|
adamc@1200
|
1840 | EWrite e =>
|
adamc@1238
|
1841 evalExp env e (fn e => (St.send true (e, loc);
|
adamc@1236
|
1842 k (Recd [])))
|
adamc@1200
|
1843 | ESeq (e1, e2) =>
|
adamc@1236
|
1844 evalExp env e1 (fn _ => evalExp env e2 k)
|
adamc@1200
|
1845 | ELet (_, _, e1, e2) =>
|
adamc@1236
|
1846 evalExp env e1 (fn e1 => evalExp (e1 :: env) e2 k)
|
adamc@1200
|
1847 | EClosure (n, es) =>
|
adamc@1200
|
1848 let
|
adamc@1236
|
1849 fun doArgs (es, acc) =
|
adamc@1236
|
1850 case es of
|
adamc@1236
|
1851 [] => k (Func (Other ("Cl" ^ Int.toString n), rev acc))
|
adamc@1236
|
1852 | e :: es =>
|
adamc@1236
|
1853 evalExp env e (fn e => doArgs (es, e :: acc))
|
adamc@1200
|
1854 in
|
adamc@1236
|
1855 doArgs (es, [])
|
adamc@1200
|
1856 end
|
adamc@1200
|
1857
|
adamc@1235
|
1858 | EQuery {query = q, body = b, initial = i, state = state, ...} =>
|
adamc@1238
|
1859 evalExp env i (fn i =>
|
adamc@1238
|
1860 let
|
adamc@1238
|
1861 val saved = St.stash ()
|
adamc@1200
|
1862
|
adamc@1238
|
1863 val () = (k i)
|
adamc@1238
|
1864 handle Cc.Contradiction => ()
|
adamc@1238
|
1865 val () = St.reinstate saved
|
adamc@1238
|
1866
|
adamc@1238
|
1867 val r = Var (St.nextVar ())
|
adamc@1238
|
1868 val acc = Var (St.nextVar ())
|
adamc@1242
|
1869
|
adamc@1242
|
1870 val touched = MonoUtil.Exp.fold {typ = fn (_, touched) => touched,
|
adamc@1242
|
1871 exp = fn (e, touched) =>
|
adamc@1242
|
1872 case e of
|
adamc@1242
|
1873 EDml e =>
|
adamc@1242
|
1874 (case parse dml e of
|
adamc@1242
|
1875 NONE => touched
|
adamc@1242
|
1876 | SOME c =>
|
adamc@1242
|
1877 case c of
|
adamc@1242
|
1878 Insert _ => touched
|
adamc@1242
|
1879 | Delete (tab, _) =>
|
adamc@1242
|
1880 SS.add (touched, tab)
|
adamc@1242
|
1881 | Update (tab, _, _) =>
|
adamc@1242
|
1882 SS.add (touched, tab))
|
adamc@1242
|
1883 | _ => touched}
|
adamc@1242
|
1884 SS.empty b
|
adamc@1238
|
1885 in
|
adamc@1242
|
1886 SS.app (St.havocReln o Sql) touched;
|
adamc@1242
|
1887
|
adamc@1242
|
1888 doQuery {Env = env,
|
adamc@1242
|
1889 NextVar = Var o St.nextVar,
|
adamc@1242
|
1890 Add = fn a => St.assert [a],
|
adamc@1242
|
1891 Save = St.stash,
|
adamc@1242
|
1892 Restore = St.reinstate,
|
adamc@1242
|
1893 UsedExp = fn (b, e) => St.send b (e, loc),
|
adamc@1242
|
1894 Cont = AllCols (fn x =>
|
adamc@1242
|
1895 (St.assert [AReln (Eq, [r, x])];
|
adamc@1242
|
1896 evalExp (acc :: r :: env) b k))} q
|
adamc@1238
|
1897 end)
|
adamc@1220
|
1898 | EDml e =>
|
adamc@1220
|
1899 (case parse dml e of
|
adamc@1220
|
1900 NONE => (print ("Warning: Information flow checker can't parse DML command at "
|
adamc@1220
|
1901 ^ ErrorMsg.spanToString loc ^ "\n");
|
adamc@1220
|
1902 default ())
|
adamc@1220
|
1903 | SOME d =>
|
adamc@1220
|
1904 case d of
|
adamc@1220
|
1905 Insert (tab, es) =>
|
adamc@1220
|
1906 let
|
adamc@1236
|
1907 val new = St.nextVar ()
|
adamc@1220
|
1908
|
adamc@1236
|
1909 val expIn = expIn (Var o St.nextVar) env
|
adamc@1236
|
1910 (fn _ => raise Fail "Iflow.evalExp: Bad field expression in INSERT [1]")
|
adamc@1220
|
1911
|
adamc@1236
|
1912 val es = map (fn (x, e) =>
|
adamc@1236
|
1913 case expIn e of
|
adamc@1236
|
1914 inl e => (x, e)
|
adamc@1236
|
1915 | inr _ => raise Fail "Iflow.evalExp: Bad field expression in INSERT [2]")
|
adamc@1236
|
1916 es
|
adamc@1220
|
1917
|
adamc@1236
|
1918 val saved = St.stash ()
|
adamc@1220
|
1919 in
|
adamc@1236
|
1920 St.assert [AReln (Sql (tab ^ "$New"), [Recd es])];
|
adamc@1236
|
1921 St.insert loc;
|
adamc@1236
|
1922 St.reinstate saved;
|
adamc@1236
|
1923 k (Recd [])
|
adamc@1221
|
1924 end
|
adamc@1221
|
1925 | Delete (tab, e) =>
|
adamc@1221
|
1926 let
|
adamc@1236
|
1927 val old = St.nextVar ()
|
adamc@1236
|
1928
|
adamc@1236
|
1929 val expIn = expIn (Var o St.nextVar) env
|
adamc@1236
|
1930 (fn "T" => Var old
|
adamc@1236
|
1931 | _ => raise Fail "Iflow.evalExp: Bad field expression in DELETE")
|
adamc@1221
|
1932
|
adamc@1236
|
1933 val p = case expIn e of
|
adamc@1236
|
1934 inl e => raise Fail "Iflow.evalExp: DELETE with non-boolean"
|
adamc@1236
|
1935 | inr p => p
|
adamc@1236
|
1936
|
adamc@1236
|
1937 val saved = St.stash ()
|
adamc@1221
|
1938 in
|
adamc@1238
|
1939 St.assert [AReln (Sql (tab ^ "$Old"), [Var old])];
|
adamc@1236
|
1940 decomp {Save = St.stash,
|
adamc@1236
|
1941 Restore = St.reinstate,
|
adamc@1236
|
1942 Add = fn a => St.assert [a]} p
|
adamc@1236
|
1943 (fn () => (St.delete loc;
|
adamc@1236
|
1944 St.reinstate saved;
|
adamc@1236
|
1945 St.havocReln (Sql tab);
|
adamc@1236
|
1946 k (Recd []))
|
adamc@1236
|
1947 handle Cc.Contradiction => ())
|
adamc@1223
|
1948 end
|
adamc@1223
|
1949 | Update (tab, fs, e) =>
|
adamc@1223
|
1950 let
|
adamc@1236
|
1951 val new = St.nextVar ()
|
adamc@1236
|
1952 val old = St.nextVar ()
|
adamc@1223
|
1953
|
adamc@1236
|
1954 val expIn = expIn (Var o St.nextVar) env
|
adamc@1236
|
1955 (fn "T" => Var old
|
adamc@1236
|
1956 | _ => raise Fail "Iflow.evalExp: Bad field expression in UPDATE")
|
adamc@1223
|
1957
|
adamc@1236
|
1958 val fs = map
|
adamc@1236
|
1959 (fn (x, e) =>
|
adamc@1236
|
1960 (x, case expIn e of
|
adamc@1236
|
1961 inl e => e
|
adamc@1236
|
1962 | inr _ => raise Fail
|
adamc@1236
|
1963 ("Iflow.evalExp: Selecting "
|
adamc@1236
|
1964 ^ "boolean expression")))
|
adamc@1236
|
1965 fs
|
adamc@1223
|
1966
|
adamc@1226
|
1967 val fs' = case SM.find (!tabs, tab) of
|
adamc@1224
|
1968 NONE => raise Fail "Iflow.evalExp: Updating unknown table"
|
adamc@1226
|
1969 | SOME (fs', _) => fs'
|
adamc@1224
|
1970
|
adamc@1224
|
1971 val fs = foldl (fn (f, fs) =>
|
adamc@1224
|
1972 if List.exists (fn (f', _) => f' = f) fs then
|
adamc@1224
|
1973 fs
|
adamc@1224
|
1974 else
|
adamc@1224
|
1975 (f, Proj (Var old, f)) :: fs) fs fs'
|
adamc@1224
|
1976
|
adamc@1236
|
1977 val p = case expIn e of
|
adamc@1236
|
1978 inl e => raise Fail "Iflow.evalExp: UPDATE with non-boolean"
|
adamc@1236
|
1979 | inr p => p
|
adamc@1236
|
1980 val saved = St.stash ()
|
adamc@1223
|
1981 in
|
adamc@1236
|
1982 St.assert [AReln (Sql (tab ^ "$New"), [Recd fs]),
|
adamc@1238
|
1983 AReln (Sql (tab ^ "$Old"), [Var old])];
|
adamc@1236
|
1984 decomp {Save = St.stash,
|
adamc@1236
|
1985 Restore = St.reinstate,
|
adamc@1236
|
1986 Add = fn a => St.assert [a]} p
|
adamc@1236
|
1987 (fn () => (St.update loc;
|
adamc@1236
|
1988 St.reinstate saved;
|
adamc@1236
|
1989 St.havocReln (Sql tab);
|
adamc@1236
|
1990 k (Recd []))
|
adamc@1236
|
1991 handle Cc.Contradiction => ())
|
adamc@1220
|
1992 end)
|
adamc@1220
|
1993
|
adamc@1229
|
1994 | ENextval (EPrim (Prim.String seq), _) =>
|
adamc@1229
|
1995 let
|
adamc@1236
|
1996 val nv = St.nextVar ()
|
adamc@1229
|
1997 in
|
adamc@1236
|
1998 St.assert [AReln (Sql (String.extract (seq, 3, NONE)), [Var nv])];
|
adamc@1236
|
1999 k (Var nv)
|
adamc@1229
|
2000 end
|
adamc@1200
|
2001 | ENextval _ => default ()
|
adamc@1200
|
2002 | ESetval _ => default ()
|
adamc@1200
|
2003
|
adamc@1238
|
2004 | EUnurlify ((EFfiApp ("Basis", "get_cookie", [(EPrim (Prim.String cname), _)]), _), _, _) =>
|
adamc@1217
|
2005 let
|
adamc@1238
|
2006 val e = Var (St.nextVar ())
|
adamc@1217
|
2007 in
|
adamc@1238
|
2008 St.assert [AReln (Known, [e])];
|
adamc@1238
|
2009 k e
|
adamc@1217
|
2010 end
|
adamc@1213
|
2011
|
adamc@1200
|
2012 | EUnurlify _ => default ()
|
adamc@1200
|
2013 | EJavaScript _ => default ()
|
adamc@1200
|
2014 | ESignalReturn _ => default ()
|
adamc@1200
|
2015 | ESignalBind _ => default ()
|
adamc@1200
|
2016 | ESignalSource _ => default ()
|
adamc@1200
|
2017 | EServerCall _ => default ()
|
adamc@1200
|
2018 | ERecv _ => default ()
|
adamc@1200
|
2019 | ESleep _ => default ()
|
adamc@1200
|
2020 | ESpawn _ => default ()
|
adamc@1200
|
2021 end
|
adamc@1200
|
2022
|
adamc@1200
|
2023 fun check file =
|
adamc@1200
|
2024 let
|
adamc@1236
|
2025 val () = St.reset ()
|
adamc@1236
|
2026
|
adamc@1213
|
2027 val file = MonoReduce.reduce file
|
adamc@1213
|
2028 val file = MonoOpt.optimize file
|
adamc@1213
|
2029 val file = Fuse.fuse file
|
adamc@1213
|
2030 val file = MonoOpt.optimize file
|
adamc@1216
|
2031 val file = MonoShake.shake file
|
adamc@1213
|
2032 (*val () = Print.preface ("File", MonoPrint.p_file MonoEnv.empty file)*)
|
adamc@1213
|
2033
|
adamc@1207
|
2034 val exptd = foldl (fn ((d, _), exptd) =>
|
adamc@1207
|
2035 case d of
|
adamc@1207
|
2036 DExport (_, _, n, _, _, _) => IS.add (exptd, n)
|
adamc@1207
|
2037 | _ => exptd) IS.empty file
|
adamc@1207
|
2038
|
adamc@1236
|
2039 fun decl (d, _) =
|
adamc@1200
|
2040 case d of
|
adamc@1226
|
2041 DTable (tab, fs, pk, _) =>
|
adamc@1226
|
2042 let
|
adamc@1226
|
2043 val ks =
|
adamc@1226
|
2044 case #1 pk of
|
adamc@1226
|
2045 EPrim (Prim.String s) =>
|
adamc@1226
|
2046 (case String.tokens (fn ch => ch = #"," orelse ch = #" ") s of
|
adamc@1226
|
2047 [] => []
|
adamc@1226
|
2048 | pk => [pk])
|
adamc@1226
|
2049 | _ => []
|
adamc@1226
|
2050 in
|
adamc@1226
|
2051 if size tab >= 3 then
|
adamc@1236
|
2052 tabs := SM.insert (!tabs, String.extract (tab, 3, NONE),
|
adamc@1236
|
2053 (map #1 fs,
|
adamc@1236
|
2054 map (map (fn s => str (Char.toUpper (String.sub (s, 3)))
|
adamc@1236
|
2055 ^ String.extract (s, 4, NONE))) ks))
|
adamc@1226
|
2056 else
|
adamc@1226
|
2057 raise Fail "Table name does not begin with uw_"
|
adamc@1226
|
2058 end
|
adamc@1238
|
2059 | DVal (x, n, _, e, _) =>
|
adamc@1200
|
2060 let
|
adamc@1238
|
2061 (*val () = print ("\n=== " ^ x ^ " ===\n\n");*)
|
adamc@1238
|
2062
|
adamc@1207
|
2063 val isExptd = IS.member (exptd, n)
|
adamc@1207
|
2064
|
adamc@1236
|
2065 val saved = St.stash ()
|
adamc@1236
|
2066
|
adamc@1236
|
2067 fun deAbs (e, env, ps) =
|
adamc@1200
|
2068 case #1 e of
|
adamc@1236
|
2069 EAbs (_, _, _, e) =>
|
adamc@1236
|
2070 let
|
adamc@1236
|
2071 val nv = Var (St.nextVar ())
|
adamc@1236
|
2072 in
|
adamc@1236
|
2073 deAbs (e, nv :: env,
|
adamc@1236
|
2074 if isExptd then
|
adamc@1236
|
2075 AReln (Known, [nv]) :: ps
|
adamc@1236
|
2076 else
|
adamc@1236
|
2077 ps)
|
adamc@1236
|
2078 end
|
adamc@1236
|
2079 | _ => (e, env, ps)
|
adamc@1200
|
2080
|
adamc@1236
|
2081 val (e, env, ps) = deAbs (e, [], [])
|
adamc@1200
|
2082 in
|
adamc@1236
|
2083 St.assert ps;
|
adamc@1236
|
2084 (evalExp env e (fn _ => ()) handle Cc.Contradiction => ());
|
adamc@1236
|
2085 St.reinstate saved
|
adamc@1200
|
2086 end
|
adamc@1202
|
2087
|
adamc@1220
|
2088 | DPolicy pol =>
|
adamc@1218
|
2089 let
|
adamc@1236
|
2090 val rvN = ref 0
|
adamc@1236
|
2091 fun rv () =
|
adamc@1236
|
2092 let
|
adamc@1236
|
2093 val n = !rvN
|
adamc@1236
|
2094 in
|
adamc@1236
|
2095 rvN := n + 1;
|
adamc@1236
|
2096 Lvar n
|
adamc@1236
|
2097 end
|
adamc@1236
|
2098
|
adamc@1236
|
2099 val atoms = ref ([] : atom list)
|
adamc@1236
|
2100 fun doQ k = doQuery {Env = [],
|
adamc@1236
|
2101 NextVar = rv,
|
adamc@1236
|
2102 Add = fn a => atoms := a :: !atoms,
|
adamc@1236
|
2103 Save = fn () => !atoms,
|
adamc@1236
|
2104 Restore = fn ls => atoms := ls,
|
adamc@1236
|
2105 UsedExp = fn _ => (),
|
adamc@1238
|
2106 Cont = SomeCol (fn r => k (rev (!atoms), r))}
|
adamc@1238
|
2107
|
adamc@1238
|
2108 fun untab tab = List.filter (fn AReln (Sql tab', _) => tab' <> tab
|
adamc@1238
|
2109 | _ => true)
|
adamc@1218
|
2110 in
|
adamc@1220
|
2111 case pol of
|
adamc@1220
|
2112 PolClient e =>
|
adamc@1238
|
2113 doQ (fn (ats, {Outs = es, ...}) => St.allowSend (ats, es)) e
|
adamc@1220
|
2114 | PolInsert e =>
|
adamc@1238
|
2115 doQ (fn (ats, {New = SOME (tab, new), ...}) =>
|
adamc@1238
|
2116 St.allowInsert (AReln (Sql (tab ^ "$New"), [new]) :: untab tab ats)
|
adamc@1238
|
2117 | _ => raise Fail "Iflow: No New in mayInsert policy") e
|
adamc@1221
|
2118 | PolDelete e =>
|
adamc@1238
|
2119 doQ (fn (ats, {Old = SOME (tab, old), ...}) =>
|
adamc@1238
|
2120 St.allowDelete (AReln (Sql (tab ^ "$Old"), [old]) :: untab tab ats)
|
adamc@1238
|
2121 | _ => raise Fail "Iflow: No Old in mayDelete policy") e
|
adamc@1223
|
2122 | PolUpdate e =>
|
adamc@1238
|
2123 doQ (fn (ats, {New = SOME (tab, new), Old = SOME (_, old), ...}) =>
|
adamc@1238
|
2124 St.allowUpdate (AReln (Sql (tab ^ "$Old"), [old])
|
adamc@1238
|
2125 :: AReln (Sql (tab ^ "$New"), [new])
|
adamc@1238
|
2126 :: untab tab ats)
|
adamc@1238
|
2127 | _ => raise Fail "Iflow: No New or Old in mayUpdate policy") e
|
adamc@1229
|
2128 | PolSequence e =>
|
adamc@1229
|
2129 (case #1 e of
|
adamc@1229
|
2130 EPrim (Prim.String seq) =>
|
adamc@1229
|
2131 let
|
adamc@1236
|
2132 val p = AReln (Sql (String.extract (seq, 3, NONE)), [Lvar 0])
|
adamc@1229
|
2133 val outs = [Lvar 0]
|
adamc@1229
|
2134 in
|
adamc@1236
|
2135 St.allowSend ([p], outs)
|
adamc@1229
|
2136 end
|
adamc@1236
|
2137 | _ => ())
|
adamc@1218
|
2138 end
|
adamc@1214
|
2139
|
adamc@1236
|
2140 | _ => ()
|
adamc@1200
|
2141 in
|
adamc@1236
|
2142 app decl file
|
adamc@1200
|
2143 end
|
adamc@1200
|
2144
|
adamc@1213
|
2145 val check = fn file =>
|
adamc@1213
|
2146 let
|
adamc@1213
|
2147 val oldInline = Settings.getMonoInline ()
|
adamc@1213
|
2148 in
|
adamc@1213
|
2149 (Settings.setMonoInline (case Int.maxInt of
|
adamc@1213
|
2150 NONE => 1000000
|
adamc@1213
|
2151 | SOME n => n);
|
adamc@1213
|
2152 check file;
|
adamc@1213
|
2153 Settings.setMonoInline oldInline)
|
adamc@1213
|
2154 handle ex => (Settings.setMonoInline oldInline;
|
adamc@1213
|
2155 raise ex)
|
adamc@1213
|
2156 end
|
adamc@1213
|
2157
|
adamc@1200
|
2158 end
|