diff --git a/Cargo.toml b/Cargo.toml index e5f890e78..50105b832 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -1,9 +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 96% rename from crates/pikelet-syntax/src/translation/desugar.rs rename to crates/pikelet-concrete/src/desugar.rs index 39e46a253..9887a320d 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)] @@ -386,41 +387,33 @@ fn desugar_record_ty( fn desugar_record_intro( env: &DesugarEnv, span: ByteSpan, - fields: &[concrete::RecordField], + fields: &[concrete::RecordIntroField], ) -> Result { - use concrete::RecordField; - - let mut env = env.clone(); + use syntax::concrete::RecordIntroField; let fields = fields .iter() .map(|field| match field { - RecordField::Punned { + RecordIntroField::Punned { label: (_, ref name), 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)) }, - RecordField::Explicit { + 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-elaborate/src/context.rs b/crates/pikelet-concrete/src/elaborate/context.rs similarity index 90% rename from crates/pikelet-elaborate/src/context.rs rename to crates/pikelet-concrete/src/elaborate/context.rs index 9a1c2eb06..10d662d29 100644 --- a/crates/pikelet-elaborate/src/context.rs +++ b/crates/pikelet-concrete/src/elaborate/context.rs @@ -1,11 +1,13 @@ use im; use moniker::{Binder, FreeVar, Var}; -use std::fmt; use std::rc::Rc; -use pikelet_syntax::core::{Literal, RcTerm, RcType, RcValue, Value}; -use pikelet_syntax::translation::{Resugar, ResugarEnv}; -use pikelet_syntax::{FloatFormat, IntFormat}; +use pikelet_core::nbe; +use pikelet_core::syntax::core::RcTerm; +use pikelet_core::syntax::domain::{RcType, RcValue, Value}; +use pikelet_core::syntax::{Import, Literal}; + +use resugar::{Resugar, ResugarEnv}; // Some helper traits for marshalling between Rust and Pikelet values // @@ -28,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>; @@ -89,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, } } @@ -98,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, } } @@ -107,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, } } @@ -116,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, } } @@ -125,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, } } @@ -134,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, } } @@ -143,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, } } @@ -152,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, } } @@ -161,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, } } @@ -170,28 +161,12 @@ 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, } } } -/// 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, @@ -239,7 +214,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"); @@ -553,14 +528,14 @@ 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 // 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, } }, @@ -594,3 +569,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 85% rename from crates/pikelet-elaborate/src/lib.rs rename to crates/pikelet-concrete/src/elaborate/mod.rs index 31213ec0d..7394f11dc 100644 --- a/crates/pikelet-elaborate/src/lib.rs +++ b/crates/pikelet-concrete/src/elaborate/mod.rs @@ -4,28 +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, RcType, RcValue, Term, Value}; -use pikelet_syntax::raw; -use pikelet_syntax::Level; +use pikelet_core::nbe; +use pikelet_core::syntax::core::{Pattern, RcPattern, RcTerm, Term}; +use pikelet_core::syntax::domain::{RcType, RcValue, Value}; +use pikelet_core::syntax::{Level, Literal}; + +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 { @@ -97,27 +90,25 @@ fn check_literal( raw_literal: &raw::Literal, expected_ty: &RcType, ) -> Result { - use pikelet_syntax::core::Literal::*; - use pikelet_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(), @@ -133,7 +124,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::Literal::{Char, String}; match *raw_literal { raw::Literal::String(_, ref val) => Ok((String(val.clone()), context.string().clone())), @@ -185,7 +176,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(( @@ -275,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 { - let ann = nf_term(context, &ann.substs(&mappings))?; + 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), _) => { @@ -403,7 +389,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)) @@ -464,7 +450,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)? @@ -492,7 +478,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()); @@ -523,7 +509,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) }; @@ -552,7 +538,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)) }, @@ -577,7 +563,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); @@ -594,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 = 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))); + 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), ()))), )) }, @@ -631,7 +615,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 88% rename from crates/pikelet-syntax/src/parse/grammar.lalrpop rename to crates/pikelet-concrete/src/parse/grammar.lalrpop index bd347c228..9b09f065e 100644 --- a/crates/pikelet-syntax/src/parse/grammar.lalrpop +++ b/crates/pikelet-concrete/src/parse/grammar.lalrpop @@ -1,9 +1,9 @@ use codespan::FileMap; use codespan::{ByteIndex, ByteSpan}; -use concrete::{Item, Literal, Pattern, Term, RecordTypeField, RecordField, ReplCommand}; use parse::{LalrpopError, ParseError, Token}; -use {FloatFormat, IntFormat}; +use syntax::{FloatFormat, IntFormat}; +use syntax::concrete::{Item, Literal, Pattern, Term, RecordTypeField, RecordIntroField, ReplCommand}; #[LALR] grammar<'err, 'input>( @@ -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/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 85% rename from crates/pikelet-syntax/src/translation/resugar.rs rename to crates/pikelet-concrete/src/resugar.rs index 855ea05c2..e45c768c9 100644 --- a/crates/pikelet-syntax/src/translation/resugar.rs +++ b/crates/pikelet-concrete/src/resugar.rs @@ -2,9 +2,10 @@ use codespan::{ByteIndex, ByteSpan}; use im; use moniker::{Binder, BoundTerm, Embed, FreeVar, Nest, Scope, Var}; -use concrete; -use core; -use {Label, Level, LevelShift}; +use pikelet_core::syntax::{core, domain}; +use pikelet_core::syntax::{Label, Level, LevelShift}; + +use syntax::{concrete, FloatFormat, IntFormat}; /// The environment used when resugaring from the core to the concrete syntax #[derive(Debug, Clone)] @@ -14,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 { @@ -155,33 +156,34 @@ 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 pikelet_core::syntax::Literal; + + use syntax::concrete::Literal::*; + use syntax::concrete::Pattern; 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, 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)), + 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, 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)), + 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, format) => Literal(Float(span, f64::from(val), format)), - core::Literal::F64(val, format) => Literal(Float(span, val, format)), + Literal::F32(v) => Pattern::Literal(Float(span, f64::from(v), FloatFormat::Dec)), + Literal::F64(v) => Pattern::Literal(Float(span, v, FloatFormat::Dec)), } }, } @@ -445,33 +447,34 @@ 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 pikelet_core::syntax::Literal; + + use syntax::concrete::Literal::*; + use syntax::concrete::Term; 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, 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)), + 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, 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)), + 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, format) => Literal(Float(span, f64::from(val), format)), - core::Literal::F64(val, format) => Literal(Float(span, val, format)), + 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) => { @@ -525,23 +528,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::RecordField::Explicit { - label: (ByteIndex::default(), name), + concrete::RecordIntroField::Explicit { + label: (ByteIndex::default(), label.0.clone()), params: term_params, return_ann: None, term: term_body, @@ -598,14 +598,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 +618,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) } diff --git a/crates/pikelet-concrete/src/syntax/concrete.rs b/crates/pikelet-concrete/src/syntax/concrete.rs new file mode 100644 index 000000000..e351a119f --- /dev/null +++ b/crates/pikelet-concrete/src/syntax/concrete.rs @@ -0,0 +1,677 @@ +//! The concrete syntax of the language + +use codespan::{ByteIndex, ByteSpan}; +use pretty::{BoxDoc, Doc}; +use std::fmt; + +use syntax::{FloatFormat, IntFormat, PRETTY_FALLBACK_WIDTH, PRETTY_INDENT_WIDTH}; + +/// Commands entered in the REPL +#[derive(Debug, Clone)] +pub enum ReplCommand { + /// Evaluate a term + /// + /// ```text + /// + /// ``` + Eval(Box), + /// Show the raw representation of a term + /// + /// ```text + /// :raw + /// ``` + Raw(Box), + /// Show the core representation of a term + /// + /// ```text + /// :core + /// ``` + Core(Box), + /// Print some help about using the REPL + /// + /// ```text + /// :? + /// :h + /// :help + /// ``` + Help, + /// Add a declaration to the REPL environment + /// + /// ```text + ///:let = + /// ``` + Let(String, Box), + /// No command + NoOp, + /// Quit the REPL + /// + /// ```text + /// :q + /// :quit + /// ``` + Quit, + /// Print the type of the term + /// + /// ```text + /// :t + /// :type + /// ``` + TypeOf(Box), + /// Repl commands that could not be parsed correctly + /// + /// This is used for error recovery + Error(ByteSpan), +} + +/// A group of lambda parameters that share an annotation +pub type FunIntroParamGroup = (Vec<(ByteIndex, String)>, Option>); + +/// The parameters to a lambda abstraction +pub type FunIntroParams = Vec; + +/// A group of parameters to a dependent function that share an annotation +pub type FunTypeParamGroup = (Vec<(ByteIndex, String)>, Term); + +/// The parameters to a dependent function type +pub type FunTypeParams = Vec; + +#[derive(Debug, Clone, PartialEq)] +pub struct RecordTypeField { + pub label: (ByteIndex, String), + pub binder: Option<(ByteIndex, String)>, + pub ann: Term, +} + +#[derive(Debug, Clone, PartialEq)] +pub enum RecordIntroField { + Punned { + label: (ByteIndex, String), + shift: Option, + }, + Explicit { + label: (ByteIndex, String), + params: FunIntroParams, + return_ann: Option>, + term: Term, + }, +} + +/// Top-level items within a module +#[derive(Debug, Clone, PartialEq)] +pub enum Item { + /// Declares the type associated with a name, prior to its definition + /// + /// ```text + /// foo : some-type + /// ``` + Declaration { + name: (ByteIndex, String), + ann: Term, + }, + /// Defines the term that should be associated with a name + /// + /// ```text + /// foo = some-body + /// foo x (y : some-type) = some-body + /// ``` + Definition { + name: (ByteIndex, String), + params: FunIntroParams, + return_ann: Option>, + body: Term, + }, + /// Items that could not be correctly parsed + /// + /// This is used for error recovery + Error(ByteSpan), +} + +impl Item { + /// Return the span of source code that this declaration originated from + pub fn span(&self) -> ByteSpan { + match *self { + Item::Definition { + name: (start, _), + body: ref term, + .. + } + | Item::Declaration { + name: (start, _), + ann: ref term, + } => ByteSpan::new(start, term.span().end()), + 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) + } +} + +/// Literals +#[derive(Debug, Clone, PartialEq)] +pub enum Literal { + /// String literals + // TODO: Preserve escapes? + String(ByteSpan, String), + /// Character literals + // TODO: Preserve escapes? + Char(ByteSpan, char), + /// Integer literals + // TODO: Preserve digit separators? + Int(ByteSpan, u64, IntFormat), + /// Floating point literals + // TODO: Preserve digit separators? + Float(ByteSpan, f64, FloatFormat), +} + +impl Literal { + /// Return the span of source code that the literal originated from + pub fn span(&self) -> ByteSpan { + match *self { + Literal::String(span, _) + | Literal::Char(span, _) + | Literal::Int(span, _, _) + | 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 +#[derive(Debug, Clone, PartialEq)] +pub enum Pattern { + /// A term that is surrounded with parentheses + /// + /// ```text + /// (p) + /// ``` + Parens(ByteSpan, Box), + /// Patterns annotated with types + /// + /// ```text + /// p : t + /// ``` + Ann(Box, Box), + /// Literal patterns + Literal(Literal), + /// Patterns that either introduce bound variables, or match by structural + /// equality with a constant in-scope + /// + /// ```text + /// x + /// true + /// false + /// ``` + Name(ByteSpan, String, Option), + /// Terms that could not be correctly parsed + /// + /// This is used for error recovery + Error(ByteSpan), +} + +impl Pattern { + /// Return the span of source code that this pattern originated from + pub fn span(&self) -> ByteSpan { + match *self { + Pattern::Parens(span, _) | Pattern::Name(span, _, _) | Pattern::Error(span) => span, + Pattern::Ann(ref pattern, ref ty) => pattern.span().to(ty.span()), + 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 +#[derive(Debug, Clone, PartialEq)] +pub enum Term { + /// A term that is surrounded with parentheses + /// + /// ```text + /// (e) + /// ``` + Parens(ByteSpan, Box), + /// A term annotated with a type + /// + /// ```text + /// e : t + /// ``` + Ann(Box, Box), + /// Type of types + /// + /// ```text + /// Type + /// ``` + Universe(ByteSpan, Option), + /// Literals + Literal(Literal), + /// Array literals + ArrayIntro(ByteSpan, Vec), + /// Holes + /// + /// ```text + /// _ + /// ``` + Hole(ByteSpan), + /// Names + /// + /// ```text + /// x + /// x^1 + /// ``` + Name(ByteSpan, String, Option), + /// An imported definition + /// + /// ```text + /// import "prelude" + /// ``` + Import(ByteSpan, ByteSpan, String), + /// Dependent function type + /// + /// ```text + /// (x : t1) -> t2 + /// (x y : t1) -> t2 + /// ``` + FunType(ByteIndex, FunTypeParams, Box), + /// Non-Dependent function type + /// + /// ```text + /// t1 -> t2 + /// ``` + FunArrow(Box, Box), + /// Function introduction + /// + /// ```text + /// \x => t + /// \x y => t + /// \x : t1 => t2 + /// \(x : t1) y (z : t2) => t3 + /// \(x y : t1) => t3 + /// ``` + FunIntro(ByteIndex, FunIntroParams, Box), + /// Function application + /// + /// ```text + /// e1 e2 + /// ``` + FunApp(Box, Vec), + /// Let binding + /// + /// ```text + /// let x : S32 + /// x = 1 + /// in + /// x + /// ``` + Let(ByteIndex, Vec, Box), + /// Where expressions + /// + /// ```text + /// id "hello" + /// where { + /// id : (A : Type) -> A -> A; + /// id A x = x; + /// } + /// ``` + Where(Box, Vec, ByteIndex), + /// If expression + /// + /// ```text + /// if t1 then t2 else t3 + /// ``` + If(ByteIndex, Box, Box, Box), + /// Case expression + /// + /// ```text + /// case t1 { pat => t2; .. } + /// ``` + Case(ByteSpan, Box, Vec<(Pattern, Term)>), + /// Record type + /// + /// ```text + /// Record { x : t1, .. } + /// ``` + RecordType(ByteSpan, Vec), + /// Record introduction + /// + /// ```text + /// record { x = t1, .. } + /// record { id (a : Type) (x : a) : a = x, .. } + /// ``` + RecordIntro(ByteSpan, Vec), + /// Record field projection + /// + /// ```text + /// e.l + /// e.l^1 + /// ``` + RecordProj(ByteSpan, Box, ByteIndex, String, Option), + /// Terms that could not be correctly parsed + /// + /// This is used for error recovery + Error(ByteSpan), +} + +impl Term { + /// Return the span of source code that this term originated from + pub fn span(&self) -> ByteSpan { + match *self { + Term::Parens(span, ..) + | Term::Universe(span, ..) + | Term::Hole(span) + | Term::Name(span, ..) + | Term::Import(span, ..) + | Term::Case(span, ..) + | Term::RecordType(span, ..) + | Term::RecordIntro(span, ..) + | Term::RecordProj(span, ..) + | Term::ArrayIntro(span, ..) + | Term::Error(span) => span, + Term::Literal(ref literal) => literal.span(), + Term::FunType(start, _, ref body) + | Term::FunIntro(start, _, ref body) + | Term::Let(start, _, ref body) + | Term::If(start, _, _, ref body) => ByteSpan::new(start, body.span().end()), + Term::Where(ref expr, _, end) => ByteSpan::new(expr.span().start(), end), + Term::Ann(ref term, ref ty) => term.span().to(ty.span()), + Term::FunArrow(ref ann, ref body) => ann.span().to(body.span()), + 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) + } +} + +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/lib.rs b/crates/pikelet-concrete/src/syntax/mod.rs similarity index 50% rename from crates/pikelet-syntax/src/lib.rs rename to crates/pikelet-concrete/src/syntax/mod.rs index fd7d3f89a..f07332765 100644 --- a/crates/pikelet-syntax/src/lib.rs +++ b/crates/pikelet-concrete/src/syntax/mod.rs @@ -1,94 +1,16 @@ -//! 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 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 parse; -pub mod pretty; pub mod raw; -pub mod translation; - -/// A universe level -#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, BoundTerm)] -pub struct Level(pub u32); - -impl Level { - pub fn succ(self) -> Level { - Level(self.0 + 1) - } -} - -impl From for Level { - fn from(src: u32) -> Level { - Level(src) - } -} - -impl fmt::Display for Level { - fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { - write!(f, "{}", self.0) - } -} - -/// A shift in universe level -#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, BoundTerm, BoundPattern)] -pub struct LevelShift(pub u32); - -impl From for LevelShift { - fn from(src: u32) -> LevelShift { - LevelShift(src) - } -} - -impl fmt::Display for LevelShift { - fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { - write!(f, "{}", self.0) - } -} - -impl Add for LevelShift { - type Output = LevelShift; - fn add(self, other: LevelShift) -> LevelShift { - LevelShift(self.0 + other.0) - } -} - -impl AddAssign for LevelShift { - fn add_assign(&mut self, other: LevelShift) { - self.0 += other.0; - } -} +const PRETTY_INDENT_WIDTH: usize = 4; -impl Add for Level { - type Output = Level; - - fn add(self, other: LevelShift) -> Level { - Level(self.0 + other.0) - } -} - -impl AddAssign for Level { - fn add_assign(&mut self, other: LevelShift) { - self.0 += other.0; - } -} +/// 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; #[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord)] pub enum IntFormat { @@ -151,21 +73,3 @@ impl BoundPattern for FloatFormat { 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 -#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, BoundPattern, BoundTerm)] -pub struct Label(pub String); - -impl From for Label { - fn from(src: String) -> Label { - Label(src) - } -} - -impl fmt::Display for Label { - fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { - write!(f, "{}", self.0) - } -} diff --git a/crates/pikelet-concrete/src/syntax/raw.rs b/crates/pikelet-concrete/src/syntax/raw.rs new file mode 100644 index 000000000..0210a8f59 --- /dev/null +++ b/crates/pikelet-concrete/src/syntax/raw.rs @@ -0,0 +1,394 @@ +//! The syntax of the language, unchecked and with implicit parts that need to +//! be elaborated in a type-directed way during type checking and inference + +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 pikelet_core::syntax::{Label, Level, LevelShift}; + +use syntax::{FloatFormat, IntFormat, PRETTY_FALLBACK_WIDTH}; + +/// Literals +#[derive(Debug, Clone, PartialEq, PartialOrd, BoundTerm, BoundPattern)] +pub enum Literal { + String(ByteSpan, String), + Char(ByteSpan, char), + Int(ByteSpan, u64, IntFormat), + Float(ByteSpan, f64, FloatFormat), +} + +impl Literal { + /// Return the span of source code that the literal originated from + pub fn span(&self) -> ByteSpan { + match *self { + Literal::String(span, ..) + | Literal::Char(span, ..) + | Literal::Int(span, ..) + | 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) + } +} + +#[derive(Debug, Clone, PartialEq, BoundPattern)] +pub enum Pattern { + /// Patterns annotated with types + Ann(RcPattern, Embed), + /// Patterns that bind variables + Binder(ByteSpan, Binder), + /// Patterns to be compared structurally with a variable in scope + Var(ByteSpan, Embed>, LevelShift), + /// Literal patterns + Literal(Literal), +} + +impl Pattern { + /// Return the span of source code that this pattern originated from + pub fn span(&self) -> ByteSpan { + match *self { + Pattern::Ann(ref pattern, Embed(ref ty)) => pattern.span().to(ty.span()), + Pattern::Var(span, _, _) | Pattern::Binder(span, _) => span, + 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) + } +} + +/// Reference counted patterns +#[derive(Debug, Clone, PartialEq, BoundPattern)] +pub struct RcPattern { + pub inner: Rc, +} + +impl From for RcPattern { + fn from(src: Pattern) -> RcPattern { + RcPattern { + inner: Rc::new(src), + } + } +} + +impl ops::Deref for RcPattern { + type Target = Pattern; + + fn deref(&self) -> &Pattern { + &self.inner + } +} + +impl fmt::Display for RcPattern { + fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { + fmt::Display::fmt(&self.inner, f) + } +} + +/// Terms, unchecked and with implicit syntax that needs to be elaborated +/// +/// For now the only implicit syntax we have is holes and lambdas that lack a +/// type annotation. +#[derive(Debug, Clone, PartialEq, BoundTerm)] +pub enum Term { + /// A term annotated with a type + Ann(RcTerm, RcTerm), + /// Universes + Universe(ByteSpan, Level), + /// Literals + Literal(Literal), + /// A hole + Hole(ByteSpan), + /// A variable + Var(ByteSpan, Var, LevelShift), + /// An imported definition + Import(ByteSpan, ByteSpan, String), + /// Dependent function types + FunType(ByteSpan, Scope<(Binder, Embed), RcTerm>), + /// Function introductions + FunIntro(ByteSpan, Scope<(Binder, Embed), RcTerm>), + /// Function application + FunApp(RcTerm, RcTerm), + /// Dependent record types + RecordType( + ByteSpan, + Scope, Embed)>, ()>, + ), + /// Record introductions + RecordIntro(ByteSpan, Vec<(Label, RcTerm)>), + /// Record field projection + RecordProj(ByteSpan, RcTerm, ByteSpan, Label, LevelShift), + /// Case expressions + Case(ByteSpan, RcTerm, Vec>), + /// Array literals + ArrayIntro(ByteSpan, Vec), + /// Let bindings + Let( + ByteSpan, + Scope, Embed<(RcTerm, RcTerm)>)>, RcTerm>, + ), +} + +impl Term { + pub fn span(&self) -> ByteSpan { + match *self { + Term::Universe(span, ..) + | Term::Hole(span) + | Term::Var(span, ..) + | Term::Import(span, ..) + | Term::FunType(span, ..) + | Term::FunIntro(span, ..) + | Term::RecordType(span, ..) + | Term::RecordIntro(span, ..) + | Term::RecordProj(span, ..) + | Term::Case(span, ..) + | Term::ArrayIntro(span, ..) + | Term::Let(span, ..) => span, + Term::Literal(ref literal) => literal.span(), + Term::Ann(ref expr, ref ty) => expr.span().to(ty.span()), + 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 fields) => Doc::nil() + .append("record {") + .append(Doc::space()) + .append(Doc::intersperse( + 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()) + .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) + } +} + +/// Reference counted terms +#[derive(Debug, Clone, PartialEq, BoundTerm)] +pub struct RcTerm { + pub inner: Rc, +} + +impl From for RcTerm { + fn from(src: Term) -> RcTerm { + RcTerm { + inner: Rc::new(src), + } + } +} + +impl ops::Deref for RcTerm { + type Target = Term; + + fn deref(&self) -> &Term { + &self.inner + } +} + +impl fmt::Display for RcTerm { + fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { + fmt::Display::fmt(&self.inner, f) + } +} 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 95% rename from crates/pikelet-elaborate/tests/infer.rs rename to crates/pikelet-concrete/tests/infer.rs index 152d80d40..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,10 +48,10 @@ 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), + 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,10 +588,10 @@ 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), + 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,9 +896,9 @@ 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), + 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 1e205422d..800daf855 100644 --- a/crates/pikelet-elaborate/tests/normalize.rs +++ b/crates/pikelet-concrete/tests/normalize.rs @@ -2,14 +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::{Neutral, RcNeutral, RcTerm, RcValue, Term, Value}; +use pikelet_concrete::elaborate::Context; +use pikelet_core::syntax::core::{RcTerm, Term}; +use pikelet_core::syntax::domain::{Neutral, RcNeutral, RcValue, Value}; mod support; @@ -21,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 94% rename from crates/pikelet-syntax/tests/resugar.rs rename to crates/pikelet-concrete/tests/resugar.rs index 09ced7460..e4672071a 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, Literal}; fn span() -> ByteSpan { ByteSpan::default() @@ -51,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); @@ -59,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); @@ -67,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())); @@ -185,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( @@ -280,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-elaborate/tests/support/mod.rs b/crates/pikelet-concrete/tests/support/mod.rs similarity index 74% rename from crates/pikelet-elaborate/tests/support/mod.rs rename to crates/pikelet-concrete/tests/support/mod.rs index b5946fec2..2e832d1c9 100644 --- a/crates/pikelet-elaborate/tests/support/mod.rs +++ b/crates/pikelet-concrete/tests/support/mod.rs @@ -4,11 +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, 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()); @@ -29,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); @@ -41,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), } } @@ -55,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 65% rename from crates/pikelet-elaborate/src/normalize.rs rename to crates/pikelet-core/src/nbe.rs index 7abbb55ef..f586419ee 100644 --- a/crates/pikelet-elaborate/src/normalize.rs +++ b/crates/pikelet-core/src/nbe.rs @@ -1,16 +1,38 @@ use moniker::{Binder, Embed, FreeVar, Nest, Scope, Var}; -use pikelet_syntax::core::{ - Head, Neutral, Pattern, RcNeutral, RcPattern, RcTerm, RcValue, Term, 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))), @@ -19,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) }, @@ -31,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(), @@ -55,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 => {}, @@ -107,7 +126,7 @@ pub fn nf_term(context: &Context, term: &RcTerm) -> Result Err(InternalError::ArgumentAppliedToNonFunction), + _ => Err(NbeError::new("argument applied to non function")), } }, @@ -117,11 +136,11 @@ pub fn nf_term(context: &Context, term: &RcTerm) -> Result Result>()?, ); @@ -141,36 +160,27 @@ pub fn nf_term(context: &Context, term: &RcTerm) -> Result { - let (fields, ()) = scope.clone().unbind(); - let fields = Nest::new( - fields - .unnest() - .into_iter() - .map(|(label, binder, Embed(term))| { - Ok((label, binder, Embed(nf_term(context, &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 Term::RecordProj(ref expr, ref label, shift) => { - 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)), 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()); } } @@ -178,14 +188,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( @@ -195,7 +206,7 @@ pub fn nf_term(context: &Context, term: &RcTerm) -> Result>()?, )), @@ -204,15 +215,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")) } }, @@ -220,7 +231,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::>()?, ))), } @@ -229,19 +240,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 51% rename from crates/pikelet-syntax/src/core.rs rename to crates/pikelet-core/src/syntax/core.rs index 1ce700c37..57cdadefa 100644 --- a/crates/pikelet-syntax/src/core.rs +++ b/crates/pikelet-core/src/syntax/core.rs @@ -1,38 +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 pretty::{self, ToDoc}; -use {FloatFormat, IntFormat, Label, Level, LevelShift}; - -/// 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, 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), -} - -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::domain::{Head, Neutral, Value}; +use syntax::{Label, Level, LevelShift, Literal, PRETTY_FALLBACK_WIDTH}; #[derive(Debug, Clone, PartialEq, BoundPattern)] pub enum Pattern { @@ -46,9 +21,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) } } @@ -102,7 +100,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 @@ -121,11 +119,174 @@ 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 fields) => Doc::nil() + .append("record {") + .append(Doc::space()) + .append(Doc::intersperse( + 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()) + .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) } } @@ -182,9 +343,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) => { @@ -202,20 +361,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), @@ -263,254 +416,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 @@ -548,20 +453,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 new file mode 100644 index 000000000..4ed75f97c --- /dev/null +++ b/crates/pikelet-core/src/syntax/domain.rs @@ -0,0 +1,244 @@ +//! The semantic domain of the language + +use moniker::{Binder, Embed, FreeVar, Nest, Scope, Var}; +use std::ops; +use std::rc::Rc; + +use syntax::core::{RcPattern, RcTerm, Term}; +use syntax::{Label, Level, LevelShift, Literal}; + +/// 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(Vec<(Label, RcValue)>), + /// 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) => 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, + } + } + + 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, + }) + } +} + +/// 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) => { + 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); + } + }, + 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 + } +} + +/// 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())) + } +} + +/// 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-core/src/syntax/mod.rs b/crates/pikelet-core/src/syntax/mod.rs new file mode 100644 index 000000000..ba98302be --- /dev/null +++ b/crates/pikelet-core/src/syntax/mod.rs @@ -0,0 +1,160 @@ +use pretty::{BoxDoc, Doc}; +use std::fmt; +use std::ops::{Add, AddAssign}; + +pub mod core; +pub mod domain; + +/// 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(), + } + } +} + +/// 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); + +impl Level { + pub fn succ(self) -> Level { + Level(self.0 + 1) + } +} + +impl From for Level { + fn from(src: u32) -> Level { + Level(src) + } +} + +impl fmt::Display for Level { + fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { + write!(f, "{}", self.0) + } +} + +/// A shift in universe level +#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, BoundTerm, BoundPattern)] +pub struct LevelShift(pub u32); + +impl From for LevelShift { + fn from(src: u32) -> LevelShift { + LevelShift(src) + } +} + +impl fmt::Display for LevelShift { + fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { + write!(f, "{}", self.0) + } +} + +impl Add for LevelShift { + type Output = LevelShift; + + fn add(self, other: LevelShift) -> LevelShift { + LevelShift(self.0 + other.0) + } +} + +impl AddAssign for LevelShift { + fn add_assign(&mut self, other: LevelShift) { + self.0 += other.0; + } +} + +impl Add for Level { + type Output = Level; + + fn add(self, other: LevelShift) -> Level { + Level(self.0 + other.0) + } +} + +impl AddAssign for Level { + fn add_assign(&mut self, other: LevelShift) { + self.0 += other.0; + } +} + +/// A label that describes the name of a field in a record +/// +/// Labels are significant when comparing for alpha-equality +#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, BoundPattern, BoundTerm)] +pub struct Label(pub String); + +impl From for Label { + fn from(src: String) -> Label { + Label(src) + } +} + +impl fmt::Display for Label { + fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { + write!(f, "{}", self.0) + } +} 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 6f10a7e0f..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::core::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, 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()); } @@ -211,7 +213,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,12 +227,16 @@ impl Driver { pub fn infer_term( &self, raw_term: &raw::RcTerm, - ) -> Result<(core::RcTerm, core::RcType), Vec> { - pikelet_elaborate::infer_term(&self.context, &raw_term).map_err(|e| vec![e.to_diagnostic()]) + ) -> Result<(core::RcTerm, domain::RcType), Vec> { + 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()]) + pub fn nf_term(&self, term: &core::RcTerm) -> Result> { + 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 05db154e1..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,13 +179,12 @@ 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_syntax::pretty::{self, ToDoc}; + use pikelet_concrete::syntax::concrete::{ReplCommand, Term}; fn term_width() -> 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); @@ -211,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/concrete.rs b/crates/pikelet-syntax/src/concrete.rs deleted file mode 100644 index 80d797ca8..000000000 --- a/crates/pikelet-syntax/src/concrete.rs +++ /dev/null @@ -1,387 +0,0 @@ -//! The concrete syntax of the language - -use codespan::{ByteIndex, ByteSpan}; -use std::fmt; - -use pretty::{self, ToDoc}; -use {FloatFormat, IntFormat}; - -/// Commands entered in the REPL -#[derive(Debug, Clone)] -pub enum ReplCommand { - /// Evaluate a term - /// - /// ```text - /// - /// ``` - Eval(Box), - /// Show the raw representation of a term - /// - /// ```text - /// :raw - /// ``` - Raw(Box), - /// Show the core representation of a term - /// - /// ```text - /// :core - /// ``` - Core(Box), - /// Print some help about using the REPL - /// - /// ```text - /// :? - /// :h - /// :help - /// ``` - Help, - /// Add a declaration to the REPL environment - /// - /// ```text - ///:let = - /// ``` - Let(String, Box), - /// No command - NoOp, - /// Quit the REPL - /// - /// ```text - /// :q - /// :quit - /// ``` - Quit, - /// Print the type of the term - /// - /// ```text - /// :t - /// :type - /// ``` - TypeOf(Box), - /// Repl commands that could not be parsed correctly - /// - /// This is used for error recovery - Error(ByteSpan), -} - -/// A group of lambda parameters that share an annotation -pub type FunIntroParamGroup = (Vec<(ByteIndex, String)>, Option>); - -/// The parameters to a lambda abstraction -pub type FunIntroParams = Vec; - -/// A group of parameters to a dependent function that share an annotation -pub type FunTypeParamGroup = (Vec<(ByteIndex, String)>, Term); - -/// The parameters to a dependent function type -pub type FunTypeParams = Vec; - -#[derive(Debug, Clone, PartialEq)] -pub struct RecordTypeField { - pub label: (ByteIndex, String), - pub binder: Option<(ByteIndex, String)>, - pub ann: Term, -} - -#[derive(Debug, Clone, PartialEq)] -pub enum RecordField { - Punned { - label: (ByteIndex, String), - shift: Option, - }, - Explicit { - label: (ByteIndex, String), - params: FunIntroParams, - return_ann: Option>, - term: Term, - }, -} - -/// Top-level items within a module -#[derive(Debug, Clone, PartialEq)] -pub enum Item { - /// Declares the type associated with a name, prior to its definition - /// - /// ```text - /// foo : some-type - /// ``` - Declaration { - name: (ByteIndex, String), - ann: Term, - }, - /// Defines the term that should be associated with a name - /// - /// ```text - /// foo = some-body - /// foo x (y : some-type) = some-body - /// ``` - Definition { - name: (ByteIndex, String), - params: FunIntroParams, - return_ann: Option>, - body: Term, - }, - /// Items that could not be correctly parsed - /// - /// This is used for error recovery - Error(ByteSpan), -} - -impl Item { - /// Return the span of source code that this declaration originated from - pub fn span(&self) -> ByteSpan { - match *self { - Item::Definition { - name: (start, _), - body: ref term, - .. - } - | Item::Declaration { - name: (start, _), - ann: ref term, - } => ByteSpan::new(start, term.span().end()), - Item::Error(span) => span, - } - } -} - -impl fmt::Display for Item { - fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { - self.to_doc().group().render_fmt(pretty::FALLBACK_WIDTH, f) - } -} - -/// Literals -#[derive(Debug, Clone, PartialEq)] -pub enum Literal { - /// String literals - // TODO: Preserve escapes? - String(ByteSpan, String), - /// Character literals - // TODO: Preserve escapes? - Char(ByteSpan, char), - /// Integer literals - // TODO: Preserve digit separators? - Int(ByteSpan, u64, IntFormat), - /// Floating point literals - // TODO: Preserve digit separators? - Float(ByteSpan, f64, FloatFormat), -} - -impl Literal { - /// Return the span of source code that the literal originated from - pub fn span(&self) -> ByteSpan { - match *self { - Literal::String(span, _) - | Literal::Char(span, _) - | Literal::Int(span, _, _) - | Literal::Float(span, _, _) => span, - } - } -} - -/// Patterns -#[derive(Debug, Clone, PartialEq)] -pub enum Pattern { - /// A term that is surrounded with parentheses - /// - /// ```text - /// (p) - /// ``` - Parens(ByteSpan, Box), - /// Patterns annotated with types - /// - /// ```text - /// p : t - /// ``` - Ann(Box, Box), - /// Literal patterns - Literal(Literal), - /// Patterns that either introduce bound variables, or match by structural - /// equality with a constant in-scope - /// - /// ```text - /// x - /// true - /// false - /// ``` - Name(ByteSpan, String, Option), - /// Terms that could not be correctly parsed - /// - /// This is used for error recovery - Error(ByteSpan), -} - -impl Pattern { - /// Return the span of source code that this pattern originated from - pub fn span(&self) -> ByteSpan { - match *self { - Pattern::Parens(span, _) | Pattern::Name(span, _, _) | Pattern::Error(span) => span, - Pattern::Ann(ref pattern, ref ty) => pattern.span().to(ty.span()), - Pattern::Literal(ref literal) => literal.span(), - } - } -} - -/// Terms -#[derive(Debug, Clone, PartialEq)] -pub enum Term { - /// A term that is surrounded with parentheses - /// - /// ```text - /// (e) - /// ``` - Parens(ByteSpan, Box), - /// A term annotated with a type - /// - /// ```text - /// e : t - /// ``` - Ann(Box, Box), - /// Type of types - /// - /// ```text - /// Type - /// ``` - Universe(ByteSpan, Option), - /// Literals - Literal(Literal), - /// Array literals - ArrayIntro(ByteSpan, Vec), - /// Holes - /// - /// ```text - /// _ - /// ``` - Hole(ByteSpan), - /// Names - /// - /// ```text - /// x - /// x^1 - /// ``` - Name(ByteSpan, String, Option), - /// An imported definition - /// - /// ```text - /// import "prelude" - /// ``` - Import(ByteSpan, ByteSpan, String), - /// Dependent function type - /// - /// ```text - /// (x : t1) -> t2 - /// (x y : t1) -> t2 - /// ``` - FunType(ByteIndex, FunTypeParams, Box), - /// Non-Dependent function type - /// - /// ```text - /// t1 -> t2 - /// ``` - FunArrow(Box, Box), - /// Function introduction - /// - /// ```text - /// \x => t - /// \x y => t - /// \x : t1 => t2 - /// \(x : t1) y (z : t2) => t3 - /// \(x y : t1) => t3 - /// ``` - FunIntro(ByteIndex, FunIntroParams, Box), - /// Function application - /// - /// ```text - /// e1 e2 - /// ``` - FunApp(Box, Vec), - /// Let binding - /// - /// ```text - /// let x : S32 - /// x = 1 - /// in - /// x - /// ``` - Let(ByteIndex, Vec, Box), - /// Where expressions - /// - /// ```text - /// id "hello" - /// where { - /// id : (A : Type) -> A -> A; - /// id A x = x; - /// } - /// ``` - Where(Box, Vec, ByteIndex), - /// If expression - /// - /// ```text - /// if t1 then t2 else t3 - /// ``` - If(ByteIndex, Box, Box, Box), - /// Case expression - /// - /// ```text - /// case t1 { pat => t2; .. } - /// ``` - Case(ByteSpan, Box, Vec<(Pattern, Term)>), - /// Record type - /// - /// ```text - /// Record { x : t1, .. } - /// ``` - RecordType(ByteSpan, Vec), - /// Record introduction - /// - /// ```text - /// record { x = t1, .. } - /// record { id (a : Type) (x : a) : a = x, .. } - /// ``` - RecordIntro(ByteSpan, Vec), - /// Record field projection - /// - /// ```text - /// e.l - /// e.l^1 - /// ``` - RecordProj(ByteSpan, Box, ByteIndex, String, Option), - /// Terms that could not be correctly parsed - /// - /// This is used for error recovery - Error(ByteSpan), -} - -impl Term { - /// Return the span of source code that this term originated from - pub fn span(&self) -> ByteSpan { - match *self { - Term::Parens(span, ..) - | Term::Universe(span, ..) - | Term::Hole(span) - | Term::Name(span, ..) - | Term::Import(span, ..) - | Term::Case(span, ..) - | Term::RecordType(span, ..) - | Term::RecordIntro(span, ..) - | Term::RecordProj(span, ..) - | Term::ArrayIntro(span, ..) - | Term::Error(span) => span, - Term::Literal(ref literal) => literal.span(), - Term::FunType(start, _, ref body) - | Term::FunIntro(start, _, ref body) - | Term::Let(start, _, ref body) - | Term::If(start, _, _, ref body) => ByteSpan::new(start, body.span().end()), - Term::Where(ref expr, _, end) => ByteSpan::new(expr.span().start(), end), - Term::Ann(ref term, ref ty) => term.span().to(ty.span()), - Term::FunArrow(ref ann, ref body) => ann.span().to(body.span()), - Term::FunApp(ref head, ref arg) => head.span().to(arg.last().unwrap().span()), - } - } -} - -impl fmt::Display for Term { - fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { - self.to_doc().group().render_fmt(pretty::FALLBACK_WIDTH, f) - } -} 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 05d725c35..000000000 --- a/crates/pikelet-syntax/src/pretty/core.rs +++ /dev/null @@ -1,405 +0,0 @@ -//! Pretty printing for the core syntax - -use super::pretty::Doc; -use moniker::{Binder, Embed, Var}; -use std::iter; - -use core::{Head, Literal, Neutral, Pattern, Term, Value}; -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("]"), - } - } -} - -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), - } - } -} 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 deleted file mode 100644 index fa018230e..000000000 --- a/crates/pikelet-syntax/src/raw.rs +++ /dev/null @@ -1,198 +0,0 @@ -//! The syntax of the language, unchecked and with implicit parts that need to -//! be elaborated in a type-directed way during type checking and inference - -use codespan::ByteSpan; -use moniker::{Binder, Embed, Nest, Scope, Var}; -use std::fmt; -use std::ops; -use std::rc::Rc; - -use pretty::{self, ToDoc}; -use {FloatFormat, IntFormat, Label, Level, LevelShift}; - -/// Literals -#[derive(Debug, Clone, PartialEq, PartialOrd, BoundTerm, BoundPattern)] -pub enum Literal { - String(ByteSpan, String), - Char(ByteSpan, char), - Int(ByteSpan, u64, IntFormat), - Float(ByteSpan, f64, FloatFormat), -} - -impl Literal { - /// Return the span of source code that the literal originated from - pub fn span(&self) -> ByteSpan { - match *self { - Literal::String(span, ..) - | Literal::Char(span, ..) - | Literal::Int(span, ..) - | Literal::Float(span, ..) => span, - } - } -} - -impl fmt::Display for Literal { - fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { - self.to_doc().group().render_fmt(pretty::FALLBACK_WIDTH, f) - } -} - -#[derive(Debug, Clone, PartialEq, BoundPattern)] -pub enum Pattern { - /// Patterns annotated with types - Ann(RcPattern, Embed), - /// Patterns that bind variables - Binder(ByteSpan, Binder), - /// Patterns to be compared structurally with a variable in scope - Var(ByteSpan, Embed>, LevelShift), - /// Literal patterns - Literal(Literal), -} - -impl Pattern { - /// Return the span of source code that this pattern originated from - pub fn span(&self) -> ByteSpan { - match *self { - Pattern::Ann(ref pattern, Embed(ref ty)) => pattern.span().to(ty.span()), - Pattern::Var(span, _, _) | Pattern::Binder(span, _) => span, - Pattern::Literal(ref literal) => literal.span(), - } - } -} - -impl fmt::Display for Pattern { - fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { - self.to_doc().group().render_fmt(pretty::FALLBACK_WIDTH, f) - } -} - -/// Reference counted patterns -#[derive(Debug, Clone, PartialEq, BoundPattern)] -pub struct RcPattern { - pub inner: Rc, -} - -impl From for RcPattern { - fn from(src: Pattern) -> RcPattern { - RcPattern { - inner: Rc::new(src), - } - } -} - -impl ops::Deref for RcPattern { - type Target = Pattern; - - fn deref(&self) -> &Pattern { - &self.inner - } -} - -impl fmt::Display for RcPattern { - fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { - fmt::Display::fmt(&self.inner, f) - } -} - -/// Terms, unchecked and with implicit syntax that needs to be elaborated -/// -/// For now the only implicit syntax we have is holes and lambdas that lack a -/// type annotation. -#[derive(Debug, Clone, PartialEq, BoundTerm)] -pub enum Term { - /// A term annotated with a type - Ann(RcTerm, RcTerm), - /// Universes - Universe(ByteSpan, Level), - /// Literals - Literal(Literal), - /// A hole - Hole(ByteSpan), - /// A variable - Var(ByteSpan, Var, LevelShift), - /// An imported definition - Import(ByteSpan, ByteSpan, String), - /// Dependent function types - FunType(ByteSpan, Scope<(Binder, Embed), RcTerm>), - /// Function introductions - FunIntro(ByteSpan, Scope<(Binder, Embed), RcTerm>), - /// Function application - FunApp(RcTerm, RcTerm), - /// Dependent record types - RecordType( - ByteSpan, - Scope, Embed)>, ()>, - ), - /// Record introductions - RecordIntro( - ByteSpan, - Scope, Embed)>, ()>, - ), - /// Record field projection - RecordProj(ByteSpan, RcTerm, ByteSpan, Label, LevelShift), - /// Case expressions - Case(ByteSpan, RcTerm, Vec>), - /// Array literals - ArrayIntro(ByteSpan, Vec), - /// Let bindings - Let( - ByteSpan, - Scope, Embed<(RcTerm, RcTerm)>)>, RcTerm>, - ), -} - -impl Term { - pub fn span(&self) -> ByteSpan { - match *self { - Term::Universe(span, ..) - | Term::Hole(span) - | Term::Var(span, ..) - | Term::Import(span, ..) - | Term::FunType(span, ..) - | Term::FunIntro(span, ..) - | Term::RecordType(span, ..) - | Term::RecordIntro(span, ..) - | Term::RecordProj(span, ..) - | Term::Case(span, ..) - | Term::ArrayIntro(span, ..) - | Term::Let(span, ..) => span, - Term::Literal(ref literal) => literal.span(), - Term::Ann(ref expr, ref ty) => expr.span().to(ty.span()), - Term::FunApp(ref head, ref arg) => head.span().to(arg.span()), - } - } -} - -impl fmt::Display for Term { - fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { - self.to_doc().group().render_fmt(pretty::FALLBACK_WIDTH, f) - } -} - -/// Reference counted terms -#[derive(Debug, Clone, PartialEq, BoundTerm)] -pub struct RcTerm { - pub inner: Rc, -} - -impl From for RcTerm { - fn from(src: Term) -> RcTerm { - RcTerm { - inner: Rc::new(src), - } - } -} - -impl ops::Deref for RcTerm { - type Target = Term; - - fn deref(&self) -> &Term { - &self.inner - } -} - -impl fmt::Display for RcTerm { - fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { - fmt::Display::fmt(&self.inner, f) - } -} 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};