extern crate alloc;
use crate::kairos::{Clock, TickCounter};
use crate::metis::{Dotted, Locus, Rhapsody};
use proptest::prelude::*;
use super::super::{REPLICAS, Seq, arb_ops, run};
proptest! {
#[test]
fn prop_visual_insert_round_trips_through_order(
ops in arb_ops(), caret_pick in 0usize..16,
) {
let (live, _) = run(&ops);
let station = u32::try_from(REPLICAS + 1).unwrap();
let clk = Clock::with_default_config(TickCounter::new(), station).unwrap();
let mut seq = live.iter().fold(Seq::new(), |acc, r| acc.merge(r));
let visible_before = seq.store().order();
let after = if visible_before.is_empty() {
None
} else {
Some(visible_before[caret_pick % visible_before.len()])
};
let anchor = seq.store().anchor_for_visual_insert(after.map(Into::into));
if let Some(top) = seq.store().children_of(anchor).next()
&& let Some(locus) = seq.store().locus(top)
{
clk.observe(locus.rank);
}
let dot = seq.next_dot(station);
let rank = clk.now(0u16);
let locus = Locus { anchor, rank };
let mut rhapsody = Rhapsody::new();
prop_assert!(rhapsody.weave(dot, locus));
seq = seq.merge(&Dotted::from_store(rhapsody));
let after_order = seq.store().order();
let idx = after_order.iter().position(|&d| d == dot).unwrap();
match after {
None => prop_assert_eq!(idx, 0, "document-start insert reads first"),
Some(a) => {
let a_idx = after_order.iter().position(|&d| d == a).unwrap();
prop_assert_eq!(idx, a_idx + 1, "the insert reads immediately after the caret element");
}
}
}
}