diff options
| -rw-r--r-- | src/checker.rs | 2 | ||||
| -rw-r--r-- | src/checker_set.rs | 67 | ||||
| -rw-r--r-- | src/checker_signature.rs | 14 | ||||
| -rw-r--r-- | src/checker_state.rs | 7 |
4 files changed, 61 insertions, 29 deletions
diff --git a/src/checker.rs b/src/checker.rs index 7b06c8b..24ba039 100644 --- a/src/checker.rs +++ b/src/checker.rs @@ -22,7 +22,7 @@ impl CheckerState { Decl::Set { name, set } => { self.assert_unbound_set(name)?; let set = self.check_set(set)?; - self.add_set(name.clone(), set) + self.add_set(name.clone(), set, false) } Decl::Element { name, element, set } => { diff --git a/src/checker_set.rs b/src/checker_set.rs index 2f934e2..f0966f6 100644 --- a/src/checker_set.rs +++ b/src/checker_set.rs @@ -10,23 +10,30 @@ impl CheckerState { match set { Set::BuiltIn(_) => Ok(set.clone()), Set::Record(fields) => { - let mut ctx = self.clone(); 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 }| { - let set = ctx.check_set(carries)?; - ctx.add_element(name.clone(), ElementValue::Hypothetical, set.clone())?; - Ok(Field { - name: name.clone(), - carries: set, - }) - }) - .collect::<Result<Vec<_>, _>>()?; - Ok(Set::Record(fields)) + + let mut ctx = self.clone(); + let temp_name = ctx.make_unique_name(); + 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)?; + new_fields.push(Field { + name: name.clone(), + carries: set, + }); + // We must iteratively add the entire signature so that + // field lookup does something, as we rely on that for type + // checking. We could hack together a signature i suppose, + // but the cleanest thing is to add the truncations of this + // signature. In any event the context is discarded + // afterward. + ctx.add_set(temp_name.clone(), Set::Record(new_fields.clone()), true)?; + } + Ok(Set::Record(new_fields)) } Set::Variant(fields) => { let field_set = fields.iter().map(|f| &f.name).collect::<HashSet<&String>>(); @@ -64,6 +71,40 @@ impl CheckerState { } } + // the goal here is to spread the love: if we are adding a hypothetical of + // some set _ : record { ... } then we must recurse into all of those + // 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( + &mut self, + name: String, + set: Set, + head: Option<&Element>, + ) -> Result<(), CheckerError> { + let value = match head { + Some(h) => ElementValue::Concrete(Element::Project { + element: Box::new(h.clone()), + field: name.clone(), + }), + None => ElementValue::Hypothetical, + }; + let self_element = match head { + Some(h) => Element::Project { + element: Box::new(h.clone()), + field: name.clone(), + }, + None => Element::Var(name.clone()), + }; + 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))?; + } + } + Ok(()) + } + fn _check_literal_set_helper( &self, value: Element, diff --git a/src/checker_signature.rs b/src/checker_signature.rs index 55682a9..39a35b4 100644 --- a/src/checker_signature.rs +++ b/src/checker_signature.rs @@ -99,12 +99,6 @@ impl CheckerState { name: name.clone(), carries: signature, }); - // We must iteratively add the entire signature so that - // field lookup does something, as we rely on that for type - // checking. We could hack together a signature i suppose, - // but the cleanest thing is to add the truncations of this - // signature. In any event the context is discarded - // afterward. ctx.add_signature(&temp_name, Signature::Theory(new_fields.clone()), true)?; } Ok(Signature::Theory(new_fields)) @@ -112,11 +106,6 @@ impl CheckerState { } } - // the goal here is to spread the love: if we are adding a hypothetical of - // some signature _ : theory { ... } then we must recurse into all of those - // 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_instance( &mut self, name: String, @@ -139,7 +128,7 @@ impl CheckerState { }; // handle the special case canonical form for _ :: Set if signature == Signature::Set { - self.add_set(name.clone(), Set::ClaimedSet(self_instance.clone()))?; + self.add_set(name.clone(), Set::ClaimedSet(self_instance.clone()), false)?; } self.add_instance(name.clone(), value, signature.clone())?; if let Signature::Theory(fields) = signature { @@ -267,6 +256,7 @@ impl CheckerState { ctx.add_set( f_n.clone(), Set::ClaimedSet(Instance::Var(f_n.clone())), + false, )?; } diff --git a/src/checker_state.rs b/src/checker_state.rs index 42f5089..c12a2d7 100644 --- a/src/checker_state.rs +++ b/src/checker_state.rs @@ -246,8 +246,9 @@ impl CheckerState { name: &String, field_set: &Set, owner_set: &Set, + rebind: bool, ) -> Result<(), CheckerError> { - if let Some(set_ref) = self.record_fields.get(name) { + if !rebind && let Some(set_ref) = self.record_fields.get(name) { self.assert_correct_owner(name, set_ref, owner_set)?; }; self.record_fields.insert( @@ -281,7 +282,7 @@ impl CheckerState { } #[instrument(skip(self), level = "debug", fields(%name, %set))] - pub fn add_set(&mut self, name: String, set: Set) -> Result<(), CheckerError> { + pub fn add_set(&mut self, name: String, set: Set, rebind: bool) -> Result<(), CheckerError> { match &set { Set::Record(fields) => { for Field { @@ -289,7 +290,7 @@ impl CheckerState { carries: field_set, } in fields { - self.add_record_field(rfn, field_set, &set)?; + self.add_record_field(rfn, field_set, &set, rebind)?; } } Set::Variant(fields) => { |