diff options
author | Son Ho | 2022-02-03 21:54:08 +0100 |
---|---|---|
committer | Son Ho | 2022-02-03 21:54:08 +0100 |
commit | f2cfba5d716986b2c26d5b7fa28236129f4c5220 (patch) | |
tree | aaf838d4df94791cc133a7ae983c5c9366164508 /rust-tests | |
parent | d8024ac7b85340a33b6034cea620de5b2a2cb5c2 (diff) |
Start working on Assumed.fst
Diffstat (limited to 'rust-tests')
-rw-r--r-- | rust-tests/src/main.rs | 47 |
1 files changed, 47 insertions, 0 deletions
diff --git a/rust-tests/src/main.rs b/rust-tests/src/main.rs index 3e0e7a43..180ecdd6 100644 --- a/rust-tests/src/main.rs +++ b/rust-tests/src/main.rs @@ -77,6 +77,53 @@ fn main() { } println!("\n"); + // Generate the code to print the scalar ranges in F* + for s in &ints_lower { + println!("println!(\"let {}_min : int = {{}}\", {}::MIN);", s, s); + println!("println!(\"let {}_max : int = {{}}\", {}::MAX);", s, s); + } + println!("\n"); + + // Generate the F* definitions for the ranges - this code is + // generated (comes from the above) + println!("let isize_min : int = {}", isize::MIN); + println!("let isize_max : int = {}", isize::MAX); + println!("let i8_min : int = {}", i8::MIN); + println!("let i8_max : int = {}", i8::MAX); + println!("let i16_min : int = {}", i16::MIN); + println!("let i16_max : int = {}", i16::MAX); + println!("let i32_min : int = {}", i32::MIN); + println!("let i32_max : int = {}", i32::MAX); + println!("let i64_min : int = {}", i64::MIN); + println!("let i64_max : int = {}", i64::MAX); + println!("let i128_min : int = {}", i128::MIN); + println!("let i128_max : int = {}", i128::MAX); + println!("let usize_min : int = {}", usize::MIN); + println!("let usize_max : int = {}", usize::MAX); + println!("let u8_min : int = {}", u8::MIN); + println!("let u8_max : int = {}", u8::MAX); + println!("let u16_min : int = {}", u16::MIN); + println!("let u16_max : int = {}", u16::MAX); + println!("let u32_min : int = {}", u32::MIN); + println!("let u32_max : int = {}", u32::MAX); + println!("let u64_min : int = {}", u64::MIN); + println!("let u64_max : int = {}", u64::MAX); + println!("let u128_min : int = {}", u128::MIN); + println!("let u128_max : int = {}", u128::MAX); + println!("\n"); + + // Generate the body for the ScalarTy definition + for (_lo, up) in &ints_pairs { + println!("| {}", up); + } + println!("\n"); + + // Generate the body for the max/min F* functions + for (lo, up) in &ints_pairs { + println!("| {} -> {}_min", up, lo); + } + println!("\n"); + // Modulo tests test_modulo(1, 2); test_modulo(-1, 2); |