Skip to content

Commit f4330df

Browse files
nikomatsakisnikomatsakis
committed
add max_size field to Program
1 parent 7c8908d commit f4330df

File tree

7 files changed

+66
-71
lines changed

7 files changed

+66
-71
lines changed

‎crates/formality-prove/src/program.rs

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -6,10 +6,11 @@ use formality_types::{
66

77
#[term]
88
pub struct Program {
9-
trait_decls: Vec<TraitDecl>,
10-
impl_decls: Vec<ImplDecl>,
11-
alias_eq_decls: Vec<AliasEqDecl>,
12-
alias_bound_decls: Vec<AliasBoundDecl>,
9+
pub max_size: usize,
10+
pub trait_decls: Vec<TraitDecl>,
11+
pub impl_decls: Vec<ImplDecl>,
12+
pub alias_eq_decls: Vec<AliasEqDecl>,
13+
pub alias_bound_decls: Vec<AliasBoundDecl>,
1314
}
1415

1516
impl Program {

‎crates/formality-prove/src/test.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,7 @@ mod universes;
1919
/// Returns the constraints that result from proving assumptions/goals. These will reference
2020
/// existential variables created for the bindings, so they're really just suitable for
2121
/// using with expect.
22-
fn test_prove(program: &Program, t: Binder<(Wcs, Wcs)>) -> Set<Binder<Constraints>> {
22+
fn test_prove(program: Program, t: Binder<(Wcs, Wcs)>) -> Set<Binder<Constraints>> {
2323
let (assumptions, goals) =
2424
t.instantiate(|kind, var_index| InferenceVar { kind, var_index }.upcast());
2525
prove_wc_list(program, assumptions, goals)

‎crates/formality-prove/src/test/eq_partial_eq.rs

Lines changed: 15 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -8,22 +8,24 @@ use formality_types::{
88
use crate::{program::Program, prove::prove_wc_list};
99

1010
/// Simple example program consisting only of two trait declarations.
11-
const EQ_PARTIAL_EQ: &str = "
12-
program(
13-
[trait Eq<ty Self> where {is_implemented(PartialEq(Self))},
14-
trait PartialEq<ty Self> where {}],
15-
[],
16-
[],
17-
[]
18-
)
19-
";
11+
fn program() -> Program {
12+
Program {
13+
max_size: 22,
14+
trait_decls: vec![
15+
term("trait Eq<ty Self> where {is_implemented(PartialEq(Self))}"),
16+
term("trait PartialEq<ty Self> where {}"),
17+
],
18+
impl_decls: vec![],
19+
alias_eq_decls: vec![],
20+
alias_bound_decls: vec![],
21+
}
22+
}
2023

2124
#[test]
2225
fn eq_implies_partial_eq() {
23-
let program: Program = term(EQ_PARTIAL_EQ);
2426
let assumptions: Wcs = Wcs::t();
2527
let goal: Wc = term("for<ty T> if {is_implemented(Eq(T))} is_implemented(PartialEq(T))");
26-
let constraints = prove_wc_list(program, assumptions, goal);
28+
let constraints = prove_wc_list(program(), assumptions, goal);
2729
expect![[r#"
2830
{
2931
<> Constraints { known_true: true, substitution: Substitution { map: {} } },
@@ -34,10 +36,9 @@ fn eq_implies_partial_eq() {
3436

3537
#[test]
3638
fn not_partial_eq_implies_eq() {
37-
let program: Program = term(EQ_PARTIAL_EQ);
3839
let assumptions: Wcs = Wcs::t();
3940
let goal: Wc = term("for<ty T> if {is_implemented(PartialEq(T))} is_implemented(Eq(T))");
40-
let constraints = prove_wc_list(program, assumptions, goal);
41+
let constraints = prove_wc_list(program(), assumptions, goal);
4142
expect![[r#"
4243
{}
4344
"#]]
@@ -46,10 +47,9 @@ fn not_partial_eq_implies_eq() {
4647

4748
#[test]
4849
fn placeholders_not_eq() {
49-
let program: Program = term(EQ_PARTIAL_EQ);
5050
let assumptions: Wcs = Wcs::t();
5151
let goal: Wc = term("for<ty T, ty U> if {is_implemented(Eq(T))} is_implemented(PartialEq(U))");
52-
let constraints = prove_wc_list(program, assumptions, goal);
52+
let constraints = prove_wc_list(program(), assumptions, goal);
5353
expect![[r#"
5454
{}
5555
"#]]

‎crates/formality-prove/src/test/exists_constraints.rs

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -7,20 +7,20 @@ use crate::program::Program;
77
use super::test_prove;
88

99
/// Simple example program consisting only of two trait declarations.
10-
const PROGRAM: &str = "
11-
program(
12-
[trait Foo<ty Self> where {}],
13-
[impl<ty T> Foo(Vec<T>) where {}],
14-
[],
15-
[]
16-
)
17-
";
10+
fn program() -> Program {
11+
Program {
12+
max_size: 22,
13+
trait_decls: vec![term("trait Foo<ty Self> where {}")],
14+
impl_decls: vec![term("impl<ty T> Foo(Vec<T>) where {}")],
15+
alias_eq_decls: vec![],
16+
alias_bound_decls: vec![],
17+
}
18+
}
1819

1920
/// Test that `exists<T> is_implemented(Foo(U))` yields `U = Vec<X>` for some fresh `X`
2021
#[test]
2122
fn exists_u_for_t() {
22-
let program: Program = term(PROGRAM);
23-
let constraints = test_prove(&program, term("<ty U> ({}, {is_implemented(Foo(U))})"));
23+
let constraints = test_prove(program(), term("<ty U> ({}, {is_implemented(Foo(U))})"));
2424
expect![[r#"
2525
{
2626
<ty> Constraints { known_true: true, substitution: Substitution { map: {?ty_0: (rigid (adt Vec) ^ty0_0)} } },

‎crates/formality-prove/src/test/occurs_check.rs

Lines changed: 12 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -7,20 +7,20 @@ use crate::program::Program;
77
use super::test_prove;
88

99
/// Simple example program consisting only of two trait declarations.
10-
const PROGRAM: &str = "
11-
program(
12-
[trait Foo<ty Self> where {}],
13-
[impl<ty T> Foo(Vec<T>) where {}],
14-
[],
15-
[]
16-
)
17-
";
10+
fn program() -> Program {
11+
Program {
12+
max_size: 22,
13+
trait_decls: vec![term("trait Foo<ty Self> where {}")],
14+
impl_decls: vec![term("impl<ty T> Foo(Vec<T>) where {}")],
15+
alias_eq_decls: vec![],
16+
alias_bound_decls: vec![],
17+
}
18+
}
1819

1920
/// Test that `X = Vec<X>` cannot be solved
2021
#[test]
2122
fn direct_cycle() {
22-
let program: Program = term(PROGRAM);
23-
let constraints = test_prove(&program, term("<ty A> ({}, {equals(A, Vec<A>)})"));
23+
let constraints = test_prove(program(), term("<ty A> ({}, {equals(A, Vec<A>)})"));
2424
expect![[r#"
2525
{}
2626
"#]]
@@ -30,9 +30,8 @@ fn direct_cycle() {
3030
/// Test that `X = Vec<X>` cannot be solved (when constructed over several steps)
3131
#[test]
3232
fn indirect_cycle_1() {
33-
let program: Program = term(PROGRAM);
3433
let constraints = test_prove(
35-
&program,
34+
program(),
3635
term("<ty A, ty B> ({}, {equals(A, Vec<B>), equals(B, A)})"),
3736
);
3837
expect![[r#"
@@ -44,9 +43,8 @@ fn indirect_cycle_1() {
4443
/// Test that `X = Vec<X>` cannot be solved (when constructed over several steps)
4544
#[test]
4645
fn indirect_cycle_2() {
47-
let program: Program = term(PROGRAM);
4846
let constraints = test_prove(
49-
&program,
47+
program(),
5048
term("<ty A, ty B> ({}, {equals(B, A), equals(A, Vec<B>)})"),
5149
);
5250
expect![[r#"

‎crates/formality-prove/src/test/simple_impl.rs

Lines changed: 13 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -8,26 +8,24 @@ use formality_types::{
88
use crate::{program::Program, prove::prove_wc_list};
99

1010
/// Simple example program consisting only of two trait declarations.
11-
const PROGRAM: &str = "
12-
program(
13-
[
14-
trait Debug<ty Self> where {},
11+
fn program() -> Program {
12+
Program {
13+
max_size: 22,
14+
trait_decls: vec![term("trait Debug<ty Self> where {}")],
15+
impl_decls: vec![
16+
term("impl<ty T> Debug(Vec<T>) where {is_implemented(Debug(T))}"),
17+
term("impl<> Debug(u32) where {}"),
1518
],
16-
[
17-
impl<ty T> Debug(Vec<T>) where {is_implemented(Debug(T))},
18-
impl<> Debug(u32) where {},
19-
],
20-
[],
21-
[]
22-
)
23-
";
19+
alias_eq_decls: vec![],
20+
alias_bound_decls: vec![],
21+
}
22+
}
2423

2524
#[test]
2625
fn vec_u32_debug() {
27-
let program: Program = term(PROGRAM);
2826
let assumptions: Wcs = Wcs::t();
2927
let goal: Wc = term("is_implemented(Debug(Vec<u32>))");
30-
let constraints = prove_wc_list(program, assumptions, goal);
28+
let constraints = prove_wc_list(program(), assumptions, goal);
3129
expect![[r#"
3230
{
3331
<> Constraints { known_true: true, substitution: Substitution { map: {} } },
@@ -38,10 +36,9 @@ fn vec_u32_debug() {
3836

3937
#[test]
4038
fn vec_vec_u32_debug() {
41-
let program: Program = term(PROGRAM);
4239
let assumptions: Wcs = Wcs::t();
4340
let goal: Wc = term("is_implemented(Debug(Vec<Vec<u32>>))");
44-
let constraints = prove_wc_list(program, assumptions, goal);
41+
let constraints = prove_wc_list(program(), assumptions, goal);
4542
expect![[r#"
4643
{
4744
<> Constraints { known_true: true, substitution: Substitution { map: {} } },

‎crates/formality-prove/src/test/universes.rs

Lines changed: 10 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -5,21 +5,20 @@ use formality_types::parse::term;
55
use crate::program::Program;
66

77
/// Simple example program consisting only of two trait declarations.
8-
const PROGRAM: &str = "
9-
program(
10-
[],
11-
[],
12-
[],
13-
[]
14-
)
15-
";
8+
fn program() -> Program {
9+
Program {
10+
max_size: 22,
11+
trait_decls: vec![],
12+
impl_decls: vec![],
13+
alias_eq_decls: vec![],
14+
alias_bound_decls: vec![],
15+
}
16+
}
1617

1718
/// There is no U that is equal to all T.
1819
#[test]
1920
fn exists_u_for_t() {
20-
let program: Program = term(PROGRAM);
21-
22-
let constraints = super::test_prove(&program, term("<ty U> ({}, {for<ty T> equals(T, U)})"));
21+
let constraints = super::test_prove(program(), term("<ty U> ({}, {for<ty T> equals(T, U)})"));
2322
expect![[r#"
2423
{}
2524
"#]]

0 commit comments

Comments
 (0)