script de bench automatique pour extraction

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

7 files changed, 105 insertions, 13 deletions

diff --git a/contrib/extraction/test/.cvsignore b/contrib/extraction/test/.cvsignore
index 7166b260b..dbf6fbcaa 100644
--- a/contrib/extraction/test/.cvsignore
+++ b/contrib/extraction/test/.cvsignore
@@ -1 +1,7 @@
 *.ml
+theories
+ml2v 
+v2ml
+.depend
+log
+
diff --git a/contrib/extraction/test/Makefile b/contrib/extraction/test/Makefile
new file mode 100644
index 000000000..88823d6d7
--- /dev/null
+++ b/contrib/extraction/test/Makefile
@@ -0,0 +1,60 @@
+TOPDIR=../../..
+
+INCL= -I theories/Arith \
+-I theories/Bool \
+-I theories/Init \
+-I theories/IntMap \
+-I theories/Lists \
+-I theories/Logic \
+-I theories/Reals \
+-I theories/Relations \
+-I theories/Sets \
+-I theories/Wellfounded \
+-I theories/Zarith
+
+
+MLNAMES=
+CMONAMES=
+
+include .names.ml
+include .names.cmo
+
+all: allml .depend allcmo
+
+allml: .names.ml $(MLNAMES)
+
+allcmo: .names.cmo $(CMONAMES)
+
+.depend: Makefile
+	rm -f .depend; ocamldep $(INCL) theories/*/*.ml > .depend
+
+.names.ml: Makefile v2ml 
+	rm -f .names.ml; \
+	echo "MLNAMES= \\" > .names.ml; \
+	find theories  -name \*.v -exec ./v2ml \{\} \; | \
+	sed -e "s/\.ml/.ml \\\\/" >> .names.ml
+
+.names.cmo: .names.ml
+	rm -f .names.cmo; \
+	sed -e "1s/ML/CMO/" -e "s/\.ml/.cmo/" < .names.ml > .names.cmo
+
+tree: 
+	cp -fur $(TOPDIR)/theories .; rm -f theories/*/*.vo theories/*/*/*.vo
+
+
+%.cmo:%.ml
+	ocamlc $(INCL) -c -i $<
+
+%.ml: ml2v
+	./extract `./ml2v $@`
+
+clean: 
+	rm -f theories/*/*.ml theories/*/*.cm*
+
+ml2v: ml2v.ml
+	ocamlc -o $@ $<
+
+v2ml: v2ml.ml
+	ocamlc -o $@ $< 
+
+include .depend
diff --git a/contrib/extraction/test/bench b/contrib/extraction/test/bench
deleted file mode 100755
index bff9bd77a..000000000
--- a/contrib/extraction/test/bench
+++ /dev/null
@@ -1,6 +0,0 @@
-#!/bin/sh
-../../../bin/coqtop.byte -batch -load-vernac-source ./bench.v
-ocamlc -c -i polylist.ml
-ocamlc -c -i zarith.ml
-ocamlc -c -i even.ml
-
diff --git a/contrib/extraction/test/bench.v b/contrib/extraction/test/bench.v
deleted file mode 100644
index 84eed5e87..000000000
--- a/contrib/extraction/test/bench.v
+++ /dev/null
@@ -1,7 +0,0 @@
-Require PolyList.
-Extraction "polylist.ml" nth nth_in_or_default.
-Require ZArith.
-Extraction "zarith.ml" Zmult.
-Require Even.
-Extraction "even.ml" even_odd_dec.
-
diff --git a/contrib/extraction/test/extract b/contrib/extraction/test/extract
new file mode 100755
index 000000000..4b3da1371
--- /dev/null
+++ b/contrib/extraction/test/extract
@@ -0,0 +1,7 @@
+#!/bin/sh
+rm -f /tmp/extr.v 
+d=`dirname $1`
+n=`basename $1 .v`
+echo "Cd \"$d\". Extraction Module $n. " > /tmp/extr.v;\
+coqtop -batch -require $n -load-vernac-source /tmp/extr.v 
+
diff --git a/contrib/extraction/test/ml2v.ml b/contrib/extraction/test/ml2v.ml
new file mode 100644
index 000000000..665aabba4
--- /dev/null
+++ b/contrib/extraction/test/ml2v.ml
@@ -0,0 +1,17 @@
+let main () = begin
+  let j = Array.length (Sys.argv) in
+  if j>0 then begin
+	let s = Sys.argv.(1) in
+	let b = Filename.chop_extension (Filename.basename s) in 
+	let b0 = String.sub b 0 1 in
+	let b1 = String.capitalize b0 in  
+	let b = String.sub b 1 ((String.length b) -1) in 
+	let d = Filename.dirname s
+	in print_string (d^"/["^b0^b1^"]"^b^".v");
+	print_newline()
+  end;
+  exit(0)	
+end;;	
+
+main();;
+ 		
diff --git a/contrib/extraction/test/v2ml.ml b/contrib/extraction/test/v2ml.ml
new file mode 100644
index 000000000..c106147bf
--- /dev/null
+++ b/contrib/extraction/test/v2ml.ml
@@ -0,0 +1,15 @@
+let main () = begin
+  let j = Array.length (Sys.argv) in
+  if j>0 then begin
+	let s = Sys.argv.(1) in
+	let b = Filename.chop_extension (Filename.basename s) in 
+	let b = String.uncapitalize b in
+	let d = Filename.dirname s
+	in print_string (d^"/"^b^".ml");
+	print_newline()
+  end;
+  exit(0)	
+end;;	
+
+main();;
+