Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1,027 changes: 1,010 additions & 17 deletions test-harness/src/snapshots/toolchain__lean-tests into-lean.snap

Large diffs are not rendered by default.

95 changes: 94 additions & 1 deletion tests/lean-tests/src/array.rs
Original file line number Diff line number Diff line change
@@ -1,8 +1,101 @@
// Arrays with const generic sizes
//! Tests on arrays
#![allow(dead_code)]
#![allow(unused_variables)]

// Arrays with const generic sizes (existing)
fn f<const N: usize>(x: [u8; N]) {}

fn g<const N: usize>(x: [u8; N]) {
f(x);
f([0u8; 10]);
}

// Array literals
fn array_literals() {
let _empty: [u32; 0] = [];
let _one = [42u32];
let _three = [1u32, 2, 3];
let _five = [10u8, 20, 30, 40, 50];
let _bools = [true, false, true];
let _chars = ['a', 'b', 'c'];
}

// Array repeat syntax
fn array_repeat() {
let _zeros = [0u32; 5];
let _ones = [1u8; 10];
let _falses = [false; 3];
}

// Array indexing
fn array_index(arr: [u32; 5]) -> u32 {
let first = arr[0];
let last = arr[4];
first + last
}

// Array element access in expressions
fn array_in_expr(arr: [u32; 3]) -> u32 {
arr[0] + arr[1] * arr[2]
}

// Array as function argument and return
fn sum_array_3(arr: [u32; 3]) -> u32 {
arr[0] + arr[1] + arr[2]
}

fn make_array(a: u32, b: u32, c: u32) -> [u32; 3] {
[a, b, c]
}

// Nested arrays
fn nested_arrays() {
let _matrix: [[u32; 3]; 2] = [[1, 2, 3], [4, 5, 6]];
let _access = _matrix[0][1];
let _row = _matrix[1];
}

// Array of tuples
fn array_of_tuples() -> [(u32, u32); 3] {
[(1, 2), (3, 4), (5, 6)]
}

// Array with const generic arithmetic
fn double_array<const N: usize>(a: [u32; N], b: [u32; N]) -> u32 {
a[0] + b[0]
}

// Pattern matching on arrays
fn match_array(arr: [u32; 3]) -> u32 {
let [a, b, c] = arr;
a + b + c
}

fn match_array_nested(arr: [[u32; 2]; 2]) -> u32 {
let [[a, b], [c, d]] = arr;
a + b + c + d
}

// Array of structs
struct Point {
x: u32,
y: u32,
}

fn array_of_structs() -> [Point; 2] {
[Point { x: 0, y: 1 }, Point { x: 2, y: 3 }]
}

// Passing array by reference
fn sum_ref(arr: &[u32; 4]) -> u32 {
arr[0] + arr[1] + arr[2] + arr[3]
}

// Const generic size in struct
struct Buffer<const N: usize> {
data: [u8; N],
}

fn make_buffer() -> Buffer<16> {
Buffer { data: [0u8; 16] }
}
2 changes: 2 additions & 0 deletions tests/lean-tests/src/binops.rs
Original file line number Diff line number Diff line change
Expand Up @@ -74,6 +74,7 @@ fn ge_int(x : i32, y: i32) -> bool { x >= y }

struct S;

#[hax_lib::exclude]
impl std::ops::Not for S {
type Output = S;
fn not(self) -> S {
Expand All @@ -88,6 +89,7 @@ impl std::ops::Add for S {
}
}

#[hax_lib::exclude]
fn not_s(x: S) -> S { !x }

fn add_s(x: S, y: S) -> S { x + y }
32 changes: 26 additions & 6 deletions tests/lean-tests/src/floats.rs
Original file line number Diff line number Diff line change
@@ -1,16 +1,36 @@
// Tests on floats
//! Tests on floats
#![allow(dead_code)]
#![allow(unused_variables)]

// Float constants
const N: f32 = 1.0;
const PI_F32: f32 = 3.14159;
const PI_F64: f64 = 3.141592653589793;
const NEG_ONE: f64 = -1.0;

fn test() {
let l0 = 1.0;
let l1 = 0.9;
let l2 = 5.0f32;
let l5 = N;
// Basic float literals
fn float_literals() {
let _l0 = 1.0;
let _l1 = 0.9;
let _l2 = 5.0f32;
let _l3 = N;
let _l4 = 0.0f64;
let _l5 = -3.14;
let _l6 = 1.0e10;
let _l7 = 2.5E-3;
let _l8 = 100.0f64;
}

// Float as function args and return
fn f(x: f64, y: f32) -> f32 {
y
}
// Float in tuple
fn float_tuple() -> (f32, f64) {
(1.5f32, 2.5f64)
}

// Float in array
fn float_array() -> [f64; 3] {
[1.0, 2.0, 3.0]
}
48 changes: 48 additions & 0 deletions tests/lean-tests/src/guards.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,48 @@
//! Tests for match guards
#![allow(dead_code)]
#![allow(unused_variables)]

// Basic if guard with boolean condition
fn simple_if_guard(x: Option<i32>) -> i32 {
match x {
Some(v) if v > 0 => v,
Some(v) if v < -10 => -v,
Some(_) => 0,
None => -1,
}
}

// Guard referencing outer variable
fn guard_with_outer(x: Option<i32>, threshold: i32) -> i32 {
match x {
Some(v) if v > threshold => v - threshold,
Some(v) => v,
None => 0,
}
}

// Guard on enum variants
enum Shape {
Circle(u32),
Rect(u32, u32),
Square(u32),
}

fn area_filter(s: Shape, min_area: u32) -> bool {
match s {
Shape::Circle(r) if r * r > min_area => true,
Shape::Rect(w, h) if w * h > min_area => true,
Shape::Square(s) if s * s > min_area => true,
_ => false,
}
}

// Guard on nested option
fn nested_option_guard(x: Option<Option<i32>>) -> i32 {
match x {
Some(Some(v)) if v > 0 => v,
Some(Some(v)) => -v,
Some(None) => -1,
None => -2,
}
}
129 changes: 129 additions & 0 deletions tests/lean-tests/src/ite.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2,11 +2,13 @@
#![allow(dead_code)]
#![allow(unused_variables)]

// Basic if-then-else as expression
fn test1() -> i32 {
let x = if true { 0 } else { 1 };
if false { 2 } else { 3 }
}

// If-then-else with mutation
fn test2(b: bool) -> i32 {
let x = if b { 0 } else { 9 };
let mut y = 0;
Expand All @@ -23,3 +25,130 @@ fn test2(b: bool) -> i32 {
z + y + x
}
}

// if-let with Option
fn if_let_option(x: Option<u32>) -> u32 {
if let Some(v) = x { v + 1 } else { 0 }
}

// if-let with Result
fn if_let_result(x: Result<u32, i32>) -> u32 {
if let Ok(v) = x { v * 2 } else { 0 }
}

// Chained if-let / else-if-let
fn chained_if_let(a: Option<u32>, b: Option<u32>) -> u32 {
if let Some(x) = a {
x
} else if let Some(y) = b {
y
} else {
0
}
}

// if-let with tuple destructuring
fn if_let_tuple(x: Option<(u32, u32)>) -> u32 {
if let Some((a, b)) = x { a + b } else { 0 }
}

// if-let with nested pattern
fn if_let_nested(x: Option<Option<u32>>) -> u32 {
if let Some(Some(v)) = x { v } else { 0 }
}

// if-let with enum variant
enum Action {
Move(i32, i32),
Rotate(f32),
Stop,
}

fn handle_move(a: Action) -> (i32, i32) {
if let Action::Move(dx, dy) = a {
(dx, dy)
} else {
(0, 0)
}
}

// Deeply nested if-else
fn deeply_nested(a: bool, b: bool, c: bool) -> u32 {
if a {
if b {
if c { 1 } else { 2 }
} else {
if c { 3 } else { 4 }
}
} else {
if b {
if c { 5 } else { 6 }
} else {
if c { 7 } else { 8 }
}
}
}

// if-else as argument to function
fn use_as_arg(b: bool) -> u32 {
let f = |x: u32| x + 1;
f(if b { 10 } else { 20 })
}

// if returning unit (statement-like)
fn if_unit(b: bool) -> u32 {
let mut x = 0;
if b {
x = 1;
}
if !b {
x = 2;
}
x
}

// Chained else-if (not if-let)
fn chained_else_if(x: u32) -> &'static str {
if x == 0 {
"zero"
} else if x == 1 {
"one"
} else if x < 10 {
"small"
} else if x < 100 {
"medium"
} else {
"large"
}
}

// if-let with struct
struct Config {
value: u32,
}

enum Setting {
On(Config),
Off,
}

fn read_config(s: Setting) -> u32 {
if let Setting::On(Config { value }) = s {
value
} else {
0
}
}

// if in loop
fn if_in_loop(n: u32) -> u32 {
let mut count = 0u32;
let mut i = 0u32;
while i < n {
if i % 2 == 0 {
count = count + 1;
}
i = i + 1;
}
count
}
Loading
Loading