summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-12-19 10:03:31 -0500
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-12-19 10:03:31 -0500
commitba83ee9a9b3d2539b820c9fcb1cb7cd42226da6c (patch)
tree147dbc155a38e55b93e8c303304bdc6c9f5e8258 /src
parent8d98194908d9001ce5da0bceda10c22e71e940ba (diff)
Initial conversion to arbitrary-kind classes
Diffstat (limited to 'src')
-rw-r--r--src/elab.sml6
-rw-r--r--src/elab_env.sml36
-rw-r--r--src/elab_print.sml46
-rw-r--r--src/elab_util.sml43
-rw-r--r--src/elaborate.sml115
-rw-r--r--src/explify.sml10
-rw-r--r--src/source.sml6
-rw-r--r--src/source_print.sml44
-rw-r--r--src/urweb.grm49
9 files changed, 212 insertions, 143 deletions
diff --git a/src/elab.sml b/src/elab.sml
index d997b7ec..8e44c43c 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -136,8 +136,8 @@ datatype sgn_item' =
| SgiStr of string * int * sgn
| SgiSgn of string * int * sgn
| SgiConstraint of con * con
- | SgiClassAbs of string * int
- | SgiClass of string * int * con
+ | SgiClassAbs of string * int * kind
+ | SgiClass of string * int * kind * con
and sgn' =
SgnConst of sgn_item list
@@ -163,7 +163,7 @@ datatype decl' =
| DExport of int * sgn * str
| DTable of int * string * int * con
| DSequence of int * string * int
- | DClass of string * int * con
+ | DClass of string * int * kind * con
| DDatabase of string
| DCookie of int * string * int * con
diff --git a/src/elab_env.sml b/src/elab_env.sml
index d1084d0c..53c934dd 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -604,8 +604,8 @@ fun sgiSeek (sgi, (sgns, strs, cons)) =
| SgiSgn (x, n, _) => (IM.insert (sgns, n, x), strs, cons)
| SgiStr (x, n, _) => (sgns, IM.insert (strs, n, x), cons)
| SgiConstraint _ => (sgns, strs, cons)
- | SgiClassAbs (x, n) => (sgns, strs, IM.insert (cons, n, x))
- | SgiClass (x, n, _) => (sgns, strs, IM.insert (cons, n, x))
+ | SgiClassAbs (x, n, _) => (sgns, strs, IM.insert (cons, n, x))
+ | SgiClass (x, n, _, _) => (sgns, strs, IM.insert (cons, n, x))
fun sgnSeek f sgis =
let
@@ -788,8 +788,8 @@ fun enrichClasses env classes (m1, ms) sgn =
fmap,
pushSgnNamedAs env x n sgn)
- | SgiClassAbs xn => found xn
- | SgiClass (x, n, _) => found (x, n)
+ | SgiClassAbs (x, n, _) => found (x, n)
+ | SgiClass (x, n, _, _) => found (x, n)
| SgiVal (x, n, (CApp (f, a), _)) =>
let
fun unravel c =
@@ -946,8 +946,8 @@ fun sgiBinds env (sgi, loc) =
| SgiSgn (x, n, sgn) => pushSgnNamedAs env x n sgn
| SgiConstraint _ => env
- | SgiClassAbs (x, n) => pushCNamedAs env x n (KArrow ((KType, loc), (KType, loc)), loc) NONE
- | SgiClass (x, n, c) => pushCNamedAs env x n (KArrow ((KType, loc), (KType, loc)), loc) (SOME c)
+ | SgiClassAbs (x, n, k) => pushCNamedAs env x n (KArrow (k, (KType, loc)), loc) NONE
+ | SgiClass (x, n, k, c) => pushCNamedAs env x n (KArrow (k, (KType, loc)), loc) (SOME c)
fun sgnSubCon x =
ElabUtil.Con.map {kind = id,
@@ -998,14 +998,14 @@ fun projectCon env {sgn, str, field} =
end
else
NONE
- | SgiClassAbs (x, _) => if x = field then
- SOME ((KArrow ((KType, #2 sgn), (KType, #2 sgn)), #2 sgn), NONE)
- else
- NONE
- | SgiClass (x, _, c) => if x = field then
- SOME ((KArrow ((KType, #2 sgn), (KType, #2 sgn)), #2 sgn), SOME c)
- else
- NONE
+ | SgiClassAbs (x, _, k) => if x = field then
+ SOME ((KArrow (k, (KType, #2 sgn)), #2 sgn), NONE)
+ else
+ NONE
+ | SgiClass (x, _, k, c) => if x = field then
+ SOME ((KArrow (k, (KType, #2 sgn)), #2 sgn), SOME c)
+ else
+ NONE
| _ => NONE) sgis of
NONE => NONE
| SOME ((k, co), subs) => SOME (k, Option.map (sgnSubCon (str, subs)) co))
@@ -1101,8 +1101,8 @@ fun sgnSeekConstraints (str, sgis) =
| 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)
- | SgiClassAbs (x, n) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
- | SgiClass (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
+ | SgiClassAbs (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
+ | SgiClass (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
in
seek (sgis, IM.empty, IM.empty, IM.empty, [])
end
@@ -1189,9 +1189,9 @@ fun declBinds env (d, loc) =
in
pushENamedAs env x n t
end
- | DClass (x, n, c) =>
+ | DClass (x, n, k, c) =>
let
- val k = (KArrow ((KType, loc), (KType, loc)), loc)
+ val k = (KArrow (k, (KType, loc)), loc)
val env = pushCNamedAs env x n k (SOME c)
in
pushClass env n
diff --git a/src/elab_print.sml b/src/elab_print.sml
index 2f652737..0e6c9767 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -534,16 +534,24 @@ fun p_sgn_item env (sgi, _) =
string "~",
space,
p_con env c2]
- | SgiClassAbs (x, n) => box [string "class",
- space,
- p_named x n]
- | SgiClass (x, n, c) => box [string "class",
- space,
- p_named x n,
- space,
- string "=",
- space,
- p_con env c]
+ | SgiClassAbs (x, n, k) => box [string "class",
+ space,
+ p_named x n,
+ space,
+ string "::",
+ space,
+ p_kind k]
+ | SgiClass (x, n, k, c) => box [string "class",
+ space,
+ p_named x n,
+ space,
+ string "::",
+ space,
+ p_kind k,
+ space,
+ string "=",
+ space,
+ p_con env c]
and p_sgn env (sgn, _) =
case sgn of
@@ -705,13 +713,17 @@ fun p_decl env (dAll as (d, _) : decl) =
| DSequence (_, x, n) => box [string "sequence",
space,
p_named x n]
- | DClass (x, n, c) => box [string "class",
- space,
- p_named x n,
- space,
- string "=",
- space,
- p_con env c]
+ | DClass (x, n, k, c) => box [string "class",
+ space,
+ p_named x n,
+ space,
+ string "::",
+ space,
+ p_kind k,
+ space,
+ string "=",
+ space,
+ p_con env c]
| DDatabase s => box [string "database",
space,
string s]
diff --git a/src/elab_util.sml b/src/elab_util.sml
index 6e2c76f6..6e78907d 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -547,11 +547,16 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
S.map2 (con ctx c2,
fn c2' =>
(SgiConstraint (c1', c2'), loc)))
- | SgiClassAbs _ => S.return2 siAll
- | SgiClass (x, n, c) =>
- S.map2 (con ctx c,
- fn c' =>
- (SgiClass (x, n, c'), loc))
+ | SgiClassAbs (x, n, k) =>
+ S.map2 (kind k,
+ fn k' =>
+ (SgiClassAbs (x, n, k'), loc))
+ | SgiClass (x, n, k, c) =>
+ S.bind2 (kind k,
+ fn k' =>
+ S.map2 (con ctx c,
+ fn c' =>
+ (SgiClass (x, n, k', c'), loc)))
and sg ctx s acc =
S.bindP (sg' ctx s acc, sgn ctx)
@@ -575,10 +580,10 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
| SgiSgn (x, _, sgn) =>
bind (ctx, Sgn (x, sgn))
| SgiConstraint _ => ctx
- | SgiClassAbs (x, n) =>
- bind (ctx, NamedC (x, n, (KArrow ((KType, loc), (KType, loc)), loc)))
- | SgiClass (x, n, _) =>
- bind (ctx, NamedC (x, n, (KArrow ((KType, loc), (KType, loc)), loc))),
+ | SgiClassAbs (x, n, k) =>
+ bind (ctx, NamedC (x, n, (KArrow (k, (KType, loc)), loc)))
+ | SgiClass (x, n, k, _) =>
+ bind (ctx, NamedC (x, n, (KArrow (k, (KType, loc)), loc))),
sgi ctx si)) ctx sgis,
fn sgis' =>
(SgnConst sgis', loc))
@@ -720,8 +725,8 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f
c), loc)))
| DSequence (tn, x, n) =>
bind (ctx, NamedE (x, (CModProj (n, [], "sql_sequence"), loc)))
- | DClass (x, n, _) =>
- bind (ctx, NamedC (x, n, (KArrow ((KType, loc), (KType, loc)), loc)))
+ | DClass (x, n, k, _) =>
+ bind (ctx, NamedC (x, n, (KArrow (k, (KType, loc)), loc)))
| DDatabase _ => ctx
| DCookie (tn, x, n, c) =>
bind (ctx, NamedE (x, (CApp ((CModProj (n, [], "cookie"), loc),
@@ -819,10 +824,12 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f
(DTable (tn, x, n, c'), loc))
| DSequence _ => S.return2 dAll
- | DClass (x, n, c) =>
- S.map2 (mfc ctx c,
- fn c' =>
- (DClass (x, n, c'), loc))
+ | DClass (x, n, k, c) =>
+ S.bind2 (mfk k,
+ fn k' =>
+ S.map2 (mfc ctx c,
+ fn c' =>
+ (DClass (x, n, k', c'), loc)))
| DDatabase _ => S.return2 dAll
@@ -963,7 +970,7 @@ and maxNameDecl (d, _) =
| DSgn (_, n, sgn) => Int.max (n, maxNameSgn sgn)
| DFfiStr (_, n, sgn) => Int.max (n, maxNameSgn sgn)
| DConstraint _ => 0
- | DClass (_, n, _) => n
+ | DClass (_, n, _, _) => n
| DExport _ => 0
| DTable (n1, _, n2, _) => Int.max (n1, n2)
| DSequence (n1, _, n2) => Int.max (n1, n2)
@@ -1002,8 +1009,8 @@ and maxNameSgi (sgi, _) =
| SgiStr (_, n, sgn) => Int.max (n, maxNameSgn sgn)
| SgiSgn (_, n, sgn) => Int.max (n, maxNameSgn sgn)
| SgiConstraint _ => 0
- | SgiClassAbs (_, n) => n
- | SgiClass (_, n, _) => n
+ | SgiClassAbs (_, n, _) => n
+ | SgiClass (_, n, _, _) => n
end
diff --git a/src/elaborate.sml b/src/elaborate.sml
index d42175ce..05e08c81 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -2059,24 +2059,26 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
([(L'.SgiConstraint (c1', c2'), loc)], (env, denv, gs1 @ gs2 @ gs3))
end
- | L.SgiClassAbs x =>
+ | L.SgiClassAbs (x, k) =>
let
- val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
- val (env, n) = E.pushCNamed env x k NONE
+ val k = elabKind k
+ val k' = (L'.KArrow (k, (L'.KType, loc)), loc)
+ val (env, n) = E.pushCNamed env x k' NONE
val env = E.pushClass env n
in
- ([(L'.SgiClassAbs (x, n), loc)], (env, denv, []))
+ ([(L'.SgiClassAbs (x, n, k), loc)], (env, denv, []))
end
- | L.SgiClass (x, c) =>
+ | L.SgiClass (x, k, c) =>
let
- val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
+ val k = elabKind k
+ val k' = (L'.KArrow (k, (L'.KType, loc)), loc)
val (c', ck, gs) = elabCon (env, denv) c
- val (env, n) = E.pushCNamed env x k (SOME c')
+ val (env, n) = E.pushCNamed env x k' (SOME c')
val env = E.pushClass env n
in
- checkKind env c' ck k;
- ([(L'.SgiClass (x, n, c'), loc)], (env, denv, []))
+ checkKind env c' ck k';
+ ([(L'.SgiClass (x, n, k, c'), loc)], (env, denv, []))
end
and elabSgn (env, denv) (sgn, loc) =
@@ -2140,13 +2142,13 @@ and elabSgn (env, denv) (sgn, loc) =
();
(cons, vals, sgns, SS.add (strs, x)))
| L'.SgiConstraint _ => (cons, vals, sgns, strs)
- | L'.SgiClassAbs (x, _) =>
+ | L'.SgiClassAbs (x, _, _) =>
(if SS.member (cons, x) then
sgnError env (DuplicateCon (loc, x))
else
();
(SS.add (cons, x), vals, sgns, strs))
- | L'.SgiClass (x, _, _) =>
+ | L'.SgiClass (x, _, _, _) =>
(if SS.member (cons, x) then
sgnError env (DuplicateCon (loc, x))
else
@@ -2222,8 +2224,8 @@ fun selfify env {str, strs, sgn} =
(L'.SgiCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)
| (L'.SgiDatatype (x, n, xs, xncs), loc) =>
(L'.SgiDatatypeImp (x, n, str, strs, x, xs, xncs), loc)
- | (L'.SgiClassAbs (x, n), loc) =>
- (L'.SgiClass (x, n, (L'.CModProj (str, strs, x), loc)), loc)
+ | (L'.SgiClassAbs (x, n, k), loc) =>
+ (L'.SgiClass (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)
| (L'.SgiStr (x, n, sgn), loc) =>
(L'.SgiStr (x, n, selfify env {str = str, strs = strs @ [x], sgn = sgn}), loc)
| x => x) sgis), #2 sgn)
@@ -2284,19 +2286,19 @@ fun dopen (env, denv) {str, strs, sgn} =
(L'.DSgn (x, n, (L'.SgnProj (str, strs, x), loc)), loc)
| L'.SgiConstraint (c1, c2) =>
(L'.DConstraint (c1, c2), loc)
- | L'.SgiClassAbs (x, n) =>
+ | L'.SgiClassAbs (x, n, k) =>
let
- val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
+ val k' = (L'.KArrow (k, (L'.KType, loc)), loc)
val c = (L'.CModProj (str, strs, x), loc)
in
- (L'.DCon (x, n, k, c), loc)
+ (L'.DCon (x, n, k', c), loc)
end
- | L'.SgiClass (x, n, _) =>
+ | L'.SgiClass (x, n, k, _) =>
let
- val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
+ val k' = (L'.KArrow (k, (L'.KType, loc)), loc)
val c = (L'.CModProj (str, strs, x), loc)
in
- (L'.DCon (x, n, k, c), loc)
+ (L'.DCon (x, n, k', c), loc)
end
in
(d, (E.declBinds env' d, denv'))
@@ -2320,7 +2322,7 @@ fun sgiOfDecl (d, loc) =
| L'.DExport _ => []
| L'.DTable (tn, x, n, c) => [(L'.SgiVal (x, n, (L'.CApp (tableOf (), c), loc)), loc)]
| L'.DSequence (tn, x, n) => [(L'.SgiVal (x, n, sequenceOf ()), loc)]
- | L'.DClass (x, n, c) => [(L'.SgiClass (x, n, c), loc)]
+ | L'.DClass (x, n, k, c) => [(L'.SgiClass (x, n, k, c), loc)]
| L'.DDatabase _ => []
| L'.DCookie (tn, x, n, c) => [(L'.SgiVal (x, n, (L'.CApp (cookieOf (), c), loc)), loc)]
@@ -2418,14 +2420,14 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
in
found (x', n1, k', SOME (L'.CModProj (m1, ms, s), loc))
end
- | L'.SgiClassAbs (x', n1) => found (x', n1,
- (L'.KArrow ((L'.KType, loc),
- (L'.KType, loc)), loc),
- NONE)
- | L'.SgiClass (x', n1, c) => found (x', n1,
- (L'.KArrow ((L'.KType, loc),
- (L'.KType, loc)), loc),
- SOME c)
+ | L'.SgiClassAbs (x', n1, k) => found (x', n1,
+ (L'.KArrow (k,
+ (L'.KType, loc)), loc),
+ NONE)
+ | L'.SgiClass (x', n1, k, c) => found (x', n1,
+ (L'.KArrow (k,
+ (L'.KType, loc)), loc),
+ SOME c)
| _ => NONE
end)
@@ -2458,8 +2460,8 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
in
case sgi1 of
L'.SgiCon (x', n1, k1, c1) => found (x', n1, k1, c1)
- | L'.SgiClass (x', n1, c1) =>
- found (x', n1, (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc), c1)
+ | L'.SgiClass (x', n1, k1, c1) =>
+ found (x', n1, (L'.KArrow (k1, (L'.KType, loc)), loc), c1)
| _ => NONE
end)
@@ -2632,13 +2634,17 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
NONE
| _ => NONE)
- | L'.SgiClassAbs (x, n2) =>
+ | L'.SgiClassAbs (x, n2, k2) =>
seek (fn (env, sgi1All as (sgi1, _)) =>
let
- fun found (x', n1, co) =
+ fun found (x', n1, k1, co) =
if x = x' then
let
- val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
+ val () = unifyKinds k1 k2
+ handle KUnify (k1, k2, err) =>
+ sgnError env (SgiWrongKind (sgi1All, k1, sgi2All, k2, err))
+
+ val k = (L'.KArrow (k1, (L'.KType, loc)), loc)
val env = E.pushCNamedAs env x n1 k co
in
SOME (if n1 = n2 then
@@ -2651,18 +2657,22 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
NONE
in
case sgi1 of
- L'.SgiClassAbs (x', n1) => found (x', n1, NONE)
- | L'.SgiClass (x', n1, c) => found (x', n1, SOME c)
+ L'.SgiClassAbs (x', n1, k1) => found (x', n1, k1, NONE)
+ | L'.SgiClass (x', n1, k1, c) => found (x', n1, k1, SOME c)
| _ => NONE
end)
- | L'.SgiClass (x, n2, c2) =>
+ | L'.SgiClass (x, n2, k2, c2) =>
seek (fn (env, sgi1All as (sgi1, _)) =>
let
- val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
+ val k = (L'.KArrow (k2, (L'.KType, loc)), loc)
- fun found (x', n1, c1) =
+ fun found (x', n1, k1, c1) =
if x = x' then
let
+ val () = unifyKinds k1 k2
+ handle KUnify (k1, k2, err) =>
+ sgnError env (SgiWrongKind (sgi1All, k1, sgi2All, k2, err))
+
fun good () =
let
val env = E.pushCNamedAs env x n2 k (SOME c2)
@@ -2685,7 +2695,7 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
NONE
in
case sgi1 of
- L'.SgiClass (x', n1, c1) => found (x', n1, c1)
+ L'.SgiClass (x', n1, k1, c1) => found (x', n1, k1, c1)
| _ => NONE
end)
end
@@ -2878,8 +2888,8 @@ fun wildifyStr env (str, sgn) =
L.DCon (x, _, _) => ((#1 (SM.remove (neededC, x)), neededV)
handle NotFound =>
needed)
- | L.DClass (x, _) => ((#1 (SM.remove (neededC, x)), neededV)
- handle NotFound => needed)
+ | L.DClass (x, _, _) => ((#1 (SM.remove (neededC, x)), neededV)
+ handle NotFound => needed)
| L.DVal (x, _, _) => ((neededC, SS.delete (neededV, x))
handle NotFound => needed)
| L.DOpen _ => (SM.empty, SS.empty)
@@ -3286,15 +3296,16 @@ fun elabDecl (dAll as (d, loc), (env, denv, gs : constraint list)) =
([(L'.DSequence (!basis_r, x, n), loc)], (env, denv, gs))
end
- | L.DClass (x, c) =>
+ | L.DClass (x, k, c) =>
let
- val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
+ val k = elabKind k
+ val k' = (L'.KArrow (k, (L'.KType, loc)), loc)
val (c', ck, gs') = elabCon (env, denv) c
- val (env, n) = E.pushCNamed env x k (SOME c')
+ val (env, n) = E.pushCNamed env x k' (SOME c')
val env = E.pushClass env n
in
- checkKind env c' ck k;
- ([(L'.DClass (x, n, c'), loc)], (env, denv, enD gs' @ gs))
+ checkKind env c' ck k';
+ ([(L'.DClass (x, n, k, c'), loc)], (env, denv, enD gs' @ gs))
end
| L.DDatabase s => ([(L'.DDatabase s, loc)], (env, denv, gs))
@@ -3408,29 +3419,25 @@ and elabStr (env, denv) (str, loc) =
((L'.SgiStr (x, n, sgn), loc) :: sgis, cons, vals, sgns, strs)
end
| L'.SgiConstraint _ => ((sgi, loc) :: sgis, cons, vals, sgns, strs)
- | L'.SgiClassAbs (x, n) =>
+ | L'.SgiClassAbs (x, n, k) =>
let
- val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
-
val (cons, x) =
if SS.member (cons, x) then
(cons, "?" ^ x)
else
(SS.add (cons, x), x)
in
- ((L'.SgiClassAbs (x, n), loc) :: sgis, cons, vals, sgns, strs)
+ ((L'.SgiClassAbs (x, n, k), loc) :: sgis, cons, vals, sgns, strs)
end
- | L'.SgiClass (x, n, c) =>
+ | L'.SgiClass (x, n, k, c) =>
let
- val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
-
val (cons, x) =
if SS.member (cons, x) then
(cons, "?" ^ x)
else
(SS.add (cons, x), x)
in
- ((L'.SgiClass (x, n, c), loc) :: sgis, cons, vals, sgns, strs)
+ ((L'.SgiClass (x, n, k, c), loc) :: sgis, cons, vals, sgns, strs)
end)
([], SS.empty, SS.empty, SS.empty, SS.empty) sgis
diff --git a/src/explify.sml b/src/explify.sml
index e3c22f20..a10037ef 100644
--- a/src/explify.sml
+++ b/src/explify.sml
@@ -139,9 +139,9 @@ fun explifySgi (sgi, 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
- | L.SgiClassAbs (x, n) => SOME (L'.SgiConAbs (x, n, (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)), loc)
- | L.SgiClass (x, n, c) => SOME (L'.SgiCon (x, n, (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc),
- explifyCon c), loc)
+ | L.SgiClassAbs (x, n, k) => SOME (L'.SgiConAbs (x, n, (L'.KArrow (explifyKind k, (L'.KType, loc)), loc)), loc)
+ | L.SgiClass (x, n, k, c) => SOME (L'.SgiCon (x, n, (L'.KArrow (explifyKind k, (L'.KType, loc)), loc),
+ explifyCon c), loc)
and explifySgn (sgn, loc) =
case sgn of
@@ -172,8 +172,8 @@ fun explifyDecl (d, loc : EM.span) =
| L.DExport (en, sgn, str) => SOME (L'.DExport (en, explifySgn sgn, explifyStr str), loc)
| L.DTable (nt, x, n, c) => SOME (L'.DTable (nt, x, n, explifyCon c), loc)
| L.DSequence (nt, x, n) => SOME (L'.DSequence (nt, x, n), loc)
- | L.DClass (x, n, c) => SOME (L'.DCon (x, n,
- (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc), explifyCon c), loc)
+ | L.DClass (x, n, k, c) => SOME (L'.DCon (x, n,
+ (L'.KArrow (explifyKind k, (L'.KType, loc)), loc), explifyCon c), loc)
| L.DDatabase s => SOME (L'.DDatabase s, loc)
| L.DCookie (nt, x, n, c) => SOME (L'.DCookie (nt, x, n, explifyCon c), loc)
diff --git a/src/source.sml b/src/source.sml
index 7685bb2f..a5c86f66 100644
--- a/src/source.sml
+++ b/src/source.sml
@@ -81,8 +81,8 @@ datatype sgn_item' =
| SgiSgn of string * sgn
| SgiInclude of sgn
| SgiConstraint of con * con
- | SgiClassAbs of string
- | SgiClass of string * con
+ | SgiClassAbs of string * kind
+ | SgiClass of string * kind * con
and sgn' =
SgnConst of sgn_item list
@@ -154,7 +154,7 @@ datatype decl' =
| DExport of str
| DTable of string * con
| DSequence of string
- | DClass of string * con
+ | DClass of string * kind * con
| DDatabase of string
| DCookie of string * con
diff --git a/src/source_print.sml b/src/source_print.sml
index 77f2d749..d6568efe 100644
--- a/src/source_print.sml
+++ b/src/source_print.sml
@@ -413,17 +413,25 @@ fun p_sgn_item (sgi, _) =
string "~",
space,
p_con c2]
- | SgiClassAbs x => box [string "class",
- space,
- string x]
- | SgiClass (x, c) => box [string "class",
- space,
- string x,
- space,
- string "=",
- space,
- p_con c]
-
+ | SgiClassAbs (x, k) => box [string "class",
+ space,
+ string x,
+ space,
+ string "::",
+ space,
+ p_kind k]
+ | SgiClass (x, k, c) => box [string "class",
+ space,
+ string x,
+ space,
+ string "::",
+ space,
+ p_kind k,
+ space,
+ string "=",
+ space,
+ p_con c]
+
and p_sgn (sgn, _) =
case sgn of
SgnConst sgis => box [string "sig",
@@ -562,13 +570,13 @@ fun p_decl ((d, _) : decl) =
| DSequence x => box [string "sequence",
space,
string x]
- | DClass (x, c) => box [string "class",
- space,
- string x,
- space,
- string "=",
- space,
- p_con c]
+ | DClass (x, k, c) => box [string "class",
+ space,
+ string x,
+ space,
+ string "=",
+ space,
+ p_con c]
| DDatabase s => box [string "database",
space,
diff --git a/src/urweb.grm b/src/urweb.grm
index 7798b018..5f2c0575 100644
--- a/src/urweb.grm
+++ b/src/urweb.grm
@@ -410,13 +410,24 @@ decl : CON SYMBOL cargl2 kopt EQ cexp (let
| EXPORT spath ([(DExport spath, s (EXPORTleft, spathright))])
| TABLE SYMBOL COLON cexp ([(DTable (SYMBOL, entable cexp), s (TABLEleft, cexpright))])
| SEQUENCE SYMBOL ([(DSequence SYMBOL, s (SEQUENCEleft, SYMBOLright))])
- | CLASS SYMBOL EQ cexp ([(DClass (SYMBOL, cexp), s (CLASSleft, cexpright))])
+ | CLASS SYMBOL EQ cexp (let
+ val loc = s (CLASSleft, cexpright)
+ in
+ [(DClass (SYMBOL, (KWild, loc), cexp), loc)]
+ end)
+ | CLASS SYMBOL DCOLON kind EQ cexp ([(DClass (SYMBOL, kind, cexp), s (CLASSleft, cexpright))])
| CLASS SYMBOL SYMBOL EQ cexp (let
val loc = s (CLASSleft, cexpright)
- val k = (KType, loc)
+ val k = (KWild, loc)
val c = (CAbs (SYMBOL2, SOME k, cexp), loc)
in
- [(DClass (SYMBOL1, c), s (CLASSleft, cexpright))]
+ [(DClass (SYMBOL1, k, c), s (CLASSleft, cexpright))]
+ end)
+ | CLASS SYMBOL LPAREN SYMBOL DCOLON kind RPAREN EQ cexp (let
+ val loc = s (CLASSleft, cexpright)
+ val c = (CAbs (SYMBOL2, SOME kind, cexp), loc)
+ in
+ [(DClass (SYMBOL1, kind, c), s (CLASSleft, cexpright))]
end)
| COOKIE SYMBOL COLON cexp ([(DCookie (SYMBOL, cexp), s (COOKIEleft, cexpright))])
@@ -501,14 +512,38 @@ sgi : CON SYMBOL DCOLON kind (SgiConAbs (SYMBOL, kind), s (CONleft, k
in
(SgiVal (SYMBOL, t), loc)
end)
- | CLASS SYMBOL (SgiClassAbs SYMBOL, s (CLASSleft, SYMBOLright))
- | CLASS SYMBOL EQ cexp (SgiClass (SYMBOL, cexp), s (CLASSleft, cexpright))
+ | CLASS SYMBOL (let
+ val loc = s (CLASSleft, SYMBOLright)
+ in
+ (SgiClassAbs (SYMBOL, (KWild, loc)), loc)
+ end)
+ | CLASS SYMBOL DCOLON kind (let
+ val loc = s (CLASSleft, kindright)
+ in
+ (SgiClassAbs (SYMBOL, kind), loc)
+ end)
+ | CLASS SYMBOL EQ cexp (let
+ val loc = s (CLASSleft, cexpright)
+ in
+ (SgiClass (SYMBOL, (KWild, loc), cexp), loc)
+ end)
+ | CLASS SYMBOL DCOLON kind EQ cexp (let
+ val loc = s (CLASSleft, cexpright)
+ in
+ (SgiClass (SYMBOL, kind, cexp), loc)
+ end)
| CLASS SYMBOL SYMBOL EQ cexp (let
val loc = s (CLASSleft, cexpright)
- val k = (KType, loc)
+ val k = (KWild, loc)
val c = (CAbs (SYMBOL2, SOME k, cexp), loc)
in
- (SgiClass (SYMBOL1, c), s (CLASSleft, cexpright))
+ (SgiClass (SYMBOL1, k, c), s (CLASSleft, cexpright))
+ end)
+ | CLASS SYMBOL LPAREN SYMBOL DCOLON kind RPAREN EQ cexp (let
+ val loc = s (CLASSleft, cexpright)
+ val c = (CAbs (SYMBOL2, SOME kind, cexp), loc)
+ in
+ (SgiClass (SYMBOL1, kind, c), s (CLASSleft, cexpright))
end)
| COOKIE SYMBOL COLON cexp (let
val loc = s (COOKIEleft, cexpright)
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-13 07:02:48 +0000