diff options
Diffstat (limited to 'contrib/extraction')
-rw-r--r-- | contrib/extraction/test/Makefile | 112 | ||||
-rwxr-xr-x | contrib/extraction/test/extract | 10 | ||||
-rwxr-xr-x | contrib/extraction/test/extract_reals | 31 | ||||
-rw-r--r-- | contrib/extraction/test/ml2v.ml | 13 | ||||
-rw-r--r-- | contrib/extraction/test/v2ml.ml | 10 |
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() |