# HG changeset patch # User Adam Chlipala # Date 1214924138 14400 # Node ID b4f2a258e52ca10d372f76627922c177e97ee8d5 # Parent 60d97de1bbe82e554a66be34e6b2d484d7585d94 Initial disjointness prover diff -r 60d97de1bbe8 -r b4f2a258e52c src/disjoint.sig --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/disjoint.sig Tue Jul 01 10:55:38 2008 -0400 @@ -0,0 +1,38 @@ +(* Copyright (c) 2008, Adam Chlipala + * All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * + * - Redistributions of source code must retain the above copyright notice, + * this list of conditions and the following disclaimer. + * - Redistributions in binary form must reproduce the above copyright notice, + * this list of conditions and the following disclaimer in the documentation + * and/or other materials provided with the distribution. + * - The names of contributors may not be used to endorse or promote products + * derived from this software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE + * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE + * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR + * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF + * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS + * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN + * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) + * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE + * POSSIBILITY OF SUCH DAMAGE. + *) + +signature DISJOINT = sig + + type env + + val empty : env + val assert : ElabEnv.env -> env -> Elab.con * Elab.con -> env + val enter : env -> env + + val prove : ElabEnv.env -> env -> Elab.con * Elab.con * ErrorMsg.span -> (Elab.con * Elab.con) list + +end diff -r 60d97de1bbe8 -r b4f2a258e52c src/disjoint.sml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/disjoint.sml Tue Jul 01 10:55:38 2008 -0400 @@ -0,0 +1,294 @@ +(* Copyright (c) 2008, Adam Chlipala + * All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * + * - Redistributions of source code must retain the above copyright notice, + * this list of conditions and the following disclaimer. + * - Redistributions in binary form must reproduce the above copyright notice, + * this list of conditions and the following disclaimer in the documentation + * and/or other materials provided with the distribution. + * - The names of contributors may not be used to endorse or promote products + * derived from this software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE + * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE + * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR + * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF + * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS + * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN + * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) + * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE + * POSSIBILITY OF SUCH DAMAGE. + *) + +structure Disjoint :> DISJOINT = struct + +open Elab +open ElabOps + +structure SS = BinarySetFn(struct + type ord_key = string + val compare = String.compare + end) + +structure IS = IntBinarySet +structure IM = IntBinaryMap + +type name_ineqs = { + namesC : SS.set, + namesR : IS.set, + namesN : IS.set +} + +val name_default = { + namesC = SS.empty, + namesR = IS.empty, + namesN = IS.empty +} + +type row_ineqs = { + namesC : SS.set, + namesR : IS.set, + namesN : IS.set, + rowsR : IS.set, + rowsN : IS.set +} + +val row_default = { + namesC = SS.empty, + namesR = IS.empty, + namesN = IS.empty, + rowsR = IS.empty, + rowsN = IS.empty +} + +fun nameToRow_ineqs {namesC, namesR, namesN} = + {namesC = namesC, + namesR = namesR, + namesN = namesN, + rowsR = IS.empty, + rowsN = IS.empty} + +type env = { + namesR : name_ineqs IM.map, + namesN : name_ineqs IM.map, + rowsR : row_ineqs IM.map, + rowsN : row_ineqs IM.map +} + +val empty = { + namesR = IM.empty, + namesN = IM.empty, + rowsR = IM.empty, + rowsN = IM.empty +} + +datatype piece = + NameC of string + | NameR of int + | NameN of int + | RowR of int + | RowN of int + | Unknown + +fun nameToRow (c, loc) = + (CRecord ((KUnit, loc), [((c, loc), (CUnit, loc))]), loc) + +fun pieceToRow (p, loc) = + case p of + NameC s => nameToRow (CName s, loc) + | NameR n => nameToRow (CRel n, loc) + | NameN n => nameToRow (CNamed n, loc) + | RowR n => (CRel n, loc) + | RowN n => (CRel n, loc) + | Unknown => raise Fail "Unknown to row" + +fun decomposeRow env c = + let + fun decomposeName (c, acc) = + case #1 (hnormCon env c) of + CName s => NameC s :: acc + | CRel n => NameR n :: acc + | CNamed n => NameN n :: acc + | _ => Unknown :: acc + + fun decomposeRow (c, acc) = + case #1 (hnormCon env c) of + CRecord (_, xcs) => foldl (fn ((x, _), acc) => decomposeName (x, acc)) acc xcs + | CConcat (c1, c2) => decomposeRow (c1, decomposeRow (c2, acc)) + | CRel n => RowR n :: acc + | CNamed n => RowN n :: acc + | _ => Unknown :: acc + in + decomposeRow (c, []) + end + +fun assertPiece_name (ps, ineqs : name_ineqs) = + {namesC = foldl (fn (p', namesC) => + case p' of + NameC s => SS.add (namesC, s) + | _ => namesC) (#namesC ineqs) ps, + namesR = foldl (fn (p', namesR) => + case p' of + NameR n => IS.add (namesR, n) + | _ => namesR) (#namesR ineqs) ps, + namesN = foldl (fn (p', namesN) => + case p' of + NameN n => IS.add (namesN, n) + | _ => namesN) (#namesN ineqs) ps} + +fun assertPiece_row (ps, ineqs : row_ineqs) = + {namesC = foldl (fn (p', namesC) => + case p' of + NameC s => SS.add (namesC, s) + | _ => namesC) (#namesC ineqs) ps, + namesR = foldl (fn (p', namesR) => + case p' of + NameR n => IS.add (namesR, n) + | _ => namesR) (#namesR ineqs) ps, + namesN = foldl (fn (p', namesN) => + case p' of + NameN n => IS.add (namesN, n) + | _ => namesN) (#namesN ineqs) ps, + rowsR = foldl (fn (p', rowsR) => + case p' of + RowR n => IS.add (rowsR, n) + | _ => rowsR) (#rowsR ineqs) ps, + rowsN = foldl (fn (p', rowsN) => + case p' of + RowN n => IS.add (rowsN, n) + | _ => rowsN) (#rowsN ineqs) ps} + +fun assertPiece ps (p, denv) = + case p of + Unknown => denv + | NameC _ => denv + + | NameR n => + let + val ineqs = Option.getOpt (IM.find (#namesR denv, n), name_default) + val ineqs = assertPiece_name (ps, ineqs) + in + {namesR = IM.insert (#namesR denv, n, ineqs), + namesN = #namesN denv, + rowsR = #rowsR denv, + rowsN = #rowsN denv} + end + + | NameN n => + let + val ineqs = Option.getOpt (IM.find (#namesN denv, n), name_default) + val ineqs = assertPiece_name (ps, ineqs) + in + {namesR = #namesR denv, + namesN = IM.insert (#namesN denv, n, ineqs), + rowsR = #rowsR denv, + rowsN = #rowsN denv} + end + + | RowR n => + let + val ineqs = Option.getOpt (IM.find (#rowsR denv, n), row_default) + val ineqs = assertPiece_row (ps, ineqs) + in + {namesR = #namesR denv, + namesN = #namesN denv, + rowsR = IM.insert (#rowsR denv, n, ineqs), + rowsN = #rowsN denv} + end + + | RowN n => + let + val ineqs = Option.getOpt (IM.find (#rowsN denv, n), row_default) + val ineqs = assertPiece_row (ps, ineqs) + in + {namesR = #namesR denv, + namesN = #namesN denv, + rowsR = #rowsR denv, + rowsN = IM.insert (#rowsN denv, n, ineqs)} + end + +fun assert env denv (c1, c2) = + let + val ps1 = decomposeRow env c1 + val ps2 = decomposeRow env c2 + + val denv = foldl (assertPiece ps2) denv ps1 + in + foldl (assertPiece ps1) denv ps2 + end + +fun nameEnter {namesC, namesR, namesN} = + {namesC = namesC, + namesR = IS.map (fn n => n + 1) namesR, + namesN = namesN} + +fun rowEnter {namesC, namesR, namesN, rowsR, rowsN} = + {namesC = namesC, + namesR = IS.map (fn n => n + 1) namesR, + namesN = namesN, + rowsR = IS.map (fn n => n + 1) rowsR, + rowsN = rowsN} + +fun enter {namesR, namesN, rowsR, rowsN} = + {namesR = IM.foldli (fn (n, ineqs, namesR) => IM.insert (namesR, n+1, nameEnter ineqs)) IM.empty namesR, + namesN = IM.map nameEnter namesN, + rowsR = IM.foldli (fn (n, ineqs, rowsR) => IM.insert (rowsR, n+1, rowEnter ineqs)) IM.empty rowsR, + rowsN = IM.map rowEnter rowsN} + +fun getIneqs (denv : env) p = + case p of + Unknown => raise Fail "getIneqs: Unknown" + | NameC _ => raise Fail "getIneqs: NameC" + | NameR n => nameToRow_ineqs (Option.getOpt (IM.find (#namesR denv, n), name_default)) + | NameN n => nameToRow_ineqs (Option.getOpt (IM.find (#namesN denv, n), name_default)) + | RowR n => Option.getOpt (IM.find (#rowsR denv, n), row_default) + | RowN n => Option.getOpt (IM.find (#rowsN denv, n), row_default) + +fun prove1' denv (p1, p2) = + let + val {namesC, namesR, namesN, rowsR, rowsN} = getIneqs denv p1 + in + case p2 of + Unknown => raise Fail "prove1': Unknown" + | NameC s => SS.member (namesC, s) + | NameR n => IS.member (namesR, n) + | NameN n => IS.member (namesN, n) + | RowR n => IS.member (rowsR, n) + | RowN n => IS.member (rowsN, n) + end + +fun prove1 denv (p1, p2) = + case (p1, p2) of + (NameC s1, NameC s2) => s1 <> s2 + | (_, RowR _) => prove1' denv (p2, p1) + | (_, RowN _) => prove1' denv (p2, p1) + | _ => prove1' denv (p1, p2) + +fun prove env denv (c1, c2, loc) = + let + val ps1 = decomposeRow env c1 + val ps2 = decomposeRow env c2 + + val hasUnknown = List.exists (fn p => p = Unknown) + in + if hasUnknown ps1 orelse hasUnknown ps2 then + (ErrorMsg.errorAt loc "Structure of row is too complicated to prove disjointness"; + Print.eprefaces' [("Row 1", ElabPrint.p_con env c1), + ("Row 2", ElabPrint.p_con env c2)]; + []) + else + foldl (fn (p1, rem) => + foldl (fn (p2, rem) => + if prove1 denv (p1, p2) then + rem + else + (pieceToRow (p1, loc), pieceToRow (p2, loc)) :: rem) rem ps2) + [] ps1 + end + +end diff -r 60d97de1bbe8 -r b4f2a258e52c src/elab.sml --- a/src/elab.sml Tue Jul 01 09:29:49 2008 -0400 +++ b/src/elab.sml Tue Jul 01 10:55:38 2008 -0400 @@ -34,6 +34,7 @@ | KArrow of kind * kind | KName | KRecord of kind + | KUnit | KError | KUnif of ErrorMsg.span * string * kind option ref @@ -61,6 +62,8 @@ | CConcat of con * con | CFold of kind * kind + | CUnit + | CError | CUnif of ErrorMsg.span * kind * string * con option ref diff -r 60d97de1bbe8 -r b4f2a258e52c src/elab_print.sml --- a/src/elab_print.sml Tue Jul 01 09:29:49 2008 -0400 +++ b/src/elab_print.sml Tue Jul 01 10:55:38 2008 -0400 @@ -48,6 +48,7 @@ p_kind k2]) | KName => string "Name" | KRecord k => box [string "{", p_kind k, string "}"] + | KUnit => string "Unit" | KError => string "" | KUnif (_, _, ref (SOME k)) => p_kind' par k @@ -155,6 +156,8 @@ p_con env c2]) | CFold _ => string "fold" + | CUnit => string "()" + | CError => string "" | CUnif (_, _, _, ref (SOME c)) => p_con' par env c | CUnif (_, k, s, _) => box [string (" (KRecord k', loc)) + | KUnit => S.return2 kAll + | KError => S.return2 kAll | KUnif (_, _, ref (SOME k)) => mfk' k @@ -150,6 +152,8 @@ fn k2' => (CFold (k1', k2'), loc))) + | CUnit => S.return2 cAll + | CError => S.return2 cAll | CUnif (_, _, _, ref (SOME c)) => mfc' ctx c | CUnif _ => S.return2 cAll diff -r 60d97de1bbe8 -r b4f2a258e52c src/elaborate.sml --- a/src/elaborate.sml Tue Jul 01 09:29:49 2008 -0400 +++ b/src/elaborate.sml Tue Jul 01 10:55:38 2008 -0400 @@ -32,6 +32,7 @@ structure L' = Elab structure E = ElabEnv structure U = ElabUtil +structure D = Disjoint open Print open ElabPrint @@ -73,6 +74,8 @@ in case (k1, k2) of (L'.KType, L'.KType) => () + | (L'.KUnit, L'.KUnit) => () + | (L'.KArrow (d1, r1), L'.KArrow (d2, r2)) => (unifyKinds' d1 d2; unifyKinds' r1 r2) @@ -199,6 +202,7 @@ | L.KArrow (k1, k2) => (L'.KArrow (elabKind k1, elabKind k2), loc) | L.KName => (L'.KName, loc) | L.KRecord k => (L'.KRecord (elabKind k), loc) + | L.KUnit => (L'.KUnit, loc) | L.KWild => kunif loc fun foldKind (dom, ran, loc)= @@ -330,6 +334,10 @@ val ku = kunif loc val k = (L'.KRecord ku, loc) in + case D.prove env D.empty (c1', c2', loc) of + [] => () + | _ => raise Fail "Can't prove disjointness"; + checkKind env c1' k1 k; checkKind env c2' k2 k; ((L'.CConcat (c1', c2'), loc), k) @@ -343,6 +351,8 @@ foldKind (dom, ran, loc)) end + | L.CUnit => ((L'.CUnit, loc), (L'.KUnit, loc)) + | L.CWild k => let val k' = elabKind k @@ -478,6 +488,8 @@ | L'.CConcat (c, _) => kindof env c | L'.CFold (dom, ran) => foldKind (dom, ran, loc) + | L'.CUnit => (L'.KUnit, loc) + | L'.CError => kerror | L'.CUnif (_, k, _, _) => k diff -r 60d97de1bbe8 -r b4f2a258e52c src/explify.sml --- a/src/explify.sml Tue Jul 01 09:29:49 2008 -0400 +++ b/src/explify.sml Tue Jul 01 10:55:38 2008 -0400 @@ -38,6 +38,8 @@ | L.KName => (L'.KName, loc) | L.KRecord k => (L'.KRecord (explifyKind k), loc) + | L.KUnit => raise Fail "Explify KUnit" + | L.KError => raise Fail ("explifyKind: KError at " ^ EM.spanToString loc) | L.KUnif (_, _, ref (SOME k)) => explifyKind k | L.KUnif _ => raise Fail ("explifyKind: KUnif at " ^ EM.spanToString loc) @@ -61,6 +63,8 @@ | L.CConcat (c1, c2) => (L'.CConcat (explifyCon c1, explifyCon c2), loc) | L.CFold (dom, ran) => (L'.CFold (explifyKind dom, explifyKind ran), loc) + | L.CUnit => raise Fail "Explify CUnit" + | L.CError => raise Fail ("explifyCon: CError at " ^ EM.spanToString loc) | L.CUnif (_, _, _, ref (SOME c)) => explifyCon c | L.CUnif _ => raise Fail ("explifyCon: CUnif at " ^ EM.spanToString loc) diff -r 60d97de1bbe8 -r b4f2a258e52c src/lacweb.grm --- a/src/lacweb.grm Tue Jul 01 09:29:49 2008 -0400 +++ b/src/lacweb.grm Tue Jul 01 10:55:38 2008 -0400 @@ -40,7 +40,7 @@ | SYMBOL of string | CSYMBOL of string | LPAREN | RPAREN | LBRACK | RBRACK | LBRACE | RBRACE | EQ | COMMA | COLON | DCOLON | TCOLON | DOT | HASH | UNDER | UNDERUNDER - | CON | LTYPE | VAL | FOLD + | CON | LTYPE | VAL | FOLD | UNIT | KUNIT | TYPE | NAME | ARROW | LARROW | DARROW | FN | PLUSPLUS | DOLLAR @@ -179,6 +179,7 @@ | LBRACE kind RBRACE (KRecord kind, s (LBRACEleft, RBRACEright)) | kind ARROW kind (KArrow (kind1, kind2), s (kind1left, kind2right)) | LPAREN kind RPAREN (#1 kind, s (LPARENleft, RPARENright)) + | KUNIT (KUnit, s (KUNITleft, KUNITright)) | UNDERUNDER (KWild, s (UNDERUNDERleft, UNDERUNDERright)) capps : cterm (cterm) @@ -216,6 +217,7 @@ | path (CVar path, s (pathleft, pathright)) | UNDER (CWild (KWild, s (UNDERleft, UNDERright)), s (UNDERleft, UNDERright)) | FOLD (CFold, s (FOLDleft, FOLDright)) + | UNIT (CUnit, s (UNITleft, UNITright)) rcon : ([]) | ident EQ cexp ([(ident, cexp)]) diff -r 60d97de1bbe8 -r b4f2a258e52c src/lacweb.lex --- a/src/lacweb.lex Tue Jul 01 09:29:49 2008 -0400 +++ b/src/lacweb.lex Tue Jul 01 10:55:38 2008 -0400 @@ -120,6 +120,7 @@ str := #"\n" :: !str; continue()); . => (str := String.sub (yytext, 0) :: !str; continue()); + "()" => (Tokens.UNIT (pos yypos, pos yypos + size yytext)); "(" => (Tokens.LPAREN (pos yypos, pos yypos + size yytext)); ")" => (Tokens.RPAREN (pos yypos, pos yypos + size yytext)); "[" => (Tokens.LBRACK (pos yypos, pos yypos + size yytext)); @@ -161,6 +162,7 @@ "Type" => (Tokens.TYPE (pos yypos, pos yypos + size yytext)); "Name" => (Tokens.NAME (pos yypos, pos yypos + size yytext)); + "Unit" => (Tokens.KUNIT (pos yypos, pos yypos + size yytext)); {id} => (Tokens.SYMBOL (yytext, pos yypos, pos yypos + size yytext)); {cid} => (Tokens.CSYMBOL (yytext, pos yypos, pos yypos + size yytext)); diff -r 60d97de1bbe8 -r b4f2a258e52c src/source.sml --- a/src/source.sml Tue Jul 01 09:29:49 2008 -0400 +++ b/src/source.sml Tue Jul 01 10:55:38 2008 -0400 @@ -34,6 +34,7 @@ | KArrow of kind * kind | KName | KRecord of kind + | KUnit | KWild withtype kind = kind' located @@ -59,6 +60,8 @@ | CConcat of con * con | CFold + | CUnit + | CWild of kind withtype con = con' located diff -r 60d97de1bbe8 -r b4f2a258e52c src/source_print.sml --- a/src/source_print.sml Tue Jul 01 09:29:49 2008 -0400 +++ b/src/source_print.sml Tue Jul 01 10:55:38 2008 -0400 @@ -44,6 +44,7 @@ p_kind k2]) | KName => string "Name" | KRecord k => box [string "{", p_kind k, string "}"] + | KUnit => string "Unit" | KWild => string "_" and p_kind k = p_kind' false k @@ -127,6 +128,9 @@ space, p_con c2]) | CFold => string "fold" + + | CUnit => string "()" + | CWild k => box [string "(_", space, string "::", diff -r 60d97de1bbe8 -r b4f2a258e52c src/sources --- a/src/sources Tue Jul 01 09:29:49 2008 -0400 +++ b/src/sources Tue Jul 01 10:55:38 2008 -0400 @@ -35,6 +35,9 @@ elab_ops.sig elab_ops.sml +disjoint.sig +disjoint.sml + elaborate.sig elaborate.sml diff -r 60d97de1bbe8 -r b4f2a258e52c tests/disjoint.lac --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/tests/disjoint.lac Tue Jul 01 10:55:38 2008 -0400 @@ -0,0 +1,1 @@ +con c = [A = ()] ++ [A = ()]