Mercurial > urweb

comparison src/elaborate.sml @ 339:075b36dbb1a4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Crud supports INSERT
author Adam Chlipala <adamc@hcoop.net>
date Sun, 14 Sep 2008 15:10:04 -0400
parents e976b187d73a
children 389399d65331
comparison
equal deleted inserted replaced
338:e976b187d73a 339:075b36dbb1a4
1017 case t of 1017 case t of
1018 (L'.TCFun (L'.Implicit, x, k, t'), _) => 1018 (L'.TCFun (L'.Implicit, x, k, t'), _) =>
1019 let 1019 let
1020 val u = cunif (loc, k) 1020 val u = cunif (loc, k)
1021 1021
1022 val (e, t, gs') = unravel (subConInCon (0, u) t', 1022 val t'' = subConInCon (0, u) t'
1023 (L'.ECApp (e, u), loc)) 1023 val (e, t, gs') = unravel (t'', (L'.ECApp (e, u), loc))
1024 in 1024 in
1025 (*prefaces "Unravel" [("t'", p_con env t'),
1026 ("t''", p_con env t'')];*)
1025 (e, t, enD gs @ gs') 1027 (e, t, enD gs @ gs')
1026 end 1028 end
1027 | _ => (e, t, enD gs) 1029 | _ => (e, t, enD gs)
1028 end 1030 end
1029 in 1031 in
1475 L'.CError => (eerror, cerror, []) 1477 L'.CError => (eerror, cerror, [])
1476 | L'.TCFun (_, x, k, eb) => 1478 | L'.TCFun (_, x, k, eb) =>
1477 let 1479 let
1478 val () = checkKind env c' ck k 1480 val () = checkKind env c' ck k
1479 val eb' = subConInCon (0, c') eb 1481 val eb' = subConInCon (0, c') eb
1480 handle SynUnif => (expError env (Unif ("substitution", eb)); 1482 handle SynUnif => (expError env (Unif ("substitution", loc, eb));
1481 cerror) 1483 cerror)
1482 in 1484 in
1483 (*prefaces "Elab ECApp" [("e", SourcePrint.p_exp eAll), 1485 (*prefaces "Elab ECApp" [("e", SourcePrint.p_exp eAll),
1484 ("et", p_con env oldEt), 1486 ("et", p_con env oldEt),
1485 ("x", PD.string x), 1487 ("x", PD.string x),
1486 ("eb", p_con (E.pushCRel env x k) eb), 1488 ("eb", p_con (E.pushCRel env x k) eb),
1487 ("c", p_con env c'), 1489 ("c", p_con env c'),
1488 ("eb'", p_con env eb')];*) 1490 ("eb'", p_con env eb')];*)
1489 ((L'.ECApp (e', c'), loc), eb', gs1 @ gs2 @ enD gs3 @ enD gs4) 1491 ((L'.ECApp (e', c'), loc), eb', gs1 @ gs2 @ enD gs3 @ enD gs4)
1490 end 1492 end
1491
1492 | L'.CUnif _ =>
1493 (expError env (Unif ("application", et));
1494 (eerror, cerror, []))
1495 1493
1496 | _ => 1494 | _ =>
1497 (expError env (WrongForm ("constructor function", e', et)); 1495 (expError env (WrongForm ("constructor function", e', et));
1498 (eerror, cerror, [])) 1496 (eerror, cerror, []))
1499 end 1497 end
1584 val gs4 = D.prove env denv (first, rest, loc) 1582 val gs4 = D.prove env denv (first, rest, loc)
1585 in 1583 in
1586 ((L'.EField (e', c', {field = ft, rest = rest}), loc), ft, gs1 @ enD gs2 @ enD gs3 @ enD gs4) 1584 ((L'.EField (e', c', {field = ft, rest = rest}), loc), ft, gs1 @ enD gs2 @ enD gs3 @ enD gs4)
1587 end 1585 end
1588 1586
1587 | L.EWith (e1, c, e2) =>
1588 let
1589 val (e1', e1t, gs1) = elabExp (env, denv) e1
1590 val (c', ck, gs2) = elabCon (env, denv) c
1591 val (e2', e2t, gs3) = elabExp (env, denv) e2
1592
1593 val rest = cunif (loc, ktype_record)
1594 val first = (L'.CRecord (ktype, [(c', e2t)]), loc)
1595
1596 val gs4 = checkCon (env, denv) e1' e1t (L'.TRecord rest, loc)
1597 val gs5 = D.prove env denv (first, rest, loc)
1598 in
1599 ((L'.EWith (e1', c', e2', {field = e2t, rest = rest}), loc),
1600 (L'.TRecord ((L'.CConcat (first, rest), loc)), loc),
1601 gs1 @ enD gs2 @ gs3 @ enD gs4 @ enD gs5)
1602 end
1589 | L.ECut (e, c) => 1603 | L.ECut (e, c) =>
1590 let 1604 let
1591 val (e', et, gs1) = elabExp (env, denv) e 1605 val (e', et, gs1) = elabExp (env, denv) e
1592 val (c', ck, gs2) = elabCon (env, denv) c 1606 val (c', ck, gs2) = elabCon (env, denv) c
1593 1607