Mercurial > urweb

annotate src/disjoint.sml @ 88:7bab29834cd6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Constraints in modules
author Adam Chlipala <adamc@hcoop.net>
date Tue, 01 Jul 2008 15:58:02 -0400
parents e86370850c30
children 94ef20a31550
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 datatype piece =
adamc@82 34 NameC of string
adamc@82 35 | NameR of int
adamc@82 36 | NameN of int
adamc@88 37 | NameM of int * string list * string
adamc@82 38 | RowR of int
adamc@82 39 | RowN of int
adamc@88 40 | RowM of int * string list * string
adamc@88 41
adamc@88 42 fun p2s p =
adamc@88 43 case p of
adamc@88 44 NameC s => "NameC(" ^ s ^ ")"
adamc@88 45 | NameR n => "NameR(" ^ Int.toString n ^ ")"
adamc@88 46 | NameN n => "NameN(" ^ Int.toString n ^ ")"
adamc@88 47 | NameM (n, _, s) => "NameR(" ^ Int.toString n ^ ", " ^ s ^ ")"
adamc@88 48 | RowR n => "RowR(" ^ Int.toString n ^ ")"
adamc@88 49 | RowN n => "RowN(" ^ Int.toString n ^ ")"
adamc@88 50 | RowM (n, _, s) => "RowR(" ^ Int.toString n ^ ", " ^ s ^ ")"
adamc@88 51
adamc@88 52 fun pp p = print (p2s p ^ "\n")
adamc@88 53
adamc@88 54 structure PK = struct
adamc@88 55
adamc@88 56 type ord_key = piece
adamc@88 57
adamc@88 58 fun join (o1, o2) =
adamc@88 59 case o1 of
adamc@88 60 EQUAL => o2 ()
adamc@88 61 | v => v
adamc@88 62
adamc@88 63 fun joinL f (os1, os2) =
adamc@88 64 case (os1, os2) of
adamc@88 65 (nil, nil) => EQUAL
adamc@88 66 | (nil, _) => LESS
adamc@88 67 | (h1 :: t1, h2 :: t2) =>
adamc@88 68 join (f (h1, h2), fn () => joinL f (t1, t2))
adamc@88 69 | (_ :: _, nil) => GREATER
adamc@88 70
adamc@88 71 fun compare (p1, p2) =
adamc@88 72 case (p1, p2) of
adamc@88 73 (NameC s1, NameC s2) => String.compare (s1, s2)
adamc@88 74 | (NameR n1, NameR n2) => Int.compare (n1, n2)
adamc@88 75 | (NameN n1, NameN n2) => Int.compare (n1, n2)
adamc@88 76 | (NameM (n1, ss1, s1), NameM (n2, ss2, s2)) =>
adamc@88 77 join (Int.compare (n1, n2),
adamc@88 78 fn () => join (String.compare (s1, s2), fn () =>
adamc@88 79 joinL String.compare (ss1, ss2)))
adamc@88 80 | (RowR n1, RowR n2) => Int.compare (n1, n2)
adamc@88 81 | (RowN n1, RowN n2) => Int.compare (n1, n2)
adamc@88 82 | (RowM (n1, ss1, s1), RowM (n2, ss2, s2)) =>
adamc@88 83 join (Int.compare (n1, n2),
adamc@88 84 fn () => join (String.compare (s1, s2), fn () =>
adamc@88 85 joinL String.compare (ss1, ss2)))
adamc@88 86
adamc@88 87 | (NameC _, _) => LESS
adamc@88 88 | (_, NameC _) => GREATER
adamc@88 89
adamc@88 90 | (NameR _, _) => LESS
adamc@88 91 | (_, NameR _) => GREATER
adamc@88 92
adamc@88 93 | (NameN _, _) => LESS
adamc@88 94 | (_, NameN _) => GREATER
adamc@88 95
adamc@88 96 | (NameM _, _) => LESS
adamc@88 97 | (_, NameM _) => GREATER
adamc@88 98
adamc@88 99 | (RowR _, _) => LESS
adamc@88 100 | (_, RowR _) => GREATER
adamc@88 101
adamc@88 102 | (RowN _, _) => LESS
adamc@88 103 | (_, RowN _) => GREATER
adamc@88 104
adamc@88 105 end
adamc@88 106
adamc@88 107 structure PS = BinarySetFn(PK)
adamc@88 108 structure PM = BinaryMapFn(PK)
adamc@88 109
adamc@88 110 type env = PS.set PM.map
adamc@88 111
adamc@88 112 val empty = PM.empty
adamc@82 113
adamc@82 114 fun nameToRow (c, loc) =
adamc@82 115 (CRecord ((KUnit, loc), [((c, loc), (CUnit, loc))]), loc)
adamc@82 116
adamc@82 117 fun pieceToRow (p, loc) =
adamc@82 118 case p of
adamc@82 119 NameC s => nameToRow (CName s, loc)
adamc@82 120 | NameR n => nameToRow (CRel n, loc)
adamc@82 121 | NameN n => nameToRow (CNamed n, loc)
adamc@88 122 | NameM (n, xs, x) => nameToRow (CModProj (n, xs, x), loc)
adamc@82 123 | RowR n => (CRel n, loc)
adamc@88 124 | RowN n => (CNamed n, loc)
adamc@88 125 | RowM (n, xs, x) => (CModProj (n, xs, x), loc)
adamc@88 126
adamc@88 127 datatype piece' =
adamc@88 128 Piece of piece
adamc@88 129 | Unknown of con
adamc@82 130
adamc@82 131 fun decomposeRow env c =
adamc@82 132 let
adamc@82 133 fun decomposeName (c, acc) =
adamc@82 134 case #1 (hnormCon env c) of
adamc@88 135 CName s => Piece (NameC s) :: acc
adamc@88 136 | CRel n => Piece (NameR n) :: acc
adamc@88 137 | CNamed n => Piece (NameN n) :: acc
adamc@88 138 | CModProj (m1, ms, x) => Piece (NameM (m1, ms, x)) :: acc
adamc@88 139 | _ => Unknown c :: acc
adamc@88 140
adamc@82 141 fun decomposeRow (c, acc) =
adamc@82 142 case #1 (hnormCon env c) of
adamc@82 143 CRecord (_, xcs) => foldl (fn ((x, _), acc) => decomposeName (x, acc)) acc xcs
adamc@82 144 | CConcat (c1, c2) => decomposeRow (c1, decomposeRow (c2, acc))
adamc@88 145 | CRel n => Piece (RowR n) :: acc
adamc@88 146 | CNamed n => Piece (RowN n) :: acc
adamc@88 147 | CModProj (m1, ms, x) => Piece (RowM (m1, ms, x)) :: acc
adamc@88 148 | _ => Unknown c :: acc
adamc@82 149 in
adamc@82 150 decomposeRow (c, [])
adamc@82 151 end
adamc@82 152
adamc@82 153 fun assert env denv (c1, c2) =
adamc@82 154 let
adamc@82 155 val ps1 = decomposeRow env c1
adamc@82 156 val ps2 = decomposeRow env c2
adamc@82 157
adamc@88 158 val unUnknown = List.mapPartial (fn Unknown _ => NONE | Piece p => SOME p)
adamc@88 159 val ps1 = unUnknown ps1
adamc@88 160 val ps2 = unUnknown ps2
adamc@88 161
adamc@88 162 (*val () = print "APieces1:\n"
adamc@88 163 val () = app pp ps1
adamc@88 164 val () = print "APieces2:\n"
adamc@88 165 val () = app pp ps2*)
adamc@88 166
adamc@88 167 fun assertPiece ps (p, denv) =
adamc@88 168 let
adamc@88 169 val pset = Option.getOpt (PM.find (denv, p), PS.empty)
adamc@88 170 val pset = PS.addList (pset, ps)
adamc@88 171 in
adamc@88 172 PM.insert (denv, p, pset)
adamc@88 173 end
adamc@88 174
adamc@82 175 val denv = foldl (assertPiece ps2) denv ps1
adamc@82 176 in
adamc@82 177 foldl (assertPiece ps1) denv ps2
adamc@82 178 end
adamc@82 179
adamc@88 180 fun pieceEnter p =
adamc@88 181 case p of
adamc@88 182 NameR n => NameR (n + 1)
adamc@88 183 | RowR n => RowR (n + 1)
adamc@88 184 | _ => p
adamc@82 185
adamc@88 186 fun enter denv =
adamc@88 187 PM.foldli (fn (p, pset, denv') =>
adamc@88 188 PM.insert (denv', pieceEnter p, PS.map pieceEnter pset))
adamc@88 189 PM.empty denv
adamc@82 190
adamc@82 191 fun prove1 denv (p1, p2) =
adamc@82 192 case (p1, p2) of
adamc@82 193 (NameC s1, NameC s2) => s1 <> s2
adamc@88 194 | _ =>
adamc@88 195 case PM.find (denv, p1) of
adamc@88 196 NONE => false
adamc@88 197 | SOME pset => PS.member (pset, p2)
adamc@82 198
adamc@82 199 fun prove env denv (c1, c2, loc) =
adamc@82 200 let
adamc@82 201 val ps1 = decomposeRow env c1
adamc@82 202 val ps2 = decomposeRow env c2
adamc@82 203
adamc@88 204 val hasUnknown = List.exists (fn Unknown _ => true | _ => false)
adamc@88 205 val unUnknown = List.mapPartial (fn Unknown _ => NONE | Piece p => SOME p)
adamc@82 206 in
adamc@82 207 if hasUnknown ps1 orelse hasUnknown ps2 then
adamc@83 208 [(c1, c2)]
adamc@82 209 else
adamc@88 210 let
adamc@88 211 val ps1 = unUnknown ps1
adamc@88 212 val ps2 = unUnknown ps2
adamc@88 213
adamc@88 214 in
adamc@88 215 (*print "Pieces1:\n";
adamc@88 216 app pp ps1;
adamc@88 217 print "Pieces2:\n";
adamc@88 218 app pp ps2;*)
adamc@88 219
adamc@88 220 foldl (fn (p1, rem) =>
adamc@88 221 foldl (fn (p2, rem) =>
adamc@88 222 if prove1 denv (p1, p2) then
adamc@88 223 rem
adamc@88 224 else
adamc@88 225 (pieceToRow (p1, loc), pieceToRow (p2, loc)) :: rem) rem ps2)
adamc@88 226 [] ps1
adamc@88 227 end
adamc@82 228 end
adamc@82 229
adamc@82 230 end