create source directory for plugins and build them

Makefile.in

@@ -91,7 +91,7 @@ EXTCMXA = $(addsuffix .cmxa,$(EXTLIBS)) $(addsuffix .cmx,$(EXTOBJS))
 # main target
 ###############
 
-all: @OCAMLBEST@
+all: @OCAMLBEST@ plugins
 
 ifeq (@enable_local@,yes)
 all: install_local
@@ -133,7 +133,7 @@ LIB_TRANSFORM = simplify_recursive_definition simplify_formula \
 		introduction abstraction close_epsilon lift_epsilon \
 		eval_match instantiate_predicate smoke_detector
 
-LIB_PRINTER = alt_ergo why3printer smtv1 smtv2 coq tptp simplify gappa \
+LIB_PRINTER = alt_ergo why3printer smtv1 smtv2 coq simplify gappa \
 	      cvc3 yices
 
 LIBMODULES = src/config \
@@ -208,7 +208,6 @@ clean::
 
 install_no_local::
 	mkdir -p $(BINDIR)
-	mkdir -p $(LIBDIR)/why3/plugins
 	mkdir -p $(LIBDIR)/why3/coq
 	mkdir -p $(DATADIR)/why3/images
 	mkdir -p $(DATADIR)/why3/emacs
@@ -242,6 +241,84 @@ endif
 
 install-all: install install-lib
 
+##################
+# Why plugins
+##################
+
+PLUGGENERATED =
+
+PLUG_PARSER = genequlin
+PLUG_PRINTER = tptp
+PLUG_TRANSFORM =
+
+PLUGINS = genequlin tptp
+
+PLUGMODULES = $(addprefix plugins/parser/, $(PLUG_PARSER)) \
+	      $(addprefix plugins/printer/, $(PLUG_PRINTER)) \
+	      $(addprefix plugins/transform/, $(PLUG_TRANSFORM))
+
+PLUGML  = $(addsuffix .ml,  $(PLUGMODULES))
+PLUGMLI = $(addsuffix .mli, $(PLUGMODULES))
+PLUGCMO = $(addsuffix .cmo, $(PLUGMODULES))
+PLUGCMX = $(addsuffix .cmx, $(PLUGMODULES))
+
+PLUGDIRS = parser printer transform
+PLUGINCLUDES = $(addprefix -I plugins/, $(PLUGDIRS))
+
+$(PLUGCMO) $(PLUGCMX): INCLUDES += $(PLUGINCLUDES)
+
+plugins.byte: $(addsuffix .cmo, $(addprefix lib/plugins/, $(PLUGINS)))
+plugins.opt : $(addsuffix .cmxs, $(addprefix lib/plugins/, $(PLUGINS)))
+
+lib/plugins/%.cmxs: plugins/parser/%.cmx
+	$(if $(QUIET), @echo 'Linking  $@' &&) \
+	    $(OCAMLOPT) $(OFLAGS) -shared -o $@ $<
+
+lib/plugins/%.cmo: plugins/parser/%.cmo
+	$(if $(QUIET),@echo 'Linking  $@' &&) \
+	    $(OCAMLC) $(BFLAGS) -pack -o $@ $<
+
+lib/plugins/%.cmxs: plugins/printer/%.cmx
+	$(if $(QUIET), @echo 'Linking  $@' &&) \
+	    $(OCAMLOPT) $(OFLAGS) -shared -o $@ $<
+
+lib/plugins/%.cmo: plugins/printer/%.cmo
+	$(if $(QUIET),@echo 'Linking  $@' &&) \
+	    $(OCAMLC) $(BFLAGS) -pack -o $@ $<
+
+lib/plugins/%.cmxs: plugins/transform/%.cmx
+	$(if $(QUIET), @echo 'Linking  $@' &&) \
+	    $(OCAMLOPT) $(OFLAGS) -shared -o $@ $<
+
+lib/plugins/%.cmo: plugins/transform/%.cmo
+	$(if $(QUIET),@echo 'Linking  $@' &&) \
+	    $(OCAMLC) $(BFLAGS) -pack -o $@ $<
+
+include .depend.plugins
+
+.depend.plugins: $(PLUGGENERATED)
+	$(OCAMLDEP) -slash -I src -I plugins $(PLUGINCLUDES) \
+		$(PLUGML) $(PLUGMLI) > $@
+
+depend: .depend.plugins
+
+PLUGSDIRS = plugins $(addprefix plugins/, $(PLUGDIRS))
+PLUGCLEAN = $(addsuffix /*.cm[iox], $(PLUGSDIRS)) \
+	    $(addsuffix /*.annot, $(PLUGSDIRS)) \
+	    $(addsuffix /*.output, $(PLUGSDIRS)) \
+	    $(addsuffix /*.automaton, $(PLUGSDIRS)) \
+	    $(addsuffix /*.o, $(PLUGSDIRS)) \
+	    $(addsuffix /*~, $(PLUGSDIRS))
+
+clean::
+	rm -f $(PLUGCLEAN) $(PLUGGENERATED)
+	rm -f lib/plugins/*
+	rm -f .depend.plugins
+
+install_no_local::
+	mkdir -p $(LIBDIR)/why3/plugins
+	cp -f lib/plugins/* $(LIBDIR)/why3/plugins
+
 
 ##################
 # Why binary
@@ -443,7 +520,6 @@ clean::
 	rm -f src/config/*.annot src/config/*~
 	rm -f src/config/*.output src/config/*.automaton
 	rm -f bin/why3config.byte bin/why3config.opt bin/why3config
-	rm -f .why.conf
 	rm -f .depend.config
 
 local_config: bin/why3config.@OCAMLBEST@
@@ -922,7 +998,7 @@ install_local: bin/why3doc
 # bench
 ########
 
-.PHONY: bench test comp_bench_plugins
+.PHONY: bench test
 
 bench:: bin/why3.@OCAMLBEST@ bin/why3ml.@OCAMLBEST@ bin/why3config.@OCAMLBEST@ plugins $(TOOLS)
 	$(MAKE) test-api
@@ -930,18 +1006,6 @@ bench:: bin/why3.@OCAMLBEST@ bin/why3ml.@OCAMLBEST@ bin/why3config.@OCAMLBEST@ p
 	    "bin/why3.@OCAMLBEST@" \
 	    "bin/why3ml.@OCAMLBEST@"
 
-BENCH_PLUGINS_CMO := helloworld.cmo
-BENCH_PLUGINS_CMO := $(addprefix bench/plugins/,$(BENCH_PLUGINS_CMO))
-BENCH_PLUGINS_CMXS := $(BENCH_PLUGINS_CMO:.cmo=.cmxs)
-
-comp_bench_plugins:: $(BENCH_PLUGINS_CMO) $(BENCH_PLUGINS_CMXS)
-
-# bench_plugins:: $(BENCH_PLUGINS_CMO) $(BENCH_PLUGINS_CMXS) byte $(TOOLS)
-# 	bin/why3.byte -D bench/plugins/helloworld.drv \
-# 	tests/test-jcf.why -T Test -G G
-# 	bin/why3.$(OCAMLBEST) -D bench/plugins/helloworld.drv  \
-# 	tests/test-jcf.why -T Test -G G
-
 ###############
 # test targets
 ###############
@@ -992,47 +1056,6 @@ bts12244: src/why3.cma
 	ocaml -I src/ $(INCLUDES) $(EXTCMA) src/why3.cma examples/bts12244.ml
 
 
-## Examples : Plugins ##
-
-PLUGDIR = examples/plugins/
-PLUG_FILES = genequlin
-
-PLUGMODULES = $(addprefix $(PLUGDIR), $(PLUG_FILES))
-
-PLUGML  = $(addsuffix .ml,  $(PLUGMODULES))
-PLUGCMO = $(addsuffix .cmo, $(PLUGMODULES))
-PLUGCMX = $(addsuffix .cmx, $(PLUGMODULES))
-PLUGCMXS = $(addsuffix .cmxs, $(PLUGMODULES))
-
-# ifeq (@enable_plug_support@,yes)
-# byte: src/plug-plugin/whytac.cma
-# opt:  src/plug-plugin/whytac.cmxs
-# endif
-
-# $(PLUGCMO):  src/why3.cma
-# $(PLUGCMXS): src/why3.cmxa
-
-.PHONY: examples_plugins.byte examples_plugins.opt
-
-examples_plugins.byte : $(PLUGCMO)
-examples_plugins.opt : $(PLUGCMXS)
-
-# depend and clean targets
-
-include .depend.plug
-
-.depend.plug: $(PLUGGENERATED)
-	$(OCAMLDEP) -slash -I src -I $(PLUGDIR) $(PLUGML) | sed "s/cmx/cmxs/" > $@
-
-depend: .depend.plug
-
-clean::
-	rm -f $(PLUGDIR)/*.cm[iox] $(PLUGDIR)/*.o
-	rm -f $(PLUGDIR)/*.cma $(PLUGDIR)/*.cmxs
-	rm -f $(PLUGDIR)/*.annot $(PLUGDIR)/*~
-	rm -f $(PLUGGENERATED)
-	rm -f .depend.plug
-
 ################
 # documentation
 ################

examples/plugins/genequlin.ml → plugins/parser/genequlin.ml

@@ -68,7 +68,7 @@ let scanf s =
 
 
 (** the main function *)
-let read_channel env filename cin =
+let read_channel env path filename cin =
   (** Find the int theory and the needed operation *)
   let th_int = Env.find_theory env ["int"] "Int" in
   let leq = ns_find_ls th_int.th_export ["infix <"] in
@@ -76,17 +76,17 @@ let read_channel env filename cin =
   let mult_symbol = Theory.ns_find_ls th_int.Theory.th_export ["infix *"] in
 
 
-  let zero = t_const (ConstInt "0") in
+  let zero = t_int_const "0" in
 
   (** create a contraint : polynome <= constant *)
   let create_lit lvar k lits _ =
     let left = List.fold_left (fun acc e ->
       let const = string_of_int ((Random.int k) - (k/2)) in
-      let monome = t_app mult_symbol [e;t_const(ConstInt const)]
+      let monome = t_app mult_symbol [e;t_int_const const]
         (Some Ty.ty_int) in
       t_app plus_symbol [acc;monome] (Some Ty.ty_int)) zero lvar in
     let rconst = string_of_int ((Random.int k) - (k/2)) in
-    t_and_simp lits (t_app leq [left;t_const(ConstInt rconst)] None) in
+    t_and_simp lits (t_app leq [left;t_int_const rconst] None) in
 
   (** create a set of constraints *)
   let create_fmla nvar m k =
@@ -107,7 +107,7 @@ let read_channel env filename cin =
   end;
   (** Create the theory *)
   let th_uc_loc = Loc.user_position filename 1 0 0 in
-  let th_uc = create_theory (id_user "EqLin" th_uc_loc) in
+  let th_uc = create_theory ~path (id_user "EqLin" th_uc_loc) in
   let th_uc = Theory.use_export th_uc th_int in
   (** Read one line and add it to the theory *)
   let fold th_uc s =
@@ -130,6 +130,4 @@ let read_channel env filename cin =
   (** Return the map with the theory *)
   Mstr.singleton "EqLin" (close_theory th_uc)
 
-
-
 let () = Env.register_format "EquLin" ["equlin"] read_channel

src/printer/tptp.ml → plugins/printer/tptp.ml

@@ -18,6 +18,8 @@
 (**************************************************************************)
 
 open Format
+
+open Why3
 open Pp
 open Ident
 open Ty