tests/src/polonius_list.rs


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30

//@ charon-args=--polonius
//@ aeneas-args=-test-trans-units
//@ [coq,fstar] subdir=misc
#![allow(dead_code)]

pub enum List<T> {
    Cons(T, Box<List<T>>),
    Nil,
}

/// An example which comes from the b-epsilon tree.
///
/// Returns a mutable borrow to the first portion of the list where we
/// can find [x]. This allows to do in-place modifications (insertion, filtering)
/// in a natural manner (this piece of code was inspired by the C++ BeTree).
pub fn get_list_at_x<'a>(ls: &'a mut List<u32>, x: u32) -> &'a mut List<u32> {
    match ls {
        List::Nil => {
            // We reached the end: just return it
            ls
        }
        List::Cons(hd, tl) => {
            if *hd == x {
                ls // Doing this requires NLL
            } else {
                get_list_at_x(tl, x)
            }
        }
    }
}