Mercurial > urweb

comparison src/elaborate.sml @ 513:5fc269f744ee

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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) =