aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--examples/equality.makkai42
-rw-r--r--src/checker.rs2
-rw-r--r--src/checker_set.rs167
-rw-r--r--src/checker_signature.rs67
-rw-r--r--src/checker_state.rs9
-rw-r--r--src/parser.rs4
6 files changed, 175 insertions, 116 deletions
diff --git a/examples/equality.makkai b/examples/equality.makkai
index ac668c7..5e9a0f9 100644
--- a/examples/equality.makkai
+++ b/examples/equality.makkai
@@ -2,31 +2,37 @@ let set Empty = variant[]
let set Unit = record {}
let element pt : Unit = {}
-let set Three = variant [ zero : Unit | one : Unit | two : Unit ]
+let set Two = variant [ zero : Unit | one : Unit]
let signature SetWithEquivRelation = theory {
Carrier :: Set,
Relation :: (x : set-of(Carrier)) (y: set-of(Carrier)) -> Set,
Reflexive :: (x : set-of(Carrier)) -> <set-of(Relation x x)>,
- Symmetric :: (x : set-of(Carrier)) (y : set-of(Carrier)) (r : set-of(Relation x y)) -> <set-of(Relation y x)>,
- Transitive :: (x : set-of(Carrier)) (y : set-of(Carrier)) (z : set-of(Carrier)) (r : set-of(Relation x y)) (s : set-of(Relation z z)) -> <set-of(Relation y z)>
+ Symmetric :: (x : set-of(Carrier)) (y : set-of(Carrier)) (r : set-of(Relation x y))
+ -> <set-of(Relation y x)>,
+ Transitive :: (x : set-of(Carrier)) (y : set-of(Carrier)) (z : set-of(Carrier))
+ (r : set-of(Relation x y)) (s : set-of(Relation y z))
+ -> <set-of(Relation x z)>
}
-let instance eqThree :: SetWithEquivRelation = {
- .Carrier = Three :: Set,
- .Relation = for (x: Three) (y: Three),
- case x of [ zero. z => case y of [ zero. w => Unit :: Set | one. w => Empty :: Set | two. w => Empty :: Set ]
- | one. z => case y of [ zero. w => Empty :: Set | one. w => Unit :: Set | two. w => Empty :: Set ]
- | two. z => case y of [ zero. w => Empty :: Set | one. w => Empty :: Set | two. w => Unit :: Set ] ],
- .Reflexive = for (x: Three), case x of [ zero. z => <pt> | one. z => <pt> | two. z => <pt> ],
- .Symmetric = for (x: Three) (y: Three) (r: set-of(Relation x y)),
- case x of [ zero. z => case y of [ zero. z => <r> | one. z => <r> | two. z => <r> ]
- | one. z => case y of [ zero. z => <r> | one. z => <r> | two. z => <r> ]
- | two. z => case y of [ zero. z => <r> | one. z => <r> | two. z => <r> ]
- ],
- .Transitive = for (x: Three)(y: Three)(z: Three)(r: set-of(Relation x y))(s: set-of(Relation y z)), <pt>
+let instance eqTwo :: SetWithEquivRelation = {
+ .Carrier = Two :: Set,
+ .Relation = for (x: Two) (y: Two),
+ case x of [ zero. _ => case y of [ zero. _ => Unit :: Set | one. _ => Empty :: Set ]
+ | one. _ => case y of [ zero. _ => Empty :: Set | one. _ => Unit :: Set ] ],
+ .Reflexive = for (x: Two), case x of [ zero. _ => <pt> | one. _ => <pt> ],
+ .Symmetric = for (x: Two) (y: Two) (r: set-of(Relation x y)),
+ case x of [ zero. _ => case y of [ zero. _ => <r> | one. _ => <r> ]
+ | one. _ => case y of [ zero. _ => <r> | one. _ => <r> ] ],
+ .Transitive = for (x: Two)(y: Two)(z: Two)(r: set-of(Relation x y))(s: set-of(Relation y z)),
+ case x of [ zero. _ => case y of
+ [ zero. _ => case z of [ zero. _ => <r> | one. _ => <s> ]
+ | one. _ => case z of [ zero. _ => <pt>| one. _ => <r> ] ]
+ | one. _ => case y of
+ [ zero. _ => case z of [ zero. _ => <r> | one. _ => <pt>]
+ | one. _ => case z of [ zero. _ => <s> | one. _ => <r> ] ] ]
}
-// let set Diagonal = record { x : set-of(eqThree .Carrier), y : set-of(eqThree .Carrier), equal : set-of((eqThree .Relation) x y) }
+let set Diagonal = record { x : set-of(eqTwo .Carrier), y : set-of(eqTwo .Carrier), equal : set-of((eqTwo .Relation) x y) }
-// let element oneEqualsOne : Diagonal = { .x = one. pt, .y = one. pt, .equal = pt }
+let element oneEqualsOne : Diagonal = { .x = one. pt, .y = one. pt, .equal = pt }
diff --git a/src/checker.rs b/src/checker.rs
index f94fccc..7b06c8b 100644
--- a/src/checker.rs
+++ b/src/checker.rs
@@ -28,7 +28,7 @@ impl CheckerState {
Decl::Element { name, element, set } => {
self.assert_unbound_element(name)?;
let set = self.check_set(set)?;
- let element = self.check_element(element.into(), &set)?;
+ let element = self.check_element(element.into(), Some(&set))?;
self.add_element(name.clone(), element.into(), set)
}
Decl::Signature { name, signature } => {
diff --git a/src/checker_set.rs b/src/checker_set.rs
index 83d97a1..f13f686 100644
--- a/src/checker_set.rs
+++ b/src/checker_set.rs
@@ -13,7 +13,7 @@ impl CheckerState {
let mut ctx = self.clone();
let field_set = fields.iter().map(|f| &f.name).collect::<HashSet<&String>>();
if field_set.len() != fields.len() {
- todo!("duplicate fields");
+ return Err(CheckerError::DuplicateFieldsSet(set.clone()));
}
let fields = fields
.into_iter()
@@ -29,6 +29,11 @@ impl CheckerState {
Ok(Set::Record(fields))
}
Set::Variant(fields) => {
+ let field_set = fields.iter().map(|f| &f.name).collect::<HashSet<&String>>();
+ if field_set.len() != fields.len() {
+ return Err(CheckerError::DuplicateFieldsSet(set.clone()));
+ }
+
let fields = fields
.into_iter()
.map(|Field { name, carries }| {
@@ -76,43 +81,59 @@ impl CheckerState {
}
}
- #[instrument(skip(self), level = "debug", fields(%element, %set))]
- pub fn check_element(&self, element: &Element, set: &Set) -> Result<Element, CheckerError> {
+ #[instrument(skip(self), level = "debug", fields(%element, set=%set.map(|s| s.to_string()).unwrap_or_default()))]
+ pub fn check_element(
+ &self,
+ element: &Element,
+ set: Option<&Set>,
+ ) -> Result<Element, CheckerError> {
match element {
Element::Literal(lit) => {
let value = element.clone();
// we may infer the type from the element
- match lit {
- Literal::Int(_) => {
- self._check_literal_set_helper(value, set, Set::BuiltIn(BuiltIn::Int))?;
- }
- Literal::Nat(_) => {
- self._check_literal_set_helper(value, set, Set::BuiltIn(BuiltIn::Nat))?;
- }
- Literal::Str(_) => {
- self._check_literal_set_helper(value, set, Set::BuiltIn(BuiltIn::Str))?;
- }
- Literal::Bool(_) => {
- self._check_literal_set_helper(value, set, Set::BuiltIn(BuiltIn::Bool))?;
- }
- Literal::Float(_) => {
- self._check_literal_set_helper(value, set, Set::BuiltIn(BuiltIn::Float))?;
+ if let Some(set) = set {
+ match lit {
+ Literal::Int(_) => {
+ self._check_literal_set_helper(value, set, Set::BuiltIn(BuiltIn::Int))?;
+ }
+ Literal::Nat(_) => {
+ self._check_literal_set_helper(value, set, Set::BuiltIn(BuiltIn::Nat))?;
+ }
+ Literal::Str(_) => {
+ self._check_literal_set_helper(value, set, Set::BuiltIn(BuiltIn::Str))?;
+ }
+ Literal::Bool(_) => {
+ self._check_literal_set_helper(
+ value,
+ set,
+ Set::BuiltIn(BuiltIn::Bool),
+ )?;
+ }
+ Literal::Float(_) => {
+ self._check_literal_set_helper(
+ value,
+ set,
+ Set::BuiltIn(BuiltIn::Float),
+ )?;
+ }
}
}
Ok(element.clone().into())
}
Element::Var(v) => {
let lookup = self.lookup_element(&v)?;
- let container = self.check_set(&lookup.container)?; // TODO: necessary why?
- // 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, &container) {
- return Err(CheckerError::WrongSetForElement {
- value: element.clone().into(),
- claimed: set.clone(),
- real: container,
- });
+ if let Some(set) = set {
+ let container = self.check_set(&lookup.container)?;
+ // 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, &container) {
+ return Err(CheckerError::WrongSetForElement {
+ value: element.clone().into(),
+ claimed: set.clone(),
+ real: container,
+ });
+ }
}
// If we found a formal binding, we have no value to report.
// This is the ONLY source of Var as a return value for
@@ -125,21 +146,53 @@ impl CheckerState {
}
}
Element::Record(assignations) => {
- let rej = |reason| CheckerError::ElementDoesNotBelong {
- element: element.clone(),
- claimed: set.clone(),
- reason,
+ // there's a very short path here for constructing {} : record {}
+ if assignations.is_empty() {
+ let element = Element::Record(Vec::new());
+ if let Some(set) = set {
+ if !self.equal(set, &Set::Record(Vec::new())) {
+ return Err(CheckerError::ElementDoesNotBelong {
+ element,
+ claimed: set.clone(),
+ reason: "the set is not the empty record".to_string(),
+ });
+ };
+ };
+ return Ok(element);
+ }
+ // from here on assignations is non-empty
+
+ // look up the owner for each tag
+ let owners = assignations
+ .iter()
+ .map(|ea| self.lookup_record_field(&ea.name).map(|x| &x.owner))
+ .collect::<Result<Vec<_>, _>>()?;
+
+ // make sure they're all the same
+ let owner = owners[0];
+ if !owners[1..].into_iter().all(|x| self.equal(*x, owner)) {
+ return Err(CheckerError::ElementInconsistentFieldChoice(
+ element.clone(),
+ ));
};
- // 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()))
- }?;
+ // if in addition we know the set, make sure it agrees
+ if let Some(set) = set
+ && !self.equal(set, owner)
+ {
+ return Err(CheckerError::WrongSetForElement {
+ value: element.clone().into(),
+ claimed: set.clone(),
+ real: owner.clone(),
+ });
+ }
+
+ let Set::Record(fields) = owner else {
+ panic!("invariant violation: looking up field owners did not retrieve a record")
+ };
let mut set_fnames_sorted: Vec<String> =
- fields.iter().map(|x| x.name.clone()).collect();
+ fields.iter().map(|f| f.name.clone()).collect();
set_fnames_sorted.sort();
let mut element_fnames_sorted: Vec<String> =
@@ -148,11 +201,15 @@ impl CheckerState {
// make sure that we are correctly filling the record
if set_fnames_sorted != element_fnames_sorted {
- return Err(rej(format!(
- "expected [{}] but found [{}]",
- set_fnames_sorted.join(", "),
- element_fnames_sorted.join(", "),
- )));
+ return Err(CheckerError::ElementDoesNotBelong {
+ element: element.clone(),
+ claimed: owner.clone(),
+ reason: format!(
+ "expected [{}] but found [{}]",
+ set_fnames_sorted.join(", "),
+ element_fnames_sorted.join(", "),
+ ),
+ });
}
let assignations = assignations
@@ -176,7 +233,7 @@ impl CheckerState {
.expect("we have already checked that all fields are present");
let f_s = ctx.check_set(f_s)?;
- let f_e = ctx.check_element(f_e, &f_s)?;
+ let f_e = ctx.check_element(f_e, Some(&f_s))?;
ctx.add_element(f_n.clone(), f_e.clone().into(), f_s)?;
Ok(ElemAssign {
@@ -200,7 +257,9 @@ impl CheckerState {
} = self.lookup_record_field(&field)?;
// enforce the correct typing of the claimed result
- if !self.equal(set, field_set) {
+ if let Some(set) = set
+ && !self.equal(set, field_set)
+ {
return Err(CheckerError::WrongSetForElement {
value: element.clone().into(),
claimed: set.clone(),
@@ -209,7 +268,7 @@ impl CheckerState {
}
// enforce the correct typing of the element
- let inner = self.check_element(inner, owner_set)?;
+ let inner = self.check_element(inner, Some(owner_set))?;
// Unfortunately we still have to do something nasty here to
// obtain the data
@@ -250,7 +309,9 @@ impl CheckerState {
} = self.lookup_variant_field(&field)?;
// enforce the correct typing of the claimed result
- if !self.equal(set, owner_set) {
+ if let Some(set) = set
+ && !self.equal(set, owner_set)
+ {
return Err(CheckerError::WrongSetForElement {
value: element.clone().into(),
claimed: set.clone(),
@@ -259,7 +320,7 @@ impl CheckerState {
}
// enforce the correct typing of the element
- let element = self.check_element(inner, field_set)?;
+ let element = self.check_element(inner, Some(field_set))?;
Ok(Element::Inject {
element: Box::new(element),
field: field.clone(),
@@ -311,7 +372,7 @@ impl CheckerState {
// 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)?;
+ let scrutinee = self.check_element(scrutinee, Some(owner))?;
// which variant are we, if any
let matching: Option<(String, Element)> = match scrutinee {
@@ -359,9 +420,9 @@ impl CheckerState {
{
let canonical =
ctx.make_element_definition(binding_name, inner.clone(), binding_set)?;
- let this_set = ctx.check_set(set)?;
+ let this_set = set.map(|set| ctx.check_set(set)).transpose()?;
- let output = ctx.check_element((&arm.body).into(), &this_set)?;
+ let output = ctx.check_element((&arm.body).into(), this_set.as_ref())?;
if matches!(computed_output, Some(_)) {
panic!(
"invariant violation: we somehow matched multiple arms in case analysis"
@@ -386,8 +447,8 @@ impl CheckerState {
owner.clone(),
)?;
};
- let this_set = ctx.check_set(set)?;
- let body = ctx.check_element((&arm.body).into(), &this_set)?;
+ let this_set = set.map(|set| ctx.check_set(set)).transpose()?;
+ let body = ctx.check_element((&arm.body).into(), this_set.as_ref())?;
CaseArm {
tag: arm.tag.clone(),
diff --git a/src/checker_signature.rs b/src/checker_signature.rs
index 9d0bffe..1ce8bc8 100644
--- a/src/checker_signature.rs
+++ b/src/checker_signature.rs
@@ -1,6 +1,6 @@
use crate::ast::*;
use crate::checker_state::*;
-use std::collections::HashMap;
+use std::collections::{HashMap, HashSet};
use std::iter::zip;
use tracing::instrument;
@@ -80,6 +80,11 @@ impl CheckerState {
})
}
Signature::Theory(fields) => {
+ let field_set = fields.iter().map(|f| &f.name).collect::<HashSet<&String>>();
+ if field_set.len() != fields.len() {
+ return Err(CheckerError::DuplicateFieldsSignature(signature.clone()));
+ }
+
let mut ctx = self.clone();
let temp_name = ctx.make_unique_name();
let mut new_fields = Vec::new();
@@ -132,7 +137,7 @@ impl CheckerState {
}
}
Instance::ElementCoerce(element) => {
- if let Some(signature) = signature {
+ let set = if let Some(signature) = signature {
let Signature::FromSet(set) = signature else {
return Err(CheckerError::WrongSignatureForInstance {
value: instance.clone().into(),
@@ -140,26 +145,13 @@ impl CheckerState {
claimed: signature.clone(),
});
};
- println!("{self}");
- let element = self.check_element(element, set)?;
- Ok(Instance::ElementCoerce(element))
+ Some(set)
} else {
- // todo!("how do we handle check_element without a set?");
- println!("THISISATTODO");
- // quick hack:
- let element = if let Element::Var(v) = element {
- let lookup = self.lookup_element(&v)?;
- if let ElementValue::Concrete(ref x) = lookup.value {
- x.clone()
- } else {
- element.clone()
- }
- } else {
- element.clone()
- };
+ None
+ };
- Ok(Instance::ElementCoerce(element.clone()))
- }
+ let element = self.check_element(element, set)?;
+ Ok(Instance::ElementCoerce(element))
}
Instance::Var(v) => {
// Exactly the same discipline as for Element::Var, see there
@@ -337,7 +329,7 @@ impl CheckerState {
required: required_field_names_sorted,
});
}
- let scrutinee = self.check_element(scrutinee, owner)?;
+ let scrutinee = self.check_element(scrutinee, Some(owner))?;
let matching: Option<(String, Element)> = match scrutinee {
Element::Inject {
@@ -376,12 +368,8 @@ impl CheckerState {
{
let canonical =
ctx.make_element_definition(binding_name, inner.clone(), binding_set)?;
- let this_signature = if let Some(signature) = signature {
- let signature = ctx.check_signature(signature)?;
- Some(signature)
- } else {
- None
- };
+ let this_signature =
+ signature.map(|s| ctx.check_signature(s)).transpose()?;
let output =
ctx.check_instance((&arm.body).into(), this_signature.as_ref())?;
@@ -409,13 +397,8 @@ impl CheckerState {
owner.clone(),
)?;
};
- let this_signature = if let Some(signature) = signature {
- let signature = ctx.check_signature(signature)?;
- Some(signature)
- } else {
- None
- };
-
+ let this_signature =
+ signature.map(|s| ctx.check_signature(s)).transpose()?;
let body =
ctx.check_instance((&arm.body).into(), this_signature.as_ref())?;
CaseArm {
@@ -683,7 +666,7 @@ impl CheckerState {
let checked = zip(params.iter(), args.iter())
.map(|(p, a)| {
let p_set = ctx.check_set(&p.set)?;
- let a = ctx.check_element(a, &p_set)?;
+ let a = ctx.check_element(a, Some(&p_set))?;
ctx.add_element(p.name.clone(), a.clone().into(), p_set)?;
Ok(a)
})
@@ -697,13 +680,13 @@ impl CheckerState {
Instance::Project { field, .. } => {
Ok(Some(self.lookup_signature_field(field)?.field.clone()))
}
- // All arms of a stuck Case share a signature by the case
- // elimination typing rule, and we've already expanded the body, so
- // we can pick any arm.
-
- // TODO! this is wrong!
- Instance::Case { arms, .. } => self
- ._stuck_subject_signature(&arms.first().expect("we don't allow bottom type").body),
+ // until we properly support motives there's nothing we can really do here
+ Instance::Case { .. } => {
+ let msg = format!(
+ "this type checker has no motives yet, and was called upon to infer the signature of {inst}, which leads with a `case`, and so has no option but to fail"
+ );
+ Err(CheckerError::Unimplemented(msg))
+ }
Instance::ElementCoerce(_)
| Instance::For { .. }
| Instance::Record(_)
diff --git a/src/checker_state.rs b/src/checker_state.rs
index 77abbdd..42f5089 100644
--- a/src/checker_state.rs
+++ b/src/checker_state.rs
@@ -19,6 +19,9 @@ pub enum CheckerError {
#[display("The following functionality is unimplemented: {_0}")]
Unimplemented(String),
+ #[display("The set contains dulplicate fiels: {_0}")]
+ DuplicateFieldsSet(Set),
+
#[display("Element {value} claimed to belong to {claimed} but actually belongs to {real}")]
WrongSetForElement {
value: ElementValue,
@@ -33,9 +36,15 @@ pub enum CheckerError {
reason: String,
},
+ #[display("Record construction involves incosistent field choice {_0}")]
+ ElementInconsistentFieldChoice(Element),
+
#[display("Case analysis {_0} does not have consistent set for scrutinee")]
ElementInconsistentCaseScrutineeSet(Element),
+ #[display("The signature contains dulplicate fiels: {_0}")]
+ DuplicateFieldsSignature(Signature),
+
#[display("Case analysis {_0} does not have consistent set for scrutinee")]
InstanceInconsistentCaseScrutineeSet(Instance),
diff --git a/src/parser.rs b/src/parser.rs
index 73e8dd3..8dbc31e 100644
--- a/src/parser.rs
+++ b/src/parser.rs
@@ -57,13 +57,13 @@ parser! {
// ====================================================================
rule lower_ident() -> String
- = !keyword() s:$(['a'..='z'] ident_tail()*) { s.to_string() }
+ = !keyword() s:$(['_' | 'a'..='z'] ident_tail()*) { s.to_string() }
rule upper_ident() -> String
= !keyword() s:$(['A'..='Z'] ident_tail()*) { s.to_string() }
rule any_ident() -> String
- = !keyword() s:$(['a'..='z' | 'A'..='Z'] ident_tail()*) { s.to_string() }
+ = !keyword() s:$(['_' | 'a'..='z' | 'A'..='Z'] ident_tail()*) { s.to_string() }
rule elem_var() -> String = lower_ident()
rule inst_var() -> String = lower_ident()
generated by cgit v1.3.1 (git 2.54.0) at 2026-08-30 17:05:24 +0000