impl<M: Memory> Machine<M> {
    #[specr::argmatch(statement)]
    fn eval_statement(&mut self, statement: Statement) -> NdResult { .. }
}

impl<M: Memory> Machine<M> {
    fn place_store(&mut self, place: Place<M>, val: Value<M>, ty: Type) -> Result {
        if !place.aligned {
            throw_ub!("storing to a place based on a misaligned pointer");
        }
        // Alignment was already checked.
        self.typed_store(place.ptr.thin_pointer, val, ty, Align::ONE, Atomicity::None)?;
        ret(())
    }

    fn eval_statement(&mut self, Statement::Assign { destination, source }: Statement) -> NdResult {
        let (place, ty) = self.eval_place(destination)?;
        let (val, _) = self.eval_value(source)?;
        self.place_store(place, val, ty)?;

        ret(())
    }
}

impl<M: Memory> Machine<M> {
    fn eval_statement(&mut self, Statement::PlaceMention(place): Statement) -> NdResult {
        self.eval_place(place)?;
        ret(())
    }
}

impl<M: Memory> Machine<M> {
    fn eval_statement(&mut self, Statement::SetDiscriminant { destination, value }: Statement) -> NdResult {
        let (place, Type::Enum { variants, .. }) = self.eval_place(destination)? else {
            panic!("setting the discriminant type of a non-enum contradicts well-formedness");
        };
        if !place.aligned {
            throw_ub!("setting the discriminant of a place based on a misaligned pointer");
        }

        let tagger = match variants.get(value) {
            Some(Variant { tagger, .. }) => tagger,
            // guaranteed unreachable by the well-formedness checks
            None => panic!("setting an invalid discriminant ({value})"),
        };

        // Write the tag directly into memory.
        // This should be fine as we don't allow encoded data and the tag to overlap for valid enum variants.
        let accessor = |offset: Offset, bytes| {
            let ptr = self.ptr_offset_inbounds(place.ptr.thin_pointer, offset.bytes())?;
            // We have ensured that the place is aligned, so no alignment requirement here
            self.mem.store(ptr, bytes, Align::ONE, Atomicity::None)
        };
        encode_discriminant::<M>(accessor, tagger)?;
        ret(())
    }
}

impl<M: Memory> ConcurrentMemory<M> {
    /// Find all pointers in this value, ensure they are valid, and retag them.
    fn retag_val(&mut self, frame_extra: &mut M::FrameExtra, val: Value<M>, ty: Type, fn_entry: bool) -> Result<Value<M>> {
        ret(match (val, ty) {
            // no (identifiable) pointers
            (Value::Int(..) | Value::Bool(..) | Value::Union(..), _) =>
                val,
            // base case
            (Value::Ptr(ptr), Type::Ptr(ptr_type)) =>
                Value::Ptr(self.retag_ptr(frame_extra, ptr, ptr_type, fn_entry)?),
            // recurse into tuples/arrays/enums
            (Value::Tuple(vals), Type::Tuple { fields, .. }) =>
                Value::Tuple(vals.zip(fields).try_map(|(val, (_offset, ty))| self.retag_val(frame_extra, val, ty, fn_entry))?),
            (Value::Tuple(vals), Type::Array { elem: ty, .. }) =>
                Value::Tuple(vals.try_map(|val| self.retag_val(frame_extra, val, ty, fn_entry))?),
            (Value::Variant { discriminant, data }, Type::Enum { variants, .. }) =>
                Value::Variant { discriminant, data: self.retag_val(frame_extra, data, variants[discriminant].ty, fn_entry)? },
            _ =>
                panic!("this value does not have that type"),
        })
    }
}

impl<M: Memory> Machine<M> {
    fn eval_statement(&mut self, Statement::Validate { place, fn_entry }: Statement) -> NdResult {
        let (place, ty) = self.eval_place(place)?;

        // WF ensures all valid expressions are sized, so we can invoke the load.
        // This also ensures the value in the place satsifies the language invariant.
        let val = self.place_load(place, ty)?;

        let val = self.mutate_cur_frame(|frame, mem| { mem.retag_val(&mut frame.extra, val, ty, fn_entry) })?;

        self.place_store(place, val, ty)?;

        ret(())
    }
}

impl<M: Memory> ConcurrentMemory<M> {
    fn deinit(&mut self, ptr: ThinPointer<M::Provenance>, len: Size, align: Align) -> Result {
        self.store(ptr, list![AbstractByte::Uninit; len.bytes()], align, Atomicity::None)?;
        ret(())
    }
}

impl<M: Memory> Machine<M> {
    fn eval_statement(&mut self, Statement::Deinit { place }: Statement) -> NdResult {
        let (p, ty) = self.eval_place(place)?;
        if !p.aligned {
            throw_ub!("de-initializing a place based on a misaligned pointer");
        }
        // Alignment was already checked.
        self.mem.deinit(p.ptr.thin_pointer, ty.layout::<M::T>().expect_size("WF ensures deinits are sized"), Align::ONE)?;

        ret(())
    }
}

impl<M: Memory> StackFrame<M> {
    fn storage_live(&mut self, mem: &mut ConcurrentMemory<M>, local: LocalName) -> NdResult {
        // First remove the old storage, if any.
        // This means the same address may be re-used for the new stoage.
        self.storage_dead(mem, local)?;
        // Then allocate the new storage.
        let pointee_size = self.func.locals[local].layout::<M::T>().expect_size("WF ensures all locals are sized");
        let pointee_align = self.func.locals[local].layout::<M::T>().expect_align("WF ensures all locals are sized");
        let ptr = mem.allocate(AllocationKind::Stack, pointee_size, pointee_align)?;
        self.locals.insert(local, ptr);
        ret(())
    }

    fn storage_dead(&mut self, mem: &mut ConcurrentMemory<M>, local: LocalName) -> NdResult {
        let pointee_size = self.func.locals[local].layout::<M::T>().expect_size("WF ensures all locals are sized");
        let pointee_align = self.func.locals[local].layout::<M::T>().expect_align("WF ensures all locals are sized");
        if let Some(ptr) = self.locals.remove(local) {
            mem.deallocate(ptr, AllocationKind::Stack, pointee_size, pointee_align)?;
        }
        ret(())
    }
}

impl<M: Memory> Machine<M> {
    fn eval_statement(&mut self, Statement::StorageLive(local): Statement) -> NdResult {
        self.try_mutate_cur_frame(|frame, mem| {
            frame.storage_live(mem, local)
        })
    }

    fn eval_statement(&mut self, Statement::StorageDead(local): Statement) -> NdResult {
        self.try_mutate_cur_frame(|frame, mem| {
            frame.storage_dead(mem, local)
        })
    }
}