prepare for more work on signatures, in particular this means processing records in telescoped contexts

rework ElementValue, CheckedElement to be type aliases for the generic version over Term : Type

4 files changed, 100 insertions, 54 deletions

diff --git a/src/checker_set.rs b/src/checker_set.rs
index 2faca9e..7ff6e4a 100644
--- a/src/checker_set.rs
+++ b/src/checker_set.rs
@@ -10,10 +10,16 @@ impl CheckerState {
         match set {
             Set::BuiltIn(_) => Ok(set.clone()),
             Set::Record(fields) => {
+                let mut ctx = self.clone();
                 let fields = fields
                     .into_iter()
                     .map(|RecordField { name, set }| {
-                        let set = self.check_set(set)?;
+                        let set = ctx.check_set(set)?;
+                        ctx.add_element(
+                            name.clone(),
+                            Value::Hypothetical(set.clone()),
+                            set.clone(),
+                        )?;
                         Ok(RecordField { name, set })
                     })
                     .collect::<Result<Vec<_>, _>>()?;
@@ -68,7 +74,7 @@ impl CheckerState {
             // hypothetical from a call to check_element, in the context of
             // check_element, we can safely ignore its payload. I'll point this
             // out later as (*)
-            ElementValue::Hypothetical(ref h_set) => {
+            Value::Hypothetical(ref h_set) => {
                 if !self.equal(set, &h_set) {
                     Err(CheckerError::WrongSetForElement {
                         value: value.clone(),
@@ -79,7 +85,7 @@ impl CheckerState {
                     Ok(value)
                 }
             }
-            ElementValue::Concrete(ref element @ Element::Literal(ref lit)) => {
+            Value::Concrete(ref element @ Element::Literal(ref lit)) => {
                 let value = value.clone();
                 // we may infer the type from the element
                 match lit {
@@ -101,20 +107,20 @@ impl CheckerState {
                 }
                 Ok(element.clone().into())
             }
-            ElementValue::Concrete(Element::Var(ref v)) => {
+            Value::Concrete(Element::Var(ref v)) => {
                 let lookup = self.lookup_element(&v)?;
                 // we have previously done the work to discover the type of
                 // this element, so what we're claiming now must match!
-                if !self.equal(set, &lookup.set) {
+                if !self.equal(set, &lookup.container) {
                     return Err(CheckerError::WrongSetForElement {
                         value: value.clone(),
                         claimed: set.clone(),
-                        real: lookup.set.clone(),
+                        real: lookup.container.clone(),
                     });
                 }
                 Ok(lookup.value.clone())
             }
-            ElementValue::Concrete(ref concrete @ Element::Record(ref assignations)) => {
+            Value::Concrete(ref concrete @ Element::Record(ref assignations)) => {
                 let rej = |reason| CheckerError::ElementDoesNotBelong {
                     element: concrete.clone(),
                     claimed: set.clone(),
@@ -159,18 +165,18 @@ impl CheckerState {
                 // rebuild, hypotheticals are contagious
                 let assignations = zip(element_fnames, sub_els)
                     .map(|(name, element)| match element {
-                        ElementValue::Concrete(element) => Some(ElemAssign { name, element }),
-                        ElementValue::Hypothetical(_) => None,
+                        Value::Concrete(element) => Some(ElemAssign { name, element }),
+                        Value::Hypothetical(_) => None,
                     })
                     .collect();
                 // resign?
                 Ok(if let Some(assignations) = assignations {
                     Element::Record(assignations).into()
                 } else {
-                    ElementValue::Hypothetical(set.clone())
+                    Value::Hypothetical(set.clone())
                 })
             }
-            ElementValue::Concrete(Element::Project {
+            Value::Concrete(Element::Project {
                 element: ref inner,
                 ref field,
             }) => {
@@ -193,7 +199,7 @@ impl CheckerState {
                 // enforce the correct typing of the element
                 let inner = self.check_element((*inner.clone()).into(), owner_set)?;
                 match inner {
-                    ElementValue::Concrete(inner) => {
+                    Value::Concrete(inner) => {
                         // Unfortunately we still have to do something nasty here to obtain the data
                         let Element::Record(assignations) = inner else {
                             panic!(
@@ -212,10 +218,10 @@ impl CheckerState {
                         Ok(sub_element.into())
                     }
                     // correct by (*)
-                    ElementValue::Hypothetical(_) => Ok(ElementValue::Hypothetical(set.clone())),
+                    Value::Hypothetical(_) => Ok(Value::Hypothetical(set.clone())),
                 }
             }
-            ElementValue::Concrete(Element::Inject {
+            Value::Concrete(Element::Inject {
                 element: ref inner,
                 ref field,
             }) => {
@@ -240,16 +246,16 @@ impl CheckerState {
                 let element = self.check_element((*inner.clone()).into(), field_set)?;
 
                 match element {
-                    ElementValue::Concrete(element) => Ok(Element::Inject {
+                    Value::Concrete(element) => Ok(Element::Inject {
                         element: Box::new(element),
                         field: field.clone(),
                     }
                     .into()),
                     // correct by (*)
-                    ElementValue::Hypothetical(_) => Ok(ElementValue::Hypothetical(set.clone())),
+                    Value::Hypothetical(_) => Ok(Value::Hypothetical(set.clone())),
                 }
             }
-            ElementValue::Concrete(
+            Value::Concrete(
                 ref element @ Element::Case {
                     ref arms,
                     ref scrutinee,
@@ -303,8 +309,8 @@ impl CheckerState {
 
                 // which variant are we, if any
                 let matching: Option<(String, Element)> = match scrutinee {
-                    ElementValue::Hypothetical(_) => None,
-                    ElementValue::Concrete(Element::Inject {
+                    Value::Hypothetical(_) => None,
+                    Value::Concrete(Element::Inject {
                         field,
                         element: inner,
                     }) => Some((field, *inner)),
@@ -348,13 +354,13 @@ impl CheckerState {
                     } else {
                         new_context.add_element(
                             binding_name,
-                            ElementValue::Hypothetical(field_set.clone()),
+                            Value::Hypothetical(field_set.clone()),
                             binding_set,
                         )?;
                         new_context.check_element(arm.body.clone().into(), set)?;
                     };
                 }
-                Ok(computed_output.unwrap_or(ElementValue::Hypothetical(set.clone())))
+                Ok(computed_output.unwrap_or(Value::Hypothetical(set.clone())))
             }
         }
     }
diff --git a/src/checker_signature.rs b/src/checker_signature.rs
index 4fa723f..4d5f02c 100644
--- a/src/checker_signature.rs
+++ b/src/checker_signature.rs
@@ -12,14 +12,20 @@ impl CheckerState {
                 let deref = self.lookup_signature(&v)?;
                 Ok(deref.clone())
             }
-            Signature::Ext { params, codomain } => Err(CheckerError::Unimplemented(
+            Signature::Ext { .. } => Err(CheckerError::Unimplemented(
                 "extension signatures".to_string(),
             )),
             Signature::Theory(fields) => {
+                let mut ctx = self.clone();
                 let fields = fields
                     .into_iter()
                     .map(|SigField { signature, name }| {
-                        let signature = self.check_signature(signature)?;
+                        let signature = ctx.check_signature(signature)?;
+                        ctx.add_instance(
+                            name.clone(),
+                            InstanceValue::Hypothetical(signature.clone()),
+                            signature.clone(),
+                        )?;
                         Ok(SigField { name, signature })
                     })
                     .collect::<Result<Vec<_>, _>>()?;
diff --git a/src/checker_state.rs b/src/checker_state.rs
index 31c3bde..a14a6e4 100644
--- a/src/checker_state.rs
+++ b/src/checker_state.rs
@@ -37,6 +37,8 @@ pub enum CheckerError {
     },
 }
 
+// -----------------------------------------------------------------------------
+// Generics for wrapping fields, values, and coercing them
 #[derive(Display, Clone)]
 #[display("{field} @ {owner}")]
 pub struct Field<T: std::fmt::Display> {
@@ -45,31 +47,45 @@ pub struct Field<T: std::fmt::Display> {
 }
 
 #[derive(Display, Clone)]
-pub enum ElementValue {
-    Concrete(Element),
+pub enum Value<Term: std::fmt::Display, Type: std::fmt::Display> {
+    Concrete(Term),
     #[display("_ : {_0}")]
-    Hypothetical(Set),
+    Hypothetical(Type),
+}
+
+pub type ElementValue = Value<Element, Set>;
+pub type InstanceValue = Value<Instance, Signature>;
+
+impl From<Element> for Value<Element, Set> {
+    fn from(e: Element) -> Value<Element, Set> {
+        Value::Concrete(e)
+    }
 }
 
-impl From<Element> for ElementValue {
-    fn from(e: Element) -> ElementValue {
-        ElementValue::Concrete(e)
+impl From<Instance> for Value<Instance, Signature> {
+    fn from(i: Instance) -> Value<Instance, Signature> {
+        Value::Concrete(i)
     }
 }
 
 #[derive(Display, Clone)]
-#[display("{value} : {set}")]
-pub struct CheckedElement {
-    pub value: ElementValue,
-    pub set: Set,
+#[display("{value} : {container}")]
+pub struct Checked<Term: std::fmt::Display, Type: std::fmt::Display> {
+    pub value: Value<Term, Type>,
+    pub container: Type,
 }
 
+pub type CheckedElement = Checked<Element, Set>;
+pub type CheckedInstance = Checked<Instance, Signature>;
+
+// -----------------------------------------------------------------------------
+// The checker state
 #[derive(Default, Clone)]
 pub struct CheckerState {
     wf_sets: HashMap<String, Set>,
     wf_elements: HashMap<String, CheckedElement>,
     wf_signatures: HashMap<String, Signature>,
-    wf_instances: HashMap<String, Instance>,
+    wf_instances: HashMap<String, CheckedInstance>,
     record_fields: HashMap<String, Field<Set>>,
     variant_fields: HashMap<String, Field<Set>>,
     signature_fields: HashMap<String, Field<Signature>>,
@@ -239,15 +255,15 @@ impl CheckerState {
     pub fn add_element(
         &mut self,
         name: String,
-        element: ElementValue,
+        element: Value<Element, Set>,
         set: Set,
     ) -> Result<(), CheckerError> {
         self.assert_unbound_element(&name)?;
         self.wf_elements.insert(
             name,
-            CheckedElement {
+            Checked {
                 value: element,
-                set,
+                container: set,
             },
         );
         Ok(())
@@ -344,6 +360,24 @@ impl CheckerState {
         Ok(())
     }
 
+    #[instrument(skip(self), level = "debug", fields(%name, %instance, %signature))]
+    pub fn add_instance(
+        &mut self,
+        name: String,
+        instance: InstanceValue,
+        signature: Signature,
+    ) -> Result<(), CheckerError> {
+        self.assert_unbound_element(&name)?;
+        self.wf_instances.insert(
+            name,
+            Checked {
+                value: instance,
+                container: signature,
+            },
+        );
+        Ok(())
+    }
+
     pub fn lookup_signature(&self, name: &String) -> Result<&Signature, CheckerError> {
         self.wf_signatures
             .get(name)
diff --git a/src/main.rs b/src/main.rs
index 2b798e1..7d04891 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -19,35 +19,35 @@ fn main() {
 
     let src = r#"
 
-let set X = record { .b : Bool, .n : Nat } // basic
-
+// let X be the set Y, call it Z
+let set X = record { .b : Bool, .n : Nat }
 let set Y = X
-
 let set Z = record { .y : Y }
-
-let set W = variant [ z. : Z | f. : Float ]
-
+// make some elements
 let element x : X = { .b = true, .n = 41 }
-
 let element z : Z = { .y = x }
+// exercise case matching
+let set Z_or_Float = variant [ z. : Z | f. : Float ]
+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 element the_nat : Nat = z .y .n
-
-let element injected : W = z. z
-
-let element compute : Nat = case injected of [ z. myz => myz .y .n | f. myf => myf ]
+let signature Graph = theory {
+    .Node :: Set,
+    .Edge :: (s : Node) (t : Node) -> Set
+}
 
-// 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-of(natPoset .Node) = 7
+//
+// let set NatEdges = record {
+//   .source: set-of(natPoset .Node),
+//   .target: set-of(natPoset .Node),
+//   .connected set-of(natPoset .Edge source target)
+// }
 "#;
     let programme = parser::parser::program(src);