added nbe, updated neb_*

--- a/src/Pure/Tools/ROOT.ML	Mon Feb 27 14:03:15 2006 +0100
+++ b/src/Pure/Tools/ROOT.ML	Mon Feb 27 14:03:31 2006 +0100
@@ -24,3 +24,4 @@
 (* norm-by-eval *)
 use "nbe_eval.ML";
 use "nbe_codegen.ML";
+use "nbe.ML";

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/nbe.ML	Mon Feb 27 14:03:31 2006 +0100
@@ -0,0 +1,74 @@
+(*  ID:         $Id$
+    Author:     Tobias Nipkow, Florian Haftmann, TU Muenchen
+
+Installing "normalization by evaluation"
+*)
+
+signature NORMBYEVAL =
+sig
+  val lookup: string -> NBE_Eval.Univ
+  val update: string * NBE_Eval.Univ -> unit
+end;
+
+structure NormByEval:NORMBYEVAL =
+struct
+
+structure NBE_Data = TheoryDataFun
+(struct
+  val name = "Pure/NormByEval";
+  type T = NBE_Eval.Univ Symtab.table
+  val empty = Symtab.empty
+  val copy = I;
+  val extend = I;
+  fun merge _ = Symtab.merge (K true)
+  fun print _ _ = ();
+end);
+
+val _ = Context.add_setup NBE_Data.init;
+
+fun use_show 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" 
+                                "\n---\n")
+      true s);
+
+val tab = ref Symtab.empty
+fun lookup s = the(Symtab.lookup (!tab) s)
+fun update sx = (tab := Symtab.update sx (!tab))
+fun defined s = Symtab.defined (!tab) s;
+
+fun top_nbe st thy =
+let val t = Sign.read_term thy st
+    val ((t',diff),thy') = CodegenPackage.codegen_incr t thy
+    val _ = (tab := NBE_Data.get thy;
+             Library.seq (use_show o NBE_Codegen.generate defined) diff)
+    val thy'' = NBE_Data.put (!tab) thy'
+    val nt' = NBE_Eval.nbe (!tab) t'
+    val _ = print nt'
+in
+  thy''
+end
+
+structure P = OuterParse and K = OuterKeyword;
+
+val nbeP =
+  OuterSyntax.command "norm_by_eval" "norm by eval" K.thy_decl
+    (P.term >> (Toplevel.theory o top_nbe));
+
+val _ = OuterSyntax.add_parsers [nbeP];
+(*
+ProofGeneral.write_keywords "nbe";
+*)
+(* isar-keywords-nbe.el -> isabelle/etc/
+   Isabelle -k nbe *)
+
+end
+
+
+(*
+fun to_term xs (C s) = Const(s,dummyT)
+  | to_term xs (V s) = Free(s,dummyT)
+  | to_term xs (B i) = Bound (find_index_eq i xs)
+  | to_term xs (A(t1,t2)) = to_term xs t1 $ to_term xs t2
+  | to_term xs (AbsN(i,t)) = Abs("u",dummyT,to_term (i::xs) t);
+*)

--- a/src/Pure/Tools/nbe_codegen.ML	Mon Feb 27 14:03:15 2006 +0100
+++ b/src/Pure/Tools/nbe_codegen.ML	Mon Feb 27 14:03:31 2006 +0100
@@ -7,27 +7,23 @@
    all defining equations have same number of arguments.
 
 FIXME
-fun MLname s = "nbe_" ^ s;
+fun MLname
 val quote = quote;
 
-FIXME xtab in theory
-
-FIXME CodegenThingol names! which "error"?
+FIXME CodegenThingol names!
 *)
 
 signature NBE_CODEGEN =
 sig
-  val export: Theory.theory -> string * CodegenThingol.def -> string
+  val generate: (string -> bool) -> 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";
-val Eval_lookup  = Eval ^ ".lookup";
+val Eval_mk_Fun  = Eval ^ ".mk_Fun";
 val Eval_apply   = Eval ^ ".apply";
 val Eval_Constr  = Eval ^ ".Constr";
 val Eval_C       = Eval ^ ".C";
@@ -37,7 +33,7 @@
 val Eval_new_name = Eval ^ ".new_name";
 val Eval_to_term = Eval ^ ".to_term";
 
-fun MLname s = "nbe_" ^ s;
+fun MLname s = "nbe_" ^ translate_string (fn "." => "_" | c => c) s;
 fun MLvname s  = "v_" ^ MLname s;
 fun MLparam n  = "p_" ^ string_of_int n;
 fun MLintern s = "i_" ^ MLname s;
@@ -68,6 +64,9 @@
 
 end
 
+val tab_lookup = S.app "NormByEval.lookup";
+val tab_update = S.app "NormByEval.update";
+
 fun mk_nbeFUN(nm,e) =
   S.app Eval_Fun (S.tup [S.abs(S.list [MLvname nm])e,S.list [],"1",
       S.abs(S.tup [])(S.Let 
@@ -88,13 +87,12 @@
 	(S.quote nm))]);
 
 
-fun mk_rexpr nm ar =
+fun mk_rexpr defined nm ar =
   let fun mk args t = case t of
     CodegenThingol.IConst((s,_),_) => 
     if s=nm then selfcall nm ar args
-    else if is_constr s then S.app Eval_Constr 
-                                   (S.tup [S.quote s,S.list args ])
-    else S.nbe_apps (MLname s) args
+    else if defined s then S.nbe_apps (MLname s) args
+    else S.app Eval_Constr (S.tup [S.quote s,S.list args ])
   | CodegenThingol.IVarE(s,_) => S.nbe_apps (MLvname s) args
   | CodegenThingol.IApp(e1,e2) => mk (args @ [mk [] e2]) e1
   | CodegenThingol.IAbs(CodegenThingol.IVarE(nm,_), e) =>
@@ -112,7 +110,8 @@
   | _ => sys_error "NBE mk_lexpr illegal pattern"
   in mk [] end;
 
-fun mk_eqn nm ar (lhs,e) = ([S.list(map mk_lexpr (rev lhs))], mk_rexpr nm ar e);
+fun mk_eqn defined nm ar (lhs,e) =
+  ([S.list(map mk_lexpr (rev lhs))], mk_rexpr defined nm ar e);
 
 fun funs_of_expr(CodegenThingol.IConst((s,_),_),fs) = s::fs
   | funs_of_expr(CodegenThingol.IApp(e1,e2),fs) =
@@ -120,23 +119,23 @@
   | funs_of_expr(CodegenThingol.IAbs(_, e),fs) = funs_of_expr(e,fs)
   | funs_of_expr(_,fs) = fs;
 
-fun lookup nm =
-  S.Val (MLname nm) (S.app Eval_lookup (S.quote nm));
+fun lookup nm = S.Val (MLname nm) (tab_lookup (S.quote nm));
 
-fun export thy (nm,CodegenThingol.Fun(eqns,_)) =
+fun generate defined (nm,CodegenThingol.Fun(eqns,_)) =
   let
     val ar = length(fst(hd eqns));
     val params = S.list (rev (MLparams ar));
     val funs = Library.flat(map (fn (_,e) => funs_of_expr(e,[])) eqns) \ nm;
-    val globals = map lookup (filter_out is_constr funs);
+    val globals = map lookup (filter defined funs);
     val default_eqn = ([params], S.app Eval_Constr (S.tup[S.quote nm,params]));
-    val code = S.eqns (MLname nm) (map (mk_eqn nm ar) eqns @ [default_eqn])
-    val register = S.app Eval_register
-                     (S.tup[S.quote nm, MLname nm, string_of_int ar])
+    val code = S.eqns (MLname nm)
+                      (map (mk_eqn defined nm ar) eqns @ [default_eqn])
+    val register = tab_update
+        (S.app Eval_mk_Fun (S.tup[S.quote nm, MLname nm, string_of_int ar]))
   in
     S.Let (globals @ [code]) register
   end
-  | export _ _ = "\"NBE no op\"";
+  | generate _ _ = "";
 
 end;
 
@@ -150,7 +149,7 @@
 
 val dummyIT = CodegenThingol.IType("DUMMY",[]);
 
-use_show(export "" ("append",CodegenThingol.Fun(
+use_show(NBE_Codegen.generate (the_context()) ("append",CodegenThingol.Fun(
   [([CodegenThingol.IConst(("Nil",dummyIT),[]),
      CodegenThingol.IVarE("ys",dummyIT)],
     CodegenThingol.IVarE("ys",dummyIT)),
@@ -205,7 +204,7 @@
 end;
 
 
-use_show(export "" ("app",CodegenThingol.Fun(
+use_show(NBE_Codegen.generate (the_context()) ("app",CodegenThingol.Fun(
   [
   ([CodegenThingol.IConst(("Nil",dummyIT),[])],
     CodegenThingol.IAbs(CodegenThingol.IVarE("ys",dummyIT),
@@ -265,7 +264,7 @@
 end;
 
 
-use_show(export "" ("add",CodegenThingol.Fun(
+use_show(NBE_Codegen.generate (the_context()) ("add",CodegenThingol.Fun(
   [
   ([CodegenThingol.IConst(("0",dummyIT),[])],
     CodegenThingol.IAbs(CodegenThingol.IVarE("n",dummyIT),
@@ -303,7 +302,7 @@
 
 
 
-use_show(export "" ("mul",CodegenThingol.Fun(
+use_show(NBE_Codegen.generate (the_context()) ("mul",CodegenThingol.Fun(
   [
   ([CodegenThingol.IConst(("0",dummyIT),[])],
     CodegenThingol.IAbs(CodegenThingol.IVarE("n",dummyIT),
@@ -347,31 +346,3 @@
 ()
 end;
 *)
-
-
-(*
-fun top_eval st thy =
-let val t = Sign.read_term thy st
-    val tabs = CodegenPackage.mk_tabs thy;
-    val thy') =
-      CodegenPackage.expand_module NONE (CodegenPackage.codegen_term
-         thy tabs [t]) thy
-    val s = map export diff
-in use s; (* FIXME val thy'' = thy' |> *)
-   Pretty.writeln (Sign.pretty_term thy t');
-   thy'
-end
-
-structure P = OuterParse;
-
-val nbeP =
-  OuterSyntax.command "norm_by_eval" "norm by eval" K.thy_decl
-    (P.term >> (Toplevel.theory o top_eval));
-
-val _ = OuterSyntax.add_parsers [nbeP];
-
-ProofGeneral.write_keywords "nbe";
-(* isar-keywords-nbe.el -> isabelle/etc/
-   Isabelle -k nbe *)
-
-*)

--- a/src/Pure/Tools/nbe_eval.ML	Mon Feb 27 14:03:15 2006 +0100
+++ b/src/Pure/Tools/nbe_eval.ML	Mon Feb 27 14:03:31 2006 +0100
@@ -6,7 +6,6 @@
 
 (* Optimizations:
  int instead of string in Constr
- xtab as real table
  treat int via ML ints
 *)
 
@@ -20,20 +19,18 @@
   | A of nterm*nterm (* Application *)
   | AbsN of int*nterm ; (* Binding of named Variables *)
 
-val nbe: term -> nterm
-
 datatype Univ = 
     Constr of string*(Univ list)       (* Named Constructors *)
   | Var of string*(Univ list)          (* Free variables *)
   | BVar of int*(Univ list)            (* Bound named variables *)
   | Fun of (Univ list -> Univ) * (Univ list) * int * (unit -> nterm);
                                             (* Functions *)
+val nbe: Univ Symtab.table -> CodegenThingol.iexpr -> nterm
+
 val apply: Univ -> Univ -> Univ;
 val to_term: Univ -> nterm;
 
-val lookup: string -> Univ;
-val is_constr: string -> bool;
-val register: string * (Univ list -> Univ) * int -> unit
+val mk_Fun: string * (Univ list -> Univ) * int -> string * Univ
 val new_name: unit -> int;
 
 (* For testing
@@ -109,22 +106,17 @@
    | apply (Var(name,args))    x = Var(name,x::args)
    | apply (BVar(name,args))   x = BVar(name,x::args);
 
+fun mk_Fun(name,v,0) = (name,v [])
+  | mk_Fun(name,v,n) = (name,Fun(v,[],n, fn () => C name));
+
 (* ---------------- table with the meaning of constants -------------------- *)
 
-val xfun_tab: (string * Univ)list ref = ref [];
-fun do_register sx = (xfun_tab := sx :: !xfun_tab);
-fun register(name,v,0) = do_register(name,v [])
-  | register(name,v,n) = do_register(name,Fun(v,[],n, fn () => C name));
+val xfun_tab: Univ Symtab.table ref = ref Symtab.empty;
 
-fun do_lookup [] s          = NONE
-  |	do_lookup ((n,v)::xs) s = if (s=n) then SOME v else do_lookup xs s;
-
-fun lookup s = case do_lookup (!xfun_tab) s of
+fun lookup s = case Symtab.lookup (!xfun_tab) s of
     SOME x => x
   | NONE   => Constr(s,[]);
 
-fun is_constr s = is_none (do_lookup (!xfun_tab) s);
-
 (* ------------------ evaluation with greetings to Tarski ------------------ *)
 
 (* generation of fresh names *)
@@ -135,17 +127,21 @@
 
 (* greetings to Tarski *)
 
-fun eval(Const(f,_)) xs = lookup f
-  | eval(Free(x,_)) xs = Var(x,[])
-  | eval(Bound n) xs = List.nth(xs,n)
-  | eval(s $ t) xs = apply (eval s xs) (eval t xs)
-  | eval(Abs(_,_, t)) xs = Fun ((fn [x] => eval t (x::xs)),[],1,
-                           fn () => let val var = new_name() in
-                         AbsN(var, to_term (eval t ((BVar(var,[]) :: xs)))) end);
+structure IL = CodegenThingol
+
+fun eval(IL.IConst((f,_),_)) xs = lookup f
+  | eval(IL.IVarE(n,_)) xs =
+      (case AList.lookup (op =) xs n of NONE => Var(n,[])
+       | SOME v => v)
+  | eval(IL.IApp(s,t)) xs = apply (eval s xs) (eval t xs)
+  | eval(IL.IAbs(IL.IVarE(n,_), t)) xs =
+      Fun (fn [x] => eval t ((n,x)::xs), [], 1,
+           fn () => let val var = new_name() in
+                 AbsN(var, to_term (eval t ((n,BVar(var,[])) :: xs))) end);
 
 
 (* finally... *)
 
-fun nbe t = (counter :=0; to_term(eval t []));
+fun nbe tab t = (counter :=0; xfun_tab := tab; to_term(eval t []));
 
 end;