Mercurial > urweb

comparison src/elaborate.sml @ 1299:3c334458c84f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fix typing of cut operators; fix lexing of XML comments
author Adam Chlipala <adam@chlipala.net>
date Thu, 16 Sep 2010 15:34:50 -0400
parents b4480a56cab7
children d008c4c43a0a
comparison
equal deleted inserted replaced
1298:e665527fce1c 1299:3c334458c84f
1996 val () = checkCon env e' et 1996 val () = checkCon env e' et
1997 (L'.TRecord (L'.CConcat (first, rest), loc), loc) 1997 (L'.TRecord (L'.CConcat (first, rest), loc), loc)
1998 1998
1999 val gs3 = D.prove env denv (first, rest, loc) 1999 val gs3 = D.prove env denv (first, rest, loc)
2000 in 2000 in
2001 checkKind env c' ck kname;
2001 ((L'.ECut (e', c', {field = ft, rest = rest}), loc), (L'.TRecord rest, loc), 2002 ((L'.ECut (e', c', {field = ft, rest = rest}), loc), (L'.TRecord rest, loc),
2002 gs1 @ enD gs2 @ enD gs3) 2003 gs1 @ enD gs2 @ enD gs3)
2003 end 2004 end
2004 | L.ECutMulti (e, c) => 2005 | L.ECutMulti (e, c) =>
2005 let 2006 let
2011 val () = checkCon env e' et 2012 val () = checkCon env e' et
2012 (L'.TRecord (L'.CConcat (c', rest), loc), loc) 2013 (L'.TRecord (L'.CConcat (c', rest), loc), loc)
2013 2014
2014 val gs3 = D.prove env denv (c', rest, loc) 2015 val gs3 = D.prove env denv (c', rest, loc)
2015 in 2016 in
2017 checkKind env c' ck (L'.KRecord ktype, loc);
2016 ((L'.ECutMulti (e', c', {rest = rest}), loc), (L'.TRecord rest, loc), 2018 ((L'.ECutMulti (e', c', {rest = rest}), loc), (L'.TRecord rest, loc),
2017 gs1 @ enD gs2 @ enD gs3) 2019 gs1 @ enD gs2 @ enD gs3)
2018 end 2020 end
2019 2021
2020 | L.ECase (e, pes) => 2022 | L.ECase (e, pes) =>