From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- test-suite/success/primitiveproj.v | 190 +++++++++++++++++++++++++++++++++++++ 1 file changed, 190 insertions(+) create mode 100644 test-suite/success/primitiveproj.v (limited to 'test-suite/success/primitiveproj.v') diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v new file mode 100644 index 00000000..068f8ac3 --- /dev/null +++ b/test-suite/success/primitiveproj.v @@ -0,0 +1,190 @@ +Set Primitive Projections. +Set Record Elimination Schemes. +Module Prim. + +Record F := { a : nat; b : a = a }. +Record G (A : Type) := { c : A; d : F }. + +Check c. +End Prim. +Module Univ. +Set Universe Polymorphism. +Set Implicit Arguments. +Record Foo (A : Type) := { foo : A }. + +Record G (A : Type) := { c : A; d : c = c; e : Foo A }. + +Definition Foon : Foo nat := {| foo := 0 |}. + +Definition Foonp : nat := Foon.(foo). + +Definition Gt : G nat := {| c:= 0; d:=eq_refl; e:= Foon |}. + +Check (Gt.(e)). + +Section bla. + + Record bar := { baz : nat; def := 0; baz' : forall x, x = baz \/ x = def }. +End bla. + +End Univ. + +Set Primitive Projections. +Unset Elimination Schemes. +Set Implicit Arguments. + +Check nat. + +(* Inductive X (U:Type) := Foo (k : nat) (x : X U). *) +(* Parameter x : X nat. *) +(* Check x.(k). *) + +Inductive X (U:Type) := { k : nat; a: k = k -> X U; b : let x := a eq_refl in X U }. + +Parameter x:X nat. +Check (a x : forall _ : @eq nat (k x) (k x), X nat). +Check (b x : X nat). + +Inductive Y := { next : option Y }. + +Check _.(next) : option Y. +Lemma eta_ind (y : Y) : y = Build_Y y.(next). +Proof. reflexivity. Defined. + +Variable t : Y. + +Fixpoint yn (n : nat) (y : Y) : Y := + match n with + | 0 => t + | S n => {| next := Some (yn n y) |} + end. + +Lemma eta_ind' (y: Y) : Some (yn 100 y) = Some {| next := (yn 100 y).(next) |}. +Proof. reflexivity. Defined. + + +(* + Rules for parsing and printing of primitive projections and their eta expansions. + If r : R A where R is a primitive record with implicit parameter A. + If p : forall {A} (r : R A) {A : Set}, list (A * B). +*) + +Record R {A : Type} := { p : forall {X : Set}, A * X }. +Arguments R : clear implicits. + +Record R' {A : Type} := { p' : forall X : Set, A * X }. +Arguments R' : clear implicits. + +Unset Printing All. + +Parameter r : R nat. + +Check (r.(p)). +Set Printing Projections. +Check (r.(p)). +Unset Printing Projections. +Set Printing All. +Check (r.(p)). +Unset Printing All. + +(* Check (r.(p)). + Elaborates to a primitive application, X arg implicit. + Of type nat * ?ex + No Printing All: p r + Set Printing Projections.: r.(p) + Printing All: r.(@p) ?ex + *) + +Check p r. +Set Printing Projections. +Check p r. +Unset Printing Projections. +Set Printing All. +Check p r. +Unset Printing All. + +Check p r (X:=nat). +Set Printing Projections. +Check p r (X:=nat). +Unset Printing Projections. +Set Printing All. +Check p r (X:=nat). +Unset Printing All. + +(* Same elaboration, printing for p r *) + +(** Explicit version of the primitive projection, under applied w.r.t implicit arguments + can be printed only using projection notation. r.(@p) *) +Check r.(@p _). +Set Printing Projections. +Check r.(@p _). +Unset Printing Projections. +Set Printing All. +Check r.(@p _). +Unset Printing All. + +(** Explicit version of the primitive projection, applied to its implicit arguments + can be printed using application notation r.(p), r.(@p) in fully explicit form *) +Check r.(@p _) nat. +Set Printing Projections. +Check r.(@p _) nat. +Unset Printing Projections. +Set Printing All. +Check r.(@p _) nat. +Unset Printing All. + +Parameter r' : R' nat. + +Check (r'.(p')). +Set Printing Projections. +Check (r'.(p')). +Unset Printing Projections. +Set Printing All. +Check (r'.(p')). +Unset Printing All. + +(* Check (r'.(p')). + Elaborates to a primitive application, X arg explicit. + Of type forall X : Set, nat * X + No Printing All: p' r' + Set Printing Projections.: r'.(p') + Printing All: r'.(@p') + *) + +Check p' r'. +Set Printing Projections. +Check p' r'. +Unset Printing Projections. +Set Printing All. +Check p' r'. +Unset Printing All. + +(* Same elaboration, printing for p r *) + +(** Explicit version of the primitive projection, under applied w.r.t implicit arguments + can be printed only using projection notation. r.(@p) *) +Check r'.(@p' _). +Set Printing Projections. +Check r'.(@p' _). +Unset Printing Projections. +Set Printing All. +Check r'.(@p' _). +Unset Printing All. + +(** Explicit version of the primitive projection, applied to its implicit arguments + can be printed only using projection notation r.(p), r.(@p) in fully explicit form *) +Check p' r' nat. +Set Printing Projections. +Check p' r' nat. +Unset Printing Projections. +Set Printing All. +Check p' r' nat. +Unset Printing All. + +Check (@p' nat). +Check p'. +Set Printing All. + +Check (@p' nat). +Check p'. +Unset Printing All. -- cgit v1.2.3