From a5c8335f575663bfc52bd1f90f31c8586ebc6ffd Mon Sep 17 00:00:00 2001 From: "Brian G. Milnes" Date: Fri, 1 Nov 2024 13:20:03 -0700 Subject: [PATCH] OCaml Unix fully wrapped. PR next. --- ocaml/fstar-lib/FStar_In_Channel.ml | 99 ++ ocaml/fstar-lib/FStar_In_Channel.mli | 50 + ocaml/fstar-lib/FStar_Out_Channel.ml | 94 ++ ocaml/fstar-lib/FStar_Out_Channel.mli | 63 + ocaml/fstar-lib/FStar_Unix.ml | 1035 +++++++++++++++++ ocaml/fstar-lib/FStar_Unix.mli | 571 +++++++++ ocaml/fstar-lib/FStar_Wrap_OCaml.ml | 99 ++ ocaml/fstar-lib/FStar_Wrap_OCaml.mli | 106 ++ .../generated/FStar_Class_Printable.ml | 19 +- .../generated/FStar_Class_Printable_Unix.ml | 964 +++++++++++++++ ocaml/fstar-lib/generated/FStar_FDString.ml | 36 + ulib/FStar.Class.Printable.Unix.fst | 563 +++++++++ ulib/FStar.Class.Printable.fst | 42 +- ulib/FStar.FDString.fst | 54 + ulib/FStar.FDString.fsti | 45 + ulib/FStar.In_Channel.fsti | 53 + ulib/FStar.Out_Channel.fsti | 59 + ulib/FStar.Unix.fsti | 494 ++++++++ 18 files changed, 4432 insertions(+), 14 deletions(-) create mode 100644 ocaml/fstar-lib/FStar_In_Channel.ml create mode 100644 ocaml/fstar-lib/FStar_In_Channel.mli create mode 100644 ocaml/fstar-lib/FStar_Out_Channel.ml create mode 100644 ocaml/fstar-lib/FStar_Out_Channel.mli create mode 100644 ocaml/fstar-lib/FStar_Unix.ml create mode 100644 ocaml/fstar-lib/FStar_Unix.mli create mode 100644 ocaml/fstar-lib/FStar_Wrap_OCaml.ml create mode 100644 ocaml/fstar-lib/FStar_Wrap_OCaml.mli create mode 100644 ocaml/fstar-lib/generated/FStar_Class_Printable_Unix.ml create mode 100644 ocaml/fstar-lib/generated/FStar_FDString.ml create mode 100644 ulib/FStar.Class.Printable.Unix.fst create mode 100644 ulib/FStar.FDString.fst create mode 100644 ulib/FStar.FDString.fsti create mode 100644 ulib/FStar.In_Channel.fsti create mode 100644 ulib/FStar.Out_Channel.fsti create mode 100644 ulib/FStar.Unix.fsti diff --git a/ocaml/fstar-lib/FStar_In_Channel.ml b/ocaml/fstar-lib/FStar_In_Channel.ml new file mode 100644 index 00000000000..fbe69b06d0a --- /dev/null +++ b/ocaml/fstar-lib/FStar_In_Channel.ml @@ -0,0 +1,99 @@ +(* + Copyright 2024 Microsoft Research + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. + + Authors: Brian G. Milnes +*) + +open In_channel +type t = In_channel.t + +(* + As In_channel.t are the subtypes here: + of_t maps In_channel t to t - used on the outputs + to_t maps t to In_channel.t - used on the inputs +*) + +let of_char c : FStar_Char.char = FStar_Char.char_of_u32 (Stdint.Uint32.of_int (Char.code c)) +let to_char c : char = Char.chr (Z.to_int (FStar_Char.int_of_char c)) + +type open_flag = | Open_rdonly | Open_wronly | Open_append | Open_creat | Open_trunc + | Open_excl | Open_binary | Open_text | Open_nonblock + +let to_open_flag (o : open_flag) = + match o with + | Open_rdonly -> In_channel.Open_rdonly + | Open_wronly -> In_channel.Open_wronly + | Open_append -> In_channel.Open_append + | Open_creat -> In_channel.Open_creat + | Open_trunc -> In_channel.Open_trunc + | Open_excl -> In_channel.Open_excl + | Open_binary -> In_channel.Open_binary + | Open_text -> In_channel.Open_text + | Open_nonblock -> In_channel.Open_nonblock + +let of_open_flag (o: In_channel.open_flag) = + match o with + | In_channel.Open_rdonly -> Open_rdonly + | In_channel.Open_wronly -> Open_wronly + | In_channel.Open_append -> Open_append + | In_channel.Open_creat -> Open_creat + | In_channel.Open_trunc -> Open_trunc + | In_channel.Open_excl -> Open_excl + | In_channel.Open_binary -> Open_binary + | In_channel.Open_text -> Open_text + | In_channel.Open_nonblock -> Open_nonblock + +let of_list_open_flag lof = List.map of_open_flag lof +let to_list_open_flag lof = List.map to_open_flag lof + +let stdin = In_channel.stdin +let open_bin = In_channel.open_bin +let open_text = In_channel.open_text +let with_open_bin = In_channel.with_open_bin +let with_open_text = In_channel.with_open_text + +let open_gen ofl i s = In_channel.open_gen (to_list_open_flag ofl) i s +let with_open_gen ofl i s fn = + In_channel.with_open_gen (to_list_open_flag ofl) i s fn + +let close = In_channel.close +let close_noerr = In_channel.close_noerr +let input_char t = + match In_channel.input_char t with + | None -> None + | Some c -> Some (of_char c) + +let input_byte = In_channel.input_byte +let input_line = In_channel.input_line +let really_input_string = In_channel.really_input_string +let input_all = In_channel.input_all + +let input t (start: Z.t) (len : Z.t) : Z.t * FStar_Bytes.bytes = + let len' = Z.to_int len in + let start' = Z.to_int start in + let bs' = Bytes.create len' in + let read = In_channel.input t bs' start' len' in + (Z.of_int read, Bytes.to_string bs') + +(* unit option here is kinda silly, it could be a bool. *) +let really_input t pos len : (unit option * FStar_Bytes.bytes) = + let bs = Bytes.create len in + let read = In_channel.really_input t bs pos len in + (read, Bytes.to_string bs) + +let seek = In_channel.seek +let pos = In_channel.pos +let length = In_channel.length +let set_binary_mode = In_channel.set_binary_mode diff --git a/ocaml/fstar-lib/FStar_In_Channel.mli b/ocaml/fstar-lib/FStar_In_Channel.mli new file mode 100644 index 00000000000..83a08df6dd1 --- /dev/null +++ b/ocaml/fstar-lib/FStar_In_Channel.mli @@ -0,0 +1,50 @@ +(* + Copyright 2024 Microsoft Research + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. + + Authors: Brian G. Milnes +*) + +(* OCaml Input channels 4.14.0 *) + +type t = In_channel.t +type open_flag = | Open_rdonly | Open_wronly | Open_append | Open_creat | Open_trunc + | Open_excl | Open_binary | Open_text | Open_nonblock + +val stdin : t +val open_bin : string -> t +val open_text : string -> t +val open_gen : open_flag list -> int -> string -> t +val with_open_bin : string -> (t -> 'a) -> 'a +val with_open_text : string -> (t -> 'a) -> 'a +val with_open_gen : open_flag list -> int -> string -> (t -> 'a) -> 'a +val seek : t -> int64 -> unit +val pos : t -> int64 +val length : t -> int64 +val close : t -> unit +val close_noerr : t -> unit +val input_char : t -> FStar_Char.char option +val input_byte : t -> int option +val input_line : t -> string option + +(* This type is modified as we don't take back mutated data from OCaml. + We could put in an input buffer but did not do that. + F* translates int into Z.t (unfortunately) but not intXs. +*) +val input : t -> Z.t -> Z.t -> (Z.t * FStar_Bytes.bytes) +val really_input : t -> int -> int -> (unit option * FStar_Bytes.bytes) +val really_input_string : t -> int -> string option +val input_all : t -> string +val set_binary_mode : t -> bool -> unit + diff --git a/ocaml/fstar-lib/FStar_Out_Channel.ml b/ocaml/fstar-lib/FStar_Out_Channel.ml new file mode 100644 index 00000000000..8b219c7cbfe --- /dev/null +++ b/ocaml/fstar-lib/FStar_Out_Channel.ml @@ -0,0 +1,94 @@ +(* + Copyright 2024 Microsoft Research + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. + + Authors: Brian G. Milnes +*) + +open Out_channel +type t = out_channel +open FStar_Wrap_OCaml + +(* + As Out_channel.t are the subtypes here: + of_t maps Out_channel t to t - used on the outputs + to_t maps t to Out_channel.t - used on the inputs +*) + +type open_flag = Stdlib.open_flag = + | Open_rdonly | Open_wronly | Open_append | Open_creat + | Open_trunc | Open_excl | Open_binary | Open_text + | Open_nonblock + +let stdout = Out_channel.stdout +let stderr = Out_channel.stderr + +let open_bin = open_bin +let open_text = open_text + +let open_gen fl perm s = + let perm' = Z.to_int perm in + open_gen fl perm' s + +let with_open_gen fl perm s fn = + let perm' = Z.to_int perm in + with_open_gen fl perm' s fn + +let with_open_bin : string -> (t -> 'a) -> 'a = with_open_bin +let with_open_text : string -> (t -> 'a) -> 'a = with_open_text + +let close : t -> unit = close +let close_noerr : t -> unit = close_noerr +let output_char : t -> Z.t -> unit = + wrapIawbOc output_char (fun z -> (Char.chr (Z.to_int z))) + +let output_byte t i = + let i' = Z.to_int i in + output_byte t i' + +let output_string : t -> string -> unit = output_string + +let output_bytes t bs = + output_bytes t (Bytes.of_string bs) + +let output t bs pos len = + let pos' = Z.to_int pos in + let len' = Z.to_int len in + let bs' = Bytes.of_string bs in + output t bs' pos' len' + +let output_substring t s pos len = + let pos' = Z.to_int pos in + let len' = Z.to_int len in + output_substring t s pos' len' + +(* No big arrays in F*. + let output_bigarray : + t -> (_, Bigarray.int8_unsigned_elt, Bigarray.c_layout) Bigarray.Array1.t -> + int -> int -> unit +*) + +let flush : t -> unit = flush +let flush_all : unit -> unit = flush_all +let seek : t -> int64 -> unit = seek +let pos : t -> int64 = pos +let length : t -> int64 = length + +let set_binary_mode : t -> bool -> unit = set_binary_mode +let set_buffered : t -> bool -> unit = set_buffered +let is_buffered : t -> bool = is_buffered + +(* Are not in this revision of OCaml. *) +(* let is_binary_mode : t -> bool = Out_channel.is_binary_mode *) +(* let isatty : t -> bool = isatty *) diff --git a/ocaml/fstar-lib/FStar_Out_Channel.mli b/ocaml/fstar-lib/FStar_Out_Channel.mli new file mode 100644 index 00000000000..eebcc2b94b0 --- /dev/null +++ b/ocaml/fstar-lib/FStar_Out_Channel.mli @@ -0,0 +1,63 @@ +(* + Copyright 2024 Microsoft Research + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. + + Authors: Brian G. Milnes +*) + +(* OCaml Input channels 4.14.0 *) +open Out_channel +type t = out_channel + +type open_flag = Stdlib.open_flag = + | Open_rdonly | Open_wronly | Open_append | Open_creat + | Open_trunc | Open_excl | Open_binary | Open_text + | Open_nonblock + +val stdout : t +val stderr : t +val open_bin : string -> t +val open_text : string -> t +val with_open_bin : string -> (t -> 'a) -> 'a +val with_open_text : string -> (t -> 'a) -> 'a +val open_gen : open_flag list -> Z.t -> string -> t +val with_open_gen : open_flag list -> Z.t -> string -> (t -> 'a) -> 'a +val close : t -> unit +val close_noerr : t -> unit +val output_char : t -> Z.t -> unit +val output_byte : t -> Z.t -> unit +val output_string : t -> string -> unit +val output_bytes : t -> FStar_Bytes.bytes -> unit +val output : t -> FStar_Bytes.bytes -> Z.t -> Z.t -> unit +val output_substring : t -> string -> Z.t -> Z.t -> unit + +(* +val output_bigarray : + t -> (_, Bigarray.int8_unsigned_elt, Bigarray.c_layout) Bigarray.Array1.t -> + int -> int -> unit +*) + +val flush : t -> unit +val flush_all : unit -> unit +val seek : t -> int64 -> unit +val pos : t -> int64 +val length : t -> int64 +val set_binary_mode : t -> bool -> unit +val set_buffered : t -> bool -> unit +val is_buffered : t -> bool + +(* Not in this OCaml revision. +val is_binary_mode : t -> bool +val isatty : t -> bool +*) diff --git a/ocaml/fstar-lib/FStar_Unix.ml b/ocaml/fstar-lib/FStar_Unix.ml new file mode 100644 index 00000000000..8fc634b1b13 --- /dev/null +++ b/ocaml/fstar-lib/FStar_Unix.ml @@ -0,0 +1,1035 @@ +(* + Copyright 2024 Microsoft Research + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. + + Authors: Brian G. Milnes +*) + +(* + There is a choice that this could written with fewer wrappers by curring more, + instead of the wrapI...O... pattern functions. + There should be a way to get much more sharing with just a few combinators. + id \o zin \o zout ... that sort of thing. + But then you'll be debugging each all about twice as much. + 86 wrap calls, 49 reuses in those, not too bad this way. + Probably just about as unreadable. + 80 lines of ml, 86 lines of mli. + Plus the z in some of the wrappers certainly shortens the lines. +*) + +open Unix +open Z +open FStar_Wrap_OCaml + +(* + As Unix.t are the subtypes here: + of_t maps Unix.t to t - used on the outputs + to_t maps t to Unix.t - used on the inputs + *) + +type error = + E2BIG + | EACCES + | EAGAIN + | EBADF + | EBUSY + | ECHILD + | EDEADLK + | EDOM + | EEXIST + | EFAULT + | EFBIG + | EINTR + | EINVAL + | EIO + | EISDIR + | EMFILE + | EMLINK + | ENAMETOOLONG + | ENFILE + | ENODEV + | ENOENT + | ENOEXEC + | ENOLCK + | ENOMEM + | ENOSPC + | ENOSYS + | ENOTDIR + | ENOTEMPTY + | ENOTTY + | ENXIO + | EPERM + | EPIPE + | ERANGE + | EROFS + | ESPIPE + | ESRCH + | EXDEV + | EWOULDBLOCK + | EINPROGRESS + | EALREADY + | ENOTSOCK + | EDESTADDRREQ + | EMSGSIZE + | EPROTOTYPE + | ENOPROTOOPT + | EPROTONOSUPPORT + | ESOCKTNOSUPPORT + | EOPNOTSUPP + | EPFNOSUPPORT + | EAFNOSUPPORT + | EADDRINUSE + | EADDRNOTAVAIL + | ENETDOWN + | ENETUNREACH + | ENETRESET + | ECONNABORTED + | ECONNRESET + | ENOBUFS + | EISCONN + | ENOTCONN + | ESHUTDOWN + | ETOOMANYREFS + | ETIMEDOUT + | ECONNREFUSED + | EHOSTDOWN + | EHOSTUNREACH + | ELOOP + | EOVERFLOW + | EUNKNOWNERR of Z.t + +let to_error (e: error) = + match e with + | E2BIG -> Unix.E2BIG + | EACCES -> Unix.EACCES + | EAGAIN -> Unix.EAGAIN + | EBADF -> Unix.EBADF + | EBUSY -> Unix.EBUSY + | ECHILD -> Unix.ECHILD + | EDEADLK -> Unix.EDEADLK + | EDOM -> Unix.EDOM + | EEXIST -> Unix.EEXIST + | EFAULT -> Unix.EFAULT + | EFBIG -> Unix.EFBIG + | EINTR -> Unix.EINTR + | EINVAL -> Unix.EINVAL + | EIO -> Unix.EIO + | EISDIR -> Unix.EISDIR + | EMFILE -> Unix.EMFILE + | EMLINK -> Unix.EMLINK + | ENAMETOOLONG -> Unix.ENAMETOOLONG + | ENFILE -> Unix.ENFILE + | ENODEV -> Unix.ENODEV + | ENOENT -> Unix.ENOENT + | ENOEXEC -> Unix.ENOEXEC + | ENOLCK -> Unix.ENOLCK + | ENOMEM -> Unix.ENOMEM + | ENOSPC -> Unix.ENOSPC + | ENOSYS -> Unix.ENOSYS + | ENOTDIR -> Unix.ENOTDIR + | ENOTEMPTY -> Unix.ENOTEMPTY + | ENOTTY -> Unix.ENOTTY + | ENXIO -> Unix.ENXIO + | EPERM -> Unix.EPERM + | EPIPE -> Unix.EPIPE + | ERANGE -> Unix.ERANGE + | EROFS -> Unix.EROFS + | ESPIPE -> Unix.ESPIPE + | ESRCH -> Unix.ESRCH + | EXDEV -> Unix.EXDEV + | EWOULDBLOCK -> Unix.EWOULDBLOCK + | EINPROGRESS -> Unix.EINPROGRESS + | EALREADY -> Unix.EALREADY + | ENOTSOCK -> Unix.ENOTSOCK + | EDESTADDRREQ -> Unix.EDESTADDRREQ + | EMSGSIZE -> Unix.EMSGSIZE + | EPROTOTYPE -> Unix.EPROTOTYPE + | ENOPROTOOPT -> Unix.ENOPROTOOPT + | EPROTONOSUPPORT -> Unix.EPROTONOSUPPORT + | ESOCKTNOSUPPORT -> Unix.ESOCKTNOSUPPORT + | EOPNOTSUPP -> Unix.EOPNOTSUPP + | EPFNOSUPPORT -> Unix.EPFNOSUPPORT + | EAFNOSUPPORT -> Unix.EAFNOSUPPORT + | EADDRINUSE -> Unix.EADDRINUSE + | EADDRNOTAVAIL -> Unix.EADDRNOTAVAIL + | ENETDOWN -> Unix.ENETDOWN + | ENETUNREACH -> Unix.ENETUNREACH + | ENETRESET -> Unix.ENETRESET + | ECONNABORTED -> Unix.ECONNABORTED + | ECONNRESET -> Unix.ECONNRESET + | ENOBUFS -> Unix.ENOBUFS + | EISCONN -> Unix.EISCONN + | ENOTCONN -> Unix.ENOTCONN + | ESHUTDOWN -> Unix.ESHUTDOWN + | ETOOMANYREFS -> Unix.ETOOMANYREFS + | ETIMEDOUT -> Unix.ETIMEDOUT + | ECONNREFUSED -> Unix.ECONNREFUSED + | EHOSTDOWN -> Unix.EHOSTDOWN + | EHOSTUNREACH -> Unix.EHOSTUNREACH + | ELOOP -> Unix.ELOOP + | EOVERFLOW -> Unix.EOVERFLOW + | EUNKNOWNERR i -> Unix.EUNKNOWNERR (Z.to_int i) + +let of_error (e: Unix.error) = + match e with + | Unix.E2BIG -> E2BIG + | Unix.EACCES -> EACCES + | Unix.EAGAIN -> EAGAIN + | Unix.EBADF -> EBADF + | Unix.EBUSY -> EBUSY + | Unix.ECHILD -> ECHILD + | Unix.EDEADLK -> EDEADLK + | Unix.EDOM -> EDOM + | Unix.EEXIST -> EEXIST + | Unix.EFAULT -> EFAULT + | Unix.EFBIG -> EFBIG + | Unix.EINTR -> EINTR + | Unix.EINVAL -> EINVAL + | Unix.EIO -> EIO + | Unix.EISDIR -> EISDIR + | Unix.EMFILE -> EMFILE + | Unix.EMLINK -> EMLINK + | Unix.ENAMETOOLONG -> ENAMETOOLONG + | Unix.ENFILE -> ENFILE + | Unix.ENODEV -> ENODEV + | Unix.ENOENT -> ENOENT + | Unix.ENOEXEC -> ENOEXEC + | Unix.ENOLCK -> ENOLCK + | Unix.ENOMEM -> ENOMEM + | Unix.ENOSPC -> ENOSPC + | Unix.ENOSYS -> ENOSYS + | Unix.ENOTDIR -> ENOTDIR + | Unix.ENOTEMPTY -> ENOTEMPTY + | Unix.ENOTTY -> ENOTTY + | Unix.ENXIO -> ENXIO + | Unix.EPERM -> EPERM + | Unix.EPIPE -> EPIPE + | Unix.ERANGE -> ERANGE + | Unix.EROFS -> EROFS + | Unix.ESPIPE -> ESPIPE + | Unix.ESRCH -> ESRCH + | Unix.EXDEV -> EXDEV + | Unix.EWOULDBLOCK -> EWOULDBLOCK + | Unix.EINPROGRESS -> EINPROGRESS + | Unix.EALREADY -> EALREADY + | Unix.ENOTSOCK -> ENOTSOCK + | Unix.EDESTADDRREQ -> EDESTADDRREQ + | Unix.EMSGSIZE -> EMSGSIZE + | Unix.EPROTOTYPE -> EPROTOTYPE + | Unix.ENOPROTOOPT -> ENOPROTOOPT + | Unix.EPROTONOSUPPORT -> EPROTONOSUPPORT + | Unix.ESOCKTNOSUPPORT -> ESOCKTNOSUPPORT + | Unix.EOPNOTSUPP -> EOPNOTSUPP + | Unix.EPFNOSUPPORT -> EPFNOSUPPORT + | Unix.EAFNOSUPPORT -> EAFNOSUPPORT + | Unix.EADDRINUSE -> EADDRINUSE + | Unix.EADDRNOTAVAIL -> EADDRNOTAVAIL + | Unix.ENETDOWN -> ENETDOWN + | Unix.ENETUNREACH -> ENETUNREACH + | Unix.ENETRESET -> ENETRESET + | Unix.ECONNABORTED -> ECONNABORTED + | Unix.ECONNRESET -> ECONNRESET + | Unix.ENOBUFS -> ENOBUFS + | Unix.EISCONN -> EISCONN + | Unix.ENOTCONN -> ENOTCONN + | Unix.ESHUTDOWN -> ESHUTDOWN + | Unix.ETOOMANYREFS -> ETOOMANYREFS + | Unix.ETIMEDOUT -> ETIMEDOUT + | Unix.ECONNREFUSED -> ECONNREFUSED + | Unix.EHOSTDOWN -> EHOSTDOWN + | Unix.EHOSTUNREACH -> EHOSTUNREACH + | Unix.ELOOP -> ELOOP + | Unix.EOVERFLOW -> EOVERFLOW + | Unix.EUNKNOWNERR i -> EUNKNOWNERR (Z.of_int i) + +exception Unix_error of error * string * string +let error_message : error -> string = wrapIwaOb error_message to_error +let handle_unix_error : ('a -> 'b) -> 'a -> 'b = handle_unix_error +let environment : unit -> string array = environment +let unsafe_environment : unit -> string array = unsafe_environment +let getenv : string -> string = getenv +let unsafe_getenv : string -> string = unsafe_getenv +let putenv : string -> string -> unit = putenv + +type process_status = + WEXITED of Z.t + | WSIGNALED of Z.t + | WSTOPPED of Z.t + +let of_process_status (e: Unix.process_status) = + match e with + | Unix.WEXITED i -> WEXITED (Z.of_int i) + | Unix.WSIGNALED i -> WSIGNALED (Z.of_int i) + | Unix.WSTOPPED i -> WSTOPPED (Z.of_int i) + +let to_process_status (e: process_status) = + match e with + | WEXITED i -> Unix.WEXITED (Z.to_int i) + | WSIGNALED i -> Unix.WSIGNALED (Z.to_int i) + | WSTOPPED i -> Unix.WSTOPPED (Z.to_int i) + +type wait_flag = Unix.wait_flag = + WNOHANG | WUNTRACED + +let to_wait_flag wf = + match wf with + | WNOHANG -> Unix.WNOHANG + | WUNTRACED -> Unix.WUNTRACED + +let execv : string -> string array -> 'a = execv +let execve : string -> string array -> string array -> 'a = execve +let execvp : string -> string array -> 'a = execvp +let execvpe : string -> string array -> string array -> 'a = execvpe + +let fork : unit -> Z.t = wrapIaOz fork +let wait : unit -> Z.t * process_status = wrapIaOpzwb wait of_process_status +let waitpid : wait_flag list -> Z.t -> Z.t * process_status = + wrapILwazOpzwb waitpid to_wait_flag of_process_status + +let system : string -> process_status = wrapIaOwb system of_process_status + +let _exit : Z.t -> 'a = wrapIzOa _exit +let getpid : unit -> Z.t = wrapIaOz getpid +let getppid : unit -> Z.t = wrapIaOz getppid +let nice : Z.t -> Z.t = wrapIzOz nice + +type file_descr = Unix.file_descr + +(* Why are these not from the channels? +let stdout = Out_channel.stdout +let stderr = Out_channel.stderr +let stdin = In_channel.stdin + *) + +let stdout = Unix.stdout +let stderr = Unix.stderr +let stdin = Unix.stdin + +type open_flag = Unix.open_flag = + O_RDONLY | O_WRONLY | O_RDWR | O_NONBLOCK | O_APPEND | O_CREAT | O_TRUNC + | O_EXCL | O_NOCTTY | O_DSYNC | O_SYNC | O_RSYNC + | O_SHARE_DELETE | O_CLOEXEC | O_KEEPEXEC + +let to_open_flag f = + match f with + | O_RDONLY -> Unix.O_RDONLY + | O_WRONLY -> Unix.O_WRONLY + | O_RDWR -> Unix.O_RDWR + | O_NONBLOCK -> Unix.O_NONBLOCK + | O_APPEND -> Unix.O_APPEND + | O_CREAT -> Unix.O_CREAT + | O_TRUNC -> Unix.O_TRUNC + | O_EXCL -> Unix.O_EXCL + | O_NOCTTY -> Unix.O_NOCTTY + | O_DSYNC -> Unix.O_DSYNC + | O_SYNC -> Unix.O_SYNC + | O_RSYNC -> Unix.O_RSYNC + | O_SHARE_DELETE -> Unix.O_SHARE_DELETE + | O_CLOEXEC -> Unix.O_CLOEXEC + | O_KEEPEXEC -> Unix.O_KEEPEXEC + +let to_open_flag_list ofl = List.map to_open_flag ofl + +type file_perm = Z.t +let openfile : string -> open_flag list -> file_perm -> file_descr = + wrapIabwcOd openfile Z.to_int +let close : file_descr -> unit = close +let fsync : file_descr -> unit = fsync + + +let read : file_descr -> bytes -> Z.t -> Z.t -> Z.t = wrapIabzzOz read +let write : file_descr -> bytes -> Z.t -> Z.t -> Z.t = wrapIabzzOz write +let single_write : file_descr -> bytes -> Z.t -> Z.t -> Z.t = + wrapIabzzOz single_write +let write_substring : file_descr -> string -> Z.t -> Z.t -> Z.t = + wrapIabzzOz write_substring +let single_write_substring : file_descr -> string -> Z.t -> Z.t -> Z.t = + wrapIabzzOz single_write_substring + +let in_channel_of_descr : file_descr -> in_channel = in_channel_of_descr +let out_channel_of_descr : file_descr -> out_channel = out_channel_of_descr +let descr_of_in_channel : in_channel -> file_descr = descr_of_in_channel +let descr_of_out_channel : out_channel -> file_descr = descr_of_out_channel + +type seek_command = Unix.seek_command = + SEEK_SET + | SEEK_CUR + | SEEK_END + +let of_seek_command (sc : Unix.seek_command) = + match sc with + | Unix.SEEK_SET -> SEEK_SET + | Unix.SEEK_CUR -> SEEK_CUR + | Unix.SEEK_END -> SEEK_END + +let lseek : file_descr -> Z.t -> seek_command -> Z.t = wrapIazwbOz lseek of_seek_command + +let truncate : string -> Z.t -> unit = wrapIazOb truncate +let ftruncate : file_descr -> Z.t -> unit = wrapIazOb ftruncate + +type file_kind = Unix.file_kind = + S_REG | S_DIR | S_CHR | S_BLK | S_LNK | S_FIFO | S_SOCK + +type stats = + { st_dev : Z.t; + st_ino : Z.t; + st_kind : file_kind; + st_perm : Z.t; + st_nlink : Z.t; + st_uid : Z.t; + st_gid : Z.t; + st_rdev : Z.t; + st_size : Z.t; + st_atime : float; + st_mtime : float; + st_ctime : float; + } + +let of_stats (s : Unix.stats) = + { st_dev = Z.of_int s.st_dev; + st_ino = Z.of_int s.st_ino; + st_kind = s.st_kind; + st_perm = Z.of_int s.st_perm; + st_nlink = Z.of_int s.st_nlink; + st_uid = Z.of_int s.st_uid; + st_gid = Z.of_int s.st_gid; + st_rdev = Z.of_int s.st_rdev; + st_size = Z.of_int s.st_size; + st_atime = s.st_atime; + st_mtime = s.st_mtime; + st_ctime = s.st_ctime; + } + +let stat : string -> stats = wrapIaOwb stat of_stats +let lstat : string -> stats = wrapIaOwb lstat of_stats +let fstat : file_descr -> stats = wrapIaOwb fstat of_stats +let isatty : file_descr -> bool = isatty +let unlink : string -> unit = unlink +let rename : string -> string -> unit = rename +let link : string -> string -> unit = link +let realpath : string -> string = realpath + +type access_permission = Unix.access_permission = + R_OK | W_OK | X_OK | F_OK + +let chmod : string -> file_perm -> unit = wrapIawbOc chmod Z.to_int +let fchmod : file_descr -> file_perm -> unit = wrapIawbOc fchmod Z.to_int +let chown : string -> Z.t -> Z.t -> unit = wrapIazzOb chown +let fchown : file_descr -> Z.t -> Z.t -> unit = wrapIazzOb fchown +let umask : file_perm -> file_perm = wrapIwaOwb umask Z.to_int Z.of_int +let access : string -> access_permission list -> unit = access +let dup : file_descr -> file_descr = dup +let dup2 : file_descr -> file_descr -> unit = dup2 + +let set_nonblock : file_descr -> unit = set_nonblock +let clear_nonblock : file_descr -> unit = clear_nonblock +let set_close_on_exec : file_descr -> unit = set_close_on_exec +let clear_close_on_exec : file_descr -> unit = clear_close_on_exec +let mkdir : string -> file_perm -> unit = wrapIawbOc mkdir Z.to_int +let rmdir : string -> unit = rmdir +let chdir : string -> unit = chdir +let getcwd : unit -> string = getcwd +let chroot : string -> unit = chroot + +type dir_handle = Unix.dir_handle + +let opendir : string -> dir_handle = opendir +let readdir : dir_handle -> string = readdir +let rewinddir : dir_handle -> unit = rewinddir +let closedir : dir_handle -> unit = closedir +let pipe : unit -> file_descr * file_descr = pipe +let mkfifo : string -> file_perm -> unit = wrapIawbOc mkfifo Z.to_int + +let create_process + : string -> string array -> file_descr -> file_descr -> file_descr -> Z.t = + wrapIabcdeOz create_process + +let create_process_env : string -> string array -> string array -> file_descr -> + file_descr -> file_descr -> Z.t = wrapIabcdefOz create_process_env + + +let open_process_in : string -> in_channel = open_process_in +let open_process_out : string -> out_channel = open_process_out +let open_process : string -> in_channel * out_channel = open_process + +let open_process_full : string -> string array -> in_channel * out_channel * in_channel = + open_process_full + +let open_process_args : string -> string array -> in_channel * out_channel = open_process_args +let open_process_args_in : string -> string array -> in_channel = open_process_args_in +let open_process_args_out : string -> string array -> out_channel = open_process_args_out +let open_process_args_full : string -> string array -> string array -> + in_channel * out_channel * in_channel = open_process_args_full +let process_in_pid : in_channel -> Z.t = wrapIaOz process_in_pid +let process_out_pid : out_channel -> Z.t = wrapIaOz process_out_pid +let process_pid : in_channel * out_channel -> Z.t = wrapIaOz process_pid +let process_full_pid : in_channel * out_channel * in_channel -> Z.t = + wrapIaOz process_full_pid + +let close_process_in : in_channel -> process_status = + wrapIaOwb close_process_in of_process_status +let close_process_out : out_channel -> process_status = + wrapIaOwb close_process_out of_process_status + +let close_process : in_channel * out_channel -> process_status = + wrapIaOwb close_process of_process_status + +let close_process_full : in_channel * out_channel * in_channel -> process_status = + wrapIaOwb close_process_full of_process_status + +let symlink : string -> string -> unit = symlink +let has_symlink : unit -> bool = has_symlink +let readlink : string -> string = readlink + +let select : file_descr list -> file_descr list -> file_descr list -> + float -> file_descr list * file_descr list * file_descr list = select + +type lock_command = Unix.lock_command = + F_ULOCK | F_LOCK | F_TLOCK | F_TEST | F_RLOCK | F_TRLOCK + +let lockf : file_descr -> lock_command -> Z.t -> unit = wrapIabzOc lockf +let kill : Z.t -> Z.t -> unit = wrapIzzOa kill + +type sigprocmask_command = Unix.sigprocmask_command = + SIG_SETMASK + | SIG_BLOCK + | SIG_UNBLOCK + +let to_sigprocmask_command spmc = + match spmc with + | SIG_SETMASK -> Unix.SIG_SETMASK + | SIG_BLOCK -> Unix.SIG_BLOCK + | SIG_UNBLOCK -> Unix.SIG_UNBLOCK + + +let sigprocmask : sigprocmask_command -> Z.t list -> Z.t list = + wrapIaLbOLwc sigprocmask Z.to_int Z.of_int + +let sigpending : unit -> Z.t list = wrapIaOLwb sigpending Z.of_int + +let sigsuspend : Z.t list -> unit = wrapILwaOb sigsuspend Z.to_int + +let pause : unit -> unit = pause + +(* Where is sigwait? +let sigwait : Z.t list -> Z.t = wrapILwaOb sigwait Z.to_int + *) + +type process_times = Unix.process_times = + { tms_utime : float; + tms_stime : float; + tms_cutime : float; + tms_cstime : float; + } + +let of_process_times (pt : Unix.process_times) : process_times = pt + +type tm = + { tm_sec : Z.t; + tm_min : Z.t; + tm_hour : Z.t; + tm_mday : Z.t; + tm_mon : Z.t; + tm_year : Z.t; + tm_wday : Z.t; + tm_yday : Z.t; + tm_isdst : bool; + } + +let to_tm (t : tm) : Unix.tm = + { tm_sec = Z.to_int t.tm_sec; + tm_min = Z.to_int t.tm_min; + tm_hour = Z.to_int t.tm_hour; + tm_mday = Z.to_int t.tm_mday; + tm_mon = Z.to_int t.tm_mon; + tm_year = Z.to_int t.tm_year; + tm_wday = Z.to_int t.tm_wday; + tm_yday = Z.to_int t.tm_yday; + tm_isdst = t.tm_isdst; + } + +let of_tm (t : Unix.tm) : tm = + { tm_sec = Z.of_int t.tm_sec; + tm_min = Z.of_int t.tm_min; + tm_hour = Z.of_int t.tm_hour; + tm_mday = Z.of_int t.tm_mday; + tm_mon = Z.of_int t.tm_mon; + tm_year = Z.of_int t.tm_year; + tm_wday = Z.of_int t.tm_wday; + tm_yday = Z.of_int t.tm_yday; + tm_isdst = t.tm_isdst; + } + +let time : unit -> float = time +let gettimeofday : unit -> float = gettimeofday +let gmtime : float -> tm = wrapIaOwb gmtime of_tm +let localtime : float -> tm = wrapIaOwb localtime of_tm +let mktime : tm -> float * tm = wrapIwaOpbwc mktime to_tm of_tm +let alarm : Z.t -> Z.t = wrapIzOz alarm +let sleep : Z.t -> unit = wrapIzOa sleep +let sleepf : float -> unit = sleepf +let times : unit -> process_times = times +let utimes : string -> float -> float -> unit = utimes + +type interval_timer = Unix.interval_timer = + ITIMER_REAL | ITIMER_VIRTUAL | ITIMER_PROF + +type interval_timer_status = Unix.interval_timer_status = + { it_interval : float; + it_value : float; + } + +let getitimer : interval_timer -> interval_timer_status = getitimer +let setitimer : interval_timer -> interval_timer_status -> interval_timer_status = setitimer +let getuid : unit -> Z.t = wrapIaOz getuid +let geteuid : unit -> Z.t = wrapIaOz geteuid +let setuid : Z.t -> unit = wrapIzOa setuid +let getgid : unit -> Z.t = wrapIaOz getgid +let getegid : unit -> Z.t = wrapIaOz getegid +let setgid : Z.t -> unit = wrapIzOa setgid +let getgroups : unit -> Z.t array = wrapIaOwA getgroups of_int +let setgroups : Z.t array -> unit = wrapIAaOb setgroups to_int + +let initgroups : string -> Z.t -> unit = wrapIazOb initgroups + +type passwd_entry = + { pw_name : string; + pw_passwd : string; + pw_uid : Z.t; + pw_gid : Z.t; + pw_gecos : string; + pw_dir : string; + pw_shell : string + } + +let of_passwd_entry (pwe : Unix.passwd_entry) : passwd_entry = + { pw_name = pwe.pw_name; + pw_passwd = pwe.pw_passwd; + pw_uid = Z.of_int pwe.pw_uid; + pw_gid = Z.of_int pwe.pw_gid; + pw_gecos = pwe.pw_gecos; + pw_dir = pwe.pw_dir; + pw_shell = pwe.pw_shell; + } + +type group_entry = + { gr_name : string; + gr_passwd : string; + gr_gid : Z.t; + gr_mem : string array + } + +let of_group_entry (ge : Unix.group_entry) : group_entry = + { gr_name = ge.gr_name; + gr_passwd = ge.gr_passwd; + gr_gid = Z.of_int ge.gr_gid; + gr_mem = ge.gr_mem; + } + +let getlogin : unit -> string = getlogin +let getpwnam : string -> passwd_entry = wrapIaOwb getpwnam of_passwd_entry +let getgrnam : string -> group_entry = wrapIaOwb getgrnam of_group_entry +let getpwuid : Z.t -> passwd_entry = wrapIazOwb getpwuid of_passwd_entry +let getgrgid : Z.t -> group_entry = wrapIazOwb getgrgid of_group_entry + +type inet_addr = Unix.inet_addr +let inet_addr_of_string : string -> inet_addr = inet_addr_of_string +let string_of_inet_addr : inet_addr -> string = string_of_inet_addr +let inet_addr_any : inet_addr = inet_addr_any +let inet_addr_loopback : inet_addr = inet_addr_loopback +let inet6_addr_any : inet_addr = inet6_addr_any +let inet6_addr_loopback : inet_addr = inet6_addr_loopback +let is_inet6_addr : inet_addr -> bool = is_inet6_addr + +type socket_domain = Unix.socket_domain = + PF_UNIX | PF_INET | PF_INET6 + +let of_socket_domain (sd: Unix.socket_domain) = + match sd with + | Unix.PF_UNIX -> PF_UNIX + | Unix.PF_INET -> PF_INET + | Unix.PF_INET6 -> PF_INET6 + +let to_socket_domain (sd: socket_domain) : Unix.socket_domain = + match sd with + | PF_UNIX -> Unix.PF_UNIX + | PF_INET -> Unix.PF_INET + | PF_INET6 -> Unix.PF_INET6 + +type socket_type = Unix.socket_type = + SOCK_STREAM | SOCK_DGRAM | SOCK_RAW | SOCK_SEQPACKET + +let of_socket_type (st: Unix.socket_type) = + match st with + | Unix.SOCK_STREAM -> SOCK_STREAM + | Unix.SOCK_DGRAM -> SOCK_DGRAM + | Unix.SOCK_RAW -> SOCK_RAW + | Unix.SOCK_SEQPACKET -> SOCK_SEQPACKET + +let to_socket_type (st: socket_type) : Unix.socket_type = + match st with + | SOCK_STREAM -> Unix.SOCK_STREAM + | SOCK_DGRAM -> Unix.SOCK_DGRAM + | SOCK_RAW -> Unix.SOCK_RAW + | SOCK_SEQPACKET -> Unix.SOCK_SEQPACKET + +type sockaddr = + ADDR_UNIX of string +| ADDR_INET of inet_addr * Z.t + +let of_sockaddr (sa : Unix.sockaddr) = + match sa with + | Unix.ADDR_UNIX s -> ADDR_UNIX s + | Unix.ADDR_INET (ia, i) -> ADDR_INET (ia, Z.of_int i) + +let to_sockaddr (sa : sockaddr) = + match sa with + | ADDR_UNIX s -> Unix.ADDR_UNIX s + | ADDR_INET (ia, i) -> Unix.ADDR_INET (ia, Z.to_int i) + + +let socket : socket_domain -> socket_type -> Z.t -> file_descr = + wrapIwawbwcOd socket to_socket_domain to_socket_type Z.to_int + +let domain_of_sockaddr : sockaddr -> socket_domain = + wrapIwaOwb domain_of_sockaddr to_sockaddr of_socket_domain + +let socketpair : socket_domain -> socket_type -> Z.t -> file_descr * file_descr = + wrapIwawbwcOd socketpair to_socket_domain to_socket_type Z.to_int + +let accept : file_descr -> file_descr * sockaddr = + wrapIaOpbwc accept of_sockaddr + +let bind : file_descr -> sockaddr -> unit = wrapIawbOc bind to_sockaddr + +let connect : file_descr -> sockaddr -> unit = wrapIawbOc connect to_sockaddr + +let listen : file_descr -> Z.t -> unit = wrapIazOb listen + +type shutdown_command = Unix.shutdown_command = + SHUTDOWN_RECEIVE | SHUTDOWN_SEND | SHUTDOWN_ALL + +let shutdown : file_descr -> shutdown_command -> unit = shutdown +let getsockname : file_descr -> sockaddr = wrapIaOwb getsockname of_sockaddr +let getpeername : file_descr -> sockaddr = wrapIaOwb getpeername of_sockaddr + +type msg_flag = Unix.msg_flag = + MSG_OOB | MSG_DONTROUTE | MSG_PEEK + +let recv : file_descr -> bytes -> Z.t -> Z.t -> msg_flag list -> Z.t = + wrapIabwcwdeOwf recv Z.to_int Z.to_int Z.of_int +let send : file_descr -> bytes -> Z.t -> Z.t -> msg_flag list -> Z.t = + wrapIabwcwdeOwf send Z.to_int Z.to_int Z.of_int +let send_substring : file_descr -> string -> Z.t -> Z.t -> msg_flag list -> Z.t = + wrapIabwcwdeOwf send_substring Z.to_int Z.to_int Z.of_int + +let sendto + : file_descr -> bytes -> Z.t -> Z.t -> msg_flag list -> sockaddr -> Z.t = + wrapIabwcwdewfOwg sendto Z.to_int Z.to_int to_sockaddr Z.of_int +let sendto_substring + : file_descr -> string -> Z.t -> Z.t -> msg_flag list -> sockaddr -> Z.t = + wrapIabwcwdewfOwg sendto_substring Z.to_int Z.to_int to_sockaddr Z.of_int + +let recvfrom : file_descr -> bytes -> Z.t -> Z.t -> msg_flag list -> Z.t * sockaddr = + wrapIabwcwdeOwNSwfwg recvfrom Z.to_int Z.to_int Z.of_int of_sockaddr + +type socket_bool_option = Unix.socket_bool_option = + SO_DEBUG | SO_BROADCAST | SO_REUSEADDR | SO_KEEPALIVE | SO_DONTROUTE + | SO_OOBINLINE | SO_ACCEPTCONN | TCP_NODELAY | IPV6_ONLY | SO_REUSEPORT + +type socket_int_option = Unix.socket_int_option = + SO_SNDBUF | SO_RCVBUF | SO_ERROR | SO_TYPE | SO_RCVLOWAT | SO_SNDLOWAT + +type socket_optint_option = Unix.socket_optint_option = + SO_LINGER +type socket_float_option = Unix.socket_float_option = + SO_RCVTIMEO | SO_SNDTIMEO + +let getsockopt : file_descr -> socket_bool_option -> bool = getsockopt +let setsockopt : file_descr -> socket_bool_option -> bool -> unit = setsockopt +let getsockopt_int : file_descr -> socket_int_option -> Z.t = + wrapIabOwc getsockopt_int Z.of_int +let setsockopt_int : file_descr -> socket_int_option -> Z.t -> unit = + wrapIabzOc setsockopt_int + +let getsockopt_optint : file_descr -> socket_optint_option -> Z.t option = + wrapIabOwNSc getsockopt_optint Z.of_int + +let setsockopt_optint : file_descr -> socket_optint_option -> Z.t option -> unit = + wrapIabwNScOd setsockopt_optint Z.to_int + +let getsockopt_float : file_descr -> socket_float_option -> float = getsockopt_float +let setsockopt_float : file_descr -> socket_float_option -> float -> unit = setsockopt_float +let getsockopt_error : file_descr -> error option = wrapIaOwNSb getsockopt_error of_error + +let open_connection : sockaddr -> in_channel * out_channel = + wrapIwaOb open_connection to_sockaddr +let shutdown_connection : in_channel -> unit = shutdown_connection +let establish_server : (in_channel -> out_channel -> unit) -> sockaddr -> unit = + wrapIawbOc establish_server to_sockaddr + +type host_entry = Unix.host_entry = + { h_name : string; + h_aliases : string array; + h_addrtype : socket_domain; + h_addr_list : inet_addr array + } + +type protocol_entry = (* Unix.protocol_entry = *) + { p_name : string; + p_aliases : string array; + p_proto : Z.t + } + +let of_protocol_entry (pe : Unix.protocol_entry) : protocol_entry = + { p_name = pe.p_name; + p_aliases = pe.p_aliases; + p_proto = Z.of_int pe.p_proto; + } + +type service_entry = + { s_name : string; + s_aliases : string array; + s_port : Z.t; + s_proto : string + } + +let of_service_entry (se: Unix.service_entry) = + { s_name = se.s_name; + s_aliases = se.s_aliases; + s_port = Z.of_int se.s_port; + s_proto = se.s_proto; + } + +let gethostname : unit -> string = wrapIaOb gethostname +let gethostbyname : string -> host_entry = gethostbyname +let gethostbyaddr : inet_addr -> host_entry = gethostbyaddr +let getprotobyname : string -> protocol_entry = + wrapIaOwb getprotobyname of_protocol_entry + +let getprotobynumber : Z.t -> protocol_entry = + wrapIwaOwb getprotobynumber Z.to_int of_protocol_entry +let getservbyname : string -> string -> service_entry = + wrapIabOwc getservbyname of_service_entry +let getservbyport : Z.t -> string -> service_entry = + wrapIwabOwc getservbyport Z.to_int of_service_entry + +type addr_info = + { ai_family : socket_domain; + ai_socktype : socket_type; + ai_protocol : Z.t; + ai_addr : sockaddr; + ai_canonname : string + } + +let of_addr_info (ai : Unix.addr_info) = + { ai_family = ai.ai_family; + ai_socktype = ai.ai_socktype; + ai_protocol = Z.of_int ai.ai_protocol; + ai_addr = of_sockaddr ai.ai_addr; + ai_canonname = ai.ai_canonname; + } + +type getaddrinfo_option = + AI_FAMILY of socket_domain + | AI_SOCKTYPE of socket_type + | AI_PROTOCOL of Z.t + | AI_NUMERICHOST + | AI_CANONNAME + | AI_PASSIVE + +let to_getaddrinfo_option (g : getaddrinfo_option) = + match g with + | AI_FAMILY sd -> Unix.AI_FAMILY sd + | AI_SOCKTYPE st -> Unix.AI_SOCKTYPE st + | AI_PROTOCOL z -> Unix.AI_PROTOCOL (Z.to_int z) + | AI_NUMERICHOST -> Unix.AI_NUMERICHOST + | AI_CANONNAME -> Unix.AI_CANONNAME + | AI_PASSIVE -> Unix.AI_PASSIVE + +let getaddrinfo: string -> string -> getaddrinfo_option list -> addr_info list = + wrapIabLwcOLwd getaddrinfo to_getaddrinfo_option of_addr_info + +type name_info = Unix.name_info = + { ni_hostname : string; + ni_service : string; + } + +type getnameinfo_option = Unix.getnameinfo_option = + NI_NOFQDN | NI_NUMERICHOST | NI_NAMEREQD | NI_NUMERICSERV | NI_DGRAM + +let getnameinfo : sockaddr -> getnameinfo_option list -> name_info = + wrapIwabOc getnameinfo to_sockaddr + +type terminal_io = + { + c_ignbrk : bool; + c_brkint : bool; + c_ignpar : bool; + c_parmrk : bool; + c_inpck : bool; + c_istrip : bool; + c_inlcr : bool; + c_igncr : bool; + c_icrnl : bool; + c_ixon : bool; + c_ixoff : bool; + + c_opost : bool; + + c_obaud : Z.t; + c_ibaud : Z.t; + c_csize : Z.t; + c_cstopb : Z.t; + c_cread : bool; + c_parenb : bool; + c_parodd : bool; + c_hupcl : bool; + c_clocal : bool; + + c_isig : bool; + c_icanon : bool; + c_noflsh : bool; + c_echo : bool; + c_echoe : bool; + c_echok : bool; + c_echonl : bool; + + c_vintr : int; + c_vquit : int; + c_verase : int; + c_vkill : int; + c_veof : int; + c_veol : int; + c_vmin : int; + c_vtime : int; + c_vstart : int; + c_vstop : int; + } + + +let of_terminal_io (tio : Unix.terminal_io) : terminal_io = + { + c_ignbrk = tio.c_ignbrk; + c_brkint = tio.c_brkint; + c_ignpar = tio.c_ignpar; + c_parmrk = tio.c_parmrk; + c_inpck = tio.c_inpck; + c_istrip = tio.c_istrip; + c_inlcr = tio.c_inlcr; + c_igncr = tio.c_igncr; + c_icrnl = tio.c_icrnl; + c_ixon = tio.c_ixon; + c_ixoff = tio.c_ixoff; + + c_opost = tio.c_opost; + + c_obaud = Z.of_int tio.c_obaud; + c_ibaud = Z.of_int tio.c_ibaud; + c_csize = Z.of_int tio.c_csize; + c_cstopb = Z.of_int tio.c_cstopb; + c_cread = tio.c_cread; + c_parenb = tio.c_parenb; + c_parodd = tio.c_parodd; + c_hupcl = tio.c_hupcl; + c_clocal = tio.c_clocal; + + c_isig = tio.c_isig; + c_icanon = tio.c_icanon; + c_noflsh = tio.c_noflsh; + c_echo = tio.c_echo; + c_echoe = tio.c_echoe; + c_echok = tio.c_echok; + c_echonl = tio.c_echonl; + + c_vintr = Char.code tio.c_vintr; + c_vquit = Char.code tio.c_vquit; + c_verase = Char.code tio.c_verase; + c_vkill = Char.code tio.c_vkill; + c_veof = Char.code tio.c_veof; + c_veol = Char.code tio.c_veol; + c_vmin = tio.c_vmin; + c_vtime = tio.c_vtime; + c_vstart = Char.code tio.c_vstart; + c_vstop = Char.code tio.c_vstop; + } + +let to_terminal_io (tio : terminal_io) : Unix.terminal_io = + { + c_ignbrk = tio.c_ignbrk; + c_brkint = tio.c_brkint; + c_ignpar = tio.c_ignpar; + c_parmrk = tio.c_parmrk; + c_inpck = tio.c_inpck; + c_istrip = tio.c_istrip; + c_inlcr = tio.c_inlcr; + c_igncr = tio.c_igncr; + c_icrnl = tio.c_icrnl; + c_ixon = tio.c_ixon; + c_ixoff = tio.c_ixoff; + + c_opost = tio.c_opost; + + c_obaud = Z.to_int tio.c_obaud; + c_ibaud = Z.to_int tio.c_ibaud; + c_csize = Z.to_int tio.c_csize; + c_cstopb = Z.to_int tio.c_cstopb; + c_cread = tio.c_cread; + c_parenb = tio.c_parenb; + c_parodd = tio.c_parodd; + c_hupcl = tio.c_hupcl; + c_clocal = tio.c_clocal; + + c_isig = tio.c_isig; + c_icanon = tio.c_icanon; + c_noflsh = tio.c_noflsh; + c_echo = tio.c_echo; + c_echoe = tio.c_echoe; + c_echok = tio.c_echok; + c_echonl = tio.c_echonl; + + c_vintr = Char.chr tio.c_vintr; + c_vquit = Char.chr tio.c_vquit; + c_verase = Char.chr tio.c_verase; + c_vkill = Char.chr tio.c_vkill; + c_veof = Char.chr tio.c_veof; + c_veol = Char.chr tio.c_veol; + c_vmin = tio.c_vmin; + c_vtime = tio.c_vtime; + c_vstart = Char.chr tio.c_vstart; + c_vstop = Char.chr tio.c_vstop; + } + +let tcgetattr : file_descr -> terminal_io = + wrapIaOwb tcgetattr of_terminal_io + +type setattr_when = Unix.setattr_when = + TCSANOW | TCSADRAIN | TCSAFLUSH + +let tcsetattr : file_descr -> setattr_when -> terminal_io -> unit = + wrapIabwcOd tcsetattr to_terminal_io + +let tcsendbreak : file_descr -> Z.t -> unit = wrapIazOb tcsendbreak +let tcdrain : file_descr -> unit = tcdrain + +type flush_queue = Unix.flush_queue = + TCIFLUSH | TCOFLUSH | TCIOFLUSH + +let tcflush : file_descr -> flush_queue -> unit = tcflush + +type flow_action = Unix.flow_action = + TCOOFF | TCOON | TCIOFF | TCION + +let tcflow : file_descr -> flow_action -> unit = tcflow +let setsid : unit -> Z.t = wrapIaOz setsid diff --git a/ocaml/fstar-lib/FStar_Unix.mli b/ocaml/fstar-lib/FStar_Unix.mli new file mode 100644 index 00000000000..3c491ef04d8 --- /dev/null +++ b/ocaml/fstar-lib/FStar_Unix.mli @@ -0,0 +1,571 @@ +(* + Copyright 2024 Microsoft Research + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. + + Authors: Brian G. Milnes +*) + +(* Wrapper of OCaml unix.mli minimized code, see the OCaml library for docs. *) + +type error = + E2BIG + | EACCES + | EAGAIN + | EBADF + | EBUSY + | ECHILD + | EDEADLK + | EDOM + | EEXIST + | EFAULT + | EFBIG + | EINTR + | EINVAL + | EIO + | EISDIR + | EMFILE + | EMLINK + | ENAMETOOLONG + | ENFILE + | ENODEV + | ENOENT + | ENOEXEC + | ENOLCK + | ENOMEM + | ENOSPC + | ENOSYS + | ENOTDIR + | ENOTEMPTY + | ENOTTY + | ENXIO + | EPERM + | EPIPE + | ERANGE + | EROFS + | ESPIPE + | ESRCH + | EXDEV + | EWOULDBLOCK + | EINPROGRESS + | EALREADY + | ENOTSOCK + | EDESTADDRREQ + | EMSGSIZE + | EPROTOTYPE + | ENOPROTOOPT + | EPROTONOSUPPORT + | ESOCKTNOSUPPORT + | EOPNOTSUPP + | EPFNOSUPPORT + | EAFNOSUPPORT + | EADDRINUSE + | EADDRNOTAVAIL + | ENETDOWN + | ENETUNREACH + | ENETRESET + | ECONNABORTED + | ECONNRESET + | ENOBUFS + | EISCONN + | ENOTCONN + | ESHUTDOWN + | ETOOMANYREFS + | ETIMEDOUT + | ECONNREFUSED + | EHOSTDOWN + | EHOSTUNREACH + | ELOOP + | EOVERFLOW + | EUNKNOWNERR of Z.t + +exception Unix_error of error * string * string +val error_message : error -> string +val handle_unix_error : ('a -> 'b) -> 'a -> 'b +val environment : unit -> string array +val unsafe_environment : unit -> string array +val getenv : string -> string +val unsafe_getenv : string -> string +val putenv : string -> string -> unit + +type process_status = + WEXITED of Z.t + | WSIGNALED of Z.t + | WSTOPPED of Z.t + +type wait_flag = Unix.wait_flag = + WNOHANG + | WUNTRACED + +val execv : string -> string array -> 'a +val execve : string -> string array -> string array -> 'a +val execvp : string -> string array -> 'a +val execvpe : string -> string array -> string array -> 'a +val fork : unit -> Z.t +val wait : unit -> Z.t * process_status +val waitpid : wait_flag list -> Z.t -> Z.t * process_status +val system : string -> process_status +val _exit : Z.t -> 'a +val getpid : unit -> Z.t +val getppid : unit -> Z.t +val nice : Z.t -> Z.t + +type file_descr = Unix.file_descr + +val stdin : file_descr +val stdout : file_descr +val stderr : file_descr + +type open_flag = Unix.open_flag = + O_RDONLY + | O_WRONLY + | O_RDWR + | O_NONBLOCK + | O_APPEND + | O_CREAT + | O_TRUNC + | O_EXCL + | O_NOCTTY + | O_DSYNC + | O_SYNC + | O_RSYNC + | O_SHARE_DELETE + | O_CLOEXEC + | O_KEEPEXEC + +type file_perm = Z.t + +val openfile : string -> open_flag list -> file_perm -> file_descr +val close : file_descr -> unit +val fsync : file_descr -> unit +val read : file_descr -> bytes -> Z.t -> Z.t -> Z.t +val write : file_descr -> bytes -> Z.t -> Z.t -> Z.t +val single_write : file_descr -> bytes -> Z.t -> Z.t -> Z.t +val write_substring : file_descr -> string -> Z.t -> Z.t -> Z.t +val single_write_substring : file_descr -> string -> Z.t -> Z.t -> Z.t +val in_channel_of_descr : file_descr -> in_channel +val out_channel_of_descr : file_descr -> out_channel +val descr_of_in_channel : in_channel -> file_descr +val descr_of_out_channel : out_channel -> file_descr +type seek_command = Unix.seek_command = + SEEK_SET + | SEEK_CUR + | SEEK_END + +val lseek : file_descr -> Z.t -> seek_command -> Z.t +val truncate : string -> Z.t -> unit +val ftruncate : file_descr -> Z.t -> unit + +type file_kind = Unix.file_kind = + S_REG + | S_DIR + | S_CHR + | S_BLK + | S_LNK + | S_FIFO + | S_SOCK + +type stats = + { st_dev : Z.t; + st_ino : Z.t; + st_kind : file_kind; + st_perm : file_perm; + st_nlink : Z.t; + st_uid : Z.t; + st_gid : Z.t; + st_rdev : Z.t; + st_size : Z.t; + st_atime : float; + st_mtime : float; + st_ctime : float; + } + +val stat : string -> stats +val lstat : string -> stats +val fstat : file_descr -> stats +val isatty : file_descr -> bool +val unlink : string -> unit +val rename : string -> string -> unit +val link : string -> string -> unit +val realpath : string -> string + +type access_permission = Unix.access_permission = + R_OK + | W_OK + | X_OK + | F_OK + +val chmod : string -> file_perm -> unit +val fchmod : file_descr -> file_perm -> unit +val chown : string -> Z.t -> Z.t -> unit +val fchown : file_descr -> Z.t -> Z.t -> unit +val umask : file_perm -> file_perm +val access : string -> access_permission list -> unit +val dup : file_descr -> file_descr +val dup2 : file_descr -> file_descr -> unit +val set_nonblock : file_descr -> unit +val clear_nonblock : file_descr -> unit +val set_close_on_exec : file_descr -> unit +val clear_close_on_exec : file_descr -> unit +val mkdir : string -> file_perm -> unit +val rmdir : string -> unit +val chdir : string -> unit +val getcwd : unit -> string +val chroot : string -> unit + +type dir_handle +val opendir : string -> dir_handle +val readdir : dir_handle -> string +val rewinddir : dir_handle -> unit +val closedir : dir_handle -> unit +val pipe : unit -> file_descr * file_descr +val mkfifo : string -> file_perm -> unit + +val create_process : string -> string array -> file_descr -> file_descr -> file_descr -> Z.t +val create_process_env : string -> string array -> string array -> file_descr -> + file_descr -> file_descr -> Z.t +val open_process_in : string -> in_channel +val open_process_out : string -> out_channel +val open_process : string -> in_channel * out_channel +val open_process_full : string -> string array -> in_channel * out_channel * in_channel +val open_process_args : string -> string array -> in_channel * out_channel +val open_process_args_in : string -> string array -> in_channel +val open_process_args_out : string -> string array -> out_channel +val open_process_args_full : string -> string array -> string array -> + in_channel * out_channel * in_channel +val process_in_pid : in_channel -> Z.t +val process_out_pid : out_channel -> Z.t +val process_pid : in_channel * out_channel -> Z.t +val process_full_pid : in_channel * out_channel * in_channel -> Z.t +val close_process_in : in_channel -> process_status +val close_process_out : out_channel -> process_status +val close_process : in_channel * out_channel -> process_status +val close_process_full : in_channel * out_channel * in_channel -> process_status +val symlink : string -> string -> unit +val has_symlink : unit -> bool +val readlink : string -> string +val select : file_descr list -> file_descr list -> file_descr list -> + float -> file_descr list * file_descr list * file_descr list + +type lock_command = Unix.lock_command = + F_ULOCK + | F_LOCK + | F_TLOCK + | F_TEST + | F_RLOCK + | F_TRLOCK + +val lockf : file_descr -> lock_command -> Z.t -> unit +val kill :Z.t -> Z.t -> unit + +type sigprocmask_command = Unix.sigprocmask_command = + SIG_SETMASK + | SIG_BLOCK + | SIG_UNBLOCK + +val sigprocmask : sigprocmask_command -> Z.t list -> Z.t list +val sigpending : unit -> Z.t list +val sigsuspend :Z.t list -> unit +val pause : unit -> unit +(* Where is this? +val sigwait :Z.t list -> Z.t + *) + +type process_times = Unix.process_times = + { tms_utime : float; + tms_stime : float; + tms_cutime : float; + tms_cstime : float; + } + +type tm = + { tm_sec :Z.t; + tm_min :Z.t; + tm_hour :Z.t; + tm_mday :Z.t; + tm_mon :Z.t; + tm_year :Z.t; + tm_wday :Z.t; + tm_yday :Z.t; + tm_isdst : bool; + } + +val time : unit -> float +val gettimeofday : unit -> float +val gmtime : float -> tm +val localtime : float -> tm +val mktime : tm -> float * tm +val alarm :Z.t -> Z.t +val sleep :Z.t -> unit +val sleepf : float -> unit +val times : unit -> process_times +val utimes : string -> float -> float -> unit +type interval_timer = Unix.interval_timer = + ITIMER_REAL | ITIMER_VIRTUAL | ITIMER_PROF + +type interval_timer_status = Unix.interval_timer_status = + { it_interval : float; + it_value : float; + } + +val getitimer : interval_timer -> interval_timer_status +val setitimer : interval_timer -> interval_timer_status -> interval_timer_status +val getuid : unit -> Z.t +val geteuid : unit -> Z.t +val setuid :Z.t -> unit +val getgid : unit -> Z.t +val getegid : unit -> Z.t +val setgid :Z.t -> unit +val getgroups : unit -> Z.t array +val setgroups :Z.t array -> unit +val initgroups : string -> Z.t -> unit + +type passwd_entry = + { pw_name : string; + pw_passwd : string; + pw_uid :Z.t; + pw_gid :Z.t; + pw_gecos : string; + pw_dir : string; + pw_shell : string + } + +type group_entry = + { gr_name : string; + gr_passwd : string; + gr_gid :Z.t; + gr_mem : string array + } +val getlogin : unit -> string +val getpwnam : string -> passwd_entry +val getgrnam : string -> group_entry +val getpwuid :Z.t -> passwd_entry +val getgrgid :Z.t -> group_entry + +type inet_addr = Unix.inet_addr + +val inet_addr_of_string : string -> inet_addr +val string_of_inet_addr : inet_addr -> string +val inet_addr_any : inet_addr +val inet_addr_loopback : inet_addr +val inet6_addr_any : inet_addr +val inet6_addr_loopback : inet_addr +val is_inet6_addr : inet_addr -> bool + +type socket_domain = Unix.socket_domain = + PF_UNIX | PF_INET | PF_INET6 + +type socket_type = Unix.socket_type = + SOCK_STREAM | SOCK_DGRAM | SOCK_RAW | SOCK_SEQPACKET + +type sockaddr = ADDR_UNIX of string | ADDR_INET of inet_addr * Z.t + +val socket : socket_domain -> socket_type -> Z.t -> file_descr +val domain_of_sockaddr: sockaddr -> socket_domain +val socketpair : socket_domain -> socket_type -> Z.t -> file_descr * file_descr +val accept : file_descr -> file_descr * sockaddr +val bind : file_descr -> sockaddr -> unit +val connect : file_descr -> sockaddr -> unit +val listen : file_descr -> Z.t -> unit + +type shutdown_command = Unix.shutdown_command = + SHUTDOWN_RECEIVE + | SHUTDOWN_SEND + | SHUTDOWN_ALL + +val shutdown : file_descr -> shutdown_command -> unit +val getsockname : file_descr -> sockaddr +val getpeername : file_descr -> sockaddr + +type msg_flag = Unix.msg_flag = + MSG_OOB + | MSG_DONTROUTE + | MSG_PEEK + +val recv : file_descr -> bytes -> Z.t -> Z.t -> msg_flag list -> Z.t +val recvfrom : file_descr -> bytes -> Z.t -> Z.t -> msg_flag list -> Z.t * sockaddr +val send : file_descr -> bytes -> Z.t -> Z.t -> msg_flag list -> Z.t +val send_substring : file_descr -> string -> Z.t -> Z.t -> msg_flag list -> Z.t +val sendto : file_descr -> bytes -> Z.t -> Z.t -> msg_flag list -> sockaddr -> Z.t +val sendto_substring : file_descr -> string -> Z.t -> Z.t -> msg_flag list -> sockaddr -> Z.t + +type socket_bool_option = Unix.socket_bool_option = + SO_DEBUG + | SO_BROADCAST + | SO_REUSEADDR + | SO_KEEPALIVE + | SO_DONTROUTE + | SO_OOBINLINE + | SO_ACCEPTCONN + | TCP_NODELAY + | IPV6_ONLY + | SO_REUSEPORT + +type socket_int_option = Unix.socket_int_option = + SO_SNDBUF + | SO_RCVBUF + | SO_ERROR + | SO_TYPE + | SO_RCVLOWAT + | SO_SNDLOWAT + +type socket_optint_option = Unix.socket_optint_option = + SO_LINGER + +type socket_float_option = Unix.socket_float_option = + SO_RCVTIMEO | SO_SNDTIMEO + +val getsockopt : file_descr -> socket_bool_option -> bool +val setsockopt : file_descr -> socket_bool_option -> bool -> unit +val getsockopt_int : file_descr -> socket_int_option -> Z.t +val setsockopt_int : file_descr -> socket_int_option -> Z.t -> unit +val getsockopt_optint : file_descr -> socket_optint_option -> Z.t option +val setsockopt_optint : file_descr -> socket_optint_option -> Z.t option -> unit +val getsockopt_float : file_descr -> socket_float_option -> float +val setsockopt_float : file_descr -> socket_float_option -> float -> unit +val getsockopt_error : file_descr -> error option +val open_connection : sockaddr -> in_channel * out_channel +val shutdown_connection : in_channel -> unit +val establish_server : (in_channel -> out_channel -> unit) -> sockaddr -> unit + +type host_entry = Unix.host_entry = + { h_name : string; + h_aliases : string array; + h_addrtype : socket_domain; + h_addr_list : inet_addr array + } + +type protocol_entry = (* Unix.protocol_entry = *) + { p_name : string; + p_aliases : string array; + p_proto : Z.t + } + +type service_entry = + { s_name : string; + s_aliases : string array; + s_port : Z.t; + s_proto : string + } +val gethostname : unit -> string +val gethostbyname : string -> host_entry +val gethostbyaddr : inet_addr -> host_entry +val getprotobyname : string -> protocol_entry +val getprotobynumber :Z.t -> protocol_entry +val getservbyname : string -> string -> service_entry +val getservbyport :Z.t -> string -> service_entry + +type addr_info = + { ai_family : socket_domain; + ai_socktype : socket_type; + ai_protocol : Z.t; + ai_addr : sockaddr; + ai_canonname : string + } + +type getaddrinfo_option = + AI_FAMILY of socket_domain + | AI_SOCKTYPE of socket_type + | AI_PROTOCOL of Z.t + | AI_NUMERICHOST + | AI_CANONNAME + | AI_PASSIVE + +val getaddrinfo: string -> string -> getaddrinfo_option list -> addr_info list + +type name_info = Unix.name_info = + { ni_hostname : string; + ni_service : string; + } + +type getnameinfo_option = Unix.getnameinfo_option = + NI_NOFQDN + | NI_NUMERICHOST + | NI_NAMEREQD + | NI_NUMERICSERV + | NI_DGRAM + +val getnameinfo : sockaddr -> getnameinfo_option list -> name_info + +type terminal_io = + { + c_ignbrk : bool; + c_brkint : bool; + c_ignpar : bool; + c_parmrk : bool; + c_inpck : bool; + c_istrip : bool; + c_inlcr : bool; + c_igncr : bool; + c_icrnl : bool; + c_ixon : bool; + c_ixoff : bool; + + c_opost : bool; + + c_obaud :Z.t; + c_ibaud :Z.t; + c_csize :Z.t; + c_cstopb :Z.t; + c_cread : bool; + c_parenb : bool; + c_parodd : bool; + c_hupcl : bool; + c_clocal : bool; + + c_isig : bool; + c_icanon : bool; + c_noflsh : bool; + c_echo : bool; + c_echoe : bool; + c_echok : bool; + c_echonl : bool; + + c_vintr : int; + c_vquit : int; + c_verase : int; + c_vkill : int; + c_veof : int; + c_veol : int; + c_vmin : int; + c_vtime : int; + c_vstart : int; + c_vstop : int; + } + +val tcgetattr : file_descr -> terminal_io + +type setattr_when = Unix.setattr_when = + TCSANOW + | TCSADRAIN + | TCSAFLUSH + +val tcsetattr : file_descr -> setattr_when -> terminal_io -> unit +val tcsendbreak : file_descr -> Z.t -> unit +val tcdrain : file_descr -> unit + +type flush_queue = Unix.flush_queue = + TCIFLUSH + | TCOFLUSH + | TCIOFLUSH + +val tcflush : file_descr -> flush_queue -> unit + +type flow_action = Unix.flow_action = + TCOOFF + | TCOON + | TCIOFF + | TCION + +val tcflow : file_descr -> flow_action -> unit +val setsid : unit -> Z.t diff --git a/ocaml/fstar-lib/FStar_Wrap_OCaml.ml b/ocaml/fstar-lib/FStar_Wrap_OCaml.ml new file mode 100644 index 00000000000..f64317d63c7 --- /dev/null +++ b/ocaml/fstar-lib/FStar_Wrap_OCaml.ml @@ -0,0 +1,99 @@ +(* + Copyright 2024 Microsoft Research + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. + + Authors: Brian G. Milnes +*) + +(* + This module provides polymorphic mappers for OCaml Wrapping for F*. + See the mli for the abbreviations. + *) + +let wrapIaOz fn a = Z.of_int (fn a) +let wrapIaOb fn a = fn a +let wrapIzOa fn i = fn (Z.to_int i) + +(* let localtime : float -> tm = wrapIaOwb gmtime to_tm *) +let wrapIaOwb fn w s = w (fn s) + +let wrapIazOz fn a i = Z.of_int (fn a (Z.to_int i)) +let wrapIazbOz fn a i b = Z.of_int (fn a (Z.to_int i) b) +let wrapIwaOb fn w a = fn (w a) +let wrapIwaOpbwc fn w1 w2 a = + match fn (w1 a) with + | (b, c) -> (b,w2 c) +let wrapIazwbOz fn w a i b = Z.of_int (fn a (Z.to_int i) (w b)) +let wrapIaOpzwb fn w a = + match (fn a) with + | (i, c) -> (Z.of_int i, w c) +let wrapIzOz fn i = Z.of_int (fn (Z.to_int i)) +let wrapIazOb fn a i = fn a (Z.to_int i) +let wrapIazzOb fn a i1 i2 = fn a (Z.to_int i1) (Z.to_int i2) +let wrapIabzOc fn a b i = fn a b (Z.to_int i) +let wrapIzzOa fn i1 i2 = fn (Z.to_int i1) (Z.to_int i2) +let wrapIabzzOz fn a b i1 i2 = (Z.of_int (fn a b (Z.to_int i1) (Z.to_int i2))) +let wrapIazzOpzb fn a i1 i2 = + match (fn a (Z.to_int i1) (Z.to_int i2)) with + | (i, b) -> (Z.of_int i, b) +let wrapILwazOpzwb fn w1 w2 lc i = + match (fn (List.map w1 lc) (Z.to_int i)) with + | (i,b) -> (Z.of_int i, w2 b) +let wrapIabcdeOz fn a b c d e = Z.of_int (fn a b c d e) +let wrapIabcdefOz fn a b c d e f = Z.of_int (fn a b c d e f) +let wrapIaOLwb fn w a = List.map w (fn a) +let wrapIaLbOLwc fn w1 w2 a dl = List.map w2 (fn a (List.map w1 dl)) +let wrapILwaOb fn w cl = fn (List.map w cl) +let wrapIaOwA fn w a = Array.map w (fn a) +let wrapIAaOb fn w c = fn (Array.map w c) +let wrapIazOwb fn w i = w (fn (Z.to_int i)) +let wrapIwawbwcOd fn w1 w2 w3 a b c = fn (w1 a) (w2 b) (w3 c) +let wrapIwaOwb fn w1 w2 c = w2 (fn (w1 c)) +let wrapIaOpbwc fn w a = + match (fn a) with + | (b,c) -> (b, w c) +let wrapIawbOc fn w a d = fn a (w d) +let wrapIabOwc fn w a b = w (fn a b) +let wrapIwabOwc fn w1 w2 d b = w2 (fn (w1 d) b) +let wrapIabLwcOLwd fn w1 w2 a b el = List.map w2 (fn a b (List.map w1 el)) +let wrapIwabOc fn w d b = (fn (w d) b) +let wrapIaOwNSb fn w a = + match (fn a) with + | None -> None + | Some e -> Some (w e) + +let wrapIabOwNSc fn w a b = + match (fn a b) with + | None -> None + | Some e -> Some (w e) + +let wrapIabwNScOd fn w a b co = + let co' = + match co with + | None -> None + | Some z -> Some (w z) + in + fn a b co' + +let wrapIabwcwdeOwf fn w1 w2 w3 a b c1 d1 f = + w3 (fn a b (w1 c1) (w2 d1) f) + +let wrapIabwcwdewfOwg fn w1 w2 w3 w4 a b c1 d1 e f1 = + w4 (fn a b (w1 c1) (w2 d1) e (w3 f1)) + +let wrapIabwcwdeOwNSwfwg fn w1 w2 w3 w4 a b c1 d1 e = + match (fn a b (w1 c1) (w2 d1) e) with + | (f1,g1) -> ((w3 f1),(w4 g1)) + +let wrapIabwcOd fn w a b c1 = fn a b (w c1) diff --git a/ocaml/fstar-lib/FStar_Wrap_OCaml.mli b/ocaml/fstar-lib/FStar_Wrap_OCaml.mli new file mode 100644 index 00000000000..7408a2e50a2 --- /dev/null +++ b/ocaml/fstar-lib/FStar_Wrap_OCaml.mli @@ -0,0 +1,106 @@ +(* + Copyright 2024 Microsoft Research + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. + + Authors: Brian G. Milnes +*) + +(* + This module provides polymorphic mappers for OCaml Wrapping for F*. + + Abbreviations + + wrap + f - the function to wrap + I - the input side. + O - the output side. + a,b,c - polymorphic input or output. + z - a Z.t argument or output. + w - a function on the input side to to get a type, + likely an inductive type, with a wrapper named to_X + w - a function on the output side to to get a type, + likely an inductive type, with a wrapper named of_X + p - a pair followed by two output function designations. + Lw(a,b,c) - a list of something to transform, + Aw(a,b,c) - an array of something to transform + NS - for option + *) + + +val wrapIaOz : ('a -> int) -> 'a -> Z.t +val wrapIzOa : (int -> 'a) -> Z.t -> 'a +val wrapIzOz : (int -> int) -> Z.t -> Z.t +val wrapIaOb : ('a -> 'b) -> 'a -> 'b +val wrapIazOb : ('a -> int -> 'b) -> 'a -> Z.t -> 'b +val wrapIazzOb : ('a -> int -> int -> 'b) -> 'a -> Z.t -> Z.t -> 'b +val wrapIabzOc : ('a -> 'b -> int -> 'c) -> 'a -> 'b -> Z.t -> 'c +val wrapIzzOa : (int -> int -> 'a) -> Z.t -> Z.t -> 'a +val wrapIaOwb : ('a -> 'b) -> ('b -> 'c) -> 'a -> 'c +val wrapIwaOb : ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b +val wrapIaOpzwb : ('a -> (int * 'c)) -> ('c -> 'b) -> 'a -> (Z.t * 'b) +val wrapIwaOpbwc : ('a -> 'b * 'c) -> ('d -> 'a) -> ('c -> 'e) -> 'd -> ('b * 'e) +val wrapIazwbOz : ('a -> int -> 'c -> int) -> ('b -> 'c) -> 'a -> Z.t -> 'b -> Z.t +val wrapIazOz : ('a -> int -> int) -> 'a -> Z.t -> Z.t +val wrapIabzzOz : ('a -> 'b -> int -> int -> int) -> + 'a -> 'b -> Z.t -> Z.t -> Z.t +val wrapIazbOz : ('a -> int -> 'b -> int) -> 'a -> Z.t -> 'b -> Z.t + +val wrapIazzOpzb : ('a -> int -> int -> (int * 'b)) -> 'a -> Z.t -> Z.t -> (Z.t * 'b) +val wrapILwazOpzwb : ('a list -> int -> int * 'b) -> ('c -> 'a) -> ('b -> 'd) -> + 'c list -> Z.t -> (Z.t * 'd) +val wrapIaOLwb : ('a -> 'b list) -> ('b -> 'c) -> 'a -> 'c list +val wrapIaLbOLwc : ('a -> 'b list -> 'c list) -> + ('d -> 'b) -> + ('c -> 'e) + -> 'a -> 'd list -> 'e list +val wrapIabcdeOz : ('a -> 'b -> 'c -> 'd -> 'e -> int) -> + 'a -> 'b -> 'c -> 'd -> 'e -> Z.t +val wrapIabcdefOz : ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> int) -> + 'a -> 'b -> 'c -> 'd -> 'e -> 'f -> Z.t +val wrapILwaOb : ('a list -> 'b) -> ('c -> 'a) -> 'c list -> 'b +val wrapIaOwA : ('a -> 'b array) -> ('b -> 'c) -> 'a -> 'c array +val wrapIAaOb : ('a array -> 'b) -> ('c -> 'a) -> 'c array -> 'b +val wrapIazOwb : (int -> 'b) -> ('b -> 'c) -> Z.t -> 'c +val wrapIwawbwcOd : ('a -> 'b -> 'c -> 'd) -> ('e -> 'a) -> ('f -> 'b) -> ('g -> 'c) -> + 'e -> 'f -> 'g -> 'd +val wrapIwaOwb : ('a -> 'b) -> ('c -> 'a) -> ('b -> 'd) -> 'c -> 'd +val wrapIaOpbwc : ('a -> ('b * 'c)) -> ('c -> 'd) -> 'a -> ('b * 'd) +val wrapIawbOc : ('a -> 'b -> 'c) -> ('d -> 'b) -> 'a -> 'd -> 'c +val wrapIabOwc : ('a -> 'b -> 'c) -> ('c -> 'd) -> 'a -> 'b -> 'd +val wrapIwabOwc : ('a -> 'b -> 'c) -> ('d -> 'a) -> ('c -> 'e) -> 'd -> 'b -> 'e +val wrapIabLwcOLwd : ('a -> 'b -> 'c list -> 'd list) -> ('e -> 'c) -> ('d -> 'f) -> + 'a -> 'b -> 'e list -> 'f list +val wrapIwabOc : ('a -> 'b -> 'c) -> ('d -> 'a) -> 'd -> 'b -> 'c +val wrapIaOwNSb : ('a -> 'c option) -> ('c -> 'b ) -> 'a -> 'b option +val wrapIabOwNSc : ('a -> 'b -> 'c option) -> ('c -> 'd ) -> 'a -> 'b -> 'd option +val wrapIabwNScOd : ('a -> 'b -> 'e option -> 'd) -> ('c -> 'e) -> + 'a -> 'b -> 'c option -> 'd +val wrapIabwcwdeOwf : ('a -> 'b -> 'c -> 'd -> 'f -> 'g) -> + ('c1 -> 'c) -> ('d1 -> 'd) -> ('g -> 'g1) -> + 'a -> 'b -> 'c1 -> 'd1 -> 'f -> 'g1 + +val wrapIabwcwdewfOwg: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g1) -> + ('c1 -> 'c) -> ('d1 -> 'd) -> ('f1 -> 'f) -> ('g1 -> 'g) -> + 'a -> 'b -> 'c1 -> 'd1 -> 'e -> 'f1 -> 'g +(* +let recvfrom : file_descr -> bytes -> Z.t -> Z.t -> msg_flag list -> Z.t * sockaddr = + wrapIabwcwdeOwNSwfwg recvfrom Z.to_int Z.to_int Z.of_int of_sockaddr + *) + +val wrapIabwcwdeOwNSwfwg : ('a -> 'b -> 'c -> 'd -> 'e -> ('f1 * 'g1)) -> + ('c1 -> 'c) -> ('d1 -> 'd) -> ('f1 -> 'f) -> ('g1 -> 'g) -> + 'a -> 'b -> 'c1 -> 'd1 -> 'e -> ('f * 'g) + +val wrapIabwcOd : ('a -> 'b -> 'c -> 'd) -> ('c1 -> 'c) -> + 'a -> 'b -> 'c1 -> 'd diff --git a/ocaml/fstar-lib/generated/FStar_Class_Printable.ml b/ocaml/fstar-lib/generated/FStar_Class_Printable.ml index a6c581cf4d4..ee9649496af 100644 --- a/ocaml/fstar-lib/generated/FStar_Class_Printable.ml +++ b/ocaml/fstar-lib/generated/FStar_Class_Printable.ml @@ -259,4 +259,21 @@ let printable_seq : 'b . 'b printable -> 'b FStar_Seq_Base.seq printable = (Prims.strcat (FStar_String.concat "; " (FStar_Seq_Base.seq_to_list strings_of_b)) ">")) - } \ No newline at end of file + } +let (printable_float : FStar_Float.float printable) = + { to_string = (fun f -> "#float") } +let (printable_double : FStar_Float.double printable) = + { to_string = (fun d -> "#double") } +let printable_array : + 'a . 'a printable -> 'a FStar_ImmutableArray_Base.t printable = + fun b -> + { + to_string = + (fun a1 -> + let l = FStar_ImmutableArray.to_list a1 in + let ss = FStar_List_Tot_Base.map (to_string b) l in + Prims.strcat "|[" + (Prims.strcat (FStar_String.concat "; " ss) "]|")) + } +let (printable_char_code : FStar_Char.char_code printable) = + { to_string = (fun cc -> FStar_UInt32.to_string cc) } \ No newline at end of file diff --git a/ocaml/fstar-lib/generated/FStar_Class_Printable_Unix.ml b/ocaml/fstar-lib/generated/FStar_Class_Printable_Unix.ml new file mode 100644 index 00000000000..033066fbfb1 --- /dev/null +++ b/ocaml/fstar-lib/generated/FStar_Class_Printable_Unix.ml @@ -0,0 +1,964 @@ +open Prims +let (printable_in_channel_open_flag : + FStar_In_Channel.open_flag FStar_Class_Printable.printable) = + { + FStar_Class_Printable.to_string = + (fun o -> + match o with + | FStar_In_Channel.Open_rdonly -> "Open_rdonly" + | FStar_In_Channel.Open_wronly -> "Open_wronly" + | FStar_In_Channel.Open_append -> "Open_append" + | FStar_In_Channel.Open_creat -> "Open_creat" + | FStar_In_Channel.Open_trunc -> "Open_trunc" + | FStar_In_Channel.Open_excl -> "Open_excl" + | FStar_In_Channel.Open_binary -> "Open_binary" + | FStar_In_Channel.Open_text -> "Open_text" + | FStar_In_Channel.Open_nonblock -> "Open_nonblock") + } +let (printable_out_channel_open_flag : + FStar_Out_Channel.open_flag FStar_Class_Printable.printable) = + { + FStar_Class_Printable.to_string = + (fun o -> + match o with + | FStar_Out_Channel.Open_rdonly -> "Open_rdonly" + | FStar_Out_Channel.Open_wronly -> "Open_wronly" + | FStar_Out_Channel.Open_append -> "Open_append" + | FStar_Out_Channel.Open_creat -> "Open_creat" + | FStar_Out_Channel.Open_trunc -> "Open_trunc" + | FStar_Out_Channel.Open_excl -> "Open_excl" + | FStar_Out_Channel.Open_binary -> "Open_binary" + | FStar_Out_Channel.Open_text -> "Open_text" + | FStar_Out_Channel.Open_nonblock -> "Open_nonblock") + } +let (printable_unix_error : FStar_Unix.error FStar_Class_Printable.printable) + = + { + FStar_Class_Printable.to_string = + (fun e -> + match e with + | FStar_Unix.E2BIG -> "E2BIG" + | FStar_Unix.EACCES -> "EACCES" + | FStar_Unix.EAGAIN -> "EAGAIN" + | FStar_Unix.EBADF -> "EBADF" + | FStar_Unix.EBUSY -> "EBUSY" + | FStar_Unix.ECHILD -> "ECHILD" + | FStar_Unix.EDEADLK -> "EDEADLK" + | FStar_Unix.EDOM -> "EDOM" + | FStar_Unix.EEXIST -> "EEXIST" + | FStar_Unix.EFAULT -> "EFAULT" + | FStar_Unix.EFBIG -> "EFBIG" + | FStar_Unix.EINTR -> "EINTR" + | FStar_Unix.EINVAL -> "EINVAL" + | FStar_Unix.EIO -> "EIO" + | FStar_Unix.EISDIR -> "EISDIR" + | FStar_Unix.EMFILE -> "EMFILE" + | FStar_Unix.EMLINK -> "EMLINK" + | FStar_Unix.ENAMETOOLONG -> "ENAMETOOLONG" + | FStar_Unix.ENFILE -> "ENFILE" + | FStar_Unix.ENODEV -> "ENODEV" + | FStar_Unix.ENOENT -> "ENOENT" + | FStar_Unix.ENOEXEC -> "ENOEXEC" + | FStar_Unix.ENOLCK -> "ENOLCK" + | FStar_Unix.ENOMEM -> "ENOMEM" + | FStar_Unix.ENOSPC -> "ENOSPC" + | FStar_Unix.ENOSYS -> "ENOSYS" + | FStar_Unix.ENOTDIR -> "ENOTDIR" + | FStar_Unix.ENOTEMPTY -> "ENOTEMPTY" + | FStar_Unix.ENOTTY -> "ENOTTY" + | FStar_Unix.ENXIO -> "ENXIO" + | FStar_Unix.EPERM -> "EPERM" + | FStar_Unix.EPIPE -> "EPIPE" + | FStar_Unix.ERANGE -> "ERANGE" + | FStar_Unix.EROFS -> "EROFS" + | FStar_Unix.ESPIPE -> "ESPIPE" + | FStar_Unix.ESRCH -> "ESRCH" + | FStar_Unix.EXDEV -> "EXDEV" + | FStar_Unix.EWOULDBLOCK -> "EWOULDBLOCK" + | FStar_Unix.EINPROGRESS -> "EINPROGRESS" + | FStar_Unix.EALREADY -> "EALREADY" + | FStar_Unix.ENOTSOCK -> "ENOTSOCK" + | FStar_Unix.EDESTADDRREQ -> "EDESTADDRREQ" + | FStar_Unix.EMSGSIZE -> "EMSGSIZE" + | FStar_Unix.EPROTOTYPE -> "EPROTOTYPE" + | FStar_Unix.ENOPROTOOPT -> "ENOPROTOOPT" + | FStar_Unix.EPROTONOSUPPORT -> "EPROTONOSUPPORT" + | FStar_Unix.ESOCKTNOSUPPORT -> "ESOCKTNOSUPPORT" + | FStar_Unix.EOPNOTSUPP -> "EOPNOTSUPP" + | FStar_Unix.EPFNOSUPPORT -> "EPFNOSUPPORT" + | FStar_Unix.EAFNOSUPPORT -> "EAFNOSUPPORT" + | FStar_Unix.EADDRINUSE -> "EADDRINUSE" + | FStar_Unix.EADDRNOTAVAIL -> "EADDRNOTAVAIL" + | FStar_Unix.ENETDOWN -> "ENETDOWN" + | FStar_Unix.ENETUNREACH -> "ENETUNREACH" + | FStar_Unix.ENETRESET -> "ENETRESET" + | FStar_Unix.ECONNABORTED -> "ECONNABORTED" + | FStar_Unix.ECONNRESET -> "ECONNRESET" + | FStar_Unix.ENOBUFS -> "ENOBUFS" + | FStar_Unix.EISCONN -> "EISCONN" + | FStar_Unix.ENOTCONN -> "ENOTCONN" + | FStar_Unix.ESHUTDOWN -> "ESHUTDOWN" + | FStar_Unix.ETOOMANYREFS -> "ETOOMANYREFS" + | FStar_Unix.ETIMEDOUT -> "ETIMEDOUT" + | FStar_Unix.ECONNREFUSED -> "ECONNREFUSED" + | FStar_Unix.EHOSTDOWN -> "EHOSTDOWN" + | FStar_Unix.EHOSTUNREACH -> "EHOSTUNREACH" + | FStar_Unix.ELOOP -> "ELOOP" + | FStar_Unix.EOVERFLOW -> "EOVERFLOW" + | FStar_Unix.EUNKNOWNERR i -> + Prims.strcat "EUNKNOWNERR " + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_int i)) + } +let (printable_unix_process_status : + FStar_Unix.process_status FStar_Class_Printable.printable) = + { + FStar_Class_Printable.to_string = + (fun p -> + match p with + | FStar_Unix.WEXITED i -> + Prims.strcat "WEXITED " + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_int i) + | FStar_Unix.WSIGNALED i -> + Prims.strcat "WSIGNALED " + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_int i) + | FStar_Unix.WSTOPPED i -> + Prims.strcat "WSTOPPED " + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_int i)) + } +let (printable_unix_wait_flag : + FStar_Unix.wait_flag FStar_Class_Printable.printable) = + { + FStar_Class_Printable.to_string = + (fun w -> + match w with + | FStar_Unix.WNOHANG -> "WNOHANG" + | FStar_Unix.WUNTRACED -> "WUNTRACED") + } +let (printable_unix_open_flag : + FStar_Unix.open_flag FStar_Class_Printable.printable) = + { + FStar_Class_Printable.to_string = + (fun o -> + match o with + | FStar_Unix.O_RDONLY -> "O_RDONLY" + | FStar_Unix.O_WRONLY -> "O_WRONLY" + | FStar_Unix.O_RDWR -> "O_RDWR" + | FStar_Unix.O_NONBLOCK -> "O_NONBLOCK" + | FStar_Unix.O_APPEND -> "O_APPEND" + | FStar_Unix.O_CREAT -> "O_CREAT" + | FStar_Unix.O_TRUNC -> "O_TRUNC" + | FStar_Unix.O_EXCL -> "O_EXCL" + | FStar_Unix.O_NOCTTY -> "O_NOCTTY" + | FStar_Unix.O_DSYNC -> "O_DSYNC" + | FStar_Unix.O_SYNC -> "O_SYNC" + | FStar_Unix.O_RSYNC -> "O_RSYNC" + | FStar_Unix.O_SHARE_DELETE -> "O_SHARE_DELETE" + | FStar_Unix.O_CLOEXEC -> "O_CLOEXEC" + | FStar_Unix.O_KEEPEXEC -> "O_KEEPEXEC") + } +let (printable_unix_file_kind : + FStar_Unix.file_kind FStar_Class_Printable.printable) = + { + FStar_Class_Printable.to_string = + (fun f -> + match f with + | FStar_Unix.S_REG -> "S_REG" + | FStar_Unix.S_DIR -> "S_DIR" + | FStar_Unix.S_CHR -> "S_CHR" + | FStar_Unix.S_BLK -> "S_BLK" + | FStar_Unix.S_LNK -> "S_LNK" + | FStar_Unix.S_FIFO -> "S_FIFO" + | FStar_Unix.S_SOCK -> "S_SOCK") + } +let (printable_unix_stats : FStar_Unix.stats FStar_Class_Printable.printable) + = + { + FStar_Class_Printable.to_string = + (fun r -> + Prims.strcat "{\n" + (Prims.strcat "st_kind = " + (Prims.strcat + (FStar_Class_Printable.to_string printable_unix_file_kind + r.FStar_Unix.st_kind) + (Prims.strcat "\n" + (Prims.strcat "st_atime = " + (Prims.strcat + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_double + r.FStar_Unix.st_atime) + (Prims.strcat "\n" + (Prims.strcat "st_mtime = " + (Prims.strcat + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_double + r.FStar_Unix.st_mtime) + (Prims.strcat "\n" + (Prims.strcat "st_ctime = " + (Prims.strcat + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_double + r.FStar_Unix.st_ctime) "\n}\n")))))))))))) + } +let (printable_unix_access_permission : + FStar_Unix.access_permission FStar_Class_Printable.printable) = + { + FStar_Class_Printable.to_string = + (fun a -> + match a with + | FStar_Unix.R_OK -> "R_OK" + | FStar_Unix.W_OK -> "W_OK" + | FStar_Unix.X_OK -> "X_OK" + | FStar_Unix.F_OK -> "F_OK") + } +let (printable_unix_lock_command : + FStar_Unix.lock_command FStar_Class_Printable.printable) = + { + FStar_Class_Printable.to_string = + (fun l -> + match l with + | FStar_Unix.F_ULOCK -> "F_ULOCK" + | FStar_Unix.F_LOCK -> "F_LOCK" + | FStar_Unix.F_TLOCK -> "F_TLOCK" + | FStar_Unix.F_TEST -> "F_TEST" + | FStar_Unix.F_RLOCK -> "F_RLOCK" + | FStar_Unix.F_TRLOCK -> "F_TRLOCK") + } +let (printable_unix_sigprocmask_command : + FStar_Unix.sigprocmask_command FStar_Class_Printable.printable) = + { + FStar_Class_Printable.to_string = + (fun s -> + match s with + | FStar_Unix.SIG_SETMASK -> "SIG_SETMASK" + | FStar_Unix.SIG_BLOCK -> "SIG_BLOCK" + | FStar_Unix.SIG_UNBLOCK -> "SIG_UNBLOCK") + } +let (printable_unix_process_times : + FStar_Unix.process_times FStar_Class_Printable.printable) = + { + FStar_Class_Printable.to_string = + (fun r -> + Prims.strcat "{\n" + (Prims.strcat "tms_utime = " + (Prims.strcat + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_double + r.FStar_Unix.tms_utime) + (Prims.strcat "\n" + (Prims.strcat "tms_stime = " + (Prims.strcat + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_double + r.FStar_Unix.tms_stime) + (Prims.strcat "\n" + (Prims.strcat "tms_cutime = " + (Prims.strcat + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_double + r.FStar_Unix.tms_cutime) + (Prims.strcat "\n" + (Prims.strcat "tms_cstime = " + (Prims.strcat + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_double + r.FStar_Unix.tms_cstime) + "\n}\n")))))))))))) + } +let (printable_unix_tm : FStar_Unix.tm FStar_Class_Printable.printable) = + { + FStar_Class_Printable.to_string = + (fun r -> + Prims.strcat "{\n" + (Prims.strcat "tm_sec = " + (Prims.strcat + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_int r.FStar_Unix.tm_sec) + (Prims.strcat "\n" + (Prims.strcat "tm_min = " + (Prims.strcat + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_int + r.FStar_Unix.tm_min) + (Prims.strcat "\n" + (Prims.strcat "tm_hour = " + (Prims.strcat + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_int + r.FStar_Unix.tm_hour) + (Prims.strcat "\n" + (Prims.strcat "tm_mday = " + (Prims.strcat + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_int + r.FStar_Unix.tm_mday) + (Prims.strcat "\n" + (Prims.strcat "tm_mon = " + (Prims.strcat + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_int + r.FStar_Unix.tm_mon) + (Prims.strcat "\n" + (Prims.strcat + "tm_year = " + (Prims.strcat + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_int + r.FStar_Unix.tm_year) + (Prims.strcat + "\n" + (Prims.strcat + "tm_wday = " + ( + Prims.strcat + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_int + r.FStar_Unix.tm_wday) + (Prims.strcat + "\n" + (Prims.strcat + "tm_yday = " + (Prims.strcat + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_int + r.FStar_Unix.tm_yday) + (Prims.strcat + "\n" + (Prims.strcat + "tm_isdst = " + (Prims.strcat + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_bool + r.FStar_Unix.tm_isdst) + "\n}\n"))))))))))))))))))))))))))) + } +let (printable_unix_interval_timer : + FStar_Unix.interval_timer FStar_Class_Printable.printable) = + { + FStar_Class_Printable.to_string = + (fun i -> + match i with + | FStar_Unix.ITIMER_REAL -> "ITIMER_REAL" + | FStar_Unix.ITIMER_VIRTUAL -> "ITIMER_VIRTUAL" + | FStar_Unix.ITIMER_PROF -> "ITIMER_PROF") + } +let (printable_unix_interval_timer_status : + FStar_Unix.interval_timer_status FStar_Class_Printable.printable) = + { + FStar_Class_Printable.to_string = + (fun r -> + Prims.strcat "{\n" + (Prims.strcat "it_interval = " + (Prims.strcat + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_double + r.FStar_Unix.it_interval) + (Prims.strcat "\n" + (Prims.strcat "it_value = " + (Prims.strcat + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_double + r.FStar_Unix.it_value) "\n}\n")))))) + } +let (printable_unix_passwd_entry : + FStar_Unix.passwd_entry FStar_Class_Printable.printable) = + { + FStar_Class_Printable.to_string = + (fun r -> + Prims.strcat "pw_name = " + (Prims.strcat + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_string r.FStar_Unix.pw_name) + (Prims.strcat "\n" + (Prims.strcat "pw_passwd = " + (Prims.strcat + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_string + r.FStar_Unix.pw_passwd) + (Prims.strcat "\n" + (Prims.strcat "pw_uid = " + (Prims.strcat + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_int + r.FStar_Unix.pw_uid) + (Prims.strcat "\n" + (Prims.strcat "pw_gid = " + (Prims.strcat + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_int + r.FStar_Unix.pw_gid) + (Prims.strcat "\n" + (Prims.strcat "pw_gecos = " + (Prims.strcat + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_string + r.FStar_Unix.pw_gecos) + (Prims.strcat "\n" + (Prims.strcat + "pw_dir = " + (Prims.strcat + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_string + r.FStar_Unix.pw_dir) + (Prims.strcat "\n" + (Prims.strcat + "pw_shell = " + (Prims.strcat + ( + FStar_Class_Printable.to_string + FStar_Class_Printable.printable_string + r.FStar_Unix.pw_shell) + "\n}\n")))))))))))))))))))) + } +let (printable_unix_group_entry : + FStar_Unix.group_entry FStar_Class_Printable.printable) = + { + FStar_Class_Printable.to_string = + (fun r -> + Prims.strcat "{\n" + (Prims.strcat "gr_name = " + (Prims.strcat + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_string + r.FStar_Unix.gr_name) + (Prims.strcat "\n" + (Prims.strcat "gr_passwd = " + (Prims.strcat + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_string + r.FStar_Unix.gr_passwd) + (Prims.strcat "\n" + (Prims.strcat "gr_gid = " + (Prims.strcat + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_int + r.FStar_Unix.gr_gid) + (Prims.strcat "\n" + (Prims.strcat "gr_mem = " + (Prims.strcat + (FStar_Class_Printable.to_string + (FStar_Class_Printable.printable_array + FStar_Class_Printable.printable_string) + r.FStar_Unix.gr_mem) "\n}\n")))))))))))) + } +let (printable_unix_socket_domain : + FStar_Unix.socket_domain FStar_Class_Printable.printable) = + { + FStar_Class_Printable.to_string = + (fun s -> + match s with + | FStar_Unix.PF_UNIX -> "PF_UNIX" + | FStar_Unix.PF_INET -> "PF_INET" + | FStar_Unix.PF_INET6 -> "PF_INET6") + } +let (printable_unix_socket_type : + FStar_Unix.socket_type FStar_Class_Printable.printable) = + { + FStar_Class_Printable.to_string = + (fun s -> + match s with + | FStar_Unix.SOCK_STREAM -> "SOCK_STREAM" + | FStar_Unix.SOCK_DGRAM -> "SOCK_DGRAM" + | FStar_Unix.SOCK_RAW -> "SOCK_RAW" + | FStar_Unix.SOCK_SEQPACKET -> "SOCK_SEQPACKET") + } +let (printable_inet_addr : + FStar_Unix.inet_addr FStar_Class_Printable.printable) = + { FStar_Class_Printable.to_string = (fun ia -> "inet_adder is abstract") } +let (printable_unix_sockaddr : + FStar_Unix.sockaddr FStar_Class_Printable.printable) = + { + FStar_Class_Printable.to_string = + (fun s -> + match s with + | FStar_Unix.ADDR_UNIX s1 -> + Prims.strcat "ADDR_UNIX " + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_string s1) + | FStar_Unix.ADDR_INET (a, i) -> + Prims.strcat "ADDR_INET " + (Prims.strcat + (FStar_Class_Printable.to_string printable_inet_addr a) + (Prims.strcat " " + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_int i)))) + } +let (printable_unix_shutdown_command : + FStar_Unix.shutdown_command FStar_Class_Printable.printable) = + { + FStar_Class_Printable.to_string = + (fun s -> + match s with + | FStar_Unix.SHUTDOWN_RECEIVE -> "SHUTDOWN_RECEIVE" + | FStar_Unix.SHUTDOWN_SEND -> "SHUTDOWN_SEND" + | FStar_Unix.SHUTDOWN_ALL -> "SHUTDOWN_ALL") + } +let (printable_unix_msg_flag : + FStar_Unix.msg_flag FStar_Class_Printable.printable) = + { + FStar_Class_Printable.to_string = + (fun m -> + match m with + | FStar_Unix.MSG_OOB -> "MSG_OOB" + | FStar_Unix.MSG_DONTROUTE -> "MSG_DONTROUTE" + | FStar_Unix.MSG_PEEK -> "MSG_PEEK") + } +let (printable_unix_socket_bool_option : + FStar_Unix.socket_bool_option FStar_Class_Printable.printable) = + { + FStar_Class_Printable.to_string = + (fun s -> + match s with + | FStar_Unix.SO_DEBUG -> "SO_DEBUG" + | FStar_Unix.SO_BROADCAST -> "SO_BROADCAST" + | FStar_Unix.SO_REUSEADDR -> "SO_REUSEADDR" + | FStar_Unix.SO_KEEPALIVE -> "SO_KEEPALIVE" + | FStar_Unix.SO_DONTROUTE -> "SO_DONTROUTE" + | FStar_Unix.SO_OOBINLINE -> "SO_OOBINLINE" + | FStar_Unix.SO_ACCEPTCONN -> "SO_ACCEPTCONN" + | FStar_Unix.TCP_NODELAY -> "TCP_NODELAY" + | FStar_Unix.IPV6_ONLY -> "IPV6_ONLY" + | FStar_Unix.SO_REUSEPORT -> "SO_REUSEPORT") + } +let (printable_unix_socket_int_option : + FStar_Unix.socket_int_option FStar_Class_Printable.printable) = + { + FStar_Class_Printable.to_string = + (fun s -> + match s with + | FStar_Unix.SO_SNDBUF -> "SO_SNDBUF" + | FStar_Unix.SO_RCVBUF -> "SO_RCVBUF" + | FStar_Unix.SO_ERROR -> "SO_ERROR" + | FStar_Unix.SO_TYPE -> "SO_TYPE" + | FStar_Unix.SO_RCVLOWAT -> "SO_RCVLOWAT" + | FStar_Unix.SO_SNDLOWAT -> "SO_SNDLOWAT") + } +let (printable_unix_socket_optint_option : + FStar_Unix.socket_optint_option FStar_Class_Printable.printable) = + { + FStar_Class_Printable.to_string = + (fun s -> match s with | FStar_Unix.SO_LINGER -> "SO_LINGER") + } +let (printable_unix_socket_float_option : + FStar_Unix.socket_float_option FStar_Class_Printable.printable) = + { + FStar_Class_Printable.to_string = + (fun s -> + match s with + | FStar_Unix.SO_RCVTIMEO -> "SO_RCVTIMEO" + | FStar_Unix.SO_SNDTIMEO -> "SO_SNDTIMEO") + } +let (printable_unix_host_entry : + FStar_Unix.host_entry FStar_Class_Printable.printable) = + { + FStar_Class_Printable.to_string = + (fun r -> + Prims.strcat "{\n" + (Prims.strcat "h_name = " + (Prims.strcat + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_string + r.FStar_Unix.h_name) + (Prims.strcat "\n" + (Prims.strcat "h_aliases = " + (Prims.strcat + (FStar_Class_Printable.to_string + (FStar_Class_Printable.printable_array + FStar_Class_Printable.printable_string) + r.FStar_Unix.h_aliases) + (Prims.strcat "\n" + (Prims.strcat "h_addrtype = " + (Prims.strcat + (FStar_Class_Printable.to_string + printable_unix_socket_domain + r.FStar_Unix.h_addrtype) + (Prims.strcat "\n" + (Prims.strcat "h_addr_list = " + (Prims.strcat + (FStar_Class_Printable.to_string + (FStar_Class_Printable.printable_array + printable_inet_addr) + r.FStar_Unix.h_addr_list) + "\n}\n")))))))))))) + } +let (printable_unix_protocol_entry : + FStar_Unix.protocol_entry FStar_Class_Printable.printable) = + { + FStar_Class_Printable.to_string = + (fun r -> + Prims.strcat "{\n" + (Prims.strcat "p_name = " + (Prims.strcat + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_string + r.FStar_Unix.p_name) + (Prims.strcat "\n" + (Prims.strcat "p_aliases = " + (Prims.strcat + (FStar_Class_Printable.to_string + (FStar_Class_Printable.printable_array + FStar_Class_Printable.printable_string) + r.FStar_Unix.p_aliases) "\n\n}\n")))))) + } +let (printable_unix_service_entry : + FStar_Unix.service_entry FStar_Class_Printable.printable) = + { + FStar_Class_Printable.to_string = + (fun r -> + Prims.strcat "{\n" + (Prims.strcat "s_name = " + (Prims.strcat + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_string + r.FStar_Unix.s_name) + (Prims.strcat "\n" + (Prims.strcat "s_aliases = " + (Prims.strcat + (FStar_Class_Printable.to_string + (FStar_Class_Printable.printable_array + FStar_Class_Printable.printable_string) + r.FStar_Unix.s_aliases) + (Prims.strcat "\n" + (Prims.strcat "\n" + (Prims.strcat "s_proto = " + (Prims.strcat + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_string + r.FStar_Unix.s_proto) "\n}\n")))))))))) + } +let (printable_unix_addr_info : + FStar_Unix.addr_info FStar_Class_Printable.printable) = + { + FStar_Class_Printable.to_string = + (fun r -> + Prims.strcat "{\n" + (Prims.strcat "ai_family = " + (Prims.strcat + (FStar_Class_Printable.to_string + printable_unix_socket_domain r.FStar_Unix.ai_family) + (Prims.strcat "\n" + (Prims.strcat "ai_socktype = " + (Prims.strcat + (FStar_Class_Printable.to_string + printable_unix_socket_type + r.FStar_Unix.ai_socktype) + (Prims.strcat "\n" + (Prims.strcat "ai_addr = " + (Prims.strcat + (FStar_Class_Printable.to_string + printable_unix_sockaddr + r.FStar_Unix.ai_addr) + (Prims.strcat "\n" + (Prims.strcat "ai_canonname = " + (Prims.strcat + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_string + r.FStar_Unix.ai_canonname) + "\n}\n")))))))))))) + } +let (printable_unix_getaddrinfo_option : + FStar_Unix.getaddrinfo_option FStar_Class_Printable.printable) = + { + FStar_Class_Printable.to_string = + (fun g -> + match g with + | FStar_Unix.AI_FAMILY sd -> + Prims.strcat "AI_FAMILY " + (FStar_Class_Printable.to_string printable_unix_socket_domain + sd) + | FStar_Unix.AI_SOCKTYPE st -> + Prims.strcat "AI_SOCKTYPE " + (FStar_Class_Printable.to_string printable_unix_socket_type st) + | FStar_Unix.AI_PROTOCOL i -> + Prims.strcat "AI_PROTOCOL " + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_int i) + | FStar_Unix.AI_NUMERICHOST -> "AI_NUMERICHOST" + | FStar_Unix.AI_CANONNAME -> "AI_CANONNAME" + | FStar_Unix.AI_PASSIVE -> "AI_PASSIVE") + } +let (printable_unix_name_info : + FStar_Unix.name_info FStar_Class_Printable.printable) = + { + FStar_Class_Printable.to_string = + (fun r -> + Prims.strcat "{\n" + (Prims.strcat "ni_hostname = " + (Prims.strcat + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_string + r.FStar_Unix.ni_hostname) + (Prims.strcat "\n" + (Prims.strcat "ni_service = " + (Prims.strcat + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_string + r.FStar_Unix.ni_service) "\n}\n")))))) + } +let (printable_unix_getnameinfo_option : + FStar_Unix.getnameinfo_option FStar_Class_Printable.printable) = + { + FStar_Class_Printable.to_string = + (fun g -> + match g with + | FStar_Unix.NI_NOFQDN -> "NI_NOFQDN" + | FStar_Unix.NI_NUMERICHOST -> "NI_NUMERICHOST" + | FStar_Unix.NI_NAMEREQD -> "NI_NAMEREQD" + | FStar_Unix.NI_NUMERICSERV -> "NI_NUMERICSERV" + | FStar_Unix.NI_DGRAM -> "NI_DGRAM") + } +let (printable_unix_terminal_io : + FStar_Unix.terminal_io FStar_Class_Printable.printable) = + { + FStar_Class_Printable.to_string = + (fun r -> + Prims.strcat "{\n" + (Prims.strcat "c_ignbrk = " + (Prims.strcat + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_bool + r.FStar_Unix.c_ignbrk) + (Prims.strcat "\n" + (Prims.strcat "c_brkint = " + (Prims.strcat + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_bool + r.FStar_Unix.c_brkint) + (Prims.strcat "\n" + (Prims.strcat "c_ignpar = " + (Prims.strcat + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_bool + r.FStar_Unix.c_ignpar) + (Prims.strcat "\n" + (Prims.strcat "c_parmrk = " + (Prims.strcat + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_bool + r.FStar_Unix.c_parmrk) + (Prims.strcat "\n" + (Prims.strcat "c_inpck = " + (Prims.strcat + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_bool + r.FStar_Unix.c_inpck) + (Prims.strcat "\n" + (Prims.strcat + "c_istrip = " + (Prims.strcat + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_bool + r.FStar_Unix.c_istrip) + (Prims.strcat + "\n" + (Prims.strcat + "c_inlcr = " + ( + Prims.strcat + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_bool + r.FStar_Unix.c_inlcr) + (Prims.strcat + "\n" + (Prims.strcat + "c_igncr = " + (Prims.strcat + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_bool + r.FStar_Unix.c_igncr) + (Prims.strcat + "\n" + (Prims.strcat + "c_icrnl = " + (Prims.strcat + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_bool + r.FStar_Unix.c_icrnl) + (Prims.strcat + "\n" + (Prims.strcat + "c_ixon = " + (Prims.strcat + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_bool + r.FStar_Unix.c_ixon) + (Prims.strcat + "\n" + (Prims.strcat + "c_ixoff = " + (Prims.strcat + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_bool + r.FStar_Unix.c_ixoff) + (Prims.strcat + "\n" + (Prims.strcat + "c_opost = " + (Prims.strcat + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_bool + r.FStar_Unix.c_opost) + (Prims.strcat + "\n" + (Prims.strcat + "c_obaud = " + (Prims.strcat + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_int + r.FStar_Unix.c_obaud) + (Prims.strcat + "\n" + (Prims.strcat + "c_ibaud = " + (Prims.strcat + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_int + r.FStar_Unix.c_ibaud) + (Prims.strcat + "\n" + (Prims.strcat + "c_csize = " + (Prims.strcat + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_int + r.FStar_Unix.c_csize) + (Prims.strcat + "\n" + (Prims.strcat + "c_cstopb = " + (Prims.strcat + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_int + r.FStar_Unix.c_cstopb) + (Prims.strcat + "\n" + (Prims.strcat + "c_cread = " + (Prims.strcat + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_bool + r.FStar_Unix.c_cread) + (Prims.strcat + "\n" + (Prims.strcat + "c_parenb = " + (Prims.strcat + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_bool + r.FStar_Unix.c_parenb) + (Prims.strcat + "\n" + (Prims.strcat + "c_parodd = " + (Prims.strcat + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_bool + r.FStar_Unix.c_parodd) + (Prims.strcat + "\n" + (Prims.strcat + "c_hupcl = " + (Prims.strcat + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_bool + r.FStar_Unix.c_hupcl) + (Prims.strcat + "\n" + (Prims.strcat + "c_clocal = " + (Prims.strcat + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_bool + r.FStar_Unix.c_clocal) + (Prims.strcat + "\n" + (Prims.strcat + "c_isig = " + (Prims.strcat + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_bool + r.FStar_Unix.c_isig) + (Prims.strcat + "\n" + (Prims.strcat + "c_icanon = " + (Prims.strcat + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_bool + r.FStar_Unix.c_icanon) + (Prims.strcat + "\n" + (Prims.strcat + "c_noflsh = " + (Prims.strcat + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_bool + r.FStar_Unix.c_noflsh) + (Prims.strcat + "\n" + (Prims.strcat + "c_echo = " + (Prims.strcat + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_bool + r.FStar_Unix.c_echo) + (Prims.strcat + "\n" + (Prims.strcat + "c_echoe = " + (Prims.strcat + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_bool + r.FStar_Unix.c_echoe) + (Prims.strcat + "\n" + (Prims.strcat + "c_echok = " + (Prims.strcat + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_bool + r.FStar_Unix.c_echok) + (Prims.strcat + "\n" + (Prims.strcat + "c_echonl = " + (Prims.strcat + (FStar_Class_Printable.to_string + FStar_Class_Printable.printable_bool + r.FStar_Unix.c_echonl) + "\n}\n")))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + } +let (printable_unix_setattr_when : + FStar_Unix.setattr_when FStar_Class_Printable.printable) = + { + FStar_Class_Printable.to_string = + (fun s -> + match s with + | FStar_Unix.TCSANOW -> "TCSANOW" + | FStar_Unix.TCSADRAIN -> "TCSADRAIN" + | FStar_Unix.TCSAFLUSH -> "TCSAFLUSH") + } +let (printable_unix_flush_queue : + FStar_Unix.flush_queue FStar_Class_Printable.printable) = + { + FStar_Class_Printable.to_string = + (fun f -> + match f with + | FStar_Unix.TCIFLUSH -> "TCIFLUSH" + | FStar_Unix.TCOFLUSH -> "TCOFLUSH" + | FStar_Unix.TCIOFLUSH -> "TCIOFLUSH") + } +let (printable_unix_flow_action : + FStar_Unix.flow_action FStar_Class_Printable.printable) = + { + FStar_Class_Printable.to_string = + (fun f -> + match f with + | FStar_Unix.TCOOFF -> "TCOOFF" + | FStar_Unix.TCOON -> "TCOON" + | FStar_Unix.TCIOFF -> "TCIOFF" + | FStar_Unix.TCION -> "TCION") + } \ No newline at end of file diff --git a/ocaml/fstar-lib/generated/FStar_FDString.ml b/ocaml/fstar-lib/generated/FStar_FDString.ml new file mode 100644 index 00000000000..904dad1942d --- /dev/null +++ b/ocaml/fstar-lib/generated/FStar_FDString.ml @@ -0,0 +1,36 @@ +open Prims +type fd_string = Prims.string Prims.list +type fd_string_read = fd_string +type fd_string_write = fd_string +let (open_read_file : unit -> fd_string_read) = + fun uu___ -> (fun uu___ -> Obj.magic []) uu___ +let (open_write_file : unit -> fd_string_write) = + fun uu___ -> (fun uu___ -> Obj.magic []) uu___ +let (print_newline : fd_string_write -> fd_string_write) = + fun uu___ -> (fun fdsw -> Obj.magic ("\n" :: (Obj.magic fdsw))) uu___ +let (print_string : fd_string_write -> Prims.string -> fd_string_write) = + fun uu___1 -> + fun uu___ -> + (fun fdsw -> fun s -> Obj.magic (s :: (Obj.magic fdsw))) uu___1 uu___ +let (input_line : fd_string_read -> (Prims.string * fd_string_read)) = + fun fdsr -> + match Obj.magic fdsr with + | [] -> FStar_Exn.raise FStar_IO.EOF + | h::t -> (h, (Obj.magic t)) +let (read_line : fd_string_read -> (Prims.string * fd_string_read)) = + fun fdsr -> + match Obj.magic fdsr with + | [] -> FStar_Exn.raise FStar_IO.EOF + | h::t -> (h, (Obj.magic t)) +let (write_string : fd_string_write -> Prims.string -> fd_string_write) = + fun uu___1 -> + fun uu___ -> + (fun fdsw -> fun s -> Obj.magic (s :: (Obj.magic fdsw))) uu___1 uu___ +let (fd_write_to_fd_read : fd_string_write -> fd_string_read) = + fun uu___ -> + (fun fdsw -> Obj.magic (FStar_List_Tot_Base.rev (Obj.magic fdsw))) uu___ +let (fd_write_to_string : fd_string_write -> Prims.string) = + fun fdsw -> + let fdsr = fd_write_to_fd_read fdsw in + FStar_List_Tot_Base.fold_right (fun s1 -> fun s2 -> Prims.strcat s1 s2) + (FStar_List_Tot_Base.rev (Obj.magic fdsw)) "" \ No newline at end of file diff --git a/ulib/FStar.Class.Printable.Unix.fst b/ulib/FStar.Class.Printable.Unix.fst new file mode 100644 index 00000000000..028bd11dac6 --- /dev/null +++ b/ulib/FStar.Class.Printable.Unix.fst @@ -0,0 +1,563 @@ +(* + Copyright 2024 Microsoft Research + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. + + Authors: Brian G. Milnes +*) + +module FStar.Class.Printable.Unix + +open FStar.String +open FStar.Seq.Properties +open FStar.Class.Printable + +/// From FStar.In_Channel and FStar.Out_Channel, can I kill this duplication? + +instance printable_in_channel_open_flag : printable FStar.In_Channel.open_flag = +{ + to_string = (fun o -> + match o with + | FStar.In_Channel.Open_rdonly -> "Open_rdonly" + | FStar.In_Channel.Open_wronly -> "Open_wronly" + | FStar.In_Channel.Open_append -> "Open_append" + | FStar.In_Channel.Open_creat -> "Open_creat" + | FStar.In_Channel.Open_trunc -> "Open_trunc" + | FStar.In_Channel.Open_excl -> "Open_excl" + | FStar.In_Channel.Open_binary -> "Open_binary" + | FStar.In_Channel.Open_text -> "Open_text" + | FStar.In_Channel.Open_nonblock -> "Open_nonblock") +} + +instance printable_out_channel_open_flag : printable FStar.Out_Channel.open_flag = +{ + to_string = (fun o -> + match o with + | FStar.Out_Channel.Open_rdonly -> "Open_rdonly" + | FStar.Out_Channel.Open_wronly -> "Open_wronly" + | FStar.Out_Channel.Open_append -> "Open_append" + | FStar.Out_Channel.Open_creat -> "Open_creat" + | FStar.Out_Channel.Open_trunc -> "Open_trunc" + | FStar.Out_Channel.Open_excl -> "Open_excl" + | FStar.Out_Channel.Open_binary -> "Open_binary" + | FStar.Out_Channel.Open_text -> "Open_text" + | FStar.Out_Channel.Open_nonblock -> "Open_nonblock") +} + +open FStar.Unix + +/// From FStar.Unix + +instance printable_unix_error : printable FStar.Unix.error = +{ + to_string = (fun e -> + match e with + | E2BIG -> "E2BIG" + | EACCES -> "EACCES" + | EAGAIN -> "EAGAIN" + | EBADF -> "EBADF" + | EBUSY -> "EBUSY" + | ECHILD -> "ECHILD" + | EDEADLK -> "EDEADLK" + | EDOM -> "EDOM" + | EEXIST -> "EEXIST" + | EFAULT -> "EFAULT" + | EFBIG -> "EFBIG" + | EINTR -> "EINTR" + | EINVAL -> "EINVAL" + | EIO -> "EIO" + | EISDIR -> "EISDIR" + | EMFILE -> "EMFILE" + | EMLINK -> "EMLINK" + | ENAMETOOLONG -> "ENAMETOOLONG" + | ENFILE -> "ENFILE" + | ENODEV -> "ENODEV" + | ENOENT -> "ENOENT" + | ENOEXEC -> "ENOEXEC" + | ENOLCK -> "ENOLCK" + | ENOMEM -> "ENOMEM" + | ENOSPC -> "ENOSPC" + | ENOSYS -> "ENOSYS" + | ENOTDIR -> "ENOTDIR" + | ENOTEMPTY -> "ENOTEMPTY" + | ENOTTY -> "ENOTTY" + | ENXIO -> "ENXIO" + | EPERM -> "EPERM" + | EPIPE -> "EPIPE" + | ERANGE -> "ERANGE" + | EROFS -> "EROFS" + | ESPIPE -> "ESPIPE" + | ESRCH -> "ESRCH" + | EXDEV -> "EXDEV" + | EWOULDBLOCK -> "EWOULDBLOCK" + | EINPROGRESS -> "EINPROGRESS" + | EALREADY -> "EALREADY" + | ENOTSOCK -> "ENOTSOCK" + | EDESTADDRREQ -> "EDESTADDRREQ" + | EMSGSIZE -> "EMSGSIZE" + | EPROTOTYPE -> "EPROTOTYPE" + | ENOPROTOOPT -> "ENOPROTOOPT" + | EPROTONOSUPPORT -> "EPROTONOSUPPORT" + | ESOCKTNOSUPPORT -> "ESOCKTNOSUPPORT" + | EOPNOTSUPP -> "EOPNOTSUPP" + | EPFNOSUPPORT -> "EPFNOSUPPORT" + | EAFNOSUPPORT -> "EAFNOSUPPORT" + | EADDRINUSE -> "EADDRINUSE" + | EADDRNOTAVAIL -> "EADDRNOTAVAIL" + | ENETDOWN -> "ENETDOWN" + | ENETUNREACH -> "ENETUNREACH" + | ENETRESET -> "ENETRESET" + | ECONNABORTED -> "ECONNABORTED" + | ECONNRESET -> "ECONNRESET" + | ENOBUFS -> "ENOBUFS" + | EISCONN -> "EISCONN" + | ENOTCONN -> "ENOTCONN" + | ESHUTDOWN -> "ESHUTDOWN" + | ETOOMANYREFS -> "ETOOMANYREFS" + | ETIMEDOUT -> "ETIMEDOUT" + | ECONNREFUSED -> "ECONNREFUSED" + | EHOSTDOWN -> "EHOSTDOWN" + | EHOSTUNREACH -> "EHOSTUNREACH" + | ELOOP -> "ELOOP" + | EOVERFLOW -> "EOVERFLOW" + | EUNKNOWNERR i -> "EUNKNOWNERR " ^ (to_string i)) +} + +(* Can I do this for exceptions? +instance printable_unix_Unix_error : printable FStar.Unix.Unix_error = +{ + to_string = (fun e -> + match e with + | Unix_error t -> "Unix_error " ^ (to_string t)) +} +*) + +instance printable_unix_process_status : printable FStar.Unix.process_status = +{ + to_string = (fun p -> + match p with + | WEXITED i -> "WEXITED " ^ (to_string i) + | WSIGNALED i -> "WSIGNALED " ^ (to_string i) + | WSTOPPED i -> "WSTOPPED " ^ (to_string i)) +} + +instance printable_unix_wait_flag : printable FStar.Unix.wait_flag = +{ + to_string = (fun w -> + match w with + | WNOHANG -> "WNOHANG" + | WUNTRACED -> "WUNTRACED") +} + +instance printable_unix_open_flag : printable FStar.Unix.open_flag = +{ + to_string = (fun o -> + match o with + | O_RDONLY -> "O_RDONLY" + | O_WRONLY -> "O_WRONLY" + | O_RDWR -> "O_RDWR" + | O_NONBLOCK -> "O_NONBLOCK" + | O_APPEND -> "O_APPEND" + | O_CREAT -> "O_CREAT" + | O_TRUNC -> "O_TRUNC" + | O_EXCL -> "O_EXCL" + | O_NOCTTY -> "O_NOCTTY" + | O_DSYNC -> "O_DSYNC" + | O_SYNC -> "O_SYNC" + | O_RSYNC -> "O_RSYNC" + | O_SHARE_DELETE -> "O_SHARE_DELETE" + | O_CLOEXEC -> "O_CLOEXEC" + | O_KEEPEXEC -> "O_KEEPEXEC") +} + +instance printable_unix_file_kind : printable FStar.Unix.file_kind = +{ + to_string = (fun f -> + match f with + | S_REG -> "S_REG" + | S_DIR -> "S_DIR" + | S_CHR -> "S_CHR" + | S_BLK -> "S_BLK" + | S_LNK -> "S_LNK" + | S_FIFO -> "S_FIFO" + | S_SOCK -> "S_SOCK") +} + +instance printable_unix_stats : printable FStar.Unix.stats = +{ + to_string = (fun r -> + "{\n" ^ +(* "st_dev = " ^ (to_string r.st_dev) ^ "\n" ^ + "st_ino = " ^ (to_string r.st_ino) ^ "\n" ^*) + "st_kind = " ^ (to_string r.st_kind) ^ "\n" ^ +(* "st_perm = " ^ (to_string r.st_perm) ^ "\n" ^ *) +(* "st_nlink = " ^ (to_string r.st_nlink) ^ "\n" ^ + "st_uid = " ^ (to_string r.st_uid) ^ "\n" ^ + "st_gid = " ^ (to_string r.st_gid) ^ "\n" ^ + "st_rdev = " ^ (to_string r.st_rdev) ^ "\n" ^ + "st_size = " ^ (to_string r.st_size) ^ "\n" ^ +*) + "st_atime = " ^ (to_string r.st_atime) ^ "\n" ^ + "st_mtime = " ^ (to_string r.st_mtime) ^ "\n" ^ + "st_ctime = " ^ (to_string r.st_ctime) ^ "\n" ^ + "}\n" + ) +} + +instance printable_unix_access_permission : printable FStar.Unix.access_permission = +{ + to_string = (fun a -> + match a with + | R_OK -> "R_OK" + | W_OK -> "W_OK" + | X_OK -> "X_OK" + | F_OK -> "F_OK") +} + +instance printable_unix_lock_command : printable FStar.Unix.lock_command = +{ +to_string = (fun l -> + match l with + | F_ULOCK -> "F_ULOCK" + | F_LOCK -> "F_LOCK" + | F_TLOCK -> "F_TLOCK" + | F_TEST -> "F_TEST" + | F_RLOCK -> "F_RLOCK" + | F_TRLOCK -> "F_TRLOCK") +} + +instance printable_unix_sigprocmask_command : printable FStar.Unix.sigprocmask_command = +{ + to_string = (fun s -> + match s with + | SIG_SETMASK -> "SIG_SETMASK" + | SIG_BLOCK -> "SIG_BLOCK" + | SIG_UNBLOCK -> "SIG_UNBLOCK") +} + +instance printable_unix_process_times : printable FStar.Unix.process_times = +{ + to_string = (fun r -> + "{\n" ^ + "tms_utime = " ^ (to_string r.tms_utime) ^ "\n" ^ + "tms_stime = " ^ (to_string r.tms_stime) ^ "\n" ^ + "tms_cutime = " ^ (to_string r.tms_cutime) ^ "\n" ^ + "tms_cstime = " ^ (to_string r.tms_cstime) ^ "\n" ^ + "}\n") +} + +instance printable_unix_tm : printable FStar.Unix.tm = +{ + to_string = (fun r -> + "{\n" ^ + "tm_sec = " ^ (to_string r.tm_sec) ^ "\n" ^ + "tm_min = " ^ (to_string r.tm_min) ^ "\n" ^ + "tm_hour = " ^ (to_string r.tm_hour) ^ "\n" ^ + "tm_mday = " ^ (to_string r.tm_mday) ^ "\n" ^ + "tm_mon = " ^ (to_string r.tm_mon) ^ "\n" ^ + "tm_year = " ^ (to_string r.tm_year) ^ "\n" ^ + "tm_wday = " ^ (to_string r.tm_wday) ^ "\n" ^ + "tm_yday = " ^ (to_string r.tm_yday) ^ "\n" ^ + "tm_isdst = " ^ (to_string r.tm_isdst) ^ "\n" ^ + "}\n") +} + +instance printable_unix_interval_timer : printable FStar.Unix.interval_timer = +{ + to_string = (fun i -> + match i with + | ITIMER_REAL -> "ITIMER_REAL" + | ITIMER_VIRTUAL -> "ITIMER_VIRTUAL" + | ITIMER_PROF -> "ITIMER_PROF") +} + +instance printable_unix_interval_timer_status : printable FStar.Unix.interval_timer_status = +{ + to_string = (fun r -> + "{\n" ^ + "it_interval = " ^ (to_string r.it_interval) ^ "\n" ^ + "it_value = " ^ (to_string r.it_value) ^ "\n" ^ + "}\n") +} + +instance printable_unix_passwd_entry : printable FStar.Unix.passwd_entry = +{ + to_string = (fun r -> + "pw_name = " ^ (to_string r.pw_name) ^ "\n" ^ + "pw_passwd = " ^ (to_string r.pw_passwd) ^ "\n" ^ + "pw_uid = " ^ (to_string r.pw_uid) ^ "\n" ^ + "pw_gid = " ^ (to_string r.pw_gid) ^ "\n" ^ + "pw_gecos = " ^ (to_string r.pw_gecos) ^ "\n" ^ + "pw_dir = " ^ (to_string r.pw_dir) ^ "\n" ^ + "pw_shell = " ^ (to_string r.pw_shell) ^ "\n" ^ + "}\n") +} + +instance printable_unix_group_entry : printable FStar.Unix.group_entry = +{ + to_string = (fun r -> + "{\n" ^ + "gr_name = " ^ (to_string r.gr_name) ^ "\n" ^ + "gr_passwd = " ^ (to_string r.gr_passwd) ^ "\n" ^ + "gr_gid = " ^ (to_string r.gr_gid) ^ "\n" ^ + "gr_mem = " ^ (to_string r.gr_mem) ^ "\n" ^ + "}\n") +} + +instance printable_unix_socket_domain : printable FStar.Unix.socket_domain = +{ + to_string = (fun s -> + match s with + | PF_UNIX -> "PF_UNIX" + | PF_INET -> "PF_INET" + | PF_INET6 -> "PF_INET6") +} + +instance printable_unix_socket_type : printable FStar.Unix.socket_type = +{ + to_string = (fun s -> + match s with + | SOCK_STREAM -> "SOCK_STREAM" + | SOCK_DGRAM -> "SOCK_DGRAM" + | SOCK_RAW -> "SOCK_RAW" + | SOCK_SEQPACKET -> "SOCK_SEQPACKET") +} + +instance printable_inet_addr : printable FStar.Unix.inet_addr = +{ + to_string = (fun ia -> "inet_adder is abstract") +} + +instance printable_unix_sockaddr : printable FStar.Unix.sockaddr = +{ + to_string = (fun s -> + match s with + | ADDR_UNIX s -> "ADDR_UNIX " ^ (to_string s) + | ADDR_INET (a,i) -> "ADDR_INET " ^ (to_string a) ^ " " ^ (to_string i)) +} + +instance printable_unix_shutdown_command : printable FStar.Unix.shutdown_command = +{ + to_string = (fun s -> + match s with + | SHUTDOWN_RECEIVE -> "SHUTDOWN_RECEIVE" + | SHUTDOWN_SEND -> "SHUTDOWN_SEND" + | SHUTDOWN_ALL -> "SHUTDOWN_ALL") +} + + +instance printable_unix_msg_flag : printable FStar.Unix.msg_flag = +{ + to_string = (fun m -> + match m with + | MSG_OOB -> "MSG_OOB" + | MSG_DONTROUTE -> "MSG_DONTROUTE" + | MSG_PEEK -> "MSG_PEEK") +} + +instance printable_unix_socket_bool_option : printable FStar.Unix.socket_bool_option = +{ + to_string = (fun s -> + match s with + | SO_DEBUG -> "SO_DEBUG" + | SO_BROADCAST -> "SO_BROADCAST" + | SO_REUSEADDR -> "SO_REUSEADDR" + | SO_KEEPALIVE -> "SO_KEEPALIVE" + | SO_DONTROUTE -> "SO_DONTROUTE" + | SO_OOBINLINE -> "SO_OOBINLINE" + | SO_ACCEPTCONN -> "SO_ACCEPTCONN" + | TCP_NODELAY -> "TCP_NODELAY" + | IPV6_ONLY -> "IPV6_ONLY" + | SO_REUSEPORT -> "SO_REUSEPORT") +} + + +instance printable_unix_socket_int_option : printable FStar.Unix.socket_int_option = +{ + to_string = (fun s -> + match s with + | SO_SNDBUF -> "SO_SNDBUF" + | SO_RCVBUF -> "SO_RCVBUF" + | SO_ERROR -> "SO_ERROR" + | SO_TYPE -> "SO_TYPE" + | SO_RCVLOWAT -> "SO_RCVLOWAT" + | SO_SNDLOWAT -> "SO_SNDLOWAT") +} + +instance printable_unix_socket_optint_option : printable FStar.Unix.socket_optint_option = +{ + to_string = (fun s -> + match s with + | SO_LINGER -> "SO_LINGER") +} + +instance printable_unix_socket_float_option : printable FStar.Unix.socket_float_option = +{ + to_string = (fun s -> + match s with + | SO_RCVTIMEO -> "SO_RCVTIMEO" + | SO_SNDTIMEO -> "SO_SNDTIMEO") +} + +instance printable_unix_host_entry : printable FStar.Unix.host_entry = +{ + to_string = (fun r -> + "{\n" ^ + "h_name = " ^ (to_string r.h_name) ^ "\n" ^ + "h_aliases = " ^ (to_string r.h_aliases) ^ "\n" ^ + "h_addrtype = " ^ (to_string r.h_addrtype) ^ "\n" ^ + "h_addr_list = " ^ (to_string r.h_addr_list) ^ "\n" ^ + "}\n") +} + +instance printable_unix_protocol_entry : printable FStar.Unix.protocol_entry = +{ + to_string = (fun r -> + "{\n" ^ + "p_name = " ^ (to_string r.p_name) ^ "\n" ^ + "p_aliases = " ^ (to_string r.p_aliases) ^ "\n" ^ +(* "p_proto = " ^ (to_string r.p_proto) ^*) "\n" ^ + "}\n" +) +} + +instance printable_unix_service_entry : printable FStar.Unix.service_entry = +{ + to_string = (fun r -> + "{\n" ^ + "s_name = " ^ (to_string r.s_name) ^ "\n" ^ + "s_aliases = " ^ (to_string r.s_aliases) ^ "\n" ^ +(* "s_port = " ^ (to_string r.s_port) ^ *) "\n" ^ + "s_proto = " ^ (to_string r.s_proto) ^ "\n" ^ + "}\n") +} + +instance printable_unix_addr_info : printable FStar.Unix.addr_info = +{ + to_string = (fun r -> + "{\n" ^ + "ai_family = " ^ (to_string r.ai_family) ^ "\n" ^ + "ai_socktype = " ^ (to_string r.ai_socktype) ^ "\n" ^ +(* "ai_protocol = " ^ (to_string r.ai_protocol) ^ "\n" ^ *) + "ai_addr = " ^ (to_string r.ai_addr) ^ "\n" ^ + "ai_canonname = " ^ (to_string r.ai_canonname) ^ "\n" ^ + "}\n") +} + +instance printable_unix_getaddrinfo_option : printable FStar.Unix.getaddrinfo_option = +{ + to_string = (fun g -> + match g with + | AI_FAMILY sd -> "AI_FAMILY " ^ (to_string sd) + | AI_SOCKTYPE st -> "AI_SOCKTYPE " ^ (to_string st) + | AI_PROTOCOL i -> "AI_PROTOCOL " ^ (to_string i) + | AI_NUMERICHOST -> "AI_NUMERICHOST" + | AI_CANONNAME -> "AI_CANONNAME" + | AI_PASSIVE -> "AI_PASSIVE") +} + +instance printable_unix_name_info : printable FStar.Unix.name_info = +{ + to_string = (fun r -> + "{\n" ^ + "ni_hostname = " ^ (to_string r.ni_hostname) ^ "\n" ^ + "ni_service = " ^ (to_string r.ni_service) ^ "\n" ^ + "}\n") +} + +instance printable_unix_getnameinfo_option : printable FStar.Unix.getnameinfo_option = +{ + to_string = (fun g -> + match g with + | NI_NOFQDN -> "NI_NOFQDN" + | NI_NUMERICHOST -> "NI_NUMERICHOST" + | NI_NAMEREQD -> "NI_NAMEREQD" + | NI_NUMERICSERV -> "NI_NUMERICSERV" + | NI_DGRAM -> "NI_DGRAM") +} + +instance printable_unix_terminal_io : printable FStar.Unix.terminal_io = +{ + to_string = (fun r -> + "{\n" ^ + "c_ignbrk = " ^ (to_string r.c_ignbrk) ^ "\n" ^ + "c_brkint = " ^ (to_string r.c_brkint) ^ "\n" ^ + "c_ignpar = " ^ (to_string r.c_ignpar) ^ "\n" ^ + "c_parmrk = " ^ (to_string r.c_parmrk) ^ "\n" ^ + "c_inpck = " ^ (to_string r.c_inpck) ^ "\n" ^ + "c_istrip = " ^ (to_string r.c_istrip) ^ "\n" ^ + "c_inlcr = " ^ (to_string r.c_inlcr) ^ "\n" ^ + "c_igncr = " ^ (to_string r.c_igncr) ^ "\n" ^ + "c_icrnl = " ^ (to_string r.c_icrnl) ^ "\n" ^ + "c_ixon = " ^ (to_string r.c_ixon) ^ "\n" ^ + "c_ixoff = " ^ (to_string r.c_ixoff) ^ "\n" ^ + "c_opost = " ^ (to_string r.c_opost) ^ "\n" ^ + "c_obaud = " ^ (to_string r.c_obaud) ^ "\n" ^ + "c_ibaud = " ^ (to_string r.c_ibaud) ^ "\n" ^ + "c_csize = " ^ (to_string r.c_csize) ^ "\n" ^ + "c_cstopb = " ^ (to_string r.c_cstopb) ^ "\n" ^ + "c_cread = " ^ (to_string r.c_cread) ^ "\n" ^ + "c_parenb = " ^ (to_string r.c_parenb) ^ "\n" ^ + "c_parodd = " ^ (to_string r.c_parodd) ^ "\n" ^ + "c_hupcl = " ^ (to_string r.c_hupcl) ^ "\n" ^ + "c_clocal = " ^ (to_string r.c_clocal) ^ "\n" ^ + "c_isig = " ^ (to_string r.c_isig) ^ "\n" ^ + "c_icanon = " ^ (to_string r.c_icanon) ^ "\n" ^ + "c_noflsh = " ^ (to_string r.c_noflsh) ^ "\n" ^ + "c_echo = " ^ (to_string r.c_echo) ^ "\n" ^ + "c_echoe = " ^ (to_string r.c_echoe) ^ "\n" ^ + "c_echok = " ^ (to_string r.c_echok) ^ "\n" ^ + "c_echonl = " ^ (to_string r.c_echonl) ^ "\n" ^ +(* BUG Is this a printables issue or mine? + "c_vintr = " ^ (to_string r.c_vintr) ^ "\n" ^ + "c_vquit = " ^ (to_string r.c_vquit) ^ "\n" ^ + + "c_verase = " ^ (to_string r.c_verase) ^ "\n" ^ + "c_vkill = " ^ (to_string r.c_vkill) ^ "\n" ^ + "c_veof = " ^ (to_string r.c_veof) ^ "\n" ^ + "c_veol = " ^ (to_string r.c_veol) ^ "\n" ^ + "c_vmin = " ^ (to_string r.c_vmin) ^ "\n" ^ + "c_vtime = " ^ (to_string r.c_vtime) ^ "\n" ^ + "c_vstart = " ^ (to_string r.c_vstart) ^ "\n" ^ + "c_vstop = " ^ (to_string r.c_vstop) ^ "\n" ^ +*) + "}\n") +} + +instance printable_unix_setattr_when : printable FStar.Unix.setattr_when = +{ + to_string = (fun s -> + match s with + | TCSANOW -> "TCSANOW" + | TCSADRAIN -> "TCSADRAIN" + | TCSAFLUSH -> "TCSAFLUSH") +} + +instance printable_unix_flush_queue : printable FStar.Unix.flush_queue = +{ + to_string = (fun f -> + match f with + | TCIFLUSH -> "TCIFLUSH" + | TCOFLUSH -> "TCOFLUSH" + | TCIOFLUSH -> "TCIOFLUSH") +} + +instance printable_unix_flow_action : printable FStar.Unix.flow_action = +{ + to_string = (fun f -> + match f with + | TCOOFF -> "TCOOFF" + | TCOON -> "TCOON" + | TCIOFF -> "TCIOFF" + | TCION -> "TCION") +} diff --git a/ulib/FStar.Class.Printable.fst b/ulib/FStar.Class.Printable.fst index 8f781012915..ccae7f2b72e 100644 --- a/ulib/FStar.Class.Printable.fst +++ b/ulib/FStar.Class.Printable.fst @@ -21,6 +21,7 @@ module FStar.Class.Printable open FStar.String open FStar.Seq.Properties + class printable (a:Type) = { to_string : a -> string @@ -85,19 +86,6 @@ instance printable_char : printable FStar.Char.char = to_string = string_of_char } -(* Floats are not yet well implemented, so these are placeholders.*) -(* -instance printable_float : printable FStar.Float.float = -{ - to_string = FStar.Float.to_string -} - -instance printable_double : printable FStar.Float.double = -{ - to_string = FStar.Float.to_string -} -*) - instance printable_byte : printable FStar.UInt8.byte = { to_string = FStar.UInt8.to_string @@ -264,3 +252,31 @@ instance printable_seq (#b:Type) (x:printable b) : printable (Seq.seq b) = FStar.String.concat "; " (Seq.seq_to_list strings_of_b) ^ ">") } + +instance printable_float : printable FStar.Float.float = +{ + to_string = (fun f -> "#float") +} + +instance printable_double : printable FStar.Float.double = +{ + to_string = (fun d -> "#double") +} + +module IA = FStar.ImmutableArray +module IAB = FStar.ImmutableArray.Base + +instance printable_array (#a: Type) (b : printable a) : printable (IAB.t a) = +{ + to_string = (fun a -> + let l = IA.to_list a in + let ss = List.Tot.map to_string l in + "|[" ^ + (FStar.String.concat "; " ss) + ^ "]|") +} + +instance printable_char_code : printable FStar.Char.char_code = +{ + to_string = (fun (cc: FStar.Char.char_code) -> FStar.UInt32.to_string cc) +} diff --git a/ulib/FStar.FDString.fst b/ulib/FStar.FDString.fst new file mode 100644 index 00000000000..4b3171ecfce --- /dev/null +++ b/ulib/FStar.FDString.fst @@ -0,0 +1,54 @@ +(* + Copyright 2024 Microsoft Research + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. + + Authors: Brian G. Milnes +*) + +/// A file descriptor for a string file, useful for test. +module FStar.FDString + +open FStar.List.Tot +open FStar.All + +type fd_string : eqtype = list string +type fd_string_read = fd_string +type fd_string_write = fd_string + +let open_read_file () = [] +let open_write_file () = [] +let close_read_file fdsr = () +let close_write_file fdsw = () + +let print_newline fdsw = "\n"::fdsw +let print_string fdsw s = s::fdsw + +let input_line fdsr = + match fdsr with + | [] -> raise FStar.IO.EOF + | h::t -> (h,t) + +let read_line fdsr = + match fdsr with + | [] -> raise FStar.IO.EOF + | h::t -> (h,t) + +let write_string fdsw s = s::fdsw + +let fd_write_to_fd_read fdsw = rev fdsw + +let fd_write_to_string fdsw = + let fdsr = fd_write_to_fd_read fdsw in + fold_right (^) (rev fdsw) "" + diff --git a/ulib/FStar.FDString.fsti b/ulib/FStar.FDString.fsti new file mode 100644 index 00000000000..6a44b4abd39 --- /dev/null +++ b/ulib/FStar.FDString.fsti @@ -0,0 +1,45 @@ +(* + Copyright 2024 Microsoft Research + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. + + Authors: Brian G. Milnes +*) + +module FStar.FDString + +(* Although this works nicely, one must thread the non-mutable fd_strings + through the code. A mutable one would be much nicer. +*) + +open FStar.All + +new val fd_string : eqtype +new val fd_string_read : eqtype +new val fd_string_write : eqtype + +val open_read_file : unit -> fd_string_read +val open_write_file : unit -> fd_string_write +val close_read_file : fd_string_read -> unit +val close_write_file : fd_string_write -> unit + +val print_newline : fd_string_write -> fd_string_write +val print_string : fd_string_write -> string -> fd_string_write + +val input_line : fd_string_read -> ML (string & fd_string_read) +val read_line : fd_string_read -> ML (string & fd_string_read) +val write_string : fd_string_write -> string -> fd_string_write + +val fd_write_to_fd_read : fd_string_write -> fd_string_read +val fd_write_to_string : fd_string_write -> string + diff --git a/ulib/FStar.In_Channel.fsti b/ulib/FStar.In_Channel.fsti new file mode 100644 index 00000000000..1b53dfdb788 --- /dev/null +++ b/ulib/FStar.In_Channel.fsti @@ -0,0 +1,53 @@ +(* + Copyright 2024 Microsoft Research + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. + + Authors: Brian G. Milnes +*) + +(* Wrapper of OCaml in_channel.mli minimized code, see the OCaml 4.14 library for docs. *) +module FStar.In_Channel +open FStar.Char +open FStar.Bytes +open FStar.All + +assume new type t + +type open_flag = | Open_rdonly | Open_wronly | Open_append | Open_creat | Open_trunc + | Open_excl | Open_binary | Open_text | Open_nonblock + +// Where OCaml specifies int, we send an int and F* annoying converts it to Z.t +// Where OCaml specifies int64, we and an UInt64 and OCaml gets it as an int64. +// Strings match nicely. Single chars may be being corrupted. + +val stdin : t +val open_bin : string -> ML t +val open_text : string -> ML t +val open_gen : list open_flag -> FStar.UInt64.t -> string -> ML t +val with_open_bin : string -> (t -> 'a) -> ML 'a +val with_open_text : string -> (t -> 'a) -> ML 'a +val with_open_gen : list open_flag -> FStar.UInt64.t -> string -> (t -> 'a) -> ML 'a +val seek : t -> FStar.UInt64.t -> ML unit +val pos : t -> ML FStar.UInt64.t +val length : t -> ML FStar.UInt64.t +val close : t -> ML unit +val close_noerr : t -> ML unit +val input_char : t -> ML (option char) +val input_byte : t -> ML (option byte) +val input_line : t -> ML (option string) +val input : t -> int -> int -> ML (int & FStar.Bytes.bytes) +val really_input : t -> bytes -> FStar.UInt64.t -> FStar.UInt64.t -> ML (option unit) +val really_input_string : t -> FStar.UInt64.t -> ML (option string) +val input_all : t -> ML string +val set_binary_mode : t -> bool -> ML unit diff --git a/ulib/FStar.Out_Channel.fsti b/ulib/FStar.Out_Channel.fsti new file mode 100644 index 00000000000..49ff0ff747f --- /dev/null +++ b/ulib/FStar.Out_Channel.fsti @@ -0,0 +1,59 @@ +(* + Copyright 2024 Microsoft Research + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. + + Authors: Brian G. Milnes +*) + +(* Wrapper of OCaml out_channel.mli minimized code, see the OCaml library for docs. *) +module FStar.Out_Channel +open FStar.Char +open FStar.Bytes +open FStar.All + +type int64 = FStar.Int64.t + +assume new type t +type open_flag = | Open_rdonly | Open_wronly | Open_append | Open_creat | Open_trunc + | Open_excl | Open_binary | Open_text | Open_nonblock + +val stdout : t +val stderr : t +val open_bin : string -> ML t +val open_text : string -> ML t +val open_gen : list open_flag -> int -> string -> ML t +val with_open_bin : string -> (t -> 'a) -> ML 'a +val with_open_text : string -> (t -> 'a) -> ML 'a +val with_open_gen : list open_flag -> int -> string -> (t -> 'a) -> ML 'a +val close : t -> ML unit +val close_noerr : t -> ML unit +val output_char : t -> int -> ML unit +val output_byte : t -> int -> ML unit +val output_string : t -> string -> ML unit +val output_bytes : t -> bytes -> ML unit +val output : t -> bytes -> int -> int -> ML unit +val output_substring : t -> string -> int -> int -> ML unit +val flush : t -> ML unit +val flush_all : unit -> ML unit +val seek : t -> int64 -> ML unit +val pos : t -> ML int64 +val length : t -> ML int64 +val set_binary_mode : t -> bool -> ML unit +val set_buffered : t -> bool -> ML unit +val is_buffered : t -> ML bool + +(* Not in this OCaml revision amazingly. +val isatty : t -> bool +val is_binary_mode : t -> bool +*) diff --git a/ulib/FStar.Unix.fsti b/ulib/FStar.Unix.fsti new file mode 100644 index 00000000000..b11aba68bc4 --- /dev/null +++ b/ulib/FStar.Unix.fsti @@ -0,0 +1,494 @@ +(* + Copyright 2024 Microsoft Research + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. + + Authors: Brian G. Milnes +*) + +(* Wrapper of OCaml unix.mli minimized code, see the OCaml library for docs. *) + +module FStar.Unix +open FStar.Char +open FStar.Bytes +open FStar.Float +open FStar.All + +module IA = FStar.ImmutableArray +module IAB = FStar.ImmutableArray.Base + +module IC = FStar.In_Channel +type in_channel = IC.t + +module OC = FStar.Out_Channel +type out_channel = OC.t + +type error = + | E2BIG + | EACCES + | EAGAIN + | EBADF + | EBUSY + | ECHILD + | EDEADLK + | EDOM + | EEXIST + | EFAULT + | EFBIG + | EINTR + | EINVAL + | EIO + | EISDIR + | EMFILE + | EMLINK + | ENAMETOOLONG + | ENFILE + | ENODEV + | ENOENT + | ENOEXEC + | ENOLCK + | ENOMEM + | ENOSPC + | ENOSYS + | ENOTDIR + | ENOTEMPTY + | ENOTTY + | ENXIO + | EPERM + | EPIPE + | ERANGE + | EROFS + | ESPIPE + | ESRCH + | EXDEV + | EWOULDBLOCK + | EINPROGRESS + | EALREADY + | ENOTSOCK + | EDESTADDRREQ + | EMSGSIZE + | EPROTOTYPE + | ENOPROTOOPT + | EPROTONOSUPPORT + | ESOCKTNOSUPPORT + | EOPNOTSUPP + | EPFNOSUPPORT + | EAFNOSUPPORT + | EADDRINUSE + | EADDRNOTAVAIL + | ENETDOWN + | ENETUNREACH + | ENETRESET + | ECONNABORTED + | ECONNRESET + | ENOBUFS + | EISCONN + | ENOTCONN + | ESHUTDOWN + | ETOOMANYREFS + | ETIMEDOUT + | ECONNREFUSED + | EHOSTDOWN + | EHOSTUNREACH + | ELOOP + | EOVERFLOW + | EUNKNOWNERR of int + +exception Unix_error of error * string * string +val error_message : error -> ML string +val handle_unix_error : ('a -> 'b) -> 'a -> ML 'b +val environment : unit -> ML (IAB.t string) +val unsafe_environment : unit -> ML (IAB.t string) +val getenv : string -> ML string +val unsafe_getenv : string -> ML string +val putenv : string -> string -> ML unit +type process_status = + | WEXITED of int + | WSIGNALED of int + | WSTOPPED of int + +type wait_flag = + | WNOHANG + | WUNTRACED +val execv : string -> IAB.t string -> ML 'a +val execve : string -> IAB.t string -> IAB.t string -> ML 'a +val execvp : string -> IAB.t string -> ML 'a +val execvpe : string -> IAB.t string -> IAB.t string -> ML 'a +val fork : unit -> ML int +val wait : unit -> ML (int * process_status) +val waitpid : list wait_flag -> int -> ML (int * process_status) +val system : string -> ML process_status +val _exit : int -> ML 'a +val getpid : unit -> ML int +val getppid : unit -> ML int +val nice : int -> ML int +assume new type file_descr +val stdin : file_descr +val stdout : file_descr +val stderr : file_descr +type open_flag = + | O_RDONLY + | O_WRONLY + | O_RDWR + | O_NONBLOCK + | O_APPEND + | O_CREAT + | O_TRUNC + | O_EXCL + | O_NOCTTY + | O_DSYNC + | O_SYNC + | O_RSYNC + | O_SHARE_DELETE + | O_CLOEXEC + | O_KEEPEXEC + +type file_perm = int +val openfile : string -> list open_flag -> file_perm -> ML file_descr +val close : file_descr -> ML unit +val fsync : file_descr -> ML unit +val read : file_descr -> bytes -> int -> int -> ML int +val write : file_descr -> bytes -> int -> int -> ML int +val single_write : file_descr -> bytes -> int -> int -> ML int +val write_substring : file_descr -> string -> int -> int -> ML int +val single_write_substring : + file_descr -> string -> int -> int -> ML int +val in_channel_of_descr : file_descr -> ML in_channel +val out_channel_of_descr : file_descr -> ML out_channel +val descr_of_in_channel : in_channel -> ML file_descr +val descr_of_out_channel : out_channel -> ML file_descr +type seek_command = | SEEK_SET | SEEK_CUR | SEEK_END +val lseek : file_descr -> int -> seek_command -> ML int +val truncate : string -> int -> ML unit +val ftruncate : file_descr -> int -> ML unit +type file_kind = | S_REG | S_DIR | S_CHR | S_BLK | S_LNK | S_FIFO + | S_SOCK +noeq type stats = + { st_dev : int; + st_ino : int; + st_kind : file_kind; + st_perm : file_perm; + st_nlink : int; + st_uid : int; + st_gid : int; + st_rdev : int; + st_size : int; + st_atime : float; + st_mtime : float; + st_ctime : float; + } + +val stat : string -> ML stats +val lstat : string -> ML stats +val fstat : file_descr -> ML stats +val isatty : file_descr -> ML bool +val unlink : string -> ML unit +val rename : string -> string -> ML unit +val link : string -> string -> ML unit +val realpath : string -> ML string +type access_permission = | R_OK | W_OK | X_OK | F_OK +val chmod : string -> file_perm -> ML unit +val fchmod : file_descr -> file_perm -> ML unit +val chown : string -> int -> int -> ML unit +val fchown : file_descr -> int -> int -> ML unit +val umask : file_perm -> ML file_perm +val access : string -> list access_permission -> ML unit +val dup : file_descr -> ML file_descr +val dup2 : file_descr -> file_descr -> ML unit +val set_nonblock : file_descr -> ML unit +val clear_nonblock : file_descr -> ML unit +val set_close_on_exec : file_descr -> ML unit +val clear_close_on_exec : file_descr -> ML unit +val mkdir : string -> file_perm -> ML unit +val rmdir : string -> ML unit +val chdir : string -> ML unit +val getcwd : unit -> ML string +val chroot : string -> ML unit + +assume new type dir_handle +val opendir : string -> ML dir_handle +val readdir : dir_handle -> ML string +val rewinddir : dir_handle -> ML unit +val closedir : dir_handle -> ML unit +val pipe : unit -> ML (file_descr * file_descr) +val mkfifo : string -> file_perm -> ML unit +val create_process : string -> IAB.t string -> file_descr -> file_descr -> file_descr -> ML int +val create_process_env : + string -> IAB.t string -> IAB.t string -> file_descr -> + file_descr -> file_descr -> ML int +val open_process_in : string -> ML in_channel +val open_process_out : string -> ML out_channel +val open_process : string -> ML (in_channel * out_channel) +val open_process_full : + string -> IAB.t string -> ML (in_channel * out_channel * in_channel) +val open_process_args : string -> IAB.t string -> ML (in_channel * out_channel) +val open_process_args_in : string -> IAB.t string -> ML in_channel +val open_process_args_out : string -> IAB.t string -> ML out_channel +val open_process_args_full : + string -> IAB.t string -> IAB.t string -> ML (in_channel * out_channel * in_channel) +val process_in_pid : in_channel -> ML int +val process_out_pid : out_channel -> ML int +val process_pid : in_channel * out_channel -> ML int +val process_full_pid : in_channel * out_channel * in_channel -> ML int +val close_process_in : in_channel -> ML process_status +val close_process_out : out_channel -> ML process_status +val close_process : in_channel * out_channel -> ML process_status +val close_process_full : + in_channel * out_channel * in_channel -> ML process_status +val symlink : string -> string -> ML unit +val has_symlink : unit -> ML bool +val readlink : string -> ML string +val select : list file_descr -> list file_descr -> list file_descr -> + float -> ML (list file_descr * list file_descr * list file_descr) +type lock_command = | F_ULOCK | F_LOCK | F_TLOCK | F_TEST + | F_RLOCK | F_TRLOCK +val lockf : file_descr -> lock_command -> int -> ML unit +val kill : int -> int -> ML unit + +type sigprocmask_command = | SIG_SETMASK | SIG_BLOCK | SIG_UNBLOCK +val sigprocmask : sigprocmask_command -> list int -> ML (list int) +val sigpending : unit -> ML (list int) +val sigsuspend : list int -> ML unit +val pause : unit -> ML unit +val sigwait : list int -> ML int + +noeq type process_times = + { tms_utime : float; + tms_stime : float; + tms_cutime : float; + tms_cstime : float; + } + +type tm = + { tm_sec : int; + tm_min : int; + tm_hour : int; + tm_mday : int; + tm_mon : int; + tm_year : int; + tm_wday : int; + tm_yday : int; + tm_isdst : bool; + } +val time : unit -> ML float +val gettimeofday : unit -> ML float +val gmtime : float -> ML tm +val localtime : float -> ML tm +val mktime : tm -> ML (float * tm) +val alarm : int -> ML int +val sleep : int -> ML unit +val sleepf : float -> ML unit +val times : unit -> ML process_times +val utimes : string -> float -> float -> ML unit + +type interval_timer = | ITIMER_REAL | ITIMER_VIRTUAL | ITIMER_PROF + +noeq type interval_timer_status = + { it_interval : float; + it_value : float; + } +val getitimer : interval_timer -> ML interval_timer_status +val setitimer : interval_timer -> interval_timer_status -> ML interval_timer_status +val getuid : unit -> ML int +val geteuid : unit -> ML int +val setuid : int -> ML unit +val getgid : unit -> ML int +val getegid : unit -> ML int +val setgid : int -> ML unit +val getgroups : unit -> ML (IAB.t int) +val setgroups : IAB.t int -> ML unit +val initgroups : string -> int -> ML unit + +type passwd_entry = + { pw_name : string; + pw_passwd : string; + pw_uid : int; + pw_gid : int; + pw_gecos : string; + pw_dir : string; + pw_shell : string + } + +noeq type group_entry = + { gr_name : string; + gr_passwd : string; + gr_gid : int; + gr_mem : IAB.t string + } +val getlogin : unit -> ML string +val getpwnam : string -> ML passwd_entry +val getgrnam : string -> ML group_entry +val getpwuid : int -> ML passwd_entry +val getgrgid : int -> ML group_entry + +assume new type inet_addr +val inet_addr_of_string : string -> ML inet_addr +val string_of_inet_addr : inet_addr -> ML string +val inet_addr_any : inet_addr +val inet_addr_loopback : inet_addr +val inet6_addr_any : inet_addr +val inet6_addr_loopback : inet_addr +val is_inet6_addr : inet_addr -> ML bool + +type socket_domain = | PF_UNIX | PF_INET | PF_INET6 + +type socket_type = | SOCK_STREAM | SOCK_DGRAM | SOCK_RAW | SOCK_SEQPACKET + +noeq type sockaddr = | ADDR_UNIX of string | ADDR_INET of inet_addr * int +val socket : bool -> socket_domain -> socket_type -> int -> ML file_descr +val domain_of_sockaddr: sockaddr -> ML socket_domain +val socketpair : socket_domain -> socket_type -> int -> ML (file_descr * file_descr) +val accept : file_descr -> ML (file_descr * sockaddr) +val bind : file_descr -> sockaddr -> ML unit +val connect : file_descr -> sockaddr -> ML unit +val listen : file_descr -> int -> ML unit + +type shutdown_command = | SHUTDOWN_RECEIVE | SHUTDOWN_SEND | SHUTDOWN_ALL +val shutdown : file_descr -> shutdown_command -> ML unit +val getsockname : file_descr -> ML sockaddr +val getpeername : file_descr -> ML sockaddr +type msg_flag = | MSG_OOB | MSG_DONTROUTE | MSG_PEEK +val recv : file_descr -> bytes -> int -> int -> list msg_flag -> ML int +val recvfrom : file_descr -> bytes -> int -> int -> list msg_flag -> ML (int * sockaddr) +val send : file_descr -> bytes -> int -> int -> list msg_flag -> ML int +val send_substring : file_descr -> string -> int -> int -> list msg_flag -> ML int +val sendto : file_descr -> bytes -> int -> int -> list msg_flag -> sockaddr -> ML int +val sendto_substring : file_descr -> string -> int -> int -> list msg_flag -> sockaddr -> ML int + +type socket_bool_option = | SO_DEBUG | SO_BROADCAST | SO_REUSEADDR | SO_KEEPALIVE + | SO_DONTROUTE | SO_OOBINLINE | SO_ACCEPTCONN | TCP_NODELAY | IPV6_ONLY + | SO_REUSEPORT + +type socket_int_option = | SO_SNDBUF | SO_RCVBUF | SO_ERROR | SO_TYPE + | SO_RCVLOWAT | SO_SNDLOWAT + +type socket_optint_option = | SO_LINGER +type socket_float_option = | SO_RCVTIMEO | SO_SNDTIMEO +val getsockopt : file_descr -> socket_bool_option -> ML bool +val setsockopt : file_descr -> socket_bool_option -> bool -> ML unit +val getsockopt_int : file_descr -> socket_int_option -> ML int +val setsockopt_int : file_descr -> socket_int_option -> int -> ML unit +val getsockopt_optint : file_descr -> socket_optint_option -> ML (option int) +val setsockopt_optint : file_descr -> socket_optint_option -> option int -> ML unit +val getsockopt_float : file_descr -> socket_float_option -> ML float +val setsockopt_float : file_descr -> socket_float_option -> float -> ML unit +val getsockopt_error : file_descr -> ML (option error) +val open_connection : sockaddr -> ML (in_channel * out_channel) +val shutdown_connection : in_channel -> ML unit +val establish_server : (in_channel -> out_channel -> unit) -> sockaddr -> ML unit + +noeq type host_entry = + { h_name : string; + h_aliases : IAB.t string; + h_addrtype : socket_domain; + h_addr_list : IAB.t inet_addr + } + +noeq type protocol_entry = + { p_name : string; + p_aliases : IAB.t string; + p_proto : int + } + +noeq type service_entry = + { s_name : string; + s_aliases : IAB.t string; + s_port : int; + s_proto : string + } +val gethostname : unit -> ML string +val gethostbyname : string -> ML host_entry +val gethostbyaddr : inet_addr -> ML host_entry +val getprotobyname : string -> ML protocol_entry +val getprotobynumber : int -> ML protocol_entry +val getservbyname : string -> string -> ML service_entry +val getservbyport : int -> string -> ML service_entry + +noeq type addr_info = + { ai_family : socket_domain; + ai_socktype : socket_type; + ai_protocol : int; + ai_addr : sockaddr; + ai_canonname : string + } + +type getaddrinfo_option = + | AI_FAMILY of socket_domain + | AI_SOCKTYPE of socket_type + | AI_PROTOCOL of int + | AI_NUMERICHOST + | AI_CANONNAME + | AI_PASSIVE + +val getaddrinfo: string -> string -> list getaddrinfo_option -> ML (list addr_info) + +type name_info = + { ni_hostname : string; + ni_service : string; + } + +type getnameinfo_option = | NI_NOFQDN | NI_NUMERICHOST | NI_NAMEREQD | NI_NUMERICSERV + | NI_DGRAM +val getnameinfo : sockaddr -> list getnameinfo_option -> ML name_info +type terminal_io = + { + c_ignbrk : bool; + c_brkint : bool; + c_ignpar : bool; + c_parmrk : bool; + c_inpck : bool; + c_istrip : bool; + c_inlcr : bool; + c_igncr : bool; + c_icrnl : bool; + c_ixon : bool; + c_ixoff : bool; + c_opost : bool; + c_obaud : int; + c_ibaud : int; + c_csize : int; + c_cstopb : int; + c_cread : bool; + c_parenb : bool; + c_parodd : bool; + c_hupcl : bool; + c_clocal : bool; + c_isig : bool; + c_icanon : bool; + c_noflsh : bool; + c_echo : bool; + c_echoe : bool; + c_echok : bool; + c_echonl : bool; + c_vintr : int; + c_vquit : int; + c_verase : int; + c_vkill : int; + c_veof : int; + c_veol : int; + c_vmin : int; + c_vtime : int; + c_vstart : int; + c_vstop : int; + } +val tcgetattr : file_descr -> ML terminal_io +type setattr_when = | TCSANOW | TCSADRAIN | TCSAFLUSH +val tcsetattr : file_descr -> setattr_when -> terminal_io -> ML unit +val tcsendbreak : file_descr -> int -> ML unit +val tcdrain : file_descr -> ML unit + +type flush_queue = | TCIFLUSH | TCOFLUSH | TCIOFLUSH +val tcflush : file_descr -> flush_queue -> ML unit +type flow_action = | TCOOFF | TCOON | TCIOFF | TCION +val tcflow : file_descr -> flow_action -> ML unit +val setsid : unit -> ML int