diff src/elaborate.sml @ 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 24a31b35e08f
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