plus_loin_dans_le_makefile

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 $<
 
 
 

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"

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

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"
+

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

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 ->

generator/tests/jsref/Prheap.mli

+
+  val prstate : bool -> JsSyntax.state -> string
+  val string_of_char_list : string -> string
+
+(*
+module Prheap : sig
+end
+*)
\ No newline at end of file