aboutsummaryrefslogtreecommitdiff
path: root/src/checker.rs
diff options
context:
space:
mode:
Diffstat (limited to 'src/checker.rs')
-rw-r--r--src/checker.rs198
1 files changed, 170 insertions, 28 deletions
diff --git a/src/checker.rs b/src/checker.rs
index f3221d9..5f01a7d 100644
--- a/src/checker.rs
+++ b/src/checker.rs
@@ -2,8 +2,9 @@ use crate::ast::*;
use tracing::{debug, instrument};
use derive_more::Display;
-use std::collections::HashMap;
+use std::collections::{HashMap, HashSet};
use std::fmt;
+use std::iter::zip;
impl Programme {
pub fn check(&self) -> Result<(), CheckError> {
@@ -20,23 +21,38 @@ pub enum CheckError {
Rebinding(String),
#[display("The following functionality is unimplemented: {_0}")]
Unimplemented(String),
+ #[display("Element claimed to belong to {_0} but actually belongs to {_1}")]
+ WrongSetForElement(Set, Set),
+ #[display("Element {element} does belong to set {claimed}: {reason}")]
+ ElementDoesNotBelong {
+ element: Element,
+ claimed: Set,
+ reason: String,
+ },
}
-#[derive(Debug, Display)]
-#[display("{set} @ {belongs_to}")]
-struct SetRef {
- set: Set,
+#[derive(Display)]
+#[display("{value} @ {belongs_to}")]
+struct SetField {
+ value: Set,
belongs_to: Set,
}
+#[derive(Display)]
+#[display("{element} : {set}")]
+struct CheckedElement {
+ element: Element,
+ set: Set,
+}
+
#[derive(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>,
+ wf_sets: HashMap<String, Set>,
+ wf_elements: HashMap<String, CheckedElement>,
+ wf_signatures: HashMap<String, Signature>,
+ wf_instances: HashMap<String, Instance>,
+ record_fields: HashMap<String, SetField>,
+ variant_fields: HashMap<String, SetField>,
}
impl fmt::Display for CheckState {
@@ -56,12 +72,12 @@ impl fmt::Display for CheckState {
}
write!(f, "CheckState {{")?;
- section(f, "sets", &self.sets)?;
- section(f, "elements", &self.elements)?;
+ 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.signatures)?;
- section(f, "instances", &self.instances)?;
+ section(f, "signatures", &self.wf_signatures)?;
+ section(f, "instances", &self.wf_instances)?;
write!(f, " }}")?;
Ok(())
}
@@ -70,7 +86,16 @@ impl fmt::Display for CheckState {
impl CheckState {
#[instrument(skip(self), level = "debug")]
fn assert_unbound_set(&self, name: &String) -> Result<(), CheckError> {
- if self.sets.contains_key(name) {
+ if self.wf_sets.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.wf_elements.contains_key(name) {
Err(CheckError::Rebinding(name.clone()))
} else {
Ok(())
@@ -81,11 +106,11 @@ impl CheckState {
fn assert_correct_owner(
&self,
name: &String,
- set_ref: &SetRef,
+ set_ref: &SetField,
belongs_to: &Set,
) -> Result<(), CheckError> {
- let SetRef {
- set: _,
+ let SetField {
+ value: _,
belongs_to: owner,
} = set_ref;
if !self.set_equal(owner, belongs_to) {
@@ -107,8 +132,8 @@ impl CheckState {
};
self.record_fields.insert(
name.clone(),
- SetRef {
- set: set.clone(),
+ SetField {
+ value: set.clone(),
belongs_to: belongs_to.clone(),
},
);
@@ -127,8 +152,8 @@ impl CheckState {
};
self.variant_fields.insert(
name.clone(),
- SetRef {
- set: set.clone(),
+ SetField {
+ value: set.clone(),
belongs_to: belongs_to.clone(),
},
);
@@ -159,7 +184,14 @@ impl CheckState {
}
_ => (),
};
- self.sets.insert(name.clone(), set);
+ self.wf_sets.insert(name.clone(), set);
+ Ok(())
+ }
+
+ fn add_element(&mut self, name: &String, element: Element, set: Set) -> Result<(), CheckError> {
+ self.assert_unbound_element(name)?;
+ self.wf_elements
+ .insert(name.clone(), CheckedElement { element, set });
Ok(())
}
}
@@ -167,7 +199,8 @@ impl CheckState {
// The invariant we're maintaining is that everything is fully evaluated before
// we commit it to be stored in the state.
impl CheckState {
- // Because of our invariant this is fine
+ // 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))]
fn set_equal(&self, set_a: &Set, set_b: &Set) -> bool {
set_a == set_b
@@ -186,8 +219,10 @@ impl CheckState {
self.add_set(name, set)
}
- Decl::Element { .. } => {
- return Err(CheckError::Unimplemented("elements".to_string()));
+ Decl::Element { name, element, set } => {
+ let set = self.check_set(set)?;
+ let element = self.check_element(element, &set)?;
+ self.add_element(name, element, set)
}
Decl::Signature { .. } => {
return Err(CheckError::Unimplemented("signatures".to_string()));
@@ -209,7 +244,7 @@ impl CheckState {
Set::Variant(fields) => self.check_variant(fields),
Set::ClaimedSet(_) => Err(CheckError::Unimplemented("instances as sets".to_string())),
Set::Var(v) => {
- if let Some(deref) = self.sets.get(v) {
+ if let Some(deref) = self.wf_sets.get(v) {
Ok(deref.clone())
} else {
Err(CheckError::Unbound(v.clone()))
@@ -247,4 +282,111 @@ impl CheckState {
.collect::<Result<Vec<_>, _>>()?;
Ok(Set::Variant(fields))
}
+
+ fn _check_literal_set_helper(&self, claimed: &Set, should_be: Set) -> Result<(), CheckError> {
+ if !self.set_equal(claimed, &should_be) {
+ Err(CheckError::WrongSetForElement(claimed.clone(), should_be))
+ } else {
+ Ok(())
+ }
+ }
+
+ #[instrument(skip(self), level = "debug")]
+ fn check_element(&self, element: &Element, set: &Set) -> Result<Element, CheckError> {
+ match element {
+ Element::Literal(lit) => {
+ // we may infer the type from the element
+ match lit {
+ Literal::Int(_) => {
+ self._check_literal_set_helper(set, Set::BuiltIn(BuiltIn::Int))?;
+ }
+ Literal::Nat(_) => {
+ self._check_literal_set_helper(set, Set::BuiltIn(BuiltIn::Nat))?;
+ }
+ Literal::Str(_) => {
+ self._check_literal_set_helper(set, Set::BuiltIn(BuiltIn::Str))?;
+ }
+ Literal::Bool(_) => {
+ self._check_literal_set_helper(set, Set::BuiltIn(BuiltIn::Bool))?;
+ }
+ Literal::Float(_) => {
+ self._check_literal_set_helper(set, Set::BuiltIn(BuiltIn::Float))?;
+ }
+ }
+ Ok(element.clone())
+ }
+ Element::Var(v) => {
+ if let Some(CheckedElement {
+ element: found_element,
+ set: found_set,
+ }) = self.wf_elements.get(v)
+ {
+ // 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, found_set) {
+ return Err(CheckError::WrongSetForElement(
+ set.clone(),
+ found_set.clone(),
+ ));
+ }
+ Ok(found_element.clone())
+ } else {
+ Err(CheckError::Unbound(v.clone()))
+ }
+ }
+ Element::Record(assignations) => {
+ let rej = |reason| CheckError::ElementDoesNotBelong {
+ element: element.clone(),
+ claimed: set.clone(),
+ reason,
+ };
+
+ // make sure we are filling a record
+ let fields = if let Set::Record(fields) = set {
+ Ok(fields)
+ } else {
+ Err(rej("element is a record instance".to_string()))
+ }?;
+
+ let (set_fnames, set_fsets): (Vec<String>, Vec<Set>) = fields
+ .iter()
+ .map(|RecordField { name, set }| (name.clone(), set.clone()))
+ .unzip();
+ let mut set_fnames_sorted = set_fnames.clone();
+ set_fnames_sorted.sort();
+
+ let (element_fnames, element_felements): (Vec<String>, Vec<&Element>) =
+ assignations
+ .iter()
+ .map(|ElemAssign { name, element }| (name.clone(), element))
+ .unzip();
+
+ let mut element_fnames_sorted = element_fnames.clone();
+ element_fnames_sorted.sort();
+
+ if set_fnames_sorted != element_fnames_sorted {
+ return Err(rej(format!(
+ "expected [{}] but found [{}]",
+ set_fnames.join(", "),
+ element_fnames.join(", "),
+ )));
+ }
+
+ // recurse, sets have already been completely expanded
+ let sub_els = zip(element_felements, set_fsets)
+ .map(|(e_f, e_s)| self.check_element(e_f, &e_s))
+ .collect::<Result<Vec<_>, _>>()?;
+ // rebuild
+ let assignations = zip(element_fnames, sub_els)
+ .map(|(name, element)| ElemAssign { name, element })
+ .collect();
+ // resign?
+ Ok(Element::Record(assignations))
+ }
+ Element::Project(_, _) => Err(CheckError::Unimplemented("element project".to_string())),
+ 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())),
+ }
+ }
}
generated by cgit v1.3.1 (git 2.54.0) at 2026-08-30 21:55:35 +0000