diff --git a/lsp/nls/src/requests/completion.rs b/lsp/nls/src/requests/completion.rs index 23f33dd4..b9d643ca 100644 --- a/lsp/nls/src/requests/completion.rs +++ b/lsp/nls/src/requests/completion.rs @@ -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 diff --git a/src/typecheck/eq.rs b/src/typecheck/eq.rs index 076634b8..1e8fb0b8 100644 --- a/src/typecheck/eq.rs +++ b/src/typecheck/eq.rs @@ -419,31 +419,31 @@ fn type_eq_bounded( | (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( state: &mut State, - tyw1: &&GenericUnifType, + uty1: &&GenericUnifType, env1: &E, - tyw2: &&GenericUnifType, + uty2: &&GenericUnifType, 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)) diff --git a/src/typecheck/error.rs b/src/typecheck/error.rs index 881d0870..7acfea70 100644 --- a/src/typecheck/error.rs +++ b/src/typecheck/error.rs @@ -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)), } } } diff --git a/src/typecheck/mk_typewrapper.rs b/src/typecheck/mk_uniftype.rs similarity index 80% rename from src/typecheck/mk_typewrapper.rs rename to src/typecheck/mk_uniftype.rs index a95b984f..7f5b37b3 100644 --- a/src/typecheck/mk_typewrapper.rs +++ b/src/typecheck/mk_uniftype.rs @@ -3,7 +3,7 @@ use super::{TypeF, UnifType}; /// Multi-ary arrow constructor for types implementing `Into`. #[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`. -/// `mk_tyw_enum_row!(id1, .., idn; tail)` correspond to `. +/// `mk_uty_enum_row!(id1, .., idn; tail)` correspond to `. #[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`. -/// `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)?) ) ) }; diff --git a/src/typecheck/mod.rs b/src/typecheck/mod.rs index ce1cbb43..499883fe 100644 --- a/src/typecheck/mod.rs +++ b/src/typecheck/mod.rs @@ -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( } 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_( 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_( lin, linearizer.scope(), t, - mk_typewrapper::str(), + mk_uniftype::str(), ), } }) @@ -1077,7 +1077,7 @@ fn type_check_( // 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_( // 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_( 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_( } 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_( } 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_( None => cases.iter().try_fold( EnumRowsF::Empty.into(), |acc, x| -> Result { - 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_( } 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_( ) })?; - 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_( }) } else { let rows = record.fields.iter().try_fold( - mk_tyw_row!(), + mk_uty_row!(), |acc, (id, field)| -> Result { // 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_( 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_( // 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), diff --git a/src/typecheck/operation.rs b/src/typecheck/operation.rs index 9f48699f..ca4fa21c 100644 --- a/src/typecheck/operation.rs +++ b/src/typecheck/operation.rs @@ -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> -> 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(), ), // -> 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. -> 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(), ) } // -> 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()"),