src/Pure/term.scala
author wenzelm
Fri Apr 12 14:54:14 2013 +0200 (2013-04-12)
changeset 51700 c8f2bad67dbb
parent 43779 47bec02c6762
child 68265 f0899dad4877
permissions -rw-r--r--
tuned signature;
tuned comments;
     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