From 0a0b0c9a74e94e9eb95becb809919974a948fbf5 Mon Sep 17 00:00:00 2001
From: charguer <arthur@chargueraud.org>
Date: Tue, 10 May 2016 16:58:32 +0200
Subject: [PATCH] heaps_as_maps
---
driver.html | 3 +
generator/.gitignore | 2 +
generator/Makefile | 7 +-
generator/TODO | 19 +-
generator/stdlib_ml/stdlib.js | 4 +
generator/stdlib_ml/stdlib.mli | 6 +-
generator/tests/jsref/Heap.ml | 75 ++---
generator/tests/jsref/HeapInt.ml | 22 ++
generator/tests/jsref/HeapList.ml | 61 ++++
generator/tests/jsref/HeapObj.ml | 23 ++
generator/tests/jsref/HeapStr.ml | 22 ++
generator/tests/jsref/JsCommon.ml | 12 +-
generator/tests/jsref/JsCommonAux.ml | 8 +-
generator/tests/jsref/JsInit.ml | 160 +++++------
generator/tests/jsref/JsInterpreter.ml | 44 +--
generator/tests/jsref/JsSyntax.ml | 6 +-
generator/tests/jsref/JsSyntaxAux.ml | 104 +++++++
generator/tests/jsref/StdMap.ml | 382 +++++++++++++++++++++++++
navig-driver.js | 19 +-
19 files changed, 801 insertions(+), 178 deletions(-)
create mode 100644 generator/tests/jsref/HeapInt.ml
create mode 100644 generator/tests/jsref/HeapList.ml
create mode 100644 generator/tests/jsref/HeapObj.ml
create mode 100644 generator/tests/jsref/HeapStr.ml
create mode 100644 generator/tests/jsref/StdMap.ml
diff --git a/driver.html b/driver.html
index 763fd08..ffdf4ce 100644
--- a/driver.html
+++ b/driver.html
@@ -151,6 +151,9 @@ Navigation:
<input type="button" id='button_reach_condition' value="Reach" />
<input type="button" id='button_test_condition' value="Test" />
<span id="reach_output"></span>
+<font style="size: 50%">
+Using: S('x'), S_raw('x'), S_line(), I('x'), I_line().
+</font>
</div>
</div>
diff --git a/generator/.gitignore b/generator/.gitignore
index d106041..da1bae8 100644
--- a/generator/.gitignore
+++ b/generator/.gitignore
@@ -2,6 +2,8 @@
*.log.js
*.unlog.js
*.token.js
+*.pseudo.js
+*.ptoken.js
*.mlloc.js
*.pre
tests/jsref/assembly.js
diff --git a/generator/Makefile b/generator/Makefile
index d496ebe..98b2d4e 100644
--- a/generator/Makefile
+++ b/generator/Makefile
@@ -34,13 +34,18 @@ ASSEMBLY_JS_FILES := \
LibList.unlog.js \
LibOption.unlog.js \
LibProd.unlog.js \
+ StdMap.unlog.js \
Heap.unlog.js \
+ HeapInt.unlog.js \
+ HeapStr.unlog.js \
+ HeapList.unlog.js \
Shared.unlog.js \
Compare.js \
Debug.js \
JsNumber.js \
JsSyntax.unlog.js \
JsSyntaxAux.unlog.js \
+ HeapObj.unlog.js \
Translate_syntax.js \
JsCommon.unlog.js \
JsCommonAux.unlog.js \
@@ -50,7 +55,7 @@ ASSEMBLY_JS_FILES := \
JsInterpreter.log.js
ASSEMBLY_JS := $(STDLIB_DIR)/stdlib.js $(addprefix tests/jsref/,$(ASSEMBLY_JS_FILES))
-# StdMap.unlog.js \
+#
###############################################################
diff --git a/generator/TODO b/generator/TODO
index ab0b734..af0e87a 100644
--- a/generator/TODO
+++ b/generator/TODO
@@ -1,4 +1,21 @@
- let%if_spec (s,x) = expr in cont
+
+
+inline let object_loc_comparable x y =
+ et al
+-----
+
+ Coq_out_ter (s1,x) ---> x
+
+ res_ref r --> r
+ res_val v --> v
+ res_normal rv --> rv
+
+----
+
+
+
+
+let%if_spec (s,x) = expr in cont
becomes
if_spec expr (fun s x -> cont)
diff --git a/generator/stdlib_ml/stdlib.js b/generator/stdlib_ml/stdlib.js
index 7ed3bf1..dd02314 100644
--- a/generator/stdlib_ml/stdlib.js
+++ b/generator/stdlib_ml/stdlib.js
@@ -58,7 +58,11 @@ val ( >= ) : float -> float -> bool
var nat_eq = function(x, y) { return x === y; };
var int_eq = function(x, y) { return x === y; };
+var int_lt = function(x, y) { return x < y; };
+var int_gt = function(x, y) { return x > y; };
+var int_le = function(x, y) { return x <= y; };
var int_ge = function(x, y) { return x >= y; };
+var int_compare = function(x, y) { return x - y; };
//----------------------------------------------------------------------------
diff --git a/generator/stdlib_ml/stdlib.mli b/generator/stdlib_ml/stdlib.mli
index c467630..c2914af 100644
--- a/generator/stdlib_ml/stdlib.mli
+++ b/generator/stdlib_ml/stdlib.mli
@@ -17,8 +17,12 @@ val ( / ) : int -> int -> int
val nat_eq : int -> int -> bool (* nat_eq x y = int_eq x y *)
val int_eq : int -> int -> bool
+val int_lt : int -> int -> bool
+val int_gt : int -> int -> bool
+val int_le : int -> int -> bool
val int_ge : int -> int -> bool
(* val int_lt : int -> int -> bool*)
+val int_compare : int -> int -> int
(*--------------------*)
(* float operations *)
@@ -125,7 +129,7 @@ val ( || ) : bool -> bool -> bool (* beware of strict vs lazy semantics: todo d
(* todo : factorize and clean up *)
val string_eq : string -> string -> bool (* === *)
-val string_compare : string -> string -> float (* actually returns an int *)
+val string_compare : string -> string -> int
(*
val string_concat : string -> string -> string (* + *)
diff --git a/generator/tests/jsref/Heap.ml b/generator/tests/jsref/Heap.ml
index 20b4a47..36d1323 100644
--- a/generator/tests/jsref/Heap.ml
+++ b/generator/tests/jsref/Heap.ml
@@ -1,76 +1,47 @@
open Datatypes
-open LibList
-open LibReflect
+type ('k, 'v) t = ('k, 'v) StdMap.t
-type ('k, 'v) heap = ('k * 'v) list
+type ('k, 'v) heap = ('k, 'v) t
-(** val empty : ('a1, 'a2) heap **)
-
-let empty =
- []
+(* type 'a1 comparison = 'a -> 'a -> int *)
-(** val assoc : 'a1 coq_Comparable -> 'a1 -> ('a1 * 'a2) list -> 'a2 **)
+(** val empty : ('a1, 'a2) heap **)
-let rec assoc h1 k l = match l with
-| [] -> raise Not_found
-| p :: l' -> let (x, v) = p in if h1 x k then v else assoc h1 k l'
+let empty =
+ StdMap.empty
-(** val read : 'a1 coq_Comparable -> ('a1, 'a2) heap -> 'a1 -> 'a2 **)
+(** val read : 'a1 comparison -> ('a1 * 'a2) list -> 'a1 -> 'a2 **)
-let read h l k =
- assoc h k l
+let read h l k =
+ StdMap.find h k l
-(** val write : ('a1, 'a2) heap -> 'a1 -> 'a2 -> ('a1 * 'a2) list **)
+(** val write : 'a1 comparison -> ('a1, 'a2) heap -> 'a1 -> 'a2 -> ('a1 * 'a2) list **)
-let write l k v =
- (k, v) :: l
+let write h l k v =
+ StdMap.add h k v l
(** val rem :
- 'a1 coq_Comparable -> ('a1, 'a2) heap -> 'a1 -> ('a1 * 'a2) list **)
+ 'a1 comparison -> ('a1, 'a2) heap -> 'a1 -> ('a1 * 'a2) list **)
-let rem h1 l k =
- filter (fun p -> if h1 (fst p) k then false else true) l
+let rem h l k =
+ StdMap.remove h k l
(** val read_option :
- 'a1 coq_Comparable -> ('a1, 'a2) heap -> 'a1 -> 'a2 option **)
+ 'a1 comparison -> ('a1, 'a2) heap -> 'a1 -> 'a2 option **)
let read_option h l k =
- let rec read_option0 l k =
- match l with
- | [] -> None
- | p :: l' ->
- let (x, v) = p in if h x k then Some v else read_option0 l' k
- in read_option0 l k
-
-(** val mem_assoc :
- 'a2 coq_Comparable -> 'a2 -> ('a2 * 'a1) list -> bool **)
-
-let rec mem_assoc h1 k l = match l with
-| [] -> false
-| p :: l' -> let (x, y) = p in (h1 x k) || (mem_assoc h1 k l')
+ StdMap.find_option h k l
(** val indom_dec :
- 'a1 coq_Comparable -> ('a1, 'a2) heap -> 'a1 -> bool **)
-
-let indom_dec h1 h k =
- mem_assoc h1 k h
-
-(** val indom_decidable :
- 'a1 coq_Comparable -> ('a1, 'a2) heap -> 'a1 -> coq_Decidable **)
-
-let indom_decidable h h0 k =
- indom_dec h h0 k
-
-
-(** val to_list : ('a1, 'a2) heap -> ('a1, 'a2) heap **)
+ 'a1 comparison -> ('a1, 'a2) heap -> 'a1 -> bool **)
-(* MODIFIED TO REMOVE DUPLICATE KEYS --- warning: quadratic complexity *)
-let rec to_list eq l =
- match l with
- | [] -> []
- | p :: l' -> p :: (to_list eq (rem eq l' (fst p)))
+let indom_dec h l k =
+ StdMap.mem h k l
+(** val to_list : 'a1 comparison -> ('a1, 'a2) heap -> ('a1 * 'a2) list **)
+let to_list h l =
+ StdMap.fold (fun k v acc -> (k,v)::acc) l []
diff --git a/generator/tests/jsref/HeapInt.ml b/generator/tests/jsref/HeapInt.ml
new file mode 100644
index 0000000..8b616c0
--- /dev/null
+++ b/generator/tests/jsref/HeapInt.ml
@@ -0,0 +1,22 @@
+
+let empty =
+ Heap.empty
+
+let read l k =
+ Heap.read int_compare l k
+
+let write l k v =
+ Heap.write int_compare l k v
+
+let rem l k =
+ Heap.rem int_compare l k
+
+let read_option l k =
+ Heap.read_option int_compare l k
+
+let indom_dec l k =
+ Heap.indom_dec int_compare l k
+
+let to_list l =
+ Heap.to_list int_compare l
+
diff --git a/generator/tests/jsref/HeapList.ml b/generator/tests/jsref/HeapList.ml
new file mode 100644
index 0000000..4382081
--- /dev/null
+++ b/generator/tests/jsref/HeapList.ml
@@ -0,0 +1,61 @@
+(* DEPRECATED: currently not used, but keep around as a possible replacement for StdMap *)
+
+
+open Datatypes
+open LibList
+
+(* type 'a1 comparison = 'a -> 'a -> int *)
+
+type ('k, 'v) heap = ('k * 'v) list
+
+(** val empty : ('a1, 'a2) heap **)
+
+let empty =
+ []
+
+
+(** val read : 'a1 comparison -> ('a1 * 'a2) list -> 'a1 -> 'a2 **)
+
+let rec read h l k = match l with
+| [] -> raise Not_found
+| p :: l' -> let (x, v) = p in if int_eq (h x k) 0 then v else read h l' k
+
+(** val write : 'a1 comparison -> ('a1, 'a2) heap -> 'a1 -> 'a2 -> ('a1 * 'a2) list **)
+
+let write h l k v =
+ (k, v) :: l
+
+(** val rem :
+ 'a1 comparison -> ('a1, 'a2) heap -> 'a1 -> ('a1 * 'a2) list **)
+
+let rem h1 l k =
+ filter (fun p -> if int_eq (h1 (fst p) k) 0 then false else true) l
+
+(** val read_option :
+ 'a1 comparison -> ('a1, 'a2) heap -> 'a1 -> 'a2 option **)
+
+let read_option h l k =
+ let rec read_option0 l k =
+ match l with
+ | [] -> None
+ | p :: l' ->
+ let (x, v) = p in if int_eq (h x k) 0 then Some v else read_option0 l' k
+ in read_option0 l k
+
+(** val indom_dec :
+ 'a1 comparison -> ('a1, 'a2) heap -> 'a1 -> bool **)
+
+let rec indom_dec h1 l k = match l with
+| [] -> false
+| p :: l' -> let (x, y) = p in int_eq (h1 x k) 0 || (indom_dec h1 l' k)
+
+(** val to_list : 'a1 comparison -> ('a1, 'a2) heap -> ('a1, 'a2) heap **)
+
+(* MODIFIED TO REMOVE DUPLICATE KEYS --- warning: quadratic complexity *)
+let rec to_list h l =
+ match l with
+ | [] -> []
+ | p :: l' -> p :: (to_list h (rem h l' (fst p)))
+
+
+
diff --git a/generator/tests/jsref/HeapObj.ml b/generator/tests/jsref/HeapObj.ml
new file mode 100644
index 0000000..82bea71
--- /dev/null
+++ b/generator/tests/jsref/HeapObj.ml
@@ -0,0 +1,23 @@
+
+
+let empty =
+ Heap.empty
+
+let read l k =
+ Heap.read JsSyntaxAux.object_loc_cmp l k
+
+let write l k v =
+ Heap.write JsSyntaxAux.object_loc_cmp l k v
+
+let rem l k =
+ Heap.rem JsSyntaxAux.object_loc_cmp l k
+
+let read_option l k =
+ Heap.read_option JsSyntaxAux.object_loc_cmp l k
+
+let indom_dec l k =
+ Heap.indom_dec JsSyntaxAux.object_loc_cmp l k
+
+let to_list l =
+ Heap.to_list JsSyntaxAux.object_loc_cmp l
+
diff --git a/generator/tests/jsref/HeapStr.ml b/generator/tests/jsref/HeapStr.ml
new file mode 100644
index 0000000..c59b2ea
--- /dev/null
+++ b/generator/tests/jsref/HeapStr.ml
@@ -0,0 +1,22 @@
+
+let empty =
+ Heap.empty
+
+let read l k =
+ Heap.read string_compare l k
+
+let write l k v =
+ Heap.write string_compare l k v
+
+let rem l k =
+ Heap.rem string_compare l k
+
+let read_option l k =
+ Heap.read_option string_compare l k
+
+let indom_dec l k =
+ Heap.indom_dec string_compare l k
+
+let to_list l =
+ Heap.to_list string_compare l
+
diff --git a/generator/tests/jsref/JsCommon.ml b/generator/tests/jsref/JsCommon.ml
index 3c77d5d..7eec4fe 100644
--- a/generator/tests/jsref/JsCommon.ml
+++ b/generator/tests/jsref/JsCommon.ml
@@ -174,7 +174,7 @@ let state_map_object_heap s f =
(* STATEFUL *)
let object_write s l o =
- state_map_object_heap s (fun h -> Heap.write h l o)
+ state_map_object_heap s (fun h -> HeapObj.write h l o)
(** val object_alloc : state -> coq_object -> object_loc * state **)
@@ -301,7 +301,7 @@ let state_map_env_record_heap s f =
(* STATEFUL *)
let env_record_write s l e =
- state_map_env_record_heap s (fun h -> Heap.write h l e)
+ state_map_env_record_heap s (fun h -> HeapInt.write h l e)
(** val env_record_alloc : state -> env_record -> int * state **)
@@ -312,7 +312,7 @@ let env_record_alloc s e =
in
let l = state_fresh_locations0 in
let alloc = state_fresh_locations0 + 1 in
- let bindings' = Heap.write bindings l e in
+ let bindings' = HeapInt.write bindings l e in
(l, { state_object_heap = cells; state_env_record_heap = bindings';
state_fresh_locations = alloc })
@@ -340,20 +340,20 @@ let decl_env_record_empty =
decl_env_record -> prop_name -> mutability -> value -> decl_env_record **)
let decl_env_record_write ed x mu v =
- Heap.write ed x (mu, v)
+ HeapStr.write ed x (mu, v)
(** val decl_env_record_rem :
decl_env_record -> prop_name -> decl_env_record **)
let decl_env_record_rem ed x =
- Heap.rem string_eq ed x
+ HeapStr.rem ed x
(** val env_record_write_decl_env :
state -> env_loc -> prop_name -> mutability -> value -> state **)
(* STATEFUL *)
let env_record_write_decl_env s l x mu v =
- match Heap.read nat_eq s.state_env_record_heap l with
+ match HeapInt.read s.state_env_record_heap l with
| Coq_env_record_decl ed ->
let env' = decl_env_record_write ed x mu v in
env_record_write s l (Coq_env_record_decl env')
diff --git a/generator/tests/jsref/JsCommonAux.ml b/generator/tests/jsref/JsCommonAux.ml
index 4c1a979..e5521e6 100644
--- a/generator/tests/jsref/JsCommonAux.ml
+++ b/generator/tests/jsref/JsCommonAux.ml
@@ -196,20 +196,20 @@ let ref_kind_comparable x y =
(* STATEFUL-RO *)
let object_binds_pickable_option s l =
- Heap.read_option object_loc_comparable s.state_object_heap l
+ HeapObj.read_option s.state_object_heap l
(** val env_record_binds_pickable_option :
state -> env_loc -> env_record coq_Pickable_option **)
(* STATEFUL-RO *)
let env_record_binds_pickable_option s l =
- Heap.read_option nat_eq s.state_env_record_heap l
+ HeapInt.read_option s.state_env_record_heap l
(** val decl_env_record_pickable_option :
decl_env_record -> prop_name -> (mutability * value) coq_Pickable_option **)
let decl_env_record_pickable_option ed x =
- Heap.read_option string_eq ed x
+ HeapStr.read_option ed x
(** val descriptor_is_data_dec : descriptor -> bool **)
@@ -398,6 +398,6 @@ let is_callable_dec s v =
(* STATEFUL-RO *)
let object_properties_keys_as_list_pickable_option s l =
- map (fun props -> LibList.map fst (Heap.to_list string_eq props))
+ map (fun props -> LibList.map fst (HeapStr.to_list props))
(map object_properties_ (object_binds_pickable_option s l))
diff --git a/generator/tests/jsref/JsInit.ml b/generator/tests/jsref/JsInit.ml
index 58a86eb..1ae7c58 100644
--- a/generator/tests/jsref/JsInit.ml
+++ b/generator/tests/jsref/JsInit.ml
@@ -50,7 +50,7 @@ let object_create_builtin vproto sclass p =
let object_create_prealloc_call_or_construct length p =
let sclass = "Function" in
let p' =
- Heap.write p ("length")
+ HeapStr.write p ("length")
(Coq_attributes_data_of (attrib_constant length))
in
object_create_builtin (Coq_value_object (Coq_object_loc_prealloc
@@ -76,7 +76,7 @@ let object_create_prealloc_constructor fprealloc length p =
Heap.heap **)
let write_native p name v =
- Heap.write p name (Coq_attributes_data_of
+ HeapStr.write p name (Coq_attributes_data_of
(prop_attributes_for_global_object v))
(** val write_constant :
@@ -84,7 +84,7 @@ let write_native p name v =
Heap.heap **)
let write_constant p name value0 =
- Heap.write p name (Coq_attributes_data_of (attrib_constant value0))
+ HeapStr.write p name (Coq_attributes_data_of (attrib_constant value0))
(** val object_prealloc_global_proto : value **)
@@ -554,7 +554,7 @@ let object_prealloc_function_proto =
(Coq_value_object (Coq_object_loc_prealloc Coq_prealloc_function))
in
let p0 =
- Heap.write p ("length")
+ HeapStr.write p ("length")
(Coq_attributes_data_of
(attrib_constant (Coq_value_prim (Coq_prim_number
0.0))))
@@ -987,43 +987,43 @@ let throw_type_error_object =
let object_heap_initial_function_objects_1 h =
let h0 =
- Heap.write h (Coq_object_loc_prealloc Coq_prealloc_throw_type_error)
+ HeapObj.write h (Coq_object_loc_prealloc Coq_prealloc_throw_type_error)
throw_type_error_object
in
let h1 =
- Heap.write h0 (Coq_object_loc_prealloc Coq_prealloc_global_eval)
+ HeapObj.write h0 (Coq_object_loc_prealloc Coq_prealloc_global_eval)
global_eval_function_object
in
let h2 =
- Heap.write h1 (Coq_object_loc_prealloc Coq_prealloc_global_parse_int)
+ HeapObj.write h1 (Coq_object_loc_prealloc Coq_prealloc_global_parse_int)
global_parse_int_function_object
in
let h3 =
- Heap.write h2 (Coq_object_loc_prealloc Coq_prealloc_global_parse_float)
+ HeapObj.write h2 (Coq_object_loc_prealloc Coq_prealloc_global_parse_float)
global_parse_float_function_object
in
let h4 =
- Heap.write h3 (Coq_object_loc_prealloc Coq_prealloc_global_is_nan)
+ HeapObj.write h3 (Coq_object_loc_prealloc Coq_prealloc_global_is_nan)
global_is_nan_function_object
in
let h5 =
- Heap.write h4 (Coq_object_loc_prealloc Coq_prealloc_global_is_finite)
+ HeapObj.write h4 (Coq_object_loc_prealloc Coq_prealloc_global_is_finite)
global_is_finite_function_object
in
let h6 =
- Heap.write h5 (Coq_object_loc_prealloc Coq_prealloc_global_decode_uri)
+ HeapObj.write h5 (Coq_object_loc_prealloc Coq_prealloc_global_decode_uri)
global_decode_uri_function_object
in
let h7 =
- Heap.write h6 (Coq_object_loc_prealloc
+ HeapObj.write h6 (Coq_object_loc_prealloc
Coq_prealloc_global_decode_uri_component)
global_decode_uri_component_function_object
in
let h8 =
- Heap.write h7 (Coq_object_loc_prealloc Coq_prealloc_global_encode_uri)
+ HeapObj.write h7 (Coq_object_loc_prealloc Coq_prealloc_global_encode_uri)
global_encode_uri_function_object
in
- Heap.write h8 (Coq_object_loc_prealloc
+ HeapObj.write h8 (Coq_object_loc_prealloc
Coq_prealloc_global_encode_uri_component)
global_encode_uri_component_function_object
@@ -1033,53 +1033,53 @@ let object_heap_initial_function_objects_1 h =
let object_heap_initial_function_objects_2 h =
let h0 = object_heap_initial_function_objects_1 h in
let h1 =
- Heap.write h0 (Coq_object_loc_prealloc Coq_prealloc_object_get_proto_of)
+ HeapObj.write h0 (Coq_object_loc_prealloc Coq_prealloc_object_get_proto_of)
object_get_proto_of_function_object
in
let h2 =
- Heap.write h1 (Coq_object_loc_prealloc
+ HeapObj.write h1 (Coq_object_loc_prealloc
Coq_prealloc_object_get_own_prop_descriptor)
object_get_own_prop_descriptor_function_object
in
let h3 =
- Heap.write h2 (Coq_object_loc_prealloc
+ HeapObj.write h2 (Coq_object_loc_prealloc
Coq_prealloc_object_get_own_prop_name)
object_get_own_prop_name_function_object
in
let h4 =
- Heap.write h3 (Coq_object_loc_prealloc Coq_prealloc_object_create)
+ HeapObj.write h3 (Coq_object_loc_prealloc Coq_prealloc_object_create)
object_create_function_object
in
let h5 =
- Heap.write h4 (Coq_object_loc_prealloc Coq_prealloc_object_define_prop)
+ HeapObj.write h4 (Coq_object_loc_prealloc Coq_prealloc_object_define_prop)
object_define_prop_function_object
in
let h6 =
- Heap.write h5 (Coq_object_loc_prealloc Coq_prealloc_object_define_props)
+ HeapObj.write h5 (Coq_object_loc_prealloc Coq_prealloc_object_define_props)
object_define_props_function_object
in
let h7 =
- Heap.write h6 (Coq_object_loc_prealloc Coq_prealloc_object_seal)
+ HeapObj.write h6 (Coq_object_loc_prealloc Coq_prealloc_object_seal)
object_seal_function_object
in
let h8 =
- Heap.write h7 (Coq_object_loc_prealloc Coq_prealloc_object_freeze)
+ HeapObj.write h7 (Coq_object_loc_prealloc Coq_prealloc_object_freeze)
object_freeze_function_object
in
let h9 =
- Heap.write h8 (Coq_object_loc_prealloc
+ HeapObj.write h8 (Coq_object_loc_prealloc
Coq_prealloc_object_prevent_extensions)
object_prevent_extensions_function_object
in
let h10 =
- Heap.write h9 (Coq_object_loc_prealloc Coq_prealloc_object_is_sealed)
+ HeapObj.write h9 (Coq_object_loc_prealloc Coq_prealloc_object_is_sealed)
object_is_sealed_function_object
in
let h11 =
- Heap.write h10 (Coq_object_loc_prealloc Coq_prealloc_object_is_frozen)
+ HeapObj.write h10 (Coq_object_loc_prealloc Coq_prealloc_object_is_frozen)
object_is_frozen_function_object
in
- Heap.write h11 (Coq_object_loc_prealloc Coq_prealloc_object_is_extensible)
+ HeapObj.write h11 (Coq_object_loc_prealloc Coq_prealloc_object_is_extensible)
object_is_extensible_function_object
(** val object_heap_initial_function_objects_3 :
@@ -1088,44 +1088,44 @@ let object_heap_initial_function_objects_2 h =
let object_heap_initial_function_objects_3 h =
let h0 = object_heap_initial_function_objects_2 h in
let h1 =
- Heap.write h0 (Coq_object_loc_prealloc
+ HeapObj.write h0 (Coq_object_loc_prealloc
Coq_prealloc_object_proto_to_string)
object_proto_to_string_function_object
in
let h2 =
- Heap.write h1 (Coq_object_loc_prealloc
+ HeapObj.write h1 (Coq_object_loc_prealloc
Coq_prealloc_object_proto_value_of)
object_proto_value_of_function_object
in
let h3 =
- Heap.write h2 (Coq_object_loc_prealloc
+ HeapObj.write h2 (Coq_object_loc_prealloc
Coq_prealloc_object_proto_has_own_prop)
object_proto_has_own_prop_function_object
in
let h4 =
- Heap.write h3 (Coq_object_loc_prealloc
+ HeapObj.write h3 (Coq_object_loc_prealloc
Coq_prealloc_object_proto_is_prototype_of)
object_proto_is_prototype_of_function_object
in
let h5 =
- Heap.write h4 (Coq_object_loc_prealloc
+ HeapObj.write h4 (Coq_object_loc_prealloc
Coq_prealloc_object_proto_prop_is_enumerable)
object_proto_prop_is_enumerable_function_object
in
let h6 =
- Heap.write h5 (Coq_object_loc_prealloc
+ HeapObj.write h5 (Coq_object_loc_prealloc
Coq_prealloc_function_proto_to_string)
function_proto_to_string_function_object
in
let h7 =
- Heap.write h6 (Coq_object_loc_prealloc Coq_prealloc_function_proto_call)
+ HeapObj.write h6 (Coq_object_loc_prealloc Coq_prealloc_function_proto_call)
function_proto_call_function_object
in
let h8 =
- Heap.write h7 (Coq_object_loc_prealloc Coq_prealloc_function_proto_bind)
+ HeapObj.write h7 (Coq_object_loc_prealloc Coq_prealloc_function_proto_bind)
function_proto_bind_function_object
in
- Heap.write h8 (Coq_object_loc_prealloc Coq_prealloc_function_proto_apply)
+ HeapObj.write h8 (Coq_object_loc_prealloc Coq_prealloc_function_proto_apply)
function_proto_apply_function_object
(** val object_heap_initial_function_objects_4 :
@@ -1134,41 +1134,41 @@ let object_heap_initial_function_objects_3 h =
let object_heap_initial_function_objects_4 h =
let h0 = object_heap_initial_function_objects_3 h in
let h1 =
- Heap.write h0 (Coq_object_loc_prealloc Coq_prealloc_array_is_array)
+ HeapObj.write h0 (Coq_object_loc_prealloc Coq_prealloc_array_is_array)
array_is_array_function_object
in
let h2 =
- Heap.write h1 (Coq_object_loc_prealloc
+ HeapObj.write h1 (Coq_object_loc_prealloc
Coq_prealloc_array_proto_to_string)
array_proto_to_string_function_object
in
let h3 =
- Heap.write h2 (Coq_object_loc_prealloc Coq_prealloc_array_proto_join)
+ HeapObj.write h2 (Coq_object_loc_prealloc Coq_prealloc_array_proto_join)
array_proto_join_function_object
in
let h4 =
- Heap.write h3 (Coq_object_loc_prealloc Coq_prealloc_array_proto_pop)
+ HeapObj.write h3 (Coq_object_loc_prealloc Coq_prealloc_array_proto_pop)
array_proto_pop_function_object
in
let h5 =
- Heap.write h4 (Coq_object_loc_prealloc Coq_prealloc_array_proto_push)
+ HeapObj.write h4 (Coq_object_loc_prealloc Coq_prealloc_array_proto_push)
array_proto_push_function_object
in
let h6 =
- Heap.write h5 (Coq_object_loc_prealloc
+ HeapObj.write h5 (Coq_object_loc_prealloc
Coq_prealloc_string_proto_to_string)
string_proto_to_string_function_object
in
let h7 =
- Heap.write h6 (Coq_object_loc_prealloc
+ HeapObj.write h6 (Coq_object_loc_prealloc
Coq_prealloc_string_proto_value_of)
string_proto_value_of_function_object
in
let h8 =
- Heap.write h7 (Coq_object_loc_prealloc Coq_prealloc_bool_proto_to_string)
+ HeapObj.write h7 (Coq_object_loc_prealloc Coq_prealloc_bool_proto_to_string)
bool_proto_to_string_function_object
in
- Heap.write h8 (Coq_object_loc_prealloc Coq_prealloc_bool_proto_value_of)
+ HeapObj.write h8 (Coq_object_loc_prealloc Coq_prealloc_bool_proto_value_of)
bool_proto_value_of_function_object
(** val object_heap_initial_function_objects :
@@ -1177,155 +1177,155 @@ let object_heap_initial_function_objects_4 h =
let object_heap_initial_function_objects h =
let h0 = object_heap_initial_function_objects_4 h in
let h1 =
- Heap.write h0 (Coq_object_loc_prealloc
+ HeapObj.write h0 (Coq_object_loc_prealloc
Coq_prealloc_number_proto_to_string)
number_proto_to_string_function_object
in
let h2 =
- Heap.write h1 (Coq_object_loc_prealloc
+ HeapObj.write h1 (Coq_object_loc_prealloc
Coq_prealloc_number_proto_value_of)
number_proto_value_of_function_object
in
- Heap.write h2 (Coq_object_loc_prealloc Coq_prealloc_error_proto_to_string)
+ HeapObj.write h2 (Coq_object_loc_prealloc Coq_prealloc_error_proto_to_string)
error_proto_to_string_function_object
-(** val object_heap_initial : (object_loc, coq_object) Heap.heap **)
+(** val object_heap_initial : (object_loc, coq_object) HeapObj.heap **)
let object_heap_initial =
let h =
- Heap.write Heap.empty (Coq_object_loc_prealloc Coq_prealloc_global)
+ HeapObj.write Heap.empty (Coq_object_loc_prealloc Coq_prealloc_global)
object_prealloc_global
in
let h0 =
- Heap.write h (Coq_object_loc_prealloc Coq_prealloc_object)
+ HeapObj.write h (Coq_object_loc_prealloc Coq_prealloc_object)
object_prealloc_object
in
let h1 =
- Heap.write h0 (Coq_object_loc_prealloc Coq_prealloc_object_proto)
+ HeapObj.write h0 (Coq_object_loc_prealloc Coq_prealloc_object_proto)
object_prealloc_object_proto
in
let h2 =
- Heap.write h1 (Coq_object_loc_prealloc Coq_prealloc_bool)
+ HeapObj.write h1 (Coq_object_loc_prealloc Coq_prealloc_bool)
object_prealloc_bool
in
let h3 =
- Heap.write h2 (Coq_object_loc_prealloc Coq_prealloc_bool_proto)
+ HeapObj.write h2 (Coq_object_loc_prealloc Coq_prealloc_bool_proto)
object_prealloc_bool_proto
in
let h4 =
- Heap.write h3 (Coq_object_loc_prealloc Coq_prealloc_number)
+ HeapObj.write h3 (Coq_object_loc_prealloc Coq_prealloc_number)
object_prealloc_number
in
let h5 =
- Heap.write h4 (Coq_object_loc_prealloc Coq_prealloc_number_proto)
+ HeapObj.write h4 (Coq_object_loc_prealloc Coq_prealloc_number_proto)
object_prealloc_number_proto
in
let h6 =
- Heap.write h5 (Coq_object_loc_prealloc Coq_prealloc_function)
+ HeapObj.write h5 (Coq_object_loc_prealloc Coq_prealloc_function)
object_prealloc_function
in
let h7 =
- Heap.write h6 (Coq_object_loc_prealloc Coq_prealloc_function_proto)
+ HeapObj.write h6 (Coq_object_loc_prealloc Coq_prealloc_function_proto)
object_prealloc_function_proto
in
let h8 =
- Heap.write h7 (Coq_object_loc_prealloc Coq_prealloc_array)
+ HeapObj.write h7 (Coq_object_loc_prealloc Coq_prealloc_array)
object_prealloc_array
in
let h9 =
- Heap.write h8 (Coq_object_loc_prealloc Coq_prealloc_array_proto)
+ HeapObj.write h8 (Coq_object_loc_prealloc Coq_prealloc_array_proto)
object_prealloc_array_proto
in
let h10 =
- Heap.write h9 (Coq_object_loc_prealloc Coq_prealloc_string)
+ HeapObj.write h9 (Coq_object_loc_prealloc Coq_prealloc_string)
object_prealloc_string
in
let h11 =
- Heap.write h10 (Coq_object_loc_prealloc Coq_prealloc_string_proto)
+ HeapObj.write h10 (Coq_object_loc_prealloc Coq_prealloc_string_proto)
object_prealloc_string_proto
in
let h12 =
- Heap.write h11 (Coq_object_loc_prealloc Coq_prealloc_math)
+ HeapObj.write h11 (Coq_object_loc_prealloc Coq_prealloc_math)
object_prealloc_math
in
let h13 =
- Heap.write h12 (Coq_object_loc_prealloc Coq_prealloc_date)
+ HeapObj.write h12 (Coq_object_loc_prealloc Coq_prealloc_date)
object_prealloc_date
in
let h14 =
- Heap.write h13 (Coq_object_loc_prealloc Coq_prealloc_regexp)
+ HeapObj.write h13 (Coq_object_loc_prealloc Coq_prealloc_regexp)
object_prealloc_regexp
in
let h15 =
- Heap.write h14 (Coq_object_loc_prealloc Coq_prealloc_error_proto)
+ HeapObj.write h14 (Coq_object_loc_prealloc Coq_prealloc_error_proto)
object_prealloc_error_proto
in
let h16 =
- Heap.write h15 (Coq_object_loc_prealloc (Coq_prealloc_native_error_proto
+ HeapObj.write h15 (Coq_object_loc_prealloc (Coq_prealloc_native_error_proto
Coq_native_error_eval))
(object_prealloc_native_error_proto Coq_native_error_eval)
in
let h17 =
- Heap.write h16 (Coq_object_loc_prealloc (Coq_prealloc_native_error_proto
+ HeapObj.write h16 (Coq_object_loc_prealloc (Coq_prealloc_native_error_proto
Coq_native_error_range))
(object_prealloc_native_error_proto Coq_native_error_range)
in
let h18 =
- Heap.write h17 (Coq_object_loc_prealloc (Coq_prealloc_native_error_proto
+ HeapObj.write h17 (Coq_object_loc_prealloc (Coq_prealloc_native_error_proto
Coq_native_error_ref))
(object_prealloc_native_error_proto Coq_native_error_ref)
in
let h19 =
- Heap.write h18 (Coq_object_loc_prealloc (Coq_prealloc_native_error_proto
+ HeapObj.write h18 (Coq_object_loc_prealloc (Coq_prealloc_native_error_proto
Coq_native_error_syntax))
(object_prealloc_native_error_proto Coq_native_error_syntax)
in
let h20 =
- Heap.write h19 (Coq_object_loc_prealloc (Coq_prealloc_native_error_proto
+ HeapObj.write h19 (Coq_object_loc_prealloc (Coq_prealloc_native_error_proto
Coq_native_error_type))
(object_prealloc_native_error_proto Coq_native_error_type)
in
let h21 =
- Heap.write h20 (Coq_object_loc_prealloc (Coq_prealloc_native_error_proto
+ HeapObj.write h20 (Coq_object_loc_prealloc (Coq_prealloc_native_error_proto
Coq_native_error_uri))
(object_prealloc_native_error_proto Coq_native_error_uri)
in
let h22 =
- Heap.write h21 (Coq_object_loc_prealloc Coq_prealloc_error)
+ HeapObj.write h21 (Coq_object_loc_prealloc Coq_prealloc_error)
object_prealloc_error
in
let h23 =
- Heap.write h22 (Coq_object_loc_prealloc (Coq_prealloc_native_error
+ HeapObj.write h22 (Coq_object_loc_prealloc (Coq_prealloc_native_error
Coq_native_error_eval))
(object_prealloc_native_error Coq_native_error_eval)
in
let h24 =
- Heap.write h23 (Coq_object_loc_prealloc (Coq_prealloc_native_error
+ HeapObj.write h23 (Coq_object_loc_prealloc (Coq_prealloc_native_error
Coq_native_error_range))
(object_prealloc_native_error Coq_native_error_range)
in
let h25 =
- Heap.write h24 (Coq_object_loc_prealloc (Coq_prealloc_native_error
+ HeapObj.write h24 (Coq_object_loc_prealloc (Coq_prealloc_native_error
Coq_native_error_ref))
(object_prealloc_native_error Coq_native_error_ref)
in
let h26 =
- Heap.write h25 (Coq_object_loc_prealloc (Coq_prealloc_native_error
+ HeapObj.write h25 (Coq_object_loc_prealloc (Coq_prealloc_native_error
Coq_native_error_syntax))
(object_prealloc_native_error Coq_native_error_syntax)
in
let h27 =
- Heap.write h26 (Coq_object_loc_prealloc (Coq_prealloc_native_error
+ HeapObj.write h26 (Coq_object_loc_prealloc (Coq_prealloc_native_error
Coq_native_error_type))
(object_prealloc_native_error Coq_native_error_type)
in
let h28 =
- Heap.write h27 (Coq_object_loc_prealloc (Coq_prealloc_native_error
+ HeapObj.write h27 (Coq_object_loc_prealloc (Coq_prealloc_native_error
Coq_native_error_uri))
(object_prealloc_native_error Coq_native_error_uri)
in
let h29 =
- Heap.write h28 (Coq_object_loc_prealloc Coq_prealloc_json)
+ HeapObj.write h28 (Coq_object_loc_prealloc Coq_prealloc_json)
object_prealloc_json
in
object_heap_initial_function_objects h29
@@ -1333,7 +1333,7 @@ let object_heap_initial =
(** val env_record_heap_initial : (env_loc, env_record) Heap.heap **)
let env_record_heap_initial =
- Heap.write Heap.empty env_loc_global_env_record
+ HeapInt.write Heap.empty env_loc_global_env_record
(env_record_object_default (Coq_object_loc_prealloc Coq_prealloc_global))
(** val dummy_fresh_locations : int stream **)
diff --git a/generator/tests/jsref/JsInterpreter.ml b/generator/tests/jsref/JsInterpreter.ml
index c7783f1..7e63443 100644
--- a/generator/tests/jsref/JsInterpreter.ml
+++ b/generator/tests/jsref/JsInterpreter.ml
@@ -584,14 +584,14 @@ and object_define_own_prop s c l x desc throwcont =
else Coq_attributes_accessor_of
(attributes_accessor_of_descriptor desc0)) in
let%some s2 = (object_heap_map_properties_pickable_option s1 l
- (fun p -> Heap.write p x0 a)) in
+ (fun p -> HeapStr.write p x0 a)) in
res_ter s2
(res_val (Coq_value_prim (Coq_prim_bool true)))
else reject s1 throwcont0
| Coq_full_descriptor_some a ->
let object_define_own_prop_write s2 a0 =
let a_2 = attributes_update a0 desc0 in
- let%some s3 = (object_heap_map_properties_pickable_option s2 l (fun p -> Heap.write p x0 a_2)) in
+ let%some s3 = (object_heap_map_properties_pickable_option s2 l (fun p -> HeapStr.write p x0 a_2)) in
res_ter s3 (res_val (Coq_value_prim (Coq_prim_bool true))) in
if descriptor_contains_dec (descriptor_of_attributes a) desc0
then res_ter s1 (res_val (Coq_value_prim (Coq_prim_bool true)))
@@ -607,7 +607,7 @@ and object_define_own_prop s c l x desc throwcont =
| Coq_attributes_accessor_of aa ->
Coq_attributes_data_of (attributes_data_of_attributes_accessor aa)) in
let%some s2 = (object_heap_map_properties_pickable_option
- s1 l (fun p -> Heap.write p x0 a_2)) in
+ s1 l (fun p -> HeapStr.write p x0 a_2)) in
object_define_own_prop_write s2 a_2
else reject s1 throwcont0
else if (attributes_is_data_dec a) && (descriptor_is_data_dec desc0)
@@ -801,7 +801,7 @@ and prim_new_object s _foo_ = match _foo_ with
let%some s_2 = (object_heap_map_properties_pickable_option
s1 l
(fun p ->
- Heap.write p ("length")
+ HeapStr.write p ("length")
(Coq_attributes_data_of
(attributes_data_intro_constant
(Coq_value_prim
@@ -847,7 +847,7 @@ and env_record_has_binding s c l x =
| Coq_env_record_decl ed ->
result_out (Coq_out_ter (s,
(res_val (Coq_value_prim (Coq_prim_bool
- (Heap.indom_decidable string_eq ed x))))))
+ (HeapStr.indom_dec ed x))))))
| Coq_env_record_object (l0, pt) -> object_has_prop s c l0 x
(** val lexical_env_get_identifier_ref :
@@ -877,7 +877,7 @@ and object_delete_default s c l x str =
if attributes_configurable a
then let%some
s_2 = (object_heap_map_properties_pickable_option s1 l (fun p ->
- Heap.rem string_eq p x)) in
+ HeapStr.rem p x)) in
res_ter s_2 (res_val (Coq_value_prim (Coq_prim_bool true)))
else out_error_or_cst s1 str Coq_native_error_type (Coq_value_prim
(Coq_prim_bool false))
@@ -914,7 +914,7 @@ and env_record_delete_binding s c l x =
let%some e = (env_record_binds_pickable_option s l) in
match e with
| Coq_env_record_decl ed ->
- (match Heap.read_option string_eq ed x with
+ (match HeapStr.read_option ed x with
| Some p ->
let (mu, v) = p in
(match mu with
@@ -968,7 +968,7 @@ and env_record_get_binding_value s c l x str =
let%some e = (env_record_binds_pickable_option s l) in
match e with
| Coq_env_record_decl ed ->
- let%some rm = (Heap.read_option string_eq ed x) in
+ let%some rm = (HeapStr.read_option ed x) in
let (mu, v) = rm in
if mutability_comparable mu Coq_mutability_uninitialized_immutable
then out_error_or_cst s str Coq_native_error_ref (Coq_value_prim
@@ -1126,7 +1126,7 @@ and env_record_set_mutable_binding s c l x v str =
let%some e = (env_record_binds_pickable_option s l) in
match e with
| Coq_env_record_decl ed ->
- let%some rm = (Heap.read_option string_eq ed x) in
+ let%some rm = (HeapStr.read_option ed x) in
let (mu, v_old) = rm in
if not (mutability_comparable mu Coq_mutability_immutable)
then res_void (env_record_write_decl_env s l x mu v)
@@ -1202,7 +1202,7 @@ and env_record_create_mutable_binding s c l x deletable_opt =
let%some e = (env_record_binds_pickable_option s l) in
match e with
| Coq_env_record_decl ed ->
- if Heap.indom_decidable string_eq ed x
+ if HeapStr.indom_dec ed x
then (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
s
("Already declared environnment record in [env_record_create_mutable_binding].")
@@ -1240,7 +1240,7 @@ and env_record_create_immutable_binding s l x =
let%some e = (env_record_binds_pickable_option s l) in
match e with
| Coq_env_record_decl ed ->
- if Heap.indom_decidable string_eq ed x
+ if HeapStr.indom_dec ed x
then (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
s
("Already declared environnment record in [env_record_create_immutable_binding].")
@@ -1305,7 +1305,7 @@ and array_args_map_loop s c l args ind =
| [] -> res_void s
| h :: rest ->
let%some s_2 = (object_heap_map_properties_pickable_option s l (fun p ->
- Heap.write p (JsNumber.to_string (of_int ind))
+ HeapStr.write p (JsNumber.to_string (of_int ind))
(Coq_attributes_data_of (attributes_data_intro_all_true h)))) in array_args_map_loop s_2 c l rest (ind +. 1.)
(** val string_of_prealloc : prealloc -> string **)
@@ -1492,7 +1492,7 @@ and run_construct_prealloc s c b args =
let follow = (fun s_3 length0 ->
let%some
s0 = (object_heap_map_properties_pickable_option s_3 l (fun p0 ->
- Heap.write p0 ("length")
+ HeapStr.write p0 ("length")
(Coq_attributes_data_of { attributes_data_value =
(Coq_value_prim (Coq_prim_number (of_int length0)));
attributes_data_writable = true;
@@ -1510,7 +1510,7 @@ and run_construct_prealloc s c b args =
s0 = (object_heap_map_properties_pickable_option s_2 l
(fun p1 ->
- Heap.write p1 ("0") (Coq_attributes_data_of
+ HeapStr.write p1 ("0") (Coq_attributes_data_of
(attributes_data_intro_all_true v)))) in
follow s0 1.0
| Coq_prim_null ->
@@ -1518,7 +1518,7 @@ and run_construct_prealloc s c b args =
s0 = (object_heap_map_properties_pickable_option s_2 l
(fun p1 ->
- Heap.write p1 ("0") (Coq_attributes_data_of
+ HeapStr.write p1 ("0") (Coq_attributes_data_of
(attributes_data_intro_all_true v)))) in
follow s0 1.0
| Coq_prim_bool b0 ->
@@ -1526,7 +1526,7 @@ and run_construct_prealloc s c b args =
s0 = (object_heap_map_properties_pickable_option s_2 l
(fun p1 ->
- Heap.write p1 ("0") (Coq_attributes_data_of
+ HeapStr.write p1 ("0") (Coq_attributes_data_of
(attributes_data_intro_all_true v)))) in
follow s0 1.0
| Coq_prim_number vlen ->
@@ -1541,20 +1541,20 @@ and run_construct_prealloc s c b args =
s1 = (object_heap_map_properties_pickable_option s_2 l
(fun p1 ->
- Heap.write p1 ("0") (Coq_attributes_data_of
+ HeapStr.write p1 ("0") (Coq_attributes_data_of
(attributes_data_intro_all_true v)))) in
follow s1 1.0)
| Coq_value_object o0 ->
let%some
s0 = (object_heap_map_properties_pickable_option s_2 l
(fun p0 ->
- Heap.write p0 ("0") (Coq_attributes_data_of
+ HeapStr.write p0 ("0") (Coq_attributes_data_of
(attributes_data_intro_all_true v)))) in
follow s0 1.0
else let%some
s0 = (object_heap_map_properties_pickable_option s_2 l
(fun p0 ->
- Heap.write p0
+ HeapStr.write p0
("length")
(Coq_attributes_data_of { attributes_data_value =
(Coq_value_prim (Coq_prim_number
@@ -1583,7 +1583,7 @@ and run_construct_prealloc s c b args =
(Coq_prim_number (number_of_int (strlength s1))))) in
let%some
s_2 = (object_heap_map_properties_pickable_option s2 l (fun p ->
- Heap.write p ("length")
+ HeapStr.write p ("length")
(Coq_attributes_data_of lenDesc))) in
res_ter s_2 (res_val (Coq_value_object l))) in
let arg_len = (LibList.length args) in
@@ -2137,7 +2137,7 @@ and run_object_get_own_prop s c l x =
res_spec s_2
(ifx_some_or_default
(convert_option_attributes
- (Heap.read_option string_eq p x))
+ (HeapStr.read_option p x))
Coq_full_descriptor_undef (fun x -> x))) in
match b with
| Coq_builtin_get_own_prop_default -> def s
@@ -4064,7 +4064,7 @@ and run_call_prealloc s c b vthis args =
let%some
s11 = (object_heap_map_properties_pickable_option
s10 l (fun p ->
- Heap.write p
+ HeapStr.write p
("length")
(Coq_attributes_data_of a0))) in
let
diff --git a/generator/tests/jsref/JsSyntax.ml b/generator/tests/jsref/JsSyntax.ml
index 88138b8..0cfbc0d 100644
--- a/generator/tests/jsref/JsSyntax.ml
+++ b/generator/tests/jsref/JsSyntax.ml
@@ -212,16 +212,16 @@ type prealloc =
| Coq_prealloc_string_proto_char_at [@f]
| Coq_prealloc_string_proto_char_code_at [@f]
| Coq_prealloc_math [@f]
-| Coq_prealloc_mathop [@f mathop] of mathop
| Coq_prealloc_date [@f]
| Coq_prealloc_regexp [@f]
| Coq_prealloc_error [@f]
| Coq_prealloc_error_proto [@f]
-| Coq_prealloc_native_error [@f error] of native_error
-| Coq_prealloc_native_error_proto [@f error] of native_error
| Coq_prealloc_error_proto_to_string [@f]
| Coq_prealloc_throw_type_error [@f]
| Coq_prealloc_json [@f]
+| Coq_prealloc_mathop [@f mathop] of mathop
+| Coq_prealloc_native_error [@f error] of native_error
+| Coq_prealloc_native_error_proto [@f error] of native_error
type call =
| Coq_call_default [@f]
diff --git a/generator/tests/jsref/JsSyntaxAux.ml b/generator/tests/jsref/JsSyntaxAux.ml
index 9906829..1239ee9 100644
--- a/generator/tests/jsref/JsSyntaxAux.ml
+++ b/generator/tests/jsref/JsSyntaxAux.ml
@@ -3,6 +3,110 @@ open JsSyntax
open LibList
open LibReflect
+let int_of_native_error e =
+ match e with
+ | Coq_native_error_eval -> 1
+ | Coq_native_error_range -> 2
+ | Coq_native_error_ref -> 3
+ | Coq_native_error_syntax -> 4
+ | Coq_native_error_type -> 5
+ | Coq_native_error_uri -> 6
+
+let int_of_mathop o =
+ match o with
+ | Coq_mathop_abs -> 1
+
+let int_of_prealloc p =
+ match p with
+ | Coq_prealloc_global -> 1
+ | Coq_prealloc_global_eval -> 2
+ | Coq_prealloc_global_parse_int -> 3
+ | Coq_prealloc_global_parse_float -> 4
+ | Coq_prealloc_global_is_finite -> 5
+ | Coq_prealloc_global_is_nan -> 6
+ | Coq_prealloc_global_decode_uri -> 7
+ | Coq_prealloc_global_decode_uri_component -> 8
+ | Coq_prealloc_global_encode_uri -> 9
+ | Coq_prealloc_global_encode_uri_component -> 10
+ | Coq_prealloc_object -> 11
+ | Coq_prealloc_object_get_proto_of -> 12
+ | Coq_prealloc_object_get_own_prop_descriptor -> 13
+ | Coq_prealloc_object_get_own_prop_name -> 14
+ | Coq_prealloc_object_create -> 15
+ | Coq_prealloc_object_define_prop -> 16
+ | Coq_prealloc_object_define_props -> 17
+ | Coq_prealloc_object_seal -> 18
+ | Coq_prealloc_object_freeze -> 19
+ | Coq_prealloc_object_prevent_extensions -> 20
+ | Coq_prealloc_object_is_sealed -> 21
+ | Coq_prealloc_object_is_frozen -> 22
+ | Coq_prealloc_object_is_extensible -> 23
+ | Coq_prealloc_object_keys -> 24
+ | Coq_prealloc_object_keys_call -> 25
+ | Coq_prealloc_object_proto -> 26
+ | Coq_prealloc_object_proto_to_string -> 27
+ | Coq_prealloc_object_proto_value_of -> 28
+ | Coq_prealloc_object_proto_has_own_prop -> 29
+ | Coq_prealloc_object_proto_is_prototype_of -> 30
+ | Coq_prealloc_object_proto_prop_is_enumerable -> 31
+ | Coq_prealloc_function -> 32
+ | Coq_prealloc_function_proto -> 33
+ | Coq_prealloc_function_proto_to_string -> 34
+ | Coq_prealloc_function_proto_apply -> 35
+ | Coq_prealloc_function_proto_call -> 36
+ | Coq_prealloc_function_proto_bind -> 37
+ | Coq_prealloc_bool -> 38
+ | Coq_prealloc_bool_proto -> 39
+ | Coq_prealloc_bool_proto_to_string -> 40
+ | Coq_prealloc_bool_proto_value_of -> 41
+ | Coq_prealloc_number -> 42
+ | Coq_prealloc_number_proto -> 43
+ | Coq_prealloc_number_proto_to_string -> 44
+ | Coq_prealloc_number_proto_value_of -> 45
+ | Coq_prealloc_number_proto_to_fixed -> 46
+ | Coq_prealloc_number_proto_to_exponential -> 47
+ | Coq_prealloc_number_proto_to_precision -> 48
+ | Coq_prealloc_array -> 49
+ | Coq_prealloc_array_is_array -> 50
+ | Coq_prealloc_array_proto -> 51
+ | Coq_prealloc_array_proto_to_string -> 52
+ | Coq_prealloc_array_proto_join -> 53
+ | Coq_prealloc_array_proto_pop -> 54
+ | Coq_prealloc_array_proto_push -> 55
+ | Coq_prealloc_string -> 56
+ | Coq_prealloc_string_proto -> 57
+ | Coq_prealloc_string_proto_to_string -> 58
+ | Coq_prealloc_string_proto_value_of -> 59
+ | Coq_prealloc_string_proto_char_at -> 60
+ | Coq_prealloc_string_proto_char_code_at -> 61
+ | Coq_prealloc_math -> 62
+ | Coq_prealloc_date -> 63
+ | Coq_prealloc_regexp -> 64
+ | Coq_prealloc_error -> 65
+ | Coq_prealloc_error_proto -> 66
+ | Coq_prealloc_error_proto_to_string -> 67
+ | Coq_prealloc_throw_type_error -> 68
+ | Coq_prealloc_json -> 69
+ | Coq_prealloc_mathop o -> 100 + int_of_mathop o
+ | Coq_prealloc_native_error e -> 200 + int_of_native_error e
+ | Coq_prealloc_native_error_proto e -> 300 + int_of_native_error e
+
+let prealloc_cmp p1 p2 =
+ int_compare (int_of_prealloc p1) (int_of_prealloc p2)
+
+let object_loc_cmp l1 l2 =
+ match l1 with
+ | Coq_object_loc_normal n1 ->
+ begin match l2 with
+ | Coq_object_loc_normal n2 -> int_compare n1 n2
+ | Coq_object_loc_prealloc p2 -> 1
+ end
+ | Coq_object_loc_prealloc p1 ->
+ begin match l2 with
+ | Coq_object_loc_normal n2 -> -1
+ | Coq_object_loc_prealloc p2 -> prealloc_cmp p1 p2
+ end
+
(** val object_create :
value -> class_name -> bool -> object_properties_type -> coq_object **)
diff --git a/generator/tests/jsref/StdMap.ml b/generator/tests/jsref/StdMap.ml
new file mode 100644
index 0000000..9ce7277
--- /dev/null
+++ b/generator/tests/jsref/StdMap.ml
@@ -0,0 +1,382 @@
+(* copied from ocaml and specialized *)
+
+
+type ('a,'b) t =
+ Empty [@f ]
+ | Node [@f l, x, d, r, h] of ('a,'b) t * 'a * 'b * ('a,'b) t * int
+
+let height = function
+ Empty -> 0
+ | Node(l,x,d,r,h) -> h
+
+let create l x d r =
+ let hl = height l and hr = height r in
+ Node(l, x, d, r, (if int_ge hl hr then hl + 1 else hr + 1))
+
+let singleton x d = Node(Empty, x, d, Empty, 1)
+
+let bal l x d r =
+ let hl = match l with Empty -> 0 | Node(_,_,_,_,h) -> h in
+ let hr = match r with Empty -> 0 | Node(_,_,_,_,h) -> h in
+ if int_gt hl (hr + 2) then begin
+ match l with
+ Empty -> assert false
+ | Node(ll, lv, ld, lr, _) ->
+ if int_ge (height ll) (height lr) then
+ create ll lv ld (create lr x d r)
+ else begin
+ match lr with
+ Empty -> assert false
+ | Node(lrl, lrv, lrd, lrr, _)->
+ create (create ll lv ld lrl) lrv lrd (create lrr x d r)
+ end
+ end else if int_gt hr (hl + 2) then begin
+ match r with
+ Empty -> assert false
+ | Node(rl, rv, rd, rr, _) ->
+ if int_ge (height rr) (height rl) then
+ create (create l x d rl) rv rd rr
+ else begin
+ match rl with
+ Empty -> assert false
+ | Node(rll, rlv, rld, rlr, _) ->
+ create (create l x d rll) rlv rld (create rlr rv rd rr)
+ end
+ end else
+ Node(l, x, d, r, (if int_ge hl hr then hl + 1 else hr + 1))
+
+let empty = Empty
+
+let is_empty s =
+ match s with
+ | Empty -> true
+ | _ -> false
+
+let rec add compare x data s =
+ match s with
+ Empty ->
+ Node(Empty, x, data, Empty, 1)
+ | Node(l, v, d, r, h) ->
+ let c = compare x v in
+ if int_eq c 0 then
+ Node(l, x, data, r, h)
+ else if int_lt c 0 then
+ bal (add compare x data l) v d r
+ else
+ bal l v d (add compare x data r)
+
+let rec find compare x s =
+ match s with
+ Empty -> assert false
+ (* raise Not_found *)
+ | Node(l, v, d, r, _) ->
+ let c = compare x v in
+ if int_eq c 0 then d
+ else find compare x (if int_lt c 0 then l else r)
+
+(* added *)
+let rec find_option compare x s =
+ match s with
+ Empty -> None
+ | Node(l, v, d, r, _) ->
+ let c = compare x v in
+ if int_eq c 0 then Some d
+ else find_option compare x (if int_lt c 0 then l else r)
+
+
+let rec mem compare x s =
+ match s with
+ Empty ->
+ false
+ | Node(l, v, d, r, _) ->
+ let c = compare x v in
+ int_eq c 0 || mem compare x (if int_lt c 0 then l else r)
+
+
+let rec min_binding s =
+ match s with
+ Empty -> raise Not_found
+ | Node(l, x, d, r, _) ->
+ match l with
+ Empty -> (x, d)
+ | _ -> min_binding l
+ (*
+ | Node(Empty, x, d, r, _) -> (x, d)
+ | Node(l, x, d, r, _) -> min_binding l
+ *)
+
+let rec remove_min_binding s =
+ match s with
+ Empty -> assert false
+ | Node(l, x, d, r, _) ->
+ match l with
+ Empty -> r
+ | _ -> bal (remove_min_binding l) x d r
+ (*
+ | Node(Empty, x, d, r, _) -> r
+ | Node(l, x, d, r, _) -> bal (remove_min_binding l) x d r
+ *)
+
+
+let merge t1 t2 =
+ match t1 with
+ | Empty -> t2
+ | _ ->
+ match t2 with
+ | Empty -> t1
+ | _ ->
+ let (x, d) = min_binding t2 in
+ bal t1 x d (remove_min_binding t2)
+
+ (*
+ match (t1, t2) with
+ (Empty, t) -> t
+ | (t, Empty) -> t
+ | (_, _) ->
+ let (x, d) = min_binding t2 in
+ bal t1 x d (remove_min_binding t2)
+ *)
+
+let rec remove compare x s =
+ match s with
+ Empty ->
+ Empty
+ | Node(l, v, d, r, h) ->
+ let c = compare x v in
+ if int_eq c 0 then
+ merge l r
+ else if int_lt c 0 then
+ bal (remove compare x l) v d r
+ else
+ bal l v d (remove compare x r)
+
+let rec fold f m accu =
+ match m with
+ Empty -> accu
+ | Node(l, v, d, r, _) ->
+ fold f r (f v d (fold f l accu))
+
+
+
+
+(*------------------------------
+ module type OrderedType =
+ sig
+ type t
+ val compare: t -> t -> int
+ end
+module type S =
+ sig
+ type key
+ type +'a t
+ val empty: 'a t
+ val is_empty: 'a t -> bool
+ val mem: key -> 'a t -> bool
+ val add: key -> 'a -> 'a t -> 'a t
+ val singleton: key -> 'a -> 'a t
+ val remove: key -> 'a t -> 'a t
+ val merge:
+ (key -> 'a option -> 'b option -> 'c option) -> 'a t -> 'b t -> 'c t
+ val compare: ('a -> 'a -> int) -> 'a t -> 'a t -> int
+ val equal: ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
+ val iter: (key -> 'a -> unit) -> 'a t -> unit
+ val fold: (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
+ val for_all: (key -> 'a -> bool) -> 'a t -> bool
+ val exists: (key -> 'a -> bool) -> 'a t -> bool
+ val filter: (key -> 'a -> bool) -> 'a t -> 'a t
+ val partition: (key -> 'a -> bool) -> 'a t -> 'a t * 'a t
+ val cardinal: 'a t -> int
+ val bindings: 'a t -> (key * 'a) list
+ val min_binding: 'a t -> (key * 'a)
+ val max_binding: 'a t -> (key * 'a)
+ val choose: 'a t -> (key * 'a)
+ val split: key -> 'a t -> 'a t * 'a option * 'a t
+ val find: key -> 'a t -> 'a
+ val map: ('a -> 'b) -> 'a t -> 'b t
+ val mapi: (key -> 'a -> 'b) -> 'a t -> 'b t
+ end
+
+module Make(Ord: OrderedType) = struct
+ type key = Ord.t
+
+
+end
+
+
+
+let rec map f = function
+ Empty ->
+ Empty
+ | Node(l, v, d, r, h) ->
+ let l' = map f l in
+ let d' = f d in
+ let r' = map f r in
+ Node(l', v, d', r', h)
+
+let rec iter f = function
+ Empty -> ()
+ | Node(l, v, d, r, _) ->
+ iter f l; f v d; iter f r
+
+let rec mapi f = function
+ Empty ->
+ Empty
+ | Node(l, v, d, r, h) ->
+ let l' = mapi f l in
+ let d' = f v d in
+ let r' = mapi f r in
+ Node(l', v, d', r', h)
+
+
+let rec max_binding = function
+ Empty -> raise Not_found
+ | Node(l, x, d, Empty, _) -> (x, d)
+ | Node(l, x, d, r, _) -> max_binding r
+
+
+
+ let rec for_all p = function
+ Empty -> true
+ | Node(l, v, d, r, _) -> p v d && for_all p l && for_all p r
+
+ let rec exists p = function
+ Empty -> false
+ | Node(l, v, d, r, _) -> p v d || exists p l || exists p r
+
+ (* Beware: those two functions assume that the added k is *strictly*
+ smaller (or bigger) than all the present keys in the tree; it
+ does not test for equality with the current min (or max) key.
+
+ Indeed, they are only used during the "join" operation which
+ respects this precondition.
+ *)
+
+ let rec add_min_binding k v = function
+ | Empty -> singleton k v
+ | Node (l, x, d, r, h) ->
+ bal (add_min_binding k v l) x d r
+
+ let rec add_max_binding k v = function
+ | Empty -> singleton k v
+ | Node (l, x, d, r, h) ->
+ bal l x d (add_max_binding k v r)
+
+ (* Same as create and bal, but no assumptions are made on the
+ relative heights of l and r. *)
+
+ let rec join l v d r =
+ match (l, r) with
+ (Empty, _) -> add_min_binding v d r
+ | (_, Empty) -> add_max_binding v d l
+ | (Node(ll, lv, ld, lr, lh), Node(rl, rv, rd, rr, rh)) ->
+ if lh > rh + 2 then bal ll lv ld (join lr v d r) else
+ if rh > lh + 2 then bal (join l v d rl) rv rd rr else
+ create l v d r
+
+ (* Merge two trees l and r into one.
+ All elements of l must precede the elements of r.
+ No assumption on the heights of l and r. *)
+
+ let concat t1 t2 =
+ match (t1, t2) with
+ (Empty, t) -> t
+ | (t, Empty) -> t
+ | (_, _) ->
+ let (x, d) = min_binding t2 in
+ join t1 x d (remove_min_binding t2)
+
+ let concat_or_join t1 v d t2 =
+ match d with
+ | Some d -> join t1 v d t2
+ | None -> concat t1 t2
+
+ let rec split x = function
+ Empty ->
+ (Empty, None, Empty)
+ | Node(l, v, d, r, _) ->
+ let c = compare x v in
+ if int_eq c 0 then (l, Some d, r)
+ else if int_lt c 0 then
+ let (ll, pres, rl) = split x l in (ll, pres, join rl v d r)
+ else
+ let (lr, pres, rr) = split x r in (join l v d lr, pres, rr)
+
+ let rec merge f s1 s2 =
+ match (s1, s2) with
+ (Empty, Empty) -> Empty
+ | (Node (l1, v1, d1, r1, h1), _) when h1 >= height s2 ->
+ let (l2, d2, r2) = split v1 s2 in
+ concat_or_join (merge f l1 l2) v1 (f v1 (Some d1) d2) (merge f r1 r2)
+ | (_, Node (l2, v2, d2, r2, h2)) ->
+ let (l1, d1, r1) = split v2 s1 in
+ concat_or_join (merge f l1 l2) v2 (f v2 d1 (Some d2)) (merge f r1 r2)
+ | _ ->
+ assert false
+
+ let rec filter p = function
+ Empty -> Empty
+ | Node(l, v, d, r, _) ->
+ (* call [p] in the expected left-to-right order *)
+ let l' = filter p l in
+ let pvd = p v d in
+ let r' = filter p r in
+ if pvd then join l' v d r' else concat l' r'
+
+ let rec partition p = function
+ Empty -> (Empty, Empty)
+ | Node(l, v, d, r, _) ->
+ (* call [p] in the expected left-to-right order *)
+ let (lt, lf) = partition p l in
+ let pvd = p v d in
+ let (rt, rf) = partition p r in
+ if pvd
+ then (join lt v d rt, concat lf rf)
+ else (concat lt rt, join lf v d rf)
+
+ type 'a enumeration = End | More of key * 'a * 'a t * 'a enumeration
+
+ let rec cons_enum m e =
+ match m with
+ Empty -> e
+ | Node(l, v, d, r, _) -> cons_enum l (More(v, d, r, e))
+
+ let compare cmp m1 m2 =
+ let rec compare_aux e1 e2 =
+ match (e1, e2) with
+ (End, End) -> 0
+ | (End, _) -> -1
+ | (_, End) -> 1
+ | (More(v1, d1, r1, e1), More(v2, d2, r2, e2)) ->
+ let c = compare v1 v2 in
+ if c <> 0 then c else
+ let c = cmp d1 d2 in
+ if c <> 0 then c else
+ compare_aux (cons_enum r1 e1) (cons_enum r2 e2)
+ in compare_aux (cons_enum m1 End) (cons_enum m2 End)
+
+ let equal cmp m1 m2 =
+ let rec equal_aux e1 e2 =
+ match (e1, e2) with
+ (End, End) -> true
+ | (End, _) -> false
+ | (_, End) -> false
+ | (More(v1, d1, r1, e1), More(v2, d2, r2, e2)) ->
+ compare v1 v2 = 0 && cmp d1 d2 &&
+ equal_aux (cons_enum r1 e1) (cons_enum r2 e2)
+ in equal_aux (cons_enum m1 End) (cons_enum m2 End)
+
+ let rec cardinal = function
+ Empty -> 0
+ | Node(l, _, _, r, _) -> cardinal l + 1 + cardinal r
+
+ let rec bindings_aux accu = function
+ Empty -> accu
+ | Node(l, v, d, r, _) -> bindings_aux ((v, d) :: bindings_aux accu r) l
+
+ let bindings s =
+ bindings_aux [] s
+
+ let choose = min_binding
+
+
+*)
diff --git a/navig-driver.js b/navig-driver.js
index e7ea22e..b716cf4 100644
--- a/navig-driver.js
+++ b/navig-driver.js
@@ -213,7 +213,7 @@ function jsvalue_of_value(v) {
}
function lookup_var_in_record_decl(name, env_record_decl) {
- var ro = Heap.read_option(string_eq, env_record_decl, name);
+ var ro = HeapStr.read_option(env_record_decl, name);
switch (ro.tag) {
case "None":
return undefined;
@@ -244,7 +244,7 @@ function lookup_var_in_object(state, name, loc) {
if (obj_opt.tag != "Some") throw "show_object: unbound object";
var obj = obj_opt.value;
var props = obj.object_properties_;
- var ro = Heap.read_option(string_eq, props, name);
+ var ro = HeapStr.read_option(props, name);
switch (ro.tag) {
case "None":
return undefined;
@@ -693,10 +693,13 @@ function string_of_any(v) {
// --------------- Views for JS state/context ----------------
-function array_of_heap(heap) {
- var items_list = Heap.to_list(string_eq, heap);
+/*
+function array_of_heap(compare, heap) {
+ var items_list = Heap.to_list(compare, heap);
return encoded_list_to_array(items_list);
-}
+}
+*/
+
function string_of_prealloc(prealloc) {
return (prealloc.tag).slice("Coq_prealloc_".length);
@@ -804,7 +807,7 @@ function show_object(state, loc, target, depth) {
if (obj_opt.tag != "Some") throw "show_object: unbound object";
var obj = obj_opt.value;
var props = obj.object_properties_;
- var key_value_pair_array = array_of_heap(props);
+ var key_value_pair_array = encoded_list_to_array(HeapStr.to_list(props));
//
var is_global = (string_of_loc(loc) == "global");
for (var j = 0; j < key_value_pair_array.length; j++) {
@@ -890,7 +893,7 @@ function show_value(state, v, target, depth) {
function show_decl_env_record(state, env_record_decl, target) {
// env_record_decl : (string, mutability * value) Heap.heap
var t = $("#" + target);
- var items_array = array_of_heap(env_record_decl);
+ var items_array = encoded_list_to_array(HeapStr.to_list(env_record_decl));
for (var i = 0; i < items_array.length; i++) {
var var_name = items_array[i][0];
var mutability = items_array[i][1][0];
@@ -1449,7 +1452,7 @@ readSourceParseAndRun();
//stepTo(5873);
// setExample(20);
setExample(3);
-$("#reach_condition").val("S_line() == 3 && S('i') == 1 && I_line() == 858");
+$("#reach_condition").val("S_line() == 3 && S('i') == 1");
function showCurrent() {
--
GitLab