# HG changeset patch
# User nipkow
# Date 1140536274 -3600
# Node ID 52f751b50716807267f4ad4b3558990a54275023
# Parent  5208677a394c5bcd95e1b4d8d60f17bbdcc092f9
added Tools/nbe, fixes

diff -r 5208677a394c -r 52f751b50716 src/Pure/Tools/ROOT.ML
--- 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";
diff -r 5208677a394c -r 52f751b50716 src/Pure/Tools/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 *)
+
 *)