--- a/src/HOL/HOL.thy Tue Aug 07 09:38:48 2007 +0200
+++ b/src/HOL/HOL.thy Tue Aug 07 09:40:34 2007 +0200
@@ -25,6 +25,7 @@
"~~/src/Provers/quantifier1.ML"
("simpdata.ML")
("~~/src/HOL/Tools/recfun_codegen.ML")
+ "~~/src/Tools/nbe.ML"
begin
subsection {* Primitive logic *}
@@ -1540,6 +1541,12 @@
subsection {* Other simple lemmas and lemma duplicates *}
+lemma Let_0 [simp]: "Let 0 f = f 0"
+ unfolding Let_def ..
+
+lemma Let_1 [simp]: "Let 1 f = f 1"
+ unfolding Let_def ..
+
lemma ex1_eq [iff]: "EX! x. x = t" "EX! x. t = x"
by blast+
@@ -1786,9 +1793,13 @@
(OCaml "failwith/ \"undefined\"")
(Haskell "error/ \"undefined\"")
-code_reserved SML Fail
-code_reserved OCaml failwith
+
+text {* Let and If *}
+setup {*
+ CodegenPackage.add_appconst (@{const_name Let}, CodegenPackage.appgen_let)
+ #> CodegenPackage.add_appconst (@{const_name If}, CodegenPackage.appgen_if)
+*}
subsubsection {* Evaluation oracle *}
@@ -1811,31 +1822,15 @@
subsubsection {* Normalization by evaluation *}
+setup Nbe.setup
+
method_setup normalization = {*
Method.no_args (Method.SIMPLE_METHOD'
- (CONVERSION (ObjectLogic.judgment_conv NBE.normalization_conv)
+ (CONVERSION (ObjectLogic.judgment_conv Nbe.normalization_conv)
THEN' resolve_tac [TrueI, refl]))
*} "solve goal by normalization"
-text {* lazy @{const If} *}
-
-definition
- if_delayed :: "bool \<Rightarrow> (bool \<Rightarrow> 'a) \<Rightarrow> (bool \<Rightarrow> 'a) \<Rightarrow> 'a" where
- [code func del]: "if_delayed b f g = (if b then f True else g False)"
-
-lemma [code func]:
- shows "if_delayed True f g = f True"
- and "if_delayed False f g = g False"
- unfolding if_delayed_def by simp_all
-
-lemma [normal pre, symmetric, normal post]:
- "(if b then x else y) = if_delayed b (\<lambda>_. x) (\<lambda>_. y)"
- unfolding if_delayed_def ..
-
-hide (open) const if_delayed
-
-
subsection {* Legacy tactics and ML bindings *}
ML {*
--- a/src/HOL/List.thy Tue Aug 07 09:38:48 2007 +0200
+++ b/src/HOL/List.thy Tue Aug 07 09:40:34 2007 +0200
@@ -757,9 +757,9 @@
lemma set_map [simp]: "set (map f xs) = f`(set xs)"
by (induct xs) auto
-lemma set_allpairs[simp]:
+lemma set_allpairs [simp]:
"set(allpairs f xs ys) = {z. EX x : set xs. EX y : set ys. z = f x y}"
-by(induct xs) auto
+by (induct xs) auto
lemma set_filter [simp]: "set (filter P xs) = {x. x : set xs \<and> P x}"
by (induct xs) auto
@@ -2923,7 +2923,7 @@
show ?case by (induct xs) (auto simp add: Cons aux)
qed
-lemma mem_iff [normal post]:
+lemma mem_iff [code post]:
"x mem xs \<longleftrightarrow> x \<in> set xs"
by (induct xs) auto
@@ -2933,14 +2933,14 @@
"xs = [] \<longleftrightarrow> null xs"
by (cases xs) simp_all
-lemmas null_empty [normal post] =
+lemmas null_empty [code post] =
empty_null [symmetric]
lemma list_inter_conv:
"set (list_inter xs ys) = set xs \<inter> set ys"
by (induct xs) auto
-lemma list_all_iff [normal post]:
+lemma list_all_iff [code post]:
"list_all P xs \<longleftrightarrow> (\<forall>x \<in> set xs. P x)"
by (induct xs) auto
@@ -2958,7 +2958,7 @@
"list_all P xs \<longleftrightarrow> (\<forall>n < length xs. P (xs ! n))"
unfolding list_all_iff by (auto intro: all_nth_imp_all_set)
-lemma list_ex_iff [normal post]:
+lemma list_ex_iff [code post]:
"list_ex P xs \<longleftrightarrow> (\<exists>x \<in> set xs. P x)"
by (induct xs) simp_all
@@ -2978,7 +2978,7 @@
by (induct xs) auto
lemma [code inline]: "listsum (map f xs) = foldl (%n x. n + f x) 0 xs"
-by(simp add:listsum_foldr foldl_map[symmetric] foldl_foldr1)
+ by (simp add: listsum_foldr foldl_map [symmetric] foldl_foldr1)
text {* Code for bounded quantification over nats. *}
--- a/src/HOL/Numeral.thy Tue Aug 07 09:38:48 2007 +0200
+++ b/src/HOL/Numeral.thy Tue Aug 07 09:40:34 2007 +0200
@@ -36,11 +36,11 @@
definition
Pls :: int where
- [code func del]:"Pls = 0"
+ [code func del]: "Pls = 0"
definition
Min :: int where
- [code func del]:"Min = - 1"
+ [code func del]: "Min = - 1"
definition
Bit :: "int \<Rightarrow> bit \<Rightarrow> int" (infixl "BIT" 90) where
@@ -67,12 +67,6 @@
-- {* Unfold all @{text let}s involving constants *}
unfolding Let_def ..
-lemma Let_0 [simp]: "Let 0 f = f 0"
- unfolding Let_def ..
-
-lemma Let_1 [simp]: "Let 1 f = f 1"
- unfolding Let_def ..
-
definition
succ :: "int \<Rightarrow> int" where
[code func del]: "succ k = k + 1"
@@ -94,11 +88,11 @@
text {* Removal of leading zeroes *}
-lemma Pls_0_eq [simp, normal post]:
+lemma Pls_0_eq [simp, code post]:
"Pls BIT B0 = Pls"
unfolding numeral_simps by simp
-lemma Min_1_eq [simp, normal post]:
+lemma Min_1_eq [simp, code post]:
"Min BIT B1 = Min"
unfolding numeral_simps by simp
@@ -613,11 +607,11 @@
lemma [code]: "nat i = nat_aux i 0"
by (simp add: nat_aux_def)
-lemma zero_is_num_zero [code func, code inline, symmetric, normal post]:
+lemma zero_is_num_zero [code func, code inline, symmetric, code post]:
"(0\<Colon>int) = Numeral0"
by simp
-lemma one_is_num_one [code func, code inline, symmetric, normal post]:
+lemma one_is_num_one [code func, code inline, symmetric, code post]:
"(1\<Colon>int) = Numeral1"
by simp
--- a/src/Pure/IsaMakefile Tue Aug 07 09:38:48 2007 +0200
+++ b/src/Pure/IsaMakefile Tue Aug 07 09:40:34 2007 +0200
@@ -63,7 +63,7 @@
Tools/codegen_consts.ML Tools/codegen_data.ML Tools/codegen_func.ML \
Tools/codegen_funcgr.ML Tools/codegen_names.ML Tools/codegen_package.ML \
Tools/codegen_serializer.ML Tools/codegen_thingol.ML Tools/invoke.ML \
- Tools/named_thms.ML Tools/nbe.ML Tools/nbe_codegen.ML Tools/nbe_eval.ML \
+ Tools/named_thms.ML \
Tools/xml.ML Tools/xml_syntax.ML assumption.ML axclass.ML codegen.ML \
compress.ML config.ML conjunction.ML consts.ML context.ML context_position.ML \
conv.ML defs.ML display.ML drule.ML envir.ML fact_index.ML goal.ML library.ML \
--- a/src/Pure/Tools/ROOT.ML Tue Aug 07 09:38:48 2007 +0200
+++ b/src/Pure/Tools/ROOT.ML Tue Aug 07 09:40:34 2007 +0200
@@ -22,8 +22,3 @@
use "codegen_thingol.ML";
use "codegen_serializer.ML";
use "codegen_package.ML";
-
-(*norm-by-eval*)
-use "nbe_eval.ML";
-use "nbe_codegen.ML";
-use "nbe.ML";
--- a/src/Pure/Tools/codegen_data.ML Tue Aug 07 09:38:48 2007 +0200
+++ b/src/Pure/Tools/codegen_data.ML Tue Aug 07 09:40:34 2007 +0200
@@ -21,6 +21,8 @@
val del_inline_proc: string -> theory -> theory
val add_preproc: string * (theory -> thm list -> thm list) -> theory -> theory
val del_preproc: string -> theory -> theory
+ val add_post: thm -> theory -> theory
+ val del_post: thm -> theory -> theory
val add_datatype: string * ((string * sort) list * (string * typ list) list)
-> theory -> theory
val add_datatype_consts: CodegenConsts.const list -> theory -> theory
@@ -33,7 +35,8 @@
val get_datatype_of_constr: theory -> CodegenConsts.const -> string option
val default_typ: theory -> CodegenConsts.const -> typ
- val preprocess_cterm: cterm -> thm
+ val preprocess_conv: cterm -> thm
+ val postprocess_conv: cterm -> thm
val print_codesetup: theory -> unit
@@ -176,24 +179,29 @@
(** exeuctable content **)
-datatype preproc = Preproc of {
+datatype thmproc = Preproc of {
inlines: thm list,
inline_procs: (string * (serial * (theory -> cterm list -> thm list))) list,
- preprocs: (string * (serial * (theory -> thm list -> thm list))) list
+ preprocs: (string * (serial * (theory -> thm list -> thm list))) list,
+ posts: thm list
};
-fun mk_preproc ((inlines, inline_procs), preprocs) =
- Preproc { inlines = inlines, inline_procs = inline_procs, preprocs = preprocs };
-fun map_preproc f (Preproc { inlines, inline_procs, preprocs }) =
- mk_preproc (f ((inlines, inline_procs), preprocs));
-fun merge_preproc (Preproc { inlines = inlines1, inline_procs = inline_procs1, preprocs = preprocs1 },
- Preproc { inlines = inlines2, inline_procs = inline_procs2, preprocs = preprocs2 }) =
+fun mk_thmproc (((inlines, inline_procs), preprocs), posts) =
+ Preproc { inlines = inlines, inline_procs = inline_procs, preprocs = preprocs,
+ posts = posts };
+fun map_thmproc f (Preproc { inlines, inline_procs, preprocs, posts }) =
+ mk_thmproc (f (((inlines, inline_procs), preprocs), posts));
+fun merge_thmproc (Preproc { inlines = inlines1, inline_procs = inline_procs1,
+ preprocs = preprocs1, posts = posts1 },
+ Preproc { inlines = inlines2, inline_procs = inline_procs2,
+ preprocs = preprocs2, posts= posts2 }) =
let
val (touched1, inlines) = merge_thms (inlines1, inlines2);
val (touched2, inline_procs) = merge_alist (op =) (eq_fst (op =)) (inline_procs1, inline_procs2);
val (touched3, preprocs) = merge_alist (op =) (eq_fst (op =)) (preprocs1, preprocs2);
+ val (_, posts) = merge_thms (posts1, posts2);
in (touched1 orelse touched2 orelse touched3,
- mk_preproc ((inlines, inline_procs), preprocs)) end;
+ mk_thmproc (((inlines, inline_procs), preprocs), posts)) end;
fun join_func_thms (tabs as (tab1, tab2)) =
let
@@ -246,29 +254,29 @@
in (touched, mk_spec (funcs, dtyps)) end;
datatype exec = Exec of {
- preproc: preproc,
+ thmproc: thmproc,
spec: spec
};
-fun mk_exec (preproc, spec) =
- Exec { preproc = preproc, spec = spec };
-fun map_exec f (Exec { preproc = preproc, spec = spec }) =
- mk_exec (f (preproc, spec));
-fun merge_exec (Exec { preproc = preproc1, spec = spec1 },
- Exec { preproc = preproc2, spec = spec2 }) =
+fun mk_exec (thmproc, spec) =
+ Exec { thmproc = thmproc, spec = spec };
+fun map_exec f (Exec { thmproc = thmproc, spec = spec }) =
+ mk_exec (f (thmproc, spec));
+fun merge_exec (Exec { thmproc = thmproc1, spec = spec1 },
+ Exec { thmproc = thmproc2, spec = spec2 }) =
let
- val (touched', preproc) = merge_preproc (preproc1, preproc2);
+ val (touched', thmproc) = merge_thmproc (thmproc1, thmproc2);
val (touched_cs, spec) = merge_spec (spec1, spec2);
val touched = if touched' then NONE else touched_cs;
- in (touched, mk_exec (preproc, spec)) end;
-val empty_exec = mk_exec (mk_preproc (([], []), []),
+ in (touched, mk_exec (thmproc, spec)) end;
+val empty_exec = mk_exec (mk_thmproc ((([], []), []), []),
mk_spec (Consttab.empty, Symtab.empty));
-fun the_preproc (Exec { preproc = Preproc x, ...}) = x;
+fun the_thmproc (Exec { thmproc = Preproc x, ...}) = x;
fun the_spec (Exec { spec = Spec x, ...}) = x;
val the_funcs = #funcs o the_spec;
val the_dtyps = #dtyps o the_spec;
-val map_preproc = map_exec o apfst o map_preproc;
+val map_thmproc = map_exec o apfst o map_thmproc;
val map_funcs = map_exec o apsnd o map_spec o apfst;
val map_dtyps = map_exec o apsnd o map_spec o apsnd;
@@ -404,9 +412,9 @@
(Pretty.block o Pretty.breaks)
(Pretty.str c :: Pretty.str "of" :: map (Pretty.quote o Sign.pretty_typ thy) tys)) cos)
);
- val inlines = (#inlines o the_preproc) exec;
- val inline_procs = (map fst o #inline_procs o the_preproc) exec;
- val preprocs = (map fst o #preprocs o the_preproc) exec;
+ val inlines = (#inlines o the_thmproc) exec;
+ val inline_procs = (map fst o #inline_procs o the_thmproc) exec;
+ val preprocs = (map fst o #preprocs o the_thmproc) exec;
val funs = the_funcs exec
|> Consttab.dest
|> (map o apfst) (CodegenConsts.string_of_const thy)
@@ -695,32 +703,43 @@
end; (*local*)
fun add_inline thm thy =
- (map_exec_purge NONE o map_preproc o apfst o apfst)
+ (map_exec_purge NONE o map_thmproc o apfst o apfst o apfst)
(insert Thm.eq_thm_prop (CodegenFunc.error_thm CodegenFunc.mk_rew thm)) thy;
(*fully applied in order to get right context for mk_rew!*)
fun del_inline thm thy =
- (map_exec_purge NONE o map_preproc o apfst o apfst)
+ (map_exec_purge NONE o map_thmproc o apfst o apfst o apfst)
(remove Thm.eq_thm_prop (CodegenFunc.error_thm CodegenFunc.mk_rew thm)) thy;
(*fully applied in order to get right context for mk_rew!*)
fun add_inline_proc (name, f) =
- (map_exec_purge NONE o map_preproc o apfst o apsnd)
+ (map_exec_purge NONE o map_thmproc o apfst o apfst o apsnd)
(AList.update (op =) (name, (serial (), f)));
fun del_inline_proc name =
- (map_exec_purge NONE o map_preproc o apfst o apsnd)
+ (map_exec_purge NONE o map_thmproc o apfst o apfst o apsnd)
(delete_force "inline procedure" name);
fun add_preproc (name, f) =
- (map_exec_purge NONE o map_preproc o apsnd) (AList.update (op =) (name, (serial (), f)));
+ (map_exec_purge NONE o map_thmproc o apfst o apsnd)
+ (AList.update (op =) (name, (serial (), f)));
fun del_preproc name =
- (map_exec_purge NONE o map_preproc o apsnd) (delete_force "preprocessor" name);
+ (map_exec_purge NONE o map_thmproc o apfst o apsnd)
+ (delete_force "preprocessor" name);
+
+fun add_post thm thy =
+ (map_exec_purge NONE o map_thmproc o apsnd)
+ (insert Thm.eq_thm_prop (CodegenFunc.error_thm CodegenFunc.mk_rew thm)) thy;
+ (*fully applied in order to get right context for mk_rew!*)
+
+fun del_post thm thy =
+ (map_exec_purge NONE o map_thmproc o apsnd)
+ (remove Thm.eq_thm_prop (CodegenFunc.error_thm CodegenFunc.mk_rew thm)) thy;
+ (*fully applied in order to get right context for mk_rew!*)
-
-(** retrieval **)
+(** , post- and preprocessing **)
local
@@ -752,20 +771,28 @@
fun preprocess thy thms =
thms
- |> fold (fn (_, (_, f)) => apply_preproc thy f) ((#preprocs o the_preproc o get_exec) thy)
- |> map (CodegenFunc.rewrite_func ((#inlines o the_preproc o get_exec) thy))
- |> fold (fn (_, (_, f)) => apply_inline_proc thy f) ((#inline_procs o the_preproc o get_exec) thy)
+ |> fold (fn (_, (_, f)) => apply_preproc thy f) ((#preprocs o the_thmproc o get_exec) thy)
+ |> map (CodegenFunc.rewrite_func ((#inlines o the_thmproc o get_exec) thy))
+ |> fold (fn (_, (_, f)) => apply_inline_proc thy f) ((#inline_procs o the_thmproc o get_exec) thy)
(*FIXME - must check: rewrite rule, defining equation, proper constant |> map (snd o check_func false thy) *)
|> common_typ_funcs;
-fun preprocess_cterm ct =
+fun preprocess_conv ct =
let
val thy = Thm.theory_of_cterm ct;
in
ct
- |> MetaSimplifier.rewrite false ((#inlines o the_preproc o get_exec) thy)
+ |> MetaSimplifier.rewrite false ((#inlines o the_thmproc o get_exec) thy)
|> fold (fn (_, (_, f)) => rhs_conv (apply_inline_proc_cterm thy f))
- ((#inline_procs o the_preproc o get_exec) thy)
+ ((#inline_procs o the_thmproc o get_exec) thy)
+ end;
+
+fun postprocess_conv ct =
+ let
+ val thy = Thm.theory_of_cterm ct;
+ in
+ ct
+ |> MetaSimplifier.rewrite false ((#posts o the_thmproc o get_exec) thy)
end;
end; (*local*)
--- a/src/Pure/Tools/codegen_funcgr.ML Tue Aug 07 09:38:48 2007 +0200
+++ b/src/Pure/Tools/codegen_funcgr.ML Tue Aug 07 09:40:34 2007 +0200
@@ -24,6 +24,10 @@
val make: theory -> CodegenConsts.const list -> T
val make_consts: theory -> CodegenConsts.const list -> CodegenConsts.const list * T
val make_term: theory -> (T -> (thm -> thm) -> cterm -> thm -> 'a) -> cterm -> 'a * T
+ (*FIXME drop make_term as soon as possible*)
+ val eval_conv: theory -> (T -> cterm -> thm) -> cterm -> thm
+ val intervene: theory -> T -> T
+ (*FIXME drop intervene as soon as possible*)
end;
structure CodegenFuncgr = (*signature is added later*)
@@ -317,7 +321,7 @@
in Thm.transitive thm thm' end
val _ = Sign.no_vars (Sign.pp thy) (Thm.term_of ct);
val _ = Term.fold_types (Type.no_tvars #> K I) (Thm.term_of ct) ();
- val thm1 = CodegenData.preprocess_cterm ct
+ val thm1 = CodegenData.preprocess_conv ct
|> fold (rhs_conv o MetaSimplifier.rewrite false o single) (rewrites thy);
val ct' = Thm.rhs_of thm1;
val consts = consts_of thy (Thm.term_of ct');
@@ -343,6 +347,20 @@
val funcgr'' = ensure_consts rewrites thy instdefs funcgr';
in (f funcgr'' drop ct'' thm5, funcgr'') end;
+fun ensure_consts_eval rewrites thy conv =
+ let
+ fun conv' funcgr drop_classes ct thm1 =
+ let
+ val thm2 = conv funcgr ct;
+ val thm3 = CodegenData.postprocess_conv (Thm.rhs_of thm2);
+ val thm23 = drop_classes (Thm.transitive thm2 thm3);
+ in
+ Thm.transitive thm1 thm23 handle THM _ =>
+ error ("eval_conv - could not construct proof:\n"
+ ^ (cat_lines o map string_of_thm) [thm1, thm2, thm3])
+ end;
+ in ensure_consts_term rewrites thy conv' end;
+
end; (*local*)
end; (*struct*)
@@ -374,6 +392,13 @@
fun make_term thy f =
Funcgr.change_yield thy o CodegenFuncgr.ensure_consts_term rewrites thy f;
+fun eval_conv thy f =
+ fst o Funcgr.change_yield thy o CodegenFuncgr.ensure_consts_eval rewrites thy f;
+
+(*FIXME*)
+fun intervene thy funcgr =
+ Funcgr.change thy (K funcgr);
+
end; (*functor*)
structure CodegenFuncgr : CODEGEN_FUNCGR =
--- a/src/Pure/Tools/codegen_package.ML Tue Aug 07 09:38:48 2007 +0200
+++ b/src/Pure/Tools/codegen_package.ML Tue Aug 07 09:40:34 2007 +0200
@@ -7,16 +7,21 @@
signature CODEGEN_PACKAGE =
sig
- val compile_term: theory -> term -> CodegenThingol.code * CodegenThingol.iterm;
+ (* interfaces *)
+ val eval_conv: theory
+ -> (CodegenThingol.code -> CodegenThingol.iterm -> cterm -> thm) -> cterm -> thm;
+ val codegen_command: theory -> string -> unit;
+
+ (* primitive interfaces *)
val eval_term: theory -> (string (*reference name!*) * 'a option ref) * term -> 'a;
val satisfies_ref: bool option ref;
val satisfies: theory -> term -> string list -> bool;
- val codegen_command: theory -> string -> unit;
- (*axiomatic interfaces*)
+ (* axiomatic interfaces *)
type appgen;
val add_appconst: string * appgen -> theory -> theory;
val appgen_let: appgen;
+ val appgen_if: appgen;
val appgen_case: (theory -> term
-> ((string * typ) list * ((term * typ) * (term * term) list)) option)
-> appgen;
@@ -125,7 +130,7 @@
val classops' = map (CodegenNames.const thy o CodegenConsts.const_of_cexpr thy) cs;
val defgen_class =
fold_map (ensure_def_class thy algbr funcgr) superclasses
- ##>> (fold_map (exprgen_type thy algbr funcgr) o map snd) cs
+ ##>> (fold_map (exprgen_typ thy algbr funcgr) o map snd) cs
#-> (fn (superclasses, classoptyps) => succeed
(CodegenThingol.Class (superclasses ~~ classrels', (unprefix "'" v, classops' ~~ classoptyps))))
in
@@ -148,7 +153,7 @@
trns
|> fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
||>> fold_map (fn (c, tys) =>
- fold_map (exprgen_type thy algbr funcgr) tys
+ fold_map (exprgen_typ thy algbr funcgr) tys
#-> (fn tys' =>
pair ((CodegenNames.const thy o CodegenConsts.const_of_cexpr thy)
(c, tys ---> Type (tyco, map TFree vs)), tys'))) cos
@@ -165,19 +170,19 @@
trns
|> fold_map (ensure_def_class thy algbr funcgr) (proj_sort sort)
|>> (fn sort => (unprefix "'" v, sort))
-and exprgen_type thy algbr funcgr (TFree vs) trns =
+and exprgen_typ thy algbr funcgr (TFree vs) trns =
trns
|> exprgen_tyvar_sort thy algbr funcgr vs
|>> (fn (v, sort) => ITyVar v)
- | exprgen_type thy algbr funcgr (Type (tyco, tys)) trns =
+ | exprgen_typ thy algbr funcgr (Type (tyco, tys)) trns =
case get_abstype thy (tyco, tys)
of SOME ty =>
trns
- |> exprgen_type thy algbr funcgr ty
+ |> exprgen_typ thy algbr funcgr ty
| NONE =>
trns
|> ensure_def_tyco thy algbr funcgr tyco
- ||>> fold_map (exprgen_type thy algbr funcgr) tys
+ ||>> fold_map (exprgen_typ thy algbr funcgr) tys
|>> (fn (tyco, tys) => tyco `%% tys);
exception CONSTRAIN of (string * typ) * typ;
@@ -291,7 +296,7 @@
|> CodegenThingol.message msg (fn trns => trns
|> timeap (fold_map (exprgen_eq o dest_eqthm) thms)
||>> fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
- ||>> exprgen_type thy algbr funcgr ty
+ ||>> exprgen_typ thy algbr funcgr ty
|-> (fn ((eqs, vs), ty) => succeed (CodegenThingol.Fun (eqs, (vs, ty)))))
end;
val defgen = if (is_some o CodegenData.get_datatype_of_constr thy) const
@@ -312,14 +317,14 @@
|> select_appgen thy algbr funcgr ((c, ty), [])
| exprgen_term thy algbr funcgr (Free (v, ty)) trns =
trns
- |> exprgen_type thy algbr funcgr ty
+ |> exprgen_typ thy algbr funcgr ty
|>> (fn _ => IVar v)
| exprgen_term thy algbr funcgr (Abs (raw_v, ty, raw_t)) trns =
let
val (v, t) = Syntax.variant_abs (raw_v, ty, raw_t);
in
trns
- |> exprgen_type thy algbr funcgr ty
+ |> exprgen_typ thy algbr funcgr ty
||>> exprgen_term thy algbr funcgr t
|>> (fn (ty, t) => (v, ty) `|-> t)
end
@@ -336,8 +341,8 @@
and appgen_default thy algbr funcgr ((c, ty), ts) trns =
trns
|> ensure_def_const thy algbr funcgr (CodegenConsts.const_of_cexpr thy (c, ty))
- ||>> fold_map (exprgen_type thy algbr funcgr) ((fst o Term.strip_type) ty)
- ||>> exprgen_type thy algbr funcgr ((snd o Term.strip_type) ty)
+ ||>> fold_map (exprgen_typ thy algbr funcgr) ((fst o Term.strip_type) ty)
+ ||>> exprgen_typ thy algbr funcgr ((snd o Term.strip_type) ty)
||>> exprgen_dict_parms thy algbr funcgr (c, ty)
||>> fold_map (exprgen_term thy algbr funcgr) ts
|>> (fn ((((c, tys), ty), iss), ts) => IConst (c, (iss, tys)) `$$ ts)
@@ -353,7 +358,7 @@
val vs = Name.names ctxt "a" tys;
in
trns
- |> fold_map (exprgen_type thy algbr funcgr) tys
+ |> fold_map (exprgen_typ thy algbr funcgr) tys
||>> appgen thy algbr funcgr ((c, ty), ts @ map Free vs)
|>> (fn (tys, t) => map2 (fn (v, _) => pair v) vs tys `|--> t)
end
@@ -397,27 +402,37 @@
(* parametrized application generators, for instantiation in object logic *)
(* (axiomatic extensions of translation kernel) *)
-fun appgen_case dest_case_expr thy algbr funcgr (app as (c_ty, ts)) trns =
+fun appgen_case dest_case_expr thy algbr funcgr (app as (c_ty, ts)) =
let
val SOME ([], ((st, sty), ds)) = dest_case_expr thy (list_comb (Const c_ty, ts));
- fun clausegen (dt, bt) trns =
- trns
- |> exprgen_term thy algbr funcgr dt
- ||>> exprgen_term thy algbr funcgr bt;
+ fun clause_gen (dt, bt) =
+ exprgen_term thy algbr funcgr dt
+ ##>> exprgen_term thy algbr funcgr bt;
in
- trns
- |> exprgen_term thy algbr funcgr st
- ||>> exprgen_type thy algbr funcgr sty
- ||>> fold_map clausegen ds
- |>> (fn ((se, sty), ds) => ICase ((se, sty), ds))
+ exprgen_term thy algbr funcgr st
+ ##>> exprgen_typ thy algbr funcgr sty
+ ##>> fold_map clause_gen ds
+ ##>> appgen_default thy algbr funcgr app
+ #>> (fn (((se, sty), ds), t0) => ICase (((se, sty), ds), t0))
end;
-fun appgen_let thy algbr funcgr (app as (_, [st, ct])) trns =
- trns
- |> exprgen_term thy algbr funcgr ct
- ||>> exprgen_term thy algbr funcgr st
- |-> (fn ((v, ty) `|-> be, se) => pair (CodegenThingol.collapse_let (((v, ty), se), be))
- | _ => appgen_default thy algbr funcgr app);
+fun appgen_let thy algbr funcgr (app as (_, [st, ct])) =
+ exprgen_term thy algbr funcgr ct
+ ##>> exprgen_term thy algbr funcgr st
+ ##>> appgen_default thy algbr funcgr app
+ #>> (fn (((v, ty) `|-> be, se), t0) =>
+ ICase (CodegenThingol.collapse_let (((v, ty), se), be), t0)
+ | (_, t0) => t0);
+
+fun appgen_if thy algbr funcgr (app as (_, [tb, tt, tf])) =
+ exprgen_term thy algbr funcgr tb
+ ##>> exprgen_typ thy algbr funcgr (Type ("bool", []))
+ ##>> exprgen_term thy algbr funcgr (Const ("True", Type ("bool", [])))
+ ##>> exprgen_term thy algbr funcgr tt
+ ##>> exprgen_term thy algbr funcgr (Const ("False", Type ("bool", [])))
+ ##>> exprgen_term thy algbr funcgr tf
+ ##>> appgen_default thy algbr funcgr app
+ #>> (fn ((((((tb, B), T), tt), F), tf), t0) => ICase (((tb, B), [(T, tt), (F, tf)]), t0));
fun add_appconst (c, appgen) thy =
let
@@ -511,6 +526,8 @@
fun generate thy funcgr gen it =
let
+ (*FIXME*)
+ val _ = Funcgr.intervene thy funcgr;
val cs = map_filter (Consttab.lookup ((snd o snd o Translation.get) thy))
(CodegenFuncgr.all funcgr);
val funcgr' = Funcgr.make thy cs;
@@ -526,6 +543,17 @@
|> fst
end;
+fun eval_conv thy conv =
+ let
+ fun conv' funcgr ct =
+ let
+ val t = generate thy funcgr exprgen_term' (Thm.term_of ct);
+ val consts = CodegenThingol.fold_constnames (insert (op =)) t [];
+ val code = Code.get thy
+ |> CodegenThingol.project_code true [] (SOME consts)
+ in conv code t ct end;
+ in Funcgr.eval_conv thy conv' end;
+
fun codegen_term thy t =
let
val ct = Thm.cterm_of thy t;
@@ -533,17 +561,6 @@
val t' = Thm.term_of ct';
in generate thy funcgr exprgen_term' t' end;
-fun compile_term thy t =
- let
- val ct = Thm.cterm_of thy t;
- val (ct', funcgr) = Funcgr.make_term thy (K (K K)) ct;
- val t' = Thm.term_of ct';
- val t'' = generate thy funcgr exprgen_term' t';
- val consts = CodegenThingol.fold_constnames (insert (op =)) t'' [];
- val code = Code.get thy
- |> CodegenThingol.project_code true [] (SOME consts)
- in (code, t'') end;
-
fun raw_eval_term thy (ref_spec, t) args =
let
val _ = (Term.map_types o Term.map_atyps) (fn _ =>
--- a/src/Pure/Tools/codegen_serializer.ML Tue Aug 07 09:38:48 2007 +0200
+++ b/src/Pure/Tools/codegen_serializer.ML Tue Aug 07 09:40:34 2007 +0200
@@ -281,7 +281,7 @@
|> Graph.fold ((fn name => Symtab.default (name, (mk_alias #> mk_prefix) name))
o fst o dest_name o fst)
code
- in (fn name => (the o Symtab.lookup tab) name) end;
+ in fn name => (the o Symtab.lookup tab) name end;
@@ -358,9 +358,30 @@
#>> (fn p => concat [str "fn", p, str "=>"]);
val (ps, vars') = fold_map pr binds vars;
in brackets (ps @ [pr_term vars' NOBR t']) end
- | pr_term vars fxy (t as ICase (_, [_])) =
+ | pr_term vars fxy (ICase (cases as (_, t0))) = (case CodegenThingol.unfold_const_app t0
+ of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
+ then pr_case vars fxy cases
+ else pr_app vars fxy c_ts
+ | NONE => pr_case vars fxy cases)
+ and pr_app' vars (app as ((c, (iss, tys)), ts)) =
+ if is_cons c then let
+ val k = length tys
+ in if k < 2 then
+ (str o deresolv) c :: map (pr_term vars BR) ts
+ else if k = length ts then
+ [(str o deresolv) c, Pretty.enum "," "(" ")" (map (pr_term vars NOBR) ts)]
+ else [pr_term vars BR (CodegenThingol.eta_expand app k)] end else
+ (str o deresolv) c
+ :: ((map (pr_dicts BR) o filter_out null) iss @ map (pr_term vars BR) ts)
+ and pr_app vars = gen_pr_app pr_app' pr_term const_syntax vars
+ and pr_bind' ((NONE, NONE), _) = str "_"
+ | pr_bind' ((SOME v, NONE), _) = str v
+ | pr_bind' ((NONE, SOME p), _) = p
+ | pr_bind' ((SOME v, SOME p), _) = concat [str v, str "as", p]
+ and pr_bind fxy = gen_pr_bind pr_bind' pr_term fxy
+ and pr_case vars fxy (cases as ((_, [_]), _)) =
let
- val (binds, t') = CodegenThingol.unfold_let t;
+ val (binds, t') = CodegenThingol.unfold_let (ICase cases);
fun pr ((pat, ty), t) vars =
vars
|> pr_bind NOBR ((NONE, SOME pat), ty)
@@ -373,7 +394,7 @@
str ("end")
]
end
- | pr_term vars fxy (ICase ((td, ty), b::bs)) =
+ | pr_case vars fxy (((td, ty), b::bs), _) =
let
fun pr delim (pat, t) =
let
@@ -389,23 +410,7 @@
:: map (pr "|") bs
)
end
- | pr_term vars fxy (t as ICase (_, [])) = str "raise Fail \"empty case\""
- and pr_app' vars (app as ((c, (iss, tys)), ts)) =
- if is_cons c then let
- val k = length tys
- in if k < 2 then
- (str o deresolv) c :: map (pr_term vars BR) ts
- else if k = length ts then
- [(str o deresolv) c, Pretty.enum "," "(" ")" (map (pr_term vars NOBR) ts)]
- else [pr_term vars BR (CodegenThingol.eta_expand app k)] end else
- (str o deresolv) c
- :: ((map (pr_dicts BR) o filter_out null) iss @ map (pr_term vars BR) ts)
- and pr_app vars = gen_pr_app pr_app' pr_term const_syntax vars
- and pr_bind' ((NONE, NONE), _) = str "_"
- | pr_bind' ((SOME v, NONE), _) = str v
- | pr_bind' ((NONE, SOME p), _) = p
- | pr_bind' ((SOME v, SOME p), _) = concat [str v, str "as", p]
- and pr_bind fxy = gen_pr_bind pr_bind' pr_term fxy;
+ | pr_case vars fxy ((_, []), _) = str "raise Fail \"empty case\""
fun pr_def (MLFuns (funns as (funn :: funns'))) =
let
val definer =
@@ -623,30 +628,11 @@
fun pr ((v, pat), ty) = pr_bind BR ((SOME v, pat), ty);
val (ps, vars') = fold_map pr binds vars;
in brackets (str "fun" :: ps @ str "->" @@ pr_term vars' NOBR t') end
- | pr_term vars fxy (t as ICase (_, [_])) =
- let
- val (binds, t') = CodegenThingol.unfold_let t;
- fun pr ((pat, ty), t) vars =
- vars
- |> pr_bind NOBR ((NONE, SOME pat), ty)
- |>> (fn p => concat [str "let", p, str "=", pr_term vars NOBR t, str "in"])
- val (ps, vars') = fold_map pr binds vars;
- in Pretty.chunks (ps @| pr_term vars' NOBR t') end
- | pr_term vars fxy (ICase ((td, ty), b::bs)) =
- let
- fun pr delim (pat, t) =
- let
- val (p, vars') = pr_bind NOBR ((NONE, SOME pat), ty) vars;
- in concat [str delim, p, str "->", pr_term vars' NOBR t] end;
- in
- (Pretty.enclose "(" ")" o single o brackify fxy) (
- str "match"
- :: pr_term vars NOBR td
- :: pr "with" b
- :: map (pr "|") bs
- )
- end
- | pr_term vars fxy (t as ICase (_, [])) = str "failwith \"empty case\""
+ | pr_term vars fxy (ICase (cases as (_, t0))) = (case CodegenThingol.unfold_const_app t0
+ of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
+ then pr_case vars fxy cases
+ else pr_app vars fxy c_ts
+ | NONE => pr_case vars fxy cases)
and pr_app' vars (app as ((c, (iss, tys)), ts)) =
if is_cons c then
if length tys = length ts
@@ -662,7 +648,31 @@
| pr_bind' ((SOME v, NONE), _) = str v
| pr_bind' ((NONE, SOME p), _) = p
| pr_bind' ((SOME v, SOME p), _) = brackets [p, str "as", str v]
- and pr_bind fxy = gen_pr_bind pr_bind' pr_term fxy;
+ and pr_bind fxy = gen_pr_bind pr_bind' pr_term fxy
+ and pr_case vars fxy (cases as ((_, [_]), _)) =
+ let
+ val (binds, t') = CodegenThingol.unfold_let (ICase cases);
+ fun pr ((pat, ty), t) vars =
+ vars
+ |> pr_bind NOBR ((NONE, SOME pat), ty)
+ |>> (fn p => concat [str "let", p, str "=", pr_term vars NOBR t, str "in"])
+ val (ps, vars') = fold_map pr binds vars;
+ in Pretty.chunks (ps @| pr_term vars' NOBR t') end
+ | pr_case vars fxy (((td, ty), b::bs), _) =
+ let
+ fun pr delim (pat, t) =
+ let
+ val (p, vars') = pr_bind NOBR ((NONE, SOME pat), ty) vars;
+ in concat [str delim, p, str "->", pr_term vars' NOBR t] end;
+ in
+ (Pretty.enclose "(" ")" o single o brackify fxy) (
+ str "match"
+ :: pr_term vars NOBR td
+ :: pr "with" b
+ :: map (pr "|") bs
+ )
+ end
+ | pr_case vars fxy ((_, []), _) = str "failwith \"empty case\"";
fun pr_def (MLFuns (funns as funn :: funns')) =
let
fun fish_parm _ (w as SOME _) = w
@@ -1123,9 +1133,18 @@
fun pr ((v, pat), ty) = pr_bind BR ((SOME v, pat), ty);
val (ps, vars') = fold_map pr binds vars;
in brackets (str "\\" :: ps @ str "->" @@ pr_term vars' NOBR t') end
- | pr_term vars fxy (t as ICase (_, [_])) =
+ | pr_term vars fxy (ICase (cases as (_, t0))) = (case CodegenThingol.unfold_const_app t0
+ of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
+ then pr_case vars fxy cases
+ else pr_app vars fxy c_ts
+ | NONE => pr_case vars fxy cases)
+ and pr_app' vars ((c, _), ts) =
+ (str o deresolv) c :: map (pr_term vars BR) ts
+ and pr_app vars = gen_pr_app pr_app' pr_term const_syntax vars
+ and pr_bind fxy = pr_bind_haskell pr_term fxy
+ and pr_case vars fxy (cases as ((_, [_]), _)) =
let
- val (binds, t) = CodegenThingol.unfold_let t;
+ val (binds, t) = CodegenThingol.unfold_let (ICase cases);
fun pr ((pat, ty), t) vars =
vars
|> pr_bind BR ((NONE, SOME pat), ty)
@@ -1137,7 +1156,7 @@
concat [str "}", str "in", pr_term vars' NOBR t]
) ps
end
- | pr_term vars fxy (ICase ((td, ty), bs as _ :: _)) =
+ | pr_case vars fxy (((td, ty), bs as _ :: _), _) =
let
fun pr (pat, t) =
let
@@ -1149,11 +1168,7 @@
str "})"
) (map pr bs)
end
- | pr_term vars fxy (t as ICase (_, [])) = str "error \"empty case\""
- and pr_app' vars ((c, _), ts) =
- (str o deresolv) c :: map (pr_term vars BR) ts
- and pr_app vars = gen_pr_app pr_app' pr_term const_syntax vars
- and pr_bind fxy = pr_bind_haskell pr_term fxy;
+ | pr_case vars fxy ((_, []), _) = str "error \"empty case\"";
fun pr_def (name, CodegenThingol.Fun (eqs, (vs, ty))) =
let
val tyvars = CodegenNames.intro_vars (map fst vs) init_syms;
@@ -1751,7 +1766,7 @@
let
fun pretty (pr : CodegenNames.var_ctxt -> fixity -> iterm -> Pretty.T)
vars fxy [(t1, _), ((v, ty) `|-> t2, _)] =
- pr vars fxy (ICase ((t1, ty), ([(IVar v, t2)])))
+ pr vars fxy (ICase (((t1, ty), ([(IVar v, t2)])), IVar ""))
| pretty pr vars fxy [(t1, _), (t2, ty2)] =
let
(*this code suffers from the lack of a proper concept for bindings*)
@@ -1760,7 +1775,7 @@
val vars' = CodegenNames.intro_vars [v] vars;
val var = IVar v;
val ty = (hd o fst o CodegenThingol.unfold_fun) ty2;
- in pr vars' fxy (ICase ((t1, ty), ([(var, t2 `$ var)]))) end;
+ in pr vars' fxy (ICase (((t1, ty), ([(var, t2 `$ var)])), IVar "")) end;
in (2, pretty) end;
end; (*local*)
@@ -2122,7 +2137,7 @@
]))
#> fold (add_reserved "SML") ML_Syntax.reserved_names
#> fold (add_reserved "SML")
- ["o" (*dictionary projections use it already*), "div", "mod" (*standard infixes*)]
+ ["o" (*dictionary projections use it already*), "Fail", "div", "mod" (*standard infixes*)]
#> fold (add_reserved "OCaml") [
"and", "as", "assert", "begin", "class",
"constraint", "do", "done", "downto", "else", "end", "exception",
@@ -2130,8 +2145,9 @@
"in", "include", "inherit", "initializer", "lazy", "let", "match", "method",
"module", "mutable", "new", "object", "of", "open", "or", "private", "rec",
"sig", "struct", "then", "to", "true", "try", "type", "val",
- "virtual", "when", "while", "with", "mod"
+ "virtual", "when", "while", "with"
]
+ #> fold (add_reserved "OCaml") ["failwith", "mod"]
#> fold (add_reserved "Haskell") [
"hiding", "deriving", "where", "case", "of", "infix", "infixl", "infixr",
"import", "default", "forall", "let", "in", "class", "qualified", "data",
--- a/src/Pure/Tools/codegen_thingol.ML Tue Aug 07 09:38:48 2007 +0200
+++ b/src/Pure/Tools/codegen_thingol.ML Tue Aug 07 09:40:34 2007 +0200
@@ -27,9 +27,8 @@
| IVar of vname
| `$ of iterm * iterm
| `|-> of (vname * itype) * iterm
- | ICase of (iterm * itype) * (iterm * iterm) list;
- (*(discriminendum term (td), discriminendum type (ty)),
- [(selector pattern (p), body term (t))] (bs))*)
+ | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
+ (*((term, type), [(selector pattern, body term )]), primitive term)*)
val `-> : itype * itype -> itype;
val `--> : itype list * itype -> itype;
val `$$ : iterm * iterm list -> iterm;
@@ -50,7 +49,8 @@
val unfold_let: iterm -> ((iterm * itype) * iterm) list * iterm;
val unfold_const_app: iterm ->
((string * (dict list list * itype list)) * iterm list) option;
- val collapse_let: ((vname * itype) * iterm) * iterm -> iterm;
+ val collapse_let: ((vname * itype) * iterm) * iterm
+ -> (iterm * itype) * (iterm * iterm) list;
val eta_expand: (string * (dict list list * itype list)) * iterm list -> int -> iterm;
val fold_constnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a;
val fold_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a;
@@ -129,7 +129,7 @@
| IVar of vname
| `$ of iterm * iterm
| `|-> of (vname * itype) * iterm
- | ICase of (iterm * itype) * (iterm * iterm) list;
+ | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
(*see also signature*)
(*
@@ -171,7 +171,7 @@
| _ => NONE);
val split_abs =
- (fn (v, ty) `|-> (t as ICase ((IVar w, _), [(p, t')])) =>
+ (fn (v, ty) `|-> (t as ICase (((IVar w, _), [(p, t')]), _)) =>
if v = w then SOME (((v, SOME p), ty), t') else SOME (((v, NONE), ty), t)
| (v, ty) `|-> t => SOME (((v, NONE), ty), t)
| _ => NONE);
@@ -179,7 +179,7 @@
val unfold_abs = unfoldr split_abs;
val split_let =
- (fn ICase ((td, ty), [(p, t)]) => SOME (((p, ty), td), t)
+ (fn ICase (((td, ty), [(p, t)]), _) => SOME (((p, ty), td), t)
| _ => NONE);
val unfold_let = unfoldr split_let;
@@ -189,16 +189,11 @@
of (IConst c, ts) => SOME (c, ts)
| _ => NONE;
-fun fold_aiterms f (t as IConst _) =
- f t
- | fold_aiterms f (t as IVar _) =
- f t
- | fold_aiterms f (t1 `$ t2) =
- fold_aiterms f t1 #> fold_aiterms f t2
- | fold_aiterms f (t as _ `|-> t') =
- f t #> fold_aiterms f t'
- | fold_aiterms f (ICase ((td, _), bs)) =
- fold_aiterms f td #> fold (fn (p, t) => fold_aiterms f p #> fold_aiterms f t) bs;
+fun fold_aiterms f (t as IConst _) = f t
+ | fold_aiterms f (t as IVar _) = f t
+ | fold_aiterms f (t1 `$ t2) = fold_aiterms f t1 #> fold_aiterms f t2
+ | fold_aiterms f (t as _ `|-> t') = f t #> fold_aiterms f t'
+ | fold_aiterms f (ICase (_, t)) = fold_aiterms f t;
fun fold_constnames f =
let
@@ -215,29 +210,24 @@
fun fold_unbound_varnames f =
let
- fun add _ (IConst _) =
- I
- | add vs (IVar v) =
- if not (member (op =) vs v) then f v else I
- | add vs (t1 `$ t2) =
- add vs t1 #> add vs t2
- | add vs ((v, _) `|-> t) =
- add (insert (op =) v vs) t
- | add vs (ICase ((td, _), bs)) =
- add vs td #> fold (fn (p, t) => add vs p #> add vs t) bs;
+ fun add _ (IConst _) = I
+ | add vs (IVar v) = if not (member (op =) vs v) then f v else I
+ | add vs (t1 `$ t2) = add vs t1 #> add vs t2
+ | add vs ((v, _) `|-> t) = add (insert (op =) v vs) t
+ | add vs (ICase (_, t)) = add vs t;
in add [] end;
-fun collapse_let (((v, ty), se), be as ICase ((IVar w, _), ds)) =
+fun collapse_let (((v, ty), se), be as ICase (((IVar w, _), ds), _)) =
let
fun exists_v t = fold_unbound_varnames (fn w => fn b =>
b orelse v = w) t false;
in if v = w andalso forall (fn (t1, t2) =>
exists_v t1 orelse not (exists_v t2)) ds
- then ICase ((se, ty), ds)
- else ICase ((se, ty), [(IVar v, be)])
+ then ((se, ty), ds)
+ else ((se, ty), [(IVar v, be)])
end
| collapse_let (((v, ty), se), be) =
- ICase ((se, ty), [(IVar v, be)])
+ ((se, ty), [(IVar v, be)])
fun eta_expand (c as (_, (_, tys)), ts) k =
let
--- a/src/Pure/codegen.ML Tue Aug 07 09:38:48 2007 +0200
+++ b/src/Pure/codegen.ML Tue Aug 07 09:40:34 2007 +0200
@@ -377,7 +377,8 @@
fn thm => add_unfold thm #> CodeData.add_inline thm));
val _ = map (Context.add_setup o add_del_attribute) [
("func", (CodeData.add_func true, CodeData.del_func)),
- ("inline", (CodeData.add_inline, CodeData.del_inline))
+ ("inline", (CodeData.add_inline, CodeData.del_inline)),
+ ("post", (CodeData.add_post, CodeData.del_post))
];
end; (*local*)
--- a/src/Tools/nbe.ML Tue Aug 07 09:38:48 2007 +0200
+++ b/src/Tools/nbe.ML Tue Aug 07 09:40:34 2007 +0200
@@ -351,7 +351,8 @@
Logic.mk_equals (t, eval thy code t t');
fun normalization_invoke thy code t t' =
- Thm.invoke_oracle_i thy "Nbe.normalization" (thy, Normalization (code, t, t'));
+ Thm.invoke_oracle_i thy "HOL.normalization" (thy, Normalization (code, t, t'));
+ (*FIXME get rid of hardwired theory name "HOL"*)
fun normalization_conv ct =
let