--- a/CONTRIBUTORS Wed Feb 22 16:21:26 2017 +0000
+++ b/CONTRIBUTORS Wed Feb 22 20:24:50 2017 +0100
@@ -6,6 +6,9 @@
Contributions to this Isabelle version
--------------------------------------
+* February 2017: Florian Haftmann, TUM
+ Statically embedded computatations implementated by generated code.
+
Contributions to Isabelle2016-1
-------------------------------
--- a/NEWS Wed Feb 22 16:21:26 2017 +0000
+++ b/NEWS Wed Feb 22 20:24:50 2017 +0100
@@ -12,6 +12,17 @@
* Document antiquotations @{prf} and @{full_prf} output proof terms
(again) in the same way as commands 'prf' and 'full_prf'.
+* Computations generated by the code generator can be embedded
+directly into ML, alongside with @{code} antiquotations, using
+the following antiquotations:
+
+ @{computation … terms: … datatypes: …} : ((term -> term) -> 'ml option -> 'a) -> Proof.context -> term -> 'a
+ @{computation_conv … terms: … datatypes: …} : ('ml -> conv) -> Proof.context -> conv
+ @{computation_check terms: … datatypes: …} : Proof.context -> conv
+
+See src/HOL/ex/Computations.thy, src/HOL/Decision_Procs/Commutative_Ring.thy
+and src/HOL/Decision_Procs/Reflective_Field.thy for examples.
+
*** Prover IDE -- Isabelle/Scala/jEdit ***
--- a/src/Doc/Codegen/Adaptation.thy Wed Feb 22 16:21:26 2017 +0000
+++ b/src/Doc/Codegen/Adaptation.thy Wed Feb 22 20:24:50 2017 +0100
@@ -148,7 +148,7 @@
discretion of the user to take care for this.
\<close>
-subsection \<open>Common adaptation applications\<close>
+subsection \<open>Common adaptation applications \label{sec:common_adaptation}\<close>
text \<open>
The @{theory HOL} @{theory Main} theory already provides a code
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/Codegen/Computations.thy Wed Feb 22 20:24:50 2017 +0100
@@ -0,0 +1,544 @@
+theory Computations
+ imports Setup
+ "~~/src/HOL/Library/Code_Target_Int"
+ "~~/src/HOL/Library/Code_Char"
+begin
+
+section \<open>Computations \label{sec:computations}\<close>
+
+subsection \<open>Prelude -- The @{text code} antiquotation \label{sec:code_antiq}\<close>
+
+text \<open>
+ The @{ML_antiquotation_def code} antiquotation allows to include constants
+ from
+ generated code directly into ML system code, as in the following toy
+ example:
+\<close>
+
+datatype %quote form = T | F | And form form | Or form form (*<*)
+
+(*>*) ML %quotetypewriter \<open>
+ fun eval_form @{code T} = true
+ | eval_form @{code F} = false
+ | eval_form (@{code And} (p, q)) =
+ eval_form p andalso eval_form q
+ | eval_form (@{code Or} (p, q)) =
+ eval_form p orelse eval_form q;
+\<close>
+
+text \<open>
+ \noindent The antiquotation @{ML_antiquotation code} takes
+ the name of a constant as argument;
+ the required code is generated
+ transparently and the corresponding constant names are inserted
+ for the given antiquotations. This technique allows to use pattern
+ matching on constructors stemming from compiled datatypes.
+ Note that the @{ML_antiquotation code}
+ antiquotation may not refer to constants which carry adaptations;
+ here you have to refer to the corresponding adapted code directly.
+\<close>
+
+
+subsection \<open>The concept of computations\<close>
+
+text \<open>
+ Computations embody the simple idea that for each
+ monomorphic Isabelle/HOL term of type @{text \<tau>} by virtue of
+ code generation there exists an corresponding ML type @{text T} and
+ a morphism @{text "\<Phi> :: \<tau> \<rightarrow> T"} satisfying
+ @{text "\<Phi> (t\<^sub>1 \<cdot> t\<^sub>2) = \<Phi> t\<^sub>1 \<cdot> \<Phi> t\<^sub>2"}, with @{text \<cdot>} denoting
+ term application.
+
+ For a given Isabelle/HOL type @{text \<tau>}, parts of @{text \<Phi>} can be
+ implemented by a corresponding ML function @{text "\<phi>\<^sub>\<tau> :: term \<rightarrow> T"}.
+ How?
+
+ \<^descr> \<open>Let input be a constant C :: \<tau>.\<close> \\
+ Then @{text "\<phi>\<^sub>\<tau> C = f\<^sub>C"} with @{text "f\<^sub>C"} being
+ the image of @{text C} under code generation.
+
+ \<^descr> \<open>Let input be an application (t\<^sub>1 \<cdot> t\<^sub>2) :: \<tau>.\<close> \\
+ Then @{text "\<phi>\<^sub>\<tau> (t\<^sub>1 \<cdot> t\<^sub>2) = \<phi>\<^sub>\<tau> t\<^sub>1 (\<phi>\<^sub>\<tau> t\<^sub>2)"}.
+
+ \noindent Using these trivial properties, each monomorphic constant
+ @{text "C : \<^vec>\<tau>\<^sub>n \<rightarrow> \<tau>"} yields the following
+ equations:
+\<close>
+
+text %quote \<open>
+ @{text "\<phi>\<^bsub>(\<tau>\<^sub>1 \<rightarrow> \<tau>\<^sub>2 \<rightarrow> \<dots> \<rightarrow> \<tau>\<^sub>n \<rightarrow> \<tau>)\<^esub> C = f\<^sub>C"} \\
+ @{text "\<phi>\<^bsub>(\<tau>\<^sub>2 \<rightarrow> \<dots> \<rightarrow> \<tau>\<^sub>n \<rightarrow> \<tau>)\<^esub> (C \<cdot> t\<^sub>1) = f\<^sub>C (\<phi>\<^bsub>\<tau>\<^sub>1\<^esub> t\<^sub>1)"} \\
+ @{text "\<dots>"} \\
+ @{text "\<phi>\<^bsub>\<tau>\<^esub> (C \<cdot> t\<^sub>1 \<cdot> \<dots> \<cdot> t\<^sub>n) = f\<^sub>C (\<phi>\<^bsub>\<tau>\<^sub>1\<^esub> t\<^sub>1) \<dots> (\<phi>\<^bsub>\<tau>\<^sub>n\<^esub> t\<^sub>n)"}
+\<close>
+
+text \<open>
+ \noindent Hence a computation is characterized as follows:
+
+ \<^item> Let @{text "input constants"} denote a set of monomorphic constants.
+
+ \<^item> Let @{text \<tau>} denote a monomorphic type and @{text "'ml"} be a schematic
+ placeholder for its corresponding type in ML under code generation.
+
+ \<^item> Then the corresponding computation is an ML function of type
+ @{ML_type "Proof.context -> term -> 'ml"}
+ partially implementing the morphism @{text "\<Phi> :: \<tau> \<rightarrow> T"} for all
+ \<^emph>\<open>input terms\<close> consisting only of input constants and applications.
+
+ \noindent The charming idea is that all required code is automatically generated
+ by the code generator for givens input constants and types;
+ that code is directly inserted into the Isabelle/ML runtime system
+ by means of antiquotations.
+\<close>
+
+
+subsection \<open>The @{text computation} antiquotation\<close>
+
+text \<open>
+ The following example illustrates its basic usage:
+\<close>
+
+ML %quotetypewriter \<open>
+ local
+
+ fun int_of_nat @{code "0 :: nat"} = 0
+ | int_of_nat (@{code Suc} n) = int_of_nat n + 1;
+
+ in
+
+ val comp_nat = @{computation nat terms:
+ "plus :: nat \<Rightarrow> nat \<Rightarrow> nat" "times :: nat \<Rightarrow> nat \<Rightarrow> nat"
+ "sum_list :: nat list \<Rightarrow> nat" "prod_list :: nat list \<Rightarrow> nat"
+ datatypes: nat "nat list"}
+ (fn post => post o HOLogic.mk_nat o int_of_nat o the);
+
+ end
+\<close>
+
+text \<open>
+ \<^item> Antiquotations occurring in the
+ same ML block always refer to the same transparently generated code;
+ particularly, they share the same transparently generated datatype
+ declarations.
+
+ \<^item> The type of a computation is specified as first argument.
+
+ \<^item> Input constants are specified the following ways:
+
+ \<^item> Each term following @{text "terms:"} specifies all constants
+ it contains as input constants.
+
+ \<^item> Each type following @{text "datatypes:"} specifies all constructors
+ of the corresponding code datatype as input constants. Note that
+ this does not increase expressiveness but succinctness for datatypes
+ with many constructors.
+
+ \<^item> The code generated by a @{text computation} antiquotation takes a functional argument
+ which describes how to conclude the computation. What's the rationale
+ behind this?
+
+ \<^item> There is no automated way to generate a reconstruction function
+ from the resulting ML type to a Isabelle term -- this is in the
+ responsibility of the implementor. One possible approach
+ for robust term reconstruction is the @{text code} antiquotation.
+
+ \<^item> Both statically specified input constants and dynamically provided input
+ terms are subject to preprocessing. Likewise the result
+ is supposed to be subject to postprocessing; the implementor
+ is expected this out explicitly.
+
+ \<^item> Computations follow the partiality principle (cf.~\secref{sec:partiality_principle}):
+ failures due to pattern matching or unspecified functions
+ are interpreted as partiality; therefore resulting ML values
+ are optional.
+
+ Hence the functional argument accepts the following parameters
+
+ \<^item> A postprocessor function @{ML_type "term -> term"}.
+
+ \<^item> The resulting value as optional argument.
+
+ The functional argument is supposed to compose the final result
+ from these in a suitable manner.
+
+ \noindent A simple application:
+\<close>
+
+ML_val %quotetypewriter \<open>
+ comp_nat @{context} @{term "sum_list [Suc 0, Suc (Suc 0)] * Suc (Suc 0)"}
+\<close>
+
+text \<open>
+ \noindent A single ML block may contain an arbitrary number of computation
+ antiquotations. These share the \<^emph>\<open>same\<close> set of possible
+ input constants. In other words, it does not matter in which
+ antiquotation constants are specified; in the following example,
+ \<^emph>\<open>all\<close> constants are specified by the first antiquotation once
+ and for all:
+\<close>
+
+ML %quotetypewriter \<open>
+ local
+
+ fun int_of_nat @{code "0 :: nat"} = 0
+ | int_of_nat (@{code Suc} n) = int_of_nat n + 1;
+
+ in
+
+ val comp_nat = @{computation nat terms:
+ "plus :: nat \<Rightarrow> nat \<Rightarrow> nat" "times :: nat \<Rightarrow> nat \<Rightarrow> nat"
+ "sum_list :: nat list \<Rightarrow> nat" "prod_list :: nat list \<Rightarrow> nat"
+ "replicate :: nat \<Rightarrow> nat \<Rightarrow> nat list"
+ datatypes: nat "nat list"}
+ (fn post => post o HOLogic.mk_nat o int_of_nat o the);
+
+ val comp_nat_list = @{computation "nat list"}
+ (fn post => post o HOLogic.mk_list @{typ nat} o
+ map (HOLogic.mk_nat o int_of_nat) o the);
+
+ end
+\<close>
+
+
+subsection \<open>Pitfalls when specifying input constants \label{sec:input_constants_pitfalls}\<close>
+
+text \<open>
+ \<^descr> \<open>Complete type coverage.\<close> Specified input constants must
+ be \<^emph>\<open>complete\<close> in the sense that for each
+ required type @{text \<tau>} there is at least one corresponding
+ input constant which can actually \<^emph>\<open>construct\<close> a concrete
+ value of type @{text \<tau>}, potentially requiring more types recursively;
+ otherwise the system of equations cannot be generated properly.
+ Hence such incomplete input constants sets are rejected immediately.
+
+ \<^descr> \<open>Unsuitful right hand sides.\<close> The generated code for a computation
+ must compile in the strict ML runtime environment. This imposes
+ the technical restriction that each compiled input constant
+ @{text f\<^sub>C} on the right hand side of a generated equations
+ must compile without throwing an exception. That rules
+ out pathological examples like @{term [source] "undefined :: nat"}
+ as input constants, as well as abstract constructors (cf. \secref{sec:invariant}).
+
+ \<^descr> \<open>Preprocessing.\<close> For consistency, input constants are subject
+ to preprocessing; however, the overall approach requires
+ to operate on constants @{text C} and their respective compiled images
+ @{text f\<^sub>C}.\footnote{Technical restrictions of the implementation
+ enforce this, although those could be lifted in the future.}
+ This is a problem whenever preprocessing maps an input constant
+ to a non-constant.
+
+ To circumvent these situations, the computation machinery
+ has a dedicated preprocessor which is applied \<^emph>\<open>before\<close>
+ the regular preprocessing, both to input constants as well as
+ input terms. This can be used to map problematic constants
+ to other ones that are not subject to regular preprocessing.
+ Rewrite rules are added using attribute @{attribute code_computation_unfold}.
+ There should rarely be a need to use this beyond the few default
+ setups in HOL, which deal with literals (see also \secref{sec:literal_input}).
+\<close>
+
+
+subsection \<open>Pitfalls concerning input terms\<close>
+
+text \<open>
+ \<^descr> \<open>No polymorphims.\<close> Input terms must be monomorphic: compilation
+ to ML requires dedicated choice of monomorphic types.
+
+ \<^descr> \<open>No abstractions.\<close> Only constants and applications are admissible
+ as input; abstractions are not possible. In theory, the
+ compilation schema could be extended to cover abstractions also,
+ but this would increase the trusted code base. If abstractions
+ are required, they can always be eliminated by a dedicated preprocessing
+ step, e.g.~using combinatorial logic.
+
+ \<^descr> \<open>Potential interfering of the preprocessor.\<close> As described in \secref{sec:input_constants_pitfalls}
+ regular preprocessing can have a disruptive effect for input constants.
+ The same also applies to input terms; however the same measures
+ to circumvent that problem for input constants apply to input terms also.
+\<close>
+
+
+subsection \<open>Computations using the @{text computation_conv} antiquotation\<close>
+
+text \<open>
+ Computations are a device to implement fast proof procedures.
+ Then results of a computation are often assumed to be trustable
+ and thus wrapped in oracles (see \cite{isabelle-isar-ref}),
+ as in the following example:\footnote{
+ The technical details how numerals are dealt with are given later in
+ \secref{sec:literal_input}.}
+\<close>
+
+ML %quotetypewriter \<open>
+ local
+
+ fun raw_dvd (b, ct) = Thm.mk_binop @{cterm "Pure.eq :: bool \<Rightarrow> bool \<Rightarrow> prop"}
+ ct (if b then @{cterm True} else @{cterm False});
+
+ val (_, dvd_oracle) = Context.>>> (Context.map_theory_result
+ (Thm.add_oracle (@{binding dvd}, raw_dvd)));
+
+ in
+
+ val conv_dvd = @{computation_conv bool terms:
+ "Rings.dvd :: int \<Rightarrow> int \<Rightarrow> bool"
+ "plus :: int \<Rightarrow> int \<Rightarrow> int"
+ "minus :: int \<Rightarrow> int \<Rightarrow> int"
+ "times :: int \<Rightarrow> int \<Rightarrow> int"
+ "0 :: int" "1 :: int" "2 :: int" "3 :: int" "-1 :: int"
+ } (curry dvd_oracle)
+
+ end
+\<close>
+
+text \<open>
+ \<^item> Antiquotation @{ML_antiquotation computation_conv} basically yields
+ a conversion of type @{ML_type "Proof.context -> cterm -> thm"}
+ (see further \cite{isabelle-implementation}).
+
+ \<^item> The antiquotation expects one functional argument to bridge the
+ \qt{untrusted gap}; this can be done e.g.~using an oracle. Since that oracle
+ will only yield \qt{valid} results in the context of that particular
+ computation, the implementor must make sure that it does not leave
+ the local ML scope; in this example, this is achieved using
+ an explicit @{text local} ML block. The very presence of the oracle
+ in the code acknowledges that each computation requires explicit thinking
+ before it can be considered trustworthy!
+
+ \<^item> Postprocessing just operates as further conversion after normalization.
+
+ \<^item> Partiality makes the whole conversion fall back to reflexivity.
+\<close> (*<*)
+
+(*>*) ML_val %quotetypewriter \<open>
+ conv_dvd @{context} @{cterm "7 dvd ( 62437867527846782 :: int)"};
+ conv_dvd @{context} @{cterm "7 dvd (-62437867527846783 :: int)"};
+\<close>
+
+text \<open>
+ \noindent An oracle is not the only way to construct a valid theorem.
+ A computation result can be used to construct an appropriate certificate:
+\<close>
+
+lemma %quote conv_div_cert:
+ "(Code_Target_Int.positive r * Code_Target_Int.positive s)
+ div Code_Target_Int.positive s \<equiv> (numeral r :: int)" (is "?lhs \<equiv> ?rhs")
+proof (rule eq_reflection)
+ have "?lhs = numeral r * numeral s div numeral s"
+ by simp
+ also have "numeral r * numeral s div numeral s = ?rhs"
+ by (rule nonzero_mult_div_cancel_right) simp
+ finally show "?lhs = ?rhs" .
+qed
+
+lemma %quote positive_mult:
+ "Code_Target_Int.positive r * Code_Target_Int.positive s =
+ Code_Target_Int.positive (r * s)"
+ by simp
+
+ML %quotetypewriter \<open>
+ local
+
+ fun integer_of_int (@{code int_of_integer} k) = k
+
+ val cterm_of_int = Thm.cterm_of @{context} o HOLogic.mk_numeral o integer_of_int;
+
+ val divisor = Thm.dest_arg o Thm.dest_arg;
+
+ fun evaluate thm =
+ Simplifier.rewrite_rule
+ (Proof_Context.transfer (Thm.theory_of_thm thm) @{context})
+ (map mk_eq @{thms arith_simps positive_mult}) thm; (*FIXME proper ctxt*)
+
+ fun revaluate k ct =
+ @{thm conv_div_cert}
+ |> Thm.instantiate' [] [SOME (cterm_of_int k), SOME (divisor ct)]
+ |> evaluate;
+
+ in
+
+ val conv_div = @{computation_conv int terms:
+ "divide :: int \<Rightarrow> int \<Rightarrow> int"
+ "0 :: int" "1 :: int" "2 :: int" "3 :: int"
+ } revaluate
+
+ end
+\<close>
+
+ML_val %quotetypewriter \<open>
+ conv_div @{context}
+ @{cterm "46782454343499999992777742432342242323423425 div (7 :: int)"}
+\<close>
+
+text \<open>
+ \noindent The example is intentionally kept simple: only positive
+ integers are covered, only remainder-free divisions are feasible,
+ and the input term is expected to have a particular shape.
+ This exhibits the idea more clearly:
+ the result of the computation is used as a mere
+ hint how to instantiate @{fact conv_div_cert}, from which the required
+ theorem is obtained by performing multiplication using the
+ simplifier; hence that theorem is built of proper inferences,
+ with no oracles involved.
+\<close>
+
+
+subsection \<open>Computations using the @{text computation_check} antiquotation\<close>
+
+text \<open>
+ The @{text computation_check} antiquotation is convenient if
+ only a positive checking of propositions is desired, because then
+ the result type is fixed (@{typ prop}) and all the technical
+ matter concerning postprocessing and oracles is done in the framework
+ once and for all:
+\<close>
+
+ML %quotetypewriter \<open>
+ val check_nat = @{computation_check terms:
+ Trueprop "less :: nat \<Rightarrow> nat \<Rightarrow> bool" "plus :: nat \<Rightarrow> nat \<Rightarrow> nat"
+ "times :: nat \<Rightarrow> nat \<Rightarrow> nat"
+ "0 :: nat" Suc
+ }
+\<close>
+
+text \<open>
+ \noindent The HOL judgement @{term Trueprop} embeds an expression
+ of type @{typ bool} into @{typ prop}.
+\<close>
+
+ML_val %quotetypewriter \<open>
+ check_nat @{context} @{cprop "less (Suc (Suc 0)) (Suc (Suc (Suc 0)))"}
+\<close>
+
+text \<open>
+ \noindent Note that such computations can only \<^emph>\<open>check\<close>
+ for @{typ prop}s to hold but not \<^emph>\<open>decide\<close>.
+\<close>
+
+
+subsection \<open>Some practical hints\<close>
+
+subsubsection \<open>Inspecting generated code\<close>
+
+text \<open>
+ The antiquotations for computations attempt to produce meaningful error
+ messages. If these are not sufficient, it might by useful to
+ inspect the generated code, which can be achieved using
+\<close>
+
+declare %quote [[ML_source_trace]] (*<*) declare %quote [[ML_source_trace = false]] (*>*)
+
+
+subsubsection \<open>Literals as input constants \label{sec:literal_input}\<close>
+
+text \<open>
+ Literals (characters, numerals) in computations cannot be processed
+ naively: the compilation pattern for computations fails whenever
+ target-language literals are involved; since various
+ common code generator setups (see \secref{sec:common_adaptation})
+ implement @{typ nat} and @{typ int} by target-language literals,
+ this problem manifests whenever numeric types are involved.
+ In practice, this is circumvented with a dedicated preprocessor
+ setup for literals (see also \secref{sec:input_constants_pitfalls}).
+
+ The following examples illustrate the pattern
+ how to specify input constants when literals are involved, without going into
+ too much detail:
+\<close>
+
+paragraph \<open>An example for @{typ nat}\<close>
+
+ML %quotetypewriter \<open>
+ val check_nat = @{computation_check terms:
+ Trueprop "even :: nat \<Rightarrow> bool" "plus :: nat \<Rightarrow> nat \<Rightarrow> nat"
+ "0 :: nat" Suc "1 :: nat" "2 :: nat" "3 :: nat"
+ }
+\<close>
+
+ML_val %quotetypewriter \<open>
+ check_nat @{context} @{cprop "even (Suc 0 + 1 + 2 + 3 + 4 + 5)"}
+\<close>
+
+paragraph \<open>An example for @{typ int}\<close>
+
+ML %quotetypewriter \<open>
+ val check_int = @{computation_check terms:
+ Trueprop "even :: int \<Rightarrow> bool" "plus :: int \<Rightarrow> int \<Rightarrow> int"
+ "0 :: int" "1 :: int" "2 :: int" "3 :: int" "-1 :: int"
+ }
+\<close>
+
+ML_val %quotetypewriter \<open>
+ check_int @{context} @{cprop "even ((0::int) + 1 + 2 + 3 + -1 + -2 + -3)"}
+\<close>
+
+paragraph \<open>An example for @{typ char}\<close>
+
+definition %quote is_cap_letter :: "char \<Rightarrow> bool"
+ where "is_cap_letter c \<longleftrightarrow> (let n = nat_of_char c in 65 \<le> n \<and> n \<le> 90)" (*<*)
+
+(*>*) ML %quotetypewriter \<open>
+ val check_char = @{computation_check terms:
+ Trueprop is_cap_letter
+ Char datatypes: num
+ }
+\<close>
+
+ML_val %quotetypewriter \<open>
+ check_char @{context} @{cprop "is_cap_letter (CHR ''Y'')"}
+\<close>
+
+
+subsubsection \<open>Preprocessing HOL terms into evaluable shape\<close>
+
+text \<open>
+ When integrating decision procedures developed inside HOL into HOL itself,
+ a common approach is to use a deep embedding where operators etc.
+ are represented by datatypes in Isabelle/HOL. Then it is necessary
+ to turn generic shallowly embedded statements into that particular
+ deep embedding (\qt{reification}).
+
+ One option is to hardcode using code antiquotations (see \secref{sec:code_antiq}).
+ Another option is to use pre-existing infrastructure in HOL:
+ @{ML "Reification.conv"} and @{ML "Reification.tac"}.
+
+ A simplistic example:
+\<close>
+
+datatype %quote form_ord = T | F | Less nat nat
+ | And form_ord form_ord | Or form_ord form_ord | Neg form_ord
+
+primrec %quote interp :: "form_ord \<Rightarrow> 'a::order list \<Rightarrow> bool"
+where
+ "interp T vs \<longleftrightarrow> True"
+| "interp F vs \<longleftrightarrow> False"
+| "interp (Less i j) vs \<longleftrightarrow> vs ! i < vs ! j"
+| "interp (And f1 f2) vs \<longleftrightarrow> interp f1 vs \<and> interp f2 vs"
+| "interp (Or f1 f2) vs \<longleftrightarrow> interp f1 vs \<or> interp f2 vs"
+| "interp (Neg f) vs \<longleftrightarrow> \<not> interp f vs"
+
+text \<open>
+ \noindent The datatype @{type form_ord} represents formulae whose semantics is given by
+ @{const interp}. Note that values are represented by variable indices (@{typ nat})
+ whose concrete values are given in list @{term vs}.
+\<close>
+
+ML %quotetypewriter (*<*) \<open>\<close>
+lemma "thm": fixes x y z :: "'a::order" shows "x < y \<and> x < z \<equiv> interp (And (Less (Suc 0) (Suc (Suc 0))) (Less (Suc 0) 0)) [z, x, y]"
+ML_prf %quotetypewriter
+(*>*) \<open>val thm =
+ Reification.conv @{context} @{thms interp.simps} @{cterm "x < y \<and> x < z"}\<close> (*<*)
+by (tactic \<open>ALLGOALS (resolve_tac @{context} [thm])\<close>)
+(*>*)
+
+text \<open>
+ \noindent By virtue of @{fact interp.simps}, @{ML "Reification.conv"} provides a conversion
+ which, for this concrete example, yields @{thm thm [no_vars]}. Note that the argument
+ to @{const interp} does not contain any free variables and can thus be evaluated
+ using evaluation.
+
+ A less meager example can be found in the AFP, session @{text "Regular-Sets"},
+ theory @{text Regexp_Method}.
+\<close>
+
+end
--- a/src/Doc/Codegen/Evaluation.thy Wed Feb 22 16:21:26 2017 +0000
+++ b/src/Doc/Codegen/Evaluation.thy Wed Feb 22 20:24:50 2017 +0100
@@ -22,14 +22,14 @@
subsection \<open>Evaluation techniques\<close>
text \<open>
- The existing infrastructure provides a rich palette of evaluation
+ There is a rich palette of evaluation
techniques, each comprising different aspects:
\begin{description}
- \item[Expressiveness.] Depending on how good symbolic computation
- is supported, the class of terms which can be evaluated may be
- bigger or smaller.
+ \item[Expressiveness.] Depending on the extent to which symbolic
+ computation is possible, the class of terms which can be evaluated
+ can be bigger or smaller.
\item[Efficiency.] The more machine-near the technique, the
faster it is.
@@ -67,27 +67,26 @@
subsubsection \<open>Evaluation in ML (@{text code})\<close>
text \<open>
- Highest performance can be achieved by evaluation in ML, at the cost
+ Considerable performance can be achieved using evaluation in ML, at the cost
of being restricted to ground results and a layered stack of code to
- be trusted, including code generator configurations by the user.
+ be trusted, including a user's specific code generator setup.
Evaluation is carried out in a target language \emph{Eval} which
inherits from \emph{SML} but for convenience uses parts of the
- Isabelle runtime environment. The soundness of computation carried
- out there depends crucially on the correctness of the code
- generator setup; this is one of the reasons why you should not use
- adaptation (see \secref{sec:adaptation}) frivolously.
+ Isabelle runtime environment. Hence soundness depends crucially
+ on the correctness of the code generator setup; this is one of the
+ reasons why you should not use adaptation (see \secref{sec:adaptation})
+ frivolously.
\<close>
-subsection \<open>Aspects of evaluation\<close>
+subsection \<open>Dynamic evaluation\<close>
text \<open>
- Each of the techniques can be combined with different aspects. The
- most important distinction is between dynamic and static evaluation.
Dynamic evaluation takes the code generator configuration \qt{as it
- is} at the point where evaluation is issued. Best example is the
- @{command_def value} command which allows ad-hoc evaluation of
+ is} at the point where evaluation is issued and computes
+ a corresponding result. Best example is the
+ @{command_def value} command for ad-hoc evaluation of
terms:
\<close>
@@ -103,257 +102,103 @@
value %quote [nbe] "42 / (12 :: rat)"
text \<open>
- To employ dynamic evaluation in the document generation, there is also
+ To employ dynamic evaluation in documents, there is also
a @{text value} antiquotation with the same evaluation techniques
as @{command value}.
+\<close>
- Static evaluation freezes the code generator configuration at a
- certain point and uses this context whenever evaluation is issued
- later on. This is particularly appropriate for proof procedures
- which use evaluation, since then the behaviour of evaluation is not
- changed or even compromised later on by actions of the user.
+
+subsubsection \<open>Term reconstruction in ML\<close>
- As a technical complication, terms after evaluation in ML must be
+text \<open>
+ Results from evaluation in ML must be
turned into Isabelle's internal term representation again. Since
- this is also configurable, it is never fully trusted. For this
- reason, evaluation in ML comes with further aspects:
+ that setup is highly configurable, it is never assumed to be trustable.
+ Hence evaluation in ML provides no full term reconstruction
+ but distinguishes the following kinds:
\begin{description}
- \item[Plain evaluation.] A term is normalized using the provided
- term reconstruction from ML to Isabelle; for applications which
- do not need to be fully trusted.
+ \item[Plain evaluation.] A term is normalized using the vanilla
+ term reconstruction from ML to Isabelle; this is a pragmatic
+ approach for applications which do not need trustability.
\item[Property conversion.] Evaluates propositions; since these
are monomorphic, the term reconstruction is fixed once and for all
- and therefore trustable.
-
- \item[Conversion.] Evaluates an arbitrary term @{term "t"} first
- by plain evaluation and certifies the result @{term "t'"} by
- checking the equation @{term "t \<equiv> t'"} using property
- conversion.
+ and therefore trustable -- in the sense that only the regular
+ code generator setup has to be trusted, without relying
+ on term reconstruction from ML to Isabelle.
\end{description}
- \noindent The picture is further complicated by the roles of
- exceptions. Here three cases have to be distinguished:
-
- \begin{itemize}
-
- \item Evaluation of @{term t} terminates with a result @{term
- "t'"}.
-
- \item Evaluation of @{term t} terminates which an exception
- indicating a pattern match failure or a non-implemented
- function. As sketched in \secref{sec:partiality}, this can be
- interpreted as partiality.
-
- \item Evaluation raises any other kind of exception.
-
- \end{itemize}
-
- \noindent For conversions, the first case yields the equation @{term
- "t = t'"}, the second defaults to reflexivity @{term "t = t"}.
- Exceptions of the third kind are propagated to the user.
-
- By default return values of plain evaluation are optional, yielding
- @{text "SOME t'"} in the first case, @{text "NONE"} in the
- second, and propagating the exception in the third case. A strict
- variant of plain evaluation either yields @{text "t'"} or propagates
- any exception, a liberal variant captures any exception in a result
- of type @{text "Exn.result"}.
-
- For property conversion (which coincides with conversion except for
- evaluation in ML), methods are provided which solve a given goal by
- evaluation.
+ \noindent The different degree of trustability is also manifest in the
+ types of the corresponding ML functions: plain evaluation
+ operates on uncertified terms, whereas property conversion
+ operates on certified terms.
\<close>
-subsection \<open>Schematic overview\<close>
+subsubsection \<open>The partiality principle \label{sec:partiality_principle}\<close>
+
+text \<open>
+ During evaluation exceptions indicating a pattern
+ match failure or a non-implemented function are treated specially:
+ as sketched in \secref{sec:partiality}, such
+ exceptions can be interpreted as partiality. For plain evaluation,
+ the result hence is optional; property conversion falls back
+ to reflexivity in such cases.
+\<close>
+
+
+subsubsection \<open>Schematic overview\<close>
text \<open>
\newcommand{\ttsize}{\fontsize{5.8pt}{8pt}\selectfont}
\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
- & 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_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}
- & property conversion & &
- & \ttsize@{ML "Code_Runtime.static_holds_conv"} \tabularnewline \cline{2-5}
- & conversion & \ttsize@{ML "Code_Simp.static_conv"}
- & \ttsize@{ML "Nbe.static_conv"}
- & \ttsize@{ML "Code_Evaluation.static_conv"}
+ \begin{tabular}{l||c|c|c}
+ & @{text simp} & @{text nbe} & @{text code} \tabularnewline \hline \hline
+ interactive evaluation & @{command value} @{text "[simp]"} & @{command value} @{text "[nbe]"} & @{command value} @{text "[code]"} \tabularnewline
+ plain evaluation & & & \ttsize@{ML "Code_Evaluation.dynamic_value"} \tabularnewline \hline
+ evaluation method & @{method code_simp} & @{method normalization} & @{method eval} \tabularnewline
+ property conversion & & & \ttsize@{ML "Code_Runtime.dynamic_holds_conv"} \tabularnewline \hline
+ conversion & \ttsize@{ML "Code_Simp.dynamic_conv"} & \ttsize@{ML "Nbe.dynamic_conv"}
\end{tabular}
\<close>
-text \<open>
- \noindent Note that @{ML Code_Evaluation.static_value} and
- @{ML Code_Evaluation.static_conv} require certain code equations to
- reconstruct Isabelle terms from results and certify results. This is
- achieved as follows:
-
- \<^enum> Identify which result types are expected.
-
- \<^enum> Define an auxiliary operation which for each possible result type @{text \<tau>}
- contains a term @{const Code_Evaluation.TERM_OF} of type @{text "\<tau> itself"}
- (for @{ML Code_Evaluation.static_value}) or
- a term @{const Code_Evaluation.TERM_OF_EQUAL} of type @{text "\<tau> itself"}
- (for @{ML Code_Evaluation.static_conv}) respectively.
-
- \<^enum> Include that auxiliary operation into the set of constants when generating
- the static conversion.
-\<close>
-
-
-subsection \<open>Preprocessing HOL terms into evaluable shape\<close>
-
+
+subsection \<open>Static evaluation\<close>
+
text \<open>
- When integrating decision procedures developed inside HOL into HOL itself,
- it is necessary to somehow get from the Isabelle/ML representation to
- the representation used by the decision procedure itself (``reification'').
- One option is to hardcode it using code antiquotations (see \secref{sec:code_antiq}).
- Another option is to use pre-existing infrastructure in HOL:
- @{ML "Reification.conv"} and @{ML "Reification.tac"}
-
- A simplistic example:
-\<close>
-
-datatype %quote form_ord = T | F | Less nat nat
- | And form_ord form_ord | Or form_ord form_ord | Neg form_ord
-
-primrec %quote interp :: "form_ord \<Rightarrow> 'a::order list \<Rightarrow> bool"
-where
- "interp T vs \<longleftrightarrow> True"
-| "interp F vs \<longleftrightarrow> False"
-| "interp (Less i j) vs \<longleftrightarrow> vs ! i < vs ! j"
-| "interp (And f1 f2) vs \<longleftrightarrow> interp f1 vs \<and> interp f2 vs"
-| "interp (Or f1 f2) vs \<longleftrightarrow> interp f1 vs \<or> interp f2 vs"
-| "interp (Neg f) vs \<longleftrightarrow> \<not> interp f vs"
-
-text \<open>
- The datatype @{type form_ord} represents formulae whose semantics is given by
- @{const interp}. Note that values are represented by variable indices (@{typ nat})
- whose concrete values are given in list @{term vs}.
-\<close>
-
-ML (*<*) \<open>\<close>
-schematic_goal "thm": fixes x y z :: "'a::order" shows "x < y \<and> x < z \<equiv> ?P"
-ML_prf
-(*>*) \<open>val thm =
- Reification.conv @{context} @{thms interp.simps} @{cterm "x < y \<and> x < z"}\<close> (*<*)
-by (tactic \<open>ALLGOALS (resolve_tac @{context} [thm])\<close>)
-(*>*)
-
-text \<open>
- By virtue of @{fact interp.simps}, @{ML "Reification.conv"} provides a conversion
- which, for this concrete example, yields @{thm thm [no_vars]}. Note that the argument
- to @{const interp} does not contain any free variables and can thus be evaluated
- using evaluation.
-
- A less meager example can be found in the AFP, session @{text "Regular-Sets"},
- theory @{text Regexp_Method}.
+ When implementing proof procedures using evaluation,
+ in most cases the code generator setup is appropriate
+ \qt{as it was} when the proof procedure was written in ML,
+ not an arbitrary later potentially modified setup. This is
+ called static evaluation.
\<close>
-subsection \<open>Intimate connection between logic and system runtime\<close>
-
-text \<open>
- The toolbox of static evaluation conversions forms a reasonable base
- to interweave generated code and system tools. However in some
- situations more direct interaction is desirable.
-\<close>
-
-
-subsubsection \<open>Static embedding of generated code into system runtime -- the @{text code} antiquotation \label{sec:code_antiq}\<close>
-
+subsubsection \<open>Static evaluation using @{text simp} and @{text nbe}\<close>
+
text \<open>
- The @{text code} antiquotation allows to include constants from
- generated code directly into ML system code, as in the following toy
- example:
-\<close>
-
-datatype %quote form = T | F | And form form | Or form form (*<*)
-
-(*>*) ML %quotett \<open>
- fun eval_form @{code T} = true
- | eval_form @{code F} = false
- | eval_form (@{code And} (p, q)) =
- eval_form p andalso eval_form q
- | eval_form (@{code Or} (p, q)) =
- eval_form p orelse eval_form q;
-\<close>
-
-text \<open>
- \noindent @{text code} takes as argument the name of a constant;
- after the whole ML is read, the necessary code is generated
- transparently and the corresponding constant names are inserted.
- This technique also allows to use pattern matching on constructors
- stemming from compiled datatypes. Note that the @{text code}
- antiquotation may not refer to constants which carry adaptations;
- here you have to refer to the corresponding adapted code directly.
-
- For a less simplistic example, theory @{text Approximation} in
- the @{text Decision_Procs} session is a good reference.
+ For @{text simp} and @{text nbe} static evaluation can be achieved using
+ @{ML Code_Simp.static_conv} and @{ML Nbe.static_conv}.
+ Note that @{ML Nbe.static_conv} by its very nature
+ requires an invocation of the ML compiler for every call,
+ which can produce significant overhead.
\<close>
-subsubsection \<open>Static embedding of generated code into system runtime -- @{text code_reflect}\<close>
-
-text \<open>
- The @{text code} antiquoation is lightweight, but the generated code
- is only accessible while the ML section is processed. Sometimes this
- is not appropriate, especially if the generated code contains datatype
- declarations which are shared with other parts of the system. In these
- cases, @{command_def code_reflect} can be used:
-\<close>
-
-code_reflect %quote Sum_Type
- datatypes sum = Inl | Inr
- functions "Sum_Type.sum.projl" "Sum_Type.sum.projr"
+subsubsection \<open>Intimate connection between logic and system runtime\<close>
text \<open>
- \noindent @{command_def code_reflect} takes a structure name and
- references to datatypes and functions; for these code is compiled
- into the named ML structure and the \emph{Eval} target is modified
- in a way that future code generation will reference these
- precompiled versions of the given datatypes and functions. This
- also allows to refer to the referenced datatypes and functions from
- arbitrary ML code as well.
-
- A typical example for @{command code_reflect} can be found in the
- @{theory Predicate} theory.
+ Static evaluation for @{text eval} operates differently --
+ the required generated code is inserted directly into an ML
+ block using antiquotations. The idea is that generated
+ code performing static evaluation (called a \<^emph>\<open>computation\<close>)
+ is compiled once and for all such that later calls do not
+ require any invocation of the code generator or the ML
+ compiler at all. This topic deserved a dedicated chapter
+ \secref{sec:computations}.
\<close>
-
-
-subsubsection \<open>Separate compilation -- @{text code_reflect}\<close>
-
-text \<open>
- For technical reasons it is sometimes necessary to separate
- generation and compilation of code which is supposed to be used in
- the system runtime. For this @{command code_reflect} with an
- optional \<^theory_text>\<open>file\<close> argument can be used:
-\<close>
-
-code_reflect %quote Rat
- datatypes rat
- functions Fract
- "(plus :: rat \<Rightarrow> rat \<Rightarrow> rat)" "(minus :: rat \<Rightarrow> rat \<Rightarrow> rat)"
- "(times :: rat \<Rightarrow> rat \<Rightarrow> rat)" "(divide :: rat \<Rightarrow> rat \<Rightarrow> rat)"
- file "$ISABELLE_TMP/examples/rat.ML"
-
-text \<open>
- \noindent This merely generates the referenced code to the given
- file which can be included into the system runtime later on.
-\<close>
-
+
end
-
--- a/src/Doc/Codegen/Further.thy Wed Feb 22 16:21:26 2017 +0000
+++ b/src/Doc/Codegen/Further.thy Wed Feb 22 20:24:50 2017 +0100
@@ -4,6 +4,57 @@
section \<open>Further issues \label{sec:further}\<close>
+subsection \<open>Incorporating generated code directly into the system runtime -- @{text code_reflect}\<close>
+
+subsubsection \<open>Static embedding of generated code into the system runtime\<close>
+
+text \<open>
+ The @{ML_antiquotation code} antiquotation is lightweight, but the generated code
+ is only accessible while the ML section is processed. Sometimes this
+ is not appropriate, especially if the generated code contains datatype
+ declarations which are shared with other parts of the system. In these
+ cases, @{command_def code_reflect} can be used:
+\<close>
+
+code_reflect %quote Sum_Type
+ datatypes sum = Inl | Inr
+ functions "Sum_Type.sum.projl" "Sum_Type.sum.projr"
+
+text \<open>
+ \noindent @{command code_reflect} takes a structure name and
+ references to datatypes and functions; for these code is compiled
+ into the named ML structure and the \emph{Eval} target is modified
+ in a way that future code generation will reference these
+ precompiled versions of the given datatypes and functions. This
+ also allows to refer to the referenced datatypes and functions from
+ arbitrary ML code as well.
+
+ A typical example for @{command code_reflect} can be found in the
+ @{theory Predicate} theory.
+\<close>
+
+
+subsubsection \<open>Separate compilation\<close>
+
+text \<open>
+ For technical reasons it is sometimes necessary to separate
+ generation and compilation of code which is supposed to be used in
+ the system runtime. For this @{command code_reflect} with an
+ optional \<^theory_text>\<open>file\<close> argument can be used:
+\<close>
+
+code_reflect %quote Rat
+ datatypes rat
+ functions Fract
+ "(plus :: rat \<Rightarrow> rat \<Rightarrow> rat)" "(minus :: rat \<Rightarrow> rat \<Rightarrow> rat)"
+ "(times :: rat \<Rightarrow> rat \<Rightarrow> rat)" "(divide :: rat \<Rightarrow> rat \<Rightarrow> rat)"
+ file "$ISABELLE_TMP/examples/rat.ML"
+
+text \<open>
+ \noindent This merely generates the referenced code to the given
+ file which can be included into the system runtime later on.
+\<close>
+
subsection \<open>Specialities of the @{text Scala} target language \label{sec:scala}\<close>
text \<open>
--- a/src/Doc/Codegen/document/root.tex Wed Feb 22 16:21:26 2017 +0000
+++ b/src/Doc/Codegen/document/root.tex Wed Feb 22 20:24:50 2017 +0100
@@ -36,6 +36,7 @@
\input{Refinement.tex}
\input{Inductive_Predicate.tex}
\input{Evaluation.tex}
+\input{Computations.tex}
\input{Adaptation.tex}
\input{Further.tex}
--- a/src/Doc/Codegen/document/style.sty Wed Feb 22 16:21:26 2017 +0000
+++ b/src/Doc/Codegen/document/style.sty Wed Feb 22 20:24:50 2017 +0100
@@ -18,6 +18,9 @@
\newcommand{\qt}[1]{``{#1}''}
\newcommand{\ditem}[1]{\item[\isastyletext #1]}
+%% vectors
+\newcommand{\isactrlvec}[1]{\emph{$\overline{#1}$}}
+
%% quote environment
\isakeeptag{quote}
\renewenvironment{quote}
--- a/src/Doc/ROOT Wed Feb 22 16:21:26 2017 +0000
+++ b/src/Doc/ROOT Wed Feb 22 20:24:50 2017 +0100
@@ -29,6 +29,7 @@
Refinement
Inductive_Predicate
Evaluation
+ Computations
Adaptation
Further
document_files (in "..")