From 6570e52bf969a8f8f9cc484cc901907b06eadc49 Mon Sep 17 00:00:00 2001
From: charguer <arthur@chargueraud.org>
Date: Tue, 5 Apr 2016 20:35:22 +0200
Subject: [PATCH] ppx
---
generator/Makefile | 19 ++++++--
generator/_tags | 1 +
generator/js_of_ast.ml | 2 +-
generator/main.ml | 10 ++++
generator/monad_ppx.ml | 65 ++++++++++++++++++++++++++
generator/parse_type.ml | 6 ++-
generator/tests/jsref/JsInterpreter.ml | 3 +-
7 files changed, 100 insertions(+), 6 deletions(-)
create mode 100644 generator/monad_ppx.ml
diff --git a/generator/Makefile b/generator/Makefile
index 241fabe..c50ea4b 100644
--- a/generator/Makefile
+++ b/generator/Makefile
@@ -88,7 +88,10 @@ OCAMLBUILD := ocamlbuild -j 4 -classic-display -use-ocamlfind -X tests -X $(STDL
OCAMLPAR := OCAMLRUNPARAM="l=200M"
LINEOF := $(OCAMLPAR) ./lineof.byte
-MLTOJS := $(OCAMLPAR) ./main.byte
+MLTOJS := $(OCAMLPAR) ./main.byte -ppx ./monad_ppx.native
+# -dsource is automatically considered by main.byte
+
+
DISPLAYGEN := $(OCAMLPAR) ./displayed_sources.byte
###############################################################
@@ -103,14 +106,24 @@ endif
###############################################################
# Rules
+
+
##### Compilation of STDLIB
$(STDLIB_DIR)/stdlib.cmi: $(STDLIB_DIR)/stdlib.mli
$(CC) $<
+##### Rule for parser extension
+
+monad_ppx.native: monad_ppx.ml
+ $(OCAMLBUILD) $@
+
+#ocamlfind ocamlc -linkpkg -o $@ $<
+# -package compiler-libs.common
+
##### Rule for binaries
-%.byte: *.ml _tags
+%.byte: *.ml _tags monad_ppx.native
$(OCAMLBUILD) $@
##### Rule for dependencies
@@ -121,7 +134,7 @@ $(JSREF_PATH)/.depends: $(JSREF_ML)
##### Rule for cmi
tests/%.cmi: tests/%.ml main.byte stdlib
- ./main.byte -mode cmi -I $(<D) $<
+ $(MLTOJS) -mode cmi -I $(<D) $<
tests/%.cmi: tests/%.mli stdlib
ocamlc -I $(JSREF_PATH) -I stdlib_ml -open Stdlib $<
diff --git a/generator/_tags b/generator/_tags
index 1b53152..ea720ef 100644
--- a/generator/_tags
+++ b/generator/_tags
@@ -6,6 +6,7 @@ true: bin_annot
<parsing>: include
<typing>: include
<utils>: include
+<driver>: include
# <tests>: precious
# <stdlib_ml>: precious
diff --git a/generator/js_of_ast.ml b/generator/js_of_ast.ml
index e5de477..3e016d0 100644
--- a/generator/js_of_ast.ml
+++ b/generator/js_of_ast.ml
@@ -881,7 +881,7 @@ and js_of_path_longident path ident =
(* for string *)
| "^" -> "+" (* !!TODO: we want to claim ability to type our sublanguage, so we should not use this *)
| res ->
- let res = if !generate_qualified_names && (Path.head path).name <> "Stdlib"
+ let res = if !generate_qualified_names && (Path.head path).Ident.name <> "Stdlib"
then ppf_path path else res in
ppf_ident_name res
diff --git a/generator/main.ml b/generator/main.ml
index df98a07..d60b1a7 100644
--- a/generator/main.ml
+++ b/generator/main.ml
@@ -20,6 +20,10 @@ let outputfile = ref None
(*#########################################################################*)
+let add_to_list li s =
+ li := s :: !li
+
+
let _ =
(*---------------------------------------------------*)
(* parsing of command line *)
@@ -30,10 +34,16 @@ let _ =
"includes a directory where to look for interface files");
("-o", Arg.String (fun s -> outputfile := Some s), "set the output file name");
("-debug", Arg.Set debug, "trace the various steps");
+ ("-ppx", Arg.String (add_to_list Clflags.all_ppx (* TODO Compenv.first_ppx *) ), "load ppx");
("-mode", Arg.String (fun s -> set_current_mode s), "current mode: unlog, log, or token")
]
(fun f -> files := f :: !files)
("usage: [-I dir] [..other options..] file.ml");
+
+ (* force: -dsource *)
+ Clflags.dump_source := true;
+
+
files := List.rev !files;
if List.length !files <> 1 then
failwith "Expects one argument: the filename of the ML source file";
diff --git a/generator/monad_ppx.ml b/generator/monad_ppx.ml
new file mode 100644
index 0000000..4795795
--- /dev/null
+++ b/generator/monad_ppx.ml
@@ -0,0 +1,65 @@
+open Ast_mapper
+open Ast_helper
+open Asttypes
+open Parsetree
+open Longident
+
+let monad_mapping =
+ [("spec", "if_spec");
+ (*("success", "ifsuccess")*)
+ ]
+
+(* e.g.
+
+ let%some x = expr in cont
+becomes
+ if_some expr (fun x -> cont)
+
+ let%if_spec (s,x) = expr in cont
+becomes
+ if_spec expr (fun s x -> cont)
+
+ *)
+
+
+
+let generate_mapper namesid = function argv ->
+ { default_mapper with
+ expr = fun mapper expr ->
+ match expr with
+ (* Is this an extension node? *)
+ | { pexp_desc =
+ (* Should have name "getenv". *)
+ Pexp_extension ({ txt = name; loc }, pstr)} ->
+ begin
+ try
+ let ident = List.assoc name namesid in
+ match pstr with
+ | PStr [{ pstr_desc =
+ Pstr_eval ({ pexp_loc = loc;
+ pexp_desc = Pexp_let
+ (rf,
+ [{pvb_pat =
+ {ppat_desc =
+ Ppat_tuple [p1;p2]};
+ pvb_expr = e}],
+ cont)
+ }, _)}] ->
+ Exp.apply ~loc (Exp.ident
+ (Location.mkloc
+ (Longident.Lident ident) Location.none))
+ [("", e);
+ ("", Exp.fun_ "" None p1 (Exp.fun_ "" None p2 cont))]
+ | _ ->
+ raise (Location.Error (
+ Location.error ~loc ("error with let%"^name)))
+ with
+ | Not_found ->
+ raise (Location.Error (
+ Location.error ~loc ("no let%"^name)))
+ end
+ (* Delegate to the default mapper. *)
+ | x -> default_mapper.expr mapper x;
+ }
+
+let () = register "my_monads" (generate_mapper monad_mapping)
diff --git a/generator/parse_type.ml b/generator/parse_type.ml
index fb16208..71a81c9 100644
--- a/generator/parse_type.ml
+++ b/generator/parse_type.ml
@@ -88,7 +88,9 @@ let parse_file inputfile parse_fun ast_magic =
with x -> close_in ic; raise x
in
close_in ic;
- ast
+ (* was: ast *)
+ Pparse.apply_rewriters ~restore:false ~tool_name:"ok" ast_magic ast
+
(** Analysis of an implementation file. Returns (Some typedtree) if
@@ -103,6 +105,8 @@ let process_implementation_file ppf sourcefile =
try
let env = initial_env () in
let parsetree = parse_file inputfile Parse.implementation ast_impl_magic_number in
+
+
let typedtree = Typemod.type_implementation sourcefile prefixname modulename env parsetree in
(Some (parsetree, typedtree), inputfile, modulename)
with
diff --git a/generator/tests/jsref/JsInterpreter.ml b/generator/tests/jsref/JsInterpreter.ml
index fc2f6f0..153775e 100644
--- a/generator/tests/jsref/JsInterpreter.ml
+++ b/generator/tests/jsref/JsInterpreter.ml
@@ -2791,7 +2791,8 @@ match _foo_ with
and run_binary_op s c op v1 v2 =
if binary_op_comparable op Coq_binary_op_add
- then if_spec (convert_twice_primitive s c v1 v2) (fun s1 ww ->
+ then (* if_spec (convert_twice_primitive s c v1 v2) (fun s1 ww ->*)
+ (let%spec (s1,ww) = convert_twice_primitive s c v1 v2 in
let (w1, w2) = ww in
if or_decidable
(type_comparable (type_of (Coq_value_prim w1)) Coq_type_string)
--
GitLab