Mercurial > urweb

comparison src/elaborate.sml @ 445:dfc8c991abd0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Replace 'with' with '++'
author Adam Chlipala <adamc@hcoop.net>
date Fri, 31 Oct 2008 09:30:22 -0400
parents 6a0e54400805
children b77863cd0be2
comparison
equal deleted inserted replaced
444:f45f23ae20ed 445:dfc8c991abd0
1 (* Copyright (c) 2008, Adam Chlipala 1 (* Copyright (c) 2008, Adam Chlipala
2 * All rights reserved. 2 * All rights reserved.
3 * 3 *
4 * Redistribution and use in source and binary forms, with or without 4 * Redistribution and use in source and binary forms, with or without
5 * modification, are permitted provided that the following conditions are met: 5 * modification, are permitted provided that the following conditions are met:
6 * 6 *
7 * - Redistributions of source code must retain the above copyright notice, 7 * - Redistributions of source code must retain the above copyright notice,
8 * this list of conditions and the following disclaimer. 8 * this list of conditions and the following disclaimer.
9 * - Redistributions in binary form must reproduce the above copyright notice, 9 * - Redistributions in binary form must reproduce the above copyright notice,
10 * this list of conditions and the following disclaimer in the documentation 10 * this list of conditions and the following disclaimer in the documentation
11 * and/or other materials provided with the distribution. 11 * and/or other materials provided with the distribution.
12 * - The names of contributors may not be used to endorse or promote products 12 * - The names of contributors may not be used to endorse or promote products
13 * derived from this software without specific prior written permission. 13 * derived from this software without specific prior written permission.
14 * 14 *
15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" 15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE 16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE 17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE 18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR 19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF 20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS 21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN 22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) 23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE 24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
25 * POSSIBILITY OF SUCH DAMAGE. 25 * POSSIBILITY OF SUCH DAMAGE.
26 *) 26 *)
27 27
28 structure Elaborate :> ELABORATE = struct 28 structure Elaborate :> ELABORATE = struct
29 29
30 structure P = Prim 30 structure P = Prim
31 structure L = Source 31 structure L = Source
1601 val gs4 = D.prove env denv (first, rest, loc) 1601 val gs4 = D.prove env denv (first, rest, loc)
1602 in 1602 in
1603 ((L'.EField (e', c', {field = ft, rest = rest}), loc), ft, gs1 @ enD gs2 @ enD gs3 @ enD gs4) 1603 ((L'.EField (e', c', {field = ft, rest = rest}), loc), ft, gs1 @ enD gs2 @ enD gs3 @ enD gs4)
1604 end 1604 end
1605 1605
1606 | L.EWith (e1, c, e2) => 1606 | L.EConcat (e1, e2) =>
1607 let 1607 let
1608 val (e1', e1t, gs1) = elabExp (env, denv) e1 1608 val (e1', e1t, gs1) = elabExp (env, denv) e1
1609 val (c', ck, gs2) = elabCon (env, denv) c 1609 val (e2', e2t, gs2) = elabExp (env, denv) e2
1610 val (e2', e2t, gs3) = elabExp (env, denv) e2 1610
1611 1611 val r1 = cunif (loc, ktype_record)
1612 val rest = cunif (loc, ktype_record) 1612 val r2 = cunif (loc, ktype_record)
1613 val first = (L'.CRecord (ktype, [(c', e2t)]), loc) 1613
1614 1614 val gs3 = checkCon (env, denv) e1' e1t (L'.TRecord r1, loc)
1615 val gs4 = checkCon (env, denv) e1' e1t (L'.TRecord rest, loc) 1615 val gs4 = checkCon (env, denv) e2' e2t (L'.TRecord r2, loc)
1616 val gs5 = D.prove env denv (first, rest, loc) 1616 val gs5 = D.prove env denv (r1, r2, loc)
1617 in 1617 in
1618 ((L'.EWith (e1', c', e2', {field = e2t, rest = rest}), loc), 1618 ((L'.EConcat (e1', r1, e2', r2), loc),
1619 (L'.TRecord ((L'.CConcat (first, rest), loc)), loc), 1619 (L'.TRecord ((L'.CConcat (r1, r2), loc)), loc),
1620 gs1 @ enD gs2 @ gs3 @ enD gs4 @ enD gs5) 1620 gs1 @ gs2 @ enD gs3 @ enD gs4 @ enD gs5)
1621 end 1621 end
1622 | L.ECut (e, c) => 1622 | L.ECut (e, c) =>
1623 let 1623 let
1624 val (e', et, gs1) = elabExp (env, denv) e 1624 val (e', et, gs1) = elabExp (env, denv) e
1625 val (c', ck, gs2) = elabCon (env, denv) c 1625 val (c', ck, gs2) = elabCon (env, denv) c