regression in WiP work to improve sets

1 files changed, 54 insertions, 13 deletions

diff --git a/src/checker_set.rs b/src/checker_set.rs
index 2f934e2..f0966f6 100644
--- a/src/checker_set.rs
+++ b/src/checker_set.rs
@@ -10,23 +10,30 @@ impl CheckerState {
         match set {
             Set::BuiltIn(_) => Ok(set.clone()),
             Set::Record(fields) => {
-                let mut ctx = self.clone();
                 let field_set = fields.iter().map(|f| &f.name).collect::<HashSet<&String>>();
                 if field_set.len() != fields.len() {
                     return Err(CheckerError::DuplicateFieldsSet(set.clone()));
                 }
-                let fields = fields
-                    .into_iter()
-                    .map(|Field { name, carries }| {
-                        let set = ctx.check_set(carries)?;
-                        ctx.add_element(name.clone(), ElementValue::Hypothetical, set.clone())?;
-                        Ok(Field {
-                            name: name.clone(),
-                            carries: set,
-                        })
-                    })
-                    .collect::<Result<Vec<_>, _>>()?;
-                Ok(Set::Record(fields))
+
+                let mut ctx = self.clone();
+                let temp_name = ctx.make_unique_name();
+                let mut new_fields = Vec::new();
+                for Field { name, carries } in fields {
+                    let set = ctx.check_set(carries)?;
+                    ctx._recursively_add_hypothetical_element(name.clone(), set.clone(), None)?;
+                    new_fields.push(Field {
+                        name: name.clone(),
+                        carries: set,
+                    });
+                    // We must iteratively add the entire signature so that
+                    // field lookup does something, as we rely on that for type
+                    // checking. We could hack together a signature i suppose,
+                    // but the cleanest thing is to add the truncations of this
+                    // signature. In any event the context is discarded
+                    // afterward.
+                    ctx.add_set(temp_name.clone(), Set::Record(new_fields.clone()), true)?;
+                }
+                Ok(Set::Record(new_fields))
             }
             Set::Variant(fields) => {
                 let field_set = fields.iter().map(|f| &f.name).collect::<HashSet<&String>>();
@@ -64,6 +71,40 @@ impl CheckerState {
         }
     }
 
+    // the goal here is to spread the love: if we are adding a hypothetical of
+    // some set _ : record { ... } then we must recurse into all of those
+    // fields and add hypotheticals for them---but, we need to build the tree as
+    // we go, giving them the concrete value of their path from the root (our
+    // canonical form).
+    fn _recursively_add_hypothetical_element(
+        &mut self,
+        name: String,
+        set: Set,
+        head: Option<&Element>,
+    ) -> Result<(), CheckerError> {
+        let value = match head {
+            Some(h) => ElementValue::Concrete(Element::Project {
+                element: Box::new(h.clone()),
+                field: name.clone(),
+            }),
+            None => ElementValue::Hypothetical,
+        };
+        let self_element = match head {
+            Some(h) => Element::Project {
+                element: Box::new(h.clone()),
+                field: name.clone(),
+            },
+            None => Element::Var(name.clone()),
+        };
+        self.add_element(name.clone(), value, set.clone())?;
+        if let Set::Record(fields) = set {
+            for f in fields {
+                self._recursively_add_hypothetical_element(f.name, f.carries, Some(&self_element))?;
+            }
+        }
+        Ok(())
+    }
+
     fn _check_literal_set_helper(
         &self,
         value: Element,