merged
authorpaulson
Mon, 15 Jul 2024 21:48:30 +0100
changeset 80570 4d4f107a778f
parent 80568 fbb655bf62d4 (diff)
parent 80569 f1872ef41766 (current diff)
child 80571 673add17a05e
child 80572 6ab6431864b6
merged
--- 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>