stdlib.mli

(*--------------------*)
(* int operations *)

(* todo : factorize and clean up *)
(*
val ( ~+ ) : int -> int
val ( ~- ) : int -> int
*)

val ( + ) : int -> int -> int
val ( - ) : int -> int -> int
val ( * ) : int -> int -> int
val ( / ) : int -> int -> int

(*val int_abs : int -> int*)

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

(*--------------------*)
(* float operations *)

(* Alan: these can be implemented directly, using Number.NaN,
   Number.POSITIVE_INFINITY, Number.NEGATIVE_INFINITY *)
(*
val nan : float
val infinity : float
val neg_infinity : float
*)

(* Alan: Do we need these ? If so, they are Number.MAX_VALUE and
   Number.MIN_VALUE

val max_float : float
val min_float : float

 *)


(* 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 *)


(*
val mod_float : float -> float -> float (* Alan: % infix *)
*)

(* 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 min : float -> float -> float
val max : float -> float -> float
*)


(* 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 int_of_float : float -> int (* will be removed, since only used by substring *)
val number_of_int : int -> float  (* = fun x -> float_of_int x *)

(** val of_int : float -> number **)
val of_int : float -> float (* = fun x -> x,  
  that is, an identity function, kept in files for documentation *)


(*val float_of_string : string -> float*)
(*val float_of_int : int -> float*)
(*
val int_of_char : char -> int
val string_of_float : float -> string
val string_of_int : int -> string
*)

(* no need to implement those in stdlib.js because JS has them already *)
val ( = ) : float -> float -> bool
val ( < ) : float -> float -> bool
val ( > ) : float -> float -> bool
val ( <= ) : float -> float -> bool 
val ( >= ) : float -> float -> bool
val fmod : float -> float -> float (*  mod_float, implemented as % operator in JS *)


(** val number_comparable : number coq_Comparable **)
val number_comparable : float -> float -> bool  (* = (fun n1 n2 -> int_eq 0  (float_compare n1 n2)) *)
  (* same as (=) *)

(*val compare : 'a -> 'a -> int*)
(*val float_lt : float -> float -> bool
val float_le : float -> float -> bool*)
(*val float_compare : float -> float -> int*)
(* val float_neg : float -> float  ~-.*)
(* val float_exp : float -> float -> float (* ( ** ) *) *)


(*--------------------*)
(* bool operations *)

val bool_eq : bool -> bool -> bool (* should be "===" in  JS *)
val ( && ) : bool -> bool -> bool  (* beware of strict vs lazy semantics: todo discuss --> just map to  *)
val not : bool -> bool
val ( || ) : bool -> bool -> bool  (* beware of strict vs lazy semantics: todo discuss --> just map to  *)


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

(* todo : factorize and clean up *)

val string_eq : string -> string -> bool (* === *)
val string_compare : string -> string -> float (* actually returns an int *)

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

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

(* let strlength s = String.length s *)
val strlength : string -> int (* in JS :  function (x) { return x.length; } *)

(* let substring n m s = String.sub s n m *)
val substring : int -> int -> string -> string  (* function(x) { return x.slice(n, n+m); } *)
 (* only need to implement this when m=1 *)


(*--------------------*)
(* 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  (* becomes === in js *)



(*--------------------*)
(* JSRef specific functions, useful for debugging *)

(* val print_endline : string -> unit *)

val __LOC__ : string (* todo: will not be needed in the future *)

(*
val prerr_string : string -> unit
val prerr_newline : unit -> unit
val prerr_endline : string -> unit
*)

val raise : exn -> 'a   (* bind to  throw "Not_found" *)
(*val stuck : string -> 'a*)





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

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