From 0886a16d73145270e953b8c2e0a4452b518ea16e Mon Sep 17 00:00:00 2001
From: tslil <tslil@posteo.de>
Date: Fri, 1 May 2026 12:36:24 +0100
Subject: working on fixing app, rework ast to have generics etc

---
 src/checker_state.rs | 41 ++++++++++++++++++++++-------------------
 1 file changed, 22 insertions(+), 19 deletions(-)

(limited to 'src/checker_state.rs')

diff --git a/src/checker_state.rs b/src/checker_state.rs
index 3d933f2..a8473ff 100644
--- a/src/checker_state.rs
+++ b/src/checker_state.rs
@@ -50,10 +50,10 @@ pub enum CheckerError {
         claimed: Signature,
         reason: String,
     },
-    #[display("Non-functional instance {instance} found in application to element {element}")]
+    #[display("Non-functional instance {instance} found in application to elements {}", elements.iter().map(|e| e.to_string()).collect::<Vec<_>>().join(" "))]
     NonFunctionalInstance {
         instance: Instance,
-        element: Element,
+        elements: Vec<Element>,
     },
 }
 
@@ -61,7 +61,7 @@ pub enum CheckerError {
 // Generics for wrapping fields, values, and coercing them
 #[derive(Display, Clone)]
 #[display("{field} @ {owner}")]
-pub struct Field<T: std::fmt::Display> {
+pub struct OwnedField<T: std::fmt::Display> {
     pub field: T,
     pub owner: T,
 }
@@ -115,9 +115,9 @@ pub struct CheckerState {
     wf_elements: HashMap<String, CheckedElement>,
     wf_signatures: HashMap<String, Signature>,
     wf_instances: HashMap<String, CheckedInstance>,
-    record_fields: HashMap<String, Field<Set>>,
-    variant_fields: HashMap<String, Field<Set>>,
-    signature_fields: HashMap<String, Field<Signature>>,
+    record_fields: HashMap<String, OwnedField<Set>>,
+    variant_fields: HashMap<String, OwnedField<Set>>,
+    signature_fields: HashMap<String, OwnedField<Signature>>,
     binder_element: Arc<AtomicUsize>,
     unique_name: Arc<AtomicUsize>,
 }
@@ -179,7 +179,7 @@ impl CheckerState {
     fn assert_correct_owner<T>(
         &self,
         name: &String,
-        field: &Field<T>,
+        field: &OwnedField<T>,
         belongs_to: &T,
     ) -> Result<(), CheckerError>
     where
@@ -225,7 +225,7 @@ impl CheckerState {
         };
         self.record_fields.insert(
             name.clone(),
-            Field {
+            OwnedField {
                 field: field_set.clone(),
                 owner: owner_set.clone(),
             },
@@ -245,7 +245,7 @@ impl CheckerState {
         };
         self.variant_fields.insert(
             name.clone(),
-            Field {
+            OwnedField {
                 field: field_set.clone(),
                 owner: owner_set.clone(),
             },
@@ -257,18 +257,18 @@ impl CheckerState {
     pub fn add_set(&mut self, name: String, set: SetValue) -> Result<(), CheckerError> {
         match &set {
             SetValue::Concrete(set @ Set::Record(fields)) => {
-                for RecordField {
+                for Field {
                     name: rfn,
-                    set: field_set,
+                    carries: field_set,
                 } in fields
                 {
                     self.add_record_field(rfn, field_set, set)?;
                 }
             }
             SetValue::Concrete(set @ Set::Variant(fields)) => {
-                for VariantField {
+                for Field {
                     name: vfn,
-                    set: field_set,
+                    carries: field_set,
                 } in fields
                 {
                     self.add_variant_field(vfn, field_set, set)?;
@@ -309,13 +309,13 @@ impl CheckerState {
             .map_or(Err(CheckerError::Unbound(name.clone())), Ok)
     }
 
-    pub fn lookup_record_field(&self, name: &String) -> Result<&Field<Set>, CheckerError> {
+    pub fn lookup_record_field(&self, name: &String) -> Result<&OwnedField<Set>, CheckerError> {
         self.record_fields
             .get(name)
             .map_or(Err(CheckerError::Unbound(name.clone())), Ok)
     }
 
-    pub fn lookup_variant_field(&self, name: &String) -> Result<&Field<Set>, CheckerError> {
+    pub fn lookup_variant_field(&self, name: &String) -> Result<&OwnedField<Set>, CheckerError> {
         self.variant_fields
             .get(name)
             .map_or(Err(CheckerError::Unbound(name.clone())), Ok)
@@ -354,7 +354,7 @@ impl CheckerState {
         };
         self.signature_fields.insert(
             name.clone(),
-            Field {
+            OwnedField {
                 field: field_signature.clone(),
                 owner: owner_signature.clone(),
             },
@@ -371,9 +371,9 @@ impl CheckerState {
     ) -> Result<(), CheckerError> {
         match &signature {
             Signature::Theory(fields) => {
-                for SigField {
+                for Field {
                     name: field_name,
-                    signature: field_sig,
+                    carries: field_sig,
                 } in fields
                 {
                     // TODO: are we supposed to recurse?
@@ -420,7 +420,10 @@ impl CheckerState {
             .map_or(Err(CheckerError::Unbound(name.clone())), Ok)
     }
 
-    pub fn lookup_signature_field(&self, name: &String) -> Result<&Field<Signature>, CheckerError> {
+    pub fn lookup_signature_field(
+        &self,
+        name: &String,
+    ) -> Result<&OwnedField<Signature>, CheckerError> {
         self.signature_fields
             .get(name)
             .map_or(Err(CheckerError::Unbound(name.clone())), Ok)
-- 
cgit v1.3.1