adamc@82: (* Copyright (c) 2008, Adam Chlipala adamc@82: * All rights reserved. adamc@82: * adamc@82: * Redistribution and use in source and binary forms, with or without adamc@82: * modification, are permitted provided that the following conditions are met: adamc@82: * adamc@82: * - Redistributions of source code must retain the above copyright notice, adamc@82: * this list of conditions and the following disclaimer. adamc@82: * - Redistributions in binary form must reproduce the above copyright notice, adamc@82: * this list of conditions and the following disclaimer in the documentation adamc@82: * and/or other materials provided with the distribution. adamc@82: * - The names of contributors may not be used to endorse or promote products adamc@82: * derived from this software without specific prior written permission. adamc@82: * adamc@82: * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" adamc@82: * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE adamc@82: * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE adamc@82: * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE adamc@82: * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR adamc@82: * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF adamc@82: * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS adamc@82: * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN adamc@82: * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) adamc@82: * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE adamc@82: * POSSIBILITY OF SUCH DAMAGE. adamc@82: *) adamc@82: adamc@82: structure Disjoint :> DISJOINT = struct adamc@82: adamc@82: open Elab adamc@82: open ElabOps adamc@82: adamc@207: datatype piece_fst = adamc@82: NameC of string adamc@82: | NameR of int adamc@82: | NameN of int adamc@88: | NameM of int * string list * string adamc@82: | RowR of int adamc@82: | RowN of int adamc@88: | RowM of int * string list * string adamc@88: adamc@207: type piece = piece_fst * int list adamc@207: adamc@88: fun p2s p = adamc@88: case p of adamc@88: NameC s => "NameC(" ^ s ^ ")" adamc@88: | NameR n => "NameR(" ^ Int.toString n ^ ")" adamc@88: | NameN n => "NameN(" ^ Int.toString n ^ ")" adamc@88: | NameM (n, _, s) => "NameR(" ^ Int.toString n ^ ", " ^ s ^ ")" adamc@88: | RowR n => "RowR(" ^ Int.toString n ^ ")" adamc@88: | RowN n => "RowN(" ^ Int.toString n ^ ")" adamc@88: | RowM (n, _, s) => "RowR(" ^ Int.toString n ^ ", " ^ s ^ ")" adamc@88: adamc@88: fun pp p = print (p2s p ^ "\n") adamc@88: adamc@88: structure PK = struct adamc@88: adamc@88: type ord_key = piece adamc@88: adamc@207: open Order adamc@88: adamc@207: fun compare' (p1, p2) = adamc@88: case (p1, p2) of adamc@88: (NameC s1, NameC s2) => String.compare (s1, s2) adamc@88: | (NameR n1, NameR n2) => Int.compare (n1, n2) adamc@88: | (NameN n1, NameN n2) => Int.compare (n1, n2) adamc@88: | (NameM (n1, ss1, s1), NameM (n2, ss2, s2)) => adamc@88: join (Int.compare (n1, n2), adamc@88: fn () => join (String.compare (s1, s2), fn () => adamc@88: joinL String.compare (ss1, ss2))) adamc@88: | (RowR n1, RowR n2) => Int.compare (n1, n2) adamc@88: | (RowN n1, RowN n2) => Int.compare (n1, n2) adamc@88: | (RowM (n1, ss1, s1), RowM (n2, ss2, s2)) => adamc@88: join (Int.compare (n1, n2), adamc@88: fn () => join (String.compare (s1, s2), fn () => adamc@88: joinL String.compare (ss1, ss2))) adamc@88: adamc@88: | (NameC _, _) => LESS adamc@88: | (_, NameC _) => GREATER adamc@88: adamc@88: | (NameR _, _) => LESS adamc@88: | (_, NameR _) => GREATER adamc@88: adamc@88: | (NameN _, _) => LESS adamc@88: | (_, NameN _) => GREATER adamc@88: adamc@88: | (NameM _, _) => LESS adamc@88: | (_, NameM _) => GREATER adamc@88: adamc@88: | (RowR _, _) => LESS adamc@88: | (_, RowR _) => GREATER adamc@88: adamc@88: | (RowN _, _) => LESS adamc@88: | (_, RowN _) => GREATER adamc@88: adamc@207: fun compare ((p1, ns1), (p2, ns2)) = adamc@207: join (compare' (p1, p2), adamc@207: fn () => joinL Int.compare (ns1, ns2)) adamc@207: adamc@88: end adamc@88: adamc@88: structure PS = BinarySetFn(PK) adamc@88: structure PM = BinaryMapFn(PK) adamc@88: adamc@88: type env = PS.set PM.map adamc@88: adamc@251: structure E = ElabEnv adamc@251: adamc@251: type goal = ErrorMsg.span * E.env * env * Elab.con * Elab.con adamc@90: adamc@88: val empty = PM.empty adamc@82: adamc@82: fun nameToRow (c, loc) = adamc@82: (CRecord ((KUnit, loc), [((c, loc), (CUnit, loc))]), loc) adamc@82: adamc@207: fun pieceToRow' (p, loc) = adamc@82: case p of adamc@82: NameC s => nameToRow (CName s, loc) adamc@82: | NameR n => nameToRow (CRel n, loc) adamc@82: | NameN n => nameToRow (CNamed n, loc) adamc@88: | NameM (n, xs, x) => nameToRow (CModProj (n, xs, x), loc) adamc@82: | RowR n => (CRel n, loc) adamc@88: | RowN n => (CNamed n, loc) adamc@88: | RowM (n, xs, x) => (CModProj (n, xs, x), loc) adamc@88: adamc@207: fun pieceToRow ((p, ns), loc) = adamc@207: foldl (fn (n, c) => (CProj (c, n), loc)) (pieceToRow' (p, loc)) ns adamc@207: adamc@88: datatype piece' = adamc@88: Piece of piece adamc@88: | Unknown of con adamc@82: adamc@207: fun pieceEnter' p = adamc@88: case p of adamc@88: NameR n => NameR (n + 1) adamc@88: | RowR n => RowR (n + 1) adamc@88: | _ => p adamc@82: adamc@207: fun pieceEnter (p, n) = (pieceEnter' p, n) adamc@207: adamc@88: fun enter denv = adamc@88: PM.foldli (fn (p, pset, denv') => adamc@88: PM.insert (denv', pieceEnter p, PS.map pieceEnter pset)) adamc@88: PM.empty denv adamc@82: adamc@82: fun prove1 denv (p1, p2) = adamc@82: case (p1, p2) of adamc@207: ((NameC s1, _), (NameC s2, _)) => s1 <> s2 adamc@88: | _ => adamc@88: case PM.find (denv, p1) of adamc@88: NONE => false adamc@88: | SOME pset => PS.member (pset, p2) adamc@82: adamc@90: fun decomposeRow (env, denv) c = adamc@82: let adamc@251: val loc = #2 c adamc@251: adamc@207: fun decomposeProj c = adamc@207: let adamc@207: val (c, gs) = hnormCon (env, denv) c adamc@207: in adamc@207: case #1 c of adamc@207: CProj (c, n) => adamc@207: let adamc@207: val (c', ns, gs') = decomposeProj c adamc@207: in adamc@207: (c', ns @ [n], gs @ gs') adamc@207: end adamc@207: | _ => (c, [], gs) adamc@207: end adamc@207: adamc@90: fun decomposeName (c, (acc, gs)) = adamc@90: let adamc@207: val (cAll as (c, _), ns, gs') = decomposeProj c adamc@90: adamc@90: val acc = case c of adamc@207: CName s => Piece (NameC s, ns) :: acc adamc@207: | CRel n => Piece (NameR n, ns) :: acc adamc@207: | CNamed n => Piece (NameN n, ns) :: acc adamc@207: | CModProj (m1, ms, x) => Piece (NameM (m1, ms, x), ns) :: acc adamc@90: | _ => Unknown cAll :: acc adamc@90: in adamc@90: (acc, gs' @ gs) adamc@90: end adamc@90: adamc@251: fun decomposeRow' (c, (acc, gs)) = adamc@90: let adamc@251: fun default () = adamc@251: let adamc@251: val (cAll as (c, _), ns, gs') = decomposeProj c adamc@251: val gs = gs' @ gs adamc@251: in adamc@251: case c of adamc@251: CRecord (_, xcs) => foldl (fn ((x, _), acc_gs) => decomposeName (x, acc_gs)) (acc, gs) xcs adamc@251: | CConcat (c1, c2) => decomposeRow' (c1, decomposeRow' (c2, (acc, gs))) adamc@251: | CRel n => (Piece (RowR n, ns) :: acc, gs) adamc@251: | CNamed n => (Piece (RowN n, ns) :: acc, gs) adamc@251: | CModProj (m1, ms, x) => (Piece (RowM (m1, ms, x), ns) :: acc, gs) adamc@251: | _ => (Unknown cAll :: acc, gs) adamc@251: end adamc@90: in adamc@251: case #1 (#1 (hnormCon (env, denv) c)) of adamc@251: CApp ( adamc@251: (CApp ( adamc@251: (CApp ((CFold (dom, ran), _), f), _), adamc@251: i), _), adamc@251: r) => adamc@251: let adamc@251: val (env', nm) = E.pushCNamed env "nm" (KName, loc) NONE adamc@251: val (env', v) = E.pushCNamed env' "v" dom NONE adamc@251: val (env', st) = E.pushCNamed env' "st" ran NONE adamc@251: adamc@251: val (denv', gs') = assert env' denv ((CRecord (dom, [((CNamed nm, loc), adamc@251: (CUnit, loc))]), loc), adamc@251: (CNamed st, loc)) adamc@251: adamc@251: val c' = (CApp (f, (CNamed nm, loc)), loc) adamc@251: val c' = (CApp (c', (CNamed v, loc)), loc) adamc@251: val c' = (CApp (c', (CNamed st, loc)), loc) adamc@251: val (ps, gs'') = decomposeRow (env', denv') c' adamc@251: adamc@251: fun covered p = adamc@251: case p of adamc@251: Unknown _ => false adamc@251: | Piece p => adamc@251: case p of adamc@251: (NameN n, []) => n = nm adamc@251: | (RowN n, []) => n = st adamc@251: | _ => false adamc@251: adamc@251: val ps = List.filter (not o covered) ps adamc@251: in adamc@251: decomposeRow' (i, decomposeRow' (r, (ps @ acc, gs'' @ gs' @ gs))) adamc@251: end adamc@251: | _ => default () adamc@90: end adamc@90: in adamc@251: decomposeRow' (c, ([], [])) adamc@90: end adamc@90: adamc@90: and assert env denv (c1, c2) = adamc@90: let adamc@90: val (ps1, gs1) = decomposeRow (env, denv) c1 adamc@90: val (ps2, gs2) = decomposeRow (env, denv) c2 adamc@90: adamc@90: val unUnknown = List.mapPartial (fn Unknown _ => NONE | Piece p => SOME p) adamc@90: val ps1 = unUnknown ps1 adamc@90: val ps2 = unUnknown ps2 adamc@90: adamc@90: (*val () = print "APieces1:\n" adamc@90: val () = app pp ps1 adamc@90: val () = print "APieces2:\n" adamc@90: val () = app pp ps2*) adamc@90: adamc@90: fun assertPiece ps (p, denv) = adamc@90: let adamc@90: val pset = Option.getOpt (PM.find (denv, p), PS.empty) adamc@90: val ps = case p of adamc@207: (NameC _, _) => List.filter (fn (NameC _, _) => false | _ => true) ps adamc@90: | _ => ps adamc@90: val pset = PS.addList (pset, ps) adamc@90: in adamc@90: PM.insert (denv, p, pset) adamc@90: end adamc@90: adamc@90: val denv = foldl (assertPiece ps2) denv ps1 adamc@90: in adamc@90: (foldl (assertPiece ps1) denv ps2, gs1 @ gs2) adamc@90: end adamc@90: adamc@90: and prove env denv (c1, c2, loc) = adamc@90: let adamc@90: val (ps1, gs1) = decomposeRow (env, denv) c1 adamc@90: val (ps2, gs2) = decomposeRow (env, denv) c2 adamc@82: adamc@88: val hasUnknown = List.exists (fn Unknown _ => true | _ => false) adamc@88: val unUnknown = List.mapPartial (fn Unknown _ => NONE | Piece p => SOME p) adamc@82: in adamc@82: if hasUnknown ps1 orelse hasUnknown ps2 then adamc@90: [(loc, env, denv, c1, c2)] adamc@82: else adamc@88: let adamc@88: val ps1 = unUnknown ps1 adamc@88: val ps2 = unUnknown ps2 adamc@88: adamc@88: in adamc@88: (*print "Pieces1:\n"; adamc@88: app pp ps1; adamc@88: print "Pieces2:\n"; adamc@88: app pp ps2;*) adamc@88: adamc@88: foldl (fn (p1, rem) => adamc@88: foldl (fn (p2, rem) => adamc@88: if prove1 denv (p1, p2) then adamc@88: rem adamc@88: else adamc@90: (loc, env, denv, pieceToRow (p1, loc), pieceToRow (p2, loc)) :: rem) rem ps2) adamc@90: (gs1 @ gs2) ps1 adamc@88: end adamc@82: end adamc@82: adamc@90: and hnormCon (env, denv) c = adamc@90: let adamc@90: val cAll as (c, loc) = ElabOps.hnormCon env c adamc@90: adamc@90: fun doDisj (c1, c2, c) = adamc@90: let adamc@90: val (c, gs) = hnormCon (env, denv) c adamc@90: in adamc@90: (c, prove env denv (c1, c2, loc) @ gs) adamc@90: end adamc@90: in adamc@90: case c of adamc@90: CDisjoint cs => doDisj cs adamc@90: | TDisjoint cs => doDisj cs adamc@90: | _ => (cAll, []) adamc@90: end adamc@90: adamc@82: end