Skip to content
Snippets Groups Projects
stdlib.mli 6.28 KiB
Newer Older
charguer's avatar
charguer committed

(*--------------------*)
(* number operations *)

(* todo : factorize and clean up *)

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

Alan Schmitt's avatar
Alan Schmitt committed
(* Alan: I don't think fpclass is needed *)

type fpclass =
  | FP_normal
  | FP_subnormal
  | FP_zero
  | FP_infinite
  | FP_nan
Alan Schmitt's avatar
Alan Schmitt committed

(* Alan: these can be implemented directly, using NaN, Infinity, -Infinity *)

val nan : float
val infinity : float
val neg_infinity : float
Alan Schmitt's avatar
Alan Schmitt committed

(* Alan: Do we need these ? *)

val max_float : float
charguer's avatar
charguer committed
val min_float : float
Alan Schmitt's avatar
Alan Schmitt committed

(* Alan: these should all be implemented along with the int operations as the JS
   ones. ** is Math.pow *)

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
Alan Schmitt's avatar
Alan Schmitt committed

(* Alan: Math.abs, if we need it *)

val abs_float : float -> float
Alan Schmitt's avatar
Alan Schmitt committed

(* Alan: % infix *)

val mod_float : float -> float -> float
Alan Schmitt's avatar
Alan Schmitt committed

(* Alan: Why do we need these? If need be, they are all in Math *)

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
Alan Schmitt's avatar
Alan Schmitt committed

(* Alan: do we need this? *)

val classify_float : float -> fpclass

charguer's avatar
charguer committed
val int_abs : int -> int

Alan Schmitt's avatar
Alan Schmitt committed
(* Alan: Ideally we would add these to the spec, but for the moment conversion
   to a string is doing a foo+"", and conversion to an int is doing +foo *)

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

charguer's avatar
charguer committed

(* no need to implement those in stdlib.js because JS has them already *)
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
charguer's avatar
charguer committed

charguer's avatar
charguer committed
(*val compare : 'a -> 'a -> int*)
charguer's avatar
charguer committed
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
charguer's avatar
charguer committed

charguer's avatar
charguer committed
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
charguer's avatar
charguer committed
(** val number_comparable : number coq_Comparable **)
val number_comparable : float -> float -> bool  (* = (fun n1 n2 -> int_eq 0  (float_compare n1 n2)) *)

(** val of_int : float -> number **)
val of_int : float -> float (* = fun x -> x *)

val number_of_int : int -> float  (* = fun x -> float_of_int x *)

val nat_eq : int -> int -> bool (* nat_eq x y = int_eq x y  *)

Alan Schmitt's avatar
Alan Schmitt committed

(* Alan: why are these here? *)

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
(*--------------------*)
(* bool operations *)
charguer's avatar
charguer committed

charguer's avatar
charguer committed
val bool_eq : bool -> bool -> bool (* should be "===" in  JS *)
val ( && ) : bool -> bool -> bool  (* beware of strict vs lazy semantics: todo discuss*)
charguer's avatar
charguer committed
val not : bool -> bool
charguer's avatar
charguer committed

(*--------------------*)
(* string operations *)

(* todo : factorize and clean up *)

val string_eq : string -> string -> bool

val string_concat : string -> string -> string
val (^) : string -> string -> string

charguer's avatar
charguer committed
(* let string_dec s1 s2 = (string_eq s1 s2) *)
val string_dec : string -> string -> bool

(* let append s1 s2 = String.append s1 s2 *)
val strappend : string -> string -> string 

(* let strlength s = String.length s *)
val strlength : string -> int

(* let substring n m s = String.sub s n m *)
val substring : int -> int -> string -> string



(*--------------------*)
(* for future use for the global heap *)

val ref : 'a -> 'a ref
val (:=) : 'a ref -> 'a -> unit
val (!) : 'a ref -> 'a

charguer's avatar
charguer committed

charguer's avatar
charguer committed
(*--------------------*)
(* special operations *)

(* We use this to compare types that are not known by stdlib, like Native_error;
  should be implemented in JS by comparing the objects, to see if they have the same
  "tag" fields (there should be no other fields, except perhaps "type") *)
val ( === ) : 'a -> 'a -> bool




(*--------------------*)

(* no longer needed it seems 
Thomas Wood's avatar
Thomas Wood committed
module Pervasives : sig
  val succ : int -> int
end
charguer's avatar
charguer committed
*)
charguer's avatar
charguer committed
(*--------------------*)
(* todo: remove when JsNumber.ml becomes .mli file *)
Alan Schmitt's avatar
Alan Schmitt committed

(* Alan: I'll do this *)

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


charguer's avatar
charguer committed

charguer's avatar
charguer committed

(*--------------------*)

(* figure out how to deal with parser *)

charguer's avatar
charguer committed
module Parser_syntax : sig (* needed by translate_syntax.mli and by parser_main (below) *)
charguer's avatar
charguer committed
  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 

charguer's avatar
charguer committed
(* ARTHUR: not needed -- tocheck
   module Parser : sig
     exception ParserFailure of string
     exception InvalidArgument
   end
charguer's avatar
charguer committed
(*--------------------*)
(* JSRef specific functions, useful for debugging *)
charguer's avatar
charguer committed

val print_endline : string -> unit
charguer's avatar
charguer committed
val __LOC__ : string
charguer's avatar
charguer committed

val prerr_string : string -> unit
val prerr_newline : unit -> unit
val prerr_endline : string -> unit

val raise : exn -> 'a
charguer's avatar
charguer committed
val stuck : string -> 'a
charguer's avatar
charguer committed




(*--------------------*)
(* deprecated *)

(* should not be needed if we don't use JsNumber.ml *)
(*
module Int64 : sig 
  val one : int64
  val float_of_bits : int64 -> float
end

module List : sig (* should rely on List0 instead *)
  val map : ('a -> 'b) -> 'a list -> 'b list
  val rev : 'a list -> 'a list
end

module String : sig (* should rely on String0 instead *)
  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
  val get : string -> int -> char
end

*)