fix: headlist builtin on assoc lists

implement chooseunit for 0 args
This commit is contained in:
microproofs 2024-01-13 18:55:39 -05:00 committed by Kasey
parent c7af27a6ba
commit d26524048e
2 changed files with 32 additions and 22 deletions

View File

@ -3770,14 +3770,25 @@ impl<'a> CodeGenerator<'a> {
builder::special_case_builtin(builtin, 0, vec![])
}
DefaultFunction::FstPair
| DefaultFunction::SndPair
| DefaultFunction::HeadList => builder::undata_builtin(
DefaultFunction::FstPair | DefaultFunction::SndPair => {
builder::undata_builtin(
builtin,
0,
&constructor.tipo.return_type().unwrap(),
vec![],
),
)
}
DefaultFunction::HeadList
if !constructor.tipo.return_type().unwrap().is_2_tuple() =>
{
builder::undata_builtin(
builtin,
0,
&constructor.tipo.return_type().unwrap(),
vec![],
)
}
DefaultFunction::MkCons | DefaultFunction::MkPairData => {
unimplemented!("MkCons and MkPairData should be handled by an anon function or using [] or ( a, b, .., z).\n")
@ -4164,9 +4175,11 @@ impl<'a> CodeGenerator<'a> {
builder::special_case_builtin(&func, count, arg_vec)
}
DefaultFunction::FstPair
| DefaultFunction::SndPair
| DefaultFunction::HeadList => {
DefaultFunction::FstPair | DefaultFunction::SndPair => {
builder::undata_builtin(&func, count, tipo, arg_vec)
}
DefaultFunction::HeadList if !tipo.is_2_tuple() => {
builder::undata_builtin(&func, count, tipo, arg_vec)
}

View File

@ -1543,7 +1543,14 @@ pub fn special_case_builtin(
mut args: Vec<Term<Name>>,
) -> Term<Name> {
match func {
DefaultFunction::IfThenElse
DefaultFunction::ChooseUnit if count > 0 => {
let term = args.pop().unwrap();
let unit = args.pop().unwrap();
term.lambda("_").apply(unit)
}
DefaultFunction::ChooseUnit
| DefaultFunction::IfThenElse
| DefaultFunction::ChooseList
| DefaultFunction::ChooseData
| DefaultFunction::Trace => {
@ -1580,16 +1587,6 @@ pub fn special_case_builtin(
term
}
DefaultFunction::ChooseUnit => {
if count == 0 {
unimplemented!("Honestly, why are you doing this?")
} else {
let term = args.pop().unwrap();
let unit = args.pop().unwrap();
term.lambda("_").apply(unit)
}
}
DefaultFunction::UnConstrData => {
let mut term: Term<Name> = (*func).into();