Support mk_cons builtin

While this builtin is readily available through the Aiken syntax
  `[head, ..tail]`, there's no reason to not support its builtin form
  even though we may not encourage its usage. For completeness and to
  avoid bad surprises, it is now supported.

  Fixes #964.
This commit is contained in:
KtorZ
2024-07-27 11:30:00 +02:00
committed by Kasey
parent bf5a406ffb
commit 1c58da4d86
3 changed files with 122 additions and 56 deletions

View File

@@ -1554,6 +1554,7 @@ pub fn to_data_builtin(
pub fn special_case_builtin(
func: &DefaultFunction,
tipo: Rc<Type>,
count: usize,
mut args: Vec<Term<Name>>,
) -> Term<Name> {
@@ -1564,6 +1565,26 @@ pub fn special_case_builtin(
term.lambda("_").apply(unit)
}
DefaultFunction::MkCons => {
let arg_type = tipo
.arg_types()
.and_then(|generics| generics.first().cloned())
.expect("mk_cons should have (exactly) one type parameter");
if let [head, tail] = &args[..] {
Term::mk_cons()
.apply(if arg_type.is_pair() {
head.clone()
} else {
convert_type_to_data(head.clone(), &arg_type)
})
.apply(tail.clone())
} else {
unreachable!("mk_cons has two arguments.");
}
}
DefaultFunction::ChooseUnit
| DefaultFunction::IfThenElse
| DefaultFunction::ChooseList