From 2ace64baba707b2e76778c74789735263eb50823 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sat, 26 Dec 2009 11:56:40 -0500 Subject: Make summary unification more conservative; infer implicit arguments after applications --- src/elaborate.sml | 58 +++++++++++++++++++++++++++++++++++++++++++++++++++---- src/urweb.grm | 17 ++++------------ 2 files changed, 58 insertions(+), 17 deletions(-) (limited to 'src') 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), -- cgit v1.2.3