aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/elab.sml1
-rw-r--r--src/elab_env.sml2
-rw-r--r--src/elab_print.sml2
-rw-r--r--src/elab_util.sml2
-rw-r--r--src/elaborate.sml96
-rw-r--r--src/explify.sml2
-rw-r--r--tests/group_by.lac2
7 files changed, 67 insertions, 40 deletions
diff --git a/src/elab.sml b/src/elab.sml
index 10f9bba6..30b53064 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -111,6 +111,7 @@ datatype exp' =
| ECase of exp * (pat * exp) list * { disc : con, result : con }
| EError
+ | EUnif of exp option ref
withtype exp = exp' located
diff --git a/src/elab_env.sml b/src/elab_env.sml
index 49eb1d86..936d8fce 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -363,6 +363,7 @@ fun class_name_in (c, _) =
case c of
CNamed n => SOME (ClNamed n)
| CModProj x => SOME (ClProj x)
+ | CUnif (_, _, _, ref (SOME c)) => class_name_in c
| _ => NONE
fun class_key_in (c, _) =
@@ -370,6 +371,7 @@ fun class_key_in (c, _) =
CRel n => SOME (CkRel n)
| CNamed n => SOME (CkNamed n)
| CModProj x => SOME (CkProj x)
+ | CUnif (_, _, _, ref (SOME c)) => class_key_in c
| _ => NONE
fun class_pair_in (c, _) =
diff --git a/src/elab_print.sml b/src/elab_print.sml
index 12abf6b0..72453f29 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -363,6 +363,8 @@ fun p_exp' par env (e, _) =
p_exp env e]) pes])
| EError => string "<ERROR>"
+ | EUnif (ref (SOME e)) => p_exp env e
+ | EUnif _ => string "_"
and p_exp env = p_exp' false env
diff --git a/src/elab_util.sml b/src/elab_util.sml
index 1c2ce4bd..327848a3 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -347,6 +347,8 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
(ECase (e', pes', {disc = disc', result = result'}), loc)))))
| EError => S.return2 eAll
+ | EUnif (ref (SOME e)) => mfe ctx e
+ | EUnif _ => S.return2 eAll
in
mfe
end
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 73889f74..97643170 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -1123,6 +1123,12 @@ fun foldType (dom, loc) =
(L'.CApp ((L'.CRel 1, loc), (L'.CRel 0, loc)), loc)), loc)),
loc)), loc)), loc)
+datatype constraint =
+ Disjoint of D.goal
+ | TypeClass of E.env * L'.con * L'.exp option ref * ErrorMsg.span
+
+val enD = map Disjoint
+
fun elabHead (env, denv) (e as (_, loc)) t =
let
fun unravel (t, e) =
@@ -1137,9 +1143,9 @@ fun elabHead (env, denv) (e as (_, loc)) t =
val (e, t, gs') = unravel (subConInCon (0, u) t',
(L'.ECApp (e, u), loc))
in
- (e, t, gs @ gs')
+ (e, t, enD gs @ gs')
end
- | _ => (e, t, gs)
+ | _ => (e, t, enD gs)
end
in
unravel (t, e)
@@ -1462,7 +1468,7 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
val (t', _, gs2) = elabCon (env, denv) t
val gs3 = checkCon (env, denv) e' et t'
in
- (e', t', gs1 @ gs2 @ gs3)
+ (e', t', gs1 @ enD gs2 @ enD gs3)
end
| L.EPrim p => ((L'.EPrim p, loc), primType env p, [])
@@ -1510,9 +1516,13 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
val (dom, gs4) = normClassConstraint (env, denv) dom
in
case E.resolveClass env dom of
- NONE => (expError env (Unresolvable (loc, dom));
- (eerror, cerror, []))
- | SOME pf => ((L'.EApp (e1', pf), loc), ran, gs1 @ gs2 @ gs3 @ gs4)
+ NONE =>
+ let
+ val r = ref NONE
+ in
+ ((L'.EUnif r, loc), ran, [TypeClass (env, dom, r, loc)])
+ end
+ | SOME pf => ((L'.EApp (e1', pf), loc), ran, gs1 @ gs2 @ enD gs3 @ enD gs4)
end
| _ => (expError env (OutOfContext (loc, SOME (e1', t1)));
(eerror, cerror, []))
@@ -1533,7 +1543,7 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
val gs4 = checkCon (env, denv) e1' t1 t
val gs5 = checkCon (env, denv) e2' t2 dom
- val gs = gs1 @ gs2 @ gs3 @ gs4 @ gs5
+ val gs = gs1 @ gs2 @ gs3 @ enD gs4 @ enD gs5
in
((L'.EApp (e1', e2'), loc), ran, gs)
end
@@ -1552,7 +1562,7 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
in
((L'.EAbs (x, t', et, e'), loc),
(L'.TFun (t', et), loc),
- gs1 @ gs2)
+ enD gs1 @ gs2)
end
| L.ECApp (e, c) =>
let
@@ -1570,7 +1580,7 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
handle SynUnif => (expError env (Unif ("substitution", eb));
cerror)
in
- ((L'.ECApp (e', c'), loc), eb', gs1 @ gs2 @ gs3 @ gs4)
+ ((L'.ECApp (e', c'), loc), eb', gs1 @ gs2 @ enD gs3 @ enD gs4)
end
| L'.CUnif _ =>
@@ -1606,7 +1616,7 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
checkKind env c1' k1 (L'.KRecord ku1, loc);
checkKind env c2' k2 (L'.KRecord ku2, loc);
- (e', (L'.TDisjoint (c1', c2', t), loc), gs1 @ gs2 @ gs3 @ gs4)
+ (e', (L'.TDisjoint (c1', c2', t), loc), enD gs1 @ enD gs2 @ enD gs3 @ gs4)
end
| L.ERecord xes =>
@@ -1617,7 +1627,7 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
val (e', et, gs2) = elabExp (env, denv) e
in
checkKind env x' xk kname;
- ((x', e', et), gs1 @ gs2 @ gs)
+ ((x', e', et), enD gs1 @ gs2 @ gs)
end)
[] xes
@@ -1641,10 +1651,13 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
in
prove (rest, gs)
end
+
+ val gsD = List.mapPartial (fn Disjoint d => SOME d | _ => NONE) gs
+ val gsO = List.filter (fn Disjoint _ => false | _ => true) gs
in
((L'.ERecord xes', loc),
(L'.TRecord (L'.CRecord (ktype, map (fn (x', _, et) => (x', et)) xes'), loc), loc),
- prove (xes', gs))
+ enD (prove (xes', gsD)) @ gsO)
end
| L.EField (e, c) =>
@@ -1661,7 +1674,7 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
(L'.TRecord (L'.CConcat (first, rest), loc), loc)
val gs4 = D.prove env denv (first, rest, loc)
in
- ((L'.EField (e', c', {field = ft, rest = rest}), loc), ft, gs1 @ gs2 @ gs3 @ gs4)
+ ((L'.EField (e', c', {field = ft, rest = rest}), loc), ft, gs1 @ enD gs2 @ enD gs3 @ enD gs4)
end
| L.ECut (e, c) =>
@@ -1678,7 +1691,8 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
(L'.TRecord (L'.CConcat (first, rest), loc), loc)
val gs4 = D.prove env denv (first, rest, loc)
in
- ((L'.ECut (e', c', {field = ft, rest = rest}), loc), (L'.TRecord rest, loc), gs1 @ gs2 @ gs3 @ gs4)
+ ((L'.ECut (e', c', {field = ft, rest = rest}), loc), (L'.TRecord rest, loc),
+ gs1 @ enD gs2 @ enD gs3 @ enD gs4)
end
| L.EFold =>
@@ -1701,7 +1715,7 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
val (e', et, gs2) = elabExp (env, denv) e
val gs3 = checkCon (env, denv) e' et result
in
- ((p', e'), gs1 @ gs2 @ gs3 @ gs)
+ ((p', e'), enD gs1 @ gs2 @ enD gs3 @ gs)
end)
gs1 pes
@@ -1712,7 +1726,7 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
else
expError env (Inexhaustive loc);
- ((L'.ECase (e', pes', {disc = et, result = result}), loc), result, gs' @ gs)
+ ((L'.ECase (e', pes', {disc = et, result = result}), loc), result, enD gs' @ gs)
end
end
@@ -2688,7 +2702,7 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
| _ => sgnError env (SgnWrongForm (sgn1, sgn2))
-fun elabDecl ((d, loc), (env, denv, gs)) =
+fun elabDecl ((d, loc), (env, denv, gs : constraint list)) =
case d of
L.DCon (x, ko, c) =>
let
@@ -2701,7 +2715,7 @@ fun elabDecl ((d, loc), (env, denv, gs)) =
in
checkKind env c' ck k';
- ([(L'.DCon (x, n, k', c'), loc)], (env', denv, gs' @ gs))
+ ([(L'.DCon (x, n, k', c'), loc)], (env', denv, enD gs' @ gs))
end
| L.DDatatype (x, xs, xcs) =>
let
@@ -2727,7 +2741,7 @@ fun elabDecl ((d, loc), (env, denv, gs)) =
val (t', tk, gs') = elabCon (env', denv') t'
in
checkKind env' t' tk k;
- (SOME t', (L'.TFun (t', t), loc), gs' @ gs)
+ (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
@@ -2762,7 +2776,7 @@ fun elabDecl ((d, loc), (env, denv, gs)) =
((L'.StrVar n, loc), sgn) ms
in
case hnormCon (env, denv) (L'.CModProj (n, ms, s), loc) of
- ((L'.CModProj (n, ms, s), _), gs) =>
+ ((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)))
@@ -2788,7 +2802,7 @@ fun elabDecl ((d, loc), (env, denv, gs)) =
E.pushENamedAs env x n t
end) env xncs
in
- ([(L'.DDatatypeImp (x, n', n, ms, s, xs, xncs), loc)], (env, denv, gs))
+ ([(L'.DDatatypeImp (x, n', n, ms, s, xs, xncs), loc)], (env, denv, enD gs' @ gs))
end)
| _ => (strError env (NotDatatype loc);
([], (env, denv, [])))
@@ -2807,7 +2821,7 @@ fun elabDecl ((d, loc), (env, denv, gs)) =
in
(*prefaces "DVal" [("x", Print.PD.string x),
("c'", p_con env c')];*)
- ([(L'.DVal (x, n, c', e'), loc)], (env', denv, gs1 @ gs2 @ gs3 @ gs4 @ gs))
+ ([(L'.DVal (x, n, c', e'), loc)], (env', denv, enD gs1 @ gs2 @ enD gs3 @ enD gs4 @ gs))
end
| L.DValRec vis =>
let
@@ -2818,7 +2832,7 @@ fun elabDecl ((d, loc), (env, denv, gs)) =
NONE => (cunif (loc, ktype), ktype, [])
| SOME c => elabCon (env, denv) c
in
- ((x, c', e), gs1 @ gs)
+ ((x, c', e), enD gs1 @ gs)
end) [] vis
val (vis, env) = ListUtil.foldlMap (fn ((x, c', e), env) =>
@@ -2834,7 +2848,7 @@ fun elabDecl ((d, loc), (env, denv, gs)) =
val gs2 = checkCon (env, denv) e' et c'
in
- ((x, n, c', e'), gs1 @ gs2 @ gs)
+ ((x, n, c', e'), gs1 @ enD gs2 @ gs)
end) gs vis
in
([(L'.DValRec vis, loc)], (env, denv, gs))
@@ -2845,7 +2859,7 @@ fun elabDecl ((d, loc), (env, denv, gs)) =
val (sgn', gs') = elabSgn (env, denv) sgn
val (env', n) = E.pushSgnNamed env x sgn'
in
- ([(L'.DSgn (x, n, sgn'), loc)], (env', denv, gs' @ gs))
+ ([(L'.DSgn (x, n, sgn'), loc)], (env', denv, enD gs' @ gs))
end
| L.DStr (x, sgno, str) =>
@@ -2906,7 +2920,7 @@ fun elabDecl ((d, loc), (env, denv, gs)) =
val (str', actual, gs2) = elabStr (env, denv) str
in
subSgn (env, denv) (selfifyAt env {str = str', sgn = actual}) formal;
- (str', formal, gs1 @ gs2)
+ (str', formal, enD gs1 @ gs2)
end
val (env', n) = E.pushStrNamed env x sgn'
@@ -2927,7 +2941,7 @@ fun elabDecl ((d, loc), (env, denv, gs)) =
val (env', n) = E.pushStrNamed env x sgn'
in
- ([(L'.DFfiStr (x, n, sgn'), loc)], (env', denv, gs' @ gs))
+ ([(L'.DFfiStr (x, n, sgn'), loc)], (env', denv, enD gs' @ gs))
end
| L.DOpen (m, ms) =>
@@ -2960,7 +2974,7 @@ fun elabDecl ((d, loc), (env, denv, gs)) =
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 @ gs4 @ gs))
+ ([(L'.DConstraint (c1', c2'), loc)], (env, denv', enD gs1 @ enD gs2 @ enD gs3 @ enD gs4 @ gs))
end
| L.DOpenConstraints (m, ms) =>
@@ -3027,7 +3041,7 @@ fun elabDecl ((d, loc), (env, denv, gs)) =
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, gs' @ gs))
+ ([(L'.DTable (!basis_r, x, n, c'), loc)], (env, denv, enD gs' @ gs))
end
| L.DClass (x, c) =>
@@ -3205,7 +3219,7 @@ and elabStr (env, denv) (str, loc) =
in
((L'.StrFun (m, n, dom', formal, str'), loc),
(L'.SgnFun (m, n, dom', formal), loc),
- gs1 @ gs2 @ gs3)
+ enD gs1 @ gs2 @ enD gs3)
end
| L.StrApp (str1, str2) =>
let
@@ -3282,15 +3296,19 @@ fun elabFile basis env file =
if ErrorMsg.anyErrors () then
()
else
- app (fn (loc, env, denv, c1, c2) =>
- case D.prove env denv (c1, c2, loc) of
- [] => ()
- | _ =>
- (ErrorMsg.errorAt loc "Couldn't prove field name disjointness";
- eprefaces' [("Con 1", p_con env c1),
- ("Con 2", p_con env c2),
- ("Hnormed 1", p_con env (ElabOps.hnormCon env c1)),
- ("Hnormed 2", p_con env (ElabOps.hnormCon env c2))])) gs;
+ app (fn Disjoint (loc, env, denv, c1, c2) =>
+ (case D.prove env denv (c1, c2, loc) of
+ [] => ()
+ | _ =>
+ (ErrorMsg.errorAt loc "Couldn't prove field name disjointness";
+ eprefaces' [("Con 1", p_con env c1),
+ ("Con 2", p_con env c2),
+ ("Hnormed 1", p_con env (ElabOps.hnormCon env c1)),
+ ("Hnormed 2", p_con env (ElabOps.hnormCon env c2))]))
+ | TypeClass (env, c, r, loc) =>
+ case E.resolveClass env c of
+ SOME e => r := SOME e
+ | NONE => expError env (Unresolvable (loc, c))) gs;
(L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan) :: ds @ file
end
diff --git a/src/explify.sml b/src/explify.sml
index f5d19a17..530f4b5f 100644
--- a/src/explify.sml
+++ b/src/explify.sml
@@ -112,6 +112,8 @@ fun explifyExp (e, loc) =
{disc = explifyCon disc, result = explifyCon result}), loc)
| L.EError => raise Fail ("explifyExp: EError at " ^ EM.spanToString loc)
+ | L.EUnif (ref (SOME e)) => explifyExp e
+ | L.EUnif _ => raise Fail ("explifyExp: Undetermined EUnif at " ^ EM.spanToString loc)
fun explifySgi (sgi, loc) =
case sgi of
diff --git a/tests/group_by.lac b/tests/group_by.lac
index 50cf553a..569676d5 100644
--- a/tests/group_by.lac
+++ b/tests/group_by.lac
@@ -8,4 +8,4 @@ val q3 = (SELECT * FROM t1 WHERE t1.A = 0 GROUP BY t1.B)
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 = 0 AND t2.D = 17)
+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)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-09 07:44:05 +0000