751 val dups = duplicates (eq_fst op =) vars; |
751 val dups = duplicates (eq_fst op =) vars; |
752 val _ = null dups orelse |
752 val _ = null dups orelse |
753 raise THM ("infer_instantiate: inconsistent types for variables " ^ |
753 raise THM ("infer_instantiate: inconsistent types for variables " ^ |
754 commas_quote (map (Syntax.string_of_term (Config.put show_types true ctxt) o Var) dups), |
754 commas_quote (map (Syntax.string_of_term (Config.put show_types true ctxt) o Var) dups), |
755 0, [th]); |
755 0, [th]); |
756 fun var_type xi = |
756 |
|
757 fun infer (xi, cu) (inst, tyenv, maxidx) = |
757 (case AList.lookup (op =) vars xi of |
758 (case AList.lookup (op =) vars xi of |
758 SOME T => T |
759 NONE => (inst, tyenv, maxidx) |
759 | NONE => raise THM ("infer_instantiate: no variable " ^ string_of_indexname xi, 0, [th])); |
760 | SOME T => |
760 |
761 let |
761 fun infer (xi, cu) (tyenv, maxidx) = |
762 val U = Thm.typ_of_cterm cu; |
762 let |
763 val maxidx' = maxidx |
763 val T = var_type xi; |
764 |> Integer.max (#2 xi) |
764 val U = Thm.typ_of_cterm cu; |
765 |> Term.maxidx_typ T |
765 val maxidx' = maxidx |
766 |> Integer.max (Thm.maxidx_of_cterm cu); |
766 |> Integer.max (#2 xi) |
767 val (tyenv', maxidx'') = Sign.typ_unify thy (T, U) (tyenv, maxidx') |
767 |> Term.maxidx_typ T |
768 handle Type.TUNIFY => |
768 |> Integer.max (Thm.maxidx_of_cterm cu); |
769 let |
769 val (tyenv', maxidx'') = Sign.typ_unify thy (T, U) (tyenv, maxidx') |
770 val t = Var (xi, T); |
770 handle Type.TUNIFY => |
771 val u = Thm.term_of cu; |
771 let |
772 in |
772 val t = Var (xi, T); |
773 raise THM ("infer_instantiate: type " ^ |
773 val u = Thm.term_of cu; |
774 Syntax.string_of_typ ctxt (Envir.norm_type tyenv T) ^ " of variable " ^ |
774 in |
775 Syntax.string_of_term ctxt (Term.map_types (Envir.norm_type tyenv) t) ^ |
775 raise THM ("infer_instantiate: type " ^ |
776 "\ncannot be unified with type " ^ |
776 Syntax.string_of_typ ctxt (Envir.norm_type tyenv T) ^ " of variable " ^ |
777 Syntax.string_of_typ ctxt (Envir.norm_type tyenv U) ^ " of term " ^ |
777 Syntax.string_of_term ctxt (Term.map_types (Envir.norm_type tyenv) t) ^ |
778 Syntax.string_of_term ctxt (Term.map_types (Envir.norm_type tyenv) u), |
778 "\ncannot be unified with type " ^ |
779 0, [th]) |
779 Syntax.string_of_typ ctxt (Envir.norm_type tyenv U) ^ " of term " ^ |
780 end; |
780 Syntax.string_of_term ctxt (Term.map_types (Envir.norm_type tyenv) u), |
781 in (((xi, T), cu) :: inst, tyenv', maxidx'') end); |
781 0, [th]) |
782 |
782 end; |
783 val (inst0, tyenv, _) = fold infer args ([], Vartab.empty, 0); |
783 in (((xi, T), cu), (tyenv', maxidx'')) end; |
|
784 |
|
785 val (args', (tyenv, _)) = fold_map infer args (Vartab.empty, 0); |
|
786 val instT = |
784 val instT = |
787 Vartab.fold (fn (xi, (S, T)) => |
785 Vartab.fold (fn (xi, (S, T)) => |
788 cons ((xi, S), Thm.ctyp_of ctxt (Envir.norm_type tyenv T))) tyenv []; |
786 cons ((xi, S), Thm.ctyp_of ctxt (Envir.norm_type tyenv T))) tyenv []; |
789 val inst = args' |> map (fn ((xi, T), cu) => |
787 val inst = inst0 |> map (fn ((xi, T), cu) => |
790 ((xi, Envir.norm_type tyenv T), |
788 ((xi, Envir.norm_type tyenv T), |
791 Thm.instantiate_cterm (instT, []) (Thm.transfer_cterm thy cu))); |
789 Thm.instantiate_cterm (instT, []) (Thm.transfer_cterm thy cu))); |
792 in instantiate_normalize (instT, inst) th end |
790 in instantiate_normalize (instT, inst) th end |
793 handle CTERM (msg, _) => raise THM (msg, 0, [th]) |
791 handle CTERM (msg, _) => raise THM (msg, 0, [th]) |
794 | TERM (msg, _) => raise THM (msg, 0, [th]) |
792 | TERM (msg, _) => raise THM (msg, 0, [th]) |