panproto_gat/
lib.rs

1//! # panproto-gat
2//!
3//! The GAT (Generalized Algebraic Theory) engine for panproto.
4//!
5//! This is Level 0 of the panproto architecture, the only component
6//! implemented directly in Rust rather than as data. It provides:
7//!
8//! - **Sorts**: Types that may depend on terms of other sorts
9//! - **Operations**: Term constructors with typed inputs and outputs
10//! - **Equations**: Judgemental equalities between terms
11//! - **Theories**: Named collections of sorts, operations, and equations
12//! - **Theory morphisms**: Structure-preserving maps between theories
13//! - **Colimits**: Pushouts of theories for composing schema languages
14//! - **Pullbacks**: Intersections of theories for overlap discovery
15//! - **Models**: Interpretations of theories in Set
16//! - **Type-checking**: Verification that terms and equations are well-typed
17//! - **Natural transformations**: Morphisms between theory morphisms
18//! - **Free models**: Initial model construction from theories
19//! - **Quotient theories**: Theory simplification by merging identified elements
20//!
21//! The mathematical foundations are based on Cartmell (1986) and
22//! the `GATlab` architecture (Lynch et al., 2024).
23
24pub mod alg_struct;
25mod check_model;
26mod colimit;
27pub mod composition;
28mod eq;
29mod error;
30mod factorize;
31mod free_model;
32mod ident;
33mod model;
34mod morphism;
35mod nat_transform;
36mod op;
37mod pullback;
38mod quotient;
39pub mod refinement;
40pub mod rewriting;
41mod schema_functor;
42mod sort;
43mod theory;
44mod typecheck;
45pub mod witness;
46
47pub use check_model::{
48    CheckModelOptions, EquationViolation, check_model, check_model_with_options,
49};
50pub use colimit::{ColimitResult, colimit, colimit_by_name};
51pub use composition::{CompositionSpec, CompositionStep, recompose};
52pub use factorize::{Factorization, factorize, validate_factorization};
53
54pub use eq::{
55    CaseBranch, DirectedEquation, Equation, Term, alpha_equivalent, alpha_equivalent_equation,
56    compose_subst, match_pattern, normalize,
57};
58pub use error::GatError;
59pub use free_model::{FreeModelConfig, FreeModelResult, free_model};
60pub use ident::{Ident, Name, NameSite, ScopeTag, SiteRename};
61pub use model::{Model, ModelValue, migrate_model};
62pub use morphism::{TheoryMorphism, check_morphism};
63pub use nat_transform::{
64    NaturalTransformation, check_interchange, check_natural_transformation, horizontal_compose,
65    vertical_compose,
66};
67pub use op::{Implicit, Operation};
68pub use pullback::{PullbackResult, pullback};
69pub use quotient::quotient;
70pub use schema_functor::{TheoryConstraint, TheoryEndofunctor, TheoryTransform};
71pub use sort::{
72    CoercionClass, Sort, SortClosure, SortExpr, SortKind, SortParam, ValueKind,
73    classify_builtin_coercion, positional_param_rename, signatures_equivalent_modulo_param_rename,
74    sort_params_equivalent_modulo_rename,
75};
76pub use theory::{ConflictPolicy, ConflictStrategy, Theory, resolve_theory, th_editable_structure};
77pub use typecheck::{
78    HoleReport, SortScheme, VarContext, infer_var_sorts, typecheck_equation,
79    typecheck_equation_modulo_rewrites, typecheck_term, typecheck_term_with_holes,
80    typecheck_theory,
81};
82
83pub use alg_struct::{AlgStruct, StructField, StructParam};
84pub use refinement::{RefinedSort, RefinementConstraint, RefinementError};
85pub use rewriting::{
86    ConfluenceReport, CriticalPair, OpPrecedence, RuleViolation, TerminationReport,
87    check_local_confluence, check_termination_via_lpo, lpo_greater,
88};
89pub use witness::{EqWitness, WitnessJustification};
panproto_gat/lib.rs

panproto_gat/
lib.rs
