|
adamc@2
|
1 (* Copyright (c) 2008, Adam Chlipala
|
|
adamc@2
|
2 * All rights reserved.
|
|
adamc@2
|
3 *
|
|
adamc@2
|
4 * Redistribution and use in source and binary forms, with or without
|
|
adamc@2
|
5 * modification, are permitted provided that the following conditions are met:
|
|
adamc@2
|
6 *
|
|
adamc@2
|
7 * - Redistributions of source code must retain the above copyright notice,
|
|
adamc@2
|
8 * this list of conditions and the following disclaimer.
|
|
adamc@2
|
9 * - Redistributions in binary form must reproduce the above copyright notice,
|
|
adamc@2
|
10 * this list of conditions and the following disclaimer in the documentation
|
|
adamc@2
|
11 * and/or other materials provided with the distribution.
|
|
adamc@2
|
12 * - The names of contributors may not be used to endorse or promote products
|
|
adamc@2
|
13 * derived from this software without specific prior written permission.
|
|
adamc@2
|
14 *
|
|
adamc@2
|
15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
|
|
adamc@2
|
16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
|
|
adamc@2
|
17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
|
|
adamc@2
|
18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
|
|
adamc@2
|
19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
|
|
adamc@2
|
20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
|
|
adamc@2
|
21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
|
|
adamc@2
|
22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
|
|
adamc@2
|
23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
|
|
adamc@2
|
24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
|
|
adamc@2
|
25 * POSSIBILITY OF SUCH DAMAGE.
|
|
adamc@2
|
26 *)
|
|
adamc@2
|
27
|
|
adamc@2
|
28 structure Elaborate :> ELABORATE = struct
|
|
adamc@2
|
29
|
|
adamc@2
|
30 structure L = Laconic
|
|
adamc@2
|
31 structure L' = Elab
|
|
adamc@2
|
32 structure E = ElabEnv
|
|
adamc@2
|
33 structure U = ElabUtil
|
|
adamc@2
|
34
|
|
adamc@2
|
35 fun elabKind (k, loc) =
|
|
adamc@2
|
36 case k of
|
|
adamc@2
|
37 L.KType => (L'.KType, loc)
|
|
adamc@2
|
38 | L.KArrow (k1, k2) => (L'.KArrow (elabKind k1, elabKind k2), loc)
|
|
adamc@2
|
39 | L.KName => (L'.KName, loc)
|
|
adamc@2
|
40 | L.KRecord k => (L'.KRecord (elabKind k), loc)
|
|
adamc@2
|
41
|
|
adamc@2
|
42 fun elabExplicitness e =
|
|
adamc@2
|
43 case e of
|
|
adamc@2
|
44 L.Explicit => L'.Explicit
|
|
adamc@2
|
45 | L.Implicit => L'.Implicit
|
|
adamc@2
|
46
|
|
adamc@2
|
47 fun occursKind r =
|
|
adamc@2
|
48 U.Kind.exists (fn L'.KUnif (_, r') => r = r'
|
|
adamc@2
|
49 | _ => false)
|
|
adamc@2
|
50
|
|
adamc@2
|
51 datatype unify_error =
|
|
adamc@2
|
52 KOccursCheckFailed of L'.kind * L'.kind
|
|
adamc@2
|
53 | KIncompatible of L'.kind * L'.kind
|
|
adamc@2
|
54
|
|
adamc@2
|
55 fun unifyError err =
|
|
adamc@2
|
56 case err of
|
|
adamc@2
|
57 KOccursCheckFailed (k1, k2) =>
|
|
adamc@2
|
58 ErrorMsg.errorAt (#2 k1) "Kind occurs check failed"
|
|
adamc@2
|
59 | KIncompatible (k1, k2) =>
|
|
adamc@2
|
60 ErrorMsg.errorAt (#2 k1) "Incompatible kinds"
|
|
adamc@2
|
61
|
|
adamc@2
|
62 fun unifyKinds (k1All as (k1, pos)) (k2All as (k2, _)) =
|
|
adamc@2
|
63 let
|
|
adamc@2
|
64 fun err f = unifyError (f (k1All, k2All))
|
|
adamc@2
|
65 in
|
|
adamc@2
|
66 case (k1, k2) of
|
|
adamc@2
|
67 (L'.KType, L'.KType) => ()
|
|
adamc@2
|
68 | (L'.KArrow (d1, r1), L'.KArrow (d2, r2)) =>
|
|
adamc@2
|
69 (unifyKinds d1 d2;
|
|
adamc@2
|
70 unifyKinds r1 r2)
|
|
adamc@2
|
71 | (L'.KName, L'.KName) => ()
|
|
adamc@2
|
72 | (L'.KRecord k1, L'.KRecord k2) => unifyKinds k1 k2
|
|
adamc@2
|
73
|
|
adamc@2
|
74 | (L'.KError, _) => ()
|
|
adamc@2
|
75 | (_, L'.KError) => ()
|
|
adamc@2
|
76
|
|
adamc@2
|
77 | (L'.KUnif (_, ref (SOME k1All)), _) => unifyKinds k1All k2All
|
|
adamc@2
|
78 | (_, L'.KUnif (_, ref (SOME k2All))) => unifyKinds k1All k2All
|
|
adamc@2
|
79
|
|
adamc@2
|
80 | (L'.KUnif (_, r1), L'.KUnif (_, r2)) =>
|
|
adamc@2
|
81 if r1 = r2 then
|
|
adamc@2
|
82 ()
|
|
adamc@2
|
83 else
|
|
adamc@2
|
84 r1 := SOME k2All
|
|
adamc@2
|
85
|
|
adamc@2
|
86 | (L'.KUnif (_, r), _) =>
|
|
adamc@2
|
87 if occursKind r k2All then
|
|
adamc@2
|
88 err KOccursCheckFailed
|
|
adamc@2
|
89 else
|
|
adamc@2
|
90 r := SOME k2All
|
|
adamc@2
|
91 | (_, L'.KUnif (_, r)) =>
|
|
adamc@2
|
92 if occursKind r k1All then
|
|
adamc@2
|
93 err KOccursCheckFailed
|
|
adamc@2
|
94 else
|
|
adamc@2
|
95 r := SOME k1All
|
|
adamc@2
|
96
|
|
adamc@2
|
97 | _ => err KIncompatible
|
|
adamc@2
|
98 end
|
|
adamc@2
|
99
|
|
adamc@2
|
100 fun elabFile _ = raise Fail ""
|
|
adamc@2
|
101
|
|
adamc@2
|
102 end
|
