src/Pure/term.scala
author wenzelm
Tue Sep 26 20:54:40 2017 +0200 (22 months ago)
changeset 66695 91500c024c7f
parent 43779 47bec02c6762
child 68265 f0899dad4877
permissions -rw-r--r--
tuned;
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@43730
    14
  type Indexname = (String, Int)
wenzelm@43730
    15
wenzelm@43730
    16
  type Sort = List[String]
wenzelm@43730
    17
  val dummyS: Sort = List("")
wenzelm@43730
    18
wenzelm@43730
    19
  sealed abstract class Typ
wenzelm@43730
    20
  case class Type(name: String, args: List[Typ] = Nil) extends Typ
wenzelm@43730
    21
  case class TFree(name: String, sort: Sort = dummyS) extends Typ
wenzelm@43730
    22
  case class TVar(name: Indexname, sort: Sort = dummyS) extends Typ
wenzelm@43730
    23
  val dummyT = Type("dummy")
wenzelm@43730
    24
wenzelm@43730
    25
  sealed abstract class Term
wenzelm@43730
    26
  case class Const(name: String, typ: Typ = dummyT) extends Term
wenzelm@43730
    27
  case class Free(name: String, typ: Typ = dummyT) extends Term
wenzelm@43730
    28
  case class Var(name: Indexname, typ: Typ = dummyT) extends Term
wenzelm@43730
    29
  case class Bound(index: Int) extends Term
wenzelm@43730
    30
  case class Abs(name: String, typ: Typ = dummyT, body: Term) extends Term
wenzelm@43730
    31
  case class App(fun: Term, arg: Term) extends Term
wenzelm@43731
    32
}
wenzelm@43731
    33