# HG changeset patch # User wenzelm # Date 1310313491 -7200 # Node ID a0ed7bc688b5b17bc5db2e8b09de776df1c214da # Parent 07d3c6afa8653fb2b210e849354cbed94a1db0bb lambda terms with XML data representation in Scala; avoid `class` in signature; diff -r 07d3c6afa865 -r a0ed7bc688b5 src/Pure/build-jars --- a/src/Pure/build-jars Sun Jul 10 16:34:17 2011 +0200 +++ b/src/Pure/build-jars Sun Jul 10 17:58:11 2011 +0200 @@ -57,6 +57,7 @@ Thy/thy_syntax.scala library.scala package.scala + term.scala ) diff -r 07d3c6afa865 -r a0ed7bc688b5 src/Pure/term.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/term.scala Sun Jul 10 17:58:11 2011 +0200 @@ -0,0 +1,88 @@ +/* Title: Pure/term.scala + Author: Makarius + +Lambda terms with XML data representation. + +Note: Isabelle/ML is the primary environment for logical operations. +*/ + +package isabelle + + +object Term +{ + /* basic type definitions */ + + type Indexname = (String, Int) + + type Sort = List[String] + val dummyS: Sort = List("") + + sealed abstract class Typ + case class Type(name: String, args: List[Typ] = Nil) extends Typ + case class TFree(name: String, sort: Sort = dummyS) extends Typ + case class TVar(name: Indexname, sort: Sort = dummyS) extends Typ + val dummyT = Type("dummy") + + sealed abstract class Term + case class Const(name: String, typ: Typ = dummyT) extends Term + case class Free(name: String, typ: Typ = dummyT) extends Term + case class Var(name: Indexname, typ: Typ = dummyT) extends Term + case class Bound(index: Int) extends Term + case class Abs(name: String, typ: Typ = dummyT, body: Term) extends Term + case class App(fun: Term, arg: Term) extends Term + + + /* XML data representation */ + + object XML + { + object Make + { + import XML_Data.Make._ + + val indexname: T[Indexname] = pair(string, int) + + val sort: T[Sort] = list(string) + + def typ: T[Typ] = + variant[Typ](List( + { case Type(a, b) => pair(string, list(typ))((a, b)) }, + { case TFree(a, b) => pair(string, sort)((a, b)) }, + { case TVar(a, b) => pair(indexname, sort)((a, b)) })) + + def term: T[Term] = + variant[Term](List( + { case Const(a, b) => pair(string, typ)((a, b)) }, + { case Free(a, b) => pair(string, typ)((a, b)) }, + { case Var(a, b) => pair(indexname, typ)((a, b)) }, + { case Bound(a) => int(a) }, + { case Abs(a, b, c) => triple(string, typ, term)((a, b, c)) }, + { case App(a, b) => pair(term, term)((a, b)) })) + } + + object Dest + { + import XML_Data.Dest._ + + val indexname: T[Indexname] = pair(string, int) + + val sort: T[Sort] = list(string) + + def typ: T[Typ] = + variant[Typ](List( + (x => { val (a, b) = pair(string, list(typ))(x); Type(a, b) }), + (x => { val (a, b) = pair(string, sort)(x); TFree(a, b) }), + (x => { val (a, b) = pair(indexname, sort)(x); TVar(a, b) }))) + + def term: T[Term] = + variant[Term](List( + (x => { val (a, b) = pair(string, typ)(x); Const(a, b) }), + (x => { val (a, b) = pair(string, typ)(x); Free(a, b) }), + (x => { val (a, b) = pair(indexname, typ)(x); Var(a, b) }), + (x => Bound(int(x))), + (x => { val (a, b, c) = triple(string, typ, term)(x); Abs(a, b, c) }), + (x => { val (a, b) = pair(term, term)(x); App(a, b) }))) + } + } +} diff -r 07d3c6afa865 -r a0ed7bc688b5 src/Pure/term_xml.ML --- a/src/Pure/term_xml.ML Sun Jul 10 16:34:17 2011 +0200 +++ b/src/Pure/term_xml.ML Sun Jul 10 17:58:11 2011 +0200 @@ -8,7 +8,6 @@ sig type 'a T val indexname: indexname T - val class: class T val sort: sort T val typ: typ T val term: term T @@ -31,8 +30,8 @@ open XML_Data.Make; val indexname = pair string int; -val class = string; -val sort = list class; + +val sort = list string; fun typ T = T |> variant [fn Type x => pair string (list typ) x, @@ -58,8 +57,8 @@ open XML_Data.Dest; val indexname = pair string int; -val class = string; -val sort = list class; + +val sort = list string; fun typ T = T |> variant [Type o pair string (list typ),