From 476db215600506479f0175e9725d8327cae2e74c Mon Sep 17 00:00:00 2001
From: charguer <arthur@chargueraud.org>
Date: Tue, 22 Dec 2015 16:04:56 +0100
Subject: [PATCH] plus_loin_dans_le_makefile
---
generator/Makefile | 24 ++++++++++++--------
generator/js_of_ast.ml | 4 +++-
generator/main.ml | 22 ++++++++++++------
generator/params.ml | 3 +++
generator/stdlib_ml/stdlib.mli | 5 ----
generator/tests/jsref/JsInterpreterMonads.ml | 6 ++---
generator/tests/jsref/Prheap.mli | 8 +++++++
7 files changed, 47 insertions(+), 25 deletions(-)
create mode 100644 generator/tests/jsref/Prheap.mli
diff --git a/generator/Makefile b/generator/Makefile
index 3726e66..cec7158 100644
--- a/generator/Makefile
+++ b/generator/Makefile
@@ -59,31 +59,37 @@ tests/%.mli.d: tests/%.mli
tests/%.ml.d: tests/%.ml
$(OCAMLDEP) -I $(<D) $< | $(DEPSED) > $@
+tests/%.cmi: tests/%.ml main.byte stdlib
+ ./main.byte -mode cmi -I $(<D) $<
+
tests/%.log.js: tests/%.ml main.byte stdlib tests/%.cmi
./main.byte -mode log -I $(<D) $<
-tests/%.unlog.js: tests/%.ml main.byte stdlib
+tests/%.unlog.js: tests/%.ml main.byte stdlib tests/%.cmi
./main.byte -mode unlog -I $(<D) $<
-tests/%.token.js: tests/%.ml main.byte stdlib
+tests/%.token.js: tests/%.ml main.byte stdlib tests/%.cmi
./main.byte -mode token -I $(<D) $<
+#tests/%.cmi: tests/%.ml main.byte stdlib
+# ./main.byte -mode unlog -I $(<D) $<
--include tests/jsref/BinNat.ml.d
-tests/%.cmi: tests/%.ml main.byte stdlib
- ./main.byte -mode log -I $(<D) $<
+# ad hoc rules
+
+tests/jsref/Translate_syntax.cmi: tests/jsref/Translate_syntax.mli stdlib
+ ocamlc -I tests/jsref -I stdlib_ml -open Stdlib $<
+
+tests/jsref/Prheap.cmi: tests/jsref/Prheap.mli stdlib tests/jsref/JsSyntax.cmi
+ ocamlc -I tests/jsref -I stdlib_ml -open Stdlib $<
+
-tests/%.cmi: tests/%.ml main.byte stdlib
- ./main.byte -mode unlog -I $(<D) $<
-tests/jsref/Translate_syntax.cmi: tests/jsref/Translate_syntax.mli stdlib
- ocamlc -I tests/jsref -I stdlib_ml -open Stdlib $<
diff --git a/generator/js_of_ast.ml b/generator/js_of_ast.ml
index 26a09ce..b9ecb2e 100644
--- a/generator/js_of_ast.ml
+++ b/generator/js_of_ast.ml
@@ -604,6 +604,9 @@ and js_of_expression ctx dest e =
(* ppf_for (ppf_ident id) (js_of_expression st) (js_of_expression ed) fl (js_of_expression body) *)
| Texp_record (llde,_) -> ppf_record (List.map (fun (_, lbl, exp) -> (lbl.lbl_name, inline_of_wrap exp)) llde)
| Texp_field (exp, _, lbl) -> ppf_field_access (inline_of_wrap exp) lbl.lbl_name
+ | Texp_assert e ->
+ let sexp = inline_of_wrap e in
+ Printf.sprintf "throw %s;" sexp
| Texp_match (_,_,_, Partial) -> out_of_scope loc "partial matching"
| Texp_match (_,_,_,_) -> out_of_scope loc "matching with exception branches"
@@ -617,7 +620,6 @@ and js_of_expression ctx dest e =
| Texp_setinstvar (_,_,_,_) -> out_of_scope loc "objects"
| Texp_override (_,_) -> out_of_scope loc "objects"
| Texp_letmodule (_,_,_,_) -> out_of_scope loc "local modules"
- | Texp_assert _ -> out_of_scope loc "assert"
| Texp_lazy _ -> out_of_scope loc "lazy expressions"
| Texp_object (_,_) -> out_of_scope loc "objects"
| Texp_pack _ -> out_of_scope loc "packing"
diff --git a/generator/main.ml b/generator/main.ml
index 04702cd..1428451 100644
--- a/generator/main.ml
+++ b/generator/main.ml
@@ -42,8 +42,12 @@ let _ =
| Some f -> f ^ ".log.js", f ^ ".unlog.js", f ^ ".token.js"
in
+ if !current_mode <> Mode_cmi
+ then Clflags.dont_write_files := true;
+
(*---------------------------------------------------*)
(* "reading and typing source file" *)
+
let (opt, _, module_name) = process_implementation_file ppf sourcefile in
let ((parsetree1 : Parsetree.structure), typedtree1) =
match opt with
@@ -51,10 +55,14 @@ let _ =
| Some (parsetree1, (typedtree1,_)) -> parsetree1, typedtree1
in
- let out = Js_of_ast.to_javascript basename module_name typedtree1 in
- let output_filename = match !current_mode with
- | Mode_unlogged -> unlog_output
- | Mode_logged -> log_output
- | Mode_line_token -> token_output
- in
- file_put_contents output_filename out
+ match !current_mode with
+ | Mode_cmi -> Printf.printf "wrote cmi file\n"
+ | _ ->
+ let out = Js_of_ast.to_javascript basename module_name typedtree1 in
+ let output_filename = match !current_mode with
+ | Mode_unlogged -> unlog_output
+ | Mode_logged -> log_output
+ | Mode_line_token -> token_output
+ in
+ file_put_contents output_filename out;
+ Printf.printf "wrote %s\n" output_filename
diff --git a/generator/params.ml b/generator/params.ml
index c5f42b8..f2b2a76 100644
--- a/generator/params.ml
+++ b/generator/params.ml
@@ -7,12 +7,15 @@ type generate_mode =
| Mode_unlogged
| Mode_line_token
| Mode_logged
+ | Mode_cmi
let current_mode = ref Mode_unlogged
let set_current_mode s =
current_mode := match s with
+ | "cmi" -> Mode_cmi
| "log" -> Mode_logged
| "unlog" -> Mode_unlogged
| "token" -> Mode_line_token
| _ -> failwith "Invalid mode, chose log, unlog, or token"
+
diff --git a/generator/stdlib_ml/stdlib.mli b/generator/stdlib_ml/stdlib.mli
index d430fc0..1f33fce 100644
--- a/generator/stdlib_ml/stdlib.mli
+++ b/generator/stdlib_ml/stdlib.mli
@@ -138,8 +138,3 @@ end
val print_endline : string -> unit
val __LOC__ : string
-
-module Prheap : sig
- val prstate : bool -> string -> string
- val string_of_char_list : string -> string
-end
\ No newline at end of file
diff --git a/generator/tests/jsref/JsInterpreterMonads.ml b/generator/tests/jsref/JsInterpreterMonads.ml
index 9e7c9fc..5daaffa 100644
--- a/generator/tests/jsref/JsInterpreterMonads.ml
+++ b/generator/tests/jsref/JsInterpreterMonads.ml
@@ -76,10 +76,10 @@ let destr_list l d f =
(** val if_empty_label :
state -> res -> (unit -> 'a1 resultof) -> 'a1 resultof **)
-let if_empty_label s r k =
+let if_empty_label (s:state) r k =
if label_comparable r.res_label Coq_label_empty
then k ()
- else (fun s message ->
+ else (fun (s:state) message ->
print_endline (__LOC__ ^ ": Stuck!\nState: " ^ Prheap.prstate true s
^ "\nMessage:\t" ^ Prheap.string_of_char_list message) ;
Coq_result_impossible)
@@ -134,7 +134,7 @@ let if_ter w k =
resvalue -> result -> (state -> resvalue -> result) -> result **)
let if_success_state rv w k =
- if_ter w (fun s0 r ->
+ if_ter w (fun (s0:state) r ->
match r.res_type with
| Coq_restype_normal ->
if_empty_label s0 r (fun x ->
diff --git a/generator/tests/jsref/Prheap.mli b/generator/tests/jsref/Prheap.mli
new file mode 100644
index 0000000..d1ade70
--- /dev/null
+++ b/generator/tests/jsref/Prheap.mli
@@ -0,0 +1,8 @@
+
+ val prstate : bool -> JsSyntax.state -> string
+ val string_of_char_list : string -> string
+
+(*
+module Prheap : sig
+end
+*)
\ No newline at end of file
--
GitLab