GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-11-11 00:26:13 +03:00
Code Issues Projects Releases Wiki Activity

Add a couple of tests with Z

Browse Source
This commit is contained in:
Iavor Diatchki 2022-09-23 17:13:14 +03:00
parent 741959f918
commit c3f6181204
5 changed files with 18 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
tests/ffi/test-ffi.c
View File

@ -129,6 +129,14 @@ void i2Q(mpz_t in, mpq_t out) {
mpq_set_num(out, in);
}
void i2Z5(mpz_t in, mpz_t out) {
mpz_set(out, in);
}
void i2Z(size_t s, mpz_t in, mpz_t out) {
mpz_set_ui(out, s+1);
}
void i2Qs(mpz_t in, mpq_t *out) {
mpq_set_num(out[0], in);
mpq_inv(out[1], out[0]);

2
tests/ffi/test-ffi.cry
View File

@ -47,5 +47,7 @@ foreign nestedSeq : {n, m, p} (fin n, fin m, fin p, n * m * p == 4 * 3 * 2) =>
foreign i2Q : Integer -> Rational
foreign i2Qs : Integer -> [2]Rational
foreign iQ2Qi : (Integer,Rational) -> (Rational,Integer)
foreign i2Z5 : Integer -> Z 5
foreign i2Z : {n} (fin n, n >= 1) => Integer -> Z n

2
tests/ffi/test-ffi.h
View File

@ -24,3 +24,5 @@ void nestedSeq(size_t n, size_t m, size_t p, uint8_t * in, uint8_t * out);
void i2Q(mpz_t in, mpq_t out);
void i2Qs(mpz_t in, mpq_t * out);
void iQ2Qi(mpz_t in_0, mpq_t in_1, mpq_t out_0, mpz_t out_1);
void i2Z5(mpz_t in, mpz_t out);
void i2Z(size_t n, mpz_t in, mpz_t out);

3
tests/ffi/test-ffi.icry
View File

@ -38,3 +38,6 @@ nestedSeq [split`{4} x | x <- split`{2} [1..24]]
i2Q 2
i2Qs 4
iQ2Qi (72,37)
i2Z5 2
i2Z5 10
i2Z 123 : Z 10

3
tests/ffi/test-ffi.icry.stdout
View File

@ -39,3 +39,6 @@ True
(ratio 2 1)
[(ratio 4 1), (ratio 1 4)]
((ratio 37 1), 72)
2
0
1