# HG changeset patch
# User haftmann
# Date 1292488006 -3600
# Node ID b0b975e197b5e72f3e7d075db9c4163366e8468e
# Parent  e20f0d0e2af390bffb043433ab6362c96734c135# Parent  08a54d394e36b06f16841f15bcbaaf0795c1a3b6
merged

diff -r e20f0d0e2af3 -r b0b975e197b5 doc-src/Codegen/Thy/Evaluation.thy
--- a/doc-src/Codegen/Thy/Evaluation.thy	Thu Dec 16 09:10:38 2010 +0100
+++ b/doc-src/Codegen/Thy/Evaluation.thy	Thu Dec 16 09:26:46 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}
 *}
 
diff -r e20f0d0e2af3 -r b0b975e197b5 doc-src/Codegen/Thy/document/Evaluation.tex
--- a/doc-src/Codegen/Thy/document/Evaluation.tex	Thu Dec 16 09:10:38 2010 +0100
+++ b/doc-src/Codegen/Thy/document/Evaluation.tex	Thu Dec 16 09:26:46 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%
diff -r e20f0d0e2af3 -r b0b975e197b5 doc-src/Codegen/Thy/examples/Example.hs
--- a/doc-src/Codegen/Thy/examples/Example.hs	Thu Dec 16 09:10:38 2010 +0100
+++ b/doc-src/Codegen/Thy/examples/Example.hs	Thu Dec 16 09:26:46 2010 +0100
@@ -1,4 +1,4 @@
-{-# OPTIONS_GHC -fglasgow-exts #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 
 module Example where {
 
diff -r e20f0d0e2af3 -r b0b975e197b5 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Thu Dec 16 09:10:38 2010 +0100
+++ b/src/HOL/HOL.thy	Thu Dec 16 09:26:46 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"
 
 
diff -r e20f0d0e2af3 -r b0b975e197b5 src/HOL/Tools/code_evaluation.ML
--- a/src/HOL/Tools/code_evaluation.ML	Thu Dec 16 09:10:38 2010 +0100
+++ b/src/HOL/Tools/code_evaluation.ML	Thu Dec 16 09:26:46 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;
diff -r e20f0d0e2af3 -r b0b975e197b5 src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Thu Dec 16 09:10:38 2010 +0100
+++ b/src/Tools/Code/code_preproc.ML	Thu Dec 16 09:26:46 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;
diff -r e20f0d0e2af3 -r b0b975e197b5 src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Thu Dec 16 09:10:38 2010 +0100
+++ b/src/Tools/Code/code_runtime.ML	Thu Dec 16 09:26:46 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;
diff -r e20f0d0e2af3 -r b0b975e197b5 src/Tools/Code/code_simp.ML
--- a/src/Tools/Code/code_simp.ML	Thu Dec 16 09:10:38 2010 +0100
+++ b/src/Tools/Code/code_simp.ML	Thu Dec 16 09:26:46 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;
diff -r e20f0d0e2af3 -r b0b975e197b5 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Thu Dec 16 09:10:38 2010 +0100
+++ b/src/Tools/Code/code_thingol.ML	Thu Dec 16 09:26:46 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));
 
 
diff -r e20f0d0e2af3 -r b0b975e197b5 src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Thu Dec 16 09:10:38 2010 +0100
+++ b/src/Tools/nbe.ML	Thu Dec 16 09:26:46 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