From 7628e1d8f7f8199531c9bc08a774c9a9e2bc5d63 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Tue, 1 Jul 2008 12:10:46 -0400 Subject: Disjointness assumptions --- src/disjoint.sml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'src/disjoint.sml') diff --git a/src/disjoint.sml b/src/disjoint.sml index fa4c8618..c9f6d2e9 100644 --- a/src/disjoint.sml +++ b/src/disjoint.sml @@ -114,7 +114,7 @@ fun decomposeRow env c = 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 @@ fun decomposeRow env c = | 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) = 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) -- cgit v1.2.3