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
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63

//! # Inline operations of categories with definitions

use open_hypergraphs::lax::{
    OpenHypergraph,
    functor::{Functor, try_define_map_arrow},
};

pub use super::types::*;

use std::collections::HashMap;
use std::hash::Hash;

#[derive(Clone)]
pub struct Inline<K, O, A> {
    env: HashMap<K, OpenHypergraph<O, A>>,
}

// Def<String, Copy> → lang::Term
// Copy → Copy

// TODO: generalise definition?
impl<K: Clone + Hash + Eq, O: Clone + PartialEq, A: Clone> Functor<O, Def<K, A>, O, Option<A>>
    for Inline<K, O, A>
{
    fn map_object(&self, o: &O) -> impl ExactSizeIterator<Item = O> {
        std::iter::once(o.clone())
    }

    fn map_operation(
        &self,
        a: &Def<K, A>,
        source: &[O],
        target: &[O],
    ) -> OpenHypergraph<O, Option<A>> {
        match a {
            Def::Def(k) => match self.env.get(k) {
                Some(term) => term.clone().map_edges(Some),
                None => OpenHypergraph::singleton(None, source.to_vec(), target.to_vec()),
            },
            Def::Arr(a) => {
                OpenHypergraph::singleton(Some(a.clone()), source.to_vec(), target.to_vec())
            }
        }
    }

    fn map_arrow(&self, f: &OpenHypergraph<O, Def<K, A>>) -> OpenHypergraph<O, Option<A>> {
        try_define_map_arrow(self, f).unwrap()
    }
}

// TODO: error with missing definitions!
pub fn inline<K: Clone + Hash + Eq, O: Clone + PartialEq, A: Clone + PartialEq>(
    env: HashMap<K, OpenHypergraph<O, A>>,
    term: OpenHypergraph<O, Def<K, A>>,
) -> Option<OpenHypergraph<O, A>> {
    let result = Inline { env }.map_arrow(&term);

    #[allow(clippy::manual_unwrap_or_default)]
    result.with_edges(|edges| match edges.into_iter().collect() {
        Some(e) => e,
        None => vec![], // Propagate error up- with_edges will fail if this is empty.
    })
}