Commit 24287596c004a8a2345de1949fde6f5d0b620ad0

  • avatar
  • Antti-Juhani Kaijanaho <antti-juhani @kaij…aho.fi> (Committer)
  • Thu Nov 22 14:25:34 EET 2012
  • avatar
  • Antti-Juhani Kaijanaho <antti-juhani @kaij…aho.fi> (Author)
  • Thu Nov 22 14:25:34 EET 2012
Clean up a bit.

Signed-off-by: Antti-Juhani Kaijanaho <antti-juhani@kaijanaho.fi>
hm.y
(91 / 153)
  
687687 assert(0);
688688}
689689
690/*
691static bool unify_types_(struct type *ty1, struct type *ty2);
692static bool unify_types(struct type *ty1, struct type *ty2)
690/* Always returns false. */
691static bool occurs_check_failure(struct type *tyvar,
692 struct type *ty,
693 struct srcloc start, struct srcloc end)
693694{
694 static size_t level;
695 print_srcloc_range(start, end, stderr);
696 fprintf(stderr,
697 "Occurs check: "
698 "Cannot construct the infinite type %s = ",
699 ty_var_name(tyvar));
700 print_type(ty, stderr);
701 fputs(".\n", stderr);
702 return false;
703}
695704
696 char buf[level+1];
697 for (size_t i = 0; i < level; i++) buf[i] = ' ';
698 buf[level] = '\0';
699
700 fputs(buf, stderr);
701 fputs("UNIFY(", stderr);
705/* Always returns false. */
706static bool type_mismatch(struct type *ty1, struct type *ty2,
707 struct srcloc start, struct srcloc end)
708{
709 print_srcloc_range(start, end, stderr);
710 fprintf(stderr, "Type mismatch: ");
702711 print_type(ty1, stderr);
703 fputs(", ", stderr);
712 fputs(" ", stderr);
704713 print_type(ty2, stderr);
705 fputs("):\n", stderr);
714 fputs(".\n", stderr);
715 return false;
716}
706717
707 level++;
708 bool rv = unify_types_(ty1, ty2);
709 level--;
710
711 fputs(buf, stderr);
712 fprintf(stderr, "%s(", rv ? "OK" : "ERR");
713 print_type(ty1, stderr);
714 fputs(", ", stderr);
715 print_type(ty2, stderr);
716 fputs(")\n", stderr);
717 return rv;
718static void swap_types(struct type **ty1, struct type **ty2)
719{
720 struct type *ty = *ty2;
721 *ty2 = *ty1;
722 *ty1 = ty;
718723}
719*/
720724
721725static bool unify_types(struct type *ty1, struct type *ty2,
722 struct srcloc start, struct srcloc end)
726 struct srcloc st, struct srcloc end)
723727{
724 if (ty1 == 0 || ty2 == 0) return false;
725728 if (ty1 == ty2) return true;
726 if (type_kind(ty2) == TY_VAR) {
727 struct type *ty = ty2;
728 ty2 = ty1;
729 ty1 = ty;
730 }
729 if (type_kind(ty2) == TY_VAR) swap_types(&ty1, &ty2);
731730 switch (type_kind(ty1)) {
732731 case TY_VAR:
733732 if (type_kind(ty2) != TY_VAR && is_free_tyvar(ty1, ty2)) {
734 print_srcloc_range(start, end, stderr);
735 fprintf(stderr,
736 "Occurs check: "
737 "Cannot construct the infinite type %s = ",
738 ty_var_name(ty1));
739 print_type(ty2, stderr);
740 fputs(".\n", stderr);
741 return false;
733 return occurs_check_failure(ty1, ty2, st, end);
742734 }
743735 ty_var_substitute(ty1, ty2);
744736 return true;
745737 case TY_FUN:
746 if (type_kind(ty2) == TY_FUN) {
747 return unify_types(ty_fun_pty(ty1),
748 ty_fun_pty(ty2),
749 start, end) &&
750 unify_types(ty_fun_rty(ty1),
751 ty_fun_rty(ty2),
752 start, end);
753 }
754 break;
738 if (type_kind(ty2) != TY_FUN) return type_mismatch(ty1, ty2,
739 st, end);
740 return unify_types(ty_fun_pty(ty1), ty_fun_pty(ty2), st, end)
741 &&
742 unify_types(ty_fun_rty(ty1), ty_fun_rty(ty2), st, end)
743 ;
755744 case TY_PAIR:
756 if (type_kind(ty2) == TY_PAIR) {
757 return unify_types(ty_pair_fst(ty1),
758 ty_pair_fst(ty2),
759 start, end) &&
760 unify_types(ty_pair_snd(ty1),
761 ty_pair_snd(ty2),
762 start, end);
763 }
745 if (type_kind(ty2) != TY_PAIR) return type_mismatch(ty1, ty2,
746 st, end);
747 return unify_types(ty_pair_fst(ty1), ty_pair_fst(ty2), st, end)
748 &&
749 unify_types(ty_pair_snd(ty1), ty_pair_snd(ty2), st, end)
750 ;
764751 break;
765752 case TY_NUM:
766 if (type_kind(ty2) == TY_NUM) return true;
753 if (type_kind(ty2) != TY_NUM) return type_mismatch(ty1, ty2,
754 st, end);
755 return true;
767756 }
768 print_srcloc_range(start, end, stderr);
769 fprintf(stderr, "Type mismatch: ");
770 print_type(ty1, stderr);
771 fputs(" ≠ ", stderr);
772 print_type(ty2, stderr);
773 fputs(".\n", stderr);
774 return false;
757 assert(0);
775758}
776759
777760/* Always returns 0. */
767767 return 0;
768768}
769769
770/*
771static struct type *infer_type_(struct term *te);
772static struct type *infer_type(struct term *te)
770/* Always returns 0. */
771static struct type *infer_fail_in(struct term *te,
772 struct term *fte,
773 const char *fte_pos)
773774{
774 static size_t level = 0;
775 char buf[level+1];
776 for (size_t i = 0; i < level; i++) buf[i] = ' ';
777 buf[level] = '\0';
778 fputs(buf, stderr);
779 ++level;
780 struct type *rv = infer_type_(te);
781 --level;
782 fputs(buf, stderr);
775 print_srcloc_range(term_start(fte), term_end(fte), stderr);
776 fprintf(stderr, " in the %s of ", fte_pos);
783777 print_term(te, stderr);
784 fputs(" : ", stderr);
785 print_type(rv, stderr);
786 fputs("\n", stderr);
787 return rv;
788
778 fputs(", namely ", stderr);
779 print_term(fte, stderr);
780 putc('\n', stderr);
781 return 0;
789782}
790*/
791783
784/* Always returns 0. */
785static struct type *infer_fail_in_mu(struct term *te)
786{
787 print_srcloc_range(term_start(te), term_end(te), stderr);
788 fputs(" in ", stderr);
789 print_term(te, stderr);
790 fprintf(stderr, " (standing for the recursive equation %s = ",
791 te_mu_var(te));
792 print_term(te_mu_body(te), stderr);
793 fputs(")\n", stderr);
794 return 0;
795}
796
797static struct type *undefined_variable(struct term *te)
798{
799 print_srcloc_range(term_start(te), term_end(te), stderr);
800 fprintf(stderr, "Undefined variable '%s'.\n", te_var_name(te));
801 return 0;
802}
803
792804static struct type *infer_type(struct term *te)
793805{
794806 switch (term_kind(te)) {
808808 struct type *ty, *ty1, *ty2;
809809 case TE_VAR:
810810 ptype = lookup_type(te_var_name(te));
811 if (ptype == 0) {
812 fprintf(stderr, "%s:%d: Undefined variable '%s'.\n",
813 term_start(te).fname, term_start(te).line,
814 te_var_name(te));
815 return 0;
816 }
811 if (ptype == 0) return undefined_variable(te);
817812 return polytype_instantiate(ptype);
818813 case TE_FST:
819814 ty1 = make_ty_var();
827827 if (!unify_types(ty1, ty,
828828 term_start(te_add_left(te)),
829829 term_end(te_add_left(te)))) {
830 struct term *fte = te_add_left(te);
831 print_srcloc_range(term_start(fte),
832 term_end(fte),
833 stderr);
834 fputs(" in the left operand of ", stderr);
835 print_term(te, stderr);
836 fputs(", namely ", stderr);
837 print_term(fte, stderr);
838 putc('\n', stderr);
839 return 0;
830 return infer_fail_in(te, te_add_left(te),
831 "left operand");
840832 }
841833 ty2 = infer_type(te_add_right(te));
842834 if (ty2 == 0) return infer_fail_at(te);
843835 if (!unify_types(ty2, ty,
844836 term_start(te_add_right(te)),
845837 term_end(te_add_right(te)))) {
846 struct term *fte = te_add_right(te);
847 print_srcloc_range(term_start(fte),
848 term_end(fte),
849 stderr);
850 fputs(" in the right operand of ", stderr);
851 print_term(te, stderr);
852 fputs(", namely ", stderr);
853 print_term(fte, stderr);
854 putc('\n', stderr);
855 return 0;
838 return infer_fail_in(te, te_add_right(te),
839 "right operand");
856840 }
857841 return ty;
858842 case TE_APP:
845845 ty2 = infer_type(te_app_arg(te));
846846 if (ty2 == 0) return infer_fail_at(te);
847847 ty = make_ty_var();
848 if (unify_types(ty1, make_ty_fun(ty2, ty),
849 term_start(te_app_fun(te)),
850 term_end(te_app_fun(te)))) {
851 return ty;
852 } else {
853 struct term *fte = te_app_fun(te);
854 print_srcloc_range(term_start(fte),
855 term_end(fte),
856 stderr);
857 fputs(" in the function part of ", stderr);
858 print_term(te, stderr);
859 fputs(", namely ", stderr);
860 print_term(fte, stderr);
861 putc('\n', stderr);
862 return 0;
848 if (!unify_types(ty1, make_ty_fun(ty2, ty),
849 term_start(te_app_fun(te)),
850 term_end(te_app_fun(te)))) {
851 return infer_fail_in(te, te_app_fun(te),
852 "function part");
863853 }
854 return ty;
864855 case TE_PAIR:
865856 ty1 = infer_type(te_pair_fst(te));
866857 if (ty1 == 0) return infer_fail_at(te);
869869 case TE_LET:
870870 ty1 = infer_type(te_let_def(te));
871871 ptype = make_polytype(ty1, true);
872/*
873 fprintf(stderr, "GENERALIZE %s : ", te_let_var(te));
874 print_polytype(ptype, stderr);
875 fputs(" WITHIN ", stderr);
876 print_term(te, stderr);
877 fputc('\n', stderr);
878 fputs("ENVIRONMENT:\n", stderr);
879 for (struct binding_iterator *it = local_bindings_begin();
880 !local_bindings_end(it); local_bindings_next(it)) {
881 const char *var = local_binding_name(it);
882 struct polytype *pt = lookup_type(var);
883 fprintf(stderr, "\t%s : ", var);
884 print_polytype(pt, stderr);
885 fputc('\n', stderr);
886 }
887*/
888872 bind_locally(te_let_var(te), 0, ptype);
889873 ty = infer_type(te_let_body(te));
890874 undo_local_binding(te_let_var(te), 0, ptype);
881881 ty2 = infer_type(te_mu_body(te));
882882 undo_local_binding(te_mu_var(te), 0, ptype);
883883 if (ty2 == 0) return infer_fail_at(te);
884 if (unify_types(ty1, ty2, term_start(te), term_end(te))) {
885 return ty1;
886 } else {
887 print_srcloc_range(term_start(te),
888 term_end(te),
889 stderr);
890 fputs(" in ", stderr);
891 print_term(te, stderr);
892 fprintf(stderr,
893 " (standing for the recursive equation %s = ",
894 te_mu_var(te));
895 print_term(te_mu_body(te), stderr);
896 fputs(")\n", stderr);
897 return 0;
884 if (!unify_types(ty1, ty2, term_start(te), term_end(te))) {
885 return infer_fail_in_mu(te);
898886 }
887 return ty1;
899888 }
900889 assert(0);
901890}