src/Pure/library.scala
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (19 months ago)
changeset 67003 49850a679c2c
parent 66351 95847ffa62dc
child 67431 84e143e64336
permissions -rw-r--r--
more robust sorted_entries;
wenzelm@34136
     1
/*  Title:      Pure/library.scala
wenzelm@34136
     2
    Author:     Makarius
wenzelm@34136
     3
wenzelm@34136
     4
Basic library.
wenzelm@34136
     5
*/
wenzelm@34136
     6
wenzelm@34136
     7
package isabelle
wenzelm@34136
     8
wenzelm@38258
     9
wenzelm@63781
    10
import scala.annotation.tailrec
wenzelm@51981
    11
import scala.collection.mutable
wenzelm@59224
    12
import scala.util.matching.Regex
wenzelm@51981
    13
wenzelm@37018
    14
wenzelm@34136
    15
object Library
wenzelm@34136
    16
{
wenzelm@63789
    17
  /* resource management */
wenzelm@63789
    18
wenzelm@63789
    19
  def using[A <: { def close() }, B](x: A)(f: A => B): B =
wenzelm@63789
    20
  {
wenzelm@63926
    21
    import scala.language.reflectiveCalls
wenzelm@63926
    22
wenzelm@63789
    23
    try { f(x) }
wenzelm@63789
    24
    finally { if (x != null) x.close() }
wenzelm@63789
    25
  }
wenzelm@63789
    26
wenzelm@63789
    27
wenzelm@57909
    28
  /* integers */
wenzelm@57909
    29
wenzelm@57909
    30
  private val small_int = 10000
wenzelm@57909
    31
  private lazy val small_int_table =
wenzelm@57909
    32
  {
wenzelm@57909
    33
    val array = new Array[String](small_int)
wenzelm@57909
    34
    for (i <- 0 until small_int) array(i) = i.toString
wenzelm@57909
    35
    array
wenzelm@57909
    36
  }
wenzelm@57909
    37
wenzelm@57909
    38
  def is_small_int(s: String): Boolean =
wenzelm@57909
    39
  {
wenzelm@57909
    40
    val len = s.length
wenzelm@57909
    41
    1 <= len && len <= 4 &&
wenzelm@57909
    42
    s.forall(c => '0' <= c && c <= '9') &&
wenzelm@57909
    43
    (len == 1 || s(0) != '0')
wenzelm@57909
    44
  }
wenzelm@57909
    45
wenzelm@57909
    46
  def signed_string_of_long(i: Long): String =
wenzelm@57909
    47
    if (0 <= i && i < small_int) small_int_table(i.toInt)
wenzelm@57909
    48
    else i.toString
wenzelm@57909
    49
wenzelm@57909
    50
  def signed_string_of_int(i: Int): String =
wenzelm@57909
    51
    if (0 <= i && i < small_int) small_int_table(i)
wenzelm@57909
    52
    else i.toString
wenzelm@57909
    53
wenzelm@57909
    54
wenzelm@48996
    55
  /* separated chunks */
wenzelm@36688
    56
wenzelm@36688
    57
  def separate[A](s: A, list: List[A]): List[A] =
wenzelm@51981
    58
  {
wenzelm@51981
    59
    val result = new mutable.ListBuffer[A]
wenzelm@51981
    60
    var first = true
wenzelm@51981
    61
    for (x <- list) {
wenzelm@51981
    62
      if (first) {
wenzelm@51981
    63
        first = false
wenzelm@51981
    64
        result += x
wenzelm@51981
    65
      }
wenzelm@51981
    66
      else {
wenzelm@51981
    67
        result += s
wenzelm@51981
    68
        result += x
wenzelm@51981
    69
      }
wenzelm@36688
    70
    }
wenzelm@51981
    71
    result.toList
wenzelm@51981
    72
  }
wenzelm@36688
    73
wenzelm@56600
    74
  def separated_chunks(sep: Char => Boolean, source: CharSequence): Iterator[CharSequence] =
wenzelm@48996
    75
    new Iterator[CharSequence] {
wenzelm@48996
    76
      private val end = source.length
wenzelm@48996
    77
      private def next_chunk(i: Int): Option[(CharSequence, Int)] =
wenzelm@48996
    78
      {
wenzelm@48996
    79
        if (i < end) {
wenzelm@56600
    80
          var j = i; do j += 1 while (j < end && !sep(source.charAt(j)))
wenzelm@48996
    81
          Some((source.subSequence(i + 1, j), j))
wenzelm@48996
    82
        }
wenzelm@48996
    83
        else None
wenzelm@43598
    84
      }
wenzelm@48996
    85
      private var state: Option[(CharSequence, Int)] = if (end == 0) None else next_chunk(-1)
wenzelm@48996
    86
wenzelm@48996
    87
      def hasNext(): Boolean = state.isDefined
wenzelm@48996
    88
      def next(): CharSequence =
wenzelm@48996
    89
        state match {
wenzelm@60215
    90
          case Some((s, i)) => state = next_chunk(i); s
wenzelm@48996
    91
          case None => Iterator.empty.next()
wenzelm@48996
    92
        }
wenzelm@43598
    93
    }
wenzelm@43598
    94
wenzelm@48996
    95
  def space_explode(sep: Char, str: String): List[String] =
wenzelm@56600
    96
    separated_chunks(_ == sep, str).map(_.toString).toList
wenzelm@48996
    97
wenzelm@48996
    98
wenzelm@48996
    99
  /* lines */
wenzelm@48996
   100
wenzelm@64002
   101
  def terminate_lines(lines: TraversableOnce[String]): String = lines.mkString("", "\n", "\n")
wenzelm@51983
   102
wenzelm@48996
   103
  def cat_lines(lines: TraversableOnce[String]): String = lines.mkString("\n")
wenzelm@48996
   104
wenzelm@43670
   105
  def split_lines(str: String): List[String] = space_explode('\n', str)
wenzelm@43670
   106
wenzelm@62590
   107
  def prefix_lines(prfx: String, str: String): String =
wenzelm@62590
   108
    if (str == "") str
wenzelm@62590
   109
    else cat_lines(split_lines(str).map(s => prfx + s))
wenzelm@62590
   110
wenzelm@48996
   111
  def first_line(source: CharSequence): String =
wenzelm@48996
   112
  {
wenzelm@56600
   113
    val lines = separated_chunks(_ == '\n', source)
wenzelm@48996
   114
    if (lines.hasNext) lines.next.toString
wenzelm@48996
   115
    else ""
wenzelm@48996
   116
  }
wenzelm@48996
   117
wenzelm@65932
   118
  def encode_lines(s: String): String = s.replace('\n', '\u000b')
wenzelm@65932
   119
  def decode_lines(s: String): String = s.replace('\u000b', '\n')
wenzelm@65932
   120
wenzelm@50847
   121
wenzelm@50847
   122
  /* strings */
wenzelm@50847
   123
wenzelm@64355
   124
  def make_string(f: StringBuilder => Unit): String =
wenzelm@64355
   125
  {
wenzelm@64355
   126
    val s = new StringBuilder
wenzelm@64355
   127
    f(s)
wenzelm@64355
   128
    s.toString
wenzelm@64355
   129
  }
wenzelm@64355
   130
wenzelm@50847
   131
  def try_unprefix(prfx: String, s: String): Option[String] =
wenzelm@50847
   132
    if (s.startsWith(prfx)) Some(s.substring(prfx.length)) else None
wenzelm@50847
   133
wenzelm@55033
   134
  def try_unsuffix(sffx: String, s: String): Option[String] =
wenzelm@55033
   135
    if (s.endsWith(sffx)) Some(s.substring(0, s.length - sffx.length)) else None
wenzelm@55033
   136
wenzelm@65606
   137
  def perhaps_unprefix(prfx: String, s: String): String = try_unprefix(prfx, s) getOrElse s
wenzelm@65606
   138
  def perhaps_unsuffix(sffx: String, s: String): String = try_unsuffix(sffx, s) getOrElse s
wenzelm@65606
   139
wenzelm@52444
   140
  def trim_line(s: String): String =
wenzelm@52444
   141
    if (s.endsWith("\r\n")) s.substring(0, s.length - 2)
wenzelm@52444
   142
    else if (s.endsWith("\r") || s.endsWith("\n")) s.substring(0, s.length - 1)
wenzelm@52444
   143
    else s
wenzelm@52444
   144
wenzelm@64063
   145
  def trim_split_lines(s: String): List[String] =
wenzelm@64063
   146
    split_lines(trim_line(s)).map(trim_line(_))
wenzelm@64063
   147
wenzelm@65903
   148
  def isolate_substring(s: String): String = new String(s.toCharArray)
wenzelm@64820
   149
wenzelm@43598
   150
wenzelm@48996
   151
  /* quote */
wenzelm@46196
   152
wenzelm@43598
   153
  def quote(s: String): String = "\"" + s + "\""
wenzelm@56843
   154
wenzelm@56843
   155
  def try_unquote(s: String): Option[String] =
wenzelm@56843
   156
    if (s.startsWith("\"") && s.endsWith("\"")) Some(s.substring(1, s.length - 1))
wenzelm@56843
   157
    else None
wenzelm@56843
   158
wenzelm@58592
   159
  def perhaps_unquote(s: String): String = try_unquote(s) getOrElse s
wenzelm@58592
   160
wenzelm@43598
   161
  def commas(ss: Iterable[String]): String = ss.iterator.mkString(", ")
wenzelm@48362
   162
  def commas_quote(ss: Iterable[String]): String = ss.iterator.map(quote).mkString(", ")
wenzelm@43598
   163
wenzelm@36688
   164
wenzelm@51983
   165
  /* CharSequence */
wenzelm@34141
   166
wenzelm@34141
   167
  class Reverse(text: CharSequence, start: Int, end: Int) extends CharSequence
wenzelm@34141
   168
  {
wenzelm@34141
   169
    require(0 <= start && start <= end && end <= text.length)
wenzelm@34141
   170
wenzelm@34141
   171
    def this(text: CharSequence) = this(text, 0, text.length)
wenzelm@34141
   172
wenzelm@34141
   173
    def length: Int = end - start
wenzelm@34141
   174
    def charAt(i: Int): Char = text.charAt(end - i - 1)
wenzelm@34141
   175
wenzelm@34141
   176
    def subSequence(i: Int, j: Int): CharSequence =
wenzelm@34141
   177
      if (0 <= i && i <= j && j <= length) new Reverse(text, end - j, end - i)
wenzelm@34141
   178
      else throw new IndexOutOfBoundsException
wenzelm@34141
   179
wenzelm@34141
   180
    override def toString: String =
wenzelm@34141
   181
    {
wenzelm@34141
   182
      val buf = new StringBuilder(length)
wenzelm@34141
   183
      for (i <- 0 until length)
wenzelm@34141
   184
        buf.append(charAt(i))
wenzelm@34141
   185
      buf.toString
wenzelm@34141
   186
    }
wenzelm@34141
   187
  }
wenzelm@34141
   188
wenzelm@51983
   189
  class Line_Termination(text: CharSequence) extends CharSequence
wenzelm@51983
   190
  {
wenzelm@51983
   191
    def length: Int = text.length + 1
wenzelm@51983
   192
    def charAt(i: Int): Char = if (i == text.length) '\n' else text.charAt(i)
wenzelm@51983
   193
    def subSequence(i: Int, j: Int): CharSequence =
wenzelm@51983
   194
      if (j == text.length + 1) new Line_Termination(text.subSequence(i, j - 1))
wenzelm@51983
   195
      else text.subSequence(i, j)
wenzelm@51983
   196
    override def toString: String = text.toString + "\n"
wenzelm@51983
   197
  }
wenzelm@51983
   198
wenzelm@34141
   199
wenzelm@59224
   200
  /* regular expressions */
wenzelm@59224
   201
wenzelm@59224
   202
  def make_regex(s: String): Option[Regex] =
wenzelm@59224
   203
    try { Some(new Regex(s)) } catch { case ERROR(_) => None }
wenzelm@59224
   204
wenzelm@64871
   205
  def is_regex_meta(c: Char): Boolean = """()[]{}\^$|?*+.<>-=!""".contains(c)
wenzelm@64871
   206
wenzelm@64871
   207
  def escape_regex(s: String): String =
wenzelm@64871
   208
    if (s.exists(is_regex_meta(_))) {
wenzelm@64871
   209
      (for (c <- s.iterator)
wenzelm@64871
   210
       yield { if (is_regex_meta(c)) "\\" + c.toString else c.toString }).mkString
wenzelm@64871
   211
    }
wenzelm@64871
   212
    else s
wenzelm@64871
   213
wenzelm@59224
   214
wenzelm@61883
   215
  /* lists */
wenzelm@61883
   216
wenzelm@61883
   217
  def take_prefix[A](pred: A => Boolean, xs: List[A]): (List[A], List[A]) =
wenzelm@61883
   218
    (xs.takeWhile(pred), xs.dropWhile(pred))
wenzelm@56686
   219
wenzelm@60215
   220
  def member[A, B](xs: List[A])(x: B): Boolean = xs.contains(x)
wenzelm@56688
   221
  def insert[A](x: A)(xs: List[A]): List[A] = if (xs.contains(x)) xs else x :: xs
wenzelm@56688
   222
  def remove[A, B](x: B)(xs: List[A]): List[A] = if (member(xs)(x)) xs.filterNot(_ == x) else xs
wenzelm@56688
   223
  def update[A](x: A)(xs: List[A]): List[A] = x :: remove(x)(xs)
wenzelm@63734
   224
wenzelm@63867
   225
  def merge[A](xs: List[A], ys: List[A]): List[A] =
wenzelm@63867
   226
    if (xs.eq(ys)) xs
wenzelm@63867
   227
    else if (xs.isEmpty) ys
wenzelm@63867
   228
    else ys.foldRight(xs)(Library.insert(_)(_))
wenzelm@63867
   229
wenzelm@64207
   230
  def distinct[A](xs: List[A], eq: (A, A) => Boolean = (x: A, y: A) => x == y): List[A] =
wenzelm@63734
   231
  {
wenzelm@63734
   232
    val result = new mutable.ListBuffer[A]
wenzelm@64207
   233
    xs.foreach(x => if (!result.exists(y => eq(x, y))) result += x)
wenzelm@63734
   234
    result.toList
wenzelm@63734
   235
  }
wenzelm@63781
   236
wenzelm@64207
   237
  def duplicates[A](lst: List[A], eq: (A, A) => Boolean = (x: A, y: A) => x == y): List[A] =
wenzelm@63781
   238
  {
wenzelm@63781
   239
    val result = new mutable.ListBuffer[A]
wenzelm@63781
   240
    @tailrec def dups(rest: List[A]): Unit =
wenzelm@63781
   241
      rest match {
wenzelm@63781
   242
        case Nil =>
wenzelm@63781
   243
        case x :: xs =>
wenzelm@64207
   244
          if (!result.exists(y => eq(x, y)) && xs.exists(y => eq(x, y))) result += x
wenzelm@63781
   245
          dups(xs)
wenzelm@63781
   246
      }
wenzelm@63781
   247
    dups(lst)
wenzelm@63781
   248
    result.toList
wenzelm@63781
   249
  }
wenzelm@65761
   250
wenzelm@65761
   251
wenzelm@65761
   252
  /* proper values */
wenzelm@65761
   253
wenzelm@65761
   254
  def proper[A](x: A): Option[A] =
wenzelm@65761
   255
    if (x == null) None else Some(x)
wenzelm@65761
   256
wenzelm@65761
   257
  def proper_string(s: String): Option[String] =
wenzelm@65761
   258
    if (s == null || s == "") None else Some(s)
wenzelm@65761
   259
wenzelm@65761
   260
  def proper_list[A](list: List[A]): Option[List[A]] =
wenzelm@65761
   261
    if (list == null || list.isEmpty) None else Some(list)
wenzelm@66351
   262
wenzelm@66351
   263
wenzelm@66351
   264
  /* UUID */
wenzelm@66351
   265
wenzelm@66351
   266
  def UUID(): String = java.util.UUID.randomUUID().toString
wenzelm@34136
   267
}