adamc@674
|
1 (* Copyright (c) 2008-2009, 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 ElabEnv :> ELAB_ENV = struct
|
adamc@2
|
29
|
adamc@2
|
30 open Elab
|
adamc@2
|
31
|
adamc@13
|
32 structure U = ElabUtil
|
adamc@13
|
33
|
adamc@2
|
34 structure IM = IntBinaryMap
|
adamc@2
|
35 structure SM = BinaryMapFn(struct
|
adamc@2
|
36 type ord_key = string
|
adamc@2
|
37 val compare = String.compare
|
adamc@2
|
38 end)
|
adamc@2
|
39
|
adamc@2
|
40 exception UnboundRel of int
|
adamc@2
|
41 exception UnboundNamed of int
|
adamc@2
|
42
|
adamc@13
|
43
|
adamc@13
|
44 (* AST utility functions *)
|
adamc@13
|
45
|
adamc@13
|
46 exception SynUnif
|
adamc@13
|
47
|
adamc@623
|
48 val liftKindInKind =
|
adamc@623
|
49 U.Kind.mapB {kind = fn bound => fn k =>
|
adamc@623
|
50 case k of
|
adamc@623
|
51 KRel xn =>
|
adamc@623
|
52 if xn < bound then
|
adamc@623
|
53 k
|
adamc@623
|
54 else
|
adamc@623
|
55 KRel (xn + 1)
|
adamc@623
|
56 | _ => k,
|
adamc@623
|
57 bind = fn (bound, _) => bound + 1}
|
adamc@623
|
58
|
adamc@623
|
59 val liftKindInCon =
|
adamc@623
|
60 U.Con.mapB {kind = fn bound => fn k =>
|
adamc@623
|
61 case k of
|
adamc@623
|
62 KRel xn =>
|
adamc@623
|
63 if xn < bound then
|
adamc@623
|
64 k
|
adamc@623
|
65 else
|
adamc@623
|
66 KRel (xn + 1)
|
adamc@623
|
67 | _ => k,
|
adamc@623
|
68 con = fn _ => fn c => c,
|
adamc@623
|
69 bind = fn (bound, U.Con.RelK _) => bound + 1
|
adamc@623
|
70 | (bound, _) => bound}
|
adamc@623
|
71
|
adamc@13
|
72 val liftConInCon =
|
adamc@623
|
73 U.Con.mapB {kind = fn _ => fn k => k,
|
adamc@13
|
74 con = fn bound => fn c =>
|
adamc@13
|
75 case c of
|
adamc@16
|
76 CRel xn =>
|
adamc@13
|
77 if xn < bound then
|
adamc@13
|
78 c
|
adamc@13
|
79 else
|
adamc@16
|
80 CRel (xn + 1)
|
adamc@17
|
81 (*| CUnif _ => raise SynUnif*)
|
adamc@13
|
82 | _ => c,
|
adamc@623
|
83 bind = fn (bound, U.Con.RelC _) => bound + 1
|
adamc@13
|
84 | (bound, _) => bound}
|
adamc@13
|
85
|
adamc@13
|
86 val lift = liftConInCon 0
|
adamc@13
|
87
|
adamc@623
|
88 val liftKindInExp =
|
adamc@623
|
89 U.Exp.mapB {kind = fn bound => fn k =>
|
adamc@623
|
90 case k of
|
adamc@623
|
91 KRel xn =>
|
adamc@623
|
92 if xn < bound then
|
adamc@623
|
93 k
|
adamc@623
|
94 else
|
adamc@623
|
95 KRel (xn + 1)
|
adamc@623
|
96 | _ => k,
|
adamc@623
|
97 con = fn _ => fn c => c,
|
adamc@623
|
98 exp = fn _ => fn e => e,
|
adamc@623
|
99 bind = fn (bound, U.Exp.RelK _) => bound + 1
|
adamc@623
|
100 | (bound, _) => bound}
|
adamc@623
|
101
|
adamc@448
|
102 val liftConInExp =
|
adamc@623
|
103 U.Exp.mapB {kind = fn _ => fn k => k,
|
adamc@448
|
104 con = fn bound => fn c =>
|
adamc@448
|
105 case c of
|
adamc@448
|
106 CRel xn =>
|
adamc@448
|
107 if xn < bound then
|
adamc@448
|
108 c
|
adamc@448
|
109 else
|
adamc@448
|
110 CRel (xn + 1)
|
adamc@448
|
111 | _ => c,
|
adamc@448
|
112 exp = fn _ => fn e => e,
|
adamc@448
|
113 bind = fn (bound, U.Exp.RelC _) => bound + 1
|
adamc@448
|
114 | (bound, _) => bound}
|
adamc@448
|
115
|
adamc@211
|
116 val liftExpInExp =
|
adamc@623
|
117 U.Exp.mapB {kind = fn _ => fn k => k,
|
adamc@211
|
118 con = fn _ => fn c => c,
|
adamc@211
|
119 exp = fn bound => fn e =>
|
adamc@211
|
120 case e of
|
adamc@211
|
121 ERel xn =>
|
adamc@211
|
122 if xn < bound then
|
adamc@211
|
123 e
|
adamc@211
|
124 else
|
adamc@211
|
125 ERel (xn + 1)
|
adamc@211
|
126 | _ => e,
|
adamc@211
|
127 bind = fn (bound, U.Exp.RelE _) => bound + 1
|
adamc@211
|
128 | (bound, _) => bound}
|
adamc@211
|
129
|
adamc@211
|
130
|
adamc@211
|
131 val liftExp = liftExpInExp 0
|
adamc@13
|
132
|
adamc@448
|
133 val subExpInExp =
|
adamc@623
|
134 U.Exp.mapB {kind = fn _ => fn k => k,
|
adamc@448
|
135 con = fn _ => fn c => c,
|
adamc@448
|
136 exp = fn (xn, rep) => fn e =>
|
adamc@448
|
137 case e of
|
adamc@448
|
138 ERel xn' =>
|
adamc@448
|
139 (case Int.compare (xn', xn) of
|
adamc@448
|
140 EQUAL => #1 rep
|
adamc@448
|
141 | GREATER=> ERel (xn' - 1)
|
adamc@448
|
142 | LESS => e)
|
adamc@448
|
143 | _ => e,
|
adamc@448
|
144 bind = fn ((xn, rep), U.Exp.RelE _) => (xn+1, liftExpInExp 0 rep)
|
adamc@448
|
145 | ((xn, rep), U.Exp.RelC _) => (xn, liftConInExp 0 rep)
|
adamc@448
|
146 | (ctx, _) => ctx}
|
adamc@448
|
147
|
adamc@13
|
148 (* Back to environments *)
|
adamc@13
|
149
|
adamc@9
|
150 datatype 'a var' =
|
adamc@9
|
151 Rel' of int * 'a
|
adamc@9
|
152 | Named' of int * 'a
|
adamc@2
|
153
|
adamc@9
|
154 datatype 'a var =
|
adamc@9
|
155 NotBound
|
adamc@9
|
156 | Rel of int * 'a
|
adamc@9
|
157 | Named of int * 'a
|
adamc@2
|
158
|
adamc@191
|
159 type datatyp = string list * (string * con option) IM.map
|
adamc@157
|
160
|
adamc@211
|
161 datatype class_name =
|
adamc@211
|
162 ClNamed of int
|
adamc@211
|
163 | ClProj of int * string list * string
|
adamc@211
|
164
|
adamc@216
|
165 fun cn2s cn =
|
adamc@216
|
166 case cn of
|
adamc@216
|
167 ClNamed n => "Named(" ^ Int.toString n ^ ")"
|
adamc@216
|
168 | ClProj (m, ms, x) => "Proj(" ^ Int.toString m ^ "," ^ String.concatWith "," ms ^ "," ^ x ^ ")"
|
adamc@216
|
169
|
adamc@211
|
170 structure CK = struct
|
adamc@211
|
171 type ord_key = class_name
|
adamc@211
|
172 open Order
|
adamc@211
|
173 fun compare x =
|
adamc@211
|
174 case x of
|
adamc@211
|
175 (ClNamed n1, ClNamed n2) => Int.compare (n1, n2)
|
adamc@211
|
176 | (ClNamed _, _) => LESS
|
adamc@211
|
177 | (_, ClNamed _) => GREATER
|
adamc@211
|
178
|
adamc@211
|
179 | (ClProj (m1, ms1, x1), ClProj (m2, ms2, x2)) =>
|
adamc@211
|
180 join (Int.compare (m1, m2),
|
adamc@211
|
181 fn () => join (joinL String.compare (ms1, ms2),
|
adamc@211
|
182 fn () => String.compare (x1, x2)))
|
adamc@211
|
183 end
|
adamc@211
|
184
|
adamc@211
|
185 structure CM = BinaryMapFn(CK)
|
adamc@211
|
186
|
adamc@211
|
187 datatype class_key =
|
adamc@211
|
188 CkNamed of int
|
adamc@211
|
189 | CkRel of int
|
adamc@211
|
190 | CkProj of int * string list * string
|
adamc@467
|
191 | CkApp of class_key * class_key
|
adamc@211
|
192
|
adamc@216
|
193 fun ck2s ck =
|
adamc@216
|
194 case ck of
|
adamc@216
|
195 CkNamed n => "Named(" ^ Int.toString n ^ ")"
|
adamc@216
|
196 | CkRel n => "Rel(" ^ Int.toString n ^ ")"
|
adamc@216
|
197 | CkProj (m, ms, x) => "Proj(" ^ Int.toString m ^ "," ^ String.concatWith "," ms ^ "," ^ x ^ ")"
|
adamc@467
|
198 | CkApp (ck1, ck2) => "App(" ^ ck2s ck1 ^ ", " ^ ck2s ck2 ^ ")"
|
adamc@216
|
199
|
adamc@674
|
200 type class_key_n = class_key * int
|
adamc@674
|
201
|
adamc@674
|
202 fun ckn2s (ck, n) = ck2s ck ^ "[" ^ Int.toString n ^ "]"
|
adamc@674
|
203
|
adamc@216
|
204 fun cp2s (cn, ck) = "(" ^ cn2s cn ^ "," ^ ck2s ck ^ ")"
|
adamc@216
|
205
|
adamc@211
|
206 structure KK = struct
|
adamc@674
|
207 type ord_key = class_key_n
|
adamc@211
|
208 open Order
|
adamc@674
|
209 fun compare' x =
|
adamc@211
|
210 case x of
|
adamc@211
|
211 (CkNamed n1, CkNamed n2) => Int.compare (n1, n2)
|
adamc@211
|
212 | (CkNamed _, _) => LESS
|
adamc@211
|
213 | (_, CkNamed _) => GREATER
|
adamc@211
|
214
|
adamc@211
|
215 | (CkRel n1, CkRel n2) => Int.compare (n1, n2)
|
adamc@211
|
216 | (CkRel _, _) => LESS
|
adamc@211
|
217 | (_, CkRel _) => GREATER
|
adamc@211
|
218
|
adamc@211
|
219 | (CkProj (m1, ms1, x1), CkProj (m2, ms2, x2)) =>
|
adamc@211
|
220 join (Int.compare (m1, m2),
|
adamc@211
|
221 fn () => join (joinL String.compare (ms1, ms2),
|
adamc@211
|
222 fn () => String.compare (x1, x2)))
|
adamc@467
|
223 | (CkProj _, _) => LESS
|
adamc@467
|
224 | (_, CkProj _) => GREATER
|
adamc@467
|
225
|
adamc@467
|
226 | (CkApp (f1, x1), CkApp (f2, x2)) =>
|
adamc@674
|
227 join (compare' (f1, f2),
|
adamc@674
|
228 fn () => compare' (x1, x2))
|
adamc@674
|
229 fun compare ((k1, n1), (k2, n2)) =
|
adamc@674
|
230 join (Int.compare (n1, n2),
|
adamc@674
|
231 fn () => compare' (k1, k2))
|
adamc@211
|
232 end
|
adamc@211
|
233
|
adamc@211
|
234 structure KM = BinaryMapFn(KK)
|
adamc@211
|
235
|
adamc@674
|
236 type class = ((class_name * class_key) list * exp) KM.map
|
adamc@674
|
237 val empty_class = KM.empty
|
adamc@211
|
238
|
adamc@419
|
239 fun printClasses cs = (print "Classes:\n";
|
adamc@674
|
240 CM.appi (fn (cn, km) =>
|
adamc@419
|
241 (print (cn2s cn ^ ":");
|
adamc@674
|
242 KM.appi (fn (ck, _) => print (" " ^ ckn2s ck)) km;
|
adamc@419
|
243 print "\n")) cs)
|
adamc@216
|
244
|
adamc@2
|
245 type env = {
|
adamc@623
|
246 renameK : int SM.map,
|
adamc@623
|
247 relK : string list,
|
adamc@623
|
248
|
adamc@9
|
249 renameC : kind var' SM.map,
|
adamc@2
|
250 relC : (string * kind) list,
|
adamc@11
|
251 namedC : (string * kind * con option) IM.map,
|
adamc@9
|
252
|
adamc@157
|
253 datatypes : datatyp IM.map,
|
adamc@191
|
254 constructors : (datatype_kind * int * string list * con option * int) SM.map,
|
adamc@157
|
255
|
adamc@211
|
256 classes : class CM.map,
|
adamc@211
|
257
|
adamc@9
|
258 renameE : con var' SM.map,
|
adamc@9
|
259 relE : (string * con) list,
|
adamc@31
|
260 namedE : (string * con) IM.map,
|
adamc@31
|
261
|
adamc@31
|
262 renameSgn : (int * sgn) SM.map,
|
adamc@31
|
263 sgn : (string * sgn) IM.map,
|
adamc@31
|
264
|
adamc@31
|
265 renameStr : (int * sgn) SM.map,
|
adamc@31
|
266 str : (string * sgn) IM.map
|
adamc@2
|
267 }
|
adamc@2
|
268
|
adamc@2
|
269 val namedCounter = ref 0
|
adamc@2
|
270
|
adamc@109
|
271 fun newNamed () =
|
adamc@109
|
272 let
|
adamc@109
|
273 val r = !namedCounter
|
adamc@109
|
274 in
|
adamc@109
|
275 namedCounter := r + 1;
|
adamc@109
|
276 r
|
adamc@109
|
277 end
|
adamc@109
|
278
|
adamc@2
|
279 val empty = {
|
adamc@623
|
280 renameK = SM.empty,
|
adamc@623
|
281 relK = [],
|
adamc@623
|
282
|
adamc@2
|
283 renameC = SM.empty,
|
adamc@2
|
284 relC = [],
|
adamc@9
|
285 namedC = IM.empty,
|
adamc@9
|
286
|
adamc@157
|
287 datatypes = IM.empty,
|
adamc@171
|
288 constructors = SM.empty,
|
adamc@157
|
289
|
adamc@211
|
290 classes = CM.empty,
|
adamc@211
|
291
|
adamc@9
|
292 renameE = SM.empty,
|
adamc@9
|
293 relE = [],
|
adamc@31
|
294 namedE = IM.empty,
|
adamc@31
|
295
|
adamc@31
|
296 renameSgn = SM.empty,
|
adamc@31
|
297 sgn = IM.empty,
|
adamc@31
|
298
|
adamc@31
|
299 renameStr = SM.empty,
|
adamc@31
|
300 str = IM.empty
|
adamc@2
|
301 }
|
adamc@2
|
302
|
adamc@674
|
303 fun liftClassKey' ck =
|
adamc@211
|
304 case ck of
|
adamc@211
|
305 CkNamed _ => ck
|
adamc@211
|
306 | CkRel n => CkRel (n + 1)
|
adamc@211
|
307 | CkProj _ => ck
|
adamc@674
|
308 | CkApp (ck1, ck2) => CkApp (liftClassKey' ck1, liftClassKey' ck2)
|
adamc@674
|
309
|
adamc@674
|
310 fun liftClassKey (ck, n) = (liftClassKey' ck, n)
|
adamc@211
|
311
|
adamc@623
|
312 fun pushKRel (env : env) x =
|
adamc@623
|
313 let
|
adamc@623
|
314 val renameK = SM.map (fn n => n+1) (#renameK env)
|
adamc@623
|
315 in
|
adamc@623
|
316 {renameK = SM.insert (renameK, x, 0),
|
adamc@623
|
317 relK = x :: #relK env,
|
adamc@623
|
318
|
adamc@623
|
319 renameC = SM.map (fn Rel' (n, k) => Rel' (n, liftKindInKind 0 k)
|
adamc@623
|
320 | x => x) (#renameC env),
|
adamc@623
|
321 relC = map (fn (x, k) => (x, liftKindInKind 0 k)) (#relC env),
|
adamc@623
|
322 namedC = #namedC env,
|
adamc@623
|
323
|
adamc@623
|
324 datatypes = #datatypes env,
|
adamc@623
|
325 constructors = #constructors env,
|
adamc@623
|
326
|
adamc@623
|
327 classes = #classes env,
|
adamc@623
|
328
|
adamc@623
|
329 renameE = SM.map (fn Rel' (n, c) => Rel' (n, liftKindInCon 0 c)
|
adamc@623
|
330 | Named' (n, c) => Named' (n, c)) (#renameE env),
|
adamc@623
|
331 relE = map (fn (x, c) => (x, liftKindInCon 0 c)) (#relE env),
|
adamc@623
|
332 namedE = #namedE env,
|
adamc@623
|
333
|
adamc@623
|
334 renameSgn = #renameSgn env,
|
adamc@623
|
335 sgn = #sgn env,
|
adamc@623
|
336
|
adamc@623
|
337 renameStr = #renameStr env,
|
adamc@623
|
338 str = #str env
|
adamc@623
|
339 }
|
adamc@623
|
340 end
|
adamc@623
|
341
|
adamc@623
|
342 fun lookupKRel (env : env) n =
|
adamc@623
|
343 (List.nth (#relK env, n))
|
adamc@623
|
344 handle Subscript => raise UnboundRel n
|
adamc@623
|
345
|
adamc@623
|
346 fun lookupK (env : env) x = SM.find (#renameK env, x)
|
adamc@623
|
347
|
adamc@2
|
348 fun pushCRel (env : env) x k =
|
adamc@2
|
349 let
|
adamc@9
|
350 val renameC = SM.map (fn Rel' (n, k) => Rel' (n+1, k)
|
adamc@2
|
351 | x => x) (#renameC env)
|
adamc@2
|
352 in
|
adamc@623
|
353 {renameK = #renameK env,
|
adamc@623
|
354 relK = #relK env,
|
adamc@623
|
355
|
adamc@623
|
356 renameC = SM.insert (renameC, x, Rel' (0, k)),
|
adamc@2
|
357 relC = (x, k) :: #relC env,
|
adamc@514
|
358 namedC = #namedC env,
|
adamc@9
|
359
|
adamc@157
|
360 datatypes = #datatypes env,
|
adamc@171
|
361 constructors = #constructors env,
|
adamc@157
|
362
|
adamc@674
|
363 classes = CM.map (fn class =>
|
adamc@674
|
364 KM.foldli (fn (ck, e, km) =>
|
adamc@674
|
365 KM.insert (km, liftClassKey ck, e))
|
adamc@674
|
366 KM.empty class)
|
adamc@211
|
367 (#classes env),
|
adamc@211
|
368
|
adamc@328
|
369 renameE = SM.map (fn Rel' (n, c) => Rel' (n, lift c)
|
adamc@517
|
370 | Named' (n, c) => Named' (n, c)) (#renameE env),
|
adamc@13
|
371 relE = map (fn (x, c) => (x, lift c)) (#relE env),
|
adamc@514
|
372 namedE = #namedE env,
|
adamc@31
|
373
|
adamc@31
|
374 renameSgn = #renameSgn env,
|
adamc@31
|
375 sgn = #sgn env,
|
adamc@31
|
376
|
adamc@31
|
377 renameStr = #renameStr env,
|
adamc@31
|
378 str = #str env
|
adamc@31
|
379 }
|
adamc@2
|
380 end
|
adamc@2
|
381
|
adamc@2
|
382 fun lookupCRel (env : env) n =
|
adamc@2
|
383 (List.nth (#relC env, n))
|
adamc@2
|
384 handle Subscript => raise UnboundRel n
|
adamc@2
|
385
|
adamc@11
|
386 fun pushCNamedAs (env : env) x n k co =
|
adamc@623
|
387 {renameK = #renameK env,
|
adamc@623
|
388 relK = #relK env,
|
adamc@623
|
389
|
adamc@623
|
390 renameC = SM.insert (#renameC env, x, Named' (n, k)),
|
adamc@5
|
391 relC = #relC env,
|
adamc@11
|
392 namedC = IM.insert (#namedC env, n, (x, k, co)),
|
adamc@9
|
393
|
adamc@157
|
394 datatypes = #datatypes env,
|
adamc@171
|
395 constructors = #constructors env,
|
adamc@157
|
396
|
adamc@211
|
397 classes = #classes env,
|
adamc@211
|
398
|
adamc@9
|
399 renameE = #renameE env,
|
adamc@9
|
400 relE = #relE env,
|
adamc@31
|
401 namedE = #namedE env,
|
adamc@31
|
402
|
adamc@31
|
403 renameSgn = #renameSgn env,
|
adamc@31
|
404 sgn = #sgn env,
|
adamc@31
|
405
|
adamc@31
|
406 renameStr = #renameStr env,
|
adamc@31
|
407 str = #str env}
|
adamc@5
|
408
|
adamc@11
|
409 fun pushCNamed env x k co =
|
adamc@2
|
410 let
|
adamc@2
|
411 val n = !namedCounter
|
adamc@2
|
412 in
|
adamc@2
|
413 namedCounter := n + 1;
|
adamc@11
|
414 (pushCNamedAs env x n k co, n)
|
adamc@2
|
415 end
|
adamc@2
|
416
|
adamc@2
|
417 fun lookupCNamed (env : env) n =
|
adamc@2
|
418 case IM.find (#namedC env, n) of
|
adamc@2
|
419 NONE => raise UnboundNamed n
|
adamc@2
|
420 | SOME x => x
|
adamc@2
|
421
|
adamc@2
|
422 fun lookupC (env : env) x =
|
adamc@2
|
423 case SM.find (#renameC env, x) of
|
adamc@9
|
424 NONE => NotBound
|
adamc@9
|
425 | SOME (Rel' x) => Rel x
|
adamc@9
|
426 | SOME (Named' x) => Named x
|
adamc@9
|
427
|
adamc@191
|
428 fun pushDatatype (env : env) n xs xncs =
|
adamc@188
|
429 let
|
adamc@188
|
430 val dk = U.classifyDatatype xncs
|
adamc@188
|
431 in
|
adamc@623
|
432 {renameK = #renameK env,
|
adamc@623
|
433 relK = #relK env,
|
adamc@623
|
434
|
adamc@623
|
435 renameC = #renameC env,
|
adamc@188
|
436 relC = #relC env,
|
adamc@188
|
437 namedC = #namedC env,
|
adamc@157
|
438
|
adamc@188
|
439 datatypes = IM.insert (#datatypes env, n,
|
adamc@191
|
440 (xs, foldl (fn ((x, n, to), cons) =>
|
adamc@191
|
441 IM.insert (cons, n, (x, to))) IM.empty xncs)),
|
adamc@188
|
442 constructors = foldl (fn ((x, n', to), cmap) =>
|
adamc@191
|
443 SM.insert (cmap, x, (dk, n', xs, to, n)))
|
adamc@188
|
444 (#constructors env) xncs,
|
adamc@157
|
445
|
adamc@211
|
446 classes = #classes env,
|
adamc@211
|
447
|
adamc@188
|
448 renameE = #renameE env,
|
adamc@188
|
449 relE = #relE env,
|
adamc@188
|
450 namedE = #namedE env,
|
adamc@157
|
451
|
adamc@188
|
452 renameSgn = #renameSgn env,
|
adamc@188
|
453 sgn = #sgn env,
|
adamc@157
|
454
|
adamc@188
|
455 renameStr = #renameStr env,
|
adamc@188
|
456 str = #str env}
|
adamc@188
|
457 end
|
adamc@157
|
458
|
adamc@157
|
459 fun lookupDatatype (env : env) n =
|
adamc@157
|
460 case IM.find (#datatypes env, n) of
|
adamc@157
|
461 NONE => raise UnboundNamed n
|
adamc@157
|
462 | SOME x => x
|
adamc@157
|
463
|
adamc@191
|
464 fun lookupDatatypeConstructor (_, dt) n =
|
adamc@157
|
465 case IM.find (dt, n) of
|
adamc@157
|
466 NONE => raise UnboundNamed n
|
adamc@157
|
467 | SOME x => x
|
adamc@157
|
468
|
adamc@171
|
469 fun lookupConstructor (env : env) s = SM.find (#constructors env, s)
|
adamc@171
|
470
|
adamc@191
|
471 fun datatypeArgs (xs, _) = xs
|
adamc@191
|
472 fun constructors (_, dt) = IM.foldri (fn (n, (x, to), ls) => (x, n, to) :: ls) [] dt
|
adamc@157
|
473
|
adamc@211
|
474 fun pushClass (env : env) n =
|
adamc@623
|
475 {renameK = #renameK env,
|
adamc@623
|
476 relK = #relK env,
|
adamc@623
|
477
|
adamc@623
|
478 renameC = #renameC env,
|
adamc@211
|
479 relC = #relC env,
|
adamc@211
|
480 namedC = #namedC env,
|
adamc@211
|
481
|
adamc@211
|
482 datatypes = #datatypes env,
|
adamc@211
|
483 constructors = #constructors env,
|
adamc@211
|
484
|
adamc@674
|
485 classes = CM.insert (#classes env, ClNamed n, KM.empty),
|
adamc@211
|
486
|
adamc@211
|
487 renameE = #renameE env,
|
adamc@211
|
488 relE = #relE env,
|
adamc@211
|
489 namedE = #namedE env,
|
adamc@211
|
490
|
adamc@211
|
491 renameSgn = #renameSgn env,
|
adamc@211
|
492 sgn = #sgn env,
|
adamc@211
|
493
|
adamc@211
|
494 renameStr = #renameStr env,
|
adamc@403
|
495 str = #str env}
|
adamc@211
|
496
|
adamc@211
|
497 fun class_name_in (c, _) =
|
adamc@211
|
498 case c of
|
adamc@211
|
499 CNamed n => SOME (ClNamed n)
|
adamc@211
|
500 | CModProj x => SOME (ClProj x)
|
adamc@228
|
501 | CUnif (_, _, _, ref (SOME c)) => class_name_in c
|
adamc@211
|
502 | _ => NONE
|
adamc@211
|
503
|
adamc@403
|
504 fun isClass (env : env) c =
|
adamc@403
|
505 let
|
adamc@403
|
506 fun find NONE = false
|
adamc@403
|
507 | find (SOME c) = Option.isSome (CM.find (#classes env, c))
|
adamc@403
|
508 in
|
adamc@403
|
509 find (class_name_in c)
|
adamc@403
|
510 end
|
adamc@403
|
511
|
adamc@211
|
512 fun class_key_in (c, _) =
|
adamc@211
|
513 case c of
|
adamc@211
|
514 CRel n => SOME (CkRel n)
|
adamc@211
|
515 | CNamed n => SOME (CkNamed n)
|
adamc@211
|
516 | CModProj x => SOME (CkProj x)
|
adamc@228
|
517 | CUnif (_, _, _, ref (SOME c)) => class_key_in c
|
adamc@467
|
518 | CApp (c1, c2) =>
|
adamc@467
|
519 (case (class_key_in c1, class_key_in c2) of
|
adamc@467
|
520 (SOME k1, SOME k2) => SOME (CkApp (k1, k2))
|
adamc@467
|
521 | _ => NONE)
|
adamc@211
|
522 | _ => NONE
|
adamc@211
|
523
|
adamc@674
|
524 fun class_key_out loc =
|
adamc@674
|
525 let
|
adamc@674
|
526 fun cko k =
|
adamc@674
|
527 case k of
|
adamc@674
|
528 CkRel n => (CRel n, loc)
|
adamc@674
|
529 | CkNamed n => (CNamed n, loc)
|
adamc@674
|
530 | CkProj x => (CModProj x, loc)
|
adamc@674
|
531 | CkApp (k1, k2) => (CApp (cko k1, cko k2), loc)
|
adamc@674
|
532 in
|
adamc@674
|
533 cko
|
adamc@674
|
534 end
|
adamc@674
|
535
|
adamc@211
|
536 fun class_pair_in (c, _) =
|
adamc@211
|
537 case c of
|
adamc@211
|
538 CApp (f, x) =>
|
adamc@211
|
539 (case (class_name_in f, class_key_in x) of
|
adamc@211
|
540 (SOME f, SOME x) => SOME (f, x)
|
adamc@211
|
541 | _ => NONE)
|
adamc@452
|
542 | CUnif (_, _, _, ref (SOME c)) => class_pair_in c
|
adamc@211
|
543 | _ => NONE
|
adamc@211
|
544
|
adamc@674
|
545 fun sub_class_key (n, c) =
|
adamc@674
|
546 let
|
adamc@674
|
547 fun csk k =
|
adamc@674
|
548 case k of
|
adamc@674
|
549 CkRel n' => if n' = n then
|
adamc@674
|
550 c
|
adamc@674
|
551 else
|
adamc@674
|
552 k
|
adamc@674
|
553 | CkNamed _ => k
|
adamc@674
|
554 | CkProj _ => k
|
adamc@674
|
555 | CkApp (k1, k2) => CkApp (csk k1, csk k2)
|
adamc@674
|
556 in
|
adamc@674
|
557 csk
|
adamc@674
|
558 end
|
adamc@674
|
559
|
adamc@211
|
560 fun resolveClass (env : env) c =
|
adamc@674
|
561 let
|
adamc@674
|
562 fun doPair (f, x) =
|
adamc@674
|
563 case CM.find (#classes env, f) of
|
adamc@674
|
564 NONE => NONE
|
adamc@674
|
565 | SOME class =>
|
adamc@674
|
566 let
|
adamc@674
|
567 val loc = #2 c
|
adamc@674
|
568
|
adamc@674
|
569 fun tryRules (k, args) =
|
adamc@674
|
570 let
|
adamc@674
|
571 val len = length args
|
adamc@674
|
572 in
|
adamc@674
|
573 case KM.find (class, (k, length args)) of
|
adamc@674
|
574 SOME (cs, e) =>
|
adamc@674
|
575 let
|
adamc@674
|
576 val es = map (fn (cn, ck) =>
|
adamc@674
|
577 let
|
adamc@674
|
578 val ck = ListUtil.foldli (fn (i, arg, ck) =>
|
adamc@674
|
579 sub_class_key (len - i - 1,
|
adamc@674
|
580 arg)
|
adamc@674
|
581 ck)
|
adamc@674
|
582 ck args
|
adamc@674
|
583 in
|
adamc@674
|
584 doPair (cn, ck)
|
adamc@674
|
585 end) cs
|
adamc@674
|
586 in
|
adamc@674
|
587 if List.exists (not o Option.isSome) es then
|
adamc@674
|
588 NONE
|
adamc@674
|
589 else
|
adamc@674
|
590 let
|
adamc@674
|
591 val e = foldl (fn (arg, e) => (ECApp (e, class_key_out loc arg), loc))
|
adamc@674
|
592 e args
|
adamc@674
|
593 val e = foldr (fn (pf, e) => (EApp (e, pf), loc))
|
adamc@674
|
594 e (List.mapPartial (fn x => x) es)
|
adamc@674
|
595 in
|
adamc@674
|
596 SOME e
|
adamc@674
|
597 end
|
adamc@674
|
598 end
|
adamc@674
|
599 | NONE =>
|
adamc@674
|
600 case k of
|
adamc@674
|
601 CkApp (k1, k2) => tryRules (k1, k2 :: args)
|
adamc@674
|
602 | _ => NONE
|
adamc@674
|
603 end
|
adamc@674
|
604 in
|
adamc@674
|
605 tryRules (x, [])
|
adamc@674
|
606 end
|
adamc@674
|
607 in
|
adamc@674
|
608 case class_pair_in c of
|
adamc@674
|
609 SOME p => doPair p
|
adamc@674
|
610 | _ => NONE
|
adamc@674
|
611 end
|
adamc@211
|
612
|
adamc@9
|
613 fun pushERel (env : env) x t =
|
adamc@9
|
614 let
|
adamc@9
|
615 val renameE = SM.map (fn Rel' (n, t) => Rel' (n+1, t)
|
adamc@9
|
616 | x => x) (#renameE env)
|
adamc@211
|
617
|
adamc@674
|
618 val classes = CM.map (KM.map (fn (ps, e) => (ps, liftExp e))) (#classes env)
|
adamc@211
|
619 val classes = case class_pair_in t of
|
adamc@211
|
620 NONE => classes
|
adamc@211
|
621 | SOME (f, x) =>
|
adamc@403
|
622 case CM.find (classes, f) of
|
adamc@403
|
623 NONE => classes
|
adamc@403
|
624 | SOME class =>
|
adamc@403
|
625 let
|
adamc@674
|
626 val class = KM.insert (class, (x, 0), ([], (ERel 0, #2 t)))
|
adamc@403
|
627 in
|
adamc@403
|
628 CM.insert (classes, f, class)
|
adamc@403
|
629 end
|
adamc@9
|
630 in
|
adamc@623
|
631 {renameK = #renameK env,
|
adamc@623
|
632 relK = #relK env,
|
adamc@623
|
633
|
adamc@623
|
634 renameC = #renameC env,
|
adamc@9
|
635 relC = #relC env,
|
adamc@9
|
636 namedC = #namedC env,
|
adamc@9
|
637
|
adamc@157
|
638 datatypes = #datatypes env,
|
adamc@171
|
639 constructors = #constructors env,
|
adamc@157
|
640
|
adamc@211
|
641 classes = classes,
|
adamc@211
|
642
|
adamc@9
|
643 renameE = SM.insert (renameE, x, Rel' (0, t)),
|
adamc@9
|
644 relE = (x, t) :: #relE env,
|
adamc@31
|
645 namedE = #namedE env,
|
adamc@31
|
646
|
adamc@31
|
647 renameSgn = #renameSgn env,
|
adamc@31
|
648 sgn = #sgn env,
|
adamc@31
|
649
|
adamc@31
|
650 renameStr = #renameStr env,
|
adamc@31
|
651 str = #str env}
|
adamc@9
|
652 end
|
adamc@9
|
653
|
adamc@9
|
654 fun lookupERel (env : env) n =
|
adamc@9
|
655 (List.nth (#relE env, n))
|
adamc@9
|
656 handle Subscript => raise UnboundRel n
|
adamc@9
|
657
|
adamc@674
|
658 fun rule_in c =
|
adamc@674
|
659 let
|
adamc@674
|
660 fun quantifiers (c, nvars) =
|
adamc@674
|
661 case #1 c of
|
adamc@674
|
662 TCFun (_, _, _, c) => quantifiers (c, nvars + 1)
|
adamc@674
|
663 | _ =>
|
adamc@674
|
664 let
|
adamc@674
|
665 fun clauses (c, hyps) =
|
adamc@674
|
666 case #1 c of
|
adamc@674
|
667 TFun (hyp, c) =>
|
adamc@674
|
668 (case class_pair_in hyp of
|
adamc@674
|
669 NONE => NONE
|
adamc@674
|
670 | SOME p => clauses (c, p :: hyps))
|
adamc@674
|
671 | _ =>
|
adamc@674
|
672 case class_pair_in c of
|
adamc@674
|
673 NONE => NONE
|
adamc@674
|
674 | SOME (cn, ck) =>
|
adamc@674
|
675 let
|
adamc@674
|
676 fun dearg (ck, i) =
|
adamc@674
|
677 if i >= nvars then
|
adamc@674
|
678 SOME (nvars, hyps, (cn, ck))
|
adamc@674
|
679 else case ck of
|
adamc@674
|
680 CkApp (ck, CkRel i') =>
|
adamc@674
|
681 if i' = i then
|
adamc@674
|
682 dearg (ck, i + 1)
|
adamc@674
|
683 else
|
adamc@674
|
684 NONE
|
adamc@674
|
685 | _ => NONE
|
adamc@674
|
686 in
|
adamc@674
|
687 dearg (ck, 0)
|
adamc@674
|
688 end
|
adamc@674
|
689 in
|
adamc@674
|
690 clauses (c, [])
|
adamc@674
|
691 end
|
adamc@674
|
692 in
|
adamc@674
|
693 quantifiers (c, 0)
|
adamc@674
|
694 end
|
adamc@674
|
695
|
adamc@9
|
696 fun pushENamedAs (env : env) x n t =
|
adamc@211
|
697 let
|
adamc@211
|
698 val classes = #classes env
|
adamc@674
|
699 val classes = case rule_in t of
|
adamc@211
|
700 NONE => classes
|
adamc@674
|
701 | SOME (nvars, hyps, (f, x)) =>
|
adamc@403
|
702 case CM.find (classes, f) of
|
adamc@403
|
703 NONE => classes
|
adamc@403
|
704 | SOME class =>
|
adamc@403
|
705 let
|
adamc@674
|
706 val class = KM.insert (class, (x, nvars), (hyps, (ENamed n, #2 t)))
|
adamc@403
|
707 in
|
adamc@403
|
708 CM.insert (classes, f, class)
|
adamc@403
|
709 end
|
adamc@211
|
710 in
|
adamc@623
|
711 {renameK = #renameK env,
|
adamc@623
|
712 relK = #relK env,
|
adamc@623
|
713
|
adamc@623
|
714 renameC = #renameC env,
|
adamc@211
|
715 relC = #relC env,
|
adamc@211
|
716 namedC = #namedC env,
|
adamc@9
|
717
|
adamc@211
|
718 datatypes = #datatypes env,
|
adamc@211
|
719 constructors = #constructors env,
|
adamc@157
|
720
|
adamc@211
|
721 classes = classes,
|
adamc@31
|
722
|
adamc@211
|
723 renameE = SM.insert (#renameE env, x, Named' (n, t)),
|
adamc@211
|
724 relE = #relE env,
|
adamc@211
|
725 namedE = IM.insert (#namedE env, n, (x, t)),
|
adamc@211
|
726
|
adamc@211
|
727 renameSgn = #renameSgn env,
|
adamc@211
|
728 sgn = #sgn env,
|
adamc@211
|
729
|
adamc@211
|
730 renameStr = #renameStr env,
|
adamc@211
|
731 str = #str env}
|
adamc@211
|
732 end
|
adamc@9
|
733
|
adamc@9
|
734 fun pushENamed env x t =
|
adamc@9
|
735 let
|
adamc@9
|
736 val n = !namedCounter
|
adamc@9
|
737 in
|
adamc@9
|
738 namedCounter := n + 1;
|
adamc@9
|
739 (pushENamedAs env x n t, n)
|
adamc@9
|
740 end
|
adamc@9
|
741
|
adamc@9
|
742 fun lookupENamed (env : env) n =
|
adamc@9
|
743 case IM.find (#namedE env, n) of
|
adamc@9
|
744 NONE => raise UnboundNamed n
|
adamc@9
|
745 | SOME x => x
|
adamc@9
|
746
|
adamc@471
|
747 fun checkENamed (env : env) n =
|
adamc@471
|
748 Option.isSome (IM.find (#namedE env, n))
|
adamc@471
|
749
|
adamc@9
|
750 fun lookupE (env : env) x =
|
adamc@9
|
751 case SM.find (#renameE env, x) of
|
adamc@9
|
752 NONE => NotBound
|
adamc@9
|
753 | SOME (Rel' x) => Rel x
|
adamc@9
|
754 | SOME (Named' x) => Named x
|
adamc@2
|
755
|
adamc@31
|
756 fun pushSgnNamedAs (env : env) x n sgis =
|
adamc@623
|
757 {renameK = #renameK env,
|
adamc@623
|
758 relK = #relK env,
|
adamc@623
|
759
|
adamc@623
|
760 renameC = #renameC env,
|
adamc@31
|
761 relC = #relC env,
|
adamc@31
|
762 namedC = #namedC env,
|
adamc@31
|
763
|
adamc@157
|
764 datatypes = #datatypes env,
|
adamc@171
|
765 constructors = #constructors env,
|
adamc@157
|
766
|
adamc@211
|
767 classes = #classes env,
|
adamc@211
|
768
|
adamc@31
|
769 renameE = #renameE env,
|
adamc@31
|
770 relE = #relE env,
|
adamc@31
|
771 namedE = #namedE env,
|
adamc@31
|
772
|
adamc@31
|
773 renameSgn = SM.insert (#renameSgn env, x, (n, sgis)),
|
adamc@31
|
774 sgn = IM.insert (#sgn env, n, (x, sgis)),
|
adamc@31
|
775
|
adamc@31
|
776 renameStr = #renameStr env,
|
adamc@31
|
777 str = #str env}
|
adamc@31
|
778
|
adamc@31
|
779 fun pushSgnNamed env x sgis =
|
adamc@31
|
780 let
|
adamc@31
|
781 val n = !namedCounter
|
adamc@31
|
782 in
|
adamc@31
|
783 namedCounter := n + 1;
|
adamc@31
|
784 (pushSgnNamedAs env x n sgis, n)
|
adamc@31
|
785 end
|
adamc@31
|
786
|
adamc@31
|
787 fun lookupSgnNamed (env : env) n =
|
adamc@31
|
788 case IM.find (#sgn env, n) of
|
adamc@31
|
789 NONE => raise UnboundNamed n
|
adamc@31
|
790 | SOME x => x
|
adamc@31
|
791
|
adamc@31
|
792 fun lookupSgn (env : env) x = SM.find (#renameSgn env, x)
|
adamc@31
|
793
|
adamc@31
|
794 fun lookupStrNamed (env : env) n =
|
adamc@31
|
795 case IM.find (#str env, n) of
|
adamc@31
|
796 NONE => raise UnboundNamed n
|
adamc@31
|
797 | SOME x => x
|
adamc@31
|
798
|
adamc@31
|
799 fun lookupStr (env : env) x = SM.find (#renameStr env, x)
|
adamc@31
|
800
|
adamc@203
|
801
|
adamc@216
|
802 fun sgiSeek (sgi, (sgns, strs, cons)) =
|
adamc@216
|
803 case sgi of
|
adamc@216
|
804 SgiConAbs (x, n, _) => (sgns, strs, IM.insert (cons, n, x))
|
adamc@216
|
805 | SgiCon (x, n, _, _) => (sgns, strs, IM.insert (cons, n, x))
|
adamc@216
|
806 | SgiDatatype (x, n, _, _) => (sgns, strs, IM.insert (cons, n, x))
|
adamc@216
|
807 | SgiDatatypeImp (x, n, _, _, _, _, _) => (sgns, strs, IM.insert (cons, n, x))
|
adamc@216
|
808 | SgiVal _ => (sgns, strs, cons)
|
adamc@216
|
809 | SgiSgn (x, n, _) => (IM.insert (sgns, n, x), strs, cons)
|
adamc@216
|
810 | SgiStr (x, n, _) => (sgns, IM.insert (strs, n, x), cons)
|
adamc@216
|
811 | SgiConstraint _ => (sgns, strs, cons)
|
adamc@563
|
812 | SgiClassAbs (x, n, _) => (sgns, strs, IM.insert (cons, n, x))
|
adamc@563
|
813 | SgiClass (x, n, _, _) => (sgns, strs, IM.insert (cons, n, x))
|
adamc@216
|
814
|
adamc@34
|
815 fun sgnSeek f sgis =
|
adamc@34
|
816 let
|
adamc@59
|
817 fun seek (sgis, sgns, strs, cons) =
|
adamc@34
|
818 case sgis of
|
adamc@34
|
819 [] => NONE
|
adamc@34
|
820 | (sgi, _) :: sgis =>
|
adamc@34
|
821 case f sgi of
|
adamc@158
|
822 SOME v =>
|
adamc@158
|
823 let
|
adamc@158
|
824 val cons =
|
adamc@158
|
825 case sgi of
|
adamc@191
|
826 SgiDatatype (x, n, _, _) => IM.insert (cons, n, x)
|
adamc@191
|
827 | SgiDatatypeImp (x, n, _, _, _, _, _) => IM.insert (cons, n, x)
|
adamc@158
|
828 | _ => cons
|
adamc@158
|
829 in
|
adamc@158
|
830 SOME (v, (sgns, strs, cons))
|
adamc@158
|
831 end
|
adamc@88
|
832 | NONE =>
|
adamc@216
|
833 let
|
adamc@216
|
834 val (sgns, strs, cons) = sgiSeek (sgi, (sgns, strs, cons))
|
adamc@216
|
835 in
|
adamc@216
|
836 seek (sgis, sgns, strs, cons)
|
adamc@216
|
837 end
|
adamc@34
|
838 in
|
adamc@59
|
839 seek (sgis, IM.empty, IM.empty, IM.empty)
|
adamc@34
|
840 end
|
adamc@34
|
841
|
adamc@34
|
842 fun id x = x
|
adamc@34
|
843
|
adamc@34
|
844 fun unravelStr (str, _) =
|
adamc@34
|
845 case str of
|
adamc@34
|
846 StrVar x => (x, [])
|
adamc@34
|
847 | StrProj (str, m) =>
|
adamc@34
|
848 let
|
adamc@34
|
849 val (x, ms) = unravelStr str
|
adamc@34
|
850 in
|
adamc@34
|
851 (x, ms @ [m])
|
adamc@34
|
852 end
|
adamc@34
|
853 | _ => raise Fail "unravelStr"
|
adamc@34
|
854
|
adamc@59
|
855 fun sgnS_con (str, (sgns, strs, cons)) c =
|
adamc@34
|
856 case c of
|
adamc@34
|
857 CModProj (m1, ms, x) =>
|
adamc@34
|
858 (case IM.find (strs, m1) of
|
adamc@34
|
859 NONE => c
|
adamc@34
|
860 | SOME m1x =>
|
adamc@34
|
861 let
|
adamc@34
|
862 val (m1, ms') = unravelStr str
|
adamc@34
|
863 in
|
adamc@34
|
864 CModProj (m1, ms' @ m1x :: ms, x)
|
adamc@34
|
865 end)
|
adamc@34
|
866 | CNamed n =>
|
adamc@34
|
867 (case IM.find (cons, n) of
|
adamc@34
|
868 NONE => c
|
adamc@34
|
869 | SOME nx =>
|
adamc@34
|
870 let
|
adamc@34
|
871 val (m1, ms) = unravelStr str
|
adamc@34
|
872 in
|
adamc@34
|
873 CModProj (m1, ms, nx)
|
adamc@34
|
874 end)
|
adamc@34
|
875 | _ => c
|
adamc@34
|
876
|
adamc@467
|
877 fun sgnS_con' (arg as (m1, ms', (sgns, strs, cons))) c =
|
adamc@216
|
878 case c of
|
adamc@216
|
879 CModProj (m1, ms, x) =>
|
adamc@216
|
880 (case IM.find (strs, m1) of
|
adamc@216
|
881 NONE => c
|
adamc@216
|
882 | SOME m1x => CModProj (m1, ms' @ m1x :: ms, x))
|
adamc@216
|
883 | CNamed n =>
|
adamc@216
|
884 (case IM.find (cons, n) of
|
adamc@216
|
885 NONE => c
|
adamc@216
|
886 | SOME nx => CModProj (m1, ms', nx))
|
adamc@467
|
887 | CApp (c1, c2) => CApp ((sgnS_con' arg (#1 c1), #2 c1),
|
adamc@467
|
888 (sgnS_con' arg (#1 c2), #2 c2))
|
adamc@216
|
889 | _ => c
|
adamc@216
|
890
|
adamc@674
|
891 fun sgnS_class_name (arg as (m1, ms', (sgns, strs, cons))) nm =
|
adamc@674
|
892 case nm of
|
adamc@674
|
893 ClProj (m1, ms, x) =>
|
adamc@674
|
894 (case IM.find (strs, m1) of
|
adamc@674
|
895 NONE => nm
|
adamc@674
|
896 | SOME m1x => ClProj (m1, ms' @ m1x :: ms, x))
|
adamc@674
|
897 | ClNamed n =>
|
adamc@674
|
898 (case IM.find (cons, n) of
|
adamc@674
|
899 NONE => nm
|
adamc@674
|
900 | SOME nx => ClProj (m1, ms', nx))
|
adamc@674
|
901
|
adamc@674
|
902 fun sgnS_class_key (arg as (m1, ms', (sgns, strs, cons))) k =
|
adamc@674
|
903 case k of
|
adamc@674
|
904 CkProj (m1, ms, x) =>
|
adamc@674
|
905 (case IM.find (strs, m1) of
|
adamc@674
|
906 NONE => k
|
adamc@674
|
907 | SOME m1x => CkProj (m1, ms' @ m1x :: ms, x))
|
adamc@674
|
908 | CkNamed n =>
|
adamc@674
|
909 (case IM.find (cons, n) of
|
adamc@674
|
910 NONE => k
|
adamc@674
|
911 | SOME nx => CkProj (m1, ms', nx))
|
adamc@674
|
912 | CkApp (k1, k2) => CkApp (sgnS_class_key arg k1,
|
adamc@674
|
913 sgnS_class_key arg k2)
|
adamc@674
|
914 | _ => k
|
adamc@674
|
915
|
adamc@59
|
916 fun sgnS_sgn (str, (sgns, strs, cons)) sgn =
|
adamc@59
|
917 case sgn of
|
adamc@59
|
918 SgnProj (m1, ms, x) =>
|
adamc@59
|
919 (case IM.find (strs, m1) of
|
adamc@59
|
920 NONE => sgn
|
adamc@59
|
921 | SOME m1x =>
|
adamc@59
|
922 let
|
adamc@59
|
923 val (m1, ms') = unravelStr str
|
adamc@59
|
924 in
|
adamc@59
|
925 SgnProj (m1, ms' @ m1x :: ms, x)
|
adamc@59
|
926 end)
|
adamc@59
|
927 | SgnVar n =>
|
adamc@59
|
928 (case IM.find (sgns, n) of
|
adamc@59
|
929 NONE => sgn
|
adamc@59
|
930 | SOME nx =>
|
adamc@59
|
931 let
|
adamc@59
|
932 val (m1, ms) = unravelStr str
|
adamc@59
|
933 in
|
adamc@59
|
934 SgnProj (m1, ms, nx)
|
adamc@59
|
935 end)
|
adamc@59
|
936 | _ => sgn
|
adamc@59
|
937
|
adamc@59
|
938 fun sgnSubSgn x =
|
adamc@34
|
939 ElabUtil.Sgn.map {kind = id,
|
adamc@59
|
940 con = sgnS_con x,
|
adamc@34
|
941 sgn_item = id,
|
adamc@59
|
942 sgn = sgnS_sgn x}
|
adamc@34
|
943
|
adamc@211
|
944
|
adamc@211
|
945
|
adamc@211
|
946 and projectSgn env {sgn, str, field} =
|
adamc@211
|
947 case #1 (hnormSgn env sgn) of
|
adamc@211
|
948 SgnConst sgis =>
|
adamc@211
|
949 (case sgnSeek (fn SgiSgn (x, _, sgn) => if x = field then SOME sgn else NONE | _ => NONE) sgis of
|
adamc@211
|
950 NONE => NONE
|
adamc@211
|
951 | SOME (sgn, subs) => SOME (sgnSubSgn (str, subs) sgn))
|
adamc@211
|
952 | SgnError => SOME (SgnError, ErrorMsg.dummySpan)
|
adamc@211
|
953 | _ => NONE
|
adamc@211
|
954
|
adamc@211
|
955 and hnormSgn env (all as (sgn, loc)) =
|
adamc@34
|
956 case sgn of
|
adamc@42
|
957 SgnError => all
|
adamc@42
|
958 | SgnVar n => hnormSgn env (#2 (lookupSgnNamed env n))
|
adamc@42
|
959 | SgnConst _ => all
|
adamc@42
|
960 | SgnFun _ => all
|
adamc@59
|
961 | SgnProj (m, ms, x) =>
|
adamc@59
|
962 let
|
adamc@59
|
963 val (_, sgn) = lookupStrNamed env m
|
adamc@59
|
964 in
|
adamc@59
|
965 case projectSgn env {str = foldl (fn (m, str) => (StrProj (str, m), loc)) (StrVar m, loc) ms,
|
adamc@59
|
966 sgn = sgn,
|
adamc@59
|
967 field = x} of
|
adamc@59
|
968 NONE => raise Fail "ElabEnv.hnormSgn: projectSgn failed"
|
adamc@59
|
969 | SOME sgn => sgn
|
adamc@59
|
970 end
|
adamc@42
|
971 | SgnWhere (sgn, x, c) =>
|
adamc@42
|
972 case #1 (hnormSgn env sgn) of
|
adamc@42
|
973 SgnError => (SgnError, loc)
|
adamc@42
|
974 | SgnConst sgis =>
|
adamc@42
|
975 let
|
adamc@42
|
976 fun traverse (pre, post) =
|
adamc@42
|
977 case post of
|
adamc@42
|
978 [] => raise Fail "ElabEnv.hnormSgn: Can't reduce 'where' [1]"
|
adamc@42
|
979 | (sgi as (SgiConAbs (x', n, k), loc)) :: rest =>
|
adamc@42
|
980 if x = x' then
|
adamc@42
|
981 List.revAppend (pre, (SgiCon (x', n, k, c), loc) :: rest)
|
adamc@42
|
982 else
|
adamc@42
|
983 traverse (sgi :: pre, rest)
|
adamc@42
|
984 | sgi :: rest => traverse (sgi :: pre, rest)
|
adamc@42
|
985
|
adamc@42
|
986 val sgis = traverse ([], sgis)
|
adamc@42
|
987 in
|
adamc@42
|
988 (SgnConst sgis, loc)
|
adamc@42
|
989 end
|
adamc@42
|
990 | _ => raise Fail "ElabEnv.hnormSgn: Can't reduce 'where' [2]"
|
adamc@42
|
991
|
adamc@211
|
992 fun enrichClasses env classes (m1, ms) sgn =
|
adamc@59
|
993 case #1 (hnormSgn env sgn) of
|
adamc@59
|
994 SgnConst sgis =>
|
adamc@211
|
995 let
|
adamc@218
|
996 val (classes, _, _, _) =
|
adamc@218
|
997 foldl (fn (sgi, (classes, newClasses, fmap, env)) =>
|
adamc@211
|
998 let
|
adamc@211
|
999 fun found (x, n) =
|
adamc@211
|
1000 (CM.insert (classes,
|
adamc@211
|
1001 ClProj (m1, ms, x),
|
adamc@211
|
1002 empty_class),
|
adamc@216
|
1003 IM.insert (newClasses, n, x),
|
adamc@218
|
1004 sgiSeek (#1 sgi, fmap),
|
adamc@218
|
1005 env)
|
adamc@216
|
1006
|
adamc@218
|
1007 fun default () = (classes, newClasses, sgiSeek (#1 sgi, fmap), env)
|
adamc@211
|
1008 in
|
adamc@211
|
1009 case #1 sgi of
|
adamc@217
|
1010 SgiStr (x, _, sgn) =>
|
adamc@217
|
1011 (enrichClasses env classes (m1, ms @ [x]) sgn,
|
adamc@217
|
1012 newClasses,
|
adamc@218
|
1013 sgiSeek (#1 sgi, fmap),
|
adamc@218
|
1014 env)
|
adamc@218
|
1015 | SgiSgn (x, n, sgn) =>
|
adamc@218
|
1016 (classes,
|
adamc@218
|
1017 newClasses,
|
adamc@218
|
1018 fmap,
|
adamc@218
|
1019 pushSgnNamedAs env x n sgn)
|
adamc@218
|
1020
|
adamc@563
|
1021 | SgiClassAbs (x, n, _) => found (x, n)
|
adamc@563
|
1022 | SgiClass (x, n, _, _) => found (x, n)
|
adamc@674
|
1023 | SgiVal (x, n, c) =>
|
adamc@674
|
1024 (case rule_in c of
|
adamc@674
|
1025 NONE => default ()
|
adamc@674
|
1026 | SOME (nvars, hyps, (cn, a)) =>
|
adamc@674
|
1027 let
|
adamc@674
|
1028 val globalize = sgnS_class_key (m1, ms, fmap)
|
adamc@674
|
1029 val ck = globalize a
|
adamc@674
|
1030 val hyps = map (fn (n, k) => (sgnS_class_name (m1, ms, fmap) n,
|
adamc@674
|
1031 globalize k)) hyps
|
adamc@216
|
1032
|
adamc@674
|
1033 fun unravel c =
|
adamc@674
|
1034 case c of
|
adamc@674
|
1035 ClNamed n =>
|
adamc@674
|
1036 ((case lookupCNamed env n of
|
adamc@674
|
1037 (_, _, SOME c') =>
|
adamc@674
|
1038 (case class_name_in c' of
|
adamc@674
|
1039 NONE => c
|
adamc@674
|
1040 | SOME k => unravel k)
|
adamc@674
|
1041 | _ => c)
|
adamc@674
|
1042 handle UnboundNamed _ => c)
|
adamc@674
|
1043 | _ => c
|
adamc@674
|
1044
|
adamc@674
|
1045 val nc =
|
adamc@674
|
1046 case cn of
|
adamc@674
|
1047 ClNamed f => IM.find (newClasses, f)
|
adamc@674
|
1048 | _ => NONE
|
adamc@674
|
1049 in
|
adamc@674
|
1050 case nc of
|
adamc@674
|
1051 NONE =>
|
adamc@419
|
1052 let
|
adamc@419
|
1053 val classes =
|
adamc@419
|
1054 case CM.find (classes, cn) of
|
adamc@419
|
1055 NONE => classes
|
adamc@419
|
1056 | SOME class =>
|
adamc@419
|
1057 let
|
adamc@674
|
1058 val class = KM.insert (class, (ck, nvars),
|
adamc@674
|
1059 (hyps,
|
adamc@674
|
1060 (EModProj (m1, ms, x),
|
adamc@674
|
1061 #2 sgn)))
|
adamc@419
|
1062 in
|
adamc@419
|
1063 CM.insert (classes, cn, class)
|
adamc@419
|
1064 end
|
adamc@419
|
1065 in
|
adamc@419
|
1066 (classes,
|
adamc@419
|
1067 newClasses,
|
adamc@419
|
1068 fmap,
|
adamc@419
|
1069 env)
|
adamc@419
|
1070 end
|
adamc@674
|
1071 | SOME fx =>
|
adamc@674
|
1072 let
|
adamc@674
|
1073 val cn = ClProj (m1, ms, fx)
|
adamc@419
|
1074
|
adamc@674
|
1075 val classes =
|
adamc@674
|
1076 case CM.find (classes, cn) of
|
adamc@674
|
1077 NONE => classes
|
adamc@674
|
1078 | SOME class =>
|
adamc@674
|
1079 let
|
adamc@674
|
1080 val class = KM.insert (class, (ck, nvars),
|
adamc@674
|
1081 (hyps,
|
adamc@674
|
1082 (EModProj (m1, ms, x), #2 sgn)))
|
adamc@674
|
1083 in
|
adamc@674
|
1084 CM.insert (classes, cn, class)
|
adamc@674
|
1085 end
|
adamc@674
|
1086 in
|
adamc@674
|
1087 (classes,
|
adamc@674
|
1088 newClasses,
|
adamc@674
|
1089 fmap,
|
adamc@674
|
1090 env)
|
adamc@674
|
1091 end
|
adamc@674
|
1092 end)
|
adamc@216
|
1093 | _ => default ()
|
adamc@211
|
1094 end)
|
adamc@218
|
1095 (classes, IM.empty, (IM.empty, IM.empty, IM.empty), env) sgis
|
adamc@211
|
1096 in
|
adamc@211
|
1097 classes
|
adamc@211
|
1098 end
|
adamc@211
|
1099 | _ => classes
|
adamc@211
|
1100
|
adamc@211
|
1101 fun pushStrNamedAs (env : env) x n sgn =
|
adamc@623
|
1102 {renameK = #renameK env,
|
adamc@623
|
1103 relK = #relK env,
|
adamc@623
|
1104
|
adamc@623
|
1105 renameC = #renameC env,
|
adamc@211
|
1106 relC = #relC env,
|
adamc@211
|
1107 namedC = #namedC env,
|
adamc@211
|
1108
|
adamc@211
|
1109 datatypes = #datatypes env,
|
adamc@211
|
1110 constructors = #constructors env,
|
adamc@211
|
1111
|
adamc@211
|
1112 classes = enrichClasses env (#classes env) (n, []) sgn,
|
adamc@211
|
1113
|
adamc@211
|
1114 renameE = #renameE env,
|
adamc@211
|
1115 relE = #relE env,
|
adamc@211
|
1116 namedE = #namedE env,
|
adamc@211
|
1117
|
adamc@211
|
1118 renameSgn = #renameSgn env,
|
adamc@211
|
1119 sgn = #sgn env,
|
adamc@211
|
1120
|
adamc@211
|
1121 renameStr = SM.insert (#renameStr env, x, (n, sgn)),
|
adamc@211
|
1122 str = IM.insert (#str env, n, (x, sgn))}
|
adamc@211
|
1123
|
adamc@211
|
1124 fun pushStrNamed env x sgn =
|
adamc@211
|
1125 let
|
adamc@211
|
1126 val n = !namedCounter
|
adamc@211
|
1127 in
|
adamc@211
|
1128 namedCounter := n + 1;
|
adamc@211
|
1129 (pushStrNamedAs env x n sgn, n)
|
adamc@211
|
1130 end
|
adamc@211
|
1131
|
adamc@211
|
1132 fun sgiBinds env (sgi, loc) =
|
adamc@211
|
1133 case sgi of
|
adamc@211
|
1134 SgiConAbs (x, n, k) => pushCNamedAs env x n k NONE
|
adamc@211
|
1135 | SgiCon (x, n, k, c) => pushCNamedAs env x n k (SOME c)
|
adamc@211
|
1136 | SgiDatatype (x, n, xs, xncs) =>
|
adamc@211
|
1137 let
|
adamc@341
|
1138 val k = (KType, loc)
|
adamc@341
|
1139 val k' = foldr (fn (_, k') => (KArrow (k, k'), loc)) k xs
|
adamc@341
|
1140
|
adamc@341
|
1141 val env = pushCNamedAs env x n k' NONE
|
adamc@211
|
1142 in
|
adamc@211
|
1143 foldl (fn ((x', n', to), env) =>
|
adamc@211
|
1144 let
|
adamc@211
|
1145 val t =
|
adamc@211
|
1146 case to of
|
adamc@211
|
1147 NONE => (CNamed n, loc)
|
adamc@211
|
1148 | SOME t => (TFun (t, (CNamed n, loc)), loc)
|
adamc@211
|
1149
|
adamc@211
|
1150 val k = (KType, loc)
|
adamc@211
|
1151 val t = foldr (fn (x, t) => (TCFun (Explicit, x, k, t), loc)) t xs
|
adamc@211
|
1152 in
|
adamc@211
|
1153 pushENamedAs env x' n' t
|
adamc@211
|
1154 end)
|
adamc@211
|
1155 env xncs
|
adamc@211
|
1156 end
|
adamc@211
|
1157 | SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) =>
|
adamc@211
|
1158 let
|
adamc@341
|
1159 val k = (KType, loc)
|
adamc@341
|
1160 val k' = foldr (fn (_, k') => (KArrow (k, k'), loc)) k xs
|
adamc@341
|
1161
|
adamc@341
|
1162 val env = pushCNamedAs env x n k' (SOME (CModProj (m1, ms, x'), loc))
|
adamc@211
|
1163 in
|
adamc@211
|
1164 foldl (fn ((x', n', to), env) =>
|
adamc@211
|
1165 let
|
adamc@211
|
1166 val t =
|
adamc@211
|
1167 case to of
|
adamc@211
|
1168 NONE => (CNamed n, loc)
|
adamc@211
|
1169 | SOME t => (TFun (t, (CNamed n, loc)), loc)
|
adamc@211
|
1170
|
adamc@211
|
1171 val k = (KType, loc)
|
adamc@211
|
1172 val t = foldr (fn (x, t) => (TCFun (Explicit, x, k, t), loc)) t xs
|
adamc@211
|
1173 in
|
adamc@211
|
1174 pushENamedAs env x' n' t
|
adamc@211
|
1175 end)
|
adamc@211
|
1176 env xncs
|
adamc@211
|
1177 end
|
adamc@211
|
1178 | SgiVal (x, n, t) => pushENamedAs env x n t
|
adamc@211
|
1179 | SgiStr (x, n, sgn) => pushStrNamedAs env x n sgn
|
adamc@211
|
1180 | SgiSgn (x, n, sgn) => pushSgnNamedAs env x n sgn
|
adamc@211
|
1181 | SgiConstraint _ => env
|
adamc@211
|
1182
|
adamc@563
|
1183 | SgiClassAbs (x, n, k) => pushCNamedAs env x n (KArrow (k, (KType, loc)), loc) NONE
|
adamc@563
|
1184 | SgiClass (x, n, k, c) => pushCNamedAs env x n (KArrow (k, (KType, loc)), loc) (SOME c)
|
adamc@459
|
1185
|
adamc@211
|
1186 fun sgnSubCon x =
|
adamc@211
|
1187 ElabUtil.Con.map {kind = id,
|
adamc@211
|
1188 con = sgnS_con x}
|
adamc@59
|
1189
|
adamc@59
|
1190 fun projectStr env {sgn, str, field} =
|
adamc@59
|
1191 case #1 (hnormSgn env sgn) of
|
adamc@59
|
1192 SgnConst sgis =>
|
adamc@59
|
1193 (case sgnSeek (fn SgiStr (x, _, sgn) => if x = field then SOME sgn else NONE | _ => NONE) sgis of
|
adamc@59
|
1194 NONE => NONE
|
adamc@59
|
1195 | SOME (sgn, subs) => SOME (sgnSubSgn (str, subs) sgn))
|
adamc@59
|
1196 | SgnError => SOME (SgnError, ErrorMsg.dummySpan)
|
adamc@59
|
1197 | _ => NONE
|
adamc@59
|
1198
|
adamc@158
|
1199 fun chaseMpath env (n, ms) =
|
adamc@158
|
1200 let
|
adamc@158
|
1201 val (_, sgn) = lookupStrNamed env n
|
adamc@158
|
1202 in
|
adamc@158
|
1203 foldl (fn (m, (str, sgn)) =>
|
adamc@158
|
1204 case projectStr env {sgn = sgn, str = str, field = m} of
|
adamc@158
|
1205 NONE => raise Fail "kindof: Unknown substructure"
|
adamc@158
|
1206 | SOME sgn => ((StrProj (str, m), #2 sgn), sgn))
|
adamc@158
|
1207 ((StrVar n, #2 sgn), sgn) ms
|
adamc@158
|
1208 end
|
adamc@158
|
1209
|
adamc@42
|
1210 fun projectCon env {sgn, str, field} =
|
adamc@42
|
1211 case #1 (hnormSgn env sgn) of
|
adamc@34
|
1212 SgnConst sgis =>
|
adamc@34
|
1213 (case sgnSeek (fn SgiConAbs (x, _, k) => if x = field then SOME (k, NONE) else NONE
|
adamc@34
|
1214 | SgiCon (x, _, k, c) => if x = field then SOME (k, SOME c) else NONE
|
adamc@341
|
1215 | SgiDatatype (x, _, xs, _) =>
|
adamc@158
|
1216 if x = field then
|
adamc@341
|
1217 let
|
adamc@341
|
1218 val k = (KType, #2 sgn)
|
adamc@341
|
1219 val k' = foldl (fn (_, k') => (KArrow (k, k'), #2 sgn)) k xs
|
adamc@341
|
1220 in
|
adamc@341
|
1221 SOME (k', NONE)
|
adamc@341
|
1222 end
|
adamc@341
|
1223 else
|
adamc@341
|
1224 NONE
|
adamc@341
|
1225 | SgiDatatypeImp (x, _, m1, ms, x', xs, _) =>
|
adamc@341
|
1226 if x = field then
|
adamc@341
|
1227 let
|
adamc@341
|
1228 val k = (KType, #2 sgn)
|
adamc@341
|
1229 val k' = foldl (fn (_, k') => (KArrow (k, k'), #2 sgn)) k xs
|
adamc@341
|
1230 in
|
adamc@341
|
1231 SOME (k', SOME (CModProj (m1, ms, x'), #2 sgn))
|
adamc@341
|
1232 end
|
adamc@158
|
1233 else
|
adamc@158
|
1234 NONE
|
adamc@563
|
1235 | SgiClassAbs (x, _, k) => if x = field then
|
adamc@563
|
1236 SOME ((KArrow (k, (KType, #2 sgn)), #2 sgn), NONE)
|
adamc@563
|
1237 else
|
adamc@563
|
1238 NONE
|
adamc@563
|
1239 | SgiClass (x, _, k, c) => if x = field then
|
adamc@563
|
1240 SOME ((KArrow (k, (KType, #2 sgn)), #2 sgn), SOME c)
|
adamc@563
|
1241 else
|
adamc@563
|
1242 NONE
|
adamc@34
|
1243 | _ => NONE) sgis of
|
adamc@34
|
1244 NONE => NONE
|
adamc@34
|
1245 | SOME ((k, co), subs) => SOME (k, Option.map (sgnSubCon (str, subs)) co))
|
adamc@34
|
1246 | SgnError => SOME ((KError, ErrorMsg.dummySpan), SOME (CError, ErrorMsg.dummySpan))
|
adamc@42
|
1247 | _ => NONE
|
adamc@34
|
1248
|
adamc@157
|
1249 fun projectDatatype env {sgn, str, field} =
|
adamc@157
|
1250 case #1 (hnormSgn env sgn) of
|
adamc@157
|
1251 SgnConst sgis =>
|
adamc@191
|
1252 (case sgnSeek (fn SgiDatatype (x, _, xs, xncs) => if x = field then SOME (xs, xncs) else NONE
|
adamc@191
|
1253 | SgiDatatypeImp (x, _, _, _, _, xs, xncs) => if x = field then SOME (xs, xncs) else NONE
|
adamc@157
|
1254 | _ => NONE) sgis of
|
adamc@157
|
1255 NONE => NONE
|
adamc@191
|
1256 | SOME ((xs, xncs), subs) => SOME (xs,
|
adamc@191
|
1257 map (fn (x, n, to) => (x, n, Option.map (sgnSubCon (str, subs)) to)) xncs))
|
adamc@157
|
1258 | _ => NONE
|
adamc@157
|
1259
|
adamc@174
|
1260 fun projectConstructor env {sgn, str, field} =
|
adamc@174
|
1261 case #1 (hnormSgn env sgn) of
|
adamc@174
|
1262 SgnConst sgis =>
|
adamc@174
|
1263 let
|
adamc@191
|
1264 fun consider (n, xs, xncs) =
|
adamc@174
|
1265 ListUtil.search (fn (x, n', to) =>
|
adamc@174
|
1266 if x <> field then
|
adamc@174
|
1267 NONE
|
adamc@174
|
1268 else
|
adamc@191
|
1269 SOME (U.classifyDatatype xncs, n', xs, to, (CNamed n, #2 str))) xncs
|
adamc@174
|
1270 in
|
adamc@191
|
1271 case sgnSeek (fn SgiDatatype (_, n, xs, xncs) => consider (n, xs, xncs)
|
adamc@191
|
1272 | SgiDatatypeImp (_, n, _, _, _, xs, xncs) => consider (n, xs, xncs)
|
adamc@174
|
1273 | _ => NONE) sgis of
|
adamc@174
|
1274 NONE => NONE
|
adamc@191
|
1275 | SOME ((dk, n, xs, to, t), subs) => SOME (dk, n, xs, Option.map (sgnSubCon (str, subs)) to,
|
adamc@191
|
1276 sgnSubCon (str, subs) t)
|
adamc@174
|
1277 end
|
adamc@174
|
1278 | _ => NONE
|
adamc@174
|
1279
|
adamc@42
|
1280 fun projectVal env {sgn, str, field} =
|
adamc@42
|
1281 case #1 (hnormSgn env sgn) of
|
adamc@34
|
1282 SgnConst sgis =>
|
adamc@162
|
1283 let
|
adamc@191
|
1284 fun seek (n, xs, xncs) =
|
adamc@162
|
1285 ListUtil.search (fn (x, _, to) =>
|
adamc@162
|
1286 if x = field then
|
adamc@191
|
1287 SOME (let
|
adamc@467
|
1288 val base = (CNamed n, #2 sgn)
|
adamc@467
|
1289 val nxs = length xs
|
adamc@467
|
1290 val base = ListUtil.foldli (fn (i, _, base) =>
|
adamc@467
|
1291 (CApp (base,
|
adamc@467
|
1292 (CRel (nxs - i - 1), #2 sgn)),
|
adamc@467
|
1293 #2 sgn))
|
adamc@467
|
1294 base xs
|
adamc@467
|
1295
|
adamc@191
|
1296 val t =
|
adamc@191
|
1297 case to of
|
adamc@467
|
1298 NONE => base
|
adamc@467
|
1299 | SOME t => (TFun (t, base), #2 sgn)
|
adamc@191
|
1300 val k = (KType, #2 sgn)
|
adamc@191
|
1301 in
|
adamc@467
|
1302 foldr (fn (x, t) => (TCFun (Implicit, x, k, t), #2 sgn))
|
adamc@191
|
1303 t xs
|
adamc@191
|
1304 end)
|
adamc@162
|
1305 else
|
adamc@162
|
1306 NONE) xncs
|
adamc@162
|
1307 in
|
adamc@162
|
1308 case sgnSeek (fn SgiVal (x, _, c) => if x = field then SOME c else NONE
|
adamc@191
|
1309 | SgiDatatype (_, n, xs, xncs) => seek (n, xs, xncs)
|
adamc@191
|
1310 | SgiDatatypeImp (_, n, _, _, _, xs, xncs) => seek (n, xs, xncs)
|
adamc@162
|
1311 | _ => NONE) sgis of
|
adamc@162
|
1312 NONE => NONE
|
adamc@162
|
1313 | SOME (c, subs) => SOME (sgnSubCon (str, subs) c)
|
adamc@162
|
1314 end
|
adamc@34
|
1315 | SgnError => SOME (CError, ErrorMsg.dummySpan)
|
adamc@42
|
1316 | _ => NONE
|
adamc@34
|
1317
|
adamc@88
|
1318 fun sgnSeekConstraints (str, sgis) =
|
adamc@88
|
1319 let
|
adamc@88
|
1320 fun seek (sgis, sgns, strs, cons, acc) =
|
adamc@88
|
1321 case sgis of
|
adamc@88
|
1322 [] => acc
|
adamc@88
|
1323 | (sgi, _) :: sgis =>
|
adamc@88
|
1324 case sgi of
|
adamc@88
|
1325 SgiConstraint (c1, c2) =>
|
adamc@88
|
1326 let
|
adamc@88
|
1327 val sub = sgnSubCon (str, (sgns, strs, cons))
|
adamc@88
|
1328 in
|
adamc@88
|
1329 seek (sgis, sgns, strs, cons, (sub c1, sub c2) :: acc)
|
adamc@88
|
1330 end
|
adamc@88
|
1331 | SgiConAbs (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
|
adamc@88
|
1332 | SgiCon (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
|
adamc@191
|
1333 | SgiDatatype (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
|
adamc@191
|
1334 | SgiDatatypeImp (x, n, _, _, _, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
|
adamc@88
|
1335 | SgiVal _ => seek (sgis, sgns, strs, cons, acc)
|
adamc@88
|
1336 | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons, acc)
|
adamc@88
|
1337 | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons, acc)
|
adamc@563
|
1338 | SgiClassAbs (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
|
adamc@563
|
1339 | SgiClass (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
|
adamc@88
|
1340 in
|
adamc@88
|
1341 seek (sgis, IM.empty, IM.empty, IM.empty, [])
|
adamc@88
|
1342 end
|
adamc@88
|
1343
|
adamc@88
|
1344 fun projectConstraints env {sgn, str} =
|
adamc@88
|
1345 case #1 (hnormSgn env sgn) of
|
adamc@88
|
1346 SgnConst sgis => SOME (sgnSeekConstraints (str, sgis))
|
adamc@88
|
1347 | SgnError => SOME []
|
adamc@88
|
1348 | _ => NONE
|
adamc@34
|
1349
|
adamc@447
|
1350 fun edeclBinds env (d, loc) =
|
adamc@447
|
1351 case d of
|
adamc@447
|
1352 EDVal (x, t, _) => pushERel env x t
|
adamc@447
|
1353 | EDValRec vis => foldl (fn ((x, t, _), env) => pushERel env x t) env vis
|
adamc@447
|
1354
|
adamc@157
|
1355 fun declBinds env (d, loc) =
|
adamc@157
|
1356 case d of
|
adamc@157
|
1357 DCon (x, n, k, c) => pushCNamedAs env x n k (SOME c)
|
adamc@191
|
1358 | DDatatype (x, n, xs, xncs) =>
|
adamc@157
|
1359 let
|
adamc@297
|
1360 val k = (KType, loc)
|
adamc@297
|
1361 val nxs = length xs
|
adamc@297
|
1362 val (tb, kb) = ListUtil.foldli (fn (i, x', (tb, kb)) =>
|
adamc@297
|
1363 ((CApp (tb, (CRel (nxs - i - 1), loc)), loc),
|
adamc@297
|
1364 (KArrow (k, kb), loc)))
|
adamc@297
|
1365 ((CNamed n, loc), k) xs
|
adamc@297
|
1366
|
adamc@297
|
1367 val env = pushCNamedAs env x n kb NONE
|
adamc@191
|
1368 val env = pushDatatype env n xs xncs
|
adamc@157
|
1369 in
|
adamc@191
|
1370 foldl (fn ((x', n', to), env) =>
|
adamc@191
|
1371 let
|
adamc@191
|
1372 val t =
|
adamc@191
|
1373 case to of
|
adamc@297
|
1374 NONE => tb
|
adamc@297
|
1375 | SOME t => (TFun (t, tb), loc)
|
adamc@297
|
1376 val t = foldr (fn (x, t) => (TCFun (Implicit, x, k, t), loc)) t xs
|
adamc@191
|
1377 in
|
adamc@191
|
1378 pushENamedAs env x' n' t
|
adamc@191
|
1379 end)
|
adamc@191
|
1380 env xncs
|
adamc@157
|
1381 end
|
adamc@191
|
1382 | DDatatypeImp (x, n, m, ms, x', xs, xncs) =>
|
adamc@157
|
1383 let
|
adamc@157
|
1384 val t = (CModProj (m, ms, x'), loc)
|
adamc@297
|
1385 val k = (KType, loc)
|
adamc@297
|
1386 val nxs = length xs
|
adamc@297
|
1387 val (tb, kb) = ListUtil.foldli (fn (i, x', (tb, kb)) =>
|
adamc@297
|
1388 ((CApp (tb, (CRel (nxs - i - 1), loc)), loc),
|
adamc@297
|
1389 (KArrow (k, kb), loc)))
|
adamc@297
|
1390 ((CNamed n, loc), k) xs
|
adamc@297
|
1391
|
adamc@341
|
1392 val env = pushCNamedAs env x n kb (SOME t)
|
adamc@191
|
1393 val env = pushDatatype env n xs xncs
|
adamc@157
|
1394 in
|
adamc@191
|
1395 foldl (fn ((x', n', to), env) =>
|
adamc@191
|
1396 let
|
adamc@191
|
1397 val t =
|
adamc@191
|
1398 case to of
|
adamc@297
|
1399 NONE => tb
|
adamc@297
|
1400 | SOME t => (TFun (t, tb), loc)
|
adamc@297
|
1401 val t = foldr (fn (x, t) => (TCFun (Implicit, x, k, t), loc)) t xs
|
adamc@191
|
1402 in
|
adamc@191
|
1403 pushENamedAs env x' n' t
|
adamc@191
|
1404 end)
|
adamc@191
|
1405 env xncs
|
adamc@157
|
1406 end
|
adamc@157
|
1407 | DVal (x, n, t, _) => pushENamedAs env x n t
|
adamc@157
|
1408 | DValRec vis => foldl (fn ((x, n, t, _), env) => pushENamedAs env x n t) env vis
|
adamc@157
|
1409 | DSgn (x, n, sgn) => pushSgnNamedAs env x n sgn
|
adamc@157
|
1410 | DStr (x, n, sgn, _) => pushStrNamedAs env x n sgn
|
adamc@157
|
1411 | DFfiStr (x, n, sgn) => pushStrNamedAs env x n sgn
|
adamc@157
|
1412 | DConstraint _ => env
|
adamc@157
|
1413 | DExport _ => env
|
adamc@205
|
1414 | DTable (tn, x, n, c) =>
|
adamc@205
|
1415 let
|
adamc@338
|
1416 val t = (CApp ((CModProj (tn, [], "sql_table"), loc), c), loc)
|
adamc@338
|
1417 in
|
adamc@338
|
1418 pushENamedAs env x n t
|
adamc@338
|
1419 end
|
adamc@338
|
1420 | DSequence (tn, x, n) =>
|
adamc@338
|
1421 let
|
adamc@338
|
1422 val t = (CModProj (tn, [], "sql_sequence"), loc)
|
adamc@205
|
1423 in
|
adamc@205
|
1424 pushENamedAs env x n t
|
adamc@205
|
1425 end
|
adamc@563
|
1426 | DClass (x, n, k, c) =>
|
adamc@213
|
1427 let
|
adamc@563
|
1428 val k = (KArrow (k, (KType, loc)), loc)
|
adamc@213
|
1429 val env = pushCNamedAs env x n k (SOME c)
|
adamc@213
|
1430 in
|
adamc@213
|
1431 pushClass env n
|
adamc@213
|
1432 end
|
adamc@271
|
1433 | DDatabase _ => env
|
adamc@459
|
1434 | DCookie (tn, x, n, c) =>
|
adamc@459
|
1435 let
|
adamc@459
|
1436 val t = (CApp ((CModProj (tn, [], "cookie"), loc), c), loc)
|
adamc@459
|
1437 in
|
adamc@459
|
1438 pushENamedAs env x n t
|
adamc@459
|
1439 end
|
adamc@157
|
1440
|
adamc@243
|
1441 fun patBinds env (p, loc) =
|
adamc@243
|
1442 case p of
|
adamc@243
|
1443 PWild => env
|
adamc@243
|
1444 | PVar (x, t) => pushERel env x t
|
adamc@243
|
1445 | PPrim _ => env
|
adamc@243
|
1446 | PCon (_, _, _, NONE) => env
|
adamc@243
|
1447 | PCon (_, _, _, SOME p) => patBinds env p
|
adamc@243
|
1448 | PRecord xps => foldl (fn ((_, p, _), env) => patBinds env p) env xps
|
adamc@243
|
1449
|
adamc@2
|
1450 end
|