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
|
adamc@1215
|
237 val database : unit -> database
|
adamc@1236
|
238 val clear : database -> unit
|
adamc@1215
|
239
|
adamc@1215
|
240 val assert : database * atom -> unit
|
adamc@1215
|
241 val check : database * atom -> bool
|
adamc@1215
|
242
|
adamc@1215
|
243 val p_database : database Print.printer
|
adamc@1218
|
244
|
adamc@1253
|
245 val builtFrom : database * {Base : exp list, Derived : exp} -> bool
|
adamc@1226
|
246
|
adamc@1226
|
247 val p_repOf : database -> exp Print.printer
|
adamc@1208
|
248 end = struct
|
adamc@1208
|
249
|
adamc@1244
|
250 local
|
adamc@1244
|
251 val count = ref 0
|
adamc@1244
|
252 in
|
adamc@1244
|
253 fun nodeId () =
|
adamc@1244
|
254 let
|
adamc@1244
|
255 val n = !count
|
adamc@1244
|
256 in
|
adamc@1244
|
257 count := n + 1;
|
adamc@1244
|
258 n
|
adamc@1244
|
259 end
|
adamc@1244
|
260 end
|
adamc@1244
|
261
|
adamc@1215
|
262 exception Contradiction
|
adamc@1215
|
263 exception Undetermined
|
adamc@1208
|
264
|
adamc@1215
|
265 structure CM = BinaryMapFn(struct
|
adamc@1215
|
266 type ord_key = Prim.t
|
adamc@1215
|
267 val compare = Prim.compare
|
adamc@1215
|
268 end)
|
adamc@1208
|
269
|
adamc@1244
|
270 datatype node = Node of {Id : int,
|
adamc@1244
|
271 Rep : node ref option ref,
|
adamc@1215
|
272 Cons : node ref SM.map ref,
|
adamc@1215
|
273 Variety : variety,
|
adamc@1245
|
274 Known : bool ref,
|
adamc@1245
|
275 Ge : Int64.int option ref}
|
adamc@1208
|
276
|
adamc@1215
|
277 and variety =
|
adamc@1215
|
278 Dt0 of string
|
adamc@1215
|
279 | Dt1 of string * node ref
|
adamc@1215
|
280 | Prim of Prim.t
|
adamc@1221
|
281 | Recrd of node ref SM.map ref * bool
|
adamc@1215
|
282 | Nothing
|
adamc@1208
|
283
|
adamc@1215
|
284 type representative = node ref
|
adamc@1215
|
285
|
adamc@1215
|
286 type database = {Vars : representative IM.map ref,
|
adamc@1215
|
287 Consts : representative CM.map ref,
|
adamc@1215
|
288 Con0s : representative SM.map ref,
|
adamc@1215
|
289 Records : (representative SM.map * representative) list ref,
|
adamc@1229
|
290 Funcs : ((string * representative list) * representative) list ref}
|
adamc@1215
|
291
|
adamc@1215
|
292 fun database () = {Vars = ref IM.empty,
|
adamc@1215
|
293 Consts = ref CM.empty,
|
adamc@1215
|
294 Con0s = ref SM.empty,
|
adamc@1215
|
295 Records = ref [],
|
adamc@1215
|
296 Funcs = ref []}
|
adamc@1215
|
297
|
adamc@1236
|
298 fun clear (t : database) = (#Vars t := IM.empty;
|
adamc@1236
|
299 #Consts t := CM.empty;
|
adamc@1236
|
300 #Con0s t := SM.empty;
|
adamc@1236
|
301 #Records t := [];
|
adamc@1236
|
302 #Funcs t := [])
|
adamc@1236
|
303
|
adamc@1215
|
304 fun unNode n =
|
adamc@1215
|
305 case !n of
|
adamc@1215
|
306 Node r => r
|
adamc@1215
|
307
|
adamc@1215
|
308 open Print
|
adamc@1215
|
309 val string = PD.string
|
adamc@1215
|
310 val newline = PD.newline
|
adamc@1215
|
311
|
adamc@1215
|
312 fun p_rep n =
|
adamc@1215
|
313 case !(#Rep (unNode n)) of
|
adamc@1215
|
314 SOME n => p_rep n
|
adamc@1215
|
315 | NONE =>
|
adamc@1244
|
316 box [string (Int.toString (#Id (unNode n)) ^ ":"),
|
adamc@1244
|
317 space,
|
adamc@1221
|
318 case #Variety (unNode n) of
|
adamc@1221
|
319 Nothing => string "?"
|
adamc@1221
|
320 | Dt0 s => string ("Dt0(" ^ s ^ ")")
|
adamc@1221
|
321 | Dt1 (s, n) => box[string ("Dt1(" ^ s ^ ","),
|
adamc@1221
|
322 space,
|
adamc@1221
|
323 p_rep n,
|
adamc@1221
|
324 string ")"]
|
adamc@1221
|
325 | Prim p => Prim.p_t p
|
adamc@1221
|
326 | Recrd (ref m, b) => box [string "{",
|
adamc@1221
|
327 p_list (fn (x, n) => box [string x,
|
adamc@1221
|
328 space,
|
adamc@1221
|
329 string "=",
|
adamc@1221
|
330 space,
|
adamc@1221
|
331 p_rep n]) (SM.listItemsi m),
|
adamc@1221
|
332 string "}",
|
adamc@1221
|
333 if b then
|
adamc@1221
|
334 box [space,
|
adamc@1221
|
335 string "(complete)"]
|
adamc@1221
|
336 else
|
adamc@1245
|
337 box []],
|
adamc@1245
|
338 if !(#Known (unNode n)) then
|
adamc@1245
|
339 string " (known)"
|
adamc@1245
|
340 else
|
adamc@1245
|
341 box [],
|
adamc@1245
|
342 case !(#Ge (unNode n)) of
|
adamc@1245
|
343 NONE => box []
|
adamc@1245
|
344 | SOME n => string (" (>= " ^ Int64.toString n ^ ")")]
|
adamc@1215
|
345
|
adamc@1215
|
346 fun p_database (db : database) =
|
adamc@1215
|
347 box [string "Vars:",
|
adamc@1215
|
348 newline,
|
adamc@1215
|
349 p_list_sep newline (fn (i, n) => box [string ("x" ^ Int.toString i),
|
adamc@1215
|
350 space,
|
adamc@1215
|
351 string "=",
|
adamc@1215
|
352 space,
|
adamc@1245
|
353 p_rep n]) (IM.listItemsi (!(#Vars db)))]
|
adamc@1215
|
354
|
adamc@1215
|
355 fun repOf (n : representative) : representative =
|
adamc@1215
|
356 case !(#Rep (unNode n)) of
|
adamc@1215
|
357 NONE => n
|
adamc@1215
|
358 | SOME r =>
|
adamc@1215
|
359 let
|
adamc@1215
|
360 val r = repOf r
|
adamc@1215
|
361 in
|
adamc@1215
|
362 #Rep (unNode n) := SOME r;
|
adamc@1215
|
363 r
|
adamc@1215
|
364 end
|
adamc@1215
|
365
|
adamc@1215
|
366 fun markKnown r =
|
adamc@1221
|
367 let
|
adamc@1221
|
368 val r = repOf r
|
adamc@1221
|
369 in
|
adamc@1221
|
370 (*Print.preface ("markKnown", p_rep r);*)
|
adamc@1221
|
371 if !(#Known (unNode r)) then
|
adamc@1221
|
372 ()(*TextIO.print "Already known\n"*)
|
adamc@1221
|
373 else
|
adamc@1221
|
374 (#Known (unNode r) := true;
|
adamc@1221
|
375 SM.app markKnown (!(#Cons (unNode r)));
|
adamc@1221
|
376 case #Variety (unNode r) of
|
adamc@1221
|
377 Dt1 (_, r) => markKnown r
|
adamc@1221
|
378 | Recrd (xes, _) => SM.app markKnown (!xes)
|
adamc@1221
|
379 | _ => ())
|
adamc@1221
|
380 end
|
adamc@1215
|
381
|
adamc@1215
|
382 fun representative (db : database, e) =
|
adamc@1208
|
383 let
|
adamc@1215
|
384 fun rep e =
|
adamc@1215
|
385 case e of
|
adamc@1215
|
386 Const p => (case CM.find (!(#Consts db), p) of
|
adamc@1215
|
387 SOME r => repOf r
|
adamc@1215
|
388 | NONE =>
|
adamc@1215
|
389 let
|
adamc@1244
|
390 val r = ref (Node {Id = nodeId (),
|
adamc@1244
|
391 Rep = ref NONE,
|
adamc@1215
|
392 Cons = ref SM.empty,
|
adamc@1215
|
393 Variety = Prim p,
|
adamc@1245
|
394 Known = ref true,
|
adamc@1245
|
395 Ge = ref (case p of
|
adamc@1245
|
396 Prim.Int n => SOME n
|
adamc@1245
|
397 | _ => NONE)})
|
adamc@1215
|
398 in
|
adamc@1215
|
399 #Consts db := CM.insert (!(#Consts db), p, r);
|
adamc@1215
|
400 r
|
adamc@1215
|
401 end)
|
adamc@1215
|
402 | Var n => (case IM.find (!(#Vars db), n) of
|
adamc@1215
|
403 SOME r => repOf r
|
adamc@1215
|
404 | NONE =>
|
adamc@1215
|
405 let
|
adamc@1244
|
406 val r = ref (Node {Id = nodeId (),
|
adamc@1244
|
407 Rep = ref NONE,
|
adamc@1215
|
408 Cons = ref SM.empty,
|
adamc@1215
|
409 Variety = Nothing,
|
adamc@1245
|
410 Known = ref false,
|
adamc@1245
|
411 Ge = ref NONE})
|
adamc@1215
|
412 in
|
adamc@1215
|
413 #Vars db := IM.insert (!(#Vars db), n, r);
|
adamc@1215
|
414 r
|
adamc@1215
|
415 end)
|
adamc@1236
|
416 | Lvar _ => raise Undetermined
|
adamc@1215
|
417 | Func (DtCon0 f, []) => (case SM.find (!(#Con0s db), f) of
|
adamc@1215
|
418 SOME r => repOf r
|
adamc@1215
|
419 | NONE =>
|
adamc@1215
|
420 let
|
adamc@1244
|
421 val r = ref (Node {Id = nodeId (),
|
adamc@1244
|
422 Rep = ref NONE,
|
adamc@1215
|
423 Cons = ref SM.empty,
|
adamc@1215
|
424 Variety = Dt0 f,
|
adamc@1245
|
425 Known = ref true,
|
adamc@1245
|
426 Ge = ref NONE})
|
adamc@1215
|
427 in
|
adamc@1215
|
428 #Con0s db := SM.insert (!(#Con0s db), f, r);
|
adamc@1215
|
429 r
|
adamc@1215
|
430 end)
|
adamc@1215
|
431 | Func (DtCon0 _, _) => raise Fail "Iflow.rep: DtCon0"
|
adamc@1215
|
432 | Func (DtCon1 f, [e]) =>
|
adamc@1215
|
433 let
|
adamc@1215
|
434 val r = rep e
|
adamc@1215
|
435 in
|
adamc@1215
|
436 case SM.find (!(#Cons (unNode r)), f) of
|
adamc@1215
|
437 SOME r => repOf r
|
adamc@1215
|
438 | NONE =>
|
adamc@1215
|
439 let
|
adamc@1244
|
440 val r' = ref (Node {Id = nodeId (),
|
adamc@1244
|
441 Rep = ref NONE,
|
adamc@1215
|
442 Cons = ref SM.empty,
|
adamc@1215
|
443 Variety = Dt1 (f, r),
|
adamc@1245
|
444 Known = ref (!(#Known (unNode r))),
|
adamc@1245
|
445 Ge = ref NONE})
|
adamc@1215
|
446 in
|
adamc@1215
|
447 #Cons (unNode r) := SM.insert (!(#Cons (unNode r)), f, r');
|
adamc@1215
|
448 r'
|
adamc@1215
|
449 end
|
adamc@1215
|
450 end
|
adamc@1215
|
451 | Func (DtCon1 _, _) => raise Fail "Iflow.rep: DtCon1"
|
adamc@1215
|
452 | Func (UnCon f, [e]) =>
|
adamc@1215
|
453 let
|
adamc@1215
|
454 val r = rep e
|
adamc@1215
|
455 in
|
adamc@1215
|
456 case #Variety (unNode r) of
|
adamc@1215
|
457 Dt1 (f', n) => if f' = f then
|
adamc@1215
|
458 repOf n
|
adamc@1215
|
459 else
|
adamc@1215
|
460 raise Contradiction
|
adamc@1215
|
461 | Nothing =>
|
adamc@1215
|
462 let
|
adamc@1215
|
463 val cons = ref SM.empty
|
adamc@1244
|
464 val r' = ref (Node {Id = nodeId (),
|
adamc@1244
|
465 Rep = ref NONE,
|
adamc@1215
|
466 Cons = cons,
|
adamc@1215
|
467 Variety = Nothing,
|
adamc@1245
|
468 Known = ref (!(#Known (unNode r))),
|
adamc@1245
|
469 Ge = ref NONE})
|
adamc@1215
|
470
|
adamc@1244
|
471 val r'' = ref (Node {Id = nodeId (),
|
adamc@1244
|
472 Rep = ref NONE,
|
adamc@1215
|
473 Cons = #Cons (unNode r),
|
adamc@1215
|
474 Variety = Dt1 (f, r'),
|
adamc@1245
|
475 Known = #Known (unNode r),
|
adamc@1245
|
476 Ge = ref NONE})
|
adamc@1215
|
477 in
|
adamc@1215
|
478 cons := SM.insert (!cons, f, r'');
|
adamc@1215
|
479 #Rep (unNode r) := SOME r'';
|
adamc@1215
|
480 r'
|
adamc@1215
|
481 end
|
adamc@1215
|
482 | _ => raise Contradiction
|
adamc@1215
|
483 end
|
adamc@1215
|
484 | Func (UnCon _, _) => raise Fail "Iflow.rep: UnCon"
|
adamc@1215
|
485 | Func (Other f, es) =>
|
adamc@1215
|
486 let
|
adamc@1215
|
487 val rs = map rep es
|
adamc@1215
|
488 in
|
adamc@1215
|
489 case List.find (fn (x : string * representative list, _) => x = (f, rs)) (!(#Funcs db)) of
|
adamc@1215
|
490 NONE =>
|
adamc@1215
|
491 let
|
adamc@1244
|
492 val r = ref (Node {Id = nodeId (),
|
adamc@1244
|
493 Rep = ref NONE,
|
adamc@1215
|
494 Cons = ref SM.empty,
|
adamc@1215
|
495 Variety = Nothing,
|
adamc@1252
|
496 Known = ref (f = "allow"),
|
adamc@1245
|
497 Ge = ref NONE})
|
adamc@1215
|
498 in
|
adamc@1215
|
499 #Funcs db := ((f, rs), r) :: (!(#Funcs db));
|
adamc@1215
|
500 r
|
adamc@1215
|
501 end
|
adamc@1215
|
502 | SOME (_, r) => repOf r
|
adamc@1215
|
503 end
|
adamc@1215
|
504 | Recd xes =>
|
adamc@1215
|
505 let
|
adamc@1215
|
506 val xes = map (fn (x, e) => (x, rep e)) xes
|
adamc@1215
|
507 val len = length xes
|
adamc@1215
|
508 in
|
adamc@1215
|
509 case List.find (fn (xes', _) =>
|
adamc@1215
|
510 SM.numItems xes' = len
|
adamc@1215
|
511 andalso List.all (fn (x, n) =>
|
adamc@1215
|
512 case SM.find (xes', x) of
|
adamc@1215
|
513 NONE => false
|
adamc@1215
|
514 | SOME n' => n = repOf n') xes)
|
adamc@1215
|
515 (!(#Records db)) of
|
adamc@1215
|
516 SOME (_, r) => repOf r
|
adamc@1215
|
517 | NONE =>
|
adamc@1215
|
518 let
|
adamc@1215
|
519 val xes = foldl SM.insert' SM.empty xes
|
adamc@1215
|
520
|
adamc@1244
|
521 val r' = ref (Node {Id = nodeId (),
|
adamc@1244
|
522 Rep = ref NONE,
|
adamc@1215
|
523 Cons = ref SM.empty,
|
adamc@1221
|
524 Variety = Recrd (ref xes, true),
|
adamc@1245
|
525 Known = ref false,
|
adamc@1245
|
526 Ge = ref NONE})
|
adamc@1215
|
527 in
|
adamc@1215
|
528 #Records db := (xes, r') :: (!(#Records db));
|
adamc@1215
|
529 r'
|
adamc@1215
|
530 end
|
adamc@1215
|
531 end
|
adamc@1215
|
532 | Proj (e, f) =>
|
adamc@1215
|
533 let
|
adamc@1215
|
534 val r = rep e
|
adamc@1215
|
535 in
|
adamc@1215
|
536 case #Variety (unNode r) of
|
adamc@1221
|
537 Recrd (xes, _) =>
|
adamc@1215
|
538 (case SM.find (!xes, f) of
|
adamc@1215
|
539 SOME r => repOf r
|
adamc@1216
|
540 | NONE => let
|
adamc@1244
|
541 val r = ref (Node {Id = nodeId (),
|
adamc@1244
|
542 Rep = ref NONE,
|
adamc@1215
|
543 Cons = ref SM.empty,
|
adamc@1215
|
544 Variety = Nothing,
|
adamc@1245
|
545 Known = ref (!(#Known (unNode r))),
|
adamc@1245
|
546 Ge = ref NONE})
|
adamc@1215
|
547 in
|
adamc@1215
|
548 xes := SM.insert (!xes, f, r);
|
adamc@1215
|
549 r
|
adamc@1215
|
550 end)
|
adamc@1215
|
551 | Nothing =>
|
adamc@1215
|
552 let
|
adamc@1244
|
553 val r' = ref (Node {Id = nodeId (),
|
adamc@1244
|
554 Rep = ref NONE,
|
adamc@1215
|
555 Cons = ref SM.empty,
|
adamc@1215
|
556 Variety = Nothing,
|
adamc@1245
|
557 Known = ref (!(#Known (unNode r))),
|
adamc@1245
|
558 Ge = ref NONE})
|
adamc@1215
|
559
|
adamc@1244
|
560 val r'' = ref (Node {Id = nodeId (),
|
adamc@1244
|
561 Rep = ref NONE,
|
adamc@1215
|
562 Cons = #Cons (unNode r),
|
adamc@1221
|
563 Variety = Recrd (ref (SM.insert (SM.empty, f, r')), false),
|
adamc@1245
|
564 Known = #Known (unNode r),
|
adamc@1245
|
565 Ge = ref NONE})
|
adamc@1215
|
566 in
|
adamc@1215
|
567 #Rep (unNode r) := SOME r'';
|
adamc@1215
|
568 r'
|
adamc@1215
|
569 end
|
adamc@1215
|
570 | _ => raise Contradiction
|
adamc@1215
|
571 end
|
adamc@1208
|
572 in
|
adamc@1215
|
573 rep e
|
adamc@1208
|
574 end
|
adamc@1208
|
575
|
adamc@1226
|
576 fun p_repOf db e = p_rep (representative (db, e))
|
adamc@1226
|
577
|
adamc@1215
|
578 fun assert (db, a) =
|
adamc@1243
|
579 let
|
adamc@1243
|
580 fun markEq (r1, r2) =
|
adamc@1215
|
581 let
|
adamc@1243
|
582 val r1 = repOf r1
|
adamc@1243
|
583 val r2 = repOf r2
|
adamc@1215
|
584 in
|
adamc@1243
|
585 if r1 = r2 then
|
adamc@1243
|
586 ()
|
adamc@1243
|
587 else case (#Variety (unNode r1), #Variety (unNode r2)) of
|
adamc@1243
|
588 (Prim p1, Prim p2) => if Prim.equal (p1, p2) then
|
adamc@1243
|
589 ()
|
adamc@1243
|
590 else
|
adamc@1243
|
591 raise Contradiction
|
adamc@1243
|
592 | (Dt0 f1, Dt0 f2) => if f1 = f2 then
|
adamc@1243
|
593 ()
|
adamc@1243
|
594 else
|
adamc@1243
|
595 raise Contradiction
|
adamc@1243
|
596 | (Dt1 (f1, r1), Dt1 (f2, r2)) => if f1 = f2 then
|
adamc@1243
|
597 markEq (r1, r2)
|
adamc@1243
|
598 else
|
adamc@1243
|
599 raise Contradiction
|
adamc@1243
|
600 | (Recrd (xes1, _), Recrd (xes2, _)) =>
|
adamc@1243
|
601 let
|
adamc@1243
|
602 fun unif (xes1, xes2) =
|
adamc@1243
|
603 SM.appi (fn (x, r1) =>
|
adamc@1243
|
604 case SM.find (!xes2, x) of
|
adamc@1243
|
605 NONE => xes2 := SM.insert (!xes2, x, r1)
|
adamc@1243
|
606 | SOME r2 => markEq (r1, r2)) (!xes1)
|
adamc@1243
|
607 in
|
adamc@1243
|
608 unif (xes1, xes2);
|
adamc@1243
|
609 unif (xes2, xes1)
|
adamc@1243
|
610 end
|
adamc@1243
|
611 | (Nothing, _) => mergeNodes (r1, r2)
|
adamc@1243
|
612 | (_, Nothing) => mergeNodes (r2, r1)
|
adamc@1243
|
613 | _ => raise Contradiction
|
adamc@1215
|
614 end
|
adamc@1243
|
615
|
adamc@1243
|
616 and mergeNodes (r1, r2) =
|
adamc@1243
|
617 (#Rep (unNode r1) := SOME r2;
|
adamc@1243
|
618 if !(#Known (unNode r1)) then
|
adamc@1243
|
619 markKnown r2
|
adamc@1243
|
620 else
|
adamc@1243
|
621 ();
|
adamc@1243
|
622 if !(#Known (unNode r2)) then
|
adamc@1243
|
623 markKnown r1
|
adamc@1243
|
624 else
|
adamc@1243
|
625 ();
|
adamc@1243
|
626 #Cons (unNode r2) := SM.unionWith #1 (!(#Cons (unNode r2)), !(#Cons (unNode r1)));
|
adamc@1243
|
627
|
adamc@1245
|
628 case !(#Ge (unNode r1)) of
|
adamc@1245
|
629 NONE => ()
|
adamc@1245
|
630 | SOME n1 =>
|
adamc@1245
|
631 case !(#Ge (unNode r2)) of
|
adamc@1245
|
632 NONE => #Ge (unNode r2) := SOME n1
|
adamc@1245
|
633 | SOME n2 => #Ge (unNode r2) := SOME (Int64.max (n1, n2));
|
adamc@1245
|
634
|
adamc@1243
|
635 compactFuncs ())
|
adamc@1243
|
636
|
adamc@1243
|
637 and compactFuncs () =
|
adamc@1215
|
638 let
|
adamc@1243
|
639 fun loop funcs =
|
adamc@1243
|
640 case funcs of
|
adamc@1243
|
641 [] => []
|
adamc@1243
|
642 | (fr as ((f, rs), r)) :: rest =>
|
adamc@1243
|
643 let
|
adamc@1243
|
644 val rest = List.filter (fn ((f' : string, rs'), r') =>
|
adamc@1243
|
645 if f' = f
|
adamc@1243
|
646 andalso ListPair.allEq (fn (r1, r2) =>
|
adamc@1243
|
647 repOf r1 = repOf r2)
|
adamc@1243
|
648 (rs, rs') then
|
adamc@1243
|
649 (markEq (r, r');
|
adamc@1243
|
650 false)
|
adamc@1243
|
651 else
|
adamc@1243
|
652 true) rest
|
adamc@1243
|
653 in
|
adamc@1243
|
654 fr :: loop rest
|
adamc@1243
|
655 end
|
adamc@1215
|
656 in
|
adamc@1243
|
657 #Funcs db := loop (!(#Funcs db))
|
adamc@1243
|
658 end
|
adamc@1243
|
659 in
|
adamc@1243
|
660 case a of
|
adamc@1243
|
661 ACond _ => ()
|
adamc@1243
|
662 | AReln x =>
|
adamc@1243
|
663 case x of
|
adamc@1243
|
664 (Known, [e]) =>
|
adamc@1243
|
665 ((*Print.prefaces "Before" [("e", p_exp e),
|
adamc@1243
|
666 ("db", p_database db)];*)
|
adamc@1243
|
667 markKnown (representative (db, e))(*;
|
adamc@1243
|
668 Print.prefaces "After" [("e", p_exp e),
|
adamc@1243
|
669 ("db", p_database db)]*))
|
adamc@1243
|
670 | (PCon0 f, [e]) =>
|
adamc@1243
|
671 let
|
adamc@1243
|
672 val r = representative (db, e)
|
adamc@1243
|
673 in
|
adamc@1243
|
674 case #Variety (unNode r) of
|
adamc@1243
|
675 Dt0 f' => if f = f' then
|
adamc@1243
|
676 ()
|
adamc@1243
|
677 else
|
adamc@1243
|
678 raise Contradiction
|
adamc@1243
|
679 | Nothing =>
|
adamc@1243
|
680 (case SM.find (!(#Con0s db), f) of
|
adamc@1243
|
681 SOME r' => markEq (r, r')
|
adamc@1243
|
682 | NONE =>
|
adamc@1243
|
683 let
|
adamc@1244
|
684 val r' = ref (Node {Id = nodeId (),
|
adamc@1244
|
685 Rep = ref NONE,
|
adamc@1243
|
686 Cons = ref SM.empty,
|
adamc@1243
|
687 Variety = Dt0 f,
|
adamc@1245
|
688 Known = ref false,
|
adamc@1245
|
689 Ge = ref NONE})
|
adamc@1243
|
690 in
|
adamc@1243
|
691 #Rep (unNode r) := SOME r';
|
adamc@1243
|
692 #Con0s db := SM.insert (!(#Con0s db), f, r')
|
adamc@1243
|
693 end)
|
adamc@1243
|
694 | _ => raise Contradiction
|
adamc@1243
|
695 end
|
adamc@1243
|
696 | (PCon1 f, [e]) =>
|
adamc@1243
|
697 let
|
adamc@1243
|
698 val r = representative (db, e)
|
adamc@1243
|
699 in
|
adamc@1243
|
700 case #Variety (unNode r) of
|
adamc@1243
|
701 Dt1 (f', e') => if f = f' then
|
adamc@1243
|
702 ()
|
adamc@1243
|
703 else
|
adamc@1243
|
704 raise Contradiction
|
adamc@1243
|
705 | Nothing =>
|
adamc@1243
|
706 let
|
adamc@1253
|
707 val cons = ref SM.empty
|
adamc@1253
|
708
|
adamc@1244
|
709 val r'' = ref (Node {Id = nodeId (),
|
adamc@1244
|
710 Rep = ref NONE,
|
adamc@1253
|
711 Cons = cons,
|
adamc@1243
|
712 Variety = Nothing,
|
adamc@1245
|
713 Known = ref (!(#Known (unNode r))),
|
adamc@1245
|
714 Ge = ref NONE})
|
adamc@1214
|
715
|
adamc@1244
|
716 val r' = ref (Node {Id = nodeId (),
|
adamc@1244
|
717 Rep = ref NONE,
|
adamc@1243
|
718 Cons = ref SM.empty,
|
adamc@1243
|
719 Variety = Dt1 (f, r''),
|
adamc@1245
|
720 Known = #Known (unNode r),
|
adamc@1245
|
721 Ge = ref NONE})
|
adamc@1243
|
722 in
|
adamc@1253
|
723 cons := SM.insert (!cons, f, r');
|
adamc@1243
|
724 #Rep (unNode r) := SOME r'
|
adamc@1243
|
725 end
|
adamc@1243
|
726 | _ => raise Contradiction
|
adamc@1243
|
727 end
|
adamc@1243
|
728 | (Eq, [e1, e2]) =>
|
adamc@1215
|
729 markEq (representative (db, e1), representative (db, e2))
|
adamc@1245
|
730 | (Ge, [e1, e2]) =>
|
adamc@1245
|
731 let
|
adamc@1245
|
732 val r1 = representative (db, e1)
|
adamc@1245
|
733 val r2 = representative (db, e2)
|
adamc@1245
|
734 in
|
adamc@1245
|
735 case !(#Ge (unNode (repOf r2))) of
|
adamc@1245
|
736 NONE => ()
|
adamc@1245
|
737 | SOME n2 =>
|
adamc@1245
|
738 case !(#Ge (unNode (repOf r1))) of
|
adamc@1245
|
739 NONE => #Ge (unNode (repOf r1)) := SOME n2
|
adamc@1245
|
740 | SOME n1 => #Ge (unNode (repOf r1)) := SOME (Int64.max (n1, n2))
|
adamc@1245
|
741 end
|
adamc@1243
|
742 | _ => ()
|
adamc@1247
|
743 end handle Undetermined => ()
|
adamc@1214
|
744
|
adamc@1215
|
745 fun check (db, a) =
|
adamc@1247
|
746 (case a of
|
adamc@1247
|
747 ACond _ => false
|
adamc@1247
|
748 | AReln x =>
|
adamc@1247
|
749 case x of
|
adamc@1247
|
750 (Known, [e]) =>
|
adamc@1247
|
751 let
|
adamc@1247
|
752 fun isKnown r =
|
adamc@1247
|
753 let
|
adamc@1247
|
754 val r = repOf r
|
adamc@1247
|
755 in
|
adamc@1247
|
756 !(#Known (unNode r))
|
adamc@1247
|
757 orelse case #Variety (unNode r) of
|
adamc@1247
|
758 Dt1 (_, r) => isKnown r
|
adamc@1247
|
759 | Recrd (xes, true) => List.all isKnown (SM.listItems (!xes))
|
adamc@1247
|
760 | _ => false
|
adamc@1247
|
761 end
|
adamc@1221
|
762
|
adamc@1247
|
763 val r = representative (db, e)
|
adamc@1247
|
764 in
|
adamc@1247
|
765 isKnown r
|
adamc@1247
|
766 end
|
adamc@1247
|
767 | (PCon0 f, [e]) =>
|
adamc@1247
|
768 (case #Variety (unNode (representative (db, e))) of
|
adamc@1247
|
769 Dt0 f' => f' = f
|
adamc@1247
|
770 | _ => false)
|
adamc@1247
|
771 | (PCon1 f, [e]) =>
|
adamc@1247
|
772 (case #Variety (unNode (representative (db, e))) of
|
adamc@1247
|
773 Dt1 (f', _) => f' = f
|
adamc@1247
|
774 | _ => false)
|
adamc@1247
|
775 | (Eq, [e1, e2]) =>
|
adamc@1247
|
776 let
|
adamc@1247
|
777 val r1 = representative (db, e1)
|
adamc@1247
|
778 val r2 = representative (db, e2)
|
adamc@1247
|
779 in
|
adamc@1247
|
780 repOf r1 = repOf r2
|
adamc@1247
|
781 end
|
adamc@1247
|
782 | (Ge, [e1, e2]) =>
|
adamc@1247
|
783 let
|
adamc@1247
|
784 val r1 = representative (db, e1)
|
adamc@1247
|
785 val r2 = representative (db, e2)
|
adamc@1247
|
786 in
|
adamc@1247
|
787 case (!(#Ge (unNode (repOf r1))), #Variety (unNode (repOf r2))) of
|
adamc@1247
|
788 (SOME n1, Prim (Prim.Int n2)) => Int64.>= (n1, n2)
|
adamc@1247
|
789 | _ => false
|
adamc@1247
|
790 end
|
adamc@1247
|
791 | _ => false)
|
adamc@1247
|
792 handle Undetermined => false
|
adamc@1212
|
793
|
adamc@1253
|
794 fun builtFrom (db, {Base = bs, Derived = d}) =
|
adamc@1218
|
795 let
|
adamc@1218
|
796 val bs = map (fn b => representative (db, b)) bs
|
adamc@1218
|
797
|
adamc@1218
|
798 fun loop d =
|
adamc@1218
|
799 let
|
adamc@1218
|
800 val d = repOf d
|
adamc@1218
|
801 in
|
adamc@1253
|
802 !(#Known (unNode d))
|
adamc@1238
|
803 orelse List.exists (fn b => repOf b = d) bs
|
adamc@1246
|
804 orelse (case #Variety (unNode d) of
|
adamc@1246
|
805 Dt0 _ => true
|
adamc@1246
|
806 | Dt1 (_, d) => loop d
|
adamc@1246
|
807 | Prim _ => true
|
adamc@1246
|
808 | Recrd (xes, _) => List.all loop (SM.listItems (!xes))
|
adamc@1246
|
809 | Nothing => false)
|
adamc@1253
|
810 orelse List.exists (fn r => List.exists (fn b => repOf b = repOf r) bs)
|
adamc@1253
|
811 (SM.listItems (!(#Cons (unNode d))))
|
adamc@1218
|
812 end
|
adamc@1238
|
813
|
adamc@1238
|
814 fun decomp e =
|
adamc@1238
|
815 case e of
|
adamc@1238
|
816 Func (Other _, es) => List.all decomp es
|
adamc@1238
|
817 | _ => loop (representative (db, e))
|
adamc@1218
|
818 in
|
adamc@1238
|
819 decomp d
|
adamc@1247
|
820 end handle Undetermined => false
|
adamc@1218
|
821
|
adamc@1208
|
822 end
|
adamc@1208
|
823
|
adamc@1226
|
824 val tabs = ref (SM.empty : (string list * string list list) SM.map)
|
adamc@1226
|
825
|
adamc@1200
|
826 fun patCon pc =
|
adamc@1200
|
827 case pc of
|
adamc@1200
|
828 PConVar n => "C" ^ Int.toString n
|
adamc@1200
|
829 | PConFfi {mod = m, datatyp = d, con = c, ...} => m ^ "." ^ d ^ "." ^ c
|
adamc@1200
|
830
|
adamc@1200
|
831 datatype chunk =
|
adamc@1200
|
832 String of string
|
adamc@1200
|
833 | Exp of Mono.exp
|
adamc@1200
|
834
|
adamc@1200
|
835 fun chunkify e =
|
adamc@1200
|
836 case #1 e of
|
adamc@1200
|
837 EPrim (Prim.String s) => [String s]
|
adamc@1207
|
838 | EStrcat (e1, e2) =>
|
adamc@1207
|
839 let
|
adamc@1207
|
840 val chs1 = chunkify e1
|
adamc@1207
|
841 val chs2 = chunkify e2
|
adamc@1207
|
842 in
|
adamc@1207
|
843 case chs2 of
|
adamc@1207
|
844 String s2 :: chs2' =>
|
adamc@1207
|
845 (case List.last chs1 of
|
adamc@1207
|
846 String s1 => List.take (chs1, length chs1 - 1) @ String (s1 ^ s2) :: chs2'
|
adamc@1207
|
847 | _ => chs1 @ chs2)
|
adamc@1207
|
848 | _ => chs1 @ chs2
|
adamc@1207
|
849 end
|
adamc@1200
|
850 | _ => [Exp e]
|
adamc@1200
|
851
|
adamc@1201
|
852 type 'a parser = chunk list -> ('a * chunk list) option
|
adamc@1201
|
853
|
adamc@1201
|
854 fun always v chs = SOME (v, chs)
|
adamc@1201
|
855
|
adamc@1202
|
856 fun parse p s =
|
adamc@1202
|
857 case p (chunkify s) of
|
adamc@1201
|
858 SOME (v, []) => SOME v
|
adamc@1201
|
859 | _ => NONE
|
adamc@1201
|
860
|
adamc@1201
|
861 fun const s chs =
|
adamc@1201
|
862 case chs of
|
adamc@1201
|
863 String s' :: chs => if String.isPrefix s s' then
|
adamc@1201
|
864 SOME ((), if size s = size s' then
|
adamc@1201
|
865 chs
|
adamc@1201
|
866 else
|
adamc@1201
|
867 String (String.extract (s', size s, NONE)) :: chs)
|
adamc@1201
|
868 else
|
adamc@1201
|
869 NONE
|
adamc@1201
|
870 | _ => NONE
|
adamc@1201
|
871
|
adamc@1201
|
872 fun follow p1 p2 chs =
|
adamc@1201
|
873 case p1 chs of
|
adamc@1201
|
874 NONE => NONE
|
adamc@1201
|
875 | SOME (v1, chs) =>
|
adamc@1201
|
876 case p2 chs of
|
adamc@1201
|
877 NONE => NONE
|
adamc@1201
|
878 | SOME (v2, chs) => SOME ((v1, v2), chs)
|
adamc@1201
|
879
|
adamc@1201
|
880 fun wrap p f chs =
|
adamc@1201
|
881 case p chs of
|
adamc@1201
|
882 NONE => NONE
|
adamc@1201
|
883 | SOME (v, chs) => SOME (f v, chs)
|
adamc@1201
|
884
|
adamc@1209
|
885 fun wrapP p f chs =
|
adamc@1209
|
886 case p chs of
|
adamc@1209
|
887 NONE => NONE
|
adamc@1209
|
888 | SOME (v, chs) =>
|
adamc@1209
|
889 case f v of
|
adamc@1209
|
890 NONE => NONE
|
adamc@1209
|
891 | SOME r => SOME (r, chs)
|
adamc@1209
|
892
|
adamc@1201
|
893 fun alt p1 p2 chs =
|
adamc@1201
|
894 case p1 chs of
|
adamc@1201
|
895 NONE => p2 chs
|
adamc@1201
|
896 | v => v
|
adamc@1201
|
897
|
adamc@1207
|
898 fun altL ps =
|
adamc@1207
|
899 case rev ps of
|
adamc@1207
|
900 [] => (fn _ => NONE)
|
adamc@1207
|
901 | p :: ps =>
|
adamc@1207
|
902 foldl (fn (p1, p2) => alt p1 p2) p ps
|
adamc@1207
|
903
|
adamc@1204
|
904 fun opt p chs =
|
adamc@1204
|
905 case p chs of
|
adamc@1204
|
906 NONE => SOME (NONE, chs)
|
adamc@1204
|
907 | SOME (v, chs) => SOME (SOME v, chs)
|
adamc@1204
|
908
|
adamc@1201
|
909 fun skip cp chs =
|
adamc@1201
|
910 case chs of
|
adamc@1201
|
911 String "" :: chs => skip cp chs
|
adamc@1201
|
912 | String s :: chs' => if cp (String.sub (s, 0)) then
|
adamc@1201
|
913 skip cp (String (String.extract (s, 1, NONE)) :: chs')
|
adamc@1201
|
914 else
|
adamc@1201
|
915 SOME ((), chs)
|
adamc@1201
|
916 | _ => SOME ((), chs)
|
adamc@1201
|
917
|
adamc@1201
|
918 fun keep cp chs =
|
adamc@1201
|
919 case chs of
|
adamc@1201
|
920 String "" :: chs => keep cp chs
|
adamc@1201
|
921 | String s :: chs' =>
|
adamc@1201
|
922 let
|
adamc@1201
|
923 val (befor, after) = Substring.splitl cp (Substring.full s)
|
adamc@1201
|
924 in
|
adamc@1201
|
925 if Substring.isEmpty befor then
|
adamc@1201
|
926 NONE
|
adamc@1201
|
927 else
|
adamc@1201
|
928 SOME (Substring.string befor,
|
adamc@1201
|
929 if Substring.isEmpty after then
|
adamc@1201
|
930 chs'
|
adamc@1201
|
931 else
|
adamc@1201
|
932 String (Substring.string after) :: chs')
|
adamc@1201
|
933 end
|
adamc@1201
|
934 | _ => NONE
|
adamc@1201
|
935
|
adamc@1204
|
936 fun ws p = wrap (follow (skip (fn ch => ch = #" "))
|
adamc@1204
|
937 (follow p (skip (fn ch => ch = #" ")))) (#1 o #2)
|
adamc@1204
|
938
|
adamc@1204
|
939 fun log name p chs =
|
adamc@1206
|
940 (if !debug then
|
adamc@1227
|
941 (print (name ^ ": ");
|
adamc@1227
|
942 app (fn String s => print s
|
adamc@1227
|
943 | _ => print "???") chs;
|
adamc@1227
|
944 print "\n")
|
adamc@1206
|
945 else
|
adamc@1206
|
946 ();
|
adamc@1204
|
947 p chs)
|
adamc@1201
|
948
|
adamc@1201
|
949 fun list p chs =
|
adamc@1207
|
950 altL [wrap (follow p (follow (ws (const ",")) (list p)))
|
adamc@1207
|
951 (fn (v, ((), ls)) => v :: ls),
|
adamc@1207
|
952 wrap (ws p) (fn v => [v]),
|
adamc@1207
|
953 always []] chs
|
adamc@1201
|
954
|
adamc@1201
|
955 val ident = keep (fn ch => Char.isAlphaNum ch orelse ch = #"_")
|
adamc@1201
|
956
|
adamc@1211
|
957 val t_ident = wrapP ident (fn s => if String.isPrefix "T_" s then
|
adamc@1211
|
958 SOME (String.extract (s, 2, NONE))
|
adamc@1201
|
959 else
|
adamc@1211
|
960 NONE)
|
adamc@1211
|
961 val uw_ident = wrapP ident (fn s => if String.isPrefix "uw_" s andalso size s >= 4 then
|
adamc@1211
|
962 SOME (str (Char.toUpper (String.sub (s, 3)))
|
adamc@1211
|
963 ^ String.extract (s, 4, NONE))
|
adamc@1211
|
964 else
|
adamc@1211
|
965 NONE)
|
adamc@1201
|
966
|
adamc@1211
|
967 val field = wrap (follow t_ident
|
adamc@1201
|
968 (follow (const ".")
|
adamc@1201
|
969 uw_ident))
|
adamc@1201
|
970 (fn (t, ((), f)) => (t, f))
|
adamc@1201
|
971
|
adamc@1206
|
972 datatype Rel =
|
adamc@1206
|
973 Exps of exp * exp -> prop
|
adamc@1206
|
974 | Props of prop * prop -> prop
|
adamc@1206
|
975
|
adamc@1204
|
976 datatype sqexp =
|
adamc@1206
|
977 SqConst of Prim.t
|
adamc@1243
|
978 | SqTrue
|
adamc@1243
|
979 | SqFalse
|
adamc@1250
|
980 | SqNot of sqexp
|
adamc@1206
|
981 | Field of string * string
|
adamc@1239
|
982 | Computed of string
|
adamc@1206
|
983 | Binop of Rel * sqexp * sqexp
|
adamc@1207
|
984 | SqKnown of sqexp
|
adamc@1207
|
985 | Inj of Mono.exp
|
adamc@1211
|
986 | SqFunc of string * sqexp
|
adamc@1245
|
987 | Unmodeled
|
adamc@1253
|
988 | Null
|
adamc@1204
|
989
|
adamc@1210
|
990 fun cmp s r = wrap (const s) (fn () => Exps (fn (e1, e2) => Reln (r, [e1, e2])))
|
adamc@1210
|
991
|
adamc@1210
|
992 val sqbrel = altL [cmp "=" Eq,
|
adamc@1210
|
993 cmp "<>" Ne,
|
adamc@1210
|
994 cmp "<=" Le,
|
adamc@1210
|
995 cmp "<" Lt,
|
adamc@1210
|
996 cmp ">=" Ge,
|
adamc@1210
|
997 cmp ">" Gt,
|
adamc@1207
|
998 wrap (const "AND") (fn () => Props And),
|
adamc@1207
|
999 wrap (const "OR") (fn () => Props Or)]
|
adamc@1204
|
1000
|
adamc@1204
|
1001 datatype ('a, 'b) sum = inl of 'a | inr of 'b
|
adamc@1204
|
1002
|
adamc@1209
|
1003 fun string chs =
|
adamc@1206
|
1004 case chs of
|
adamc@1209
|
1005 String s :: chs =>
|
adamc@1209
|
1006 if size s >= 2 andalso String.sub (s, 0) = #"'" then
|
adamc@1209
|
1007 let
|
adamc@1209
|
1008 fun loop (cs, acc) =
|
adamc@1209
|
1009 case cs of
|
adamc@1209
|
1010 [] => NONE
|
adamc@1209
|
1011 | c :: cs =>
|
adamc@1209
|
1012 if c = #"'" then
|
adamc@1209
|
1013 SOME (String.implode (rev acc), cs)
|
adamc@1209
|
1014 else if c = #"\\" then
|
adamc@1209
|
1015 case cs of
|
adamc@1209
|
1016 c :: cs => loop (cs, c :: acc)
|
adamc@1209
|
1017 | _ => raise Fail "Iflow.string: Unmatched backslash escape"
|
adamc@1209
|
1018 else
|
adamc@1209
|
1019 loop (cs, c :: acc)
|
adamc@1209
|
1020 in
|
adamc@1209
|
1021 case loop (String.explode (String.extract (s, 1, NONE)), []) of
|
adamc@1209
|
1022 NONE => NONE
|
adamc@1209
|
1023 | SOME (s, []) => SOME (s, chs)
|
adamc@1209
|
1024 | SOME (s, cs) => SOME (s, String (String.implode cs) :: chs)
|
adamc@1209
|
1025 end
|
adamc@1209
|
1026 else
|
adamc@1209
|
1027 NONE
|
adamc@1209
|
1028 | _ => NONE
|
adamc@1206
|
1029
|
adamc@1209
|
1030 val prim =
|
adamc@1209
|
1031 altL [wrap (follow (wrapP (follow (keep Char.isDigit) (follow (const ".") (keep Char.isDigit)))
|
adamc@1209
|
1032 (fn (x, ((), y)) => Option.map Prim.Float (Real64.fromString (x ^ "." ^ y))))
|
adamc@1209
|
1033 (opt (const "::float8"))) #1,
|
adamc@1209
|
1034 wrap (follow (wrapP (keep Char.isDigit)
|
adamc@1209
|
1035 (Option.map Prim.Int o Int64.fromString))
|
adamc@1209
|
1036 (opt (const "::int8"))) #1,
|
adamc@1209
|
1037 wrap (follow (opt (const "E")) (follow string (opt (const "::text"))))
|
adamc@1209
|
1038 (Prim.String o #1 o #2)]
|
adamc@1206
|
1039
|
adamc@1207
|
1040 fun known' chs =
|
adamc@1207
|
1041 case chs of
|
adamc@1207
|
1042 Exp (EFfi ("Basis", "sql_known"), _) :: chs => SOME ((), chs)
|
adamc@1207
|
1043 | _ => NONE
|
adamc@1207
|
1044
|
adamc@1207
|
1045 fun sqlify chs =
|
adamc@1207
|
1046 case chs of
|
adamc@1207
|
1047 Exp (EFfiApp ("Basis", f, [e]), _) :: chs =>
|
adamc@1207
|
1048 if String.isPrefix "sqlify" f then
|
adamc@1207
|
1049 SOME (e, chs)
|
adamc@1207
|
1050 else
|
adamc@1207
|
1051 NONE
|
adamc@1243
|
1052 | Exp (ECase (e, [((PCon (_, PConFfi {mod = "Basis", con = "True", ...}, NONE), _),
|
adamc@1243
|
1053 (EPrim (Prim.String "TRUE"), _)),
|
adamc@1243
|
1054 ((PCon (_, PConFfi {mod = "Basis", con = "False", ...}, NONE), _),
|
adamc@1243
|
1055 (EPrim (Prim.String "FALSE"), _))], _), _) :: chs =>
|
adamc@1243
|
1056 SOME (e, chs)
|
adamc@1243
|
1057
|
adamc@1207
|
1058 | _ => NONE
|
adamc@1207
|
1059
|
adamc@1211
|
1060 fun constK s = wrap (const s) (fn () => s)
|
adamc@1211
|
1061
|
adamc@1211
|
1062 val funcName = altL [constK "COUNT",
|
adamc@1211
|
1063 constK "MIN",
|
adamc@1211
|
1064 constK "MAX",
|
adamc@1211
|
1065 constK "SUM",
|
adamc@1211
|
1066 constK "AVG"]
|
adamc@1211
|
1067
|
adamc@1245
|
1068 val unmodeled = altL [const "COUNT(*)",
|
adamc@1245
|
1069 const "CURRENT_TIMESTAMP"]
|
adamc@1245
|
1070
|
adamc@1204
|
1071 fun sqexp chs =
|
adamc@1206
|
1072 log "sqexp"
|
adamc@1207
|
1073 (altL [wrap prim SqConst,
|
adamc@1243
|
1074 wrap (const "TRUE") (fn () => SqTrue),
|
adamc@1243
|
1075 wrap (const "FALSE") (fn () => SqFalse),
|
adamc@1253
|
1076 wrap (const "NULL") (fn () => Null),
|
adamc@1211
|
1077 wrap field Field,
|
adamc@1239
|
1078 wrap uw_ident Computed,
|
adamc@1207
|
1079 wrap known SqKnown,
|
adamc@1211
|
1080 wrap func SqFunc,
|
adamc@1245
|
1081 wrap unmodeled (fn () => Unmodeled),
|
adamc@1207
|
1082 wrap sqlify Inj,
|
adamc@1211
|
1083 wrap (follow (const "COALESCE(") (follow sqexp (follow (const ",")
|
adamc@1211
|
1084 (follow (keep (fn ch => ch <> #")")) (const ")")))))
|
adamc@1211
|
1085 (fn ((), (e, _)) => e),
|
adamc@1250
|
1086 wrap (follow (const "(NOT ") (follow sqexp (const ")")))
|
adamc@1250
|
1087 (fn ((), (e, _)) => SqNot e),
|
adamc@1207
|
1088 wrap (follow (ws (const "("))
|
adamc@1207
|
1089 (follow (wrap
|
adamc@1207
|
1090 (follow sqexp
|
adamc@1207
|
1091 (alt
|
adamc@1207
|
1092 (wrap
|
adamc@1207
|
1093 (follow (ws sqbrel)
|
adamc@1207
|
1094 (ws sqexp))
|
adamc@1207
|
1095 inl)
|
adamc@1207
|
1096 (always (inr ()))))
|
adamc@1207
|
1097 (fn (e1, sm) =>
|
adamc@1207
|
1098 case sm of
|
adamc@1207
|
1099 inl (bo, e2) => Binop (bo, e1, e2)
|
adamc@1207
|
1100 | inr () => e1))
|
adamc@1207
|
1101 (const ")")))
|
adamc@1207
|
1102 (fn ((), (e, ())) => e)])
|
adamc@1207
|
1103 chs
|
adamc@1206
|
1104
|
adamc@1207
|
1105 and known chs = wrap (follow known' (follow (const "(") (follow sqexp (const ")"))))
|
adamc@1211
|
1106 (fn ((), ((), (e, ()))) => e) chs
|
adamc@1211
|
1107
|
adamc@1211
|
1108 and func chs = wrap (follow funcName (follow (const "(") (follow sqexp (const ")"))))
|
adamc@1211
|
1109 (fn (f, ((), (e, ()))) => (f, e)) chs
|
adamc@1211
|
1110
|
adamc@1211
|
1111 datatype sitem =
|
adamc@1211
|
1112 SqField of string * string
|
adamc@1211
|
1113 | SqExp of sqexp * string
|
adamc@1211
|
1114
|
adamc@1239
|
1115 val sitem = alt (wrap (follow sqexp (follow (const " AS ") uw_ident))
|
adamc@1239
|
1116 (fn (e, ((), s)) => SqExp (e, s)))
|
adamc@1239
|
1117 (wrap field SqField)
|
adamc@1207
|
1118
|
adamc@1207
|
1119 val select = log "select"
|
adamc@1207
|
1120 (wrap (follow (const "SELECT ") (list sitem))
|
adamc@1207
|
1121 (fn ((), ls) => ls))
|
adamc@1201
|
1122
|
adamc@1201
|
1123 val fitem = wrap (follow uw_ident
|
adamc@1201
|
1124 (follow (const " AS ")
|
adamc@1201
|
1125 t_ident))
|
adamc@1201
|
1126 (fn (t, ((), f)) => (t, f))
|
adamc@1201
|
1127
|
adamc@1207
|
1128 val from = log "from"
|
adamc@1207
|
1129 (wrap (follow (const "FROM ") (list fitem))
|
adamc@1207
|
1130 (fn ((), ls) => ls))
|
adamc@1201
|
1131
|
adamc@1204
|
1132 val wher = wrap (follow (ws (const "WHERE ")) sqexp)
|
adamc@1204
|
1133 (fn ((), ls) => ls)
|
adamc@1204
|
1134
|
adamc@1227
|
1135 type query1 = {Select : sitem list,
|
adamc@1227
|
1136 From : (string * string) list,
|
adamc@1227
|
1137 Where : sqexp option}
|
adamc@1227
|
1138
|
adamc@1227
|
1139 val query1 = log "query1"
|
adamc@1207
|
1140 (wrap (follow (follow select from) (opt wher))
|
adamc@1207
|
1141 (fn ((fs, ts), wher) => {Select = fs, From = ts, Where = wher}))
|
adamc@1201
|
1142
|
adamc@1227
|
1143 datatype query =
|
adamc@1227
|
1144 Query1 of query1
|
adamc@1227
|
1145 | Union of query * query
|
adamc@1227
|
1146
|
adamc@1239
|
1147 val orderby = log "orderby"
|
adamc@1239
|
1148 (wrap (follow (ws (const "ORDER BY "))
|
adamc@1243
|
1149 (follow (list sqexp)
|
adamc@1243
|
1150 (opt (ws (const "DESC")))))
|
adamc@1243
|
1151 ignore)
|
adamc@1239
|
1152
|
adamc@1227
|
1153 fun query chs = log "query"
|
adamc@1239
|
1154 (wrap
|
adamc@1239
|
1155 (follow
|
adamc@1239
|
1156 (alt (wrap (follow (const "((")
|
adamc@1239
|
1157 (follow query
|
adamc@1239
|
1158 (follow (const ") UNION (")
|
adamc@1239
|
1159 (follow query (const "))")))))
|
adamc@1239
|
1160 (fn ((), (q1, ((), (q2, ())))) => Union (q1, q2)))
|
adamc@1239
|
1161 (wrap query1 Query1))
|
adamc@1239
|
1162 (opt orderby))
|
adamc@1239
|
1163 #1)
|
adamc@1227
|
1164 chs
|
adamc@1227
|
1165
|
adamc@1220
|
1166 datatype dml =
|
adamc@1220
|
1167 Insert of string * (string * sqexp) list
|
adamc@1221
|
1168 | Delete of string * sqexp
|
adamc@1223
|
1169 | Update of string * (string * sqexp) list * sqexp
|
adamc@1220
|
1170
|
adamc@1220
|
1171 val insert = log "insert"
|
adamc@1220
|
1172 (wrapP (follow (const "INSERT INTO ")
|
adamc@1220
|
1173 (follow uw_ident
|
adamc@1220
|
1174 (follow (const " (")
|
adamc@1220
|
1175 (follow (list uw_ident)
|
adamc@1220
|
1176 (follow (const ") VALUES (")
|
adamc@1220
|
1177 (follow (list sqexp)
|
adamc@1220
|
1178 (const ")")))))))
|
adamc@1220
|
1179 (fn ((), (tab, ((), (fs, ((), (es, ())))))) =>
|
adamc@1221
|
1180 (SOME (tab, ListPair.zipEq (fs, es)))
|
adamc@1220
|
1181 handle ListPair.UnequalLengths => NONE))
|
adamc@1220
|
1182
|
adamc@1221
|
1183 val delete = log "delete"
|
adamc@1221
|
1184 (wrap (follow (const "DELETE FROM ")
|
adamc@1221
|
1185 (follow uw_ident
|
adamc@1221
|
1186 (follow (const " AS T_T WHERE ")
|
adamc@1221
|
1187 sqexp)))
|
adamc@1221
|
1188 (fn ((), (tab, ((), es))) => (tab, es)))
|
adamc@1221
|
1189
|
adamc@1223
|
1190 val setting = log "setting"
|
adamc@1223
|
1191 (wrap (follow uw_ident (follow (const " = ") sqexp))
|
adamc@1223
|
1192 (fn (f, ((), e)) => (f, e)))
|
adamc@1223
|
1193
|
adamc@1223
|
1194 val update = log "update"
|
adamc@1223
|
1195 (wrap (follow (const "UPDATE ")
|
adamc@1223
|
1196 (follow uw_ident
|
adamc@1223
|
1197 (follow (const " AS T_T SET ")
|
adamc@1223
|
1198 (follow (list setting)
|
adamc@1223
|
1199 (follow (ws (const "WHERE "))
|
adamc@1223
|
1200 sqexp)))))
|
adamc@1223
|
1201 (fn ((), (tab, ((), (fs, ((), e))))) =>
|
adamc@1223
|
1202 (tab, fs, e)))
|
adamc@1223
|
1203
|
adamc@1220
|
1204 val dml = log "dml"
|
adamc@1221
|
1205 (altL [wrap insert Insert,
|
adamc@1223
|
1206 wrap delete Delete,
|
adamc@1223
|
1207 wrap update Update])
|
adamc@1220
|
1208
|
adamc@1236
|
1209 type check = exp * ErrorMsg.span
|
adamc@1236
|
1210
|
adamc@1236
|
1211 structure St :> sig
|
adamc@1236
|
1212 val reset : unit -> unit
|
adamc@1236
|
1213
|
adamc@1236
|
1214 type stashed
|
adamc@1236
|
1215 val stash : unit -> stashed
|
adamc@1236
|
1216 val reinstate : stashed -> unit
|
adamc@1236
|
1217
|
adamc@1249
|
1218 type stashedPath
|
adamc@1249
|
1219 val stashPath : unit -> stashedPath
|
adamc@1249
|
1220 val reinstatePath : stashedPath -> unit
|
adamc@1249
|
1221
|
adamc@1236
|
1222 val nextVar : unit -> int
|
adamc@1236
|
1223
|
adamc@1236
|
1224 val assert : atom list -> unit
|
adamc@1236
|
1225
|
adamc@1236
|
1226 val addPath : check -> unit
|
adamc@1236
|
1227
|
adamc@1236
|
1228 val allowSend : atom list * exp list -> unit
|
adamc@1253
|
1229 val send : check -> unit
|
adamc@1236
|
1230
|
adam@1280
|
1231 val allowEqualKnown : { table : string, field : string } -> unit
|
adam@1280
|
1232 val mayTest : prop -> bool
|
adam@1280
|
1233
|
adamc@1236
|
1234 val allowInsert : atom list -> unit
|
adamc@1236
|
1235 val insert : ErrorMsg.span -> unit
|
adamc@1236
|
1236
|
adamc@1236
|
1237 val allowDelete : atom list -> unit
|
adamc@1236
|
1238 val delete : ErrorMsg.span -> unit
|
adamc@1236
|
1239
|
adamc@1236
|
1240 val allowUpdate : atom list -> unit
|
adamc@1236
|
1241 val update : ErrorMsg.span -> unit
|
adamc@1236
|
1242
|
adamc@1236
|
1243 val havocReln : reln -> unit
|
adamc@1245
|
1244 val havocCookie : string -> unit
|
adamc@1238
|
1245
|
adamc@1251
|
1246 val check : atom -> bool
|
adamc@1251
|
1247
|
adamc@1238
|
1248 val debug : unit -> unit
|
adamc@1236
|
1249 end = struct
|
adamc@1236
|
1250
|
adamc@1236
|
1251 val hnames = ref 1
|
adamc@1236
|
1252
|
adamc@1244
|
1253 type hyps = int * atom list * bool ref
|
adamc@1236
|
1254
|
adamc@1236
|
1255 val db = Cc.database ()
|
adamc@1244
|
1256 val path = ref ([] : ((int * atom list) * check) option ref list)
|
adamc@1244
|
1257 val hyps = ref (0, [] : atom list, ref false)
|
adamc@1236
|
1258 val nvar = ref 0
|
adamc@1236
|
1259
|
adamc@1244
|
1260 fun setHyps (n', hs) =
|
adamc@1236
|
1261 let
|
adamc@1244
|
1262 val (n, _, _) = !hyps
|
adamc@1236
|
1263 in
|
adamc@1236
|
1264 if n' = n then
|
adamc@1236
|
1265 ()
|
adamc@1236
|
1266 else
|
adamc@1244
|
1267 (hyps := (n', hs, ref false);
|
adamc@1236
|
1268 Cc.clear db;
|
adamc@1236
|
1269 app (fn a => Cc.assert (db, a)) hs)
|
adamc@1236
|
1270 end
|
adamc@1236
|
1271
|
adamc@1244
|
1272 fun useKeys () =
|
adamc@1244
|
1273 let
|
adamc@1244
|
1274 val changed = ref false
|
adamc@1244
|
1275
|
adamc@1244
|
1276 fun findKeys (hyps, acc) =
|
adamc@1244
|
1277 case hyps of
|
adamc@1247
|
1278 [] => rev acc
|
adamc@1244
|
1279 | (a as AReln (Sql tab, [r1])) :: hyps =>
|
adamc@1244
|
1280 (case SM.find (!tabs, tab) of
|
adamc@1244
|
1281 NONE => findKeys (hyps, a :: acc)
|
adamc@1244
|
1282 | SOME (_, []) => findKeys (hyps, a :: acc)
|
adamc@1244
|
1283 | SOME (_, ks) =>
|
adamc@1244
|
1284 let
|
adamc@1244
|
1285 fun finder (hyps, acc) =
|
adamc@1244
|
1286 case hyps of
|
adamc@1247
|
1287 [] => rev acc
|
adamc@1244
|
1288 | (a as AReln (Sql tab', [r2])) :: hyps =>
|
adamc@1244
|
1289 if tab' = tab andalso
|
adamc@1244
|
1290 List.exists (List.all (fn f =>
|
adamc@1244
|
1291 let
|
adamc@1244
|
1292 val r =
|
adamc@1244
|
1293 Cc.check (db,
|
adamc@1244
|
1294 AReln (Eq, [Proj (r1, f),
|
adamc@1244
|
1295 Proj (r2, f)]))
|
adamc@1244
|
1296 in
|
adamc@1244
|
1297 (*Print.prefaces "Fs"
|
adamc@1244
|
1298 [("tab",
|
adamc@1244
|
1299 Print.PD.string tab),
|
adamc@1244
|
1300 ("r1",
|
adamc@1244
|
1301 p_exp (Proj (r1, f))),
|
adamc@1244
|
1302 ("r2",
|
adamc@1244
|
1303 p_exp (Proj (r2, f))),
|
adamc@1244
|
1304 ("r",
|
adamc@1244
|
1305 Print.PD.string
|
adamc@1244
|
1306 (Bool.toString r))];*)
|
adamc@1244
|
1307 r
|
adamc@1244
|
1308 end)) ks then
|
adamc@1244
|
1309 (changed := true;
|
adamc@1244
|
1310 Cc.assert (db, AReln (Eq, [r1, r2]));
|
adamc@1244
|
1311 finder (hyps, acc))
|
adamc@1244
|
1312 else
|
adamc@1244
|
1313 finder (hyps, a :: acc)
|
adamc@1244
|
1314 | a :: hyps => finder (hyps, a :: acc)
|
adamc@1244
|
1315
|
adamc@1244
|
1316 val hyps = finder (hyps, [])
|
adamc@1244
|
1317 in
|
adamc@1246
|
1318 findKeys (hyps, a :: acc)
|
adamc@1244
|
1319 end)
|
adamc@1244
|
1320 | a :: hyps => findKeys (hyps, a :: acc)
|
adamc@1244
|
1321
|
adamc@1244
|
1322 fun loop hs =
|
adamc@1244
|
1323 let
|
adamc@1244
|
1324 val hs = findKeys (hs, [])
|
adamc@1244
|
1325 in
|
adamc@1244
|
1326 if !changed then
|
adamc@1244
|
1327 (changed := false;
|
adamc@1244
|
1328 loop hs)
|
adamc@1244
|
1329 else
|
adamc@1244
|
1330 ()
|
adamc@1244
|
1331 end
|
adamc@1244
|
1332
|
adamc@1244
|
1333 val (_, hs, _) = !hyps
|
adamc@1244
|
1334 in
|
adamc@1246
|
1335 (*print "useKeys\n";*)
|
adamc@1244
|
1336 loop hs
|
adamc@1244
|
1337 end
|
adamc@1244
|
1338
|
adamc@1244
|
1339 fun complete () =
|
adamc@1244
|
1340 let
|
adamc@1244
|
1341 val (_, _, bf) = !hyps
|
adamc@1244
|
1342 in
|
adamc@1244
|
1343 if !bf then
|
adamc@1244
|
1344 ()
|
adamc@1244
|
1345 else
|
adamc@1244
|
1346 (bf := true;
|
adamc@1244
|
1347 useKeys ())
|
adamc@1244
|
1348 end
|
adamc@1244
|
1349
|
adamc@1244
|
1350 type stashed = int * ((int * atom list) * check) option ref list * (int * atom list)
|
adamc@1244
|
1351 fun stash () = (!nvar, !path, (#1 (!hyps), #2 (!hyps)))
|
adamc@1236
|
1352 fun reinstate (nv, p, h) =
|
adamc@1236
|
1353 (nvar := nv;
|
adamc@1236
|
1354 path := p;
|
adamc@1236
|
1355 setHyps h)
|
adamc@1236
|
1356
|
adamc@1249
|
1357 type stashedPath = ((int * atom list) * check) option ref list
|
adamc@1249
|
1358 fun stashPath () = !path
|
adamc@1249
|
1359 fun reinstatePath p = path := p
|
adamc@1249
|
1360
|
adamc@1236
|
1361 fun nextVar () =
|
adamc@1236
|
1362 let
|
adamc@1236
|
1363 val n = !nvar
|
adamc@1236
|
1364 in
|
adamc@1236
|
1365 nvar := n + 1;
|
adamc@1236
|
1366 n
|
adamc@1236
|
1367 end
|
adamc@1236
|
1368
|
adamc@1236
|
1369 fun assert ats =
|
adamc@1236
|
1370 let
|
adamc@1236
|
1371 val n = !hnames
|
adamc@1244
|
1372 val (_, hs, _) = !hyps
|
adamc@1236
|
1373 in
|
adamc@1236
|
1374 hnames := n + 1;
|
adamc@1244
|
1375 hyps := (n, ats @ hs, ref false);
|
adamc@1236
|
1376 app (fn a => Cc.assert (db, a)) ats
|
adamc@1236
|
1377 end
|
adamc@1236
|
1378
|
adamc@1244
|
1379 fun addPath c = path := ref (SOME ((#1 (!hyps), #2 (!hyps)), c)) :: !path
|
adamc@1236
|
1380
|
adamc@1236
|
1381 val sendable = ref ([] : (atom list * exp list) list)
|
adamc@1236
|
1382
|
adamc@1238
|
1383 fun checkGoals goals k =
|
adamc@1238
|
1384 let
|
adamc@1238
|
1385 fun checkGoals goals unifs =
|
adamc@1238
|
1386 case goals of
|
adamc@1238
|
1387 [] => k unifs
|
adamc@1238
|
1388 | AReln (Sql tab, [Lvar lv]) :: goals =>
|
adamc@1238
|
1389 let
|
adamc@1238
|
1390 val saved = stash ()
|
adamc@1244
|
1391 val (_, hyps, _) = !hyps
|
adamc@1236
|
1392
|
adamc@1238
|
1393 fun tryAll unifs hyps =
|
adamc@1238
|
1394 case hyps of
|
adamc@1238
|
1395 [] => false
|
adamc@1238
|
1396 | AReln (Sql tab', [e]) :: hyps =>
|
adamc@1238
|
1397 (tab' = tab andalso
|
adamc@1238
|
1398 checkGoals goals (IM.insert (unifs, lv, e)))
|
adamc@1238
|
1399 orelse tryAll unifs hyps
|
adamc@1238
|
1400 | _ :: hyps => tryAll unifs hyps
|
adamc@1238
|
1401 in
|
adamc@1238
|
1402 tryAll unifs hyps
|
adamc@1238
|
1403 end
|
adamc@1243
|
1404 | (g as AReln (r, es)) :: goals =>
|
adamc@1244
|
1405 (complete ();
|
adamc@1245
|
1406 (if Cc.check (db, AReln (r, map (simplify unifs) es)) then
|
adamc@1245
|
1407 true
|
adamc@1245
|
1408 else
|
adamc@1245
|
1409 ((*Print.preface ("Fail", p_atom (AReln (r, map (simplify unifs) es)));*)
|
adamc@1245
|
1410 false))
|
adamc@1244
|
1411 andalso checkGoals goals unifs)
|
adamc@1238
|
1412 | ACond _ :: _ => false
|
adamc@1238
|
1413 in
|
adamc@1238
|
1414 checkGoals goals IM.empty
|
adamc@1238
|
1415 end
|
adamc@1236
|
1416
|
adamc@1253
|
1417 fun buildable (e, loc) =
|
adamc@1238
|
1418 let
|
adamc@1238
|
1419 fun doPols pols acc =
|
adamc@1236
|
1420 case pols of
|
adamc@1253
|
1421 [] =>
|
adamc@1253
|
1422 let
|
adamc@1253
|
1423 val b = Cc.builtFrom (db, {Base = acc, Derived = e})
|
adamc@1253
|
1424 in
|
adamc@1253
|
1425 (*Print.prefaces "buildable" [("Base", Print.p_list p_exp acc),
|
adamc@1253
|
1426 ("Derived", p_exp e),
|
adamc@1253
|
1427 ("Hyps", Print.p_list p_atom (#2 (!hyps))),
|
adamc@1253
|
1428 ("Good", Print.PD.string (Bool.toString b))];*)
|
adamc@1253
|
1429 b
|
adamc@1253
|
1430 end
|
adamc@1236
|
1431 | (goals, es) :: pols =>
|
adamc@1238
|
1432 checkGoals goals (fn unifs => doPols pols (map (simplify unifs) es @ acc))
|
adamc@1238
|
1433 orelse doPols pols acc
|
adamc@1236
|
1434 in
|
adamc@1238
|
1435 if doPols (!sendable) [] then
|
adamc@1238
|
1436 ()
|
adamc@1238
|
1437 else
|
adamc@1238
|
1438 let
|
adamc@1244
|
1439 val (_, hs, _) = !hyps
|
adamc@1238
|
1440 in
|
adamc@1238
|
1441 ErrorMsg.errorAt loc "The information flow policy may be violated here.";
|
adamc@1245
|
1442 Print.prefaces "Situation" [("User learns", p_exp e),
|
adamc@1253
|
1443 ("Hypotheses", Print.p_list p_atom hs),
|
adamc@1253
|
1444 ("E-graph", Cc.p_database db)]
|
adamc@1238
|
1445 end
|
adamc@1246
|
1446 end
|
adamc@1236
|
1447
|
adamc@1236
|
1448 fun checkPaths () =
|
adamc@1236
|
1449 let
|
adamc@1244
|
1450 val (n, hs, _) = !hyps
|
adamc@1244
|
1451 val hs = (n, hs)
|
adamc@1236
|
1452 in
|
adamc@1236
|
1453 app (fn r =>
|
adamc@1236
|
1454 case !r of
|
adamc@1236
|
1455 NONE => ()
|
adamc@1236
|
1456 | SOME (hs, e) =>
|
adamc@1236
|
1457 (r := NONE;
|
adamc@1236
|
1458 setHyps hs;
|
adamc@1253
|
1459 buildable e)) (!path);
|
adamc@1236
|
1460 setHyps hs
|
adamc@1236
|
1461 end
|
adamc@1236
|
1462
|
adamc@1238
|
1463 fun allowSend v = ((*Print.prefaces "Allow" [("goals", Print.p_list p_atom (#1 v)),
|
adamc@1243
|
1464 ("exps", Print.p_list p_exp (#2 v))];*)
|
adamc@1238
|
1465 sendable := v :: !sendable)
|
adamc@1236
|
1466
|
adamc@1253
|
1467 fun send (e, loc) = ((*Print.preface ("Send[" ^ Bool.toString uk ^ "]", p_exp e);*)
|
adamc@1253
|
1468 complete ();
|
adamc@1253
|
1469 checkPaths ();
|
adamc@1253
|
1470 if isKnown e then
|
adamc@1253
|
1471 ()
|
adamc@1253
|
1472 else
|
adamc@1253
|
1473 buildable (e, loc))
|
adamc@1236
|
1474
|
adamc@1236
|
1475 fun doable pols (loc : ErrorMsg.span) =
|
adamc@1236
|
1476 let
|
adamc@1236
|
1477 val pols = !pols
|
adamc@1236
|
1478 in
|
adamc@1244
|
1479 complete ();
|
adamc@1236
|
1480 if List.exists (fn goals =>
|
adamc@1238
|
1481 if checkGoals goals (fn _ => true) then
|
adamc@1238
|
1482 ((*Print.prefaces "Match" [("goals", Print.p_list p_atom goals),
|
adamc@1238
|
1483 ("hyps", Print.p_list p_atom (#2 (!hyps)))];*)
|
adamc@1238
|
1484 true)
|
adamc@1238
|
1485 else
|
adamc@1246
|
1486 ((*Print.prefaces "No match" [("goals", Print.p_list p_atom goals)(*,
|
adamc@1246
|
1487 ("hyps", Print.p_list p_atom (#2 (!hyps)))*)];*)
|
adamc@1238
|
1488 false)) pols then
|
adamc@1236
|
1489 ()
|
adamc@1236
|
1490 else
|
adamc@1236
|
1491 let
|
adamc@1244
|
1492 val (_, hs, _) = !hyps
|
adamc@1236
|
1493 in
|
adamc@1236
|
1494 ErrorMsg.errorAt loc "The database update policy may be violated here.";
|
adamc@1250
|
1495 Print.prefaces "Situation" [("Hypotheses", Print.p_list p_atom hs)(*,
|
adamc@1250
|
1496 ("E-graph", Cc.p_database db)*)]
|
adamc@1236
|
1497 end
|
adamc@1236
|
1498 end
|
adamc@1236
|
1499
|
adamc@1236
|
1500 val insertable = ref ([] : atom list list)
|
adamc@1236
|
1501 fun allowInsert v = insertable := v :: !insertable
|
adamc@1236
|
1502 val insert = doable insertable
|
adamc@1236
|
1503
|
adamc@1236
|
1504 val updatable = ref ([] : atom list list)
|
adamc@1236
|
1505 fun allowUpdate v = updatable := v :: !updatable
|
adamc@1236
|
1506 val update = doable updatable
|
adamc@1236
|
1507
|
adamc@1236
|
1508 val deletable = ref ([] : atom list list)
|
adamc@1236
|
1509 fun allowDelete v = deletable := v :: !deletable
|
adamc@1236
|
1510 val delete = doable deletable
|
adamc@1236
|
1511
|
adam@1280
|
1512 val testable = ref ([] : { table : string, field : string } list)
|
adam@1280
|
1513 fun allowEqualKnown v = testable := v :: !testable
|
adam@1280
|
1514 fun mayTest p =
|
adam@1280
|
1515 case p of
|
adam@1280
|
1516 Reln (Eq, [e1, e2]) =>
|
adam@1280
|
1517 let
|
adam@1280
|
1518 val (_, hs, _) = !hyps
|
adam@1280
|
1519
|
adam@1280
|
1520 fun tableInHyps (tab, x) = List.exists (fn AReln (Sql tab', [Var x']) => tab' = tab andalso x' = x
|
adam@1280
|
1521 | _ => false) hs
|
adam@1280
|
1522
|
adam@1280
|
1523 fun allowed (tab, v) =
|
adam@1280
|
1524 case tab of
|
adam@1280
|
1525 Proj (Var tab, fd) =>
|
adam@1280
|
1526 List.exists (fn {table = tab', field = fd'} =>
|
adam@1280
|
1527 fd' = fd
|
adam@1280
|
1528 andalso tableInHyps (tab', tab)) (!testable)
|
adam@1280
|
1529 andalso Cc.check (db, AReln (Known, [v]))
|
adam@1280
|
1530 | _ => false
|
adam@1280
|
1531 in
|
adam@1280
|
1532 if allowed (e1, e2) orelse allowed (e2, e1) then
|
adam@1280
|
1533 (Cc.assert (db, AReln (Eq, [e1, e2]));
|
adam@1280
|
1534 true)
|
adam@1280
|
1535 else
|
adam@1280
|
1536 false
|
adam@1280
|
1537 end
|
adam@1280
|
1538 | _ => false
|
adam@1280
|
1539
|
adamc@1238
|
1540 fun reset () = (Cc.clear db;
|
adamc@1238
|
1541 path := [];
|
adamc@1244
|
1542 hyps := (0, [], ref false);
|
adamc@1238
|
1543 nvar := 0;
|
adamc@1238
|
1544 sendable := [];
|
adam@1280
|
1545 testable := [];
|
adamc@1238
|
1546 insertable := [];
|
adamc@1238
|
1547 updatable := [];
|
adamc@1238
|
1548 deletable := [])
|
adamc@1238
|
1549
|
adamc@1236
|
1550 fun havocReln r =
|
adamc@1236
|
1551 let
|
adamc@1236
|
1552 val n = !hnames
|
adamc@1244
|
1553 val (_, hs, _) = !hyps
|
adamc@1236
|
1554 in
|
adamc@1236
|
1555 hnames := n + 1;
|
adamc@1244
|
1556 hyps := (n, List.filter (fn AReln (r', _) => r' <> r | _ => true) hs, ref false)
|
adamc@1236
|
1557 end
|
adamc@1236
|
1558
|
adamc@1245
|
1559 fun havocCookie cname =
|
adamc@1245
|
1560 let
|
adamc@1245
|
1561 val cname = "cookie/" ^ cname
|
adamc@1245
|
1562 val n = !hnames
|
adamc@1245
|
1563 val (_, hs, _) = !hyps
|
adamc@1245
|
1564 in
|
adamc@1245
|
1565 hnames := n + 1;
|
adamc@1245
|
1566 hyps := (n, List.filter (fn AReln (Eq, [_, Func (Other f, [])]) => f <> cname | _ => true) hs, ref false)
|
adamc@1245
|
1567 end
|
adamc@1245
|
1568
|
adamc@1251
|
1569 fun check a = Cc.check (db, a)
|
adamc@1251
|
1570
|
adamc@1238
|
1571 fun debug () =
|
adamc@1238
|
1572 let
|
adamc@1244
|
1573 val (_, hs, _) = !hyps
|
adamc@1238
|
1574 in
|
adamc@1238
|
1575 Print.preface ("Hyps", Print.p_list p_atom hs)
|
adamc@1238
|
1576 end
|
adamc@1238
|
1577
|
adamc@1236
|
1578 end
|
adamc@1236
|
1579
|
adamc@1236
|
1580
|
adamc@1215
|
1581 fun removeDups (ls : (string * string) list) =
|
adamc@1211
|
1582 case ls of
|
adamc@1211
|
1583 [] => []
|
adamc@1211
|
1584 | x :: ls =>
|
adamc@1211
|
1585 let
|
adamc@1211
|
1586 val ls = removeDups ls
|
adamc@1211
|
1587 in
|
adamc@1211
|
1588 if List.exists (fn x' => x' = x) ls then
|
adamc@1211
|
1589 ls
|
adamc@1211
|
1590 else
|
adamc@1211
|
1591 x :: ls
|
adamc@1211
|
1592 end
|
adamc@1211
|
1593
|
adamc@1241
|
1594 fun deinj env e =
|
adamc@1241
|
1595 case #1 e of
|
adamc@1241
|
1596 ERel n => SOME (List.nth (env, n))
|
adamc@1241
|
1597 | EField (e, f) =>
|
adamc@1241
|
1598 (case deinj env e of
|
adamc@1241
|
1599 NONE => NONE
|
adamc@1241
|
1600 | SOME e => SOME (Proj (e, f)))
|
adamc@1251
|
1601 | EApp ((EFfi mf, _), e) =>
|
adamc@1251
|
1602 if Settings.isEffectful mf orelse Settings.isBenignEffectful mf then
|
adamc@1251
|
1603 NONE
|
adamc@1251
|
1604 else (case deinj env e of
|
adamc@1251
|
1605 NONE => NONE
|
adamc@1251
|
1606 | SOME e => SOME (Func (Other (#1 mf ^ "." ^ #2 mf), [e])))
|
adamc@1241
|
1607 | _ => NONE
|
adamc@1241
|
1608
|
adamc@1220
|
1609 fun expIn rv env rvOf =
|
adamc@1220
|
1610 let
|
adamc@1236
|
1611 fun expIn e =
|
adamc@1220
|
1612 let
|
adamc@1236
|
1613 fun default () = inl (rv ())
|
adamc@1220
|
1614 in
|
adamc@1220
|
1615 case e of
|
adamc@1236
|
1616 SqConst p => inl (Const p)
|
adamc@1243
|
1617 | SqTrue => inl (Func (DtCon0 "Basis.bool.True", []))
|
adamc@1243
|
1618 | SqFalse => inl (Func (DtCon0 "Basis.bool.False", []))
|
adamc@1253
|
1619 | Null => inl (Func (DtCon0 "None", []))
|
adamc@1250
|
1620 | SqNot e =>
|
adamc@1250
|
1621 inr (case expIn e of
|
adamc@1250
|
1622 inl e => Reln (Eq, [e, Func (DtCon0 "Basis.bool.False", [])])
|
adamc@1250
|
1623 | inr _ => Unknown)
|
adamc@1236
|
1624 | Field (v, f) => inl (Proj (rvOf v, f))
|
adamc@1239
|
1625 | Computed _ => default ()
|
adamc@1220
|
1626 | Binop (bo, e1, e2) =>
|
adamc@1220
|
1627 let
|
adamc@1236
|
1628 val e1 = expIn e1
|
adamc@1236
|
1629 val e2 = expIn e2
|
adamc@1220
|
1630 in
|
adamc@1236
|
1631 inr (case (bo, e1, e2) of
|
adamc@1236
|
1632 (Exps f, inl e1, inl e2) => f (e1, e2)
|
adamc@1243
|
1633 | (Props f, v1, v2) =>
|
adamc@1243
|
1634 let
|
adamc@1243
|
1635 fun pin v =
|
adamc@1243
|
1636 case v of
|
adamc@1243
|
1637 inl e => Reln (Eq, [e, Func (DtCon0 "Basis.bool.True", [])])
|
adamc@1243
|
1638 | inr p => p
|
adamc@1243
|
1639 in
|
adamc@1243
|
1640 f (pin v1, pin v2)
|
adamc@1243
|
1641 end
|
adamc@1236
|
1642 | _ => Unknown)
|
adamc@1220
|
1643 end
|
adamc@1220
|
1644 | SqKnown e =>
|
adamc@1236
|
1645 (case expIn e of
|
adamc@1236
|
1646 inl e => inr (Reln (Known, [e]))
|
adamc@1236
|
1647 | _ => inr Unknown)
|
adamc@1220
|
1648 | Inj e =>
|
adamc@1241
|
1649 inl (case deinj env e of
|
adamc@1241
|
1650 NONE => rv ()
|
adamc@1241
|
1651 | SOME e => e)
|
adamc@1220
|
1652 | SqFunc (f, e) =>
|
adamc@1236
|
1653 (case expIn e of
|
adamc@1236
|
1654 inl e => inl (Func (Other f, [e]))
|
adamc@1220
|
1655 | _ => default ())
|
adamc@1220
|
1656
|
adamc@1252
|
1657 | Unmodeled => inl (Func (Other "allow", [rv ()]))
|
adamc@1220
|
1658 end
|
adamc@1220
|
1659 in
|
adamc@1220
|
1660 expIn
|
adamc@1220
|
1661 end
|
adamc@1216
|
1662
|
adamc@1236
|
1663 fun decomp {Save = save, Restore = restore, Add = add} =
|
adamc@1216
|
1664 let
|
adamc@1236
|
1665 fun go p k =
|
adamc@1236
|
1666 case p of
|
adamc@1238
|
1667 True => (k () handle Cc.Contradiction => ())
|
adamc@1236
|
1668 | False => ()
|
adamc@1236
|
1669 | Unknown => ()
|
adamc@1236
|
1670 | And (p1, p2) => go p1 (fn () => go p2 k)
|
adamc@1236
|
1671 | Or (p1, p2) =>
|
adamc@1236
|
1672 let
|
adamc@1236
|
1673 val saved = save ()
|
adamc@1236
|
1674 in
|
adamc@1236
|
1675 go p1 k;
|
adamc@1236
|
1676 restore saved;
|
adamc@1236
|
1677 go p2 k
|
adamc@1236
|
1678 end
|
adamc@1236
|
1679 | Reln x => (add (AReln x); k ())
|
adamc@1236
|
1680 | Cond x => (add (ACond x); k ())
|
adamc@1236
|
1681 in
|
adamc@1236
|
1682 go
|
adamc@1236
|
1683 end
|
adamc@1236
|
1684
|
adamc@1236
|
1685 datatype queryMode =
|
adamc@1238
|
1686 SomeCol of {New : (string * exp) option, Old : (string * exp) option, Outs : exp list} -> unit
|
adamc@1236
|
1687 | AllCols of exp -> unit
|
adamc@1236
|
1688
|
adamc@1236
|
1689 type 'a doQuery = {
|
adamc@1236
|
1690 Env : exp list,
|
adamc@1236
|
1691 NextVar : unit -> exp,
|
adamc@1236
|
1692 Add : atom -> unit,
|
adamc@1236
|
1693 Save : unit -> 'a,
|
adamc@1236
|
1694 Restore : 'a -> unit,
|
adam@1280
|
1695 Cont : queryMode,
|
adam@1280
|
1696 Send : exp -> unit
|
adamc@1236
|
1697 }
|
adamc@1236
|
1698
|
adamc@1241
|
1699 fun doQuery (arg : 'a doQuery) (e as (_, loc)) =
|
adamc@1236
|
1700 let
|
adamc@1241
|
1701 fun default () = ErrorMsg.errorAt loc "Information flow checker can't parse SQL query"
|
adamc@1216
|
1702 in
|
adamc@1216
|
1703 case parse query e of
|
adamc@1216
|
1704 NONE => default ()
|
adamc@1227
|
1705 | SOME q =>
|
adamc@1216
|
1706 let
|
adamc@1236
|
1707 fun doQuery q =
|
adamc@1227
|
1708 case q of
|
adamc@1227
|
1709 Query1 r =>
|
adamc@1227
|
1710 let
|
adamc@1238
|
1711 val new = ref NONE
|
adamc@1238
|
1712 val old = ref NONE
|
adamc@1238
|
1713
|
adamc@1238
|
1714 val rvs = map (fn (tab, v) =>
|
adamc@1238
|
1715 let
|
adamc@1238
|
1716 val nv = #NextVar arg ()
|
adamc@1238
|
1717 in
|
adamc@1238
|
1718 case v of
|
adamc@1238
|
1719 "New" => new := SOME (tab, nv)
|
adamc@1238
|
1720 | "Old" => old := SOME (tab, nv)
|
adamc@1238
|
1721 | _ => ();
|
adamc@1238
|
1722 (v, nv)
|
adamc@1238
|
1723 end) (#From r)
|
adamc@1214
|
1724
|
adamc@1227
|
1725 fun rvOf v =
|
adamc@1227
|
1726 case List.find (fn (v', _) => v' = v) rvs of
|
adamc@1227
|
1727 NONE => raise Fail "Iflow.queryProp: Bad table variable"
|
adamc@1227
|
1728 | SOME (_, e) => e
|
adamc@1214
|
1729
|
adamc@1236
|
1730 val expIn = expIn (#NextVar arg) (#Env arg) rvOf
|
adamc@1236
|
1731
|
adamc@1236
|
1732 val saved = #Save arg ()
|
adamc@1236
|
1733 fun addFrom () = app (fn (t, v) => #Add arg (AReln (Sql t, [rvOf v]))) (#From r)
|
adamc@1236
|
1734
|
adam@1280
|
1735 fun leavesE e =
|
adamc@1227
|
1736 case e of
|
adam@1280
|
1737 Const _ => []
|
adam@1280
|
1738 | Var _ => []
|
adam@1280
|
1739 | Lvar _ => []
|
adam@1280
|
1740 | Func (_, es) => List.concat (map leavesE es)
|
adam@1280
|
1741 | Recd xes => List.concat (map (leavesE o #2) xes)
|
adam@1280
|
1742 | Proj _ => [e]
|
adam@1280
|
1743
|
adam@1280
|
1744 fun leavesP p =
|
adam@1280
|
1745 case p of
|
adam@1280
|
1746 True => []
|
adam@1280
|
1747 | False => []
|
adam@1280
|
1748 | Unknown => []
|
adam@1280
|
1749 | And (p1, p2) => leavesP p1 @ leavesP p2
|
adam@1280
|
1750 | Or (p1, p2) => leavesP p1 @ leavesP p2
|
adam@1280
|
1751 | Reln (_, es) => List.concat (map leavesE es)
|
adam@1280
|
1752 | Cond (e, p) => e :: leavesP p
|
adamc@1214
|
1753
|
adamc@1236
|
1754 fun normal' () =
|
adamc@1236
|
1755 case #Cont arg of
|
adamc@1236
|
1756 SomeCol k =>
|
adamc@1227
|
1757 let
|
adamc@1236
|
1758 val sis = map (fn si =>
|
adamc@1236
|
1759 case si of
|
adamc@1236
|
1760 SqField (v, f) => Proj (rvOf v, f)
|
adamc@1236
|
1761 | SqExp (e, f) =>
|
adamc@1236
|
1762 case expIn e of
|
adamc@1236
|
1763 inr _ => #NextVar arg ()
|
adamc@1236
|
1764 | inl e => e) (#Select r)
|
adamc@1227
|
1765 in
|
adamc@1238
|
1766 k {New = !new, Old = !old, Outs = sis}
|
adamc@1227
|
1767 end
|
adamc@1236
|
1768 | AllCols k =>
|
adamc@1227
|
1769 let
|
adamc@1236
|
1770 val (ts, es) =
|
adamc@1236
|
1771 foldl (fn (si, (ts, es)) =>
|
adamc@1227
|
1772 case si of
|
adamc@1227
|
1773 SqField (v, f) =>
|
adamc@1227
|
1774 let
|
adamc@1227
|
1775 val fs = getOpt (SM.find (ts, v), SM.empty)
|
adamc@1227
|
1776 in
|
adamc@1236
|
1777 (SM.insert (ts, v, SM.insert (fs, f, Proj (rvOf v, f))), es)
|
adamc@1227
|
1778 end
|
adamc@1227
|
1779 | SqExp (e, f) =>
|
adamc@1227
|
1780 let
|
adamc@1236
|
1781 val e =
|
adamc@1236
|
1782 case expIn e of
|
adamc@1236
|
1783 inr _ => #NextVar arg ()
|
adamc@1236
|
1784 | inl e => e
|
adamc@1227
|
1785 in
|
adamc@1236
|
1786 (ts, SM.insert (es, f, e))
|
adamc@1227
|
1787 end)
|
adamc@1236
|
1788 (SM.empty, SM.empty) (#Select r)
|
adamc@1227
|
1789 in
|
adamc@1236
|
1790 k (Recd (map (fn (t, fs) => (t, Recd (SM.listItemsi fs)))
|
adamc@1236
|
1791 (SM.listItemsi ts)
|
adamc@1236
|
1792 @ SM.listItemsi es))
|
adamc@1227
|
1793 end
|
adamc@1227
|
1794
|
adamc@1236
|
1795 fun doWhere final =
|
adamc@1236
|
1796 (addFrom ();
|
adamc@1236
|
1797 case #Where r of
|
adamc@1253
|
1798 NONE => final ()
|
adamc@1236
|
1799 | SOME e =>
|
adamc@1243
|
1800 let
|
adamc@1243
|
1801 val p = case expIn e of
|
adamc@1243
|
1802 inl e => Reln (Eq, [e, Func (DtCon0 "Basis.bool.True", [])])
|
adamc@1243
|
1803 | inr p => p
|
adamc@1243
|
1804
|
adam@1280
|
1805 fun getConjuncts p =
|
adam@1280
|
1806 case p of
|
adam@1280
|
1807 And (p1, p2) => getConjuncts p1 @ getConjuncts p2
|
adam@1280
|
1808 | _ => [p]
|
adam@1280
|
1809
|
adamc@1243
|
1810 val saved = #Save arg ()
|
adam@1280
|
1811
|
adam@1280
|
1812 val conjs = getConjuncts p
|
adam@1280
|
1813 val conjs = List.filter (not o St.mayTest) conjs
|
adamc@1243
|
1814 in
|
adam@1280
|
1815 app (fn p => app (#Send arg) (leavesP p)) conjs;
|
adamc@1243
|
1816 decomp {Save = #Save arg, Restore = #Restore arg, Add = #Add arg}
|
adamc@1253
|
1817 p (fn () => final () handle Cc.Contradiction => ());
|
adamc@1243
|
1818 #Restore arg saved
|
adamc@1243
|
1819 end)
|
adamc@1236
|
1820 handle Cc.Contradiction => ()
|
adamc@1236
|
1821
|
adamc@1236
|
1822 fun normal () = doWhere normal'
|
adamc@1227
|
1823 in
|
adamc@1236
|
1824 (case #Select r of
|
adamc@1236
|
1825 [SqExp (Binop (Exps bo, Count, SqConst (Prim.Int 0)), f)] =>
|
adamc@1236
|
1826 (case bo (Const (Prim.Int 1), Const (Prim.Int 2)) of
|
adamc@1236
|
1827 Reln (Gt, [Const (Prim.Int 1), Const (Prim.Int 2)]) =>
|
adamc@1236
|
1828 (case #Cont arg of
|
adamc@1236
|
1829 SomeCol _ => ()
|
adamc@1236
|
1830 | AllCols k =>
|
adamc@1236
|
1831 let
|
adamc@1236
|
1832 fun answer e = k (Recd [(f, e)])
|
adamc@1236
|
1833
|
adamc@1236
|
1834 val saved = #Save arg ()
|
adamc@1238
|
1835 val () = (answer (Func (DtCon0 "Basis.bool.False", [])))
|
adamc@1238
|
1836 handle Cc.Contradiction => ()
|
adamc@1236
|
1837 in
|
adamc@1238
|
1838 #Restore arg saved;
|
adamc@1238
|
1839 (*print "True time!\n";*)
|
adamc@1236
|
1840 doWhere (fn () => answer (Func (DtCon0 "Basis.bool.True", [])));
|
adamc@1236
|
1841 #Restore arg saved
|
adamc@1236
|
1842 end)
|
adamc@1236
|
1843 | _ => normal ())
|
adamc@1236
|
1844 | _ => normal ())
|
adamc@1236
|
1845 before #Restore arg saved
|
adamc@1227
|
1846 end
|
adamc@1227
|
1847 | Union (q1, q2) =>
|
adamc@1220
|
1848 let
|
adamc@1236
|
1849 val saved = #Save arg ()
|
adamc@1220
|
1850 in
|
adamc@1236
|
1851 doQuery q1;
|
adamc@1236
|
1852 #Restore arg saved;
|
adamc@1236
|
1853 doQuery q2;
|
adamc@1236
|
1854 #Restore arg saved
|
adamc@1220
|
1855 end
|
adamc@1216
|
1856 in
|
adamc@1236
|
1857 doQuery q
|
adamc@1216
|
1858 end
|
adamc@1220
|
1859 end
|
adamc@1220
|
1860
|
adamc@1211
|
1861 fun evalPat env e (pt, _) =
|
adamc@1211
|
1862 case pt of
|
adamc@1236
|
1863 PWild => env
|
adamc@1236
|
1864 | PVar _ => e :: env
|
adamc@1236
|
1865 | PPrim _ => env
|
adamc@1236
|
1866 | PCon (_, pc, NONE) => (St.assert [AReln (PCon0 (patCon pc), [e])]; env)
|
adamc@1211
|
1867 | PCon (_, pc, SOME pt) =>
|
adamc@1211
|
1868 let
|
adamc@1236
|
1869 val env = evalPat env (Func (UnCon (patCon pc), [e])) pt
|
adamc@1211
|
1870 in
|
adamc@1236
|
1871 St.assert [AReln (PCon1 (patCon pc), [e])];
|
adamc@1236
|
1872 env
|
adamc@1211
|
1873 end
|
adamc@1211
|
1874 | PRecord xpts =>
|
adamc@1236
|
1875 foldl (fn ((x, pt, _), env) => evalPat env (Proj (e, x)) pt) env xpts
|
adamc@1236
|
1876 | PNone _ => (St.assert [AReln (PCon0 "None", [e])]; env)
|
adamc@1211
|
1877 | PSome (_, pt) =>
|
adamc@1211
|
1878 let
|
adamc@1236
|
1879 val env = evalPat env (Func (UnCon "Some", [e])) pt
|
adamc@1211
|
1880 in
|
adamc@1236
|
1881 St.assert [AReln (PCon1 "Some", [e])];
|
adamc@1236
|
1882 env
|
adamc@1211
|
1883 end
|
adamc@1211
|
1884
|
adamc@1251
|
1885 datatype arg_mode = Fixed | Decreasing | Arbitrary
|
adamc@1251
|
1886 type rfun = {args : arg_mode list, tables : SS.set, cookies : SS.set, body : Mono.exp}
|
adamc@1251
|
1887 val rfuns = ref (IM.empty : rfun IM.map)
|
adamc@1251
|
1888
|
adamc@1236
|
1889 fun evalExp env (e as (_, loc)) k =
|
adamc@1236
|
1890 let
|
adamc@1238
|
1891 (*val () = St.debug ()*)
|
adamc@1236
|
1892 (*val () = Print.preface ("evalExp", MonoPrint.p_exp MonoEnv.empty e)*)
|
adamc@1211
|
1893
|
adamc@1236
|
1894 fun default () = k (Var (St.nextVar ()))
|
adamc@1234
|
1895
|
adamc@1234
|
1896 fun doFfi (m, s, es) =
|
adamc@1234
|
1897 if m = "Basis" andalso SS.member (writers, s) then
|
adamc@1234
|
1898 let
|
adamc@1236
|
1899 fun doArgs es =
|
adamc@1236
|
1900 case es of
|
adamc@1245
|
1901 [] =>
|
adamc@1245
|
1902 (if s = "set_cookie" then
|
adamc@1245
|
1903 case es of
|
adamc@1245
|
1904 [_, cname, _, _, _] =>
|
adamc@1245
|
1905 (case #1 cname of
|
adamc@1245
|
1906 EPrim (Prim.String cname) =>
|
adamc@1245
|
1907 St.havocCookie cname
|
adamc@1245
|
1908 | _ => ())
|
adamc@1245
|
1909 | _ => ()
|
adamc@1245
|
1910 else
|
adamc@1245
|
1911 ();
|
adamc@1245
|
1912 k (Recd []))
|
adamc@1236
|
1913 | e :: es =>
|
adamc@1253
|
1914 evalExp env e (fn e => (St.send (e, loc); doArgs es))
|
adamc@1234
|
1915 in
|
adamc@1236
|
1916 doArgs es
|
adamc@1234
|
1917 end
|
adamc@1234
|
1918 else if Settings.isEffectful (m, s) andalso not (Settings.isBenignEffectful (m, s)) then
|
adamc@1234
|
1919 default ()
|
adamc@1234
|
1920 else
|
adamc@1234
|
1921 let
|
adamc@1236
|
1922 fun doArgs (es, acc) =
|
adamc@1236
|
1923 case es of
|
adamc@1236
|
1924 [] => k (Func (Other (m ^ "." ^ s), rev acc))
|
adamc@1236
|
1925 | e :: es =>
|
adamc@1236
|
1926 evalExp env e (fn e => doArgs (es, e :: acc))
|
adamc@1234
|
1927 in
|
adamc@1236
|
1928 doArgs (es, [])
|
adamc@1234
|
1929 end
|
adamc@1200
|
1930 in
|
adamc@1200
|
1931 case #1 e of
|
adamc@1236
|
1932 EPrim p => k (Const p)
|
adamc@1236
|
1933 | ERel n => k (List.nth (env, n))
|
adamc@1200
|
1934 | ENamed _ => default ()
|
adamc@1236
|
1935 | ECon (_, pc, NONE) => k (Func (DtCon0 (patCon pc), []))
|
adamc@1236
|
1936 | ECon (_, pc, SOME e) => evalExp env e (fn e => k (Func (DtCon1 (patCon pc), [e])))
|
adamc@1236
|
1937 | ENone _ => k (Func (DtCon0 "None", []))
|
adamc@1236
|
1938 | ESome (_, e) => evalExp env e (fn e => k (Func (DtCon1 "Some", [e])))
|
adamc@1200
|
1939 | EFfi _ => default ()
|
adamc@1213
|
1940
|
adamc@1250
|
1941 | EFfiApp ("Basis", "rand", []) =>
|
adamc@1250
|
1942 let
|
adamc@1250
|
1943 val e = Var (St.nextVar ())
|
adamc@1250
|
1944 in
|
adamc@1250
|
1945 St.assert [AReln (Known, [e])];
|
adamc@1250
|
1946 k e
|
adamc@1250
|
1947 end
|
adamc@1234
|
1948 | EFfiApp x => doFfi x
|
adamc@1234
|
1949 | EApp ((EFfi (m, s), _), e) => doFfi (m, s, [e])
|
adamc@1213
|
1950
|
adamc@1251
|
1951 | EApp (e1 as (EError _, _), _) => evalExp env e1 k
|
adamc@1251
|
1952
|
adamc@1251
|
1953 | EApp (e1, e2) =>
|
adamc@1251
|
1954 let
|
adamc@1251
|
1955 fun adefault () = (ErrorMsg.errorAt loc "Excessively fancy function call";
|
adamc@1251
|
1956 Print.preface ("Call", MonoPrint.p_exp MonoEnv.empty e);
|
adamc@1251
|
1957 default ())
|
adamc@1251
|
1958
|
adamc@1251
|
1959 fun doArgs (e, args) =
|
adamc@1251
|
1960 case #1 e of
|
adamc@1251
|
1961 EApp (e1, e2) => doArgs (e1, e2 :: args)
|
adamc@1251
|
1962 | ENamed n =>
|
adamc@1251
|
1963 (case IM.find (!rfuns, n) of
|
adamc@1251
|
1964 NONE => adefault ()
|
adamc@1251
|
1965 | SOME rf =>
|
adamc@1251
|
1966 if length (#args rf) <> length args then
|
adamc@1251
|
1967 adefault ()
|
adamc@1251
|
1968 else
|
adamc@1251
|
1969 let
|
adamc@1251
|
1970 val () = (SS.app (St.havocReln o Sql) (#tables rf);
|
adamc@1251
|
1971 SS.app St.havocCookie (#cookies rf))
|
adamc@1251
|
1972 val saved = St.stash ()
|
adamc@1251
|
1973
|
adamc@1251
|
1974 fun doArgs (args, modes, env') =
|
adamc@1251
|
1975 case (args, modes) of
|
adamc@1251
|
1976 ([], []) => (evalExp env' (#body rf) (fn _ => ());
|
adamc@1251
|
1977 St.reinstate saved;
|
adamc@1251
|
1978 default ())
|
adamc@1251
|
1979
|
adamc@1251
|
1980 | (arg :: args, mode :: modes) =>
|
adamc@1251
|
1981 evalExp env arg (fn arg =>
|
adamc@1251
|
1982 let
|
adamc@1251
|
1983 val v = case mode of
|
adamc@1251
|
1984 Arbitrary => Var (St.nextVar ())
|
adamc@1251
|
1985 | Fixed => arg
|
adamc@1251
|
1986 | Decreasing =>
|
adamc@1251
|
1987 let
|
adamc@1251
|
1988 val v = Var (St.nextVar ())
|
adamc@1251
|
1989 in
|
adamc@1251
|
1990 if St.check (AReln (Known, [arg])) then
|
adamc@1251
|
1991 St.assert [(AReln (Known, [v]))]
|
adamc@1251
|
1992 else
|
adamc@1251
|
1993 ();
|
adamc@1251
|
1994 v
|
adamc@1251
|
1995 end
|
adamc@1251
|
1996 in
|
adamc@1251
|
1997 doArgs (args, modes, v :: env')
|
adamc@1251
|
1998 end)
|
adamc@1251
|
1999 | _ => raise Fail "Iflow.doArgs: Impossible"
|
adamc@1251
|
2000 in
|
adamc@1251
|
2001 doArgs (args, #args rf, [])
|
adamc@1251
|
2002 end)
|
adamc@1251
|
2003 | _ => adefault ()
|
adamc@1251
|
2004 in
|
adamc@1251
|
2005 doArgs (e, [])
|
adamc@1251
|
2006 end
|
adamc@1213
|
2007
|
adamc@1200
|
2008 | EAbs _ => default ()
|
adamc@1236
|
2009 | EUnop (s, e1) => evalExp env e1 (fn e1 => k (Func (Other s, [e1])))
|
adamc@1236
|
2010 | EBinop (s, e1, e2) => evalExp env e1 (fn e1 => evalExp env e2 (fn e2 => k (Func (Other s, [e1, e2]))))
|
adamc@1200
|
2011 | ERecord xets =>
|
adamc@1200
|
2012 let
|
adamc@1236
|
2013 fun doFields (xes, acc) =
|
adamc@1236
|
2014 case xes of
|
adamc@1236
|
2015 [] => k (Recd (rev acc))
|
adamc@1236
|
2016 | (x, e, _) :: xes =>
|
adamc@1236
|
2017 evalExp env e (fn e => doFields (xes, (x, e) :: acc))
|
adamc@1200
|
2018 in
|
adamc@1236
|
2019 doFields (xets, [])
|
adamc@1200
|
2020 end
|
adamc@1236
|
2021 | EField (e, s) => evalExp env e (fn e => k (Proj (e, s)))
|
adamc@1218
|
2022 | ECase (e, pes, {result = res, ...}) =>
|
adamc@1236
|
2023 evalExp env e (fn e =>
|
adamc@1248
|
2024 if List.all (fn (_, (EWrite (EPrim _, _), _)) => true
|
adamc@1248
|
2025 | _ => false) pes then
|
adamc@1253
|
2026 (St.send (e, loc);
|
adamc@1248
|
2027 k (Recd []))
|
adamc@1248
|
2028 else
|
adamc@1248
|
2029 (St.addPath (e, loc);
|
adamc@1248
|
2030 app (fn (p, pe) =>
|
adamc@1248
|
2031 let
|
adamc@1248
|
2032 val saved = St.stash ()
|
adamc@1248
|
2033 in
|
adamc@1248
|
2034 let
|
adamc@1248
|
2035 val env = evalPat env e p
|
adamc@1248
|
2036 in
|
adamc@1248
|
2037 evalExp env pe k;
|
adamc@1248
|
2038 St.reinstate saved
|
adamc@1248
|
2039 end
|
adamc@1248
|
2040 handle Cc.Contradiction => St.reinstate saved
|
adamc@1248
|
2041 end) pes))
|
adamc@1200
|
2042 | EStrcat (e1, e2) =>
|
adamc@1236
|
2043 evalExp env e1 (fn e1 =>
|
adamc@1236
|
2044 evalExp env e2 (fn e2 =>
|
adamc@1236
|
2045 k (Func (Other "cat", [e1, e2]))))
|
adamc@1253
|
2046 | EError (e, _) => evalExp env e (fn e => St.send (e, loc))
|
adamc@1200
|
2047 | EReturnBlob {blob = b, mimeType = m, ...} =>
|
adamc@1236
|
2048 evalExp env b (fn b =>
|
adamc@1253
|
2049 (St.send (b, loc);
|
adamc@1236
|
2050 evalExp env m
|
adamc@1253
|
2051 (fn m => St.send (m, loc))))
|
adamc@1200
|
2052 | ERedirect (e, _) =>
|
adamc@1253
|
2053 evalExp env e (fn e => St.send (e, loc))
|
adamc@1200
|
2054 | EWrite e =>
|
adamc@1253
|
2055 evalExp env e (fn e => (St.send (e, loc);
|
adamc@1236
|
2056 k (Recd [])))
|
adamc@1200
|
2057 | ESeq (e1, e2) =>
|
adamc@1249
|
2058 let
|
adamc@1249
|
2059 val path = St.stashPath ()
|
adamc@1249
|
2060 in
|
adamc@1249
|
2061 evalExp env e1 (fn _ => (St.reinstatePath path; evalExp env e2 k))
|
adamc@1249
|
2062 end
|
adamc@1200
|
2063 | ELet (_, _, e1, e2) =>
|
adamc@1236
|
2064 evalExp env e1 (fn e1 => evalExp (e1 :: env) e2 k)
|
adamc@1200
|
2065 | EClosure (n, es) =>
|
adamc@1200
|
2066 let
|
adamc@1236
|
2067 fun doArgs (es, acc) =
|
adamc@1236
|
2068 case es of
|
adamc@1236
|
2069 [] => k (Func (Other ("Cl" ^ Int.toString n), rev acc))
|
adamc@1236
|
2070 | e :: es =>
|
adamc@1236
|
2071 evalExp env e (fn e => doArgs (es, e :: acc))
|
adamc@1200
|
2072 in
|
adamc@1236
|
2073 doArgs (es, [])
|
adamc@1200
|
2074 end
|
adamc@1200
|
2075
|
adamc@1235
|
2076 | EQuery {query = q, body = b, initial = i, state = state, ...} =>
|
adamc@1238
|
2077 evalExp env i (fn i =>
|
adamc@1238
|
2078 let
|
adamc@1238
|
2079 val r = Var (St.nextVar ())
|
adamc@1238
|
2080 val acc = Var (St.nextVar ())
|
adamc@1242
|
2081
|
adamc@1249
|
2082 val (ts, cs) = MonoUtil.Exp.fold {typ = fn (_, st) => st,
|
adamc@1249
|
2083 exp = fn (e, st as (cs, ts)) =>
|
adamc@1242
|
2084 case e of
|
adamc@1242
|
2085 EDml e =>
|
adamc@1242
|
2086 (case parse dml e of
|
adamc@1249
|
2087 NONE => st
|
adamc@1242
|
2088 | SOME c =>
|
adamc@1242
|
2089 case c of
|
adamc@1249
|
2090 Insert _ => st
|
adamc@1242
|
2091 | Delete (tab, _) =>
|
adamc@1249
|
2092 (cs, SS.add (ts, tab))
|
adamc@1242
|
2093 | Update (tab, _, _) =>
|
adamc@1249
|
2094 (cs, SS.add (ts, tab)))
|
adamc@1249
|
2095 | EFfiApp ("Basis", "set_cookie",
|
adamc@1249
|
2096 [_, (EPrim (Prim.String cname), _),
|
adamc@1249
|
2097 _, _, _]) =>
|
adamc@1249
|
2098 (SS.add (cs, cname), ts)
|
adamc@1249
|
2099 | _ => st}
|
adamc@1249
|
2100 (SS.empty, SS.empty) b
|
adamc@1238
|
2101 in
|
adamc@1249
|
2102 case (#1 state, SS.isEmpty ts, SS.isEmpty cs) of
|
adamc@1249
|
2103 (TRecord [], true, true) => ()
|
adamc@1249
|
2104 | _ =>
|
adamc@1249
|
2105 let
|
adamc@1249
|
2106 val saved = St.stash ()
|
adamc@1249
|
2107 in
|
adamc@1249
|
2108 (k i)
|
adamc@1249
|
2109 handle Cc.Contradiction => ();
|
adamc@1249
|
2110 St.reinstate saved
|
adamc@1249
|
2111 end;
|
adamc@1249
|
2112
|
adamc@1249
|
2113 SS.app (St.havocReln o Sql) ts;
|
adamc@1249
|
2114 SS.app St.havocCookie cs;
|
adamc@1242
|
2115
|
adamc@1242
|
2116 doQuery {Env = env,
|
adamc@1242
|
2117 NextVar = Var o St.nextVar,
|
adamc@1242
|
2118 Add = fn a => St.assert [a],
|
adamc@1242
|
2119 Save = St.stash,
|
adamc@1242
|
2120 Restore = St.reinstate,
|
adam@1280
|
2121 Send = fn e => St.send (e, loc),
|
adamc@1242
|
2122 Cont = AllCols (fn x =>
|
adamc@1242
|
2123 (St.assert [AReln (Eq, [r, x])];
|
adamc@1242
|
2124 evalExp (acc :: r :: env) b k))} q
|
adamc@1238
|
2125 end)
|
adamc@1220
|
2126 | EDml e =>
|
adamc@1220
|
2127 (case parse dml e of
|
adamc@1220
|
2128 NONE => (print ("Warning: Information flow checker can't parse DML command at "
|
adamc@1220
|
2129 ^ ErrorMsg.spanToString loc ^ "\n");
|
adamc@1220
|
2130 default ())
|
adamc@1220
|
2131 | SOME d =>
|
adamc@1220
|
2132 case d of
|
adamc@1220
|
2133 Insert (tab, es) =>
|
adamc@1220
|
2134 let
|
adamc@1236
|
2135 val new = St.nextVar ()
|
adamc@1220
|
2136
|
adamc@1236
|
2137 val expIn = expIn (Var o St.nextVar) env
|
adamc@1236
|
2138 (fn _ => raise Fail "Iflow.evalExp: Bad field expression in INSERT [1]")
|
adamc@1220
|
2139
|
adamc@1236
|
2140 val es = map (fn (x, e) =>
|
adamc@1236
|
2141 case expIn e of
|
adamc@1236
|
2142 inl e => (x, e)
|
adamc@1236
|
2143 | inr _ => raise Fail "Iflow.evalExp: Bad field expression in INSERT [2]")
|
adamc@1236
|
2144 es
|
adamc@1220
|
2145
|
adamc@1236
|
2146 val saved = St.stash ()
|
adamc@1220
|
2147 in
|
adamc@1236
|
2148 St.assert [AReln (Sql (tab ^ "$New"), [Recd es])];
|
adamc@1236
|
2149 St.insert loc;
|
adamc@1236
|
2150 St.reinstate saved;
|
adamc@1251
|
2151 St.assert [AReln (Sql tab, [Recd es])];
|
adamc@1236
|
2152 k (Recd [])
|
adamc@1221
|
2153 end
|
adamc@1221
|
2154 | Delete (tab, e) =>
|
adamc@1221
|
2155 let
|
adamc@1236
|
2156 val old = St.nextVar ()
|
adamc@1236
|
2157
|
adamc@1236
|
2158 val expIn = expIn (Var o St.nextVar) env
|
adamc@1236
|
2159 (fn "T" => Var old
|
adamc@1236
|
2160 | _ => raise Fail "Iflow.evalExp: Bad field expression in DELETE")
|
adamc@1221
|
2161
|
adamc@1236
|
2162 val p = case expIn e of
|
adamc@1236
|
2163 inl e => raise Fail "Iflow.evalExp: DELETE with non-boolean"
|
adamc@1236
|
2164 | inr p => p
|
adamc@1236
|
2165
|
adamc@1236
|
2166 val saved = St.stash ()
|
adamc@1221
|
2167 in
|
adamc@1246
|
2168 St.assert [AReln (Sql (tab ^ "$Old"), [Var old]),
|
adamc@1246
|
2169 AReln (Sql (tab), [Var old])];
|
adamc@1236
|
2170 decomp {Save = St.stash,
|
adamc@1236
|
2171 Restore = St.reinstate,
|
adamc@1236
|
2172 Add = fn a => St.assert [a]} p
|
adamc@1236
|
2173 (fn () => (St.delete loc;
|
adamc@1236
|
2174 St.reinstate saved;
|
adamc@1236
|
2175 St.havocReln (Sql tab);
|
adamc@1236
|
2176 k (Recd []))
|
adamc@1236
|
2177 handle Cc.Contradiction => ())
|
adamc@1223
|
2178 end
|
adamc@1223
|
2179 | Update (tab, fs, e) =>
|
adamc@1223
|
2180 let
|
adamc@1236
|
2181 val new = St.nextVar ()
|
adamc@1236
|
2182 val old = St.nextVar ()
|
adamc@1223
|
2183
|
adamc@1236
|
2184 val expIn = expIn (Var o St.nextVar) env
|
adamc@1236
|
2185 (fn "T" => Var old
|
adamc@1236
|
2186 | _ => raise Fail "Iflow.evalExp: Bad field expression in UPDATE")
|
adamc@1223
|
2187
|
adamc@1236
|
2188 val fs = map
|
adamc@1236
|
2189 (fn (x, e) =>
|
adamc@1236
|
2190 (x, case expIn e of
|
adamc@1236
|
2191 inl e => e
|
adamc@1236
|
2192 | inr _ => raise Fail
|
adamc@1236
|
2193 ("Iflow.evalExp: Selecting "
|
adamc@1236
|
2194 ^ "boolean expression")))
|
adamc@1236
|
2195 fs
|
adamc@1223
|
2196
|
adamc@1226
|
2197 val fs' = case SM.find (!tabs, tab) of
|
adamc@1224
|
2198 NONE => raise Fail "Iflow.evalExp: Updating unknown table"
|
adamc@1226
|
2199 | SOME (fs', _) => fs'
|
adamc@1224
|
2200
|
adamc@1224
|
2201 val fs = foldl (fn (f, fs) =>
|
adamc@1224
|
2202 if List.exists (fn (f', _) => f' = f) fs then
|
adamc@1224
|
2203 fs
|
adamc@1224
|
2204 else
|
adamc@1224
|
2205 (f, Proj (Var old, f)) :: fs) fs fs'
|
adamc@1224
|
2206
|
adamc@1236
|
2207 val p = case expIn e of
|
adamc@1236
|
2208 inl e => raise Fail "Iflow.evalExp: UPDATE with non-boolean"
|
adamc@1236
|
2209 | inr p => p
|
adamc@1236
|
2210 val saved = St.stash ()
|
adamc@1223
|
2211 in
|
adamc@1236
|
2212 St.assert [AReln (Sql (tab ^ "$New"), [Recd fs]),
|
adamc@1246
|
2213 AReln (Sql (tab ^ "$Old"), [Var old]),
|
adamc@1246
|
2214 AReln (Sql tab, [Var old])];
|
adamc@1236
|
2215 decomp {Save = St.stash,
|
adamc@1236
|
2216 Restore = St.reinstate,
|
adamc@1236
|
2217 Add = fn a => St.assert [a]} p
|
adamc@1236
|
2218 (fn () => (St.update loc;
|
adamc@1236
|
2219 St.reinstate saved;
|
adamc@1236
|
2220 St.havocReln (Sql tab);
|
adamc@1236
|
2221 k (Recd []))
|
adamc@1236
|
2222 handle Cc.Contradiction => ())
|
adamc@1220
|
2223 end)
|
adamc@1220
|
2224
|
adamc@1229
|
2225 | ENextval (EPrim (Prim.String seq), _) =>
|
adamc@1229
|
2226 let
|
adamc@1236
|
2227 val nv = St.nextVar ()
|
adamc@1229
|
2228 in
|
adamc@1236
|
2229 St.assert [AReln (Sql (String.extract (seq, 3, NONE)), [Var nv])];
|
adamc@1236
|
2230 k (Var nv)
|
adamc@1229
|
2231 end
|
adamc@1200
|
2232 | ENextval _ => default ()
|
adamc@1200
|
2233 | ESetval _ => default ()
|
adamc@1200
|
2234
|
adamc@1238
|
2235 | EUnurlify ((EFfiApp ("Basis", "get_cookie", [(EPrim (Prim.String cname), _)]), _), _, _) =>
|
adamc@1217
|
2236 let
|
adamc@1238
|
2237 val e = Var (St.nextVar ())
|
adamc@1245
|
2238 val e' = Func (Other ("cookie/" ^ cname), [])
|
adamc@1217
|
2239 in
|
adamc@1245
|
2240 St.assert [AReln (Known, [e]), AReln (Eq, [e, e'])];
|
adamc@1238
|
2241 k e
|
adamc@1217
|
2242 end
|
adamc@1213
|
2243
|
adamc@1200
|
2244 | EUnurlify _ => default ()
|
adamc@1200
|
2245 | EJavaScript _ => default ()
|
adamc@1200
|
2246 | ESignalReturn _ => default ()
|
adamc@1200
|
2247 | ESignalBind _ => default ()
|
adamc@1200
|
2248 | ESignalSource _ => default ()
|
adamc@1200
|
2249 | EServerCall _ => default ()
|
adamc@1200
|
2250 | ERecv _ => default ()
|
adamc@1200
|
2251 | ESleep _ => default ()
|
adamc@1200
|
2252 | ESpawn _ => default ()
|
adamc@1200
|
2253 end
|
adamc@1200
|
2254
|
adamc@1251
|
2255 datatype var_source = Input of int | SubInput of int | Unknown
|
adamc@1251
|
2256
|
adamc@1200
|
2257 fun check file =
|
adamc@1200
|
2258 let
|
adamc@1251
|
2259 val () = (St.reset ();
|
adamc@1251
|
2260 rfuns := IM.empty)
|
adamc@1236
|
2261
|
adamc@1213
|
2262 val file = MonoReduce.reduce file
|
adamc@1213
|
2263 val file = MonoOpt.optimize file
|
adamc@1213
|
2264 val file = Fuse.fuse file
|
adamc@1213
|
2265 val file = MonoOpt.optimize file
|
adamc@1216
|
2266 val file = MonoShake.shake file
|
adamc@1213
|
2267 (*val () = Print.preface ("File", MonoPrint.p_file MonoEnv.empty file)*)
|
adamc@1213
|
2268
|
adamc@1207
|
2269 val exptd = foldl (fn ((d, _), exptd) =>
|
adamc@1207
|
2270 case d of
|
adamc@1207
|
2271 DExport (_, _, n, _, _, _) => IS.add (exptd, n)
|
adamc@1207
|
2272 | _ => exptd) IS.empty file
|
adamc@1207
|
2273
|
adamc@1249
|
2274 fun decl (d, loc) =
|
adamc@1200
|
2275 case d of
|
adamc@1226
|
2276 DTable (tab, fs, pk, _) =>
|
adamc@1226
|
2277 let
|
adamc@1226
|
2278 val ks =
|
adamc@1226
|
2279 case #1 pk of
|
adamc@1226
|
2280 EPrim (Prim.String s) =>
|
adamc@1226
|
2281 (case String.tokens (fn ch => ch = #"," orelse ch = #" ") s of
|
adamc@1226
|
2282 [] => []
|
adamc@1226
|
2283 | pk => [pk])
|
adamc@1226
|
2284 | _ => []
|
adamc@1226
|
2285 in
|
adamc@1226
|
2286 if size tab >= 3 then
|
adamc@1236
|
2287 tabs := SM.insert (!tabs, String.extract (tab, 3, NONE),
|
adamc@1236
|
2288 (map #1 fs,
|
adamc@1236
|
2289 map (map (fn s => str (Char.toUpper (String.sub (s, 3)))
|
adamc@1236
|
2290 ^ String.extract (s, 4, NONE))) ks))
|
adamc@1226
|
2291 else
|
adamc@1226
|
2292 raise Fail "Table name does not begin with uw_"
|
adamc@1226
|
2293 end
|
adamc@1238
|
2294 | DVal (x, n, _, e, _) =>
|
adamc@1200
|
2295 let
|
adamc@1238
|
2296 (*val () = print ("\n=== " ^ x ^ " ===\n\n");*)
|
adamc@1238
|
2297
|
adamc@1207
|
2298 val isExptd = IS.member (exptd, n)
|
adamc@1207
|
2299
|
adamc@1236
|
2300 val saved = St.stash ()
|
adamc@1236
|
2301
|
adamc@1236
|
2302 fun deAbs (e, env, ps) =
|
adamc@1200
|
2303 case #1 e of
|
adamc@1236
|
2304 EAbs (_, _, _, e) =>
|
adamc@1236
|
2305 let
|
adamc@1236
|
2306 val nv = Var (St.nextVar ())
|
adamc@1236
|
2307 in
|
adamc@1236
|
2308 deAbs (e, nv :: env,
|
adamc@1236
|
2309 if isExptd then
|
adamc@1236
|
2310 AReln (Known, [nv]) :: ps
|
adamc@1236
|
2311 else
|
adamc@1236
|
2312 ps)
|
adamc@1236
|
2313 end
|
adamc@1236
|
2314 | _ => (e, env, ps)
|
adamc@1200
|
2315
|
adamc@1236
|
2316 val (e, env, ps) = deAbs (e, [], [])
|
adamc@1200
|
2317 in
|
adamc@1236
|
2318 St.assert ps;
|
adamc@1236
|
2319 (evalExp env e (fn _ => ()) handle Cc.Contradiction => ());
|
adamc@1236
|
2320 St.reinstate saved
|
adamc@1200
|
2321 end
|
adamc@1202
|
2322
|
adamc@1251
|
2323 | DValRec [(x, n, _, e, _)] =>
|
adamc@1251
|
2324 let
|
adamc@1251
|
2325 val tables = ref SS.empty
|
adamc@1251
|
2326 val cookies = ref SS.empty
|
adamc@1251
|
2327
|
adamc@1251
|
2328 fun deAbs (e, env, modes) =
|
adamc@1251
|
2329 case #1 e of
|
adamc@1251
|
2330 EAbs (_, _, _, e) => deAbs (e, Input (length env) :: env, ref Fixed :: modes)
|
adamc@1251
|
2331 | _ => (e, env, rev modes)
|
adamc@1251
|
2332
|
adamc@1251
|
2333 val (e, env, modes) = deAbs (e, [], [])
|
adamc@1251
|
2334
|
adamc@1251
|
2335 fun doExp env (e as (_, loc)) =
|
adamc@1251
|
2336 case #1 e of
|
adamc@1251
|
2337 EPrim _ => e
|
adamc@1251
|
2338 | ERel _ => e
|
adamc@1251
|
2339 | ENamed _ => e
|
adamc@1251
|
2340 | ECon (_, _, NONE) => e
|
adamc@1251
|
2341 | ECon (dk, pc, SOME e) => (ECon (dk, pc, SOME (doExp env e)), loc)
|
adamc@1251
|
2342 | ENone _ => e
|
adamc@1251
|
2343 | ESome (t, e) => (ESome (t, doExp env e), loc)
|
adamc@1251
|
2344 | EFfi _ => e
|
adamc@1251
|
2345 | EFfiApp (m, f, es) =>
|
adamc@1251
|
2346 (case (m, f, es) of
|
adamc@1251
|
2347 ("Basis", "set_cookie", [_, (EPrim (Prim.String cname), _), _, _, _]) =>
|
adamc@1251
|
2348 cookies := SS.add (!cookies, cname)
|
adamc@1251
|
2349 | _ => ();
|
adamc@1251
|
2350 (EFfiApp (m, f, map (doExp env) es), loc))
|
adamc@1251
|
2351
|
adamc@1251
|
2352 | EApp (e1, e2) =>
|
adamc@1251
|
2353 let
|
adamc@1251
|
2354 fun default () = (EApp (doExp env e1, doExp env e2), loc)
|
adamc@1251
|
2355
|
adamc@1251
|
2356 fun explore (e, args) =
|
adamc@1251
|
2357 case #1 e of
|
adamc@1251
|
2358 EApp (e1, e2) => explore (e1, e2 :: args)
|
adamc@1251
|
2359 | ENamed n' =>
|
adamc@1251
|
2360 if n' = n then
|
adamc@1251
|
2361 let
|
adamc@1251
|
2362 fun doArgs (pos, args, modes) =
|
adamc@1251
|
2363 case (args, modes) of
|
adamc@1251
|
2364 ((e1, _) :: args, m1 :: modes) =>
|
adamc@1251
|
2365 (case e1 of
|
adamc@1251
|
2366 ERel n =>
|
adamc@1251
|
2367 (case List.nth (env, n) of
|
adamc@1251
|
2368 Input pos' =>
|
adamc@1251
|
2369 if pos' = pos then
|
adamc@1251
|
2370 ()
|
adamc@1251
|
2371 else
|
adamc@1251
|
2372 m1 := Arbitrary
|
adamc@1251
|
2373 | SubInput pos' =>
|
adamc@1251
|
2374 if pos' = pos then
|
adamc@1251
|
2375 if !m1 = Arbitrary then
|
adamc@1251
|
2376 ()
|
adamc@1251
|
2377 else
|
adamc@1251
|
2378 m1 := Decreasing
|
adamc@1251
|
2379 else
|
adamc@1251
|
2380 m1 := Arbitrary
|
adamc@1251
|
2381 | Unknown => m1 := Arbitrary)
|
adamc@1251
|
2382 | _ => m1 := Arbitrary;
|
adamc@1251
|
2383 doArgs (pos + 1, args, modes))
|
adamc@1251
|
2384 | (_ :: _, []) => ()
|
adamc@1251
|
2385 | ([], ms) => app (fn m => m := Arbitrary) ms
|
adamc@1251
|
2386 in
|
adamc@1251
|
2387 doArgs (0, args, modes);
|
adamc@1251
|
2388 (EFfi ("Basis", "?"), loc)
|
adamc@1251
|
2389 end
|
adamc@1251
|
2390 else
|
adamc@1251
|
2391 default ()
|
adamc@1251
|
2392 | _ => default ()
|
adamc@1251
|
2393 in
|
adamc@1251
|
2394 explore (e, [])
|
adamc@1251
|
2395 end
|
adamc@1251
|
2396 | EAbs (x, t1, t2, e) => (EAbs (x, t1, t2, doExp (Unknown :: env) e), loc)
|
adamc@1251
|
2397 | EUnop (uo, e1) => (EUnop (uo, doExp env e1), loc)
|
adamc@1251
|
2398 | EBinop (bo, e1, e2) => (EBinop (bo, doExp env e1, doExp env e2), loc)
|
adamc@1251
|
2399 | ERecord xets => (ERecord (map (fn (x, e, t) => (x, doExp env e, t)) xets), loc)
|
adamc@1251
|
2400 | EField (e1, f) => (EField (doExp env e1, f), loc)
|
adamc@1251
|
2401 | ECase (e, pes, ts) =>
|
adamc@1251
|
2402 let
|
adamc@1251
|
2403 val source =
|
adamc@1251
|
2404 case #1 e of
|
adamc@1251
|
2405 ERel n =>
|
adamc@1251
|
2406 (case List.nth (env, n) of
|
adamc@1251
|
2407 Input n => SOME n
|
adamc@1251
|
2408 | SubInput n => SOME n
|
adamc@1251
|
2409 | Unknown => NONE)
|
adamc@1251
|
2410 | _ => NONE
|
adamc@1251
|
2411
|
adamc@1251
|
2412 fun doV v =
|
adamc@1251
|
2413 let
|
adamc@1251
|
2414 fun doPat (p, env) =
|
adamc@1251
|
2415 case #1 p of
|
adamc@1251
|
2416 PWild => env
|
adamc@1251
|
2417 | PVar _ => v :: env
|
adamc@1251
|
2418 | PPrim _ => env
|
adamc@1251
|
2419 | PCon (_, _, NONE) => env
|
adamc@1251
|
2420 | PCon (_, _, SOME p) => doPat (p, env)
|
adamc@1251
|
2421 | PRecord xpts => foldl (fn ((_, p, _), env) => doPat (p, env)) env xpts
|
adamc@1251
|
2422 | PNone _ => env
|
adamc@1251
|
2423 | PSome (_, p) => doPat (p, env)
|
adamc@1251
|
2424 in
|
adamc@1251
|
2425 (ECase (e, map (fn (p, e) => (p, doExp (doPat (p, env)) e)) pes, ts), loc)
|
adamc@1251
|
2426 end
|
adamc@1251
|
2427 in
|
adamc@1251
|
2428 case source of
|
adamc@1251
|
2429 NONE => doV Unknown
|
adamc@1251
|
2430 | SOME inp => doV (SubInput inp)
|
adamc@1251
|
2431 end
|
adamc@1251
|
2432 | EStrcat (e1, e2) => (EStrcat (doExp env e1, doExp env e2), loc)
|
adamc@1251
|
2433 | EError (e1, t) => (EError (doExp env e1, t), loc)
|
adamc@1251
|
2434 | EReturnBlob {blob = b, mimeType = m, t} =>
|
adamc@1251
|
2435 (EReturnBlob {blob = doExp env b, mimeType = doExp env m, t = t}, loc)
|
adamc@1251
|
2436 | ERedirect (e1, t) => (ERedirect (doExp env e1, t), loc)
|
adamc@1251
|
2437 | EWrite e1 => (EWrite (doExp env e1), loc)
|
adamc@1251
|
2438 | ESeq (e1, e2) => (ESeq (doExp env e1, doExp env e2), loc)
|
adamc@1251
|
2439 | ELet (x, t, e1, e2) => (ELet (x, t, doExp env e1, doExp (Unknown :: env) e2), loc)
|
adamc@1251
|
2440 | EClosure (n, es) => (EClosure (n, map (doExp env) es), loc)
|
adamc@1251
|
2441 | EQuery {exps, tables, state, query, body, initial} =>
|
adamc@1251
|
2442 (EQuery {exps = exps, tables = tables, state = state,
|
adamc@1251
|
2443 query = doExp env query,
|
adamc@1251
|
2444 body = doExp (Unknown :: Unknown :: env) body,
|
adamc@1251
|
2445 initial = doExp env initial}, loc)
|
adamc@1251
|
2446 | EDml e1 =>
|
adamc@1251
|
2447 (case parse dml e1 of
|
adamc@1251
|
2448 NONE => ()
|
adamc@1251
|
2449 | SOME c =>
|
adamc@1251
|
2450 case c of
|
adamc@1251
|
2451 Insert _ => ()
|
adamc@1251
|
2452 | Delete (tab, _) =>
|
adamc@1251
|
2453 tables := SS.add (!tables, tab)
|
adamc@1251
|
2454 | Update (tab, _, _) =>
|
adamc@1251
|
2455 tables := SS.add (!tables, tab);
|
adamc@1251
|
2456 (EDml (doExp env e1), loc))
|
adamc@1251
|
2457 | ENextval e1 => (ENextval (doExp env e1), loc)
|
adamc@1251
|
2458 | ESetval (e1, e2) => (ESetval (doExp env e1, doExp env e2), loc)
|
adamc@1251
|
2459 | EUnurlify (e1, t, b) => (EUnurlify (doExp env e1, t, b), loc)
|
adamc@1251
|
2460 | EJavaScript (m, e) => (EJavaScript (m, doExp env e), loc)
|
adamc@1251
|
2461 | ESignalReturn _ => e
|
adamc@1251
|
2462 | ESignalBind _ => e
|
adamc@1251
|
2463 | ESignalSource _ => e
|
adamc@1251
|
2464 | EServerCall _ => e
|
adamc@1251
|
2465 | ERecv _ => e
|
adamc@1251
|
2466 | ESleep _ => e
|
adamc@1251
|
2467 | ESpawn _ => e
|
adamc@1251
|
2468
|
adamc@1251
|
2469 val e = doExp env e
|
adamc@1251
|
2470 in
|
adamc@1251
|
2471 rfuns := IM.insert (!rfuns, n, {tables = !tables, cookies = !cookies,
|
adamc@1251
|
2472 args = map (fn r => !r) modes, body = e})
|
adamc@1251
|
2473 end
|
adamc@1251
|
2474
|
adamc@1251
|
2475 | DValRec _ => ErrorMsg.errorAt loc "Iflow can't check mutually-recursive functions yet."
|
adamc@1249
|
2476
|
adamc@1220
|
2477 | DPolicy pol =>
|
adamc@1218
|
2478 let
|
adamc@1236
|
2479 val rvN = ref 0
|
adamc@1236
|
2480 fun rv () =
|
adamc@1236
|
2481 let
|
adamc@1236
|
2482 val n = !rvN
|
adamc@1236
|
2483 in
|
adamc@1236
|
2484 rvN := n + 1;
|
adamc@1236
|
2485 Lvar n
|
adamc@1236
|
2486 end
|
adamc@1236
|
2487
|
adamc@1236
|
2488 val atoms = ref ([] : atom list)
|
adamc@1236
|
2489 fun doQ k = doQuery {Env = [],
|
adamc@1236
|
2490 NextVar = rv,
|
adamc@1236
|
2491 Add = fn a => atoms := a :: !atoms,
|
adamc@1236
|
2492 Save = fn () => !atoms,
|
adamc@1236
|
2493 Restore = fn ls => atoms := ls,
|
adam@1280
|
2494 Send = fn _ => (),
|
adamc@1238
|
2495 Cont = SomeCol (fn r => k (rev (!atoms), r))}
|
adamc@1238
|
2496
|
adamc@1247
|
2497 fun untab (tab, nams) = List.filter (fn AReln (Sql tab', [Lvar lv]) =>
|
adamc@1247
|
2498 tab' <> tab
|
adamc@1247
|
2499 orelse List.all (fn Lvar lv' => lv' <> lv
|
adamc@1247
|
2500 | _ => false) nams
|
adamc@1247
|
2501 | _ => true)
|
adamc@1218
|
2502 in
|
adamc@1220
|
2503 case pol of
|
adamc@1220
|
2504 PolClient e =>
|
adamc@1238
|
2505 doQ (fn (ats, {Outs = es, ...}) => St.allowSend (ats, es)) e
|
adamc@1220
|
2506 | PolInsert e =>
|
adamc@1238
|
2507 doQ (fn (ats, {New = SOME (tab, new), ...}) =>
|
adamc@1247
|
2508 St.allowInsert (AReln (Sql (tab ^ "$New"), [new]) :: untab (tab, [new]) ats)
|
adamc@1238
|
2509 | _ => raise Fail "Iflow: No New in mayInsert policy") e
|
adamc@1221
|
2510 | PolDelete e =>
|
adamc@1238
|
2511 doQ (fn (ats, {Old = SOME (tab, old), ...}) =>
|
adamc@1247
|
2512 St.allowDelete (AReln (Sql (tab ^ "$Old"), [old]) :: untab (tab, [old]) ats)
|
adamc@1238
|
2513 | _ => raise Fail "Iflow: No Old in mayDelete policy") e
|
adamc@1223
|
2514 | PolUpdate e =>
|
adamc@1238
|
2515 doQ (fn (ats, {New = SOME (tab, new), Old = SOME (_, old), ...}) =>
|
adamc@1238
|
2516 St.allowUpdate (AReln (Sql (tab ^ "$Old"), [old])
|
adamc@1238
|
2517 :: AReln (Sql (tab ^ "$New"), [new])
|
adamc@1247
|
2518 :: untab (tab, [new, old]) ats)
|
adamc@1238
|
2519 | _ => raise Fail "Iflow: No New or Old in mayUpdate policy") e
|
adamc@1229
|
2520 | PolSequence e =>
|
adamc@1229
|
2521 (case #1 e of
|
adamc@1229
|
2522 EPrim (Prim.String seq) =>
|
adamc@1229
|
2523 let
|
adamc@1236
|
2524 val p = AReln (Sql (String.extract (seq, 3, NONE)), [Lvar 0])
|
adamc@1229
|
2525 val outs = [Lvar 0]
|
adamc@1229
|
2526 in
|
adamc@1236
|
2527 St.allowSend ([p], outs)
|
adamc@1229
|
2528 end
|
adamc@1236
|
2529 | _ => ())
|
adam@1280
|
2530 | PolEqualKnown {table = tab, field = nm} =>
|
adam@1280
|
2531 (case #1 tab of
|
adam@1280
|
2532 EPrim (Prim.String tab) => St.allowEqualKnown {table = String.extract (tab, 3, NONE),
|
adam@1280
|
2533 field = nm}
|
adam@1280
|
2534 | _ => ErrorMsg.errorAt loc "Table for 'equalKnown' policy isn't fully resolved.")
|
adamc@1218
|
2535 end
|
adamc@1214
|
2536
|
adamc@1236
|
2537 | _ => ()
|
adamc@1200
|
2538 in
|
adamc@1236
|
2539 app decl file
|
adamc@1200
|
2540 end
|
adamc@1200
|
2541
|
adamc@1213
|
2542 val check = fn file =>
|
adamc@1213
|
2543 let
|
adamc@1213
|
2544 val oldInline = Settings.getMonoInline ()
|
adamc@1213
|
2545 in
|
adamc@1213
|
2546 (Settings.setMonoInline (case Int.maxInt of
|
adamc@1213
|
2547 NONE => 1000000
|
adamc@1213
|
2548 | SOME n => n);
|
adamc@1213
|
2549 check file;
|
adamc@1213
|
2550 Settings.setMonoInline oldInline)
|
adamc@1213
|
2551 handle ex => (Settings.setMonoInline oldInline;
|
adamc@1213
|
2552 raise ex)
|
adamc@1213
|
2553 end
|
adamc@1213
|
2554
|
adamc@1200
|
2555 end
|