summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-12-26 11:56:40 -0500
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-12-26 11:56:40 -0500
commitc4120c8ddaa5340efad5f835ce4565f2a8ae2cbf (patch)
treeb4c6e798738335ded8d209afc369885664396d08 /src
parent4300120544123e9dfb262eb8b4e3d0a0f17ff9bc (diff)
Make summary unification more conservative; infer implicit arguments after applications
Diffstat (limited to 'src')
-rw-r--r--src/elaborate.sml58
-rw-r--r--src/urweb.grm17
2 files changed, 58 insertions, 17 deletions
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 2a237c50..f1ddd83e 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -693,6 +693,13 @@
and consNeq env (c1, c2) =
case (#1 (hnormCon env c1), #1 (hnormCon env c2)) of
(L'.CName x1, L'.CName x2) => x1 <> x2
+ | (L'.CName _, L'.CRel _) => true
+ | (L'.CRel _, L'.CName _) => true
+ | (L'.CRel n1, L'.CRel n2) => n1 <> n2
+ | (L'.CRel _, L'.CNamed _) => true
+ | (L'.CNamed _, L'.CRel _) => true
+ | (L'.CRel _, L'.CModProj _) => true
+ | (L'.CModProj _, L'.CRel _) => true
| _ => false
and unifySummaries env (loc, k, s1 : record_summary, s2 : record_summary) =
@@ -1619,6 +1626,34 @@ fun normClassConstraint env (c, loc) =
| L'.CUnif (_, _, _, ref (SOME c)) => normClassConstraint env c
| _ => unmodCon env (c, loc)
+fun findHead e e' =
+ let
+ fun findHead (e, _) =
+ case e of
+ L.EVar (_, _, infer) =>
+ let
+ fun findHead' (e, _) =
+ case e of
+ L'.ENamed _ => true
+ | L'.EModProj _ => true
+ | L'.EApp (e, _) => findHead' e
+ | L'.ECApp (e, _) => findHead' e
+ | L'.EKApp (e, _) => findHead' e
+ | _ => false
+ in
+ if findHead' e' then
+ SOME infer
+ else
+ NONE
+ end
+ | L.EApp (e, _) => findHead e
+ | L.ECApp (e, _) => findHead e
+ | L.EDisjointApp e => findHead e
+ | _ => NONE
+ in
+ findHead e
+ end
+
fun elabExp (env, denv) (eAll as (e, loc)) =
let
(*val () = eprefaces "elabExp" [("eAll", SourcePrint.p_exp eAll)]*)
@@ -1674,15 +1709,23 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
| L.EApp (e1, e2) =>
let
val (e1', t1, gs1) = elabExp (env, denv) e1
+
val (e2', t2, gs2) = elabExp (env, denv) e2
val dom = cunif (loc, ktype)
val ran = cunif (loc, ktype)
val t = (L'.TFun (dom, ran), loc)
+
+ val () = checkCon env e1' t1 t
+ val () = checkCon env e2' t2 dom
+
+ val ef = (L'.EApp (e1', e2'), loc)
+ val (ef, et, gs3) =
+ case findHead e1 e1' of
+ NONE => (ef, ran, [])
+ | SOME infer => elabHead (env, denv) infer ef ran
in
- checkCon env e1' t1 t;
- checkCon env e2' t2 dom;
- ((L'.EApp (e1', e2'), loc), ran, gs1 @ gs2)
+ (ef, et, gs1 @ gs2 @ gs3)
end
| L.EAbs (x, to, e) =>
let
@@ -1705,6 +1748,7 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
| L.ECApp (e, c) =>
let
val (e', et, gs1) = elabExp (env, denv) e
+
val oldEt = et
val (c', ck, gs2) = elabCon (env, denv) c
val (et', _) = hnormCon env et
@@ -1717,6 +1761,12 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
val eb' = subConInCon (0, c') eb
handle SynUnif => (expError env (Unif ("substitution", loc, eb));
cerror)
+
+ val ef = (L'.ECApp (e', c'), loc)
+ val (ef, eb', gs3) =
+ case findHead e e' of
+ NONE => (ef, eb', [])
+ | SOME infer => elabHead (env, denv) infer ef eb'
in
(*prefaces "Elab ECApp" [("e", SourcePrint.p_exp eAll),
("et", p_con env oldEt),
@@ -1724,7 +1774,7 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
("eb", p_con (E.pushCRel env x k) eb),
("c", p_con env c'),
("eb'", p_con env eb')];*)
- ((L'.ECApp (e', c'), loc), eb', gs1 @ enD gs2)
+ (ef, eb', gs1 @ enD gs2 @ gs3)
end
| _ =>
diff --git a/src/urweb.grm b/src/urweb.grm
index 00c39b52..93ff7321 100644
--- a/src/urweb.grm
+++ b/src/urweb.grm
@@ -540,9 +540,8 @@ cst : UNIQUE tnames (let
val e = (EVar (["Basis"], "unique", Infer), loc)
val e = (ECApp (e, #1 (#1 tnames)), loc)
val e = (ECApp (e, (CRecord (#2 tnames), loc)), loc)
- val e = (EDisjointApp e, loc)
in
- (EDisjointApp e, loc)
+ e
end)
| CHECK sqlexp (let
@@ -562,9 +561,6 @@ cst : UNIQUE tnames (let
val e = (EVar (["Basis"], "mat_cons", Infer), loc)
val e = (ECApp (e, nm1), loc)
val e = (ECApp (e, nm2), loc)
- val e = (EDisjointApp e, loc)
- val e = (EDisjointApp e, loc)
- val e = (EApp (e, (EWild, loc)), loc)
in
(EApp (e, mat), loc)
end)
@@ -634,7 +630,7 @@ pkopt : (EVar (["Basis"], "no_primary_key", Infe
| PRIMARY KEY tnames (let
val loc = s (PRIMARYleft, tnamesright)
- val e = (EVar (["Basis"], "primary_key", Infer), loc)
+ val e = (EVar (["Basis"], "primary_key", TypesOnly), loc)
val e = (ECApp (e, #1 (#1 tnames)), loc)
val e = (ECApp (e, (CRecord (#2 tnames), loc)), loc)
val e = (EDisjointApp e, loc)
@@ -1192,7 +1188,6 @@ eterm : LPAREN eexp RPAREN (#1 eexp, s (LPARENleft, RPARENright))
val e = (EVar (["Basis"], "update", Infer), loc)
val e = (ECApp (e, (CWild (KRecord (KType, loc), loc), loc)), loc)
- val e = (EDisjointApp e, loc)
val e = (EApp (e, (ERecord fsets, loc)), loc)
val e = (EApp (e, texp), loc)
in
@@ -1335,11 +1330,8 @@ xmlOne : NOTAGS (EApp ((EVar (["Basis"], "cdata", Infer)
if et = "form" then
(EApp ((EVar (["Basis"], "form", Infer), pos),
xmlOpt), pos)
- else if et = "subform" then
- (EApp ((EDisjointApp (#2 (#1 tag)), pos),
- xmlOpt), pos)
- else if et = "subforms" then
- (EApp ((EDisjointApp (#2 (#1 tag)), pos),
+ else if et = "subform" orelse et = "subforms" then
+ (EApp (#2 (#1 tag),
xmlOpt), pos)
else if et = "entry" then
(EApp ((EVar (["Basis"], "entry", Infer), pos),
@@ -1504,7 +1496,6 @@ query1 : SELECT dopt select FROM tables wopt gopt hopt
val e = (EVar (["Basis"], "sql_query1", Infer), loc)
val e = (ECApp (e, (CRecord (map (fn nm => (nm, (CUnit, loc))) empties),
loc)), loc)
- val e = (EDisjointApp e, loc)
val re = (ERecord [((CName "Distinct", loc),
dopt),
((CName "From", loc),