--- a/NEWS Fri Jun 24 10:49:40 2022 +0200
+++ b/NEWS Fri Jun 24 21:17:35 2022 +0200
@@ -34,6 +34,9 @@
*** HOL ***
+* Theory Char_ord: streamlined logical specifications.
+Minor INCOMPATIBILITY.
+
* Rule split_of_bool_asm is not split any longer, analogously to
split_if_asm. INCOMPATIBILITY.
--- a/src/HOL/Library/Char_ord.thy Fri Jun 24 10:49:40 2022 +0200
+++ b/src/HOL/Library/Char_ord.thy Fri Jun 24 21:17:35 2022 +0200
@@ -8,14 +8,93 @@
imports Main
begin
+context linordered_semidom
+begin
+
+lemma horner_sum_nonnegative:
+ \<open>0 \<le> horner_sum of_bool 2 bs\<close>
+ by (induction bs) simp_all
+
+end
+
+context unique_euclidean_semiring_numeral
+begin
+
+lemma horner_sum_bound:
+ \<open>horner_sum of_bool 2 bs < 2 ^ length bs\<close>
+proof (induction bs)
+ case Nil
+ then show ?case
+ by simp
+next
+ case (Cons b bs)
+ moreover define a where \<open>a = 2 ^ length bs - horner_sum of_bool 2 bs\<close>
+ ultimately have *: \<open>2 ^ length bs = horner_sum of_bool 2 bs + a\<close>
+ by simp
+ have \<open>1 < a * 2\<close> if \<open>0 < a\<close>
+ using that add_mono [of 1 a 1 a]
+ by (simp add: mult_2_right discrete)
+ with Cons show ?case
+ by (simp add: algebra_simps *)
+qed
+
+end
+
+context unique_euclidean_semiring_numeral
+begin
+
+lemma horner_sum_less_eq_iff_lexordp_eq:
+ \<open>horner_sum of_bool 2 bs \<le> horner_sum of_bool 2 cs \<longleftrightarrow> lexordp_eq (rev bs) (rev cs)\<close>
+ if \<open>length bs = length cs\<close>
+proof -
+ have \<open>horner_sum of_bool 2 (rev bs) \<le> horner_sum of_bool 2 (rev cs) \<longleftrightarrow> lexordp_eq bs cs\<close>
+ if \<open>length bs = length cs\<close> for bs cs
+ using that proof (induction bs cs rule: list_induct2)
+ case Nil
+ then show ?case
+ by simp
+ next
+ case (Cons b bs c cs)
+ with horner_sum_nonnegative [of \<open>rev bs\<close>] horner_sum_nonnegative [of \<open>rev cs\<close>]
+ horner_sum_bound [of \<open>rev bs\<close>] horner_sum_bound [of \<open>rev cs\<close>]
+ show ?case
+ by (auto simp add: horner_sum_append not_le Cons intro: add_strict_increasing2 add_increasing)
+ qed
+ from that this [of \<open>rev bs\<close> \<open>rev cs\<close>] show ?thesis
+ by simp
+qed
+
+lemma horner_sum_less_iff_lexordp:
+ \<open>horner_sum of_bool 2 bs < horner_sum of_bool 2 cs \<longleftrightarrow> ord_class.lexordp (rev bs) (rev cs)\<close>
+ if \<open>length bs = length cs\<close>
+proof -
+ have \<open>horner_sum of_bool 2 (rev bs) < horner_sum of_bool 2 (rev cs) \<longleftrightarrow> ord_class.lexordp bs cs\<close>
+ if \<open>length bs = length cs\<close> for bs cs
+ using that proof (induction bs cs rule: list_induct2)
+ case Nil
+ then show ?case
+ by simp
+ next
+ case (Cons b bs c cs)
+ with horner_sum_nonnegative [of \<open>rev bs\<close>] horner_sum_nonnegative [of \<open>rev cs\<close>]
+ horner_sum_bound [of \<open>rev bs\<close>] horner_sum_bound [of \<open>rev cs\<close>]
+ show ?case
+ by (auto simp add: horner_sum_append not_less Cons intro: add_strict_increasing2 add_increasing)
+ qed
+ from that this [of \<open>rev bs\<close> \<open>rev cs\<close>] show ?thesis
+ by simp
+qed
+
+end
+
instantiation char :: linorder
begin
-definition less_eq_char :: "char \<Rightarrow> char \<Rightarrow> bool"
- where "c1 \<le> c2 \<longleftrightarrow> of_char c1 \<le> (of_char c2 :: nat)"
+definition less_eq_char :: \<open>char \<Rightarrow> char \<Rightarrow> bool\<close>
+ where \<open>c1 \<le> c2 \<longleftrightarrow> of_char c1 \<le> (of_char c2 :: nat)\<close>
-definition less_char :: "char \<Rightarrow> char \<Rightarrow> bool"
- where "c1 < c2 \<longleftrightarrow> of_char c1 < (of_char c2 :: nat)"
+definition less_char :: \<open>char \<Rightarrow> char \<Rightarrow> bool\<close>
+ where \<open>c1 < c2 \<longleftrightarrow> of_char c1 < (of_char c2 :: nat)\<close>
instance
@@ -23,23 +102,21 @@
end
-lemma less_eq_char_simp [simp]:
- "Char b0 b1 b2 b3 b4 b5 b6 b7 \<le> Char c0 c1 c2 c3 c4 c5 c6 c7
- \<longleftrightarrow> foldr (\<lambda>b k. of_bool b + k * 2) [b0, b1, b2, b3, b4, b5, b6, b7] 0
- \<le> foldr (\<lambda>b k. of_bool b + k * 2) [c0, c1, c2, c3, c4, c5, c6, c7] (0::nat)"
- by (simp add: less_eq_char_def)
+lemma less_eq_char_simp [simp, code]:
+ \<open>Char b0 b1 b2 b3 b4 b5 b6 b7 \<le> Char c0 c1 c2 c3 c4 c5 c6 c7
+ \<longleftrightarrow> lexordp_eq [b7, b6, b5, b4, b3, b2, b1, b0] [c7, c6, c5, c4, c3, c2, c1, c0]\<close>
+ by (simp only: less_eq_char_def of_char_def char.sel horner_sum_less_eq_iff_lexordp_eq list.size) simp
-lemma less_char_simp [simp]:
- "Char b0 b1 b2 b3 b4 b5 b6 b7 < Char c0 c1 c2 c3 c4 c5 c6 c7
- \<longleftrightarrow> foldr (\<lambda>b k. of_bool b + k * 2) [b0, b1, b2, b3, b4, b5, b6, b7] 0
- < foldr (\<lambda>b k. of_bool b + k * 2) [c0, c1, c2, c3, c4, c5, c6, c7] (0::nat)"
- by (simp add: less_char_def)
+lemma less_char_simp [simp, code]:
+ \<open>Char b0 b1 b2 b3 b4 b5 b6 b7 < Char c0 c1 c2 c3 c4 c5 c6 c7
+ \<longleftrightarrow> ord_class.lexordp [b7, b6, b5, b4, b3, b2, b1, b0] [c7, c6, c5, c4, c3, c2, c1, c0]\<close>
+ by (simp only: less_char_def of_char_def char.sel horner_sum_less_iff_lexordp list.size) simp
instantiation char :: distrib_lattice
begin
-definition "(inf :: char \<Rightarrow> _) = min"
-definition "(sup :: char \<Rightarrow> _) = max"
+definition \<open>(inf :: char \<Rightarrow> _) = min\<close>
+definition \<open>(sup :: char \<Rightarrow> _) = max\<close>
instance
by standard (auto simp add: inf_char_def sup_char_def max_min_distrib2)
--- a/src/HOL/Library/code_test.ML Fri Jun 24 10:49:40 2022 +0200
+++ b/src/HOL/Library/code_test.ML Fri Jun 24 21:17:35 2022 +0200
@@ -153,7 +153,8 @@
| SOME drv => drv)
val with_dir = if Config.get ctxt debug then with_debug_dir else Isabelle_System.with_tmp_dir
fun eval result =
- with_dir "Code_Test" (driver ctxt ((apfst o map o apfst) Long_Name.implode result))
+ with_dir "Code_Test"
+ (driver ctxt ((apfst o map) (apfst Long_Name.implode #> apsnd Bytes.content) result))
|> parse_result compiler
fun evaluator program _ vs_ty deps =
Exn.interruptible_capture eval
--- a/src/HOL/List.thy Fri Jun 24 10:49:40 2022 +0200
+++ b/src/HOL/List.thy Fri Jun 24 21:17:35 2022 +0200
@@ -2247,13 +2247,13 @@
lemma butlast_take:
"n \<le> length xs \<Longrightarrow> butlast (take n xs) = take (n - 1) xs"
- by (simp add: butlast_conv_take min.absorb1 min.absorb2)
+ by (simp add: butlast_conv_take)
lemma butlast_drop: "butlast (drop n xs) = drop n (butlast xs)"
by (simp add: butlast_conv_take drop_take ac_simps)
lemma take_butlast: "n < length xs \<Longrightarrow> take n (butlast xs) = take n xs"
- by (simp add: butlast_conv_take min.absorb1)
+ by (simp add: butlast_conv_take)
lemma drop_butlast: "drop n (butlast xs) = butlast (drop n xs)"
by (simp add: butlast_conv_take drop_take ac_simps)
@@ -2374,7 +2374,7 @@
qed auto
lemma nth_image: "l \<le> size xs \<Longrightarrow> nth xs ` {0..<l} = set(take l xs)"
- by(auto simp: set_conv_nth image_def) (metis Suc_le_eq nth_take order_trans)
+ by (simp add: set_conv_nth) force
subsubsection \<open>\<^const>\<open>takeWhile\<close> and \<^const>\<open>dropWhile\<close>\<close>
@@ -2808,7 +2808,7 @@
proof (induction "zip xs (zip ys zs)" arbitrary: xs ys zs)
case Nil
from Nil [symmetric] show ?case
- by (auto simp add: zip_eq_Nil_iff)
+ by auto
next
case (Cons xyz xyzs)
from Cons.hyps(2) [symmetric] show ?case
@@ -2820,7 +2820,7 @@
proof (induction "zip xs ys" arbitrary: xs ys)
case Nil
then show ?case
- by (auto simp add: zip_eq_Nil_iff dest: sym)
+ by auto
next
case (Cons xy xys)
from Cons.hyps(2) [symmetric] show ?case
@@ -3702,8 +3702,9 @@
proof (induct xs)
case (Cons x xs)
show ?case
- apply (auto simp add: Cons nth_Cons split: nat.split_asm)
- apply (metis Suc_less_eq2 in_set_conv_nth less_not_refl zero_less_Suc)+
+ apply (auto simp add: Cons nth_Cons less_Suc_eq_le split: nat.split_asm)
+ apply (metis Suc_leI in_set_conv_nth length_pos_if_in_set lessI less_imp_le_nat less_nat_zero_code)
+ apply (metis Suc_le_eq)
done
qed auto
@@ -5256,8 +5257,8 @@
case (Suc j)
have *: "\<And>xss. xs # map tl xss = map tl ((x#xs)#xss)" by simp
have **: "\<And>xss. (x#xs) # filter (\<lambda>ys. ys \<noteq> []) xss = filter (\<lambda>ys. ys \<noteq> []) ((x#xs)#xss)" by simp
- { fix x have "Suc j < length x \<longleftrightarrow> x \<noteq> [] \<and> j < length x - Suc 0"
- by (cases x) simp_all
+ { fix xs :: \<open>'a list\<close> have "Suc j < length xs \<longleftrightarrow> xs \<noteq> [] \<and> j < length xs - Suc 0"
+ by (cases xs) simp_all
} note *** = this
have j_less: "j < length (transpose (xs # concat (map (case_list [] (\<lambda>h t. [t])) xss)))"
@@ -5282,6 +5283,7 @@
by (simp add: nth_transpose filter_map comp_def)
qed
+
subsubsection \<open>\<^const>\<open>min\<close> and \<^const>\<open>arg_min\<close>\<close>
lemma min_list_Min: "xs \<noteq> [] \<Longrightarrow> min_list xs = Min (set xs)"
@@ -5548,8 +5550,6 @@
lemmas sorted2_simps = sorted1 sorted2
-lemmas [code] = sorted0 sorted2_simps
-
lemma sorted_append:
"sorted (xs@ys) = (sorted xs \<and> sorted ys \<and> (\<forall>x \<in> set xs. \<forall>y \<in> set ys. x\<le>y))"
by (simp add: sorted_wrt_append)
@@ -5966,6 +5966,9 @@
lemma sorted_enumerate [simp]: "sorted (map fst (enumerate n xs))"
by (simp add: enumerate_eq_zip)
+lemma sorted_insort_is_snoc: "sorted xs \<Longrightarrow> \<forall>x \<in> set xs. a \<ge> x \<Longrightarrow> insort a xs = xs @ [a]"
+ by (induct xs) (auto dest!: insort_is_Cons)
+
text \<open>Stability of \<^const>\<open>sort_key\<close>:\<close>
lemma sort_key_stable: "filter (\<lambda>y. f y = k) (sort_key f xs) = filter (\<lambda>y. f y = k) xs"
@@ -7011,7 +7014,7 @@
end
-lemma lexordp_simps [simp]:
+lemma lexordp_simps [simp, code]:
"lexordp [] ys = (ys \<noteq> [])"
"lexordp xs [] = False"
"lexordp (x # xs) (y # ys) \<longleftrightarrow> x < y \<or> \<not> y < x \<and> lexordp xs ys"
@@ -7022,7 +7025,7 @@
| Cons: "x < y \<Longrightarrow> lexordp_eq (x # xs) (y # ys)"
| Cons_eq: "\<lbrakk> \<not> x < y; \<not> y < x; lexordp_eq xs ys \<rbrakk> \<Longrightarrow> lexordp_eq (x # xs) (y # ys)"
-lemma lexordp_eq_simps [simp]:
+lemma lexordp_eq_simps [simp, code]:
"lexordp_eq [] ys = True"
"lexordp_eq xs [] \<longleftrightarrow> xs = []"
"lexordp_eq (x # xs) [] = False"
@@ -7062,7 +7065,7 @@
end
declare ord.lexordp_simps [simp, code]
-declare ord.lexordp_eq_simps [code, simp]
+declare ord.lexordp_eq_simps [simp, code]
context order
begin
@@ -7155,9 +7158,6 @@
end
-lemma sorted_insort_is_snoc: "sorted xs \<Longrightarrow> \<forall>x \<in> set xs. a \<ge> x \<Longrightarrow> insort a xs = xs @ [a]"
- by (induct xs) (auto dest!: insort_is_Cons)
-
subsubsection \<open>Lexicographic combination of measure functions\<close>
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Fri Jun 24 10:49:40 2022 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Fri Jun 24 21:17:35 2022 +0200
@@ -215,8 +215,9 @@
|> Exn.release
fun value (contains_existentials, ((genuine_only, (quiet, verbose)), size))
- ctxt cookie (code_modules, _) =
+ ctxt cookie (code_modules_bytes, _) =
let
+ val code_modules = (map o apsnd) Bytes.content code_modules_bytes
val ((is_genuine, counterexample_of), (get, put, put_ml)) = cookie
fun message s = if quiet then () else writeln s
fun verbose_message s = if not quiet andalso verbose then writeln s else ()
--- a/src/Pure/General/bytes.ML Fri Jun 24 10:49:40 2022 +0200
+++ b/src/Pure/General/bytes.ML Fri Jun 24 21:17:35 2022 +0200
@@ -12,6 +12,7 @@
sig
val chunk_size: int
type T
+ val eq: T * T -> bool
val length: T -> int
val contents: T -> string list
val contents_blob: T -> XML.body
@@ -27,9 +28,14 @@
val last_string: T -> string option
val trim_line: T -> T
val append: T -> T -> T
+ val appends: T list -> T
val string: string -> T
val newline: T
val buffer: Buffer.T -> T
+ val space_explode: string -> T -> string list
+ val split_lines: T -> string list
+ val trim_split_lines: T -> string list
+ val cat_lines: string list -> T
val read_block: int -> BinIO.instream -> string
val read_stream: int -> BinIO.instream -> T
val write_stream: BinIO.outstream -> T -> unit
@@ -52,6 +58,10 @@
val compact = implode o rev;
+fun eq (Bytes {buffer, chunks, m, n}, Bytes {buffer = buffer', chunks = chunks', m = m', n = n'}) =
+ m = m' andalso n = n' andalso chunks = chunks' andalso
+ (buffer = buffer' orelse compact buffer = compact buffer);
+
fun contents (Bytes {buffer, chunks, ...}) =
rev (chunks |> not (null buffer) ? cons (compact buffer));
@@ -132,12 +142,57 @@
else if is_empty bytes2 then bytes1
else bytes1 |> fold add (contents bytes2);
+val appends = build o fold (fn b => fn a => append a b);
+
val string = build o add;
val newline = string "\n";
val buffer = build o fold add o Buffer.contents;
+
+(* space_explode *)
+
+fun space_explode sep bytes =
+ if is_empty bytes then []
+ else if size sep <> 1 then [content bytes]
+ else
+ let
+ val sep_char = String.sub (sep, 0);
+
+ fun add_part s part =
+ Buffer.add (Substring.string s) (the_default Buffer.empty part);
+
+ fun explode head tail part res =
+ if Substring.isEmpty head then
+ (case tail of
+ [] =>
+ (case part of
+ NONE => rev res
+ | SOME buf => rev (Buffer.content buf :: res))
+ | chunk :: chunks => explode (Substring.full chunk) chunks part res)
+ else
+ (case Substring.fields (fn c => c = sep_char) head of
+ [a] => explode Substring.empty tail (SOME (add_part a part)) res
+ | a :: rest =>
+ let
+ val (bs, c) = split_last rest;
+ val res' = res
+ |> cons (Buffer.content (add_part a part))
+ |> fold (cons o Substring.string) bs;
+ val part' = SOME (add_part c NONE);
+ in explode Substring.empty tail part' res' end)
+ in explode Substring.empty (contents bytes) NONE [] end;
+
+val split_lines = space_explode "\n";
+
+val trim_split_lines = trim_line #> split_lines #> map Library.trim_line;
+
+fun cat_lines lines = build (fold add (separate "\n" lines));
+
+
+(* IO *)
+
fun read_block limit =
File.input_size (if limit < 0 then chunk_size else Int.min (chunk_size, limit));
@@ -149,10 +204,12 @@
| s => read (add s bytes))
in read empty end;
-fun write_stream stream = File.outputs stream o contents;
+fun write_stream stream bytes =
+ File.outputs stream (contents bytes);
-val read = File.open_input (read_stream ~1);
-val write = File.open_output write_stream;
+fun read path = File.open_input (fn stream => read_stream ~1 stream) path;
+
+fun write path bytes = File.open_output (fn stream => write_stream stream bytes) path;
(* ML pretty printing *)
--- a/src/Pure/General/bytes.scala Fri Jun 24 10:49:40 2022 +0200
+++ b/src/Pure/General/bytes.scala Fri Jun 24 21:17:35 2022 +0200
@@ -42,36 +42,32 @@
/* base64 */
- def base64(s: String): Bytes = {
+ def decode_base64(s: String): Bytes = {
val a = Base64.getDecoder.decode(s)
new Bytes(a, 0, a.length)
}
- object Decode_Base64 extends Scala.Fun("decode_base64") {
+ object Decode_Base64 extends Scala.Fun_Bytes("decode_base64") {
val here = Scala_Project.here
- def invoke(args: List[Bytes]): List[Bytes] =
- List(base64(Library.the_single(args).text))
+ def apply(arg: Bytes): Bytes = decode_base64(arg.text)
}
- object Encode_Base64 extends Scala.Fun("encode_base64") {
+ object Encode_Base64 extends Scala.Fun_Bytes("encode_base64") {
val here = Scala_Project.here
- def invoke(args: List[Bytes]): List[Bytes] =
- List(Bytes(Library.the_single(args).base64))
+ def apply(arg: Bytes): Bytes = Bytes(arg.encode_base64)
}
/* XZ compression */
- object Compress extends Scala.Fun("compress") {
+ object Compress extends Scala.Fun_Bytes("compress") {
val here = Scala_Project.here
- def invoke(args: List[Bytes]): List[Bytes] =
- List(Library.the_single(args).compress())
+ def apply(arg: Bytes): Bytes = arg.compress()
}
- object Uncompress extends Scala.Fun("uncompress") {
+ object Uncompress extends Scala.Fun_Bytes("uncompress") {
val here = Scala_Project.here
- def invoke(args: List[Bytes]): List[Bytes] =
- List(Library.the_single(args).uncompress())
+ def apply(arg: Bytes): Bytes = arg.uncompress()
}
@@ -160,16 +156,16 @@
def text: String = UTF8.decode_permissive(this)
- def base64: String = {
+ def encode_base64: String = {
val b =
if (offset == 0 && length == bytes.length) bytes
else Bytes(bytes, offset, length).bytes
Base64.getEncoder.encodeToString(b)
}
- def maybe_base64: (Boolean, String) = {
+ def maybe_encode_base64: (Boolean, String) = {
val s = text
- if (this == Bytes(s)) (false, s) else (true, base64)
+ if (this == Bytes(s)) (false, s) else (true, encode_base64)
}
override def toString: String = "Bytes(" + length + ")"
--- a/src/Pure/General/csv.scala Fri Jun 24 10:49:40 2022 +0200
+++ b/src/Pure/General/csv.scala Fri Jun 24 21:17:35 2022 +0200
@@ -10,7 +10,7 @@
object CSV {
def print_field(field: Any): String = {
val str = field.toString
- if (str.exists("\",\r\n".contains(_))) {
+ if (str.exists("\",\r\n ".contains(_))) {
(for (c <- str) yield { if (c == '"') "\"\"" else c.toString }).mkString("\"", "", "\"")
}
else str
--- a/src/Pure/General/file.ML Fri Jun 24 10:49:40 2022 +0200
+++ b/src/Pure/General/file.ML Fri Jun 24 21:17:35 2022 +0200
@@ -30,13 +30,10 @@
val input_size: int -> BinIO.instream -> string
val input_all: BinIO.instream -> string
val fold_lines: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a
- val fold_pages: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a
val read_lines: Path.T -> string list
- val read_pages: Path.T -> string list
val read: Path.T -> string
val write: Path.T -> string -> unit
val append: Path.T -> string -> unit
- val generate: Path.T -> string -> unit
val output: BinIO.outstream -> string -> unit
val outputs: BinIO.outstream -> string list -> unit
val write_list: Path.T -> string list -> unit
@@ -143,24 +140,20 @@
. avoid size limit of TextIO.inputAll and overhead of many TextIO.inputLine
. optional terminator at end-of-input
*)
-fun fold_chunks terminator f path a = open_input (fn file =>
+fun fold_lines f path a = open_input (fn file =>
let
fun read buf x =
(case input file of
"" => (case Buffer.content buf of "" => x | line => f line x)
| input =>
- (case String.fields (fn c => c = terminator) input of
+ (case String.fields (fn c => c = #"\n") input of
[rest] => read (Buffer.add rest buf) x
- | line :: more => read_lines more (f (Buffer.content (Buffer.add line buf)) x)))
- and read_lines [rest] x = read (Buffer.add rest Buffer.empty) x
- | read_lines (line :: more) x = read_lines more (f line x);
+ | line :: more => read_more more (f (Buffer.content (Buffer.add line buf)) x)))
+ and read_more [rest] x = read (Buffer.add rest Buffer.empty) x
+ | read_more (line :: more) x = read_more more (f line x);
in read Buffer.empty a end) path;
-fun fold_lines f = fold_chunks #"\n" f;
-fun fold_pages f = fold_chunks #"\f" f;
-
fun read_lines path = rev (fold_lines cons path []);
-fun read_pages path = rev (fold_pages cons path []);
val read = open_input input_all;
@@ -176,7 +169,6 @@
fun write path txt = write_list path [txt];
fun append path txt = append_list path [txt];
-fun generate path txt = if try read path = SOME txt then () else write path txt;
fun write_buffer path buf =
open_output (fn file => List.app (output file) (Buffer.contents buf)) path;
--- a/src/Pure/ML/ml_init.ML Fri Jun 24 10:49:40 2022 +0200
+++ b/src/Pure/ML/ml_init.ML Fri Jun 24 21:17:35 2022 +0200
@@ -33,3 +33,9 @@
if n = 1 then String.str (String.sub (s, i))
else String.substring (s, i, n);
end;
+
+structure Substring =
+struct
+ open Substring;
+ val empty = full "";
+end;
--- a/src/Pure/ML/ml_process.scala Fri Jun 24 10:49:40 2022 +0200
+++ b/src/Pure/ML/ml_process.scala Fri Jun 24 21:17:35 2022 +0200
@@ -72,22 +72,20 @@
// options
+ val eval_options = if (heaps.isEmpty) Nil else List("Options.load_default ()")
val isabelle_process_options = Isabelle_System.tmp_file("options")
Isabelle_System.chmod("600", File.path(isabelle_process_options))
File.write(isabelle_process_options, YXML.string_of_body(options.encode))
- val eval_options = if (heaps.isEmpty) Nil else List("Options.load_default ()")
// session base
+ val (init_session_base, eval_init_session) =
+ session_base match {
+ case None => (sessions_structure.bootstrap, Nil)
+ case Some(base) => (base, List("Resources.init_session_env ()"))
+ }
val init_session = Isabelle_System.tmp_file("init_session")
Isabelle_System.chmod("600", File.path(init_session))
- val eval_init_session =
- session_base match {
- case None => Nil
- case Some(base) =>
- File.write(init_session, new Resources(sessions_structure, base).init_session_yxml)
- List("Resources.init_session_file (Path.explode " +
- ML_Syntax.print_string_bytes(File.path(init_session).implode) + ")")
- }
+ File.write(init_session, new Resources(sessions_structure, init_session_base).init_session_yxml)
// process
val eval_process =
@@ -119,9 +117,9 @@
val bash_env = new HashMap(env)
bash_env.put("ISABELLE_PROCESS_OPTIONS", File.standard_path(isabelle_process_options))
+ bash_env.put("ISABELLE_INIT_SESSION", File.standard_path(init_session))
bash_env.put("ISABELLE_TMP", File.standard_path(isabelle_tmp))
bash_env.put("POLYSTATSDIR", isabelle_tmp.getAbsolutePath)
- bash_env.put("ISABELLE_SCALA_FUNCTIONS", Scala.functions.mkString(","))
Bash.process(
options.string("ML_process_policy") + """ "$ML_HOME/poly" -q """ +
--- a/src/Pure/PIDE/resources.ML Fri Jun 24 10:49:40 2022 +0200
+++ b/src/Pure/PIDE/resources.ML Fri Jun 24 21:17:35 2022 +0200
@@ -13,19 +13,18 @@
bibtex_entries: (string * string list) list,
command_timings: Properties.T list,
load_commands: (string * Position.T) list,
- scala_functions: (string * (bool * Position.T)) list,
+ scala_functions: (string * ((bool * bool) * Position.T)) list,
global_theories: (string * string) list,
loaded_theories: string list} -> unit
val init_session_yxml: string -> unit
- val init_session_file: Path.T -> unit
+ val init_session_env: unit -> unit
val finish_session_base: unit -> unit
val global_theory: string -> string option
val loaded_theory: string -> bool
val check_session: Proof.context -> string * Position.T -> string
val last_timing: Toplevel.transition -> Time.time
val check_load_command: Proof.context -> string * Position.T -> string
- val scala_functions: unit -> string list
- val check_scala_function: Proof.context -> string * Position.T -> string * bool
+ val check_scala_function: Proof.context -> string * Position.T -> string * (bool * bool)
val master_directory: theory -> Path.T
val imports_of: theory -> (string * Position.T) list
val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
@@ -104,7 +103,7 @@
bibtex_entries = Symtab.empty: string list Symtab.table,
timings = empty_timings,
load_commands = []: (string * Position.T) list,
- scala_functions = Symtab.empty: (bool * Position.T) Symtab.table},
+ scala_functions = Symtab.empty: ((bool * bool) * Position.T) Symtab.table},
{global_theories = Symtab.empty: string Symtab.table,
loaded_theories = Symtab.empty: unit Symtab.table});
@@ -137,7 +136,7 @@
(pair (list (pair string string))
(pair (list (pair string (list string))) (pair (list properties)
(pair (list (pair string properties))
- (pair (list (pair string (pair bool properties)))
+ (pair (list (pair string (pair (pair bool bool) properties)))
(pair (list (pair string string)) (list string))))))))
end;
in
@@ -152,8 +151,14 @@
loaded_theories = loaded_theories}
end;
-fun init_session_file path =
- init_session_yxml (File.read path) before File.rm path;
+fun init_session_env () =
+ (case getenv "ISABELLE_INIT_SESSION" of
+ "" => ()
+ | name =>
+ try File.read (Path.explode name)
+ |> Option.app init_session_yxml);
+
+val _ = init_session_env ();
fun finish_session_base () =
Synchronized.change global_session_base
@@ -180,22 +185,13 @@
(* Scala functions *)
-(*raw bootstrap environment*)
-fun scala_functions () = space_explode "," (getenv "ISABELLE_SCALA_FUNCTIONS");
-
-(*regular resources*)
-fun scala_function a =
- (a, the_default (false, Position.none) (Symtab.lookup (get_session_base1 #scala_functions) a));
-
fun check_scala_function ctxt arg =
let
- val funs = scala_functions () |> sort_strings |> map scala_function;
- val name = Completion.check_entity Markup.scala_functionN (map (apsnd #2) funs) ctxt arg;
- val multi =
- (case AList.lookup (op =) funs name of
- SOME (multi, _) => multi
- | NONE => false);
- in (name, multi) end;
+ val table = get_session_base1 #scala_functions;
+ val funs = Symtab.fold (fn (a, (_, pos)) => cons (a, pos)) table [] |> sort_by #1;
+ val name = Completion.check_entity Markup.scala_functionN funs ctxt arg;
+ val flags = #1 (the (Symtab.lookup table name));
+ in (name, flags) end;
val _ = Theory.setup
(Document_Output.antiquotation_verbatim_embedded \<^binding>\<open>scala_function\<close>
@@ -206,8 +202,10 @@
ML_Antiquotation.value_embedded \<^binding>\<open>scala\<close>
(Args.context -- Scan.lift Parse.embedded_position >> (fn (ctxt, arg) =>
let
- val (name, multi) = check_scala_function ctxt arg;
- val func = if multi then "Scala.function" else "Scala.function1";
+ val (name, (single, bytes)) = check_scala_function ctxt arg;
+ val func =
+ (if single then "Scala.function1" else "Scala.function") ^
+ (if bytes then "_bytes" else "");
in ML_Syntax.atomic (func ^ " " ^ ML_Syntax.print_string name) end)));
--- a/src/Pure/PIDE/resources.scala Fri Jun 24 10:49:40 2022 +0200
+++ b/src/Pure/PIDE/resources.scala Fri Jun 24 21:17:35 2022 +0200
@@ -46,14 +46,14 @@
pair(list(pair(string, list(string))),
pair(list(properties),
pair(list(pair(string, properties)),
- pair(list(pair(string, pair(bool, properties))),
+ pair(list(Scala.encode_fun),
pair(list(pair(string, string)), list(string))))))))(
(sessions_structure.session_positions,
(sessions_structure.dest_session_directories,
(sessions_structure.bibtex_entries,
(command_timings,
(Command_Span.load_commands.map(cmd => (cmd.name, cmd.position)),
- (Scala.functions.map(fun => (fun.name, (fun.multi, fun.position))),
+ (Scala.functions,
(session_base.global_theories.toList,
session_base.loaded_theories.keys)))))))))
}
--- a/src/Pure/System/options.ML Fri Jun 24 10:49:40 2022 +0200
+++ b/src/Pure/System/options.ML Fri Jun 24 21:17:35 2022 +0200
@@ -211,11 +211,8 @@
(case getenv "ISABELLE_PROCESS_OPTIONS" of
"" => ()
| name =>
- let val path = Path.explode name in
- (case try File.read path of
- SOME s => set_default (decode (YXML.parse_body s))
- | NONE => ())
- end);
+ try File.read (Path.explode name)
+ |> Option.app (set_default o decode o YXML.parse_body));
val _ = load_default ();
val _ = ML_Print_Depth.set_print_depth (default_int "ML_print_depth");
--- a/src/Pure/System/scala.scala Fri Jun 24 10:49:40 2022 +0200
+++ b/src/Pure/System/scala.scala Fri Jun 24 21:17:35 2022 +0200
@@ -18,12 +18,16 @@
abstract class Fun(val name: String, val thread: Boolean = false) {
override def toString: String = name
- def multi: Boolean = true
+ def single: Boolean = false
+ def bytes: Boolean = false
def position: Properties.T = here.position
def here: Scala_Project.Here
def invoke(args: List[Bytes]): List[Bytes]
}
+ trait Single_Fun extends Fun { override def single: Boolean = true }
+ trait Bytes_Fun extends Fun { override def bytes: Boolean = true }
+
abstract class Fun_Strings(name: String, thread: Boolean = false)
extends Fun(name, thread = thread) {
override def invoke(args: List[Bytes]): List[Bytes] =
@@ -32,13 +36,25 @@
}
abstract class Fun_String(name: String, thread: Boolean = false)
- extends Fun_Strings(name, thread = thread) {
- override def multi: Boolean = false
+ extends Fun_Strings(name, thread = thread) with Single_Fun {
override def apply(args: List[String]): List[String] =
List(apply(Library.the_single(args)))
def apply(arg: String): String
}
+ abstract class Fun_Bytes(name: String, thread: Boolean = false)
+ extends Fun(name, thread = thread) with Single_Fun with Bytes_Fun {
+ override def invoke(args: List[Bytes]): List[Bytes] =
+ List(apply(Library.the_single(args)))
+ def apply(arg: Bytes): Bytes
+ }
+
+ val encode_fun: XML.Encode.T[Fun] = { fun =>
+ import XML.Encode._
+ pair(string, pair(pair(bool, bool), properties))(
+ fun.name, ((fun.single, fun.bytes), fun.position))
+ }
+
class Functions(val functions: Fun*) extends Isabelle_System.Service
lazy val functions: List[Fun] =
--- a/src/Pure/Thy/export.ML Fri Jun 24 10:49:40 2022 +0200
+++ b/src/Pure/Thy/export.ML Fri Jun 24 21:17:35 2022 +0200
@@ -53,10 +53,10 @@
{theory = thy, binding = binding, executable = true, compress = true, strict = true} body;
fun export_file thy binding file =
- export thy binding [XML.Text (File.read file)];
+ export thy binding (Bytes.contents_blob (Bytes.read file));
fun export_executable_file thy binding file =
- export_executable thy binding [XML.Text (File.read file)];
+ export_executable thy binding (Bytes.contents_blob (Bytes.read file));
(* information message *)
--- a/src/Pure/Tools/generated_files.ML Fri Jun 24 10:49:40 2022 +0200
+++ b/src/Pure/Tools/generated_files.ML Fri Jun 24 21:17:35 2022 +0200
@@ -6,8 +6,8 @@
signature GENERATED_FILES =
sig
- val add_files: Path.binding * string -> theory -> theory
- type file = {path: Path.T, pos: Position.T, content: string}
+ val add_files: Path.binding * Bytes.T -> theory -> theory
+ type file = {path: Path.T, pos: Position.T, content: Bytes.T}
val file_binding: file -> Path.binding
val file_markup: file -> Markup.T
val print_file: file -> string
@@ -52,7 +52,7 @@
(** context data **)
-type file = Path.T * (Position.T * string);
+type file = Path.T * (Position.T * Bytes.T);
type file_type =
{name: string, ext: string, make_comment: string -> string, make_string: string -> string};
@@ -75,10 +75,11 @@
fun merge ((files1, types1, antiqs1), (files2, types2, antiqs2)) =
let
val files' =
- (files1, files2) |> Symtab.join (K (Library.merge (fn ((path1, file1), (path2, file2)) =>
- if path1 <> path2 then false
- else if file1 = file2 then true
- else err_dup_files path1 (#1 file1) (#1 file2))));
+ (files1, files2) |> Symtab.join (fn _ =>
+ Library.merge (fn ((path1, (pos1, bytes1)), (path2, (pos2, bytes2))) =>
+ if path1 <> path2 then false
+ else if pos1 = pos2 andalso Bytes.eq (bytes1, bytes2) then true
+ else err_dup_files path1 pos1 pos2));
val types' = Name_Space.merge_tables (types1, types2);
val antiqs' = Name_Space.merge_tables (antiqs1, antiqs2);
in (files', types', antiqs') end;
@@ -104,7 +105,7 @@
(* get files *)
-type file = {path: Path.T, pos: Position.T, content: string};
+type file = {path: Path.T, pos: Position.T, content: Bytes.T};
fun file_binding (file: file) = Path.binding (#path file, #pos file);
@@ -147,11 +148,15 @@
let
val path = Path.expand (dir + #path file);
val _ = Isabelle_System.make_directory (Path.dir path);
- val _ = File.generate path (#content file);
- in () end;
+ val content = #content file;
+ val write_content =
+ (case try Bytes.read path of
+ SOME old_content => not (Bytes.eq (content, old_content))
+ | NONE => true)
+ in if write_content then Bytes.write path content else () end;
fun export_file thy (file: file) =
- Export.export thy (file_binding file) [XML.Text (#content file)];
+ Export.export thy (file_binding file) (Bytes.contents_blob (#content file));
(* file types *)
@@ -244,7 +249,7 @@
handle ERROR msg => error (msg ^ Position.here pos);
val header = #make_comment file_type " generated by Isabelle ";
- val content = header ^ "\n" ^ read_source lthy file_type source;
+ val content = Bytes.string (header ^ "\n" ^ read_source lthy file_type source);
in lthy |> (Local_Theory.background_theory o add_files) (binding, content) end;
fun generate_file_cmd (file, source) lthy =
@@ -297,15 +302,15 @@
val binding = binding0 |> Path.map_binding (executable = SOME true ? Path.exe);
val (path, pos) = Path.dest_binding binding;
val content =
- (case try File.read (dir + path) of
- SOME context => context
+ (case try Bytes.read (dir + path) of
+ SOME bytes => Bytes.contents_blob bytes
| NONE => error ("Missing result file " ^ Path.print path ^ Position.here pos));
val _ = Export.report_export thy export_prefix;
val binding' =
Path.map_binding (Path.append (Path.path_of_binding export_prefix)) binding;
in
(if is_some executable then Export.export_executable else Export.export)
- thy binding' [XML.Text content]
+ thy binding' content
end));
val _ =
if null export then ()
--- a/src/Pure/Tools/server_commands.scala Fri Jun 24 10:49:40 2022 +0200
+++ b/src/Pure/Tools/server_commands.scala Fri Jun 24 21:17:35 2022 +0200
@@ -266,7 +266,7 @@
val matcher = Export.make_matcher(args.export_pattern)
for { entry <- snapshot.exports if matcher(entry.theory_name, entry.name) }
yield {
- val (base64, body) = entry.uncompressed.maybe_base64
+ val (base64, body) = entry.uncompressed.maybe_encode_base64
JSON.Object("name" -> entry.name, "base64" -> base64, "body" -> body)
}
}))
--- a/src/Tools/Code/code_printer.ML Fri Jun 24 10:49:40 2022 +0200
+++ b/src/Tools/Code/code_printer.ML Fri Jun 24 21:17:35 2022 +0200
@@ -26,7 +26,7 @@
val doublesemicolon: Pretty.T list -> Pretty.T
val indent: int -> Pretty.T -> Pretty.T
val markup_stmt: Code_Symbol.T -> Pretty.T -> Pretty.T
- val format: Code_Symbol.T list -> int -> Pretty.T -> string
+ val format: Code_Symbol.T list -> int -> Pretty.T -> Bytes.T
type var_ctxt
val make_vars: string list -> var_ctxt
@@ -165,7 +165,7 @@
#> YXML.parse_body
#> filter_presentation presentation_names
#> Buffer.add "\n"
- #> Buffer.content;
+ #> Bytes.buffer;
(** names and variable name contexts **)
--- a/src/Tools/Code/code_runtime.ML Fri Jun 24 10:49:40 2022 +0200
+++ b/src/Tools/Code/code_runtime.ML Fri Jun 24 21:17:35 2022 +0200
@@ -92,7 +92,7 @@
fun build_compilation_text ctxt some_target program consts =
Code_Target.compilation_text ctxt (the_default target some_target) program consts false
- #>> (fn ml_modules => space_implode "\n\n" (map snd ml_modules));
+ #>> (fn ml_modules => space_implode "\n\n" (map (Bytes.content o snd) ml_modules));
fun run_compilation_text cookie ctxt comp vs_t args =
let
@@ -439,7 +439,7 @@
val (ml_modules, target_names) =
Code_Target.produce_code_for ctxt
target module_name NONE [] program false (map Constant consts @ map Type_Constructor tycos);
- val ml_code = space_implode "\n\n" (map snd ml_modules);
+ val ml_code = space_implode "\n\n" (map (Bytes.content o snd) ml_modules);
val (consts', tycos') = chop (length consts) target_names;
val consts_map = map2 (fn const =>
fn NONE =>
@@ -482,7 +482,7 @@
| SOME c' => c';
val tyco_names = map deresolve_tyco named_tycos;
val const_names = map deresolve_const named_consts;
- val generated_code = space_implode "\n\n" (map snd ml_modules);
+ val generated_code = space_implode "\n\n" (map (Bytes.content o snd) ml_modules);
val (of_term_code, of_term_names) =
print_computation_code ctxt compiled_value computation_cTs computation_Ts;
val compiled_computation = generated_code ^ "\n" ^ of_term_code;
@@ -720,7 +720,7 @@
"(* Generated from " ^
Path.implode (Resources.thy_path (Path.basic (Context.theory_name thy))) ^
"; DO NOT EDIT! *)";
- val thy' = Code_Target.export code_binding (preamble ^ "\n\n" ^ code) thy;
+ val thy' = Code_Target.export code_binding (Bytes.string (preamble ^ "\n\n" ^ code)) thy;
val _ = Code_Target.code_export_message thy';
in thy' end;
--- a/src/Tools/Code/code_target.ML Fri Jun 24 10:49:40 2022 +0200
+++ b/src/Tools/Code/code_target.ML Fri Jun 24 21:17:35 2022 +0200
@@ -16,9 +16,9 @@
-> int option -> Token.T list -> Code_Thingol.program -> bool -> Code_Symbol.T list
-> local_theory -> local_theory
val produce_code_for: Proof.context -> string -> string -> int option -> Token.T list
- -> Code_Thingol.program -> bool -> Code_Symbol.T list -> (string list * string) list * string option list
+ -> Code_Thingol.program -> bool -> Code_Symbol.T list -> (string list * Bytes.T) list * string option list
val present_code_for: Proof.context -> string -> string -> int option -> Token.T list
- -> Code_Thingol.program -> Code_Symbol.T list * Code_Symbol.T list -> string
+ -> Code_Thingol.program -> Code_Symbol.T list * Code_Symbol.T list -> Bytes.T
val check_code_for: string -> bool -> Token.T list
-> Code_Thingol.program -> bool -> Code_Symbol.T list -> local_theory -> local_theory
@@ -29,9 +29,9 @@
-> (((string * string) * ({physical: bool} * Input.source) option) * Token.T list) list
-> local_theory -> local_theory
val produce_code: Proof.context -> bool -> string list
- -> string -> string -> int option -> Token.T list -> (string list * string) list * string option list
+ -> string -> string -> int option -> Token.T list -> (string list * Bytes.T) list * string option list
val present_code: Proof.context -> string list -> Code_Symbol.T list
- -> string -> string -> int option -> Token.T list -> string
+ -> string -> string -> int option -> Token.T list -> Bytes.T
val check_code: bool -> string list -> ((string * bool) * Token.T list) list
-> local_theory -> local_theory
@@ -39,13 +39,13 @@
val generatedN: string
val code_path: Path.T -> Path.T
val code_export_message: theory -> unit
- val export: Path.binding -> string -> theory -> theory
+ val export: Path.binding -> Bytes.T -> theory -> theory
val compilation_text: Proof.context -> string -> Code_Thingol.program
-> Code_Symbol.T list -> bool -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm
- -> (string list * string) list * string
+ -> (string list * Bytes.T) list * string
val compilation_text': Proof.context -> string -> string option -> Code_Thingol.program
-> Code_Symbol.T list -> bool -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm
- -> ((string list * string) list * string) * (Code_Symbol.T -> string option)
+ -> ((string list * Bytes.T) list * string) * (Code_Symbol.T -> string option)
type serializer
type literals = Code_Printer.literals
@@ -289,7 +289,7 @@
fun export binding content thy =
let
val thy' = thy |> Generated_Files.add_files (binding, content);
- val _ = Export.export thy' binding [XML.Text content];
+ val _ = Export.export thy' binding (Bytes.contents_blob content);
in thy' end;
local
@@ -309,11 +309,11 @@
fun export_physical root format pretty_modules =
(case pretty_modules of
- Singleton (_, p) => File.write root (format p)
+ Singleton (_, p) => Bytes.write root (format p)
| Hierarchy code_modules =>
(Isabelle_System.make_directory root;
List.app (fn (names, p) =>
- File.write (Path.appends (root :: map Path.basic names)) (format p)) code_modules));
+ Bytes.write (Path.appends (root :: map Path.basic names)) (format p)) code_modules));
in
@@ -343,7 +343,8 @@
let val format = Code_Printer.format selects width in
(case pretty_modules of
Singleton (_, p) => format p
- | Hierarchy code_modules => space_implode "\n\n" (map (format o #2) code_modules))
+ | Hierarchy code_modules =>
+ Bytes.appends (separate (Bytes.string "\n\n") (map (format o #2) code_modules)))
end;
end;
@@ -788,6 +789,7 @@
(fn ctxt => fn ((consts, symbols), (target_name, some_width)) =>
present_code ctxt consts symbols
target_name "Example" some_width []
+ |> Bytes.content
|> trim_line
|> Document_Output.verbatim (Config.put Document_Antiquotation.thy_output_display true ctxt)));