Mercurial > urweb

comparison src/elaborate.sml @ 90:94ef20a31550

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fancier head normalization pushed inside of Disjoint
author Adam Chlipala <adamc@hcoop.net>
date Thu, 03 Jul 2008 11:04:25 -0400
parents 7bab29834cd6
children 4327abd52997
comparison
equal deleted inserted replaced
89:d3ee072fa609 90:94ef20a31550
249 val (c2', k2, gs2) = elabCon (env, denv) c2 249 val (c2', k2, gs2) = elabCon (env, denv) c2
250 250
251 val ku1 = kunif loc 251 val ku1 = kunif loc
252 val ku2 = kunif loc 252 val ku2 = kunif loc
253 253
254 val denv' = D.assert env denv (c1', c2') 254 val (denv', gs3) = D.assert env denv (c1', c2')
255 val (c', k, gs3) = elabCon (env, denv') c 255 val (c', k, gs4) = elabCon (env, denv') c
256 in 256 in
257 checkKind env c1' k1 (L'.KRecord ku1, loc); 257 checkKind env c1' k1 (L'.KRecord ku1, loc);
258 checkKind env c2' k2 (L'.KRecord ku2, loc); 258 checkKind env c2' k2 (L'.KRecord ku2, loc);
259 259
260 ((L'.TDisjoint (c1', c2', c'), loc), k, gs1 @ gs2 @ gs3) 260 ((L'.TDisjoint (c1', c2', c'), loc), k, gs1 @ gs2 @ gs3 @ gs4)
261 end 261 end
262 | L.TRecord c => 262 | L.TRecord c =>
263 let 263 let
264 val (c', ck, gs) = elabCon (env, denv) c 264 val (c', ck, gs) = elabCon (env, denv) c
265 val k = (L'.KRecord ktype, loc) 265 val k = (L'.KRecord ktype, loc)
328 val (c2', k2, gs2) = elabCon (env, denv) c2 328 val (c2', k2, gs2) = elabCon (env, denv) c2
329 329
330 val ku1 = kunif loc 330 val ku1 = kunif loc
331 val ku2 = kunif loc 331 val ku2 = kunif loc
332 332
333 val denv' = D.assert env denv (c1', c2') 333 val (denv', gs3) = D.assert env denv (c1', c2')
334 val (c', k, gs3) = elabCon (env, denv') c 334 val (c', k, gs4) = elabCon (env, denv') c
335 in 335 in
336 checkKind env c1' k1 (L'.KRecord ku1, loc); 336 checkKind env c1' k1 (L'.KRecord ku1, loc);
337 checkKind env c2' k2 (L'.KRecord ku2, loc); 337 checkKind env c2' k2 (L'.KRecord ku2, loc);
338 338
339 ((L'.CDisjoint (c1', c2', c'), loc), k, gs1 @ gs2 @ gs3) 339 ((L'.CDisjoint (c1', c2', c'), loc), k, gs1 @ gs2 @ gs3 @ gs4)
340 end 340 end
341 341
342 | L.CName s => 342 | L.CName s =>
343 ((L'.CName s, loc), kname, []) 343 ((L'.CName s, loc), kname, [])
344 344
367 val r1 = (L'.CRecord (k, [xc]), loc) 367 val r1 = (L'.CRecord (k, [xc]), loc)
368 val ds = foldl (fn (xc', ds) => 368 val ds = foldl (fn (xc', ds) =>
369 let 369 let
370 val r2 = (L'.CRecord (k, [xc']), loc) 370 val r2 = (L'.CRecord (k, [xc']), loc)
371 in 371 in
372 map (fn cs => (loc, env, denv, cs)) (D.prove env denv (r1, r2, loc)) 372 D.prove env denv (r1, r2, loc) @ ds
373 @ ds
374 end) 373 end)
375 ds rest 374 ds rest
376 in 375 in
377 prove (rest, ds) 376 prove (rest, ds)
378 end 377 end
387 val k = (L'.KRecord ku, loc) 386 val k = (L'.KRecord ku, loc)
388 in 387 in
389 checkKind env c1' k1 k; 388 checkKind env c1' k1 k;
390 checkKind env c2' k2 k; 389 checkKind env c2' k2 k;
391 ((L'.CConcat (c1', c2'), loc), k, 390 ((L'.CConcat (c1', c2'), loc), k,
392 map (fn cs => (loc, env, denv, cs)) (D.prove env denv (c1', c2', loc)) @ gs1 @ gs2) 391 D.prove env denv (c1', c2', loc) @ gs1 @ gs2)
393 end 392 end
394 | L.CFold => 393 | L.CFold =>
395 let 394 let
396 val dom = kunif loc 395 val dom = kunif loc
397 val ran = kunif loc 396 val ran = kunif loc
543 | L'.CUnit => (L'.KUnit, loc) 542 | L'.CUnit => (L'.KUnit, loc)
544 543
545 | L'.CError => kerror 544 | L'.CError => kerror
546 | L'.CUnif (_, k, _, _) => k 545 | L'.CUnif (_, k, _, _) => k
547 546
548 fun hnormCon (env, denv) c = 547 val hnormCon = D.hnormCon
549 let
550 val cAll as (c, loc) = ElabOps.hnormCon env c
551
552 fun doDisj (c1, c2, c) =
553 let
554 val (c, gs) = hnormCon (env, denv) c
555 in
556 (c,
557 map (fn cs => (loc, env, denv, cs)) (D.prove env denv (c1, c2, loc)) @ gs)
558 end
559 in
560 case c of
561 L'.CDisjoint cs => doDisj cs
562 | L'.TDisjoint cs => doDisj cs
563 | _ => (cAll, [])
564 end
565 548
566 fun unifyRecordCons (env, denv) (c1, c2) = 549 fun unifyRecordCons (env, denv) (c1, c2) =
567 let 550 let
568 val k1 = kindof env c1 551 val k1 = kindof env c1
569 val k2 = kindof env c2 552 val k2 = kindof env c2
701 684
702 and unifyCons' (env, denv) c1 c2 = 685 and unifyCons' (env, denv) c1 c2 =
703 let 686 let
704 val (c1, gs1) = hnormCon (env, denv) c1 687 val (c1, gs1) = hnormCon (env, denv) c1
705 val (c2, gs2) = hnormCon (env, denv) c2 688 val (c2, gs2) = hnormCon (env, denv) c2
689 val gs3 = unifyCons'' (env, denv) c1 c2
706 in 690 in
707 unifyCons'' (env, denv) c1 c2; 691 gs1 @ gs2 @ gs3
708 gs1 @ gs2
709 end 692 end
710 693
711 and unifyCons'' (env, denv) (c1All as (c1, _)) (c2All as (c2, _)) = 694 and unifyCons'' (env, denv) (c1All as (c1, _)) (c2All as (c2, _)) =
712 let 695 let
713 fun err f = raise CUnify' (f (c1All, c2All)) 696 fun err f = raise CUnify' (f (c1All, c2All))
1038 val (c2', k2, gs2) = elabCon (env, denv) c2 1021 val (c2', k2, gs2) = elabCon (env, denv) c2
1039 1022
1040 val ku1 = kunif loc 1023 val ku1 = kunif loc
1041 val ku2 = kunif loc 1024 val ku2 = kunif loc
1042 1025
1043 val denv' = D.assert env denv (c1', c2') 1026 val (denv', gs3) = D.assert env denv (c1', c2')
1044 val (e', t, gs3) = elabExp (env, denv') e 1027 val (e', t, gs4) = elabExp (env, denv') e
1045 in 1028 in
1046 checkKind env c1' k1 (L'.KRecord ku1, loc); 1029 checkKind env c1' k1 (L'.KRecord ku1, loc);
1047 checkKind env c2' k2 (L'.KRecord ku2, loc); 1030 checkKind env c2' k2 (L'.KRecord ku2, loc);
1048 1031
1049 (e', (L'.TDisjoint (c1', c2', t), loc), gs1 @ gs2 @ gs3) 1032 (e', (L'.TDisjoint (c1', c2', t), loc), gs1 @ gs2 @ gs3 @ gs4)
1050 end 1033 end
1051 1034
1052 | L.ERecord xes => 1035 | L.ERecord xes =>
1053 let 1036 let
1054 val (xes', gs) = ListUtil.foldlMap (fn ((x, e), gs) => 1037 val (xes', gs) = ListUtil.foldlMap (fn ((x, e), gs) =>
1073 val gs = foldl (fn ((x', _, t'), gs) => 1056 val gs = foldl (fn ((x', _, t'), gs) =>
1074 let 1057 let
1075 val xc' = (x', t') 1058 val xc' = (x', t')
1076 val r2 = (L'.CRecord (k, [xc']), loc) 1059 val r2 = (L'.CRecord (k, [xc']), loc)
1077 in 1060 in
1078 map (fn cs => (loc, env, denv, cs)) (D.prove env denv (r1, r2, loc)) 1061 D.prove env denv (r1, r2, loc) @ gs
1079 @ gs
1080 end) 1062 end)
1081 gs rest 1063 gs rest
1082 in 1064 in
1083 prove (rest, gs) 1065 prove (rest, gs)
1084 end 1066 end
1098 val first = (L'.CRecord (ktype, [(c', ft)]), loc) 1080 val first = (L'.CRecord (ktype, [(c', ft)]), loc)
1099 1081
1100 val gs3 = 1082 val gs3 =
1101 checkCon (env, denv) e' et 1083 checkCon (env, denv) e' et
1102 (L'.TRecord (L'.CConcat (first, rest), loc), loc) 1084 (L'.TRecord (L'.CConcat (first, rest), loc), loc)
1103 val gs4 = 1085 val gs4 = D.prove env denv (first, rest, loc)
1104 map (fn cs => (loc, env, denv, cs))
1105 (D.prove env denv (first, rest, loc))
1106 in 1086 in
1107 ((L'.EField (e', c', {field = ft, rest = rest}), loc), ft, gs1 @ gs2 @ gs3 @ gs4) 1087 ((L'.EField (e', c', {field = ft, rest = rest}), loc), ft, gs1 @ gs2 @ gs3 @ gs4)
1108 end 1088 end
1109 1089
1110 | L.EFold => 1090 | L.EFold =>
1285 | L.SgiConstraint (c1, c2) => 1265 | L.SgiConstraint (c1, c2) =>
1286 let 1266 let
1287 val (c1', k1, gs1) = elabCon (env, denv) c1 1267 val (c1', k1, gs1) = elabCon (env, denv) c1
1288 val (c2', k2, gs2) = elabCon (env, denv) c2 1268 val (c2', k2, gs2) = elabCon (env, denv) c2
1289 1269
1290 val denv = D.assert env denv (c1', c2') 1270 val (denv, gs3) = D.assert env denv (c1', c2')
1291 in 1271 in
1292 checkKind env c1' k1 (L'.KRecord (kunif loc), loc); 1272 checkKind env c1' k1 (L'.KRecord (kunif loc), loc);
1293 checkKind env c2' k2 (L'.KRecord (kunif loc), loc); 1273 checkKind env c2' k2 (L'.KRecord (kunif loc), loc);
1294 1274
1295 ([(L'.SgiConstraint (c1', c2'), loc)], (env, denv, gs1 @ gs2)) 1275 ([(L'.SgiConstraint (c1', c2'), loc)], (env, denv, gs1 @ gs2 @ gs3))
1296 end 1276 end
1297 1277
1298 and elabSgn (env, denv) (sgn, loc) = 1278 and elabSgn (env, denv) (sgn, loc) =
1299 case sgn of 1279 case sgn of
1300 L.SgnConst sgis => 1280 L.SgnConst sgis =>
1482 val cso = E.projectConstraints env {sgn = sgn, str = st} 1462 val cso = E.projectConstraints env {sgn = sgn, str = st}
1483 1463
1484 val denv = case cso of 1464 val denv = case cso of
1485 NONE => (strError env (UnboundStr (loc, str)); 1465 NONE => (strError env (UnboundStr (loc, str));
1486 denv) 1466 denv)
1487 | SOME cs => foldl (fn ((c1, c2), denv) => D.assert env denv (c1, c2)) denv cs 1467 | SOME cs => foldl (fn ((c1, c2), denv) =>
1468 let
1469 val (denv, gs) = D.assert env denv (c1, c2)
1470 in
1471 case gs of
1472 [] => ()
1473 | _ => raise Fail "dopenConstraints: Sub-constraints remain";
1474
1475 denv
1476 end) denv cs
1488 in 1477 in
1489 denv 1478 denv
1490 end 1479 end
1491 1480
1492 fun sgiOfDecl (d, loc) = 1481 fun sgiOfDecl (d, loc) =
1498 | L'.DFfiStr (x, n, sgn) => (L'.SgiStr (x, n, sgn), loc) 1487 | L'.DFfiStr (x, n, sgn) => (L'.SgiStr (x, n, sgn), loc)
1499 | L'.DConstraint cs => (L'.SgiConstraint cs, loc) 1488 | L'.DConstraint cs => (L'.SgiConstraint cs, loc)
1500 1489
1501 fun sgiBindsD (env, denv) (sgi, _) = 1490 fun sgiBindsD (env, denv) (sgi, _) =
1502 case sgi of 1491 case sgi of
1503 L'.SgiConstraint (c1, c2) => D.assert env denv (c1, c2) 1492 L'.SgiConstraint (c1, c2) =>
1493 (case D.assert env denv (c1, c2) of
1494 (denv, []) => denv
1495 | _ => raise Fail "sgiBindsD: Sub-constraints remain")
1504 | _ => denv 1496 | _ => denv
1505 1497
1506 fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) = 1498 fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
1507 case (#1 (hnormSgn env sgn1), #1 (hnormSgn env sgn2)) of 1499 case (#1 (hnormSgn env sgn1), #1 (hnormSgn env sgn2)) of
1508 (L'.SgnError, _) => () 1500 (L'.SgnError, _) => ()
1632 | L'.SgiConstraint (c2, d2) => 1624 | L'.SgiConstraint (c2, d2) =>
1633 seek (fn sgi1All as (sgi1, _) => 1625 seek (fn sgi1All as (sgi1, _) =>
1634 case sgi1 of 1626 case sgi1 of
1635 L'.SgiConstraint (c1, d1) => 1627 L'.SgiConstraint (c1, d1) =>
1636 if consEq (env, denv) (c1, c2) andalso consEq (env, denv) (d1, d2) then 1628 if consEq (env, denv) (c1, c2) andalso consEq (env, denv) (d1, d2) then
1637 SOME (env, D.assert env denv (c2, d2)) 1629 let
1630 val (denv, gs) = D.assert env denv (c2, d2)
1631 in
1632 case gs of
1633 [] => ()
1634 | _ => raise Fail "subSgn: Sub-constraints remain";
1635
1636 SOME (env, denv)
1637 end
1638 else 1638 else
1639 NONE 1639 NONE
1640 | _ => NONE) 1640 | _ => NONE)
1641 end 1641 end
1642 in 1642 in
1791 1791
1792 | L.DConstraint (c1, c2) => 1792 | L.DConstraint (c1, c2) =>
1793 let 1793 let
1794 val (c1', k1, gs1) = elabCon (env, denv) c1 1794 val (c1', k1, gs1) = elabCon (env, denv) c1
1795 val (c2', k2, gs2) = elabCon (env, denv) c2 1795 val (c2', k2, gs2) = elabCon (env, denv) c2
1796 val gs3 = map (fn cs => (loc, env, denv, cs)) (D.prove env denv (c1', c2', loc)) 1796 val gs3 = D.prove env denv (c1', c2', loc)
1797 1797
1798 val denv' = D.assert env denv (c1', c2') 1798 val (denv', gs4) = D.assert env denv (c1', c2')
1799 in 1799 in
1800 checkKind env c1' k1 (L'.KRecord (kunif loc), loc); 1800 checkKind env c1' k1 (L'.KRecord (kunif loc), loc);
1801 checkKind env c2' k2 (L'.KRecord (kunif loc), loc); 1801 checkKind env c2' k2 (L'.KRecord (kunif loc), loc);
1802 1802
1803 ([(L'.DConstraint (c1', c2'), loc)], (env, denv', gs1 @ gs2 @ gs3)) 1803 ([(L'.DConstraint (c1', c2'), loc)], (env, denv', gs1 @ gs2 @ gs3 @ gs4))
1804 end 1804 end
1805 1805
1806 | L.DOpenConstraints (m, ms) => 1806 | L.DOpenConstraints (m, ms) =>
1807 let 1807 let
1808 val denv = dopenConstraints (loc, env, denv) {str = m, strs = ms} 1808 val denv = dopenConstraints (loc, env, denv) {str = m, strs = ms}
1980 val (file, (_, gs)) = ListUtil.foldlMapConcat elabDecl' (env', []) file 1980 val (file, (_, gs)) = ListUtil.foldlMapConcat elabDecl' (env', []) file
1981 in 1981 in
1982 if ErrorMsg.anyErrors () then 1982 if ErrorMsg.anyErrors () then
1983 () 1983 ()
1984 else 1984 else
1985 app (fn (loc, env, denv, (c1, c2)) => 1985 app (fn (loc, env, denv, c1, c2) =>
1986 case D.prove env denv (c1, c2, loc) of 1986 case D.prove env denv (c1, c2, loc) of
1987 [] => () 1987 [] => ()
1988 | _ => 1988 | _ =>
1989 (ErrorMsg.errorAt loc "Couldn't prove field name disjointness"; 1989 (ErrorMsg.errorAt loc "Couldn't prove field name disjointness";
1990 eprefaces' [("Con 1", p_con env c1), 1990 eprefaces' [("Con 1", p_con env c1),
1991 ("Con 2", p_con env c2)])) gs; 1991 ("Con 2", p_con env c2),
1992 ("Hnormed 1", p_con env (ElabOps.hnormCon env c1)),
1993 ("Hnormed 2", p_con env (ElabOps.hnormCon env c2))])) gs;
1992 1994
1993 (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan) :: ds @ file 1995 (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan) :: ds @ file
1994 end 1996 end
1995 1997
1996 end 1998 end