Mercurial > urweb

comparison 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
comparison
equal deleted inserted replaced
83:0a1baddd8ab2 84:e86370850c30
112 fun decomposeName (c, acc) = 112 fun decomposeName (c, acc) =
113 case #1 (hnormCon env c) of 113 case #1 (hnormCon env c) of
114 CName s => NameC s :: acc 114 CName s => NameC s :: acc
115 | CRel n => NameR n :: acc 115 | CRel n => NameR n :: acc
116 | CNamed n => NameN n :: acc 116 | CNamed n => NameN n :: acc
117 | _ => Unknown :: acc 117 | _ => (print "Unknown name\n"; Unknown :: acc)
118 118
119 fun decomposeRow (c, acc) = 119 fun decomposeRow (c, acc) =
120 case #1 (hnormCon env c) of 120 case #1 (hnormCon env c) of
121 CRecord (_, xcs) => foldl (fn ((x, _), acc) => decomposeName (x, acc)) acc xcs 121 CRecord (_, xcs) => foldl (fn ((x, _), acc) => decomposeName (x, acc)) acc xcs
122 | CConcat (c1, c2) => decomposeRow (c1, decomposeRow (c2, acc)) 122 | CConcat (c1, c2) => decomposeRow (c1, decomposeRow (c2, acc))
123 | CRel n => RowR n :: acc 123 | CRel n => RowR n :: acc
124 | CNamed n => RowN n :: acc 124 | CNamed n => RowN n :: acc
125 | _ => Unknown :: acc 125 | _ => (print "Unknown row\n"; Unknown :: acc)
126 in 126 in
127 decomposeRow (c, []) 127 decomposeRow (c, [])
128 end 128 end
129 129
130 fun assertPiece_name (ps, ineqs : name_ineqs) = 130 fun assertPiece_name (ps, ineqs : name_ineqs) =
263 end 263 end
264 264
265 fun prove1 denv (p1, p2) = 265 fun prove1 denv (p1, p2) =
266 case (p1, p2) of 266 case (p1, p2) of
267 (NameC s1, NameC s2) => s1 <> s2 267 (NameC s1, NameC s2) => s1 <> s2
268 | (NameC _, _) => prove1' denv (p2, p1)
268 | (_, RowR _) => prove1' denv (p2, p1) 269 | (_, RowR _) => prove1' denv (p2, p1)
269 | (_, RowN _) => prove1' denv (p2, p1) 270 | (_, RowN _) => prove1' denv (p2, p1)
270 | _ => prove1' denv (p1, p2) 271 | _ => prove1' denv (p1, p2)
271 272
272 fun prove env denv (c1, c2, loc) = 273 fun prove env denv (c1, c2, loc) =