src/Pure/term.scala
author wenzelm
Thu May 24 21:13:09 2018 +0200 (16 months ago)
changeset 68265 f0899dad4877
parent 43779 47bec02c6762
child 70383 38ac2e714729
permissions -rw-r--r--
more general cache, also for term substructures;
     1 /*  Title:      Pure/term.scala
     2     Author:     Makarius
     3 
     4 Lambda terms, types, sorts.
     5 
     6 Note: Isabelle/ML is the primary environment for logical operations.
     7 */
     8 
     9 package isabelle
    10 
    11 
    12 object Term
    13 {
    14   type Indexname = (String, Int)
    15 
    16   type Sort = List[String]
    17   val dummyS: Sort = List("")
    18 
    19   sealed abstract class Typ
    20   case class Type(name: String, args: List[Typ] = Nil) extends Typ
    21   case class TFree(name: String, sort: Sort = dummyS) extends Typ
    22   case class TVar(name: Indexname, sort: Sort = dummyS) extends Typ
    23   val dummyT = Type("dummy")
    24 
    25   sealed abstract class Term
    26   case class Const(name: String, typ: Typ = dummyT) extends Term
    27   case class Free(name: String, typ: Typ = dummyT) extends Term
    28   case class Var(name: Indexname, typ: Typ = dummyT) extends Term
    29   case class Bound(index: Int) extends Term
    30   case class Abs(name: String, typ: Typ = dummyT, body: Term) extends Term
    31   case class App(fun: Term, arg: Term) extends Term
    32 
    33 
    34 
    35   /** cache **/
    36 
    37   def make_cache(initial_size: Int = 131071, max_string: Int = Integer.MAX_VALUE): Cache =
    38     new Cache(initial_size, max_string)
    39 
    40   class Cache private[Term](initial_size: Int, max_string: Int)
    41     extends isabelle.Cache(initial_size, max_string)
    42   {
    43     protected def cache_indexname(x: Indexname): Indexname =
    44       lookup(x) getOrElse store(cache_string(x._1), cache_int(x._2))
    45 
    46     protected def cache_sort(x: Sort): Sort =
    47       if (x == dummyS) dummyS
    48       else lookup(x) getOrElse store(x.map(cache_string(_)))
    49 
    50     protected def cache_typ(x: Typ): Typ =
    51     {
    52       if (x == dummyT) dummyT
    53       else
    54         lookup(x) match {
    55           case Some(y) => y
    56           case None =>
    57             x match {
    58               case Type(name, args) => store(Type(cache_string(name), args.map(cache_typ(_))))
    59               case TFree(name, sort) => store(TFree(cache_string(name), cache_sort(sort)))
    60               case TVar(name, sort) => store(TVar(cache_indexname(name), cache_sort(sort)))
    61             }
    62         }
    63     }
    64 
    65     protected def cache_term(x: Term): Term =
    66     {
    67       lookup(x) match {
    68         case Some(y) => y
    69         case None =>
    70           x match {
    71             case Const(name, typ) => store(Const(cache_string(name), cache_typ(typ)))
    72             case Free(name, typ) => store(Free(cache_string(name), cache_typ(typ)))
    73             case Var(name, typ) => store(Var(cache_indexname(name), cache_typ(typ)))
    74             case Bound(index) => store(Bound(cache_int(index)))
    75             case Abs(name, typ, body) =>
    76               store(Abs(cache_string(name), cache_typ(typ), cache_term(body)))
    77             case App(fun, arg) => store(App(cache_term(fun), cache_term(arg)))
    78           }
    79       }
    80     }
    81 
    82     // main methods
    83     def indexname(x: Indexname): Indexname = synchronized { cache_indexname(x) }
    84     def sort(x: Sort): Sort = synchronized { cache_sort(x) }
    85     def typ(x: Typ): Typ = synchronized { cache_typ(x) }
    86     def term(x: Term): Term = synchronized { cache_term(x) }
    87 
    88     def position(x: Position.T): Position.T =
    89       synchronized { x.map({ case (a, b) => (cache_string(a), cache_string(b)) }) }
    90   }
    91 }