diff --git a/test-harness/src/snapshots/toolchain__lean-tests into-lean.snap b/test-harness/src/snapshots/toolchain__lean-tests into-lean.snap index c9bd78693..d3e949942 100644 --- a/test-harness/src/snapshots/toolchain__lean-tests into-lean.snap +++ b/test-harness/src/snapshots/toolchain__lean-tests into-lean.snap @@ -57,6 +57,110 @@ def g (N : usize) (x : (RustArray u8 N)) : (f ((10 : usize)) (← (rust_primitives.hax.repeat (0 : u8) (10 : usize)))); (pure rust_primitives.hax.Tuple0.mk) +@[spec] +def array_literals (_ : rust_primitives.hax.Tuple0) : + RustM rust_primitives.hax.Tuple0 := do + let _empty : (RustArray u32 0) := (RustArray.ofVec #v[]); + let _one : (RustArray u32 1) := (RustArray.ofVec #v[(42 : u32)]); + let _three : (RustArray u32 3) := + (RustArray.ofVec #v[(1 : u32), (2 : u32), (3 : u32)]); + let _five : (RustArray u8 5) := + (RustArray.ofVec #v[(10 : u8), (20 : u8), (30 : u8), (40 : u8), (50 : u8)]); + let _bools : (RustArray Bool 3) := (RustArray.ofVec #v[true, false, true]); + let _chars : (RustArray Char 3) := (RustArray.ofVec #v['a', 'b', 'c']); + (pure rust_primitives.hax.Tuple0.mk) + +@[spec] +def array_repeat (_ : rust_primitives.hax.Tuple0) : + RustM rust_primitives.hax.Tuple0 := do + let _zeros : (RustArray u32 5) ← + (rust_primitives.hax.repeat (0 : u32) (5 : usize)); + let _ones : (RustArray u8 10) ← + (rust_primitives.hax.repeat (1 : u8) (10 : usize)); + let _falses : (RustArray Bool 3) ← + (rust_primitives.hax.repeat false (3 : usize)); + (pure rust_primitives.hax.Tuple0.mk) + +@[spec] +def array_index (arr : (RustArray u32 5)) : RustM u32 := do + let first : u32 ← arr[(0 : usize)]_?; + let last : u32 ← arr[(4 : usize)]_?; + (first +? last) + +@[spec] +def array_in_expr (arr : (RustArray u32 3)) : RustM u32 := do + ((← arr[(0 : usize)]_?) + +? (← ((← arr[(1 : usize)]_?) *? (← arr[(2 : usize)]_?)))) + +@[spec] +def sum_array_3 (arr : (RustArray u32 3)) : RustM u32 := do + ((← ((← arr[(0 : usize)]_?) +? (← arr[(1 : usize)]_?))) + +? (← arr[(2 : usize)]_?)) + +@[spec] +def make_array (a : u32) (b : u32) (c : u32) : RustM (RustArray u32 3) := do + (pure (RustArray.ofVec #v[a, b, c])) + +@[spec] +def nested_arrays (_ : rust_primitives.hax.Tuple0) : + RustM rust_primitives.hax.Tuple0 := do + let _matrix : (RustArray (RustArray u32 3) 2) := + (RustArray.ofVec #v[(RustArray.ofVec #v[(1 : u32), (2 : u32), (3 : u32)]), + (RustArray.ofVec #v[(4 : u32), + (5 : u32), + (6 : u32)])]); + let _access : u32 ← (← _matrix[(0 : usize)]_?)[(1 : usize)]_?; + let _row : (RustArray u32 3) ← _matrix[(1 : usize)]_?; + (pure rust_primitives.hax.Tuple0.mk) + +@[spec] +def array_of_tuples (_ : rust_primitives.hax.Tuple0) : + RustM (RustArray (rust_primitives.hax.Tuple2 u32 u32) 3) := do + (pure (RustArray.ofVec #v[(rust_primitives.hax.Tuple2.mk (1 : u32) (2 : u32)), + (rust_primitives.hax.Tuple2.mk + (3 : u32) + (4 : u32)), + (rust_primitives.hax.Tuple2.mk + (5 : u32) + (6 : u32))])) + +@[spec] +def double_array (N : usize) (a : (RustArray u32 N)) (b : (RustArray u32 N)) : + RustM u32 := do + ((← a[(0 : usize)]_?) +? (← b[(0 : usize)]_?)) + +@[spec] +def match_array (arr : (RustArray u32 3)) : RustM u32 := do (pure sorry) + +@[spec] +def match_array_nested (arr : (RustArray (RustArray u32 2) 2)) : RustM u32 := do + (pure sorry) + +structure Point where + x : u32 + y : u32 + +@[spec] +def array_of_structs (_ : rust_primitives.hax.Tuple0) : + RustM (RustArray Point 2) := do + (pure (RustArray.ofVec #v[(Point.mk (x := (0 : u32)) (y := (1 : u32))), + (Point.mk (x := (2 : u32)) (y := (3 : u32)))])) + +@[spec] +def sum_ref (arr : (RustArray u32 4)) : RustM u32 := do + ((← ((← ((← arr[(0 : usize)]_?) +? (← arr[(1 : usize)]_?))) + +? (← arr[(2 : usize)]_?))) + +? (← arr[(3 : usize)]_?)) + +structure Buffer (N : usize) where + data : (RustArray u8 N) + +@[spec] +def make_buffer (_ : rust_primitives.hax.Tuple0) : + RustM (Buffer ((16 : usize))) := do + (pure (Buffer.mk + (data := (← (rust_primitives.hax.repeat (0 : u8) (16 : usize)))))) + end lean_tests.array @@ -212,24 +316,13 @@ structure S where -- no fields @[reducible] instance Impl.AssociatedTypes : - core_models.ops.bit.Not.AssociatedTypes S - where - Output := S - -instance Impl : core_models.ops.bit.Not S where - not := fun (self : S) => do (pure self) - -@[reducible] instance Impl_1.AssociatedTypes : core_models.ops.arith.Add.AssociatedTypes S S where Output := S -instance Impl_1 : core_models.ops.arith.Add S S where +instance Impl : core_models.ops.arith.Add S S where add := fun (self : S) (rhs : S) => do (pure self) -@[spec] -def not_s (x : S) : RustM S := do (core_models.ops.bit.Not.not S x) - @[spec] def add_s (x : S) (y : S) : RustM S := do (core_models.ops.arith.Add.add S S x y) @@ -417,21 +510,152 @@ namespace lean_tests.floats def N : f32 := (1.0 : f32) +def PI_F32 : f32 := (3.14159 : f32) + +def PI_F64 : f64 := (3.141592653589793 : f64) + +def NEG_ONE : f64 := (-1.0 : f64) + @[spec] -def test (_ : rust_primitives.hax.Tuple0) : +def float_literals (_ : rust_primitives.hax.Tuple0) : RustM rust_primitives.hax.Tuple0 := do - let l0 : f64 := (1.0 : f64); - let l1 : f64 := (0.9 : f64); - let l2 : f32 := (5.0 : f32); - let l5 : f32 := N; + let _l0 : f64 := (1.0 : f64); + let _l1 : f64 := (0.9 : f64); + let _l2 : f32 := (5.0 : f32); + let _l3 : f32 := N; + let _l4 : f64 := (0.0 : f64); + let _l5 : f64 := (-3.14 : f64); + let _l6 : f64 := (1.0e10 : f64); + let _l7 : f64 := (2.5E-3 : f64); + let _l8 : f64 := (100.0 : f64); (pure rust_primitives.hax.Tuple0.mk) @[spec] def f (x : f64) (y : f32) : RustM f32 := do (pure y) +@[spec] +def float_tuple (_ : rust_primitives.hax.Tuple0) : + RustM (rust_primitives.hax.Tuple2 f32 f64) := do + (pure (rust_primitives.hax.Tuple2.mk (1.5 : f32) (2.5 : f64))) + +@[spec] +def float_array (_ : rust_primitives.hax.Tuple0) : RustM (RustArray f64 3) := do + (pure (RustArray.ofVec #v[(1.0 : f64), (2.0 : f64), (3.0 : f64)])) + end lean_tests.floats +namespace lean_tests.guards + +@[spec] +def simple_if_guard (x : (core_models.option.Option i32)) : RustM i32 := do + match + (← match x with + | (core_models.option.Option.Some v) => do + match (← (v >? (0 : i32))) with + | true => do (pure (core_models.option.Option.Some v)) + | _ => do (pure core_models.option.Option.None) + | _ => do (pure core_models.option.Option.None)) + with + | (core_models.option.Option.Some x) => do (pure x) + | (core_models.option.Option.None ) => do + match + (← match x with + | (core_models.option.Option.Some v) => do + match (← (v do (pure (core_models.option.Option.Some (← (-? v)))) + | _ => do (pure core_models.option.Option.None) + | _ => do (pure core_models.option.Option.None)) + with + | (core_models.option.Option.Some x) => do (pure x) + | (core_models.option.Option.None ) => do + match x with + | (core_models.option.Option.Some _) => do (pure (0 : i32)) + | (core_models.option.Option.None ) => do (pure (-1 : i32)) + +@[spec] +def guard_with_outer (x : (core_models.option.Option i32)) (threshold : i32) : + RustM i32 := do + match + (← match x with + | (core_models.option.Option.Some v) => do + match (← (v >? threshold)) with + | true => do + (pure (core_models.option.Option.Some (← (v -? threshold)))) + | _ => do (pure core_models.option.Option.None) + | _ => do (pure core_models.option.Option.None)) + with + | (core_models.option.Option.Some x) => do (pure x) + | (core_models.option.Option.None ) => do + match x with + | (core_models.option.Option.Some v) => do (pure v) + | (core_models.option.Option.None ) => do (pure (0 : i32)) + +inductive Shape : Type +| Circle : u32 -> Shape +| Rect : u32 -> u32 -> Shape +| Square : u32 -> Shape + +@[spec] +def area_filter (s : Shape) (min_area : u32) : RustM Bool := do + match + (← match s with + | (Shape.Circle r) => do + match (← ((← (r *? r)) >? min_area)) with + | true => do (pure (core_models.option.Option.Some true)) + | _ => do (pure core_models.option.Option.None) + | _ => do (pure core_models.option.Option.None)) + with + | (core_models.option.Option.Some x) => do (pure x) + | (core_models.option.Option.None ) => do + match + (← match s with + | (Shape.Rect w h) => do + match (← ((← (w *? h)) >? min_area)) with + | true => do (pure (core_models.option.Option.Some true)) + | _ => do (pure core_models.option.Option.None) + | _ => do (pure core_models.option.Option.None)) + with + | (core_models.option.Option.Some x) => do (pure x) + | (core_models.option.Option.None ) => do + match + (← match s with + | (Shape.Square s) => do + match (← ((← (s *? s)) >? min_area)) with + | true => do (pure (core_models.option.Option.Some true)) + | _ => do (pure core_models.option.Option.None) + | _ => do (pure core_models.option.Option.None)) + with + | (core_models.option.Option.Some x) => do (pure x) + | (core_models.option.Option.None ) => do (pure false) + +@[spec] +def nested_option_guard + (x : (core_models.option.Option (core_models.option.Option i32))) : + RustM i32 := do + match + (← match x with + | (core_models.option.Option.Some (core_models.option.Option.Some v)) => + do + match (← (v >? (0 : i32))) with + | true => do (pure (core_models.option.Option.Some v)) + | _ => do (pure core_models.option.Option.None) + | _ => do (pure core_models.option.Option.None)) + with + | (core_models.option.Option.Some x) => do (pure x) + | (core_models.option.Option.None ) => do + match x with + | (core_models.option.Option.Some (core_models.option.Option.Some v)) + => do + (-? v) + | (core_models.option.Option.Some (core_models.option.Option.None )) => + do + (pure (-1 : i32)) + | (core_models.option.Option.None ) => do (pure (-2 : i32)) + +end lean_tests.guards + + namespace lean_tests.ite @[spec] @@ -455,9 +679,228 @@ def test2 (b : Bool) : RustM i32 := do let z : i32 ← (y -? x); ((← (z +? y)) +? x) +@[spec] +def if_let_option (x : (core_models.option.Option u32)) : RustM u32 := do + match x with + | (core_models.option.Option.Some v) => do (v +? (1 : u32)) + | _ => do (pure (0 : u32)) + +@[spec] +def if_let_result (x : (core_models.result.Result u32 i32)) : RustM u32 := do + match x with + | (core_models.result.Result.Ok v) => do (v *? (2 : u32)) + | _ => do (pure (0 : u32)) + +@[spec] +def chained_if_let + (a : (core_models.option.Option u32)) + (b : (core_models.option.Option u32)) : + RustM u32 := do + match a with + | (core_models.option.Option.Some x) => do (pure x) + | _ => do + match b with + | (core_models.option.Option.Some y) => do (pure y) + | _ => do (pure (0 : u32)) + +@[spec] +def if_let_tuple + (x : (core_models.option.Option (rust_primitives.hax.Tuple2 u32 u32))) : + RustM u32 := do + match x with + | (core_models.option.Option.Some ⟨a, b⟩) => do (a +? b) + | _ => do (pure (0 : u32)) + +@[spec] +def if_let_nested + (x : (core_models.option.Option (core_models.option.Option u32))) : + RustM u32 := do + match x with + | (core_models.option.Option.Some (core_models.option.Option.Some v)) => + do + (pure v) + | _ => do (pure (0 : u32)) + +inductive Action : Type +| Move : i32 -> i32 -> Action +| Rotate : f32 -> Action +| Stop : Action + +@[spec] +def handle_move (a : Action) : RustM (rust_primitives.hax.Tuple2 i32 i32) := do + match a with + | (Action.Move dx dy) => do (pure (rust_primitives.hax.Tuple2.mk dx dy)) + | _ => do (pure (rust_primitives.hax.Tuple2.mk (0 : i32) (0 : i32))) + +@[spec] +def deeply_nested (a : Bool) (b : Bool) (c : Bool) : RustM u32 := do + if a then do + if b then do + if c then do (pure (1 : u32)) else do (pure (2 : u32)) + else do + if c then do (pure (3 : u32)) else do (pure (4 : u32)) + else do + if b then do + if c then do (pure (5 : u32)) else do (pure (6 : u32)) + else do + if c then do (pure (7 : u32)) else do (pure (8 : u32)) + +@[spec] +def use_as_arg (b : Bool) : RustM u32 := do + let f : (u32 -> RustM u32) := (fun x => (do (x +? (1 : u32)) : RustM u32)); + (core_models.ops.function.Fn.call + (u32 -> RustM u32) + (rust_primitives.hax.Tuple1 u32) + f + (rust_primitives.hax.Tuple1.mk + (← if b then do (pure (10 : u32)) else do (pure (20 : u32))))) + +@[spec] +def if_unit (b : Bool) : RustM u32 := do + let x : u32 := (0 : u32); + let x : u32 ← + if b then do let x : u32 := (1 : u32); (pure x) else do (pure x); + let x : u32 ← + if (← (!? b)) then do let x : u32 := (2 : u32); (pure x) else do (pure x); + (pure x) + +@[spec] +def chained_else_if (x : u32) : RustM String := do + if (← (x ==? (0 : u32))) then do + (pure \"zero\") + else do + if (← (x ==? (1 : u32))) then do + (pure \"one\") + else do + if (← (x Setting +| Off : Setting + +@[spec] +def read_config (s : Setting) : RustM u32 := do + match s with + | (Setting.On {value := value}) => do (pure value) + | _ => do (pure (0 : u32)) + +@[spec] +def if_in_loop (n : u32) : RustM u32 := do + let count : u32 := (0 : u32); + let i : u32 := (0 : u32); + let ⟨count, i⟩ ← + (rust_primitives.hax.while_loop + (fun ⟨count, i⟩ => (do (pure true) : RustM Bool)) + (fun ⟨count, i⟩ => (do (i + (do + (rust_primitives.hax.int.from_machine (0 : u32)) : + RustM hax_lib.int.Int)) + (rust_primitives.hax.Tuple2.mk count i) + (fun ⟨count, i⟩ => + (do + let count : u32 ← + if (← ((← (i %? (2 : u32))) ==? (0 : u32))) then do + let count : u32 ← (count +? (1 : u32)); + (pure count) + else do + (pure count); + let i : u32 ← (i +? (1 : u32)); + (pure (rust_primitives.hax.Tuple2.mk count i)) : + RustM (rust_primitives.hax.Tuple2 u32 u32)))); + (pure count) + end lean_tests.ite +namespace lean_tests.let_else + +@[spec] +def basic_option (opt : (core_models.option.Option u32)) : RustM u32 := do + match opt with + | (core_models.option.Option.Some x) => do (x +? (1 : u32)) + | _ => do (pure (0 : u32)) + +@[spec] +def basic_result (res : (core_models.result.Result u32 i32)) : RustM u32 := do + match res with + | (core_models.result.Result.Ok x) => do (x +? (1 : u32)) + | _ => do (pure (0 : u32)) + +@[spec] +def chained + (a : (core_models.option.Option u32)) + (b : (core_models.option.Option u32)) : + RustM u32 := do + match a with + | (core_models.option.Option.Some x) => do + match b with + | (core_models.option.Option.Some y) => do (x +? y) + | _ => do (pure x) + | _ => do (pure (0 : u32)) + +@[spec] +def tuple_destructure + (opt : (core_models.option.Option (rust_primitives.hax.Tuple2 u32 u32))) : + RustM u32 := do + match opt with + | (core_models.option.Option.Some ⟨a, b⟩) => do (a +? b) + | _ => do (pure (0 : u32)) + +structure Point where + x : i32 + y : i32 + +inductive Geom : Type +| Pt : Point -> Geom +| Nothing : Geom + +@[spec] +def struct_let_else (g : Geom) : RustM i32 := do + match g with + | (Geom.Pt {x := x, y := y}) => do (x +? y) + | _ => do (pure (-1 : i32)) + +@[spec] +def nested_option + (opt : (core_models.option.Option (core_models.option.Option u32))) : + RustM u32 := do + match opt with + | (core_models.option.Option.Some inner) => do + match inner with + | (core_models.option.Option.Some v) => do (v +? (2 : u32)) + | _ => do (pure (1 : u32)) + | _ => do (pure (0 : u32)) + +@[spec] +def with_early_return_result (opt : (core_models.option.Option u32)) : + RustM (core_models.result.Result u32 String) := do + match opt with + | (core_models.option.Option.Some x) => do + (pure (core_models.result.Result.Ok (← (x *? (2 : u32))))) + | _ => do (pure (core_models.result.Result.Err \"missing\")) + +inductive Token : Type +| Number : u32 -> Token +| Plus : Token +| Minus : Token +| Eof : Token + +@[spec] +def extract_number (t : Token) : RustM (core_models.option.Option u32) := do + match t with + | (Token.Number n) => do (pure (core_models.option.Option.Some n)) + | _ => do (pure core_models.option.Option.None) + +end lean_tests.let_else + + namespace lean_tests.loops -- Simple for-loop @@ -808,6 +1251,141 @@ def test_ellipsis_tuples (_ : rust_primitives.hax.Tuple0) : &&? (← (d ==? (4 : u8)))))); (pure rust_primitives.hax.Tuple0.mk) +@[spec] +def nested_tuple_match + (x : + (rust_primitives.hax.Tuple2 + (rust_primitives.hax.Tuple2 u32 u32) + (rust_primitives.hax.Tuple2 u32 u32))) : + RustM u32 := do + match x with | ⟨⟨a, b⟩, ⟨c, d⟩⟩ => do ((← ((← (a +? b)) +? c)) +? d) + +@[spec] +def multi_arm (x : u32) : RustM u32 := do + match x with + | 0 => do (pure (100 : u32)) + | 1 => do (pure (200 : u32)) + | 2 => do (pure (300 : u32)) + | 3 => do (pure (400 : u32)) + | _ => do (pure (0 : u32)) + +@[spec] +def match_expressions (x : (core_models.option.Option u32)) : RustM u32 := do + match x with + | (core_models.option.Option.Some v) => do (v *? (2 : u32)) + | (core_models.option.Option.None ) => do (pure (0 : u32)) + +inductive Wrapper : Type +| Single : u32 -> Wrapper +| Pair : u32 -> u32 -> Wrapper +| Empty : Wrapper + +@[spec] +def match_wrapper (w : Wrapper) : RustM u32 := do + match w with + | (Wrapper.Single x) => do (pure x) + | (Wrapper.Pair x y) => do (x +? y) + | (Wrapper.Empty ) => do (pure (0 : u32)) + +@[spec] +def match_nested_option + (x : (core_models.option.Option (core_models.option.Option u32))) : + RustM u32 := do + match x with + | (core_models.option.Option.Some (core_models.option.Option.Some v)) => + do + (pure v) + | (core_models.option.Option.Some (core_models.option.Option.None )) => do + (pure (1 : u32)) + | (core_models.option.Option.None ) => do (pure (2 : u32)) + +@[spec] +def match_result (x : (core_models.result.Result u32 i32)) : RustM u32 := do + match x with + | (core_models.result.Result.Ok v) => do (pure v) + | (core_models.result.Result.Err _) => do (pure (0 : u32)) + +@[spec] +def match_bool_exhaustive (b : Bool) : RustM u32 := do + match b with | true => do (pure (1 : u32)) | false => do (pure (0 : u32)) + +@[spec] +def match_enum_pair + (a : (core_models.option.Option u32)) + (b : (core_models.option.Option u32)) : + RustM u32 := do + match (rust_primitives.hax.Tuple2.mk a b) with + | ⟨(core_models.option.Option.Some x), (core_models.option.Option.Some y)⟩ + => do + (x +? y) + | ⟨(core_models.option.Option.Some x), (core_models.option.Option.None )⟩ + => do + (pure x) + | ⟨(core_models.option.Option.None ), (core_models.option.Option.Some y)⟩ + => do + (pure y) + | ⟨(core_models.option.Option.None ), (core_models.option.Option.None )⟩ => + do + (pure (0 : u32)) + +@[spec] +def deep_pattern + (x : + (core_models.option.Option + (core_models.result.Result (rust_primitives.hax.Tuple2 u32 u32) u32))) : + RustM u32 := do + match x with + | (core_models.option.Option.Some (core_models.result.Result.Ok ⟨a, b⟩)) + => do + (a +? b) + | (core_models.option.Option.Some (core_models.result.Result.Err e)) => do + (pure e) + | (core_models.option.Option.None ) => do (pure (0 : u32)) + +@[spec] +def match_with_block (x : (core_models.option.Option u32)) : RustM u32 := do + match x with + | (core_models.option.Option.Some v) => do + let doubled : u32 ← (v *? (2 : u32)); + let tripled : u32 ← (v *? (3 : u32)); + (doubled +? tripled) + | (core_models.option.Option.None ) => do (pure (42 : u32)) + +@[spec] +def multiple_let_destruct (_ : rust_primitives.hax.Tuple0) : RustM u32 := do + let ⟨a, b⟩ := (rust_primitives.hax.Tuple2.mk (1 : u32) (2 : u32)); + let ⟨c, ⟨d, e⟩⟩ := + (rust_primitives.hax.Tuple2.mk + (3 : u32) + (rust_primitives.hax.Tuple2.mk (4 : u32) (5 : u32))); + ((← ((← ((← (a +? b)) +? c)) +? d)) +? e) + +@[spec] +def at_binding_enum (x : (core_models.option.Option u32)) : RustM u32 := do + match x with + | v@(core_models.option.Option.Some 42) => do (pure (100 : u32)) + | (core_models.option.Option.Some n) => do (pure n) + | (core_models.option.Option.None ) => do (pure (0 : u32)) + +@[spec] +def match_on_ref (x : u32) : RustM u32 := do + match x with + | 0 => do (pure (100 : u32)) + | 1 => do (pure (200 : u32)) + | _ => do (pure (0 : u32)) + +@[spec] +def match_unit (x : u32) : RustM rust_primitives.hax.Tuple0 := do + match x with + | 0 => do (pure rust_primitives.hax.Tuple0.mk) + | _ => do (pure rust_primitives.hax.Tuple0.mk) + +@[spec] +def match_range (x : u32) : RustM String := do (pure sorry) + +@[spec] +def char_class (c : Char) : RustM u32 := do (pure sorry) + end lean_tests.matching @@ -992,6 +1570,262 @@ opaque OpaqueStruct : Type end lean_tests.opaque +namespace lean_tests.pattern_or + +inductive Color : Type +| Red : Color +| Green : Color +| Blue : Color +| Yellow : Color +| Cyan : Color + +@[spec] +def Color_cast_to_repr (x : Color) : RustM isize := do + match x with + | (Color.Red ) => do (pure (0 : isize)) + | (Color.Green ) => do (pure (1 : isize)) + | (Color.Blue ) => do (pure (2 : isize)) + | (Color.Yellow ) => do (pure (3 : isize)) + | (Color.Cyan ) => do (pure (4 : isize)) + +@[spec] +def simple_or (c : Color) : RustM u32 := do + match c with + | (Color.Red ) | (Color.Green ) => do (pure (1 : u32)) + | (Color.Blue ) | (Color.Yellow ) | (Color.Cyan ) => do (pure (2 : u32)) + +@[spec] +def int_or (x : u32) : RustM u32 := do + match x with + | 0 | 1 => do (pure (10 : u32)) + | 2 | 3 | 4 => do (pure (20 : u32)) + | _ => do (pure (30 : u32)) + +@[spec] +def nested_option (x : (core_models.option.Option i32)) : RustM i32 := do + match x with + | (core_models.option.Option.Some 1) | (core_models.option.Option.Some 2) + => do + (pure (1 : i32)) + | (core_models.option.Option.Some 3) | (core_models.option.Option.Some 4) + | (core_models.option.Option.Some 5) => do + (pure (2 : i32)) + | (core_models.option.Option.Some x) => do (pure x) + | (core_models.option.Option.None ) => do (pure (0 : i32)) + +@[spec] +def deep_tuple + (x : (rust_primitives.hax.Tuple2 i32 (core_models.option.Option i32))) : + RustM i32 := do + match x with + | ⟨1, (core_models.option.Option.Some 3)⟩ | ⟨1, + (core_models.option.Option.Some + 4)⟩ | ⟨2, + (core_models.option.Option.Some + 3)⟩ | ⟨2, + (core_models.option.Option.Some + 4)⟩ => + do + (pure (0 : i32)) + | ⟨5, (core_models.option.Option.None )⟩ | ⟨6, + (core_models.option.Option.None + )⟩ => do + (pure (1 : i32)) + | ⟨x, _⟩ => do (pure x) + +@[spec] +def capture_across_or + (x : + (core_models.result.Result + (rust_primitives.hax.Tuple2 i32 i32) + (rust_primitives.hax.Tuple2 i32 i32))) : + RustM i32 := do + match x with + | (core_models.result.Result.Ok ⟨1, y⟩) | (core_models.result.Result.Ok + ⟨2, y⟩) | (core_models.result.Result.Err ⟨3, y⟩) | + (core_models.result.Result.Err ⟨4, y⟩) => do + (pure y) + | (core_models.result.Result.Ok ⟨x, _⟩) | (core_models.result.Result.Err + ⟨x, _⟩) => do + (pure x) + +@[spec] +def let_or (x : (rust_primitives.hax.Tuple2 u8 u8)) : RustM u8 := do + let ⟨a, b⟩ := x; + (a +? b) + +@[spec] +def char_or (c : Char) : RustM u32 := do + match c with + | 'a' | 'e' | 'i' | 'o' | 'u' => do (pure (1 : u32)) + | 'A' | 'E' | 'I' | 'O' | 'U' => do (pure (2 : u32)) + | _ => do (pure (0 : u32)) + +@[spec] +def bool_or (x : Bool) (y : Bool) : RustM u32 := do + match (rust_primitives.hax.Tuple2.mk x y) with + | ⟨true, true⟩ | ⟨false, false⟩ => do (pure (1 : u32)) + | ⟨true, false⟩ | ⟨false, true⟩ => do (pure (2 : u32)) + +inductive Inner : Type +| X : Inner +| Y : u32 -> Inner + +inductive Outer : Type +| A : Inner -> Outer +| B : Inner -> Outer + +@[spec] +def nested_enum_or (o : Outer) : RustM u32 := do + match o with + | (Outer.A (Inner.X )) | (Outer.B (Inner.X )) => do (pure (0 : u32)) + | (Outer.A (Inner.Y v)) | (Outer.B (Inner.Y v)) => do (pure v) + +@[spec] +def or_with_wildcard (x : (rust_primitives.hax.Tuple3 u32 u32 u32)) : + RustM u32 := do + match x with + | ⟨0, _, z⟩ | ⟨1, _, z⟩ => do (pure z) + | ⟨_, 0, z⟩ | ⟨_, 1, z⟩ => do (z +? (1 : u32)) + | ⟨_, _, z⟩ => do (z +? (2 : u32)) + +@[spec] +def or_in_if_let (x : (core_models.option.Option u32)) : RustM u32 := do + match x with + | (core_models.option.Option.Some 1) | (core_models.option.Option.Some 2) + | (core_models.option.Option.Some 3) => do + (pure (42 : u32)) + | _ => do (pure (0 : u32)) + +end lean_tests.pattern_or + + +namespace lean_tests.question_mark + +@[spec] +def option_basic (x : (core_models.option.Option u32)) : + RustM (core_models.option.Option u32) := do + match x with + | (core_models.option.Option.Some v) => do + (pure (core_models.option.Option.Some (← (v +? (1 : u32))))) + | (core_models.option.Option.None ) => do + (pure core_models.option.Option.None) + +@[spec] +def option_multi + (x : (core_models.option.Option u32)) + (y : (core_models.option.Option u32)) : + RustM (core_models.option.Option u32) := do + match x with + | (core_models.option.Option.Some hoist6) => do + match y with + | (core_models.option.Option.Some hoist5) => do + (pure (core_models.option.Option.Some (← (hoist6 +? hoist5)))) + | (core_models.option.Option.None ) => do + (pure core_models.option.Option.None) + | (core_models.option.Option.None ) => do + (pure core_models.option.Option.None) + +@[spec] +def option_in_if (x : (core_models.option.Option u32)) : + RustM (core_models.option.Option u32) := do + match x with + | (core_models.option.Option.Some v) => do + if (← (v >? (10 : u32))) then do + (pure (core_models.option.Option.Some (← (v -? (10 : u32))))) + else do + (pure (core_models.option.Option.Some v)) + | (core_models.option.Option.None ) => do + (pure core_models.option.Option.None) + +@[spec] +def result_basic (x : (core_models.result.Result u32 String)) : + RustM (core_models.result.Result u32 String) := do + match x with + | (core_models.result.Result.Ok v) => do + (pure (core_models.result.Result.Ok (← (v +? (1 : u32))))) + | (core_models.result.Result.Err err) => do + (pure (core_models.result.Result.Err err)) + +@[spec] +def result_unit + (x : (core_models.result.Result rust_primitives.hax.Tuple0 u32)) : + RustM (core_models.result.Result i8 u32) := do + match x with + | (core_models.result.Result.Ok _) => do + (pure (core_models.result.Result.Ok (0 : i8))) + | (core_models.result.Result.Err err) => do + (pure (core_models.result.Result.Err err)) + +@[spec] +def result_multi + (a : (core_models.result.Result u32 String)) + (b : (core_models.result.Result u32 String)) : + RustM (core_models.result.Result u32 String) := do + match a with + | (core_models.result.Result.Ok hoist9) => do + match b with + | (core_models.result.Result.Ok hoist8) => do + (pure (core_models.result.Result.Ok (← (hoist9 +? hoist8)))) + | (core_models.result.Result.Err err) => do + (pure (core_models.result.Result.Err err)) + | (core_models.result.Result.Err err) => do + (pure (core_models.result.Result.Err err)) + +@[spec] +def chained_transforms (x : (core_models.result.Result u32 String)) : + RustM (core_models.result.Result u32 String) := do + match x with + | (core_models.result.Result.Ok a) => do + match (core_models.result.Result.Ok (← (a +? (1 : u32)))) with + | (core_models.result.Result.Ok b) => do + match (core_models.result.Result.Ok (← (b *? (2 : u32)))) with + | (core_models.result.Result.Ok c) => do + (pure (core_models.result.Result.Ok c)) + | (core_models.result.Result.Err err) => do + (pure (core_models.result.Result.Err err)) + | (core_models.result.Result.Err err) => do + (pure (core_models.result.Result.Err err)) + | (core_models.result.Result.Err err) => do + (pure (core_models.result.Result.Err err)) + +@[spec] +def nested_result_option + (x : (core_models.result.Result (core_models.option.Option u32) String)) : + RustM (core_models.result.Result u32 String) := do + match x with + | (core_models.result.Result.Ok opt) => do + match opt with + | (core_models.option.Option.Some v) => do + (pure (core_models.result.Result.Ok v)) + | (core_models.option.Option.None ) => do + (pure (core_models.result.Result.Ok (0 : u32))) + | (core_models.result.Result.Err err) => do + (pure (core_models.result.Result.Err err)) + +structure Pair where + a : u32 + b : u32 + +@[spec] +def construct_with_question_mark + (x : (core_models.option.Option u32)) + (y : (core_models.option.Option u32)) : + RustM (core_models.option.Option Pair) := do + match x with + | (core_models.option.Option.Some hoist12) => do + match y with + | (core_models.option.Option.Some hoist11) => do + (pure (core_models.option.Option.Some + (Pair.mk (a := hoist12) (b := hoist11)))) + | (core_models.option.Option.None ) => do + (pure core_models.option.Option.None) + | (core_models.option.Option.None ) => do + (pure core_models.option.Option.None) + +end lean_tests.question_mark + + namespace lean_tests.specs def test (x : u8) : RustM u8 := do (pure x) @@ -1833,6 +2667,135 @@ abbrev ESMonad (A : Type) (S : Type) (E : Type) : Type := (rust_primitives.hax.Tuple2 (core_models.result.Result A E) S) +structure Meters where + _0 : f64 + +structure Seconds where + _0 : f64 + +structure Velocity where + _0 : f64 + +structure Unit where + -- no fields + +structure Marker where + -- no fields + +@[spec] +def make_unit (_ : rust_primitives.hax.Tuple0) : RustM Unit := do (pure Unit.mk) + +@[spec] +def take_marker (_m : Marker) : RustM u32 := do (pure (42 : u32)) + +structure Tagged (T : Type) where + value : u32 + _phantom : (core_models.marker.PhantomData T) + +structure Meters2 where + -- no fields + +structure Kilograms where + -- no fields + +@[spec] +def make_tagged_meters (v : u32) : RustM (Tagged Meters2) := do + (pure (Tagged.mk + (value := v) + (_phantom := core_models.marker.PhantomData.mk))) + +@[spec] +def make_tagged_kg (v : u32) : RustM (Tagged Kilograms) := do + (pure (Tagged.mk + (value := v) + (_phantom := core_models.marker.PhantomData.mk))) + +@[spec] +def read_tagged (T : Type) (t : (Tagged T)) : RustM u32 := do + (pure (Tagged.value t)) + +abbrev Pair (A : Type) : Type := (rust_primitives.hax.Tuple2 A A) + +abbrev Triple (A : Type) : Type := (rust_primitives.hax.Tuple3 A A A) + +abbrev NestedPair (A : Type) : + Type := + (rust_primitives.hax.Tuple2 + (rust_primitives.hax.Tuple2 A A) + (rust_primitives.hax.Tuple2 A A)) + +abbrev OptionPair (A : Type) : + Type := + (core_models.option.Option (rust_primitives.hax.Tuple2 A A)) + +@[spec] +def make_pair (x : u32) : RustM (rust_primitives.hax.Tuple2 u32 u32) := do + (pure (rust_primitives.hax.Tuple2.mk x x)) + +@[spec] +def make_nested_pair (x : u32) : + RustM + (rust_primitives.hax.Tuple2 + (rust_primitives.hax.Tuple2 u32 u32) + (rust_primitives.hax.Tuple2 u32 u32)) + := do + (pure (rust_primitives.hax.Tuple2.mk + (rust_primitives.hax.Tuple2.mk x x) + (rust_primitives.hax.Tuple2.mk x x))) + +@[spec] +def unwrap_option_pair + (x : (core_models.option.Option (rust_primitives.hax.Tuple2 u32 u32))) : + RustM u32 := do + match x with + | (core_models.option.Option.Some ⟨a, b⟩) => do (a +? b) + | (core_models.option.Option.None ) => do (pure (0 : u32)) + +abbrev Callback : Type := (u32 -> RustM u32) + +@[spec] +def apply (f : (u32 -> RustM u32)) (x : u32) : RustM u32 := do (f x) + +structure Either (L : Type) (R : Type) where + is_left : Bool + left : (core_models.option.Option L) + right : (core_models.option.Option R) + +@[spec] +def make_left (L : Type) (R : Type) (v : L) : RustM (Either L R) := do + (pure (Either.mk + (is_left := true) + (left := (core_models.option.Option.Some v)) + (right := core_models.option.Option.None))) + +@[spec] +def make_right (L : Type) (R : Type) (v : R) : RustM (Either L R) := do + (pure (Either.mk + (is_left := false) + (left := core_models.option.Option.None) + (right := (core_models.option.Option.Some v)))) + +structure Wrapper (T : Type) where + _0 : T + +@[spec] +def wrap (x : u32) : RustM (Wrapper u32) := do (pure (Wrapper.mk x)) + +@[spec] +def unwrap (w : (Wrapper u32)) : RustM u32 := do (pure (Wrapper._0 w)) + +abbrev ParseResult (T : Type) : + Type := + (core_models.result.Result (rust_primitives.hax.Tuple2 T String) String) + +@[spec] +def dummy_parse (input : String) : + RustM + (core_models.result.Result (rust_primitives.hax.Tuple2 u32 String) String) + := do + (pure (core_models.result.Result.Ok + (rust_primitives.hax.Tuple2.mk (42 : u32) input))) + end lean_tests.types @@ -2065,6 +3028,17 @@ class Chain1 (Self : Type) end lean_tests.traits.associated_types +namespace lean_tests.types + +inductive Expr : Type +| Lit : i32 -> Expr +| Add : Expr -> Expr -> Expr +| Mul : Expr -> Expr -> Expr +| Neg : Expr -> Expr + +end lean_tests.types + + namespace lean_tests.associated_types.basic @[spec] @@ -2251,6 +3225,25 @@ class T2 (Self : Type) [trait_constr_T_i1 : T1 associatedTypes.T ] f (Self) : (Self -> associatedTypes.T -> RustM usize) +end lean_tests.traits.associated_types + + +namespace lean_tests.types + +@[spec] +def eval (e : Expr) : RustM i32 := do + match e with + | (Expr.Lit n) => do (pure n) + | (Expr.Add a b) => do ((← (eval a)) +? (← (eval b))) + | (Expr.Mul a b) => do ((← (eval a)) *? (← (eval b))) + | (Expr.Neg a) => do (-? (← (eval a))) +partial_fixpoint + +end lean_tests.types + + +namespace lean_tests.traits.associated_types + @[reducible] instance Impl_1.AssociatedTypes : T2.AssociatedTypes S where T := S diff --git a/tests/lean-tests/src/array.rs b/tests/lean-tests/src/array.rs index 538066a12..1d51ffa96 100644 --- a/tests/lean-tests/src/array.rs +++ b/tests/lean-tests/src/array.rs @@ -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(x: [u8; N]) {} fn g(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(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 { + data: [u8; N], +} + +fn make_buffer() -> Buffer<16> { + Buffer { data: [0u8; 16] } +} diff --git a/tests/lean-tests/src/binops.rs b/tests/lean-tests/src/binops.rs index 97b653314..4ac33fd3f 100644 --- a/tests/lean-tests/src/binops.rs +++ b/tests/lean-tests/src/binops.rs @@ -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 { @@ -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 } diff --git a/tests/lean-tests/src/floats.rs b/tests/lean-tests/src/floats.rs index 99213ac82..670ee2f23 100644 --- a/tests/lean-tests/src/floats.rs +++ b/tests/lean-tests/src/floats.rs @@ -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] +} diff --git a/tests/lean-tests/src/guards.rs b/tests/lean-tests/src/guards.rs new file mode 100644 index 000000000..bb9d95b60 --- /dev/null +++ b/tests/lean-tests/src/guards.rs @@ -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 { + 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, 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>) -> i32 { + match x { + Some(Some(v)) if v > 0 => v, + Some(Some(v)) => -v, + Some(None) => -1, + None => -2, + } +} diff --git a/tests/lean-tests/src/ite.rs b/tests/lean-tests/src/ite.rs index 20fb45612..ba2b8a98a 100644 --- a/tests/lean-tests/src/ite.rs +++ b/tests/lean-tests/src/ite.rs @@ -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; @@ -23,3 +25,130 @@ fn test2(b: bool) -> i32 { z + y + x } } + +// if-let with Option +fn if_let_option(x: Option) -> u32 { + if let Some(v) = x { v + 1 } else { 0 } +} + +// if-let with Result +fn if_let_result(x: Result) -> u32 { + if let Ok(v) = x { v * 2 } else { 0 } +} + +// Chained if-let / else-if-let +fn chained_if_let(a: Option, b: Option) -> 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>) -> 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 +} diff --git a/tests/lean-tests/src/let_else.rs b/tests/lean-tests/src/let_else.rs new file mode 100644 index 000000000..4e79a11e9 --- /dev/null +++ b/tests/lean-tests/src/let_else.rs @@ -0,0 +1,74 @@ +//! Tests for let-else statements +#![allow(dead_code)] +#![allow(unused_variables)] + +// Basic let-else with Option +fn basic_option(opt: Option) -> u32 { + let Some(x) = opt else { return 0 }; + x + 1 +} + +// let-else with Result +fn basic_result(res: Result) -> u32 { + let Ok(x) = res else { return 0 }; + x + 1 +} + +// Multiple let-else in sequence +fn chained(a: Option, b: Option) -> u32 { + let Some(x) = a else { return 0 }; + let Some(y) = b else { return x }; + x + y +} + +// let-else with tuple destructuring +fn tuple_destructure(opt: Option<(u32, u32)>) -> u32 { + let Some((a, b)) = opt else { return 0 }; + a + b +} + +// let-else with struct pattern +struct Point { + x: i32, + y: i32, +} + +enum Geom { + Pt(Point), + Nothing, +} + +fn struct_let_else(g: Geom) -> i32 { + let Geom::Pt(Point { x, y }) = g else { + return -1; + }; + x + y +} + +// let-else with nested Option +fn nested_option(opt: Option>) -> u32 { + let Some(inner) = opt else { return 0 }; + let Some(v) = inner else { return 1 }; + v + 2 +} + +// let-else returning different divergent expressions +fn with_early_return_result(opt: Option) -> Result { + let Some(x) = opt else { + return Err("missing"); + }; + Ok(x * 2) +} + +// let-else with enum variant +enum Token { + Number(u32), + Plus, + Minus, + Eof, +} + +fn extract_number(t: Token) -> Option { + let Token::Number(n) = t else { return None }; + Some(n) +} diff --git a/tests/lean-tests/src/lib.rs b/tests/lean-tests/src/lib.rs index a8032d951..f273788a3 100644 --- a/tests/lean-tests/src/lib.rs +++ b/tests/lean-tests/src/lib.rs @@ -9,12 +9,16 @@ pub mod comments; pub mod constants; pub mod enums; pub mod floats; +pub mod guards; pub mod ite; +pub mod let_else; pub mod loops; pub mod matching; pub mod monadic; pub mod nested_control_flow; pub mod opaque; +pub mod pattern_or; +pub mod question_mark; pub mod recursion; pub mod specs; pub mod structs; diff --git a/tests/lean-tests/src/matching.rs b/tests/lean-tests/src/matching.rs index 7d12506e8..851792474 100644 --- a/tests/lean-tests/src/matching.rs +++ b/tests/lean-tests/src/matching.rs @@ -1,3 +1,8 @@ +//! Tests on pattern matching +#![allow(dead_code)] +#![allow(unused_variables)] + +// Matching on constants fn test_const_matching(x: u32, c: char, s: &str, b: bool) -> u32 { let x = match x { 0 => 42, @@ -18,6 +23,7 @@ fn test_const_matching(x: u32, c: char, s: &str, b: bool) -> u32 { return x + c + s + b; } +// Binding subpattern with @ fn test_binding_subpattern_matching(x: (u8, (u8, u8))) -> u8 { match x { (0, pair @ (a, b)) => a + b + pair.0 + pair.1, @@ -25,6 +31,7 @@ fn test_binding_subpattern_matching(x: (u8, (u8, u8))) -> u8 { } } +// Ellipsis (..) in record/struct-variant patterns: all fields, some fields, no fields fn test_ellipsis_records() { enum E { C { f1: u8, f2: u8, f3: u8, f4: u8 }, @@ -54,6 +61,7 @@ fn test_ellipsis_records() { }; } +// Ellipsis (..) in plain struct patterns fn test_ellipsis_structs() { struct S { f1: u8, @@ -86,6 +94,7 @@ fn test_ellipsis_structs() { }; } +// Ellipsis (..) in bare tuple patterns: prefix, suffix, both ends fn test_ellipsis_bare_tuples() { let t = (1u8, 2u8, 3u8, 4u8); @@ -112,6 +121,7 @@ fn test_ellipsis_bare_tuples() { }; } +// Ellipsis (..) in enum tuple-variant patterns fn test_ellipsis_tuples() { enum F { D(u8, u8, u8, u8), @@ -141,3 +151,156 @@ fn test_ellipsis_tuples() { F::D(a, b, c, d) => assert!(a == 1 && b == 2 && c == 3 && d == 4), }; } + +// Nested tuple destructuring +fn nested_tuple_match(x: ((u32, u32), (u32, u32))) -> u32 { + match x { + ((a, b), (c, d)) => a + b + c + d, + } +} + +// Match with multiple arms and fallthrough wildcard +fn multi_arm(x: u32) -> u32 { + match x { + 0 => 100, + 1 => 200, + 2 => 300, + 3 => 400, + _ => 0, + } +} + +// Match returning different types from each arm (all same type) +fn match_expressions(x: Option) -> u32 { + match x { + Some(v) => v * 2, + None => 0, + } +} + +// Match on nested enums +enum Wrapper { + Single(u32), + Pair(u32, u32), + Empty, +} + +fn match_wrapper(w: Wrapper) -> u32 { + match w { + Wrapper::Single(x) => x, + Wrapper::Pair(x, y) => x + y, + Wrapper::Empty => 0, + } +} + +// Match on nested Options +fn match_nested_option(x: Option>) -> u32 { + match x { + Some(Some(v)) => v, + Some(None) => 1, + None => 2, + } +} + +// Match on Result +fn match_result(x: Result) -> u32 { + match x { + Ok(v) => v, + Err(_) => 0, + } +} + +// Exhaustive matching on bool +fn match_bool_exhaustive(b: bool) -> u32 { + match b { + true => 1, + false => 0, + } +} + +// Match on tuple of enums +fn match_enum_pair(a: Option, b: Option) -> u32 { + match (a, b) { + (Some(x), Some(y)) => x + y, + (Some(x), None) => x, + (None, Some(y)) => y, + (None, None) => 0, + } +} + +// Deeply nested pattern +fn deep_pattern(x: Option>) -> u32 { + match x { + Some(Ok((a, b))) => a + b, + Some(Err(e)) => e, + None => 0, + } +} + +// Match with binding and computation in arm +fn match_with_block(x: Option) -> u32 { + match x { + Some(v) => { + let doubled = v * 2; + let tripled = v * 3; + doubled + tripled + } + None => { + let default = 42; + default + } + } +} + +// Multiple let-destructurings +fn multiple_let_destruct() -> u32 { + let (a, b) = (1u32, 2u32); + let (c, (d, e)) = (3u32, (4u32, 5u32)); + a + b + c + d + e +} + +// Match with @ binding on enum +fn at_binding_enum(x: Option) -> u32 { + match x { + v @ Some(42) => 100, + Some(n) => n, + None => 0, + } +} + +// Match on reference +fn match_on_ref(x: &u32) -> u32 { + match x { + &0 => 100, + &1 => 200, + _ => 0, + } +} + +// Match returning unit +fn match_unit(x: u32) { + match x { + 0 => (), + _ => (), + } +} + +// Matching on ranges (inclusive) +fn match_range(x: u32) -> &'static str { + match x { + 0..=9 => "digit", + 10..=99 => "two-digit", + 100..=999 => "three-digit", + _ => "large", + } +} + +// Matching on char ranges +fn char_class(c: char) -> u32 { + match c { + 'a'..='z' => 1, + 'A'..='Z' => 2, + '0'..='9' => 3, + _ => 0, + } +} diff --git a/tests/lean-tests/src/pattern_or.rs b/tests/lean-tests/src/pattern_or.rs new file mode 100644 index 000000000..5126355db --- /dev/null +++ b/tests/lean-tests/src/pattern_or.rs @@ -0,0 +1,110 @@ +//! Tests for OR patterns in match expressions +#![allow(dead_code)] +#![allow(unused_variables)] + +enum Color { + Red, + Green, + Blue, + Yellow, + Cyan, +} + +// Simple OR pattern on enum variants +fn simple_or(c: Color) -> u32 { + match c { + Color::Red | Color::Green => 1, + Color::Blue | Color::Yellow | Color::Cyan => 2, + } +} + +// OR pattern on integers +fn int_or(x: u32) -> u32 { + match x { + 0 | 1 => 10, + 2 | 3 | 4 => 20, + _ => 30, + } +} + +// Nested OR inside Option +fn nested_option(x: Option) -> i32 { + match x { + Some(1 | 2) => 1, + Some(3 | 4 | 5) => 2, + Some(x) => x, + None => 0, + } +} + +// Deep OR with tuples +fn deep_tuple(x: (i32, Option)) -> i32 { + match x { + (1 | 2, Some(3 | 4)) => 0, + (5 | 6, None) => 1, + (x, _) => x, + } +} + +// OR pattern with variable capture across Result branches +fn capture_across_or(x: Result<(i32, i32), (i32, i32)>) -> i32 { + match x { + Ok((1 | 2, y)) | Err((3 | 4, y)) => y, + Ok((x, _)) | Err((x, _)) => x, + } +} + +// OR pattern in let destructuring +fn let_or(x: (u8, u8)) -> u8 { + let (a, b) = x; + a + b +} + +// OR pattern on chars +fn char_or(c: char) -> u32 { + match c { + 'a' | 'e' | 'i' | 'o' | 'u' => 1, + 'A' | 'E' | 'I' | 'O' | 'U' => 2, + _ => 0, + } +} + +// OR pattern on booleans +fn bool_or(x: bool, y: bool) -> u32 { + match (x, y) { + (true, true) | (false, false) => 1, + (true, false) | (false, true) => 2, + } +} + +// OR in nested enum +enum Outer { + A(Inner), + B(Inner), +} + +enum Inner { + X, + Y(u32), +} + +fn nested_enum_or(o: Outer) -> u32 { + match o { + Outer::A(Inner::X) | Outer::B(Inner::X) => 0, + Outer::A(Inner::Y(v)) | Outer::B(Inner::Y(v)) => v, + } +} + +// OR combined with wildcard +fn or_with_wildcard(x: (u32, u32, u32)) -> u32 { + match x { + (0 | 1, _, z) => z, + (_, 0 | 1, z) => z + 1, + (_, _, z) => z + 2, + } +} + +// OR in if-let (refutable pattern) +fn or_in_if_let(x: Option) -> u32 { + if let Some(1 | 2 | 3) = x { 42 } else { 0 } +} diff --git a/tests/lean-tests/src/question_mark.rs b/tests/lean-tests/src/question_mark.rs new file mode 100644 index 000000000..78144e160 --- /dev/null +++ b/tests/lean-tests/src/question_mark.rs @@ -0,0 +1,67 @@ +//! Tests for the ? (question mark) operator +#![allow(dead_code)] +#![allow(unused_variables)] + +// Basic ? on Option +fn option_basic(x: Option) -> Option { + let v = x?; + Some(v + 1) +} + +// Multiple ? on Option +fn option_multi(x: Option, y: Option) -> Option { + Some(x? + y?) +} + +// ? on Option in conditional +fn option_in_if(x: Option) -> Option { + let v = x?; + if v > 10 { Some(v - 10) } else { Some(v) } +} + +// Basic ? on Result +fn result_basic(x: Result) -> Result { + let v = x?; + Ok(v + 1) +} + +// ? on Result with unit Ok +fn result_unit(x: Result<(), u32>) -> Result { + x?; + Ok(0) +} + +// Multiple ? on Result +fn result_multi( + a: Result, + b: Result, +) -> Result { + Ok(a? + b?) +} + +// Chained ? with transformations +fn chained_transforms(x: Result) -> Result { + let a = x?; + let b = Ok::(a + 1)?; + let c = Ok::(b * 2)?; + Ok(c) +} + +// Nested Result/Option with ? +fn nested_result_option(x: Result, &'static str>) -> Result { + let opt = x?; + match opt { + Some(v) => Ok(v), + None => Ok(0), + } +} + +// ? combined with struct construction +struct Pair { + a: u32, + b: u32, +} + +fn construct_with_question_mark(x: Option, y: Option) -> Option { + Some(Pair { a: x?, b: y? }) +} diff --git a/tests/lean-tests/src/recursion.rs b/tests/lean-tests/src/recursion.rs index 607a4f042..5990956b5 100644 --- a/tests/lean-tests/src/recursion.rs +++ b/tests/lean-tests/src/recursion.rs @@ -1,3 +1,8 @@ +//! Tests on recursion +#![allow(dead_code)] +#![allow(unused_variables)] + +// Simple recursion (non-tail) fn factorial(n: u32) -> u32 { if n == 0 { 1 } else { n * factorial(n - 1) } } diff --git a/tests/lean-tests/src/types.rs b/tests/lean-tests/src/types.rs index f43fed6fb..9c99bc675 100644 --- a/tests/lean-tests/src/types.rs +++ b/tests/lean-tests/src/types.rs @@ -1,11 +1,145 @@ +//! Tests on type aliases and type definitions #![allow(dead_code)] #![allow(unused_variables)] -// Tests on type aliases +// Basic type aliases type UsizeAlias = usize; type MyOption = Option; type MyResult = Result, B>; +// Monad-like type aliases type ErrorMonad = Result; type StateMonad = (A, S); type ESMonad = StateMonad, S>; + +// Newtype wrappers +struct Meters(f64); +struct Seconds(f64); +struct Velocity(f64); + +// Unit struct (zero-sized type) +struct Unit; +struct Marker; + +fn make_unit() -> Unit { + Unit +} + +fn take_marker(_m: Marker) -> u32 { + 42 +} + +// Phantom data (generic but unused in data) +use core::marker::PhantomData; + +struct Tagged { + value: u32, + _phantom: PhantomData, +} + +struct Meters2; +struct Kilograms; + +fn make_tagged_meters(v: u32) -> Tagged { + Tagged { + value: v, + _phantom: PhantomData, + } +} + +fn make_tagged_kg(v: u32) -> Tagged { + Tagged { + value: v, + _phantom: PhantomData, + } +} + +fn read_tagged(t: Tagged) -> u32 { + t.value +} + +// Nested type aliases +type Pair = (A, A); +type Triple = (A, A, A); +type NestedPair = Pair>; +type OptionPair = Option>; + +fn make_pair(x: u32) -> Pair { + (x, x) +} + +fn make_nested_pair(x: u32) -> NestedPair { + ((x, x), (x, x)) +} + +fn unwrap_option_pair(x: OptionPair) -> u32 { + match x { + Some((a, b)) => a + b, + None => 0, + } +} + +// Type alias in function signature +type Callback = fn(u32) -> u32; + +fn apply(f: Callback, x: u32) -> u32 { + f(x) +} + +// Generic struct with multiple type params +struct Either { + is_left: bool, + left: Option, + right: Option, +} + +fn make_left(v: L) -> Either { + Either { + is_left: true, + left: Some(v), + right: None, + } +} + +fn make_right(v: R) -> Either { + Either { + is_left: false, + left: None, + right: Some(v), + } +} + +// Recursive type via Box +enum Expr { + Lit(i32), + Add(Box, Box), + Mul(Box, Box), + Neg(Box), +} + +fn eval(e: &Expr) -> i32 { + match e { + Expr::Lit(n) => *n, + Expr::Add(a, b) => eval(a) + eval(b), + Expr::Mul(a, b) => eval(a) * eval(b), + Expr::Neg(a) => -eval(a), + } +} + +// Tuple struct with generic +struct Wrapper(T); + +fn wrap(x: u32) -> Wrapper { + Wrapper(x) +} + +fn unwrap(w: Wrapper) -> u32 { + w.0 +} + +// Type alias for complex return types +type ParseResult<'a, T> = Result<(T, &'a str), &'a str>; + +fn dummy_parse(input: &str) -> ParseResult { + Ok((42, input)) +}