aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/ast.rs10
-rw-r--r--src/checker.rs3
-rw-r--r--src/checker_set.rs37
-rw-r--r--src/checker_signature.rs83
-rw-r--r--src/checker_state.rs2
-rw-r--r--src/parser.rs66
6 files changed, 148 insertions, 53 deletions
diff --git a/src/ast.rs b/src/ast.rs
index e254c65..24c7125 100644
--- a/src/ast.rs
+++ b/src/ast.rs
@@ -68,6 +68,9 @@ pub enum Signature {
#[display("Set")]
Set,
+ #[display("⟨{_0}⟩")]
+ FromSet(Set),
+
#[display("theory {{ {} }}", _0.iter().map(|f| f.to_string()).collect::<Vec<_>>().join(" , "))]
Theory(Vec<Field<Signature>>),
@@ -126,7 +129,7 @@ pub enum Element {
element: Box<Element>,
},
- #[display("case {} of {{ {} }}", scrutinee, arms.iter().map(|a| a.to_string()).collect::<Vec<_>>().join(" | "))]
+ #[display("case {scrutinee} of [ {} ]", arms.iter().map(|a| a.to_string()).collect::<Vec<_>>().join(" | "))]
Case {
scrutinee: Box<Element>,
arms: Vec<CaseArm<Element>>,
@@ -147,6 +150,9 @@ pub enum Instance {
#[display("({_0} :: Set)")]
SetCoerce(Box<Set>),
+ #[display("⟨{_0}⟩")]
+ ElementCoerce(Element),
+
#[display("{_0}")]
Var(String),
@@ -171,7 +177,7 @@ pub enum Instance {
field: String,
},
- #[display("case {} of [ {} ]", scrutinee, arms.iter().map(|a| a.to_string()).collect::<Vec<_>>().join(" | "))]
+ #[display("case {scrutinee} of [ {} ]", arms.iter().map(|a| a.to_string()).collect::<Vec<_>>().join(" | "))]
Case {
scrutinee: Box<Element>,
arms: Vec<CaseArm<Instance>>,
diff --git a/src/checker.rs b/src/checker.rs
index 2474bab..f94fccc 100644
--- a/src/checker.rs
+++ b/src/checker.rs
@@ -16,7 +16,7 @@ impl CheckerState {
let Programme(decls) = prog;
for decl in decls {
- debug!(%decl);
+ print!("{decl} ... ");
self.reset_binders();
match decl {
Decl::Set { name, set } => {
@@ -47,6 +47,7 @@ impl CheckerState {
self.add_instance(name.clone(), instance.into(), signature)
}
}?;
+ println!("Ok");
}
debug!(%self);
Ok(())
diff --git a/src/checker_set.rs b/src/checker_set.rs
index a00ea81..1a89631 100644
--- a/src/checker_set.rs
+++ b/src/checker_set.rs
@@ -230,7 +230,7 @@ impl CheckerState {
.element;
Ok(sub_element)
}
- _ => panic!(
+ Element::Inject { .. } | Element::Literal(_) => panic!(
"invariant violation: check_element returned neither a record or stuck computation for record set"
),
}
@@ -312,7 +312,6 @@ impl CheckerState {
let scrutinee = self.check_element(scrutinee, owner)?;
// which variant are we, if any
-
let matching: Option<(String, Element)> = match scrutinee {
Element::Inject {
ref field,
@@ -326,6 +325,18 @@ impl CheckerState {
),
};
+ // are we allowed to posit the equality of elements scrutinee =
+ // (arm.tag). (arm.bound) when looking at necessarily
+ // non-matching arms?
+ let posit_equality_with = match &scrutinee {
+ Element::Var(v) => Some(v.clone()),
+ Element::Inject { .. }
+ | Element::Project { .. }
+ | Element::Case { .. }
+ | Element::Literal(_)
+ | Element::Record(_) => None,
+ };
+
// for each arm, recurse with a concrete value (if we have one)
// otherwise fall back to hypothetical elements; in the former
// case record the end result
@@ -333,7 +344,8 @@ impl CheckerState {
let mut processed_arms = Vec::new();
for arm in arms {
let OwnedField {
- field: field_set, ..
+ field: field_set,
+ owner,
} = self.lookup_variant_field(&arm.tag)?;
let mut ctx = self.clone();
@@ -345,7 +357,9 @@ impl CheckerState {
{
let canonical =
ctx.make_element_definition(binding_name, inner.clone(), binding_set)?;
- let output = ctx.check_element((&arm.body).into(), set)?;
+ let this_set = ctx.check_set(set)?;
+
+ let output = ctx.check_element((&arm.body).into(), &this_set)?;
if matches!(computed_output, Some(_)) {
panic!(
"invariant violation: we somehow matched multiple arms in case analysis"
@@ -359,7 +373,20 @@ impl CheckerState {
}
} else {
let canonical = ctx.make_element_binding(binding_name, binding_set)?;
- let body = ctx.check_element((&arm.body).into(), set)?;
+
+ if let Some(ref scrutinee_var) = posit_equality_with {
+ ctx.make_element_definition(
+ scrutinee_var.clone(),
+ Element::Inject {
+ field: arm.tag.clone(),
+ element: Box::new(Element::Var(canonical.clone())),
+ },
+ owner.clone(),
+ )?;
+ };
+ let this_set = ctx.check_set(set)?;
+ let body = ctx.check_element((&arm.body).into(), &this_set)?;
+
CaseArm {
tag: arm.tag.clone(),
bound: canonical,
diff --git a/src/checker_signature.rs b/src/checker_signature.rs
index cc6cadc..ab54fd1 100644
--- a/src/checker_signature.rs
+++ b/src/checker_signature.rs
@@ -10,6 +10,7 @@ impl CheckerState {
pub fn check_signature(&self, signature: &Signature) -> Result<Signature, CheckerError> {
match signature {
Signature::Set => Ok(Signature::Set),
+ Signature::FromSet(set) => Ok(Signature::FromSet(self.check_set(set)?)),
Signature::Var(v) => {
let deref = self.lookup_signature(&v)?;
Ok(deref.clone())
@@ -64,6 +65,7 @@ impl CheckerState {
.into_iter()
.map(|Param { name, set }| {
let canonical = ctx.make_element_binding(name, set.clone())?;
+ let set = ctx.check_set(&set)?;
Ok(Param {
name: canonical,
set,
@@ -129,6 +131,22 @@ impl CheckerState {
Ok(Instance::SetCoerce(set))
}
}
+ Instance::ElementCoerce(element) => {
+ if let Some(signature) = signature {
+ let Signature::FromSet(set) = signature else {
+ return Err(CheckerError::WrongSignatureForInstance {
+ value: instance.clone().into(),
+ real: Signature::FromSet(Set::Var("_".to_string())),
+ claimed: signature.clone(),
+ });
+ };
+ let element = self.check_element(element, set)?;
+ Ok(Instance::ElementCoerce(element))
+ } else {
+ // todo!("how do we handle check_element without a set?");
+ Ok(Instance::ElementCoerce(element.clone()))
+ }
+ }
Instance::Var(v) => {
// Exactly the same discipline as for Element::Var, see there
// for some sparse comments
@@ -260,7 +278,11 @@ impl CheckerState {
.instance;
Ok(sub_element)
}
- _ => panic!(
+ Instance::For { .. }
+ | Instance::ElementCoerce(_)
+ | Instance::SetCoerce(_)
+ | Instance::App { .. }
+ | Instance::Case { .. } => panic!(
"invariant violation: check_instance returned neither a record or stuck computation for record set"
),
}
@@ -314,11 +336,21 @@ impl CheckerState {
),
};
+ let posit_equality_with = match &scrutinee {
+ Element::Var(v) => Some(v.clone()),
+ Element::Inject { .. }
+ | Element::Project { .. }
+ | Element::Case { .. }
+ | Element::Literal(_)
+ | Element::Record(_) => None,
+ };
+
let mut computed_output = None;
let mut processed_arms = Vec::new();
for arm in arms {
let OwnedField {
- field: field_set, ..
+ field: field_set,
+ owner,
} = self.lookup_variant_field(&arm.tag)?;
let mut ctx = self.clone();
@@ -330,7 +362,15 @@ impl CheckerState {
{
let canonical =
ctx.make_element_definition(binding_name, inner.clone(), binding_set)?;
- let output = ctx.check_instance((&arm.body).into(), signature)?;
+ let this_signature = if let Some(signature) = signature {
+ let signature = ctx.check_signature(signature)?;
+ Some(signature)
+ } else {
+ None
+ };
+
+ let output =
+ ctx.check_instance((&arm.body).into(), this_signature.as_ref())?;
if matches!(computed_output, Some(_)) {
panic!(
"invariant violation: we somehow matched multiple arms in case analysis"
@@ -344,7 +384,26 @@ impl CheckerState {
}
} else {
let canonical = ctx.make_element_binding(binding_name, binding_set)?;
- let body = ctx.check_instance((&arm.body).into(), signature)?;
+ if let Some(ref scrutinee_var) = posit_equality_with {
+ ctx.add_element(
+ scrutinee_var.clone(),
+ Element::Inject {
+ field: arm.tag.clone(),
+ element: Box::new(Element::Var(canonical.clone())),
+ }
+ .into(),
+ owner.clone(),
+ )?;
+ };
+ let this_signature = if let Some(signature) = signature {
+ let signature = ctx.check_signature(signature)?;
+ Some(signature)
+ } else {
+ None
+ };
+
+ let body =
+ ctx.check_instance((&arm.body).into(), this_signature.as_ref())?;
CaseArm {
tag: arm.tag.clone(),
bound: canonical,
@@ -508,7 +567,7 @@ impl CheckerState {
// nevertheless we need the tiniest amount of bidirectionality
// here to deal with case, project, and var recursively
- let subject_sig: Option<Signature> = self.stuck_subject_signature(&subject)?;
+ let subject_sig: Option<Signature> = self._stuck_subject_signature(&subject)?;
if let Some(subject_sig) = subject_sig {
let Signature::Ext { params, codomain } = subject_sig else {
@@ -567,7 +626,7 @@ impl CheckerState {
ctx.check_instance(&residual, signature)
}
}
- Instance::Record(_) | Instance::SetCoerce(_) => {
+ Instance::Record(_) | Instance::SetCoerce(_) | Instance::ElementCoerce(_) => {
Err(CheckerError::NonFunctionalInstance {
instance: subject,
elements: args,
@@ -611,7 +670,7 @@ impl CheckerState {
Ok((ctx, checked))
}
- fn stuck_subject_signature(&self, inst: &Instance) -> Result<Option<Signature>, CheckerError> {
+ fn _stuck_subject_signature(&self, inst: &Instance) -> Result<Option<Signature>, CheckerError> {
match inst {
Instance::Var(v) => Ok(Some(self.lookup_instance(v)?.container.clone())),
Instance::Project { field, .. } => {
@@ -620,10 +679,14 @@ impl CheckerState {
// 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.
- Instance::Case { arms, .. } => self
- .stuck_subject_signature(&arms.first().expect("we don't allow bottom type").body),
- Instance::For { .. } | Instance::Record(_) | Instance::SetCoerce(_) => Ok(None),
+ // TODO! this is wrong!
+ Instance::Case { arms, .. } => self
+ ._stuck_subject_signature(&arms.first().expect("we don't allow bottom type").body),
+ Instance::ElementCoerce(_)
+ | Instance::For { .. }
+ | Instance::Record(_)
+ | Instance::SetCoerce(_) => Ok(None),
Instance::App { .. } => unreachable!(
"invariant violation: _stuck_head_signature called on a left-nested App"
diff --git a/src/checker_state.rs b/src/checker_state.rs
index ad01d50..a88c6b0 100644
--- a/src/checker_state.rs
+++ b/src/checker_state.rs
@@ -399,7 +399,7 @@ impl CheckerState {
Signature::Ext { codomain, .. } => {
self._register_signature_fields(codomain, rebind)?;
}
- _ => (),
+ Signature::Var(_) | Signature::Set | Signature::FromSet(_) => (),
}
Ok(())
}
diff --git a/src/parser.rs b/src/parser.rs
index f205407..73e8dd3 100644
--- a/src/parser.rs
+++ b/src/parser.rs
@@ -45,12 +45,12 @@ parser! {
rule kw_false() = "false" wb()
rule keyword() =
- kw_let_set() / kw_let_element() / kw_let_signature() / kw_let_instance()
- / kw_record() / kw_variant() / kw_theory()
- / kw_case() / kw_of() / kw_for()
- / kw_Set() / kw_set_of() / kw_set()
- / kw_Nat() / kw_Int() / kw_Float() / kw_Str() / kw_Bool()
- / kw_true() / kw_false()
+ kw_let_set() / kw_let_element() / kw_let_signature() / kw_let_instance()
+ / kw_record() / kw_variant() / kw_theory()
+ / kw_case() / kw_of() / kw_for()
+ / kw_Set() / kw_set_of() / kw_set()
+ / kw_Nat() / kw_Int() / kw_Float() / kw_Str() / kw_Bool()
+ / kw_true() / kw_false()
// ====================================================================
// Identifiers
@@ -134,19 +134,20 @@ parser! {
= kw_set_of() _ "(" _ i:instance() _ ")" { i }
rule set() -> Set
- = kw_record() _ "{" _ fs:(set_field() ** ",") _ "}" { Set::Record(fs) }
- / kw_variant() _ "[" _ vs:(variant_field() ** "|") _ "]" { Set::Variant(vs) }
- / b:builtin() { Set::BuiltIn(b) }
- / i:claimed_set() { Set::ClaimedSet(i) }
- / v:set_var() { Set::Var(v) }
- / "(" _ s:set() _ ")" { s }
+ = kw_record() _ "{" _ fs:(set_field() ** ",") _ "}" { Set::Record(fs) }
+ / kw_variant() _ "[" _ vs:(variant_field() ** "|") _ "]" { Set::Variant(vs) }
+ / b:builtin() { Set::BuiltIn(b) }
+ / i:claimed_set() { Set::ClaimedSet(i) }
+ / v:set_var() { Set::Var(v) }
+ / "(" _ s:set() _ ")" { s }
// ====================================================================
// Signatures
// ====================================================================
rule param() -> Param
- = "(" _ n:elem_var() _ ":" _ s:set() _ ")" { Param { name: n, set: s } }
+ = "(" _ n:elem_var() _ ":" _ s:set() _ ")"
+ { Param { name: n, set: s } }
rule param_list() -> Vec<Param> = param() ++ _
@@ -168,11 +169,12 @@ parser! {
}
rule signature() -> Signature
- = kw_Set() { Signature::Set }
- / kw_theory() _ "{" _ fs:(sig_field() ** ",") _ "}" { Signature::Theory(fs) }
- / s:sig_ext() { s }
- / v:sig_var() { Signature::Var(v) }
- / "(" _ s:signature() _ ")" { s }
+ = kw_Set() { Signature::Set }
+ / "<" _ s:set() _ ">" { Signature::FromSet(s) }
+ / kw_theory() _ "{" _ fs:(sig_field() ** ",") _ "}" { Signature::Theory(fs) }
+ / s:sig_ext() { s }
+ / v:sig_var() { Signature::Var(v) }
+ / "(" _ s:signature() _ ")" { s }
// ====================================================================
// Elements
@@ -204,9 +206,8 @@ parser! {
{ CaseArm { tag: t, bound: x, body } }
rule element() -> Element
- = kw_case() _ scrut:element() _ kw_of() _ "[" _ arms:(case_arm() ** "|") _ "]"
- { Element::Case { scrutinee: Box::new(scrut), arms } }
- / d:dot_elem() { d }
+ = kw_case() _ scrut:element() _ kw_of() _ "[" _ arms:(case_arm() ** "|") _ "]" { Element::Case { scrutinee: Box::new(scrut), arms } }
+ / d:dot_elem() { d }
// ====================================================================
// Instances
@@ -221,10 +222,12 @@ parser! {
{ InstAssign { name: n, instance: i } }
rule explicit_set_coerce() -> Set
- = s:set() _ "::" _ kw_Set() { s }
+ = s:set() _ "::" _ kw_Set()
+ { s }
rule atom_inst() -> Instance
= s:explicit_set_coerce() { Instance::SetCoerce(Box::new(s)) }
+ / "<" _ e:element() _ ">" { Instance::ElementCoerce(e) }
/ v:inst_var() { Instance::Var(v) }
/ f:sig_var() { Instance::Var(f) }
/ "{" _ fs:(inst_assign() ** ",") _ "}" { Instance::Record(fs) }
@@ -269,24 +272,19 @@ parser! {
}
rule instance() -> Instance
- = i:inst_for() { i }
- / kw_case() _ scrut:element() _ kw_of() _ "[" _ arms:(inst_case_arm() ** "|") _ "]"
- { Instance::Case { scrutinee: Box::new(scrut), arms } }
- / app_inst()
+ = i:inst_for() { i }
+ / kw_case() _ scrut:element() _ kw_of() _ "[" _ arms:(inst_case_arm() ** "|") _ "]" { Instance::Case { scrutinee: Box::new(scrut), arms } }
+ / a:app_inst() { a }
// ====================================================================
// Top-level declarations
// ====================================================================
rule decl() -> Decl
- = kw_let_set() _ n:set_var() _ "=" _ s:set()
- { Decl::Set { name: n, set: s } }
- / kw_let_element() _ n:elem_var() _ ":" _ s:set() _ "=" _ e:element()
- { Decl::Element { name: n, set: s, element: e } }
- / kw_let_signature() _ n:sig_var() _ "=" _ sg:signature()
- { Decl::Signature { name: n, signature: sg } }
- / kw_let_instance() _ n:inst_var() _ "::" _ sg:signature() _ "=" _ i:instance()
- { Decl::Instance { name: n, signature: sg, instance: i } }
+ = kw_let_set() _ n:set_var() _ "=" _ s:set() { Decl::Set { name: n, set: s } }
+ / kw_let_element() _ n:elem_var() _ ":" _ s:set() _ "=" _ e:element() { Decl::Element { name: n, set: s, element: e } }
+ / kw_let_signature() _ n:sig_var() _ "=" _ sg:signature() { Decl::Signature { name: n, signature: sg } }
+ / kw_let_instance() _ n:inst_var() _ "::" _ sg:signature() _ "=" _ i:instance() { Decl::Instance { name: n, signature: sg, instance: i } }
pub rule program() -> Programme
= _ ds:(decl() ** _) _ { Programme(ds) }
generated by cgit v1.3.1 (git 2.54.0) at 2026-08-30 21:23:43 +0000