Mercurial > urweb

comparison src/elaborate.sml @ 84:e86370850c30

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Disjointness assumptions
author Adam Chlipala <adamc@hcoop.net>
date Tue, 01 Jul 2008 12:10:46 -0400
parents 0a1baddd8ab2
children 1f85890c9846
comparison
equal deleted inserted replaced
83:0a1baddd8ab2 84:e86370850c30
304 ((L'.CAbs (x, k', t'), loc), 304 ((L'.CAbs (x, k', t'), loc),
305 (L'.KArrow (k', tk), loc), 305 (L'.KArrow (k', tk), loc),
306 gs) 306 gs)
307 end 307 end
308 308
309 | L.CDisjoint (c1, c2, c) =>
310 let
311 val (c1', k1, gs1) = elabCon (env, denv) c1
312 val (c2', k2, gs2) = elabCon (env, denv) c2
313
314 val ku1 = kunif loc
315 val ku2 = kunif loc
316
317 val denv' = D.assert env denv (c1', c2')
318 val (c', k, gs3) = elabCon (env, denv') c
319 in
320 checkKind env c1' k1 (L'.KRecord ku1, loc);
321 checkKind env c2' k2 (L'.KRecord ku2, loc);
322
323 ((L'.CDisjoint (c1', c2', c'), loc), k, gs1 @ gs2 @ gs3)
324 end
325
309 | L.CName s => 326 | L.CName s =>
310 ((L'.CName s, loc), kname, []) 327 ((L'.CName s, loc), kname, [])
311 328
312 | L.CRecord xcs => 329 | L.CRecord xcs =>
313 let 330 let
496 (case #1 (hnormKind (kindof env c)) of 513 (case #1 (hnormKind (kindof env c)) of
497 L'.KArrow (_, k) => k 514 L'.KArrow (_, k) => k
498 | L'.KError => kerror 515 | L'.KError => kerror
499 | _ => raise CUnify' (CKindof c)) 516 | _ => raise CUnify' (CKindof c))
500 | L'.CAbs (x, k, c) => (L'.KArrow (k, kindof (E.pushCRel env x k) c), loc) 517 | L'.CAbs (x, k, c) => (L'.KArrow (k, kindof (E.pushCRel env x k) c), loc)
518 | L'.CDisjoint (_, _, c) => kindof env c
501 519
502 | L'.CName _ => kname 520 | L'.CName _ => kname
503 521
504 | L'.CRecord (k, _) => (L'.KRecord k, loc) 522 | L'.CRecord (k, _) => (L'.KRecord k, loc)
505 | L'.CConcat (c, _) => kindof env c 523 | L'.CConcat (c, _) => kindof env c
1759 (ds, (env, gs)) 1777 (ds, (env, gs))
1760 end 1778 end
1761 1779
1762 val (file, (_, gs)) = ListUtil.foldlMapConcat elabDecl' (env', []) file 1780 val (file, (_, gs)) = ListUtil.foldlMapConcat elabDecl' (env', []) file
1763 in 1781 in
1764 app (fn (loc, env, denv, (c1, c2)) => 1782 if ErrorMsg.anyErrors () then
1765 case D.prove env denv (c1, c2, loc) of 1783 ()
1766 [] => () 1784 else
1767 | _ => 1785 app (fn (loc, env, denv, (c1, c2)) =>
1768 (ErrorMsg.errorAt loc "Remaining constraint"; 1786 case D.prove env denv (c1, c2, loc) of
1769 eprefaces' [("Con 1", p_con env c1), 1787 [] => ()
1770 ("Con 2", p_con env c2)])) gs; 1788 | _ =>
1789 (ErrorMsg.errorAt loc "Remaining constraint";
1790 eprefaces' [("Con 1", p_con env c1),
1791 ("Con 2", p_con env c2)])) gs;
1771 1792
1772 (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan) :: ds @ file 1793 (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan) :: ds @ file
1773 end 1794 end
1774 1795
1775 end 1796 end