Mercurial > urweb

annotate src/disjoint.sml @ 1736:7ec8dab190a7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Better discovery of type class instances from recursive definitions
author Adam Chlipala <adam@chlipala.net>
date Wed, 02 May 2012 08:34:50 -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