Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: extraction_dep.v Sprache: Coq

Original von: Coq^©

(** Examples of code elimination inside modules during extraction *)

Require Coq.extraction.Extraction.

(** NB: we should someday check the produced code instead of
    extracting and just compiling. *)

(** 1) Without signature ... *)

Module A.
Definition u := 0.
Definition v := 1.
Module B.
  Definition w := 2.
  Definition x := 3.
End B.
End A.

Definition testA := A.u + A.B.x.

Recursive Extraction testA. (* without: v w *)
Extraction TestCompile testA.

(** 1b) Same with an Include *)

Module Abis.
Include A.
Definition y := 4.
End Abis.

Definition testAbis := Abis.u + Abis.y.

Recursive Extraction testAbis. (* without: A B v w x *)
Extraction TestCompile testAbis.

(** 2) With signature, we only keep elements mentioned in signature. *)

Module Type SIG.
Parameter u : nat.
Parameter v : nat.
End SIG.

Module Ater : SIG.
Include A.
End Ater.

Definition testAter := Ater.u.

Recursive Extraction testAter. (* with only: u v *)
Extraction TestCompile testAter.

¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.