--- a/NEWS Fri May 09 22:14:06 2014 +0200
+++ b/NEWS Fri May 09 22:56:06 2014 +0200
@@ -204,6 +204,12 @@
*** HOL ***
+* Command and antiquotation ''value'' are hardcoded against nbe and
+ML now. Minor INCOMPATIBILITY.
+
+* Separate command ''approximate'' for approximative computation
+in Decision_Procs/Approximation. Minor INCOMPATIBILITY.
+
* Adjustion of INF and SUP operations:
* Elongated constants INFI and SUPR to INFIMUM and SUPREMUM.
* Consolidated theorem names containing INFI and SUPR: have INF
--- a/src/Doc/Codegen/Evaluation.thy Fri May 09 22:14:06 2014 +0200
+++ b/src/Doc/Codegen/Evaluation.thy Fri May 09 22:56:06 2014 +0200
@@ -90,18 +90,12 @@
value %quote "42 / (12 :: rat)"
text {*
- \noindent By default @{command value} tries all available evaluation
- techniques and prints the result of the first succeeding one. A particular
- technique may be specified in square brackets, e.g.
-*}
+ \noindent @{command value} tries first to evaluate using ML, falling
+ back to normalization by evaluation if this fails.
-value %quote [nbe] "42 / (12 :: rat)"
-
-text {*
To employ dynamic evaluation in the document generation, there is also
- a @{text value} antiquotation. By default, it also tries all available evaluation
- techniques and prints the result of the first succeeding one, unless a particular
- technique is specified in square brackets.
+ a @{text value} antiquotation with the same evaluation techniques
+ as @{command value}.
Static evaluation freezes the code generator configuration at a
certain point and uses this context whenever evaluation is issued
@@ -172,10 +166,7 @@
\fontsize{9pt}{12pt}\selectfont
\begin{tabular}{ll||c|c|c}
& & @{text simp} & @{text nbe} & @{text code} \tabularnewline \hline \hline
- \multirow{5}{1ex}{\rotatebox{90}{dynamic}}
- & interactive evaluation
- & @{command value} @{text "[simp]"} & @{command value} @{text "[nbe]"} & @{command value} @{text "[code]"}
- \tabularnewline
+ \multirow{4}{1ex}{\rotatebox{90}{dynamic}}
& 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}
--- a/src/Doc/Isar_Ref/HOL_Specific.thy Fri May 09 22:14:06 2014 +0200
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy Fri May 09 22:56:06 2014 +0200
@@ -2114,7 +2114,7 @@
\end{matharray}
@{rail \<open>
- @@{command (HOL) value} ( '[' @{syntax name} ']' )? modes? @{syntax term}
+ @@{command (HOL) value} modes? @{syntax term}
;
@@{command (HOL) values} modes? @{syntax nat}? @{syntax term}
@@ -2144,13 +2144,8 @@
\item @{command (HOL) "value"}~@{text t} evaluates and prints a
term; optionally @{text modes} can be specified, which are appended
to the current print mode; see \secref{sec:print-modes}.
- Internally, the evaluation is performed by registered evaluators,
- which are invoked sequentially until a result is returned.
- Alternatively a specific evaluator can be selected using square
- brackets; typical evaluators use the current set of code equations
- to normalize and include @{text simp} for fully symbolic evaluation
- using the simplifier, @{text nbe} for \emph{normalization by
- evaluation} and \emph{code} for code generation in SML.
+ Evaluation is tried first using ML, falling
+ back to normalization by evaluation if this fails.
\item @{command (HOL) "values"}~@{text t} enumerates a set
comprehension by evaluation and prints its values up to the given
@@ -2611,7 +2606,8 @@
"del"}'' removes) theorems which are applied as rewrite rules to any
result of an evaluation.
- \item @{attribute (HOL) code_abbrev} declares equations which are
+ \item @{attribute (HOL) code_abbrev} declares (or with option ``@{text
+ "del"}'' removes) equations which are
applied as rewrite rules to any result of an evaluation and
symmetrically during preprocessing to any code equation or evaluation
input.
--- a/src/HOL/Code_Evaluation.thy Fri May 09 22:14:06 2014 +0200
+++ b/src/HOL/Code_Evaluation.thy Fri May 09 22:56:06 2014 +0200
@@ -6,6 +6,7 @@
theory Code_Evaluation
imports Typerep Limited_Sequence
+keywords "value" :: diag
begin
subsection {* Term representation *}
@@ -72,11 +73,18 @@
shows "x \<equiv> y"
using assms by simp
+code_printing
+ type_constructor "term" \<rightharpoonup> (Eval) "Term.term"
+| constant Const \<rightharpoonup> (Eval) "Term.Const/ ((_), (_))"
+| constant App \<rightharpoonup> (Eval) "Term.$/ ((_), (_))"
+| constant Abs \<rightharpoonup> (Eval) "Term.Abs/ ((_), (_), (_))"
+| constant Free \<rightharpoonup> (Eval) "Term.Free/ ((_), (_))"
+
ML_file "Tools/code_evaluation.ML"
code_reserved Eval Code_Evaluation
-setup {* Code_Evaluation.setup *}
+ML_file "~~/src/HOL/Tools/value.ML"
subsection {* @{text term_of} instances *}
@@ -105,19 +113,9 @@
end
-
-subsubsection {* Code generator setup *}
-
-lemmas [code del] = term.rec term.case term.size
-lemma [code, code del]: "HOL.equal (t1\<Colon>term) t2 \<longleftrightarrow> HOL.equal t1 t2" ..
-
-lemma [code, code del]: "(term_of \<Colon> typerep \<Rightarrow> term) = term_of" ..
-lemma [code, code del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" ..
-lemma [code, code del]: "(term_of \<Colon> String.literal \<Rightarrow> term) = term_of" ..
-lemma [code, code del]: "(Code_Evaluation.term_of \<Colon> 'a::{type, term_of} Predicate.pred \<Rightarrow> Code_Evaluation.term)
- = Code_Evaluation.term_of" ..
-lemma [code, code del]: "(Code_Evaluation.term_of \<Colon> 'a::{type, term_of} Predicate.seq \<Rightarrow> Code_Evaluation.term)
- = Code_Evaluation.term_of" ..
+declare [[code drop: rec_term case_term size_term "size :: term \<Rightarrow> _" "HOL.equal :: term \<Rightarrow> _"
+ "term_of :: typerep \<Rightarrow> _" "term_of :: term \<Rightarrow> _" "term_of :: String.literal \<Rightarrow> _"
+ "term_of :: _ Predicate.pred \<Rightarrow> term" "term_of :: _ Predicate.seq \<Rightarrow> term"]]
lemma term_of_char [unfolded typerep_fun_def typerep_char_def typerep_nibble_def, code]:
"Code_Evaluation.term_of c = (case c of Char x y \<Rightarrow>
@@ -127,30 +125,15 @@
by (subst term_of_anything) rule
code_printing
- type_constructor "term" \<rightharpoonup> (Eval) "Term.term"
-| constant Const \<rightharpoonup> (Eval) "Term.Const/ ((_), (_))"
-| constant App \<rightharpoonup> (Eval) "Term.$/ ((_), (_))"
-| constant Abs \<rightharpoonup> (Eval) "Term.Abs/ ((_), (_), (_))"
-| constant Free \<rightharpoonup> (Eval) "Term.Free/ ((_), (_))"
-| constant "term_of \<Colon> integer \<Rightarrow> term" \<rightharpoonup> (Eval) "HOLogic.mk'_number/ HOLogic.code'_integerT"
+ constant "term_of \<Colon> integer \<Rightarrow> term" \<rightharpoonup> (Eval) "HOLogic.mk'_number/ HOLogic.code'_integerT"
| constant "term_of \<Colon> String.literal \<Rightarrow> term" \<rightharpoonup> (Eval) "HOLogic.mk'_literal"
code_reserved Eval HOLogic
-subsubsection {* Obfuscation *}
+subsection {* Generic reification *}
-print_translation {*
- let
- val term = Const ("<TERM>", dummyT);
- fun tr1' _ [_, _] = term;
- fun tr2' _ [] = term;
- in
- [(@{const_syntax Const}, tr1'),
- (@{const_syntax App}, tr1'),
- (@{const_syntax dummy_term}, tr2')]
- end
-*}
+ML_file "~~/src/HOL/Tools/reification.ML"
subsection {* Diagnostic *}
@@ -162,11 +145,6 @@
constant "tracing :: String.literal => 'a => 'a" \<rightharpoonup> (Eval) "Code'_Evaluation.tracing"
-subsection {* Generic reification *}
-
-ML_file "~~/src/HOL/Tools/reification.ML"
-
-
hide_const dummy_term valapp
hide_const (open) Const App Abs Free termify valtermify term_of tracing
--- a/src/HOL/Decision_Procs/Approximation.thy Fri May 09 22:14:06 2014 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Fri May 09 22:56:06 2014 +0200
@@ -9,6 +9,7 @@
"~~/src/HOL/Library/Float"
Dense_Linear_Order
"~~/src/HOL/Library/Code_Target_Numeral"
+keywords "approximate" :: diag
begin
declare powr_one [simp]
@@ -3449,6 +3450,4 @@
ML_file "approximation.ML"
-setup {* Value.add_evaluator ("approximate", Approximation.approx 30) *}
-
end
--- a/src/HOL/Decision_Procs/approximation.ML Fri May 09 22:14:06 2014 +0200
+++ b/src/HOL/Decision_Procs/approximation.ML Fri May 09 22:56:06 2014 +0200
@@ -91,11 +91,6 @@
val t = Term.subst_TVars m t
in t end
-fun converted_result t =
- prop_of t
- |> HOLogic.dest_Trueprop
- |> HOLogic.dest_eq |> snd
-
fun apply_tactic ctxt term tactic =
cterm_of (Proof_Context.theory_of ctxt) term
|> Goal.init
@@ -140,4 +135,24 @@
else if type_of t = @{typ bool} then approx_form prec ctxt (@{const Trueprop} $ t)
else approx_arith prec ctxt t
+fun approximate_cmd modes raw_t state =
+ let
+ val ctxt = Toplevel.context_of state;
+ val t = Syntax.read_term ctxt raw_t;
+ val t' = approx 30 ctxt t;
+ val ty' = Term.type_of t';
+ val ctxt' = Variable.auto_fixes t' ctxt;
+ val p = Print_Mode.with_modes modes (fn () =>
+ Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
+ Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
+ in Pretty.writeln p end;
+
+val opt_modes =
+ Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
+
+val _ =
+ Outer_Syntax.improper_command @{command_spec "approximate"} "print approximation of term"
+ (opt_modes -- Parse.term
+ >> (fn (modes, t) => Toplevel.keep (approximate_cmd modes t)));
+
end;
--- a/src/HOL/Decision_Procs/ex/Approximation_Ex.thy Fri May 09 22:14:06 2014 +0200
+++ b/src/HOL/Decision_Procs/ex/Approximation_Ex.thy Fri May 09 22:56:06 2014 +0200
@@ -75,6 +75,6 @@
lemma "x \<in> { 0 .. 1 :: real } \<longrightarrow> x\<^sup>2 \<le> x"
by (approximation 30 splitting: x=1 taylor: x = 3)
-value [approximate] "10"
+approximate "10"
end
--- a/src/HOL/IMP/Abs_Int1_parity.thy Fri May 09 22:14:06 2014 +0200
+++ b/src/HOL/IMP/Abs_Int1_parity.thy Fri May 09 22:56:06 2014 +0200
@@ -134,7 +134,7 @@
definition "test1_parity =
''x'' ::= N 1;;
WHILE Less (V ''x'') (N 100) DO ''x'' ::= Plus (V ''x'') (N 2)"
-value [code] "show_acom (the(AI_parity test1_parity))"
+value "show_acom (the(AI_parity test1_parity))"
definition "test2_parity =
''x'' ::= N 1;;
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy Fri May 09 22:14:06 2014 +0200
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy Fri May 09 22:56:06 2014 +0200
@@ -100,12 +100,12 @@
WHILE Less (V ''x'') (N 1)
DO (''x'' ::= V ''y'';; ''y'' ::= V ''z'';; ''z'' ::= V ''u'')"
-value [code] "list (AI_const test1_const Top)"
-value [code] "list (AI_const test2_const Top)"
-value [code] "list (AI_const test3_const Top)"
-value [code] "list (AI_const test4_const Top)"
-value [code] "list (AI_const test5_const Top)"
-value [code] "list (AI_const test6_const Top)"
-value [code] "list (AI_const test7_const Top)"
+value "list (AI_const test1_const Top)"
+value "list (AI_const test2_const Top)"
+value "list (AI_const test3_const Top)"
+value "list (AI_const test4_const Top)"
+value "list (AI_const test5_const Top)"
+value "list (AI_const test6_const Top)"
+value "list (AI_const test7_const Top)"
end
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy Fri May 09 22:14:06 2014 +0200
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy Fri May 09 22:56:06 2014 +0200
@@ -213,22 +213,22 @@
"list_up bot = bot" |
"list_up (Up x) = Up(list x)"
-value [code] "list_up(afilter_ivl (N 5) (I (Some 4) (Some 5)) Top)"
-value [code] "list_up(afilter_ivl (N 5) (I (Some 4) (Some 4)) Top)"
-value [code] "list_up(afilter_ivl (V ''x'') (I (Some 4) (Some 4))
+value "list_up(afilter_ivl (N 5) (I (Some 4) (Some 5)) Top)"
+value "list_up(afilter_ivl (N 5) (I (Some 4) (Some 4)) Top)"
+value "list_up(afilter_ivl (V ''x'') (I (Some 4) (Some 4))
(Up(FunDom(Top(''x'':=I (Some 5) (Some 6))) [''x''])))"
-value [code] "list_up(afilter_ivl (V ''x'') (I (Some 4) (Some 5))
+value "list_up(afilter_ivl (V ''x'') (I (Some 4) (Some 5))
(Up(FunDom(Top(''x'':=I (Some 5) (Some 6))) [''x''])))"
-value [code] "list_up(afilter_ivl (Plus (V ''x'') (V ''x'')) (I (Some 0) (Some 10))
+value "list_up(afilter_ivl (Plus (V ''x'') (V ''x'')) (I (Some 0) (Some 10))
(Up(FunDom(Top(''x'':= I (Some 0) (Some 100)))[''x''])))"
-value [code] "list_up(afilter_ivl (Plus (V ''x'') (N 7)) (I (Some 0) (Some 10))
+value "list_up(afilter_ivl (Plus (V ''x'') (N 7)) (I (Some 0) (Some 10))
(Up(FunDom(Top(''x'':= I (Some 0) (Some 100)))[''x''])))"
-value [code] "list_up(bfilter_ivl (Less (V ''x'') (V ''x'')) True
+value "list_up(bfilter_ivl (Less (V ''x'') (V ''x'')) True
(Up(FunDom(Top(''x'':= I (Some 0) (Some 0)))[''x''])))"
-value [code] "list_up(bfilter_ivl (Less (V ''x'') (V ''x'')) True
+value "list_up(bfilter_ivl (Less (V ''x'') (V ''x'')) True
(Up(FunDom(Top(''x'':= I (Some 0) (Some 2)))[''x''])))"
-value [code] "list_up(bfilter_ivl (Less (V ''x'') (Plus (N 10) (V ''y''))) True
+value "list_up(bfilter_ivl (Less (V ''x'') (Plus (N 10) (V ''y''))) True
(Up(FunDom(Top(''x'':= I (Some 15) (Some 20),''y'':= I (Some 5) (Some 7)))[''x'', ''y''])))"
definition "test_ivl1 =
@@ -236,7 +236,7 @@
IF Less (V ''x'') (V ''y'')
THEN ''y'' ::= Plus (V ''y'') (V ''x'')
ELSE ''x'' ::= Plus (V ''x'') (V ''y'')"
-value [code] "list_up(AI_ivl test_ivl1 Top)"
+value "list_up(AI_ivl test_ivl1 Top)"
value "list_up (AI_ivl test3_const Top)"
@@ -247,24 +247,24 @@
definition "test2_ivl =
''y'' ::= N 7;;
WHILE Less (V ''x'') (N 100) DO ''y'' ::= Plus (V ''y'') (N 1)"
-value [code] "list_up(AI_ivl test2_ivl Top)"
+value "list_up(AI_ivl test2_ivl Top)"
definition "test3_ivl =
''x'' ::= N 0;; ''y'' ::= N 100;; ''z'' ::= Plus (V ''x'') (V ''y'');;
WHILE Less (V ''x'') (N 11)
DO (''x'' ::= Plus (V ''x'') (N 1);; ''y'' ::= Plus (V ''y'') (N -1))"
-value [code] "list_up(AI_ivl test3_ivl Top)"
+value "list_up(AI_ivl test3_ivl Top)"
definition "test4_ivl =
''x'' ::= N 0;; ''y'' ::= N 0;;
WHILE Less (V ''x'') (N 1001)
DO (''y'' ::= V ''x'';; ''x'' ::= Plus (V ''x'') (N 1))"
-value [code] "list_up(AI_ivl test4_ivl Top)"
+value "list_up(AI_ivl test4_ivl Top)"
text{* Nontermination not detected: *}
definition "test5_ivl =
''x'' ::= N 0;;
WHILE Less (V ''x'') (N 1) DO ''x'' ::= Plus (V ''x'') (N -1)"
-value [code] "list_up(AI_ivl test5_ivl Top)"
+value "list_up(AI_ivl test5_ivl Top)"
end
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den2.thy Fri May 09 22:14:06 2014 +0200
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den2.thy Fri May 09 22:56:06 2014 +0200
@@ -200,8 +200,8 @@
and aval_ivl' = aval'
proof qed (auto simp: iter'_pfp_above)
-value [code] "list_up(AI_ivl' test3_ivl Top)"
-value [code] "list_up(AI_ivl' test4_ivl Top)"
-value [code] "list_up(AI_ivl' test5_ivl Top)"
+value "list_up(AI_ivl' test3_ivl Top)"
+value "list_up(AI_ivl' test4_ivl Top)"
+value "list_up(AI_ivl' test5_ivl Top)"
end
--- a/src/HOL/Library/Extended_Real.thy Fri May 09 22:14:06 2014 +0200
+++ b/src/HOL/Library/Extended_Real.thy Fri May 09 22:56:06 2014 +0200
@@ -2444,10 +2444,10 @@
(* A small list of simple arithmetic expressions *)
-value [code] "- \<infinity> :: ereal"
-value [code] "\<bar>-\<infinity>\<bar> :: ereal"
-value [code] "4 + 5 / 4 - ereal 2 :: ereal"
-value [code] "ereal 3 < \<infinity>"
-value [code] "real (\<infinity>::ereal) = 0"
+value "- \<infinity> :: ereal"
+value "\<bar>-\<infinity>\<bar> :: ereal"
+value "4 + 5 / 4 - ereal 2 :: ereal"
+value "ereal 3 < \<infinity>"
+value "real (\<infinity>::ereal) = 0"
end
--- a/src/HOL/Library/Transitive_Closure_Table.thy Fri May 09 22:14:06 2014 +0200
+++ b/src/HOL/Library/Transitive_Closure_Table.thy Fri May 09 22:56:06 2014 +0200
@@ -190,29 +190,4 @@
code_pred rtranclp using rtranclp_eq_rtrancl_tab_nil [THEN iffD1] by fastforce
-subsection {* A simple example *}
-
-datatype ty = A | B | C
-
-inductive test :: "ty \<Rightarrow> ty \<Rightarrow> bool"
-where
- "test A B"
-| "test B A"
-| "test B C"
-
-subsubsection {* Invoking with the predicate compiler and the generic code generator *}
-
-code_pred test .
-
-values "{x. test\<^sup>*\<^sup>* A C}"
-values "{x. test\<^sup>*\<^sup>* C A}"
-values "{x. test\<^sup>*\<^sup>* A x}"
-values "{x. test\<^sup>*\<^sup>* x C}"
-
-value "test\<^sup>*\<^sup>* A C"
-value "test\<^sup>*\<^sup>* C A"
-
-hide_type ty
-hide_const test A B C
-
end
\ No newline at end of file
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy Fri May 09 22:14:06 2014 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy Fri May 09 22:56:06 2014 +0200
@@ -452,8 +452,8 @@
values [random_dseq 1, 3, 3] 10 "{(xs, ys, zs::int list). append xs ys zs}"
values [random_dseq 1, 1, 4] 10 "{(xs, ys, zs::int list). append xs ys zs}"
-value [code] "Predicate.the (concat [0::int, 1, 2] [3, 4, 5])"
-value [code] "Predicate.the (slice ([]::int list))"
+value "Predicate.the (concat [0::int, 1, 2] [3, 4, 5])"
+value "Predicate.the (slice ([]::int list))"
text {* tricky case with alternative rules *}
@@ -830,7 +830,7 @@
code_pred divmod_rel .
thm divmod_rel.equation
-value [code] "Predicate.the (divmod_rel_i_i_o_o 1705 42)"
+value "Predicate.the (divmod_rel_i_i_o_o 1705 42)"
subsection {* Transforming predicate logic into logic programs *}
--- a/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy Fri May 09 22:14:06 2014 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy Fri May 09 22:56:06 2014 +0200
@@ -183,7 +183,7 @@
quickcheck[tester = smart_exhaustive]
oops
-value [code] "prop_regex a_sol"
+value "prop_regex a_sol"
end
--- a/src/HOL/ROOT Fri May 09 22:14:06 2014 +0200
+++ b/src/HOL/ROOT Fri May 09 22:56:06 2014 +0200
@@ -518,6 +518,7 @@
Serbian
"~~/src/HOL/Library/FinFun_Syntax"
"~~/src/HOL/Library/Refute"
+ "~~/src/HOL/Library/Transitive_Closure_Table"
Cartouche_Examples
theories
Iff_Oracle
@@ -560,6 +561,7 @@
Sqrt_Script
Transfer_Ex
Transfer_Int_Nat
+ Transitive_Closure_Table_Ex
HarmonicSeries
Refute_Examples
Execute_Choice
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Fri May 09 22:14:06 2014 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Fri May 09 22:56:06 2014 +0200
@@ -305,9 +305,9 @@
fun dynamic_value_strict opts cookie ctxt postproc t =
let
- fun evaluator program ((_, vs_ty), t) deps =
+ fun evaluator program _ vs_ty_t deps =
Exn.interruptible_capture (value opts ctxt cookie)
- (Code_Target.evaluator ctxt target program deps true (vs_ty, t));
+ (Code_Target.evaluator ctxt target program deps true vs_ty_t);
in Exn.release (Code_Thingol.dynamic_value ctxt (Exn.map_result o postproc) evaluator t) end;
(** counterexample generator **)
--- a/src/HOL/Tools/code_evaluation.ML Fri May 09 22:14:06 2014 +0200
+++ b/src/HOL/Tools/code_evaluation.ML Fri May 09 22:56:06 2014 +0200
@@ -16,7 +16,6 @@
val static_conv: Proof.context -> string list -> typ list -> Proof.context -> conv
val put_term: (unit -> term) -> Proof.context -> Proof.context
val tracing: string -> 'a -> 'a
- val setup: theory -> theory
end;
structure Code_Evaluation : CODE_EVALUATION =
@@ -129,6 +128,15 @@
in if has_inst then add_abs_term_of_code tyco raw_vs abs ty proj thy else thy end;
+(* setup *)
+
+val _ = Context.>> (Context.map_theory
+ (Code.datatype_interpretation ensure_term_of
+ #> Code.abstype_interpretation ensure_term_of
+ #> Code.datatype_interpretation ensure_term_of_code
+ #> Code.abstype_interpretation ensure_abs_term_of_code));
+
+
(** termifying syntax **)
fun map_default f xs =
@@ -155,6 +163,8 @@
fun check_termify ctxt ts =
the_default ts (map_default subst_termify ts);
+val _ = Context.>> (Syntax_Phases.term_check 0 "termify" check_termify);
+
(** evaluation **)
@@ -220,15 +230,4 @@
fun tracing s x = (Output.tracing s; x);
-
-(** setup **)
-
-val setup =
- Code.datatype_interpretation ensure_term_of
- #> Code.abstype_interpretation ensure_term_of
- #> Code.datatype_interpretation ensure_term_of_code
- #> Code.abstype_interpretation ensure_abs_term_of_code
- #> Context.theory_map (Syntax_Phases.term_check 0 "termify" check_termify)
- #> Value.add_evaluator ("code", dynamic_value_strict);
-
end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/value.ML Fri May 09 22:56:06 2014 +0200
@@ -0,0 +1,53 @@
+(* Title: HOL/Tools/value.ML
+ Author: Florian Haftmann, TU Muenchen
+
+Evaluation using nbe or SML.
+*)
+
+signature VALUE =
+sig
+ val value: Proof.context -> term -> term
+ val value_cmd: string list -> string -> Toplevel.state -> unit
+end;
+
+structure Value : VALUE =
+struct
+
+fun value ctxt t =
+ if null (Term.add_frees t [])
+ then case try (Code_Evaluation.dynamic_value_strict ctxt) t of
+ SOME t' => t'
+ | NONE => Nbe.dynamic_value ctxt t
+ else Nbe.dynamic_value ctxt t;
+
+fun value_cmd modes raw_t state =
+ let
+ val ctxt = Toplevel.context_of state;
+ val t = Syntax.read_term ctxt raw_t;
+ val t' = value ctxt t;
+ val ty' = Term.type_of t';
+ val ctxt' = Variable.auto_fixes t' ctxt;
+ val p = Print_Mode.with_modes modes (fn () =>
+ Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
+ Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
+ in Pretty.writeln p end;
+
+val opt_modes =
+ Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
+
+val opt_evaluator =
+ Scan.option (@{keyword "["} |-- Parse.xname --| @{keyword "]"})
+
+val _ =
+ Outer_Syntax.improper_command @{command_spec "value"} "evaluate and print term"
+ (opt_modes -- Parse.term
+ >> (fn (modes, t) => Toplevel.keep (value_cmd modes t)));
+
+val _ = Context.>> (Context.map_theory
+ (Thy_Output.antiquotation @{binding value}
+ (Term_Style.parse -- Args.term)
+ (fn {source, context, ...} => fn (style, t) => Thy_Output.output context
+ (Thy_Output.maybe_pretty_source Thy_Output.pretty_term context source
+ [style (value context t)]))));
+
+end;
--- a/src/HOL/ex/Eval_Examples.thy Fri May 09 22:14:06 2014 +0200
+++ b/src/HOL/ex/Eval_Examples.thy Fri May 09 22:56:06 2014 +0200
@@ -25,36 +25,20 @@
text {* term evaluation *}
value "(Suc 2 + 1) * 4"
-value [code] "(Suc 2 + 1) * 4"
-value [nbe] "(Suc 2 + 1) * 4"
value "(Suc 2 + Suc 0) * Suc 3"
-value [code] "(Suc 2 + Suc 0) * Suc 3"
-value [nbe] "(Suc 2 + Suc 0) * Suc 3"
value "nat 100"
-value [code] "nat 100"
-value [nbe] "nat 100"
value "(10::int) \<le> 12"
-value [code] "(10::int) \<le> 12"
-value [nbe] "(10::int) \<le> 12"
value "max (2::int) 4"
-value [code] "max (2::int) 4"
-value [nbe] "max (2::int) 4"
value "of_int 2 / of_int 4 * (1::rat)"
-value [code] "of_int 2 / of_int 4 * (1::rat)"
-value [nbe] "of_int 2 / of_int 4 * (1::rat)"
value "[] :: nat list"
-value [code] "[] :: nat list"
-value [nbe] "[] :: nat list"
value "[(nat 100, ())]"
-value [code] "[(nat 100, ())]"
-value [nbe] "[(nat 100, ())]"
text {* a fancy datatype *}
@@ -67,7 +51,5 @@
| Blubb "('a, 'b) foo"
value "Bla (Bar (4::nat) [Suc 0])"
-value [code] "Bla (Bar (4::nat) [Suc 0])"
-value [nbe] "Bla (Bar (4::nat) [Suc 0])"
end
--- a/src/HOL/ex/Normalization_by_Evaluation.thy Fri May 09 22:14:06 2014 +0200
+++ b/src/HOL/ex/Normalization_by_Evaluation.thy Fri May 09 22:56:06 2014 +0200
@@ -68,20 +68,20 @@
lemma "map (%f. f True) ([id, g, Not] @ fs) = [True, g True, False] @ map (%f. f True) fs"
by normalization rule
lemma "rev [a, b, c] = [c, b, a]" by normalization
-value [nbe] "rev (a#b#cs) = rev cs @ [b, a]"
-value [nbe] "map (%F. F [a,b,c::'x]) (map map [f,g,h])"
-value [nbe] "map (%F. F ([a,b,c] @ ds)) (map map ([f,g,h]@fs))"
-value [nbe] "map (%F. F [Z,S Z,S(S Z)]) (map map [S,add (S Z),mul (S(S Z)),id])"
+value "rev (a#b#cs) = rev cs @ [b, a]"
+value "map (%F. F [a,b,c::'x]) (map map [f,g,h])"
+value "map (%F. F ([a,b,c] @ ds)) (map map ([f,g,h]@fs))"
+value "map (%F. F [Z,S Z,S(S Z)]) (map map [S,add (S Z),mul (S(S Z)),id])"
lemma "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) [None, Some ()] = [False, True]"
by normalization
-value [nbe] "case xs of [] \<Rightarrow> True | x#xs \<Rightarrow> False"
-value [nbe] "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) xs = P"
+value "case xs of [] \<Rightarrow> True | x#xs \<Rightarrow> False"
+value "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) xs = P"
lemma "let x = y in [x, x] = [y, y]" by normalization
lemma "Let y (%x. [x,x]) = [y, y]" by normalization
-value [nbe] "case n of Z \<Rightarrow> True | S x \<Rightarrow> False"
+value "case n of Z \<Rightarrow> True | S x \<Rightarrow> False"
lemma "(%(x,y). add x y) (S z,S z) = S (add z (S z))" by normalization
-value [nbe] "filter (%x. x) ([True,False,x]@xs)"
-value [nbe] "filter Not ([True,False,x]@xs)"
+value "filter (%x. x) ([True,False,x]@xs)"
+value "filter Not ([True,False,x]@xs)"
lemma "[x,y,z] @ [a,b,c] = [x, y, z, a, b, c]" by normalization
lemma "(%(xs, ys). xs @ ys) ([a, b, c], [d, e, f]) = [a, b, c, d, e, f]" by normalization
@@ -106,7 +106,7 @@
lemma "[Suc 0, 0] = [Suc 0, 0]" by normalization
lemma "max (Suc 0) 0 = Suc 0" by normalization
lemma "(42::rat) / 1704 = 1 / 284 + 3 / 142" by normalization
-value [nbe] "Suc 0 \<in> set ms"
+value "Suc 0 \<in> set ms"
(* non-left-linear patterns, equality by extensionality *)
@@ -115,13 +115,13 @@
lemma "(f o g) x = f (g x)" by normalization
lemma "(f o id) x = f x" by normalization
lemma "(id :: bool \<Rightarrow> bool) = id" by normalization
-value [nbe] "(\<lambda>x. x)"
+value "(\<lambda>x. x)"
(* Church numerals: *)
-value [nbe] "(%m n f x. m f (n f x)) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
-value [nbe] "(%m n f x. m (n f) x) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
-value [nbe] "(%m n. n m) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
+value "(%m n f x. m f (n f x)) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
+value "(%m n f x. m (n f) x) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
+value "(%m n. n m) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
(* handling of type classes in connection with equality *)
--- a/src/HOL/ex/Parallel_Example.thy Fri May 09 22:14:06 2014 +0200
+++ b/src/HOL/ex/Parallel_Example.thy Fri May 09 22:56:06 2014 +0200
@@ -93,7 +93,7 @@
(\<lambda>() \<Rightarrow> let c = Parallel.fork computation_harmonic
in (computation_primes (), Parallel.join c))"
-value [code] "computation_future ()"
+value "computation_future ()"
definition computation_factorise :: "nat \<Rightarrow> nat list" where
"computation_factorise = Debug.timing (STR ''factorise'') factorise"
@@ -102,7 +102,7 @@
"computation_parallel _ = Debug.timing (STR ''overall computation'')
(Parallel.map computation_factorise) [20000..<20100]"
-value [code] "computation_parallel ()"
+value "computation_parallel ()"
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Transitive_Closure_Table_Ex.thy Fri May 09 22:56:06 2014 +0200
@@ -0,0 +1,30 @@
+(* Author: Stefan Berghofer, Lukas Bulwahn, TU Muenchen *)
+
+header {* Simple example for table-based implementation of the reflexive transitive closure *}
+
+theory Transitive_Closure_Table_Ex
+imports "~~/src/HOL/Library/Transitive_Closure_Table"
+begin
+
+datatype ty = A | B | C
+
+inductive test :: "ty \<Rightarrow> ty \<Rightarrow> bool"
+where
+ "test A B"
+| "test B A"
+| "test B C"
+
+
+text {* Invoking with the predicate compiler and the generic code generator *}
+
+code_pred test .
+
+values "{x. test\<^sup>*\<^sup>* A C}"
+values "{x. test\<^sup>*\<^sup>* C A}"
+values "{x. test\<^sup>*\<^sup>* A x}"
+values "{x. test\<^sup>*\<^sup>* x C}"
+
+value "test\<^sup>*\<^sup>* A C"
+value "test\<^sup>*\<^sup>* C A"
+
+end
--- a/src/Pure/Isar/class_declaration.ML Fri May 09 22:14:06 2014 +0200
+++ b/src/Pure/Isar/class_declaration.ML Fri May 09 22:56:06 2014 +0200
@@ -309,11 +309,12 @@
fun gen_class prep_class_spec before_exit b raw_supclasses raw_elems thy =
let
val class = Sign.full_name thy b;
+ val prefix = Binding.qualify true "class";
val (((sups, supparam_names), (supsort, base_sort, supexpr)), (elems, global_syntax)) =
prep_class_spec thy raw_supclasses raw_elems;
in
thy
- |> Expression.add_locale I b (Binding.qualify true "class" b) supexpr elems
+ |> Expression.add_locale I b (prefix b) supexpr elems
|> snd |> Local_Theory.exit_global
|> adjungate_axclass b class base_sort sups supsort supparam_names global_syntax
|-> (fn (param_map, params, assm_axiom) =>
@@ -321,7 +322,9 @@
#-> (fn (base_morph, eq_morph, export_morph, some_axiom, some_assm_intro, of_class) =>
Context.theory_map (Locale.add_registration (class, base_morph)
(Option.map (rpair true) eq_morph) export_morph)
- #> Class.register class sups params base_sort base_morph export_morph some_axiom some_assm_intro of_class))
+ #> Class.register class sups params base_sort base_morph export_morph some_axiom some_assm_intro of_class
+ #> Global_Theory.store_thm (prefix (Binding.qualified_name (class ^ ".of_class.intro")), of_class)))
+ |> snd
|> Named_Target.init before_exit class
|> pair class
end;
--- a/src/Tools/Code/code_preproc.ML Fri May 09 22:14:06 2014 +0200
+++ b/src/Tools/Code/code_preproc.ML Fri May 09 22:56:06 2014 +0200
@@ -9,7 +9,6 @@
sig
val map_pre: (Proof.context -> Proof.context) -> theory -> theory
val map_post: (Proof.context -> Proof.context) -> theory -> theory
- val add_unfold: thm -> theory -> theory
val add_functrans: string * (Proof.context -> (thm * bool) list -> (thm * bool) list option) -> theory -> theory
val del_functrans: string -> theory -> theory
val simple_functrans: (Proof.context -> thm list -> thm list option)
@@ -24,14 +23,14 @@
val pretty: Proof.context -> code_graph -> Pretty.T
val obtain: bool -> theory -> string list -> term list -> code_algebra * code_graph
val dynamic_conv: Proof.context
- -> (code_algebra -> code_graph -> (string * sort) list -> term -> conv) -> conv
+ -> (code_algebra -> code_graph -> term -> conv) -> conv
val dynamic_value: Proof.context -> ((term -> term) -> 'a -> 'a)
- -> (code_algebra -> code_graph -> (string * sort) list -> term -> 'a) -> term -> 'a
+ -> (code_algebra -> code_graph -> term -> 'a) -> term -> 'a
val static_conv: Proof.context -> string list
- -> (code_algebra -> code_graph -> Proof.context -> (string * sort) list -> term -> conv)
+ -> (code_algebra -> code_graph -> Proof.context -> term -> conv)
-> Proof.context -> conv
val static_value: Proof.context -> ((term -> term) -> 'a -> 'a) -> string list
- -> (code_algebra -> code_graph -> Proof.context -> (string * sort) list -> term -> 'a)
+ -> (code_algebra -> code_graph -> Proof.context -> term -> 'a)
-> Proof.context -> term -> 'a
val setup: theory -> theory
@@ -87,20 +86,18 @@
val map_pre = map_simpset apfst;
val map_post = map_simpset apsnd;
-val add_unfold = map_pre o Simplifier.add_simp;
-val del_unfold = map_pre o Simplifier.del_simp;
-val add_post = map_post o Simplifier.add_simp;
-val del_post = map_post o Simplifier.del_simp;
+fun process_unfold add_del = map_pre o add_del;
+fun process_post add_del = map_post o add_del;
-fun add_code_abbrev raw_thm thy =
+fun process_abbrev add_del raw_thm thy =
let
val ctxt = Proof_Context.init_global thy;
val thm = Local_Defs.meta_rewrite_rule ctxt raw_thm;
val thm_sym = Thm.symmetric thm;
in
thy |> map_pre_post (fn (pre, post) =>
- (pre |> simpset_map ctxt (Simplifier.add_simp thm_sym),
- post |> simpset_map ctxt (Simplifier.add_simp thm)))
+ (pre |> simpset_map ctxt (add_del thm_sym),
+ post |> simpset_map ctxt (add_del thm)))
end;
fun add_functrans (name, f) = (map_data o apsnd)
@@ -462,17 +459,15 @@
(Wellsorted.change_yield (if ignore_cache then NONE else SOME thy)
(extend_arities_eqngr (Proof_Context.init_global thy) consts ts));
-fun dest_cterm ct = let val t = Thm.term_of ct in (Term.add_tfrees t [], t) end;
-
fun dynamic_conv ctxt conv = no_variables_conv ctxt (fn ct =>
let
val thm1 = preprocess_conv ctxt ctxt ct;
val ct' = Thm.rhs_of thm1;
- val (vs', t') = dest_cterm ct';
+ val t' = Thm.term_of ct';
val consts = fold_aterms
(fn Const (c, _) => insert (op =) c | _ => I) t' [];
val (algebra', eqngr') = obtain false (Proof_Context.theory_of ctxt) consts [t'];
- val thm2 = conv algebra' eqngr' vs' t' ct';
+ val thm2 = conv algebra' eqngr' t' ct';
val thm3 = postprocess_conv ctxt ctxt (Thm.rhs_of thm2);
in
Thm.transitive thm1 (Thm.transitive thm2 thm3) handle THM _ =>
@@ -483,13 +478,12 @@
fun dynamic_value ctxt postproc evaluator t =
let
val (resubst, t') = preprocess_term ctxt ctxt t;
- val vs' = Term.add_tfrees t' [];
val consts = fold_aterms
(fn Const (c, _) => insert (op =) c | _ => I) t' [];
val (algebra', eqngr') = obtain false (Proof_Context.theory_of ctxt) consts [t'];
in
t'
- |> evaluator algebra' eqngr' vs'
+ |> evaluator algebra' eqngr'
|> postproc (postprocess_term ctxt ctxt o resubst)
end;
@@ -500,7 +494,7 @@
val conv' = conv algebra eqngr;
val post_conv = postprocess_conv ctxt;
in fn ctxt' => no_variables_conv ctxt' ((pre_conv ctxt')
- then_conv (fn ct => uncurry (conv' ctxt') (dest_cterm ct) ct)
+ then_conv (fn ct => conv' ctxt' (Thm.term_of ct) ct)
then_conv (post_conv ctxt'))
end;
@@ -513,7 +507,7 @@
in fn ctxt' =>
preproc ctxt'
#-> (fn resubst => fn t => t
- |> evaluator' ctxt' (Term.add_tfrees t [])
+ |> evaluator' ctxt'
|> postproc (postproc' ctxt' o resubst))
end;
@@ -523,14 +517,15 @@
val setup =
let
fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
- fun add_del_attribute_parser add del =
- Attrib.add_del (mk_attribute add) (mk_attribute del);
+ fun add_del_attribute_parser process =
+ Attrib.add_del (mk_attribute (process Simplifier.add_simp))
+ (mk_attribute (process Simplifier.del_simp));
in
- Attrib.setup @{binding code_unfold} (add_del_attribute_parser add_unfold del_unfold)
+ Attrib.setup @{binding code_unfold} (add_del_attribute_parser process_unfold)
"preprocessing equations for code generator"
- #> Attrib.setup @{binding code_post} (add_del_attribute_parser add_post del_post)
+ #> Attrib.setup @{binding code_post} (add_del_attribute_parser process_post)
"postprocessing equations for code generator"
- #> Attrib.setup @{binding code_abbrev} (Scan.succeed (mk_attribute add_code_abbrev))
+ #> Attrib.setup @{binding code_abbrev} (add_del_attribute_parser process_abbrev)
"post- and preprocessing equations for code generator"
end;
--- a/src/Tools/Code/code_runtime.ML Fri May 09 22:14:06 2014 +0200
+++ b/src/Tools/Code/code_runtime.ML Fri May 09 22:56:06 2014 +0200
@@ -112,8 +112,8 @@
val _ = if ! trace
then tracing ("Evaluation of term " ^ quote (Syntax.string_of_term ctxt t))
else ()
- fun evaluator program ((_, vs_ty), t) deps =
- evaluation cookie ctxt (obtain_evaluator ctxt some_target program deps) (vs_ty, t) args;
+ fun evaluator program _ vs_ty_t deps =
+ evaluation cookie ctxt (obtain_evaluator ctxt some_target program deps) vs_ty_t args;
in Code_Thingol.dynamic_value ctxt (Exn.map_result o postproc) evaluator t end;
fun dynamic_value_strict cookie ctxt some_target postproc t args =
@@ -126,7 +126,7 @@
let
val evaluator = obtain_evaluator ctxt some_target program (map Constant consts');
val evaluation' = evaluation cookie ctxt evaluator;
- in fn _ => fn ((_, vs_ty), t) => fn _ => evaluation' (vs_ty, t) [] end;
+ in fn _ => fn _ => fn vs_ty_t => fn _ => evaluation' vs_ty_t [] end;
fun static_value_exn cookie ctxt some_target postproc consts =
let
@@ -175,14 +175,14 @@
(Thm.add_oracle (@{binding holds_by_evaluation},
fn (ctxt, evaluator, vs_t, ct) => check_holds ctxt evaluator vs_t ct)));
-fun check_holds_oracle ctxt evaluator ((_, vs_ty), t) deps ct =
- raw_check_holds_oracle (ctxt, evaluator, (vs_ty, t), ct);
+fun check_holds_oracle ctxt evaluator vs_ty_t ct =
+ raw_check_holds_oracle (ctxt, evaluator, vs_ty_t, ct);
in
fun dynamic_holds_conv ctxt = Code_Thingol.dynamic_conv ctxt
- (fn program => fn vs_t => fn deps =>
- check_holds_oracle ctxt (obtain_evaluator ctxt NONE program deps) vs_t deps)
+ (fn program => fn _ => fn vs_t => fn deps =>
+ check_holds_oracle ctxt (obtain_evaluator ctxt NONE program deps) vs_t)
o reject_vars ctxt;
fun static_holds_conv ctxt consts =
@@ -190,7 +190,7 @@
let
val evaluator' = obtain_evaluator ctxt NONE program (map Constant consts')
in
- fn ctxt' => fn vs_t => fn deps => check_holds_oracle ctxt' evaluator' vs_t deps o reject_vars ctxt'
+ fn ctxt' => fn _ => fn vs_t => fn _ => check_holds_oracle ctxt' evaluator' vs_t o reject_vars ctxt'
end);
(* o reject_vars ctxt'*)
--- a/src/Tools/Code/code_simp.ML Fri May 09 22:14:06 2014 +0200
+++ b/src/Tools/Code/code_simp.ML Fri May 09 22:56:06 2014 +0200
@@ -76,7 +76,7 @@
(* evaluation with dynamic code context *)
fun dynamic_conv ctxt = Code_Thingol.dynamic_conv ctxt
- (fn program => fn _ => fn _ => rewrite_modulo ctxt NONE program ctxt);
+ (fn program => fn _ => fn _ => fn _ => rewrite_modulo ctxt NONE program ctxt);
fun dynamic_tac ctxt = CONVERSION (dynamic_conv ctxt)
THEN' conclude_tac ctxt NONE ctxt;
@@ -87,8 +87,7 @@
val setup =
Method.setup @{binding code_simp}
(Scan.succeed (SIMPLE_METHOD' o (CHANGED_PROP oo dynamic_tac)))
- "simplification with code equations"
- #> Value.add_evaluator ("simp", dynamic_value);
+ "simplification with code equations";
(* evaluation with static code context *)
@@ -96,7 +95,7 @@
fun static_conv ctxt some_ss consts =
Code_Thingol.static_conv_simple ctxt consts
(fn program => let val conv' = rewrite_modulo ctxt some_ss program
- in fn ctxt' => fn _ => fn _ => conv' ctxt' end);
+ in fn ctxt' => fn _ => conv' ctxt' end);
fun static_tac ctxt some_ss consts =
let
--- a/src/Tools/Code/code_target.ML Fri May 09 22:14:06 2014 +0200
+++ b/src/Tools/Code/code_target.ML Fri May 09 22:56:06 2014 +0200
@@ -428,7 +428,7 @@
else Isabelle_System.with_tmp_dir "Code_Test" ext_check
end;
-fun evaluation mounted_serializer prepared_program syms all_public ((vs, ty), t) =
+fun subevaluator mounted_serializer prepared_program syms all_public ((vs, ty), t) =
let
val _ = if Code_Thingol.contains_dict_var t then
error "Term to be evaluated contains free dictionaries" else ();
@@ -449,7 +449,7 @@
let
val (mounted_serializer, (_, prepared_program)) =
mount_serializer ctxt target NONE generatedN [] program syms;
- in evaluation mounted_serializer prepared_program syms end;
+ in subevaluator mounted_serializer prepared_program syms end;
end; (* local *)
--- a/src/Tools/Code/code_thingol.ML Fri May 09 22:14:06 2014 +0200
+++ b/src/Tools/Code/code_thingol.ML Fri May 09 22:56:06 2014 +0200
@@ -86,20 +86,20 @@
val read_const_exprs: Proof.context -> string list -> string list
val consts_program: theory -> string list -> program
val dynamic_conv: Proof.context -> (program
- -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.T list -> conv)
+ -> (string -> (string * sort)) -> typscheme * iterm -> Code_Symbol.T list -> conv)
-> conv
val dynamic_value: Proof.context -> ((term -> term) -> 'a -> 'a) -> (program
- -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.T list -> 'a)
+ -> (string -> (string * sort)) -> typscheme * iterm -> Code_Symbol.T list -> 'a)
-> term -> 'a
val static_conv: Proof.context -> string list -> (program -> string list
- -> Proof.context -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.T list -> conv)
+ -> Proof.context -> (string -> (string * sort)) -> typscheme * iterm -> Code_Symbol.T list -> conv)
-> Proof.context -> conv
val static_conv_simple: Proof.context -> string list
- -> (program -> Proof.context -> (string * sort) list -> term -> conv)
+ -> (program -> Proof.context -> term -> conv)
-> Proof.context -> conv
val static_value: Proof.context -> ((term -> term) -> 'a -> 'a) -> string list ->
(program -> string list
- -> Proof.context -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.T list -> 'a)
+ -> Proof.context -> (string -> (string * sort)) -> typscheme * iterm -> Code_Symbol.T list -> 'a)
-> Proof.context -> term -> 'a
end;
@@ -388,7 +388,7 @@
exception PERMISSIVE of unit;
-fun translation_error ctxt program permissive some_thm deps msg sub_msg =
+fun translation_error ctxt permissive some_thm deps msg sub_msg =
if permissive
then raise PERMISSIVE ()
else
@@ -408,14 +408,14 @@
fun maybe_permissive f prgrm =
f prgrm |>> SOME handle PERMISSIVE () => (NONE, prgrm);
-fun not_wellsorted ctxt program permissive some_thm deps ty sort e =
+fun not_wellsorted ctxt permissive some_thm deps ty sort e =
let
val err_class = Sorts.class_error (Context.pretty ctxt) e;
val err_typ =
"Type " ^ Syntax.string_of_typ ctxt ty ^ " not of sort " ^
Syntax.string_of_sort ctxt sort;
in
- translation_error ctxt program permissive some_thm deps
+ translation_error ctxt permissive some_thm deps
"Wellsortedness error" (err_typ ^ "\n" ^ err_class)
end;
@@ -483,7 +483,7 @@
{class_relation = K (Sorts.classrel_derivation algebra class_relation),
type_constructor = type_constructor,
type_variable = type_variable} (ty, proj_sort sort)
- handle Sorts.CLASS_ERROR e => not_wellsorted ctxt program permissive some_thm deps ty sort e;
+ handle Sorts.CLASS_ERROR e => not_wellsorted ctxt permissive some_thm deps ty sort e;
in (typarg_witnesses, (deps, program)) end;
@@ -630,7 +630,7 @@
val thy = Proof_Context.theory_of ctxt;
val _ = if (case some_abs of NONE => true | SOME abs => not (c = abs))
andalso Code.is_abstr thy c
- then translation_error ctxt program permissive some_thm deps
+ then translation_error ctxt permissive some_thm deps
"Abstraction violation" ("constant " ^ Code.string_of_const thy c)
else ()
in translate_const_proper ctxt algbr eqngr permissive some_thm (c, ty) (deps, program) end
@@ -795,11 +795,18 @@
(* value evaluation *)
-fun ensure_value ctxt algbr eqngr t =
+fun normalize_tvars t =
let
val ty = fastype_of t;
- val vs = fold_term_types (K (fold_atyps (insert (eq_fst op =)
+ val vs_original = fold_term_types (K (fold_atyps (insert (eq_fst op =)
o dest_TFree))) t [];
+ val vs_normalized = Name.invent_names Name.context Name.aT (map snd vs_original);
+ val normalize = map_type_tfree (TFree o the o AList.lookup (op =) (vs_original ~~ vs_normalized));
+ in ((vs_original, (vs_normalized, normalize ty)), map_types normalize t) end;
+
+fun ensure_value ctxt algbr eqngr t_original =
+ let
+ val ((vs_original, (vs, ty)), t) = normalize_tvars t_original;
val t' = annotate ctxt algbr eqngr (@{const_name Pure.dummy_pattern}, ty) [] t;
val dummy_constant = Constant @{const_name Pure.dummy_pattern};
val stmt_value =
@@ -808,29 +815,27 @@
##>> translate_term ctxt algbr eqngr false NONE (t', NONE)
#>> (fn ((vs, ty), t) => Fun
(((vs, ty), [(([], t), (NONE, true))]), NONE));
- fun term_value (deps, program1) =
+ fun term_value (_, program1) =
let
- val Fun ((vs_ty, [(([], t), _)]), _) =
+ val Fun ((vs_ty as (vs, _), [(([], t), _)]), _) =
Code_Symbol.Graph.get_node program1 dummy_constant;
val deps' = Code_Symbol.Graph.immediate_succs program1 dummy_constant;
val program2 = Code_Symbol.Graph.del_node dummy_constant program1;
val deps_all = Code_Symbol.Graph.all_succs program2 deps';
val program3 = Code_Symbol.Graph.restrict (member (op =) deps_all) program2;
- in ((program3, ((vs_ty, t), deps')), (deps, program2)) end;
+ val vs_mapping = map fst vs ~~ vs_original;
+ in (((the o AList.lookup (op =) vs_mapping), (program3, ((vs_ty, t), deps'))), (deps', program2)) end;
in
ensure_stmt Constant stmt_value @{const_name Pure.dummy_pattern}
#> snd
#> term_value
end;
-fun original_sorts vs =
- map (fn (v, _) => (v, (the o AList.lookup (op =) vs o prefix "'") v));
-
-fun dynamic_evaluator ctxt evaluator algebra eqngr vs t =
+fun dynamic_evaluator ctxt evaluator algebra eqngr t =
let
- val ((program, (((vs', ty'), t'), deps)), _) =
+ val ((resubst_tvar, (program, ((vs_ty', t'), deps))), _) =
invoke_generation false (Proof_Context.theory_of ctxt) (algebra, eqngr) ensure_value t;
- in evaluator program ((original_sorts vs vs', (vs', ty')), t') deps end;
+ in evaluator program resubst_tvar (vs_ty', t') deps end;
fun dynamic_conv ctxt conv =
Code_Preproc.dynamic_conv ctxt (dynamic_evaluator ctxt conv);
@@ -838,22 +843,22 @@
fun dynamic_value ctxt postproc evaluator =
Code_Preproc.dynamic_value ctxt postproc (dynamic_evaluator ctxt evaluator);
-fun lift_evaluation ctxt evaluation algebra eqngr program vs t =
+fun static_subevaluator ctxt subevaluator algebra eqngr program t =
let
- val ((_, (((vs', ty'), t'), deps)), _) =
+ val ((resubst_tvar, (_, ((vs_ty', t'), deps))), _) =
ensure_value ctxt algebra eqngr t ([], program);
- in evaluation ctxt ((original_sorts vs vs', (vs', ty')), t') deps end;
+ in subevaluator ctxt resubst_tvar (vs_ty', t') deps end;
-fun lift_evaluator ctxt evaluator consts algebra eqngr =
+fun static_evaluator ctxt evaluator consts algebra eqngr =
let
fun generate_consts ctxt algebra eqngr =
fold_map (ensure_const ctxt algebra eqngr false);
val (consts', program) =
invoke_generation true (Proof_Context.theory_of ctxt) (algebra, eqngr) generate_consts consts;
- val evaluation = evaluator program consts';
- in fn ctxt' => lift_evaluation ctxt' evaluation algebra eqngr program end;
+ val subevaluator = evaluator program consts';
+ in fn ctxt' => static_subevaluator ctxt' subevaluator algebra eqngr program end;
-fun lift_evaluator_simple ctxt evaluator consts algebra eqngr =
+fun static_evaluator_simple ctxt evaluator consts algebra eqngr =
let
fun generate_consts ctxt algebra eqngr =
fold_map (ensure_const ctxt algebra eqngr false);
@@ -862,13 +867,13 @@
in evaluator program end;
fun static_conv ctxt consts conv =
- Code_Preproc.static_conv ctxt consts (lift_evaluator ctxt conv consts);
+ Code_Preproc.static_conv ctxt consts (static_evaluator ctxt conv consts);
fun static_conv_simple ctxt consts conv =
- Code_Preproc.static_conv ctxt consts (lift_evaluator_simple ctxt conv consts);
+ Code_Preproc.static_conv ctxt consts (static_evaluator_simple ctxt conv consts);
fun static_value ctxt postproc consts evaluator =
- Code_Preproc.static_value ctxt postproc consts (lift_evaluator ctxt evaluator consts);
+ Code_Preproc.static_value ctxt postproc consts (static_evaluator ctxt evaluator consts);
(** constant expressions **)
--- a/src/Tools/Code_Generator.thy Fri May 09 22:14:06 2014 +0200
+++ b/src/Tools/Code_Generator.thy Fri May 09 22:56:06 2014 +0200
@@ -7,14 +7,13 @@
theory Code_Generator
imports Pure
keywords
- "value" "print_codeproc" "code_thms" "code_deps" :: diag and
+ "print_codeproc" "code_thms" "code_deps" :: diag and
"export_code" "code_identifier" "code_printing" "code_reserved"
"code_monad" "code_reflect" :: thy_decl and
"datatypes" "functions" "module_name" "file" "checking"
"constant" "type_constructor" "type_class" "class_relation" "class_instance" "code_module"
begin
-ML_file "~~/src/Tools/value.ML"
ML_file "~~/src/Tools/cache_io.ML"
ML_file "~~/src/Tools/Code/code_preproc.ML"
ML_file "~~/src/Tools/Code/code_symbol.ML"
@@ -28,8 +27,7 @@
ML_file "~~/src/Tools/Code/code_scala.ML"
setup {*
- Value.setup
- #> Code_Preproc.setup
+ Code_Preproc.setup
#> Code_Simp.setup
#> Code_Target.setup
#> Code_ML.setup
@@ -66,7 +64,6 @@
ML_file "~~/src/Tools/Code/code_runtime.ML"
ML_file "~~/src/Tools/nbe.ML"
-setup Nbe.setup
hide_const (open) holds
--- a/src/Tools/nbe.ML Fri May 09 22:14:06 2014 +0200
+++ b/src/Tools/nbe.ML Fri May 09 22:56:06 2014 +0200
@@ -24,7 +24,6 @@
val put_result: (unit -> Univ list -> Univ list) -> Proof.context -> Proof.context
val trace: bool Unsynchronized.ref
- val setup: theory -> theory
val add_const_alias: thm -> theory -> theory
end;
@@ -502,10 +501,11 @@
(* reconstruction *)
-fun typ_of_itype vs (tyco `%% itys) =
- Type (tyco, map (typ_of_itype vs) itys)
- | typ_of_itype vs (ITyVar v) =
- TFree ("'" ^ v, (the o AList.lookup (op =) vs) v);
+fun typ_of_itype resubst_tvar =
+ let
+ fun typ_of (tyco `%% itys) = Type (tyco, map typ_of itys)
+ | typ_of (ITyVar v) = TFree (resubst_tvar v);
+ in typ_of end;
fun term_of_univ ctxt (idx_tab : Code_Symbol.T Inttab.table) t =
let
@@ -542,11 +542,11 @@
(* evaluation with type reconstruction *)
-fun eval_term raw_ctxt (nbe_program, idx_tab) ((vs0, (vs, ty)), t) deps =
+fun eval_term raw_ctxt (nbe_program, idx_tab) resubst_tvar ((vs, ty), t) deps =
let
val ctxt = Syntax.init_pretty_global (Proof_Context.theory_of raw_ctxt);
val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt);
- val ty' = typ_of_itype vs0 ty;
+ val ty' = typ_of_itype resubst_tvar ty;
fun type_infer t =
Syntax.check_term (Config.put Type_Infer_Context.const_sorts false ctxt)
(Type.constraint ty' t);
@@ -592,11 +592,11 @@
val (_, raw_oracle) = Context.>>> (Context.map_theory_result
(Thm.add_oracle (@{binding normalization_by_evaluation},
- fn (ctxt, nbe_program_idx_tab, vsp_ty_t, deps, ct) =>
- mk_equals ctxt ct (eval_term ctxt nbe_program_idx_tab vsp_ty_t deps))));
+ fn (ctxt, nbe_program_idx_tab, resubst_tvars, vs_ty_t, deps, ct) =>
+ mk_equals ctxt ct (eval_term ctxt nbe_program_idx_tab resubst_tvars vs_ty_t deps))));
-fun oracle ctxt nbe_program_idx_tab vsp_ty_t deps ct =
- raw_oracle (ctxt, nbe_program_idx_tab, vsp_ty_t, deps, ct);
+fun oracle ctxt nbe_program_idx_tab resubst_tvars vs_ty_t deps ct =
+ raw_oracle (ctxt, nbe_program_idx_tab, resubst_tvars, vs_ty_t, deps, ct);
fun dynamic_conv ctxt = lift_triv_classes_conv ctxt
(Code_Thingol.dynamic_conv ctxt (oracle ctxt o compile false ctxt));
@@ -616,9 +616,4 @@
(fn program => fn _ => K (eval_term ctxt (compile true ctxt program)));
in fn ctxt' => lift_triv_classes_rew ctxt' (evaluator ctxt') end;
-
-(** setup **)
-
-val setup = Value.add_evaluator ("nbe", dynamic_value);
-
end;
--- a/src/Tools/value.ML Fri May 09 22:14:06 2014 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,79 +0,0 @@
-(* Title: Tools/value.ML
- Author: Florian Haftmann, TU Muenchen
-
-Generic value command for arbitrary evaluators.
-*)
-
-signature VALUE =
-sig
- val value: Proof.context -> term -> term
- val value_select: string -> Proof.context -> term -> term
- val value_cmd: string option -> string list -> string -> Toplevel.state -> unit
- val add_evaluator: string * (Proof.context -> term -> term) -> theory -> theory
- val setup : theory -> theory
-end;
-
-structure Value : VALUE =
-struct
-
-structure Evaluator = Theory_Data
-(
- type T = (string * (Proof.context -> term -> term)) list;
- val empty = [];
- val extend = I;
- fun merge data : T = AList.merge (op =) (K true) data;
-)
-
-val add_evaluator = Evaluator.map o AList.update (op =);
-
-fun value_select name ctxt =
- case AList.lookup (op =) (Evaluator.get (Proof_Context.theory_of ctxt)) name
- of NONE => error ("No such evaluator: " ^ name)
- | SOME f => f ctxt;
-
-fun value ctxt t = let val evaluators = Evaluator.get (Proof_Context.theory_of ctxt)
- in if null evaluators then error "No evaluators"
- else let val (evaluators, (_, evaluator)) = split_last evaluators
- in case get_first (fn (_, f) => try (f ctxt) t) evaluators
- of SOME t' => t'
- | NONE => evaluator ctxt t
- end end;
-
-fun value_maybe_select some_name =
- case some_name
- of NONE => value
- | SOME name => value_select name;
-
-fun value_cmd some_name modes raw_t state =
- let
- val ctxt = Toplevel.context_of state;
- val t = Syntax.read_term ctxt raw_t;
- val t' = value_maybe_select some_name ctxt t;
- val ty' = Term.type_of t';
- val ctxt' = Variable.auto_fixes t' ctxt;
- val p = Print_Mode.with_modes modes (fn () =>
- Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
- Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
- in Pretty.writeln p end;
-
-val opt_modes =
- Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
-
-val opt_evaluator =
- Scan.option (@{keyword "["} |-- Parse.xname --| @{keyword "]"})
-
-val _ =
- Outer_Syntax.improper_command @{command_spec "value"} "evaluate and print term"
- (opt_evaluator -- opt_modes -- Parse.term
- >> (fn ((some_name, modes), t) => Toplevel.keep (value_cmd some_name modes t)));
-
-val antiq_setup =
- Thy_Output.antiquotation @{binding value}
- (Scan.lift opt_evaluator -- Term_Style.parse -- Args.term)
- (fn {source, context, ...} => fn ((some_name, style), t) => Thy_Output.output context
- (Thy_Output.maybe_pretty_source Thy_Output.pretty_term context source
- [style (value_maybe_select some_name context t)]));
-
-val setup = antiq_setup;
-
-end;