src/Pure/term.scala
author wenzelm
Thu Aug 15 16:02:47 2019 +0200 (9 months ago)
changeset 70533 031620901fcd
parent 70385 68d2c533db9c
child 70535 de6062ac70b6
permissions -rw-r--r--
support for (fully reconstructed) proof terms in Scala;
proper cache_typs;
wenzelm@43730
     1
/*  Title:      Pure/term.scala
wenzelm@43730
     2
    Author:     Makarius
wenzelm@43730
     3
wenzelm@43779
     4
Lambda terms, types, sorts.
wenzelm@43730
     5
wenzelm@43730
     6
Note: Isabelle/ML is the primary environment for logical operations.
wenzelm@43730
     7
*/
wenzelm@43730
     8
wenzelm@43730
     9
package isabelle
wenzelm@43730
    10
wenzelm@43730
    11
wenzelm@43730
    12
object Term
wenzelm@43730
    13
{
wenzelm@70383
    14
  /* types and terms */
wenzelm@70383
    15
wenzelm@43730
    16
  type Indexname = (String, Int)
wenzelm@43730
    17
wenzelm@43730
    18
  type Sort = List[String]
wenzelm@43730
    19
  val dummyS: Sort = List("")
wenzelm@43730
    20
wenzelm@43730
    21
  sealed abstract class Typ
wenzelm@43730
    22
  case class Type(name: String, args: List[Typ] = Nil) extends Typ
wenzelm@43730
    23
  case class TFree(name: String, sort: Sort = dummyS) extends Typ
wenzelm@43730
    24
  case class TVar(name: Indexname, sort: Sort = dummyS) extends Typ
wenzelm@43730
    25
  val dummyT = Type("dummy")
wenzelm@43730
    26
wenzelm@43730
    27
  sealed abstract class Term
wenzelm@43730
    28
  case class Const(name: String, typ: Typ = dummyT) extends Term
wenzelm@43730
    29
  case class Free(name: String, typ: Typ = dummyT) extends Term
wenzelm@43730
    30
  case class Var(name: Indexname, typ: Typ = dummyT) extends Term
wenzelm@43730
    31
  case class Bound(index: Int) extends Term
wenzelm@43730
    32
  case class Abs(name: String, typ: Typ = dummyT, body: Term) extends Term
wenzelm@43730
    33
  case class App(fun: Term, arg: Term) extends Term
wenzelm@68265
    34
wenzelm@70533
    35
  sealed abstract class Proof
wenzelm@70533
    36
  case object MinProof extends Proof
wenzelm@70533
    37
  case class PBound(index: Int) extends Proof
wenzelm@70533
    38
  case class Abst(name: String, typ: Typ, body: Proof) extends Proof
wenzelm@70533
    39
  case class AbsP(name: String, hyp: Term, body: Proof) extends Proof
wenzelm@70533
    40
  case class Appt(fun: Proof, arg: Term) extends Proof
wenzelm@70533
    41
  case class AppP(fun: Proof, arg: Proof) extends Proof
wenzelm@70533
    42
  case class Hyp(hyp: Term) extends Proof
wenzelm@70533
    43
  case class PAxm(name: String, types: List[Typ]) extends Proof
wenzelm@70533
    44
  case class OfClass(typ: Typ, cls: String) extends Proof
wenzelm@70533
    45
  case class Oracle(name: String, prop: Term, types: List[Typ]) extends Proof
wenzelm@70533
    46
  case class PThm(serial: Long, pseudo_name: String, types: List[Typ]) extends Proof
wenzelm@70533
    47
wenzelm@68265
    48
wenzelm@70385
    49
  /* Pure logic */
wenzelm@70385
    50
wenzelm@70385
    51
  def itselfT(ty: Typ): Typ = Type(Pure_Thy.ITSELF, List(ty))
wenzelm@70385
    52
  val propT: Typ = Type(Pure_Thy.PROP, Nil)
wenzelm@70385
    53
  def funT(ty1: Typ, ty2: Typ): Typ = Type(Pure_Thy.FUN, List(ty1, ty2))
wenzelm@70385
    54
wenzelm@70385
    55
  def mk_type(ty: Typ): Term = Const(Pure_Thy.TYPE, itselfT(ty))
wenzelm@70385
    56
wenzelm@70385
    57
  def const_of_class(c: String): String = c + "_class"
wenzelm@70385
    58
wenzelm@70385
    59
  def mk_of_sort(ty: Typ, s: Sort): List[Term] =
wenzelm@70385
    60
  {
wenzelm@70385
    61
    val class_type = funT(itselfT(ty), propT)
wenzelm@70385
    62
    val t = mk_type(ty)
wenzelm@70385
    63
    s.map(c => App(Const(const_of_class(c), class_type), t))
wenzelm@70385
    64
  }
wenzelm@70385
    65
wenzelm@70385
    66
wenzelm@70383
    67
  /* type arguments of consts */
wenzelm@70383
    68
wenzelm@70383
    69
  def const_typargs(name: String, typ: Typ, typargs: List[String], decl: Typ): List[Typ] =
wenzelm@70383
    70
  {
wenzelm@70383
    71
    var subst = Map.empty[String, Typ]
wenzelm@70383
    72
wenzelm@70383
    73
    def bad_match(): Nothing = error("Malformed type instance for " + name + ": " + typ)
wenzelm@70383
    74
    def raw_match(arg: (Typ, Typ))
wenzelm@70383
    75
    {
wenzelm@70383
    76
      arg match {
wenzelm@70383
    77
        case (TFree(a, _), ty) =>
wenzelm@70383
    78
          subst.get(a) match {
wenzelm@70383
    79
            case None => subst += (a -> ty)
wenzelm@70383
    80
            case Some(ty1) => if (ty != ty1) bad_match()
wenzelm@70383
    81
          }
wenzelm@70383
    82
        case (Type(c1, args1), Type(c2, args2)) if c1 == c2 =>
wenzelm@70383
    83
          (args1 zip args2).foreach(raw_match)
wenzelm@70383
    84
        case _ => bad_match()
wenzelm@70383
    85
      }
wenzelm@70383
    86
    }
wenzelm@70383
    87
    raw_match(decl, typ)
wenzelm@70383
    88
wenzelm@70383
    89
    typargs.map(subst)
wenzelm@70383
    90
  }
wenzelm@70383
    91
wenzelm@70383
    92
wenzelm@68265
    93
wenzelm@68265
    94
  /** cache **/
wenzelm@68265
    95
wenzelm@68265
    96
  def make_cache(initial_size: Int = 131071, max_string: Int = Integer.MAX_VALUE): Cache =
wenzelm@68265
    97
    new Cache(initial_size, max_string)
wenzelm@68265
    98
wenzelm@68265
    99
  class Cache private[Term](initial_size: Int, max_string: Int)
wenzelm@68265
   100
    extends isabelle.Cache(initial_size, max_string)
wenzelm@68265
   101
  {
wenzelm@68265
   102
    protected def cache_indexname(x: Indexname): Indexname =
wenzelm@68265
   103
      lookup(x) getOrElse store(cache_string(x._1), cache_int(x._2))
wenzelm@68265
   104
wenzelm@68265
   105
    protected def cache_sort(x: Sort): Sort =
wenzelm@68265
   106
      if (x == dummyS) dummyS
wenzelm@68265
   107
      else lookup(x) getOrElse store(x.map(cache_string(_)))
wenzelm@68265
   108
wenzelm@68265
   109
    protected def cache_typ(x: Typ): Typ =
wenzelm@68265
   110
    {
wenzelm@68265
   111
      if (x == dummyT) dummyT
wenzelm@68265
   112
      else
wenzelm@68265
   113
        lookup(x) match {
wenzelm@68265
   114
          case Some(y) => y
wenzelm@68265
   115
          case None =>
wenzelm@68265
   116
            x match {
wenzelm@70533
   117
              case Type(name, args) => store(Type(cache_string(name), cache_typs(args)))
wenzelm@68265
   118
              case TFree(name, sort) => store(TFree(cache_string(name), cache_sort(sort)))
wenzelm@68265
   119
              case TVar(name, sort) => store(TVar(cache_indexname(name), cache_sort(sort)))
wenzelm@68265
   120
            }
wenzelm@68265
   121
        }
wenzelm@68265
   122
    }
wenzelm@68265
   123
wenzelm@70533
   124
    protected def cache_typs(x: List[Typ]): List[Typ] =
wenzelm@70533
   125
    {
wenzelm@70533
   126
      if (x.isEmpty) Nil
wenzelm@70533
   127
      else {
wenzelm@70533
   128
        lookup(x) match {
wenzelm@70533
   129
          case Some(y) => y
wenzelm@70533
   130
          case None => store(x.map(cache_typ(_)))
wenzelm@70533
   131
        }
wenzelm@70533
   132
      }
wenzelm@70533
   133
    }
wenzelm@70533
   134
wenzelm@68265
   135
    protected def cache_term(x: Term): Term =
wenzelm@68265
   136
    {
wenzelm@68265
   137
      lookup(x) match {
wenzelm@68265
   138
        case Some(y) => y
wenzelm@68265
   139
        case None =>
wenzelm@68265
   140
          x match {
wenzelm@68265
   141
            case Const(name, typ) => store(Const(cache_string(name), cache_typ(typ)))
wenzelm@68265
   142
            case Free(name, typ) => store(Free(cache_string(name), cache_typ(typ)))
wenzelm@68265
   143
            case Var(name, typ) => store(Var(cache_indexname(name), cache_typ(typ)))
wenzelm@68265
   144
            case Bound(index) => store(Bound(cache_int(index)))
wenzelm@68265
   145
            case Abs(name, typ, body) =>
wenzelm@68265
   146
              store(Abs(cache_string(name), cache_typ(typ), cache_term(body)))
wenzelm@68265
   147
            case App(fun, arg) => store(App(cache_term(fun), cache_term(arg)))
wenzelm@68265
   148
          }
wenzelm@68265
   149
      }
wenzelm@68265
   150
    }
wenzelm@68265
   151
wenzelm@70533
   152
    protected def cache_proof(x: Proof): Proof =
wenzelm@70533
   153
    {
wenzelm@70533
   154
      if (x == MinProof) MinProof
wenzelm@70533
   155
      else {
wenzelm@70533
   156
        lookup(x) match {
wenzelm@70533
   157
          case Some(y) => y
wenzelm@70533
   158
          case None =>
wenzelm@70533
   159
            x match {
wenzelm@70533
   160
              case MinProof => x
wenzelm@70533
   161
              case PBound(index) => store(PBound(cache_int(index)))
wenzelm@70533
   162
              case Abst(name, typ, body) =>
wenzelm@70533
   163
                store(Abst(cache_string(name), cache_typ(typ), cache_proof(body)))
wenzelm@70533
   164
              case AbsP(name, hyp, body) =>
wenzelm@70533
   165
                store(AbsP(cache_string(name), cache_term(hyp), cache_proof(body)))
wenzelm@70533
   166
              case Appt(fun, arg) => store(Appt(cache_proof(fun), cache_term(arg)))
wenzelm@70533
   167
              case AppP(fun, arg) => store(AppP(cache_proof(fun), cache_proof(arg)))
wenzelm@70533
   168
              case OfClass(typ, cls) => store(OfClass(cache_typ(typ), cache_string(cls)))
wenzelm@70533
   169
              case Oracle(name, prop, types) =>
wenzelm@70533
   170
                store(Oracle(cache_string(name), cache_term(prop), cache_typs(types)))
wenzelm@70533
   171
              case PThm(serial, name, types) =>
wenzelm@70533
   172
                store(PThm(serial, cache_string(name), cache_typs(types)))
wenzelm@70533
   173
            }
wenzelm@70533
   174
        }
wenzelm@70533
   175
      }
wenzelm@70533
   176
    }
wenzelm@70533
   177
wenzelm@68265
   178
    // main methods
wenzelm@68265
   179
    def indexname(x: Indexname): Indexname = synchronized { cache_indexname(x) }
wenzelm@68265
   180
    def sort(x: Sort): Sort = synchronized { cache_sort(x) }
wenzelm@68265
   181
    def typ(x: Typ): Typ = synchronized { cache_typ(x) }
wenzelm@68265
   182
    def term(x: Term): Term = synchronized { cache_term(x) }
wenzelm@70533
   183
    def proof(x: Proof): Proof = synchronized { cache_proof(x) }
wenzelm@68265
   184
wenzelm@68265
   185
    def position(x: Position.T): Position.T =
wenzelm@68265
   186
      synchronized { x.map({ case (a, b) => (cache_string(a), cache_string(b)) }) }
wenzelm@68265
   187
  }
wenzelm@43731
   188
}