1/*  Title:      Pure/term.scala
2    Author:     Makarius
3
4Lambda terms, types, sorts.
5
6Note: Isabelle/ML is the primary environment for logical operations.
7*/
8
9package isabelle
10
11
12object Term
13{
14  /* types and terms */
15
16  sealed case class Indexname(name: String, index: Int = 0)
17  {
18    override def toString: String =
19      if (index == -1) name
20      else {
21        val dot =
22          Symbol.explode(name).reverse match {
23            case _ :: s :: _ if s == Symbol.sub_decoded || s == Symbol.sub => false
24            case c :: _ => Symbol.is_digit(c)
25            case _ => true
26          }
27        if (dot) "?" + name + "." + index
28        else if (index != 0) "?" + name + index
29        else "?" + name
30      }
31  }
32
33  type Class = String
34  type Sort = List[Class]
35
36  sealed abstract class Typ
37  case class Type(name: String, args: List[Typ] = Nil) extends Typ
38  {
39    override def toString: String =
40      if (this == dummyT) "_"
41      else "Type(" + name + (if (args.isEmpty) "" else "," + args) + ")"
42  }
43  case class TFree(name: String, sort: Sort = Nil) extends Typ
44  {
45    override def toString: String =
46      "TFree(" + name + (if (sort.isEmpty) "" else "," + sort) + ")"
47  }
48  case class TVar(name: Indexname, sort: Sort = Nil) extends Typ
49  {
50    override def toString: String =
51      "TVar(" + name + (if (sort.isEmpty) "" else "," + sort) + ")"
52  }
53  val dummyT = Type("dummy")
54
55  sealed abstract class Term
56  {
57    def head: Term =
58      this match {
59        case App(fun, _) => fun.head
60        case _ => this
61      }
62  }
63  case class Const(name: String, typargs: List[Typ] = Nil) extends Term
64  {
65    override def toString: String =
66      if (this == dummy) "_"
67      else "Const(" + name + (if (typargs.isEmpty) "" else "," + typargs) + ")"
68  }
69  case class Free(name: String, typ: Typ = dummyT) extends Term
70  {
71    override def toString: String =
72      "Free(" + name + (if (typ == dummyT) "" else "," + typ) + ")"
73  }
74  case class Var(name: Indexname, typ: Typ = dummyT) extends Term
75  {
76    override def toString: String =
77      "Var(" + name + (if (typ == dummyT) "" else "," + typ) + ")"
78  }
79  case class Bound(index: Int) extends Term
80  case class Abs(name: String, typ: Typ, body: Term) extends Term
81  case class App(fun: Term, arg: Term) extends Term
82  {
83    override def toString: String =
84      this match {
85        case OFCLASS(ty, c) => "OFCLASS(" + ty + "," + c + ")"
86        case _ => "App(" + fun + "," + arg + ")"
87      }
88  }
89
90  def dummy_pattern(ty: Typ): Term = Const("Pure.dummy_pattern", List(ty))
91  val dummy: Term = dummy_pattern(dummyT)
92
93  sealed abstract class Proof
94  case object MinProof extends Proof
95  case class PBound(index: Int) extends Proof
96  case class Abst(name: String, typ: Typ, body: Proof) extends Proof
97  case class AbsP(name: String, hyp: Term, body: Proof) extends Proof
98  case class Appt(fun: Proof, arg: Term) extends Proof
99  case class AppP(fun: Proof, arg: Proof) extends Proof
100  case class Hyp(hyp: Term) extends Proof
101  case class PAxm(name: String, types: List[Typ]) extends Proof
102  case class OfClass(typ: Typ, cls: Class) extends Proof
103  case class Oracle(name: String, prop: Term, types: List[Typ]) extends Proof
104  case class PThm(serial: Long, theory_name: String, name: String, types: List[Typ]) extends Proof
105
106
107  /* type classes within the logic */
108
109  object Class_Const
110  {
111    val suffix = "_class"
112    def apply(c: Class): String = c + suffix
113    def unapply(s: String): Option[Class] =
114      if (s.endsWith(suffix)) Some(s.substring(0, s.length - suffix.length)) else None
115  }
116
117  object OFCLASS
118  {
119    def apply(ty: Typ, s: Sort): List[Term] = s.map(c => apply(ty, c))
120
121    def apply(ty: Typ, c: Class): Term =
122      App(Const(Class_Const(c), List(ty)), Const(Pure_Thy.TYPE, List(ty)))
123
124    def unapply(t: Term): Option[(Typ, String)] =
125      t match {
126        case App(Const(Class_Const(c), List(ty)), Const(Pure_Thy.TYPE, List(ty1)))
127        if ty == ty1 => Some((ty, c))
128        case _ => None
129      }
130  }
131
132
133
134  /** cache **/
135
136  def make_cache(initial_size: Int = 131071, max_string: Int = Integer.MAX_VALUE): Cache =
137    new Cache(initial_size, max_string)
138
139  class Cache private[Term](initial_size: Int, max_string: Int)
140    extends isabelle.Cache(initial_size, max_string)
141  {
142    protected def cache_indexname(x: Indexname): Indexname =
143      lookup(x) getOrElse store(Indexname(cache_string(x.name), x.index))
144
145    protected def cache_sort(x: Sort): Sort =
146      if (x.isEmpty) Nil else lookup(x) getOrElse store(x.map(cache_string(_)))
147
148    protected def cache_typ(x: Typ): Typ =
149    {
150      if (x == dummyT) dummyT
151      else
152        lookup(x) match {
153          case Some(y) => y
154          case None =>
155            x match {
156              case Type(name, args) => store(Type(cache_string(name), cache_typs(args)))
157              case TFree(name, sort) => store(TFree(cache_string(name), cache_sort(sort)))
158              case TVar(name, sort) => store(TVar(cache_indexname(name), cache_sort(sort)))
159            }
160        }
161    }
162
163    protected def cache_typs(x: List[Typ]): List[Typ] =
164    {
165      if (x.isEmpty) Nil
166      else {
167        lookup(x) match {
168          case Some(y) => y
169          case None => store(x.map(cache_typ(_)))
170        }
171      }
172    }
173
174    protected def cache_term(x: Term): Term =
175    {
176      lookup(x) match {
177        case Some(y) => y
178        case None =>
179          x match {
180            case Const(name, typargs) => store(Const(cache_string(name), cache_typs(typargs)))
181            case Free(name, typ) => store(Free(cache_string(name), cache_typ(typ)))
182            case Var(name, typ) => store(Var(cache_indexname(name), cache_typ(typ)))
183            case Bound(_) => store(x)
184            case Abs(name, typ, body) =>
185              store(Abs(cache_string(name), cache_typ(typ), cache_term(body)))
186            case App(fun, arg) => store(App(cache_term(fun), cache_term(arg)))
187          }
188      }
189    }
190
191    protected def cache_proof(x: Proof): Proof =
192    {
193      if (x == MinProof) MinProof
194      else {
195        lookup(x) match {
196          case Some(y) => y
197          case None =>
198            x match {
199              case PBound(_) => store(x)
200              case Abst(name, typ, body) =>
201                store(Abst(cache_string(name), cache_typ(typ), cache_proof(body)))
202              case AbsP(name, hyp, body) =>
203                store(AbsP(cache_string(name), cache_term(hyp), cache_proof(body)))
204              case Appt(fun, arg) => store(Appt(cache_proof(fun), cache_term(arg)))
205              case AppP(fun, arg) => store(AppP(cache_proof(fun), cache_proof(arg)))
206              case Hyp(hyp) => store(Hyp(cache_term(hyp)))
207              case PAxm(name, types) => store(PAxm(cache_string(name), cache_typs(types)))
208              case OfClass(typ, cls) => store(OfClass(cache_typ(typ), cache_string(cls)))
209              case Oracle(name, prop, types) =>
210                store(Oracle(cache_string(name), cache_term(prop), cache_typs(types)))
211              case PThm(serial, theory_name, name, types) =>
212                store(PThm(serial, cache_string(theory_name), cache_string(name), cache_typs(types)))
213            }
214        }
215      }
216    }
217
218    // main methods
219    def indexname(x: Indexname): Indexname = synchronized { cache_indexname(x) }
220    def sort(x: Sort): Sort = synchronized { cache_sort(x) }
221    def typ(x: Typ): Typ = synchronized { cache_typ(x) }
222    def term(x: Term): Term = synchronized { cache_term(x) }
223    def proof(x: Proof): Proof = synchronized { cache_proof(x) }
224
225    def position(x: Position.T): Position.T =
226      synchronized { x.map({ case (a, b) => (cache_string(a), cache_string(b)) }) }
227  }
228}
229