Mercurial > urweb

comparison src/iflow.sml @ 1203:a75c66dd2aeb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Relax checking of table implications
author Adam Chlipala <adamc@hcoop.net>
date Sun, 04 Apr 2010 16:44:34 -0400
parents 509a6d7b60fb
children 7af5e2af64f4
comparison
equal deleted inserted replaced
1202:509a6d7b60fb 1203:a75c66dd2aeb
184 decomp 184 decomp
185 end 185 end
186 186
187 val unif = ref (IM.empty : exp IM.map) 187 val unif = ref (IM.empty : exp IM.map)
188 188
189 fun reset () = unif := IM.empty
190 fun save () = !unif
191 fun restore x = unif := x
192
189 fun lvarIn lv = 193 fun lvarIn lv =
190 let 194 let
191 fun lvi e = 195 fun lvi e =
192 case e of 196 case e of
193 Const _ => false 197 Const _ => false
240 | (Finish, Finish) => true 244 | (Finish, Finish) => true
241 | _ => false 245 | _ => false
242 246
243 fun eq (e1, e2) = 247 fun eq (e1, e2) =
244 let 248 let
245 val saved = !unif 249 val saved = save ()
246 in 250 in
247 if eq' (simplify e1, simplify e2) then 251 if eq' (simplify e1, simplify e2) then
248 true 252 true
249 else 253 else
250 (unif := saved; 254 (restore saved;
251 false) 255 false)
252 end 256 end
253 257
254 exception Imply of prop * prop 258 exception Imply of prop * prop
255 259
258 (Sql r1', Sql r2') => 262 (Sql r1', Sql r2') =>
259 r1' = r2' andalso 263 r1' = r2' andalso
260 (case (es1, es2) of 264 (case (es1, es2) of
261 ([Recd xes1], [Recd xes2]) => 265 ([Recd xes1], [Recd xes2]) =>
262 let 266 let
263 val saved = !unif 267 val saved = save ()
264 in 268 in
265 (*print ("Go: " ^ r1' ^ "\n");*)
266 (*raise Imply (Reln (r1, es1), Reln (r2, es2));*)
267 if List.all (fn (f, e2) => 269 if List.all (fn (f, e2) =>
268 List.exists (fn (f', e1) => 270 case ListUtil.search (fn (f', e1) => if f' = f then SOME e1 else NONE) xes1 of
269 f' = f andalso eq (e1, e2)) xes1) xes2 then 271 NONE => true
272 | SOME e1 => eq (e1, e2)) xes2 then
270 true 273 true
271 else 274 else
272 (unif := saved; 275 (restore saved;
273 false) 276 false)
274 end 277 end
275 | _ => false) 278 | _ => false)
276 | (Eq, Eq) => 279 | (Eq, Eq) =>
277 (case (es1, es2) of 280 (case (es1, es2) of
278 ([x1, y1], [x2, y2]) => 281 ([x1, y1], [x2, y2]) =>
279 let 282 let
280 val saved = !unif 283 val saved = save ()
281 in 284 in
282 if eq (x1, x2) andalso eq (y1, y2) then 285 if eq (x1, x2) andalso eq (y1, y2) then
283 true 286 true
284 else 287 else
285 (unif := saved; 288 (restore saved;
286 (*raise Imply (Reln (Eq, es1), Reln (Eq, es2));*) 289 (*raise Imply (Reln (Eq, es1), Reln (Eq, es2));*)
287 eq (x1, y2) andalso eq (y1, x2)) 290 eq (x1, y2) andalso eq (y1, x2))
288 end 291 end
289 | _ => false) 292 | _ => false)
290 | _ => false 293 | _ => false
291 294
292 fun imply (p1, p2) = 295 fun imply (p1, p2) =
293 (unif := IM.empty; 296 (reset ();
294 (*raise (Imply (p1, p2));*) 297 (*raise (Imply (p1, p2));*)
295 decomp true (fn (e1, e2) => e1 andalso e2 ()) p1 298 decomp true (fn (e1, e2) => e1 andalso e2 ()) p1
296 (fn hyps => 299 (fn hyps =>
297 decomp false (fn (e1, e2) => e1 orelse e2 ()) p2 300 decomp false (fn (e1, e2) => e1 orelse e2 ()) p2
298 (fn goals => 301 (fn goals =>
305 fun hps hyps = 308 fun hps hyps =
306 case hyps of 309 case hyps of
307 [] => onFail () 310 [] => onFail ()
308 | h :: hyps => 311 | h :: hyps =>
309 let 312 let
310 val saved = !unif 313 val saved = save ()
311 in 314 in
312 if rimp (h, g) then 315 if rimp (h, g) then
313 let 316 let
314 val changed = IM.numItems (!unif) = IM.numItems saved 317 val changed = IM.numItems (!unif) <> IM.numItems saved
315 in 318 in
316 gls goals (fn () => (unif := saved; 319 gls goals (fn () => (restore saved;
317 changed andalso hps hyps)) 320 changed andalso hps hyps))
318 end 321 end
319 else 322 else
320 hps hyps 323 hps hyps
321 end 324 end
658 661
659 | DPolicy (PolQuery e) => (vals, queryProp 0 (SOME (Var 0)) e :: pols) 662 | DPolicy (PolQuery e) => (vals, queryProp 0 (SOME (Var 0)) e :: pols)
660 663
661 | _ => (vals, pols) 664 | _ => (vals, pols)
662 665
663 val () = unif := IM.empty 666 val () = reset ()
664 667
665 val (vals, pols) = foldl decl ([], []) file 668 val (vals, pols) = foldl decl ([], []) file
666 in 669 in
667 app (fn (name, _, _, sent) => 670 app (fn (name, _, _, sent) =>
668 app (fn (loc, e, p) => 671 app (fn (loc, e, p) =>