Mercurial > urweb

annotate src/disjoint.sml @ 345:b85e6ba56618

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Merge CDisjoint and TDisjoint
author Adam Chlipala <adamc@hcoop.net>
date Sat, 04 Oct 2008 15:50:28 -0400
parents bc5015b89dd2
children 6ee1c761818f
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@335 146 val lowercase = CharVector.map Char.toLower
adamc@335 147
adamc@82 148 fun prove1 denv (p1, p2) =
adamc@82 149 case (p1, p2) of
adamc@335 150 ((NameC s1, _), (NameC s2, _)) => lowercase s1 <> lowercase s2
adamc@88 151 | _ =>
adamc@88 152 case PM.find (denv, p1) of
adamc@88 153 NONE => false
adamc@88 154 | SOME pset => PS.member (pset, p2)
adamc@82 155
adamc@90 156 fun decomposeRow (env, denv) c =
adamc@82 157 let
adamc@251 158 val loc = #2 c
adamc@251 159
adamc@207 160 fun decomposeProj c =
adamc@207 161 let
adamc@207 162 val (c, gs) = hnormCon (env, denv) c
adamc@207 163 in
adamc@207 164 case #1 c of
adamc@207 165 CProj (c, n) =>
adamc@207 166 let
adamc@207 167 val (c', ns, gs') = decomposeProj c
adamc@207 168 in
adamc@207 169 (c', ns @ [n], gs @ gs')
adamc@207 170 end
adamc@207 171 | _ => (c, [], gs)
adamc@207 172 end
adamc@207 173
adamc@90 174 fun decomposeName (c, (acc, gs)) =
adamc@90 175 let
adamc@207 176 val (cAll as (c, _), ns, gs') = decomposeProj c
adamc@90 177
adamc@90 178 val acc = case c of
adamc@207 179 CName s => Piece (NameC s, ns) :: acc
adamc@207 180 | CRel n => Piece (NameR n, ns) :: acc
adamc@207 181 | CNamed n => Piece (NameN n, ns) :: acc
adamc@207 182 | CModProj (m1, ms, x) => Piece (NameM (m1, ms, x), ns) :: acc
adamc@90 183 | _ => Unknown cAll :: acc
adamc@90 184 in
adamc@90 185 (acc, gs' @ gs)
adamc@90 186 end
adamc@90 187
adamc@251 188 fun decomposeRow' (c, (acc, gs)) =
adamc@90 189 let
adamc@251 190 fun default () =
adamc@251 191 let
adamc@251 192 val (cAll as (c, _), ns, gs') = decomposeProj c
adamc@251 193 val gs = gs' @ gs
adamc@251 194 in
adamc@251 195 case c of
adamc@251 196 CRecord (_, xcs) => foldl (fn ((x, _), acc_gs) => decomposeName (x, acc_gs)) (acc, gs) xcs
adamc@251 197 | CConcat (c1, c2) => decomposeRow' (c1, decomposeRow' (c2, (acc, gs)))
adamc@251 198 | CRel n => (Piece (RowR n, ns) :: acc, gs)
adamc@251 199 | CNamed n => (Piece (RowN n, ns) :: acc, gs)
adamc@251 200 | CModProj (m1, ms, x) => (Piece (RowM (m1, ms, x), ns) :: acc, gs)
adamc@251 201 | _ => (Unknown cAll :: acc, gs)
adamc@251 202 end
adamc@90 203 in
adamc@326 204 (*Print.prefaces "decomposeRow'" [("c", ElabPrint.p_con env c),
adamc@326 205 ("c'", ElabPrint.p_con env (#1 (hnormCon (env, denv) c)))];*)
adamc@251 206 case #1 (#1 (hnormCon (env, denv) c)) of
adamc@251 207 CApp (
adamc@251 208 (CApp (
adamc@251 209 (CApp ((CFold (dom, ran), _), f), _),
adamc@251 210 i), _),
adamc@251 211 r) =>
adamc@251 212 let
adamc@251 213 val (env', nm) = E.pushCNamed env "nm" (KName, loc) NONE
adamc@251 214 val (env', v) = E.pushCNamed env' "v" dom NONE
adamc@251 215 val (env', st) = E.pushCNamed env' "st" ran NONE
adamc@251 216
adamc@251 217 val (denv', gs') = assert env' denv ((CRecord (dom, [((CNamed nm, loc),
adamc@251 218 (CUnit, loc))]), loc),
adamc@251 219 (CNamed st, loc))
adamc@251 220
adamc@251 221 val c' = (CApp (f, (CNamed nm, loc)), loc)
adamc@251 222 val c' = (CApp (c', (CNamed v, loc)), loc)
adamc@251 223 val c' = (CApp (c', (CNamed st, loc)), loc)
adamc@251 224 val (ps, gs'') = decomposeRow (env', denv') c'
adamc@251 225
adamc@251 226 fun covered p =
adamc@251 227 case p of
adamc@251 228 Unknown _ => false
adamc@251 229 | Piece p =>
adamc@251 230 case p of
adamc@251 231 (NameN n, []) => n = nm
adamc@251 232 | (RowN n, []) => n = st
adamc@251 233 | _ => false
adamc@251 234
adamc@251 235 val ps = List.filter (not o covered) ps
adamc@251 236 in
adamc@251 237 decomposeRow' (i, decomposeRow' (r, (ps @ acc, gs'' @ gs' @ gs)))
adamc@251 238 end
adamc@251 239 | _ => default ()
adamc@90 240 end
adamc@90 241 in
adamc@251 242 decomposeRow' (c, ([], []))
adamc@90 243 end
adamc@90 244
adamc@90 245 and assert env denv (c1, c2) =
adamc@90 246 let
adamc@90 247 val (ps1, gs1) = decomposeRow (env, denv) c1
adamc@90 248 val (ps2, gs2) = decomposeRow (env, denv) c2
adamc@90 249
adamc@90 250 val unUnknown = List.mapPartial (fn Unknown _ => NONE | Piece p => SOME p)
adamc@90 251 val ps1 = unUnknown ps1
adamc@90 252 val ps2 = unUnknown ps2
adamc@90 253
adamc@90 254 (*val () = print "APieces1:\n"
adamc@90 255 val () = app pp ps1
adamc@90 256 val () = print "APieces2:\n"
adamc@90 257 val () = app pp ps2*)
adamc@90 258
adamc@90 259 fun assertPiece ps (p, denv) =
adamc@90 260 let
adamc@90 261 val pset = Option.getOpt (PM.find (denv, p), PS.empty)
adamc@90 262 val ps = case p of
adamc@207 263 (NameC _, _) => List.filter (fn (NameC _, _) => false | _ => true) ps
adamc@90 264 | _ => ps
adamc@90 265 val pset = PS.addList (pset, ps)
adamc@90 266 in
adamc@90 267 PM.insert (denv, p, pset)
adamc@90 268 end
adamc@90 269
adamc@90 270 val denv = foldl (assertPiece ps2) denv ps1
adamc@90 271 in
adamc@90 272 (foldl (assertPiece ps1) denv ps2, gs1 @ gs2)
adamc@90 273 end
adamc@90 274
adamc@90 275 and prove env denv (c1, c2, loc) =
adamc@90 276 let
adamc@90 277 val (ps1, gs1) = decomposeRow (env, denv) c1
adamc@90 278 val (ps2, gs2) = decomposeRow (env, denv) c2
adamc@82 279
adamc@88 280 val hasUnknown = List.exists (fn Unknown _ => true | _ => false)
adamc@88 281 val unUnknown = List.mapPartial (fn Unknown _ => NONE | Piece p => SOME p)
adamc@82 282 in
adamc@82 283 if hasUnknown ps1 orelse hasUnknown ps2 then
adamc@90 284 [(loc, env, denv, c1, c2)]
adamc@82 285 else
adamc@88 286 let
adamc@88 287 val ps1 = unUnknown ps1
adamc@88 288 val ps2 = unUnknown ps2
adamc@88 289
adamc@88 290 in
adamc@88 291 (*print "Pieces1:\n";
adamc@88 292 app pp ps1;
adamc@88 293 print "Pieces2:\n";
adamc@88 294 app pp ps2;*)
adamc@88 295
adamc@88 296 foldl (fn (p1, rem) =>
adamc@88 297 foldl (fn (p2, rem) =>
adamc@88 298 if prove1 denv (p1, p2) then
adamc@88 299 rem
adamc@88 300 else
adamc@90 301 (loc, env, denv, pieceToRow (p1, loc), pieceToRow (p2, loc)) :: rem) rem ps2)
adamc@90 302 (gs1 @ gs2) ps1
adamc@88 303 end
adamc@82 304 end
adamc@82 305
adamc@90 306 and hnormCon (env, denv) c =
adamc@90 307 let
adamc@90 308 val cAll as (c, loc) = ElabOps.hnormCon env c
adamc@90 309
adamc@90 310 fun doDisj (c1, c2, c) =
adamc@90 311 let
adamc@90 312 val (c, gs) = hnormCon (env, denv) c
adamc@90 313 in
adamc@90 314 (c, prove env denv (c1, c2, loc) @ gs)
adamc@90 315 end
adamc@90 316 in
adamc@90 317 case c of
adamc@345 318 CDisjoint (Instantiate, c1, c2, c) => doDisj (c1, c2, c)
adamc@90 319 | _ => (cAll, [])
adamc@90 320 end
adamc@90 321
adamc@82 322 end