Add more definitions for Stdlib

Author: clarus

proofs/Basics.v

@@ -105,6 +105,8 @@ Definition int64 := Z.
 
 Definition nativeint := Z.
 
+Definition char := ascii.
+
 Definition bytes := string.
 
 Definition try {A : Set} (x : A) : A := x.

proofs/Stdlib.v

@@ -133,17 +133,339 @@ Parameter lsr : int -> int -> int.
 Parameter asr : int -> int -> int.
 
 (** * Floating-point arithmetic *)
+Parameter op_tildeminuspoint : float -> float.
 
+Parameter op_tildepluspoint : float -> float.
+
+Parameter op_pluspoint : float -> float -> float.
+
+Parameter op_minuspoint : float -> float -> float.
+
+Parameter op_timespoint : float -> float -> float.
+
+Parameter op_divpoint : float -> float -> float.
+
+Parameter op_timestimespoint : float -> float -> float.
+
+Parameter sqrt : float -> float.
+
+Parameter exp : float -> float.
+
+Parameter log : float -> float.
+
+Parameter log10 : float -> float.
+
+Parameter expm1 : float -> float.
+
+Parameter log1p : float -> float.
+
+Parameter cos : float -> float.
+
+Parameter sin : float -> float.
+
+Parameter tan : float -> float.
+
+Parameter acos : float -> float.
+
+Parameter asin : float -> float.
+
+Parameter atan : float -> float.
+
+Parameter atan2 : float -> float -> float.
+
+Parameter hypot : float -> float -> float.
+
+Parameter cosh : float -> float.
+
+Parameter sinh : float -> float.
+
+Parameter tanh : float -> float.
+
+Parameter acosh : float -> float.
+
+Parameter asinh : float -> float.
+
+Parameter atanh : float -> float.
+
+Parameter ceil : float -> float.
+
+Parameter floor : float -> float.
+
+Parameter abs_float : float -> float.
+
+Parameter copysign : float -> float -> float.
+
+Parameter mod_float : float -> float -> float.
+
+Parameter frexp : float -> float * int.
+
+Parameter ldexp : float -> int -> float.
+
+Parameter modf : float -> float * float.
+
+Parameter float_value : int -> float.
+
+Parameter float_of_int : int -> float.
+
+Parameter truncate : float -> int.
+
+Parameter int_of_float : float -> int.
+
+Parameter infinity : float.
+
+Parameter neg_infinity : float.
+
+Parameter nan : float.
+
+Parameter max_float : float.
+
+Parameter min_float : float.
+
+Parameter epsilon_float : float.
+
+Inductive fpclass : Set :=
+| FP_normal
+| FP_subnormal
+| FP_zero
+| FP_infinite
+| FP_nan.
+
+Parameter classify_float : float -> fpclass.
 
 (** * String operations *)
+Parameter op_caret : string -> string -> string.
+
 (** * Character operations *)
+Parameter int_of_char : char -> int.
+
+Parameter char_of_int : int -> char.
+
 (** * Unit operations *)
+Definition ignore {a : Set} (_ : a) : unit :=
+  tt.
+
 (** * String conversion functions *)
+Parameter string_of_bool : bool -> string.
+
+Parameter bool_of_string_opt : string -> option bool.
+
+Parameter bool_of_string : string -> bool.
+
+Parameter string_of_int : int -> string.
+
+Parameter int_of_string_opt : string -> option int.
+
+Parameter int_of_string : string -> int.
+
+Parameter string_of_float : float -> string.
+
+Parameter float_of_string_opt : string -> option float.
+
+Parameter float_of_string : string -> float.
+
 (** * Pair operations *)
+Parameter fst : forall {a b : Set}, a * b -> a.
+
+Parameter snd : forall {a b : Set}, a * b -> b.
+
 (** * List operations *)
+Parameter op_at : forall {a : Set}, list a -> list a -> list a.
+
 (** * Input/output *)
+Parameter in_channel : Set.
+
+Parameter out_channel : Set.
+
+Parameter stdin : in_channel.
+
+Parameter stdout : out_channel.
+
+Parameter stderr : out_channel.
+
+(** ** Output functions on standard output *)
+Parameter print_char : char -> unit.
+
+Parameter print_string : string -> unit.
+
+Parameter print_bytes : bytes -> unit.
+
+Parameter print_int : int -> unit.
+
+Parameter print_float : float -> unit.
+
+Parameter print_endline : string -> unit.
+
+Parameter print_newline : unit -> unit.
+
+(** ** Output functions on standard error *)
+Parameter prerr_char : char -> unit.
+
+Parameter prerr_string : string -> unit.
+
+Parameter prerr_bytes : bytes -> unit.
+
+Parameter prerr_int : int -> unit.
+
+Parameter prerr_float : float -> unit.
+
+Parameter prerr_endline : string -> unit.
+
+Parameter prerr_newline : unit -> unit.
+
+(** ** Input functions on standard input *)
+Parameter read_line : unit -> string.
+
+Parameter read_int_opt : unit -> option int.
+
+Parameter read_int : unit -> int.
+
+Parameter read_float_opt : unit -> option float.
+
+Parameter read_float : unit -> float.
+
+(** ** General output functions *)
+Inductive open_flag : Set :=
+| Open_rdonly
+| Open_wronly
+| Open_append
+| Open_creat
+| Open_trunc
+| Open_excl
+| Open_binary
+| Open_text
+| Open_nonblock.
+
+Parameter open_out : string -> out_channel.
+
+Parameter open_out_bin : string -> out_channel.
+
+Parameter open_out_gen : list open_flag -> int -> string -> out_channel.
+
+Parameter flush : out_channel -> unit.
+
+Parameter flush_all : unit -> unit.
+
+Parameter output_char : out_channel -> char -> unit.
+
+Parameter output_string : out_channel -> string -> unit.
+
+Parameter output_bytes : out_channel -> bytes -> unit.
+
+Parameter output : out_channel -> bytes -> int -> int -> unit.
+
+Parameter output_substring : out_channel -> string -> int -> int -> unit.
+
+Parameter output_byte : out_channel -> int -> unit.
+
+Parameter output_binary_int : out_channel -> int -> unit.
+
+Parameter output_value : forall {a : Set}, out_channel -> a -> unit.
+
+Parameter seek_out : out_channel -> int -> unit.
+
+Parameter pos_out : out_channel -> int.
+
+Parameter out_channel_length : out_channel -> int.
+
+Parameter close_out : out_channel -> unit.
+
+Parameter close_out_noerr : out_channel -> unit.
+
+Parameter set_binary_mode_out : out_channel -> bool -> unit.
+
+(** ** General input functions *)
+Parameter open_in : string -> in_channel.
+
+Parameter open_in_bin : string -> in_channel.
+
+Parameter open_in_gen : list open_flag -> int -> string -> in_channel.
+
+Parameter input_char : in_channel -> char.
+
+Parameter input_line : in_channel -> string.
+
+Parameter input : in_channel -> bytes -> int -> int -> int.
+
+Parameter really_input : in_channel -> bytes -> int -> int -> unit.
+
+Parameter really_input_string : in_channel -> int -> string.
+
+Parameter input_byte : in_channel -> int.
+
+Parameter input_binary_int : in_channel -> int.
+
+Parameter input_value : forall {a : Set}, in_channel -> a.
+
+Parameter seek_in : in_channel -> int -> unit.
+
+Parameter pos_in : in_channel -> int.
+
+Parameter in_channel_length : in_channel -> int.
+
+Parameter close_in : in_channel -> unit.
+
+Parameter close_in_noerr : in_channel -> unit.
+
+Parameter set_binary_mode_in : in_channel -> bool -> unit.
+
+(** ** Operations on large files *)
+Module LargeFile.
+  Parameter seek_out : out_channel -> int64 -> unit.
+
+  Parameter pos_out : out_channel -> int64.
+
+  Parameter out_channel_length : out_channel -> int64.
+
+  Parameter seek_in : in_channel -> int64 -> unit.
+
+  Parameter pos_in : in_channel -> int64.
+
+  Parameter in_channel_length : in_channel -> int64.
+End LargeFile.
+
 (** * References *)
+Record ref {a : Set} : Set := {
+  contents : a;
+}.
+Arguments ref : clear implicits.
+
+Parameter ref_value : forall {a : Set}, a -> ref a.
+
+Parameter op_exclamation : forall {a : Set}, ref a -> a.
+
+Parameter op_coloneq : forall {a : Set}, ref a -> a -> unit.
+
+Parameter incr : ref int -> unit.
+
+Parameter decr : ref int -> unit.
+
 (** * Result type *)
+Inductive result (a b : Set) : Set :=
+| Ok : a -> result a b
+| Error : b -> result a b.
+Arguments Ok {_}.
+Arguments Error {_}.
+
 (** * Operations on format strings *)
+Definition format6 : Set -> Set -> Set -> Set -> Set -> Set -> Set :=
+  CamlinternalFormatBasics.format6.
+
+Definition format4 (a b c d : Set) : Set := format6 a b c c c d.
+
+Definition format (a b c : Set) : Set := format4 a b c c.
+
+Parameter string_of_format : forall {a b c d e f : Set},
+  format6 a b c d e f -> string.
+
+Parameter format_of_string : forall {a b c d e f : Set},
+  format6 a b c d e f -> format6 a b c d e f.
+
+Parameter op_caretcaret : forall {a b c d e f g h : Set},
+  format6 a b c d e f -> format6 f b c e g h -> format6 a b c d g h.
+
 (** * Program termination *)
+Parameter exit : forall {a : Set}, int -> a.
+
+Parameter at_exit : (unit -> unit) -> unit.
+
 (** * Standard library modules  *)

src/configurationRenaming.ml

@@ -1,12 +1,10 @@
 let rules =
   [
     (* Built-in types *)
-    ("char", "ascii");
     ("()", "tt");
     ("op_coloncolon", "cons");
     ("Ok", "inl");
     ("Error", "inr");
-    ("exn", "extensible_type");
     (* Predefined exceptions *)
     ("Match_failure", "CoqOfOCaml.Match_failure");
     ("Assert_failure", "CoqOfOCaml.Assert_failure");

tests/builtin_types.v

@@ -3,13 +3,13 @@ Require Import CoqOfOCaml.Settings.
 
 Definition n : int := 12.
 
-Definition c1 : ascii := "a" % char.
+Definition c1 : char := "a" % char.
 
-Definition c2 : ascii := "010" % char.
+Definition c2 : char := "010" % char.
 
-Definition c3 : ascii := "009" % char.
+Definition c3 : char := "009" % char.
 
-Definition c4 : ascii := """" % char.
+Definition c4 : char := """" % char.
 
 Definition s : string := "hi\n\t:)\""".
 

tests/functor.v

@@ -32,7 +32,7 @@ Parameter Make :
   forall {P_t : Set},
   forall (P : COMPARABLE (t := P_t)), S (t := P.(COMPARABLE.t)).
 
-Parameter Char : S (t := ascii).
+Parameter Char : S (t := char).
 
 Parameter Abstract_t : Set.
 

tests/pre_defined_types.v

@@ -13,7 +13,7 @@ Definition o1 {A : Set} : option A := None.
 
 Definition o2 : option int := Some 12.
 
-Definition c : ascii := "g" % char.
+Definition c : char := "g" % char.
 
 Definition s1 : string := "bla".