From 62cfbb77d4d153cdcc61b0f8c063a358dfcbbc29 Mon Sep 17 00:00:00 2001
From: tslil <tslil@posteo.de>
Date: Mon, 27 Apr 2026 15:16:06 +0100
Subject: basic signature functionality, missing extension signatures

---
 src/checker_set.rs       |  5 +----
 src/checker_signature.rs | 23 ++++++++++++++++++++---
 src/checker_state.rs     |  6 ++++++
 3 files changed, 27 insertions(+), 7 deletions(-)

diff --git a/src/checker_set.rs b/src/checker_set.rs
index 2ea0c3d..2faca9e 100644
--- a/src/checker_set.rs
+++ b/src/checker_set.rs
@@ -14,10 +14,7 @@ impl CheckerState {
                     .into_iter()
                     .map(|RecordField { name, set }| {
                         let set = self.check_set(set)?;
-                        Ok(RecordField {
-                            name: name.clone(),
-                            set,
-                        })
+                        Ok(RecordField { name, set })
                     })
                     .collect::<Result<Vec<_>, _>>()?;
                 Ok(Set::Record(fields))
diff --git a/src/checker_signature.rs b/src/checker_signature.rs
index 8fc982a..4fa723f 100644
--- a/src/checker_signature.rs
+++ b/src/checker_signature.rs
@@ -6,8 +6,25 @@ use tracing::instrument;
 impl CheckerState {
     #[instrument(skip(self), level = "debug", fields(%signature))]
     pub fn check_signature(&self, signature: Signature) -> Result<Signature, CheckerError> {
-        Err(CheckerError::Unimplemented(
-            "signature checking".to_string(),
-        ))
+        match signature {
+            Signature::Set => Ok(Signature::Set),
+            Signature::Var(v) => {
+                let deref = self.lookup_signature(&v)?;
+                Ok(deref.clone())
+            }
+            Signature::Ext { params, codomain } => Err(CheckerError::Unimplemented(
+                "extension signatures".to_string(),
+            )),
+            Signature::Theory(fields) => {
+                let fields = fields
+                    .into_iter()
+                    .map(|SigField { signature, name }| {
+                        let signature = self.check_signature(signature)?;
+                        Ok(SigField { name, signature })
+                    })
+                    .collect::<Result<Vec<_>, _>>()?;
+                Ok(Signature::Theory(fields))
+            }
+        }
     }
 }
diff --git a/src/checker_state.rs b/src/checker_state.rs
index 8ec153d..31c3bde 100644
--- a/src/checker_state.rs
+++ b/src/checker_state.rs
@@ -343,4 +343,10 @@ impl CheckerState {
 
         Ok(())
     }
+
+    pub fn lookup_signature(&self, name: &String) -> Result<&Signature, CheckerError> {
+        self.wf_signatures
+            .get(name)
+            .map_or(Err(CheckerError::Unbound(name.clone())), Ok)
+    }
 }
-- 
cgit v1.3.1