Merge pull request #3404 from rtfeldman/ambient-lset-specialization

The ambient lambda set specialization algorithm
This commit is contained in:
Ayaz 2022-07-09 17:23:27 -05:00 committed by GitHub
commit 7b308d9efe
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
22 changed files with 1816 additions and 280 deletions

View file

@ -968,6 +968,7 @@ fn unify_lambda_set<M: MetaCollector>(
solved: UnionLabels::default(),
recursion_var: OptVariable::NONE,
unspecialized: SubsSlice::default(),
ambient_function: subs.fresh_unnamed_flex_var(),
};
extract_specialization_lambda_set(subs, ctx, lambda_set, zero_lambda_set)
@ -1013,6 +1014,7 @@ fn extract_specialization_lambda_set<M: MetaCollector>(
solved: member_solved,
recursion_var: member_rec_var,
unspecialized: member_uls_slice,
ambient_function: _,
} = ability_member_proto_lset;
debug_assert!(
@ -1207,6 +1209,64 @@ fn separate_union_lambdas(
}
}
fn unify_unspecialized_lambdas<M: MetaCollector>(
subs: &mut Subs,
pool: &mut Pool,
uls1: SubsSlice<Uls>,
uls2: SubsSlice<Uls>,
) -> Result<SubsSlice<Uls>, Outcome<M>> {
// For now we merge all variables of unspecialized lambdas in a lambda set that share the same
// ability member/region.
// See the section "A property that's lost, and how we can hold on to it" of
// solve/docs/ambient_lambda_set_specialization.md to see how we can loosen this restriction.
// Note that we don't need to update the bookkeeping of variable -> lambda set to be resolved,
// because if we had v1 -> lset1, and now lset1 ~ lset2, then afterward either lset1 still
// resolves to itself or re-points to lset2.
// In either case the merged unspecialized lambda sets will be there.
match (uls1.is_empty(), uls2.is_empty()) {
(true, true) => Ok(SubsSlice::default()),
(false, true) => Ok(uls1),
(true, false) => Ok(uls2),
(false, false) => {
let mut all_uls = (subs.get_subs_slice(uls1).iter())
.chain(subs.get_subs_slice(uls2))
.map(|&Uls(var, sym, region)| {
// Take the root key to deduplicate
Uls(subs.get_root_key_without_compacting(var), sym, region)
})
.collect::<Vec<_>>();
// Arrange into partitions of (_, member, region).
all_uls.sort_by_key(|&Uls(_, sym, region)| (sym, region));
// Now merge the variables of unspecialized lambdas pointing to the same
// member/region.
let mut j = 1;
while j < all_uls.len() {
let i = j - 1;
let Uls(var_i, sym_i, region_i) = all_uls[i];
let Uls(var_j, sym_j, region_j) = all_uls[j];
if sym_i == sym_j && region_i == region_j {
let outcome = unify_pool(subs, pool, var_i, var_j, Mode::EQ);
if !outcome.mismatches.is_empty() {
return Err(outcome);
}
// Keep the Uls in position `i` and remove the one in position `j`.
all_uls.remove(j);
} else {
// Keep both Uls, look at the next one.
j += 1;
}
}
Ok(SubsSlice::extend_new(
&mut subs.unspecialized_lambda_sets,
all_uls,
))
}
}
}
fn unify_lambda_set_help<M: MetaCollector>(
subs: &mut Subs,
pool: &mut Pool,
@ -1221,13 +1281,20 @@ fn unify_lambda_set_help<M: MetaCollector>(
solved: solved1,
recursion_var: rec1,
unspecialized: uls1,
ambient_function: ambient_function_var1,
} = lset1;
let LambdaSet {
solved: solved2,
recursion_var: rec2,
unspecialized: uls2,
ambient_function: ambient_function_var2,
} = lset2;
// Assumed precondition: the ambient functions have already been unified, or are in the process
// of being unified - otherwise, how could we have reached unification of lambda sets?
let _ = ambient_function_var2;
let ambient_function_var = ambient_function_var1;
debug_assert!(
(rec1.into_variable().into_iter())
.chain(rec2.into_variable().into_iter())
@ -1266,26 +1333,11 @@ fn unify_lambda_set_help<M: MetaCollector>(
(None, None) => OptVariable::NONE,
};
// Combine the unspecialized lambda sets as needed. Note that we don't need to update the
// bookkeeping of variable -> lambda set to be resolved, because if we had v1 -> lset1, and
// now lset1 ~ lset2, then afterward either lset1 still resolves to itself or re-points to
// lset2. In either case the merged unspecialized lambda sets will be there.
let merged_unspecialized = match (uls1.is_empty(), uls2.is_empty()) {
(true, true) => SubsSlice::default(),
(false, true) => uls1,
(true, false) => uls2,
(false, false) => {
let mut all_uls = (subs.get_subs_slice(uls1).iter())
.chain(subs.get_subs_slice(uls2))
.map(|&Uls(var, sym, region)| {
// Take the root key to deduplicate
Uls(subs.get_root_key_without_compacting(var), sym, region)
})
.collect::<Vec<_>>();
all_uls.sort();
all_uls.dedup();
SubsSlice::extend_new(&mut subs.unspecialized_lambda_sets, all_uls)
let merged_unspecialized = match unify_unspecialized_lambdas(subs, pool, uls1, uls2) {
Ok(merged) => merged,
Err(outcome) => {
debug_assert!(!outcome.mismatches.is_empty());
return outcome;
}
};
@ -1294,6 +1346,7 @@ fn unify_lambda_set_help<M: MetaCollector>(
solved: new_solved,
recursion_var,
unspecialized: merged_unspecialized,
ambient_function: ambient_function_var,
});
merge(subs, ctx, new_lambda_set)
@ -1927,8 +1980,9 @@ fn maybe_mark_union_recursive(subs: &mut Subs, union_var: Variable) {
solved,
recursion_var: OptVariable::NONE,
unspecialized,
ambient_function: ambient_function_var,
}) => {
subs.mark_lambda_set_recursive(v, solved, unspecialized);
subs.mark_lambda_set_recursive(v, solved, unspecialized, ambient_function_var);
continue 'outer;
}
_ => { /* fall through */ }
@ -2681,10 +2735,12 @@ fn unify_function_or_tag_union_and_func<M: MetaCollector>(
{
let union_tags = UnionLambdas::tag_without_arguments(subs, tag_symbol);
let ambient_function_var = if left { ctx.first } else { ctx.second };
let lambda_set_content = LambdaSet(self::LambdaSet {
solved: union_tags,
recursion_var: OptVariable::NONE,
unspecialized: SubsSlice::default(),
ambient_function: ambient_function_var,
});
let tag_lambda_set = register(