Quelle Extraction_ffi.v Sprache: Coq

(* @eladrion's example for issue #18212 *)

From Corelib Require Extraction.

(* Define an axiomatic function. *)
Axiom ax_fun : nat -> nat.

(* Define a fully specified function*)
Definition exact_fun (a : nat) := (ax_fun a) + 1.

(* Define duplicate of the fully specified function*)
Definition exact_fun2 (a : nat) := (ax_fun a) + 1.

(* before we give the directive axioms produce failwith "axiom to be realized" *)
Extraction ax_fun.

(* ax_fun shall be a FFI call to the C function my_c_fun *)
Extract Foreign Constant ax_fun => "my_c_fun".
Extraction ax_fun.

(* Extract exact_fun *)
Extraction exact_fun.

(* exact_fun shall now be a FFI call to the C function my_c_fun *)
Extract Foreign Constant exact_fun => "my_exact_c_fun".
Extraction exact_fun.

(* Now, exact_fun is an entry point exposed to C *)
Extract Callback "call_exact_fun" exact_fun2.
Extraction exact_fun2.

(* Now we make sure that a callback registration can be reverted *)
Reset Extraction Callback.
Extraction exact_fun2.

quality99%

¤ Dauer der Verarbeitung: 0.4 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.