1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
|
From Coq Require BinNat.
From Coq Require Extraction.
(* Define axiomatic functions. *)
Axiom ax_fun : nat -> nat.
Axiom ax_fun2 : nat -> nat.
(* Declare a function that executes ax_fun if a is positive
and returns 0, else. *)
Definition my_fun (a : nat) :=
if Nat.leb a 0
then ax_fun a
else 0.
(* Extraction of foreign constant and callback for Haskell must fail *)
Extraction Language Haskell.
Fail Extract Foreign Constant ax_fun => "my_c_fun".
Fail Extract Callback "call_my_fun" my_fun.
(* Extraction of foreign constant and callback for Scheme must fail *)
Extraction Language Scheme.
Fail Extract Foreign Constant ax_fun => "my_c_fun".
Fail Extract Callback "call_my_fun" my_fun.
(* Extraction of foreign constant and callback for JSON must fail *)
Extraction Language JSON.
Fail Extract Foreign Constant ax_fun => "my_c_fun".
Fail Extract Callback "call_my_fun" my_fun.
(* Extraction of foreign constant for already defined inlined ml function must fail. *)
Extraction Language OCaml.
Extract Inlined Constant ax_fun => "my_ml_fun".
Fail Extract Foreign Constant ax_fun => "my_c_fun".
(* Extraction of inlined constant for already defined foreign function must fail. *)
Extract Foreign Constant ax_fun2 => "my_c_fun".
Fail Extract Inlined Constant ax_fun2 => "my_ml_fun".
|
