From 2a71f5a3d33ad7e0d7d464ff228d01f2ac6ac57b Mon Sep 17 00:00:00 2001
From: charguer <arthur@chargueraud.org>
Date: Tue, 9 Feb 2016 10:35:14 +0100
Subject: [PATCH] int_float
---
generator/TODO | 10 +-
generator/js_of_ast.ml | 8 +-
generator/stdlib_ml/stdlib.mli | 27 ++--
generator/tests/jsref/BinInt.ml | 149 +++++++++++-----------
generator/tests/jsref/BinNat.ml | 110 +++++++++--------
generator/tests/jsref/BinPos.ml | 157 +++++++++++------------
generator/tests/jsref/BinPosDef.ml | 164 +++++++++++++------------
generator/tests/jsref/JsInterpreter.ml | 22 ++--
generator/tests/jsref/JsNumber.ml | 12 +-
generator/tests/jsref/JsPreliminary.ml | 2 +-
generator/tests/jsref/LibList.ml | 2 +-
generator/tests/jsref/LibNat.ml | 6 +-
generator/tests/jsref/LibReflect.ml | 2 +-
generator/tests/jsref/Peano.ml | 2 +-
generator/tests/jsref/Shared.ml | 2 +-
generator/tests/jsref/String0.ml | 2 +-
16 files changed, 360 insertions(+), 317 deletions(-)
diff --git a/generator/TODO b/generator/TODO
index fc05b7a..652447a 100644
--- a/generator/TODO
+++ b/generator/TODO
@@ -1,10 +1,14 @@
-- deal with unsupported let record in jsinterpreter.ml
+
+
- cases seem to be in reversed order, check and fix
+ => corriger à la main le jour où on s'amuse à relire le code.
+ => order in pattern matching extraction seems to follow
+ order from the definition of the inductive type,
+ instead of the order of the code.
- untab closing bracket for fun def
-
-- default case with error in switch, for logged/token mode
+ => later maybe
- understand spec of polymorphic equality (= vs ===)
diff --git a/generator/js_of_ast.ml b/generator/js_of_ast.ml
index 7e5e4fa..807a7f4 100644
--- a/generator/js_of_ast.ml
+++ b/generator/js_of_ast.ml
@@ -119,6 +119,12 @@ let ppf_apply_infix f arg1 arg2 =
let ppf_match value cases const =
let cons_fld = if const then "" else ".type" in
+ let cases =
+ match !current_mode with
+ | Mode_unlogged -> cases
+ | Mode_line_token
+ | Mode_logged -> cases ^ "@,default: throw \"No matching case for switch\";"
+ in
let s = Printf.sprintf "switch (%s%s) {@;<1 2>@[<v 0>%s@]@,}@,"
value cons_fld cases
in s
@@ -315,7 +321,7 @@ let generate_logged_return ctx sbody =
Printf.sprintf "%sreturn %s;%s" token_start sbody token_stop
| Mode_logged ->
let id = id_fresh "_return_" in
- Printf.sprintf "var %s = %s;@,log_event(%s, ctx_push(%s, {\"return_value\", %s}), \"return\");@,return %s"
+ Printf.sprintf "var %s = %s;@,log_event(%s, ctx_push(%s, {\"return_value\", %s}), \"return\");@,return %s;"
id sbody token_lineof ctx id id
| Mode_unlogged ->
Printf.sprintf "return %s;" sbody
diff --git a/generator/stdlib_ml/stdlib.mli b/generator/stdlib_ml/stdlib.mli
index 34aeb5d..883c174 100644
--- a/generator/stdlib_ml/stdlib.mli
+++ b/generator/stdlib_ml/stdlib.mli
@@ -43,20 +43,33 @@ val int_of_float : float -> int
val string_of_float : float -> string
val string_of_int : int -> string
-val ( === ) : 'a -> 'a -> bool
-val ( <> ) : 'a -> 'a -> bool
-val ( < ) : 'a -> 'a -> bool
+(*val ( === ) : 'a -> 'a -> bool*)
+(*val ( <> ) : 'a -> 'a -> bool*)
+(*val ( < ) : 'a -> 'a -> bool
val ( > ) : 'a -> 'a -> bool
val ( <= ) : 'a -> 'a -> bool
val ( >= ) : 'a -> 'a -> bool
-val compare : 'a -> 'a -> int
+*)
+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*)
+
+val bool_eq : bool -> bool -> bool
+val int_eq : int -> int -> bool
+val int_ge : int -> int -> bool
+val string_eq : string -> string -> bool
+val float_eq : float -> float -> bool
+val float_compare : float -> float -> int
val ( && ) : bool -> bool -> bool
-
+val not : bool -> bool
val stuck : string -> 'a
-(* Structural equality, need to be careful with implementation *)
-val (=) : 'a -> 'a -> bool
+(* Structural equality, need to be careful with implementation
+val (=) : 'a -> 'a -> bool*)
val (^) : string -> string -> string
diff --git a/generator/tests/jsref/BinInt.ml b/generator/tests/jsref/BinInt.ml
index 3fce9d7..8aa1811 100644
--- a/generator/tests/jsref/BinInt.ml
+++ b/generator/tests/jsref/BinInt.ml
@@ -10,6 +10,11 @@ module Z =
struct
type t = float
+ (* HACK *)
+ let is_even p =
+ float_eq (mod_float p 2.) 0.
+
+
(** val zero : float **)
let zero =
@@ -28,7 +33,7 @@ module Z =
(** val double : float -> float **)
let double x =
- (fun f0 fp fn z -> if z=0. then f0 () else if z>0. then fp z else fn (~-. z))
+ (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
(fun _ ->
0.)
(fun p -> ((fun p -> 2. *. p)
@@ -40,7 +45,7 @@ module Z =
(** val succ_double : float -> float **)
let succ_double x =
- (fun f0 fp fn z -> if z=0. then f0 () else if z>0. then fp z else fn (~-. z))
+ (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
(fun _ ->
1.)
(fun p -> ((fun p -> 1. +. (2. *. p))
@@ -52,7 +57,7 @@ module Z =
(** val pred_double : float -> float **)
let pred_double x =
- (fun f0 fp fn z -> if z=0. then f0 () else if z>0. then fp z else fn (~-. z))
+ (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
(fun _ -> (~-.)
1.)
(fun p ->
@@ -65,10 +70,10 @@ module Z =
let rec pos_sub x y =
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun q ->
double (pos_sub p q))
(fun q ->
@@ -78,7 +83,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
y)
(fun p ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun q ->
pred_double (pos_sub p q))
(fun q ->
@@ -88,7 +93,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
y)
(fun _ ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun q -> (~-.) ((fun p -> 2. *. p)
q))
(fun q -> (~-.)
@@ -130,7 +135,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val pow : float -> float -> float **)
let pow x y =
- (fun f0 fp fn z -> if z=0. then f0 () else if z>0. then fp z else fn (~-. z))
+ (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
(fun _ ->
1.)
(fun p ->
@@ -142,7 +147,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val square : float -> float **)
let square x =
- (fun f0 fp fn z -> if z=0. then f0 () else if z>0. then fp z else fn (~-. z))
+ (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
(fun _ ->
0.)
(fun p ->
@@ -153,12 +158,12 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val compare : float -> float -> comparison **)
- let compare = fun x y -> if x=y then Eq else if x<y then Lt else Gt
+ let compare = fun x y -> if float_eq x y then Eq else if x<y then Lt else Gt
(** val sgn : float -> float **)
let sgn z =
- (fun f0 fp fn z -> if z=0. then f0 () else if z>0. then fp z else fn (~-. z))
+ (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
(fun _ ->
0.)
(fun p ->
@@ -202,9 +207,9 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val eqb : float -> float -> bool **)
let rec eqb x y =
- (fun f0 fp fn z -> if z=0. then f0 () else if z>0. then fp z else fn (~-. z))
+ (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
(fun _ ->
- (fun f0 fp fn z -> if z=0. then f0 () else if z>0. then fp z else fn (~-. z))
+ (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
(fun _ ->
true)
(fun p ->
@@ -213,7 +218,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
false)
y)
(fun p ->
- (fun f0 fp fn z -> if z=0. then f0 () else if z>0. then fp z else fn (~-. z))
+ (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
(fun _ ->
false)
(fun q ->
@@ -222,7 +227,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
false)
y)
(fun p ->
- (fun f0 fp fn z -> if z=0. then f0 () else if z>0. then fp z else fn (~-. z))
+ (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
(fun _ ->
false)
(fun p0 ->
@@ -247,7 +252,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val abs_nat : float -> int **)
let abs_nat z =
- (fun f0 fp fn z -> if z=0. then f0 () else if z>0. then fp z else fn (~-. z))
+ (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
(fun _ ->
0)
(fun p ->
@@ -259,7 +264,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val abs_N : float -> float **)
let abs_N z =
- (fun f0 fp fn z -> if z=0. then f0 () else if z>0. then fp z else fn (~-. z))
+ (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
(fun _ ->
0.)
(fun p ->
@@ -271,7 +276,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val to_nat : float -> int **)
let to_nat z =
- (fun f0 fp fn z -> if z=0. then f0 () else if z>0. then fp z else fn (~-. z))
+ (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
(fun _ ->
0)
(fun p ->
@@ -283,7 +288,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val to_N : float -> float **)
let to_N z =
- (fun f0 fp fn z -> if z=0. then f0 () else if z>0. then fp z else fn (~-. z))
+ (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
(fun _ ->
0.)
(fun p ->
@@ -295,7 +300,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val of_nat : int -> float **)
let of_nat n =
- (fun fO fS n -> if n=0 then fO () else fS (n-1))
+ (fun fO fS n -> if int_eq n 0 then fO () else fS (n-1))
(fun _ ->
0.)
(fun n0 ->
@@ -305,7 +310,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val of_N : float -> float **)
let of_N n =
- (fun f0 fp n -> if n=0. then f0 () else fp n)
+ (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
(fun _ ->
0.)
(fun p ->
@@ -315,7 +320,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val to_pos : float -> float **)
let to_pos z =
- (fun f0 fp fn z -> if z=0. then f0 () else if z>0. then fp z else fn (~-. z))
+ (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
(fun _ ->
1.)
(fun p ->
@@ -327,7 +332,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val iter : float -> ('a1 -> 'a1) -> 'a1 -> 'a1 **)
let iter n f x =
- (fun f0 fp fn z -> if z=0. then f0 () else if z>0. then fp z else fn (~-. z))
+ (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
(fun _ ->
x)
(fun p ->
@@ -340,7 +345,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
let rec pos_div_eucl a b =
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun a' ->
let (q, r) = pos_div_eucl a' b in
let r' = add (mul ((fun p -> 2. *. p) 1.) r) 1. in
@@ -360,18 +365,18 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val div_eucl : float -> float -> float * float **)
let div_eucl a b =
- (fun f0 fp fn z -> if z=0. then f0 () else if z>0. then fp z else fn (~-. z))
+ (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
(fun _ -> (0.,
0.))
(fun a' ->
- (fun f0 fp fn z -> if z=0. then f0 () else if z>0. then fp z else fn (~-. z))
+ (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
(fun _ -> (0.,
0.))
(fun p ->
pos_div_eucl a' b)
(fun b' ->
let (q, r) = pos_div_eucl a' b' in
- ((fun f0 fp fn z -> if z=0. then f0 () else if z>0. then fp z else fn (~-. z))
+ ((fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
(fun _ -> ((opp q),
0.))
(fun p -> ((opp (add q 1.)),
@@ -381,12 +386,12 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
r))
b)
(fun a' ->
- (fun f0 fp fn z -> if z=0. then f0 () else if z>0. then fp z else fn (~-. z))
+ (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
(fun _ -> (0.,
0.))
(fun p ->
let (q, r) = pos_div_eucl a' b in
- ((fun f0 fp fn z -> if z=0. then f0 () else if z>0. then fp z else fn (~-. z))
+ ((fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
(fun _ -> ((opp q),
0.))
(fun p0 -> ((opp (add q 1.)),
@@ -412,11 +417,11 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val quotrem : float -> float -> float * float **)
let quotrem a b =
- (fun f0 fp fn z -> if z=0. then f0 () else if z>0. then fp z else fn (~-. z))
+ (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
(fun _ -> (0.,
0.))
(fun a0 ->
- (fun f0 fp fn z -> if z=0. then f0 () else if z>0. then fp z else fn (~-. z))
+ (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
(fun _ -> (0.,
a))
(fun b0 ->
@@ -425,7 +430,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
let (q, r) = N.pos_div_eucl a0 b0 in ((opp (of_N q)), (of_N r)))
b)
(fun a0 ->
- (fun f0 fp fn z -> if z=0. then f0 () else if z>0. then fp z else fn (~-. z))
+ (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
(fun _ -> (0.,
a))
(fun b0 ->
@@ -448,12 +453,12 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val even : float -> bool **)
let even z =
- (fun f0 fp fn z -> if z=0. then f0 () else if z>0. then fp z else fn (~-. z))
+ (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
(fun _ ->
true)
(fun p ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p0 ->
false)
(fun p0 ->
@@ -463,7 +468,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
p)
(fun p ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p0 ->
false)
(fun p0 ->
@@ -476,12 +481,12 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val odd : float -> bool **)
let odd z =
- (fun f0 fp fn z -> if z=0. then f0 () else if z>0. then fp z else fn (~-. z))
+ (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
(fun _ ->
false)
(fun p ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p0 ->
true)
(fun p0 ->
@@ -491,7 +496,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
p)
(fun p ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p0 ->
true)
(fun p0 ->
@@ -504,12 +509,12 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val div2 : float -> float **)
let div2 z =
- (fun f0 fp fn z -> if z=0. then f0 () else if z>0. then fp z else fn (~-. z))
+ (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
(fun _ ->
0.)
(fun p ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p0 ->
(Pos.div2 p))
(fun p0 ->
@@ -524,12 +529,12 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val quot2 : float -> float **)
let quot2 z =
- (fun f0 fp fn z -> if z=0. then f0 () else if z>0. then fp z else fn (~-. z))
+ (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
(fun _ ->
0.)
(fun p ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p0 ->
(Pos.div2 p))
(fun p0 ->
@@ -539,7 +544,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
p)
(fun p ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p0 -> (~-.)
(Pos.div2 p))
(fun p0 -> (~-.)
@@ -552,12 +557,12 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val log2 : float -> float **)
let log2 z =
- (fun f0 fp fn z -> if z=0. then f0 () else if z>0. then fp z else fn (~-. z))
+ (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
(fun _ ->
0.)
(fun p0 ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p ->
(Pos.size p))
(fun p ->
@@ -572,7 +577,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val sqrtrem : float -> float * float **)
let sqrtrem n =
- (fun f0 fp fn z -> if z=0. then f0 () else if z>0. then fp z else fn (~-. z))
+ (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
(fun _ -> (0.,
0.))
(fun p ->
@@ -588,7 +593,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val sqrt : float -> float **)
let sqrt n =
- (fun f0 fp fn z -> if z=0. then f0 () else if z>0. then fp z else fn (~-. z))
+ (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
(fun _ ->
0.)
(fun p ->
@@ -600,11 +605,11 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val gcd : float -> float -> float **)
let gcd a b =
- (fun f0 fp fn z -> if z=0. then f0 () else if z>0. then fp z else fn (~-. z))
+ (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
(fun _ ->
abs b)
(fun a0 ->
- (fun f0 fp fn z -> if z=0. then f0 () else if z>0. then fp z else fn (~-. z))
+ (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
(fun _ ->
abs a)
(fun b0 ->
@@ -613,7 +618,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(Pos.gcd a0 b0))
b)
(fun a0 ->
- (fun f0 fp fn z -> if z=0. then f0 () else if z>0. then fp z else fn (~-. z))
+ (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
(fun _ ->
abs a)
(fun b0 ->
@@ -626,11 +631,11 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val ggcd : float -> float -> float * (float * float) **)
let ggcd a b =
- (fun f0 fp fn z -> if z=0. then f0 () else if z>0. then fp z else fn (~-. z))
+ (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
(fun _ -> ((abs b), (0.,
(sgn b))))
(fun a0 ->
- (fun f0 fp fn z -> if z=0. then f0 () else if z>0. then fp z else fn (~-. z))
+ (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
(fun _ -> ((abs a), ((sgn a),
0.)))
(fun b0 ->
@@ -640,7 +645,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
let (aa, bb) = p in (g, (aa, ((~-.) bb))))
b)
(fun a0 ->
- (fun f0 fp fn z -> if z=0. then f0 () else if z>0. then fp z else fn (~-. z))
+ (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
(fun _ -> ((abs a), ((sgn a),
0.)))
(fun b0 ->
@@ -655,11 +660,11 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val testbit : float -> float -> bool **)
let testbit a n =
- (fun f0 fp fn z -> if z=0. then f0 () else if z>0. then fp z else fn (~-. z))
+ (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
(fun _ ->
odd a)
(fun p ->
- (fun f0 fp fn z -> if z=0. then f0 () else if z>0. then fp z else fn (~-. z))
+ (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
(fun _ ->
false)
(fun a0 ->
@@ -674,7 +679,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val shiftl : float -> float -> float **)
let shiftl a n =
- (fun f0 fp fn z -> if z=0. then f0 () else if z>0. then fp z else fn (~-. z))
+ (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
(fun _ ->
a)
(fun p ->
@@ -691,11 +696,11 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val coq_lor : float -> float -> float **)
let coq_lor a b =
- (fun f0 fp fn z -> if z=0. then f0 () else if z>0. then fp z else fn (~-. z))
+ (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
(fun _ ->
b)
(fun a0 ->
- (fun f0 fp fn z -> if z=0. then f0 () else if z>0. then fp z else fn (~-. z))
+ (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
(fun _ ->
a)
(fun b0 ->
@@ -704,7 +709,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(N.succ_pos (N.ldiff (Pos.pred_N b0) a0)))
b)
(fun a0 ->
- (fun f0 fp fn z -> if z=0. then f0 () else if z>0. then fp z else fn (~-. z))
+ (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
(fun _ ->
a)
(fun b0 -> (~-.)
@@ -717,11 +722,11 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val coq_land : float -> float -> float **)
let coq_land a b =
- (fun f0 fp fn z -> if z=0. then f0 () else if z>0. then fp z else fn (~-. z))
+ (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
(fun _ ->
0.)
(fun a0 ->
- (fun f0 fp fn z -> if z=0. then f0 () else if z>0. then fp z else fn (~-. z))
+ (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
(fun _ ->
0.)
(fun b0 ->
@@ -730,7 +735,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
of_N (N.ldiff a0 (Pos.pred_N b0)))
b)
(fun a0 ->
- (fun f0 fp fn z -> if z=0. then f0 () else if z>0. then fp z else fn (~-. z))
+ (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
(fun _ ->
0.)
(fun b0 ->
@@ -743,11 +748,11 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val ldiff : float -> float -> float **)
let ldiff a b =
- (fun f0 fp fn z -> if z=0. then f0 () else if z>0. then fp z else fn (~-. z))
+ (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
(fun _ ->
0.)
(fun a0 ->
- (fun f0 fp fn z -> if z=0. then f0 () else if z>0. then fp z else fn (~-. z))
+ (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
(fun _ ->
a)
(fun b0 ->
@@ -756,7 +761,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
of_N (N.coq_land a0 (Pos.pred_N b0)))
b)
(fun a0 ->
- (fun f0 fp fn z -> if z=0. then f0 () else if z>0. then fp z else fn (~-. z))
+ (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
(fun _ ->
a)
(fun b0 -> (~-.)
@@ -769,11 +774,11 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val coq_lxor : float -> float -> float **)
let coq_lxor a b =
- (fun f0 fp fn z -> if z=0. then f0 () else if z>0. then fp z else fn (~-. z))
+ (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
(fun _ ->
b)
(fun a0 ->
- (fun f0 fp fn z -> if z=0. then f0 () else if z>0. then fp z else fn (~-. z))
+ (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
(fun _ ->
a)
(fun b0 ->
@@ -782,7 +787,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(N.succ_pos (N.coq_lxor a0 (Pos.pred_N b0))))
b)
(fun a0 ->
- (fun f0 fp fn z -> if z=0. then f0 () else if z>0. then fp z else fn (~-. z))
+ (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
(fun _ ->
a)
(fun b0 -> (~-.)
@@ -795,9 +800,9 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val eq_dec : float -> float -> bool **)
let eq_dec x y =
- ((fun f0 fp fn z -> if z=0. then f0 () else if z>0. then fp z else fn (~-. z))
+ ((fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
(fun _ y0 ->
- (fun f0 fp fn z -> if z=0. then f0 () else if z>0. then fp z else fn (~-. z))
+ (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
(fun _ ->
true)
(fun p ->
@@ -806,7 +811,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
false)
y0)
(fun x0 y0 ->
- (fun f0 fp fn z -> if z=0. then f0 () else if z>0. then fp z else fn (~-. z))
+ (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
(fun _ ->
false)
(fun p0 ->
@@ -815,7 +820,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
false)
y0)
(fun x0 y0 ->
- (fun f0 fp fn z -> if z=0. then f0 () else if z>0. then fp z else fn (~-. z))
+ (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
(fun _ ->
false)
(fun p0 ->
diff --git a/generator/tests/jsref/BinNat.ml b/generator/tests/jsref/BinNat.ml
index 394b02a..3968878 100644
--- a/generator/tests/jsref/BinNat.ml
+++ b/generator/tests/jsref/BinNat.ml
@@ -11,7 +11,11 @@ let __ = let rec f _ = Obj.repr f in Obj.repr f
module N =
struct
type t = float
-
+
+ (* HACK *)
+ let is_even p =
+ float_eq (mod_float p 2.) 0.
+
(** val zero : float **)
let zero =
@@ -30,7 +34,7 @@ module N =
(** val succ_double : float -> float **)
let succ_double x =
- (fun f0 fp n -> if n=0. then f0 () else fp n)
+ (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
(fun _ ->
1.)
(fun p -> ((fun p -> 1. +. (2. *. p))
@@ -40,7 +44,7 @@ module N =
(** val double : float -> float **)
let double n =
- (fun f0 fp n -> if n=0. then f0 () else fp n)
+ (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
(fun _ ->
0.)
(fun p -> ((fun p -> 2. *. p)
@@ -58,7 +62,7 @@ module N =
(** val succ_pos : float -> float **)
let succ_pos n =
- (fun f0 fp n -> if n=0. then f0 () else fp n)
+ (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
(fun _ ->
1.)
(fun p ->
@@ -79,21 +83,21 @@ module N =
(** val compare : float -> float -> comparison **)
- let compare = fun x y -> if x=y then Eq else if x<y then Lt else Gt
+ let compare = fun x y -> if float_eq x y then Eq else if x<y then Lt else Gt
(** val eqb : float -> float -> bool **)
let rec eqb n m =
- (fun f0 fp n -> if n=0. then f0 () else fp n)
+ (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
(fun _ ->
- (fun f0 fp n -> if n=0. then f0 () else fp n)
+ (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
(fun _ ->
true)
(fun p ->
false)
m)
(fun p ->
- (fun f0 fp n -> if n=0. then f0 () else fp n)
+ (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
(fun _ ->
false)
(fun q ->
@@ -128,12 +132,12 @@ module N =
(** val div2 : float -> float **)
let div2 n =
- (fun f0 fp n -> if n=0. then f0 () else fp n)
+ (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
(fun _ ->
0.)
(fun p0 ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p ->
p)
(fun p ->
@@ -146,12 +150,12 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val even : float -> bool **)
let even n =
- (fun f0 fp n -> if n=0. then f0 () else fp n)
+ (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
(fun _ ->
true)
(fun p ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p0 ->
false)
(fun p0 ->
@@ -169,11 +173,11 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val pow : float -> float -> float **)
let pow n p =
- (fun f0 fp n -> if n=0. then f0 () else fp n)
+ (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
(fun _ ->
1.)
(fun p0 ->
- (fun f0 fp n -> if n=0. then f0 () else fp n)
+ (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
(fun _ ->
0.)
(fun q ->
@@ -184,7 +188,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val square : float -> float **)
let square n =
- (fun f0 fp n -> if n=0. then f0 () else fp n)
+ (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
(fun _ ->
0.)
(fun p ->
@@ -194,12 +198,12 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val log2 : float -> float **)
let log2 n =
- (fun f0 fp n -> if n=0. then f0 () else fp n)
+ (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
(fun _ ->
0.)
(fun p0 ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p ->
(Pos.size p))
(fun p ->
@@ -212,7 +216,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val size : float -> float **)
let size n =
- (fun f0 fp n -> if n=0. then f0 () else fp n)
+ (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
(fun _ ->
0.)
(fun p ->
@@ -222,7 +226,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val size_nat : float -> int **)
let size_nat n =
- (fun f0 fp n -> if n=0. then f0 () else fp n)
+ (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
(fun _ ->
0)
(fun p ->
@@ -233,7 +237,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
let rec pos_div_eucl a b =
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun a' ->
let (q, r) = pos_div_eucl a' b in
let r' = succ_double r in
@@ -243,12 +247,12 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
let r' = double r in
if leb b r' then ((succ_double q), (sub r' b)) else ((double q), r'))
(fun _ ->
- (fun f0 fp n -> if n=0. then f0 () else fp n)
+ (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
(fun _ -> (0.,
1.))
(fun p ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p0 -> (0.,
1.))
(fun p0 -> (0.,
@@ -262,11 +266,11 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val div_eucl : float -> float -> float * float **)
let div_eucl a b =
- (fun f0 fp n -> if n=0. then f0 () else fp n)
+ (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
(fun _ -> (0.,
0.))
(fun na ->
- (fun f0 fp n -> if n=0. then f0 () else fp n)
+ (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
(fun _ -> (0.,
a))
(fun p ->
@@ -276,7 +280,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val div : float -> float -> float **)
- let div = (fun x y -> if x = 0. then 0. else floor (x /. y))
+ let div = (fun x y -> if float_eq x 0. then 0. else floor (x /. y))
(** val modulo : float -> float -> float **)
@@ -285,11 +289,11 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val gcd : float -> float -> float **)
let gcd a b =
- (fun f0 fp n -> if n=0. then f0 () else fp n)
+ (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
(fun _ ->
b)
(fun p ->
- (fun f0 fp n -> if n=0. then f0 () else fp n)
+ (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
(fun _ ->
a)
(fun q ->
@@ -300,11 +304,11 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val ggcd : float -> float -> float * (float * float) **)
let ggcd a b =
- (fun f0 fp n -> if n=0. then f0 () else fp n)
+ (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
(fun _ -> (b, (0.,
1.)))
(fun p ->
- (fun f0 fp n -> if n=0. then f0 () else fp n)
+ (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
(fun _ -> (a, (1.,
0.)))
(fun q ->
@@ -315,7 +319,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val sqrtrem : float -> float * float **)
let sqrtrem n =
- (fun f0 fp n -> if n=0. then f0 () else fp n)
+ (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
(fun _ -> (0.,
0.))
(fun p ->
@@ -329,7 +333,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val sqrt : float -> float **)
let sqrt n =
- (fun f0 fp n -> if n=0. then f0 () else fp n)
+ (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
(fun _ ->
0.)
(fun p ->
@@ -339,11 +343,11 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val coq_lor : float -> float -> float **)
let coq_lor n m =
- (fun f0 fp n -> if n=0. then f0 () else fp n)
+ (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
(fun _ ->
m)
(fun p ->
- (fun f0 fp n -> if n=0. then f0 () else fp n)
+ (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
(fun _ ->
n)
(fun q ->
@@ -354,11 +358,11 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val coq_land : float -> float -> float **)
let coq_land n m =
- (fun f0 fp n -> if n=0. then f0 () else fp n)
+ (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
(fun _ ->
0.)
(fun p ->
- (fun f0 fp n -> if n=0. then f0 () else fp n)
+ (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
(fun _ ->
0.)
(fun q ->
@@ -369,11 +373,11 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val ldiff : float -> float -> float **)
let rec ldiff n m =
- (fun f0 fp n -> if n=0. then f0 () else fp n)
+ (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
(fun _ ->
0.)
(fun p ->
- (fun f0 fp n -> if n=0. then f0 () else fp n)
+ (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
(fun _ ->
n)
(fun q ->
@@ -384,11 +388,11 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val coq_lxor : float -> float -> float **)
let coq_lxor n m =
- (fun f0 fp n -> if n=0. then f0 () else fp n)
+ (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
(fun _ ->
m)
(fun p ->
- (fun f0 fp n -> if n=0. then f0 () else fp n)
+ (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
(fun _ ->
n)
(fun q ->
@@ -409,7 +413,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val shiftl : float -> float -> float **)
let shiftl a n =
- (fun f0 fp n -> if n=0. then f0 () else fp n)
+ (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
(fun _ ->
0.)
(fun a0 ->
@@ -419,7 +423,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val shiftr : float -> float -> float **)
let shiftr a n =
- (fun f0 fp n -> if n=0. then f0 () else fp n)
+ (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
(fun _ ->
a)
(fun p ->
@@ -429,7 +433,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val testbit_nat : float -> int -> bool **)
let testbit_nat a =
- (fun f0 fp n -> if n=0. then f0 () else fp n)
+ (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
(fun _ x ->
false)
(fun p ->
@@ -439,7 +443,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val testbit : float -> float -> bool **)
let testbit a n =
- (fun f0 fp n -> if n=0. then f0 () else fp n)
+ (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
(fun _ ->
false)
(fun p ->
@@ -449,7 +453,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val to_nat : float -> int **)
let to_nat a =
- (fun f0 fp n -> if n=0. then f0 () else fp n)
+ (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
(fun _ ->
0)
(fun p ->
@@ -459,7 +463,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val of_nat : int -> float **)
let of_nat n =
- (fun fO fS n -> if n=0 then fO () else fS (n-1))
+ (fun fO fS n -> if int_eq n 0 then fO () else fS (n-1))
(fun _ ->
0.)
(fun n' ->
@@ -469,7 +473,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val iter : float -> ('a1 -> 'a1) -> 'a1 -> 'a1 **)
let iter n f x =
- (fun f0 fp n -> if n=0. then f0 () else fp n)
+ (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
(fun _ ->
x)
(fun p ->
@@ -479,16 +483,16 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val eq_dec : float -> float -> bool **)
let eq_dec n m =
- ((fun f0 fp n -> if n=0. then f0 () else fp n)
+ ((fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
(fun _ m0 ->
- (fun f0 fp n -> if n=0. then f0 () else fp n)
+ (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
(fun _ ->
true)
(fun p ->
false)
m0)
(fun x m0 ->
- (fun f0 fp n -> if n=0. then f0 () else fp n)
+ (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
(fun _ ->
false)
(fun p0 ->
@@ -499,7 +503,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val discr : float -> float option **)
let discr n =
- (fun f0 fp n -> if n=0. then f0 () else fp n)
+ (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
(fun _ ->
None)
(fun p -> Some
@@ -512,13 +516,13 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
let binary_rect f0 f2 fS2 n =
let f2' = fun p -> f2 p in
let fS2' = fun p -> fS2 p in
- ((fun f0 fp n -> if n=0. then f0 () else fp n)
+ ((fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
(fun _ ->
f0)
(fun p ->
let rec f p0 =
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p1 ->
fS2' p1 (f p1))
(fun p1 ->
@@ -539,7 +543,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
let peano_rect f0 f n =
let f' = fun p -> f p in
- ((fun f0 fp n -> if n=0. then f0 () else fp n)
+ ((fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
(fun _ ->
f0)
(fun p ->
diff --git a/generator/tests/jsref/BinPos.ml b/generator/tests/jsref/BinPos.ml
index 1a61483..6bd8cc3 100644
--- a/generator/tests/jsref/BinPos.ml
+++ b/generator/tests/jsref/BinPos.ml
@@ -12,6 +12,11 @@ module Pos =
struct
type t = float
+ (* HACK *)
+ let is_even p =
+ float_eq (mod_float p 2.) 0.
+
+
(** val succ : float -> float **)
let rec succ = (+.) 1.
@@ -24,10 +29,10 @@ module Pos =
and add_carry x y =
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun q -> (fun p -> 1. +. (2. *. p))
(add_carry p q))
(fun q -> (fun p -> 2. *. p)
@@ -37,7 +42,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
y)
(fun p ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun q -> (fun p -> 2. *. p)
(add_carry p q))
(fun q -> (fun p -> 1. +. (2. *. p))
@@ -47,7 +52,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
y)
(fun _ ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun q -> (fun p -> 1. +. (2. *. p))
(succ q))
(fun q -> (fun p -> 2. *. p)
@@ -61,7 +66,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
let rec pred_double x =
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p -> (fun p -> 1. +. (2. *. p)) ((fun p -> 2. *. p)
p))
(fun p -> (fun p -> 1. +. (2. *. p))
@@ -78,7 +83,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
let pred_N x =
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p -> ((fun p -> 2. *. p)
p))
(fun p ->
@@ -124,7 +129,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
let double_pred_mask x =
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p -> IsPos ((fun p -> 2. *. p) ((fun p -> 2. *. p)
p)))
(fun p -> IsPos ((fun p -> 2. *. p)
@@ -139,7 +144,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
| IsNul -> IsNeg
| IsPos q ->
((fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p0 -> IsPos
(pred q))
(fun p0 -> IsPos
@@ -153,10 +158,10 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
let rec sub_mask x y =
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun q ->
double_mask (sub_mask p q))
(fun q ->
@@ -166,7 +171,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
y)
(fun p ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun q ->
succ_double_mask (sub_mask_carry p q))
(fun q ->
@@ -176,7 +181,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
y)
(fun _ ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p ->
IsNeg)
(fun p ->
@@ -190,10 +195,10 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
and sub_mask_carry x y =
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun q ->
succ_double_mask (sub_mask_carry p q))
(fun q ->
@@ -203,7 +208,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
y)
(fun p ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun q ->
double_mask (sub_mask_carry p q))
(fun q ->
@@ -227,7 +232,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
let rec iter n f x =
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun n' ->
f (iter n' f (iter n' f x)))
(fun n' ->
@@ -245,7 +250,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
let rec square p =
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p0 -> (fun p -> 1. +. (2. *. p)) ((fun p -> 2. *. p)
(add (square p0) p0)))
(fun p0 -> (fun p -> 2. *. p) ((fun p -> 2. *. p)
@@ -258,7 +263,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
let div2 p =
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p0 ->
p0)
(fun p0 ->
@@ -271,7 +276,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
let div2_up p =
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p0 ->
succ p0)
(fun p0 ->
@@ -284,7 +289,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
let rec size_nat p =
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p0 -> Pervasives.succ
(size_nat p0))
(fun p0 -> Pervasives.succ
@@ -297,7 +302,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
let rec size p =
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p0 ->
succ (size p0))
(fun p0 ->
@@ -308,11 +313,11 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val compare_cont : float -> float -> comparison -> comparison **)
- let rec compare_cont = fun x y c -> if x=y then c else if x<y then Lt else Gt
+ let rec compare_cont = fun x y c -> if float_eq x y then c else if x<y then Lt else Gt
(** val compare : float -> float -> comparison **)
- let compare = fun x y -> if x=y then Eq else if x<y then Lt else Gt
+ let compare = fun x y -> if float_eq x y then Eq else if x<y then Lt else Gt
(** val min : float -> float -> float **)
@@ -326,10 +331,10 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
let rec eqb p q =
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p0 ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun q0 ->
eqb p0 q0)
(fun p1 ->
@@ -339,7 +344,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
q)
(fun p0 ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p1 ->
false)
(fun q0 ->
@@ -349,7 +354,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
q)
(fun _ ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p0 ->
false)
(fun p0 ->
@@ -398,10 +403,10 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
let rec sqrtrem p =
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p0 ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p1 ->
sqrtrem_step (fun x -> (fun p -> 1. +. (2. *. p)) x) (fun x ->
(fun p -> 1. +. (2. *. p)) x) (sqrtrem p1))
@@ -413,7 +418,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
p0)
(fun p0 ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p1 ->
sqrtrem_step (fun x -> (fun p -> 1. +. (2. *. p)) x) (fun x ->
(fun p -> 2. *. p) x) (sqrtrem p1))
@@ -435,15 +440,15 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val gcdn : int -> float -> float -> float **)
let rec gcdn n a b =
- (fun fO fS n -> if n=0 then fO () else fS (n-1))
+ (fun fO fS n -> if int_eq n 0 then fO () else fS (n-1))
(fun _ ->
1.)
(fun n0 ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun a' ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun b' ->
match compare a' b' with
| Eq -> a
@@ -456,7 +461,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
b)
(fun a0 ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p ->
gcdn n0 a0 b)
(fun b0 -> (fun p -> 2. *. p)
@@ -477,15 +482,15 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val ggcdn : int -> float -> float -> float * (float * float) **)
let rec ggcdn n a b =
- (fun fO fS n -> if n=0 then fO () else fS (n-1))
+ (fun fO fS n -> if int_eq n 0 then fO () else fS (n-1))
(fun _ -> (1., (a,
b)))
(fun n0 ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun a' ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun b' ->
match compare a' b' with
| Eq -> (a, (1., 1.))
@@ -503,7 +508,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
b)
(fun a0 ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p ->
let (g, p0) = ggcdn n0 a0 b in
let (aa, bb) = p0 in (g, (((fun p -> 2. *. p) aa), bb)))
@@ -525,7 +530,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val coq_Nsucc_double : float -> float **)
let coq_Nsucc_double x =
- (fun f0 fp n -> if n=0. then f0 () else fp n)
+ (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
(fun _ ->
1.)
(fun p -> ((fun p -> 1. +. (2. *. p))
@@ -535,7 +540,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val coq_Ndouble : float -> float **)
let coq_Ndouble n =
- (fun f0 fp n -> if n=0. then f0 () else fp n)
+ (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
(fun _ ->
0.)
(fun p -> ((fun p -> 2. *. p)
@@ -546,10 +551,10 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
let rec coq_lor p q =
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p0 ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun q0 -> (fun p -> 1. +. (2. *. p))
(coq_lor p0 q0))
(fun q0 -> (fun p -> 1. +. (2. *. p))
@@ -559,7 +564,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
q)
(fun p0 ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun q0 -> (fun p -> 1. +. (2. *. p))
(coq_lor p0 q0))
(fun q0 -> (fun p -> 2. *. p)
@@ -569,7 +574,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
q)
(fun _ ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p0 ->
q)
(fun q0 -> (fun p -> 1. +. (2. *. p))
@@ -583,10 +588,10 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
let rec coq_land p q =
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p0 ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun q0 ->
coq_Nsucc_double (coq_land p0 q0))
(fun q0 ->
@@ -596,7 +601,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
q)
(fun p0 ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun q0 ->
coq_Ndouble (coq_land p0 q0))
(fun q0 ->
@@ -606,7 +611,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
q)
(fun _ ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p0 ->
1.)
(fun q0 ->
@@ -620,10 +625,10 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
let rec ldiff p q =
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p0 ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun q0 ->
coq_Ndouble (ldiff p0 q0))
(fun q0 ->
@@ -633,7 +638,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
q)
(fun p0 ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun q0 ->
coq_Ndouble (ldiff p0 q0))
(fun q0 ->
@@ -643,7 +648,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
q)
(fun _ ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p0 ->
0.)
(fun q0 ->
@@ -657,10 +662,10 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
let rec coq_lxor p q =
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p0 ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun q0 ->
coq_Ndouble (coq_lxor p0 q0))
(fun q0 ->
@@ -670,7 +675,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
q)
(fun p0 ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun q0 ->
coq_Nsucc_double (coq_lxor p0 q0))
(fun q0 ->
@@ -680,7 +685,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
q)
(fun _ ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun q0 -> ((fun p -> 2. *. p)
q0))
(fun q0 -> ((fun p -> 1. +. (2. *. p))
@@ -703,7 +708,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val shiftl : float -> float -> float **)
let shiftl p n =
- (fun f0 fp n -> if n=0. then f0 () else fp n)
+ (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
(fun _ ->
p)
(fun n0 ->
@@ -713,7 +718,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val shiftr : float -> float -> float **)
let shiftr p n =
- (fun f0 fp n -> if n=0. then f0 () else fp n)
+ (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
(fun _ ->
p)
(fun n0 ->
@@ -724,23 +729,23 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
let rec testbit_nat p =
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p0 n ->
- (fun fO fS n -> if n=0 then fO () else fS (n-1))
+ (fun fO fS n -> if int_eq n 0 then fO () else fS (n-1))
(fun _ ->
true)
(fun n' ->
testbit_nat p0 n')
n)
(fun p0 n ->
- (fun fO fS n -> if n=0 then fO () else fS (n-1))
+ (fun fO fS n -> if int_eq n 0 then fO () else fS (n-1))
(fun _ ->
false)
(fun n' ->
testbit_nat p0 n')
n)
(fun _ n ->
- (fun fO fS n -> if n=0 then fO () else fS (n-1))
+ (fun fO fS n -> if int_eq n 0 then fO () else fS (n-1))
(fun _ ->
true)
(fun n0 ->
@@ -752,23 +757,23 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
let rec testbit p n =
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p0 ->
- (fun f0 fp n -> if n=0. then f0 () else fp n)
+ (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
(fun _ ->
true)
(fun n0 ->
testbit p0 (pred_N n0))
n)
(fun p0 ->
- (fun f0 fp n -> if n=0. then f0 () else fp n)
+ (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
(fun _ ->
false)
(fun n0 ->
testbit p0 (pred_N n0))
n)
(fun _ ->
- (fun f0 fp n -> if n=0. then f0 () else fp n)
+ (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
(fun _ ->
true)
(fun p0 ->
@@ -781,7 +786,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
let iter_op op =
let rec iter0 p a =
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p0 ->
op a (iter0 p0 (op a a)))
(fun p0 ->
@@ -799,11 +804,11 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val of_nat : int -> float **)
let rec of_nat n =
- (fun fO fS n -> if n=0 then fO () else fS (n-1))
+ (fun fO fS n -> if int_eq n 0 then fO () else fS (n-1))
(fun _ ->
1.)
(fun x ->
- (fun fO fS n -> if n=0 then fO () else fS (n-1))
+ (fun fO fS n -> if int_eq n 0 then fO () else fS (n-1))
(fun _ ->
1.)
(fun n0 ->
@@ -814,7 +819,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val of_succ_nat : int -> float **)
let rec of_succ_nat n =
- (fun fO fS n -> if n=0 then fO () else fS (n-1))
+ (fun fO fS n -> if int_eq n 0 then fO () else fS (n-1))
(fun _ ->
1.)
(fun x ->
@@ -826,10 +831,10 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
let eq_dec x y =
let rec f p =
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p0 y0 ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p1 ->
if f p0 p1 then true else false)
(fun p1 ->
@@ -839,7 +844,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
y0)
(fun p0 y0 ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p1 ->
false)
(fun p1 ->
@@ -849,7 +854,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
y0)
(fun _ y0 ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p0 ->
false)
(fun p0 ->
@@ -868,7 +873,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
f (succ ((fun p -> 2. *. p) p0)) (f ((fun p -> 2. *. p) p0) x))
in
((fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun q ->
f ((fun p -> 2. *. p) q) (f2 q))
(fun q ->
@@ -922,7 +927,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
let rec peanoView p =
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p0 ->
peanoView_xI p0 (peanoView p0))
(fun p0 ->
diff --git a/generator/tests/jsref/BinPosDef.ml b/generator/tests/jsref/BinPosDef.ml
index 1b910c6..5ef3d33 100644
--- a/generator/tests/jsref/BinPosDef.ml
+++ b/generator/tests/jsref/BinPosDef.ml
@@ -5,11 +5,17 @@ module Pos =
struct
type t = float
+
+ (* HACK *)
+ let is_even p =
+ float_eq (mod_float p 2.) 0.
+
+
(** val succ : float -> float **)
let rec succ x =
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p -> (fun p -> 2. *. p)
(succ p))
(fun p -> (fun p -> 1. +. (2. *. p))
@@ -22,10 +28,10 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
let rec add x y =
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun q -> (fun p -> 2. *. p)
(add_carry p q))
(fun q -> (fun p -> 1. +. (2. *. p))
@@ -35,7 +41,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
y)
(fun p ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun q -> (fun p -> 1. +. (2. *. p))
(add p q))
(fun q -> (fun p -> 2. *. p)
@@ -45,7 +51,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
y)
(fun _ ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun q -> (fun p -> 2. *. p)
(succ q))
(fun q -> (fun p -> 1. +. (2. *. p))
@@ -59,10 +65,10 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
and add_carry x y =
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun q -> (fun p -> 1. +. (2. *. p))
(add_carry p q))
(fun q -> (fun p -> 2. *. p)
@@ -72,7 +78,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
y)
(fun p ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun q -> (fun p -> 2. *. p)
(add_carry p q))
(fun q -> (fun p -> 1. +. (2. *. p))
@@ -82,7 +88,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
y)
(fun _ ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun q -> (fun p -> 1. +. (2. *. p))
(succ q))
(fun q -> (fun p -> 2. *. p)
@@ -96,7 +102,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
let rec pred_double x =
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p -> (fun p -> 1. +. (2. *. p)) ((fun p -> 2. *. p)
p))
(fun p -> (fun p -> 1. +. (2. *. p))
@@ -109,7 +115,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
let pred x =
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p -> (fun p -> 2. *. p)
p)
(fun p ->
@@ -122,7 +128,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
let pred_N x =
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p -> ((fun p -> 2. *. p)
p))
(fun p ->
@@ -168,7 +174,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
let double_pred_mask x =
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p -> IsPos ((fun p -> 2. *. p) ((fun p -> 2. *. p)
p)))
(fun p -> IsPos ((fun p -> 2. *. p)
@@ -183,7 +189,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
| IsNul -> IsNeg
| IsPos q ->
((fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p0 -> IsPos
(pred q))
(fun p0 -> IsPos
@@ -197,10 +203,10 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
let rec sub_mask x y =
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun q ->
double_mask (sub_mask p q))
(fun q ->
@@ -210,7 +216,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
y)
(fun p ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun q ->
succ_double_mask (sub_mask_carry p q))
(fun q ->
@@ -220,7 +226,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
y)
(fun _ ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p ->
IsNeg)
(fun p ->
@@ -234,10 +240,10 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
and sub_mask_carry x y =
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun q ->
succ_double_mask (sub_mask_carry p q))
(fun q ->
@@ -247,7 +253,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
y)
(fun p ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun q ->
double_mask (sub_mask_carry p q))
(fun q ->
@@ -271,7 +277,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
let rec mul x y =
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p ->
add y ((fun p -> 2. *. p) (mul p y)))
(fun p -> (fun p -> 2. *. p)
@@ -284,7 +290,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
let rec iter n f x =
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun n' ->
f (iter n' f (iter n' f x)))
(fun n' ->
@@ -302,7 +308,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
let rec square p =
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p0 -> (fun p -> 1. +. (2. *. p)) ((fun p -> 2. *. p)
(add (square p0) p0)))
(fun p0 -> (fun p -> 2. *. p) ((fun p -> 2. *. p)
@@ -315,7 +321,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
let div2 p =
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p0 ->
p0)
(fun p0 ->
@@ -328,7 +334,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
let div2_up p =
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p0 ->
succ p0)
(fun p0 ->
@@ -341,7 +347,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
let rec size_nat p =
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p0 -> Pervasives.succ
(size_nat p0))
(fun p0 -> Pervasives.succ
@@ -354,7 +360,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
let rec size p =
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p0 ->
succ (size p0))
(fun p0 ->
@@ -367,10 +373,10 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
let rec compare_cont x y r =
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun q ->
compare_cont p q r)
(fun q ->
@@ -380,7 +386,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
y)
(fun p ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun q ->
compare_cont p q Lt)
(fun q ->
@@ -390,7 +396,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
y)
(fun _ ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun q ->
Lt)
(fun q ->
@@ -425,10 +431,10 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
let rec eqb p q =
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p0 ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun q0 ->
eqb p0 q0)
(fun p1 ->
@@ -438,7 +444,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
q)
(fun p0 ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p1 ->
false)
(fun q0 ->
@@ -448,7 +454,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
q)
(fun _ ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p0 ->
false)
(fun p0 ->
@@ -497,10 +503,10 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
let rec sqrtrem p =
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p0 ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p1 ->
sqrtrem_step (fun x -> (fun p -> 1. +. (2. *. p)) x) (fun x ->
(fun p -> 1. +. (2. *. p)) x) (sqrtrem p1))
@@ -512,7 +518,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
p0)
(fun p0 ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p1 ->
sqrtrem_step (fun x -> (fun p -> 1. +. (2. *. p)) x) (fun x ->
(fun p -> 2. *. p) x) (sqrtrem p1))
@@ -534,15 +540,15 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val gcdn : int -> float -> float -> float **)
let rec gcdn n a b =
- (fun fO fS n -> if n=0 then fO () else fS (n-1))
+ (fun fO fS n -> if int_eq n 0 then fO () else fS (n-1))
(fun _ ->
1.)
(fun n0 ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun a' ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun b' ->
match compare a' b' with
| Eq -> a
@@ -555,7 +561,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
b)
(fun a0 ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p ->
gcdn n0 a0 b)
(fun b0 -> (fun p -> 2. *. p)
@@ -576,15 +582,15 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val ggcdn : int -> float -> float -> float * (float * float) **)
let rec ggcdn n a b =
- (fun fO fS n -> if n=0 then fO () else fS (n-1))
+ (fun fO fS n -> if int_eq n 0 then fO () else fS (n-1))
(fun _ -> (1., (a,
b)))
(fun n0 ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun a' ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun b' ->
match compare a' b' with
| Eq -> (a, (1., 1.))
@@ -602,7 +608,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
b)
(fun a0 ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p ->
let (g, p0) = ggcdn n0 a0 b in
let (aa, bb) = p0 in (g, (((fun p -> 2. *. p) aa), bb)))
@@ -624,7 +630,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val coq_Nsucc_double : float -> float **)
let coq_Nsucc_double x =
- (fun f0 fp n -> if n=0. then f0 () else fp n)
+ (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
(fun _ ->
1.)
(fun p -> ((fun p -> 1. +. (2. *. p))
@@ -634,7 +640,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val coq_Ndouble : float -> float **)
let coq_Ndouble n =
- (fun f0 fp n -> if n=0. then f0 () else fp n)
+ (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
(fun _ ->
0.)
(fun p -> ((fun p -> 2. *. p)
@@ -645,10 +651,10 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
let rec coq_lor p q =
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p0 ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun q0 -> (fun p -> 1. +. (2. *. p))
(coq_lor p0 q0))
(fun q0 -> (fun p -> 1. +. (2. *. p))
@@ -658,7 +664,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
q)
(fun p0 ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun q0 -> (fun p -> 1. +. (2. *. p))
(coq_lor p0 q0))
(fun q0 -> (fun p -> 2. *. p)
@@ -668,7 +674,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
q)
(fun _ ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p0 ->
q)
(fun q0 -> (fun p -> 1. +. (2. *. p))
@@ -682,10 +688,10 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
let rec coq_land p q =
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p0 ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun q0 ->
coq_Nsucc_double (coq_land p0 q0))
(fun q0 ->
@@ -695,7 +701,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
q)
(fun p0 ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun q0 ->
coq_Ndouble (coq_land p0 q0))
(fun q0 ->
@@ -705,7 +711,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
q)
(fun _ ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p0 ->
1.)
(fun q0 ->
@@ -719,10 +725,10 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
let rec ldiff p q =
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p0 ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun q0 ->
coq_Ndouble (ldiff p0 q0))
(fun q0 ->
@@ -732,7 +738,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
q)
(fun p0 ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun q0 ->
coq_Ndouble (ldiff p0 q0))
(fun q0 ->
@@ -742,7 +748,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
q)
(fun _ ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p0 ->
0.)
(fun q0 ->
@@ -756,10 +762,10 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
let rec coq_lxor p q =
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p0 ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun q0 ->
coq_Ndouble (coq_lxor p0 q0))
(fun q0 ->
@@ -769,7 +775,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
q)
(fun p0 ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun q0 ->
coq_Nsucc_double (coq_lxor p0 q0))
(fun q0 ->
@@ -779,7 +785,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
q)
(fun _ ->
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun q0 -> ((fun p -> 2. *. p)
q0))
(fun q0 -> ((fun p -> 1. +. (2. *. p))
@@ -802,7 +808,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val shiftl : float -> float -> float **)
let shiftl p n =
- (fun f0 fp n -> if n=0. then f0 () else fp n)
+ (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
(fun _ ->
p)
(fun n0 ->
@@ -812,7 +818,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val shiftr : float -> float -> float **)
let shiftr p n =
- (fun f0 fp n -> if n=0. then f0 () else fp n)
+ (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
(fun _ ->
p)
(fun n0 ->
@@ -823,23 +829,23 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
let rec testbit_nat p =
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p0 n ->
- (fun fO fS n -> if n=0 then fO () else fS (n-1))
+ (fun fO fS n -> if int_eq n 0 then fO () else fS (n-1))
(fun _ ->
true)
(fun n' ->
testbit_nat p0 n')
n)
(fun p0 n ->
- (fun fO fS n -> if n=0 then fO () else fS (n-1))
+ (fun fO fS n -> if int_eq n 0 then fO () else fS (n-1))
(fun _ ->
false)
(fun n' ->
testbit_nat p0 n')
n)
(fun _ n ->
- (fun fO fS n -> if n=0 then fO () else fS (n-1))
+ (fun fO fS n -> if int_eq n 0 then fO () else fS (n-1))
(fun _ ->
true)
(fun n0 ->
@@ -851,23 +857,23 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
let rec testbit p n =
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p0 ->
- (fun f0 fp n -> if n=0. then f0 () else fp n)
+ (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
(fun _ ->
true)
(fun n0 ->
testbit p0 (pred_N n0))
n)
(fun p0 ->
- (fun f0 fp n -> if n=0. then f0 () else fp n)
+ (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
(fun _ ->
false)
(fun n0 ->
testbit p0 (pred_N n0))
n)
(fun _ ->
- (fun f0 fp n -> if n=0. then f0 () else fp n)
+ (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
(fun _ ->
true)
(fun p0 ->
@@ -880,7 +886,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
let iter_op op =
let rec iter0 p a =
(fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
+if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
(fun p0 ->
op a (iter0 p0 (op a a)))
(fun p0 ->
@@ -898,11 +904,11 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val of_nat : int -> float **)
let rec of_nat n =
- (fun fO fS n -> if n=0 then fO () else fS (n-1))
+ (fun fO fS n -> if int_eq n 0 then fO () else fS (n-1))
(fun _ ->
1.)
(fun x ->
- (fun fO fS n -> if n=0 then fO () else fS (n-1))
+ (fun fO fS n -> if int_eq n 0 then fO () else fS (n-1))
(fun _ ->
1.)
(fun n0 ->
@@ -913,7 +919,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
(** val of_succ_nat : int -> float **)
let rec of_succ_nat n =
- (fun fO fS n -> if n=0 then fO () else fS (n-1))
+ (fun fO fS n -> if int_eq n 0 then fO () else fS (n-1))
(fun _ ->
1.)
(fun x ->
diff --git a/generator/tests/jsref/JsInterpreter.ml b/generator/tests/jsref/JsInterpreter.ml
index b126188..45000c0 100644
--- a/generator/tests/jsref/JsInterpreter.ml
+++ b/generator/tests/jsref/JsInterpreter.ml
@@ -307,7 +307,7 @@ let runs_type_object_define_own_prop_array_loop x = x.runs_type_object_define_ow
let object_has_prop runs0 s c l x =
if_some (run_object_method object_has_prop_ s l) (fun b ->
- let Coq_builtin_has_prop_default = b in
+ match b with Coq_builtin_has_prop_default ->
if_spec (runs0.runs_type_object_get_prop s c l x) (fun s1 d ->
res_ter s1
(res_val (Coq_value_prim (Coq_prim_bool
@@ -371,7 +371,7 @@ let run_object_get runs0 s c l x =
let run_object_get_prop runs0 s c l x =
if_some (run_object_method object_get_prop_ s l) (fun b ->
- let Coq_builtin_get_prop_default = b in
+ match b with Coq_builtin_get_prop_default ->
if_spec (runs0.runs_type_object_get_own_prop s c l x) (fun s1 d ->
if full_descriptor_comparable d Coq_full_descriptor_undef
then if_some (run_object_method object_proto_ s1 l) (fun proto ->
@@ -462,7 +462,7 @@ let object_proto_is_prototype_of runs0 s l0 l =
let object_default_value runs0 s c l prefo =
if_some (run_object_method object_default_value_ s l) (fun b ->
- let Coq_builtin_default_value_default = b in
+ match b with Coq_builtin_default_value_default ->
let gpref = unsome_default Coq_preftype_number prefo in
let lpref = other_preftypes gpref in
let_binding (fun s' x k ->
@@ -550,7 +550,7 @@ let to_string runs0 s c _foo_ = match _foo_ with
let object_can_put runs0 s c l x =
if_some (run_object_method object_can_put_ s l) (fun b ->
- let Coq_builtin_can_put_default = b in
+ match b with Coq_builtin_can_put_default ->
if_spec (runs0.runs_type_object_get_own_prop s c l x) (fun s1 d ->
match d with
| Coq_full_descriptor_undef ->
@@ -1381,7 +1381,7 @@ let run_expr_get_value runs0 s c e =
-> prop_name -> value -> strictness_flag -> result_void **)
let object_put_complete runs0 b s c vthis l x v str =
- let Coq_builtin_put_default = b in
+ match b with Coq_builtin_put_default ->
if_bool (object_can_put runs0 s c l x) (fun s1 b0 ->
if b0
then if_spec (runs0.runs_type_object_get_own_prop s1 c l x) (fun s2 d ->
@@ -2751,7 +2751,7 @@ let make_arg_setter runs0 s c x x0 =
string list -> result_void **)
let rec arguments_object_map_loop runs0 s c l xs len args x str lmap xsmap =
- (fun fO fS n -> if n=0 then fO () else fS (n-1))
+ (fun fO fS n -> if int_eq n 0 then fO () else fS (n-1))
(fun _ ->
if list_eq_nil_decidable xsmap
then res_void s
@@ -4757,7 +4757,7 @@ let run_stat_while runs0 s c rv labs e1 t2 =
let rec run_stat_switch_end runs0 s c rv _foo_ = match _foo_ with
| [] -> result_out (Coq_out_ter (s, (res_normal rv)))
| y :: scs' ->
- let Coq_switchclause_intro (e, ts) = y in
+ match y with Coq_switchclause_intro (e, ts) ->
if_success_state rv (run_block runs0 s c (rev ts)) (fun s1 rv1 ->
run_stat_switch_end runs0 s1 c rv1 scs')
@@ -4768,7 +4768,7 @@ let rec run_stat_switch_end runs0 s c rv _foo_ = match _foo_ with
let rec run_stat_switch_no_default runs0 s c vi rv _foo_ = match _foo_ with
| [] -> result_out (Coq_out_ter (s, (res_normal rv)))
| y :: scs' ->
- let Coq_switchclause_intro (e, ts) = y in
+ match y with Coq_switchclause_intro (e, ts) ->
if_spec (run_expr_get_value runs0 s c e) (fun s1 v1 ->
let_binding (strict_equality_test v1 vi) (fun b ->
if b
@@ -4791,7 +4791,7 @@ let run_stat_switch_with_default_default runs0 s c ts scs =
let rec run_stat_switch_with_default_B runs0 s c vi rv ts0 scs = match scs with
| [] -> run_stat_switch_with_default_default runs0 s c ts0 scs
| y :: scs' ->
- let Coq_switchclause_intro (e, ts) = y in
+ match y with Coq_switchclause_intro (e, ts) ->
if_spec (run_expr_get_value runs0 s c e) (fun s1 v1 ->
let_binding (strict_equality_test v1 vi) (fun b ->
if b
@@ -4810,7 +4810,7 @@ let rec run_stat_switch_with_default_A runs0 s c found vi rv scs1 ts0 scs2 =
then run_stat_switch_with_default_default runs0 s c ts0 scs2
else run_stat_switch_with_default_B runs0 s c vi rv ts0 scs2
| y :: scs' ->
- let Coq_switchclause_intro (e, ts) = y in
+ match y with Coq_switchclause_intro (e, ts) ->
let_binding (fun s0 ->
if_success_state rv (run_block runs0 s0 c (rev ts)) (fun s1 rv0 ->
run_stat_switch_with_default_A runs0 s1 c true vi rv0 scs' ts0 scs2))
@@ -6142,7 +6142,7 @@ let run_javascript runs0 p =
(** val runs : int -> runs_type **)
let rec runs max_step =
- (fun fO fS n -> if n=0 then fO () else fS (n-1))
+ (fun fO fS n -> if int_eq n 0 then fO () else fS (n-1))
(fun _ -> { runs_type_expr = (fun s x x0 -> Coq_result_bottom s);
runs_type_stat = (fun s x x0 -> Coq_result_bottom s); runs_type_prog =
(fun s x x0 -> Coq_result_bottom s); runs_type_call =
diff --git a/generator/tests/jsref/JsNumber.ml b/generator/tests/jsref/JsNumber.ml
index e552789..3c4fd4f 100644
--- a/generator/tests/jsref/JsNumber.ml
+++ b/generator/tests/jsref/JsNumber.ml
@@ -52,7 +52,7 @@ let ln2 = (log 2.)
let from_string = (fun s ->
(*try*)
(* let s = (String.concat "" (List.map (String.make 1) s)) in ARTHUR hack*)
- if s = "" then 0. else float_of_string s
+ if string_eq s "" then 0. else float_of_string s
(* FIXME: with Failure "float_of_string" -> nan *) )
(* Note that we're using `float_of_string' there, which does not have the same
behavior than JavaScript. For instance it will read "022" as 22 instead of
@@ -65,9 +65,9 @@ let to_string = (fun f ->
prerr_newline();
let string_of_number n =
let sfn = string_of_float n in
- (if (sfn = "inf") then "Infinity" else
- if (sfn = "-inf") then "-Infinity" else
- if (sfn = "nan") then "NaN" else
+ (if (string_eq sfn "inf") then "Infinity" else
+ if (string_eq sfn "-inf") then "-Infinity" else
+ if (string_eq sfn "nan") then "NaN" else
let inum = int_of_float n in
if (float_of_int inum = n) then (string_of_int inum) else (string_of_float n)) in
string_of_number f
@@ -95,7 +95,7 @@ let absolute = abs_float
(** val sign : number -> number **)
-let sign = (fun f -> float_of_int (compare f 0.))
+let sign = (fun f -> float_of_int (float_compare f 0.))
(** val lt_bool : number -> number -> bool **)
@@ -123,7 +123,7 @@ let div = (/.)
(** val number_comparable : number coq_Comparable **)
-let number_comparable = (fun n1 n2 -> 0 = compare n1 n2)
+let number_comparable = (fun n1 n2 -> int_eq 0 (float_compare n1 n2))
(** val of_int : float -> number **)
diff --git a/generator/tests/jsref/JsPreliminary.ml b/generator/tests/jsref/JsPreliminary.ml
index 7a284e8..2b060b8 100644
--- a/generator/tests/jsref/JsPreliminary.ml
+++ b/generator/tests/jsref/JsPreliminary.ml
@@ -163,7 +163,7 @@ let rec inequality_test_string s1 s2 =
then inequality_test_string s1' s2'
else lt_int_decidable (int_of_char c1) (int_of_char c2))
*)
-let inequality_test_string s1 s2 = (s1 <> s2)
+let inequality_test_string s1 s2 = (not (string_eq s1 s2))
(** val inequality_test_primitive : prim -> prim -> prim **)
diff --git a/generator/tests/jsref/LibList.ml b/generator/tests/jsref/LibList.ml
index e34e1e5..aafdc80 100644
--- a/generator/tests/jsref/LibList.ml
+++ b/generator/tests/jsref/LibList.ml
@@ -63,7 +63,7 @@ let rec take_drop_last l = match l with
let rec nth_def d n l = match l with
| [] -> d
- | x :: l' -> if n=0 then x else nth_def d (n-1) l'
+ | x :: l' -> if int_eq n 0 then x else nth_def d (n-1) l'
(** val mem_decide : 'a1 coq_Comparable -> 'a1 -> 'a1 list -> bool **)
diff --git a/generator/tests/jsref/LibNat.ml b/generator/tests/jsref/LibNat.ml
index f1fe6af..96922ec 100644
--- a/generator/tests/jsref/LibNat.ml
+++ b/generator/tests/jsref/LibNat.ml
@@ -3,16 +3,16 @@ open LibReflect
(** val nat_compare : int -> int -> bool **)
let rec nat_compare x y =
- (fun fO fS n -> if n=0 then fO () else fS (n-1))
+ (fun fO fS n -> if int_eq n 0 then fO () else fS (n-1))
(fun _ ->
- (fun fO fS n -> if n=0 then fO () else fS (n-1))
+ (fun fO fS n -> if int_eq n 0 then fO () else fS (n-1))
(fun _ ->
true)
(fun n ->
false)
y)
(fun x' ->
- (fun fO fS n -> if n=0 then fO () else fS (n-1))
+ (fun fO fS n -> if int_eq n 0 then fO () else fS (n-1))
(fun _ ->
false)
(fun y' ->
diff --git a/generator/tests/jsref/LibReflect.ml b/generator/tests/jsref/LibReflect.ml
index 61b683d..6a03ff9 100644
--- a/generator/tests/jsref/LibReflect.ml
+++ b/generator/tests/jsref/LibReflect.ml
@@ -52,5 +52,5 @@ let bool_comparable x y =
(** val prop_eq_decidable :
coq_Decidable -> coq_Decidable -> coq_Decidable **)
-let prop_eq_decidable = (=)
+let prop_eq_decidable = bool_eq
diff --git a/generator/tests/jsref/Peano.ml b/generator/tests/jsref/Peano.ml
index 99c30cf..d3bd560 100644
--- a/generator/tests/jsref/Peano.ml
+++ b/generator/tests/jsref/Peano.ml
@@ -5,5 +5,5 @@ let rec plus = (+)
(** val nat_iter : int -> ('a1 -> 'a1) -> 'a1 -> 'a1 **)
let rec nat_iter n f x =
- if n=0 then x else f (nat_iter (n-1) f x)
+ if int_eq n 0 then x else f (nat_iter (n-1) f x)
diff --git a/generator/tests/jsref/Shared.ml b/generator/tests/jsref/Shared.ml
index 002d695..1327790 100644
--- a/generator/tests/jsref/Shared.ml
+++ b/generator/tests/jsref/Shared.ml
@@ -33,7 +33,7 @@ let le_int_decidable = (<=)
(** val ge_nat_decidable : int -> int -> coq_Decidable **)
-let ge_nat_decidable = (>=)
+let ge_nat_decidable = int_ge
type 'a coq_Pickable_option =
'a option
diff --git a/generator/tests/jsref/String0.ml b/generator/tests/jsref/String0.ml
index fdd7e9f..b638ef0 100644
--- a/generator/tests/jsref/String0.ml
+++ b/generator/tests/jsref/String0.ml
@@ -1,7 +1,7 @@
(* ARTHUR: hacked this file *)
-let string_dec s1 s2 = (s1 = s2)
+let string_dec s1 s2 = (string_eq s1 s2)
let append s1 s2 = String.append s1 s2
--
GitLab