computing cases

5 files changed, 151 insertions, 62 deletions

diff --git a/src/checker.rs b/src/checker.rs
index 7a7f4d4..3ebcb4d 100644
--- a/src/checker.rs
+++ b/src/checker.rs
@@ -1,23 +1,22 @@
 use crate::ast::*;
-use crate::check_state::{CheckError, CheckState};
+use crate::checker_state::{CheckerError, CheckerState};
 
 use tracing::{debug, instrument};
 
 impl Programme {
-    pub fn check(&self) -> Result<(), CheckError> {
-        let mut state = CheckState::default();
+    pub fn check(&self) -> Result<(), CheckerError> {
+        let mut state = CheckerState::default();
         state.check(self)
     }
 }
 
-impl CheckState {
+impl CheckerState {
     #[instrument(skip(self, prog), level = "debug")]
-    pub fn check(&mut self, prog: &Programme) -> Result<(), CheckError> {
+    pub fn check(&mut self, prog: &Programme) -> Result<(), CheckerError> {
         let Programme(decls) = prog;
 
         for decl in decls {
-            debug!(%self);
-            debug!(%decl);
+            debug!(%self, %decl);
             match decl {
                 Decl::Set { name, set } => {
                     let set = self.check_set(set)?;
@@ -27,17 +26,17 @@ impl CheckState {
                 Decl::Element { name, element, set } => {
                     let set = self.check_set(set)?;
                     let element = self.check_element(element, &set)?;
-                    self.add_element(name, element, set)
+                    self.add_element(name.clone(), element, set)
                 }
                 Decl::Signature { .. } => {
-                    return Err(CheckError::Unimplemented("signatures".to_string()));
+                    return Err(CheckerError::Unimplemented("signatures".to_string()));
                 }
                 Decl::Instance { .. } => {
-                    return Err(CheckError::Unimplemented("instances".to_string()));
+                    return Err(CheckerError::Unimplemented("instances".to_string()));
                 }
             }?;
         }
-        debug!(%self, "END");
+        debug!(%self);
         Ok(())
     }
 }
diff --git a/src/set_checker.rs b/src/checker_set.rs
index 5762d9c..a14ac9a 100644
--- a/src/set_checker.rs
+++ b/src/checker_set.rs
@@ -1,12 +1,12 @@
 use crate::ast::*;
-use crate::check_state::*;
+use crate::checker_state::*;
 
 use std::iter::zip;
 use tracing::instrument;
 
-impl CheckState {
+impl CheckerState {
     #[instrument(skip(self), level = "debug", fields(%set))]
-    pub fn check_set(&self, set: &Set) -> Result<Set, CheckError> {
+    pub fn check_set(&self, set: &Set) -> Result<Set, CheckerError> {
         match set {
             Set::BuiltIn(_) => Ok(set.clone()),
             Set::Record(fields) => {
@@ -35,7 +35,7 @@ impl CheckState {
                     .collect::<Result<Vec<_>, _>>()?;
                 Ok(Set::Variant(fields))
             }
-            Set::ClaimedSet(_) => Err(CheckError::Unimplemented("instances as sets".to_string())),
+            Set::ClaimedSet(_) => Err(CheckerError::Unimplemented("instances as sets".to_string())),
             Set::Var(v) => {
                 let deref = self.lookup_set(v)?;
                 Ok(deref.clone())
@@ -43,16 +43,16 @@ impl CheckState {
         }
     }
 
-    fn _check_literal_set_helper(&self, claimed: &Set, should_be: Set) -> Result<(), CheckError> {
+    fn _check_literal_set_helper(&self, claimed: &Set, should_be: Set) -> Result<(), CheckerError> {
         if !self.set_equal(claimed, &should_be) {
-            Err(CheckError::WrongSetForElement(claimed.clone(), should_be))
+            Err(CheckerError::WrongSetForElement(claimed.clone(), should_be))
         } else {
             Ok(())
         }
     }
 
     #[instrument(skip(self), level = "debug", fields(%element, %set))]
-    pub fn check_element(&self, element: &Element, set: &Set) -> Result<Element, CheckError> {
+    pub fn check_element(&self, element: &Element, set: &Set) -> Result<Element, CheckerError> {
         match element {
             Element::Literal(lit) => {
                 // we may infer the type from the element
@@ -80,7 +80,7 @@ impl CheckState {
                 // we have previously done the work to discover the type of
                 // this element, so what we're claiming now must match!
                 if !self.set_equal(set, &lookup.set) {
-                    return Err(CheckError::WrongSetForElement(
+                    return Err(CheckerError::WrongSetForElement(
                         set.clone(),
                         lookup.set.clone(),
                     ));
@@ -88,7 +88,7 @@ impl CheckState {
                 Ok(lookup.element.clone())
             }
             Element::Record(assignations) => {
-                let rej = |reason| CheckError::ElementDoesNotBelong {
+                let rej = |reason| CheckerError::ElementDoesNotBelong {
                     element: element.clone(),
                     claimed: set.clone(),
                     reason,
@@ -149,7 +149,7 @@ impl CheckState {
 
                 // enforce the correct typing of the claimed result
                 if !self.set_equal(set, field_set) {
-                    return Err(CheckError::WrongSetForElement(
+                    return Err(CheckerError::WrongSetForElement(
                         set.clone(),
                         field_set.clone(),
                     ));
@@ -185,7 +185,7 @@ impl CheckState {
 
                 // enforce the correct typing of the claimed result
                 if !self.set_equal(set, owner_set) {
-                    return Err(CheckError::WrongSetForElement(
+                    return Err(CheckerError::WrongSetForElement(
                         set.clone(),
                         owner_set.clone(),
                     ));
@@ -199,7 +199,85 @@ impl CheckState {
                     field: field.clone(),
                 })
             }
-            Element::Case { .. } => Err(CheckError::Unimplemented("element case".to_string())),
+            Element::Case { arms, scrutinee } => {
+                // TODO: do we allow mapping out of bottom?
+                if arms.is_empty() {
+                    return Err(CheckerError::Unimplemented(
+                        "mapping out of bottom types".to_string(),
+                    ));
+                }
+
+                // 1. Syntactic checks
+                // -------------------
+                // arms agree on the set to which the scrutinee should belong
+                let arm_owners = arms
+                    .iter()
+                    .map(|ca| self.lookup_variant_field(&ca.tag).map(|sf| &sf.owner_set))
+                    .collect::<Result<Vec<_>, _>>()?;
+                let owner = arm_owners[0]; // safe because of the above decision about bottom
+                if !arm_owners.iter().all(|o| self.set_equal(owner, o)) {
+                    return Err(CheckerError::IncosistentCaseScrutineeSet(element.clone()));
+                }
+
+                // all cases are handled
+                let Set::Variant(fields) = owner else {
+                    panic!(
+                        "invariant violation: looking up the owner of a variant field resulted in a non-variant set",
+                    )
+                };
+                let mut required_field_names_sorted: Vec<String> =
+                    fields.iter().map(|vf| vf.name.clone()).collect();
+                required_field_names_sorted.sort();
+                let mut covered_field_names_sorted: Vec<String> =
+                    arms.iter().map(|ca| ca.tag.clone()).collect();
+                covered_field_names_sorted.sort();
+                if required_field_names_sorted != covered_field_names_sorted {
+                    return Err(CheckerError::IncompleteCaseAnalysis {
+                        found: covered_field_names_sorted,
+                        required: required_field_names_sorted,
+                    });
+                }
+
+                // 2. semantic checks
+                // ------------------
+
+                // scrutinee must be of the same set that all the arms are
+                // implying, in particular this implies that the following holds
+                // `inner : self.lookup_variant_field(field).field_set`
+                let scrutinee = self.check_element(scrutinee, owner)?;
+
+                // which variant are we?
+                let Element::Inject {
+                    field,
+                    element: inner,
+                } = scrutinee
+                else {
+                    panic!(
+                        "invariant violation: we believe element is of a variant set but it's not an injection"
+                    );
+                };
+
+                // TODO: we would like to check that each arm is correct, but
+                // there's no easy way to do this? we can insert hypothetical
+                // elements of the correct type into the checkerstate, but if
+                // the body exacts non-trivial computation we won't be to pass
+                // further checks. In the future would could build first class
+                // support for hypothetical elements and do proper bi-di
+                // checking, but for now we only check the branch that matters.
+
+                let CaseArm { tag, bound, body } = arms.iter().find(|ca| ca.tag == field).expect("invariant violation: we know that all cases are covered and that the element is of the valid type");
+                let SetField { field_set, .. } = self.lookup_variant_field(tag)?;
+                // TODO: if we were worried about overhead we'd have a separate
+                // locals stack, though truly if we were worried about overhead
+                // we'd not have NNN instances of clone elsewhere in the
+                // codebase and we wouldn't be eagerly evaluating all
+                // expressions fully.
+                let mut new_context = self.clone();
+                new_context.add_element(bound.clone(), *inner.clone(), field_set.clone())?;
+                let computed = new_context.check_element(body, set)?;
+
+                Ok(computed)
+            }
         }
     }
 }
diff --git a/src/check_state.rs b/src/checker_state.rs
index d775993..c4b4a3a 100644
--- a/src/check_state.rs
+++ b/src/checker_state.rs
@@ -6,7 +6,7 @@ use std::collections::HashMap;
 use std::fmt;
 
 #[derive(Display)]
-pub enum CheckError {
+pub enum CheckerError {
     #[display("Unbound: {_0}")]
     Unbound(String),
     #[display("Rebinding: {_0}")]
@@ -21,24 +21,34 @@ pub enum CheckError {
         claimed: Set,
         reason: String,
     },
+    #[display("Case analysis {_0} does not have consistent set for scrutinee")]
+    IncosistentCaseScrutineeSet(Element),
+    #[display("Incomplete case analysis: covered [{}] but required [{}]",
+        found.join(", "),
+        required.join(", ")
+    )]
+    IncompleteCaseAnalysis {
+        found: Vec<String>,
+        required: Vec<String>,
+    },
 }
 
-#[derive(Display)]
+#[derive(Display, Clone)]
 #[display("{field_set} @ {owner_set}")]
 pub struct SetField {
     pub field_set: Set,
     pub owner_set: Set,
 }
 
-#[derive(Display)]
+#[derive(Display, Clone)]
 #[display("{element} : {set}")]
 pub struct CheckedElement {
     pub element: Element,
     pub set: Set,
 }
 
-#[derive(Default)]
-pub struct CheckState {
+#[derive(Default, Clone)]
+pub struct CheckerState {
     wf_sets: HashMap<String, Set>,
     wf_elements: HashMap<String, CheckedElement>,
     wf_signatures: HashMap<String, Signature>,
@@ -47,37 +57,37 @@ pub struct CheckState {
     variant_fields: HashMap<String, SetField>,
 }
 
-impl fmt::Display for CheckState {
+impl fmt::Display for CheckerState {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
         fn section<K, V>(f: &mut fmt::Formatter<'_>, name: &str, map: &HashMap<K, V>) -> fmt::Result
         where
             K: fmt::Display + Ord,
             V: fmt::Display,
         {
-            write!(f, " {name} = {{")?;
+            writeln!(f, "  {name} = {{")?;
             let mut entries: Vec<_> = map.iter().collect();
             entries.sort_by(|a, b| a.0.cmp(b.0));
             for (k, v) in entries {
-                write!(f, "{k} ~> {v}, ")?;
+                writeln!(f, "    {k} ~> {v},")?;
             }
-            write!(f, "}},")
+            writeln!(f, "  }},")
         }
 
-        write!(f, "CheckState {{")?;
+        writeln!(f, "CheckState {{")?;
         section(f, "sets", &self.wf_sets)?;
         section(f, "elements", &self.wf_elements)?;
         section(f, "record_fields", &self.record_fields)?;
         section(f, "variant_fields", &self.variant_fields)?;
         section(f, "signatures", &self.wf_signatures)?;
         section(f, "instances", &self.wf_instances)?;
-        write!(f, " }}")?;
+        writeln!(f, " }}")?;
         Ok(())
     }
 }
 
 // The invariant we're maintaining is that everything is fully evaluated before
 // we commit it to be stored in the state.
-impl CheckState {
+impl CheckerState {
     // Because of our invariant we don't actually need to do anything
     // non-trivial here.
     #[instrument(skip(self), level = "debug", fields(%set_a, %set_b))]
@@ -86,18 +96,18 @@ impl CheckState {
     }
 
     #[instrument(skip(self), level = "debug")]
-    fn assert_unbound_set(&self, name: &String) -> Result<(), CheckError> {
+    fn assert_unbound_set(&self, name: &String) -> Result<(), CheckerError> {
         if self.wf_sets.contains_key(name) {
-            Err(CheckError::Rebinding(name.clone()))
+            Err(CheckerError::Rebinding(name.clone()))
         } else {
             Ok(())
         }
     }
 
     #[instrument(skip(self), level = "debug")]
-    fn assert_unbound_element(&self, name: &String) -> Result<(), CheckError> {
+    fn assert_unbound_element(&self, name: &String) -> Result<(), CheckerError> {
         if self.wf_elements.contains_key(name) {
-            Err(CheckError::Rebinding(name.clone()))
+            Err(CheckerError::Rebinding(name.clone()))
         } else {
             Ok(())
         }
@@ -109,9 +119,9 @@ impl CheckState {
         name: &String,
         set_ref: &SetField,
         belongs_to: &Set,
-    ) -> Result<(), CheckError> {
+    ) -> Result<(), CheckerError> {
         if !self.set_equal(&set_ref.owner_set, belongs_to) {
-            Err(CheckError::Rebinding(name.clone()))
+            Err(CheckerError::Rebinding(name.clone()))
         } else {
             Ok(())
         }
@@ -123,7 +133,7 @@ impl CheckState {
         name: &String,
         field_set: &Set,
         owner_set: &Set,
-    ) -> Result<(), CheckError> {
+    ) -> Result<(), CheckerError> {
         if let Some(set_ref) = self.record_fields.get(name) {
             self.assert_correct_owner(name, set_ref, owner_set)?;
         };
@@ -143,7 +153,7 @@ impl CheckState {
         name: &String,
         field_set: &Set,
         owner_set: &Set,
-    ) -> Result<(), CheckError> {
+    ) -> Result<(), CheckerError> {
         if let Some(set_ref) = self.variant_fields.get(name) {
             self.assert_correct_owner(name, set_ref, owner_set)?;
         };
@@ -158,7 +168,7 @@ impl CheckState {
     }
 
     #[instrument(skip(self), level = "debug", fields(%name, %set))]
-    pub fn add_set(&mut self, name: &String, set: Set) -> Result<(), CheckError> {
+    pub fn add_set(&mut self, name: &String, set: Set) -> Result<(), CheckerError> {
         self.assert_unbound_set(name)?;
         match &set {
             Set::Record(fields) => {
@@ -187,37 +197,37 @@ impl CheckState {
 
     pub fn add_element(
         &mut self,
-        name: &String,
+        name: String,
         element: Element,
         set: Set,
-    ) -> Result<(), CheckError> {
-        self.assert_unbound_element(name)?;
+    ) -> Result<(), CheckerError> {
+        self.assert_unbound_element(&name)?;
         self.wf_elements
-            .insert(name.clone(), CheckedElement { element, set });
+            .insert(name, CheckedElement { element, set });
         Ok(())
     }
 
-    pub fn lookup_set(&self, name: &String) -> Result<&Set, CheckError> {
+    pub fn lookup_set(&self, name: &String) -> Result<&Set, CheckerError> {
         self.wf_sets
             .get(name)
-            .map_or(Err(CheckError::Unbound(name.clone())), Ok)
+            .map_or(Err(CheckerError::Unbound(name.clone())), Ok)
     }
 
-    pub fn lookup_element(&self, name: &String) -> Result<&CheckedElement, CheckError> {
+    pub fn lookup_element(&self, name: &String) -> Result<&CheckedElement, CheckerError> {
         self.wf_elements
             .get(name)
-            .map_or(Err(CheckError::Unbound(name.clone())), Ok)
+            .map_or(Err(CheckerError::Unbound(name.clone())), Ok)
     }
 
-    pub fn lookup_record_field(&self, name: &String) -> Result<&SetField, CheckError> {
+    pub fn lookup_record_field(&self, name: &String) -> Result<&SetField, CheckerError> {
         self.record_fields
             .get(name)
-            .map_or(Err(CheckError::Unbound(name.clone())), Ok)
+            .map_or(Err(CheckerError::Unbound(name.clone())), Ok)
     }
 
-    pub fn lookup_variant_field(&self, name: &String) -> Result<&SetField, CheckError> {
+    pub fn lookup_variant_field(&self, name: &String) -> Result<&SetField, CheckerError> {
         self.variant_fields
             .get(name)
-            .map_or(Err(CheckError::Unbound(name.clone())), Ok)
+            .map_or(Err(CheckerError::Unbound(name.clone())), Ok)
     }
 }
diff --git a/src/main.rs b/src/main.rs
index df36027..c57eef6 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -1,8 +1,8 @@
 mod ast;
-mod check_state;
 mod checker;
+mod checker_set;
+mod checker_state;
 mod parser;
-mod set_checker;
 
 use tracing_subscriber::{layer::SubscriberExt, util::SubscriberInitExt};
 use tracing_tree::HierarchicalLayer;
@@ -32,7 +32,9 @@ let element z : Z = { .y = x }
 
 let element the_nat : Nat = z .y .n
 
-let element w : W = f. 1.44
+let element injected : W = z. z
+
+let element compute : Nat = case injected of [ z. myz => myz .y .n | f. myf => 2 ]
 
 // let signature Graph = theory {
 //     .Node :: Set,
diff --git a/src/parser.rs b/src/parser.rs
index 5dd777b..958f09d 100644
--- a/src/parser.rs
+++ b/src/parser.rs
@@ -169,7 +169,7 @@ parser! {
         = 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 } }
+        = kw_case() __ scrut:element() _ kw_of() _ "[" arms:(_ a:case_arm() _ { a }) ** "|"  _ "]" { Element::Case { scrutinee: Box::new(scrut), arms } }
         / d:dot_elem() { d }
 
         // instance layer
@@ -263,10 +263,10 @@ let set Maybe = variant [
     fn test_elements() {
         let src = r#"
             let element foo : Nat =
-                case some. config .count of {
+                case some. config .count of [
                     none. ignore => 0
                   | some. n => n
-                }
+                ]
         "#;
 
         debug_parse(src);