summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-10-04 20:05:50 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-10-04 20:05:50 -0400
commit9bd2b016ef2eedf73d2d00d22c009b0d3a8558d3 (patch)
tree8794d17ecb26e681bc92bc7b712ea9f498ce609c
parent8f22c3384c8b715c97fa781fa388ef9090d13fb6 (diff)
Expand cases where expression wildcards are allowed
-rw-r--r--src/elaborate.sml37
-rw-r--r--tests/crud1.ur8
2 files changed, 15 insertions, 30 deletions
diff --git a/src/elaborate.sml b/src/elaborate.sml
index fce46209..b2d1f958 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -1411,32 +1411,13 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
((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 @@ fun elabFile basis topStr topSgn env file =
("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
diff --git a/tests/crud1.ur b/tests/crud1.ur
index 10722b55..cca71aab 100644
--- a/tests/crud1.ur
+++ b/tests/crud1.ur
@@ -12,7 +12,7 @@ open Crud.Make(struct
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 @@ open Crud.Make(struct
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 @@ open Crud.Make(struct
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 @@ open Crud.Make(struct
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)