diff --git a/src/Pure/General/bytes.ML b/src/Pure/General/bytes.ML --- a/src/Pure/General/bytes.ML +++ b/src/Pure/General/bytes.ML @@ -1,112 +1,164 @@ (* Title: Pure/General/bytes.ML Author: Makarius Scalable byte strings, with incremental construction (add content to the end). Note: type string is implicitly limited by String.maxSize (approx. 64 MB on 64_32 architecture). *) signature BYTES = sig val chunk_size: int type T val length: T -> int val contents: T -> string list + val contents_blob: T -> XML.body val content: T -> string val is_empty: T -> bool val empty: T + val build: (T -> T) -> T val add_substring: substring -> T -> T val add: string -> T -> T + val beginning: int -> T -> string + val exists_string: (string -> bool) -> T -> bool + val forall_string: (string -> bool) -> T -> bool + val last_string: T -> string option + val trim_line: T -> T val append: T -> T -> T - val build: (T -> T) -> T val string: string -> T + val newline: T val buffer: Buffer.T -> T - val read_chunk: BinIO.instream -> string - val read_stream: BinIO.instream -> T + val read_block: int -> BinIO.instream -> string + val read_stream: int -> BinIO.instream -> T val write_stream: BinIO.outstream -> T -> unit val read: Path.T -> T val write: Path.T -> T -> unit end; structure Bytes: BYTES = struct (* primitive operations *) val chunk_size = 1024 * 1024; abstype T = Bytes of {buffer: string list, chunks: string list, m: int (*buffer size*), n: int (*chunks size*)} with fun length (Bytes {m, n, ...}) = m + n; val compact = implode o rev; fun contents (Bytes {buffer, chunks, ...}) = rev (chunks |> not (null buffer) ? cons (compact buffer)); +val contents_blob = contents #> XML.blob; + val content = implode o contents; fun is_empty bytes = length bytes = 0; val empty = Bytes {buffer = [], chunks = [], m = 0, n = 0}; +fun build (f: T -> T) = f empty; + fun add_substring s (bytes as Bytes {buffer, chunks, m, n}) = if Substring.isEmpty s then bytes else let val l = Substring.size s in if l + m < chunk_size then Bytes {buffer = Substring.string s :: buffer, chunks = chunks, m = l + m, n = n} else let val k = chunk_size - m; val chunk = compact (Substring.string (Substring.slice (s, 0, SOME k)) :: buffer); val s' = Substring.slice (s, k, SOME (l - k)); val bytes' = Bytes {buffer = [], chunks = chunk :: chunks, m = 0, n = chunk_size + n}; in add_substring s' bytes' end end; val add = add_substring o Substring.full; +fun exists_string pred (Bytes {buffer, chunks, ...}) = + let val ex = (exists o Library.exists_string) pred + in ex buffer orelse ex chunks end; + +fun forall_string pred = not o exists_string (not o pred); + +fun last_string (Bytes {buffer, chunks, ...}) = + (case buffer of + s :: _ => Library.last_string s + | [] => + (case chunks of + s :: _ => Library.last_string s + | [] => NONE)); + +fun trim_line (bytes as Bytes {buffer, chunks, ...}) = + let + val is_line = + (case last_string bytes of + SOME s => Symbol.is_ascii_line_terminator s + | NONE => false); + in + if is_line then + let + val (last_chunk, chunks') = + (case chunks of + [] => ("", []) + | c :: cs => (c, cs)); + val trimed = Library.trim_line (last_chunk ^ compact buffer); + in build (fold_rev add chunks' #> add trimed) end + else bytes + end; + end; (* derived operations *) +fun beginning n bytes = + let + val dots = " ..."; + val m = (String.maxSize - size dots) div chunk_size; + val a = implode (take m (contents bytes)); + val b = String.substring (a, 0, Int.min (n, size a)); + in if size b < length bytes then b ^ dots else b end; + fun append bytes1 bytes2 = (*left-associative*) if is_empty bytes1 then bytes2 else if is_empty bytes2 then bytes1 else bytes1 |> fold add (contents bytes2); -fun build (f: T -> T) = f empty; +val string = build o add; -val string = build o add; +val newline = string "\n"; val buffer = build o fold add o Buffer.contents; -val read_chunk = File.input_size chunk_size; +fun read_block limit = + File.input_size (if limit < 0 then chunk_size else Int.min (chunk_size, limit)); -fun read_stream stream = +fun read_stream limit stream = let - fun read_bytes bytes = - (case read_chunk stream of + fun read bytes = + (case read_block (limit - length bytes) stream of "" => bytes - | s => read_bytes (add s bytes)) - in read_bytes empty end; + | s => read (add s bytes)) + in read empty end; fun write_stream stream = File.outputs stream o contents; -val read = File.open_input read_stream; +val read = File.open_input (read_stream ~1); val write = File.open_output write_stream; (* ML pretty printing *) val _ = ML_system_pp (fn _ => fn _ => fn bytes => PolyML.PrettyString ("Bytes {length = " ^ string_of_int (length bytes) ^ "}")) end; diff --git a/src/Pure/General/socket_io.ML b/src/Pure/General/socket_io.ML --- a/src/Pure/General/socket_io.ML +++ b/src/Pure/General/socket_io.ML @@ -1,101 +1,101 @@ (* Title: Pure/General/socket_io.ML Author: Timothy Bourke, NICTA Author: Makarius Stream IO over TCP sockets. Following example 10.2 in "The Standard ML Basis Library" by Emden R. Gansner and John H. Reppy. *) signature SOCKET_IO = sig val make_streams: Socket.active INetSock.stream_sock -> BinIO.instream * BinIO.outstream val open_streams: string -> BinIO.instream * BinIO.outstream val with_streams: (BinIO.instream * BinIO.outstream -> 'a) -> string -> 'a val with_streams': (BinIO.instream * BinIO.outstream -> 'a) -> string -> string -> 'a end; structure Socket_IO: SOCKET_IO = struct fun close_permissive socket = Socket.close socket handle OS.SysErr _ => (); fun make_streams socket = let val (host, port) = INetSock.fromAddr (Socket.Ctl.getSockName socket); val name = NetHostDB.toString host ^ ":" ^ string_of_int port; val rd = BinPrimIO.RD { name = name, chunkSize = 4096, readVec = SOME (fn n => Socket.recvVec (socket, n)), readArr = SOME (fn buffer => Socket.recvArr (socket, buffer)), readVecNB = NONE, readArrNB = NONE, block = NONE, canInput = NONE, avail = fn () => NONE, getPos = NONE, setPos = NONE, endPos = NONE, verifyPos = NONE, close = fn () => close_permissive socket, ioDesc = NONE }; val wr = BinPrimIO.WR { name = name, chunkSize = 4096, writeVec = SOME (fn buffer => Socket.sendVec (socket, buffer)), writeArr = SOME (fn buffer => Socket.sendArr (socket, buffer)), writeVecNB = NONE, writeArrNB = NONE, block = NONE, canOutput = NONE, getPos = NONE, setPos = NONE, endPos = NONE, verifyPos = NONE, close = fn () => close_permissive socket, ioDesc = NONE }; val in_stream = BinIO.mkInstream (BinIO.StreamIO.mkInstream (rd, Word8Vector.fromList [])); val out_stream = BinIO.mkOutstream (BinIO.StreamIO.mkOutstream (wr, IO.BLOCK_BUF)); in (in_stream, out_stream) end; fun open_streams socket_name = let fun err () = error ("Bad socket name: " ^ quote socket_name); val (host, port) = (case space_explode ":" socket_name of [h, p] => (case NetHostDB.getByName h of SOME host => host | NONE => err (), case Int.fromString p of SOME port => port | NONE => err ()) | _ => err ()); val socket: Socket.active INetSock.stream_sock = INetSock.TCP.socket (); val _ = Socket.connect (socket, INetSock.toAddr (NetHostDB.addr host, port)); in make_streams socket end handle OS.SysErr (msg, _) => error (msg ^ ": failed to open socket " ^ socket_name); fun with_streams f = Thread_Attributes.uninterruptible (fn restore_attributes => fn socket_name => let val streams = open_streams socket_name; val result = Exn.capture (restore_attributes f) streams; in BinIO.closeIn (#1 streams); BinIO.closeOut (#2 streams); Exn.release result end); fun with_streams' f socket_name password = with_streams (fn streams => - (Byte_Message.write_line (#2 streams) password; f streams)) socket_name; + (Byte_Message.write_line (#2 streams) (Bytes.string password); f streams)) socket_name; end; diff --git a/src/Pure/PIDE/byte_message.ML b/src/Pure/PIDE/byte_message.ML --- a/src/Pure/PIDE/byte_message.ML +++ b/src/Pure/PIDE/byte_message.ML @@ -1,116 +1,127 @@ (* Title: Pure/General/byte_message.ML Author: Makarius Byte-oriented messages. *) signature BYTE_MESSAGE = sig - val write: BinIO.outstream -> string list -> unit + val write: BinIO.outstream -> Bytes.T list -> unit val write_yxml: BinIO.outstream -> XML.tree -> unit val flush: BinIO.outstream -> unit - val write_line: BinIO.outstream -> string -> unit - val read: BinIO.instream -> int -> string - val read_block: BinIO.instream -> int -> string option * int - val read_line: BinIO.instream -> string option - val write_message: BinIO.outstream -> string list -> unit + val write_line: BinIO.outstream -> Bytes.T -> unit + val read: BinIO.instream -> int -> Bytes.T + val read_block: BinIO.instream -> int -> Bytes.T option * int + val read_line: BinIO.instream -> Bytes.T option + val write_message: BinIO.outstream -> Bytes.T list -> unit + val write_message_string: BinIO.outstream -> string list -> unit val write_message_yxml: BinIO.outstream -> XML.body list -> unit - val read_message: BinIO.instream -> string list option - val write_line_message: BinIO.outstream -> string -> unit - val read_line_message: BinIO.instream -> string option + val read_message: BinIO.instream -> Bytes.T list option + val read_message_string: BinIO.instream -> string list option + val write_line_message: BinIO.outstream -> Bytes.T -> unit + val read_line_message: BinIO.instream -> Bytes.T option end; structure Byte_Message: BYTE_MESSAGE = struct (* output operations *) -val write = File.outputs; +val write = List.app o Bytes.write_stream; fun write_yxml stream tree = YXML.traverse (fn s => fn () => File.output stream s) tree (); fun flush stream = ignore (try BinIO.flushOut stream); -fun write_line stream s = (write stream [s, "\n"]; flush stream); +fun write_line stream bs = (write stream [bs, Bytes.newline]; flush stream); (* input operations *) -fun read stream n = File.input_size n stream; +fun read stream n = Bytes.read_stream n stream; fun read_block stream n = let val msg = read stream n; - val len = size msg; + val len = Bytes.length msg; in (if len = n then SOME msg else NONE, len) end; fun read_line stream = let - val result = trim_line o String.implode o rev; - fun read_body cs = + val result = SOME o Bytes.trim_line; + fun read_body bs = (case BinIO.input1 stream of - NONE => if null cs then NONE else SOME (result cs) + NONE => if Bytes.is_empty bs then NONE else result bs | SOME b => (case Byte.byteToChar b of - #"\n" => SOME (result cs) - | c => read_body (c :: cs))); - in read_body [] end; + #"\n" => result bs + | c => read_body (Bytes.add (str c) bs))); + in read_body Bytes.empty end; (* messages with multiple chunks (arbitrary content) *) fun make_header ns = - [space_implode "," (map Value.print_int ns), "\n"]; + [Bytes.string (space_implode "," (map Value.print_int ns)), Bytes.newline]; fun write_message stream chunks = - (write stream (make_header (map size chunks) @ chunks); flush stream); + (write stream (make_header (map Bytes.length chunks) @ chunks); flush stream); + +fun write_message_string stream = + write_message stream o map Bytes.string; fun write_message_yxml stream chunks = (write stream (make_header (map YXML.body_size chunks)); (List.app o List.app) (write_yxml stream) chunks; flush stream); fun parse_header line = map Value.parse_nat (space_explode "," line) handle Fail _ => error ("Malformed message header: " ^ quote line); fun read_chunk stream n = (case read_block stream n of (SOME chunk, _) => chunk | (NONE, len) => error ("Malformed message chunk: unexpected EOF after " ^ string_of_int len ^ " of " ^ string_of_int n ^ " bytes")); fun read_message stream = - read_line stream |> Option.map (parse_header #> map (read_chunk stream)); + read_line stream |> Option.map (Bytes.content #> parse_header #> map (read_chunk stream)); + +fun read_message_string stream = + read_message stream |> (Option.map o map) Bytes.content; (* hybrid messages: line or length+block (with content restriction) *) +(* line message format *) + fun is_length msg = - msg <> "" andalso forall_string Symbol.is_ascii_digit msg; + not (Bytes.is_empty msg) andalso Bytes.forall_string Symbol.is_ascii_digit msg; fun is_terminated msg = - let val len = size msg - in len > 0 andalso Symbol.is_ascii_line_terminator (str (String.sub (msg, len - 1))) end; + (case Bytes.last_string msg of + NONE => false + | SOME s => Symbol.is_ascii_line_terminator s); fun write_line_message stream msg = if is_length msg orelse is_terminated msg then - error ("Bad content for line message:\n" ^ implode (take 100 (Symbol.explode msg))) + error ("Bad content for line message:\n" ^ Bytes.beginning 100 msg) else - let val n = size msg in + let val n = Bytes.length msg in write stream - ((if n > 100 orelse exists_string (fn s => s = "\n") msg - then make_header [n + 1] else []) @ [msg, "\n"]); + ((if n > 100 orelse Bytes.exists_string (fn s => s = "\n") msg + then make_header [n + 1] else []) @ [msg, Bytes.newline]); flush stream end; fun read_line_message stream = (case read_line stream of NONE => NONE | SOME line => - (case try Value.parse_nat line of + (case try (Value.parse_nat o Bytes.content) line of NONE => SOME line - | SOME n => Option.map trim_line (#1 (read_block stream n)))); + | SOME n => Option.map Bytes.trim_line (#1 (read_block stream n)))); end; diff --git a/src/Pure/PIDE/protocol_command.ML b/src/Pure/PIDE/protocol_command.ML --- a/src/Pure/PIDE/protocol_command.ML +++ b/src/Pure/PIDE/protocol_command.ML @@ -1,47 +1,50 @@ (* Title: Pure/PIDE/protocol_command.ML Author: Makarius Protocol commands. *) signature PROTOCOL_COMMAND = sig exception STOP of int val is_protocol_exn: exn -> bool + val define_bytes: string -> (Bytes.T list -> unit) -> unit val define: string -> (string list -> unit) -> unit - val run: string -> string list -> unit + val run: string -> Bytes.T list -> unit end; structure Protocol_Command: PROTOCOL_COMMAND = struct exception STOP of int; val is_protocol_exn = fn STOP _ => true | _ => false; local val commands = Synchronized.var "Protocol_Command.commands" - (Symtab.empty: (string list -> unit) Symtab.table); + (Symtab.empty: (Bytes.T list -> unit) Symtab.table); in -fun define name cmd = +fun define_bytes name cmd = Synchronized.change commands (fn cmds => (if not (Symtab.defined cmds name) then () else warning ("Redefining Isabelle protocol command " ^ quote name); Symtab.update (name, cmd) cmds)); +fun define name cmd = define_bytes name (map Bytes.content #> cmd); + fun run name args = (case Symtab.lookup (Synchronized.value commands) name of NONE => error ("Undefined Isabelle protocol command " ^ quote name) | SOME cmd => (Runtime.exn_trace_system (fn () => cmd args) handle exn => if is_protocol_exn exn then Exn.reraise exn else error ("Isabelle protocol command failure: " ^ quote name))); end; end; diff --git a/src/Pure/System/isabelle_process.ML b/src/Pure/System/isabelle_process.ML --- a/src/Pure/System/isabelle_process.ML +++ b/src/Pure/System/isabelle_process.ML @@ -1,226 +1,226 @@ (* Title: Pure/System/isabelle_process.ML Author: Makarius Isabelle process wrapper. *) signature ISABELLE_PROCESS = sig val is_active: unit -> bool val reset_tracing: Document_ID.exec -> unit val crashes: exn list Synchronized.var val init_options: unit -> unit val init_options_interactive: unit -> unit val init: unit -> unit val init_build: unit -> unit end; structure Isabelle_Process: ISABELLE_PROCESS = struct (* print mode *) val isabelle_processN = "isabelle_process"; fun is_active () = Print_Mode.print_mode_active isabelle_processN; val _ = Output.add_mode isabelle_processN Output.default_output Output.default_escape; val _ = Markup.add_mode isabelle_processN YXML.output_markup; val protocol_modes1 = [Syntax_Trans.no_bracketsN, Syntax_Trans.no_type_bracketsN]; val protocol_modes2 = [isabelle_processN, Pretty.symbolicN]; (* restricted tracing messages *) val tracing_messages = Synchronized.var "tracing_messages" (Inttab.empty: int Inttab.table); fun reset_tracing exec_id = Synchronized.change tracing_messages (Inttab.delete_safe exec_id); fun update_tracing () = (case Position.parse_id (Position.thread_data ()) of NONE => () | SOME exec_id => let val ok = Synchronized.change_result tracing_messages (fn tab => let val n = the_default 0 (Inttab.lookup tab exec_id) + 1; val limit = Options.default_int "editor_tracing_messages"; val ok = limit <= 0 orelse n <= limit; in (ok, Inttab.update (exec_id, n) tab) end); in if ok then () else let val (text, promise) = Active.dialog_text (); val _ = writeln ("Tracing paused. " ^ text "Stop" ^ ", or continue with next " ^ text "100" ^ ", " ^ text "1000" ^ ", " ^ text "10000" ^ " messages?") val m = Value.parse_int (Future.join promise) handle Fail _ => error "Stopped"; in Synchronized.change tracing_messages (Inttab.map_default (exec_id, 0) (fn k => k - m)) end end); (* init protocol -- uninterruptible *) val crashes = Synchronized.var "Isabelle_Process.crashes" ([]: exn list); local fun recover crash = (Synchronized.change crashes (cons crash); Output.physical_stderr "Recovered from Isabelle process crash -- see also Isabelle_Process.crashes\n"); fun ml_statistics () = Output.protocol_message (Markup.ML_statistics {pid = ML_Pid.get (), stats_dir = getenv "POLYSTATSDIR"}) []; in fun init_protocol modes = Thread_Attributes.uninterruptible (fn _ => fn (address, password) => let val _ = SHA1.test_samples () handle exn as Fail msg => (Output.physical_stderr (msg ^ "\n"); Exn.reraise exn); val _ = Output.physical_stderr Symbol.STX; (* streams *) val (in_stream, out_stream) = Socket_IO.open_streams address; - val _ = Byte_Message.write_line out_stream password; + val _ = Byte_Message.write_line out_stream (Bytes.string password); val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdOut, IO.LINE_BUF); val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdErr, IO.LINE_BUF); val _ = BinIO.StreamIO.setBufferMode (BinIO.getOutstream out_stream, IO.BLOCK_BUF); (* messages *) val message_channel = Message_Channel.make out_stream; val message = Message_Channel.message message_channel; fun standard_message props name ss = if forall (fn s => s = "") ss then () else let val pos_props = if exists Markup.position_property props then props else props @ Position.properties_of (Position.thread_data ()); in message name pos_props [XML.blob ss] end; fun report_message ss = if Context_Position.pide_reports () then standard_message [] Markup.reportN ss else (); val serial_props = Markup.serial_properties o serial; val message_context = Unsynchronized.setmp Private_Output.status_fn (standard_message [] Markup.statusN) #> Unsynchronized.setmp Private_Output.report_fn report_message #> Unsynchronized.setmp Private_Output.result_fn (fn props => fn s => standard_message (props @ serial_props ()) Markup.resultN s) #> Unsynchronized.setmp Private_Output.writeln_fn (fn s => standard_message (serial_props ()) Markup.writelnN s) #> Unsynchronized.setmp Private_Output.state_fn (fn s => standard_message (serial_props ()) Markup.stateN s) #> Unsynchronized.setmp Private_Output.information_fn (fn s => standard_message (serial_props ()) Markup.informationN s) #> Unsynchronized.setmp Private_Output.tracing_fn (fn s => (update_tracing (); standard_message (serial_props ()) Markup.tracingN s)) #> Unsynchronized.setmp Private_Output.warning_fn (fn s => standard_message (serial_props ()) Markup.warningN s) #> Unsynchronized.setmp Private_Output.legacy_fn (fn s => standard_message (serial_props ()) Markup.legacyN s) #> Unsynchronized.setmp Private_Output.error_message_fn (fn (i, s) => standard_message (Markup.serial_properties i) Markup.errorN s) #> Unsynchronized.setmp Private_Output.system_message_fn (fn ss => message Markup.systemN [] [XML.blob ss]) #> Unsynchronized.setmp Private_Output.protocol_message_fn (fn props => fn chunks => message Markup.protocolN props chunks) #> Unsynchronized.setmp print_mode ((! print_mode @ #1 modes) |> fold (update op =) (#2 modes)); (* protocol *) fun protocol_loop () = let val _ = (case Byte_Message.read_message in_stream of NONE => raise Protocol_Command.STOP 0 | SOME [] => Output.system_message "Isabelle process: no input" - | SOME (name :: args) => Protocol_Command.run name args) + | SOME (name :: args) => Protocol_Command.run (Bytes.content name) args) handle exn => if Protocol_Command.is_protocol_exn exn then Exn.reraise exn else (Runtime.exn_system_message exn handle crash => recover crash); in protocol_loop () end; fun protocol () = (message Markup.initN [] [[XML.Text (Session.welcome ())]]; ml_statistics (); protocol_loop ()); val result = Exn.capture (message_context protocol) (); (* shutdown *) val _ = Future.shutdown (); val _ = Execution.reset (); val _ = Message_Channel.shutdown message_channel; val _ = BinIO.closeIn in_stream; val _ = BinIO.closeOut out_stream; val _ = Options.reset_default (); in (case result of Exn.Exn (Protocol_Command.STOP rc) => if rc = 0 then () else exit rc | _ => Exn.release result) end); end; (* init options *) fun init_options () = (ML_Print_Depth.set_print_depth (Options.default_int "ML_print_depth"); Multithreading.trace := Options.default_int "threads_trace"; Multithreading.max_threads_update (Options.default_int "threads"); Multithreading.parallel_proofs := Options.default_int "parallel_proofs"; if Options.default_bool "export_standard_proofs" then Proofterm.proofs := 2 else (); let val proofs = Options.default_int "record_proofs" in if proofs < 0 then () else Proofterm.proofs := proofs end; Printer.show_markup_default := false); fun init_options_interactive () = (init_options (); Multithreading.parallel_proofs := (if Options.default_int "parallel_proofs" > 0 then 3 else 0); Printer.show_markup_default := true); (* generic init *) fun init_modes modes = let val address = Options.default_string \<^system_option>\system_channel_address\; val password = Options.default_string \<^system_option>\system_channel_password\; in if address <> "" andalso password <> "" then init_protocol modes (address, password) else init_options () end; fun init () = init_modes (protocol_modes1, protocol_modes2); fun init_build () = init_modes ([], protocol_modes2); end; 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,186 +1,186 @@ (* Title: Pure/System/isabelle_system.ML Author: Makarius Isabelle system support. *) signature ISABELLE_SYSTEM = sig val bash_process: Bash.params -> 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 absolute_path: Path.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 val download_file: string -> Path.T -> unit val decode_base64: string -> string val encode_base64: string -> string val isabelle_id: unit -> string val isabelle_identifier: unit -> string option val isabelle_heading: unit -> string val isabelle_name: unit -> string val identification: unit -> string end; structure Isabelle_System: ISABELLE_SYSTEM = struct (* bash *) val absolute_path = Path.implode o File.absolute_path; fun bash_process params = let val {script, input, cwd, putenv, redirect, timeout, description} = Bash.dest_params params; val run = [Bash.server_run, script, input, let open XML.Encode in YXML.string_of_body (option (string o absolute_path) cwd) end, let open XML.Encode in YXML.string_of_body o list (pair string string) end (("ISABELLE_TMP", getenv "ISABELLE_TMP") :: putenv), Value.print_bool redirect, Value.print_real (Time.toReal timeout), description]; val address = Options.default_string \<^system_option>\bash_process_address\; val password = Options.default_string \<^system_option>\bash_process_password\; val _ = address = "" andalso raise Fail "Bad bash_process server address"; fun with_streams f = Socket_IO.with_streams' f address password; fun kill (SOME uuid) = - with_streams (fn s => Byte_Message.write_message (#2 s) [Bash.server_kill, uuid]) + with_streams (fn s => Byte_Message.write_message_string (#2 s) [Bash.server_kill, uuid]) | kill NONE = (); in Thread_Attributes.uninterruptible (fn restore_attributes => fn () => let fun err () = raise Fail "Malformed result from bash_process server"; fun loop maybe_uuid s = - (case restore_attributes Byte_Message.read_message (#1 s) of + (case restore_attributes Byte_Message.read_message_string (#1 s) of SOME (head :: args) => if head = Bash.server_uuid andalso length args = 1 then loop (SOME (hd args)) s else if head = Bash.server_interrupt andalso null args then raise Exn.Interrupt else if head = Bash.server_failure andalso length args = 1 then raise Fail (hd args) else if head = Bash.server_result andalso length args >= 4 then let val a :: b :: c :: d :: lines = args; 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 if rc = Process_Result.timeout_rc then raise Timeout.TIMEOUT elapsed else Process_Result.make {rc = rc, out_lines = out_lines, err_lines = err_lines, timing = {elapsed = elapsed, cpu = cpu, gc = Time.zeroTime}} end else err () | _ => err ()) handle exn => (kill maybe_uuid; Exn.reraise exn); - in with_streams (fn s => (Byte_Message.write_message (#2 s) run; loop NONE s)) end) () + in with_streams (fn s => (Byte_Message.write_message_string (#2 s) run; loop NONE s)) end) () end; val bash = Bash.script #> bash_process #> Process_Result.print #> Process_Result.rc; fun bash_output s = let val res = bash_process (Bash.script s); val _ = warning (Process_Result.err res); in (Process_Result.out res, Process_Result.rc res) end; (* bash functions *) fun bash_functions () = bash_process (Bash.script "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 *) fun scala_function name = ignore o Scala.function 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 = ignore (Scala.function "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 *) val download = Scala.function1 "download"; fun download_file url path = File.write path (download url); (* base64 *) val decode_base64 = Scala.function1 "decode_base64"; val encode_base64 = Scala.function1 "encode_base64"; (* Isabelle distribution identification *) fun isabelle_id () = Scala.function1 "isabelle_id" ""; fun isabelle_identifier () = try getenv_strict "ISABELLE_IDENTIFIER"; fun isabelle_heading () = (case isabelle_identifier () of NONE => "" | SOME version => " (" ^ version ^ ")"); fun isabelle_name () = getenv_strict "ISABELLE_NAME"; fun identification () = "Isabelle" ^ (case try isabelle_id () of SOME id => "/" ^ id | NONE => "") ^ isabelle_heading (); end; diff --git a/src/Pure/System/scala.ML b/src/Pure/System/scala.ML --- a/src/Pure/System/scala.ML +++ b/src/Pure/System/scala.ML @@ -1,69 +1,75 @@ (* Title: Pure/System/scala.ML Author: Makarius Invoke Scala functions from the ML runtime. *) signature SCALA = sig exception Null + val function_bytes: string -> Bytes.T list -> Bytes.T list + val function1_bytes: string -> Bytes.T -> Bytes.T val function: string -> string list -> string list val function1: string -> string -> string end; structure Scala: SCALA = struct exception Null; local val new_id = string_of_int o Counter.make (); val results = - Synchronized.var "Scala.results" (Symtab.empty: string list Exn.result Symtab.table); + Synchronized.var "Scala.results" (Symtab.empty: Bytes.T list Exn.result Symtab.table); val _ = - Protocol_Command.define "Scala.result" - (fn id :: args => + Protocol_Command.define_bytes "Scala.result" + (fn id :: tag :: rest => let val result = - (case args of - ["0"] => Exn.Exn Null - | "1" :: rest => Exn.Res rest - | ["2", msg] => Exn.Exn (ERROR msg) - | ["3", msg] => Exn.Exn (Fail msg) - | ["4"] => Exn.Exn Exn.Interrupt + (case (Bytes.content tag, rest) of + ("0", []) => Exn.Exn Null + | ("1", _) => Exn.Res rest + | ("2", [msg]) => Exn.Exn (ERROR (Bytes.content msg)) + | ("3", [msg]) => Exn.Exn (Fail (Bytes.content msg)) + | ("4", []) => Exn.Exn Exn.Interrupt | _ => raise Fail "Malformed Scala.result"); - in Synchronized.change results (Symtab.map_entry id (K result)) end); + in Synchronized.change results (Symtab.map_entry (Bytes.content id) (K result)) end); in -fun function name args = +fun function_bytes name args = Thread_Attributes.uninterruptible (fn restore_attributes => fn () => let val id = new_id (); fun invoke () = (Synchronized.change results (Symtab.update (id, Exn.Exn Match)); - Output.protocol_message (Markup.invoke_scala name id) (map (single o XML.Text) args)); + Output.protocol_message (Markup.invoke_scala name id) (map Bytes.contents_blob args)); fun cancel () = (Synchronized.change results (Symtab.delete_safe id); Output.protocol_message (Markup.cancel_scala id) []); fun await_result () = Synchronized.guarded_access results (fn tab => (case Symtab.lookup tab id of SOME (Exn.Exn Match) => NONE | SOME result => SOME (result, Symtab.delete id tab) | NONE => SOME (Exn.Exn Exn.Interrupt, tab))); in invoke (); Exn.release (restore_attributes await_result ()) handle exn => (if Exn.is_interrupt exn then cancel () else (); Exn.reraise exn) end) (); +val function1_bytes = singleton o function_bytes; + +fun function name = map Bytes.string #> function_bytes name #> map Bytes.content; + val function1 = singleton o function; end; end; diff --git a/src/Pure/library.ML b/src/Pure/library.ML --- a/src/Pure/library.ML +++ b/src/Pure/library.ML @@ -1,1106 +1,1110 @@ (* 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 build: ('a list -> 'a list) -> 'a list val build_rev: ('a list -> 'a list) -> 'a list 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 member_string: string -> string -> bool + val last_string: string -> string option 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 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 pointer_eq_ord: ('a * 'a -> order) -> 'a * 'a -> order val bool_ord: bool ord val int_ord: int ord val string_ord: string ord val size_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 length_ord: '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 build (f: 'a list -> 'a list) = f []; fun build_rev f = build f |> rev; 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 member_string str s = exists_string (fn s' => s = s') str; +fun last_string "" = NONE + | last_string s = SOME (str (String.sub (s, size s - 1))); + 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"; 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 pointer_eq_ord ord (x, y) = if pointer_eq (x, y) then EQUAL else ord (x, y); fun bool_ord (false, true) = LESS | bool_ord (true, false) = GREATER | bool_ord _ = EQUAL; val int_ord = Int.compare; val string_ord = String.compare; val size_ord = int_ord o apply2 size; val fast_string_ord = pointer_eq_ord (size_ord ||| string_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 length_ord (xs, ys) = int_ord (length xs, length ys); fun list_ord elem_ord = length_ord ||| dict_ord elem_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;