panproto-gat 0.39.0

GAT (Generalized Algebraic Theory) engine for panproto
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89

//! # 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).

pub mod alg_struct;
mod check_model;
mod colimit;
pub mod composition;
mod eq;
mod error;
mod factorize;
mod free_model;
mod ident;
mod model;
mod morphism;
mod nat_transform;
mod op;
mod pullback;
mod quotient;
pub mod refinement;
pub mod rewriting;
mod schema_functor;
mod sort;
mod theory;
mod typecheck;
pub mod witness;

pub use check_model::{
    CheckModelOptions, EquationViolation, check_model, check_model_with_options,
};
pub use colimit::{ColimitResult, colimit, colimit_by_name};
pub use composition::{CompositionSpec, CompositionStep, recompose};
pub use factorize::{Factorization, factorize, validate_factorization};

pub use eq::{
    CaseBranch, DirectedEquation, Equation, Term, alpha_equivalent, alpha_equivalent_equation,
    compose_subst, match_pattern, normalize,
};
pub use error::GatError;
pub use free_model::{FreeModelConfig, FreeModelResult, free_model};
pub use ident::{Ident, Name, NameSite, ScopeTag, SiteRename};
pub use model::{Model, ModelValue, migrate_model};
pub use morphism::{TheoryMorphism, check_morphism};
pub use nat_transform::{
    NaturalTransformation, check_interchange, check_natural_transformation, horizontal_compose,
    vertical_compose,
};
pub use op::{Implicit, Operation};
pub use pullback::{PullbackResult, pullback};
pub use quotient::quotient;
pub use schema_functor::{TheoryConstraint, TheoryEndofunctor, TheoryTransform};
pub use sort::{
    CoercionClass, Sort, SortClosure, SortExpr, SortKind, SortParam, ValueKind,
    classify_builtin_coercion, positional_param_rename, signatures_equivalent_modulo_param_rename,
    sort_params_equivalent_modulo_rename,
};
pub use theory::{ConflictPolicy, ConflictStrategy, Theory, resolve_theory, th_editable_structure};
pub use typecheck::{
    HoleReport, SortScheme, VarContext, infer_var_sorts, typecheck_equation,
    typecheck_equation_modulo_rewrites, typecheck_term, typecheck_term_with_holes,
    typecheck_theory,
};

pub use alg_struct::{AlgStruct, StructField, StructParam};
pub use refinement::{RefinedSort, RefinementConstraint, RefinementError};
pub use rewriting::{
    ConfluenceReport, CriticalPair, OpPrecedence, RuleViolation, TerminationReport,
    check_local_confluence, check_termination_via_lpo, lpo_greater,
};
pub use witness::{EqWitness, WitnessJustification};