(fix) issues with JS runtime for singleton/double

Signed-off-by: Jerome Simeon <[email protected]>

backends/javascript/ergo-runtime.js

@@ -361,9 +361,9 @@ function enhanced_cast(brands,v) {
 }
 function singleton(v) {
     if (v.length == 1) {
-        return left(v[0]);
+        return v[0];
     } else {
-        return right(null); /* Not a singleton */
+        return null; /* Not a singleton */
     }
 }
 function unbrand(v) {
@@ -526,7 +526,19 @@ function substringNoLength(v, start) {
 }
 
 // Math operations
-function float_of_string(s) { return parseFloat(s); }
+function floatOfString(s) {
+    // Check whether we're dealing with nan, since it's the error case for Number.parseFloat
+    if (s === 'nan') {
+        return nan;
+    } else {
+        let num = Number.parseFloat(s);
+        if (Number.isNaN(num)) {
+            return null;
+        } else {
+            return num
+        }
+    }
+}
 function acos(x) { return Math.acos(x); }
 function asin(x) { return Math.asin(x); }
 function atan(x) { return Math.atan(x); }

examples/volumediscount/logic8.ergo

@@ -18,9 +18,9 @@ contract VolumeDiscount over VolumeDiscountContract {
    // Clause for volume discount
    clause volumediscount(request : VolumeDiscountRequest) : VolumeDiscountResponse {
     if request.netAnnualChargeVolume < contract.firstVolume
- 	  then return VolumeDiscountResponse{ discountRate: double(toString(contract.firstRate)) }
+ 	  then return VolumeDiscountResponse{ discountRate: double("2000") }
     else if request.netAnnualChargeVolume < contract.secondVolume
-    then return VolumeDiscountResponse{ discountRate: contract.secondRate }
-    else return VolumeDiscountResponse{ discountRate: contract.thirdRate }
+ 	  then return VolumeDiscountResponse{ discountRate: double("2000") }
+		else return VolumeDiscountResponse{ discountRate: double("2000") }
   }
 }

mechanization/Backend/Model/MathModelPart.v

@@ -83,7 +83,7 @@ Inductive math_unary_op
 
 Definition math_unary_op_tostring (f:math_unary_op) : String.string
   := match f with
-     | uop_math_of_string => "float_of_string"
+     | uop_math_of_string => "floatOfString"
      | uop_math_acos => "acos"
      | uop_math_asin => "asin"
      | uop_math_atan => "atan"
@@ -101,7 +101,7 @@ Definition math_to_java_unary_op
              (quotel:String.string) (fu:math_unary_op)
              (d:java_json) : java_json
   := match fu with
-     | uop_math_of_string => mk_java_unary_op0 "float_of_string" d
+     | uop_math_of_string => mk_java_unary_op0 "floatOfString" d
      | uop_math_acos => mk_java_unary_op0 "acos" d
      | uop_math_asin => mk_java_unary_op0 "asin" d
      | uop_math_atan => mk_java_unary_op0 "atan" d
@@ -118,7 +118,7 @@ Definition math_to_javascript_unary_op
              (quotel:String.string) (fu:math_unary_op)
              (d:String.string) : String.string
   := match fu with
-     | uop_math_of_string => "float_of_string(" ++ d ++ ")"
+     | uop_math_of_string => "floatOfString(" ++ d ++ ")"
      | uop_math_acos => "acos(" ++ d ++ ")"
      | uop_math_asin => "asin(" ++ d ++ ")"
      | uop_math_atan => "atan(" ++ d ++ ")"
@@ -134,7 +134,7 @@ Definition math_to_ajavascript_unary_op
              (fu:math_unary_op)
              (e:JsSyntax.expr) : JsSyntax.expr
   := match fu with
-     | uop_math_of_string => call_runtime "float_of_string" [ e ]
+     | uop_math_of_string => call_runtime "floatOfString" [ e ]
      | uop_math_acos => call_runtime "acos" [ e ]
      | uop_math_asin => call_runtime "asin" [ e ]
      | uop_math_atan => call_runtime "atan" [ e ]