diff options
Diffstat (limited to 'src/checker_state.rs')
| -rw-r--r-- | src/checker_state.rs | 112 |
1 files changed, 93 insertions, 19 deletions
diff --git a/src/checker_state.rs b/src/checker_state.rs index 73edd10..dc76a10 100644 --- a/src/checker_state.rs +++ b/src/checker_state.rs @@ -35,6 +35,18 @@ pub enum CheckerError { found: Vec<String>, required: Vec<String>, }, + #[display("Instance {value} claimed to belong to {claimed} but actually belongs to {real}")] + WrongSignatureForInstance { + value: InstanceValue, + claimed: Signature, + real: Signature, + }, + #[display("Instance {instance} does belong to set {claimed}: {reason}")] + InstanceDoesNotBelong { + instance: Instance, + claimed: Signature, + reason: String, + }, } // ----------------------------------------------------------------------------- @@ -47,33 +59,40 @@ pub struct Field<T: std::fmt::Display> { } #[derive(Display, Clone)] -pub enum Value<Term: std::fmt::Display, Type: std::fmt::Display> { +pub enum Value<Term: std::fmt::Display> { /// The storage format for concrete terms. Concrete(Term), - #[display("_ : {_0}")] + #[display("_")] /// The storage format for formal bindings. - Hypothetical(Type), + Hypothetical, } -pub type ElementValue = Value<Element, Set>; -pub type InstanceValue = Value<Instance, Signature>; +pub type ElementValue = Value<Element>; +pub type InstanceValue = Value<Instance>; +pub type SetValue = Value<Set>; -impl From<Element> for Value<Element, Set> { - fn from(e: Element) -> Value<Element, Set> { +impl From<Element> for ElementValue { + fn from(e: Element) -> ElementValue { Value::Concrete(e) } } -impl From<Instance> for Value<Instance, Signature> { - fn from(i: Instance) -> Value<Instance, Signature> { +impl From<Instance> for InstanceValue { + fn from(i: Instance) -> InstanceValue { Value::Concrete(i) } } +impl From<Set> for SetValue { + fn from(s: Set) -> SetValue { + Value::Concrete(s) + } +} + #[derive(Display, Clone)] #[display("{value} : {container}")] pub struct Checked<Term: std::fmt::Display, Type: std::fmt::Display> { - pub value: Value<Term, Type>, + pub value: Value<Term>, pub container: Type, } @@ -84,13 +103,15 @@ pub type CheckedInstance = Checked<Instance, Signature>; // The checker state #[derive(Default, Clone)] pub struct CheckerState { - wf_sets: HashMap<String, Set>, + wf_sets: HashMap<String, SetValue>, wf_elements: HashMap<String, CheckedElement>, wf_signatures: HashMap<String, Signature>, wf_instances: HashMap<String, CheckedInstance>, record_fields: HashMap<String, Field<Set>>, variant_fields: HashMap<String, Field<Set>>, signature_fields: HashMap<String, Field<Signature>>, + binder_element: usize, + binder_instance: usize, } impl fmt::Display for CheckerState { @@ -224,29 +245,29 @@ 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: SetValue) -> Result<(), CheckerError> { match &set { - Set::Record(fields) => { + SetValue::Concrete(set @ Set::Record(fields)) => { for RecordField { name: rfn, set: field_set, } in fields { - self.add_record_field(rfn, field_set, &set)?; + self.add_record_field(rfn, field_set, set)?; } } - Set::Variant(fields) => { + SetValue::Concrete(set @ Set::Variant(fields)) => { for VariantField { name: vfn, set: field_set, } in fields { - self.add_variant_field(vfn, field_set, &set)?; + self.add_variant_field(vfn, field_set, set)?; } } _ => (), }; - self.wf_sets.insert(name.clone(), set); + self.wf_sets.insert(name, set.into()); Ok(()) } @@ -254,7 +275,7 @@ impl CheckerState { pub fn add_element( &mut self, name: String, - element: Value<Element, Set>, + element: ElementValue, set: Set, ) -> Result<(), CheckerError> { self.wf_elements.insert( @@ -267,7 +288,7 @@ impl CheckerState { Ok(()) } - pub fn lookup_set(&self, name: &String) -> Result<&Set, CheckerError> { + pub fn lookup_set(&self, name: &String) -> Result<&SetValue, CheckerError> { self.wf_sets .get(name) .map_or(Err(CheckerError::Unbound(name.clone())), Ok) @@ -378,4 +399,57 @@ impl CheckerState { .get(name) .map_or(Err(CheckerError::Unbound(name.clone())), Ok) } + + pub fn lookup_instance(&self, name: &String) -> Result<&CheckedInstance, CheckerError> { + self.wf_instances + .get(name) + .map_or(Err(CheckerError::Unbound(name.clone())), Ok) + } + + pub fn lookup_signature_field(&self, name: &String) -> Result<&Field<Signature>, CheckerError> { + self.signature_fields + .get(name) + .map_or(Err(CheckerError::Unbound(name.clone())), Ok) + } +} + +// ----------------------------------------------------------------------------- +// Bindings +impl CheckerState { + #[instrument(skip(self), level = "debug", fields(%name, %set))] + pub fn make_element_binding(&mut self, name: String, set: Set) -> Result<(), CheckerError> { + let canonical = format!("db_e_{}", self.binder_element); + self.add_element(canonical.clone(), ElementValue::Hypothetical, set.clone())?; + self.add_element(name, Element::Var(canonical).into(), set)?; + self.binder_element += 1; + Ok(()) + } + + #[instrument(skip(self), level = "debug", fields(%name, %signature))] + pub fn make_instance_binding( + &mut self, + name: String, + signature: Signature, + ) -> Result<(), CheckerError> { + let canonical = format!("db_i_{}", self.binder_instance); + self.add_instance( + canonical.clone(), + InstanceValue::Hypothetical, + signature.clone(), + )?; + self.add_instance( + name.clone(), + Instance::Var(canonical.clone()).into(), + signature.clone(), + )?; + // And lo, the special case: + // TODO: is this correct in the presence of de bruijn? + if signature == Signature::Set { + self.add_set(canonical.clone(), SetValue::Hypothetical)?; + self.add_set(name, Set::Var(canonical).into())?; + } + + self.binder_instance += 1; + Ok(()) + } } |