add distinction between hypothetical and concrete elements to the set checker, it now enforces that all arms in case are well typed!

1 files changed, 23 insertions, 5 deletions

diff --git a/src/checker_state.rs b/src/checker_state.rs
index 30f83be..7590457 100644
--- a/src/checker_state.rs
+++ b/src/checker_state.rs
@@ -41,9 +41,22 @@ pub struct SetField {
 }
 
 #[derive(Display, Clone)]
-#[display("{element} : {set}")]
+pub enum ElementValue {
+    Concrete(Element),
+    #[display("_ : {_0}")]
+    Hypothetical(Set),
+}
+
+impl From<Element> for ElementValue {
+    fn from(e: Element) -> ElementValue {
+        ElementValue::Concrete(e)
+    }
+}
+
+#[derive(Display, Clone)]
+#[display("{value} : {set}")]
 pub struct CheckedElement {
-    pub element: Element,
+    pub value: ElementValue,
     pub set: Set,
 }
 
@@ -198,12 +211,17 @@ impl CheckerState {
     pub fn add_element(
         &mut self,
         name: String,
-        element: Element,
+        element: ElementValue,
         set: Set,
     ) -> Result<(), CheckerError> {
         self.assert_unbound_element(&name)?;
-        self.wf_elements
-            .insert(name, CheckedElement { element, set });
+        self.wf_elements.insert(
+            name,
+            CheckedElement {
+                value: element,
+                set,
+            },
+        );
         Ok(())
     }