aboutsummaryrefslogtreecommitdiff
path: root/src/checker_set.rs
diff options
context:
space:
mode:
Diffstat (limited to 'src/checker_set.rs')
-rw-r--r--src/checker_set.rs11
1 files changed, 7 insertions, 4 deletions
diff --git a/src/checker_set.rs b/src/checker_set.rs
index f0966f6..536a7ec 100644
--- a/src/checker_set.rs
+++ b/src/checker_set.rs
@@ -20,7 +20,7 @@ impl CheckerState {
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)?;
+ ctx.recursively_add_hypothetical_element(name.clone(), set.clone(), None)?;
new_fields.push(Field {
name: name.clone(),
carries: set,
@@ -76,7 +76,8 @@ impl CheckerState {
// 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(
+ #[instrument(skip(self), level = "debug", fields(%name, %set, head=%head.map(|s| s.to_string()).unwrap_or_default()) )]
+ fn recursively_add_hypothetical_element(
&mut self,
name: String,
set: Set,
@@ -99,7 +100,7 @@ impl CheckerState {
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))?;
+ self.recursively_add_hypothetical_element(f.name, f.carries, Some(&self_element))?;
}
}
Ok(())
@@ -308,9 +309,11 @@ impl CheckerState {
owner: owner_set,
} = self.lookup_record_field(&field)?;
+ let field_set = self.check_set(field_set)?;
+
// enforce the correct typing of the claimed result
if let Some(set) = set
- && !self.equal(set, field_set)
+ && !self.equal(set, &field_set)
{
return Err(CheckerError::WrongSetForElement {
value: element.clone().into(),