Skip to content

Rename wc to goal #453

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
System625 wants to merge 2 commits into
base: main
Choose a base branch
from
Open

Rename wc to goal #453

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
b3372d1
Rename `Wc`/`Wcs` to `Goal`/`Goals`
System625 Aug 20, 2026
7eeac9e
Rename the `prove_wc` judgments to `prove_goal`
System625 Aug 20, 2026
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
4 changes: 2 additions & 2 deletions book/src/formality_core/judgment_fn.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -178,9 +178,9 @@ if let Some(Expr::Add(left, right)) = arg1.downcast() {
}
```

If you want to see a real judgement, take a look at the one for proving where clauses:
If you want to see a real judgement, take a look at the one for proving goals:

{judgment}`prove_wc`
{judgment}`prove_goal`

### Handling cycles

Expand Down
4 changes: 2 additions & 2 deletions book/src/formality_rust.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -28,9 +28,9 @@ The different kinds of crate items are dispatched by `check_crate_item`:

## `prove/`

The `prove` module answers Rust-specific goals such as where-clauses, equality, subtyping, and outlives. Checking code calls into `prove` whenever it needs to establish those facts. The main entry point is `prove_wc`:
The `prove` module answers Rust-specific goals such as where-clauses, equality, subtyping, and outlives. Checking code calls into `prove` whenever it needs to establish those facts. The main entry point is `prove_goal`:

{judgment}`prove_wc`
{judgment}`prove_goal`

## Pipeline

Expand Down
6 changes: 3 additions & 3 deletions crates/formality-macros/src/parse.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -752,12 +752,12 @@ fn field_ident_cloned(field: &syn::Field, index: usize) -> TokenStream {
/// Wraps a sequence of struct/tuple bindings in nested `each_nonterminal` calls,
/// separated by commas. Used for `#[cast]` variants and the default `name(a, b)` syntax.
///
/// For example, given bindings `[v0: Wcs, v1: Wcs]` and tail `__p.ok(Prove(v0.clone(), v1.clone()))`:
/// For example, given bindings `[v0: Goals, v1: Goals]` and tail `__p.ok(Prove(v0.clone(), v1.clone()))`:
///
/// ```rust,ignore
/// __p.each_nonterminal(|v0: Wcs, __p| {
/// __p.each_nonterminal(|v0: Goals, __p| {
/// __p.expect_char(',')?;
/// __p.each_nonterminal(|v1: Wcs, __p| {
/// __p.each_nonterminal(|v1: Goals, __p| {
/// __p.ok(Prove(v0.clone(), v1.clone()))
/// })
/// })
Expand Down
24 changes: 12 additions & 12 deletions crates/formality-rust/src/check/borrow_check/env.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,14 +3,14 @@ use std::collections::BTreeSet;
use crate::check::borrow_check::flow_state::{FlowState, PendingOutlives};

use crate::check::borrow_check::outlives::verify_universal_outlives;
use crate::grammar::{Binder, ExistentialVar, Predicate, Ty, UniversalVar, Wcs};
use crate::grammar::{Binder, ExistentialVar, Goals, Predicate, Ty, UniversalVar};
use crate::grammar::{Crates, Parameter};
use crate::prove::{prove_normalize, Constrained, Constraints, Env, Program};
use crate::rust::Fold;
use formality_core::judgment::{FailureLocation, ProofTree, Proven};
use formality_core::{cast_impl, Downcast, DowncastTo, Set, Upcast};

use crate::check::{Debug, ProvenSet, ToWcs, Visit};
use crate::check::{Debug, ProvenSet, ToGoals, Visit};

#[derive(PartialEq, PartialOrd, Eq, Ord, Clone, Hash)]
pub struct TypeckEnv {
Expand Down Expand Up @@ -61,19 +61,19 @@ impl TypeckEnv {
#[track_caller]
pub(crate) fn prove_goal(
&self,
assumptions: impl ToWcs,
assumptions: impl ToGoals,
state: &FlowState,
goal: impl ToWcs + Debug,
goal: impl ToGoals + Debug,
) -> ProvenSet<FlowState> {
let goal: Wcs = goal.to_wcs();
self.prove_judgment(state, assumptions, goal.to_wcs(), crate::prove::prove)
let goal: Goals = goal.to_goals();
self.prove_judgment(state, assumptions, goal.to_goals(), crate::prove::prove)
.map(|(((), state), proof_tree)| (state, proof_tree))
}

#[track_caller]
pub(crate) fn prove_normalize<T>(
&self,
assumptions: impl ToWcs,
assumptions: impl ToGoals,
state: &FlowState,
goal: &T,
) -> ProvenSet<(T, FlowState)>
Expand Down Expand Up @@ -109,16 +109,16 @@ impl TypeckEnv {
fn prove_judgment<G, C, T>(
&self,
state: &FlowState,
assumptions: impl ToWcs,
assumptions: impl ToGoals,
goal: G,
judgment_fn: impl FnOnce(Program, Env, Wcs, G) -> ProvenSet<C>,
judgment_fn: impl FnOnce(Program, Env, Goals, G) -> ProvenSet<C>,
) -> ProvenSet<(T, FlowState)>
where
G: Debug + Visit + Clone,
C: Upcast<Constrained<T>> + Ord + Debug,
T: Clone + Ord + Debug,
{
let assumptions: Wcs = assumptions.to_wcs();
let assumptions: Goals = assumptions.to_goals();

assert!(self.env.encloses((&assumptions, &goal)));

Expand Down Expand Up @@ -255,12 +255,12 @@ impl TypeckEnv {

// Convert the pending goals into a series of `PendingOutlives`.
//
// The `Constraints` struct contains a set of "pending where-clauses"
// The `Constraints` struct contains a set of "pending goals"
// which must still be proven. In practice, the final result of the
// top-level judgments we use in the type checker should only have
// pending outlives requests. This function checks that this is true,
// converting to a set of `PendingOutlives`, and returns `None` if
// any other sort of where-clause is found.
// any other sort of goal is found.
fn convert_to_pending_outlives(&self, c: &Constraints) -> Option<BTreeSet<PendingOutlives>> {
let mut c_outlives = BTreeSet::default();

Expand Down
66 changes: 33 additions & 33 deletions crates/formality-rust/src/check/borrow_check/nll.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,9 +8,9 @@ use crate::check::feature_gate_enabled_in_program;

use crate::grammar::expr::{Block, Expr, Init, Literal, PlaceExpr, Stmt};
use crate::grammar::{
AliasName, AliasTy, AssociatedItemId, ExistentialVar, FeatureGateName, FieldName, Fn, Lt,
Parameter, Predicate, RefKind, RigidName, RigidTy, ScalarId, Struct, StructBoundData, TraitId,
TraitRef, Ty, Variable, VariantId, Wcs, WhereClause,
AliasName, AliasTy, AssociatedItemId, ExistentialVar, FeatureGateName, FieldName, Fn, Goals,
Lt, Parameter, Predicate, RefKind, RigidName, RigidTy, ScalarId, Struct, StructBoundData,
TraitId, TraitRef, Ty, Variable, VariantId, WhereClause,
};
use crate::grammar::{FnBoundData, PredicateTy};
use crate::prove::Safety;
Expand All @@ -20,7 +20,7 @@ use formality_core::{judgment_fn, term, ProvenSet, Set, Union, Upcast};
use crate::check::borrow_check::liveness::{Assignment, Either, LiveBefore, LivePlaces};

// Treats each name brought in by exists as OK to use when checking the code inside.
fn wf_assumptions_for_existential_subst(subst: &[ExistentialVar]) -> Wcs {
fn wf_assumptions_for_existential_subst(subst: &[ExistentialVar]) -> Goals {
subst
.iter()
.map(|v| Predicate::well_formed(v.clone()))
Expand Down Expand Up @@ -128,7 +128,7 @@ judgment_fn! {
/// Prove that any loans issued in this basic block are respected.
pub fn borrow_check(
env: TypeckEnv,
assumptions: Wcs,
assumptions: Goals,
state: FlowState,
block: Block,
) => () {
Expand All @@ -146,7 +146,7 @@ judgment_fn! {
/// Prove that any loans issued in this basic block are respected.
fn borrow_check_block(
env: TypeckEnv,
assumptions: Wcs,
assumptions: Goals,
state: FlowState,
block: Block,
places_live_on_exit: LivePlaces,
Expand Down Expand Up @@ -178,7 +178,7 @@ judgment_fn! {
/// Prove that any loans issued in this statement are respected.
fn borrow_check_statement(
env: TypeckEnv,
assumptions: Wcs,
assumptions: Goals,
state: FlowState,
statement: Stmt,
places_live_on_exit: LivePlaces,
Expand Down Expand Up @@ -352,7 +352,7 @@ judgment_fn! {
/// Prove that any loans issued in this value expression are respected, and return its type.
fn borrow_check_expr_has_ty(
env: TypeckEnv,
assumptions: Wcs,
assumptions: Goals,
state: FlowState,
expr: Expr,
ty: Ty,
Expand All @@ -373,7 +373,7 @@ judgment_fn! {
/// Prove that any loans issued in this value expression are respected, and return its type.
pub fn borrow_check_expr(
env: TypeckEnv,
assumptions: Wcs,
assumptions: Goals,
state: FlowState,
expr: Expr,
places_live_on_exit: LivePlaces,
Expand Down Expand Up @@ -576,7 +576,7 @@ judgment_fn! {
/// Borrow-check a place expression, returning its type.
fn borrow_check_loop(
env: TypeckEnv,
assumptions: Wcs,
assumptions: Goals,
state: FlowState,
body: Block,
places_live_on_exit: LivePlaces,
Expand Down Expand Up @@ -604,7 +604,7 @@ judgment_fn! {
/// Borrow-check a place expression, returning its type.
pub fn borrow_check_place_expr(
env: TypeckEnv,
assumptions: Wcs,
assumptions: Goals,
state: FlowState,
place: PlaceExpr,
) => (TypedPlaceExpr, FlowState) {
Expand Down Expand Up @@ -777,7 +777,7 @@ judgment_fn! {
/// Locals should be provided in reverse declaration order (LIFO drop order).
fn drop_places(
env: TypeckEnv,
assumptions: Wcs,
assumptions: Goals,
state: FlowState,
places: Vec<TypedPlaceExpr>,
places_live_after_drop: LivePlaces,
Expand All @@ -798,7 +798,7 @@ judgment_fn! {
/// Check that the given access is permitted.
fn access_permitted(
env: TypeckEnv,
assumptions: Wcs,
assumptions: Goals,
state: FlowState,
access: Access,
places_live_after_access: LivePlaces,
Expand All @@ -821,7 +821,7 @@ judgment_fn! {
/// Prove that none of the borrows in `borrowed` does not affect `place`.
fn access_permitted_by_loans(
env: TypeckEnv,
assumptions: Wcs,
assumptions: Goals,
state: FlowState,
access: Access,
places_live_after_access: LivePlaces,
Expand All @@ -841,7 +841,7 @@ judgment_fn! {
/// Prove that the borrow `borrow` does not affect `place`.
fn access_permitted_by_loan(
env: TypeckEnv,
assumptions: Wcs,
assumptions: Goals,
state: FlowState,
loan: Loan,
access: Access,
Expand Down Expand Up @@ -934,7 +934,7 @@ judgment_fn! {
/// is treated as a move so overlapping live loans can reject it.
fn access_kind_for_place_use(
env: TypeckEnv,
assumptions: Wcs,
assumptions: Goals,
state: FlowState,
place: TypedPlaceExpr,
) => (AccessKind, FlowState) {
Expand All @@ -957,7 +957,7 @@ judgment_fn! {
/// Prove that a type implements Copy.
fn prove_ty_is_copy(
env: TypeckEnv,
assumptions: Wcs,
assumptions: Goals,
state: FlowState,
ty: Ty,
) => FlowState {
Expand All @@ -981,7 +981,7 @@ judgment_fn! {
/// references (`&T` / `&mut T`) will cause this judgment to fail.
fn prove_place_is_movable(
env: TypeckEnv,
assumptions: Wcs,
assumptions: Goals,
state: FlowState,
place: TypedPlaceExpr,
) => FlowState {
Expand Down Expand Up @@ -1026,7 +1026,7 @@ judgment_fn! {
/// Prove that any loans issued in thes value expressions (evaluated in this order) are respected.
fn prove_ty_is_ref(
env: TypeckEnv,
assumptions: Wcs,
assumptions: Goals,
state: FlowState,
ty: Ty,
) => FlowState {
Expand All @@ -1044,7 +1044,7 @@ judgment_fn! {
/// Prove that any loans issued in thes value expressions (evaluated in this order) are respected.
pub fn prove_ty_is_rigid(
env: TypeckEnv,
assumptions: Wcs,
assumptions: Goals,
state: FlowState,
ty: Ty,
) => (RigidTy, FlowState) {
Expand All @@ -1068,7 +1068,7 @@ judgment_fn! {
/// Prove that `a` is assignable to `b`.
fn prove_assignable(
env: TypeckEnv,
assumptions: Wcs,
assumptions: Goals,
state: FlowState,
a: Ty,
b: Ty,
Expand All @@ -1091,7 +1091,7 @@ judgment_fn! {

fn prove_sub_type(
env: &TypeckEnv,
assumptions: &Wcs,
assumptions: &Goals,
state: &FlowState,
a: impl Upcast<Parameter>,
b: impl Upcast<Parameter>,
Expand All @@ -1101,7 +1101,7 @@ fn prove_sub_type(

fn prove_where_clauses(
env: &TypeckEnv,
assumptions: &Wcs,
assumptions: &Goals,
state: &FlowState,
where_clauses: &[WhereClause],
) -> ProvenSet<FlowState> {
Expand All @@ -1110,7 +1110,7 @@ fn prove_where_clauses(

fn prove_ty_is_wf(
env: &TypeckEnv,
assumptions: &Wcs,
assumptions: &Goals,
state: &FlowState,
ty: &Ty,
) -> ProvenSet<FlowState> {
Expand All @@ -1119,7 +1119,7 @@ fn prove_ty_is_wf(

fn prove_normalize_ty(
env: &TypeckEnv,
assumptions: &Wcs,
assumptions: &Goals,
state: &FlowState,
ty: &Ty,
) -> ProvenSet<(Ty, FlowState)> {
Expand All @@ -1128,7 +1128,7 @@ fn prove_normalize_ty(

fn prove_is_implemented(
env: &TypeckEnv,
assumptions: &Wcs,
assumptions: &Goals,
state: &FlowState,
trait_ref: TraitRef,
) -> ProvenSet<FlowState> {
Expand Down Expand Up @@ -1171,7 +1171,7 @@ judgment_fn! {
/// Prove that the loan does not outlive any universal regions.
fn loan_cannot_outlive_universal_regions(
env: TypeckEnv,
assumptions: Wcs,
assumptions: Goals,
outlives: Set<PendingOutlives>,
loan: Loan,
) => () {
Expand Down Expand Up @@ -1238,7 +1238,7 @@ judgment_fn! {
/// ...show that `place_live` does not require data derived from `x`.
fn loan_not_required_by_live_places(
env: TypeckEnv,
assumptions: Wcs,
assumptions: Goals,
state: FlowState,
loan: Loan,
places_live_after_access: LivePlaces,
Expand Down Expand Up @@ -1267,7 +1267,7 @@ judgment_fn! {
/// ...show that `place_live` does not require data derived from `x`.
fn loan_not_required_by_live_place(
env: TypeckEnv,
assumptions: Wcs,
assumptions: Goals,
outlives: Set<PendingOutlives>,
loan: Loan,
live_place: TypedPlaceExpr,
Expand Down Expand Up @@ -1301,7 +1301,7 @@ judgment_fn! {
/// ...show that `place_live` does not require data derived from `x`.
fn loan_not_required_by_live_place_prefix(
env: TypeckEnv,
assumptions: Wcs,
assumptions: Goals,
outlives: Set<PendingOutlives>,
loan: Loan,
live_place: TypedPlaceExpr,
Expand Down Expand Up @@ -1335,7 +1335,7 @@ judgment_fn! {
/// ...show that `place_live_ty` does not require data derived from `x`.
fn loan_not_required_by_parameter(
env: TypeckEnv,
assumptions: Wcs,
assumptions: Goals,
outlives: Set<PendingOutlives>,
loan: Loan,
live_parameter: Parameter,
Expand Down Expand Up @@ -1444,7 +1444,7 @@ judgment_fn! {
/// Prove that the loan does not outlive any universal regions.
fn loan_cannot_outlive(
env: TypeckEnv,
assumptions: Wcs,
assumptions: Goals,
outlives: Set<PendingOutlives>,
loan: Loan,
lifetime: Lt,
Expand Down Expand Up @@ -1472,7 +1472,7 @@ judgment_fn! {
/// ...show that `place_live_ty` does not require data derived from `x`.
fn loan_not_required_by_parameters(
env: TypeckEnv,
assumptions: Wcs,
assumptions: Goals,
outlives: Set<PendingOutlives>,
loan: Loan,
live_parameters: Vec<Parameter>,
Expand Down
Loading
Loading