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