src/Pure/library.scala
author wenzelm
Mon Feb 23 14:50:30 2015 +0100 (2015-02-23)
changeset 59564 fdc03c8daacc
parent 59224 e3f90d5c0006
child 59697 43e14b0e2ef8
permissions -rw-r--r--
Goal.prove_multi is superseded by the fully general Goal.prove_common;
wenzelm@34136
     1
/*  Title:      Pure/library.scala
wenzelm@45673
     2
    Module:     PIDE
wenzelm@34136
     3
    Author:     Makarius
wenzelm@34136
     4
wenzelm@34136
     5
Basic library.
wenzelm@34136
     6
*/
wenzelm@34136
     7
wenzelm@34136
     8
package isabelle
wenzelm@34136
     9
wenzelm@38258
    10
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@43652
    17
  /* user errors */
wenzelm@43652
    18
wenzelm@43652
    19
  object ERROR
wenzelm@43652
    20
  {
wenzelm@43652
    21
    def apply(message: String): Throwable = new RuntimeException(message)
wenzelm@48479
    22
    def unapply(exn: Throwable): Option[String] = Exn.user_message(exn)
wenzelm@43652
    23
  }
wenzelm@43652
    24
wenzelm@43652
    25
  def error(message: String): Nothing = throw ERROR(message)
wenzelm@43652
    26
wenzelm@54548
    27
  def cat_message(msg1: String, msg2: String): String =
wenzelm@54548
    28
    if (msg1 == "") msg2
wenzelm@57831
    29
    else if (msg2 == "") msg1
wenzelm@54548
    30
    else msg1 + "\n" + msg2
wenzelm@54548
    31
wenzelm@43652
    32
  def cat_error(msg1: String, msg2: String): Nothing =
wenzelm@54548
    33
    error(cat_message(msg1, msg2))
wenzelm@43652
    34
wenzelm@43652
    35
wenzelm@57909
    36
  /* integers */
wenzelm@57909
    37
wenzelm@57909
    38
  private val small_int = 10000
wenzelm@57909
    39
  private lazy val small_int_table =
wenzelm@57909
    40
  {
wenzelm@57909
    41
    val array = new Array[String](small_int)
wenzelm@57909
    42
    for (i <- 0 until small_int) array(i) = i.toString
wenzelm@57909
    43
    array
wenzelm@57909
    44
  }
wenzelm@57909
    45
wenzelm@57909
    46
  def is_small_int(s: String): Boolean =
wenzelm@57909
    47
  {
wenzelm@57909
    48
    val len = s.length
wenzelm@57909
    49
    1 <= len && len <= 4 &&
wenzelm@57909
    50
    s.forall(c => '0' <= c && c <= '9') &&
wenzelm@57909
    51
    (len == 1 || s(0) != '0')
wenzelm@57909
    52
  }
wenzelm@57909
    53
wenzelm@57909
    54
  def signed_string_of_long(i: Long): String =
wenzelm@57909
    55
    if (0 <= i && i < small_int) small_int_table(i.toInt)
wenzelm@57909
    56
    else i.toString
wenzelm@57909
    57
wenzelm@57909
    58
  def signed_string_of_int(i: Int): String =
wenzelm@57909
    59
    if (0 <= i && i < small_int) small_int_table(i)
wenzelm@57909
    60
    else i.toString
wenzelm@57909
    61
wenzelm@57909
    62
wenzelm@48996
    63
  /* separated chunks */
wenzelm@36688
    64
wenzelm@36688
    65
  def separate[A](s: A, list: List[A]): List[A] =
wenzelm@51981
    66
  {
wenzelm@51981
    67
    val result = new mutable.ListBuffer[A]
wenzelm@51981
    68
    var first = true
wenzelm@51981
    69
    for (x <- list) {
wenzelm@51981
    70
      if (first) {
wenzelm@51981
    71
        first = false
wenzelm@51981
    72
        result += x
wenzelm@51981
    73
      }
wenzelm@51981
    74
      else {
wenzelm@51981
    75
        result += s
wenzelm@51981
    76
        result += x
wenzelm@51981
    77
      }
wenzelm@36688
    78
    }
wenzelm@51981
    79
    result.toList
wenzelm@51981
    80
  }
wenzelm@36688
    81
wenzelm@56600
    82
  def separated_chunks(sep: Char => Boolean, source: CharSequence): Iterator[CharSequence] =
wenzelm@48996
    83
    new Iterator[CharSequence] {
wenzelm@48996
    84
      private val end = source.length
wenzelm@48996
    85
      private def next_chunk(i: Int): Option[(CharSequence, Int)] =
wenzelm@48996
    86
      {
wenzelm@48996
    87
        if (i < end) {
wenzelm@56600
    88
          var j = i; do j += 1 while (j < end && !sep(source.charAt(j)))
wenzelm@48996
    89
          Some((source.subSequence(i + 1, j), j))
wenzelm@48996
    90
        }
wenzelm@48996
    91
        else None
wenzelm@43598
    92
      }
wenzelm@48996
    93
      private var state: Option[(CharSequence, Int)] = if (end == 0) None else next_chunk(-1)
wenzelm@48996
    94
wenzelm@48996
    95
      def hasNext(): Boolean = state.isDefined
wenzelm@48996
    96
      def next(): CharSequence =
wenzelm@48996
    97
        state match {
wenzelm@48996
    98
          case Some((s, i)) => { state = next_chunk(i); s }
wenzelm@48996
    99
          case None => Iterator.empty.next()
wenzelm@48996
   100
        }
wenzelm@43598
   101
    }
wenzelm@43598
   102
wenzelm@48996
   103
  def space_explode(sep: Char, str: String): List[String] =
wenzelm@56600
   104
    separated_chunks(_ == sep, str).map(_.toString).toList
wenzelm@48996
   105
wenzelm@48996
   106
wenzelm@48996
   107
  /* lines */
wenzelm@48996
   108
wenzelm@51983
   109
  def terminate_lines(lines: Iterable[CharSequence]): Iterable[CharSequence] =
wenzelm@51983
   110
    new Iterable[CharSequence] {
wenzelm@51983
   111
      def iterator: Iterator[CharSequence] =
wenzelm@51983
   112
        lines.iterator.map(line => new Line_Termination(line))
wenzelm@51983
   113
    }
wenzelm@51983
   114
wenzelm@48996
   115
  def cat_lines(lines: TraversableOnce[String]): String = lines.mkString("\n")
wenzelm@48996
   116
wenzelm@43670
   117
  def split_lines(str: String): List[String] = space_explode('\n', str)
wenzelm@43670
   118
wenzelm@48996
   119
  def first_line(source: CharSequence): String =
wenzelm@48996
   120
  {
wenzelm@56600
   121
    val lines = separated_chunks(_ == '\n', source)
wenzelm@48996
   122
    if (lines.hasNext) lines.next.toString
wenzelm@48996
   123
    else ""
wenzelm@48996
   124
  }
wenzelm@48996
   125
wenzelm@50847
   126
wenzelm@50847
   127
  /* strings */
wenzelm@50847
   128
wenzelm@50847
   129
  def try_unprefix(prfx: String, s: String): Option[String] =
wenzelm@50847
   130
    if (s.startsWith(prfx)) Some(s.substring(prfx.length)) else None
wenzelm@50847
   131
wenzelm@55033
   132
  def try_unsuffix(sffx: String, s: String): Option[String] =
wenzelm@55033
   133
    if (s.endsWith(sffx)) Some(s.substring(0, s.length - sffx.length)) else None
wenzelm@55033
   134
wenzelm@52444
   135
  def trim_line(s: String): String =
wenzelm@52444
   136
    if (s.endsWith("\r\n")) s.substring(0, s.length - 2)
wenzelm@52444
   137
    else if (s.endsWith("\r") || s.endsWith("\n")) s.substring(0, s.length - 1)
wenzelm@52444
   138
    else s
wenzelm@52444
   139
wenzelm@43598
   140
wenzelm@48996
   141
  /* quote */
wenzelm@46196
   142
wenzelm@43598
   143
  def quote(s: String): String = "\"" + s + "\""
wenzelm@56843
   144
wenzelm@56843
   145
  def try_unquote(s: String): Option[String] =
wenzelm@56843
   146
    if (s.startsWith("\"") && s.endsWith("\"")) Some(s.substring(1, s.length - 1))
wenzelm@56843
   147
    else None
wenzelm@56843
   148
wenzelm@58592
   149
  def perhaps_unquote(s: String): String = try_unquote(s) getOrElse s
wenzelm@58592
   150
wenzelm@43598
   151
  def commas(ss: Iterable[String]): String = ss.iterator.mkString(", ")
wenzelm@48362
   152
  def commas_quote(ss: Iterable[String]): String = ss.iterator.map(quote).mkString(", ")
wenzelm@43598
   153
wenzelm@36688
   154
wenzelm@51983
   155
  /* CharSequence */
wenzelm@34141
   156
wenzelm@34141
   157
  class Reverse(text: CharSequence, start: Int, end: Int) extends CharSequence
wenzelm@34141
   158
  {
wenzelm@34141
   159
    require(0 <= start && start <= end && end <= text.length)
wenzelm@34141
   160
wenzelm@34141
   161
    def this(text: CharSequence) = this(text, 0, text.length)
wenzelm@34141
   162
wenzelm@34141
   163
    def length: Int = end - start
wenzelm@34141
   164
    def charAt(i: Int): Char = text.charAt(end - i - 1)
wenzelm@34141
   165
wenzelm@34141
   166
    def subSequence(i: Int, j: Int): CharSequence =
wenzelm@34141
   167
      if (0 <= i && i <= j && j <= length) new Reverse(text, end - j, end - i)
wenzelm@34141
   168
      else throw new IndexOutOfBoundsException
wenzelm@34141
   169
wenzelm@34141
   170
    override def toString: String =
wenzelm@34141
   171
    {
wenzelm@34141
   172
      val buf = new StringBuilder(length)
wenzelm@34141
   173
      for (i <- 0 until length)
wenzelm@34141
   174
        buf.append(charAt(i))
wenzelm@34141
   175
      buf.toString
wenzelm@34141
   176
    }
wenzelm@34141
   177
  }
wenzelm@34141
   178
wenzelm@51983
   179
  class Line_Termination(text: CharSequence) extends CharSequence
wenzelm@51983
   180
  {
wenzelm@51983
   181
    def length: Int = text.length + 1
wenzelm@51983
   182
    def charAt(i: Int): Char = if (i == text.length) '\n' else text.charAt(i)
wenzelm@51983
   183
    def subSequence(i: Int, j: Int): CharSequence =
wenzelm@51983
   184
      if (j == text.length + 1) new Line_Termination(text.subSequence(i, j - 1))
wenzelm@51983
   185
      else text.subSequence(i, j)
wenzelm@51983
   186
    override def toString: String = text.toString + "\n"
wenzelm@51983
   187
  }
wenzelm@51983
   188
wenzelm@34141
   189
wenzelm@59224
   190
  /* regular expressions */
wenzelm@59224
   191
wenzelm@59224
   192
  def make_regex(s: String): Option[Regex] =
wenzelm@59224
   193
    try { Some(new Regex(s)) } catch { case ERROR(_) => None }
wenzelm@59224
   194
wenzelm@59224
   195
wenzelm@56686
   196
  /* canonical list operations */
wenzelm@56686
   197
wenzelm@56688
   198
  def member[A, B](xs: List[A])(x: B): Boolean = xs.exists(_ == x)
wenzelm@56688
   199
  def insert[A](x: A)(xs: List[A]): List[A] = if (xs.contains(x)) xs else x :: xs
wenzelm@56688
   200
  def remove[A, B](x: B)(xs: List[A]): List[A] = if (member(xs)(x)) xs.filterNot(_ == x) else xs
wenzelm@56688
   201
  def update[A](x: A)(xs: List[A]): List[A] = x :: remove(x)(xs)
wenzelm@34136
   202
}
wenzelm@43652
   203
wenzelm@43652
   204
wenzelm@43652
   205
class Basic_Library
wenzelm@43652
   206
{
wenzelm@43670
   207
  val ERROR = Library.ERROR
wenzelm@43670
   208
  val error = Library.error _
wenzelm@43670
   209
  val cat_error = Library.cat_error _
wenzelm@43670
   210
wenzelm@43652
   211
  val space_explode = Library.space_explode _
wenzelm@43670
   212
  val split_lines = Library.split_lines _
wenzelm@46196
   213
  val cat_lines = Library.cat_lines _
wenzelm@43652
   214
  val quote = Library.quote _
wenzelm@43652
   215
  val commas = Library.commas _
wenzelm@43652
   216
  val commas_quote = Library.commas_quote _
wenzelm@43652
   217
}