From 3f1d505f96055c4e822dc84b1590a8677631f9cf Mon Sep 17 00:00:00 2001 From: Brendan Zabarauskas Date: Fri, 30 Nov 2018 16:30:55 +1100 Subject: [PATCH 1/9] Move values to another module --- crates/pikelet-driver/src/lib.rs | 14 +- crates/pikelet-elaborate/src/context.rs | 3 +- crates/pikelet-elaborate/src/lib.rs | 3 +- crates/pikelet-elaborate/src/normalize.rs | 5 +- crates/pikelet-elaborate/tests/normalize.rs | 3 +- crates/pikelet-elaborate/tests/support/mod.rs | 3 +- crates/pikelet-syntax/src/core.rs | 249 +---------------- crates/pikelet-syntax/src/domain.rs | 258 ++++++++++++++++++ crates/pikelet-syntax/src/lib.rs | 1 + crates/pikelet-syntax/src/pretty/core.rs | 7 +- .../pikelet-syntax/src/translation/resugar.rs | 9 +- 11 files changed, 287 insertions(+), 268 deletions(-) create mode 100644 crates/pikelet-syntax/src/domain.rs diff --git a/crates/pikelet-driver/src/lib.rs b/crates/pikelet-driver/src/lib.rs index 6f10a7e0f..44a355db3 100644 --- a/crates/pikelet-driver/src/lib.rs +++ b/crates/pikelet-driver/src/lib.rs @@ -37,9 +37,9 @@ //! .---------------------------. //! | pikelet_syntax::raw::Term | //! '---------------------------' -//! | .-----------------------------. -//! pikelet_elaborate::{check,infer} <------------- | pikelet_syntax::core::Value | -//! | '-----------------------------' +//! | .-------------------------------. +//! pikelet_elaborate::{check,infer} <------------- | pikelet_syntax::domain::Value | +//! | '-------------------------------' //! v ^ //! .----------------------------. | //! | pikelet_syntax::core::Term | - pikelet_elaborate::normalize -' @@ -137,7 +137,7 @@ use std::sync::Arc; use pikelet_elaborate::{Context, Import}; use pikelet_syntax::translation::{Desugar, DesugarEnv, Resugar}; -use pikelet_syntax::{core, raw}; +use pikelet_syntax::{core, domain, raw}; /// An environment that keeps track of the state of a Pikelet program during /// compilation or interactive sessions @@ -211,7 +211,7 @@ impl Driver { &mut self, name: &str, raw_term: &raw::RcTerm, - ) -> Result<(core::RcTerm, core::RcType), Vec> { + ) -> Result<(core::RcTerm, domain::RcType), Vec> { let (term, inferred) = self.infer_term(&raw_term)?; let fv = self.desugar_env.on_binding(&name); @@ -225,11 +225,11 @@ impl Driver { pub fn infer_term( &self, raw_term: &raw::RcTerm, - ) -> Result<(core::RcTerm, core::RcType), Vec> { + ) -> Result<(core::RcTerm, domain::RcType), Vec> { pikelet_elaborate::infer_term(&self.context, &raw_term).map_err(|e| vec![e.to_diagnostic()]) } - pub fn nf_term(&self, term: &core::RcTerm) -> Result> { + pub fn nf_term(&self, term: &core::RcTerm) -> Result> { pikelet_elaborate::nf_term(&self.context, term).map_err(|e| vec![e.to_diagnostic()]) } diff --git a/crates/pikelet-elaborate/src/context.rs b/crates/pikelet-elaborate/src/context.rs index 9a1c2eb06..85ac0a936 100644 --- a/crates/pikelet-elaborate/src/context.rs +++ b/crates/pikelet-elaborate/src/context.rs @@ -3,7 +3,8 @@ use moniker::{Binder, FreeVar, Var}; use std::fmt; use std::rc::Rc; -use pikelet_syntax::core::{Literal, RcTerm, RcType, RcValue, Value}; +use pikelet_syntax::core::{Literal, RcTerm}; +use pikelet_syntax::domain::{RcType, RcValue, Value}; use pikelet_syntax::translation::{Resugar, ResugarEnv}; use pikelet_syntax::{FloatFormat, IntFormat}; diff --git a/crates/pikelet-elaborate/src/lib.rs b/crates/pikelet-elaborate/src/lib.rs index 31213ec0d..bd37380a3 100644 --- a/crates/pikelet-elaborate/src/lib.rs +++ b/crates/pikelet-elaborate/src/lib.rs @@ -15,7 +15,8 @@ extern crate pikelet_syntax; use codespan::ByteSpan; use moniker::{Binder, BoundPattern, BoundTerm, Embed, FreeVar, Nest, Scope, Var}; -use pikelet_syntax::core::{Literal, Pattern, RcPattern, RcTerm, RcType, RcValue, Term, Value}; +use pikelet_syntax::core::{Literal, Pattern, RcPattern, RcTerm, Term}; +use pikelet_syntax::domain::{RcType, RcValue, Value}; use pikelet_syntax::raw; use pikelet_syntax::Level; diff --git a/crates/pikelet-elaborate/src/normalize.rs b/crates/pikelet-elaborate/src/normalize.rs index 7abbb55ef..fca65dbce 100644 --- a/crates/pikelet-elaborate/src/normalize.rs +++ b/crates/pikelet-elaborate/src/normalize.rs @@ -1,8 +1,7 @@ use moniker::{Binder, Embed, FreeVar, Nest, Scope, Var}; -use pikelet_syntax::core::{ - Head, Neutral, Pattern, RcNeutral, RcPattern, RcTerm, RcValue, Term, Value, -}; +use pikelet_syntax::core::{Pattern, RcPattern, RcTerm, Term}; +use pikelet_syntax::domain::{Head, Neutral, RcNeutral, RcValue, Value}; use {Context, Import, InternalError}; diff --git a/crates/pikelet-elaborate/tests/normalize.rs b/crates/pikelet-elaborate/tests/normalize.rs index 1e205422d..37e0d2ab9 100644 --- a/crates/pikelet-elaborate/tests/normalize.rs +++ b/crates/pikelet-elaborate/tests/normalize.rs @@ -9,7 +9,8 @@ use codespan::CodeMap; use moniker::{Binder, Embed, FreeVar, Scope, Var}; use pikelet_elaborate::Context; -use pikelet_syntax::core::{Neutral, RcNeutral, RcTerm, RcValue, Term, Value}; +use pikelet_syntax::core::{RcTerm, Term}; +use pikelet_syntax::domain::{Neutral, RcNeutral, RcValue, Value}; mod support; diff --git a/crates/pikelet-elaborate/tests/support/mod.rs b/crates/pikelet-elaborate/tests/support/mod.rs index b5946fec2..47e0fef0a 100644 --- a/crates/pikelet-elaborate/tests/support/mod.rs +++ b/crates/pikelet-elaborate/tests/support/mod.rs @@ -6,7 +6,8 @@ use codespan_reporting::termcolor::{ColorChoice, StandardStream}; use pikelet_elaborate::{self, Context}; use pikelet_syntax::concrete; -use pikelet_syntax::core::{RcTerm, RcType, RcValue}; +use pikelet_syntax::core::RcTerm; +use pikelet_syntax::domain::{RcType, RcValue}; use pikelet_syntax::parse; use pikelet_syntax::translation::{Desugar, DesugarEnv}; diff --git a/crates/pikelet-syntax/src/core.rs b/crates/pikelet-syntax/src/core.rs index 1ce700c37..cd788325f 100644 --- a/crates/pikelet-syntax/src/core.rs +++ b/crates/pikelet-syntax/src/core.rs @@ -5,6 +5,7 @@ use std::fmt; use std::ops; use std::rc::Rc; +use domain::{Head, Neutral, Value}; use pretty::{self, ToDoc}; use {FloatFormat, IntFormat, Label, Level, LevelShift}; @@ -263,254 +264,6 @@ impl fmt::Display for RcTerm { } } -/// Values -/// -/// These are either in _normal form_ (they cannot be reduced further) or are -/// _neutral terms_ (there is a possibility of reducing further depending -/// on the bindings given in the context) -#[derive(Debug, Clone, PartialEq, BoundTerm)] -pub enum Value { - /// Universes - Universe(Level), - /// Literals - Literal(Literal), - /// Dependent function types - FunType(Scope<(Binder, Embed), RcValue>), - /// Function introductions - FunIntro(Scope<(Binder, Embed), RcValue>), - /// Dependent record types - RecordType(Scope, Embed)>, ()>), - /// Dependent record introductions - RecordIntro(Scope, Embed)>, ()>), - /// Array literals - ArrayIntro(Vec), - /// Neutral terms - /// - /// A term whose computation has stopped because of an attempt to compute an - /// application `Head`. - Neutral(RcNeutral, Spine), -} - -impl Value { - pub fn universe(level: impl Into) -> Value { - Value::Universe(level.into()) - } - - pub fn var(var: impl Into>, shift: impl Into) -> Value { - Value::Neutral(RcNeutral::from(Neutral::var(var, shift)), Spine::new()) - } - - pub fn substs(&self, mappings: &[(FreeVar, RcTerm)]) -> RcTerm { - // FIXME: This seems quite wasteful! - RcTerm::from(Term::from(self)).substs(mappings) - } - - /// Returns `true` if the value is in weak head normal form - pub fn is_whnf(&self) -> bool { - match *self { - Value::Universe(_) - | Value::Literal(_) - | Value::FunType(_) - | Value::FunIntro(_) - | Value::RecordType(_) - | Value::RecordIntro(_) - | Value::ArrayIntro(_) => true, - Value::Neutral(_, _) => false, - } - } - - /// Returns `true` if the value is in normal form (ie. it contains no neutral terms within it) - pub fn is_nf(&self) -> bool { - match *self { - Value::Universe(_) | Value::Literal(_) => true, - 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 - .unsafe_pattern - .unsafe_patterns - .iter() - .all(|(_, _, Embed(ref term))| term.is_nf()), - Value::ArrayIntro(ref elems) => elems.iter().all(|elem| elem.is_nf()), - Value::Neutral(_, _) => false, - } - } - - pub fn head_app(&self) -> Option<(&Head, &Spine)> { - if let Value::Neutral(ref neutral, ref spine) = *self { - if let Neutral::Head(ref head) = **neutral { - return Some((head, spine)); - } - } - None - } - - pub fn free_var_app(&self) -> Option<(&FreeVar, LevelShift, &[RcValue])> { - self.head_app().and_then(|(head, spine)| match *head { - Head::Var(Var::Free(ref free_var), shift) => Some((free_var, shift, &spine[..])), - Head::Import(_) | Head::Var(Var::Bound(_), _) => None, - }) - } -} - -impl fmt::Display for Value { - fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { - self.to_doc().group().render_fmt(pretty::FALLBACK_WIDTH, f) - } -} - -/// Reference counted values -#[derive(Debug, Clone, PartialEq, BoundTerm)] -pub struct RcValue { - pub inner: Rc, -} - -impl RcValue { - pub fn shift_universes(&mut self, shift: LevelShift) { - match *Rc::make_mut(&mut self.inner) { - Value::Universe(ref mut level) => *level += shift, - Value::Literal(_) => {}, - Value::FunType(ref mut scope) | Value::FunIntro(ref mut scope) => { - (scope.unsafe_pattern.1).0.shift_universes(shift); - scope.unsafe_body.shift_universes(shift); - }, - Value::RecordType(ref mut scope) | Value::RecordIntro(ref mut scope) => { - for &mut (_, _, Embed(ref mut term)) in &mut scope.unsafe_pattern.unsafe_patterns { - term.shift_universes(shift); - } - }, - Value::ArrayIntro(ref mut elems) => { - for elem in elems { - elem.shift_universes(shift); - } - }, - Value::Neutral(ref mut neutral, ref mut spine) => { - neutral.shift_universes(shift); - for arg in spine { - arg.shift_universes(shift); - } - }, - } - } -} - -impl From for RcValue { - fn from(src: Value) -> RcValue { - RcValue { - inner: Rc::new(src), - } - } -} - -impl ops::Deref for RcValue { - type Target = Value; - - fn deref(&self) -> &Value { - &self.inner - } -} - -impl fmt::Display for RcValue { - fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { - fmt::Display::fmt(&self.inner, f) - } -} - -/// The head of an application -#[derive(Debug, Clone, PartialEq, BoundTerm)] -pub enum Head { - /// Variables that have not yet been replaced with a definition - Var(Var, LevelShift), - /// Imported definitions - Import(String), - // TODO: Metavariables -} - -/// The spine of a neutral term -/// -/// These are arguments that are awaiting application -pub type Spine = Vec; - -/// Neutral values -/// -/// These might be able to be reduced further depending on the bindings in the -/// context -#[derive(Debug, Clone, PartialEq, BoundTerm)] -pub enum Neutral { - /// Head of an application - Head(Head), - /// Field projection - RecordProj(RcNeutral, Label, LevelShift), - /// Case expressions - Case(RcNeutral, Vec>), -} - -impl Neutral { - pub fn var(var: impl Into>, shift: impl Into) -> Neutral { - Neutral::Head(Head::Var(var.into(), shift.into())) - } -} - -impl fmt::Display for Neutral { - fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { - self.to_doc().group().render_fmt(pretty::FALLBACK_WIDTH, f) - } -} - -/// Reference counted neutral values -#[derive(Debug, Clone, PartialEq, BoundTerm)] -pub struct RcNeutral { - pub inner: Rc, -} - -impl RcNeutral { - pub fn shift_universes(&mut self, shift: LevelShift) { - match *Rc::make_mut(&mut self.inner) { - // Neutral::Head(Head::Var(_, ref mut head_shift)) => { - // *head_shift += shift; // NOTE: Not sure if this is correct! - // }, - Neutral::Head(Head::Var(_, _)) | Neutral::Head(Head::Import(_)) => {}, - Neutral::RecordProj(ref mut expr, _, _) => expr.shift_universes(shift), - Neutral::Case(ref mut expr, ref mut clauses) => { - expr.shift_universes(shift); - for clause in clauses { - // FIXME: implement shifting for patterns as well! - // clause.unsafe_pattern.shift_universes(shift); - clause.unsafe_body.shift_universes(shift); - } - }, - } - } -} - -impl From for RcNeutral { - fn from(src: Neutral) -> RcNeutral { - RcNeutral { - inner: Rc::new(src), - } - } -} - -impl ops::Deref for RcNeutral { - type Target = Neutral; - - fn deref(&self) -> &Neutral { - &self.inner - } -} - -/// Types are at the term level, so this is just an alias -pub type Type = Value; - -/// Types are at the term level, so this is just an alias -pub type RcType = RcValue; - -impl From for Value { - fn from(src: Neutral) -> Value { - Value::Neutral(RcNeutral::from(src), Spine::new()) - } -} - impl<'a> From<&'a Value> for Term { fn from(src: &'a Value) -> Term { // Bypassing `Scope::new` and `Scope::unbind` here should be fine diff --git a/crates/pikelet-syntax/src/domain.rs b/crates/pikelet-syntax/src/domain.rs new file mode 100644 index 000000000..947ebc6d2 --- /dev/null +++ b/crates/pikelet-syntax/src/domain.rs @@ -0,0 +1,258 @@ +//! The semantic domain of the language + +use moniker::{Binder, Embed, FreeVar, Nest, Scope, Var}; +use std::fmt; +use std::ops; +use std::rc::Rc; + +use core::{Literal, RcPattern, RcTerm, Term}; +use pretty::{self, ToDoc}; +use {Label, Level, LevelShift}; + +/// Values +/// +/// These are either in _normal form_ (they cannot be reduced further) or are +/// _neutral terms_ (there is a possibility of reducing further depending +/// on the bindings given in the context) +#[derive(Debug, Clone, PartialEq, BoundTerm)] +pub enum Value { + /// Universes + Universe(Level), + /// Literals + Literal(Literal), + /// Dependent function types + FunType(Scope<(Binder, Embed), RcValue>), + /// Function introductions + FunIntro(Scope<(Binder, Embed), RcValue>), + /// Dependent record types + RecordType(Scope, Embed)>, ()>), + /// Dependent record introductions + RecordIntro(Scope, Embed)>, ()>), + /// Array literals + ArrayIntro(Vec), + /// Neutral terms + /// + /// A term whose computation has stopped because of an attempt to compute an + /// application `Head`. + Neutral(RcNeutral, Spine), +} + +impl Value { + pub fn universe(level: impl Into) -> Value { + Value::Universe(level.into()) + } + + pub fn var(var: impl Into>, shift: impl Into) -> Value { + Value::Neutral(RcNeutral::from(Neutral::var(var, shift)), Spine::new()) + } + + pub fn substs(&self, mappings: &[(FreeVar, RcTerm)]) -> RcTerm { + // FIXME: This seems quite wasteful! + RcTerm::from(Term::from(self)).substs(mappings) + } + + /// Returns `true` if the value is in weak head normal form + pub fn is_whnf(&self) -> bool { + match *self { + Value::Universe(_) + | Value::Literal(_) + | Value::FunType(_) + | Value::FunIntro(_) + | Value::RecordType(_) + | Value::RecordIntro(_) + | Value::ArrayIntro(_) => true, + Value::Neutral(_, _) => false, + } + } + + /// Returns `true` if the value is in normal form (ie. it contains no neutral terms within it) + pub fn is_nf(&self) -> bool { + match *self { + Value::Universe(_) | Value::Literal(_) => true, + 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 + .unsafe_pattern + .unsafe_patterns + .iter() + .all(|(_, _, Embed(ref term))| term.is_nf()), + Value::ArrayIntro(ref elems) => elems.iter().all(|elem| elem.is_nf()), + Value::Neutral(_, _) => false, + } + } + + pub fn head_app(&self) -> Option<(&Head, &Spine)> { + if let Value::Neutral(ref neutral, ref spine) = *self { + if let Neutral::Head(ref head) = **neutral { + return Some((head, spine)); + } + } + None + } + + pub fn free_var_app(&self) -> Option<(&FreeVar, LevelShift, &[RcValue])> { + self.head_app().and_then(|(head, spine)| match *head { + Head::Var(Var::Free(ref free_var), shift) => Some((free_var, shift, &spine[..])), + Head::Import(_) | Head::Var(Var::Bound(_), _) => None, + }) + } +} + +impl fmt::Display for Value { + fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { + self.to_doc().group().render_fmt(pretty::FALLBACK_WIDTH, f) + } +} + +/// Reference counted values +#[derive(Debug, Clone, PartialEq, BoundTerm)] +pub struct RcValue { + pub inner: Rc, +} + +impl RcValue { + pub fn shift_universes(&mut self, shift: LevelShift) { + match *Rc::make_mut(&mut self.inner) { + Value::Universe(ref mut level) => *level += shift, + Value::Literal(_) => {}, + Value::FunType(ref mut scope) | Value::FunIntro(ref mut scope) => { + (scope.unsafe_pattern.1).0.shift_universes(shift); + scope.unsafe_body.shift_universes(shift); + }, + Value::RecordType(ref mut scope) | Value::RecordIntro(ref mut scope) => { + for &mut (_, _, Embed(ref mut term)) in &mut scope.unsafe_pattern.unsafe_patterns { + term.shift_universes(shift); + } + }, + Value::ArrayIntro(ref mut elems) => { + for elem in elems { + elem.shift_universes(shift); + } + }, + Value::Neutral(ref mut neutral, ref mut spine) => { + neutral.shift_universes(shift); + for arg in spine { + arg.shift_universes(shift); + } + }, + } + } +} + +impl From for RcValue { + fn from(src: Value) -> RcValue { + RcValue { + inner: Rc::new(src), + } + } +} + +impl ops::Deref for RcValue { + type Target = Value; + + fn deref(&self) -> &Value { + &self.inner + } +} + +impl fmt::Display for RcValue { + fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { + fmt::Display::fmt(&self.inner, f) + } +} + +/// The head of an application +#[derive(Debug, Clone, PartialEq, BoundTerm)] +pub enum Head { + /// Variables that have not yet been replaced with a definition + Var(Var, LevelShift), + /// Imported definitions + Import(String), + // TODO: Metavariables +} + +/// The spine of a neutral term +/// +/// These are arguments that are awaiting application +pub type Spine = Vec; + +/// Neutral values +/// +/// These might be able to be reduced further depending on the bindings in the +/// context +#[derive(Debug, Clone, PartialEq, BoundTerm)] +pub enum Neutral { + /// Head of an application + Head(Head), + /// Field projection + RecordProj(RcNeutral, Label, LevelShift), + /// Case expressions + Case(RcNeutral, Vec>), +} + +impl Neutral { + pub fn var(var: impl Into>, shift: impl Into) -> Neutral { + Neutral::Head(Head::Var(var.into(), shift.into())) + } +} + +impl fmt::Display for Neutral { + fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { + self.to_doc().group().render_fmt(pretty::FALLBACK_WIDTH, f) + } +} + +/// Reference counted neutral values +#[derive(Debug, Clone, PartialEq, BoundTerm)] +pub struct RcNeutral { + pub inner: Rc, +} + +impl RcNeutral { + pub fn shift_universes(&mut self, shift: LevelShift) { + match *Rc::make_mut(&mut self.inner) { + // Neutral::Head(Head::Var(_, ref mut head_shift)) => { + // *head_shift += shift; // NOTE: Not sure if this is correct! + // }, + Neutral::Head(Head::Var(_, _)) | Neutral::Head(Head::Import(_)) => {}, + Neutral::RecordProj(ref mut expr, _, _) => expr.shift_universes(shift), + Neutral::Case(ref mut expr, ref mut clauses) => { + expr.shift_universes(shift); + for clause in clauses { + // FIXME: implement shifting for patterns as well! + // clause.unsafe_pattern.shift_universes(shift); + clause.unsafe_body.shift_universes(shift); + } + }, + } + } +} + +impl From for RcNeutral { + fn from(src: Neutral) -> RcNeutral { + RcNeutral { + inner: Rc::new(src), + } + } +} + +impl ops::Deref for RcNeutral { + type Target = Neutral; + + fn deref(&self) -> &Neutral { + &self.inner + } +} + +/// Types are at the term level, so this is just an alias +pub type Type = Value; + +/// Types are at the term level, so this is just an alias +pub type RcType = RcValue; + +impl From for Value { + fn from(src: Neutral) -> Value { + Value::Neutral(RcNeutral::from(src), Spine::new()) + } +} diff --git a/crates/pikelet-syntax/src/lib.rs b/crates/pikelet-syntax/src/lib.rs index fd7d3f89a..6c0e93599 100644 --- a/crates/pikelet-syntax/src/lib.rs +++ b/crates/pikelet-syntax/src/lib.rs @@ -19,6 +19,7 @@ use std::ops::{Add, AddAssign}; pub mod concrete; pub mod core; +pub mod domain; pub mod parse; pub mod pretty; pub mod raw; diff --git a/crates/pikelet-syntax/src/pretty/core.rs b/crates/pikelet-syntax/src/pretty/core.rs index 05d725c35..0fc929069 100644 --- a/crates/pikelet-syntax/src/pretty/core.rs +++ b/crates/pikelet-syntax/src/pretty/core.rs @@ -4,7 +4,8 @@ use super::pretty::Doc; use moniker::{Binder, Embed, Var}; use std::iter; -use core::{Head, Literal, Neutral, Pattern, Term, Value}; +use core::{Literal, Pattern, Term}; +use domain::{Head, Neutral, Value}; use raw; use {FloatFormat, IntFormat, Label, Level, LevelShift}; @@ -308,7 +309,9 @@ impl ToDoc for Term { }, ), )), - Term::RecordProj(ref expr, ref label, shift) => pretty_record_proj(&expr.inner, label, shift), + Term::RecordProj(ref expr, ref label, shift) => { + pretty_record_proj(&expr.inner, label, shift) + }, Term::Case(ref head, ref clauses) => pretty_case( &head.inner, clauses diff --git a/crates/pikelet-syntax/src/translation/resugar.rs b/crates/pikelet-syntax/src/translation/resugar.rs index 855ea05c2..2aadcca70 100644 --- a/crates/pikelet-syntax/src/translation/resugar.rs +++ b/crates/pikelet-syntax/src/translation/resugar.rs @@ -4,6 +4,7 @@ use moniker::{Binder, BoundTerm, Embed, FreeVar, Nest, Scope, Var}; use concrete; use core; +use domain; use {Label, Level, LevelShift}; /// The environment used when resugaring from the core to the concrete syntax @@ -598,14 +599,14 @@ impl Resugar for core::Term { } } -impl Resugar for core::Value { +impl Resugar for domain::Value { fn resugar(&self, env: &ResugarEnv) -> concrete::Term { // FIXME: Make this more efficient? resugar_term(env, &core::Term::from(self), Prec::NO_WRAP) } } -impl Resugar for core::Neutral { +impl Resugar for domain::Neutral { fn resugar(&self, env: &ResugarEnv) -> concrete::Term { // FIXME: Make this more efficient? resugar_term(env, &core::Term::from(self), Prec::NO_WRAP) @@ -618,13 +619,13 @@ impl Resugar for core::RcTerm { } } -impl Resugar for core::RcValue { +impl Resugar for domain::RcValue { fn resugar(&self, env: &ResugarEnv) -> concrete::Term { self.inner.resugar(env) } } -impl Resugar for core::RcNeutral { +impl Resugar for domain::RcNeutral { fn resugar(&self, env: &ResugarEnv) -> concrete::Term { self.inner.resugar(env) } From 7e341e20544f8008dd806fdafaa464711404abcf Mon Sep 17 00:00:00 2001 From: Brendan Zabarauskas Date: Fri, 30 Nov 2018 16:49:08 +1100 Subject: [PATCH 2/9] Remove domain formatting --- crates/pikelet-elaborate/tests/infer.rs | 6 +- crates/pikelet-syntax/src/domain.rs | 20 ------ crates/pikelet-syntax/src/pretty/core.rs | 80 ------------------------ 3 files changed, 3 insertions(+), 103 deletions(-) diff --git a/crates/pikelet-elaborate/tests/infer.rs b/crates/pikelet-elaborate/tests/infer.rs index 152d80d40..8d09921ce 100644 --- a/crates/pikelet-elaborate/tests/infer.rs +++ b/crates/pikelet-elaborate/tests/infer.rs @@ -51,7 +51,7 @@ fn import_not_found() { match pikelet_elaborate::infer_term(&context, &raw_term) { Err(TypeError::UndefinedImport { .. }) => {}, Err(err) => panic!("unexpected error: {:?}", err), - Ok((term, ty)) => panic!("expected error, found {} : {}", term, ty), + Ok((term, ty)) => panic!("expected error, found {} : {:?}", term, ty), } } @@ -591,7 +591,7 @@ fn case_expr_bool_bad() { match pikelet_elaborate::infer_term(&context, &raw_term) { Err(TypeError::Mismatch { .. }) => {}, Err(err) => panic!("unexpected error: {:?}", err), - Ok((term, ty)) => panic!("expected error, found {} : {}", term, ty), + Ok((term, ty)) => panic!("expected error, found {} : {:?}", term, ty), } } @@ -899,6 +899,6 @@ fn array_intro_ambiguous() { match pikelet_elaborate::infer_term(&context, &raw_term) { Err(TypeError::AmbiguousArrayLiteral { .. }) => {}, Err(err) => panic!("unexpected error: {:?}", err), - Ok((term, ty)) => panic!("expected error, found {} : {}", term, ty), + Ok((term, ty)) => panic!("expected error, found {} : {:?}", term, ty), } } diff --git a/crates/pikelet-syntax/src/domain.rs b/crates/pikelet-syntax/src/domain.rs index 947ebc6d2..66c3f9df8 100644 --- a/crates/pikelet-syntax/src/domain.rs +++ b/crates/pikelet-syntax/src/domain.rs @@ -1,12 +1,10 @@ //! The semantic domain of the language use moniker::{Binder, Embed, FreeVar, Nest, Scope, Var}; -use std::fmt; use std::ops; use std::rc::Rc; use core::{Literal, RcPattern, RcTerm, Term}; -use pretty::{self, ToDoc}; use {Label, Level, LevelShift}; /// Values @@ -99,12 +97,6 @@ impl Value { } } -impl fmt::Display for Value { - fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { - self.to_doc().group().render_fmt(pretty::FALLBACK_WIDTH, f) - } -} - /// Reference counted values #[derive(Debug, Clone, PartialEq, BoundTerm)] pub struct RcValue { @@ -156,12 +148,6 @@ impl ops::Deref for RcValue { } } -impl fmt::Display for RcValue { - fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { - fmt::Display::fmt(&self.inner, f) - } -} - /// The head of an application #[derive(Debug, Clone, PartialEq, BoundTerm)] pub enum Head { @@ -197,12 +183,6 @@ impl Neutral { } } -impl fmt::Display for Neutral { - fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { - self.to_doc().group().render_fmt(pretty::FALLBACK_WIDTH, f) - } -} - /// Reference counted neutral values #[derive(Debug, Clone, PartialEq, BoundTerm)] pub struct RcNeutral { diff --git a/crates/pikelet-syntax/src/pretty/core.rs b/crates/pikelet-syntax/src/pretty/core.rs index 0fc929069..6485c0eda 100644 --- a/crates/pikelet-syntax/src/pretty/core.rs +++ b/crates/pikelet-syntax/src/pretty/core.rs @@ -5,7 +5,6 @@ use moniker::{Binder, Embed, Var}; use std::iter; use core::{Literal, Pattern, Term}; -use domain::{Head, Neutral, Value}; use raw; use {FloatFormat, IntFormat, Label, Level, LevelShift}; @@ -327,82 +326,3 @@ impl ToDoc for Term { } } } - -impl ToDoc for Value { - fn to_doc(&self) -> StaticDoc { - match *self { - Value::Universe(level) => pretty_universe(level), - Value::Literal(ref literal) => literal.to_doc(), - Value::FunIntro(ref scope) => pretty_fun_intro( - &scope.unsafe_pattern.0, - &(scope.unsafe_pattern.1).0.inner, - &scope.unsafe_body.inner, - ), - Value::FunType(ref scope) => pretty_fun_ty( - &scope.unsafe_pattern.0, - &(scope.unsafe_pattern.1).0.inner, - &scope.unsafe_body.inner, - ), - Value::RecordType(ref scope) => pretty_record_ty(Doc::concat( - scope.unsafe_pattern.unsafe_patterns.iter().map( - |&(ref label, _, Embed(ref ann))| { - parens( - Doc::as_string(label) - .append(Doc::space()) - .append(ann.to_doc().group()), - ) - .append(Doc::newline()) - }, - ), - )), - Value::RecordIntro(ref scope) => pretty_record_intro(Doc::concat( - scope.unsafe_pattern.unsafe_patterns.iter().map( - |&(ref label, _, Embed(ref term))| { - parens( - Doc::as_string(label) - .append(Doc::space()) - .append(term.to_doc().group()), - ) - .append(Doc::newline()) - }, - ), - )), - Value::ArrayIntro(ref elems) => Doc::text("[") - .append(Doc::intersperse( - elems.iter().map(|elem| elem.to_doc()), - Doc::text(";").append(Doc::space()), - )) - .append("]"), - Value::Neutral(ref neutral, ref spine) if spine.is_empty() => neutral.to_doc(), - Value::Neutral(ref neutral, ref spine) => { - pretty_fun_app(neutral.to_doc(), spine.iter().map(|arg| &arg.inner)) - }, - } - } -} - -impl ToDoc for Neutral { - fn to_doc(&self) -> StaticDoc { - match *self { - Neutral::Head(ref head) => head.to_doc(), - Neutral::RecordProj(ref expr, ref label, shift) => { - pretty_record_proj(&expr.inner, label, shift) - }, - Neutral::Case(ref head, ref clauses) => pretty_case( - &head.inner, - clauses - .iter() - .map(|clause| (&clause.unsafe_pattern.inner, &clause.unsafe_body.inner)), - ), - } - } -} - -impl ToDoc for Head { - fn to_doc(&self) -> StaticDoc { - match *self { - Head::Var(ref var, shift) => pretty_var(var, shift), - Head::Import(ref name) => pretty_import(name), - } - } -} From 5cd1411cab906f592b25128f4d8580f24828234e Mon Sep 17 00:00:00 2001 From: Brendan Zabarauskas Date: Fri, 30 Nov 2018 17:15:05 +1100 Subject: [PATCH 3/9] Remove pretty printing module --- crates/pikelet-repl/src/lib.rs | 3 +- crates/pikelet-syntax/src/concrete.rs | 302 +++++++++++++++- crates/pikelet-syntax/src/core.rs | 222 +++++++++++- crates/pikelet-syntax/src/lib.rs | 11 +- .../pikelet-syntax/src/parse/grammar.lalrpop | 38 +- crates/pikelet-syntax/src/pretty/concrete.rs | 295 ---------------- crates/pikelet-syntax/src/pretty/core.rs | 328 ------------------ crates/pikelet-syntax/src/pretty/mod.rs | 48 --- crates/pikelet-syntax/src/raw.rs | 212 ++++++++++- .../pikelet-syntax/src/translation/desugar.rs | 8 +- .../pikelet-syntax/src/translation/resugar.rs | 2 +- 11 files changed, 755 insertions(+), 714 deletions(-) delete mode 100644 crates/pikelet-syntax/src/pretty/concrete.rs delete mode 100644 crates/pikelet-syntax/src/pretty/core.rs delete mode 100644 crates/pikelet-syntax/src/pretty/mod.rs diff --git a/crates/pikelet-repl/src/lib.rs b/crates/pikelet-repl/src/lib.rs index 05db154e1..8e61158ba 100644 --- a/crates/pikelet-repl/src/lib.rs +++ b/crates/pikelet-repl/src/lib.rs @@ -179,12 +179,11 @@ fn eval_print(pikelet: &mut Driver, filemap: &FileMap) -> Result usize { term_size::dimensions() .map(|(width, _)| width) - .unwrap_or(pretty::FALLBACK_WIDTH) + .unwrap_or(1_000_000) } let (repl_command, _import_paths, parse_errors) = parse::repl_command(filemap); diff --git a/crates/pikelet-syntax/src/concrete.rs b/crates/pikelet-syntax/src/concrete.rs index 80d797ca8..b799496ee 100644 --- a/crates/pikelet-syntax/src/concrete.rs +++ b/crates/pikelet-syntax/src/concrete.rs @@ -1,10 +1,10 @@ //! The concrete syntax of the language use codespan::{ByteIndex, ByteSpan}; +use pretty::{BoxDoc, Doc}; use std::fmt; -use pretty::{self, ToDoc}; -use {FloatFormat, IntFormat}; +use {FloatFormat, IntFormat, PRETTY_FALLBACK_WIDTH, PRETTY_INDENT_WIDTH}; /// Commands entered in the REPL #[derive(Debug, Clone)] @@ -83,7 +83,7 @@ pub struct RecordTypeField { } #[derive(Debug, Clone, PartialEq)] -pub enum RecordField { +pub enum RecordIntroField { Punned { label: (ByteIndex, String), shift: Option, @@ -142,11 +142,46 @@ impl Item { Item::Error(span) => span, } } + + pub fn to_doc(&self) -> Doc> { + match *self { + Item::Declaration { + name: (_, ref name), + ref ann, + .. + } => Doc::as_string(name) + .append(Doc::space()) + .append(":") + .append(Doc::space()) + .append(ann.to_doc()), + Item::Definition { + name: (_, ref name), + ref params, + ref return_ann, + ref body, + } => Doc::as_string(name) + .append(Doc::space()) + .append(match params[..] { + [] => Doc::nil(), + _ => pretty_fun_intro_params(params).append(Doc::space()), + }) + .append(return_ann.as_ref().map_or(Doc::nil(), |return_ann| { + Doc::text(":") + .append(return_ann.to_doc()) + .append(Doc::space()) + })) + .append("=") + .append(Doc::space()) + .append(body.to_doc().nest(PRETTY_INDENT_WIDTH)), + Item::Error(_) => Doc::text(""), + } + .append(";") + } } impl fmt::Display for Item { fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { - self.to_doc().group().render_fmt(pretty::FALLBACK_WIDTH, f) + self.to_doc().group().render_fmt(PRETTY_FALLBACK_WIDTH, f) } } @@ -177,6 +212,18 @@ impl Literal { | Literal::Float(span, _, _) => span, } } + + pub fn to_doc(&self) -> Doc> { + match *self { + Literal::String(_, ref value) => Doc::text(format!("{:?}", value)), + Literal::Char(_, value) => Doc::text(format!("{:?}", value)), + Literal::Int(_, value, IntFormat::Bin) => Doc::text(format!("0b{:b}", value)), + Literal::Int(_, value, IntFormat::Oct) => Doc::text(format!("0o{:o}", value)), + Literal::Int(_, value, IntFormat::Dec) => Doc::text(format!("{}", value)), + Literal::Int(_, value, IntFormat::Hex) => Doc::text(format!("0x{:x}", value)), + Literal::Float(_, value, FloatFormat::Dec) => Doc::text(format!("{}", value)), + } + } } /// Patterns @@ -220,6 +267,22 @@ impl Pattern { Pattern::Literal(ref literal) => literal.span(), } } + + pub fn to_doc(&self) -> Doc> { + match *self { + Pattern::Parens(_, ref term) => Doc::text("(").append(term.to_doc()).append(")"), + Pattern::Ann(ref term, ref ty) => term + .to_doc() + .append(Doc::space()) + .append(":") + .append(Doc::space()) + .append(ty.to_doc()), + Pattern::Name(_, ref name, None) => Doc::text(format!("{}", name)), + Pattern::Name(_, ref name, Some(shift)) => Doc::text(format!("{}^{}", name, shift)), + Pattern::Literal(ref literal) => literal.to_doc(), + Pattern::Error(_) => Doc::text(""), + } + } } /// Terms @@ -338,7 +401,7 @@ pub enum Term { /// record { x = t1, .. } /// record { id (a : Type) (x : a) : a = x, .. } /// ``` - RecordIntro(ByteSpan, Vec), + RecordIntro(ByteSpan, Vec), /// Record field projection /// /// ```text @@ -378,10 +441,237 @@ impl Term { Term::FunApp(ref head, ref arg) => head.span().to(arg.last().unwrap().span()), } } + + pub fn to_doc(&self) -> Doc> { + match *self { + Term::Parens(_, ref term) => Doc::text("(").append(term.to_doc()).append(")"), + Term::Ann(ref term, ref ty) => Doc::nil() + .append(term.to_doc()) + .append(Doc::space()) + .append(":") + .append(Doc::space()) + .append(ty.to_doc()), + Term::Universe(_, None) => Doc::text("Type"), + Term::Universe(_, Some(level)) => Doc::text(format!("Type^{}", level)), + Term::Literal(ref literal) => literal.to_doc(), + Term::ArrayIntro(_, ref elems) => Doc::nil() + .append("[") + .append(Doc::intersperse( + elems.iter().map(Term::to_doc), + Doc::text(";").append(Doc::space()), + )) + .append("]"), + Term::Hole(_) => Doc::text("_"), + Term::Name(_, ref name, None) => Doc::text(format!("{}", name)), + Term::Name(_, ref name, Some(shift)) => Doc::text(format!("{}^{}", name, shift)), + Term::Import(_, _, ref name) => Doc::nil() + .append("import") + .append(Doc::space()) + .append(format!("{:?}", name)), + Term::FunIntro(_, ref params, ref body) => Doc::nil() + .append("\\") + .append(pretty_fun_intro_params(params)) + .append(Doc::space()) + .append("=>") + .append(Doc::space()) + .append(body.to_doc()), + Term::FunType(_, ref params, ref body) => Doc::nil() + .append(pretty_fun_ty_params(params)) + .append(Doc::space()) + .append("->") + .append(Doc::space()) + .append(body.to_doc()), + Term::FunArrow(ref ann, ref body) => Doc::nil() + .append(ann.to_doc()) + .append(Doc::space()) + .append("->") + .append(Doc::space()) + .append(body.to_doc()), + Term::FunApp(ref head, ref args) => head.to_doc().append(Doc::space()).append( + Doc::intersperse(args.iter().map(|arg| arg.to_doc()), Doc::space()), + ), + Term::Let(_, ref items, ref body) => { + Doc::nil() + .append("let") + .append(Doc::space()) + .append(Doc::intersperse( + // FIXME: Indentation + items.iter().map(|item| item.to_doc()), + Doc::newline(), + )) + .append("in") + .append(body.to_doc()) + }, + Term::Where(ref expr, ref items, _) => Doc::nil() + .append(expr.to_doc()) + .append(Doc::newline()) + .append("where {") + .append(Doc::newline()) + .append(Doc::intersperse( + items.iter().map(|item| item.to_doc().group()), + Doc::newline(), + )) + .append(Doc::newline()) + .nest(PRETTY_INDENT_WIDTH) + .append("}"), + Term::If(_, ref cond, ref if_true, ref if_false) => Doc::nil() + .append("if") + .append(Doc::space()) + .append(cond.to_doc()) + .append(Doc::space()) + .append("then") + .append(Doc::space()) + .append(if_true.to_doc()) + .append(Doc::space()) + .append("else") + .append(Doc::space()) + .append(if_false.to_doc()), + Term::Case(_, ref head, ref clauses) => Doc::nil() + .append("case") + .append(Doc::space()) + .append(head.to_doc()) + .append(Doc::space()) + .append("of") + .append(Doc::space()) + .append("{") + .append(Doc::newline()) + .append(Doc::intersperse( + clauses.iter().map(|&(ref pattern, ref body)| { + Doc::nil() + .append(pattern.to_doc()) + .append(Doc::space()) + .append("=>") + .append(Doc::space()) + .append(body.to_doc()) + .append(";") + }), + Doc::newline(), + )) + .append(Doc::newline()) + .nest(PRETTY_INDENT_WIDTH) + .append("}"), + Term::RecordType(_, ref fields) if fields.is_empty() => Doc::text("Record {}"), + Term::RecordIntro(_, ref fields) if fields.is_empty() => Doc::text("record {}"), + Term::RecordType(_, ref fields) => Doc::nil() + .append("Record {") + .append(Doc::space()) + .append(Doc::intersperse( + fields.iter().map(|field| { + Doc::group( + Doc::nil() + .append(Doc::as_string(&field.label.1)) + .append(match field.binder { + Some((_, ref binder)) => Doc::space() + .append("as") + .append(Doc::space()) + .append(Doc::as_string(binder)), + None => Doc::nil(), + }) + .append(Doc::space()) + .append(":") + .append(Doc::space()) + .append(field.ann.to_doc()), + ) + }), + Doc::text(";").append(Doc::space()), + )) + .nest(PRETTY_INDENT_WIDTH) + .append(Doc::space()) + .append("}"), + Term::RecordIntro(_, ref fields) => Doc::nil() + .append("record {") + .append(Doc::space()) + .append(Doc::intersperse( + fields.iter().map(|field| match field { + RecordIntroField::Punned { + label: (_, ref label), + shift, + } => match shift { + None => Doc::text(format!("{}", label)), + Some(shift) => Doc::text(format!("{}^{}", label, shift)), + }, + RecordIntroField::Explicit { + label: (_, ref label), + ref params, + ref return_ann, + ref term, + } => Doc::group( + Doc::nil() + .append(Doc::as_string(label)) + .append(Doc::space()) + .append(match params[..] { + [] => Doc::nil(), + _ => pretty_fun_intro_params(params).append(Doc::space()), + }) + .append(return_ann.as_ref().map_or(Doc::nil(), |return_ann| { + Doc::text(":") + .append(return_ann.to_doc()) + .append(Doc::space()) + })) + .append("=") + .append(Doc::space()) + .append(term.to_doc()), + ), + }), + Doc::text(";").append(Doc::space()), + )) + .nest(PRETTY_INDENT_WIDTH) + .append(Doc::space()) + .append("}"), + Term::RecordProj(_, ref expr, _, ref label, None) => { + expr.to_doc().append(".").append(format!("{}", label)) + }, + Term::RecordProj(_, ref expr, _, ref label, Some(shift)) => Doc::nil() + .append(expr.to_doc()) + .append(".") + .append(format!("{}^{}", label, shift)), + Term::Error(_) => Doc::text(""), + } + } } impl fmt::Display for Term { fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { - self.to_doc().group().render_fmt(pretty::FALLBACK_WIDTH, f) + self.to_doc().group().render_fmt(PRETTY_FALLBACK_WIDTH, f) } } + +fn pretty_fun_intro_params(params: &[FunIntroParamGroup]) -> Doc> { + Doc::intersperse( + params.iter().map(|&(ref names, ref ann)| match *ann { + None if names.len() == 1 => Doc::as_string(&names[0].1), + None => unreachable!(), // FIXME - shouldn't be possible in AST + Some(ref ann) => Doc::nil() + .append("(") + .append(Doc::intersperse( + names.iter().map(|name| Doc::as_string(&name.1)), + Doc::space(), + )) + .append(Doc::space()) + .append(":") + .append(Doc::space()) + .append(ann.to_doc()) + .append(")"), + }), + Doc::space(), + ) +} + +fn pretty_fun_ty_params(params: &[FunTypeParamGroup]) -> Doc> { + Doc::intersperse( + params.iter().map(|&(ref names, ref ann)| { + Doc::nil() + .append("(") + .append(Doc::intersperse( + names.iter().map(|name| Doc::as_string(&name.1)), + Doc::space(), + )) + .append(Doc::space()) + .append(":") + .append(Doc::space()) + .append(ann.to_doc()) + .append(")") + }), + Doc::space(), + ) +} diff --git a/crates/pikelet-syntax/src/core.rs b/crates/pikelet-syntax/src/core.rs index cd788325f..44232c74a 100644 --- a/crates/pikelet-syntax/src/core.rs +++ b/crates/pikelet-syntax/src/core.rs @@ -1,13 +1,13 @@ //! The core syntax of the language use moniker::{Binder, Embed, FreeVar, Nest, Scope, Var}; +use pretty::{BoxDoc, Doc}; use std::fmt; use std::ops; use std::rc::Rc; use domain::{Head, Neutral, Value}; -use pretty::{self, ToDoc}; -use {FloatFormat, IntFormat, Label, Level, LevelShift}; +use {FloatFormat, IntFormat, Label, Level, LevelShift, PRETTY_FALLBACK_WIDTH}; /// Literals /// @@ -29,9 +29,30 @@ pub enum Literal { F64(f64, FloatFormat), } +impl Literal { + pub fn to_doc(&self) -> Doc> { + match *self { + Literal::Bool(true) => Doc::text("true"), + Literal::Bool(false) => Doc::text("false"), + Literal::String(ref value) => Doc::text(format!("{:?}", value)), + Literal::Char(value) => Doc::text(format!("{:?}", value)), + Literal::U8(value, _) => Doc::as_string(&value), + Literal::U16(value, _) => Doc::as_string(&value), + Literal::U32(value, _) => Doc::as_string(&value), + Literal::U64(value, _) => Doc::as_string(&value), + Literal::S8(value, _) => Doc::as_string(&value), + Literal::S16(value, _) => Doc::as_string(&value), + Literal::S32(value, _) => Doc::as_string(&value), + Literal::S64(value, _) => Doc::as_string(&value), + Literal::F32(value, _) => Doc::as_string(&value), + Literal::F64(value, _) => Doc::as_string(&value), + } + } +} + impl fmt::Display for Literal { fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { - self.to_doc().group().render_fmt(pretty::FALLBACK_WIDTH, f) + self.to_doc().group().render_fmt(PRETTY_FALLBACK_WIDTH, f) } } @@ -47,9 +68,32 @@ pub enum Pattern { Literal(Literal), } +impl Pattern { + pub fn to_doc(&self) -> Doc> { + match *self { + Pattern::Ann(ref pattern, Embed(ref ty)) => Doc::nil() + .append(pattern.to_doc()) + .append(Doc::space()) + .append(":") + .append(Doc::space()) + .append(ty.to_doc()), // fun-intro? + ref pattern => pattern.to_doc_atomic(), + } + } + + fn to_doc_atomic(&self) -> Doc> { + match *self { + Pattern::Binder(ref binder) => Doc::as_string(binder), + Pattern::Var(Embed(ref var), shift) => Doc::as_string(format!("{}^{}", var, shift)), + Pattern::Literal(ref literal) => literal.to_doc(), + ref pattern => Doc::text("(").append(pattern.to_doc()).append(")"), + } + } +} + impl fmt::Display for Pattern { fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { - self.to_doc().group().render_fmt(pretty::FALLBACK_WIDTH, f) + self.to_doc().group().render_fmt(PRETTY_FALLBACK_WIDTH, f) } } @@ -122,11 +166,179 @@ impl Term { pub fn var(var: impl Into>, shift: impl Into) -> Term { Term::Var(var.into(), shift.into()) } + + pub fn to_doc(&self) -> Doc> { + match *self { + Term::Ann(ref term, ref ty) => Doc::nil() + .append(term.to_doc_expr()) + .append(Doc::space()) + .append(":") + .append(Doc::space()) + .append(ty.to_doc_expr()), + ref term => term.to_doc_expr(), + } + } + + fn to_doc_expr(&self) -> Doc> { + match *self { + Term::Import(ref name) => Doc::nil() + .append("import") + .append(Doc::space()) + .append(format!("{:?}", name)), + Term::FunIntro(ref scope) => Doc::nil() + .append("\\") + .append(Doc::as_string(&scope.unsafe_pattern.0)) + .append(Doc::space()) + .append(":") + .append(Doc::space()) + .append((scope.unsafe_pattern.1).0.to_doc_arrow()) + .append(Doc::space()) + .append("=>") + .append(Doc::space()) + .append(scope.unsafe_body.to_doc_expr()), + Term::Case(ref head, ref clauses) => Doc::nil() + .append("case") + .append(Doc::space()) + .append(head.to_doc_app()) + .append(Doc::space()) + .append("{") + .append(Doc::space()) + .append(Doc::intersperse( + clauses.iter().map(|scope| { + Doc::nil() + .append(scope.unsafe_pattern.to_doc()) + .append(Doc::space()) + .append("=>") + .append(Doc::space()) + .append(scope.unsafe_body.to_doc()) + .append(";") + }), + Doc::newline(), + )) + .append(Doc::space()) + .append("}"), + Term::Let(ref scope) => Doc::nil() + .append("let") + .append(Doc::space()) + .append(Doc::intersperse( + scope.unsafe_pattern.unsafe_patterns.iter().map( + |&(ref binder, Embed((ref ann, ref value)))| { + Doc::nil() + .append(Doc::as_string(binder)) + .append(Doc::space()) + .append(":") + .append(Doc::space()) + .append(ann.to_doc()) + .append(Doc::space()) + .append("=") + .append(Doc::space()) + .append(value.to_doc()) + }, + ), + Doc::newline(), + )) + .append(Doc::space()) + .append("in") + .append(Doc::space()) + .append(scope.unsafe_body.to_doc_expr()), + ref term => term.to_doc_arrow(), + } + } + + fn to_doc_arrow(&self) -> Doc> { + match *self { + Term::FunType(ref scope) => Doc::nil() + .append("(") + .append(Doc::as_string(&scope.unsafe_pattern.0)) + .append(Doc::space()) + .append(":") + .append(Doc::space()) + .append((scope.unsafe_pattern.1).0.to_doc_arrow()) + .append(")") + .append(Doc::space()) + .append("->") + .append(Doc::space()) + .append(scope.unsafe_body.to_doc_expr()), + ref term => term.to_doc_app(), + } + } + + fn to_doc_app(&self) -> Doc> { + match *self { + Term::FunApp(ref fun, ref arg) => Doc::nil() + .append(fun.to_doc_atomic()) + .append(Doc::space()) + .append(arg.to_doc_atomic()), + ref term => term.to_doc_atomic(), + } + } + + fn to_doc_atomic(&self) -> Doc> { + match *self { + Term::Universe(level) => Doc::text(format!("Type^{}", level)), + Term::ArrayIntro(ref elems) => Doc::nil() + .append("[") + .append(Doc::intersperse( + elems.iter().map(|elem| elem.to_doc()), + Doc::text(";").append(Doc::space()), + )) + .append("]"), + Term::Var(ref var, ref level) => Doc::text(format!("{}^{}", var, level)), + Term::RecordType(ref scope) => Doc::nil() + .append("Record {") + .append(Doc::space()) + .append(Doc::intersperse( + scope.unsafe_pattern.unsafe_patterns.iter().map( + |&(ref label, ref binder, Embed(ref ann))| { + Doc::nil() + .append(Doc::as_string(label)) + .append(Doc::space()) + .append("as") + .append(Doc::space()) + .append(Doc::as_string(binder)) + .append(Doc::space()) + .append(":") + .append(Doc::space()) + .append(ann.to_doc()) + }, + ), + Doc::text(";").append(Doc::space()), + )) + .append(Doc::space()) + .append("}"), + Term::RecordIntro(ref scope) => 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()) + }, + ), + Doc::text(";").append(Doc::space()), + )) + .append(Doc::space()) + .append("}"), + Term::RecordProj(ref expr, ref label, ref shift) => Doc::nil() + .append(expr.to_doc_atomic()) + .append(".") + .append(format!("{}^{}", label, shift)), + ref term => Doc::text("(").append(term.to_doc()).append(")"), + } + } } impl fmt::Display for Term { fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { - self.to_doc().group().render_fmt(pretty::FALLBACK_WIDTH, f) + self.to_doc().group().render_fmt(PRETTY_FALLBACK_WIDTH, f) } } diff --git a/crates/pikelet-syntax/src/lib.rs b/crates/pikelet-syntax/src/lib.rs index 6c0e93599..38d4482b9 100644 --- a/crates/pikelet-syntax/src/lib.rs +++ b/crates/pikelet-syntax/src/lib.rs @@ -11,6 +11,7 @@ extern crate moniker; #[cfg(test)] #[macro_use] extern crate pretty_assertions; +extern crate pretty; extern crate unicode_xid; use moniker::{Binder, BoundPattern, BoundTerm, OnBoundFn, OnFreeFn, ScopeState, Var}; @@ -21,7 +22,6 @@ pub mod concrete; pub mod core; pub mod domain; pub mod parse; -pub mod pretty; pub mod raw; pub mod translation; @@ -170,3 +170,12 @@ impl fmt::Display for Label { write!(f, "{}", self.0) } } + +const PRETTY_INDENT_WIDTH: usize = 4; + +/// An effectively 'infinite' line length for when we don't have an explicit +/// width provided for pretty printing. +/// +/// `pretty.rs` seems to bug-out and break on every line when using +/// `usize::MAX`, so we'll just use a really big number instead... +pub const PRETTY_FALLBACK_WIDTH: usize = 1_000_000; diff --git a/crates/pikelet-syntax/src/parse/grammar.lalrpop b/crates/pikelet-syntax/src/parse/grammar.lalrpop index bd347c228..a341e4af6 100644 --- a/crates/pikelet-syntax/src/parse/grammar.lalrpop +++ b/crates/pikelet-syntax/src/parse/grammar.lalrpop @@ -1,7 +1,7 @@ use codespan::FileMap; use codespan::{ByteIndex, ByteSpan}; -use concrete::{Item, Literal, Pattern, Term, RecordTypeField, RecordField, ReplCommand}; +use concrete::{Item, Literal, Pattern, Term, RecordTypeField, RecordIntroField, ReplCommand}; use parse::{LalrpopError, ParseError, Token}; use {FloatFormat, IntFormat}; @@ -125,7 +125,7 @@ Literal: Literal = { pub Pattern: Pattern = { AtomicPattern, - ":" => { + ":" => { Pattern::Ann(Box::new(pattern), Box::new(ty)) } }; @@ -145,25 +145,25 @@ AtomicPattern : Pattern = { } pub Term: Term = { - FunIntroTerm, - ":" => { + ExprTerm, + ":" => { Term::Ann(Box::new(expr), Box::new(ty)) }, - "where" "{" "}" => { + "where" "{" "}" => { Term::Where(Box::new(expr), items, end) } }; -FunIntroTerm: Term = { - FunTypeTerm, +ExprTerm: Term = { + ArrowTerm, "import" => { import_paths.push(path.clone()); Term::Import(ByteSpan::new(start, end), ByteSpan::new(path_start, end), path) }, - "\\" ":" "=>" => { + "\\" ":" "=>" => { Term::FunIntro(start, vec![(vec![name], Some(Box::new(ann)))], Box::new(body)) }, - "\\" "=>" => { + "\\" "=>" => { Term::FunIntro(start, params, Box::new(body)) }, "if" "then" "else" => { @@ -174,27 +174,27 @@ FunIntroTerm: Term = { arms.extend(last); Term::Case(ByteSpan::new(start, end), Box::new(head), arms) }, - "let" "in" => { + "let" "in" => { Term::Let(start, items, Box::new(body)) }, }; -FunTypeTerm: Term = { +ArrowTerm: Term = { AppTerm, // Naively we would want to write the following rules: // // ```lalrpop - // ":" ")")+> "->" => { + // ":" ")")+> "->" => { // Term::FunType(params, Box::new(body)) // }, - // "->" => { + // "->" => { // Term::Arrow(Box::new(ann), Box::new(body)) // }, // ``` // // Alas this causes an ambiguity with the `AtomicTerm` rule. Therefore we // have to hack this in by reparsing the binder: - "->" =>? { + "->" =>? { super::reparse_fun_ty_hack(ByteSpan::new(start, end), binder, body) }, }; @@ -224,7 +224,7 @@ AtomicTerm: Term = { fields.extend(last); Term::RecordType(ByteSpan::new(start, end), fields) }, - "record" "{" ";")*> "}" => { + "record" "{" ";")*> "}" => { let mut fields = fields; fields.extend(last); Term::RecordIntro(ByteSpan::new(start, end), fields) @@ -240,7 +240,7 @@ AtomicTerm: Term = { AtomicLamParam: (Vec<(ByteIndex, String)>, Option>) = { => (vec![name], None), - "(" )?> ")" => (names, ann.map(Box::new)), + "(" )?> ")" => (names, ann.map(Box::new)), }; RecordTypeField: RecordTypeField = { @@ -253,13 +253,13 @@ PatternArm: (Pattern, Term) = { "=>" , }; -RecordField: RecordField = { +RecordIntroField: RecordIntroField = { )?> => { - RecordField::Punned { label, shift: shift.map(|x| x as u32) } + RecordIntroField::Punned { label, shift: shift.map(|x| x as u32) } }, )?> "=" => { let return_ann = return_ann.map(Box::new); - RecordField::Explicit { label, params, return_ann, term } + RecordIntroField::Explicit { label, params, return_ann, term } }, }; diff --git a/crates/pikelet-syntax/src/pretty/concrete.rs b/crates/pikelet-syntax/src/pretty/concrete.rs deleted file mode 100644 index 550552670..000000000 --- a/crates/pikelet-syntax/src/pretty/concrete.rs +++ /dev/null @@ -1,295 +0,0 @@ -//! Pretty printing for the concrete syntax - -use super::pretty::Doc; - -use concrete::{FunIntroParamGroup, FunTypeParamGroup, Item, Literal, Pattern, RecordField, Term}; -use {FloatFormat, IntFormat}; - -use super::{StaticDoc, ToDoc}; - -const INDENT_WIDTH: usize = 4; - -impl ToDoc for Item { - fn to_doc(&self) -> StaticDoc { - match *self { - Item::Declaration { - name: (_, ref name), - ref ann, - .. - } => Doc::as_string(name) - .append(Doc::space()) - .append(":") - .append(Doc::space()) - .append(ann.to_doc()), - Item::Definition { - name: (_, ref name), - ref params, - ref return_ann, - ref body, - } => Doc::as_string(name) - .append(Doc::space()) - .append(match params[..] { - [] => Doc::nil(), - _ => pretty_fun_intro_params(params).append(Doc::space()), - }) - .append(return_ann.as_ref().map_or(Doc::nil(), |return_ann| { - Doc::text(":") - .append(return_ann.to_doc()) - .append(Doc::space()) - })) - .append("=") - .append(Doc::space()) - .append(body.to_doc().nest(INDENT_WIDTH)), - Item::Error(_) => Doc::text(""), - } - .append(";") - } -} - -impl ToDoc for Literal { - fn to_doc(&self) -> StaticDoc { - match *self { - Literal::String(_, ref value) => Doc::text(format!("{:?}", value)), - Literal::Char(_, value) => Doc::text(format!("{:?}", value)), - Literal::Int(_, value, IntFormat::Bin) => Doc::text(format!("0b{:b}", value)), - Literal::Int(_, value, IntFormat::Oct) => Doc::text(format!("0o{:o}", value)), - Literal::Int(_, value, IntFormat::Dec) => Doc::text(format!("{}", value)), - Literal::Int(_, value, IntFormat::Hex) => Doc::text(format!("0x{:x}", value)), - Literal::Float(_, value, FloatFormat::Dec) => Doc::text(format!("{}", value)), - } - } -} - -impl ToDoc for Pattern { - fn to_doc(&self) -> StaticDoc { - match *self { - Pattern::Parens(_, ref term) => Doc::text("(").append(term.to_doc()).append(")"), - Pattern::Ann(ref term, ref ty) => term - .to_doc() - .append(Doc::space()) - .append(":") - .append(Doc::space()) - .append(ty.to_doc()), - Pattern::Name(_, ref name, None) => Doc::text(format!("{}", name)), - Pattern::Name(_, ref name, Some(shift)) => Doc::text(format!("{}^{}", name, shift)), - Pattern::Literal(ref literal) => literal.to_doc(), - Pattern::Error(_) => Doc::text(""), - } - } -} - -impl ToDoc for Term { - fn to_doc(&self) -> StaticDoc { - match *self { - Term::Parens(_, ref term) => Doc::text("(").append(term.to_doc()).append(")"), - Term::Ann(ref term, ref ty) => term - .to_doc() - .append(Doc::space()) - .append(":") - .append(Doc::space()) - .append(ty.to_doc()), - Term::Universe(_, None) => Doc::text("Type"), - Term::Universe(_, Some(level)) => Doc::text(format!("Type^{}", level)), - Term::Literal(ref literal) => literal.to_doc(), - Term::ArrayIntro(_, ref elems) => Doc::text("[") - .append(Doc::intersperse( - elems.iter().map(Term::to_doc), - Doc::text(";").append(Doc::space()), - )) - .append("]"), - Term::Hole(_) => Doc::text("_"), - Term::Name(_, ref name, None) => Doc::text(format!("{}", name)), - Term::Name(_, ref name, Some(shift)) => Doc::text(format!("{}^{}", name, shift)), - Term::Import(_, _, ref name) => Doc::text("import") - .append(Doc::space()) - .append(format!("{:?}", name)), - Term::FunIntro(_, ref params, ref body) => Doc::text("\\") - .append(pretty_fun_intro_params(params)) - .append(Doc::space()) - .append("=>") - .append(Doc::space()) - .append(body.to_doc()), - Term::FunType(_, ref params, ref body) => pretty_fun_ty_params(params) - .append(Doc::space()) - .append("->") - .append(Doc::space()) - .append(body.to_doc()), - Term::FunArrow(ref ann, ref body) => ann - .to_doc() - .append(Doc::space()) - .append("->") - .append(Doc::space()) - .append(body.to_doc()), - Term::FunApp(ref head, ref args) => head.to_doc().append(Doc::space()).append( - Doc::intersperse(args.iter().map(|arg| arg.to_doc()), Doc::space()), - ), - Term::Let(_, ref items, ref body) => { - Doc::text("let") - .append(Doc::space()) - .append(Doc::intersperse( - // FIXME: Indentation - items.iter().map(|item| item.to_doc()), - Doc::newline(), - )) - .append("in") - .append(body.to_doc()) - }, - Term::Where(ref expr, ref items, _) => expr - .to_doc() - .append(Doc::newline()) - .append("where {") - .append(Doc::newline()) - .append(Doc::intersperse( - items.iter().map(|item| item.to_doc().group()), - Doc::newline(), - )) - .append(Doc::newline()) - .nest(INDENT_WIDTH) - .append("}"), - Term::If(_, ref cond, ref if_true, ref if_false) => Doc::text("if") - .append(Doc::space()) - .append(cond.to_doc()) - .append(Doc::space()) - .append("then") - .append(Doc::space()) - .append(if_true.to_doc()) - .append(Doc::space()) - .append("else") - .append(Doc::space()) - .append(if_false.to_doc()), - Term::Case(_, ref head, ref clauses) => Doc::text("case") - .append(Doc::space()) - .append(head.to_doc()) - .append(Doc::space()) - .append("of") - .append(Doc::space()) - .append("{") - .append(Doc::newline()) - .append(Doc::intersperse( - clauses.iter().map(|&(ref pattern, ref body)| { - pattern - .to_doc() - .append(Doc::space()) - .append("=>") - .append(Doc::space()) - .append(body.to_doc()) - .append(";") - }), - Doc::newline(), - )) - .append(Doc::newline()) - .nest(INDENT_WIDTH) - .append("}"), - Term::RecordType(_, ref fields) if fields.is_empty() => Doc::text("Record {}"), - Term::RecordIntro(_, ref fields) if fields.is_empty() => Doc::text("record {}"), - Term::RecordType(_, ref fields) => Doc::text("Record {") - .append(Doc::space()) - .append(Doc::intersperse( - fields.iter().map(|field| { - Doc::group( - Doc::as_string(&field.label.1) - .append(match field.binder { - Some((_, ref binder)) => Doc::space() - .append("as") - .append(Doc::space()) - .append(Doc::as_string(binder)), - None => Doc::nil(), - }) - .append(Doc::space()) - .append(":") - .append(Doc::space()) - .append(field.ann.to_doc()), - ) - }), - Doc::text(";").append(Doc::space()), - )) - .nest(INDENT_WIDTH) - .append(Doc::space()) - .append("}"), - Term::RecordIntro(_, ref fields) => Doc::text("record {") - .append(Doc::space()) - .append(Doc::intersperse( - fields.iter().map(|field| match field { - RecordField::Punned { - label: (_, ref label), - shift, - } => match shift { - None => Doc::text(format!("{}", label)), - Some(shift) => Doc::text(format!("{}^{}", label, shift)), - }, - RecordField::Explicit { - label: (_, ref label), - ref params, - ref return_ann, - ref term, - } => Doc::group( - Doc::as_string(label) - .append(Doc::space()) - .append(match params[..] { - [] => Doc::nil(), - _ => pretty_fun_intro_params(params).append(Doc::space()), - }) - .append(return_ann.as_ref().map_or(Doc::nil(), |return_ann| { - Doc::text(":") - .append(return_ann.to_doc()) - .append(Doc::space()) - })) - .append("=") - .append(Doc::space()) - .append(term.to_doc()), - ), - }), - Doc::text(";").append(Doc::space()), - )) - .nest(INDENT_WIDTH) - .append(Doc::space()) - .append("}"), - Term::RecordProj(_, ref expr, _, ref label, None) => { - expr.to_doc().append(".").append(format!("{}", label)) - }, - Term::RecordProj(_, ref expr, _, ref label, Some(shift)) => expr - .to_doc() - .append(".") - .append(format!("{}^{}", label, shift)), - Term::Error(_) => Doc::text(""), - } - } -} - -fn pretty_fun_intro_params(params: &[FunIntroParamGroup]) -> StaticDoc { - Doc::intersperse( - params.iter().map(|&(ref names, ref ann)| match *ann { - None if names.len() == 1 => Doc::as_string(&names[0].1), - None => unreachable!(), // FIXME - shouldn't be possible in AST - Some(ref ann) => Doc::text("(") - .append(Doc::intersperse( - names.iter().map(|name| Doc::as_string(&name.1)), - Doc::space(), - )) - .append(Doc::space()) - .append(":") - .append(Doc::space()) - .append(ann.to_doc()) - .append(")"), - }), - Doc::space(), - ) -} - -fn pretty_fun_ty_params(params: &[FunTypeParamGroup]) -> StaticDoc { - Doc::intersperse( - params.iter().map(|&(ref names, ref ann)| { - Doc::text("(") - .append(Doc::intersperse( - names.iter().map(|name| Doc::as_string(&name.1)), - Doc::space(), - )) - .append(Doc::space()) - .append(":") - .append(Doc::space()) - .append(ann.to_doc()) - .append(")") - }), - Doc::space(), - ) -} diff --git a/crates/pikelet-syntax/src/pretty/core.rs b/crates/pikelet-syntax/src/pretty/core.rs deleted file mode 100644 index 6485c0eda..000000000 --- a/crates/pikelet-syntax/src/pretty/core.rs +++ /dev/null @@ -1,328 +0,0 @@ -//! Pretty printing for the core syntax - -use super::pretty::Doc; -use moniker::{Binder, Embed, Var}; -use std::iter; - -use core::{Literal, Pattern, Term}; -use raw; -use {FloatFormat, IntFormat, Label, Level, LevelShift}; - -use super::{parens, sexpr, StaticDoc, ToDoc}; - -fn pretty_ann(expr: &impl ToDoc, ty: &impl ToDoc) -> StaticDoc { - sexpr( - "ann", - expr.to_doc().append(Doc::space()).append(ty.to_doc()), - ) -} - -fn pretty_universe(level: Level) -> StaticDoc { - sexpr("Type", Doc::as_string(&level)) -} - -fn pretty_binder(binder: &Binder) -> StaticDoc { - sexpr("binder", Doc::text(format!("{:#}", binder))) -} - -fn pretty_var(var: &Var, shift: LevelShift) -> StaticDoc { - sexpr("var", Doc::text(format!("{:#}^{}", var, shift))) -} - -fn pretty_import(name: &str) -> StaticDoc { - sexpr("import", Doc::text(format!("{:?}", name))) -} - -fn pretty_fun_intro(binder: &Binder, ann: &impl ToDoc, body: &impl ToDoc) -> StaticDoc { - sexpr( - "λ", - Doc::group(parens( - pretty_binder(binder) - .append(Doc::space()) - .append(ann.to_doc().group()), - )) - .append(Doc::space()) - .append(body.to_doc()), - ) -} - -fn pretty_let(binders: StaticDoc, body: &impl ToDoc) -> StaticDoc { - sexpr("let", binders.append(Doc::space()).append(body.to_doc())) -} - -fn pretty_fun_ty(binder: &Binder, ann: &impl ToDoc, body: &impl ToDoc) -> StaticDoc { - sexpr( - "Π", - Doc::group(parens( - pretty_binder(binder) - .append(Doc::space()) - .append(ann.to_doc().group()), - )) - .append(Doc::space()) - .append(body.to_doc()), - ) -} - -fn pretty_fun_app<'a, As, A>(expr: StaticDoc, args: As) -> StaticDoc -where - As: 'a + IntoIterator, - A: 'a + ToDoc, -{ - sexpr( - "app", - expr.append(Doc::space()).append(Doc::intersperse( - args.into_iter().map(A::to_doc), - Doc::space(), - )), - ) -} - -fn pretty_record_ty(inner: StaticDoc) -> StaticDoc { - sexpr("Record", inner) -} - -fn pretty_record_intro(inner: StaticDoc) -> StaticDoc { - sexpr("record", inner) -} - -fn pretty_case<'a, Cs, P, T>(head: &impl ToDoc, clauses: Cs) -> StaticDoc -where - Cs: 'a + IntoIterator, - P: 'a + ToDoc, - T: 'a + ToDoc, -{ - sexpr( - "case", - head.to_doc().append(Doc::space()).append(Doc::intersperse( - clauses.into_iter().map(|(pattern, body)| { - parens(pattern.to_doc().append(Doc::space()).append(body.to_doc())) - }), - Doc::space(), - )), - ) -} - -fn pretty_record_proj(expr: &impl ToDoc, label: &Label, shift: LevelShift) -> StaticDoc { - sexpr( - "proj", - expr.to_doc() - .append(Doc::space()) - .append(Doc::text(format!("{:#}^{}", label, shift))), - ) -} - -impl ToDoc for raw::Literal { - fn to_doc(&self) -> StaticDoc { - match *self { - raw::Literal::String(_, ref value) => Doc::text(format!("{:?}", value)), - raw::Literal::Char(_, value) => Doc::text(format!("{:?}", value)), - raw::Literal::Int(_, value, IntFormat::Bin) => Doc::text(format!("0b{:b}", value)), - raw::Literal::Int(_, value, IntFormat::Oct) => Doc::text(format!("0o{:o}", value)), - raw::Literal::Int(_, value, IntFormat::Dec) => Doc::text(format!("{}", value)), - raw::Literal::Int(_, value, IntFormat::Hex) => Doc::text(format!("0x{:x}", value)), - raw::Literal::Float(_, value, FloatFormat::Dec) => Doc::text(format!("{}", value)), - } - } -} - -impl ToDoc for raw::Pattern { - fn to_doc(&self) -> StaticDoc { - match *self { - raw::Pattern::Ann(ref pattern, Embed(ref ty)) => pretty_ann(&pattern.inner, &ty.inner), - raw::Pattern::Binder(_, ref binder) => pretty_binder(binder), - raw::Pattern::Var(_, Embed(ref var), shift) => pretty_var(var, shift), - raw::Pattern::Literal(ref literal) => literal.to_doc(), - } - } -} - -impl ToDoc for raw::Term { - fn to_doc(&self) -> StaticDoc { - match *self { - raw::Term::Ann(ref expr, ref ty) => pretty_ann(&expr.inner, &ty.inner), - raw::Term::Universe(_, level) => pretty_universe(level), - raw::Term::Hole(_) => parens(Doc::text("hole")), - raw::Term::Literal(ref literal) => literal.to_doc(), - raw::Term::Var(_, ref var, shift) => pretty_var(var, shift), - raw::Term::Import(_, _, ref name) => pretty_import(name), - raw::Term::FunIntro(_, ref scope) => pretty_fun_intro( - &scope.unsafe_pattern.0, - &(scope.unsafe_pattern.1).0.inner, - &scope.unsafe_body.inner, - ), - raw::Term::FunType(_, ref scope) => pretty_fun_ty( - &scope.unsafe_pattern.0, - &(scope.unsafe_pattern.1).0.inner, - &scope.unsafe_body.inner, - ), - raw::Term::FunApp(ref head, ref arg) => { - pretty_fun_app(head.to_doc(), iter::once(&arg.inner)) - }, - raw::Term::Let(_, ref scope) => pretty_let( - Doc::concat(scope.unsafe_pattern.unsafe_patterns.iter().map( - |&(ref binder, Embed((ref ann, ref term)))| { - parens( - pretty_binder(binder) - .append(Doc::space()) - .append(ann.to_doc().group()) - .append(Doc::space()) - .append(term.to_doc().group()), - ) - .append(Doc::newline()) - }, - )), - &scope.unsafe_body.inner, - ), - raw::Term::RecordType(_, ref scope) => pretty_record_ty(Doc::concat( - scope.unsafe_pattern.unsafe_patterns.iter().map( - |&(ref label, _, Embed(ref ann))| { - parens( - Doc::as_string(label) - .append(Doc::space()) - .append(ann.to_doc().group()), - ) - .append(Doc::newline()) - }, - ), - )), - raw::Term::RecordIntro(_, ref scope) => pretty_record_intro(Doc::concat( - scope.unsafe_pattern.unsafe_patterns.iter().map( - |&(ref label, _, Embed(ref term))| { - parens( - Doc::as_string(label) - .append(Doc::space()) - .append(term.to_doc().group()), - ) - .append(Doc::newline()) - }, - ), - )), - raw::Term::RecordProj(_, ref expr, _, ref label, shift) => { - pretty_record_proj(&expr.inner, label, shift) - }, - raw::Term::Case(_, ref head, ref clauses) => pretty_case( - &head.inner, - clauses - .iter() - .map(|clause| (&clause.unsafe_pattern.inner, &clause.unsafe_body.inner)), - ), - raw::Term::ArrayIntro(_, ref elems) => Doc::text("[") - .append(Doc::intersperse( - elems.iter().map(|elem| elem.to_doc()), - Doc::text(";").append(Doc::space()), - )) - .append("]"), - } - } -} - -impl ToDoc for Literal { - fn to_doc(&self) -> StaticDoc { - match *self { - Literal::Bool(true) => Doc::text("true"), - Literal::Bool(false) => Doc::text("false"), - Literal::String(ref value) => Doc::text(format!("{:?}", value)), - Literal::Char(value) => Doc::text(format!("{:?}", value)), - Literal::U8(value, _) => Doc::as_string(&value), - Literal::U16(value, _) => Doc::as_string(&value), - Literal::U32(value, _) => Doc::as_string(&value), - Literal::U64(value, _) => Doc::as_string(&value), - Literal::S8(value, _) => Doc::as_string(&value), - Literal::S16(value, _) => Doc::as_string(&value), - Literal::S32(value, _) => Doc::as_string(&value), - Literal::S64(value, _) => Doc::as_string(&value), - Literal::F32(value, _) => Doc::as_string(&value), - Literal::F64(value, _) => Doc::as_string(&value), - } - } -} - -impl ToDoc for Pattern { - fn to_doc(&self) -> StaticDoc { - match *self { - Pattern::Ann(ref pattern, Embed(ref ty)) => pretty_ann(&pattern.inner, &ty.inner), - Pattern::Binder(ref binder) => pretty_binder(binder), - Pattern::Var(Embed(ref var), shift) => pretty_var(var, shift), - Pattern::Literal(ref literal) => literal.to_doc(), - } - } -} - -impl ToDoc for Term { - fn to_doc(&self) -> StaticDoc { - match *self { - Term::Ann(ref expr, ref ty) => pretty_ann(&expr.inner, &ty.inner), - Term::Universe(level) => pretty_universe(level), - Term::Literal(ref literal) => literal.to_doc(), - Term::Var(ref var, shift) => pretty_var(var, shift), - Term::Import(ref name) => pretty_import(name), - Term::FunIntro(ref scope) => pretty_fun_intro( - &scope.unsafe_pattern.0, - &(scope.unsafe_pattern.1).0.inner, - &scope.unsafe_body.inner, - ), - Term::FunType(ref scope) => pretty_fun_ty( - &scope.unsafe_pattern.0, - &(scope.unsafe_pattern.1).0.inner, - &scope.unsafe_body.inner, - ), - Term::Let(ref scope) => pretty_let( - Doc::concat(scope.unsafe_pattern.unsafe_patterns.iter().map( - |&(ref binder, Embed((ref ann, ref term)))| { - parens( - pretty_binder(binder) - .append(Doc::space()) - .append(ann.to_doc().group()) - .append(Doc::space()) - .append(term.to_doc().group()), - ) - .append(Doc::newline()) - }, - )), - &scope.unsafe_body.inner, - ), - Term::FunApp(ref head, ref arg) => { - pretty_fun_app(head.to_doc(), iter::once(&arg.inner)) - }, - Term::RecordType(ref scope) => pretty_record_ty(Doc::concat( - scope.unsafe_pattern.unsafe_patterns.iter().map( - |&(ref label, _, Embed(ref ann))| { - parens( - Doc::as_string(label) - .append(Doc::space()) - .append(ann.to_doc().group()), - ) - .append(Doc::newline()) - }, - ), - )), - Term::RecordIntro(ref scope) => pretty_record_intro(Doc::concat( - scope.unsafe_pattern.unsafe_patterns.iter().map( - |&(ref label, _, Embed(ref term))| { - parens( - Doc::as_string(label) - .append(Doc::space()) - .append(term.to_doc().group()), - ) - .append(Doc::newline()) - }, - ), - )), - Term::RecordProj(ref expr, ref label, shift) => { - pretty_record_proj(&expr.inner, label, shift) - }, - Term::Case(ref head, ref clauses) => pretty_case( - &head.inner, - clauses - .iter() - .map(|clause| (&clause.unsafe_pattern.inner, &clause.unsafe_body.inner)), - ), - Term::ArrayIntro(ref elems) => Doc::text("[") - .append(Doc::intersperse( - elems.iter().map(|elem| elem.to_doc()), - Doc::text(";").append(Doc::space()), - )) - .append("]"), - } - } -} diff --git a/crates/pikelet-syntax/src/pretty/mod.rs b/crates/pikelet-syntax/src/pretty/mod.rs deleted file mode 100644 index c729f44f8..000000000 --- a/crates/pikelet-syntax/src/pretty/mod.rs +++ /dev/null @@ -1,48 +0,0 @@ -//! Pretty printing utilities - -extern crate pretty; - -use self::pretty::termcolor::ColorSpec; -use self::pretty::{BoxDoc, Doc}; -use std::rc::Rc; - -mod concrete; -mod core; - -/// An effectively 'infinite' line length for when we don't have an explicit -/// width provided for pretty printing. -/// -/// `pretty.rs` seems to bug-out and break on every line when using -/// `usize::MAX`, so we'll just use a really big number instead... -pub const FALLBACK_WIDTH: usize = 1_000_000; - -pub type StaticDoc = Doc<'static, BoxDoc<'static, ColorSpec>, ColorSpec>; - -/// Convert a datatype to a pretty-printable document -pub trait ToDoc { - fn to_doc(&self) -> StaticDoc; -} - -impl<'a, T: ToDoc> ToDoc for &'a T { - fn to_doc(&self) -> StaticDoc { - (*self).to_doc() - } -} - -impl ToDoc for Rc { - fn to_doc(&self) -> StaticDoc { - (**self).to_doc() - } -} - -fn parens(doc: StaticDoc) -> StaticDoc { - Doc::text("(").append(doc.append(")").nest(1)) -} - -fn sexpr(name: &'static str, doc: StaticDoc) -> StaticDoc { - parens( - Doc::text(name) - .append(Doc::space()) - .append(doc.nest(name.len())), - ) -} diff --git a/crates/pikelet-syntax/src/raw.rs b/crates/pikelet-syntax/src/raw.rs index fa018230e..1ea4464ea 100644 --- a/crates/pikelet-syntax/src/raw.rs +++ b/crates/pikelet-syntax/src/raw.rs @@ -3,12 +3,12 @@ use codespan::ByteSpan; use moniker::{Binder, Embed, Nest, Scope, Var}; +use pretty::{BoxDoc, Doc}; use std::fmt; use std::ops; use std::rc::Rc; -use pretty::{self, ToDoc}; -use {FloatFormat, IntFormat, Label, Level, LevelShift}; +use {FloatFormat, IntFormat, Label, Level, LevelShift, PRETTY_FALLBACK_WIDTH}; /// Literals #[derive(Debug, Clone, PartialEq, PartialOrd, BoundTerm, BoundPattern)] @@ -29,11 +29,23 @@ impl Literal { | Literal::Float(span, ..) => span, } } + + pub fn to_doc(&self) -> Doc> { + match *self { + Literal::String(_, ref value) => Doc::text(format!("{:?}", value)), + Literal::Char(_, value) => Doc::text(format!("{:?}", value)), + Literal::Int(_, value, IntFormat::Bin) => Doc::text(format!("0b{:b}", value)), + Literal::Int(_, value, IntFormat::Oct) => Doc::text(format!("0o{:o}", value)), + Literal::Int(_, value, IntFormat::Dec) => Doc::text(format!("{}", value)), + Literal::Int(_, value, IntFormat::Hex) => Doc::text(format!("0x{:x}", value)), + Literal::Float(_, value, FloatFormat::Dec) => Doc::text(format!("{}", value)), + } + } } impl fmt::Display for Literal { fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { - self.to_doc().group().render_fmt(pretty::FALLBACK_WIDTH, f) + self.to_doc().group().render_fmt(PRETTY_FALLBACK_WIDTH, f) } } @@ -58,11 +70,32 @@ impl Pattern { Pattern::Literal(ref literal) => literal.span(), } } + + pub fn to_doc(&self) -> Doc> { + match *self { + Pattern::Ann(ref pattern, Embed(ref ty)) => Doc::nil() + .append(pattern.to_doc()) + .append(Doc::space()) + .append(":") + .append(Doc::space()) + .append(ty.to_doc_expr()), + ref pattern => pattern.to_doc_atomic(), + } + } + + fn to_doc_atomic(&self) -> Doc> { + match *self { + Pattern::Binder(_, ref binder) => Doc::as_string(binder), + Pattern::Var(_, Embed(ref var), shift) => Doc::as_string(format!("{}^{}", var, shift)), + Pattern::Literal(ref literal) => literal.to_doc(), + ref pattern => Doc::text("(").append(pattern.to_doc()).append(")"), + } + } } impl fmt::Display for Pattern { fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { - self.to_doc().group().render_fmt(pretty::FALLBACK_WIDTH, f) + self.to_doc().group().render_fmt(PRETTY_FALLBACK_WIDTH, f) } } @@ -161,11 +194,180 @@ impl Term { Term::FunApp(ref head, ref arg) => head.span().to(arg.span()), } } + + pub fn to_doc(&self) -> Doc> { + match *self { + Term::Ann(ref term, ref ty) => Doc::nil() + .append(term.to_doc_expr()) + .append(Doc::space()) + .append(":") + .append(Doc::space()) + .append(ty.to_doc_expr()), + ref term => term.to_doc_expr(), + } + } + + fn to_doc_expr(&self) -> Doc> { + match *self { + Term::Import(_, _, ref name) => Doc::nil() + .append("import") + .append(Doc::space()) + .append(format!("{:?}", name)), + Term::FunIntro(_, ref scope) => Doc::nil() + .append("\\") + .append(Doc::as_string(&scope.unsafe_pattern.0)) + .append(Doc::space()) + .append(":") + .append(Doc::space()) + .append((scope.unsafe_pattern.1).0.to_doc_arrow()) + .append(Doc::space()) + .append("=>") + .append(Doc::space()) + .append(scope.unsafe_body.to_doc_expr()), + Term::Case(_, ref head, ref clauses) => Doc::nil() + .append("case") + .append(Doc::space()) + .append(head.to_doc_app()) + .append(Doc::space()) + .append("{") + .append(Doc::space()) + .append(Doc::intersperse( + clauses.iter().map(|scope| { + Doc::nil() + .append(scope.unsafe_pattern.to_doc()) + .append(Doc::space()) + .append("=>") + .append(Doc::space()) + .append(scope.unsafe_body.to_doc()) + .append(";") + }), + Doc::newline(), + )) + .append(Doc::space()) + .append("}"), + Term::Let(_, ref scope) => Doc::nil() + .append("let") + .append(Doc::space()) + .append(Doc::intersperse( + scope.unsafe_pattern.unsafe_patterns.iter().map( + |&(ref binder, Embed((ref ann, ref value)))| { + Doc::nil() + .append(Doc::as_string(binder)) + .append(Doc::space()) + .append(":") + .append(Doc::space()) + .append(ann.to_doc()) + .append(Doc::space()) + .append("=") + .append(Doc::space()) + .append(value.to_doc()) + }, + ), + Doc::newline(), + )) + .append(Doc::space()) + .append("in") + .append(Doc::space()) + .append(scope.unsafe_body.to_doc_expr()), + ref term => term.to_doc_arrow(), + } + } + + fn to_doc_arrow(&self) -> Doc> { + match *self { + Term::FunType(_, ref scope) => Doc::nil() + .append("(") + .append(Doc::as_string(&scope.unsafe_pattern.0)) + .append(Doc::space()) + .append(":") + .append(Doc::space()) + .append((scope.unsafe_pattern.1).0.to_doc_arrow()) + .append(")") + .append(Doc::space()) + .append("->") + .append(Doc::space()) + .append(scope.unsafe_body.to_doc_expr()), + ref term => term.to_doc_app(), + } + } + + fn to_doc_app(&self) -> Doc> { + match *self { + Term::FunApp(ref fun, ref arg) => Doc::nil() + .append(fun.to_doc_atomic()) + .append(Doc::space()) + .append(arg.to_doc_atomic()), + ref term => term.to_doc_atomic(), + } + } + + fn to_doc_atomic(&self) -> Doc> { + match *self { + Term::Universe(_, level) => Doc::text(format!("Type^{}", level)), + Term::ArrayIntro(_, ref elems) => Doc::nil() + .append("[") + .append(Doc::intersperse( + elems.iter().map(|elem| elem.to_doc()), + Doc::text(";").append(Doc::space()), + )) + .append("]"), + Term::Var(_, ref var, ref level) => Doc::text(format!("{}^{}", var, level)), + Term::Hole(_) => Doc::text("_"), + Term::RecordType(_, ref scope) => Doc::nil() + .append("Record {") + .append(Doc::space()) + .append(Doc::intersperse( + scope.unsafe_pattern.unsafe_patterns.iter().map( + |&(ref label, ref binder, Embed(ref ann))| { + Doc::nil() + .append(Doc::as_string(label)) + .append(Doc::space()) + .append("as") + .append(Doc::space()) + .append(Doc::as_string(binder)) + .append(Doc::space()) + .append(":") + .append(Doc::space()) + .append(ann.to_doc()) + }, + ), + Doc::text(";").append(Doc::space()), + )) + .append(Doc::space()) + .append("}"), + Term::RecordIntro(_, ref scope) => 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()) + }, + ), + Doc::text(";").append(Doc::space()), + )) + .append(Doc::space()) + .append("}"), + Term::RecordProj(_, ref expr, _, ref label, ref shift) => Doc::nil() + .append(expr.to_doc_atomic()) + .append(".") + .append(format!("{}^{}", label, shift)), + ref term => Doc::text("(").append(term.to_doc()).append(")"), + } + } } impl fmt::Display for Term { fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { - self.to_doc().group().render_fmt(pretty::FALLBACK_WIDTH, f) + self.to_doc().group().render_fmt(PRETTY_FALLBACK_WIDTH, f) } } diff --git a/crates/pikelet-syntax/src/translation/desugar.rs b/crates/pikelet-syntax/src/translation/desugar.rs index 39e46a253..3fb266f84 100644 --- a/crates/pikelet-syntax/src/translation/desugar.rs +++ b/crates/pikelet-syntax/src/translation/desugar.rs @@ -386,16 +386,16 @@ fn desugar_record_ty( fn desugar_record_intro( env: &DesugarEnv, span: ByteSpan, - fields: &[concrete::RecordField], + fields: &[concrete::RecordIntroField], ) -> Result { - use concrete::RecordField; + use concrete::RecordIntroField; let mut env = env.clone(); let fields = fields .iter() .map(|field| match field { - RecordField::Punned { + RecordIntroField::Punned { label: (_, ref name), shift, } => { @@ -403,7 +403,7 @@ fn desugar_record_intro( let free_var = env.on_binding(name); Ok((Label(name.clone()), Binder(free_var), Embed(var))) }, - RecordField::Explicit { + RecordIntroField::Explicit { label: (_, ref name), ref params, ref return_ann, diff --git a/crates/pikelet-syntax/src/translation/resugar.rs b/crates/pikelet-syntax/src/translation/resugar.rs index 2aadcca70..40c81288a 100644 --- a/crates/pikelet-syntax/src/translation/resugar.rs +++ b/crates/pikelet-syntax/src/translation/resugar.rs @@ -541,7 +541,7 @@ fn resugar_term(env: &ResugarEnv, term: &core::Term, prec: Prec) -> concrete::Te let name = env.on_item(&label, &binder); // TODO: use a punned label if possible? - concrete::RecordField::Explicit { + concrete::RecordIntroField::Explicit { label: (ByteIndex::default(), name), params: term_params, return_ann: None, From af14f8574337d9124d198efa61b89cae2cd53a44 Mon Sep 17 00:00:00 2001 From: Brendan Zabarauskas Date: Sat, 1 Dec 2018 16:41:27 +1100 Subject: [PATCH 4/9] Add missing keyword --- crates/pikelet-syntax/src/translation/resugar.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/crates/pikelet-syntax/src/translation/resugar.rs b/crates/pikelet-syntax/src/translation/resugar.rs index 40c81288a..451860052 100644 --- a/crates/pikelet-syntax/src/translation/resugar.rs +++ b/crates/pikelet-syntax/src/translation/resugar.rs @@ -15,7 +15,7 @@ pub struct ResugarEnv { } const KEYWORDS: &[&str] = &[ - "as", "case", "else", "if", "import", "in", "let", "record", "Record", "then", "Type", + "as", "case", "else", "if", "import", "in", "let", "record", "Record", "then", "Type", "where", ]; impl ResugarEnv { From 9bd201001045bbf31aea122814239c371d0ad656 Mon Sep 17 00:00:00 2001 From: Brendan Zabarauskas Date: Sat, 1 Dec 2018 16:58:58 +1100 Subject: [PATCH 5/9] Add missing crate to cargo workspace --- Cargo.toml | 1 + 1 file changed, 1 insertion(+) diff --git a/Cargo.toml b/Cargo.toml index e5f890e78..8ef0dfcb5 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -4,6 +4,7 @@ members = [ "./crates/pikelet-driver", "./crates/pikelet-elaborate", "./crates/pikelet-language-server", + "./crates/pikelet-library", "./crates/pikelet-repl", "./crates/pikelet-syntax", ] From b62c95a3b76673bbf6541279045e51ac6c8e7f4d Mon Sep 17 00:00:00 2001 From: Brendan Zabarauskas Date: Sat, 1 Dec 2018 18:02:57 +1100 Subject: [PATCH 6/9] Rework crate structure of compiler front-end This replaces the `pikelet-syntax` and `pikelet-elaborate` crates with the `pikelet-concrete` and `pikelet-core` crates. This will make it easier to begin rebuilding on a foundation based on https://github.com/brendanzab/rust-nbe-for-mltt --- Cargo.toml | 4 +- crates/README.md | 16 +- .../Cargo.toml | 3 +- crates/pikelet-concrete/README.md | 17 ++ .../build.rs | 0 .../src}/desugar.rs | 9 +- .../src/elaborate}/context.rs | 42 +++-- .../src/elaborate}/errors.rs | 46 +++--- .../src/elaborate/mod.rs} | 48 +++--- crates/pikelet-concrete/src/lib.rs | 22 +++ .../src/parse/errors.rs | 0 .../src/parse/grammar.lalrpop | 5 +- .../src/parse/lexer.rs | 0 .../src/parse/mod.rs | 4 +- .../src}/resugar.rs | 20 +-- .../src/syntax}/concrete.rs | 4 +- crates/pikelet-concrete/src/syntax/mod.rs | 11 ++ .../src/syntax}/raw.rs | 4 +- .../tests/check.rs | 18 +-- .../tests/desugar.rs | 11 +- .../tests/goldenfiles/ann | 0 .../tests/goldenfiles/ann_ann_ann | 0 .../tests/goldenfiles/ann_ann_left | 0 .../tests/goldenfiles/ann_ann_right | 0 .../tests/goldenfiles/ty | 0 .../tests/goldenfiles/ty_level | 0 .../tests/infer.rs | 32 ++-- .../tests/normalize.rs | 12 +- .../tests/parse.rs | 6 +- .../tests/resugar.rs | 8 +- .../tests/support/mod.rs | 25 ++- .../Cargo.toml | 7 +- crates/pikelet-core/README.md | 10 ++ crates/pikelet-core/src/lib.rs | 14 ++ .../normalize.rs => pikelet-core/src/nbe.rs} | 110 +++++++------ .../src => pikelet-core/src/syntax}/core.rs | 4 +- .../src => pikelet-core/src/syntax}/domain.rs | 4 +- .../lib.rs => pikelet-core/src/syntax/mod.rs} | 52 +++---- crates/pikelet-driver/Cargo.toml | 4 +- crates/pikelet-driver/src/lib.rs | 146 +++++++++--------- crates/pikelet-elaborate/README.md | 7 - crates/pikelet-repl/Cargo.toml | 3 +- crates/pikelet-repl/src/lib.rs | 9 +- crates/pikelet-syntax/README.md | 11 -- crates/pikelet-syntax/src/translation/mod.rs | 7 - 45 files changed, 412 insertions(+), 343 deletions(-) rename crates/{pikelet-syntax => pikelet-concrete}/Cargo.toml (87%) create mode 100644 crates/pikelet-concrete/README.md rename crates/{pikelet-syntax => pikelet-concrete}/build.rs (100%) rename crates/{pikelet-syntax/src/translation => pikelet-concrete/src}/desugar.rs (99%) rename crates/{pikelet-elaborate/src => pikelet-concrete/src/elaborate}/context.rs (97%) rename crates/{pikelet-elaborate/src => pikelet-concrete/src/elaborate}/errors.rs (92%) rename crates/{pikelet-elaborate/src/lib.rs => pikelet-concrete/src/elaborate/mod.rs} (95%) create mode 100644 crates/pikelet-concrete/src/lib.rs rename crates/{pikelet-syntax => pikelet-concrete}/src/parse/errors.rs (100%) rename crates/{pikelet-syntax => pikelet-concrete}/src/parse/grammar.lalrpop (98%) rename crates/{pikelet-syntax => pikelet-concrete}/src/parse/lexer.rs (100%) rename crates/{pikelet-syntax => pikelet-concrete}/src/parse/mod.rs (98%) rename crates/{pikelet-syntax/src/translation => pikelet-concrete/src}/resugar.rs (98%) rename crates/{pikelet-syntax/src => pikelet-concrete/src/syntax}/concrete.rs (99%) create mode 100644 crates/pikelet-concrete/src/syntax/mod.rs rename crates/{pikelet-syntax/src => pikelet-concrete/src/syntax}/raw.rs (99%) rename crates/{pikelet-elaborate => pikelet-concrete}/tests/check.rs (92%) rename crates/{pikelet-syntax => pikelet-concrete}/tests/desugar.rs (97%) rename crates/{pikelet-syntax => pikelet-concrete}/tests/goldenfiles/ann (100%) rename crates/{pikelet-syntax => pikelet-concrete}/tests/goldenfiles/ann_ann_ann (100%) rename crates/{pikelet-syntax => pikelet-concrete}/tests/goldenfiles/ann_ann_left (100%) rename crates/{pikelet-syntax => pikelet-concrete}/tests/goldenfiles/ann_ann_right (100%) rename crates/{pikelet-syntax => pikelet-concrete}/tests/goldenfiles/ty (100%) rename crates/{pikelet-syntax => pikelet-concrete}/tests/goldenfiles/ty_level (100%) rename crates/{pikelet-elaborate => pikelet-concrete}/tests/infer.rs (96%) rename crates/{pikelet-elaborate => pikelet-concrete}/tests/normalize.rs (97%) rename crates/{pikelet-syntax => pikelet-concrete}/tests/parse.rs (94%) rename crates/{pikelet-syntax => pikelet-concrete}/tests/resugar.rs (98%) rename crates/{pikelet-elaborate => pikelet-concrete}/tests/support/mod.rs (73%) rename crates/{pikelet-elaborate => pikelet-core}/Cargo.toml (76%) create mode 100644 crates/pikelet-core/README.md create mode 100644 crates/pikelet-core/src/lib.rs rename crates/{pikelet-elaborate/src/normalize.rs => pikelet-core/src/nbe.rs} (70%) rename crates/{pikelet-syntax/src => pikelet-core/src/syntax}/core.rs (99%) rename crates/{pikelet-syntax/src => pikelet-core/src/syntax}/domain.rs (98%) rename crates/{pikelet-syntax/src/lib.rs => pikelet-core/src/syntax/mod.rs} (90%) delete mode 100644 crates/pikelet-elaborate/README.md delete mode 100644 crates/pikelet-syntax/README.md delete mode 100644 crates/pikelet-syntax/src/translation/mod.rs diff --git a/Cargo.toml b/Cargo.toml index 8ef0dfcb5..50105b832 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -1,10 +1,10 @@ [workspace] members = [ "./crates/pikelet", + "./crates/pikelet-concrete", + "./crates/pikelet-core", "./crates/pikelet-driver", - "./crates/pikelet-elaborate", "./crates/pikelet-language-server", "./crates/pikelet-library", "./crates/pikelet-repl", - "./crates/pikelet-syntax", ] diff --git a/crates/README.md b/crates/README.md index a5d40cc78..ddb812b18 100644 --- a/crates/README.md +++ b/crates/README.md @@ -19,14 +19,14 @@ your stay! ### Compiler -| Name | Description | -|-----------------------------|---------------------------------------------------------| -| [`pikelet-driver`] | Main entry-point for the compiler pipeline | -| [`pikelet-library`] | Builtin libraries | -| [`pikelet-syntax`] | Parsing, ASTs, pretty printing, and desugaring | -| [`pikelet-elaborate`] | Type checking, normalization, and elaboration of terms | +| Name | Description | +|-----------------------------|-------------------------------------------------------------------| +| [`pikelet-driver`] | Main entry-point for the compiler pipeline | +| [`pikelet-library`] | Builtin libraries | +| [`pikelet-concrete`] | Parsing, pretty printing, and elaboration of the concrete syntax | +| [`pikelet-core`] | Normalization-by-evaluation and checking of the core language | [`pikelet-driver`]: /crates/pikelet-driver [`pikelet-library`]: /crates/pikelet-library -[`pikelet-syntax`]: /crates/pikelet-syntax -[`pikelet-elaborate`]: /crates/pikelet-elaborate +[`pikelet-concrete`]: /crates/pikelet-concrete +[`pikelet-core`]: /crates/pikelet-core diff --git a/crates/pikelet-syntax/Cargo.toml b/crates/pikelet-concrete/Cargo.toml similarity index 87% rename from crates/pikelet-syntax/Cargo.toml rename to crates/pikelet-concrete/Cargo.toml index c5dfe8627..5ff60925f 100644 --- a/crates/pikelet-syntax/Cargo.toml +++ b/crates/pikelet-concrete/Cargo.toml @@ -1,5 +1,5 @@ [package] -name = "pikelet-syntax" +name = "pikelet-concrete" version = "0.1.0" license = "Apache-2.0" readme = "README.md" @@ -15,6 +15,7 @@ failure = "0.1.2" im = "12.2.0" lalrpop-util = "0.16.0" moniker = { version = "0.5.0", features = ["codespan", "im"] } +pikelet-core = { version = "0.1.0", path = "../pikelet-core" } pretty = { version = "0.5.2", features = ["termcolor"] } unicode-xid = "0.1.0" diff --git a/crates/pikelet-concrete/README.md b/crates/pikelet-concrete/README.md new file mode 100644 index 000000000..91ee093b8 --- /dev/null +++ b/crates/pikelet-concrete/README.md @@ -0,0 +1,17 @@ +# Pikelet Concrete Syntax + +This crate is responsible for: + +- defining data structures for: + - concrete terms + - raw terms +- parsing the concrete syntax +- pretty printing +- desugaring from the concrete syntax +- resugaring to the concrete syntax +- bidirectional elaboration, involving: + - bidirectional type checking + - passing implicit arguments explicitly (TODO) + - passing instance arguments explicitly (TODO) + - returning the fully explicit core syntax + diff --git a/crates/pikelet-syntax/build.rs b/crates/pikelet-concrete/build.rs similarity index 100% rename from crates/pikelet-syntax/build.rs rename to crates/pikelet-concrete/build.rs diff --git a/crates/pikelet-syntax/src/translation/desugar.rs b/crates/pikelet-concrete/src/desugar.rs similarity index 99% rename from crates/pikelet-syntax/src/translation/desugar.rs rename to crates/pikelet-concrete/src/desugar.rs index 3fb266f84..ce3e3051c 100644 --- a/crates/pikelet-syntax/src/translation/desugar.rs +++ b/crates/pikelet-concrete/src/desugar.rs @@ -3,9 +3,10 @@ use codespan_reporting::{Diagnostic, Label as DiagnosticLabel}; use im; use moniker::{Binder, Embed, FreeVar, Nest, Scope, Var}; -use concrete; -use raw; -use {Label, Level, LevelShift}; +use pikelet_core::syntax::{Label, Level, LevelShift}; + +use syntax::concrete; +use syntax::raw; /// The environment used when desugaring from the concrete to raw syntax #[derive(Debug, Clone)] @@ -388,7 +389,7 @@ fn desugar_record_intro( span: ByteSpan, fields: &[concrete::RecordIntroField], ) -> Result { - use concrete::RecordIntroField; + use syntax::concrete::RecordIntroField; let mut env = env.clone(); diff --git a/crates/pikelet-elaborate/src/context.rs b/crates/pikelet-concrete/src/elaborate/context.rs similarity index 97% rename from crates/pikelet-elaborate/src/context.rs rename to crates/pikelet-concrete/src/elaborate/context.rs index 85ac0a936..2f25de9de 100644 --- a/crates/pikelet-elaborate/src/context.rs +++ b/crates/pikelet-concrete/src/elaborate/context.rs @@ -1,12 +1,14 @@ use im; use moniker::{Binder, FreeVar, Var}; -use std::fmt; use std::rc::Rc; -use pikelet_syntax::core::{Literal, RcTerm}; -use pikelet_syntax::domain::{RcType, RcValue, Value}; -use pikelet_syntax::translation::{Resugar, ResugarEnv}; -use pikelet_syntax::{FloatFormat, IntFormat}; +use pikelet_core::nbe; +use pikelet_core::syntax::core::{Literal, RcTerm}; +use pikelet_core::syntax::domain::{RcType, RcValue, Value}; +use pikelet_core::syntax::Import; +use pikelet_core::syntax::{FloatFormat, IntFormat}; + +use resugar::{Resugar, ResugarEnv}; // Some helper traits for marshalling between Rust and Pikelet values // @@ -177,22 +179,6 @@ impl TryFromValueRef for f64 { } } -/// Imported definitions -#[derive(Clone)] -pub enum Import { - Term(RcTerm), - Prim(for<'a> fn(&'a [RcValue]) -> Option), -} - -impl fmt::Debug for Import { - fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { - match *self { - Import::Term(ref term) => f.debug_tuple("Term").field(term).finish(), - Import::Prim(_) => f.debug_tuple("Prim").field(&"|params| { .. }").finish(), - } - } -} - #[derive(Clone, Debug)] pub struct Globals { ty_bool: RcType, @@ -240,7 +226,7 @@ impl Default for Context { fn default() -> Context { use moniker::{Embed, Scope}; - use pikelet_syntax::core::Term; + use pikelet_core::syntax::core::Term; let var_bool = FreeVar::fresh_named("Bool"); let var_true = FreeVar::fresh_named("true"); @@ -554,7 +540,7 @@ impl Context { } pub fn array<'a>(&self, ty: &'a RcType) -> Option<(u64, &'a RcType)> { - use pikelet_syntax::LevelShift; + use pikelet_core::syntax::LevelShift; match ty.free_var_app() { // Conservatively forcing the shift to be zero for now. Perhaps this @@ -595,3 +581,13 @@ impl Context { self.definitions.insert(free_var, term); } } + +impl nbe::Env for Context { + fn get_import(&self, name: &str) -> Option<&Import> { + self.imports.get(name).map(|&(ref import, _)| import) + } + + fn get_definition(&self, free_var: &FreeVar) -> Option<&RcTerm> { + self.definitions.get(free_var) + } +} diff --git a/crates/pikelet-elaborate/src/errors.rs b/crates/pikelet-concrete/src/elaborate/errors.rs similarity index 92% rename from crates/pikelet-elaborate/src/errors.rs rename to crates/pikelet-concrete/src/elaborate/errors.rs index f68818fa7..20e1ae69c 100644 --- a/crates/pikelet-elaborate/src/errors.rs +++ b/crates/pikelet-concrete/src/elaborate/errors.rs @@ -4,7 +4,10 @@ use codespan::ByteSpan; use codespan_reporting::{Diagnostic, Label}; use moniker::{Binder, FreeVar, Var}; -use pikelet_syntax::{self, concrete, raw}; +use pikelet_core::nbe::NbeError; +use pikelet_core::syntax; + +use syntax::{concrete, raw}; /// An internal error. These are bugs! #[derive(Debug, Fail, Clone, PartialEq)] @@ -14,19 +17,19 @@ pub enum InternalError { span: Option, var: Var, }, - #[fail(display = "Argument applied to non-function.")] - ArgumentAppliedToNonFunction, - #[fail(display = "Expected a boolean expression.")] - ExpectedBoolExpr, - #[fail(display = "Projected on non-existent field `{}`.", label)] - ProjectedOnNonExistentField { label: pikelet_syntax::Label }, - #[fail(display = "No patterns matched the given expression.")] - NoPatternsApplicable, #[fail(display = "not yet implemented: {}", message)] Unimplemented { span: Option, message: String, }, + #[fail(display = "nbe: {}", _0)] + Nbe(#[cause] NbeError), +} + +impl From for InternalError { + fn from(src: NbeError) -> InternalError { + InternalError::Nbe(src) + } } impl InternalError { @@ -41,16 +44,6 @@ impl InternalError { ), } }, - InternalError::ArgumentAppliedToNonFunction => { - Diagnostic::new_bug("argument applied to non-function") - }, - InternalError::ExpectedBoolExpr => Diagnostic::new_bug("expected a boolean expression"), - InternalError::ProjectedOnNonExistentField { ref label } => { - Diagnostic::new_bug(format!("projected on non-existent field `{}`.", label)) - }, - InternalError::NoPatternsApplicable => { - Diagnostic::new_bug("no patterns matched the given expression") - }, InternalError::Unimplemented { span, ref message } => { let base = Diagnostic::new_bug(format!("not yet implemented: {}", message)); match span { @@ -61,6 +54,9 @@ impl InternalError { ), } }, + InternalError::Nbe(ref nbe_error) => { + Diagnostic::new_bug(format!("failed to normalize: {}", nbe_error)) + }, } } } @@ -161,8 +157,8 @@ pub enum TypeError { )] LabelMismatch { span: ByteSpan, - found: pikelet_syntax::Label, - expected: pikelet_syntax::Label, + found: syntax::Label, + expected: syntax::Label, }, #[fail( display = "Mismatched array length: expected {} elements but found {}", @@ -181,7 +177,7 @@ pub enum TypeError { )] NoFieldInType { label_span: ByteSpan, - expected_label: pikelet_syntax::Label, + expected_label: syntax::Label, found: Box, }, #[fail( @@ -393,3 +389,9 @@ impl From for TypeError { TypeError::Internal(src) } } + +impl From for TypeError { + fn from(src: NbeError) -> TypeError { + TypeError::from(InternalError::from(src)) + } +} diff --git a/crates/pikelet-elaborate/src/lib.rs b/crates/pikelet-concrete/src/elaborate/mod.rs similarity index 95% rename from crates/pikelet-elaborate/src/lib.rs rename to crates/pikelet-concrete/src/elaborate/mod.rs index bd37380a3..c8f3f979f 100644 --- a/crates/pikelet-elaborate/src/lib.rs +++ b/crates/pikelet-concrete/src/elaborate/mod.rs @@ -4,29 +4,21 @@ //! //! For more information, check out the theory appendix of the Pikelet book. -extern crate codespan; -extern crate codespan_reporting; -#[macro_use] -extern crate failure; -extern crate im; -extern crate moniker; -extern crate pikelet_syntax; - use codespan::ByteSpan; use moniker::{Binder, BoundPattern, BoundTerm, Embed, FreeVar, Nest, Scope, Var}; -use pikelet_syntax::core::{Literal, Pattern, RcPattern, RcTerm, Term}; -use pikelet_syntax::domain::{RcType, RcValue, Value}; -use pikelet_syntax::raw; -use pikelet_syntax::Level; +use pikelet_core::nbe; +use pikelet_core::syntax::core::{Literal, Pattern, RcPattern, RcTerm, Term}; +use pikelet_core::syntax::domain::{RcType, RcValue, Value}; +use pikelet_core::syntax::Level; + +use syntax::raw; mod context; mod errors; -mod normalize; -pub use self::context::{Context, Globals, Import}; +pub use self::context::{Context, Globals}; pub use self::errors::{InternalError, TypeError}; -pub use self::normalize::{match_value, nf_term}; /// Returns true if `ty1` is a subtype of `ty2` fn is_subtype(context: &Context, ty1: &RcType, ty2: &RcType) -> bool { @@ -98,8 +90,8 @@ fn check_literal( raw_literal: &raw::Literal, expected_ty: &RcType, ) -> Result { - use pikelet_syntax::core::Literal::*; - use pikelet_syntax::FloatFormat::Dec as FloatDec; + use pikelet_core::syntax::core::Literal::*; + use pikelet_core::syntax::FloatFormat::Dec as FloatDec; let ty = expected_ty; match *raw_literal { @@ -134,7 +126,7 @@ fn infer_literal( context: &Context, raw_literal: &raw::Literal, ) -> Result<(Literal, RcType), TypeError> { - use pikelet_syntax::core::Literal::{Char, String}; + use pikelet_core::syntax::core::Literal::{Char, String}; match *raw_literal { raw::Literal::String(_, ref val) => Ok((String(val.clone()), context.string().clone())), @@ -186,7 +178,7 @@ pub fn infer_pattern( match *raw_pattern.inner { raw::Pattern::Ann(ref raw_pattern, Embed(ref raw_ty)) => { let (ty, _) = infer_universe(context, raw_ty)?; - let value_ty = nf_term(context, &ty)?; + let value_ty = nbe::nf_term(context, &ty)?; let (pattern, declarations) = check_pattern(context, raw_pattern, &value_ty)?; Ok(( @@ -304,7 +296,7 @@ pub fn check_term( let (ty_label, Binder(ty_free_var), Embed(ann)) = ty_field; if label == ty_label { - let ann = nf_term(context, &ann.substs(&mappings))?; + 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))) @@ -404,7 +396,7 @@ pub fn infer_term( // I-ANN raw::Term::Ann(ref raw_expr, ref raw_ty) => { let (ty, _) = infer_universe(context, raw_ty)?; - let value_ty = nf_term(context, &ty)?; + let value_ty = nbe::nf_term(context, &ty)?; let expr = check_term(context, raw_expr, &value_ty)?; Ok((RcTerm::from(Term::Ann(expr, ty)), value_ty)) @@ -465,7 +457,7 @@ pub fn infer_term( let (ann, ann_level) = infer_universe(context, &raw_ann)?; let (body, body_level) = { - let ann = nf_term(context, &ann)?; + let ann = nbe::nf_term(context, &ann)?; let mut body_context = context.clone(); body_context.insert_declaration(free_var.clone(), ann); infer_universe(&body_context, &raw_body)? @@ -493,7 +485,7 @@ pub fn infer_term( } let (fun_ann, _) = infer_universe(context, &raw_ann)?; - let fun_ty_ann = nf_term(context, &fun_ann)?; + let fun_ty_ann = nbe::nf_term(context, &fun_ann)?; let (fun_body, fun_ty_body) = { let mut body_context = context.clone(); body_context.insert_declaration(free_var.clone(), fun_ty_ann.clone()); @@ -524,7 +516,7 @@ pub fn infer_term( (term, RcTerm::from(&*ann_value.inner), ann_value) } else { let (ann, _) = infer_universe(&context, &raw_ann)?; - let ann_value = nf_term(&context, &ann)?; + let ann_value = nbe::nf_term(&context, &ann)?; (check_term(&context, &raw_term, &ann_value)?, ann, ann_value) }; @@ -553,7 +545,7 @@ pub fn infer_term( let ((Binder(free_var), Embed(ann)), body) = scope.clone().unbind(); let arg = check_term(context, raw_arg, &ann)?; - let body = nf_term(context, &body.substs(&[(free_var, arg.clone())]))?; + let body = nbe::nf_term(context, &body.substs(&[(free_var, arg.clone())]))?; Ok((RcTerm::from(Term::FunApp(head, arg)), body)) }, @@ -578,7 +570,7 @@ pub fn infer_term( .into_iter() .map(|(label, Binder(free_var), Embed(raw_ann))| { let (ann, ann_level) = infer_universe(&context, &raw_ann)?; - let nf_ann = nf_term(&context, &ann)?; + let nf_ann = nbe::nf_term(&context, &ann)?; max_level = cmp::max(max_level, ann_level); context.insert_declaration(free_var.clone(), nf_ann); @@ -607,7 +599,7 @@ pub fn infer_term( let mut ty_mappings = Vec::with_capacity(raw_fields.len()); for (label, Binder(free_var), Embed(raw_term)) in raw_fields { let (term, term_ty) = infer_term(context, &raw_term)?; - let term_ty = nf_term(context, &term_ty.substs(&ty_mappings))?; + 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))); @@ -632,7 +624,7 @@ pub fn infer_term( for (current_label, Binder(free_var), Embed(current_ann)) in fields.unnest() { if current_label == *label { let expr = RcTerm::from(Term::RecordProj(expr, current_label, shift)); - let mut ty = nf_term(context, ¤t_ann.substs(&mappings))?; + let mut ty = nbe::nf_term(context, ¤t_ann.substs(&mappings))?; ty.shift_universes(shift); return Ok((expr, ty)); diff --git a/crates/pikelet-concrete/src/lib.rs b/crates/pikelet-concrete/src/lib.rs new file mode 100644 index 000000000..b3e1e4b95 --- /dev/null +++ b/crates/pikelet-concrete/src/lib.rs @@ -0,0 +1,22 @@ +//! The syntax of the language + +extern crate codespan; +extern crate codespan_reporting; +#[macro_use] +extern crate failure; +extern crate im; +extern crate lalrpop_util; +#[macro_use] +extern crate moniker; +extern crate pikelet_core; +#[cfg(test)] +#[macro_use] +extern crate pretty_assertions; +extern crate pretty; +extern crate unicode_xid; + +pub mod desugar; +pub mod elaborate; +pub mod parse; +pub mod resugar; +pub mod syntax; diff --git a/crates/pikelet-syntax/src/parse/errors.rs b/crates/pikelet-concrete/src/parse/errors.rs similarity index 100% rename from crates/pikelet-syntax/src/parse/errors.rs rename to crates/pikelet-concrete/src/parse/errors.rs diff --git a/crates/pikelet-syntax/src/parse/grammar.lalrpop b/crates/pikelet-concrete/src/parse/grammar.lalrpop similarity index 98% rename from crates/pikelet-syntax/src/parse/grammar.lalrpop rename to crates/pikelet-concrete/src/parse/grammar.lalrpop index a341e4af6..519359f23 100644 --- a/crates/pikelet-syntax/src/parse/grammar.lalrpop +++ b/crates/pikelet-concrete/src/parse/grammar.lalrpop @@ -1,9 +1,10 @@ use codespan::FileMap; use codespan::{ByteIndex, ByteSpan}; -use concrete::{Item, Literal, Pattern, Term, RecordTypeField, RecordIntroField, ReplCommand}; +use pikelet_core::syntax::{FloatFormat, IntFormat}; + use parse::{LalrpopError, ParseError, Token}; -use {FloatFormat, IntFormat}; +use syntax::concrete::{Item, Literal, Pattern, Term, RecordTypeField, RecordIntroField, ReplCommand}; #[LALR] grammar<'err, 'input>( diff --git a/crates/pikelet-syntax/src/parse/lexer.rs b/crates/pikelet-concrete/src/parse/lexer.rs similarity index 100% rename from crates/pikelet-syntax/src/parse/lexer.rs rename to crates/pikelet-concrete/src/parse/lexer.rs diff --git a/crates/pikelet-syntax/src/parse/mod.rs b/crates/pikelet-concrete/src/parse/mod.rs similarity index 98% rename from crates/pikelet-syntax/src/parse/mod.rs rename to crates/pikelet-concrete/src/parse/mod.rs index 666b98647..8f304ddb2 100644 --- a/crates/pikelet-syntax/src/parse/mod.rs +++ b/crates/pikelet-concrete/src/parse/mod.rs @@ -3,8 +3,8 @@ use codespan::{ByteIndex, ByteSpan, FileMap}; use lalrpop_util::ParseError as LalrpopError; -use concrete; use parse::lexer::Lexer; +use syntax::concrete; mod errors; mod lexer; @@ -50,7 +50,7 @@ fn reparse_fun_ty_hack( binder: concrete::Term, body: concrete::Term, ) -> Result> { - use concrete::Term; + use syntax::concrete::Term; fn fun_ty_binder( binder: &Term, diff --git a/crates/pikelet-syntax/src/translation/resugar.rs b/crates/pikelet-concrete/src/resugar.rs similarity index 98% rename from crates/pikelet-syntax/src/translation/resugar.rs rename to crates/pikelet-concrete/src/resugar.rs index 451860052..27bef7c2d 100644 --- a/crates/pikelet-syntax/src/translation/resugar.rs +++ b/crates/pikelet-concrete/src/resugar.rs @@ -2,10 +2,10 @@ use codespan::{ByteIndex, ByteSpan}; use im; use moniker::{Binder, BoundTerm, Embed, FreeVar, Nest, Scope, Var}; -use concrete; -use core; -use domain; -use {Label, Level, LevelShift}; +use pikelet_core::syntax::{core, domain}; +use pikelet_core::syntax::{Label, Level, LevelShift}; + +use syntax::concrete; /// The environment used when resugaring from the core to the concrete syntax #[derive(Debug, Clone)] @@ -156,9 +156,9 @@ fn resugar_pattern( panic!("Tried to convert a term that was not locally closed"); }, core::Pattern::Literal(ref literal) => { - use concrete::Literal::*; - use concrete::Pattern; - use concrete::Pattern::Literal; + use syntax::concrete::Literal::*; + use syntax::concrete::Pattern; + use syntax::concrete::Pattern::Literal; let span = ByteSpan::default(); @@ -446,9 +446,9 @@ fn resugar_term(env: &ResugarEnv, term: &core::Term, prec: Prec) -> concrete::Te ) }, core::Term::Literal(ref literal) => { - use concrete::Literal::*; - use concrete::Term; - use concrete::Term::Literal; + use syntax::concrete::Literal::*; + use syntax::concrete::Term; + use syntax::concrete::Term::Literal; let span = ByteSpan::default(); diff --git a/crates/pikelet-syntax/src/concrete.rs b/crates/pikelet-concrete/src/syntax/concrete.rs similarity index 99% rename from crates/pikelet-syntax/src/concrete.rs rename to crates/pikelet-concrete/src/syntax/concrete.rs index b799496ee..00a89f50c 100644 --- a/crates/pikelet-syntax/src/concrete.rs +++ b/crates/pikelet-concrete/src/syntax/concrete.rs @@ -4,7 +4,9 @@ use codespan::{ByteIndex, ByteSpan}; use pretty::{BoxDoc, Doc}; use std::fmt; -use {FloatFormat, IntFormat, PRETTY_FALLBACK_WIDTH, PRETTY_INDENT_WIDTH}; +use pikelet_core::syntax::{FloatFormat, IntFormat}; + +use syntax::{PRETTY_FALLBACK_WIDTH, PRETTY_INDENT_WIDTH}; /// Commands entered in the REPL #[derive(Debug, Clone)] diff --git a/crates/pikelet-concrete/src/syntax/mod.rs b/crates/pikelet-concrete/src/syntax/mod.rs new file mode 100644 index 000000000..6340f9c8b --- /dev/null +++ b/crates/pikelet-concrete/src/syntax/mod.rs @@ -0,0 +1,11 @@ +pub mod concrete; +pub mod raw; + +const PRETTY_INDENT_WIDTH: usize = 4; + +/// An effectively 'infinite' line length for when we don't have an explicit +/// width provided for pretty printing. +/// +/// `pretty.rs` seems to bug-out and break on every line when using +/// `usize::MAX`, so we'll just use a really big number instead... +pub const PRETTY_FALLBACK_WIDTH: usize = 1_000_000; diff --git a/crates/pikelet-syntax/src/raw.rs b/crates/pikelet-concrete/src/syntax/raw.rs similarity index 99% rename from crates/pikelet-syntax/src/raw.rs rename to crates/pikelet-concrete/src/syntax/raw.rs index 1ea4464ea..f3e9b2a61 100644 --- a/crates/pikelet-syntax/src/raw.rs +++ b/crates/pikelet-concrete/src/syntax/raw.rs @@ -8,7 +8,9 @@ use std::fmt; use std::ops; use std::rc::Rc; -use {FloatFormat, IntFormat, Label, Level, LevelShift, PRETTY_FALLBACK_WIDTH}; +use pikelet_core::syntax::{FloatFormat, IntFormat, Label, Level, LevelShift}; + +use syntax::PRETTY_FALLBACK_WIDTH; /// Literals #[derive(Debug, Clone, PartialEq, PartialOrd, BoundTerm, BoundPattern)] diff --git a/crates/pikelet-elaborate/tests/check.rs b/crates/pikelet-concrete/tests/check.rs similarity index 92% rename from crates/pikelet-elaborate/tests/check.rs rename to crates/pikelet-concrete/tests/check.rs index 706860c20..302ddd629 100644 --- a/crates/pikelet-elaborate/tests/check.rs +++ b/crates/pikelet-concrete/tests/check.rs @@ -1,13 +1,13 @@ extern crate codespan; extern crate codespan_reporting; extern crate moniker; -extern crate pikelet_elaborate; -extern crate pikelet_syntax; +extern crate pikelet_concrete; +extern crate pikelet_core; use codespan::CodeMap; -use pikelet_elaborate::{Context, TypeError}; -use pikelet_syntax::translation::{Desugar, DesugarEnv}; +use pikelet_concrete::desugar::{Desugar, DesugarEnv}; +use pikelet_concrete::elaborate::{self, Context, TypeError}; mod support; @@ -37,7 +37,7 @@ fn record_intro_field_mismatch_lt() { .desugar(&desugar_env) .unwrap(); - match pikelet_elaborate::check_term(&context, &raw_term, &expected_ty) { + match elaborate::check_term(&context, &raw_term, &expected_ty) { Err(TypeError::RecordSizeMismatch { .. }) => {}, Err(err) => panic!("unexpected error: {:?}", err), Ok(term) => panic!("expected error but found: {}", term), @@ -58,7 +58,7 @@ fn record_intro_field_mismatch_gt() { .desugar(&desugar_env) .unwrap(); - match pikelet_elaborate::check_term(&context, &raw_term, &expected_ty) { + match elaborate::check_term(&context, &raw_term, &expected_ty) { Err(TypeError::RecordSizeMismatch { .. }) => {}, Err(err) => panic!("unexpected error: {:?}", err), Ok(term) => panic!("expected error but found: {}", term), @@ -122,7 +122,7 @@ fn case_expr_bad_literal() { .desugar(&desugar_env) .unwrap(); - match pikelet_elaborate::check_term(&context, &raw_term, &expected_ty) { + match elaborate::check_term(&context, &raw_term, &expected_ty) { Err(TypeError::LiteralMismatch { .. }) => {}, Err(err) => panic!("unexpected error: {:?}", err), Ok(term) => panic!("expected error but found: {}", term), @@ -193,7 +193,7 @@ fn array_intro_len_mismatch() { .desugar(&desugar_env) .unwrap(); - match pikelet_elaborate::check_term(&context, &raw_term, &expected_ty) { + match elaborate::check_term(&context, &raw_term, &expected_ty) { Err(TypeError::ArrayLengthMismatch { .. }) => {}, Err(err) => panic!("unexpected error: {:?}", err), Ok(term) => panic!("expected error but found: {}", term), @@ -214,7 +214,7 @@ fn array_intro_elem_ty_mismatch() { .desugar(&desugar_env) .unwrap(); - match pikelet_elaborate::check_term(&context, &raw_term, &expected_ty) { + match elaborate::check_term(&context, &raw_term, &expected_ty) { Err(_) => {}, Ok(term) => panic!("expected error but found: {}", term), } diff --git a/crates/pikelet-syntax/tests/desugar.rs b/crates/pikelet-concrete/tests/desugar.rs similarity index 97% rename from crates/pikelet-syntax/tests/desugar.rs rename to crates/pikelet-concrete/tests/desugar.rs index da25d319a..011813c17 100644 --- a/crates/pikelet-syntax/tests/desugar.rs +++ b/crates/pikelet-concrete/tests/desugar.rs @@ -5,7 +5,8 @@ extern crate im; #[macro_use] extern crate moniker; extern crate goldenfile; -extern crate pikelet_syntax; +extern crate pikelet_concrete; +extern crate pikelet_core; use codespan::{ByteSpan, CodeMap, FileName}; use codespan_reporting::termcolor::{ColorChoice, StandardStream}; @@ -13,9 +14,11 @@ use goldenfile::Mint; use moniker::{Binder, Embed, FreeVar, Scope, Var}; use std::io::Write; -use pikelet_syntax::raw::{RcTerm, Term}; -use pikelet_syntax::translation::{Desugar, DesugarEnv, DesugarError}; -use pikelet_syntax::{concrete, parse, raw, Level, LevelShift}; +use pikelet_concrete::desugar::{Desugar, DesugarEnv, DesugarError}; +use pikelet_concrete::parse; +use pikelet_concrete::syntax::raw::{RcTerm, Term}; +use pikelet_concrete::syntax::{concrete, raw}; +use pikelet_core::syntax::{Level, LevelShift}; fn golden(filename: &str, literal: &str) { let path = "tests/goldenfiles"; diff --git a/crates/pikelet-syntax/tests/goldenfiles/ann b/crates/pikelet-concrete/tests/goldenfiles/ann similarity index 100% rename from crates/pikelet-syntax/tests/goldenfiles/ann rename to crates/pikelet-concrete/tests/goldenfiles/ann diff --git a/crates/pikelet-syntax/tests/goldenfiles/ann_ann_ann b/crates/pikelet-concrete/tests/goldenfiles/ann_ann_ann similarity index 100% rename from crates/pikelet-syntax/tests/goldenfiles/ann_ann_ann rename to crates/pikelet-concrete/tests/goldenfiles/ann_ann_ann diff --git a/crates/pikelet-syntax/tests/goldenfiles/ann_ann_left b/crates/pikelet-concrete/tests/goldenfiles/ann_ann_left similarity index 100% rename from crates/pikelet-syntax/tests/goldenfiles/ann_ann_left rename to crates/pikelet-concrete/tests/goldenfiles/ann_ann_left diff --git a/crates/pikelet-syntax/tests/goldenfiles/ann_ann_right b/crates/pikelet-concrete/tests/goldenfiles/ann_ann_right similarity index 100% rename from crates/pikelet-syntax/tests/goldenfiles/ann_ann_right rename to crates/pikelet-concrete/tests/goldenfiles/ann_ann_right diff --git a/crates/pikelet-syntax/tests/goldenfiles/ty b/crates/pikelet-concrete/tests/goldenfiles/ty similarity index 100% rename from crates/pikelet-syntax/tests/goldenfiles/ty rename to crates/pikelet-concrete/tests/goldenfiles/ty diff --git a/crates/pikelet-syntax/tests/goldenfiles/ty_level b/crates/pikelet-concrete/tests/goldenfiles/ty_level similarity index 100% rename from crates/pikelet-syntax/tests/goldenfiles/ty_level rename to crates/pikelet-concrete/tests/goldenfiles/ty_level diff --git a/crates/pikelet-elaborate/tests/infer.rs b/crates/pikelet-concrete/tests/infer.rs similarity index 96% rename from crates/pikelet-elaborate/tests/infer.rs rename to crates/pikelet-concrete/tests/infer.rs index 8d09921ce..d8d65e6dd 100644 --- a/crates/pikelet-elaborate/tests/infer.rs +++ b/crates/pikelet-concrete/tests/infer.rs @@ -2,21 +2,21 @@ extern crate codespan; extern crate codespan_reporting; #[macro_use] extern crate moniker; -extern crate pikelet_elaborate; -extern crate pikelet_syntax; +extern crate pikelet_concrete; +extern crate pikelet_core; use codespan::{ByteIndex, ByteSpan, CodeMap}; use moniker::{FreeVar, Var}; -use pikelet_elaborate::{Context, TypeError}; -use pikelet_syntax::translation::{Desugar, DesugarEnv}; -use pikelet_syntax::{concrete, raw}; +use pikelet_concrete::desugar::{Desugar, DesugarEnv}; +use pikelet_concrete::elaborate::{self, Context, TypeError}; +use pikelet_concrete::syntax::{concrete, raw}; mod support; #[test] fn undefined_name() { - use pikelet_syntax::LevelShift; + use pikelet_core::syntax::LevelShift; let context = Context::default(); @@ -28,7 +28,7 @@ fn undefined_name() { )); assert_eq!( - pikelet_elaborate::infer_term(&context, &given_expr), + elaborate::infer_term(&context, &given_expr), Err(TypeError::UndefinedName { span: ByteSpan::default(), free_var: x.clone(), @@ -48,7 +48,7 @@ fn import_not_found() { .desugar(&desugar_env) .unwrap(); - match pikelet_elaborate::infer_term(&context, &raw_term) { + match elaborate::infer_term(&context, &raw_term) { Err(TypeError::UndefinedImport { .. }) => {}, Err(err) => panic!("unexpected error: {:?}", err), Ok((term, ty)) => panic!("expected error, found {} : {:?}", term, ty), @@ -123,7 +123,7 @@ fn ann_id_as_ty() { .desugar(&desugar_env) .unwrap(); - match pikelet_elaborate::infer_term(&context, &raw_term) { + match elaborate::infer_term(&context, &raw_term) { Err(TypeError::UnexpectedFunction { .. }) => {}, other => panic!("unexpected result: {:#?}", other), } @@ -156,7 +156,7 @@ fn fun_app_ty() { .unwrap(); assert_eq!( - pikelet_elaborate::infer_term(&context, &raw_term), + elaborate::infer_term(&context, &raw_term), Err(TypeError::ArgAppliedToNonFunction { fn_span: ByteSpan::new(ByteIndex(1), ByteIndex(5)), arg_span: ByteSpan::new(ByteIndex(6), ByteIndex(10)), @@ -486,7 +486,7 @@ fn let_shift_universes_literals_bad() { .desugar(&desugar_env) .unwrap(); - match pikelet_elaborate::infer_term(&context, &raw_term) { + match elaborate::infer_term(&context, &raw_term) { Ok(_) => panic!("expected error"), Err(TypeError::LiteralMismatch { .. }) => {}, Err(err) => panic!("unexpected error: {}", err), @@ -513,7 +513,7 @@ fn let_shift_universes_too_little() { .desugar(&desugar_env) .unwrap(); - match pikelet_elaborate::infer_term(&context, &raw_term) { + match elaborate::infer_term(&context, &raw_term) { Ok(_) => panic!("expected error"), Err(TypeError::Mismatch { .. }) => {}, Err(err) => panic!("unexpected error: {}", err), @@ -588,7 +588,7 @@ fn case_expr_bool_bad() { .desugar(&desugar_env) .unwrap(); - match pikelet_elaborate::infer_term(&context, &raw_term) { + match elaborate::infer_term(&context, &raw_term) { Err(TypeError::Mismatch { .. }) => {}, Err(err) => panic!("unexpected error: {:?}", err), Ok((term, ty)) => panic!("expected error, found {} : {:?}", term, ty), @@ -623,7 +623,7 @@ fn case_expr_empty() { .desugar(&desugar_env) .unwrap(); - match pikelet_elaborate::infer_term(&context, &raw_term) { + match elaborate::infer_term(&context, &raw_term) { Err(TypeError::AmbiguousEmptyCase { .. }) => {}, other => panic!("unexpected result: {:#?}", other), } @@ -819,7 +819,7 @@ fn record_proj_missing() { .desugar(&desugar_env) .unwrap(); - match pikelet_elaborate::infer_term(&context, &raw_term) { + match elaborate::infer_term(&context, &raw_term) { Err(TypeError::NoFieldInType { .. }) => {}, x => panic!("expected a field lookup error, found {:?}", x), } @@ -896,7 +896,7 @@ fn array_intro_ambiguous() { .desugar(&desugar_env) .unwrap(); - match pikelet_elaborate::infer_term(&context, &raw_term) { + match elaborate::infer_term(&context, &raw_term) { Err(TypeError::AmbiguousArrayLiteral { .. }) => {}, Err(err) => panic!("unexpected error: {:?}", err), Ok((term, ty)) => panic!("expected error, found {} : {:?}", term, ty), diff --git a/crates/pikelet-elaborate/tests/normalize.rs b/crates/pikelet-concrete/tests/normalize.rs similarity index 97% rename from crates/pikelet-elaborate/tests/normalize.rs rename to crates/pikelet-concrete/tests/normalize.rs index 37e0d2ab9..800daf855 100644 --- a/crates/pikelet-elaborate/tests/normalize.rs +++ b/crates/pikelet-concrete/tests/normalize.rs @@ -2,15 +2,15 @@ extern crate codespan; extern crate codespan_reporting; #[macro_use] extern crate moniker; -extern crate pikelet_elaborate; -extern crate pikelet_syntax; +extern crate pikelet_concrete; +extern crate pikelet_core; use codespan::CodeMap; use moniker::{Binder, Embed, FreeVar, Scope, Var}; -use pikelet_elaborate::Context; -use pikelet_syntax::core::{RcTerm, Term}; -use pikelet_syntax::domain::{Neutral, RcNeutral, RcValue, Value}; +use pikelet_concrete::elaborate::Context; +use pikelet_core::syntax::core::{RcTerm, Term}; +use pikelet_core::syntax::domain::{Neutral, RcNeutral, RcValue, Value}; mod support; @@ -22,7 +22,7 @@ fn var() { let var = RcTerm::from(Term::var(Var::Free(x.clone()), 0)); assert_eq!( - pikelet_elaborate::nf_term(&context, &var).unwrap(), + pikelet_core::nbe::nf_term(&context, &var).unwrap(), RcValue::from(Value::var(Var::Free(x), 0)), ); } diff --git a/crates/pikelet-syntax/tests/parse.rs b/crates/pikelet-concrete/tests/parse.rs similarity index 94% rename from crates/pikelet-syntax/tests/parse.rs rename to crates/pikelet-concrete/tests/parse.rs index d25f4de05..450201406 100644 --- a/crates/pikelet-syntax/tests/parse.rs +++ b/crates/pikelet-concrete/tests/parse.rs @@ -1,10 +1,10 @@ extern crate codespan; -extern crate pikelet_syntax; +extern crate pikelet_concrete; use codespan::{ByteIndex, ByteSpan}; use codespan::{CodeMap, FileName}; -use pikelet_syntax::concrete; -use pikelet_syntax::parse::{self, LexerError, ParseError}; +use pikelet_concrete::parse::{self, LexerError, ParseError}; +use pikelet_concrete::syntax::concrete; #[test] fn imports() { diff --git a/crates/pikelet-syntax/tests/resugar.rs b/crates/pikelet-concrete/tests/resugar.rs similarity index 98% rename from crates/pikelet-syntax/tests/resugar.rs rename to crates/pikelet-concrete/tests/resugar.rs index 09ced7460..1d5209718 100644 --- a/crates/pikelet-syntax/tests/resugar.rs +++ b/crates/pikelet-concrete/tests/resugar.rs @@ -1,12 +1,14 @@ extern crate codespan; extern crate moniker; -extern crate pikelet_syntax; +extern crate pikelet_concrete; +extern crate pikelet_core; use codespan::{ByteIndex, ByteSpan}; use moniker::{Binder, Embed, FreeVar, Nest, Scope, Var}; -use pikelet_syntax::translation::{Resugar, ResugarEnv}; -use pikelet_syntax::{concrete, core, Label, LevelShift}; +use pikelet_concrete::resugar::{Resugar, ResugarEnv}; +use pikelet_concrete::syntax::concrete; +use pikelet_core::syntax::{core, Label, LevelShift}; fn span() -> ByteSpan { ByteSpan::default() diff --git a/crates/pikelet-elaborate/tests/support/mod.rs b/crates/pikelet-concrete/tests/support/mod.rs similarity index 73% rename from crates/pikelet-elaborate/tests/support/mod.rs rename to crates/pikelet-concrete/tests/support/mod.rs index 47e0fef0a..2e832d1c9 100644 --- a/crates/pikelet-elaborate/tests/support/mod.rs +++ b/crates/pikelet-concrete/tests/support/mod.rs @@ -4,12 +4,13 @@ use codespan::{CodeMap, FileName}; use codespan_reporting; use codespan_reporting::termcolor::{ColorChoice, StandardStream}; -use pikelet_elaborate::{self, Context}; -use pikelet_syntax::concrete; -use pikelet_syntax::core::RcTerm; -use pikelet_syntax::domain::{RcType, RcValue}; -use pikelet_syntax::parse; -use pikelet_syntax::translation::{Desugar, DesugarEnv}; +use pikelet_concrete::desugar::{Desugar, DesugarEnv}; +use pikelet_concrete::elaborate::{self, Context}; +use pikelet_concrete::parse; +use pikelet_concrete::syntax::concrete; +use pikelet_core::nbe; +use pikelet_core::syntax::core::RcTerm; +use pikelet_core::syntax::domain::{RcType, RcValue}; pub fn parse_term(codemap: &mut CodeMap, src: &str) -> concrete::Term { let filemap = codemap.add_filemap(FileName::virtual_("test"), src.into()); @@ -30,7 +31,7 @@ pub fn parse_infer_term(codemap: &mut CodeMap, context: &Context, src: &str) -> let raw_term = parse_term(codemap, src) .desugar(&DesugarEnv::new(context.mappings())) .unwrap(); - match pikelet_elaborate::infer_term(context, &raw_term) { + match elaborate::infer_term(context, &raw_term) { Ok((term, ty)) => (term, ty), Err(error) => { let writer = StandardStream::stdout(ColorChoice::Always); @@ -42,13 +43,9 @@ pub fn parse_infer_term(codemap: &mut CodeMap, context: &Context, src: &str) -> pub fn parse_nf_term(codemap: &mut CodeMap, context: &Context, src: &str) -> RcValue { let term = parse_infer_term(codemap, context, src).0; - match pikelet_elaborate::nf_term(context, &term) { + match nbe::nf_term(context, &term) { Ok(value) => value, - Err(error) => { - let writer = StandardStream::stdout(ColorChoice::Always); - codespan_reporting::emit(&mut writer.lock(), &codemap, &error.to_diagnostic()).unwrap(); - panic!("internal error!"); - }, + Err(error) => panic!("normalize error: {}", error), } } @@ -56,7 +53,7 @@ pub fn parse_check_term(codemap: &mut CodeMap, context: &Context, src: &str, exp let raw_term = parse_term(codemap, src) .desugar(&DesugarEnv::new(context.mappings())) .unwrap(); - match pikelet_elaborate::check_term(context, &raw_term, expected) { + match elaborate::check_term(context, &raw_term, expected) { Ok(_) => {}, Err(error) => { let writer = StandardStream::stdout(ColorChoice::Always); diff --git a/crates/pikelet-elaborate/Cargo.toml b/crates/pikelet-core/Cargo.toml similarity index 76% rename from crates/pikelet-elaborate/Cargo.toml rename to crates/pikelet-core/Cargo.toml index aac9c21f7..af59b3b0f 100644 --- a/crates/pikelet-elaborate/Cargo.toml +++ b/crates/pikelet-core/Cargo.toml @@ -1,5 +1,5 @@ [package] -name = "pikelet-elaborate" +name = "pikelet-core" version = "0.1.0" license = "Apache-2.0" readme = "README.md" @@ -14,7 +14,8 @@ codespan-reporting = "0.2.0" failure = "0.1.2" im = "12.2.0" moniker = { version = "0.5.0", features = ["codespan", "im"] } -pikelet-syntax = { version = "0.1.0", path = "../pikelet-syntax" } +pretty = { version = "0.5.2", features = ["termcolor"] } +unicode-xid = "0.1.0" [dev-dependencies] -goldenfile = "0.7.1" +pretty_assertions = "0.5.1" diff --git a/crates/pikelet-core/README.md b/crates/pikelet-core/README.md new file mode 100644 index 000000000..31a2336bc --- /dev/null +++ b/crates/pikelet-core/README.md @@ -0,0 +1,10 @@ +# Pikelet Core Syntax + +This crate is responsible for: + +- defining data structures for: + - core terms + - weak head normal forms + - normal forms (TODO) +- normalization-by-evaluation +- checking the core terms (TODO) diff --git a/crates/pikelet-core/src/lib.rs b/crates/pikelet-core/src/lib.rs new file mode 100644 index 000000000..079246be4 --- /dev/null +++ b/crates/pikelet-core/src/lib.rs @@ -0,0 +1,14 @@ +//! The syntax of the language + +extern crate codespan; +extern crate codespan_reporting; +#[macro_use] +extern crate failure; +extern crate im; +#[macro_use] +extern crate moniker; +extern crate pretty; +extern crate unicode_xid; + +pub mod nbe; +pub mod syntax; diff --git a/crates/pikelet-elaborate/src/normalize.rs b/crates/pikelet-core/src/nbe.rs similarity index 70% rename from crates/pikelet-elaborate/src/normalize.rs rename to crates/pikelet-core/src/nbe.rs index fca65dbce..c3a9ab51b 100644 --- a/crates/pikelet-elaborate/src/normalize.rs +++ b/crates/pikelet-core/src/nbe.rs @@ -1,15 +1,38 @@ use moniker::{Binder, Embed, FreeVar, Nest, Scope, Var}; -use pikelet_syntax::core::{Pattern, RcPattern, RcTerm, Term}; -use pikelet_syntax::domain::{Head, Neutral, RcNeutral, RcValue, Value}; +use syntax::core::{Pattern, RcPattern, RcTerm, Term}; +use syntax::domain::{Head, Neutral, RcNeutral, RcValue, Value}; +use syntax::Import; -use {Context, Import, InternalError}; +/// An error produced during normalization +/// +/// If a term has been successfully type checked prior to evaluation or +/// normalization, then this error should never be produced. +#[derive(Debug, Clone, PartialEq, Fail)] +#[fail(display = "{}", message)] +pub struct NbeError { + pub message: String, +} + +impl NbeError { + pub fn new(message: impl Into) -> NbeError { + NbeError { + message: message.into(), + } + } +} + +/// An environment where normalization happens +pub trait Env { + fn get_import(&self, name: &str) -> Option<&Import>; + fn get_definition(&self, free_var: &FreeVar) -> Option<&RcTerm>; +} /// Reduce a term to its normal form -pub fn nf_term(context: &Context, term: &RcTerm) -> Result { +pub fn nf_term(env: &dyn Env, term: &RcTerm) -> Result { match *term.inner { // E-ANN - Term::Ann(ref expr, _) => nf_term(context, expr), + Term::Ann(ref expr, _) => nf_term(env, expr), // E-TYPE Term::Universe(level) => Ok(RcValue::from(Value::Universe(level))), @@ -18,9 +41,9 @@ pub fn nf_term(context: &Context, term: &RcTerm) -> Result match *var { - Var::Free(ref name) => match context.get_definition(name) { + Var::Free(ref name) => match env.get_definition(name) { Some(term) => { - let mut value = nf_term(context, term)?; + let mut value = nf_term(env, term)?; value.shift_universes(shift); Ok(value) }, @@ -30,15 +53,12 @@ pub fn nf_term(context: &Context, term: &RcTerm) -> Result Err(InternalError::UnexpectedBoundVar { - span: None, - var: var.clone(), - }), + Var::Bound(_) => Err(NbeError::new(format!("unexpected bound var `{}`", var))), }, - Term::Import(ref name) => match context.get_import(name) { - Some(&(Import::Term(ref term), _)) => nf_term(context, term), - Some(&(Import::Prim(ref interpretation), _)) => match interpretation(&[]) { + Term::Import(ref name) => match env.get_import(name) { + Some(&Import::Term(ref term)) => nf_term(env, term), + Some(&Import::Prim(ref interpretation)) => match interpretation(&[]) { Some(value) => Ok(value), None => Ok(RcValue::from(Value::from(Neutral::Head(Head::Import( name.clone(), @@ -54,8 +74,8 @@ pub fn nf_term(context: &Context, term: &RcTerm) -> Result Result { - match *nf_term(context, head)?.inner { + match *nf_term(env, head)?.inner { Value::FunIntro(ref scope) => { // FIXME: do a local unbind here let ((Binder(free_var), Embed(_)), body) = scope.clone().unbind(); - nf_term(context, &body.substs(&[(free_var, arg.clone())])) + nf_term(env, &body.substs(&[(free_var, arg.clone())])) }, Value::Neutral(ref neutral, ref spine) => { - let arg = nf_term(context, arg)?; + let arg = nf_term(env, arg)?; let mut spine = spine.clone(); match *neutral.inner { Neutral::Head(Head::Import(ref name)) => { spine.push(arg); - match context.get_import(name) { - Some(&(Import::Term(ref _term), _)) => { - // nf_term(context, term) + match env.get_import(name) { + Some(&Import::Term(ref _term)) => { + // nf_term(env, term) unimplemented!("import applications") }, - Some(&(Import::Prim(ref interpretation), _)) => { + Some(&Import::Prim(ref interpretation)) => { match interpretation(&spine) { Some(value) => return Ok(value), None => {}, @@ -106,7 +126,7 @@ pub fn nf_term(context: &Context, term: &RcTerm) -> Result Err(InternalError::ArgumentAppliedToNonFunction), + _ => Err(NbeError::new("argument applied to non function")), } }, @@ -116,11 +136,11 @@ pub fn nf_term(context: &Context, term: &RcTerm) -> Result Result>()?, ); @@ -147,7 +167,7 @@ pub fn nf_term(context: &Context, term: &RcTerm) -> Result>()?, ); @@ -157,7 +177,7 @@ pub fn nf_term(context: &Context, term: &RcTerm) -> Result { - match *nf_term(context, expr)? { + match *nf_term(env, expr)? { Value::Neutral(ref neutral, ref spine) => { return Ok(RcValue::from(Value::Neutral( RcNeutral::from(Neutral::RecordProj(neutral.clone(), label.clone(), shift)), @@ -177,14 +197,15 @@ pub fn nf_term(context: &Context, term: &RcTerm) -> Result {}, } - Err(InternalError::ProjectedOnNonExistentField { - label: label.clone(), - }) + Err(NbeError::new(format!( + "projected on non existent field `{}`", + label + ))) }, // E-CASE Term::Case(ref head, ref clauses) => { - let head = nf_term(context, head)?; + let head = nf_term(env, head)?; if let Value::Neutral(ref neutral, ref spine) = *head { Ok(RcValue::from(Value::Neutral( @@ -194,7 +215,7 @@ pub fn nf_term(context: &Context, term: &RcTerm) -> Result>()?, )), @@ -203,15 +224,15 @@ pub fn nf_term(context: &Context, term: &RcTerm) -> Result>(); - return nf_term(context, &body.substs(&mappings)); + return nf_term(env, &body.substs(&mappings)); } } - Err(InternalError::NoPatternsApplicable) + Err(NbeError::new("no patterns applicable")) } }, @@ -219,7 +240,7 @@ pub fn nf_term(context: &Context, term: &RcTerm) -> Result Ok(RcValue::from(Value::ArrayIntro( elems .iter() - .map(|elem| nf_term(context, elem)) + .map(|elem| nf_term(env, elem)) .collect::>()?, ))), } @@ -228,19 +249,16 @@ pub fn nf_term(context: &Context, term: &RcTerm) -> Result Result, RcValue)>>, InternalError> { +) -> Result, RcValue)>>, NbeError> { match (&*pattern.inner, &*value.inner) { (&Pattern::Binder(Binder(ref free_var)), _) => { Ok(Some(vec![(free_var.clone(), value.clone())])) }, (&Pattern::Var(Embed(Var::Free(ref free_var)), _), _) => { - match context - .get_definition(free_var) - .map(|term| nf_term(context, term)) - { + match env.get_definition(free_var).map(|term| nf_term(env, term)) { Some(Ok(ref term)) if term == value => Ok(Some(vec![])), Some(Ok(_)) | None => Ok(None), Some(Err(err)) => Err(err), diff --git a/crates/pikelet-syntax/src/core.rs b/crates/pikelet-core/src/syntax/core.rs similarity index 99% rename from crates/pikelet-syntax/src/core.rs rename to crates/pikelet-core/src/syntax/core.rs index 44232c74a..1c5a6942c 100644 --- a/crates/pikelet-syntax/src/core.rs +++ b/crates/pikelet-core/src/syntax/core.rs @@ -6,8 +6,8 @@ use std::fmt; use std::ops; use std::rc::Rc; -use domain::{Head, Neutral, Value}; -use {FloatFormat, IntFormat, Label, Level, LevelShift, PRETTY_FALLBACK_WIDTH}; +use syntax::domain::{Head, Neutral, Value}; +use syntax::{FloatFormat, IntFormat, Label, Level, LevelShift, PRETTY_FALLBACK_WIDTH}; /// Literals /// diff --git a/crates/pikelet-syntax/src/domain.rs b/crates/pikelet-core/src/syntax/domain.rs similarity index 98% rename from crates/pikelet-syntax/src/domain.rs rename to crates/pikelet-core/src/syntax/domain.rs index 66c3f9df8..6ae026152 100644 --- a/crates/pikelet-syntax/src/domain.rs +++ b/crates/pikelet-core/src/syntax/domain.rs @@ -4,8 +4,8 @@ use moniker::{Binder, Embed, FreeVar, Nest, Scope, Var}; use std::ops; use std::rc::Rc; -use core::{Literal, RcPattern, RcTerm, Term}; -use {Label, Level, LevelShift}; +use syntax::core::{Literal, RcPattern, RcTerm, Term}; +use syntax::{Label, Level, LevelShift}; /// Values /// diff --git a/crates/pikelet-syntax/src/lib.rs b/crates/pikelet-core/src/syntax/mod.rs similarity index 90% rename from crates/pikelet-syntax/src/lib.rs rename to crates/pikelet-core/src/syntax/mod.rs index 38d4482b9..49847ce09 100644 --- a/crates/pikelet-syntax/src/lib.rs +++ b/crates/pikelet-core/src/syntax/mod.rs @@ -1,29 +1,32 @@ -//! The syntax of the language - -extern crate codespan; -extern crate codespan_reporting; -#[macro_use] -extern crate failure; -extern crate im; -extern crate lalrpop_util; -#[macro_use] -extern crate moniker; -#[cfg(test)] -#[macro_use] -extern crate pretty_assertions; -extern crate pretty; -extern crate unicode_xid; - use moniker::{Binder, BoundPattern, BoundTerm, OnBoundFn, OnFreeFn, ScopeState, Var}; use std::fmt; use std::ops::{Add, AddAssign}; -pub mod concrete; pub mod core; pub mod domain; -pub mod parse; -pub mod raw; -pub mod translation; + +/// An effectively 'infinite' line length for when we don't have an explicit +/// width provided for pretty printing. +/// +/// `pretty.rs` seems to bug-out and break on every line when using +/// `usize::MAX`, so we'll just use a really big number instead... +pub const PRETTY_FALLBACK_WIDTH: usize = 1_000_000; + +/// Imported definitions +#[derive(Clone)] +pub enum Import { + Term(core::RcTerm), + Prim(for<'a> fn(&'a [domain::RcValue]) -> Option), +} + +impl fmt::Debug for Import { + fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { + match *self { + Import::Term(ref term) => f.debug_tuple("Term").field(term).finish(), + Import::Prim(_) => f.debug_tuple("Prim").field(&"|params| { .. }").finish(), + } + } +} /// A universe level #[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, BoundTerm)] @@ -170,12 +173,3 @@ impl fmt::Display for Label { write!(f, "{}", self.0) } } - -const PRETTY_INDENT_WIDTH: usize = 4; - -/// An effectively 'infinite' line length for when we don't have an explicit -/// width provided for pretty printing. -/// -/// `pretty.rs` seems to bug-out and break on every line when using -/// `usize::MAX`, so we'll just use a really big number instead... -pub const PRETTY_FALLBACK_WIDTH: usize = 1_000_000; diff --git a/crates/pikelet-driver/Cargo.toml b/crates/pikelet-driver/Cargo.toml index 2c6536174..7729a5775 100644 --- a/crates/pikelet-driver/Cargo.toml +++ b/crates/pikelet-driver/Cargo.toml @@ -11,6 +11,6 @@ publish = false [dependencies] codespan = "0.2.0" codespan-reporting = "0.2.0" -pikelet-elaborate = { version = "0.1.0", path = "../pikelet-elaborate" } +pikelet-concrete = { version = "0.1.0", path = "../pikelet-concrete" } +pikelet-core = { version = "0.1.0", path = "../pikelet-core" } pikelet-library = { version = "0.1.0", path = "../pikelet-library" } -pikelet-syntax = { version = "0.1.0", path = "../pikelet-syntax" } diff --git a/crates/pikelet-driver/src/lib.rs b/crates/pikelet-driver/src/lib.rs index 44a355db3..af837d7e2 100644 --- a/crates/pikelet-driver/src/lib.rs +++ b/crates/pikelet-driver/src/lib.rs @@ -10,68 +10,68 @@ //! parsed, desugared, and type checked/elaborated: //! //! ```bob -//! .------------. -//! | String | -//! '------------' -//! | -//! - - - - - - - - - - | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -//! Frontend | -//! | -//! pikelet_syntax::parse::lexer -//! | -//! v -//! .-------------------------------------. -//! | pikelet_syntax::parse::lexer::Token | -//! '-------------------------------------' -//! | -//! pikelet_syntax::parse::grammar -//! | -//! v -//! .--------------------------------. -//! | pikelet_syntax::concrete::Term |---------> Code formatter (TODO) -//! '--------------------------------' -//! | -//! pikelet_syntax::translation::desugar -//! | -//! v -//! .---------------------------. -//! | pikelet_syntax::raw::Term | -//! '---------------------------' -//! | .-------------------------------. -//! pikelet_elaborate::{check,infer} <------------- | pikelet_syntax::domain::Value | -//! | '-------------------------------' -//! v ^ -//! .----------------------------. | -//! | pikelet_syntax::core::Term | - pikelet_elaborate::normalize -' -//! '----------------------------' -//! | -//! | -//! - - - - - - - - - - | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -//! Middle (TODO) | -//! | -//! v -//! A-Normal Form (ANF) -//! | -//! v -//! Closure Conversion (CC) -//! | -//! v -//! Static Single Assignment (SSA) -//! | -//! | -//! - - - - - - - - - - | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -//! Backend (TODO) | -//! | -//! v -//! Codegen -//! | -//! *-------> Bytecode? -//! | -//! *-------> WASM? -//! | -//! *-------> Cranelift IR? -//! | -//! '-------> LLVM IR? +//! .------------. +//! | String | +//! '------------' +//! | +//! - - - - - - - - - - - | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - +//! Frontend | +//! | +//! pikelet_concrete::parse::lexer +//! | +//! v +//! .---------------------------------------. +//! | pikelet_concrete::parse::lexer::Token | +//! '---------------------------------------' +//! | +//! pikelet_concrete::parse +//! | +//! v +//! .------------------------------------------. +//! | pikelet_concrete::syntax::concrete::Term |---------> Code formatter (TODO) +//! '------------------------------------------' +//! | +//! pikelet_concrete::desugar +//! | +//! v +//! .-------------------------------------. +//! | pikelet_concrete::syntax::raw::Term | +//! '-------------------------------------' +//! | .-------------------------------------. +//! pikelet_concrete::elaborate::{check,infer} <---------- | pikelet_core::syntax::domain::Value | +//! | '-------------------------------------' +//! v ^ +//! .----------------------------------. | +//! | pikelet_core::syntax::core::Term | -- pikelet_core::normalize -------' +//! '----------------------------------' +//! | +//! | +//! - - - - - - - - - - - | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - +//! Middle (TODO) | +//! | +//! v +//! A-Normal Form (ANF) +//! | +//! v +//! Closure Conversion (CC) +//! | +//! v +//! Static Single Assignment (SSA) +//! | +//! | +//! - - - - - - - - - - - | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - +//! Backend (TODO) | +//! | +//! v +//! Codegen +//! | +//! *-------> Bytecode? +//! | +//! *-------> WASM? +//! | +//! *-------> Cranelift IR? +//! | +//! '-------> LLVM IR? //! ``` //! //! As you can see we have only built the front-end as of the time of writing. When @@ -127,17 +127,19 @@ extern crate codespan; extern crate codespan_reporting; -extern crate pikelet_elaborate; +extern crate pikelet_concrete; +extern crate pikelet_core; extern crate pikelet_library; -extern crate pikelet_syntax; use codespan::{CodeMap, FileMap, FileName}; use codespan_reporting::Diagnostic; use std::sync::Arc; -use pikelet_elaborate::{Context, Import}; -use pikelet_syntax::translation::{Desugar, DesugarEnv, Resugar}; -use pikelet_syntax::{core, domain, raw}; +use pikelet_concrete::desugar::{Desugar, DesugarEnv}; +use pikelet_concrete::elaborate::Context; +use pikelet_concrete::resugar::Resugar; +use pikelet_concrete::syntax::raw; +use pikelet_core::syntax::{core, domain, Import}; /// An environment that keeps track of the state of a Pikelet program during /// compilation or interactive sessions @@ -189,7 +191,7 @@ impl Driver { internal_path: String, file_map: Arc, ) -> Result<(), Vec> { - let (concrete_term, _import_paths, errors) = pikelet_syntax::parse::term(&file_map); + let (concrete_term, _import_paths, errors) = pikelet_concrete::parse::term(&file_map); if !errors.is_empty() { return Err(errors.iter().map(|error| error.to_diagnostic()).collect()); } @@ -226,11 +228,15 @@ impl Driver { &self, raw_term: &raw::RcTerm, ) -> Result<(core::RcTerm, domain::RcType), Vec> { - pikelet_elaborate::infer_term(&self.context, &raw_term).map_err(|e| vec![e.to_diagnostic()]) + pikelet_concrete::elaborate::infer_term(&self.context, &raw_term) + .map_err(|err| vec![err.to_diagnostic()]) } pub fn nf_term(&self, term: &core::RcTerm) -> Result> { - pikelet_elaborate::nf_term(&self.context, term).map_err(|e| vec![e.to_diagnostic()]) + use pikelet_concrete::elaborate::InternalError; + + pikelet_core::nbe::nf_term(&self.context, term) + .map_err(|err| vec![InternalError::from(err).to_diagnostic()]) } pub fn resugar(&self, src: &impl Resugar) -> T { diff --git a/crates/pikelet-elaborate/README.md b/crates/pikelet-elaborate/README.md deleted file mode 100644 index 2f9d5077b..000000000 --- a/crates/pikelet-elaborate/README.md +++ /dev/null @@ -1,7 +0,0 @@ -# Pikelet elaboration - -This crate is responsible for: - -- checking/inferring the types of raw Pikelet terms -- elaborating raw Pikelet terms into core terms -- normalizing core terms into values diff --git a/crates/pikelet-repl/Cargo.toml b/crates/pikelet-repl/Cargo.toml index 23b1a594c..29a778ac2 100644 --- a/crates/pikelet-repl/Cargo.toml +++ b/crates/pikelet-repl/Cargo.toml @@ -13,7 +13,8 @@ codespan = "0.2.0" codespan-reporting = "0.2.0" failure = "0.1.2" linefeed = "0.5.3" +pikelet-concrete = { version = "0.1.0", path = "../pikelet-concrete" } +pikelet-core = { version = "0.1.0", path = "../pikelet-core" } pikelet-driver = { version = "0.1.0", path = "../pikelet-driver" } -pikelet-syntax = { version = "0.1.0", path = "../pikelet-syntax" } structopt = "0.2.12" term_size = "0.3.1" diff --git a/crates/pikelet-repl/src/lib.rs b/crates/pikelet-repl/src/lib.rs index 8e61158ba..d00f5102a 100644 --- a/crates/pikelet-repl/src/lib.rs +++ b/crates/pikelet-repl/src/lib.rs @@ -5,8 +5,9 @@ extern crate codespan_reporting; #[macro_use] extern crate failure; extern crate linefeed; +extern crate pikelet_concrete; +extern crate pikelet_core; extern crate pikelet_driver; -extern crate pikelet_syntax; #[macro_use] extern crate structopt; extern crate term_size; @@ -18,8 +19,8 @@ use failure::Error; use linefeed::{Interface, ReadResult, Signal}; use std::path::PathBuf; +use pikelet_concrete::parse; use pikelet_driver::Driver; -use pikelet_syntax::parse; /// Options for the `repl` subcommand #[derive(Debug, StructOpt)] @@ -178,7 +179,7 @@ pub fn run(opts: Opts) -> Result<(), Error> { fn eval_print(pikelet: &mut Driver, filemap: &FileMap) -> Result> { use codespan::ByteSpan; - use pikelet_syntax::concrete::{ReplCommand, Term}; + use pikelet_concrete::syntax::concrete::{ReplCommand, Term}; fn term_width() -> usize { term_size::dimensions() @@ -210,7 +211,7 @@ fn eval_print(pikelet: &mut Driver, filemap: &FileMap) -> Result { - use pikelet_syntax::core::{RcTerm, Term}; + use pikelet_core::syntax::core::{RcTerm, Term}; let raw_term = pikelet.desugar(&*concrete_term)?; let (term, inferred) = pikelet.infer_term(&raw_term)?; diff --git a/crates/pikelet-syntax/README.md b/crates/pikelet-syntax/README.md deleted file mode 100644 index 9586ae9a2..000000000 --- a/crates/pikelet-syntax/README.md +++ /dev/null @@ -1,11 +0,0 @@ -# Pikelet Syntax - -This crate is responsible for: - -- defining data structures for: - - concrete term - - raw terms - - core terms -- parsing the concrete syntax -- desugaring/resugaring -- pretty printing diff --git a/crates/pikelet-syntax/src/translation/mod.rs b/crates/pikelet-syntax/src/translation/mod.rs deleted file mode 100644 index 779a4ea47..000000000 --- a/crates/pikelet-syntax/src/translation/mod.rs +++ /dev/null @@ -1,7 +0,0 @@ -//! Translations between representations in the compiler - -mod desugar; -mod resugar; - -pub use self::desugar::{Desugar, DesugarEnv, DesugarError}; -pub use self::resugar::{Resugar, ResugarEnv}; From 8c9f801e2360fe358dd753e3d1d7fb9ca6f6e800 Mon Sep 17 00:00:00 2001 From: Brendan Zabarauskas Date: Sat, 1 Dec 2018 20:17:09 +1100 Subject: [PATCH 7/9] Move numeric formatting out of pikelet-core --- .../pikelet-concrete/src/elaborate/context.rs | 54 ++++++---------- crates/pikelet-concrete/src/elaborate/mod.rs | 34 +++++----- .../src/parse/grammar.lalrpop | 3 +- crates/pikelet-concrete/src/resugar.rs | 42 ++++++------ .../pikelet-concrete/src/syntax/concrete.rs | 4 +- crates/pikelet-concrete/src/syntax/mod.rs | 64 +++++++++++++++++++ crates/pikelet-concrete/src/syntax/raw.rs | 4 +- crates/pikelet-core/src/syntax/core.rs | 42 ++++++------ crates/pikelet-core/src/syntax/mod.rs | 63 ------------------ 9 files changed, 147 insertions(+), 163 deletions(-) diff --git a/crates/pikelet-concrete/src/elaborate/context.rs b/crates/pikelet-concrete/src/elaborate/context.rs index 2f25de9de..974a647e0 100644 --- a/crates/pikelet-concrete/src/elaborate/context.rs +++ b/crates/pikelet-concrete/src/elaborate/context.rs @@ -6,7 +6,6 @@ use pikelet_core::nbe; use pikelet_core::syntax::core::{Literal, RcTerm}; use pikelet_core::syntax::domain::{RcType, RcValue, Value}; use pikelet_core::syntax::Import; -use pikelet_core::syntax::{FloatFormat, IntFormat}; use resugar::{Resugar, ResugarEnv}; @@ -31,32 +30,21 @@ macro_rules! impl_into_value { } } }; - ($T:ty, $ty:ident, $Variant:ident, $format:expr) => { - impl IntoValue for $T { - fn ty(context: &Context) -> RcType { - context.$ty().clone() - } - - fn into_value(self) -> RcValue { - RcValue::from(Value::Literal(Literal::$Variant(self, $format))) - } - } - }; } impl_into_value!(String, string, String); impl_into_value!(char, char, Char); impl_into_value!(bool, bool, Bool); -impl_into_value!(u8, u8, U8, IntFormat::Dec); -impl_into_value!(u16, u16, U16, IntFormat::Dec); -impl_into_value!(u32, u32, U32, IntFormat::Dec); -impl_into_value!(u64, u64, U64, IntFormat::Dec); -impl_into_value!(i8, s8, S8, IntFormat::Dec); -impl_into_value!(i16, s16, S16, IntFormat::Dec); -impl_into_value!(i32, s32, S32, IntFormat::Dec); -impl_into_value!(i64, s64, S64, IntFormat::Dec); -impl_into_value!(f32, f32, F32, FloatFormat::Dec); -impl_into_value!(f64, f64, F64, FloatFormat::Dec); +impl_into_value!(u8, u8, U8); +impl_into_value!(u16, u16, U16); +impl_into_value!(u32, u32, U32); +impl_into_value!(u64, u64, U64); +impl_into_value!(i8, s8, S8); +impl_into_value!(i16, s16, S16); +impl_into_value!(i32, s32, S32); +impl_into_value!(i64, s64, S64); +impl_into_value!(f32, f32, F32); +impl_into_value!(f64, f64, F64); trait TryFromValueRef { fn try_from_value_ref(src: &Value) -> Option<&Self>; @@ -92,7 +80,7 @@ impl TryFromValueRef for bool { impl TryFromValueRef for u8 { fn try_from_value_ref(src: &Value) -> Option<&Self> { match *src { - Value::Literal(Literal::U8(ref val, _)) => Some(val), + Value::Literal(Literal::U8(ref val)) => Some(val), _ => None, } } @@ -101,7 +89,7 @@ impl TryFromValueRef for u8 { impl TryFromValueRef for u16 { fn try_from_value_ref(src: &Value) -> Option<&Self> { match *src { - Value::Literal(Literal::U16(ref val, _)) => Some(val), + Value::Literal(Literal::U16(ref val)) => Some(val), _ => None, } } @@ -110,7 +98,7 @@ impl TryFromValueRef for u16 { impl TryFromValueRef for u32 { fn try_from_value_ref(src: &Value) -> Option<&Self> { match *src { - Value::Literal(Literal::U32(ref val, _)) => Some(val), + Value::Literal(Literal::U32(ref val)) => Some(val), _ => None, } } @@ -119,7 +107,7 @@ impl TryFromValueRef for u32 { impl TryFromValueRef for u64 { fn try_from_value_ref(src: &Value) -> Option<&Self> { match *src { - Value::Literal(Literal::U64(ref val, _)) => Some(val), + Value::Literal(Literal::U64(ref val)) => Some(val), _ => None, } } @@ -128,7 +116,7 @@ impl TryFromValueRef for u64 { impl TryFromValueRef for i8 { fn try_from_value_ref(src: &Value) -> Option<&Self> { match *src { - Value::Literal(Literal::S8(ref val, _)) => Some(val), + Value::Literal(Literal::S8(ref val)) => Some(val), _ => None, } } @@ -137,7 +125,7 @@ impl TryFromValueRef for i8 { impl TryFromValueRef for i16 { fn try_from_value_ref(src: &Value) -> Option<&Self> { match *src { - Value::Literal(Literal::S16(ref val, _)) => Some(val), + Value::Literal(Literal::S16(ref val)) => Some(val), _ => None, } } @@ -146,7 +134,7 @@ impl TryFromValueRef for i16 { impl TryFromValueRef for i32 { fn try_from_value_ref(src: &Value) -> Option<&Self> { match *src { - Value::Literal(Literal::S32(ref val, _)) => Some(val), + Value::Literal(Literal::S32(ref val)) => Some(val), _ => None, } } @@ -155,7 +143,7 @@ impl TryFromValueRef for i32 { impl TryFromValueRef for i64 { fn try_from_value_ref(src: &Value) -> Option<&Self> { match *src { - Value::Literal(Literal::S64(ref val, _)) => Some(val), + Value::Literal(Literal::S64(ref val)) => Some(val), _ => None, } } @@ -164,7 +152,7 @@ impl TryFromValueRef for i64 { impl TryFromValueRef for f32 { fn try_from_value_ref(src: &Value) -> Option<&Self> { match *src { - Value::Literal(Literal::F32(ref val, _)) => Some(val), + Value::Literal(Literal::F32(ref val)) => Some(val), _ => None, } } @@ -173,7 +161,7 @@ impl TryFromValueRef for f32 { impl TryFromValueRef for f64 { fn try_from_value_ref(src: &Value) -> Option<&Self> { match *src { - Value::Literal(Literal::F64(ref val, _)) => Some(val), + Value::Literal(Literal::F64(ref val)) => Some(val), _ => None, } } @@ -547,7 +535,7 @@ impl Context { // could be relaxed in the future if it becomes a problem? Some((fv, LevelShift(0), &[ref len, ref elem_ty])) if *fv == self.globals.var_array => { match **len { - Value::Literal(Literal::U64(len, _)) => Some((len, elem_ty)), + Value::Literal(Literal::U64(len)) => Some((len, elem_ty)), _ => None, } }, diff --git a/crates/pikelet-concrete/src/elaborate/mod.rs b/crates/pikelet-concrete/src/elaborate/mod.rs index c8f3f979f..60f7a73f7 100644 --- a/crates/pikelet-concrete/src/elaborate/mod.rs +++ b/crates/pikelet-concrete/src/elaborate/mod.rs @@ -90,27 +90,25 @@ fn check_literal( raw_literal: &raw::Literal, expected_ty: &RcType, ) -> Result { - use pikelet_core::syntax::core::Literal::*; - use pikelet_core::syntax::FloatFormat::Dec as FloatDec; - - let ty = expected_ty; match *raw_literal { - raw::Literal::String(_, ref val) if context.string() == ty => Ok(String(val.clone())), - raw::Literal::Char(_, val) if context.char() == ty => Ok(Char(val)), + raw::Literal::String(_, ref val) if context.string() == expected_ty => { + Ok(Literal::String(val.clone())) + }, + raw::Literal::Char(_, val) if context.char() == expected_ty => Ok(Literal::Char(val)), // FIXME: overflow? - raw::Literal::Int(_, v, format) if context.u8() == ty => Ok(U8(v as u8, format)), - raw::Literal::Int(_, v, format) if context.u16() == ty => Ok(U16(v as u16, format)), - raw::Literal::Int(_, v, format) if context.u32() == ty => Ok(U32(v as u32, format)), - raw::Literal::Int(_, v, format) if context.u64() == ty => Ok(U64(v, format)), - raw::Literal::Int(_, v, format) if context.s8() == ty => Ok(S8(v as i8, format)), - raw::Literal::Int(_, v, format) if context.s16() == ty => Ok(S16(v as i16, format)), - raw::Literal::Int(_, v, format) if context.s32() == ty => Ok(S32(v as i32, format)), - raw::Literal::Int(_, v, format) if context.s64() == ty => Ok(S64(v as i64, format)), - raw::Literal::Int(_, v, _) if context.f32() == ty => Ok(F32(v as f32, FloatDec)), - raw::Literal::Int(_, v, _) if context.f64() == ty => Ok(F64(v as f64, FloatDec)), - raw::Literal::Float(_, v, format) if context.f32() == ty => Ok(F32(v as f32, format)), - raw::Literal::Float(_, v, format) if context.f64() == ty => Ok(F64(v, format)), + raw::Literal::Int(_, v, _) if context.u8() == expected_ty => Ok(Literal::U8(v as u8)), + raw::Literal::Int(_, v, _) if context.u16() == expected_ty => Ok(Literal::U16(v as u16)), + raw::Literal::Int(_, v, _) if context.u32() == expected_ty => Ok(Literal::U32(v as u32)), + raw::Literal::Int(_, v, _) if context.u64() == expected_ty => Ok(Literal::U64(v)), + raw::Literal::Int(_, v, _) if context.s8() == expected_ty => Ok(Literal::S8(v as i8)), + raw::Literal::Int(_, v, _) if context.s16() == expected_ty => Ok(Literal::S16(v as i16)), + raw::Literal::Int(_, v, _) if context.s32() == expected_ty => Ok(Literal::S32(v as i32)), + raw::Literal::Int(_, v, _) if context.s64() == expected_ty => Ok(Literal::S64(v as i64)), + raw::Literal::Int(_, v, _) if context.f32() == expected_ty => Ok(Literal::F32(v as f32)), + raw::Literal::Int(_, v, _) if context.f64() == expected_ty => Ok(Literal::F64(v as f64)), + raw::Literal::Float(_, v, _) if context.f32() == expected_ty => Ok(Literal::F32(v as f32)), + raw::Literal::Float(_, v, _) if context.f64() == expected_ty => Ok(Literal::F64(v)), _ => Err(TypeError::LiteralMismatch { literal_span: raw_literal.span(), diff --git a/crates/pikelet-concrete/src/parse/grammar.lalrpop b/crates/pikelet-concrete/src/parse/grammar.lalrpop index 519359f23..9b09f065e 100644 --- a/crates/pikelet-concrete/src/parse/grammar.lalrpop +++ b/crates/pikelet-concrete/src/parse/grammar.lalrpop @@ -1,9 +1,8 @@ use codespan::FileMap; use codespan::{ByteIndex, ByteSpan}; -use pikelet_core::syntax::{FloatFormat, IntFormat}; - use parse::{LalrpopError, ParseError, Token}; +use syntax::{FloatFormat, IntFormat}; use syntax::concrete::{Item, Literal, Pattern, Term, RecordTypeField, RecordIntroField, ReplCommand}; #[LALR] diff --git a/crates/pikelet-concrete/src/resugar.rs b/crates/pikelet-concrete/src/resugar.rs index 27bef7c2d..5362caecb 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; +use syntax::{concrete, IntFormat, FloatFormat}; /// The environment used when resugaring from the core to the concrete syntax #[derive(Debug, Clone)] @@ -170,19 +170,19 @@ fn resugar_pattern( core::Literal::String(ref val) => Literal(String(span, val.clone())), core::Literal::Char(val) => Literal(Char(span, val)), - core::Literal::U8(val, format) => Literal(Int(span, u64::from(val), format)), - core::Literal::U16(val, format) => Literal(Int(span, u64::from(val), format)), - core::Literal::U32(val, format) => Literal(Int(span, u64::from(val), format)), - core::Literal::U64(val, format) => Literal(Int(span, val, format)), + core::Literal::U8(val) => Literal(Int(span, u64::from(val), IntFormat::Dec)), + core::Literal::U16(val) => Literal(Int(span, u64::from(val), IntFormat::Dec)), + core::Literal::U32(val) => Literal(Int(span, u64::from(val), IntFormat::Dec)), + core::Literal::U64(val) => Literal(Int(span, val, IntFormat::Dec)), // FIXME: Underflow for negative numbers - core::Literal::S8(val, format) => Literal(Int(span, val as u64, format)), - core::Literal::S16(val, format) => Literal(Int(span, val as u64, format)), - core::Literal::S32(val, format) => Literal(Int(span, val as u64, format)), - core::Literal::S64(val, format) => Literal(Int(span, val as u64, format)), + core::Literal::S8(val) => Literal(Int(span, val as u64, IntFormat::Dec)), + core::Literal::S16(val) => Literal(Int(span, val as u64, IntFormat::Dec)), + core::Literal::S32(val) => Literal(Int(span, val as u64, IntFormat::Dec)), + core::Literal::S64(val) => Literal(Int(span, val as u64, IntFormat::Dec)), - core::Literal::F32(val, format) => Literal(Float(span, f64::from(val), format)), - core::Literal::F64(val, format) => Literal(Float(span, val, format)), + core::Literal::F32(val) => Literal(Float(span, f64::from(val), FloatFormat::Dec)), + core::Literal::F64(val) => Literal(Float(span, val, FloatFormat::Dec)), } }, } @@ -460,19 +460,19 @@ fn resugar_term(env: &ResugarEnv, term: &core::Term, prec: Prec) -> concrete::Te core::Literal::String(ref val) => Literal(String(span, val.clone())), core::Literal::Char(val) => Literal(Char(span, val)), - core::Literal::U8(val, format) => Literal(Int(span, u64::from(val), format)), - core::Literal::U16(val, format) => Literal(Int(span, u64::from(val), format)), - core::Literal::U32(val, format) => Literal(Int(span, u64::from(val), format)), - core::Literal::U64(val, format) => Literal(Int(span, val, format)), + core::Literal::U8(val) => Literal(Int(span, u64::from(val), IntFormat::Dec)), + core::Literal::U16(val) => Literal(Int(span, u64::from(val), IntFormat::Dec)), + core::Literal::U32(val) => Literal(Int(span, u64::from(val), IntFormat::Dec)), + core::Literal::U64(val) => Literal(Int(span, val, IntFormat::Dec)), // FIXME: Underflow for negative numbers - core::Literal::S8(val, format) => Literal(Int(span, val as u64, format)), - core::Literal::S16(val, format) => Literal(Int(span, val as u64, format)), - core::Literal::S32(val, format) => Literal(Int(span, val as u64, format)), - core::Literal::S64(val, format) => Literal(Int(span, val as u64, format)), + core::Literal::S8(val) => Literal(Int(span, val as u64, IntFormat::Dec)), + core::Literal::S16(val) => Literal(Int(span, val as u64, IntFormat::Dec)), + core::Literal::S32(val) => Literal(Int(span, val as u64, IntFormat::Dec)), + core::Literal::S64(val) => Literal(Int(span, val as u64, IntFormat::Dec)), - core::Literal::F32(val, format) => Literal(Float(span, f64::from(val), format)), - core::Literal::F64(val, format) => Literal(Float(span, val, format)), + core::Literal::F32(val) => Literal(Float(span, f64::from(val), FloatFormat::Dec)), + core::Literal::F64(val) => Literal(Float(span, val, FloatFormat::Dec)), } }, core::Term::Var(Var::Free(ref free_var), shift) => { diff --git a/crates/pikelet-concrete/src/syntax/concrete.rs b/crates/pikelet-concrete/src/syntax/concrete.rs index 00a89f50c..e351a119f 100644 --- a/crates/pikelet-concrete/src/syntax/concrete.rs +++ b/crates/pikelet-concrete/src/syntax/concrete.rs @@ -4,9 +4,7 @@ use codespan::{ByteIndex, ByteSpan}; use pretty::{BoxDoc, Doc}; use std::fmt; -use pikelet_core::syntax::{FloatFormat, IntFormat}; - -use syntax::{PRETTY_FALLBACK_WIDTH, PRETTY_INDENT_WIDTH}; +use syntax::{FloatFormat, IntFormat, PRETTY_FALLBACK_WIDTH, PRETTY_INDENT_WIDTH}; /// Commands entered in the REPL #[derive(Debug, Clone)] diff --git a/crates/pikelet-concrete/src/syntax/mod.rs b/crates/pikelet-concrete/src/syntax/mod.rs index 6340f9c8b..f07332765 100644 --- a/crates/pikelet-concrete/src/syntax/mod.rs +++ b/crates/pikelet-concrete/src/syntax/mod.rs @@ -1,3 +1,5 @@ +use moniker::{Binder, BoundPattern, BoundTerm, OnBoundFn, OnFreeFn, ScopeState, Var}; + pub mod concrete; pub mod raw; @@ -9,3 +11,65 @@ const PRETTY_INDENT_WIDTH: usize = 4; /// `pretty.rs` seems to bug-out and break on every line when using /// `usize::MAX`, so we'll just use a really big number instead... pub const PRETTY_FALLBACK_WIDTH: usize = 1_000_000; + +#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord)] +pub enum IntFormat { + Bin, + Oct, + Dec, + Hex, +} + +impl BoundTerm for IntFormat { + fn term_eq(&self, _: &IntFormat) -> bool { + true + } + + fn close_term(&mut self, _: ScopeState, _: &impl OnFreeFn) {} + fn open_term(&mut self, _: ScopeState, _: &impl OnBoundFn) {} + fn visit_vars(&self, _: &mut impl FnMut(&Var)) {} + fn visit_mut_vars(&mut self, _: &mut impl FnMut(&mut Var)) {} +} + +impl BoundPattern for IntFormat { + fn pattern_eq(&self, _: &IntFormat) -> bool { + true + } + + fn close_pattern(&mut self, _: ScopeState, _: &impl OnFreeFn) {} + fn open_pattern(&mut self, _: ScopeState, _: &impl OnBoundFn) {} + fn visit_vars(&self, _: &mut impl FnMut(&Var)) {} + fn visit_mut_vars(&mut self, _: &mut impl FnMut(&mut Var)) {} + fn visit_binders(&self, _: &mut impl FnMut(&Binder)) {} + fn visit_mut_binders(&mut self, _: &mut impl FnMut(&mut Binder)) {} +} + +#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord)] +pub enum FloatFormat { + Dec, + // TODO: Binary and Hex floats? +} + +impl BoundTerm for FloatFormat { + fn term_eq(&self, _: &FloatFormat) -> bool { + true + } + + fn close_term(&mut self, _: ScopeState, _: &impl OnFreeFn) {} + fn open_term(&mut self, _: ScopeState, _: &impl OnBoundFn) {} + fn visit_vars(&self, _: &mut impl FnMut(&Var)) {} + fn visit_mut_vars(&mut self, _: &mut impl FnMut(&mut Var)) {} +} + +impl BoundPattern for FloatFormat { + fn pattern_eq(&self, _: &FloatFormat) -> bool { + true + } + + fn close_pattern(&mut self, _: ScopeState, _: &impl OnFreeFn) {} + fn open_pattern(&mut self, _: ScopeState, _: &impl OnBoundFn) {} + fn visit_vars(&self, _: &mut impl FnMut(&Var)) {} + fn visit_mut_vars(&mut self, _: &mut impl FnMut(&mut Var)) {} + fn visit_binders(&self, _: &mut impl FnMut(&Binder)) {} + fn visit_mut_binders(&mut self, _: &mut impl FnMut(&mut Binder)) {} +} diff --git a/crates/pikelet-concrete/src/syntax/raw.rs b/crates/pikelet-concrete/src/syntax/raw.rs index f3e9b2a61..c65630443 100644 --- a/crates/pikelet-concrete/src/syntax/raw.rs +++ b/crates/pikelet-concrete/src/syntax/raw.rs @@ -8,9 +8,9 @@ use std::fmt; use std::ops; use std::rc::Rc; -use pikelet_core::syntax::{FloatFormat, IntFormat, Label, Level, LevelShift}; +use pikelet_core::syntax::{Label, Level, LevelShift}; -use syntax::PRETTY_FALLBACK_WIDTH; +use syntax::{FloatFormat, IntFormat, PRETTY_FALLBACK_WIDTH}; /// Literals #[derive(Debug, Clone, PartialEq, PartialOrd, BoundTerm, BoundPattern)] diff --git a/crates/pikelet-core/src/syntax/core.rs b/crates/pikelet-core/src/syntax/core.rs index 1c5a6942c..26bffd2c0 100644 --- a/crates/pikelet-core/src/syntax/core.rs +++ b/crates/pikelet-core/src/syntax/core.rs @@ -7,7 +7,7 @@ use std::ops; use std::rc::Rc; use syntax::domain::{Head, Neutral, Value}; -use syntax::{FloatFormat, IntFormat, Label, Level, LevelShift, PRETTY_FALLBACK_WIDTH}; +use syntax::{Label, Level, LevelShift, PRETTY_FALLBACK_WIDTH}; /// Literals /// @@ -17,16 +17,16 @@ pub enum Literal { Bool(bool), String(String), Char(char), - U8(u8, IntFormat), - U16(u16, IntFormat), - U32(u32, IntFormat), - U64(u64, IntFormat), - S8(i8, IntFormat), - S16(i16, IntFormat), - S32(i32, IntFormat), - S64(i64, IntFormat), - F32(f32, FloatFormat), - F64(f64, FloatFormat), + U8(u8), + U16(u16), + U32(u32), + U64(u64), + S8(i8), + S16(i16), + S32(i32), + S64(i64), + F32(f32), + F64(f64), } impl Literal { @@ -36,16 +36,16 @@ impl Literal { Literal::Bool(false) => Doc::text("false"), Literal::String(ref value) => Doc::text(format!("{:?}", value)), Literal::Char(value) => Doc::text(format!("{:?}", value)), - Literal::U8(value, _) => Doc::as_string(&value), - Literal::U16(value, _) => Doc::as_string(&value), - Literal::U32(value, _) => Doc::as_string(&value), - Literal::U64(value, _) => Doc::as_string(&value), - Literal::S8(value, _) => Doc::as_string(&value), - Literal::S16(value, _) => Doc::as_string(&value), - Literal::S32(value, _) => Doc::as_string(&value), - Literal::S64(value, _) => Doc::as_string(&value), - Literal::F32(value, _) => Doc::as_string(&value), - Literal::F64(value, _) => Doc::as_string(&value), + Literal::U8(value) => Doc::as_string(&value), + Literal::U16(value) => Doc::as_string(&value), + Literal::U32(value) => Doc::as_string(&value), + Literal::U64(value) => Doc::as_string(&value), + Literal::S8(value) => Doc::as_string(&value), + Literal::S16(value) => Doc::as_string(&value), + Literal::S32(value) => Doc::as_string(&value), + Literal::S64(value) => Doc::as_string(&value), + Literal::F32(value) => Doc::as_string(&value), + Literal::F64(value) => Doc::as_string(&value), } } } diff --git a/crates/pikelet-core/src/syntax/mod.rs b/crates/pikelet-core/src/syntax/mod.rs index 49847ce09..ef4b4191e 100644 --- a/crates/pikelet-core/src/syntax/mod.rs +++ b/crates/pikelet-core/src/syntax/mod.rs @@ -1,4 +1,3 @@ -use moniker::{Binder, BoundPattern, BoundTerm, OnBoundFn, OnFreeFn, ScopeState, Var}; use std::fmt; use std::ops::{Add, AddAssign}; @@ -94,68 +93,6 @@ impl AddAssign for Level { } } -#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord)] -pub enum IntFormat { - Bin, - Oct, - Dec, - Hex, -} - -impl BoundTerm for IntFormat { - fn term_eq(&self, _: &IntFormat) -> bool { - true - } - - fn close_term(&mut self, _: ScopeState, _: &impl OnFreeFn) {} - fn open_term(&mut self, _: ScopeState, _: &impl OnBoundFn) {} - fn visit_vars(&self, _: &mut impl FnMut(&Var)) {} - fn visit_mut_vars(&mut self, _: &mut impl FnMut(&mut Var)) {} -} - -impl BoundPattern for IntFormat { - fn pattern_eq(&self, _: &IntFormat) -> bool { - true - } - - fn close_pattern(&mut self, _: ScopeState, _: &impl OnFreeFn) {} - fn open_pattern(&mut self, _: ScopeState, _: &impl OnBoundFn) {} - fn visit_vars(&self, _: &mut impl FnMut(&Var)) {} - fn visit_mut_vars(&mut self, _: &mut impl FnMut(&mut Var)) {} - fn visit_binders(&self, _: &mut impl FnMut(&Binder)) {} - fn visit_mut_binders(&mut self, _: &mut impl FnMut(&mut Binder)) {} -} - -#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord)] -pub enum FloatFormat { - Dec, - // TODO: Binary and Hex floats? -} - -impl BoundTerm for FloatFormat { - fn term_eq(&self, _: &FloatFormat) -> bool { - true - } - - fn close_term(&mut self, _: ScopeState, _: &impl OnFreeFn) {} - fn open_term(&mut self, _: ScopeState, _: &impl OnBoundFn) {} - fn visit_vars(&self, _: &mut impl FnMut(&Var)) {} - fn visit_mut_vars(&mut self, _: &mut impl FnMut(&mut Var)) {} -} - -impl BoundPattern for FloatFormat { - fn pattern_eq(&self, _: &FloatFormat) -> bool { - true - } - - fn close_pattern(&mut self, _: ScopeState, _: &impl OnFreeFn) {} - fn open_pattern(&mut self, _: ScopeState, _: &impl OnBoundFn) {} - fn visit_vars(&self, _: &mut impl FnMut(&Var)) {} - fn visit_mut_vars(&mut self, _: &mut impl FnMut(&mut Var)) {} - fn visit_binders(&self, _: &mut impl FnMut(&Binder)) {} - fn visit_mut_binders(&mut self, _: &mut impl FnMut(&mut Binder)) {} -} - /// A label that describes the name of a field in a record /// /// Labels are significant when comparing for alpha-equality From 9744f48ccb72abc628c4cb0aaf48675476ad083e Mon Sep 17 00:00:00 2001 From: Brendan Zabarauskas Date: Sat, 1 Dec 2018 21:05:40 +1100 Subject: [PATCH 8/9] 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); From e8f106b6849875380877509a588f1da30fa20ed5 Mon Sep 17 00:00:00 2001 From: Brendan Zabarauskas Date: Sun, 2 Dec 2018 00:27:00 +1100 Subject: [PATCH 9/9] Move literals --- .../pikelet-concrete/src/elaborate/context.rs | 4 +- crates/pikelet-concrete/src/elaborate/mod.rs | 6 +- crates/pikelet-concrete/src/resugar.rs | 62 ++++++++++--------- crates/pikelet-concrete/tests/resugar.rs | 8 +-- crates/pikelet-core/src/syntax/core.rs | 49 +-------------- crates/pikelet-core/src/syntax/domain.rs | 4 +- crates/pikelet-core/src/syntax/mod.rs | 48 ++++++++++++++ 7 files changed, 92 insertions(+), 89 deletions(-) diff --git a/crates/pikelet-concrete/src/elaborate/context.rs b/crates/pikelet-concrete/src/elaborate/context.rs index 974a647e0..10d662d29 100644 --- a/crates/pikelet-concrete/src/elaborate/context.rs +++ b/crates/pikelet-concrete/src/elaborate/context.rs @@ -3,9 +3,9 @@ use moniker::{Binder, FreeVar, Var}; use std::rc::Rc; use pikelet_core::nbe; -use pikelet_core::syntax::core::{Literal, RcTerm}; +use pikelet_core::syntax::core::RcTerm; use pikelet_core::syntax::domain::{RcType, RcValue, Value}; -use pikelet_core::syntax::Import; +use pikelet_core::syntax::{Import, Literal}; use resugar::{Resugar, ResugarEnv}; diff --git a/crates/pikelet-concrete/src/elaborate/mod.rs b/crates/pikelet-concrete/src/elaborate/mod.rs index 899632bfd..7394f11dc 100644 --- a/crates/pikelet-concrete/src/elaborate/mod.rs +++ b/crates/pikelet-concrete/src/elaborate/mod.rs @@ -8,9 +8,9 @@ use codespan::ByteSpan; use moniker::{Binder, BoundPattern, BoundTerm, Embed, FreeVar, Nest, Scope, Var}; use pikelet_core::nbe; -use pikelet_core::syntax::core::{Literal, Pattern, RcPattern, RcTerm, Term}; +use pikelet_core::syntax::core::{Pattern, RcPattern, RcTerm, Term}; use pikelet_core::syntax::domain::{RcType, RcValue, Value}; -use pikelet_core::syntax::Level; +use pikelet_core::syntax::{Level, Literal}; use syntax::raw; @@ -124,7 +124,7 @@ fn infer_literal( context: &Context, raw_literal: &raw::Literal, ) -> Result<(Literal, RcType), TypeError> { - use pikelet_core::syntax::core::Literal::{Char, String}; + use pikelet_core::syntax::Literal::{Char, String}; match *raw_literal { raw::Literal::String(_, ref val) => Ok((String(val.clone()), context.string().clone())), diff --git a/crates/pikelet-concrete/src/resugar.rs b/crates/pikelet-concrete/src/resugar.rs index b3aedd3c7..e45c768c9 100644 --- a/crates/pikelet-concrete/src/resugar.rs +++ b/crates/pikelet-concrete/src/resugar.rs @@ -156,33 +156,34 @@ fn resugar_pattern( panic!("Tried to convert a term that was not locally closed"); }, core::Pattern::Literal(ref literal) => { + use pikelet_core::syntax::Literal; + use syntax::concrete::Literal::*; use syntax::concrete::Pattern; - use syntax::concrete::Pattern::Literal; let span = ByteSpan::default(); match *literal { // FIXME: Draw these names from some environment? - core::Literal::Bool(true) => Pattern::Name(span, "true".to_owned(), None), - core::Literal::Bool(false) => Pattern::Name(span, "false".to_owned(), None), + Literal::Bool(true) => Pattern::Name(span, "true".to_owned(), None), + Literal::Bool(false) => Pattern::Name(span, "false".to_owned(), None), - core::Literal::String(ref val) => Literal(String(span, val.clone())), - core::Literal::Char(val) => Literal(Char(span, val)), + Literal::String(ref val) => Pattern::Literal(String(span, val.clone())), + Literal::Char(val) => Pattern::Literal(Char(span, val)), - core::Literal::U8(val) => Literal(Int(span, u64::from(val), IntFormat::Dec)), - core::Literal::U16(val) => Literal(Int(span, u64::from(val), IntFormat::Dec)), - core::Literal::U32(val) => Literal(Int(span, u64::from(val), IntFormat::Dec)), - core::Literal::U64(val) => Literal(Int(span, val, IntFormat::Dec)), + Literal::U8(val) => Pattern::Literal(Int(span, u64::from(val), IntFormat::Dec)), + Literal::U16(val) => Pattern::Literal(Int(span, u64::from(val), IntFormat::Dec)), + Literal::U32(val) => Pattern::Literal(Int(span, u64::from(val), IntFormat::Dec)), + Literal::U64(val) => Pattern::Literal(Int(span, val, IntFormat::Dec)), // FIXME: Underflow for negative numbers - core::Literal::S8(val) => Literal(Int(span, val as u64, IntFormat::Dec)), - core::Literal::S16(val) => Literal(Int(span, val as u64, IntFormat::Dec)), - core::Literal::S32(val) => Literal(Int(span, val as u64, IntFormat::Dec)), - core::Literal::S64(val) => Literal(Int(span, val as u64, IntFormat::Dec)), + Literal::S8(val) => Pattern::Literal(Int(span, val as u64, IntFormat::Dec)), + Literal::S16(val) => Pattern::Literal(Int(span, val as u64, IntFormat::Dec)), + Literal::S32(val) => Pattern::Literal(Int(span, val as u64, IntFormat::Dec)), + Literal::S64(val) => Pattern::Literal(Int(span, val as u64, IntFormat::Dec)), - core::Literal::F32(val) => Literal(Float(span, f64::from(val), FloatFormat::Dec)), - core::Literal::F64(val) => Literal(Float(span, val, FloatFormat::Dec)), + Literal::F32(v) => Pattern::Literal(Float(span, f64::from(v), FloatFormat::Dec)), + Literal::F64(v) => Pattern::Literal(Float(span, v, FloatFormat::Dec)), } }, } @@ -446,33 +447,34 @@ fn resugar_term(env: &ResugarEnv, term: &core::Term, prec: Prec) -> concrete::Te ) }, core::Term::Literal(ref literal) => { + use pikelet_core::syntax::Literal; + use syntax::concrete::Literal::*; use syntax::concrete::Term; - use syntax::concrete::Term::Literal; let span = ByteSpan::default(); match *literal { // FIXME: Draw these names from some environment? - core::Literal::Bool(true) => Term::Name(span, "true".to_owned(), None), - core::Literal::Bool(false) => Term::Name(span, "false".to_owned(), None), + Literal::Bool(true) => Term::Name(span, "true".to_owned(), None), + Literal::Bool(false) => Term::Name(span, "false".to_owned(), None), - core::Literal::String(ref val) => Literal(String(span, val.clone())), - core::Literal::Char(val) => Literal(Char(span, val)), + Literal::String(ref val) => Term::Literal(String(span, val.clone())), + Literal::Char(val) => Term::Literal(Char(span, val)), - core::Literal::U8(val) => Literal(Int(span, u64::from(val), IntFormat::Dec)), - core::Literal::U16(val) => Literal(Int(span, u64::from(val), IntFormat::Dec)), - core::Literal::U32(val) => Literal(Int(span, u64::from(val), IntFormat::Dec)), - core::Literal::U64(val) => Literal(Int(span, val, IntFormat::Dec)), + Literal::U8(val) => Term::Literal(Int(span, u64::from(val), IntFormat::Dec)), + Literal::U16(val) => Term::Literal(Int(span, u64::from(val), IntFormat::Dec)), + Literal::U32(val) => Term::Literal(Int(span, u64::from(val), IntFormat::Dec)), + Literal::U64(val) => Term::Literal(Int(span, val, IntFormat::Dec)), // FIXME: Underflow for negative numbers - core::Literal::S8(val) => Literal(Int(span, val as u64, IntFormat::Dec)), - core::Literal::S16(val) => Literal(Int(span, val as u64, IntFormat::Dec)), - core::Literal::S32(val) => Literal(Int(span, val as u64, IntFormat::Dec)), - core::Literal::S64(val) => Literal(Int(span, val as u64, IntFormat::Dec)), + Literal::S8(val) => Term::Literal(Int(span, val as u64, IntFormat::Dec)), + Literal::S16(val) => Term::Literal(Int(span, val as u64, IntFormat::Dec)), + Literal::S32(val) => Term::Literal(Int(span, val as u64, IntFormat::Dec)), + Literal::S64(val) => Term::Literal(Int(span, val as u64, IntFormat::Dec)), - core::Literal::F32(val) => Literal(Float(span, f64::from(val), FloatFormat::Dec)), - core::Literal::F64(val) => Literal(Float(span, val, FloatFormat::Dec)), + Literal::F32(val) => Term::Literal(Float(span, f64::from(val), FloatFormat::Dec)), + Literal::F64(val) => Term::Literal(Float(span, val, FloatFormat::Dec)), } }, core::Term::Var(Var::Free(ref free_var), shift) => { diff --git a/crates/pikelet-concrete/tests/resugar.rs b/crates/pikelet-concrete/tests/resugar.rs index 80eef6279..e4672071a 100644 --- a/crates/pikelet-concrete/tests/resugar.rs +++ b/crates/pikelet-concrete/tests/resugar.rs @@ -8,7 +8,7 @@ use moniker::{Binder, Embed, FreeVar, Nest, Scope, Var}; use pikelet_concrete::resugar::{Resugar, ResugarEnv}; use pikelet_concrete::syntax::concrete; -use pikelet_core::syntax::{core, Label, LevelShift}; +use pikelet_core::syntax::{core, Label, LevelShift, Literal}; fn span() -> ByteSpan { ByteSpan::default() @@ -53,7 +53,7 @@ fn universe1() { #[test] fn lit_bool_true() { - let core_term = core::Term::Literal(core::Literal::Bool(true)); + let core_term = core::Term::Literal(Literal::Bool(true)); let concrete_term = concrete::Term::Name(span(), "true".to_owned(), None); assert_eq!(core_term.resugar(&ResugarEnv::new()), concrete_term); @@ -61,7 +61,7 @@ fn lit_bool_true() { #[test] fn lit_bool_false() { - let core_term = core::Term::Literal(core::Literal::Bool(false)); + let core_term = core::Term::Literal(Literal::Bool(false)); let concrete_term = concrete::Term::Name(span(), "false".to_owned(), None); assert_eq!(core_term.resugar(&ResugarEnv::new()), concrete_term); @@ -69,7 +69,7 @@ fn lit_bool_false() { #[test] fn lit_string() { - let core_term = core::Term::Literal(core::Literal::String("hello".to_owned())); + let core_term = core::Term::Literal(Literal::String("hello".to_owned())); let concrete_term = concrete::Term::Literal(concrete::Literal::String(span(), "hello".to_owned())); diff --git a/crates/pikelet-core/src/syntax/core.rs b/crates/pikelet-core/src/syntax/core.rs index a6d7eb582..57cdadefa 100644 --- a/crates/pikelet-core/src/syntax/core.rs +++ b/crates/pikelet-core/src/syntax/core.rs @@ -7,54 +7,7 @@ use std::ops; use std::rc::Rc; use syntax::domain::{Head, Neutral, Value}; -use syntax::{Label, Level, LevelShift, PRETTY_FALLBACK_WIDTH}; - -/// Literals -/// -/// We could church encode all the things, but that would be prohibitively expensive! -#[derive(Debug, Clone, PartialEq, PartialOrd, BoundTerm, BoundPattern)] -pub enum Literal { - Bool(bool), - String(String), - Char(char), - U8(u8), - U16(u16), - U32(u32), - U64(u64), - S8(i8), - S16(i16), - S32(i32), - S64(i64), - F32(f32), - F64(f64), -} - -impl Literal { - pub fn to_doc(&self) -> Doc> { - match *self { - Literal::Bool(true) => Doc::text("true"), - Literal::Bool(false) => Doc::text("false"), - Literal::String(ref value) => Doc::text(format!("{:?}", value)), - Literal::Char(value) => Doc::text(format!("{:?}", value)), - Literal::U8(value) => Doc::as_string(&value), - Literal::U16(value) => Doc::as_string(&value), - Literal::U32(value) => Doc::as_string(&value), - Literal::U64(value) => Doc::as_string(&value), - Literal::S8(value) => Doc::as_string(&value), - Literal::S16(value) => Doc::as_string(&value), - Literal::S32(value) => Doc::as_string(&value), - Literal::S64(value) => Doc::as_string(&value), - Literal::F32(value) => Doc::as_string(&value), - Literal::F64(value) => Doc::as_string(&value), - } - } -} - -impl fmt::Display for Literal { - fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { - self.to_doc().group().render_fmt(PRETTY_FALLBACK_WIDTH, f) - } -} +use syntax::{Label, Level, LevelShift, Literal, PRETTY_FALLBACK_WIDTH}; #[derive(Debug, Clone, PartialEq, BoundPattern)] pub enum Pattern { diff --git a/crates/pikelet-core/src/syntax/domain.rs b/crates/pikelet-core/src/syntax/domain.rs index 580a88065..4ed75f97c 100644 --- a/crates/pikelet-core/src/syntax/domain.rs +++ b/crates/pikelet-core/src/syntax/domain.rs @@ -4,8 +4,8 @@ use moniker::{Binder, Embed, FreeVar, Nest, Scope, Var}; use std::ops; use std::rc::Rc; -use syntax::core::{Literal, RcPattern, RcTerm, Term}; -use syntax::{Label, Level, LevelShift}; +use syntax::core::{RcPattern, RcTerm, Term}; +use syntax::{Label, Level, LevelShift, Literal}; /// Values /// diff --git a/crates/pikelet-core/src/syntax/mod.rs b/crates/pikelet-core/src/syntax/mod.rs index ef4b4191e..ba98302be 100644 --- a/crates/pikelet-core/src/syntax/mod.rs +++ b/crates/pikelet-core/src/syntax/mod.rs @@ -1,3 +1,4 @@ +use pretty::{BoxDoc, Doc}; use std::fmt; use std::ops::{Add, AddAssign}; @@ -27,6 +28,53 @@ impl fmt::Debug for Import { } } +/// Literals +/// +/// We could church encode all the things, but that would be prohibitively expensive! +#[derive(Debug, Clone, PartialEq, PartialOrd, BoundTerm, BoundPattern)] +pub enum Literal { + Bool(bool), + String(String), + Char(char), + U8(u8), + U16(u16), + U32(u32), + U64(u64), + S8(i8), + S16(i16), + S32(i32), + S64(i64), + F32(f32), + F64(f64), +} + +impl Literal { + pub fn to_doc(&self) -> Doc> { + match *self { + Literal::Bool(true) => Doc::text("true"), + Literal::Bool(false) => Doc::text("false"), + Literal::String(ref value) => Doc::text(format!("{:?}", value)), + Literal::Char(value) => Doc::text(format!("{:?}", value)), + Literal::U8(value) => Doc::as_string(&value), + Literal::U16(value) => Doc::as_string(&value), + Literal::U32(value) => Doc::as_string(&value), + Literal::U64(value) => Doc::as_string(&value), + Literal::S8(value) => Doc::as_string(&value), + Literal::S16(value) => Doc::as_string(&value), + Literal::S32(value) => Doc::as_string(&value), + Literal::S64(value) => Doc::as_string(&value), + Literal::F32(value) => Doc::as_string(&value), + Literal::F64(value) => Doc::as_string(&value), + } + } +} + +impl fmt::Display for Literal { + fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { + self.to_doc().group().render_fmt(PRETTY_FALLBACK_WIDTH, f) + } +} + /// A universe level #[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, BoundTerm)] pub struct Level(pub u32);