metacat 0.2.1

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

//! Builtin `nat` syntax category used by the multi-theory loader.
//!
//! This is the free symmetric monoidal category generated by:
//! - one object `One`
//! - one arrow `one : I -> One`
//!
//! A natural number `n` is represented by an arrow `I -> One^n`, encoded in
//! surface syntax by the numeral `n`.
//!
//! Strictly speaking, a numeral `n` is actually a *definition* named `n`, standing for the
//! `n`-fold tensor product of the generating arrow `one`, denoted `1`.
//! However, in a (unique) special case, these definitions are inlined, so that one can write
//! `foo : 2 -> 1` and have it auto-expanded to `foo : {1 1} -> 1` under the hood.

use hexpr::{Operation, Signature};

/// Reserved theory name for the builtin `nat` syntax category.
pub const NAT_THEORY_NAME: &str = "nat";

/// Parsed operation key for the builtin `nat` syntax category.
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct NatKey(pub usize);

/// Signature adapter for interpreting numerals as arrows `I -> One^n`.
pub struct NatObj;

impl Signature for NatObj {
    type Arr = NatKey;
    type Obj = ();
    type Error = std::num::ParseIntError;

    fn try_parse_op(&self, op: &Operation) -> Result<Self::Arr, Self::Error> {
        Ok(NatKey(op.as_str().parse()?))
    }

    fn profile(&self, op: &Self::Arr) -> (Vec<Option<Self::Obj>>, Vec<Option<Self::Obj>>) {
        (vec![], vec![Some(()); op.0])
    }
}