summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-08-31 15:04:10 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-08-31 15:04:10 -0400
commit0ca7aad45b1581ab86d136aaf7829418e093bb24 (patch)
treecea3dc87d8c098a2e61a5f6f4253020fbda34465
parentb145f505390243386da2992877a276edc8ab0256 (diff)
Monoized GROUP BY
-rw-r--r--src/elaborate.sml701
-rw-r--r--src/monoize.sml19
-rw-r--r--tests/group_by.ur20
-rw-r--r--tests/where.ur19
4 files changed, 413 insertions, 346 deletions
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 206c58cd..9fa22026 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -1681,6 +1681,7 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
val gsD = List.mapPartial (fn Disjoint d => SOME d | _ => NONE) gs
val gsO = List.filter (fn Disjoint _ => false | _ => true) gs
in
+ (*TextIO.print ("|gsO| = " ^ Int.toString (length gsO) ^ "\n");*)
((L'.ERecord xes', loc),
(L'.TRecord (L'.CRecord (ktype, map (fn (x', _, et) => (x', et)) xes'), loc), loc),
enD (prove (xes', gsD)) @ gsO)
@@ -2729,377 +2730,387 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
fun elabDecl ((d, loc), (env, denv, gs : constraint list)) =
- case d of
- L.DCon (x, ko, c) =>
- let
- val k' = case ko of
- NONE => kunif loc
- | SOME k => elabKind k
-
- val (c', ck, gs') = elabCon (env, denv) c
- val (env', n) = E.pushCNamed env x k' (SOME c')
- in
- checkKind env c' ck k';
-
- ([(L'.DCon (x, n, k', c'), loc)], (env', denv, enD gs' @ gs))
- end
- | L.DDatatype (x, xs, xcs) =>
- let
- val k = (L'.KType, loc)
- val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
- val (env, n) = E.pushCNamed env x k' NONE
- val t = (L'.CNamed n, loc)
- val nxs = length xs - 1
- val t = ListUtil.foldli (fn (i, _, t) => (L'.CApp (t, (L'.CRel (nxs - i), loc)), loc)) t xs
-
- val (env', denv') = foldl (fn (x, (env', denv')) =>
- (E.pushCRel env' x k,
- D.enter denv')) (env, denv) xs
-
- val (xcs, (used, env, gs)) =
- ListUtil.foldlMap
- (fn ((x, to), (used, env, gs)) =>
- let
- val (to, t, gs') = case to of
- NONE => (NONE, t, gs)
- | SOME t' =>
- let
- val (t', tk, gs') = elabCon (env', denv') t'
- in
- checkKind env' t' tk k;
- (SOME t', (L'.TFun (t', t), loc), enD gs' @ gs)
- end
- val t = foldr (fn (x, t) => (L'.TCFun (L'.Implicit, x, k, t), loc)) t xs
-
- val (env, n') = E.pushENamed env x t
- in
- if SS.member (used, x) then
- strError env (DuplicateConstructor (x, loc))
- else
- ();
- ((x, n', to), (SS.add (used, x), env, gs'))
- end)
- (SS.empty, env, []) xcs
-
- val env = E.pushDatatype env n xs xcs
- in
- ([(L'.DDatatype (x, n, xs, xcs), loc)], (env, denv, gs))
- end
-
- | L.DDatatypeImp (_, [], _) => raise Fail "Empty DDatatypeImp"
-
- | L.DDatatypeImp (x, m1 :: ms, s) =>
- (case E.lookupStr env m1 of
- NONE => (expError env (UnboundStrInExp (loc, m1));
- ([], (env, denv, gs)))
- | SOME (n, sgn) =>
- let
- val (str, sgn) = foldl (fn (m, (str, sgn)) =>
- case E.projectStr env {sgn = sgn, str = str, field = m} of
- NONE => (conError env (UnboundStrInCon (loc, m));
- (strerror, sgnerror))
- | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
- ((L'.StrVar n, loc), sgn) ms
- in
- case hnormCon (env, denv) (L'.CModProj (n, ms, s), loc) of
- ((L'.CModProj (n, ms, s), _), gs') =>
- (case E.projectDatatype env {sgn = sgn, str = str, field = s} of
- NONE => (conError env (UnboundDatatype (loc, s));
- ([], (env, denv, gs)))
- | SOME (xs, xncs) =>
- let
- val k = (L'.KType, loc)
- val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
- val t = (L'.CModProj (n, ms, s), loc)
- val (env, n') = E.pushCNamed env x k' (SOME t)
- val env = E.pushDatatype env n' xs xncs
+ let
+ (*val () = preface ("elabDecl", SourcePrint.p_decl (d, loc))*)
- val t = (L'.CNamed n', loc)
- val env = foldl (fn ((x, n, to), env) =>
- let
- val t = case to of
- NONE => t
- | SOME t' => (L'.TFun (t', t), loc)
+ val r =
+ case d of
+ L.DCon (x, ko, c) =>
+ let
+ val k' = case ko of
+ NONE => kunif loc
+ | SOME k => elabKind k
- val t = foldr (fn (x, t) =>
- (L'.TCFun (L'.Implicit, x, k, t), loc))
- t xs
- in
- E.pushENamedAs env x n t
- end) env xncs
- in
- ([(L'.DDatatypeImp (x, n', n, ms, s, xs, xncs), loc)], (env, denv, enD gs' @ gs))
- end)
- | _ => (strError env (NotDatatype loc);
- ([], (env, denv, [])))
- end)
+ val (c', ck, gs') = elabCon (env, denv) c
+ val (env', n) = E.pushCNamed env x k' (SOME c')
+ in
+ checkKind env c' ck k';
- | L.DVal (x, co, e) =>
- let
- val (c', _, gs1) = case co of
- NONE => (cunif (loc, ktype), ktype, [])
- | SOME c => elabCon (env, denv) c
+ ([(L'.DCon (x, n, k', c'), loc)], (env', denv, enD gs' @ gs))
+ end
+ | L.DDatatype (x, xs, xcs) =>
+ let
+ val k = (L'.KType, loc)
+ val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
+ val (env, n) = E.pushCNamed env x k' NONE
+ val t = (L'.CNamed n, loc)
+ val nxs = length xs - 1
+ val t = ListUtil.foldli (fn (i, _, t) => (L'.CApp (t, (L'.CRel (nxs - i), loc)), loc)) t xs
+
+ val (env', denv') = foldl (fn (x, (env', denv')) =>
+ (E.pushCRel env' x k,
+ D.enter denv')) (env, denv) xs
+
+ val (xcs, (used, env, gs')) =
+ ListUtil.foldlMap
+ (fn ((x, to), (used, env, gs)) =>
+ let
+ val (to, t, gs') = case to of
+ NONE => (NONE, t, gs)
+ | SOME t' =>
+ let
+ val (t', tk, gs') = elabCon (env', denv') t'
+ in
+ checkKind env' t' tk k;
+ (SOME t', (L'.TFun (t', t), loc), enD gs' @ gs)
+ end
+ val t = foldr (fn (x, t) => (L'.TCFun (L'.Implicit, x, k, t), loc)) t xs
+
+ val (env, n') = E.pushENamed env x t
+ in
+ if SS.member (used, x) then
+ strError env (DuplicateConstructor (x, loc))
+ else
+ ();
+ ((x, n', to), (SS.add (used, x), env, gs'))
+ end)
+ (SS.empty, env, []) xcs
- val (e', et, gs2) = elabExp (env, denv) e
- val gs3 = checkCon (env, denv) e' et c'
- val (c', gs4) = normClassConstraint (env, denv) c'
- val (env', n) = E.pushENamed env x c'
- in
- (*prefaces "DVal" [("x", Print.PD.string x),
- ("c'", p_con env c')];*)
- ([(L'.DVal (x, n, c', e'), loc)], (env', denv, enD gs1 @ gs2 @ enD gs3 @ enD gs4 @ gs))
- end
- | L.DValRec vis =>
- let
- fun allowable (e, _) =
- case e of
- L.EAbs _ => true
- | L.ECAbs (_, _, _, e) => allowable e
- | L.EDisjoint (_, _, e) => allowable e
- | _ => false
-
- val (vis, gs) = ListUtil.foldlMap
- (fn ((x, co, e), gs) =>
- let
- val (c', _, gs1) = case co of
- NONE => (cunif (loc, ktype), ktype, [])
- | SOME c => elabCon (env, denv) c
- in
- ((x, c', e), enD gs1 @ gs)
- end) [] vis
+ val env = E.pushDatatype env n xs xcs
+ in
+ ([(L'.DDatatype (x, n, xs, xcs), loc)], (env, denv, gs' @ gs))
+ end
- val (vis, env) = ListUtil.foldlMap (fn ((x, c', e), env) =>
- let
- val (env, n) = E.pushENamed env x c'
- in
- ((x, n, c', e), env)
- end) env vis
+ | L.DDatatypeImp (_, [], _) => raise Fail "Empty DDatatypeImp"
+
+ | L.DDatatypeImp (x, m1 :: ms, s) =>
+ (case E.lookupStr env m1 of
+ NONE => (expError env (UnboundStrInExp (loc, m1));
+ ([], (env, denv, gs)))
+ | SOME (n, sgn) =>
+ let
+ val (str, sgn) = foldl (fn (m, (str, sgn)) =>
+ case E.projectStr env {sgn = sgn, str = str, field = m} of
+ NONE => (conError env (UnboundStrInCon (loc, m));
+ (strerror, sgnerror))
+ | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
+ ((L'.StrVar n, loc), sgn) ms
+ in
+ case hnormCon (env, denv) (L'.CModProj (n, ms, s), loc) of
+ ((L'.CModProj (n, ms, s), _), gs') =>
+ (case E.projectDatatype env {sgn = sgn, str = str, field = s} of
+ NONE => (conError env (UnboundDatatype (loc, s));
+ ([], (env, denv, gs)))
+ | SOME (xs, xncs) =>
+ let
+ val k = (L'.KType, loc)
+ val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
+ val t = (L'.CModProj (n, ms, s), loc)
+ val (env, n') = E.pushCNamed env x k' (SOME t)
+ val env = E.pushDatatype env n' xs xncs
+
+ val t = (L'.CNamed n', loc)
+ val env = foldl (fn ((x, n, to), env) =>
+ let
+ val t = case to of
+ NONE => t
+ | SOME t' => (L'.TFun (t', t), loc)
+
+ val t = foldr (fn (x, t) =>
+ (L'.TCFun (L'.Implicit, x, k, t), loc))
+ t xs
+ in
+ E.pushENamedAs env x n t
+ end) env xncs
+ in
+ ([(L'.DDatatypeImp (x, n', n, ms, s, xs, xncs), loc)], (env, denv, enD gs' @ gs))
+ end)
+ | _ => (strError env (NotDatatype loc);
+ ([], (env, denv, [])))
+ end)
- val (vis, gs) = ListUtil.foldlMap (fn ((x, n, c', e), gs) =>
- let
- val (e', et, gs1) = elabExp (env, denv) e
-
- val gs2 = checkCon (env, denv) e' et c'
- in
- if allowable e then
- ()
- else
- expError env (IllegalRec (x, e'));
- ((x, n, c', e'), gs1 @ enD gs2 @ gs)
- end) gs vis
- in
- ([(L'.DValRec vis, loc)], (env, denv, gs))
- end
+ | L.DVal (x, co, e) =>
+ let
+ val (c', _, gs1) = case co of
+ NONE => (cunif (loc, ktype), ktype, [])
+ | SOME c => elabCon (env, denv) c
+
+ val (e', et, gs2) = elabExp (env, denv) e
+ val gs3 = checkCon (env, denv) e' et c'
+ val (c', gs4) = normClassConstraint (env, denv) c'
+ val (env', n) = E.pushENamed env x c'
+ in
+ (*prefaces "DVal" [("x", Print.PD.string x),
+ ("c'", p_con env c')];*)
+ ([(L'.DVal (x, n, c', e'), loc)], (env', denv, enD gs1 @ gs2 @ enD gs3 @ enD gs4 @ gs))
+ end
+ | L.DValRec vis =>
+ let
+ fun allowable (e, _) =
+ case e of
+ L.EAbs _ => true
+ | L.ECAbs (_, _, _, e) => allowable e
+ | L.EDisjoint (_, _, e) => allowable e
+ | _ => false
+
+ val (vis, gs) = ListUtil.foldlMap
+ (fn ((x, co, e), gs) =>
+ let
+ val (c', _, gs1) = case co of
+ NONE => (cunif (loc, ktype), ktype, [])
+ | SOME c => elabCon (env, denv) c
+ in
+ ((x, c', e), enD gs1 @ gs)
+ end) [] vis
+
+ val (vis, env) = ListUtil.foldlMap (fn ((x, c', e), env) =>
+ let
+ val (env, n) = E.pushENamed env x c'
+ in
+ ((x, n, c', e), env)
+ end) env vis
+
+ val (vis, gs) = ListUtil.foldlMap (fn ((x, n, c', e), gs) =>
+ let
+ val (e', et, gs1) = elabExp (env, denv) e
+
+ val gs2 = checkCon (env, denv) e' et c'
+ in
+ if allowable e then
+ ()
+ else
+ expError env (IllegalRec (x, e'));
+ ((x, n, c', e'), gs1 @ enD gs2 @ gs)
+ end) gs vis
+ in
+ ([(L'.DValRec vis, loc)], (env, denv, gs))
+ end
- | L.DSgn (x, sgn) =>
- let
- val (sgn', gs') = elabSgn (env, denv) sgn
- val (env', n) = E.pushSgnNamed env x sgn'
- in
- ([(L'.DSgn (x, n, sgn'), loc)], (env', denv, enD gs' @ gs))
- end
+ | L.DSgn (x, sgn) =>
+ let
+ val (sgn', gs') = elabSgn (env, denv) sgn
+ val (env', n) = E.pushSgnNamed env x sgn'
+ in
+ ([(L'.DSgn (x, n, sgn'), loc)], (env', denv, enD gs' @ gs))
+ end
- | L.DStr (x, sgno, str) =>
- let
- val () = if x = "Basis" then
- raise Fail "Not allowed to redefine structure 'Basis'"
- else
- ()
+ | L.DStr (x, sgno, str) =>
+ let
+ val () = if x = "Basis" then
+ raise Fail "Not allowed to redefine structure 'Basis'"
+ else
+ ()
- val formal = Option.map (elabSgn (env, denv)) sgno
+ val formal = Option.map (elabSgn (env, denv)) sgno
- val (str', sgn', gs') =
- case formal of
- NONE =>
- let
- val (str', actual, ds) = elabStr (env, denv) str
- in
- (str', selfifyAt env {str = str', sgn = actual}, ds)
- end
- | SOME (formal, gs1) =>
- let
- val str =
- case #1 (hnormSgn env formal) of
- L'.SgnConst sgis =>
- (case #1 str of
- L.StrConst ds =>
- let
- val needed = foldl (fn ((sgi, _), needed) =>
- case sgi of
- L'.SgiConAbs (x, _, _) => SS.add (needed, x)
- | _ => needed)
- SS.empty sgis
-
- val needed = foldl (fn ((d, _), needed) =>
- case d of
- L.DCon (x, _, _) => (SS.delete (needed, x)
- handle NotFound => needed)
- | L.DClass (x, _) => (SS.delete (needed, x)
- handle NotFound => needed)
- | L.DOpen _ => SS.empty
- | _ => needed)
- needed ds
- in
- case SS.listItems needed of
- [] => str
- | xs =>
+ val (str', sgn', gs') =
+ case formal of
+ NONE =>
+ let
+ val (str', actual, gs') = elabStr (env, denv) str
+ in
+ (str', selfifyAt env {str = str', sgn = actual}, gs')
+ end
+ | SOME (formal, gs1) =>
+ let
+ val str =
+ case #1 (hnormSgn env formal) of
+ L'.SgnConst sgis =>
+ (case #1 str of
+ L.StrConst ds =>
let
- val kwild = (L.KWild, #2 str)
- val cwild = (L.CWild kwild, #2 str)
- val ds' = map (fn x => (L.DCon (x, NONE, cwild), #2 str)) xs
+ val needed = foldl (fn ((sgi, _), needed) =>
+ case sgi of
+ L'.SgiConAbs (x, _, _) => SS.add (needed, x)
+ | _ => needed)
+ SS.empty sgis
+
+ val needed = foldl (fn ((d, _), needed) =>
+ case d of
+ L.DCon (x, _, _) => (SS.delete (needed, x)
+ handle NotFound =>
+ needed)
+ | L.DClass (x, _) => (SS.delete (needed, x)
+ handle NotFound => needed)
+ | L.DOpen _ => SS.empty
+ | _ => needed)
+ needed ds
in
- (L.StrConst (ds @ ds'), #2 str)
+ case SS.listItems needed of
+ [] => str
+ | xs =>
+ let
+ val kwild = (L.KWild, #2 str)
+ val cwild = (L.CWild kwild, #2 str)
+ val ds' = map (fn x => (L.DCon (x, NONE, cwild), #2 str)) xs
+ in
+ (L.StrConst (ds @ ds'), #2 str)
+ end
end
- end
- | _ => str)
- | _ => str
-
- val (str', actual, gs2) = elabStr (env, denv) str
- in
- subSgn (env, denv) (selfifyAt env {str = str', sgn = actual}) formal;
- (str', formal, enD gs1 @ gs2)
- end
+ | _ => str)
+ | _ => str
- val (env', n) = E.pushStrNamed env x sgn'
- in
- case #1 (hnormSgn env sgn') of
- L'.SgnFun _ =>
- (case #1 str' of
- L'.StrFun _ => ()
- | _ => strError env (FunctorRebind loc))
- | _ => ();
-
- ([(L'.DStr (x, n, sgn', str'), loc)], (env', denv, gs' @ gs))
- end
+ val (str', actual, gs2) = elabStr (env, denv) str
+ in
+ subSgn (env, denv) (selfifyAt env {str = str', sgn = actual}) formal;
+ (str', formal, enD gs1 @ gs2)
+ end
- | L.DFfiStr (x, sgn) =>
- let
- val (sgn', gs') = elabSgn (env, denv) sgn
+ val (env', n) = E.pushStrNamed env x sgn'
+ in
+ case #1 (hnormSgn env sgn') of
+ L'.SgnFun _ =>
+ (case #1 str' of
+ L'.StrFun _ => ()
+ | _ => strError env (FunctorRebind loc))
+ | _ => ();
+
+ ([(L'.DStr (x, n, sgn', str'), loc)], (env', denv, gs' @ gs))
+ end
- val (env', n) = E.pushStrNamed env x sgn'
- in
- ([(L'.DFfiStr (x, n, sgn'), loc)], (env', denv, enD gs' @ gs))
- end
+ | L.DFfiStr (x, sgn) =>
+ let
+ val (sgn', gs') = elabSgn (env, denv) sgn
- | L.DOpen (m, ms) =>
- (case E.lookupStr env m of
- NONE => (strError env (UnboundStr (loc, m));
- ([], (env, denv, gs)))
- | 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 (env', n) = E.pushStrNamed env x sgn'
+ in
+ ([(L'.DFfiStr (x, n, sgn'), loc)], (env', denv, enD gs' @ gs))
+ end
- val (ds, (env', denv')) = dopen (env, denv) {str = n, strs = ms, sgn = sgn}
- val denv' = dopenConstraints (loc, env', denv') {str = m, strs = ms}
- in
- (ds, (env', denv', gs))
- end)
+ | L.DOpen (m, ms) =>
+ (case E.lookupStr env m of
+ NONE => (strError env (UnboundStr (loc, m));
+ ([], (env, denv, gs)))
+ | 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', gs))
+ end)
- | L.DConstraint (c1, c2) =>
- let
- val (c1', k1, gs1) = elabCon (env, denv) c1
- val (c2', k2, gs2) = elabCon (env, denv) c2
- val gs3 = D.prove env denv (c1', c2', loc)
+ | L.DConstraint (c1, c2) =>
+ let
+ val (c1', k1, gs1) = elabCon (env, denv) c1
+ val (c2', k2, gs2) = elabCon (env, denv) c2
+ val gs3 = D.prove env denv (c1', c2', loc)
- val (denv', gs4) = 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);
+ val (denv', gs4) = 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', enD gs1 @ enD gs2 @ enD gs3 @ enD gs4 @ gs))
- end
+ ([(L'.DConstraint (c1', c2'), loc)], (env, denv', enD gs1 @ enD gs2 @ enD gs3 @ enD gs4 @ gs))
+ end
- | L.DOpenConstraints (m, ms) =>
- let
- val denv = dopenConstraints (loc, env, denv) {str = m, strs = ms}
- in
- ([], (env, denv, gs))
- end
+ | L.DOpenConstraints (m, ms) =>
+ let
+ val denv = dopenConstraints (loc, env, denv) {str = m, strs = ms}
+ in
+ ([], (env, denv, gs))
+ end
- | L.DExport str =>
- let
- val (str', sgn, gs') = elabStr (env, denv) str
+ | L.DExport str =>
+ let
+ val (str', sgn, gs') = elabStr (env, denv) str
- val sgn =
- case #1 (hnormSgn env sgn) of
- L'.SgnConst sgis =>
- let
- fun doOne (all as (sgi, _), env) =
- (case sgi of
- L'.SgiVal (x, n, t) =>
- (case hnormCon (env, denv) t of
- ((L'.TFun (dom, ran), _), []) =>
- (case (hnormCon (env, denv) dom, hnormCon (env, denv) ran) of
- (((L'.TRecord domR, _), []),
- ((L'.CApp (tf, arg), _), [])) =>
- (case (hnormCon (env, denv) tf, hnormCon (env, denv) arg) of
- (((L'.CModProj (basis, [], "transaction"), _), []),
- ((L'.CApp (tf, arg3), _), [])) =>
- (case (basis = !basis_r,
- hnormCon (env, denv) tf, hnormCon (env, denv) arg3) of
- (true,
- ((L'.CApp (tf, arg2), _), []),
- (((L'.CRecord (_, []), _), []))) =>
- (case (hnormCon (env, denv) tf) of
- ((L'.CApp (tf, arg1), _), []) =>
- (case (hnormCon (env, denv) tf,
- hnormCon (env, denv) domR,
- hnormCon (env, denv) arg1,
- hnormCon (env, denv) arg2) of
- ((tf, []), (domR, []), (arg1, []),
- ((L'.CRecord (_, []), _), [])) =>
- let
- val t = (L'.CApp (tf, arg1), loc)
- val t = (L'.CApp (t, arg2), loc)
- val t = (L'.CApp (t, arg3), loc)
- val t = (L'.CApp (
- (L'.CModProj (basis, [], "transaction"), loc),
- t), loc)
- in
- (L'.SgiVal (x, n, (L'.TFun ((L'.TRecord domR, loc),
- t),
- loc)), loc)
- end
- | _ => all)
- | _ => all)
- | _ => all)
- | _ => all)
- | _ => all)
- | _ => all)
- | _ => all,
- E.sgiBinds env all)
- in
- (L'.SgnConst (#1 (ListUtil.foldlMap doOne env sgis)), loc)
- end
- | _ => sgn
- in
- ([(L'.DExport (E.newNamed (), sgn, str'), loc)], (env, denv, gs' @ gs))
- end
+ val sgn =
+ case #1 (hnormSgn env sgn) of
+ L'.SgnConst sgis =>
+ let
+ fun doOne (all as (sgi, _), env) =
+ (case sgi of
+ L'.SgiVal (x, n, t) =>
+ (case hnormCon (env, denv) t of
+ ((L'.TFun (dom, ran), _), []) =>
+ (case (hnormCon (env, denv) dom, hnormCon (env, denv) ran) of
+ (((L'.TRecord domR, _), []),
+ ((L'.CApp (tf, arg), _), [])) =>
+ (case (hnormCon (env, denv) tf, hnormCon (env, denv) arg) of
+ (((L'.CModProj (basis, [], "transaction"), _), []),
+ ((L'.CApp (tf, arg3), _), [])) =>
+ (case (basis = !basis_r,
+ hnormCon (env, denv) tf, hnormCon (env, denv) arg3) of
+ (true,
+ ((L'.CApp (tf, arg2), _), []),
+ (((L'.CRecord (_, []), _), []))) =>
+ (case (hnormCon (env, denv) tf) of
+ ((L'.CApp (tf, arg1), _), []) =>
+ (case (hnormCon (env, denv) tf,
+ hnormCon (env, denv) domR,
+ hnormCon (env, denv) arg1,
+ hnormCon (env, denv) arg2) of
+ ((tf, []), (domR, []), (arg1, []),
+ ((L'.CRecord (_, []), _), [])) =>
+ let
+ val t = (L'.CApp (tf, arg1), loc)
+ val t = (L'.CApp (t, arg2), loc)
+ val t = (L'.CApp (t, arg3), loc)
+ val t = (L'.CApp (
+ (L'.CModProj
+ (basis, [], "transaction"), loc),
+ t), loc)
+ in
+ (L'.SgiVal (x, n, (L'.TFun ((L'.TRecord domR,
+ loc),
+ t),
+ loc)), loc)
+ end
+ | _ => all)
+ | _ => all)
+ | _ => all)
+ | _ => all)
+ | _ => all)
+ | _ => all)
+ | _ => all,
+ E.sgiBinds env all)
+ in
+ (L'.SgnConst (#1 (ListUtil.foldlMap doOne env sgis)), loc)
+ end
+ | _ => sgn
+ in
+ ([(L'.DExport (E.newNamed (), sgn, str'), loc)], (env, denv, gs' @ gs))
+ end
- | L.DTable (x, c) =>
- let
- val (c', k, gs') = elabCon (env, denv) c
- val (env, n) = E.pushENamed env x (L'.CApp (tableOf (), c'), loc)
- in
- checkKind env c' k (L'.KRecord (L'.KType, loc), loc);
- ([(L'.DTable (!basis_r, x, n, c'), loc)], (env, denv, enD gs' @ gs))
- end
+ | L.DTable (x, c) =>
+ let
+ val (c', k, gs') = elabCon (env, denv) c
+ val (env, n) = E.pushENamed env x (L'.CApp (tableOf (), c'), loc)
+ in
+ checkKind env c' k (L'.KRecord (L'.KType, loc), loc);
+ ([(L'.DTable (!basis_r, x, n, c'), loc)], (env, denv, enD gs' @ gs))
+ end
- | L.DClass (x, c) =>
- let
- val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
- 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, c'), loc)], (env, denv, []))
- end
+ | L.DClass (x, c) =>
+ let
+ val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
+ 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, c'), loc)], (env, denv, []))
+ end
+ in
+ r
+ end
and elabStr (env, denv) (str, loc) =
case str of
diff --git a/src/monoize.sml b/src/monoize.sml
index 7344c22f..5341ab99 100644
--- a/src/monoize.sml
+++ b/src/monoize.sml
@@ -614,7 +614,24 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
strcatComma loc (map (fn (x, _) => strcat loc [(L'.EField (gf "From", x), loc),
sc (" AS " ^ x)]) tables),
sc " WHERE ",
- gf "Where"
+ gf "Where",
+ if List.all (fn (x, xts) =>
+ case List.find (fn (x', _) => x' = x) grouped of
+ NONE => List.null xts
+ | SOME (_, xts') =>
+ List.all (fn (x, _) =>
+ List.exists (fn (x', _) => x' = x)
+ xts') xts) tables then
+ sc ""
+ else
+ strcat loc [
+ sc " GROUP BY ",
+ strcatComma loc (map (fn (x, xts) =>
+ strcatComma loc
+ (map (fn (x', _) =>
+ sc (x ^ "." ^ x'))
+ xts)) grouped)
+ ]
]), loc),
fm)
| _ => poly ()
diff --git a/tests/group_by.ur b/tests/group_by.ur
index 569676d5..93655568 100644
--- a/tests/group_by.ur
+++ b/tests/group_by.ur
@@ -9,3 +9,23 @@ val q4 = (SELECT * FROM t1 WHERE t1.A = 0 GROUP BY t1.C HAVING t1.C < 0.2)
val q5 = (SELECT t1.A, t2.D FROM t1, t2 GROUP BY t2.D, t1.A)
val q6 = (SELECT t1.A, t2.D FROM t1, t2 WHERE t1.C = 0.0 GROUP BY t2.D, t1.A HAVING t1.A = t1.A AND t2.D = 17)
+
+
+datatype list a = Nil | Cons of a * list a
+
+val r1 : transaction (list {B : string}) =
+ query q1
+ (fn fs acc => return (Cons (fs.T1, acc)))
+ Nil
+
+val r2 : transaction string =
+ ls <- r1;
+ return (case ls of
+ Nil => "Problem"
+ | Cons ({B = b, ...}, _) => b)
+
+val main : unit -> transaction page = fn () =>
+ s <- r2;
+ return <html><body>
+ {cdata s}
+ </body></html>
diff --git a/tests/where.ur b/tests/where.ur
index ab430941..8b4d89c5 100644
--- a/tests/where.ur
+++ b/tests/where.ur
@@ -9,3 +9,22 @@ val q5 = (SELECT * FROM t1 WHERE {1} = {1})
val q6 = (SELECT * FROM t1 WHERE {"Hi"} < {"Bye"})
val q7 = (SELECT * FROM t1 WHERE {1} <> {1} AND NOT ({"Hi"} >= {"Bye"}))
val q8 = (SELECT * FROM t1 WHERE t1.A = 1 OR t1.C < 3.0)
+
+datatype list a = Nil | Cons of a * list a
+
+val r1 : transaction (list {A : int, B : string, C : float}) =
+ query q8
+ (fn fs acc => return (Cons (fs.T1, acc)))
+ Nil
+
+val r2 : transaction string =
+ ls <- r1;
+ return (case ls of
+ Nil => "Problem"
+ | Cons ({B = b, ...}, _) => b)
+
+val main : unit -> transaction page = fn () =>
+ s <- r2;
+ return <html><body>
+ {cdata s}
+ </body></html>