16 val unyxml : string -> string |
16 val unyxml : string -> string |
17 val maybe_quote : string -> string |
17 val maybe_quote : string -> string |
18 val typ_of_dtyp : |
18 val typ_of_dtyp : |
19 Datatype_Aux.descr -> (Datatype_Aux.dtyp * typ) list -> Datatype_Aux.dtyp |
19 Datatype_Aux.descr -> (Datatype_Aux.dtyp * typ) list -> Datatype_Aux.dtyp |
20 -> typ |
20 -> typ |
|
21 val varify_type : Proof.context -> typ -> typ |
|
22 val instantiate_type : theory -> typ -> typ -> typ -> typ |
|
23 val varify_and_instantiate_type : Proof.context -> typ -> typ -> typ -> typ |
21 val monomorphic_term : Type.tyenv -> term -> term |
24 val monomorphic_term : Type.tyenv -> term -> term |
22 val eta_expand : typ list -> term -> int -> term |
25 val eta_expand : typ list -> term -> int -> term |
23 val transform_elim_term : term -> term |
26 val transform_elim_term : term -> term |
24 val specialize_type : theory -> (string * typ) -> term -> term |
27 val specialize_type : theory -> (string * typ) -> term -> term |
25 val subgoal_count : Proof.state -> int |
28 val subgoal_count : Proof.state -> int |
90 | typ_of_dtyp descr typ_assoc (Datatype_Aux.DtRec i) = |
93 | typ_of_dtyp descr typ_assoc (Datatype_Aux.DtRec i) = |
91 let val (s, ds, _) = the (AList.lookup (op =) descr i) in |
94 let val (s, ds, _) = the (AList.lookup (op =) descr i) in |
92 Type (s, map (typ_of_dtyp descr typ_assoc) ds) |
95 Type (s, map (typ_of_dtyp descr typ_assoc) ds) |
93 end |
96 end |
94 |
97 |
|
98 fun varify_type ctxt T = |
|
99 Variable.polymorphic_types ctxt [Const (@{const_name undefined}, T)] |
|
100 |> snd |> the_single |> dest_Const |> snd |
|
101 |
|
102 (* TODO: use "Term_Subst.instantiateT" instead? *) |
|
103 fun instantiate_type thy T1 T1' T2 = |
|
104 Same.commit (Envir.subst_type_same |
|
105 (Sign.typ_match thy (T1, T1') Vartab.empty)) T2 |
|
106 handle Type.TYPE_MATCH => raise TYPE ("instantiate_type", [T1, T1'], []) |
|
107 |
|
108 fun varify_and_instantiate_type ctxt T1 T1' T2 = |
|
109 let val thy = Proof_Context.theory_of ctxt in |
|
110 instantiate_type thy (varify_type ctxt T1) T1' (varify_type ctxt T2) |
|
111 end |
|
112 |
95 fun monomorphic_term subst t = |
113 fun monomorphic_term subst t = |
96 map_types (map_type_tvar (fn v => |
114 map_types (map_type_tvar (fn v => |
97 case Type.lookup subst v of |
115 case Type.lookup subst v of |
98 SOME typ => typ |
116 SOME typ => typ |
99 | NONE => raise TERM ("monomorphic_term: uninstanitated schematic type \ |
117 | NONE => raise TERM ("monomorphic_term: uninstanitated schematic type \ |