Mercurial > urweb
comparison src/elaborate.sml @ 513:5fc269f744ee
Remove unnecessary [kindof] calls
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Thu, 27 Nov 2008 10:13:22 -0500 |
parents | ae03d09043c1 |
children | 0fc08d1750e1 |
comparison
equal
deleted
inserted
replaced
512:40b19310ea9a | 513:5fc269f744ee |
---|---|
538 | Cons => "Cons" | 538 | Cons => "Cons" |
539 | Unknown => "Unknown") | 539 | Unknown => "Unknown") |
540 | 540 |
541 exception SummaryFailure | 541 exception SummaryFailure |
542 | 542 |
543 fun isUnitCon env (c, loc) = | |
544 case c of | |
545 L'.TFun _ => false | |
546 | L'.TCFun _ => false | |
547 | L'.TRecord _ => false | |
548 | |
549 | L'.CRel xn => #1 (#2 (E.lookupCRel env xn)) = L'.KUnit | |
550 | L'.CNamed xn => #1 (#2 (E.lookupCNamed env xn)) = L'.KUnit | |
551 | L'.CModProj (n, ms, x) => | |
552 let | |
553 val (_, sgn) = E.lookupStrNamed env n | |
554 val (str, sgn) = foldl (fn (m, (str, sgn)) => | |
555 case E.projectStr env {sgn = sgn, str = str, field = m} of | |
556 NONE => raise Fail "kindof: Unknown substructure" | |
557 | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) | |
558 ((L'.StrVar n, loc), sgn) ms | |
559 in | |
560 case E.projectCon env {sgn = sgn, str = str, field = x} of | |
561 NONE => raise Fail "kindof: Unknown con in structure" | |
562 | SOME ((k, _), _) => k = L'.KUnit | |
563 end | |
564 | |
565 | L'.CApp (c, _) => | |
566 (case hnormKind (kindof env c) of | |
567 (L'.KArrow (_, k), _) => #1 k = L'.KUnit | |
568 | (L'.KError, _) => false | |
569 | k => raise CUnify' (CKindof (k, c, "arrow"))) | |
570 | L'.CAbs _ => false | |
571 | L'.CDisjoint (_, _, _, c) => isUnitCon env c | |
572 | |
573 | L'.CName _ => false | |
574 | |
575 | L'.CRecord _ => false | |
576 | L'.CConcat _ => false | |
577 | L'.CFold _ => false | |
578 | |
579 | L'.CUnit => true | |
580 | |
581 | L'.CTuple _ => false | |
582 | L'.CProj (c, n) => | |
583 (case hnormKind (kindof env c) of | |
584 (L'.KTuple ks, _) => #1 (List.nth (ks, n - 1)) = L'.KUnit | |
585 | k => raise CUnify' (CKindof (k, c, "tuple"))) | |
586 | |
587 | L'.CError => false | |
588 | L'.CUnif (_, k, _, _) => #1 k = L'.KUnit | |
589 | |
543 fun unifyRecordCons (env, denv) (c1, c2) = | 590 fun unifyRecordCons (env, denv) (c1, c2) = |
544 let | 591 let |
545 fun rkindof c = | 592 fun rkindof c = |
546 case hnormKind (kindof env c) of | 593 case hnormKind (kindof env c) of |
547 (L'.KRecord k, _) => k | 594 (L'.KRecord k, _) => k |
822 val gs4 = unifyCons' (env, denv') t1 t2 | 869 val gs4 = unifyCons' (env, denv') t1 t2 |
823 in | 870 in |
824 gs1 @ gs2 @ gs3 @ gs4 | 871 gs1 @ gs2 @ gs3 @ gs4 |
825 end | 872 end |
826 | _ => | 873 | _ => |
827 case (kindof env c1, kindof env c2) of | 874 if isUnitCon env c1 andalso isUnitCon env c2 then |
828 ((L'.KUnit, _), (L'.KUnit, _)) => [] | 875 [] |
829 | _ => | 876 else |
830 let | 877 let |
831 val (c1, gs1) = hnormCon (env, denv) c1 | 878 val (c1, gs1) = hnormCon (env, denv) c1 |
832 val (c2, gs2) = hnormCon (env, denv) c2 | 879 val (c2, gs2) = hnormCon (env, denv) c2 |
833 in | 880 in |
834 let | 881 let |
1720 val (e, t, gs2) = elabExp (env, denv) e | 1767 val (e, t, gs2) = elabExp (env, denv) e |
1721 in | 1768 in |
1722 ((L'.ELet (eds, e), loc), t, gs1 @ gs2) | 1769 ((L'.ELet (eds, e), loc), t, gs1 @ gs2) |
1723 end | 1770 end |
1724 in | 1771 in |
1725 (*prefaces "/elabExp" [("e", SourcePrint.p_exp eAll)];*) | 1772 (*prefaces "elabExp" [("e", SourcePrint.p_exp eAll), |
1773 ("t", PD.string (LargeInt.toString (Time.toMilliseconds (Time.- (Time.now (), befor)))))];*) | |
1726 r | 1774 r |
1727 end | 1775 end |
1728 | 1776 |
1729 and elabEdecl denv (dAll as (d, loc), (env, gs : constraint list)) = | 1777 and elabEdecl denv (dAll as (d, loc), (env, gs : constraint list)) = |
1730 let | 1778 let |
3243 end | 3291 end |
3244 | 3292 |
3245 (*val tcs = List.filter (fn TypeClass _ => true | _ => false) (#3 (#2 r))*) | 3293 (*val tcs = List.filter (fn TypeClass _ => true | _ => false) (#3 (#2 r))*) |
3246 in | 3294 in |
3247 (*prefaces "elabDecl" [("e", SourcePrint.p_decl dAll), | 3295 (*prefaces "elabDecl" [("e", SourcePrint.p_decl dAll), |
3248 ("|tcs|", PD.string (Int.toString (length tcs)))];*) | 3296 ("t", PD.string (LargeInt.toString (Time.toMilliseconds |
3297 (Time.- (Time.now (), befor)))))];*) | |
3249 | 3298 |
3250 r | 3299 r |
3251 end | 3300 end |
3252 | 3301 |
3253 and elabStr (env, denv) (str, loc) = | 3302 and elabStr (env, denv) (str, loc) = |