regression in WiP work to improve sets

4 files changed, 61 insertions, 29 deletions

diff --git a/src/checker.rs b/src/checker.rs
index 7b06c8b..24ba039 100644
--- a/src/checker.rs
+++ b/src/checker.rs
@@ -22,7 +22,7 @@ impl CheckerState {
                 Decl::Set { name, set } => {
                     self.assert_unbound_set(name)?;
                     let set = self.check_set(set)?;
-                    self.add_set(name.clone(), set)
+                    self.add_set(name.clone(), set, false)
                 }
 
                 Decl::Element { name, element, set } => {
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,
diff --git a/src/checker_signature.rs b/src/checker_signature.rs
index 55682a9..39a35b4 100644
--- a/src/checker_signature.rs
+++ b/src/checker_signature.rs
@@ -99,12 +99,6 @@ impl CheckerState {
                         name: name.clone(),
                         carries: signature,
                     });
-                    // 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_signature(&temp_name, Signature::Theory(new_fields.clone()), true)?;
                 }
                 Ok(Signature::Theory(new_fields))
@@ -112,11 +106,6 @@ impl CheckerState {
         }
     }
 
-    // the goal here is to spread the love: if we are adding a hypothetical of
-    // some signature _ : theory { ... } 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_instance(
         &mut self,
         name: String,
@@ -139,7 +128,7 @@ impl CheckerState {
         };
         // handle the special case canonical form for _ :: Set
         if signature == Signature::Set {
-            self.add_set(name.clone(), Set::ClaimedSet(self_instance.clone()))?;
+            self.add_set(name.clone(), Set::ClaimedSet(self_instance.clone()), false)?;
         }
         self.add_instance(name.clone(), value, signature.clone())?;
         if let Signature::Theory(fields) = signature {
@@ -267,6 +256,7 @@ impl CheckerState {
                                     ctx.add_set(
                                         f_n.clone(),
                                         Set::ClaimedSet(Instance::Var(f_n.clone())),
+                                        false,
                                     )?;
                                 }
 
diff --git a/src/checker_state.rs b/src/checker_state.rs
index 42f5089..c12a2d7 100644
--- a/src/checker_state.rs
+++ b/src/checker_state.rs
@@ -246,8 +246,9 @@ impl CheckerState {
         name: &String,
         field_set: &Set,
         owner_set: &Set,
+        rebind: bool,
     ) -> Result<(), CheckerError> {
-        if let Some(set_ref) = self.record_fields.get(name) {
+        if !rebind && let Some(set_ref) = self.record_fields.get(name) {
             self.assert_correct_owner(name, set_ref, owner_set)?;
         };
         self.record_fields.insert(
@@ -281,7 +282,7 @@ impl CheckerState {
     }
 
     #[instrument(skip(self), level = "debug", fields(%name, %set))]
-    pub fn add_set(&mut self, name: String, set: Set) -> Result<(), CheckerError> {
+    pub fn add_set(&mut self, name: String, set: Set, rebind: bool) -> Result<(), CheckerError> {
         match &set {
             Set::Record(fields) => {
                 for Field {
@@ -289,7 +290,7 @@ impl CheckerState {
                     carries: field_set,
                 } in fields
                 {
-                    self.add_record_field(rfn, field_set, &set)?;
+                    self.add_record_field(rfn, field_set, &set, rebind)?;
                 }
             }
             Set::Variant(fields) => {