Move list of realized theories to a generated file: src/coq_config.ml

Moreover,
- Coq realizations are disabled for Coq < 8.3 due to coqdep bugs,
- Whyconf.magicnumber is incremented to ensure coqc and coqide are called
  with -R,
- realizations for FP arithmetic are disabled if Flocq is missing.

.gitignore

@@ -115,6 +115,7 @@ why3.conf
 # /src/
 /src/config.sh
 /src/config.ml
+/src/coq_config.ml
 /src/*.cma
 /src/*.cmxa
 /src/*.a

Makefile.in

@@ -112,7 +112,7 @@ plugins: plugins.@OCAMLBEST@
 LIBGENERATED = src/util/rc.ml src/parser/lexer.ml \
 	       src/parser/parser.mli src/parser/parser.ml \
 	       src/driver/driver_parser.mli src/driver/driver_parser.ml \
-	       src/driver/driver_lexer.ml
+	       src/driver/driver_lexer.ml src/coq_config.ml
 
 LIB_UTIL = stdlib exn_printer debug pp loc print_tree print_number \
 	   cmdline hashweak hashcons util sysutil rc plugin
@@ -139,7 +139,7 @@ LIB_TRANSFORM = simplify_recursive_definition simplify_formula \
 LIB_PRINTER = alt_ergo why3printer smtv1 smtv2 coq simplify gappa \
 	      cvc3 yices
 
-LIBMODULES = src/config \
+LIBMODULES = src/config src/coq_config \
 	      $(addprefix src/util/, $(LIB_UTIL)) \
 	      $(addprefix src/core/, $(LIB_CORE)) \
 	      $(addprefix src/parser/, $(LIB_PARSER)) \
@@ -845,8 +845,11 @@ COQLIBS_INT = $(addprefix lib/coq/int/, $(COQLIBS_INT_FILES))
 COQLIBS_REAL_FILES = Abs FromInt MinMax Real Square
 COQLIBS_REAL = $(addprefix lib/coq/real/, $(COQLIBS_REAL_FILES))
 
-COQLIBS_FP_FILES = Rounding GenFloat Single Double
-COQLIBS_FP = $(addprefix lib/coq/floating_point/, $(COQLIBS_FP_FILES))
+ifeq (@enable_coq_fp_libs@,yes)
+COQLIBS_FP_FILES = Rounding Single Double
+COQLIBS_FP_ALL_FILES = GenFloat $(COQLIBS_FP_FILES)
+COQLIBS_FP = $(addprefix lib/coq/floating_point/, $(COQLIBS_FP_ALL_FILES))
+endif
 
 COQLIBS_FILES = $(COQLIBS_INT) $(COQLIBS_REAL) $(COQLIBS_FP)
 
@@ -856,16 +859,27 @@ COQVO = $(addsuffix .vo, $(COQLIBS_FILES))
 %.vo: %.v
 	$(COQC) -R lib/coq Why3 $<
 
+src/coq_config.ml:
+	echo "let realized_theories = [" > $@
+	for f in $(COQLIBS_INT_FILES); do echo '  ["int"; "'"$$f"'"];'; done >> $@
+	for f in $(COQLIBS_REAL_FILES); do echo '  ["real"; "'"$$f"'"];'; done >> $@
+ifeq (@enable_coq_fp_libs@,yes)
+	for f in $(COQLIBS_FP_FILES); do echo '  ["floating_point"; "'"$$f"'"];'; done >> $@
+endif
+	echo "]" >> $@
+
 all: $(COQVO)
 
 install_no_local::
 	mkdir -p $(LIBDIR)/why3/coq
 	mkdir -p $(LIBDIR)/why3/coq/int
-	mkdir -p $(LIBDIR)/why3/coq/real
-	mkdir -p $(LIBDIR)/why3/coq/floating_point
 	cp $(addsuffix .vo, $(COQLIBS_INT)) $(LIBDIR)/why3/coq/int/
+	mkdir -p $(LIBDIR)/why3/coq/real
 	cp $(addsuffix .vo, $(COQLIBS_REAL)) $(LIBDIR)/why3/coq/real/
+ifeq (@enable_coq_fp_libs@,yes)
+	mkdir -p $(LIBDIR)/why3/coq/floating_point
 	cp $(addsuffix .vo, $(COQLIBS_FP)) $(LIBDIR)/why3/coq/floating_point/
+endif
 
 install_local: $(COQVO)
 
@@ -880,6 +894,11 @@ clean::
 	rm -f $COQVO $(addsuffix .glob, $(COQLIBS_FILES))
 	rm -f .depend.coq-libs
 
+else
+
+src/coq_config.ml:
+	echo "let realized_theories = []" > $@
+
 endif
 
 ########

configure.in

@@ -367,6 +367,8 @@ dnl AC_CHECK_PROG(OCAMLWEB,ocamlweb,ocamlweb,true)
 
 # Coq
 
+enable_coq_fp_libs=yes
+
 if test "$enable_coq_plugins" = no -a "$enable_coq_libs" = no; then
     enable_coq_support=no
     AC_MSG_WARN(coq support disabled)
@@ -383,14 +385,19 @@ else
         COQVERSION=`$COQC -v | sed -n -e 's|.*version* *\([[^ ]]*\) .*$|\1|p' `
 
         case $COQVERSION in
+          8.0*|8.1*|8.2*)
+                enable_coq_support=no
+                AC_MSG_WARN(You need Coq 8.3 or later; Coq discarded)
+                reason_coq_support=" (need version 8.3 or later)"
+                ;;
           8.*|trunk)
 	        enable_coq_support=yes
                 AC_MSG_RESULT($COQVERSION)
                 ;;
           *)
                 enable_coq_support=no
-	        AC_MSG_WARN(You need Coq 8.x or later; Coq discarded)
-                reason_coq_support=" (need version 8.x or later)"
+	        AC_MSG_WARN(You need Coq 8.3 or later; Coq discarded)
+                reason_coq_support=" (need version 8.3 or later)"
                 ;;
         esac
     fi
@@ -426,6 +433,19 @@ if test "$enable_coq_libs" = yes; then
    fi
 fi
 
+if test "$enable_coq_libs" = yes; then
+   AC_MSG_CHECKING([for Flocq])
+   AS_IF(
+     [ echo "Require Fcore Fcalc_digits." > conftest.v
+       "$COQC" conftest.v > conftest.err ],
+     [ AC_MSG_RESULT(yes) ],
+     [ AC_MSG_RESULT(no)
+       enable_coq_fp_libs=no
+       AC_MSG_WARN(Cannot find Flocq.)
+       reason_coq_fp_libs=" (Flocq >= 1.4 not found)" ])
+   rm -f conftest.v conftest.vo conftest.err
+fi
+
 # hypothesis_selection
 
 if test "$enable_hypothesis_selection" = yes; then
@@ -504,6 +524,7 @@ AC_SUBST(META_OCAMLGRAPH)
 
 AC_SUBST(enable_coq_plugin)
 AC_SUBST(enable_coq_libs)
+AC_SUBST(enable_coq_fp_libs)
 
 AC_SUBST(COQC)
 AC_SUBST(COQDEP)
@@ -554,6 +575,9 @@ if test "$enable_coq_support" = "yes" ; then
    echo "    Lib                 : $COQLIB"
    echo "    Plugin support      : $enable_coq_plugin $reason_coq_plugin"
    echo "    Realization support : $enable_coq_libs $reason_coq_libs"
+   if test "$enable_coq_libs" = "yes" ; then
+      echo "        FP arithmetic   : $enable_coq_fp_libs $reason_coq_fp_libs"
+   fi
 fi
 echo "TPTP parser             : $enable_whytptp"
 echo "Menhir library          : $enable_menhirlib"

src/driver/whyconf.ml

@@ -29,10 +29,11 @@ open Rc
   - 6 driver renaming
   - 7 yices native (used for release 0.70)
   - 8 for release 0.71
+  - 9 coq realizations
 
 If a configuration doesn't contain the actual magic number we don't use it.*)
 
-let magicnumber = 8
+let magicnumber = 9
 
 exception WrongMagicNumber
 

src/printer/coq.ml

@@ -683,23 +683,9 @@ let init_printer th =
   Sid.iter (fun id -> ignore (id_unique pr id)) th.Theory.th_local;
   pr
 
-(* TODO: change into a less intrusive coding, e.g. a driver meta, and
-   make the lookup a bit more efficient along the way *)
-let realized_theories = [
-  ["int"; "Abs"];
-  ["int"; "ComputerDivision"];
-  ["int"; "EuclideanDivision"];
-  ["int"; "Int"];
-  ["int"; "MinMax"];
-  ["real"; "Abs"];
-  ["real"; "FromInt"];
-  ["real"; "MinMax"];
-  ["real"; "Real"];
-  ["real"; "Square"];
-  ["floating_point"; "Rounding"];
-  ["floating_point"; "Single"];
-  ["floating_point"; "Double"];
-]
+(* TODO: add a driver meta and make lookup for realized theories a bit
+   more efficient *)
+let realized_theories = Coq_config.realized_theories
 
 let print_task _env pr thpr realize ?old fmt task =
   forget_all ();