# 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 }