# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1270413874 14400
# Node ID a75c66dd2aebe17389e28647928bdf2b6abfc27d
# Parent  509a6d7b60fb0f034f633e02515ec12e1eeda733
Relax checking of table implications

diff -r 509a6d7b60fb -r a75c66dd2aeb src/iflow.sml
--- a/src/iflow.sml	Sun Apr 04 16:17:23 2010 -0400
+++ b/src/iflow.sml	Sun Apr 04 16:44:34 2010 -0400
@@ -186,6 +186,10 @@
 
 val unif = ref (IM.empty : exp IM.map)
 
+fun reset () = unif := IM.empty
+fun save () = !unif
+fun restore x = unif := x
+
 fun lvarIn lv =
     let
         fun lvi e =
@@ -242,12 +246,12 @@
 
 fun eq (e1, e2) =
     let
-        val saved = !unif
+        val saved = save ()
     in
         if eq' (simplify e1, simplify e2) then
             true
         else
-            (unif := saved;
+            (restore saved;
              false)
     end
 
@@ -260,16 +264,15 @@
         (case (es1, es2) of
              ([Recd xes1], [Recd xes2]) =>
              let
-                 val saved = !unif
+                 val saved = save ()
              in
-                 (*print ("Go: " ^ r1' ^ "\n");*)
-                 (*raise Imply (Reln (r1, es1), Reln (r2, es2));*)
                  if List.all (fn (f, e2) =>
-                                 List.exists (fn (f', e1) =>
-                                                 f' = f andalso eq (e1, e2)) xes1) xes2 then
+                                 case ListUtil.search (fn (f', e1) => if f' = f then SOME e1 else NONE) xes1 of
+                                     NONE => true
+                                   | SOME e1 => eq (e1, e2)) xes2 then
                      true
                  else
-                     (unif := saved;
+                     (restore saved;
                       false)
              end
            | _ => false)
@@ -277,12 +280,12 @@
         (case (es1, es2) of
              ([x1, y1], [x2, y2]) =>
              let
-                 val saved = !unif
+                 val saved = save ()
              in
                  if eq (x1, x2) andalso eq (y1, y2) then
                      true
                  else
-                     (unif := saved;
+                     (restore saved;
                       (*raise Imply (Reln (Eq, es1), Reln (Eq, es2));*)
                       eq (x1, y2) andalso eq (y1, x2))
              end
@@ -290,7 +293,7 @@
       | _ => false
 
 fun imply (p1, p2) =
-    (unif := IM.empty;
+    (reset ();
      (*raise (Imply (p1, p2));*)
      decomp true (fn (e1, e2) => e1 andalso e2 ()) p1
             (fn hyps =>
@@ -307,13 +310,13 @@
                                             [] => onFail ()
                                           | h :: hyps =>
                                             let
-                                                val saved = !unif
+                                                val saved = save ()
                                             in
                                                 if rimp (h, g) then
                                                     let
-                                                        val changed = IM.numItems (!unif) = IM.numItems saved
+                                                        val changed = IM.numItems (!unif) <> IM.numItems saved
                                                     in
-                                                        gls goals (fn () => (unif := saved;
+                                                        gls goals (fn () => (restore saved;
                                                                              changed andalso hps hyps))
                                                     end
                                                 else
@@ -660,7 +663,7 @@
 
               | _ => (vals, pols)
 
-        val () = unif := IM.empty
+        val () = reset ()
 
         val (vals, pols) = foldl decl ([], []) file
     in
diff -r 509a6d7b60fb -r a75c66dd2aeb tests/policy.ur
--- a/tests/policy.ur	Sun Apr 04 16:17:23 2010 -0400
+++ b/tests/policy.ur	Sun Apr 04 16:44:34 2010 -0400
@@ -1,11 +1,11 @@
 table fruit : { Id : int, Nam : string, Weight : float, Secret : string }
 
-policy query_policy (SELECT fruit.Id, fruit.Nam FROM fruit)
+policy query_policy (SELECT fruit.Id, fruit.Nam, fruit.Weight FROM fruit)
 
 fun main () =
-    xml <- queryX (SELECT fruit.Id, fruit.Nam, fruit.Secret
+    xml <- queryX (SELECT fruit.Id, fruit.Nam
                    FROM fruit)
-           (fn x => <xml><li>{[x.Fruit.Secret]}</li></xml>);
+           (fn x => <xml><li>{[x.Fruit.Id]}: {[x.Fruit.Nam]}</li></xml>);
 
     return <xml><body>
       {xml}