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@1202
|
32 structure IM = IntBinaryMap
|
adamc@1202
|
33
|
adamc@1200
|
34 structure SS = BinarySetFn(struct
|
adamc@1200
|
35 type ord_key = string
|
adamc@1200
|
36 val compare = String.compare
|
adamc@1200
|
37 end)
|
adamc@1200
|
38
|
adamc@1200
|
39 val writers = ["htmlifyInt_w",
|
adamc@1200
|
40 "htmlifyFloat_w",
|
adamc@1200
|
41 "htmlifyString_w",
|
adamc@1200
|
42 "htmlifyBool_w",
|
adamc@1200
|
43 "htmlifyTime_w",
|
adamc@1200
|
44 "attrifyInt_w",
|
adamc@1200
|
45 "attrifyFloat_w",
|
adamc@1200
|
46 "attrifyString_w",
|
adamc@1200
|
47 "attrifyChar_w",
|
adamc@1200
|
48 "urlifyInt_w",
|
adamc@1200
|
49 "urlifyFloat_w",
|
adamc@1200
|
50 "urlifyString_w",
|
adamc@1200
|
51 "urlifyBool_w"]
|
adamc@1200
|
52
|
adamc@1200
|
53 val writers = SS.addList (SS.empty, writers)
|
adamc@1200
|
54
|
adamc@1200
|
55 type lvar = int
|
adamc@1200
|
56
|
adamc@1200
|
57 datatype exp =
|
adamc@1200
|
58 Const of Prim.t
|
adamc@1200
|
59 | Var of int
|
adamc@1200
|
60 | Lvar of lvar
|
adamc@1200
|
61 | Func of string * exp list
|
adamc@1200
|
62 | Recd of (string * exp) list
|
adamc@1200
|
63 | Proj of exp * string
|
adamc@1200
|
64 | Finish
|
adamc@1200
|
65
|
adamc@1200
|
66 datatype reln =
|
adamc@1200
|
67 Sql of string
|
adamc@1200
|
68 | Eq
|
adamc@1200
|
69
|
adamc@1200
|
70 datatype prop =
|
adamc@1200
|
71 True
|
adamc@1200
|
72 | False
|
adamc@1200
|
73 | Unknown
|
adamc@1200
|
74 | And of prop * prop
|
adamc@1200
|
75 | Or of prop * prop
|
adamc@1200
|
76 | Reln of reln * exp list
|
adamc@1200
|
77 | Select of int * lvar * lvar * prop * exp
|
adamc@1200
|
78
|
adamc@1200
|
79 local
|
adamc@1202
|
80 val count = ref 1
|
adamc@1200
|
81 in
|
adamc@1200
|
82 fun newLvar () =
|
adamc@1200
|
83 let
|
adamc@1200
|
84 val n = !count
|
adamc@1200
|
85 in
|
adamc@1200
|
86 count := n + 1;
|
adamc@1200
|
87 n
|
adamc@1200
|
88 end
|
adamc@1200
|
89 end
|
adamc@1200
|
90
|
adamc@1200
|
91 fun subExp (v, lv) =
|
adamc@1200
|
92 let
|
adamc@1200
|
93 fun sub e =
|
adamc@1200
|
94 case e of
|
adamc@1200
|
95 Const _ => e
|
adamc@1200
|
96 | Var v' => if v' = v then Lvar lv else e
|
adamc@1200
|
97 | Lvar _ => e
|
adamc@1200
|
98 | Func (f, es) => Func (f, map sub es)
|
adamc@1200
|
99 | Recd xes => Recd (map (fn (x, e) => (x, sub e)) xes)
|
adamc@1200
|
100 | Proj (e, s) => Proj (sub e, s)
|
adamc@1200
|
101 | Finish => Finish
|
adamc@1200
|
102 in
|
adamc@1200
|
103 sub
|
adamc@1200
|
104 end
|
adamc@1200
|
105
|
adamc@1200
|
106 fun subProp (v, lv) =
|
adamc@1200
|
107 let
|
adamc@1200
|
108 fun sub p =
|
adamc@1200
|
109 case p of
|
adamc@1200
|
110 True => p
|
adamc@1200
|
111 | False => p
|
adamc@1200
|
112 | Unknown => p
|
adamc@1200
|
113 | And (p1, p2) => And (sub p1, sub p2)
|
adamc@1200
|
114 | Or (p1, p2) => Or (sub p1, sub p2)
|
adamc@1200
|
115 | Reln (r, es) => Reln (r, map (subExp (v, lv)) es)
|
adamc@1200
|
116 | Select (v1, lv1, lv2, p, e) => Select (v1, lv1, lv2, sub p, subExp (v, lv) e)
|
adamc@1200
|
117 in
|
adamc@1200
|
118 sub
|
adamc@1200
|
119 end
|
adamc@1200
|
120
|
adamc@1200
|
121 fun isKnown e =
|
adamc@1200
|
122 case e of
|
adamc@1200
|
123 Const _ => true
|
adamc@1200
|
124 | Func (_, es) => List.all isKnown es
|
adamc@1200
|
125 | Recd xes => List.all (isKnown o #2) xes
|
adamc@1200
|
126 | Proj (e, _) => isKnown e
|
adamc@1200
|
127 | _ => false
|
adamc@1200
|
128
|
adamc@1200
|
129 fun isFinish e =
|
adamc@1200
|
130 case e of
|
adamc@1200
|
131 Finish => true
|
adamc@1200
|
132 | _ => false
|
adamc@1200
|
133
|
adamc@1200
|
134 fun simplify e =
|
adamc@1200
|
135 case e of
|
adamc@1200
|
136 Const _ => e
|
adamc@1200
|
137 | Var _ => e
|
adamc@1200
|
138 | Lvar _ => e
|
adamc@1200
|
139 | Func (f, es) =>
|
adamc@1200
|
140 let
|
adamc@1200
|
141 val es = map simplify es
|
adamc@1200
|
142 in
|
adamc@1200
|
143 if List.exists isFinish es then
|
adamc@1200
|
144 Finish
|
adamc@1200
|
145 else
|
adamc@1200
|
146 Func (f, es)
|
adamc@1200
|
147 end
|
adamc@1200
|
148 | Recd xes =>
|
adamc@1200
|
149 let
|
adamc@1200
|
150 val xes = map (fn (x, e) => (x, simplify e)) xes
|
adamc@1200
|
151 in
|
adamc@1200
|
152 if List.exists (isFinish o #2) xes then
|
adamc@1200
|
153 Finish
|
adamc@1200
|
154 else
|
adamc@1200
|
155 Recd xes
|
adamc@1200
|
156 end
|
adamc@1200
|
157 | Proj (e, s) =>
|
adamc@1200
|
158 (case simplify e of
|
adamc@1200
|
159 Recd xes =>
|
adamc@1200
|
160 getOpt (ListUtil.search (fn (x, e') => if x = s then SOME e' else NONE) xes, Recd xes)
|
adamc@1200
|
161 | e' =>
|
adamc@1200
|
162 if isFinish e' then
|
adamc@1200
|
163 Finish
|
adamc@1200
|
164 else
|
adamc@1200
|
165 Proj (e', s))
|
adamc@1200
|
166 | Finish => Finish
|
adamc@1200
|
167
|
adamc@1202
|
168 fun decomp fals or =
|
adamc@1200
|
169 let
|
adamc@1200
|
170 fun decomp p k =
|
adamc@1200
|
171 case p of
|
adamc@1200
|
172 True => k []
|
adamc@1202
|
173 | False => fals
|
adamc@1200
|
174 | Unknown => k []
|
adamc@1200
|
175 | And (p1, p2) =>
|
adamc@1200
|
176 decomp p1 (fn ps1 =>
|
adamc@1200
|
177 decomp p2 (fn ps2 =>
|
adamc@1200
|
178 k (ps1 @ ps2)))
|
adamc@1200
|
179 | Or (p1, p2) =>
|
adamc@1200
|
180 or (decomp p1 k, fn () => decomp p2 k)
|
adamc@1200
|
181 | Reln x => k [x]
|
adamc@1200
|
182 | Select _ => k []
|
adamc@1200
|
183 in
|
adamc@1200
|
184 decomp
|
adamc@1200
|
185 end
|
adamc@1200
|
186
|
adamc@1202
|
187 val unif = ref (IM.empty : exp IM.map)
|
adamc@1200
|
188
|
adamc@1203
|
189 fun reset () = unif := IM.empty
|
adamc@1203
|
190 fun save () = !unif
|
adamc@1203
|
191 fun restore x = unif := x
|
adamc@1203
|
192
|
adamc@1202
|
193 fun lvarIn lv =
|
adamc@1202
|
194 let
|
adamc@1202
|
195 fun lvi e =
|
adamc@1202
|
196 case e of
|
adamc@1202
|
197 Const _ => false
|
adamc@1202
|
198 | Var _ => false
|
adamc@1202
|
199 | Lvar lv' => lv' = lv
|
adamc@1202
|
200 | Func (_, es) => List.exists lvi es
|
adamc@1202
|
201 | Recd xes => List.exists (lvi o #2) xes
|
adamc@1202
|
202 | Proj (e, _) => lvi e
|
adamc@1202
|
203 | Finish => false
|
adamc@1202
|
204 in
|
adamc@1202
|
205 lvi
|
adamc@1202
|
206 end
|
adamc@1202
|
207
|
adamc@1202
|
208 fun eq' (e1, e2) =
|
adamc@1202
|
209 case (e1, e2) of
|
adamc@1202
|
210 (Const p1, Const p2) => Prim.equal (p1, p2)
|
adamc@1202
|
211 | (Var n1, Var n2) => n1 = n2
|
adamc@1202
|
212
|
adamc@1202
|
213 | (Lvar n1, _) =>
|
adamc@1202
|
214 (case IM.find (!unif, n1) of
|
adamc@1202
|
215 SOME e1 => eq' (e1, e2)
|
adamc@1202
|
216 | NONE =>
|
adamc@1202
|
217 case e2 of
|
adamc@1202
|
218 Lvar n2 =>
|
adamc@1202
|
219 (case IM.find (!unif, n2) of
|
adamc@1202
|
220 SOME e2 => eq' (e1, e2)
|
adamc@1202
|
221 | NONE => n1 = n2
|
adamc@1202
|
222 orelse (unif := IM.insert (!unif, n1, e2);
|
adamc@1202
|
223 true))
|
adamc@1202
|
224 | _ =>
|
adamc@1202
|
225 if lvarIn n1 e2 then
|
adamc@1202
|
226 false
|
adamc@1202
|
227 else
|
adamc@1202
|
228 (unif := IM.insert (!unif, n1, e2);
|
adamc@1202
|
229 true))
|
adamc@1202
|
230
|
adamc@1202
|
231 | (_, Lvar n2) =>
|
adamc@1202
|
232 (case IM.find (!unif, n2) of
|
adamc@1202
|
233 SOME e2 => eq' (e1, e2)
|
adamc@1202
|
234 | NONE =>
|
adamc@1202
|
235 if lvarIn n2 e1 then
|
adamc@1202
|
236 false
|
adamc@1202
|
237 else
|
adamc@1202
|
238 (unif := IM.insert (!unif, n2, e1);
|
adamc@1202
|
239 true))
|
adamc@1202
|
240
|
adamc@1202
|
241 | (Func (f1, es1), Func (f2, es2)) => f1 = f2 andalso ListPair.allEq eq' (es1, es2)
|
adamc@1202
|
242 | (Recd xes1, Recd xes2) => ListPair.allEq (fn ((x1, e1), (x2, e2)) => x1 = x2 andalso eq' (e1, e2)) (xes1, xes2)
|
adamc@1202
|
243 | (Proj (e1, s1), Proj (e2, s2)) => eq' (e1, e2) andalso s1 = s2
|
adamc@1202
|
244 | (Finish, Finish) => true
|
adamc@1202
|
245 | _ => false
|
adamc@1202
|
246
|
adamc@1202
|
247 fun eq (e1, e2) =
|
adamc@1202
|
248 let
|
adamc@1203
|
249 val saved = save ()
|
adamc@1202
|
250 in
|
adamc@1202
|
251 if eq' (simplify e1, simplify e2) then
|
adamc@1202
|
252 true
|
adamc@1202
|
253 else
|
adamc@1203
|
254 (restore saved;
|
adamc@1202
|
255 false)
|
adamc@1202
|
256 end
|
adamc@1202
|
257
|
adamc@1202
|
258 exception Imply of prop * prop
|
adamc@1202
|
259
|
adamc@1202
|
260 fun rimp ((r1, es1), (r2, es2)) =
|
adamc@1202
|
261 case (r1, r2) of
|
adamc@1202
|
262 (Sql r1', Sql r2') =>
|
adamc@1202
|
263 r1' = r2' andalso
|
adamc@1202
|
264 (case (es1, es2) of
|
adamc@1202
|
265 ([Recd xes1], [Recd xes2]) =>
|
adamc@1202
|
266 let
|
adamc@1203
|
267 val saved = save ()
|
adamc@1202
|
268 in
|
adamc@1202
|
269 if List.all (fn (f, e2) =>
|
adamc@1203
|
270 case ListUtil.search (fn (f', e1) => if f' = f then SOME e1 else NONE) xes1 of
|
adamc@1203
|
271 NONE => true
|
adamc@1203
|
272 | SOME e1 => eq (e1, e2)) xes2 then
|
adamc@1202
|
273 true
|
adamc@1202
|
274 else
|
adamc@1203
|
275 (restore saved;
|
adamc@1202
|
276 false)
|
adamc@1202
|
277 end
|
adamc@1202
|
278 | _ => false)
|
adamc@1202
|
279 | (Eq, Eq) =>
|
adamc@1202
|
280 (case (es1, es2) of
|
adamc@1202
|
281 ([x1, y1], [x2, y2]) =>
|
adamc@1202
|
282 let
|
adamc@1203
|
283 val saved = save ()
|
adamc@1202
|
284 in
|
adamc@1202
|
285 if eq (x1, x2) andalso eq (y1, y2) then
|
adamc@1202
|
286 true
|
adamc@1202
|
287 else
|
adamc@1203
|
288 (restore saved;
|
adamc@1202
|
289 (*raise Imply (Reln (Eq, es1), Reln (Eq, es2));*)
|
adamc@1202
|
290 eq (x1, y2) andalso eq (y1, x2))
|
adamc@1202
|
291 end
|
adamc@1202
|
292 | _ => false)
|
adamc@1202
|
293 | _ => false
|
adamc@1202
|
294
|
adamc@1202
|
295 fun imply (p1, p2) =
|
adamc@1203
|
296 (reset ();
|
adamc@1202
|
297 (*raise (Imply (p1, p2));*)
|
adamc@1202
|
298 decomp true (fn (e1, e2) => e1 andalso e2 ()) p1
|
adamc@1202
|
299 (fn hyps =>
|
adamc@1202
|
300 decomp false (fn (e1, e2) => e1 orelse e2 ()) p2
|
adamc@1202
|
301 (fn goals =>
|
adamc@1202
|
302 let
|
adamc@1202
|
303 fun gls goals onFail =
|
adamc@1202
|
304 case goals of
|
adamc@1202
|
305 [] => true
|
adamc@1202
|
306 | g :: goals =>
|
adamc@1202
|
307 let
|
adamc@1202
|
308 fun hps hyps =
|
adamc@1202
|
309 case hyps of
|
adamc@1202
|
310 [] => onFail ()
|
adamc@1202
|
311 | h :: hyps =>
|
adamc@1202
|
312 let
|
adamc@1203
|
313 val saved = save ()
|
adamc@1202
|
314 in
|
adamc@1202
|
315 if rimp (h, g) then
|
adamc@1202
|
316 let
|
adamc@1203
|
317 val changed = IM.numItems (!unif) <> IM.numItems saved
|
adamc@1202
|
318 in
|
adamc@1203
|
319 gls goals (fn () => (restore saved;
|
adamc@1202
|
320 changed andalso hps hyps))
|
adamc@1202
|
321 end
|
adamc@1202
|
322 else
|
adamc@1202
|
323 hps hyps
|
adamc@1202
|
324 end
|
adamc@1202
|
325 in
|
adamc@1202
|
326 hps hyps
|
adamc@1202
|
327 end
|
adamc@1202
|
328 in
|
adamc@1202
|
329 gls goals (fn () => false)
|
adamc@1202
|
330 end)))
|
adamc@1202
|
331
|
adamc@1200
|
332
|
adamc@1200
|
333 fun patCon pc =
|
adamc@1200
|
334 case pc of
|
adamc@1200
|
335 PConVar n => "C" ^ Int.toString n
|
adamc@1200
|
336 | PConFfi {mod = m, datatyp = d, con = c, ...} => m ^ "." ^ d ^ "." ^ c
|
adamc@1200
|
337
|
adamc@1202
|
338
|
adamc@1200
|
339
|
adamc@1200
|
340 datatype chunk =
|
adamc@1200
|
341 String of string
|
adamc@1200
|
342 | Exp of Mono.exp
|
adamc@1200
|
343
|
adamc@1200
|
344 fun chunkify e =
|
adamc@1200
|
345 case #1 e of
|
adamc@1200
|
346 EPrim (Prim.String s) => [String s]
|
adamc@1200
|
347 | EStrcat (e1, e2) => chunkify e1 @ chunkify e2
|
adamc@1200
|
348 | _ => [Exp e]
|
adamc@1200
|
349
|
adamc@1201
|
350 type 'a parser = chunk list -> ('a * chunk list) option
|
adamc@1201
|
351
|
adamc@1201
|
352 fun always v chs = SOME (v, chs)
|
adamc@1201
|
353
|
adamc@1202
|
354 fun parse p s =
|
adamc@1202
|
355 case p (chunkify s) of
|
adamc@1201
|
356 SOME (v, []) => SOME v
|
adamc@1201
|
357 | _ => NONE
|
adamc@1201
|
358
|
adamc@1201
|
359 fun const s chs =
|
adamc@1201
|
360 case chs of
|
adamc@1201
|
361 String s' :: chs => if String.isPrefix s s' then
|
adamc@1201
|
362 SOME ((), if size s = size s' then
|
adamc@1201
|
363 chs
|
adamc@1201
|
364 else
|
adamc@1201
|
365 String (String.extract (s', size s, NONE)) :: chs)
|
adamc@1201
|
366 else
|
adamc@1201
|
367 NONE
|
adamc@1201
|
368 | _ => NONE
|
adamc@1201
|
369
|
adamc@1201
|
370 fun follow p1 p2 chs =
|
adamc@1201
|
371 case p1 chs of
|
adamc@1201
|
372 NONE => NONE
|
adamc@1201
|
373 | SOME (v1, chs) =>
|
adamc@1201
|
374 case p2 chs of
|
adamc@1201
|
375 NONE => NONE
|
adamc@1201
|
376 | SOME (v2, chs) => SOME ((v1, v2), chs)
|
adamc@1201
|
377
|
adamc@1201
|
378 fun wrap p f chs =
|
adamc@1201
|
379 case p chs of
|
adamc@1201
|
380 NONE => NONE
|
adamc@1201
|
381 | SOME (v, chs) => SOME (f v, chs)
|
adamc@1201
|
382
|
adamc@1201
|
383 fun alt p1 p2 chs =
|
adamc@1201
|
384 case p1 chs of
|
adamc@1201
|
385 NONE => p2 chs
|
adamc@1201
|
386 | v => v
|
adamc@1201
|
387
|
adamc@1204
|
388 fun opt p chs =
|
adamc@1204
|
389 case p chs of
|
adamc@1204
|
390 NONE => SOME (NONE, chs)
|
adamc@1204
|
391 | SOME (v, chs) => SOME (SOME v, chs)
|
adamc@1204
|
392
|
adamc@1201
|
393 fun skip cp chs =
|
adamc@1201
|
394 case chs of
|
adamc@1201
|
395 String "" :: chs => skip cp chs
|
adamc@1201
|
396 | String s :: chs' => if cp (String.sub (s, 0)) then
|
adamc@1201
|
397 skip cp (String (String.extract (s, 1, NONE)) :: chs')
|
adamc@1201
|
398 else
|
adamc@1201
|
399 SOME ((), chs)
|
adamc@1201
|
400 | _ => SOME ((), chs)
|
adamc@1201
|
401
|
adamc@1201
|
402 fun keep cp chs =
|
adamc@1201
|
403 case chs of
|
adamc@1201
|
404 String "" :: chs => keep cp chs
|
adamc@1201
|
405 | String s :: chs' =>
|
adamc@1201
|
406 let
|
adamc@1201
|
407 val (befor, after) = Substring.splitl cp (Substring.full s)
|
adamc@1201
|
408 in
|
adamc@1201
|
409 if Substring.isEmpty befor then
|
adamc@1201
|
410 NONE
|
adamc@1201
|
411 else
|
adamc@1201
|
412 SOME (Substring.string befor,
|
adamc@1201
|
413 if Substring.isEmpty after then
|
adamc@1201
|
414 chs'
|
adamc@1201
|
415 else
|
adamc@1201
|
416 String (Substring.string after) :: chs')
|
adamc@1201
|
417 end
|
adamc@1201
|
418 | _ => NONE
|
adamc@1201
|
419
|
adamc@1204
|
420 fun ws p = wrap (follow (skip (fn ch => ch = #" "))
|
adamc@1204
|
421 (follow p (skip (fn ch => ch = #" ")))) (#1 o #2)
|
adamc@1204
|
422
|
adamc@1206
|
423 val debug = ref false
|
adamc@1206
|
424
|
adamc@1204
|
425 fun log name p chs =
|
adamc@1206
|
426 (if !debug then
|
adamc@1206
|
427 case chs of
|
adamc@1206
|
428 String s :: [] => print (name ^ ": " ^ s ^ "\n")
|
adamc@1206
|
429 | _ => print (name ^ ": blocked!\n")
|
adamc@1206
|
430 else
|
adamc@1206
|
431 ();
|
adamc@1204
|
432 p chs)
|
adamc@1201
|
433
|
adamc@1201
|
434 fun list p chs =
|
adamc@1201
|
435 (alt (wrap (follow p (follow (ws (const ",")) (list p)))
|
adamc@1201
|
436 (fn (v, ((), ls)) => v :: ls))
|
adamc@1201
|
437 (alt (wrap (ws p) (fn v => [v]))
|
adamc@1201
|
438 (always []))) chs
|
adamc@1201
|
439
|
adamc@1201
|
440 val ident = keep (fn ch => Char.isAlphaNum ch orelse ch = #"_")
|
adamc@1201
|
441
|
adamc@1201
|
442 val t_ident = wrap ident (fn s => if String.isPrefix "T_" s then
|
adamc@1201
|
443 String.extract (s, 2, NONE)
|
adamc@1201
|
444 else
|
adamc@1201
|
445 raise Fail "Iflow: Bad table variable")
|
adamc@1201
|
446 val uw_ident = wrap ident (fn s => if String.isPrefix "uw_" s then
|
adamc@1201
|
447 String.extract (s, 3, NONE)
|
adamc@1201
|
448 else
|
adamc@1201
|
449 raise Fail "Iflow: Bad uw_* variable")
|
adamc@1201
|
450
|
adamc@1201
|
451 val sitem = wrap (follow t_ident
|
adamc@1201
|
452 (follow (const ".")
|
adamc@1201
|
453 uw_ident))
|
adamc@1201
|
454 (fn (t, ((), f)) => (t, f))
|
adamc@1201
|
455
|
adamc@1206
|
456 datatype Rel =
|
adamc@1206
|
457 Exps of exp * exp -> prop
|
adamc@1206
|
458 | Props of prop * prop -> prop
|
adamc@1206
|
459
|
adamc@1204
|
460 datatype sqexp =
|
adamc@1206
|
461 SqConst of Prim.t
|
adamc@1206
|
462 | Field of string * string
|
adamc@1206
|
463 | Binop of Rel * sqexp * sqexp
|
adamc@1204
|
464
|
adamc@1206
|
465 val sqbrel = alt (wrap (const "=") (fn () => Exps (fn (e1, e2) => Reln (Eq, [e1, e2]))))
|
adamc@1206
|
466 (alt (wrap (const "AND") (fn () => Props And))
|
adamc@1206
|
467 (wrap (const "OR") (fn () => Props Or)))
|
adamc@1204
|
468
|
adamc@1204
|
469 datatype ('a, 'b) sum = inl of 'a | inr of 'b
|
adamc@1204
|
470
|
adamc@1206
|
471 fun int chs =
|
adamc@1206
|
472 case chs of
|
adamc@1206
|
473 String s :: chs' =>
|
adamc@1206
|
474 let
|
adamc@1206
|
475 val (befor, after) = Substring.splitl Char.isDigit (Substring.full s)
|
adamc@1206
|
476 in
|
adamc@1206
|
477 if Substring.isEmpty befor then
|
adamc@1206
|
478 NONE
|
adamc@1206
|
479 else case Int64.fromString (Substring.string befor) of
|
adamc@1206
|
480 NONE => NONE
|
adamc@1206
|
481 | SOME n => SOME (n, if Substring.isEmpty after then
|
adamc@1206
|
482 chs'
|
adamc@1206
|
483 else
|
adamc@1206
|
484 String (Substring.string after) :: chs')
|
adamc@1206
|
485 end
|
adamc@1206
|
486 | _ => NONE
|
adamc@1206
|
487
|
adamc@1206
|
488 val prim = wrap (follow (wrap int Prim.Int) (opt (const "::int8"))) #1
|
adamc@1206
|
489
|
adamc@1204
|
490 fun sqexp chs =
|
adamc@1206
|
491 log "sqexp"
|
adamc@1206
|
492 (alt
|
adamc@1206
|
493 (wrap prim SqConst)
|
adamc@1206
|
494 (alt
|
adamc@1206
|
495 (wrap sitem Field)
|
adamc@1206
|
496 (wrap
|
adamc@1206
|
497 (follow (ws (const "("))
|
adamc@1206
|
498 (follow (wrap
|
adamc@1206
|
499 (follow sqexp
|
adamc@1206
|
500 (alt
|
adamc@1206
|
501 (wrap
|
adamc@1206
|
502 (follow (ws sqbrel)
|
adamc@1206
|
503 (ws sqexp))
|
adamc@1206
|
504 inl)
|
adamc@1206
|
505 (always (inr ()))))
|
adamc@1206
|
506 (fn (e1, sm) =>
|
adamc@1206
|
507 case sm of
|
adamc@1206
|
508 inl (bo, e2) => Binop (bo, e1, e2)
|
adamc@1206
|
509 | inr () => e1))
|
adamc@1206
|
510 (const ")")))
|
adamc@1206
|
511 (fn ((), (e, ())) => e))))
|
adamc@1206
|
512 chs
|
adamc@1206
|
513
|
adamc@1201
|
514 val select = wrap (follow (const "SELECT ") (list sitem))
|
adamc@1201
|
515 (fn ((), ls) => ls)
|
adamc@1201
|
516
|
adamc@1201
|
517 val fitem = wrap (follow uw_ident
|
adamc@1201
|
518 (follow (const " AS ")
|
adamc@1201
|
519 t_ident))
|
adamc@1201
|
520 (fn (t, ((), f)) => (t, f))
|
adamc@1201
|
521
|
adamc@1201
|
522 val from = wrap (follow (const "FROM ") (list fitem))
|
adamc@1201
|
523 (fn ((), ls) => ls)
|
adamc@1201
|
524
|
adamc@1204
|
525 val wher = wrap (follow (ws (const "WHERE ")) sqexp)
|
adamc@1204
|
526 (fn ((), ls) => ls)
|
adamc@1204
|
527
|
adamc@1204
|
528 val query = wrap (follow (follow select from) (opt wher))
|
adamc@1204
|
529 (fn ((fs, ts), wher) => {Select = fs, From = ts, Where = wher})
|
adamc@1201
|
530
|
adamc@1202
|
531 fun queryProp rv oe e =
|
adamc@1202
|
532 case parse query e of
|
adamc@1204
|
533 NONE => (print "Crap\n"; Unknown)
|
adamc@1201
|
534 | SOME r =>
|
adamc@1202
|
535 let
|
adamc@1202
|
536 val p =
|
adamc@1202
|
537 foldl (fn ((t, v), p) =>
|
adamc@1202
|
538 And (p,
|
adamc@1202
|
539 Reln (Sql t,
|
adamc@1202
|
540 [Recd (foldl (fn ((v', f), fs) =>
|
adamc@1202
|
541 if v' = v then
|
adamc@1202
|
542 (f, Proj (Proj (Lvar rv, v), f)) :: fs
|
adamc@1202
|
543 else
|
adamc@1202
|
544 fs) [] (#Select r))])))
|
adamc@1202
|
545 True (#From r)
|
adamc@1205
|
546
|
adamc@1205
|
547 fun expIn e =
|
adamc@1205
|
548 case e of
|
adamc@1206
|
549 SqConst p => inl (Const p)
|
adamc@1206
|
550 | Field (v, f) => inl (Proj (Proj (Lvar rv, v), f))
|
adamc@1205
|
551 | Binop (bo, e1, e2) =>
|
adamc@1206
|
552 inr (case (bo, expIn e1, expIn e2) of
|
adamc@1206
|
553 (Exps f, inl e1, inl e2) => f (e1, e2)
|
adamc@1206
|
554 | (Props f, inr p1, inr p2) => f (p1, p2)
|
adamc@1206
|
555 | _ => Unknown)
|
adamc@1205
|
556
|
adamc@1205
|
557 val p = case #Where r of
|
adamc@1205
|
558 NONE => p
|
adamc@1205
|
559 | SOME e =>
|
adamc@1205
|
560 case expIn e of
|
adamc@1205
|
561 inr p' => And (p, p')
|
adamc@1205
|
562 | _ => p
|
adamc@1202
|
563 in
|
adamc@1202
|
564 case oe of
|
adamc@1202
|
565 NONE => p
|
adamc@1202
|
566 | SOME oe =>
|
adamc@1205
|
567 And (p, foldl (fn ((v, f), p) =>
|
adamc@1205
|
568 Or (p,
|
adamc@1205
|
569 Reln (Eq, [oe, Proj (Proj (Lvar rv, v), f)])))
|
adamc@1205
|
570 False (#Select r))
|
adamc@1202
|
571 end
|
adamc@1200
|
572
|
adamc@1202
|
573 fun evalExp env (e as (_, loc), st as (nv, p, sent)) =
|
adamc@1200
|
574 let
|
adamc@1200
|
575 fun default () =
|
adamc@1200
|
576 (Var nv, (nv+1, p, sent))
|
adamc@1200
|
577
|
adamc@1200
|
578 fun addSent (p, e, sent) =
|
adamc@1200
|
579 if isKnown e then
|
adamc@1200
|
580 sent
|
adamc@1200
|
581 else
|
adamc@1202
|
582 (loc, e, p) :: sent
|
adamc@1200
|
583 in
|
adamc@1200
|
584 case #1 e of
|
adamc@1200
|
585 EPrim p => (Const p, st)
|
adamc@1200
|
586 | ERel n => (List.nth (env, n), st)
|
adamc@1200
|
587 | ENamed _ => default ()
|
adamc@1200
|
588 | ECon (_, pc, NONE) => (Func (patCon pc, []), st)
|
adamc@1200
|
589 | ECon (_, pc, SOME e) =>
|
adamc@1200
|
590 let
|
adamc@1200
|
591 val (e, st) = evalExp env (e, st)
|
adamc@1200
|
592 in
|
adamc@1200
|
593 (Func (patCon pc, [e]), st)
|
adamc@1200
|
594 end
|
adamc@1200
|
595 | ENone _ => (Func ("None", []), st)
|
adamc@1200
|
596 | ESome (_, e) =>
|
adamc@1200
|
597 let
|
adamc@1200
|
598 val (e, st) = evalExp env (e, st)
|
adamc@1200
|
599 in
|
adamc@1200
|
600 (Func ("Some", [e]), st)
|
adamc@1200
|
601 end
|
adamc@1200
|
602 | EFfi _ => default ()
|
adamc@1200
|
603 | EFfiApp (m, s, es) =>
|
adamc@1200
|
604 if m = "Basis" andalso SS.member (writers, s) then
|
adamc@1200
|
605 let
|
adamc@1200
|
606 val (es, st) = ListUtil.foldlMap (evalExp env) st es
|
adamc@1200
|
607 in
|
adamc@1200
|
608 (Func ("unit", []), (#1 st, p, foldl (fn (e, sent) => addSent (#2 st, e, sent)) sent es))
|
adamc@1200
|
609 end
|
adamc@1200
|
610 else if Settings.isEffectful (m, s) andalso not (Settings.isBenignEffectful (m, s)) then
|
adamc@1200
|
611 default ()
|
adamc@1200
|
612 else
|
adamc@1200
|
613 let
|
adamc@1200
|
614 val (es, st) = ListUtil.foldlMap (evalExp env) st es
|
adamc@1200
|
615 in
|
adamc@1200
|
616 (Func (m ^ "." ^ s, es), st)
|
adamc@1200
|
617 end
|
adamc@1200
|
618 | EApp _ => default ()
|
adamc@1200
|
619 | EAbs _ => default ()
|
adamc@1200
|
620 | EUnop (s, e1) =>
|
adamc@1200
|
621 let
|
adamc@1200
|
622 val (e1, st) = evalExp env (e1, st)
|
adamc@1200
|
623 in
|
adamc@1200
|
624 (Func (s, [e1]), st)
|
adamc@1200
|
625 end
|
adamc@1200
|
626 | EBinop (s, e1, e2) =>
|
adamc@1200
|
627 let
|
adamc@1200
|
628 val (e1, st) = evalExp env (e1, st)
|
adamc@1200
|
629 val (e2, st) = evalExp env (e2, st)
|
adamc@1200
|
630 in
|
adamc@1200
|
631 (Func (s, [e1, e2]), st)
|
adamc@1200
|
632 end
|
adamc@1200
|
633 | ERecord xets =>
|
adamc@1200
|
634 let
|
adamc@1200
|
635 val (xes, st) = ListUtil.foldlMap (fn ((x, e, _), st) =>
|
adamc@1200
|
636 let
|
adamc@1200
|
637 val (e, st) = evalExp env (e, st)
|
adamc@1200
|
638 in
|
adamc@1200
|
639 ((x, e), st)
|
adamc@1200
|
640 end) st xets
|
adamc@1200
|
641 in
|
adamc@1200
|
642 (Recd xes, st)
|
adamc@1200
|
643 end
|
adamc@1200
|
644 | EField (e, s) =>
|
adamc@1200
|
645 let
|
adamc@1200
|
646 val (e, st) = evalExp env (e, st)
|
adamc@1200
|
647 in
|
adamc@1200
|
648 (Proj (e, s), st)
|
adamc@1200
|
649 end
|
adamc@1200
|
650 | ECase _ => default ()
|
adamc@1200
|
651 | EStrcat (e1, e2) =>
|
adamc@1200
|
652 let
|
adamc@1200
|
653 val (e1, st) = evalExp env (e1, st)
|
adamc@1200
|
654 val (e2, st) = evalExp env (e2, st)
|
adamc@1200
|
655 in
|
adamc@1200
|
656 (Func ("cat", [e1, e2]), st)
|
adamc@1200
|
657 end
|
adamc@1200
|
658 | EError _ => (Finish, st)
|
adamc@1200
|
659 | EReturnBlob {blob = b, mimeType = m, ...} =>
|
adamc@1200
|
660 let
|
adamc@1200
|
661 val (b, st) = evalExp env (b, st)
|
adamc@1200
|
662 val (m, st) = evalExp env (m, st)
|
adamc@1200
|
663 in
|
adamc@1200
|
664 (Finish, (#1 st, p, addSent (#2 st, b, addSent (#2 st, m, sent))))
|
adamc@1200
|
665 end
|
adamc@1200
|
666 | ERedirect (e, _) =>
|
adamc@1200
|
667 let
|
adamc@1200
|
668 val (e, st) = evalExp env (e, st)
|
adamc@1200
|
669 in
|
adamc@1200
|
670 (Finish, (#1 st, p, addSent (#2 st, e, sent)))
|
adamc@1200
|
671 end
|
adamc@1200
|
672 | EWrite e =>
|
adamc@1200
|
673 let
|
adamc@1200
|
674 val (e, st) = evalExp env (e, st)
|
adamc@1200
|
675 in
|
adamc@1200
|
676 (Func ("unit", []), (#1 st, p, addSent (#2 st, e, sent)))
|
adamc@1200
|
677 end
|
adamc@1200
|
678 | ESeq (e1, e2) =>
|
adamc@1200
|
679 let
|
adamc@1200
|
680 val (_, st) = evalExp env (e1, st)
|
adamc@1200
|
681 in
|
adamc@1200
|
682 evalExp env (e2, st)
|
adamc@1200
|
683 end
|
adamc@1200
|
684 | ELet (_, _, e1, e2) =>
|
adamc@1200
|
685 let
|
adamc@1200
|
686 val (e1, st) = evalExp env (e1, st)
|
adamc@1200
|
687 in
|
adamc@1200
|
688 evalExp (e1 :: env) (e2, st)
|
adamc@1200
|
689 end
|
adamc@1200
|
690 | EClosure (n, es) =>
|
adamc@1200
|
691 let
|
adamc@1200
|
692 val (es, st) = ListUtil.foldlMap (evalExp env) st es
|
adamc@1200
|
693 in
|
adamc@1200
|
694 (Func ("Cl" ^ Int.toString n, es), st)
|
adamc@1200
|
695 end
|
adamc@1200
|
696
|
adamc@1200
|
697 | EQuery {query = q, body = b, initial = i, ...} =>
|
adamc@1200
|
698 let
|
adamc@1200
|
699 val (_, st) = evalExp env (q, st)
|
adamc@1200
|
700 val (i, st) = evalExp env (i, st)
|
adamc@1200
|
701
|
adamc@1200
|
702 val r = #1 st
|
adamc@1200
|
703 val acc = #1 st + 1
|
adamc@1200
|
704 val st' = (#1 st + 2, #2 st, #3 st)
|
adamc@1200
|
705
|
adamc@1200
|
706 val (b, st') = evalExp (Var acc :: Var r :: env) (b, st')
|
adamc@1200
|
707
|
adamc@1200
|
708 val r' = newLvar ()
|
adamc@1200
|
709 val acc' = newLvar ()
|
adamc@1202
|
710 val qp = queryProp r' NONE q
|
adamc@1200
|
711
|
adamc@1200
|
712 val doSubExp = subExp (r, r') o subExp (acc, acc')
|
adamc@1200
|
713 val doSubProp = subProp (r, r') o subProp (acc, acc')
|
adamc@1200
|
714
|
adamc@1200
|
715 val p = doSubProp (#2 st')
|
adamc@1200
|
716 val p = And (p, qp)
|
adamc@1200
|
717 val p = Select (r, r', acc', p, doSubExp b)
|
adamc@1200
|
718 in
|
adamc@1202
|
719 (Var r, (#1 st + 1, And (#2 st, p), map (fn (loc, e, p) => (loc,
|
adamc@1202
|
720 doSubExp e,
|
adamc@1202
|
721 And (qp, doSubProp p))) (#3 st')))
|
adamc@1200
|
722 end
|
adamc@1200
|
723 | EDml _ => default ()
|
adamc@1200
|
724 | ENextval _ => default ()
|
adamc@1200
|
725 | ESetval _ => default ()
|
adamc@1200
|
726
|
adamc@1200
|
727 | EUnurlify _ => default ()
|
adamc@1200
|
728 | EJavaScript _ => default ()
|
adamc@1200
|
729 | ESignalReturn _ => default ()
|
adamc@1200
|
730 | ESignalBind _ => default ()
|
adamc@1200
|
731 | ESignalSource _ => default ()
|
adamc@1200
|
732 | EServerCall _ => default ()
|
adamc@1200
|
733 | ERecv _ => default ()
|
adamc@1200
|
734 | ESleep _ => default ()
|
adamc@1200
|
735 | ESpawn _ => default ()
|
adamc@1200
|
736 end
|
adamc@1200
|
737
|
adamc@1200
|
738 fun check file =
|
adamc@1200
|
739 let
|
adamc@1202
|
740 fun decl ((d, _), (vals, pols)) =
|
adamc@1200
|
741 case d of
|
adamc@1200
|
742 DVal (x, _, _, e, _) =>
|
adamc@1200
|
743 let
|
adamc@1200
|
744 fun deAbs (e, env, nv) =
|
adamc@1200
|
745 case #1 e of
|
adamc@1200
|
746 EAbs (_, _, _, e) => deAbs (e, Var nv :: env, nv + 1)
|
adamc@1200
|
747 | _ => (e, env, nv)
|
adamc@1200
|
748
|
adamc@1202
|
749 val (e, env, nv) = deAbs (e, [], 1)
|
adamc@1200
|
750
|
adamc@1200
|
751 val (e, (_, p, sent)) = evalExp env (e, (nv, True, []))
|
adamc@1200
|
752 in
|
adamc@1202
|
753 ((x, e, p, sent) :: vals, pols)
|
adamc@1200
|
754 end
|
adamc@1202
|
755
|
adamc@1202
|
756 | DPolicy (PolQuery e) => (vals, queryProp 0 (SOME (Var 0)) e :: pols)
|
adamc@1202
|
757
|
adamc@1202
|
758 | _ => (vals, pols)
|
adamc@1202
|
759
|
adamc@1203
|
760 val () = reset ()
|
adamc@1202
|
761
|
adamc@1202
|
762 val (vals, pols) = foldl decl ([], []) file
|
adamc@1200
|
763 in
|
adamc@1202
|
764 app (fn (name, _, _, sent) =>
|
adamc@1202
|
765 app (fn (loc, e, p) =>
|
adamc@1202
|
766 let
|
adamc@1202
|
767 val p = And (p, Reln (Eq, [Var 0, e]))
|
adamc@1202
|
768 in
|
adamc@1202
|
769 if List.exists (fn pol => imply (p, pol)) pols then
|
adamc@1202
|
770 ()
|
adamc@1202
|
771 else
|
adamc@1202
|
772 ErrorMsg.errorAt loc "The information flow policy may be violated here."
|
adamc@1202
|
773 end) sent) vals
|
adamc@1200
|
774 end
|
adamc@1200
|
775
|
adamc@1200
|
776 end
|