1 files changed, 43 insertions, 0 deletions
diff --git a/src/theory/context.rs b/src/theory/context.rs
new file mode 100644
index 0000000..241cd9a
--- /dev/null
+++ b/src/theory/context.rs
@@ -0,0 +1,43 @@
+use std::collections::{HashMap, HashSet};
+
+pub struct TheoryContext {
+    name: String,
+    stages: HashMap<String, StageContext>,
+}
+
+pub struct StageContext {
+    domain: RecordContext,
+    codomain: RecordContext,
+}
+
+pub enum TheoryMorphismKind {
+    Term,
+    Dependency,
+}
+
+pub type TheoryType = String;
+pub type TheoryMorphism = String;
+
+pub struct CheckedPath {
+    domain_type: TheoryType,
+    codomain_type: TheoryType,
+    path: Vec<TheoryMorphism>,
+    kind: TheoryMorphismKind,
+}
+
+pub struct RecordContext {
+    /// The types at issue.
+    types: HashSet<TheoryType>,
+    /// The known terms/dependencies.
+    terms: Vec<CheckedPath>,
+    /// Equalities between parallel composites indexed by their paired (domain,
+    /// codomain) types.
+    equality: HashMap<(TheoryType, TheoryType), (CheckedPath, CheckedPath)>,
+    /// TODO
+    bindings: HashMap<String, CheckedStageReference>,
+}
+
+pub struct CheckedStageReference {
+    stage: String,
+    via: Box<RecordContext>,
+}