Add support for compiler plugins and a use case

.merlin.in

@@ -43,4 +43,4 @@ B plugins/tptp
 B plugins/python
 B lib/why3
 
-PKG str unix num dynlink @ZIPLIB@ @LABLGTK2PKG@ @META_OCAMLGRAPH@
+PKG str unix num dynlink @COMPILERLIBSPKG@ @ZIPLIB@ @LABLGTK2PKG@ @META_OCAMLGRAPH@

Makefile.in

@@ -281,6 +281,16 @@ endif
 src/util/strings.cmo: WARNINGS:=$(WARNINGS)-3
 src/util/strings.cmx: WARNINGS:=$(WARNINGS)-3
 
+# compiler plugins
+
+ifeq (@enable_compiler_plugins@,yes)
+$(LIBCMO) $(LIBCMX): INCLUDES += -I @COMPILERLIBS@
+src/utils/debug_optim.cmxs:
+	$(OCAMLOPT) -I @COMPILERLIBS@ -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
+endif
+
 # 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

configure.in

@@ -340,6 +340,33 @@ else
    OCAMLINSTALLLIB=$OCAMLLIB
 fi
 
+# compiler plugins
+
+AX_VERSION_GE([$OCAMLVERSION], 4.03.0,
+  [if test "$USEOCAMLFIND" = yes; then
+     COMPILERLIBS=$(ocamlfind query compiler-libs)
+   fi
+   if test -n "$COMPILERLIBS"; then
+     echo "ocamlfind found compiler-libs in $COMPILERLIBS"
+     enable_compiler_plugins="yes"
+   else
+     COMPILERLIBS="+compiler-libs"
+     AC_CHECK_FILE($OCAMLLIB/compiler-libs/,
+                   enable_compiler_plugins=yes,
+                   enable_compiler_plugins=no)
+     if test "$enable_compiler_plugins" = no; then
+       reason_compiler_plugins=" (compiler-libs not found)"
+     fi
+   fi],
+  [enable_compiler_plugins="no"
+   reason_compiler_plugins=" (Ocaml version 4.03.0 required)"])
+
+if test "$enable_compiler_plugins" = yes; then
+  COMPILERLIBSPKG="compiler-libs"
+else
+  COMPILERLIBSPKG=
+fi
+
 # checking for rubber
 if test "$enable_doc" = yes ; then
    AC_CHECK_PROG(RUBBER,rubber,rubber,no)
@@ -847,6 +874,10 @@ AC_SUBST(HASJSOFOCAML)
 
 AC_SUBST(META_OCAMLGRAPH)
 
+AC_SUBST(enable_compiler_plugins)
+AC_SUBST(COMPILERLIBS)
+AC_SUBST(COMPILERLIBSPKG)
+
 AC_SUBST(enable_zarith)
 AC_SUBST(BIGINTINCLUDE)
 AC_SUBST(BIGINTLIB)
@@ -938,6 +969,7 @@ echo "    Version                 : $OCAMLVERSION"
 echo "    Library path            : $OCAMLLIB"
 echo "    Native compilation      : $enable_native_code"
 echo "    Profiling               : $enable_profiling"
+echo "    Compiler plugins        : $enable_compiler_plugins$reason_compiler_plugins"
 echo "Components"
 echo "    Why3 library            : $enable_why3_lib"
 echo "    GTK IDE                 : $enable_ide$reason_ide"

src/util/debug_optim.ml

+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