Commit 7b1be96e authored by Raphael Rieu-Helft's avatar Raphael Rieu-Helft

Revert "Use a compiler plugin to optimize Debug.dprintf calls in reification"

This reverts commit 9629e273.
parent 9629e273
......@@ -43,4 +43,4 @@ B plugins/tptp
B plugins/python
B lib/why3
PKG str unix num dynlink compiler-libs @ZIPLIB@ @LABLGTK2PKG@ @META_OCAMLGRAPH@
PKG str unix num dynlink @ZIPLIB@ @LABLGTK2PKG@ @META_OCAMLGRAPH@
......@@ -251,7 +251,7 @@ LIBCMO = $(addsuffix .cmo, $(LIBMODULES))
LIBCMX = $(addsuffix .cmx, $(LIBMODULES))
$(LIBDEP): DEPFLAGS += $(LIBINCLUDES)
$(LIBCMO) $(LIBCMX): INCLUDES += $(LIBINCLUDES) -I +compiler-libs
$(LIBCMO) $(LIBCMX): INCLUDES += $(LIBINCLUDES)
$(LIBCMX): OFLAGS += -for-pack Why3
$(LIBDEP): $(LIBGENERATED)
......@@ -281,14 +281,6 @@ endif
src/util/strings.cmo: WARNINGS:=$(WARNINGS)-3
src/util/strings.cmx: WARNINGS:=$(WARNINGS)-3
# debug optimization
src/utils/debug_optim.cmxs:
ocamlopt -I +compiler-libs -for-pack Why3 -shared src/util/debug_optim.ml -o src/util/debug_optim.cmxs
src/transform/reification.cmx: src/utils/debug_optim.cmxs
src/transform/reification.cmx: OFLAGS += -plugin debug_optim.cmxs
# hide warning 'no cmx file was found in path for module ..., and its interface was not compiled with -opaque' for the coq tactic
src/coq-tactic/why3tac.cmx: WARNINGS:=$(WARNINGS)-58
......
open Parsetree
open Ast_mapper
open Asttypes
open Longident
let ast_mapper =
{ Ast_mapper.default_mapper with
expr = fun mapper expr ->
match expr with
| { pexp_desc =
Pexp_apply ({ pexp_desc =
Pexp_ident { txt = Ldot (Lident "Debug", "dprintf")}},
flag :: _args) } as app ->
let open Ast_helper in
Exp.ifthenelse
(Exp.apply
(Exp.ident { txt = Ldot (Lident "Debug", "test_flag");
loc = Location.none (*TODO*) })
[flag])
app
None
| other -> default_mapper.expr mapper other; }
let transform _hook_info structure =
ast_mapper.structure ast_mapper structure
let () = Pparse.ImplementationHooks.add_hook "Debug hook" transform
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment