more uniform Term and Term_XML modules;
authorwenzelm
Tue Jul 12 18:00:05 2011 +0200 (2011-07-12)
changeset 4377947bec02c6762
parent 43778 ce9189450447
child 43780 2cb2310d68b6
more uniform Term and Term_XML modules;
src/Pure/build-jars
src/Pure/term.scala
src/Pure/term_xml.ML
src/Pure/term_xml.scala
     1.1 --- a/src/Pure/build-jars	Tue Jul 12 17:53:06 2011 +0200
     1.2 +++ b/src/Pure/build-jars	Tue Jul 12 18:00:05 2011 +0200
     1.3 @@ -57,6 +57,7 @@
     1.4    library.scala
     1.5    package.scala
     1.6    term.scala
     1.7 +  term_xml.scala
     1.8  )
     1.9  
    1.10  
     2.1 --- a/src/Pure/term.scala	Tue Jul 12 17:53:06 2011 +0200
     2.2 +++ b/src/Pure/term.scala	Tue Jul 12 18:00:05 2011 +0200
     2.3 @@ -1,7 +1,7 @@
     2.4  /*  Title:      Pure/term.scala
     2.5      Author:     Makarius
     2.6  
     2.7 -Lambda terms with XML data representation.
     2.8 +Lambda terms, types, sorts.
     2.9  
    2.10  Note: Isabelle/ML is the primary environment for logical operations.
    2.11  */
    2.12 @@ -11,8 +11,6 @@
    2.13  
    2.14  object Term
    2.15  {
    2.16 -  /* basic type definitions */
    2.17 -
    2.18    type Indexname = (String, Int)
    2.19  
    2.20    type Sort = List[String]
    2.21 @@ -33,55 +31,3 @@
    2.22    case class App(fun: Term, arg: Term) extends Term
    2.23  }
    2.24  
    2.25 -
    2.26 -object Term_XML
    2.27 -{
    2.28 -  import Term._
    2.29 -
    2.30 -
    2.31 -  /* XML data representation */
    2.32 -
    2.33 -  object Encode
    2.34 -  {
    2.35 -    import XML.Encode._
    2.36 -
    2.37 -    val sort: T[Sort] = list(string)
    2.38 -
    2.39 -    def typ: T[Typ] =
    2.40 -      variant[Typ](List(
    2.41 -        { case Type(a, b) => (List(a), list(typ)(b)) },
    2.42 -        { case TFree(a, b) => (List(a), sort(b)) },
    2.43 -        { case TVar((a, b), c) => (List(a, int_atom(b)), sort(c)) }))
    2.44 -
    2.45 -    def term: T[Term] =
    2.46 -      variant[Term](List(
    2.47 -        { case Const(a, b) => (List(a), typ(b)) },
    2.48 -        { case Free(a, b) => (List(a), typ(b)) },
    2.49 -        { case Var((a, b), c) => (List(a, int_atom(b)), typ(c)) },
    2.50 -        { case Bound(a) => (List(int_atom(a)), Nil) },
    2.51 -        { case Abs(a, b, c) => (List(a), pair(typ, term)(b, c)) },
    2.52 -        { case App(a, b) => (Nil, pair(term, term)(a, b)) }))
    2.53 -  }
    2.54 -
    2.55 -  object Decode
    2.56 -  {
    2.57 -    import XML.Decode._
    2.58 -
    2.59 -    val sort: T[Sort] = list(string)
    2.60 -
    2.61 -    def typ: T[Typ] =
    2.62 -      variant[Typ](List(
    2.63 -        { case (List(a), b) => Type(a, list(typ)(b)) },
    2.64 -        { case (List(a), b) => TFree(a, sort(b)) },
    2.65 -        { case (List(a, b), c) => TVar((a, int_atom(b)), sort(c)) }))
    2.66 -
    2.67 -    def term: T[Term] =
    2.68 -      variant[Term](List(
    2.69 -        { case (List(a), b) => Const(a, typ(b)) },
    2.70 -        { case (List(a), b) => Free(a, typ(b)) },
    2.71 -        { case (List(a, b), c) => Var((a, int_atom(b)), typ(c)) },
    2.72 -        { case (List(a), Nil) => Bound(int_atom(a)) },
    2.73 -        { case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) },
    2.74 -        { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) }))
    2.75 -  }
    2.76 -}
     3.1 --- a/src/Pure/term_xml.ML	Tue Jul 12 17:53:06 2011 +0200
     3.2 +++ b/src/Pure/term_xml.ML	Tue Jul 12 18:00:05 2011 +0200
     3.3 @@ -14,15 +14,13 @@
     3.4  
     3.5  signature TERM_XML =
     3.6  sig
     3.7 -  structure Encode: TERM_XML_OPS where type 'a T = 'a XML.Encode.T
     3.8 -  structure Decode: TERM_XML_OPS where type 'a T = 'a XML.Decode.T
     3.9 +  structure Encode: TERM_XML_OPS
    3.10 +  structure Decode: TERM_XML_OPS
    3.11  end;
    3.12  
    3.13  structure Term_XML: TERM_XML =
    3.14  struct
    3.15  
    3.16 -(* encode *)
    3.17 -
    3.18  structure Encode =
    3.19  struct
    3.20  
    3.21 @@ -45,9 +43,6 @@
    3.22  
    3.23  end;
    3.24  
    3.25 -
    3.26 -(* decode *)
    3.27 -
    3.28  structure Decode =
    3.29  struct
    3.30  
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Pure/term_xml.scala	Tue Jul 12 18:00:05 2011 +0200
     4.3 @@ -0,0 +1,57 @@
     4.4 +/*  Title:      Pure/term_xml.scala
     4.5 +    Author:     Makarius
     4.6 +
     4.7 +XML data representation of lambda terms.
     4.8 +*/
     4.9 +
    4.10 +package isabelle
    4.11 +
    4.12 +
    4.13 +object Term_XML
    4.14 +{
    4.15 +  import Term._
    4.16 +
    4.17 +  object Encode
    4.18 +  {
    4.19 +    import XML.Encode._
    4.20 +
    4.21 +    val sort: T[Sort] = list(string)
    4.22 +
    4.23 +    def typ: T[Typ] =
    4.24 +      variant[Typ](List(
    4.25 +        { case Type(a, b) => (List(a), list(typ)(b)) },
    4.26 +        { case TFree(a, b) => (List(a), sort(b)) },
    4.27 +        { case TVar((a, b), c) => (List(a, int_atom(b)), sort(c)) }))
    4.28 +
    4.29 +    def term: T[Term] =
    4.30 +      variant[Term](List(
    4.31 +        { case Const(a, b) => (List(a), typ(b)) },
    4.32 +        { case Free(a, b) => (List(a), typ(b)) },
    4.33 +        { case Var((a, b), c) => (List(a, int_atom(b)), typ(c)) },
    4.34 +        { case Bound(a) => (List(int_atom(a)), Nil) },
    4.35 +        { case Abs(a, b, c) => (List(a), pair(typ, term)(b, c)) },
    4.36 +        { case App(a, b) => (Nil, pair(term, term)(a, b)) }))
    4.37 +  }
    4.38 +
    4.39 +  object Decode
    4.40 +  {
    4.41 +    import XML.Decode._
    4.42 +
    4.43 +    val sort: T[Sort] = list(string)
    4.44 +
    4.45 +    def typ: T[Typ] =
    4.46 +      variant[Typ](List(
    4.47 +        { case (List(a), b) => Type(a, list(typ)(b)) },
    4.48 +        { case (List(a), b) => TFree(a, sort(b)) },
    4.49 +        { case (List(a, b), c) => TVar((a, int_atom(b)), sort(c)) }))
    4.50 +
    4.51 +    def term: T[Term] =
    4.52 +      variant[Term](List(
    4.53 +        { case (List(a), b) => Const(a, typ(b)) },
    4.54 +        { case (List(a), b) => Free(a, typ(b)) },
    4.55 +        { case (List(a, b), c) => Var((a, int_atom(b)), typ(c)) },
    4.56 +        { case (List(a), Nil) => Bound(int_atom(a)) },
    4.57 +        { case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) },
    4.58 +        { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) }))
    4.59 +  }
    4.60 +}