100 |> perhaps (perhaps_loop (perhaps_apply functrans)) |
100 |> perhaps (perhaps_loop (perhaps_apply functrans)) |
101 |> Code.assert_eqns_const thy c; |
101 |> Code.assert_eqns_const thy c; |
102 |
102 |
103 fun rhs_conv conv thm = Thm.transitive thm ((conv o Thm.rhs_of) thm); |
103 fun rhs_conv conv thm = Thm.transitive thm ((conv o Thm.rhs_of) thm); |
104 |
104 |
|
105 fun eqn_conv conv = |
|
106 let |
|
107 fun lhs_conv ct = if can Thm.dest_comb ct |
|
108 then Conv.combination_conv lhs_conv conv ct |
|
109 else Conv.all_conv ct; |
|
110 in Conv.combination_conv (Conv.arg_conv lhs_conv) conv end; |
|
111 |
|
112 val rewrite_eqn = Conv.fconv_rule o eqn_conv o Simplifier.rewrite; |
|
113 |
105 fun term_of_conv thy f = |
114 fun term_of_conv thy f = |
106 Thm.cterm_of thy |
115 Thm.cterm_of thy |
107 #> f |
116 #> f |
108 #> Thm.prop_of |
117 #> Thm.prop_of |
109 #> Logic.dest_equals |
118 #> Logic.dest_equals |
115 val functrans = (map (fn (_, (_, f)) => f thy) o #functrans |
124 val functrans = (map (fn (_, (_, f)) => f thy) o #functrans |
116 o the_thmproc) thy; |
125 o the_thmproc) thy; |
117 in |
126 in |
118 eqns |
127 eqns |
119 |> apply_functrans thy c functrans |
128 |> apply_functrans thy c functrans |
120 |> (map o apfst) (Code.rewrite_eqn pre) |
129 |> (map o apfst) (rewrite_eqn pre) |
121 |> (map o apfst) (AxClass.unoverload thy) |
130 |> (map o apfst) (AxClass.unoverload thy) |
122 |> map (Code.assert_eqn thy) |
131 |> map (Code.assert_eqn thy) |
123 |> burrow_fst (Code.norm_args thy) |
132 |> burrow_fst (Code.norm_args thy) |
124 |> burrow_fst (Code.norm_varnames thy) |
133 |> burrow_fst (Code.norm_varnames thy) |
125 end; |
134 end; |
211 |
220 |
212 fun consts_of thy eqns = [] |> (fold o fold o fold_aterms) |
221 fun consts_of thy eqns = [] |> (fold o fold o fold_aterms) |
213 (fn Const (c, ty) => insert (op =) (c, Sign.const_typargs thy (c, Logic.unvarifyT ty)) | _ => I) |
222 (fn Const (c, ty) => insert (op =) (c, Sign.const_typargs thy (c, Logic.unvarifyT ty)) | _ => I) |
214 (map (op :: o swap o apfst (snd o strip_comb) o Logic.dest_equals o Thm.plain_prop_of o fst) eqns); |
223 (map (op :: o swap o apfst (snd o strip_comb) o Logic.dest_equals o Thm.plain_prop_of o fst) eqns); |
215 |
224 |
|
225 fun default_typscheme_of thy c = |
|
226 let |
|
227 val ty = (snd o dest_Const o TermSubst.zero_var_indexes o curry Const c |
|
228 o Type.strip_sorts o Sign.the_const_type thy) c; |
|
229 in case AxClass.class_of_param thy c |
|
230 of SOME class => ([(Name.aT, [class])], ty) |
|
231 | NONE => Code.typscheme thy (c, ty) |
|
232 end; |
|
233 |
216 fun tyscm_rhss_of thy c eqns = |
234 fun tyscm_rhss_of thy c eqns = |
217 let |
235 let |
218 val tyscm = case eqns of [] => Code.default_typscheme thy c |
236 val tyscm = case eqns |
|
237 of [] => default_typscheme_of thy c |
219 | ((thm, _) :: _) => Code.typscheme_eqn thy thm; |
238 | ((thm, _) :: _) => Code.typscheme_eqn thy thm; |
220 val rhss = consts_of thy eqns; |
239 val rhss = consts_of thy eqns; |
221 in (tyscm, rhss) end; |
240 in (tyscm, rhss) end; |
222 |
241 |
223 |
242 |
379 { class_relation = class_relation, type_constructor = type_constructor, |
398 { class_relation = class_relation, type_constructor = type_constructor, |
380 type_variable = type_variable } (T, proj_sort sort) |
399 type_variable = type_variable } (T, proj_sort sort) |
381 handle Sorts.CLASS_ERROR _ => [] (*permissive!*)) |
400 handle Sorts.CLASS_ERROR _ => [] (*permissive!*)) |
382 end; |
401 end; |
383 |
402 |
|
403 fun inst_thm thy tvars' thm = |
|
404 let |
|
405 val tvars = (Term.add_tvars o Thm.prop_of) thm []; |
|
406 val inter_sort = Sorts.inter_sort (Sign.classes_of thy); |
|
407 fun mk_inst (tvar as (v, sort)) = case Vartab.lookup tvars' v |
|
408 of SOME sort' => SOME (pairself (Thm.ctyp_of thy o TVar) |
|
409 (tvar, (v, inter_sort (sort, sort')))) |
|
410 | NONE => NONE; |
|
411 val insts = map_filter mk_inst tvars; |
|
412 in Thm.instantiate (insts, []) thm end; |
|
413 |
384 fun add_arity thy vardeps (class, tyco) = |
414 fun add_arity thy vardeps (class, tyco) = |
385 AList.default (op =) |
415 AList.default (op =) |
386 ((class, tyco), map (fn k => (snd o Vargraph.get_node vardeps) (Inst (class, tyco), k)) |
416 ((class, tyco), map (fn k => (snd o Vargraph.get_node vardeps) (Inst (class, tyco), k)) |
387 (0 upto Sign.arity_number thy tyco - 1)); |
417 (0 upto Sign.arity_number thy tyco - 1)); |
388 |
418 |
392 val lhs = map_index (fn (k, (v, _)) => |
422 val lhs = map_index (fn (k, (v, _)) => |
393 (v, snd (Vargraph.get_node vardeps (Fun c, k)))) proto_lhs; |
423 (v, snd (Vargraph.get_node vardeps (Fun c, k)))) proto_lhs; |
394 val inst_tab = Vartab.empty |> fold (fn (v, sort) => |
424 val inst_tab = Vartab.empty |> fold (fn (v, sort) => |
395 Vartab.update ((v, 0), sort)) lhs; |
425 Vartab.update ((v, 0), sort)) lhs; |
396 val eqns = proto_eqns |
426 val eqns = proto_eqns |
397 |> (map o apfst) (Code.inst_thm thy inst_tab); |
427 |> (map o apfst) (inst_thm thy inst_tab); |
398 val (tyscm, rhss') = tyscm_rhss_of thy c eqns; |
428 val (tyscm, rhss') = tyscm_rhss_of thy c eqns; |
399 val eqngr' = Graph.new_node (c, (tyscm, eqns)) eqngr; |
429 val eqngr' = Graph.new_node (c, (tyscm, eqns)) eqngr; |
400 in (map (pair c) rhss' @ rhss, eqngr') end; |
430 in (map (pair c) rhss' @ rhss, eqngr') end; |
401 |
431 |
402 fun extend_arities_eqngr thy cs ts (arities, eqngr) = |
432 fun extend_arities_eqngr thy cs ts (arities, eqngr) = |