Add arity check for constructor patterns

This commit is contained in:
imaqtkatt 2024-02-02 15:51:36 -03:00
parent 9faac6e6cb
commit 5e858f6024
6 changed files with 80 additions and 1 deletions

View File

@ -76,6 +76,7 @@ pub fn desugar_book(book: &mut Book, opts: Opts) -> Result<(DefId, Vec<Warning>)
pub fn encode_pattern_matching(book: &mut Book, warnings: &mut Vec<Warning>) -> Result<(), String> {
book.resolve_ctrs_in_pats();
book.check_unbound_pats()?;
book.check_ctrs_arities()?;
book.resolve_refs()?;
book.desugar_let_destructors();
book.desugar_implicit_match_binds();

View File

@ -0,0 +1,67 @@
use std::collections::HashMap;
use crate::term::{Book, Name, Pattern};
impl Book {
/// Checks if every constructor pattern of every definition rule has the same arity from the
/// defined adt constructor.
///
/// Constructors should be already resolved.
pub fn check_ctrs_arities(&self) -> Result<(), String> {
let arities = self.ctr_arities();
for def in self.defs.values() {
let def_name = &self.def_names.id_to_name[&def.def_id];
for rule in def.rules.iter() {
for pat in rule.pats.iter() {
pat.check(&arities).map_err(|err| format!("In definition {}: {}", def_name, err))?;
}
}
}
Ok(())
}
/// Returns a hashmap of the constructor name to its arity.
pub fn ctr_arities(&self) -> HashMap<Name, usize> {
let mut arities = HashMap::new();
for adt in self.adts.values() {
for (ctr_name, fields) in adt.ctrs.iter() {
arities.insert(ctr_name.clone(), fields.len());
}
}
arities
}
}
impl Pattern {
fn check(&self, arities: &HashMap<Name, usize>) -> Result<(), String> {
match self {
Pattern::Ctr(name, args) => {
let arity = arities.get(name).unwrap();
let args = args.len();
if *arity != args {
return Err(format!(
"Arity error. Constructor '{}' expects {} fields but was found {}.",
name, arity, args
));
} else {
Ok(())
}
}
Pattern::Tup(fst, snd) => {
fst.check(arities)?;
snd.check(arities)
}
Pattern::List(els) => {
for el in els {
el.check(arities)?;
}
Ok(())
}
Pattern::Var(..) | Pattern::Num(..) => Ok(()),
}
}
}

View File

@ -4,3 +4,4 @@ pub mod shared_names;
pub mod type_check;
pub mod unbound_pats;
pub mod unbound_vars;
pub mod ctrs_arities;

View File

@ -4,7 +4,7 @@ use std::collections::HashSet;
impl Book {
/// Check if the constructors in rule patterns or match patterns are defined.
pub fn check_unbound_pats(&self) -> Result<(), String> {
let is_ctr = |nam: &Name| self.def_names.contains_name(nam);
let is_ctr = |nam: &Name| self.ctrs.contains_key(nam);
for def in self.defs.values() {
let def_name = self.def_names.name(&def.def_id).unwrap();
for rule in &def.rules {

View File

@ -0,0 +1,5 @@
data Boxed = (Box val)
Bar (*, (Box x y)) = x
main = *

View File

@ -0,0 +1,5 @@
---
source: tests/golden_tests.rs
input_file: tests/golden_tests/compile_file/wrong_ctr_arity.hvm
---
In definition Bar: Arity error. Constructor 'Box' expects 1 fields but was found 2.