iter¶

In [ ]:
open rust
open rust_operators
In [ ]:
//// test

open testing

rust¶

enumerate¶

In [ ]:
inl enumerate forall t. (iter : into_iterator t) : into_iterator (pair unativeint t) =
    !\($'"!iter.enumerate().map(std::sync::Arc::new)"')

into_iter¶

In [ ]:
inl into_iter forall (t : * -> *) u. (x : t u) : into_iterator u =
    !\($'"!x.into_iter()"')

iter¶

In [ ]:
inl iter forall (t : * -> *) u. (x : t u) : into_iterator u =
    !\\(x, $'"$0.iter()"')

iter_ref¶

In [ ]:
inl iter_ref forall (t : * -> *) u. (x : t u) : into_iterator (rust.ref u) =
    !\\(x, $'"$0.iter()"')

iter_ref'¶

In [ ]:
inl iter_ref' forall (t : * -> *) u. (x : rust.ref (t u)) : into_iterator (rust.ref u) =
    !\\(x, $'"$0.iter()"')

iter_ref''¶

In [ ]:
inl iter_ref'' forall (t : * -> *) u (v : * -> *). (x : v (t u)) : into_iterator (rust.ref u) =
    !\\(x, $'"$0.iter()"')

iter_ref'''¶

In [ ]:
inl iter_ref''' forall (t : * -> *) u (v : * -> *) (w : * -> *). (x : w (v (t u))) : into_iterator (rust.ref u) =
    !\\(x, $'"$0.iter()"')

map¶

In [ ]:
inl map forall t u. (fn : t -> u) (iter : into_iterator t) : into_iterator u =
    !\\(fn, $'"!iter.map(|x| $0(x))"')

cloned¶

In [ ]:
inl cloned forall t. (iter : into_iterator (rust.ref t)) : into_iterator t =
    !\($'"!iter.cloned()"')

for_each¶

In [ ]:
inl for_each forall t. (fn : t -> ()) (iter : into_iterator t) : () =
    (!\\(fn, $'"true; !iter.for_each(|x| $0(x))"') : bool) |> ignore

try_for_each¶

In [ ]:
inl try_for_each forall t. (fn : t -> rust.try ()) x : resultm.result' () string =
    (!\($'"true; let mut !x = !x; let _iter_try_for_each = !x.try_for_each(|x| { //"') : bool) |> ignore
    (!\\(fn !\($'"x"'), $'"true; $0 }); //"') : bool) |> ignore
    !\($'"_iter_try_for_each.map_err(|x| x.into())"')

all¶

In [ ]:
inl all forall t. (fn : t -> bool) (x : rust.mut' (into_iterator t)) : bool =
    x |> rust.to_mut
    !\\(fn, $'$"!x.all(|x| $0(x))"')

enumerate¶

In [ ]:
inl enumerate forall dim {int; number} t. (ar : a dim t) : a dim (unativeint * t) =
    inl (a ar) = ar
    ar
    |> am'.to_vec
    |> into_iter
    |> enumerate
    |> iter_collect
    |> am'.vec_map' from_pair
    |> am'.from_vec
In [ ]:
//// test
///! rust

am'.init_series 0i32 2 1
|> fun x => a x : _ int _
|> enumerate
|> fun (a x : _ int _) => x
|> _assert_eq' ;[ convert 0i32, 0; convert 1i32, 1; convert 2i32, 2 ]

__assert_eq' / actual: Array(MutCell([(0, 0), (1, 1), (2, 2)])) / expected: Array(MutCell([(0, 0), (1, 1), (2, 2)]))