Skip to content

Commit

Permalink
(Mostly) fully test constructor generation
Browse files Browse the repository at this point in the history
A few modules were selected to compare their constructors with the generated ones.
  • Loading branch information
edusporto committed Apr 11, 2024
1 parent 67ea1e6 commit e77cdeb
Showing 1 changed file with 36 additions and 21 deletions.
57 changes: 36 additions & 21 deletions src/book/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -206,20 +206,18 @@ mod tests {
Some(nam) => Term::Lam {
era: *era,
nam: nam.clone(),
bod: Box::new(rename_variables(bod, i, uses)),
bod: Box::new(rename_variables(bod, i, uses))
},
None => {
let new_nam = format!("x{i}");
Term::Lam {
era: *era,
nam: new_nam.clone(),
bod: Box::new(rename_variables(bod, i + 1, &uses.update(nam.clone(), new_nam.clone()))),
bod: Box::new(rename_variables(bod, i + 1, &uses.update(nam.clone(), new_nam))),
}
}
},
Term::Var { nam } => {
Term::Var { nam: uses.get(nam).unwrap_or(nam).clone() }
}
Term::Var { nam } => Term::Var { nam: uses.get(nam).unwrap_or(nam).clone() },
_ => apply(t, |t| rename_variables(t, i, uses)),
}
}
Expand All @@ -229,28 +227,45 @@ mod tests {
fn constructor_generation() {
let book_dir = PathBuf::from(env!("CARGO_MANIFEST_DIR")).join("book");
// TODO: test with all books instead of only "Test"
let book = Book::boot(&book_dir.to_string_lossy(), "Test").unwrap();
let modules_to_test = [
"BBT", "BMap", "Bool", "Char", "Cmp", "Empty", "Equal", "List", "Maybe", "Monad", "Nat", "Pair",
"String", "Vector",
];

for module in modules_to_test {
println!("Testing module `{module}`.");
let mut book = Book::boot(&book_dir.to_string_lossy(), module).unwrap();
// Needed because some constructors are loaded as ADT.cons instead of ADT/cons
book.defs = book.defs.into_iter().map(|(key, val)| (key.replace(".", "/"), val)).collect();

for (_, term) in book.defs.iter() {
if let Some(adt) = extract_adt(term).as_adt() {
let full_name = |adt_name: &str, ctr_name: &str| format!("{adt_name}/{ctr_name}");
for (_, term) in book.defs.iter() {
if let Some(adt) = extract_adt(term).as_adt() {
println!("Testing ADT `{}`.", adt.name);
let full_name = |adt_name: &str, ctr_name: &str| format!("{adt_name}/{ctr_name}");

let ctrs: Vec<(&str, &Term)> = adt
.ctrs
.iter()
.map(|ctr| (ctr.name.as_ref(), &book.defs[&full_name(&adt.name, &ctr.name)]))
.collect();
let ctrs: Vec<(&str, &Term)> = adt
.ctrs
.iter()
.map(|ctr| {
let name = full_name(&adt.name, &ctr.name);
(ctr.name.as_ref(), book.defs.get(&name).expect(&format!("couldn't find {name}")))
})
.collect();

for (ctr_name, ctr_term) in ctrs {
let ctr_ref = full_name(&adt.name, ctr_name);
let gen_code = Term::constructor_code((&adt.name, term), &ctr_ref).unwrap();
let gen_term = KindParser::new(&gen_code).parse_def(0, &im::HashMap::new()).unwrap().1;
for (ctr_name, ctr_term) in ctrs {
println!("Testing constructor {ctr_name}");

let ctr_ref = full_name(&adt.name, ctr_name);
let gen_code = Term::constructor_code((&adt.name, term), &ctr_ref).unwrap();
let gen_term = KindParser::new(&gen_code).parse_def(0, &im::HashMap::new()).unwrap().1;

let t1 = rename_variables(ctr_term, 0, &im::HashMap::new());
let t2 = rename_variables(&gen_term, 0, &im::HashMap::new());
assert_eq!(t1.show(), t2.show());
let t1 = rename_variables(ctr_term, 0, &im::HashMap::new());
let t2 = rename_variables(&gen_term, 0, &im::HashMap::new());
assert_eq!(t1.show(), t2.show());
}
}
}
println!();
}
}
}

0 comments on commit e77cdeb

Please sign in to comment.