XMerge branch 'master' of git+ssh://scm.gforge.inria.fr//gitroot/why3/why3

doc/exec.tex

@@ -92,6 +92,19 @@ For instance, it could be
            -I `why3 --print-libdir`/why3 why3extract.cmxa \
            ...
 \end{verbatim}
+To make the compilation process easier, one can write a
+\texttt{Makefile} which can include informations about Why3
+configuration as follows.
+\begin{whycode}
+WHY3SHARE=$(shell why3 --print-datadir)
+
+include $(WHY3SHARE)/Makefile.config
+
+maxsum:
+        ocamlopt $(INCLUDE) $(BIGINTLIB).cmxa why3extract.cmxa \
+                -o maxsum maxsum__MaxAndSum.ml main.ml
+\end{whycode}
+
 
 
 %%% Local Variables:

examples/in_progress/prover/Makefile

@@ -20,18 +20,22 @@ ifeq ($(BENCH),yes)
 endif
 
 
-MLW=BacktrackArray Firstorder_symbol_impl ISet Firstorder_term_impl \
+MLWUTIL=Nat
+
+MLWTYPES=BacktrackArray Firstorder_symbol_impl ISet Firstorder_term_impl \
 	Firstorder_formula_impl Firstorder_formula_list_impl \
 	Firstorder_tableau_impl Unification FormulaTransformations \
-	Prover ProverMain ProverTest
+	Prover
+
+MLWIMPL=$(MLWTYPES) ProverMain ProverTest
 
 BD=build
-MLUTIL=$(BD)/Nat__Nat
-MLTYPES=$(patsubst %,$(BD)/%__Types,$(MLW))
-MLIMPL=$(patsubst %,$(BD)/%__Impl,$(MLW))
-ML=$(MLUTIL) $(MLTYPES) $(MLIMPL)
-CMX=$(patsubst %,%.cmx,$(ML))
-CMI=$(patsubst %,%.cmi,$(ML))
+MLUTIL=$(patsubst %,$(BD)/%__Nat,$(MLWUTIL))
+MLTYPES=$(patsubst %,$(BD)/%__Types,$(MLWTYPES))
+MLIMPL=$(patsubst %,$(BD)/%__Impl,$(MLWIMPL))
+MLALL=$(MLUTIL) $(MLTYPES) $(MLIMPL)
+ML=$(patsubst %,%.ml,$(MLALL))
+CMX=$(patsubst %,%.cmx,$(MLALL))
 OCAMLC=ocamlopt.opt
 INCLUDES=-I $(BD) $(INCLUDE)
 LIBS=unix.cmxa $(BIGINTLIB).cmxa why3extract.cmxa
@@ -41,34 +45,37 @@ MLFLAGS=
 MLIFLAGS=
 MLEXECFLAGS=
 
+.PHONY: clean depend extract replay
+
 $(BD)/prover: $(CMX) run.cmx
 	$(OCAMLC) $(INCLUDES) $(LIBS) $(MLFLAGS) $(MLEXECFLAGS) \
 		-o $(BD)/prover $^
 
-%.cmx: %.ml
-	$(OCAMLC) $(INCLUDES) $(MLFLAGS) -c $<
-
-$(BD)/Nat__Nat.ml: Nat.mlw
-	why3 $(WHY3FLAGS) extract -D ocaml64 -o $(BD) $< -T Nat
-
-$(BD)/%__Types.ml: %.mlw
-	why3 $(WHY3FLAGS) extract -D ocaml64 -o $(BD) $< -T Types
-
-$(BD)/%__Impl.ml: %.mlw
-	why3 $(WHY3FLAGS) extract -D ocaml64 -o $(BD) $< -T Impl
+extract: $(ML)
 
+$(ML):
+	why3 $(WHY3FLAGS) extract -D ocaml64 -o $(BD) ProverTest.mlw
 
-.PHONY: clean depend
-
-depend: .depend
+%.cmx: %.ml
+	$(OCAMLC) $(INCLUDES) $(MLFLAGS) -c $<
 
-.depend: Makefile $(patsubst %,%.ml,$(ML))
-	ocamldep.opt -I $(BD) $(patsubst %,%.ml,$(ML)) > .depend
+.depend: Makefile $(ML)
+	ocamldep.opt -I $(BD) $(ML) > .depend
 
 ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
+ifneq "$(MAKECMDGOALS:extract%=extract)" "extract"
 include .depend
 endif
+endif
+
+replay:
+	for i in $(MLWUTIL) $(MLWIMPL); do \
+		why3 replay -L . $$i ; \
+	done
+
+depend: .depend
 
 clean:
 	rm -f $(BD)/*.o $(BD)/*.cmi $(BD)/*.cmx
 	rm -f $(BD)/*__*.ml
+	rm -f *~ *.o *.cmi *.cmx build/prover

examples/in_progress/prover/run.ml

@@ -26,7 +26,7 @@ and pr_term_list fmt tl =
   match tl with
   | NL_FONil -> fprintf fmt "()"
   | NL_FOCons(t,tl) ->
-      fprintf fmt "@[(%a%a)@]" pr_term t pr_term_list_tail tl
+      fprintf fmt "@[<hov 2>(%a%a)@]" pr_term t pr_term_list_tail tl
 
 and pr_term_list_tail fmt tl =
   match tl with
@@ -38,21 +38,23 @@ let pr_term_impl fmt t = pr_term fmt t.nlrepr_fo_term_field
 
 let rec pr_formula fmt f =
   match f with
-  | NL_Forall f -> fprintf fmt "@[(forall@ %a)@]" pr_formula f
-  | NL_Exists f  -> fprintf fmt "@[(exists@ %a)@]" pr_formula f
-  | NL_And(f1,f2) -> fprintf fmt "@[(%a@ and %a)@]" pr_formula f1 pr_formula f2
-  | NL_Or(f1,f2) -> fprintf fmt "@[(%a@ or %a)@]" pr_formula f1 pr_formula f2
-  | NL_Not f -> fprintf fmt "@[(not@ %a)@]" pr_formula f
+  | NL_Forall f -> fprintf fmt "@[<hov 2>(forall@ %a)@]" pr_formula f
+  | NL_Exists f  -> fprintf fmt "@[<hov 2>(exists@ %a)@]" pr_formula f
+  | NL_And(f1,f2) ->
+    fprintf fmt "@[<hov 2>(%a@ and %a)@]" pr_formula f1 pr_formula f2
+  | NL_Or(f1,f2) ->
+    fprintf fmt "@[<hov 2>(%a@ or %a)@]" pr_formula f1 pr_formula f2
+  | NL_Not f -> fprintf fmt "@[<hov 2>(not@ %a)@]" pr_formula f
   | NL_FTrue -> fprintf fmt "true"
   | NL_FFalse -> fprintf fmt "false"
   | NL_PApp(s,tl) ->
-    fprintf fmt "@[%a%a@]" pr_symbol s pr_term_list tl
+    fprintf fmt "@[<hov 2>%a%a@]" pr_symbol s pr_term_list tl
 
 and pr_formula_list fmt l =
   match l with
   | NL_FOFNil -> fprintf fmt "[]"
   | NL_FOFCons(f,l) ->
-    fprintf fmt "@[[%a%a]@]" pr_formula f pr_formula_list_tail l
+    fprintf fmt "@[<hov 2>[ %a%a ]@]" pr_formula f pr_formula_list_tail l
 
 and pr_formula_list_tail fmt l =
   match l with
@@ -84,6 +86,20 @@ let () =
   run_test "bidon4" (ProverTest__Impl.bidon4 ());
   run_test "pierce" (ProverTest__Impl.pierce ());
   run_test "zenon5" (ProverTest__Impl.zenon5 ());
-(* too long  run_test "zenon6" (ProverTest__Impl.zenon6 ()); *)
+(* too long -> sat ?
+  run_test "zenon6" (ProverTest__Impl.zenon6 ());
+*)
   run_test "zenon10 2" (ProverTest__Impl.zenon10 (n 2));
-(* too long run_test "zenon10 3" (ProverTest__Impl.zenon10 (n 3)) *)
+(* too long -> sat !
+  run_test "zenon10 3" (ProverTest__Impl.zenon10 (n 3))
+*)
+  run_test "zenon10 4" (ProverTest__Impl.zenon10 (n 4));
+  run_test "zenon10 6" (ProverTest__Impl.zenon10 (n 6));
+  run_test "zenon10 8" (ProverTest__Impl.zenon10 (n 8));
+  run_test "zenon10 10" (ProverTest__Impl.zenon10 (n 10));
+  run_test "zenon10 12" (ProverTest__Impl.zenon10 (n 12));
+(* warning: the following needs around 6 minutes *)
+(*
+  run_test "zenon10 14" (ProverTest__Impl.zenon10 (n 14));
+*)
+  printf "End of tests.@."