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.rs167
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(),
generated by cgit v1.3.1 (git 2.54.0) at 2026-08-30 19:05:04 +0000