diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2008-07-01 12:10:46 -0400 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2008-07-01 12:10:46 -0400 |
| commit | 7628e1d8f7f8199531c9bc08a774c9a9e2bc5d63 (patch) | |
| tree | 3d434c77c5ec6ac3660a553072e1c1ba26cd4665 /src/disjoint.sml | |
| parent | d28cad7cc5881018717c7e875c99c51469da9d44 (diff) | |
Disjointness assumptions
Diffstat (limited to 'src/disjoint.sml')
| -rw-r--r-- | src/disjoint.sml | 5 |
1 files changed, 3 insertions, 2 deletions
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) |