diff options
| -rw-r--r-- | src/checker.rs | 2 | ||||
| -rw-r--r-- | src/checker_set.rs | 18 | ||||
| -rw-r--r-- | src/checker_signature.rs | 154 | ||||
| -rw-r--r-- | src/checker_state.rs | 112 | ||||
| -rw-r--r-- | src/main.rs | 16 |
5 files changed, 258 insertions, 44 deletions
diff --git a/src/checker.rs b/src/checker.rs index da4463c..aefbb02 100644 --- a/src/checker.rs +++ b/src/checker.rs @@ -21,7 +21,7 @@ impl CheckerState { Decl::Set { name, set } => { self.assert_unbound_set(name)?; let set = self.check_set(set.clone())?; - self.add_set(name, set) + self.add_set(name.clone(), set.into()) } Decl::Element { name, element, set } => { diff --git a/src/checker_set.rs b/src/checker_set.rs index 729ce08..86661c7 100644 --- a/src/checker_set.rs +++ b/src/checker_set.rs @@ -15,11 +15,7 @@ impl CheckerState { .into_iter() .map(|RecordField { name, set }| { let set = ctx.check_set(set)?; - ctx.add_element( - name.clone(), - Value::Hypothetical(set.clone()), - set.clone(), - )?; + ctx.make_element_binding(name.clone(), set.clone())?; Ok(RecordField { name, set }) }) .collect::<Result<Vec<_>, _>>()?; @@ -38,10 +34,16 @@ impl CheckerState { .collect::<Result<Vec<_>, _>>()?; Ok(Set::Variant(fields)) } - Set::ClaimedSet(_) => Err(CheckerError::Unimplemented("instances as sets".to_string())), + Set::ClaimedSet(instance) => { + let instance = self.check_instance(instance, &Signature::Set)?; + Ok(Set::ClaimedSet(instance)) + } Set::Var(v) => { let deref = self.lookup_set(&v)?; - Ok(deref.clone()) + match deref { + SetValue::Hypothetical => Ok(Set::Var(v)), + SetValue::Concrete(deref) => Ok(deref.clone()), + } } } } @@ -334,7 +336,7 @@ impl CheckerState { } else { new_context.add_element( binding_name.clone(), - Value::Hypothetical(field_set.clone()), + Value::Hypothetical, binding_set, )?; new_context.check_element(arm.body.clone().into(), set)? diff --git a/src/checker_signature.rs b/src/checker_signature.rs index 4d5f02c..36b11ca 100644 --- a/src/checker_signature.rs +++ b/src/checker_signature.rs @@ -1,5 +1,6 @@ use crate::ast::*; use crate::checker_state::*; +use std::iter::zip; use tracing::instrument; @@ -12,20 +13,27 @@ impl CheckerState { let deref = self.lookup_signature(&v)?; Ok(deref.clone()) } - Signature::Ext { .. } => Err(CheckerError::Unimplemented( - "extension signatures".to_string(), - )), + Signature::Ext { params, codomain } => { + let mut ctx = self.clone(); + let params = params + .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 }) + }) + .collect::<Result<Vec<_>, _>>()?; + let codomain = Box::new(ctx.check_signature(*codomain)?); + Ok(Signature::Ext { params, codomain }) + } 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( - name.clone(), - InstanceValue::Hypothetical(signature.clone()), - signature.clone(), - )?; + // This call handles the special case in the event that signature is Set + ctx.make_instance_binding(name.clone(), signature.clone())?; Ok(SigField { name, signature }) }) .collect::<Result<Vec<_>, _>>()?; @@ -33,4 +41,134 @@ impl CheckerState { } } } + + #[instrument(skip(self), level = "debug", fields(%instance, %signature))] + pub fn check_instance( + &self, + instance: Instance, + signature: &Signature, + ) -> Result<Instance, CheckerError> { + match instance { + Instance::SetCoerce(ref set) => { + if *signature != Signature::Set { + return Err(CheckerError::WrongSignatureForInstance { + value: instance.clone().into(), + real: Signature::Set, + claimed: signature.clone(), + }); + }; + let set = Box::new(self.check_set(*set.clone())?); + Ok(Instance::SetCoerce(set)) + } + Instance::Var(ref v) => { + // 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) { + return Err(CheckerError::WrongSignatureForInstance { + value: instance.clone().into(), + claimed: signature.clone(), + real: lookup.container.clone(), + }); + } + if let InstanceValue::Concrete(ref deref) = lookup.value { + Ok(deref.clone()) + } else { + Ok(Instance::Var(v.clone())) + } + } + 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 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() + .map(|InstAssign { name, instance }| (name.clone(), instance)) + .unzip(); + + 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 sub_els = zip(instance_finstances, signature_fsigs) + .map(|(e_f, e_s)| self.check_instance(e_f.clone(), &e_s)) + .collect::<Result<Vec<_>, _>>()?; + let assignations = zip(instance_fnames, sub_els) + .map(|(name, instance)| InstAssign { name, instance }) + .collect(); + Ok(Instance::Record(assignations)) + } + Instance::Project { + ref instance, + ref field, + } => { + let Field { + field: field_signature, + owner: owner_signature, + } = self.lookup_signature_field(&field)?; + + if !self.equal(signature, field_signature) { + return Err(CheckerError::WrongSignatureForInstance { + value: (*instance.clone()).into(), + claimed: signature.clone(), + real: field_signature.clone(), + }); + } + + let inner = self.check_instance(*instance.clone(), owner_signature)?; + + match inner { + Instance::Var(_) | Instance::Project { .. } => Ok(Instance::Project { + instance: Box::new(inner), + field: field.clone(), + }), + Instance::Record(assignations) => { + let sub_element = assignations + .into_iter() + .find(|a| a.name == *field) + .expect( + "invariant violation: record missing field that was type-checked", + ) + .instance; + Ok(sub_element) + } + _ => panic!( + "invariant violation: check_element returned neither a record or stuck computation for record set" + ), + } + } + Instance::For { params, body } => { + Err(CheckerError::Unimplemented("instance for".to_string())) + } + Instance::App(inst, elem) => { + println!("{}", self); + Err(CheckerError::Unimplemented("instance app".to_string())) + } + } + } } 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(()) + } } diff --git a/src/main.rs b/src/main.rs index 3f6b3cc..a40eb87 100644 --- a/src/main.rs +++ b/src/main.rs @@ -20,16 +20,16 @@ fn main() { let src = r#" // let X be the set Y, call it Z -let set X = record { b : Bool, n : Nat } -let set Y = X -let set Z = record { y : Y } +// let set X = record { b : Bool, n : Nat } +// let set Y = X +// let set Z = record { y : Y } // make some elements -let element x : X = { .b = true, .n = 41 } -let element z : Z = { .y = x } +// let element x : X = { .b = true, .n = 41 } +// let element z : Z = { .y = x } // exercise case matching -let set Z_or_Float = variant [ z : Z | f : Float ] -let element injected : Z_or_Float = z. z -let element check_cases : Nat = case injected of [ z. myz => myz .y .n | f. myf => 2 ] +// let set Z_or_Float = variant [ z : Z | f : Float ] +// let element injected : Z_or_Float = z. z +// let element check_cases : Nat = case injected of [ z. myz => myz .y .n | f. myf => 2 ] // this should be difficult unless we correctly handle various forms of alpha/beta let signature OneSet = theory { F :: Set } |