Mercurial > urweb

comparison src/elaborate.sml @ 349:beb72f8a7218

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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
comparison
equal deleted inserted replaced
348:b88f4297167f 349:beb72f8a7218
1409 | SOME t => t 1409 | SOME t => t
1410 in 1410 in
1411 ((L'.EModProj (n, ms, s), loc), t, []) 1411 ((L'.EModProj (n, ms, s), loc), t, [])
1412 end) 1412 end)
1413 1413
1414 | L.EApp (e1, (L.EWild, _)) => 1414 | L.EWild =>
1415 let 1415 let
1416 val (e1', t1, gs1) = elabExp (env, denv) e1 1416 val r = ref NONE
1417 val (e1', t1, gs2) = elabHead (env, denv) e1' t1 1417 val c = cunif (loc, (L'.KType, loc))
1418 val (t1, gs3) = hnormCon (env, denv) t1
1419 in 1418 in
1420 case t1 of 1419 ((L'.EUnif r, loc), c, [TypeClass (env, c, r, loc)])
1421 (L'.TFun (dom, ran), _) =>
1422 let
1423 val (dom, gs4) = normClassConstraint (env, denv) dom
1424 in
1425 case E.resolveClass env dom of
1426 NONE =>
1427 let
1428 val r = ref NONE
1429 in
1430 ((L'.EApp (e1', (L'.EUnif r, loc)), loc),
1431 ran, [TypeClass (env, dom, r, loc)])
1432 end
1433 | SOME pf => ((L'.EApp (e1', pf), loc), ran, gs1 @ gs2 @ enD gs3 @ enD gs4)
1434 end
1435 | _ => (expError env (OutOfContext (loc, SOME (e1', t1)));
1436 (eerror, cerror, []))
1437 end 1420 end
1438 | L.EWild => (expError env (OutOfContext (loc, NONE));
1439 (eerror, cerror, []))
1440 1421
1441 | L.EApp (e1, e2) => 1422 | L.EApp (e1, e2) =>
1442 let 1423 let
1443 val (e1', t1, gs1) = elabExp (env, denv) e1 1424 val (e1', t1, gs1) = elabExp (env, denv) e1
1444 val (e1', t1, gs2) = elabHead (env, denv) e1' t1 1425 val (e1', t1, gs2) = elabHead (env, denv) e1' t1
3397 eprefaces' [("Con 1", p_con env c1), 3378 eprefaces' [("Con 1", p_con env c1),
3398 ("Con 2", p_con env c2), 3379 ("Con 2", p_con env c2),
3399 ("Hnormed 1", p_con env (ElabOps.hnormCon env c1)), 3380 ("Hnormed 1", p_con env (ElabOps.hnormCon env c1)),
3400 ("Hnormed 2", p_con env (ElabOps.hnormCon env c2))])) 3381 ("Hnormed 2", p_con env (ElabOps.hnormCon env c2))]))
3401 | TypeClass (env, c, r, loc) => 3382 | TypeClass (env, c, r, loc) =>
3402 case E.resolveClass env c of 3383 let
3403 SOME e => r := SOME e 3384 val c = ElabOps.hnormCon env c
3404 | NONE => expError env (Unresolvable (loc, c))) gs; 3385 in
3386 case E.resolveClass env c of
3387 SOME e => r := SOME e
3388 | NONE => expError env (Unresolvable (loc, c))
3389 end) gs;
3405 3390
3406 (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan) 3391 (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan)
3407 :: ds 3392 :: ds
3408 @ (L'.DStr ("Top", top_n, topSgn, topStr), ErrorMsg.dummySpan) 3393 @ (L'.DStr ("Top", top_n, topSgn, topStr), ErrorMsg.dummySpan)
3409 :: ds' @ file 3394 :: ds' @ file