Mercurial > urweb
changeset 349:beb72f8a7218
Expand cases where expression wildcards are allowed
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Sat, 04 Oct 2008 20:05:50 -0400 |
| parents | b88f4297167f |
| children | 3a1e36b14105 |
| files | src/elaborate.sml tests/crud1.ur |
| diffstat | 2 files changed, 15 insertions(+), 30 deletions(-) [+] |
line wrap: on
line diff
--- a/src/elaborate.sml Sat Oct 04 19:56:59 2008 -0400 +++ b/src/elaborate.sml Sat Oct 04 20:05:50 2008 -0400 @@ -1411,32 +1411,13 @@ ((L'.EModProj (n, ms, s), loc), t, []) end) - | L.EApp (e1, (L.EWild, _)) => + | L.EWild => let - val (e1', t1, gs1) = elabExp (env, denv) e1 - val (e1', t1, gs2) = elabHead (env, denv) e1' t1 - val (t1, gs3) = hnormCon (env, denv) t1 + val r = ref NONE + val c = cunif (loc, (L'.KType, loc)) in - case t1 of - (L'.TFun (dom, ran), _) => - let - val (dom, gs4) = normClassConstraint (env, denv) dom - in - case E.resolveClass env dom of - NONE => - let - val r = ref NONE - in - ((L'.EApp (e1', (L'.EUnif r, loc)), 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, [])) + ((L'.EUnif r, loc), c, [TypeClass (env, c, r, loc)]) end - | L.EWild => (expError env (OutOfContext (loc, NONE)); - (eerror, cerror, [])) | L.EApp (e1, e2) => let @@ -3399,9 +3380,13 @@ ("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; + let + val c = ElabOps.hnormCon env c + in + case E.resolveClass env c of + SOME e => r := SOME e + | NONE => expError env (Unresolvable (loc, c)) + end) gs; (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan) :: ds
--- a/tests/crud1.ur Sat Oct 04 19:56:59 2008 -0400 +++ b/tests/crud1.ur Sat Oct 04 20:05:50 2008 -0400 @@ -12,7 +12,7 @@ Widget = fn nm :: Name => <lform><textbox{nm}/></lform>, WidgetPopulated = fn (nm :: Name) n => <lform><textbox{nm} value={show _ n}/></lform>, Parse = readError _, - Inject = sql_int + Inject = _ }, B = { Nam = "B", @@ -20,7 +20,7 @@ Widget = fn nm :: Name => <lform><textbox{nm}/></lform>, WidgetPopulated = fn (nm :: Name) s => <lform><textbox{nm} value={s}/></lform>, Parse = readError _, - Inject = sql_string + Inject = _ }, C = { Nam = "C", @@ -28,7 +28,7 @@ Widget = fn nm :: Name => <lform><textbox{nm}/></lform>, WidgetPopulated = fn (nm :: Name) n => <lform><textbox{nm} value={show _ n}/></lform>, Parse = readError _, - Inject = sql_float + Inject = _ }, D = { Nam = "D", @@ -36,7 +36,7 @@ Widget = fn nm :: Name => <lform><checkbox{nm}/></lform>, WidgetPopulated = fn (nm :: Name) b => <lform><checkbox{nm} checked={b}/></lform>, Parse = fn x => x, - Inject = sql_bool + Inject = _ } } end)