From a3f2cd92bd0ffaa6317b0ddaafd6585def0f2413 Mon Sep 17 00:00:00 2001
From: Alan Schmitt <alan.schmitt@polytechnique.org>
Date: Tue, 2 Feb 2016 10:41:57 +0100
Subject: [PATCH] =?UTF-8?q?=C3=A7a=20compile?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
generator/stdlib_ml/stdlib.mli | 3 ++
generator/tests/jsref/JsCommon.ml | 8 +++--
generator/tests/jsref/JsCommonAux.ml | 2 +-
generator/tests/jsref/JsInit.ml | 23 +++---------
generator/tests/jsref/JsInterpreter.ml | 37 ++++++++++++--------
generator/tests/jsref/JsInterpreterMonads.ml | 2 +-
generator/tests/jsref/JsSyntax.ml | 2 +-
generator/tests/jsref/Prheap.mli | 4 ++-
8 files changed, 42 insertions(+), 39 deletions(-)
diff --git a/generator/stdlib_ml/stdlib.mli b/generator/stdlib_ml/stdlib.mli
index f151742..3ab8fa9 100644
--- a/generator/stdlib_ml/stdlib.mli
+++ b/generator/stdlib_ml/stdlib.mli
@@ -51,6 +51,8 @@ val ( <= ) : 'a -> 'a -> bool
val ( >= ) : 'a -> 'a -> bool
val compare : 'a -> 'a -> int
+val ( && ) : bool -> bool -> bool
+
val stuck : string -> 'a
(* Structural equality, need to be careful with implementation *)
@@ -111,6 +113,7 @@ val raise : exn -> 'a
(* JSRef specific functions *)
val prerr_string : string -> unit
val prerr_newline : unit -> unit
+val prerr_endline : string -> unit
module Parser_syntax : sig (* ARTHUR: to implement *)
diff --git a/generator/tests/jsref/JsCommon.ml b/generator/tests/jsref/JsCommon.ml
index ff70f85..8c8b346 100644
--- a/generator/tests/jsref/JsCommon.ml
+++ b/generator/tests/jsref/JsCommon.ml
@@ -188,7 +188,8 @@ let object_alloc s o =
state_fresh_locations = state_fresh_locations0; state_event_list =
ev_list } = s
in
- let Coq_stream_intro (n, alloc) = Lazy.force state_fresh_locations0 in
+ let n = state_fresh_locations0 in
+ let alloc = state_fresh_locations0 + 1 in
let l = Coq_object_loc_normal n in
(l,
(object_write { state_object_heap = cells; state_env_record_heap =
@@ -312,7 +313,8 @@ let env_record_alloc s e =
state_fresh_locations = state_fresh_locations0; state_event_list =
ev_list } = s
in
- let Coq_stream_intro (l, alloc) = Lazy.force state_fresh_locations0 in
+ let l = state_fresh_locations0 in
+ let alloc = state_fresh_locations0 + 1 in
let bindings' = Heap.write bindings l e in
(l, { state_object_heap = cells; state_env_record_heap = bindings';
state_fresh_locations = alloc; state_event_list = ev_list })
@@ -582,7 +584,7 @@ let elision_tail_remove ol =
(** val parse_pickable : string -> bool -> prog coq_Pickable_option **)
let parse_pickable = (fun s strict ->
- let str = String.concat "" (List.map (String.make 1) s) in
+ let str = s in
(* try ARTHUR HACK *)
let parserExp = Parser_main.exp_from_string ~force_strict:strict str in
Some (JsSyntaxInfos.add_infos_prog strict
diff --git a/generator/tests/jsref/JsCommonAux.ml b/generator/tests/jsref/JsCommonAux.ml
index 0df384e..ff87f89 100644
--- a/generator/tests/jsref/JsCommonAux.ml
+++ b/generator/tests/jsref/JsCommonAux.ml
@@ -10,7 +10,7 @@ open LibReflect
open LibString
open Shared
-let __ = let rec f _ = Obj.repr f in Obj.repr f
+let __ = ()
(** val if_some_then_same_dec :
'a1 option -> 'a1 option -> ('a1 -> 'a1 -> coq_Decidable) ->
diff --git a/generator/tests/jsref/JsInit.ml b/generator/tests/jsref/JsInit.ml
index 046ec3f..91b3f8a 100644
--- a/generator/tests/jsref/JsInit.ml
+++ b/generator/tests/jsref/JsInit.ml
@@ -73,14 +73,7 @@ let object_prealloc_global_proto = (Coq_value_prim Coq_prim_null)
(** val object_prealloc_global_class : string **)
-let object_prealloc_global_class = (
- let rec aux s _foo_ = match _foo_ with
- | 0 -> []
- | n -> let n' = n - 1 in
- s.[n'] :: aux s n'
- in let aux2 s =
- List.rev (aux s (String.length s))
- in aux2 "GlobalClass")
+let object_prealloc_global_class = "GlobalClass"
(** val object_prealloc_global_properties :
(prop_name, attributes) Heap.heap **)
@@ -791,7 +784,7 @@ let object_prealloc_string_proto =
Coq_prealloc_object_proto))
("String") p1
in
- object_with_primitive_value o (Coq_value_prim (Coq_prim_string []))
+ object_with_primitive_value o (Coq_value_prim (Coq_prim_string ""))
(** val string_proto_to_string_function_object : coq_object **)
@@ -905,7 +898,7 @@ let object_prealloc_error_proto =
in
let p1 =
write_native p0 ("message")
- (Coq_value_prim (Coq_prim_string []))
+ (Coq_value_prim (Coq_prim_string ""))
in
let p2 =
write_native p1
@@ -950,7 +943,7 @@ let object_prealloc_native_error_proto ne =
in
let p1 =
write_native p0 ("message")
- (Coq_value_prim (Coq_prim_string []))
+ (Coq_value_prim (Coq_prim_string ""))
in
object_create_builtin (Coq_value_object (Coq_object_loc_prealloc
Coq_prealloc_error_proto)) ("Error") p1
@@ -1326,15 +1319,9 @@ let env_record_heap_initial =
Heap.write Heap.empty env_loc_global_env_record
(env_record_object_default (Coq_object_loc_prealloc Coq_prealloc_global))
-(** val all_locations : int -> int stream **)
-
-let rec all_locations k =
- lazy (Coq_stream_intro (k, (all_locations (Pervasives.succ k))))
-
(** val dummy_fresh_locations : int stream **)
-let dummy_fresh_locations =
- all_locations (Pervasives.succ 0)
+let dummy_fresh_locations = 0
(** val state_initial : state **)
diff --git a/generator/tests/jsref/JsInterpreter.ml b/generator/tests/jsref/JsInterpreter.ml
index 992914b..b126188 100644
--- a/generator/tests/jsref/JsInterpreter.ml
+++ b/generator/tests/jsref/JsInterpreter.ml
@@ -23,8 +23,8 @@ open List0
open Shared
open String0
-type __ = Obj.t
-let __ = let rec f _ = Obj.repr f in Obj.repr f
+type __ = unit
+let __ = ()
(** val build_error : state -> value -> value -> result **)
@@ -68,7 +68,7 @@ let run_object_method proj s l =
let run_object_method proj s l =
let opt = object_binds_pickable_option s l in
begin match opt with
- | None -> prerr_endline (Printf.sprintf "Warning: in run_object_method the location %s is unfetchable." (Prheap.prloc l))
+ | None -> prerr_endline ("Warning: in run_object_method the location" ^ (Prheap.prloc l) ^ " is unfetchable." )
| _ -> ()
end;
LibOption.map proj opt
@@ -83,7 +83,7 @@ let run_object_heap_set_extensible b s l =
let run_object_heap_set_extensible b s l =
let opt = object_binds_pickable_option s l in
begin match opt with
- | None -> prerr_endline (Printf.sprintf "Warning: in run_object_heap_set_extensible the location %s is unfetchable." (Prheap.prloc l))
+ | None -> prerr_endline ("Warning: in run_object_heap_set_extensible the location " ^ (Prheap.prloc l) ^ " is unfetchable." )
| _ -> ()
end;
LibOption.map (fun o -> object_write s l (object_set_extensible o b)) opt
@@ -1353,11 +1353,20 @@ let ref_get_value runs0 s c _foo_ = match _foo_ with
let ref_get_value runs s c r =
let res = ref_get_value runs s c r in match res with
- | JsInterpreterMonads.Coq_result_some (Coq_specret_val (_, rs)) -> begin match rs with
- | Coq_value_prim (Coq_prim_undef) ->
+ | JsInterpreterMonads.Coq_result_some crs ->
+ begin match crs with
+ | (Coq_specret_val (_,rs)) ->
+ begin match rs with
+ | Coq_value_prim cvp ->
+ begin match cvp with
+ | Coq_prim_undef ->
prerr_string ("Warning: ref_get_value returns the undefined value on "); prerr_string (Prheap.prresvalue r); prerr_newline(); res
+ | _ -> res
+ end
| _ -> res
- end
+ end
+ | _ -> res
+ end
| _ -> res
(** val run_expr_get_value :
@@ -2353,7 +2362,7 @@ let run_construct_prealloc runs0 s c b args =
res_ter s' (res_val (Coq_value_object l)))))) (fun follow ->
let_binding (LibList.length args) (fun arg_len ->
if nat_comparable arg_len 0
- then follow s []
+ then follow s ""
else let_binding (get_arg 0 args) (fun arg ->
if_string (to_string runs0 s c arg) (fun s0 s1 ->
follow s0 s1))))))
@@ -2728,7 +2737,7 @@ let make_arg_getter runs0 s c x x0 =
let make_arg_setter runs0 s c x x0 =
let xparam = append x ("_arg") in
let xbd =
- append x (append (" = ") (append xparam (';'::[])))
+ append x (append (" = ") (append xparam ";"))
in
let bd = Coq_funcbody_intro ((Coq_prog_intro (true, ((Coq_element_stat
(Coq_stat_expr (Coq_expr_assign ((Coq_expr_identifier x), None,
@@ -2768,7 +2777,7 @@ let rec arguments_object_map_loop runs0 s c l xs len args x str lmap xsmap =
(fun s1 b ->
if ge_nat_decidable len' (LibList.length xs)
then arguments_object_map_loop' s1 xsmap
- else let dummy = [] in
+ else let dummy = "" in
let_binding (nth_def dummy len' xs) (fun x0 ->
if or_decidable (bool_comparable str true)
(coq_Mem_decidable string_comparable x0 xsmap)
@@ -5236,8 +5245,8 @@ let valueToStringForJoin runs0 s c l k =
match v with
| Coq_value_prim p ->
(match p with
- | Coq_prim_undef -> res_spec s1 []
- | Coq_prim_null -> res_spec s1 []
+ | Coq_prim_undef -> res_spec s1 ""
+ | Coq_prim_null -> res_spec s1 ""
| Coq_prim_bool b ->
if_string (to_string runs0 s1 c v) (fun s2 s3 -> res_spec s2 s3)
| Coq_prim_number n ->
@@ -5933,7 +5942,7 @@ let run_call_prealloc runs0 s c b vthis args =
if_string (to_string runs0 s2 c rsep) (fun s3 sep ->
if int_comparable ilen (my_Z_of_nat 0)
then res_ter s3
- (res_val (Coq_value_prim (Coq_prim_string [])))
+ (res_val (Coq_value_prim (Coq_prim_string "")))
else let_binding (valueToStringForJoin runs0 s3 c l 0.)
(fun sR ->
if_spec sR (fun s4 sR0 ->
@@ -5975,7 +5984,7 @@ let run_call_prealloc runs0 s c b vthis args =
push runs0 s2 c l args ilen)))
| Coq_prealloc_string ->
if list_eq_nil_decidable args
- then res_ter s (res_val (Coq_value_prim (Coq_prim_string [])))
+ then res_ter s (res_val (Coq_value_prim (Coq_prim_string "")))
else let_binding (get_arg 0 args) (fun value0 ->
if_string (to_string runs0 s c value0) (fun s0 s1 ->
res_ter s0 (res_val (Coq_value_prim (Coq_prim_string s1)))))
diff --git a/generator/tests/jsref/JsInterpreterMonads.ml b/generator/tests/jsref/JsInterpreterMonads.ml
index 5daaffa..7213fb2 100644
--- a/generator/tests/jsref/JsInterpreterMonads.ml
+++ b/generator/tests/jsref/JsInterpreterMonads.ml
@@ -6,7 +6,7 @@ open LibList
open LibOption
open Shared
-type __ = Obj.t
+type __ = unit
type 't resultof =
| Coq_result_some [@f label0] of 't (** Auto Generated Attributes **)
diff --git a/generator/tests/jsref/JsSyntax.ml b/generator/tests/jsref/JsSyntax.ml
index a1fe142..90952b1 100644
--- a/generator/tests/jsref/JsSyntax.ml
+++ b/generator/tests/jsref/JsSyntax.ml
@@ -574,7 +574,7 @@ type event =
type state = { state_object_heap : (object_loc, coq_object) Heap.heap;
state_env_record_heap : (env_loc, env_record) Heap.heap;
- state_fresh_locations : int stream;
+ state_fresh_locations : int;
state_event_list : event list }
(** val state_object_heap : state -> (object_loc, coq_object) Heap.heap **)
diff --git a/generator/tests/jsref/Prheap.mli b/generator/tests/jsref/Prheap.mli
index d1ade70..47031c0 100644
--- a/generator/tests/jsref/Prheap.mli
+++ b/generator/tests/jsref/Prheap.mli
@@ -1,8 +1,10 @@
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
-*)
\ No newline at end of file
+*)
--
GitLab