hax-rust-engine 0.3.4

//! The global identifiers of hax.
use hax_frontend_exporter::{DefKind, DisambiguatedDefPathItem};
use hax_rust_engine_macros::*;

pub mod view;

/// A Rust `DefId`: a lighter version of [`hax_frontend_exporter::DefId`].
#[derive_group_for_ast]
pub struct DefId {
    /// The crate of the definition
    pub krate: String,
    /// The full path for this definition, under the crate `krate`
    pub path: Vec<DisambiguatedDefPathItem>,
    /// The parent `DefId`, if any.
    /// `parent` if node if and only if `path` is empty
    pub parent: Option<Box<DefId>>,
    /// What kind is this definition? (e.g. an `enum`, a `const`, an assoc. `fn`...)
    pub kind: DefKind,
}

/// An [`ExpliciDefId`] is a Rust [`DefId`] tagged withg some disambiguation metadata.
///
/// [`DefId`] can be ambiguous, consider the following Rust code:
///
/// ```rust
/// struct S;
/// fn f() -> S { S }
/// ```
///
/// Here, the return type of `f` (that is, `S`) and the constructor `S` in the body of `f` refer to the exact same identifier `mycrate::S`.
/// Yet, they denote two very different objects: a type versus a constructor.
///
/// [`ExplicitDefId`] clears up this ambiguity, making constructors and types two separate things.
///
/// Also, an [`ExplicitDefId`] always points to an item: an [`ExplicitDefId`] is never pointing to a crate alone.
#[derive_group_for_ast]
struct ExplicitDefId {
    /// Is this `DefId` a constructor?
    is_constructor: bool,
    /// The `DefId` itself
    def_id: DefId,
}

impl ExplicitDefId {
    /// Get the parent of an `ExplicitDefId`.
    pub fn parent(&self) -> Option<Self> {
        let def_id = &self.def_id;
        let is_constructor = matches!(&def_id.kind, DefKind::Field);
        Some(Self {
            is_constructor,
            def_id: def_id.parent.as_ref()?.as_ref().clone(),
        })
    }
    /// Returns an iterator that yields `self`, then `self.parent()`, etc.
    /// This iterator is non-empty.
    pub fn parents(&self) -> impl Iterator<Item = Self> {
        std::iter::successors(Some(self.clone()), |id| id.parent())
    }
}

/// Represents a fresh module: a module generated by hax and guaranteed to be fresh.
#[derive_group_for_ast]
struct FreshModule {
    /// Internal (unique) identifier
    id: usize,
    /// Non-empty list of identifiers that will be used to decide the name of the fresh module.
    hints: Vec<ExplicitDefId>,
    /// A decoration label that will be also used to decide the name of the fresh module.
    label: String,
}

/// [`ReservedSuffix`] helps at deriving fresh identifiers out of existing (Rust) ones.
#[derive_group_for_ast]
enum ReservedSuffix {
    /// Precondition of a function-like item.
    Pre,
    /// Postcondition of a function-like item.
    Post,
    /// Cast function for an `enum` discriminant.
    Cast,
}

/// A identifier that we call concrete: it exists concretely somewhere in Rust.
#[derive_group_for_ast]
pub struct ConcreteId {
    /// The explicit `def_id`.
    def_id: ExplicitDefId,
    /// A fresh module if this definition was moved to a fresh module.
    moved: Option<FreshModule>,
    /// An optional suffix.
    suffix: Option<ReservedSuffix>,
}

/// A global identifier in hax.
#[derive_group_for_ast]
pub enum GlobalId {
    /// A concrete identifier that exists in Rust.
    Concrete(ConcreteId),
    /// A projector.
    Projector(ConcreteId),
}

impl GlobalId {
    /// Extracts the Crate info
    pub fn krate(&self) -> String {
        match self {
            GlobalId::Concrete(concrete_id) | GlobalId::Projector(concrete_id) => {
                concrete_id.def_id.def_id.krate.clone()
            }
        }
    }

    /// Tests if the raw output is reduced to "_". Should be used only for
    /// testing. See https://github.com/cryspen/hax/issues/1599
    pub fn is_empty(&self) -> bool {
        self.to_debug_string() == "_"
    }

    /// Extract the raw `DefId` from a `GlobalId`.
    /// This should never be used for name printing.
    pub fn def_id(&self) -> DefId {
        let (GlobalId::Concrete(concrete_id) | GlobalId::Projector(concrete_id)) = self;
        concrete_id.def_id.def_id.clone()
    }

    /// Raw printing of identifier separated by underscore. Should be used
    /// only for testing. See https://github.com/cryspen/hax/issues/1599
    pub fn to_debug_string(&self) -> String {
        match self {
            GlobalId::Concrete(concrete_id) => concrete_id
                .def_id
                .def_id
                .clone()
                .path
                .into_iter()
                .map(|def| {
                    let data = match def.clone().data {
                        hax_frontend_exporter::DefPathItem::ValueNs(s)
                        | hax_frontend_exporter::DefPathItem::MacroNs(s)
                        | hax_frontend_exporter::DefPathItem::TypeNs(s) => s.clone(),
                        hax_frontend_exporter::DefPathItem::Impl => "impl".to_string(),
                        other => unimplemented!("{other:?}"),
                    };
                    if def.disambiguator != 0 && !data.is_empty() && data != "_" {
                        // Don't print disambiguator of empty data
                        format!("_{}_{}", def.disambiguator, data)
                    } else {
                        data
                    }
                })
                .collect::<Vec<String>>()
                .join("_"),
            GlobalId::Projector(_concrete_id) => todo!(),
        }
    }

    /// Turns a `GlobalId` into a `ConcreteId`: returns `None` on projectors.
    pub fn as_concrete(&self) -> Option<ConcreteId> {
        match self {
            GlobalId::Concrete(concrete_id) => Some(concrete_id.clone()),
            _ => None,
        }
    }
    /// Turns a `GlobalId` into a projector `ConcreteId`: returns `Some` only on projectors.
    pub fn as_projector(&self) -> Option<ConcreteId> {
        match self {
            GlobalId::Projector(concrete_id) => Some(concrete_id.clone()),
            _ => None,
        }
    }
}

impl ConcreteId {
    /// Renders a view of the concrete identifier.
    pub fn view(&self) -> view::View {
        self.def_id.clone().into()
    }

    /// Gets the closest mod-only parent.
    pub fn mod_only_closest_parent(&self) -> Self {
        let mut parents = self.def_id.parents().collect::<Vec<_>>();
        parents.reverse();
        let def_id = parents
            .into_iter()
            .take_while(|id| matches!(id.def_id.kind, DefKind::Mod))
            .next()
            .expect("Invariant broken: a DefId must always contain at least on `mod` segment (the crate)");
        Self {
            def_id,
            moved: self.moved.clone(),
            suffix: None,
        }
    }

    /// Turns a ConcreteId into a GlobalId
    pub fn into_concrete(self) -> GlobalId {
        GlobalId::Concrete(self)
    }
}

impl PartialEq<DefId> for GlobalId {
    fn eq(&self, other: &DefId) -> bool {
        if let Self::Concrete(concrete) = self {
            &concrete.def_id.def_id == other
        } else {
            false
        }
    }
}
impl PartialEq<GlobalId> for DefId {
    fn eq(&self, other: &GlobalId) -> bool {
        other == self
    }
}