From 8cd83fb8dd41521bbc109d37dd49dd3aae0de373 Mon Sep 17 00:00:00 2001 From: letouzey Date: Mon, 5 Nov 2001 17:20:41 +0000 Subject: refonte du test git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2162 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/extraction/test/Makefile | 29 ++++++----------------------- contrib/extraction/test/custom/ListSet | 1 + contrib/extraction/test/custom/PolyList | 1 + contrib/extraction/test/custom/R_Ifp | 2 ++ contrib/extraction/test/custom/Raxioms | 2 ++ contrib/extraction/test/custom/Rbase | 2 ++ contrib/extraction/test/custom/Rbasic_fun | 2 ++ contrib/extraction/test/custom/Rdefinitions | 2 ++ contrib/extraction/test/custom/Reals.v | 12 ++++++++++++ contrib/extraction/test/custom/Rfunctions | 2 ++ contrib/extraction/test/custom/Rlimit | 2 ++ contrib/extraction/test/custom/Rseries | 2 ++ contrib/extraction/test/custom/all | 1 + contrib/extraction/test/custom/fast_integer | 1 + contrib/extraction/test/extract | 9 ++++++--- contrib/extraction/test/extract_reals | 27 --------------------------- 16 files changed, 44 insertions(+), 53 deletions(-) create mode 100644 contrib/extraction/test/custom/ListSet create mode 100644 contrib/extraction/test/custom/PolyList create mode 100644 contrib/extraction/test/custom/R_Ifp create mode 100644 contrib/extraction/test/custom/Raxioms create mode 100644 contrib/extraction/test/custom/Rbase create mode 100644 contrib/extraction/test/custom/Rbasic_fun create mode 100644 contrib/extraction/test/custom/Rdefinitions create mode 100644 contrib/extraction/test/custom/Reals.v create mode 100644 contrib/extraction/test/custom/Rfunctions create mode 100644 contrib/extraction/test/custom/Rlimit create mode 100644 contrib/extraction/test/custom/Rseries create mode 100644 contrib/extraction/test/custom/all create mode 100644 contrib/extraction/test/custom/fast_integer delete mode 100755 contrib/extraction/test/extract_reals 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,32 +48,12 @@ 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/custom/Reals.v b/contrib/extraction/test/custom/Reals.v new file mode 100644 index 0000000000..d42fe0a53c --- /dev/null +++ b/contrib/extraction/test/custom/Reals.v @@ -0,0 +1,12 @@ +Require Reals. +Extract Inlined Constant R => float. +Extract Inlined Constant R0 => "0.0". +Extract Inlined Constant R1 => "1.0". +Extract Inlined Constant Rplus => "(+.)". +Extract Inlined Constant Rmult => "( *.)". +Extract Inlined Constant Ropp => "(~-.)". +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". + 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 diff --git a/contrib/extraction/test/extract_reals b/contrib/extraction/test/extract_reals deleted file mode 100755 index 9cb14ef458..0000000000 --- a/contrib/extraction/test/extract_reals +++ /dev/null @@ -1,27 +0,0 @@ -#!/bin/sh -rm -f /tmp/extr$$.v -cat > /tmp/extr$$.v << EOF -Cd "theories/Reals". -Require Reals. -Extract Inlined Constant R => float. -Extract Inlined Constant R0 => "0.0". -Extract Inlined Constant R1 => "1.0". -Extract Inlined Constant Rplus => "(+.)". -Extract Inlined Constant Rmult => "( *.)". -Extract Inlined Constant Ropp => "(~-.)". -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 - - -- cgit v1.2.3