diff --git a/generator/js_of_ast.ml b/generator/js_of_ast.ml
index c013cdf4f228f0a3d42a62fa8141e4ce2b601e74..7b878e776869d0b5cb747ddf26dabc03c4239464 100644
--- a/generator/js_of_ast.ml
+++ b/generator/js_of_ast.ml
@@ -781,13 +781,27 @@ and js_of_constant = function
and js_of_path_longident path ident =
match String.concat "." @@ Longident.flatten ident.txt with
+ (* for unit: *)
| "()" -> unit_repr
+ (* for bool: *)
+ | "&&" -> "&&"
+ | "||" -> "||"
+ (* for float: *)
| "+." -> "+"
| "*." -> "*"
| "-." -> "-"
| "~-." -> "-"
| "/." -> "/"
- | "=" -> "=="
+ | "<" -> "<"
+ | ">" -> ">"
+ | "<=" -> "<="
+ | ">=" -> ">="
+ (* for int: *)
+ | "+" -> "+"
+ | "*" -> "*"
+ | "-" -> "-"
+ | "/" -> "/"
+ (* for string *)
| "^" -> "+" (* !!TODO: we want to claim ability to type our sublanguage, so we should not use this *)
| res ->
let res = if !generate_qualified_names && (Path.head path).name <> "Stdlib"
diff --git a/generator/stdlib_ml/stdlib.js b/generator/stdlib_ml/stdlib.js
index 35181ed141b514fe7b356438aa34eb900d321563..5e3f1e1718a43c5fcb72ebc497bf6fd1c338c309 100644
--- a/generator/stdlib_ml/stdlib.js
+++ b/generator/stdlib_ml/stdlib.js
@@ -1,3 +1,6 @@
+
+//----------------------------------------------------------------------------
+
var None = function() {
return { type: "option", tag: "None" };
};
@@ -6,11 +9,7 @@ var Some = function(value) {
return { type: "option", tag: "Some", value: value };
};
-
-
-var max_float = Number.MAX_VALUE; // TODO: find absolute value for this
-var min_float = Number.MIN_VALUE; // TODO: find absolute value for this
-
+//----------------------------------------------------------------------------
var mk_nil = function() {
return { type: "list", tag: "[]" };
@@ -20,83 +19,84 @@ var mk_cons = function(head, tail) {
return { type: "list", tag: "::", head: head, tail: tail };
};
-var add = function (a, b) { return a + b }
-var sub = function (a, b) { return a - b }
-var mul = function (a, b) { return a * b }
-var div = function (a, b) { return a / b }
-
-var eq = function (a, b) { return a === b }
-var le = function (a, b) { return a < b }
-var ge = function (a, b) { return a > b }
-
-var leq = function (a, b) { return a <= b }
-var geq = function (a, b) { return a >= b }
-
-var print = function (x) { console.log(x) }
-
-var stuck = function (msg) { throw {type:'stuck', msg:msg} }
-
-var to_string = function (x) { return String(x) }
-
-var parse = function (source) {
- var ast = require('esprima').parse(source).body[0].expression;
-
- // Esprima does it's little thing. To be handled by auto generated code we need to
- // reshape the tree structure to match the labels and expected content.
-
- function transform (tree) {
- if (tree === undefined) {
- } else {
- // Javascript style instructions are well handled with no additional creation.
- switch (tree.operator) {
- case '+':
- tree.type = "Add"; tree.operator = undefined; break;
- case '-':
- tree.type = "Sub"; tree.operator = undefined; break;
- case "*":
- tree.type = "Mul"; tree.operator = undefined; break;
- case "/":
- tree.type = "Div"; tree.operator = undefined; break;
- default: break;
- }
-
- if (tree.type === "Literal") {
- tree.type = "Const";
- }
-
- // tree.left and tree.right from parser interpretation
- if (tree.left !== undefined) tree.left = transform(tree.left);
- if (tree.right !== undefined) tree.right = transform(tree.right);
-
- // Esprima sees these standalone type instructions as Identifiers
- if (tree.type === "Identifier") {
- switch (tree.name) {
- case "Emp":
- tree.type = "Emp"; break;
- default: console.log("Unknown ident"); break;
- }
- }
-
- // Esprima generates a function type structure that needs reshaping to the
- // automatically generated structure, respecting label names!
- if (tree.type === "CallExpression") {
- switch (tree.callee.name) {
- case "Push":
- tree.type = "Push";
- tree.value = transform(tree.arguments[0]);
- tree.stack = transform(tree.arguments[1]);
- break;
- case "Pop":
- tree.type = "Pop";
- tree.stack = transform(tree.arguments[0]);
- break;
- default: console.log("Unknown callexpr"); break;
- }
- }
-
- return tree;
- }
- }
-
- return transform(ast);
-}
+//----------------------------------------------------------------------------
+
+// var print = function (x) { console.log(x) }
+
+// var stuck = function (msg) { throw {type:'stuck', msg:msg} }
+
+// var to_string = function (x) { return String(x) }
+
+//----------------------------------------------------------------------------
+
+/* automatically dealt with js_of_ast.ml
+
+val ( + ) : int -> int -> int
+val ( - ) : int -> int -> int
+val ( * ) : int -> int -> int
+val ( / ) : int -> int -> int
+val ( +. ) : float -> float -> float
+val ( -. ) : float -> float -> float
+val ( *. ) : float -> float -> float
+val ( /. ) : float -> float -> float
+val ( = ) : float -> float -> bool
+val ( < ) : float -> float -> bool
+val ( > ) : float -> float -> bool
+val ( <= ) : float -> float -> bool
+val ( >= ) : float -> float -> bool
+*/
+
+//----------------------------------------------------------------------------
+
+var nat_eq = function(x, y) { return x === y; };
+var int_eq = function(x, y) { return x === y; };
+var int_ge = function(x, y) { return x >= y; };
+
+//----------------------------------------------------------------------------
+
+var int_of_float = function(x) { return x; };
+var number_of_int = function(x) { return x; };
+var of_int = function(x) { return x; };
+
+//----------------------------------------------------------------------------
+
+var number_comparable = function(x, y) { return x === y; };
+
+//----------------------------------------------------------------------------
+
+var bool_eq = function(x, y) { return x === y; };
+
+var not = function(x) { return !x; };
+
+
+//----------------------------------------------------------------------------
+
+var string_eq = function(x, y) { return x === y; };
+
+var strappend = function(x, y) { return x + y; };
+
+var strlength = function(x) { return x.length; };
+
+var substring = function(n, m, s) { return s.slice(n, n+m); };
+
+
+//----------------------------------------------------------------------------
+
+/*
+(* We use this to compare types that are not known by stdlib, like Native_error;
+ should be implemented in JS by comparing the objects, to see if they have the same
+ "tag" fields (there should be no other fields, except perhaps "type") *)
+val ( === ) : 'a -> 'a -> bool (* becomes === in js *)
+
+*/
+
+//----------------------------------------------------------------------------
+
+
+var __LOC__ = "___LOC___"
+
+var raise = function(x) { throw "Not_found"; };
+
+
+
+
diff --git a/generator/stdlib_ml/stdlib.mli b/generator/stdlib_ml/stdlib.mli
index d84a70541d1b5ee5e351a9f7e518d6904c9c696e..15a8e718b651e0ef821e6233319747ef4e35a1d2 100644
--- a/generator/stdlib_ml/stdlib.mli
+++ b/generator/stdlib_ml/stdlib.mli
@@ -3,9 +3,11 @@
(* int operations *)
(* todo : factorize and clean up *)
-
+(*
val ( ~+ ) : int -> int
val ( ~- ) : int -> int
+*)
+
val ( + ) : int -> int -> int
val ( - ) : int -> int -> int
val ( * ) : int -> int -> int
@@ -23,31 +25,35 @@ val int_ge : int -> int -> bool
(* Alan: these can be implemented directly, using Number.NaN,
Number.POSITIVE_INFINITY, Number.NEGATIVE_INFINITY *)
-
+(*
val nan : float
val infinity : float
val neg_infinity : float
+*)
(* Alan: Do we need these ? If so, they are Number.MAX_VALUE and
- Number.MIN_VALUE *)
+ Number.MIN_VALUE
val max_float : float
val min_float : float
+ *)
+
+
(* Alan: these should all be implemented along with the int operations as the JS
ones. ** is Math.pow *)
+(*
val ( ~+. ) : float -> float
val ( ~-. ) : float -> float
+*)
+
val ( +. ) : float -> float -> float
val ( -. ) : float -> float -> float
val ( *. ) : float -> float -> float
val ( /. ) : float -> float -> float
-val ( ** ) : float -> float -> float
-
-(* Alan: Math.abs, if we need it *)
+(* val ( ** ) : float -> float -> float *)
-val abs_float : float -> float
(*
val mod_float : float -> float -> float (* Alan: % infix *)
@@ -67,7 +73,7 @@ val max : float -> float -> float
(* Alan: Ideally we would add these to the spec, but for the moment conversion
to a string is doing a foo+"", and conversion to an int is doing +foo *)
-val int_of_float : float -> int
+val int_of_float : float -> int (* will be removed, since only used by substring *)
val number_of_int : int -> float (* = fun x -> float_of_int x *)
(** val of_int : float -> number **)
diff --git a/generator/tests/jsref/JsCommonAux.ml b/generator/tests/jsref/JsCommonAux.ml
index 7214ae8fc99ec9d1b0e6aaf28f333f0e1dcc0919..6078bf76f20a4d35eb141c6aeb8c6af8d5fc81bc 100644
--- a/generator/tests/jsref/JsCommonAux.ml
+++ b/generator/tests/jsref/JsCommonAux.ml
@@ -45,7 +45,7 @@ let same_value_dec v1 v2 =
(value_comparable v1 (Coq_value_prim (Coq_prim_number
JsNumber.nan)))
(value_comparable v2 (Coq_value_prim (Coq_prim_number
- nan)))
+ JsNumber.nan)))
in
(if h2
then (fun _ -> true_decidable)
diff --git a/generator/tests/jsref/JsInterpreter.ml b/generator/tests/jsref/JsInterpreter.ml
index 8f3587e1d1176e94b7a421d467eced1757330df4..75d2bbba3f95571aa7497930b9efa4c70fe61b8c 100644
--- a/generator/tests/jsref/JsInterpreter.ml
+++ b/generator/tests/jsref/JsInterpreter.ml
@@ -2814,7 +2814,7 @@ let run_object_get_own_prop runs0 s c l x =
(fun s1 k ->
if_string
(runs0.runs_type_to_string s1 c (Coq_value_prim
- (Coq_prim_number (abs_float k))))
+ (Coq_prim_number (JsNumber.absolute k))))
(fun s2 s3 ->
if not_decidable (string_comparable x s3)
then res_spec s2 Coq_full_descriptor_undef
@@ -2996,7 +2996,7 @@ let is_lazy_op _foo_ = match _foo_ with
let get_puremath_op _foo_ = match _foo_ with
| Coq_binary_op_mult -> Some (fun x y -> x *. y)
| Coq_binary_op_div -> Some (fun x y -> x /. y)
-| Coq_binary_op_mod -> Some fmod
+| Coq_binary_op_mod -> Some JsNumber.fmod
| Coq_binary_op_add -> None
| Coq_binary_op_sub -> Some (fun x y -> x -. y)
| Coq_binary_op_left_shift -> None
diff --git a/generator/tests/jsref/JsNumber.mli b/generator/tests/jsref/JsNumber.mli
index 819e2833bdca8d8747209e5ea4b587e3f89bd9fa..c21ccfd2a412f8e81e7ccc16d19908df8804ec5d 100644
--- a/generator/tests/jsref/JsNumber.mli
+++ b/generator/tests/jsref/JsNumber.mli
@@ -36,3 +36,5 @@ val sign : number -> number
val absolute : number -> number
val modulo_32 : number -> number
+
+val fmod : number -> number -> number
diff --git a/generator/tests/jsref/JsPreliminary.ml b/generator/tests/jsref/JsPreliminary.ml
index e9e2905ab2436a20b6e0f5722490de910d7154ae..085a7c79ddcfed19ae69722919a09b1c6c584c5d 100644
--- a/generator/tests/jsref/JsPreliminary.ml
+++ b/generator/tests/jsref/JsPreliminary.ml
@@ -126,7 +126,7 @@ let strict_equality_test v1 v2 =
(** val inequality_test_number : number -> number -> prim **)
let inequality_test_number n1 n2 =
- if or_decidable (number_comparable n1 JsNumber.nan) (number_comparable n2 nan)
+ if or_decidable (number_comparable n1 JsNumber.nan) (number_comparable n2 JsNumber.nan)
then Coq_prim_undef
else if number_comparable n1 n2
then Coq_prim_bool false