src/Tools/nbe.ML
changeset 27103 d8549f4d900b
parent 26970 bc28e7bcb765
child 27264 843472ae2116
     1.1 --- a/src/Tools/nbe.ML	Tue Jun 10 15:30:01 2008 +0200
     1.2 +++ b/src/Tools/nbe.ML	Tue Jun 10 15:30:06 2008 +0200
     1.3 @@ -277,14 +277,14 @@
     1.4        #-> fold (fn (name, univ) => (Graph.map_node name o apfst) (K (SOME univ))))
     1.5    end;
     1.6  
     1.7 -fun ensure_stmts code =
     1.8 +fun ensure_stmts program =
     1.9    let
    1.10      fun add_stmts names (gr, (maxidx, idx_tab)) = if exists ((can o Graph.get_node) gr) names
    1.11        then (gr, (maxidx, idx_tab))
    1.12        else (gr, (maxidx, idx_tab))
    1.13 -        |> compile_stmts (map (fn name => ((name, Graph.get_node code name),
    1.14 -          Graph.imm_succs code name)) names);
    1.15 -  in fold_rev add_stmts (Graph.strong_conn code) end;
    1.16 +        |> compile_stmts (map (fn name => ((name, Graph.get_node program name),
    1.17 +          Graph.imm_succs program name)) names);
    1.18 +  in fold_rev add_stmts (Graph.strong_conn program) end;
    1.19  
    1.20  
    1.21  (** evaluation **)
    1.22 @@ -364,9 +364,9 @@
    1.23  
    1.24  (* compilation, evaluation and reification *)
    1.25  
    1.26 -fun compile_eval thy code vs_ty_t deps =
    1.27 +fun compile_eval thy program vs_ty_t deps =
    1.28    let
    1.29 -    val (gr, (_, idx_tab)) = Nbe_Functions.change thy (ensure_stmts code);
    1.30 +    val (gr, (_, idx_tab)) = Nbe_Functions.change thy (ensure_stmts program);
    1.31    in
    1.32      vs_ty_t
    1.33      |> eval_term gr deps
    1.34 @@ -375,7 +375,7 @@
    1.35  
    1.36  (* evaluation with type reconstruction *)
    1.37  
    1.38 -fun eval thy t code vs_ty_t deps =
    1.39 +fun eval thy t program vs_ty_t deps =
    1.40    let
    1.41      fun subst_const f = map_aterms (fn t as Term.Const (c, ty) => Term.Const (f c, ty)
    1.42        | t => t);
    1.43 @@ -395,7 +395,7 @@
    1.44          ^ setmp show_types true (Syntax.string_of_term_global thy) t);
    1.45      val string_of_term = setmp show_types true (Syntax.string_of_term_global thy);
    1.46    in
    1.47 -    compile_eval thy code vs_ty_t deps
    1.48 +    compile_eval thy program vs_ty_t deps
    1.49      |> tracing (fn t => "Normalized:\n" ^ string_of_term t)
    1.50      |> subst_triv_consts
    1.51      |> type_frees
    1.52 @@ -408,14 +408,14 @@
    1.53  
    1.54  (* evaluation oracle *)
    1.55  
    1.56 -exception Norm of term * CodeThingol.code
    1.57 +exception Norm of term * CodeThingol.program
    1.58    * (CodeThingol.typscheme * CodeThingol.iterm) * string list;
    1.59  
    1.60 -fun norm_oracle (thy, Norm (t, code, vs_ty_t, deps)) =
    1.61 -  Logic.mk_equals (t, eval thy t code vs_ty_t deps);
    1.62 +fun norm_oracle (thy, Norm (t, program, vs_ty_t, deps)) =
    1.63 +  Logic.mk_equals (t, eval thy t program vs_ty_t deps);
    1.64  
    1.65 -fun norm_invoke thy t code vs_ty_t deps =
    1.66 -  Thm.invoke_oracle_i thy "HOL.norm" (thy, Norm (t, code, vs_ty_t, deps));
    1.67 +fun norm_invoke thy t program vs_ty_t deps =
    1.68 +  Thm.invoke_oracle_i thy "HOL.norm" (thy, Norm (t, program, vs_ty_t, deps));
    1.69    (*FIXME get rid of hardwired theory name*)
    1.70  
    1.71  fun add_triv_classes thy =
    1.72 @@ -430,15 +430,15 @@
    1.73  fun norm_conv ct =
    1.74    let
    1.75      val thy = Thm.theory_of_cterm ct;
    1.76 -    fun evaluator' t code vs_ty_t deps = norm_invoke thy t code vs_ty_t deps;
    1.77 +    fun evaluator' t program vs_ty_t deps = norm_invoke thy t program vs_ty_t deps;
    1.78      fun evaluator t = (add_triv_classes thy t, evaluator' t);
    1.79 -  in CodePackage.evaluate_conv thy evaluator ct end;
    1.80 +  in CodeThingol.eval_conv thy evaluator ct end;
    1.81  
    1.82  fun norm_term thy t =
    1.83    let
    1.84 -    fun evaluator' t code vs_ty_t deps = eval thy t code vs_ty_t deps;
    1.85 +    fun evaluator' t program vs_ty_t deps = eval thy t program vs_ty_t deps;
    1.86      fun evaluator t = (add_triv_classes thy t, evaluator' t);
    1.87 -  in (Code.postprocess_term thy o CodePackage.evaluate_term thy evaluator) t end;
    1.88 +  in (Code.postprocess_term thy o CodeThingol.eval_term thy evaluator) t end;
    1.89  
    1.90  (* evaluation command *)
    1.91