Skip to content

Commit

Permalink
Remove scopes from record introductions
Browse files Browse the repository at this point in the history
  • Loading branch information
@brendanzab
brendanzab committed Dec 1, 2018
1 parent 8c9f801 commit 9744f48
Show file tree
Hide file tree
Showing 8 changed files with 80 additions and 129 deletions.
20 changes: 6 additions & 14 deletions crates/pikelet-concrete/src/desugar.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -391,8 +391,6 @@ fn desugar_record_intro(
) -> Result<raw::RcTerm, DesugarError> {
use syntax::concrete::RecordIntroField;

let mut env = env.clone();

let fields = fields
.iter()
.map(|field| match field {
Expand All @@ -401,27 +399,21 @@ fn desugar_record_intro(
shift,
} => {
let var = env.on_name(span, name, shift.unwrap_or(0));
let free_var = env.on_binding(name);
Ok((Label(name.clone()), Binder(free_var), Embed(var)))
Ok((Label(name.clone()), var))
},
RecordIntroField::Explicit {
label: (_, ref name),
ref params,
ref return_ann,
ref term,
} => {
let expr =
desugar_fun_intro(&env, params, return_ann.as_ref().map(<_>::as_ref), term)?;
let free_var = env.on_binding(name);
Ok((Label(name.clone()), Binder(free_var), Embed(expr)))
},
} => Ok((
Label(name.clone()),
desugar_fun_intro(env, params, return_ann.as_ref().map(<_>::as_ref), term)?,
)),
})
.collect::<Result<Vec<_>, _>>()?;

Ok(raw::RcTerm::from(raw::Term::RecordIntro(
span,
Scope::new(Nest::new(fields), ()),
)))
Ok(raw::RcTerm::from(raw::Term::RecordIntro(span, fields)))
}

impl Desugar<raw::Literal> for concrete::Literal {
Expand Down
43 changes: 18 additions & 25 deletions crates/pikelet-concrete/src/elaborate/mod.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -266,52 +266,47 @@ pub fn check_term(
},

// C-RECORD
(&raw::Term::RecordIntro(span, ref raw_scope), &Value::RecordType(ref raw_ty_scope)) => {
let (raw_fields, (), raw_ty_fields, ()) = {
// Until Scope::unbind2 returns a Result.
let found_size = raw_scope.unsafe_pattern.binders().len();
(&raw::Term::RecordIntro(span, ref raw_fields), &Value::RecordType(ref raw_ty_scope)) => {
let (raw_ty_fields, ()) = {
let expected_size = raw_ty_scope.unsafe_pattern.binders().len();
if found_size == expected_size {
Scope::unbind2(raw_scope.clone(), raw_ty_scope.clone())
if raw_fields.len() == raw_ty_scope.unsafe_pattern.binders().len() {
raw_ty_scope.clone().unbind()
} else {
return Err(TypeError::RecordSizeMismatch {
span,
found_size: found_size as u64,
found_size: raw_fields.len() as u64,
expected_size: expected_size as u64,
});
}
};

let raw_fields = raw_fields.unnest();
let raw_ty_fields = raw_ty_fields.unnest();

// FIXME: Check that record is well-formed?
let fields = {
let mut mappings = Vec::with_capacity(raw_fields.len());
let fields = <_>::zip(raw_fields.into_iter(), raw_ty_fields.into_iter())
<_>::zip(raw_fields.iter(), raw_ty_fields.into_iter())
.map(|(field, ty_field)| {
let (label, Binder(free_var), Embed(raw_expr)) = field;
let &(ref label, ref raw_expr) = field;
let (ty_label, Binder(ty_free_var), Embed(ann)) = ty_field;

if label == ty_label {
if *label == ty_label {
let ann = nbe::nf_term(context, &ann.substs(&mappings))?;
let expr = check_term(context, &raw_expr, &ann)?;
mappings.push((ty_free_var, expr.clone()));
Ok((label, Binder(free_var), Embed(expr)))
Ok((label.clone(), expr))
} else {
Err(TypeError::LabelMismatch {
span,
found: label,
found: label.clone(),
expected: ty_label,
})
}
})
.collect::<Result<_, _>>()?;

Nest::new(fields)
.collect::<Result<_, _>>()?
};

return Ok(RcTerm::from(Term::RecordIntro(Scope::new(fields, ()))));
return Ok(RcTerm::from(Term::RecordIntro(fields)));
},

(&raw::Term::Case(_, ref raw_head, ref raw_clauses), _) => {
Expand Down Expand Up @@ -585,28 +580,26 @@ pub fn infer_term(
},

// I-RECORD, I-EMPTY-RECORD
raw::Term::RecordIntro(_, ref raw_scope) => {
let (raw_fields, ()) = raw_scope.clone().unbind();
let raw_fields = raw_fields.unnest();

raw::Term::RecordIntro(_, ref raw_fields) => {
let mut fields = Vec::with_capacity(raw_fields.len());
let mut ty_fields = Vec::with_capacity(raw_fields.len());

// FIXME: error on duplicate field names
{
let mut ty_mappings = Vec::with_capacity(raw_fields.len());
for (label, Binder(free_var), Embed(raw_term)) in raw_fields {
for &(ref label, ref raw_term) in raw_fields {
let free_var = FreeVar::fresh_named(label.0.clone());
let (term, term_ty) = infer_term(context, &raw_term)?;
let term_ty = nbe::nf_term(context, &term_ty.substs(&ty_mappings))?;

fields.push((label.clone(), Binder(free_var.clone()), Embed(term.clone())));
ty_fields.push((label, Binder(free_var.clone()), Embed(term_ty)));
fields.push((label.clone(), term.clone()));
ty_fields.push((label.clone(), Binder(free_var.clone()), Embed(term_ty)));
ty_mappings.push((free_var, term));
}
}

Ok((
RcTerm::from(Term::RecordIntro(Scope::new(Nest::new(fields), ()))),
RcTerm::from(Term::RecordIntro(fields)),
RcValue::from(Value::RecordType(Scope::new(Nest::new(ty_fields), ()))),
))
},
Expand Down
15 changes: 6 additions & 9 deletions crates/pikelet-concrete/src/resugar.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ use moniker::{Binder, BoundTerm, Embed, FreeVar, Nest, Scope, Var};
use pikelet_core::syntax::{core, domain};
use pikelet_core::syntax::{Label, Level, LevelShift};

use syntax::{concrete, IntFormat, FloatFormat};
use syntax::{concrete, FloatFormat, IntFormat};

/// The environment used when resugaring from the core to the concrete syntax
#[derive(Debug, Clone)]
Expand Down Expand Up @@ -526,23 +526,20 @@ fn resugar_term(env: &ResugarEnv, term: &core::Term, prec: Prec) -> concrete::Te

concrete::Term::RecordType(ByteSpan::default(), fields)
},
core::Term::RecordIntro(ref scope) => {
core::Term::RecordIntro(ref fields) => {
let mut env = env.clone();
let (scope, ()) = scope.clone().unbind();

let fields = scope
.unnest()
.into_iter()
.map(|(label, binder, Embed(term))| {
let fields = fields
.iter()
.map(|&(ref label, ref term)| {
let (term_params, term_body) = match resugar_term(&env, &term, Prec::NO_WRAP) {
concrete::Term::FunIntro(_, params, term_body) => (params, *term_body),
term_body => (vec![], term_body),
};
let name = env.on_item(&label, &binder);

// TODO: use a punned label if possible?
concrete::RecordIntroField::Explicit {
label: (ByteIndex::default(), name),
label: (ByteIndex::default(), label.0.clone()),
params: term_params,
return_ann: None,
term: term_body,
Expand Down
28 changes: 10 additions & 18 deletions crates/pikelet-concrete/src/syntax/raw.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -159,10 +159,7 @@ pub enum Term {
Scope<Nest<(Label, Binder<String>, Embed<RcTerm>)>, ()>,
),
/// Record introductions
RecordIntro(
ByteSpan,
Scope<Nest<(Label, Binder<String>, Embed<RcTerm>)>, ()>,
),
RecordIntro(ByteSpan, Vec<(Label, RcTerm)>),
/// Record field projection
RecordProj(ByteSpan, RcTerm, ByteSpan, Label, LevelShift),
/// Case expressions
Expand Down Expand Up @@ -337,23 +334,18 @@ impl Term {
))
.append(Doc::space())
.append("}"),
Term::RecordIntro(_, ref scope) => Doc::nil()
Term::RecordIntro(_, ref fields) => Doc::nil()
.append("record {")
.append(Doc::space())
.append(Doc::intersperse(
scope.unsafe_pattern.unsafe_patterns.iter().map(
|&(ref label, ref binder, Embed(ref value))| {
Doc::nil()
.append(Doc::as_string(label))
.append("as")
.append(Doc::space())
.append(Doc::as_string(binder))
.append(Doc::space())
.append("=")
.append(Doc::space())
.append(value.to_doc())
},
),
fields.iter().map(|&(ref label, ref value)| {
Doc::nil()
.append(Doc::as_string(label))
.append(Doc::space())
.append("=")
.append(Doc::space())
.append(value.to_doc())
}),
Doc::text(";").append(Doc::space()),
))
.append(Doc::space())
Expand Down
4 changes: 2 additions & 2 deletions crates/pikelet-concrete/tests/resugar.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -187,7 +187,7 @@ fn let_shadow_keyword() {
)),
),
]),
core::RcTerm::from(core::Term::RecordIntro(Scope::new(Nest::new(vec![]), ()))),
core::RcTerm::from(core::Term::RecordIntro(vec![])),
));

let concrete_module = concrete::Term::Let(
Expand Down Expand Up @@ -282,7 +282,7 @@ fn record_ty() {

#[test]
fn record_empty() {
let core_term = core::Term::RecordIntro(Scope::new(Nest::new(vec![]), ()));
let core_term = core::Term::RecordIntro(vec![]);
let concrete_term = concrete::Term::RecordIntro(span(), vec![]);

assert_eq!(core_term.resugar(&ResugarEnv::new()), concrete_term);
Expand Down
27 changes: 9 additions & 18 deletions crates/pikelet-core/src/nbe.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -160,19 +160,13 @@ pub fn nf_term(env: &dyn Env, term: &RcTerm) -> Result<RcValue, NbeError> {
},

// E-RECORD, E-EMPTY-RECORD
Term::RecordIntro(ref scope) => {
let (fields, ()) = scope.clone().unbind();
let fields = Nest::new(
fields
.unnest()
.into_iter()
.map(|(label, binder, Embed(term))| {
Ok((label, binder, Embed(nf_term(env, &term)?)))
})
.collect::<Result<_, _>>()?,
);
Term::RecordIntro(ref fields) => {
let fields = fields
.iter()
.map(|&(ref label, ref term)| Ok((label.clone(), nf_term(env, &term)?)))
.collect::<Result<_, _>>()?;

Ok(RcValue::from(Value::RecordIntro(Scope::new(fields, ()))))
Ok(RcValue::from(Value::RecordIntro(fields)))
},

// E-PROJ
Expand All @@ -184,12 +178,9 @@ pub fn nf_term(env: &dyn Env, term: &RcTerm) -> Result<RcValue, NbeError> {
spine.clone(),
)));
},
Value::RecordIntro(ref scope) => {
let (fields, ()) = scope.clone().unbind();

// FIXME: mappings?
for (current_label, _, Embed(current_expr)) in fields.unnest() {
if current_label == *label {
Value::RecordIntro(ref fields) => {
for &(ref current_label, ref current_expr) in fields {
if current_label == label {
return Ok(current_expr.clone());
}
}
Expand Down
60 changes: 20 additions & 40 deletions crates/pikelet-core/src/syntax/core.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -147,7 +147,7 @@ pub enum Term {
/// Dependent record types
RecordType(Scope<Nest<(Label, Binder<String>, Embed<RcTerm>)>, ()>),
/// Record introductions
RecordIntro(Scope<Nest<(Label, Binder<String>, Embed<RcTerm>)>, ()>),
RecordIntro(Vec<(Label, RcTerm)>),
/// Record field projection
RecordProj(RcTerm, Label, LevelShift),
/// Case expressions
Expand Down Expand Up @@ -306,23 +306,18 @@ impl Term {
))
.append(Doc::space())
.append("}"),
Term::RecordIntro(ref scope) => Doc::nil()
Term::RecordIntro(ref fields) => Doc::nil()
.append("record {")
.append(Doc::space())
.append(Doc::intersperse(
scope.unsafe_pattern.unsafe_patterns.iter().map(
|&(ref label, ref binder, Embed(ref value))| {
Doc::nil()
.append(Doc::as_string(label))
.append("as")
.append(Doc::space())
.append(Doc::as_string(binder))
.append(Doc::space())
.append("=")
.append(Doc::space())
.append(value.to_doc())
},
),
fields.iter().map(|&(ref label, ref value)| {
Doc::nil()
.append(Doc::as_string(label))
.append(Doc::space())
.append("=")
.append(Doc::space())
.append(value.to_doc())
}),
Doc::text(";").append(Doc::space()),
))
.append(Doc::space())
Expand Down Expand Up @@ -395,9 +390,7 @@ impl RcTerm {
Term::FunApp(ref head, ref arg) => {
RcTerm::from(Term::FunApp(head.substs(mappings), arg.substs(mappings)))
},
Term::RecordType(ref scope) | Term::RecordIntro(ref scope)
if scope.unsafe_pattern.unsafe_patterns.is_empty() =>
{
Term::RecordType(ref scope) if scope.unsafe_pattern.unsafe_patterns.is_empty() => {
self.clone()
},
Term::RecordType(ref scope) => {
Expand All @@ -415,20 +408,14 @@ impl RcTerm {
unsafe_body: (),
}))
},
Term::RecordIntro(ref scope) => {
let unsafe_patterns = scope
.unsafe_pattern
.unsafe_patterns
Term::RecordIntro(ref fields) if fields.is_empty() => self.clone(),
Term::RecordIntro(ref fields) => {
let fields = fields
.iter()
.map(|&(ref label, ref binder, Embed(ref expr))| {
(label.clone(), binder.clone(), Embed(expr.substs(mappings)))
})
.map(|&(ref label, ref expr)| (label.clone(), expr.substs(mappings)))
.collect();

RcTerm::from(Term::RecordIntro(Scope {
unsafe_pattern: Nest { unsafe_patterns },
unsafe_body: (),
}))
RcTerm::from(Term::RecordIntro(fields))
},
Term::RecordProj(ref expr, ref label, shift) => RcTerm::from(Term::RecordProj(
expr.substs(mappings),
Expand Down Expand Up @@ -513,20 +500,13 @@ impl<'a> From<&'a Value> for Term {
unsafe_body: (),
})
},
Value::RecordIntro(ref scope) => {
let unsafe_patterns = scope
.unsafe_pattern
.unsafe_patterns
Value::RecordIntro(ref fields) => {
let fields = fields
.iter()
.map(|&(ref label, ref binder, Embed(ref expr))| {
(label.clone(), binder.clone(), Embed(RcTerm::from(&**expr)))
})
.map(|&(ref label, ref expr)| (label.clone(), RcTerm::from(&**expr)))
.collect();

Term::RecordIntro(Scope {
unsafe_pattern: Nest { unsafe_patterns },
unsafe_body: (),
})
Term::RecordIntro(fields)
},
Value::ArrayIntro(ref elems) => {
Term::ArrayIntro(elems.iter().map(|elem| RcTerm::from(&**elem)).collect())
Expand Down
Loading

0 comments on commit 9744f48

Please sign in to comment.