Mercurial > urweb

diff src/disjoint.sml @ 84:e86370850c30

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Disjointness assumptions
author Adam Chlipala <adamc@hcoop.net>
date Tue, 01 Jul 2008 12:10:46 -0400
parents 0a1baddd8ab2
children 7bab29834cd6
line wrap: on
line diff
--- a/src/disjoint.sml	Tue Jul 01 11:39:14 2008 -0400
+++ b/src/disjoint.sml	Tue Jul 01 12:10:46 2008 -0400
@@ -114,7 +114,7 @@
                 CName s => NameC s :: acc
               | CRel n => NameR n :: acc
               | CNamed n => NameN n :: acc
-              | _ => Unknown :: acc
+              | _ => (print "Unknown name\n"; Unknown :: acc)
                      
         fun decomposeRow (c, acc) =
             case #1 (hnormCon env c) of
@@ -122,7 +122,7 @@
               | CConcat (c1, c2) => decomposeRow (c1, decomposeRow (c2, acc))
               | CRel n => RowR n :: acc
               | CNamed n => RowN n :: acc
-              | _ => Unknown :: acc
+              | _ => (print "Unknown row\n"; Unknown :: acc)
     in
         decomposeRow (c, [])
     end
@@ -265,6 +265,7 @@
 fun prove1 denv (p1, p2) =
     case (p1, p2) of
         (NameC s1, NameC s2) => s1 <> s2
+      | (NameC _, _) => prove1' denv (p2, p1)
       | (_, RowR _) => prove1' denv (p2, p1)
       | (_, RowN _) => prove1' denv (p2, p1)
       | _ => prove1' denv (p1, p2)