summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/disjoint.sml344
-rw-r--r--src/elab.sml2
-rw-r--r--src/elab_env.sig1
-rw-r--r--src/elab_env.sml44
-rw-r--r--src/elab_print.sml57
-rw-r--r--src/elab_util.sml18
-rw-r--r--src/elaborate.sml210
-rw-r--r--src/explify.sml28
-rw-r--r--src/lacweb.grm8
-rw-r--r--src/lacweb.lex2
-rw-r--r--src/source.sml3
-rw-r--r--src/source_print.sml19
-rw-r--r--tests/constraint.lac29
13 files changed, 461 insertions, 304 deletions
diff --git a/src/disjoint.sml b/src/disjoint.sml
index c9f6d2e9..6c66fdd8 100644
--- a/src/disjoint.sml
+++ b/src/disjoint.sml
@@ -30,70 +30,86 @@ 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
+ | 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 @@ fun pieceToRow (p, loc) =
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 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 =
+fun pieceEnter 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
+ NameR n => NameR (n + 1)
+ | RowR n => RowR (n + 1)
+ | _ => p
+
+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 --git a/src/elab.sml b/src/elab.sml
index cf9a7e7a..9eb8ad2f 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -95,6 +95,7 @@ datatype sgn_item' =
| 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 @@ datatype decl' =
| 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 --git a/src/elab_env.sig b/src/elab_env.sig
index 54e53607..0e43c9a7 100644
--- a/src/elab_env.sig
+++ b/src/elab_env.sig
@@ -81,5 +81,6 @@ signature ELAB_ENV = sig
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 --git a/src/elab_env.sml b/src/elab_env.sml
index 4c27c98d..897f481d 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -291,6 +291,7 @@ fun declBinds env (d, _) =
| 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 @@ fun sgiBinds env (sgi, _) =
| 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 @@ fun sgnSeek f sgis =
| (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 @@ fun projectVal env {sgn, str, field} =
| 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 --git a/src/elab_print.sml b/src/elab_print.sml
index c90a0494..d394c679 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -111,15 +111,16 @@ fun p_con' par env (c, _) =
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 @@ fun p_exp' par env (e, _) =
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 @@ fun p_sgn_item env (sgi, _) =
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 @@ and p_sgn env (sgn, _) =
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 @@ and p_sgn env (sgn, _) =
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 "<ERROR>"
@@ -430,6 +443,13 @@ fun p_decl env ((d, _) : decl) =
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 @@ and p_str env (str, _) =
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 --git a/src/elab_util.sml b/src/elab_util.sml
index 65906c72..9879a9f9 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -379,6 +379,12 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
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 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
| 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 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f
| 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 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f
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 --git a/src/elaborate.sml b/src/elaborate.sml
index bc43515f..216d483f 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -715,7 +715,9 @@ and unifyCons'' (env, denv) (c1All as (c1, _)) (c2All as (c2, _)) =
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 @@ datatype sgn_error =
| 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 @@ fun sgnError env err =
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 @@ fun strError env err =
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 @@ fun elabSgn_item denv ((sgi, loc), (env, gs)) =
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 @@ fun elabSgn_item denv ((sgi, loc), (env, gs)) =
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 @@ fun elabSgn_item denv ((sgi, loc), (env, gs)) =
(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 @@ fun elabSgn_item denv ((sgi, loc), (env, gs)) =
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 @@ fun elabSgn_item denv ((sgi, loc), (env, gs)) =
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 @@ fun elabSgn_item denv ((sgi, loc), (env, gs)) =
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 @@ and elabSgn (env, denv) (sgn, loc) =
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 @@ fun selfifyAt env {str, sgn} =
| 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 @@ fun sgiOfDecl (d, loc) =
| 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 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
| (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 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
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 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
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 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
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 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
(selfifyAt env {str = (L'.StrVar n1, #2 sgn2),
sgn = sgn2})
in
- SOME env
+ SOME (env, denv)
end
else
NONE
@@ -1566,14 +1623,24 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
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 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
| _ => 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 @@ fun elabDecl denv ((d, loc), (env, gs)) =
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 @@ fun elabDecl denv ((d, loc), (env, gs)) =
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 @@ fun elabDecl denv ((d, loc), (env, gs)) =
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 @@ fun elabDecl denv ((d, loc), (env, gs)) =
| _ => 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 @@ fun elabDecl denv ((d, loc), (env, gs)) =
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
-
- val (ds, env') = dopen env {str = n, strs = ms, sgn = sgn}
- in
- (ds, (env', []))
- end
+ (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', 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 @@ and elabStr (env, denv) (str, loc) =
(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 @@ fun elabFile basis env file =
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 @@ fun elabFile basis env file =
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 --git a/src/explify.sml b/src/explify.sml
index e0226213..c5e7fbd4 100644
--- a/src/explify.sml
+++ b/src/explify.sml
@@ -91,15 +91,16 @@ fun explifyExp (e, loc) =
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 @@ and explifySgn (sgn, loc) =
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 --git a/src/lacweb.grm b/src/lacweb.grm
index 4bf03388..84877eee 100644
--- a/src/lacweb.grm
+++ b/src/lacweb.grm
@@ -44,7 +44,8 @@ val s = ErrorMsg.spanOf
| 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 @@ decl : CON SYMBOL EQ cexp (DCon (SYMBOL, NONE, cexp), s (CONleft,
| 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 @@ sgi : CON SYMBOL DCOLON kind (SgiConAbs (SYMBOL, kind), s (CONleft, k
(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 --git a/src/lacweb.lex b/src/lacweb.lex
index 3fa0b45c..8b4a1789 100644
--- a/src/lacweb.lex
+++ b/src/lacweb.lex
@@ -160,6 +160,8 @@ realconst = [0-9]+\.[0-9]*;
<INITIAL> "extern" => (Tokens.EXTERN (pos yypos, pos yypos + size yytext));
<INITIAL> "include" => (Tokens.INCLUDE (pos yypos, pos yypos + size yytext));
<INITIAL> "open" => (Tokens.OPEN (pos yypos, pos yypos + size yytext));
+<INITIAL> "constraint"=> (Tokens.CONSTRAINT (pos yypos, pos yypos + size yytext));
+<INITIAL> "constraints"=> (Tokens.CONSTRAINTS (pos yypos, pos yypos + size yytext));
<INITIAL> "Type" => (Tokens.TYPE (pos yypos, pos yypos + size yytext));
<INITIAL> "Name" => (Tokens.NAME (pos yypos, pos yypos + size yytext));
diff --git a/src/source.sml b/src/source.sml
index 0b168dd0..4aea002e 100644
--- a/src/source.sml
+++ b/src/source.sml
@@ -75,6 +75,7 @@ datatype sgn_item' =
| 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 @@ datatype decl' =
| 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 --git a/src/source_print.sml b/src/source_print.sml
index 41051c81..8fc27106 100644
--- a/src/source_print.sml
+++ b/src/source_print.sml
@@ -287,6 +287,13 @@ fun p_sgn_item (sgi, _) =
| 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 @@ fun p_decl ((d, _) : decl) =
| 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 --git a/tests/constraint.lac b/tests/constraint.lac
new file mode 100644
index 00000000..54c77093
--- /dev/null
+++ b/tests/constraint.lac
@@ -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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-18 11:21:27 +0000