src/Pure/term.scala
author wenzelm
Sun, 22 Jul 2012 12:26:41 +0200
changeset 48423 0ccf143a2a69
parent 43779 47bec02c6762
child 68265 f0899dad4877
permissions -rw-r--r--
maintain set of source digests, including relevant parts of session entry;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43730
a0ed7bc688b5 lambda terms with XML data representation in Scala;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/term.scala
a0ed7bc688b5 lambda terms with XML data representation in Scala;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
a0ed7bc688b5 lambda terms with XML data representation in Scala;
wenzelm
parents:
diff changeset
     3
43779
47bec02c6762 more uniform Term and Term_XML modules;
wenzelm
parents: 43778
diff changeset
     4
Lambda terms, types, sorts.
43730
a0ed7bc688b5 lambda terms with XML data representation in Scala;
wenzelm
parents:
diff changeset
     5
a0ed7bc688b5 lambda terms with XML data representation in Scala;
wenzelm
parents:
diff changeset
     6
Note: Isabelle/ML is the primary environment for logical operations.
a0ed7bc688b5 lambda terms with XML data representation in Scala;
wenzelm
parents:
diff changeset
     7
*/
a0ed7bc688b5 lambda terms with XML data representation in Scala;
wenzelm
parents:
diff changeset
     8
a0ed7bc688b5 lambda terms with XML data representation in Scala;
wenzelm
parents:
diff changeset
     9
package isabelle
a0ed7bc688b5 lambda terms with XML data representation in Scala;
wenzelm
parents:
diff changeset
    10
a0ed7bc688b5 lambda terms with XML data representation in Scala;
wenzelm
parents:
diff changeset
    11
a0ed7bc688b5 lambda terms with XML data representation in Scala;
wenzelm
parents:
diff changeset
    12
object Term
a0ed7bc688b5 lambda terms with XML data representation in Scala;
wenzelm
parents:
diff changeset
    13
{
a0ed7bc688b5 lambda terms with XML data representation in Scala;
wenzelm
parents:
diff changeset
    14
  type Indexname = (String, Int)
a0ed7bc688b5 lambda terms with XML data representation in Scala;
wenzelm
parents:
diff changeset
    15
a0ed7bc688b5 lambda terms with XML data representation in Scala;
wenzelm
parents:
diff changeset
    16
  type Sort = List[String]
a0ed7bc688b5 lambda terms with XML data representation in Scala;
wenzelm
parents:
diff changeset
    17
  val dummyS: Sort = List("")
a0ed7bc688b5 lambda terms with XML data representation in Scala;
wenzelm
parents:
diff changeset
    18
a0ed7bc688b5 lambda terms with XML data representation in Scala;
wenzelm
parents:
diff changeset
    19
  sealed abstract class Typ
a0ed7bc688b5 lambda terms with XML data representation in Scala;
wenzelm
parents:
diff changeset
    20
  case class Type(name: String, args: List[Typ] = Nil) extends Typ
a0ed7bc688b5 lambda terms with XML data representation in Scala;
wenzelm
parents:
diff changeset
    21
  case class TFree(name: String, sort: Sort = dummyS) extends Typ
a0ed7bc688b5 lambda terms with XML data representation in Scala;
wenzelm
parents:
diff changeset
    22
  case class TVar(name: Indexname, sort: Sort = dummyS) extends Typ
a0ed7bc688b5 lambda terms with XML data representation in Scala;
wenzelm
parents:
diff changeset
    23
  val dummyT = Type("dummy")
a0ed7bc688b5 lambda terms with XML data representation in Scala;
wenzelm
parents:
diff changeset
    24
a0ed7bc688b5 lambda terms with XML data representation in Scala;
wenzelm
parents:
diff changeset
    25
  sealed abstract class Term
a0ed7bc688b5 lambda terms with XML data representation in Scala;
wenzelm
parents:
diff changeset
    26
  case class Const(name: String, typ: Typ = dummyT) extends Term
a0ed7bc688b5 lambda terms with XML data representation in Scala;
wenzelm
parents:
diff changeset
    27
  case class Free(name: String, typ: Typ = dummyT) extends Term
a0ed7bc688b5 lambda terms with XML data representation in Scala;
wenzelm
parents:
diff changeset
    28
  case class Var(name: Indexname, typ: Typ = dummyT) extends Term
a0ed7bc688b5 lambda terms with XML data representation in Scala;
wenzelm
parents:
diff changeset
    29
  case class Bound(index: Int) extends Term
a0ed7bc688b5 lambda terms with XML data representation in Scala;
wenzelm
parents:
diff changeset
    30
  case class Abs(name: String, typ: Typ = dummyT, body: Term) extends Term
a0ed7bc688b5 lambda terms with XML data representation in Scala;
wenzelm
parents:
diff changeset
    31
  case class App(fun: Term, arg: Term) extends Term
43731
70072780e095 inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents: 43730
diff changeset
    32
}
70072780e095 inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents: 43730
diff changeset
    33