SimpleIO.IO_Stdlib

OCaml standard library

Extraction of OCaml's Stdlib module.

This depends on ExtrOcamlBasic and ExtrOcamlIntConv that define extraction for a few basic types (option, list, int). Other types that do not have a natural counterpart in Coq are left abstract. In particular, this module does not assume any particular representation of Coq's string and ascii (as opposed to the RawChar module).

Types

The native string type in OCaml.

Parameter ocaml_string : Type.

Mutable bytestrings.

Parameter bytes : Type.

Floating point values.

Parameter float : Type.

The native char type in OCaml (8 bit integers).

Parameter char : Type.

Input-output channels.

Parameter in_channel : Type.
Parameter out_channel : Type.

Mutable references.

Parameter ref : Type -> Type.

Operations on int

Parameter int_add : int -> int -> int.
Parameter int_sub : int -> int -> int.
Parameter int_mul : int -> int -> int.
Parameter int_div_opt : int -> int -> option int.
Parameter int_mod_opt : int -> int -> option int.
Parameter int_eqb : int -> int -> bool.
Parameter int_neqb : int -> int -> bool.
Parameter int_le : int -> int -> bool.
Parameter int_lt : int -> int -> bool.
Parameter int_min : int -> int -> int.
Parameter int_max : int -> int -> int.

Parameter land : int -> int -> int.
Parameter lor : int -> int -> int.
Parameter lxor : int -> int -> int.
Parameter lnot : int -> int -> int.

Parameter max_int : int.
Parameter min_int : int.

Delimit Scope int_scope with int.
Bind Scope int_scope with int.
Infix "+" := int_add : int_scope.
Infix "-" := int_sub : int_scope.
Infix "*" := int_mul : int_scope.
Infix "<?" := int_lt (at level 70, no associativity) : int_scope.
Infix "<=?" := int_le (at level 70, no associativity) : int_scope.
Infix "=?" := int_eqb (at level 70, no associativity) : int_scope.
Infix "<>?" := int_neqb (at level 70, no associativity) : int_scope.

Strings and char

Append strings.

Parameter ostring_app : ocaml_string -> ocaml_string -> ocaml_string.

Compare strings.

Parameter ostring_eqb : ocaml_string -> ocaml_string -> bool.

Compare characters.

Parameter char_eqb : char -> char -> bool.

Convert a char to an int.

Parameter int_of_char : char -> int.

Convert an int to a char.

Equals None if the argument is greater than 255.

Parameter char_of_int_opt : int -> option char.

Convert an int to a char, in IO.

Throws an Invalid_argument exception if the argument is greater than 255.

Parameter char_of_int_io : int -> IO char.

Return the string representation of a boolean.

Parameter ostring_of_bool : bool -> ocaml_string.

Show an int as an ocaml_string.

Parameter ostring_of_int : int -> ocaml_string.

Parse an ocaml_string into an int.

Parameter int_of_ostring_opt : ocaml_string -> option int.

Notes:

There is no total int_of_ostring. (See IO_Unsafe.unsafe_int_of_ostring.)
Comparisons between mutable structures (bytes, ref) should happen in IO.

Exceptions

Throw an Invalid_argument exception.

Parameter invalid_arg : forall {a}, ocaml_string -> IO a.

Throw a Failure exception.

Parameter failwith : forall {a}, ocaml_string -> IO a.

Standard channels

Parameter stdin : in_channel.
Parameter stdout : out_channel.
Parameter stderr : out_channel.

stdout

Parameter print_char : char -> IO unit.
Parameter print_bytes : bytes -> IO unit.
Parameter print_int : int -> IO unit.
Parameter print_string : ocaml_string -> IO unit.
Parameter print_endline : ocaml_string -> IO unit.
Parameter print_newline : IO unit.

stderr

Parameter prerr_char : char -> IO unit.
Parameter prerr_bytes : bytes -> IO unit.
Parameter prerr_int : int -> IO unit.
Parameter prerr_string : ocaml_string -> IO unit.
Parameter prerr_endline : ocaml_string -> IO unit.
Parameter prerr_newline : IO unit.

stdin

Parameter read_line : IO ocaml_string.
Parameter read_int : IO int.
Parameter read_int_opt : IO (option int).

File handles

Output

Open a file for output.

Parameter open_out : ocaml_string -> IO out_channel.

Close an output file.

Parameter close_out : out_channel -> IO unit.

Same as close_out, but ignore all errors.

Parameter close_out_noerr : out_channel -> IO unit.

Flush output buffers.

Parameter flush : out_channel -> IO unit.
Parameter flush_all : IO unit.

Parameter output_char : out_channel -> char -> IO unit.
Parameter output_string : out_channel -> ocaml_string -> IO unit.
Parameter output_bytes : out_channel -> bytes -> IO unit.
Parameter output_substring : out_channel -> ocaml_string -> int -> int -> IO unit.
Parameter output_byte : out_channel -> int -> IO unit.

Input

Open a file for input.

Parameter open_in : ocaml_string -> IO in_channel.

Close an input file.

Parameter close_in : in_channel -> IO unit.

Same as close_in, but ignore all errors.

Parameter close_in_noerr : in_channel -> IO unit.

Parameter input_char : in_channel -> IO char.
Parameter input_line : in_channel -> IO ocaml_string.

input ic buf pos len reads up to len characters from the given channel ic, storing them in byte sequence buf, starting at character number pos. It returns the actual number of characters read, between 0 and len (inclusive). A return value of 0 means that the end of file was reached. A return value between 0 and len exclusive means that not all requested len characters were read, either because no more characters were available at that time, or because the implementation found it convenient to do a partial read; input must be called again to read the remaining characters, if desired. (See also really_input for reading exactly len characters.) Exception Invalid_argument "input" is raised if pos and len do not designate a valid range of buf.

Parameter input : in_channel -> bytes -> int -> int -> IO int.

really_input ic buf pos len reads len characters from channel ic, storing them in byte sequence buf, starting at character number pos. @raise End_of_file if the end of file is reached before len characters have been read. @raise Invalid_argument if pos and len do not designate a valid range of buf.

Parameter really_input : in_channel -> bytes -> int -> int -> IO unit.

really_input_string ic len reads len characters from channel ic and returns them in a new string. @raise End_of_file if the end of file is reached before len characters have been read.

Parameter really_input_string : in_channel -> int -> IO ocaml_string.

Parameter input_byte : in_channel -> IO int.

Return the size (number of characters) of the regular file on which the given channel is opened. If the channel is opened on a file that is not a regular file, the result is meaningless. The returned size does not take into account the end-of-line translations that can be performed when reading from a channel opened in text mode.

Parameter in_channel_length : in_channel -> IO int.

Mutable references

Parameter new_ref : forall {a}, a -> IO (ref a).
Parameter read_ref : forall {a}, ref a -> IO a.
Parameter write_ref : forall {a}, ref a -> a -> IO unit.
Parameter incr_ref : ref int -> IO unit.
Parameter decr_ref : ref int -> IO unit.

Program termination

Terminate with an exit code. (0 for success.)

Parameter exit : forall {a}, int -> IO a.

Extraction

Types

Extract Inlined Constant ocaml_string => "String.t".
Extract Inlined Constant char => "char".
Extract Inlined Constant float => "float".

Extract Inlined Constant bytes => "bytes".
Extract Inlined Constant in_channel => "Stdlib.in_channel".
Extract Inlined Constant out_channel => "Stdlib.out_channel".
Extract Constant ref "'a" => "'a Stdlib.ref".

Operations on int

Extract Inlined Constant int_add => "Stdlib.(+)".
Extract Inlined Constant int_sub => "Stdlib.(-)".
Extract Inlined Constant int_mul => "Stdlib.( * )".
Extract Inlined Constant int_div_opt =>
"fun x y -> try Some (x Stdlib./ y) with Division_by_zero -> None".
Extract Inlined Constant int_mod_opt =>
"fun x y -> try Some Stdlib.(x mod y) with Division_by_zero -> None".
Extract Inlined Constant int_eqb => "Stdlib.(=)".
Extract Inlined Constant int_neqb => "Stdlib.(<>)".
Extract Inlined Constant int_le => "Stdlib.(<=)".
Extract Inlined Constant int_lt => "Stdlib.(<)".

Extract Inlined Constant int_min => "Stdlib.min".
Extract Inlined Constant int_max => "Stdlib.max".

Extract Inlined Constant land => "Stdlib.(land)".
Extract Inlined Constant lor => "Stdlib.(lor)".
Extract Inlined Constant lxor => "Stdlib.(lxor)".
Extract Inlined Constant lnot => "Stdlib.lnot".

Extract Inlined Constant max_int => "Stdlib.max_int".
Extract Inlined Constant min_int => "Stdlib.min_int".

Misc

Extract Inlined Constant ostring_app => "Stdlib.(^)".

Extract Inlined Constant ostring_eqb => "Stdlib.(=)".
Extract Inlined Constant char_eqb => "Stdlib.(=)".

Extract Inlined Constant int_of_char => "Stdlib.int_of_char".

Extract Constant char_of_int_opt =>
"fun n -> try Some (Stdlib.char_of_int n) with Invalid_argument _ -> None".

Extract Constant char_of_int_io => "fun n k -> k (Stdlib.char_of_int n)".

Extract Constant ostring_of_bool => "Stdlib.string_of_bool".
Extract Inlined Constant ostring_of_int => "Stdlib.string_of_int".
Extract Inlined Constant int_of_ostring_opt => "Stdlib.int_of_string_opt".

Exceptions

Extract Inlined Constant invalid_arg => "Stdlib.invalid_arg".
Extract Inlined Constant failwith => "Stdlib.failwith".

Standard channels

Extract Inlined Constant stdin => "Stdlib.stdin".
Extract Inlined Constant stdout => "Stdlib.stdout".
Extract Inlined Constant stderr => "Stdlib.stderr".

stdout

Extract Constant print_char => "fun c k -> k (Stdlib.print_char c)".
Extract Constant print_bytes => "fun b k -> k (Stdlib.print_bytes b)".
Extract Constant print_int => "fun n k -> k (Stdlib.print_int n)".
Extract Constant print_string => "fun s k -> k (Stdlib.print_string s)".
Extract Constant print_endline => "fun s k -> k (Stdlib.print_endline s)".
Extract Constant print_newline => "fun k -> k (Stdlib.print_newline ())".

stderr

Extract Constant prerr_char => "fun c k -> k (Stdlib.prerr_char c)".
Extract Constant prerr_bytes => "fun bs k -> k (Stdlib.prerr_bytes bs)".
Extract Constant prerr_int => "fun n k -> k (Stdlib.prerr_int n)".
Extract Constant prerr_string => "fun s k -> k (Stdlib.prerr_string s)".
Extract Constant prerr_endline => "fun s k -> k (Stdlib.prerr_endline s)".
Extract Constant prerr_newline => "fun k -> k (Stdlib.prerr_newline ())".

stdin

Extract Constant read_line => "fun k -> k (Stdlib.read_line ())".
Extract Constant read_int => "fun k -> k (Stdlib.read_int ())".
Extract Constant read_int_opt => "fun k -> k (Stdlib.read_int_opt ())".

File handles

Output

Extract Constant open_out => "fun s k -> k (Stdlib.open_out s)".
Extract Constant flush => "fun h k -> k (Stdlib.flush h)".
Extract Constant flush_all => "fun k -> k (Stdlib.flush_all ())".

Extract Constant output_char => "fun h c k -> k (Stdlib.output_char h c)".
Extract Constant output_string => "fun h s k -> k (Stdlib.output_string h s)".
Extract Constant output_bytes => "fun h b k -> k (Stdlib.output_bytes h b)".
Extract Constant output_byte => "fun h b k -> k (Stdlib.output_byte h b)".
Extract Constant output_substring =>
"fun h s i n k -> k (Stdlib.output_substring h s i n)".

Extract Constant close_out => "fun h k -> k (close_out h)".
Extract Constant close_out_noerr => "fun h k -> k (close_out_noerr h)".

Input

Extract Constant open_in => "fun s k -> k (Stdlib.open_in s)".

Extract Constant input_char => "fun h k -> k (Stdlib.input_char h)".
Extract Constant input_line => "fun h k -> k (Stdlib.input_line h)".
Extract Constant input => "fun h b p l k -> k (Stdlib.input h b p l)".
Extract Constant really_input =>
  "fun h b p l k -> k (Stdlib.really_input h b p l)".
Extract Constant really_input_string =>
  "fun h l k -> k (Stdlib.really_input_string h l)".
Extract Constant input_byte => "fun h k -> k (Stdlib.input_byte h)".
Extract Constant in_channel_length =>
  "fun h k -> k (Stdlib.in_channel_length h)".

Extract Constant close_in => "fun h k -> k (Stdlib.close_in h)".
Extract Constant close_in_noerr => "fun h k -> k (Stdlib.close_in_noerr h)".

Mutable references

Extract Constant new_ref =>
  "fun x k -> k (Stdlib.ref x)".
Extract Constant read_ref =>
  "fun r k -> k (Stdlib.(!) r)".
Extract Constant write_ref =>
  "fun r x k -> k (Stdlib.(:=) r x)".
Extract Constant incr_ref => "fun r k -> k (Stdlib.incr r)".
Extract Constant decr_ref => "fun r k -> k (Stdlib.decr r)".

Program termination

Extract Constant exit => "fun n k -> k (Stdlib.exit n)".