src/Pure/term.scala
author wenzelm
Wed, 31 Jul 2019 19:50:38 +0200
changeset 70451 550a5a822edb
parent 70385 68d2c533db9c
child 70533 031620901fcd
permissions -rw-r--r--
clarified export: retain proof boxes as local definitions -- more scalable;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43730
a0ed7bc688b5 lambda terms with XML data representation in Scala;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/term.scala
a0ed7bc688b5 lambda terms with XML data representation in Scala;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
a0ed7bc688b5 lambda terms with XML data representation in Scala;
wenzelm
parents:
diff changeset
     3
43779
47bec02c6762 more uniform Term and Term_XML modules;
wenzelm
parents: 43778
diff changeset
     4
Lambda terms, types, sorts.
43730
a0ed7bc688b5 lambda terms with XML data representation in Scala;
wenzelm
parents:
diff changeset
     5
a0ed7bc688b5 lambda terms with XML data representation in Scala;
wenzelm
parents:
diff changeset
     6
Note: Isabelle/ML is the primary environment for logical operations.
a0ed7bc688b5 lambda terms with XML data representation in Scala;
wenzelm
parents:
diff changeset
     7
*/
a0ed7bc688b5 lambda terms with XML data representation in Scala;
wenzelm
parents:
diff changeset
     8
a0ed7bc688b5 lambda terms with XML data representation in Scala;
wenzelm
parents:
diff changeset
     9
package isabelle
a0ed7bc688b5 lambda terms with XML data representation in Scala;
wenzelm
parents:
diff changeset
    10
a0ed7bc688b5 lambda terms with XML data representation in Scala;
wenzelm
parents:
diff changeset
    11
a0ed7bc688b5 lambda terms with XML data representation in Scala;
wenzelm
parents:
diff changeset
    12
object Term
a0ed7bc688b5 lambda terms with XML data representation in Scala;
wenzelm
parents:
diff changeset
    13
{
70383
38ac2e714729 more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);
wenzelm
parents: 68265
diff changeset
    14
  /* types and terms */
38ac2e714729 more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);
wenzelm
parents: 68265
diff changeset
    15
43730
a0ed7bc688b5 lambda terms with XML data representation in Scala;
wenzelm
parents:
diff changeset
    16
  type Indexname = (String, Int)
a0ed7bc688b5 lambda terms with XML data representation in Scala;
wenzelm
parents:
diff changeset
    17
a0ed7bc688b5 lambda terms with XML data representation in Scala;
wenzelm
parents:
diff changeset
    18
  type Sort = List[String]
a0ed7bc688b5 lambda terms with XML data representation in Scala;
wenzelm
parents:
diff changeset
    19
  val dummyS: Sort = List("")
a0ed7bc688b5 lambda terms with XML data representation in Scala;
wenzelm
parents:
diff changeset
    20
a0ed7bc688b5 lambda terms with XML data representation in Scala;
wenzelm
parents:
diff changeset
    21
  sealed abstract class Typ
a0ed7bc688b5 lambda terms with XML data representation in Scala;
wenzelm
parents:
diff changeset
    22
  case class Type(name: String, args: List[Typ] = Nil) extends Typ
a0ed7bc688b5 lambda terms with XML data representation in Scala;
wenzelm
parents:
diff changeset
    23
  case class TFree(name: String, sort: Sort = dummyS) extends Typ
a0ed7bc688b5 lambda terms with XML data representation in Scala;
wenzelm
parents:
diff changeset
    24
  case class TVar(name: Indexname, sort: Sort = dummyS) extends Typ
a0ed7bc688b5 lambda terms with XML data representation in Scala;
wenzelm
parents:
diff changeset
    25
  val dummyT = Type("dummy")
a0ed7bc688b5 lambda terms with XML data representation in Scala;
wenzelm
parents:
diff changeset
    26
a0ed7bc688b5 lambda terms with XML data representation in Scala;
wenzelm
parents:
diff changeset
    27
  sealed abstract class Term
a0ed7bc688b5 lambda terms with XML data representation in Scala;
wenzelm
parents:
diff changeset
    28
  case class Const(name: String, typ: Typ = dummyT) extends Term
a0ed7bc688b5 lambda terms with XML data representation in Scala;
wenzelm
parents:
diff changeset
    29
  case class Free(name: String, typ: Typ = dummyT) extends Term
a0ed7bc688b5 lambda terms with XML data representation in Scala;
wenzelm
parents:
diff changeset
    30
  case class Var(name: Indexname, typ: Typ = dummyT) extends Term
a0ed7bc688b5 lambda terms with XML data representation in Scala;
wenzelm
parents:
diff changeset
    31
  case class Bound(index: Int) extends Term
a0ed7bc688b5 lambda terms with XML data representation in Scala;
wenzelm
parents:
diff changeset
    32
  case class Abs(name: String, typ: Typ = dummyT, body: Term) extends Term
a0ed7bc688b5 lambda terms with XML data representation in Scala;
wenzelm
parents:
diff changeset
    33
  case class App(fun: Term, arg: Term) extends Term
68265
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents: 43779
diff changeset
    34
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents: 43779
diff changeset
    35
70385
68d2c533db9c more operations: support type classes within the logic;
wenzelm
parents: 70383
diff changeset
    36
  /* Pure logic */
68d2c533db9c more operations: support type classes within the logic;
wenzelm
parents: 70383
diff changeset
    37
68d2c533db9c more operations: support type classes within the logic;
wenzelm
parents: 70383
diff changeset
    38
  def itselfT(ty: Typ): Typ = Type(Pure_Thy.ITSELF, List(ty))
68d2c533db9c more operations: support type classes within the logic;
wenzelm
parents: 70383
diff changeset
    39
  val propT: Typ = Type(Pure_Thy.PROP, Nil)
68d2c533db9c more operations: support type classes within the logic;
wenzelm
parents: 70383
diff changeset
    40
  def funT(ty1: Typ, ty2: Typ): Typ = Type(Pure_Thy.FUN, List(ty1, ty2))
68d2c533db9c more operations: support type classes within the logic;
wenzelm
parents: 70383
diff changeset
    41
68d2c533db9c more operations: support type classes within the logic;
wenzelm
parents: 70383
diff changeset
    42
  def mk_type(ty: Typ): Term = Const(Pure_Thy.TYPE, itselfT(ty))
68d2c533db9c more operations: support type classes within the logic;
wenzelm
parents: 70383
diff changeset
    43
68d2c533db9c more operations: support type classes within the logic;
wenzelm
parents: 70383
diff changeset
    44
  def const_of_class(c: String): String = c + "_class"
68d2c533db9c more operations: support type classes within the logic;
wenzelm
parents: 70383
diff changeset
    45
68d2c533db9c more operations: support type classes within the logic;
wenzelm
parents: 70383
diff changeset
    46
  def mk_of_sort(ty: Typ, s: Sort): List[Term] =
68d2c533db9c more operations: support type classes within the logic;
wenzelm
parents: 70383
diff changeset
    47
  {
68d2c533db9c more operations: support type classes within the logic;
wenzelm
parents: 70383
diff changeset
    48
    val class_type = funT(itselfT(ty), propT)
68d2c533db9c more operations: support type classes within the logic;
wenzelm
parents: 70383
diff changeset
    49
    val t = mk_type(ty)
68d2c533db9c more operations: support type classes within the logic;
wenzelm
parents: 70383
diff changeset
    50
    s.map(c => App(Const(const_of_class(c), class_type), t))
68d2c533db9c more operations: support type classes within the logic;
wenzelm
parents: 70383
diff changeset
    51
  }
68d2c533db9c more operations: support type classes within the logic;
wenzelm
parents: 70383
diff changeset
    52
68d2c533db9c more operations: support type classes within the logic;
wenzelm
parents: 70383
diff changeset
    53
70383
38ac2e714729 more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);
wenzelm
parents: 68265
diff changeset
    54
  /* type arguments of consts */
38ac2e714729 more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);
wenzelm
parents: 68265
diff changeset
    55
38ac2e714729 more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);
wenzelm
parents: 68265
diff changeset
    56
  def const_typargs(name: String, typ: Typ, typargs: List[String], decl: Typ): List[Typ] =
38ac2e714729 more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);
wenzelm
parents: 68265
diff changeset
    57
  {
38ac2e714729 more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);
wenzelm
parents: 68265
diff changeset
    58
    var subst = Map.empty[String, Typ]
38ac2e714729 more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);
wenzelm
parents: 68265
diff changeset
    59
38ac2e714729 more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);
wenzelm
parents: 68265
diff changeset
    60
    def bad_match(): Nothing = error("Malformed type instance for " + name + ": " + typ)
38ac2e714729 more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);
wenzelm
parents: 68265
diff changeset
    61
    def raw_match(arg: (Typ, Typ))
38ac2e714729 more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);
wenzelm
parents: 68265
diff changeset
    62
    {
38ac2e714729 more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);
wenzelm
parents: 68265
diff changeset
    63
      arg match {
38ac2e714729 more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);
wenzelm
parents: 68265
diff changeset
    64
        case (TFree(a, _), ty) =>
38ac2e714729 more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);
wenzelm
parents: 68265
diff changeset
    65
          subst.get(a) match {
38ac2e714729 more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);
wenzelm
parents: 68265
diff changeset
    66
            case None => subst += (a -> ty)
38ac2e714729 more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);
wenzelm
parents: 68265
diff changeset
    67
            case Some(ty1) => if (ty != ty1) bad_match()
38ac2e714729 more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);
wenzelm
parents: 68265
diff changeset
    68
          }
38ac2e714729 more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);
wenzelm
parents: 68265
diff changeset
    69
        case (Type(c1, args1), Type(c2, args2)) if c1 == c2 =>
38ac2e714729 more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);
wenzelm
parents: 68265
diff changeset
    70
          (args1 zip args2).foreach(raw_match)
38ac2e714729 more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);
wenzelm
parents: 68265
diff changeset
    71
        case _ => bad_match()
38ac2e714729 more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);
wenzelm
parents: 68265
diff changeset
    72
      }
38ac2e714729 more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);
wenzelm
parents: 68265
diff changeset
    73
    }
38ac2e714729 more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);
wenzelm
parents: 68265
diff changeset
    74
    raw_match(decl, typ)
38ac2e714729 more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);
wenzelm
parents: 68265
diff changeset
    75
38ac2e714729 more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);
wenzelm
parents: 68265
diff changeset
    76
    typargs.map(subst)
38ac2e714729 more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);
wenzelm
parents: 68265
diff changeset
    77
  }
38ac2e714729 more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);
wenzelm
parents: 68265
diff changeset
    78
38ac2e714729 more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);
wenzelm
parents: 68265
diff changeset
    79
68265
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents: 43779
diff changeset
    80
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents: 43779
diff changeset
    81
  /** cache **/
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents: 43779
diff changeset
    82
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents: 43779
diff changeset
    83
  def make_cache(initial_size: Int = 131071, max_string: Int = Integer.MAX_VALUE): Cache =
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents: 43779
diff changeset
    84
    new Cache(initial_size, max_string)
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents: 43779
diff changeset
    85
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents: 43779
diff changeset
    86
  class Cache private[Term](initial_size: Int, max_string: Int)
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents: 43779
diff changeset
    87
    extends isabelle.Cache(initial_size, max_string)
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents: 43779
diff changeset
    88
  {
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents: 43779
diff changeset
    89
    protected def cache_indexname(x: Indexname): Indexname =
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents: 43779
diff changeset
    90
      lookup(x) getOrElse store(cache_string(x._1), cache_int(x._2))
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents: 43779
diff changeset
    91
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents: 43779
diff changeset
    92
    protected def cache_sort(x: Sort): Sort =
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents: 43779
diff changeset
    93
      if (x == dummyS) dummyS
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents: 43779
diff changeset
    94
      else lookup(x) getOrElse store(x.map(cache_string(_)))
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents: 43779
diff changeset
    95
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents: 43779
diff changeset
    96
    protected def cache_typ(x: Typ): Typ =
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents: 43779
diff changeset
    97
    {
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents: 43779
diff changeset
    98
      if (x == dummyT) dummyT
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents: 43779
diff changeset
    99
      else
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents: 43779
diff changeset
   100
        lookup(x) match {
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents: 43779
diff changeset
   101
          case Some(y) => y
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents: 43779
diff changeset
   102
          case None =>
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents: 43779
diff changeset
   103
            x match {
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents: 43779
diff changeset
   104
              case Type(name, args) => store(Type(cache_string(name), args.map(cache_typ(_))))
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents: 43779
diff changeset
   105
              case TFree(name, sort) => store(TFree(cache_string(name), cache_sort(sort)))
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents: 43779
diff changeset
   106
              case TVar(name, sort) => store(TVar(cache_indexname(name), cache_sort(sort)))
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents: 43779
diff changeset
   107
            }
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents: 43779
diff changeset
   108
        }
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents: 43779
diff changeset
   109
    }
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents: 43779
diff changeset
   110
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents: 43779
diff changeset
   111
    protected def cache_term(x: Term): Term =
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents: 43779
diff changeset
   112
    {
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents: 43779
diff changeset
   113
      lookup(x) match {
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents: 43779
diff changeset
   114
        case Some(y) => y
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents: 43779
diff changeset
   115
        case None =>
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents: 43779
diff changeset
   116
          x match {
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents: 43779
diff changeset
   117
            case Const(name, typ) => store(Const(cache_string(name), cache_typ(typ)))
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents: 43779
diff changeset
   118
            case Free(name, typ) => store(Free(cache_string(name), cache_typ(typ)))
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents: 43779
diff changeset
   119
            case Var(name, typ) => store(Var(cache_indexname(name), cache_typ(typ)))
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents: 43779
diff changeset
   120
            case Bound(index) => store(Bound(cache_int(index)))
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents: 43779
diff changeset
   121
            case Abs(name, typ, body) =>
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents: 43779
diff changeset
   122
              store(Abs(cache_string(name), cache_typ(typ), cache_term(body)))
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents: 43779
diff changeset
   123
            case App(fun, arg) => store(App(cache_term(fun), cache_term(arg)))
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents: 43779
diff changeset
   124
          }
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents: 43779
diff changeset
   125
      }
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents: 43779
diff changeset
   126
    }
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents: 43779
diff changeset
   127
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents: 43779
diff changeset
   128
    // main methods
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents: 43779
diff changeset
   129
    def indexname(x: Indexname): Indexname = synchronized { cache_indexname(x) }
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents: 43779
diff changeset
   130
    def sort(x: Sort): Sort = synchronized { cache_sort(x) }
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents: 43779
diff changeset
   131
    def typ(x: Typ): Typ = synchronized { cache_typ(x) }
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents: 43779
diff changeset
   132
    def term(x: Term): Term = synchronized { cache_term(x) }
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents: 43779
diff changeset
   133
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents: 43779
diff changeset
   134
    def position(x: Position.T): Position.T =
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents: 43779
diff changeset
   135
      synchronized { x.map({ case (a, b) => (cache_string(a), cache_string(b)) }) }
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents: 43779
diff changeset
   136
  }
43731
70072780e095 inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents: 43730
diff changeset
   137
}