Remove dependency on Prheap for jsjsref

generator/Makefile

@@ -73,7 +73,6 @@ all: everything
 
 CC          := ocamlc -c
 OCAMLDEP    := ocamldep -one-line
-DEPSED      := sed -e "s/cmx/cmi/; s/cmx/cmi/g"
 OCAMLBUILD := ocamlbuild -j 4 -classic-display -use-ocamlfind -X tests -X $(STDLIB_DIR)
 
 GENERATOR := ./main.byte
@@ -106,23 +105,15 @@ $(STDLIB_DIR)/stdlib.cmi: $(STDLIB_DIR)/stdlib.mli
 
 ##### Rule for dependencies
 
-tests/%.mli.d: tests/%.mli
-	$(OCAMLDEP) -I $(<D) $< | $(DEPSED) > $@
-
-tests/%.ml.d: tests/%.ml
-	$(OCAMLDEP) -I $(<D) $< | $(DEPSED) > $@
+tests/%.d: tests/%
+	$(OCAMLDEP) -all -I $(<D) $< > $@
 
 ##### Rule for cmi
 
 tests/%.cmi: tests/%.ml main.byte stdlib 
 	./main.byte -mode cmi -I $(<D) $<
 
-##### Custome cmi rules for compilation of mli files without ml source
-
-$(JSREF_PATH)/Translate_syntax.cmi: $(JSREF_PATH)/Translate_syntax.mli $(JSREF_PATH)/JsSyntax.cmi stdlib
-	ocamlc -I $(JSREF_PATH) -I stdlib_ml -open Stdlib $<
-
-$(JSREF_PATH)/Prheap.cmi: $(JSREF_PATH)/Prheap.mli stdlib $(JSREF_PATH)/JsSyntax.cmi
+tests/%.cmi: tests/%.mli stdlib
 	ocamlc -I $(JSREF_PATH) -I stdlib_ml -open Stdlib $<
 
 ##### Rule for log/unlog/token

generator/tests/jsref/Debug.mli

+val not_yet_implemented_because : string -> string -> unit
+val impossible_because : string -> string -> unit
+val impossible_with_heap_because :
+  string -> JsSyntax.state -> string -> unit
+val ref_get_value : JsSyntax.ref -> unit
+val ref_get_value_2 : JsSyntax.resvalue -> unit
+val run_object_method : JsSyntax.object_loc -> unit
+val run_object_heap_set_extensible : JsSyntax.object_loc -> unit
+val lexical_env_get_identifier_ref : string -> unit

generator/tests/jsref/JsInterpreterMonads.ml

@@ -79,10 +79,7 @@ let destr_list l d f =
 let if_empty_label s r k =
   if label_comparable r.res_label Coq_label_empty
   then k ()
-  else (fun s message ->
-  print_endline (__LOC__ ^ ": Stuck!\nState:  " ^ Prheap.prstate true s
-    ^ "\nMessage:\t" ^ Prheap.string_of_char_list message) ;
-  Coq_result_impossible)
+  else (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
          s
          ("[if_empty_label] received a normal result with non-empty label.")
 
@@ -92,9 +89,7 @@ let if_some op k =
   match op with
   | Some a -> k a
   | None ->
-    (fun s ->
-  print_endline (__LOC__ ^ ": Stuck because: " ^ Prheap.string_of_char_list s) ;
-  Coq_result_impossible)
+    (fun s -> Debug.impossible_because __LOC__ s; Coq_result_impossible)
       ("[if_some] called with [None].")
 
 (** val if_some_or_default : 'a2 option -> 'a1 -> ('a2 -> 'a1) -> 'a1 **)
@@ -166,17 +161,11 @@ let if_void w k =
     match rv with
     | Coq_resvalue_empty -> k s
     | Coq_resvalue_value v ->
-      (fun s message ->
-  print_endline (__LOC__ ^ ": Stuck!\nState:  " ^ Prheap.prstate true s
-    ^ "\nMessage:\t" ^ Prheap.string_of_char_list message) ;
-  Coq_result_impossible)
+      (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
         s
         ("[if_void called] with non-void result value.")
     | Coq_resvalue_ref r ->
-      (fun s message ->
-  print_endline (__LOC__ ^ ": Stuck!\nState:  " ^ Prheap.prstate true s
-    ^ "\nMessage:\t" ^ Prheap.string_of_char_list message) ;
-  Coq_result_impossible)
+      (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
         s
         ("[if_void called] with non-void result value."))
 
@@ -205,18 +194,12 @@ let if_any_or_throw w k1 k2 =
     | Coq_restype_throw ->
       (match r.res_value with
        | Coq_resvalue_empty ->
-         (fun s message ->
-  print_endline (__LOC__ ^ ": Stuck!\nState:  " ^ Prheap.prstate true s
-    ^ "\nMessage:\t" ^ Prheap.string_of_char_list message) ;
-  Coq_result_impossible)
+         (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
            s
            ("[if_any_or_throw] called with a non-value result.")
        | Coq_resvalue_value v -> if_empty_label s r (fun x -> k2 s v)
        | Coq_resvalue_ref r0 ->
-         (fun s message ->
-  print_endline (__LOC__ ^ ": Stuck!\nState:  " ^ Prheap.prstate true s
-    ^ "\nMessage:\t" ^ Prheap.string_of_char_list message) ;
-  Coq_result_impossible)
+         (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
            s
            ("[if_any_or_throw] called with a non-value result.")))
 
@@ -250,18 +233,12 @@ let if_value w k =
   if_success w (fun s rv ->
     match rv with
     | Coq_resvalue_empty ->
-      (fun s message ->
-  print_endline (__LOC__ ^ ": Stuck!\nState:  " ^ Prheap.prstate true s
-    ^ "\nMessage:\t" ^ Prheap.string_of_char_list message) ;
-  Coq_result_impossible)
+      (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
         s
         ("[if_value] called with non-value.")
     | Coq_resvalue_value v -> k s v
     | Coq_resvalue_ref r ->
-      (fun s message ->
-  print_endline (__LOC__ ^ ": Stuck!\nState:  " ^ Prheap.prstate true s
-    ^ "\nMessage:\t" ^ Prheap.string_of_char_list message) ;
-  Coq_result_impossible)
+      (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
         s
         ("[if_value] called with non-value."))
 
@@ -273,39 +250,24 @@ let if_bool w k =
     | Coq_value_prim p ->
       (match p with
        | Coq_prim_undef ->
-         (fun s message ->
-  print_endline (__LOC__ ^ ": Stuck!\nState:  " ^ Prheap.prstate true s
-    ^ "\nMessage:\t" ^ Prheap.string_of_char_list message) ;
-  Coq_result_impossible)
+         (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
            s
            ("[if_bool] called with non-boolean value.")
        | Coq_prim_null ->
-         (fun s message ->
-  print_endline (__LOC__ ^ ": Stuck!\nState:  " ^ Prheap.prstate true s
-    ^ "\nMessage:\t" ^ Prheap.string_of_char_list message) ;
-  Coq_result_impossible)
+         (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
            s
            ("[if_bool] called with non-boolean value.")
        | Coq_prim_bool b -> k s b
        | Coq_prim_number n ->
-         (fun s message ->
-  print_endline (__LOC__ ^ ": Stuck!\nState:  " ^ Prheap.prstate true s
-    ^ "\nMessage:\t" ^ Prheap.string_of_char_list message) ;
-  Coq_result_impossible)
+         (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
            s
            ("[if_bool] called with non-boolean value.")
        | Coq_prim_string s0 ->
-         (fun s message ->
-  print_endline (__LOC__ ^ ": Stuck!\nState:  " ^ Prheap.prstate true s
-    ^ "\nMessage:\t" ^ Prheap.string_of_char_list message) ;
-  Coq_result_impossible)
+         (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
            s
            ("[if_bool] called with non-boolean value."))
     | Coq_value_object o ->
-      (fun s message ->
-  print_endline (__LOC__ ^ ": Stuck!\nState:  " ^ Prheap.prstate true s
-    ^ "\nMessage:\t" ^ Prheap.string_of_char_list message) ;
-  Coq_result_impossible)
+      (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
         s
         ("[if_bool] called with non-boolean value."))
 
@@ -316,10 +278,7 @@ let if_object w k =
   if_value w (fun s v ->
     match v with
     | Coq_value_prim p ->
-      (fun s message ->
-  print_endline (__LOC__ ^ ": Stuck!\nState:  " ^ Prheap.prstate true s
-    ^ "\nMessage:\t" ^ Prheap.string_of_char_list message) ;
-  Coq_result_impossible)
+      (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
         s
         ("[if_object] called on a primitive.")
     | Coq_value_object l -> k s l)
@@ -333,39 +292,24 @@ let if_string w k =
     | Coq_value_prim p ->
       (match p with
        | Coq_prim_undef ->
-         (fun s message ->
-  print_endline (__LOC__ ^ ": Stuck!\nState:  " ^ Prheap.prstate true s
-    ^ "\nMessage:\t" ^ Prheap.string_of_char_list message) ;
-  Coq_result_impossible)
+         (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
            s
            ("[if_string] called on a non-string value.")
        | Coq_prim_null ->
-         (fun s message ->
-  print_endline (__LOC__ ^ ": Stuck!\nState:  " ^ Prheap.prstate true s
-    ^ "\nMessage:\t" ^ Prheap.string_of_char_list message) ;
-  Coq_result_impossible)
+         (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
            s
            ("[if_string] called on a non-string value.")
        | Coq_prim_bool b ->
-         (fun s message ->
-  print_endline (__LOC__ ^ ": Stuck!\nState:  " ^ Prheap.prstate true s
-    ^ "\nMessage:\t" ^ Prheap.string_of_char_list message) ;
-  Coq_result_impossible)
+         (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
            s
            ("[if_string] called on a non-string value.")
        | Coq_prim_number n ->
-         (fun s message ->
-  print_endline (__LOC__ ^ ": Stuck!\nState:  " ^ Prheap.prstate true s
-    ^ "\nMessage:\t" ^ Prheap.string_of_char_list message) ;
-  Coq_result_impossible)
+         (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
            s
            ("[if_string] called on a non-string value.")
        | Coq_prim_string s0 -> k s s0)
     | Coq_value_object o ->
-      (fun s message ->
-  print_endline (__LOC__ ^ ": Stuck!\nState:  " ^ Prheap.prstate true s
-    ^ "\nMessage:\t" ^ Prheap.string_of_char_list message) ;
-  Coq_result_impossible)
+      (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
         s
         ("[if_string] called on a non-string value."))
 
@@ -378,39 +322,24 @@ let if_number w k =
     | Coq_value_prim p ->
       (match p with
        | Coq_prim_undef ->
-         (fun s message ->
-  print_endline (__LOC__ ^ ": Stuck!\nState:  " ^ Prheap.prstate true s
-    ^ "\nMessage:\t" ^ Prheap.string_of_char_list message) ;
-  Coq_result_impossible)
+         (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
            s
            ("[if_number] called with non-number value.")
        | Coq_prim_null ->
-         (fun s message ->
-  print_endline (__LOC__ ^ ": Stuck!\nState:  " ^ Prheap.prstate true s
-    ^ "\nMessage:\t" ^ Prheap.string_of_char_list message) ;
-  Coq_result_impossible)
+         (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
            s
            ("[if_number] called with non-number value.")
        | Coq_prim_bool b ->
-         (fun s message ->
-  print_endline (__LOC__ ^ ": Stuck!\nState:  " ^ Prheap.prstate true s
-    ^ "\nMessage:\t" ^ Prheap.string_of_char_list message) ;
-  Coq_result_impossible)
+         (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
            s
            ("[if_number] called with non-number value.")
        | Coq_prim_number n -> k s n
        | Coq_prim_string s0 ->
-         (fun s message ->
-  print_endline (__LOC__ ^ ": Stuck!\nState:  " ^ Prheap.prstate true s
-    ^ "\nMessage:\t" ^ Prheap.string_of_char_list message) ;
-  Coq_result_impossible)
+         (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
            s
            ("[if_number] called with non-number value."))
     | Coq_value_object o ->
-      (fun s message ->
-  print_endline (__LOC__ ^ ": Stuck!\nState:  " ^ Prheap.prstate true s
-    ^ "\nMessage:\t" ^ Prheap.string_of_char_list message) ;
-  Coq_result_impossible)
+      (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
         s
         ("[if_number] called with non-number value."))
 
@@ -421,10 +350,7 @@ let if_prim w k =
     match v with
     | Coq_value_prim w0 -> k s w0
     | Coq_value_object o ->
-      (fun s message ->
-  print_endline (__LOC__ ^ ": Stuck!\nState:  " ^ Prheap.prstate true s
-    ^ "\nMessage:\t" ^ Prheap.string_of_char_list message) ;
-  Coq_result_impossible)
+      (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
         s
         ("[if_primitive] called on an object."))
 
@@ -441,10 +367,7 @@ let if_abort o k =
   | Coq_out_div -> k ()
   | Coq_out_ter (s0, r) ->
     if restype_comparable r.res_type Coq_restype_normal
-    then (fun s message ->
-  print_endline (__LOC__ ^ ": Stuck!\nState:  " ^ Prheap.prstate true s
-    ^ "\nMessage:\t" ^ Prheap.string_of_char_list message) ;
-  Coq_result_impossible)
+    then (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
            s0
            ("[if_abort] received a normal result!")
     else k ()

generator/tests/jsref/Prheap.mli

-
-  val prstate : bool -> JsSyntax.state -> string
-  val prloc : JsSyntax.object_loc -> string
-  val prresvalue : JsSyntax.resvalue -> string
-  val string_of_char_list : string -> string
-
-(*
-module Prheap : sig
-end
-*)