Support type aliasing for refined opaque structs

Sometimes, it's nice to alias types for documentation / readability. In particular, here's an example with refined maps...

flux_rs::defs! {
    fn map_set<K, V>(m:Map<K, V>, k: K, v: V) -> Map<K, V> { map_store(m, k, v) }
    fn map_get<K, V>(m: Map<K, V>, k:K) -> V { map_select(m, k) }
}

use std::hash::Hash;

/// define a type indexed by a map
#[derive(Debug)]
#[flux_rs::opaque]
#[flux_rs::refined_by(vals: Map<K, V>)]
pub struct Regs<K, V> {
    inner: std::collections::HashMap<K, V>,
}

#[flux_rs::generics(K as base, V as base)]
impl<K, V> Regs<K, V> {
    #[flux_rs::trusted]
    #[flux_rs::sig(fn(self: &strg Regs<K,V>[@m], k: K, v: V) ensures self: Regs<K,V>[map_set(m.vals, k, v)])]
    pub fn set(&mut self, k: K, v: V)
    where
        K: Eq + Hash,
    {
        self.inner.insert(k, v);
    }

    #[flux_rs::trusted]
    #[flux_rs::sig(fn(&Regs<K, V>[@m], &K[@k]) -> Option<&V[map_get(m.vals, k)]>)]
    pub fn get(&self, k: &K) -> Option<&V>
    where
        K: Eq + Hash,
    {
        self.inner.get(k)
    }
}

I might want to do something like this for readability:

pub type ArmGeneralRegs = Regs<GeneralPurposeRegister, u32>;
pub type ArmSpecialRegs = Regs<SpecialRegister, u32>;

Unforunately, I cannot use these in the actual refinement annotations:

#[derive(Debug)]
#[flux_rs::refined_by(
    general_regs: Map<GeneralPurposeRegister, int>,
    special_regs: Map<SpecialRegister, int>,
)]
pub struct Armv7m {
    // General Registers r0 - r11
    #[field(Regs<GeneralPurposeRegister, u32>[general_regs])]
    pub general_regs: ArmGeneralRegs,
    // Special Registers
    #[field(Regs<SpecialRegister, u32>[special_regs])]
    pub special_regs: ArmSpecialRegs,
}

It would be great if instead, I could do something like this:

#[derive(Debug)]
#[flux_rs::refined_by(
    general_regs: Map<GeneralPurposeRegister, int>,
    special_regs: Map<SpecialRegister, int>,
)]
pub struct Armv7m {
    // General Registers r0 - r11
    #[field(ArmGeneralRegs[general_regs])]
    pub general_regs: ArmGeneralRegs,
    // Special Registers
    #[field(ArmSpecialRegs[special_regs])]
    pub special_regs: ArmSpecialRegs,
}

Furthermore, it would be nice to support type aliasing with generics:

pub type HalfwaySpecialized<K> = Reg<K, u32>;

I don't believe this is currently possible.

flux-rs / flux

Support type aliasing for refined opaque structs #866