(fix) Wrong JS code generation for infinity/nan

Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
accordproject · Apr 30, 2019 · 0b90adf · 0b90adf
1 parent 5f61880
commit 0b90adf
Show file tree

Hide file tree

Showing 6 changed files with 6,909 additions and 6,901 deletions.
diff --git a/examples/smoke/logic.ergo b/examples/smoke/logic.ergo
@@ -22,6 +22,8 @@ contract Smoke over TemplateModel {
     enforce(some(A{ a : 1 })?.a ?? 2 = 1);
     enforce(C{ contract : "foo" }.contract = "foo");
     enforce(C{ contract : "foo" }.contract = "foo");
+		enforce(infinity = 1.0/0.0);
+		enforce(-infinity = -1.0/0.0);
 		enforce("\"\\
 	" = "\034\092\010\013\009");
 		enforce("\"\\

diff --git a/mechanization/Utils/EJSON.v b/mechanization/Utils/EJSON.v
@@ -135,7 +135,11 @@ Section EJSON.
     Fixpoint ejsonToJS (quotel:string) (j : ejson) : estring
       := match j with
          | ejnull => `"null" (* to be discussed *)
-         | ejnumber n => `to_string n
+         | ejnumber n =>
+           if (float_eq n float_infinity) then `"Infinity"
+           else if (float_eq n float_neg_infinity) then `"-Infinity"
+           else if (float_eq n float_nan) then `"NaN"
+           else `to_string n
          | ejbool b => if b then `"true" else `"false"
          | ejstring s => stringToJS quotel s
          | ejarray ls =>