Quelle bug_4720.v Sprache: Coq

(** Bug 4720 : extraction and "with" in module type *)

Module Type A.
Parameter t : Set.
End A.

Module A_instance <: A.
Definition t := nat.
End A_instance.

Module A_private : A.
Definition t := nat.
End A_private.

Module Type B.
End B.

Module Type C (b : B).
Declare Module a : A.
End C.

Module WithMod (a' : A) (b' : B) (c' : C b' with Module a := A_instance).
End WithMod.

Module WithDef (a' : A) (b' : B) (c' : C b' with Definition a.t := nat).
End WithDef.

Module WithModPriv (a' : A) (b' : B) (c' : C b' with Module a := A_private).
End WithModPriv.

(* The initial bug report was concerning the extraction of WithModPriv
   in Coq 8.4, which was suboptimal: it was compiling, but could have been
   turned into some faulty code since A_private and c'.a were not seen as
   identical by the extraction.

   In Coq 8.5 and 8.6, the extractions of WithMod, WithDef, WithModPriv
   were all causing Anomaly or Assert Failure. This should be fixed now.
*)

Require Extraction.

Recursive Extraction WithMod.

Recursive Extraction WithDef.

Recursive Extraction WithModPriv.

(* Let's even check that all this extracted code is actually compilable: *)

Extraction TestCompile WithMod WithDef WithModPriv.

quality98%

¤ Dauer der Verarbeitung: 0.2 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.