summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | haftmann |

Wed, 22 Feb 2017 20:24:50 +0100 | |

changeset 65041 | 2525e680f94f |

parent 65040 | 5975839e8d25 |

child 65042 | 956ea00a162a |

basic documentation for computations

--- 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}