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
90
91
92
93
94
95
96
97
98
99
use std::sync::Arc;
/// An operation (term constructor) in a GAT.
///
/// Operations are the functions/constructors of a GAT. Each operation
/// has typed inputs and a typed output, where types are sort names.
///
/// # Examples
///
/// - `src: Edge → Vertex` (graph source map)
/// - `add: (a: Int, b: Int) → Int` (integer addition)
/// - `id: (x: Ob) → Hom(x, x)` (identity morphism)
///
/// Based on the formal definition of GAT operations from Cartmell (1986).
#[derive(Debug, Clone, PartialEq, Eq, Hash, serde::Serialize, serde::Deserialize)]
pub struct Operation {
/// The operation name (e.g., "src", "tgt", "compose").
pub name: Arc<str>,
/// Typed inputs as `(param_name, sort_name)` pairs.
pub inputs: Vec<(Arc<str>, Arc<str>)>,
/// The output sort name.
pub output: Arc<str>,
}
impl Operation {
/// Create a new operation.
#[must_use]
pub fn new(
name: impl Into<Arc<str>>,
inputs: Vec<(Arc<str>, Arc<str>)>,
output: impl Into<Arc<str>>,
) -> Self {
Self {
name: name.into(),
inputs,
output: output.into(),
}
}
/// Create a unary operation (one input, one output).
#[must_use]
pub fn unary(
name: impl Into<Arc<str>>,
input_name: impl Into<Arc<str>>,
input_sort: impl Into<Arc<str>>,
output: impl Into<Arc<str>>,
) -> Self {
Self {
name: name.into(),
inputs: vec![(input_name.into(), input_sort.into())],
output: output.into(),
}
}
/// Create a nullary operation (constant / zero-input constructor).
#[must_use]
pub fn nullary(name: impl Into<Arc<str>>, output: impl Into<Arc<str>>) -> Self {
Self {
name: name.into(),
inputs: Vec::new(),
output: output.into(),
}
}
/// Returns the number of inputs.
#[must_use]
pub fn arity(&self) -> usize {
self.inputs.len()
}
}
#[cfg(test)]
mod tests {
use super::*;
#[test]
fn unary_op() {
let op = Operation::unary("src", "e", "Edge", "Vertex");
assert_eq!(op.arity(), 1);
assert_eq!(&*op.output, "Vertex");
}
#[test]
fn nullary_op() {
let op = Operation::nullary("zero", "Int");
assert_eq!(op.arity(), 0);
assert_eq!(&*op.output, "Int");
}
#[test]
fn binary_op() {
let op = Operation::new(
"add",
vec![("a".into(), "Int".into()), ("b".into(), "Int".into())],
"Int",
);
assert_eq!(op.arity(), 2);
}
}