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 ElabUtil :> ELAB_UTIL = struct
|
adamc@2
|
29
|
adamc@2
|
30 open Elab
|
adamc@2
|
31
|
adamc@2
|
32 structure S = Search
|
adamc@2
|
33
|
adamc@2
|
34 structure Kind = struct
|
adamc@2
|
35
|
adamc@6
|
36 fun mapfold f =
|
adamc@2
|
37 let
|
adamc@2
|
38 fun mfk k acc =
|
adamc@2
|
39 S.bindP (mfk' k acc, f)
|
adamc@2
|
40
|
adamc@2
|
41 and mfk' (kAll as (k, loc)) =
|
adamc@2
|
42 case k of
|
adamc@2
|
43 KType => S.return2 kAll
|
adamc@2
|
44
|
adamc@2
|
45 | KArrow (k1, k2) =>
|
adamc@2
|
46 S.bind2 (mfk k1,
|
adamc@2
|
47 fn k1' =>
|
adamc@2
|
48 S.map2 (mfk k2,
|
adamc@2
|
49 fn k2' =>
|
adamc@2
|
50 (KArrow (k1', k2'), loc)))
|
adamc@2
|
51
|
adamc@2
|
52 | KName => S.return2 kAll
|
adamc@2
|
53
|
adamc@2
|
54 | KRecord k =>
|
adamc@2
|
55 S.map2 (mfk k,
|
adamc@2
|
56 fn k' =>
|
adamc@2
|
57 (KRecord k', loc))
|
adamc@2
|
58
|
adamc@2
|
59 | KError => S.return2 kAll
|
adamc@2
|
60
|
adamc@2
|
61 | KUnif (_, ref (SOME k)) => mfk' k
|
adamc@2
|
62 | KUnif _ => S.return2 kAll
|
adamc@2
|
63 in
|
adamc@2
|
64 mfk
|
adamc@2
|
65 end
|
adamc@2
|
66
|
adamc@2
|
67 fun exists f k =
|
adamc@6
|
68 case mapfold (fn k => fn () =>
|
adamc@6
|
69 if f k then
|
adamc@6
|
70 S.Return ()
|
adamc@6
|
71 else
|
adamc@6
|
72 S.Continue (k, ())) k () of
|
adamc@6
|
73 S.Return _ => true
|
adamc@6
|
74 | S.Continue _ => false
|
adamc@6
|
75
|
adamc@6
|
76 end
|
adamc@6
|
77
|
adamc@6
|
78 structure Con = struct
|
adamc@6
|
79
|
adamc@6
|
80 fun mapfold {kind = fk, con = fc} =
|
adamc@6
|
81 let
|
adamc@6
|
82 val mfk = Kind.mapfold fk
|
adamc@6
|
83
|
adamc@6
|
84 fun mfc c acc =
|
adamc@6
|
85 S.bindP (mfc' c acc, fc)
|
adamc@6
|
86
|
adamc@6
|
87 and mfc' (cAll as (c, loc)) =
|
adamc@6
|
88 case c of
|
adamc@6
|
89 TFun (c1, c2) =>
|
adamc@6
|
90 S.bind2 (mfc c1,
|
adamc@6
|
91 fn c1' =>
|
adamc@6
|
92 S.map2 (mfc c2,
|
adamc@6
|
93 fn c2' =>
|
adamc@6
|
94 (TFun (c1', c2'), loc)))
|
adamc@6
|
95 | TCFun (e, x, k, c) =>
|
adamc@6
|
96 S.bind2 (mfk k,
|
adamc@6
|
97 fn k' =>
|
adamc@6
|
98 S.map2 (mfc c,
|
adamc@6
|
99 fn c' =>
|
adamc@6
|
100 (TCFun (e, x, k', c'), loc)))
|
adamc@6
|
101 | TRecord c =>
|
adamc@6
|
102 S.map2 (mfc c,
|
adamc@6
|
103 fn c' =>
|
adamc@6
|
104 (TRecord c', loc))
|
adamc@6
|
105
|
adamc@6
|
106 | CRel _ => S.return2 cAll
|
adamc@6
|
107 | CNamed _ => S.return2 cAll
|
adamc@6
|
108 | CApp (c1, c2) =>
|
adamc@6
|
109 S.bind2 (mfc c1,
|
adamc@6
|
110 fn c1' =>
|
adamc@6
|
111 S.map2 (mfc c2,
|
adamc@6
|
112 fn c2' =>
|
adamc@6
|
113 (CApp (c1', c2'), loc)))
|
adamc@8
|
114 | CAbs (x, k, c) =>
|
adamc@6
|
115 S.bind2 (mfk k,
|
adamc@6
|
116 fn k' =>
|
adamc@6
|
117 S.map2 (mfc c,
|
adamc@6
|
118 fn c' =>
|
adamc@8
|
119 (CAbs (x, k', c'), loc)))
|
adamc@6
|
120
|
adamc@6
|
121 | CName _ => S.return2 cAll
|
adamc@6
|
122
|
adamc@6
|
123 | CRecord (k, xcs) =>
|
adamc@6
|
124 S.bind2 (mfk k,
|
adamc@6
|
125 fn k' =>
|
adamc@6
|
126 S.map2 (ListUtil.mapfold (fn (x, c) =>
|
adamc@6
|
127 S.bind2 (mfc x,
|
adamc@6
|
128 fn x' =>
|
adamc@6
|
129 S.map2 (mfc c,
|
adamc@6
|
130 fn c' =>
|
adamc@6
|
131 (x', c'))))
|
adamc@6
|
132 xcs,
|
adamc@6
|
133 fn xcs' =>
|
adamc@6
|
134 (CRecord (k', xcs'), loc)))
|
adamc@6
|
135 | CConcat (c1, c2) =>
|
adamc@6
|
136 S.bind2 (mfc c1,
|
adamc@6
|
137 fn c1' =>
|
adamc@6
|
138 S.map2 (mfc c2,
|
adamc@6
|
139 fn c2' =>
|
adamc@6
|
140 (CConcat (c1', c2'), loc)))
|
adamc@6
|
141
|
adamc@6
|
142 | CError => S.return2 cAll
|
adamc@6
|
143 | CUnif (_, _, ref (SOME c)) => mfc' c
|
adamc@6
|
144 | CUnif _ => S.return2 cAll
|
adamc@6
|
145 in
|
adamc@6
|
146 mfc
|
adamc@6
|
147 end
|
adamc@6
|
148
|
adamc@6
|
149 fun exists {kind, con} k =
|
adamc@6
|
150 case mapfold {kind = fn k => fn () =>
|
adamc@6
|
151 if kind k then
|
adamc@6
|
152 S.Return ()
|
adamc@6
|
153 else
|
adamc@6
|
154 S.Continue (k, ()),
|
adamc@6
|
155 con = fn c => fn () =>
|
adamc@6
|
156 if con c then
|
adamc@6
|
157 S.Return ()
|
adamc@6
|
158 else
|
adamc@6
|
159 S.Continue (c, ())} k () of
|
adamc@2
|
160 S.Return _ => true
|
adamc@2
|
161 | S.Continue _ => false
|
adamc@2
|
162
|
adamc@2
|
163 end
|
adamc@2
|
164
|
adamc@10
|
165 structure Exp = struct
|
adamc@10
|
166
|
adamc@10
|
167 fun mapfold {kind = fk, con = fc, exp = fe} =
|
adamc@10
|
168 let
|
adamc@10
|
169 val mfk = Kind.mapfold fk
|
adamc@10
|
170 val mfc = Con.mapfold {kind = fk, con = fc}
|
adamc@10
|
171
|
adamc@10
|
172 fun mfe e acc =
|
adamc@10
|
173 S.bindP (mfe' e acc, fe)
|
adamc@10
|
174
|
adamc@10
|
175 and mfe' (eAll as (e, loc)) =
|
adamc@10
|
176 case e of
|
adamc@10
|
177 ERel _ => S.return2 eAll
|
adamc@10
|
178 | ENamed _ => S.return2 eAll
|
adamc@10
|
179 | EApp (e1, e2) =>
|
adamc@10
|
180 S.bind2 (mfe e1,
|
adamc@10
|
181 fn e1' =>
|
adamc@10
|
182 S.map2 (mfe e2,
|
adamc@10
|
183 fn e2' =>
|
adamc@10
|
184 (EApp (e1', e2'), loc)))
|
adamc@10
|
185 | EAbs (x, t, e) =>
|
adamc@10
|
186 S.bind2 (mfc t,
|
adamc@10
|
187 fn t' =>
|
adamc@10
|
188 S.map2 (mfe e,
|
adamc@10
|
189 fn e' =>
|
adamc@10
|
190 (EAbs (x, t', e'), loc)))
|
adamc@10
|
191
|
adamc@10
|
192 | ECApp (e, c) =>
|
adamc@10
|
193 S.bind2 (mfe e,
|
adamc@10
|
194 fn e' =>
|
adamc@10
|
195 S.map2 (mfc c,
|
adamc@10
|
196 fn c' =>
|
adamc@10
|
197 (ECApp (e', c'), loc)))
|
adamc@10
|
198 | ECAbs (expl, x, k, e) =>
|
adamc@10
|
199 S.bind2 (mfk k,
|
adamc@10
|
200 fn k' =>
|
adamc@10
|
201 S.map2 (mfe e,
|
adamc@10
|
202 fn e' =>
|
adamc@10
|
203 (ECAbs (expl, x, k', e'), loc)))
|
adamc@10
|
204
|
adamc@10
|
205 | EError => S.return2 eAll
|
adamc@10
|
206 in
|
adamc@10
|
207 mfe
|
adamc@10
|
208 end
|
adamc@10
|
209
|
adamc@10
|
210 fun exists {kind, con, exp} k =
|
adamc@10
|
211 case mapfold {kind = fn k => fn () =>
|
adamc@10
|
212 if kind k then
|
adamc@10
|
213 S.Return ()
|
adamc@10
|
214 else
|
adamc@10
|
215 S.Continue (k, ()),
|
adamc@10
|
216 con = fn c => fn () =>
|
adamc@10
|
217 if con c then
|
adamc@10
|
218 S.Return ()
|
adamc@10
|
219 else
|
adamc@10
|
220 S.Continue (c, ()),
|
adamc@10
|
221 exp = fn e => fn () =>
|
adamc@10
|
222 if exp e then
|
adamc@10
|
223 S.Return ()
|
adamc@10
|
224 else
|
adamc@10
|
225 S.Continue (e, ())} k () of
|
adamc@10
|
226 S.Return _ => true
|
adamc@10
|
227 | S.Continue _ => false
|
adamc@10
|
228
|
adamc@10
|
229 end
|
adamc@10
|
230
|
adamc@3
|
231 structure E = ElabEnv
|
adamc@3
|
232
|
adamc@3
|
233 fun declBinds env (d, _) =
|
adamc@3
|
234 case d of
|
adamc@5
|
235 DCon (x, n, k, _) => E.pushCNamedAs env x n k
|
adamc@9
|
236 | DVal (x, n, t, _) => E.pushENamedAs env x n t
|
adamc@3
|
237
|
adamc@2
|
238 end
|