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