aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-06-19 12:55:48 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-06-24 16:33:29 +0200
commite82b364a070513fe660598588f5a6e8111460adf (patch)
tree8f17328fd21f827078c3c6199d76cb7cac6c80e3
parente8eb53266491bfdd8dd40e8bc6df4399fb23c592 (diff)
Adding various tests for mutual records.
-rw-r--r--test-suite/success/mutual_record.v57
-rw-r--r--test-suite/success/vm_records.v40
2 files changed, 97 insertions, 0 deletions
diff --git a/test-suite/success/mutual_record.v b/test-suite/success/mutual_record.v
new file mode 100644
index 000000000..77529733b
--- /dev/null
+++ b/test-suite/success/mutual_record.v
@@ -0,0 +1,57 @@
+Module M0.
+
+Inductive foo (A : Type) := Foo {
+ foo0 : option (bar A);
+ foo1 : nat;
+ foo2 := foo1 = 0;
+ foo3 : foo2;
+}
+
+with bar (A : Type) := Bar {
+ bar0 : A;
+ bar1 := 0;
+ bar2 : bar1 = 0;
+ bar3 : nat -> foo A;
+}.
+
+End M0.
+
+Module M1.
+
+Set Primitive Projections.
+
+Inductive foo (A : Type) := Foo {
+ foo0 : option (bar A);
+ foo1 : nat;
+ foo2 := foo1 = 0;
+ foo3 : foo2;
+}
+
+with bar (A : Type) := Bar {
+ bar0 : A;
+ bar1 := 0;
+ bar2 : bar1 = 0;
+ bar3 : nat -> foo A;
+}.
+
+End M1.
+
+Module M2.
+
+Set Primitive Projections.
+
+CoInductive foo (A : Type) := Foo {
+ foo0 : option (bar A);
+ foo1 : nat;
+ foo2 := foo1 = 0;
+ foo3 : foo2;
+}
+
+with bar (A : Type) := Bar {
+ bar0 : A;
+ bar1 := 0;
+ bar2 : bar1 = 0;
+ bar3 : nat -> foo A;
+}.
+
+End M2.
diff --git a/test-suite/success/vm_records.v b/test-suite/success/vm_records.v
new file mode 100644
index 000000000..8a1544c8e
--- /dev/null
+++ b/test-suite/success/vm_records.v
@@ -0,0 +1,40 @@
+Set Primitive Projections.
+
+Module M.
+
+CoInductive foo := Foo {
+ foo0 : foo;
+ foo1 : bar;
+}
+with bar := Bar {
+ bar0 : foo;
+ bar1 : bar;
+}.
+
+CoFixpoint f : foo := Foo f g
+with g : bar := Bar f g.
+
+Check (@eq_refl _ g.(bar0) <: f.(foo0).(foo0) = g.(bar0)).
+Check (@eq_refl _ g <: g.(bar1).(bar0).(foo1) = g).
+
+End M.
+
+Module N.
+
+Inductive foo := Foo {
+ foo0 : option foo;
+ foo1 : list bar;
+}
+with bar := Bar {
+ bar0 : option bar;
+ bar1 : list foo;
+}.
+
+Definition f_0 := Foo None nil.
+Definition g_0 := Bar None nil.
+
+Definition f := Foo (Some f_0) (cons g_0 nil).
+
+Check (@eq_refl _ f.(foo1) <: f.(foo1) = cons g_0 nil).
+
+End N.