diff options
| -rw-r--r-- | src/ast.rs | 30 | ||||
| -rw-r--r-- | src/checker.rs | 11 | ||||
| -rw-r--r-- | src/checker_signature.rs | 18 | ||||
| -rw-r--r-- | src/checker_state.rs | 29 | ||||
| -rw-r--r-- | src/main.rs | 10 | ||||
| -rw-r--r-- | src/parser.rs | 39 |
6 files changed, 64 insertions, 73 deletions
@@ -2,7 +2,7 @@ use derive_more::Display; // Set layer -#[derive(Clone, PartialEq, Display)] +#[derive(Clone, PartialEq, Display, Debug)] pub enum BuiltIn { Nat, Int, @@ -11,21 +11,21 @@ pub enum BuiltIn { Bool, } -#[derive(Clone, PartialEq, Display)] +#[derive(Clone, PartialEq, Display, Debug)] #[display("{name} : {set}")] pub struct RecordField { pub name: String, pub set: Set, } -#[derive(Clone, PartialEq, Display)] +#[derive(Clone, PartialEq, Display, Debug)] #[display("{name} : {set}")] pub struct VariantField { pub name: String, pub set: Set, } -#[derive(Clone, PartialEq, Display)] +#[derive(Clone, PartialEq, Display, Debug)] pub enum Set { #[display("{_0}")] BuiltIn(BuiltIn), @@ -45,21 +45,21 @@ pub enum Set { // Signature layer -#[derive(Clone, PartialEq, Display)] +#[derive(Clone, PartialEq, Display, Debug)] #[display("({name} : {set})")] pub struct Param { pub name: String, pub set: Set, } -#[derive(Clone, PartialEq, Display)] +#[derive(Clone, PartialEq, Display, Debug)] #[display("{name} :: {signature}")] pub struct SigField { pub name: String, pub signature: Signature, } -#[derive(Clone, PartialEq, Display)] +#[derive(Clone, PartialEq, Display, Debug)] pub enum Signature { #[display("Set")] Set, @@ -79,7 +79,7 @@ pub enum Signature { // Element layer -#[derive(Clone, PartialEq, Display)] +#[derive(Clone, PartialEq, Display, Debug)] pub enum Literal { Nat(u64), Int(i64), @@ -88,14 +88,14 @@ pub enum Literal { Bool(bool), } -#[derive(Clone, PartialEq, Display)] +#[derive(Clone, PartialEq, Display, Debug)] #[display(".{name} = {element}")] pub struct ElemAssign { pub name: String, pub element: Element, } -#[derive(Clone, PartialEq, Display)] +#[derive(Clone, PartialEq, Display, Debug)] #[display(".{tag} {bound} => {body}")] pub struct CaseArm { pub tag: String, @@ -103,7 +103,7 @@ pub struct CaseArm { pub body: Element, } -#[derive(Clone, PartialEq, Display)] +#[derive(Clone, PartialEq, Display, Debug)] pub enum Element { #[display("{_0}")] Literal(Literal), @@ -135,14 +135,14 @@ pub enum Element { // Instance layer -#[derive(Clone, PartialEq, Display)] +#[derive(Clone, PartialEq, Display, Debug)] #[display(".{name} = {instance}")] pub struct InstAssign { pub name: String, pub instance: Instance, } -#[derive(Clone, PartialEq, Display)] +#[derive(Clone, PartialEq, Display, Debug)] pub enum Instance { #[display("({_0} :: Set)")] SetCoerce(Box<Set>), @@ -171,7 +171,7 @@ pub enum Instance { // Declarations -#[derive(Clone, PartialEq, Display)] +#[derive(Clone, PartialEq, Display, Debug)] pub enum Decl { #[display("let set {name} = {set}")] Set { name: String, set: Set }, @@ -194,6 +194,6 @@ pub enum Decl { }, } -#[derive(Display)] +#[derive(Display, Debug)] #[display("{}", _0.iter().map(|d| d.to_string()).collect::<Vec<_>>().join("\n"))] pub struct Programme(pub Vec<Decl>); diff --git a/src/checker.rs b/src/checker.rs index aefbb02..dc3dc3c 100644 --- a/src/checker.rs +++ b/src/checker.rs @@ -35,10 +35,15 @@ impl CheckerState { let signature = self.check_signature(signature.clone())?; self.add_signature(name, signature) } - Decl::Instance { name, .. } => { + Decl::Instance { + name, + instance, + signature, + } => { self.assert_unbound_instance(name)?; - - return Err(CheckerError::Unimplemented("instances".to_string())); + let signature = self.check_signature(signature.clone())?; + let instance = self.check_instance(instance.clone(), &signature)?; + self.add_instance(name.clone(), instance.into(), signature) } }?; } diff --git a/src/checker_signature.rs b/src/checker_signature.rs index 15203b2..e92d424 100644 --- a/src/checker_signature.rs +++ b/src/checker_signature.rs @@ -32,8 +32,18 @@ impl CheckerState { .into_iter() .map(|SigField { signature, name }| { let signature = ctx.check_signature(signature)?; - // This call handles the special case in the event that signature is Set - ctx.make_instance_binding(name.clone(), signature.clone())?; + 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(), + Set::ClaimedSet(Instance::Var(name.clone())).into(), + )?; + } Ok(SigField { name, signature }) }) .collect::<Result<Vec<_>, _>>()?; @@ -42,7 +52,7 @@ impl CheckerState { } } - #[instrument(skip(self), level = "debug", fields(%instance, %signature))] + #[instrument(skip(self), level = "debug", fields(%instance, ?signature))] pub fn check_instance( &self, instance: Instance, @@ -92,7 +102,7 @@ impl CheckerState { let fields = if let Signature::Theory(fields) = signature { Ok(fields) } else { - Err(rej("instance is a record instance".to_string())) + Err(rej("instance is not a record instance".to_string())) }?; let (signature_fnames, signature_fsigs): (Vec<String>, Vec<Signature>) = fields diff --git a/src/checker_state.rs b/src/checker_state.rs index b710ac3..1a6a0bd 100644 --- a/src/checker_state.rs +++ b/src/checker_state.rs @@ -41,7 +41,7 @@ pub enum CheckerError { claimed: Signature, real: Signature, }, - #[display("Instance {instance} does belong to set {claimed}: {reason}")] + #[display("Instance {instance} is not of signature {claimed}: {reason}")] InstanceDoesNotBelong { instance: Instance, claimed: Signature, @@ -111,7 +111,6 @@ pub struct CheckerState { variant_fields: HashMap<String, Field<Set>>, signature_fields: HashMap<String, Field<Signature>>, binder_element: usize, - binder_instance: usize, } impl fmt::Display for CheckerState { @@ -424,30 +423,4 @@ impl CheckerState { 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, our chosen canonical form - if signature == Signature::Set { - self.add_set(name, Set::ClaimedSet(Instance::Var(canonical)).into())?; - } - - self.binder_instance += 1; - Ok(()) - } } diff --git a/src/main.rs b/src/main.rs index 94a9428..f721ef4 100644 --- a/src/main.rs +++ b/src/main.rs @@ -31,6 +31,10 @@ fn main() { // 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 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 element e : set-of(natPoset .Edge 3 5) = true + // this should be difficult unless we correctly handle various forms of alpha/beta let signature OneSet = theory { F :: Set } let signature T = theory { @@ -57,11 +61,7 @@ let set NatEdges = record { connected: set-of(natPoset .Edge source target) } "#; - let programme = parser::parser::program(src); - - assert!(programme.is_ok()); - let programme = programme.unwrap(); - println!("Parsed:\n```\n{}\n```\n", programme); + let programme = parser::debug_parse(src); if let Err(e) = programme.check() { println!("{}", e); diff --git a/src/parser.rs b/src/parser.rs index e917aac..418a17e 100644 --- a/src/parser.rs +++ b/src/parser.rs @@ -222,27 +222,30 @@ parser! { } } -#[cfg(test)] -mod tests { - use super::*; - - fn debug_parse(src: &str) { - match parser::program(src) { - Ok(p) => println!("```{}\n```\n=>\n{}\n", src, p), - Err(e) => { - let line = e.location.line; - let col = e.location.column; - let off = e.location.offset; - println!("FAIL at {}:{} (offset {})", line, col, off); - println!("expected: {:#}", e.expected); +pub fn debug_parse(src: &str) -> Programme { + match parser::program(src) { + Ok(p) => { + println!("```{}\n```\n=>\n{}\n", src, p); + p + } + Err(e) => { + let line = e.location.line; + let col = e.location.column; + let off = e.location.offset; + println!("FAIL at {}:{} (offset {})", line, col, off); + println!("expected: {:#}", e.expected); - let before = &src[off.saturating_sub(40)..off]; - let after = &src[off..(off + 40).min(src.len())]; - println!("...{}⟨HERE⟩{}...", before, after); - panic!("Parse failed!"); - } + let before = &src[off.saturating_sub(40)..off]; + let after = &src[off..(off + 40).min(src.len())]; + println!("...{}⟨HERE⟩{}...", before, after); + panic!("Parse failed!"); } } +} + +#[cfg(test)] +mod tests { + use super::*; #[test] fn test_sets() { |