Crate panproto_gat 

panproto-gat

The GAT (Generalized Algebraic Theory) engine for panproto.

This is Level 0 of the panproto architecture, the only component implemented directly in Rust rather than as data. It provides:

• Sorts: Types that may depend on terms of other sorts
• Operations: Term constructors with typed inputs and outputs
• Equations: Judgemental equalities between terms
• Theories: Named collections of sorts, operations, and equations
• Theory morphisms: Structure-preserving maps between theories
• Colimits: Pushouts of theories for composing schema languages
• Pullbacks: Intersections of theories for overlap discovery
• Models: Interpretations of theories in Set
• Type-checking: Verification that terms and equations are well-typed
• Natural transformations: Morphisms between theory morphisms
• Free models: Initial model construction from theories
• Quotient theories: Theory simplification by merging identified elements

The mathematical foundations are based on Cartmell (1986) and the GATlab architecture (Lynch et al., 2024).

Re-exports

pub use composition::CompositionSpec;

pub use composition::CompositionStep;

pub use composition::recompose;

pub use alg_struct::AlgStruct;

pub use alg_struct::StructField;

pub use alg_struct::StructParam;

pub use refinement::RefinedSort;

pub use refinement::RefinementConstraint;

pub use refinement::RefinementError;

pub use rewriting::ConfluenceReport;

pub use rewriting::CriticalPair;

pub use rewriting::OpPrecedence;

pub use rewriting::RuleViolation;

pub use rewriting::TerminationReport;

pub use rewriting::check_local_confluence;

pub use rewriting::check_termination_via_lpo;

pub use rewriting::lpo_greater;

pub use witness::EqWitness;

pub use witness::WitnessJustification;

Modules

alg_struct

Algebraic struct types for theories.

composition

Declarative composition specs for theory colimit recipes.

refinement

Refinement types: sorts constrained by predicates.

rewriting

Rewrite-system properties: confluence and termination.

witness

Equality witnesses: propositional equality proofs.

Structs

CaseBranch

One branch of a Term::Case expression.

CheckModelOptions

Options for model checking.

ColimitResult

Result of a categorical pushout (colimit) computation.

ConflictPolicy

A conflict resolution policy for merge operations.

DirectedEquation

A directed equation (rewrite rule) with a computation term.

Equation

An equation (axiom) in a GAT.

EquationViolation

A single violation of an equation in a model.

Factorization

The result of factorizing a theory morphism.

FreeModelConfig

Configuration for free model construction.

FreeModelResult

Result of free model construction, including completeness status.

HoleReport

A report generated for each typed hole encountered by typecheck_term_with_holes.

Ident

A first-class identifier separating stable identity from display name.

Model

A model (interpretation) of a theory in Set.

Name

An interned name handle with a pointer-equality fast path.

NaturalTransformation

A natural transformation between two theory morphisms F, G: T1 -> T2.

Operation

An operation (term constructor) in a GAT.

PullbackResult

Result of a pullback computation.

ScopeTag

An opaque scope tag distinguishing different naming contexts.

SiteRename

A site-qualified rename operation.

Sort

A sort declaration in a GAT.

SortParam

A parameter of a dependent sort.

SortScheme

A sort scheme: a sort expression universally quantified over a list of metavariable names.

Theory

A generalized algebraic theory (GAT).

TheoryEndofunctor

A theory endofunctor: maps theories to theories.

TheoryMorphism

A structure-preserving map between two theories.

Enums

CoercionClass

Classification of a coercion’s round-trip properties.

ConflictStrategy

A conflict resolution strategy for merge operations.

GatError

Errors that can occur in GAT operations.

Implicit

Implicit/explicit tag on an Operation input parameter.

ModelValue

A value in a model interpretation.

NameSite

Enumerates the 9 naming sites in the panproto system.

SortClosure

Closure attribute on a Sort.

SortExpr

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

SortKind

The kind of a sort, distinguishing structural sorts from value/coercion sorts.

Term

A term in a GAT expression.

TheoryConstraint

A predicate on theories: the precondition for applying a transform.

TheoryTransform

How a theory endofunctor transforms a theory.

ValueKind

The primitive value kind that a value sort ranges over.

Functions

alpha_equivalent

Check if two terms are α-equivalent (equal up to consistent variable renaming).

alpha_equivalent_equation

Check if two equations are α-equivalent.

check_interchange

Check the interchange law for 2-categorical structure.

check_model

Check whether a model satisfies all equations of its theory.

check_model_with_options

Check with configurable options.

check_morphism

Soundness note on equation preservation

check_natural_transformation

Check that a natural transformation is valid.

classify_builtin_coercion

Classify a builtin coercion operation by its source/target value kinds and round-trip class.

colimit

Compute the pushout (colimit) of two theories over explicit morphisms.

colimit_by_name

Compute the pushout (colimit) of two theories over a shared base theory.

compose_subst

Compose two term substitutions.

factorize

Factorize a theory morphism into elementary endofunctors.

free_model

Construct a bounded approximation of the free (initial) model.

horizontal_compose

Horizontal composition: given alpha: F => G and beta: H => K where G’s codomain is H’s domain, produce (beta * alpha): H.F => K.G.

infer_var_sorts

Infer variable sorts from an equation’s term structure.

match_pattern

Try to match a pattern term against a concrete term, returning a substitution if successful. Pattern variables can match any subterm; operation names must match exactly.

migrate_model

Migrate a model along a theory morphism.

normalize

Normalize a term by repeatedly applying directed equations as rewrite rules.

positional_param_rename

Build a variable-rename substitution that sends each domain parameter name to the codomain parameter name at the same position.

pullback

Compute the pullback of two theories over a common codomain.

quotient

Quotient a theory by identifying sorts and/or operations.

resolve_theory

Resolve a theory by computing the transitive closure of its extends chain.

signatures_equivalent_modulo_param_rename

Compare two operation or sort signatures modulo positional alpha-rename of the declared parameter names.

sort_params_equivalent_modulo_rename

Compare two sort declarations’ parameter blocks modulo positional alpha-rename of the declared parameter names.

th_editable_structure

The abstract theory of editable structures (Hofmann, Pierce, Wagner 2012).

typecheck_equation

Typecheck an equation: infer variable sorts, typecheck both sides, verify they produce the same output sort.

typecheck_equation_modulo_rewrites

Typecheck an equation with sort equality relaxed modulo a set of directed rewrite rules.

typecheck_term

Infer the output sort expression of a term given a variable context and theory.

typecheck_term_with_holes

Typecheck a term, collecting a HoleReport at every Term::Hole site.

typecheck_theory

Typecheck all equations in a theory.

validate_factorization

Validate that applying a factorization to the domain yields a theory compatible with the codomain.

vertical_compose

Vertical composition: given alpha: F => G and beta: G => H, produce beta . alpha: F => H.

Type Aliases

VarContext

A variable typing context.