HigherOrderCO/Kind
1
1
Fork 0
mirror of https://github.com/HigherOrderCO/Kind.git synced 2024-08-17 16:40:28 +03:00
Code Issues Packages Projects Releases Wiki Activity

Add specific Kind2 tests for constructor generation

Browse Source
This commit is contained in:
Eduardo Sandalo Porto 2024-04-11 17:52:12 -03:00
parent 63f0dc3466
commit af819567fd
10 changed files with 18 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
book/Nested/Test.kind2
View File

@ -1,4 +0,0 @@
data Nested/Test T Z
| ctr1 : (Nested/Test T Z)
| ctr2 : (Nested/Test T Z)

2
book/Nested/Test/ctr1.kind2
View File

@ -1,2 +0,0 @@
ctr1 <T> <Z> : (Nested/Test T Z) =
~λP λctr1 λctr2 (ctr1 )

2
book/Nested/Test/ctr2.kind2
View File

@ -1,2 +0,0 @@
ctr2 <T> <Z> : (Nested/Test T Z) =
~λP λctr1 λctr2 (ctr2 )

3
book/Tests/CtrGen/ParamsTest.kind2 Normal file
View File

@ -0,0 +1,3 @@
data Tests/CtrGen/ParamsTest T Z
| ctr1 : (Tests/CtrGen/ParamsTest T Z)
| ctr2 : (Tests/CtrGen/ParamsTest T Z)

2
book/Tests/CtrGen/ParamsTest/ctr1.kind2 Normal file
View File

@ -0,0 +1,2 @@
ctr1 <T> <Z> : (Tests/CtrGen/ParamsTest T Z) =
~λP λctr1 λctr2 (ctr1 )

2
book/Tests/CtrGen/ParamsTest/ctr2.kind2 Normal file
View File

@ -0,0 +1,2 @@
ctr2 <T> <Z> : (Tests/CtrGen/ParamsTest T Z) =
~λP λctr1 λctr2 (ctr2 )

6
book/Tests/CtrGen/VectorTest.kind2 Normal file
View File

@ -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)

2
book/Tests/CtrGen/VectorTest/cons.kind2 Normal file
View File

@ -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)

2
book/Tests/CtrGen/VectorTest/nil.kind2 Normal file
View File

@ -0,0 +1,2 @@
nil <T> : (Tests/CtrGen/VectorTest T Nat/zero) =
~λP λcons λnil (nil )

2
src/book/mod.rs
View File

@ -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 {