Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: bug_3746.v Sprache: Coq

Original von: Coq^©

(* Bug report #3746 : Include and restricted signature *)

Module Type MT. Parameter p : nat. End MT.
Module Type EMPTY. End EMPTY.
Module Empty. End Empty.

(* Include of an applied functor with restricted sig :
   Used to create axioms (bug report #3746), now forbidden. *)

Module F (X:EMPTY) : MT.
Definition p := 0.
End F.

Module InclFunctRestr.
Fail Include F(Empty).
End InclFunctRestr.

(* A few variants (indirect restricted signature), also forbidden. *)

Module F1 := F.
Module F2 (X:EMPTY) := F X.

Module F3a (X:EMPTY). Definition p := 0. End F3a.
Module F3 (X:EMPTY) : MT := F3a X.

Module InclFunctRestrBis.
Fail Include F1(Empty).
Fail Include F2(Empty).
Fail Include F3(Empty).
End InclFunctRestrBis.

(* Recommended workaround: manual instance before the include. *)

Module InclWorkaround.
Module Temp := F(Empty).
Include Temp.
End InclWorkaround.

Compute InclWorkaround.p.
Print InclWorkaround.p.
Print Assumptions InclWorkaround.p. (* Closed under the global context *)

(* Related situations which are ok, just to check *)

(* A) Include of non-functor with restricted signature :
   creates a proxy to initial stuff *)

Module M : MT.
  Definition p := 0.
End M.

Module InclNonFunct.
  Include M.
End InclNonFunct.

Definition check : InclNonFunct.p = M.p := eq_refl.
Print Assumptions InclNonFunct.p. (* Closed *)

(* B) Include of a module type with opaque content:
   The opaque content is "copy-pasted". *)

Module Type SigOpaque.
Definition p : nat. Proof. exact 0. Qed.
End SigOpaque.

Module InclSigOpaque.
Include SigOpaque.
End InclSigOpaque.

Compute InclSigOpaque.p.
Print InclSigOpaque.p.
Print Assumptions InclSigOpaque.p. (* Closed *)

(* C) Include of an applied functor with opaque proofs :
   opaque proof "copy-pasted" (and substituted). *)

Module F' (X:EMPTY).
Definition p : nat. Proof. exact 0. Qed.
End F'.

Module InclFunctOpa.
Include F'(Empty).
End InclFunctOpa.

Compute InclFunctOpa.p.
Print InclFunctOpa.p.
Print Assumptions InclFunctOpa.p. (* Closed *)

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