Remaniement Makefile de test. make reals possible

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

5 files changed, 122 insertions, 54 deletions

diff --git a/contrib/extraction/test/Makefile b/contrib/extraction/test/Makefile
index bfc5ad0e5..9d91de87b 100644
--- a/contrib/extraction/test/Makefile
+++ b/contrib/extraction/test/Makefile
@@ -1,62 +1,96 @@
+# 
+#	General variables
+#
+
 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
+# Files with axioms to be realized: can't be extracted directly
 
+AXIOMSVO:= \
+theories/Arith/Arith.vo \
+theories/Lists/List.vo \
+theories/Reals/% \
+theories/Relations/Rstar.vo \
+theories/Sets/Integers.vo \
+theories/ZArith/Zsyntax.vo
 
-MLNAMES=
-CMONAMES=
+DIRS:= $(shell (cd $(TOPDIR);find theories -type d ! -name CVS))
 
-include .names.ml
-include .names.cmo
+INCL:= $(patsubst %,-I %,$(DIRS))
 
-all: ml2v v2ml allml .depend allcmo
+VO:= $(shell (cd $(TOPDIR);find theories -name \*.vo))
 
-allml: .names.ml $(MLNAMES)
+VO:= $(filter-out $(AXIOMSVO),$(VO))
 
-allcmo: .names.cmo $(CMONAMES)
+ML:= $(shell test -x v2ml && ./v2ml $(VO))
 
-.depend: Makefile
-	rm -f .depend; ocamldep $(INCL) theories/*/*.ml > .depend
+CMO:= $(patsubst %.ml,%.cmo,$(ML))
 
-.names.ml: Makefile v2ml 
-	rm -f .names.ml; \
-	echo "MLNAMES= \\" > .names.ml; \
-	V2ML=`pwd`/v2ml; \
-	(cd $(TOPDIR); find theories  -name \*.v -exec $$V2ML \{\} \;) | \
-	sed -e "s/\.ml/.ml \\\\/" >> .names.ml
+#
+#	General rules 
+#
 
-.names.cmo: .names.ml
-	rm -f .names.cmo; \
-	sed -e "1s/ML/CMO/" -e "s/\.ml/.cmo/" < .names.ml > .names.cmo
+all: $(ML) .depend $(CMO) v2ml
 
-tree:
-	for f in `cd $(TOPDIR); find theories -type d ! -name CVS`; do \
-		mkdir -p $$f; \
-	done
+depend: $(ML)
+	rm -f .depend; ocamldep $(INCL) $(ML) > .depend
 
-ml2v: ml2v.ml
-	ocamlc -o $@ $<
-
-v2ml: v2ml.ml
-	ocamlc -o $@ $< 
+tree:
+	mkdir -p $(DIRS)
 
 %.cmo:%.ml
 	ocamlc $(INCL) -c -i $<
 
-%.ml: 
+$(ML): ml2v
 	./extract `./ml2v $@`
 
 clean: 
 	rm -f theories/*/*.ml theories/*/*.cm*
 
+#
+#	Extraction of Reals
+#
+
+REALSML:= \
+theories/Reals/typeSyntax.ml \
+theories/Reals/addReals.ml \
+theories/Reals/rdefinitions.ml \
+theories/Reals/raxioms.ml \
+theories/Reals/r_Ifp.ml \
+theories/Reals/rbase.ml \
+theories/Reals/rbasic_fun.ml \
+theories/Reals/rlimit.ml \
+theories/Reals/rderiv.ml
+
+REALSCMO:= $(patsubst %.ml,%.cmo,$(REALSML))
+
+reals: all $(REALSML) $(REALSCMO)
+
+realsml: 
+	./extract_reals
+	cp -f addReals.ml theories/Reals
+
+$(REALSML): realsml
+
+
+#
+#	Utilities
+#
+
+ml2v: ml2v.ml
+	ocamlc -o $@ $<
+
+v2ml: v2ml.ml
+	ocamlc -o $@ $< 
+	$(MAKE)
+
+#
+#	The End
+#
+
+.PHONY: all tree clean reals realsml depend
+
 include .depend
+
+
+
diff --git a/contrib/extraction/test/extract b/contrib/extraction/test/extract
index b5d6a6a78..356a36209 100755
--- a/contrib/extraction/test/extract
+++ b/contrib/extraction/test/extract
@@ -1,8 +1,10 @@
 #!/bin/sh
-rm -f /tmp/extr.v 
+rm -f /tmp/extr$$.v 
 d=`dirname $1`
 n=`basename $1 .v`
-echo "Cd \"$d\". Extraction Module $n. " > /tmp/extr$$.v;\
-(../../../bin/coqtop.opt -silent -batch -require $n -load-vernac-source /tmp/extr$$.v && rm -f /tmp/extr$$.v) || (rm -f /tmp/extr$$.v; exit 1)
-
+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
+exit $out
 
diff --git a/contrib/extraction/test/extract_reals b/contrib/extraction/test/extract_reals
new file mode 100755
index 000000000..92749ff0a
--- /dev/null
+++ b/contrib/extraction/test/extract_reals
@@ -0,0 +1,31 @@
+#!/bin/sh
+rm -f /tmp/extr$$.v
+cat > /tmp/extr$$.v << EOF
+Cd "theories/Reals".
+Require Reals.
+Extract Constant R => float.
+Extract Constant R0 => "0.0".
+Extract Constant R1 => "1.0".
+Extract Constant Rplus => "(+.)".
+Extract Constant Rmult => "( *.)".
+Extract Constant Ropp => "(~-.)".
+Extract Constant Rinv => "(fun x -> 1.0 /. x)".
+Extract Constant Rlt => "(<)".
+Extract Constant up => "AddReals.my_ceil".
+Extract Constant total_order_T => "AddReals.total_order_T".
+Extraction Module Rdefinitions.
+Extraction Module TypeSyntax.
+Extraction Module Raxioms.
+Extraction Module Rbase.   
+Extraction Module R_Ifp.
+Extraction Module Rbasic_fun.
+Extraction Module Rlimit.
+Extraction Module Rfunctions.
+Extraction Module Rderiv.
+EOF
+../../../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/ml2v.ml b/contrib/extraction/test/ml2v.ml
index 2cf9190e1..363ea642f 100644
--- a/contrib/extraction/test/ml2v.ml
+++ b/contrib/extraction/test/ml2v.ml
@@ -1,13 +1,14 @@
 let _ =
-  let j = Array.length Sys.argv in
-  if j > 0 then
-    let fml = Sys.argv.(1) in
+  for j = 1 to ((Array.length Sys.argv)-1) do
+    let fml = Sys.argv.(j) in
     let f = Filename.chop_extension fml in 
     let fv = f ^ ".v" in
     if Sys.file_exists ("../../../" ^ fv) then
-      print_endline fv
+      print_string (fv^" ") 
     else
       let d = Filename.dirname f in
       let b = String.capitalize (Filename.basename f) in
-      let fv = Filename.concat d (b ^ ".v") in
-      print_endline fv
+      let fv = Filename.concat d (b ^ ".v ") in
+      print_string fv
+  done;
+  print_newline()
diff --git a/contrib/extraction/test/v2ml.ml b/contrib/extraction/test/v2ml.ml
index 0a28f6084..245a1b1e2 100644
--- a/contrib/extraction/test/v2ml.ml
+++ b/contrib/extraction/test/v2ml.ml
@@ -1,9 +1,9 @@
 let _ = 
-  let j = Array.length (Sys.argv) in
-  if j>0 then 
-    let s = Sys.argv.(1) in
+  for j = 1 to ((Array.length Sys.argv) -1) do 
+    let s = Sys.argv.(j) in
     let b = Filename.chop_extension (Filename.basename s) in 
     let b = String.uncapitalize b in
     let d = Filename.dirname s in 
-    print_endline (Filename.concat d (b ^ ".ml"))
-
+    print_string (Filename.concat d (b ^ ".ml "))
+  done;	
+  print_newline()