Mercurial > urweb

comparison src/iflow.sml @ 1244:1eedc9086e6c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Use key information in more places, and catch cases where one key completion depends on another having happened already
author Adam Chlipala <adamc@hcoop.net>
date Sun, 18 Apr 2010 13:00:36 -0400
parents e754dc92c47c
children 5c2555dfce8f
comparison
equal deleted inserted replaced
1243:e754dc92c47c 1244:1eedc9086e6c
246 val builtFrom : database * {UseKnown : bool, Base : exp list, Derived : exp} -> bool 246 val builtFrom : database * {UseKnown : bool, Base : exp list, Derived : exp} -> bool
247 247
248 val p_repOf : database -> exp Print.printer 248 val p_repOf : database -> exp Print.printer
249 end = struct 249 end = struct
250 250
251 local
252 val count = ref 0
253 in
254 fun nodeId () =
255 let
256 val n = !count
257 in
258 count := n + 1;
259 n
260 end
261 end
262
251 exception Contradiction 263 exception Contradiction
252 exception Undetermined 264 exception Undetermined
253 265
254 structure CM = BinaryMapFn(struct 266 structure CM = BinaryMapFn(struct
255 type ord_key = Prim.t 267 type ord_key = Prim.t
256 val compare = Prim.compare 268 val compare = Prim.compare
257 end) 269 end)
258 270
259 datatype node = Node of {Rep : node ref option ref, 271 datatype node = Node of {Id : int,
272 Rep : node ref option ref,
260 Cons : node ref SM.map ref, 273 Cons : node ref SM.map ref,
261 Variety : variety, 274 Variety : variety,
262 Known : bool ref} 275 Known : bool ref}
263 276
264 and variety = 277 and variety =
298 311
299 fun p_rep n = 312 fun p_rep n =
300 case !(#Rep (unNode n)) of 313 case !(#Rep (unNode n)) of
301 SOME n => p_rep n 314 SOME n => p_rep n
302 | NONE => 315 | NONE =>
303 box [(*string (Int.toString (Unsafe.cast n) ^ ":"), 316 box [string (Int.toString (#Id (unNode n)) ^ ":"),
304 space,*) 317 space,
305 case #Variety (unNode n) of 318 case #Variety (unNode n) of
306 Nothing => string "?" 319 Nothing => string "?"
307 | Dt0 s => string ("Dt0(" ^ s ^ ")") 320 | Dt0 s => string ("Dt0(" ^ s ^ ")")
308 | Dt1 (s, n) => box[string ("Dt1(" ^ s ^ ","), 321 | Dt1 (s, n) => box[string ("Dt1(" ^ s ^ ","),
309 space, 322 space,
370 case e of 383 case e of
371 Const p => (case CM.find (!(#Consts db), p) of 384 Const p => (case CM.find (!(#Consts db), p) of
372 SOME r => repOf r 385 SOME r => repOf r
373 | NONE => 386 | NONE =>
374 let 387 let
375 val r = ref (Node {Rep = ref NONE, 388 val r = ref (Node {Id = nodeId (),
389 Rep = ref NONE,
376 Cons = ref SM.empty, 390 Cons = ref SM.empty,
377 Variety = Prim p, 391 Variety = Prim p,
378 Known = ref true}) 392 Known = ref true})
379 in 393 in
380 #Consts db := CM.insert (!(#Consts db), p, r); 394 #Consts db := CM.insert (!(#Consts db), p, r);
382 end) 396 end)
383 | Var n => (case IM.find (!(#Vars db), n) of 397 | Var n => (case IM.find (!(#Vars db), n) of
384 SOME r => repOf r 398 SOME r => repOf r
385 | NONE => 399 | NONE =>
386 let 400 let
387 val r = ref (Node {Rep = ref NONE, 401 val r = ref (Node {Id = nodeId (),
402 Rep = ref NONE,
388 Cons = ref SM.empty, 403 Cons = ref SM.empty,
389 Variety = Nothing, 404 Variety = Nothing,
390 Known = ref false}) 405 Known = ref false})
391 in 406 in
392 #Vars db := IM.insert (!(#Vars db), n, r); 407 #Vars db := IM.insert (!(#Vars db), n, r);
395 | Lvar _ => raise Undetermined 410 | Lvar _ => raise Undetermined
396 | Func (DtCon0 f, []) => (case SM.find (!(#Con0s db), f) of 411 | Func (DtCon0 f, []) => (case SM.find (!(#Con0s db), f) of
397 SOME r => repOf r 412 SOME r => repOf r
398 | NONE => 413 | NONE =>
399 let 414 let
400 val r = ref (Node {Rep = ref NONE, 415 val r = ref (Node {Id = nodeId (),
416 Rep = ref NONE,
401 Cons = ref SM.empty, 417 Cons = ref SM.empty,
402 Variety = Dt0 f, 418 Variety = Dt0 f,
403 Known = ref true}) 419 Known = ref true})
404 in 420 in
405 #Con0s db := SM.insert (!(#Con0s db), f, r); 421 #Con0s db := SM.insert (!(#Con0s db), f, r);
412 in 428 in
413 case SM.find (!(#Cons (unNode r)), f) of 429 case SM.find (!(#Cons (unNode r)), f) of
414 SOME r => repOf r 430 SOME r => repOf r
415 | NONE => 431 | NONE =>
416 let 432 let
417 val r' = ref (Node {Rep = ref NONE, 433 val r' = ref (Node {Id = nodeId (),
434 Rep = ref NONE,
418 Cons = ref SM.empty, 435 Cons = ref SM.empty,
419 Variety = Dt1 (f, r), 436 Variety = Dt1 (f, r),
420 Known = ref (!(#Known (unNode r)))}) 437 Known = ref (!(#Known (unNode r)))})
421 in 438 in
422 #Cons (unNode r) := SM.insert (!(#Cons (unNode r)), f, r'); 439 #Cons (unNode r) := SM.insert (!(#Cons (unNode r)), f, r');
434 else 451 else
435 raise Contradiction 452 raise Contradiction
436 | Nothing => 453 | Nothing =>
437 let 454 let
438 val cons = ref SM.empty 455 val cons = ref SM.empty
439 val r' = ref (Node {Rep = ref NONE, 456 val r' = ref (Node {Id = nodeId (),
457 Rep = ref NONE,
440 Cons = cons, 458 Cons = cons,
441 Variety = Nothing, 459 Variety = Nothing,
442 Known = ref (!(#Known (unNode r)))}) 460 Known = ref (!(#Known (unNode r)))})
443 461
444 val r'' = ref (Node {Rep = ref NONE, 462 val r'' = ref (Node {Id = nodeId (),
463 Rep = ref NONE,
445 Cons = #Cons (unNode r), 464 Cons = #Cons (unNode r),
446 Variety = Dt1 (f, r'), 465 Variety = Dt1 (f, r'),
447 Known = #Known (unNode r)}) 466 Known = #Known (unNode r)})
448 in 467 in
449 cons := SM.insert (!cons, f, r''); 468 cons := SM.insert (!cons, f, r'');
458 val rs = map rep es 477 val rs = map rep es
459 in 478 in
460 case List.find (fn (x : string * representative list, _) => x = (f, rs)) (!(#Funcs db)) of 479 case List.find (fn (x : string * representative list, _) => x = (f, rs)) (!(#Funcs db)) of
461 NONE => 480 NONE =>
462 let 481 let
463 val r = ref (Node {Rep = ref NONE, 482 val r = ref (Node {Id = nodeId (),
483 Rep = ref NONE,
464 Cons = ref SM.empty, 484 Cons = ref SM.empty,
465 Variety = Nothing, 485 Variety = Nothing,
466 Known = ref false}) 486 Known = ref false})
467 in 487 in
468 #Funcs db := ((f, rs), r) :: (!(#Funcs db)); 488 #Funcs db := ((f, rs), r) :: (!(#Funcs db));
485 SOME (_, r) => repOf r 505 SOME (_, r) => repOf r
486 | NONE => 506 | NONE =>
487 let 507 let
488 val xes = foldl SM.insert' SM.empty xes 508 val xes = foldl SM.insert' SM.empty xes
489 509
490 val r' = ref (Node {Rep = ref NONE, 510 val r' = ref (Node {Id = nodeId (),
511 Rep = ref NONE,
491 Cons = ref SM.empty, 512 Cons = ref SM.empty,
492 Variety = Recrd (ref xes, true), 513 Variety = Recrd (ref xes, true),
493 Known = ref false}) 514 Known = ref false})
494 in 515 in
495 #Records db := (xes, r') :: (!(#Records db)); 516 #Records db := (xes, r') :: (!(#Records db));
503 case #Variety (unNode r) of 524 case #Variety (unNode r) of
504 Recrd (xes, _) => 525 Recrd (xes, _) =>
505 (case SM.find (!xes, f) of 526 (case SM.find (!xes, f) of
506 SOME r => repOf r 527 SOME r => repOf r
507 | NONE => let 528 | NONE => let
508 val r = ref (Node {Rep = ref NONE, 529 val r = ref (Node {Id = nodeId (),
530 Rep = ref NONE,
509 Cons = ref SM.empty, 531 Cons = ref SM.empty,
510 Variety = Nothing, 532 Variety = Nothing,
511 Known = ref (!(#Known (unNode r)))}) 533 Known = ref (!(#Known (unNode r)))})
512 in 534 in
513 xes := SM.insert (!xes, f, r); 535 xes := SM.insert (!xes, f, r);
514 r 536 r
515 end) 537 end)
516 | Nothing => 538 | Nothing =>
517 let 539 let
518 val r' = ref (Node {Rep = ref NONE, 540 val r' = ref (Node {Id = nodeId (),
541 Rep = ref NONE,
519 Cons = ref SM.empty, 542 Cons = ref SM.empty,
520 Variety = Nothing, 543 Variety = Nothing,
521 Known = ref (!(#Known (unNode r)))}) 544 Known = ref (!(#Known (unNode r)))})
522 545
523 val r'' = ref (Node {Rep = ref NONE, 546 val r'' = ref (Node {Id = nodeId (),
547 Rep = ref NONE,
524 Cons = #Cons (unNode r), 548 Cons = #Cons (unNode r),
525 Variety = Recrd (ref (SM.insert (SM.empty, f, r')), false), 549 Variety = Recrd (ref (SM.insert (SM.empty, f, r')), false),
526 Known = #Known (unNode r)}) 550 Known = #Known (unNode r)})
527 in 551 in
528 #Rep (unNode r) := SOME r''; 552 #Rep (unNode r) := SOME r'';
633 | Nothing => 657 | Nothing =>
634 (case SM.find (!(#Con0s db), f) of 658 (case SM.find (!(#Con0s db), f) of
635 SOME r' => markEq (r, r') 659 SOME r' => markEq (r, r')
636 | NONE => 660 | NONE =>
637 let 661 let
638 val r' = ref (Node {Rep = ref NONE, 662 val r' = ref (Node {Id = nodeId (),
663 Rep = ref NONE,
639 Cons = ref SM.empty, 664 Cons = ref SM.empty,
640 Variety = Dt0 f, 665 Variety = Dt0 f,
641 Known = ref false}) 666 Known = ref false})
642 in 667 in
643 #Rep (unNode r) := SOME r'; 668 #Rep (unNode r) := SOME r';
654 () 679 ()
655 else 680 else
656 raise Contradiction 681 raise Contradiction
657 | Nothing => 682 | Nothing =>
658 let 683 let
659 val r'' = ref (Node {Rep = ref NONE, 684 val r'' = ref (Node {Id = nodeId (),
685 Rep = ref NONE,
660 Cons = ref SM.empty, 686 Cons = ref SM.empty,
661 Variety = Nothing, 687 Variety = Nothing,
662 Known = ref (!(#Known (unNode r)))}) 688 Known = ref (!(#Known (unNode r)))})
663 689
664 val r' = ref (Node {Rep = ref NONE, 690 val r' = ref (Node {Id = nodeId (),
691 Rep = ref NONE,
665 Cons = ref SM.empty, 692 Cons = ref SM.empty,
666 Variety = Dt1 (f, r''), 693 Variety = Dt1 (f, r''),
667 Known = #Known (unNode r)}) 694 Known = #Known (unNode r)})
668 in 695 in
669 #Rep (unNode r) := SOME r' 696 #Rep (unNode r) := SOME r'
741 end 768 end
742 769
743 end 770 end
744 771
745 val tabs = ref (SM.empty : (string list * string list list) SM.map) 772 val tabs = ref (SM.empty : (string list * string list list) SM.map)
746
747 fun ccOf hyps =
748 let
749 val cc = Cc.database ()
750 val () = app (fn a => Cc.assert (cc, a)) hyps
751
752 (* Take advantage of table key information *)
753 fun findKeys hyps =
754 case hyps of
755 [] => ()
756 | AReln (Sql tab, [r1]) :: hyps =>
757 (case SM.find (!tabs, tab) of
758 NONE => findKeys hyps
759 | SOME (_, []) => findKeys hyps
760 | SOME (_, ks) =>
761 let
762 fun finder hyps =
763 case hyps of
764 [] => ()
765 | AReln (Sql tab', [r2]) :: hyps =>
766 (if tab' = tab andalso
767 List.exists (List.all (fn f =>
768 let
769 val r =
770 Cc.check (cc,
771 AReln (Eq, [Proj (r1, f),
772 Proj (r2, f)]))
773 in
774 (*Print.prefaces "Fs"
775 [("tab",
776 Print.PD.string tab),
777 ("r1",
778 p_exp (Proj (r1, f))),
779 ("r2",
780 p_exp (Proj (r2, f))),
781 ("r",
782 Print.PD.string
783 (Bool.toString r))];*)
784 r
785 end)) ks then
786 ((*Print.prefaces "Key match" [("tab", Print.PD.string tab),
787 ("r1", p_exp r1),
788 ("r2", p_exp r2),
789 ("rp1", Cc.p_repOf cc r1),
790 ("rp2", Cc.p_repOf cc r2)];*)
791 Cc.assert (cc, AReln (Eq, [r1, r2])))
792 else
793 ();
794 finder hyps)
795 | _ :: hyps => finder hyps
796 in
797 finder hyps;
798 findKeys hyps
799 end)
800 | _ :: hyps => findKeys hyps
801 in
802 findKeys hyps;
803 cc
804 end
805 773
806 fun patCon pc = 774 fun patCon pc =
807 case pc of 775 case pc of
808 PConVar n => "C" ^ Int.toString n 776 PConVar n => "C" ^ Int.toString n
809 | PConFfi {mod = m, datatyp = d, con = c, ...} => m ^ "." ^ d ^ "." ^ c 777 | PConFfi {mod = m, datatyp = d, con = c, ...} => m ^ "." ^ d ^ "." ^ c
1210 val debug : unit -> unit 1178 val debug : unit -> unit
1211 end = struct 1179 end = struct
1212 1180
1213 val hnames = ref 1 1181 val hnames = ref 1
1214 1182
1215 type hyps = int * atom list 1183 type hyps = int * atom list * bool ref
1216 1184
1217 val db = Cc.database () 1185 val db = Cc.database ()
1218 val path = ref ([] : (hyps * check) option ref list) 1186 val path = ref ([] : ((int * atom list) * check) option ref list)
1219 val hyps = ref (0, [] : atom list) 1187 val hyps = ref (0, [] : atom list, ref false)
1220 val nvar = ref 0 1188 val nvar = ref 0
1221 1189
1222 fun setHyps (h as (n', hs)) = 1190 fun setHyps (n', hs) =
1223 let 1191 let
1224 val (n, _) = !hyps 1192 val (n, _, _) = !hyps
1225 in 1193 in
1226 if n' = n then 1194 if n' = n then
1227 () 1195 ()
1228 else 1196 else
1229 (hyps := h; 1197 (hyps := (n', hs, ref false);
1230 Cc.clear db; 1198 Cc.clear db;
1231 app (fn a => Cc.assert (db, a)) hs) 1199 app (fn a => Cc.assert (db, a)) hs)
1232 end 1200 end
1233 1201
1234 type stashed = int * (hyps * check) option ref list * (int * atom list) 1202 fun useKeys () =
1235 fun stash () = (!nvar, !path, !hyps) 1203 let
1204 val changed = ref false
1205
1206 fun findKeys (hyps, acc) =
1207 case hyps of
1208 [] => acc
1209 | (a as AReln (Sql tab, [r1])) :: hyps =>
1210 (case SM.find (!tabs, tab) of
1211 NONE => findKeys (hyps, a :: acc)
1212 | SOME (_, []) => findKeys (hyps, a :: acc)
1213 | SOME (_, ks) =>
1214 let
1215 fun finder (hyps, acc) =
1216 case hyps of
1217 [] => acc
1218 | (a as AReln (Sql tab', [r2])) :: hyps =>
1219 if tab' = tab andalso
1220 List.exists (List.all (fn f =>
1221 let
1222 val r =
1223 Cc.check (db,
1224 AReln (Eq, [Proj (r1, f),
1225 Proj (r2, f)]))
1226 in
1227 (*Print.prefaces "Fs"
1228 [("tab",
1229 Print.PD.string tab),
1230 ("r1",
1231 p_exp (Proj (r1, f))),
1232 ("r2",
1233 p_exp (Proj (r2, f))),
1234 ("r",
1235 Print.PD.string
1236 (Bool.toString r))];*)
1237 r
1238 end)) ks then
1239 (changed := true;
1240 Cc.assert (db, AReln (Eq, [r1, r2]));
1241 finder (hyps, acc))
1242 else
1243 finder (hyps, a :: acc)
1244 | a :: hyps => finder (hyps, a :: acc)
1245
1246 val hyps = finder (hyps, [])
1247 in
1248 findKeys (hyps, acc)
1249 end)
1250 | a :: hyps => findKeys (hyps, a :: acc)
1251
1252 fun loop hs =
1253 let
1254 val hs = findKeys (hs, [])
1255 in
1256 if !changed then
1257 (changed := false;
1258 loop hs)
1259 else
1260 ()
1261 end
1262
1263 val (_, hs, _) = !hyps
1264 in
1265 (*print "findKeys\n";*)
1266 loop hs
1267 end
1268
1269 fun complete () =
1270 let
1271 val (_, _, bf) = !hyps
1272 in
1273 if !bf then
1274 ()
1275 else
1276 (bf := true;
1277 useKeys ())
1278 end
1279
1280 type stashed = int * ((int * atom list) * check) option ref list * (int * atom list)
1281 fun stash () = (!nvar, !path, (#1 (!hyps), #2 (!hyps)))
1236 fun reinstate (nv, p, h) = 1282 fun reinstate (nv, p, h) =
1237 (nvar := nv; 1283 (nvar := nv;
1238 path := p; 1284 path := p;
1239 setHyps h) 1285 setHyps h)
1240 1286
1247 end 1293 end
1248 1294
1249 fun assert ats = 1295 fun assert ats =
1250 let 1296 let
1251 val n = !hnames 1297 val n = !hnames
1252 val (_, hs) = !hyps 1298 val (_, hs, _) = !hyps
1253 in 1299 in
1254 hnames := n + 1; 1300 hnames := n + 1;
1255 hyps := (n, ats @ hs); 1301 hyps := (n, ats @ hs, ref false);
1256 app (fn a => Cc.assert (db, a)) ats 1302 app (fn a => Cc.assert (db, a)) ats
1257 end 1303 end
1258 1304
1259 fun addPath c = path := ref (SOME (!hyps, c)) :: !path 1305 fun addPath c = path := ref (SOME ((#1 (!hyps), #2 (!hyps)), c)) :: !path
1260 1306
1261 val sendable = ref ([] : (atom list * exp list) list) 1307 val sendable = ref ([] : (atom list * exp list) list)
1262 1308
1263 fun checkGoals goals k = 1309 fun checkGoals goals k =
1264 let 1310 let
1266 case goals of 1312 case goals of
1267 [] => k unifs 1313 [] => k unifs
1268 | AReln (Sql tab, [Lvar lv]) :: goals => 1314 | AReln (Sql tab, [Lvar lv]) :: goals =>
1269 let 1315 let
1270 val saved = stash () 1316 val saved = stash ()
1271 val (_, hyps) = !hyps 1317 val (_, hyps, _) = !hyps
1272 1318
1273 fun tryAll unifs hyps = 1319 fun tryAll unifs hyps =
1274 case hyps of 1320 case hyps of
1275 [] => false 1321 [] => false
1276 | AReln (Sql tab', [e]) :: hyps => 1322 | AReln (Sql tab', [e]) :: hyps =>
1280 | _ :: hyps => tryAll unifs hyps 1326 | _ :: hyps => tryAll unifs hyps
1281 in 1327 in
1282 tryAll unifs hyps 1328 tryAll unifs hyps
1283 end 1329 end
1284 | (g as AReln (r, es)) :: goals => 1330 | (g as AReln (r, es)) :: goals =>
1285 Cc.check (db, AReln (r, map (simplify unifs) es)) 1331 (complete ();
1286 andalso checkGoals goals unifs 1332 Cc.check (db, AReln (r, map (simplify unifs) es))
1333 andalso checkGoals goals unifs)
1287 | ACond _ :: _ => false 1334 | ACond _ :: _ => false
1288 in 1335 in
1289 checkGoals goals IM.empty 1336 checkGoals goals IM.empty
1290 end
1291
1292 fun useKeys () =
1293 let
1294 fun findKeys hyps =
1295 case hyps of
1296 [] => ()
1297 | AReln (Sql tab, [r1]) :: hyps =>
1298 (case SM.find (!tabs, tab) of
1299 NONE => findKeys hyps
1300 | SOME (_, []) => findKeys hyps
1301 | SOME (_, ks) =>
1302 let
1303 fun finder hyps =
1304 case hyps of
1305 [] => ()
1306 | AReln (Sql tab', [r2]) :: hyps =>
1307 (if tab' = tab andalso
1308 List.exists (List.all (fn f =>
1309 let
1310 val r =
1311 Cc.check (db,
1312 AReln (Eq, [Proj (r1, f),
1313 Proj (r2, f)]))
1314 in
1315 (*Print.prefaces "Fs"
1316 [("tab",
1317 Print.PD.string tab),
1318 ("r1",
1319 p_exp (Proj (r1, f))),
1320 ("r2",
1321 p_exp (Proj (r2, f))),
1322 ("r",
1323 Print.PD.string
1324 (Bool.toString r))];*)
1325 r
1326 end)) ks then
1327 ((*Print.prefaces "Key match" [("tab", Print.PD.string tab),
1328 ("r1", p_exp r1),
1329 ("r2", p_exp r2),
1330 ("rp1", Cc.p_repOf cc r1),
1331 ("rp2", Cc.p_repOf cc r2)];*)
1332 Cc.assert (db, AReln (Eq, [r1, r2])))
1333 else
1334 ();
1335 finder hyps)
1336 | _ :: hyps => finder hyps
1337 in
1338 finder hyps;
1339 findKeys hyps
1340 end)
1341 | _ :: hyps => findKeys hyps
1342
1343 val (_, hs) = !hyps
1344 in
1345 (*print "findKeys\n";*)
1346 findKeys hs
1347 end 1337 end
1348 1338
1349 fun buildable uk (e, loc) = 1339 fun buildable uk (e, loc) =
1350 let 1340 let
1351 fun doPols pols acc = 1341 fun doPols pols acc =
1356 Cc.builtFrom (db, {UseKnown = uk, Base = acc, Derived = e})) 1346 Cc.builtFrom (db, {UseKnown = uk, Base = acc, Derived = e}))
1357 | (goals, es) :: pols => 1347 | (goals, es) :: pols =>
1358 checkGoals goals (fn unifs => doPols pols (map (simplify unifs) es @ acc)) 1348 checkGoals goals (fn unifs => doPols pols (map (simplify unifs) es @ acc))
1359 orelse doPols pols acc 1349 orelse doPols pols acc
1360 in 1350 in
1361 useKeys ();
1362 if doPols (!sendable) [] then 1351 if doPols (!sendable) [] then
1363 () 1352 ()
1364 else 1353 else
1365 let 1354 let
1366 val (_, hs) = !hyps 1355 val (_, hs, _) = !hyps
1367 in 1356 in
1368 ErrorMsg.errorAt loc "The information flow policy may be violated here."; 1357 ErrorMsg.errorAt loc "The information flow policy may be violated here.";
1369 Print.prefaces "Situation" [("Hypotheses", Print.p_list p_atom hs), 1358 Print.prefaces "Situation" [("Hypotheses", Print.p_list p_atom hs),
1370 ("User learns", p_exp e), 1359 ("User learns", p_exp e)(*,
1371 ("E-graph", Cc.p_database db)] 1360 ("E-graph", Cc.p_database db)*)]
1372 end 1361 end
1373 end 1362 end
1374 1363
1375 fun checkPaths () = 1364 fun checkPaths () =
1376 let 1365 let
1377 val hs = !hyps 1366 val (n, hs, _) = !hyps
1367 val hs = (n, hs)
1378 in 1368 in
1379 app (fn r => 1369 app (fn r =>
1380 case !r of 1370 case !r of
1381 NONE => () 1371 NONE => ()
1382 | SOME (hs, e) => 1372 | SOME (hs, e) =>
1389 fun allowSend v = ((*Print.prefaces "Allow" [("goals", Print.p_list p_atom (#1 v)), 1379 fun allowSend v = ((*Print.prefaces "Allow" [("goals", Print.p_list p_atom (#1 v)),
1390 ("exps", Print.p_list p_exp (#2 v))];*) 1380 ("exps", Print.p_list p_exp (#2 v))];*)
1391 sendable := v :: !sendable) 1381 sendable := v :: !sendable)
1392 1382
1393 fun send uk (e, loc) = ((*Print.preface ("Send", p_exp e);*) 1383 fun send uk (e, loc) = ((*Print.preface ("Send", p_exp e);*)
1384 complete ();
1394 checkPaths (); 1385 checkPaths ();
1395 if isKnown e then 1386 if isKnown e then
1396 () 1387 ()
1397 else 1388 else
1398 buildable uk (e, loc)) 1389 buildable uk (e, loc))
1399 1390
1400 fun doable pols (loc : ErrorMsg.span) = 1391 fun doable pols (loc : ErrorMsg.span) =
1401 let 1392 let
1402 val pols = !pols 1393 val pols = !pols
1403 in 1394 in
1395 complete ();
1404 if List.exists (fn goals => 1396 if List.exists (fn goals =>
1405 if checkGoals goals (fn _ => true) then 1397 if checkGoals goals (fn _ => true) then
1406 ((*Print.prefaces "Match" [("goals", Print.p_list p_atom goals), 1398 ((*Print.prefaces "Match" [("goals", Print.p_list p_atom goals),
1407 ("hyps", Print.p_list p_atom (#2 (!hyps)))];*) 1399 ("hyps", Print.p_list p_atom (#2 (!hyps)))];*)
1408 true) 1400 true)
1411 ("hyps", Print.p_list p_atom (#2 (!hyps)))];*) 1403 ("hyps", Print.p_list p_atom (#2 (!hyps)))];*)
1412 false)) pols then 1404 false)) pols then
1413 () 1405 ()
1414 else 1406 else
1415 let 1407 let
1416 val (_, hs) = !hyps 1408 val (_, hs, _) = !hyps
1417 in 1409 in
1418 ErrorMsg.errorAt loc "The database update policy may be violated here."; 1410 ErrorMsg.errorAt loc "The database update policy may be violated here.";
1419 Print.preface ("Hypotheses", Print.p_list p_atom hs) 1411 Print.preface ("Hypotheses", Print.p_list p_atom hs)
1420 end 1412 end
1421 end 1413 end
1432 fun allowDelete v = deletable := v :: !deletable 1424 fun allowDelete v = deletable := v :: !deletable
1433 val delete = doable deletable 1425 val delete = doable deletable
1434 1426
1435 fun reset () = (Cc.clear db; 1427 fun reset () = (Cc.clear db;
1436 path := []; 1428 path := [];
1437 hyps := (0, []); 1429 hyps := (0, [], ref false);
1438 nvar := 0; 1430 nvar := 0;
1439 sendable := []; 1431 sendable := [];
1440 insertable := []; 1432 insertable := [];
1441 updatable := []; 1433 updatable := [];
1442 deletable := []) 1434 deletable := [])
1443 1435
1444 fun havocReln r = 1436 fun havocReln r =
1445 let 1437 let
1446 val n = !hnames 1438 val n = !hnames
1447 val (_, hs) = !hyps 1439 val (_, hs, _) = !hyps
1448 in 1440 in
1449 hnames := n + 1; 1441 hnames := n + 1;
1450 hyps := (n, List.filter (fn AReln (r', _) => r' <> r | _ => true) hs) 1442 hyps := (n, List.filter (fn AReln (r', _) => r' <> r | _ => true) hs, ref false)
1451 end 1443 end
1452 1444
1453 fun debug () = 1445 fun debug () =
1454 let 1446 let
1455 val (_, hs) = !hyps 1447 val (_, hs, _) = !hyps
1456 in 1448 in
1457 Print.preface ("Hyps", Print.p_list p_atom hs) 1449 Print.preface ("Hyps", Print.p_list p_atom hs)
1458 end 1450 end
1459 1451
1460 end 1452 end