litex-lang 0.9.68-beta

A simple formal proof language and verifier, learnable in 2 hours
Documentation
use crate::prelude::*;
use std::fmt;

#[derive(Clone)]
pub struct Identifier {
    pub name: String,
}

pub fn identifier_to_string(name: &str) -> String {
    name.to_string()
}

#[derive(Clone)]
pub struct IdentifierWithMod {
    pub mod_name: String,
    pub name: String,
}

pub fn identifier_with_mod_to_string(mod_name: &str, name: &str) -> String {
    format!("{}{}{}", mod_name, MOD_SIGN, name)
}

#[derive(Clone)]
pub struct FieldAccess {
    pub name: String,
    pub field: String,
}

#[derive(Clone)]
pub struct FieldAccessWithMod {
    pub mod_name: String,
    pub name: String,
    pub field: String,
}

impl Identifier {
    pub fn new(name: String) -> Self {
        Identifier { name }
    }
}

impl IdentifierWithMod {
    pub fn new(mod_name: String, name: String) -> Self {
        IdentifierWithMod { mod_name, name }
    }
}

impl FieldAccess {
    pub fn new(name: String, field: String) -> Self {
        FieldAccess { name, field }
    }

    /// 在已有 `root.field` 上再追加一段(嵌套 struct 绑定等运行时路径;`name` 中可含 `.`)。
    pub fn with_appended_field(&self, field_name: &str) -> FieldAccess {
        let prefix = format!("{}{}{}", self.name, DOT_AKA_FIELD_ACCESS_SIGN, self.field);
        FieldAccess::new(prefix, field_name.to_string())
    }
}

impl FieldAccessWithMod {
    pub fn new(mod_name: String, name: String, field: String) -> Self {
        FieldAccessWithMod {
            mod_name,
            name,
            field,
        }
    }

    pub fn with_appended_field(&self, field_name: &str) -> FieldAccessWithMod {
        let prefix = format!("{}{}{}", self.name, DOT_AKA_FIELD_ACCESS_SIGN, self.field);
        FieldAccessWithMod::new(self.mod_name.clone(), prefix, field_name.to_string())
    }
}

impl fmt::Display for FieldAccess {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        write!(f, "{}", field_access_to_string(&self.name, &self.field))
    }
}

pub fn field_access_to_string(name: &str, field: &str) -> String {
    format!("{}{}{}", name, DOT_AKA_FIELD_ACCESS_SIGN, field)
}

impl fmt::Display for FieldAccessWithMod {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        write!(
            f,
            "{}",
            field_access_with_mod_to_string(&self.mod_name, &self.name, &self.field)
        )
    }
}

pub fn field_access_with_mod_to_string(mod_name: &str, name: &str, field: &str) -> String {
    format!(
        "{}{}{}{}{}",
        mod_name, MOD_SIGN, name, DOT_AKA_FIELD_ACCESS_SIGN, field
    )
}