Enum SortExpr 

pub enum SortExpr {
    Name(Arc<str>),
    App {
        name: Arc<str>,
        args: Vec<Term>,
    },
}

A sort expression: a plain sort name or a dependent sort applied to argument terms.

Appears in Operation::output, Operation::inputs entries, and SortParam::sort, wherever a sort occurs.

Normalization invariant: every SortExpr produced by constructors and public operations is normalized. A normalized value uses the Name spelling whenever the argument list is empty; App { name, args: [] } never appears in normalized values. This invariant is enforced by the smart constructor SortExpr::app, by Self::subst, by Self::rename_head, by Self::apply_maps, and by the custom serde::Deserialize impl. The derived PartialEq and Hash are replaced with manual impls that treat Name(n) and App { name: n, args: [] } as equal (in case a caller constructs a non-normalized value directly through the App variant).

The serde representation uses #[serde(untagged)], so Name(n) serializes as the bare string "n" and App serializes as a struct with name and args fields.

Variants

Name(Arc<str>)

A plain sort name with no parameters applied.

App

A dependent sort applied to argument terms, e.g. Tm(Γ, A).

Fields

name: Arc<str>

The sort’s declared name.

args: Vec<Term>

Argument terms, one per declared sort parameter.

Implementations

impl SortExpr

pub fn app(name: impl Into<Arc<str>>, args: Vec<Term>) -> Self

Smart constructor: produces Self::Name when args is empty, otherwise Self::App. This is the only way to construct a normalized SortExpr::App; direct use of the App variant is allowed for backwards compatibility, but normalization should be restored via Self::normalize before the value escapes its local context.

pub fn normalize(self) -> Self

Normalize this expression: collapse App { name, args: [] } into Name(name). Idempotent; leaves already-normalized values unchanged. The argument list is not recursed into because the term AST inside arguments does not share this two-spelling ambiguity.

pub const fn head(&self) -> &Arc<str>

Extract the bare sort name, ignoring any applied arguments.

pub fn args(&self) -> &[Term]

Argument terms, if any; empty slice for Name.

pub fn subst(&self, mapping: &FxHashMap<Arc<str>, Term>) -> Self

Substitute mapping (parameter name to term) throughout this sort expression’s argument terms.

pub fn alpha_eq(&self, other: &Self) -> bool

Structural equality modulo Name(n) == App { name: n, args: [] }.

Equivalent to PartialEq::eq after the normalization invariant; retained as a named method for documentation and for code that wants to make the two-spelling quotient explicit at call sites.

pub fn alpha_eq_modulo_rewrites( &self, other: &Self, rules: &[DirectedEquation], step_limit: usize, ) -> bool

Definitional equality modulo a directed-rewrite system.

Normalizes both sides by rewriting every argument term with crate::eq::normalize under rules and a bounded step budget, then compares the normalized sort expressions with Self::alpha_eq. Heads must agree; if they do not, no amount of rewriting closes the gap and the function returns false immediately. Callers that want the strict structural equality should continue to use Self::alpha_eq.

pub fn rename_head(&self, sort_map: &HashMap<Arc<str>, Arc<str>>) -> Self

Rename the head (sort name) via sort_map, leaving arguments unchanged.

pub fn apply_maps( &self, sort_map: &HashMap<Arc<str>, Arc<str>>, op_map: &HashMap<Arc<str>, Arc<str>>, ) -> Self

Apply a sort-name rename to the head and an operation rename to every term in the argument list.

Trait Implementations

impl Clone for SortExpr

fn clone(&self) -> SortExpr

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for SortExpr

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for SortExpr

fn deserialize<D>(deserializer: D) -> Result<Self, D::Error>

where D: Deserializer<'de>,

Normalize on load: any App { name, args: [] } incoming from JSON collapses to Name(name) so that every downstream consumer sees the canonical spelling.

impl Display for SortExpr

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl From<&Arc<str>> for SortExpr

fn from(s: &Arc<str>) -> Self

Converts to this type from the input type.

impl From<&str> for SortExpr

fn from(s: &str) -> Self

Converts to this type from the input type.

impl From<Arc<str>> for SortExpr

fn from(s: Arc<str>) -> Self

Converts to this type from the input type.

impl From<String> for SortExpr

fn from(s: String) -> Self

Converts to this type from the input type.

impl Hash for SortExpr

fn hash<H: Hasher>(&self, state: &mut H)

Hash by head and arguments. This agrees with PartialEq::eq across the Name / empty-args App quotient so that both spellings occupy the same hash bucket when used as a map key.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl PartialEq for SortExpr

fn eq(&self, other: &Self) -> bool

Two sort expressions are equal when their heads and argument lists agree. This reduces Name(n) to App { name: n, args: [] } under equality, matching SortExpr::alpha_eq and ensuring that the Eq/Hash contract holds across both spellings.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Serialize for SortExpr

fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.

impl Eq for SortExpr