1.1 --- a/src/Tools/Code/code_simp.ML	Mon Aug 23 11:09:48 2010 +0200
     1.2 +++ b/src/Tools/Code/code_simp.ML	Mon Aug 23 11:09:49 2010 +0200
     1.3 @@ -8,11 +8,11 @@
     1.4  sig
     1.5    val no_frees_conv: conv -> conv
     1.6    val map_ss: (simpset -> simpset) -> theory -> theory
     1.7 -  val current_conv: theory -> conv
     1.8 -  val current_tac: theory -> int -> tactic
     1.9 -  val current_value: theory -> term -> term
    1.10 -  val make_conv: theory -> simpset option -> string list -> conv
    1.11 -  val make_tac: theory -> simpset option -> string list -> int -> tactic
    1.12 +  val dynamic_eval_conv: theory -> conv
    1.13 +  val dynamic_eval_tac: theory -> int -> tactic
    1.14 +  val dynamic_eval_value: theory -> term -> term
    1.15 +  val static_eval_conv: theory -> simpset option -> string list -> conv
    1.16 +  val static_eval_tac: theory -> simpset option -> string list -> int -> tactic
    1.17    val setup: theory -> theory
    1.18  end;
    1.19  
    1.20 @@ -67,25 +67,25 @@
    1.21  
    1.22  (* evaluation with current code context *)
    1.23  
    1.24 -fun current_conv thy = no_frees_conv (Code_Thingol.eval_conv thy
    1.25 +fun dynamic_eval_conv thy = no_frees_conv (Code_Thingol.dynamic_eval_conv thy
    1.26    (fn naming => fn program => fn t => fn deps => rewrite_modulo thy NONE program));
    1.27  
    1.28 -fun current_tac thy = CONVERSION (current_conv thy) THEN' conclude_tac thy NONE;
    1.29 +fun dynamic_eval_tac thy = CONVERSION (dynamic_eval_conv thy) THEN' conclude_tac thy NONE;
    1.30  
    1.31 -fun current_value thy = snd o Logic.dest_equals o Thm.prop_of o current_conv thy o Thm.cterm_of thy;
    1.32 +fun dynamic_eval_value thy = snd o Logic.dest_equals o Thm.prop_of o dynamic_eval_conv thy o Thm.cterm_of thy;
    1.33  
    1.34  val setup = Method.setup (Binding.name "code_simp")
    1.35 -  (Scan.succeed (SIMPLE_METHOD' o (CHANGED_PROP oo current_tac o ProofContext.theory_of)))
    1.36 +  (Scan.succeed (SIMPLE_METHOD' o (CHANGED_PROP oo dynamic_eval_tac o ProofContext.theory_of)))
    1.37    "simplification with code equations"
    1.38 -  #> Value.add_evaluator ("simp", current_value o ProofContext.theory_of);
    1.39 +  #> Value.add_evaluator ("simp", dynamic_eval_value o ProofContext.theory_of);
    1.40  
    1.41  
    1.42  (* evaluation with freezed code context *)
    1.43  
    1.44 -fun make_conv thy some_ss consts = no_frees_conv (Code_Preproc.pre_post_conv thy
    1.45 +fun static_eval_conv thy some_ss consts = no_frees_conv (Code_Preproc.pre_post_conv thy
    1.46    ((rewrite_modulo thy some_ss o snd o snd o Code_Thingol.consts_program thy false) consts));
    1.47  
    1.48 -fun make_tac thy some_ss consts = CONVERSION (make_conv thy some_ss consts)
    1.49 +fun static_eval_tac thy some_ss consts = CONVERSION (static_eval_conv thy some_ss consts)
    1.50    THEN' conclude_tac thy some_ss;
    1.51  
    1.52  end;