Skip to content

Refactor ty_is_int #200

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 16 commits into
base: main
Choose a base branch
from
Open

Refactor ty_is_int #200

Show file tree
Hide file tree
Changes from 5 commits
Commits
Show all changes
16 commits
Select commit Hold shift + click to select a range
a889ecd
UPDATE_EXPECT=1 for the failing test in main
tiif Aug 12, 2025
992f4c2
Write down the rules
tiif Aug 11, 2025
9980d0e
Use prove_goal to check if the type is int
tiif Aug 11, 2025
6ee4489
Update tests
tiif Aug 11, 2025
4379ad6
fmt
tiif Aug 12, 2025
652dba9
remove spurious change
tiif Aug 12, 2025
331c737
Experiment with projection
tiif Aug 12, 2025
e237c2d
fmt
tiif Aug 12, 2025
df0fe30
Remove spurious change
tiif Aug 12, 2025
c0fbd8b
Make is_int work with normalization
tiif Aug 12, 2025
c7f3363
Add an extra rule for rigidty
tiif Aug 12, 2025
582560e
Slightly tweak the logic
tiif Aug 12, 2025
1f601cf
Refactor ty_is_int
tiif Aug 15, 2025
33d8a48
remove fn is_alias
tiif Aug 15, 2025
afd30d2
support one-off judgments in type check
nikomatsakis Aug 15, 2025
130f628
Update crates/formality-check/src/mini_rust_check.rs
nikomatsakis Aug 15, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 2 additions & 5 deletions crates/formality-check/src/mini_rust_check.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,8 +6,7 @@ use formality_rust::grammar::minirust::ArgumentExpression::{ByValue, InPlace};
use formality_rust::grammar::minirust::PlaceExpression::Local;
use formality_rust::grammar::minirust::ValueExpression::{Constant, Fn, Load};
use formality_rust::grammar::minirust::{
self, ty_is_int, ArgumentExpression, BasicBlock, BbId, LocalId, PlaceExpression,
ValueExpression,
self, ArgumentExpression, BasicBlock, BbId, LocalId, PlaceExpression, ValueExpression,
};
use formality_rust::grammar::FnBoundData;
use formality_types::grammar::{CrateId, FnId};
Expand Down Expand Up @@ -229,9 +228,7 @@ impl Check<'_> {
// Check if the value is well-formed.
let value_ty = self.check_value(typeck_env, switch_value).unwrap();

if !ty_is_int(value_ty) {
bail!("The value used for switch must be an int.");
}
self.prove_goal(&typeck_env.env, Wcs::default(), value_ty.is_int())?;
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I personally don't like introducing a new judgement for this. I think if we want this check to be a proper judgement maybe add a builtin trait and prove value_ty: BuiltinInteger here 🤔

Even if it's a proper judegement:tm: but instead be just something else you can prove. Predicates feel core to the type system in a way in which "is this an integer" does not. That's just my personal vibe here though

What's the reasoning behind changing an assertion to an actual goal?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The reason of changing this to a goal is I feel we should have a way to say "this type is an int" somewhere instead of having this function https://github.com/rust-lang/a-mir-formality/pull/200/files#diff-b58482e54c5aa3c63282fc2a3a0aa88194e826004773bd7bc9e385f29b5c3e0d

But I do agree that adding a predicate for this might be an overkill.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

could we instead just use a "non-predicate" judgement here. Same as we do for trait_ref_is_knowable or however it's called?

Copy link
Member Author

@tiif tiif Aug 15, 2025 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Oh, I forgot to mention that I was using a Relation instead of Predicate.

From my understanding, we can only use a judgment_fn! through prove_wc, and when we call prove_wc, we need to pick one of the below as the Wc type:

pub enum WcData {
    /// Means the built-in relation holds.
    #[cast]
    Relation(Relation),

    /// Means the predicate holds.
    #[cast]
    Predicate(Predicate),

    // Equivalent to `for<'a>` except that it can also express `for<ty T>` and so forth:
    // means `$v0` is true for any value of the bound variables (e.g., `'a` or `T`).
    #[grammar(for $v0)]
    ForAll(Binder<Wc>),

    #[grammar(if $v0 $v1)]
    Implies(Wcs, Wc),
}

Relation looks the most reasonable to me among all of them.


// Ensure all bbid are valid.
for switch_target in switch_targets {
Expand Down
19 changes: 19 additions & 0 deletions crates/formality-prove/src/prove/is_local.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -316,6 +316,25 @@ judgment_fn! {
}
}

judgment_fn! {
fn is_int(
_decls: Decls,
env: Env,
assumptions: Wcs,
goal: Parameter,
) => Constraints {
debug(goal, assumptions, env)

(
(if id.is_int())
------- ("is int")
(is_int(_decls, env, _assumptions, RigidTy {name: RigidName::ScalarId(id), parameters: _}) => Constraints::none(env))
)

}

}

fn is_fundamental(_decls: &Decls, name: &RigidName) -> bool {
// From https://rust-lang.github.io/rfcs/2451-re-rebalancing-coherence.html:
//
Expand Down
9 changes: 6 additions & 3 deletions crates/formality-prove/src/prove/minimize/test.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,12 +17,14 @@ fn minimize_a() {
let (env, subst) = env.existential_substitution(&term);
let term = term.instantiate_with(&subst).unwrap();

expect!["(Env { variables: [?ty_1, ?ty_2, ?ty_3], bias: Soundness }, [?ty_1, ?ty_3])"]
.assert_eq(&format!("{:?}", (&env, &term)));
expect![
"(Env { variables: [?ty_1, ?ty_2, ?ty_3], bias: Soundness, pending: [] }, [?ty_1, ?ty_3])"
]
.assert_eq(&format!("{:?}", (&env, &term)));

let (mut env_min, term_min, m) = minimize(env, term);

expect!["(Env { variables: [?ty_0, ?ty_1], bias: Soundness }, [?ty_0, ?ty_1])"]
expect!["(Env { variables: [?ty_0, ?ty_1], bias: Soundness, pending: [] }, [?ty_0, ?ty_1])"]
.assert_eq(&format!("{:?}", (&env_min, &term_min)));

let ty0 = term_min[0].as_variable().unwrap();
Expand Down Expand Up @@ -51,6 +53,7 @@ fn minimize_a() {
?ty_3,
],
bias: Soundness,
pending: [],
},
known_true: true,
substitution: {
Expand Down
29 changes: 28 additions & 1 deletion crates/formality-prove/src/prove/prove_wc.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,9 @@ use crate::{
};

use super::constraints::Constraints;
use formality_types::grammar::Parameter::Ty;
use formality_types::grammar::Parameter::{self, Ty};
use formality_types::grammar::RigidName;
use formality_types::grammar::RigidTy;

judgment_fn! {
/// The "heart" of the trait system -- prove that a where-clause holds given a set of declarations, variable environment, and set of assumptions.
Expand Down Expand Up @@ -145,5 +147,30 @@ judgment_fn! {
----------------------------- ("const has ty")
(prove_wc(decls, env, assumptions, Predicate::ConstHasType(ct, ty)) => c)
)

(
(is_int(decl, env, assumptions, ty) => c)
----------------------------- ("ty is int")
(prove_wc(decl, env, assumptions, Relation::IsInt(ty)) => c)
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

how does a-mir-formality handle normalization when proving predicates/relations?

Because right now <u32 as Id>::This fails to satisfy IsInt

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yeah that's true, I did an experiment in 331c737#diff-2ca1246445028c80247cd13d93fd973d22ca55cfb7a76c0903a04c09055d706c and it indeed failed.

The place where normalization is done should be here

a-mir-formality/crates/formality-prove/src/prove/prove_normalize.rs

Line 17 in 8b130f7

pub fn prove_normalize(

It is possible to use prove_normalize when proving a goal, for example:

a-mir-formality/crates/formality-prove/src/prove/is_local.rs

Lines 288 to 295 in 8b130f7

(
(prove_normalize(&decls, env, &assumptions, goal) => (c1, p))
(let assumptions = c1.substitution().apply(&assumptions))
(is_local_parameter(&decls, c1.env(), assumptions, p) => c2)
--- ("local parameter")
(is_local_parameter(decls, env, assumptions, goal) => c1.seq(c2))
)

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

But with the change in c0fbd8b, it is possible to make IsInt work with normalization.

)
}
}

judgment_fn! {
pub fn is_int(
_decls: Decls,
env: Env,
assumptions: Wcs,
goal: Parameter,
) => Constraints {
debug(goal, assumptions, env)

(
(if id.is_int())
------- ("is int")
(is_int(_decls, env, _assumptions, RigidTy {name: RigidName::ScalarId(id), parameters: _}) => Constraints::none(env))
)

}

}
17 changes: 9 additions & 8 deletions crates/formality-prove/src/test/adt_wf.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,7 @@ fn well_formed_adt() {
env: Env {
variables: [],
bias: Soundness,
pending: [],
},
known_true: true,
substitution: {},
Expand All @@ -51,21 +52,21 @@ fn not_well_formed_adt() {
assumptions,
Relation::WellFormed(goal),
).assert_err(expect![[r#"
judgment `prove { goal: {@ wf(X<u64>)}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo <ty> ], [impl Foo(u32)], [], [], [], [adt X <ty> where {Foo(^ty0_0)}], {}, {}) }` failed at the following rule(s):
judgment `prove { goal: {@ wf(X<u64>)}, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] }, decls: decls(222, [trait Foo <ty> ], [impl Foo(u32)], [], [], [], [adt X <ty> where {Foo(^ty0_0)}], {}, {}) }` failed at the following rule(s):
failed at (src/file.rs:LL:CC) because
judgment `prove_wc_list { goal: {@ wf(X<u64>)}, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s):
judgment `prove_wc_list { goal: {@ wf(X<u64>)}, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] } }` failed at the following rule(s):
the rule "some" failed at step #0 (src/file.rs:LL:CC) because
judgment `prove_wc { goal: @ wf(X<u64>), assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s):
judgment `prove_wc { goal: @ wf(X<u64>), assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] } }` failed at the following rule(s):
the rule "parameter well formed" failed at step #0 (src/file.rs:LL:CC) because
judgment `prove_wf { goal: X<u64>, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s):
judgment `prove_wf { goal: X<u64>, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] } }` failed at the following rule(s):
the rule "ADT" failed at step #3 (src/file.rs:LL:CC) because
judgment `prove_after { constraints: Constraints { env: Env { variables: [], bias: Soundness }, known_true: true, substitution: {} }, goal: {Foo(u64)}, assumptions: {} }` failed at the following rule(s):
judgment `prove_after { constraints: Constraints { env: Env { variables: [], bias: Soundness, pending: [] }, known_true: true, substitution: {} }, goal: {Foo(u64)}, assumptions: {} }` failed at the following rule(s):
the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because
judgment `prove { goal: {Foo(u64)}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo <ty> ], [impl Foo(u32)], [], [], [], [adt X <ty> where {Foo(^ty0_0)}], {}, {}) }` failed at the following rule(s):
judgment `prove { goal: {Foo(u64)}, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] }, decls: decls(222, [trait Foo <ty> ], [impl Foo(u32)], [], [], [], [adt X <ty> where {Foo(^ty0_0)}], {}, {}) }` failed at the following rule(s):
failed at (src/file.rs:LL:CC) because
judgment `prove_wc_list { goal: {Foo(u64)}, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s):
judgment `prove_wc_list { goal: {Foo(u64)}, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] } }` failed at the following rule(s):
the rule "some" failed at step #0 (src/file.rs:LL:CC) because
judgment `prove_wc { goal: Foo(u64), assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s):
judgment `prove_wc { goal: Foo(u64), assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] } }` failed at the following rule(s):
the rule "trait implied bound" failed at step #0 (src/file.rs:LL:CC) because
expression evaluated to an empty collection: `decls.trait_invariants()`"#]]);
}
Loading
Loading