From 17edc1d615d8cd591dec1881e512933c89ff71b9 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 27 Jan 2021 16:26:03 -0800
Subject: [PATCH] test: inductive types for testing `SizeOf.lean`

---
 tests/lean/run/sizeof1.lean | 14 ++++++++++++++
 tests/lean/run/sizeof2.lean | 12 ++++++++++++
 tests/lean/run/sizeof3.lean | 23 +++++++++++++++++++++++
 tests/lean/run/sizeof4.lean | 14 ++++++++++++++
 tests/lean/run/sizeof5.lean | 10 ++++++++++
 5 files changed, 73 insertions(+)
 create mode 100644 tests/lean/run/sizeof1.lean
 create mode 100644 tests/lean/run/sizeof2.lean
 create mode 100644 tests/lean/run/sizeof3.lean
 create mode 100644 tests/lean/run/sizeof4.lean
 create mode 100644 tests/lean/run/sizeof5.lean

diff --git a/tests/lean/run/sizeof1.lean b/tests/lean/run/sizeof1.lean
new file mode 100644
index 0000000000..a8307e7ad7
--- /dev/null
+++ b/tests/lean/run/sizeof1.lean
@@ -0,0 +1,14 @@
+mutual
+
+inductive TreePos (α : Type u) (β : Type v) where
+  | leaf (a : α)
+  | node (children : List (List (TreeNeg α β)))
+
+inductive TreeNeg (α : Type u) (β : Type v) where
+  | leaf (a : β)
+  | node (children : List (List (TreePos α β)))
+
+end
+
+#print TreePos.leaf.sizeOf_spec
+#print TreePos.node.sizeOf_spec
diff --git a/tests/lean/run/sizeof2.lean b/tests/lean/run/sizeof2.lean
new file mode 100644
index 0000000000..929ba9a182
--- /dev/null
+++ b/tests/lean/run/sizeof2.lean
@@ -0,0 +1,12 @@
+mutual
+
+  inductive Arg (α : Type u) where
+    | val  (a : α)
+    | expr (e : Expr α)
+
+  inductive Expr (α : Type u) where
+    | app (f : String) (a : List (Arg α))
+
+end
+
+#print Expr.app.sizeOf_spec
diff --git a/tests/lean/run/sizeof3.lean b/tests/lean/run/sizeof3.lean
new file mode 100644
index 0000000000..c82385f3cf
--- /dev/null
+++ b/tests/lean/run/sizeof3.lean
@@ -0,0 +1,23 @@
+set_option trace.Meta.sizeOf true in
+mutual
+  inductive AList (α β : Type u)
+    | nil
+    | cons (a : α) (t : BList α β)
+
+  inductive BList (α β : Type u)
+    | cons (b : β) (t : AList α β)
+end
+
+#print AList.nil.sizeOf_spec
+#print AList.cons.sizeOf_spec
+#print BList.cons.sizeOf_spec
+
+mutual
+  inductive Foo (α : Type u)
+    | mk (cs : AList (Foo α) (Boo α))
+
+  inductive Boo (α : Type u)
+    | mk (a : α) (cs : BList (Foo α) (Boo α))
+end
+
+#print Boo.mk.sizeOf_spec
diff --git a/tests/lean/run/sizeof4.lean b/tests/lean/run/sizeof4.lean
new file mode 100644
index 0000000000..5e66efa29c
--- /dev/null
+++ b/tests/lean/run/sizeof4.lean
@@ -0,0 +1,14 @@
+inductive Foo (β : Type u) : Sort v → Type (max u v)
+  | mk {α : Sort v} (b : β) (a : α) : Foo β α
+
+inductive Bla (α : Type u) : Type (u+1) where
+  | mk₁ (x : Foo (Bla α) Nat)
+  | mk₂ (n m : Nat) (x : Foo (Bla α) (n = m))
+
+#print Bla.rec
+
+#print Bla._sizeOf_1
+#print Bla._sizeOf_2
+#print Bla._sizeOf_3
+#print Bla.mk₁.sizeOf_spec
+#print Bla.mk₂.sizeOf_spec
diff --git a/tests/lean/run/sizeof5.lean b/tests/lean/run/sizeof5.lean
new file mode 100644
index 0000000000..e857b8695c
--- /dev/null
+++ b/tests/lean/run/sizeof5.lean
@@ -0,0 +1,10 @@
+inductive Vec (α : Type u) : Nat → Type u where
+  | nil  : Vec α 0
+  | cons : α → {n : Nat} → Vec α n → Vec α (n+1)
+
+inductive Expr where
+  | app2 (f : String) (args : Vec Expr 2)
+  | app3 (f : String) (args : Vec Expr 3)
+
+#print Expr.app2.sizeOf_spec
+#print Expr.app3.sizeOf_spec