diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/checker.rs | 4 | ||||
| -rw-r--r-- | src/checker_set.rs | 40 | ||||
| -rw-r--r-- | src/checker_signature.rs | 170 | ||||
| -rw-r--r-- | src/checker_state.rs | 50 | ||||
| -rw-r--r-- | src/main.rs | 28 | ||||
| -rw-r--r-- | src/parser.rs | 2 |
6 files changed, 191 insertions, 103 deletions
diff --git a/src/checker.rs b/src/checker.rs index dc3dc3c..f3c5205 100644 --- a/src/checker.rs +++ b/src/checker.rs @@ -33,7 +33,7 @@ impl CheckerState { Decl::Signature { name, signature } => { self.assert_unbound_signature(name)?; let signature = self.check_signature(signature.clone())?; - self.add_signature(name, signature) + self.add_signature(name, signature, false) } Decl::Instance { name, @@ -42,7 +42,7 @@ impl CheckerState { } => { self.assert_unbound_instance(name)?; let signature = self.check_signature(signature.clone())?; - let instance = self.check_instance(instance.clone(), &signature)?; + let instance = self.check_instance(instance.clone(), (&signature).into())?; self.add_instance(name.clone(), instance.into(), signature) } }?; diff --git a/src/checker_set.rs b/src/checker_set.rs index 86661c7..2bd011d 100644 --- a/src/checker_set.rs +++ b/src/checker_set.rs @@ -35,7 +35,7 @@ impl CheckerState { Ok(Set::Variant(fields)) } Set::ClaimedSet(instance) => { - let instance = self.check_instance(instance, &Signature::Set)?; + let instance = self.check_instance(instance, Some(&Signature::Set))?; Ok(Set::ClaimedSet(instance)) } Set::Var(v) => { @@ -313,40 +313,38 @@ impl CheckerState { field: field_set, .. } = self.lookup_variant_field(&arm.tag)?; - let mut new_context = self.clone(); + let mut ctx = self.clone(); let binding_name = arm.bound.clone(); let binding_set = field_set.clone(); - let body = if let Some((tag, inner)) = &matching + let case_arm = if let Some((tag, inner)) = &matching && *tag == arm.tag { - new_context.add_element( - binding_name.clone(), - inner.clone().into(), - binding_set, - )?; - let output = new_context.check_element(arm.body.clone().into(), set)?; + let canonical = + ctx.make_element_definition(binding_name, inner.clone(), binding_set)?; + let output = ctx.check_element(arm.body.clone().into(), set)?; if matches!(computed_output, Some(_)) { panic!( "invariant violation: we somehow matched multiple arms in case analysis" ) } computed_output = Some(output.clone()); - output + CaseArm { + tag: arm.tag.clone(), + bound: canonical, + body: output, + } } else { - new_context.add_element( - binding_name.clone(), - Value::Hypothetical, - binding_set, - )?; - new_context.check_element(arm.body.clone().into(), set)? + let canonical = ctx.make_element_binding(binding_name, binding_set)?; + let body = ctx.check_element(arm.body.clone().into(), set)?; + CaseArm { + tag: arm.tag.clone(), + bound: canonical, + body, + } }; - processed_arms.push(CaseArm { - tag: arm.tag.clone(), - bound: binding_name, - body, - }); + processed_arms.push(case_arm); } Ok(computed_output.unwrap_or(Element::Case { scrutinee: Box::new(scrutinee), diff --git a/src/checker_signature.rs b/src/checker_signature.rs index e92d424..b979f54 100644 --- a/src/checker_signature.rs +++ b/src/checker_signature.rs @@ -19,8 +19,8 @@ impl CheckerState { .into_iter() .map(|p| { let set = ctx.check_set(p.set.clone())?; - ctx.make_element_binding(p.name.clone(), set.clone())?; - Ok(Param { set, name: p.name }) + let canon = ctx.make_element_binding(p.name.clone(), set.clone())?; + Ok(Param { set, name: canon }) }) .collect::<Result<Vec<_>, _>>()?; let codomain = Box::new(ctx.check_signature(*codomain)?); @@ -28,26 +28,28 @@ impl CheckerState { } Signature::Theory(fields) => { let mut ctx = self.clone(); - let fields = fields - .into_iter() - .map(|SigField { signature, name }| { - let signature = ctx.check_signature(signature)?; - ctx.add_instance( + let temp_name = ctx.make_unique_name(); + let mut new_fields = Vec::new(); + for SigField { signature, name } in fields { + let signature = ctx.check_signature(signature)?; + ctx.add_instance(name.clone(), InstanceValue::Hypothetical, signature.clone())?; + // And lo, the special case, our chosen canonical form + if signature == Signature::Set { + ctx.add_set( name.clone(), - InstanceValue::Hypothetical, - signature.clone(), + Set::ClaimedSet(Instance::Var(name.clone())).into(), )?; - // And lo, the special case, our chosen canonical form - if signature == Signature::Set { - ctx.add_set( - name.clone(), - Set::ClaimedSet(Instance::Var(name.clone())).into(), - )?; - } - Ok(SigField { name, signature }) - }) - .collect::<Result<Vec<_>, _>>()?; - Ok(Signature::Theory(fields)) + } + new_fields.push(SigField { name, 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)) } } } @@ -56,11 +58,13 @@ impl CheckerState { pub fn check_instance( &self, instance: Instance, - signature: &Signature, + signature: Option<&Signature>, ) -> Result<Instance, CheckerError> { match instance { Instance::SetCoerce(ref set) => { - if *signature != Signature::Set { + if let Some(signature) = signature + && *signature != Signature::Set + { return Err(CheckerError::WrongSignatureForInstance { value: instance.clone().into(), real: Signature::Set, @@ -78,7 +82,9 @@ impl CheckerState { // Exactly the same discipline as for Element::Var, see there // for some sparse comments let lookup = self.lookup_instance(&v)?; - if !self.equal(signature, &lookup.container) { + if let Some(signature) = signature + && !self.equal(signature, &lookup.container) + { return Err(CheckerError::WrongSignatureForInstance { value: instance.clone().into(), claimed: signature.clone(), @@ -93,25 +99,6 @@ impl CheckerState { } Instance::Record(ref assignations) => { // once again, mutatis mutandis from elements - let rej = |reason| CheckerError::InstanceDoesNotBelong { - instance: instance.clone(), - claimed: signature.clone(), - reason, - }; - - let fields = if let Signature::Theory(fields) = signature { - Ok(fields) - } else { - Err(rej("instance is not a record instance".to_string())) - }?; - - let (signature_fnames, signature_fsigs): (Vec<String>, Vec<Signature>) = fields - .iter() - .map(|SigField { name, signature }| (name.clone(), signature.clone())) - .unzip(); - let mut signature_fnames_sorted = signature_fnames.clone(); - signature_fnames_sorted.sort(); - let (instance_fnames, instance_finstances): (Vec<String>, Vec<&Instance>) = assignations .iter() @@ -121,16 +108,45 @@ impl CheckerState { let mut instance_fnames_sorted = instance_fnames.clone(); instance_fnames_sorted.sort(); - if signature_fnames_sorted != instance_fnames_sorted { - return Err(rej(format!( - "expected [{}] but found [{}]", - signature_fnames.join(", "), - instance_fnames.join(", "), - ))); + let signature_fsigs: Vec<Option<Signature>>; + if let Some(signature) = signature { + let rej = |reason| CheckerError::InstanceDoesNotBelong { + instance: instance.clone(), + claimed: signature.clone(), + reason: reason, + }; + + let fields = if let Signature::Theory(fields) = signature { + Ok(fields) + } else { + Err(rej("signature has no fields".to_string())) + }?; + + let signature_fnames: Vec<String>; + (signature_fnames, signature_fsigs) = fields + .iter() + .map(|SigField { name, signature }| { + (name.clone(), signature.clone().into()) + }) + .unzip(); + let mut signature_fnames_sorted = signature_fnames.clone(); + signature_fnames_sorted.sort(); + + if signature_fnames_sorted != instance_fnames_sorted { + return Err(rej(format!( + "expected [{}] but found [{}]", + signature_fnames.join(", "), + instance_fnames.join(", "), + ))); + } + } else { + signature_fsigs = std::iter::repeat(None) + .take(instance_finstances.len()) + .collect(); } let sub_els = zip(instance_finstances, signature_fsigs) - .map(|(e_f, e_s)| self.check_instance(e_f.clone(), &e_s)) + .map(|(e_f, e_s)| self.check_instance(e_f.clone(), (&e_s).into())) .collect::<Result<Vec<_>, _>>()?; let assignations = zip(instance_fnames, sub_els) .map(|(name, instance)| InstAssign { name, instance }) @@ -146,7 +162,9 @@ impl CheckerState { owner: owner_signature, } = self.lookup_signature_field(&field)?; - if !self.equal(signature, field_signature) { + if let Some(signature) = signature + && !self.equal(signature, field_signature) + { return Err(CheckerError::WrongSignatureForInstance { value: (*instance.clone()).into(), claimed: signature.clone(), @@ -154,7 +172,7 @@ impl CheckerState { }); } - let inner = self.check_instance(*instance.clone(), owner_signature)?; + let inner = self.check_instance(*instance.clone(), owner_signature.into())?; match inner { Instance::Var(_) | Instance::Project { .. } => Ok(Instance::Project { @@ -176,12 +194,52 @@ impl CheckerState { ), } } - Instance::For { params, body } => { - Err(CheckerError::Unimplemented("instance for".to_string())) + Instance::For { .. } => { + todo!("instance for") } - Instance::App(inst, elem) => { - println!("{}", self); - Err(CheckerError::Unimplemented("instance app".to_string())) + Instance::App(inner, element) => { + let inner = self.check_instance(*inner, None)?; + match &inner { + Instance::Var(v) => { + let field = self.lookup_signature_field(&v)?; + let Signature::Ext { + ref params, + ref codomain, + } = field.field + else { + return Err(CheckerError::WrongSignatureForInstance { + value: inner.clone().into(), + claimed: Signature::Ext { + params: vec![Param { + name: "...".to_string(), + set: Set::Var("...".to_string()), + }], + codomain: Box::new(Signature::Var("...".to_string())), + }, + real: field.owner.clone(), + }); + }; + // TODO: we need to assert (somewhere else) that ext has >=1 params + // TODO: in the special case that params.len() == 1 we need to do something with codomain + let element = self.check_element(*element, ¶ms[0].set)?; + Ok(Instance::App( + Box::new(Instance::Var(v.clone())), + Box::new(element), + )) + } + Instance::For { .. } => { + todo!("app for") + } + Instance::Record(_) | Instance::SetCoerce(_) => { + Err(CheckerError::NonFunctionalInstance { + instance: inner, + element: *element, + }) + } + Instance::Project { .. } | Instance::App(_, _) => panic!( + "invariant violation: we did not completely expand the inner instance in our app" + ), + } } } } diff --git a/src/checker_state.rs b/src/checker_state.rs index 1a6a0bd..6a458d5 100644 --- a/src/checker_state.rs +++ b/src/checker_state.rs @@ -47,6 +47,11 @@ pub enum CheckerError { claimed: Signature, reason: String, }, + #[display("Non-functional instance {instance} found in application to element {element}")] + NonFunctionalInstance { + instance: Instance, + element: Element, + }, } // ----------------------------------------------------------------------------- @@ -111,6 +116,7 @@ pub struct CheckerState { variant_fields: HashMap<String, Field<Set>>, signature_fields: HashMap<String, Field<Signature>>, binder_element: usize, + unique_name: usize, } impl fmt::Display for CheckerState { @@ -136,6 +142,7 @@ impl fmt::Display for CheckerState { section(f, "variant_fields", &self.variant_fields)?; section(f, "signatures", &self.wf_signatures)?; section(f, "instances", &self.wf_instances)?; + section(f, "signature_fields", &self.signature_fields)?; writeln!(f, " }}")?; Ok(()) } @@ -332,13 +339,14 @@ impl CheckerState { } #[instrument(skip(self), level = "debug", fields(%name, %field_signature, %owner_signature))] - fn add_signature_field( + pub fn add_signature_field( &mut self, name: &String, field_signature: &Signature, owner_signature: &Signature, + rebind: bool, ) -> Result<(), CheckerError> { - if let Some(signature_ref) = self.signature_fields.get(name) { + if !rebind && let Some(signature_ref) = self.signature_fields.get(name) { self.assert_correct_owner(name, signature_ref, owner_signature)?; }; self.signature_fields.insert( @@ -356,6 +364,7 @@ impl CheckerState { &mut self, name: &String, signature: Signature, + rebind: bool, ) -> Result<(), CheckerError> { match &signature { Signature::Theory(fields) => { @@ -364,7 +373,7 @@ impl CheckerState { signature: field_sig, } in fields { - self.add_signature_field(field_name, field_sig, &signature)?; + self.add_signature_field(field_name, field_sig, &signature, rebind)?; } } // TODO: is there more? @@ -415,12 +424,35 @@ impl CheckerState { // ----------------------------------------------------------------------------- // 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)?; + fn _make_canonical_element(&mut self, name: String, set: Set) -> Result<String, CheckerError> { + let canonical = format!("_#{}", self.binder_element); + self.add_element(name, Element::Var(canonical.clone()).into(), set)?; self.binder_element += 1; - Ok(()) + Ok(canonical) + } + + #[instrument(skip(self), level = "debug", fields(%name, %set))] + pub fn make_element_binding(&mut self, name: String, set: Set) -> Result<String, CheckerError> { + let canonical = self._make_canonical_element(name, set.clone())?; + self.add_element(canonical.clone(), ElementValue::Hypothetical, set)?; + Ok(canonical) + } + + #[instrument(skip(self), level = "debug", fields(%name, %set))] + pub fn make_element_definition( + &mut self, + name: String, + value: Element, + set: Set, + ) -> Result<String, CheckerError> { + let canonical = self._make_canonical_element(name, set.clone())?; + self.add_element(canonical.clone(), Value::Concrete(value), set)?; + Ok(canonical) + } + + #[instrument(skip(self))] + pub fn make_unique_name(&mut self) -> String { + self.unique_name += 1; + format!("_#{}", self.unique_name) } } diff --git a/src/main.rs b/src/main.rs index f721ef4..b8987a2 100644 --- a/src/main.rs +++ b/src/main.rs @@ -43,23 +43,23 @@ let signature T = theory { C :: (x : set-of(set-of(set-of(A) :: Set) :: Set)) (b : set-of(B x)) -> Set } -let signature Graph = theory { - Node :: Set, - Edge :: (s : set-of(Node)) (t : set-of(Node)) -> Set -} +// let signature Graph = theory { +// Node :: Set, +// Edge :: (s : set-of(Node)) (t : set-of(Node)) -> Set +// } -let instance natPoset :: Graph = { - .Node = Nat :: Set, - .Edge = for (s : Nat) (t : Nat), Bool :: Set -} +// let instance natPoset :: Graph = { +// .Node = Nat :: Set, +// .Edge = for (s : Nat) (t : Nat), Bool :: Set +// } -let element node : set-of(natPoset .Node) = 7 +// let element node : set-of(natPoset .Node) = 7 -let set NatEdges = record { - source: set-of(natPoset .Node), - target: set-of(natPoset .Node), - connected: set-of(natPoset .Edge source target) -} +// let set NatEdges = record { +// source: set-of(natPoset .Node), +// target: set-of(natPoset .Node), +// connected: set-of(natPoset .Edge source target) +// } "#; let programme = parser::debug_parse(src); diff --git a/src/parser.rs b/src/parser.rs index 418a17e..1aed3f8 100644 --- a/src/parser.rs +++ b/src/parser.rs @@ -225,7 +225,7 @@ parser! { pub fn debug_parse(src: &str) -> Programme { match parser::program(src) { Ok(p) => { - println!("```{}\n```\n=>\n{}\n", src, p); + println!("{}", p); p } Err(e) => { |