Mercurial > urweb

comparison src/iflow.sml @ 1281:60e19545841b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
equalAny policies
author Adam Chlipala <adam@chlipala.net>
date Tue, 27 Jul 2010 12:12:08 -0400
parents 3d06e0f7a6f3
children a9a500d22ebc
comparison
equal deleted inserted replaced
1280:3d06e0f7a6f3 1281:60e19545841b
1226 val addPath : check -> unit 1226 val addPath : check -> unit
1227 1227
1228 val allowSend : atom list * exp list -> unit 1228 val allowSend : atom list * exp list -> unit
1229 val send : check -> unit 1229 val send : check -> unit
1230 1230
1231 val allowEqualKnown : { table : string, field : string } -> unit 1231 val allowEqual : { table : string, field : string, known : bool } -> unit
1232 val mayTest : prop -> bool 1232 val mayTest : prop -> bool
1233 1233
1234 val allowInsert : atom list -> unit 1234 val allowInsert : atom list -> unit
1235 val insert : ErrorMsg.span -> unit 1235 val insert : ErrorMsg.span -> unit
1236 1236
1507 1507
1508 val deletable = ref ([] : atom list list) 1508 val deletable = ref ([] : atom list list)
1509 fun allowDelete v = deletable := v :: !deletable 1509 fun allowDelete v = deletable := v :: !deletable
1510 val delete = doable deletable 1510 val delete = doable deletable
1511 1511
1512 val testable = ref ([] : { table : string, field : string } list) 1512 val testable = ref ([] : { table : string, field : string, known : bool } list)
1513 fun allowEqualKnown v = testable := v :: !testable 1513 fun allowEqual v = testable := v :: !testable
1514 fun mayTest p = 1514 fun mayTest p =
1515 case p of 1515 case p of
1516 Reln (Eq, [e1, e2]) => 1516 Reln (Eq, [e1, e2]) =>
1517 let 1517 let
1518 val (_, hs, _) = !hyps 1518 val (_, hs, _) = !hyps
1521 | _ => false) hs 1521 | _ => false) hs
1522 1522
1523 fun allowed (tab, v) = 1523 fun allowed (tab, v) =
1524 case tab of 1524 case tab of
1525 Proj (Var tab, fd) => 1525 Proj (Var tab, fd) =>
1526 List.exists (fn {table = tab', field = fd'} => 1526 List.exists (fn {table = tab', field = fd', known} =>
1527 fd' = fd 1527 fd' = fd
1528 andalso tableInHyps (tab', tab)) (!testable) 1528 andalso tableInHyps (tab', tab)
1529 andalso Cc.check (db, AReln (Known, [v])) 1529 andalso (not known orelse Cc.check (db, AReln (Known, [v])))) (!testable)
1530 | _ => false 1530 | _ => false
1531 in 1531 in
1532 if allowed (e1, e2) orelse allowed (e2, e1) then 1532 if allowed (e1, e2) orelse allowed (e2, e1) then
1533 (Cc.assert (db, AReln (Eq, [e1, e2])); 1533 (assert [AReln (Eq, [e1, e2])];
1534 true) 1534 true)
1535 else 1535 else
1536 false 1536 false
1537 end 1537 end
1538 | _ => false 1538 | _ => false
2525 val outs = [Lvar 0] 2525 val outs = [Lvar 0]
2526 in 2526 in
2527 St.allowSend ([p], outs) 2527 St.allowSend ([p], outs)
2528 end 2528 end
2529 | _ => ()) 2529 | _ => ())
2530 | PolEqualKnown {table = tab, field = nm} => 2530 | PolEqual {table = tab, field = nm, known} =>
2531 (case #1 tab of 2531 (case #1 tab of
2532 EPrim (Prim.String tab) => St.allowEqualKnown {table = String.extract (tab, 3, NONE), 2532 EPrim (Prim.String tab) => St.allowEqual {table = String.extract (tab, 3, NONE),
2533 field = nm} 2533 field = nm,
2534 known = known}
2534 | _ => ErrorMsg.errorAt loc "Table for 'equalKnown' policy isn't fully resolved.") 2535 | _ => ErrorMsg.errorAt loc "Table for 'equalKnown' policy isn't fully resolved.")
2535 end 2536 end
2536 2537
2537 | _ => () 2538 | _ => ()
2538 in 2539 in