aufbau 0.3.1

Generalized prefix parsing for a class of context-dependent languages
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

//! Typing constraint domain — `sec:typing-domain`, §3 of the draft.
//!
//! The constraint domain `D = (Rules, Closed, Ctx, eval, ⊕)` is realized by:
//! - rules    = `TypingRule`
//! - evidence = `Type` (interned as `TypeId = EvidenceId`)
//! - `Ctx`    = `Context` (ordered `Identifier → Type` map)
//! - `∇`      = `ContextTransition` (extend/overwrite operations on `Context`)
//!
//! ## Realizability status
//!
//! ### Monotonicity (`lem:evidence-monotone`-analog)
//! Status: PROVEN — §3 Lemma (Type evidence is monotone).
//! Type evidence can only shrink under input extension via regex derivatives.
//!
//! ### Evidence realizability (`lem:evidence-realizable`-analog)
//! Status: PROVEN — §3 Lemma (Type evidence is realizable).
//!
//! ### Premise realizability (`lem:typeof-realizable`-analog)
//! Status: PROVEN — §3 Lemma (`typeof` is realizable).
//!
//! ### Rule realizability (`lem:rule-realizable`-analog)
//! Status: PROVEN — §3 Lemma (Rule realizability).
//!
//! ### `eval_impl` = eval (`thm:typing-realizable`-analog)
//! Status: PROVEN — §3 Theorem (Typing implementation computes ideal evaluator).

pub mod complete;
pub mod context;
pub mod domain;
pub mod ir;
pub mod loader;
pub mod normalize;
pub mod pattern;
pub mod rule;
pub mod syntax;
pub mod term;
pub mod types;

#[cfg(test)]
mod tests;

pub use complete::{Completeness, completeness};
pub use context::{Context, ContextTransition};
pub use domain::TypingDomain;
pub use ir::{Instr, Program, compile};
pub use normalize::{Normalizer, RewriteRule, unify_modulo};
pub use pattern::{Match, Pattern};
pub use syntax::render;
pub use term::{Evidence, Subst, Term};
pub use types::{Atom, TyExpr, Type, TypeExpr};

pub use rule::{Conclusion, Judgment, Premise, PremiseStatus, RuleParser, TypingRule};

pub use crate::engine::synth::Synthesizer as TypingSynth;
pub use crate::semantics::runtime::TypingRuntime;