wip case for instances

6 files changed, 120 insertions, 7 deletions

diff --git a/src/ast.rs b/src/ast.rs
index d13b2a8..24d5b9b 100644
--- a/src/ast.rs
+++ b/src/ast.rs
@@ -143,6 +143,14 @@ pub struct InstAssign {
 }
 
 #[derive(Clone, PartialEq, Display, Debug)]
+#[display(".{tag} {bound} => {body}")]
+pub struct InstCaseArm {
+    pub tag: String,
+    pub bound: String,
+    pub body: Instance,
+}
+
+#[derive(Clone, PartialEq, Display, Debug)]
 pub enum Instance {
     #[display("({_0} :: Set)")]
     SetCoerce(Box<Set>),
@@ -167,6 +175,12 @@ pub enum Instance {
         instance: Box<Instance>,
         field: String,
     },
+
+    #[display("case {} of {{ {} }}", scrutinee, arms.iter().map(|a| a.to_string()).collect::<Vec<_>>().join(" | "))]
+    Case {
+        scrutinee: Box<Element>,
+        arms: Vec<InstCaseArm>,
+    },
 }
 
 // Declarations
diff --git a/src/checker_set.rs b/src/checker_set.rs
index e12cfb2..87da8bd 100644
--- a/src/checker_set.rs
+++ b/src/checker_set.rs
@@ -259,7 +259,6 @@ impl CheckerState {
                     field: field.clone(),
                 })
             }
-
             Element::Case { arms, scrutinee } => {
                 // TODO: do we allow mapping out of bottom?
                 if arms.is_empty() {
diff --git a/src/checker_signature.rs b/src/checker_signature.rs
index 89f4441..17154dd 100644
--- a/src/checker_signature.rs
+++ b/src/checker_signature.rs
@@ -1,3 +1,5 @@
+// Time-stamp: <2026-04-30 17h19 BST (9561bc0c)>
+
 use crate::ast::*;
 use crate::checker_state::*;
 use std::collections::HashMap;
@@ -101,7 +103,6 @@ impl CheckerState {
                     Ok(Instance::Var(v.clone()))
                 }
             }
-
             Instance::Record(assignations) => {
                 if let Some(signature) = signature {
                     let rej = |reason| CheckerError::InstanceDoesNotBelong {
@@ -219,6 +220,98 @@ impl CheckerState {
                     ),
                 }
             }
+            Instance::Case { scrutinee, arms } => {
+                if arms.is_empty() {
+                    return Err(CheckerError::Unimplemented(
+                        "mapping out of bottom types".to_string(),
+                    ));
+                }
+
+                let arm_owners = arms
+                    .iter()
+                    .map(|ca| self.lookup_variant_field(&ca.tag).map(|sf| &sf.owner))
+                    .collect::<Result<Vec<_>, _>>()?;
+                let owner = arm_owners[0];
+
+                if !arm_owners.into_iter().all(|o| self.equal(owner, o)) {
+                    todo!("inconsistent case scrutinee set");
+                }
+
+                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,
+                    });
+                }
+                let scrutinee = self.check_element(scrutinee, owner)?;
+
+                let matching: Option<(String, Element)> = match scrutinee {
+                    Element::Inject {
+                        ref field,
+                        element: ref inner,
+                    } => Some((field.clone(), *inner.clone())),
+                    Element::Var(_) | Element::Project { .. } | Element::Case { .. } => None,
+                    Element::Literal(_) | Element::Record(_) => panic!(
+                        "invariant violation: scrutinee is a non-variant value at variant set"
+                    ),
+                };
+
+                let mut computed_output = None;
+                let mut processed_arms = Vec::new();
+                for arm in arms {
+                    let Field {
+                        field: field_set, ..
+                    } = self.lookup_variant_field(&arm.tag)?;
+
+                    let mut ctx = self.clone();
+                    let binding_name = arm.bound.clone();
+                    let binding_set = field_set.clone();
+
+                    let case_arm = if let Some((tag, inner)) = &matching
+                        && *tag == arm.tag
+                    {
+                        let canonical =
+                            ctx.make_element_definition(binding_name, inner.clone(), binding_set)?;
+                        let output = ctx.check_instance((&arm.body).into(), signature)?;
+                        if matches!(computed_output, Some(_)) {
+                            panic!(
+                                "invariant violation: we somehow matched multiple arms in case analysis"
+                            )
+                        }
+                        computed_output = Some(output.clone());
+                        InstCaseArm {
+                            tag: arm.tag.clone(),
+                            bound: canonical,
+                            body: output,
+                        }
+                    } else {
+                        let canonical = ctx.make_element_binding(binding_name, binding_set)?;
+                        let body = ctx.check_instance((&arm.body).into(), signature)?;
+                        InstCaseArm {
+                            tag: arm.tag.clone(),
+                            bound: canonical,
+                            body,
+                        }
+                    };
+
+                    processed_arms.push(case_arm);
+                }
+                Ok(computed_output.unwrap_or(Instance::Case {
+                    scrutinee: Box::new(scrutinee),
+                    arms: processed_arms,
+                }))
+            }
             Instance::For {
                 params: inst_params,
                 body,
@@ -372,7 +465,7 @@ impl CheckerState {
                             element: *element.clone(),
                         })
                     }
-                    Instance::Project { .. } | Instance::App(_, _) => {
+                    Instance::Project { .. } | Instance::App(_, _) | Instance::Case { .. } => {
                         // it would appear that we are stuck here, so our only
                         // choice is to continue to be so
                         Ok(Instance::App(Box::new(inner), element.clone()))
diff --git a/src/checker_state.rs b/src/checker_state.rs
index c9be445..a0fe6b1 100644
--- a/src/checker_state.rs
+++ b/src/checker_state.rs
@@ -115,6 +115,7 @@ pub struct CheckerState {
     record_fields: HashMap<String, Field<Set>>,
     variant_fields: HashMap<String, Field<Set>>,
     signature_fields: HashMap<String, Field<Signature>>,
+    // TODO: do we need to make these strictly monotonic somewhere somehow?
     binder_element: usize,
     unique_name: usize,
 }
diff --git a/src/main.rs b/src/main.rs
index 34d6360..a395db8 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -23,9 +23,11 @@ let signature Graph = theory {
     Edge :: (s : set-of(Node)) (t : set-of(Node)) -> Set
 }
 
+let set FinTwo = variant [ zero : record{} | one : record{} ]
+
 let instance natGraph :: Graph = {
-    .Node = Nat :: Set,
-    .Edge = for (s : Nat) (t : Nat), Bool :: Set
+    .Node = FinTwo :: Set,
+    .Edge = for (s : set-of(Node)) (t : set-of(Node)), case s of [ zero. ignore => Bool :: Set | one. ignore => Nat :: Set ]
 }
 
 let set NatEdges = record {
diff --git a/src/parser.rs b/src/parser.rs
index 1aed3f8..d95c190 100644
--- a/src/parser.rs
+++ b/src/parser.rs
@@ -175,6 +175,9 @@ parser! {
 
         // instance layer
 
+        rule inst_case_arm() -> InstCaseArm
+        = t:inject() _ x:elem_var() _ "=>" _ body:instance() { InstCaseArm { tag: t, bound: x, body } }
+
         rule inst_assign() -> InstAssign
         = n:project_upper() _ "=" _ i:instance()
         { InstAssign { name: n, instance: i } }
@@ -183,9 +186,9 @@ parser! {
         = _ s:set() _ "::" _ kw_Set() _ { s }
 
         rule atom_inst() -> Instance
-        = v:inst_var() { Instance::Var(v) }
+        = s:explicit_set_coerce() { Instance::SetCoerce(Box::new(s)) }
+        / v:inst_var() { Instance::Var(v) }
         / f:sig_var() { Instance::Var(f) }
-        / s:explicit_set_coerce() { Instance::SetCoerce(Box::new(s)) }
         / "{" fs:(inst_assign() ** ",") _ "}" { Instance::Record(fs) }
         / "(" _ i:instance() _ ")" { i }
 
@@ -207,6 +210,7 @@ parser! {
 
         rule instance() -> Instance
         = kw_for() __ ps:param_list() _ "," _ body:instance() { Instance::For { params: ps, body: Box::new(body) } }
+        / kw_case() __ scrut:element() _ kw_of() _ "[" arms:(_ a:inst_case_arm() _ { a }) ** "|"  _ "]" { Instance::Case { scrutinee: Box::new(scrut), arms } }
         / app_inst()
 
         // declarations