--- a/NEWS Wed Aug 18 12:33:31 2021 +0200
+++ b/NEWS Wed Aug 25 21:43:43 2021 +0200
@@ -9,6 +9,17 @@
*** General ***
+* Configuration option "show_results" controls output of final results
+in commands like 'definition' or 'theorem'. Output is normally enabled
+in interactive mode, but it could occasionally cause unnecessary
+slowdown. It can be disabled like this:
+
+ context notes [[show_results = true]]
+ begin
+ definition "test = True"
+ theorem test by (simp add: test_def)
+ end
+
* Timeouts for Isabelle/ML tools are subject to system option
"timeout_scale" --- this already used for the overall session build
process before, and allows to adapt to slow machines. The underlying
@@ -195,6 +206,10 @@
in classes (semi)ring_bit_operations, class semiring_bit_shifts is
gone.
+* Expressions of the form "NOT (numeral _)" are not simplified by
+default any longer. INCOMPATIBILITY, use not_one_eq and not_numeral_eq
+as simp rule explicitly if needed.
+
* Abbreviation "max_word" has been moved to session Word_Lib in the AFP,
as also have constants "shiftl1", "shiftr1", "sshiftr1", "bshiftr1",
"setBit", "clearBit". See there further the changelog in theory Guide.
--- a/src/HOL/Bit_Operations.thy Wed Aug 18 12:33:31 2021 +0200
+++ b/src/HOL/Bit_Operations.thy Wed Aug 25 21:43:43 2021 +0200
@@ -758,6 +758,10 @@
\<open>a XOR 1 = a + of_bool (even a) - of_bool (odd a)\<close>
using one_xor_eq [of a] by (simp add: ac_simps)
+lemma xor_self_eq [simp]:
+ \<open>a XOR a = 0\<close>
+ by (rule bit_eqI) (simp add: bit_simps)
+
lemma bit_iff_odd_drop_bit:
\<open>bit a n \<longleftrightarrow> odd (drop_bit n a)\<close>
by (simp add: bit_iff_odd drop_bit_eq_div)
@@ -1319,7 +1323,7 @@
\<open>bit (- 2) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> n > 0\<close>
by (simp add: bit_minus_iff bit_1_iff)
-lemma not_one [simp]:
+lemma not_one_eq:
\<open>NOT 1 = - 2\<close>
by (simp add: bit_eq_iff bit_not_iff) (simp add: bit_1_iff)
@@ -1464,7 +1468,7 @@
\<open>NOT k div 2 = NOT (k div 2)\<close> for k :: int
by (cases k) (simp_all add: not_int_def divide_int_def nat_add_distrib)
-lemma bit_not_int_iff [bit_simps]:
+lemma bit_not_int_iff:
\<open>bit (NOT k) n \<longleftrightarrow> \<not> bit k n\<close>
for k :: int
by (simp add: bit_not_int_iff' not_int_def)
@@ -2057,6 +2061,11 @@
else \<bar>k mod 2 - l mod 2\<bar> + 2 * ((k div 2) XOR (l div 2)))\<close> for k l :: int
by (auto simp add: xor_int_rec [of k l] not_int_def elim!: oddE)
+lemma bit_minus_int_iff:
+ \<open>bit (- k) n \<longleftrightarrow> bit (NOT (k - 1)) n\<close>
+ for k :: int
+ by (simp add: bit_simps)
+
subsection \<open>Instance \<^typ>\<open>nat\<close>\<close>
@@ -2215,7 +2224,7 @@
lemma [code]:
\<open>unset_bit 0 m = 2 * (m div 2)\<close>
- \<open>unset_bit (Suc n) m = m mod 2 + 2 * unset_bit n (m div 2)\<close>
+ \<open>unset_bit (Suc n) m = m mod 2 + 2 * unset_bit n (m div 2)\<close> for m n :: nat
by (simp_all add: unset_bit_Suc)
@@ -2308,10 +2317,6 @@
\<open>of_nat (drop_bit m n) = drop_bit m (of_nat n)\<close>
by (simp add: drop_bit_eq_div Bit_Operations.drop_bit_eq_div of_nat_div)
-lemma bit_push_bit_iff_of_nat_iff [bit_simps]:
- \<open>bit (push_bit m (of_nat r)) n \<longleftrightarrow> m \<le> n \<and> bit (of_nat r) (n - m)\<close>
- by (auto simp add: bit_push_bit_iff)
-
lemma take_bit_sum:
"take_bit n a = (\<Sum>k = 0..<n. push_bit k (of_bool (bit a k)))"
for n :: nat
@@ -2338,6 +2343,293 @@
instance int :: unique_euclidean_semiring_with_bit_operations ..
+subsection \<open>Symbolic computations on numeral expressions\<close>
+
+context unique_euclidean_semiring_with_bit_operations
+begin
+
+lemma bit_numeral_iff:
+ \<open>bit (numeral m) n \<longleftrightarrow> bit (numeral m :: nat) n\<close>
+ using bit_of_nat_iff_bit [of \<open>numeral m\<close> n] by simp
+
+lemma bit_numeral_Bit0_Suc_iff [simp]:
+ \<open>bit (numeral (Num.Bit0 m)) (Suc n) \<longleftrightarrow> bit (numeral m) n\<close>
+ by (simp add: bit_Suc numeral_Bit0_div_2)
+
+lemma bit_numeral_Bit1_Suc_iff [simp]:
+ \<open>bit (numeral (Num.Bit1 m)) (Suc n) \<longleftrightarrow> bit (numeral m) n\<close>
+ by (simp add: bit_Suc numeral_Bit1_div_2)
+
+lemma bit_numeral_rec:
+ \<open>bit (numeral (Num.Bit0 w)) n \<longleftrightarrow> (case n of 0 \<Rightarrow> False | Suc m \<Rightarrow> bit (numeral w) m)\<close>
+ \<open>bit (numeral (Num.Bit1 w)) n \<longleftrightarrow> (case n of 0 \<Rightarrow> True | Suc m \<Rightarrow> bit (numeral w) m)\<close>
+ by (cases n; simp)+
+
+lemma bit_numeral_simps [simp]:
+ \<open>\<not> bit 1 (numeral n)\<close>
+ \<open>bit (numeral (Num.Bit0 w)) (numeral n) \<longleftrightarrow> bit (numeral w) (pred_numeral n)\<close>
+ \<open>bit (numeral (Num.Bit1 w)) (numeral n) \<longleftrightarrow> bit (numeral w) (pred_numeral n)\<close>
+ by (simp_all add: bit_1_iff numeral_eq_Suc)
+
+lemma and_numerals [simp]:
+ \<open>1 AND numeral (Num.Bit0 y) = 0\<close>
+ \<open>1 AND numeral (Num.Bit1 y) = 1\<close>
+ \<open>numeral (Num.Bit0 x) AND numeral (Num.Bit0 y) = 2 * (numeral x AND numeral y)\<close>
+ \<open>numeral (Num.Bit0 x) AND numeral (Num.Bit1 y) = 2 * (numeral x AND numeral y)\<close>
+ \<open>numeral (Num.Bit0 x) AND 1 = 0\<close>
+ \<open>numeral (Num.Bit1 x) AND numeral (Num.Bit0 y) = 2 * (numeral x AND numeral y)\<close>
+ \<open>numeral (Num.Bit1 x) AND numeral (Num.Bit1 y) = 1 + 2 * (numeral x AND numeral y)\<close>
+ \<open>numeral (Num.Bit1 x) AND 1 = 1\<close>
+ by (simp_all add: bit_eq_iff) (simp_all add: bit_simps bit_Suc bit_numeral_rec split: nat.splits)
+
+fun and_num :: \<open>num \<Rightarrow> num \<Rightarrow> num option\<close> \<^marker>\<open>contributor \<open>Andreas Lochbihler\<close>\<close>
+where
+ \<open>and_num num.One num.One = Some num.One\<close>
+| \<open>and_num num.One (num.Bit0 n) = None\<close>
+| \<open>and_num num.One (num.Bit1 n) = Some num.One\<close>
+| \<open>and_num (num.Bit0 m) num.One = None\<close>
+| \<open>and_num (num.Bit0 m) (num.Bit0 n) = map_option num.Bit0 (and_num m n)\<close>
+| \<open>and_num (num.Bit0 m) (num.Bit1 n) = map_option num.Bit0 (and_num m n)\<close>
+| \<open>and_num (num.Bit1 m) num.One = Some num.One\<close>
+| \<open>and_num (num.Bit1 m) (num.Bit0 n) = map_option num.Bit0 (and_num m n)\<close>
+| \<open>and_num (num.Bit1 m) (num.Bit1 n) = (case and_num m n of None \<Rightarrow> Some num.One | Some n' \<Rightarrow> Some (num.Bit1 n'))\<close>
+
+lemma numeral_and_num:
+ \<open>numeral m AND numeral n = (case and_num m n of None \<Rightarrow> 0 | Some n' \<Rightarrow> numeral n')\<close>
+ by (induction m n rule: and_num.induct) (simp_all add: split: option.split)
+
+lemma and_num_eq_None_iff:
+ \<open>and_num m n = None \<longleftrightarrow> numeral m AND numeral n = 0\<close>
+ by (simp add: numeral_and_num split: option.split)
+
+lemma and_num_eq_Some_iff:
+ \<open>and_num m n = Some q \<longleftrightarrow> numeral m AND numeral n = numeral q\<close>
+ by (simp add: numeral_and_num split: option.split)
+
+lemma or_numerals [simp]:
+ \<open>1 OR numeral (Num.Bit0 y) = numeral (Num.Bit1 y)\<close>
+ \<open>1 OR numeral (Num.Bit1 y) = numeral (Num.Bit1 y)\<close>
+ \<open>numeral (Num.Bit0 x) OR numeral (Num.Bit0 y) = 2 * (numeral x OR numeral y)\<close>
+ \<open>numeral (Num.Bit0 x) OR numeral (Num.Bit1 y) = 1 + 2 * (numeral x OR numeral y)\<close>
+ \<open>numeral (Num.Bit0 x) OR 1 = numeral (Num.Bit1 x)\<close>
+ \<open>numeral (Num.Bit1 x) OR numeral (Num.Bit0 y) = 1 + 2 * (numeral x OR numeral y)\<close>
+ \<open>numeral (Num.Bit1 x) OR numeral (Num.Bit1 y) = 1 + 2 * (numeral x OR numeral y)\<close>
+ \<open>numeral (Num.Bit1 x) OR 1 = numeral (Num.Bit1 x)\<close>
+ by (simp_all add: bit_eq_iff) (simp_all add: bit_simps bit_Suc bit_numeral_rec split: nat.splits)
+
+fun or_num :: \<open>num \<Rightarrow> num \<Rightarrow> num\<close> \<^marker>\<open>contributor \<open>Andreas Lochbihler\<close>\<close>
+where
+ \<open>or_num num.One num.One = num.One\<close>
+| \<open>or_num num.One (num.Bit0 n) = num.Bit1 n\<close>
+| \<open>or_num num.One (num.Bit1 n) = num.Bit1 n\<close>
+| \<open>or_num (num.Bit0 m) num.One = num.Bit1 m\<close>
+| \<open>or_num (num.Bit0 m) (num.Bit0 n) = num.Bit0 (or_num m n)\<close>
+| \<open>or_num (num.Bit0 m) (num.Bit1 n) = num.Bit1 (or_num m n)\<close>
+| \<open>or_num (num.Bit1 m) num.One = num.Bit1 m\<close>
+| \<open>or_num (num.Bit1 m) (num.Bit0 n) = num.Bit1 (or_num m n)\<close>
+| \<open>or_num (num.Bit1 m) (num.Bit1 n) = num.Bit1 (or_num m n)\<close>
+
+lemma numeral_or_num:
+ \<open>numeral m OR numeral n = numeral (or_num m n)\<close>
+ by (induction m n rule: or_num.induct) simp_all
+
+lemma numeral_or_num_eq:
+ \<open>numeral (or_num m n) = numeral m OR numeral n\<close>
+ by (simp add: numeral_or_num)
+
+lemma xor_numerals [simp]:
+ \<open>1 XOR numeral (Num.Bit0 y) = numeral (Num.Bit1 y)\<close>
+ \<open>1 XOR numeral (Num.Bit1 y) = numeral (Num.Bit0 y)\<close>
+ \<open>numeral (Num.Bit0 x) XOR numeral (Num.Bit0 y) = 2 * (numeral x XOR numeral y)\<close>
+ \<open>numeral (Num.Bit0 x) XOR numeral (Num.Bit1 y) = 1 + 2 * (numeral x XOR numeral y)\<close>
+ \<open>numeral (Num.Bit0 x) XOR 1 = numeral (Num.Bit1 x)\<close>
+ \<open>numeral (Num.Bit1 x) XOR numeral (Num.Bit0 y) = 1 + 2 * (numeral x XOR numeral y)\<close>
+ \<open>numeral (Num.Bit1 x) XOR numeral (Num.Bit1 y) = 2 * (numeral x XOR numeral y)\<close>
+ \<open>numeral (Num.Bit1 x) XOR 1 = numeral (Num.Bit0 x)\<close>
+ by (simp_all add: bit_eq_iff) (simp_all add: bit_simps bit_Suc bit_numeral_rec split: nat.splits)
+
+fun xor_num :: \<open>num \<Rightarrow> num \<Rightarrow> num option\<close> \<^marker>\<open>contributor \<open>Andreas Lochbihler\<close>\<close>
+where
+ \<open>xor_num num.One num.One = None\<close>
+| \<open>xor_num num.One (num.Bit0 n) = Some (num.Bit1 n)\<close>
+| \<open>xor_num num.One (num.Bit1 n) = Some (num.Bit0 n)\<close>
+| \<open>xor_num (num.Bit0 m) num.One = Some (num.Bit1 m)\<close>
+| \<open>xor_num (num.Bit0 m) (num.Bit0 n) = map_option num.Bit0 (xor_num m n)\<close>
+| \<open>xor_num (num.Bit0 m) (num.Bit1 n) = Some (case xor_num m n of None \<Rightarrow> num.One | Some n' \<Rightarrow> num.Bit1 n')\<close>
+| \<open>xor_num (num.Bit1 m) num.One = Some (num.Bit0 m)\<close>
+| \<open>xor_num (num.Bit1 m) (num.Bit0 n) = Some (case xor_num m n of None \<Rightarrow> num.One | Some n' \<Rightarrow> num.Bit1 n')\<close>
+| \<open>xor_num (num.Bit1 m) (num.Bit1 n) = map_option num.Bit0 (xor_num m n)\<close>
+
+lemma numeral_xor_num:
+ \<open>numeral m XOR numeral n = (case xor_num m n of None \<Rightarrow> 0 | Some n' \<Rightarrow> numeral n')\<close>
+ by (induction m n rule: xor_num.induct) (simp_all split: option.split)
+
+lemma xor_num_eq_None_iff:
+ \<open>xor_num m n = None \<longleftrightarrow> numeral m XOR numeral n = 0\<close>
+ by (simp add: numeral_xor_num split: option.split)
+
+lemma xor_num_eq_Some_iff:
+ \<open>xor_num m n = Some q \<longleftrightarrow> numeral m XOR numeral n = numeral q\<close>
+ by (simp add: numeral_xor_num split: option.split)
+
+end
+
+context ring_bit_operations
+begin
+
+lemma minus_numeral_inc_eq:
+ \<open>- numeral (Num.inc n) = NOT (numeral n)\<close>
+ by (simp add: not_eq_complement sub_inc_One_eq add_One)
+
+lemma sub_one_eq_not_neg:
+ \<open>Num.sub n num.One = NOT (- numeral n)\<close>
+ by (simp add: not_eq_complement)
+
+lemma minus_numeral_eq_not_sub_one:
+ \<open>- numeral n = NOT (Num.sub n num.One)\<close>
+ by (simp add: not_eq_complement)
+
+lemma not_numeral_eq:
+ \<open>NOT (numeral n) = - numeral (Num.inc n)\<close>
+ by (simp add: minus_numeral_inc_eq)
+
+lemma not_minus_numeral_eq [simp]:
+ \<open>NOT (- numeral n) = Num.sub n num.One\<close>
+ by (simp add: sub_one_eq_not_neg)
+
+lemma minus_not_numeral_eq [simp]:
+ \<open>- (NOT (numeral n)) = numeral (Num.inc n)\<close>
+ by (simp add: not_numeral_eq)
+
+end
+
+lemma bit_minus_numeral_int [simp]:
+ \<open>bit (- numeral (num.Bit0 w) :: int) (numeral n) \<longleftrightarrow> bit (- numeral w :: int) (pred_numeral n)\<close>
+ \<open>bit (- numeral (num.Bit1 w) :: int) (numeral n) \<longleftrightarrow> \<not> bit (numeral w :: int) (pred_numeral n)\<close>
+ by (simp_all add: bit_minus_iff bit_not_iff numeral_eq_Suc bit_Suc add_One sub_inc_One_eq)
+
+lemma and_not_numerals [simp]:
+ \<open>1 AND NOT 1 = (0 :: int)\<close>
+ \<open>1 AND NOT (numeral (Num.Bit0 n)) = (1 :: int)\<close>
+ \<open>1 AND NOT (numeral (Num.Bit1 n)) = (0 :: int)\<close>
+ \<open>numeral (Num.Bit0 m) AND NOT (1 :: int) = numeral (Num.Bit0 m)\<close>
+ \<open>numeral (Num.Bit0 m) AND NOT (numeral (Num.Bit0 n)) = (2 :: int) * (numeral m AND NOT (numeral n))\<close>
+ \<open>numeral (Num.Bit0 m) AND NOT (numeral (Num.Bit1 n)) = (2 :: int) * (numeral m AND NOT (numeral n))\<close>
+ \<open>numeral (Num.Bit1 m) AND NOT (1 :: int) = numeral (Num.Bit0 m)\<close>
+ \<open>numeral (Num.Bit1 m) AND NOT (numeral (Num.Bit0 n)) = 1 + (2 :: int) * (numeral m AND NOT (numeral n))\<close>
+ \<open>numeral (Num.Bit1 m) AND NOT (numeral (Num.Bit1 n)) = (2 :: int) * (numeral m AND NOT (numeral n))\<close>
+ by (simp_all add: bit_eq_iff) (auto simp add: bit_simps bit_Suc bit_numeral_rec BitM_inc_eq split: nat.splits)
+
+lemma and_not_not_numerals [simp]:
+ \<open>NOT 1 AND NOT 1 = NOT (1 :: int)\<close>
+ \<open>NOT 1 AND NOT (numeral n) = NOT (1 OR numeral n :: int)\<close>
+ \<open>NOT (numeral m) AND NOT 1 = NOT (numeral m OR 1 :: int)\<close>
+ \<open>NOT (numeral m) AND NOT (numeral n) = NOT (numeral m OR numeral n :: int)\<close>
+ by simp_all
+
+lemma and_minus_numerals [simp]:
+ \<open>- 1 AND k = k\<close>
+ \<open>k AND - 1 = k\<close>
+ \<open>- numeral n AND k = NOT (neg_numeral_class.sub n num.One) AND k\<close>
+ \<open>k AND - numeral n = k AND NOT (neg_numeral_class.sub n num.One)\<close> for k :: int
+ by (simp_all add: minus_numeral_eq_not_sub_one)
+
+fun and_not_num :: \<open>num \<Rightarrow> num \<Rightarrow> num option\<close> \<^marker>\<open>contributor \<open>Andreas Lochbihler\<close>\<close>
+where
+ \<open>and_not_num num.One num.One = None\<close>
+| \<open>and_not_num num.One (num.Bit0 n) = Some num.One\<close>
+| \<open>and_not_num num.One (num.Bit1 n) = None\<close>
+| \<open>and_not_num (num.Bit0 m) num.One = Some (num.Bit0 m)\<close>
+| \<open>and_not_num (num.Bit0 m) (num.Bit0 n) = map_option num.Bit0 (and_not_num m n)\<close>
+| \<open>and_not_num (num.Bit0 m) (num.Bit1 n) = map_option num.Bit0 (and_not_num m n)\<close>
+| \<open>and_not_num (num.Bit1 m) num.One = Some (num.Bit0 m)\<close>
+| \<open>and_not_num (num.Bit1 m) (num.Bit0 n) = (case and_not_num m n of None \<Rightarrow> Some num.One | Some n' \<Rightarrow> Some (num.Bit1 n'))\<close>
+| \<open>and_not_num (num.Bit1 m) (num.Bit1 n) = map_option num.Bit0 (and_not_num m n)\<close>
+
+lemma int_numeral_and_not_num:
+ \<open>numeral m AND NOT (numeral n) = (case and_not_num m n of None \<Rightarrow> 0 :: int | Some n' \<Rightarrow> numeral n')\<close>
+ by (induction m n rule: and_not_num.induct) (simp_all split: option.split)
+
+lemma int_numeral_not_and_num:
+ \<open>NOT (numeral m) AND numeral n = (case and_not_num n m of None \<Rightarrow> 0 :: int | Some n' \<Rightarrow> numeral n')\<close>
+ using int_numeral_and_not_num [of n m] by (simp add: ac_simps)
+
+lemma and_not_num_eq_None_iff:
+ \<open>and_not_num m n = None \<longleftrightarrow> numeral m AND NOT (numeral n) = (0 :: int)\<close>
+ by (simp add: int_numeral_and_not_num split: option.split)
+
+lemma and_not_num_eq_Some_iff:
+ \<open>and_not_num m n = Some q \<longleftrightarrow> numeral m AND NOT (numeral n) = (numeral q :: int)\<close>
+ by (simp add: int_numeral_and_not_num split: option.split)
+
+lemma or_not_numerals [simp]:
+ \<open>1 OR NOT 1 = NOT (0 :: int)\<close>
+ \<open>1 OR NOT (numeral (Num.Bit0 n)) = NOT (numeral (Num.Bit0 n) :: int)\<close>
+ \<open>1 OR NOT (numeral (Num.Bit1 n)) = NOT (numeral (Num.Bit0 n) :: int)\<close>
+ \<open>numeral (Num.Bit0 m) OR NOT (1 :: int) = NOT (1 :: int)\<close>
+ \<open>numeral (Num.Bit0 m) OR NOT (numeral (Num.Bit0 n)) = 1 + (2 :: int) * (numeral m OR NOT (numeral n))\<close>
+ \<open>numeral (Num.Bit0 m) OR NOT (numeral (Num.Bit1 n)) = (2 :: int) * (numeral m OR NOT (numeral n))\<close>
+ \<open>numeral (Num.Bit1 m) OR NOT (1 :: int) = NOT (0 :: int)\<close>
+ \<open>numeral (Num.Bit1 m) OR NOT (numeral (Num.Bit0 n)) = 1 + (2 :: int) * (numeral m OR NOT (numeral n))\<close>
+ \<open>numeral (Num.Bit1 m) OR NOT (numeral (Num.Bit1 n)) = 1 + (2 :: int) * (numeral m OR NOT (numeral n))\<close>
+ by (simp_all add: bit_eq_iff) (simp_all add: bit_simps bit_Suc bit_numeral_rec split: nat.splits)
+
+lemma or_and_numerals [simp]:
+ \<open>NOT 1 OR 1 = NOT (0 :: int)\<close>
+ \<open>NOT 1 OR numeral n = numeral n OR NOT (1 :: int)\<close>
+ \<open>NOT (numeral m) OR 1 = 1 OR NOT (numeral m :: int)\<close>
+ \<open>NOT (numeral m) OR (numeral n) = numeral n OR NOT (numeral m :: int)\<close>
+ by (simp_all add: ac_simps)
+
+lemma or_not_not_numerals [simp]:
+ \<open>NOT 1 OR NOT 1 = NOT (1 :: int)\<close>
+ \<open>NOT 1 OR NOT (numeral n) = NOT (1 AND numeral n :: int)\<close>
+ \<open>NOT (numeral m) OR NOT 1 = NOT (numeral m AND 1 :: int)\<close>
+ \<open>NOT (numeral m) OR NOT (numeral n) = NOT (numeral m AND numeral n :: int)\<close>
+ by simp_all
+
+lemma or_minus_numerals [simp]:
+ \<open>- 1 OR k = - 1\<close>
+ \<open>k OR - 1 = - 1\<close>
+ \<open>- numeral n OR k = NOT (neg_numeral_class.sub n num.One) OR k\<close>
+ \<open>k OR - numeral n = k OR NOT (neg_numeral_class.sub n num.One)\<close> for k :: int
+ by (simp_all add: minus_numeral_eq_not_sub_one)
+
+fun or_not_num_neg :: \<open>num \<Rightarrow> num \<Rightarrow> num\<close> \<^marker>\<open>contributor \<open>Andreas Lochbihler\<close>\<close>
+where
+ \<open>or_not_num_neg num.One num.One = num.One\<close>
+| \<open>or_not_num_neg num.One (num.Bit0 m) = num.Bit1 m\<close>
+| \<open>or_not_num_neg num.One (num.Bit1 m) = num.Bit1 m\<close>
+| \<open>or_not_num_neg (num.Bit0 n) num.One = num.Bit0 num.One\<close>
+| \<open>or_not_num_neg (num.Bit0 n) (num.Bit0 m) = Num.BitM (or_not_num_neg n m)\<close>
+| \<open>or_not_num_neg (num.Bit0 n) (num.Bit1 m) = num.Bit0 (or_not_num_neg n m)\<close>
+| \<open>or_not_num_neg (num.Bit1 n) num.One = num.One\<close>
+| \<open>or_not_num_neg (num.Bit1 n) (num.Bit0 m) = Num.BitM (or_not_num_neg n m)\<close>
+| \<open>or_not_num_neg (num.Bit1 n) (num.Bit1 m) = Num.BitM (or_not_num_neg n m)\<close>
+
+lemma int_numeral_or_not_num_neg:
+ \<open>numeral m OR NOT (numeral n :: int) = - numeral (or_not_num_neg m n)\<close>
+ apply (induction m n rule: or_not_num_neg.induct)
+ apply simp_all
+ apply (simp_all add: not_one_eq not_numeral_eq)
+ done
+
+lemma int_numeral_not_or_num_neg:
+ \<open>NOT (numeral m) OR (numeral n :: int) = - numeral (or_not_num_neg n m)\<close>
+ using int_numeral_or_not_num_neg [of n m] by (simp add: ac_simps)
+
+lemma numeral_or_not_num_eq:
+ \<open>numeral (or_not_num_neg m n) = - (numeral m OR NOT (numeral n :: int))\<close>
+ using int_numeral_or_not_num_neg [of m n] by simp
+
+lemma xor_minus_numerals [simp]:
+ \<open>- 1 XOR k = NOT k\<close>
+ \<open>k XOR - 1 = NOT k\<close>
+ \<open>- numeral n XOR k = NOT (neg_numeral_class.sub n num.One XOR k)\<close>
+ \<open>k XOR - numeral n = NOT (k XOR (neg_numeral_class.sub n num.One))\<close> for k :: int
+ by (simp_all add: minus_numeral_eq_not_sub_one)
+
+
subsection \<open>More properties\<close>
lemma take_bit_eq_mask_iff:
@@ -2425,6 +2717,10 @@
\<open>of_int (NOT k) = NOT (of_int k)\<close>
by (rule bit_eqI) (simp add: bit_not_iff Bit_Operations.bit_not_iff bit_of_int_iff)
+lemma of_int_not_numeral:
+ \<open>of_int (NOT (numeral k)) = NOT (numeral k)\<close>
+ by (simp add: local.of_int_not_eq)
+
lemma of_int_and_eq:
\<open>of_int (k AND l) = of_int k AND of_int l\<close>
by (rule bit_eqI) (simp add: bit_of_int_iff bit_and_iff Bit_Operations.bit_and_iff)
@@ -2547,157 +2843,6 @@
by (auto simp add: le_less take_bit_int_greater_self_iff take_bit_int_eq_self_iff
dest: sym not_sym intro: less_trans [of k 0 \<open>2 ^ n\<close>])
-lemma minus_numeral_inc_eq:
- \<open>- numeral (Num.inc n) = NOT (numeral n :: int)\<close>
- by (simp add: not_int_def sub_inc_One_eq add_One)
-
-lemma sub_one_eq_not_neg:
- \<open>Num.sub n num.One = NOT (- numeral n :: int)\<close>
- by (simp add: not_int_def)
-
-lemma bit_numeral_int_iff [bit_simps]:
- \<open>bit (numeral m :: int) n \<longleftrightarrow> bit (numeral m :: nat) n\<close>
- using bit_of_nat_iff_bit [of \<open>numeral m\<close> n] by simp
-
-lemma bit_minus_int_iff [bit_simps]:
- \<open>bit (- k) n \<longleftrightarrow> \<not> bit (k - 1) n\<close>
- for k :: int
- using bit_not_int_iff' [of \<open>k - 1\<close>] by simp
-
-lemma bit_numeral_int_simps [simp]:
- \<open>bit (1 :: int) (numeral n) \<longleftrightarrow> bit (0 :: int) (pred_numeral n)\<close>
- \<open>bit (numeral (num.Bit0 w) :: int) (numeral n) \<longleftrightarrow> bit (numeral w :: int) (pred_numeral n)\<close>
- \<open>bit (numeral (num.Bit1 w) :: int) (numeral n) \<longleftrightarrow> bit (numeral w :: int) (pred_numeral n)\<close>
- \<open>bit (numeral (Num.BitM w) :: int) (numeral n) \<longleftrightarrow> \<not> bit (- numeral w :: int) (pred_numeral n)\<close>
- \<open>bit (- numeral (num.Bit0 w) :: int) (numeral n) \<longleftrightarrow> bit (- numeral w :: int) (pred_numeral n)\<close>
- \<open>bit (- numeral (num.Bit1 w) :: int) (numeral n) \<longleftrightarrow> \<not> bit (numeral w :: int) (pred_numeral n)\<close>
- \<open>bit (- numeral (Num.BitM w) :: int) (numeral n) \<longleftrightarrow> bit (- (numeral w) :: int) (pred_numeral n)\<close>
- by (simp_all add: bit_1_iff numeral_eq_Suc bit_Suc add_One sub_inc_One_eq bit_minus_int_iff)
-
-lemma bit_numeral_Bit0_Suc_iff [simp]:
- \<open>bit (numeral (Num.Bit0 m) :: int) (Suc n) \<longleftrightarrow> bit (numeral m :: int) n\<close>
- by (simp add: bit_Suc)
-
-lemma bit_numeral_Bit1_Suc_iff [simp]:
- \<open>bit (numeral (Num.Bit1 m) :: int) (Suc n) \<longleftrightarrow> bit (numeral m :: int) n\<close>
- by (simp add: bit_Suc)
-
-lemma int_not_numerals [simp]:
- \<open>NOT (numeral (Num.Bit0 n) :: int) = - numeral (Num.Bit1 n)\<close>
- \<open>NOT (numeral (Num.Bit1 n) :: int) = - numeral (Num.inc (num.Bit1 n))\<close>
- \<open>NOT (numeral (Num.BitM n) :: int) = - numeral (num.Bit0 n)\<close>
- \<open>NOT (- numeral (Num.Bit0 n) :: int) = numeral (Num.BitM n)\<close>
- \<open>NOT (- numeral (Num.Bit1 n) :: int) = numeral (Num.Bit0 n)\<close>
- by (simp_all add: not_int_def add_One inc_BitM_eq)
-
-text \<open>FIXME: The rule sets below are very large (24 rules for each
- operator). Is there a simpler way to do this?\<close>
-
-context
-begin
-
-private lemma eqI:
- \<open>k = l\<close>
- if num: \<open>\<And>n. bit k (numeral n) \<longleftrightarrow> bit l (numeral n)\<close>
- and even: \<open>even k \<longleftrightarrow> even l\<close>
- for k l :: int
-proof (rule bit_eqI)
- fix n
- show \<open>bit k n \<longleftrightarrow> bit l n\<close>
- proof (cases n)
- case 0
- with even show ?thesis
- by simp
- next
- case (Suc n)
- with num [of \<open>num_of_nat (Suc n)\<close>] show ?thesis
- by (simp only: numeral_num_of_nat)
- qed
-qed
-
-lemma int_and_numerals [simp]:
- \<open>numeral (Num.Bit0 x) AND numeral (Num.Bit0 y) = (2 :: int) * (numeral x AND numeral y)\<close>
- \<open>numeral (Num.Bit0 x) AND numeral (Num.Bit1 y) = (2 :: int) * (numeral x AND numeral y)\<close>
- \<open>numeral (Num.Bit1 x) AND numeral (Num.Bit0 y) = (2 :: int) * (numeral x AND numeral y)\<close>
- \<open>numeral (Num.Bit1 x) AND numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x AND numeral y)\<close>
- \<open>numeral (Num.Bit0 x) AND - numeral (Num.Bit0 y) = (2 :: int) * (numeral x AND - numeral y)\<close>
- \<open>numeral (Num.Bit0 x) AND - numeral (Num.Bit1 y) = (2 :: int) * (numeral x AND - numeral (y + Num.One))\<close>
- \<open>numeral (Num.Bit1 x) AND - numeral (Num.Bit0 y) = (2 :: int) * (numeral x AND - numeral y)\<close>
- \<open>numeral (Num.Bit1 x) AND - numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x AND - numeral (y + Num.One))\<close>
- \<open>- numeral (Num.Bit0 x) AND numeral (Num.Bit0 y) = (2 :: int) * (- numeral x AND numeral y)\<close>
- \<open>- numeral (Num.Bit0 x) AND numeral (Num.Bit1 y) = (2 :: int) * (- numeral x AND numeral y)\<close>
- \<open>- numeral (Num.Bit1 x) AND numeral (Num.Bit0 y) = (2 :: int) * (- numeral (x + Num.One) AND numeral y)\<close>
- \<open>- numeral (Num.Bit1 x) AND numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral (x + Num.One) AND numeral y)\<close>
- \<open>- numeral (Num.Bit0 x) AND - numeral (Num.Bit0 y) = (2 :: int) * (- numeral x AND - numeral y)\<close>
- \<open>- numeral (Num.Bit0 x) AND - numeral (Num.Bit1 y) = (2 :: int) * (- numeral x AND - numeral (y + Num.One))\<close>
- \<open>- numeral (Num.Bit1 x) AND - numeral (Num.Bit0 y) = (2 :: int) * (- numeral (x + Num.One) AND - numeral y)\<close>
- \<open>- numeral (Num.Bit1 x) AND - numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral (x + Num.One) AND - numeral (y + Num.One))\<close>
- \<open>(1::int) AND numeral (Num.Bit0 y) = 0\<close>
- \<open>(1::int) AND numeral (Num.Bit1 y) = 1\<close>
- \<open>(1::int) AND - numeral (Num.Bit0 y) = 0\<close>
- \<open>(1::int) AND - numeral (Num.Bit1 y) = 1\<close>
- \<open>numeral (Num.Bit0 x) AND (1::int) = 0\<close>
- \<open>numeral (Num.Bit1 x) AND (1::int) = 1\<close>
- \<open>- numeral (Num.Bit0 x) AND (1::int) = 0\<close>
- \<open>- numeral (Num.Bit1 x) AND (1::int) = 1\<close>
- by (auto simp add: bit_and_iff bit_minus_iff even_and_iff bit_double_iff even_bit_succ_iff add_One sub_inc_One_eq intro: eqI)
-
-lemma int_or_numerals [simp]:
- \<open>numeral (Num.Bit0 x) OR numeral (Num.Bit0 y) = (2 :: int) * (numeral x OR numeral y)\<close>
- \<open>numeral (Num.Bit0 x) OR numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x OR numeral y)\<close>
- \<open>numeral (Num.Bit1 x) OR numeral (Num.Bit0 y) = 1 + (2 :: int) * (numeral x OR numeral y)\<close>
- \<open>numeral (Num.Bit1 x) OR numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x OR numeral y)\<close>
- \<open>numeral (Num.Bit0 x) OR - numeral (Num.Bit0 y) = (2 :: int) * (numeral x OR - numeral y)\<close>
- \<open>numeral (Num.Bit0 x) OR - numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x OR - numeral (y + Num.One))\<close>
- \<open>numeral (Num.Bit1 x) OR - numeral (Num.Bit0 y) = 1 + (2 :: int) * (numeral x OR - numeral y)\<close>
- \<open>numeral (Num.Bit1 x) OR - numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x OR - numeral (y + Num.One))\<close>
- \<open>- numeral (Num.Bit0 x) OR numeral (Num.Bit0 y) = (2 :: int) * (- numeral x OR numeral y)\<close>
- \<open>- numeral (Num.Bit0 x) OR numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral x OR numeral y)\<close>
- \<open>- numeral (Num.Bit1 x) OR numeral (Num.Bit0 y) = 1 + (2 :: int) * (- numeral (x + Num.One) OR numeral y)\<close>
- \<open>- numeral (Num.Bit1 x) OR numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral (x + Num.One) OR numeral y)\<close>
- \<open>- numeral (Num.Bit0 x) OR - numeral (Num.Bit0 y) = (2 :: int) * (- numeral x OR - numeral y)\<close>
- \<open>- numeral (Num.Bit0 x) OR - numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral x OR - numeral (y + Num.One))\<close>
- \<open>- numeral (Num.Bit1 x) OR - numeral (Num.Bit0 y) = 1 + (2 :: int) * (- numeral (x + Num.One) OR - numeral y)\<close>
- \<open>- numeral (Num.Bit1 x) OR - numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral (x + Num.One) OR - numeral (y + Num.One))\<close>
- \<open>(1::int) OR numeral (Num.Bit0 y) = numeral (Num.Bit1 y)\<close>
- \<open>(1::int) OR numeral (Num.Bit1 y) = numeral (Num.Bit1 y)\<close>
- \<open>(1::int) OR - numeral (Num.Bit0 y) = - numeral (Num.BitM y)\<close>
- \<open>(1::int) OR - numeral (Num.Bit1 y) = - numeral (Num.Bit1 y)\<close>
- \<open>numeral (Num.Bit0 x) OR (1::int) = numeral (Num.Bit1 x)\<close>
- \<open>numeral (Num.Bit1 x) OR (1::int) = numeral (Num.Bit1 x)\<close>
- \<open>- numeral (Num.Bit0 x) OR (1::int) = - numeral (Num.BitM x)\<close>
- \<open>- numeral (Num.Bit1 x) OR (1::int) = - numeral (Num.Bit1 x)\<close>
- by (auto simp add: bit_or_iff bit_minus_iff even_or_iff bit_double_iff even_bit_succ_iff add_One sub_inc_One_eq sub_BitM_One_eq intro: eqI)
-
-lemma int_xor_numerals [simp]:
- \<open>numeral (Num.Bit0 x) XOR numeral (Num.Bit0 y) = (2 :: int) * (numeral x XOR numeral y)\<close>
- \<open>numeral (Num.Bit0 x) XOR numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x XOR numeral y)\<close>
- \<open>numeral (Num.Bit1 x) XOR numeral (Num.Bit0 y) = 1 + (2 :: int) * (numeral x XOR numeral y)\<close>
- \<open>numeral (Num.Bit1 x) XOR numeral (Num.Bit1 y) = (2 :: int) * (numeral x XOR numeral y)\<close>
- \<open>numeral (Num.Bit0 x) XOR - numeral (Num.Bit0 y) = (2 :: int) * (numeral x XOR - numeral y)\<close>
- \<open>numeral (Num.Bit0 x) XOR - numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x XOR - numeral (y + Num.One))\<close>
- \<open>numeral (Num.Bit1 x) XOR - numeral (Num.Bit0 y) = 1 + (2 :: int) * (numeral x XOR - numeral y)\<close>
- \<open>numeral (Num.Bit1 x) XOR - numeral (Num.Bit1 y) = (2 :: int) * (numeral x XOR - numeral (y + Num.One))\<close>
- \<open>- numeral (Num.Bit0 x) XOR numeral (Num.Bit0 y) = (2 :: int) * (- numeral x XOR numeral y)\<close>
- \<open>- numeral (Num.Bit0 x) XOR numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral x XOR numeral y)\<close>
- \<open>- numeral (Num.Bit1 x) XOR numeral (Num.Bit0 y) = 1 + (2 :: int) * (- numeral (x + Num.One) XOR numeral y)\<close>
- \<open>- numeral (Num.Bit1 x) XOR numeral (Num.Bit1 y) = (2 :: int) * (- numeral (x + Num.One) XOR numeral y)\<close>
- \<open>- numeral (Num.Bit0 x) XOR - numeral (Num.Bit0 y) = (2 :: int) * (- numeral x XOR - numeral y)\<close>
- \<open>- numeral (Num.Bit0 x) XOR - numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral x XOR - numeral (y + Num.One))\<close>
- \<open>- numeral (Num.Bit1 x) XOR - numeral (Num.Bit0 y) = 1 + (2 :: int) * (- numeral (x + Num.One) XOR - numeral y)\<close>
- \<open>- numeral (Num.Bit1 x) XOR - numeral (Num.Bit1 y) = (2 :: int) * (- numeral (x + Num.One) XOR - numeral (y + Num.One))\<close>
- \<open>(1::int) XOR numeral (Num.Bit0 y) = numeral (Num.Bit1 y)\<close>
- \<open>(1::int) XOR numeral (Num.Bit1 y) = numeral (Num.Bit0 y)\<close>
- \<open>(1::int) XOR - numeral (Num.Bit0 y) = - numeral (Num.BitM y)\<close>
- \<open>(1::int) XOR - numeral (Num.Bit1 y) = - numeral (Num.Bit0 (y + Num.One))\<close>
- \<open>numeral (Num.Bit0 x) XOR (1::int) = numeral (Num.Bit1 x)\<close>
- \<open>numeral (Num.Bit1 x) XOR (1::int) = numeral (Num.Bit0 x)\<close>
- \<open>- numeral (Num.Bit0 x) XOR (1::int) = - numeral (Num.BitM x)\<close>
- \<open>- numeral (Num.Bit1 x) XOR (1::int) = - numeral (Num.Bit0 (x + Num.One))\<close>
- by (auto simp add: bit_xor_iff bit_minus_iff even_xor_iff bit_double_iff even_bit_succ_iff add_One sub_inc_One_eq sub_BitM_One_eq intro: eqI)
-
-end
-
context semiring_bit_operations
begin
@@ -3368,129 +3513,6 @@
qed
-subsection \<open>Symbolic computations on numeral expressions\<close> \<^marker>\<open>contributor \<open>Andreas Lochbihler\<close>\<close>
-
-fun and_num :: \<open>num \<Rightarrow> num \<Rightarrow> num option\<close>
-where
- \<open>and_num num.One num.One = Some num.One\<close>
-| \<open>and_num num.One (num.Bit0 n) = None\<close>
-| \<open>and_num num.One (num.Bit1 n) = Some num.One\<close>
-| \<open>and_num (num.Bit0 m) num.One = None\<close>
-| \<open>and_num (num.Bit0 m) (num.Bit0 n) = map_option num.Bit0 (and_num m n)\<close>
-| \<open>and_num (num.Bit0 m) (num.Bit1 n) = map_option num.Bit0 (and_num m n)\<close>
-| \<open>and_num (num.Bit1 m) num.One = Some num.One\<close>
-| \<open>and_num (num.Bit1 m) (num.Bit0 n) = map_option num.Bit0 (and_num m n)\<close>
-| \<open>and_num (num.Bit1 m) (num.Bit1 n) = (case and_num m n of None \<Rightarrow> Some num.One | Some n' \<Rightarrow> Some (num.Bit1 n'))\<close>
-
-fun and_not_num :: \<open>num \<Rightarrow> num \<Rightarrow> num option\<close>
-where
- \<open>and_not_num num.One num.One = None\<close>
-| \<open>and_not_num num.One (num.Bit0 n) = Some num.One\<close>
-| \<open>and_not_num num.One (num.Bit1 n) = None\<close>
-| \<open>and_not_num (num.Bit0 m) num.One = Some (num.Bit0 m)\<close>
-| \<open>and_not_num (num.Bit0 m) (num.Bit0 n) = map_option num.Bit0 (and_not_num m n)\<close>
-| \<open>and_not_num (num.Bit0 m) (num.Bit1 n) = map_option num.Bit0 (and_not_num m n)\<close>
-| \<open>and_not_num (num.Bit1 m) num.One = Some (num.Bit0 m)\<close>
-| \<open>and_not_num (num.Bit1 m) (num.Bit0 n) = (case and_not_num m n of None \<Rightarrow> Some num.One | Some n' \<Rightarrow> Some (num.Bit1 n'))\<close>
-| \<open>and_not_num (num.Bit1 m) (num.Bit1 n) = map_option num.Bit0 (and_not_num m n)\<close>
-
-fun or_num :: \<open>num \<Rightarrow> num \<Rightarrow> num\<close>
-where
- \<open>or_num num.One num.One = num.One\<close>
-| \<open>or_num num.One (num.Bit0 n) = num.Bit1 n\<close>
-| \<open>or_num num.One (num.Bit1 n) = num.Bit1 n\<close>
-| \<open>or_num (num.Bit0 m) num.One = num.Bit1 m\<close>
-| \<open>or_num (num.Bit0 m) (num.Bit0 n) = num.Bit0 (or_num m n)\<close>
-| \<open>or_num (num.Bit0 m) (num.Bit1 n) = num.Bit1 (or_num m n)\<close>
-| \<open>or_num (num.Bit1 m) num.One = num.Bit1 m\<close>
-| \<open>or_num (num.Bit1 m) (num.Bit0 n) = num.Bit1 (or_num m n)\<close>
-| \<open>or_num (num.Bit1 m) (num.Bit1 n) = num.Bit1 (or_num m n)\<close>
-
-fun or_not_num_neg :: \<open>num \<Rightarrow> num \<Rightarrow> num\<close>
-where
- \<open>or_not_num_neg num.One num.One = num.One\<close>
-| \<open>or_not_num_neg num.One (num.Bit0 m) = num.Bit1 m\<close>
-| \<open>or_not_num_neg num.One (num.Bit1 m) = num.Bit1 m\<close>
-| \<open>or_not_num_neg (num.Bit0 n) num.One = num.Bit0 num.One\<close>
-| \<open>or_not_num_neg (num.Bit0 n) (num.Bit0 m) = Num.BitM (or_not_num_neg n m)\<close>
-| \<open>or_not_num_neg (num.Bit0 n) (num.Bit1 m) = num.Bit0 (or_not_num_neg n m)\<close>
-| \<open>or_not_num_neg (num.Bit1 n) num.One = num.One\<close>
-| \<open>or_not_num_neg (num.Bit1 n) (num.Bit0 m) = Num.BitM (or_not_num_neg n m)\<close>
-| \<open>or_not_num_neg (num.Bit1 n) (num.Bit1 m) = Num.BitM (or_not_num_neg n m)\<close>
-
-fun xor_num :: \<open>num \<Rightarrow> num \<Rightarrow> num option\<close>
-where
- \<open>xor_num num.One num.One = None\<close>
-| \<open>xor_num num.One (num.Bit0 n) = Some (num.Bit1 n)\<close>
-| \<open>xor_num num.One (num.Bit1 n) = Some (num.Bit0 n)\<close>
-| \<open>xor_num (num.Bit0 m) num.One = Some (num.Bit1 m)\<close>
-| \<open>xor_num (num.Bit0 m) (num.Bit0 n) = map_option num.Bit0 (xor_num m n)\<close>
-| \<open>xor_num (num.Bit0 m) (num.Bit1 n) = Some (case xor_num m n of None \<Rightarrow> num.One | Some n' \<Rightarrow> num.Bit1 n')\<close>
-| \<open>xor_num (num.Bit1 m) num.One = Some (num.Bit0 m)\<close>
-| \<open>xor_num (num.Bit1 m) (num.Bit0 n) = Some (case xor_num m n of None \<Rightarrow> num.One | Some n' \<Rightarrow> num.Bit1 n')\<close>
-| \<open>xor_num (num.Bit1 m) (num.Bit1 n) = map_option num.Bit0 (xor_num m n)\<close>
-
-lemma int_numeral_and_num:
- \<open>numeral m AND numeral n = (case and_num m n of None \<Rightarrow> 0 :: int | Some n' \<Rightarrow> numeral n')\<close>
- by (induction m n rule: and_num.induct) (simp_all split: option.split)
-
-lemma and_num_eq_None_iff:
- \<open>and_num m n = None \<longleftrightarrow> numeral m AND numeral n = (0::int)\<close>
- by (simp add: int_numeral_and_num split: option.split)
-
-lemma and_num_eq_Some_iff:
- \<open>and_num m n = Some q \<longleftrightarrow> numeral m AND numeral n = (numeral q :: int)\<close>
- by (simp add: int_numeral_and_num split: option.split)
-
-lemma int_numeral_and_not_num:
- \<open>numeral m AND NOT (numeral n) = (case and_not_num m n of None \<Rightarrow> 0 :: int | Some n' \<Rightarrow> numeral n')\<close>
- by (induction m n rule: and_not_num.induct) (simp_all add: add_One BitM_inc_eq not_int_def split: option.split)
-
-lemma int_numeral_not_and_num:
- \<open>NOT (numeral m) AND numeral n = (case and_not_num n m of None \<Rightarrow> 0 :: int | Some n' \<Rightarrow> numeral n')\<close>
- using int_numeral_and_not_num [of n m] by (simp add: ac_simps)
-
-lemma and_not_num_eq_None_iff:
- \<open>and_not_num m n = None \<longleftrightarrow> numeral m AND NOT (numeral n) = (0::int)\<close>
- by (simp add: int_numeral_and_not_num split: option.split)
-
-lemma and_not_num_eq_Some_iff:
- \<open>and_not_num m n = Some q \<longleftrightarrow> numeral m AND NOT (numeral n) = (numeral q :: int)\<close>
- by (simp add: int_numeral_and_not_num split: option.split)
-
-lemma int_numeral_or_num:
- \<open>numeral m OR numeral n = (numeral (or_num m n) :: int)\<close>
- by (induction m n rule: or_num.induct) simp_all
-
-lemma numeral_or_num_eq:
- \<open>numeral (or_num m n) = (numeral m OR numeral n :: int)\<close>
- by (simp add: int_numeral_or_num)
-
-lemma int_numeral_or_not_num_neg:
- \<open>numeral m OR NOT (numeral n :: int) = - numeral (or_not_num_neg m n)\<close>
- by (induction m n rule: or_not_num_neg.induct) (simp_all add: add_One BitM_inc_eq not_int_def)
-
-lemma int_numeral_not_or_num_neg:
- \<open>NOT (numeral m) OR (numeral n :: int) = - numeral (or_not_num_neg n m)\<close>
- using int_numeral_or_not_num_neg [of n m] by (simp add: ac_simps)
-
-lemma numeral_or_not_num_eq:
- \<open>numeral (or_not_num_neg m n) = - (numeral m OR NOT (numeral n :: int))\<close>
- using int_numeral_or_not_num_neg [of m n] by simp
-
-lemma int_numeral_xor_num:
- \<open>numeral m XOR numeral n = (case xor_num m n of None \<Rightarrow> 0 :: int | Some n' \<Rightarrow> numeral n')\<close>
- by (induction m n rule: xor_num.induct) (simp_all split: option.split)
-
-lemma xor_num_eq_None_iff:
- \<open>xor_num m n = None \<longleftrightarrow> numeral m XOR numeral n = (0::int)\<close>
- by (simp add: int_numeral_xor_num split: option.split)
-
-lemma xor_num_eq_Some_iff:
- \<open>xor_num m n = Some q \<longleftrightarrow> numeral m XOR numeral n = (numeral q :: int)\<close>
- by (simp add: int_numeral_xor_num split: option.split)
-
-
subsection \<open>Key ideas of bit operations\<close>
text \<open>
--- a/src/HOL/Library/AList.thy Wed Aug 18 12:33:31 2021 +0200
+++ b/src/HOL/Library/AList.thy Wed Aug 25 21:43:43 2021 +0200
@@ -424,7 +424,7 @@
qed
lemma graph_map_of: "Map.graph (map_of al) = set (clearjunk al)"
- by (metis distinct_clearjunk graph_map_of_if_distinct_ran map_of_clearjunk)
+ by (metis distinct_clearjunk graph_map_of_if_distinct_dom map_of_clearjunk)
lemma clearjunk_update: "clearjunk (update k v al) = update k v (clearjunk al)"
by (induct al rule: clearjunk.induct) (simp_all add: delete_update)
--- a/src/HOL/Library/Mapping.thy Wed Aug 18 12:33:31 2021 +0200
+++ b/src/HOL/Library/Mapping.thy Wed Aug 25 21:43:43 2021 +0200
@@ -284,16 +284,22 @@
qed
qed
-lemma lookup_update: "lookup (update k v m) k = Some v"
+lemma lookup_update[simp]: "lookup (update k v m) k = Some v"
+ by transfer simp
+
+lemma lookup_update_neq[simp]: "k \<noteq> k' \<Longrightarrow> lookup (update k v m) k' = lookup m k'"
by transfer simp
-lemma lookup_update_neq: "k \<noteq> k' \<Longrightarrow> lookup (update k v m) k' = lookup m k'"
+lemma lookup_update': "lookup (update k v m) k' = (if k = k' then Some v else lookup m k')"
by transfer simp
-lemma lookup_update': "Mapping.lookup (update k v m) k' = (if k = k' then Some v else lookup m k')"
- by (auto simp: lookup_update lookup_update_neq)
+lemma lookup_empty[simp]: "lookup empty k = None"
+ by transfer simp
-lemma lookup_empty: "lookup empty k = None"
+lemma lookup_delete[simp]: "lookup (delete k m) k = None"
+ by transfer simp
+
+lemma lookup_delete_neq[simp]: "k \<noteq> k' \<Longrightarrow> lookup (delete k m) k' = lookup m k'"
by transfer simp
lemma lookup_filter:
@@ -310,11 +316,11 @@
by (simp add: lookup_default_def lookup_empty)
lemma lookup_default_update: "lookup_default d (update k v m) k = v"
- by (simp add: lookup_default_def lookup_update)
+ by (simp add: lookup_default_def)
lemma lookup_default_update_neq:
"k \<noteq> k' \<Longrightarrow> lookup_default d (update k v m) k' = lookup_default d m k'"
- by (simp add: lookup_default_def lookup_update_neq)
+ by (simp add: lookup_default_def)
lemma lookup_default_update':
"lookup_default d (update k v m) k' = (if k = k' then v else lookup_default d m k')"
@@ -398,7 +404,7 @@
shows "Mapping.lookup (Mapping.tabulate xs f) x = (if x \<in> set xs then Some (f x) else None)"
using assms by transfer (auto simp: map_of_eq_None_iff o_def dest!: map_of_SomeD)
-lemma lookup_of_alist: "Mapping.lookup (Mapping.of_alist xs) k = map_of xs k"
+lemma lookup_of_alist: "lookup (of_alist xs) k = map_of xs k"
by transfer simp_all
lemma keys_is_none_rep [code_unfold]: "k \<in> keys m \<longleftrightarrow> \<not> (Option.is_none (lookup m k))"
@@ -420,6 +426,10 @@
lemma delete_empty [simp]: "delete k empty = empty"
by transfer simp
+lemma Mapping_delete_if_notin_keys[simp]:
+ "k \<notin> keys m \<Longrightarrow> delete k m = m"
+ by transfer simp
+
lemma replace_update:
"k \<notin> keys m \<Longrightarrow> replace k v m = m"
"k \<in> keys m \<Longrightarrow> replace k v m = update k v m"
@@ -487,9 +497,6 @@
lemma in_keysD: "k \<in> keys m \<Longrightarrow> \<exists>v. lookup m k = Some v"
by transfer (fact domD)
-lemma in_entriesI: "lookup m k = Some v \<Longrightarrow> (k, v) \<in> entries m"
- by transfer (fact in_graphI)
-
lemma keys_update [simp]: "keys (update k v m) = insert k (keys m)"
by transfer simp
@@ -527,6 +534,14 @@
lemma keys_bulkload [simp]: "keys (bulkload xs) = {0..<length xs}"
by (simp add: bulkload_tabulate)
+lemma finite_keys_update[simp]:
+ "finite (keys (update k v m)) = finite (keys m)"
+ by transfer simp
+
+lemma set_ordered_keys[simp]:
+ "finite (Mapping.keys m) \<Longrightarrow> set (Mapping.ordered_keys m) = Mapping.keys m"
+ unfolding ordered_keys_def by transfer auto
+
lemma distinct_ordered_keys [simp]: "distinct (ordered_keys m)"
by (simp add: ordered_keys_def)
@@ -536,6 +551,9 @@
lemma ordered_keys_empty [simp]: "ordered_keys empty = []"
by (simp add: ordered_keys_def)
+lemma sorted_ordered_keys[simp]: "sorted (ordered_keys m)"
+ unfolding ordered_keys_def by simp
+
lemma ordered_keys_update [simp]:
"k \<in> keys m \<Longrightarrow> ordered_keys (update k v m) = ordered_keys m"
"finite (keys m) \<Longrightarrow> k \<notin> keys m \<Longrightarrow>
@@ -806,42 +824,43 @@
qed simp
qed simp
+lemma entries_empty[simp]: "entries empty = {}"
+ by transfer (fact graph_empty)
+
lemma entries_lookup: "entries m = Map.graph (lookup m)"
by transfer rule
-lemma entries_empty[simp]: "entries empty = {}"
- by transfer (fact graph_empty)
+lemma in_entriesI: "lookup m k = Some v \<Longrightarrow> (k, v) \<in> entries m"
+ by transfer (fact in_graphI)
+
+lemma in_entriesD: "(k, v) \<in> entries m \<Longrightarrow> lookup m k = Some v"
+ by transfer (fact in_graphD)
+
+lemma fst_image_entries_eq_keys[simp]: "fst ` Mapping.entries m = Mapping.keys m"
+ by transfer (fact fst_graph_eq_dom)
lemma finite_entries_iff_finite_keys[simp]:
"finite (entries m) = finite (keys m)"
by transfer (fact finite_graph_iff_finite_dom)
-lemma entries_update[simp]:
+lemma entries_update:
"entries (update k v m) = insert (k, v) (entries (delete k m))"
by transfer (fact graph_map_upd)
-lemma Mapping_delete_if_notin_keys[simp]:
- "k \<notin> Mapping.keys m \<Longrightarrow> delete k m = m"
- by transfer simp
-
lemma entries_delete:
"entries (delete k m) = {e \<in> entries m. fst e \<noteq> k}"
by transfer (fact graph_fun_upd_None)
lemma entries_of_alist[simp]:
"distinct (List.map fst xs) \<Longrightarrow> entries (of_alist xs) = set xs"
- by transfer (fact graph_map_of_if_distinct_ran)
+ by transfer (fact graph_map_of_if_distinct_dom)
lemma entries_keysD:
"x \<in> entries m \<Longrightarrow> fst x \<in> keys m"
by transfer (fact graph_domD)
-lemma finite_keys_entries[simp]:
- "finite (keys (update k v m)) = finite (keys m)"
- by transfer simp
-
lemma set_ordered_entries[simp]:
- "finite (Mapping.keys m) \<Longrightarrow> set (ordered_entries m) = entries m"
+ "finite (keys m) \<Longrightarrow> set (ordered_entries m) = entries m"
unfolding ordered_entries_def
by transfer (auto simp: folding_Map_graph.set_sorted_key_list_of_set[OF subset_refl])
@@ -884,6 +903,22 @@
"ordered_entries (delete k m) = AList.delete k (ordered_entries m)"
unfolding ordered_entries_def by transfer auto
+lemma map_fst_ordered_entries[simp]:
+ "List.map fst (ordered_entries m) = ordered_keys m"
+proof(cases "finite (Mapping.keys m)")
+ case True
+ then have "set (List.map fst (Mapping.ordered_entries m)) = set (Mapping.ordered_keys m)"
+ unfolding ordered_entries_def ordered_keys_def
+ by (transfer) (simp add: folding_Map_graph.set_sorted_key_list_of_set[OF subset_refl] fst_graph_eq_dom)
+ with True show "List.map fst (Mapping.ordered_entries m) = Mapping.ordered_keys m"
+ by (metis distinct_ordered_entries ordered_keys_def sorted_list_of_set.idem_if_sorted_distinct
+ sorted_list_of_set.set_sorted_key_list_of_set sorted_ordered_entries)
+next
+ case False
+ then show ?thesis
+ unfolding ordered_entries_def ordered_keys_def by simp
+qed
+
lemma fold_empty[simp]: "fold f empty a = a"
unfolding fold_def by simp
@@ -908,7 +943,9 @@
unfolding ordered_entries_def
by transfer (fastforce simp: folding_Map_graph.set_sorted_key_list_of_set[OF order_refl]
dest: graph_domD)
- from insort_key_is_snoc_if_sorted_and_distinct[OF _ _ this] k_notin_entries show ?thesis
+ from insort_key_is_snoc_if_sorted_and_distinct[OF _ _ this] k_notin_entries \<open>finite (keys m)\<close>
+ show ?thesis
+ using sorted_ordered_keys
unfolding insort_insert_key_def by auto
qed
finally show ?thesis unfolding fold_def by simp
--- a/src/HOL/Library/RBT_Mapping.thy Wed Aug 18 12:33:31 2021 +0200
+++ b/src/HOL/Library/RBT_Mapping.thy Wed Aug 25 21:43:43 2021 +0200
@@ -58,7 +58,7 @@
by (transfer fixing: t) (auto simp add: lookup_keys intro: sorted_distinct_set_unique)
lemma Map_graph_lookup: "Map.graph (RBT.lookup t) = set (RBT.entries t)"
- by (metis RBT.distinct_entries RBT.map_of_entries graph_map_of_if_distinct_ran)
+ by (metis RBT.distinct_entries RBT.map_of_entries graph_map_of_if_distinct_dom)
lemma entries_Mapping [code]: "Mapping.entries (Mapping t) = set (RBT.entries t)"
by (transfer fixing: t) (fact Map_graph_lookup)
--- a/src/HOL/Library/Word.thy Wed Aug 18 12:33:31 2021 +0200
+++ b/src/HOL/Library/Word.thy Wed Aug 25 21:43:43 2021 +0200
@@ -3394,7 +3394,11 @@
"1 XOR - numeral b = word_of_int (1 XOR - numeral b)"
"numeral a XOR 1 = word_of_int (numeral a XOR 1)"
"- numeral a XOR 1 = word_of_int (- numeral a XOR 1)"
- by (transfer, simp)+
+ apply (simp_all add: word_uint_eq_iff unsigned_not_eq unsigned_and_eq unsigned_or_eq unsigned_xor_eq not_one_eq of_nat_take_bit ac_simps)
+ apply (simp_all add: minus_numeral_eq_not_sub_one)
+ apply (simp_all only: sub_one_eq_not_neg bit.xor_compl_right take_bit_xor bit.double_compl)
+ apply simp_all
+ done
text \<open>Special cases for when one of the arguments equals -1.\<close>
@@ -3408,6 +3412,10 @@
"x XOR (-1::'a::len word) = NOT x"
by (transfer, simp)+
+lemma word_of_int_not_numeral_eq [simp]:
+ \<open>(word_of_int (NOT (numeral bin)) :: 'a::len word) = - numeral bin - 1\<close>
+ by transfer (simp add: not_eq_complement)
+
lemma uint_and:
\<open>uint (x AND y) = uint x AND uint y\<close>
by transfer simp
--- a/src/HOL/Map.thy Wed Aug 18 12:33:31 2021 +0200
+++ b/src/HOL/Map.thy Wed Aug 25 21:43:43 2021 +0200
@@ -765,7 +765,7 @@
unfolding graph_eq_to_snd_dom finite_dom_map_of
using finite_dom_map_of by blast
-lemma graph_map_of_if_distinct_ran: "distinct (map fst al) \<Longrightarrow> graph (map_of al) = set al"
+lemma graph_map_of_if_distinct_dom: "distinct (map fst al) \<Longrightarrow> graph (map_of al) = set al"
unfolding graph_def by auto
lemma finite_graph_iff_finite_dom[simp]: "finite (graph m) = finite (dom m)"
--- a/src/HOL/SPARK/Tools/fdl_lexer.ML Wed Aug 18 12:33:31 2021 +0200
+++ b/src/HOL/SPARK/Tools/fdl_lexer.ML Wed Aug 25 21:43:43 2021 +0200
@@ -82,7 +82,7 @@
fun symbol (x : string, _ : Position.T) = x;
fun explode_pos s pos = fst (fold_map (fn x => fn pos =>
- ((x, pos), Position.advance x pos)) (raw_explode s) pos);
+ ((x, pos), Position.symbol x pos)) (raw_explode s) pos);
(** scanners **)
--- a/src/HOL/Tools/ATP/atp_problem.ML Wed Aug 18 12:33:31 2021 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Wed Aug 25 21:43:43 2021 +0200
@@ -101,6 +101,7 @@
val tptp_empty_list : string
val tptp_unary_builtins : string list
val tptp_binary_builtins : string list
+ val tptp_ternary_builtins : string list
val dfg_individual_type : string
val isabelle_info_prefix : string
val isabelle_info : bool -> string -> int -> (string, 'a) atp_term list
@@ -266,6 +267,7 @@
val tptp_unary_builtins = [tptp_not]
val tptp_binary_builtins =
[tptp_and, tptp_or, tptp_implies, tptp_if, tptp_iff, tptp_not_iff, tptp_equal]
+val tptp_ternary_builtins = [tptp_ite]
val dfg_individual_type = "iii" (* cannot clash *)
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Aug 18 12:33:31 2021 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Aug 25 21:43:43 2021 +0200
@@ -1528,7 +1528,8 @@
(make_fixed_const NONE \<^const_name>\<open>undefined\<close>, mk_sym_info false 0) ::
(map (rpair (mk_sym_info true 0)) [tptp_false, tptp_true]) @
(map (rpair (mk_sym_info true 1)) tptp_unary_builtins) @
- (map (rpair (mk_sym_info true 2)) (tptp_old_equal :: tptp_binary_builtins))
+ (map (rpair (mk_sym_info true 2)) (tptp_old_equal :: tptp_binary_builtins)) @
+ (map (rpair (mk_sym_info true 3)) tptp_ternary_builtins)
|> not (is_type_enc_fool type_enc orelse is_type_enc_full_higher_order type_enc)
? cons (prefixed_predicator_name, mk_sym_info true 1)
end
--- a/src/Pure/Concurrent/future.ML Wed Aug 18 12:33:31 2021 +0200
+++ b/src/Pure/Concurrent/future.ML Wed Aug 25 21:43:43 2021 +0200
@@ -407,7 +407,7 @@
fun error_message pos ((serial, msg), exec_id) =
Position.setmp_thread_data pos (fn () =>
- let val id = Position.get_id pos in
+ let val id = Position.id_of pos in
if is_none id orelse is_none exec_id orelse id = exec_id
then Output.error_message' (serial, msg) else ()
end) ();
@@ -415,7 +415,7 @@
fun identify_result pos res =
res |> Exn.map_exn (fn exn =>
let val exec_id =
- (case Position.get_id pos of
+ (case Position.id_of pos of
NONE => []
| SOME id => [(Markup.exec_idN, id)])
in Par_Exn.identify exec_id exn end);
--- a/src/Pure/General/name_space.ML Wed Aug 18 12:33:31 2021 +0200
+++ b/src/Pure/General/name_space.ML Wed Aug 25 21:43:43 2021 +0200
@@ -112,7 +112,7 @@
serial: serial};
fun entry_markup def kind (name, {pos, serial, ...}: entry) =
- Markup.properties (Position.entity_properties_of def serial pos) (Markup.entity kind name);
+ Position.make_entity_markup def serial kind (name, pos);
fun print_entry_ref kind (name, entry) =
quote (Markup.markup (entry_markup false kind (name, entry)) name);
--- a/src/Pure/General/position.ML Wed Aug 18 12:33:31 2021 +0200
+++ b/src/Pure/General/position.ML Wed Aug 25 21:43:43 2021 +0200
@@ -1,7 +1,9 @@
(* Title: Pure/General/position.ML
- Author: Markus Wenzel, TU Muenchen
+ Author: Makarius
-Source positions: counting Isabelle symbols, starting from 1.
+Source positions starting from 1; values <= 0 mean "absent". Count Isabelle
+symbols, not UTF8 bytes nor UTF16 characters. Position range specifies a
+right-open interval offset .. end_offset (exclusive).
*)
signature POSITION =
@@ -14,8 +16,9 @@
val offset_of: T -> int option
val end_offset_of: T -> int option
val file_of: T -> string option
- val advance: Symbol.symbol -> T -> T
- val advance_offsets: int -> T -> T
+ val id_of: T -> string option
+ val symbol: Symbol.symbol -> T -> T
+ val symbol_explode: string -> T -> T
val distance_of: T * T -> int option
val none: T
val start: T
@@ -28,18 +31,18 @@
val get_props: T -> Properties.T
val id: string -> T
val id_only: string -> T
- val get_id: T -> string option
val put_id: string -> T -> T
val copy_id: T -> T -> T
val id_properties_of: T -> Properties.T
val parse_id: T -> int option
+ val advance_offsets: int -> T -> T
val adjust_offsets: (int -> int option) -> T -> T
val of_properties: Properties.T -> T
val properties_of: T -> Properties.T
val offset_properties_of: T -> Properties.T
val def_properties_of: T -> Properties.T
val entity_markup: string -> string * T -> Markup.T
- val entity_properties_of: bool -> serial -> T -> Properties.T
+ val make_entity_markup: bool -> serial -> string -> string * T -> Markup.T
val markup: T -> Markup.T -> Markup.T
val is_reported: T -> bool
val is_reported_range: T -> bool
@@ -73,7 +76,8 @@
(* datatype position *)
-datatype T = Pos of (int * int * int) * Properties.T;
+type count = int * int * int;
+datatype T = Pos of count * Properties.T;
fun dest2 f = apply2 (fn Pos p => f p);
@@ -92,37 +96,34 @@
fun dest (Pos ((i, j, k), props)) = {line = i, offset = j, end_offset = k, props = props};
fun valid (i: int) = i > 0;
+val invalid = not o valid;
+fun maybe_valid i = if valid i then SOME i else NONE;
fun if_valid i i' = if valid i then i' else i;
(* fields *)
-fun line_of (Pos ((i, _, _), _)) = if valid i then SOME i else NONE;
-fun offset_of (Pos ((_, j, _), _)) = if valid j then SOME j else NONE;
-fun end_offset_of (Pos ((_, _, k), _)) = if valid k then SOME k else NONE;
+fun line_of (Pos ((i, _, _), _)) = maybe_valid i;
+fun offset_of (Pos ((_, j, _), _)) = maybe_valid j;
+fun end_offset_of (Pos ((_, _, k), _)) = maybe_valid k;
fun file_of (Pos (_, props)) = Properties.get props Markup.fileN;
+fun id_of (Pos (_, props)) = Properties.get props Markup.idN;
-(* advance *)
+(* count position *)
-fun advance_count "\n" (i: int, j: int, k: int) =
+fun count_symbol "\n" ((i, j, k): count) =
(if_valid i (i + 1), if_valid j (j + 1), k)
- | advance_count s (i, j, k) =
- if Symbol.not_eof s then (i, if_valid j (j + 1), k)
- else (i, j, k);
+ | count_symbol s (i, j, k) =
+ if Symbol.not_eof s then (i, if_valid j (j + 1), k) else (i, j, k);
-fun invalid_count (i, j, _: int) =
- not (valid i orelse valid j);
-
-fun advance sym (pos as (Pos (count, props))) =
- if invalid_count count then pos else Pos (advance_count sym count, props);
+fun count_invalid ((i, j, _): count) = invalid i andalso invalid j;
-fun advance_offsets offset (pos as (Pos (count as (i, j, k), props))) =
- if offset = 0 orelse invalid_count count then pos
- else if offset < 0 then raise Fail "Illegal offset"
- else if valid i then raise Fail "Illegal line position"
- else Pos ((i, if_valid j (j + offset), if_valid k (k + offset)), props);
+fun symbol sym (pos as (Pos (count, props))) =
+ if count_invalid count then pos else Pos (count_symbol sym count, props);
+
+val symbol_explode = fold symbol o Symbol.explode;
(* distance of adjacent positions *)
@@ -152,17 +153,25 @@
fun id id = Pos ((0, 1, 0), [(Markup.idN, id)]);
fun id_only id = Pos ((0, 0, 0), [(Markup.idN, id)]);
-fun get_id (Pos (_, props)) = Properties.get props Markup.idN;
fun put_id id (Pos (count, props)) = Pos (count, norm_props (Properties.put (Markup.idN, id) props));
-fun copy_id pos = (case get_id pos of NONE => I | SOME id => put_id id);
+fun copy_id pos = (case id_of pos of NONE => I | SOME id => put_id id);
-fun parse_id pos = Option.map Value.parse_int (get_id pos);
+fun parse_id pos = Option.map Value.parse_int (id_of pos);
fun id_properties_of pos =
- (case get_id pos of
+ (case id_of pos of
SOME id => [(Markup.idN, id)]
| NONE => []);
+
+(* adjust offsets *)
+
+fun advance_offsets offset (pos as (Pos (count as (i, j, k), props))) =
+ if offset = 0 orelse count_invalid count then pos
+ else if offset < 0 then raise Fail "Illegal offset"
+ else if valid i then raise Fail "Illegal line position"
+ else Pos ((i, if_valid j (j + offset), if_valid k (k + offset)), props);
+
fun adjust_offsets adjust (pos as Pos (_, props)) =
if is_none (file_of pos) then
(case parse_id pos of
@@ -178,40 +187,47 @@
(* markup properties *)
-fun get props name =
+fun get_int props name =
(case Properties.get props name of
NONE => 0
| SOME s => Value.parse_int s);
fun of_properties props =
- make {line = get props Markup.lineN,
- offset = get props Markup.offsetN,
- end_offset = get props Markup.end_offsetN,
+ make {
+ line = get_int props Markup.lineN,
+ offset = get_int props Markup.offsetN,
+ end_offset = get_int props Markup.end_offsetN,
props = props};
-fun value k i = if valid i then [(k, Value.print_int i)] else [];
+fun int_entry k i = if invalid i then [] else [(k, Value.print_int i)];
fun properties_of (Pos ((i, j, k), props)) =
- value Markup.lineN i @ value Markup.offsetN j @ value Markup.end_offsetN k @ props;
+ int_entry Markup.lineN i @
+ int_entry Markup.offsetN j @
+ int_entry Markup.end_offsetN k @ props;
fun offset_properties_of (Pos ((_, j, k), _)) =
- value Markup.offsetN j @ value Markup.end_offsetN k;
+ int_entry Markup.offsetN j @
+ int_entry Markup.end_offsetN k;
-val def_properties_of = properties_of #> map (fn (x, y) => ("def_" ^ x, y));
+val def_properties_of = properties_of #> map (apfst Markup.def_name);
fun entity_markup kind (name, pos) =
Markup.entity kind name |> Markup.properties (def_properties_of pos);
-fun entity_properties_of def serial pos =
- if def then (Markup.defN, Value.print_int serial) :: properties_of pos
- else (Markup.refN, Value.print_int serial) :: def_properties_of pos;
+fun make_entity_markup def serial kind (name, pos) =
+ let
+ val props =
+ if def then (Markup.defN, Value.print_int serial) :: properties_of pos
+ else (Markup.refN, Value.print_int serial) :: def_properties_of pos;
+ in Markup.entity kind name |> Markup.properties props end;
val markup = Markup.properties o properties_of;
(* reports *)
-fun is_reported pos = is_some (offset_of pos) andalso is_some (get_id pos);
+fun is_reported pos = is_some (offset_of pos) andalso is_some (id_of pos);
fun is_reported_range pos = is_reported pos andalso is_some (end_offset_of pos);
fun reported_text pos m txt = if is_reported pos then Markup.markup (markup pos m) txt else "";
@@ -271,14 +287,14 @@
let
val pos = of_properties props;
val pos' =
- make {line = get props Markup.end_lineN,
- offset = get props Markup.end_offsetN,
+ make {line = get_int props Markup.end_lineN,
+ offset = get_int props Markup.end_offsetN,
end_offset = 0,
props = props};
in (pos, pos') end;
fun properties_of_range (pos, pos') =
- properties_of pos @ value Markup.end_lineN (the_default 0 (line_of pos'));
+ properties_of pos @ int_entry Markup.end_lineN (the_default 0 (line_of pos'));
(* thread data *)
--- a/src/Pure/General/symbol_explode.ML Wed Aug 18 12:33:31 2021 +0200
+++ b/src/Pure/General/symbol_explode.ML Wed Aug 25 21:43:43 2021 +0200
@@ -18,13 +18,12 @@
fun explode string =
let
fun char i = String.sub (string, i);
- fun string_range i j = String.substring (string, i, j - i);
+ fun substring i j = String.substring (string, i, j - i);
val n = size string;
fun test pred i = i < n andalso pred (char i);
fun many pred i = if test pred i then many pred (i + 1) else i;
- fun maybe pred i = if test pred i then i + 1 else i;
- fun maybe_char c = maybe (fn c' => c = c');
+ fun maybe_char c i = if test (fn c' => c = c') i then i + 1 else i;
fun maybe_ascii_id i = if test is_ascii_letter i then many is_ascii_letdig (i + 1) else i;
fun scan i =
@@ -39,11 +38,11 @@
(*utf8*)
else if is_utf8 ch then
let val j = many is_utf8_trailer (i + 1)
- in string_range i j :: scan j end
+ in substring i j :: scan j end
(*named symbol*)
else if ch = #"\\" andalso test (fn c => c = #"<") (i + 1) then
let val j = (i + 2) |> maybe_char #"^" |> maybe_ascii_id |> maybe_char #">"
- in string_range i j :: scan j end
+ in substring i j :: scan j end
(*single character*)
else String.str ch :: scan (i + 1)
end
--- a/src/Pure/General/symbol_pos.ML Wed Aug 18 12:33:31 2021 +0200
+++ b/src/Pure/General/symbol_pos.ML Wed Aug 25 21:43:43 2021 +0200
@@ -40,7 +40,7 @@
type text = string
val implode: T list -> text
val implode_range: Position.range -> T list -> text * Position.range
- val explode_delete: text * Position.T -> T list * Position.T list
+ val explode_deleted: string * Position.T -> Position.T list
val explode: text * Position.T -> T list
val explode0: string -> T list
val scan_ident: T list scanner
@@ -62,7 +62,7 @@
val content = implode o map symbol;
fun range (syms as (_, pos) :: _) =
- let val pos' = List.last syms |-> Position.advance
+ let val pos' = List.last syms |-> Position.symbol
in Position.range (pos, pos') end
| range [] = Position.no_range;
@@ -75,7 +75,7 @@
val is_eof = Symbol.is_eof o symbol;
val stopper =
- Scan.stopper (fn [] => eof | inp => mk_eof (List.last inp |-> Position.advance)) is_eof;
+ Scan.stopper (fn [] => eof | inp => mk_eof (List.last inp |-> Position.symbol)) is_eof;
(* basic scanners *)
@@ -233,7 +233,7 @@
fun source pos =
Source.source' pos Symbol.stopper (Scan.bulk (Scan.depend (fn pos =>
- Scan.one Symbol.not_eof >> (fn s => (Position.advance s pos, (s, pos))))));
+ Scan.one Symbol.not_eof >> (fn s => (Position.symbol s pos, (s, pos))))));
(* compact representation -- with Symbol.DEL padding *)
@@ -244,7 +244,7 @@
| pad [(s, _)] = [s]
| pad ((s1, pos1) :: (rest as (_, pos2) :: _)) =
let
- val end_pos1 = Position.advance s1 pos1;
+ val end_pos1 = Position.symbol s1 pos1;
val d = Int.max (0, the_default 0 (Position.distance_of (end_pos1, pos2)));
in s1 :: replicate d Symbol.DEL @ pad rest end;
@@ -254,19 +254,25 @@
let val syms' = (("", pos1) :: syms @ [("", pos2)])
in (implode syms', range syms') end;
-fun explode_delete (str, pos) =
- let
- val (res, _) =
- fold (fn s => fn (res, p) => ((s, p) :: res, Position.advance s p))
- (Symbol.explode str) ([], Position.no_range_position pos);
- in
- fold (fn (s, p) => if s = Symbol.DEL then apsnd (cons p) else apfst (cons (s, p)))
- res ([], [])
- end;
+local
+
+fun rev_explode (str, pos) =
+ fold (fn s => fn (res, p) => ((s, p) :: res, Position.symbol s p))
+ (Symbol.explode str) ([], Position.no_range_position pos)
+ |> #1;
+
+in
-val explode = explode_delete #> #1;
+fun explode_deleted arg =
+ fold (fn (s, p) => s = Symbol.DEL ? cons p) (rev_explode arg) [];
+
+fun explode arg =
+ fold (fn (s, p) => s <> Symbol.DEL ? cons (s, p)) (rev_explode arg) [];
+
fun explode0 str = explode (str, Position.none);
+end;
+
(* identifiers *)
--- a/src/Pure/General/time.scala Wed Aug 18 12:33:31 2021 +0200
+++ b/src/Pure/General/time.scala Wed Aug 25 21:43:43 2021 +0200
@@ -14,8 +14,8 @@
object Time
{
def seconds(s: Double): Time = new Time((s * 1000.0).round)
- def minutes(s: Double): Time = new Time((s * 60000.0).round)
- def ms(m: Long): Time = new Time(m)
+ def minutes(m: Double): Time = new Time((m * 60000.0).round)
+ def ms(ms: Long): Time = new Time(ms)
def hms(h: Int, m: Int, s: Double): Time = seconds(s + 60 * m + 3600 * h)
def now(): Time = ms(System.currentTimeMillis())
--- a/src/Pure/General/timing.ML Wed Aug 18 12:33:31 2021 +0200
+++ b/src/Pure/General/timing.ML Wed Aug 25 21:43:43 2021 +0200
@@ -1,7 +1,7 @@
(* Title: Pure/General/timing.ML
Author: Makarius
-Basic support for time measurement.
+Support for time measurement.
*)
signature BASIC_TIMING =
--- a/src/Pure/Isar/attrib.ML Wed Aug 18 12:33:31 2021 +0200
+++ b/src/Pure/Isar/attrib.ML Wed Aug 25 21:43:43 2021 +0200
@@ -602,6 +602,7 @@
register_config_bool Thm.show_consts #>
register_config_bool Thm.show_hyps #>
register_config_bool Thm.show_tags #>
+ register_config_bool Proof_Display.show_results #>
register_config_bool Pattern.unify_trace_failure #>
register_config_int Unify.trace_bound #>
register_config_int Unify.search_bound #>
--- a/src/Pure/Isar/calculation.ML Wed Aug 18 12:33:31 2021 +0200
+++ b/src/Pure/Isar/calculation.ML Wed Aug 25 21:43:43 2021 +0200
@@ -68,8 +68,7 @@
fun report def serial pos =
Context_Position.report (Proof.context_of state)
(Position.thread_data ())
- (Markup.entity calculationN ""
- |> Markup.properties (Position.entity_properties_of def serial pos));
+ (Position.make_entity_markup def serial calculationN ("", pos));
val calculation =
(case calc of
NONE => NONE
--- a/src/Pure/Isar/keyword.ML Wed Aug 18 12:33:31 2021 +0200
+++ b/src/Pure/Isar/keyword.ML Wed Aug 25 21:43:43 2021 +0200
@@ -216,8 +216,7 @@
fun command_markup keywords name =
lookup_command keywords name
|> Option.map (fn {pos, id, ...} =>
- Markup.properties (Position.entity_properties_of false id pos)
- (Markup.entity Markup.command_keywordN name));
+ Position.make_entity_markup false id Markup.command_keywordN (name, pos));
fun command_kind keywords = Option.map #kind o lookup_command keywords;
--- a/src/Pure/Isar/outer_syntax.ML Wed Aug 18 12:33:31 2021 +0200
+++ b/src/Pure/Isar/outer_syntax.ML Wed Aug 25 21:43:43 2021 +0200
@@ -65,8 +65,7 @@
fun command_pos (Command {pos, ...}) = pos;
fun command_markup def (name, Command {pos, id, ...}) =
- Markup.properties (Position.entity_properties_of def id pos)
- (Markup.entity Markup.commandN name);
+ Position.make_entity_markup def id Markup.commandN (name, pos);
fun pretty_command (cmd as (name, Command {comment, ...})) =
Pretty.block
--- a/src/Pure/Isar/proof_display.ML Wed Aug 18 12:33:31 2021 +0200
+++ b/src/Pure/Isar/proof_display.ML Wed Aug 25 21:43:43 2021 +0200
@@ -22,6 +22,7 @@
val pretty_goal_facts: Proof.context -> string -> thm list -> Pretty.T
val method_error: string -> Position.T ->
{context: Proof.context, facts: thm list, goal: thm} -> 'a Seq.result
+ val show_results: bool Config.T
val print_results: bool -> Position.T -> Proof.context ->
((string * string) * (string * thm list) list) -> unit
val print_consts: bool -> Position.T -> Proof.context ->
@@ -263,6 +264,14 @@
fun position_markup pos = Pretty.mark (Position.markup pos Markup.position);
+val interactive =
+ Config.declare_bool ("interactive", \<^here>) (K false);
+
+val show_results =
+ Config.declare_bool ("show_results", \<^here>) (fn context => Config.get_generic context interactive);
+
+fun no_print int ctxt = not (Config.get (Config.put interactive int ctxt) show_results);
+
local
fun pretty_fact_name pos (kind, "") = position_markup pos (Pretty.keyword1 kind)
@@ -276,8 +285,8 @@
in
-fun print_results do_print pos ctxt ((kind, name), facts) =
- if not do_print orelse kind = "" then ()
+fun print_results int pos ctxt ((kind, name), facts) =
+ if kind = "" orelse no_print int ctxt then ()
else if name = "" then
(Output.state o Pretty.string_of)
(Pretty.block (position_markup pos (Pretty.keyword1 kind) :: Pretty.brk 1 ::
@@ -315,8 +324,8 @@
in
-fun print_consts do_print pos ctxt pred cs =
- if not do_print orelse null cs then ()
+fun print_consts int pos ctxt pred cs =
+ if null cs orelse no_print int ctxt then ()
else Output.state (Pretty.string_of (pretty_consts pos ctxt pred cs));
end;
--- a/src/Pure/Isar/token.ML Wed Aug 18 12:33:31 2021 +0200
+++ b/src/Pure/Isar/token.ML Wed Aug 25 21:43:43 2021 +0200
@@ -338,8 +338,8 @@
let
val pos = pos_of tok;
val (m, text) = token_kind_markup (kind_of tok);
- val delete = #2 (Symbol_Pos.explode_delete (source_of tok, pos));
- in ((pos, m), text) :: map (fn p => ((p, Markup.delete), "")) delete end;
+ val deleted = Symbol_Pos.explode_deleted (source_of tok, pos);
+ in ((pos, m), text) :: map (fn p => ((p, Markup.delete), "")) deleted end;
fun markups keywords = map (#2 o #1) o reports keywords;
@@ -381,7 +381,7 @@
fun file_source (file: file) =
let
val text = cat_lines (#lines file);
- val end_pos = fold Position.advance (Symbol.explode text) (#pos file);
+ val end_pos = Position.symbol_explode text (#pos file);
in Input.source true text (Position.range (#pos file, end_pos)) end;
fun get_files (Token (_, _, Value (SOME (Files files)))) = files
--- a/src/Pure/ML/ml_antiquotations2.ML Wed Aug 18 12:33:31 2021 +0200
+++ b/src/Pure/ML/ml_antiquotations2.ML Wed Aug 25 21:43:43 2021 +0200
@@ -9,12 +9,11 @@
val _ = Theory.setup
(ML_Antiquotation.inline_embedded \<^binding>\<open>method\<close>
- (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, (name, pos)) =>
- ML_Syntax.print_string (Method.check_name ctxt (name, pos)))) #>
+ (Args.context -- Scan.lift Args.embedded_position >>
+ (ML_Syntax.print_string o uncurry Method.check_name)) #>
ML_Antiquotation.inline_embedded \<^binding>\<open>locale\<close>
- (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, (name, pos)) =>
- Locale.check (Proof_Context.theory_of ctxt) (name, pos)
- |> ML_Syntax.print_string)));
+ (Args.theory -- Scan.lift Args.embedded_position >>
+ (ML_Syntax.print_string o uncurry Locale.check)));
end;
--- a/src/Pure/ML/ml_lex.ML Wed Aug 18 12:33:31 2021 +0200
+++ b/src/Pure/ML/ml_lex.ML Wed Aug 25 21:43:43 2021 +0200
@@ -333,8 +333,8 @@
if null syms then []
else
let
- val pos1 = List.last syms |-> Position.advance;
- val pos2 = Position.advance Symbol.space pos1;
+ val pos1 = List.last syms |-> Position.symbol;
+ val pos2 = Position.symbol Symbol.space pos1;
in [Antiquote.Text (Token (Position.range (pos1, pos2), (Space, Symbol.space)))] end;
fun check (Antiquote.Text tok) =
--- a/src/Pure/PIDE/command.ML Wed Aug 18 12:33:31 2021 +0200
+++ b/src/Pure/PIDE/command.ML Wed Aug 25 21:43:43 2021 +0200
@@ -95,7 +95,7 @@
let
val file_pos =
Position.file file_node |>
- (case Position.get_id (Position.thread_data ()) of
+ (case Position.id_of (Position.thread_data ()) of
NONE => I
| SOME exec_id => Position.put_id exec_id);
in {src_path = src_path, lines = lines, digest = digest, pos = file_pos} end
--- a/src/Pure/PIDE/document.ML Wed Aug 18 12:33:31 2021 +0200
+++ b/src/Pure/PIDE/document.ML Wed Aug 25 21:43:43 2021 +0200
@@ -132,7 +132,7 @@
if null errors then ()
else
cat_lines errors |>
- (case Position.get_id (Position.thread_data ()) of
+ (case Position.id_of (Position.thread_data ()) of
NONE => I
| SOME id => Protocol_Message.command_positions_yxml id)
|> error;
--- a/src/Pure/PIDE/markup.ML Wed Aug 18 12:33:31 2021 +0200
+++ b/src/Pure/PIDE/markup.ML Wed Aug 25 21:43:43 2021 +0200
@@ -60,9 +60,10 @@
val end_offsetN: string
val fileN: string
val idN: string
+ val positionN: string val position: T
val position_properties: string list
val position_property: Properties.entry -> bool
- val positionN: string val position: T
+ val def_name: string -> string
val expressionN: string val expression: string -> T
val citationN: string val citation: string -> T
val pathN: string val path: string -> T
@@ -394,10 +395,22 @@
val fileN = "file";
val idN = "id";
+val (positionN, position) = markup_elem "position";
+
val position_properties = [lineN, offsetN, end_offsetN, fileN, idN];
fun position_property (entry: Properties.entry) = member (op =) position_properties (#1 entry);
-val (positionN, position) = markup_elem "position";
+
+(* position "def" names *)
+
+fun make_def a = "def_" ^ a;
+
+val def_names = Symtab.make (map (fn a => (a, make_def a)) position_properties);
+
+fun def_name a =
+ (case Symtab.lookup def_names a of
+ SOME b => b
+ | NONE => make_def a);
(* expression *)
--- a/src/Pure/PIDE/markup.scala Wed Aug 18 12:33:31 2021 +0200
+++ b/src/Pure/PIDE/markup.scala Wed Aug 25 21:43:43 2021 +0200
@@ -159,10 +159,19 @@
val DEF_FILE = "def_file"
val DEF_ID = "def_id"
+ val POSITION = "position"
+
val POSITION_PROPERTIES = Set(LINE, OFFSET, END_OFFSET, FILE, ID)
def position_property(entry: Properties.Entry): Boolean = POSITION_PROPERTIES(entry._1)
- val POSITION = "position"
+
+ /* position "def" name */
+
+ private val def_names: Map[String, String] =
+ Map(LINE -> DEF_LINE, OFFSET -> DEF_OFFSET, END_OFFSET -> DEF_END_OFFSET,
+ FILE -> DEF_FILE, ID -> DEF_ID)
+
+ def def_name(a: String): String = def_names.getOrElse(a, a + "def_")
/* expression */
--- a/src/Pure/PIDE/resources.ML Wed Aug 18 12:33:31 2021 +0200
+++ b/src/Pure/PIDE/resources.ML Wed Aug 25 21:43:43 2021 +0200
@@ -168,8 +168,7 @@
fun check_session ctxt arg =
Completion.check_item "session"
(fn (name, {pos, serial}) =>
- Markup.entity Markup.sessionN name
- |> Markup.properties (Position.entity_properties_of false serial pos))
+ Position.make_entity_markup false serial Markup.sessionN (name, pos))
(get_session_base1 #session_positions) ctxt arg;
fun session_chapter name =
--- a/src/Pure/Pure.thy Wed Aug 18 12:33:31 2021 +0200
+++ b/src/Pure/Pure.thy Wed Aug 25 21:43:43 2021 +0200
@@ -134,7 +134,7 @@
val _ =
(lines, pos0) |-> fold (fn line => fn pos1 =>
let
- val pos2 = pos1 |> fold Position.advance (Symbol.explode line);
+ val pos2 = Position.symbol_explode line pos1;
val range = Position.range (pos1, pos2);
val source = Input.source true line range;
val _ =
@@ -144,7 +144,7 @@
else
(ignore (Resources.check_session_dir ctxt (SOME dir) source)
handle ERROR msg => Output.error_message msg);
- in pos2 |> Position.advance "\n" end);
+ in pos2 |> Position.symbol "\n" end);
in thy' end)));
val _ =
--- a/src/Pure/Syntax/syntax_phases.ML Wed Aug 18 12:33:31 2021 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML Wed Aug 25 21:43:43 2021 +0200
@@ -60,10 +60,7 @@
fun markup_var xi = [Markup.name (Term.string_of_vname xi) Markup.var];
fun markup_bound def ps (name, id) =
- let val entity = Markup.entity Markup.boundN name in
- Markup.bound ::
- map (fn pos => Markup.properties (Position.entity_properties_of def id pos) entity) ps
- end;
+ Markup.bound :: map (fn pos => Position.make_entity_markup def id Markup.boundN (name, pos)) ps;
fun markup_entity ctxt c =
(case Syntax.lookup_const (Proof_Context.syn_of ctxt) c of
@@ -84,7 +81,7 @@
| reports_of_scope (def_pos :: ps) =
let
val id = serial ();
- fun entity def = (Markup.entityN, Position.entity_properties_of def id def_pos);
+ fun entity def = Position.make_entity_markup def id "" ("", def_pos);
in
map (rpair Markup.bound) (def_pos :: ps) @
((def_pos, entity true) :: map (rpair (entity false)) ps)
--- a/src/Pure/System/bash.ML Wed Aug 18 12:33:31 2021 +0200
+++ b/src/Pure/System/bash.ML Wed Aug 25 21:43:43 2021 +0200
@@ -1,7 +1,7 @@
(* Title: Pure/System/bash.ML
Author: Makarius
-Syntax for GNU bash.
+Support for GNU bash.
*)
signature BASH =
--- a/src/Pure/System/bash.scala Wed Aug 18 12:33:31 2021 +0200
+++ b/src/Pure/System/bash.scala Wed Aug 25 21:43:43 2021 +0200
@@ -1,7 +1,8 @@
/* Title: Pure/System/bash.scala
Author: Makarius
-GNU bash processes, with propagation of interrupts.
+Support for GNU bash: portable external processes with propagation of
+interrupts.
*/
package isabelle
--- a/src/Pure/System/options.ML Wed Aug 18 12:33:31 2021 +0200
+++ b/src/Pure/System/options.ML Wed Aug 25 21:43:43 2021 +0200
@@ -26,7 +26,8 @@
val put_string: string -> string -> T -> T
val declare: {pos: Position.T, name: string, typ: string, value: string} -> T -> T
val update: string -> string -> T -> T
- val decode: XML.body -> T
+ val encode: T XML.Encode.T
+ val decode: T XML.Decode.T
val default: unit -> T
val default_typ: string -> string
val default_bool: string -> bool
@@ -150,15 +151,24 @@
in options' end;
-(* decode *)
+(* XML data *)
-fun decode_opt body =
- let open XML.Decode
- in list (pair properties (pair string (pair string string))) end body
- |> map (fn (props, (name, (typ, value))) =>
- {pos = Position.of_properties props, name = name, typ = typ, value = value});
+fun encode (Options tab) =
+ let
+ val opts =
+ (tab, []) |-> Symtab.fold (fn (name, {pos, typ, value}) =>
+ cons (Position.properties_of pos, (name, (typ, value))));
+ open XML.Encode;
+ in list (pair properties (pair string (pair string string))) opts end;
-fun decode body = fold declare (decode_opt body) empty;
+fun decode body =
+ let
+ open XML.Decode;
+ val decode_options =
+ list (pair properties (pair string (pair string string)))
+ #> map (fn (props, (name, (typ, value))) =>
+ {pos = Position.of_properties props, name = name, typ = typ, value = value});
+ in fold declare (decode_options body) empty end;
--- a/src/Pure/Thy/export.ML Wed Aug 18 12:33:31 2021 +0200
+++ b/src/Pure/Thy/export.ML Wed Aug 25 21:43:43 2021 +0200
@@ -36,7 +36,7 @@
fun export_params ({theory = thy, binding, executable, compress, strict}: params) body =
(report_export thy binding;
(Output.try_protocol_message o Markup.export)
- {id = Position.get_id (Position.thread_data ()),
+ {id = Position.id_of (Position.thread_data ()),
serial = serial (),
theory_name = Context.theory_long_name thy,
name = Path.implode_binding (tap Path.proper_binding binding),
--- a/src/Pure/theory.ML Wed Aug 18 12:33:31 2021 +0200
+++ b/src/Pure/theory.ML Wed Aug 25 21:43:43 2021 +0200
@@ -120,9 +120,7 @@
fun theory_markup def name id pos =
if id = 0 then Markup.empty
- else
- Markup.properties (Position.entity_properties_of def id pos)
- (Markup.entity Markup.theoryN name);
+ else Position.make_entity_markup def id Markup.theoryN (name, pos);
fun init_markup (name, pos) thy =
let
--- a/src/Tools/Haskell/Haskell.thy Wed Aug 18 12:33:31 2021 +0200
+++ b/src/Tools/Haskell/Haskell.thy Wed Aug 25 21:43:43 2021 +0200
@@ -210,7 +210,8 @@
Basic library of Isabelle idioms.
-See also \<^file>\<open>$ISABELLE_HOME/src/Pure/General/basics.ML\<close>, \<^file>\<open>$ISABELLE_HOME/src/Pure/library.ML\<close>.
+See \<^file>\<open>$ISABELLE_HOME/src/Pure/General/basics.ML\<close>
+and \<^file>\<open>$ISABELLE_HOME/src/Pure/library.ML\<close>.
-}
{-# LANGUAGE OverloadedStrings #-}
@@ -221,14 +222,12 @@
module Isabelle.Library (
(|>), (|->), (#>), (#->),
- the, the_default,
-
fold, fold_rev, single, map_index, get_index, separate,
StringLike, STRING (..), TEXT (..), BYTES (..),
show_bytes, show_text,
- proper_string, quote, space_implode, commas, commas_quote, cat_lines,
+ proper_string, enclose, quote, space_implode, commas, commas_quote, cat_lines,
space_explode, split_lines, trim_line)
where
@@ -258,17 +257,6 @@
(f #-> g) x = x |> f |-> g
-{- options -}
-
-the :: Maybe a -> a
-the (Just x) = x
-the Nothing = error "the Nothing"
-
-the_default :: a -> Maybe a -> a
-the_default x Nothing = x
-the_default _ (Just y) = y
-
-
{- lists -}
fold :: (a -> b -> b) -> [a] -> b -> b
@@ -383,8 +371,11 @@
proper_string :: StringLike a => a -> Maybe a
proper_string s = if s == "" then Nothing else Just s
+enclose :: StringLike a => a -> a -> a -> a
+enclose lpar rpar str = lpar <> str <> rpar
+
quote :: StringLike a => a -> a
-quote s = "\"" <> s <> "\""
+quote = enclose "\"" "\""
space_implode :: StringLike a => a -> [a] -> a
space_implode s = mconcat . separate s
@@ -407,9 +398,40 @@
LICENSE: BSD 3-clause (Isabelle)
Isabelle text symbols.
+
+See \<^file>\<open>$ISABELLE_HOME/src/Pure/General/symbol.ML\<close>
+and \<^file>\<open>$ISABELLE_HOME/src/Pure/General/symbol_explode.ML\<close>.
-}
-module Isabelle.Symbol where
+{-# LANGUAGE OverloadedStrings #-}
+
+module Isabelle.Symbol (
+ Symbol, eof, is_eof, not_eof,
+
+ is_ascii_letter, is_ascii_digit, is_ascii_hex, is_ascii_quasi,
+ is_ascii_blank, is_ascii_line_terminator, is_ascii_letdig,
+ is_ascii_identifier,
+
+ explode
+)
+where
+
+import Data.Word (Word8)
+import qualified Isabelle.Bytes as Bytes
+import Isabelle.Bytes (Bytes)
+
+
+{- type -}
+
+type Symbol = Bytes
+
+eof :: Symbol
+eof = ""
+
+is_eof, not_eof :: Symbol -> Bool
+is_eof = Bytes.null
+not_eof = not . is_eof
+
{- ASCII characters -}
@@ -426,7 +448,7 @@
is_ascii_quasi c = c == '_' || c == '\''
is_ascii_blank :: Char -> Bool
-is_ascii_blank c = c `elem` " \t\n\11\f\r"
+is_ascii_blank c = c `elem` (" \t\n\11\f\r" :: String)
is_ascii_line_terminator :: Char -> Bool
is_ascii_line_terminator c = c == '\r' || c == '\n'
@@ -437,6 +459,62 @@
is_ascii_identifier :: String -> Bool
is_ascii_identifier s =
not (null s) && is_ascii_letter (head s) && all is_ascii_letdig s
+
+
+{- explode symbols: ASCII, UTF8, named -}
+
+is_utf8 :: Word8 -> Bool
+is_utf8 b = b >= 128
+
+is_utf8_trailer :: Word8 -> Bool
+is_utf8_trailer b = 128 <= b && b < 192
+
+is_utf8_control :: Word8 -> Bool
+is_utf8_control b = 128 <= b && b < 160
+
+(|>) :: a -> (a -> b) -> b
+x |> f = f x
+
+explode :: Bytes -> [Symbol]
+explode string = scan 0
+ where
+ byte = Bytes.index string
+ substring i j =
+ if i == j - 1 then Bytes.singleton (byte i)
+ else Bytes.pack (map byte [i .. j - 1])
+
+ n = Bytes.length string
+ test pred i = i < n && pred (byte i)
+ test_char pred i = i < n && pred (Bytes.char (byte i))
+ many pred i = if test pred i then many pred (i + 1) else i
+ maybe_char c i = if test_char (== c) i then i + 1 else i
+ maybe_ascii_id i =
+ if test_char is_ascii_letter i
+ then many (is_ascii_letdig . Bytes.char) (i + 1)
+ else i
+
+ scan i =
+ if i < n then
+ let
+ b = byte i
+ c = Bytes.char b
+ in
+ {-encoded newline-}
+ if c == '\r' then "\n" : scan (maybe_char '\n' (i + 1))
+ {-pseudo utf8: encoded ascii control-}
+ else if b == 192 && test is_utf8_control (i + 1) && not (test is_utf8 (i + 2))
+ then Bytes.singleton (byte (i + 1) - 128) : scan (i + 2)
+ {-utf8-}
+ else if is_utf8 b then
+ let j = many is_utf8_trailer (i + 1)
+ in substring i j : scan j
+ {-named symbol-}
+ else if c == '\\' && test_char (== '<') (i + 1) then
+ let j = (i + 2) |> maybe_char '^' |> maybe_ascii_id |> maybe_char '>'
+ in substring i j : scan j
+ {-single character-}
+ else Bytes.singleton b : scan (i + 1)
+ else []
\<close>
generate_file "Isabelle/Buffer.hs" = \<open>
@@ -446,7 +524,7 @@
Efficient buffer of byte strings.
-See also \<^file>\<open>$ISABELLE_HOME/src/Pure/General/buffer.ML\<close>.
+See \<^file>\<open>$ISABELLE_HOME/src/Pure/General/buffer.ML\<close>.
-}
module Isabelle.Buffer (T, empty, add, content)
@@ -475,7 +553,7 @@
Plain values, represented as string.
-See also \<^file>\<open>$ISABELLE_HOME/src/Pure/General/value.ML\<close>.
+See \<^file>\<open>$ISABELLE_HOME/src/Pure/General/value.ML\<close>.
-}
{-# LANGUAGE OverloadedStrings #-}
@@ -540,7 +618,7 @@
Property lists.
-See also \<^file>\<open>$ISABELLE_HOME/src/Pure/General/properties.ML\<close>.
+See \<^file>\<open>$ISABELLE_HOME/src/Pure/General/properties.ML\<close>.
-}
module Isabelle.Properties (Entry, T, defined, get, get_value, put, remove)
@@ -581,7 +659,7 @@
Quasi-abstract markup elements.
-See also \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/markup.ML\<close>.
+See \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/markup.ML\<close>.
-}
{-# LANGUAGE OverloadedStrings #-}
@@ -597,6 +675,7 @@
completionN, completion, no_completionN, no_completion,
lineN, end_lineN, offsetN, end_offsetN, fileN, idN, positionN, position,
+ position_properties, def_name,
expressionN, expression,
@@ -636,6 +715,8 @@
where
import Prelude hiding (words, error, break)
+import Data.Map.Strict (Map)
+import qualified Data.Map.Strict as Map
import Isabelle.Library
import qualified Isabelle.Properties as Properties
@@ -738,6 +819,24 @@
position :: T
position = markup_elem positionN
+position_properties :: [Bytes]
+position_properties = [lineN, offsetN, end_offsetN, fileN, idN]
+
+
+{- position "def" names -}
+
+make_def :: Bytes -> Bytes
+make_def a = "def_" <> a
+
+def_names :: Map Bytes Bytes
+def_names = Map.fromList $ map (\a -> (a, make_def a)) position_properties
+
+def_name :: Bytes -> Bytes
+def_name a =
+ case Map.lookup a def_names of
+ Just b -> b
+ Nothing -> make_def a
+
{- expression -}
@@ -1090,6 +1189,238 @@
no_output = ("", "")
\<close>
+generate_file "Isabelle/Position.hs" = \<open>
+{- Title: Isabelle/Position.hs
+ Author: Makarius
+ LICENSE: BSD 3-clause (Isabelle)
+
+Source positions starting from 1; values <= 0 mean "absent". Count Isabelle
+symbols, not UTF8 bytes nor UTF16 characters. Position range specifies a
+right-open interval offset .. end_offset (exclusive).
+
+See \<^file>\<open>$ISABELLE_HOME/src/Pure/General/position.ML\<close>.
+-}
+
+{-# LANGUAGE OverloadedStrings #-}
+
+module Isabelle.Position (
+ T, line_of, column_of, offset_of, end_offset_of, file_of, id_of,
+ start, none, put_file, file, file_only, put_id, id, id_only,
+ symbol, symbol_explode, symbol_explode_string, shift_offsets,
+ of_properties, properties_of, def_properties_of, entity_markup, make_entity_markup,
+ Report, Report_Text, is_reported, is_reported_range, here,
+ Range, no_range, no_range_position, range_position, range
+)
+where
+
+import Prelude hiding (id)
+import Data.Maybe (isJust, fromMaybe)
+import Data.Bifunctor (first)
+import qualified Isabelle.Properties as Properties
+import qualified Isabelle.Bytes as Bytes
+import qualified Isabelle.Value as Value
+import Isabelle.Bytes (Bytes)
+import qualified Isabelle.Markup as Markup
+import qualified Isabelle.YXML as YXML
+import Isabelle.Library
+import qualified Isabelle.Symbol as Symbol
+import Isabelle.Symbol (Symbol)
+
+
+{- position -}
+
+data T =
+ Position {
+ _line :: Int,
+ _column :: Int,
+ _offset :: Int,
+ _end_offset :: Int,
+ _file :: Bytes,
+ _id :: Bytes }
+ deriving (Eq, Ord)
+
+valid, invalid :: Int -> Bool
+valid i = i > 0
+invalid = not . valid
+
+maybe_valid :: Int -> Maybe Int
+maybe_valid i = if valid i then Just i else Nothing
+
+if_valid :: Int -> Int -> Int
+if_valid i i' = if valid i then i' else i
+
+
+{- fields -}
+
+line_of, column_of, offset_of, end_offset_of :: T -> Maybe Int
+line_of = maybe_valid . _line
+column_of = maybe_valid . _column
+offset_of = maybe_valid . _offset
+end_offset_of = maybe_valid . _end_offset
+
+file_of :: T -> Maybe Bytes
+file_of = proper_string . _file
+
+id_of :: T -> Maybe Bytes
+id_of = proper_string . _id
+
+
+{- make position -}
+
+start :: T
+start = Position 1 1 1 0 Bytes.empty Bytes.empty
+
+none :: T
+none = Position 0 0 0 0 Bytes.empty Bytes.empty
+
+put_file :: Bytes -> T -> T
+put_file file pos = pos { _file = file }
+
+file :: Bytes -> T
+file file = put_file file start
+
+file_only :: Bytes -> T
+file_only file = put_file file none
+
+put_id :: Bytes -> T -> T
+put_id id pos = pos { _id = id }
+
+id :: Bytes -> T
+id id = put_id id start
+
+id_only :: Bytes -> T
+id_only id = put_id id none
+
+
+{- count position -}
+
+count_line :: Symbol -> Int -> Int
+count_line "\n" line = if_valid line (line + 1)
+count_line _ line = line
+
+count_column :: Symbol -> Int -> Int
+count_column "\n" column = if_valid column 1
+count_column s column = if Symbol.not_eof s then if_valid column (column + 1) else column
+
+count_offset :: Symbol -> Int -> Int
+count_offset s offset = if Symbol.not_eof s then if_valid offset (offset + 1) else offset
+
+symbol :: Symbol -> T -> T
+symbol s pos =
+ pos {
+ _line = count_line s (_line pos),
+ _column = count_column s (_column pos),
+ _offset = count_offset s (_offset pos) }
+
+symbol_explode :: BYTES a => a -> T -> T
+symbol_explode = fold symbol . Symbol.explode . make_bytes
+
+symbol_explode_string :: String -> T -> T
+symbol_explode_string = symbol_explode
+
+
+{- shift offsets -}
+
+shift_offsets :: Int -> T -> T
+shift_offsets shift pos = pos { _offset = offset', _end_offset = end_offset' }
+ where
+ offset = _offset pos
+ end_offset = _end_offset pos
+ offset' = if invalid offset || invalid shift then offset else offset + shift
+ end_offset' = if invalid end_offset || invalid shift then end_offset else end_offset + shift
+
+
+{- markup properties -}
+
+get_string :: Properties.T -> Bytes -> Bytes
+get_string props name = fromMaybe "" (Properties.get_value Just props name)
+
+get_int :: Properties.T -> Bytes -> Int
+get_int props name = fromMaybe 0 (Properties.get_value Value.parse_int props name)
+
+of_properties :: Properties.T -> T
+of_properties props =
+ none {
+ _line = get_int props Markup.lineN,
+ _offset = get_int props Markup.offsetN,
+ _end_offset = get_int props Markup.end_offsetN,
+ _file = get_string props Markup.fileN,
+ _id = get_string props Markup.idN }
+
+string_entry :: Bytes -> Bytes -> Properties.T
+string_entry k s = if Bytes.null s then [] else [(k, s)]
+
+int_entry :: Bytes -> Int -> Properties.T
+int_entry k i = if invalid i then [] else [(k, Value.print_int i)]
+
+properties_of :: T -> Properties.T
+properties_of pos =
+ int_entry Markup.lineN (_line pos) ++
+ int_entry Markup.offsetN (_offset pos) ++
+ int_entry Markup.end_offsetN (_end_offset pos) ++
+ string_entry Markup.fileN (_file pos) ++
+ string_entry Markup.idN (_id pos)
+
+def_properties_of :: T -> Properties.T
+def_properties_of = properties_of #> map (first Markup.def_name)
+
+entity_markup :: Bytes -> (Bytes, T) -> Markup.T
+entity_markup kind (name, pos) =
+ Markup.entity kind name |> Markup.properties (def_properties_of pos)
+
+make_entity_markup :: Bool -> Int -> Bytes -> (Bytes, T) -> Markup.T
+make_entity_markup def serial kind (name, pos) =
+ let
+ props =
+ if def then (Markup.defN, Value.print_int serial) : properties_of pos
+ else (Markup.refN, Value.print_int serial) : def_properties_of pos
+ in Markup.entity kind name |> Markup.properties props
+
+
+{- reports -}
+
+type Report = (T, Markup.T)
+type Report_Text = (Report, Bytes)
+
+is_reported :: T -> Bool
+is_reported pos = isJust (offset_of pos) && isJust (id_of pos)
+
+is_reported_range :: T -> Bool
+is_reported_range pos = is_reported pos && isJust (end_offset_of pos)
+
+
+{- here: user output -}
+
+here :: T -> Bytes
+here pos = if Bytes.null s2 then "" else s1 <> m1 <> s2 <> m2
+ where
+ props = properties_of pos
+ (m1, m2) = YXML.output_markup (Markup.properties props Markup.position)
+ (s1, s2) =
+ case (line_of pos, file_of pos) of
+ (Just i, Nothing) -> (" ", "(line " <> Value.print_int i <> ")")
+ (Just i, Just name) -> (" ", "(line " <> Value.print_int i <> " of " <> quote name <> ")")
+ (Nothing, Just name) -> (" ", "(file " <> quote name <> ")")
+ _ -> if is_reported pos then ("", "\092<^here>") else ("", "")
+
+
+{- range -}
+
+type Range = (T, T)
+
+no_range :: Range
+no_range = (none, none)
+
+no_range_position :: T -> T
+no_range_position pos = pos { _end_offset = 0 }
+
+range_position :: Range -> T
+range_position (pos, pos') = pos { _end_offset = _offset pos' }
+
+range :: Range -> Range
+range (pos, pos') = (range_position (pos, pos'), no_range_position pos')
+\<close>
+
generate_file "Isabelle/XML.hs" = \<open>
{- Title: Isabelle/XML.hs
Author: Makarius
@@ -1097,7 +1428,7 @@
Untyped XML trees and representation of ML values.
-See also \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/xml.ML\<close>.
+See \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/xml.ML\<close>.
-}
{-# LANGUAGE OverloadedStrings #-}
@@ -1185,7 +1516,7 @@
XML as data representation language.
-See also \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/xml.ML\<close>.
+See \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/xml.ML\<close>.
-}
{-# LANGUAGE OverloadedStrings #-}
@@ -1200,6 +1531,8 @@
)
where
+import Data.Maybe (fromJust)
+
import Isabelle.Library
import Isabelle.Bytes (Bytes)
import qualified Isabelle.Value as Value
@@ -1270,7 +1603,7 @@
option f (Just x) = [node (f x)]
variant :: [V a] -> T a
-variant fs x = [tagged (the (get_index (\f -> f x) fs))]
+variant fs x = [tagged (fromJust (get_index (\f -> f x) fs))]
\<close>
generate_file "Isabelle/XML/Decode.hs" = \<open>
@@ -1280,7 +1613,7 @@
XML as data representation language.
-See also \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/xml.ML\<close>.
+See \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/xml.ML\<close>.
-}
{-# LANGUAGE OverloadedStrings #-}
@@ -1395,7 +1728,7 @@
Efficient text representation of XML trees. Suitable for direct
inlining into plain text.
-See also \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/yxml.ML\<close>.
+See \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/yxml.ML\<close>.
-}
{-# LANGUAGE OverloadedStrings #-}
@@ -1534,7 +1867,7 @@
Completion of names.
-See also \<^file>\<open>$ISABELLE_HOME/src/Pure/General/completion.ML\<close>.
+See \<^file>\<open>$ISABELLE_HOME/src/Pure/General/completion.ML\<close>.
-}
{-# LANGUAGE OverloadedStrings #-}
@@ -1591,7 +1924,7 @@
File-system operations.
-See also \<^file>\<open>$ISABELLE_HOME/src/Pure/General/file.ML\<close>.
+See \<^file>\<open>$ISABELLE_HOME/src/Pure/General/file.ML\<close>.
-}
module Isabelle.File (read, write, append) where
@@ -1619,7 +1952,7 @@
Generic pretty printing module.
-See also \<^file>\<open>$ISABELLE_HOME/src/Pure/General/pretty.ML\<close>.
+See \<^file>\<open>$ISABELLE_HOME/src/Pure/General/pretty.ML\<close>.
-}
{-# LANGUAGE OverloadedStrings #-}
@@ -1637,7 +1970,7 @@
import qualified Isabelle.Bytes as Bytes
import Isabelle.Bytes (Bytes)
-import Isabelle.Library hiding (quote, separate, commas)
+import Isabelle.Library hiding (enclose, quote, separate, commas)
import qualified Isabelle.Buffer as Buffer
import qualified Isabelle.Markup as Markup
import qualified Isabelle.XML as XML
@@ -1775,7 +2108,7 @@
Names of basic logical entities (variables etc.).
-See also \<^file>\<open>$ISABELLE_HOME/src/Pure/name.ML\<close>.
+See \<^file>\<open>$ISABELLE_HOME/src/Pure/name.ML\<close>.
-}
{-# LANGUAGE OverloadedStrings #-}
@@ -1870,7 +2203,7 @@
Lambda terms, types, sorts.
-See also \<^file>\<open>$ISABELLE_HOME/src/Pure/term.scala\<close>.
+See \<^file>\<open>$ISABELLE_HOME/src/Pure/term.scala\<close>.
-}
{-# LANGUAGE OverloadedStrings #-}
@@ -1878,7 +2211,7 @@
module Isabelle.Term (
Indexname, Sort, Typ(..), Term(..),
Free, lambda, declare_frees, incr_boundvars, subst_bound, dest_abs, strip_abs,
- type_op0, type_op1, op0, op1, op2, typed_op2, binder,
+ type_op0, type_op1, op0, op1, op2, typed_op1, typed_op2, binder,
dummyS, dummyT, is_dummyT, propT, is_propT, (-->), dest_funT, (--->),
aconv, list_comb, strip_comb, head_of
)
@@ -2012,6 +2345,13 @@
dest (App (App (Const (c, _), t), u)) | c == name = Just (t, u)
dest _ = Nothing
+typed_op1 :: Name -> (Typ -> Term -> Term, Term -> Maybe (Typ, Term))
+typed_op1 name = (mk, dest)
+ where
+ mk ty t = App (Const (name, [ty]), t)
+ dest (App (Const (c, [ty]), t)) | c == name = Just (ty, t)
+ dest _ = Nothing
+
typed_op2 :: Name -> (Typ -> Term -> Term -> Term, Term -> Maybe (Typ, Term, Term))
typed_op2 name = (mk, dest)
where
@@ -2075,19 +2415,23 @@
Support for Isabelle/Pure logic.
-See also \<^file>\<open>$ISABELLE_HOME/src/Pure/logic.ML\<close>.
+See \<^file>\<open>$ISABELLE_HOME/src/Pure/logic.ML\<close>.
-}
{-# LANGUAGE OverloadedStrings #-}
module Isabelle.Pure (
- mk_forall, dest_forall, mk_equals, dest_equals, mk_implies, dest_implies
+ mk_forall_op, dest_forall_op, mk_forall, dest_forall,
+ mk_equals, dest_equals, mk_implies, dest_implies
)
where
import qualified Isabelle.Name as Name
import Isabelle.Term
+mk_forall_op :: Typ -> Term -> Term; dest_forall_op :: Term -> Maybe (Typ, Term)
+(mk_forall_op, dest_forall_op) = typed_op1 \<open>\<^const_name>\<open>Pure.all\<close>\<close>
+
mk_forall :: Free -> Term -> Term; dest_forall :: Name.Context -> Term -> Maybe (Free, Term)
(mk_forall, dest_forall) = binder \<open>\<^const_name>\<open>Pure.all\<close>\<close>
@@ -2105,7 +2449,7 @@
Support for Isabelle/HOL logic.
-See also \<^file>\<open>$ISABELLE_HOME/src/HOL/Tools/hologic.ML\<close>.
+See \<^file>\<open>$ISABELLE_HOME/src/HOL/Tools/hologic.ML\<close>.
-}
{-# LANGUAGE OverloadedStrings #-}
@@ -2116,6 +2460,7 @@
mk_eq, dest_eq, true, is_true, false, is_false,
mk_not, dest_not, mk_conj, dest_conj, mk_disj, dest_disj,
mk_imp, dest_imp, mk_iff, dest_iff,
+ mk_all_op, dest_all_op, mk_ex_op, dest_ex_op,
mk_all, dest_all, mk_ex, dest_ex
)
where
@@ -2166,6 +2511,12 @@
Just (ty, t, u) | ty == boolT -> Just (t, u)
_ -> Nothing
+mk_all_op :: Typ -> Term -> Term; dest_all_op :: Term -> Maybe (Typ, Term)
+(mk_all_op, dest_all_op) = typed_op1 \<open>\<^const_name>\<open>All\<close>\<close>
+
+mk_ex_op :: Typ -> Term -> Term; dest_ex_op :: Term -> Maybe (Typ, Term)
+(mk_ex_op, dest_ex_op) = typed_op1 \<open>\<^const_name>\<open>Ex\<close>\<close>
+
mk_all :: Free -> Term -> Term; dest_all :: Name.Context -> Term -> Maybe (Free, Term)
(mk_all, dest_all) = binder \<open>\<^const_name>\<open>All\<close>\<close>
@@ -2180,7 +2531,7 @@
XML data representation of lambda terms.
-See also \<^file>\<open>$ISABELLE_HOME/src/Pure/term_xml.ML\<close>.
+See \<^file>\<open>$ISABELLE_HOME/src/Pure/term_xml.ML\<close>.
-}
{-# LANGUAGE LambdaCase #-}
@@ -2226,7 +2577,7 @@
XML data representation of lambda terms.
-See also \<^file>\<open>$ISABELLE_HOME/src/Pure/term_xml.ML\<close>.
+See \<^file>\<open>$ISABELLE_HOME/src/Pure/term_xml.ML\<close>.
-}
{-# OPTIONS_GHC -fno-warn-incomplete-patterns #-}
@@ -2405,6 +2756,7 @@
write, write_line,
read, read_block, read_line,
make_message, write_message, read_message,
+ exchange_message, exchange_message0,
make_line_message, write_line_message, read_line_message,
read_yxml, write_yxml
)
@@ -2507,6 +2859,16 @@
Just line -> Just <$> mapM (read_chunk socket) (parse_header line)
Nothing -> return Nothing
+exchange_message :: Socket -> [Bytes] -> IO (Maybe [Bytes])
+exchange_message socket msg = do
+ write_message socket msg
+ read_message socket
+
+exchange_message0 :: Socket -> [Bytes] -> IO ()
+exchange_message0 socket msg = do
+ _ <- exchange_message socket msg
+ return ()
+
-- hybrid messages: line or length+block (with content restriction)
@@ -2830,6 +3192,407 @@
client socket
\<close>
+generate_file "Isabelle/Time.hs" = \<open>
+{- Title: Isabelle/Time.hs
+ Author: Makarius
+ LICENSE: BSD 3-clause (Isabelle)
+
+Time based on milliseconds.
+
+See \<^file>\<open>~~/src/Pure/General/time.scala\<close>
+-}
+
+{-# LANGUAGE OverloadedStrings #-}
+
+module Isabelle.Time (
+ Time, seconds, minutes, ms, zero, is_zero, is_relevant,
+ get_seconds, get_minutes, get_ms, message
+)
+where
+
+import Text.Printf (printf)
+import Isabelle.Bytes (Bytes)
+import Isabelle.Library
+
+
+data Time = Time Int
+
+instance Eq Time where Time ms1 == Time ms2 = ms1 == ms2
+instance Ord Time where compare (Time ms1) (Time ms2) = compare ms1 ms2
+
+seconds :: Double -> Time
+seconds s = Time (round (s * 1000.0))
+
+minutes :: Double -> Time
+minutes m = Time (round (m * 60000.0))
+
+ms :: Int -> Time
+ms = Time
+
+zero :: Time
+zero = ms 0
+
+is_zero :: Time -> Bool
+is_zero (Time ms) = ms == 0
+
+is_relevant :: Time -> Bool
+is_relevant (Time ms) = ms >= 1
+
+get_seconds :: Time -> Double
+get_seconds (Time ms) = fromIntegral ms / 1000.0
+
+get_minutes :: Time -> Double
+get_minutes (Time ms) = fromIntegral ms / 60000.0
+
+get_ms :: Time -> Int
+get_ms (Time ms) = ms
+
+instance Show Time where
+ show t = printf "%.3f" (get_seconds t)
+
+message :: Time -> Bytes
+message t = make_bytes (show t) <> "s"
+\<close>
+
+generate_file "Isabelle/Timing.hs" = \<open>
+{- Title: Isabelle/Timing.hs
+ Author: Makarius
+ LICENSE: BSD 3-clause (Isabelle)
+
+Support for time measurement.
+
+See \<^file>\<open>~~/src/Pure/General/timing.ML\<close>
+and \<^file>\<open>~~/src/Pure/General/timing.scala\<close>
+-}
+
+module Isabelle.Timing (
+ Timing (..), zero, is_zero, is_relevant
+)
+where
+
+import qualified Isabelle.Time as Time
+import Isabelle.Time (Time)
+
+data Timing = Timing {elapsed :: Time, cpu :: Time, gc :: Time}
+ deriving (Show, Eq)
+
+zero :: Timing
+zero = Timing Time.zero Time.zero Time.zero
+
+is_zero :: Timing -> Bool
+is_zero t = Time.is_zero (elapsed t) && Time.is_zero (cpu t) && Time.is_zero (gc t)
+
+is_relevant :: Timing -> Bool
+is_relevant t = Time.is_relevant (elapsed t) || Time.is_relevant (cpu t) || Time.is_relevant (gc t)
+\<close>
+
+generate_file "Isabelle/Bash.hs" = \<open>
+{- Title: Isabelle/Bash.hs
+ Author: Makarius
+ LICENSE: BSD 3-clause (Isabelle)
+
+Support for GNU bash.
+
+See \<^file>\<open>$ISABELLE_HOME/src/Pure/System/bash.ML\<close>
+-}
+
+{-# LANGUAGE OverloadedStrings #-}
+
+module Isabelle.Bash (
+ string, strings,
+
+ Params,
+ get_script, get_input, get_cwd, get_putenv, get_redirect,
+ get_timeout, get_description,
+ script, input, cwd, putenv, redirect, timeout, description,
+)
+where
+
+import Text.Printf (printf)
+import qualified Isabelle.Symbol as Symbol
+import qualified Isabelle.Bytes as Bytes
+import Isabelle.Bytes (Bytes)
+import qualified Isabelle.Time as Time
+import Isabelle.Time (Time)
+import Isabelle.Library
+
+
+{- concrete syntax -}
+
+string :: Bytes -> Bytes
+string str =
+ if Bytes.null str then "\"\""
+ else str |> Bytes.unpack |> map trans |> Bytes.concat
+ where
+ trans b =
+ case Bytes.char b of
+ '\t' -> "$'\\t'"
+ '\n' -> "$'\\n'"
+ '\f' -> "$'\\f'"
+ '\r' -> "$'\\r'"
+ c ->
+ if Symbol.is_ascii_letter c || Symbol.is_ascii_digit c || c `elem` ("+,-./:_" :: String)
+ then Bytes.singleton b
+ else if b < 32 || b >= 127 then make_bytes (printf "$'\\x%02x'" b :: String)
+ else "\\" <> Bytes.singleton b
+
+strings :: [Bytes] -> Bytes
+strings = space_implode " " . map string
+
+
+{- server parameters -}
+
+data Params = Params {
+ _script :: Bytes,
+ _input :: Bytes,
+ _cwd :: Maybe Bytes,
+ _putenv :: [(Bytes, Bytes)],
+ _redirect :: Bool,
+ _timeout :: Time,
+ _description :: Bytes}
+ deriving (Show, Eq)
+
+get_script :: Params -> Bytes
+get_script = _script
+
+get_input :: Params -> Bytes
+get_input = _input
+
+get_cwd :: Params -> Maybe Bytes
+get_cwd = _cwd
+
+get_putenv :: Params -> [(Bytes, Bytes)]
+get_putenv = _putenv
+
+get_redirect :: Params -> Bool
+get_redirect = _redirect
+
+get_timeout :: Params -> Time
+get_timeout = _timeout
+
+get_description :: Params -> Bytes
+get_description = _description
+
+script :: Bytes -> Params
+script script = Params script "" Nothing [] False Time.zero ""
+
+input :: Bytes -> Params -> Params
+input input params = params { _input = input }
+
+cwd :: Bytes -> Params -> Params
+cwd cwd params = params { _cwd = Just cwd }
+
+putenv :: [(Bytes, Bytes)] -> Params -> Params
+putenv putenv params = params { _putenv = putenv }
+
+redirect :: Params -> Params
+redirect params = params { _redirect = True }
+
+timeout :: Time -> Params -> Params
+timeout timeout params = params { _timeout = timeout }
+
+description :: Bytes -> Params -> Params
+description description params = params { _description = description }
+\<close>
+
+generate_file "Isabelle/Process_Result.hs" = \<open>
+{- Title: Isabelle/Process_Result.hs
+ Author: Makarius
+ LICENSE: BSD 3-clause (Isabelle)
+
+Result of system process.
+
+See \<^file>\<open>~~/src/Pure/System/process_result.ML\<close>
+and \<^file>\<open>~~/src/Pure/System/process_result.scala\<close>
+-}
+
+{-# LANGUAGE OverloadedStrings #-}
+
+module Isabelle.Process_Result (
+ interrupt_rc, timeout_rc,
+
+ T, make, rc, out_lines, err_lines, timing, timing_elapsed, out, err, ok, check
+)
+where
+
+import Isabelle.Time (Time)
+import qualified Isabelle.Timing as Timing
+import Isabelle.Timing (Timing)
+import Isabelle.Bytes (Bytes)
+import Isabelle.Library
+
+
+interrupt_rc :: Int
+interrupt_rc = 130
+
+timeout_rc :: Int
+timeout_rc = 142
+
+data T =
+ Process_Result {
+ _rc :: Int,
+ _out_lines :: [Bytes],
+ _err_lines :: [Bytes],
+ _timing :: Timing}
+ deriving (Show, Eq)
+
+make :: Int -> [Bytes] -> [Bytes] -> Timing -> T
+make = Process_Result
+
+rc :: T -> Int
+rc = _rc
+
+out_lines :: T -> [Bytes]
+out_lines = _out_lines
+
+err_lines :: T -> [Bytes]
+err_lines = _err_lines
+
+timing :: T -> Timing
+timing = _timing
+
+timing_elapsed :: T -> Time
+timing_elapsed = Timing.elapsed . timing
+
+out :: T -> Bytes
+out = trim_line . cat_lines . out_lines
+
+err :: T -> Bytes
+err = trim_line . cat_lines . err_lines
+
+ok :: T -> Bool
+ok result = rc result == 0
+
+check :: T -> T
+check result = if ok result then result else error (make_string $ err result)
+\<close>
+
+generate_file "Isabelle/Options.hs" = \<open>
+{- Title: Isabelle/Options.hs
+ Author: Makarius
+ LICENSE: BSD 3-clause (Isabelle)
+
+System options with external string representation.
+
+See \<^file>\<open>~~/src/Pure/System/options.ML\<close>
+and \<^file>\<open>~~/src/Pure/System/options.scala\<close>
+-}
+
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE InstanceSigs #-}
+
+module Isabelle.Options (
+ boolT, intT, realT, stringT, unknownT,
+
+ T, typ, bool, int, real, seconds, string,
+ decode
+)
+where
+
+import qualified Data.Map.Strict as Map
+import Data.Map.Strict (Map)
+import qualified Isabelle.Properties as Properties
+import Isabelle.Bytes (Bytes)
+import qualified Isabelle.Value as Value
+import qualified Isabelle.Time as Time
+import Isabelle.Time (Time)
+import Isabelle.Library
+import qualified Isabelle.XML.Decode as Decode
+import Isabelle.XML.Classes (Decode (..))
+
+
+{- representation -}
+
+boolT :: Bytes
+boolT = "bool"
+
+intT :: Bytes
+intT = "int"
+
+realT :: Bytes
+realT = "real"
+
+stringT :: Bytes
+stringT = "string"
+
+unknownT :: Bytes
+unknownT = "unknown"
+
+data Opt = Opt {
+ _pos :: Properties.T,
+ _name :: Bytes,
+ _typ :: Bytes,
+ _value :: Bytes }
+
+data T = Options (Map Bytes Opt)
+
+
+{- check -}
+
+check_name :: T -> Bytes -> Opt
+check_name (Options map) name =
+ case Map.lookup name map of
+ Just opt | _typ opt /= unknownT -> opt
+ _ -> error (make_string ("Unknown system option " <> quote name))
+
+check_type :: T -> Bytes -> Bytes -> Opt
+check_type options name typ =
+ let
+ opt = check_name options name
+ t = _typ opt
+ in
+ if t == typ then opt
+ else error (make_string ("Ill-typed system option " <> quote name <> " : " <> t <> " vs. " <> typ))
+
+
+{- get typ -}
+
+typ :: T -> Bytes -> Bytes
+typ options name = _typ (check_name options name)
+
+
+{- get value -}
+
+get :: Bytes -> (Bytes -> Maybe a) -> T -> Bytes -> a
+get typ parse options name =
+ let opt = check_type options name typ in
+ case parse (_value opt) of
+ Just x -> x
+ Nothing ->
+ error (make_string ("Malformed value for system option " <> quote name <>
+ " : " <> typ <> " =\n" <> quote (_value opt)))
+
+bool :: T -> Bytes -> Bool
+bool = get boolT Value.parse_bool
+
+int :: T -> Bytes -> Int
+int = get intT Value.parse_int
+
+real :: T -> Bytes -> Double
+real = get realT Value.parse_real
+
+seconds :: T -> Bytes -> Time
+seconds options = Time.seconds . real options
+
+string :: T -> Bytes -> Bytes
+string = get stringT Just
+
+
+{- decode -}
+
+instance Decode T where
+ decode :: Decode.T T
+ decode =
+ let
+ decode_entry :: Decode.T (Bytes, Opt)
+ decode_entry body =
+ let
+ (pos, (name, (typ, value))) =
+ Decode.pair Decode.properties (Decode.pair Decode.string (Decode.pair Decode.string Decode.string)) body
+ in (name, Opt { _pos = pos, _name = name, _typ = typ, _value = value })
+ in Options . Map.fromList . Decode.list decode_entry
+\<close>
+
export_generated_files _
end
--- a/src/Tools/Haskell/Test.thy Wed Aug 18 12:33:31 2021 +0200
+++ b/src/Tools/Haskell/Test.thy Wed Aug 25 21:43:43 2021 +0200
@@ -18,7 +18,7 @@
GHC.new_project dir
{name = "isabelle",
depends =
- ["array", "bytestring", "containers", "network", "split", "text", "threads", "uuid"],
+ ["array", "bytestring", "containers", "network", "split", "text", "time", "threads", "uuid"],
modules = modules};
in
writeln (Generated_Files.execute dir \<open>Build\<close> "mv Isabelle src && isabelle ghc_stack build")