--- a/doc-src/Codegen/Thy/Evaluation.thy Wed Dec 15 08:34:01 2010 +0100
+++ b/doc-src/Codegen/Thy/Evaluation.thy Wed Dec 15 10:15:55 2010 +0100
@@ -174,15 +174,15 @@
& plain evaluation & & & \ttsize@{ML "Code_Evaluation.dynamic_value"} \tabularnewline \cline{2-5}
& evaluation method & @{method code_simp} & @{method normalization} & @{method eval} \tabularnewline
& property conversion & & & \ttsize@{ML "Code_Runtime.dynamic_holds_conv"} \tabularnewline \cline{2-5}
- & conversion & \ttsize@{ML "Code_Simp.dynamic_eval_conv"} & \ttsize@{ML "Nbe.dynamic_eval_conv"}
- & \ttsize@{ML "Code_Evaluation.dynamic_eval_conv"} \tabularnewline \hline \hline
+ & conversion & \ttsize@{ML "Code_Simp.dynamic_conv"} & \ttsize@{ML "Nbe.dynamic_conv"}
+ & \ttsize@{ML "Code_Evaluation.dynamic_conv"} \tabularnewline \hline \hline
\multirow{3}{1ex}{\rotatebox{90}{static}}
- & plain evaluation & & & \ttsize@{ML "Code_Evaluation.static_value"} \tabularnewline \cline{2-5}
+ & plain evaluation & & & \ttsize@{ML "Code_Evaluation.static_value"} \tabularnewline \cline{2-5}
& property conversion & &
& \ttsize@{ML "Code_Runtime.static_holds_conv"} \tabularnewline \cline{2-5}
- & conversion & \ttsize@{ML "Code_Simp.static_eval_conv"}
- & \ttsize@{ML "Nbe.static_eval_conv"}
- & \ttsize@{ML "Code_Evaluation.static_eval_conv"}
+ & conversion & \ttsize@{ML "Code_Simp.static_conv"}
+ & \ttsize@{ML "Nbe.static_conv"}
+ & \ttsize@{ML "Code_Evaluation.static_conv"}
\end{tabular}
*}
--- a/doc-src/Codegen/Thy/document/Evaluation.tex Wed Dec 15 08:34:01 2010 +0100
+++ b/doc-src/Codegen/Thy/document/Evaluation.tex Wed Dec 15 10:15:55 2010 +0100
@@ -228,15 +228,15 @@
& plain evaluation & & & \ttsize\verb|Code_Evaluation.dynamic_value| \tabularnewline \cline{2-5}
& evaluation method & \hyperlink{method.code-simp}{\mbox{\isa{code{\isaliteral{5F}{\isacharunderscore}}simp}}} & \hyperlink{method.normalization}{\mbox{\isa{normalization}}} & \hyperlink{method.eval}{\mbox{\isa{eval}}} \tabularnewline
& property conversion & & & \ttsize\verb|Code_Runtime.dynamic_holds_conv| \tabularnewline \cline{2-5}
- & conversion & \ttsize\verb|Code_Simp.dynamic_eval_conv| & \ttsize\verb|Nbe.dynamic_eval_conv|
- & \ttsize\verb|Code_Evaluation.dynamic_eval_conv| \tabularnewline \hline \hline
+ & conversion & \ttsize\verb|Code_Simp.dynamic_conv| & \ttsize\verb|Nbe.dynamic_conv|
+ & \ttsize\verb|Code_Evaluation.dynamic_conv| \tabularnewline \hline \hline
\multirow{3}{1ex}{\rotatebox{90}{static}}
- & plain evaluation & & & \ttsize\verb|Code_Evaluation.static_value| \tabularnewline \cline{2-5}
+ & plain evaluation & & & \ttsize\verb|Code_Evaluation.static_value| \tabularnewline \cline{2-5}
& property conversion & &
& \ttsize\verb|Code_Runtime.static_holds_conv| \tabularnewline \cline{2-5}
- & conversion & \ttsize\verb|Code_Simp.static_eval_conv|
- & \ttsize\verb|Nbe.static_eval_conv|
- & \ttsize\verb|Code_Evaluation.static_eval_conv|
+ & conversion & \ttsize\verb|Code_Simp.static_conv|
+ & \ttsize\verb|Nbe.static_conv|
+ & \ttsize\verb|Code_Evaluation.static_conv|
\end{tabular}%
\end{isamarkuptext}%
\isamarkuptrue%
--- a/doc-src/Codegen/Thy/examples/Example.hs Wed Dec 15 08:34:01 2010 +0100
+++ b/doc-src/Codegen/Thy/examples/Example.hs Wed Dec 15 10:15:55 2010 +0100
@@ -1,4 +1,4 @@
-{-# OPTIONS_GHC -fglasgow-exts #-}
+{-# LANGUAGE ScopedTypeVariables #-}
module Example where {
--- a/src/HOL/HOL.thy Wed Dec 15 08:34:01 2010 +0100
+++ b/src/HOL/HOL.thy Wed Dec 15 10:15:55 2010 +0100
@@ -1976,7 +1976,7 @@
method_setup normalization = {*
Scan.succeed (K (SIMPLE_METHOD'
- (CHANGED_PROP o (CONVERSION Nbe.dynamic_eval_conv THEN' (fn k => TRY (rtac TrueI k))))))
+ (CHANGED_PROP o (CONVERSION Nbe.dynamic_conv THEN' (fn k => TRY (rtac TrueI k))))))
*} "solve goal by normalization"
--- a/src/HOL/Tools/code_evaluation.ML Wed Dec 15 08:34:01 2010 +0100
+++ b/src/HOL/Tools/code_evaluation.ML Wed Dec 15 10:15:55 2010 +0100
@@ -12,8 +12,8 @@
val static_value: theory -> string list -> typ list -> term -> term option
val static_value_strict: theory -> string list -> typ list -> term -> term
val static_value_exn: theory -> string list -> typ list -> term -> term Exn.result
- val dynamic_eval_conv: conv
- val static_eval_conv: theory -> string list -> typ list -> conv
+ val dynamic_conv: conv
+ val static_conv: theory -> string list -> typ list -> conv
val put_term: (unit -> term) -> Proof.context -> Proof.context
val tracing: string -> 'a -> 'a
val setup: theory -> theory
@@ -194,10 +194,10 @@
error ("Failed to certify evaluation result of " ^ Syntax.string_of_term_global thy t)
end;
-val dynamic_eval_conv = Conv.tap_thy
+val dynamic_conv = Conv.tap_thy
(fn thy => certify_eval thy (dynamic_value thy) Code_Runtime.dynamic_holds_conv);
-fun static_eval_conv thy consts Ts =
+fun static_conv thy consts Ts =
let
val eqs = "==" :: @{const_name HOL.eq} ::
map (fn T => AxClass.unoverload_const thy (@{const_name HOL.equal}, T)) Ts;
--- a/src/Tools/Code/code_preproc.ML Wed Dec 15 08:34:01 2010 +0100
+++ b/src/Tools/Code/code_preproc.ML Wed Dec 15 10:15:55 2010 +0100
@@ -24,13 +24,13 @@
val all: code_graph -> string list
val pretty: theory -> code_graph -> Pretty.T
val obtain: bool -> theory -> string list -> term list -> code_algebra * code_graph
- val dynamic_eval_conv: theory
+ val dynamic_conv: theory
-> (code_algebra -> code_graph -> (string * sort) list -> term -> conv) -> conv
- val dynamic_eval_value: theory -> ((term -> term) -> 'a -> 'a)
+ val dynamic_value: theory -> ((term -> term) -> 'a -> 'a)
-> (code_algebra -> code_graph -> (string * sort) list -> term -> 'a) -> term -> 'a
- val static_eval_conv: theory -> string list
+ val static_conv: theory -> string list
-> (code_algebra -> code_graph -> theory -> (string * sort) list -> term -> conv) -> conv
- val static_eval_value: theory -> ((term -> term) -> 'a -> 'a) -> string list
+ val static_value: theory -> ((term -> term) -> 'a -> 'a) -> string list
-> (code_algebra -> code_graph -> theory -> (string * sort) list -> term -> 'a) -> term -> 'a
val setup: theory -> theory
@@ -457,7 +457,7 @@
fun dest_cterm ct = let val t = Thm.term_of ct in (Term.add_tfrees t [], t) end;
-fun dynamic_eval_conv thy conv = no_variables_conv (fn ct =>
+fun dynamic_conv thy conv = no_variables_conv (fn ct =>
let
val thm1 = preprocess_conv thy ct;
val ct' = Thm.rhs_of thm1;
@@ -473,7 +473,7 @@
^ (cat_lines o map (Display.string_of_thm_global thy)) [thm1, thm2, thm3])
end);
-fun dynamic_eval_value thy postproc evaluator t =
+fun dynamic_value thy postproc evaluator t =
let
val (resubst, t') = preprocess_term thy t;
val vs' = Term.add_tfrees t' [];
@@ -486,7 +486,7 @@
|> postproc (postprocess_term thy o resubst)
end;
-fun static_eval_conv thy consts conv =
+fun static_conv thy consts conv =
let
val (algebra, eqngr) = obtain true thy consts [];
val conv' = conv algebra eqngr;
@@ -496,7 +496,7 @@
then_conv (postprocess_conv thy)))
end;
-fun static_eval_value thy postproc consts evaluator =
+fun static_value thy postproc consts evaluator =
let
val (algebra, eqngr) = obtain true thy consts [];
val evaluator' = evaluator algebra eqngr;
--- a/src/Tools/Code/code_runtime.ML Wed Dec 15 08:34:01 2010 +0100
+++ b/src/Tools/Code/code_runtime.ML Wed Dec 15 10:15:55 2010 +0100
@@ -120,7 +120,7 @@
else ()
fun evaluator naming program ((_, vs_ty), t) deps =
base_evaluator cookie (obtain_serializer thy some_target) naming thy program (vs_ty, t) deps args;
- in Code_Thingol.dynamic_eval_value thy (Exn.map_result o postproc) evaluator t end;
+ in Code_Thingol.dynamic_value thy (Exn.map_result o postproc) evaluator t end;
fun dynamic_value_strict cookie thy some_target postproc t args =
Exn.release (dynamic_value_exn cookie thy some_target postproc t args);
@@ -133,7 +133,7 @@
val serializer = obtain_serializer thy some_target;
fun evaluator naming program thy ((_, vs_ty), t) deps =
base_evaluator cookie serializer naming thy program (vs_ty, t) deps [];
- in Code_Thingol.static_eval_value thy (Exn.map_result o postproc) consts evaluator o reject_vars thy end;
+ in Code_Thingol.static_value thy (Exn.map_result o postproc) consts evaluator o reject_vars thy end;
fun static_value_strict cookie thy some_target postproc consts t =
Exn.release (static_value_exn cookie thy some_target postproc consts t);
@@ -175,7 +175,7 @@
fun check_holds_oracle serializer naming thy program ((_, vs_ty), t) deps ct =
raw_check_holds_oracle (serializer, naming, thy, program, (vs_ty, t), deps, ct);
-val dynamic_holds_conv = Conv.tap_thy (fn thy => Code_Thingol.dynamic_eval_conv thy
+val dynamic_holds_conv = Conv.tap_thy (fn thy => Code_Thingol.dynamic_conv thy
(fn naming => check_holds_oracle (obtain_serializer thy NONE) naming thy)
o reject_vars thy);
@@ -183,7 +183,7 @@
let
val serializer = obtain_serializer thy NONE;
in
- Code_Thingol.static_eval_conv thy consts
+ Code_Thingol.static_conv thy consts
(fn naming => fn program => fn thy => check_holds_oracle serializer naming thy program)
o reject_vars thy
end;
--- a/src/Tools/Code/code_simp.ML Wed Dec 15 08:34:01 2010 +0100
+++ b/src/Tools/Code/code_simp.ML Wed Dec 15 10:15:55 2010 +0100
@@ -7,10 +7,10 @@
signature CODE_SIMP =
sig
val map_ss: (simpset -> simpset) -> theory -> theory
- val dynamic_eval_conv: conv
+ val dynamic_conv: conv
val dynamic_eval_tac: theory -> int -> tactic
- val dynamic_eval_value: theory -> term -> term
- val static_eval_conv: theory -> simpset option -> string list -> conv
+ val dynamic_value: theory -> term -> term
+ val static_conv: theory -> simpset option -> string list -> conv
val static_eval_tac: theory -> simpset option -> string list -> int -> tactic
val setup: theory -> theory
end;
@@ -51,26 +51,26 @@
(* evaluation with dynamic code context *)
-val dynamic_eval_conv = Conv.tap_thy (fn thy => Code_Thingol.dynamic_eval_conv thy
+val dynamic_conv = Conv.tap_thy (fn thy => Code_Thingol.dynamic_conv thy
(fn naming => fn program => fn t => fn deps => rewrite_modulo thy NONE program));
-fun dynamic_eval_tac thy = CONVERSION dynamic_eval_conv THEN' conclude_tac thy NONE;
+fun dynamic_eval_tac thy = CONVERSION dynamic_conv THEN' conclude_tac thy NONE;
-fun dynamic_eval_value thy = snd o Logic.dest_equals o Thm.prop_of o dynamic_eval_conv o Thm.cterm_of thy;
+fun dynamic_value thy = snd o Logic.dest_equals o Thm.prop_of o dynamic_conv o Thm.cterm_of thy;
val setup = Method.setup (Binding.name "code_simp")
(Scan.succeed (SIMPLE_METHOD' o (CHANGED_PROP oo dynamic_eval_tac o ProofContext.theory_of)))
"simplification with code equations"
- #> Value.add_evaluator ("simp", dynamic_eval_value o ProofContext.theory_of);
+ #> Value.add_evaluator ("simp", dynamic_value o ProofContext.theory_of);
(* evaluation with static code context *)
-fun static_eval_conv thy some_ss consts =
- Code_Thingol.static_eval_conv_simple thy consts
+fun static_conv thy some_ss consts =
+ Code_Thingol.static_conv_simple thy consts
(fn program => fn thy => fn _ => fn _ => rewrite_modulo thy some_ss program);
-fun static_eval_tac thy some_ss consts = CONVERSION (static_eval_conv thy some_ss consts)
+fun static_eval_tac thy some_ss consts = CONVERSION (static_conv thy some_ss consts)
THEN' conclude_tac thy some_ss;
end;
--- a/src/Tools/Code/code_thingol.ML Wed Dec 15 08:34:01 2010 +0100
+++ b/src/Tools/Code/code_thingol.ML Wed Dec 15 10:15:55 2010 +0100
@@ -94,18 +94,18 @@
val read_const_exprs: theory -> string list -> string list * string list
val consts_program: theory -> bool -> string list -> string list * (naming * program)
- val dynamic_eval_conv: theory -> (naming -> program
+ val dynamic_conv: theory -> (naming -> program
-> ((string * sort) list * typscheme) * iterm -> string list -> conv)
-> conv
- val dynamic_eval_value: theory -> ((term -> term) -> 'a -> 'a) -> (naming -> program
+ val dynamic_value: theory -> ((term -> term) -> 'a -> 'a) -> (naming -> program
-> ((string * sort) list * typscheme) * iterm -> string list -> 'a)
-> term -> 'a
- val static_eval_conv: theory -> string list -> (naming -> program
+ val static_conv: theory -> string list -> (naming -> program
-> theory -> ((string * sort) list * typscheme) * iterm -> string list -> conv)
-> conv
- val static_eval_conv_simple: theory -> string list
+ val static_conv_simple: theory -> string list
-> (program -> theory -> (string * sort) list -> term -> conv) -> conv
- val static_eval_value: theory -> ((term -> term) -> 'a -> 'a) -> string list ->
+ val static_value: theory -> ((term -> term) -> 'a -> 'a) -> string list ->
(naming -> program
-> theory -> ((string * sort) list * typscheme) * iterm -> string list -> 'a)
-> term -> 'a
@@ -906,11 +906,11 @@
invoke_generation false thy (algebra, eqngr) ensure_value t;
in evaluator naming program ((original_sorts vs vs', (vs', ty')), t') deps end;
-fun dynamic_eval_conv thy evaluator =
- Code_Preproc.dynamic_eval_conv thy (dynamic_evaluator thy evaluator);
+fun dynamic_conv thy evaluator =
+ Code_Preproc.dynamic_conv thy (dynamic_evaluator thy evaluator);
-fun dynamic_eval_value thy postproc evaluator =
- Code_Preproc.dynamic_eval_value thy postproc (dynamic_evaluator thy evaluator);
+fun dynamic_value thy postproc evaluator =
+ Code_Preproc.dynamic_value thy postproc (dynamic_evaluator thy evaluator);
fun provide_program thy consts f algebra eqngr =
let
@@ -926,16 +926,16 @@
ensure_value thy algebra eqngr t (NONE, (naming, program));
in evaluator naming program' thy ((original_sorts vs vs', (vs', ty')), t') deps end;
-fun static_eval_conv thy consts conv =
- Code_Preproc.static_eval_conv thy consts
+fun static_conv thy consts conv =
+ Code_Preproc.static_conv thy consts
(provide_program thy consts (static_evaluator conv));
-fun static_eval_conv_simple thy consts conv =
- Code_Preproc.static_eval_conv thy consts
+fun static_conv_simple thy consts conv =
+ Code_Preproc.static_conv thy consts
(provide_program thy consts ((K o K o K) conv));
-fun static_eval_value thy postproc consts evaluator =
- Code_Preproc.static_eval_value thy postproc consts
+fun static_value thy postproc consts evaluator =
+ Code_Preproc.static_value thy postproc consts
(provide_program thy consts (static_evaluator evaluator));
--- a/src/Tools/nbe.ML Wed Dec 15 08:34:01 2010 +0100
+++ b/src/Tools/nbe.ML Wed Dec 15 10:15:55 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