wire in instance checking to the main checker

6 files changed, 64 insertions, 73 deletions

diff --git a/src/ast.rs b/src/ast.rs
index 7fcbee0..d13b2a8 100644
--- a/src/ast.rs
+++ b/src/ast.rs
@@ -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() {