Skip to content
Snippets Groups Projects
stdlib.mli 4.29 KiB
Newer Older
  • Learn to ignore specific revisions
  • (*
    Field name attributes for builtins (eg: ::) are defined in attributes.ml
    
    val ( ~+ ) : int -> int
    val ( ~- ) : int -> int
    
    Thomas Wood's avatar
    Thomas Wood committed
    val ( + ) : int -> int -> int
    val ( - ) : int -> int -> int
    val ( * ) : int -> int -> int
    val ( / ) : int -> int -> int
    
    
    type fpclass =
      | FP_normal
      | FP_subnormal
      | FP_zero
      | FP_infinite
      | FP_nan
    val nan : float
    val infinity : float
    val neg_infinity : float
    val max_float : float
    
    charguer's avatar
    charguer committed
    val min_float : float
    
    val ( ~+. ) : float -> float
    val ( ~-. ) : float -> float
    val ( +. ) : float -> float -> float
    val ( -. ) : float -> float -> float
    val ( *. ) : float -> float -> float
    val ( /. ) : float -> float -> float
    val ( ** ) : float -> float -> float
    val abs_float : float -> float
    val mod_float : float -> float -> float
    val atan : float -> float
    val exp : float -> float
    val log : float -> float
    val floor : float -> float
    val min : float -> float -> float
    val max : float -> float -> float
    val classify_float : float -> fpclass
    
    
    charguer's avatar
    charguer committed
    val int_abs : int -> int
    
    
    val float_of_int : int -> float
    val float_of_string : string -> float
    val int_of_char : char -> int
    val int_of_float : float -> int
    val string_of_float : float -> string
    val string_of_int : int -> string
    
    
    Alan Schmitt's avatar
    Alan Schmitt committed
    (* We use this to compare types that are not known by stdlib, like Native_error *)
    val ( === ) : 'a -> 'a -> bool
    
    charguer's avatar
    charguer committed
    (*val ( <> ) : 'a -> 'a -> bool*)
    (*val ( < ) : 'a -> 'a -> bool
    
    val ( > ) : 'a -> 'a -> bool
    val ( <= ) : 'a -> 'a -> bool 
    val ( >= ) : 'a -> 'a -> bool
    
    charguer's avatar
    charguer committed
    *)
    val ( = ) : float -> float -> bool
    val ( < ) : float -> float -> bool
    val ( > ) : float -> float -> bool
    val ( <= ) : float -> float -> bool 
    val ( >= ) : float -> float -> bool
    (*val compare : 'a -> 'a -> int*)
    
    charguer's avatar
    charguer committed
    val bool_eq : bool -> bool -> bool
    val int_eq : int -> int -> bool
    
    charguer's avatar
    charguer committed
    val int_lt : int -> int -> bool
    
    charguer's avatar
    charguer committed
    val int_ge : int -> int -> bool
    val string_eq : string -> string -> bool
    val float_eq : float -> float -> bool
    
    charguer's avatar
    charguer committed
    val float_lt : float -> float -> bool
    val float_le : float -> float -> bool
    
    charguer's avatar
    charguer committed
    val float_compare : float -> float -> int
    
    Alan Schmitt's avatar
    Alan Schmitt committed
    
    
    charguer's avatar
    charguer committed
    val string_concat : string -> string -> string
    
    
    
    charguer's avatar
    charguer committed
    val pi : float
    val e : float
    val ln2 : float
    
    
    charguer's avatar
    charguer committed
    val float_neg : float -> float (* ~-.*)
    
    val lt_bool : float -> float -> bool (*   (<) *)
    val add : float -> float -> float (*  (+.) *)
    val sub : float -> float -> float (*  (-.) *)
    val mult : float -> float -> float (*  ( *. ) *)
    val div : float -> float -> float (*  (/.) *)
    val fmod : float -> float -> float (*  mod_float *)
    val float_exp : float -> float -> float (* ( ** ) *)
    
    
    
    
    charguer's avatar
    charguer committed
    val ( && ) : bool -> bool -> bool
    val not : bool -> bool
    
    val stuck : string -> 'a
    
    
    charguer's avatar
    charguer committed
    (* Structural equality, need to be careful with implementation 
    val (=) : 'a -> 'a -> bool*)
    
    val (^) : string -> string -> string
    
    val ref : 'a -> 'a ref
    val (:=) : 'a ref -> 'a -> unit
    val (!) : 'a ref -> 'a
    
    
    Thomas Wood's avatar
    Thomas Wood committed
    (* Coq extraction builtins refer directly to Pervasives at times *)
    module Pervasives : sig
      val succ : int -> int
    end
    
    
    module Int32 : sig
      val logand : int32 -> int32 -> int32
      val lognot : int32 -> int32
      val logor : int32 -> int32 -> int32
      val logxor : int32 -> int32 -> int32
      val of_float : float -> int32
      val shift_left : int32 -> int -> int32
      val shift_right : int32 -> int -> int32
      val shift_right_logical : int32 -> int -> int32
      val to_float : int32 -> float
    end
    
    module Int64 : sig
      val one : int64
      val float_of_bits : int64 -> float
    end
    
    module List : sig
      val map : ('a -> 'b) -> 'a list -> 'b list
      val rev : 'a list -> 'a list
    end
    
    module String : sig
    
    charguer's avatar
    charguer committed
      val length : string -> int
      val append : string -> string -> string
      val sub : string -> int -> int -> string
    
      val concat : string -> string list -> string
      val iter : (char -> unit) -> string -> unit
      val make : int -> char -> string
    
    Alan Schmitt's avatar
    Alan Schmitt committed
      val get : string -> int -> char
    
    Thomas Wood's avatar
    Thomas Wood committed
    (* Coq outputs exceptions in the place of arbitrary *)
    val raise : exn -> 'a
    
    
    (* JSRef specific functions *)
    val prerr_string : string -> unit
    val prerr_newline : unit -> unit
    
    Alan Schmitt's avatar
    Alan Schmitt committed
    val prerr_endline : string -> unit
    
    charguer's avatar
    charguer committed
    
    
    module Parser_syntax : sig (* ARTHUR: to implement *)
      type unary_op
      type arith_op
      type bin_op
      type exp
    end
    
    
    charguer's avatar
    charguer committed
    module Parser_main : sig 
      val exp_from_string : ?force_strict:bool -> string -> Parser_syntax.exp
    end 
    
    (* ARTHUR: not needed
    module Parser : sig
      exception ParserFailure of string
      exception InvalidArgument
    end
    
    *)
    
    module Obj : sig
      type t
    end
    
    val print_endline : string -> unit
    
    val __LOC__ : string