# HG changeset patch # User haftmann # Date 1464269270 -7200 # Node ID 2660ba49879803b9484624ea856473fed617150e # Parent 80a91e0e236e556858aebe2950af531f8e0605bb delegate inclusion of required dictionaries to user-space instead of half-working magic diff -r 80a91e0e236e -r 2660ba498798 NEWS --- a/NEWS Thu May 26 15:27:50 2016 +0200 +++ b/NEWS Thu May 26 15:27:50 2016 +0200 @@ -101,6 +101,11 @@ permutations of a set, i.e. the set of all lists that contain every element of the carrier set exactly once. +* Static evaluators (Code_Evaluation.static_* in Isabelle/ML) rely on +explicitly provided auxiliary definitions for required type class +dictionaries rather than half-working magic. INCOMPATIBILITY, see +the tutorial on code generation for details. + * New abbreviations for negated existence (but not bounded existence): \x. P x \ \ (\x. P x) diff -r 80a91e0e236e -r 2660ba498798 src/Doc/Codegen/Evaluation.thy --- a/src/Doc/Codegen/Evaluation.thy Thu May 26 15:27:50 2016 +0200 +++ b/src/Doc/Codegen/Evaluation.thy Thu May 26 15:27:50 2016 +0200 @@ -143,7 +143,7 @@ \item Evaluation of @{term t} terminates with a result @{term "t'"}. - \item Evaluation of @{term t} terminates which en exception + \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. @@ -195,18 +195,36 @@ \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\ text \ - When integration decision procedures developed inside HOL into HOL itself, + 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"} - An simplistic example: + A simplistic example: \ datatype %quote form_ord = T | F | Less nat nat diff -r 80a91e0e236e -r 2660ba498798 src/HOL/Code_Evaluation.thy --- a/src/HOL/Code_Evaluation.thy Thu May 26 15:27:50 2016 +0200 +++ b/src/HOL/Code_Evaluation.thy Thu May 26 15:27:50 2016 +0200 @@ -68,6 +68,19 @@ subsection \Tools setup and evaluation\ +context +begin + +qualified definition TERM_OF :: "'a::term_of itself" +where + "TERM_OF = snd (Code_Evaluation.term_of :: 'a \ _, TYPE('a))" + +qualified definition TERM_OF_EQUAL :: "'a::term_of itself" +where + "TERM_OF_EQUAL = snd (\(a::'a). (Code_Evaluation.term_of a, HOL.eq a), TYPE('a))" + +end + lemma eq_eq_TrueD: fixes x y :: "'a::{}" assumes "(x \ y) \ Trueprop True" diff -r 80a91e0e236e -r 2660ba498798 src/HOL/Tools/code_evaluation.ML --- a/src/HOL/Tools/code_evaluation.ML Thu May 26 15:27:50 2016 +0200 +++ b/src/HOL/Tools/code_evaluation.ML Thu May 26 15:27:50 2016 +0200 @@ -9,14 +9,14 @@ val dynamic_value: Proof.context -> term -> term option val dynamic_value_strict: Proof.context -> term -> term val dynamic_value_exn: Proof.context -> term -> term Exn.result - val static_value: { ctxt: Proof.context, consts: string list, Ts: typ list } + val static_value: { ctxt: Proof.context, consts: string list } -> Proof.context -> term -> term option - val static_value_strict: { ctxt: Proof.context, consts: string list, Ts: typ list } + val static_value_strict: { ctxt: Proof.context, consts: string list } -> Proof.context -> term -> term - val static_value_exn: { ctxt: Proof.context, consts: string list, Ts: typ list } + val static_value_exn: { ctxt: Proof.context, consts: string list } -> Proof.context -> term -> term Exn.result val dynamic_conv: Proof.context -> conv - val static_conv: { ctxt: Proof.context, consts: string list, Ts: typ list } + val static_conv: { ctxt: Proof.context, consts: string list } -> Proof.context -> conv val put_term: (unit -> term) -> Proof.context -> Proof.context val tracing: string -> 'a -> 'a @@ -183,8 +183,6 @@ fun mk_term_of t = HOLogic.mk_term_of (fastype_of t) t; -fun term_of_const_for thy = Axclass.unoverload_const thy o dest_Const o HOLogic.term_of_const; - fun gen_dynamic_value computation ctxt t = computation cookie ctxt NONE I (mk_term_of t) []; @@ -192,11 +190,10 @@ val dynamic_value_strict = gen_dynamic_value Code_Runtime.dynamic_value_strict; val dynamic_value_exn = gen_dynamic_value Code_Runtime.dynamic_value_exn; -fun gen_static_value computation { ctxt, consts, Ts } = +fun gen_static_value computation { ctxt, consts } = let val computation' = computation cookie - { ctxt = ctxt, target = NONE, lift_postproc = I, consts = - union (op =) (map (term_of_const_for (Proof_Context.theory_of ctxt)) Ts) consts } + { ctxt = ctxt, target = NONE, lift_postproc = I, consts = consts } in fn ctxt' => computation' ctxt' o mk_term_of end; val static_value = gen_static_value Code_Runtime.static_value; @@ -219,13 +216,12 @@ fun dynamic_conv ctxt = certify_eval ctxt dynamic_value Code_Runtime.dynamic_holds_conv; -fun static_conv { ctxt, consts, Ts } = +fun static_conv { ctxt, consts } = let - val eqs = @{const_name Pure.eq} :: @{const_name HOL.eq} :: - map (fn T => Axclass.unoverload_const (Proof_Context.theory_of ctxt) - (@{const_name HOL.equal}, T)) Ts; (*assumes particular code equations for Pure.eq etc.*) - val value = static_value { ctxt = ctxt, consts = consts, Ts = Ts }; - val holds = Code_Runtime.static_holds_conv { ctxt = ctxt, consts = union (op =) eqs consts }; + val value = static_value { ctxt = ctxt, consts = consts }; + val holds = Code_Runtime.static_holds_conv { ctxt = ctxt, + consts = insert (op =) @{const_name Pure.eq} consts + (*assumes particular code equation for Pure.eq*) }; in fn ctxt' => certify_eval ctxt' value holds end;