115 val functrans = (map (fn (_, (_, f)) => f thy) o #functrans |
115 val functrans = (map (fn (_, (_, f)) => f thy) o #functrans |
116 o the_thmproc) thy; |
116 o the_thmproc) thy; |
117 in |
117 in |
118 eqns |
118 eqns |
119 |> apply_functrans thy c functrans |
119 |> apply_functrans thy c functrans |
120 |> (map o apfst) (Code_Unit.rewrite_eqn pre) |
120 |> (map o apfst) (Code.rewrite_eqn pre) |
121 |> (map o apfst) (AxClass.unoverload thy) |
121 |> (map o apfst) (AxClass.unoverload thy) |
122 |> map (Code.assert_eqn thy) |
122 |> map (Code.assert_eqn thy) |
123 |> burrow_fst (Code_Unit.norm_args thy) |
123 |> burrow_fst (Code.norm_args thy) |
124 |> burrow_fst (Code_Unit.norm_varnames thy) |
124 |> burrow_fst (Code.norm_varnames thy) |
125 end; |
125 end; |
126 |
126 |
127 fun preprocess_conv thy ct = |
127 fun preprocess_conv thy ct = |
128 let |
128 let |
129 val pre = (Simplifier.theory_context thy o #pre o the_thmproc) thy; |
129 val pre = (Simplifier.theory_context thy o #pre o the_thmproc) thy; |
184 fun typ eqngr = fst o Graph.get_node eqngr; |
184 fun typ eqngr = fst o Graph.get_node eqngr; |
185 fun all eqngr = Graph.keys eqngr; |
185 fun all eqngr = Graph.keys eqngr; |
186 |
186 |
187 fun pretty thy eqngr = |
187 fun pretty thy eqngr = |
188 AList.make (snd o Graph.get_node eqngr) (Graph.keys eqngr) |
188 AList.make (snd o Graph.get_node eqngr) (Graph.keys eqngr) |
189 |> (map o apfst) (Code_Unit.string_of_const thy) |
189 |> (map o apfst) (Code.string_of_const thy) |
190 |> sort (string_ord o pairself fst) |
190 |> sort (string_ord o pairself fst) |
191 |> map (fn (s, thms) => |
191 |> map (fn (s, thms) => |
192 (Pretty.block o Pretty.fbreaks) ( |
192 (Pretty.block o Pretty.fbreaks) ( |
193 Pretty.str s |
193 Pretty.str s |
194 :: map (Display.pretty_thm o fst) thms |
194 :: map (Display.pretty_thm o fst) thms |
214 (map (op :: o swap o apfst (snd o strip_comb) o Logic.dest_equals o Thm.plain_prop_of o fst) eqns); |
214 (map (op :: o swap o apfst (snd o strip_comb) o Logic.dest_equals o Thm.plain_prop_of o fst) eqns); |
215 |
215 |
216 fun tyscm_rhss_of thy c eqns = |
216 fun tyscm_rhss_of thy c eqns = |
217 let |
217 let |
218 val tyscm = case eqns of [] => Code.default_typscheme thy c |
218 val tyscm = case eqns of [] => Code.default_typscheme thy c |
219 | ((thm, _) :: _) => Code_Unit.typscheme_eqn thy thm; |
219 | ((thm, _) :: _) => Code.typscheme_eqn thy thm; |
220 val rhss = consts_of thy eqns; |
220 val rhss = consts_of thy eqns; |
221 in (tyscm, rhss) end; |
221 in (tyscm, rhss) end; |
222 |
222 |
223 |
223 |
224 (* data structures *) |
224 (* data structures *) |
392 val lhs = map_index (fn (k, (v, _)) => |
392 val lhs = map_index (fn (k, (v, _)) => |
393 (v, snd (Vargraph.get_node vardeps (Fun c, k)))) proto_lhs; |
393 (v, snd (Vargraph.get_node vardeps (Fun c, k)))) proto_lhs; |
394 val inst_tab = Vartab.empty |> fold (fn (v, sort) => |
394 val inst_tab = Vartab.empty |> fold (fn (v, sort) => |
395 Vartab.update ((v, 0), sort)) lhs; |
395 Vartab.update ((v, 0), sort)) lhs; |
396 val eqns = proto_eqns |
396 val eqns = proto_eqns |
397 |> (map o apfst) (Code_Unit.inst_thm thy inst_tab); |
397 |> (map o apfst) (Code.inst_thm thy inst_tab); |
398 val (tyscm, rhss') = tyscm_rhss_of thy c eqns; |
398 val (tyscm, rhss') = tyscm_rhss_of thy c eqns; |
399 val eqngr' = Graph.new_node (c, (tyscm, eqns)) eqngr; |
399 val eqngr' = Graph.new_node (c, (tyscm, eqns)) eqngr; |
400 in (map (pair c) rhss' @ rhss, eqngr') end; |
400 in (map (pair c) rhss' @ rhss, eqngr') end; |
401 |
401 |
402 fun extend_arities_eqngr thy cs ts (arities, eqngr) = |
402 fun extend_arities_eqngr thy cs ts (arities, eqngr) = |