Move unify::Mode to roc_solve_schema

This commit is contained in:
Ayaz Hafiz 2023-07-16 09:58:04 -05:00
parent 87d108eccc
commit 18e9f8f034
No known key found for this signature in database
GPG key ID: 0E2A37416A25EF58
19 changed files with 140 additions and 98 deletions

View file

@ -9,6 +9,7 @@ version.workspace = true
[dependencies]
roc_module = { path = "../module" }
roc_solve_schema = { path = "../solve_schema" }
roc_types = { path = "../types" }
serde.workspace = true

View file

@ -15,6 +15,7 @@ roc_derive_key = { path = "../derive_key" }
roc_error_macros = { path = "../../error_macros" }
roc_module = { path = "../module" }
roc_region = { path = "../region" }
roc_solve_schema = { path = "../solve_schema" }
roc_types = { path = "../types" }
roc_unify = { path = "../unify" }

View file

@ -2,6 +2,7 @@ use roc_can::{abilities::SpecializationLambdaSets, module::ExposedByModule};
use roc_checkmate::with_checkmate;
use roc_error_macros::internal_error;
use roc_module::symbol::{IdentIds, Symbol};
use roc_solve_schema::UnificationMode;
use roc_types::{
subs::{instantiate_rigids, Subs, Variable},
types::Polarity,
@ -73,7 +74,7 @@ impl Env<'_> {
pub fn unify(&mut self, left: Variable, right: Variable) {
use roc_unify::{
unify::{unify, Mode, Unified},
unify::{unify, Unified},
Env,
};
@ -85,7 +86,7 @@ impl Env<'_> {
}),
left,
right,
Mode::EQ,
UnificationMode::EQ,
Polarity::OF_PATTERN,
);
@ -112,7 +113,7 @@ impl Env<'_> {
ability_member: Symbol,
) -> SpecializationLambdaSets {
use roc_unify::{
unify::{unify_introduced_ability_specialization, Mode, Unified},
unify::{unify_introduced_ability_specialization, Unified},
Env,
};
@ -126,7 +127,7 @@ impl Env<'_> {
}),
member_signature,
specialization_type,
Mode::EQ,
UnificationMode::EQ,
);
match unified {

View file

@ -15,6 +15,7 @@ roc_derive = { path = "../derive" }
roc_error_macros = { path = "../../error_macros" }
roc_module = { path = "../module" }
roc_solve = { path = "../solve" }
roc_solve_schema = { path = "../solve_schema" }
roc_types = { path = "../types" }
roc_unify = { path = "../unify" }

View file

@ -16,11 +16,12 @@ use roc_solve::ability::AbilityResolver;
use roc_solve::specialize::{compact_lambda_sets_of_vars, Phase};
use roc_solve::Pools;
use roc_solve::{DerivedEnv, SolveEnv};
use roc_solve_schema::UnificationMode;
use roc_types::subs::{get_member_lambda_sets_at_region, Content, FlatType, LambdaSet};
use roc_types::subs::{ExposedTypesStorageSubs, Subs, Variable};
use roc_types::types::Polarity;
use roc_unify::unify::MetaCollector;
use roc_unify::unify::{Mode, Unified};
use roc_unify::unify::Unified;
use roc_unify::Env as UEnv;
pub use roc_solve::ability::{ResolveError, Resolved};
@ -369,7 +370,7 @@ pub fn unify(
}),
left,
right,
Mode::EQ,
UnificationMode::EQ,
Polarity::Pos,
);

View file

@ -21,6 +21,7 @@ roc_packaging = { path = "../../packaging" }
roc_problem = { path = "../problem" }
roc_region = { path = "../region" }
roc_solve_problem = { path = "../solve_problem" }
roc_solve_schema = { path = "../solve_schema" }
roc_types = { path = "../types" }
roc_unify = { path = "../unify" }

View file

@ -13,6 +13,7 @@ use roc_solve_problem::{
NotDerivableContext, NotDerivableDecode, NotDerivableEncode, NotDerivableEq, TypeError,
UnderivableReason, Unfulfilled,
};
use roc_solve_schema::UnificationMode;
use roc_types::num::NumericRange;
use roc_types::subs::{
instantiate_rigids, Content, FlatType, GetSubsSlice, Rank, RecordFields, Subs, SubsSlice,
@ -1287,7 +1288,7 @@ impl DerivableVisitor for DeriveEq {
subs: &mut Subs,
content_var: Variable,
) -> Result<Descend, NotDerivable> {
use roc_unify::unify::{unify, Mode};
use roc_unify::unify::unify;
// Of the floating-point types,
// only Dec implements Eq.
@ -1299,7 +1300,7 @@ impl DerivableVisitor for DeriveEq {
}),
content_var,
Variable::DECIMAL,
Mode::EQ,
UnificationMode::EQ,
Polarity::Pos,
);
match unified {
@ -1417,7 +1418,7 @@ pub fn resolve_ability_specialization<R: AbilityResolver>(
ability_member: Symbol,
specialization_var: Variable,
) -> Result<Resolved, ResolveError> {
use roc_unify::unify::{unify, Mode};
use roc_unify::unify::unify;
let (parent_ability, signature_var) = resolver
.member_parent_and_signature_var(ability_member, subs)
@ -1435,7 +1436,7 @@ pub fn resolve_ability_specialization<R: AbilityResolver>(
}),
specialization_var,
signature_var,
Mode::EQ,
UnificationMode::EQ,
Polarity::Pos,
)
.expect_success(

View file

@ -24,13 +24,14 @@ use roc_module::symbol::Symbol;
use roc_problem::can::CycleEntry;
use roc_region::all::Loc;
use roc_solve_problem::TypeError;
use roc_solve_schema::UnificationMode;
use roc_types::subs::{
self, Content, FlatType, GetSubsSlice, Mark, OptVariable, Rank, Subs, TagExt, UlsOfVar,
Variable,
};
use roc_types::types::{Category, Polarity, Reason, RecordField, Type, TypeExtension, Types, Uls};
use roc_unify::unify::{
unify, unify_introduced_ability_specialization, Mode, Obligated, SpecializationLsetCollector,
unify, unify_introduced_ability_specialization, Obligated, SpecializationLsetCollector,
Unified::*,
};
@ -489,7 +490,7 @@ fn solve(
&mut env.uenv(),
actual,
expected,
Mode::EQ,
UnificationMode::EQ,
Polarity::OF_VALUE,
) {
Success {
@ -600,7 +601,7 @@ fn solve(
&mut env.uenv(),
actual,
expected,
Mode::EQ,
UnificationMode::EQ,
Polarity::OF_VALUE,
) {
Success {
@ -699,8 +700,8 @@ fn solve(
);
let mode = match constraint {
PatternPresence(..) => Mode::PRESENT,
_ => Mode::EQ,
PatternPresence(..) => UnificationMode::PRESENT,
_ => UnificationMode::EQ,
};
match unify(
@ -919,7 +920,7 @@ fn solve(
&mut env.uenv(),
actual,
includes,
Mode::PRESENT,
UnificationMode::PRESENT,
Polarity::OF_PATTERN,
) {
Success {
@ -1053,7 +1054,7 @@ fn solve(
&mut env.uenv(),
branches_var,
real_var,
Mode::EQ,
UnificationMode::EQ,
cond_polarity,
);
@ -1103,7 +1104,7 @@ fn solve(
&mut env.uenv(),
real_var,
branches_var,
Mode::EQ,
UnificationMode::EQ,
cond_polarity,
),
Success { .. }
@ -1121,7 +1122,7 @@ fn solve(
&mut env.uenv(),
real_var,
branches_var,
Mode::EQ,
UnificationMode::EQ,
cond_polarity,
) {
Failure(vars, actual_type, expected_type, _bad_impls) => {
@ -1320,7 +1321,7 @@ fn solve(
&mut env.uenv(),
actual,
Variable::LIST_U8,
Mode::EQ,
UnificationMode::EQ,
Polarity::OF_VALUE,
) {
// List U8 always valid.
@ -1340,7 +1341,7 @@ fn solve(
&mut env.uenv(),
actual,
Variable::STR,
Mode::EQ,
UnificationMode::EQ,
Polarity::OF_VALUE,
) {
Success {
@ -1591,7 +1592,7 @@ fn check_ability_specialization(
&mut env.uenv(),
root_signature_var,
symbol_loc_var.value,
Mode::EQ,
UnificationMode::EQ,
);
let resolved_mark = match unified {

View file

@ -10,6 +10,7 @@ use roc_debug_flags::ROC_TRACE_COMPACTION;
use roc_derive_key::{DeriveError, DeriveKey};
use roc_error_macros::{internal_error, todo_abilities};
use roc_module::symbol::{ModuleId, Symbol};
use roc_solve_schema::UnificationMode;
use roc_types::{
subs::{
get_member_lambda_sets_at_region, Content, Descriptor, GetSubsSlice, LambdaSet, Mark,
@ -17,7 +18,7 @@ use roc_types::{
},
types::{AliasKind, MemberImpl, Polarity, Uls},
};
use roc_unify::unify::{unify, Mode, MustImplementConstraints};
use roc_unify::unify::{unify, MustImplementConstraints};
use crate::{
ability::builtin_module_with_unlisted_ability_impl,
@ -577,7 +578,7 @@ fn compact_lambda_set<P: Phase>(
&mut env.uenv(),
t_f1,
t_f2,
Mode::LAMBDA_SET_SPECIALIZATION,
UnificationMode::LAMBDA_SET_SPECIALIZATION,
Polarity::Pos,
)
.expect_success("ambient functions don't unify");

View file

@ -6,6 +6,7 @@ use roc_error_macros::internal_error;
use roc_module::{ident::TagName, symbol::Symbol};
use roc_region::all::Loc;
use roc_solve_problem::TypeError;
use roc_solve_schema::UnificationMode;
use roc_types::{
subs::{
self, AliasVariables, Content, FlatType, GetSubsSlice, LambdaSet, OptVariable, Rank,
@ -17,7 +18,7 @@ use roc_types::{
Category, ExtImplicitOpenness, Polarity, TypeTag, Types,
},
};
use roc_unify::unify::{unify, Mode, Unified};
use roc_unify::unify::{unify, Unified};
use crate::{
ability::{AbilityImplError, ObligationCache},
@ -875,7 +876,7 @@ pub(crate) fn type_to_var_help(
&mut env.uenv(),
var,
flex_ability,
Mode::EQ,
UnificationMode::EQ,
Polarity::OF_VALUE,
) {
Unified::Success {

View file

@ -0,0 +1,11 @@
[package]
name = "roc_solve_schema"
description = "Types used in the solver."
authors.workspace = true
edition.workspace = true
license.workspace = true
version.workspace = true
[dependencies]
bitflags.workspace = true

View file

@ -0,0 +1,3 @@
mod unify;
pub use unify::UnificationMode;

View file

@ -0,0 +1,50 @@
use bitflags::bitflags;
bitflags! {
pub struct UnificationMode : u8 {
/// Instructs the unifier to solve two types for equality.
///
/// For example, { n : Str }a ~ { n: Str, m : Str } will solve "a" to "{ m : Str }".
const EQ = 1 << 0;
/// Instructs the unifier to treat the right-hand-side of a constraint as
/// present in the left-hand-side, rather than strictly equal.
///
/// For example, t1 += [A Str] says we should "add" the tag "A Str" to the type of "t1".
const PRESENT = 1 << 1;
/// Like [`UnificationMode::EQ`], but also instructs the unifier that the ambient lambda set
/// specialization algorithm is running. This has implications for the unification of
/// unspecialized lambda sets; see [`unify_unspecialized_lambdas`].
const LAMBDA_SET_SPECIALIZATION = UnificationMode::EQ.bits | (1 << 2);
}
}
impl UnificationMode {
pub fn is_eq(&self) -> bool {
debug_assert!(!self.contains(UnificationMode::EQ | UnificationMode::PRESENT));
self.contains(UnificationMode::EQ)
}
pub fn is_present(&self) -> bool {
debug_assert!(!self.contains(UnificationMode::EQ | UnificationMode::PRESENT));
self.contains(UnificationMode::PRESENT)
}
pub fn is_lambda_set_specialization(&self) -> bool {
debug_assert!(!self.contains(UnificationMode::EQ | UnificationMode::PRESENT));
self.contains(UnificationMode::LAMBDA_SET_SPECIALIZATION)
}
pub fn as_eq(self) -> Self {
(self - UnificationMode::PRESENT) | UnificationMode::EQ
}
pub fn pretty_print(&self) -> &str {
if self.contains(UnificationMode::EQ) {
"~"
} else if self.contains(UnificationMode::PRESENT) {
"+="
} else {
unreachable!("Bad mode!")
}
}
}

View file

@ -8,7 +8,6 @@ license.workspace = true
version.workspace = true
[dependencies]
bitflags.workspace = true
[dependencies.roc_collections]
path = "../collections"
@ -30,3 +29,6 @@ path = "../../tracing"
[dependencies.roc_checkmate]
path = "../checkmate"
[dependencies.roc_solve_schema]
path = "../solve_schema"

View file

@ -2,8 +2,6 @@ use roc_checkmate::debug_checkmate;
use roc_collections::VecSet;
use roc_types::subs::{Descriptor, Subs, Variable};
use crate::unify::Mode;
pub struct Env<'a> {
subs: &'a mut Subs,
#[cfg(debug_assertions)]
@ -104,7 +102,12 @@ impl<'a> Env<'a> {
}
#[cfg(debug_assertions)]
pub(crate) fn debug_start_unification(&mut self, left: Variable, right: Variable, mode: Mode) {
pub(crate) fn debug_start_unification(
&mut self,
left: Variable,
right: Variable,
mode: roc_solve_schema::UnificationMode,
) {
debug_checkmate!(self.cm, cm => {
cm.start_unification(self.subs, left, right);
});

View file

@ -1,4 +1,3 @@
use bitflags::bitflags;
use roc_collections::VecMap;
use roc_debug_flags::{dbg_do, dbg_set};
#[cfg(debug_assertions)]
@ -8,6 +7,7 @@ use roc_debug_flags::{
use roc_error_macros::{internal_error, todo_lambda_erasure};
use roc_module::ident::{Lowercase, TagName};
use roc_module::symbol::{ModuleId, Symbol};
use roc_solve_schema::UnificationMode;
use roc_types::num::{FloatWidth, IntLitWidth, NumericRange};
use roc_types::subs::Content::{self, *};
use roc_types::subs::{
@ -101,63 +101,13 @@ macro_rules! mismatch {
type Pool = Vec<Variable>;
bitflags! {
pub struct Mode : u8 {
/// Instructs the unifier to solve two types for equality.
///
/// For example, { n : Str }a ~ { n: Str, m : Str } will solve "a" to "{ m : Str }".
const EQ = 1 << 0;
/// Instructs the unifier to treat the right-hand-side of a constraint as
/// present in the left-hand-side, rather than strictly equal.
///
/// For example, t1 += [A Str] says we should "add" the tag "A Str" to the type of "t1".
const PRESENT = 1 << 1;
/// Like [`Mode::EQ`], but also instructs the unifier that the ambient lambda set
/// specialization algorithm is running. This has implications for the unification of
/// unspecialized lambda sets; see [`unify_unspecialized_lambdas`].
const LAMBDA_SET_SPECIALIZATION = Mode::EQ.bits | (1 << 2);
}
}
impl Mode {
fn is_eq(&self) -> bool {
debug_assert!(!self.contains(Mode::EQ | Mode::PRESENT));
self.contains(Mode::EQ)
}
fn is_present(&self) -> bool {
debug_assert!(!self.contains(Mode::EQ | Mode::PRESENT));
self.contains(Mode::PRESENT)
}
fn is_lambda_set_specialization(&self) -> bool {
debug_assert!(!self.contains(Mode::EQ | Mode::PRESENT));
self.contains(Mode::LAMBDA_SET_SPECIALIZATION)
}
fn as_eq(self) -> Self {
(self - Mode::PRESENT) | Mode::EQ
}
#[cfg(debug_assertions)]
fn pretty_print(&self) -> &str {
if self.contains(Mode::EQ) {
"~"
} else if self.contains(Mode::PRESENT) {
"+="
} else {
unreachable!("Bad mode!")
}
}
}
#[derive(Debug)]
pub struct Context {
first: Variable,
first_desc: Descriptor,
second: Variable,
second_desc: Descriptor,
mode: Mode,
mode: UnificationMode,
}
pub trait MetaCollector: Default + std::fmt::Debug {
@ -333,7 +283,7 @@ impl<M: MetaCollector> Outcome<M> {
}
/// Unifies two types.
/// The [mode][Mode] enables or disables certain extensional features of unification.
/// The [mode][UnificationMode] enables or disables certain extensional features of unification.
///
/// `observed_pol` describes the [polarity][Polarity] of the type observed to be under unification.
/// This is only relevant for producing error types, and is not material to the unification
@ -343,7 +293,7 @@ pub fn unify(
env: &mut Env,
var1: Variable,
var2: Variable,
mode: Mode,
mode: UnificationMode,
observed_pol: Polarity,
) -> Unified {
unify_help(env, var1, var2, mode, observed_pol)
@ -355,7 +305,7 @@ pub fn unify_introduced_ability_specialization(
env: &mut Env,
ability_member_signature: Variable,
specialization_var: Variable,
mode: Mode,
mode: UnificationMode,
) -> Unified<SpecializationLsetCollector> {
unify_help(
env,
@ -372,7 +322,7 @@ pub fn unify_with_collector<M: MetaCollector>(
env: &mut Env,
var1: Variable,
var2: Variable,
mode: Mode,
mode: UnificationMode,
observed_pol: Polarity,
) -> Unified<M> {
unify_help(env, var1, var2, mode, observed_pol)
@ -384,7 +334,7 @@ fn unify_help<M: MetaCollector>(
env: &mut Env,
var1: Variable,
var2: Variable,
mode: Mode,
mode: UnificationMode,
observed_pol: Polarity,
) -> Unified<M> {
let mut vars = Vec::new();
@ -438,7 +388,7 @@ pub fn unify_pool<M: MetaCollector>(
pool: &mut Pool,
var1: Variable,
var2: Variable,
mode: Mode,
mode: UnificationMode,
) -> Outcome<M> {
if env.equivalent(var1, var2) {
Outcome::default()
@ -1332,7 +1282,7 @@ struct SeparatedUnionLambdas {
fn separate_union_lambdas<M: MetaCollector>(
env: &mut Env,
pool: &mut Pool,
mode: Mode,
mode: UnificationMode,
fields1: UnionLambdas,
fields2: UnionLambdas,
) -> Result<(Outcome<M>, SeparatedUnionLambdas), Outcome<M>> {
@ -1585,7 +1535,7 @@ fn is_sorted_unspecialized_lamba_set_list(subs: &Subs, uls: &[Uls]) -> bool {
fn unify_unspecialized_lambdas<M: MetaCollector>(
env: &mut Env,
pool: &mut Pool,
mode: Mode,
mode: UnificationMode,
uls_left: SubsSlice<Uls>,
uls_right: SubsSlice<Uls>,
) -> Result<(SubsSlice<Uls>, Outcome<M>), Outcome<M>> {
@ -2651,7 +2601,7 @@ fn unify_tag_ext<M: MetaCollector>(
env: &mut Env,
pool: &mut Pool,
vars: UnifySides<TagExt, Variable>,
mode: Mode,
mode: UnificationMode,
) -> Outcome<M> {
let (ext, var, flip_for_unify) = match vars {
UnifySides::Left(ext, var) => (ext, var, false),
@ -3437,7 +3387,7 @@ fn unify_zip_slices<M: MetaCollector>(
pool: &mut Pool,
left: SubsSlice<Variable>,
right: SubsSlice<Variable>,
mode: Mode,
mode: UnificationMode,
) -> Outcome<M> {
let mut outcome = Outcome::default();