comparison src/elaborate.sml @ 518:685d232bd1a5

Remove some isUnitCon cases
author Adam Chlipala <adamc@hcoop.net>
date Thu, 27 Nov 2008 11:17:56 -0500
parents 0fc08d1750e1
children 44958d74c43f
comparison
equal deleted inserted replaced
517:aceb2d982f8f 518:685d232bd1a5
546 | L'.TCFun _ => false 546 | L'.TCFun _ => false
547 | L'.TRecord _ => false 547 | L'.TRecord _ => false
548 548
549 | L'.CRel xn => #1 (#2 (E.lookupCRel env xn)) = L'.KUnit 549 | L'.CRel xn => #1 (#2 (E.lookupCRel env xn)) = L'.KUnit
550 | L'.CNamed xn => #1 (#2 (E.lookupCNamed env xn)) = L'.KUnit 550 | L'.CNamed xn => #1 (#2 (E.lookupCNamed env xn)) = L'.KUnit
551 | L'.CModProj (n, ms, x) => 551 | L'.CModProj (n, ms, x) => false
552 let 552 (*let
553 val (_, sgn) = E.lookupStrNamed env n 553 val (_, sgn) = E.lookupStrNamed env n
554 val (str, sgn) = foldl (fn (m, (str, sgn)) => 554 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
555 case E.projectStr env {sgn = sgn, str = str, field = m} of 555 case E.projectStr env {sgn = sgn, str = str, field = m} of
556 NONE => raise Fail "kindof: Unknown substructure" 556 NONE => raise Fail "kindof: Unknown substructure"
557 | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) 557 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
558 ((L'.StrVar n, loc), sgn) ms 558 ((L'.StrVar n, loc), sgn) ms
559 in 559 in
560 case E.projectCon env {sgn = sgn, str = str, field = x} of 560 case E.projectCon env {sgn = sgn, str = str, field = x} of
561 NONE => raise Fail "kindof: Unknown con in structure" 561 NONE => raise Fail "kindof: Unknown con in structure"
562 | SOME ((k, _), _) => k = L'.KUnit 562 | SOME ((k, _), _) => k = L'.KUnit
563 end 563 end*)
564 564
565 | L'.CApp (c, _) => 565 | L'.CApp (c, _) => false
566 (case hnormKind (kindof env c) of 566 (*(case hnormKind (kindof env c) of
567 (L'.KArrow (_, k), _) => #1 k = L'.KUnit 567 (L'.KArrow (_, k), _) => #1 k = L'.KUnit
568 | (L'.KError, _) => false 568 | (L'.KError, _) => false
569 | k => raise CUnify' (CKindof (k, c, "arrow"))) 569 | k => raise CUnify' (CKindof (k, c, "arrow")))*)
570 | L'.CAbs _ => false 570 | L'.CAbs _ => false
571 | L'.CDisjoint (_, _, _, c) => isUnitCon env c 571 | L'.CDisjoint (_, _, _, c) => false(*isUnitCon env c*)
572 572
573 | L'.CName _ => false 573 | L'.CName _ => false
574 574
575 | L'.CRecord _ => false 575 | L'.CRecord _ => false
576 | L'.CConcat _ => false 576 | L'.CConcat _ => false
577 | L'.CFold _ => false 577 | L'.CFold _ => false
578 578
579 | L'.CUnit => true 579 | L'.CUnit => true
580 580
581 | L'.CTuple _ => false 581 | L'.CTuple _ => false
582 | L'.CProj (c, n) => 582 | L'.CProj (c, n) => false
583 (case hnormKind (kindof env c) of 583 (*(case hnormKind (kindof env c) of
584 (L'.KTuple ks, _) => #1 (List.nth (ks, n - 1)) = L'.KUnit 584 (L'.KTuple ks, _) => #1 (List.nth (ks, n - 1)) = L'.KUnit
585 | k => raise CUnify' (CKindof (k, c, "tuple"))) 585 | k => raise CUnify' (CKindof (k, c, "tuple")))*)
586 586
587 | L'.CError => false 587 | L'.CError => false
588 | L'.CUnif (_, k, _, _) => #1 k = L'.KUnit 588 | L'.CUnif (_, k, _, _) => #1 k = L'.KUnit
589 589
590 fun unifyRecordCons (env, denv) (c1, c2) = 590 fun unifyRecordCons (env, denv) (c1, c2) =