SimpleIO.IO_Unsafe

Unsafe primitives


From Coq.extraction Require Import
     ExtrOcamlIntConv.

From SimpleIO Require Import
     IO_Stdlib.

Throws an exception if the divisor is 0.
Parameter unsafe_int_div : int -> int -> int.

Throws an exception if the divisor is 0.
Parameter unsafe_int_mod : int -> int -> int.

Throws an exception if the argument is smaller than 0 or greater than 255.
Parameter unsafe_char_of_int : int -> char.

Throws an exception if the argument string does not represent an integer.
Parameter unsafe_int_of_ostring : ocaml_string -> int.

(* N.B.: I am not sure whether these are actually unsafe.
   It depends on what "undefined" means here. It might be fine if
   the result is architecture dependent but still constant. They
   would be really unsafe if the result could change from one
   operation to the next. *)

Logical shift left (treats int as unsigned). Undefined result if shift is negative or greater than int size.
Parameter unsafe_lsl : int -> int -> int.

Logical shift right (treats int as unsigned). Undefined result if shift is negative or greater than int size.
Parameter unsafe_lsr : int -> int -> int.

Arithmetic shift right (replicates the bit sign). Undefined result if shift is negative or greater than int size.
Parameter unsafe_asr : int -> int -> int.

Extract Inlined Constant unsafe_int_div => "Stdlib.(/)".
Extract Inlined Constant unsafe_int_mod => "Stdlib.(mod)".
Extract Inlined Constant unsafe_char_of_int => "Stdlib.char_of_int".
Extract Inlined Constant unsafe_int_of_ostring => "Stdlib.int_of_string".
Extract Inlined Constant unsafe_lsl => "Stdlib.(lsl)".
Extract Inlined Constant unsafe_lsr => "Stdlib.(lsr)".
Extract Inlined Constant unsafe_asr => "Stdlib.(asr)".