summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/elab.sml1
-rw-r--r--src/elab_env.sml7
-rw-r--r--src/elab_print.sml11
-rw-r--r--src/elab_util.sml10
-rw-r--r--src/elaborate.sml18
-rw-r--r--src/explify.sml2
-rw-r--r--src/source.sml1
-rw-r--r--src/source_print.sml7
-rw-r--r--src/unnest.sml1
-rw-r--r--src/urweb.grm19
10 files changed, 3 insertions, 74 deletions
diff --git a/src/elab.sml b/src/elab.sml
index 15365951..9147f7d3 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -175,7 +175,6 @@ datatype decl' =
| DTable of int * string * int * con * exp * con * exp * con
| DSequence of int * string * int
| DView of int * string * int * exp * con
- | DClass of string * int * kind * con
| DDatabase of string
| DCookie of int * string * int * con
| DStyle of int * string * int
diff --git a/src/elab_env.sml b/src/elab_env.sml
index f31804f2..5d684817 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -1647,13 +1647,6 @@ fun declBinds env (d, loc) =
in
pushENamedAs env x n ct
end
- | DClass (x, n, k, c) =>
- let
- val k = (KArrow (k, (KType, loc)), loc)
- val env = pushCNamedAs env x n k (SOME c)
- in
- pushClass env n
- end
| DDatabase _ => env
| DCookie (tn, x, n, c) =>
let
diff --git a/src/elab_print.sml b/src/elab_print.sml
index 37669312..c32368a9 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -828,17 +828,6 @@ fun p_decl env (dAll as (d, _) : decl) =
string "as",
space,
p_exp env e]
- | DClass (x, n, k, c) => box [string "class",
- space,
- p_named x n,
- space,
- string "::",
- space,
- p_kind env 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 97e3b572..51bcba5a 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -919,8 +919,6 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f
in
bind (ctx, NamedE (x, ct))
end
- | DClass (x, n, k, c) =>
- bind (ctx, NamedC (x, n, (KArrow (k, (KType, loc)), loc), SOME c))
| DDatabase _ => ctx
| DCookie (tn, x, n, c) =>
bind (ctx, NamedE (x, (CApp ((CModProj (n, [], "cookie"), loc),
@@ -1040,13 +1038,6 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f
fn c' =>
(DView (tn, x, n, e', c'), loc)))
- | DClass (x, n, k, c) =>
- S.bind2 (mfk ctx k,
- fn k' =>
- S.map2 (mfc ctx c,
- fn c' =>
- (DClass (x, n, k', c'), loc)))
-
| DDatabase _ => S.return2 dAll
| DCookie (tn, x, n, c) =>
@@ -1233,7 +1224,6 @@ and maxNameDecl (d, _) =
| DSgn (_, n, sgn) => Int.max (n, maxNameSgn sgn)
| DFfiStr (_, n, sgn) => Int.max (n, maxNameSgn sgn)
| DConstraint _ => 0
- | DClass (_, n, _, _) => n
| DExport _ => 0
| DTable (n1, _, n2, _, _, _, _, _) => Int.max (n1, n2)
| DSequence (n1, _, n2) => Int.max (n1, n2)
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 8436c975..426934bd 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -2982,7 +2982,6 @@ and sgiOfDecl (d, loc) =
| L'.DSequence (tn, x, n) => [(L'.SgiVal (x, n, sequenceOf ()), loc)]
| L'.DView (tn, x, n, _, c) =>
[(L'.SgiVal (x, n, (L'.CApp (viewOf (), c), loc)), 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)]
| L'.DStyle (tn, x, n) => [(L'.SgiVal (x, n, styleOf ()), loc)]
@@ -3362,6 +3361,8 @@ and subSgn' counterparts env strLoc sgn1 (sgn2 as (_, loc2)) =
case sgi1 of
L'.SgiClassAbs (x', n1, k1) => found (x', n1, k1, NONE)
| L'.SgiClass (x', n1, k1, c) => found (x', n1, k1, SOME c)
+ | L'.SgiConAbs (x', n1, k1) => found (x', n1, k1, NONE)
+ | L'.SgiCon (x', n1, k1, c) => found (x', n1, k1, SOME c)
| _ => NONE
end)
| L'.SgiClass (x, n2, k2, c2) =>
@@ -3401,6 +3402,7 @@ and subSgn' counterparts env strLoc sgn1 (sgn2 as (_, loc2)) =
in
case sgi1 of
L'.SgiClass (x', n1, k1, c1) => found (x', n1, k1, c1)
+ | L'.SgiCon (x', n1, k1, c1) => found (x', n1, k1, c1)
| _ => NONE
end)
end
@@ -3508,7 +3510,6 @@ and wildifyStr env (str, sgn) =
fun dname (d, _) =
case d of
L.DCon (x, _, _) => SOME x
- | L.DClass (x, _, _) => SOME x
| _ => NONE
fun decompileKind (k, loc) =
@@ -3641,7 +3642,6 @@ and wildifyStr env (str, sgn) =
foldl (fn ((d, _), nd) =>
case d of
L.DCon (x, _, _) => ndelCon (nd, x)
- | L.DClass (x, _, _) => ndelCon (nd, x)
| L.DVal (x, _, _) => ndelVal (nd, x)
| L.DOpen _ => nempty
| L.DStr (x, _, _, (L.StrConst ds', _)) =>
@@ -3666,7 +3666,6 @@ and wildifyStr env (str, sgn) =
| L.DDatatypeImp _ => true
| L.DStr _ => true
| L.DConstraint _ => true
- | L.DClass _ => true
| _ => false
in
if isCony then
@@ -4184,17 +4183,6 @@ and elabDecl (dAll as (d, loc), (env, denv, gs)) =
(env', denv, gs' @ gs))
end
- | L.DClass (x, k, c) =>
- let
- val k = elabKind env k
- val (c', ck, gs') = elabCon (env, denv) 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, k, c'), loc)], (env, denv, enD gs' @ gs))
- end
-
| L.DDatabase s => ([(L'.DDatabase s, loc)], (env, denv, gs))
| L.DCookie (x, c) =>
diff --git a/src/explify.sml b/src/explify.sml
index 3c922a44..65e78443 100644
--- a/src/explify.sml
+++ b/src/explify.sml
@@ -192,8 +192,6 @@ fun explifyDecl (d, loc : EM.span) =
| L.DView (nt, x, n, e, c) =>
SOME (L'.DView (nt, x, n, explifyExp e, explifyCon c), loc)
| L.DSequence (nt, x, n) => SOME (L'.DSequence (nt, x, n), 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)
| L.DStyle (nt, x, n) => SOME (L'.DStyle (nt, x, n), loc)
diff --git a/src/source.sml b/src/source.sml
index 8b126628..18f83d2b 100644
--- a/src/source.sml
+++ b/src/source.sml
@@ -163,7 +163,6 @@ datatype decl' =
| DTable of string * con * exp * exp
| DSequence of string
| DView of string * exp
- | DClass of string * kind * con
| DDatabase of string
| DCookie of string * con
| DStyle of string
diff --git a/src/source_print.sml b/src/source_print.sml
index aad673f3..cd3314e1 100644
--- a/src/source_print.sml
+++ b/src/source_print.sml
@@ -640,13 +640,6 @@ fun p_decl ((d, _) : decl) =
string "=",
space,
p_exp e]
- | 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/unnest.sml b/src/unnest.sml
index 2d6956cb..52d729d7 100644
--- a/src/unnest.sml
+++ b/src/unnest.sml
@@ -428,7 +428,6 @@ fun unnest file =
| DTable _ => default ()
| DSequence _ => default ()
| DView _ => default ()
- | DClass _ => default ()
| DDatabase _ => default ()
| DCookie _ => default ()
| DStyle _ => default ()
diff --git a/src/urweb.grm b/src/urweb.grm
index 708e5fcd..084cec1e 100644
--- a/src/urweb.grm
+++ b/src/urweb.grm
@@ -602,25 +602,6 @@ decl : CON SYMBOL cargl2 kopt EQ cexp (let
s (VIEWleft, queryright))])
| VIEW SYMBOL EQ LBRACE eexp RBRACE ([(DView (SYMBOL, eexp),
s (VIEWleft, RBRACEright))])
- | 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 = (KWild, loc)
- val c = (CAbs (SYMBOL2, SOME k, cexp), loc)
- in
- [(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))])
| STYLE SYMBOL ([(DStyle SYMBOL, s (STYLEleft, SYMBOLright))])
| TASK eapps EQ eexp ([(DTask (eapps, eexp), s (TASKleft, eexpright))])
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-05 02:35:02 +0000