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