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@84:               | _ => (print "Unknown name\n"; 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@84:               | _ => (print "Unknown row\n"; 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@84:       | (NameC _, _) => prove1' denv (p2, p1)
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