# HG changeset patch # User Adam Chlipala # Date 1214942282 14400 # Node ID 7bab29834cd629d3d584991fa56e06d18a5be069 # Parent 275aaeb73f1fe714fbdace81c5bd5ad4ef98ab44 Constraints in modules diff -r 275aaeb73f1f -r 7bab29834cd6 src/disjoint.sml --- a/src/disjoint.sml Tue Jul 01 13:23:46 2008 -0400 +++ b/src/disjoint.sml Tue Jul 01 15:58:02 2008 -0400 @@ -30,70 +30,86 @@ 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 + | NameM of int * string list * string | RowR of int | RowN of int - | Unknown + | RowM of int * string list * string + +fun p2s p = + case p of + NameC s => "NameC(" ^ s ^ ")" + | NameR n => "NameR(" ^ Int.toString n ^ ")" + | NameN n => "NameN(" ^ Int.toString n ^ ")" + | NameM (n, _, s) => "NameR(" ^ Int.toString n ^ ", " ^ s ^ ")" + | RowR n => "RowR(" ^ Int.toString n ^ ")" + | RowN n => "RowN(" ^ Int.toString n ^ ")" + | RowM (n, _, s) => "RowR(" ^ Int.toString n ^ ", " ^ s ^ ")" + +fun pp p = print (p2s p ^ "\n") + +structure PK = struct + +type ord_key = piece + +fun join (o1, o2) = + case o1 of + EQUAL => o2 () + | v => v + +fun joinL f (os1, os2) = + case (os1, os2) of + (nil, nil) => EQUAL + | (nil, _) => LESS + | (h1 :: t1, h2 :: t2) => + join (f (h1, h2), fn () => joinL f (t1, t2)) + | (_ :: _, nil) => GREATER + +fun compare (p1, p2) = + case (p1, p2) of + (NameC s1, NameC s2) => String.compare (s1, s2) + | (NameR n1, NameR n2) => Int.compare (n1, n2) + | (NameN n1, NameN n2) => Int.compare (n1, n2) + | (NameM (n1, ss1, s1), NameM (n2, ss2, s2)) => + join (Int.compare (n1, n2), + fn () => join (String.compare (s1, s2), fn () => + joinL String.compare (ss1, ss2))) + | (RowR n1, RowR n2) => Int.compare (n1, n2) + | (RowN n1, RowN n2) => Int.compare (n1, n2) + | (RowM (n1, ss1, s1), RowM (n2, ss2, s2)) => + join (Int.compare (n1, n2), + fn () => join (String.compare (s1, s2), fn () => + joinL String.compare (ss1, ss2))) + + | (NameC _, _) => LESS + | (_, NameC _) => GREATER + + | (NameR _, _) => LESS + | (_, NameR _) => GREATER + + | (NameN _, _) => LESS + | (_, NameN _) => GREATER + + | (NameM _, _) => LESS + | (_, NameM _) => GREATER + + | (RowR _, _) => LESS + | (_, RowR _) => GREATER + + | (RowN _, _) => LESS + | (_, RowN _) => GREATER + +end + +structure PS = BinarySetFn(PK) +structure PM = BinaryMapFn(PK) + +type env = PS.set PM.map + +val empty = PM.empty fun nameToRow (c, loc) = (CRecord ((KUnit, loc), [((c, loc), (CUnit, loc))]), loc) @@ -103,190 +119,112 @@ NameC s => nameToRow (CName s, loc) | NameR n => nameToRow (CRel n, loc) | NameN n => nameToRow (CNamed n, loc) + | NameM (n, xs, x) => nameToRow (CModProj (n, xs, x), loc) | RowR n => (CRel n, loc) - | RowN n => (CRel n, loc) - | Unknown => raise Fail "Unknown to row" + | RowN n => (CNamed n, loc) + | RowM (n, xs, x) => (CModProj (n, xs, x), loc) + +datatype piece' = + Piece of piece + | Unknown of con 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 - | _ => (print "Unknown name\n"; Unknown :: acc) - + CName s => Piece (NameC s) :: acc + | CRel n => Piece (NameR n) :: acc + | CNamed n => Piece (NameN n) :: acc + | CModProj (m1, ms, x) => Piece (NameM (m1, ms, x)) :: acc + | _ => Unknown c :: 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 - | _ => (print "Unknown row\n"; Unknown :: acc) + | CRel n => Piece (RowR n) :: acc + | CNamed n => Piece (RowN n) :: acc + | CModProj (m1, ms, x) => Piece (RowM (m1, ms, x)) :: acc + | _ => Unknown c :: 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 unUnknown = List.mapPartial (fn Unknown _ => NONE | Piece p => SOME p) + val ps1 = unUnknown ps1 + val ps2 = unUnknown ps2 + + (*val () = print "APieces1:\n" + val () = app pp ps1 + val () = print "APieces2:\n" + val () = app pp ps2*) + + fun assertPiece ps (p, denv) = + let + val pset = Option.getOpt (PM.find (denv, p), PS.empty) + val pset = PS.addList (pset, ps) + in + PM.insert (denv, p, pset) + end + 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 pieceEnter p = + case p of + NameR n => NameR (n + 1) + | RowR n => RowR (n + 1) + | _ => p -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 enter denv = + PM.foldli (fn (p, pset, denv') => + PM.insert (denv', pieceEnter p, PS.map pieceEnter pset)) + PM.empty denv fun prove1 denv (p1, p2) = case (p1, p2) of (NameC s1, NameC s2) => s1 <> s2 - | (NameC _, _) => prove1' denv (p2, p1) - | (_, RowR _) => prove1' denv (p2, p1) - | (_, RowN _) => prove1' denv (p2, p1) - | _ => prove1' denv (p1, p2) + | _ => + case PM.find (denv, p1) of + NONE => false + | SOME pset => PS.member (pset, 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) + val hasUnknown = List.exists (fn Unknown _ => true | _ => false) + val unUnknown = List.mapPartial (fn Unknown _ => NONE | Piece p => SOME p) in if hasUnknown ps1 orelse hasUnknown ps2 then [(c1, 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 + let + val ps1 = unUnknown ps1 + val ps2 = unUnknown ps2 + + in + (*print "Pieces1:\n"; + app pp ps1; + print "Pieces2:\n"; + app pp ps2;*) + + 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 end diff -r 275aaeb73f1f -r 7bab29834cd6 src/elab.sml --- a/src/elab.sml Tue Jul 01 13:23:46 2008 -0400 +++ b/src/elab.sml Tue Jul 01 15:58:02 2008 -0400 @@ -95,6 +95,7 @@ | SgiVal of string * int * con | SgiStr of string * int * sgn | SgiSgn of string * int * sgn + | SgiConstraint of con * con and sgn' = SgnConst of sgn_item list @@ -113,6 +114,7 @@ | DSgn of string * int * sgn | DStr of string * int * sgn * str | DFfiStr of string * int * sgn + | DConstraint of con * con and str' = StrConst of decl list diff -r 275aaeb73f1f -r 7bab29834cd6 src/elab_env.sig --- a/src/elab_env.sig Tue Jul 01 13:23:46 2008 -0400 +++ b/src/elab_env.sig Tue Jul 01 15:58:02 2008 -0400 @@ -81,5 +81,6 @@ val projectVal : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> Elab.con option val projectSgn : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> Elab.sgn option val projectStr : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> Elab.sgn option + val projectConstraints : env -> { sgn : Elab.sgn, str : Elab.str } -> (Elab.con * Elab.con) list option end diff -r 275aaeb73f1f -r 7bab29834cd6 src/elab_env.sml --- a/src/elab_env.sml Tue Jul 01 13:23:46 2008 -0400 +++ b/src/elab_env.sml Tue Jul 01 15:58:02 2008 -0400 @@ -291,6 +291,7 @@ | DSgn (x, n, sgn) => pushSgnNamedAs env x n sgn | DStr (x, n, sgn, _) => pushStrNamedAs env x n sgn | DFfiStr (x, n, sgn) => pushStrNamedAs env x n sgn + | DConstraint _ => env fun sgiBinds env (sgi, _) = case sgi of @@ -299,6 +300,7 @@ | SgiVal (x, n, t) => pushENamedAs env x n t | SgiStr (x, n, sgn) => pushStrNamedAs env x n sgn | SgiSgn (x, n, sgn) => pushSgnNamedAs env x n sgn + | SgiConstraint _ => env fun sgnSeek f sgis = let @@ -308,13 +310,14 @@ | (sgi, _) :: sgis => case f sgi of SOME v => SOME (v, (sgns, strs, cons)) - | NONE => - case sgi of - SgiConAbs (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x)) - | SgiCon (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x)) - | SgiVal _ => seek (sgis, sgns, strs, cons) - | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons) - | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons) + | NONE => + case sgi of + SgiConAbs (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x)) + | SgiCon (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x)) + | SgiVal _ => seek (sgis, sgns, strs, cons) + | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons) + | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons) + | SgiConstraint _ => seek (sgis, sgns, strs, cons) in seek (sgis, IM.empty, IM.empty, IM.empty) end @@ -461,5 +464,32 @@ | SgnError => SOME (CError, ErrorMsg.dummySpan) | _ => NONE +fun sgnSeekConstraints (str, sgis) = + let + fun seek (sgis, sgns, strs, cons, acc) = + case sgis of + [] => acc + | (sgi, _) :: sgis => + case sgi of + SgiConstraint (c1, c2) => + let + val sub = sgnSubCon (str, (sgns, strs, cons)) + in + seek (sgis, sgns, strs, cons, (sub c1, sub c2) :: acc) + end + | SgiConAbs (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc) + | SgiCon (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc) + | SgiVal _ => seek (sgis, sgns, strs, cons, acc) + | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons, acc) + | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons, acc) + in + seek (sgis, IM.empty, IM.empty, IM.empty, []) + end + +fun projectConstraints env {sgn, str} = + case #1 (hnormSgn env sgn) of + SgnConst sgis => SOME (sgnSeekConstraints (str, sgis)) + | SgnError => SOME [] + | _ => NONE end diff -r 275aaeb73f1f -r 7bab29834cd6 src/elab_print.sml --- a/src/elab_print.sml Tue Jul 01 13:23:46 2008 -0400 +++ b/src/elab_print.sml Tue Jul 01 15:58:02 2008 -0400 @@ -111,15 +111,16 @@ handle E.UnboundNamed _ => string ("UNBOUND_NAMED" ^ Int.toString n)) | CModProj (m1, ms, x) => let - val (m1x, sgn) = E.lookupStrNamed env m1 - + val m1x = #1 (E.lookupStrNamed env m1) + handle E.UnboundNamed _ => "UNBOUND_STR_" ^ Int.toString m1 + val m1s = if !debug then m1x ^ "__" ^ Int.toString m1 else m1x in p_list_sep (string ".") string (m1x :: ms @ [x]) - end + end | CApp (c1, c2) => parenIf par (box [p_con env c1, space, @@ -193,19 +194,22 @@ case e of EPrim p => Prim.p_t p | ERel n => - if !debug then - string (#1 (E.lookupERel env n) ^ "_" ^ Int.toString n) - else - string (#1 (E.lookupERel env n)) + ((if !debug then + string (#1 (E.lookupERel env n) ^ "_" ^ Int.toString n) + else + string (#1 (E.lookupERel env n))) + handle E.UnboundRel _ => string ("UNBOUND_REL" ^ Int.toString n)) | ENamed n => - if !debug then - string (#1 (E.lookupENamed env n) ^ "__" ^ Int.toString n) - else - string (#1 (E.lookupENamed env n)) + ((if !debug then + string (#1 (E.lookupENamed env n) ^ "__" ^ Int.toString n) + else + string (#1 (E.lookupENamed env n))) + handle E.UnboundRel _ => string ("UNBOUND_NAMED" ^ Int.toString n)) | EModProj (m1, ms, x) => let - val (m1x, sgn) = E.lookupStrNamed env m1 - + val m1x = #1 (E.lookupStrNamed env m1) + handle E.UnboundNamed _ => "UNBOUND_STR_" ^ Int.toString m1 + val m1s = if !debug then m1x ^ "__" ^ Int.toString m1 else @@ -325,6 +329,13 @@ string "=", space, p_sgn env sgn] + | SgiConstraint (c1, c2) => box [string "constraint", + space, + p_con env c1, + space, + string "~", + space, + p_con env c2] and p_sgn env (sgn, _) = case sgn of @@ -340,7 +351,8 @@ end, newline, string "end"] - | SgnVar n => string (#1 (E.lookupSgnNamed env n)) + | SgnVar n => ((string (#1 (E.lookupSgnNamed env n))) + handle E.UnboundNamed _ => string ("UNBOUND_SGN_" ^ Int.toString n)) | SgnFun (x, n, sgn, sgn') => box [string "functor", space, string "(", @@ -367,13 +379,14 @@ p_con env c] | SgnProj (m1, ms, x) => let - val (m1x, sgn) = E.lookupStrNamed env m1 - + val m1x = #1 (E.lookupStrNamed env m1) + handle E.UnboundNamed _ => "UNBOUND_SGN_" ^ Int.toString m1 + val m1s = if !debug then m1x ^ "__" ^ Int.toString m1 else m1x - in + in p_list_sep (string ".") string (m1x :: ms @ [x]) end | SgnError => string "" @@ -430,6 +443,13 @@ string ":", space, p_sgn env sgn] + | DConstraint (c1, c2) => box [string "constraint", + space, + p_con env c1, + space, + string "~", + space, + p_con env c2] and p_str env (str, _) = case str of @@ -438,7 +458,8 @@ p_file env ds, newline, string "end"] - | StrVar n => string (#1 (E.lookupStrNamed env n)) + | StrVar n => ((string (#1 (E.lookupStrNamed env n))) + handle E.UnboundNamed _ => string ("UNBOUND_STR_" ^ Int.toString n)) | StrProj (str, s) => box [p_str env str, string ".", string s] diff -r 275aaeb73f1f -r 7bab29834cd6 src/elab_util.sml --- a/src/elab_util.sml Tue Jul 01 13:23:46 2008 -0400 +++ b/src/elab_util.sml Tue Jul 01 15:58:02 2008 -0400 @@ -379,6 +379,12 @@ S.map2 (sg ctx s, fn s' => (SgiSgn (x, n, s'), loc)) + | SgiConstraint (c1, c2) => + S.bind2 (con ctx c1, + fn c1' => + S.map2 (con ctx c2, + fn c2' => + (SgiConstraint (c1', c2'), loc))) and sg ctx s acc = S.bindP (sg' ctx s acc, sgn ctx) @@ -396,7 +402,8 @@ | SgiStr (x, _, sgn) => bind (ctx, Str (x, sgn)) | SgiSgn (x, _, sgn) => - bind (ctx, Sgn (x, sgn)), + bind (ctx, Sgn (x, sgn)) + | SgiConstraint _ => ctx, sgi ctx si)) ctx sgis, fn sgis' => (SgnConst sgis', loc)) @@ -502,7 +509,8 @@ | DStr (x, _, sgn, _) => bind (ctx, Str (x, sgn)) | DFfiStr (x, _, sgn) => - bind (ctx, Str (x, sgn)), + bind (ctx, Str (x, sgn)) + | DConstraint _ => ctx, mfd ctx d)) ctx ds, fn ds' => (StrConst ds', loc)) | StrVar _ => S.return2 strAll @@ -557,6 +565,12 @@ S.map2 (mfsg ctx sgn, fn sgn' => (DFfiStr (x, n, sgn'), loc)) + | DConstraint (c1, c2) => + S.bind2 (mfc ctx c1, + fn c1' => + S.map2 (mfc ctx c2, + fn c2' => + (DConstraint (c1', c2'), loc))) in mfd end diff -r 275aaeb73f1f -r 7bab29834cd6 src/elaborate.sml --- a/src/elaborate.sml Tue Jul 01 13:23:46 2008 -0400 +++ b/src/elaborate.sml Tue Jul 01 15:58:02 2008 -0400 @@ -715,7 +715,9 @@ fun isRecord () = unifyRecordCons (env, denv) (c1All, c2All) in case (c1, c2) of - (L'.TFun (d1, r1), L'.TFun (d2, r2)) => + (L'.CUnit, L'.CUnit) => [] + + | (L'.TFun (d1, r1), L'.TFun (d2, r2)) => unifyCons' (env, denv) d1 d2 @ unifyCons' (env, denv) r1 r2 | (L'.TCFun (expl1, x1, d1, r1), L'.TCFun (expl2, _, d2, r2)) => @@ -1137,6 +1139,7 @@ | DuplicateVal of ErrorMsg.span * string | DuplicateSgn of ErrorMsg.span * string | DuplicateStr of ErrorMsg.span * string + | NotConstraintsable of L'.sgn fun sgnError env err = case err of @@ -1183,6 +1186,9 @@ ErrorMsg.errorAt loc ("Duplicate signature " ^ s ^ " in signature") | DuplicateStr (loc, s) => ErrorMsg.errorAt loc ("Duplicate structure " ^ s ^ " in signature") + | NotConstraintsable sgn => + (ErrorMsg.errorAt (#2 sgn) "Invalid signature for 'open constraints'"; + eprefaces' [("Signature", p_sgn env sgn)]) datatype str_error = UnboundStr of ErrorMsg.span * string @@ -1212,7 +1218,7 @@ val hnormSgn = E.hnormSgn -fun elabSgn_item denv ((sgi, loc), (env, gs)) = +fun elabSgn_item ((sgi, loc), (env, denv, gs)) = case sgi of L.SgiConAbs (x, k) => let @@ -1220,7 +1226,7 @@ val (env', n) = E.pushCNamed env x k' NONE in - ([(L'.SgiConAbs (x, n, k'), loc)], (env', gs)) + ([(L'.SgiConAbs (x, n, k'), loc)], (env', denv, gs)) end | L.SgiCon (x, ko, c) => @@ -1234,7 +1240,7 @@ in checkKind env c' ck k'; - ([(L'.SgiCon (x, n, k', c'), loc)], (env', gs' @ gs)) + ([(L'.SgiCon (x, n, k', c'), loc)], (env', denv, gs' @ gs)) end | L.SgiVal (x, c) => @@ -1246,7 +1252,7 @@ (unifyKinds ck ktype handle KUnify ue => strError env (NotType (ck, ue))); - ([(L'.SgiVal (x, n, c'), loc)], (env', gs' @ gs)) + ([(L'.SgiVal (x, n, c'), loc)], (env', denv, gs' @ gs)) end | L.SgiStr (x, sgn) => @@ -1254,7 +1260,7 @@ val (sgn', gs') = elabSgn (env, denv) sgn val (env', n) = E.pushStrNamed env x sgn' in - ([(L'.SgiStr (x, n, sgn'), loc)], (env', gs' @ gs)) + ([(L'.SgiStr (x, n, sgn'), loc)], (env', denv, gs' @ gs)) end | L.SgiSgn (x, sgn) => @@ -1262,7 +1268,7 @@ val (sgn', gs') = elabSgn (env, denv) sgn val (env', n) = E.pushSgnNamed env x sgn' in - ([(L'.SgiSgn (x, n, sgn'), loc)], (env', gs' @ gs)) + ([(L'.SgiSgn (x, n, sgn'), loc)], (env', denv, gs' @ gs)) end | L.SgiInclude sgn => @@ -1271,16 +1277,29 @@ in case #1 (hnormSgn env sgn') of L'.SgnConst sgis => - (sgis, (foldl (fn (sgi, env) => E.sgiBinds env sgi) env sgis, gs' @ gs)) + (sgis, (foldl (fn (sgi, env) => E.sgiBinds env sgi) env sgis, denv, gs' @ gs)) | _ => (sgnError env (NotIncludable sgn'); - ([], (env, []))) + ([], (env, denv, []))) + end + + | L.SgiConstraint (c1, c2) => + let + val (c1', k1, gs1) = elabCon (env, denv) c1 + val (c2', k2, gs2) = elabCon (env, denv) c2 + + val denv = D.assert env denv (c1', c2') + in + checkKind env c1' k1 (L'.KRecord (kunif loc), loc); + checkKind env c2' k2 (L'.KRecord (kunif loc), loc); + + ([(L'.SgiConstraint (c1', c2'), loc)], (env, denv, gs1 @ gs2)) end and elabSgn (env, denv) (sgn, loc) = case sgn of L.SgnConst sgis => let - val (sgis', (_, gs)) = ListUtil.foldlMapConcat (elabSgn_item denv) (env, []) sgis + val (sgis', (_, _, gs)) = ListUtil.foldlMapConcat elabSgn_item (env, denv, []) sgis val _ = foldl (fn ((sgi, loc), (cons, vals, sgns, strs)) => case sgi of @@ -1313,7 +1332,8 @@ sgnError env (DuplicateStr (loc, x)) else (); - (cons, vals, sgns, SS.add (strs, x)))) + (cons, vals, sgns, SS.add (strs, x))) + | L'.SgiConstraint _ => (cons, vals, sgns, strs)) (SS.empty, SS.empty, SS.empty, SS.empty) sgis' in ((L'.SgnConst sgis', loc), gs) @@ -1410,35 +1430,65 @@ | SOME (str, strs) => selfify env {sgn = sgn, str = str, strs = strs} end -fun dopen env {str, strs, sgn} = +fun dopen (env, denv) {str, strs, sgn} = let val m = foldl (fn (m, str) => (L'.StrProj (str, m), #2 sgn)) (L'.StrVar str, #2 sgn) strs in case #1 (hnormSgn env sgn) of L'.SgnConst sgis => - ListUtil.foldlMap (fn ((sgi, loc), env') => + ListUtil.foldlMap (fn ((sgi, loc), (env', denv')) => case sgi of L'.SgiConAbs (x, n, k) => - ((L'.DCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc), - E.pushCNamedAs env' x n k NONE) + let + val c = (L'.CModProj (str, strs, x), loc) + in + ((L'.DCon (x, n, k, c), loc), + (E.pushCNamedAs env' x n k (SOME c), denv')) + end | L'.SgiCon (x, n, k, c) => ((L'.DCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc), - E.pushCNamedAs env' x n k (SOME c)) + (E.pushCNamedAs env' x n k (SOME c), denv')) | L'.SgiVal (x, n, t) => ((L'.DVal (x, n, t, (L'.EModProj (str, strs, x), loc)), loc), - E.pushENamedAs env' x n t) + (E.pushENamedAs env' x n t, denv')) | L'.SgiStr (x, n, sgn) => ((L'.DStr (x, n, sgn, (L'.StrProj (m, x), loc)), loc), - E.pushStrNamedAs env' x n sgn) + (E.pushStrNamedAs env' x n sgn, denv')) | L'.SgiSgn (x, n, sgn) => ((L'.DSgn (x, n, (L'.SgnProj (str, strs, x), loc)), loc), - E.pushSgnNamedAs env' x n sgn)) - env sgis + (E.pushSgnNamedAs env' x n sgn, denv')) + | L'.SgiConstraint (c1, c2) => + ((L'.DConstraint (c1, c2), loc), + (env', denv (* D.assert env denv (c1, c2) *) ))) + (env, denv) sgis | _ => (strError env (UnOpenable sgn); - ([], env)) + ([], (env, denv))) end +fun dopenConstraints (loc, env, denv) {str, strs} = + case E.lookupStr env str of + NONE => (strError env (UnboundStr (loc, str)); + denv) + | SOME (n, sgn) => + let + val (st, sgn) = foldl (fn (m, (str, sgn)) => + case E.projectStr env {str = str, sgn = sgn, field = m} of + NONE => (strError env (UnboundStr (loc, m)); + (strerror, sgnerror)) + | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) + ((L'.StrVar n, loc), sgn) strs + + val cso = E.projectConstraints env {sgn = sgn, str = st} + + val denv = case cso of + NONE => (strError env (UnboundStr (loc, str)); + denv) + | SOME cs => foldl (fn ((c1, c2), denv) => D.assert env denv (c1, c2)) denv cs + in + denv + end + fun sgiOfDecl (d, loc) = case d of L'.DCon (x, n, k, c) => (L'.SgiCon (x, n, k, c), loc) @@ -1446,6 +1496,12 @@ | L'.DSgn (x, n, sgn) => (L'.SgiSgn (x, n, sgn), loc) | L'.DStr (x, n, sgn, _) => (L'.SgiStr (x, n, sgn), loc) | L'.DFfiStr (x, n, sgn) => (L'.SgiStr (x, n, sgn), loc) + | L'.DConstraint cs => (L'.SgiConstraint cs, loc) + +fun sgiBindsD (env, denv) (sgi, _) = + case sgi of + L'.SgiConstraint (c1, c2) => D.assert env denv (c1, c2) + | _ => denv fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) = case (#1 (hnormSgn env sgn1), #1 (hnormSgn env sgn2)) of @@ -1454,20 +1510,20 @@ | (L'.SgnConst sgis1, L'.SgnConst sgis2) => let - fun folder (sgi2All as (sgi, _), env) = + fun folder (sgi2All as (sgi, _), (env, denv)) = let fun seek p = let - fun seek env ls = + fun seek (env, denv) ls = case ls of [] => (sgnError env (UnmatchedSgi sgi2All); - env) + (env, denv)) | h :: t => case p h of - NONE => seek (E.sgiBinds env h) t - | SOME env => env + NONE => seek (E.sgiBinds env h, sgiBindsD (env, denv) h) t + | SOME envs => envs in - seek env sgis1 + seek (env, denv) sgis1 end in case sgi of @@ -1485,7 +1541,8 @@ SOME (if n1 = n2 then env else - E.pushCNamedAs env x n2 k2 (SOME (L'.CNamed n1, loc2))) + E.pushCNamedAs env x n2 k2 (SOME (L'.CNamed n1, loc2)), + denv) end else NONE @@ -1502,7 +1559,7 @@ L'.SgiCon (x', n1, k1, c1) => if x = x' then let - fun good () = SOME (E.pushCNamedAs env x n2 k2 (SOME c2)) + fun good () = SOME (E.pushCNamedAs env x n2 k2 (SOME c2), denv) in (case unifyCons (env, denv) c1 c2 of [] => good () @@ -1521,11 +1578,11 @@ L'.SgiVal (x', n1, c1) => if x = x' then (case unifyCons (env, denv) c1 c2 of - [] => SOME env + [] => SOME (env, denv) | _ => NONE) handle CUnify (c1, c2, err) => (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err)); - SOME env) + SOME (env, denv)) else NONE | _ => NONE) @@ -1545,7 +1602,7 @@ (selfifyAt env {str = (L'.StrVar n1, #2 sgn2), sgn = sgn2}) in - SOME env + SOME (env, denv) end else NONE @@ -1566,14 +1623,24 @@ else E.pushSgnNamedAs env x n1 sgn2 in - SOME env + SOME (env, denv) end else NONE | _ => NONE) + + | L'.SgiConstraint (c2, d2) => + seek (fn sgi1All as (sgi1, _) => + case sgi1 of + L'.SgiConstraint (c1, d1) => + if consEq (env, denv) (c1, c2) andalso consEq (env, denv) (d1, d2) then + SOME (env, D.assert env denv (c2, d2)) + else + NONE + | _ => NONE) end in - ignore (foldl folder env sgis2) + ignore (foldl folder (env, denv) sgis2) end | (L'.SgnFun (m1, n1, dom1, ran1), L'.SgnFun (m2, n2, dom2, ran2)) => @@ -1591,7 +1658,7 @@ | _ => sgnError env (SgnWrongForm (sgn1, sgn2)) -fun elabDecl denv ((d, loc), (env, gs)) = +fun elabDecl ((d, loc), (env, denv, gs)) = case d of L.DCon (x, ko, c) => let @@ -1604,7 +1671,7 @@ in checkKind env c' ck k'; - ([(L'.DCon (x, n, k', c'), loc)], (env', gs' @ gs)) + ([(L'.DCon (x, n, k', c'), loc)], (env', denv, gs' @ gs)) end | L.DVal (x, co, e) => let @@ -1617,7 +1684,7 @@ val gs3 = checkCon (env, denv) e' et c' in - ([(L'.DVal (x, n, c', e'), loc)], (env', gs1 @ gs2 @ gs3 @ gs)) + ([(L'.DVal (x, n, c', e'), loc)], (env', denv, gs1 @ gs2 @ gs3 @ gs)) end | L.DSgn (x, sgn) => @@ -1625,7 +1692,7 @@ val (sgn', gs') = elabSgn (env, denv) sgn val (env', n) = E.pushSgnNamed env x sgn' in - ([(L'.DSgn (x, n, sgn'), loc)], (env', gs' @ gs)) + ([(L'.DSgn (x, n, sgn'), loc)], (env', denv, gs' @ gs)) end | L.DStr (x, sgno, str) => @@ -1691,7 +1758,7 @@ | _ => strError env (FunctorRebind loc)) | _ => (); - ([(L'.DStr (x, n, sgn', str'), loc)], (env', gs' @ gs)) + ([(L'.DStr (x, n, sgn', str'), loc)], (env', denv, gs' @ gs)) end | L.DFfiStr (x, sgn) => @@ -1700,32 +1767,54 @@ val (env', n) = E.pushStrNamed env x sgn' in - ([(L'.DFfiStr (x, n, sgn'), loc)], (env', gs' @ gs)) + ([(L'.DFfiStr (x, n, sgn'), loc)], (env', denv, gs' @ gs)) end | L.DOpen (m, ms) => - case E.lookupStr env m of - NONE => (strError env (UnboundStr (loc, m)); - ([], (env, []))) - | SOME (n, sgn) => - let - val (_, sgn) = foldl (fn (m, (str, sgn)) => - case E.projectStr env {str = str, sgn = sgn, field = m} of - NONE => (strError env (UnboundStr (loc, m)); - (strerror, sgnerror)) - | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) - ((L'.StrVar n, loc), sgn) ms + (case E.lookupStr env m of + NONE => (strError env (UnboundStr (loc, m)); + ([], (env, denv, []))) + | SOME (n, sgn) => + let + val (_, sgn) = foldl (fn (m, (str, sgn)) => + case E.projectStr env {str = str, sgn = sgn, field = m} of + NONE => (strError env (UnboundStr (loc, m)); + (strerror, sgnerror)) + | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) + ((L'.StrVar n, loc), sgn) ms - val (ds, env') = dopen env {str = n, strs = ms, sgn = sgn} - in - (ds, (env', [])) - end + val (ds, (env', denv')) = dopen (env, denv) {str = n, strs = ms, sgn = sgn} + val denv' = dopenConstraints (loc, env', denv') {str = m, strs = ms} + in + (ds, (env', denv', [])) + end) + + | L.DConstraint (c1, c2) => + let + val (c1', k1, gs1) = elabCon (env, denv) c1 + val (c2', k2, gs2) = elabCon (env, denv) c2 + val gs3 = map (fn cs => (loc, env, denv, cs)) (D.prove env denv (c1', c2', loc)) + + val denv' = D.assert env denv (c1', c2') + in + checkKind env c1' k1 (L'.KRecord (kunif loc), loc); + checkKind env c2' k2 (L'.KRecord (kunif loc), loc); + + ([(L'.DConstraint (c1', c2'), loc)], (env, denv', gs1 @ gs2 @ gs3)) + end + + | L.DOpenConstraints (m, ms) => + let + val denv = dopenConstraints (loc, env, denv) {str = m, strs = ms} + in + ([], (env, denv, [])) + end and elabStr (env, denv) (str, loc) = case str of L.StrConst ds => let - val (ds', (env', gs)) = ListUtil.foldlMapConcat (elabDecl denv) (env, []) ds + val (ds', (_, _, gs)) = ListUtil.foldlMapConcat elabDecl (env, denv, []) ds val sgis = map sgiOfDecl ds' val (sgis, _, _, _, _) = @@ -1781,7 +1870,8 @@ (SS.add (strs, x), x) in ((L'.SgiStr (x, n, sgn), loc) :: sgis, cons, vals, sgns, strs) - end) + end + | L'.SgiConstraint _ => ((sgi, loc) :: sgis, cons, vals, sgns, strs)) ([], SS.empty, SS.empty, SS.empty, SS.empty) sgis in @@ -1852,7 +1942,7 @@ val (env', basis_n) = E.pushStrNamed env "Basis" sgn - val (ds, env') = dopen env' {str = basis_n, strs = [], sgn = sgn} + val (ds, (env', _)) = dopen (env', D.empty) {str = basis_n, strs = [], sgn = sgn} fun discoverC r x = case E.lookupC env' x of @@ -1868,7 +1958,7 @@ let val () = resetKunif () val () = resetCunif () - val (ds, (env, gs)) = elabDecl D.empty (d, (env, gs)) + val (ds, (env, _, gs)) = elabDecl (d, (env, D.empty, gs)) in if ErrorMsg.anyErrors () then () diff -r 275aaeb73f1f -r 7bab29834cd6 src/explify.sml --- a/src/explify.sml Tue Jul 01 13:23:46 2008 -0400 +++ b/src/explify.sml Tue Jul 01 15:58:02 2008 -0400 @@ -91,15 +91,16 @@ fun explifySgi (sgi, loc) = case sgi of - L.SgiConAbs (x, n, k) => (L'.SgiConAbs (x, n, explifyKind k), loc) - | L.SgiCon (x, n, k, c) => (L'.SgiCon (x, n, explifyKind k, explifyCon c), loc) - | L.SgiVal (x, n, c) => (L'.SgiVal (x, n, explifyCon c), loc) - | L.SgiStr (x, n, sgn) => (L'.SgiStr (x, n, explifySgn sgn), loc) - | L.SgiSgn (x, n, sgn) => (L'.SgiSgn (x, n, explifySgn sgn), loc) + L.SgiConAbs (x, n, k) => SOME (L'.SgiConAbs (x, n, explifyKind k), loc) + | L.SgiCon (x, n, k, c) => SOME (L'.SgiCon (x, n, explifyKind k, explifyCon c), loc) + | L.SgiVal (x, n, c) => SOME (L'.SgiVal (x, n, explifyCon c), loc) + | L.SgiStr (x, n, sgn) => SOME (L'.SgiStr (x, n, explifySgn sgn), loc) + | L.SgiSgn (x, n, sgn) => SOME (L'.SgiSgn (x, n, explifySgn sgn), loc) + | L.SgiConstraint _ => NONE and explifySgn (sgn, loc) = case sgn of - L.SgnConst sgis => (L'.SgnConst (map explifySgi sgis), loc) + L.SgnConst sgis => (L'.SgnConst (List.mapPartial explifySgi sgis), loc) | L.SgnVar n => (L'.SgnVar n, loc) | L.SgnFun (m, n, dom, ran) => (L'.SgnFun (m, n, explifySgn dom, explifySgn ran), loc) | L.SgnWhere (sgn, x, c) => (L'.SgnWhere (explifySgn sgn, x, explifyCon c), loc) @@ -108,22 +109,23 @@ fun explifyDecl (d, loc : EM.span) = case d of - L.DCon (x, n, k, c) => (L'.DCon (x, n, explifyKind k, explifyCon c), loc) - | L.DVal (x, n, t, e) => (L'.DVal (x, n, explifyCon t, explifyExp e), loc) + L.DCon (x, n, k, c) => SOME (L'.DCon (x, n, explifyKind k, explifyCon c), loc) + | L.DVal (x, n, t, e) => SOME (L'.DVal (x, n, explifyCon t, explifyExp e), loc) - | L.DSgn (x, n, sgn) => (L'.DSgn (x, n, explifySgn sgn), loc) - | L.DStr (x, n, sgn, str) => (L'.DStr (x, n, explifySgn sgn, explifyStr str), loc) - | L.DFfiStr (x, n, sgn) => (L'.DFfiStr (x, n, explifySgn sgn), loc) + | L.DSgn (x, n, sgn) => SOME (L'.DSgn (x, n, explifySgn sgn), loc) + | L.DStr (x, n, sgn, str) => SOME (L'.DStr (x, n, explifySgn sgn, explifyStr str), loc) + | L.DFfiStr (x, n, sgn) => SOME (L'.DFfiStr (x, n, explifySgn sgn), loc) + | L.DConstraint (c1, c2) => NONE and explifyStr (str, loc) = case str of - L.StrConst ds => (L'.StrConst (map explifyDecl ds), loc) + L.StrConst ds => (L'.StrConst (List.mapPartial explifyDecl ds), loc) | L.StrVar n => (L'.StrVar n, loc) | L.StrProj (str, s) => (L'.StrProj (explifyStr str, s), loc) | L.StrFun (m, n, dom, ran, str) => (L'.StrFun (m, n, explifySgn dom, explifySgn ran, explifyStr str), loc) | L.StrApp (str1, str2) => (L'.StrApp (explifyStr str1, explifyStr str2), loc) | L.StrError => raise Fail ("explifyStr: StrError at " ^ EM.spanToString loc) -val explify = map explifyDecl +val explify = List.mapPartial explifyDecl end diff -r 275aaeb73f1f -r 7bab29834cd6 src/lacweb.grm --- a/src/lacweb.grm Tue Jul 01 13:23:46 2008 -0400 +++ b/src/lacweb.grm Tue Jul 01 15:58:02 2008 -0400 @@ -44,7 +44,8 @@ | TYPE | NAME | ARROW | LARROW | DARROW | FN | PLUSPLUS | DOLLAR | TWIDDLE - | STRUCTURE | SIGNATURE | STRUCT | SIG | END | FUNCTOR | WHERE | EXTERN | INCLUDE | OPEN + | STRUCTURE | SIGNATURE | STRUCT | SIG | END | FUNCTOR | WHERE | EXTERN + | INCLUDE | OPEN | CONSTRAINT | CONSTRAINTS %nonterm file of decl list @@ -128,6 +129,10 @@ | OPEN mpath (case mpath of [] => raise Fail "Impossible mpath parse [1]" | m :: ms => (DOpen (m, ms), s (OPENleft, mpathright))) + | OPEN CONSTRAINTS mpath (case mpath of + [] => raise Fail "Impossible mpath parse [3]" + | m :: ms => (DOpenConstraints (m, ms), s (OPENleft, mpathright))) + | CONSTRAINT cterm TWIDDLE cterm (DConstraint (cterm1, cterm2), s (CONSTRAINTleft, ctermright)) sgn : sgntm (sgntm) | FUNCTOR LPAREN CSYMBOL COLON sgn RPAREN COLON sgn @@ -161,6 +166,7 @@ (SgnFun (CSYMBOL2, sgn1, sgn2), s (FUNCTORleft, sgn2right))), s (FUNCTORleft, sgn2right)) | INCLUDE sgn (SgiInclude sgn, s (INCLUDEleft, sgnright)) + | CONSTRAINT cterm TWIDDLE cterm (SgiConstraint (cterm1, cterm2), s (CONSTRAINTleft, ctermright)) sgis : ([]) | sgi sgis (sgi :: sgis) diff -r 275aaeb73f1f -r 7bab29834cd6 src/lacweb.lex --- a/src/lacweb.lex Tue Jul 01 13:23:46 2008 -0400 +++ b/src/lacweb.lex Tue Jul 01 15:58:02 2008 -0400 @@ -160,6 +160,8 @@ "extern" => (Tokens.EXTERN (pos yypos, pos yypos + size yytext)); "include" => (Tokens.INCLUDE (pos yypos, pos yypos + size yytext)); "open" => (Tokens.OPEN (pos yypos, pos yypos + size yytext)); + "constraint"=> (Tokens.CONSTRAINT (pos yypos, pos yypos + size yytext)); + "constraints"=> (Tokens.CONSTRAINTS (pos yypos, pos yypos + size yytext)); "Type" => (Tokens.TYPE (pos yypos, pos yypos + size yytext)); "Name" => (Tokens.NAME (pos yypos, pos yypos + size yytext)); diff -r 275aaeb73f1f -r 7bab29834cd6 src/source.sml --- a/src/source.sml Tue Jul 01 13:23:46 2008 -0400 +++ b/src/source.sml Tue Jul 01 15:58:02 2008 -0400 @@ -75,6 +75,7 @@ | SgiStr of string * sgn | SgiSgn of string * sgn | SgiInclude of sgn + | SgiConstraint of con * con and sgn' = SgnConst of sgn_item list @@ -110,6 +111,8 @@ | DStr of string * sgn option * str | DFfiStr of string * sgn | DOpen of string * string list + | DConstraint of con * con + | DOpenConstraints of string * string list and str' = StrConst of decl list diff -r 275aaeb73f1f -r 7bab29834cd6 src/source_print.sml --- a/src/source_print.sml Tue Jul 01 13:23:46 2008 -0400 +++ b/src/source_print.sml Tue Jul 01 15:58:02 2008 -0400 @@ -287,6 +287,13 @@ | SgiInclude sgn => box [string "include", space, p_sgn sgn] + | SgiConstraint (c1, c2) => box [string "constraint", + space, + p_con c1, + space, + string "~", + space, + p_con c2] and p_sgn (sgn, _) = case sgn of @@ -398,6 +405,18 @@ | DOpen (m, ms) => box [string "open", space, p_list_sep (string ".") string (m :: ms)] + | DConstraint (c1, c2) => box [string "constraint", + space, + p_con c1, + space, + string "~", + space, + p_con c2] + | DOpenConstraints (m, ms) => box [string "open", + space, + string "constraints", + space, + p_list_sep (string ".") string (m :: ms)] and p_str (str, _) = case str of diff -r 275aaeb73f1f -r 7bab29834cd6 tests/constraint.lac --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/tests/constraint.lac Tue Jul 01 15:58:02 2008 -0400 @@ -0,0 +1,29 @@ +signature S = sig + con nm :: Name + con r :: {Type} + + constraint [nm] ~ r +end + +structure M : S = struct + con nm = #A + con r = [B = float, C = string] + + constraint [A] ~ [B] + constraint [nm] ~ r + constraint [C] ~ [D] +end + +structure M' = struct + open M + + con combo = [nm = int] ++ r +end + +structure M' = struct + open constraints M + + con nm' = M.nm + con r' = M.r + con combo = [nm' = int] ++ r' +end