added 'extraction' plugins -- this might help 'HOL-Proofs'
authorblanchet
Tue Sep 16 19:23:37 2014 +0200 (2014-09-16)
changeset 58350919149921e46
parent 58349 107341a15946
child 58351 b3f7c69e9fcd
added 'extraction' plugins -- this might help 'HOL-Proofs'
src/HOL/Code_Evaluation.thy
src/HOL/Enum.thy
src/HOL/Extraction.thy
src/HOL/Lazy_Sequence.thy
src/HOL/Nitpick.thy
src/HOL/Predicate.thy
src/HOL/Quickcheck_Exhaustive.thy
src/HOL/Quickcheck_Narrowing.thy
     1.1 --- a/src/HOL/Code_Evaluation.thy	Tue Sep 16 18:42:33 2014 +0200
     1.2 +++ b/src/HOL/Code_Evaluation.thy	Tue Sep 16 19:23:37 2014 +0200
     1.3 @@ -13,7 +13,7 @@
     1.4  
     1.5  subsubsection {* Terms and class @{text term_of} *}
     1.6  
     1.7 -datatype (plugins only: code) "term" = dummy_term
     1.8 +datatype (plugins only: code extraction) "term" = dummy_term
     1.9  
    1.10  definition Const :: "String.literal \<Rightarrow> typerep \<Rightarrow> term" where
    1.11    "Const _ _ = dummy_term"
     2.1 --- a/src/HOL/Enum.thy	Tue Sep 16 18:42:33 2014 +0200
     2.2 +++ b/src/HOL/Enum.thy	Tue Sep 16 19:23:37 2014 +0200
     2.3 @@ -493,7 +493,8 @@
     2.4  
     2.5  text {* We define small finite types for use in Quickcheck *}
     2.6  
     2.7 -datatype (plugins only: code "quickcheck*") finite_1 = a\<^sub>1
     2.8 +datatype (plugins only: code "quickcheck*" extraction) finite_1 =
     2.9 +  a\<^sub>1
    2.10  
    2.11  notation (output) a\<^sub>1  ("a\<^sub>1")
    2.12  
    2.13 @@ -595,7 +596,8 @@
    2.14  declare [[simproc del: finite_1_eq]]
    2.15  hide_const (open) a\<^sub>1
    2.16  
    2.17 -datatype (plugins only: code "quickcheck*") finite_2 = a\<^sub>1 | a\<^sub>2
    2.18 +datatype (plugins only: code "quickcheck*" extraction) finite_2 =
    2.19 +  a\<^sub>1 | a\<^sub>2
    2.20  
    2.21  notation (output) a\<^sub>1  ("a\<^sub>1")
    2.22  notation (output) a\<^sub>2  ("a\<^sub>2")
    2.23 @@ -701,7 +703,8 @@
    2.24  
    2.25  hide_const (open) a\<^sub>1 a\<^sub>2
    2.26  
    2.27 -datatype (plugins only: code "quickcheck*") finite_3 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3
    2.28 +datatype (plugins only: code "quickcheck*" extraction) finite_3 =
    2.29 +  a\<^sub>1 | a\<^sub>2 | a\<^sub>3
    2.30  
    2.31  notation (output) a\<^sub>1  ("a\<^sub>1")
    2.32  notation (output) a\<^sub>2  ("a\<^sub>2")
    2.33 @@ -825,7 +828,8 @@
    2.34  
    2.35  hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3
    2.36  
    2.37 -datatype (plugins only: code "quickcheck*") finite_4 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4
    2.38 +datatype (plugins only: code "quickcheck*" extraction) finite_4 =
    2.39 +  a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4
    2.40  
    2.41  notation (output) a\<^sub>1  ("a\<^sub>1")
    2.42  notation (output) a\<^sub>2  ("a\<^sub>2")
    2.43 @@ -926,7 +930,8 @@
    2.44  
    2.45  hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3 a\<^sub>4
    2.46  
    2.47 -datatype (plugins only: code "quickcheck*") finite_5 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4 | a\<^sub>5
    2.48 +datatype (plugins only: code "quickcheck*" extraction) finite_5 =
    2.49 +  a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4 | a\<^sub>5
    2.50  
    2.51  notation (output) a\<^sub>1  ("a\<^sub>1")
    2.52  notation (output) a\<^sub>2  ("a\<^sub>2")
     3.1 --- a/src/HOL/Extraction.thy	Tue Sep 16 18:42:33 2014 +0200
     3.2 +++ b/src/HOL/Extraction.thy	Tue Sep 16 19:23:37 2014 +0200
     3.3 @@ -37,7 +37,7 @@
     3.4    induct_forall_def induct_implies_def induct_equal_def induct_conj_def
     3.5    induct_true_def induct_false_def
     3.6  
     3.7 -datatype (plugins only: code) sumbool = Left | Right
     3.8 +datatype (plugins only: code extraction) sumbool = Left | Right
     3.9  
    3.10  subsection {* Type of extracted program *}
    3.11  
     4.1 --- a/src/HOL/Lazy_Sequence.thy	Tue Sep 16 18:42:33 2014 +0200
     4.2 +++ b/src/HOL/Lazy_Sequence.thy	Tue Sep 16 19:23:37 2014 +0200
     4.3 @@ -8,7 +8,8 @@
     4.4  
     4.5  subsection {* Type of lazy sequences *}
     4.6  
     4.7 -datatype (plugins only: code) (dead 'a) lazy_sequence = lazy_sequence_of_list "'a list"
     4.8 +datatype (plugins only: code extraction) (dead 'a) lazy_sequence =
     4.9 +  lazy_sequence_of_list "'a list"
    4.10  
    4.11  primrec list_of_lazy_sequence :: "'a lazy_sequence \<Rightarrow> 'a list"
    4.12  where
     5.1 --- a/src/HOL/Nitpick.thy	Tue Sep 16 18:42:33 2014 +0200
     5.2 +++ b/src/HOL/Nitpick.thy	Tue Sep 16 19:23:37 2014 +0200
     5.3 @@ -14,9 +14,9 @@
     5.4    "nitpick_params" :: thy_decl
     5.5  begin
     5.6  
     5.7 -datatype (plugins only:) (dead 'a, dead 'b) fun_box = FunBox "'a \<Rightarrow> 'b"
     5.8 -datatype (plugins only:) (dead 'a, dead 'b) pair_box = PairBox 'a 'b
     5.9 -datatype (plugins only:) (dead 'a) word = Word "'a set"
    5.10 +datatype (plugins only: extraction) (dead 'a, dead 'b) fun_box = FunBox "'a \<Rightarrow> 'b"
    5.11 +datatype (plugins only: extraction) (dead 'a, dead 'b) pair_box = PairBox 'a 'b
    5.12 +datatype (plugins only: extraction) (dead 'a) word = Word "'a set"
    5.13  
    5.14  typedecl bisim_iterator
    5.15  typedecl unsigned_bit
     6.1 --- a/src/HOL/Predicate.thy	Tue Sep 16 18:42:33 2014 +0200
     6.2 +++ b/src/HOL/Predicate.thy	Tue Sep 16 19:23:37 2014 +0200
     6.3 @@ -10,7 +10,7 @@
     6.4  
     6.5  subsection {* The type of predicate enumerations (a monad) *}
     6.6  
     6.7 -datatype (plugins only: code) (dead 'a) pred = Pred "'a \<Rightarrow> bool"
     6.8 +datatype (plugins only: code extraction) (dead 'a) pred = Pred "'a \<Rightarrow> bool"
     6.9  
    6.10  primrec eval :: "'a pred \<Rightarrow> 'a \<Rightarrow> bool" where
    6.11    eval_pred: "eval (Pred f) = f"
    6.12 @@ -402,7 +402,7 @@
    6.13  
    6.14  subsection {* Implementation *}
    6.15  
    6.16 -datatype (plugins only: code) (dead 'a) seq =
    6.17 +datatype (plugins only: code extraction) (dead 'a) seq =
    6.18    Empty
    6.19  | Insert "'a" "'a pred"
    6.20  | Join "'a pred" "'a seq"
     7.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Tue Sep 16 18:42:33 2014 +0200
     7.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Tue Sep 16 19:23:37 2014 +0200
     7.3 @@ -574,8 +574,11 @@
     7.4  where
     7.5    "pos_bound_cps_if b = (if b then pos_bound_cps_single () else pos_bound_cps_empty)"
     7.6  
     7.7 -datatype (plugins only: code) (dead 'a) unknown = Unknown | Known 'a
     7.8 -datatype (plugins only: code) (dead 'a) three_valued = Unknown_value | Value 'a | No_value
     7.9 +datatype (plugins only: code extraction) (dead 'a) unknown =
    7.10 +  Unknown | Known 'a
    7.11 +
    7.12 +datatype (plugins only: code extraction) (dead 'a) three_valued =
    7.13 +  Unknown_value | Value 'a | No_value
    7.14  
    7.15  type_synonym 'a neg_bound_cps = "('a unknown => term list three_valued) => natural => term list three_valued"
    7.16  
     8.1 --- a/src/HOL/Quickcheck_Narrowing.thy	Tue Sep 16 18:42:33 2014 +0200
     8.2 +++ b/src/HOL/Quickcheck_Narrowing.thy	Tue Sep 16 19:23:37 2014 +0200
     8.3 @@ -26,14 +26,14 @@
     8.4  
     8.5  subsubsection {* Narrowing's deep representation of types and terms *}
     8.6  
     8.7 -datatype (plugins only: code) narrowing_type =
     8.8 +datatype (plugins only: code extraction) narrowing_type =
     8.9    Narrowing_sum_of_products "narrowing_type list list"
    8.10  
    8.11 -datatype (plugins only: code) narrowing_term =
    8.12 +datatype (plugins only: code extraction) narrowing_term =
    8.13    Narrowing_variable "integer list" narrowing_type
    8.14  | Narrowing_constructor integer "narrowing_term list"
    8.15  
    8.16 -datatype (plugins only: code) (dead 'a) narrowing_cons =
    8.17 +datatype (plugins only: code extraction) (dead 'a) narrowing_cons =
    8.18    Narrowing_cons narrowing_type "(narrowing_term list \<Rightarrow> 'a) list"
    8.19  
    8.20  primrec map_cons :: "('a => 'b) => 'a narrowing_cons => 'b narrowing_cons"
    8.21 @@ -127,7 +127,7 @@
    8.22  class narrowing =
    8.23    fixes narrowing :: "integer => 'a narrowing_cons"
    8.24  
    8.25 -datatype (plugins only: code) property =
    8.26 +datatype (plugins only: code extraction) property =
    8.27    Universal narrowing_type "(narrowing_term => property)" "narrowing_term => Code_Evaluation.term"
    8.28  | Existential narrowing_type "(narrowing_term => property)" "narrowing_term => Code_Evaluation.term"
    8.29  | Property bool
    8.30 @@ -158,7 +158,7 @@
    8.31  
    8.32  subsubsection {* Defining a simple datatype to represent functions in an incomplete and redundant way *}
    8.33  
    8.34 -datatype (plugins only: code quickcheck_narrowing) (dead 'a, dead 'b) ffun =
    8.35 +datatype (plugins only: code quickcheck_narrowing extraction) (dead 'a, dead 'b) ffun =
    8.36    Constant 'b
    8.37  | Update 'a 'b "('a, 'b) ffun"
    8.38  
    8.39 @@ -170,7 +170,7 @@
    8.40  hide_type (open) ffun
    8.41  hide_const (open) Constant Update eval_ffun
    8.42  
    8.43 -datatype (plugins only: code quickcheck_narrowing) (dead 'b) cfun = Constant 'b
    8.44 +datatype (plugins only: code quickcheck_narrowing extraction) (dead 'b) cfun = Constant 'b
    8.45  
    8.46  primrec eval_cfun :: "'b cfun => 'a => 'b"
    8.47  where