Skip to content

Optional field types #2185

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
wants to merge 2 commits into
base: master
Choose a base branch
from
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions core/src/bytecode/ast/compat.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1042,6 +1042,7 @@ impl<'ast> FromAst<RecordRow<'ast>> for mline_type::RecordRow {
fn from_ast(rrow: &RecordRow<'ast>) -> Self {
mline_type::RecordRowF {
id: rrow.id,
opt: false,
typ: Box::new(rrow.typ.to_mainline()),
}
}
Expand Down
14 changes: 13 additions & 1 deletion core/src/bytecode/ast/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -271,7 +271,7 @@ pub struct Annotation<'ast> {
pub contracts: &'ast [Type<'ast>],
}

impl Annotation<'_> {
impl<'ast> Annotation<'ast> {
/// Returns a string representation of the contracts (without the static type annotation) as a
/// comma-separated list.
pub fn contracts_to_string(&self) -> Option<String> {
Expand All @@ -290,6 +290,18 @@ impl Annotation<'_> {
pub fn is_empty(&self) -> bool {
self.typ.is_none() && self.contracts.is_empty()
}

/// If this annotation represents a single type (and not a user-defined contract), return it.
///
/// This returns `Some(Number)` for either `| Number` or `: Number`, although it currently
/// returns `None` for `: Number | Number`. Should it?
pub fn simple_type(&self) -> Option<&Type<'ast>> {
match (&self.typ, self.contracts) {
(None, [ctr]) if !matches!(&ctr.typ, TypeF::Contract(_)) => Some(ctr),
(Some(ty), []) => Some(ty),
_ => None,
}
}
}

/// Specifies where something should be imported from.
Expand Down
41 changes: 39 additions & 2 deletions core/src/bytecode/typecheck/eq.rs
Original file line number Diff line number Diff line change
Expand Up @@ -373,6 +373,35 @@ where
}
}

impl<'ast, S, T> TypeEqBounded<'ast> for (S, T)
where
S: TypeEqBounded<'ast>,
T: TypeEqBounded<'ast>,
{
fn type_eq_bounded(
&self,
other: &Self,
state: &mut State,
env1: &TermEnv<'ast>,
env2: &TermEnv<'ast>,
) -> bool {
self.0.type_eq_bounded(&other.0, state, env1, env2)
&& self.1.type_eq_bounded(&other.1, state, env1, env2)
}
}

impl<'ast> TypeEqBounded<'ast> for bool {
fn type_eq_bounded(
&self,
other: &Self,
_state: &mut State,
_env1: &TermEnv<'ast>,
_env2: &TermEnv<'ast>,
) -> bool {
*self == *other
}
}

impl<'ast> TypeEqBounded<'ast> for UnifEnumRows<'ast> {
fn type_eq_bounded(
&self,
Expand Down Expand Up @@ -416,15 +445,23 @@ impl<'ast> TypeEqBounded<'ast> for UnifRecordRows<'ast> {
let map_self: Option<IndexMap<LocIdent, _>> = self
.iter()
.map(|item| match item {
RecordRowsElt::Row(RecordRowF { id, typ: types }) => Some((id, types)),
RecordRowsElt::Row(RecordRowF {
id,
opt,
typ: types,
}) => Some((id, (opt, types))),
_ => None,
})
.collect();

let map_other: Option<IndexMap<LocIdent, _>> = other
.iter()
.map(|item| match item {
RecordRowsElt::Row(RecordRowF { id, typ: types }) => Some((id, types)),
RecordRowsElt::Row(RecordRowF {
id,
opt,
typ: types,
}) => Some((id, (opt, types))),
_ => None,
})
.collect();
Expand Down
1 change: 1 addition & 0 deletions core/src/bytecode/typecheck/mk_uniftype.rs
Original file line number Diff line number Diff line change
Expand Up @@ -77,6 +77,7 @@ macro_rules! mk_buty_record_row {
$crate::typ::RecordRowsF::Extend {
row: $crate::typ::RecordRowF {
id: $crate::identifier::LocIdent::from($id),
opt: false,
typ: Box::new($ty.into()),
},
tail: Box::new($crate::mk_buty_record_row!($(($ids, $tys)),* $(; $tail)?)),
Expand Down
4 changes: 3 additions & 1 deletion core/src/bytecode/typecheck/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -335,7 +335,7 @@ impl VarLevelUpperBound for UnifRecordRowsUnr<'_> {
// A var that hasn't be instantiated yet isn't a unification variable
RecordRowsF::Empty | RecordRowsF::TailVar(_) | RecordRowsF::TailDyn => VarLevel::NO_VAR,
RecordRowsF::Extend {
row: RecordRowF { id: _, typ },
row: RecordRowF { id: _, opt: _, typ },
tail,
} => max(tail.var_level_upper_bound(), typ.var_level_upper_bound()),
}
Expand Down Expand Up @@ -1155,6 +1155,7 @@ impl<'a, 'ast> Iterator for RecordRowsIterator<'a, UnifType<'ast>, UnifRecordRow
self.rrows = Some(tail);
Some(RecordRowsElt::Row(RecordRowF {
id: row.id,
opt: row.opt,
typ: row.typ.as_ref(),
}))
}
Expand Down Expand Up @@ -3072,6 +3073,7 @@ pub fn infer_record_type<'ast>(
RecordRowsF::Extend {
row: UnifRecordRow {
id,
opt: false,
typ: Box::new(uty),
},
tail: Box::new(rtype.into()),
Expand Down
1 change: 1 addition & 0 deletions core/src/bytecode/typecheck/pattern.rs
Original file line number Diff line number Diff line change
Expand Up @@ -492,6 +492,7 @@ impl<'ast> PatternTypes<'ast> for FieldPattern<'ast> {

Ok(UnifRecordRow {
id: self.matched_id,
opt: false,
typ: Box::new(ty_row),
})
}
Expand Down
1 change: 1 addition & 0 deletions core/src/bytecode/typecheck/reporting.rs
Original file line number Diff line number Diff line change
Expand Up @@ -263,6 +263,7 @@ impl<'ast> ToType<'ast> for UnifRecordRow<'ast> {
) -> Self::Target {
RecordRow {
id: self.id,
opt: self.opt,
typ: alloc.alloc(self.typ.to_type(alloc, reg, table)),
}
}
Expand Down
1 change: 1 addition & 0 deletions core/src/bytecode/typecheck/unif.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1734,6 +1734,7 @@ impl<'ast> RemoveRow<'ast> for UnifRecordRows<'ast> {

let row_to_insert = UnifRecordRow {
id: *target,
opt: false,
typ: Box::new(target_content.clone()),
};

Expand Down
10 changes: 5 additions & 5 deletions core/src/eval/contract_eq.rs
Original file line number Diff line number Diff line change
Expand Up @@ -348,11 +348,11 @@ where
///
/// Require the rows to be closed (i.e. the last element must be `RowEmpty`), otherwise `None` is
/// returned. `None` is returned as well if a type encountered is not row, or if it is a enum row.
fn rrows_as_map(erows: &RecordRows) -> Option<IndexMap<LocIdent, &Type>> {
fn rrows_as_map(erows: &RecordRows) -> Option<IndexMap<LocIdent, (bool, &Type)>> {
let map: Option<IndexMap<LocIdent, _>> = erows
.iter()
.map(|item| match item {
RecordRowsIteratorItem::Row(RecordRowF { id, typ }) => Some((id, typ)),
RecordRowsIteratorItem::Row(RecordRowF { id, opt, typ }) => Some((id, (opt, typ))),
_ => None,
})
.collect();
Expand Down Expand Up @@ -493,12 +493,12 @@ fn type_eq_bounded(
(TypeF::Record(uty1), TypeF::Record(uty2)) => {
fn type_eq_bounded_wrapper(
state: &mut State,
uty1: &&Type,
(opt1, uty1): &(bool, &Type),
env1: &Environment,
uty2: &&Type,
(opt2, uty2): &(bool, &Type),
env2: &Environment,
) -> bool {
type_eq_bounded(state, uty1, env1, uty2, env2)
opt1 == opt2 && type_eq_bounded(state, uty1, env1, uty2, env2)
}

let map1 = rrows_as_map(uty1);
Expand Down
9 changes: 8 additions & 1 deletion core/src/eval/operation.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3026,11 +3026,18 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
};

let split::SplitResult {
left,
mut left,
center,
right,
} = split::split(record1.fields, record2.fields);

// This doesn't seem very... principled. But at least it's sort of reasonable
// current usages of %record/split_pair%? $record_type wants this behavior
// because the contract is on the left and we allow optional fields to be
// ignored. The other user is std.contract.Equal, and ignoring of optionals
// means that `{ } | std.contract.Equal { foo | optional = 1 }` will succeed.
left.retain(|_name, value| !value.metadata.opt);

let left_only = Term::Record(RecordData {
fields: left,
sealed_tail: record1.sealed_tail,
Expand Down
6 changes: 5 additions & 1 deletion core/src/label.rs
Original file line number Diff line number Diff line change
Expand Up @@ -177,7 +177,11 @@ pub mod ty_path {
(TypeF::Record(rows), next @ Some(Elem::Field(ident))) => {
for row_item in rows.iter() {
match row_item {
RecordRowsIteratorItem::Row(RecordRowF { id, typ: ty }) if id == *ident => {
RecordRowsIteratorItem::Row(RecordRowF {
id,
typ: ty,
opt: _,
}) if id == *ident => {
let path_span = span(path_it, ty)?;

return Some(PathSpan {
Expand Down
42 changes: 21 additions & 21 deletions core/src/parser/uniterm.rs
Original file line number Diff line number Diff line change
Expand Up @@ -198,7 +198,7 @@ where
}

/// A record in the `UniTerm` syntax.
#[derive(Clone)]
#[derive(Clone, Debug)]
pub struct UniRecord<'ast> {
pub fields: Vec<FieldDef<'ast>>,
pub tail: Option<(RecordRows<'ast>, TermPos)>,
Expand Down Expand Up @@ -334,17 +334,13 @@ impl<'ast> UniRecord<'ast> {
metadata:
FieldMetadata {
doc: None,
annotation:
Annotation {
typ: Some(_),
contracts,
},
opt: false,
annotation,
opt: _,
not_exported: false,
priority: MergePriority::Neutral,
},
..
} if contracts.is_empty())
} if annotation.simple_type().is_some())
})
}

Expand All @@ -370,23 +366,26 @@ impl<'ast> UniRecord<'ast> {
metadata:
FieldMetadata {
doc: None,
annotation:
Annotation {
typ: Some(typ),
contracts: [],
},
opt: false,
annotation,
opt,
not_exported: false,
priority: MergePriority::Neutral,
},
pos: _,
} => Ok(RecordRows(RecordRowsF::Extend {
row: RecordRow {
id,
typ: alloc.type_data(typ.typ, typ.pos),
},
tail: alloc.record_rows(tail.0),
})),
} => match annotation.simple_type() {
Some(typ) => Ok(RecordRows(RecordRowsF::Extend {
row: RecordRow {
id,
opt,
typ: alloc.type_data(typ.typ.clone(), typ.pos),
},
tail: alloc.record_rows(tail.0),
})),
None => Err(InvalidRecordTypeError::InvalidField(
// Position of identifiers must always be set at this stage (parsing)
id.pos.fuse(field_def.pos).unwrap(),
)),
},
_ => {
Err(InvalidRecordTypeError::InvalidField(
// Position of identifiers must always be set at this stage (parsing)
Expand Down Expand Up @@ -943,6 +942,7 @@ impl<'ast> FixTypeVars<'ast> for RecordRow<'ast> {
.fix_type_vars_env(alloc, bound_vars, span)?
.map(|typ| RecordRow {
id: self.id,
opt: self.opt,
typ: alloc.alloc(typ),
}))
}
Expand Down
3 changes: 2 additions & 1 deletion core/src/pretty.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1218,7 +1218,8 @@ where
docs![
allocator,
ident_quoted(&self.id),
" : ",
// FIXME: we don't actually have a surface syntax for optional fields in types
if self.opt { " ?: " } else { " : " },
allocator.type_part(self.typ.deref()),
]
}
Expand Down
Loading
Loading