--- a/src/Tools/nbe.ML Tue Dec 14 00:16:30 2010 +0100
+++ b/src/Tools/nbe.ML Wed Dec 15 09:47:12 2010 +0100
@@ -6,9 +6,10 @@
signature NBE =
sig
- val dynamic_eval_conv: conv
- val dynamic_eval_value: theory -> term -> term
- val static_eval_conv: theory -> string list -> conv
+ val dynamic_conv: conv
+ val dynamic_value: theory -> term -> term
+ val static_conv: theory -> string list -> conv
+ val static_value: theory -> string list -> term -> term
datatype Univ =
Const of int * Univ list (*named (uninterpreted) constants*)
@@ -592,23 +593,28 @@
fun oracle thy program nbe_program_idx_tab vsp_ty_t deps ct =
raw_oracle (thy, program, nbe_program_idx_tab, vsp_ty_t, deps, ct);
-val dynamic_eval_conv = Conv.tap_thy (fn thy =>
- lift_triv_classes_conv thy (Code_Thingol.dynamic_eval_conv thy
+val dynamic_conv = Conv.tap_thy (fn thy =>
+ lift_triv_classes_conv thy (Code_Thingol.dynamic_conv thy
(K (fn program => oracle thy program (compile false thy program)))));
-fun dynamic_eval_value thy = lift_triv_classes_rew thy
- (Code_Thingol.dynamic_eval_value thy I
+fun dynamic_value thy = lift_triv_classes_rew thy
+ (Code_Thingol.dynamic_value thy I
(K (fn program => eval_term thy program (compile false thy program))));
-fun static_eval_conv thy consts =
- lift_triv_classes_conv thy (Code_Thingol.static_eval_conv thy consts
+fun static_conv thy consts =
+ lift_triv_classes_conv thy (Code_Thingol.static_conv thy consts
(K (fn program => let val nbe_program = compile true thy program
in fn thy => oracle thy program nbe_program end)));
+fun static_value thy consts = lift_triv_classes_rew thy
+ (Code_Thingol.static_value thy I consts
+ (K (fn program => let val nbe_program = compile true thy program
+ in fn thy => eval_term thy program (compile false thy program) end)));
+
(** setup **)
-val setup = Value.add_evaluator ("nbe", dynamic_eval_value o ProofContext.theory_of);
+val setup = Value.add_evaluator ("nbe", dynamic_value o ProofContext.theory_of);
end;
\ No newline at end of file