# HG changeset patch
# User wenzelm
# Date 1720972170 -7200
# Node ID 446b887e23c7f6b36320062b1a5673c5bd8ad546
# Parent  2acdaa0a7d297c957b7da539c5091e7d739af942
clarified data representation: prefer explicit OFCLASS constructor, following datatype zterm;

diff -r 2acdaa0a7d29 -r 446b887e23c7 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Sun Jul 14 16:17:31 2024 +0200
+++ b/src/Pure/proofterm.ML	Sun Jul 14 17:49:30 2024 +0200
@@ -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 => ([], []),
diff -r 2acdaa0a7d29 -r 446b887e23c7 src/Pure/term.scala
--- a/src/Pure/term.scala	Sun Jul 14 16:17:31 2024 +0200
+++ b/src/Pure/term.scala	Sun Jul 14 17:49:30 2024 +0200
@@ -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)))
           }
       }
     }
diff -r 2acdaa0a7d29 -r 446b887e23c7 src/Pure/term_xml.ML
--- a/src/Pure/term_xml.ML	Sun Jul 14 16:17:31 2024 +0200
+++ b/src/Pure/term_xml.ML	Sun Jul 14 17:49:30 2024 +0200
@@ -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;
 
diff -r 2acdaa0a7d29 -r 446b887e23c7 src/Pure/term_xml.scala
--- a/src/Pure/term_xml.scala	Sun Jul 14 16:17:31 2024 +0200
+++ b/src/Pure/term_xml.scala	Sun Jul 14 17:49:30 2024 +0200
@@ -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
     }