1/* Title: Pure/library.scala 2 Author: Makarius 3 4Basic library. 5*/ 6 7package isabelle 8 9 10import scala.annotation.tailrec 11import scala.collection.mutable 12import scala.util.matching.Regex 13 14 15object 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 else cat_lines(split_lines(str).map(prfx + _)) 107 108 def first_line(source: CharSequence): String = 109 { 110 val lines = separated_chunks(_ == '\n', source) 111 if (lines.hasNext) lines.next.toString 112 else "" 113 } 114 115 def encode_lines(s: String): String = s.replace('\n', '\u000b') 116 def decode_lines(s: String): String = s.replace('\u000b', '\n') 117 118 119 /* strings */ 120 121 def make_string(f: StringBuilder => Unit): String = 122 { 123 val s = new StringBuilder 124 f(s) 125 s.toString 126 } 127 128 def try_unprefix(prfx: String, s: String): Option[String] = 129 if (s.startsWith(prfx)) Some(s.substring(prfx.length)) else None 130 131 def try_unsuffix(sffx: String, s: String): Option[String] = 132 if (s.endsWith(sffx)) Some(s.substring(0, s.length - sffx.length)) else None 133 134 def perhaps_unprefix(prfx: String, s: String): String = try_unprefix(prfx, s) getOrElse s 135 def perhaps_unsuffix(sffx: String, s: String): String = try_unsuffix(sffx, s) getOrElse s 136 137 def trim_line(s: String): String = 138 if (s.endsWith("\r\n")) s.substring(0, s.length - 2) 139 else if (s.endsWith("\r") || s.endsWith("\n")) s.substring(0, s.length - 1) 140 else s 141 142 def trim_split_lines(s: String): List[String] = 143 split_lines(trim_line(s)).map(trim_line(_)) 144 145 def isolate_substring(s: String): String = new String(s.toCharArray) 146 147 148 /* quote */ 149 150 def single_quote(s: String): String = "'" + s + "'" 151 152 def quote(s: String): String = "\"" + s + "\"" 153 154 def try_unquote(s: String): Option[String] = 155 if (s.startsWith("\"") && s.endsWith("\"")) Some(s.substring(1, s.length - 1)) 156 else None 157 158 def perhaps_unquote(s: String): String = try_unquote(s) getOrElse s 159 160 def commas(ss: Iterable[String]): String = ss.iterator.mkString(", ") 161 def commas_quote(ss: Iterable[String]): String = ss.iterator.map(quote).mkString(", ") 162 163 164 /* CharSequence */ 165 166 class Reverse(text: CharSequence, start: Int, end: Int) extends CharSequence 167 { 168 require(0 <= start && start <= end && end <= text.length) 169 170 def this(text: CharSequence) = this(text, 0, text.length) 171 172 def length: Int = end - start 173 def charAt(i: Int): Char = text.charAt(end - i - 1) 174 175 def subSequence(i: Int, j: Int): CharSequence = 176 if (0 <= i && i <= j && j <= length) new Reverse(text, end - j, end - i) 177 else throw new IndexOutOfBoundsException 178 179 override def toString: String = 180 { 181 val buf = new StringBuilder(length) 182 for (i <- 0 until length) 183 buf.append(charAt(i)) 184 buf.toString 185 } 186 } 187 188 class Line_Termination(text: CharSequence) extends CharSequence 189 { 190 def length: Int = text.length + 1 191 def charAt(i: Int): Char = if (i == text.length) '\n' else text.charAt(i) 192 def subSequence(i: Int, j: Int): CharSequence = 193 if (j == text.length + 1) new Line_Termination(text.subSequence(i, j - 1)) 194 else text.subSequence(i, j) 195 override def toString: String = text.toString + "\n" 196 } 197 198 199 /* regular expressions */ 200 201 def make_regex(s: String): Option[Regex] = 202 try { Some(new Regex(s)) } catch { case ERROR(_) => None } 203 204 def is_regex_meta(c: Char): Boolean = """()[]{}\^$|?*+.<>-=!""".contains(c) 205 206 def escape_regex(s: String): String = 207 if (s.exists(is_regex_meta(_))) { 208 (for (c <- s.iterator) 209 yield { if (is_regex_meta(c)) "\\" + c.toString else c.toString }).mkString 210 } 211 else s 212 213 214 /* lists */ 215 216 def take_prefix[A](pred: A => Boolean, xs: List[A]): (List[A], List[A]) = 217 (xs.takeWhile(pred), xs.dropWhile(pred)) 218 219 def take_suffix[A](pred: A => Boolean, xs: List[A]): (List[A], List[A]) = 220 { 221 val rev_xs = xs.reverse 222 (rev_xs.dropWhile(pred).reverse, rev_xs.takeWhile(pred).reverse) 223 } 224 225 def trim[A](pred: A => Boolean, xs: List[A]): List[A] = 226 take_suffix(pred, take_prefix(pred, xs)._2)._1 227 228 def member[A, B](xs: List[A])(x: B): Boolean = xs.contains(x) 229 def insert[A](x: A)(xs: List[A]): List[A] = if (xs.contains(x)) xs else x :: xs 230 def remove[A, B](x: B)(xs: List[A]): List[A] = if (member(xs)(x)) xs.filterNot(_ == x) else xs 231 def update[A](x: A)(xs: List[A]): List[A] = x :: remove(x)(xs) 232 233 def merge[A](xs: List[A], ys: List[A]): List[A] = 234 if (xs.eq(ys)) xs 235 else if (xs.isEmpty) ys 236 else ys.foldRight(xs)(Library.insert(_)(_)) 237 238 def distinct[A](xs: List[A], eq: (A, A) => Boolean = (x: A, y: A) => x == y): List[A] = 239 { 240 val result = new mutable.ListBuffer[A] 241 xs.foreach(x => if (!result.exists(y => eq(x, y))) result += x) 242 result.toList 243 } 244 245 def duplicates[A](lst: List[A], eq: (A, A) => Boolean = (x: A, y: A) => x == y): List[A] = 246 { 247 val result = new mutable.ListBuffer[A] 248 @tailrec def dups(rest: List[A]): Unit = 249 rest match { 250 case Nil => 251 case x :: xs => 252 if (!result.exists(y => eq(x, y)) && xs.exists(y => eq(x, y))) result += x 253 dups(xs) 254 } 255 dups(lst) 256 result.toList 257 } 258 259 def replicate[A](n: Int, a: A): List[A] = 260 if (n < 0) throw new IllegalArgumentException 261 else if (n == 0) Nil 262 else { 263 val res = new mutable.ListBuffer[A] 264 (1 to n).foreach(_ => res += a) 265 res.toList 266 } 267 268 269 /* proper values */ 270 271 def proper_string(s: String): Option[String] = 272 if (s == null || s == "") None else Some(s) 273 274 def proper_list[A](list: List[A]): Option[List[A]] = 275 if (list == null || list.isEmpty) None else Some(list) 276} 277