Mercurial > urweb
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) = |