# HG changeset patch
# User wenzelm
# Date 1563624231 -7200
# Node ID 68d2c533db9cee47b1a6bec57b956c8823c41c61
# Parent  8ce08b154aa146600b75f4d0cb625b050413c2b3
more operations: support type classes within the logic;

diff -r 8ce08b154aa1 -r 68d2c533db9c src/Pure/pure_thy.scala
--- a/src/Pure/pure_thy.scala	Sat Jul 20 12:52:29 2019 +0200
+++ b/src/Pure/pure_thy.scala	Sat Jul 20 14:03:51 2019 +0200
@@ -19,6 +19,7 @@
   val ALL: String = "Pure.all"
   val IMP: String = "Pure.imp"
   val EQ: String = "Pure.eq"
+  val TYPE: String = "Pure.type"
 
 
   /* proof terms (abstract syntax) */
diff -r 8ce08b154aa1 -r 68d2c533db9c src/Pure/term.scala
--- a/src/Pure/term.scala	Sat Jul 20 12:52:29 2019 +0200
+++ b/src/Pure/term.scala	Sat Jul 20 14:03:51 2019 +0200
@@ -33,6 +33,24 @@
   case class App(fun: Term, arg: Term) extends Term
 
 
+  /* Pure logic */
+
+  def itselfT(ty: Typ): Typ = Type(Pure_Thy.ITSELF, List(ty))
+  val propT: Typ = Type(Pure_Thy.PROP, Nil)
+  def funT(ty1: Typ, ty2: Typ): Typ = Type(Pure_Thy.FUN, List(ty1, ty2))
+
+  def mk_type(ty: Typ): Term = Const(Pure_Thy.TYPE, itselfT(ty))
+
+  def const_of_class(c: String): String = c + "_class"
+
+  def mk_of_sort(ty: Typ, s: Sort): List[Term] =
+  {
+    val class_type = funT(itselfT(ty), propT)
+    val t = mk_type(ty)
+    s.map(c => App(Const(const_of_class(c), class_type), t))
+  }
+
+
   /* type arguments of consts */
 
   def const_typargs(name: String, typ: Typ, typargs: List[String], decl: Typ): List[Typ] =