language-servers/roc
1
0
Fork 0
mirror of https://github.com/roc-lang/roc.git synced 2025-08-03 19:58:18 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions 6

Merge pull request #4880 from roc-lang/weakening-2

Browse source 
Implement weakening of variables introduced in branch patterns
This commit is contained in:
Ayaz 2023-01-11 16:46:54 -06:00 • committed by GitHub
commit 8bca5840b9
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
3 changed files with 125 additions and 47 deletions
Download patch file Download diff file Expand all files Collapse all files

36
crates/compiler/constrain/src/expr.rs
View file

@ -1055,6 +1055,7 @@ pub fn constrain_expr(
pattern_headers,
pattern_constraints,
body_constraints,
// Never generalize identifiers introduced in branch-patterns
Generalizable(false),
);
@ -2282,6 +2283,7 @@ fn constrain_when_branch_help(
[],
guard_constraint,
ret_constraint,
// Never generalize identifiers introduced in branch guards
Generalizable(false),
);
@ -2399,7 +2401,8 @@ pub fn constrain_decls(
[],
expect_constraint,
constraint,
Generalizable(false),
// TODO(weakening)
Generalizable(true),
)
}
ExpectationFx => {
@ -2427,7 +2430,8 @@ pub fn constrain_decls(
[],
expect_constraint,
constraint,
Generalizable(false),
// TODO(weakening)
Generalizable(true),
)
}
Function(function_def_index) => {
@ -3604,7 +3608,9 @@ pub fn rec_defs_help_simple(
}
_ => true, // this must be a function
});
Generalizable(generalizable)
// TODO(weakening)
#[allow(clippy::logic_bug)]
Generalizable(generalizable || true)
};
for index in range {
@ -3816,15 +3822,17 @@ pub fn rec_defs_help_simple(
/// A let-bound expression is generalizable if it is
/// - a syntactic function under an opaque wrapper
/// - a number literal under an opaque wrapper
fn is_generalizable_expr(mut expr: &Expr) -> bool {
loop {
match expr {
Num(..) | Int(..) | Float(..) => return true,
Closure(_) => return true,
OpaqueRef { argument, .. } => expr = &argument.1.value,
_ => return false,
}
}
fn is_generalizable_expr(_expr: &Expr) -> bool {
// TODO(weakening)
// loop {
// match expr {
// Num(..) | Int(..) | Float(..) => return true,
// Closure(_) => return true,
// OpaqueRef { argument, .. } => expr = &argument.1.value,
// _ => return false,
// }
// }
true
}
fn constrain_recursive_defs(
@ -3858,7 +3866,9 @@ fn rec_defs_help(
let generalizable = defs
.iter()
.all(|d| is_generalizable_expr(&d.loc_expr.value));
Generalizable(generalizable)
// TODO(weakening)
#[allow(clippy::logic_bug)]
Generalizable(generalizable || true)
};
for def in defs {

113
crates/compiler/solve/src/solve.rs
View file

@ -767,8 +767,6 @@ fn solve(
let offset = let_con.defs_and_ret_constraint.index();
let ret_constraint = &constraints.constraints[offset + 1];
let next_rank = rank.next();
let mark = state.mark;
let saved_env = state.env;
@ -776,10 +774,16 @@ fn solve(
let visit_mark = young_mark.next();
let final_mark = visit_mark.next();
let intro_rank = if let_con.generalizable.0 {
rank.next()
} else {
rank
};
// Add a variable for each def to local_def_vars.
let local_def_vars = LocalDefVarsVec::from_def_types(
constraints,
next_rank,
intro_rank,
pools,
problems,
abilities_store,
@ -790,17 +794,26 @@ fn solve(
let_con.def_types,
);
pools.get_mut(next_rank).extend(pool_variables);
// If the let-binding can be generalized, introduce all variables at the next rank;
// those that persist at the next rank after rank-adjustment will be generalized.
//
// Otherwise, introduce all variables at the current rank; since none of them will
// end up at the next rank, none will be generalized.
if let_con.generalizable.0 {
pools.get_mut(rank.next()).extend(pool_variables);
} else {
pools.get_mut(rank).extend(pool_variables);
}
debug_assert_eq!(
// Check that no variable ended up in a higher rank than the next rank.. that
// would mean we generalized one level more than we need to!
{
let offenders = pools
.get(next_rank)
.get(rank.next())
.iter()
.filter(|var| {
subs.get_rank(**var).into_usize() > next_rank.into_usize()
subs.get_rank(**var).into_usize() > rank.next().into_usize()
})
.collect::<Vec<_>>();
@ -817,9 +830,12 @@ fn solve(
0
);
// pop pool
generalize(subs, young_mark, visit_mark, next_rank, pools);
debug_assert!(pools.get(next_rank).is_empty());
// If the let-binding is eligible for generalization, it was solved at the
// next-higher level. Those that are still at that level (intuitively, they did not
// "escape" into the lower level before or after the let-binding) now get to be
// generalized.
generalize(subs, young_mark, visit_mark, rank.next(), pools);
debug_assert!(pools.get(rank.next()).is_empty());
// check that things went well
dbg_do!(ROC_VERIFY_RIGID_LET_GENERALIZED, {
@ -1245,39 +1261,45 @@ fn solve(
state
} else {
// work in the next pool to localize header
let next_rank = rank.next();
// introduce variables
for &var in rigid_vars.iter().chain(flex_vars.iter()) {
subs.set_rank(var, next_rank);
}
// If the let-binding is generalizable, work at the next rank (which will be
// the rank promoted to generalization); otherwise, stay at the current level.
let binding_rank = if let_con.generalizable.0 {
rank.next()
} else {
rank
};
// determine the next pool
if next_rank.into_usize() < pools.len() {
if binding_rank.into_usize() < pools.len() {
// Nothing to do, we already accounted for the next rank, no need to
// adjust the pools
} else {
// we should be off by one at this point
debug_assert_eq!(next_rank.into_usize(), 1 + pools.len());
pools.extend_to(next_rank.into_usize());
debug_assert_eq!(binding_rank.into_usize(), 1 + pools.len());
pools.extend_to(binding_rank.into_usize());
}
let pool: &mut Vec<Variable> = pools.get_mut(next_rank);
let pool: &mut Vec<Variable> = pools.get_mut(binding_rank);
// Replace the contents of this pool with rigid_vars and flex_vars
pool.clear();
// Introduce the variables of this binding, and extend the pool at our binding
// rank.
for &var in rigid_vars.iter().chain(flex_vars.iter()) {
subs.set_rank(var, binding_rank);
}
pool.reserve(rigid_vars.len() + flex_vars.len());
pool.extend(rigid_vars.iter());
pool.extend(flex_vars.iter());
// run solver in next pool
// items are popped from the stack in reverse order. That means that we'll
// Now, run our binding constraint, generalize, then solve the rest of the
// program.
//
// Items are popped from the stack in reverse order. That means that we'll
// first solve then defs_constraint, and then (eventually) the ret_constraint.
//
// Note that the LetConSimple gets the current env and rank,
// and not the env/rank from after solving the defs_constraint
// NB: LetCon gets the current env and rank, not the env/rank from after solving the defs_constraint.
// That's because the defs constraints may be solved in next_rank if we are
// eligible for generalization. The LetCon will then promote variables still at
// next_rank to generalized variables.
stack.push(Work::LetConIntroducesVariables {
env,
rank,
@ -1286,7 +1308,7 @@ fn solve(
});
stack.push(Work::Constraint {
env,
rank: next_rank,
rank: binding_rank,
constraint: defs_constraint,
});
@ -3479,6 +3501,12 @@ fn circular_error(
problems.push(problem);
}
/// Promotes variables at the `young_rank`, which did not escape a let-binding
/// into a lower scope, to generalization.
///
/// Ensures that variables introduced at the `young_rank`, but that should be
/// stuck at a lower level, are marked at that level and not generalized at the
/// present `young_rank`. See [adjust_rank].
fn generalize(
subs: &mut Subs,
young_mark: Mark,
@ -3521,7 +3549,8 @@ fn generalize(
}
}
// re-use the last_vector (which likely has a good capacity for future runs
// re-use the last_vector (which likely has a good capacity for future runs)
debug_assert!(last_pool.is_empty());
*pools.get_mut(young_rank) = last_pool;
}
@ -3562,6 +3591,23 @@ fn pool_to_rank_table(
/// Adjust variable ranks such that ranks never increase as you move deeper.
/// This way the outermost rank is representative of the entire structure.
///
/// This procedure also catches type variables at a given rank that contain types at a higher rank.
/// In such cases, the contained types must be lowered to the rank of the outer type. This is
/// critical for soundness of the type inference; for example consider
///
/// ```ignore(illustrative)
/// \f -> # rank=1
/// g = \x -> f x # rank=2
/// g
/// ```
///
/// say that during the solving of the outer body at rank 1 we conditionally give `f` the type
/// `a -> b (rank=1)`. Without rank-adjustment, the type of `g` would be solved as `c -> d (rank=2)` for
/// some `c ~ a`, `d ~ b`, and hence would be generalized to the function `c -> d`, even though `c`
/// and `d` are individually at rank 1 after unfication with `a` and `b` respectively.
/// This is incorrect; the whole of `c -> d` must lie at rank 1, and only be generalized at the
/// level that `f` is introduced.
fn adjust_rank(
subs: &mut Subs,
young_mark: Mark,
@ -3575,15 +3621,14 @@ fn adjust_rank(
let desc_mark = subs.get_mark_unchecked(var);
if desc_mark == young_mark {
let content = {
let ptr = subs.get_content_unchecked(var) as *const _;
unsafe { &*ptr }
};
let content = *subs.get_content_unchecked(var);
// Mark the variable as visited before adjusting content, as it may be cyclic.
subs.set_mark_unchecked(var, visit_mark);
let max_rank = adjust_rank_content(subs, young_mark, visit_mark, group_rank, content);
// Adjust the nested types' ranks, making sure that no nested unbound type variable is at a
// higher rank than the group rank this `var` is at
let max_rank = adjust_rank_content(subs, young_mark, visit_mark, group_rank, &content);
subs.set_rank_unchecked(var, max_rank);
subs.set_mark_unchecked(var, visit_mark);

23
crates/compiler/solve/tests/solve_expr.rs
View file

@ -8674,4 +8674,27 @@ mod solve_expr {
@"main : (a -[[]]-> b) -[[main(0)]]-> (a -[[y(2) (a -[[]]-> b)]]-> b)"
);
}
#[test]
fn when_branch_variables_not_generalized() {
infer_queries!(
indoc!(
r#"
app "test" provides [main] to "./platform"
main = \{} -> when Red is
#^^^^{-1}
x ->
y : [Red]_
y = x
z : [Red, Green]_
z = x
{y, z}
"#
),
@"main : {}* -[[main(0)]]-> { y : [Green, Red]a, z : [Green, Red]a }"
);
}
}