more abstract signature;
authorwenzelm
Sun Jul 10 15:48:15 2011 +0200 (2011-07-10)
changeset 43725bebcfcad12d4
parent 43724 4e58485fa320
child 43726 8e2be96f2d94
more abstract signature;
tuned;
src/Pure/General/xml_data.ML
src/Pure/General/xml_data.scala
src/Pure/Thy/thy_header.scala
     1.1 --- a/src/Pure/General/xml_data.ML	Sun Jul 10 13:51:21 2011 +0200
     1.2 +++ b/src/Pure/General/xml_data.ML	Sun Jul 10 15:48:15 2011 +0200
     1.3 @@ -8,31 +8,33 @@
     1.4  sig
     1.5    structure Make:
     1.6    sig
     1.7 -    val properties: Properties.T -> XML.body
     1.8 -    val string: string -> XML.body
     1.9 -    val int: int -> XML.body
    1.10 -    val bool: bool -> XML.body
    1.11 -    val unit: unit -> XML.body
    1.12 -    val pair: ('a -> XML.body) -> ('b -> XML.body) -> 'a * 'b -> XML.body
    1.13 -    val triple: ('a -> XML.body) -> ('b -> XML.body) -> ('c -> XML.body) -> 'a * 'b * 'c -> XML.body
    1.14 -    val list: ('a -> XML.body) -> 'a list -> XML.body
    1.15 -    val option: ('a -> XML.body) -> 'a option -> XML.body
    1.16 -    val variant: ('a -> XML.body) list -> 'a -> XML.body
    1.17 +    type 'a T = 'a -> XML.body
    1.18 +    val properties: Properties.T T
    1.19 +    val string: string T
    1.20 +    val int: int T
    1.21 +    val bool: bool T
    1.22 +    val unit: unit T
    1.23 +    val pair: 'a T -> 'b T -> ('a * 'b) T
    1.24 +    val triple: 'a T -> 'b T -> 'c T -> ('a * 'b * 'c) T
    1.25 +    val list: 'a T -> 'a list T
    1.26 +    val option: 'a T -> 'a option T
    1.27 +    val variant: 'a T list -> 'a T
    1.28    end
    1.29    exception XML_ATOM of string
    1.30    exception XML_BODY of XML.body
    1.31    structure Dest:
    1.32    sig
    1.33 -    val properties: XML.body -> Properties.T
    1.34 -    val string : XML.body -> string
    1.35 -    val int : XML.body -> int
    1.36 -    val bool: XML.body -> bool
    1.37 -    val unit: XML.body -> unit
    1.38 -    val pair: (XML.body -> 'a) -> (XML.body -> 'b) -> XML.body -> 'a * 'b
    1.39 -    val triple: (XML.body -> 'a) -> (XML.body -> 'b) -> (XML.body -> 'c) -> XML.body -> 'a * 'b * 'c
    1.40 -    val list: (XML.body -> 'a) -> XML.body -> 'a list
    1.41 -    val option: (XML.body -> 'a) -> XML.body -> 'a option
    1.42 -    val variant: (XML.body -> 'a) list -> XML.body -> 'a
    1.43 +    type 'a T = XML.body -> 'a
    1.44 +    val properties: Properties.T T
    1.45 +    val string : string T
    1.46 +    val int : int T
    1.47 +    val bool: bool T
    1.48 +    val unit: unit T
    1.49 +    val pair: 'a T -> 'b T -> ('a * 'b) T
    1.50 +    val triple: 'a T -> 'b T -> 'c T -> ('a * 'b * 'c) T
    1.51 +    val list: 'a T -> 'a list T
    1.52 +    val option: 'a T -> 'a option T
    1.53 +    val variant: 'a T list -> 'a T
    1.54    end
    1.55  end;
    1.56  
    1.57 @@ -44,6 +46,9 @@
    1.58  structure Make =
    1.59  struct
    1.60  
    1.61 +type 'a T = 'a -> XML.body;
    1.62 +
    1.63 +
    1.64  (* basic values *)
    1.65  
    1.66  fun int_atom i = signed_string_of_int i;
    1.67 @@ -97,6 +102,9 @@
    1.68  structure Dest =
    1.69  struct
    1.70  
    1.71 +type 'a T = XML.body -> 'a;
    1.72 +
    1.73 +
    1.74  (* basic values *)
    1.75  
    1.76  fun int_atom s =
     2.1 --- a/src/Pure/General/xml_data.scala	Sun Jul 10 13:51:21 2011 +0200
     2.2 +++ b/src/Pure/General/xml_data.scala	Sun Jul 10 15:48:15 2011 +0200
     2.3 @@ -14,6 +14,9 @@
     2.4  
     2.5    object Make
     2.6    {
     2.7 +    type T[A] = A => XML.Body
     2.8 +
     2.9 +
    2.10      /* basic values */
    2.11  
    2.12      private def long_atom(i: Long): String = i.toString
    2.13 @@ -35,39 +38,39 @@
    2.14  
    2.15      /* representation of standard types */
    2.16  
    2.17 -    def properties(props: List[(String, String)]): XML.Body =
    2.18 -      List(XML.Elem(Markup(":", props), Nil))
    2.19 +    val properties: T[List[(String, String)]] =
    2.20 +      (props => List(XML.Elem(Markup(":", props), Nil)))
    2.21  
    2.22 -    def string(s: String): XML.Body = if (s.isEmpty) Nil else List(XML.Text(s))
    2.23 +    val string: T[String] = (s => if (s.isEmpty) Nil else List(XML.Text(s)))
    2.24  
    2.25 -    def long(i: Long): XML.Body = string(long_atom(i))
    2.26 +    val long: T[Long] = (x => string(long_atom(x)))
    2.27  
    2.28 -    def int(i: Int): XML.Body = string(int_atom(i))
    2.29 +    val int: T[Int] = (x => string(int_atom(x)))
    2.30  
    2.31 -    def bool(b: Boolean): XML.Body = string(bool_atom(b))
    2.32 +    val bool: T[Boolean] = (x => string(bool_atom(x)))
    2.33  
    2.34 -    def unit(u: Unit): XML.Body = string(unit_atom(u))
    2.35 +    val unit: T[Unit] = (x => string(unit_atom(x)))
    2.36  
    2.37 -    def pair[A, B](f: A => XML.Body, g: B => XML.Body)(p: (A, B)): XML.Body =
    2.38 -      List(node(f(p._1)), node(g(p._2)))
    2.39 +    def pair[A, B](f: T[A], g: T[B]): T[(A, B)] =
    2.40 +      (x => List(node(f(x._1)), node(g(x._2))))
    2.41  
    2.42 -    def triple[A, B, C](f: A => XML.Body, g: B => XML.Body, h: C => XML.Body)
    2.43 -        (p: (A, B, C)): XML.Body =
    2.44 -      List(node(f(p._1)), node(g(p._2)), node(h(p._3)))
    2.45 +    def triple[A, B, C](f: T[A], g: T[B], h: T[C]): T[(A, B, C)] =
    2.46 +      (x => List(node(f(x._1)), node(g(x._2)), node(h(x._3))))
    2.47  
    2.48 -    def list[A](f: A => XML.Body)(xs: List[A]): XML.Body =
    2.49 -      xs.map((x: A) => node(f(x)))
    2.50 +    def list[A](f: T[A]): T[List[A]] =
    2.51 +      (xs => xs.map((x: A) => node(f(x))))
    2.52  
    2.53 -    def option[A](f: A => XML.Body)(opt: Option[A]): XML.Body =
    2.54 -      opt match {
    2.55 -        case None => Nil
    2.56 -        case Some(x) => List(node(f(x)))
    2.57 -      }
    2.58 +    def option[A](f: T[A]): T[Option[A]] =
    2.59 +    {
    2.60 +      case None => Nil
    2.61 +      case Some(x) => List(node(f(x)))
    2.62 +    }
    2.63  
    2.64 -    def variant[A](fs: List[PartialFunction[A, XML.Body]])(x: A): XML.Body =
    2.65 +    def variant[A](fs: List[PartialFunction[A, XML.Body]]): T[A] =
    2.66      {
    2.67 -      val (f, tag) = fs.iterator.zipWithIndex.find(p => p._1.isDefinedAt(x)).get
    2.68 -      List(tagged(tag, f(x)))
    2.69 +      case x =>
    2.70 +        val (f, tag) = fs.iterator.zipWithIndex.find(p => p._1.isDefinedAt(x)).get
    2.71 +        List(tagged(tag, f(x)))
    2.72      }
    2.73    }
    2.74  
    2.75 @@ -80,6 +83,9 @@
    2.76  
    2.77    object Dest
    2.78    {
    2.79 +    type T[A] = XML.Body => A
    2.80 +
    2.81 +
    2.82       /* basic values */
    2.83  
    2.84      private def long_atom(s: String): Long =
    2.85 @@ -116,56 +122,55 @@
    2.86  
    2.87      /* representation of standard types */
    2.88  
    2.89 -    def properties(ts: XML.Body): List[(String, String)] =
    2.90 -      ts match {
    2.91 -        case List(XML.Elem(Markup(":", props), Nil)) => props
    2.92 -        case _ => throw new XML_Body(ts)
    2.93 -      }
    2.94 +    val properties: T[List[(String, String)]] =
    2.95 +    {
    2.96 +      case List(XML.Elem(Markup(":", props), Nil)) => props
    2.97 +      case ts => throw new XML_Body(ts)
    2.98 +    }
    2.99  
   2.100 -    def string(ts: XML.Body): String =
   2.101 -      ts match {
   2.102 -        case Nil => ""
   2.103 -        case List(XML.Text(s)) => s
   2.104 -        case _ => throw new XML_Body(ts)
   2.105 -      }
   2.106 +    val string: T[String] =
   2.107 +    {
   2.108 +      case Nil => ""
   2.109 +      case List(XML.Text(s)) => s
   2.110 +      case ts => throw new XML_Body(ts)
   2.111 +    }
   2.112  
   2.113 -    def long(ts: XML.Body): Long = long_atom(string(ts))
   2.114 +    val long: T[Long] = (x => long_atom(string(x)))
   2.115  
   2.116 -    def int(ts: XML.Body): Int = int_atom(string(ts))
   2.117 +    val int: T[Int] = (x => int_atom(string(x)))
   2.118  
   2.119 -    def bool(ts: XML.Body) = bool_atom(string(ts))
   2.120 +    val bool: T[Boolean] = (x => bool_atom(string(x)))
   2.121  
   2.122 -    def unit(ts: XML.Body): Unit = unit_atom(string(ts))
   2.123 +    val unit: T[Unit] = (x => unit_atom(string(x)))
   2.124  
   2.125 -    def pair[A, B](f: XML.Body => A, g: XML.Body => B)(ts: XML.Body): (A, B) =
   2.126 -      ts match {
   2.127 -        case List(t1, t2) => (f(node(t1)), g(node(t2)))
   2.128 -        case _ => throw new XML_Body(ts)
   2.129 -      }
   2.130 +    def pair[A, B](f: T[A], g: T[B]): T[(A, B)] =
   2.131 +    {
   2.132 +      case List(t1, t2) => (f(node(t1)), g(node(t2)))
   2.133 +      case ts => throw new XML_Body(ts)
   2.134 +    }
   2.135  
   2.136 -    def triple[A, B, C](f: XML.Body => A, g: XML.Body => B, h: XML.Body => C)
   2.137 -        (ts: XML.Body): (A, B, C) =
   2.138 -      ts match {
   2.139 -        case List(t1, t2, t3) => (f(node(t1)), g(node(t2)), h(node(t3)))
   2.140 -        case _ => throw new XML_Body(ts)
   2.141 -      }
   2.142 +    def triple[A, B, C](f: T[A], g: T[B], h: T[C]): T[(A, B, C)] =
   2.143 +    {
   2.144 +      case List(t1, t2, t3) => (f(node(t1)), g(node(t2)), h(node(t3)))
   2.145 +      case ts => throw new XML_Body(ts)
   2.146 +    }
   2.147 +
   2.148 +    def list[A](f: T[A]): T[List[A]] =
   2.149 +      (ts => ts.map(t => f(node(t))))
   2.150  
   2.151 -    def list[A](f: XML.Body => A)(ts: XML.Body): List[A] =
   2.152 -      ts.map((t: XML.Tree) => f(node(t)))
   2.153 +    def option[A](f: T[A]): T[Option[A]] =
   2.154 +    {
   2.155 +      case Nil => None
   2.156 +      case List(t) => Some(f(node(t)))
   2.157 +      case ts => throw new XML_Body(ts)
   2.158 +    }
   2.159  
   2.160 -    def option[A](f: XML.Body => A)(ts: XML.Body): Option[A] =
   2.161 -      ts match {
   2.162 -        case Nil => None
   2.163 -        case List(t) => Some(f(node(t)))
   2.164 -        case _ => throw new XML_Body(ts)
   2.165 -      }
   2.166 -
   2.167 -    def variant[A](fs: List[XML.Body => A])(ts: XML.Body): A =
   2.168 -      ts match {
   2.169 -        case List(t) =>
   2.170 -          val (tag, ts) = tagged(t)
   2.171 -          fs(tag)(ts)
   2.172 -        case _ => throw new XML_Body(ts)
   2.173 -      }
   2.174 +    def variant[A](fs: List[T[A]]): T[A] =
   2.175 +    {
   2.176 +      case List(t) =>
   2.177 +        val (tag, ts) = tagged(t)
   2.178 +        fs(tag)(ts)
   2.179 +      case ts => throw new XML_Body(ts)
   2.180 +    }
   2.181    }
   2.182  }
     3.1 --- a/src/Pure/Thy/thy_header.scala	Sun Jul 10 13:51:21 2011 +0200
     3.2 +++ b/src/Pure/Thy/thy_header.scala	Sun Jul 10 15:48:15 2011 +0200
     3.3 @@ -31,9 +31,12 @@
     3.4        Header(f(name), imports.map(f), uses.map(f))
     3.5    }
     3.6  
     3.7 -  def make_xml_data(header: Header): XML.Body =
     3.8 -  { import XML_Data.Make._
     3.9 -    triple(string, list(string), list(string))(header.name, header.imports, header.uses) }
    3.10 +  val make_xml_data: XML_Data.Make.T[Header] =
    3.11 +  {
    3.12 +    case Header(name, imports, uses) =>
    3.13 +      import XML_Data.Make._
    3.14 +      triple(string, list(string), list(string))(name, imports, uses)
    3.15 +  }
    3.16  
    3.17  
    3.18    /* file name */