tweag/nickel
1
1
Fork 0
mirror of https://github.com/tweag/nickel.git synced 2024-09-20 08:05:15 +03:00
Code Issues Projects Releases Wiki Activity

Merge pull request #217 from tweag/feature/dyn-record-contracts

Browse Source 
Open record contracts
This commit is contained in:
Yann Hamdaoui 2020-12-09 10:53:47 +00:00 committed by GitHub
commit c35100e7f8
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
7 changed files with 109 additions and 17 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

33
src/error.rs
View File

@ -87,6 +87,12 @@ pub enum TypecheckError {
/* the inferred/annotated type */ Types,
Option<RawSpan>,
),
/// A dynamic tail was expected to be in the type of an expression, but was not.
MissingDynTail(
/* the expected type */ Types,
/* the inferred/annotated type */ Types,
Option<RawSpan>,
),
/// A specific row was not expected to be in the type of an expression.
ExtraRow(
Ident,
@ -94,6 +100,13 @@ pub enum TypecheckError {
/* the inferred/annotated type */ Types,
Option<RawSpan>,
),
/// A additional dynamic tail was not expected to be in the type of an expression.
ExtraDynTail(
/* the expected type */ Types,
/* the inferred/annotated type */ Types,
Option<RawSpan>,
),
/// An unbound type variable was referenced.
UnboundTypeVariable(Ident, Option<RawSpan>),
/// The actual (inferred or annotated) type of an expression is incompatible with its expected
@ -956,6 +969,16 @@ impl ToDiagnostic<FileId> for TypecheckError {
format!("The type of the expression was inferred to be `{}`, which does not contain the field `{}`", actual, ident),
])]
,
TypecheckError::MissingDynTail(expd, actual, span_opt) =>
vec![Diagnostic::error()
.with_message(String::from("Type error: missing dynamic tail `| Dyn`"))
.with_labels(mk_expr_label(span_opt))
.with_notes(vec![
format!("The type of the expression was expected to be `{}` which contains the tail `| Dyn`", expd),
format!("The type of the expression was inferred to be `{}`, which does not contain the tail `| Dyn`", actual),
])]
,
TypecheckError::ExtraRow(Ident(ident), expd, actual, span_opt) =>
vec![Diagnostic::error()
.with_message(format!("Type error: extra row `{}`", ident))
@ -965,6 +988,16 @@ impl ToDiagnostic<FileId> for TypecheckError {
format!("Tye type of the expression was inferred to be `{}`, which contains the extra field `{}`", actual, ident),
])]
,
TypecheckError::ExtraDynTail(expd, actual, span_opt) =>
vec![Diagnostic::error()
.with_message(String::from("Type error: extra dynamic tail `| Dyn`"))
.with_labels(mk_expr_label(span_opt))
.with_notes(vec![
format!("The type of the expression was expected to be `{}`, which does not contain the tail `| Dyn`", expd),
format!("Tye type of the expression was inferred to be `{}`, which contains the extra tail `| Dyn`", actual),
])]
,
TypecheckError::UnboundTypeVariable(Ident(ident), span_opt) =>
vec![Diagnostic::error()
.with_message(String::from("Unbound type variable"))

14
src/grammar.lalrpop
View File

@ -402,6 +402,11 @@ BaseType: Types = {
"List" => Types(AbsType::List()),
};
RowTail: Types = {
<Ident> => Types(AbsType::Var(<>)),
"Dyn" => Types(AbsType::Dyn()),
}
subType : Types = {
<BaseType>,
<Ident> => Types(AbsType::Var(<>)),
@ -428,7 +433,7 @@ subType : Types = {
},
"{" <rows:(<Ident> ":" <Types> ",")*>
<last:(<Ident> ":" <Types>)?>
<tail: ("|" <Ident>)?> "}" => {
<tail: ("|" <RowTail>)?> "}" => {
let ty = rows.into_iter()
.chain(last.into_iter())
// As we build row types as a linked list via a fold on the original
@ -437,12 +442,7 @@ subType : Types = {
// order for error reporting.
.rev()
.fold(
Types(
match tail {
Some(id) => AbsType::Var(id),
None => AbsType::RowEmpty(),
}
),
tail.unwrap_or(Types(AbsType::RowEmpty())),
|t, i_ty| {
let (i, ty) = i_ty;
Types(AbsType::RowExtend(i, Some(Box::new(ty)), Box::new(t)))

20
src/program.rs
View File

@ -1405,9 +1405,6 @@ Assume(#alwaysTrue -> #alwaysFalse, not ) true
.unwrap_err();
}
#[test]
fn records_contracts_dyn() {}
#[test]
fn records_contracts_poly() {
let id = "let f = Assume(forall a. { | a} -> { | a }, fun x => x) in f";
@ -1467,6 +1464,23 @@ Assume(#alwaysTrue -> #alwaysFalse, not ) true
.unwrap_err();
}
#[test]
fn records_contracts_dyn() {
assert_peq!(
"Assume({a: Num, b: Str | Dyn}, {a = 1; b = \"b\"})",
"{a = 1; b = \"b\"}"
);
assert_peq!(
"Assume({a: Num, b: Str | Dyn}, {a = 1; b = \"b\"; c = false})",
"{a = 1; b = \"b\"; c = false}"
);
assert_peq!(
"Assume({a: Num | Dyn} -> Dyn, fun r => r.b) {a = 1; b = 2}",
"2"
);
eval_string("Assume({a: Num, b: Str | Dyn}, {a = 1})").unwrap_err();
}
#[test]
fn multiline_string_indent() {
// /!\ Trailing spaces on the first line are on purpose, don't remove ! /!\

1
src/stdlib.rs
View File

@ -48,5 +48,6 @@ pub mod contracts {
generate_accessor!(dyn_record);
generate_accessor!(record_extend);
generate_accessor!(forall_tail);
generate_accessor!(dyn_tail);
generate_accessor!(empty_tail);
}

52
src/typecheck.rs
View File

@ -56,17 +56,21 @@ use std::collections::{HashMap, HashSet};
pub enum RowUnifError {
/// The LHS had a binding that was missing in the RHS.
MissingRow(Ident),
/// The LHS had a `Dyn` tail that was missing in the RHS.
MissingDynTail(),
/// The RHS had a binding that was not in the LHS.
ExtraRow(Ident),
/// The RHS had a additional `Dyn` tail.
ExtraDynTail(),
/// There were two incompatible definitions for the same row.
RowMismatch(Ident, UnifError),
/// Tried to unify an enum row and a record row.
RowKindMismatch(Ident, Option<TypeWrapper>, Option<TypeWrapper>),
/// One of the row was ill-formed (typically, a tail was neither a row nor a variable).
/// One of the row was ill-formed (typically, a tail was neither a row, a variable nor `Dyn`).
///
/// This should probably not happen with proper restrictions on the parser and a correct
/// typechecking algorithm. We let it as an error for now, but it could be removed and turned
/// into a panic! in the future.
/// typechecking algorithm. We let it as an error for now, but it could be removed in the
/// future.
IllformedRow(TypeWrapper),
/// A [row constraint](./type.RowConstr.html) was violated.
UnsatConstr(Ident, Option<TypeWrapper>),
@ -89,7 +93,9 @@ impl RowUnifError {
pub fn to_unif_err(self, left: TypeWrapper, right: TypeWrapper) -> UnifError {
match self {
RowUnifError::MissingRow(id) => UnifError::MissingRow(id, left, right),
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)
}
@ -117,8 +123,12 @@ pub enum UnifError {
ConstMismatch(usize, usize),
/// Tried to unify two rows, but an identifier of the LHS was absent from the RHS.
MissingRow(Ident, TypeWrapper, TypeWrapper),
/// Tried to unify two rows, but the `Dyn` tail of the RHS was absent from the LHS.
MissingDynTail(TypeWrapper, TypeWrapper),
/// Tried to unify two rows, but an identifier of the RHS was absent from the LHS.
ExtraRow(Ident, TypeWrapper, TypeWrapper),
/// Tried to unify two rows, but the `Dyn` tail of the RHS was absent from the LHS.
ExtraDynTail(TypeWrapper, TypeWrapper),
/// A row was ill-formed.
IllformedRow(TypeWrapper),
/// Tried to unify a unification variable with a row type violating the [row
@ -217,12 +227,23 @@ impl UnifError {
reporting::to_type(state, names, tyw2),
pos_opt,
),
UnifError::MissingDynTail(tyw1, tyw2) => TypecheckError::MissingDynTail(
reporting::to_type(state, names, tyw1),
reporting::to_type(state, names, tyw2),
pos_opt,
),
UnifError::ExtraRow(id, tyw1, tyw2) => TypecheckError::ExtraRow(
id,
reporting::to_type(state, names, tyw1),
reporting::to_type(state, names, tyw2),
pos_opt,
),
UnifError::ExtraDynTail(tyw1, tyw2) => TypecheckError::ExtraDynTail(
reporting::to_type(state, names, tyw1),
reporting::to_type(state, names, tyw2),
pos_opt,
),
UnifError::IllformedRow(tyw) => {
TypecheckError::IllformedType(reporting::to_type(state, names, tyw))
}
@ -546,7 +567,7 @@ fn type_check_(
};
if let TypeWrapper::Concrete(AbsType::DynRecord(rec_ty)) = root_ty.clone() {
// Checking for an dynamic record
// Checking for a dynamic record
stat_map
.into_iter()
.try_for_each(|(_, t)| -> Result<(), TypecheckError> {
@ -851,7 +872,9 @@ fn row_add(
r = get_root(state.table, p);
}
match r {
TypeWrapper::Concrete(AbsType::RowEmpty()) => Err(RowUnifError::MissingRow(id.clone())),
TypeWrapper::Concrete(AbsType::RowEmpty()) | TypeWrapper::Concrete(AbsType::Dyn()) => {
Err(RowUnifError::MissingRow(id.clone()))
}
TypeWrapper::Concrete(AbsType::RowExtend(id2, ty2, r2)) => {
if *id == id2 {
Ok((ty2, *r2))
@ -1036,8 +1059,12 @@ pub fn unify_rows(
t2: AbsType<Box<TypeWrapper>>,
) -> Result<(), RowUnifError> {
match (t1, t2) {
(AbsType::RowEmpty(), AbsType::RowEmpty()) => Ok(()),
(AbsType::RowEmpty(), AbsType::RowEmpty()) | (AbsType::Dyn(), AbsType::Dyn()) => Ok(()),
(AbsType::RowEmpty(), AbsType::Dyn()) => Err(RowUnifError::ExtraDynTail()),
(AbsType::Dyn(), AbsType::RowEmpty()) => Err(RowUnifError::MissingDynTail()),
(AbsType::RowEmpty(), AbsType::RowExtend(ident, _, _))
| (AbsType::Dyn(), AbsType::RowExtend(ident, _, _))
| (AbsType::RowExtend(ident, _, _), AbsType::Dyn())
| (AbsType::RowExtend(ident, _, _), AbsType::RowEmpty()) => {
Err(RowUnifError::ExtraRow(ident))
}
@ -2159,4 +2186,17 @@ mod tests {
);
assert_row_conflict(res);
}
#[test]
fn dynamic_row_tail() {
parse_and_typecheck("let r = Assume({a: Num | Dyn}, {a = 1; b = 2}) in Promise(Num, r.a)")
.unwrap();
parse_and_typecheck("Promise({a: Num | Dyn}, Assume({a: Num | Dyn}, {a = 1; b = 2}))")
.unwrap();
// Currently, typechecking is conservative wrt the dynamic row type, meaning it can
parse_and_typecheck("Promise({a: Num | Dyn}, {a = 1; b = 2})").unwrap_err();
parse_and_typecheck("Promise({a: Num | Dyn}, {a = 1})").unwrap_err();
parse_and_typecheck("Promise({a: Num}, Assume({a: Num | Dyn}, {a = 1}))").unwrap_err();
parse_and_typecheck("Promise({a: Num | Dyn}, {a = 1})").unwrap_err();
}
}

4
src/types.rs
View File

@ -137,7 +137,7 @@ impl<Ty> AbsType<Ty> {
/// Determine if a type is a row type.
pub fn is_row_type(&self) -> bool {
match self {
AbsType::RowExtend(_, _, _) | AbsType::RowEmpty() => true,
AbsType::RowExtend(_, _, _) | AbsType::RowEmpty() | AbsType::Dyn() => true,
_ => false,
}
}
@ -248,6 +248,7 @@ impl Types {
) -> RichTerm {
match &ty.0 {
AbsType::RowEmpty() => contracts::empty_tail(),
AbsType::Dyn() => contracts::dyn_tail(),
AbsType::Var(id) => {
let (_, rt) = h
.get(&id)
@ -350,6 +351,7 @@ impl fmt::Display for Types {
match tail.0 {
AbsType::RowEmpty() => write!(f, "{}", tail),
AbsType::Var(_) => write!(f, " | {}", tail),
AbsType::Dyn() => write!(f, " | Dyn"),
_ => write!(f, ", {}", tail),
}
}

2
stdlib/contracts.ncl
View File

@ -65,6 +65,8 @@
else
acc$[magic_fld = wrap sy t];
dyn_tail = fun acc l t => acc & t;
empty_tail = fun acc l t =>
if t == {} then acc
else blame (tag "extra field" l);