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