equal
deleted
inserted
replaced
504 and of_univ bounds (Const (idx, ts)) typidx = |
504 and of_univ bounds (Const (idx, ts)) typidx = |
505 let |
505 let |
506 val ts' = take_until is_dict ts; |
506 val ts' = take_until is_dict ts; |
507 val c = const_of_idx idx; |
507 val c = const_of_idx idx; |
508 val T = map_type_tvar (fn ((v, i), _) => |
508 val T = map_type_tvar (fn ((v, i), _) => |
509 TypeInfer.param typidx (v ^ string_of_int i, [])) |
509 Type_Infer.param typidx (v ^ string_of_int i, [])) |
510 (Sign.the_const_type thy c); |
510 (Sign.the_const_type thy c); |
511 val typidx' = typidx + 1; |
511 val typidx' = typidx + 1; |
512 in of_apps bounds (Term.Const (c, T), ts') typidx' end |
512 in of_apps bounds (Term.Const (c, T), ts') typidx' end |
513 | of_univ bounds (BVar (n, ts)) typidx = |
513 | of_univ bounds (BVar (n, ts)) typidx = |
514 of_apps bounds (Bound (bounds - n - 1), ts) typidx |
514 of_apps bounds (Bound (bounds - n - 1), ts) typidx |
546 |
546 |
547 fun normalize thy program ((vs0, (vs, ty)), t) deps = |
547 fun normalize thy program ((vs0, (vs, ty)), t) deps = |
548 let |
548 let |
549 val ty' = typ_of_itype program vs0 ty; |
549 val ty' = typ_of_itype program vs0 ty; |
550 fun type_infer t = |
550 fun type_infer t = |
551 singleton (TypeInfer.infer_types (Syntax.pp_global thy) (Sign.tsig_of thy) I |
551 singleton (Type_Infer.infer_types (Syntax.pp_global thy) (Sign.tsig_of thy) I |
552 (try (Type.strip_sorts o Sign.the_const_type thy)) (K NONE) Name.context 0) |
552 (try (Type.strip_sorts o Sign.the_const_type thy)) (K NONE) Name.context 0) |
553 (TypeInfer.constrain ty' t); |
553 (Type_Infer.constrain ty' t); |
554 fun check_tvars t = if null (Term.add_tvars t []) then t else |
554 fun check_tvars t = if null (Term.add_tvars t []) then t else |
555 error ("Illegal schematic type variables in normalized term: " |
555 error ("Illegal schematic type variables in normalized term: " |
556 ^ setmp_CRITICAL show_types true (Syntax.string_of_term_global thy) t); |
556 ^ setmp_CRITICAL show_types true (Syntax.string_of_term_global thy) t); |
557 val string_of_term = setmp_CRITICAL show_types true (Syntax.string_of_term_global thy); |
557 val string_of_term = setmp_CRITICAL show_types true (Syntax.string_of_term_global thy); |
558 in |
558 in |