src/Tools/nbe.ML

     val (fun_vars, fun_vals) = map_split assemble_eqns eqnss';
     val deps_vars = ml_list (map (nbe_fun 0) deps);
   in ml_abs deps_vars (ml_Let (ml_fundefs (flat fun_vars)) (ml_list fun_vals)) end;
 
 
-(* code compilation *)
-
-fun compile_eqnss ctxt gr raw_deps [] = []
-  | compile_eqnss ctxt gr raw_deps eqnss =
-      let
+(* compile equations *)
+
+fun compile_eqnss thy nbe_program raw_deps [] = []
+  | compile_eqnss thy nbe_program raw_deps eqnss =
+      let
+        val ctxt = ProofContext.init_global thy;
         val (deps, deps_vals) = split_list (map_filter
-          (fn dep => Option.map (fn univ => (dep, univ)) (fst ((Graph.get_node gr dep)))) raw_deps);
+          (fn dep => Option.map (fn univ => (dep, univ)) (fst ((Graph.get_node nbe_program dep)))) raw_deps);
         val idx_of = raw_deps
-          |> map (fn dep => (dep, snd (Graph.get_node gr dep)))
+          |> map (fn dep => (dep, snd (Graph.get_node nbe_program dep)))
           |> AList.lookup (op =)
           |> (fn f => the o f);
         val s = assemble_eqnss idx_of deps eqnss;
         val cs = map fst eqnss;
       in

         |> (fn f => f deps_vals)
         |> (fn univs => cs ~~ univs)
       end;
 
 
-(* preparing function equations *)
+(* extract equations from statements *)
 
 fun eqns_of_stmt (_, Code_Thingol.Fun (_, ((_, []), _))) =
       []
   | eqns_of_stmt (const, Code_Thingol.Fun (_, (((vs, _), eqns), _))) =
       [(const, (vs, map fst eqns))]

   | eqns_of_stmt (inst, Code_Thingol.Classinst ((class, (_, arity_args)), (super_instances, (classparam_instances, _)))) =
       [(inst, (arity_args, [([], IConst (class, (([], []), [])) `$$
         map (fn (_, (_, (inst, dss))) => IConst (inst, (([], dss), []))) super_instances
         @ map (IConst o snd o fst) classparam_instances)]))];
 
-fun compile_stmts ctxt stmts_deps =
+
+(* compile whole programs *)
+
+fun compile_stmts thy stmts_deps =
   let
     val names = map (fst o fst) stmts_deps;
     val names_deps = map (fn ((name, _), deps) => (name, deps)) stmts_deps;
     val eqnss = maps (eqns_of_stmt o fst) stmts_deps;
     val refl_deps = names_deps
       |> maps snd
       |> distinct (op =)
       |> fold (insert (op =)) names;
-    fun new_node name (gr, (maxidx, idx_tab)) = if can (Graph.get_node gr) name
-      then (gr, (maxidx, idx_tab))
-      else (Graph.new_node (name, (NONE, maxidx)) gr,
+    fun new_node name (nbe_program, (maxidx, idx_tab)) = if can (Graph.get_node nbe_program) name
+      then (nbe_program, (maxidx, idx_tab))
+      else (Graph.new_node (name, (NONE, maxidx)) nbe_program,
         (maxidx + 1, Inttab.update_new (maxidx, name) idx_tab));
-    fun compile gr = eqnss
-      |> compile_eqnss ctxt gr refl_deps
-      |> rpair gr;
+    fun compile nbe_program = eqnss
+      |> compile_eqnss thy nbe_program refl_deps
+      |> rpair nbe_program;
   in
     fold new_node refl_deps
     #> apfst (fold (fn (name, deps) => fold (curry Graph.add_edge name) deps) names_deps
       #> compile
       #-> fold (fn (name, univ) => (Graph.map_node name o apfst) (K (SOME univ))))
   end;
 
-fun ensure_stmts ctxt 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),
+fun compile_program thy program =
+  let
+    fun add_stmts names (nbe_program, (maxidx, idx_tab)) = if exists ((can o Graph.get_node) nbe_program) names
+      then (nbe_program, (maxidx, idx_tab))
+      else (nbe_program, (maxidx, idx_tab))
+        |> compile_stmts thy (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;
 
 
 (** evaluation **)
 
-(* term evaluation *)
-
-fun eval_term ctxt gr deps (vs : (string * sort) list, t) =
+(* term evaluation by compilation *)
+
+fun compile_term thy nbe_program deps (vs : (string * sort) list, t) =
   let 
     val dict_frees = maps (fn (v, sort) => map_index (curry DFree v o fst) sort) vs;
   in
     ("", (vs, [([], t)]))
-    |> singleton (compile_eqnss ctxt gr deps)
+    |> singleton (compile_eqnss thy nbe_program deps)
     |> snd
     |> (fn t => apps t (rev dict_frees))
   end;
 
 
-(* reification *)
+(* reconstruction *)
 
 fun typ_of_itype program vs (ityco `%% itys) =
       let
         val Code_Thingol.Datatype (tyco, _) = Graph.get_node program ityco;
       in Type (tyco, map (typ_of_itype program vs) itys) end

           |> of_univ (bounds + 1) (apps t [BVar (bounds, [])])
           |-> (fn t' => pair (Term.Abs ("u", dummyT, t')))
   in of_univ 0 t 0 |> fst end;
 
 
-(* function store *)
-
-structure Nbe_Functions = Code_Data
-(
-  type T = (Univ option * int) Graph.T * (int * string Inttab.table);
-  val empty = (Graph.empty, (0, Inttab.empty));
-);
-
-
-(* compilation, evaluation and reification *)
-
-fun compile_eval thy program =
-  let
-    val ctxt = ProofContext.init_global thy;
-    val (gr, (_, idx_tab)) =
-      Nbe_Functions.change thy (ensure_stmts ctxt program);
-  in fn vs_t => fn deps =>
-    vs_t
-    |> eval_term ctxt gr deps
-    |> term_of_univ thy program idx_tab
-  end;
-
-
 (* evaluation with type reconstruction *)
 
-fun normalize thy program ((vs0, (vs, ty)), t) deps =
+fun eval_term thy program (nbe_program, idx_tab) ((vs0, (vs, ty)), t) deps =
   let
     val ctxt = Syntax.init_pretty_global thy;
+    val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt);
     val ty' = typ_of_itype program vs0 ty;
-    fun type_infer t =
-      singleton
-        (Type_Infer.infer_types ctxt (try (Type.strip_sorts o Sign.the_const_type thy)) (K NONE))
-        (Type.constraint ty' t);
-    val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt);
+    fun type_infer t = singleton
+      (Type_Infer.infer_types ctxt (try (Type.strip_sorts o Sign.the_const_type thy)) (K NONE))
+      (Type.constraint ty' t);
     fun check_tvars t =
       if null (Term.add_tvars t []) then t
       else error ("Illegal schematic type variables in normalized term: " ^ string_of_term t);
   in
-    compile_eval thy program (vs, t) deps
+    compile_term thy nbe_program deps (vs, t)
+    |> term_of_univ thy program idx_tab
     |> traced (fn t => "Normalized:\n" ^ string_of_term t)
     |> type_infer
     |> traced (fn t => "Types inferred:\n" ^ string_of_term t)
     |> check_tvars
     |> traced (fn _ => "---\n")
   end;
 
+(* function store *)
+
+structure Nbe_Functions = Code_Data
+(
+  type T = (Univ option * int) Graph.T * (int * string Inttab.table);
+  val empty = (Graph.empty, (0, Inttab.empty));
+);
+
+fun compile thy program =
+  let
+    val (nbe_program, (_, idx_tab)) =
+      Nbe_Functions.change thy (compile_program thy program);
+  in (nbe_program, idx_tab) end;
+
 
 (* evaluation oracle *)
 
 fun mk_equals thy lhs raw_rhs =
   let

     val rhs = Thm.cterm_of thy raw_rhs;
   in Thm.mk_binop eq lhs rhs end;
 
 val (_, raw_oracle) = Context.>>> (Context.map_theory_result
   (Thm.add_oracle (Binding.name "norm", fn (thy, program, vsp_ty_t, deps, ct) =>
-    mk_equals thy ct (normalize thy program vsp_ty_t deps))));
+    mk_equals thy ct (eval_term thy program (compile thy program) vsp_ty_t deps))));
 
 fun oracle thy program vsp_ty_t deps ct = raw_oracle (thy, program, vsp_ty_t, deps, ct);
 
 fun no_frees_rew rew t =
   let

 
 val dynamic_eval_conv = Code_Simp.no_frees_conv (Conv.tap_thy
   (fn thy => lift_triv_classes_conv thy (Code_Thingol.dynamic_eval_conv thy (K (oracle thy)))));
 
 fun dynamic_eval_value thy = lift_triv_classes_rew thy
-  (no_frees_rew (Code_Thingol.dynamic_eval_value thy I (K (normalize thy))));
+  (no_frees_rew (Code_Thingol.dynamic_eval_value thy I
+    (K (fn program => eval_term thy program (compile thy program)))));
 
 
 (* evaluation command *)
 
 fun norm_print_term ctxt modes t =