Skip to content

Commit

Permalink
Take more specific args
Browse files Browse the repository at this point in the history
  • Loading branch information
azdavis committed May 4, 2024
1 parent 9dc33af commit afb8556
Show file tree
Hide file tree
Showing 5 changed files with 46 additions and 25 deletions.
45 changes: 30 additions & 15 deletions crates/sml-statics/src/compatible.rs
Original file line number Diff line number Diff line change
Expand Up @@ -8,50 +8,65 @@ type Result = std::result::Result<(), ErrorKind>;

/// returns `Ok(())` iff the ty fns are equal. (this is distinct from equal ty schemes because the
/// order of bound variables is significant.)
pub(crate) fn eq_ty_fn_no_emit(st: &mut St<'_>, mut lhs: TyScheme, mut rhs: TyScheme) -> Result {
pub(crate) fn eq_ty_fn_no_emit(
st: &mut sml_statics_types::St,
mode: sml_statics_types::mode::Mode,
mut lhs: TyScheme,
mut rhs: TyScheme,
) -> Result {
if lhs.bound_vars.len() != rhs.bound_vars.len() {
return Err(ErrorKind::WrongNumTyArgs(lhs.bound_vars.len(), rhs.bound_vars.len()));
}
let subst = fixed_var_subst(st, &lhs.bound_vars);
apply_bv(&mut st.syms_tys.tys, &subst, &mut lhs.ty);
apply_bv(&mut st.syms_tys.tys, &subst, &mut rhs.ty);
unify_no_emit(st, lhs.ty, rhs.ty)
apply_bv(&mut st.tys, &subst, &mut lhs.ty);
apply_bv(&mut st.tys, &subst, &mut rhs.ty);
unify_no_emit(st, mode, lhs.ty, rhs.ty)
}

/// emits no error iff the ty fns are equal.
pub(crate) fn eq_ty_fn(st: &mut St<'_>, idx: sml_hir::Idx, lhs: TyScheme, rhs: TyScheme) {
match eq_ty_fn_no_emit(st, lhs, rhs) {
match eq_ty_fn_no_emit(st.syms_tys, st.info.mode, lhs, rhs) {
Ok(()) => {}
Err(e) => st.err(idx, e),
}
}

/// returns `Ok(())` iff the ty schemes are equal.
pub(crate) fn eq_ty_scheme(st: &mut St<'_>, lhs: &TyScheme, rhs: &TyScheme) -> Result {
generalizes_no_emit(st, lhs, rhs)?;
generalizes_no_emit(st, rhs, lhs)?;
pub(crate) fn eq_ty_scheme(
st: &mut sml_statics_types::St,
mode: sml_statics_types::mode::Mode,
lhs: &TyScheme,
rhs: &TyScheme,
) -> Result {
generalizes_no_emit(st, mode, lhs, rhs)?;
generalizes_no_emit(st, mode, rhs, lhs)?;
Ok(())
}

fn fixed_var_subst(st: &mut St<'_>, bound_vars: &BoundTyVars) -> Vec<Ty> {
fn fixed_var_subst(st: &mut sml_statics_types::St, bound_vars: &BoundTyVars) -> Vec<Ty> {
bound_vars
.iter()
.enumerate()
.map(|(idx, data)| {
let equality = matches!(data.ty_var_kind(), TyVarKind::Equality);
let ty_var = sml_hir::UnutterableTyVar::new(equality, idx);
st.syms_tys.tys.fixed_var(sml_hir::TyVar::unutterable(ty_var), TyVarSrc::Ty)
st.tys.fixed_var(sml_hir::TyVar::unutterable(ty_var), TyVarSrc::Ty)
})
.collect()
}

/// returns `Ok(())` iff `general` generalizes `specific`.
fn generalizes_no_emit(st: &mut St<'_>, general: &TyScheme, specific: &TyScheme) -> Result {
let general = instantiate(&mut st.syms_tys.tys, Generalizable::Always, general);
fn generalizes_no_emit(
st: &mut sml_statics_types::St,
mode: sml_statics_types::mode::Mode,
general: &TyScheme,
specific: &TyScheme,
) -> Result {
let general = instantiate(&mut st.tys, Generalizable::Always, general);
let subst = fixed_var_subst(st, &specific.bound_vars);
let mut specific = specific.ty;
apply_bv(&mut st.syms_tys.tys, &subst, &mut specific);
unify_no_emit(st, specific, general)
apply_bv(&mut st.tys, &subst, &mut specific);
unify_no_emit(st, mode, specific, general)
}

/// emits no error iff `general` generalizes `specific`.
Expand All @@ -61,7 +76,7 @@ pub(crate) fn generalizes(
general: &TyScheme,
specific: &TyScheme,
) {
match generalizes_no_emit(st, general, specific) {
match generalizes_no_emit(st.syms_tys, st.info.mode, general, specific) {
Ok(()) => {}
Err(e) => st.err(idx, e),
}
Expand Down
2 changes: 1 addition & 1 deletion crates/sml-statics/src/pat.rs
Original file line number Diff line number Diff line change
Expand Up @@ -228,7 +228,7 @@ fn get_(
assert!(rest_val_info.id_status.same_kind_as(IdStatus::Val));
fst_val_info.defs.extend(rest_val_info.defs);
let rest_ty_scheme = rest_val_info.ty_scheme.clone();
match eq_ty_scheme(st, &fst_val_info.ty_scheme, &rest_ty_scheme) {
match eq_ty_scheme(st.syms_tys, st.info.mode, &fst_val_info.ty_scheme, &rest_ty_scheme) {
Ok(()) => {}
Err(e) => st.err(idx, e),
}
Expand Down
2 changes: 1 addition & 1 deletion crates/sml-statics/src/st.rs
Original file line number Diff line number Diff line change
Expand Up @@ -177,7 +177,7 @@ impl<'a> St<'a> {
self.err(idx, ErrorKind::CanEtaReduce(name));
}
for (idx, name, old, new) in std::mem::take(&mut self.shadows) {
if compatible::eq_ty_scheme(self, &old, &new).is_ok() {
if compatible::eq_ty_scheme(self.syms_tys, self.info.mode, &old, &new).is_ok() {
self.err(idx, ErrorKind::ShadowInCaseWithSameTy(name, old));
}
}
Expand Down
9 changes: 5 additions & 4 deletions crates/sml-statics/src/top_dec/instance.rs
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ pub(crate) fn env_of_sig(
let mut path = Vec::<&str_util::Name>::new();
let bound_vars = st.syms_tys.syms.get(sym).unwrap().ty_info.ty_scheme.bound_vars.clone();
let ty_scheme = n_ary_con(&mut st.syms_tys.tys, bound_vars, sym);
if !bound_ty_name_to_path(st, &mut path, &sig.env, &ty_scheme) {
if !bound_ty_name_to_path(st.syms_tys, st.info.mode, &mut path, &sig.env, &ty_scheme) {
// there should have already been an error emitted for this
cov_mark::hit("no_path_to_sym");
return;
Expand Down Expand Up @@ -57,20 +57,21 @@ pub(crate) fn env_of_sig(
/// this seems slightly questionable, but I'm not actually sure if it's an issue. I mean, it says
/// right there that they should be equal anyway.
fn bound_ty_name_to_path<'e>(
st: &mut St<'_>,
st: &mut sml_statics_types::St,
mode: sml_statics_types::mode::Mode,
ac: &mut Vec<&'e str_util::Name>,
env: &'e Env,
ty_scheme: &TyScheme,
) -> bool {
for (name, ty_info) in env.ty_env.iter() {
if eq_ty_fn_no_emit(st, ty_info.ty_scheme.clone(), ty_scheme.clone()).is_ok() {
if eq_ty_fn_no_emit(st, mode, ty_info.ty_scheme.clone(), ty_scheme.clone()).is_ok() {
ac.push(name);
return true;
}
}
for (name, env) in env.str_env.iter() {
ac.push(name);
if bound_ty_name_to_path(st, ac, env, ty_scheme) {
if bound_ty_name_to_path(st, mode, ac, env, ty_scheme) {
return true;
}
ac.pop();
Expand Down
13 changes: 9 additions & 4 deletions crates/sml-statics/src/unify.rs
Original file line number Diff line number Diff line change
Expand Up @@ -6,17 +6,22 @@ use sml_statics_types::ty::Ty;
use sml_statics_types::unify;

pub(crate) fn unify(st: &mut St<'_>, idx: sml_hir::Idx, want: Ty, got: Ty) {
match unify_no_emit(st, want, got) {
match unify_no_emit(st.syms_tys, st.info.mode, want, got) {
Ok(()) => {}
Err(e) => st.err(idx, e),
}
}

pub(crate) fn unify_no_emit(st: &mut St<'_>, want: Ty, got: Ty) -> Result<(), ErrorKind> {
if st.info.mode.is_path_order() {
pub(crate) fn unify_no_emit(
st: &mut sml_statics_types::St,
mode: sml_statics_types::mode::Mode,
want: Ty,
got: Ty,
) -> Result<(), ErrorKind> {
if mode.is_path_order() {
return Ok(());
}
unify::unify(&mut st.syms_tys.tys, &st.syms_tys.syms, want, got).map_err(|err| match err {
unify::unify(&mut st.tys, &st.syms, want, got).map_err(|err| match err {
unify::Error::Circularity(circ) => ErrorKind::Circularity(circ),
unify::Error::Incompatible(reason) => ErrorKind::IncompatibleTys(reason, want, got),
})
Expand Down

0 comments on commit afb8556

Please sign in to comment.