From c5ebf74c917b94c8499fa5cd2e125b04ec7529b4 Mon Sep 17 00:00:00 2001
From: tslil <tslil@posteo.de>
Date: Mon, 27 Apr 2026 15:49:54 +0100
Subject: prepare for more work on signatures, in particular this means
 processing records in telescoped contexts

rework ElementValue, CheckedElement to be type aliases for the generic version over Term : Type
---
 src/checker_state.rs | 62 ++++++++++++++++++++++++++++++++++++++++------------
 1 file changed, 48 insertions(+), 14 deletions(-)

(limited to 'src/checker_state.rs')

diff --git a/src/checker_state.rs b/src/checker_state.rs
index 31c3bde..a14a6e4 100644
--- a/src/checker_state.rs
+++ b/src/checker_state.rs
@@ -37,6 +37,8 @@ pub enum CheckerError {
     },
 }
 
+// -----------------------------------------------------------------------------
+// Generics for wrapping fields, values, and coercing them
 #[derive(Display, Clone)]
 #[display("{field} @ {owner}")]
 pub struct Field<T: std::fmt::Display> {
@@ -45,31 +47,45 @@ pub struct Field<T: std::fmt::Display> {
 }
 
 #[derive(Display, Clone)]
-pub enum ElementValue {
-    Concrete(Element),
+pub enum Value<Term: std::fmt::Display, Type: std::fmt::Display> {
+    Concrete(Term),
     #[display("_ : {_0}")]
-    Hypothetical(Set),
+    Hypothetical(Type),
+}
+
+pub type ElementValue = Value<Element, Set>;
+pub type InstanceValue = Value<Instance, Signature>;
+
+impl From<Element> for Value<Element, Set> {
+    fn from(e: Element) -> Value<Element, Set> {
+        Value::Concrete(e)
+    }
 }
 
-impl From<Element> for ElementValue {
-    fn from(e: Element) -> ElementValue {
-        ElementValue::Concrete(e)
+impl From<Instance> for Value<Instance, Signature> {
+    fn from(i: Instance) -> Value<Instance, Signature> {
+        Value::Concrete(i)
     }
 }
 
 #[derive(Display, Clone)]
-#[display("{value} : {set}")]
-pub struct CheckedElement {
-    pub value: ElementValue,
-    pub set: Set,
+#[display("{value} : {container}")]
+pub struct Checked<Term: std::fmt::Display, Type: std::fmt::Display> {
+    pub value: Value<Term, Type>,
+    pub container: Type,
 }
 
+pub type CheckedElement = Checked<Element, Set>;
+pub type CheckedInstance = Checked<Instance, Signature>;
+
+// -----------------------------------------------------------------------------
+// The checker state
 #[derive(Default, Clone)]
 pub struct CheckerState {
     wf_sets: HashMap<String, Set>,
     wf_elements: HashMap<String, CheckedElement>,
     wf_signatures: HashMap<String, Signature>,
-    wf_instances: HashMap<String, Instance>,
+    wf_instances: HashMap<String, CheckedInstance>,
     record_fields: HashMap<String, Field<Set>>,
     variant_fields: HashMap<String, Field<Set>>,
     signature_fields: HashMap<String, Field<Signature>>,
@@ -239,15 +255,15 @@ impl CheckerState {
     pub fn add_element(
         &mut self,
         name: String,
-        element: ElementValue,
+        element: Value<Element, Set>,
         set: Set,
     ) -> Result<(), CheckerError> {
         self.assert_unbound_element(&name)?;
         self.wf_elements.insert(
             name,
-            CheckedElement {
+            Checked {
                 value: element,
-                set,
+                container: set,
             },
         );
         Ok(())
@@ -344,6 +360,24 @@ impl CheckerState {
         Ok(())
     }
 
+    #[instrument(skip(self), level = "debug", fields(%name, %instance, %signature))]
+    pub fn add_instance(
+        &mut self,
+        name: String,
+        instance: InstanceValue,
+        signature: Signature,
+    ) -> Result<(), CheckerError> {
+        self.assert_unbound_element(&name)?;
+        self.wf_instances.insert(
+            name,
+            Checked {
+                value: instance,
+                container: signature,
+            },
+        );
+        Ok(())
+    }
+
     pub fn lookup_signature(&self, name: &String) -> Result<&Signature, CheckerError> {
         self.wf_signatures
             .get(name)
-- 
cgit v1.3.1