From 89ddb38279e2201c231b7ace63e8ac7f7ed301e6 Mon Sep 17 00:00:00 2001
From: charguer <arthur@chargueraud.org>
Date: Tue, 22 Mar 2016 10:34:56 +0100
Subject: [PATCH] stdlib_simplify
---
generator/stdlib_ml/stdlib.mli | 162 ++++++++++---------------
generator/tests/jsref/JsCommon.ml | 4 +-
generator/tests/jsref/JsInterpreter.ml | 22 ++--
generator/tests/jsref/JsNumber.mli | 3 +
generator/tests/jsref/JsPreliminary.ml | 4 +-
generator/tests/jsref/LibString.ml | 2 +-
generator/tests/jsref/Shared.ml | 6 +-
7 files changed, 86 insertions(+), 117 deletions(-)
diff --git a/generator/stdlib_ml/stdlib.mli b/generator/stdlib_ml/stdlib.mli
index b1d92ef..d84a705 100644
--- a/generator/stdlib_ml/stdlib.mli
+++ b/generator/stdlib_ml/stdlib.mli
@@ -1,6 +1,6 @@
(*--------------------*)
-(* number operations *)
+(* int operations *)
(* todo : factorize and clean up *)
@@ -11,17 +11,15 @@ val ( - ) : int -> int -> int
val ( * ) : int -> int -> int
val ( / ) : int -> int -> int
-(* Alan: I don't think fpclass is needed. To compare numbers, we can use
- - isNaN https://es5.github.io/#x15.1.2.4
- - === with Number.POSITIVE_INFINITY or NUMBER.NEGATIVE_INFINITY
- - === to 0 *)
+(*val int_abs : int -> int*)
-type fpclass =
- | FP_normal
- | FP_subnormal
- | FP_zero
- | FP_infinite
- | FP_nan
+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 *)
@@ -51,35 +49,39 @@ val ( ** ) : float -> float -> float
val abs_float : float -> float
-(* Alan: % infix *)
-
-val mod_float : 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 floor : float -> float
val min : float -> float -> float
val max : float -> float -> float
+*)
-(* Alan: do we need this? *)
-
-val classify_float : float -> fpclass
-
-val int_abs : int -> int
(* 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 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
@@ -87,50 +89,26 @@ 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 compare : 'a -> 'a -> int*)
-val int_eq : int -> int -> bool
-val int_lt : int -> int -> bool
-val int_ge : int -> int -> bool
-
-val float_eq : float -> float -> bool
-val float_lt : float -> float -> bool
-val float_le : float -> float -> bool
-val float_compare : float -> float -> int
(** 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 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: why are these here? *)
-
-val pi : float
-val e : float
-val ln2 : float
-
-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 (* ( ** ) *)
+(*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*)
+val ( && ) : bool -> bool -> bool (* beware of strict vs lazy semantics: todo discuss --> just map to *)
val not : bool -> bool
@@ -139,32 +117,22 @@ val not : bool -> bool
(* todo : factorize and clean up *)
-val string_eq : string -> string -> bool
-
-val string_concat : string -> string -> string
+val string_eq : string -> string -> bool (* === *)
-val (^) : string -> string -> string
-
-(* let string_dec s1 s2 = (string_eq s1 s2) *)
-val string_dec : string -> string -> bool
+(*
+ val string_concat : string -> string -> string (* + *)
+ val (^) : string -> string -> string
+*)
(* let append s1 s2 = String.append s1 s2 *)
-val strappend : string -> string -> string
+val strappend : string -> string -> string (* + *)
(* let strlength s = String.length s *)
-val strlength : string -> int
+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
-
-
-
-(*--------------------*)
-(* for future use for the global heap *)
-
-val ref : 'a -> 'a ref
-val (:=) : 'a ref -> 'a -> unit
-val (!) : 'a ref -> 'a
+val substring : int -> int -> string -> string (* function(x) { return x.slice(n, n+m); } *)
+ (* only need to implement this when m=1 *)
(*--------------------*)
@@ -173,37 +141,35 @@ val (!) : 'a ref -> 'a
(* 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
-
+val ( === ) : 'a -> 'a -> bool (* becomes === in js *)
-(*--------------------*)
-(* todo: remove when JsNumber.ml becomes .mli file *)
-
-(* 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
(*--------------------*)
(* JSRef specific functions, useful for debugging *)
-val print_endline : string -> unit
-val __LOC__ : string
+(* 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*)
+
+
-val raise : exn -> 'a
-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
+ *)
diff --git a/generator/tests/jsref/JsCommon.ml b/generator/tests/jsref/JsCommon.ml
index e15e7aa..b36efa4 100644
--- a/generator/tests/jsref/JsCommon.ml
+++ b/generator/tests/jsref/JsCommon.ml
@@ -520,12 +520,12 @@ let throw_irrelevant =
(** val add_one : number -> number **)
let add_one n =
- add n JsNumber.one
+ n +. JsNumber.one
(** val sub_one : number -> number **)
let sub_one n =
- sub n JsNumber.one
+ n -. JsNumber.one
(** val is_syntactic_eval : expr -> bool **)
diff --git a/generator/tests/jsref/JsInterpreter.ml b/generator/tests/jsref/JsInterpreter.ml
index dcdafb9..8f3587e 100644
--- a/generator/tests/jsref/JsInterpreter.ml
+++ b/generator/tests/jsref/JsInterpreter.ml
@@ -592,7 +592,7 @@ let object_can_put runs0 s c l x =
strictness_flag -> __ specres) -> result **)
let run_object_define_own_prop_array_loop runs0 s c l newLen oldLen newLenDesc newWritable throwcont def =
- if lt_int_decidable newLen oldLen
+ if newLen < oldLen
then let_binding (oldLen -. 1.) (fun oldLen' ->
if_string
(to_string runs0 s c (Coq_value_prim (Coq_prim_number
@@ -821,7 +821,7 @@ let object_define_own_prop runs0 s c l x desc throwcont =
(fun s2 slen ->
if and_decidable (string_comparable x slen)
(not_decidable
- (float_eq ilen
+ ( ilen =
((fun p -> 1. +. (2. *. p))
((fun p -> 1. +. (2. *. p))
((fun p -> 1. +. (2. *. p))
@@ -2994,11 +2994,11 @@ let is_lazy_op _foo_ = match _foo_ with
binary_op -> (number -> number -> number) option **)
let get_puremath_op _foo_ = match _foo_ with
-| Coq_binary_op_mult -> Some mult
-| Coq_binary_op_div -> Some div
+| Coq_binary_op_mult -> Some (fun x y -> x *. y)
+| Coq_binary_op_div -> Some (fun x y -> x /. y)
| Coq_binary_op_mod -> Some fmod
| Coq_binary_op_add -> None
-| Coq_binary_op_sub -> Some sub
+| Coq_binary_op_sub -> Some (fun x y -> x -. y)
| Coq_binary_op_left_shift -> None
| Coq_binary_op_right_shift -> None
| Coq_binary_op_unsigned_right_shift -> None
@@ -3220,7 +3220,7 @@ let run_binary_op runs0 s c op v1 v2 =
(Coq_value_prim w2)) (fun s2 nn ->
let (n1, n2) = nn in
res_out (Coq_out_ter (s2,
- (res_val (Coq_value_prim (Coq_prim_number (add n1 n2))))))))
+ (res_val (Coq_value_prim (Coq_prim_number (n1 +. n2))))))))
else if issome (get_puremath_op op)
then if_some (get_puremath_op op) (fun mop ->
if_spec (convert_twice_number runs0 s c v1 v2) (fun s1 nn ->
@@ -4730,7 +4730,7 @@ let rec run_object_is_frozen runs0 s c l _foo_ = match _foo_ with
value list specres **)
let run_get_args_for_apply runs0 s c l index n =
- if lt_int_decidable index n
+ if index < n
then if_string
(to_string runs0 s c (Coq_value_prim (Coq_prim_number
(of_int index)))) (fun s0 sindex ->
@@ -4769,7 +4769,7 @@ let valueToStringForJoin runs0 s c l k =
string -> string -> result **)
let run_array_join_elements runs0 s c l k length0 sep sR =
- if lt_int_decidable k length0
+ if k < length0
then let_binding (append sR sep) (fun ss ->
let_binding (valueToStringForJoin runs0 s c l k) (fun sE ->
if_spec sE (fun s0 element ->
@@ -5145,7 +5145,7 @@ let run_call_prealloc runs0 s c b vthis args =
(to_int32 runs0 s'0 c (Coq_value_prim
(Coq_prim_number n)))
(fun s'1 ilen ->
- if lt_int_decidable ilen
+ if ilen <
(number_of_int (LibList.length a))
then res_spec s'1 0.
else res_spec s'1
@@ -5389,7 +5389,7 @@ let run_call_prealloc runs0 s c b vthis args =
then vsep
else Coq_value_prim (Coq_prim_string (","))) (fun rsep ->
if_string (to_string runs0 s2 c rsep) (fun s3 sep ->
- if float_eq ilen 0.0
+ if ilen = 0.0
then res_ter s3
(res_val (Coq_value_prim (Coq_prim_string "")))
else let_binding (valueToStringForJoin runs0 s3 c l 0.)
@@ -5402,7 +5402,7 @@ let run_call_prealloc runs0 s c b vthis args =
(run_object_get runs0 s0 c l
("length")) (fun s1 vlen ->
if_spec (to_uint32 runs0 s1 c vlen) (fun s2 ilen ->
- if float_eq ilen 0.0
+ if ilen = 0.0
then if_not_throw
(object_put runs0 s2 c l
("length")
diff --git a/generator/tests/jsref/JsNumber.mli b/generator/tests/jsref/JsNumber.mli
index 7d0a7cd..819e283 100644
--- a/generator/tests/jsref/JsNumber.mli
+++ b/generator/tests/jsref/JsNumber.mli
@@ -1,5 +1,8 @@
type number = float
+val floor : float -> float
+
+
val zero: number
val neg_zero : number
val one : number
diff --git a/generator/tests/jsref/JsPreliminary.ml b/generator/tests/jsref/JsPreliminary.ml
index e396aeb..e9e2905 100644
--- a/generator/tests/jsref/JsPreliminary.ml
+++ b/generator/tests/jsref/JsPreliminary.ml
@@ -55,7 +55,7 @@ let convert_number_to_integer n =
(or_decidable (number_comparable n JsNumber.infinity)
(number_comparable n JsNumber.neg_infinity)))
then n
- else mult (JsNumber.sign n) (floor (JsNumber.absolute n))
+ else (JsNumber.sign n) *. (JsNumber.floor (JsNumber.absolute n))
(** val convert_bool_to_string : bool -> string **)
@@ -144,7 +144,7 @@ let inequality_test_number n1 n2 =
then Coq_prim_bool false
else if number_comparable n1 JsNumber.neg_infinity
then Coq_prim_bool true
- else Coq_prim_bool (lt_bool n1 n2)
+ else Coq_prim_bool (n1 < n2)
(** val inequality_test_string : string -> string -> bool **)
diff --git a/generator/tests/jsref/LibString.ml b/generator/tests/jsref/LibString.ml
index da3ea98..856da27 100644
--- a/generator/tests/jsref/LibString.ml
+++ b/generator/tests/jsref/LibString.ml
@@ -4,5 +4,5 @@ open LibReflect
(** val string_comparable : string coq_Comparable **)
let string_comparable x y =
- comparable_of_dec string_dec x y
+ comparable_of_dec string_eq x y
diff --git a/generator/tests/jsref/Shared.ml b/generator/tests/jsref/Shared.ml
index 9c4adb4..8e4a5ee 100644
--- a/generator/tests/jsref/Shared.ml
+++ b/generator/tests/jsref/Shared.ml
@@ -14,7 +14,7 @@ let option_case d f o = match o with
(** val int_of_char : char -> float **)
-let int_of_char = (fun c -> float_of_int (int_of_char c))
+ (* let int_of_char = (fun c -> float_of_int (int_of_char c)) *)
(** val string_sub : string -> int -> int -> string **)
@@ -23,11 +23,11 @@ let string_sub s n l =
(** val lt_int_decidable : float -> float -> coq_Decidable **)
-let lt_int_decidable x y = float_lt x y
+let lt_int_decidable x y = x < y
(** val le_int_decidable : float -> float -> coq_Decidable **)
-let le_int_decidable x y = float_le x y
+let le_int_decidable x y = x <= y
(** val ge_nat_decidable : int -> int -> coq_Decidable **)
--
GitLab