From af819567fd69ed990224a43038d90752a03747ad Mon Sep 17 00:00:00 2001
From: Eduardo Sandalo Porto <edu@sandalo.dev>
Date: Thu, 11 Apr 2024 17:52:12 -0300
Subject: [PATCH] Add specific Kind2 tests for constructor generation

---
 book/Nested/Test.kind2                  | 4 ----
 book/Nested/Test/ctr1.kind2             | 2 --
 book/Nested/Test/ctr2.kind2             | 2 --
 book/Tests/CtrGen/ParamsTest.kind2      | 3 +++
 book/Tests/CtrGen/ParamsTest/ctr1.kind2 | 2 ++
 book/Tests/CtrGen/ParamsTest/ctr2.kind2 | 2 ++
 book/Tests/CtrGen/VectorTest.kind2      | 6 ++++++
 book/Tests/CtrGen/VectorTest/cons.kind2 | 2 ++
 book/Tests/CtrGen/VectorTest/nil.kind2  | 2 ++
 src/book/mod.rs                         | 2 +-
 10 files changed, 18 insertions(+), 9 deletions(-)
 delete mode 100644 book/Nested/Test.kind2
 delete mode 100644 book/Nested/Test/ctr1.kind2
 delete mode 100644 book/Nested/Test/ctr2.kind2
 create mode 100644 book/Tests/CtrGen/ParamsTest.kind2
 create mode 100644 book/Tests/CtrGen/ParamsTest/ctr1.kind2
 create mode 100644 book/Tests/CtrGen/ParamsTest/ctr2.kind2
 create mode 100644 book/Tests/CtrGen/VectorTest.kind2
 create mode 100644 book/Tests/CtrGen/VectorTest/cons.kind2
 create mode 100644 book/Tests/CtrGen/VectorTest/nil.kind2

diff --git a/book/Nested/Test.kind2 b/book/Nested/Test.kind2
deleted file mode 100644
index 40ffccb6..00000000
--- a/book/Nested/Test.kind2
+++ /dev/null
@@ -1,4 +0,0 @@
-data Nested/Test T Z
-| ctr1 : (Nested/Test T Z)
-| ctr2 : (Nested/Test T Z)
-
diff --git a/book/Nested/Test/ctr1.kind2 b/book/Nested/Test/ctr1.kind2
deleted file mode 100644
index d2dbb912..00000000
--- a/book/Nested/Test/ctr1.kind2
+++ /dev/null
@@ -1,2 +0,0 @@
-ctr1 <T> <Z> : (Nested/Test T Z) =
-  ~λP λctr1 λctr2 (ctr1 )
\ No newline at end of file
diff --git a/book/Nested/Test/ctr2.kind2 b/book/Nested/Test/ctr2.kind2
deleted file mode 100644
index 84300810..00000000
--- a/book/Nested/Test/ctr2.kind2
+++ /dev/null
@@ -1,2 +0,0 @@
-ctr2 <T> <Z> : (Nested/Test T Z) =
-  ~λP λctr1 λctr2 (ctr2 )
\ No newline at end of file
diff --git a/book/Tests/CtrGen/ParamsTest.kind2 b/book/Tests/CtrGen/ParamsTest.kind2
new file mode 100644
index 00000000..98df41e1
--- /dev/null
+++ b/book/Tests/CtrGen/ParamsTest.kind2
@@ -0,0 +1,3 @@
+data Tests/CtrGen/ParamsTest T Z
+| ctr1 : (Tests/CtrGen/ParamsTest T Z)
+| ctr2 : (Tests/CtrGen/ParamsTest T Z)
diff --git a/book/Tests/CtrGen/ParamsTest/ctr1.kind2 b/book/Tests/CtrGen/ParamsTest/ctr1.kind2
new file mode 100644
index 00000000..3a4b4e28
--- /dev/null
+++ b/book/Tests/CtrGen/ParamsTest/ctr1.kind2
@@ -0,0 +1,2 @@
+ctr1 <T> <Z> : (Tests/CtrGen/ParamsTest T Z) =
+  ~λP λctr1 λctr2 (ctr1 )
\ No newline at end of file
diff --git a/book/Tests/CtrGen/ParamsTest/ctr2.kind2 b/book/Tests/CtrGen/ParamsTest/ctr2.kind2
new file mode 100644
index 00000000..cf1c103f
--- /dev/null
+++ b/book/Tests/CtrGen/ParamsTest/ctr2.kind2
@@ -0,0 +1,2 @@
+ctr2 <T> <Z> : (Tests/CtrGen/ParamsTest T Z) =
+  ~λP λctr1 λctr2 (ctr2 )
\ No newline at end of file
diff --git a/book/Tests/CtrGen/VectorTest.kind2 b/book/Tests/CtrGen/VectorTest.kind2
new file mode 100644
index 00000000..6533cfb5
--- /dev/null
+++ b/book/Tests/CtrGen/VectorTest.kind2
@@ -0,0 +1,6 @@
+data Tests/CtrGen/VectorTest T (len: Nat)
+| cons (len: Nat)
+       (head: T)
+       (tail: (Tests/CtrGen/VectorTest T len)) :
+       (Tests/CtrGen/VectorTest T (Nat/succ len))
+| nil : (Tests/CtrGen/VectorTest T Nat/zero)
diff --git a/book/Tests/CtrGen/VectorTest/cons.kind2 b/book/Tests/CtrGen/VectorTest/cons.kind2
new file mode 100644
index 00000000..07c44753
--- /dev/null
+++ b/book/Tests/CtrGen/VectorTest/cons.kind2
@@ -0,0 +1,2 @@
+cons <T> (len: Nat) (head: T) (tail: (Tests/CtrGen/VectorTest T len)): (Tests/CtrGen/VectorTest T (Nat/succ len)) =
+  ~λP λcons λnil (cons len head tail)
\ No newline at end of file
diff --git a/book/Tests/CtrGen/VectorTest/nil.kind2 b/book/Tests/CtrGen/VectorTest/nil.kind2
new file mode 100644
index 00000000..ef3c76e6
--- /dev/null
+++ b/book/Tests/CtrGen/VectorTest/nil.kind2
@@ -0,0 +1,2 @@
+nil <T> : (Tests/CtrGen/VectorTest T Nat/zero) =
+  ~λP λcons λnil (nil )
\ No newline at end of file
diff --git a/src/book/mod.rs b/src/book/mod.rs
index ec3a0b60..fbd1fdc2 100644
--- a/src/book/mod.rs
+++ b/src/book/mod.rs
@@ -228,7 +228,7 @@ mod tests {
     let book_dir = PathBuf::from(env!("CARGO_MANIFEST_DIR")).join("book");
     let modules_to_test = [
       "BBT", "BMap", "Bool", "Char", "Cmp", "Empty", "Equal", "List", "Maybe", "Monad", "Nat", "Pair",
-      "String", "Vector", "Nested/Test"
+      "String", "Vector", "Tests/CtrGen/ParamsTest", "Tests/CtrGen/VectorTest"
     ];
 
     for module in modules_to_test {