Fix more tests and issues

This commit is contained in:
microproofs 2024-10-29 18:12:04 -04:00
parent 7655a6ecbe
commit 6e94d502a7
No known key found for this signature in database
GPG Key ID: 14F93C84DE6AFD17
4 changed files with 75 additions and 91 deletions

View File

@ -2485,7 +2485,7 @@ impl<'a> CodeGenerator<'a> {
AirTree::clause( AirTree::clause(
test_subject_name.clone(), test_subject_name.clone(),
case.get_air_pattern(), case.get_air_pattern(current_tipo.clone()),
current_tipo.clone(), current_tipo.clone(),
case_air, case_air,
AirTree::anon_func(vec![], acc, true), AirTree::anon_func(vec![], acc, true),

View File

@ -53,18 +53,6 @@ impl ToString for Path {
} }
} }
// impl Display for Path {
// fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
// match self {
// Path::Pair(i) => write!(f, "Pair({})", i),
// Path::Tuple(i) => write!(f, "Tuple({})", i),
// Path::Constr(_, i) => write!(f, "Constr({})", i),
// Path::List(i) => write!(f, "List({})", i),
// Path::ListTail(i) => write!(f, "ListTail({})", i),
// }
// }
// }
impl PartialEq for Path { impl PartialEq for Path {
fn eq(&self, other: &Self) -> bool { fn eq(&self, other: &Self) -> bool {
match (self, other) { match (self, other) {
@ -115,9 +103,15 @@ pub enum CaseTest {
} }
impl CaseTest { impl CaseTest {
pub fn get_air_pattern(&self) -> AirTree { pub fn get_air_pattern(&self, current_type: Rc<Type>) -> AirTree {
match self { match self {
CaseTest::Constr(i) => AirTree::int(i), CaseTest::Constr(i) => {
if current_type.is_bool() {
AirTree::bool(1 == *i)
} else {
AirTree::int(i)
}
}
CaseTest::Int(i) => AirTree::int(i), CaseTest::Int(i) => AirTree::int(i),
CaseTest::Bytes(vec) => AirTree::byte_array(vec.clone()), CaseTest::Bytes(vec) => AirTree::byte_array(vec.clone()),
CaseTest::List(_) => unreachable!(), CaseTest::List(_) => unreachable!(),
@ -839,13 +833,14 @@ impl<'a, 'b> TreeGen<'a, 'b> {
// Add inner patterns to existing row // Add inner patterns to existing row
let mut new_cols = remaining_patts.into_iter().flat_map(|x| x.1).collect_vec(); let mut new_cols = remaining_patts.into_iter().flat_map(|x| x.1).collect_vec();
let added_columns = new_cols.len();
// Pop off tail so that it aligns more easily with other list patterns
if matches!(case, CaseTest::ListWithTail(_)) { if matches!(case, CaseTest::ListWithTail(_)) {
new_cols.pop(); new_cols.pop();
} }
let added_columns = new_cols.len();
// Pop off tail so that it aligns more easily with other list patterns
new_cols.extend(row.columns); new_cols.extend(row.columns);
row.columns = new_cols; row.columns = new_cols;

View File

@ -23,10 +23,11 @@ pub enum Builtin {
impl PartialEq for Builtin { impl PartialEq for Builtin {
fn eq(&self, other: &Self) -> bool { fn eq(&self, other: &Self) -> bool {
match (self, other) { match (self, other) {
(Builtin::HeadList(_), Builtin::HeadList(_)) => true, (Builtin::HeadList(_), Builtin::HeadList(_))
(Builtin::TailList, Builtin::TailList) => true, | (Builtin::TailList, Builtin::TailList)
(Builtin::UnConstrFields, Builtin::UnConstrFields) => true, | (Builtin::UnConstrFields, Builtin::UnConstrFields)
(Builtin::SndPair(_), Builtin::SndPair(_)) => true, | (Builtin::FstPair(_), Builtin::FstPair(_))
| (Builtin::SndPair(_), Builtin::SndPair(_)) => true,
_ => false, _ => false,
} }
} }
@ -112,7 +113,7 @@ impl Builtins {
match i { match i {
Path::Pair(i) => { Path::Pair(i) => {
if i == 0 { if i == 0 {
builtins.push(Builtin::HeadList(get_tipo_by_path( builtins.push(Builtin::FstPair(get_tipo_by_path(
subject_tipo.clone(), subject_tipo.clone(),
&rebuilt_path, &rebuilt_path,
))); )));

View File

@ -1484,11 +1484,11 @@ fn acceptance_test_12_filter_even() {
.apply(Term::var("rest")), .apply(Term::var("rest")),
) )
.lambda("rest") .lambda("rest")
.apply(Term::tail_list().apply(Term::var("xs")))
.lambda("x") .lambda("x")
.apply(Term::un_i_data().apply( .apply(Term::un_i_data().apply(
Term::head_list().apply(Term::var("xs")), Term::head_list().apply(Term::var("xs")),
)), ))
.apply(Term::tail_list().apply(Term::var("xs"))),
) )
.lambda("xs") .lambda("xs")
.lambda("filter"), .lambda("filter"),
@ -2154,53 +2154,41 @@ fn acceptance_test_23_to_list() {
Term::head_list() Term::head_list()
.apply(Term::var("elems")) .apply(Term::var("elems"))
.as_var("elem_0", |elem_0| { .as_var("elem_0", |elem_0| {
Term::tail_list()
.apply(Term::var("elems"))
.as_var("rest", |rest| {
Term::un_b_data()
.apply(Term::fst_pair().apply(Term::Var(elem_0.clone())))
.as_var("k2", |k2| {
Term::un_i_data()
.apply(Term::snd_pair().apply(Term::Var(elem_0.clone())))
.as_var("v2", |v2| {
Term::equals_bytestring() Term::equals_bytestring()
.apply(Term::var("k")) .apply(Term::var("k"))
.apply(Term::Var(k2.clone())) .apply(Term::var("k2"))
.delayed_if_then_else( .delayed_if_then_else(
Term::mk_cons() Term::mk_cons()
.apply( .apply(
Term::mk_pair_data() Term::mk_pair_data()
.apply( .apply(Term::b_data().apply(Term::var("k")))
Term::b_data() .apply(Term::i_data().apply(Term::var("v"))),
.apply(Term::var("k")),
) )
.apply( .apply(Term::var("rest")),
Term::i_data()
.apply(Term::var("v")),
),
)
.apply(Term::Var(rest.clone())),
Term::mk_cons() Term::mk_cons()
.apply( .apply(
Term::mk_pair_data() Term::mk_pair_data()
.apply( .apply(Term::b_data().apply(Term::var("k2")))
Term::b_data() .apply(Term::i_data().apply(Term::var("v2"))),
.apply(Term::Var(k2)),
)
.apply(
Term::i_data()
.apply(Term::Var(v2)),
),
) )
.apply( .apply(
Term::var("do_insert") Term::var("do_insert")
.apply(Term::var("do_insert")) .apply(Term::var("do_insert"))
.apply(Term::Var(rest)), .apply(Term::var("rest")),
), ),
) )
}) .lambda("rest")
}) .lambda("v2")
}) .lambda("k2")
.apply(
Term::un_b_data()
.apply(Term::fst_pair().apply(Term::Var(elem_0.clone()))),
)
.apply(
Term::un_i_data()
.apply(Term::snd_pair().apply(Term::Var(elem_0.clone()))),
)
.apply(Term::tail_list().apply(Term::var("elems")))
}), }),
) )
.lambda("elems") .lambda("elems")
@ -2852,9 +2840,9 @@ fn acceptance_test_28_unique_empty_list() {
), ),
) )
.lambda("rest") .lambda("rest")
.apply(Term::tail_list().apply(Term::var("xs")))
.lambda("x") .lambda("x")
.apply(Term::head_list().apply(Term::var("xs"))), .apply(Term::head_list().apply(Term::var("xs")))
.apply(Term::tail_list().apply(Term::var("xs"))),
) )
.lambda("xs") .lambda("xs")
.lambda("unique"), .lambda("unique"),
@ -2882,9 +2870,9 @@ fn acceptance_test_28_unique_empty_list() {
.apply(Term::var("rest")), .apply(Term::var("rest")),
) )
.lambda("rest") .lambda("rest")
.apply(Term::tail_list().apply(Term::var("xs")))
.lambda("x") .lambda("x")
.apply(Term::head_list().apply(Term::var("xs"))), .apply(Term::head_list().apply(Term::var("xs")))
.apply(Term::tail_list().apply(Term::var("xs"))),
) )
.lambda("xs") .lambda("xs")
.lambda("filter"), .lambda("filter"),
@ -2960,12 +2948,12 @@ fn acceptance_test_28_unique_list() {
), ),
) )
.lambda("rest") .lambda("rest")
.apply(Term::tail_list().apply(Term::var("xs")))
.lambda("x") .lambda("x")
.apply( .apply(
Term::un_i_data() Term::un_i_data()
.apply(Term::head_list().apply(Term::var("xs"))), .apply(Term::head_list().apply(Term::var("xs"))),
), )
.apply(Term::tail_list().apply(Term::var("xs"))),
) )
.lambda("xs") .lambda("xs")
.lambda("unique"), .lambda("unique"),
@ -2995,11 +2983,11 @@ fn acceptance_test_28_unique_list() {
.apply(Term::var("rest")), .apply(Term::var("rest")),
) )
.lambda("rest") .lambda("rest")
.apply(Term::tail_list().apply(Term::var("xs")))
.lambda("x") .lambda("x")
.apply(Term::un_i_data().apply( .apply(Term::un_i_data().apply(
Term::head_list().apply(Term::var("xs")), Term::head_list().apply(Term::var("xs")),
)), ))
.apply(Term::tail_list().apply(Term::var("xs"))),
) )
.lambda("xs") .lambda("xs")
.lambda("filter"), .lambda("filter"),
@ -3363,19 +3351,19 @@ fn acceptance_test_29_union_tuple() {
.apply(Term::var("k")) .apply(Term::var("k"))
.apply(Term::var("v")), .apply(Term::var("v")),
) )
.lambda("rest")
.lambda("v") .lambda("v")
.lambda("k")
.apply(
Term::un_b_data()
.apply(Term::head_list().apply(Term::var("tuple"))),
)
.apply( .apply(
Term::un_i_data() Term::un_i_data()
.apply(Term::head_list().apply( .apply(Term::head_list().apply(
Term::tail_list().apply(Term::var("tuple")), Term::tail_list().apply(Term::var("tuple")),
)), )),
) )
.lambda("k")
.apply(
Term::un_b_data()
.apply(Term::head_list().apply(Term::var("tuple"))),
)
.lambda("rest")
.apply(Term::tail_list().apply(Term::var("left"))) .apply(Term::tail_list().apply(Term::var("left")))
.lambda("tuple") .lambda("tuple")
.apply( .apply(
@ -3461,19 +3449,19 @@ fn acceptance_test_29_union_tuple() {
.apply(Term::var("rest")), .apply(Term::var("rest")),
), ),
) )
.lambda("rest")
.lambda("v2") .lambda("v2")
.apply(Term::un_i_data().apply(
Term::head_list().apply(
Term::tail_list().apply(Term::var("tuple")),
),
))
.lambda("k2") .lambda("k2")
.apply( .apply(
Term::un_b_data().apply( Term::un_b_data().apply(
Term::head_list().apply(Term::var("tuple")), Term::head_list().apply(Term::var("tuple")),
), ),
) )
.lambda("rest") .apply(Term::un_i_data().apply(
Term::head_list().apply(
Term::tail_list().apply(Term::var("tuple")),
),
))
.apply(Term::tail_list().apply(Term::var("elems"))) .apply(Term::tail_list().apply(Term::var("elems")))
.lambda("tuple") .lambda("tuple")
.apply(Term::unlist_data().apply( .apply(Term::unlist_data().apply(