mirror of
https://github.com/tweag/nickel.git
synced 2024-10-05 23:57:09 +03:00
tyw -> uty
Get rid of the last references of the old name of UnifType (previously TypeWrapper) in function, macro and variable names.
This commit is contained in:
Yann Hamdaoui
parent
b529181f62
commit
a8bbad464b
@ -427,13 +427,13 @@ mod tests {
|
||||
|
||||
#[test]
|
||||
fn test_extract_ident_with_path() {
|
||||
use nickel_lang::{mk_tyw_record, mk_tyw_row, types::RecordRowsF};
|
||||
use nickel_lang::{mk_uty_record, mk_uty_row, types::RecordRowsF};
|
||||
use std::convert::TryInto;
|
||||
|
||||
// Representing the type: {a: {b : {c1 : Num, c2: Num}}}
|
||||
let c_record_type = mk_tyw_record!(("c1", TypeF::Num), ("c2", TypeF::Num));
|
||||
let b_record_type = mk_tyw_record!(("b", c_record_type));
|
||||
let a_record_type = mk_tyw_row!(("a", b_record_type));
|
||||
let c_record_type = mk_uty_record!(("c1", TypeF::Num), ("c2", TypeF::Num));
|
||||
let b_record_type = mk_uty_record!(("b", c_record_type));
|
||||
let a_record_type = mk_uty_row!(("a", b_record_type));
|
||||
|
||||
let mut path = vec![Ident::from("b"), Ident::from("a")];
|
||||
// unwrap: the conversion must succeed because we built a type without unification variable
|
||||
|
||||
@ -419,31 +419,31 @@ fn type_eq_bounded<E: TermEnvironment>(
|
||||
| (TypeF::Bool, TypeF::Bool)
|
||||
| (TypeF::Sym, TypeF::Sym)
|
||||
| (TypeF::Str, TypeF::Str) => true,
|
||||
(TypeF::Dict(tyw1), TypeF::Dict(tyw2)) | (TypeF::Array(tyw1), TypeF::Array(tyw2)) => {
|
||||
type_eq_bounded(state, tyw1, env1, tyw2, env2)
|
||||
(TypeF::Dict(uty1), TypeF::Dict(uty2)) | (TypeF::Array(uty1), TypeF::Array(uty2)) => {
|
||||
type_eq_bounded(state, uty1, env1, uty2, env2)
|
||||
}
|
||||
(TypeF::Arrow(s1, t1), TypeF::Arrow(s2, t2)) => {
|
||||
type_eq_bounded(state, s1, env1, s2, env2)
|
||||
&& type_eq_bounded(state, t1, env1, t2, env2)
|
||||
}
|
||||
(TypeF::Enum(tyw1), TypeF::Enum(tyw2)) => {
|
||||
let rows1 = rows_as_set(tyw1);
|
||||
let rows2 = rows_as_set(tyw2);
|
||||
(TypeF::Enum(uty1), TypeF::Enum(uty2)) => {
|
||||
let rows1 = rows_as_set(uty1);
|
||||
let rows2 = rows_as_set(uty2);
|
||||
rows1.is_some() && rows2.is_some() && rows1 == rows2
|
||||
}
|
||||
(TypeF::Record(tyw1), TypeF::Record(tyw2)) => {
|
||||
(TypeF::Record(uty1), TypeF::Record(uty2)) => {
|
||||
fn type_eq_bounded_wrapper<E: TermEnvironment>(
|
||||
state: &mut State,
|
||||
tyw1: &&GenericUnifType<E>,
|
||||
uty1: &&GenericUnifType<E>,
|
||||
env1: &E,
|
||||
tyw2: &&GenericUnifType<E>,
|
||||
uty2: &&GenericUnifType<E>,
|
||||
env2: &E,
|
||||
) -> bool {
|
||||
type_eq_bounded(state, *tyw1, env1, *tyw2, env2)
|
||||
type_eq_bounded(state, *uty1, env1, *uty2, env2)
|
||||
}
|
||||
|
||||
let map1 = rows_as_map(tyw1);
|
||||
let map2 = rows_as_map(tyw2);
|
||||
let map1 = rows_as_map(uty1);
|
||||
let map2 = rows_as_map(uty2);
|
||||
|
||||
map1.zip(map2)
|
||||
.map(|(m1, m2)| map_eq(type_eq_bounded_wrapper, state, &m1, env1, &m2, env2))
|
||||
|
||||
@ -46,12 +46,12 @@ impl RowUnifError {
|
||||
RowUnifError::MissingDynTail() => UnifError::MissingDynTail(left, right),
|
||||
RowUnifError::ExtraRow(id) => UnifError::ExtraRow(id, left, right),
|
||||
RowUnifError::ExtraDynTail() => UnifError::ExtraDynTail(left, right),
|
||||
RowUnifError::RowKindMismatch(id, tyw1, tyw2) => {
|
||||
UnifError::RowKindMismatch(id, tyw1, tyw2)
|
||||
RowUnifError::RowKindMismatch(id, uty1, uty2) => {
|
||||
UnifError::RowKindMismatch(id, uty1, uty2)
|
||||
}
|
||||
RowUnifError::RowMismatch(id, err) => UnifError::RowMismatch(id, left, right, err),
|
||||
RowUnifError::UnsatConstr(id, tyw) => UnifError::RowConflict(id, tyw, left, right),
|
||||
RowUnifError::WithConst(c, tyw) => UnifError::WithConst(c, tyw),
|
||||
RowUnifError::UnsatConstr(id, uty) => UnifError::RowConflict(id, uty, left, right),
|
||||
RowUnifError::WithConst(c, uty) => UnifError::WithConst(c, uty),
|
||||
RowUnifError::ConstMismatch(c1, c2) => UnifError::ConstMismatch(c1, c2),
|
||||
RowUnifError::UnboundTypeVariable(id) => UnifError::UnboundTypeVariable(id),
|
||||
}
|
||||
@ -131,10 +131,10 @@ impl UnifError {
|
||||
reporting::to_type(state.table, state.names, names, ty2),
|
||||
pos_opt,
|
||||
),
|
||||
UnifError::RowMismatch(ident, tyw1, tyw2, err) => TypecheckError::RowMismatch(
|
||||
UnifError::RowMismatch(ident, uty1, uty2, err) => TypecheckError::RowMismatch(
|
||||
ident,
|
||||
reporting::to_type(state.table, state.names, names, tyw1),
|
||||
reporting::to_type(state.table, state.names, names, tyw2),
|
||||
reporting::to_type(state.table, state.names, names, uty1),
|
||||
reporting::to_type(state.table, state.names, names, uty2),
|
||||
Box::new((*err).into_typecheck_err_(state, names, TermPos::None)),
|
||||
pos_opt,
|
||||
),
|
||||
@ -160,31 +160,31 @@ impl UnifError {
|
||||
UnifError::IncomparableFlatTypes(rt1, rt2) => {
|
||||
TypecheckError::IncomparableFlatTypes(rt1, rt2, pos_opt)
|
||||
}
|
||||
UnifError::MissingRow(id, tyw1, tyw2) => TypecheckError::MissingRow(
|
||||
UnifError::MissingRow(id, uty1, uty2) => TypecheckError::MissingRow(
|
||||
id,
|
||||
reporting::to_type(state.table, state.names, names, tyw1),
|
||||
reporting::to_type(state.table, state.names, names, tyw2),
|
||||
reporting::to_type(state.table, state.names, names, uty1),
|
||||
reporting::to_type(state.table, state.names, names, uty2),
|
||||
pos_opt,
|
||||
),
|
||||
UnifError::MissingDynTail(tyw1, tyw2) => TypecheckError::MissingDynTail(
|
||||
reporting::to_type(state.table, state.names, names, tyw1),
|
||||
reporting::to_type(state.table, state.names, names, tyw2),
|
||||
UnifError::MissingDynTail(uty1, uty2) => TypecheckError::MissingDynTail(
|
||||
reporting::to_type(state.table, state.names, names, uty1),
|
||||
reporting::to_type(state.table, state.names, names, uty2),
|
||||
pos_opt,
|
||||
),
|
||||
UnifError::ExtraRow(id, tyw1, tyw2) => TypecheckError::ExtraRow(
|
||||
UnifError::ExtraRow(id, uty1, uty2) => TypecheckError::ExtraRow(
|
||||
id,
|
||||
reporting::to_type(state.table, state.names, names, tyw1),
|
||||
reporting::to_type(state.table, state.names, names, tyw2),
|
||||
reporting::to_type(state.table, state.names, names, uty1),
|
||||
reporting::to_type(state.table, state.names, names, uty2),
|
||||
pos_opt,
|
||||
),
|
||||
UnifError::ExtraDynTail(tyw1, tyw2) => TypecheckError::ExtraDynTail(
|
||||
reporting::to_type(state.table, state.names, names, tyw1),
|
||||
reporting::to_type(state.table, state.names, names, tyw2),
|
||||
UnifError::ExtraDynTail(uty1, uty2) => TypecheckError::ExtraDynTail(
|
||||
reporting::to_type(state.table, state.names, names, uty1),
|
||||
reporting::to_type(state.table, state.names, names, uty2),
|
||||
pos_opt,
|
||||
),
|
||||
UnifError::RowConflict(id, tyw, left, right) => TypecheckError::RowConflict(
|
||||
UnifError::RowConflict(id, uty, left, right) => TypecheckError::RowConflict(
|
||||
id,
|
||||
tyw.map(|tyw| reporting::to_type(state.table, state.names, names, tyw)),
|
||||
uty.map(|uty| reporting::to_type(state.table, state.names, names, uty)),
|
||||
reporting::to_type(state.table, state.names, names, left),
|
||||
reporting::to_type(state.table, state.names, names, right),
|
||||
pos_opt,
|
||||
@ -230,16 +230,16 @@ impl UnifError {
|
||||
let mut path = ty_path::Path::new();
|
||||
// The original expected and actual type. They are just updated once, in the first
|
||||
// iteration of the loop below.
|
||||
let mut tyws: Option<(UnifType, UnifType)> = None;
|
||||
let mut utys: Option<(UnifType, UnifType)> = None;
|
||||
|
||||
loop {
|
||||
match curr {
|
||||
UnifError::DomainMismatch(
|
||||
tyw1 @ UnifType::Concrete(TypeF::Arrow(_, _)),
|
||||
tyw2 @ UnifType::Concrete(TypeF::Arrow(_, _)),
|
||||
uty1 @ UnifType::Concrete(TypeF::Arrow(_, _)),
|
||||
uty2 @ UnifType::Concrete(TypeF::Arrow(_, _)),
|
||||
err,
|
||||
) => {
|
||||
tyws = tyws.or(Some((tyw1, tyw2)));
|
||||
utys = utys.or(Some((uty1, uty2)));
|
||||
path.push(ty_path::Elem::Domain);
|
||||
curr = *err;
|
||||
}
|
||||
@ -247,20 +247,20 @@ impl UnifError {
|
||||
"typechecking::to_type_path(): domain mismatch error on a non arrow type"
|
||||
),
|
||||
UnifError::CodomainMismatch(
|
||||
tyw1 @ UnifType::Concrete(TypeF::Arrow(_, _)),
|
||||
tyw2 @ UnifType::Concrete(TypeF::Arrow(_, _)),
|
||||
uty1 @ UnifType::Concrete(TypeF::Arrow(_, _)),
|
||||
uty2 @ UnifType::Concrete(TypeF::Arrow(_, _)),
|
||||
err,
|
||||
) => {
|
||||
tyws = tyws.or(Some((tyw1, tyw2)));
|
||||
utys = utys.or(Some((uty1, uty2)));
|
||||
path.push(ty_path::Elem::Codomain);
|
||||
curr = *err;
|
||||
}
|
||||
UnifError::CodomainMismatch(_, _, _) => panic!(
|
||||
"typechecking::to_type_path(): codomain mismatch error on a non arrow type"
|
||||
),
|
||||
// tyws equals to `None` iff we did not even enter the case above once, i.e. if
|
||||
// utys equals to `None` iff we did not even enter the case above once, i.e. if
|
||||
// `self` was indeed neither a `DomainMismatch` nor a `CodomainMismatch`
|
||||
_ => break tyws.map(|(expd, actual)| (expd, actual, path, curr)),
|
||||
_ => break utys.map(|(expd, actual)| (expd, actual, path, curr)),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
@ -3,7 +3,7 @@ use super::{TypeF, UnifType};
|
||||
|
||||
/// Multi-ary arrow constructor for types implementing `Into<TypeWrapper>`.
|
||||
#[macro_export]
|
||||
macro_rules! mk_tyw_arrow {
|
||||
macro_rules! mk_uty_arrow {
|
||||
($left:expr, $right:expr) => {
|
||||
$crate::typecheck::UnifType::Concrete(
|
||||
$crate::types::TypeF::Arrow(
|
||||
@ -13,14 +13,14 @@ macro_rules! mk_tyw_arrow {
|
||||
)
|
||||
};
|
||||
( $fst:expr, $snd:expr , $( $types:expr ),+ ) => {
|
||||
mk_tyw_arrow!($fst, mk_tyw_arrow!($snd, $( $types ),+))
|
||||
mk_uty_arrow!($fst, mk_uty_arrow!($snd, $( $types ),+))
|
||||
};
|
||||
}
|
||||
|
||||
/// Multi-ary enum row constructor for types implementing `Into<TypeWrapper>`.
|
||||
/// `mk_tyw_enum_row!(id1, .., idn; tail)` correspond to `<id1, .., idn | tail>.
|
||||
/// `mk_uty_enum_row!(id1, .., idn; tail)` correspond to `<id1, .., idn | tail>.
|
||||
#[macro_export]
|
||||
macro_rules! mk_tyw_enum_row {
|
||||
macro_rules! mk_uty_enum_row {
|
||||
() => {
|
||||
$crate::typecheck::UnifEnumRows::Concrete(EnumRowsF::Empty)
|
||||
};
|
||||
@ -31,17 +31,17 @@ macro_rules! mk_tyw_enum_row {
|
||||
$crate::typecheck::UnifEnumRows::Concrete(
|
||||
$crate::types::EnumRowsF::Extend {
|
||||
row: Ident::from($id),
|
||||
tail: Box::new(mk_tyw_enum_row!($( $ids ),* $(; $tail)?))
|
||||
tail: Box::new(mk_uty_enum_row!($( $ids ),* $(; $tail)?))
|
||||
}
|
||||
)
|
||||
};
|
||||
}
|
||||
|
||||
/// Multi-ary record row constructor for types implementing `Into<TypeWrapper>`.
|
||||
/// `mk_tyw_row!((id1, ty1), .., (idn, tyn); tail)` correspond to `{id1: ty1, .., idn: tyn |
|
||||
/// `mk_uty_row!((id1, ty1), .., (idn, tyn); tail)` correspond to `{id1: ty1, .., idn: tyn |
|
||||
/// tail}. The tail can be omitted, in which case the empty row is uses as a tail instead.
|
||||
#[macro_export]
|
||||
macro_rules! mk_tyw_row {
|
||||
macro_rules! mk_uty_row {
|
||||
() => {
|
||||
$crate::typecheck::UnifRecordRows::Concrete(RecordRowsF::Empty)
|
||||
};
|
||||
@ -55,31 +55,31 @@ macro_rules! mk_tyw_row {
|
||||
id: Ident::from($id),
|
||||
types: Box::new($ty.into()),
|
||||
},
|
||||
tail: Box::new(mk_tyw_row!($(($ids, $tys)),* $(; $tail)?)),
|
||||
tail: Box::new(mk_uty_row!($(($ids, $tys)),* $(; $tail)?)),
|
||||
}
|
||||
)
|
||||
};
|
||||
}
|
||||
|
||||
/// Wrapper around `mk_tyw_enum_row!` to build an enum type from an enum row.
|
||||
/// Wrapper around `mk_uty_enum_row!` to build an enum type from an enum row.
|
||||
#[macro_export]
|
||||
macro_rules! mk_tyw_enum {
|
||||
macro_rules! mk_uty_enum {
|
||||
($( $ids:expr ),* $(; $tail:expr)?) => {
|
||||
$crate::typecheck::UnifType::Concrete(
|
||||
$crate::types::TypeF::Enum(
|
||||
mk_tyw_enum_row!($( $ids ),* $(; $tail)?)
|
||||
mk_uty_enum_row!($( $ids ),* $(; $tail)?)
|
||||
)
|
||||
)
|
||||
};
|
||||
}
|
||||
|
||||
/// Wrapper around `mk_tyw_record!` to build a record type from a record row.
|
||||
/// Wrapper around `mk_uty_record!` to build a record type from a record row.
|
||||
#[macro_export]
|
||||
macro_rules! mk_tyw_record {
|
||||
macro_rules! mk_uty_record {
|
||||
($(($ids:expr, $tys:expr)),* $(; $tail:expr)?) => {
|
||||
$crate::typecheck::UnifType::Concrete(
|
||||
$crate::types::TypeF::Record(
|
||||
mk_tyw_row!($(($ids, $tys)),* $(; $tail)?)
|
||||
mk_uty_row!($(($ids, $tys)),* $(; $tail)?)
|
||||
)
|
||||
)
|
||||
};
|
||||
@ -57,7 +57,7 @@ use crate::{
|
||||
types::{
|
||||
EnumRow, EnumRows, EnumRowsF, RecordRowF, RecordRows, RecordRowsF, TypeF, Types, VarKind,
|
||||
},
|
||||
{mk_tyw_arrow, mk_tyw_enum, mk_tyw_enum_row, mk_tyw_record, mk_tyw_row},
|
||||
{mk_uty_arrow, mk_uty_enum, mk_uty_enum_row, mk_uty_record, mk_uty_row},
|
||||
};
|
||||
|
||||
use std::{
|
||||
@ -72,7 +72,7 @@ pub mod linearization;
|
||||
pub mod operation;
|
||||
pub mod reporting;
|
||||
#[macro_use]
|
||||
pub mod mk_typewrapper;
|
||||
pub mod mk_uniftype;
|
||||
pub mod eq;
|
||||
|
||||
use eq::{SimpleTermEnvironment, TermEnvironment};
|
||||
@ -805,7 +805,7 @@ fn walk<L: Linearizer>(
|
||||
}
|
||||
Term::Fun(id, t) => {
|
||||
// The parameter of an un-annotated function is assigned the type `Dyn`.
|
||||
ctxt.type_env.insert(*id, mk_typewrapper::dynamic());
|
||||
ctxt.type_env.insert(*id, mk_uniftype::dynamic());
|
||||
walk(state, ctxt, lin, linearizer, t)
|
||||
}
|
||||
Term::FunPattern(id, pat, t) => {
|
||||
@ -1044,16 +1044,16 @@ fn type_check_<L: Linearizer>(
|
||||
match t.as_ref() {
|
||||
Term::ParseError(_) => Ok(()),
|
||||
// null is inferred to be of type Dyn
|
||||
Term::Null => unify(state, &ctxt, ty, mk_typewrapper::dynamic())
|
||||
Term::Null => unify(state, &ctxt, ty, mk_uniftype::dynamic())
|
||||
.map_err(|err| err.into_typecheck_err(state, rt.pos)),
|
||||
Term::Bool(_) => unify(state, &ctxt, ty, mk_typewrapper::bool())
|
||||
Term::Bool(_) => unify(state, &ctxt, ty, mk_uniftype::bool())
|
||||
.map_err(|err| err.into_typecheck_err(state, rt.pos)),
|
||||
Term::Num(_) => unify(state, &ctxt, ty, mk_typewrapper::num())
|
||||
Term::Num(_) => unify(state, &ctxt, ty, mk_uniftype::num())
|
||||
.map_err(|err| err.into_typecheck_err(state, rt.pos)),
|
||||
Term::Str(_) => unify(state, &ctxt, ty, mk_typewrapper::str())
|
||||
Term::Str(_) => unify(state, &ctxt, ty, mk_uniftype::str())
|
||||
.map_err(|err| err.into_typecheck_err(state, rt.pos)),
|
||||
Term::StrChunks(chunks) => {
|
||||
unify(state, &ctxt, ty, mk_typewrapper::str())
|
||||
unify(state, &ctxt, ty, mk_uniftype::str())
|
||||
.map_err(|err| err.into_typecheck_err(state, rt.pos))?;
|
||||
|
||||
chunks
|
||||
@ -1067,7 +1067,7 @@ fn type_check_<L: Linearizer>(
|
||||
lin,
|
||||
linearizer.scope(),
|
||||
t,
|
||||
mk_typewrapper::str(),
|
||||
mk_uniftype::str(),
|
||||
),
|
||||
}
|
||||
})
|
||||
@ -1077,7 +1077,7 @@ fn type_check_<L: Linearizer>(
|
||||
// TODO what to do here, this makes more sense to me, but it means let x = foo in bar
|
||||
// behaves quite different to (\x.bar) foo, worth considering if it's ok to type these two differently
|
||||
let trg = state.table.fresh_type_uvar();
|
||||
let arr = mk_tyw_arrow!(src.clone(), trg.clone());
|
||||
let arr = mk_uty_arrow!(src.clone(), trg.clone());
|
||||
linearizer.retype_ident(lin, x, src.clone());
|
||||
|
||||
unify(state, &ctxt, ty, arr).map_err(|err| err.into_typecheck_err(state, rt.pos))?;
|
||||
@ -1090,7 +1090,7 @@ fn type_check_<L: Linearizer>(
|
||||
// TODO what to do here, this makes more sense to me, but it means let x = foo in bar
|
||||
// behaves quite different to (\x.bar) foo, worth considering if it's ok to type these two differently
|
||||
let trg = state.table.fresh_type_uvar();
|
||||
let arr = mk_tyw_arrow!(src.clone(), trg.clone());
|
||||
let arr = mk_uty_arrow!(src.clone(), trg.clone());
|
||||
if let Some(x) = x {
|
||||
linearizer.retype_ident(lin, x, src.clone());
|
||||
ctxt.type_env.insert(*x, src);
|
||||
@ -1102,7 +1102,7 @@ fn type_check_<L: Linearizer>(
|
||||
Term::Array(terms, _) => {
|
||||
let ty_elts = state.table.fresh_type_uvar();
|
||||
|
||||
unify(state, &ctxt, ty, mk_typewrapper::array(ty_elts.clone()))
|
||||
unify(state, &ctxt, ty, mk_uniftype::array(ty_elts.clone()))
|
||||
.map_err(|err| err.into_typecheck_err(state, rt.pos))?;
|
||||
|
||||
terms
|
||||
@ -1120,7 +1120,7 @@ fn type_check_<L: Linearizer>(
|
||||
}
|
||||
Term::Lbl(_) => {
|
||||
// TODO implement lbl type
|
||||
unify(state, &ctxt, ty, mk_typewrapper::dynamic())
|
||||
unify(state, &ctxt, ty, mk_uniftype::dynamic())
|
||||
.map_err(|err| err.into_typecheck_err(state, rt.pos))
|
||||
}
|
||||
Term::Let(x, re, rt, attrs) => {
|
||||
@ -1171,7 +1171,7 @@ fn type_check_<L: Linearizer>(
|
||||
}
|
||||
Term::App(e, t) => {
|
||||
let src = state.table.fresh_type_uvar();
|
||||
let arr = mk_tyw_arrow!(src.clone(), ty);
|
||||
let arr = mk_uty_arrow!(src.clone(), ty);
|
||||
|
||||
type_check_(state, ctxt.clone(), lin, linearizer.scope(), e, arr)?;
|
||||
type_check_(state, ctxt, lin, linearizer, t, src)
|
||||
@ -1200,13 +1200,13 @@ fn type_check_<L: Linearizer>(
|
||||
None => cases.iter().try_fold(
|
||||
EnumRowsF::Empty.into(),
|
||||
|acc, x| -> Result<UnifEnumRows, TypecheckError> {
|
||||
Ok(mk_tyw_enum_row!(*x.0; acc))
|
||||
Ok(mk_uty_enum_row!(*x.0; acc))
|
||||
},
|
||||
)?,
|
||||
};
|
||||
|
||||
unify(state, &ctxt, ty, res).map_err(|err| err.into_typecheck_err(state, rt.pos))?;
|
||||
type_check_(state, ctxt, lin, linearizer, exp, mk_tyw_enum!(; erows))
|
||||
type_check_(state, ctxt, lin, linearizer, exp, mk_uty_enum!(; erows))
|
||||
}
|
||||
Term::Var(x) => {
|
||||
let x_ty = ctxt
|
||||
@ -1221,7 +1221,7 @@ fn type_check_<L: Linearizer>(
|
||||
}
|
||||
Term::Enum(id) => {
|
||||
let row = state.table.fresh_erows_uvar();
|
||||
unify(state, &ctxt, ty, mk_tyw_enum!(*id; row))
|
||||
unify(state, &ctxt, ty, mk_uty_enum!(*id; row))
|
||||
.map_err(|err| err.into_typecheck_err(state, rt.pos))
|
||||
}
|
||||
// If some fields are defined dynamically, the only potential type that works is `{_ : a}`
|
||||
@ -1250,7 +1250,7 @@ fn type_check_<L: Linearizer>(
|
||||
)
|
||||
})?;
|
||||
|
||||
unify(state, &ctxt, ty, mk_typewrapper::dyn_record(ty_dict))
|
||||
unify(state, &ctxt, ty, mk_uniftype::dyn_record(ty_dict))
|
||||
.map_err(|err| err.into_typecheck_err(state, rt.pos))
|
||||
}
|
||||
Term::Record(record) | Term::RecRecord(record, ..) => {
|
||||
@ -1284,7 +1284,7 @@ fn type_check_<L: Linearizer>(
|
||||
})
|
||||
} else {
|
||||
let rows = record.fields.iter().try_fold(
|
||||
mk_tyw_row!(),
|
||||
mk_uty_row!(),
|
||||
|acc, (id, field)| -> Result<UnifRecordRows, TypecheckError> {
|
||||
// In the case of a recursive record, new types (either type variables or
|
||||
// annotations) have already be determined and put in the typing context,
|
||||
@ -1304,11 +1304,11 @@ fn type_check_<L: Linearizer>(
|
||||
ty.clone(),
|
||||
)?;
|
||||
|
||||
Ok(mk_tyw_row!((*id, ty); acc))
|
||||
Ok(mk_uty_row!((*id, ty); acc))
|
||||
},
|
||||
)?;
|
||||
|
||||
unify(state, &ctxt, ty, mk_tyw_record!(; rows))
|
||||
unify(state, &ctxt, ty, mk_uty_record!(; rows))
|
||||
.map_err(|err| err.into_typecheck_err(state, rt.pos))
|
||||
}
|
||||
}
|
||||
@ -1402,14 +1402,14 @@ fn type_check_<L: Linearizer>(
|
||||
// TODO: we might have something to with the linearizer to clear the current
|
||||
// metadata. It looks like it may be unduly attached to the next field definition,
|
||||
// which is not critical, but still a bug.
|
||||
_ => unify(state, &ctxt, ty, mk_typewrapper::dynamic())
|
||||
_ => unify(state, &ctxt, ty, mk_uniftype::dynamic())
|
||||
.map_err(|err| err.into_typecheck_err(state, rt.pos)),
|
||||
}
|
||||
}
|
||||
Term::SealingKey(_) => unify(state, &ctxt, ty, mk_typewrapper::sym())
|
||||
Term::SealingKey(_) => unify(state, &ctxt, ty, mk_uniftype::sym())
|
||||
.map_err(|err| err.into_typecheck_err(state, rt.pos)),
|
||||
Term::Sealed(_, t, _) => type_check_(state, ctxt, lin, linearizer, t, ty),
|
||||
Term::Import(_) => unify(state, &ctxt, ty, mk_typewrapper::dynamic())
|
||||
Term::Import(_) => unify(state, &ctxt, ty, mk_uniftype::dynamic())
|
||||
.map_err(|err| err.into_typecheck_err(state, rt.pos)),
|
||||
// We use the apparent type of the import for checking. This function doesn't recursively
|
||||
// typecheck imports: this is the responsibility of the caller.
|
||||
@ -1810,12 +1810,12 @@ pub fn unify(
|
||||
(TypeF::Flat(s), TypeF::Flat(t)) => Err(UnifError::IncomparableFlatTypes(s, t)),
|
||||
(TypeF::Enum(erows1), TypeF::Enum(erows2)) => {
|
||||
unify_erows(state, erows1.clone(), erows2.clone()).map_err(|err| {
|
||||
err.into_unif_err(mk_tyw_enum!(; erows1), mk_tyw_enum!(; erows2))
|
||||
err.into_unif_err(mk_uty_enum!(; erows1), mk_uty_enum!(; erows2))
|
||||
})
|
||||
}
|
||||
(TypeF::Record(rrows1), TypeF::Record(rrows2)) => {
|
||||
unify_rrows(state, ctxt, rrows1.clone(), rrows2.clone()).map_err(|err| {
|
||||
err.into_unif_err(mk_tyw_record!(; rrows1), mk_tyw_record!(; rrows2))
|
||||
err.into_unif_err(mk_uty_record!(; rrows1), mk_uty_record!(; rrows2))
|
||||
})
|
||||
}
|
||||
(TypeF::Dict(t1), TypeF::Dict(t2)) => unify(state, ctxt, *t1, *t2),
|
||||
|
||||
@ -5,7 +5,7 @@ use crate::{
|
||||
term::{BinaryOp, NAryOp, UnaryOp},
|
||||
types::TypeF,
|
||||
};
|
||||
use crate::{mk_tyw_arrow, mk_tyw_enum, mk_tyw_enum_row, mk_tyw_record, mk_tyw_row};
|
||||
use crate::{mk_uty_arrow, mk_uty_enum, mk_uty_enum_row, mk_uty_record, mk_uty_row};
|
||||
|
||||
/// Type of unary operations.
|
||||
pub fn get_uop_type(
|
||||
@ -18,37 +18,36 @@ pub fn get_uop_type(
|
||||
let branches = UnifType::UnifVar(state.table.fresh_type_var_id());
|
||||
|
||||
(
|
||||
mk_typewrapper::bool(),
|
||||
mk_tyw_arrow!(branches.clone(), branches.clone(), branches),
|
||||
mk_uniftype::bool(),
|
||||
mk_uty_arrow!(branches.clone(), branches.clone(), branches),
|
||||
)
|
||||
}
|
||||
// Dyn -> [| `Num, `Bool, `Str, `Enum, `Fun, `Array, `Record, `Lbl, `Other |]
|
||||
UnaryOp::Typeof() => (
|
||||
mk_typewrapper::dynamic(),
|
||||
mk_tyw_enum!("Num", "Bool", "Str", "Enum", "Fun", "Array", "Record", "Lbl", "Other"),
|
||||
mk_uniftype::dynamic(),
|
||||
mk_uty_enum!("Num", "Bool", "Str", "Enum", "Fun", "Array", "Record", "Lbl", "Other"),
|
||||
),
|
||||
// Bool -> Bool -> Bool
|
||||
UnaryOp::BoolAnd() | UnaryOp::BoolOr() => (
|
||||
mk_typewrapper::bool(),
|
||||
mk_tyw_arrow!(TypeF::Bool, TypeF::Bool),
|
||||
),
|
||||
UnaryOp::BoolAnd() | UnaryOp::BoolOr() => {
|
||||
(mk_uniftype::bool(), mk_uty_arrow!(TypeF::Bool, TypeF::Bool))
|
||||
}
|
||||
// Bool -> Bool
|
||||
UnaryOp::BoolNot() => (mk_typewrapper::bool(), mk_typewrapper::bool()),
|
||||
UnaryOp::BoolNot() => (mk_uniftype::bool(), mk_uniftype::bool()),
|
||||
// forall a. Dyn -> a
|
||||
UnaryOp::Blame() => {
|
||||
let res = UnifType::UnifVar(state.table.fresh_type_var_id());
|
||||
|
||||
(mk_typewrapper::dynamic(), res)
|
||||
(mk_uniftype::dynamic(), res)
|
||||
}
|
||||
// Dyn -> Bool
|
||||
UnaryOp::Pol() => (mk_typewrapper::dynamic(), mk_typewrapper::bool()),
|
||||
UnaryOp::Pol() => (mk_uniftype::dynamic(), mk_uniftype::bool()),
|
||||
// forall rows. < | rows> -> <id | rows>
|
||||
UnaryOp::Embed(id) => {
|
||||
let row_var_id = state.table.fresh_erows_var_id();
|
||||
let row = UnifEnumRows::UnifVar(row_var_id);
|
||||
|
||||
let domain = mk_tyw_enum!(; row.clone());
|
||||
let codomain = mk_tyw_enum!(*id; row);
|
||||
let domain = mk_uty_enum!(; row.clone());
|
||||
let codomain = mk_uty_enum!(*id; row);
|
||||
|
||||
// The codomain is the only type which can impose a constraint on the fresh row
|
||||
// unification variable, namely that it can't contain `id`.
|
||||
@ -59,34 +58,34 @@ pub fn get_uop_type(
|
||||
UnaryOp::Switch(_) => panic!("cannot typecheck Switch()"),
|
||||
// Dyn -> Dyn
|
||||
UnaryOp::ChangePolarity() | UnaryOp::GoDom() | UnaryOp::GoCodom() | UnaryOp::GoArray() => {
|
||||
(mk_typewrapper::dynamic(), mk_typewrapper::dynamic())
|
||||
(mk_uniftype::dynamic(), mk_uniftype::dynamic())
|
||||
}
|
||||
// forall rows a. { id: a | rows} -> a
|
||||
UnaryOp::StaticAccess(id) => {
|
||||
let rows = state.table.fresh_rrows_uvar();
|
||||
let res = state.table.fresh_type_uvar();
|
||||
|
||||
(mk_tyw_record!((*id, res.clone()); rows), res)
|
||||
(mk_uty_record!((*id, res.clone()); rows), res)
|
||||
}
|
||||
// forall a b. Array a -> (a -> b) -> Array b
|
||||
UnaryOp::ArrayMap() => {
|
||||
let a = UnifType::UnifVar(state.table.fresh_type_var_id());
|
||||
let b = UnifType::UnifVar(state.table.fresh_type_var_id());
|
||||
|
||||
let f_type = mk_tyw_arrow!(a.clone(), b.clone());
|
||||
let f_type = mk_uty_arrow!(a.clone(), b.clone());
|
||||
(
|
||||
mk_typewrapper::array(a),
|
||||
mk_tyw_arrow!(f_type, mk_typewrapper::array(b)),
|
||||
mk_uniftype::array(a),
|
||||
mk_uty_arrow!(f_type, mk_uniftype::array(b)),
|
||||
)
|
||||
}
|
||||
// forall a. Num -> (Num -> a) -> Array a
|
||||
UnaryOp::ArrayGen() => {
|
||||
let a = UnifType::UnifVar(state.table.fresh_type_var_id());
|
||||
|
||||
let f_type = mk_tyw_arrow!(TypeF::Num, a.clone());
|
||||
let f_type = mk_uty_arrow!(TypeF::Num, a.clone());
|
||||
(
|
||||
mk_typewrapper::num(),
|
||||
mk_tyw_arrow!(f_type, mk_typewrapper::array(a)),
|
||||
mk_uniftype::num(),
|
||||
mk_uty_arrow!(f_type, mk_uniftype::array(a)),
|
||||
)
|
||||
}
|
||||
// forall a b. { _ : a} -> (Str -> a -> b) -> { _ : b }
|
||||
@ -97,10 +96,10 @@ pub fn get_uop_type(
|
||||
let a = UnifType::UnifVar(state.table.fresh_type_var_id());
|
||||
let b = UnifType::UnifVar(state.table.fresh_type_var_id());
|
||||
|
||||
let f_type = mk_tyw_arrow!(TypeF::Str, a.clone(), b.clone());
|
||||
let f_type = mk_uty_arrow!(TypeF::Str, a.clone(), b.clone());
|
||||
(
|
||||
mk_typewrapper::dyn_record(a),
|
||||
mk_tyw_arrow!(f_type, mk_typewrapper::dyn_record(b)),
|
||||
mk_uniftype::dyn_record(a),
|
||||
mk_uty_arrow!(f_type, mk_uniftype::dyn_record(b)),
|
||||
)
|
||||
}
|
||||
// forall a b. a -> b -> b
|
||||
@ -108,93 +107,90 @@ pub fn get_uop_type(
|
||||
let fst = UnifType::UnifVar(state.table.fresh_type_var_id());
|
||||
let snd = UnifType::UnifVar(state.table.fresh_type_var_id());
|
||||
|
||||
(fst, mk_tyw_arrow!(snd.clone(), snd))
|
||||
(fst, mk_uty_arrow!(snd.clone(), snd))
|
||||
}
|
||||
// forall a. Array a -> a
|
||||
UnaryOp::ArrayHead() => {
|
||||
let ty_elt = UnifType::UnifVar(state.table.fresh_type_var_id());
|
||||
(mk_typewrapper::array(ty_elt.clone()), ty_elt)
|
||||
(mk_uniftype::array(ty_elt.clone()), ty_elt)
|
||||
}
|
||||
// forall a. Array a -> Array a
|
||||
UnaryOp::ArrayTail() => {
|
||||
let ty_elt = UnifType::UnifVar(state.table.fresh_type_var_id());
|
||||
(
|
||||
mk_typewrapper::array(ty_elt.clone()),
|
||||
mk_typewrapper::array(ty_elt),
|
||||
mk_uniftype::array(ty_elt.clone()),
|
||||
mk_uniftype::array(ty_elt),
|
||||
)
|
||||
}
|
||||
// forall a. Array a -> Num
|
||||
UnaryOp::ArrayLength() => {
|
||||
let ty_elt = UnifType::UnifVar(state.table.fresh_type_var_id());
|
||||
(mk_typewrapper::array(ty_elt), mk_typewrapper::num())
|
||||
(mk_uniftype::array(ty_elt), mk_uniftype::num())
|
||||
}
|
||||
// This should not happen, as ChunksConcat() is only produced during evaluation.
|
||||
UnaryOp::ChunksConcat() => panic!("cannot type ChunksConcat()"),
|
||||
// BEFORE: forall rows. { rows } -> Array
|
||||
// Dyn -> Array Str
|
||||
UnaryOp::FieldsOf() => (
|
||||
mk_typewrapper::dynamic(),
|
||||
//mk_tyw_record!(; TypeWrapper::Ptr(state.table.fresh_type_var_id())),
|
||||
mk_typewrapper::array(TypeF::Str),
|
||||
mk_uniftype::dynamic(),
|
||||
//mk_uty_record!(; TypeWrapper::Ptr(state.table.fresh_type_var_id())),
|
||||
mk_uniftype::array(TypeF::Str),
|
||||
),
|
||||
// Dyn -> Array Dyn
|
||||
UnaryOp::ValuesOf() => (mk_typewrapper::dynamic(), mk_typewrapper::array(TypeF::Dyn)),
|
||||
UnaryOp::ValuesOf() => (mk_uniftype::dynamic(), mk_uniftype::array(TypeF::Dyn)),
|
||||
// Str -> Str
|
||||
UnaryOp::StrTrim() => (mk_typewrapper::str(), mk_typewrapper::str()),
|
||||
UnaryOp::StrTrim() => (mk_uniftype::str(), mk_uniftype::str()),
|
||||
// Str -> Array Str
|
||||
UnaryOp::StrChars() => (
|
||||
mk_typewrapper::str(),
|
||||
mk_typewrapper::array(mk_typewrapper::str()),
|
||||
),
|
||||
UnaryOp::StrChars() => (mk_uniftype::str(), mk_uniftype::array(mk_uniftype::str())),
|
||||
// Str -> Num
|
||||
UnaryOp::CharCode() => (mk_typewrapper::str(), mk_typewrapper::num()),
|
||||
UnaryOp::CharCode() => (mk_uniftype::str(), mk_uniftype::num()),
|
||||
// Num -> Str
|
||||
UnaryOp::CharFromCode() => (mk_typewrapper::num(), mk_typewrapper::str()),
|
||||
UnaryOp::CharFromCode() => (mk_uniftype::num(), mk_uniftype::str()),
|
||||
// Str -> Str
|
||||
UnaryOp::StrUppercase() => (mk_typewrapper::str(), mk_typewrapper::str()),
|
||||
UnaryOp::StrUppercase() => (mk_uniftype::str(), mk_uniftype::str()),
|
||||
// Str -> Str
|
||||
UnaryOp::StrLowercase() => (mk_typewrapper::str(), mk_typewrapper::str()),
|
||||
UnaryOp::StrLowercase() => (mk_uniftype::str(), mk_uniftype::str()),
|
||||
// Str -> Num
|
||||
UnaryOp::StrLength() => (mk_typewrapper::str(), mk_typewrapper::num()),
|
||||
UnaryOp::StrLength() => (mk_uniftype::str(), mk_uniftype::num()),
|
||||
// Dyn -> Str
|
||||
UnaryOp::ToStr() => (mk_typewrapper::dynamic(), mk_typewrapper::str()),
|
||||
UnaryOp::ToStr() => (mk_uniftype::dynamic(), mk_uniftype::str()),
|
||||
// Str -> Num
|
||||
UnaryOp::NumFromStr() => (mk_typewrapper::str(), mk_typewrapper::num()),
|
||||
UnaryOp::NumFromStr() => (mk_uniftype::str(), mk_uniftype::num()),
|
||||
// Str -> < | a> for a rigid type variable a
|
||||
UnaryOp::EnumFromStr() => (
|
||||
mk_typewrapper::str(),
|
||||
mk_tyw_enum!(; state.table.fresh_erows_const()),
|
||||
mk_uniftype::str(),
|
||||
mk_uty_enum!(; state.table.fresh_erows_const()),
|
||||
),
|
||||
// Str -> Str -> Bool
|
||||
UnaryOp::StrIsMatch() => (
|
||||
mk_typewrapper::str(),
|
||||
mk_tyw_arrow!(mk_typewrapper::str(), mk_typewrapper::bool()),
|
||||
mk_uniftype::str(),
|
||||
mk_uty_arrow!(mk_uniftype::str(), mk_uniftype::bool()),
|
||||
),
|
||||
// Str -> Str -> {match: Str, index: Num, groups: Array Str}
|
||||
UnaryOp::StrMatch() => (
|
||||
mk_typewrapper::str(),
|
||||
mk_tyw_arrow!(
|
||||
mk_typewrapper::str(),
|
||||
mk_tyw_record!(
|
||||
mk_uniftype::str(),
|
||||
mk_uty_arrow!(
|
||||
mk_uniftype::str(),
|
||||
mk_uty_record!(
|
||||
("match", TypeF::Str),
|
||||
("index", TypeF::Num),
|
||||
("groups", mk_typewrapper::array(TypeF::Str))
|
||||
("groups", mk_uniftype::array(TypeF::Str))
|
||||
)
|
||||
),
|
||||
),
|
||||
// Str -> Bool
|
||||
UnaryOp::StrIsMatchCompiled(_) => (mk_typewrapper::str(), mk_typewrapper::bool()),
|
||||
UnaryOp::StrIsMatchCompiled(_) => (mk_uniftype::str(), mk_uniftype::bool()),
|
||||
// Str -> {match: Str, index: Num, groups: Array Str}
|
||||
UnaryOp::StrMatchCompiled(_) => (
|
||||
mk_typewrapper::str(),
|
||||
mk_tyw_record!(
|
||||
mk_uniftype::str(),
|
||||
mk_uty_record!(
|
||||
("match", TypeF::Str),
|
||||
("index", TypeF::Num),
|
||||
("groups", mk_typewrapper::array(TypeF::Str))
|
||||
("groups", mk_uniftype::array(TypeF::Str))
|
||||
),
|
||||
),
|
||||
// Dyn -> Dyn
|
||||
UnaryOp::Force(_) => (mk_typewrapper::dynamic(), mk_typewrapper::dynamic()),
|
||||
UnaryOp::Force(_) => (mk_uniftype::dynamic(), mk_uniftype::dynamic()),
|
||||
// forall a. a -> a
|
||||
UnaryOp::PushDefault() => {
|
||||
let ty = state.table.fresh_type_uvar();
|
||||
@ -219,70 +215,58 @@ pub fn get_bop_type(
|
||||
| BinaryOp::Sub()
|
||||
| BinaryOp::Mult()
|
||||
| BinaryOp::Div()
|
||||
| BinaryOp::Modulo() => (
|
||||
mk_typewrapper::num(),
|
||||
mk_typewrapper::num(),
|
||||
mk_typewrapper::num(),
|
||||
),
|
||||
| BinaryOp::Modulo() => (mk_uniftype::num(), mk_uniftype::num(), mk_uniftype::num()),
|
||||
// Sym -> Dyn -> Dyn -> Dyn
|
||||
BinaryOp::Seal() => (
|
||||
mk_typewrapper::sym(),
|
||||
mk_typewrapper::dynamic(),
|
||||
mk_tyw_arrow!(TypeF::Dyn, TypeF::Dyn),
|
||||
mk_uniftype::sym(),
|
||||
mk_uniftype::dynamic(),
|
||||
mk_uty_arrow!(TypeF::Dyn, TypeF::Dyn),
|
||||
),
|
||||
// Str -> Str -> Str
|
||||
BinaryOp::StrConcat() => (
|
||||
mk_typewrapper::str(),
|
||||
mk_typewrapper::str(),
|
||||
mk_typewrapper::str(),
|
||||
),
|
||||
BinaryOp::StrConcat() => (mk_uniftype::str(), mk_uniftype::str(), mk_uniftype::str()),
|
||||
// Ideally: Contract -> Label -> Dyn -> Dyn
|
||||
// Currenty: Dyn -> Dyn -> (Dyn -> Dyn)
|
||||
BinaryOp::Assume() => (
|
||||
mk_typewrapper::dynamic(),
|
||||
mk_typewrapper::dynamic(),
|
||||
mk_tyw_arrow!(mk_typewrapper::dynamic(), mk_typewrapper::dynamic()),
|
||||
mk_uniftype::dynamic(),
|
||||
mk_uniftype::dynamic(),
|
||||
mk_uty_arrow!(mk_uniftype::dynamic(), mk_uniftype::dynamic()),
|
||||
),
|
||||
// Sym -> Dyn -> Dyn -> Dyn
|
||||
BinaryOp::Unseal() => (
|
||||
mk_typewrapper::sym(),
|
||||
mk_typewrapper::dynamic(),
|
||||
mk_tyw_arrow!(TypeF::Dyn, TypeF::Dyn),
|
||||
mk_uniftype::sym(),
|
||||
mk_uniftype::dynamic(),
|
||||
mk_uty_arrow!(TypeF::Dyn, TypeF::Dyn),
|
||||
),
|
||||
// Str -> Dyn -> Dyn
|
||||
BinaryOp::Tag() => (
|
||||
mk_typewrapper::str(),
|
||||
mk_typewrapper::dynamic(),
|
||||
mk_typewrapper::dynamic(),
|
||||
mk_uniftype::str(),
|
||||
mk_uniftype::dynamic(),
|
||||
mk_uniftype::dynamic(),
|
||||
),
|
||||
// forall a b. a -> b -> Bool
|
||||
BinaryOp::Eq() => (
|
||||
UnifType::UnifVar(state.table.fresh_type_var_id()),
|
||||
UnifType::UnifVar(state.table.fresh_type_var_id()),
|
||||
mk_typewrapper::bool(),
|
||||
mk_uniftype::bool(),
|
||||
),
|
||||
// Num -> Num -> Bool
|
||||
BinaryOp::LessThan()
|
||||
| BinaryOp::LessOrEq()
|
||||
| BinaryOp::GreaterThan()
|
||||
| BinaryOp::GreaterOrEq() => (
|
||||
mk_typewrapper::num(),
|
||||
mk_typewrapper::num(),
|
||||
mk_typewrapper::bool(),
|
||||
),
|
||||
| BinaryOp::GreaterOrEq() => (mk_uniftype::num(), mk_uniftype::num(), mk_uniftype::bool()),
|
||||
// Str -> Dyn -> Dyn
|
||||
BinaryOp::GoField() => (
|
||||
mk_typewrapper::str(),
|
||||
mk_typewrapper::dynamic(),
|
||||
mk_typewrapper::dynamic(),
|
||||
mk_uniftype::str(),
|
||||
mk_uniftype::dynamic(),
|
||||
mk_uniftype::dynamic(),
|
||||
),
|
||||
// forall a. Str -> { _ : a} -> a
|
||||
BinaryOp::DynAccess() => {
|
||||
let res = UnifType::UnifVar(state.table.fresh_type_var_id());
|
||||
|
||||
(
|
||||
mk_typewrapper::str(),
|
||||
mk_typewrapper::dyn_record(res.clone()),
|
||||
mk_uniftype::str(),
|
||||
mk_uniftype::dyn_record(res.clone()),
|
||||
res,
|
||||
)
|
||||
}
|
||||
@ -290,98 +274,90 @@ pub fn get_bop_type(
|
||||
BinaryOp::DynExtend() => {
|
||||
let res = UnifType::UnifVar(state.table.fresh_type_var_id());
|
||||
(
|
||||
mk_typewrapper::str(),
|
||||
mk_typewrapper::dyn_record(res.clone()),
|
||||
mk_tyw_arrow!(res.clone(), mk_typewrapper::dyn_record(res)),
|
||||
mk_uniftype::str(),
|
||||
mk_uniftype::dyn_record(res.clone()),
|
||||
mk_uty_arrow!(res.clone(), mk_uniftype::dyn_record(res)),
|
||||
)
|
||||
}
|
||||
// forall a. Str -> { _ : a } -> { _ : a}
|
||||
BinaryOp::DynRemove() => {
|
||||
let res = UnifType::UnifVar(state.table.fresh_type_var_id());
|
||||
(
|
||||
mk_typewrapper::str(),
|
||||
mk_typewrapper::dyn_record(res.clone()),
|
||||
mk_typewrapper::dyn_record(res),
|
||||
mk_uniftype::str(),
|
||||
mk_uniftype::dyn_record(res.clone()),
|
||||
mk_uniftype::dyn_record(res),
|
||||
)
|
||||
}
|
||||
// forall a. Str -> {_: a} -> Bool
|
||||
BinaryOp::HasField() => {
|
||||
let ty_elt = UnifType::UnifVar(state.table.fresh_type_var_id());
|
||||
(
|
||||
mk_typewrapper::str(),
|
||||
mk_typewrapper::dyn_record(ty_elt),
|
||||
mk_typewrapper::bool(),
|
||||
mk_uniftype::str(),
|
||||
mk_uniftype::dyn_record(ty_elt),
|
||||
mk_uniftype::bool(),
|
||||
)
|
||||
}
|
||||
// forall a. Array a -> Array a -> Array a
|
||||
BinaryOp::ArrayConcat() => {
|
||||
let ty_elt = UnifType::UnifVar(state.table.fresh_type_var_id());
|
||||
let ty_array = mk_typewrapper::array(ty_elt);
|
||||
let ty_array = mk_uniftype::array(ty_elt);
|
||||
(ty_array.clone(), ty_array.clone(), ty_array)
|
||||
}
|
||||
// forall a. Array a -> Num -> a
|
||||
BinaryOp::ArrayElemAt() => {
|
||||
let ty_elt = UnifType::UnifVar(state.table.fresh_type_var_id());
|
||||
(
|
||||
mk_typewrapper::array(ty_elt.clone()),
|
||||
mk_typewrapper::num(),
|
||||
mk_uniftype::array(ty_elt.clone()),
|
||||
mk_uniftype::num(),
|
||||
ty_elt,
|
||||
)
|
||||
}
|
||||
// Dyn -> Dyn -> Dyn
|
||||
BinaryOp::Merge() => (
|
||||
mk_typewrapper::dynamic(),
|
||||
mk_typewrapper::dynamic(),
|
||||
mk_typewrapper::dynamic(),
|
||||
mk_uniftype::dynamic(),
|
||||
mk_uniftype::dynamic(),
|
||||
mk_uniftype::dynamic(),
|
||||
),
|
||||
// <Md5, Sha1, Sha256, Sha512> -> Str -> Str
|
||||
BinaryOp::Hash() => (
|
||||
mk_tyw_enum!("Md5", "Sha1", "Sha256", "Sha512"),
|
||||
mk_typewrapper::str(),
|
||||
mk_typewrapper::str(),
|
||||
mk_uty_enum!("Md5", "Sha1", "Sha256", "Sha512"),
|
||||
mk_uniftype::str(),
|
||||
mk_uniftype::str(),
|
||||
),
|
||||
// forall a. <Json, Yaml, Toml> -> a -> Str
|
||||
BinaryOp::Serialize() => {
|
||||
let ty_input = UnifType::UnifVar(state.table.fresh_type_var_id());
|
||||
(
|
||||
mk_tyw_enum!("Json", "Yaml", "Toml"),
|
||||
mk_uty_enum!("Json", "Yaml", "Toml"),
|
||||
ty_input,
|
||||
mk_typewrapper::str(),
|
||||
mk_uniftype::str(),
|
||||
)
|
||||
}
|
||||
// <Json, Yaml, Toml> -> Str -> Dyn
|
||||
BinaryOp::Deserialize() => (
|
||||
mk_tyw_enum!("Json", "Yaml", "Toml"),
|
||||
mk_typewrapper::str(),
|
||||
mk_typewrapper::dynamic(),
|
||||
mk_uty_enum!("Json", "Yaml", "Toml"),
|
||||
mk_uniftype::str(),
|
||||
mk_uniftype::dynamic(),
|
||||
),
|
||||
// Num -> Num -> Num
|
||||
BinaryOp::Pow() => (
|
||||
mk_typewrapper::num(),
|
||||
mk_typewrapper::num(),
|
||||
mk_typewrapper::num(),
|
||||
),
|
||||
BinaryOp::Pow() => (mk_uniftype::num(), mk_uniftype::num(), mk_uniftype::num()),
|
||||
// Str -> Str -> Bool
|
||||
BinaryOp::StrContains() => (
|
||||
mk_typewrapper::str(),
|
||||
mk_typewrapper::str(),
|
||||
mk_typewrapper::bool(),
|
||||
),
|
||||
BinaryOp::StrContains() => (mk_uniftype::str(), mk_uniftype::str(), mk_uniftype::bool()),
|
||||
// Str -> Str -> Array Str
|
||||
BinaryOp::StrSplit() => (
|
||||
mk_typewrapper::str(),
|
||||
mk_typewrapper::str(),
|
||||
mk_typewrapper::array(TypeF::Str),
|
||||
mk_uniftype::str(),
|
||||
mk_uniftype::str(),
|
||||
mk_uniftype::array(TypeF::Str),
|
||||
),
|
||||
// The first argument is a contract, the second is a label.
|
||||
// forall a. Dyn -> Dyn -> Array a -> Array a
|
||||
BinaryOp::ArrayLazyAssume() => {
|
||||
let ty_elt = UnifType::UnifVar(state.table.fresh_type_var_id());
|
||||
let ty_array = mk_typewrapper::array(ty_elt);
|
||||
let ty_array = mk_uniftype::array(ty_elt);
|
||||
(
|
||||
mk_typewrapper::dynamic(),
|
||||
mk_typewrapper::dynamic(),
|
||||
mk_tyw_arrow!(ty_array.clone(), ty_array),
|
||||
mk_uniftype::dynamic(),
|
||||
mk_uniftype::dynamic(),
|
||||
mk_uty_arrow!(ty_array.clone(), ty_array),
|
||||
)
|
||||
}
|
||||
})
|
||||
@ -394,21 +370,13 @@ pub fn get_nop_type(
|
||||
Ok(match op {
|
||||
// Str -> Str -> Str -> Str
|
||||
NAryOp::StrReplace() | NAryOp::StrReplaceRegex() => (
|
||||
vec![
|
||||
mk_typewrapper::str(),
|
||||
mk_typewrapper::str(),
|
||||
mk_typewrapper::str(),
|
||||
],
|
||||
mk_typewrapper::str(),
|
||||
vec![mk_uniftype::str(), mk_uniftype::str(), mk_uniftype::str()],
|
||||
mk_uniftype::str(),
|
||||
),
|
||||
// Str -> Num -> Num -> Str
|
||||
NAryOp::StrSubstr() => (
|
||||
vec![
|
||||
mk_typewrapper::str(),
|
||||
mk_typewrapper::num(),
|
||||
mk_typewrapper::num(),
|
||||
],
|
||||
mk_typewrapper::str(),
|
||||
vec![mk_uniftype::str(), mk_uniftype::num(), mk_uniftype::num()],
|
||||
mk_uniftype::str(),
|
||||
),
|
||||
// This should not happen, as Switch() is only produced during evaluation.
|
||||
NAryOp::MergeContract() => panic!("cannot typecheck MergeContract()"),
|
||||
|
||||
Loading…
Reference in New Issue
Block a user