From 9744f48ccb72abc628c4cb0aaf48675476ad083e Mon Sep 17 00:00:00 2001 From: Brendan Zabarauskas Date: Sat, 1 Dec 2018 21:05:40 +1100 Subject: [PATCH] Remove scopes from record introductions --- crates/pikelet-concrete/src/desugar.rs | 20 ++----- crates/pikelet-concrete/src/elaborate/mod.rs | 43 ++++++-------- crates/pikelet-concrete/src/resugar.rs | 15 ++--- crates/pikelet-concrete/src/syntax/raw.rs | 28 ++++----- crates/pikelet-concrete/tests/resugar.rs | 4 +- crates/pikelet-core/src/nbe.rs | 27 +++------ crates/pikelet-core/src/syntax/core.rs | 60 +++++++------------- crates/pikelet-core/src/syntax/domain.rs | 12 +++- 8 files changed, 80 insertions(+), 129 deletions(-) diff --git a/crates/pikelet-concrete/src/desugar.rs b/crates/pikelet-concrete/src/desugar.rs index ce3e3051c..9887a320d 100644 --- a/crates/pikelet-concrete/src/desugar.rs +++ b/crates/pikelet-concrete/src/desugar.rs @@ -391,8 +391,6 @@ fn desugar_record_intro( ) -> Result { use syntax::concrete::RecordIntroField; - let mut env = env.clone(); - let fields = fields .iter() .map(|field| match field { @@ -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::, _>>()?; - Ok(raw::RcTerm::from(raw::Term::RecordIntro( - span, - Scope::new(Nest::new(fields), ()), - ))) + Ok(raw::RcTerm::from(raw::Term::RecordIntro(span, fields))) } impl Desugar for concrete::Literal { diff --git a/crates/pikelet-concrete/src/elaborate/mod.rs b/crates/pikelet-concrete/src/elaborate/mod.rs index 60f7a73f7..899632bfd 100644 --- a/crates/pikelet-concrete/src/elaborate/mod.rs +++ b/crates/pikelet-concrete/src/elaborate/mod.rs @@ -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::>()?; - - Nest::new(fields) + .collect::>()? }; - 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), _) => { @@ -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), ()))), )) }, diff --git a/crates/pikelet-concrete/src/resugar.rs b/crates/pikelet-concrete/src/resugar.rs index 5362caecb..b3aedd3c7 100644 --- a/crates/pikelet-concrete/src/resugar.rs +++ b/crates/pikelet-concrete/src/resugar.rs @@ -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)] @@ -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, diff --git a/crates/pikelet-concrete/src/syntax/raw.rs b/crates/pikelet-concrete/src/syntax/raw.rs index c65630443..0210a8f59 100644 --- a/crates/pikelet-concrete/src/syntax/raw.rs +++ b/crates/pikelet-concrete/src/syntax/raw.rs @@ -159,10 +159,7 @@ pub enum Term { Scope, Embed)>, ()>, ), /// Record introductions - RecordIntro( - ByteSpan, - Scope, Embed)>, ()>, - ), + RecordIntro(ByteSpan, Vec<(Label, RcTerm)>), /// Record field projection RecordProj(ByteSpan, RcTerm, ByteSpan, Label, LevelShift), /// Case expressions @@ -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()) diff --git a/crates/pikelet-concrete/tests/resugar.rs b/crates/pikelet-concrete/tests/resugar.rs index 1d5209718..80eef6279 100644 --- a/crates/pikelet-concrete/tests/resugar.rs +++ b/crates/pikelet-concrete/tests/resugar.rs @@ -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( @@ -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); diff --git a/crates/pikelet-core/src/nbe.rs b/crates/pikelet-core/src/nbe.rs index c3a9ab51b..f586419ee 100644 --- a/crates/pikelet-core/src/nbe.rs +++ b/crates/pikelet-core/src/nbe.rs @@ -160,19 +160,13 @@ pub fn nf_term(env: &dyn Env, term: &RcTerm) -> Result { }, // 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::>()?, - ); + Term::RecordIntro(ref fields) => { + let fields = fields + .iter() + .map(|&(ref label, ref term)| Ok((label.clone(), nf_term(env, &term)?))) + .collect::>()?; - Ok(RcValue::from(Value::RecordIntro(Scope::new(fields, ())))) + Ok(RcValue::from(Value::RecordIntro(fields))) }, // E-PROJ @@ -184,12 +178,9 @@ pub fn nf_term(env: &dyn Env, term: &RcTerm) -> Result { 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()); } } diff --git a/crates/pikelet-core/src/syntax/core.rs b/crates/pikelet-core/src/syntax/core.rs index 26bffd2c0..a6d7eb582 100644 --- a/crates/pikelet-core/src/syntax/core.rs +++ b/crates/pikelet-core/src/syntax/core.rs @@ -147,7 +147,7 @@ pub enum Term { /// Dependent record types RecordType(Scope, Embed)>, ()>), /// Record introductions - RecordIntro(Scope, Embed)>, ()>), + RecordIntro(Vec<(Label, RcTerm)>), /// Record field projection RecordProj(RcTerm, Label, LevelShift), /// Case expressions @@ -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()) @@ -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) => { @@ -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), @@ -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()) diff --git a/crates/pikelet-core/src/syntax/domain.rs b/crates/pikelet-core/src/syntax/domain.rs index 6ae026152..580a88065 100644 --- a/crates/pikelet-core/src/syntax/domain.rs +++ b/crates/pikelet-core/src/syntax/domain.rs @@ -25,7 +25,7 @@ pub enum Value { /// Dependent record types RecordType(Scope, Embed)>, ()>), /// Dependent record introductions - RecordIntro(Scope, Embed)>, ()>), + RecordIntro(Vec<(Label, RcValue)>), /// Array literals ArrayIntro(Vec), /// Neutral terms @@ -70,11 +70,12 @@ impl Value { Value::FunType(ref scope) | Value::FunIntro(ref scope) => { (scope.unsafe_pattern.1).0.is_nf() && scope.unsafe_body.is_nf() }, - Value::RecordType(ref scope) | Value::RecordIntro(ref scope) => scope + Value::RecordType(ref scope) => scope .unsafe_pattern .unsafe_patterns .iter() .all(|(_, _, Embed(ref term))| term.is_nf()), + Value::RecordIntro(ref fields) => fields.iter().all(|&(_, ref term)| term.is_nf()), Value::ArrayIntro(ref elems) => elems.iter().all(|elem| elem.is_nf()), Value::Neutral(_, _) => false, } @@ -112,11 +113,16 @@ impl RcValue { (scope.unsafe_pattern.1).0.shift_universes(shift); scope.unsafe_body.shift_universes(shift); }, - Value::RecordType(ref mut scope) | Value::RecordIntro(ref mut scope) => { + Value::RecordType(ref mut scope) => { for &mut (_, _, Embed(ref mut term)) in &mut scope.unsafe_pattern.unsafe_patterns { term.shift_universes(shift); } }, + Value::RecordIntro(ref mut fields) => { + for &mut (_, ref mut term) in fields { + term.shift_universes(shift); + } + }, Value::ArrayIntro(ref mut elems) => { for elem in elems { elem.shift_universes(shift);