finish the implementation, we don't have motives so this is how it will have to stay

1 files changed, 114 insertions, 53 deletions

diff --git a/src/checker_set.rs b/src/checker_set.rs
index 83d97a1..f13f686 100644
--- a/src/checker_set.rs
+++ b/src/checker_set.rs
@@ -13,7 +13,7 @@ impl CheckerState {
                 let mut ctx = self.clone();
                 let field_set = fields.iter().map(|f| &f.name).collect::<HashSet<&String>>();
                 if field_set.len() != fields.len() {
-                    todo!("duplicate fields");
+                    return Err(CheckerError::DuplicateFieldsSet(set.clone()));
                 }
                 let fields = fields
                     .into_iter()
@@ -29,6 +29,11 @@ impl CheckerState {
                 Ok(Set::Record(fields))
             }
             Set::Variant(fields) => {
+                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 }| {
@@ -76,43 +81,59 @@ impl CheckerState {
         }
     }
 
-    #[instrument(skip(self), level = "debug", fields(%element, %set))]
-    pub fn check_element(&self, element: &Element, set: &Set) -> Result<Element, CheckerError> {
+    #[instrument(skip(self), level = "debug", fields(%element, set=%set.map(|s| s.to_string()).unwrap_or_default()))]
+    pub fn check_element(
+        &self,
+        element: &Element,
+        set: Option<&Set>,
+    ) -> Result<Element, CheckerError> {
         match element {
             Element::Literal(lit) => {
                 let value = element.clone();
                 // we may infer the type from the element
-                match lit {
-                    Literal::Int(_) => {
-                        self._check_literal_set_helper(value, set, Set::BuiltIn(BuiltIn::Int))?;
-                    }
-                    Literal::Nat(_) => {
-                        self._check_literal_set_helper(value, set, Set::BuiltIn(BuiltIn::Nat))?;
-                    }
-                    Literal::Str(_) => {
-                        self._check_literal_set_helper(value, set, Set::BuiltIn(BuiltIn::Str))?;
-                    }
-                    Literal::Bool(_) => {
-                        self._check_literal_set_helper(value, set, Set::BuiltIn(BuiltIn::Bool))?;
-                    }
-                    Literal::Float(_) => {
-                        self._check_literal_set_helper(value, set, Set::BuiltIn(BuiltIn::Float))?;
+                if let Some(set) = set {
+                    match lit {
+                        Literal::Int(_) => {
+                            self._check_literal_set_helper(value, set, Set::BuiltIn(BuiltIn::Int))?;
+                        }
+                        Literal::Nat(_) => {
+                            self._check_literal_set_helper(value, set, Set::BuiltIn(BuiltIn::Nat))?;
+                        }
+                        Literal::Str(_) => {
+                            self._check_literal_set_helper(value, set, Set::BuiltIn(BuiltIn::Str))?;
+                        }
+                        Literal::Bool(_) => {
+                            self._check_literal_set_helper(
+                                value,
+                                set,
+                                Set::BuiltIn(BuiltIn::Bool),
+                            )?;
+                        }
+                        Literal::Float(_) => {
+                            self._check_literal_set_helper(
+                                value,
+                                set,
+                                Set::BuiltIn(BuiltIn::Float),
+                            )?;
+                        }
                     }
                 }
                 Ok(element.clone().into())
             }
             Element::Var(v) => {
                 let lookup = self.lookup_element(&v)?;
-                let container = self.check_set(&lookup.container)?; // TODO: necessary why?
 
-                // we have previously done the work to discover the type of
-                // this element, so what we're claiming now must match!
-                if !self.equal(set, &container) {
-                    return Err(CheckerError::WrongSetForElement {
-                        value: element.clone().into(),
-                        claimed: set.clone(),
-                        real: container,
-                    });
+                if let Some(set) = set {
+                    let container = self.check_set(&lookup.container)?;
+                    // we have previously done the work to discover the type of
+                    // this element, so what we're claiming now must match!
+                    if !self.equal(set, &container) {
+                        return Err(CheckerError::WrongSetForElement {
+                            value: element.clone().into(),
+                            claimed: set.clone(),
+                            real: container,
+                        });
+                    }
                 }
                 // If we found a formal binding, we have no value to report.
                 // This is the ONLY source of Var as a return value for
@@ -125,21 +146,53 @@ impl CheckerState {
                 }
             }
             Element::Record(assignations) => {
-                let rej = |reason| CheckerError::ElementDoesNotBelong {
-                    element: element.clone(),
-                    claimed: set.clone(),
-                    reason,
+                // there's a very short path here for constructing {} : record {}
+                if assignations.is_empty() {
+                    let element = Element::Record(Vec::new());
+                    if let Some(set) = set {
+                        if !self.equal(set, &Set::Record(Vec::new())) {
+                            return Err(CheckerError::ElementDoesNotBelong {
+                                element,
+                                claimed: set.clone(),
+                                reason: "the set is not the empty record".to_string(),
+                            });
+                        };
+                    };
+                    return Ok(element);
+                }
+                // from here on assignations is non-empty
+
+                // look up the owner for each tag
+                let owners = assignations
+                    .iter()
+                    .map(|ea| self.lookup_record_field(&ea.name).map(|x| &x.owner))
+                    .collect::<Result<Vec<_>, _>>()?;
+
+                // make sure they're all the same
+                let owner = owners[0];
+                if !owners[1..].into_iter().all(|x| self.equal(*x, owner)) {
+                    return Err(CheckerError::ElementInconsistentFieldChoice(
+                        element.clone(),
+                    ));
                 };
 
-                // make sure we are filling a record
-                let fields = if let Set::Record(fields) = set {
-                    Ok(fields)
-                } else {
-                    Err(rej("element is a record instance".to_string()))
-                }?;
+                // if in addition we know the set, make sure it agrees
+                if let Some(set) = set
+                    && !self.equal(set, owner)
+                {
+                    return Err(CheckerError::WrongSetForElement {
+                        value: element.clone().into(),
+                        claimed: set.clone(),
+                        real: owner.clone(),
+                    });
+                }
+
+                let Set::Record(fields) = owner else {
+                    panic!("invariant violation: looking up field owners did not retrieve a record")
+                };
 
                 let mut set_fnames_sorted: Vec<String> =
-                    fields.iter().map(|x| x.name.clone()).collect();
+                    fields.iter().map(|f| f.name.clone()).collect();
                 set_fnames_sorted.sort();
 
                 let mut element_fnames_sorted: Vec<String> =
@@ -148,11 +201,15 @@ impl CheckerState {
 
                 // make sure that we are correctly filling the record
                 if set_fnames_sorted != element_fnames_sorted {
-                    return Err(rej(format!(
-                        "expected [{}] but found [{}]",
-                        set_fnames_sorted.join(", "),
-                        element_fnames_sorted.join(", "),
-                    )));
+                    return Err(CheckerError::ElementDoesNotBelong {
+                        element: element.clone(),
+                        claimed: owner.clone(),
+                        reason: format!(
+                            "expected [{}] but found [{}]",
+                            set_fnames_sorted.join(", "),
+                            element_fnames_sorted.join(", "),
+                        ),
+                    });
                 }
 
                 let assignations = assignations
@@ -176,7 +233,7 @@ impl CheckerState {
                                 .expect("we have already checked that all fields are present");
 
                             let f_s = ctx.check_set(f_s)?;
-                            let f_e = ctx.check_element(f_e, &f_s)?;
+                            let f_e = ctx.check_element(f_e, Some(&f_s))?;
                             ctx.add_element(f_n.clone(), f_e.clone().into(), f_s)?;
 
                             Ok(ElemAssign {
@@ -200,7 +257,9 @@ impl CheckerState {
                 } = self.lookup_record_field(&field)?;
 
                 // enforce the correct typing of the claimed result
-                if !self.equal(set, field_set) {
+                if let Some(set) = set
+                    && !self.equal(set, field_set)
+                {
                     return Err(CheckerError::WrongSetForElement {
                         value: element.clone().into(),
                         claimed: set.clone(),
@@ -209,7 +268,7 @@ impl CheckerState {
                 }
 
                 // enforce the correct typing of the element
-                let inner = self.check_element(inner, owner_set)?;
+                let inner = self.check_element(inner, Some(owner_set))?;
 
                 // Unfortunately we still have to do something nasty here to
                 // obtain the data
@@ -250,7 +309,9 @@ impl CheckerState {
                 } = self.lookup_variant_field(&field)?;
 
                 // enforce the correct typing of the claimed result
-                if !self.equal(set, owner_set) {
+                if let Some(set) = set
+                    && !self.equal(set, owner_set)
+                {
                     return Err(CheckerError::WrongSetForElement {
                         value: element.clone().into(),
                         claimed: set.clone(),
@@ -259,7 +320,7 @@ impl CheckerState {
                 }
 
                 // enforce the correct typing of the element
-                let element = self.check_element(inner, field_set)?;
+                let element = self.check_element(inner, Some(field_set))?;
                 Ok(Element::Inject {
                     element: Box::new(element),
                     field: field.clone(),
@@ -311,7 +372,7 @@ impl CheckerState {
                 // scrutinee must be of the same set that all the arms are
                 // implying, in particular this implies that the following holds
                 // `inner : self.lookup_variant_field(field).field_set`
-                let scrutinee = self.check_element(scrutinee, owner)?;
+                let scrutinee = self.check_element(scrutinee, Some(owner))?;
 
                 // which variant are we, if any
                 let matching: Option<(String, Element)> = match scrutinee {
@@ -359,9 +420,9 @@ impl CheckerState {
                     {
                         let canonical =
                             ctx.make_element_definition(binding_name, inner.clone(), binding_set)?;
-                        let this_set = ctx.check_set(set)?;
+                        let this_set = set.map(|set| ctx.check_set(set)).transpose()?;
 
-                        let output = ctx.check_element((&arm.body).into(), &this_set)?;
+                        let output = ctx.check_element((&arm.body).into(), this_set.as_ref())?;
                         if matches!(computed_output, Some(_)) {
                             panic!(
                                 "invariant violation: we somehow matched multiple arms in case analysis"
@@ -386,8 +447,8 @@ impl CheckerState {
                                 owner.clone(),
                             )?;
                         };
-                        let this_set = ctx.check_set(set)?;
-                        let body = ctx.check_element((&arm.body).into(), &this_set)?;
+                        let this_set = set.map(|set| ctx.check_set(set)).transpose()?;
+                        let body = ctx.check_element((&arm.body).into(), this_set.as_ref())?;
 
                         CaseArm {
                             tag: arm.tag.clone(),