summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/elab.sml4
-rw-r--r--src/elab_env.sml30
-rw-r--r--src/elab_print.sml28
-rw-r--r--src/elab_util.sml12
-rw-r--r--src/elaborate.sml161
-rw-r--r--tests/table.lac13
6 files changed, 178 insertions, 70 deletions
diff --git a/src/elab.sml b/src/elab.sml
index 25ec6a79..66f5f3ed 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -119,7 +119,7 @@ datatype sgn_item' =
| SgiStr of string * int * sgn
| SgiSgn of string * int * sgn
| SgiConstraint of con * con
- | SgiTable of string * int * con
+ | SgiTable of int * string * int * con
and sgn' =
SgnConst of sgn_item list
@@ -143,7 +143,7 @@ datatype decl' =
| DFfiStr of string * int * sgn
| DConstraint of con * con
| DExport of int * sgn * str
- | DTable of string * int * con
+ | DTable of int * string * int * con
and str' =
StrConst of decl list
diff --git a/src/elab_env.sml b/src/elab_env.sml
index 2d6afa4a..acd918ec 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -404,15 +404,12 @@ fun sgiBinds env (sgi, loc) =
| SgiSgn (x, n, sgn) => pushSgnNamedAs env x n sgn
| SgiConstraint _ => env
- | SgiTable (x, n, c) =>
- (case lookupStr env "Basis" of
- NONE => raise Fail "ElabEnv.sgiBinds: Can't find Basis"
- | SOME (n, _) =>
- let
- val t = (CApp ((CModProj (n, [], "table"), loc), c), loc)
- in
- pushENamedAs env x n t
- end)
+ | SgiTable (tn, x, n, c) =>
+ let
+ val t = (CApp ((CModProj (tn, [], "table"), loc), c), loc)
+ in
+ pushENamedAs env x n t
+ end
fun sgnSeek f sgis =
let
@@ -737,14 +734,11 @@ fun declBinds env (d, loc) =
| DFfiStr (x, n, sgn) => pushStrNamedAs env x n sgn
| DConstraint _ => env
| DExport _ => env
- | DTable (x, n, c) =>
- (case lookupStr env "Basis" of
- NONE => raise Fail "ElabEnv.declBinds: Can't find Basis"
- | SOME (n, _) =>
- let
- val t = (CApp ((CModProj (n, [], "table"), loc), c), loc)
- in
- pushENamedAs env x n t
- end)
+ | DTable (tn, x, n, c) =>
+ let
+ val t = (CApp ((CModProj (tn, [], "table"), loc), c), loc)
+ in
+ pushENamedAs env x n t
+ end
end
diff --git a/src/elab_print.sml b/src/elab_print.sml
index a46a642a..6c42351c 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -447,13 +447,13 @@ fun p_sgn_item env (sgi, _) =
string "~",
space,
p_con env c2]
- | SgiTable (x, n, c) => box [string "table",
- space,
- p_named x n,
- space,
- string ":",
- space,
- p_con env c]
+ | SgiTable (_, x, n, c) => box [string "table",
+ space,
+ p_named x n,
+ space,
+ string ":",
+ space,
+ p_con env c]
and p_sgn env (sgn, _) =
case sgn of
@@ -603,13 +603,13 @@ fun p_decl env (dAll as (d, _) : decl) =
string ":",
space,
p_sgn env sgn]
- | DTable (x, n, c) => box [string "table",
- space,
- p_named x n,
- space,
- string ":",
- space,
- p_con env c]
+ | DTable (_, x, n, c) => box [string "table",
+ space,
+ p_named x n,
+ space,
+ string ":",
+ space,
+ p_con env c]
and p_str env (str, _) =
case str of
diff --git a/src/elab_util.sml b/src/elab_util.sml
index 8cd02549..3c1860c7 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -436,10 +436,10 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
S.map2 (con ctx c2,
fn c2' =>
(SgiConstraint (c1', c2'), loc)))
- | SgiTable (x, n, c) =>
+ | SgiTable (tn, x, n, c) =>
S.map2 (con ctx c,
fn c' =>
- (SgiTable (x, n, c'), loc))
+ (SgiTable (tn, x, n, c'), loc))
and sg ctx s acc =
S.bindP (sg' ctx s acc, sgn ctx)
@@ -600,7 +600,9 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f
bind (ctx, Str (x, sgn))
| DConstraint _ => ctx
| DExport _ => ctx
- | DTable _ => ctx,
+ | DTable (tn, x, n, c) =>
+ bind (ctx, NamedE (x, (CApp ((CModProj (n, [], "table"), loc),
+ c), loc))),
mfd ctx d)) ctx ds,
fn ds' => (StrConst ds', loc))
| StrVar _ => S.return2 strAll
@@ -688,10 +690,10 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f
fn str' =>
(DExport (en, sgn', str'), loc)))
- | DTable (x, n, c) =>
+ | DTable (tn, x, n, c) =>
S.map2 (mfc ctx c,
fn c' =>
- (DTable (x, n, c'), loc))
+ (DTable (tn, x, n, c'), loc))
and mfvi ctx (x, n, c, e) =
S.bind2 (mfc ctx c,
diff --git a/src/elaborate.sml b/src/elaborate.sml
index b6073e7f..be23b41a 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -558,6 +558,40 @@ fun kindof env (c, loc) =
val hnormCon = D.hnormCon
+datatype con_summary =
+ Nil
+ | Cons
+ | Unknown
+
+fun compatible cs =
+ case cs of
+ (Unknown, _) => false
+ | (_, Unknown) => false
+ | (s1, s2) => s1 = s2
+
+fun summarizeCon (env, denv) c =
+ let
+ val (c, gs) = hnormCon (env, denv) c
+ in
+ case #1 c of
+ L'.CRecord (_, []) => (Nil, gs)
+ | L'.CRecord (_, _ :: _) => (Cons, gs)
+ | L'.CConcat ((L'.CRecord (_, _ :: _), _), _) => (Cons, gs)
+ | L'.CDisjoint (_, _, c) =>
+ let
+ val (s, gs') = summarizeCon (env, denv) c
+ in
+ (s, gs @ gs')
+ end
+ | _ => (Unknown, gs)
+ end
+
+fun p_con_summary s =
+ Print.PD.string (case s of
+ Nil => "Nil"
+ | Cons => "Cons"
+ | Unknown => "Unknown")
+
fun unifyRecordCons (env, denv) (c1, c2) =
let
fun rkindof c =
@@ -705,12 +739,77 @@ and unifyCons' (env, denv) c1 c2 =
let
val (c1, gs1) = hnormCon (env, denv) c1
val (c2, gs2) = hnormCon (env, denv) c2
- val gs3 = unifyCons'' (env, denv) c1 c2
in
- gs1 @ gs2 @ gs3
+ let
+ val gs3 = unifyCons'' (env, denv) c1 c2
+ in
+ gs1 @ gs2 @ gs3
+ end
+ handle ex =>
+ let
+ val loc = #2 c1
+
+ fun unfold (dom, f, i, r, c) =
+ let
+ val nm = cunif (loc, (L'.KName, loc))
+ val v = cunif (loc, dom)
+ val rest = cunif (loc, (L'.KRecord dom, loc))
+
+ val (iS, gs3) = summarizeCon (env, denv) i
+
+ val app = (L'.CApp (f, nm), loc)
+ val app = (L'.CApp (app, v), loc)
+ val app = (L'.CApp (app, rest), loc)
+ val (appS, gs4) = summarizeCon (env, denv) app
+
+ val (cS, gs5) = summarizeCon (env, denv) c
+ in
+ (*prefaces "Summaries" [("iS", p_con_summary iS),
+ ("appS", p_con_summary appS),
+ ("cS", p_con_summary cS)];*)
+
+ if compatible (iS, appS) then
+ raise ex
+ else if compatible (cS, iS) then
+ let
+ (*val () = prefaces "Same?" [("i", p_con env i),
+ ("c", p_con env c)]*)
+ val gs6 = unifyCons (env, denv) i c
+ (*val () = TextIO.print "Yes!\n"*)
+
+ val gs7 = unifyCons (env, denv) r (L'.CRecord (dom, []), loc)
+ in
+ gs1 @ gs2 @ gs3 @ gs4 @ gs5 @ gs6 @ gs7
+ end
+ else if compatible (cS, appS) then
+ let
+ (*val () = prefaces "Same?" [("app", p_con env app),
+ ("c", p_con env c),
+ ("app'", p_con env (#1 (hnormCon (env, denv) app)))]*)
+ val gs6 = unifyCons (env, denv) app c
+ (*val () = TextIO.print "Yes!\n"*)
+
+ val singleton = (L'.CRecord (dom, [(nm, v)]), loc)
+ val concat = (L'.CConcat (singleton, rest), loc)
+ val gs7 = unifyCons (env, denv) r concat
+ in
+ (loc, env, denv, singleton, rest) :: gs1 @ gs2 @ gs3 @ gs4 @ gs5 @ gs6 @ gs7
+ end
+ else
+ raise ex
+ end
+ handle _ => raise ex
+ in
+ case (#1 c1, #1 c2) of
+ (L'.CApp ((L'.CApp ((L'.CApp ((L'.CFold (dom, _), _), f), _), i), _), r), _) =>
+ unfold (dom, f, i, r, c2)
+ | (_, L'.CApp ((L'.CApp ((L'.CApp ((L'.CFold (dom, _), _), f), _), i), _), r)) =>
+ unfold (dom, f, i, r, c1)
+ | _ => raise ex
+ end
end
-and unifyCons'' (env, denv) (c1All as (c1, _)) (c2All as (c2, _)) =
+and unifyCons'' (env, denv) (c1All as (c1, loc)) (c2All as (c2, _)) =
let
fun err f = raise CUnify' (f (c1All, c2All))
@@ -794,12 +893,12 @@ and unifyCons'' (env, denv) (c1All as (c1, _)) (c2All as (c2, _)) =
(r := SOME c1All;
[])
-
| (L'.CFold (dom1, ran1), L'.CFold (dom2, ran2)) =>
(unifyKinds dom1 dom2;
unifyKinds ran1 ran2;
[])
+
| _ => err CIncompatible
end
@@ -1264,8 +1363,10 @@ 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
in
- ((L'.EApp (e1', e2'), loc), ran, gs1 @ gs2 @ gs3 @ gs4 @ gs5)
+ ((L'.EApp (e1', e2'), loc), ran, gs)
end
| L.EAbs (x, to, e) =>
let
@@ -1571,6 +1672,13 @@ fun strError env err =
val hnormSgn = E.hnormSgn
+fun tableOf' env =
+ case E.lookupStr env "Basis" of
+ NONE => raise Fail "Elaborate.tableOf: Can't find Basis"
+ | SOME (n, _) => n
+
+fun tableOf env = (L'.CModProj (tableOf' env, [], "sql_table"), ErrorMsg.dummySpan)
+
fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
case sgi of
L.SgiConAbs (x, k) =>
@@ -1739,10 +1847,10 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
| L.SgiTable (x, c) =>
let
val (c', k, gs) = elabCon (env, denv) c
- val (env, n) = E.pushENamed env x c'
+ val (env, n) = E.pushENamed env x (L'.CApp (tableOf env, c'), loc)
in
checkKind env c' k (L'.KRecord (L'.KType, loc), loc);
- ([(L'.SgiTable (x, n, c'), loc)], (env, denv, gs))
+ ([(L'.SgiTable (tableOf' env, x, n, c'), loc)], (env, denv, gs))
end
and elabSgn (env, denv) (sgn, loc) =
@@ -1806,7 +1914,7 @@ and elabSgn (env, denv) (sgn, loc) =
();
(cons, vals, sgns, SS.add (strs, x)))
| L'.SgiConstraint _ => (cons, vals, sgns, strs)
- | L'.SgiTable (x, _, _) =>
+ | L'.SgiTable (_, x, _, _) =>
(if SS.member (vals, x) then
sgnError env (DuplicateVal (loc, x))
else
@@ -1910,11 +2018,6 @@ fun selfifyAt env {str, sgn} =
| SOME (str, strs) => selfify env {sgn = sgn, str = str, strs = strs}
end
-fun tableOf env =
- case E.lookupStr env "Basis" of
- NONE => raise Fail "Elaborate.tableOf: Can't find Basis"
- | SOME (n, _) => (L'.CModProj (n, [], "sql_table"), ErrorMsg.dummySpan)
-
fun dopen (env, denv) {str, strs, sgn} =
let
val m = foldl (fn (m, str) => (L'.StrProj (str, m), #2 sgn))
@@ -1946,7 +2049,7 @@ 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'.SgiTable (x, n, c) =>
+ | L'.SgiTable (_, x, n, c) =>
(L'.DVal (x, n, (L'.CApp (tableOf env, c), loc),
(L'.EModProj (str, strs, x), loc)), loc)
in
@@ -2001,7 +2104,7 @@ fun sgiOfDecl (d, loc) =
| L'.DFfiStr (x, n, sgn) => [(L'.SgiStr (x, n, sgn), loc)]
| L'.DConstraint cs => [(L'.SgiConstraint cs, loc)]
| L'.DExport _ => []
- | L'.DTable (x, n, c) => [(L'.SgiTable (x, n, c), loc)]
+ | L'.DTable (tn, x, n, c) => [(L'.SgiTable (tn, x, n, c), loc)]
fun sgiBindsD (env, denv) (sgi, _) =
case sgi of
@@ -2194,7 +2297,7 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
SOME (env, denv))
else
NONE
- | L'.SgiTable (x', n1, c1) =>
+ | L'.SgiTable (_, x', n1, c1) =>
if x = x' then
(case unifyCons (env, denv) (L'.CApp (tableOf env, c1), loc) c2 of
[] => SOME (env, denv)
@@ -2266,10 +2369,10 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
NONE
| _ => NONE)
- | L'.SgiTable (x, n2, c2) =>
+ | L'.SgiTable (_, x, n2, c2) =>
seek (fn sgi1All as (sgi1, _) =>
case sgi1 of
- L'.SgiTable (x', n1, c1) =>
+ L'.SgiTable (_, x', n1, c1) =>
if x = x' then
(case unifyCons (env, denv) c1 c2 of
[] => SOME (env, denv)
@@ -2541,7 +2644,7 @@ fun elabDecl ((d, loc), (env, denv, gs)) =
| L.DOpen (m, ms) =>
(case E.lookupStr env m of
NONE => (strError env (UnboundStr (loc, m));
- ([], (env, denv, [])))
+ ([], (env, denv, gs)))
| SOME (n, sgn) =>
let
val (_, sgn) = foldl (fn (m, (str, sgn)) =>
@@ -2554,7 +2657,7 @@ fun elabDecl ((d, loc), (env, denv, gs)) =
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', []))
+ (ds, (env', denv', gs))
end)
| L.DConstraint (c1, c2) =>
@@ -2568,19 +2671,19 @@ 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))
+ ([(L'.DConstraint (c1', c2'), loc)], (env, denv', gs1 @ gs2 @ gs3 @ gs4 @ gs))
end
| L.DOpenConstraints (m, ms) =>
let
val denv = dopenConstraints (loc, env, denv) {str = m, strs = ms}
in
- ([], (env, denv, []))
+ ([], (env, denv, gs))
end
| L.DExport str =>
let
- val (str', sgn, gs) = elabStr (env, denv) str
+ val (str', sgn, gs') = elabStr (env, denv) str
val sgn =
case #1 (hnormSgn env sgn) of
@@ -2626,16 +2729,16 @@ fun elabDecl ((d, loc), (env, denv, gs)) =
end
| _ => sgn
in
- ([(L'.DExport (E.newNamed (), sgn, str'), loc)], (env, denv, gs))
+ ([(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 c'
+ val (c', k, gs') = elabCon (env, denv) c
+ val (env, n) = E.pushENamed env x (L'.CApp (tableOf env, c'), loc)
in
checkKind env c' k (L'.KRecord (L'.KType, loc), loc);
- ([(L'.DTable (x, n, c'), loc)], (env, denv, gs))
+ ([(L'.DTable (tableOf' env, x, n, c'), loc)], (env, denv, gs' @ gs))
end
and elabStr (env, denv) (str, loc) =
@@ -2729,7 +2832,7 @@ 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'.SgiTable (x, n, c) =>
+ | L'.SgiTable (tn, x, n, c) =>
let
val (vals, x) =
if SS.member (vals, x) then
@@ -2737,7 +2840,7 @@ and elabStr (env, denv) (str, loc) =
else
(SS.add (vals, x), x)
in
- ((L'.SgiTable (x, n, c), loc) :: sgis, cons, vals, sgns, strs)
+ ((L'.SgiTable (tn, x, n, c), loc) :: sgis, cons, vals, sgns, strs)
end)
([], SS.empty, SS.empty, SS.empty, SS.empty) sgis
diff --git a/tests/table.lac b/tests/table.lac
index 4c44f857..30422db2 100644
--- a/tests/table.lac
+++ b/tests/table.lac
@@ -1,3 +1,12 @@
-table t : {A : int, B : string, C : float}
+table t1 : {A : int, B : string, C : float}
-val my_query = (SELECT * FROM t)
+val q1 = (SELECT * FROM t1)
+
+table t2 : {A : float, D : int}
+
+val q2 = (SELECT * FROM t1, t2)
+
+(*val q3 = (SELECT * FROM t1, t1)*)
+val q3 = (SELECT * FROM t1, t1 AS T2)
+
+val q4 = (SELECT * FROM {t1} AS T, t1 AS T2)
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-13 16:23:25 +0000