Mercurial > urweb

comparison src/elaborate.sml @ 2:64f09f7822c3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Start of elaboration
author Adam Chlipala <adamc@hcoop.net>
date Sat, 26 Jan 2008 14:27:33 -0500
parents
children daa4f1d7a663
comparison
equal deleted inserted replaced
1:4202f6eda946 2:64f09f7822c3
1 (* Copyright (c) 2008, Adam Chlipala
2 * All rights reserved.
3 *
4 * Redistribution and use in source and binary forms, with or without
5 * modification, are permitted provided that the following conditions are met:
6 *
7 * - Redistributions of source code must retain the above copyright notice,
8 * this list of conditions and the following disclaimer.
9 * - Redistributions in binary form must reproduce the above copyright notice,
10 * this list of conditions and the following disclaimer in the documentation
11 * and/or other materials provided with the distribution.
12 * - The names of contributors may not be used to endorse or promote products
13 * derived from this software without specific prior written permission.
14 *
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
17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
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
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
25 * POSSIBILITY OF SUCH DAMAGE.
26 *)
27
28 structure Elaborate :> ELABORATE = struct
29
30 structure L = Laconic
31 structure L' = Elab
32 structure E = ElabEnv
33 structure U = ElabUtil
34
35 fun elabKind (k, loc) =
36 case k of
37 L.KType => (L'.KType, loc)
38 | L.KArrow (k1, k2) => (L'.KArrow (elabKind k1, elabKind k2), loc)
39 | L.KName => (L'.KName, loc)
40 | L.KRecord k => (L'.KRecord (elabKind k), loc)
41
42 fun elabExplicitness e =
43 case e of
44 L.Explicit => L'.Explicit
45 | L.Implicit => L'.Implicit
46
47 fun occursKind r =
48 U.Kind.exists (fn L'.KUnif (_, r') => r = r'
49 | _ => false)
50
51 datatype unify_error =
52 KOccursCheckFailed of L'.kind * L'.kind
53 | KIncompatible of L'.kind * L'.kind
54
55 fun unifyError err =
56 case err of
57 KOccursCheckFailed (k1, k2) =>
58 ErrorMsg.errorAt (#2 k1) "Kind occurs check failed"
59 | KIncompatible (k1, k2) =>
60 ErrorMsg.errorAt (#2 k1) "Incompatible kinds"
61
62 fun unifyKinds (k1All as (k1, pos)) (k2All as (k2, _)) =
63 let
64 fun err f = unifyError (f (k1All, k2All))
65 in
66 case (k1, k2) of
67 (L'.KType, L'.KType) => ()
68 | (L'.KArrow (d1, r1), L'.KArrow (d2, r2)) =>
69 (unifyKinds d1 d2;
70 unifyKinds r1 r2)
71 | (L'.KName, L'.KName) => ()
72 | (L'.KRecord k1, L'.KRecord k2) => unifyKinds k1 k2
73
74 | (L'.KError, _) => ()
75 | (_, L'.KError) => ()
76
77 | (L'.KUnif (_, ref (SOME k1All)), _) => unifyKinds k1All k2All
78 | (_, L'.KUnif (_, ref (SOME k2All))) => unifyKinds k1All k2All
79
80 | (L'.KUnif (_, r1), L'.KUnif (_, r2)) =>
81 if r1 = r2 then
82 ()
83 else
84 r1 := SOME k2All
85
86 | (L'.KUnif (_, r), _) =>
87 if occursKind r k2All then
88 err KOccursCheckFailed
89 else
90 r := SOME k2All
91 | (_, L'.KUnif (_, r)) =>
92 if occursKind r k1All then
93 err KOccursCheckFailed
94 else
95 r := SOME k1All
96
97 | _ => err KIncompatible
98 end
99
100 fun elabFile _ = raise Fail ""
101
102 end