more operations: support type classes within the logic;
authorwenzelm
Sat Jul 20 14:03:51 2019 +0200 (3 months ago)
changeset 7038568d2c533db9c
parent 70384 8ce08b154aa1
child 70386 6af87375b95f
more operations: support type classes within the logic;
src/Pure/pure_thy.scala
src/Pure/term.scala
     1.1 --- a/src/Pure/pure_thy.scala	Sat Jul 20 12:52:29 2019 +0200
     1.2 +++ b/src/Pure/pure_thy.scala	Sat Jul 20 14:03:51 2019 +0200
     1.3 @@ -19,6 +19,7 @@
     1.4    val ALL: String = "Pure.all"
     1.5    val IMP: String = "Pure.imp"
     1.6    val EQ: String = "Pure.eq"
     1.7 +  val TYPE: String = "Pure.type"
     1.8  
     1.9  
    1.10    /* proof terms (abstract syntax) */
     2.1 --- a/src/Pure/term.scala	Sat Jul 20 12:52:29 2019 +0200
     2.2 +++ b/src/Pure/term.scala	Sat Jul 20 14:03:51 2019 +0200
     2.3 @@ -33,6 +33,24 @@
     2.4    case class App(fun: Term, arg: Term) extends Term
     2.5  
     2.6  
     2.7 +  /* Pure logic */
     2.8 +
     2.9 +  def itselfT(ty: Typ): Typ = Type(Pure_Thy.ITSELF, List(ty))
    2.10 +  val propT: Typ = Type(Pure_Thy.PROP, Nil)
    2.11 +  def funT(ty1: Typ, ty2: Typ): Typ = Type(Pure_Thy.FUN, List(ty1, ty2))
    2.12 +
    2.13 +  def mk_type(ty: Typ): Term = Const(Pure_Thy.TYPE, itselfT(ty))
    2.14 +
    2.15 +  def const_of_class(c: String): String = c + "_class"
    2.16 +
    2.17 +  def mk_of_sort(ty: Typ, s: Sort): List[Term] =
    2.18 +  {
    2.19 +    val class_type = funT(itselfT(ty), propT)
    2.20 +    val t = mk_type(ty)
    2.21 +    s.map(c => App(Const(const_of_class(c), class_type), t))
    2.22 +  }
    2.23 +
    2.24 +
    2.25    /* type arguments of consts */
    2.26  
    2.27    def const_typargs(name: String, typ: Typ, typargs: List[String], decl: Typ): List[Typ] =