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 : (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 : (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 : (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 : (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 (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 : (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 {