src/Pure/term.scala
author wenzelm
Sat Jul 20 14:03:51 2019 +0200 (4 months ago)
changeset 70385 68d2c533db9c
parent 70383 38ac2e714729
child 70533 031620901fcd
permissions -rw-r--r--
more operations: support type classes within the logic;
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@68265
    35
wenzelm@70385
    36
  /* Pure logic */
wenzelm@70385
    37
wenzelm@70385
    38
  def itselfT(ty: Typ): Typ = Type(Pure_Thy.ITSELF, List(ty))
wenzelm@70385
    39
  val propT: Typ = Type(Pure_Thy.PROP, Nil)
wenzelm@70385
    40
  def funT(ty1: Typ, ty2: Typ): Typ = Type(Pure_Thy.FUN, List(ty1, ty2))
wenzelm@70385
    41
wenzelm@70385
    42
  def mk_type(ty: Typ): Term = Const(Pure_Thy.TYPE, itselfT(ty))
wenzelm@70385
    43
wenzelm@70385
    44
  def const_of_class(c: String): String = c + "_class"
wenzelm@70385
    45
wenzelm@70385
    46
  def mk_of_sort(ty: Typ, s: Sort): List[Term] =
wenzelm@70385
    47
  {
wenzelm@70385
    48
    val class_type = funT(itselfT(ty), propT)
wenzelm@70385
    49
    val t = mk_type(ty)
wenzelm@70385
    50
    s.map(c => App(Const(const_of_class(c), class_type), t))
wenzelm@70385
    51
  }
wenzelm@70385
    52
wenzelm@70385
    53
wenzelm@70383
    54
  /* type arguments of consts */
wenzelm@70383
    55
wenzelm@70383
    56
  def const_typargs(name: String, typ: Typ, typargs: List[String], decl: Typ): List[Typ] =
wenzelm@70383
    57
  {
wenzelm@70383
    58
    var subst = Map.empty[String, Typ]
wenzelm@70383
    59
wenzelm@70383
    60
    def bad_match(): Nothing = error("Malformed type instance for " + name + ": " + typ)
wenzelm@70383
    61
    def raw_match(arg: (Typ, Typ))
wenzelm@70383
    62
    {
wenzelm@70383
    63
      arg match {
wenzelm@70383
    64
        case (TFree(a, _), ty) =>
wenzelm@70383
    65
          subst.get(a) match {
wenzelm@70383
    66
            case None => subst += (a -> ty)
wenzelm@70383
    67
            case Some(ty1) => if (ty != ty1) bad_match()
wenzelm@70383
    68
          }
wenzelm@70383
    69
        case (Type(c1, args1), Type(c2, args2)) if c1 == c2 =>
wenzelm@70383
    70
          (args1 zip args2).foreach(raw_match)
wenzelm@70383
    71
        case _ => bad_match()
wenzelm@70383
    72
      }
wenzelm@70383
    73
    }
wenzelm@70383
    74
    raw_match(decl, typ)
wenzelm@70383
    75
wenzelm@70383
    76
    typargs.map(subst)
wenzelm@70383
    77
  }
wenzelm@70383
    78
wenzelm@70383
    79
wenzelm@68265
    80
wenzelm@68265
    81
  /** cache **/
wenzelm@68265
    82
wenzelm@68265
    83
  def make_cache(initial_size: Int = 131071, max_string: Int = Integer.MAX_VALUE): Cache =
wenzelm@68265
    84
    new Cache(initial_size, max_string)
wenzelm@68265
    85
wenzelm@68265
    86
  class Cache private[Term](initial_size: Int, max_string: Int)
wenzelm@68265
    87
    extends isabelle.Cache(initial_size, max_string)
wenzelm@68265
    88
  {
wenzelm@68265
    89
    protected def cache_indexname(x: Indexname): Indexname =
wenzelm@68265
    90
      lookup(x) getOrElse store(cache_string(x._1), cache_int(x._2))
wenzelm@68265
    91
wenzelm@68265
    92
    protected def cache_sort(x: Sort): Sort =
wenzelm@68265
    93
      if (x == dummyS) dummyS
wenzelm@68265
    94
      else lookup(x) getOrElse store(x.map(cache_string(_)))
wenzelm@68265
    95
wenzelm@68265
    96
    protected def cache_typ(x: Typ): Typ =
wenzelm@68265
    97
    {
wenzelm@68265
    98
      if (x == dummyT) dummyT
wenzelm@68265
    99
      else
wenzelm@68265
   100
        lookup(x) match {
wenzelm@68265
   101
          case Some(y) => y
wenzelm@68265
   102
          case None =>
wenzelm@68265
   103
            x match {
wenzelm@68265
   104
              case Type(name, args) => store(Type(cache_string(name), args.map(cache_typ(_))))
wenzelm@68265
   105
              case TFree(name, sort) => store(TFree(cache_string(name), cache_sort(sort)))
wenzelm@68265
   106
              case TVar(name, sort) => store(TVar(cache_indexname(name), cache_sort(sort)))
wenzelm@68265
   107
            }
wenzelm@68265
   108
        }
wenzelm@68265
   109
    }
wenzelm@68265
   110
wenzelm@68265
   111
    protected def cache_term(x: Term): Term =
wenzelm@68265
   112
    {
wenzelm@68265
   113
      lookup(x) match {
wenzelm@68265
   114
        case Some(y) => y
wenzelm@68265
   115
        case None =>
wenzelm@68265
   116
          x match {
wenzelm@68265
   117
            case Const(name, typ) => store(Const(cache_string(name), cache_typ(typ)))
wenzelm@68265
   118
            case Free(name, typ) => store(Free(cache_string(name), cache_typ(typ)))
wenzelm@68265
   119
            case Var(name, typ) => store(Var(cache_indexname(name), cache_typ(typ)))
wenzelm@68265
   120
            case Bound(index) => store(Bound(cache_int(index)))
wenzelm@68265
   121
            case Abs(name, typ, body) =>
wenzelm@68265
   122
              store(Abs(cache_string(name), cache_typ(typ), cache_term(body)))
wenzelm@68265
   123
            case App(fun, arg) => store(App(cache_term(fun), cache_term(arg)))
wenzelm@68265
   124
          }
wenzelm@68265
   125
      }
wenzelm@68265
   126
    }
wenzelm@68265
   127
wenzelm@68265
   128
    // main methods
wenzelm@68265
   129
    def indexname(x: Indexname): Indexname = synchronized { cache_indexname(x) }
wenzelm@68265
   130
    def sort(x: Sort): Sort = synchronized { cache_sort(x) }
wenzelm@68265
   131
    def typ(x: Typ): Typ = synchronized { cache_typ(x) }
wenzelm@68265
   132
    def term(x: Term): Term = synchronized { cache_term(x) }
wenzelm@68265
   133
wenzelm@68265
   134
    def position(x: Position.T): Position.T =
wenzelm@68265
   135
      synchronized { x.map({ case (a, b) => (cache_string(a), cache_string(b)) }) }
wenzelm@68265
   136
  }
wenzelm@43731
   137
}