Mercurial > urweb

annotate src/disjoint.sml @ 305:55eedecb6c50

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Remove need to mention table name in expressions for UPDATE and DELETE
author Adam Chlipala <adamc@hcoop.net>
date Sun, 07 Sep 2008 14:30:32 -0400
parents 326fb4686f60
children 950320f33232
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@207 33 datatype piece_fst =
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@207 42 type piece = piece_fst * int list
adamc@207 43
adamc@88 44 fun p2s p =
adamc@88 45 case p of
adamc@88 46 NameC s => "NameC(" ^ s ^ ")"
adamc@88 47 | NameR n => "NameR(" ^ Int.toString n ^ ")"
adamc@88 48 | NameN n => "NameN(" ^ Int.toString n ^ ")"
adamc@88 49 | NameM (n, _, s) => "NameR(" ^ Int.toString n ^ ", " ^ s ^ ")"
adamc@88 50 | RowR n => "RowR(" ^ Int.toString n ^ ")"
adamc@88 51 | RowN n => "RowN(" ^ Int.toString n ^ ")"
adamc@88 52 | RowM (n, _, s) => "RowR(" ^ Int.toString n ^ ", " ^ s ^ ")"
adamc@88 53
adamc@88 54 fun pp p = print (p2s p ^ "\n")
adamc@88 55
adamc@88 56 structure PK = struct
adamc@88 57
adamc@88 58 type ord_key = piece
adamc@88 59
adamc@207 60 open Order
adamc@88 61
adamc@207 62 fun compare' (p1, p2) =
adamc@88 63 case (p1, p2) of
adamc@88 64 (NameC s1, NameC s2) => String.compare (s1, s2)
adamc@88 65 | (NameR n1, NameR n2) => Int.compare (n1, n2)
adamc@88 66 | (NameN n1, NameN n2) => Int.compare (n1, n2)
adamc@88 67 | (NameM (n1, ss1, s1), NameM (n2, ss2, s2)) =>
adamc@88 68 join (Int.compare (n1, n2),
adamc@88 69 fn () => join (String.compare (s1, s2), fn () =>
adamc@88 70 joinL String.compare (ss1, ss2)))
adamc@88 71 | (RowR n1, RowR n2) => Int.compare (n1, n2)
adamc@88 72 | (RowN n1, RowN n2) => Int.compare (n1, n2)
adamc@88 73 | (RowM (n1, ss1, s1), RowM (n2, ss2, s2)) =>
adamc@88 74 join (Int.compare (n1, n2),
adamc@88 75 fn () => join (String.compare (s1, s2), fn () =>
adamc@88 76 joinL String.compare (ss1, ss2)))
adamc@88 77
adamc@88 78 | (NameC _, _) => LESS
adamc@88 79 | (_, NameC _) => GREATER
adamc@88 80
adamc@88 81 | (NameR _, _) => LESS
adamc@88 82 | (_, NameR _) => GREATER
adamc@88 83
adamc@88 84 | (NameN _, _) => LESS
adamc@88 85 | (_, NameN _) => GREATER
adamc@88 86
adamc@88 87 | (NameM _, _) => LESS
adamc@88 88 | (_, NameM _) => GREATER
adamc@88 89
adamc@88 90 | (RowR _, _) => LESS
adamc@88 91 | (_, RowR _) => GREATER
adamc@88 92
adamc@88 93 | (RowN _, _) => LESS
adamc@88 94 | (_, RowN _) => GREATER
adamc@88 95
adamc@207 96 fun compare ((p1, ns1), (p2, ns2)) =
adamc@207 97 join (compare' (p1, p2),
adamc@207 98 fn () => joinL Int.compare (ns1, ns2))
adamc@207 99
adamc@88 100 end
adamc@88 101
adamc@88 102 structure PS = BinarySetFn(PK)
adamc@88 103 structure PM = BinaryMapFn(PK)
adamc@88 104
adamc@88 105 type env = PS.set PM.map
adamc@88 106
adamc@251 107 structure E = ElabEnv
adamc@251 108
adamc@251 109 type goal = ErrorMsg.span * E.env * env * Elab.con * Elab.con
adamc@90 110
adamc@88 111 val empty = PM.empty
adamc@82 112
adamc@82 113 fun nameToRow (c, loc) =
adamc@82 114 (CRecord ((KUnit, loc), [((c, loc), (CUnit, loc))]), loc)
adamc@82 115
adamc@207 116 fun pieceToRow' (p, loc) =
adamc@82 117 case p of
adamc@82 118 NameC s => nameToRow (CName s, loc)
adamc@82 119 | NameR n => nameToRow (CRel n, loc)
adamc@82 120 | NameN n => nameToRow (CNamed n, loc)
adamc@88 121 | NameM (n, xs, x) => nameToRow (CModProj (n, xs, x), loc)
adamc@82 122 | RowR n => (CRel n, loc)
adamc@88 123 | RowN n => (CNamed n, loc)
adamc@88 124 | RowM (n, xs, x) => (CModProj (n, xs, x), loc)
adamc@88 125
adamc@207 126 fun pieceToRow ((p, ns), loc) =
adamc@207 127 foldl (fn (n, c) => (CProj (c, n), loc)) (pieceToRow' (p, loc)) ns
adamc@207 128
adamc@88 129 datatype piece' =
adamc@88 130 Piece of piece
adamc@88 131 | Unknown of con
adamc@82 132
adamc@207 133 fun pieceEnter' p =
adamc@88 134 case p of
adamc@88 135 NameR n => NameR (n + 1)
adamc@88 136 | RowR n => RowR (n + 1)
adamc@88 137 | _ => p
adamc@82 138
adamc@207 139 fun pieceEnter (p, n) = (pieceEnter' p, n)
adamc@207 140
adamc@88 141 fun enter denv =
adamc@88 142 PM.foldli (fn (p, pset, denv') =>
adamc@88 143 PM.insert (denv', pieceEnter p, PS.map pieceEnter pset))
adamc@88 144 PM.empty denv
adamc@82 145
adamc@82 146 fun prove1 denv (p1, p2) =
adamc@82 147 case (p1, p2) of
adamc@207 148 ((NameC s1, _), (NameC s2, _)) => s1 <> s2
adamc@88 149 | _ =>
adamc@88 150 case PM.find (denv, p1) of
adamc@88 151 NONE => false
adamc@88 152 | SOME pset => PS.member (pset, p2)
adamc@82 153
adamc@90 154 fun decomposeRow (env, denv) c =
adamc@82 155 let
adamc@251 156 val loc = #2 c
adamc@251 157
adamc@207 158 fun decomposeProj c =
adamc@207 159 let
adamc@207 160 val (c, gs) = hnormCon (env, denv) c
adamc@207 161 in
adamc@207 162 case #1 c of
adamc@207 163 CProj (c, n) =>
adamc@207 164 let
adamc@207 165 val (c', ns, gs') = decomposeProj c
adamc@207 166 in
adamc@207 167 (c', ns @ [n], gs @ gs')
adamc@207 168 end
adamc@207 169 | _ => (c, [], gs)
adamc@207 170 end
adamc@207 171
adamc@90 172 fun decomposeName (c, (acc, gs)) =
adamc@90 173 let
adamc@207 174 val (cAll as (c, _), ns, gs') = decomposeProj c
adamc@90 175
adamc@90 176 val acc = case c of
adamc@207 177 CName s => Piece (NameC s, ns) :: acc
adamc@207 178 | CRel n => Piece (NameR n, ns) :: acc
adamc@207 179 | CNamed n => Piece (NameN n, ns) :: acc
adamc@207 180 | CModProj (m1, ms, x) => Piece (NameM (m1, ms, x), ns) :: acc
adamc@90 181 | _ => Unknown cAll :: acc
adamc@90 182 in
adamc@90 183 (acc, gs' @ gs)
adamc@90 184 end
adamc@90 185
adamc@251 186 fun decomposeRow' (c, (acc, gs)) =
adamc@90 187 let
adamc@251 188 fun default () =
adamc@251 189 let
adamc@251 190 val (cAll as (c, _), ns, gs') = decomposeProj c
adamc@251 191 val gs = gs' @ gs
adamc@251 192 in
adamc@251 193 case c of
adamc@251 194 CRecord (_, xcs) => foldl (fn ((x, _), acc_gs) => decomposeName (x, acc_gs)) (acc, gs) xcs
adamc@251 195 | CConcat (c1, c2) => decomposeRow' (c1, decomposeRow' (c2, (acc, gs)))
adamc@251 196 | CRel n => (Piece (RowR n, ns) :: acc, gs)
adamc@251 197 | CNamed n => (Piece (RowN n, ns) :: acc, gs)
adamc@251 198 | CModProj (m1, ms, x) => (Piece (RowM (m1, ms, x), ns) :: acc, gs)
adamc@251 199 | _ => (Unknown cAll :: acc, gs)
adamc@251 200 end
adamc@90 201 in
adamc@251 202 case #1 (#1 (hnormCon (env, denv) c)) of
adamc@251 203 CApp (
adamc@251 204 (CApp (
adamc@251 205 (CApp ((CFold (dom, ran), _), f), _),
adamc@251 206 i), _),
adamc@251 207 r) =>
adamc@251 208 let
adamc@251 209 val (env', nm) = E.pushCNamed env "nm" (KName, loc) NONE
adamc@251 210 val (env', v) = E.pushCNamed env' "v" dom NONE
adamc@251 211 val (env', st) = E.pushCNamed env' "st" ran NONE
adamc@251 212
adamc@251 213 val (denv', gs') = assert env' denv ((CRecord (dom, [((CNamed nm, loc),
adamc@251 214 (CUnit, loc))]), loc),
adamc@251 215 (CNamed st, loc))
adamc@251 216
adamc@251 217 val c' = (CApp (f, (CNamed nm, loc)), loc)
adamc@251 218 val c' = (CApp (c', (CNamed v, loc)), loc)
adamc@251 219 val c' = (CApp (c', (CNamed st, loc)), loc)
adamc@251 220 val (ps, gs'') = decomposeRow (env', denv') c'
adamc@251 221
adamc@251 222 fun covered p =
adamc@251 223 case p of
adamc@251 224 Unknown _ => false
adamc@251 225 | Piece p =>
adamc@251 226 case p of
adamc@251 227 (NameN n, []) => n = nm
adamc@251 228 | (RowN n, []) => n = st
adamc@251 229 | _ => false
adamc@251 230
adamc@251 231 val ps = List.filter (not o covered) ps
adamc@251 232 in
adamc@251 233 decomposeRow' (i, decomposeRow' (r, (ps @ acc, gs'' @ gs' @ gs)))
adamc@251 234 end
adamc@251 235 | _ => default ()
adamc@90 236 end
adamc@90 237 in
adamc@251 238 decomposeRow' (c, ([], []))
adamc@90 239 end
adamc@90 240
adamc@90 241 and assert env denv (c1, c2) =
adamc@90 242 let
adamc@90 243 val (ps1, gs1) = decomposeRow (env, denv) c1
adamc@90 244 val (ps2, gs2) = decomposeRow (env, denv) c2
adamc@90 245
adamc@90 246 val unUnknown = List.mapPartial (fn Unknown _ => NONE | Piece p => SOME p)
adamc@90 247 val ps1 = unUnknown ps1
adamc@90 248 val ps2 = unUnknown ps2
adamc@90 249
adamc@90 250 (*val () = print "APieces1:\n"
adamc@90 251 val () = app pp ps1
adamc@90 252 val () = print "APieces2:\n"
adamc@90 253 val () = app pp ps2*)
adamc@90 254
adamc@90 255 fun assertPiece ps (p, denv) =
adamc@90 256 let
adamc@90 257 val pset = Option.getOpt (PM.find (denv, p), PS.empty)
adamc@90 258 val ps = case p of
adamc@207 259 (NameC _, _) => List.filter (fn (NameC _, _) => false | _ => true) ps
adamc@90 260 | _ => ps
adamc@90 261 val pset = PS.addList (pset, ps)
adamc@90 262 in
adamc@90 263 PM.insert (denv, p, pset)
adamc@90 264 end
adamc@90 265
adamc@90 266 val denv = foldl (assertPiece ps2) denv ps1
adamc@90 267 in
adamc@90 268 (foldl (assertPiece ps1) denv ps2, gs1 @ gs2)
adamc@90 269 end
adamc@90 270
adamc@90 271 and prove env denv (c1, c2, loc) =
adamc@90 272 let
adamc@90 273 val (ps1, gs1) = decomposeRow (env, denv) c1
adamc@90 274 val (ps2, gs2) = decomposeRow (env, denv) c2
adamc@82 275
adamc@88 276 val hasUnknown = List.exists (fn Unknown _ => true | _ => false)
adamc@88 277 val unUnknown = List.mapPartial (fn Unknown _ => NONE | Piece p => SOME p)
adamc@82 278 in
adamc@82 279 if hasUnknown ps1 orelse hasUnknown ps2 then
adamc@90 280 [(loc, env, denv, c1, c2)]
adamc@82 281 else
adamc@88 282 let
adamc@88 283 val ps1 = unUnknown ps1
adamc@88 284 val ps2 = unUnknown ps2
adamc@88 285
adamc@88 286 in
adamc@88 287 (*print "Pieces1:\n";
adamc@88 288 app pp ps1;
adamc@88 289 print "Pieces2:\n";
adamc@88 290 app pp ps2;*)
adamc@88 291
adamc@88 292 foldl (fn (p1, rem) =>
adamc@88 293 foldl (fn (p2, rem) =>
adamc@88 294 if prove1 denv (p1, p2) then
adamc@88 295 rem
adamc@88 296 else
adamc@90 297 (loc, env, denv, pieceToRow (p1, loc), pieceToRow (p2, loc)) :: rem) rem ps2)
adamc@90 298 (gs1 @ gs2) ps1
adamc@88 299 end
adamc@82 300 end
adamc@82 301
adamc@90 302 and hnormCon (env, denv) c =
adamc@90 303 let
adamc@90 304 val cAll as (c, loc) = ElabOps.hnormCon env c
adamc@90 305
adamc@90 306 fun doDisj (c1, c2, c) =
adamc@90 307 let
adamc@90 308 val (c, gs) = hnormCon (env, denv) c
adamc@90 309 in
adamc@90 310 (c, prove env denv (c1, c2, loc) @ gs)
adamc@90 311 end
adamc@90 312 in
adamc@90 313 case c of
adamc@90 314 CDisjoint cs => doDisj cs
adamc@90 315 | TDisjoint cs => doDisj cs
adamc@90 316 | _ => (cAll, [])
adamc@90 317 end
adamc@90 318
adamc@82 319 end