--- a/src/HOL/Proofs/ex/XML_Data.thy Mon Jul 15 21:48:23 2024 +0100
+++ b/src/HOL/Proofs/ex/XML_Data.thy Mon Jul 15 21:48:30 2024 +0100
@@ -48,11 +48,11 @@
text \<open>Some fairly large proof:\<close>
ML_val \<open>
- val xml = export_proof thy1 @{thm abs_less_iff};
+ val xml = export_proof thy1 @{thm Int.times_int.abs_eq};
val thm = import_proof thy1 xml;
- val xml_size = size (YXML.string_of_body xml);
- \<^assert> (xml_size > 100000);
+ val xml_size = Bytes.size (YXML.bytes_of_body xml);
+ \<^assert> (xml_size > 10000000);
\<close>
end
--- a/src/Pure/General/bytes.ML Mon Jul 15 21:48:23 2024 +0100
+++ b/src/Pure/General/bytes.ML Mon Jul 15 21:48:30 2024 +0100
@@ -13,7 +13,7 @@
val chunk_size: int
type T
val eq: T * T -> bool
- val length: T -> int
+ val size: T -> int
val contents: T -> string list
val contents_blob: T -> XML.body
val content: T -> string
@@ -54,7 +54,7 @@
{buffer: string list, chunks: string list, m: int (*buffer size*), n: int (*chunks size*)}
with
-fun length (Bytes {m, n, ...}) = m + n;
+fun size (Bytes {m, n, ...}) = m + n;
val compact = implode o rev;
@@ -69,7 +69,7 @@
val content = implode o contents;
-fun is_empty bytes = length bytes = 0;
+fun is_empty bytes = size bytes = 0;
val empty = Bytes {buffer = [], chunks = [], m = 0, n = 0};
@@ -132,10 +132,10 @@
fun beginning n bytes =
let
val dots = " ...";
- val m = (String.maxSize - size dots) div chunk_size;
+ val m = (String.maxSize - String.size dots) div chunk_size;
val a = implode (take m (contents bytes));
- val b = String.substring (a, 0, Int.min (n, size a));
- in if size b < length bytes then b ^ dots else b end;
+ val b = String.substring (a, 0, Int.min (n, String.size a));
+ in if String.size b < size bytes then b ^ dots else b end;
fun append bytes1 bytes2 = (*left-associative*)
if is_empty bytes1 then bytes2
@@ -155,7 +155,7 @@
fun space_explode sep bytes =
if is_empty bytes then []
- else if size sep <> 1 then [content bytes]
+ else if String.size sep <> 1 then [content bytes]
else
let
val sep_char = String.nth sep 0;
@@ -199,7 +199,7 @@
fun read_stream limit stream =
let
fun read bytes =
- (case read_block (limit - length bytes) stream of
+ (case read_block (limit - size bytes) stream of
"" => bytes
| s => read (add s bytes))
in read empty end;
@@ -216,6 +216,8 @@
val _ =
ML_system_pp (fn _ => fn _ => fn bytes =>
- PolyML.PrettyString ("Bytes {length = " ^ string_of_int (length bytes) ^ "}"))
+ PolyML.PrettyString
+ (if is_empty bytes then "Bytes.empty"
+ else "Bytes {size = " ^ string_of_int (size bytes) ^ "}"))
end;
--- a/src/Pure/PIDE/byte_message.ML Mon Jul 15 21:48:23 2024 +0100
+++ b/src/Pure/PIDE/byte_message.ML Mon Jul 15 21:48:30 2024 +0100
@@ -44,7 +44,7 @@
fun read_block stream n =
let
val msg = read stream n;
- val len = Bytes.length msg;
+ val len = Bytes.size msg;
in (if len = n then SOME msg else NONE, len) end;
fun read_line stream =
@@ -66,7 +66,7 @@
[Bytes.string (space_implode "," (map Value.print_int ns)), Bytes.newline];
fun write_message stream chunks =
- (write stream (make_header (map Bytes.length chunks) @ chunks); flush stream);
+ (write stream (make_header (map Bytes.size chunks) @ chunks); flush stream);
fun write_message_string stream =
write_message stream o map Bytes.string;
@@ -110,7 +110,7 @@
if is_length msg orelse is_terminated msg then
error ("Bad content for line message:\n" ^ Bytes.beginning 100 msg)
else
- let val n = Bytes.length msg in
+ let val n = Bytes.size msg in
write stream
((if n > 100 orelse Bytes.exists_string (fn s => s = "\n") msg
then make_header [n + 1] else []) @ [msg, Bytes.newline]);
--- a/src/Pure/PIDE/yxml.ML Mon Jul 15 21:48:23 2024 +0100
+++ b/src/Pure/PIDE/yxml.ML Mon Jul 15 21:48:30 2024 +0100
@@ -24,6 +24,8 @@
val body_size: XML.body -> int
val string_of_body: XML.body -> string
val string_of: XML.tree -> string
+ val bytes_of_body: XML.body -> Bytes.T
+ val bytes_of: XML.tree -> Bytes.T
val write_body: Path.T -> XML.body -> unit
val output_markup: Markup.T -> string * string
val output_markup_elem: Markup.T -> (string * string) * string
@@ -76,6 +78,9 @@
val string_of_body = Buffer.build_content o fold (traverse Buffer.add);
val string_of = string_of_body o single;
+val bytes_of_body = Bytes.build o fold (traverse Bytes.add);
+val bytes_of = bytes_of_body o single;
+
fun write_body path body =
path |> File_Stream.open_output (fn file =>
fold (traverse (fn s => fn () => File_Stream.output file s)) body ());
@@ -109,8 +114,7 @@
val split_bytes =
Bytes.space_explode X
- #> filter (fn "" => false | _ => true)
- #> map (space_explode Y);
+ #> map_filter (fn "" => NONE | s => SOME (space_explode Y s));
(* structural errors *)
--- a/src/Pure/PIDE/yxml.scala Mon Jul 15 21:48:23 2024 +0100
+++ b/src/Pure/PIDE/yxml.scala Mon Jul 15 21:48:30 2024 +0100
@@ -148,14 +148,16 @@
/* parse chunks */
- for (chunk <- source.iterator_X if !chunk.is_empty) {
- if (chunk.is_Y) pop()
- else {
- chunk.iterator_Y.toList match {
- case ch :: name :: atts if ch.is_empty =>
- push(parse_string(name), atts.map(parse_attrib))
- case txts =>
- for (txt <- txts) add(cache.tree0(XML.Text(cache.string(parse_string(txt)))))
+ for (chunk <- source.iterator_X) {
+ if (!chunk.is_empty) {
+ if (chunk.is_Y) pop()
+ else {
+ chunk.iterator_Y.toList match {
+ case ch :: name :: atts if ch.is_empty =>
+ push(parse_string(name), atts.map(parse_attrib))
+ case txts =>
+ for (txt <- txts) add(cache.tree0(XML.Text(cache.string(parse_string(txt)))))
+ }
}
}
}
--- a/src/Pure/Proof/extraction.ML Mon Jul 15 21:48:23 2024 +0100
+++ b/src/Pure/Proof/extraction.ML Mon Jul 15 21:48:30 2024 +0100
@@ -188,7 +188,7 @@
{oracles = Ord_List.make Proofterm.oracle_ord oracles,
thms = Ord_List.make Proofterm.thm_ord thms,
zboxes = [],
- zproof = ZDummy,
+ zproof = ZNop,
proof = prf};
in Proofterm.thm_body body end;
--- a/src/Pure/proofterm.ML Mon Jul 15 21:48:23 2024 +0100
+++ b/src/Pure/proofterm.ML Mon Jul 15 21:48:30 2024 +0100
@@ -336,7 +336,7 @@
fun no_proof_body zproof proof =
PBody {oracles = [], thms = [], zboxes = [], zproof = zproof, proof = proof};
-val no_thm_body = thm_body (no_proof_body ZDummy MinProof);
+val no_thm_body = thm_body (no_proof_body ZNop MinProof);
fun no_thm_names (Abst (x, T, prf)) = Abst (x, T, no_thm_names prf)
| no_thm_names (AbsP (x, t, prf)) = AbsP (x, t, no_thm_names prf)
@@ -405,7 +405,12 @@
fn Var (a, _) => (indexname a, []),
fn Bound a => ([], int a),
fn Abs (a, b, c) => ([a], pair typ (standard_term consts) (b, c)),
- fn op $ a => ([], pair (standard_term consts) (standard_term consts) a)];
+ fn t as op $ a =>
+ if can Logic.match_of_class t then raise Match
+ else ([], pair (standard_term consts) (standard_term consts) a),
+ fn t =>
+ let val (T, c) = Logic.match_of_class t
+ in ([c], typ T) end];
fun standard_proof consts prf = prf |> variant
[fn MinProof => ([], []),
@@ -459,7 +464,7 @@
val (a, b, c) =
triple (list (pair (pair string (Position.of_properties o properties))
(option (term consts)))) (list (thm consts)) (proof consts) x;
- in PBody {oracles = a, thms = b, zboxes = [], zproof = ZDummy, proof = c} end
+ in PBody {oracles = a, thms = b, zboxes = [], zproof = ZNop, proof = c} end
and thm consts x =
let
val (a, (b, (c, (d, e)))) =
@@ -2187,7 +2192,7 @@
val (zproof1, zboxes1) =
if zproof_enabled proofs then
ZTerm.add_box_proof {unconstrain = unconstrain} thy hyps concl zproof0 zboxes0
- else (ZDummy, []);
+ else (ZNop, []);
val proof1 =
if proof_enabled proofs then fold_rev implies_intr_proof hyps proof0
else MinProof;
@@ -2198,7 +2203,7 @@
val unconstrainT = unconstrainT_proof (Sign.classes_of thy) sorts_proof ucontext;
val postproc = map_proof_of (unconstrainT #> named ? rew_proof thy);
val body1 =
- {oracles = oracles0, thms = thms0, zboxes = [], zproof = ZDummy, proof = proof1};
+ {oracles = oracles0, thms = thms0, zboxes = [], zproof = ZNop, proof = proof1};
in (i, fulfill_proof_future thy promises postproc (Future.value (PBody body1))) end;
val (i, body') =
--- a/src/Pure/term.scala Mon Jul 15 21:48:23 2024 +0100
+++ b/src/Pure/term.scala Mon Jul 15 21:48:30 2024 +0100
@@ -96,17 +96,17 @@
case class App(fun: Term, arg: Term) extends Term {
private lazy val hash: Int = ("App", fun, arg).hashCode()
override def hashCode(): Int = hash
-
- override def toString: String =
- this match {
- case OFCLASS(ty, c) => "OFCLASS(" + ty + "," + c + ")"
- case _ => "App(" + fun + "," + arg + ")"
- }
+ }
+ case class OFCLASS(typ: Typ, name: String) extends Term {
+ private lazy val hash: Int = ("OFCLASS", typ, name).hashCode()
+ override def hashCode(): Int = hash
}
def dummy_pattern(ty: Typ): Term = Const("Pure.dummy_pattern", List(ty))
val dummy: Term = dummy_pattern(dummyT)
+ def mk_of_sort(typ: Typ, s: Sort): List[Term] = s.map(c => OFCLASS(typ, c))
+
sealed abstract class Proof
case object MinProof extends Proof
case class PBound(index: Int) extends Proof
@@ -148,30 +148,6 @@
}
- /* type classes within the logic */
-
- object Class_Const {
- val suffix = "_class"
- def apply(c: Class): String = c + suffix
- def unapply(s: String): Option[Class] =
- if (s.endsWith(suffix)) Some(s.substring(0, s.length - suffix.length)) else None
- }
-
- object OFCLASS {
- def apply(ty: Typ, s: Sort): List[Term] = s.map(c => apply(ty, c))
-
- def apply(ty: Typ, c: Class): Term =
- App(Const(Class_Const(c), List(ty)), Const(Pure_Thy.TYPE, List(ty)))
-
- def unapply(t: Term): Option[(Typ, String)] =
- t match {
- case App(Const(Class_Const(c), List(ty)), Const(Pure_Thy.TYPE, List(ty1)))
- if ty == ty1 => Some((ty, c))
- case _ => None
- }
- }
-
-
/** cache **/
@@ -230,6 +206,7 @@
case Abs(name, typ, body) =>
store(Abs(cache_string(name), cache_typ(typ), cache_term(body)))
case App(fun, arg) => store(App(cache_term(fun), cache_term(arg)))
+ case OFCLASS(typ, name) => store(OFCLASS(cache_typ(typ), cache_string(name)))
}
}
}
--- a/src/Pure/term_xml.ML Mon Jul 15 21:48:23 2024 +0100
+++ b/src/Pure/term_xml.ML Mon Jul 15 21:48:30 2024 +0100
@@ -55,7 +55,12 @@
fn Var (a, b) => (indexname a, typ_body b),
fn Bound a => ([], int a),
fn Abs (a, b, c) => ([a], pair typ (term consts) (b, c)),
- fn op $ a => ([], pair (term consts) (term consts) a)];
+ fn t as op $ a =>
+ if can Logic.match_of_class t then raise Match
+ else ([], pair (term consts) (term consts) a),
+ fn t =>
+ let val (T, c) = Logic.match_of_class t
+ in ([c], typ T) end];
end;
@@ -91,7 +96,8 @@
fn (a, b) => Var (indexname a, typ_body b),
fn ([], a) => Bound (int a),
fn ([a], b) => let val (c, d) = pair typ (term consts) b in Abs (a, c, d) end,
- fn ([], a) => op $ (pair (term consts) (term consts) a)];
+ fn ([], a) => op $ (pair (term consts) (term consts) a),
+ fn ([a], b) => Logic.mk_of_class (typ b, a)];
end;
--- a/src/Pure/term_xml.scala Mon Jul 15 21:48:23 2024 +0100
+++ b/src/Pure/term_xml.scala Mon Jul 15 21:48:30 2024 +0100
@@ -34,7 +34,8 @@
{ case Var(a, b) => (indexname(a), typ_body(b)) },
{ case Bound(a) => (Nil, int(a)) },
{ case Abs(a, b, c) => (List(a), pair(typ, term)(b, c)) },
- { case App(a, b) => (Nil, pair(term, term)(a, b)) }))
+ { case App(a, b) => (Nil, pair(term, term)(a, b)) },
+ { case OFCLASS(a, b) => (List(b), typ(a)) }))
}
object Decode {
@@ -61,7 +62,8 @@
{ case (a, b) => Var(indexname(a), typ_body(b)) },
{ case (Nil, a) => Bound(int(a)) },
{ case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) },
- { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) }))
+ { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) },
+ { case (List(a), b) => OFCLASS(typ(b), a) }))
def term_env(env: Map[String, Typ]): T[Term] = {
def env_type(x: String, t: Typ): Typ =
@@ -74,7 +76,8 @@
{ case (a, b) => Var(indexname(a), typ_body(b)) },
{ case (Nil, a) => Bound(int(a)) },
{ case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) },
- { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) }))
+ { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) },
+ { case (List(a), b) => OFCLASS(typ(b), a) }))
term
}
--- a/src/Pure/thm.ML Mon Jul 15 21:48:23 2024 +0100
+++ b/src/Pure/thm.ML Mon Jul 15 21:48:30 2024 +0100
@@ -757,7 +757,7 @@
make_deriv0 promises
(PBody {oracles = oracles, thms = thms, zboxes = zboxes, zproof = zproof, proof = proof});
-val empty_deriv = make_deriv [] [] [] [] ZDummy MinProof;
+val empty_deriv = make_deriv [] [] [] [] ZNop MinProof;
(* inference rules *)
@@ -778,7 +778,7 @@
val zboxes' = ZTerm.union_zboxes zboxes1 zboxes2;
val proofs = Proofterm.get_proofs_level ();
- val zproof' = if Proofterm.zproof_enabled proofs then zproof zprf1 zprf2 else ZDummy;
+ val zproof' = if Proofterm.zproof_enabled proofs then zproof zprf1 zprf2 else ZNop;
val proof' = if Proofterm.proof_enabled proofs then proof prf1 prf2 else MinProof;
in make_deriv ps' oracles' thms' zboxes' zproof' proof' end;
@@ -788,7 +788,7 @@
let val proofs = Proofterm.get_proofs_level () in
if Proofterm.proof_enabled proofs orelse Proofterm.zproof_enabled proofs then
deriv_rule1 I I (make_deriv [] [] [] []
- (if Proofterm.zproof_enabled proofs then zproof () else ZDummy)
+ (if Proofterm.zproof_enabled proofs then zproof () else ZNop)
(if Proofterm.proof_enabled proofs then proof () else MinProof))
else empty_deriv
end;
@@ -853,7 +853,7 @@
val i = serial ();
val future = future_thm |> Future.map (future_result i cert sorts prop);
in
- Thm (make_deriv [(i, future)] [] [] [] ZDummy MinProof,
+ Thm (make_deriv [(i, future)] [] [] [] ZNop MinProof,
{cert = cert,
tags = [],
maxidx = maxidx,
@@ -1203,7 +1203,7 @@
val thy = Context.certificate_theory cert handle ERROR msg =>
raise CONTEXT (msg, [], [ct], [], NONE);
in ZTerm.oracle_proof thy name prop end
- else ZDummy;
+ else ZNop;
in
Thm (make_deriv [] [oracle] [] [] zproof proof,
{cert = cert,
@@ -2115,7 +2115,7 @@
raise THM ("store_zproof: theorem may not use promises", 0, [thm]);
val ((i, (_, zproof1)), zproof2) = ZTerm.thm_proof thy name hyps prop zproof;
- val der1 = if Options.default_bool "prune_proofs" then deriv [] ZDummy else deriv zboxes zproof1;
+ val der1 = if Options.default_bool "prune_proofs" then deriv [] ZNop else deriv zboxes zproof1;
val der2 = deriv [] zproof2;
val thm' = trim_context (Thm (der1, args));
--- a/src/Pure/zterm.ML Mon Jul 15 21:48:23 2024 +0100
+++ b/src/Pure/zterm.ML Mon Jul 15 21:48:30 2024 +0100
@@ -200,7 +200,7 @@
type zproof_const = (zproof_name * zterm) * (ztyp ZTVars.table * zterm ZVars.table);
datatype zproof =
- ZDummy (*dummy proof*)
+ ZNop
| ZConstp of zproof_const
| ZBoundp of int
| ZAbst of string * ztyp * zproof
@@ -480,7 +480,7 @@
fun fold_proof {hyps} typ term =
let
- fun proof ZDummy = I
+ fun proof ZNop = I
| proof (ZConstp (_, (instT, inst))) =
ZTVars.fold (typ o #2) instT #> ZVars.fold (term o #2) inst
| proof (ZBoundp _) = I
@@ -538,7 +538,7 @@
fun map_proof_same {hyps} typ term =
let
- fun proof ZDummy = raise Same.SAME
+ fun proof ZNop = raise Same.SAME
| proof (ZConstp (a, (instT, inst))) =
ZConstp (a, map_insts_same typ term (instT, inst))
| proof (ZBoundp _) = raise Same.SAME
--- a/src/Tools/Haskell/Haskell.thy Mon Jul 15 21:48:23 2024 +0100
+++ b/src/Tools/Haskell/Haskell.thy Mon Jul 15 21:48:30 2024 +0100
@@ -2347,6 +2347,7 @@
| Bound Int
| Abs (Name, Typ, Term)
| App (Term, Term)
+ | OFCLASS (Typ, Name)
deriving (Show, Eq, Ord)
@@ -2681,7 +2682,8 @@
\case { Var (a, b) -> Just (indexname a, typ_body b); _ -> Nothing },
\case { Bound a -> Just ([], int a); _ -> Nothing },
\case { Abs (a, b, c) -> Just ([a], pair typ term (b, c)); _ -> Nothing },
- \case { App a -> Just ([], pair term term a); _ -> Nothing }]
+ \case { App a -> Just ([], pair term term a); _ -> Nothing },
+ \case { OFCLASS (a, b) -> Just ([b], typ a); _ -> Nothing }]
\<close>
generate_file "Isabelle/Term_XML/Decode.hs" = \<open>
@@ -2730,7 +2732,8 @@
\(a, b) -> Var (indexname a, typ_body b),
\([], a) -> Bound (int a),
\([a], b) -> let (c, d) = pair typ term b in Abs (a, c, d),
- \([], a) -> App (pair term term a)]
+ \([], a) -> App (pair term term a),
+ \([a], b) -> OFCLASS (typ b, a)]
\<close>
generate_file "Isabelle/XML/Classes.hs" = \<open>