Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
2.5 kB · 82 lines
at master
1234567891011121314151617181920212223242526272829303132333435363738394041424344454647484950515253545556575859606162636465666768697071727374757677787980818283(* Inlining declarations ([Parameter Inline]) belong to module types: they are read back when a module type is used as a functor parameter, and turned into an actual substitution of bodies when the functor is applied. They are meaningless anywhere else. *)
Set Warnings "+inline-parameter-in-module".
(* A plain module cannot declare an inlinable parameter. *)Module M. Fail Parameter Inline(1) x : Type.End M.
Module Type T. Parameter Inline t : Type. Parameter u : t -> t.End T.
(* The declaration survives the various ways of building a module type out of another one. *)Module Type T2 := T.Module Type T3. Include T. End T3.Module Type T4. Declare Module Sub : T. End T4.
Module A. Definition t := nat. Definition u (x : nat) := x.End A.
Module F (X : T) := X.Module F2 (X : T2) := X.Module F3 (X : T3) := X.Module F4 (X : T4) := X.Module B. Module Sub := A. End B.
Module A1 := F A.Module A2 := F2 A.Module A3 := F3 A.Module B4 := F4 B.
(* A functor whose parameter type is itself a functor type mentioning [T]: the subtyping check of the argument against [FS] must not confuse the inlining declaration of [T] with an actual body. *)Module Type FS (X : T). Parameter v : X.t -> X.t. End FS.Module G (X : T). Definition v := X.u. End G.Module H (K : FS) (X : T) := K X.Module C := H G A.
(* The application may also be reached through an [Include], possibly nested. *)Module I1. Include F A. End I1.Module I2. Module Inner. Include F A. End Inner. End I2.Module I3. Module N := F A. End I3.
(* Applying a functor type. *)Module Type FT (X : T). Definition u := X.u. End FT.Module Type S1 := FT A.Module Type S2. Include FT A. End S2.Module J1 : S1. Definition u := A.u. End J1.Module J2 : S2. Definition u := A.u. End J2.
(* [A1.u] is [A.u], whose argument is in [nat_scope]; the notation below would otherwise make [1] a [bool]. Getting this right requires the body [nat] of the inlinable field [t] to reach the objects of the functor. See also test-suite/bugs/bug_15403.v. *)Notation "1" := true.
Check A1.u 1.Check A2.u 1.Check A3.u 1.Check B4.Sub.u 1.Check C.v 1.Check I1.u 1.Check I2.Inner.u 1.Check I3.N.u 1.Check J1.u 1.Check J2.u 1.
(* An inlinable field of a functor argument stays identified with the argument's field: the inlining does not replace the name equivalence. *)Module K (X : T). Include F X. End K.Module K1 := K A.Definition check_alias : K1.t = A.t := eq_refl.Definition check_alias' : K1.u = A.u := eq_refl.