diff --git a/src/Pure/System/bash.scala b/src/Pure/System/bash.scala --- a/src/Pure/System/bash.scala +++ b/src/Pure/System/bash.scala @@ -1,234 +1,235 @@ /* Title: Pure/System/bash.scala Author: Makarius GNU bash processes, with propagation of interrupts. */ package isabelle import java.io.{File => JFile, BufferedReader, InputStreamReader, BufferedWriter, OutputStreamWriter} import scala.annotation.tailrec object Bash { /* concrete syntax */ private def bash_chr(c: Byte): String = { val ch = c.toChar ch match { case '\t' => "$'\\t'" case '\n' => "$'\\n'" case '\f' => "$'\\f'" case '\r' => "$'\\r'" case _ => if (Symbol.is_ascii_letter(ch) || Symbol.is_ascii_digit(ch) || "+,-./:_".contains(ch)) Symbol.ascii(ch) else if (c < 0) "$'\\x" + Integer.toHexString(256 + c) + "'" else if (c < 16) "$'\\x0" + Integer.toHexString(c) + "'" else if (c < 32 || c >= 127) "$'\\x" + Integer.toHexString(c) + "'" else "\\" + ch } } def string(s: String): String = if (s == "") "\"\"" else UTF8.bytes(s).iterator.map(bash_chr).mkString def strings(ss: List[String]): String = ss.iterator.map(Bash.string).mkString(" ") /* process and result */ type Watchdog = (Time, Process => Boolean) def process(script: String, cwd: JFile = null, env: Map[String, String] = Isabelle_System.settings(), redirect: Boolean = false, cleanup: () => Unit = () => ()): Process = new Process(script, cwd, env, redirect, cleanup) class Process private[Bash]( script: String, cwd: JFile, env: Map[String, String], redirect: Boolean, cleanup: () => Unit) { private val timing_file = Isabelle_System.tmp_file("bash_timing") private val timing = Synchronized[Option[Timing]](None) def get_timing: Timing = timing.value getOrElse Timing.zero private val script_file = Isabelle_System.tmp_file("bash_script") File.write(script_file, script) private val proc = Isabelle_System.process( List(File.platform_path(Path.variable("ISABELLE_BASH_PROCESS")), "-", File.standard_path(timing_file), "bash", File.standard_path(script_file)), cwd = cwd, env = env, redirect = redirect) // channels val stdin: BufferedWriter = new BufferedWriter(new OutputStreamWriter(proc.getOutputStream, UTF8.charset)) val stdout: BufferedReader = new BufferedReader(new InputStreamReader(proc.getInputStream, UTF8.charset)) val stderr: BufferedReader = new BufferedReader(new InputStreamReader(proc.getErrorStream, UTF8.charset)) // signals private val pid = stdout.readLine @tailrec private def kill(signal: String, count: Int = 1): Boolean = { count <= 0 || { Isabelle_System.kill(signal, pid) val running = Isabelle_System.kill("0", pid)._2 == 0 if (running) { Time.seconds(0.1).sleep kill(signal, count - 1) } else false } } def terminate(): Unit = Isabelle_Thread.try_uninterruptible { kill("INT", count = 7) && kill("TERM", count = 3) && kill("KILL") proc.destroy do_cleanup() } def interrupt(): Unit = Isabelle_Thread.try_uninterruptible { Isabelle_System.kill("INT", pid) } // JVM shutdown hook private val shutdown_hook = Isabelle_Thread.create(() => terminate()) try { Runtime.getRuntime.addShutdownHook(shutdown_hook) } catch { case _: IllegalStateException => } // cleanup private def do_cleanup() { try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) } catch { case _: IllegalStateException => } script_file.delete timing.change { case None => if (timing_file.isFile) { val t = Word.explode(File.read(timing_file)) match { case List(Value.Long(elapsed), Value.Long(cpu)) => Timing(Time.ms(elapsed), Time.ms(cpu), Time.zero) case _ => Timing.zero } timing_file.delete Some(t) } else Some(Timing.zero) case some => some } cleanup() } // join def join: Int = { val rc = proc.waitFor do_cleanup() rc } // result def result( progress_stdout: String => Unit = (_: String) => (), progress_stderr: String => Unit = (_: String) => (), watchdog: Option[Watchdog] = None, strict: Boolean = true): Process_Result = { stdin.close val out_lines = Future.thread("bash_stdout") { File.read_lines(stdout, progress_stdout) } val err_lines = Future.thread("bash_stderr") { File.read_lines(stderr, progress_stderr) } val watchdog_thread = for ((time, check) <- watchdog) yield { Future.thread("bash_watchdog") { while (proc.isAlive) { time.sleep if (check(this)) interrupt() } } } val rc = try { join } catch { case Exn.Interrupt() => terminate(); Exn.Interrupt.return_code } watchdog_thread.foreach(_.cancel) if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt() Process_Result(rc, out_lines.join, err_lines.join, get_timing) } } /* Scala function */ object Process extends Scala.Fun("bash_process") { val here = Scala_Project.here def apply(script: String): String = { val result = Exn.capture { Isabelle_System.bash(script) } val is_interrupt = result match { case Exn.Res(res) => res.rc == Exn.Interrupt.return_code case Exn.Exn(exn) => Exn.is_interrupt(exn) } result match { case _ if is_interrupt => "" case Exn.Exn(exn) => Exn.message(exn) case Exn.Res(res) => - (res.rc.toString :: - res.timing.elapsed.ms.toString :: - res.timing.cpu.ms.toString :: - res.out_lines.length.toString :: - res.out_lines ::: res.err_lines).mkString("\u0000") + Library.cat_strings0( + res.rc.toString :: + res.timing.elapsed.ms.toString :: + res.timing.cpu.ms.toString :: + res.out_lines.length.toString :: + res.out_lines ::: res.err_lines) } } } } diff --git a/src/Pure/System/isabelle_system.ML b/src/Pure/System/isabelle_system.ML --- a/src/Pure/System/isabelle_system.ML +++ b/src/Pure/System/isabelle_system.ML @@ -1,119 +1,119 @@ (* Title: Pure/System/isabelle_system.ML Author: Makarius Isabelle system support. *) signature ISABELLE_SYSTEM = sig val bash_process: string -> Process_Result.T val bash_output: string -> string * int val bash: string -> int val bash_functions: unit -> string list val check_bash_function: Proof.context -> string * Position.T -> string val make_directory: Path.T -> Path.T val copy_dir: Path.T -> Path.T -> unit val copy_file: Path.T -> Path.T -> unit val copy_file_base: Path.T * Path.T -> Path.T -> unit val create_tmp_path: string -> string -> Path.T val with_tmp_file: string -> string -> (Path.T -> 'a) -> 'a val rm_tree: Path.T -> unit val with_tmp_dir: string -> (Path.T -> 'a) -> 'a val download: string -> string end; structure Isabelle_System: ISABELLE_SYSTEM = struct (* bash *) fun bash_process script = Scala.function_thread "bash_process" ("export ISABELLE_TMP=" ^ Bash.string (getenv "ISABELLE_TMP") ^ "\n" ^ script) - |> space_explode "\000" + |> split_strings0 |> (fn [] => raise Exn.Interrupt | [err] => error err | a :: b :: c :: d :: lines => let val rc = Value.parse_int a; val (elapsed, cpu) = apply2 (Time.fromMilliseconds o Value.parse_int) (b, c); val (out_lines, err_lines) = chop (Value.parse_int d) lines; in Process_Result.make {rc = rc, out_lines = out_lines, err_lines = err_lines, timing = {elapsed = elapsed, cpu = cpu, gc = Time.zeroTime}} end | _ => raise Fail "Malformed Isabelle/Scala result"); val bash = bash_process #> Process_Result.print #> Process_Result.rc; fun bash_output s = let val res = bash_process s; val _ = warning (Process_Result.err res); in (Process_Result.out res, Process_Result.rc res) end; (* bash functions *) fun bash_functions () = bash_process "declare -Fx" |> Process_Result.check |> Process_Result.out_lines |> map_filter (space_explode " " #> try List.last); fun check_bash_function ctxt arg = Completion.check_entity Markup.bash_functionN (bash_functions () |> map (rpair Position.none)) ctxt arg; (* directory and file operations *) val absolute_path = Path.implode o File.absolute_path; -fun scala_function0 name = ignore o Scala.function name o space_implode "\000"; +fun scala_function0 name = ignore o Scala.function name o cat_strings0; fun scala_function name = scala_function0 name o map absolute_path; fun make_directory path = (scala_function "make_directory" [path]; path); fun copy_dir src dst = scala_function "copy_dir" [src, dst]; fun copy_file src dst = scala_function "copy_file" [src, dst]; fun copy_file_base (base_dir, src) target_dir = scala_function0 "copy_file_base" [absolute_path base_dir, Path.implode src, absolute_path target_dir]; (* tmp files *) fun create_tmp_path name ext = let val path = File.tmp_path (Path.basic (name ^ serial_string ()) |> Path.ext ext); val _ = File.exists path andalso raise Fail ("Temporary file already exists: " ^ Path.print path); in path end; fun with_tmp_file name ext f = let val path = create_tmp_path name ext in Exn.release (Exn.capture f path before ignore (try File.rm path)) end; (* tmp dirs *) fun rm_tree path = scala_function "rm_tree" [path]; fun with_tmp_dir name f = let val path = create_tmp_path name "" in Exn.release (Exn.capture f (make_directory path) before ignore (try rm_tree path)) end; (* download file *) fun download url = with_tmp_file "download" "" (fn path => (scala_function0 "download" [url, absolute_path path]; File.read path)); end; diff --git a/src/Pure/System/isabelle_system.scala b/src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala +++ b/src/Pure/System/isabelle_system.scala @@ -1,575 +1,575 @@ /* Title: Pure/System/isabelle_system.scala Author: Makarius Fundamental Isabelle system environment: quasi-static module with optional init operation. */ package isabelle import java.io.{File => JFile, IOException} import java.nio.file.{Path => JPath, Files, SimpleFileVisitor, FileVisitResult, StandardCopyOption, FileSystemException} import java.nio.file.attribute.BasicFileAttributes import scala.annotation.tailrec object Isabelle_System { /** bootstrap information **/ def jdk_home(): String = { val java_home = System.getProperty("java.home", "") val home = new JFile(java_home) val parent = home.getParent if (home.getName == "jre" && parent != null && (new JFile(new JFile(parent, "bin"), "javac")).exists) parent else java_home } def bootstrap_directory( preference: String, envar: String, property: String, description: String): String = { val value = proper_string(preference) orElse // explicit argument proper_string(System.getenv(envar)) orElse // e.g. inherited from running isabelle tool proper_string(System.getProperty(property)) getOrElse // e.g. via JVM application boot process error("Unknown " + description + " directory") if ((new JFile(value)).isDirectory) value else error("Bad " + description + " directory " + quote(value)) } /** implicit settings environment **/ abstract class Service @volatile private var _settings: Option[Map[String, String]] = None @volatile private var _services: Option[List[Class[Service]]] = None def settings(): Map[String, String] = { if (_settings.isEmpty) init() // unsynchronized check _settings.get } def services(): List[Class[Service]] = { if (_services.isEmpty) init() // unsynchronized check _services.get } def make_services[C](c: Class[C]): List[C] = for { c1 <- services() if Library.is_subclass(c1, c) } yield c1.getDeclaredConstructor().newInstance().asInstanceOf[C] def init(isabelle_root: String = "", cygwin_root: String = ""): Unit = synchronized { if (_settings.isEmpty || _services.isEmpty) { val isabelle_root1 = bootstrap_directory(isabelle_root, "ISABELLE_ROOT", "isabelle.root", "Isabelle root") val cygwin_root1 = if (Platform.is_windows) bootstrap_directory(cygwin_root, "CYGWIN_ROOT", "cygwin.root", "Cygwin root") else "" if (Platform.is_windows) Cygwin.init(isabelle_root1, cygwin_root1) def set_cygwin_root() { if (Platform.is_windows) _settings = Some(_settings.getOrElse(Map.empty) + ("CYGWIN_ROOT" -> cygwin_root1)) } set_cygwin_root() def default(env: Map[String, String], entry: (String, String)): Map[String, String] = if (env.isDefinedAt(entry._1) || entry._2 == "") env else env + entry val env = { val temp_windows = { val temp = if (Platform.is_windows) System.getenv("TEMP") else null if (temp != null && temp.contains('\\')) temp else "" } val user_home = System.getProperty("user.home", "") val isabelle_app = System.getProperty("isabelle.app", "") default( default( default(sys.env + ("ISABELLE_JDK_HOME" -> File.standard_path(jdk_home())), "TEMP_WINDOWS" -> temp_windows), "HOME" -> user_home), "ISABELLE_APP" -> "true") } val settings = { val dump = JFile.createTempFile("settings", null) dump.deleteOnExit try { val cmd1 = if (Platform.is_windows) List(cygwin_root1 + "\\bin\\bash", "-l", File.standard_path(isabelle_root1 + "\\bin\\isabelle")) else List(isabelle_root1 + "/bin/isabelle") val cmd = cmd1 ::: List("getenv", "-d", dump.toString) val (output, rc) = process_output(process(cmd, env = env, redirect = true)) if (rc != 0) error(output) val entries = - (for (entry <- File.read(dump).split("\u0000") if entry != "") yield { + (for (entry <- Library.split_strings0(File.read(dump)) if entry != "") yield { val i = entry.indexOf('=') if (i <= 0) entry -> "" else entry.substring(0, i) -> entry.substring(i + 1) }).toMap entries + ("PATH" -> entries("PATH_JVM")) - "PATH_JVM" } finally { dump.delete } } _settings = Some(settings) set_cygwin_root() val variable = "ISABELLE_SCALA_SERVICES" val services = for (name <- space_explode(':', settings.getOrElse(variable, getenv_error(variable)))) yield { def err(msg: String): Nothing = error("Bad entry " + quote(name) + " in " + variable + "\n" + msg) try { Class.forName(name).asInstanceOf[Class[Service]] } catch { case _: ClassNotFoundException => err("Class not found") case exn: Throwable => err(Exn.message(exn)) } } _services = Some(services) } } /* getenv */ private def getenv_error(name: String): Nothing = error("Undefined Isabelle environment variable: " + quote(name)) def getenv(name: String, env: Map[String, String] = settings()): String = env.getOrElse(name, "") def getenv_strict(name: String, env: Map[String, String] = settings()): String = proper_string(getenv(name, env)) getOrElse error("Undefined Isabelle environment variable: " + quote(name)) def cygwin_root(): String = getenv_strict("CYGWIN_ROOT") def isabelle_id(): String = proper_string(getenv("ISABELLE_ID")) getOrElse Mercurial.repository(Path.explode("~~")).parent() /** file-system operations **/ /* scala functions */ private def apply_paths(arg: String, fun: List[Path] => Unit): String = - { fun(Library.space_explode('\u0000', arg).map(Path.explode)); "" } + { fun(Library.split_strings0(arg).map(Path.explode)); "" } private def apply_paths1(arg: String, fun: Path => Unit): String = apply_paths(arg, { case List(path) => fun(path) }) private def apply_paths2(arg: String, fun: (Path, Path) => Unit): String = apply_paths(arg, { case List(path1, path2) => fun(path1, path2) }) private def apply_paths3(arg: String, fun: (Path, Path, Path) => Unit): String = apply_paths(arg, { case List(path1, path2, path3) => fun(path1, path2, path3) }) /* permissions */ def chmod(arg: String, path: Path): Unit = bash("chmod " + arg + " " + File.bash_path(path)).check def chown(arg: String, path: Path): Unit = bash("chown " + arg + " " + File.bash_path(path)).check /* directories */ def make_directory(path: Path): Path = { if (!path.is_dir) { try { Files.createDirectories(path.file.toPath) } catch { case ERROR(_) => error("Failed to create directory: " + path.absolute) } } path } def new_directory(path: Path): Path = if (path.is_dir) error("Directory already exists: " + path.absolute) else make_directory(path) def copy_dir(dir1: Path, dir2: Path): Unit = { val res = bash("cp -a " + File.bash_path(dir1) + " " + File.bash_path(dir2)) if (!res.ok) { cat_error("Failed to copy directory " + dir1.absolute + " to " + dir2.absolute, res.err) } } object Make_Directory extends Scala.Fun("make_directory") { val here = Scala_Project.here def apply(arg: String): String = apply_paths1(arg, make_directory) } object Copy_Dir extends Scala.Fun("copy_dir") { val here = Scala_Project.here def apply(arg: String): String = apply_paths2(arg, copy_dir) } /* copy files */ def copy_file(src: JFile, dst: JFile): Unit = { val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst if (!File.eq(src, target)) { try { Files.copy(src.toPath, target.toPath, StandardCopyOption.COPY_ATTRIBUTES, StandardCopyOption.REPLACE_EXISTING) } catch { case ERROR(msg) => cat_error("Failed top copy file " + File.path(src).absolute + " to " + File.path(dst).absolute, msg) } } } def copy_file(src: Path, dst: Path): Unit = copy_file(src.file, dst.file) def copy_file_base(base_dir: Path, src: Path, target_dir: Path): Unit = { val src1 = src.expand val src1_dir = src1.dir if (!src1.starts_basic) error("Illegal path specification " + src1 + " beyond base directory") copy_file(base_dir + src1, Isabelle_System.make_directory(target_dir + src1_dir)) } object Copy_File extends Scala.Fun("copy_file") { val here = Scala_Project.here def apply(arg: String): String = apply_paths2(arg, copy_file) } object Copy_File_Base extends Scala.Fun("copy_file_base") { val here = Scala_Project.here def apply(arg: String): String = apply_paths3(arg, copy_file_base) } /* move files */ def move_file(src: JFile, dst: JFile) { val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst if (!File.eq(src, target)) Files.move(src.toPath, target.toPath, StandardCopyOption.REPLACE_EXISTING) } def move_file(src: Path, dst: Path): Unit = move_file(src.file, dst.file) /* symbolic link */ def symlink(src: Path, dst: Path, force: Boolean = false) { val src_file = src.file val dst_file = dst.file val target = if (dst_file.isDirectory) new JFile(dst_file, src_file.getName) else dst_file if (force) target.delete try { Files.createSymbolicLink(target.toPath, src_file.toPath) } catch { case _: UnsupportedOperationException if Platform.is_windows => Cygwin.link(File.standard_path(src), target) case _: FileSystemException if Platform.is_windows => Cygwin.link(File.standard_path(src), target) } } /* tmp files */ def isabelle_tmp_prefix(): JFile = { val path = Path.explode("$ISABELLE_TMP_PREFIX") path.file.mkdirs // low-level mkdirs to avoid recursion via Isabelle environment File.platform_file(path) } def tmp_file(name: String, ext: String = "", base_dir: JFile = isabelle_tmp_prefix()): JFile = { val suffix = if (ext == "") "" else "." + ext val file = Files.createTempFile(base_dir.toPath, name, suffix).toFile file.deleteOnExit file } def with_tmp_file[A](name: String, ext: String = "")(body: Path => A): A = { val file = tmp_file(name, ext) try { body(File.path(file)) } finally { file.delete } } /* tmp dirs */ def rm_tree(root: JFile): Unit = { root.delete if (root.isDirectory) { Files.walkFileTree(root.toPath, new SimpleFileVisitor[JPath] { override def visitFile(file: JPath, attrs: BasicFileAttributes): FileVisitResult = { try { Files.deleteIfExists(file) } catch { case _: IOException => } FileVisitResult.CONTINUE } override def postVisitDirectory(dir: JPath, e: IOException): FileVisitResult = { if (e == null) { try { Files.deleteIfExists(dir) } catch { case _: IOException => } FileVisitResult.CONTINUE } else throw e } } ) } } def rm_tree(root: Path): Unit = rm_tree(root.file) object Rm_Tree extends Scala.Fun("rm_tree") { val here = Scala_Project.here def apply(arg: String): String = apply_paths1(arg, rm_tree) } def tmp_dir(name: String, base_dir: JFile = isabelle_tmp_prefix()): JFile = { val dir = Files.createTempDirectory(base_dir.toPath, name).toFile dir.deleteOnExit dir } def with_tmp_dir[A](name: String)(body: Path => A): A = { val dir = tmp_dir(name) try { body(File.path(dir)) } finally { rm_tree(dir) } } /* quasi-atomic update of directory */ def update_directory(dir: Path, f: Path => Unit) { val new_dir = dir.ext("new") val old_dir = dir.ext("old") rm_tree(new_dir) rm_tree(old_dir) f(new_dir) if (dir.is_dir) move_file(dir, old_dir) move_file(new_dir, dir) rm_tree(old_dir) } /** external processes **/ /* raw process */ def process(command_line: List[String], cwd: JFile = null, env: Map[String, String] = settings(), redirect: Boolean = false): Process = { val proc = new ProcessBuilder proc.command(command_line:_*) // fragile on Windows if (cwd != null) proc.directory(cwd) if (env != null) { proc.environment.clear for ((x, y) <- env) proc.environment.put(x, y) } proc.redirectErrorStream(redirect) proc.start } def process_output(proc: Process): (String, Int) = { proc.getOutputStream.close val output = File.read_stream(proc.getInputStream) val rc = try { proc.waitFor } finally { proc.getInputStream.close proc.getErrorStream.close proc.destroy Exn.Interrupt.dispose() } (output, rc) } def kill(signal: String, group_pid: String): (String, Int) = { val bash = if (Platform.is_windows) List(cygwin_root() + "\\bin\\bash.exe") else List("/usr/bin/env", "bash") process_output(process(bash ::: List("-c", "kill -" + signal + " -" + group_pid))) } /* GNU bash */ def bash(script: String, cwd: JFile = null, env: Map[String, String] = settings(), redirect: Boolean = false, progress_stdout: String => Unit = (_: String) => (), progress_stderr: String => Unit = (_: String) => (), watchdog: Option[Bash.Watchdog] = None, strict: Boolean = true, cleanup: () => Unit = () => ()): Process_Result = { Bash.process(script, cwd = cwd, env = env, redirect = redirect, cleanup = cleanup). result(progress_stdout = progress_stdout, progress_stderr = progress_stderr, watchdog = watchdog, strict = strict) } private lazy val gnutar_check: Boolean = try { bash("tar --version").check.out.containsSlice("GNU tar") || error("") } catch { case ERROR(_) => false } def gnutar( args: String, dir: Path = Path.current, original_owner: Boolean = false, redirect: Boolean = false): Process_Result = { val options = (if (dir.is_current) "" else "-C " + File.bash_path(dir) + " ") + (if (original_owner) "" else "--owner=root --group=staff ") if (gnutar_check) bash("tar " + options + args, redirect = redirect) else error("Expected to find GNU tar executable") } def require_command(cmds: String*) { for (cmd <- cmds) { if (!bash(Bash.string(cmd) + " --version").ok) error("Missing command: " + quote(cmd)) } } def hostname(): String = bash("hostname -s").check.out def open(arg: String): Unit = bash("exec \"$ISABELLE_OPEN\" " + Bash.string(arg) + " >/dev/null 2>/dev/null &") def pdf_viewer(arg: Path): Unit = bash("exec \"$PDF_VIEWER\" " + File.bash_path(arg) + " >/dev/null 2>/dev/null &") def open_external_file(name: String): Boolean = { val ext = Library.take_suffix((c: Char) => c != '.', name.toList)._2.mkString val external = ext.nonEmpty && Library.space_explode(':', getenv("ISABELLE_EXTERNAL_FILES")).contains(ext) if (external) { if (ext == "pdf" && Path.is_wellformed(name)) pdf_viewer(Path.explode(name)) else open(name) } external } def export_isabelle_identifier(isabelle_identifier: String): String = if (isabelle_identifier == "") "" else "export ISABELLE_IDENTIFIER=" + Bash.string(isabelle_identifier) + "\n" /** Isabelle resources **/ /* repository clone with Admin */ def admin(): Boolean = Path.explode("~~/Admin").is_dir /* components */ def components(): List[Path] = Path.split(getenv_strict("ISABELLE_COMPONENTS")) /* default logic */ def default_logic(args: String*): String = { args.find(_ != "") match { case Some(logic) => logic case None => getenv_strict("ISABELLE_LOGIC") } } /* download file */ private lazy val curl_check: Unit = try { require_command("curl") } catch { case ERROR(msg) => error(msg + " --- cannot download files") } def download(url: String, file: Path, progress: Progress = new Progress): Unit = { curl_check progress.echo("Getting " + quote(url)) try { bash("curl --fail --silent --location " + Bash.string(url) + " > " + File.bash_path(file)).check } catch { case ERROR(msg) => cat_error("Failed to download " + quote(url), msg) } } object Download extends Scala.Fun("download") { val here = Scala_Project.here def apply(arg: String): String = - Library.space_explode('\u0000', arg) match { + Library.split_strings0(arg) match { case List(url, file) => download(url, Path.explode(file)); "" } } } diff --git a/src/Pure/library.ML b/src/Pure/library.ML --- a/src/Pure/library.ML +++ b/src/Pure/library.ML @@ -1,1093 +1,1098 @@ (* Title: Pure/library.ML Author: Lawrence C Paulson, Cambridge University Computer Laboratory Author: Markus Wenzel, TU Muenchen Basic library: functions, pairs, booleans, lists, integers, strings, lists as sets, orders, current directory, misc. See also General/basics.ML for the most fundamental concepts. *) infixr 0 <<< infix 2 ? infix 3 o oo ooo oooo infix 4 ~~ upto downto infix orf andf signature BASIC_LIBRARY = sig (*functions*) val undefined: 'a -> 'b val I: 'a -> 'a val K: 'a -> 'b -> 'a val curry: ('a * 'b -> 'c) -> 'a -> 'b -> 'c val uncurry: ('a -> 'b -> 'c) -> 'a * 'b -> 'c val ? : bool * ('a -> 'a) -> 'a -> 'a val oo: ('a -> 'b) * ('c -> 'd -> 'a) -> 'c -> 'd -> 'b val ooo: ('a -> 'b) * ('c -> 'd -> 'e -> 'a) -> 'c -> 'd -> 'e -> 'b val oooo: ('a -> 'b) * ('c -> 'd -> 'e -> 'f -> 'a) -> 'c -> 'd -> 'e -> 'f -> 'b val funpow: int -> ('a -> 'a) -> 'a -> 'a val funpow_yield: int -> ('a -> 'b * 'a) -> 'a -> 'b list * 'a (*pairs*) val pair: 'a -> 'b -> 'a * 'b val rpair: 'a -> 'b -> 'b * 'a val fst: 'a * 'b -> 'a val snd: 'a * 'b -> 'b val eq_fst: ('a * 'c -> bool) -> ('a * 'b) * ('c * 'd) -> bool val eq_snd: ('b * 'd -> bool) -> ('a * 'b) * ('c * 'd) -> bool val eq_pair: ('a * 'c -> bool) -> ('b * 'd -> bool) -> ('a * 'b) * ('c * 'd) -> bool val swap: 'a * 'b -> 'b * 'a val apfst: ('a -> 'b) -> 'a * 'c -> 'b * 'c val apsnd: ('a -> 'b) -> 'c * 'a -> 'c * 'b val apply2: ('a -> 'b) -> 'a * 'a -> 'b * 'b (*booleans*) val equal: ''a -> ''a -> bool val not_equal: ''a -> ''a -> bool val orf: ('a -> bool) * ('a -> bool) -> 'a -> bool val andf: ('a -> bool) * ('a -> bool) -> 'a -> bool val exists: ('a -> bool) -> 'a list -> bool val forall: ('a -> bool) -> 'a list -> bool (*lists*) val single: 'a -> 'a list val the_single: 'a list -> 'a val singleton: ('a list -> 'b list) -> 'a -> 'b val yield_singleton: ('a list -> 'c -> 'b list * 'c) -> 'a -> 'c -> 'b * 'c val perhaps_apply: ('a -> 'a option) list -> 'a -> 'a option val perhaps_loop: ('a -> 'a option) -> 'a -> 'a option val foldl1: ('a * 'a -> 'a) -> 'a list -> 'a val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a val eq_list: ('a * 'a -> bool) -> 'a list * 'a list -> bool val maps: ('a -> 'b list) -> 'a list -> 'b list val filter: ('a -> bool) -> 'a list -> 'a list val filter_out: ('a -> bool) -> 'a list -> 'a list val map_filter: ('a -> 'b option) -> 'a list -> 'b list val take: int -> 'a list -> 'a list val drop: int -> 'a list -> 'a list val chop: int -> 'a list -> 'a list * 'a list val chop_groups: int -> 'a list -> 'a list list val nth: 'a list -> int -> 'a val nth_list: 'a list list -> int -> 'a list val nth_map: int -> ('a -> 'a) -> 'a list -> 'a list val nth_drop: int -> 'a list -> 'a list val map_index: (int * 'a -> 'b) -> 'a list -> 'b list val fold_index: (int * 'a -> 'b -> 'b) -> 'a list -> 'b -> 'b val map_range: (int -> 'a) -> int -> 'a list val fold_range: (int -> 'a -> 'a) -> int -> 'a -> 'a val split_last: 'a list -> 'a list * 'a val find_first: ('a -> bool) -> 'a list -> 'a option val find_index: ('a -> bool) -> 'a list -> int val get_first: ('a -> 'b option) -> 'a list -> 'b option val get_index: ('a -> 'b option) -> 'a list -> (int * 'b) option val flat: 'a list list -> 'a list val unflat: 'a list list -> 'b list -> 'b list list val grouped: int -> (('a list -> 'b list) -> 'c list list -> 'd list list) -> ('a -> 'b) -> 'c list -> 'd list val burrow: ('a list -> 'b list) -> 'a list list -> 'b list list val burrow_options: ('a list -> 'b list) -> 'a option list -> 'b option list val fold_burrow: ('a list -> 'c -> 'b list * 'd) -> 'a list list -> 'c -> 'b list list * 'd val separate: 'a -> 'a list -> 'a list val surround: 'a -> 'a list -> 'a list val replicate: int -> 'a -> 'a list val map_product: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list val fold_product: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c val map2: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list val fold2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c val map_split: ('a -> 'b * 'c) -> 'a list -> 'b list * 'c list val zip_options: 'a list -> 'b option list -> ('a * 'b) list val ~~ : 'a list * 'b list -> ('a * 'b) list val split_list: ('a * 'b) list -> 'a list * 'b list val burrow_fst: ('a list -> 'b list) -> ('a * 'c) list -> ('b * 'c) list val take_prefix: ('a -> bool) -> 'a list -> 'a list val drop_prefix: ('a -> bool) -> 'a list -> 'a list val chop_prefix: ('a -> bool) -> 'a list -> 'a list * 'a list val take_suffix: ('a -> bool) -> 'a list -> 'a list val drop_suffix: ('a -> bool) -> 'a list -> 'a list val chop_suffix: ('a -> bool) -> 'a list -> 'a list * 'a list val is_prefix: ('a * 'a -> bool) -> 'a list -> 'a list -> bool val chop_common_prefix: ('a * 'b -> bool) -> 'a list * 'b list -> 'a list * ('a list * 'b list) val prefixes1: 'a list -> 'a list list val prefixes: 'a list -> 'a list list val suffixes1: 'a list -> 'a list list val suffixes: 'a list -> 'a list list val trim: ('a -> bool) -> 'a list -> 'a list (*integers*) val upto: int * int -> int list val downto: int * int -> int list val hex_digit: int -> string val radixpand: int * int -> int list val radixstring: int * string * int -> string val string_of_int: int -> string val signed_string_of_int: int -> string val string_of_indexname: string * int -> string val read_radix_int: int -> string list -> int * string list val read_int: string list -> int * string list val oct_char: string -> string (*strings*) val nth_string: string -> int -> string val fold_string: (string -> 'a -> 'a) -> string -> 'a -> 'a val exists_string: (string -> bool) -> string -> bool val forall_string: (string -> bool) -> string -> bool val first_field: string -> string -> (string * string) option val enclose: string -> string -> string -> string val unenclose: string -> string val quote: string -> string val cartouche: string -> string val space_implode: string -> string list -> string val commas: string list -> string val commas_quote: string list -> string val cat_lines: string list -> string val space_explode: string -> string -> string list val split_lines: string -> string list + val cat_strings0: string list -> string + val split_strings0: string -> string list val plain_words: string -> string val prefix_lines: string -> string -> string val prefix: string -> string -> string val suffix: string -> string -> string val unprefix: string -> string -> string val unsuffix: string -> string -> string val trim_line: string -> string val trim_split_lines: string -> string list val normalize_lines: string -> string val replicate_string: int -> string -> string val translate_string: (string -> string) -> string -> string val encode_lines: string -> string val decode_lines: string -> string val align_right: string -> int -> string -> string val match_string: string -> string -> bool (*reals*) val string_of_real: real -> string val signed_string_of_real: real -> string (*lists as sets -- see also Pure/General/ord_list.ML*) val member: ('b * 'a -> bool) -> 'a list -> 'b -> bool val insert: ('a * 'a -> bool) -> 'a -> 'a list -> 'a list val remove: ('b * 'a -> bool) -> 'b -> 'a list -> 'a list val update: ('a * 'a -> bool) -> 'a -> 'a list -> 'a list val union: ('a * 'a -> bool) -> 'a list -> 'a list -> 'a list val subtract: ('b * 'a -> bool) -> 'b list -> 'a list -> 'a list val inter: ('a * 'b -> bool) -> 'b list -> 'a list -> 'a list val merge: ('a * 'a -> bool) -> 'a list * 'a list -> 'a list val subset: ('a * 'b -> bool) -> 'a list * 'b list -> bool val eq_set: ('a * 'a -> bool) -> 'a list * 'a list -> bool val distinct: ('a * 'a -> bool) -> 'a list -> 'a list val duplicates: ('a * 'a -> bool) -> 'a list -> 'a list val has_duplicates: ('a * 'a -> bool) -> 'a list -> bool val map_transpose: ('a list -> 'b) -> 'a list list -> 'b list (*lists as multisets*) val remove1: ('b * 'a -> bool) -> 'b -> 'a list -> 'a list val combine: ('a * 'a -> bool) -> 'a list -> 'a list -> 'a list val submultiset: ('a * 'b -> bool) -> 'a list * 'b list -> bool (*orders*) type 'a ord = 'a * 'a -> order val is_equal: order -> bool val is_less: order -> bool val is_less_equal: order -> bool val is_greater: order -> bool val is_greater_equal: order -> bool val rev_order: order -> order val make_ord: ('a * 'a -> bool) -> 'a ord val bool_ord: bool ord val int_ord: int ord val string_ord: string ord val fast_string_ord: string ord val option_ord: ('a * 'b -> order) -> 'a option * 'b option -> order val <<< : ('a -> order) * ('a -> order) -> 'a -> order val prod_ord: ('a * 'b -> order) -> ('c * 'd -> order) -> ('a * 'c) * ('b * 'd) -> order val dict_ord: ('a * 'b -> order) -> 'a list * 'b list -> order val list_ord: ('a * 'b -> order) -> 'a list * 'b list -> order val sort: 'a ord -> 'a list -> 'a list val sort_distinct: 'a ord -> 'a list -> 'a list val sort_strings: string list -> string list val sort_by: ('a -> string) -> 'a list -> 'a list val tag_list: int -> 'a list -> (int * 'a) list val untag_list: (int * 'a) list -> 'a list val order_list: (int * 'a) list -> 'a list (*misc*) val divide_and_conquer: ('a -> 'a list * ('b list -> 'b)) -> 'a -> 'b val divide_and_conquer': ('a -> 'b -> ('a list * ('c list * 'b -> 'c * 'b)) * 'b) -> 'a -> 'b -> 'c * 'b val partition_eq: ('a * 'a -> bool) -> 'a list -> 'a list list val partition_list: (int -> 'a -> bool) -> int -> int -> 'a list -> 'a list list type serial = int val serial: unit -> serial val serial_string: unit -> string eqtype stamp val stamp: unit -> stamp structure Any: sig type T = exn end val getenv: string -> string val getenv_strict: string -> string end; signature LIBRARY = sig include BASIC_LIBRARY val foldl: ('a * 'b -> 'a) -> 'a * 'b list -> 'a val foldr: ('a * 'b -> 'b) -> 'a list * 'b -> 'b end; structure Library: LIBRARY = struct (* functions *) fun undefined _ = raise Match; fun I x = x; fun K x = fn _ => x; fun curry f x y = f (x, y); fun uncurry f (x, y) = f x y; (*conditional application*) fun b ? f = fn x => if b then f x else x; (*composition with multiple args*) fun (f oo g) x y = f (g x y); fun (f ooo g) x y z = f (g x y z); fun (f oooo g) x y z w = f (g x y z w); (*function exponentiation: f (... (f x) ...) with n applications of f*) fun funpow (0: int) _ x = x | funpow n f x = funpow (n - 1) f (f x); fun funpow_yield (0 : int) _ x = ([], x) | funpow_yield n f x = x |> f ||>> funpow_yield (n - 1) f |>> op ::; (* pairs *) fun pair x y = (x, y); fun rpair x y = (y, x); fun fst (x, y) = x; fun snd (x, y) = y; fun eq_fst eq ((x1, _), (x2, _)) = eq (x1, x2); fun eq_snd eq ((_, y1), (_, y2)) = eq (y1, y2); fun eq_pair eqx eqy ((x1, y1), (x2, y2)) = eqx (x1, x2) andalso eqy (y1, y2); fun swap (x, y) = (y, x); fun apfst f (x, y) = (f x, y); fun apsnd f (x, y) = (x, f y); fun apply2 f (x, y) = (f x, f y); (* booleans *) (*polymorphic equality*) fun equal x y = x = y; fun not_equal x y = x <> y; (*combining predicates*) fun p orf q = fn x => p x orelse q x; fun p andf q = fn x => p x andalso q x; val exists = List.exists; val forall = List.all; (** lists **) fun single x = [x]; fun the_single [x] = x | the_single _ = raise List.Empty; fun singleton f x = the_single (f [x]); fun yield_singleton f x = f [x] #>> the_single; fun perhaps_apply funs arg = let fun app [] res = res | app (f :: fs) (changed, x) = (case f x of NONE => app fs (changed, x) | SOME x' => app fs (true, x')); in (case app funs (false, arg) of (false, _) => NONE | (true, arg') => SOME arg') end; fun perhaps_loop f arg = let fun loop (changed, x) = (case f x of NONE => (changed, x) | SOME x' => loop (true, x')); in (case loop (false, arg) of (false, _) => NONE | (true, arg') => SOME arg') end; (* fold -- old versions *) (*the following versions of fold are designed to fit nicely with infixes*) (* (op @) (e, [x1, ..., xn]) ===> ((e @ x1) @ x2) ... @ xn for operators that associate to the left (TAIL RECURSIVE)*) fun foldl (f: 'a * 'b -> 'a) : 'a * 'b list -> 'a = let fun itl (e, []) = e | itl (e, a::l) = itl (f(e, a), l) in itl end; (* (op @) ([x1, ..., xn], e) ===> x1 @ (x2 ... @ (xn @ e)) for operators that associate to the right (not tail recursive)*) fun foldr f (l, e) = let fun itr [] = e | itr (a::l) = f(a, itr l) in itr l end; (* (op @) [x1, ..., xn] ===> ((x1 @ x2) @ x3) ... @ xn for operators that associate to the left (TAIL RECURSIVE)*) fun foldl1 f [] = raise List.Empty | foldl1 f (x :: xs) = foldl f (x, xs); (* (op @) [x1, ..., xn] ===> x1 @ (x2 ... @ (x[n-1] @ xn)) for n > 0, operators that associate to the right (not tail recursive)*) fun foldr1 f [] = raise List.Empty | foldr1 f l = let fun itr [x] = x | itr (x::l) = f(x, itr l) in itr l end; (* basic list functions *) fun eq_list eq (list1, list2) = pointer_eq (list1, list2) orelse let fun eq_lst (x :: xs, y :: ys) = eq (x, y) andalso eq_lst (xs, ys) | eq_lst _ = true; in length list1 = length list2 andalso eq_lst (list1, list2) end; fun maps f [] = [] | maps f (x :: xs) = f x @ maps f xs; val filter = List.filter; fun filter_out f = filter (not o f); val map_filter = List.mapPartial; fun take (0: int) xs = [] | take _ [] = [] | take n (x :: xs) = x :: take (n - 1) xs; fun drop (0: int) xs = xs | drop _ [] = [] | drop n (x :: xs) = drop (n - 1) xs; fun chop (0: int) xs = ([], xs) | chop _ [] = ([], []) | chop n (x :: xs) = chop (n - 1) xs |>> cons x; fun chop_groups n list = (case chop (Int.max (n, 1)) list of ([], _) => [] | (g, rest) => g :: chop_groups n rest); (*return nth element of a list, where 0 designates the first element; raise Subscript if list too short*) fun nth xs i = List.nth (xs, i); fun nth_list xss i = nth xss i handle General.Subscript => []; fun nth_map 0 f (x :: xs) = f x :: xs | nth_map n f (x :: xs) = x :: nth_map (n - 1) f xs | nth_map (_: int) _ [] = raise Subscript; fun nth_drop n xs = List.take (xs, n) @ List.drop (xs, n + 1); fun map_index f = let fun map_aux (_: int) [] = [] | map_aux i (x :: xs) = f (i, x) :: map_aux (i + 1) xs in map_aux 0 end; fun fold_index f = let fun fold_aux (_: int) [] y = y | fold_aux i (x :: xs) y = fold_aux (i + 1) xs (f (i, x) y) in fold_aux 0 end; fun map_range f i = let fun map_aux (k: int) = if k < i then f k :: map_aux (k + 1) else [] in map_aux 0 end; fun fold_range f i = let fun fold_aux (k: int) y = if k < i then fold_aux (k + 1) (f k y) else y in fold_aux 0 end; (*rear decomposition*) fun split_last [] = raise List.Empty | split_last [x] = ([], x) | split_last (x :: xs) = apfst (cons x) (split_last xs); (*find first element satisfying predicate*) val find_first = List.find; (*find position of first element satisfying a predicate*) fun find_index pred = let fun find (_: int) [] = ~1 | find n (x :: xs) = if pred x then n else find (n + 1) xs; in find 0 end; (*get first element by lookup function*) fun get_first _ [] = NONE | get_first f (x :: xs) = (case f x of NONE => get_first f xs | some => some); fun get_index f = let fun get_aux (_: int) [] = NONE | get_aux i (x :: xs) = (case f x of NONE => get_aux (i + 1) xs | SOME y => SOME (i, y)) in get_aux 0 end; val flat = List.concat; fun unflat (xs :: xss) ys = let val (ps, qs) = chop (length xs) ys in ps :: unflat xss qs end | unflat [] [] = [] | unflat _ _ = raise ListPair.UnequalLengths; fun grouped n comb f = chop_groups n #> comb (map f) #> flat; fun burrow f xss = unflat xss (f (flat xss)); fun burrow_options f os = map (try hd) (burrow f (map the_list os)); fun fold_burrow f xss s = apfst (unflat xss) (f (flat xss) s); (*separate s [x1, x2, ..., xn] ===> [x1, s, x2, s, ..., s, xn]*) fun separate s (x :: (xs as _ :: _)) = x :: s :: separate s xs | separate _ xs = xs; fun surround s (x :: xs) = s :: x :: surround s xs | surround s [] = [s]; (*make the list [x, x, ..., x] of length n*) fun replicate (n: int) x = let fun rep (0, xs) = xs | rep (n, xs) = rep (n - 1, x :: xs) in if n < 0 then raise Subscript else rep (n, []) end; (* direct product *) fun map_product f _ [] = [] | map_product f [] _ = [] | map_product f (x :: xs) ys = map (f x) ys @ map_product f xs ys; fun fold_product f _ [] z = z | fold_product f [] _ z = z | fold_product f (x :: xs) ys z = z |> fold (f x) ys |> fold_product f xs ys; (* lists of pairs *) fun map2 _ [] [] = [] | map2 f (x :: xs) (y :: ys) = f x y :: map2 f xs ys | map2 _ _ _ = raise ListPair.UnequalLengths; fun fold2 _ [] [] z = z | fold2 f (x :: xs) (y :: ys) z = fold2 f xs ys (f x y z) | fold2 _ _ _ _ = raise ListPair.UnequalLengths; fun map_split _ [] = ([], []) | map_split f (x :: xs) = let val (y, w) = f x; val (ys, ws) = map_split f xs; in (y :: ys, w :: ws) end; fun zip_options (x :: xs) (SOME y :: ys) = (x, y) :: zip_options xs ys | zip_options (_ :: xs) (NONE :: ys) = zip_options xs ys | zip_options _ [] = [] | zip_options [] _ = raise ListPair.UnequalLengths; (*combine two lists forming a list of pairs: [x1, ..., xn] ~~ [y1, ..., yn] ===> [(x1, y1), ..., (xn, yn)]*) fun [] ~~ [] = [] | (x :: xs) ~~ (y :: ys) = (x, y) :: (xs ~~ ys) | _ ~~ _ = raise ListPair.UnequalLengths; (*inverse of ~~; the old 'split': [(x1, y1), ..., (xn, yn)] ===> ([x1, ..., xn], [y1, ..., yn])*) val split_list = ListPair.unzip; fun burrow_fst f xs = split_list xs |>> f |> op ~~; (* take, drop, chop, trim according to predicate *) fun take_prefix pred list = let fun take res (x :: xs) = if pred x then take (x :: res) xs else rev res | take res [] = rev res; in take [] list end; fun drop_prefix pred list = let fun drop (x :: xs) = if pred x then drop xs else x :: xs | drop [] = []; in drop list end; fun chop_prefix pred list = let val prfx = take_prefix pred list; val sffx = drop (length prfx) list; in (prfx, sffx) end; fun take_suffix pred list = let fun take res (x :: xs) = if pred x then take (x :: res) xs else res | take res [] = res; in take [] (rev list) end; fun drop_suffix pred list = let fun drop (x :: xs) = if pred x then drop xs else rev (x :: xs) | drop [] = []; in drop (rev list) end; fun chop_suffix pred list = let val prfx = drop_suffix pred list; val sffx = drop (length prfx) list; in (prfx, sffx) end; fun trim pred = drop_prefix pred #> drop_suffix pred; (* prefixes, suffixes *) fun is_prefix _ [] _ = true | is_prefix eq (x :: xs) (y :: ys) = eq (x, y) andalso is_prefix eq xs ys | is_prefix eq _ _ = false; fun chop_common_prefix eq ([], ys) = ([], ([], ys)) | chop_common_prefix eq (xs, []) = ([], (xs, [])) | chop_common_prefix eq (xs as x :: xs', ys as y :: ys') = if eq (x, y) then let val (ps', xys'') = chop_common_prefix eq (xs', ys') in (x :: ps', xys'') end else ([], (xs, ys)); fun prefixes1 [] = [] | prefixes1 (x :: xs) = map (cons x) ([] :: prefixes1 xs); fun prefixes xs = [] :: prefixes1 xs; fun suffixes1 xs = map rev (prefixes1 (rev xs)); fun suffixes xs = [] :: suffixes1 xs; (** integers **) (* lists of integers *) (*make the list [from, from + 1, ..., to]*) fun ((i: int) upto j) = if i > j then [] else i :: (i + 1 upto j); (*make the list [from, from - 1, ..., to]*) fun ((i: int) downto j) = if i < j then [] else i :: (i - 1 downto j); (* convert integers to strings *) (*hexadecimal*) fun hex_digit i = if i < 10 then chr (Char.ord #"0" + i) else chr (Char.ord #"a" + i - 10); (*expand the number in the given base; example: radixpand (2, 8) gives [1, 0, 0, 0]*) fun radixpand (base, num) : int list = let fun radix (n, tail) = if n < base then n :: tail else radix (n div base, (n mod base) :: tail) in radix (num, []) end; (*expands a number into a string of characters starting from "zerochar"; example: radixstring (2, "0", 8) gives "1000"*) fun radixstring (base, zerochar, num) = let val offset = ord zerochar; fun chrof n = chr (offset + n) in implode (map chrof (radixpand (base, num))) end; local val zero = Char.ord #"0"; val small_int = 10000: int; val small_int_table = Vector.tabulate (small_int, Int.toString); in fun string_of_int i = if i < 0 then Int.toString i else if i < 10 then chr (zero + i) else if i < small_int then Vector.sub (small_int_table, i) else Int.toString i; end; fun signed_string_of_int i = if i < 0 then "-" ^ string_of_int (~ i) else string_of_int i; fun string_of_indexname (a, 0) = a | string_of_indexname (a, i) = a ^ "_" ^ string_of_int i; (* read integers *) fun read_radix_int radix cs = let val zero = Char.ord #"0"; val limit = zero + radix; fun scan (num, []) = (num, []) | scan (num, c :: cs) = if zero <= ord c andalso ord c < limit then scan (radix * num + (ord c - zero), cs) else (num, c :: cs); in scan (0, cs) end; val read_int = read_radix_int 10; fun oct_char s = chr (#1 (read_radix_int 8 (raw_explode s))); (** strings **) (* functions tuned for strings, avoiding explode *) fun nth_string str i = (case try String.substring (str, i, 1) of SOME s => s | NONE => raise Subscript); fun fold_string f str x0 = let val n = size str; fun iter (x, i) = if i < n then iter (f (String.substring (str, i, 1)) x, i + 1) else x; in iter (x0, 0) end; fun exists_string pred str = let val n = size str; fun ex i = i < n andalso (pred (String.substring (str, i, 1)) orelse ex (i + 1)); in ex 0 end; fun forall_string pred = not o exists_string (not o pred); fun first_field sep str = let val n = size sep; val len = size str; fun find i = if i + n > len then NONE else if String.substring (str, i, n) = sep then SOME i else find (i + 1); in (case find 0 of NONE => NONE | SOME i => SOME (String.substring (str, 0, i), String.extract (str, i + n, NONE))) end; (*enclose in brackets*) fun enclose lpar rpar str = lpar ^ str ^ rpar; fun unenclose str = String.substring (str, 1, size str - 2); (*simple quoting (does not escape special chars)*) val quote = enclose "\"" "\""; val cartouche = enclose "\" "\"; val space_implode = String.concatWith; val commas = space_implode ", "; val commas_quote = commas o map quote; val cat_lines = space_implode "\n"; (*space_explode "." "h.e..l.lo" = ["h", "e", "", "l", "lo"]*) fun space_explode _ "" = [] | space_explode sep s = String.fields (fn c => str c = sep) s; val split_lines = space_explode "\n"; +val cat_strings0 = space_implode "\000"; +val split_strings0 = space_explode "\000"; + fun plain_words s = space_explode "_" s |> space_implode " "; fun prefix_lines "" txt = txt | prefix_lines prfx txt = txt |> split_lines |> map (fn s => prfx ^ s) |> cat_lines; fun prefix prfx s = prfx ^ s; fun suffix sffx s = s ^ sffx; fun unprefix prfx s = if String.isPrefix prfx s then String.substring (s, size prfx, size s - size prfx) else raise Fail "unprefix"; fun unsuffix sffx s = if String.isSuffix sffx s then String.substring (s, 0, size s - size sffx) else raise Fail "unsuffix"; fun trim_line s = if String.isSuffix "\r\n" s then String.substring (s, 0, size s - 2) else if String.isSuffix "\r" s orelse String.isSuffix "\n" s then String.substring (s, 0, size s - 1) else s; val trim_split_lines = trim_line #> split_lines #> map trim_line; fun normalize_lines str = if exists_string (fn s => s = "\r") str then split_lines str |> map trim_line |> cat_lines else str; fun replicate_string (0: int) _ = "" | replicate_string 1 a = a | replicate_string k a = if k mod 2 = 0 then replicate_string (k div 2) (a ^ a) else replicate_string (k div 2) (a ^ a) ^ a; fun translate_string f = String.translate (f o String.str); val encode_lines = translate_string (fn "\n" => "\v" | c => c); val decode_lines = translate_string (fn "\v" => "\n" | c => c); fun align_right c k s = let val _ = if size c <> 1 orelse size s > k then raise Fail "align_right" else () in replicate_string (k - size s) c ^ s end; (*crude matching of str against simple glob pat*) fun match_string pat str = let fun match [] _ = true | match (p :: ps) s = size p <= size s andalso (case try (unprefix p) s of SOME s' => match ps s' | NONE => match (p :: ps) (String.substring (s, 1, size s - 1))); in match (space_explode "*" pat) str end; (** reals **) val string_of_real = Real.fmt (StringCvt.GEN NONE); fun signed_string_of_real x = if x < 0.0 then "-" ^ string_of_real (~ x) else string_of_real x; (** lists as sets -- see also Pure/General/ord_list.ML **) (* canonical operations *) fun member eq list x = let fun memb [] = false | memb (y :: ys) = eq (x, y) orelse memb ys; in memb list end; fun insert eq x xs = if member eq xs x then xs else x :: xs; fun remove eq x xs = if member eq xs x then filter_out (fn y => eq (x, y)) xs else xs; fun update eq x xs = cons x (remove eq x xs); fun inter eq xs = filter (member eq xs); fun union eq = fold (insert eq); fun subtract eq = fold (remove eq); fun merge eq (xs, ys) = if pointer_eq (xs, ys) then xs else if null xs then ys else fold_rev (insert eq) ys xs; (* subset and set equality *) fun subset eq (xs, ys) = forall (member eq ys) xs; fun eq_set eq (xs, ys) = eq_list eq (xs, ys) orelse (subset eq (xs, ys) andalso subset (eq o swap) (ys, xs)); (*makes a list of the distinct members of the input; preserves order, takes first of equal elements*) fun distinct eq lst = let fun dist (rev_seen, []) = rev rev_seen | dist (rev_seen, x :: xs) = if member eq rev_seen x then dist (rev_seen, xs) else dist (x :: rev_seen, xs); in dist ([], lst) end; (*returns a list containing all repeated elements exactly once; preserves order, takes first of equal elements*) fun duplicates eq lst = let fun dups (rev_dups, []) = rev rev_dups | dups (rev_dups, x :: xs) = if member eq rev_dups x orelse not (member eq xs x) then dups (rev_dups, xs) else dups (x :: rev_dups, xs); in dups ([], lst) end; fun has_duplicates eq = let fun dups [] = false | dups (x :: xs) = member eq xs x orelse dups xs; in dups end; (* matrices *) fun map_transpose f xss = let val n = (case distinct (op =) (map length xss) of [] => 0 | [n] => n | _ => raise ListPair.UnequalLengths); in map_range (fn m => f (map (fn xs => nth xs m) xss)) n end; (** lists as multisets **) fun remove1 eq x [] = [] | remove1 eq x (y :: ys) = if eq (x, y) then ys else y :: remove1 eq x ys; fun combine eq xs ys = fold (remove1 eq) ys xs @ ys; fun submultiset _ ([], _) = true | submultiset eq (x :: xs, ys) = member eq ys x andalso submultiset eq (xs, remove1 eq x ys); (** orders **) type 'a ord = 'a * 'a -> order; fun is_equal ord = ord = EQUAL; fun is_less ord = ord = LESS; fun is_less_equal ord = ord = LESS orelse ord = EQUAL; fun is_greater ord = ord = GREATER; fun is_greater_equal ord = ord = GREATER orelse ord = EQUAL; fun rev_order LESS = GREATER | rev_order EQUAL = EQUAL | rev_order GREATER = LESS; (*compose orders*) fun (a_ord <<< b_ord) p = (case a_ord p of EQUAL => b_ord p | ord => ord); (*assume rel is a linear strict order*) fun make_ord rel (x, y) = if rel (x, y) then LESS else if rel (y, x) then GREATER else EQUAL; fun bool_ord (false, true) = LESS | bool_ord (true, false) = GREATER | bool_ord _ = EQUAL; val int_ord = Int.compare; val string_ord = String.compare; fun fast_string_ord (s1, s2) = if pointer_eq (s1, s2) then EQUAL else (case int_ord (size s1, size s2) of EQUAL => string_ord (s1, s2) | ord => ord); fun option_ord ord (SOME x, SOME y) = ord (x, y) | option_ord _ (NONE, NONE) = EQUAL | option_ord _ (NONE, SOME _) = LESS | option_ord _ (SOME _, NONE) = GREATER; (*lexicographic product*) fun prod_ord a_ord b_ord ((x, y), (x', y')) = (case a_ord (x, x') of EQUAL => b_ord (y, y') | ord => ord); (*dictionary order -- in general NOT well-founded!*) fun dict_ord elem_ord (x :: xs, y :: ys) = (case elem_ord (x, y) of EQUAL => dict_ord elem_ord (xs, ys) | ord => ord) | dict_ord _ ([], []) = EQUAL | dict_ord _ ([], _ :: _) = LESS | dict_ord _ (_ :: _, []) = GREATER; (*lexicographic product of lists*) fun list_ord elem_ord (xs, ys) = (case int_ord (length xs, length ys) of EQUAL => dict_ord elem_ord (xs, ys) | ord => ord); (* sorting *) (*stable mergesort -- preserves order of equal elements*) fun mergesort unique ord = let fun merge (xs as x :: xs') (ys as y :: ys') = (case ord (x, y) of LESS => x :: merge xs' ys | EQUAL => if unique then merge xs ys' else x :: merge xs' ys | GREATER => y :: merge xs ys') | merge [] ys = ys | merge xs [] = xs; fun merge_all [xs] = xs | merge_all xss = merge_all (merge_pairs xss) and merge_pairs (xs :: ys :: xss) = merge xs ys :: merge_pairs xss | merge_pairs xss = xss; fun runs (x :: y :: xs) = (case ord (x, y) of LESS => ascending y [x] xs | EQUAL => if unique then runs (x :: xs) else ascending y [x] xs | GREATER => descending y [x] xs) | runs xs = [xs] and ascending x xs (zs as y :: ys) = (case ord (x, y) of LESS => ascending y (x :: xs) ys | EQUAL => if unique then ascending x xs ys else ascending y (x :: xs) ys | GREATER => rev (x :: xs) :: runs zs) | ascending x xs [] = [rev (x :: xs)] and descending x xs (zs as y :: ys) = (case ord (x, y) of GREATER => descending y (x :: xs) ys | EQUAL => if unique then descending x xs ys else (x :: xs) :: runs zs | LESS => (x :: xs) :: runs zs) | descending x xs [] = [x :: xs]; in merge_all o runs end; fun sort ord = mergesort false ord; fun sort_distinct ord = mergesort true ord; val sort_strings = sort string_ord; fun sort_by key xs = sort (string_ord o apply2 key) xs; (* items tagged by integer index *) (*insert tags*) fun tag_list k [] = [] | tag_list k (x :: xs) = (k:int, x) :: tag_list (k + 1) xs; (*remove tags and suppress duplicates -- list is assumed sorted!*) fun untag_list [] = [] | untag_list [(k: int, x)] = [x] | untag_list ((k, x) :: (rest as (k', x') :: _)) = if k = k' then untag_list rest else x :: untag_list rest; (*return list elements in original order*) fun order_list list = untag_list (sort (int_ord o apply2 fst) list); (** misc **) fun divide_and_conquer decomp x = let val (ys, recomb) = decomp x in recomb (map (divide_and_conquer decomp) ys) end; fun divide_and_conquer' decomp x s = let val ((ys, recomb), s') = decomp x s in recomb (fold_map (divide_and_conquer' decomp) ys s') end; (*Partition a list into buckets [ bi, b(i+1), ..., bj ] putting x in bk if p(k)(x) holds. Preserve order of elements if possible.*) fun partition_list p i j = let fun part (k: int) xs = if k > j then (case xs of [] => [] | _ => raise Fail "partition_list") else let val (ns, rest) = List.partition (p k) xs in ns :: part (k + 1) rest end; in part (i: int) end; fun partition_eq (eq: 'a * 'a -> bool) = let fun part [] = [] | part (x :: ys) = let val (xs, xs') = List.partition (fn y => eq (x, y)) ys in (x :: xs) :: part xs' end; in part end; (* serial numbers and abstract stamps *) type serial = int; val serial = Counter.make (); val serial_string = string_of_int o serial; datatype stamp = Stamp of serial; fun stamp () = Stamp (serial ()); (* values of any type *) (*note that the builtin exception datatype may be extended by new constructors at any time*) structure Any = struct type T = exn end; (* getenv *) fun getenv x = (case OS.Process.getEnv x of NONE => "" | SOME y => y); fun getenv_strict x = (case getenv x of "" => error ("Undefined Isabelle environment variable: " ^ quote x) | y => y); end; structure Basic_Library: BASIC_LIBRARY = Library; open Basic_Library; diff --git a/src/Pure/library.scala b/src/Pure/library.scala --- a/src/Pure/library.scala +++ b/src/Pure/library.scala @@ -1,295 +1,298 @@ /* Title: Pure/library.scala Author: Makarius Basic library. */ package isabelle import scala.annotation.tailrec import scala.collection.mutable import scala.util.matching.Regex object Library { /* resource management */ def using[A <: AutoCloseable, B](a: A)(f: A => B): B = { try { f(a) } finally { if (a != null) a.close() } } /* integers */ private val small_int = 10000 private lazy val small_int_table = { val array = new Array[String](small_int) for (i <- 0 until small_int) array(i) = i.toString array } def is_small_int(s: String): Boolean = { val len = s.length 1 <= len && len <= 4 && s.forall(c => '0' <= c && c <= '9') && (len == 1 || s(0) != '0') } def signed_string_of_long(i: Long): String = if (0 <= i && i < small_int) small_int_table(i.toInt) else i.toString def signed_string_of_int(i: Int): String = if (0 <= i && i < small_int) small_int_table(i) else i.toString /* separated chunks */ def separate[A](s: A, list: List[A]): List[A] = { val result = new mutable.ListBuffer[A] var first = true for (x <- list) { if (first) { first = false result += x } else { result += s result += x } } result.toList } def separated_chunks(sep: Char => Boolean, source: CharSequence): Iterator[CharSequence] = new Iterator[CharSequence] { private val end = source.length private def next_chunk(i: Int): Option[(CharSequence, Int)] = { if (i < end) { var j = i; do j += 1 while (j < end && !sep(source.charAt(j))) Some((source.subSequence(i + 1, j), j)) } else None } private var state: Option[(CharSequence, Int)] = if (end == 0) None else next_chunk(-1) def hasNext(): Boolean = state.isDefined def next(): CharSequence = state match { case Some((s, i)) => state = next_chunk(i); s case None => Iterator.empty.next() } } def space_explode(sep: Char, str: String): List[String] = separated_chunks(_ == sep, str).map(_.toString).toList /* lines */ def terminate_lines(lines: TraversableOnce[String]): String = lines.mkString("", "\n", "\n") def cat_lines(lines: TraversableOnce[String]): String = lines.mkString("\n") def split_lines(str: String): List[String] = space_explode('\n', str) def prefix_lines(prfx: String, str: String): String = if (str == "") str else cat_lines(split_lines(str).map(prfx + _)) def first_line(source: CharSequence): String = { val lines = separated_chunks(_ == '\n', source) if (lines.hasNext) lines.next.toString else "" } def trim_line(s: String): String = if (s.endsWith("\r\n")) s.substring(0, s.length - 2) else if (s.endsWith("\r") || s.endsWith("\n")) s.substring(0, s.length - 1) else s def trim_split_lines(s: String): List[String] = split_lines(trim_line(s)).map(trim_line) def encode_lines(s: String): String = s.replace('\n', '\u000b') def decode_lines(s: String): String = s.replace('\u000b', '\n') /* strings */ + def cat_strings0(strs: TraversableOnce[String]): String = strs.mkString("\u0000") + def split_strings0(str: String): List[String] = space_explode('\u0000', str) + def make_string(f: StringBuilder => Unit): String = { val s = new StringBuilder f(s) s.toString } def try_unprefix(prfx: String, s: String): Option[String] = if (s.startsWith(prfx)) Some(s.substring(prfx.length)) else None def try_unsuffix(sffx: String, s: String): Option[String] = if (s.endsWith(sffx)) Some(s.substring(0, s.length - sffx.length)) else None def perhaps_unprefix(prfx: String, s: String): String = try_unprefix(prfx, s) getOrElse s def perhaps_unsuffix(sffx: String, s: String): String = try_unsuffix(sffx, s) getOrElse s def isolate_substring(s: String): String = new String(s.toCharArray) def strip_ansi_color(s: String): String = s.replaceAll("""\u001b\[\d+m""", "") /* quote */ def single_quote(s: String): String = "'" + s + "'" def quote(s: String): String = "\"" + s + "\"" def try_unquote(s: String): Option[String] = if (s.startsWith("\"") && s.endsWith("\"")) Some(s.substring(1, s.length - 1)) else None def perhaps_unquote(s: String): String = try_unquote(s) getOrElse s def commas(ss: Iterable[String]): String = ss.iterator.mkString(", ") def commas_quote(ss: Iterable[String]): String = ss.iterator.map(quote).mkString(", ") /* CharSequence */ class Reverse(text: CharSequence, start: Int, end: Int) extends CharSequence { require(0 <= start && start <= end && end <= text.length, "bad reverse range") def this(text: CharSequence) = this(text, 0, text.length) def length: Int = end - start def charAt(i: Int): Char = text.charAt(end - i - 1) def subSequence(i: Int, j: Int): CharSequence = if (0 <= i && i <= j && j <= length) new Reverse(text, end - j, end - i) else throw new IndexOutOfBoundsException override def toString: String = { val buf = new StringBuilder(length) for (i <- 0 until length) buf.append(charAt(i)) buf.toString } } class Line_Termination(text: CharSequence) extends CharSequence { def length: Int = text.length + 1 def charAt(i: Int): Char = if (i == text.length) '\n' else text.charAt(i) def subSequence(i: Int, j: Int): CharSequence = if (j == text.length + 1) new Line_Termination(text.subSequence(i, j - 1)) else text.subSequence(i, j) override def toString: String = text.toString + "\n" } /* regular expressions */ def make_regex(s: String): Option[Regex] = try { Some(new Regex(s)) } catch { case ERROR(_) => None } def is_regex_meta(c: Char): Boolean = """()[]{}\^$|?*+.<>-=!""".contains(c) def escape_regex(s: String): String = if (s.exists(is_regex_meta)) { (for (c <- s.iterator) yield { if (is_regex_meta(c)) "\\" + c.toString else c.toString }).mkString } else s /* lists */ def take_prefix[A](pred: A => Boolean, xs: List[A]): (List[A], List[A]) = (xs.takeWhile(pred), xs.dropWhile(pred)) def take_suffix[A](pred: A => Boolean, xs: List[A]): (List[A], List[A]) = { val rev_xs = xs.reverse (rev_xs.dropWhile(pred).reverse, rev_xs.takeWhile(pred).reverse) } def trim[A](pred: A => Boolean, xs: List[A]): List[A] = take_suffix(pred, take_prefix(pred, xs)._2)._1 def member[A, B](xs: List[A])(x: B): Boolean = xs.contains(x) def insert[A](x: A)(xs: List[A]): List[A] = if (xs.contains(x)) xs else x :: xs def remove[A, B](x: B)(xs: List[A]): List[A] = if (member(xs)(x)) xs.filterNot(_ == x) else xs def update[A](x: A)(xs: List[A]): List[A] = x :: remove(x)(xs) def merge[A](xs: List[A], ys: List[A]): List[A] = if (xs.eq(ys)) xs else if (xs.isEmpty) ys else ys.foldRight(xs)(Library.insert(_)(_)) def distinct[A](xs: List[A], eq: (A, A) => Boolean = (x: A, y: A) => x == y): List[A] = { val result = new mutable.ListBuffer[A] xs.foreach(x => if (!result.exists(y => eq(x, y))) result += x) result.toList } def duplicates[A](lst: List[A], eq: (A, A) => Boolean = (x: A, y: A) => x == y): List[A] = { val result = new mutable.ListBuffer[A] @tailrec def dups(rest: List[A]): Unit = rest match { case Nil => case x :: xs => if (!result.exists(y => eq(x, y)) && xs.exists(y => eq(x, y))) result += x dups(xs) } dups(lst) result.toList } def replicate[A](n: Int, a: A): List[A] = if (n < 0) throw new IllegalArgumentException else if (n == 0) Nil else { val res = new mutable.ListBuffer[A] (1 to n).foreach(_ => res += a) res.toList } /* proper values */ def proper_string(s: String): Option[String] = if (s == null || s == "") None else Some(s) def proper_list[A](list: List[A]): Option[List[A]] = if (list == null || list.isEmpty) None else Some(list) /* reflection */ def is_subclass[A, B](a: Class[A], b: Class[B]): Boolean = { @tailrec def subclass(c: Class[_]): Boolean = { c == b || { val d = c.getSuperclass d != null && subclass(d) } } subclass(a) } }