Initial disjointness prover

1 files changed, 294 insertions, 0 deletions

diff --git a/src/disjoint.sml b/src/disjoint.sml
new file mode 100644
index 00000000..784bd635
--- /dev/null
+++ b/src/disjoint.sml
@@ -0,0 +1,294 @@
+(* Copyright (c) 2008, Adam Chlipala
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *
+ * - Redistributions of source code must retain the above copyright notice,
+ *   this list of conditions and the following disclaimer.
+ * - Redistributions in binary form must reproduce the above copyright notice,
+ *   this list of conditions and the following disclaimer in the documentation
+ *   and/or other materials provided with the distribution.
+ * - The names of contributors may not be used to endorse or promote products
+ *   derived from this software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
+ * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR 
+ * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+ * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+ * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+ * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+ * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+ * POSSIBILITY OF SUCH DAMAGE.
+ *)
+
+structure Disjoint :> DISJOINT = struct
+
+open Elab
+open ElabOps
+
+structure SS = BinarySetFn(struct
+                           type ord_key = string
+                           val compare = String.compare
+                           end)
+
+structure IS = IntBinarySet
+structure IM = IntBinaryMap
+
+type name_ineqs = {
+     namesC : SS.set,
+     namesR : IS.set,
+     namesN : IS.set
+}
+
+val name_default = {
+    namesC = SS.empty,
+    namesR = IS.empty,
+    namesN = IS.empty
+}
+
+type row_ineqs = {
+     namesC : SS.set,
+     namesR : IS.set,
+     namesN : IS.set,
+     rowsR : IS.set,
+     rowsN : IS.set
+}
+
+val row_default = {
+    namesC = SS.empty,
+    namesR = IS.empty,
+    namesN = IS.empty,
+    rowsR = IS.empty,
+    rowsN = IS.empty
+}
+
+fun nameToRow_ineqs {namesC, namesR, namesN} =
+    {namesC = namesC,
+     namesR = namesR,
+     namesN = namesN,
+     rowsR = IS.empty,
+     rowsN = IS.empty}
+
+type env = {
+     namesR : name_ineqs IM.map,
+     namesN : name_ineqs IM.map,
+     rowsR : row_ineqs IM.map,
+     rowsN : row_ineqs IM.map
+}
+
+val empty = {
+    namesR = IM.empty,
+    namesN = IM.empty,
+    rowsR = IM.empty,
+    rowsN = IM.empty
+}
+
+datatype piece =
+         NameC of string
+       | NameR of int
+       | NameN of int
+       | RowR of int
+       | RowN of int
+       | Unknown
+
+fun nameToRow (c, loc) =
+    (CRecord ((KUnit, loc), [((c, loc), (CUnit, loc))]), loc)
+
+fun pieceToRow (p, loc) =
+    case p of
+        NameC s => nameToRow (CName s, loc)
+      | NameR n => nameToRow (CRel n, loc)
+      | NameN n => nameToRow (CNamed n, loc)
+      | RowR n => (CRel n, loc)
+      | RowN n => (CRel n, loc)
+      | Unknown => raise Fail "Unknown to row"
+
+fun decomposeRow env c =
+    let
+        fun decomposeName (c, acc) =
+            case #1 (hnormCon env c) of
+                CName s => NameC s :: acc
+              | CRel n => NameR n :: acc
+              | CNamed n => NameN n :: acc
+              | _ => Unknown :: acc
+                     
+        fun decomposeRow (c, acc) =
+            case #1 (hnormCon env c) of
+                CRecord (_, xcs) => foldl (fn ((x, _), acc) => decomposeName (x, acc)) acc xcs
+              | CConcat (c1, c2) => decomposeRow (c1, decomposeRow (c2, acc))
+              | CRel n => RowR n :: acc
+              | CNamed n => RowN n :: acc
+              | _ => Unknown :: acc
+    in
+        decomposeRow (c, [])
+    end
+
+fun assertPiece_name (ps, ineqs : name_ineqs) =
+    {namesC = foldl (fn (p', namesC) =>
+                        case p' of
+                            NameC s => SS.add (namesC, s)
+                          | _ => namesC) (#namesC ineqs) ps,
+     namesR = foldl (fn (p', namesR) =>
+                        case p' of
+                            NameR n => IS.add (namesR, n)
+                          | _ => namesR) (#namesR ineqs) ps,
+     namesN = foldl (fn (p', namesN) =>
+                        case p' of
+                            NameN n => IS.add (namesN, n)
+                          | _ => namesN) (#namesN ineqs) ps}
+
+fun assertPiece_row (ps, ineqs : row_ineqs) =
+    {namesC = foldl (fn (p', namesC) =>
+                        case p' of
+                            NameC s => SS.add (namesC, s)
+                          | _ => namesC) (#namesC ineqs) ps,
+     namesR = foldl (fn (p', namesR) =>
+                        case p' of
+                            NameR n => IS.add (namesR, n)
+                          | _ => namesR) (#namesR ineqs) ps,
+     namesN = foldl (fn (p', namesN) =>
+                        case p' of
+                            NameN n => IS.add (namesN, n)
+                          | _ => namesN) (#namesN ineqs) ps,
+     rowsR = foldl (fn (p', rowsR) =>
+                        case p' of
+                            RowR n => IS.add (rowsR, n)
+                          | _ => rowsR) (#rowsR ineqs) ps,
+     rowsN = foldl (fn (p', rowsN) =>
+                        case p' of
+                            RowN n => IS.add (rowsN, n)
+                          | _ => rowsN) (#rowsN ineqs) ps}
+
+fun assertPiece ps (p, denv) =
+    case p of
+        Unknown => denv
+      | NameC _ => denv
+
+      | NameR n =>
+        let
+            val ineqs = Option.getOpt (IM.find (#namesR denv, n), name_default)
+            val ineqs = assertPiece_name (ps, ineqs)
+        in
+            {namesR = IM.insert (#namesR denv, n, ineqs),
+             namesN = #namesN denv,
+             rowsR = #rowsR denv,
+             rowsN = #rowsN denv}
+        end
+
+      | NameN n =>
+        let
+            val ineqs = Option.getOpt (IM.find (#namesN denv, n), name_default)
+            val ineqs = assertPiece_name (ps, ineqs)
+        in
+            {namesR = #namesR denv,
+             namesN = IM.insert (#namesN denv, n, ineqs),
+             rowsR = #rowsR denv,
+             rowsN = #rowsN denv}
+        end
+
+      | RowR n =>
+        let
+            val ineqs = Option.getOpt (IM.find (#rowsR denv, n), row_default)
+            val ineqs = assertPiece_row (ps, ineqs)
+        in
+            {namesR = #namesR denv,
+             namesN = #namesN denv,
+             rowsR = IM.insert (#rowsR denv, n, ineqs),
+             rowsN = #rowsN denv}
+        end
+
+      | RowN n =>
+        let
+            val ineqs = Option.getOpt (IM.find (#rowsN denv, n), row_default)
+            val ineqs = assertPiece_row (ps, ineqs)
+        in
+            {namesR = #namesR denv,
+             namesN = #namesN denv,
+             rowsR = #rowsR denv,
+             rowsN = IM.insert (#rowsN denv, n, ineqs)}
+        end
+
+fun assert env denv (c1, c2) =
+    let
+        val ps1 = decomposeRow env c1
+        val ps2 = decomposeRow env c2
+
+        val denv = foldl (assertPiece ps2) denv ps1
+    in
+        foldl (assertPiece ps1) denv ps2
+    end
+
+fun nameEnter {namesC, namesR, namesN} =
+    {namesC = namesC,
+     namesR = IS.map (fn n => n + 1) namesR,
+     namesN = namesN}
+
+fun rowEnter {namesC, namesR, namesN, rowsR, rowsN} =
+    {namesC = namesC,
+     namesR = IS.map (fn n => n + 1) namesR,
+     namesN = namesN,
+     rowsR = IS.map (fn n => n + 1) rowsR,
+     rowsN = rowsN}
+
+fun enter {namesR, namesN, rowsR, rowsN} =
+    {namesR = IM.foldli (fn (n, ineqs, namesR) => IM.insert (namesR, n+1, nameEnter ineqs)) IM.empty namesR,
+     namesN = IM.map nameEnter namesN,
+     rowsR = IM.foldli (fn (n, ineqs, rowsR) => IM.insert (rowsR, n+1, rowEnter ineqs)) IM.empty rowsR,
+     rowsN = IM.map rowEnter rowsN}
+
+fun getIneqs (denv : env) p =
+    case p of
+        Unknown => raise Fail "getIneqs: Unknown"
+      | NameC _ => raise Fail "getIneqs: NameC"
+      | NameR n => nameToRow_ineqs (Option.getOpt (IM.find (#namesR denv, n), name_default))
+      | NameN n => nameToRow_ineqs (Option.getOpt (IM.find (#namesN denv, n), name_default))
+      | RowR n => Option.getOpt (IM.find (#rowsR denv, n), row_default)
+      | RowN n => Option.getOpt (IM.find (#rowsN denv, n), row_default)
+
+fun prove1' denv (p1, p2) =
+    let
+        val {namesC, namesR, namesN, rowsR, rowsN} = getIneqs denv p1
+    in
+        case p2 of
+            Unknown => raise Fail "prove1': Unknown"
+          | NameC s => SS.member (namesC, s)
+          | NameR n => IS.member (namesR, n)
+          | NameN n => IS.member (namesN, n)
+          | RowR n => IS.member (rowsR, n)
+          | RowN n => IS.member (rowsN, n)
+    end
+
+fun prove1 denv (p1, p2) =
+    case (p1, p2) of
+        (NameC s1, NameC s2) => s1 <> s2
+      | (_, RowR _) => prove1' denv (p2, p1)
+      | (_, RowN _) => prove1' denv (p2, p1)
+      | _ => prove1' denv (p1, p2)
+
+fun prove env denv (c1, c2, loc) =
+    let
+        val ps1 = decomposeRow env c1
+        val ps2 = decomposeRow env c2
+
+        val hasUnknown = List.exists (fn p => p = Unknown)
+    in
+        if hasUnknown ps1 orelse hasUnknown ps2 then
+            (ErrorMsg.errorAt loc "Structure of row is too complicated to prove disjointness";
+             Print.eprefaces' [("Row 1", ElabPrint.p_con env c1),
+                               ("Row 2", ElabPrint.p_con env c2)];
+             [])
+        else
+            foldl (fn (p1, rem) =>
+                      foldl (fn (p2, rem) =>
+                                if prove1 denv (p1, p2) then
+                                    rem
+                                else
+                                    (pieceToRow (p1, loc), pieceToRow (p2, loc)) :: rem) rem ps2)
+            [] ps1
+    end
+
+end