Struct Sort 

pub struct Sort {
    pub name: Arc<str>,
    pub params: Vec<SortParam>,
    pub kind: SortKind,
    pub closure: SortClosure,
}

A sort declaration in a GAT.

Sorts are the types of a GAT. They may be simple (no parameters) or dependent (parameterized by terms of other sorts). A sort may additionally be declared closed against an enumerated set of constructors, enabling exhaustive pattern matching.

Examples

• Simple sort: Vertex (no params)
• Dependent sort: Hom(a: Ob, b: Ob) (two params of sort Ob)
• Dependent sort: Constraint(v: Vertex) (one param of sort Vertex)
• Closed inductive sort: Nat closed against [zero, succ]

Based on the formal definition of GAT sorts from Cartmell (1986).

Fields

name: Arc<str>

The sort name (e.g., “Vertex”, “Edge”, “Hom”).

params: Vec<SortParam>

Parameters this sort depends on. Empty for simple sorts.

kind: SortKind

The kind of this sort (structural, value, coercion, or merger).

closure: SortClosure

Closure attribute. Defaults to SortClosure::Open.

Implementations

impl Sort

pub fn simple(name: impl Into<Arc<str>>) -> Self

Create a simple (non-dependent) sort with structural kind and open closure.

pub fn dependent(name: impl Into<Arc<str>>, params: Vec<SortParam>) -> Self

Create a dependent sort with the given parameters, structural kind, and open closure.

pub fn with_kind(name: impl Into<Arc<str>>, kind: SortKind) -> Self

Create a simple sort with a specific kind and open closure.

pub fn closed<I, S>( name: impl Into<Arc<str>>, params: Vec<SortParam>, constructors: I, ) -> Self

where I: IntoIterator<Item = S>, S: Into<Arc<str>>,

Create a closed simple sort with the given constructor op names.

The closure declares these ops as the exhaustive set of constructors for this sort. A Term::Case over the sort must cover every listed constructor exactly once; adding a new constructor elsewhere in the theory without updating the closure fails typecheck_theory.

pub fn default_vertex_kind(&self) -> Arc<str>

Returns the canonical schema-level vertex kind for this sort.

The vertex kind is derived from the SortKind via the Grothendieck fibration: Val(vk) maps to the canonical value kind name, Structural maps to the sort name itself.

pub fn is_simple(&self) -> bool

Returns true if this sort has no parameters.

pub fn arity(&self) -> usize

Returns the arity (number of parameters) of this sort.

Trait Implementations

impl Clone for Sort

fn clone(&self) -> Sort

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Sort

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

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for Sort

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl Hash for Sort

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

Feeds this value into the given Hasher.

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 Sort

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

Tests for self and other values to be equal, and is used by ==.

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 Sort

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 Sort

impl StructuralPartialEq for Sort