--- a/src/Pure/Tools/ROOT.ML Tue Feb 21 16:37:33 2006 +0100
+++ b/src/Pure/Tools/ROOT.ML Tue Feb 21 16:37:54 2006 +0100
@@ -20,3 +20,7 @@
use "am_compiler.ML";
use "am_util.ML";
use "compute.ML";
+
+(* norm-by-eval *)
+use "nbe_eval.ML";
+use "nbe_codegen.ML";
--- a/src/Pure/Tools/nbe_codegen.ML Tue Feb 21 16:37:33 2006 +0100
+++ b/src/Pure/Tools/nbe_codegen.ML Tue Feb 21 16:37:54 2006 +0100
@@ -11,14 +11,19 @@
val quote = quote;
FIXME xtab in theory
-*)
-(*
-structure NBE_Codegen =
-struct
FIXME CodegenThingol names! which "error"?
*)
+signature NBE_CODEGEN =
+sig
+ val export: Theory.theory -> string * CodegenThingol.def -> string
+end
+
+
+structure NBE_Codegen: NBE_CODEGEN =
+struct
+
val is_constr = NBE_Eval.is_constr;
val Eval = "NBE_Eval";
val Eval_register= Eval ^ ".register";
@@ -133,6 +138,10 @@
end
| export _ _ = "\"NBE no op\"";
+end;
+
+(*
+
val use_show = fn s => (writeln ("\n---generated code:\n"^ s);
use_text(writeln o enclose "\n---compiler echo:\n" "\n---\n",
writeln o enclose "\n--- compiler echo (with error!):\n"
@@ -337,15 +346,10 @@
(A (C "add", V "y"),A(A (C "mul", V "x"),A(C "S",A(C "S",A(C "S", V"y")))))))))))));
()
end;
-
-
-
+*)
(*
- | export(nm,Fun(cls,(_,ty)))
- | export _ = ""
-
fun top_eval st thy =
let val t = Sign.read_term thy st
val tabs = CodegenPackage.mk_tabs thy;
@@ -369,4 +373,5 @@
ProofGeneral.write_keywords "nbe";
(* isar-keywords-nbe.el -> isabelle/etc/
Isabelle -k nbe *)
+
*)