aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/extraction
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/extraction')
-rw-r--r--contrib/extraction/test/Makefile112
-rwxr-xr-xcontrib/extraction/test/extract10
-rwxr-xr-xcontrib/extraction/test/extract_reals31
-rw-r--r--contrib/extraction/test/ml2v.ml13
-rw-r--r--contrib/extraction/test/v2ml.ml10
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()