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