checking for injections, projections, rm vesitigial App

4 files changed, 98 insertions, 43 deletions

diff --git a/src/ast.rs b/src/ast.rs
index 1b34fc3..f517b37 100644
--- a/src/ast.rs
+++ b/src/ast.rs
@@ -126,9 +126,6 @@ pub enum Element {
         element: Box<Element>,
     },
 
-    #[display("{_0} {_1}")]
-    App(Box<Element>, Box<Element>),
-
     #[display("case {} of {{ {} }}", scrutinee, arms.iter().map(|a| a.to_string()).collect::<Vec<_>>().join(" | "))]
     Case {
         scrutinee: Box<Element>,
diff --git a/src/checker.rs b/src/checker.rs
index d45a5a4..2c6c5d0 100644
--- a/src/checker.rs
+++ b/src/checker.rs
@@ -32,10 +32,10 @@ pub enum CheckError {
 }
 
 #[derive(Display)]
-#[display("{value} @ {belongs_to}")]
+#[display("{field_set} @ {owner_set}")]
 struct SetField {
-    value: Set,
-    belongs_to: Set,
+    field_set: Set,
+    owner_set: Set,
 }
 
 #[derive(Display)]
@@ -109,52 +109,48 @@ impl CheckState {
         set_ref: &SetField,
         belongs_to: &Set,
     ) -> Result<(), CheckError> {
-        let SetField {
-            value: _,
-            belongs_to: owner,
-        } = set_ref;
-        if !self.set_equal(owner, belongs_to) {
+        if !self.set_equal(&set_ref.owner_set, belongs_to) {
             Err(CheckError::Rebinding(name.clone()))
         } else {
             Ok(())
         }
     }
 
-    #[instrument(skip(self), level = "debug", fields(%name, %set, %belongs_to))]
+    #[instrument(skip(self), level = "debug", fields(%name, %field_set, %owner_set))]
     fn add_record_field(
         &mut self,
         name: &String,
-        set: &Set,
-        belongs_to: &Set,
+        field_set: &Set,
+        owner_set: &Set,
     ) -> Result<(), CheckError> {
         if let Some(set_ref) = self.record_fields.get(name) {
-            self.assert_correct_owner(name, set_ref, belongs_to)?;
+            self.assert_correct_owner(name, set_ref, owner_set)?;
         };
         self.record_fields.insert(
             name.clone(),
             SetField {
-                value: set.clone(),
-                belongs_to: belongs_to.clone(),
+                field_set: field_set.clone(),
+                owner_set: owner_set.clone(),
             },
         );
         Ok(())
     }
 
-    #[instrument(skip(self), level = "debug", fields(%name, %set, %belongs_to))]
+    #[instrument(skip(self), level = "debug", fields(%name, %field_set, %owner_set))]
     fn add_variant_field(
         &mut self,
         name: &String,
-        set: &Set,
-        belongs_to: &Set,
+        field_set: &Set,
+        owner_set: &Set,
     ) -> Result<(), CheckError> {
         if let Some(set_ref) = self.variant_fields.get(name) {
-            self.assert_correct_owner(name, set_ref, belongs_to)?;
+            self.assert_correct_owner(name, set_ref, owner_set)?;
         };
         self.variant_fields.insert(
             name.clone(),
             SetField {
-                value: set.clone(),
-                belongs_to: belongs_to.clone(),
+                field_set: field_set.clone(),
+                owner_set: owner_set.clone(),
             },
         );
         Ok(())
@@ -167,19 +163,19 @@ impl CheckState {
             Set::Record(fields) => {
                 for RecordField {
                     name: rfn,
-                    set: rset,
+                    set: field_set,
                 } in fields
                 {
-                    self.add_record_field(rfn, rset, &set)?;
+                    self.add_record_field(rfn, field_set, &set)?;
                 }
             }
             Set::Variant(fields) => {
                 for VariantField {
                     name: vfn,
-                    set: vset,
+                    set: field_set,
                 } in fields
                 {
-                    self.add_variant_field(vfn, vset, &set)?;
+                    self.add_variant_field(vfn, field_set, &set)?;
                 }
             }
             _ => (),
@@ -377,11 +373,75 @@ impl CheckState {
                 // resign?
                 Ok(Element::Record(assignations))
             }
-            Element::Project { .. } => {
-                Err(CheckError::Unimplemented("element project".to_string()))
+            Element::Project {
+                element: inner,
+                field,
+            } => {
+                // globally unique projections mean we know what the sets going
+                // in and out must be
+                let Some(SetField {
+                    field_set,
+                    owner_set,
+                }) = self.record_fields.get(field)
+                else {
+                    return Err(CheckError::Unbound(field.clone()));
+                };
+
+                // enforce the correct typing of the claimed result
+                if !self.set_equal(set, field_set) {
+                    return Err(CheckError::WrongSetForElement(
+                        set.clone(),
+                        field_set.clone(),
+                    ));
+                }
+
+                // enforce the correct typing of the element
+                let inner = self.check_element(inner, owner_set)?;
+
+                // Unfortunately we still have to do something nasty here to obtain the data
+                let Element::Record(assignations) = inner else {
+                    panic!("invariant violation: check_element returned non-record for record set");
+                };
+                let sub_element = assignations
+                    .into_iter()
+                    .find(|a| a.name == *field)
+                    .expect("invariant violation: record missing field that was type-checked")
+                    .element
+                    .clone();
+
+                Ok(sub_element)
+            }
+            Element::Inject {
+                element: inner,
+                field,
+            } => {
+                // globally unique injections mean that we know what the sets
+                // going in and out must be, but compared to projections their
+                // roles are here interchanged
+                let Some(SetField {
+                    field_set,
+                    owner_set,
+                }) = self.variant_fields.get(field)
+                else {
+                    return Err(CheckError::Unbound(field.clone()));
+                };
+
+                // enforce the correct typing of the claimed result
+                if !self.set_equal(set, owner_set) {
+                    return Err(CheckError::WrongSetForElement(
+                        set.clone(),
+                        owner_set.clone(),
+                    ));
+                }
+
+                // enforce the correct typing of the element
+                let element = self.check_element(inner, field_set)?;
+
+                Ok(Element::Inject {
+                    element: Box::new(element),
+                    field: field.clone(),
+                })
             }
-            Element::Inject { .. } => Err(CheckError::Unimplemented("element inject".to_string())),
-            Element::App(_, _) => Err(CheckError::Unimplemented("element app".to_string())),
             Element::Case { .. } => Err(CheckError::Unimplemented("element case".to_string())),
         }
     }
diff --git a/src/main.rs b/src/main.rs
index e389983..f7ad1c1 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -22,10 +22,16 @@ let set Y = X
 
 let set Z = record { .y : Y }
 
+let set W = variant [ z. : Z | f. : Float ]
+
 let element x : X = { .b = true, .n = 41 }
 
 let element z : Z = { .y = x }
 
+let element the_nat : Nat = z .y .n
+
+let element w : W = f. 1.44
+
 // let signature Graph = theory {
 //     .Node :: Set,
 //     .Edge :: (s : Node) (t : Node) -> Set
diff --git a/src/parser.rs b/src/parser.rs
index 8b75c2c..5dd777b 100644
--- a/src/parser.rs
+++ b/src/parser.rs
@@ -120,7 +120,7 @@ parser! {
 
         rule set() -> Set
         = kw_record()  _ "{" fs:(set_field() ** ",") _ "}" { Set::Record(fs) }
-        / kw_variant() _ "{" _ vs:(variant_field() ** "|") "}" { Set::Variant(vs) }
+        / kw_variant() _ "[" _ vs:(variant_field() ** "|") "]" { Set::Variant(vs) }
         / b:builtin() { Set::BuiltIn(b) }
         / i:claimed_set() { Set::ClaimedSet(i) }
         / v:set_var() { Set::Var(v) }
@@ -165,20 +165,12 @@ parser! {
             })
         }
 
-        rule app_elem() -> Element
-        = head:dot_elem() tail:(__ d:dot_elem() { d })*
-        {
-            tail.into_iter().fold(head, |acc, a| {
-                Element::App(Box::new(acc), Box::new(a))
-            })
-        }
-
         rule case_arm() -> CaseArm
         = t:inject() _ x:elem_var() _ "=>" _ body:element() { CaseArm { tag: t, bound: x, body } }
 
         rule element() -> Element
         = kw_case() __ scrut:element() _ kw_of() _ "{" arms:(_ a:case_arm() _ { a }) ** "|"  _ "}" { Element::Case { scrutinee: Box::new(scrut), arms } }
-        / app_elem()
+        / d:dot_elem() { d }
 
         // instance layer
 
@@ -258,10 +250,10 @@ let set Config = record {
     .label   : Str
 }
 
-let set Maybe = variant {
+let set Maybe = variant [
     none. : record {}
   | some. : Config
-}
+]
         "#;
 
         debug_parse(src);