# HG changeset patch # User blanchet # Date 1410888217 -7200 # Node ID 919149921e467293634de992fc8a1f03f24cf2fc # Parent 107341a1594677701d4015cdd86a35028e92b17c added 'extraction' plugins -- this might help 'HOL-Proofs' diff -r 107341a15946 -r 919149921e46 src/HOL/Code_Evaluation.thy --- a/src/HOL/Code_Evaluation.thy Tue Sep 16 18:42:33 2014 +0200 +++ b/src/HOL/Code_Evaluation.thy Tue Sep 16 19:23:37 2014 +0200 @@ -13,7 +13,7 @@ subsubsection {* Terms and class @{text term_of} *} -datatype (plugins only: code) "term" = dummy_term +datatype (plugins only: code extraction) "term" = dummy_term definition Const :: "String.literal \ typerep \ term" where "Const _ _ = dummy_term" diff -r 107341a15946 -r 919149921e46 src/HOL/Enum.thy --- a/src/HOL/Enum.thy Tue Sep 16 18:42:33 2014 +0200 +++ b/src/HOL/Enum.thy Tue Sep 16 19:23:37 2014 +0200 @@ -493,7 +493,8 @@ text {* We define small finite types for use in Quickcheck *} -datatype (plugins only: code "quickcheck*") finite_1 = a\<^sub>1 +datatype (plugins only: code "quickcheck*" extraction) finite_1 = + a\<^sub>1 notation (output) a\<^sub>1 ("a\<^sub>1") @@ -595,7 +596,8 @@ declare [[simproc del: finite_1_eq]] hide_const (open) a\<^sub>1 -datatype (plugins only: code "quickcheck*") finite_2 = a\<^sub>1 | a\<^sub>2 +datatype (plugins only: code "quickcheck*" extraction) finite_2 = + a\<^sub>1 | a\<^sub>2 notation (output) a\<^sub>1 ("a\<^sub>1") notation (output) a\<^sub>2 ("a\<^sub>2") @@ -701,7 +703,8 @@ hide_const (open) a\<^sub>1 a\<^sub>2 -datatype (plugins only: code "quickcheck*") finite_3 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 +datatype (plugins only: code "quickcheck*" extraction) finite_3 = + a\<^sub>1 | a\<^sub>2 | a\<^sub>3 notation (output) a\<^sub>1 ("a\<^sub>1") notation (output) a\<^sub>2 ("a\<^sub>2") @@ -825,7 +828,8 @@ hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3 -datatype (plugins only: code "quickcheck*") finite_4 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4 +datatype (plugins only: code "quickcheck*" extraction) finite_4 = + a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4 notation (output) a\<^sub>1 ("a\<^sub>1") notation (output) a\<^sub>2 ("a\<^sub>2") @@ -926,7 +930,8 @@ hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3 a\<^sub>4 -datatype (plugins only: code "quickcheck*") finite_5 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4 | a\<^sub>5 +datatype (plugins only: code "quickcheck*" extraction) finite_5 = + a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4 | a\<^sub>5 notation (output) a\<^sub>1 ("a\<^sub>1") notation (output) a\<^sub>2 ("a\<^sub>2") diff -r 107341a15946 -r 919149921e46 src/HOL/Extraction.thy --- a/src/HOL/Extraction.thy Tue Sep 16 18:42:33 2014 +0200 +++ b/src/HOL/Extraction.thy Tue Sep 16 19:23:37 2014 +0200 @@ -37,7 +37,7 @@ induct_forall_def induct_implies_def induct_equal_def induct_conj_def induct_true_def induct_false_def -datatype (plugins only: code) sumbool = Left | Right +datatype (plugins only: code extraction) sumbool = Left | Right subsection {* Type of extracted program *} diff -r 107341a15946 -r 919149921e46 src/HOL/Lazy_Sequence.thy --- a/src/HOL/Lazy_Sequence.thy Tue Sep 16 18:42:33 2014 +0200 +++ b/src/HOL/Lazy_Sequence.thy Tue Sep 16 19:23:37 2014 +0200 @@ -8,7 +8,8 @@ subsection {* Type of lazy sequences *} -datatype (plugins only: code) (dead 'a) lazy_sequence = lazy_sequence_of_list "'a list" +datatype (plugins only: code extraction) (dead 'a) lazy_sequence = + lazy_sequence_of_list "'a list" primrec list_of_lazy_sequence :: "'a lazy_sequence \ 'a list" where diff -r 107341a15946 -r 919149921e46 src/HOL/Nitpick.thy --- a/src/HOL/Nitpick.thy Tue Sep 16 18:42:33 2014 +0200 +++ b/src/HOL/Nitpick.thy Tue Sep 16 19:23:37 2014 +0200 @@ -14,9 +14,9 @@ "nitpick_params" :: thy_decl begin -datatype (plugins only:) (dead 'a, dead 'b) fun_box = FunBox "'a \ 'b" -datatype (plugins only:) (dead 'a, dead 'b) pair_box = PairBox 'a 'b -datatype (plugins only:) (dead 'a) word = Word "'a set" +datatype (plugins only: extraction) (dead 'a, dead 'b) fun_box = FunBox "'a \ 'b" +datatype (plugins only: extraction) (dead 'a, dead 'b) pair_box = PairBox 'a 'b +datatype (plugins only: extraction) (dead 'a) word = Word "'a set" typedecl bisim_iterator typedecl unsigned_bit diff -r 107341a15946 -r 919149921e46 src/HOL/Predicate.thy --- a/src/HOL/Predicate.thy Tue Sep 16 18:42:33 2014 +0200 +++ b/src/HOL/Predicate.thy Tue Sep 16 19:23:37 2014 +0200 @@ -10,7 +10,7 @@ subsection {* The type of predicate enumerations (a monad) *} -datatype (plugins only: code) (dead 'a) pred = Pred "'a \ bool" +datatype (plugins only: code extraction) (dead 'a) pred = Pred "'a \ bool" primrec eval :: "'a pred \ 'a \ bool" where eval_pred: "eval (Pred f) = f" @@ -402,7 +402,7 @@ subsection {* Implementation *} -datatype (plugins only: code) (dead 'a) seq = +datatype (plugins only: code extraction) (dead 'a) seq = Empty | Insert "'a" "'a pred" | Join "'a pred" "'a seq" diff -r 107341a15946 -r 919149921e46 src/HOL/Quickcheck_Exhaustive.thy --- a/src/HOL/Quickcheck_Exhaustive.thy Tue Sep 16 18:42:33 2014 +0200 +++ b/src/HOL/Quickcheck_Exhaustive.thy Tue Sep 16 19:23:37 2014 +0200 @@ -574,8 +574,11 @@ where "pos_bound_cps_if b = (if b then pos_bound_cps_single () else pos_bound_cps_empty)" -datatype (plugins only: code) (dead 'a) unknown = Unknown | Known 'a -datatype (plugins only: code) (dead 'a) three_valued = Unknown_value | Value 'a | No_value +datatype (plugins only: code extraction) (dead 'a) unknown = + Unknown | Known 'a + +datatype (plugins only: code extraction) (dead 'a) three_valued = + Unknown_value | Value 'a | No_value type_synonym 'a neg_bound_cps = "('a unknown => term list three_valued) => natural => term list three_valued" diff -r 107341a15946 -r 919149921e46 src/HOL/Quickcheck_Narrowing.thy --- a/src/HOL/Quickcheck_Narrowing.thy Tue Sep 16 18:42:33 2014 +0200 +++ b/src/HOL/Quickcheck_Narrowing.thy Tue Sep 16 19:23:37 2014 +0200 @@ -26,14 +26,14 @@ subsubsection {* Narrowing's deep representation of types and terms *} -datatype (plugins only: code) narrowing_type = +datatype (plugins only: code extraction) narrowing_type = Narrowing_sum_of_products "narrowing_type list list" -datatype (plugins only: code) narrowing_term = +datatype (plugins only: code extraction) narrowing_term = Narrowing_variable "integer list" narrowing_type | Narrowing_constructor integer "narrowing_term list" -datatype (plugins only: code) (dead 'a) narrowing_cons = +datatype (plugins only: code extraction) (dead 'a) narrowing_cons = Narrowing_cons narrowing_type "(narrowing_term list \ 'a) list" primrec map_cons :: "('a => 'b) => 'a narrowing_cons => 'b narrowing_cons" @@ -127,7 +127,7 @@ class narrowing = fixes narrowing :: "integer => 'a narrowing_cons" -datatype (plugins only: code) property = +datatype (plugins only: code extraction) property = Universal narrowing_type "(narrowing_term => property)" "narrowing_term => Code_Evaluation.term" | Existential narrowing_type "(narrowing_term => property)" "narrowing_term => Code_Evaluation.term" | Property bool @@ -158,7 +158,7 @@ subsubsection {* Defining a simple datatype to represent functions in an incomplete and redundant way *} -datatype (plugins only: code quickcheck_narrowing) (dead 'a, dead 'b) ffun = +datatype (plugins only: code quickcheck_narrowing extraction) (dead 'a, dead 'b) ffun = Constant 'b | Update 'a 'b "('a, 'b) ffun" @@ -170,7 +170,7 @@ hide_type (open) ffun hide_const (open) Constant Update eval_ffun -datatype (plugins only: code quickcheck_narrowing) (dead 'b) cfun = Constant 'b +datatype (plugins only: code quickcheck_narrowing extraction) (dead 'b) cfun = Constant 'b primrec eval_cfun :: "'b cfun => 'a => 'b" where