InitHEADmain

7 files changed, 237 insertions, 0 deletions

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..ea8c4bf
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1 @@
+/target
diff --git a/Cargo.lock b/Cargo.lock
new file mode 100644
index 0000000..9aaef71
--- /dev/null
+++ b/Cargo.lock
@@ -0,0 +1,132 @@
+# This file is automatically @generated by Cargo.
+# It is not intended for manual editing.
+version = 4
+
+[[package]]
+name = "convert_case"
+version = "0.10.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "633458d4ef8c78b72454de2d54fd6ab2e60f9e02be22f3c6104cdc8a4e0fceb9"
+dependencies = [
+ "unicode-segmentation",
+]
+
+[[package]]
+name = "derive_more"
+version = "2.1.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d751e9e49156b02b44f9c1815bcb94b984cdcc4396ecc32521c739452808b134"
+dependencies = [
+ "derive_more-impl",
+]
+
+[[package]]
+name = "derive_more-impl"
+version = "2.1.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "799a97264921d8623a957f6c3b9011f3b5492f557bbb7a5a19b7fa6d06ba8dcb"
+dependencies = [
+ "convert_case",
+ "proc-macro2",
+ "quote",
+ "rustc_version",
+ "syn",
+ "unicode-xid",
+]
+
+[[package]]
+name = "peg"
+version = "0.8.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "0aad070be5b63aa72103f2fcdd70a83adbd5e90112ce5b574171ff1c65501773"
+dependencies = [
+ "peg-macros",
+ "peg-runtime",
+]
+
+[[package]]
+name = "peg-macros"
+version = "0.8.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ddd8ef6825cae95355031ae26a99b616a2a21f22ba2de0197c43dfb05acbe7ee"
+dependencies = [
+ "peg-runtime",
+ "proc-macro2",
+ "quote",
+]
+
+[[package]]
+name = "peg-runtime"
+version = "0.8.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "7011d97b484a5ebdc4b1fdb3b12d5e4bbbea56e9d22b688f2e79e04b65a7d8a6"
+
+[[package]]
+name = "proc-macro2"
+version = "1.0.107"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "985e7ec9bb745e6ce6535b544d84d6cd6f7ad8bd711c398938ae983b91a766d9"
+dependencies = [
+ "unicode-ident",
+]
+
+[[package]]
+name = "quote"
+version = "1.0.47"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1fbf4db142a473a8d80c26bbf18454ed458bf8d26c8219c331daecfdbd079001"
+dependencies = [
+ "proc-macro2",
+]
+
+[[package]]
+name = "rustc_version"
+version = "0.4.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "cfcb3a22ef46e85b45de6ee7e79d063319ebb6594faafcf1c225ea92ab6e9b92"
+dependencies = [
+ "semver",
+]
+
+[[package]]
+name = "semver"
+version = "1.0.28"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8a7852d02fc848982e0c167ef163aaff9cd91dc640ba85e263cb1ce46fae51cd"
+
+[[package]]
+name = "syn"
+version = "2.0.119"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "872831b642d1a07999a962a351ed35b955ea2cfc8f3862091e2a240a84f17297"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "unicode-ident",
+]
+
+[[package]]
+name = "unicode-ident"
+version = "1.0.24"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e6e4313cd5fcd3dad5cafa179702e2b244f760991f45397d14d4ebf38247da75"
+
+[[package]]
+name = "unicode-segmentation"
+version = "1.13.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "c6f5d3c3b1bf09027a88a6bc961fc00497d651009560b5463668dc81b0fa87a8"
+
+[[package]]
+name = "unicode-xid"
+version = "0.2.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ebc1c04c71510c7f702b52b7c350734c9ff1295c464a03335b00bb84fc54f853"
+
+[[package]]
+name = "wittt"
+version = "0.1.0"
+dependencies = [
+ "derive_more",
+ "peg",
+]
diff --git a/Cargo.toml b/Cargo.toml
new file mode 100644
index 0000000..6b30505
--- /dev/null
+++ b/Cargo.toml
@@ -0,0 +1,8 @@
+[package]
+name = "wittt"
+version = "0.1.0"
+edition = "2024"
+
+[dependencies]
+derive_more = { version = "2.1.1", features = ["display"] }
+peg = "0.8.6"
diff --git a/src/main.rs b/src/main.rs
new file mode 100644
index 0000000..7e87917
--- /dev/null
+++ b/src/main.rs
@@ -0,0 +1,5 @@
+mod theory;
+
+fn main() {
+    println!("Hello, world!");
+}
diff --git a/src/theory/ast.rs b/src/theory/ast.rs
new file mode 100644
index 0000000..4236cd7
--- /dev/null
+++ b/src/theory/ast.rs
@@ -0,0 +1,45 @@
+use derive_more::Display;
+
+#[derive(Display)]
+#[display("{name}{{\n{}\n}}", DHList((stages, "\n")))]
+pub struct ASTTheory {
+    name: String,
+    stages: Vec<ASTStage>,
+}
+
+#[derive(Display)]
+#[display("{name} {} => {}", DHList((domain, ",")), DHList((domain, ",")))]
+pub struct ASTStage {
+    name: String,
+    domain: Vec<ASTRecordEntry>,
+    codomain: Vec<ASTRecordEntry>,
+}
+
+#[derive(Display)]
+pub enum ASTRecordEntry {
+    #[display("{name} type")]
+    ASTType { name: String },
+    #[display("{path} : {of}")]
+    ASTTerm { path: ASTPath, of: String },
+    #[display("{path} ~: {of}")]
+    ASTDependency { path: ASTPath, of: String },
+    #[display("{lhs_path} == {rhs_path}")]
+    ASTEquality {
+        lhs_path: ASTPath,
+        rhs_path: ASTPath,
+    },
+    #[display("let {var} = {stage}({})", DHList((args, ", ")))]
+    ASTLet {
+        var: String,
+        stage: String,
+        args: Vec<ASTPath>,
+    },
+}
+
+#[derive(Display)]
+#[display("{}", DHList((_0, ".")))]
+pub struct ASTPath(Vec<String>);
+
+#[derive(Display)]
+#[display("{}", _0.0.iter().map(|x| x.to_string()).collect::<Vec<_>>().join(_0.1))]
+struct DHList<'a, T: std::fmt::Display>((&'a Vec<T>, &'static str));
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>,
+}
diff --git a/src/theory/mod.rs b/src/theory/mod.rs
new file mode 100644
index 0000000..d8d26d1
--- /dev/null
+++ b/src/theory/mod.rs
@@ -0,0 +1,3 @@
+mod ast;
+mod check;
+mod context;