Library SimpleIO.IO_Unsafe

From Coq.extraction Require Import
     ExtrOcamlIntConv.

From SimpleIO Require Import
     IO_Pervasives.

Parameter unsafe_int_div : int -> int -> int.
Extract Inlined Constant unsafe_int_div => "Pervasives.(/)".

Parameter unsafe_int_mod : int -> int -> int.
Extract Inlined Constant unsafe_int_mod => "Pervasives.(mod)".

Parameter unsafe_char_of_int : int -> char.
Extract Constant unsafe_char_of_int => "Pervasives.char_of_int".

Parameter unsafe_int_of_ostring : ocaml_string -> int.
Extract Inlined Constant unsafe_int_of_ostring => "Pervasives.int_of_string".


Parameter unsafe_lsl : int -> int -> int.

Parameter unsafe_lsr : int -> int -> int.

Parameter unsafe_asr : int -> int -> int.

Extract Inlined Constant unsafe_lsl => "Pervasives.(lsl)".
Extract Inlined Constant unsafe_lsr => "Pervasives.(lsr)".
Extract Inlined Constant unsafe_asr => "Pervasives.(asr)".