Mercurial > urweb

annotate src/disjoint.sml @ 1726:4df4521fbd3b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Removed excess zero byte from empty pages. Zero byte sometimes breaks http tunneling in Safari. Empty page is a "Not Modified" response for app.js
author Vladimir Shabanov <vshabanoff@gmail.com>
date Wed, 25 Apr 2012 03:07:07 +0400
parents a779402841f6
children
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@478 56 fun rp2s (p, ns) = String.concatWith " " (p2s p :: map Int.toString ns)
adamc@478 57
adamc@88 58 structure PK = struct
adamc@88 59
adamc@88 60 type ord_key = piece
adamc@88 61
adamc@207 62 open Order
adamc@88 63
adamc@207 64 fun compare' (p1, p2) =
adamc@88 65 case (p1, p2) of
adamc@88 66 (NameC s1, NameC s2) => String.compare (s1, s2)
adamc@88 67 | (NameR n1, NameR n2) => Int.compare (n1, n2)
adamc@88 68 | (NameN n1, NameN n2) => Int.compare (n1, n2)
adamc@88 69 | (NameM (n1, ss1, s1), NameM (n2, ss2, s2)) =>
adamc@88 70 join (Int.compare (n1, n2),
adamc@88 71 fn () => join (String.compare (s1, s2), fn () =>
adamc@88 72 joinL String.compare (ss1, ss2)))
adamc@88 73 | (RowR n1, RowR n2) => Int.compare (n1, n2)
adamc@88 74 | (RowN n1, RowN n2) => Int.compare (n1, n2)
adamc@88 75 | (RowM (n1, ss1, s1), RowM (n2, ss2, s2)) =>
adamc@88 76 join (Int.compare (n1, n2),
adamc@88 77 fn () => join (String.compare (s1, s2), fn () =>
adamc@88 78 joinL String.compare (ss1, ss2)))
adamc@88 79
adamc@88 80 | (NameC _, _) => LESS
adamc@88 81 | (_, NameC _) => GREATER
adamc@88 82
adamc@88 83 | (NameR _, _) => LESS
adamc@88 84 | (_, NameR _) => GREATER
adamc@88 85
adamc@88 86 | (NameN _, _) => LESS
adamc@88 87 | (_, NameN _) => GREATER
adamc@88 88
adamc@88 89 | (NameM _, _) => LESS
adamc@88 90 | (_, NameM _) => GREATER
adamc@88 91
adamc@88 92 | (RowR _, _) => LESS
adamc@88 93 | (_, RowR _) => GREATER
adamc@88 94
adamc@88 95 | (RowN _, _) => LESS
adamc@88 96 | (_, RowN _) => GREATER
adamc@88 97
adamc@207 98 fun compare ((p1, ns1), (p2, ns2)) =
adamc@207 99 join (compare' (p1, p2),
adamc@207 100 fn () => joinL Int.compare (ns1, ns2))
adamc@207 101
adamc@88 102 end
adamc@88 103
adamc@88 104 structure PS = BinarySetFn(PK)
adamc@88 105 structure PM = BinaryMapFn(PK)
adamc@88 106
adamc@88 107 type env = PS.set PM.map
adamc@88 108
adamc@478 109 fun p_env x =
adamc@478 110 (print "\nDENV:\n";
adamc@478 111 PM.appi (fn (p1, ps) =>
adamc@478 112 PS.app (fn p2 =>
adamc@478 113 print (rp2s p1 ^ " ~ " ^ rp2s p2 ^ "\n")) ps) x)
adamc@478 114
adamc@251 115 structure E = ElabEnv
adamc@251 116
adamc@251 117 type goal = ErrorMsg.span * E.env * env * Elab.con * Elab.con
adamc@90 118
adamc@88 119 val empty = PM.empty
adamc@82 120
adamc@82 121 fun nameToRow (c, loc) =
adamc@82 122 (CRecord ((KUnit, loc), [((c, loc), (CUnit, loc))]), loc)
adamc@82 123
adamc@207 124 fun pieceToRow' (p, loc) =
adamc@82 125 case p of
adamc@82 126 NameC s => nameToRow (CName s, loc)
adamc@82 127 | NameR n => nameToRow (CRel n, loc)
adamc@82 128 | NameN n => nameToRow (CNamed n, loc)
adamc@88 129 | NameM (n, xs, x) => nameToRow (CModProj (n, xs, x), loc)
adamc@82 130 | RowR n => (CRel n, loc)
adamc@88 131 | RowN n => (CNamed n, loc)
adamc@88 132 | RowM (n, xs, x) => (CModProj (n, xs, x), loc)
adamc@88 133
adamc@207 134 fun pieceToRow ((p, ns), loc) =
adamc@207 135 foldl (fn (n, c) => (CProj (c, n), loc)) (pieceToRow' (p, loc)) ns
adamc@207 136
adamc@88 137 datatype piece' =
adamc@88 138 Piece of piece
adamc@88 139 | Unknown of con
adamc@82 140
adamc@207 141 fun pieceEnter' p =
adamc@88 142 case p of
adamc@88 143 NameR n => NameR (n + 1)
adamc@88 144 | RowR n => RowR (n + 1)
adamc@88 145 | _ => p
adamc@82 146
adamc@207 147 fun pieceEnter (p, n) = (pieceEnter' p, n)
adamc@207 148
adamc@88 149 fun enter denv =
adamc@88 150 PM.foldli (fn (p, pset, denv') =>
adamc@88 151 PM.insert (denv', pieceEnter p, PS.map pieceEnter pset))
adamc@88 152 PM.empty denv
adamc@82 153
adamc@335 154 val lowercase = CharVector.map Char.toLower
adamc@335 155
adamc@82 156 fun prove1 denv (p1, p2) =
adamc@82 157 case (p1, p2) of
adamc@335 158 ((NameC s1, _), (NameC s2, _)) => lowercase s1 <> lowercase s2
adamc@88 159 | _ =>
adamc@88 160 case PM.find (denv, p1) of
adamc@88 161 NONE => false
adamc@88 162 | SOME pset => PS.member (pset, p2)
adamc@82 163
adamc@1034 164 val proved = ref 0
adamc@1034 165 fun reset () = (ElabOps.reset ();
adamc@1034 166 proved := 0)
adamc@1034 167
adamc@628 168 fun decomposeRow env c =
adamc@82 169 let
adamc@251 170 val loc = #2 c
adamc@251 171
adamc@207 172 fun decomposeProj c =
adamc@207 173 let
adamc@628 174 val c = hnormCon env c
adamc@207 175 in
adamc@207 176 case #1 c of
adamc@207 177 CProj (c, n) =>
adamc@207 178 let
adamc@628 179 val (c', ns) = decomposeProj c
adamc@207 180 in
adamc@628 181 (c', ns @ [n])
adamc@207 182 end
adamc@628 183 | _ => (c, [])
adamc@207 184 end
adamc@207 185
adamc@628 186 fun decomposeName (c, acc) =
adamc@90 187 let
adamc@628 188 val (cAll as (c, _), ns) = decomposeProj c
adamc@90 189 in
adamc@628 190 case c of
adamc@628 191 CName s => Piece (NameC s, ns) :: acc
adamc@628 192 | CRel n => Piece (NameR n, ns) :: acc
adamc@628 193 | CNamed n => Piece (NameN n, ns) :: acc
adamc@628 194 | CModProj (m1, ms, x) => Piece (NameM (m1, ms, x), ns) :: acc
adamc@628 195 | _ => Unknown cAll :: acc
adamc@90 196 end
adamc@90 197
adamc@628 198 fun decomposeRow' (c, acc) =
adamc@90 199 let
adamc@251 200 fun default () =
adamc@251 201 let
adamc@628 202 val (cAll as (c, _), ns) = decomposeProj c
adamc@251 203 in
adamc@251 204 case c of
adamc@628 205 CRecord (_, xcs) => foldl (fn ((x, _), acc) => decomposeName (x, acc)) acc xcs
adamc@628 206 | CConcat (c1, c2) => decomposeRow' (c1, decomposeRow' (c2, acc))
adamc@628 207 | CRel n => Piece (RowR n, ns) :: acc
adamc@628 208 | CNamed n => Piece (RowN n, ns) :: acc
adamc@628 209 | CModProj (m1, ms, x) => Piece (RowM (m1, ms, x), ns) :: acc
adamc@628 210 | _ => Unknown cAll :: acc
adamc@251 211 end
adamc@90 212 in
adamc@628 213 case #1 (hnormCon env c) of
adamc@251 214 CApp (
adamc@621 215 (CApp ((CMap _, _), _), _),
adamc@628 216 r) => decomposeRow' (r, acc)
adamc@251 217 | _ => default ()
adamc@90 218 end
adamc@90 219 in
adamc@628 220 decomposeRow' (c, [])
adamc@90 221 end
adamc@90 222
adamc@90 223 and assert env denv (c1, c2) =
adamc@90 224 let
adamc@628 225 val ps1 = decomposeRow env c1
adamc@628 226 val ps2 = decomposeRow env c2
adamc@90 227
adamc@90 228 val unUnknown = List.mapPartial (fn Unknown _ => NONE | Piece p => SOME p)
adamc@90 229 val ps1 = unUnknown ps1
adamc@90 230 val ps2 = unUnknown ps2
adamc@90 231
adamc@90 232 (*val () = print "APieces1:\n"
adamc@90 233 val () = app pp ps1
adamc@90 234 val () = print "APieces2:\n"
adamc@90 235 val () = app pp ps2*)
adamc@90 236
adamc@90 237 fun assertPiece ps (p, denv) =
adamc@90 238 let
adamc@90 239 val pset = Option.getOpt (PM.find (denv, p), PS.empty)
adamc@90 240 val ps = case p of
adamc@207 241 (NameC _, _) => List.filter (fn (NameC _, _) => false | _ => true) ps
adamc@90 242 | _ => ps
adamc@90 243 val pset = PS.addList (pset, ps)
adamc@90 244 in
adamc@90 245 PM.insert (denv, p, pset)
adamc@90 246 end
adamc@90 247
adamc@90 248 val denv = foldl (assertPiece ps2) denv ps1
adamc@90 249 in
adamc@628 250 foldl (assertPiece ps1) denv ps2
adamc@90 251 end
adamc@90 252
adamc@90 253 and prove env denv (c1, c2, loc) =
adamc@90 254 let
adamc@1034 255 val () = proved := !proved + 1
adamc@628 256 val ps1 = decomposeRow env c1
adamc@628 257 val ps2 = decomposeRow env c2
adamc@82 258
adamc@88 259 val hasUnknown = List.exists (fn Unknown _ => true | _ => false)
adamc@88 260 val unUnknown = List.mapPartial (fn Unknown _ => NONE | Piece p => SOME p)
adamc@82 261 in
adamc@709 262 if (hasUnknown ps1 andalso not (List.null ps2))
adamc@709 263 orelse (hasUnknown ps2 andalso not (List.null ps1)) then
adamc@90 264 [(loc, env, denv, c1, c2)]
adamc@82 265 else
adamc@88 266 let
adamc@88 267 val ps1 = unUnknown ps1
adamc@88 268 val ps2 = unUnknown ps2
adamc@88 269 in
adamc@88 270 (*print "Pieces1:\n";
adamc@88 271 app pp ps1;
adamc@88 272 print "Pieces2:\n";
adamc@88 273 app pp ps2;*)
adamc@88 274
adamc@88 275 foldl (fn (p1, rem) =>
adamc@88 276 foldl (fn (p2, rem) =>
adamc@88 277 if prove1 denv (p1, p2) then
adamc@88 278 rem
adamc@88 279 else
adamc@90 280 (loc, env, denv, pieceToRow (p1, loc), pieceToRow (p2, loc)) :: rem) rem ps2)
adamc@628 281 [] ps1
adamc@88 282 end
adamc@82 283 end
adamc@82 284
adamc@82 285 end