Mercurial > urweb

comparison src/elab_env.sml @ 711:7292bcb7c02d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Made type class system very general; demo compiles
author Adam Chlipala <adamc@hcoop.net>
date Thu, 09 Apr 2009 12:31:56 -0400
parents d8217b4cb617
children f152f215a02c
comparison
equal deleted inserted replaced
710:71409a4ccb67 711:7292bcb7c02d
160 160
161 datatype class_name = 161 datatype class_name =
162 ClNamed of int 162 ClNamed of int
163 | ClProj of int * string list * string 163 | ClProj of int * string list * string
164 164
165 fun class_name_out cn =
166 case cn of
167 ClNamed n => (CNamed n, ErrorMsg.dummySpan)
168 | ClProj x => (CModProj x, ErrorMsg.dummySpan)
169
165 fun cn2s cn = 170 fun cn2s cn =
166 case cn of 171 case cn of
167 ClNamed n => "Named(" ^ Int.toString n ^ ")" 172 ClNamed n => "Named(" ^ Int.toString n ^ ")"
168 | ClProj (m, ms, x) => "Proj(" ^ Int.toString m ^ "," ^ String.concatWith "," ms ^ "," ^ x ^ ")" 173 | ClProj (m, ms, x) => "Proj(" ^ Int.toString m ^ "," ^ String.concatWith "," ms ^ "," ^ x ^ ")"
169 174
183 end 188 end
184 189
185 structure CS = BinarySetFn(CK) 190 structure CS = BinarySetFn(CK)
186 structure CM = BinaryMapFn(CK) 191 structure CM = BinaryMapFn(CK)
187 192
188 datatype class_key = 193 type class = {ground : (con * exp) list,
189 CkNamed of int 194 rules : (int * con list * con * exp) list}
190 | CkRel of int 195 val empty_class = {ground = [],
191 | CkProj of int * string list * string 196 rules = []}
192 | CkApp of class_key * class_key
193 | CkOther of con
194
195 fun ck2s ck =
196 case ck of
197 CkNamed n => "Named(" ^ Int.toString n ^ ")"
198 | CkRel n => "Rel(" ^ Int.toString n ^ ")"
199 | CkProj (m, ms, x) => "Proj(" ^ Int.toString m ^ "," ^ String.concatWith "," ms ^ "," ^ x ^ ")"
200 | CkApp (ck1, ck2) => "App(" ^ ck2s ck1 ^ ", " ^ ck2s ck2 ^ ")"
201 | CkOther _ => "Other"
202
203 type class_key_n = class_key * int
204
205 fun ckn2s (ck, n) = ck2s ck ^ "[" ^ Int.toString n ^ "]"
206
207 fun cp2s (cn, ck) = "(" ^ cn2s cn ^ "," ^ ck2s ck ^ ")"
208
209 structure KK = struct
210 type ord_key = class_key_n
211 open Order
212 fun compare' x =
213 case x of
214 (CkNamed n1, CkNamed n2) => Int.compare (n1, n2)
215 | (CkNamed _, _) => LESS
216 | (_, CkNamed _) => GREATER
217
218 | (CkRel n1, CkRel n2) => Int.compare (n1, n2)
219 | (CkRel _, _) => LESS
220 | (_, CkRel _) => GREATER
221
222 | (CkProj (m1, ms1, x1), CkProj (m2, ms2, x2)) =>
223 join (Int.compare (m1, m2),
224 fn () => join (joinL String.compare (ms1, ms2),
225 fn () => String.compare (x1, x2)))
226 | (CkProj _, _) => LESS
227 | (_, CkProj _) => GREATER
228
229 | (CkApp (f1, x1), CkApp (f2, x2)) =>
230 join (compare' (f1, f2),
231 fn () => compare' (x1, x2))
232 | (CkApp _, _) => LESS
233 | (_, CkApp _) => GREATER
234
235 | (CkOther _, CkOther _) => EQUAL
236 fun compare ((k1, n1), (k2, n2)) =
237 join (Int.compare (n1, n2),
238 fn () => compare' (k1, k2))
239 end
240
241 structure KM = BinaryMapFn(KK)
242
243 type class = {ground : ((class_name * class_key) list * exp) KM.map,
244 inclusions : exp CM.map}
245 val empty_class = {ground = KM.empty,
246 inclusions = CM.empty}
247
248 fun printClasses cs = (print "Classes:\n";
249 CM.appi (fn (cn, {ground = km, ...} : class) =>
250 (print (cn2s cn ^ ":");
251 KM.appi (fn (ck, _) => print (" " ^ ckn2s ck)) km;
252 print "\n")) cs)
253 197
254 type env = { 198 type env = {
255 renameK : int SM.map, 199 renameK : int SM.map,
256 relK : string list, 200 relK : string list,
257 201
306 sgn = IM.empty, 250 sgn = IM.empty,
307 251
308 renameStr = SM.empty, 252 renameStr = SM.empty,
309 str = IM.empty 253 str = IM.empty
310 } 254 }
311
312 fun liftClassKey' ck =
313 case ck of
314 CkNamed _ => ck
315 | CkRel n => CkRel (n + 1)
316 | CkProj _ => ck
317 | CkApp (ck1, ck2) => CkApp (liftClassKey' ck1, liftClassKey' ck2)
318 | CkOther c => CkOther (lift c)
319
320 fun liftClassKey (ck, n) = (liftClassKey' ck, n)
321 255
322 fun pushKRel (env : env) x = 256 fun pushKRel (env : env) x =
323 let 257 let
324 val renameK = SM.map (fn n => n+1) (#renameK env) 258 val renameK = SM.map (fn n => n+1) (#renameK env)
325 in 259 in
332 namedC = #namedC env, 266 namedC = #namedC env,
333 267
334 datatypes = #datatypes env, 268 datatypes = #datatypes env,
335 constructors = #constructors env, 269 constructors = #constructors env,
336 270
337 classes = #classes env, 271 classes = CM.map (fn cl => {ground = map (fn (c, e) =>
272 (liftKindInCon 0 c,
273 e))
274 (#ground cl),
275 rules = #rules cl})
276 (#classes env),
338 277
339 renameE = SM.map (fn Rel' (n, c) => Rel' (n, liftKindInCon 0 c) 278 renameE = SM.map (fn Rel' (n, c) => Rel' (n, liftKindInCon 0 c)
340 | Named' (n, c) => Named' (n, c)) (#renameE env), 279 | Named' (n, c) => Named' (n, c)) (#renameE env),
341 relE = map (fn (x, c) => (x, liftKindInCon 0 c)) (#relE env), 280 relE = map (fn (x, c) => (x, liftKindInCon 0 c)) (#relE env),
342 namedE = #namedE env, 281 namedE = #namedE env,
369 308
370 datatypes = #datatypes env, 309 datatypes = #datatypes env,
371 constructors = #constructors env, 310 constructors = #constructors env,
372 311
373 classes = CM.map (fn class => 312 classes = CM.map (fn class =>
374 {ground = KM.foldli (fn (ck, e, km) => 313 {ground = map (fn (c, e) =>
375 KM.insert (km, liftClassKey ck, e)) 314 (liftConInCon 0 c,
376 KM.empty (#ground class), 315 e))
377 inclusions = #inclusions class}) 316 (#ground class),
317 rules = #rules class})
378 (#classes env), 318 (#classes env),
379 319
380 renameE = SM.map (fn Rel' (n, c) => Rel' (n, lift c) 320 renameE = SM.map (fn Rel' (n, c) => Rel' (n, lift c)
381 | Named' (n, c) => Named' (n, c)) (#renameE env), 321 | Named' (n, c) => Named' (n, c)) (#renameE env),
382 relE = map (fn (x, c) => (x, lift c)) (#relE env), 322 relE = map (fn (x, c) => (x, lift c)) (#relE env),
480 fun lookupConstructor (env : env) s = SM.find (#constructors env, s) 420 fun lookupConstructor (env : env) s = SM.find (#constructors env, s)
481 421
482 fun datatypeArgs (xs, _) = xs 422 fun datatypeArgs (xs, _) = xs
483 fun constructors (_, dt) = IM.foldri (fn (n, (x, to), ls) => (x, n, to) :: ls) [] dt 423 fun constructors (_, dt) = IM.foldri (fn (n, (x, to), ls) => (x, n, to) :: ls) [] dt
484 424
425 fun listClasses (env : env) =
426 map (fn (cn, {ground, rules}) =>
427 (class_name_out cn,
428 ground
429 @ map (fn (nvs, cs, c, e) =>
430 let
431 val loc = #2 c
432 val c = foldr (fn (c', c) => (TFun (c', c), loc)) c cs
433 val c = ListUtil.foldli (fn (n, (), c) => (TCFun (Explicit,
434 "x" ^ Int.toString n,
435 (KError, loc),
436 c), loc))
437 c (List.tabulate (nvs, fn _ => ()))
438 in
439 (c, e)
440 end) rules)) (CM.listItemsi (#classes env))
441
485 fun pushClass (env : env) n = 442 fun pushClass (env : env) n =
486 {renameK = #renameK env, 443 {renameK = #renameK env,
487 relK = #relK env, 444 relK = #relK env,
488 445
489 renameC = #renameC env, 446 renameC = #renameC env,
518 | find (SOME c) = Option.isSome (CM.find (#classes env, c)) 475 | find (SOME c) = Option.isSome (CM.find (#classes env, c))
519 in 476 in
520 find (class_name_in c) 477 find (class_name_in c)
521 end 478 end
522 479
523 fun class_key_in (all as (c, _)) = 480 fun class_head_in c =
524 case c of 481 case #1 c of
525 CRel n => CkRel n 482 CApp (f, _) => class_head_in f
526 | CNamed n => CkNamed n 483 | CUnif (_, _, _, ref (SOME c)) => class_head_in c
527 | CModProj x => CkProj x 484 | _ => class_name_in c
528 | CUnif (_, _, _, ref (SOME c)) => class_key_in c 485
529 | CApp (c1, c2) => CkApp (class_key_in c1, class_key_in c2) 486 exception Unify
530 | _ => CkOther all 487
531 488 fun unifyKinds (k1, k2) =
532 fun class_key_out loc = 489 case (#1 k1, #1 k2) of
533 let 490 (KType, KType) => ()
534 fun cko k = 491 | (KArrow (d1, r1), KArrow (d2, r2)) => (unifyKinds (d1, d2); unifyKinds (r1, r2))
535 case k of 492 | (KName, KName) => ()
536 CkRel n => (CRel n, loc) 493 | (KRecord k1, KRecord k2) => unifyKinds (k1, k2)
537 | CkNamed n => (CNamed n, loc) 494 | (KUnit, KUnit) => ()
538 | CkProj x => (CModProj x, loc) 495 | (KTuple ks1, KTuple ks2) => (ListPair.appEq unifyKinds (ks1, ks2)
539 | CkApp (k1, k2) => (CApp (cko k1, cko k2), loc) 496 handle ListPair.UnequalLengths => raise Unify)
540 | CkOther c => c 497 | (KUnif (_, _, ref (SOME k1)), _) => unifyKinds (k1, k2)
541 in 498 | (_, KUnif (_, _, ref (SOME k2))) => unifyKinds (k1, k2)
542 cko 499 | (KRel n1, KRel n2) => if n1 = n2 then () else raise Unify
543 end 500 | (KFun (_, k1), KFun (_, k2)) => unifyKinds (k1, k2)
544 501 | _ => raise Unify
545 fun class_pair_in (c, _) = 502
546 case c of 503 fun unifyCons rs =
547 CApp (f, x) => 504 let
548 (case class_name_in f of 505 fun unify d (c1, c2) =
549 SOME f => SOME (f, class_key_in x) 506 case (#1 c1, #1 c2) of
550 | _ => NONE) 507 (CUnif (_, _, _, ref (SOME c1)), _) => unify d (c1, c2)
551 | CUnif (_, _, _, ref (SOME c)) => class_pair_in c 508 | (_, CUnif (_, _, _, ref (SOME c2))) => unify d (c1, c2)
552 | _ => NONE 509
553 510 | (c1', CRel n2) =>
554 fun sub_class_key (n, c) = 511 if n2 < d then
555 let 512 case c1' of
556 fun csk k = 513 CRel n1 => if n1 = n2 then () else raise Unify
557 case k of 514 | _ => raise Unify
558 CkRel n' => SOME (if n' = n then 515 else if n2 - d >= length rs then
559 c 516 case c1' of
560 else 517 CRel n1 => if n1 = n2 - length rs then () else raise Unify
561 k) 518 | _ => raise Unify
562 | CkNamed _ => SOME k 519 else
563 | CkProj _ => SOME k 520 let
564 | CkApp (k1, k2) => 521 val r = List.nth (rs, n2 - d)
565 (case (csk k1, csk k2) of 522 in
566 (SOME k1, SOME k2) => SOME (CkApp (k1, k2)) 523 case !r of
567 | _ => NONE) 524 NONE => r := SOME c1
568 | CkOther _ => NONE 525 | SOME c2 => unify d (c1, c2)
569 in 526 end
570 csk 527
571 end 528 | (TFun (d1, r1), TFun (d2, r2)) => (unify d (d1, d2); unify d (r1, r2))
572 529 | (TCFun (_, _, k1, r1), TCFun (_, _, k2, r2)) => (unifyKinds (k1, k2); unify (d + 1) (r1, r2))
573 fun resolveClass (env : env) c = 530 | (TRecord c1, TRecord c2) => unify d (c1, c2)
574 let 531 | (TDisjoint (a1, b1, c1), TDisjoint (a2, b2, c2)) =>
575 fun doPair (f, x) = 532 (unify d (a1, a2); unify d (b1, b2); unify d (c1, c2))
576 case CM.find (#classes env, f) of 533
577 NONE => NONE 534 | (CNamed n1, CNamed n2) => if n1 = n2 then () else raise Unify
578 | SOME class => 535 | (CModProj (n1, ms1, x1), CModProj (n2, ms2, x2)) =>
579 let 536 if n1 = n2 andalso ms1 = ms2 andalso x1 = x2 then () else raise Unify
580 val loc = #2 c 537 | (CApp (f1, x1), CApp (f2, x2)) => (unify d (f1, f2); unify d (x1, x2))
581 538 | (CAbs (_, k1, b1), CAbs (_, k2, b2)) => (unifyKinds (k1, k2); unify (d + 1) (b1, b2))
582 fun tryIncs () = 539
540 | (CKAbs (_, b1), CKAbs (_, b2)) => unify d (b1, b2)
541 | (CKApp (c1, k1), CKApp (c2, k2)) => (unify d (c1, c2); unifyKinds (k1, k2))
542 | (TKFun (_, c1), TKFun (_, c2)) => unify d (c1, c2)
543
544 | (CName s1, CName s2) => if s1 = s2 then () else raise Unify
545
546 | (CRecord (k1, xcs1), CRecord (k2, xcs2)) =>
547 (unifyKinds (k1, k2);
548 ListPair.appEq (fn ((x1, c1), (x2, c2)) => (unify d (x1, x2); unify d (c1, c2))) (xcs1, xcs2)
549 handle ListPair.UnequalLengths => raise Unify)
550 | (CConcat (f1, x1), CConcat (f2, x2)) => (unify d (f1, f2); unify d (x1, x2))
551 | (CMap (d1, r1), CMap (d2, r2)) => (unifyKinds (d1, d2); unifyKinds (r1, r2))
552
553 | (CUnit, CUnit) => ()
554
555 | (CTuple cs1, CTuple cs2) => (ListPair.appEq (unify d) (cs1, cs2)
556 handle ListPair.UnequalLengths => raise Unify)
557 | (CProj (c1, n1), CProj (c2, n2)) => (unify d (c1, c2);
558 if n1 = n2 then () else raise Unify)
559
560 | _ => raise Unify
561 in
562 unify
563 end
564
565 fun tryUnify nRs (c1, c2) =
566 let
567 val rs = List.tabulate (nRs, fn _ => ref NONE)
568 in
569 (unifyCons rs 0 (c1, c2);
570 SOME (map (fn r => case !r of
571 NONE => raise Unify
572 | SOME c => c) rs))
573 handle Unify => NONE
574 end
575
576 fun unifySubst (rs : con list) =
577 U.Con.mapB {kind = fn _ => fn k => k,
578 con = fn d => fn c =>
579 case c of
580 CRel n =>
581 if n < d then
582 c
583 else
584 #1 (List.nth (rs, n - d))
585 | _ => c,
586 bind = fn (d, U.Con.RelC _) => d + 1
587 | (d, _) => d}
588 0
589
590 fun resolveClass (env : env) =
591 let
592 fun resolve c =
593 let
594 fun doHead f =
595 case CM.find (#classes env, f) of
596 NONE => NONE
597 | SOME class =>
583 let 598 let
584 fun tryIncs fs = 599 val loc = #2 c
585 case fs of 600
601 fun tryRules rules =
602 case rules of
586 [] => NONE 603 [] => NONE
587 | (f', e') :: fs => 604 | (nRs, cs, c', e) :: rules' =>
588 case doPair (f', x) of 605 case tryUnify nRs (c, c') of
589 NONE => tryIncs fs 606 NONE => tryRules rules'
590 | SOME e => 607 | SOME rs =>
591 let 608 let
592 val e' = (ECApp (e', class_key_out loc x), loc) 609 val eos = map (resolve o unifySubst rs) cs
593 val e' = (EApp (e', e), loc)
594 in 610 in
595 SOME e' 611 if List.exists (not o Option.isSome) eos then
612 tryRules rules'
613 else
614 let
615 val es = List.mapPartial (fn x => x) eos
616
617 val e = foldr (fn (c, e) => (ECApp (e, c), loc)) e rs
618 val e = foldl (fn (e', e) => (EApp (e, e'), loc)) e es
619 in
620 SOME e
621 end
596 end 622 end
623
624 fun rules () = tryRules (#rules class)
625
626 fun tryGrounds ces =
627 case ces of
628 [] => rules ()
629 | (c', e) :: ces' =>
630 case tryUnify 0 (c, c') of
631 NONE => tryGrounds ces'
632 | SOME _ => SOME e
597 in 633 in
598 tryIncs (CM.listItemsi (#inclusions class)) 634 tryGrounds (#ground class)
599 end 635 end
600 636 in
601 fun tryRules (k, args) = 637 case class_head_in c of
602 let 638 SOME f => doHead f
603 val len = length args 639 | _ => NONE
604 640 end
605 fun tryNext () = 641 in
606 case k of 642 resolve
607 CkApp (k1, k2) => tryRules (k1, k2 :: args)
608 | _ => tryIncs ()
609 in
610 case KM.find (#ground class, (k, length args)) of
611 SOME (cs, e) =>
612 let
613 val es = map (fn (cn, ck) =>
614 let
615 val ck = ListUtil.foldli (fn (i, arg, ck) =>
616 case ck of
617 NONE => NONE
618 | SOME ck =>
619 sub_class_key (len - i - 1,
620 arg)
621 ck)
622 (SOME ck) args
623 in
624 case ck of
625 NONE => NONE
626 | SOME ck => doPair (cn, ck)
627 end) cs
628 in
629 if List.exists (not o Option.isSome) es then
630 tryNext ()
631 else
632 let
633 val e = foldl (fn (arg, e) => (ECApp (e, class_key_out loc arg), loc))
634 e args
635 val e = foldr (fn (pf, e) => (EApp (e, pf), loc))
636 e (List.mapPartial (fn x => x) es)
637 in
638 SOME e
639 end
640 end
641 | NONE => tryNext ()
642 end
643 in
644 tryRules (x, [])
645 end
646 in
647 case class_pair_in c of
648 SOME p => doPair p
649 | _ => NONE
650 end 643 end
651 644
652 fun pushERel (env : env) x t = 645 fun pushERel (env : env) x t =
653 let 646 let
654 val renameE = SM.map (fn Rel' (n, t) => Rel' (n+1, t) 647 val renameE = SM.map (fn Rel' (n, t) => Rel' (n+1, t)
655 | x => x) (#renameE env) 648 | x => x) (#renameE env)
656 649
657 val classes = CM.map (fn class => 650 val classes = CM.map (fn class =>
658 {ground = KM.map (fn (ps, e) => (ps, liftExp e)) (#ground class), 651 {ground = map (fn (c, e) => (c, liftExp e)) (#ground class),
659 inclusions = #inclusions class}) (#classes env) 652 rules = #rules class}) (#classes env)
660 val classes = case class_pair_in t of 653 val classes = case class_head_in t of
661 NONE => classes 654 NONE => classes
662 | SOME (f, x) => 655 | SOME f =>
663 case CM.find (classes, f) of 656 case CM.find (classes, f) of
664 NONE => classes 657 NONE => classes
665 | SOME class => 658 | SOME class =>
666 let 659 let
667 val class = {ground = KM.insert (#ground class, (x, 0), ([], (ERel 0, #2 t))), 660 val class = {ground = (t, (ERel 0, #2 t)) :: #ground class,
668 inclusions = #inclusions class} 661 rules = #rules class}
669 in 662 in
670 CM.insert (classes, f, class) 663 CM.insert (classes, f, class)
671 end 664 end
672 in 665 in
673 {renameK = #renameK env, 666 {renameK = #renameK env,
694 end 687 end
695 688
696 fun lookupERel (env : env) n = 689 fun lookupERel (env : env) n =
697 (List.nth (#relE env, n)) 690 (List.nth (#relE env, n))
698 handle Subscript => raise UnboundRel n 691 handle Subscript => raise UnboundRel n
699
700 datatype rule =
701 Normal of int * (class_name * class_key) list * class_key
702 | Inclusion of class_name
703
704 fun containsOther k =
705 case k of
706 CkOther _ => true
707 | CkApp (k1, k2) => containsOther k1 orelse containsOther k2
708 | _ => false
709 692
710 fun rule_in c = 693 fun rule_in c =
711 let 694 let
712 fun quantifiers (c, nvars) = 695 fun quantifiers (c, nvars) =
713 case #1 c of 696 case #1 c of
715 | _ => 698 | _ =>
716 let 699 let
717 fun clauses (c, hyps) = 700 fun clauses (c, hyps) =
718 case #1 c of 701 case #1 c of
719 TFun (hyp, c) => 702 TFun (hyp, c) =>
720 (case class_pair_in hyp of 703 (case class_head_in hyp of
721 SOME (p as (_, CkRel _)) => clauses (c, p :: hyps) 704 SOME _ => clauses (c, hyp :: hyps)
722 | _ => NONE) 705 | NONE => NONE)
723 | _ => 706 | _ =>
724 case class_pair_in c of 707 case class_head_in c of
725 NONE => NONE 708 NONE => NONE
726 | SOME (cn, ck) => 709 | SOME f => SOME (f, nvars, rev hyps, c)
727 let
728 fun dearg (ck, i) =
729 if i >= nvars then
730 if containsOther ck
731 orelse List.exists (fn (_, k) => containsOther k) hyps then
732 NONE
733 else
734 SOME (cn, Normal (nvars, hyps, ck))
735 else case ck of
736 CkApp (ck, CkRel i') =>
737 if i' = i then
738 dearg (ck, i + 1)
739 else
740 NONE
741 | _ => NONE
742 in
743 dearg (ck, 0)
744 end
745 in 710 in
746 clauses (c, []) 711 clauses (c, [])
747 end 712 end
748 in 713 in
749 case #1 c of 714 quantifiers (c, 0)
750 TCFun (_, _, _, (TFun ((CApp (f1, (CRel 0, _)), _),
751 (CApp (f2, (CRel 0, _)), _)), _)) =>
752 (case (class_name_in f1, class_name_in f2) of
753 (SOME f1, SOME f2) => SOME (f2, Inclusion f1)
754 | _ => NONE)
755 | _ => quantifiers (c, 0)
756 end
757
758 fun inclusion (classes : class CM.map, init, inclusions, f, e : exp) =
759 let
760 fun search (f, fs) =
761 if f = init then
762 NONE
763 else if CS.member (fs, f) then
764 SOME fs
765 else
766 let
767 val fs = CS.add (fs, f)
768 in
769 case CM.find (classes, f) of
770 NONE => SOME fs
771 | SOME {inclusions = fs', ...} =>
772 CM.foldli (fn (f', _, fs) =>
773 case fs of
774 NONE => NONE
775 | SOME fs => search (f', fs)) (SOME fs) fs'
776 end
777 in
778 case search (f, CS.empty) of
779 SOME _ => CM.insert (inclusions, f, e)
780 | NONE => (ErrorMsg.errorAt (#2 e) "Type class inclusion would create a cycle";
781 inclusions)
782 end 715 end
783 716
784 fun pushENamedAs (env : env) x n t = 717 fun pushENamedAs (env : env) x n t =
785 let 718 let
786 val classes = #classes env 719 val classes = #classes env
787 val classes = case rule_in t of 720 val classes = case rule_in t of
788 NONE => classes 721 NONE => classes
789 | SOME (f, rule) => 722 | SOME (f, nvs, cs, c) =>
790 case CM.find (classes, f) of 723 case CM.find (classes, f) of
791 NONE => classes 724 NONE => classes
792 | SOME class => 725 | SOME class =>
793 let 726 let
794 val e = (ENamed n, #2 t) 727 val e = (ENamed n, #2 t)
795 728
796 val class = 729 val class =
797 case rule of 730 {ground = #ground class,
798 Normal (nvars, hyps, x) => 731 rules = (nvs, cs, c, e) :: #rules class}
799 {ground = KM.insert (#ground class, (x, nvars), (hyps, e)),
800 inclusions = #inclusions class}
801 | Inclusion f' =>
802 {ground = #ground class,
803 inclusions = inclusion (classes, f, #inclusions class, f', e)}
804 in 732 in
805 CM.insert (classes, f, class) 733 CM.insert (classes, f, class)
806 end 734 end
807 in 735 in
808 {renameK = #renameK env, 736 {renameK = #renameK env,
982 NONE => c 910 NONE => c
983 | SOME nx => CModProj (m1, ms', nx)) 911 | SOME nx => CModProj (m1, ms', nx))
984 | CApp (c1, c2) => CApp ((sgnS_con' arg (#1 c1), #2 c1), 912 | CApp (c1, c2) => CApp ((sgnS_con' arg (#1 c1), #2 c1),
985 (sgnS_con' arg (#1 c2), #2 c2)) 913 (sgnS_con' arg (#1 c2), #2 c2))
986 | _ => c 914 | _ => c
987
988 fun sgnS_class_name (arg as (m1, ms', (sgns, strs, cons))) nm =
989 case nm of
990 ClProj (m1, ms, x) =>
991 (case IM.find (strs, m1) of
992 NONE => nm
993 | SOME m1x => ClProj (m1, ms' @ m1x :: ms, x))
994 | ClNamed n =>
995 (case IM.find (cons, n) of
996 NONE => nm
997 | SOME nx => ClProj (m1, ms', nx))
998
999 fun sgnS_class_key (arg as (m1, ms', (sgns, strs, cons))) k =
1000 case k of
1001 CkProj (m1, ms, x) =>
1002 (case IM.find (strs, m1) of
1003 NONE => k
1004 | SOME m1x => CkProj (m1, ms' @ m1x :: ms, x))
1005 | CkNamed n =>
1006 (case IM.find (cons, n) of
1007 NONE => k
1008 | SOME nx => CkProj (m1, ms', nx))
1009 | CkApp (k1, k2) => CkApp (sgnS_class_key arg k1,
1010 sgnS_class_key arg k2)
1011 | _ => k
1012 915
1013 fun sgnS_sgn (str, (sgns, strs, cons)) sgn = 916 fun sgnS_sgn (str, (sgns, strs, cons)) sgn =
1014 case sgn of 917 case sgn of
1015 SgnProj (m1, ms, x) => 918 SgnProj (m1, ms, x) =>
1016 (case IM.find (strs, m1) of 919 (case IM.find (strs, m1) of
1118 | SgiClassAbs (x, n, _) => found (x, n) 1021 | SgiClassAbs (x, n, _) => found (x, n)
1119 | SgiClass (x, n, _, _) => found (x, n) 1022 | SgiClass (x, n, _, _) => found (x, n)
1120 | SgiVal (x, n, c) => 1023 | SgiVal (x, n, c) =>
1121 (case rule_in c of 1024 (case rule_in c of
1122 NONE => default () 1025 NONE => default ()
1123 | SOME (cn, rule) => 1026 | SOME (cn, nvs, cs, c) =>
1124 let 1027 let
1125 val globalizeN = sgnS_class_name (m1, ms, fmap) 1028 val loc = #2 c
1126 val globalize = sgnS_class_key (m1, ms, fmap) 1029 fun globalize (c, loc) = (sgnS_con' (m1, ms, fmap) c, loc)
1127
1128 fun unravel c =
1129 case c of
1130 ClNamed n =>
1131 ((case lookupCNamed env n of
1132 (_, _, SOME c') =>
1133 (case class_name_in c' of
1134 NONE => c
1135 | SOME k => unravel k)
1136 | _ => c)
1137 handle UnboundNamed _ => c)
1138 | _ => c
1139 1030
1140 val nc = 1031 val nc =
1141 case cn of 1032 case cn of
1142 ClNamed f => IM.find (newClasses, f) 1033 ClNamed f => IM.find (newClasses, f)
1143 | _ => NONE 1034 | _ => NONE
1148 val classes = 1039 val classes =
1149 case CM.find (classes, cn) of 1040 case CM.find (classes, cn) of
1150 NONE => classes 1041 NONE => classes
1151 | SOME class => 1042 | SOME class =>
1152 let 1043 let
1153 val e = (EModProj (m1, ms, x), 1044 val e = (EModProj (m1, ms, x), #2 sgn)
1154 #2 sgn)
1155 1045
1156 val class = 1046 val class =
1157 case rule of 1047 {ground = #ground class,
1158 Normal (nvars, hyps, a) => 1048 rules = (nvs,
1159 {ground = 1049 map globalize cs,
1160 KM.insert (#ground class, (globalize a, nvars), 1050 globalize c,
1161 (map (fn (n, k) => 1051 e) :: #rules class}
1162 (globalizeN n,
1163 globalize k)) hyps, e)),
1164 inclusions = #inclusions class}
1165 | Inclusion f' =>
1166 {ground = #ground class,
1167 inclusions = inclusion (classes, cn,
1168 #inclusions class,
1169 globalizeN f', e)}
1170 in 1052 in
1171 CM.insert (classes, cn, class) 1053 CM.insert (classes, cn, class)
1172 end 1054 end
1173 in 1055 in
1174 (classes, 1056 (classes,
1186 | SOME class => 1068 | SOME class =>
1187 let 1069 let
1188 val e = (EModProj (m1, ms, x), #2 sgn) 1070 val e = (EModProj (m1, ms, x), #2 sgn)
1189 1071
1190 val class = 1072 val class =
1191 case rule of 1073 {ground = #ground class,
1192 Normal (nvars, hyps, a) => 1074 rules = (nvs,
1193 {ground = 1075 map globalize cs,
1194 KM.insert (#ground class, (globalize a, nvars), 1076 globalize c,
1195 (map (fn (n, k) => 1077 e) :: #rules class}
1196 (globalizeN n,
1197 globalize k)) hyps, e)),
1198 inclusions = #inclusions class}
1199 | Inclusion f' =>
1200 {ground = #ground class,
1201 inclusions = inclusion (classes, cn,
1202 #inclusions class,
1203 globalizeN f', e)}
1204 in 1078 in
1205 CM.insert (classes, cn, class) 1079 CM.insert (classes, cn, class)
1206 end 1080 end
1207 in 1081 in
1208 (classes, 1082 (classes,
1299 | SgiVal (x, n, t) => pushENamedAs env x n t 1173 | SgiVal (x, n, t) => pushENamedAs env x n t
1300 | SgiStr (x, n, sgn) => pushStrNamedAs env x n sgn 1174 | SgiStr (x, n, sgn) => pushStrNamedAs env x n sgn
1301 | SgiSgn (x, n, sgn) => pushSgnNamedAs env x n sgn 1175 | SgiSgn (x, n, sgn) => pushSgnNamedAs env x n sgn
1302 | SgiConstraint _ => env 1176 | SgiConstraint _ => env
1303 1177
1304 | SgiClassAbs (x, n, k) => pushCNamedAs env x n (KArrow (k, (KType, loc)), loc) NONE 1178 | SgiClassAbs (x, n, k) => pushCNamedAs env x n k NONE
1305 | SgiClass (x, n, k, c) => pushCNamedAs env x n (KArrow (k, (KType, loc)), loc) (SOME c) 1179 | SgiClass (x, n, k, c) => pushCNamedAs env x n k (SOME c)
1306 1180
1307 fun sgnSubCon x = 1181 fun sgnSubCon x =
1308 ElabUtil.Con.map {kind = id, 1182 ElabUtil.Con.map {kind = id,
1309 con = sgnS_con x} 1183 con = sgnS_con x}
1310 1184