# HG changeset patch # User blanchet # Date 1410728370 -7200 # Node ID 7553a1bcecb7df2fa48ed4db8db34dcc2dcfa184 # Parent ec949d7206bbc6b411626b4bf0a2cda0e3ff2637 disable datatype 'plugins' for internal types diff -r ec949d7206bb -r 7553a1bcecb7 src/HOL/Code_Evaluation.thy --- a/src/HOL/Code_Evaluation.thy Sat Sep 13 18:08:45 2014 +0200 +++ b/src/HOL/Code_Evaluation.thy Sun Sep 14 22:59:30 2014 +0200 @@ -13,7 +13,7 @@ subsubsection {* Terms and class @{text term_of} *} -datatype "term" = dummy_term +datatype (plugins only: code) "term" = dummy_term definition Const :: "String.literal \ typerep \ term" where "Const _ _ = dummy_term" @@ -113,7 +113,7 @@ end -declare [[code drop: rec_term case_term size_term "size :: term \ _" "HOL.equal :: term \ _" +declare [[code drop: rec_term case_term "HOL.equal :: term \ _" "term_of :: typerep \ _" "term_of :: term \ _" "term_of :: String.literal \ _" "term_of :: _ Predicate.pred \ term" "term_of :: _ Predicate.seq \ term"]] diff -r ec949d7206bb -r 7553a1bcecb7 src/HOL/Enum.thy --- a/src/HOL/Enum.thy Sat Sep 13 18:08:45 2014 +0200 +++ b/src/HOL/Enum.thy Sun Sep 14 22:59:30 2014 +0200 @@ -491,9 +491,9 @@ subsection {* Small finite types *} -text {* We define small finite types for the use in Quickcheck *} +text {* We define small finite types for use in Quickcheck *} -datatype finite_1 = a\<^sub>1 +datatype (plugins only: code "quickcheck*") finite_1 = a\<^sub>1 notation (output) a\<^sub>1 ("a\<^sub>1") @@ -595,7 +595,7 @@ declare [[simproc del: finite_1_eq]] hide_const (open) a\<^sub>1 -datatype finite_2 = a\<^sub>1 | a\<^sub>2 +datatype (plugins only: code "quickcheck*") 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 +701,7 @@ hide_const (open) a\<^sub>1 a\<^sub>2 -datatype finite_3 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 +datatype (plugins only: code "quickcheck*") 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 +825,7 @@ hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3 -datatype finite_4 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4 +datatype (plugins only: code "quickcheck*") 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,8 +926,7 @@ hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3 a\<^sub>4 - -datatype finite_5 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4 | a\<^sub>5 +datatype (plugins only: code "quickcheck*") 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 ec949d7206bb -r 7553a1bcecb7 src/HOL/Extraction.thy --- a/src/HOL/Extraction.thy Sat Sep 13 18:08:45 2014 +0200 +++ b/src/HOL/Extraction.thy Sun Sep 14 22:59:30 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 sumbool = Left | Right +datatype (plugins only: code) sumbool = Left | Right subsection {* Type of extracted program *} diff -r ec949d7206bb -r 7553a1bcecb7 src/HOL/Lazy_Sequence.thy --- a/src/HOL/Lazy_Sequence.thy Sat Sep 13 18:08:45 2014 +0200 +++ b/src/HOL/Lazy_Sequence.thy Sun Sep 14 22:59:30 2014 +0200 @@ -1,4 +1,3 @@ - (* Author: Lukas Bulwahn, TU Muenchen *) header {* Lazy sequences *} @@ -9,7 +8,7 @@ subsection {* Type of lazy sequences *} -datatype (dead 'a) lazy_sequence = lazy_sequence_of_list "'a list" +datatype (plugins only: code) (dead 'a) lazy_sequence = lazy_sequence_of_list "'a list" primrec list_of_lazy_sequence :: "'a lazy_sequence \ 'a list" where @@ -27,11 +26,6 @@ "xq = yq \ list_of_lazy_sequence xq = list_of_lazy_sequence yq" by (auto intro: lazy_sequence_eqI) -lemma size_lazy_sequence_eq [code]: - "size_lazy_sequence f xq = Suc (size_list f (list_of_lazy_sequence xq))" - "size xq = Suc (length (list_of_lazy_sequence xq))" - by (cases xq, simp)+ - lemma case_lazy_sequence [simp]: "case_lazy_sequence f xq = f (list_of_lazy_sequence xq)" by (cases xq) auto @@ -72,12 +66,6 @@ case_list g (\x. curry h x \ lazy_sequence_of_list) (list_of_lazy_sequence xq)" by (cases "list_of_lazy_sequence xq") (simp_all add: yield_def) -lemma size_lazy_sequence_code [code]: - "size_lazy_sequence s xq = (case yield xq of - None \ 1 - | Some (x, xq') \ Suc (s x + size_lazy_sequence s xq'))" - by (cases "list_of_lazy_sequence xq") (simp_all add: size_lazy_sequence_eq) - lemma equal_lazy_sequence_code [code]: "HOL.equal xq yq = (case (yield xq, yield yq) of (None, None) \ True diff -r ec949d7206bb -r 7553a1bcecb7 src/HOL/Nitpick.thy --- a/src/HOL/Nitpick.thy Sat Sep 13 18:08:45 2014 +0200 +++ b/src/HOL/Nitpick.thy Sun Sep 14 22:59:30 2014 +0200 @@ -14,9 +14,9 @@ "nitpick_params" :: thy_decl begin -datatype (dead 'a, dead 'b) fun_box = FunBox "'a \ 'b" -datatype (dead 'a, dead 'b) pair_box = PairBox 'a 'b -datatype (dead 'a) word = Word "'a set" +datatype (plugins only: code) (dead 'a, dead 'b) fun_box = FunBox "'a \ 'b" +datatype (plugins only: code) (dead 'a, dead 'b) pair_box = PairBox 'a 'b +datatype (plugins only: code) (dead 'a) word = Word "'a set" typedecl bisim_iterator typedecl unsigned_bit diff -r ec949d7206bb -r 7553a1bcecb7 src/HOL/Predicate.thy --- a/src/HOL/Predicate.thy Sat Sep 13 18:08:45 2014 +0200 +++ b/src/HOL/Predicate.thy Sun Sep 14 22:59:30 2014 +0200 @@ -10,7 +10,7 @@ subsection {* The type of predicate enumerations (a monad) *} -datatype 'a pred = Pred "'a \ bool" +datatype (plugins only: code) (dead 'a) pred = Pred "'a \ bool" primrec eval :: "'a pred \ 'a \ bool" where eval_pred: "eval (Pred f) = f" @@ -402,7 +402,10 @@ subsection {* Implementation *} -datatype 'a seq = Empty | Insert "'a" "'a pred" | Join "'a pred" "'a seq" +datatype (plugins only: code) (dead 'a) seq = + Empty +| Insert "'a" "'a pred" +| Join "'a pred" "'a seq" primrec pred_of_seq :: "'a seq \ 'a pred" where "pred_of_seq Empty = \" @@ -494,12 +497,6 @@ by (simp add: adjunct_sup sup_assoc sup_commute sup_left_commute) qed -lemma [code]: - "size (P :: 'a Predicate.pred) = 0" by (cases P) simp - -lemma [code]: - "size_pred f P = 0" by (cases P) simp - primrec contained :: "'a seq \ 'a pred \ bool" where "contained Empty Q \ True" | "contained (Insert x P) Q \ eval Q x \ P \ Q" diff -r ec949d7206bb -r 7553a1bcecb7 src/HOL/Quickcheck_Exhaustive.thy --- a/src/HOL/Quickcheck_Exhaustive.thy Sat Sep 13 18:08:45 2014 +0200 +++ b/src/HOL/Quickcheck_Exhaustive.thy Sun Sep 14 22:59:30 2014 +0200 @@ -574,8 +574,8 @@ where "pos_bound_cps_if b = (if b then pos_bound_cps_single () else pos_bound_cps_empty)" -datatype (dead 'a) unknown = Unknown | Known 'a -datatype (dead 'a) three_valued = Unknown_value | Value 'a | No_value +datatype (plugins only: code) (dead 'a) unknown = Unknown | Known 'a +datatype (plugins only: code) (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 ec949d7206bb -r 7553a1bcecb7 src/HOL/Quickcheck_Narrowing.thy --- a/src/HOL/Quickcheck_Narrowing.thy Sat Sep 13 18:08:45 2014 +0200 +++ b/src/HOL/Quickcheck_Narrowing.thy Sun Sep 14 22:59:30 2014 +0200 @@ -26,14 +26,14 @@ subsubsection {* Narrowing's deep representation of types and terms *} -datatype narrowing_type = +datatype (plugins only: code) narrowing_type = Narrowing_sum_of_products "narrowing_type list list" -datatype narrowing_term = +datatype (plugins only: code) narrowing_term = Narrowing_variable "integer list" narrowing_type | Narrowing_constructor integer "narrowing_term list" -datatype (dead 'a) narrowing_cons = +datatype (plugins only: code) (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,10 @@ class narrowing = fixes narrowing :: "integer => 'a narrowing_cons" -datatype 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 +datatype (plugins only: code) 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 (* FIXME: hard-wired maximal depth of 100 here *) definition exists :: "('a :: {narrowing, partial_term_of} => property) => property" @@ -155,7 +158,9 @@ subsubsection {* Defining a simple datatype to represent functions in an incomplete and redundant way *} -datatype (dead 'a, dead 'b) ffun = Constant 'b | Update 'a 'b "('a, 'b) ffun" +datatype (plugins only: code quickcheck_narrowing) (dead 'a, dead 'b) ffun = + Constant 'b +| Update 'a 'b "('a, 'b) ffun" primrec eval_ffun :: "('a, 'b) ffun => 'a => 'b" where @@ -165,7 +170,7 @@ hide_type (open) ffun hide_const (open) Constant Update eval_ffun -datatype (dead 'b) cfun = Constant 'b +datatype (plugins only: code quickcheck_narrowing) (dead 'b) cfun = Constant 'b primrec eval_cfun :: "'b cfun => 'a => 'b" where