Mercurial > urweb

comparison src/elab_env.sml @ 211:e86411f647c6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Initial type class support
author Adam Chlipala <adamc@hcoop.net>
date Sat, 16 Aug 2008 14:32:18 -0400
parents cb8f69556975
children 0343557355fc
comparison
equal deleted inserted replaced
210:f4033abd6ab1 211:e86411f647c6
29 29
30 open Elab 30 open Elab
31 31
32 structure U = ElabUtil 32 structure U = ElabUtil
33 33
34 structure IS = IntBinarySet
34 structure IM = IntBinaryMap 35 structure IM = IntBinaryMap
35 structure SM = BinaryMapFn(struct 36 structure SM = BinaryMapFn(struct
36 type ord_key = string 37 type ord_key = string
37 val compare = String.compare 38 val compare = String.compare
38 end) 39 end)
59 bind = fn (bound, U.Con.Rel _) => bound + 1 60 bind = fn (bound, U.Con.Rel _) => bound + 1
60 | (bound, _) => bound} 61 | (bound, _) => bound}
61 62
62 val lift = liftConInCon 0 63 val lift = liftConInCon 0
63 64
65 val liftExpInExp =
66 U.Exp.mapB {kind = fn k => k,
67 con = fn _ => fn c => c,
68 exp = fn bound => fn e =>
69 case e of
70 ERel xn =>
71 if xn < bound then
72 e
73 else
74 ERel (xn + 1)
75 | _ => e,
76 bind = fn (bound, U.Exp.RelE _) => bound + 1
77 | (bound, _) => bound}
78
79
80 val liftExp = liftExpInExp 0
64 81
65 (* Back to environments *) 82 (* Back to environments *)
66 83
67 datatype 'a var' = 84 datatype 'a var' =
68 Rel' of int * 'a 85 Rel' of int * 'a
73 | Rel of int * 'a 90 | Rel of int * 'a
74 | Named of int * 'a 91 | Named of int * 'a
75 92
76 type datatyp = string list * (string * con option) IM.map 93 type datatyp = string list * (string * con option) IM.map
77 94
95 datatype class_name =
96 ClNamed of int
97 | ClProj of int * string list * string
98
99 structure CK = struct
100 type ord_key = class_name
101 open Order
102 fun compare x =
103 case x of
104 (ClNamed n1, ClNamed n2) => Int.compare (n1, n2)
105 | (ClNamed _, _) => LESS
106 | (_, ClNamed _) => GREATER
107
108 | (ClProj (m1, ms1, x1), ClProj (m2, ms2, x2)) =>
109 join (Int.compare (m1, m2),
110 fn () => join (joinL String.compare (ms1, ms2),
111 fn () => String.compare (x1, x2)))
112 end
113
114 structure CM = BinaryMapFn(CK)
115
116 datatype class_key =
117 CkNamed of int
118 | CkRel of int
119 | CkProj of int * string list * string
120
121 structure KK = struct
122 type ord_key = class_key
123 open Order
124 fun compare x =
125 case x of
126 (CkNamed n1, CkNamed n2) => Int.compare (n1, n2)
127 | (CkNamed _, _) => LESS
128 | (_, CkNamed _) => GREATER
129
130 | (CkRel n1, CkRel n2) => Int.compare (n1, n2)
131 | (CkRel _, _) => LESS
132 | (_, CkRel _) => GREATER
133
134 | (CkProj (m1, ms1, x1), CkProj (m2, ms2, x2)) =>
135 join (Int.compare (m1, m2),
136 fn () => join (joinL String.compare (ms1, ms2),
137 fn () => String.compare (x1, x2)))
138 end
139
140 structure KM = BinaryMapFn(KK)
141
142 type class = {
143 ground : exp KM.map
144 }
145
146 val empty_class = {
147 ground = KM.empty
148 }
149
78 type env = { 150 type env = {
79 renameC : kind var' SM.map, 151 renameC : kind var' SM.map,
80 relC : (string * kind) list, 152 relC : (string * kind) list,
81 namedC : (string * kind * con option) IM.map, 153 namedC : (string * kind * con option) IM.map,
82 154
83 datatypes : datatyp IM.map, 155 datatypes : datatyp IM.map,
84 constructors : (datatype_kind * int * string list * con option * int) SM.map, 156 constructors : (datatype_kind * int * string list * con option * int) SM.map,
85 157
158 classes : class CM.map,
159
86 renameE : con var' SM.map, 160 renameE : con var' SM.map,
87 relE : (string * con) list, 161 relE : (string * con) list,
88 namedE : (string * con) IM.map, 162 namedE : (string * con) IM.map,
89 163
90 renameSgn : (int * sgn) SM.map, 164 renameSgn : (int * sgn) SM.map,
110 namedC = IM.empty, 184 namedC = IM.empty,
111 185
112 datatypes = IM.empty, 186 datatypes = IM.empty,
113 constructors = SM.empty, 187 constructors = SM.empty,
114 188
189 classes = CM.empty,
190
115 renameE = SM.empty, 191 renameE = SM.empty,
116 relE = [], 192 relE = [],
117 namedE = IM.empty, 193 namedE = IM.empty,
118 194
119 renameSgn = SM.empty, 195 renameSgn = SM.empty,
121 197
122 renameStr = SM.empty, 198 renameStr = SM.empty,
123 str = IM.empty 199 str = IM.empty
124 } 200 }
125 201
202 fun liftClassKey ck =
203 case ck of
204 CkNamed _ => ck
205 | CkRel n => CkRel (n + 1)
206 | CkProj _ => ck
207
126 fun pushCRel (env : env) x k = 208 fun pushCRel (env : env) x k =
127 let 209 let
128 val renameC = SM.map (fn Rel' (n, k) => Rel' (n+1, k) 210 val renameC = SM.map (fn Rel' (n, k) => Rel' (n+1, k)
129 | x => x) (#renameC env) 211 | x => x) (#renameC env)
130 in 212 in
132 relC = (x, k) :: #relC env, 214 relC = (x, k) :: #relC env,
133 namedC = IM.map (fn (x, k, co) => (x, k, Option.map lift co)) (#namedC env), 215 namedC = IM.map (fn (x, k, co) => (x, k, Option.map lift co)) (#namedC env),
134 216
135 datatypes = #datatypes env, 217 datatypes = #datatypes env,
136 constructors = #constructors env, 218 constructors = #constructors env,
219
220 classes = CM.map (fn class => {
221 ground = KM.foldli (fn (ck, e, km) =>
222 KM.insert (km, liftClassKey ck, e))
223 KM.empty (#ground class)
224 })
225 (#classes env),
137 226
138 renameE = #renameE env, 227 renameE = #renameE env,
139 relE = map (fn (x, c) => (x, lift c)) (#relE env), 228 relE = map (fn (x, c) => (x, lift c)) (#relE env),
140 namedE = IM.map (fn (x, c) => (x, lift c)) (#namedE env), 229 namedE = IM.map (fn (x, c) => (x, lift c)) (#namedE env),
141 230
156 relC = #relC env, 245 relC = #relC env,
157 namedC = IM.insert (#namedC env, n, (x, k, co)), 246 namedC = IM.insert (#namedC env, n, (x, k, co)),
158 247
159 datatypes = #datatypes env, 248 datatypes = #datatypes env,
160 constructors = #constructors env, 249 constructors = #constructors env,
250
251 classes = #classes env,
161 252
162 renameE = #renameE env, 253 renameE = #renameE env,
163 relE = #relE env, 254 relE = #relE env,
164 namedE = #namedE env, 255 namedE = #namedE env,
165 256
201 IM.insert (cons, n, (x, to))) IM.empty xncs)), 292 IM.insert (cons, n, (x, to))) IM.empty xncs)),
202 constructors = foldl (fn ((x, n', to), cmap) => 293 constructors = foldl (fn ((x, n', to), cmap) =>
203 SM.insert (cmap, x, (dk, n', xs, to, n))) 294 SM.insert (cmap, x, (dk, n', xs, to, n)))
204 (#constructors env) xncs, 295 (#constructors env) xncs,
205 296
297 classes = #classes env,
298
206 renameE = #renameE env, 299 renameE = #renameE env,
207 relE = #relE env, 300 relE = #relE env,
208 namedE = #namedE env, 301 namedE = #namedE env,
209 302
210 renameSgn = #renameSgn env, 303 renameSgn = #renameSgn env,
227 fun lookupConstructor (env : env) s = SM.find (#constructors env, s) 320 fun lookupConstructor (env : env) s = SM.find (#constructors env, s)
228 321
229 fun datatypeArgs (xs, _) = xs 322 fun datatypeArgs (xs, _) = xs
230 fun constructors (_, dt) = IM.foldri (fn (n, (x, to), ls) => (x, n, to) :: ls) [] dt 323 fun constructors (_, dt) = IM.foldri (fn (n, (x, to), ls) => (x, n, to) :: ls) [] dt
231 324
325 fun pushClass (env : env) n =
326 {renameC = #renameC env,
327 relC = #relC env,
328 namedC = #namedC env,
329
330 datatypes = #datatypes env,
331 constructors = #constructors env,
332
333 classes = CM.insert (#classes env, ClNamed n, {ground = KM.empty}),
334
335 renameE = #renameE env,
336 relE = #relE env,
337 namedE = #namedE env,
338
339 renameSgn = #renameSgn env,
340 sgn = #sgn env,
341
342 renameStr = #renameStr env,
343 str = #str env}
344
345 fun class_name_in (c, _) =
346 case c of
347 CNamed n => SOME (ClNamed n)
348 | CModProj x => SOME (ClProj x)
349 | _ => NONE
350
351 fun class_key_in (c, _) =
352 case c of
353 CRel n => SOME (CkRel n)
354 | CNamed n => SOME (CkNamed n)
355 | CModProj x => SOME (CkProj x)
356 | _ => NONE
357
358 fun class_pair_in (c, _) =
359 case c of
360 CApp (f, x) =>
361 (case (class_name_in f, class_key_in x) of
362 (SOME f, SOME x) => SOME (f, x)
363 | _ => NONE)
364 | _ => NONE
365
366 fun resolveClass (env : env) c =
367 case class_pair_in c of
368 SOME (f, x) =>
369 (case CM.find (#classes env, f) of
370 NONE => NONE
371 | SOME class =>
372 case KM.find (#ground class, x) of
373 NONE => NONE
374 | SOME e => SOME e)
375 | _ => NONE
376
232 fun pushERel (env : env) x t = 377 fun pushERel (env : env) x t =
233 let 378 let
234 val renameE = SM.map (fn Rel' (n, t) => Rel' (n+1, t) 379 val renameE = SM.map (fn Rel' (n, t) => Rel' (n+1, t)
235 | x => x) (#renameE env) 380 | x => x) (#renameE env)
381
382 val classes = CM.map (fn class => {
383 ground = KM.map liftExp (#ground class)
384 }) (#classes env)
385 val classes = case class_pair_in t of
386 NONE => classes
387 | SOME (f, x) =>
388 let
389 val class = Option.getOpt (CM.find (classes, f), empty_class)
390 val class = {
391 ground = KM.insert (#ground class, x, (ERel 0, #2 t))
392 }
393 in
394 CM.insert (classes, f, class)
395 end
236 in 396 in
237 {renameC = #renameC env, 397 {renameC = #renameC env,
238 relC = #relC env, 398 relC = #relC env,
239 namedC = #namedC env, 399 namedC = #namedC env,
240 400
241 datatypes = #datatypes env, 401 datatypes = #datatypes env,
242 constructors = #constructors env, 402 constructors = #constructors env,
243 403
404 classes = classes,
405
244 renameE = SM.insert (renameE, x, Rel' (0, t)), 406 renameE = SM.insert (renameE, x, Rel' (0, t)),
245 relE = (x, t) :: #relE env, 407 relE = (x, t) :: #relE env,
246 namedE = #namedE env, 408 namedE = #namedE env,
247 409
248 renameSgn = #renameSgn env, 410 renameSgn = #renameSgn env,
255 fun lookupERel (env : env) n = 417 fun lookupERel (env : env) n =
256 (List.nth (#relE env, n)) 418 (List.nth (#relE env, n))
257 handle Subscript => raise UnboundRel n 419 handle Subscript => raise UnboundRel n
258 420
259 fun pushENamedAs (env : env) x n t = 421 fun pushENamedAs (env : env) x n t =
260 {renameC = #renameC env, 422 let
261 relC = #relC env, 423 val classes = #classes env
262 namedC = #namedC env, 424 val classes = case class_pair_in t of
263 425 NONE => classes
264 datatypes = #datatypes env, 426 | SOME (f, x) =>
265 constructors = #constructors env, 427 let
266 428 val class = Option.getOpt (CM.find (classes, f), empty_class)
267 renameE = SM.insert (#renameE env, x, Named' (n, t)), 429 val class = {
268 relE = #relE env, 430 ground = KM.insert (#ground class, x, (ENamed n, #2 t))
269 namedE = IM.insert (#namedE env, n, (x, t)), 431 }
270 432 in
271 renameSgn = #renameSgn env, 433 CM.insert (classes, f, class)
272 sgn = #sgn env, 434 end
273 435 in
274 renameStr = #renameStr env, 436 {renameC = #renameC env,
275 str = #str env} 437 relC = #relC env,
438 namedC = #namedC env,
439
440 datatypes = #datatypes env,
441 constructors = #constructors env,
442
443 classes = classes,
444
445 renameE = SM.insert (#renameE env, x, Named' (n, t)),
446 relE = #relE env,
447 namedE = IM.insert (#namedE env, n, (x, t)),
448
449 renameSgn = #renameSgn env,
450 sgn = #sgn env,
451
452 renameStr = #renameStr env,
453 str = #str env}
454 end
276 455
277 fun pushENamed env x t = 456 fun pushENamed env x t =
278 let 457 let
279 val n = !namedCounter 458 val n = !namedCounter
280 in 459 in
299 namedC = #namedC env, 478 namedC = #namedC env,
300 479
301 datatypes = #datatypes env, 480 datatypes = #datatypes env,
302 constructors = #constructors env, 481 constructors = #constructors env,
303 482
483 classes = #classes env,
484
304 renameE = #renameE env, 485 renameE = #renameE env,
305 relE = #relE env, 486 relE = #relE env,
306 namedE = #namedE env, 487 namedE = #namedE env,
307 488
308 renameSgn = SM.insert (#renameSgn env, x, (n, sgis)), 489 renameSgn = SM.insert (#renameSgn env, x, (n, sgis)),
324 NONE => raise UnboundNamed n 505 NONE => raise UnboundNamed n
325 | SOME x => x 506 | SOME x => x
326 507
327 fun lookupSgn (env : env) x = SM.find (#renameSgn env, x) 508 fun lookupSgn (env : env) x = SM.find (#renameSgn env, x)
328 509
329 fun pushStrNamedAs (env : env) x n sgis =
330 {renameC = #renameC env,
331 relC = #relC env,
332 namedC = #namedC env,
333
334 datatypes = #datatypes env,
335 constructors = #constructors env,
336
337 renameE = #renameE env,
338 relE = #relE env,
339 namedE = #namedE env,
340
341 renameSgn = #renameSgn env,
342 sgn = #sgn env,
343
344 renameStr = SM.insert (#renameStr env, x, (n, sgis)),
345 str = IM.insert (#str env, n, (x, sgis))}
346
347 fun pushStrNamed env x sgis =
348 let
349 val n = !namedCounter
350 in
351 namedCounter := n + 1;
352 (pushStrNamedAs env x n sgis, n)
353 end
354
355 fun lookupStrNamed (env : env) n = 510 fun lookupStrNamed (env : env) n =
356 case IM.find (#str env, n) of 511 case IM.find (#str env, n) of
357 NONE => raise UnboundNamed n 512 NONE => raise UnboundNamed n
358 | SOME x => x 513 | SOME x => x
359 514
360 fun lookupStr (env : env) x = SM.find (#renameStr env, x) 515 fun lookupStr (env : env) x = SM.find (#renameStr env, x)
361 516
362 fun sgiBinds env (sgi, loc) =
363 case sgi of
364 SgiConAbs (x, n, k) => pushCNamedAs env x n k NONE
365 | SgiCon (x, n, k, c) => pushCNamedAs env x n k (SOME c)
366 | SgiDatatype (x, n, xs, xncs) =>
367 let
368 val env = pushCNamedAs env x n (KType, loc) NONE
369 in
370 foldl (fn ((x', n', to), env) =>
371 let
372 val t =
373 case to of
374 NONE => (CNamed n, loc)
375 | SOME t => (TFun (t, (CNamed n, loc)), loc)
376
377 val k = (KType, loc)
378 val t = foldr (fn (x, t) => (TCFun (Explicit, x, k, t), loc)) t xs
379 in
380 pushENamedAs env x' n' t
381 end)
382 env xncs
383 end
384 | SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) =>
385 let
386 val env = pushCNamedAs env x n (KType, loc) (SOME (CModProj (m1, ms, x'), loc))
387 in
388 foldl (fn ((x', n', to), env) =>
389 let
390 val t =
391 case to of
392 NONE => (CNamed n, loc)
393 | SOME t => (TFun (t, (CNamed n, loc)), loc)
394
395 val k = (KType, loc)
396 val t = foldr (fn (x, t) => (TCFun (Explicit, x, k, t), loc)) t xs
397 in
398 pushENamedAs env x' n' t
399 end)
400 env xncs
401 end
402 | SgiVal (x, n, t) => pushENamedAs env x n t
403 | SgiStr (x, n, sgn) => pushStrNamedAs env x n sgn
404 | SgiSgn (x, n, sgn) => pushSgnNamedAs env x n sgn
405 | SgiConstraint _ => env
406
407 | SgiTable (tn, x, n, c) =>
408 let
409 val t = (CApp ((CModProj (tn, [], "table"), loc), c), loc)
410 in
411 pushENamedAs env x n t
412 end
413 517
414 fun sgnSeek f sgis = 518 fun sgnSeek f sgis =
415 let 519 let
416 fun seek (sgis, sgns, strs, cons) = 520 fun seek (sgis, sgns, strs, cons) =
417 case sgis of 521 case sgis of
437 | SgiVal _ => seek (sgis, sgns, strs, cons) 541 | SgiVal _ => seek (sgis, sgns, strs, cons)
438 | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons) 542 | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons)
439 | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons) 543 | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons)
440 | SgiConstraint _ => seek (sgis, sgns, strs, cons) 544 | SgiConstraint _ => seek (sgis, sgns, strs, cons)
441 | SgiTable _ => seek (sgis, sgns, strs, cons) 545 | SgiTable _ => seek (sgis, sgns, strs, cons)
546 | SgiClassAbs (x, n) => seek (sgis, sgns, strs, IM.insert (cons, n, x))
547 | SgiClass (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x))
442 in 548 in
443 seek (sgis, IM.empty, IM.empty, IM.empty) 549 seek (sgis, IM.empty, IM.empty, IM.empty)
444 end 550 end
445 551
446 fun id x = x 552 fun id x = x
498 in 604 in
499 SgnProj (m1, ms, nx) 605 SgnProj (m1, ms, nx)
500 end) 606 end)
501 | _ => sgn 607 | _ => sgn
502 608
503 fun sgnSubCon x =
504 ElabUtil.Con.map {kind = id,
505 con = sgnS_con x}
506
507 fun sgnSubSgn x = 609 fun sgnSubSgn x =
508 ElabUtil.Sgn.map {kind = id, 610 ElabUtil.Sgn.map {kind = id,
509 con = sgnS_con x, 611 con = sgnS_con x,
510 sgn_item = id, 612 sgn_item = id,
511 sgn = sgnS_sgn x} 613 sgn = sgnS_sgn x}
512 614
513 fun hnormSgn env (all as (sgn, loc)) = 615
616
617 and projectSgn env {sgn, str, field} =
618 case #1 (hnormSgn env sgn) of
619 SgnConst sgis =>
620 (case sgnSeek (fn SgiSgn (x, _, sgn) => if x = field then SOME sgn else NONE | _ => NONE) sgis of
621 NONE => NONE
622 | SOME (sgn, subs) => SOME (sgnSubSgn (str, subs) sgn))
623 | SgnError => SOME (SgnError, ErrorMsg.dummySpan)
624 | _ => NONE
625
626 and hnormSgn env (all as (sgn, loc)) =
514 case sgn of 627 case sgn of
515 SgnError => all 628 SgnError => all
516 | SgnVar n => hnormSgn env (#2 (lookupSgnNamed env n)) 629 | SgnVar n => hnormSgn env (#2 (lookupSgnNamed env n))
517 | SgnConst _ => all 630 | SgnConst _ => all
518 | SgnFun _ => all 631 | SgnFun _ => all
545 in 658 in
546 (SgnConst sgis, loc) 659 (SgnConst sgis, loc)
547 end 660 end
548 | _ => raise Fail "ElabEnv.hnormSgn: Can't reduce 'where' [2]" 661 | _ => raise Fail "ElabEnv.hnormSgn: Can't reduce 'where' [2]"
549 662
550 and projectSgn env {sgn, str, field} = 663 fun enrichClasses env classes (m1, ms) sgn =
551 case #1 (hnormSgn env sgn) of 664 case #1 (hnormSgn env sgn) of
552 SgnConst sgis => 665 SgnConst sgis =>
553 (case sgnSeek (fn SgiSgn (x, _, sgn) => if x = field then SOME sgn else NONE | _ => NONE) sgis of 666 let
554 NONE => NONE 667 val (classes, _) =
555 | SOME (sgn, subs) => SOME (sgnSubSgn (str, subs) sgn)) 668 foldl (fn (sgi, (classes, newClasses)) =>
556 | SgnError => SOME (SgnError, ErrorMsg.dummySpan) 669 let
557 | _ => NONE 670 fun found (x, n) =
671 (CM.insert (classes,
672 ClProj (m1, ms, x),
673 empty_class),
674 IS.add (newClasses, n))
675 in
676 case #1 sgi of
677 SgiClassAbs xn => found xn
678 | SgiClass (x, n, _) => found (x, n)
679 | _ => (classes, newClasses)
680 end)
681 (classes, IS.empty) sgis
682 in
683 classes
684 end
685 | _ => classes
686
687 fun pushStrNamedAs (env : env) x n sgn =
688 {renameC = #renameC env,
689 relC = #relC env,
690 namedC = #namedC env,
691
692 datatypes = #datatypes env,
693 constructors = #constructors env,
694
695 classes = enrichClasses env (#classes env) (n, []) sgn,
696
697 renameE = #renameE env,
698 relE = #relE env,
699 namedE = #namedE env,
700
701 renameSgn = #renameSgn env,
702 sgn = #sgn env,
703
704 renameStr = SM.insert (#renameStr env, x, (n, sgn)),
705 str = IM.insert (#str env, n, (x, sgn))}
706
707 fun pushStrNamed env x sgn =
708 let
709 val n = !namedCounter
710 in
711 namedCounter := n + 1;
712 (pushStrNamedAs env x n sgn, n)
713 end
714
715 fun sgiBinds env (sgi, loc) =
716 case sgi of
717 SgiConAbs (x, n, k) => pushCNamedAs env x n k NONE
718 | SgiCon (x, n, k, c) => pushCNamedAs env x n k (SOME c)
719 | SgiDatatype (x, n, xs, xncs) =>
720 let
721 val env = pushCNamedAs env x n (KType, loc) NONE
722 in
723 foldl (fn ((x', n', to), env) =>
724 let
725 val t =
726 case to of
727 NONE => (CNamed n, loc)
728 | SOME t => (TFun (t, (CNamed n, loc)), loc)
729
730 val k = (KType, loc)
731 val t = foldr (fn (x, t) => (TCFun (Explicit, x, k, t), loc)) t xs
732 in
733 pushENamedAs env x' n' t
734 end)
735 env xncs
736 end
737 | SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) =>
738 let
739 val env = pushCNamedAs env x n (KType, loc) (SOME (CModProj (m1, ms, x'), loc))
740 in
741 foldl (fn ((x', n', to), env) =>
742 let
743 val t =
744 case to of
745 NONE => (CNamed n, loc)
746 | SOME t => (TFun (t, (CNamed n, loc)), loc)
747
748 val k = (KType, loc)
749 val t = foldr (fn (x, t) => (TCFun (Explicit, x, k, t), loc)) t xs
750 in
751 pushENamedAs env x' n' t
752 end)
753 env xncs
754 end
755 | SgiVal (x, n, t) => pushENamedAs env x n t
756 | SgiStr (x, n, sgn) => pushStrNamedAs env x n sgn
757 | SgiSgn (x, n, sgn) => pushSgnNamedAs env x n sgn
758 | SgiConstraint _ => env
759
760 | SgiTable (tn, x, n, c) =>
761 let
762 val t = (CApp ((CModProj (tn, [], "table"), loc), c), loc)
763 in
764 pushENamedAs env x n t
765 end
766
767 | SgiClassAbs (x, n) => pushCNamedAs env x n (KArrow ((KType, loc), (KType, loc)), loc) NONE
768 | SgiClass (x, n, c) => pushCNamedAs env x n (KArrow ((KType, loc), (KType, loc)), loc) (SOME c)
769
770
771 fun sgnSubCon x =
772 ElabUtil.Con.map {kind = id,
773 con = sgnS_con x}
558 774
559 fun projectStr env {sgn, str, field} = 775 fun projectStr env {sgn, str, field} =
560 case #1 (hnormSgn env sgn) of 776 case #1 (hnormSgn env sgn) of
561 SgnConst sgis => 777 SgnConst sgis =>
562 (case sgnSeek (fn SgiStr (x, _, sgn) => if x = field then SOME sgn else NONE | _ => NONE) sgis of 778 (case sgnSeek (fn SgiStr (x, _, sgn) => if x = field then SOME sgn else NONE | _ => NONE) sgis of
673 | SgiDatatypeImp (x, n, _, _, _, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc) 889 | SgiDatatypeImp (x, n, _, _, _, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
674 | SgiVal _ => seek (sgis, sgns, strs, cons, acc) 890 | SgiVal _ => seek (sgis, sgns, strs, cons, acc)
675 | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons, acc) 891 | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons, acc)
676 | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons, acc) 892 | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons, acc)
677 | SgiTable _ => seek (sgis, sgns, strs, cons, acc) 893 | SgiTable _ => seek (sgis, sgns, strs, cons, acc)
894 | SgiClassAbs (x, n) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
895 | SgiClass (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
678 in 896 in
679 seek (sgis, IM.empty, IM.empty, IM.empty, []) 897 seek (sgis, IM.empty, IM.empty, IM.empty, [])
680 end 898 end
681 899
682 fun projectConstraints env {sgn, str} = 900 fun projectConstraints env {sgn, str} =