src/Pure/term.scala
author wenzelm
Tue Jul 12 18:00:05 2011 +0200 (2011-07-12)
changeset 43779 47bec02c6762
parent 43778 ce9189450447
child 68265 f0899dad4877
permissions -rw-r--r--
more uniform Term and Term_XML modules;
     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