--- a/src/Pure/Tools/codegen_funcgr.ML Fri Jan 05 14:31:49 2007 +0100
+++ b/src/Pure/Tools/codegen_funcgr.ML Fri Jan 05 14:31:50 2007 +0100
@@ -16,7 +16,6 @@
val deps: T -> CodegenConsts.const list -> CodegenConsts.const list list
val all: T -> CodegenConsts.const list
val norm_varnames: theory -> thm list -> thm list
- val expand_eta: theory -> int -> thm -> thm
val print_codethms: theory -> CodegenConsts.const list -> unit
structure Constgraph : GRAPH
end;
@@ -51,42 +50,13 @@
(** theorem purification **)
-fun expand_eta thy k thm =
- let
- val (lhs, rhs) = (Logic.dest_equals o Drule.plain_prop_of) thm;
- val (head, args) = strip_comb lhs;
- val l = Int.max (0, k - length args);
- val used = Name.make_context (map (fst o fst) (Term.add_vars lhs []));
- fun get_name _ 0 used = ([], used)
- | get_name (Abs (v, ty, t)) k used =
- used
- |> Name.variants [CodegenNames.purify_var v]
- ||>> get_name t (k - 1)
- |>> (fn ([v'], vs') => (v', ty) :: vs')
- | get_name t k used =
- let
- val (tys, _) = (strip_type o fastype_of) t
- in case tys
- of [] => raise TERM ("expand_eta", [t])
- | ty :: _ =>
- used
- |> Name.variants [""]
- |-> (fn [v] => get_name (t $ Var ((v, 0), ty)) (k - 1)
- #>> (fn vs' => (v, ty) :: vs'))
- end;
- val (vs, _) = get_name rhs l used;
- val vs_refl = map (fn (v, ty) => Thm.reflexive (Thm.cterm_of thy (Var ((v, 0), ty)))) vs;
- in
- fold (fn refl => fn thm => Thm.combination thm refl) vs_refl thm
- end;
-
fun norm_args thy thms =
let
val num_args_of = length o snd o strip_comb o fst o Logic.dest_equals;
val k = fold (curry Int.max o num_args_of o Drule.plain_prop_of) thms 0;
in
thms
- |> map (expand_eta thy k)
+ |> map (CodegenFunc.expand_eta thy k)
|> map (Drule.fconv_rule Drule.beta_eta_conversion)
end;
--- a/src/Pure/Tools/codegen_package.ML Fri Jan 05 14:31:49 2007 +0100
+++ b/src/Pure/Tools/codegen_package.ML Fri Jan 05 14:31:50 2007 +0100
@@ -93,7 +93,7 @@
val ty = (Logic.unvarifyT o CodegenData.typ_func thy) thm;
val thms' = if (null o Term.typ_tfrees) ty orelse (null o fst o strip_type) ty
then thms
- else map (CodegenFuncgr.expand_eta thy 1) thms;
+ else map (CodegenFunc.expand_eta thy 1) thms;
in (ty, thms') end;