From 64f53ce675b370628fad10de9b6b5854ef5632d8 Mon Sep 17 00:00:00 2001
From: Thomas Wood <thomas.wood09@imperial.ac.uk>
Date: Thu, 27 Oct 2016 18:03:33 +0200
Subject: [PATCH] jsref' now compiles against both js_to_ast and OCaml
---
Makefile | 13 +-
jsref/.gitignore | 3 +
jsref/.merlin | 1 +
jsref/Compare.ml | 0
jsref/Debug.ml | 36 ++++
jsref/JsCommon.ml | 2 +-
jsref/JsNumber.ml | 91 +++++++++
jsref/JsNumber.mli | 1 +
jsref/Makefile | 130 +++++++++----
jsref/ModuleExport.ml | 0
jsref/ModuleExport.mli | 0
jsref/Prheap.js | 0
jsref/Prheap.ml | 390 +++++++++++++++++++++++++++++++++++++
jsref/Prheap.mli | 6 +
jsref/Translate_syntax.js | 2 +-
jsref/Translate_syntax.ml | 375 +++++++++++++++++++++++++++++++++++
jsref/Translate_syntax.mli | 8 +-
jsref/run_js.ml | 225 +++++++++++++++++++++
jsref/run_js.mli | 0
opam | 16 +-
20 files changed, 1245 insertions(+), 54 deletions(-)
create mode 100644 jsref/.merlin
create mode 100644 jsref/Compare.ml
create mode 100644 jsref/Debug.ml
create mode 100644 jsref/JsNumber.ml
create mode 100644 jsref/ModuleExport.ml
create mode 100644 jsref/ModuleExport.mli
create mode 100644 jsref/Prheap.js
create mode 100644 jsref/Prheap.ml
create mode 100644 jsref/Prheap.mli
create mode 100644 jsref/Translate_syntax.ml
create mode 100644 jsref/run_js.ml
create mode 100644 jsref/run_js.mli
diff --git a/Makefile b/Makefile
index bbf5ad5..8b2c1f0 100644
--- a/Makefile
+++ b/Makefile
@@ -3,12 +3,13 @@ PUB_FILES=driver.html libraries jquery-ui-1.11.4.custom jquery_scroll \
esprima-to-ast.js jsref/lineof.js navig-driver.js \
jsref/assembly.js
-all: jsjsref
+all: generator jsjsref mljsref
init:
opam switch 4.03.0
eval `opam config env`
opam pin -yn add jsjsref .
+ opam pin -yn add JS_Parser "https://github.com/resource-reasoning/JS_Parser.git#v0.1.0"
opam install -y jsjsref --deps-only
publish: generator $(PUB_FILES)
@@ -17,8 +18,14 @@ publish: generator $(PUB_FILES)
generator:
$(MAKE) -C generator
+generator-stdlib:
+ $(MAKE) -C generator stdlib
+
jsjsref: generator
- $(MAKE) -C jsref
+ $(MAKE) -C jsref jsjsref
+
+mljsref: generator-stdlib
+ $(MAKE) -C jsref mljsref
test_init:
git submodule update --init test/test262
@@ -31,4 +38,4 @@ clean:
$(MAKE) -C generator clean
$(MAKE) -C jsref clean
-.PHONY: publish jsjsref generator test_init test clean
+.PHONY: publish jsjsref mljsref generator generator-stdlib test_init test clean
diff --git a/jsref/.gitignore b/jsref/.gitignore
index 813a567..8d73be8 100644
--- a/jsref/.gitignore
+++ b/jsref/.gitignore
@@ -10,3 +10,6 @@ assembly.js
lineof.js
.depends
displayed_sources.js
+*.cmo
+*.byte
+*.native
diff --git a/jsref/.merlin b/jsref/.merlin
new file mode 100644
index 0000000..5b5675f
--- /dev/null
+++ b/jsref/.merlin
@@ -0,0 +1 @@
+PKG JS_Parser
diff --git a/jsref/Compare.ml b/jsref/Compare.ml
new file mode 100644
index 0000000..e69de29
diff --git a/jsref/Debug.ml b/jsref/Debug.ml
new file mode 100644
index 0000000..7b7b953
--- /dev/null
+++ b/jsref/Debug.ml
@@ -0,0 +1,36 @@
+
+(* Various debug helper functions *)
+
+(* Inserted by extraction *)
+
+let not_yet_implemented_because loc s =
+ print_endline (loc ^ ": Not implemented because: " ^ Prheap.string_of_char_list s)
+
+let impossible_because loc s =
+ print_endline (loc ^ ": Stuck because: " ^ Prheap.string_of_char_list s)
+
+let impossible_with_heap_because loc s message =
+ print_endline (loc ^ ": Stuck!\nState: " ^ Prheap.prstate true s ^ "\nMessage:\t" ^ Prheap.string_of_char_list message)
+
+(* Inserted into JsInterpreter by patching in Makefile functions named after the appropriate insertion *)
+
+let ref_get_value r =
+ prerr_string "Warning: ref_get_value returns the undefined value on ";
+ prerr_string (Prheap.prref r);
+ prerr_newline()
+
+
+let ref_get_value_2 r =
+ prerr_string ("Warning: ref_get_value returns the undefined value on ");
+ prerr_string (Prheap.prresvalue r);
+ prerr_newline()
+
+let run_object_method l =
+ prerr_endline (Printf.sprintf "Warning: in run_object_method the location %s is unfetchable." (Prheap.prloc l))
+
+let run_object_heap_set_extensible l =
+ prerr_endline (Printf.sprintf "Warning: in run_object_heap_set_extensible the location %s is unfetchable." (Prheap.prloc l))
+
+let lexical_env_get_identifier_ref x0 =
+ prerr_endline ("Warning: lexical_env_get_identifier_ref fails to find " ^ (Prheap.string_of_char_list x0))
+
diff --git a/jsref/JsCommon.ml b/jsref/JsCommon.ml
index 77de460..22073ff 100644
--- a/jsref/JsCommon.ml
+++ b/jsref/JsCommon.ml
@@ -585,7 +585,7 @@ let elision_tail_remove ol =
(** val parse_pickable : string -> bool -> prog coq_Pickable_option **)
let parse_pickable = (fun s strict ->
- Translate_syntax.parse_esprima strict s
+ Translate_syntax.parse_js_syntax strict s
(*Translate_syntax.parse_esprima strict s*)
(* with
(* | Translate_syntax.CoqSyntaxDoesNotSupport _ -> assert false (* Temporary *) *)
diff --git a/jsref/JsNumber.ml b/jsref/JsNumber.ml
new file mode 100644
index 0000000..1efd933
--- /dev/null
+++ b/jsref/JsNumber.ml
@@ -0,0 +1,91 @@
+type number = float
+
+let floor = floor;;
+
+let zero = 0.;;
+let neg_zero = -0.;;
+let one = 1.;;
+let infinity = infinity;;
+let neg_infinity = neg_infinity;;
+let max_value = max_float;;
+let min_value = (Int64.float_of_bits Int64.one);;
+let nan = nan;;
+let pi = 4. *. atan 1.;;
+let e = exp 1.;;
+let ln2 = log 2.
+
+(* 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
+ 18, which should be the JavaScript result for it. *)
+let from_string s =
+ try
+ if s = "" then 0. else float_of_string s
+ with
+ Failure "float_of_string" -> nan
+
+(* Note that this is ugly, we should use the spec of JsNumber.to_string here (9.8.1). *)
+let to_string f =
+ let sfn = string_of_float f in
+ (if (sfn = "inf") then "Infinity" else
+ if (sfn = "-inf") then "-Infinity" else
+ if (sfn = "nan") then "NaN" else
+ let inum = int_of_float f in
+ if (float_of_int inum = f)
+ then (string_of_int inum)
+ else (string_of_float f))
+
+let to_int32 = fun n ->
+ match classify_float n with
+ | FP_normal | FP_subnormal ->
+ let i32 = 2. ** 32. in
+ let i31 = 2. ** 31. in
+ let posint = (if n < 0. then (-1.) else 1.) *. (floor (abs_float n)) in
+ let int32bit =
+ let smod = mod_float posint i32 in
+ if smod < 0. then smod +. i32 else smod
+ in
+ (if int32bit >= i31 then int32bit -. i32 else int32bit)
+ | _ -> 0.
+
+let to_uint32 = fun n ->
+ match classify_float n with
+ | FP_normal | FP_subnormal ->
+ let i32 = 2. ** 32. in
+ let posint = (if n < 0. then (-1.) else 1.) *. (floor (abs_float n)) in
+ let int32bit =
+ let smod = mod_float posint i32 in
+ if smod < 0. then smod +. i32 else smod
+ in
+ int32bit
+ | _ -> 0.
+
+let int32_left_shift x y =
+ Int32.to_float (Int32.shift_left (Int32.of_float x) (int_of_float y))
+let int32_right_shift x y =
+ Int32.to_float (Int32.shift_right (Int32.of_float x) (int_of_float y))
+
+let int32_bitwise_and x y =
+ Int32.to_float (Int32.logand (Int32.of_float x) (Int32.of_float y))
+let int32_bitwise_or x y =
+ Int32.to_float (Int32.logor (Int32.of_float x) (Int32.of_float y))
+let int32_bitwise_xor x y =
+ Int32.to_float (Int32.logxor (Int32.of_float x) (Int32.of_float y))
+let int32_bitwise_not x =
+ Int32.to_float (Int32.lognot (Int32.of_float x))
+
+let uint32_right_shift x y =
+ let i31 = 2. ** 31. in
+ let i32 = 2. ** 32. in
+ let newx = if x >= i31 then x -. i32 else x in
+ let r = Int32.to_float (Int32.shift_right_logical (Int32.of_float newx) (int_of_float y)) in
+ if r < 0. then r +. i32 else r
+
+let neg = (~-.)
+let sign f = float_of_int (compare f 0.)
+let absolute = abs_float
+
+let modulo_32 x =
+ let r = mod_float x 32. in
+ if x < 0. then r +. 32. else r
+
+let fmod = mod_float
diff --git a/jsref/JsNumber.mli b/jsref/JsNumber.mli
index c21ccfd..a4be8a2 100644
--- a/jsref/JsNumber.mli
+++ b/jsref/JsNumber.mli
@@ -1,3 +1,4 @@
+(* JS Number type *)
type number = float
val floor : float -> float
diff --git a/jsref/Makefile b/jsref/Makefile
index cbe992d..1f8f360 100644
--- a/jsref/Makefile
+++ b/jsref/Makefile
@@ -6,20 +6,37 @@
# make interp # build interp.js
#
###############################################################
-# Paths
-all: # Defined below
+all: jsjsref mljsref
-JSREF_ML := $(filter-out JsOutput.ml,$(wildcard *.ml))
+ML_FRONTEND_SRC := ml_frontend
+
+###############################################################
+##### Dependencies
+
+# Avoid dependency generation for non-jsjsref build targets
+ifeq ($(filter clean%,$(MAKECMDGOALS)),)
+include .depends
+endif
+
+.depends: $(JSREF_ML) $(PPX_BIN)
+ $(OCAMLDEP) -ppx $(PPX_BIN) -I . -all * $(ML_FRONTEND_SRC)/* > $@
+
+###############################################################
+###############################################################
+# JS-JSRef
+JSREF_ML := $(wildcard *.ml)
JSREF_MLI := $(wildcard *.mli)
GENERATOR_DIR := ../generator
-STDLIB_DIR := $(GENERATOR_DIR)/stdlib_ml
-###############################################################
+STDLIB_DIR := $(GENERATOR_DIR)/stdlib_ml
+STDLIB_FLAG := -I $(STDLIB_DIR) -open Stdlib
+REPLACE_STDLIB := -nopervasives -nostdlib $(STDLIB_FLAG)
-# ASSEMBLY_JS must respect dependencies order
+# ASSEMBLY_JS_FILES must respect dependencies order
ASSEMBLY_JS_FILES := \
+ $(STDLIB_DIR)/stdlib.js \
BinNums.unlog.js \
Bool0.unlog.js \
List0.unlog.js \
@@ -36,7 +53,6 @@ ASSEMBLY_JS_FILES := \
HeapList.unlog.js \
Shared.unlog.js \
Compare.js \
- Debug.js \
JsNumber.js \
JsSyntax.unlog.js \
JsSyntaxAux.unlog.js \
@@ -46,11 +62,14 @@ ASSEMBLY_JS_FILES := \
JsCommonAux.unlog.js \
JsPreliminary.unlog.js \
JsInit.unlog.js \
+ Prheap.js \
+ Debug.js \
JsInterpreterMonads.unlog.js \
JsInterpreter.log.js \
- ModuleExport.js
-ASSEMBLY_JS := $(STDLIB_DIR)/stdlib.js $(ASSEMBLY_JS_FILES)
+ASSEMBLY_JS := \
+ $(ASSEMBLY_JS_FILES) \
+ ModuleExport.js
###############################################################
@@ -62,7 +81,7 @@ ALL_DISPLAYED := $(DISPLAYED:.ml=.unlog.js) $(DISPLAYED:.ml=.pseudo.js) $(DISPLA
ALL_LINEOF := $(DISPLAYED:.ml=.token.js) $(DISPLAYED:.ml=.mlloc.js) $(DISPLAYED:.ml=.ptoken.js)
###############################################################
-# Tools
+##### Tools
OCAMLDEP := ocamldep -one-line
OCAMLPAR := OCAMLRUNPARAM="l=200M"
@@ -70,9 +89,11 @@ OCAMLPAR := OCAMLRUNPARAM="l=200M"
LINEOF_BIN := $(GENERATOR_DIR)/lineof.byte
LINEOF := $(OCAMLPAR) $(LINEOF_BIN)
+PPX_BIN := $(GENERATOR_DIR)/monad_ppx.byte
+PPX_FLAG := -ppx $(PPX_BIN)
+
MLTOJS_BIN := $(GENERATOR_DIR)/main.byte
-PPX_BIN := $(GENERATOR_DIR)/monad_ppx.native
-MLTOJS := $(OCAMLPAR) $(MLTOJS_BIN) -ppx $(PPX_BIN)
+MLTOJS := $(OCAMLPAR) $(MLTOJS_BIN) $(PPX_FLAG)
# -dsource is automatically considered by main.byte
ASSEMBLY_BIN := $(GENERATOR_DIR)/assembly.byte
@@ -85,28 +106,18 @@ DISPLAYGEN := $(OCAMLPAR) $(DISPLAYGEN_BIN)
$(MLTOJS_BIN) $(LINEOF_BIN) $(PPX_BIN) $(ASSEMBLY_BIN) $(DISPLAYGEN_BIN):
$(error Missing generator tools, build from project root, or set paths.)
-###############################################################
-# Dependencies
-
-ifeq ($(filter clean%,$(MAKECMDGOALS)),)
-include .depends
-endif
-
###############################################################
# Rules
-##### Rule for dependencies
-.depends: $(JSREF_ML)
- $(OCAMLDEP) -all $(<D)/* > $@
-
##### Rule for cmi
+# Ordering of these rules is important, mli rule must be first.
+%.cmi: %.mli
+ ocamlc $(REPLACE_STDLIB) $<
+
%.cmi: %.ml $(MLTOJS_BIN)
$(MLTOJS) -mode cmi -I $(STDLIB_DIR) $<
-%.cmi: %.mli
- ocamlc -I $(STDLIB_DIR) -open Stdlib $<
-
##### Rule for log/unlog/token
%.log.js: %.ml %.cmi $(MLTOJS_BIN)
@@ -133,21 +144,18 @@ lineof.js: $(ALL_LINEOF) $(LINEOF_BIN)
#--LATER (optional) add as dependencies the unlog files: $(JSREF_ML:.ml=.unlog.js)
-assembly.js: $(ASSEMBLY_JS) $(ASSEMBLY_BIN)
+assembly.js: $(ASSEMBLY_JS) $(ASEMBLY_BIN)
$(ASSEMBLY) -o $@ $(ASSEMBLY_JS)
-# -stdlib $(STDLIB_DIR)/stdlib.js
##### Rule for displayed_sources.js
displayed_sources.js: $(ALL_DISPLAYED) $(DISPLAYGEN_BIN)
$(DISPLAYGEN) -o $@ $(ALL_DISPLAYED)
-
-#####################################################################
+###############################################################
# Short targets
-ALL_TARGETS := lineof.js assembly.js displayed_sources.js
-all: $(ALL_TARGETS)
+jsjsref: assembly lineof display
cmi: $(JSREF_ML:.ml=.cmi) $(JSREF_MLI:.mli=.cmi)
@@ -167,22 +175,58 @@ assembly: assembly.js
display: displayed_sources.js
+DIRTY_EXTS := {log,unlog,token,pseudo,ptoken,mlloc}.js
+clean_jsjsref:
+ sh -c "rm -f {lineof,assembly,displayed_sources}.js"
+ sh -c "rm -f *.$(DIRTY_EXTS)"
+
+.PHONY: jsjsref cmi gen ref pseudo log unlog lineof assembly display clean_jsjsref
+
###############################################################
-# Global options
+###############################################################
+# ML-JSRef
-.PHONY: all cmi gen ref pseudo log unlog lineof assembly display clean
+# Strip all extensions of $(ASSEMBLY_JS) and replace with .cmo
+ASSEMBLY_ML_FILES := $(addsuffix .cmo,$(basename $(basename $(ASSEMBLY_JS_FILES))))
+ASSEMBLY_ML := $(ASSEMBLY_ML_FILES) \
+ run_js.cmo
-# Do not delete intermediate files.
-.SECONDARY:
+mljsref: main.byte
+
+main.byte: $(ASSEMBLY_ML)
+ ocamlfind ocamlc -linkpkg -package JS_Parser -o $@ $^
+
+run_js.cmo: run_js.ml run_js.mli run_js.cmi
+ ocamlfind ocamlc -c -package JS_Parser $<
+Translate_syntax.cmo: Translate_syntax.ml Translate_syntax.mli Translate_syntax.cmi
+ ocamlfind ocamlc -c -package JS_Parser $<
-#####################################################################
-# Clean
+# Ordering of the .cmo rules is important. mli dependency forces "standard" compilation
+%.cmo: %.ml %.mli %.cmi $(PPX_BIN)
+ ocamlc -c $(PPX_FLAG) $<
-DIRTY_EXTS := cmi,{mlloc,log,unlog,pseudo,token,ptoken}.js
+# Standalone .ml files
+%.cmo: %.ml %.cmi $(PPX_BIN)
+ ocamlc -c $(REPLACE_STDLIB) $(PPX_FLAG) $<
+clean_mljsref:
+ sh -c "rm -f $(ML_FRONTEND_SRC)/*.mli"
+ sh -c "rm -f {,$(ML_FRONTEND_SRC)/}*.{cmo,byte}"
+
+.PHONY: mljsref clean_mljsref
+
+##############################################################
+##############################################################
+# Global options
+
+clean: clean_jsjsref clean_mljsref
+ sh -c "rm -f *.cmi"
+ sh -c "rm -f .depends"
+
+# Phony global targets
+.PHONY: all clean
+
+# Do not delete intermediate files.
+.SECONDARY:
-clean:
- bash -c "rm -f $(ALL_TARGETS)"
- bash -c "rm -f *.{$(DIRTY_EXTS)}"
- bash -c "rm -f .depends"
diff --git a/jsref/ModuleExport.ml b/jsref/ModuleExport.ml
new file mode 100644
index 0000000..e69de29
diff --git a/jsref/ModuleExport.mli b/jsref/ModuleExport.mli
new file mode 100644
index 0000000..e69de29
diff --git a/jsref/Prheap.js b/jsref/Prheap.js
new file mode 100644
index 0000000..e69de29
diff --git a/jsref/Prheap.ml b/jsref/Prheap.ml
new file mode 100644
index 0000000..4b35687
--- /dev/null
+++ b/jsref/Prheap.ml
@@ -0,0 +1,390 @@
+open Shared
+open JsSyntax
+open JsInit
+
+let prbool = function
+ | true -> "true"
+ | false -> "false"
+
+let proption f = function
+ | None -> "None"
+ | Some x -> "Some (" ^ f x ^ ")"
+
+let prprealloc = function
+ | Coq_prealloc_global -> "Coq_prealloc_global"
+ | Coq_prealloc_global_eval -> "Coq_prealloc_global_eval"
+ | Coq_prealloc_global_parse_int -> "Coq_prealloc_global_parse_int"
+ | Coq_prealloc_global_parse_float -> "Coq_prealloc_global_parse_float"
+ | Coq_prealloc_global_is_finite -> "Coq_prealloc_global_is_finite"
+ | Coq_prealloc_global_is_nan -> "Coq_prealloc_global_is_nan"
+ | Coq_prealloc_global_decode_uri -> "Coq_prealloc_global_decode_uri"
+ | Coq_prealloc_global_decode_uri_component -> "Coq_prealloc_global_decode_uri_component"
+ | Coq_prealloc_global_encode_uri -> "Coq_prealloc_global_encode_uri"
+ | Coq_prealloc_global_encode_uri_component -> "Coq_prealloc_global_encode_uri_component"
+ | Coq_prealloc_object -> "Coq_prealloc_object"
+ | Coq_prealloc_object_get_proto_of -> "Coq_prealloc_object_get_proto_of"
+ | Coq_prealloc_object_get_own_prop_descriptor -> "Coq_prealloc_object_get_own_prop_descriptor"
+ | Coq_prealloc_object_get_own_prop_name -> "Coq_prealloc_object_get_own_prop_name"
+ | Coq_prealloc_object_create -> "Coq_prealloc_object_create"
+ | Coq_prealloc_object_define_prop -> "Coq_prealloc_object_define_prop"
+ | Coq_prealloc_object_define_props -> "Coq_prealloc_object_define_props"
+ | Coq_prealloc_object_seal -> "Coq_prealloc_object_seal"
+ | Coq_prealloc_object_freeze -> "Coq_prealloc_object_freeze"
+ | Coq_prealloc_object_prevent_extensions -> "Coq_prealloc_object_prevent_extensions"
+ | Coq_prealloc_object_is_sealed -> "Coq_prealloc_object_is_sealed"
+ | Coq_prealloc_object_is_frozen -> "Coq_prealloc_object_is_frozen"
+ | Coq_prealloc_object_is_extensible -> "Coq_prealloc_object_is_extensible"
+ | Coq_prealloc_object_keys -> "Coq_prealloc_object_keys"
+ | Coq_prealloc_object_keys_call -> "Coq_prealloc_object_keys_call"
+ | Coq_prealloc_object_proto -> "Coq_prealloc_object_proto"
+ | Coq_prealloc_object_proto_to_string -> "Coq_prealloc_object_proto_to_string"
+ | Coq_prealloc_object_proto_value_of -> "Coq_prealloc_object_proto_value_of"
+ | Coq_prealloc_object_proto_has_own_prop -> "Coq_prealloc_object_proto_has_own_prop"
+ | Coq_prealloc_object_proto_is_prototype_of -> "Coq_prealloc_object_proto_is_prototype_of"
+ | Coq_prealloc_object_proto_prop_is_enumerable -> "Coq_prealloc_object_proto_prop_is_enumerable"
+ | Coq_prealloc_function -> "Coq_prealloc_function"
+ | Coq_prealloc_function_proto -> "Coq_prealloc_function_proto"
+ | Coq_prealloc_function_proto_to_string -> "Coq_prealloc_function_proto_to_string"
+ | Coq_prealloc_function_proto_apply -> "Coq_prealloc_function_proto_apply"
+ | Coq_prealloc_function_proto_bind -> "Coq_prealloc_function_proto_bind"
+ | Coq_prealloc_function_proto_call -> "Coq_prealloc_function_proto_call"
+ | Coq_prealloc_bool -> "Coq_prealloc_bool"
+ | Coq_prealloc_bool_proto -> "Coq_prealloc_bool_proto"
+ | Coq_prealloc_bool_proto_to_string -> "Coq_prealloc_bool_proto_to_string"
+ | Coq_prealloc_bool_proto_value_of -> "Coq_prealloc_bool_proto_value_of"
+ | Coq_prealloc_number -> "Coq_prealloc_number"
+ | Coq_prealloc_number_proto -> "Coq_prealloc_number_proto"
+ | Coq_prealloc_number_proto_to_string -> "Coq_prealloc_number_proto_to_string"
+ | Coq_prealloc_number_proto_value_of -> "Coq_prealloc_number_proto_value_of"
+ | Coq_prealloc_number_proto_to_fixed -> "Coq_prealloc_number_proto_to_fixed"
+ | Coq_prealloc_number_proto_to_exponential -> "Coq_prealloc_number_proto_to_exponential"
+ | Coq_prealloc_number_proto_to_precision -> "Coq_prealloc_number_proto_to_precision"
+ | Coq_prealloc_array -> "Coq_prealloc_array"
+ | Coq_prealloc_array_is_array -> "Coq_prealloc_array_is_array"
+ | Coq_prealloc_array_proto -> "Coq_prealloc_array_proto"
+ | Coq_prealloc_array_proto_join -> "Coq_prealloc_array_proto_join"
+ | Coq_prealloc_array_proto_pop -> "Coq_prealloc_array_proto_pop"
+ | Coq_prealloc_array_proto_push -> "Coq_prealloc_array_proto_push"
+ | Coq_prealloc_array_proto_to_string -> "Coq_prealloc_array_proto_to_string"
+ | Coq_prealloc_string -> "Coq_prealloc_string"
+ | Coq_prealloc_string_proto -> "Coq_prealloc_string_proto"
+ | Coq_prealloc_string_proto_to_string -> "Coq_prealloc_string_proto_to_string"
+ | Coq_prealloc_string_proto_value_of -> "Coq_prealloc_string_proto_value_of"
+ | Coq_prealloc_string_proto_char_at -> "Coq_prealloc_string_proto_char_at"
+ | Coq_prealloc_string_proto_char_code_at -> "Coq_prealloc_string_proto_char_code_at"
+ | Coq_prealloc_math -> "Coq_prealloc_math"
+ | Coq_prealloc_mathop _ -> "Coq_prealloc_mathop"
+ | Coq_prealloc_date -> "Coq_prealloc_date"
+ | Coq_prealloc_regexp -> "Coq_prealloc_regexp"
+ | Coq_prealloc_error -> "Coq_prealloc_error"
+ | Coq_prealloc_native_error Coq_native_error_eval -> "Coq_prealloc_native_error_eval"
+ | Coq_prealloc_native_error Coq_native_error_range -> "Coq_prealloc_native_error_range"
+ | Coq_prealloc_native_error Coq_native_error_ref -> "Coq_prealloc_native_error_ref"
+ | Coq_prealloc_native_error Coq_native_error_syntax -> "Coq_prealloc_native_error_syntax"
+ | Coq_prealloc_native_error Coq_native_error_type -> "Coq_prealloc_native_error_type"
+ | Coq_prealloc_native_error Coq_native_error_uri -> "Coq_prealloc_native_error_uri"
+ | Coq_prealloc_native_error_proto Coq_native_error_eval -> "Coq_prealloc_native_error_proto_eval"
+ | Coq_prealloc_native_error_proto Coq_native_error_range -> "Coq_prealloc_native_error_proto_range"
+ | Coq_prealloc_native_error_proto Coq_native_error_ref -> "Coq_prealloc_native_error_proto_ref"
+ | Coq_prealloc_native_error_proto Coq_native_error_syntax -> "Coq_prealloc_native_error_proto_syntax"
+ | Coq_prealloc_native_error_proto Coq_native_error_type -> "Coq_prealloc_native_error_proto_type"
+ | Coq_prealloc_native_error_proto Coq_native_error_uri -> "Coq_prealloc_native_error_proto_uri"
+ | Coq_prealloc_throw_type_error -> "Coq_prealloc_throw_type_error"
+ | Coq_prealloc_error_proto -> "Coq_prealloc_error_proto"
+ | Coq_prealloc_error_proto_to_string -> "Coq_prealloc_error_proto_to_string"
+ | Coq_prealloc_json -> "Coq_prealloc_json"
+
+
+let prcall = function
+ | Coq_call_default -> "Coq_call_default"
+ | Coq_call_after_bind -> "Coq_call_after_bind"
+ | Coq_call_prealloc pa -> "Coq_call_prealloc " ^ prprealloc pa
+
+let prconstruct = function
+ | Coq_construct_default -> "Coq_construct_default"
+ | Coq_construct_after_bind -> "Coq_construct_after_bind"
+ | Coq_construct_prealloc pa -> "Coq_construct_prealloc " ^ prprealloc pa
+
+let prhas_instance = function
+ | Coq_builtin_has_instance_function -> "Coq_builtin_has_instance_function"
+ | Coq_builtin_has_instance_after_bind -> "Coq_builtin_has_instance_after_bind"
+
+let prget = function
+ | Coq_builtin_get_default -> "Coq_builtin_get_default"
+ | Coq_builtin_get_function -> "Coq_builtin_get_function"
+ | Coq_builtin_get_args_obj -> "Coq_builtin_get_args_obj"
+
+let prdelete = function
+ | Coq_builtin_delete_default -> "Coq_builtin_delete_default"
+ | Coq_builtin_delete_args_obj -> "Coq_builtin_delete_args_obj"
+
+let prloc = function
+ | Coq_object_loc_normal i -> "@" ^ string_of_int i
+ | Coq_object_loc_prealloc builtinid ->
+ prprealloc builtinid
+
+let prmutability = function
+ | Coq_mutability_uninitialized_immutable -> "Coq_mutability_uninitialized_immutable"
+ | Coq_mutability_immutable -> "Coq_mutability_immutable"
+ | Coq_mutability_nondeletable -> "Coq_mutability_nondeletable"
+ | Coq_mutability_deletable -> "Coq_mutability_deletable"
+
+let prenv_loc i =
+ "#" ^ string_of_int i
+
+let prlexical_env l =
+ String.concat ", " (List.map prenv_loc l)
+
+let string_of_char_list cl = cl
+
+let prprop_name = string_of_char_list
+
+let prlabel = function
+ | Coq_label_empty -> "<empty>"
+ | Coq_label_string l -> "label:" ^ string_of_char_list l
+
+let prlabel_set s =
+ "{ " ^ String.concat "; " (List.map prlabel s) ^ " }"
+
+let char_list_of_string s =
+ let rec acc_ch acc n =
+ if n < 0 then acc else acc_ch ((String.get s n)::acc) (n-1)
+ in
+ acc_ch [] ((String.length s) - 1)
+
+let prbinary_op = function
+ | Coq_binary_op_add -> "+"
+ | Coq_binary_op_mult -> "*"
+ | Coq_binary_op_div -> "/"
+ | Coq_binary_op_equal -> "==="
+ | Coq_binary_op_instanceof -> "instanceof"
+ | Coq_binary_op_in -> "in"
+ | _ -> "Binary Op NIY"
+
+let prliteral = function
+ | Coq_literal_null -> "null"
+ | Coq_literal_bool b -> string_of_bool b
+ | Coq_literal_number f -> string_of_float f
+ | Coq_literal_string cl -> string_of_char_list cl
+
+let prprim = function
+ | Coq_prim_undef -> "undefined"
+ | Coq_prim_null -> "null"
+ | Coq_prim_bool b -> string_of_bool b
+ | Coq_prim_number f -> string_of_float f
+ | Coq_prim_string cl -> "\"" ^ string_of_char_list cl ^ "\""
+
+let prvalue = function
+ | Coq_value_prim p -> prprim p
+ | Coq_value_object ol -> prloc ol
+
+let prattributes = function
+ | Coq_attributes_data_of d ->
+ Printf.sprintf "{ value: %s, writable: %s, enum: %s, config: %s }"
+ (prvalue (attributes_data_value d))
+ (prbool (attributes_data_writable d))
+ (prbool (attributes_data_enumerable d))
+ (prbool (attributes_data_configurable d))
+ | Coq_attributes_accessor_of a ->
+ Printf.sprintf "{ get: %s, set: %s, enum: %s, config: %s }"
+ (prvalue (attributes_accessor_get a))
+ (prvalue (attributes_accessor_set a))
+ (prbool (attributes_accessor_enumerable a))
+ (prbool (attributes_accessor_configurable a))
+
+let prfull_descriptor = function
+ | Coq_full_descriptor_undef -> "undef"
+ | Coq_full_descriptor_some a -> "attribute: " ^ prattributes a
+
+let prdescriptor desc =
+ Printf.sprintf "{ value : %s ; writable : %s ; get : %s ; set : %s ; enumerable : %s ; configurable : %s }"
+ (proption prvalue desc.descriptor_value)
+ (proption prbool desc.descriptor_writable)
+ (proption prvalue desc.descriptor_get)
+ (proption prvalue desc.descriptor_set)
+ (proption prbool desc.descriptor_enumerable)
+ (proption prbool desc.descriptor_configurable)
+
+let remove_siblings l =
+ let l' = List.stable_sort (fun (k1, _) (k2, _) -> compare k1 k2) l in
+ let rec aux = function
+ | [] -> []
+ | (k1, v) :: (k2, _) :: l when k1 = k2 ->
+ aux ((k1, v) :: l)
+ | a :: l -> a :: aux l
+ in aux l'
+
+let heap_to_list h =
+ remove_siblings (Heap.to_list () h)
+
+let probject_properties_aux skip_init old str p =
+ String.concat "" (List.fold_left
+ (fun acc (x, a) ->
+ if skip_init
+ && option_case false (fun old0 ->
+ List.mem (x, a) old0) old
+ then acc
+ else Printf.sprintf "\t %s %s = %s;\n"
+ str
+ (string_of_char_list x)
+ (prattributes a)
+ :: acc) []
+ (heap_to_list p))
+
+let probject_properties = probject_properties_aux false None ""
+
+let prfieldmap (old : (prop_name * attributes) list option) skip_init loc obj =
+ probject_properties_aux skip_init old (prloc loc ^ " .") (obj.object_properties_)
+
+
+let prheap =
+ let list_heap_init = heap_to_list object_heap_initial in
+ fun skip_init heap ->
+ "digraph g{\n" ^
+ "node [shape=record];\n" ^
+ "rankdir=LR;\n" ^
+ (String.concat ""
+ (List.rev (List.map (fun (key, v) ->
+ let str =
+ let old =
+ try Some (List.assoc key list_heap_init)
+ with Not_found -> None in
+ prfieldmap (option_case None (fun obj ->
+ Some (heap_to_list (object_properties_ obj))) old)
+ skip_init key v ^
+ String.concat "" (
+ let pr s p g =
+ if p (g v) = "" || (skip_init
+ && option_case false (fun obj ->
+ g v = g obj) old)
+ then ""
+ else
+ Printf.sprintf "\t %s @ %s = %s;\n"
+ (prloc key) s (p (g v)) in [
+ pr "proto" prvalue object_proto_ ;
+ pr "class" string_of_char_list object_class_ ;
+ pr "this" (option_case "" prvalue) (fun obj -> obj.object_bound_this_) ;
+ pr "call" (option_case "" prcall) object_call_ ;
+ pr "construct" (option_case "" prconstruct) object_construct_ ;
+ pr "has_instance" (option_case "" prhas_instance) object_has_instance_ ;
+ pr "prim_value" (option_case "" prvalue) object_prim_value_ ;
+ pr "extensible" prbool object_extensible_ ;
+ pr "get" prget object_get_ ;
+ pr "delete" prdelete (fun obj -> obj.object_delete_) ;
+ pr "scope" (option_case "" prlexical_env) object_scope_ ;
+ ]) in
+ if str = "" then Printf.sprintf "\t %s, an object;\n" (prloc key)
+ else str) (heap_to_list heap)
+ ))) ^
+ "}"
+
+let prenv_record r =
+ String.concat "\n"
+ (List.rev (List.map (fun (loc, er) ->
+ prenv_loc loc ^ " -> " ^
+ match er with
+ | Coq_env_record_decl der ->
+ String.concat "\n" (List.rev (List.map (fun (x, (mu, v)) ->
+ "\t\"" ^ string_of_char_list x ^ "\" -> " ^
+ prmutability mu ^ ", " ^ prvalue v
+ ) (heap_to_list der)))
+ | Coq_env_record_object (o, this) ->
+ prloc o ^ " with provide this = " ^ prbool this
+ ) (heap_to_list r)
+ ))
+
+let prstate skip s =
+ "State:\n" ^
+ "\tHeap:\n" ^ prheap skip (state_object_heap s) ^
+ "\n\tEnv. Record:\n" ^ prenv_record (state_env_record_heap s)
+
+let formatterstate formatter state =
+ Format.fprintf formatter "%s" (prstate false state)
+
+
+let prrestype = function
+ | Coq_restype_normal -> "normal"
+ | Coq_restype_break -> "break"
+ | Coq_restype_continue -> "continue"
+ | Coq_restype_return -> "return"
+ | Coq_restype_throw -> "throw"
+
+let prref_base_type = function
+ | Coq_ref_base_type_value v -> "value: " ^ prvalue v
+ | Coq_ref_base_type_env_loc l -> "env_loc: " ^ prenv_loc l
+
+let prref { ref_base = rb ; ref_name = rn ; ref_strict = str } =
+ (if str then "strict " else "") ^ "ref: (" ^ prref_base_type rb ^ ") . " ^ prprop_name rn
+
+let prresvalue = function
+ | Coq_resvalue_empty -> "Coq_resvalue_empty"
+ | Coq_resvalue_value v -> "Coq_resvalue_value: " ^ prvalue v
+ | Coq_resvalue_ref r -> "Coq_resvalue_ref: " ^ prref r
+
+(*
+module M1 = Map.Make (struct type t = loc let compare = Pervasives.compare end)
+module M2 = Map.Make (struct type t = field let compare = Pervasives.compare end)
+
+let id = ref 0
+
+let new_id () =
+ incr id; "__" ^ (string_of_int (!id))
+let print_to_file f h=
+ let oc = open_out f in
+ output_string oc (main h);
+ close_out oc
+ *)
+
+
+let dump_expr_step = function
+ | Coq_expr_this -> "Expr_this"
+ | Coq_expr_identifier _ -> "Expr_identifier"
+ | Coq_expr_literal _ -> "Expr_literal"
+ | Coq_expr_object _ -> "Expr_object"
+ | Coq_expr_array _ -> "Expr_array"
+ | Coq_expr_function _ -> "Expr_function"
+ | Coq_expr_access _ -> "Expr_access"
+ | Coq_expr_member _ -> "Expr_member"
+ | Coq_expr_new _ -> "Expr_new"
+ | Coq_expr_call _ -> "Expr_call"
+ | Coq_expr_unary_op _ -> "Expr_unary_op"
+ | Coq_expr_binary_op _ -> "Expr_binary_op"
+ | Coq_expr_conditional _ -> "Expr_conditional"
+ | Coq_expr_assign _ -> "Expr_assign"
+
+let dump_propbody_step = function
+ | Coq_propbody_val _ -> "Propbody_val"
+ | Coq_propbody_get _ -> "Propbody_get"
+ | Coq_propbody_set _ -> "Propbody_set"
+
+let dump_funcbody_step = function
+ | Coq_funcbody_intro _ -> "Funcbody_intro"
+
+let dump_stat_step = function
+ | Coq_stat_expr _ -> "Stat_expr"
+ | Coq_stat_block _ -> "Stat_block"
+ | Coq_stat_label (l, _) -> "Stat_label: " ^ string_of_char_list l
+ | Coq_stat_var_decl _ -> "Stat_var_decl"
+ | Coq_stat_if _ -> "Stat_if"
+ | Coq_stat_while _ -> "Stat_while"
+ | Coq_stat_do_while _ -> "Stat_do_while"
+ | Coq_stat_with _ -> "Stat_with"
+ | Coq_stat_throw _ -> "Stat_throw"
+ | Coq_stat_return _ -> "Stat_return"
+ | Coq_stat_break _ -> "Stat_break"
+ | Coq_stat_continue _ -> "Stat_continue"
+ | Coq_stat_try _ -> "Stat_try"
+ | Coq_stat_for _ -> "Stat_for"
+ | Coq_stat_for_var _ -> "Stat_for_var"
+ | Coq_stat_for_in _ -> "Stat_for_in"
+ | Coq_stat_for_in_var _ -> "Stat_for_in_var"
+ | Coq_stat_debugger -> "Stat_debugger"
+ | Coq_stat_switch (_, _, _) -> "Stat_switch"
+
+let dump_prog_step = function
+ | Coq_prog_intro (b, es) ->
+ String.concat " ; "
+ (List.map (function
+ | Coq_element_stat _ -> "Element_stat"
+ | Coq_element_func_decl _ -> "Element_func_decl") es)
+
diff --git a/jsref/Prheap.mli b/jsref/Prheap.mli
new file mode 100644
index 0000000..a594761
--- /dev/null
+++ b/jsref/Prheap.mli
@@ -0,0 +1,6 @@
+val string_of_char_list : string -> string
+val prvalue : JsSyntax.value -> string
+val prstate : bool (* skip init *) -> JsSyntax.state -> string
+val prref : JsSyntax.ref -> string
+val prresvalue : JsSyntax.resvalue -> string
+val prloc : JsSyntax.object_loc -> string
diff --git a/jsref/Translate_syntax.js b/jsref/Translate_syntax.js
index df83e1b..f997129 100644
--- a/jsref/Translate_syntax.js
+++ b/jsref/Translate_syntax.js
@@ -1,6 +1,6 @@
var Translate_syntax = {
eval_counter: 0,
- parse_esprima: function (strictness, src) {
+ parse_js_syntax: function (strictness, src) {
try {
// EVAL: Uncomment line below to enable multiple eval tabs
//return Some(parseSource(src, "_eval_" + Translate_syntax.eval_counter++, true));
diff --git a/jsref/Translate_syntax.ml b/jsref/Translate_syntax.ml
new file mode 100644
index 0000000..f423301
--- /dev/null
+++ b/jsref/Translate_syntax.ml
@@ -0,0 +1,375 @@
+open Fappli_IEEE_bits
+open JsNumber
+open Parser_syntax
+open List
+
+exception CoqSyntaxDoesNotSupport of string
+exception Empty_list
+
+let string_to_coq s = s
+
+let unary_op_to_coq op : JsSyntax.unary_op =
+ match op with
+ | Not -> JsSyntax.Coq_unary_op_not
+ | TypeOf -> JsSyntax.Coq_unary_op_typeof
+ | Positive -> JsSyntax.Coq_unary_op_add
+ | Negative -> JsSyntax.Coq_unary_op_neg
+ | Pre_Decr -> JsSyntax.Coq_unary_op_pre_decr
+ | Post_Decr -> JsSyntax.Coq_unary_op_post_decr
+ | Pre_Incr -> JsSyntax.Coq_unary_op_pre_incr
+ | Post_Incr -> JsSyntax.Coq_unary_op_post_incr
+ | Bitnot -> JsSyntax.Coq_unary_op_bitwise_not
+ | Void -> JsSyntax.Coq_unary_op_void
+
+let arith_op_to_coq op : JsSyntax.binary_op =
+ begin match op with
+ | Plus -> JsSyntax.Coq_binary_op_add
+ | Minus -> JsSyntax.Coq_binary_op_sub
+ | Times -> JsSyntax.Coq_binary_op_mult
+ | Div -> JsSyntax.Coq_binary_op_div
+ | Mod -> JsSyntax.Coq_binary_op_mod
+ | Bitand -> JsSyntax.Coq_binary_op_bitwise_and
+ | Bitor -> JsSyntax.Coq_binary_op_bitwise_or
+ | Bitxor -> JsSyntax.Coq_binary_op_bitwise_xor
+ | Ursh -> JsSyntax.Coq_binary_op_unsigned_right_shift
+ | Lsh -> JsSyntax.Coq_binary_op_left_shift
+ | Rsh -> JsSyntax.Coq_binary_op_right_shift
+ end
+
+let bin_op_to_coq op : JsSyntax.binary_op =
+ match op with
+ | Comparison op ->
+ begin match op with
+ | Lt -> JsSyntax.Coq_binary_op_lt
+ | Le -> JsSyntax.Coq_binary_op_le
+ | Gt -> JsSyntax.Coq_binary_op_gt
+ | Ge -> JsSyntax.Coq_binary_op_ge
+ | Equal -> JsSyntax.Coq_binary_op_equal
+ | NotEqual -> JsSyntax.Coq_binary_op_disequal
+ | TripleEqual -> JsSyntax.Coq_binary_op_strict_equal
+ | NotTripleEqual -> JsSyntax.Coq_binary_op_strict_disequal
+ | In -> JsSyntax.Coq_binary_op_in
+ | InstanceOf -> JsSyntax.Coq_binary_op_instanceof
+ end
+ | Arith op -> arith_op_to_coq op
+ | Boolean op ->
+ begin match op with
+ | And -> JsSyntax.Coq_binary_op_and
+ | Or -> JsSyntax.Coq_binary_op_or
+ end
+
+let exp_to_literal exp : JsSyntax.literal =
+ match exp.exp_stx with
+ | Num n -> JsSyntax.Coq_literal_number n
+ | String s -> JsSyntax.Coq_literal_string (string_to_coq s)
+ | Null -> JsSyntax.Coq_literal_null
+ | Bool b -> JsSyntax.Coq_literal_bool b
+ | _ -> raise Parser.InvalidArgument
+
+let rec exp_to_exp exp : JsSyntax.expr =
+ let f = exp_to_exp in
+ let string_to_coq_op e = match e with
+ | None -> None
+ | Some e -> Some (string_to_coq e) in
+ match exp.exp_stx with
+ (* Literals *)
+ | Num _
+ | String _
+ | Null
+ | Bool _ -> JsSyntax.Coq_expr_literal (exp_to_literal exp)
+
+ | RegExp _ -> raise (CoqSyntaxDoesNotSupport (Pretty_print.string_of_exp false exp))
+ | This -> JsSyntax.Coq_expr_this
+ | Var v -> JsSyntax.Coq_expr_identifier (string_to_coq v)
+ | Delete e -> JsSyntax.Coq_expr_unary_op (JsSyntax.Coq_unary_op_delete, f e)
+ | Access (e, v) -> JsSyntax.Coq_expr_member (f e, string_to_coq v)
+ | Unary_op (op, e) -> JsSyntax.Coq_expr_unary_op (unary_op_to_coq op, f e)
+ | BinOp (e1, op, e2) -> JsSyntax.Coq_expr_binary_op (f e1, bin_op_to_coq op, f e2)
+ | Assign (e1, e2) -> JsSyntax.Coq_expr_assign (f e1, None, f e2)
+ | AssignOp (e1, op, e2) -> JsSyntax.Coq_expr_assign (f e1, Some (arith_op_to_coq op), f e2)
+ | CAccess (e1, e2) -> JsSyntax.Coq_expr_access (f e1, f e2)
+ | Comma (e1, e2) -> JsSyntax.Coq_expr_binary_op (f e1, JsSyntax.Coq_binary_op_coma, f e2)
+ | Call (e1, e2s) -> JsSyntax.Coq_expr_call (f e1, map (fun e2 -> f e2) e2s)
+ | New (e1, e2s) -> JsSyntax.Coq_expr_new (f e1, map (fun e2 -> f e2) e2s)
+ | FunctionExp (s, n, vs, e) -> JsSyntax.Coq_expr_function ((string_to_coq_op n), (map string_to_coq vs), exp_to_funcbody e s)
+ | Function (s, n, vs, e) -> JsSyntax.Coq_expr_function ((string_to_coq_op n), (map string_to_coq vs), exp_to_funcbody e s)
+ | Obj xs -> JsSyntax.Coq_expr_object (map (fun (pn,p,e) ->
+ (match pn with
+ | PropnameId id -> JsSyntax.Coq_propname_identifier (string_to_coq id)
+ | PropnameString s -> JsSyntax.Coq_propname_string (string_to_coq s)
+ | PropnameNum n -> JsSyntax.Coq_propname_number n
+ ),
+ (match p with
+ | PropbodyVal -> JsSyntax.Coq_propbody_val (f e)
+ | PropbodyGet ->
+ begin match e.exp_stx with
+ | FunctionExp (s, None, vs, e) -> JsSyntax.Coq_propbody_get (exp_to_funcbody e s)
+ | Function (s, None, vs, e) -> JsSyntax.Coq_propbody_get (exp_to_funcbody e s)
+ | _ -> raise Parser.InvalidArgument
+ end
+ | PropbodySet ->
+ begin match e.exp_stx with
+ | FunctionExp (s, None, vs, e) -> JsSyntax.Coq_propbody_set (map string_to_coq vs, exp_to_funcbody e s)
+ | Function (s, None, vs, e) -> JsSyntax.Coq_propbody_set (map string_to_coq vs, exp_to_funcbody e s)
+ | _ -> raise Parser.InvalidArgument
+ end)
+ ) xs)
+ (* _ARRAYS_ : Parsing array arguments *)
+ | Array oes -> JsSyntax.Coq_expr_array (map (fun oe -> begin match oe with
+ | None -> None
+ | Some e -> Some (f e)
+ end) oes)
+ | ConditionalOp (e1, e2, e3) -> JsSyntax.Coq_expr_conditional (f e1, f e2, f e3)
+
+ (*Statements*)
+ | Skip
+ | Return _
+ | Break _
+ | Continue _
+ | Debugger
+ | VarDec _
+ | Throw _
+ | Label _
+ | While _
+ | DoWhile _
+ | With _
+ | Try _
+ | If _
+ | ForIn _
+ | For _
+ | Switch _
+ | Block _
+ | Script _ -> raise Parser.InvalidArgument
+
+and exp_to_stat exp : JsSyntax.stat =
+ let f = exp_to_stat in
+ match exp.exp_stx with
+ (* Literals *)
+ | Num _
+ | String _
+ | Null
+ | Bool _
+
+ (* Expressions *)
+ | RegExp _
+ | This
+ | Var _
+ | Delete _
+ | Access _
+ | Unary_op _
+ | BinOp _
+ | Assign _
+ | AssignOp _
+ | CAccess _
+ | Comma _
+ | Call _
+ | New _
+ | Obj _
+ | Array _
+ | ConditionalOp _
+ | FunctionExp _ -> JsSyntax.Coq_stat_expr (exp_to_exp exp)
+
+ | Function _ -> raise Parser.InvalidArgument
+ (* If a function appears in the middle of a statement, it shall not be interpreted as an expression function, but as a function declaration *)
+ (* NOTE in spec p.86 *)
+ (* ... It is recommended that ECMAScript implementations either disallow this usage of FunctionDeclaration or issue a warning *)
+
+ (*Statements*)
+ | Skip -> JsSyntax.Coq_stat_block []
+ | Return (Some e) -> JsSyntax.Coq_stat_return (Some (exp_to_exp e))
+ | Return None -> JsSyntax.Coq_stat_return None
+ | Break (Some l) -> JsSyntax.Coq_stat_break (JsSyntax.Coq_label_string (string_to_coq l))
+ | Break None -> JsSyntax.Coq_stat_break JsSyntax.Coq_label_empty
+ | Continue (Some l) -> JsSyntax.Coq_stat_continue (JsSyntax.Coq_label_string (string_to_coq l))
+ | Continue None -> JsSyntax.Coq_stat_continue JsSyntax.Coq_label_empty
+ | Debugger -> JsSyntax.Coq_stat_debugger
+ | VarDec vs -> JsSyntax.Coq_stat_var_decl (map (fun (v, e) ->
+ string_to_coq v, match e with None -> None | Some e -> Some (exp_to_exp e)) vs)
+ | Throw e -> JsSyntax.Coq_stat_throw (exp_to_exp e)
+ | Label (l, e) -> JsSyntax.Coq_stat_label (string_to_coq l, f e)
+ | While (e1, e2) -> JsSyntax.Coq_stat_while ([], exp_to_exp e1, f e2)
+ | DoWhile (e1, e2) -> JsSyntax.Coq_stat_do_while ([], f e1, exp_to_exp e2)
+ | With (e1, e2) -> JsSyntax.Coq_stat_with (exp_to_exp e1, f e2)
+ | Try (e, None, None) -> JsSyntax.Coq_stat_try (f e, None, None)
+ | Try (e, None, Some fe) -> JsSyntax.Coq_stat_try (f e, None, Some (f fe))
+ | Try (e, Some (s, ce), None) -> JsSyntax.Coq_stat_try (f e, Some (string_to_coq s, f ce), None)
+ | Try (e, Some (s, ce), Some fe) -> JsSyntax.Coq_stat_try (f e, Some (string_to_coq s, f ce), Some (f fe))
+ | If (e1, e2, Some e3) -> JsSyntax.Coq_stat_if (exp_to_exp e1, f e2, Some (f e3))
+ | If (e1, e2, None) -> JsSyntax.Coq_stat_if (exp_to_exp e1, f e2, None)
+ | ForIn (e1, e2, e3) -> raise (CoqSyntaxDoesNotSupport (Pretty_print.string_of_exp false exp))
+ | For (e1, e2, e3, e4) ->
+ let to_option expr = begin match expr with
+ | None -> None
+ | Some(real_e) -> Some (exp_to_exp real_e) end in
+ (match e1 with
+ | Some ({exp_offset; exp_stx = (VarDec vs); exp_annot}) ->
+ JsSyntax.Coq_stat_for_var ([], (map (fun (v, e) ->
+ string_to_coq v, match e with None -> None
+ | Some e -> Some (exp_to_exp e)) vs),
+ to_option e2, to_option e3, f e4)
+ | _ ->
+ JsSyntax.Coq_stat_for ([], to_option e1, to_option e2, to_option e3, f e4))
+ | Switch (e1, e2s) ->
+ let (firstpart, defaultcase, secondpart) = List.fold_left (fun (fi, de, se) el -> (
+ if de = None then
+ match el with
+ | (DefaultCase, {exp_stx = Block es}) -> (fi, Some (List.map f es), [])
+ | (Case cexp, {exp_stx = Block es}) -> (fi @ [JsSyntax.Coq_switchclause_intro (exp_to_exp cexp, List.map f es)], None, [])
+ | _ -> raise CannotHappen
+ else match el with
+ | (Case cexp, {exp_stx = Block es}) -> (fi, de, se @ [JsSyntax.Coq_switchclause_intro (exp_to_exp cexp, List.map f es)])
+ | _ -> raise CannotHappen
+ )) ([], None, []) e2s in
+ let switchbody = match defaultcase with
+ | None -> JsSyntax.Coq_switchbody_nodefault firstpart
+ | Some de -> JsSyntax.Coq_switchbody_withdefault (firstpart, de, secondpart) in
+ JsSyntax.Coq_stat_switch ([], exp_to_exp e1, switchbody)
+ | Block es -> JsSyntax.Coq_stat_block (List.map f es)
+
+ | Script _ -> raise Parser.InvalidArgument
+
+and exp_to_prog exp : JsSyntax.prog =
+ match exp.exp_stx with
+ | Script (s, e2s) -> JsSyntax.Coq_prog_intro (s, map exp_to_elem e2s)
+ | Block (e2s) -> JsSyntax.Coq_prog_intro (false, map exp_to_elem e2s)
+ | _ -> JsSyntax.Coq_prog_intro (false, [exp_to_elem exp])
+
+and exp_to_elem exp : JsSyntax.element =
+ let tos = string_to_coq in
+ match exp.exp_stx with
+ | FunctionExp (s, (Some name), args, body) -> JsSyntax.Coq_element_func_decl (tos name, map tos args, exp_to_funcbody body s)
+ | Function (s, (Some name), args, body) -> JsSyntax.Coq_element_func_decl (tos name, map tos args, exp_to_funcbody body s)
+ | _ -> JsSyntax.Coq_element_stat (exp_to_stat exp)
+
+and exp_to_funcbody exp strict : JsSyntax.funcbody =
+ let body =
+ match exp_to_prog exp with
+ | JsSyntax.Coq_prog_intro (_, elems) -> JsSyntax.Coq_prog_intro (strict, elems)
+ in JsSyntax.Coq_funcbody_intro (body, "")
+
+module JsSyntaxInfos = struct
+ open JsSyntax
+ open JsSyntaxAux
+
+ let rec add_infos_exp str e =
+ let f = add_infos_exp str in
+ (match e with
+ | Coq_expr_this -> e
+ | Coq_expr_identifier s -> e
+ | Coq_expr_literal l -> e
+ | Coq_expr_object l -> e
+ | Coq_expr_array oes ->
+ Coq_expr_array
+ (List.map (fun oe ->
+ match oe with
+ | Some e0 -> Some (f e0)
+ | None -> None) oes)
+ | Coq_expr_function (so, ss, fb) ->
+ Coq_expr_function (so, ss, (add_infos_funcbody str fb))
+ | Coq_expr_access (e1, e2) -> Coq_expr_access ((f e1), (f e2))
+ | Coq_expr_member (e0, s) -> Coq_expr_member ((f e0), s)
+ | Coq_expr_new (e0, es) -> Coq_expr_new ((f e0), (List.map f es))
+ | Coq_expr_call (e0, es) -> Coq_expr_call ((f e0), (List.map f es))
+ | Coq_expr_unary_op (op, e0) -> Coq_expr_unary_op (op, (f e0))
+ | Coq_expr_binary_op (e1, op, e2) ->
+ Coq_expr_binary_op ((f e1), op, (f e2))
+ | Coq_expr_conditional (e1, e2, e3) ->
+ Coq_expr_conditional ((f e1), (f e2), (f e3))
+ | Coq_expr_assign (e1, op, e2) -> Coq_expr_assign ((f e1), op, (f e2)))
+
+ (** val add_infos_funcbody : strictness_flag -> funcbody -> funcbody **)
+
+ and add_infos_funcbody str = function
+ | Coq_funcbody_intro (p, s) -> Coq_funcbody_intro ((add_infos_prog str p), s)
+
+ (** val add_infos_stat : strictness_flag -> label_set -> stat -> stat **)
+
+ and add_infos_stat str labs t =
+ let opt = fun f smth ->
+ match smth with
+ | Some smth0 -> Some (f smth0)
+ | None -> None
+ in
+ let f = add_infos_stat str label_set_empty in
+ let fo = opt f in
+ let fe = add_infos_exp str in
+ let feo = opt fe in
+ let fsb = add_infos_switchbody str in
+ (match t with
+ | Coq_stat_expr e -> Coq_stat_expr (fe e)
+ | Coq_stat_label (l, t0) ->
+ Coq_stat_label (l,
+ (add_infos_stat str (label_set_add (Coq_label_string l) labs) t0))
+ | Coq_stat_block ts -> Coq_stat_block (List.map f ts)
+ | Coq_stat_var_decl vars ->
+ Coq_stat_var_decl
+ (List.map (fun var -> let (s, eo) = var in (s, (feo eo))) vars)
+ | Coq_stat_if (e, t0, to0) -> Coq_stat_if ((fe e), (f t0), (fo to0))
+ | Coq_stat_do_while (l, t0, e) ->
+ Coq_stat_do_while ((label_set_add_empty labs), (f t0), (fe e))
+ | Coq_stat_while (l, e, t0) ->
+ Coq_stat_while ((label_set_add_empty labs), (fe e), (f t0))
+ | Coq_stat_with (e, t0) -> Coq_stat_with ((fe e), (f t0))
+ | Coq_stat_throw e -> Coq_stat_throw (fe e)
+ | Coq_stat_return eo -> Coq_stat_return (feo eo)
+ | Coq_stat_break lopt -> Coq_stat_break lopt
+ | Coq_stat_continue lopt -> Coq_stat_continue lopt
+ | Coq_stat_try (t0, catch, to0) ->
+ Coq_stat_try ((f t0),
+ (opt (fun c -> let (cs, t1) = c in (cs, (f t1))) catch), (fo to0))
+ | Coq_stat_for (l, eo1, eo2, eo3, t0) ->
+ Coq_stat_for ((label_set_add_empty labs), (feo eo1), (feo eo2),
+ (feo eo3), (f t0))
+ | Coq_stat_for_var (l, vars, eo2, eo3, t0) ->
+ Coq_stat_for_var ((label_set_add_empty labs),
+ (List.map (fun var -> let (s, eo) = var in (s, (feo eo))) vars), (feo eo2),
+ (feo eo3), (f t0))
+ | Coq_stat_for_in (l, e1, e2, t0) ->
+ Coq_stat_for_in ((label_set_add_empty labs), (fe e1), (fe e2), (f t0))
+ | Coq_stat_for_in_var (l, str0, eo, e, t0) ->
+ Coq_stat_for_in_var ((label_set_add_empty labs), str0, (feo eo),
+ (fe e), (f t0))
+ | Coq_stat_debugger -> Coq_stat_debugger
+ | Coq_stat_switch (labs0, e, ts) ->
+ Coq_stat_switch ((label_set_add_empty labs0), (fe e), (fsb ts)))
+
+ (** val add_infos_switchbody :
+ strictness_flag -> switchbody -> switchbody **)
+
+ and add_infos_switchbody str ts =
+ let fe = add_infos_exp str in
+ let fs = add_infos_stat str label_set_empty in
+ let f = fun sc ->
+ let Coq_switchclause_intro (e, l) = sc in
+ Coq_switchclause_intro ((fe e), (List.map fs l))
+ in
+ (match ts with
+ | Coq_switchbody_nodefault l -> Coq_switchbody_nodefault (List.map f l)
+ | Coq_switchbody_withdefault (l1, s, l2) ->
+ Coq_switchbody_withdefault ((List.map f l1), (List.map fs s), (List.map f l2)))
+
+ (** val add_infos_prog : strictness_flag -> prog -> prog **)
+
+ and add_infos_prog str = function
+ | Coq_prog_intro (str', els) ->
+ let str'' = str || str' in
+ Coq_prog_intro (str'', (List.map (add_infos_element str'') els))
+
+ (** val add_infos_element : strictness_flag -> element -> element **)
+
+ and add_infos_element str = function
+ | Coq_element_stat t ->
+ Coq_element_stat (add_infos_stat str label_set_empty t)
+ | Coq_element_func_decl (s, ss, fb) ->
+ Coq_element_func_decl (s, ss, (add_infos_funcbody str fb))
+end
+
+let parse (p : ?force_strict:bool -> string -> Parser_syntax.exp) strictness s =
+ let exp = p ~force_strict:strictness s in
+ JsSyntaxInfos.add_infos_prog strictness (exp_to_prog exp)
+
+let parse_js_syntax strictness str =
+ try Some (parse Parser_main.exp_from_string strictness str)
+ with _ -> (prerr_endline ("Parser failure on input \"" ^ str ^ "\""); None)
+
+let parse_js_syntax_from_file = parse (Parser_main.exp_from_file ~init:false)
diff --git a/jsref/Translate_syntax.mli b/jsref/Translate_syntax.mli
index c3e2a37..cd2b29a 100644
--- a/jsref/Translate_syntax.mli
+++ b/jsref/Translate_syntax.mli
@@ -1,2 +1,8 @@
(* parse_esprima strictness source *)
-val parse_esprima : bool -> string -> JsSyntax.prog option
+val parse_js_syntax : bool -> string -> JsSyntax.prog option
+
+(* Not implemented in JS *)
+(* potentially throws an exception *)
+val parse_js_syntax_from_file : bool -> string -> JsSyntax.prog
+
+exception CoqSyntaxDoesNotSupport of string
diff --git a/jsref/run_js.ml b/jsref/run_js.ml
new file mode 100644
index 0000000..fd68c02
--- /dev/null
+++ b/jsref/run_js.ml
@@ -0,0 +1,225 @@
+exception AbnormalPreludeTermination of JsInterpreterMonads.result
+
+let file = ref ""
+let test_prelude = ref []
+let test = ref false
+let printHeap = ref false
+let skipInit = ref false
+let noParasite = ref false
+let strictMode = ref false
+let parser_path = ref None
+
+let string_to_list str = (* Does it already exists somewhere? *)
+ let l = ref [] in
+ let current = ref "" in
+ String.iter (fun c ->
+ if c = ',' then (
+ l := !current :: !l ;
+ current := ""
+ ) else
+ current := !current ^ String.make 1 c
+ ) str ;
+ !current :: List.rev !l
+
+let arguments () =
+ let usage_msg="Usage: -jsparser <path> -file <path>" in
+ Arg.parse
+ [ "-json",
+ Arg.Set Parser_main.use_json,
+ "use the JSON parser (Esprima), -jsparser argument is ignored";
+
+ "-jsparser",
+ Arg.String(fun f -> parser_path := Some f),
+ "path to JS_Parser runtime directory (optional, if omitted uses findlib to discover)";
+
+ "-file",
+ Arg.Set_string file,
+ "file to run";
+
+ "-verbose",
+ Arg.Set Parser_main.verbose,
+ "print the parsed program";
+
+ "-test_prelude",
+ Arg.String(fun f ->
+ test_prelude := !test_prelude @ string_to_list f; test := true),
+ "include the given files before runnning the specified file";
+
+ "-print-heap",
+ Arg.Set printHeap,
+ "print the final state of the heap";
+
+ "-skip-init",
+ Arg.Set skipInit,
+ "do not print the initial heap";
+
+ "-no-parasite",
+ Arg.Set noParasite,
+ "do not run interpreter's code without being explicitely asked for";
+
+ "-force-strict",
+ Arg.Set strictMode,
+ "force strict mode"
+ ]
+ (fun s -> Format.eprintf "WARNING: Ignored argument %s.@." s)
+ usage_msg
+
+let get_value_ref state r =
+ match JsInterpreter.ref_get_value
+ state (JsCommon.execution_ctx_initial false)
+ (JsSyntax.Coq_resvalue_ref r) with
+ | JsInterpreterMonads.Coq_result_some (JsSyntax.Coq_specret_val (_, v)) ->
+ Some v
+ | _ -> None
+
+let get_global_value state name =
+ let r =
+ JsCommon.ref_create_env_loc
+ JsSyntax.env_loc_global_env_record
+ name true in
+ get_value_ref state r
+
+let pr_test state =
+ if not !noParasite then
+ match get_global_value state "__$ERROR__" with
+ | Some v ->
+ print_endline ("\nA variable [__$ERROR__] is defined at global scope. Its value is:\n\t"
+ ^ Prheap.prvalue v ^ "\n") ;
+ if !test then exit 1
+ | None ->
+ if not !test then
+ print_endline "No variable [__$ERROR__] is defined at global scope.\n"
+
+let handle_result result =
+ let exit_if_test _ = if !test then exit 1 in
+ match result with
+ | JsInterpreterMonads.Coq_result_some (JsSyntax.Coq_specret_val (_, _)) ->
+ print_endline "\n\nA `nothing' object has been created.\n" ;
+ print_endline "\n\nFIXME: this should be impossible!\n" ;
+ exit_if_test ()
+ | JsInterpreterMonads.Coq_result_some (JsSyntax.Coq_specret_out o) ->
+ begin
+ match o with
+ | JsSyntax.Coq_out_ter (state, res) ->
+ begin
+ if !printHeap then
+ print_endline (Prheap.prstate !skipInit state);
+ match JsSyntax.res_type res with
+ | JsSyntax.Coq_restype_normal ->
+ if not !test then
+ begin
+ match JsSyntax.res_value res with
+ | JsSyntax.Coq_resvalue_value v ->
+ print_endline "\n\nResult:\n";
+ print_endline (Prheap.prvalue v)
+ | JsSyntax.Coq_resvalue_ref re ->
+ print_endline
+ ("\n\nResult is a reference of name " ^ (* I’ve added this relatively ugly part to get more precision from the result. -- Martin *)
+ Prheap.string_of_char_list re.JsSyntax.ref_name ^
+ if !noParasite then "" else (
+ " and of value:\n\t" ^
+ (match get_value_ref state re with
+ | Some v -> Prheap.prvalue v
+ | None -> "Unknown!")) ^ "\n")
+ | JsSyntax.Coq_resvalue_empty ->
+ print_endline "\n\nNo result\n"
+ end;
+ pr_test state
+ | JsSyntax.Coq_restype_break ->
+ print_endline "\n\nBREAK\n" ; exit_if_test ()
+ | JsSyntax.Coq_restype_continue ->
+ print_endline "\n\nCONTINUE\n" ; exit_if_test ()
+ | JsSyntax.Coq_restype_return ->
+ print_endline "\n\nRETURN\n" ; exit_if_test ()
+ | JsSyntax.Coq_restype_throw ->
+ print_endline "\n\nEXCEPTION THROWN\n" ;
+ (match JsSyntax.res_value res with
+ | JsSyntax.Coq_resvalue_value v ->
+ print_endline ("\tReturned value:\t" ^ Prheap.prvalue v) ;
+ (match v with
+ | JsSyntax.Coq_value_prim _ -> ()
+ | JsSyntax.Coq_value_object l ->
+ print_newline () ;
+ let r = {
+ JsSyntax.ref_base = JsSyntax.Coq_ref_base_type_value v ;
+ JsSyntax.ref_name = "__$ERROR__" ;
+ JsSyntax.ref_strict = false } in
+ if not !noParasite then
+ match get_value_ref state r with
+ | Some v' ->
+ print_endline ("Fetching the `__$ERROR__' field of this returned object resulted to:\t" ^ Prheap.prvalue v')
+ | None ->
+ print_endline "No `__$ERROR__' field has been defined in this returned object.")
+ | JsSyntax.Coq_resvalue_ref _ ->
+ print_endline "With a reference."
+ | JsSyntax.Coq_resvalue_empty ->
+ print_endline "No result with this throw.") ;
+ pr_test state ; exit_if_test ()
+ end
+ | JsSyntax.Coq_out_div ->
+ print_endline "\n\nDIV\n" ; exit_if_test ()
+ end;
+ | JsInterpreterMonads.Coq_result_impossible ->
+ print_endline "\n\nFIXME: this should be impossible!\n" ; exit_if_test ()
+ | JsInterpreterMonads.Coq_result_not_yet_implemented ->
+ print_endline "\n\nNYI: this has not yet been implemented in Coq!\n" ; exit 2
+ | JsInterpreterMonads.Coq_result_bottom s ->
+ print_endline ("\n\nBOTTOM\nCurrent state:\n" ^ Prheap.prstate !skipInit s)
+
+let run_prog_with_state state prog =
+ let ctx = JsCommon.execution_ctx_initial (JsSyntaxAux.prog_intro_strictness prog) in
+ (JsInterpreterMonads.if_void
+ (JsInterpreter.execution_ctx_binding_inst state ctx JsSyntax.Coq_codetype_global None prog [])
+ (fun s' -> JsInterpreter.run_prog s' ctx prog))
+
+let run_prog_incremental prog_res prog =
+ match prog_res with
+ | JsInterpreterMonads.Coq_result_some (JsSyntax.Coq_specret_out o) ->
+ begin
+ match o with
+ | JsSyntax.Coq_out_ter (state, res) ->
+ begin
+ match JsSyntax.res_type res with
+ | JsSyntax.Coq_restype_normal ->
+ (run_prog_with_state state prog)
+ | _ -> raise (AbnormalPreludeTermination prog_res) (* to print out a sensible error *)
+ end
+ | _ -> raise (AbnormalPreludeTermination prog_res) (* to print out a sensible error *)
+ end
+ | _ -> raise (AbnormalPreludeTermination prog_res) (* to print out a sensible error *)
+
+let _ =
+ arguments ();
+ Parser_main.init ?path:!parser_path ();
+ let exit_if_test _ = if !test then exit 1 in
+ try
+ let prog = Translate_syntax.parse_js_syntax_from_file !strictMode !file in
+ let JsSyntax.Coq_prog_intro (str, el) = prog in
+ let str' = !strictMode || str in
+ let prog' = JsSyntax.Coq_prog_intro (str', el) in
+ let exp_prelude = begin
+ let els = List.concat (List.map (fun f ->
+ let JsSyntax.Coq_prog_intro (_, el0) =
+ Translate_syntax.parse_js_syntax_from_file str' f in
+ el0) !test_prelude) in
+ JsSyntax.Coq_prog_intro (str', els)
+ end in
+ let prelude_res = JsInterpreter.run_javascript exp_prelude in
+ handle_result (run_prog_incremental prelude_res prog')
+ with
+ | AbnormalPreludeTermination res ->
+ handle_result res;
+ exit 2
+ | Assert_failure (file, line, col) ->
+ print_string (
+ "\nNot implemented code in file `" ^ file ^ "', line " ^
+ string_of_int line ^ " and column " ^ string_of_int col) ;
+ exit 2
+ | Translate_syntax.CoqSyntaxDoesNotSupport s ->
+ print_string
+ ("\nTranslation of Javascript syntax does not support `" ^ s ^ "' yet.") ;
+ exit 2
+ | Parser.ParserFailure file ->
+ print_string ("\nParsing problem with the file `" ^ file ^ "'.") ;
+ exit_if_test ()
+
diff --git a/jsref/run_js.mli b/jsref/run_js.mli
new file mode 100644
index 0000000..e69de29
diff --git a/opam b/opam
index 83cb116..686acf9 100644
--- a/opam
+++ b/opam
@@ -1,16 +1,22 @@
opam-version: "1.2"
-name: "jsjsref"
+name: "jsjsref-generator"
version: "1.0~dev"
maintainer: "Thomas Wood <thomas.wood09@imperial.ac.uk>"
-authors: ["Arthur Charguéraud <arthur@chargueraud.org>"
- "Alan Schmitt <alan.schmitt@inria.fr"
- "Thomas Wood <thomas.wood09@imperial.ac.uk>"]
+authors: [
+ "Arthur Charguéraud <arthur@chargueraud.org>"
+ "Alan Schmitt <alan.schmitt@inria.fr"
+ "Thomas Wood <thomas.wood09@imperial.ac.uk>"
+]
homepage: "http://jscert.org/"
+bug-reports: "https://github.com/jscert/jsexplain/issues"
license: "BSD 3-clause"
-available: [ocaml-version >= "4.03.0" && ocaml-version < "4.04"]
+dev-repo: "https://github.com/jscert/jsexplain.git"
+
+available: [ocaml-version >= "4.03.0" & ocaml-version < "4.04"]
build: [
[make]
]
depends: [
"ocamlfind" {build}
+ "JS_Parser" { >= "0.1" & < "0.2" }
]
--
GitLab