diff options
Diffstat (limited to 'contrib/extraction/test/custom')
24 files changed, 61 insertions, 0 deletions
diff --git a/contrib/extraction/test/custom/Adalloc b/contrib/extraction/test/custom/Adalloc new file mode 100644 index 00000000..0fb556aa --- /dev/null +++ b/contrib/extraction/test/custom/Adalloc @@ -0,0 +1,2 @@ +Require Import Addr. +Extraction NoInline ad_double ad_double_plus_un. diff --git a/contrib/extraction/test/custom/Euclid b/contrib/extraction/test/custom/Euclid new file mode 100644 index 00000000..a58e3940 --- /dev/null +++ b/contrib/extraction/test/custom/Euclid @@ -0,0 +1 @@ +Extraction Inline Wf_nat.gt_wf_rec Wf_nat.lt_wf_rec. diff --git a/contrib/extraction/test/custom/List b/contrib/extraction/test/custom/List new file mode 100644 index 00000000..ffee7dc9 --- /dev/null +++ b/contrib/extraction/test/custom/List @@ -0,0 +1 @@ +Extraction NoInline map. diff --git a/contrib/extraction/test/custom/ListSet b/contrib/extraction/test/custom/ListSet new file mode 100644 index 00000000..c9bea52a --- /dev/null +++ b/contrib/extraction/test/custom/ListSet @@ -0,0 +1 @@ +Extraction NoInline set_add set_mem. diff --git a/contrib/extraction/test/custom/Lsort b/contrib/extraction/test/custom/Lsort new file mode 100644 index 00000000..6a185683 --- /dev/null +++ b/contrib/extraction/test/custom/Lsort @@ -0,0 +1,2 @@ +Require Import Addr. +Extraction NoInline ad_double ad_double_plus_un. diff --git a/contrib/extraction/test/custom/Map b/contrib/extraction/test/custom/Map new file mode 100644 index 00000000..3e464e39 --- /dev/null +++ b/contrib/extraction/test/custom/Map @@ -0,0 +1,3 @@ +Require Import Addr. +Extraction NoInline ad_double ad_double_plus_un. + diff --git a/contrib/extraction/test/custom/Mapcard b/contrib/extraction/test/custom/Mapcard new file mode 100644 index 00000000..ca555aa3 --- /dev/null +++ b/contrib/extraction/test/custom/Mapcard @@ -0,0 +1,4 @@ +Require Import Plus. +Extraction NoInline plus_is_one. +Require Import Addr. +Extraction NoInline ad_double ad_double_plus_un. diff --git a/contrib/extraction/test/custom/Mapiter b/contrib/extraction/test/custom/Mapiter new file mode 100644 index 00000000..6a185683 --- /dev/null +++ b/contrib/extraction/test/custom/Mapiter @@ -0,0 +1,2 @@ +Require Import Addr. +Extraction NoInline ad_double ad_double_plus_un. diff --git a/contrib/extraction/test/custom/R_Ifp b/contrib/extraction/test/custom/R_Ifp new file mode 100644 index 00000000..d8f1b3e7 --- /dev/null +++ b/contrib/extraction/test/custom/R_Ifp @@ -0,0 +1,2 @@ +Load "custom/Reals". + diff --git a/contrib/extraction/test/custom/R_sqr b/contrib/extraction/test/custom/R_sqr new file mode 100644 index 00000000..d8f1b3e7 --- /dev/null +++ b/contrib/extraction/test/custom/R_sqr @@ -0,0 +1,2 @@ +Load "custom/Reals". + diff --git a/contrib/extraction/test/custom/Ranalysis b/contrib/extraction/test/custom/Ranalysis new file mode 100644 index 00000000..d8f1b3e7 --- /dev/null +++ b/contrib/extraction/test/custom/Ranalysis @@ -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 00000000..d8f1b3e7 --- /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 00000000..d8f1b3e7 --- /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 00000000..d8f1b3e7 --- /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 00000000..d8f1b3e7 --- /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 00000000..45d0a224 --- /dev/null +++ b/contrib/extraction/test/custom/Reals.v @@ -0,0 +1,17 @@ +Require Import 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". +Extract Inlined Constant sqrt => "sqrt". +Extract Inlined Constant sigma => "(fun l h -> sigma_aux l h (Minus.minus h l))". +Extract Inlined Constant PI => "3.141593". +Extract Inlined Constant cos => cos. +Extract Inlined Constant sin => sin. +Extract Inlined Constant derive_pt => "(fun f x -> ((f (x+.1E-5))-.(f x))*.1E5)". diff --git a/contrib/extraction/test/custom/Rfunctions b/contrib/extraction/test/custom/Rfunctions new file mode 100644 index 00000000..d8f1b3e7 --- /dev/null +++ b/contrib/extraction/test/custom/Rfunctions @@ -0,0 +1,2 @@ +Load "custom/Reals". + diff --git a/contrib/extraction/test/custom/Rgeom b/contrib/extraction/test/custom/Rgeom new file mode 100644 index 00000000..d8f1b3e7 --- /dev/null +++ b/contrib/extraction/test/custom/Rgeom @@ -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 00000000..d8f1b3e7 --- /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 00000000..d8f1b3e7 --- /dev/null +++ b/contrib/extraction/test/custom/Rseries @@ -0,0 +1,2 @@ +Load "custom/Reals". + diff --git a/contrib/extraction/test/custom/Rsigma b/contrib/extraction/test/custom/Rsigma new file mode 100644 index 00000000..d8f1b3e7 --- /dev/null +++ b/contrib/extraction/test/custom/Rsigma @@ -0,0 +1,2 @@ +Load "custom/Reals". + diff --git a/contrib/extraction/test/custom/Rtrigo b/contrib/extraction/test/custom/Rtrigo new file mode 100644 index 00000000..d8f1b3e7 --- /dev/null +++ b/contrib/extraction/test/custom/Rtrigo @@ -0,0 +1,2 @@ +Load "custom/Reals". + diff --git a/contrib/extraction/test/custom/ZArith_dec b/contrib/extraction/test/custom/ZArith_dec new file mode 100644 index 00000000..2201419e --- /dev/null +++ b/contrib/extraction/test/custom/ZArith_dec @@ -0,0 +1 @@ +Extraction Inline Dcompare_inf Zcompare_rec. diff --git a/contrib/extraction/test/custom/fast_integer b/contrib/extraction/test/custom/fast_integer new file mode 100644 index 00000000..e2b24953 --- /dev/null +++ b/contrib/extraction/test/custom/fast_integer @@ -0,0 +1 @@ +Extraction NoInline Zero_suivi_de Un_suivi_de. |