basic checking sketch

4 files changed, 435 insertions, 183 deletions

diff --git a/src/ast.rs b/src/ast.rs
new file mode 100644
index 0000000..0590556
--- /dev/null
+++ b/src/ast.rs
@@ -0,0 +1,172 @@
+use derive_more::Display;
+
+// Set layer
+
+#[derive(Clone, Debug, PartialEq, Display)]
+pub enum BuiltIn {
+    Nat,
+    Int,
+    Float,
+    Str,
+    Bool,
+}
+
+#[derive(Clone, Debug, PartialEq, Display)]
+#[display(".{name} : {set}")]
+pub struct RecordField {
+    pub name: String,
+    pub set: Set,
+}
+
+#[derive(Clone, Debug, PartialEq, Display)]
+#[display("{name}. : {set}")]
+pub struct VariantField {
+    pub name: String,
+    pub set: Set,
+}
+
+#[derive(Clone, Debug, PartialEq, Display)]
+pub enum Set {
+    #[display("{_0}")]
+    BuiltIn(BuiltIn),
+    #[display("record {{ {} }}", _0.iter().map(|f| f.to_string()).collect::<Vec<_>>().join(" , "))]
+    Record(Vec<RecordField>),
+    #[display("variant [ {} ]", _0.iter().map(|f| f.to_string()).collect::<Vec<_>>().join(" | "))]
+    Variant(Vec<VariantField>),
+    #[display("set({_0})")]
+    ClaimedSet(Instance),
+    #[display("{_0}")]
+    Var(String),
+}
+
+// Signature layer
+
+#[derive(Clone, Debug, PartialEq, Display)]
+#[display("({name} : {set})")]
+pub struct Param {
+    pub name: String,
+    pub set: Set,
+}
+
+#[derive(Clone, Debug, PartialEq, Display)]
+#[display(".{name} :: {signature}")]
+pub struct SigField {
+    pub name: String,
+    pub signature: Signature,
+}
+
+#[derive(Clone, Debug, PartialEq, Display)]
+pub enum Signature {
+    #[display("Set")]
+    Set,
+    #[display("theory {{ {} }}", _0.iter().map(|f| f.to_string()).collect::<Vec<_>>().join(" , "))]
+    Theory(Vec<SigField>),
+    #[display("{} -> {}", params.iter().map(|p| p.to_string()).collect::<Vec<_>>().join(", "), codomain)]
+    Ext {
+        params: Vec<Param>,
+        codomain: Box<Signature>,
+    },
+    #[display("{_0}")]
+    Var(String),
+}
+
+// Element layer
+
+#[derive(Clone, Debug, PartialEq, Display)]
+pub enum Literal {
+    Nat(u64),
+    Int(i64),
+    Float(f64),
+    Str(String),
+    Bool(bool),
+}
+
+#[derive(Clone, Debug, PartialEq, Display)]
+#[display(".{name} = {element}")]
+pub struct ElemAssign {
+    pub name: String,
+    pub element: Element,
+}
+
+#[derive(Clone, Debug, PartialEq, Display)]
+#[display(".{tag} {bound} => {body}")]
+pub struct CaseArm {
+    pub tag: String,
+    pub bound: String,
+    pub body: Element,
+}
+
+#[derive(Clone, Debug, PartialEq, Display)]
+pub enum Element {
+    #[display("{_0}")]
+    Literal(Literal),
+    #[display("{_0}")]
+    Var(String),
+    #[display("{{ {} }}", _0.iter().map(|f| f.to_string()).collect::<Vec<_>>().join(" , "))]
+    Record(Vec<ElemAssign>),
+    #[display("{_0} .{_1}")]
+    Project(Box<Element>, String),
+    #[display("{_0}. {_1}")]
+    Inject(String, Box<Element>),
+    #[display("{_0} {_1}")]
+    App(Box<Element>, Box<Element>),
+    #[display("case {} of {{ {} }}", scrutinee, arms.iter().map(|f| f.to_string()).collect::<Vec<_>>().join(" | "))]
+    Case {
+        scrutinee: Box<Element>,
+        arms: Vec<CaseArm>,
+    },
+}
+
+// Instance layer
+
+#[derive(Clone, Debug, PartialEq, Display)]
+#[display(".{name} = {instance}")]
+pub struct InstAssign {
+    pub name: String,
+    pub instance: Instance,
+}
+
+#[derive(Clone, Debug, PartialEq, Display)]
+pub enum Instance {
+    #[display("({_0} :: Set)")]
+    SetCoerce(Box<Set>),
+    #[display("{_0}")]
+    Var(String),
+    #[display("{{ {} }}", _0.iter().map(|f| f.to_string()).collect::<Vec<_>>().join(", "))]
+    Record(Vec<InstAssign>),
+    #[display("for {}, {body}", params.iter().map(|f| f.to_string()).collect::<Vec<_>>().join(""))]
+    For {
+        params: Vec<Param>,
+        body: Box<Instance>,
+    },
+    #[display("{_0} {_1}")]
+    App(Box<Instance>, Box<Element>),
+    #[display("{_0} .{_1}")]
+    Project(Box<Instance>, String),
+}
+
+// Declarations
+
+#[derive(Clone, Debug, PartialEq, Display)]
+pub enum Decl {
+    #[display("let set {name} = {set}")]
+    Set { name: String, set: Set },
+    #[display("let element {name} : {set} = {element}")]
+    Element {
+        name: String,
+        set: Set,
+        element: Element,
+    },
+    #[display("let signature {name} = {signature}")]
+    Signature { name: String, signature: Signature },
+    #[display("let instance {name} :: {signature} = {instance}")]
+    Instance {
+        name: String,
+        signature: Signature,
+        instance: Instance,
+    },
+}
+
+#[derive(Display)]
+#[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 ea099ab..a53a48a 100644
--- a/src/checker.rs
+++ b/src/checker.rs
@@ -1,7 +1,219 @@
-use crate::parser::*;
+use crate::ast::*;
+use tracing::{debug, instrument, trace};
 
+use derive_more::Display;
+use std::collections::HashMap;
+
+#[derive(Display)]
 pub enum CheckError {
+    #[display("Unbound: {_0}")]
     Unbound(String),
+    #[display("Duplicate field: {_0}")]
     DuplicateField(String),
-    ExpectedTypeFoundTerm(String),
+    #[display("Rebinding: {_0}")]
+    Rebinding(String),
+    #[display("The following functionality is unimplemented: {_0}")]
+    Unimplemented(String),
+}
+
+#[derive(Debug)]
+struct SetRef {
+    set: Set,
+    belongs_to: String,
+}
+
+#[derive(Debug)]
+struct ElRef {
+    set: Set,
+    belongs_to: String,
+}
+
+#[derive(Debug, Default)]
+struct CheckState {
+    sets: HashMap<String, Set>,
+    elements: HashMap<String, Element>,
+    record_fields: HashMap<String, SetRef>,
+    variant_fields: HashMap<String, SetRef>,
+    signatures: HashMap<String, Signature>,
+    instances: HashMap<String, Instance>,
+}
+
+impl CheckState {
+    #[instrument(skip(self), level = "debug")]
+    fn assert_unbound_set(&self, name: &String) -> Result<(), CheckError> {
+        if self.sets.contains_key(name) {
+            Err(CheckError::Rebinding(name.clone()))
+        } else {
+            Ok(())
+        }
+    }
+
+    #[instrument(skip(self), level = "debug")]
+    fn assert_unbound_record_field(&self, name: &String) -> Result<(), CheckError> {
+        if self.record_fields.contains_key(name) {
+            Err(CheckError::Rebinding(name.clone()))
+        } else {
+            Ok(())
+        }
+    }
+
+    #[instrument(skip(self), level = "debug")]
+    fn assert_unbound_variant_field(&self, name: &String) -> Result<(), CheckError> {
+        if self.variant_fields.contains_key(name) {
+            Err(CheckError::Rebinding(name.clone()))
+        } else {
+            Ok(())
+        }
+    }
+
+    #[instrument(skip(self), level = "debug")]
+    fn assert_unbound_element(&self, name: &String) -> Result<(), CheckError> {
+        if self.elements.contains_key(name) {
+            Err(CheckError::Rebinding(name.clone()))
+        } else {
+            Ok(())
+        }
+    }
+
+    #[instrument(skip(self), level = "debug")]
+    fn add_record_field(
+        &mut self,
+        name: &String,
+        set: &Set,
+        belongs_to: &String,
+    ) -> Result<(), CheckError> {
+        self.assert_unbound_record_field(name)?;
+        self.record_fields.insert(
+            name.clone(),
+            SetRef {
+                set: set.clone(),
+                belongs_to: belongs_to.clone(),
+            },
+        );
+        Ok(())
+    }
+
+    #[instrument(skip(self), level = "debug")]
+    fn add_variant_field(
+        &mut self,
+        name: &String,
+        set: &Set,
+        belongs_to: &String,
+    ) -> Result<(), CheckError> {
+        self.assert_unbound_variant_field(name)?;
+        self.variant_fields.insert(
+            name.clone(),
+            SetRef {
+                set: set.clone(),
+                belongs_to: belongs_to.clone(),
+            },
+        );
+        Ok(())
+    }
+
+    #[instrument(skip(self), level = "debug")]
+    fn add_set(&mut self, name: &String, set: &Set) -> Result<(), CheckError> {
+        self.assert_unbound_set(name)?;
+        match set {
+            Set::Record(fields) => {
+                for RecordField { name: rfn, set } in fields {
+                    self.add_record_field(rfn, set, name)?;
+                }
+            }
+            Set::Variant(fields) => {
+                for VariantField { name: vfn, set } in fields {
+                    self.add_variant_field(vfn, set, name)?;
+                }
+            }
+            _ => (),
+        };
+        self.sets.insert(name.clone(), set.clone());
+        Ok(())
+    }
+
+    #[instrument(skip(self), level = "debug")]
+    fn add_element(&mut self, name: &String, element: &Element) -> Result<(), CheckError> {
+        self.assert_unbound_element(name)?;
+        self.elements.insert(name.clone(), element.clone());
+        Ok(())
+    }
+}
+
+impl CheckState {
+    #[instrument(skip(self, prog), level = "debug")]
+    pub fn check(&mut self, prog: &Programme) -> Result<(), CheckError> {
+        let Programme(decls) = prog;
+
+        for decl in decls {
+            debug!(%decl, "checking declaration");
+            match decl {
+                Decl::Set { name, set } => {
+                    self.assert_unbound_set(name)?;
+                    self.check_set(set)?;
+                    // One catch, prohibit "let .. X = X"
+                    if let Set::Var(v) = set
+                        && v == name
+                    {
+                        return Err(CheckError::Rebinding(v.clone()));
+                    };
+                    self.add_set(name, set)
+                }
+
+                Decl::Element { name, set, element } => {
+                    self.check_element(name, set, element)?;
+                    // TODO: don't drop the set?
+                    self.add_element(name, element)
+                }
+                Decl::Signature { name, signature } => Ok(()),
+                Decl::Instance {
+                    name,
+                    signature,
+                    instance,
+                } => Ok(()),
+            }?;
+        }
+        Ok(())
+    }
+
+    #[instrument(skip(self), level = "debug")]
+    fn check_set(&self, set: &Set) -> Result<(), CheckError> {
+        match set {
+            Set::BuiltIn(_) => Ok(()),
+            Set::Record(fields) => self.check_record(fields),
+            Set::Variant(fields) => Err(CheckError::Unimplemented("variants".to_string())),
+            Set::ClaimedSet(instance) => {
+                Err(CheckError::Unimplemented("instances as sets".to_string()))
+            }
+            Set::Var(v) => {
+                if self.sets.contains_key(v) {
+                    Ok(())
+                } else {
+                    Err(CheckError::Unbound(v.clone()))
+                }
+            }
+        }
+    }
+
+    #[instrument(skip(self), level = "debug")]
+    fn check_record(&self, fields: &Vec<RecordField>) -> Result<(), CheckError> {
+        for RecordField { name, set } in fields {
+            self.assert_unbound_record_field(name)?;
+            self.check_set(set)?;
+        }
+        Ok(())
+    }
+
+    #[instrument(skip(self), level = "debug")]
+    fn check_element(&self, name: &String, set: &Set, element: &Element) -> Result<(), CheckError> {
+        self.assert_unbound_element(name)?;
+        self.check_set(set)?;
+        Ok(())
+    }
+}
+
+impl Programme {
+    pub fn check(&self) -> Result<(), CheckError> {
+        let mut state = CheckState::default();
+        state.check(self)
+    }
 }
diff --git a/src/main.rs b/src/main.rs
index 56e14c5..11357a9 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -1,6 +1,44 @@
+mod ast;
 mod checker;
 mod parser;
 
+use tracing_subscriber::{layer::SubscriberExt, util::SubscriberInitExt};
+use tracing_tree::HierarchicalLayer;
+
 fn main() {
-    println!("Hello, world!");
+    tracing_subscriber::registry()
+        .with(
+            HierarchicalLayer::new(2)
+                .with_targets(false)
+                .with_bracketed_fields(true),
+        )
+        .init();
+
+    let src = r#"
+
+let set X = record { .b : Bool, .n : Nat }
+
+let element x : X = { .b = true, .n = 41, .x = 3.14 }
+
+let signature Graph = theory {
+    .Node :: Set,
+    .Edge :: (s : Node) (t : Node) -> Set
+}
+
+let instance natPoset :: Graph = {
+    .Node = Nat,
+    .Edge = for (s : Nat) (t : Nat), Bool
+}
+
+let element node : set(natPoset .Node) = 7
+"#;
+    let programme = parser::parser::program(src);
+
+    assert!(programme.is_ok());
+    let programme = programme.unwrap();
+    println!("Parsed:\n```\n{}\n```\n", programme);
+
+    if let Err(e) = programme.check() {
+        println!("{}", e);
+    }
 }
diff --git a/src/parser.rs b/src/parser.rs
index a0da79c..f98673e 100644
--- a/src/parser.rs
+++ b/src/parser.rs
@@ -1,176 +1,6 @@
-use derive_more::Display;
 use peg::parser;
 
-// Set layer
-
-#[derive(Clone, Debug, PartialEq, Display)]
-pub enum BuiltIn {
-    Nat,
-    Int,
-    Float,
-    Str,
-    Bool,
-}
-
-#[derive(Clone, Debug, PartialEq, Display)]
-#[display(".{name} : {set}")]
-pub struct SetField {
-    pub name: String,
-    pub set: Set,
-}
-
-#[derive(Clone, Debug, PartialEq, Display)]
-#[display("{name}. : {set}")]
-pub struct VariantField {
-    pub name: String,
-    pub set: Set,
-}
-
-#[derive(Clone, Debug, PartialEq, Display)]
-pub enum Set {
-    #[display("{_0}")]
-    BuiltIn(BuiltIn),
-    #[display("record {{ {} }}", _0.iter().map(|f| f.to_string()).collect::<Vec<_>>().join(" , "))]
-    Record(Vec<SetField>),
-    #[display("variant [ {} ]", _0.iter().map(|f| f.to_string()).collect::<Vec<_>>().join(" | "))]
-    Variant(Vec<VariantField>),
-    #[display("set({_0})")]
-    ClaimedSet(Instance),
-    #[display("{_0}")]
-    Var(String),
-}
-
-// Signature layer
-
-#[derive(Clone, Debug, PartialEq, Display)]
-#[display("({name} : {set})")]
-pub struct Param {
-    pub name: String,
-    pub set: Set,
-}
-
-#[derive(Clone, Debug, PartialEq, Display)]
-#[display(".{name} :: {signature}")]
-pub struct SigField {
-    pub name: String,
-    pub signature: Signature,
-}
-
-#[derive(Clone, Debug, PartialEq, Display)]
-pub enum Signature {
-    #[display("Set")]
-    Set,
-    #[display("theory {{ {} }}", _0.iter().map(|f| f.to_string()).collect::<Vec<_>>().join(" , "))]
-    Theory(Vec<SigField>),
-    #[display("{} -> {}", params.iter().map(|p| p.to_string()).collect::<Vec<_>>().join(", "), codomain)]
-    Ext {
-        params: Vec<Param>,
-        codomain: Box<Signature>,
-    },
-    #[display("{_0}")]
-    Var(String),
-}
-
-// Element layer
-
-#[derive(Clone, Debug, PartialEq, Display)]
-pub enum Literal {
-    Nat(u64),
-    Int(i64),
-    Float(f64),
-    Str(String),
-    Bool(bool),
-}
-
-#[derive(Clone, Debug, PartialEq, Display)]
-#[display(".{name} = {element}")]
-pub struct ElemAssign {
-    pub name: String,
-    pub element: Element,
-}
-
-#[derive(Clone, Debug, PartialEq, Display)]
-#[display(".{tag} {bound} => {body}")]
-pub struct CaseArm {
-    pub tag: String,
-    pub bound: String,
-    pub body: Element,
-}
-
-#[derive(Clone, Debug, PartialEq, Display)]
-pub enum Element {
-    #[display("{_0}")]
-    Literal(Literal),
-    #[display("{_0}")]
-    Var(String),
-    #[display("{{ {} }}", _0.iter().map(|f| f.to_string()).collect::<Vec<_>>().join(" , "))]
-    Record(Vec<ElemAssign>),
-    #[display("{_0} .{_1}")]
-    Project(Box<Element>, String),
-    #[display("{_0}. {_1}")]
-    Inject(String, Box<Element>),
-    #[display("{_0} {_1}")]
-    App(Box<Element>, Box<Element>),
-    #[display("case {} of {{ {} }}", scrutinee, arms.iter().map(|f| f.to_string()).collect::<Vec<_>>().join(" | "))]
-    Case {
-        scrutinee: Box<Element>,
-        arms: Vec<CaseArm>,
-    },
-}
-
-// Instance layer
-
-#[derive(Clone, Debug, PartialEq, Display)]
-#[display(".{name} = {instance}")]
-pub struct InstAssign {
-    pub name: String,
-    pub instance: Instance,
-}
-
-#[derive(Clone, Debug, PartialEq, Display)]
-pub enum Instance {
-    #[display("{_0}")]
-    SetCoerce(Box<Set>),
-    #[display("{_0}")]
-    Var(String),
-    #[display("{{ {} }}", _0.iter().map(|f| f.to_string()).collect::<Vec<_>>().join(", "))]
-    Record(Vec<InstAssign>),
-    #[display("for {}, {body}", params.iter().map(|f| f.to_string()).collect::<Vec<_>>().join(""))]
-    For {
-        params: Vec<Param>,
-        body: Box<Instance>,
-    },
-    #[display("{_0} {_1}")]
-    App(Box<Instance>, Box<Element>),
-    #[display("{_0} .{_1}")]
-    Project(Box<Instance>, String),
-}
-
-// Declarations
-
-#[derive(Clone, Debug, PartialEq, Display)]
-pub enum Decl {
-    #[display("let set {name} = {set}")]
-    Set { name: String, set: Set },
-    #[display("let element {name} : {set} = {element}")]
-    Element {
-        name: String,
-        set: Set,
-        element: Element,
-    },
-    #[display("let signature {name} = {signature}")]
-    Signature { name: String, signature: Signature },
-    #[display("let instance {name} :: {signature} = {instance}")]
-    Instance {
-        name: String,
-        signature: Signature,
-        instance: Instance,
-    },
-}
-
-#[derive(Display)]
-#[display("{}", _0.iter().map(|d| d.to_string()).collect::<Vec<_>>().join("\n"))]
-pub struct Programme(Vec<Decl>);
+use crate::ast::*;
 
 parser! {
     pub grammar parser() for str {
@@ -272,8 +102,8 @@ parser! {
 
         // set layer
 
-        rule set_field() -> SetField
-        = n:project_lower() _ ":" _ s:set() { SetField { name: n, set: s } }
+        rule set_field() -> RecordField
+        = n:project_lower() _ ":" _ s:set() { RecordField { name: n, set: s } }
 
         rule variant_field() -> VariantField
         = n:inject_lower() _ ":" _ s:set() _ { VariantField { name: n, set: s } }
@@ -281,7 +111,7 @@ parser! {
         rule claimed_set() -> Instance
         = kw_set() "(" _ i:instance() _ ")" { i }
 
-        pub rule set() -> Set
+        rule set() -> Set
         = kw_record()  _ "{" fs:(set_field() ** ",") _ "}" { Set::Record(fs) }
         / kw_variant() _ "{" _ vs:(variant_field() ** "|") "}" { Set::Variant(vs) }
         / b:builtin() { Set::BuiltIn(b) }
@@ -299,7 +129,7 @@ parser! {
         rule sig_field() -> SigField
         = n:project_upper() _ "::" _ s:signature() { SigField { name: n, signature: s } }
 
-        pub rule signature() -> Signature
+        rule signature() -> Signature
         = kw_Set()    { Signature::Set }
         / kw_theory() _ "{" fs:(sig_field() ** ",") _ "}" { Signature::Theory(fs) }
         / ps:param_list() _ "->" _ cod:signature() { Signature::Ext { params: ps, codomain: Box::new(cod) } }
@@ -339,7 +169,7 @@ parser! {
         rule case_arm() -> CaseArm
         = t:inject() _ x:elem_var() _ "=>" _ body:element() { CaseArm { tag: t, bound: x, body } }
 
-        pub rule element() -> Element
+        rule element() -> Element
         = kw_case() __ scrut:element() _ kw_of() _ "{" arms:(_ a:case_arm() _ { a }) ** "|"  _ "}" { Element::Case { scrutinee: Box::new(scrut), arms } }
         / app_elem()
 
@@ -371,7 +201,7 @@ parser! {
             })
         }
 
-        pub rule instance() -> Instance
+        rule instance() -> Instance
         = kw_for() __ ps:param_list() _ "," _ body:instance() { Instance::For { params: ps, body: Box::new(body) } }
         / app_inst()
 
@@ -451,12 +281,12 @@ let set Maybe = variant {
                 .Edge :: (s : Node) (t : Node) -> Set
             }
 
-            let instance loop :: Graph = {
+            let instance natPoset :: Graph = {
                 .Node = Nat,
-                .Edge = for (s : Nat) (t : Nat), Nat
+                .Edge = for (s : Nat) (t : Nat), Bool
             }
 
-            let element node : set(loop .Node) = 7
+            let element node : set(natPoset .Node) = 7
         "#;
 
         debug_parse(src);