--- a/NEWS Sun Nov 15 07:17:05 2020 +0000
+++ b/NEWS Sun Nov 15 07:17:06 2020 +0000
@@ -179,6 +179,9 @@
* Syntax for state monad combinators fcomp and scomp is organized in
bundle state_combinator_syntax. Minor INCOMPATIBILITY.
+* Syntax for reflected term syntax is organized in bundle term_syntax,
+discontinuing previous locale term_syntax. Minor INCOMPATIBILITY.
+
*** FOL ***
--- a/src/HOL/Code_Evaluation.thy Sun Nov 15 07:17:05 2020 +0000
+++ b/src/HOL/Code_Evaluation.thy Sun Nov 15 07:17:06 2020 +0000
@@ -52,7 +52,7 @@
abbreviation valtermify :: "'a \<Rightarrow> 'a \<times> (unit \<Rightarrow> term)" where
"valtermify x \<equiv> (x, \<lambda>u. termify x)"
-locale term_syntax
+bundle term_syntax
begin
notation App (infixl "<\<cdot>>" 70)
@@ -60,11 +60,6 @@
end
-interpretation term_syntax .
-
-no_notation App (infixl "<\<cdot>>" 70)
- and valapp (infixl "{\<cdot>}" 70)
-
subsection \<open>Tools setup and evaluation\<close>
--- a/src/HOL/Library/DAList.thy Sun Nov 15 07:17:05 2020 +0000
+++ b/src/HOL/Library/DAList.thy Sun Nov 15 07:17:06 2020 +0000
@@ -128,21 +128,21 @@
subsection \<open>Quickcheck generators\<close>
-definition (in term_syntax)
+context
+ includes state_combinator_syntax term_syntax
+begin
+
+definition
valterm_empty :: "('key :: typerep, 'value :: typerep) alist \<times> (unit \<Rightarrow> Code_Evaluation.term)"
where "valterm_empty = Code_Evaluation.valtermify empty"
-definition (in term_syntax)
+definition
valterm_update :: "'key :: typerep \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow>
'value :: typerep \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow>
('key, 'value) alist \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow>
('key, 'value) alist \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
[code_unfold]: "valterm_update k v a = Code_Evaluation.valtermify update {\<cdot>} k {\<cdot>} v {\<cdot>}a"
-context
- includes state_combinator_syntax
-begin
-
fun random_aux_alist
where
"random_aux_alist i j =
--- a/src/HOL/Library/FSet.thy Sun Nov 15 07:17:05 2020 +0000
+++ b/src/HOL/Library/FSet.thy Sun Nov 15 07:17:06 2020 +0000
@@ -1314,12 +1314,18 @@
notation Quickcheck_Exhaustive.orelse (infixr "orelse" 55)
-definition (in term_syntax) [code_unfold]:
+context
+ includes term_syntax
+begin
+
+definition [code_unfold]:
"valterm_femptyset = Code_Evaluation.valtermify ({||} :: ('a :: typerep) fset)"
-definition (in term_syntax) [code_unfold]:
+definition [code_unfold]:
"valtermify_finsert x s = Code_Evaluation.valtermify finsert {\<cdot>} (x :: ('a :: typerep * _)) {\<cdot>} s"
+end
+
instantiation fset :: (exhaustive) exhaustive
begin
--- a/src/HOL/Library/Float.thy Sun Nov 15 07:17:05 2020 +0000
+++ b/src/HOL/Library/Float.thy Sun Nov 15 07:17:06 2020 +0000
@@ -318,9 +318,15 @@
end
-definition (in term_syntax) [code_unfold]:
+context
+ includes term_syntax
+begin
+
+definition [code_unfold]:
"valtermify_float x y = Code_Evaluation.valtermify Float {\<cdot>} x {\<cdot>} y"
+end
+
instantiation float :: full_exhaustive
begin
--- a/src/HOL/Library/IArray.thy Sun Nov 15 07:17:05 2020 +0000
+++ b/src/HOL/Library/IArray.thy Sun Nov 15 07:17:06 2020 +0000
@@ -89,7 +89,8 @@
"IArray.all p = Not \<circ> IArray.exists (Not \<circ> p)"
by (simp add: fun_eq_iff)
-context term_syntax
+context
+ includes term_syntax
begin
lemma [code]:
--- a/src/HOL/Library/Interval.thy Sun Nov 15 07:17:05 2020 +0000
+++ b/src/HOL/Library/Interval.thy Sun Nov 15 07:17:06 2020 +0000
@@ -816,9 +816,15 @@
end
-definition (in term_syntax) [code_unfold]:
+context
+ includes term_syntax
+begin
+
+definition [code_unfold]:
"valtermify_interval x y = Code_Evaluation.valtermify (Ivl::'a::{preorder,typerep}\<Rightarrow>_) {\<cdot>} x {\<cdot>} y"
+end
+
instantiation interval :: ("{full_exhaustive,preorder,typerep}") full_exhaustive
begin
--- a/src/HOL/Library/Multiset.thy Sun Nov 15 07:17:05 2020 +0000
+++ b/src/HOL/Library/Multiset.thy Sun Nov 15 07:17:06 2020 +0000
@@ -3534,11 +3534,17 @@
text \<open>Quickcheck generators\<close>
-definition (in term_syntax)
+context
+ includes term_syntax
+begin
+
+definition
msetify :: "'a::typerep list \<times> (unit \<Rightarrow> Code_Evaluation.term)
\<Rightarrow> 'a multiset \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
[code_unfold]: "msetify xs = Code_Evaluation.valtermify mset {\<cdot>} xs"
+end
+
instantiation multiset :: (random) random
begin
--- a/src/HOL/Probability/PMF_Impl.thy Sun Nov 15 07:17:05 2020 +0000
+++ b/src/HOL/Probability/PMF_Impl.thy Sun Nov 15 07:17:06 2020 +0000
@@ -530,22 +530,22 @@
definition single :: "'a \<Rightarrow> 'a multiset" where
"single s = {#s#}"
-definition (in term_syntax)
- pmfify :: "('a::typerep multiset \<times> (unit \<Rightarrow> Code_Evaluation.term)) \<Rightarrow>
- 'a \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow>
- 'a pmf \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
+instantiation pmf :: (random) random
+begin
+
+context
+ includes state_combinator_syntax term_syntax
+begin
+
+definition
+ pmfify :: "('b::typerep multiset \<times> (unit \<Rightarrow> Code_Evaluation.term)) \<Rightarrow>
+ 'b \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow>
+ 'b pmf \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
[code_unfold]: "pmfify A x =
Code_Evaluation.valtermify pmf_of_multiset {\<cdot>}
(Code_Evaluation.valtermify (+) {\<cdot>} A {\<cdot>}
(Code_Evaluation.valtermify single {\<cdot>} x))"
-instantiation pmf :: (random) random
-begin
-
-context
- includes state_combinator_syntax
-begin
-
definition
"Quickcheck_Random.random i =
Quickcheck_Random.random i \<circ>\<rightarrow> (\<lambda>A.
--- a/src/HOL/Quickcheck_Exhaustive.thy Sun Nov 15 07:17:05 2020 +0000
+++ b/src/HOL/Quickcheck_Exhaustive.thy Sun Nov 15 07:17:06 2020 +0000
@@ -180,10 +180,16 @@
end
-definition (in term_syntax)
+context
+ includes term_syntax
+begin
+
+definition
[code_unfold]: "valtermify_pair x y =
Code_Evaluation.valtermify (Pair :: 'a::typerep \<Rightarrow> 'b::typerep \<Rightarrow> 'a \<times> 'b) {\<cdot>} x {\<cdot>} y"
+end
+
instantiation prod :: (full_exhaustive, full_exhaustive) full_exhaustive
begin
@@ -253,11 +259,17 @@
(\<lambda>_::'a. v,
\<lambda>u::unit. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a::typerep)) (t ())))"
-definition (in term_syntax)
+context
+ includes term_syntax
+begin
+
+definition
[code_unfold]: "valtermify_fun_upd g a b =
Code_Evaluation.valtermify
(fun_upd :: ('a::typerep \<Rightarrow> 'b::typerep) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b) {\<cdot>} g {\<cdot>} a {\<cdot>} b"
+end
+
instantiation "fun" :: ("{equal,full_exhaustive}", full_exhaustive) full_exhaustive
begin
@@ -296,11 +308,17 @@
else check_all (\<lambda>(x, xt).
check_all_n_lists (\<lambda>(xs, xst). f ((x # xs), (\<lambda>_. (xt () # xst ())))) (n - 1)))"
-definition (in term_syntax)
+context
+ includes term_syntax
+begin
+
+definition
[code_unfold]: "termify_fun_upd g a b =
(Code_Evaluation.termify
(fun_upd :: ('a::typerep \<Rightarrow> 'b::typerep) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b) <\<cdot>> g <\<cdot>> a <\<cdot>> b)"
+end
+
definition mk_map_term ::
"(unit \<Rightarrow> typerep) \<Rightarrow> (unit \<Rightarrow> typerep) \<Rightarrow>
(unit \<Rightarrow> term list) \<Rightarrow> (unit \<Rightarrow> term list) \<Rightarrow> unit \<Rightarrow> term"
@@ -357,7 +375,11 @@
end
-fun (in term_syntax) check_all_subsets ::
+context
+ includes term_syntax
+begin
+
+fun check_all_subsets ::
"(('a::typerep) set \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow>
('a \<times> (unit \<Rightarrow> term)) list \<Rightarrow> (bool \<times> term list) option"
where
@@ -365,18 +387,19 @@
| "check_all_subsets f (x # xs) =
check_all_subsets (\<lambda>s. case f s of Some ts \<Rightarrow> Some ts | None \<Rightarrow> f (valtermify_insert x s)) xs"
-
-definition (in term_syntax)
+definition
[code_unfold]: "term_emptyset = Code_Evaluation.termify ({} :: ('a::typerep) set)"
-definition (in term_syntax)
+definition
[code_unfold]: "termify_insert x s =
Code_Evaluation.termify (insert :: ('a::typerep) \<Rightarrow> 'a set \<Rightarrow> 'a set) <\<cdot>> x <\<cdot>> s"
-definition (in term_syntax) setify :: "('a::typerep) itself \<Rightarrow> term list \<Rightarrow> term"
+definition setify :: "('a::typerep) itself \<Rightarrow> term list \<Rightarrow> term"
where
"setify T ts = foldr (termify_insert T) ts (term_emptyset T)"
+end
+
instantiation set :: (check_all) check_all
begin
@@ -423,10 +446,16 @@
end
-definition (in term_syntax) [code_unfold]:
+context
+ includes term_syntax
+begin
+
+definition [code_unfold]:
"termify_pair x y =
Code_Evaluation.termify (Pair :: 'a::typerep \<Rightarrow> 'b :: typerep \<Rightarrow> 'a * 'b) <\<cdot>> x <\<cdot>> y"
+end
+
instantiation prod :: (check_all, check_all) check_all
begin
@@ -442,14 +471,20 @@
end
-definition (in term_syntax)
+context
+ includes term_syntax
+begin
+
+definition
[code_unfold]: "valtermify_Inl x =
Code_Evaluation.valtermify (Inl :: 'a::typerep \<Rightarrow> 'a + 'b :: typerep) {\<cdot>} x"
-definition (in term_syntax)
+definition
[code_unfold]: "valtermify_Inr x =
Code_Evaluation.valtermify (Inr :: 'b::typerep \<Rightarrow> 'a::typerep + 'b) {\<cdot>} x"
+end
+
instantiation sum :: (check_all, check_all) check_all
begin
--- a/src/HOL/Quickcheck_Random.thy Sun Nov 15 07:17:05 2020 +0000
+++ b/src/HOL/Quickcheck_Random.thy Sun Nov 15 07:17:06 2020 +0000
@@ -201,13 +201,18 @@
lemma beyond_zero: "beyond k 0 = 0"
by (simp add: beyond_def)
+context
+ includes term_syntax
+begin
-definition (in term_syntax) [code_unfold]:
+definition [code_unfold]:
"valterm_emptyset = Code_Evaluation.valtermify ({} :: ('a :: typerep) set)"
-definition (in term_syntax) [code_unfold]:
+definition [code_unfold]:
"valtermify_insert x s = Code_Evaluation.valtermify insert {\<cdot>} (x :: ('a :: typerep * _)) {\<cdot>} s"
+end
+
instantiation set :: (random) random
begin
--- a/src/HOL/Rat.thy Sun Nov 15 07:17:05 2020 +0000
+++ b/src/HOL/Rat.thy Sun Nov 15 07:17:06 2020 +0000
@@ -998,12 +998,18 @@
text \<open>Quickcheck\<close>
-definition (in term_syntax)
+context
+ includes term_syntax
+begin
+
+definition
valterm_fract :: "int \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow>
int \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow>
rat \<times> (unit \<Rightarrow> Code_Evaluation.term)"
where [code_unfold]: "valterm_fract k l = Code_Evaluation.valtermify Fract {\<cdot>} k {\<cdot>} l"
+end
+
instantiation rat :: random
begin
--- a/src/HOL/Real.thy Sun Nov 15 07:17:05 2020 +0000
+++ b/src/HOL/Real.thy Sun Nov 15 07:17:06 2020 +0000
@@ -1634,10 +1634,16 @@
text \<open>Quickcheck\<close>
-definition (in term_syntax)
+context
+ includes term_syntax
+begin
+
+definition
valterm_ratreal :: "rat \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> real \<times> (unit \<Rightarrow> Code_Evaluation.term)"
where [code_unfold]: "valterm_ratreal k = Code_Evaluation.valtermify Ratreal {\<cdot>} k"
+end
+
instantiation real :: random
begin