Mercurial > urweb

comparison src/elab_env.sml @ 684:f0224c7f12bb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Expunging nullable fields
author Adam Chlipala <adamc@hcoop.net>
date Sun, 29 Mar 2009 14:13:50 -0400
parents 81573f62d6c3
children 70cbdcf5989b
comparison
equal deleted inserted replaced
683:9a2c18dab11d 684:f0224c7f12bb
188 datatype class_key = 188 datatype class_key =
189 CkNamed of int 189 CkNamed of int
190 | CkRel of int 190 | CkRel of int
191 | CkProj of int * string list * string 191 | CkProj of int * string list * string
192 | CkApp of class_key * class_key 192 | CkApp of class_key * class_key
193 | CkOther of con
193 194
194 fun ck2s ck = 195 fun ck2s ck =
195 case ck of 196 case ck of
196 CkNamed n => "Named(" ^ Int.toString n ^ ")" 197 CkNamed n => "Named(" ^ Int.toString n ^ ")"
197 | CkRel n => "Rel(" ^ Int.toString n ^ ")" 198 | CkRel n => "Rel(" ^ Int.toString n ^ ")"
198 | CkProj (m, ms, x) => "Proj(" ^ Int.toString m ^ "," ^ String.concatWith "," ms ^ "," ^ x ^ ")" 199 | CkProj (m, ms, x) => "Proj(" ^ Int.toString m ^ "," ^ String.concatWith "," ms ^ "," ^ x ^ ")"
199 | CkApp (ck1, ck2) => "App(" ^ ck2s ck1 ^ ", " ^ ck2s ck2 ^ ")" 200 | CkApp (ck1, ck2) => "App(" ^ ck2s ck1 ^ ", " ^ ck2s ck2 ^ ")"
201 | CkOther _ => "Other"
200 202
201 type class_key_n = class_key * int 203 type class_key_n = class_key * int
202 204
203 fun ckn2s (ck, n) = ck2s ck ^ "[" ^ Int.toString n ^ "]" 205 fun ckn2s (ck, n) = ck2s ck ^ "[" ^ Int.toString n ^ "]"
204 206
225 | (_, CkProj _) => GREATER 227 | (_, CkProj _) => GREATER
226 228
227 | (CkApp (f1, x1), CkApp (f2, x2)) => 229 | (CkApp (f1, x1), CkApp (f2, x2)) =>
228 join (compare' (f1, f2), 230 join (compare' (f1, f2),
229 fn () => compare' (x1, x2)) 231 fn () => compare' (x1, x2))
232 | (CkApp _, _) => LESS
233 | (_, CkApp _) => GREATER
234
235 | (CkOther _, CkOther _) => EQUAL
230 fun compare ((k1, n1), (k2, n2)) = 236 fun compare ((k1, n1), (k2, n2)) =
231 join (Int.compare (n1, n2), 237 join (Int.compare (n1, n2),
232 fn () => compare' (k1, k2)) 238 fn () => compare' (k1, k2))
233 end 239 end
234 240
307 case ck of 313 case ck of
308 CkNamed _ => ck 314 CkNamed _ => ck
309 | CkRel n => CkRel (n + 1) 315 | CkRel n => CkRel (n + 1)
310 | CkProj _ => ck 316 | CkProj _ => ck
311 | CkApp (ck1, ck2) => CkApp (liftClassKey' ck1, liftClassKey' ck2) 317 | CkApp (ck1, ck2) => CkApp (liftClassKey' ck1, liftClassKey' ck2)
318 | CkOther c => CkOther (lift c)
312 319
313 fun liftClassKey (ck, n) = (liftClassKey' ck, n) 320 fun liftClassKey (ck, n) = (liftClassKey' ck, n)
314 321
315 fun pushKRel (env : env) x = 322 fun pushKRel (env : env) x =
316 let 323 let
511 | find (SOME c) = Option.isSome (CM.find (#classes env, c)) 518 | find (SOME c) = Option.isSome (CM.find (#classes env, c))
512 in 519 in
513 find (class_name_in c) 520 find (class_name_in c)
514 end 521 end
515 522
516 fun class_key_in (c, _) = 523 fun class_key_in (all as (c, _)) =
517 case c of 524 case c of
518 CRel n => SOME (CkRel n) 525 CRel n => CkRel n
519 | CNamed n => SOME (CkNamed n) 526 | CNamed n => CkNamed n
520 | CModProj x => SOME (CkProj x) 527 | CModProj x => CkProj x
521 | CUnif (_, _, _, ref (SOME c)) => class_key_in c 528 | CUnif (_, _, _, ref (SOME c)) => class_key_in c
522 | CApp (c1, c2) => 529 | CApp (c1, c2) => CkApp (class_key_in c1, class_key_in c2)
523 (case (class_key_in c1, class_key_in c2) of 530 | _ => CkOther all
524 (SOME k1, SOME k2) => SOME (CkApp (k1, k2))
525 | _ => NONE)
526 | _ => NONE
527 531
528 fun class_key_out loc = 532 fun class_key_out loc =
529 let 533 let
530 fun cko k = 534 fun cko k =
531 case k of 535 case k of
532 CkRel n => (CRel n, loc) 536 CkRel n => (CRel n, loc)
533 | CkNamed n => (CNamed n, loc) 537 | CkNamed n => (CNamed n, loc)
534 | CkProj x => (CModProj x, loc) 538 | CkProj x => (CModProj x, loc)
535 | CkApp (k1, k2) => (CApp (cko k1, cko k2), loc) 539 | CkApp (k1, k2) => (CApp (cko k1, cko k2), loc)
540 | CkOther c => c
536 in 541 in
537 cko 542 cko
538 end 543 end
539 544
540 fun class_pair_in (c, _) = 545 fun class_pair_in (c, _) =
541 case c of 546 case c of
542 CApp (f, x) => 547 CApp (f, x) =>
543 (case (class_name_in f, class_key_in x) of 548 (case class_name_in f of
544 (SOME f, SOME x) => SOME (f, x) 549 SOME f => SOME (f, class_key_in x)
545 | _ => NONE) 550 | _ => NONE)
546 | CUnif (_, _, _, ref (SOME c)) => class_pair_in c 551 | CUnif (_, _, _, ref (SOME c)) => class_pair_in c
547 | _ => NONE 552 | _ => NONE
548 553
549 fun sub_class_key (n, c) = 554 fun sub_class_key (n, c) =
550 let 555 let
551 fun csk k = 556 fun csk k =
552 case k of 557 case k of
553 CkRel n' => if n' = n then 558 CkRel n' => SOME (if n' = n then
554 c 559 c
555 else 560 else
556 k 561 k)
557 | CkNamed _ => k 562 | CkNamed _ => SOME k
558 | CkProj _ => k 563 | CkProj _ => SOME k
559 | CkApp (k1, k2) => CkApp (csk k1, csk k2) 564 | CkApp (k1, k2) =>
565 (case (csk k1, csk k2) of
566 (SOME k1, SOME k2) => SOME (CkApp (k1, k2))
567 | _ => NONE)
568 | CkOther _ => NONE
560 in 569 in
561 csk 570 csk
562 end 571 end
563 572
564 fun resolveClass (env : env) c = 573 fun resolveClass (env : env) c =
602 SOME (cs, e) => 611 SOME (cs, e) =>
603 let 612 let
604 val es = map (fn (cn, ck) => 613 val es = map (fn (cn, ck) =>
605 let 614 let
606 val ck = ListUtil.foldli (fn (i, arg, ck) => 615 val ck = ListUtil.foldli (fn (i, arg, ck) =>
607 sub_class_key (len - i - 1, 616 case ck of
608 arg) 617 NONE => NONE
609 ck) 618 | SOME ck =>
610 ck args 619 sub_class_key (len - i - 1,
620 arg)
621 ck)
622 (SOME ck) args
611 in 623 in
612 doPair (cn, ck) 624 case ck of
625 NONE => NONE
626 | SOME ck => doPair (cn, ck)
613 end) cs 627 end) cs
614 in 628 in
615 if List.exists (not o Option.isSome) es then 629 if List.exists (not o Option.isSome) es then
616 tryNext () 630 tryNext ()
617 else 631 else
685 699
686 datatype rule = 700 datatype rule =
687 Normal of int * (class_name * class_key) list * class_key 701 Normal of int * (class_name * class_key) list * class_key
688 | Inclusion of class_name 702 | Inclusion of class_name
689 703
704 fun containsOther k =
705 case k of
706 CkOther _ => true
707 | CkApp (k1, k2) => containsOther k1 orelse containsOther k2
708 | _ => false
709
690 fun rule_in c = 710 fun rule_in c =
691 let 711 let
692 fun quantifiers (c, nvars) = 712 fun quantifiers (c, nvars) =
693 case #1 c of 713 case #1 c of
694 TCFun (_, _, _, c) => quantifiers (c, nvars + 1) 714 TCFun (_, _, _, c) => quantifiers (c, nvars + 1)
705 NONE => NONE 725 NONE => NONE
706 | SOME (cn, ck) => 726 | SOME (cn, ck) =>
707 let 727 let
708 fun dearg (ck, i) = 728 fun dearg (ck, i) =
709 if i >= nvars then 729 if i >= nvars then
710 SOME (cn, Normal (nvars, hyps, ck)) 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))
711 else case ck of 735 else case ck of
712 CkApp (ck, CkRel i') => 736 CkApp (ck, CkRel i') =>
713 if i' = i then 737 if i' = i then
714 dearg (ck, i + 1) 738 dearg (ck, i + 1)
715 else 739 else