simplified evaluation function names
authorhaftmann
Wed Dec 15 09:47:12 2010 +0100 (2010-12-15)
changeset 411845c6f44d22f51
parent 41119 573f557ed716
child 41185 d5f0e556ffd3
simplified evaluation function names
doc-src/Codegen/Thy/Evaluation.thy
doc-src/Codegen/Thy/document/Evaluation.tex
src/HOL/HOL.thy
src/HOL/Tools/code_evaluation.ML
src/Tools/Code/code_preproc.ML
src/Tools/Code/code_runtime.ML
src/Tools/Code/code_simp.ML
src/Tools/Code/code_thingol.ML
src/Tools/nbe.ML
     1.1 --- a/doc-src/Codegen/Thy/Evaluation.thy	Tue Dec 14 00:16:30 2010 +0100
     1.2 +++ b/doc-src/Codegen/Thy/Evaluation.thy	Wed Dec 15 09:47:12 2010 +0100
     1.3 @@ -174,15 +174,15 @@
     1.4      & plain evaluation & & & \ttsize@{ML "Code_Evaluation.dynamic_value"} \tabularnewline \cline{2-5}
     1.5      & evaluation method & @{method code_simp} & @{method normalization} & @{method eval} \tabularnewline
     1.6      & property conversion & & & \ttsize@{ML "Code_Runtime.dynamic_holds_conv"} \tabularnewline \cline{2-5}
     1.7 -    & conversion & \ttsize@{ML "Code_Simp.dynamic_eval_conv"} & \ttsize@{ML "Nbe.dynamic_eval_conv"}
     1.8 -      & \ttsize@{ML "Code_Evaluation.dynamic_eval_conv"} \tabularnewline \hline \hline
     1.9 +    & conversion & \ttsize@{ML "Code_Simp.dynamic_conv"} & \ttsize@{ML "Nbe.dynamic_conv"}
    1.10 +      & \ttsize@{ML "Code_Evaluation.dynamic_conv"} \tabularnewline \hline \hline
    1.11      \multirow{3}{1ex}{\rotatebox{90}{static}}
    1.12 -      & plain evaluation & & & \ttsize@{ML "Code_Evaluation.static_value"} \tabularnewline \cline{2-5}
    1.13 +    & plain evaluation & & & \ttsize@{ML "Code_Evaluation.static_value"} \tabularnewline \cline{2-5}
    1.14      & property conversion & &
    1.15        & \ttsize@{ML "Code_Runtime.static_holds_conv"} \tabularnewline \cline{2-5}
    1.16 -    & conversion & \ttsize@{ML "Code_Simp.static_eval_conv"}
    1.17 -      & \ttsize@{ML "Nbe.static_eval_conv"}
    1.18 -      & \ttsize@{ML "Code_Evaluation.static_eval_conv"}
    1.19 +    & conversion & \ttsize@{ML "Code_Simp.static_conv"}
    1.20 +      & \ttsize@{ML "Nbe.static_conv"}
    1.21 +      & \ttsize@{ML "Code_Evaluation.static_conv"}
    1.22    \end{tabular}
    1.23  *}
    1.24  
     2.1 --- a/doc-src/Codegen/Thy/document/Evaluation.tex	Tue Dec 14 00:16:30 2010 +0100
     2.2 +++ b/doc-src/Codegen/Thy/document/Evaluation.tex	Wed Dec 15 09:47:12 2010 +0100
     2.3 @@ -228,15 +228,15 @@
     2.4      & plain evaluation & & & \ttsize\verb|Code_Evaluation.dynamic_value| \tabularnewline \cline{2-5}
     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
     2.6      & property conversion & & & \ttsize\verb|Code_Runtime.dynamic_holds_conv| \tabularnewline \cline{2-5}
     2.7 -    & conversion & \ttsize\verb|Code_Simp.dynamic_eval_conv| & \ttsize\verb|Nbe.dynamic_eval_conv|
     2.8 -      & \ttsize\verb|Code_Evaluation.dynamic_eval_conv| \tabularnewline \hline \hline
     2.9 +    & conversion & \ttsize\verb|Code_Simp.dynamic_conv| & \ttsize\verb|Nbe.dynamic_conv|
    2.10 +      & \ttsize\verb|Code_Evaluation.dynamic_conv| \tabularnewline \hline \hline
    2.11      \multirow{3}{1ex}{\rotatebox{90}{static}}
    2.12        & plain evaluation & & & \ttsize\verb|Code_Evaluation.static_value| \tabularnewline \cline{2-5}
    2.13      & property conversion & &
    2.14        & \ttsize\verb|Code_Runtime.static_holds_conv| \tabularnewline \cline{2-5}
    2.15 -    & conversion & \ttsize\verb|Code_Simp.static_eval_conv|
    2.16 -      & \ttsize\verb|Nbe.static_eval_conv|
    2.17 -      & \ttsize\verb|Code_Evaluation.static_eval_conv|
    2.18 +    & conversion & \ttsize\verb|Code_Simp.static_conv|
    2.19 +      & \ttsize\verb|Nbe.static_conv|
    2.20 +      & \ttsize\verb|Code_Evaluation.static_conv|
    2.21    \end{tabular}%
    2.22  \end{isamarkuptext}%
    2.23  \isamarkuptrue%
     3.1 --- a/src/HOL/HOL.thy	Tue Dec 14 00:16:30 2010 +0100
     3.2 +++ b/src/HOL/HOL.thy	Wed Dec 15 09:47:12 2010 +0100
     3.3 @@ -1976,7 +1976,7 @@
     3.4  
     3.5  method_setup normalization = {*
     3.6    Scan.succeed (K (SIMPLE_METHOD'
     3.7 -    (CHANGED_PROP o (CONVERSION Nbe.dynamic_eval_conv THEN' (fn k => TRY (rtac TrueI k))))))
     3.8 +    (CHANGED_PROP o (CONVERSION Nbe.dynamic_conv THEN' (fn k => TRY (rtac TrueI k))))))
     3.9  *} "solve goal by normalization"
    3.10  
    3.11  
     4.1 --- a/src/HOL/Tools/code_evaluation.ML	Tue Dec 14 00:16:30 2010 +0100
     4.2 +++ b/src/HOL/Tools/code_evaluation.ML	Wed Dec 15 09:47:12 2010 +0100
     4.3 @@ -12,8 +12,8 @@
     4.4    val static_value: theory -> string list -> typ list -> term -> term option
     4.5    val static_value_strict: theory -> string list -> typ list -> term -> term
     4.6    val static_value_exn: theory -> string list -> typ list -> term -> term Exn.result
     4.7 -  val dynamic_eval_conv: conv
     4.8 -  val static_eval_conv: theory -> string list -> typ list -> conv
     4.9 +  val dynamic_conv: conv
    4.10 +  val static_conv: theory -> string list -> typ list -> conv
    4.11    val put_term: (unit -> term) -> Proof.context -> Proof.context
    4.12    val tracing: string -> 'a -> 'a
    4.13    val setup: theory -> theory
    4.14 @@ -194,10 +194,10 @@
    4.15            error ("Failed to certify evaluation result of " ^ Syntax.string_of_term_global thy t)
    4.16    end;
    4.17  
    4.18 -val dynamic_eval_conv = Conv.tap_thy
    4.19 +val dynamic_conv = Conv.tap_thy
    4.20    (fn thy => certify_eval thy (dynamic_value thy) Code_Runtime.dynamic_holds_conv);
    4.21  
    4.22 -fun static_eval_conv thy consts Ts =
    4.23 +fun static_conv thy consts Ts =
    4.24    let
    4.25      val eqs = "==" :: @{const_name HOL.eq} ::
    4.26        map (fn T => AxClass.unoverload_const thy (@{const_name HOL.equal}, T)) Ts;
     5.1 --- a/src/Tools/Code/code_preproc.ML	Tue Dec 14 00:16:30 2010 +0100
     5.2 +++ b/src/Tools/Code/code_preproc.ML	Wed Dec 15 09:47:12 2010 +0100
     5.3 @@ -24,13 +24,13 @@
     5.4    val all: code_graph -> string list
     5.5    val pretty: theory -> code_graph -> Pretty.T
     5.6    val obtain: bool -> theory -> string list -> term list -> code_algebra * code_graph
     5.7 -  val dynamic_eval_conv: theory
     5.8 +  val dynamic_conv: theory
     5.9      -> (code_algebra -> code_graph -> (string * sort) list -> term -> conv) -> conv
    5.10 -  val dynamic_eval_value: theory -> ((term -> term) -> 'a -> 'a)
    5.11 +  val dynamic_value: theory -> ((term -> term) -> 'a -> 'a)
    5.12      -> (code_algebra -> code_graph -> (string * sort) list -> term -> 'a) -> term -> 'a
    5.13 -  val static_eval_conv: theory -> string list
    5.14 +  val static_conv: theory -> string list
    5.15      -> (code_algebra -> code_graph -> theory -> (string * sort) list -> term -> conv) -> conv
    5.16 -  val static_eval_value: theory -> ((term -> term) -> 'a -> 'a) -> string list
    5.17 +  val static_value: theory -> ((term -> term) -> 'a -> 'a) -> string list
    5.18      -> (code_algebra -> code_graph -> theory -> (string * sort) list -> term -> 'a) -> term -> 'a
    5.19  
    5.20    val setup: theory -> theory
    5.21 @@ -457,7 +457,7 @@
    5.22  
    5.23  fun dest_cterm ct = let val t = Thm.term_of ct in (Term.add_tfrees t [], t) end;
    5.24  
    5.25 -fun dynamic_eval_conv thy conv = no_variables_conv (fn ct =>
    5.26 +fun dynamic_conv thy conv = no_variables_conv (fn ct =>
    5.27    let
    5.28      val thm1 = preprocess_conv thy ct;
    5.29      val ct' = Thm.rhs_of thm1;
    5.30 @@ -473,7 +473,7 @@
    5.31        ^ (cat_lines o map (Display.string_of_thm_global thy)) [thm1, thm2, thm3])
    5.32    end);
    5.33  
    5.34 -fun dynamic_eval_value thy postproc evaluator t =
    5.35 +fun dynamic_value thy postproc evaluator t =
    5.36    let
    5.37      val (resubst, t') = preprocess_term thy t;
    5.38      val vs' = Term.add_tfrees t' [];
    5.39 @@ -486,7 +486,7 @@
    5.40      |> postproc (postprocess_term thy o resubst)
    5.41    end;
    5.42  
    5.43 -fun static_eval_conv thy consts conv =
    5.44 +fun static_conv thy consts conv =
    5.45    let
    5.46      val (algebra, eqngr) = obtain true thy consts [];
    5.47      val conv' = conv algebra eqngr;
    5.48 @@ -496,7 +496,7 @@
    5.49        then_conv (postprocess_conv thy)))
    5.50    end;
    5.51  
    5.52 -fun static_eval_value thy postproc consts evaluator =
    5.53 +fun static_value thy postproc consts evaluator =
    5.54    let
    5.55      val (algebra, eqngr) = obtain true thy consts [];
    5.56      val evaluator' = evaluator algebra eqngr;
     6.1 --- a/src/Tools/Code/code_runtime.ML	Tue Dec 14 00:16:30 2010 +0100
     6.2 +++ b/src/Tools/Code/code_runtime.ML	Wed Dec 15 09:47:12 2010 +0100
     6.3 @@ -120,7 +120,7 @@
     6.4        else ()
     6.5      fun evaluator naming program ((_, vs_ty), t) deps =
     6.6        base_evaluator cookie (obtain_serializer thy some_target) naming thy program (vs_ty, t) deps args;
     6.7 -  in Code_Thingol.dynamic_eval_value thy (Exn.map_result o postproc) evaluator t end;
     6.8 +  in Code_Thingol.dynamic_value thy (Exn.map_result o postproc) evaluator t end;
     6.9  
    6.10  fun dynamic_value_strict cookie thy some_target postproc t args =
    6.11    Exn.release (dynamic_value_exn cookie thy some_target postproc t args);
    6.12 @@ -133,7 +133,7 @@
    6.13      val serializer = obtain_serializer thy some_target;
    6.14      fun evaluator naming program thy ((_, vs_ty), t) deps =
    6.15        base_evaluator cookie serializer naming thy program (vs_ty, t) deps [];
    6.16 -  in Code_Thingol.static_eval_value thy (Exn.map_result o postproc) consts evaluator o reject_vars thy end;
    6.17 +  in Code_Thingol.static_value thy (Exn.map_result o postproc) consts evaluator o reject_vars thy end;
    6.18  
    6.19  fun static_value_strict cookie thy some_target postproc consts t =
    6.20    Exn.release (static_value_exn cookie thy some_target postproc consts t);
    6.21 @@ -175,7 +175,7 @@
    6.22  fun check_holds_oracle serializer naming thy program ((_, vs_ty), t) deps ct =
    6.23    raw_check_holds_oracle (serializer, naming, thy, program, (vs_ty, t), deps, ct);
    6.24  
    6.25 -val dynamic_holds_conv = Conv.tap_thy (fn thy => Code_Thingol.dynamic_eval_conv thy
    6.26 +val dynamic_holds_conv = Conv.tap_thy (fn thy => Code_Thingol.dynamic_conv thy
    6.27    (fn naming => check_holds_oracle (obtain_serializer thy NONE) naming thy)
    6.28    o reject_vars thy);
    6.29  
    6.30 @@ -183,7 +183,7 @@
    6.31    let
    6.32      val serializer = obtain_serializer thy NONE;
    6.33    in
    6.34 -    Code_Thingol.static_eval_conv thy consts
    6.35 +    Code_Thingol.static_conv thy consts
    6.36        (fn naming => fn program => fn thy => check_holds_oracle serializer naming thy program)
    6.37      o reject_vars thy
    6.38    end;
     7.1 --- a/src/Tools/Code/code_simp.ML	Tue Dec 14 00:16:30 2010 +0100
     7.2 +++ b/src/Tools/Code/code_simp.ML	Wed Dec 15 09:47:12 2010 +0100
     7.3 @@ -7,10 +7,10 @@
     7.4  signature CODE_SIMP =
     7.5  sig
     7.6    val map_ss: (simpset -> simpset) -> theory -> theory
     7.7 -  val dynamic_eval_conv: conv
     7.8 +  val dynamic_conv: conv
     7.9    val dynamic_eval_tac: theory -> int -> tactic
    7.10 -  val dynamic_eval_value: theory -> term -> term
    7.11 -  val static_eval_conv: theory -> simpset option -> string list -> conv
    7.12 +  val dynamic_value: theory -> term -> term
    7.13 +  val static_conv: theory -> simpset option -> string list -> conv
    7.14    val static_eval_tac: theory -> simpset option -> string list -> int -> tactic
    7.15    val setup: theory -> theory
    7.16  end;
    7.17 @@ -51,26 +51,26 @@
    7.18  
    7.19  (* evaluation with dynamic code context *)
    7.20  
    7.21 -val dynamic_eval_conv = Conv.tap_thy (fn thy => Code_Thingol.dynamic_eval_conv thy
    7.22 +val dynamic_conv = Conv.tap_thy (fn thy => Code_Thingol.dynamic_conv thy
    7.23    (fn naming => fn program => fn t => fn deps => rewrite_modulo thy NONE program));
    7.24  
    7.25 -fun dynamic_eval_tac thy = CONVERSION dynamic_eval_conv THEN' conclude_tac thy NONE;
    7.26 +fun dynamic_eval_tac thy = CONVERSION dynamic_conv THEN' conclude_tac thy NONE;
    7.27  
    7.28 -fun dynamic_eval_value thy = snd o Logic.dest_equals o Thm.prop_of o dynamic_eval_conv o Thm.cterm_of thy;
    7.29 +fun dynamic_value thy = snd o Logic.dest_equals o Thm.prop_of o dynamic_conv o Thm.cterm_of thy;
    7.30  
    7.31  val setup = Method.setup (Binding.name "code_simp")
    7.32    (Scan.succeed (SIMPLE_METHOD' o (CHANGED_PROP oo dynamic_eval_tac o ProofContext.theory_of)))
    7.33    "simplification with code equations"
    7.34 -  #> Value.add_evaluator ("simp", dynamic_eval_value o ProofContext.theory_of);
    7.35 +  #> Value.add_evaluator ("simp", dynamic_value o ProofContext.theory_of);
    7.36  
    7.37  
    7.38  (* evaluation with static code context *)
    7.39  
    7.40 -fun static_eval_conv thy some_ss consts =
    7.41 -  Code_Thingol.static_eval_conv_simple thy consts
    7.42 +fun static_conv thy some_ss consts =
    7.43 +  Code_Thingol.static_conv_simple thy consts
    7.44      (fn program => fn thy => fn _ => fn _ => rewrite_modulo thy some_ss program);
    7.45  
    7.46 -fun static_eval_tac thy some_ss consts = CONVERSION (static_eval_conv thy some_ss consts)
    7.47 +fun static_eval_tac thy some_ss consts = CONVERSION (static_conv thy some_ss consts)
    7.48    THEN' conclude_tac thy some_ss;
    7.49  
    7.50  end;
     8.1 --- a/src/Tools/Code/code_thingol.ML	Tue Dec 14 00:16:30 2010 +0100
     8.2 +++ b/src/Tools/Code/code_thingol.ML	Wed Dec 15 09:47:12 2010 +0100
     8.3 @@ -94,18 +94,18 @@
     8.4  
     8.5    val read_const_exprs: theory -> string list -> string list * string list
     8.6    val consts_program: theory -> bool -> string list -> string list * (naming * program)
     8.7 -  val dynamic_eval_conv: theory -> (naming -> program
     8.8 +  val dynamic_conv: theory -> (naming -> program
     8.9      -> ((string * sort) list * typscheme) * iterm -> string list -> conv)
    8.10      -> conv
    8.11 -  val dynamic_eval_value: theory -> ((term -> term) -> 'a -> 'a) -> (naming -> program
    8.12 +  val dynamic_value: theory -> ((term -> term) -> 'a -> 'a) -> (naming -> program
    8.13      -> ((string * sort) list * typscheme) * iterm -> string list -> 'a)
    8.14      -> term -> 'a
    8.15 -  val static_eval_conv: theory -> string list -> (naming -> program
    8.16 +  val static_conv: theory -> string list -> (naming -> program
    8.17      -> theory -> ((string * sort) list * typscheme) * iterm -> string list -> conv)
    8.18      -> conv
    8.19 -  val static_eval_conv_simple: theory -> string list
    8.20 +  val static_conv_simple: theory -> string list
    8.21      -> (program -> theory -> (string * sort) list -> term -> conv) -> conv
    8.22 -  val static_eval_value: theory -> ((term -> term) -> 'a -> 'a) -> string list ->
    8.23 +  val static_value: theory -> ((term -> term) -> 'a -> 'a) -> string list ->
    8.24      (naming -> program
    8.25        -> theory -> ((string * sort) list * typscheme) * iterm -> string list -> 'a)
    8.26      -> term -> 'a
    8.27 @@ -906,11 +906,11 @@
    8.28        invoke_generation false thy (algebra, eqngr) ensure_value t;
    8.29    in evaluator naming program ((original_sorts vs vs', (vs', ty')), t') deps end;
    8.30  
    8.31 -fun dynamic_eval_conv thy evaluator =
    8.32 -  Code_Preproc.dynamic_eval_conv thy (dynamic_evaluator thy evaluator);
    8.33 +fun dynamic_conv thy evaluator =
    8.34 +  Code_Preproc.dynamic_conv thy (dynamic_evaluator thy evaluator);
    8.35  
    8.36 -fun dynamic_eval_value thy postproc evaluator =
    8.37 -  Code_Preproc.dynamic_eval_value thy postproc (dynamic_evaluator thy evaluator);
    8.38 +fun dynamic_value thy postproc evaluator =
    8.39 +  Code_Preproc.dynamic_value thy postproc (dynamic_evaluator thy evaluator);
    8.40  
    8.41  fun provide_program thy consts f algebra eqngr =
    8.42    let
    8.43 @@ -926,16 +926,16 @@
    8.44        ensure_value thy algebra eqngr t (NONE, (naming, program));
    8.45    in evaluator naming program' thy ((original_sorts vs vs', (vs', ty')), t') deps end;
    8.46  
    8.47 -fun static_eval_conv thy consts conv =
    8.48 -  Code_Preproc.static_eval_conv thy consts
    8.49 +fun static_conv thy consts conv =
    8.50 +  Code_Preproc.static_conv thy consts
    8.51      (provide_program thy consts (static_evaluator conv));
    8.52  
    8.53 -fun static_eval_conv_simple thy consts conv =
    8.54 -  Code_Preproc.static_eval_conv thy consts
    8.55 +fun static_conv_simple thy consts conv =
    8.56 +  Code_Preproc.static_conv thy consts
    8.57      (provide_program thy consts ((K o K o K) conv));
    8.58  
    8.59 -fun static_eval_value thy postproc consts evaluator =
    8.60 -  Code_Preproc.static_eval_value thy postproc consts
    8.61 +fun static_value thy postproc consts evaluator =
    8.62 +  Code_Preproc.static_value thy postproc consts
    8.63      (provide_program thy consts (static_evaluator evaluator));
    8.64  
    8.65  
     9.1 --- a/src/Tools/nbe.ML	Tue Dec 14 00:16:30 2010 +0100
     9.2 +++ b/src/Tools/nbe.ML	Wed Dec 15 09:47:12 2010 +0100
     9.3 @@ -6,9 +6,10 @@
     9.4  
     9.5  signature NBE =
     9.6  sig
     9.7 -  val dynamic_eval_conv: conv
     9.8 -  val dynamic_eval_value: theory -> term -> term
     9.9 -  val static_eval_conv: theory -> string list -> conv
    9.10 +  val dynamic_conv: conv
    9.11 +  val dynamic_value: theory -> term -> term
    9.12 +  val static_conv: theory -> string list -> conv
    9.13 +  val static_value: theory -> string list -> term -> term
    9.14  
    9.15    datatype Univ =
    9.16        Const of int * Univ list               (*named (uninterpreted) constants*)
    9.17 @@ -592,23 +593,28 @@
    9.18  fun oracle thy program nbe_program_idx_tab vsp_ty_t deps ct =
    9.19    raw_oracle (thy, program, nbe_program_idx_tab, vsp_ty_t, deps, ct);
    9.20  
    9.21 -val dynamic_eval_conv = Conv.tap_thy (fn thy =>
    9.22 -  lift_triv_classes_conv thy (Code_Thingol.dynamic_eval_conv thy
    9.23 +val dynamic_conv = Conv.tap_thy (fn thy =>
    9.24 +  lift_triv_classes_conv thy (Code_Thingol.dynamic_conv thy
    9.25      (K (fn program => oracle thy program (compile false thy program)))));
    9.26  
    9.27 -fun dynamic_eval_value thy = lift_triv_classes_rew thy
    9.28 -  (Code_Thingol.dynamic_eval_value thy I
    9.29 +fun dynamic_value thy = lift_triv_classes_rew thy
    9.30 +  (Code_Thingol.dynamic_value thy I
    9.31      (K (fn program => eval_term thy program (compile false thy program))));
    9.32  
    9.33 -fun static_eval_conv thy consts =
    9.34 -  lift_triv_classes_conv thy (Code_Thingol.static_eval_conv thy consts
    9.35 +fun static_conv thy consts =
    9.36 +  lift_triv_classes_conv thy (Code_Thingol.static_conv thy consts
    9.37      (K (fn program => let val nbe_program = compile true thy program
    9.38        in fn thy => oracle thy program nbe_program end)));
    9.39  
    9.40 +fun static_value thy consts = lift_triv_classes_rew thy
    9.41 +  (Code_Thingol.static_value thy I consts
    9.42 +    (K (fn program => let val nbe_program = compile true thy program
    9.43 +      in fn thy => eval_term thy program (compile false thy program) end)));
    9.44 +
    9.45  
    9.46  (** setup **)
    9.47  
    9.48 -val setup = Value.add_evaluator ("nbe", dynamic_eval_value o ProofContext.theory_of);
    9.49 +val setup = Value.add_evaluator ("nbe", dynamic_value o ProofContext.theory_of);
    9.50  
    9.51  end;
    9.52   
    9.53 \ No newline at end of file