Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: subtyping.v Sprache: Coq

Original von: Coq^©

(* Non regression for bug #1302 *)

(* With universe polymorphism for inductive types, subtyping of
   inductive types needs a special treatment: the standard conversion
   algorithm does not work as it only knows to deal with constraints of
   the form alpha = beta or max(alphas, alphas+1) <= beta, while
   subtyping of inductive types in Type generates constraints of the form
   max(alphas, alphas+1) <= max(betas, betas+1).

   These constraints are anyway valid by monotonicity of subtyping but we
   have to detect it early enough to avoid breaking the standard
   algorithm for constraints on algebraic universes. *)

Module Type T.

Parameter A : Type (* Top.1 *) .

Inductive L : Type (* max(Top.1,1) *) :=
| L0
| L1 :  (A -> Prop) -> L.

End T.

Axiom Tp : Type (* Top.5 *) .

Module TT : T.

Definition A : Type (* Top.6 *) := Tp. (* generates Top.5 <= Top.6 *)

Inductive L : Type (* max(Top.6,1) *) :=
| L0
| L1 :  (A -> Prop) -> L.

End TT. (* Generates Top.6 <= Top.1 (+ auxiliary constraints for L_rect) *)

(* Note: Top.6 <= Top.1 is generated by subtyping on A;
   subtyping of L follows and has not to be checked *)

(* The same bug as #1302 but for Definition *)
(* Check that inferred algebraic universes in interfaces are considered *)

Module Type U. Definition A := Type -> Type. End U.
Module M:U. Definition A := Type -> Type. End M.

¤ 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.