restored incremental code generation

--- a/src/Tools/code/code_thingol.ML	Tue Oct 28 16:59:01 2008 +0100
+++ b/src/Tools/code/code_thingol.ML	Tue Oct 28 16:59:02 2008 +0100
@@ -57,6 +57,7 @@
   val fold_unbound_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a
 
   type naming
+  val empty_naming: naming
   val lookup_class: naming -> class -> string option
   val lookup_classrel: naming -> class * class -> string option
   val lookup_tyco: naming -> string -> string option
@@ -259,14 +260,11 @@
   fun thyname_of_instance thy inst = case AxClass.arity_property thy inst Markup.theory_nameN
    of [] => error ("no such instance: " ^ quote (snd inst ^ " :: " ^ fst inst))
     | thyname :: _ => thyname;
-  fun thyname_of_const thy c = case Code.get_datatype_of_constr thy c
-     of SOME dtco => thyname_of_tyco thy dtco
-      | NONE => (case AxClass.class_of_param thy c
-         of SOME class => thyname_of_class thy class
-          | NONE => (case AxClass.inst_of_param thy c
-             of SOME (c, tyco) => thyname_of_instance thy
-                  ((the o AxClass.class_of_param thy) c, tyco)
-              | NONE => thyname_of thy (Consts.the_tags (Sign.consts_of thy)) c));
+  fun thyname_of_const thy c = case AxClass.class_of_param thy c
+   of SOME class => thyname_of_class thy class
+    | NONE => (case Code.get_datatype_of_constr thy c
+       of SOME dtco => thyname_of_tyco thy dtco
+        | NONE => thyname_of thy (Consts.the_tags (Sign.consts_of thy)) c);
   fun namify thy get_basename get_thyname name =
     let
       val prefix = get_thyname thy name;
@@ -453,27 +451,26 @@
 
 fun ensure_stmt lookup declare generate thing (dep, (naming, program)) =
   let
-    fun add_dep name = case dep
-     of NONE => I | SOME dep => Graph.add_edge (dep, name);
-  in case lookup naming thing
-   of SOME name => program
+    fun add_dep name = case dep of NONE => I
+      | SOME dep => Graph.add_edge (dep, name);
+    val (name, naming') = case lookup naming thing
+     of SOME name => (name, naming)
+      | NONE => declare thing naming;
+  in case try (Graph.get_node program) name
+   of SOME stmt => program
         |> add_dep name
-        |> pair naming
+        |> pair naming'
         |> pair dep
         |> pair name
-    | NONE => let
-          val (name, naming') = declare thing naming;
-        in
-          program
-          |> Graph.default_node (name, NoStmt)
-          |> add_dep name
-          |> pair naming'
-          |> curry generate (SOME name)
-          ||> snd
-          |-> (fn stmt => (apsnd o Graph.map_node name) (K stmt))
-          |> pair dep
-          |> pair name
-        end
+    | NONE => program
+        |> Graph.default_node (name, NoStmt)
+        |> add_dep name
+        |> pair naming'
+        |> curry generate (SOME name)
+        ||> snd
+        |-> (fn stmt => (apsnd o Graph.map_node name) (K stmt))
+        |> pair dep
+        |> pair name
   end;
 
 fun not_wellsorted thy thm ty sort e =
@@ -719,15 +716,14 @@
 (
   type T = naming * program;
   val empty = (empty_naming, Graph.empty);
-  fun purge thy cs (naming, program) = empty (*FIXME: problem: un-declaration of names
+  fun purge thy cs (naming, program) =
     let
-      val cs_exisiting =
-        map_filter (Code_Name.const_rev thy) (Graph.keys program);
-      val dels = (Graph.all_preds program
-          o map (Code_Name.const thy)
-          o filter (member (op =) cs_exisiting)
-        ) cs;
-    in Graph.del_nodes dels program end;*)
+      val names_delete = cs
+        |> map_filter (lookup_const naming)
+        |> filter (can (Graph.get_node program))
+        |> Graph.all_preds program;
+      val program' = Graph.del_nodes names_delete program;
+    in (naming, program') end;
 );
 
 val cached_program = Program.get;

--- a/src/Tools/nbe.ML	Tue Oct 28 16:59:01 2008 +0100
+++ b/src/Tools/nbe.ML	Tue Oct 28 16:59:02 2008 +0100
@@ -336,14 +336,17 @@
       #-> fold (fn (name, univ) => (Graph.map_node name o apfst) (K (SOME univ))))
   end;
 
-fun ensure_stmts ctxt program =
+fun ensure_stmts ctxt naming program =
   let
     fun add_stmts names (gr, (maxidx, idx_tab)) = if exists ((can o Graph.get_node) gr) names
       then (gr, (maxidx, idx_tab))
       else (gr, (maxidx, idx_tab))
         |> compile_stmts ctxt (map (fn name => ((name, Graph.get_node program name),
           Graph.imm_succs program name)) names);
-  in fold_rev add_stmts (Graph.strong_conn program) end;
+  in
+    fold_rev add_stmts (Graph.strong_conn program)
+    #> pair naming
+  end;
 
 
 (** evaluation **)
@@ -404,25 +407,25 @@
 
 structure Nbe_Functions = CodeDataFun
 (
-  type T = (Univ option * int) Graph.T * (int * string Inttab.table);
-  val empty = (Graph.empty, (0, Inttab.empty));
-  fun purge thy cs (gr, (maxidx, idx_tab)) = empty (*FIXME
+  type T = Code_Thingol.naming * ((Univ option * int) Graph.T * (int * string Inttab.table));
+  val empty = (Code_Thingol.empty_naming, (Graph.empty, (0, Inttab.empty)));
+  fun purge thy cs (naming, (gr, (maxidx, idx_tab))) =
     let
-      val cs_exisiting =
-        map_filter (Code_Name.const_rev thy) (Graph.keys gr);
-      val dels = (Graph.all_preds gr
-          o map (Code_Name.const thy)
-          o filter (member (op =) cs_exisiting)
-        ) cs;
-    in (Graph.del_nodes dels gr, (maxidx, idx_tab)) end*);
+      val names_delete = cs
+        |> map_filter (Code_Thingol.lookup_const naming)
+        |> filter (can (Graph.get_node gr))
+        |> Graph.all_preds gr;
+      val gr' = Graph.del_nodes names_delete gr;
+    in (naming, (gr', (maxidx, idx_tab))) end;
 );
 
 (* compilation, evaluation and reification *)
 
-fun compile_eval thy program vs_ty_t deps =
+fun compile_eval thy naming program vs_ty_t deps =
   let
     val ctxt = ProofContext.init thy;
-    val (gr, (_, idx_tab)) = Nbe_Functions.change thy (ensure_stmts ctxt program);
+    val (_, (gr, (_, idx_tab))) =
+      Nbe_Functions.change thy (ensure_stmts ctxt naming program o snd);
   in
     vs_ty_t
     |> eval_term ctxt gr deps
@@ -431,7 +434,7 @@
 
 (* evaluation with type reconstruction *)
 
-fun eval thy t program vs_ty_t deps =
+fun eval thy t naming program vs_ty_t deps =
   let
     fun subst_const f = map_aterms (fn t as Term.Const (c, ty) => Term.Const (f c, ty)
       | t => t);
@@ -450,7 +453,7 @@
         ^ setmp show_types true (Syntax.string_of_term_global thy) t);
     val string_of_term = setmp show_types true (Syntax.string_of_term_global thy);
   in
-    compile_eval thy program vs_ty_t deps
+    compile_eval thy naming program vs_ty_t deps
     |> tracing (fn t => "Normalized:\n" ^ string_of_term t)
     |> subst_triv_consts
     |> type_frees
@@ -464,8 +467,8 @@
 (* evaluation oracle *)
 
 val (_, norm_oracle) = Context.>>> (Context.map_theory_result
-  (Thm.add_oracle ("norm", fn (thy, t, program, vs_ty_t, deps) =>
-    Thm.cterm_of thy (Logic.mk_equals (t, eval thy t program vs_ty_t deps)))));
+  (Thm.add_oracle ("norm", fn (thy, t, naming, program, vs_ty_t, deps) =>
+    Thm.cterm_of thy (Logic.mk_equals (t, eval thy t naming program vs_ty_t deps)))));
 
 fun add_triv_classes thy =
   let
@@ -479,13 +482,14 @@
 fun norm_conv ct =
   let
     val thy = Thm.theory_of_cterm ct;
-    fun evaluator' t naming program vs_ty_t deps = norm_oracle (thy, t, program, vs_ty_t, deps);
+    fun evaluator' t naming program vs_ty_t deps =
+      norm_oracle (thy, t, naming, program, vs_ty_t, deps);
     fun evaluator t = (add_triv_classes thy t, evaluator' t);
   in Code_Thingol.eval_conv thy evaluator ct end;
 
 fun norm_term thy t =
   let
-    fun evaluator' t naming program vs_ty_t deps = eval thy t program vs_ty_t deps;
+    fun evaluator' t naming program vs_ty_t deps = eval thy t naming program vs_ty_t deps;
     fun evaluator t = (add_triv_classes thy t, evaluator' t);
   in (Code.postprocess_term thy o Code_Thingol.eval_term thy evaluator) t end;