metacat 0.2.0

metacat: a categorical theorem prover
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

//! Loader and data model for the multi-theory surface syntax.
//!
//! This module provides the primary parsing and resolution pipeline for files
//! of the form:
//!
//! ```text
//! (theory fol.syntax nat { ... })
//! (theory fol.proof fol.syntax { ... })
//! ```
//!
//! A complete file can be loaded directly from a string:
//!
//! ```rust
//! use metacat::theory::{Theory, TheoryId, TheorySet};
//!
//! let file = TheorySet::from_text(
//!     r#"
//!     (theory fol.syntax nat {
//!       (arr wff : 1 -> 1)
//!       (arr -> : 2 -> 1)
//!       (arr -. : 1 -> 1)
//!     })
//!
//!     (theory fol.proof fol.syntax {
//!       (arr wn : wff -> (-. wff))
//!       (arr wi : {wff wff} -> (-> wff))
//!       (def win : {wff wff} -> (-> -. wff) = (wi wn))
//!     })
//!     "#,
//! )?;
//!
//! let syntax_id = TheoryId("fol.syntax".parse()?);
//! let proof_id = TheoryId("fol.proof".parse()?);
//!
//! assert!(matches!(file.theories.get(&syntax_id), Some(Theory::Theory { .. })));
//! assert!(matches!(file.theories.get(&proof_id), Some(Theory::Theory { .. })));
//! # Ok::<(), Box<dyn std::error::Error>>(())
//! ```
//!
//! Multiple source strings can be loaded together before resolution:
//!
//! ```rust
//! use metacat::theory::{Theory, TheoryId, TheorySet};
//!
//! let file = TheorySet::from_texts([
//!     r#"
//!     (theory fol.syntax nat {
//!       (arr wff : 1 -> 1)
//!       (arr -> : 2 -> 1)
//!     })
//!     "#,
//!     r#"
//!     (theory fol.proof fol.syntax {
//!       (arr wi : {wff wff} -> (-> wff))
//!     })
//!     "#,
//! ])?;
//!
//! let proof_id = TheoryId("fol.proof".parse()?);
//! assert!(matches!(file.theories.get(&proof_id), Some(Theory::Theory { .. })));
//! # Ok::<(), Box<dyn std::error::Error>>(())
//! ```
//!
//! The implementation is split into:
//! - [`ast`], which parses raw hexprs into a file-level AST;
//! - [`nat`], which defines the builtin `nat` syntax category;
//! - [`model`], which defines the resolved in-memory representation;
//! - [`load`], which resolves theory dependencies and interprets type maps and
//!   definitions into open hypergraphs.

pub mod ast;
pub mod load;
pub mod model;
pub mod nat;

pub use ast::{MergeRawError, RawTheorySet};
pub use load::LoadError;
pub use model::{Term, Theory, TheoryArrow, TheoryId, TheorySet};