#[path = "context-model.rs"]
#[allow(dead_code)]
mod model;
use std::{
    cell::{Cell, RefCell},
    rc::Rc,
};
use turkos_os_context_switch::context::{self as ctx, Backend as _};
use turkos_os_runqueue::runqueue::*;
use turkos_os_threads::threads::{self as thread, ThreadId};

struct Member {
    context: ctx::Handle,
    thread: ThreadId,
    retained: Rc<Cell<usize>>,
}
impl Drop for Member {
    fn drop(&mut self) {
        self.retained.set(self.retained.get() - 1);
    }
}
struct Prepared {
    token: Option<ctx::OwnedHandoff>,
    epoch: u64,
    nonce: u64,
    queue_nonce: u64,
    arrived: bool,
}
struct Tick {
    sequence: u64,
    observation: TickObservation,
}
#[derive(Default)]
struct Control {
    prepares: u64,
    departures: u64,
    arrivals: u64,
    finishes: u64,
    aborts: u64,
    finish_fail: bool,
    tick_live: Option<u64>,
    consumed: u64,
    sequence: u64,
}
struct Device {
    bank: ctx::AsyncBank<model::Device, 4>,
    handles: Vec<ctx::Handle>,
    hardware: Rc<RefCell<model::saved::Hardware>>,
    cpu: Rc<RefCell<model::Cpu>>,
    control: Rc<RefCell<Control>>,
    retained: Rc<Cell<usize>>,
}
unsafe impl Backend for Device {
    type Member = Member;
    type Prepared = Prepared;
    type Tick = Tick;
    fn execution(&self) -> Execution {
        let e = self.bank.bank().with_backend_observation(|b| b.execution());
        Execution {
            cpu: e.cpu,
            masked: e.daif & 128 != 0,
            in_irq: e.in_irq,
            thread: e.thread,
            root: e.root,
        }
    }
    fn observe(&self, m: &Member) -> Result<Observation, Error> {
        let context = self
            .bank
            .bank()
            .record(m.context)
            .map_err(|_| Error::Stale)?;
        if context.thread != m.thread {
            return Err(Error::Stale);
        }
        self.bank.bank().with_backend_observation(|b| {
            let record = b
                .inner
                .table
                .borrow()
                .record(m.thread)
                .map_err(|_| Error::Stale)?;
            let bytes = b.inner.stacks[m.thread.slot()].borrow();
            let hardware = self.hardware.borrow();
            Ok(Observation {
                thread: record,
                context,
                stack: thread::StackObservation {
                    layout: record.layout,
                    guard_descriptor: u64::from(hardware.corrupt_guard),
                    low_canary: u64::from_le_bytes(bytes[..8].try_into().unwrap())
                        ^ u64::from(hardware.corrupt_canary),
                    high_canary: u64::from_le_bytes(bytes[bytes.len() - 8..].try_into().unwrap()),
                    initially_zeroed: false,
                },
            })
        })
    }
    fn tick(&self, t: &Tick) -> Result<TickObservation, Error> {
        if self.control.borrow().tick_live == Some(t.sequence) {
            Ok(t.observation)
        } else {
            Err(Error::Tick)
        }
    }
    fn consume_tick(&mut self, t: Tick) {
        let mut c = self.control.borrow_mut();
        assert_eq!(c.tick_live, Some(t.sequence));
        c.tick_live = None;
        c.consumed += 1;
    }
    fn prepare(
        &mut self,
        source: Option<&Member>,
        target: &Member,
        epoch: u64,
        disposition: Disposition,
    ) -> Result<Prepared, Error> {
        let nonce = self
            .control
            .borrow()
            .prepares
            .checked_add(1)
            .ok_or(Error::Exhausted)?;
        let token = match source {
            None => self.bank.start(target.context),
            Some(source) => {
                let capture = self.hardware.borrow().capture.ok_or(Error::Backend)?;
                match disposition {
                    Disposition::Ready => {
                        self.bank.cooperate(source.context, target.context, capture)
                    }
                    Disposition::Sleeping => {
                        self.bank.sleep_to(source.context, target.context, capture)
                    }
                }
            }
        }
        .map_err(|_| Error::Backend)?;
        self.control.borrow_mut().prepares = nonce;
        Ok(Prepared {
            token: Some(token),
            epoch,
            nonce,
            queue_nonce: 0,
            arrived: false,
        })
    }
    fn commit(
        &mut self,
        _: &mut Prepared,
        _: Option<&Member>,
        _: &Member,
        _: u64,
        _: Disposition,
    ) -> Result<(), Failure> {
        panic!("synchronous queue commit must not span the assembly handoff")
    }
    fn finish(&mut self, p: Prepared) -> Result<(), (Error, Prepared)> {
        assert!(p.arrived && p.token.is_none());
        if self.control.borrow().finish_fail {
            return Err((Error::Backend, p));
        }
        self.control.borrow_mut().finishes += 1;
        Ok(())
    }
    fn abort(&mut self, mut p: Prepared) -> Result<(), (Error, Prepared)> {
        let token = p.token.take().unwrap();
        match self.bank.abort(token) {
            Ok(()) => {
                self.control.borrow_mut().aborts += 1;
                Ok(())
            }
            Err(ctx::HandoffFailure::Before(_, token)) => {
                p.token = Some(token);
                Err((Error::Backend, p))
            }
            Err(ctx::HandoffFailure::Quarantined(_)) => Err((Error::Backend, p)),
        }
    }
}
unsafe impl SelectionHandoffBackend for Device {
    fn depart(
        &mut self,
        p: &mut Prepared,
        _: Option<&Member>,
        _: &Member,
        epoch: u64,
        _: Disposition,
        nonce: u64,
    ) -> Result<(), Failure> {
        assert_eq!(p.epoch, epoch);
        assert_ne!(p.nonce, 0);
        assert_eq!(p.queue_nonce, 0);
        let token = p.token.take().unwrap();
        match self.bank.depart(token) {
            Ok(token) => {
                p.token = Some(token);
                p.queue_nonce = nonce;
                self.control.borrow_mut().departures += 1;
                Ok(())
            }
            Err(ctx::HandoffFailure::Before(_, token)) => {
                p.token = Some(token);
                Err(Failure {
                    error: Error::Backend,
                    phase: ctx::FailurePhase::BeforeSwitch,
                })
            }
            Err(ctx::HandoffFailure::Quarantined(_)) => Err(Failure {
                error: Error::Backend,
                phase: ctx::FailurePhase::AfterSwitch,
            }),
        }
    }
    fn arrive(
        &mut self,
        p: &mut Prepared,
        _: &Member,
        epoch: u64,
        nonce: u64,
    ) -> Result<(), Error> {
        assert_eq!(p.epoch, epoch);
        if p.queue_nonce != nonce {
            return Err(Error::Stale);
        }
        let token = p.token.take().unwrap();
        match self.bank.landed(token) {
            Ok(()) => {
                p.arrived = true;
                self.control.borrow_mut().arrivals += 1;
                Ok(())
            }
            Err(ctx::HandoffFailure::Before(_, token)) => {
                p.token = Some(token);
                Err(Error::Backend)
            }
            Err(ctx::HandoffFailure::Quarantined(_)) => Err(Error::Backend),
        }
    }
}
type TestQueue = AsyncQueue<Device, 4>;
fn setup(count: usize) -> (TestQueue, Vec<Handle>, Rc<RefCell<Control>>) {
    let (bank, handles, hardware, cpu) = model::setup(count);
    let retained = Rc::new(Cell::new(count));
    let members = handles
        .iter()
        .map(|h| Member {
            context: *h,
            thread: bank.bank().record(*h).unwrap().thread,
            retained: retained.clone(),
        })
        .collect::<Vec<_>>();
    let control = Rc::new(RefCell::new(Control::default()));
    let device = Device {
        bank,
        handles,
        hardware,
        cpu,
        control: control.clone(),
        retained,
    };
    let mut queue = Queue::<_, 4>::new(device).ok().unwrap();
    let ids = members
        .into_iter()
        .enumerate()
        .map(|(i, m)| {
            queue
                .enqueue(m, if i == 1 { Class::Low } else { Class::Normal })
                .ok()
                .unwrap()
        })
        .collect();
    (AsyncQueue::new(queue).ok().unwrap(), ids, control)
}
fn arm(queue: &TestQueue) {
    queue.queue().with_backend_observation(|b| {
        let current = b.hardware.borrow().current;
        if let Some(id) = current {
            let handle = *b
                .handles
                .iter()
                .find(|h| b.bank.bank().record(**h).unwrap().thread == id)
                .unwrap();
            model::capture(
                &b.bank,
                handle,
                &b.hardware,
                19 + b.control.borrow().prepares,
                false,
            );
        }
    });
}
fn physical_step(queue: &TestQueue) {
    queue.queue().with_retained_observation(|p| {
        queue.queue().with_backend_observation(|b| {
            model::physical_step(&b.bank, p.unwrap().token.as_ref().unwrap())
        });
    });
}
fn switch(queue: &mut TestQueue, disposition: Disposition) -> Handle {
    arm(queue);
    let token = queue.select(disposition).unwrap();
    let token = queue.depart(token).ok().unwrap();
    physical_step(queue);
    queue.landed(token).ok().unwrap()
}
fn inventory(queue: &TestQueue) -> (usize, usize, u64) {
    queue.queue().with_backend_observation(|b| {
        (
            b.retained.get(),
            b.hardware.borrow().pins,
            b.hardware.borrow().stack_pages,
        )
    })
}
fn prepared(queue: &TestQueue) -> (u64, u64, u64, bool) {
    queue.queue().with_retained_observation(|p| {
        let p = p.unwrap();
        (p.nonce, p.epoch, p.queue_nonce, p.arrived)
    })
}
fn tick(queue: &TestQueue, handle: Handle) -> Tick {
    let record = queue.queue().record(handle).unwrap();
    queue.queue().with_backend_observation(|b| {
        let mut c = b.control.borrow_mut();
        c.sequence += 1;
        c.tick_live = Some(c.sequence);
        Tick {
            sequence: c.sequence,
            observation: TickObservation {
                cpu: 0,
                source: 0x1060,
                sequence: c.sequence,
                counter: c.sequence * 100,
                thread: record.thread,
                slice: record.slice,
            },
        }
    })
}