# HG changeset patch # User haftmann # Date 1487791490 -3600 # Node ID 2525e680f94ff4362d05ab6107ded1e975104585 # Parent 5975839e8d258472a751642b06bc6d7ab0747472 basic documentation for computations diff -r 5975839e8d25 -r 2525e680f94f CONTRIBUTORS --- 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 ------------------------------- diff -r 5975839e8d25 -r 2525e680f94f NEWS --- 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 *** diff -r 5975839e8d25 -r 2525e680f94f src/Doc/Codegen/Adaptation.thy --- 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. \ -subsection \Common adaptation applications\ +subsection \Common adaptation applications \label{sec:common_adaptation}\ text \ The @{theory HOL} @{theory Main} theory already provides a code diff -r 5975839e8d25 -r 2525e680f94f src/Doc/Codegen/Computations.thy --- /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 \Computations \label{sec:computations}\ + +subsection \Prelude -- The @{text code} antiquotation \label{sec:code_antiq}\ + +text \ + The @{ML_antiquotation_def code} antiquotation allows to include constants + from + generated code directly into ML system code, as in the following toy + example: +\ + +datatype %quote form = T | F | And form form | Or form form (*<*) + +(*>*) ML %quotetypewriter \ + 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; +\ + +text \ + \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. +\ + + +subsection \The concept of computations\ + +text \ + Computations embody the simple idea that for each + monomorphic Isabelle/HOL term of type @{text \} by virtue of + code generation there exists an corresponding ML type @{text T} and + a morphism @{text "\ :: \ \ T"} satisfying + @{text "\ (t\<^sub>1 \ t\<^sub>2) = \ t\<^sub>1 \ \ t\<^sub>2"}, with @{text \} denoting + term application. + + For a given Isabelle/HOL type @{text \}, parts of @{text \} can be + implemented by a corresponding ML function @{text "\\<^sub>\ :: term \ T"}. + How? + + \<^descr> \Let input be a constant C :: \.\ \\ + Then @{text "\\<^sub>\ C = f\<^sub>C"} with @{text "f\<^sub>C"} being + the image of @{text C} under code generation. + + \<^descr> \Let input be an application (t\<^sub>1 \ t\<^sub>2) :: \.\ \\ + Then @{text "\\<^sub>\ (t\<^sub>1 \ t\<^sub>2) = \\<^sub>\ t\<^sub>1 (\\<^sub>\ t\<^sub>2)"}. + + \noindent Using these trivial properties, each monomorphic constant + @{text "C : \<^vec>\\<^sub>n \ \"} yields the following + equations: +\ + +text %quote \ + @{text "\\<^bsub>(\\<^sub>1 \ \\<^sub>2 \ \ \ \\<^sub>n \ \)\<^esub> C = f\<^sub>C"} \\ + @{text "\\<^bsub>(\\<^sub>2 \ \ \ \\<^sub>n \ \)\<^esub> (C \ t\<^sub>1) = f\<^sub>C (\\<^bsub>\\<^sub>1\<^esub> t\<^sub>1)"} \\ + @{text "\"} \\ + @{text "\\<^bsub>\\<^esub> (C \ t\<^sub>1 \ \ \ t\<^sub>n) = f\<^sub>C (\\<^bsub>\\<^sub>1\<^esub> t\<^sub>1) \ (\\<^bsub>\\<^sub>n\<^esub> t\<^sub>n)"} +\ + +text \ + \noindent Hence a computation is characterized as follows: + + \<^item> Let @{text "input constants"} denote a set of monomorphic constants. + + \<^item> Let @{text \} 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 "\ :: \ \ T"} for all + \<^emph>\input terms\ 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. +\ + + +subsection \The @{text computation} antiquotation\ + +text \ + The following example illustrates its basic usage: +\ + +ML %quotetypewriter \ + 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 \ nat \ nat" "times :: nat \ nat \ nat" + "sum_list :: nat list \ nat" "prod_list :: nat list \ nat" + datatypes: nat "nat list"} + (fn post => post o HOLogic.mk_nat o int_of_nat o the); + + end +\ + +text \ + \<^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: +\ + +ML_val %quotetypewriter \ + comp_nat @{context} @{term "sum_list [Suc 0, Suc (Suc 0)] * Suc (Suc 0)"} +\ + +text \ + \noindent A single ML block may contain an arbitrary number of computation + antiquotations. These share the \<^emph>\same\ set of possible + input constants. In other words, it does not matter in which + antiquotation constants are specified; in the following example, + \<^emph>\all\ constants are specified by the first antiquotation once + and for all: +\ + +ML %quotetypewriter \ + 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 \ nat \ nat" "times :: nat \ nat \ nat" + "sum_list :: nat list \ nat" "prod_list :: nat list \ nat" + "replicate :: nat \ nat \ 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 +\ + + +subsection \Pitfalls when specifying input constants \label{sec:input_constants_pitfalls}\ + +text \ + \<^descr> \Complete type coverage.\ Specified input constants must + be \<^emph>\complete\ in the sense that for each + required type @{text \} there is at least one corresponding + input constant which can actually \<^emph>\construct\ a concrete + value of type @{text \}, potentially requiring more types recursively; + otherwise the system of equations cannot be generated properly. + Hence such incomplete input constants sets are rejected immediately. + + \<^descr> \Unsuitful right hand sides.\ 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> \Preprocessing.\ 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>\before\ + 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}). +\ + + +subsection \Pitfalls concerning input terms\ + +text \ + \<^descr> \No polymorphims.\ Input terms must be monomorphic: compilation + to ML requires dedicated choice of monomorphic types. + + \<^descr> \No abstractions.\ 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> \Potential interfering of the preprocessor.\ 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. +\ + + +subsection \Computations using the @{text computation_conv} antiquotation\ + +text \ + 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}.} +\ + +ML %quotetypewriter \ + local + + fun raw_dvd (b, ct) = Thm.mk_binop @{cterm "Pure.eq :: bool \ bool \ 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 \ int \ bool" + "plus :: int \ int \ int" + "minus :: int \ int \ int" + "times :: int \ int \ int" + "0 :: int" "1 :: int" "2 :: int" "3 :: int" "-1 :: int" + } (curry dvd_oracle) + + end +\ + +text \ + \<^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. +\ (*<*) + +(*>*) ML_val %quotetypewriter \ + conv_dvd @{context} @{cterm "7 dvd ( 62437867527846782 :: int)"}; + conv_dvd @{context} @{cterm "7 dvd (-62437867527846783 :: int)"}; +\ + +text \ + \noindent An oracle is not the only way to construct a valid theorem. + A computation result can be used to construct an appropriate certificate: +\ + +lemma %quote conv_div_cert: + "(Code_Target_Int.positive r * Code_Target_Int.positive s) + div Code_Target_Int.positive s \ (numeral r :: int)" (is "?lhs \ ?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 \ + 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 \ int \ int" + "0 :: int" "1 :: int" "2 :: int" "3 :: int" + } revaluate + + end +\ + +ML_val %quotetypewriter \ + conv_div @{context} + @{cterm "46782454343499999992777742432342242323423425 div (7 :: int)"} +\ + +text \ + \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. +\ + + +subsection \Computations using the @{text computation_check} antiquotation\ + +text \ + 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: +\ + +ML %quotetypewriter \ + val check_nat = @{computation_check terms: + Trueprop "less :: nat \ nat \ bool" "plus :: nat \ nat \ nat" + "times :: nat \ nat \ nat" + "0 :: nat" Suc + } +\ + +text \ + \noindent The HOL judgement @{term Trueprop} embeds an expression + of type @{typ bool} into @{typ prop}. +\ + +ML_val %quotetypewriter \ + check_nat @{context} @{cprop "less (Suc (Suc 0)) (Suc (Suc (Suc 0)))"} +\ + +text \ + \noindent Note that such computations can only \<^emph>\check\ + for @{typ prop}s to hold but not \<^emph>\decide\. +\ + + +subsection \Some practical hints\ + +subsubsection \Inspecting generated code\ + +text \ + 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 +\ + +declare %quote [[ML_source_trace]] (*<*) declare %quote [[ML_source_trace = false]] (*>*) + + +subsubsection \Literals as input constants \label{sec:literal_input}\ + +text \ + 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: +\ + +paragraph \An example for @{typ nat}\ + +ML %quotetypewriter \ + val check_nat = @{computation_check terms: + Trueprop "even :: nat \ bool" "plus :: nat \ nat \ nat" + "0 :: nat" Suc "1 :: nat" "2 :: nat" "3 :: nat" + } +\ + +ML_val %quotetypewriter \ + check_nat @{context} @{cprop "even (Suc 0 + 1 + 2 + 3 + 4 + 5)"} +\ + +paragraph \An example for @{typ int}\ + +ML %quotetypewriter \ + val check_int = @{computation_check terms: + Trueprop "even :: int \ bool" "plus :: int \ int \ int" + "0 :: int" "1 :: int" "2 :: int" "3 :: int" "-1 :: int" + } +\ + +ML_val %quotetypewriter \ + check_int @{context} @{cprop "even ((0::int) + 1 + 2 + 3 + -1 + -2 + -3)"} +\ + +paragraph \An example for @{typ char}\ + +definition %quote is_cap_letter :: "char \ bool" + where "is_cap_letter c \ (let n = nat_of_char c in 65 \ n \ n \ 90)" (*<*) + +(*>*) ML %quotetypewriter \ + val check_char = @{computation_check terms: + Trueprop is_cap_letter + Char datatypes: num + } +\ + +ML_val %quotetypewriter \ + check_char @{context} @{cprop "is_cap_letter (CHR ''Y'')"} +\ + + +subsubsection \Preprocessing HOL terms into evaluable shape\ + +text \ + 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: +\ + +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 \ 'a::order list \ bool" +where + "interp T vs \ True" +| "interp F vs \ False" +| "interp (Less i j) vs \ vs ! i < vs ! j" +| "interp (And f1 f2) vs \ interp f1 vs \ interp f2 vs" +| "interp (Or f1 f2) vs \ interp f1 vs \ interp f2 vs" +| "interp (Neg f) vs \ \ interp f vs" + +text \ + \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}. +\ + +ML %quotetypewriter (*<*) \\ +lemma "thm": fixes x y z :: "'a::order" shows "x < y \ x < z \ interp (And (Less (Suc 0) (Suc (Suc 0))) (Less (Suc 0) 0)) [z, x, y]" +ML_prf %quotetypewriter +(*>*) \val thm = + Reification.conv @{context} @{thms interp.simps} @{cterm "x < y \ x < z"}\ (*<*) +by (tactic \ALLGOALS (resolve_tac @{context} [thm])\) +(*>*) + +text \ + \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}. +\ + +end diff -r 5975839e8d25 -r 2525e680f94f src/Doc/Codegen/Evaluation.thy --- 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 \Evaluation techniques\ text \ - 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 \Evaluation in ML (@{text code})\ text \ - 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. \ -subsection \Aspects of evaluation\ +subsection \Dynamic evaluation\ text \ - 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: \ @@ -103,257 +102,103 @@ value %quote [nbe] "42 / (12 :: rat)" text \ - 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}. +\ - 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 \Term reconstruction in ML\ - As a technical complication, terms after evaluation in ML must be +text \ + 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 \ 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. \ -subsection \Schematic overview\ +subsubsection \The partiality principle \label{sec:partiality_principle}\ + +text \ + 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. +\ + + +subsubsection \Schematic overview\ text \ \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} \ -text \ - \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 \} - contains a term @{const Code_Evaluation.TERM_OF} of type @{text "\ itself"} - (for @{ML Code_Evaluation.static_value}) or - a term @{const Code_Evaluation.TERM_OF_EQUAL} of type @{text "\ itself"} - (for @{ML Code_Evaluation.static_conv}) respectively. - - \<^enum> Include that auxiliary operation into the set of constants when generating - the static conversion. -\ - - -subsection \Preprocessing HOL terms into evaluable shape\ - + +subsection \Static evaluation\ + text \ - 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: -\ - -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 \ 'a::order list \ bool" -where - "interp T vs \ True" -| "interp F vs \ False" -| "interp (Less i j) vs \ vs ! i < vs ! j" -| "interp (And f1 f2) vs \ interp f1 vs \ interp f2 vs" -| "interp (Or f1 f2) vs \ interp f1 vs \ interp f2 vs" -| "interp (Neg f) vs \ \ interp f vs" - -text \ - 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}. -\ - -ML (*<*) \\ -schematic_goal "thm": fixes x y z :: "'a::order" shows "x < y \ x < z \ ?P" -ML_prf -(*>*) \val thm = - Reification.conv @{context} @{thms interp.simps} @{cterm "x < y \ x < z"}\ (*<*) -by (tactic \ALLGOALS (resolve_tac @{context} [thm])\) -(*>*) - -text \ - 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. \ -subsection \Intimate connection between logic and system runtime\ - -text \ - 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. -\ - - -subsubsection \Static embedding of generated code into system runtime -- the @{text code} antiquotation \label{sec:code_antiq}\ - +subsubsection \Static evaluation using @{text simp} and @{text nbe}\ + text \ - The @{text code} antiquotation allows to include constants from - generated code directly into ML system code, as in the following toy - example: -\ - -datatype %quote form = T | F | And form form | Or form form (*<*) - -(*>*) ML %quotett \ - 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; -\ - -text \ - \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. \ -subsubsection \Static embedding of generated code into system runtime -- @{text code_reflect}\ - -text \ - 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: -\ - -code_reflect %quote Sum_Type - datatypes sum = Inl | Inr - functions "Sum_Type.sum.projl" "Sum_Type.sum.projr" +subsubsection \Intimate connection between logic and system runtime\ text \ - \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>\computation\) + 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}. \ - - -subsubsection \Separate compilation -- @{text code_reflect}\ - -text \ - 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>\file\ argument can be used: -\ - -code_reflect %quote Rat - datatypes rat - functions Fract - "(plus :: rat \ rat \ rat)" "(minus :: rat \ rat \ rat)" - "(times :: rat \ rat \ rat)" "(divide :: rat \ rat \ rat)" - file "$ISABELLE_TMP/examples/rat.ML" - -text \ - \noindent This merely generates the referenced code to the given - file which can be included into the system runtime later on. -\ - + end - diff -r 5975839e8d25 -r 2525e680f94f src/Doc/Codegen/Further.thy --- 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 \Further issues \label{sec:further}\ +subsection \Incorporating generated code directly into the system runtime -- @{text code_reflect}\ + +subsubsection \Static embedding of generated code into the system runtime\ + +text \ + 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: +\ + +code_reflect %quote Sum_Type + datatypes sum = Inl | Inr + functions "Sum_Type.sum.projl" "Sum_Type.sum.projr" + +text \ + \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. +\ + + +subsubsection \Separate compilation\ + +text \ + 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>\file\ argument can be used: +\ + +code_reflect %quote Rat + datatypes rat + functions Fract + "(plus :: rat \ rat \ rat)" "(minus :: rat \ rat \ rat)" + "(times :: rat \ rat \ rat)" "(divide :: rat \ rat \ rat)" + file "$ISABELLE_TMP/examples/rat.ML" + +text \ + \noindent This merely generates the referenced code to the given + file which can be included into the system runtime later on. +\ + subsection \Specialities of the @{text Scala} target language \label{sec:scala}\ text \ diff -r 5975839e8d25 -r 2525e680f94f src/Doc/Codegen/document/root.tex --- 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} diff -r 5975839e8d25 -r 2525e680f94f src/Doc/Codegen/document/style.sty --- 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} diff -r 5975839e8d25 -r 2525e680f94f src/Doc/ROOT --- 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 "..")