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
|
adamc@1236
|
1231 val allowInsert : atom list -> unit
|
adamc@1236
|
1232 val insert : ErrorMsg.span -> unit
|
adamc@1236
|
1233
|
adamc@1236
|
1234 val allowDelete : atom list -> unit
|
adamc@1236
|
1235 val delete : ErrorMsg.span -> unit
|
adamc@1236
|
1236
|
adamc@1236
|
1237 val allowUpdate : atom list -> unit
|
adamc@1236
|
1238 val update : ErrorMsg.span -> unit
|
adamc@1236
|
1239
|
adamc@1236
|
1240 val havocReln : reln -> unit
|
adamc@1245
|
1241 val havocCookie : string -> unit
|
adamc@1238
|
1242
|
adamc@1251
|
1243 val check : atom -> bool
|
adamc@1251
|
1244
|
adamc@1238
|
1245 val debug : unit -> unit
|
adamc@1236
|
1246 end = struct
|
adamc@1236
|
1247
|
adamc@1236
|
1248 val hnames = ref 1
|
adamc@1236
|
1249
|
adamc@1244
|
1250 type hyps = int * atom list * bool ref
|
adamc@1236
|
1251
|
adamc@1236
|
1252 val db = Cc.database ()
|
adamc@1244
|
1253 val path = ref ([] : ((int * atom list) * check) option ref list)
|
adamc@1244
|
1254 val hyps = ref (0, [] : atom list, ref false)
|
adamc@1236
|
1255 val nvar = ref 0
|
adamc@1236
|
1256
|
adamc@1244
|
1257 fun setHyps (n', hs) =
|
adamc@1236
|
1258 let
|
adamc@1244
|
1259 val (n, _, _) = !hyps
|
adamc@1236
|
1260 in
|
adamc@1236
|
1261 if n' = n then
|
adamc@1236
|
1262 ()
|
adamc@1236
|
1263 else
|
adamc@1244
|
1264 (hyps := (n', hs, ref false);
|
adamc@1236
|
1265 Cc.clear db;
|
adamc@1236
|
1266 app (fn a => Cc.assert (db, a)) hs)
|
adamc@1236
|
1267 end
|
adamc@1236
|
1268
|
adamc@1244
|
1269 fun useKeys () =
|
adamc@1244
|
1270 let
|
adamc@1244
|
1271 val changed = ref false
|
adamc@1244
|
1272
|
adamc@1244
|
1273 fun findKeys (hyps, acc) =
|
adamc@1244
|
1274 case hyps of
|
adamc@1247
|
1275 [] => rev acc
|
adamc@1244
|
1276 | (a as AReln (Sql tab, [r1])) :: hyps =>
|
adamc@1244
|
1277 (case SM.find (!tabs, tab) of
|
adamc@1244
|
1278 NONE => findKeys (hyps, a :: acc)
|
adamc@1244
|
1279 | SOME (_, []) => findKeys (hyps, a :: acc)
|
adamc@1244
|
1280 | SOME (_, ks) =>
|
adamc@1244
|
1281 let
|
adamc@1244
|
1282 fun finder (hyps, acc) =
|
adamc@1244
|
1283 case hyps of
|
adamc@1247
|
1284 [] => rev acc
|
adamc@1244
|
1285 | (a as AReln (Sql tab', [r2])) :: hyps =>
|
adamc@1244
|
1286 if tab' = tab andalso
|
adamc@1244
|
1287 List.exists (List.all (fn f =>
|
adamc@1244
|
1288 let
|
adamc@1244
|
1289 val r =
|
adamc@1244
|
1290 Cc.check (db,
|
adamc@1244
|
1291 AReln (Eq, [Proj (r1, f),
|
adamc@1244
|
1292 Proj (r2, f)]))
|
adamc@1244
|
1293 in
|
adamc@1244
|
1294 (*Print.prefaces "Fs"
|
adamc@1244
|
1295 [("tab",
|
adamc@1244
|
1296 Print.PD.string tab),
|
adamc@1244
|
1297 ("r1",
|
adamc@1244
|
1298 p_exp (Proj (r1, f))),
|
adamc@1244
|
1299 ("r2",
|
adamc@1244
|
1300 p_exp (Proj (r2, f))),
|
adamc@1244
|
1301 ("r",
|
adamc@1244
|
1302 Print.PD.string
|
adamc@1244
|
1303 (Bool.toString r))];*)
|
adamc@1244
|
1304 r
|
adamc@1244
|
1305 end)) ks then
|
adamc@1244
|
1306 (changed := true;
|
adamc@1244
|
1307 Cc.assert (db, AReln (Eq, [r1, r2]));
|
adamc@1244
|
1308 finder (hyps, acc))
|
adamc@1244
|
1309 else
|
adamc@1244
|
1310 finder (hyps, a :: acc)
|
adamc@1244
|
1311 | a :: hyps => finder (hyps, a :: acc)
|
adamc@1244
|
1312
|
adamc@1244
|
1313 val hyps = finder (hyps, [])
|
adamc@1244
|
1314 in
|
adamc@1246
|
1315 findKeys (hyps, a :: acc)
|
adamc@1244
|
1316 end)
|
adamc@1244
|
1317 | a :: hyps => findKeys (hyps, a :: acc)
|
adamc@1244
|
1318
|
adamc@1244
|
1319 fun loop hs =
|
adamc@1244
|
1320 let
|
adamc@1244
|
1321 val hs = findKeys (hs, [])
|
adamc@1244
|
1322 in
|
adamc@1244
|
1323 if !changed then
|
adamc@1244
|
1324 (changed := false;
|
adamc@1244
|
1325 loop hs)
|
adamc@1244
|
1326 else
|
adamc@1244
|
1327 ()
|
adamc@1244
|
1328 end
|
adamc@1244
|
1329
|
adamc@1244
|
1330 val (_, hs, _) = !hyps
|
adamc@1244
|
1331 in
|
adamc@1246
|
1332 (*print "useKeys\n";*)
|
adamc@1244
|
1333 loop hs
|
adamc@1244
|
1334 end
|
adamc@1244
|
1335
|
adamc@1244
|
1336 fun complete () =
|
adamc@1244
|
1337 let
|
adamc@1244
|
1338 val (_, _, bf) = !hyps
|
adamc@1244
|
1339 in
|
adamc@1244
|
1340 if !bf then
|
adamc@1244
|
1341 ()
|
adamc@1244
|
1342 else
|
adamc@1244
|
1343 (bf := true;
|
adamc@1244
|
1344 useKeys ())
|
adamc@1244
|
1345 end
|
adamc@1244
|
1346
|
adamc@1244
|
1347 type stashed = int * ((int * atom list) * check) option ref list * (int * atom list)
|
adamc@1244
|
1348 fun stash () = (!nvar, !path, (#1 (!hyps), #2 (!hyps)))
|
adamc@1236
|
1349 fun reinstate (nv, p, h) =
|
adamc@1236
|
1350 (nvar := nv;
|
adamc@1236
|
1351 path := p;
|
adamc@1236
|
1352 setHyps h)
|
adamc@1236
|
1353
|
adamc@1249
|
1354 type stashedPath = ((int * atom list) * check) option ref list
|
adamc@1249
|
1355 fun stashPath () = !path
|
adamc@1249
|
1356 fun reinstatePath p = path := p
|
adamc@1249
|
1357
|
adamc@1236
|
1358 fun nextVar () =
|
adamc@1236
|
1359 let
|
adamc@1236
|
1360 val n = !nvar
|
adamc@1236
|
1361 in
|
adamc@1236
|
1362 nvar := n + 1;
|
adamc@1236
|
1363 n
|
adamc@1236
|
1364 end
|
adamc@1236
|
1365
|
adamc@1236
|
1366 fun assert ats =
|
adamc@1236
|
1367 let
|
adamc@1236
|
1368 val n = !hnames
|
adamc@1244
|
1369 val (_, hs, _) = !hyps
|
adamc@1236
|
1370 in
|
adamc@1236
|
1371 hnames := n + 1;
|
adamc@1244
|
1372 hyps := (n, ats @ hs, ref false);
|
adamc@1236
|
1373 app (fn a => Cc.assert (db, a)) ats
|
adamc@1236
|
1374 end
|
adamc@1236
|
1375
|
adamc@1244
|
1376 fun addPath c = path := ref (SOME ((#1 (!hyps), #2 (!hyps)), c)) :: !path
|
adamc@1236
|
1377
|
adamc@1236
|
1378 val sendable = ref ([] : (atom list * exp list) list)
|
adamc@1236
|
1379
|
adamc@1238
|
1380 fun checkGoals goals k =
|
adamc@1238
|
1381 let
|
adamc@1238
|
1382 fun checkGoals goals unifs =
|
adamc@1238
|
1383 case goals of
|
adamc@1238
|
1384 [] => k unifs
|
adamc@1238
|
1385 | AReln (Sql tab, [Lvar lv]) :: goals =>
|
adamc@1238
|
1386 let
|
adamc@1238
|
1387 val saved = stash ()
|
adamc@1244
|
1388 val (_, hyps, _) = !hyps
|
adamc@1236
|
1389
|
adamc@1238
|
1390 fun tryAll unifs hyps =
|
adamc@1238
|
1391 case hyps of
|
adamc@1238
|
1392 [] => false
|
adamc@1238
|
1393 | AReln (Sql tab', [e]) :: hyps =>
|
adamc@1238
|
1394 (tab' = tab andalso
|
adamc@1238
|
1395 checkGoals goals (IM.insert (unifs, lv, e)))
|
adamc@1238
|
1396 orelse tryAll unifs hyps
|
adamc@1238
|
1397 | _ :: hyps => tryAll unifs hyps
|
adamc@1238
|
1398 in
|
adamc@1238
|
1399 tryAll unifs hyps
|
adamc@1238
|
1400 end
|
adamc@1243
|
1401 | (g as AReln (r, es)) :: goals =>
|
adamc@1244
|
1402 (complete ();
|
adamc@1245
|
1403 (if Cc.check (db, AReln (r, map (simplify unifs) es)) then
|
adamc@1245
|
1404 true
|
adamc@1245
|
1405 else
|
adamc@1245
|
1406 ((*Print.preface ("Fail", p_atom (AReln (r, map (simplify unifs) es)));*)
|
adamc@1245
|
1407 false))
|
adamc@1244
|
1408 andalso checkGoals goals unifs)
|
adamc@1238
|
1409 | ACond _ :: _ => false
|
adamc@1238
|
1410 in
|
adamc@1238
|
1411 checkGoals goals IM.empty
|
adamc@1238
|
1412 end
|
adamc@1236
|
1413
|
adamc@1253
|
1414 fun buildable (e, loc) =
|
adamc@1238
|
1415 let
|
adamc@1238
|
1416 fun doPols pols acc =
|
adamc@1236
|
1417 case pols of
|
adamc@1253
|
1418 [] =>
|
adamc@1253
|
1419 let
|
adamc@1253
|
1420 val b = Cc.builtFrom (db, {Base = acc, Derived = e})
|
adamc@1253
|
1421 in
|
adamc@1253
|
1422 (*Print.prefaces "buildable" [("Base", Print.p_list p_exp acc),
|
adamc@1253
|
1423 ("Derived", p_exp e),
|
adamc@1253
|
1424 ("Hyps", Print.p_list p_atom (#2 (!hyps))),
|
adamc@1253
|
1425 ("Good", Print.PD.string (Bool.toString b))];*)
|
adamc@1253
|
1426 b
|
adamc@1253
|
1427 end
|
adamc@1236
|
1428 | (goals, es) :: pols =>
|
adamc@1238
|
1429 checkGoals goals (fn unifs => doPols pols (map (simplify unifs) es @ acc))
|
adamc@1238
|
1430 orelse doPols pols acc
|
adamc@1236
|
1431 in
|
adamc@1238
|
1432 if doPols (!sendable) [] then
|
adamc@1238
|
1433 ()
|
adamc@1238
|
1434 else
|
adamc@1238
|
1435 let
|
adamc@1244
|
1436 val (_, hs, _) = !hyps
|
adamc@1238
|
1437 in
|
adamc@1238
|
1438 ErrorMsg.errorAt loc "The information flow policy may be violated here.";
|
adamc@1245
|
1439 Print.prefaces "Situation" [("User learns", p_exp e),
|
adamc@1253
|
1440 ("Hypotheses", Print.p_list p_atom hs),
|
adamc@1253
|
1441 ("E-graph", Cc.p_database db)]
|
adamc@1238
|
1442 end
|
adamc@1246
|
1443 end
|
adamc@1236
|
1444
|
adamc@1236
|
1445 fun checkPaths () =
|
adamc@1236
|
1446 let
|
adamc@1244
|
1447 val (n, hs, _) = !hyps
|
adamc@1244
|
1448 val hs = (n, hs)
|
adamc@1236
|
1449 in
|
adamc@1236
|
1450 app (fn r =>
|
adamc@1236
|
1451 case !r of
|
adamc@1236
|
1452 NONE => ()
|
adamc@1236
|
1453 | SOME (hs, e) =>
|
adamc@1236
|
1454 (r := NONE;
|
adamc@1236
|
1455 setHyps hs;
|
adamc@1253
|
1456 buildable e)) (!path);
|
adamc@1236
|
1457 setHyps hs
|
adamc@1236
|
1458 end
|
adamc@1236
|
1459
|
adamc@1238
|
1460 fun allowSend v = ((*Print.prefaces "Allow" [("goals", Print.p_list p_atom (#1 v)),
|
adamc@1243
|
1461 ("exps", Print.p_list p_exp (#2 v))];*)
|
adamc@1238
|
1462 sendable := v :: !sendable)
|
adamc@1236
|
1463
|
adamc@1253
|
1464 fun send (e, loc) = ((*Print.preface ("Send[" ^ Bool.toString uk ^ "]", p_exp e);*)
|
adamc@1253
|
1465 complete ();
|
adamc@1253
|
1466 checkPaths ();
|
adamc@1253
|
1467 if isKnown e then
|
adamc@1253
|
1468 ()
|
adamc@1253
|
1469 else
|
adamc@1253
|
1470 buildable (e, loc))
|
adamc@1236
|
1471
|
adamc@1236
|
1472 fun doable pols (loc : ErrorMsg.span) =
|
adamc@1236
|
1473 let
|
adamc@1236
|
1474 val pols = !pols
|
adamc@1236
|
1475 in
|
adamc@1244
|
1476 complete ();
|
adamc@1236
|
1477 if List.exists (fn goals =>
|
adamc@1238
|
1478 if checkGoals goals (fn _ => true) then
|
adamc@1238
|
1479 ((*Print.prefaces "Match" [("goals", Print.p_list p_atom goals),
|
adamc@1238
|
1480 ("hyps", Print.p_list p_atom (#2 (!hyps)))];*)
|
adamc@1238
|
1481 true)
|
adamc@1238
|
1482 else
|
adamc@1246
|
1483 ((*Print.prefaces "No match" [("goals", Print.p_list p_atom goals)(*,
|
adamc@1246
|
1484 ("hyps", Print.p_list p_atom (#2 (!hyps)))*)];*)
|
adamc@1238
|
1485 false)) pols then
|
adamc@1236
|
1486 ()
|
adamc@1236
|
1487 else
|
adamc@1236
|
1488 let
|
adamc@1244
|
1489 val (_, hs, _) = !hyps
|
adamc@1236
|
1490 in
|
adamc@1236
|
1491 ErrorMsg.errorAt loc "The database update policy may be violated here.";
|
adamc@1250
|
1492 Print.prefaces "Situation" [("Hypotheses", Print.p_list p_atom hs)(*,
|
adamc@1250
|
1493 ("E-graph", Cc.p_database db)*)]
|
adamc@1236
|
1494 end
|
adamc@1236
|
1495 end
|
adamc@1236
|
1496
|
adamc@1236
|
1497 val insertable = ref ([] : atom list list)
|
adamc@1236
|
1498 fun allowInsert v = insertable := v :: !insertable
|
adamc@1236
|
1499 val insert = doable insertable
|
adamc@1236
|
1500
|
adamc@1236
|
1501 val updatable = ref ([] : atom list list)
|
adamc@1236
|
1502 fun allowUpdate v = updatable := v :: !updatable
|
adamc@1236
|
1503 val update = doable updatable
|
adamc@1236
|
1504
|
adamc@1236
|
1505 val deletable = ref ([] : atom list list)
|
adamc@1236
|
1506 fun allowDelete v = deletable := v :: !deletable
|
adamc@1236
|
1507 val delete = doable deletable
|
adamc@1236
|
1508
|
adamc@1238
|
1509 fun reset () = (Cc.clear db;
|
adamc@1238
|
1510 path := [];
|
adamc@1244
|
1511 hyps := (0, [], ref false);
|
adamc@1238
|
1512 nvar := 0;
|
adamc@1238
|
1513 sendable := [];
|
adamc@1238
|
1514 insertable := [];
|
adamc@1238
|
1515 updatable := [];
|
adamc@1238
|
1516 deletable := [])
|
adamc@1238
|
1517
|
adamc@1236
|
1518 fun havocReln r =
|
adamc@1236
|
1519 let
|
adamc@1236
|
1520 val n = !hnames
|
adamc@1244
|
1521 val (_, hs, _) = !hyps
|
adamc@1236
|
1522 in
|
adamc@1236
|
1523 hnames := n + 1;
|
adamc@1244
|
1524 hyps := (n, List.filter (fn AReln (r', _) => r' <> r | _ => true) hs, ref false)
|
adamc@1236
|
1525 end
|
adamc@1236
|
1526
|
adamc@1245
|
1527 fun havocCookie cname =
|
adamc@1245
|
1528 let
|
adamc@1245
|
1529 val cname = "cookie/" ^ cname
|
adamc@1245
|
1530 val n = !hnames
|
adamc@1245
|
1531 val (_, hs, _) = !hyps
|
adamc@1245
|
1532 in
|
adamc@1245
|
1533 hnames := n + 1;
|
adamc@1245
|
1534 hyps := (n, List.filter (fn AReln (Eq, [_, Func (Other f, [])]) => f <> cname | _ => true) hs, ref false)
|
adamc@1245
|
1535 end
|
adamc@1245
|
1536
|
adamc@1251
|
1537 fun check a = Cc.check (db, a)
|
adamc@1251
|
1538
|
adamc@1238
|
1539 fun debug () =
|
adamc@1238
|
1540 let
|
adamc@1244
|
1541 val (_, hs, _) = !hyps
|
adamc@1238
|
1542 in
|
adamc@1238
|
1543 Print.preface ("Hyps", Print.p_list p_atom hs)
|
adamc@1238
|
1544 end
|
adamc@1238
|
1545
|
adamc@1236
|
1546 end
|
adamc@1236
|
1547
|
adamc@1236
|
1548
|
adamc@1215
|
1549 fun removeDups (ls : (string * string) list) =
|
adamc@1211
|
1550 case ls of
|
adamc@1211
|
1551 [] => []
|
adamc@1211
|
1552 | x :: ls =>
|
adamc@1211
|
1553 let
|
adamc@1211
|
1554 val ls = removeDups ls
|
adamc@1211
|
1555 in
|
adamc@1211
|
1556 if List.exists (fn x' => x' = x) ls then
|
adamc@1211
|
1557 ls
|
adamc@1211
|
1558 else
|
adamc@1211
|
1559 x :: ls
|
adamc@1211
|
1560 end
|
adamc@1211
|
1561
|
adamc@1241
|
1562 fun deinj env e =
|
adamc@1241
|
1563 case #1 e of
|
adamc@1241
|
1564 ERel n => SOME (List.nth (env, n))
|
adamc@1241
|
1565 | EField (e, f) =>
|
adamc@1241
|
1566 (case deinj env e of
|
adamc@1241
|
1567 NONE => NONE
|
adamc@1241
|
1568 | SOME e => SOME (Proj (e, f)))
|
adamc@1251
|
1569 | EApp ((EFfi mf, _), e) =>
|
adamc@1251
|
1570 if Settings.isEffectful mf orelse Settings.isBenignEffectful mf then
|
adamc@1251
|
1571 NONE
|
adamc@1251
|
1572 else (case deinj env e of
|
adamc@1251
|
1573 NONE => NONE
|
adamc@1251
|
1574 | SOME e => SOME (Func (Other (#1 mf ^ "." ^ #2 mf), [e])))
|
adamc@1241
|
1575 | _ => NONE
|
adamc@1241
|
1576
|
adamc@1220
|
1577 fun expIn rv env rvOf =
|
adamc@1220
|
1578 let
|
adamc@1236
|
1579 fun expIn e =
|
adamc@1220
|
1580 let
|
adamc@1236
|
1581 fun default () = inl (rv ())
|
adamc@1220
|
1582 in
|
adamc@1220
|
1583 case e of
|
adamc@1236
|
1584 SqConst p => inl (Const p)
|
adamc@1243
|
1585 | SqTrue => inl (Func (DtCon0 "Basis.bool.True", []))
|
adamc@1243
|
1586 | SqFalse => inl (Func (DtCon0 "Basis.bool.False", []))
|
adamc@1253
|
1587 | Null => inl (Func (DtCon0 "None", []))
|
adamc@1250
|
1588 | SqNot e =>
|
adamc@1250
|
1589 inr (case expIn e of
|
adamc@1250
|
1590 inl e => Reln (Eq, [e, Func (DtCon0 "Basis.bool.False", [])])
|
adamc@1250
|
1591 | inr _ => Unknown)
|
adamc@1236
|
1592 | Field (v, f) => inl (Proj (rvOf v, f))
|
adamc@1239
|
1593 | Computed _ => default ()
|
adamc@1220
|
1594 | Binop (bo, e1, e2) =>
|
adamc@1220
|
1595 let
|
adamc@1236
|
1596 val e1 = expIn e1
|
adamc@1236
|
1597 val e2 = expIn e2
|
adamc@1220
|
1598 in
|
adamc@1236
|
1599 inr (case (bo, e1, e2) of
|
adamc@1236
|
1600 (Exps f, inl e1, inl e2) => f (e1, e2)
|
adamc@1243
|
1601 | (Props f, v1, v2) =>
|
adamc@1243
|
1602 let
|
adamc@1243
|
1603 fun pin v =
|
adamc@1243
|
1604 case v of
|
adamc@1243
|
1605 inl e => Reln (Eq, [e, Func (DtCon0 "Basis.bool.True", [])])
|
adamc@1243
|
1606 | inr p => p
|
adamc@1243
|
1607 in
|
adamc@1243
|
1608 f (pin v1, pin v2)
|
adamc@1243
|
1609 end
|
adamc@1236
|
1610 | _ => Unknown)
|
adamc@1220
|
1611 end
|
adamc@1220
|
1612 | SqKnown e =>
|
adamc@1236
|
1613 (case expIn e of
|
adamc@1236
|
1614 inl e => inr (Reln (Known, [e]))
|
adamc@1236
|
1615 | _ => inr Unknown)
|
adamc@1220
|
1616 | Inj e =>
|
adamc@1241
|
1617 inl (case deinj env e of
|
adamc@1241
|
1618 NONE => rv ()
|
adamc@1241
|
1619 | SOME e => e)
|
adamc@1220
|
1620 | SqFunc (f, e) =>
|
adamc@1236
|
1621 (case expIn e of
|
adamc@1236
|
1622 inl e => inl (Func (Other f, [e]))
|
adamc@1220
|
1623 | _ => default ())
|
adamc@1220
|
1624
|
adamc@1252
|
1625 | Unmodeled => inl (Func (Other "allow", [rv ()]))
|
adamc@1220
|
1626 end
|
adamc@1220
|
1627 in
|
adamc@1220
|
1628 expIn
|
adamc@1220
|
1629 end
|
adamc@1216
|
1630
|
adamc@1236
|
1631 fun decomp {Save = save, Restore = restore, Add = add} =
|
adamc@1216
|
1632 let
|
adamc@1236
|
1633 fun go p k =
|
adamc@1236
|
1634 case p of
|
adamc@1238
|
1635 True => (k () handle Cc.Contradiction => ())
|
adamc@1236
|
1636 | False => ()
|
adamc@1236
|
1637 | Unknown => ()
|
adamc@1236
|
1638 | And (p1, p2) => go p1 (fn () => go p2 k)
|
adamc@1236
|
1639 | Or (p1, p2) =>
|
adamc@1236
|
1640 let
|
adamc@1236
|
1641 val saved = save ()
|
adamc@1236
|
1642 in
|
adamc@1236
|
1643 go p1 k;
|
adamc@1236
|
1644 restore saved;
|
adamc@1236
|
1645 go p2 k
|
adamc@1236
|
1646 end
|
adamc@1236
|
1647 | Reln x => (add (AReln x); k ())
|
adamc@1236
|
1648 | Cond x => (add (ACond x); k ())
|
adamc@1236
|
1649 in
|
adamc@1236
|
1650 go
|
adamc@1236
|
1651 end
|
adamc@1236
|
1652
|
adamc@1236
|
1653 datatype queryMode =
|
adamc@1238
|
1654 SomeCol of {New : (string * exp) option, Old : (string * exp) option, Outs : exp list} -> unit
|
adamc@1236
|
1655 | AllCols of exp -> unit
|
adamc@1236
|
1656
|
adamc@1236
|
1657 type 'a doQuery = {
|
adamc@1236
|
1658 Env : exp list,
|
adamc@1236
|
1659 NextVar : unit -> exp,
|
adamc@1236
|
1660 Add : atom -> unit,
|
adamc@1236
|
1661 Save : unit -> 'a,
|
adamc@1236
|
1662 Restore : 'a -> unit,
|
adam@1282
|
1663 Cont : queryMode
|
adamc@1236
|
1664 }
|
adamc@1236
|
1665
|
adamc@1241
|
1666 fun doQuery (arg : 'a doQuery) (e as (_, loc)) =
|
adamc@1236
|
1667 let
|
adamc@1241
|
1668 fun default () = ErrorMsg.errorAt loc "Information flow checker can't parse SQL query"
|
adamc@1216
|
1669 in
|
adamc@1216
|
1670 case parse query e of
|
adamc@1216
|
1671 NONE => default ()
|
adamc@1227
|
1672 | SOME q =>
|
adamc@1216
|
1673 let
|
adamc@1236
|
1674 fun doQuery q =
|
adamc@1227
|
1675 case q of
|
adamc@1227
|
1676 Query1 r =>
|
adamc@1227
|
1677 let
|
adamc@1238
|
1678 val new = ref NONE
|
adamc@1238
|
1679 val old = ref NONE
|
adamc@1238
|
1680
|
adamc@1238
|
1681 val rvs = map (fn (tab, v) =>
|
adamc@1238
|
1682 let
|
adamc@1238
|
1683 val nv = #NextVar arg ()
|
adamc@1238
|
1684 in
|
adamc@1238
|
1685 case v of
|
adamc@1238
|
1686 "New" => new := SOME (tab, nv)
|
adamc@1238
|
1687 | "Old" => old := SOME (tab, nv)
|
adamc@1238
|
1688 | _ => ();
|
adamc@1238
|
1689 (v, nv)
|
adamc@1238
|
1690 end) (#From r)
|
adamc@1214
|
1691
|
adamc@1227
|
1692 fun rvOf v =
|
adamc@1227
|
1693 case List.find (fn (v', _) => v' = v) rvs of
|
adamc@1227
|
1694 NONE => raise Fail "Iflow.queryProp: Bad table variable"
|
adamc@1227
|
1695 | SOME (_, e) => e
|
adamc@1214
|
1696
|
adamc@1236
|
1697 val expIn = expIn (#NextVar arg) (#Env arg) rvOf
|
adamc@1236
|
1698
|
adamc@1236
|
1699 val saved = #Save arg ()
|
adamc@1236
|
1700 fun addFrom () = app (fn (t, v) => #Add arg (AReln (Sql t, [rvOf v]))) (#From r)
|
adamc@1236
|
1701
|
adam@1282
|
1702 fun usedFields e =
|
adamc@1227
|
1703 case e of
|
adam@1282
|
1704 SqConst _ => []
|
adam@1282
|
1705 | SqTrue => []
|
adam@1282
|
1706 | SqFalse => []
|
adam@1282
|
1707 | Null => []
|
adam@1282
|
1708 | SqNot e => usedFields e
|
adam@1282
|
1709 | Field (v, f) => [(false, Proj (rvOf v, f))]
|
adam@1282
|
1710 | Computed _ => []
|
adam@1282
|
1711 | Binop (_, e1, e2) => usedFields e1 @ usedFields e2
|
adam@1282
|
1712 | SqKnown _ => []
|
adam@1282
|
1713 | Inj e =>
|
adam@1282
|
1714 (case deinj (#Env arg) e of
|
adam@1282
|
1715 NONE => (ErrorMsg.errorAt loc "Expression injected into SQL is too complicated";
|
adam@1282
|
1716 [])
|
adam@1282
|
1717 | SOME e => [(true, e)])
|
adam@1282
|
1718 | SqFunc (_, e) => usedFields e
|
adam@1282
|
1719 | Unmodeled => []
|
adamc@1214
|
1720
|
adamc@1236
|
1721 fun normal' () =
|
adamc@1236
|
1722 case #Cont arg of
|
adamc@1236
|
1723 SomeCol k =>
|
adamc@1227
|
1724 let
|
adamc@1236
|
1725 val sis = map (fn si =>
|
adamc@1236
|
1726 case si of
|
adamc@1236
|
1727 SqField (v, f) => Proj (rvOf v, f)
|
adamc@1236
|
1728 | SqExp (e, f) =>
|
adamc@1236
|
1729 case expIn e of
|
adamc@1236
|
1730 inr _ => #NextVar arg ()
|
adamc@1236
|
1731 | inl e => e) (#Select r)
|
adamc@1227
|
1732 in
|
adamc@1238
|
1733 k {New = !new, Old = !old, Outs = sis}
|
adamc@1227
|
1734 end
|
adamc@1236
|
1735 | AllCols k =>
|
adamc@1227
|
1736 let
|
adamc@1236
|
1737 val (ts, es) =
|
adamc@1236
|
1738 foldl (fn (si, (ts, es)) =>
|
adamc@1227
|
1739 case si of
|
adamc@1227
|
1740 SqField (v, f) =>
|
adamc@1227
|
1741 let
|
adamc@1227
|
1742 val fs = getOpt (SM.find (ts, v), SM.empty)
|
adamc@1227
|
1743 in
|
adamc@1236
|
1744 (SM.insert (ts, v, SM.insert (fs, f, Proj (rvOf v, f))), es)
|
adamc@1227
|
1745 end
|
adamc@1227
|
1746 | SqExp (e, f) =>
|
adamc@1227
|
1747 let
|
adamc@1236
|
1748 val e =
|
adamc@1236
|
1749 case expIn e of
|
adamc@1236
|
1750 inr _ => #NextVar arg ()
|
adamc@1236
|
1751 | inl e => e
|
adamc@1227
|
1752 in
|
adamc@1236
|
1753 (ts, SM.insert (es, f, e))
|
adamc@1227
|
1754 end)
|
adamc@1236
|
1755 (SM.empty, SM.empty) (#Select r)
|
adamc@1227
|
1756 in
|
adamc@1236
|
1757 k (Recd (map (fn (t, fs) => (t, Recd (SM.listItemsi fs)))
|
adamc@1236
|
1758 (SM.listItemsi ts)
|
adamc@1236
|
1759 @ SM.listItemsi es))
|
adamc@1227
|
1760 end
|
adamc@1227
|
1761
|
adamc@1236
|
1762 fun doWhere final =
|
adamc@1236
|
1763 (addFrom ();
|
adamc@1236
|
1764 case #Where r of
|
adamc@1253
|
1765 NONE => final ()
|
adamc@1236
|
1766 | SOME e =>
|
adamc@1243
|
1767 let
|
adamc@1243
|
1768 val p = case expIn e of
|
adamc@1243
|
1769 inl e => Reln (Eq, [e, Func (DtCon0 "Basis.bool.True", [])])
|
adamc@1243
|
1770 | inr p => p
|
adamc@1243
|
1771
|
adamc@1243
|
1772 val saved = #Save arg ()
|
adamc@1243
|
1773 in
|
adamc@1243
|
1774 decomp {Save = #Save arg, Restore = #Restore arg, Add = #Add arg}
|
adamc@1253
|
1775 p (fn () => final () handle Cc.Contradiction => ());
|
adamc@1243
|
1776 #Restore arg saved
|
adamc@1243
|
1777 end)
|
adamc@1236
|
1778 handle Cc.Contradiction => ()
|
adamc@1236
|
1779
|
adamc@1236
|
1780 fun normal () = doWhere normal'
|
adamc@1227
|
1781 in
|
adamc@1236
|
1782 (case #Select r of
|
adamc@1236
|
1783 [SqExp (Binop (Exps bo, Count, SqConst (Prim.Int 0)), f)] =>
|
adamc@1236
|
1784 (case bo (Const (Prim.Int 1), Const (Prim.Int 2)) of
|
adamc@1236
|
1785 Reln (Gt, [Const (Prim.Int 1), Const (Prim.Int 2)]) =>
|
adamc@1236
|
1786 (case #Cont arg of
|
adamc@1236
|
1787 SomeCol _ => ()
|
adamc@1236
|
1788 | AllCols k =>
|
adamc@1236
|
1789 let
|
adamc@1236
|
1790 fun answer e = k (Recd [(f, e)])
|
adamc@1236
|
1791
|
adamc@1236
|
1792 val saved = #Save arg ()
|
adamc@1238
|
1793 val () = (answer (Func (DtCon0 "Basis.bool.False", [])))
|
adamc@1238
|
1794 handle Cc.Contradiction => ()
|
adamc@1236
|
1795 in
|
adamc@1238
|
1796 #Restore arg saved;
|
adamc@1238
|
1797 (*print "True time!\n";*)
|
adamc@1236
|
1798 doWhere (fn () => answer (Func (DtCon0 "Basis.bool.True", [])));
|
adamc@1236
|
1799 #Restore arg saved
|
adamc@1236
|
1800 end)
|
adamc@1236
|
1801 | _ => normal ())
|
adamc@1236
|
1802 | _ => normal ())
|
adamc@1236
|
1803 before #Restore arg saved
|
adamc@1227
|
1804 end
|
adamc@1227
|
1805 | Union (q1, q2) =>
|
adamc@1220
|
1806 let
|
adamc@1236
|
1807 val saved = #Save arg ()
|
adamc@1220
|
1808 in
|
adamc@1236
|
1809 doQuery q1;
|
adamc@1236
|
1810 #Restore arg saved;
|
adamc@1236
|
1811 doQuery q2;
|
adamc@1236
|
1812 #Restore arg saved
|
adamc@1220
|
1813 end
|
adamc@1216
|
1814 in
|
adamc@1236
|
1815 doQuery q
|
adamc@1216
|
1816 end
|
adamc@1220
|
1817 end
|
adamc@1220
|
1818
|
adamc@1211
|
1819 fun evalPat env e (pt, _) =
|
adamc@1211
|
1820 case pt of
|
adamc@1236
|
1821 PWild => env
|
adamc@1236
|
1822 | PVar _ => e :: env
|
adamc@1236
|
1823 | PPrim _ => env
|
adamc@1236
|
1824 | PCon (_, pc, NONE) => (St.assert [AReln (PCon0 (patCon pc), [e])]; env)
|
adamc@1211
|
1825 | PCon (_, pc, SOME pt) =>
|
adamc@1211
|
1826 let
|
adamc@1236
|
1827 val env = evalPat env (Func (UnCon (patCon pc), [e])) pt
|
adamc@1211
|
1828 in
|
adamc@1236
|
1829 St.assert [AReln (PCon1 (patCon pc), [e])];
|
adamc@1236
|
1830 env
|
adamc@1211
|
1831 end
|
adamc@1211
|
1832 | PRecord xpts =>
|
adamc@1236
|
1833 foldl (fn ((x, pt, _), env) => evalPat env (Proj (e, x)) pt) env xpts
|
adamc@1236
|
1834 | PNone _ => (St.assert [AReln (PCon0 "None", [e])]; env)
|
adamc@1211
|
1835 | PSome (_, pt) =>
|
adamc@1211
|
1836 let
|
adamc@1236
|
1837 val env = evalPat env (Func (UnCon "Some", [e])) pt
|
adamc@1211
|
1838 in
|
adamc@1236
|
1839 St.assert [AReln (PCon1 "Some", [e])];
|
adamc@1236
|
1840 env
|
adamc@1211
|
1841 end
|
adamc@1211
|
1842
|
adamc@1251
|
1843 datatype arg_mode = Fixed | Decreasing | Arbitrary
|
adamc@1251
|
1844 type rfun = {args : arg_mode list, tables : SS.set, cookies : SS.set, body : Mono.exp}
|
adamc@1251
|
1845 val rfuns = ref (IM.empty : rfun IM.map)
|
adamc@1251
|
1846
|
adamc@1236
|
1847 fun evalExp env (e as (_, loc)) k =
|
adamc@1236
|
1848 let
|
adamc@1238
|
1849 (*val () = St.debug ()*)
|
adamc@1236
|
1850 (*val () = Print.preface ("evalExp", MonoPrint.p_exp MonoEnv.empty e)*)
|
adamc@1211
|
1851
|
adamc@1236
|
1852 fun default () = k (Var (St.nextVar ()))
|
adamc@1234
|
1853
|
adamc@1234
|
1854 fun doFfi (m, s, es) =
|
adamc@1234
|
1855 if m = "Basis" andalso SS.member (writers, s) then
|
adamc@1234
|
1856 let
|
adamc@1236
|
1857 fun doArgs es =
|
adamc@1236
|
1858 case es of
|
adamc@1245
|
1859 [] =>
|
adamc@1245
|
1860 (if s = "set_cookie" then
|
adamc@1245
|
1861 case es of
|
adamc@1245
|
1862 [_, cname, _, _, _] =>
|
adamc@1245
|
1863 (case #1 cname of
|
adamc@1245
|
1864 EPrim (Prim.String cname) =>
|
adamc@1245
|
1865 St.havocCookie cname
|
adamc@1245
|
1866 | _ => ())
|
adamc@1245
|
1867 | _ => ()
|
adamc@1245
|
1868 else
|
adamc@1245
|
1869 ();
|
adamc@1245
|
1870 k (Recd []))
|
adamc@1236
|
1871 | e :: es =>
|
adamc@1253
|
1872 evalExp env e (fn e => (St.send (e, loc); doArgs es))
|
adamc@1234
|
1873 in
|
adamc@1236
|
1874 doArgs es
|
adamc@1234
|
1875 end
|
adamc@1234
|
1876 else if Settings.isEffectful (m, s) andalso not (Settings.isBenignEffectful (m, s)) then
|
adamc@1234
|
1877 default ()
|
adamc@1234
|
1878 else
|
adamc@1234
|
1879 let
|
adamc@1236
|
1880 fun doArgs (es, acc) =
|
adamc@1236
|
1881 case es of
|
adamc@1236
|
1882 [] => k (Func (Other (m ^ "." ^ s), rev acc))
|
adamc@1236
|
1883 | e :: es =>
|
adamc@1236
|
1884 evalExp env e (fn e => doArgs (es, e :: acc))
|
adamc@1234
|
1885 in
|
adamc@1236
|
1886 doArgs (es, [])
|
adamc@1234
|
1887 end
|
adamc@1200
|
1888 in
|
adamc@1200
|
1889 case #1 e of
|
adamc@1236
|
1890 EPrim p => k (Const p)
|
adamc@1236
|
1891 | ERel n => k (List.nth (env, n))
|
adamc@1200
|
1892 | ENamed _ => default ()
|
adamc@1236
|
1893 | ECon (_, pc, NONE) => k (Func (DtCon0 (patCon pc), []))
|
adamc@1236
|
1894 | ECon (_, pc, SOME e) => evalExp env e (fn e => k (Func (DtCon1 (patCon pc), [e])))
|
adamc@1236
|
1895 | ENone _ => k (Func (DtCon0 "None", []))
|
adamc@1236
|
1896 | ESome (_, e) => evalExp env e (fn e => k (Func (DtCon1 "Some", [e])))
|
adamc@1200
|
1897 | EFfi _ => default ()
|
adamc@1213
|
1898
|
adamc@1250
|
1899 | EFfiApp ("Basis", "rand", []) =>
|
adamc@1250
|
1900 let
|
adamc@1250
|
1901 val e = Var (St.nextVar ())
|
adamc@1250
|
1902 in
|
adamc@1250
|
1903 St.assert [AReln (Known, [e])];
|
adamc@1250
|
1904 k e
|
adamc@1250
|
1905 end
|
adamc@1234
|
1906 | EFfiApp x => doFfi x
|
adamc@1234
|
1907 | EApp ((EFfi (m, s), _), e) => doFfi (m, s, [e])
|
adamc@1213
|
1908
|
adamc@1251
|
1909 | EApp (e1 as (EError _, _), _) => evalExp env e1 k
|
adamc@1251
|
1910
|
adamc@1251
|
1911 | EApp (e1, e2) =>
|
adamc@1251
|
1912 let
|
adamc@1251
|
1913 fun adefault () = (ErrorMsg.errorAt loc "Excessively fancy function call";
|
adamc@1251
|
1914 Print.preface ("Call", MonoPrint.p_exp MonoEnv.empty e);
|
adamc@1251
|
1915 default ())
|
adamc@1251
|
1916
|
adamc@1251
|
1917 fun doArgs (e, args) =
|
adamc@1251
|
1918 case #1 e of
|
adamc@1251
|
1919 EApp (e1, e2) => doArgs (e1, e2 :: args)
|
adamc@1251
|
1920 | ENamed n =>
|
adamc@1251
|
1921 (case IM.find (!rfuns, n) of
|
adamc@1251
|
1922 NONE => adefault ()
|
adamc@1251
|
1923 | SOME rf =>
|
adamc@1251
|
1924 if length (#args rf) <> length args then
|
adamc@1251
|
1925 adefault ()
|
adamc@1251
|
1926 else
|
adamc@1251
|
1927 let
|
adamc@1251
|
1928 val () = (SS.app (St.havocReln o Sql) (#tables rf);
|
adamc@1251
|
1929 SS.app St.havocCookie (#cookies rf))
|
adamc@1251
|
1930 val saved = St.stash ()
|
adamc@1251
|
1931
|
adamc@1251
|
1932 fun doArgs (args, modes, env') =
|
adamc@1251
|
1933 case (args, modes) of
|
adamc@1251
|
1934 ([], []) => (evalExp env' (#body rf) (fn _ => ());
|
adamc@1251
|
1935 St.reinstate saved;
|
adamc@1251
|
1936 default ())
|
adamc@1251
|
1937
|
adamc@1251
|
1938 | (arg :: args, mode :: modes) =>
|
adamc@1251
|
1939 evalExp env arg (fn arg =>
|
adamc@1251
|
1940 let
|
adamc@1251
|
1941 val v = case mode of
|
adamc@1251
|
1942 Arbitrary => Var (St.nextVar ())
|
adamc@1251
|
1943 | Fixed => arg
|
adamc@1251
|
1944 | Decreasing =>
|
adamc@1251
|
1945 let
|
adamc@1251
|
1946 val v = Var (St.nextVar ())
|
adamc@1251
|
1947 in
|
adamc@1251
|
1948 if St.check (AReln (Known, [arg])) then
|
adamc@1251
|
1949 St.assert [(AReln (Known, [v]))]
|
adamc@1251
|
1950 else
|
adamc@1251
|
1951 ();
|
adamc@1251
|
1952 v
|
adamc@1251
|
1953 end
|
adamc@1251
|
1954 in
|
adamc@1251
|
1955 doArgs (args, modes, v :: env')
|
adamc@1251
|
1956 end)
|
adamc@1251
|
1957 | _ => raise Fail "Iflow.doArgs: Impossible"
|
adamc@1251
|
1958 in
|
adamc@1251
|
1959 doArgs (args, #args rf, [])
|
adamc@1251
|
1960 end)
|
adamc@1251
|
1961 | _ => adefault ()
|
adamc@1251
|
1962 in
|
adamc@1251
|
1963 doArgs (e, [])
|
adamc@1251
|
1964 end
|
adamc@1213
|
1965
|
adamc@1200
|
1966 | EAbs _ => default ()
|
adamc@1236
|
1967 | EUnop (s, e1) => evalExp env e1 (fn e1 => k (Func (Other s, [e1])))
|
adam@1360
|
1968 | EBinop (_, s, e1, e2) => evalExp env e1 (fn e1 => evalExp env e2 (fn e2 => k (Func (Other s, [e1, e2]))))
|
adamc@1200
|
1969 | ERecord xets =>
|
adamc@1200
|
1970 let
|
adamc@1236
|
1971 fun doFields (xes, acc) =
|
adamc@1236
|
1972 case xes of
|
adamc@1236
|
1973 [] => k (Recd (rev acc))
|
adamc@1236
|
1974 | (x, e, _) :: xes =>
|
adamc@1236
|
1975 evalExp env e (fn e => doFields (xes, (x, e) :: acc))
|
adamc@1200
|
1976 in
|
adamc@1236
|
1977 doFields (xets, [])
|
adamc@1200
|
1978 end
|
adamc@1236
|
1979 | EField (e, s) => evalExp env e (fn e => k (Proj (e, s)))
|
adamc@1218
|
1980 | ECase (e, pes, {result = res, ...}) =>
|
adamc@1236
|
1981 evalExp env e (fn e =>
|
adamc@1248
|
1982 if List.all (fn (_, (EWrite (EPrim _, _), _)) => true
|
adamc@1248
|
1983 | _ => false) pes then
|
adamc@1253
|
1984 (St.send (e, loc);
|
adamc@1248
|
1985 k (Recd []))
|
adamc@1248
|
1986 else
|
adamc@1248
|
1987 (St.addPath (e, loc);
|
adamc@1248
|
1988 app (fn (p, pe) =>
|
adamc@1248
|
1989 let
|
adamc@1248
|
1990 val saved = St.stash ()
|
adamc@1248
|
1991 in
|
adamc@1248
|
1992 let
|
adamc@1248
|
1993 val env = evalPat env e p
|
adamc@1248
|
1994 in
|
adamc@1248
|
1995 evalExp env pe k;
|
adamc@1248
|
1996 St.reinstate saved
|
adamc@1248
|
1997 end
|
adamc@1248
|
1998 handle Cc.Contradiction => St.reinstate saved
|
adamc@1248
|
1999 end) pes))
|
adamc@1200
|
2000 | EStrcat (e1, e2) =>
|
adamc@1236
|
2001 evalExp env e1 (fn e1 =>
|
adamc@1236
|
2002 evalExp env e2 (fn e2 =>
|
adamc@1236
|
2003 k (Func (Other "cat", [e1, e2]))))
|
adamc@1253
|
2004 | EError (e, _) => evalExp env e (fn e => St.send (e, loc))
|
adamc@1200
|
2005 | EReturnBlob {blob = b, mimeType = m, ...} =>
|
adamc@1236
|
2006 evalExp env b (fn b =>
|
adamc@1253
|
2007 (St.send (b, loc);
|
adamc@1236
|
2008 evalExp env m
|
adamc@1253
|
2009 (fn m => St.send (m, loc))))
|
adamc@1200
|
2010 | ERedirect (e, _) =>
|
adamc@1253
|
2011 evalExp env e (fn e => St.send (e, loc))
|
adamc@1200
|
2012 | EWrite e =>
|
adamc@1253
|
2013 evalExp env e (fn e => (St.send (e, loc);
|
adamc@1236
|
2014 k (Recd [])))
|
adamc@1200
|
2015 | ESeq (e1, e2) =>
|
adamc@1249
|
2016 let
|
adamc@1249
|
2017 val path = St.stashPath ()
|
adamc@1249
|
2018 in
|
adamc@1249
|
2019 evalExp env e1 (fn _ => (St.reinstatePath path; evalExp env e2 k))
|
adamc@1249
|
2020 end
|
adamc@1200
|
2021 | ELet (_, _, e1, e2) =>
|
adamc@1236
|
2022 evalExp env e1 (fn e1 => evalExp (e1 :: env) e2 k)
|
adamc@1200
|
2023 | EClosure (n, es) =>
|
adamc@1200
|
2024 let
|
adamc@1236
|
2025 fun doArgs (es, acc) =
|
adamc@1236
|
2026 case es of
|
adamc@1236
|
2027 [] => k (Func (Other ("Cl" ^ Int.toString n), rev acc))
|
adamc@1236
|
2028 | e :: es =>
|
adamc@1236
|
2029 evalExp env e (fn e => doArgs (es, e :: acc))
|
adamc@1200
|
2030 in
|
adamc@1236
|
2031 doArgs (es, [])
|
adamc@1200
|
2032 end
|
adamc@1200
|
2033
|
adamc@1235
|
2034 | EQuery {query = q, body = b, initial = i, state = state, ...} =>
|
adamc@1238
|
2035 evalExp env i (fn i =>
|
adamc@1238
|
2036 let
|
adamc@1238
|
2037 val r = Var (St.nextVar ())
|
adamc@1238
|
2038 val acc = Var (St.nextVar ())
|
adamc@1242
|
2039
|
adamc@1249
|
2040 val (ts, cs) = MonoUtil.Exp.fold {typ = fn (_, st) => st,
|
adamc@1249
|
2041 exp = fn (e, st as (cs, ts)) =>
|
adamc@1242
|
2042 case e of
|
adam@1293
|
2043 EDml (e, _) =>
|
adamc@1242
|
2044 (case parse dml e of
|
adamc@1249
|
2045 NONE => st
|
adamc@1242
|
2046 | SOME c =>
|
adamc@1242
|
2047 case c of
|
adamc@1249
|
2048 Insert _ => st
|
adamc@1242
|
2049 | Delete (tab, _) =>
|
adamc@1249
|
2050 (cs, SS.add (ts, tab))
|
adamc@1242
|
2051 | Update (tab, _, _) =>
|
adamc@1249
|
2052 (cs, SS.add (ts, tab)))
|
adamc@1249
|
2053 | EFfiApp ("Basis", "set_cookie",
|
adamc@1249
|
2054 [_, (EPrim (Prim.String cname), _),
|
adamc@1249
|
2055 _, _, _]) =>
|
adamc@1249
|
2056 (SS.add (cs, cname), ts)
|
adamc@1249
|
2057 | _ => st}
|
adamc@1249
|
2058 (SS.empty, SS.empty) b
|
adamc@1238
|
2059 in
|
adamc@1249
|
2060 case (#1 state, SS.isEmpty ts, SS.isEmpty cs) of
|
adamc@1249
|
2061 (TRecord [], true, true) => ()
|
adamc@1249
|
2062 | _ =>
|
adamc@1249
|
2063 let
|
adamc@1249
|
2064 val saved = St.stash ()
|
adamc@1249
|
2065 in
|
adamc@1249
|
2066 (k i)
|
adamc@1249
|
2067 handle Cc.Contradiction => ();
|
adamc@1249
|
2068 St.reinstate saved
|
adamc@1249
|
2069 end;
|
adamc@1249
|
2070
|
adamc@1249
|
2071 SS.app (St.havocReln o Sql) ts;
|
adamc@1249
|
2072 SS.app St.havocCookie cs;
|
adamc@1242
|
2073
|
adamc@1242
|
2074 doQuery {Env = env,
|
adamc@1242
|
2075 NextVar = Var o St.nextVar,
|
adamc@1242
|
2076 Add = fn a => St.assert [a],
|
adamc@1242
|
2077 Save = St.stash,
|
adamc@1242
|
2078 Restore = St.reinstate,
|
adamc@1242
|
2079 Cont = AllCols (fn x =>
|
adamc@1242
|
2080 (St.assert [AReln (Eq, [r, x])];
|
adamc@1242
|
2081 evalExp (acc :: r :: env) b k))} q
|
adamc@1238
|
2082 end)
|
adam@1293
|
2083 | EDml (e, _) =>
|
adamc@1220
|
2084 (case parse dml e of
|
adamc@1220
|
2085 NONE => (print ("Warning: Information flow checker can't parse DML command at "
|
adamc@1220
|
2086 ^ ErrorMsg.spanToString loc ^ "\n");
|
adamc@1220
|
2087 default ())
|
adamc@1220
|
2088 | SOME d =>
|
adamc@1220
|
2089 case d of
|
adamc@1220
|
2090 Insert (tab, es) =>
|
adamc@1220
|
2091 let
|
adamc@1236
|
2092 val new = St.nextVar ()
|
adamc@1220
|
2093
|
adamc@1236
|
2094 val expIn = expIn (Var o St.nextVar) env
|
adamc@1236
|
2095 (fn _ => raise Fail "Iflow.evalExp: Bad field expression in INSERT [1]")
|
adamc@1220
|
2096
|
adamc@1236
|
2097 val es = map (fn (x, e) =>
|
adamc@1236
|
2098 case expIn e of
|
adamc@1236
|
2099 inl e => (x, e)
|
adamc@1236
|
2100 | inr _ => raise Fail "Iflow.evalExp: Bad field expression in INSERT [2]")
|
adamc@1236
|
2101 es
|
adamc@1220
|
2102
|
adamc@1236
|
2103 val saved = St.stash ()
|
adamc@1220
|
2104 in
|
adamc@1236
|
2105 St.assert [AReln (Sql (tab ^ "$New"), [Recd es])];
|
adamc@1236
|
2106 St.insert loc;
|
adamc@1236
|
2107 St.reinstate saved;
|
adamc@1251
|
2108 St.assert [AReln (Sql tab, [Recd es])];
|
adamc@1236
|
2109 k (Recd [])
|
adamc@1221
|
2110 end
|
adamc@1221
|
2111 | Delete (tab, e) =>
|
adamc@1221
|
2112 let
|
adamc@1236
|
2113 val old = St.nextVar ()
|
adamc@1236
|
2114
|
adamc@1236
|
2115 val expIn = expIn (Var o St.nextVar) env
|
adamc@1236
|
2116 (fn "T" => Var old
|
adamc@1236
|
2117 | _ => raise Fail "Iflow.evalExp: Bad field expression in DELETE")
|
adamc@1221
|
2118
|
adamc@1236
|
2119 val p = case expIn e of
|
adamc@1236
|
2120 inl e => raise Fail "Iflow.evalExp: DELETE with non-boolean"
|
adamc@1236
|
2121 | inr p => p
|
adamc@1236
|
2122
|
adamc@1236
|
2123 val saved = St.stash ()
|
adamc@1221
|
2124 in
|
adamc@1246
|
2125 St.assert [AReln (Sql (tab ^ "$Old"), [Var old]),
|
adamc@1246
|
2126 AReln (Sql (tab), [Var old])];
|
adamc@1236
|
2127 decomp {Save = St.stash,
|
adamc@1236
|
2128 Restore = St.reinstate,
|
adamc@1236
|
2129 Add = fn a => St.assert [a]} p
|
adamc@1236
|
2130 (fn () => (St.delete loc;
|
adamc@1236
|
2131 St.reinstate saved;
|
adamc@1236
|
2132 St.havocReln (Sql tab);
|
adamc@1236
|
2133 k (Recd []))
|
adamc@1236
|
2134 handle Cc.Contradiction => ())
|
adamc@1223
|
2135 end
|
adamc@1223
|
2136 | Update (tab, fs, e) =>
|
adamc@1223
|
2137 let
|
adamc@1236
|
2138 val new = St.nextVar ()
|
adamc@1236
|
2139 val old = St.nextVar ()
|
adamc@1223
|
2140
|
adamc@1236
|
2141 val expIn = expIn (Var o St.nextVar) env
|
adamc@1236
|
2142 (fn "T" => Var old
|
adamc@1236
|
2143 | _ => raise Fail "Iflow.evalExp: Bad field expression in UPDATE")
|
adamc@1223
|
2144
|
adamc@1236
|
2145 val fs = map
|
adamc@1236
|
2146 (fn (x, e) =>
|
adamc@1236
|
2147 (x, case expIn e of
|
adamc@1236
|
2148 inl e => e
|
adamc@1236
|
2149 | inr _ => raise Fail
|
adamc@1236
|
2150 ("Iflow.evalExp: Selecting "
|
adamc@1236
|
2151 ^ "boolean expression")))
|
adamc@1236
|
2152 fs
|
adamc@1223
|
2153
|
adamc@1226
|
2154 val fs' = case SM.find (!tabs, tab) of
|
adamc@1224
|
2155 NONE => raise Fail "Iflow.evalExp: Updating unknown table"
|
adamc@1226
|
2156 | SOME (fs', _) => fs'
|
adamc@1224
|
2157
|
adamc@1224
|
2158 val fs = foldl (fn (f, fs) =>
|
adamc@1224
|
2159 if List.exists (fn (f', _) => f' = f) fs then
|
adamc@1224
|
2160 fs
|
adamc@1224
|
2161 else
|
adamc@1224
|
2162 (f, Proj (Var old, f)) :: fs) fs fs'
|
adamc@1224
|
2163
|
adamc@1236
|
2164 val p = case expIn e of
|
adamc@1236
|
2165 inl e => raise Fail "Iflow.evalExp: UPDATE with non-boolean"
|
adamc@1236
|
2166 | inr p => p
|
adamc@1236
|
2167 val saved = St.stash ()
|
adamc@1223
|
2168 in
|
adamc@1236
|
2169 St.assert [AReln (Sql (tab ^ "$New"), [Recd fs]),
|
adamc@1246
|
2170 AReln (Sql (tab ^ "$Old"), [Var old]),
|
adamc@1246
|
2171 AReln (Sql tab, [Var old])];
|
adamc@1236
|
2172 decomp {Save = St.stash,
|
adamc@1236
|
2173 Restore = St.reinstate,
|
adamc@1236
|
2174 Add = fn a => St.assert [a]} p
|
adamc@1236
|
2175 (fn () => (St.update loc;
|
adamc@1236
|
2176 St.reinstate saved;
|
adamc@1236
|
2177 St.havocReln (Sql tab);
|
adamc@1236
|
2178 k (Recd []))
|
adamc@1236
|
2179 handle Cc.Contradiction => ())
|
adamc@1220
|
2180 end)
|
adamc@1220
|
2181
|
adamc@1229
|
2182 | ENextval (EPrim (Prim.String seq), _) =>
|
adamc@1229
|
2183 let
|
adamc@1236
|
2184 val nv = St.nextVar ()
|
adamc@1229
|
2185 in
|
adamc@1236
|
2186 St.assert [AReln (Sql (String.extract (seq, 3, NONE)), [Var nv])];
|
adamc@1236
|
2187 k (Var nv)
|
adamc@1229
|
2188 end
|
adamc@1200
|
2189 | ENextval _ => default ()
|
adamc@1200
|
2190 | ESetval _ => default ()
|
adamc@1200
|
2191
|
adamc@1238
|
2192 | EUnurlify ((EFfiApp ("Basis", "get_cookie", [(EPrim (Prim.String cname), _)]), _), _, _) =>
|
adamc@1217
|
2193 let
|
adamc@1238
|
2194 val e = Var (St.nextVar ())
|
adamc@1245
|
2195 val e' = Func (Other ("cookie/" ^ cname), [])
|
adamc@1217
|
2196 in
|
adamc@1245
|
2197 St.assert [AReln (Known, [e]), AReln (Eq, [e, e'])];
|
adamc@1238
|
2198 k e
|
adamc@1217
|
2199 end
|
adamc@1213
|
2200
|
adamc@1200
|
2201 | EUnurlify _ => default ()
|
adamc@1200
|
2202 | EJavaScript _ => default ()
|
adamc@1200
|
2203 | ESignalReturn _ => default ()
|
adamc@1200
|
2204 | ESignalBind _ => default ()
|
adamc@1200
|
2205 | ESignalSource _ => default ()
|
adamc@1200
|
2206 | EServerCall _ => default ()
|
adamc@1200
|
2207 | ERecv _ => default ()
|
adamc@1200
|
2208 | ESleep _ => default ()
|
adamc@1200
|
2209 | ESpawn _ => default ()
|
adamc@1200
|
2210 end
|
adamc@1200
|
2211
|
adamc@1251
|
2212 datatype var_source = Input of int | SubInput of int | Unknown
|
adamc@1251
|
2213
|
adamc@1200
|
2214 fun check file =
|
adamc@1200
|
2215 let
|
adamc@1251
|
2216 val () = (St.reset ();
|
adamc@1251
|
2217 rfuns := IM.empty)
|
adamc@1236
|
2218
|
adamc@1213
|
2219 val file = MonoReduce.reduce file
|
adamc@1213
|
2220 val file = MonoOpt.optimize file
|
adamc@1213
|
2221 val file = Fuse.fuse file
|
adamc@1213
|
2222 val file = MonoOpt.optimize file
|
adamc@1216
|
2223 val file = MonoShake.shake file
|
adamc@1213
|
2224 (*val () = Print.preface ("File", MonoPrint.p_file MonoEnv.empty file)*)
|
adamc@1213
|
2225
|
adamc@1207
|
2226 val exptd = foldl (fn ((d, _), exptd) =>
|
adamc@1207
|
2227 case d of
|
adamc@1207
|
2228 DExport (_, _, n, _, _, _) => IS.add (exptd, n)
|
adamc@1207
|
2229 | _ => exptd) IS.empty file
|
adamc@1207
|
2230
|
adamc@1249
|
2231 fun decl (d, loc) =
|
adamc@1200
|
2232 case d of
|
adamc@1226
|
2233 DTable (tab, fs, pk, _) =>
|
adamc@1226
|
2234 let
|
adamc@1226
|
2235 val ks =
|
adamc@1226
|
2236 case #1 pk of
|
adamc@1226
|
2237 EPrim (Prim.String s) =>
|
adamc@1226
|
2238 (case String.tokens (fn ch => ch = #"," orelse ch = #" ") s of
|
adamc@1226
|
2239 [] => []
|
adamc@1226
|
2240 | pk => [pk])
|
adamc@1226
|
2241 | _ => []
|
adamc@1226
|
2242 in
|
adamc@1226
|
2243 if size tab >= 3 then
|
adamc@1236
|
2244 tabs := SM.insert (!tabs, String.extract (tab, 3, NONE),
|
adamc@1236
|
2245 (map #1 fs,
|
adamc@1236
|
2246 map (map (fn s => str (Char.toUpper (String.sub (s, 3)))
|
adamc@1236
|
2247 ^ String.extract (s, 4, NONE))) ks))
|
adamc@1226
|
2248 else
|
adamc@1226
|
2249 raise Fail "Table name does not begin with uw_"
|
adamc@1226
|
2250 end
|
adamc@1238
|
2251 | DVal (x, n, _, e, _) =>
|
adamc@1200
|
2252 let
|
adamc@1238
|
2253 (*val () = print ("\n=== " ^ x ^ " ===\n\n");*)
|
adamc@1238
|
2254
|
adamc@1207
|
2255 val isExptd = IS.member (exptd, n)
|
adamc@1207
|
2256
|
adamc@1236
|
2257 val saved = St.stash ()
|
adamc@1236
|
2258
|
adamc@1236
|
2259 fun deAbs (e, env, ps) =
|
adamc@1200
|
2260 case #1 e of
|
adamc@1236
|
2261 EAbs (_, _, _, e) =>
|
adamc@1236
|
2262 let
|
adamc@1236
|
2263 val nv = Var (St.nextVar ())
|
adamc@1236
|
2264 in
|
adamc@1236
|
2265 deAbs (e, nv :: env,
|
adamc@1236
|
2266 if isExptd then
|
adamc@1236
|
2267 AReln (Known, [nv]) :: ps
|
adamc@1236
|
2268 else
|
adamc@1236
|
2269 ps)
|
adamc@1236
|
2270 end
|
adamc@1236
|
2271 | _ => (e, env, ps)
|
adamc@1200
|
2272
|
adamc@1236
|
2273 val (e, env, ps) = deAbs (e, [], [])
|
adamc@1200
|
2274 in
|
adamc@1236
|
2275 St.assert ps;
|
adamc@1236
|
2276 (evalExp env e (fn _ => ()) handle Cc.Contradiction => ());
|
adamc@1236
|
2277 St.reinstate saved
|
adamc@1200
|
2278 end
|
adamc@1202
|
2279
|
adamc@1251
|
2280 | DValRec [(x, n, _, e, _)] =>
|
adamc@1251
|
2281 let
|
adamc@1251
|
2282 val tables = ref SS.empty
|
adamc@1251
|
2283 val cookies = ref SS.empty
|
adamc@1251
|
2284
|
adamc@1251
|
2285 fun deAbs (e, env, modes) =
|
adamc@1251
|
2286 case #1 e of
|
adamc@1251
|
2287 EAbs (_, _, _, e) => deAbs (e, Input (length env) :: env, ref Fixed :: modes)
|
adamc@1251
|
2288 | _ => (e, env, rev modes)
|
adamc@1251
|
2289
|
adamc@1251
|
2290 val (e, env, modes) = deAbs (e, [], [])
|
adamc@1251
|
2291
|
adamc@1251
|
2292 fun doExp env (e as (_, loc)) =
|
adamc@1251
|
2293 case #1 e of
|
adamc@1251
|
2294 EPrim _ => e
|
adamc@1251
|
2295 | ERel _ => e
|
adamc@1251
|
2296 | ENamed _ => e
|
adamc@1251
|
2297 | ECon (_, _, NONE) => e
|
adamc@1251
|
2298 | ECon (dk, pc, SOME e) => (ECon (dk, pc, SOME (doExp env e)), loc)
|
adamc@1251
|
2299 | ENone _ => e
|
adamc@1251
|
2300 | ESome (t, e) => (ESome (t, doExp env e), loc)
|
adamc@1251
|
2301 | EFfi _ => e
|
adamc@1251
|
2302 | EFfiApp (m, f, es) =>
|
adamc@1251
|
2303 (case (m, f, es) of
|
adamc@1251
|
2304 ("Basis", "set_cookie", [_, (EPrim (Prim.String cname), _), _, _, _]) =>
|
adamc@1251
|
2305 cookies := SS.add (!cookies, cname)
|
adamc@1251
|
2306 | _ => ();
|
adamc@1251
|
2307 (EFfiApp (m, f, map (doExp env) es), loc))
|
adamc@1251
|
2308
|
adamc@1251
|
2309 | EApp (e1, e2) =>
|
adamc@1251
|
2310 let
|
adamc@1251
|
2311 fun default () = (EApp (doExp env e1, doExp env e2), loc)
|
adamc@1251
|
2312
|
adamc@1251
|
2313 fun explore (e, args) =
|
adamc@1251
|
2314 case #1 e of
|
adamc@1251
|
2315 EApp (e1, e2) => explore (e1, e2 :: args)
|
adamc@1251
|
2316 | ENamed n' =>
|
adamc@1251
|
2317 if n' = n then
|
adamc@1251
|
2318 let
|
adamc@1251
|
2319 fun doArgs (pos, args, modes) =
|
adamc@1251
|
2320 case (args, modes) of
|
adamc@1251
|
2321 ((e1, _) :: args, m1 :: modes) =>
|
adamc@1251
|
2322 (case e1 of
|
adamc@1251
|
2323 ERel n =>
|
adamc@1251
|
2324 (case List.nth (env, n) of
|
adamc@1251
|
2325 Input pos' =>
|
adamc@1251
|
2326 if pos' = pos then
|
adamc@1251
|
2327 ()
|
adamc@1251
|
2328 else
|
adamc@1251
|
2329 m1 := Arbitrary
|
adamc@1251
|
2330 | SubInput pos' =>
|
adamc@1251
|
2331 if pos' = pos then
|
adamc@1251
|
2332 if !m1 = Arbitrary then
|
adamc@1251
|
2333 ()
|
adamc@1251
|
2334 else
|
adamc@1251
|
2335 m1 := Decreasing
|
adamc@1251
|
2336 else
|
adamc@1251
|
2337 m1 := Arbitrary
|
adamc@1251
|
2338 | Unknown => m1 := Arbitrary)
|
adamc@1251
|
2339 | _ => m1 := Arbitrary;
|
adamc@1251
|
2340 doArgs (pos + 1, args, modes))
|
adamc@1251
|
2341 | (_ :: _, []) => ()
|
adamc@1251
|
2342 | ([], ms) => app (fn m => m := Arbitrary) ms
|
adamc@1251
|
2343 in
|
adamc@1251
|
2344 doArgs (0, args, modes);
|
adamc@1251
|
2345 (EFfi ("Basis", "?"), loc)
|
adamc@1251
|
2346 end
|
adamc@1251
|
2347 else
|
adamc@1251
|
2348 default ()
|
adamc@1251
|
2349 | _ => default ()
|
adamc@1251
|
2350 in
|
adamc@1251
|
2351 explore (e, [])
|
adamc@1251
|
2352 end
|
adamc@1251
|
2353 | EAbs (x, t1, t2, e) => (EAbs (x, t1, t2, doExp (Unknown :: env) e), loc)
|
adamc@1251
|
2354 | EUnop (uo, e1) => (EUnop (uo, doExp env e1), loc)
|
adam@1360
|
2355 | EBinop (bi, bo, e1, e2) => (EBinop (bi, bo, doExp env e1, doExp env e2), loc)
|
adamc@1251
|
2356 | ERecord xets => (ERecord (map (fn (x, e, t) => (x, doExp env e, t)) xets), loc)
|
adamc@1251
|
2357 | EField (e1, f) => (EField (doExp env e1, f), loc)
|
adamc@1251
|
2358 | ECase (e, pes, ts) =>
|
adamc@1251
|
2359 let
|
adamc@1251
|
2360 val source =
|
adamc@1251
|
2361 case #1 e of
|
adamc@1251
|
2362 ERel n =>
|
adamc@1251
|
2363 (case List.nth (env, n) of
|
adamc@1251
|
2364 Input n => SOME n
|
adamc@1251
|
2365 | SubInput n => SOME n
|
adamc@1251
|
2366 | Unknown => NONE)
|
adamc@1251
|
2367 | _ => NONE
|
adamc@1251
|
2368
|
adamc@1251
|
2369 fun doV v =
|
adamc@1251
|
2370 let
|
adamc@1251
|
2371 fun doPat (p, env) =
|
adamc@1251
|
2372 case #1 p of
|
adamc@1251
|
2373 PWild => env
|
adamc@1251
|
2374 | PVar _ => v :: env
|
adamc@1251
|
2375 | PPrim _ => env
|
adamc@1251
|
2376 | PCon (_, _, NONE) => env
|
adamc@1251
|
2377 | PCon (_, _, SOME p) => doPat (p, env)
|
adamc@1251
|
2378 | PRecord xpts => foldl (fn ((_, p, _), env) => doPat (p, env)) env xpts
|
adamc@1251
|
2379 | PNone _ => env
|
adamc@1251
|
2380 | PSome (_, p) => doPat (p, env)
|
adamc@1251
|
2381 in
|
adamc@1251
|
2382 (ECase (e, map (fn (p, e) => (p, doExp (doPat (p, env)) e)) pes, ts), loc)
|
adamc@1251
|
2383 end
|
adamc@1251
|
2384 in
|
adamc@1251
|
2385 case source of
|
adamc@1251
|
2386 NONE => doV Unknown
|
adamc@1251
|
2387 | SOME inp => doV (SubInput inp)
|
adamc@1251
|
2388 end
|
adamc@1251
|
2389 | EStrcat (e1, e2) => (EStrcat (doExp env e1, doExp env e2), loc)
|
adamc@1251
|
2390 | EError (e1, t) => (EError (doExp env e1, t), loc)
|
adamc@1251
|
2391 | EReturnBlob {blob = b, mimeType = m, t} =>
|
adamc@1251
|
2392 (EReturnBlob {blob = doExp env b, mimeType = doExp env m, t = t}, loc)
|
adamc@1251
|
2393 | ERedirect (e1, t) => (ERedirect (doExp env e1, t), loc)
|
adamc@1251
|
2394 | EWrite e1 => (EWrite (doExp env e1), loc)
|
adamc@1251
|
2395 | ESeq (e1, e2) => (ESeq (doExp env e1, doExp env e2), loc)
|
adamc@1251
|
2396 | ELet (x, t, e1, e2) => (ELet (x, t, doExp env e1, doExp (Unknown :: env) e2), loc)
|
adamc@1251
|
2397 | EClosure (n, es) => (EClosure (n, map (doExp env) es), loc)
|
adamc@1251
|
2398 | EQuery {exps, tables, state, query, body, initial} =>
|
adamc@1251
|
2399 (EQuery {exps = exps, tables = tables, state = state,
|
adamc@1251
|
2400 query = doExp env query,
|
adamc@1251
|
2401 body = doExp (Unknown :: Unknown :: env) body,
|
adamc@1251
|
2402 initial = doExp env initial}, loc)
|
adam@1293
|
2403 | EDml (e1, mode) =>
|
adamc@1251
|
2404 (case parse dml e1 of
|
adamc@1251
|
2405 NONE => ()
|
adamc@1251
|
2406 | SOME c =>
|
adamc@1251
|
2407 case c of
|
adamc@1251
|
2408 Insert _ => ()
|
adamc@1251
|
2409 | Delete (tab, _) =>
|
adamc@1251
|
2410 tables := SS.add (!tables, tab)
|
adamc@1251
|
2411 | Update (tab, _, _) =>
|
adamc@1251
|
2412 tables := SS.add (!tables, tab);
|
adam@1293
|
2413 (EDml (doExp env e1, mode), loc))
|
adamc@1251
|
2414 | ENextval e1 => (ENextval (doExp env e1), loc)
|
adamc@1251
|
2415 | ESetval (e1, e2) => (ESetval (doExp env e1, doExp env e2), loc)
|
adamc@1251
|
2416 | EUnurlify (e1, t, b) => (EUnurlify (doExp env e1, t, b), loc)
|
adamc@1251
|
2417 | EJavaScript (m, e) => (EJavaScript (m, doExp env e), loc)
|
adamc@1251
|
2418 | ESignalReturn _ => e
|
adamc@1251
|
2419 | ESignalBind _ => e
|
adamc@1251
|
2420 | ESignalSource _ => e
|
adamc@1251
|
2421 | EServerCall _ => e
|
adamc@1251
|
2422 | ERecv _ => e
|
adamc@1251
|
2423 | ESleep _ => e
|
adamc@1251
|
2424 | ESpawn _ => e
|
adamc@1251
|
2425
|
adamc@1251
|
2426 val e = doExp env e
|
adamc@1251
|
2427 in
|
adamc@1251
|
2428 rfuns := IM.insert (!rfuns, n, {tables = !tables, cookies = !cookies,
|
adamc@1251
|
2429 args = map (fn r => !r) modes, body = e})
|
adamc@1251
|
2430 end
|
adamc@1251
|
2431
|
adamc@1251
|
2432 | DValRec _ => ErrorMsg.errorAt loc "Iflow can't check mutually-recursive functions yet."
|
adamc@1249
|
2433
|
adamc@1220
|
2434 | DPolicy pol =>
|
adamc@1218
|
2435 let
|
adamc@1236
|
2436 val rvN = ref 0
|
adamc@1236
|
2437 fun rv () =
|
adamc@1236
|
2438 let
|
adamc@1236
|
2439 val n = !rvN
|
adamc@1236
|
2440 in
|
adamc@1236
|
2441 rvN := n + 1;
|
adamc@1236
|
2442 Lvar n
|
adamc@1236
|
2443 end
|
adamc@1236
|
2444
|
adamc@1236
|
2445 val atoms = ref ([] : atom list)
|
adamc@1236
|
2446 fun doQ k = doQuery {Env = [],
|
adamc@1236
|
2447 NextVar = rv,
|
adamc@1236
|
2448 Add = fn a => atoms := a :: !atoms,
|
adamc@1236
|
2449 Save = fn () => !atoms,
|
adamc@1236
|
2450 Restore = fn ls => atoms := ls,
|
adamc@1238
|
2451 Cont = SomeCol (fn r => k (rev (!atoms), r))}
|
adamc@1238
|
2452
|
adamc@1247
|
2453 fun untab (tab, nams) = List.filter (fn AReln (Sql tab', [Lvar lv]) =>
|
adamc@1247
|
2454 tab' <> tab
|
adamc@1247
|
2455 orelse List.all (fn Lvar lv' => lv' <> lv
|
adamc@1247
|
2456 | _ => false) nams
|
adamc@1247
|
2457 | _ => true)
|
adamc@1218
|
2458 in
|
adamc@1220
|
2459 case pol of
|
adamc@1220
|
2460 PolClient e =>
|
adamc@1238
|
2461 doQ (fn (ats, {Outs = es, ...}) => St.allowSend (ats, es)) e
|
adamc@1220
|
2462 | PolInsert e =>
|
adamc@1238
|
2463 doQ (fn (ats, {New = SOME (tab, new), ...}) =>
|
adamc@1247
|
2464 St.allowInsert (AReln (Sql (tab ^ "$New"), [new]) :: untab (tab, [new]) ats)
|
adamc@1238
|
2465 | _ => raise Fail "Iflow: No New in mayInsert policy") e
|
adamc@1221
|
2466 | PolDelete e =>
|
adamc@1238
|
2467 doQ (fn (ats, {Old = SOME (tab, old), ...}) =>
|
adamc@1247
|
2468 St.allowDelete (AReln (Sql (tab ^ "$Old"), [old]) :: untab (tab, [old]) ats)
|
adamc@1238
|
2469 | _ => raise Fail "Iflow: No Old in mayDelete policy") e
|
adamc@1223
|
2470 | PolUpdate e =>
|
adamc@1238
|
2471 doQ (fn (ats, {New = SOME (tab, new), Old = SOME (_, old), ...}) =>
|
adamc@1238
|
2472 St.allowUpdate (AReln (Sql (tab ^ "$Old"), [old])
|
adamc@1238
|
2473 :: AReln (Sql (tab ^ "$New"), [new])
|
adamc@1247
|
2474 :: untab (tab, [new, old]) ats)
|
adamc@1238
|
2475 | _ => raise Fail "Iflow: No New or Old in mayUpdate policy") e
|
adamc@1229
|
2476 | PolSequence e =>
|
adamc@1229
|
2477 (case #1 e of
|
adamc@1229
|
2478 EPrim (Prim.String seq) =>
|
adamc@1229
|
2479 let
|
adamc@1236
|
2480 val p = AReln (Sql (String.extract (seq, 3, NONE)), [Lvar 0])
|
adamc@1229
|
2481 val outs = [Lvar 0]
|
adamc@1229
|
2482 in
|
adamc@1236
|
2483 St.allowSend ([p], outs)
|
adamc@1229
|
2484 end
|
adamc@1236
|
2485 | _ => ())
|
adamc@1218
|
2486 end
|
adamc@1214
|
2487
|
adamc@1236
|
2488 | _ => ()
|
adamc@1200
|
2489 in
|
adamc@1236
|
2490 app decl file
|
adamc@1200
|
2491 end
|
adamc@1200
|
2492
|
adamc@1213
|
2493 val check = fn file =>
|
adamc@1213
|
2494 let
|
adamc@1213
|
2495 val oldInline = Settings.getMonoInline ()
|
adamc@1213
|
2496 in
|
adamc@1213
|
2497 (Settings.setMonoInline (case Int.maxInt of
|
adamc@1213
|
2498 NONE => 1000000
|
adamc@1213
|
2499 | SOME n => n);
|
adamc@1213
|
2500 check file;
|
adamc@1213
|
2501 Settings.setMonoInline oldInline)
|
adamc@1213
|
2502 handle ex => (Settings.setMonoInline oldInline;
|
adamc@1213
|
2503 raise ex)
|
adamc@1213
|
2504 end
|
adamc@1213
|
2505
|
adamc@1200
|
2506 end
|