prepare for more work on signatures, in particular this means processing records in telescoped contexts

rework ElementValue, CheckedElement to be type aliases for the generic version over Term : Type

1 files changed, 27 insertions, 21 deletions

diff --git a/src/checker_set.rs b/src/checker_set.rs
index 2faca9e..7ff6e4a 100644
--- a/src/checker_set.rs
+++ b/src/checker_set.rs
@@ -10,10 +10,16 @@ impl CheckerState {
         match set {
             Set::BuiltIn(_) => Ok(set.clone()),
             Set::Record(fields) => {
+                let mut ctx = self.clone();
                 let fields = fields
                     .into_iter()
                     .map(|RecordField { name, set }| {
-                        let set = self.check_set(set)?;
+                        let set = ctx.check_set(set)?;
+                        ctx.add_element(
+                            name.clone(),
+                            Value::Hypothetical(set.clone()),
+                            set.clone(),
+                        )?;
                         Ok(RecordField { name, set })
                     })
                     .collect::<Result<Vec<_>, _>>()?;
@@ -68,7 +74,7 @@ impl CheckerState {
             // hypothetical from a call to check_element, in the context of
             // check_element, we can safely ignore its payload. I'll point this
             // out later as (*)
-            ElementValue::Hypothetical(ref h_set) => {
+            Value::Hypothetical(ref h_set) => {
                 if !self.equal(set, &h_set) {
                     Err(CheckerError::WrongSetForElement {
                         value: value.clone(),
@@ -79,7 +85,7 @@ impl CheckerState {
                     Ok(value)
                 }
             }
-            ElementValue::Concrete(ref element @ Element::Literal(ref lit)) => {
+            Value::Concrete(ref element @ Element::Literal(ref lit)) => {
                 let value = value.clone();
                 // we may infer the type from the element
                 match lit {
@@ -101,20 +107,20 @@ impl CheckerState {
                 }
                 Ok(element.clone().into())
             }
-            ElementValue::Concrete(Element::Var(ref v)) => {
+            Value::Concrete(Element::Var(ref v)) => {
                 let lookup = self.lookup_element(&v)?;
                 // 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, &lookup.set) {
+                if !self.equal(set, &lookup.container) {
                     return Err(CheckerError::WrongSetForElement {
                         value: value.clone(),
                         claimed: set.clone(),
-                        real: lookup.set.clone(),
+                        real: lookup.container.clone(),
                     });
                 }
                 Ok(lookup.value.clone())
             }
-            ElementValue::Concrete(ref concrete @ Element::Record(ref assignations)) => {
+            Value::Concrete(ref concrete @ Element::Record(ref assignations)) => {
                 let rej = |reason| CheckerError::ElementDoesNotBelong {
                     element: concrete.clone(),
                     claimed: set.clone(),
@@ -159,18 +165,18 @@ impl CheckerState {
                 // rebuild, hypotheticals are contagious
                 let assignations = zip(element_fnames, sub_els)
                     .map(|(name, element)| match element {
-                        ElementValue::Concrete(element) => Some(ElemAssign { name, element }),
-                        ElementValue::Hypothetical(_) => None,
+                        Value::Concrete(element) => Some(ElemAssign { name, element }),
+                        Value::Hypothetical(_) => None,
                     })
                     .collect();
                 // resign?
                 Ok(if let Some(assignations) = assignations {
                     Element::Record(assignations).into()
                 } else {
-                    ElementValue::Hypothetical(set.clone())
+                    Value::Hypothetical(set.clone())
                 })
             }
-            ElementValue::Concrete(Element::Project {
+            Value::Concrete(Element::Project {
                 element: ref inner,
                 ref field,
             }) => {
@@ -193,7 +199,7 @@ impl CheckerState {
                 // enforce the correct typing of the element
                 let inner = self.check_element((*inner.clone()).into(), owner_set)?;
                 match inner {
-                    ElementValue::Concrete(inner) => {
+                    Value::Concrete(inner) => {
                         // Unfortunately we still have to do something nasty here to obtain the data
                         let Element::Record(assignations) = inner else {
                             panic!(
@@ -212,10 +218,10 @@ impl CheckerState {
                         Ok(sub_element.into())
                     }
                     // correct by (*)
-                    ElementValue::Hypothetical(_) => Ok(ElementValue::Hypothetical(set.clone())),
+                    Value::Hypothetical(_) => Ok(Value::Hypothetical(set.clone())),
                 }
             }
-            ElementValue::Concrete(Element::Inject {
+            Value::Concrete(Element::Inject {
                 element: ref inner,
                 ref field,
             }) => {
@@ -240,16 +246,16 @@ impl CheckerState {
                 let element = self.check_element((*inner.clone()).into(), field_set)?;
 
                 match element {
-                    ElementValue::Concrete(element) => Ok(Element::Inject {
+                    Value::Concrete(element) => Ok(Element::Inject {
                         element: Box::new(element),
                         field: field.clone(),
                     }
                     .into()),
                     // correct by (*)
-                    ElementValue::Hypothetical(_) => Ok(ElementValue::Hypothetical(set.clone())),
+                    Value::Hypothetical(_) => Ok(Value::Hypothetical(set.clone())),
                 }
             }
-            ElementValue::Concrete(
+            Value::Concrete(
                 ref element @ Element::Case {
                     ref arms,
                     ref scrutinee,
@@ -303,8 +309,8 @@ impl CheckerState {
 
                 // which variant are we, if any
                 let matching: Option<(String, Element)> = match scrutinee {
-                    ElementValue::Hypothetical(_) => None,
-                    ElementValue::Concrete(Element::Inject {
+                    Value::Hypothetical(_) => None,
+                    Value::Concrete(Element::Inject {
                         field,
                         element: inner,
                     }) => Some((field, *inner)),
@@ -348,13 +354,13 @@ impl CheckerState {
                     } else {
                         new_context.add_element(
                             binding_name,
-                            ElementValue::Hypothetical(field_set.clone()),
+                            Value::Hypothetical(field_set.clone()),
                             binding_set,
                         )?;
                         new_context.check_element(arm.body.clone().into(), set)?;
                     };
                 }
-                Ok(computed_output.unwrap_or(ElementValue::Hypothetical(set.clone())))
+                Ok(computed_output.unwrap_or(Value::Hypothetical(set.clone())))
             }
         }
     }