From 67e3285ae6c7b94adc1983dcff18a009455bc582 Mon Sep 17 00:00:00 2001 From: tslil Date: Tue, 28 Apr 2026 15:00:45 +0100 Subject: snapshot of working through instances/singatures <> sets/elements --- src/checker_state.rs | 112 ++++++++++++++++++++++++++++++++++++++++++--------- 1 file changed, 93 insertions(+), 19 deletions(-) (limited to 'src/checker_state.rs') 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, required: Vec, }, + #[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 { } #[derive(Display, Clone)] -pub enum Value { +pub enum Value { /// The storage format for concrete terms. Concrete(Term), - #[display("_ : {_0}")] + #[display("_")] /// The storage format for formal bindings. - Hypothetical(Type), + Hypothetical, } -pub type ElementValue = Value; -pub type InstanceValue = Value; +pub type ElementValue = Value; +pub type InstanceValue = Value; +pub type SetValue = Value; -impl From for Value { - fn from(e: Element) -> Value { +impl From for ElementValue { + fn from(e: Element) -> ElementValue { Value::Concrete(e) } } -impl From for Value { - fn from(i: Instance) -> Value { +impl From for InstanceValue { + fn from(i: Instance) -> InstanceValue { Value::Concrete(i) } } +impl From for SetValue { + fn from(s: Set) -> SetValue { + Value::Concrete(s) + } +} + #[derive(Display, Clone)] #[display("{value} : {container}")] pub struct Checked { - pub value: Value, + pub value: Value, pub container: Type, } @@ -84,13 +103,15 @@ pub type CheckedInstance = Checked; // The checker state #[derive(Default, Clone)] pub struct CheckerState { - wf_sets: HashMap, + wf_sets: HashMap, wf_elements: HashMap, wf_signatures: HashMap, wf_instances: HashMap, record_fields: HashMap>, variant_fields: HashMap>, signature_fields: HashMap>, + 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: 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, 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(()) + } } -- cgit v1.3.1