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@82: structure SS = BinarySetFn(struct adamc@82: type ord_key = string adamc@82: val compare = String.compare adamc@82: end) adamc@82: adamc@82: structure IS = IntBinarySet adamc@82: structure IM = IntBinaryMap adamc@82: adamc@82: type name_ineqs = { adamc@82: namesC : SS.set, adamc@82: namesR : IS.set, adamc@82: namesN : IS.set adamc@82: } adamc@82: adamc@82: val name_default = { adamc@82: namesC = SS.empty, adamc@82: namesR = IS.empty, adamc@82: namesN = IS.empty adamc@82: } adamc@82: adamc@82: type row_ineqs = { adamc@82: namesC : SS.set, adamc@82: namesR : IS.set, adamc@82: namesN : IS.set, adamc@82: rowsR : IS.set, adamc@82: rowsN : IS.set adamc@82: } adamc@82: adamc@82: val row_default = { adamc@82: namesC = SS.empty, adamc@82: namesR = IS.empty, adamc@82: namesN = IS.empty, adamc@82: rowsR = IS.empty, adamc@82: rowsN = IS.empty adamc@82: } adamc@82: adamc@82: fun nameToRow_ineqs {namesC, namesR, namesN} = adamc@82: {namesC = namesC, adamc@82: namesR = namesR, adamc@82: namesN = namesN, adamc@82: rowsR = IS.empty, adamc@82: rowsN = IS.empty} adamc@82: adamc@82: type env = { adamc@82: namesR : name_ineqs IM.map, adamc@82: namesN : name_ineqs IM.map, adamc@82: rowsR : row_ineqs IM.map, adamc@82: rowsN : row_ineqs IM.map adamc@82: } adamc@82: adamc@82: val empty = { adamc@82: namesR = IM.empty, adamc@82: namesN = IM.empty, adamc@82: rowsR = IM.empty, adamc@82: rowsN = IM.empty adamc@82: } adamc@82: adamc@82: datatype piece = adamc@82: NameC of string adamc@82: | NameR of int adamc@82: | NameN of int adamc@82: | RowR of int adamc@82: | RowN of int adamc@82: | Unknown adamc@82: adamc@82: fun nameToRow (c, loc) = adamc@82: (CRecord ((KUnit, loc), [((c, loc), (CUnit, loc))]), loc) adamc@82: adamc@82: 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@82: | RowR n => (CRel n, loc) adamc@82: | RowN n => (CRel n, loc) adamc@82: | Unknown => raise Fail "Unknown to row" adamc@82: adamc@82: fun decomposeRow env c = adamc@82: let adamc@82: fun decomposeName (c, acc) = adamc@82: case #1 (hnormCon env c) of adamc@82: CName s => NameC s :: acc adamc@82: | CRel n => NameR n :: acc adamc@82: | CNamed n => NameN n :: acc adamc@82: | _ => Unknown :: acc adamc@82: adamc@82: fun decomposeRow (c, acc) = adamc@82: case #1 (hnormCon env c) of adamc@82: CRecord (_, xcs) => foldl (fn ((x, _), acc) => decomposeName (x, acc)) acc xcs adamc@82: | CConcat (c1, c2) => decomposeRow (c1, decomposeRow (c2, acc)) adamc@82: | CRel n => RowR n :: acc adamc@82: | CNamed n => RowN n :: acc adamc@82: | _ => Unknown :: acc adamc@82: in adamc@82: decomposeRow (c, []) adamc@82: end adamc@82: adamc@82: fun assertPiece_name (ps, ineqs : name_ineqs) = adamc@82: {namesC = foldl (fn (p', namesC) => adamc@82: case p' of adamc@82: NameC s => SS.add (namesC, s) adamc@82: | _ => namesC) (#namesC ineqs) ps, adamc@82: namesR = foldl (fn (p', namesR) => adamc@82: case p' of adamc@82: NameR n => IS.add (namesR, n) adamc@82: | _ => namesR) (#namesR ineqs) ps, adamc@82: namesN = foldl (fn (p', namesN) => adamc@82: case p' of adamc@82: NameN n => IS.add (namesN, n) adamc@82: | _ => namesN) (#namesN ineqs) ps} adamc@82: adamc@82: fun assertPiece_row (ps, ineqs : row_ineqs) = adamc@82: {namesC = foldl (fn (p', namesC) => adamc@82: case p' of adamc@82: NameC s => SS.add (namesC, s) adamc@82: | _ => namesC) (#namesC ineqs) ps, adamc@82: namesR = foldl (fn (p', namesR) => adamc@82: case p' of adamc@82: NameR n => IS.add (namesR, n) adamc@82: | _ => namesR) (#namesR ineqs) ps, adamc@82: namesN = foldl (fn (p', namesN) => adamc@82: case p' of adamc@82: NameN n => IS.add (namesN, n) adamc@82: | _ => namesN) (#namesN ineqs) ps, adamc@82: rowsR = foldl (fn (p', rowsR) => adamc@82: case p' of adamc@82: RowR n => IS.add (rowsR, n) adamc@82: | _ => rowsR) (#rowsR ineqs) ps, adamc@82: rowsN = foldl (fn (p', rowsN) => adamc@82: case p' of adamc@82: RowN n => IS.add (rowsN, n) adamc@82: | _ => rowsN) (#rowsN ineqs) ps} adamc@82: adamc@82: fun assertPiece ps (p, denv) = adamc@82: case p of adamc@82: Unknown => denv adamc@82: | NameC _ => denv adamc@82: adamc@82: | NameR n => adamc@82: let adamc@82: val ineqs = Option.getOpt (IM.find (#namesR denv, n), name_default) adamc@82: val ineqs = assertPiece_name (ps, ineqs) adamc@82: in adamc@82: {namesR = IM.insert (#namesR denv, n, ineqs), adamc@82: namesN = #namesN denv, adamc@82: rowsR = #rowsR denv, adamc@82: rowsN = #rowsN denv} adamc@82: end adamc@82: adamc@82: | NameN n => adamc@82: let adamc@82: val ineqs = Option.getOpt (IM.find (#namesN denv, n), name_default) adamc@82: val ineqs = assertPiece_name (ps, ineqs) adamc@82: in adamc@82: {namesR = #namesR denv, adamc@82: namesN = IM.insert (#namesN denv, n, ineqs), adamc@82: rowsR = #rowsR denv, adamc@82: rowsN = #rowsN denv} adamc@82: end adamc@82: adamc@82: | RowR n => adamc@82: let adamc@82: val ineqs = Option.getOpt (IM.find (#rowsR denv, n), row_default) adamc@82: val ineqs = assertPiece_row (ps, ineqs) adamc@82: in adamc@82: {namesR = #namesR denv, adamc@82: namesN = #namesN denv, adamc@82: rowsR = IM.insert (#rowsR denv, n, ineqs), adamc@82: rowsN = #rowsN denv} adamc@82: end adamc@82: adamc@82: | RowN n => adamc@82: let adamc@82: val ineqs = Option.getOpt (IM.find (#rowsN denv, n), row_default) adamc@82: val ineqs = assertPiece_row (ps, ineqs) adamc@82: in adamc@82: {namesR = #namesR denv, adamc@82: namesN = #namesN denv, adamc@82: rowsR = #rowsR denv, adamc@82: rowsN = IM.insert (#rowsN denv, n, ineqs)} adamc@82: end adamc@82: adamc@82: fun assert env denv (c1, c2) = adamc@82: let adamc@82: val ps1 = decomposeRow env c1 adamc@82: val ps2 = decomposeRow env c2 adamc@82: adamc@82: val denv = foldl (assertPiece ps2) denv ps1 adamc@82: in adamc@82: foldl (assertPiece ps1) denv ps2 adamc@82: end adamc@82: adamc@82: fun nameEnter {namesC, namesR, namesN} = adamc@82: {namesC = namesC, adamc@82: namesR = IS.map (fn n => n + 1) namesR, adamc@82: namesN = namesN} adamc@82: adamc@82: fun rowEnter {namesC, namesR, namesN, rowsR, rowsN} = adamc@82: {namesC = namesC, adamc@82: namesR = IS.map (fn n => n + 1) namesR, adamc@82: namesN = namesN, adamc@82: rowsR = IS.map (fn n => n + 1) rowsR, adamc@82: rowsN = rowsN} adamc@82: adamc@82: fun enter {namesR, namesN, rowsR, rowsN} = adamc@82: {namesR = IM.foldli (fn (n, ineqs, namesR) => IM.insert (namesR, n+1, nameEnter ineqs)) IM.empty namesR, adamc@82: namesN = IM.map nameEnter namesN, adamc@82: rowsR = IM.foldli (fn (n, ineqs, rowsR) => IM.insert (rowsR, n+1, rowEnter ineqs)) IM.empty rowsR, adamc@82: rowsN = IM.map rowEnter rowsN} adamc@82: adamc@82: fun getIneqs (denv : env) p = adamc@82: case p of adamc@82: Unknown => raise Fail "getIneqs: Unknown" adamc@82: | NameC _ => raise Fail "getIneqs: NameC" adamc@82: | NameR n => nameToRow_ineqs (Option.getOpt (IM.find (#namesR denv, n), name_default)) adamc@82: | NameN n => nameToRow_ineqs (Option.getOpt (IM.find (#namesN denv, n), name_default)) adamc@82: | RowR n => Option.getOpt (IM.find (#rowsR denv, n), row_default) adamc@82: | RowN n => Option.getOpt (IM.find (#rowsN denv, n), row_default) adamc@82: adamc@82: fun prove1' denv (p1, p2) = adamc@82: let adamc@82: val {namesC, namesR, namesN, rowsR, rowsN} = getIneqs denv p1 adamc@82: in adamc@82: case p2 of adamc@82: Unknown => raise Fail "prove1': Unknown" adamc@82: | NameC s => SS.member (namesC, s) adamc@82: | NameR n => IS.member (namesR, n) adamc@82: | NameN n => IS.member (namesN, n) adamc@82: | RowR n => IS.member (rowsR, n) adamc@82: | RowN n => IS.member (rowsN, n) adamc@82: end adamc@82: adamc@82: fun prove1 denv (p1, p2) = adamc@82: case (p1, p2) of adamc@82: (NameC s1, NameC s2) => s1 <> s2 adamc@82: | (_, RowR _) => prove1' denv (p2, p1) adamc@82: | (_, RowN _) => prove1' denv (p2, p1) adamc@82: | _ => prove1' denv (p1, p2) adamc@82: adamc@82: fun prove env denv (c1, c2, loc) = adamc@82: let adamc@82: val ps1 = decomposeRow env c1 adamc@82: val ps2 = decomposeRow env c2 adamc@82: adamc@82: val hasUnknown = List.exists (fn p => p = Unknown) adamc@82: in adamc@82: if hasUnknown ps1 orelse hasUnknown ps2 then adamc@83: [(c1, c2)] adamc@82: else adamc@82: foldl (fn (p1, rem) => adamc@82: foldl (fn (p2, rem) => adamc@82: if prove1 denv (p1, p2) then adamc@82: rem adamc@82: else adamc@82: (pieceToRow (p1, loc), pieceToRow (p2, loc)) :: rem) rem ps2) adamc@82: [] ps1 adamc@82: end adamc@82: adamc@82: end