refonte du test

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2162 85f007b7-540e-0410-9357-904b9bb8a0f7

15 files changed, 33 insertions, 42 deletions

diff --git a/contrib/extraction/test/Makefile b/contrib/extraction/test/Makefile
index c28e961e9c..af2ae59ffa 100644
--- a/contrib/extraction/test/Makefile
+++ b/contrib/extraction/test/Makefile
@@ -9,7 +9,7 @@ TOPDIR=../../..
 AXIOMSVO:= \
 theories/Arith/Arith.vo \
 theories/Lists/List.vo \
-theories/Reals/% \
+theories/Reals/Rsyntax.vo \
 theories/Num/% \
 theories/Relations/Rstar.vo \
 theories/Sets/Integers.vo \
@@ -31,7 +31,10 @@ CMO:= $(patsubst %.ml,%.cmo,$(ML))
 #	General rules 
 #
 
-all: ml $(CMO) v2ml
+all: ml theories/Reals/addReals.cmo $(CMO) v2ml
+
+theories/Reals/addReals.ml: 
+	cp -f addReals theories/Reals/addReals.ml
 
 ml: $(ML)
 
@@ -45,33 +48,13 @@ tree:
 	ocamlc $(INCL) -c -i $<
 
 $(ML): ml2v
-	./extract `./ml2v $@`
+	./extract $@
 
 clean: 
 	rm -f theories/*/*.ml theories/*/*.cm* theories/*/*.ml.orig
 
 
 #
-#	Extraction of Reals
-#
-
-REALSALLVO:=$(shell cd ../../..; ls -tr theories/Reals/*.vo)
-REALSVO:=$(filter-out theories/Reals/Rsyntax.vo,$(REALSALLVO))
-REALSML:=$(shell test -x v2ml && ./v2ml $(REALSVO))
-REALSCMO:= $(patsubst %.ml,%.cmo,$(REALSML))
-
-reals: all $(REALSML) theories/Reals/addReals.cmo $(REALSCMO)
-
-realsml: 
-	./extract_reals $(REALSVO)
-
-theories/Reals/addReals.ml: 
-	cp -f addReals theories/Reals/addReals.ml
-
-$(REALSML): realsml
-
-
-#
 #	Utilities
 #
 
diff --git a/contrib/extraction/test/custom/ListSet b/contrib/extraction/test/custom/ListSet
new file mode 100644
index 0000000000..c9bea52a4c
--- /dev/null
+++ b/contrib/extraction/test/custom/ListSet
@@ -0,0 +1 @@
+Extraction NoInline set_add set_mem.
diff --git a/contrib/extraction/test/custom/PolyList b/contrib/extraction/test/custom/PolyList
new file mode 100644
index 0000000000..ffee7dc9c1
--- /dev/null
+++ b/contrib/extraction/test/custom/PolyList
@@ -0,0 +1 @@
+Extraction NoInline map.
diff --git a/contrib/extraction/test/custom/R_Ifp b/contrib/extraction/test/custom/R_Ifp
new file mode 100644
index 0000000000..d8f1b3e7b7
--- /dev/null
+++ b/contrib/extraction/test/custom/R_Ifp
@@ -0,0 +1,2 @@
+Load "custom/Reals".
+
diff --git a/contrib/extraction/test/custom/Raxioms b/contrib/extraction/test/custom/Raxioms
new file mode 100644
index 0000000000..d8f1b3e7b7
--- /dev/null
+++ b/contrib/extraction/test/custom/Raxioms
@@ -0,0 +1,2 @@
+Load "custom/Reals".
+
diff --git a/contrib/extraction/test/custom/Rbase b/contrib/extraction/test/custom/Rbase
new file mode 100644
index 0000000000..d8f1b3e7b7
--- /dev/null
+++ b/contrib/extraction/test/custom/Rbase
@@ -0,0 +1,2 @@
+Load "custom/Reals".
+
diff --git a/contrib/extraction/test/custom/Rbasic_fun b/contrib/extraction/test/custom/Rbasic_fun
new file mode 100644
index 0000000000..d8f1b3e7b7
--- /dev/null
+++ b/contrib/extraction/test/custom/Rbasic_fun
@@ -0,0 +1,2 @@
+Load "custom/Reals".
+
diff --git a/contrib/extraction/test/custom/Rdefinitions b/contrib/extraction/test/custom/Rdefinitions
new file mode 100644
index 0000000000..d8f1b3e7b7
--- /dev/null
+++ b/contrib/extraction/test/custom/Rdefinitions
@@ -0,0 +1,2 @@
+Load "custom/Reals".
+
diff --git a/contrib/extraction/test/extract_reals b/contrib/extraction/test/custom/Reals.v
index 9cb14ef458..d42fe0a53c 100755..100644
--- a/contrib/extraction/test/extract_reals
+++ b/contrib/extraction/test/custom/Reals.v
@@ -1,8 +1,4 @@
-#!/bin/sh
-rm -f /tmp/extr$$.v
-cat > /tmp/extr$$.v << EOF
-Cd "theories/Reals".
-Require Reals.
+Require Reals. 
 Extract Inlined Constant R => float.
 Extract Inlined Constant R0 => "0.0".
 Extract Inlined Constant R1 => "1.0".
@@ -13,15 +9,4 @@ Extract Inlined Constant Rinv => "(fun x -> 1.0 /. x)".
 Extract Inlined Constant Rlt => "(<)".
 Extract Inlined Constant up => "AddReals.my_ceil".
 Extract Inlined Constant total_order_T => "AddReals.total_order_T".
-EOF
-for f in $*; do
-    ff=`basename $f .vo`
-    echo "Require $ff." >> /tmp/extr$$.v
-    echo "Extraction Module $ff." >> /tmp/extr$$.v
-done
-../../../bin/coqtop.opt -silent -batch -load-vernac-source /tmp/extr$$.v
-out=$?
-#rm -f /tmp/extr$$.v
-exit $out
-
 
diff --git a/contrib/extraction/test/custom/Rfunctions b/contrib/extraction/test/custom/Rfunctions
new file mode 100644
index 0000000000..d8f1b3e7b7
--- /dev/null
+++ b/contrib/extraction/test/custom/Rfunctions
@@ -0,0 +1,2 @@
+Load "custom/Reals".
+
diff --git a/contrib/extraction/test/custom/Rlimit b/contrib/extraction/test/custom/Rlimit
new file mode 100644
index 0000000000..d8f1b3e7b7
--- /dev/null
+++ b/contrib/extraction/test/custom/Rlimit
@@ -0,0 +1,2 @@
+Load "custom/Reals".
+
diff --git a/contrib/extraction/test/custom/Rseries b/contrib/extraction/test/custom/Rseries
new file mode 100644
index 0000000000..d8f1b3e7b7
--- /dev/null
+++ b/contrib/extraction/test/custom/Rseries
@@ -0,0 +1,2 @@
+Load "custom/Reals".
+
diff --git a/contrib/extraction/test/custom/all b/contrib/extraction/test/custom/all
new file mode 100644
index 0000000000..deeb977d70
--- /dev/null
+++ b/contrib/extraction/test/custom/all
@@ -0,0 +1 @@
+Extraction Inline sigS_rec.
diff --git a/contrib/extraction/test/custom/fast_integer b/contrib/extraction/test/custom/fast_integer
new file mode 100644
index 0000000000..e2b2495340
--- /dev/null
+++ b/contrib/extraction/test/custom/fast_integer
@@ -0,0 +1 @@
+Extraction NoInline Zero_suivi_de Un_suivi_de.
diff --git a/contrib/extraction/test/extract b/contrib/extraction/test/extract
index 356a362099..ea85582dff 100755
--- a/contrib/extraction/test/extract
+++ b/contrib/extraction/test/extract
@@ -1,8 +1,11 @@
 #!/bin/sh
 rm -f /tmp/extr$$.v 
-d=`dirname $1`
-n=`basename $1 .v`
-echo "Cd \"$d\". Extraction Module $n. " > /tmp/extr$$.v
+vfile=`./ml2v $1`
+d=`dirname $vfile`
+n=`basename $vfile .v`
+cat custom/all > /tmp/extr$$.v
+if [ -e custom/$n ]; then cat custom/$n >> /tmp/extr$$.v; fi  
+echo "Cd \"$d\". Extraction Module $n. " >> /tmp/extr$$.v
 ../../../bin/coqtop.opt -silent -batch -require $n -load-vernac-source /tmp/extr$$.v 
 out=$?
 rm -f /tmp/extr$$.v