Mercurial > urweb

annotate src/disjoint.sml @ 82:b4f2a258e52c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Initial disjointness prover
author Adam Chlipala <adamc@hcoop.net>
date Tue, 01 Jul 2008 10:55:38 -0400
parents
children 0a1baddd8ab2
rev   line source
adamc@82 1 (* Copyright (c) 2008, Adam Chlipala
adamc@82 2 * All rights reserved.
adamc@82 3 *
adamc@82 4 * Redistribution and use in source and binary forms, with or without
adamc@82 5 * modification, are permitted provided that the following conditions are met:
adamc@82 6 *
adamc@82 7 * - Redistributions of source code must retain the above copyright notice,
adamc@82 8 * this list of conditions and the following disclaimer.
adamc@82 9 * - Redistributions in binary form must reproduce the above copyright notice,
adamc@82 10 * this list of conditions and the following disclaimer in the documentation
adamc@82 11 * and/or other materials provided with the distribution.
adamc@82 12 * - The names of contributors may not be used to endorse or promote products
adamc@82 13 * derived from this software without specific prior written permission.
adamc@82 14 *
adamc@82 15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adamc@82 16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adamc@82 17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adamc@82 18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adamc@82 19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
adamc@82 20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adamc@82 21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adamc@82 22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adamc@82 23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adamc@82 24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adamc@82 25 * POSSIBILITY OF SUCH DAMAGE.
adamc@82 26 *)
adamc@82 27
adamc@82 28 structure Disjoint :> DISJOINT = struct
adamc@82 29
adamc@82 30 open Elab
adamc@82 31 open ElabOps
adamc@82 32
adamc@82 33 structure SS = BinarySetFn(struct
adamc@82 34 type ord_key = string
adamc@82 35 val compare = String.compare
adamc@82 36 end)
adamc@82 37
adamc@82 38 structure IS = IntBinarySet
adamc@82 39 structure IM = IntBinaryMap
adamc@82 40
adamc@82 41 type name_ineqs = {
adamc@82 42 namesC : SS.set,
adamc@82 43 namesR : IS.set,
adamc@82 44 namesN : IS.set
adamc@82 45 }
adamc@82 46
adamc@82 47 val name_default = {
adamc@82 48 namesC = SS.empty,
adamc@82 49 namesR = IS.empty,
adamc@82 50 namesN = IS.empty
adamc@82 51 }
adamc@82 52
adamc@82 53 type row_ineqs = {
adamc@82 54 namesC : SS.set,
adamc@82 55 namesR : IS.set,
adamc@82 56 namesN : IS.set,
adamc@82 57 rowsR : IS.set,
adamc@82 58 rowsN : IS.set
adamc@82 59 }
adamc@82 60
adamc@82 61 val row_default = {
adamc@82 62 namesC = SS.empty,
adamc@82 63 namesR = IS.empty,
adamc@82 64 namesN = IS.empty,
adamc@82 65 rowsR = IS.empty,
adamc@82 66 rowsN = IS.empty
adamc@82 67 }
adamc@82 68
adamc@82 69 fun nameToRow_ineqs {namesC, namesR, namesN} =
adamc@82 70 {namesC = namesC,
adamc@82 71 namesR = namesR,
adamc@82 72 namesN = namesN,
adamc@82 73 rowsR = IS.empty,
adamc@82 74 rowsN = IS.empty}
adamc@82 75
adamc@82 76 type env = {
adamc@82 77 namesR : name_ineqs IM.map,
adamc@82 78 namesN : name_ineqs IM.map,
adamc@82 79 rowsR : row_ineqs IM.map,
adamc@82 80 rowsN : row_ineqs IM.map
adamc@82 81 }
adamc@82 82
adamc@82 83 val empty = {
adamc@82 84 namesR = IM.empty,
adamc@82 85 namesN = IM.empty,
adamc@82 86 rowsR = IM.empty,
adamc@82 87 rowsN = IM.empty
adamc@82 88 }
adamc@82 89
adamc@82 90 datatype piece =
adamc@82 91 NameC of string
adamc@82 92 | NameR of int
adamc@82 93 | NameN of int
adamc@82 94 | RowR of int
adamc@82 95 | RowN of int
adamc@82 96 | Unknown
adamc@82 97
adamc@82 98 fun nameToRow (c, loc) =
adamc@82 99 (CRecord ((KUnit, loc), [((c, loc), (CUnit, loc))]), loc)
adamc@82 100
adamc@82 101 fun pieceToRow (p, loc) =
adamc@82 102 case p of
adamc@82 103 NameC s => nameToRow (CName s, loc)
adamc@82 104 | NameR n => nameToRow (CRel n, loc)
adamc@82 105 | NameN n => nameToRow (CNamed n, loc)
adamc@82 106 | RowR n => (CRel n, loc)
adamc@82 107 | RowN n => (CRel n, loc)
adamc@82 108 | Unknown => raise Fail "Unknown to row"
adamc@82 109
adamc@82 110 fun decomposeRow env c =
adamc@82 111 let
adamc@82 112 fun decomposeName (c, acc) =
adamc@82 113 case #1 (hnormCon env c) of
adamc@82 114 CName s => NameC s :: acc
adamc@82 115 | CRel n => NameR n :: acc
adamc@82 116 | CNamed n => NameN n :: acc
adamc@82 117 | _ => Unknown :: acc
adamc@82 118
adamc@82 119 fun decomposeRow (c, acc) =
adamc@82 120 case #1 (hnormCon env c) of
adamc@82 121 CRecord (_, xcs) => foldl (fn ((x, _), acc) => decomposeName (x, acc)) acc xcs
adamc@82 122 | CConcat (c1, c2) => decomposeRow (c1, decomposeRow (c2, acc))
adamc@82 123 | CRel n => RowR n :: acc
adamc@82 124 | CNamed n => RowN n :: acc
adamc@82 125 | _ => Unknown :: acc
adamc@82 126 in
adamc@82 127 decomposeRow (c, [])
adamc@82 128 end
adamc@82 129
adamc@82 130 fun assertPiece_name (ps, ineqs : name_ineqs) =
adamc@82 131 {namesC = foldl (fn (p', namesC) =>
adamc@82 132 case p' of
adamc@82 133 NameC s => SS.add (namesC, s)
adamc@82 134 | _ => namesC) (#namesC ineqs) ps,
adamc@82 135 namesR = foldl (fn (p', namesR) =>
adamc@82 136 case p' of
adamc@82 137 NameR n => IS.add (namesR, n)
adamc@82 138 | _ => namesR) (#namesR ineqs) ps,
adamc@82 139 namesN = foldl (fn (p', namesN) =>
adamc@82 140 case p' of
adamc@82 141 NameN n => IS.add (namesN, n)
adamc@82 142 | _ => namesN) (#namesN ineqs) ps}
adamc@82 143
adamc@82 144 fun assertPiece_row (ps, ineqs : row_ineqs) =
adamc@82 145 {namesC = foldl (fn (p', namesC) =>
adamc@82 146 case p' of
adamc@82 147 NameC s => SS.add (namesC, s)
adamc@82 148 | _ => namesC) (#namesC ineqs) ps,
adamc@82 149 namesR = foldl (fn (p', namesR) =>
adamc@82 150 case p' of
adamc@82 151 NameR n => IS.add (namesR, n)
adamc@82 152 | _ => namesR) (#namesR ineqs) ps,
adamc@82 153 namesN = foldl (fn (p', namesN) =>
adamc@82 154 case p' of
adamc@82 155 NameN n => IS.add (namesN, n)
adamc@82 156 | _ => namesN) (#namesN ineqs) ps,
adamc@82 157 rowsR = foldl (fn (p', rowsR) =>
adamc@82 158 case p' of
adamc@82 159 RowR n => IS.add (rowsR, n)
adamc@82 160 | _ => rowsR) (#rowsR ineqs) ps,
adamc@82 161 rowsN = foldl (fn (p', rowsN) =>
adamc@82 162 case p' of
adamc@82 163 RowN n => IS.add (rowsN, n)
adamc@82 164 | _ => rowsN) (#rowsN ineqs) ps}
adamc@82 165
adamc@82 166 fun assertPiece ps (p, denv) =
adamc@82 167 case p of
adamc@82 168 Unknown => denv
adamc@82 169 | NameC _ => denv
adamc@82 170
adamc@82 171 | NameR n =>
adamc@82 172 let
adamc@82 173 val ineqs = Option.getOpt (IM.find (#namesR denv, n), name_default)
adamc@82 174 val ineqs = assertPiece_name (ps, ineqs)
adamc@82 175 in
adamc@82 176 {namesR = IM.insert (#namesR denv, n, ineqs),
adamc@82 177 namesN = #namesN denv,
adamc@82 178 rowsR = #rowsR denv,
adamc@82 179 rowsN = #rowsN denv}
adamc@82 180 end
adamc@82 181
adamc@82 182 | NameN n =>
adamc@82 183 let
adamc@82 184 val ineqs = Option.getOpt (IM.find (#namesN denv, n), name_default)
adamc@82 185 val ineqs = assertPiece_name (ps, ineqs)
adamc@82 186 in
adamc@82 187 {namesR = #namesR denv,
adamc@82 188 namesN = IM.insert (#namesN denv, n, ineqs),
adamc@82 189 rowsR = #rowsR denv,
adamc@82 190 rowsN = #rowsN denv}
adamc@82 191 end
adamc@82 192
adamc@82 193 | RowR n =>
adamc@82 194 let
adamc@82 195 val ineqs = Option.getOpt (IM.find (#rowsR denv, n), row_default)
adamc@82 196 val ineqs = assertPiece_row (ps, ineqs)
adamc@82 197 in
adamc@82 198 {namesR = #namesR denv,
adamc@82 199 namesN = #namesN denv,
adamc@82 200 rowsR = IM.insert (#rowsR denv, n, ineqs),
adamc@82 201 rowsN = #rowsN denv}
adamc@82 202 end
adamc@82 203
adamc@82 204 | RowN n =>
adamc@82 205 let
adamc@82 206 val ineqs = Option.getOpt (IM.find (#rowsN denv, n), row_default)
adamc@82 207 val ineqs = assertPiece_row (ps, ineqs)
adamc@82 208 in
adamc@82 209 {namesR = #namesR denv,
adamc@82 210 namesN = #namesN denv,
adamc@82 211 rowsR = #rowsR denv,
adamc@82 212 rowsN = IM.insert (#rowsN denv, n, ineqs)}
adamc@82 213 end
adamc@82 214
adamc@82 215 fun assert env denv (c1, c2) =
adamc@82 216 let
adamc@82 217 val ps1 = decomposeRow env c1
adamc@82 218 val ps2 = decomposeRow env c2
adamc@82 219
adamc@82 220 val denv = foldl (assertPiece ps2) denv ps1
adamc@82 221 in
adamc@82 222 foldl (assertPiece ps1) denv ps2
adamc@82 223 end
adamc@82 224
adamc@82 225 fun nameEnter {namesC, namesR, namesN} =
adamc@82 226 {namesC = namesC,
adamc@82 227 namesR = IS.map (fn n => n + 1) namesR,
adamc@82 228 namesN = namesN}
adamc@82 229
adamc@82 230 fun rowEnter {namesC, namesR, namesN, rowsR, rowsN} =
adamc@82 231 {namesC = namesC,
adamc@82 232 namesR = IS.map (fn n => n + 1) namesR,
adamc@82 233 namesN = namesN,
adamc@82 234 rowsR = IS.map (fn n => n + 1) rowsR,
adamc@82 235 rowsN = rowsN}
adamc@82 236
adamc@82 237 fun enter {namesR, namesN, rowsR, rowsN} =
adamc@82 238 {namesR = IM.foldli (fn (n, ineqs, namesR) => IM.insert (namesR, n+1, nameEnter ineqs)) IM.empty namesR,
adamc@82 239 namesN = IM.map nameEnter namesN,
adamc@82 240 rowsR = IM.foldli (fn (n, ineqs, rowsR) => IM.insert (rowsR, n+1, rowEnter ineqs)) IM.empty rowsR,
adamc@82 241 rowsN = IM.map rowEnter rowsN}
adamc@82 242
adamc@82 243 fun getIneqs (denv : env) p =
adamc@82 244 case p of
adamc@82 245 Unknown => raise Fail "getIneqs: Unknown"
adamc@82 246 | NameC _ => raise Fail "getIneqs: NameC"
adamc@82 247 | NameR n => nameToRow_ineqs (Option.getOpt (IM.find (#namesR denv, n), name_default))
adamc@82 248 | NameN n => nameToRow_ineqs (Option.getOpt (IM.find (#namesN denv, n), name_default))
adamc@82 249 | RowR n => Option.getOpt (IM.find (#rowsR denv, n), row_default)
adamc@82 250 | RowN n => Option.getOpt (IM.find (#rowsN denv, n), row_default)
adamc@82 251
adamc@82 252 fun prove1' denv (p1, p2) =
adamc@82 253 let
adamc@82 254 val {namesC, namesR, namesN, rowsR, rowsN} = getIneqs denv p1
adamc@82 255 in
adamc@82 256 case p2 of
adamc@82 257 Unknown => raise Fail "prove1': Unknown"
adamc@82 258 | NameC s => SS.member (namesC, s)
adamc@82 259 | NameR n => IS.member (namesR, n)
adamc@82 260 | NameN n => IS.member (namesN, n)
adamc@82 261 | RowR n => IS.member (rowsR, n)
adamc@82 262 | RowN n => IS.member (rowsN, n)
adamc@82 263 end
adamc@82 264
adamc@82 265 fun prove1 denv (p1, p2) =
adamc@82 266 case (p1, p2) of
adamc@82 267 (NameC s1, NameC s2) => s1 <> s2
adamc@82 268 | (_, RowR _) => prove1' denv (p2, p1)
adamc@82 269 | (_, RowN _) => prove1' denv (p2, p1)
adamc@82 270 | _ => prove1' denv (p1, p2)
adamc@82 271
adamc@82 272 fun prove env denv (c1, c2, loc) =
adamc@82 273 let
adamc@82 274 val ps1 = decomposeRow env c1
adamc@82 275 val ps2 = decomposeRow env c2
adamc@82 276
adamc@82 277 val hasUnknown = List.exists (fn p => p = Unknown)
adamc@82 278 in
adamc@82 279 if hasUnknown ps1 orelse hasUnknown ps2 then
adamc@82 280 (ErrorMsg.errorAt loc "Structure of row is too complicated to prove disjointness";
adamc@82 281 Print.eprefaces' [("Row 1", ElabPrint.p_con env c1),
adamc@82 282 ("Row 2", ElabPrint.p_con env c2)];
adamc@82 283 [])
adamc@82 284 else
adamc@82 285 foldl (fn (p1, rem) =>
adamc@82 286 foldl (fn (p2, rem) =>
adamc@82 287 if prove1 denv (p1, p2) then
adamc@82 288 rem
adamc@82 289 else
adamc@82 290 (pieceToRow (p1, loc), pieceToRow (p2, loc)) :: rem) rem ps2)
adamc@82 291 [] ps1
adamc@82 292 end
adamc@82 293
adamc@82 294 end