diff options
| -rw-r--r-- | src/elab.sml | 6 | ||||
| -rw-r--r-- | src/elab_env.sml | 36 | ||||
| -rw-r--r-- | src/elab_print.sml | 46 | ||||
| -rw-r--r-- | src/elab_util.sml | 43 | ||||
| -rw-r--r-- | src/elaborate.sml | 115 | ||||
| -rw-r--r-- | src/explify.sml | 10 | ||||
| -rw-r--r-- | src/source.sml | 6 | ||||
| -rw-r--r-- | src/source_print.sml | 44 | ||||
| -rw-r--r-- | src/urweb.grm | 49 |
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) |