OCaml Unix fully wrapped. PR next.

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

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
+

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 *)

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
+*)