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.rs68
1 files changed, 44 insertions, 24 deletions
diff --git a/src/checker_set.rs b/src/checker_set.rs
index 10f9b28..c3d1b3a 100644
--- a/src/checker_set.rs
+++ b/src/checker_set.rs
@@ -1,6 +1,7 @@
use crate::ast::*;
use crate::checker_state::*;
+use std::collections::HashMap;
use std::iter::zip;
use tracing::instrument;
@@ -39,7 +40,11 @@ impl CheckerState {
}
Set::ClaimedSet(instance) => {
let instance = self.check_instance(instance, Some(&Signature::Set))?;
- Ok(Set::ClaimedSet(instance))
+ if let Instance::SetCoerce(set) = instance {
+ Ok(*set)
+ } else {
+ Ok(Set::ClaimedSet(instance))
+ }
}
Set::Var(v) => {
let deref = self.lookup_set(&v)?;
@@ -128,40 +133,55 @@ impl CheckerState {
Err(rej("element is a record instance".to_string()))
}?;
- let (set_fnames, set_fsets): (Vec<String>, Vec<Set>) = fields
- .iter()
- .map(|RecordField { name, set }| (name.clone(), set.clone()))
- .unzip();
- let mut set_fnames_sorted = set_fnames.clone();
+ let mut set_fnames_sorted: Vec<String> =
+ fields.iter().map(|x| x.name.clone()).collect();
set_fnames_sorted.sort();
- let (element_fnames, element_felements): (Vec<String>, Vec<&Element>) =
- assignations
- .iter()
- .map(|ElemAssign { name, element }| (name.clone(), element))
- .unzip();
-
- let mut element_fnames_sorted = element_fnames.clone();
+ let mut element_fnames_sorted: Vec<String> =
+ assignations.iter().map(|x| x.name.clone()).collect();
element_fnames_sorted.sort();
+ // 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.join(", "),
- element_fnames.join(", "),
+ set_fnames_sorted.join(", "),
+ element_fnames_sorted.join(", "),
)));
}
- // recurse, sets have already been completely expanded
- let sub_els = zip(element_felements, set_fsets)
- .map(|(e_f, e_s)| self.check_element(e_f.into(), &e_s))
+ let assignations = assignations
+ .into_iter()
+ .map(|x| (&x.name, &x.element))
+ .collect::<HashMap<_, _>>();
+
+ let mut ctx = self.clone();
+ // the basic pattern here is that we use ctx.check_* to perform
+ // substitutions for us, as we steadily march through the users
+ // definitions
+ let sub_elements = fields
+ .iter()
+ .map(
+ |RecordField {
+ name: f_n,
+ set: f_s,
+ }| {
+ let f_e = assignations
+ .get(f_n)
+ .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)?;
+ ctx.add_element(f_n.clone(), f_e.clone().into(), f_s)?;
+
+ Ok(ElemAssign {
+ name: f_n.clone(),
+ element: f_e,
+ })
+ },
+ )
.collect::<Result<Vec<_>, _>>()?;
- // rebuild
- let assignations = zip(element_fnames, sub_els)
- .map(|(name, element)| ElemAssign { name, element })
- .collect();
- // resign?
- Ok(Element::Record(assignations))
+ Ok(Element::Record(sub_elements))
}
Element::Project {
element: inner,