diff --git a/doc/roadmap.md b/doc/roadmap.md index db5bc87ad..49e2db599 100644 --- a/doc/roadmap.md +++ b/doc/roadmap.md @@ -39,14 +39,14 @@ - [ ] refinement types - [x] match expressions - [x] single-layer pattern matching - - [ ] multi-layer pattern matching + - [x] multi-layer pattern matching - [ ] dependent pattern matching -- [ ] patterns +- [x] patterns - [x] wildcard patterns - [x] named patterns - [x] annotated patterns - [x] numeric literal patterns - - [ ] record literal patterns + - [x] record literal patterns - [ ] invertible format descriptions ## Implementation diff --git a/fathom/src/core.rs b/fathom/src/core.rs index 11920930b..34436d836 100644 --- a/fathom/src/core.rs +++ b/fathom/src/core.rs @@ -2,7 +2,9 @@ use std::fmt; -use crate::env::{Index, Level}; +use scoped_arena::Scope; + +use crate::env::{EnvLen, Index, Level}; use crate::source::{Span, StringId}; pub mod binary; @@ -205,6 +207,10 @@ pub enum Term<'arena> { } impl<'arena> Term<'arena> { + pub fn error(span: impl Into) -> Self { + Self::Prim(span.into(), Prim::ReportedError) + } + /// Get the source span of the term. pub fn span(&self) -> Span { match self { @@ -279,6 +285,155 @@ impl<'arena> Term<'arena> { pub fn is_error(&self) -> bool { matches!(self, Term::Prim(_, Prim::ReportedError)) } + + // TODO: Add a new `Weaken` variant to `core::Term` instead of eagerly + // traversing the term? See [Andras Kovacs’ staged language](https://github.com/AndrasKovacs/staged/blob/9e381eb162f44912d70fb843c4ca6567b0d1683a/demo/Syntax.hs#L52) for an example + pub fn shift(&self, scope: &'arena Scope<'arena>, amount: EnvLen) -> Term<'arena> { + self.shift_inner(scope, Index::last(), amount) + } + + /// Increment all `LocalVar`s greater than or equal to `min` by `amount` + fn shift_inner( + &self, + scope: &'arena Scope<'arena>, + mut min: Index, + amount: EnvLen, + ) -> Term<'arena> { + // Skip traversing and rebuilding the term if it would make no change. Increases + // sharing. + if amount == EnvLen::new() { + return self.clone(); + } + + match self { + Term::LocalVar(span, var) if *var >= min => Term::LocalVar(*span, *var + amount), + Term::LocalVar(..) + | Term::ItemVar(..) + | Term::MetaVar(..) + | Term::InsertedMeta(..) + | Term::Prim(..) + | Term::ConstLit(..) + | Term::Universe(..) => self.clone(), + Term::Ann(span, expr, r#type) => Term::Ann( + *span, + scope.to_scope(expr.shift_inner(scope, min, amount)), + scope.to_scope(r#type.shift_inner(scope, min, amount)), + ), + Term::Let(span, name, def_type, def_expr, body) => Term::Let( + *span, + *name, + scope.to_scope(def_type.shift_inner(scope, min, amount)), + scope.to_scope(def_expr.shift_inner(scope, min, amount)), + scope.to_scope(body.shift_inner(scope, min.prev(), amount)), + ), + Term::FunType(span, plicity, name, input, output) => Term::FunType( + *span, + *plicity, + *name, + scope.to_scope(input.shift_inner(scope, min, amount)), + scope.to_scope(output.shift_inner(scope, min.prev(), amount)), + ), + Term::FunLit(span, plicity, name, body) => Term::FunLit( + *span, + *plicity, + *name, + scope.to_scope(body.shift_inner(scope, min.prev(), amount)), + ), + Term::FunApp(span, plicity, fun, arg) => Term::FunApp( + *span, + *plicity, + scope.to_scope(fun.shift_inner(scope, min, amount)), + scope.to_scope(arg.shift_inner(scope, min, amount)), + ), + Term::RecordType(span, labels, types) => Term::RecordType( + *span, + labels, + scope.to_scope_from_iter(types.iter().map(|r#type| { + let ret = r#type.shift_inner(scope, min, amount); + min = min.prev(); + ret + })), + ), + Term::RecordLit(span, labels, exprs) => Term::RecordLit( + *span, + labels, + scope.to_scope_from_iter( + exprs + .iter() + .map(|expr| expr.shift_inner(scope, min, amount)), + ), + ), + Term::RecordProj(span, head, label) => Term::RecordProj( + *span, + scope.to_scope(head.shift_inner(scope, min, amount)), + *label, + ), + Term::ArrayLit(span, terms) => Term::ArrayLit( + *span, + scope.to_scope_from_iter( + terms + .iter() + .map(|term| term.shift_inner(scope, min, amount)), + ), + ), + Term::FormatRecord(span, labels, terms) => Term::FormatRecord( + *span, + labels, + scope.to_scope_from_iter(terms.iter().map(|term| { + let ret = term.shift_inner(scope, min, amount); + min = min.prev(); + ret + })), + ), + Term::FormatCond(span, name, format, pred) => Term::FormatCond( + *span, + *name, + scope.to_scope(format.shift_inner(scope, min, amount)), + scope.to_scope(pred.shift_inner(scope, min.prev(), amount)), + ), + Term::FormatOverlap(span, labels, terms) => Term::FormatOverlap( + *span, + labels, + scope.to_scope_from_iter(terms.iter().map(|term| { + let ret = term.shift_inner(scope, min, amount); + min = min.prev(); + ret + })), + ), + Term::ConstMatch(span, scrut, branches, default) => Term::ConstMatch( + *span, + scope.to_scope(scrut.shift_inner(scope, min, amount)), + scope.to_scope_from_iter( + branches + .iter() + .map(|(r#const, term)| (*r#const, term.shift_inner(scope, min, amount))), + ), + default.map(|(name, term)| { + ( + name, + scope.to_scope(term.shift_inner(scope, min.prev(), amount)) as &_, + ) + }), + ), + } + } + + /// Returns `true` if `self` can be evaluated in a single step. + /// Used as a heuristic to prevent increase in runtime when expanding + /// pattern matches + pub fn is_atomic(&self) -> bool { + match self { + Term::ItemVar(_, _) + | Term::LocalVar(_, _) + | Term::MetaVar(_, _) + | Term::InsertedMeta(_, _, _) + | Term::Universe(_) + | Term::Prim(_, _) + | Term::ConstLit(_, _) => true, + Term::RecordProj(_, head, _) => head.is_atomic(), + _ => false, + } + } } macro_rules! def_prims { @@ -599,6 +754,21 @@ pub enum Const { Ref(usize), } +impl Const { + /// Return the number of inhabitants of `self`. + /// `None` represents infinity + pub fn num_inhabitants(&self) -> Option { + match self { + Const::Bool(_) => Some(2), + Const::U8(_, _) | Const::S8(_) => Some(1 << 8), + Const::U16(_, _) | Const::S16(_) => Some(1 << 16), + Const::U32(_, _) | Const::S32(_) => Some(1 << 32), + Const::U64(_, _) | Const::S64(_) => Some(1 << 64), + Const::F32(_) | Const::F64(_) | Const::Pos(_) | Const::Ref(_) => None, + } + } +} + impl PartialEq for Const { fn eq(&self, other: &Self) -> bool { match (*self, *other) { diff --git a/fathom/src/core/semantics.rs b/fathom/src/core/semantics.rs index 8623e5aaf..4afd8f040 100644 --- a/fathom/src/core/semantics.rs +++ b/fathom/src/core/semantics.rs @@ -53,6 +53,8 @@ pub enum Value<'arena> { } impl<'arena> Value<'arena> { + pub const ERROR: Self = Self::Stuck(Head::Prim(Prim::ReportedError), Vec::new()); + pub fn prim(prim: Prim, params: impl IntoIterator>) -> Value<'arena> { let params = params .into_iter() @@ -76,6 +78,13 @@ impl<'arena> Value<'arena> { } } + pub fn match_record_type(&self) -> Option<&Telescope<'arena>> { + match self { + Value::RecordType(_, telescope) => Some(telescope), + _ => None, + } + } + pub fn is_error(&self) -> bool { matches!(self, Value::Stuck(Head::Prim(Prim::ReportedError), _)) } diff --git a/fathom/src/env.rs b/fathom/src/env.rs index 2f62a6032..ffae34d71 100644 --- a/fathom/src/env.rs +++ b/fathom/src/env.rs @@ -18,6 +18,7 @@ //! [`SharedEnv`] to increase the amount of sharing at the expense of locality. use std::fmt; +use std::ops::Add; /// Underlying variable representation. type RawVar = u16; @@ -56,6 +57,13 @@ impl Index { } } +impl Add for Index { + type Output = Self; + fn add(self, rhs: EnvLen) -> Self::Output { + Self(self.0 + rhs.0) // FIXME: check overflow? + } +} + impl fmt::Debug for Index { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { write!(f, "Index(")?; @@ -126,6 +134,13 @@ pub fn levels() -> impl Iterator { #[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord)] pub struct EnvLen(RawVar); +impl Add for EnvLen { + type Output = Self; + fn add(self, rhs: Index) -> Self::Output { + Self(self.0 + rhs.0) // FIXME: check overflow? + } +} + impl EnvLen { /// Construct a new, empty environment. pub fn new() -> EnvLen { @@ -152,6 +167,10 @@ impl EnvLen { Level(self.0) } + pub fn next(&self) -> EnvLen { + Self(self.0 + 1) // FIXME: check overflow? + } + /// Push an entry onto the environment. pub fn push(&mut self) { self.0 += 1; // FIXME: check overflow? diff --git a/fathom/src/surface.rs b/fathom/src/surface.rs index 7d9e2defd..9c3b54407 100644 --- a/fathom/src/surface.rs +++ b/fathom/src/surface.rs @@ -76,7 +76,7 @@ pub struct ItemDef<'arena, Range> { /// Surface patterns. #[derive(Debug, Clone)] -pub enum Pattern { +pub enum Pattern<'arena, Range> { /// Named patterns, eg. `x`, `true`, `false` Name(Range, StringId), /// Placeholder patterns, eg. `_` @@ -93,8 +93,10 @@ pub enum Pattern { NumberLiteral(Range, StringId), /// Boolean literal patterns BooleanLiteral(Range, bool), - // TODO: Record literal patterns - // RecordLiteral(Range, &'arena [((Range, StringId), Pattern<'arena, Range>)]), + /// Record literal patterns + RecordLiteral(Range, &'arena [PatternField<'arena, Range>]), + /// Tuple literal patterns + TupleLiteral(Range, &'arena [Pattern<'arena, Range>]), } #[derive(Debug, Clone, Copy)] @@ -167,14 +169,16 @@ impl fmt::Display for BinOp { } } -impl Pattern { +impl<'arena, Range: Clone> Pattern<'arena, Range> { pub fn range(&self) -> Range { match self { Pattern::Name(range, _) | Pattern::Placeholder(range) | Pattern::StringLiteral(range, _) | Pattern::NumberLiteral(range, _) - | Pattern::BooleanLiteral(range, _) => range.clone(), + | Pattern::BooleanLiteral(range, _) + | Pattern::RecordLiteral(range, _) + | Pattern::TupleLiteral(range, _) => range.clone(), } } } @@ -199,7 +203,7 @@ pub enum Term<'arena, Range> { /// Let expressions. Let( Range, - Pattern, + &'arena Pattern<'arena, Range>, Option<&'arena Term<'arena, Range>>, &'arena Term<'arena, Range>, &'arena Term<'arena, Range>, @@ -215,7 +219,7 @@ pub enum Term<'arena, Range> { Match( Range, &'arena Term<'arena, Range>, - &'arena [(Pattern, Term<'arena, Range>)], + &'arena [(Pattern<'arena, Range>, Term<'arena, Range>)], ), /// The type of types. Universe(Range), @@ -352,7 +356,7 @@ impl<'arena> Term<'arena, FileRange> { #[derive(Debug, Clone)] pub struct Param<'arena, Range> { pub plicity: Plicity, - pub pattern: Pattern, + pub pattern: Pattern<'arena, Range>, pub r#type: Option>, } @@ -403,6 +407,15 @@ pub struct ExprField<'arena, Range> { expr: Term<'arena, Range>, } +/// A field definition in a record pattern +#[derive(Debug, Clone)] +pub struct PatternField<'arena, Range> { + /// Label identifying the field + label: (Range, StringId), + /// The pattern that this field will match + pattern: Pattern<'arena, Range>, +} + /// Messages produced during parsing #[derive(Clone, Debug)] pub enum ParseMessage { @@ -529,14 +542,14 @@ mod tests { #[test] #[cfg(target_pointer_width = "64")] fn term_size() { - assert_eq!(std::mem::size_of::>(), 32); + assert_eq!(std::mem::size_of::>(), 40); assert_eq!(std::mem::size_of::>(), 48); } #[test] #[cfg(target_pointer_width = "64")] fn pattern_size() { - assert_eq!(std::mem::size_of::>(), 8); - assert_eq!(std::mem::size_of::>(), 16); + assert_eq!(std::mem::size_of::>(), 24); + assert_eq!(std::mem::size_of::>(), 32); } } diff --git a/fathom/src/surface/distillation.rs b/fathom/src/surface/distillation.rs index e85eafe4a..f50cf5b30 100644 --- a/fathom/src/surface/distillation.rs +++ b/fathom/src/surface/distillation.rs @@ -163,7 +163,7 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> { Term::NumberLiteral((), number) } - fn check_boolean_pattern(&mut self, boolean: bool) -> Pattern<()> { + fn check_boolean_pattern(&mut self, boolean: bool) -> Pattern<'arena, ()> { let name = match boolean { true => self.interner.borrow_mut().get_or_intern("true"), false => self.interner.borrow_mut().get_or_intern("false"), @@ -171,7 +171,7 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> { Pattern::Name((), name) } - fn check_number_pattern(&mut self, number: T) -> Pattern<()> { + fn check_number_pattern(&mut self, number: T) -> Pattern<'arena, ()> { let number = self.interner.borrow_mut().get_or_intern(number.to_string()); Pattern::NumberLiteral((), number) } @@ -180,14 +180,14 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> { &mut self, number: T, style: UIntStyle, - ) -> Pattern<()> { + ) -> Pattern<'arena, ()> { // TODO: Share with check_number_literal_styled let string = style.format(number); let number = self.interner.borrow_mut().get_or_intern(string); Pattern::NumberLiteral((), number) } - fn check_constant_pattern(&mut self, r#const: &Const) -> Pattern<()> { + fn check_constant_pattern(&mut self, r#const: &Const) -> Pattern<'arena, ()> { match r#const { Const::Bool(boolean) => self.check_boolean_pattern(*boolean), Const::U8(number, style) => self.check_number_pattern_styled(number, *style), @@ -286,7 +286,6 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> { let def_name = self.freshen_name(*def_name, body_expr); let def_name = self.push_local(def_name); - let def_pattern = name_to_pattern(def_name); let body_expr = self.check_prec(Prec::Let, body_expr); self.pop_local(); @@ -294,7 +293,7 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> { prec > Prec::Let, Term::Let( (), - def_pattern, + self.scope.to_scope(name_to_pattern(def_name)), Some(self.scope.to_scope(def_type)), self.scope.to_scope(def_expr), self.scope.to_scope(body_expr), @@ -380,11 +379,33 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> { core::Const::Ref(number) => self.check_number_literal(number), }, core::Term::ConstMatch(_span, head_expr, branches, default_branch) => { - if let Some((then_expr, else_expr)) = match_if_then_else(branches, *default_branch) + if let Some(((then_name, then_expr), (else_name, else_expr))) = + match_if_then_else(branches, *default_branch) { let cond_expr = self.check_prec(Prec::Fun, head_expr); - let then_expr = self.check_prec(Prec::Let, then_expr); - let else_expr = self.check_prec(Prec::Let, else_expr); + + let then_expr = match then_name { + None => self.check_prec(Prec::Let, then_expr), + Some(name) => { + let name = self.freshen_name(name, then_expr); + self.push_local(name); + let then_expr = self.check_prec(Prec::Let, then_expr); + self.pop_local(); + then_expr + } + }; + + let else_expr = match else_name { + None => self.check_prec(Prec::Let, else_expr), + Some(name) => { + let name = self.freshen_name(name, else_expr); + self.push_local(name); + let else_expr = self.check_prec(Prec::Let, else_expr); + self.pop_local(); + else_expr + } + }; + return self.paren( prec > Prec::Let, Term::If( @@ -450,11 +471,11 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> { match core_term { core::Term::ItemVar(_span, var) => match self.get_item_name(*var) { Some(name) => Term::Name((), name), - None => todo!("misbound variable"), // TODO: error? + None => panic!("misbound item variable: {var:?}"), }, core::Term::LocalVar(_span, var) => match self.get_local_name(*var) { Some(name) => Term::Name((), name), - None => todo!("misbound variable"), // TODO: error? + None => panic!("Unbound local variable: {var:?}"), }, core::Term::MetaVar(_span, var) => match self.get_hole_name(*var) { Some(name) => Term::Hole((), name), @@ -514,7 +535,7 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> { prec > Prec::Let, Term::Let( (), - name_to_pattern(def_name), + self.scope.to_scope(name_to_pattern(def_name)), Some(self.scope.to_scope(def_type)), self.scope.to_scope(def_expr), self.scope.to_scope(body_expr), @@ -769,15 +790,41 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> { } }, core::Term::ConstMatch(_span, head_expr, branches, default_expr) => { - if let Some((then_expr, else_expr)) = match_if_then_else(branches, *default_expr) { + if let Some(((then_name, then_expr), (else_name, else_expr))) = + match_if_then_else(branches, *default_expr) + { let cond_expr = self.check_prec(Prec::Fun, head_expr); - let then_expr = self.synth_prec(Prec::Let, then_expr); - let else_expr = self.synth_prec(Prec::Let, else_expr); - return Term::If( - (), - self.scope.to_scope(cond_expr), - self.scope.to_scope(then_expr), - self.scope.to_scope(else_expr), + + let then_expr = match then_name { + None => self.synth_prec(Prec::Let, then_expr), + Some(name) => { + let name = self.freshen_name(name, then_expr); + self.push_local(name); + let then_expr = self.synth_prec(Prec::Let, then_expr); + self.pop_local(); + then_expr + } + }; + + let else_expr = match else_name { + None => self.synth_prec(Prec::Let, else_expr), + Some(name) => { + let name = self.freshen_name(name, else_expr); + self.push_local(name); + let else_expr = self.synth_prec(Prec::Let, else_expr); + self.pop_local(); + else_expr + } + }; + + return self.paren( + prec > Prec::Let, + Term::If( + (), + self.scope.to_scope(cond_expr), + self.scope.to_scope(then_expr), + self.scope.to_scope(else_expr), + ), ); } @@ -883,22 +930,30 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> { } } -fn name_to_pattern(name: Option) -> Pattern<()> { +fn name_to_pattern<'arena>(name: Option) -> Pattern<'arena, ()> { match name { Some(name) => Pattern::Name((), name), None => Pattern::Placeholder(()), } } - +#[allow(clippy::type_complexity)] fn match_if_then_else<'arena>( branches: &'arena [(Const, core::Term<'arena>)], default_branch: Option<(Option, &'arena core::Term<'arena>)>, -) -> Option<(&'arena core::Term<'arena>, &'arena core::Term<'arena>)> { +) -> Option<( + (Option>, &'arena core::Term<'arena>), + (Option>, &'arena core::Term<'arena>), +)> { match (branches, default_branch) { - ([(Const::Bool(false), else_expr), (Const::Bool(true), then_expr)], None) - // TODO: Normalize boolean branches when elaborating patterns - | ([(Const::Bool(true), then_expr)], Some((_, else_expr))) - | ([(Const::Bool(false), else_expr)], Some((_, then_expr))) => Some((then_expr, else_expr)), + ([(Const::Bool(false), else_expr), (Const::Bool(true), then_expr)], None) => { + Some(((None, then_expr), (None, else_expr))) + } + ([(Const::Bool(true), then_expr)], Some((name, else_expr))) => { + Some(((None, then_expr), (Some(name), else_expr))) + } + ([(Const::Bool(false), else_expr)], Some((name, then_expr))) => { + Some(((Some(name), then_expr), (None, else_expr))) + } _ => None, } } diff --git a/fathom/src/surface/elaboration.rs b/fathom/src/surface/elaboration.rs index 712f419d1..63325f0cd 100644 --- a/fathom/src/surface/elaboration.rs +++ b/fathom/src/surface/elaboration.rs @@ -26,9 +26,9 @@ use std::sync::Arc; use scoped_arena::Scope; -use super::ExprField; +use self::patterns::{Body, CheckedPattern, PatMatrix, PatternMode}; use crate::alloc::SliceVec; -use crate::core::semantics::{self, ArcValue, Head, Telescope, Value}; +use crate::core::semantics::{self, ArcValue, Closure, Head, Telescope, Value}; use crate::core::{self, prim, Const, Plicity, Prim, UIntStyle}; use crate::env::{self, EnvLen, Level, SharedEnv, UniqueEnv}; use crate::files::FileId; @@ -39,6 +39,7 @@ use crate::surface::{ }; mod order; +mod patterns; mod reporting; mod unification; @@ -122,6 +123,10 @@ impl<'arena> LocalEnv<'arena> { self.names.len() } + fn next_var(&self) -> ArcValue<'arena> { + Spanned::empty(Arc::new(Value::local_var(self.exprs.len().next_level()))) + } + fn reserve(&mut self, additional: usize) { self.names.reserve(additional); self.types.reserve(additional); @@ -143,17 +148,15 @@ impl<'arena> LocalEnv<'arena> { } /// Push a local parameter onto the context. - fn push_param(&mut self, name: Option, r#type: ArcValue<'arena>) -> ArcValue<'arena> { + fn push_param(&mut self, name: Option, r#type: ArcValue<'arena>) { // An expression that refers to itself once it is pushed onto the local // expression environment. - let expr = Spanned::empty(Arc::new(Value::local_var(self.exprs.len().next_level()))); + let expr = self.next_var(); self.names.push(name); self.types.push(r#type); self.infos.push(core::LocalInfo::Param); - self.exprs.push(expr.clone()); - - expr + self.exprs.push(expr); } /// Pop a local binder off the context. @@ -500,6 +503,76 @@ impl<'interner, 'arena> Context<'interner, 'arena> { (labels.into(), filtered_fields) } + fn check_tuple_fields( + &mut self, + range: ByteRange, + fields: &[F], + get_range: fn(&F) -> ByteRange, + expected_labels: &[StringId], + ) -> Result<(), ()> { + if fields.len() == expected_labels.len() { + return Ok(()); + } + + let mut found_labels = Vec::with_capacity(fields.len()); + let mut fields_iter = fields.iter().enumerate().peekable(); + let mut expected_labels_iter = expected_labels.iter(); + + // use the label names from the expected labels + while let Some(((_, field), label)) = + Option::zip(fields_iter.peek(), expected_labels_iter.next()) + { + found_labels.push((self.file_range(get_range(field)), *label)); + fields_iter.next(); + } + + // use numeric labels for excess fields + for (index, field) in fields_iter { + found_labels.push(( + self.file_range(get_range(field)), + self.interner.borrow_mut().get_tuple_label(index), + )); + } + + self.push_message(Message::MismatchedFieldLabels { + range: self.file_range(range), + found_labels, + expected_labels: expected_labels.to_vec(), + }); + Err(()) + } + + fn check_record_fields( + &mut self, + range: ByteRange, + fields: &[F], + get_label: impl Fn(&F) -> (ByteRange, StringId), + labels: &'arena [StringId], + ) -> Result<(), ()> { + if fields.len() == labels.len() + && fields + .iter() + .zip(labels.iter()) + .all(|(field, type_label)| get_label(field).1 == *type_label) + { + return Ok(()); + } + + // TODO: improve handling of duplicate labels + self.push_message(Message::MismatchedFieldLabels { + range: self.file_range(range), + found_labels: fields + .iter() + .map(|field| { + let (range, label) = get_label(field); + (self.file_range(range), label) + }) + .collect(), + expected_labels: labels.to_vec(), + }); + Err(()) + } + /// Parse a source string into number, assuming an ASCII encoding. fn parse_ascii( &mut self, @@ -675,17 +748,17 @@ impl<'interner, 'arena> Context<'interner, 'arena> { for item in elab_order.iter().copied().map(|i| &surface_module.items[i]) { match item { Item::Def(item) => { - let (expr, r#type) = + let (expr, type_value) = self.synth_fun_lit(item.range, item.params, item.expr, item.r#type); let expr_value = self.eval_env().eval(&expr); - let type_value = self.eval_env().eval(&r#type); + let type_expr = self.quote_env().quote(self.scope, &type_value); self.item_env .push_definition(item.label.1, type_value, expr_value); items.push(core::Item::Def { label: item.label.1, - r#type: self.scope.to_scope(r#type), + r#type: self.scope.to_scope(type_expr), expr: self.scope.to_scope(expr), }); } @@ -757,247 +830,24 @@ impl<'interner, 'arena> Context<'interner, 'arena> { term } - /// Check that a pattern matches an expected type. - fn check_pattern( - &mut self, - pattern: &Pattern, - expected_type: &ArcValue<'arena>, - ) -> CheckedPattern { - let file_range = self.file_range(pattern.range()); - match pattern { - Pattern::Name(_, name) => CheckedPattern::Binder(file_range, *name), - Pattern::Placeholder(_) => CheckedPattern::Placeholder(file_range), - Pattern::StringLiteral(range, lit) => { - let constant = match expected_type.match_prim_spine() { - Some((Prim::U8Type, [])) => self.parse_ascii(*range, *lit, Const::U8), - Some((Prim::U16Type, [])) => self.parse_ascii(*range, *lit, Const::U16), - Some((Prim::U32Type, [])) => self.parse_ascii(*range, *lit, Const::U32), - Some((Prim::U64Type, [])) => self.parse_ascii(*range, *lit, Const::U64), - // Some((Prim::Array8Type, [len, _])) => todo!(), - // Some((Prim::Array16Type, [len, _])) => todo!(), - // Some((Prim::Array32Type, [len, _])) => todo!(), - // Some((Prim::Array64Type, [len, _])) => todo!(), - Some((Prim::ReportedError, _)) => None, - _ => { - let expected_type = self.pretty_print_value(expected_type); - self.push_message(Message::StringLiteralNotSupported { - range: file_range, - expected_type, - }); - None - } - }; - - match constant { - Some(constant) => CheckedPattern::ConstLit(file_range, constant), - None => CheckedPattern::ReportedError(file_range), - } - } - Pattern::NumberLiteral(range, lit) => { - let constant = match expected_type.match_prim_spine() { - Some((Prim::U8Type, [])) => self.parse_number_radix(*range, *lit, Const::U8), - Some((Prim::U16Type, [])) => self.parse_number_radix(*range, *lit, Const::U16), - Some((Prim::U32Type, [])) => self.parse_number_radix(*range, *lit, Const::U32), - Some((Prim::U64Type, [])) => self.parse_number_radix(*range, *lit, Const::U64), - Some((Prim::S8Type, [])) => self.parse_number(*range, *lit, Const::S8), - Some((Prim::S16Type, [])) => self.parse_number(*range, *lit, Const::S16), - Some((Prim::S32Type, [])) => self.parse_number(*range, *lit, Const::S32), - Some((Prim::S64Type, [])) => self.parse_number(*range, *lit, Const::S64), - Some((Prim::F32Type, [])) => self.parse_number(*range, *lit, Const::F32), - Some((Prim::F64Type, [])) => self.parse_number(*range, *lit, Const::F64), - Some((Prim::ReportedError, _)) => None, - _ => { - let expected_type = self.pretty_print_value(expected_type); - self.push_message(Message::NumericLiteralNotSupported { - range: file_range, - expected_type, - }); - None - } - }; - - match constant { - Some(constant) => CheckedPattern::ConstLit(file_range, constant), - None => CheckedPattern::ReportedError(file_range), - } - } - Pattern::BooleanLiteral(_, boolean) => { - let constant = match expected_type.match_prim_spine() { - Some((Prim::BoolType, [])) => match *boolean { - true => Some(Const::Bool(true)), - false => Some(Const::Bool(false)), - }, - _ => { - self.push_message(Message::BooleanLiteralNotSupported { - range: file_range, - }); - None - } - }; - - match constant { - Some(constant) => CheckedPattern::ConstLit(file_range, constant), - None => CheckedPattern::ReportedError(file_range), - } - } - } - } - - /// Synthesize the type of a pattern. - fn synth_pattern( - &mut self, - pattern: &Pattern, - ) -> (CheckedPattern, ArcValue<'arena>) { - let file_range = self.file_range(pattern.range()); - match pattern { - Pattern::Name(_, name) => { - let source = MetaSource::NamedPatternType(file_range, *name); - let r#type = self.push_unsolved_type(source); - (CheckedPattern::Binder(file_range, *name), r#type) - } - Pattern::Placeholder(_) => { - let source = MetaSource::PlaceholderPatternType(file_range); - let r#type = self.push_unsolved_type(source); - (CheckedPattern::Placeholder(file_range), r#type) - } - Pattern::StringLiteral(_, _) => { - self.push_message(Message::AmbiguousStringLiteral { range: file_range }); - let source = MetaSource::ReportedErrorType(file_range); - let r#type = self.push_unsolved_type(source); - (CheckedPattern::ReportedError(file_range), r#type) - } - Pattern::NumberLiteral(_, _) => { - self.push_message(Message::AmbiguousNumericLiteral { range: file_range }); - let source = MetaSource::ReportedErrorType(file_range); - let r#type = self.push_unsolved_type(source); - (CheckedPattern::ReportedError(file_range), r#type) - } - Pattern::BooleanLiteral(_, val) => { - let r#const = Const::Bool(*val); - let r#type = self.bool_type.clone(); - (CheckedPattern::ConstLit(file_range, r#const), r#type) - } - } - } - - /// Check that the type of an annotated pattern matches an expected type. - fn check_ann_pattern( - &mut self, - pattern: &Pattern, - r#type: Option<&Term<'_, ByteRange>>, - expected_type: &ArcValue<'arena>, - ) -> CheckedPattern { - match r#type { - None => self.check_pattern(pattern, expected_type), - Some(r#type) => { - let file_range = self.file_range(r#type.range()); - let r#type = self.check(r#type, &self.universe.clone()); - let r#type = self.eval_env().eval(&r#type); - - match self.unification_context().unify(&r#type, expected_type) { - Ok(()) => self.check_pattern(pattern, &r#type), - Err(error) => { - let lhs = self.pretty_print_value(&r#type); - let rhs = self.pretty_print_value(expected_type); - self.push_message(Message::FailedToUnify { - range: file_range, - found: lhs, - expected: rhs, - error, - }); - CheckedPattern::ReportedError(file_range) - } - } - } - } - } - - /// Synthesize the type of an annotated pattern. - fn synth_ann_pattern( - &mut self, - pattern: &Pattern, - r#type: Option<&Term<'_, ByteRange>>, - ) -> (CheckedPattern, core::Term<'arena>, ArcValue<'arena>) { - match r#type { - None => { - let (pattern, type_value) = self.synth_pattern(pattern); - let r#type = self.quote_env().quote(self.scope, &type_value); - (pattern, r#type, type_value) - } - Some(r#type) => { - let r#type = self.check(r#type, &self.universe.clone()); - let type_value = self.eval_env().eval(&r#type); - (self.check_pattern(pattern, &type_value), r#type, type_value) - } - } - } - /// Push a local definition onto the context. - /// The supplied `pattern` is expected to be irrefutable. fn push_local_def( &mut self, - pattern: CheckedPattern, - expr: ArcValue<'arena>, - r#type: ArcValue<'arena>, - ) -> Option { - let name = match pattern { - CheckedPattern::Binder(_, name) => Some(name), - CheckedPattern::Placeholder(_) => None, - // FIXME: generate failing parameter expressions? - CheckedPattern::ConstLit(range, _) => { - self.push_message(Message::RefutablePattern { - pattern_range: range, - }); - None - } - CheckedPattern::ReportedError(_) => None, - }; - - self.local_env.push_def(name, expr, r#type); - - name + pattern: &CheckedPattern<'arena>, + scrut: Scrutinee<'arena>, + value: ArcValue<'arena>, + ) -> Vec<(Option, Scrutinee<'arena>)> { + self.push_pattern(pattern, scrut, value, PatternMode::Let, true) } /// Push a local parameter onto the context. - /// The supplied `pattern` is expected to be irrefutable. fn push_local_param( &mut self, - pattern: CheckedPattern, - r#type: ArcValue<'arena>, - ) -> (Option, ArcValue<'arena>) { - let name = match pattern { - CheckedPattern::Binder(_, name) => Some(name), - CheckedPattern::Placeholder(_) => None, - // FIXME: generate failing parameter expressions? - CheckedPattern::ConstLit(range, _) => { - self.push_message(Message::RefutablePattern { - pattern_range: range, - }); - None - } - CheckedPattern::ReportedError(_) => None, - }; - - let expr = self.local_env.push_param(name, r#type); - - (name, expr) - } - - /// Elaborate a list of parameters, pushing them onto the context. - fn synth_and_push_params( - &mut self, - params: &[Param], - ) -> Vec<(ByteRange, Plicity, Option, core::Term<'arena>)> { - self.local_env.reserve(params.len()); - - Vec::from_iter(params.iter().map(|param| { - let range = param.pattern.range(); - let (pattern, r#type, type_value) = - self.synth_ann_pattern(¶m.pattern, param.r#type.as_ref()); - let (name, _) = self.push_local_param(pattern, type_value); - - (range, param.plicity, name, r#type) - })) + pattern: &CheckedPattern<'arena>, + scrut: Scrutinee<'arena>, + ) -> Vec<(Option, Scrutinee<'arena>)> { + let value = self.local_env.next_var(); + self.push_pattern(pattern, scrut, value, PatternMode::Fun, true) } /// Check that a surface term conforms to the given type. @@ -1013,23 +863,26 @@ impl<'interner, 'arena> Context<'interner, 'arena> { match (surface_term, expected_type.as_ref()) { (Term::Paren(_, term), _) => self.check(term, &expected_type), - (Term::Let(_, def_pattern, def_type, def_expr, body_expr), _) => { - let (def_pattern, def_type, def_type_value) = + (Term::Let(range, def_pattern, def_type, def_expr, body_expr), _) => { + let (def_pattern, _, def_type_value) = self.synth_ann_pattern(def_pattern, *def_type); - let def_expr = self.check(def_expr, &def_type_value); - let def_expr_value = self.eval_env().eval(&def_expr); + let scrut = self.check_scrutinee(def_expr, def_type_value); + let value = self.eval_env().eval(scrut.expr); + let (scrut, extra_def) = self.freshen_scrutinee(scrut, &value, [&def_pattern]); - let def_name = self.push_local_def(def_pattern, def_expr_value, def_type_value); // TODO: split on constants + let initial_len = self.local_env.len(); + let defs = self.push_local_def(&def_pattern, scrut.clone(), value); let body_expr = self.check(body_expr, &expected_type); - self.local_env.pop(); - - core::Term::Let( - file_range.into(), - def_name, - self.scope.to_scope(def_type), - self.scope.to_scope(def_expr), - self.scope.to_scope(body_expr), - ) + self.local_env.truncate(initial_len); + + let matrix = PatMatrix::singleton(scrut, def_pattern); + let body = self.elab_match( + matrix, + &[Body::new(body_expr, defs)], + *range, + def_expr.range(), + ); + self.insert_extra_let(*range, body, extra_def) } (Term::If(_, cond_expr, then_expr, else_expr), _) => { let cond_expr = self.check(cond_expr, &self.bool_type.clone()); @@ -1050,8 +903,8 @@ impl<'interner, 'arena> Context<'interner, 'arena> { (Term::Match(range, scrutinee_expr, equations), _) => { self.check_match(*range, scrutinee_expr, equations, &expected_type) } - (Term::FunLiteral(range, patterns, body_expr), _) => { - self.check_fun_lit(*range, patterns, body_expr, &expected_type) + (Term::FunLiteral(range, params, body_expr), _) => { + self.check_fun_lit(*range, params, body_expr, &expected_type) } // Attempt to specialize terms with freshly inserted implicit // arguments if an explicit function was expected. @@ -1060,19 +913,11 @@ impl<'interner, 'arena> Context<'interner, 'arena> { let (synth_term, synth_type) = self.synth_and_insert_implicit_apps(surface_term); self.coerce(surface_range, synth_term, &synth_type, &expected_type) } - (Term::RecordLiteral(_, expr_fields), Value::RecordType(labels, types)) => { - // TODO: improve handling of duplicate labels - if expr_fields.len() != labels.len() - || Iterator::zip(expr_fields.iter(), labels.iter()) - .any(|(expr_field, type_label)| expr_field.label.1 != *type_label) + (Term::RecordLiteral(range, expr_fields), Value::RecordType(labels, types)) => { + if self + .check_record_fields(*range, expr_fields, |field| field.label, labels) + .is_err() { - self.push_message(Message::MismatchedFieldLabels { - range: file_range, - expr_labels: (expr_fields.iter()) - .map(|ExprField { label, .. }| (self.file_range(label.0), label.1)) - .collect(), - type_labels: labels.to_vec(), - }); return core::Term::Prim(file_range.into(), Prim::ReportedError); } @@ -1135,34 +980,12 @@ impl<'interner, 'arena> Context<'interner, 'arena> { core::Term::FormatRecord(file_range.into(), labels, formats) } - (Term::Tuple(_, elem_exprs), Value::RecordType(labels, types)) => { - if elem_exprs.len() != labels.len() { - let mut expr_labels = Vec::with_capacity(elem_exprs.len()); - let mut elem_exprs = elem_exprs.iter().enumerate().peekable(); - let mut label_iter = labels.iter(); - - // use the label names from the expected type - while let Some(((_, elem_expr), label)) = - Option::zip(elem_exprs.peek(), label_iter.next()) - { - expr_labels.push((self.file_range(elem_expr.range()), *label)); - elem_exprs.next(); - } - - // use numeric labels for excess elems - for (index, elem_expr) in elem_exprs { - expr_labels.push(( - self.file_range(elem_expr.range()), - self.interner.borrow_mut().get_tuple_label(index), - )); - } - - self.push_message(Message::MismatchedFieldLabels { - range: file_range, - expr_labels, - type_labels: labels.to_vec(), - }); - return core::Term::Prim(file_range.into(), Prim::ReportedError); + (Term::Tuple(range, elem_exprs), Value::RecordType(labels, types)) => { + if self + .check_tuple_fields(*range, elem_exprs, |expr| expr.range(), labels) + .is_err() + { + return core::Term::error(self.file_range(*range)); } let mut types = types.clone(); @@ -1420,24 +1243,26 @@ impl<'interner, 'arena> Context<'interner, 'arena> { (ann_expr, type_value) } - Term::Let(_, def_pattern, def_type, def_expr, body_expr) => { - let (def_pattern, def_type, def_type_value) = + Term::Let(range, def_pattern, def_type, def_expr, body_expr) => { + let (def_pattern, _, def_type_value) = self.synth_ann_pattern(def_pattern, *def_type); - let def_expr = self.check(def_expr, &def_type_value); - let def_expr_value = self.eval_env().eval(&def_expr); + let scrut = self.check_scrutinee(def_expr, def_type_value); + let value = self.eval_env().eval(scrut.expr); + let (scrut, extra_def) = self.freshen_scrutinee(scrut, &value, [&def_pattern]); - let def_name = self.push_local_def(def_pattern, def_expr_value, def_type_value); + let initial_len = self.local_env.len(); + let defs = self.push_local_def(&def_pattern, scrut.clone(), value); let (body_expr, body_type) = self.synth(body_expr); - self.local_env.pop(); - - let let_expr = core::Term::Let( - file_range.into(), - def_name, - self.scope.to_scope(def_type), - self.scope.to_scope(def_expr), - self.scope.to_scope(body_expr), + self.local_env.truncate(initial_len); + + let matrix = patterns::PatMatrix::singleton(scrut, def_pattern); + let body = self.elab_match( + matrix, + &[Body::new(body_expr, defs)], + *range, + def_expr.range(), ); - + let let_expr = self.insert_extra_let(*range, body, extra_def); (let_expr, body_type) } Term::If(_, cond_expr, then_expr, else_expr) => { @@ -1487,38 +1312,13 @@ impl<'interner, 'arena> Context<'interner, 'arena> { self.scope.to_scope(body_type), ); - (fun_type, self.universe.clone()) + (fun_type, universe) } - Term::FunType(range, params, body_type) => { - let initial_local_len = self.local_env.len(); - - let params = self.synth_and_push_params(params); - let mut fun_type = self.check(body_type, &self.universe.clone()); - self.local_env.truncate(initial_local_len); - - // Construct the function type from the parameters in reverse - for (i, (param_range, plicity, name, r#type)) in - params.into_iter().enumerate().rev() - { - let range = match i { - 0 => *range, // Use the range of the full function type - _ => ByteRange::merge(param_range, body_type.range()), - }; - - fun_type = core::Term::FunType( - self.file_range(range).into(), - plicity, - name, - self.scope.to_scope(r#type), - self.scope.to_scope(fun_type), - ); - } - - (fun_type, self.universe.clone()) + Term::FunType(range, patterns, body_type) => { + self.synth_fun_type(*range, patterns, body_type) } Term::FunLiteral(range, params, body_expr) => { - let (expr, r#type) = self.synth_fun_lit(*range, params, body_expr, None); - (expr, self.eval_env().eval(&r#type)) + self.synth_fun_lit(*range, params, body_expr, None) } Term::App(range, head_expr, args) => { let mut head_range = head_expr.range(); @@ -1771,6 +1571,7 @@ impl<'interner, 'arena> Context<'interner, 'arena> { } } + // TODO: use iteration instead of recursion fn check_fun_lit( &mut self, range: ByteRange, @@ -1780,38 +1581,63 @@ impl<'interner, 'arena> Context<'interner, 'arena> { ) -> core::Term<'arena> { let file_range = self.file_range(range); match params.split_first() { + None => self.check(body_expr, expected_type), Some((param, next_params)) => { - let body_type = self.elim_env().force(expected_type); - match body_type.as_ref() { - Value::FunType(param_plicity, _, param_type, next_body_type) - if param.plicity == *param_plicity => + let expected_type = self.elim_env().force(expected_type); + match expected_type.as_ref() { + Value::FunType(expected_plicity, _, expected_type, next_body_type) + if param.plicity == *expected_plicity => { - let range = ByteRange::merge(param.pattern.range(), body_expr.range()); - let pattern = self.check_ann_pattern( - ¶m.pattern, - param.r#type.as_ref(), - param_type, - ); - let (name, arg_expr) = self.push_local_param(pattern, param_type.clone()); - - let body_type = self.elim_env().apply_closure(next_body_type, arg_expr); - let body_expr = - self.check_fun_lit(range, next_params, body_expr, &body_type); - self.local_env.pop(); + let initial_len = self.local_env.len(); + let (pattern, scrut) = self.check_param(param, expected_type); + let name = pattern.name(); + let scrut_type = scrut.r#type.clone(); + let scrut_range = scrut.range; + + let (defs, body_term) = { + let arg_expr = self.local_env.next_var(); + let expected_type = + self.elim_env().apply_closure(next_body_type, arg_expr); + + let defs = self.push_local_param(&pattern, scrut.clone()); + let body_term = + self.check_fun_lit(range, next_params, body_expr, &expected_type); + self.local_env.truncate(initial_len); + (defs, body_term) + }; + + let matrix = PatMatrix::singleton(scrut, pattern); + + let body_term = { + self.local_env.push_param(name, scrut_type); + let body_term = self.elab_match( + matrix, + &[Body::new(body_term, defs)], + range, + scrut_range, + ); + self.local_env.truncate(initial_len); + body_term + }; core::Term::FunLit( - self.file_range(range).into(), + file_range.into(), param.plicity, name, - self.scope.to_scope(body_expr), + self.scope.to_scope(body_term), ) } - // If an implicit function is expected, try to generalize the + + // If an implicit function is expected, try to generalise the // function literal by wrapping it in an implicit function - Value::FunType(Plicity::Implicit, param_name, param_type, next_body_type) - if param.plicity == Plicity::Explicit => - { - let arg_expr = self.local_env.push_param(*param_name, param_type.clone()); + Value::FunType( + Plicity::Implicit, + param_name, + expected_type, + next_body_type, + ) if param.plicity == Plicity::Explicit => { + let arg_expr = self.local_env.next_var(); + (self.local_env).push_param(*param_name, expected_type.clone()); let body_type = self.elim_env().apply_closure(next_body_type, arg_expr); let body_expr = self.check_fun_lit(range, params, body_expr, &body_type); self.local_env.pop(); @@ -1822,17 +1648,15 @@ impl<'interner, 'arena> Context<'interner, 'arena> { self.scope.to_scope(body_expr), ) } + // Attempt to elaborate the the body of the function in synthesis // mode if we are checking against a metavariable. Value::Stuck(Head::MetaVar(_), _) => { let range = ByteRange::merge(param.pattern.range(), body_expr.range()); let (expr, r#type) = self.synth_fun_lit(range, params, body_expr, None); - let type_value = self.eval_env().eval(&r#type); - self.coerce(range, expr, &type_value, expected_type) - } - Value::Stuck(Head::Prim(Prim::ReportedError), _) => { - core::Term::Prim(file_range.into(), Prim::ReportedError) + self.coerce(range, expr, &r#type, &expected_type) } + r#type if r#type.is_error() => core::Term::error(file_range), _ => { self.push_message(Message::UnexpectedParameter { param_range: self.file_range(param.pattern.range()), @@ -1840,63 +1664,131 @@ impl<'interner, 'arena> Context<'interner, 'arena> { // TODO: For improved error recovery, bind the rest of // the parameters, and check the body of the function // literal using the expected body type. - core::Term::Prim(file_range.into(), Prim::ReportedError) + core::Term::error(file_range) } } } - None => self.check(body_expr, expected_type), } } + // TODO: use iteration instead of recursion fn synth_fun_lit( &mut self, range: ByteRange, params: &[Param<'_, ByteRange>], body_expr: &Term<'_, ByteRange>, body_type: Option<&Term<'_, ByteRange>>, - ) -> (core::Term<'arena>, core::Term<'arena>) { - self.local_env.reserve(params.len()); - let initial_local_len = self.local_env.len(); + ) -> (core::Term<'arena>, ArcValue<'arena>) { + match params.split_first() { + None => match body_type { + None => self.synth(body_expr), + Some(body_type) => { + let body_type = self.check(body_type, &self.universe.clone()); + let body_type = self.eval_env().eval(&body_type); + let term = self.check(body_expr, &body_type); + (term, body_type) + } + }, + Some((param, next_params)) => { + let initial_len = self.local_env.len(); + let (pattern, scrut) = self.synth_param(param); + let name = pattern.name(); + let scrut_type = scrut.r#type.clone(); + let scrut_range = scrut.range; + + let (defs, body_term, body_type) = { + let defs = self.push_local_param(&pattern, scrut.clone()); + let (body_term, body_type_value) = + self.synth_fun_lit(range, next_params, body_expr, body_type); + let body_type = self.quote_env().quote(self.scope, &body_type_value); + self.local_env.truncate(initial_len); + (defs, body_term, body_type) + }; - let params = self.synth_and_push_params(params); + let matrix = PatMatrix::singleton(scrut, pattern); - let (mut fun_lit, mut fun_type) = match body_type { - Some(body_type) => { - let body_type = self.check(body_type, &self.universe.clone()); - let body_type_value = self.eval_env().eval(&body_type); - (self.check(body_expr, &body_type_value), body_type) + let term = { + self.local_env.push_param(name, scrut_type.clone()); + let body_term = self.elab_match( + matrix.clone(), + &[Body::new(body_term, defs.clone())], + range, + scrut_range, + ); + self.local_env.truncate(initial_len); + core::Term::FunLit( + self.file_range(range).into(), + param.plicity, + name, + self.scope.to_scope(body_term), + ) + }; + + let r#type = { + self.local_env.push_param(name, scrut_type.clone()); + let body_type = self.elab_match( + matrix, + &[Body::new(body_type, defs.clone())], + range, + scrut_range, + ); + self.local_env.truncate(initial_len); + Spanned::empty(Arc::new(Value::FunType( + param.plicity, + name, + scrut_type, + Closure::new(self.local_env.exprs.clone(), self.scope.to_scope(body_type)), + ))) + }; + + (term, r#type) } + } + } + + // TODO: use iteration instead of recursion + fn synth_fun_type( + &mut self, + range: ByteRange, + params: &[Param<'_, ByteRange>], + body_type: &Term<'_, ByteRange>, + ) -> (core::Term<'arena>, ArcValue<'arena>) { + let universe = self.universe.clone(); + match params.split_first() { None => { - let (body_expr, body_type) = self.synth(body_expr); - (body_expr, self.quote_env().quote(self.scope, &body_type)) + let term = self.check(body_type, &universe); + (term, universe) } - }; + Some((param, next_params)) => { + let (pattern, scrut) = self.synth_param(param); + let name = pattern.name(); + let input_type_expr = self.quote_env().quote(self.scope, &scrut.r#type); + + let initial_len = self.local_env.len(); + let defs = self.push_local_param(&pattern, scrut.clone()); + let (body_expr, _) = self.synth_fun_type(range, next_params, body_type); + self.local_env.truncate(initial_len); + + let body_expr = { + self.local_env.push_param(name, scrut.r#type.clone()); + let matrix = PatMatrix::singleton(scrut, pattern); + let body_expr = + self.elab_match(matrix, &[Body::new(body_expr, defs)], range, range); + self.local_env.truncate(initial_len); + body_expr + }; - self.local_env.truncate(initial_local_len); + let term = core::Term::FunType( + self.file_range(range).into(), + param.plicity, + name, + self.scope.to_scope(input_type_expr), + self.scope.to_scope(body_expr), + ); - // Construct the function literal and type from the parameters in reverse - for (i, (param_range, plicity, name, r#type)) in params.into_iter().enumerate().rev() { - let range = match i { - 0 => range, // Use the range of the full function literal - _ => ByteRange::merge(param_range, body_expr.range()), - }; - - fun_lit = core::Term::FunLit( - self.file_range(range).into(), - plicity, - name, - self.scope.to_scope(fun_lit), - ); - fun_type = core::Term::FunType( - Span::Empty, - plicity, - name, - self.scope.to_scope(r#type), - self.scope.to_scope(fun_type), - ); + (term, universe) + } } - - (fun_lit, fun_type) } fn synth_bin_op( @@ -2167,13 +2059,38 @@ impl<'interner, 'arena> Context<'interner, 'arena> { equations: &[(Pattern, Term<'_, ByteRange>)], expected_type: &ArcValue<'arena>, ) -> core::Term<'arena> { - let match_info = MatchInfo { - range, - scrutinee: self.synth_scrutinee(scrutinee_expr), - expected_type: self.elim_env().force(expected_type), - }; + let expected_type = self.elim_env().force(expected_type); + let scrut = self.synth_scrutinee(scrutinee_expr); + let value = self.eval_env().eval(scrut.expr); + + let patterns: Vec<_> = equations + .iter() + .map(|(pat, _)| self.check_pattern(pat, &scrut.r#type)) + .collect(); + let (scrut, extra_def) = self.freshen_scrutinee(scrut, &value, &patterns); + + let mut rows = Vec::with_capacity(equations.len()); + let mut bodies = Vec::with_capacity(equations.len()); + + for (pattern, (_, expr)) in patterns.into_iter().zip(equations) { + let initial_len = self.local_env.len(); + let defs = self.push_pattern( + &pattern, + scrut.clone(), + value.clone(), + PatternMode::Match, + true, + ); + let expr = self.check(expr, &expected_type); + self.local_env.truncate(initial_len); + + rows.push(patterns::PatRow::singleton((pattern, scrut.clone()))); + bodies.push(Body::new(expr, defs)); + } - self.elab_match(&match_info, true, equations.iter()) + let matrix = patterns::PatMatrix::new(rows); + let body = self.elab_match(matrix, &bodies, range, scrut.range); + self.insert_extra_let(range, body, extra_def) } fn synth_scrutinee(&mut self, scrutinee_expr: &Term<'_, ByteRange>) -> Scrutinee<'arena> { @@ -2186,220 +2103,114 @@ impl<'interner, 'arena> Context<'interner, 'arena> { } } - /// Elaborate a pattern match into a case tree in the core language. - /// - /// The implementation is based on the algorithm described in Section 5 of - /// [“The Implementation of Functional Programming Languages”][impl-fpl]. - /// - /// [impl-fpl]: https://www.microsoft.com/en-us/research/publication/the-implementation-of-functional-programming-languages/ - fn elab_match<'a>( + fn check_scrutinee( &mut self, - match_info: &MatchInfo<'arena>, - is_reachable: bool, - mut equations: impl Iterator, Term<'a, ByteRange>)>, - ) -> core::Term<'arena> { - match equations.next() { - Some((pattern, body_expr)) => { - match self.check_pattern(pattern, &match_info.scrutinee.r#type) { - // Named patterns are elaborated to let bindings, where the - // scrutinee is bound as a definition in the body expression. - // Subsequent patterns are unreachable. - CheckedPattern::Binder(range, name) => { - self.check_match_reachable(is_reachable, range); - - let def_name = Some(name); - let def_expr = self.eval_env().eval(match_info.scrutinee.expr); - let def_type_value = match_info.scrutinee.r#type.clone(); - let def_type = self.quote_env().quote(self.scope, &def_type_value); - - self.local_env.push_def(def_name, def_expr, def_type_value); - let body_expr = self.check(body_expr, &match_info.expected_type); - self.local_env.pop(); - - self.elab_match_unreachable(match_info, equations); - - core::Term::Let( - Span::merge(&range.into(), &body_expr.span()), - def_name, - self.scope.to_scope(def_type), - match_info.scrutinee.expr, - self.scope.to_scope(body_expr), - ) - } - // Placeholder patterns just elaborate to the body - // expression. Subsequent patterns are unreachable. - CheckedPattern::Placeholder(range) => { - self.check_match_reachable(is_reachable, range); - - let body_expr = self.check(body_expr, &match_info.expected_type); - self.elab_match_unreachable(match_info, equations); - - body_expr - } - // If we see a constant pattern we should expect a run of - // constants, elaborating to a constant elimination. - CheckedPattern::ConstLit(range, r#const) => { - self.check_match_reachable(is_reachable, range); - - let body_expr = self.check(body_expr, &match_info.expected_type); - let const_equation = (range, r#const, body_expr); - - self.elab_match_const(match_info, is_reachable, const_equation, equations) - } - // If we hit an error, propagate it, while still checking - // the body expression and the subsequent branches. - CheckedPattern::ReportedError(range) => { - self.check(body_expr, &match_info.expected_type); - self.elab_match_unreachable(match_info, equations); - core::Term::Prim(range.into(), Prim::ReportedError) - } - } - } - None => self.elab_match_absurd(is_reachable, match_info), + scrutinee_expr: &Term<'_, ByteRange>, + expected_type: ArcValue<'arena>, + ) -> Scrutinee<'arena> { + let expr = self.check(scrutinee_expr, &expected_type); + Scrutinee { + range: scrutinee_expr.range(), + expr: self.scope.to_scope(expr), + r#type: expected_type, } } - /// Ensure that this part of a match expression is reachable, reporting - /// a message if it is not. - fn check_match_reachable(&mut self, is_reachable: bool, range: FileRange) { - if !is_reachable { - self.push_message(Message::UnreachablePattern { range }); + // Bind `scrut` to a fresh variable if it is unsafe to evaluate multiple times, + // and may be evaluated multiple times by any of `patterns` + // Don't forget to wrap the body in a `Term::Let` with `insert_extra_let`! + fn freshen_scrutinee<'a>( + &mut self, + mut scrut: Scrutinee<'arena>, + value: &ArcValue<'arena>, + patterns: impl IntoIterator>, + ) -> ( + Scrutinee<'arena>, + Option<(Option, core::Term<'arena>, core::Term<'arena>)>, + ) { + if scrut.expr.is_atomic() || patterns.into_iter().all(|pat| pat.is_atomic()) { + return (scrut, None); } + + let def_name = None; // TODO: generate a fresh name + let def_type = self.quote_env().quote(self.scope, &scrut.r#type); + let def_expr = scrut.expr.clone(); + + let var = core::Term::LocalVar(def_expr.span(), env::Index::last()); + scrut.expr = self.scope.to_scope(var); + (self.local_env).push_def(def_name, value.clone(), scrut.r#type.clone()); + let extra_def = Some((def_name, def_type, def_expr)); + (scrut, extra_def) } - /// Elaborate the equations, expecting a series of constant patterns - fn elab_match_const<'a>( + /// Wrap `body` in a `Term::Let` binding `extra_def` if it is `Some`. + /// Used in conjunction with `freshen_scrutinee` + fn insert_extra_let( &mut self, - match_info: &MatchInfo<'arena>, - is_reachable: bool, - (const_range, r#const, body_expr): (FileRange, Const, core::Term<'arena>), - mut equations: impl Iterator, Term<'a, ByteRange>)>, + range: ByteRange, + body: core::Term<'arena>, + extra_def: Option<(Option, core::Term<'arena>, core::Term<'arena>)>, ) -> core::Term<'arena> { - // The full range of this series of patterns - let mut full_span = Span::merge(&const_range.into(), &body_expr.span()); - // Temporary vector for accumulating branches - let mut branches = vec![(r#const, body_expr)]; - - // Elaborate a run of constant patterns. - 'patterns: while let Some((pattern, body_expr)) = equations.next() { - // Update the range up to the end of the next body expression - full_span = Span::merge(&full_span, &self.file_range(body_expr.range()).into()); - - // Default expression, defined if we arrive at a default case - let default_branch; - - match self.check_pattern(pattern, &match_info.scrutinee.r#type) { - // Accumulate constant pattern. Search for it in the accumulated - // branches and insert it in order. - CheckedPattern::ConstLit(range, r#const) => { - let body_expr = self.check(body_expr, &match_info.expected_type); - - // Find insertion index of the branch - let insertion_index = branches.binary_search_by(|(probe_const, _)| { - Const::partial_cmp(probe_const, &r#const) - .expect("attempt to compare non-ordered value") - }); - - match insertion_index { - Ok(_) => self.push_message(Message::UnreachablePattern { range }), - Err(index) => { - // This has not yet been covered, so it should be reachable. - self.check_match_reachable(is_reachable, range); - branches.insert(index, (r#const, body_expr)); - } - } - - // No default case yet, continue looking for constant patterns. - continue 'patterns; - } - - // Time to elaborate the default pattern. The default case of - // `core::Term::ConstMatch` binds a variable, so both - // the named and placeholder patterns should bind this. - CheckedPattern::Binder(range, name) => { - self.check_match_reachable(is_reachable, range); - - // TODO: If we know this is an exhaustive match, bind the - // scrutinee to a let binding with the elaborated body, and - // add it to the branches. This will simplify the - // distillation of if expressions. - (self.local_env).push_param(Some(name), match_info.scrutinee.r#type.clone()); - let default_expr = self.check(body_expr, &match_info.expected_type); - default_branch = (Some(name), self.scope.to_scope(default_expr) as &_); - self.local_env.pop(); - } - CheckedPattern::Placeholder(range) => { - self.check_match_reachable(is_reachable, range); - - (self.local_env).push_param(None, match_info.scrutinee.r#type.clone()); - let default_expr = self.check(body_expr, &match_info.expected_type); - default_branch = (None, self.scope.to_scope(default_expr) as &_); - self.local_env.pop(); - } - CheckedPattern::ReportedError(range) => { - (self.local_env).push_param(None, match_info.scrutinee.r#type.clone()); - let default_expr = core::Term::Prim(range.into(), Prim::ReportedError); - default_branch = (None, self.scope.to_scope(default_expr) as &_); - self.local_env.pop(); - } - }; - - // A default pattern was found, check any unreachable patterns. - self.elab_match_unreachable(match_info, equations); - - return core::Term::ConstMatch( - full_span, - match_info.scrutinee.expr, - self.scope.to_scope_from_iter(branches.into_iter()), - Some(default_branch), - ); + match extra_def { + None => body, + Some((def_name, def_type, def_expr)) => { + self.local_env.pop(); + core::Term::Let( + self.file_range(range).into(), + def_name, + self.scope.to_scope(def_type), + self.scope.to_scope(def_expr), + self.scope.to_scope(body), + ) + } } + } - // Finished all the constant patterns without encountering a default - // case. This should have been an exhaustive match, so check to see if - // all the cases were covered. - let default_expr = match match_info.scrutinee.r#type.match_prim_spine() { - // No need for a default case if all the values were covered - Some((Prim::BoolType, [])) if branches.len() >= 2 => None, - _ => Some(self.elab_match_absurd(is_reachable, match_info)), + fn synth_param( + &mut self, + param: &Param<'_, ByteRange>, + ) -> (CheckedPattern<'arena>, Scrutinee<'arena>) { + let (pattern, _, r#type) = self.synth_ann_pattern(¶m.pattern, param.r#type.as_ref()); + let expr = + core::Term::LocalVar(self.file_range(pattern.range()).into(), env::Index::last()); + let scrut = Scrutinee { + range: pattern.range(), + expr: self.scope.to_scope(expr), + r#type, }; - - core::Term::ConstMatch( - full_span, - match_info.scrutinee.expr, - self.scope.to_scope_from_iter(branches.into_iter()), - default_expr.map(|expr| (None, self.scope.to_scope(expr) as &_)), - ) + (pattern, scrut) } - /// Elaborate unreachable match cases. This is useful for that these cases - /// are correctly typed, even if they are never actually needed. - fn elab_match_unreachable<'a>( + fn check_param( &mut self, - match_info: &MatchInfo<'arena>, - equations: impl Iterator, Term<'a, ByteRange>)>, - ) { - self.elab_match(match_info, false, equations); + param: &Param<'_, ByteRange>, + expected_type: &ArcValue<'arena>, + ) -> (CheckedPattern<'arena>, Scrutinee<'arena>) { + let pattern = self.check_ann_pattern(¶m.pattern, param.r#type.as_ref(), expected_type); + let expr = + core::Term::LocalVar(self.file_range(pattern.range()).into(), env::Index::last()); + let scrut = Scrutinee { + range: pattern.range(), + expr: self.scope.to_scope(expr), + r#type: expected_type.clone(), + }; + (pattern, scrut) } - /// All the equations have been consumed. - fn elab_match_absurd( + fn elab_match( &mut self, - is_reachable: bool, - match_info: &MatchInfo<'arena>, + mut matrix: PatMatrix<'arena>, + bodies: &[Body<'arena>], + match_range: ByteRange, + scrut_range: ByteRange, ) -> core::Term<'arena> { - // Report if we can still reach this point - if is_reachable { - // TODO: this should be admitted if the scrutinee type is uninhabited - self.push_message(Message::NonExhaustiveMatchExpr { - match_expr_range: self.file_range(match_info.range), - scrutinee_expr_range: self.file_range(match_info.scrutinee.range), - }); - } - core::Term::Prim( - self.file_range(match_info.range).into(), - Prim::ReportedError, - ) + debug_assert_eq!( + matrix.num_rows(), + bodies.len(), + "Must have one body for each row" + ); + patterns::check_coverage(self, &matrix, match_range, scrut_range); + patterns::compile_match(self, &mut matrix, bodies, EnvLen::new()) } } @@ -2423,42 +2234,10 @@ impl_from_str_radix!(u16); impl_from_str_radix!(u32); impl_from_str_radix!(u64); -/// Simple patterns that have had some initial elaboration performed on them -#[derive(Debug)] -enum CheckedPattern { - /// Pattern that binds local variable - Binder(FileRange, StringId), - /// Placeholder patterns that match everything - Placeholder(FileRange), - /// Constant literals - ConstLit(FileRange, Const), - /// Error sentinel - ReportedError(FileRange), -} - /// Scrutinee of a match expression -struct Scrutinee<'arena> { +#[derive(Debug, Clone)] +pub struct Scrutinee<'arena> { range: ByteRange, expr: &'arena core::Term<'arena>, r#type: ArcValue<'arena>, } - -struct MatchInfo<'arena> { - /// The full range of the match expression - range: ByteRange, - /// The expression being matched on - scrutinee: Scrutinee<'arena>, - /// The expected type of the match arms - expected_type: ArcValue<'arena>, -} - -#[cfg(test)] -mod tests { - use super::*; - - #[test] - #[cfg(target_pointer_width = "64")] - fn checked_pattern_size() { - assert_eq!(std::mem::size_of::(), 32); - } -} diff --git a/fathom/src/surface/elaboration/order.rs b/fathom/src/surface/elaboration/order.rs index ce9f7a32d..3363a0198 100644 --- a/fathom/src/surface/elaboration/order.rs +++ b/fathom/src/surface/elaboration/order.rs @@ -333,6 +333,12 @@ fn push_pattern(pattern: &Pattern, local_names: &mut Vec) { Pattern::StringLiteral(_, _) => {} Pattern::NumberLiteral(_, _) => {} Pattern::BooleanLiteral(_, _) => {} + Pattern::RecordLiteral(_, fields) => fields + .iter() + .for_each(|field| push_pattern(&field.pattern, local_names)), + Pattern::TupleLiteral(_, patterns) => patterns + .iter() + .for_each(|pattern| push_pattern(pattern, local_names)), } } @@ -345,5 +351,11 @@ fn pop_pattern(pattern: &Pattern, local_names: &mut Vec) { Pattern::StringLiteral(_, _) => {} Pattern::NumberLiteral(_, _) => {} Pattern::BooleanLiteral(_, _) => {} + Pattern::RecordLiteral(_, fields) => fields + .iter() + .for_each(|field| pop_pattern(&field.pattern, local_names)), + Pattern::TupleLiteral(_, patterns) => patterns + .iter() + .for_each(|pattern| pop_pattern(pattern, local_names)), } } diff --git a/fathom/src/surface/elaboration/patterns.rs b/fathom/src/surface/elaboration/patterns.rs new file mode 100644 index 000000000..b03c12117 --- /dev/null +++ b/fathom/src/surface/elaboration/patterns.rs @@ -0,0 +1,755 @@ +use super::*; +use crate::surface::elaboration; + +mod compile; +mod coverage; + +pub use self::compile::compile_match; +pub use self::coverage::check_coverage; + +/// Simple patterns that have had some initial elaboration performed on them +#[derive(Debug, Clone)] +pub enum CheckedPattern<'arena> { + /// Error sentinel + ReportedError(ByteRange), + /// Placeholder patterns that match everything + Placeholder(ByteRange), + /// Pattern that binds local variable + Binder(ByteRange, StringId), + /// Constant literals + ConstLit(ByteRange, Const), + /// Record literals + RecordLit(ByteRange, &'arena [StringId], &'arena [Self]), +} + +impl<'arena> CheckedPattern<'arena> { + pub fn range(&self) -> ByteRange { + match self { + CheckedPattern::ReportedError(range) + | CheckedPattern::Placeholder(range) + | CheckedPattern::Binder(range, _) + | CheckedPattern::ConstLit(range, _) + | CheckedPattern::RecordLit(range, _, _) => *range, + } + } + + pub fn name(&self) -> Option { + match self { + CheckedPattern::Binder(_, name) => Some(*name), + _ => None, + } + } + + /// Returns `true` if `self` is a "wildcard" pattern - ie always matches its + /// scrutinee + pub fn is_wildcard(&self) -> bool { + match self { + CheckedPattern::ReportedError(_) + | CheckedPattern::Placeholder(_) + | CheckedPattern::Binder(_, _) => true, + CheckedPattern::ConstLit(_, _) | CheckedPattern::RecordLit(_, _, _) => false, + } + } + + /// Returns `true` if `self` evaluates its scrutinee exactly once. + /// Used as a heuristic to prevent increase in runtime when expanding + /// pattern matches + pub fn is_atomic(&self) -> bool { + match self { + CheckedPattern::ReportedError(_) + | CheckedPattern::Placeholder(_) + | CheckedPattern::Binder(_, _) + | CheckedPattern::ConstLit(_, _) => true, + CheckedPattern::RecordLit(_, _, _) => false, + } + } + + pub fn is_error(&self) -> bool { + matches!(self, CheckedPattern::ReportedError(_)) + } +} + +#[derive(Debug, Copy, Clone, PartialEq, Eq)] +pub enum PatternMode { + Fun, + Let, + Match, +} + +impl<'interner, 'arena> Context<'interner, 'arena> { + /// Check that a pattern matches an expected type. + pub fn check_pattern( + &mut self, + pattern: &Pattern<'_, ByteRange>, + expected_type: &ArcValue<'arena>, + ) -> CheckedPattern<'arena> { + let expected_type = self.elim_env().force(expected_type); + + match (pattern, expected_type.as_ref()) { + (Pattern::Name(range, name), _) => CheckedPattern::Binder(*range, *name), + (Pattern::Placeholder(range), _) => CheckedPattern::Placeholder(*range), + (Pattern::StringLiteral(range, lit), _) => { + let constant = match expected_type.match_prim_spine() { + Some((Prim::U8Type, [])) => self.parse_ascii(*range, *lit, Const::U8), + Some((Prim::U16Type, [])) => self.parse_ascii(*range, *lit, Const::U16), + Some((Prim::U32Type, [])) => self.parse_ascii(*range, *lit, Const::U32), + Some((Prim::U64Type, [])) => self.parse_ascii(*range, *lit, Const::U64), + // Some((Prim::Array8Type, [len, _])) => todo!(), + // Some((Prim::Array16Type, [len, _])) => todo!(), + // Some((Prim::Array32Type, [len, _])) => todo!(), + // Some((Prim::Array64Type, [len, _])) => todo!(), + Some((Prim::ReportedError, _)) => None, + _ => { + let expected_type = self.pretty_print_value(&expected_type); + self.push_message(Message::StringLiteralNotSupported { + range: self.file_range(*range), + expected_type, + }); + None + } + }; + + match constant { + Some(constant) => CheckedPattern::ConstLit(*range, constant), + None => CheckedPattern::ReportedError(*range), + } + } + (Pattern::NumberLiteral(range, lit), _) => { + let constant = match expected_type.match_prim_spine() { + Some((Prim::U8Type, [])) => self.parse_number_radix(*range, *lit, Const::U8), + Some((Prim::U16Type, [])) => self.parse_number_radix(*range, *lit, Const::U16), + Some((Prim::U32Type, [])) => self.parse_number_radix(*range, *lit, Const::U32), + Some((Prim::U64Type, [])) => self.parse_number_radix(*range, *lit, Const::U64), + Some((Prim::S8Type, [])) => self.parse_number(*range, *lit, Const::S8), + Some((Prim::S16Type, [])) => self.parse_number(*range, *lit, Const::S16), + Some((Prim::S32Type, [])) => self.parse_number(*range, *lit, Const::S32), + Some((Prim::S64Type, [])) => self.parse_number(*range, *lit, Const::S64), + Some((Prim::F32Type, [])) => self.parse_number(*range, *lit, Const::F32), + Some((Prim::F64Type, [])) => self.parse_number(*range, *lit, Const::F64), + Some((Prim::ReportedError, _)) => None, + _ => { + let expected_type = self.pretty_print_value(&expected_type); + self.push_message(Message::NumericLiteralNotSupported { + range: self.file_range(*range), + expected_type, + }); + None + } + }; + + match constant { + Some(constant) => CheckedPattern::ConstLit(*range, constant), + None => CheckedPattern::ReportedError(*range), + } + } + (Pattern::BooleanLiteral(range, boolean), _) => { + let constant = match expected_type.match_prim_spine() { + Some((Prim::BoolType, [])) => match *boolean { + true => Some(Const::Bool(true)), + false => Some(Const::Bool(false)), + }, + _ => { + self.push_message(Message::BooleanLiteralNotSupported { + range: self.file_range(*range), + }); + None + } + }; + + match constant { + Some(constant) => CheckedPattern::ConstLit(*range, constant), + None => CheckedPattern::ReportedError(*range), + } + } + ( + Pattern::RecordLiteral(range, pattern_fields), + Value::RecordType(labels, telescope), + ) => { + if self + .check_record_fields(*range, pattern_fields, |field| field.label, labels) + .is_err() + { + return CheckedPattern::ReportedError(*range); + } + + let mut telescope = telescope.clone(); + let mut pattern_fields = pattern_fields.iter(); + let mut patterns = SliceVec::new(self.scope, labels.len()); + + while let Some((field, (r#type, next_telescope))) = Option::zip( + pattern_fields.next(), + self.elim_env().split_telescope(telescope.clone()), + ) { + let pattern = self.check_pattern(&field.pattern, &r#type); + telescope = next_telescope(Spanned::empty(Arc::new(Value::local_var( + self.local_env.len().next_level(), + )))); + patterns.push(pattern); + } + CheckedPattern::RecordLit(*range, labels, patterns.into()) + } + (Pattern::TupleLiteral(range, elem_patterns), Value::RecordType(labels, telescope)) => { + if self + .check_tuple_fields(*range, elem_patterns, |pattern| pattern.range(), labels) + .is_err() + { + return CheckedPattern::ReportedError(*range); + } + + let mut telescope = telescope.clone(); + let mut elem_patterns = elem_patterns.iter(); + let mut patterns = SliceVec::new(self.scope, elem_patterns.len()); + + while let Some((pattern, (r#type, next_telescope))) = Option::zip( + elem_patterns.next(), + self.elim_env().split_telescope(telescope.clone()), + ) { + let pattern = self.check_pattern(pattern, &r#type); + telescope = next_telescope(Spanned::empty(Arc::new(Value::local_var( + self.local_env.len().next_level(), + )))); + patterns.push(pattern); + } + + CheckedPattern::RecordLit(*range, labels, patterns.into()) + } + _ => { + let range = pattern.range(); + let (pattern, r#type) = self.synth_pattern(pattern); + match self.unification_context().unify(&r#type, &expected_type) { + Ok(()) => pattern, + Err(error) => { + let found = self.pretty_print_value(&r#type); + let expected = self.pretty_print_value(&expected_type); + self.push_message(Message::FailedToUnify { + range: self.file_range(range), + found, + expected, + error, + }); + CheckedPattern::ReportedError(range) + } + } + } + } + } + + /// Synthesize the type of a pattern. + pub fn synth_pattern( + &mut self, + pattern: &Pattern, + ) -> (CheckedPattern<'arena>, ArcValue<'arena>) { + let file_range = self.file_range(pattern.range()); + match pattern { + Pattern::Name(range, name) => { + let source = MetaSource::NamedPatternType(file_range, *name); + let r#type = self.push_unsolved_type(source); + (CheckedPattern::Binder(*range, *name), r#type) + } + Pattern::Placeholder(range) => { + let source = MetaSource::PlaceholderPatternType(file_range); + let r#type = self.push_unsolved_type(source); + (CheckedPattern::Placeholder(*range), r#type) + } + Pattern::StringLiteral(range, _) => { + self.push_message(Message::AmbiguousStringLiteral { range: file_range }); + let source = MetaSource::ReportedErrorType(file_range); + let r#type = self.push_unsolved_type(source); + (CheckedPattern::ReportedError(*range), r#type) + } + Pattern::NumberLiteral(range, _) => { + self.push_message(Message::AmbiguousNumericLiteral { range: file_range }); + let source = MetaSource::ReportedErrorType(file_range); + let r#type = self.push_unsolved_type(source); + (CheckedPattern::ReportedError(*range), r#type) + } + Pattern::BooleanLiteral(range, val) => { + let r#const = Const::Bool(*val); + let r#type = self.bool_type.clone(); + (CheckedPattern::ConstLit(*range, r#const), r#type) + } + Pattern::RecordLiteral(range, pattern_fields) => { + let (labels, pattern_fields) = + self.report_duplicate_labels(*range, pattern_fields, |f| f.label); + + let mut patterns = SliceVec::new(self.scope, labels.len()); + let mut types = SliceVec::new(self.scope, labels.len()); + + for field in pattern_fields { + let (pattern, r#type) = self.synth_pattern(&field.pattern); + patterns.push(pattern); + types.push(self.quote_env().quote(self.scope, &r#type)); + } + + let telescope = Telescope::new(self.local_env.exprs.clone(), types.into()); + ( + CheckedPattern::RecordLit(*range, labels, patterns.into()), + Spanned::new( + file_range.into(), + Arc::new(Value::RecordType(labels, telescope)), + ), + ) + } + Pattern::TupleLiteral(range, elem_patterns) => { + let mut interner = self.interner.borrow_mut(); + let labels = interner.get_tuple_labels(0..elem_patterns.len()); + let labels = self.scope.to_scope_from_iter(labels.iter().copied()); + + let mut patterns = SliceVec::new(self.scope, labels.len()); + let mut types = SliceVec::new(self.scope, labels.len()); + + for pattern in elem_patterns.iter() { + let (pattern, r#type) = self.synth_pattern(pattern); + patterns.push(pattern); + types.push(self.quote_env().quote(self.scope, &r#type)); + } + + let telescope = Telescope::new(self.local_env.exprs.clone(), types.into()); + ( + CheckedPattern::RecordLit(*range, labels, patterns.into()), + Spanned::new( + file_range.into(), + Arc::new(Value::RecordType(labels, telescope)), + ), + ) + } + } + } + + /// Check that the type of an annotated pattern matches an expected type. + pub fn check_ann_pattern( + &mut self, + pattern: &Pattern, + r#type: Option<&Term<'_, ByteRange>>, + expected_type: &ArcValue<'arena>, + ) -> CheckedPattern<'arena> { + match r#type { + None => self.check_pattern(pattern, expected_type), + Some(r#type) => { + let range = r#type.range(); + let r#type = self.check(r#type, &self.universe.clone()); + let r#type = self.eval_env().eval(&r#type); + + match self.unification_context().unify(&r#type, expected_type) { + Ok(()) => self.check_pattern(pattern, &r#type), + Err(error) => { + let found = self.pretty_print_value(&r#type); + let expected = self.pretty_print_value(expected_type); + self.push_message(Message::FailedToUnify { + range: self.file_range(range), + found, + expected, + error, + }); + CheckedPattern::ReportedError(range) + } + } + } + } + } + + /// Synthesize the type of an annotated pattern. + pub fn synth_ann_pattern( + &mut self, + pattern: &Pattern, + r#type: Option<&Term<'_, ByteRange>>, + ) -> (CheckedPattern<'arena>, core::Term<'arena>, ArcValue<'arena>) { + match r#type { + None => { + let (pattern, type_value) = self.synth_pattern(pattern); + let r#type = self.quote_env().quote(self.scope, &type_value); + (pattern, r#type, type_value) + } + Some(r#type) => { + let r#type = self.check(r#type, &self.universe.clone()); + let type_value = self.eval_env().eval(&r#type); + (self.check_pattern(pattern, &type_value), r#type, type_value) + } + } + } + + /// Push a pattern onto the local context + pub fn push_pattern( + &mut self, + pattern: &CheckedPattern<'arena>, + scrut: Scrutinee<'arena>, + value: ArcValue<'arena>, + mode: PatternMode, + toplevel: bool, + ) -> Vec<(Option, Scrutinee<'arena>)> { + let mut defs = Vec::new(); + self.push_pattern_inner(pattern, scrut, value, mode, toplevel, &mut defs); + defs + } + + fn push_pattern_inner( + &mut self, + pattern: &CheckedPattern<'arena>, + scrut: Scrutinee<'arena>, + value: ArcValue<'arena>, + mode: PatternMode, + toplevel: bool, + defs: &mut Vec<(Option, Scrutinee<'arena>)>, + ) { + let r#type = scrut.r#type.clone(); + match pattern { + CheckedPattern::ReportedError(_) | CheckedPattern::Placeholder(_) => { + match (mode, toplevel) { + (PatternMode::Fun, true) => self.local_env.push_param(None, r#type), + (PatternMode::Let, true) => { + defs.push((None, scrut)); + self.local_env.push_def(None, value, r#type) + } + (PatternMode::Match, true) => self.local_env.push_def(None, value, r#type), + _ => {} + } + } + CheckedPattern::Binder(_, name) => match (mode, toplevel) { + (PatternMode::Fun, true) => self.local_env.push_param(Some(*name), r#type), + (PatternMode::Fun, _) | (PatternMode::Let, _) | (PatternMode::Match, _) => { + defs.push((Some(*name), scrut)); + self.local_env.push_def(Some(*name), value, r#type) + } + }, + CheckedPattern::ConstLit(_, _) => match (mode, toplevel) { + (PatternMode::Fun, true) => self.local_env.push_param(None, r#type), + (PatternMode::Let, true) => { + defs.push((None, scrut)); + self.local_env.push_def(None, value, r#type) + } + _ => {} + }, + CheckedPattern::RecordLit(_, labels, patterns) => { + if let (PatternMode::Fun, true) = (mode, toplevel) { + self.local_env.push_param(None, r#type.clone()) + } + + let range = scrut.range; + let mut iter = Iterator::zip(labels.iter(), patterns.iter()); + let mut telescope = self + .elim_env() + .force(&r#type) + .match_record_type() + .unwrap() + .clone(); + while let Some(((label, pattern), (r#type, next_telescope))) = Option::zip( + iter.next(), + self.elim_env().split_telescope(telescope.clone()), + ) { + telescope = next_telescope(self.local_env.next_var()); + let value = self.elim_env().record_proj(value.clone(), *label); + let expr = + core::Term::RecordProj(self.file_range(range).into(), scrut.expr, *label); + let scrut = Scrutinee { + range, + expr: self.scope.to_scope(expr), + r#type, + }; + self.push_pattern_inner(pattern, scrut, value, mode, false, defs) + } + } + } + } +} + +#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord)] +pub enum Constructor<'arena> { + Const(Const), + Record(&'arena [StringId]), +} + +impl<'arena> Constructor<'arena> { + /// Return number of fields `self` carries + pub fn arity(&self) -> usize { + match self { + Constructor::Const(_) => 0, + Constructor::Record(labels) => labels.len(), + } + } + + pub fn is_exhaustive(ctors: &[Constructor]) -> bool { + match ctors.first() { + None => false, + Some(ctor) => match ctor.num_inhabitants() { + None => false, + Some(n) => ctors.len() as u128 >= n, + }, + } + } + + /// Return the number of inhabitants of `self`. + /// `None` represents infinity + pub fn num_inhabitants(&self) -> Option { + match self { + Constructor::Const(r#const) => r#const.num_inhabitants(), + Constructor::Record(_) => Some(1), + } + } + + pub fn as_const(&self) -> Option<&Const> { + match self { + Constructor::Const(r#const) => Some(r#const), + _ => None, + } + } +} + +#[derive(Debug, Clone)] +pub struct PatMatrix<'arena> { + rows: Vec>, + indices: Vec, +} + +#[derive(Debug, Clone)] +/// The right hand side of a match clause +pub struct Body<'arena> { + /// The expression to be evaluated + expr: core::Term<'arena>, + /// The variables to be let-bound before `expr` is evaluated + defs: Vec<(Option, Scrutinee<'arena>)>, +} + +impl<'arena> Body<'arena> { + pub fn new(expr: core::Term<'arena>, defs: Vec<(Option, Scrutinee<'arena>)>) -> Self { + Self { expr, defs } + } +} + +impl<'arena> PatMatrix<'arena> { + pub fn new(rows: Vec>) -> Self { + if let Some((first, rows)) = rows.split_first() { + for row in rows { + debug_assert_eq!( + first.pairs.len(), + row.pairs.len(), + "All rows must be same length" + ); + } + } + let indices = (0..rows.len()).collect(); + Self { rows, indices } + } + + pub fn singleton(scrut: Scrutinee<'arena>, pat: CheckedPattern<'arena>) -> Self { + Self::new(vec![PatRow::singleton((pat, scrut))]) + } + + pub fn num_rows(&self) -> usize { + self.rows.len() + } + + pub fn num_columns(&self) -> Option { + self.rows.first().map(|row| row.len()) + } + + /// Return true if `self` is the null matrix, `∅` - ie `self` has zero rows + pub fn is_null(&self) -> bool { + self.num_rows() == 0 + } + + /// Return true if `self` is the unit matrix, `()` - ie `self` has zero + /// columns and at least one row + pub fn is_unit(&self) -> bool { + self.num_columns() == Some(0) + } + + /// Iterate over all the pairs in the `index`th column + pub fn column(&self, index: usize) -> impl ExactSizeIterator> + '_ { + self.rows.iter().map(move |row| &row.pairs[index]) + } + + pub fn row(&self, index: usize) -> &PatRow<'arena> { + &self.rows[index] + } + + pub fn row_index(&self, index: usize) -> usize { + self.indices[index] + } + + /// Collect all the `Constructor`s in the `index`th column + pub fn column_constructors(&self, index: usize) -> Vec> { + let mut ctors = Vec::with_capacity(self.num_rows()); + for (pat, _) in self.column(index) { + match pat { + CheckedPattern::ReportedError(_) + | CheckedPattern::Placeholder(_) + | CheckedPattern::Binder(_, _) => continue, + CheckedPattern::ConstLit(_, r#const) => ctors.push(Constructor::Const(*r#const)), + CheckedPattern::RecordLit(_, labels, _) => ctors.push(Constructor::Record(labels)), + } + } + ctors.sort_unstable(); + ctors.dedup(); + ctors + } + + pub fn iter(&self) -> impl ExactSizeIterator, usize)> { + self.rows.iter().zip(self.indices.iter().copied()) + } +} + +pub type PatPair<'arena> = (CheckedPattern<'arena>, Scrutinee<'arena>); + +#[derive(Debug, Clone)] +pub struct PatRow<'arena> { + pairs: Vec>, +} + +impl<'arena> PatRow<'arena> { + pub fn new(pairs: Vec>) -> Self { + Self { pairs } + } + + pub fn singleton(pair: PatPair<'arena>) -> Self { + Self::new(vec![pair]) + } + + pub fn tail(&self) -> Self { + debug_assert!(!self.is_empty()); + Self::new(self.pairs[1..].to_vec()) + } + + pub fn len(&self) -> usize { + self.pairs.len() + } + + pub fn is_empty(&self) -> bool { + self.pairs.is_empty() + } + + pub fn first(&self) -> Option<&PatPair<'arena>> { + self.pairs.first() + } + + pub fn all_wildcards(&self) -> bool { + self.pairs.iter().all(|(pat, _)| pat.is_wildcard()) + } + + pub fn split_first(&self) -> Option<(&PatPair<'arena>, Self)> { + let (first, rest) = self.pairs.split_first()?; + Some((first, Self::new(rest.to_vec()))) + } + + pub fn append(&mut self, mut other: Self) { + self.pairs.append(&mut other.pairs); + } + + pub fn patterns(&self) -> impl ExactSizeIterator> { + self.pairs.iter().map(|(pattern, _)| pattern) + } +} + +impl<'arena> CheckedPattern<'arena> { + /// Specialise `self` with respect to the constructor `ctor`. + pub fn specialize( + &self, + ctx: &mut elaboration::Context<'_, 'arena>, + ctor: &Constructor, + scrut: &Scrutinee<'arena>, + ) -> Option> { + match self { + CheckedPattern::ReportedError(range) + | CheckedPattern::Placeholder(range) + | CheckedPattern::Binder(range, _) => { + let columns = + vec![(CheckedPattern::Placeholder(*range), scrut.clone()); ctor.arity()]; + Some(PatRow::new(columns)) + } + CheckedPattern::ConstLit(_, r#const) if *ctor == Constructor::Const(*r#const) => { + Some(PatRow::new(vec![])) + } + CheckedPattern::RecordLit(_, labels, patterns) + if *ctor == Constructor::Record(labels) => + { + let mut columns = Vec::with_capacity(labels.len()); + let mut iter = Iterator::zip(labels.iter(), patterns.iter()); + let mut telescope = ctx + .elim_env() + .force(&scrut.r#type) + .match_record_type() + .unwrap() + .clone(); + + while let Some(((label, pattern), (r#type, next_telescope))) = Option::zip( + iter.next(), + ctx.elim_env().split_telescope(telescope.clone()), + ) { + telescope = next_telescope(ctx.local_env.next_var()); + let scrut_expr = core::Term::RecordProj(Span::Empty, scrut.expr, *label); + let scrut_expr = ctx.scope.to_scope(scrut_expr); + let scrut = Scrutinee { + range: scrut.range, + expr: scrut_expr, + r#type, + }; + columns.push((pattern.clone(), scrut)); + } + Some(PatRow::new(columns)) + } + CheckedPattern::ConstLit(_, _) | CheckedPattern::RecordLit(_, _, _) => None, + } + } +} + +impl<'arena> PatRow<'arena> { + /// Specialise `self` with respect to the constructor `ctor`. + pub fn specialize( + &self, + ctx: &mut elaboration::Context<'_, 'arena>, + ctor: &Constructor, + ) -> Option> { + debug_assert!(!self.pairs.is_empty(), "Cannot specialize empty PatRow"); + let ((pat, scrut), rest) = self.split_first().unwrap(); + let mut row = pat.specialize(ctx, ctor, scrut)?; + row.append(rest); + Some(row) + } +} + +impl<'arena> PatMatrix<'arena> { + /// Specialise `self` with respect to the constructor `ctor`. + /// This is the `S` function in *Compiling pattern matching to good decision + /// trees* + pub fn specialize( + &self, + ctx: &mut elaboration::Context<'_, 'arena>, + ctor: &Constructor, + ) -> Self { + let (rows, indices) = self + .iter() + .flat_map(|(row, body)| { + let row = row.specialize(ctx, ctor)?; + Some((row, body)) + }) + .unzip(); + Self { rows, indices } + } + + /// Discard the first column, and all rows starting with a constructed + /// pattern. This is the `D` function in *Compiling pattern matching to + /// good decision trees* + pub fn default(&self) -> Self { + debug_assert!(!self.is_unit(), "Cannot default PatMatrix with no columns"); + let (rows, indices) = self + .iter() + .flat_map(|(row, body)| match row.first().unwrap().0 { + CheckedPattern::ReportedError(_) + | CheckedPattern::Placeholder(_) + | CheckedPattern::Binder(_, _) => Some((row.tail(), body)), + CheckedPattern::ConstLit(_, _) | CheckedPattern::RecordLit(_, _, _) => None, + }) + .unzip(); + Self { rows, indices } + } +} + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + #[cfg(target_pointer_width = "64")] + fn checked_pattern_size() { + assert_eq!(std::mem::size_of::(), 48); + } +} diff --git a/fathom/src/surface/elaboration/patterns/compile.rs b/fathom/src/surface/elaboration/patterns/compile.rs new file mode 100644 index 000000000..eef925992 --- /dev/null +++ b/fathom/src/surface/elaboration/patterns/compile.rs @@ -0,0 +1,162 @@ +//! # Bibliography +//! - [Compiling pattern matching to good decision trees](https://dl.acm.org/doi/10.1145/1411304.1411311) +//! - [The Case for Pattern Matching](https://alan-j-hu.github.io/writing/pattern-matching.html) +//! - [How to compile pattern matching](https://julesjacobs.com/notes/patternmatching/patternmatching.pdf) + +// TODO: Use join points to prevent code size explosion. See [Compiling without continuations](https://www.microsoft.com/en-us/research/publication/compiling-without-continuations) + +use super::*; +use crate::surface::elaboration; + +/// Compilation of pattern matrices to decision trees. +/// This is the `CC` function in *Compiling pattern matching to good decision +/// trees*. +pub fn compile_match<'arena>( + ctx: &mut elaboration::Context<'_, 'arena>, + matrix: &mut PatMatrix<'arena>, + bodies: &[Body<'arena>], + mut shift_amount: EnvLen, +) -> core::Term<'arena> { + // Base case 1: + // If the matrix is empty, matching always fails. + if matrix.is_null() { + return core::Term::error(Span::Empty); // TODO + } + + // Base case 2: + // If the first row is all wildcards, matching always suceeds. + if matrix.row(0).all_wildcards() { + let index = matrix.row_index(0); + let Body { expr, defs } = &bodies[index]; + + let initial_len = ctx.local_env.len(); + #[allow(clippy::needless_collect)] + let defs: Vec<_> = defs + .iter() + .map(|(def_name, scrut)| { + let def_name = *def_name; + let def_range = scrut.range; + let def_type = ctx.quote_env().quote(ctx.scope, &scrut.r#type); + let def_expr = scrut.expr.shift(ctx.scope, shift_amount); + let def_value = ctx.eval_env().eval(&def_expr); + ctx.local_env + .push_def(def_name, def_value, scrut.r#type.clone()); + shift_amount.push(); + (def_range, def_name, def_type, def_expr) + }) + .collect(); + ctx.local_env.truncate(initial_len); + + return defs.into_iter().rev().fold( + expr.clone(), + |body, (def_range, def_name, def_type, def_expr)| { + core::Term::Let( + ctx.file_range(def_range).into(), + def_name, + ctx.scope.to_scope(def_type), + ctx.scope.to_scope(def_expr), + ctx.scope.to_scope(body), + ) + }, + ); + } + + // Inductive case: + // The matrix must have at least one column with at least one non-wildcard + // pattern. Select such a column, and for each constructor in the column, + // generate a decision subtree. If the column is non-exhaustive, generate a + // default branch as well. + let column = matrix.column_to_split_on().unwrap(); + matrix.swap_columns(0, column); + for (pat, scrut) in matrix.column(0) { + match pat { + CheckedPattern::ConstLit(_, _) => { + let scrut_expr = scrut.expr.shift(ctx.scope, shift_amount); + let ctors = matrix.column_constructors(0); + + let mut branches = SliceVec::new(ctx.scope, ctors.len()); + for ctor in ctors.iter() { + let r#const = ctor.as_const().unwrap(); + let mut matrix = matrix.specialize(ctx, ctor); + let expr = compile_match(ctx, &mut matrix, bodies, shift_amount); + branches.push((*r#const, expr)) + } + + let default_branch = match Constructor::is_exhaustive(&ctors) { + true => None, + false => { + let name = None; // TODO: recover default branch name? + let mut matrix = matrix.default(); + + let value = ctx.eval_env().eval(&scrut_expr); + ctx.local_env.push_def(name, value, scrut.r#type.clone()); + shift_amount.push(); + let expr = compile_match(ctx, &mut matrix, bodies, shift_amount); + ctx.local_env.pop(); + + Some((name, ctx.scope.to_scope(expr) as &_)) + } + }; + + return core::Term::ConstMatch( + Span::Empty, + ctx.scope.to_scope(scrut_expr), + branches.into(), + default_branch, + ); + } + + // There is only one constructor for each record type, + // so we only need to generate a single subtree (ie no branching needed) + CheckedPattern::RecordLit(_, labels, _) => { + let mut matrix = matrix.specialize(ctx, &Constructor::Record(labels)); + return compile_match(ctx, &mut matrix, bodies, shift_amount); + } + + // Skip over non-constructor patterns + CheckedPattern::ReportedError(_) + | CheckedPattern::Placeholder(_) + | CheckedPattern::Binder(_, _) => continue, + } + } + + unreachable!() +} + +impl<'arena> PatMatrix<'arena> { + /// Return the index of any column in the matrix with at least one + /// non-wildcard pattern. At the moment, we simply selec the leftmost + /// column, but more advanced splitting heuristcs can be used to + /// minimize the size of the decision tree and potentially skip some tests + /// altogether (see section 8 of *Compiling pattern matching to good + /// decision trees*) + pub fn column_to_split_on(&self) -> Option { + debug_assert!(!self.is_null(), "Cannot split null PatternMatrix"); + + (0..self.num_columns().unwrap()).find(|&column| { + self.column(column).any(|(pat, _)| match pat { + CheckedPattern::ConstLit(_, _) | CheckedPattern::RecordLit(_, _, _) => true, + CheckedPattern::ReportedError(_) + | CheckedPattern::Placeholder(_) + | CheckedPattern::Binder(_, _) => false, + }) + }) + } + + pub fn swap_columns(&mut self, column1: usize, column2: usize) { + debug_assert!( + column1 < self.num_columns().unwrap_or(0), + "column1 is out of bounds (num_columns = {:?})", + self.num_columns() + ); + debug_assert!( + column2 < self.num_columns().unwrap_or(0), + "column2 is out of bounds (num_columns = {:?})", + self.num_columns() + ); + + for row in self.rows.iter_mut() { + row.pairs.swap(column1, column2); + } + } +} diff --git a/fathom/src/surface/elaboration/patterns/coverage.rs b/fathom/src/surface/elaboration/patterns/coverage.rs new file mode 100644 index 000000000..93fd43fd3 --- /dev/null +++ b/fathom/src/surface/elaboration/patterns/coverage.rs @@ -0,0 +1,133 @@ +//! # Bibliography +//! - [Warnings for pattern matching](http://moscova.inria.fr/~maranget/papers/warn/index.html) +//! - [rustc usefulness check](https://github.com/rust-lang/rust/blob/8a09420ac48658cad726e0a6997687ceac4151e3/compiler/rustc_mir_build/src/thir/pattern/usefulness.rs) + +// TODO: Currently we only report that the match is non-exhaustive, but we do +// not report which patterns are missing. The algorithm for calculating the set +// of missing patterns is described in part two of *Warnings for pattern +// matching* + +use super::*; +use crate::surface::elaboration; + +pub fn check_coverage<'arena>( + ctx: &mut elaboration::Context<'_, 'arena>, + matrix: &PatMatrix<'arena>, + match_range: ByteRange, + scrut_range: ByteRange, +) { + let dummy_scrut = Scrutinee { + range: scrut_range, + expr: ctx.scope.to_scope(core::Term::error(Span::Empty)), + r#type: ArcValue::new(ctx.file_range(scrut_range).into(), Arc::new(Value::ERROR)), + }; + let row = PatRow::singleton((CheckedPattern::Placeholder(match_range), dummy_scrut)); + + // A matrix is exhaustive iff the the wildcard pattern `_` is not useful + if is_useful(ctx, matrix, &row) { + ctx.push_message(Message::NonExhaustiveMatchExpr { + match_expr_range: ctx.file_range(match_range), + scrutinee_expr_range: ctx.file_range(scrut_range), + }); + } + + // A matrix row is reachable iff it is useful relative to the rows in the matrix + // above it + let mut rows = Vec::with_capacity(matrix.num_rows()); + for (row, _) in matrix.iter() { + let matrix = PatMatrix::new(rows.clone()); + rows.push(row.clone()); + + // Don't check reachability for patterns with errors + if row.patterns().any(|pattern| pattern.is_error()) { + continue; + } + + if !is_useful(ctx, &matrix, row) { + let range = row.first().unwrap().0.range(); + ctx.push_message(Message::UnreachablePattern { + range: ctx.file_range(range), + }); + } + } +} + +/// A row of patterns, *q*, is useful relative to a matrix *m* iff there is a +/// value matched by `q` and not matched by *m*. This is the `U` function in +/// *Warnings for pattern matching* +fn is_useful<'arena>( + ctx: &mut elaboration::Context<'_, 'arena>, + matrix: &PatMatrix<'arena>, + row: &PatRow<'arena>, +) -> bool { + if let Some(n) = matrix.num_columns() { + debug_assert_eq!( + n, + row.len(), + "`row` must have a pattern for each column of `matrix`" + ) + } + + // Base case 1: + // If the matrix has no columns, but at least one row, the test row is not + // useful + if matrix.is_unit() { + return false; + } + + // Base case 2: + // If the matrix has no columns and no rows, the test row is useful + if matrix.is_null() { + return true; + } + + let (pat, _) = row.first().unwrap(); + match pat { + // Inductive case 1: + // If the first pattern is a constructed pattern, specialise the matrix and test row and + // recurse + CheckedPattern::ConstLit(_, r#const) => { + is_useful_ctor(ctx, matrix, row, &Constructor::Const(*r#const)) + } + CheckedPattern::RecordLit(_, labels, _) => { + is_useful_ctor(ctx, matrix, row, &Constructor::Record(labels)) + } + + // Inductive case 2: + // If the first pattern is a wildcard pattern, collect all the constructors in the first + // column of matrix and test for exhaustiveness + CheckedPattern::ReportedError(_) + | CheckedPattern::Placeholder(_) + | CheckedPattern::Binder(_, _) => { + let ctors = matrix.column_constructors(0); + match Constructor::is_exhaustive(&ctors) { + // Inductive case 2a: + // If the constructors are exhaustive, specialise the matrix and test row against + // each constructor and recurse + true => ctors + .into_iter() + .any(|ctor| is_useful_ctor(ctx, matrix, row, &ctor)), + // Inductive case 2b: + // If the constructors are not exhaustive, recurse on the defaulted matrix + false => { + let matrix = matrix.default(); + is_useful(ctx, &matrix, &row.tail()) + } + } + } + } +} + +fn is_useful_ctor<'arena>( + ctx: &mut elaboration::Context<'_, 'arena>, + matrix: &PatMatrix<'arena>, + row: &PatRow<'arena>, + ctor: &Constructor<'arena>, +) -> bool { + let matrix = matrix.specialize(ctx, ctor); + let row = row.specialize(ctx, ctor); + match row { + None => false, + Some(row) => is_useful(ctx, &matrix, &row), + } +} diff --git a/fathom/src/surface/elaboration/reporting.rs b/fathom/src/surface/elaboration/reporting.rs index ed429af47..60bad4c51 100644 --- a/fathom/src/surface/elaboration/reporting.rs +++ b/fathom/src/surface/elaboration/reporting.rs @@ -52,8 +52,8 @@ pub enum Message { }, MismatchedFieldLabels { range: FileRange, - expr_labels: Vec<(FileRange, StringId)>, - type_labels: Vec, + found_labels: Vec<(FileRange, StringId)>, + expected_labels: Vec, // TODO: add expected type // expected_type: Doc<_>, }, @@ -243,8 +243,8 @@ impl Message { } Message::MismatchedFieldLabels { range, - expr_labels, - type_labels, + found_labels: expr_labels, + expected_labels: type_labels, } => { let interner = interner.borrow(); let mut diagnostic_labels = Vec::with_capacity(expr_labels.len()); diff --git a/fathom/src/surface/grammar.lalrpop b/fathom/src/surface/grammar.lalrpop index 26d35046b..86783256f 100644 --- a/fathom/src/surface/grammar.lalrpop +++ b/fathom/src/surface/grammar.lalrpop @@ -4,10 +4,11 @@ use std::cell::RefCell; use crate::source::{ByteRange, BytePos, StringId, StringInterner}; use crate::surface::{ Arg, BinOp, ExprField, FormatField, Item, ItemDef, Module, ParseMessage, - Pattern, Param, Plicity, Term, TypeField, + Pattern, PatternField, Param, Plicity, Term, TypeField, }; use crate::surface::lexer::{Error as LexerError, Token}; + grammar<'arena, 'source>( interner: &RefCell, scope: &'arena Scope<'arena>, @@ -91,13 +92,15 @@ Item: Item<'arena, ByteRange> = { }, }; -Pattern: Pattern = { +Pattern: Pattern<'arena, ByteRange> = { => Pattern::Name(ByteRange::new(start, end), name), "_" => Pattern::Placeholder(ByteRange::new(start, end)), => Pattern::StringLiteral(ByteRange::new(start, end), string), => Pattern::NumberLiteral(ByteRange::new(start, end), number), "true" => Pattern::BooleanLiteral(ByteRange::new(start, end), true), "false" => Pattern::BooleanLiteral(ByteRange::new(start, end), false), + "{" > "}" => Pattern::RecordLiteral(ByteRange::new(start, end), fields), + > => Pattern::TupleLiteral(ByteRange::new(start, end), patterns), }; pub Term: Term<'arena, ByteRange> = { @@ -116,7 +119,7 @@ LetTerm: Term<'arena, ByteRange> = { "let" )?> "=" ";" => { Term::Let( ByteRange::new(start, end), - def_pattern, + scope.to_scope(def_pattern), def_type.map(|def_type| scope.to_scope(def_type) as &_), scope.to_scope(def_expr), scope.to_scope(body_expr), @@ -258,6 +261,10 @@ ExprField: ExprField<'arena, ByteRange> = { "=" => ExprField { label, expr }, }; +PatternField: PatternField<'arena, ByteRange> = { + "=" => PatternField { label, pattern }, +}; + BinExpr: Term<'arena, ByteRange> = { => { Term::BinOp( @@ -288,8 +295,8 @@ BinOpGte: BinOp = ">=" => BinOp::Gte(ByteRange: Tuple: &'arena [Elem] = { "(" ")" => &[], - "(" "," ")" => scope.to_scope_from_iter([term]), - "(" > ")" => terms, + "(" "," ")" => scope.to_scope_from_iter([term]), + "(" > ")" => terms, }; #[inline] diff --git a/fathom/src/surface/pretty.rs b/fathom/src/surface/pretty.rs index 97c8157a4..77b83cba8 100644 --- a/fathom/src/surface/pretty.rs +++ b/fathom/src/surface/pretty.rs @@ -89,6 +89,20 @@ impl<'interner, 'arena> Context<'interner, 'arena> { true => self.text("true"), false => self.text("false"), }, + Pattern::RecordLiteral(_, pattern_fields) => { + self.pretty_record(pattern_fields, |field| { + self.concat([ + self.string_id(field.label.1), + self.space(), + self.text("="), + self.space(), + self.pattern(&field.pattern), + ]) + }) + } + Pattern::TupleLiteral(_, patterns) => { + self.pretty_tuple(patterns, |pattern| self.pattern(pattern)) + } } } @@ -253,29 +267,25 @@ impl<'interner, 'arena> Context<'interner, 'arena> { self.space(), self.intersperse((args.iter()).map(|arg| self.arg(arg)), self.space()), ]), - Term::RecordType(_, fields) => { - let fields = fields.iter().map(|field| { - self.ident(field.label.1) - .append(" : ") - .append(self.term(&field.r#type)) - }); - self.sequence(true, self.text("{"), fields, self.text(","), self.text("}")) - } - Term::RecordLiteral(_, fields) => { - let fields = fields.iter().map(|field| { - self.ident(field.label.1) - .append(" = ") - .append(self.term(&field.expr)) - }); - self.sequence(true, self.text("{"), fields, self.text(","), self.text("}")) - } - Term::Tuple(_, terms) if terms.len() == 1 => { - self.text("(").append(self.term(&terms[0]).append(",)")) - } - Term::Tuple(_, terms) => { - let terms = terms.iter().map(|term| self.term(term)); - self.sequence(false, self.text("("), terms, self.text(","), self.text(")")) - } + Term::RecordType(_, type_fields) => self.pretty_record(type_fields, |field| { + self.concat([ + self.string_id(field.label.1), + self.space(), + self.text(":"), + self.space(), + self.term(&field.r#type), + ]) + }), + Term::RecordLiteral(_, expr_fields) => self.pretty_record(expr_fields, |field| { + self.concat([ + self.string_id(field.label.1), + self.space(), + self.text("="), + self.space(), + self.term(&field.expr), + ]) + }), + Term::Tuple(_, terms) => self.pretty_tuple(terms, |term| self.term(term)), Term::Proj(_, head_expr, labels) => self.concat([ self.term(head_expr), self.concat( @@ -419,6 +429,40 @@ impl<'interner, 'arena> Context<'interner, 'arena> { ]) .group() } + + fn pretty_tuple( + &'arena self, + terms: &[T], + pretty: impl Fn(&T) -> DocBuilder<'arena, Self>, + ) -> DocBuilder<'arena, Self> { + if terms.len() == 1 { + self.concat([self.text("("), pretty(&terms[0]), self.text(",)")]) + } else { + #[allow(clippy::redundant_closure)] + self.sequence( + false, + self.text("("), + terms.iter().map(|term| pretty(term)), + self.text(","), + self.text(")"), + ) + } + } + + fn pretty_record( + &'arena self, + fields: &[T], + pretty: impl Fn(&T) -> DocBuilder<'arena, Self>, + ) -> DocBuilder<'arena, Self> { + #[allow(clippy::redundant_closure)] + self.sequence( + true, + self.text("{"), + fields.iter().map(|field| pretty(field)), + self.text(","), + self.text("}"), + ) + } } impl<'interner, 'arena, A: 'arena> DocAllocator<'arena, A> for Context<'interner, 'arena> { diff --git a/formats/opentype.snap b/formats/opentype.snap index 9596e81c9..9b61c131b 100644 --- a/formats/opentype.snap +++ b/formats/opentype.snap @@ -30,28 +30,28 @@ def link_table : Pos -> { } -> Format -> Format = fun file_start table_record table_format => link (file_start + table_record.offset) (limit32 table_record.length table_format); def platform_id : Format = u16be; -def encoding_id : Repr platform_id -> Format = fun platform => u16be; +def encoding_id : U16 -> Format = fun platform => u16be; def empty : Format = (); def offset32 : Pos -> Format -> Format = fun base format => { offset <- u32be, link <- match offset { 0 => empty, _ => link (base + offset) format }, }; def language_id : Format = u16be; -def cmap_language_id : Repr platform_id -> Format = fun platform => language_id; +def cmap_language_id : U16 -> Format = fun platform => language_id; def small_glyph_id : Format = u8; -def cmap_subtable_format0 : Repr platform_id -> Format = fun platform => { +def cmap_subtable_format0 : U16 -> Format = fun platform => { length <- u16be, language <- cmap_language_id platform, glyph_id_array <- repeat_len16 256 small_glyph_id, }; -def cmap_subtable_format2 : Repr platform_id -> Format = fun platform => { +def cmap_subtable_format2 : U16 -> Format = fun platform => { length <- u16be, language <- cmap_language_id platform, sub_header_keys <- repeat_len16 256 u16be, }; def reserved : fun (format : Format) -> Repr format -> Format = fun format default => format; -def cmap_subtable_format4 : Repr platform_id -> Format = fun platform => { +def cmap_subtable_format4 : U16 -> Format = fun platform => { length <- u16be, language <- cmap_language_id platform, seg_count_x2 <- u16be, @@ -65,7 +65,7 @@ def cmap_subtable_format4 : Repr platform_id -> Format = fun platform => { id_delta <- repeat_len16 seg_count s16be, id_range_offsets <- repeat_len16 seg_count u16be, }; -def cmap_subtable_format6 : Repr platform_id -> Format = fun platform => { +def cmap_subtable_format6 : U16 -> Format = fun platform => { length <- u16be, language <- cmap_language_id platform, first_code <- u16be, @@ -73,14 +73,13 @@ def cmap_subtable_format6 : Repr platform_id -> Format = fun platform => { glyph_id_array <- repeat_len16 entry_count u16be, }; def language_id32 : Format = u32be; -def cmap_language_id32 : Repr platform_id -> Format = -fun platform => language_id32; +def cmap_language_id32 : U16 -> Format = fun platform => language_id32; def sequential_map_group : Format = { start_char_code <- u32be, end_char_code <- u32be, start_glyph_id <- u32be, }; -def cmap_subtable_format8 : Repr platform_id -> Format = fun platform => { +def cmap_subtable_format8 : U16 -> Format = fun platform => { _reserved <- reserved u16be 0, length <- u32be, language <- cmap_language_id32 platform, @@ -88,7 +87,7 @@ def cmap_subtable_format8 : Repr platform_id -> Format = fun platform => { num_groups <- u32be, groups <- repeat_len32 num_groups sequential_map_group, }; -def cmap_subtable_format10 : Repr platform_id -> Format = fun platform => { +def cmap_subtable_format10 : U16 -> Format = fun platform => { _reserved <- reserved u16be 0, length <- u32be, language <- cmap_language_id32 platform, @@ -96,7 +95,7 @@ def cmap_subtable_format10 : Repr platform_id -> Format = fun platform => { num_chars <- u32be, glyph_id_array <- repeat_len32 num_chars u16be, }; -def cmap_subtable_format12 : Repr platform_id -> Format = fun platform => { +def cmap_subtable_format12 : U16 -> Format = fun platform => { _reserved <- reserved u16be 0, length <- u32be, language <- cmap_language_id32 platform, @@ -104,7 +103,7 @@ def cmap_subtable_format12 : Repr platform_id -> Format = fun platform => { groups <- repeat_len32 num_groups sequential_map_group, }; def constant_map_group : Format = sequential_map_group; -def cmap_subtable_format13 : Repr platform_id -> Format = fun platform => { +def cmap_subtable_format13 : U16 -> Format = fun platform => { _reserved <- reserved u16be 0, length <- u32be, language <- cmap_language_id32 platform, @@ -130,14 +129,14 @@ def variation_selector : Pos -> Format = fun table_start => { default_uvs_offset <- offset32 table_start default_uvs_table, non_default_uvs_offset <- offset32 table_start non_default_uvs_table, }; -def cmap_subtable_format14 : Repr platform_id -> Pos -> Format = +def cmap_subtable_format14 : U16 -> Pos -> Format = fun platform table_start => { length <- u32be, num_var_selector_records <- u32be, var_selector <- repeat_len32 num_var_selector_records (variation_selector table_start), }; def unknown_table : Format = (); -def cmap_subtable : Repr platform_id -> Format = fun platform => { +def cmap_subtable : U16 -> Format = fun platform => { table_start <- stream_pos, format <- u16be, data <- match format { diff --git a/tests/fail/elaboration/non-exhaustive-patterns/match-duplicate.snap b/tests/fail/elaboration/non-exhaustive-patterns/match-duplicate.snap index 4a84ba173..60a92a7aa 100644 --- a/tests/fail/elaboration/non-exhaustive-patterns/match-duplicate.snap +++ b/tests/fail/elaboration/non-exhaustive-patterns/match-duplicate.snap @@ -1,11 +1,5 @@ stdout = '' stderr = ''' -warning: unreachable pattern - ┌─ tests/fail/elaboration/non-exhaustive-patterns/match-duplicate.fathom:5:3 - │ -5 │ true => 2 - │ ^^^^ - error: non-exhaustive patterns in match expression ┌─ tests/fail/elaboration/non-exhaustive-patterns/match-duplicate.fathom:3:7 │ @@ -16,4 +10,10 @@ error: non-exhaustive patterns in match expression 6 │ │ } : U32 │ ╰─' in match expression +warning: unreachable pattern + ┌─ tests/fail/elaboration/non-exhaustive-patterns/match-duplicate.fathom:5:3 + │ +5 │ true => 2 + │ ^^^^ + ''' diff --git a/tests/fail/elaboration/unification/mismatch/match-equation-body-exprs.snap b/tests/fail/elaboration/unification/mismatch/match-equation-body-exprs.snap index e408c537b..4cfd3c47f 100644 --- a/tests/fail/elaboration/unification/mismatch/match-equation-body-exprs.snap +++ b/tests/fail/elaboration/unification/mismatch/match-equation-body-exprs.snap @@ -6,12 +6,6 @@ error: cannot find `x` in scope 3 │ match (x : U8) { │ ^ unbound name -warning: unreachable pattern - ┌─ tests/fail/elaboration/unification/mismatch/match-equation-body-exprs.fathom:5:5 - │ -5 │ _ => 4 : U64, - │ ^ - error: mismatched types ┌─ tests/fail/elaboration/unification/mismatch/match-equation-body-exprs.fathom:5:10 │ @@ -21,12 +15,6 @@ error: mismatched types = expected `U32` found `U64` -warning: unreachable pattern - ┌─ tests/fail/elaboration/unification/mismatch/match-equation-body-exprs.fathom:6:5 - │ -6 │ _ => Type, - │ ^ - error: mismatched types ┌─ tests/fail/elaboration/unification/mismatch/match-equation-body-exprs.fathom:6:10 │ @@ -36,4 +24,16 @@ error: mismatched types = expected `U32` found `Type` +warning: unreachable pattern + ┌─ tests/fail/elaboration/unification/mismatch/match-equation-body-exprs.fathom:5:5 + │ +5 │ _ => 4 : U64, + │ ^ + +warning: unreachable pattern + ┌─ tests/fail/elaboration/unification/mismatch/match-equation-body-exprs.fathom:6:5 + │ +6 │ _ => Type, + │ ^ + ''' diff --git a/tests/succeed/equality.snap b/tests/succeed/equality.snap index 9ab405c21..beb271a72 100644 --- a/tests/succeed/equality.snap +++ b/tests/succeed/equality.snap @@ -2,40 +2,51 @@ stdout = ''' let id : fun (A : Type) -> A -> A = fun A a => a; let Eq : fun (A : Type) -> A -> A -> Type = fun A a0 a1 => fun (P : A -> Type) -> P a0 -> P a1; -let refl : fun (A : Type) (a : A) -> Eq A a a = fun A a P => id (P a); -let fun_eta_left : fun (f : Type -> Type) -> Eq (Type -> -Type) f (fun x => f x) = fun f => refl (Type -> Type) f; -let fun_eta_right : fun (f : Type -> Type) -> Eq (Type -> -Type) (fun x => f x) f = fun f => refl (Type -> Type) f; -let fun_eta_left : fun (f : Type -> Type -> Type) -> Eq (Type -> Type -> -Type) f (fun x => f x) = fun f => refl (Type -> Type -> Type) f; -let fun_eta_right : fun (f : Type -> Type -> Type) -> Eq (Type -> Type -> -Type) (fun x => f x) f = fun f => refl (Type -> Type -> Type) f; -let fun_eta_left : fun (f : Type -> Type -> Type) -> Eq (Type -> Type -> -Type) f (fun x y => f x y) = fun f => refl (Type -> Type -> Type) f; -let fun_eta_right : fun (f : Type -> Type -> Type) -> Eq (Type -> Type -> -Type) (fun x y => f x y) f = fun f => refl (Type -> Type -> Type) f; -let fun_eta_left : fun (f : Type -> Type -> Type) -> Eq (Type -> Type -> -Type) (fun x => f x) (fun x y => f x y) = fun f => refl (Type -> Type -> +let refl : fun (A : Type) (a : A) (P : A -> Type) -> P a -> P a = +fun A a P => id (P a); +let fun_eta_left : fun (f : Type -> Type) (P : (Type -> Type) -> Type) -> P f -> +P (fun x => f x) = fun f => refl (Type -> Type) f; +let fun_eta_right : fun (f : Type -> Type) (P : (Type -> Type) -> Type) -> +P (fun x => f x) -> P f = fun f => refl (Type -> Type) f; +let fun_eta_left : fun (f : Type -> Type -> Type) (P : (Type -> Type -> Type) -> +Type) -> P f -> P (fun x => f x) = fun f => refl (Type -> Type -> Type) f; +let fun_eta_right : fun (f : Type -> Type -> Type) (P : (Type -> Type -> Type) +-> Type) -> P (fun x => f x) -> P f = fun f => refl (Type -> Type -> Type) f; +let fun_eta_left : fun (f : Type -> Type -> Type) (P : (Type -> Type -> Type) -> +Type) -> P f -> P (fun x y => f x y) = fun f => refl (Type -> Type -> Type) f; +let fun_eta_right : fun (f : Type -> Type -> Type) (P : (Type -> Type -> Type) +-> Type) -> P (fun x y => f x y) -> P f = fun f => refl (Type -> Type -> Type) f; -let fun_eta_right : fun (f : Type -> Type -> Type) -> Eq (Type -> Type -> -Type) (fun x y => f x y) (fun x => f x) = fun f => refl (Type -> Type -> -Type) f; -let record_eta_left : fun (r : { x : Type, y : Type }) -> Eq { +let fun_eta_left : fun (f : Type -> Type -> Type) (P : (Type -> Type -> Type) -> +Type) -> P (fun x => f x) -> P (fun x y => f x y) = fun f => refl (Type -> Type +-> Type) f; +let fun_eta_right : fun (f : Type -> Type -> Type) (P : (Type -> Type -> Type) +-> Type) -> P (fun x y => f x y) -> P (fun x => f x) = fun f => refl (Type -> +Type -> Type) f; +let record_eta_left : fun (r : { x : Type, y : Type }) (P : { + x : Type, + y : Type, +} -> Type) -> P r -> P { x = r.x, y = r.y } = fun r => refl { + x : Type, + y : Type, +} r; +let record_eta_right : fun (r : { x : Type, y : Type }) (P : { x : Type, y : Type, -} r { x = r.x, y = r.y } = fun r => refl { x : Type, y : Type } r; -let record_eta_right : fun (r : { x : Type, y : Type }) -> Eq { +} -> Type) -> P { x = r.x, y = r.y } -> P r = fun r => refl { x : Type, y : Type, -} { x = r.x, y = r.y } r = fun r => refl { x : Type, y : Type } r; -let four_chars : Eq U32 "beng" 1650814567 = refl U32 "beng"; -let three_chars : Eq U32 "BEN " 1111838240 = refl U32 "BEN "; -let foo : U32 -> U32 = fun x => match x { 1 => 0, x => x }; -let eq_foo : Eq (U32 -> U32) foo foo = refl (U32 -> U32) (fun a => match a { +} r; +let four_chars : fun (P : U32 -> Type) -> P "beng" -> P 1650814567 = +refl U32 "beng"; +let three_chars : fun (P : U32 -> Type) -> P "BEN " -> P 1111838240 = +refl U32 "BEN "; +let foo : U32 -> U32 = fun x => match x { 1 => 0, _ => let x : U32 = x; x }; +let eq_foo : fun (P : (U32 -> U32) -> Type) -> P (fun x => match x { 1 => 0, - x => x, -}); + _ => x, +}) -> P (fun x => match x { 1 => 0, _ => x }) = refl (U32 -> +U32) (fun a => match a { 1 => 0, _ => a }); Type : Type ''' stderr = '' diff --git a/tests/succeed/format-cond/simple.snap b/tests/succeed/format-cond/simple.snap index b2cff4c88..06f086e7d 100644 --- a/tests/succeed/format-cond/simple.snap +++ b/tests/succeed/format-cond/simple.snap @@ -2,7 +2,7 @@ stdout = ''' let format : Format = { sfnt_version <- { version <- u32be | version == (0xffff : U32) }, }; -let _ : Repr format -> { sfnt_version : Repr u32be } = fun x => x; +let _ : { sfnt_version : U32 } -> { sfnt_version : U32 } = fun x => x; () : () ''' stderr = '' diff --git a/tests/succeed/format-overlap/dependent.snap b/tests/succeed/format-overlap/dependent.snap index 0f017d55c..ebfda3e75 100644 --- a/tests/succeed/format-overlap/dependent.snap +++ b/tests/succeed/format-overlap/dependent.snap @@ -8,7 +8,10 @@ let silly : Format = overlap { record0 <- record0, record1 <- record1 record0.length, }; -let _ : Repr silly -> { +let _ : { + record0 : { length : U8 }, + record1 : { _length : U8, data : Array8 record0.length U8 }, +} -> { record0 : { length : U8 }, record1 : { _length : U8, data : Array8 record0.length U8 }, } = fun silly => silly; diff --git a/tests/succeed/format-overlap/field-refinements.snap b/tests/succeed/format-overlap/field-refinements.snap index 4c883bfc5..68ff62b78 100644 --- a/tests/succeed/format-overlap/field-refinements.snap +++ b/tests/succeed/format-overlap/field-refinements.snap @@ -1,6 +1,6 @@ stdout = ''' let number : Format = overlap { u <- u32be where u >= (2 : U32), s <- s32be }; -let _ : Repr number -> { u : U32, s : S32 } = fun n => n; +let _ : { u : U32, s : S32 } -> { u : U32, s : S32 } = fun n => n; () : () ''' stderr = '' diff --git a/tests/succeed/format-overlap/numbers.snap b/tests/succeed/format-overlap/numbers.snap index 2c0e3d9de..bdcefeeb4 100644 --- a/tests/succeed/format-overlap/numbers.snap +++ b/tests/succeed/format-overlap/numbers.snap @@ -1,6 +1,6 @@ stdout = ''' let number : Format = overlap { u <- u32be, s <- s32be }; -let _ : Repr number -> { u : U32, s : S32 } = fun n => n; +let _ : { u : U32, s : S32 } -> { u : U32, s : S32 } = fun n => n; () : () ''' stderr = '' diff --git a/tests/succeed/format-record/computed-fields.snap b/tests/succeed/format-record/computed-fields.snap index fdf12baa8..f3d1214d6 100644 --- a/tests/succeed/format-record/computed-fields.snap +++ b/tests/succeed/format-record/computed-fields.snap @@ -5,14 +5,19 @@ let format : Format = { start_code <- repeat_len16 seg_count u16be, id_delta <- repeat_len16 seg_count s16be, }; -let _ : Repr format -> { +let _ : { + seg_count_x2 : U16, + seg_count : U16, + start_code : Array16 seg_count U16, + id_delta : Array16 seg_count S16, +} -> { seg_count_x2 : U16, seg_count : U16, start_code : Array16 seg_count U16, id_delta : Array16 seg_count S16, } = fun x => x; let format : Format = { let x : U32 = 256 }; -let _ : Repr format -> { x : U32 } = fun x => x; +let _ : { x : U32 } -> { x : U32 } = fun x => x; () : () ''' stderr = '' diff --git a/tests/succeed/format-record/field-refinements.snap b/tests/succeed/format-record/field-refinements.snap index e53127fb2..c5044bd07 100644 --- a/tests/succeed/format-record/field-refinements.snap +++ b/tests/succeed/format-record/field-refinements.snap @@ -4,8 +4,11 @@ let format : Format = { len <- u8 where len <= (16 : U8), data <- repeat_len8 len u8, }; -let _ : Repr format -> { magic : U64, len : U8, data : Array8 len U8 } = -fun x => x; +let _ : { magic : U64, len : U8, data : Array8 len U8 } -> { + magic : U64, + len : U8, + data : Array8 len U8, +} = fun x => x; () : () ''' stderr = '' diff --git a/tests/succeed/format-repr/coercions.snap b/tests/succeed/format-repr/coercions.snap index 13608b9e2..1e4aa769b 100644 --- a/tests/succeed/format-repr/coercions.snap +++ b/tests/succeed/format-repr/coercions.snap @@ -1,6 +1,6 @@ stdout = ''' let num : Format = s32be; -let x : Repr num = 3; +let x : S32 = 3; let Point : Type = { x : Repr num, y : Repr num }; x : S32 ''' diff --git a/tests/succeed/format-repr/pair-dependent.snap b/tests/succeed/format-repr/pair-dependent.snap index 50345c9f8..b6e141461 100644 --- a/tests/succeed/format-repr/pair-dependent.snap +++ b/tests/succeed/format-repr/pair-dependent.snap @@ -1,7 +1,8 @@ stdout = ''' let repeat_len32 : U32 -> Format -> Format = fun len Elem => Elem; let pair : Format = { len <- u32be, data <- repeat_len32 len u32be }; -let test_pair : Repr pair -> { len : U32, data : U32 } = fun p => p; +let test_pair : { len : U32, data : U32 } -> { len : U32, data : U32 } = +fun p => p; pair : Format ''' stderr = '' diff --git a/tests/succeed/format-repr/primitives.snap b/tests/succeed/format-repr/primitives.snap index 27f7d8e68..7e0ac32a4 100644 --- a/tests/succeed/format-repr/primitives.snap +++ b/tests/succeed/format-repr/primitives.snap @@ -1,49 +1,42 @@ stdout = ''' -let test_u8_repr : Repr u8 -> U8 = fun x => x; -let test_u16be_repr : Repr u16be -> U16 = fun x => x; -let test_u16le_repr : Repr u16le -> U16 = fun x => x; -let test_u32be_repr : Repr u32be -> U32 = fun x => x; -let test_u32le_repr : Repr u32le -> U32 = fun x => x; -let test_u64be_repr : Repr u64be -> U64 = fun x => x; -let test_u64le_repr : Repr u64le -> U64 = fun x => x; -let test_s8_repr : Repr s8 -> S8 = fun x => x; -let test_s16be_repr : Repr s16be -> S16 = fun x => x; -let test_s16le_repr : Repr s16le -> S16 = fun x => x; -let test_s32be_repr : Repr s32be -> S32 = fun x => x; -let test_s32le_repr : Repr s32le -> S32 = fun x => x; -let test_s64be_repr : Repr s64be -> S64 = fun x => x; -let test_s64le_repr : Repr s64le -> S64 = fun x => x; -let test_f32be_repr : Repr f32be -> F32 = fun x => x; -let test_f32le_repr : Repr f32le -> F32 = fun x => x; -let test_f64be_repr : Repr f64be -> F64 = fun x => x; -let test_f64le_repr : Repr f64le -> F64 = fun x => x; -let test_repeat_len8 : fun (n : U8) (f : Format) -> Repr (repeat_len8 n f) -> +let test_u8_repr : U8 -> U8 = fun x => x; +let test_u16be_repr : U16 -> U16 = fun x => x; +let test_u16le_repr : U16 -> U16 = fun x => x; +let test_u32be_repr : U32 -> U32 = fun x => x; +let test_u32le_repr : U32 -> U32 = fun x => x; +let test_u64be_repr : U64 -> U64 = fun x => x; +let test_u64le_repr : U64 -> U64 = fun x => x; +let test_s8_repr : S8 -> S8 = fun x => x; +let test_s16be_repr : S16 -> S16 = fun x => x; +let test_s16le_repr : S16 -> S16 = fun x => x; +let test_s32be_repr : S32 -> S32 = fun x => x; +let test_s32le_repr : S32 -> S32 = fun x => x; +let test_s64be_repr : S64 -> S64 = fun x => x; +let test_s64le_repr : S64 -> S64 = fun x => x; +let test_f32be_repr : F32 -> F32 = fun x => x; +let test_f32le_repr : F32 -> F32 = fun x => x; +let test_f64be_repr : F64 -> F64 = fun x => x; +let test_f64le_repr : F64 -> F64 = fun x => x; +let test_repeat_len8 : fun (n : U8) (f : Format) -> Array8 n (Repr f) -> Array8 n (Repr f) = fun _ _ x => x; -let test_repeat_len16 : fun (n : U16) (f : Format) -> Repr (repeat_len16 n f) -> +let test_repeat_len16 : fun (n : U16) (f : Format) -> Array16 n (Repr f) -> Array16 n (Repr f) = fun _ _ x => x; -let test_repeat_len32 : fun (n : U32) (f : Format) -> Repr (repeat_len32 n f) -> +let test_repeat_len32 : fun (n : U32) (f : Format) -> Array32 n (Repr f) -> Array32 n (Repr f) = fun _ _ x => x; -let test_repeat_len64 : fun (n : U64) (f : Format) -> Repr (repeat_len64 n f) -> +let test_repeat_len64 : fun (n : U64) (f : Format) -> Array64 n (Repr f) -> Array64 n (Repr f) = fun _ _ x => x; -let test_repeat_until_end : fun (f : Format) -> Repr (repeat_until_end f) -> +let test_repeat_until_end : fun (f : Format) -> Array (Repr f) -> Array (Repr f) = fun _ x => x; -let test_limit8 : fun (n : U8) (f : Format) -> Repr (limit8 n f) -> Repr f = -fun _ _ x => x; -let test_limit16 : fun (n : U16) (f : Format) -> Repr (limit16 n f) -> Repr f = -fun _ _ x => x; -let test_limit32 : fun (n : U32) (f : Format) -> Repr (limit32 n f) -> Repr f = -fun _ _ x => x; -let test_limit64 : fun (n : U64) (f : Format) -> Repr (limit64 n f) -> Repr f = -fun _ _ x => x; -let test_link : fun (pos : Pos) (f : Format) -> Repr (link pos f) -> Ref f = -fun _ _ x => x; -let test_deref : fun (f : Format) (ref : Ref f) -> Repr (deref @f ref) -> -Repr f = fun _ _ x => x; -let test_stream_pos : Repr stream_pos -> Pos = fun x => x; -let test_succeed : Repr (succeed @S32 42) -> S32 = fun x => x; -let test_fail : Repr fail -> Void = fun x => x; -let test_unwrap : fun (A : Type) (opt_a : Option A) -> Repr (unwrap @A opt_a) -> -A = fun _ _ x => x; +let test_limit8 : U8 -> fun (f : Format) -> Repr f -> Repr f = fun _ _ x => x; +let test_limit16 : U16 -> fun (f : Format) -> Repr f -> Repr f = fun _ _ x => x; +let test_limit32 : U32 -> fun (f : Format) -> Repr f -> Repr f = fun _ _ x => x; +let test_limit64 : U64 -> fun (f : Format) -> Repr f -> Repr f = fun _ _ x => x; +let test_link : Pos -> fun (f : Format) -> Ref f -> Ref f = fun _ _ x => x; +let test_deref : fun (f : Format) -> Ref f -> Repr f -> Repr f = fun _ _ x => x; +let test_stream_pos : Pos -> Pos = fun x => x; +let test_succeed : S32 -> S32 = fun x => x; +let test_fail : Void -> Void = fun x => x; +let test_unwrap : fun (A : Type) -> Option A -> A -> A = fun _ _ x => x; Type : Type ''' stderr = '' diff --git a/tests/succeed/format-repr/record.snap b/tests/succeed/format-repr/record.snap index f86b823cc..a42873ae9 100644 --- a/tests/succeed/format-repr/record.snap +++ b/tests/succeed/format-repr/record.snap @@ -1,10 +1,9 @@ stdout = ''' let pair : Format = { fst <- u32be, snd <- u32be }; -let test_pair : Repr pair -> { fst : U32, snd : U32 } = fun p => p; -let test_pair : Repr pair -> { fst : U32, snd : U32 } = fun p => { - fst = p.fst, - snd = p.snd, -}; +let test_pair : { fst : U32, snd : U32 } -> { fst : U32, snd : U32 } = +fun p => p; +let test_pair : { fst : U32, snd : U32 } -> { fst : U32, snd : U32 } = +fun p => { fst = p.fst, snd = p.snd }; pair : Format ''' stderr = '' diff --git a/tests/succeed/format-repr/unit-literal.snap b/tests/succeed/format-repr/unit-literal.snap index da0d2f6d4..2d9a5b128 100644 --- a/tests/succeed/format-repr/unit-literal.snap +++ b/tests/succeed/format-repr/unit-literal.snap @@ -1,7 +1,7 @@ stdout = ''' let unit : Format = (); -let test_unit : Repr unit -> () = fun p => p; -let test_unit : Repr unit -> () = fun p => (); +let test_unit : () -> () = fun p => p; +let test_unit : () -> () = fun p => (); unit : Format ''' stderr = '' diff --git a/tests/succeed/let/id-type.snap b/tests/succeed/let/id-type.snap index c40f34eee..f3d1277b2 100644 --- a/tests/succeed/let/id-type.snap +++ b/tests/succeed/let/id-type.snap @@ -1,6 +1,6 @@ stdout = ''' let Id : Type -> Type = fun A => A; -let test_id : fun (A : Type) -> Id A -> A = fun A a => a; +let test_id : fun (A : Type) -> A -> A = fun A a => a; Type : Type ''' stderr = '' diff --git a/tests/succeed/match/check-const-1.snap b/tests/succeed/match/check-const-1.snap index ec77653c8..fde5f8fa6 100644 --- a/tests/succeed/match/check-const-1.snap +++ b/tests/succeed/match/check-const-1.snap @@ -1,4 +1,4 @@ stdout = ''' -let x : U8 = 3; match x { 1 => 0, x => x } : U8 +let x : U8 = 3; match x { 1 => 0, _ => let x : U8 = x; x } : U8 ''' stderr = '' diff --git a/tests/succeed/match/check-const-2.snap b/tests/succeed/match/check-const-2.snap index 2023e6468..650e2da7b 100644 --- a/tests/succeed/match/check-const-2.snap +++ b/tests/succeed/match/check-const-2.snap @@ -1,4 +1,4 @@ stdout = ''' -let x : U8 = 3; match x { 1 => 0, 3 => 7, x => x } : U8 +let x : U8 = 3; match x { 1 => 0, 3 => 7, _ => let x : U8 = x; x } : U8 ''' stderr = '' diff --git a/tests/succeed/match/check-const-bool.snap b/tests/succeed/match/check-const-bool.snap index 7699f35d0..664e70ebf 100644 --- a/tests/succeed/match/check-const-bool.snap +++ b/tests/succeed/match/check-const-bool.snap @@ -1,4 +1,4 @@ stdout = ''' -let x : Bool = false; if x then 1 else 0 : U8 +let x : Bool = false; if x then let x : Bool = x; 1 else 0 : U8 ''' stderr = '' diff --git a/tests/succeed/match/check-const-redundant.snap b/tests/succeed/match/check-const-redundant.snap index c1ccc9013..25eac0227 100644 --- a/tests/succeed/match/check-const-redundant.snap +++ b/tests/succeed/match/check-const-redundant.snap @@ -1,5 +1,6 @@ stdout = ''' -let x : U8 = 3; match x { 1 => 0, 3 => 7, x => x } : U8 +let x : U8 = 3; +match x { 1 => 0, 3 => 7, 5 => let x : U8 = x; x, _ => let x : U8 = x; x } : U8 ''' stderr = ''' warning: unreachable pattern diff --git a/tests/succeed/match/synth-const-1.snap b/tests/succeed/match/synth-const-1.snap index 098d6b2df..be7ce6364 100644 --- a/tests/succeed/match/synth-const-1.snap +++ b/tests/succeed/match/synth-const-1.snap @@ -1,4 +1,4 @@ stdout = ''' -let x : U8 = 3; match x { 1 => x, x => x } : U8 +let x : U8 = 3; match x { 1 => x, _ => let x : U8 = x; x } : U8 ''' stderr = '' diff --git a/tests/succeed/match/synth-const-2.snap b/tests/succeed/match/synth-const-2.snap index 38aaac02b..8b4114854 100644 --- a/tests/succeed/match/synth-const-2.snap +++ b/tests/succeed/match/synth-const-2.snap @@ -1,4 +1,4 @@ stdout = ''' -let x : U8 = 3; match x { 1 => x, 3 => x, x => x } : U8 +let x : U8 = 3; match x { 1 => x, 3 => x, _ => let x : U8 = x; x } : U8 ''' stderr = '' diff --git a/tests/succeed/prelude.snap b/tests/succeed/prelude.snap index 0775b8d3b..d43b7e6c8 100644 --- a/tests/succeed/prelude.snap +++ b/tests/succeed/prelude.snap @@ -4,48 +4,82 @@ let always : fun (A : Type) (B : Type) -> A -> B -> A = fun _ _ a _ => a; let compose : fun (A : Type) (B : Type) (C : Type) -> (A -> B) -> (B -> C) -> A -> C = fun _ _ _ ab bc a => bc (ab a); let Nat : Type = fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat; -let zero : Nat = fun Nat succ zero => zero; -let succ : Nat -> Nat = fun prev Nat succ zero => succ (prev Nat succ zero); -let add : Nat -> Nat -> Nat = -fun n0 n1 Nat succ zero => n0 Nat succ (n1 Nat succ zero); -let mul : Nat -> Nat -> Nat = -fun n0 n1 Nat succ zero => n0 Nat (n1 Nat succ) zero; +let zero : fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat = +fun Nat succ zero => zero; +let succ : (fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat) -> fun (Nat : +Type) -> (Nat -> Nat) -> Nat -> Nat = +fun prev Nat succ zero => succ (prev Nat succ zero); +let add : (fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat) -> (fun (Nat : +Type) -> (Nat -> Nat) -> Nat -> Nat) -> fun (Nat : Type) -> (Nat -> Nat) -> Nat +-> Nat = fun n0 n1 Nat succ zero => n0 Nat succ (n1 Nat succ zero); +let mul : (fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat) -> (fun (Nat : +Type) -> (Nat -> Nat) -> Nat -> Nat) -> fun (Nat : Type) -> (Nat -> Nat) -> Nat +-> Nat = fun n0 n1 Nat succ zero => n0 Nat (n1 Nat succ) zero; let List : Type -> Type = fun Elem => fun (List : Type) -> List -> (Elem -> List -> List) -> List; -let nil : fun (Elem : Type) -> List Elem = fun Elem List nil cons => nil; -let cons : fun (Elem : Type) -> Elem -> List Elem -> List Elem = -fun Elem head tail List nil cons => cons head (tail List nil cons); -let Vec : Type -> Nat -> Type = fun Elem len => fun (Vec : Nat -> Type) -> -Vec zero -> (fun (len : fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat) -> Elem --> Vec len -> Vec (succ len)) -> Vec len; -let vnil : fun (Elem : Type) -> Vec Elem zero = fun Elem Vec nil cons => nil; +let nil : fun (Elem : Type) (List : Type) -> List -> (Elem -> List -> List) -> +List = fun Elem List nil cons => nil; +let cons : fun (Elem : Type) -> Elem -> (fun (List : Type) -> List -> (Elem -> +List -> List) -> List) -> fun (List : Type) -> List -> (Elem -> List -> List) -> +List = fun Elem head tail List nil cons => cons head (tail List nil cons); +let Vec : Type -> (fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat) -> Type = +fun Elem len => fun (Vec : (fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat) -> +Type) -> Vec (fun Nat succ zero => zero) -> (fun (len : fun (Nat : Type) -> (Nat +-> Nat) -> Nat -> Nat) -> Elem -> Vec len -> +Vec (fun Nat succ zero => succ (len Nat succ zero))) -> Vec len; +let vnil : fun (Elem : Type) (Vec : (fun (Nat : Type) -> (Nat -> Nat) -> Nat -> +Nat) -> Type) -> Vec (fun Nat succ zero => zero) -> (fun (len : fun (Nat : +Type) -> (Nat -> Nat) -> Nat -> Nat) -> Elem -> Vec len -> +Vec (fun Nat succ zero => succ (len Nat succ zero))) -> +Vec (fun Nat succ zero => zero) = fun Elem Vec nil cons => nil; let vcons : fun (Elem : Type) (len : fun (Nat : Type) -> (Nat -> Nat) -> Nat -> -Nat) -> Elem -> Vec Elem len -> Vec Elem (succ len) = +Nat) -> Elem -> (fun (Vec : (fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat) -> +Type) -> Vec (fun Nat succ zero => zero) -> (fun (len : fun (Nat : Type) -> (Nat +-> Nat) -> Nat -> Nat) -> Elem -> Vec len -> +Vec (fun Nat succ zero => succ (len Nat succ zero))) -> Vec len) -> fun (Vec : +(fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat) -> Type) -> +Vec (fun Nat succ zero => zero) -> (fun (len : fun (Nat : Type) -> (Nat -> Nat) +-> Nat -> Nat) -> Elem -> Vec len -> +Vec (fun Nat succ zero => succ (len Nat succ zero))) -> +Vec (fun Nat succ zero => succ (len Nat succ zero)) = fun Elem len head tail Vec nil cons => cons len head (tail Vec nil cons); let Void : Type = fun (Void : Type) -> Void; -let absurd : fun (A : Type) -> Void -> A = fun A void => void A; +let absurd : fun (A : Type) -> (fun (Void : Type) -> Void) -> A = +fun A void => void A; let Unit : Type = fun (Unit : Type) -> Unit -> Unit; -let unit : Unit = fun Unit unit => unit; +let unit : fun (Unit : Type) -> Unit -> Unit = fun Unit unit => unit; let Eq : fun (A : Type) -> A -> A -> Type = fun A a0 a1 => fun (P : A -> Type) -> P a0 -> P a1; -let refl : fun (A : Type) (a : A) -> Eq A a a = fun A a P => id (P a); -let trans : fun (A : Type) (a0 : A) (a1 : A) (a2 : A) -> Eq A a0 a1 -> -Eq A a1 a2 -> Eq A a0 a2 = +let refl : fun (A : Type) (a : A) (P : A -> Type) -> P a -> P a = +fun A a P => id (P a); +let trans : fun (A : Type) (a0 : A) (a1 : A) (a2 : A) -> (fun (P : A -> Type) -> +P a0 -> P a1) -> (fun (P : A -> Type) -> P a1 -> P a2) -> fun (P : A -> Type) -> +P a0 -> P a2 = fun _ a0 a1 a2 p0 p1 P => compose (P a0) (P a1) (P a2) (p0 P) (p1 P); -let sym : fun (A : Type) (a0 : A) (a1 : A) -> Eq A a0 a1 -> Eq A a1 a0 = +let sym : fun (A : Type) (a0 : A) (a1 : A) -> (fun (P : A -> Type) -> P a0 -> +P a1) -> fun (P : A -> Type) -> P a1 -> P a0 = fun a a0 a1 p => p (fun a1 => Eq a a1 a0) (refl a a0); let id_apply_type : Type = (fun a => a) Type; -let list1 : List Bool = cons Bool (id Bool true) (nil Bool); -let five : Nat = succ (succ (succ (succ (succ zero)))); -let ten : Nat = add five five; -let hundred : Nat = mul ten ten; -let thousand : Nat = mul ten hundred; -let eq_test : Eq (fun (Nat : Type) -> (Nat -> Nat) -> Nat -> -Nat) hundred hundred = refl (fun (Nat : Type) -> (Nat -> Nat) -> Nat -> +let list1 : fun (List : Type) -> List -> (Bool -> List -> List) -> List = +cons Bool (id Bool true) (nil Bool); +let five : fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat = +succ (succ (succ (succ (succ zero)))); +let ten : fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat = add five five; +let hundred : fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat = mul ten ten; +let thousand : fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat = mul ten hundred; +let eq_test : fun (P : (fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat) -> +Type) -> +P (fun Nat succ zero => succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) +-> +P (fun Nat succ zero => succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) = +refl (fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat) (fun _ a b => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))); -let eq_id_apply_type : Eq Type ((fun a => a) Type) Type = refl Type Type; -let eq_id_apply_true : Eq Bool ((fun a => a) true) true = refl Bool true; -let eq_id_apply_false : Eq Bool ((fun a => a) false) false = refl Bool false; +let eq_id_apply_type : fun (P : Type -> Type) -> P Type -> P Type = +refl Type Type; +let eq_id_apply_true : fun (P : Bool -> Type) -> P true -> P true = +refl Bool true; +let eq_id_apply_false : fun (P : Bool -> Type) -> P false -> P false = +refl Bool false; Type : Type ''' stderr = '' diff --git a/tests/succeed/primitive-ops.snap b/tests/succeed/primitive-ops.snap index d1994c908..dc585f955 100644 --- a/tests/succeed/primitive-ops.snap +++ b/tests/succeed/primitive-ops.snap @@ -1,12 +1,12 @@ stdout = ''' -let test : Array8 ((1 : U8) + (2 : U8)) () -> Array8 3 () = fun x => x; -let test : Array16 ((1 : U16) + (2 : U16)) () -> Array16 3 () = fun x => x; -let test : Array32 ((1 : U32) + (2 : U32)) () -> Array32 3 () = fun x => x; -let test : Array64 ((1 : U64) + (2 : U64)) () -> Array64 3 () = fun x => x; -let test : Array8 ((3 : U8) - (1 : U8)) () -> Array8 2 () = fun x => x; -let test : Array16 ((3 : U16) - (1 : U16)) () -> Array16 2 () = fun x => x; -let test : Array32 ((3 : U32) - (1 : U32)) () -> Array32 2 () = fun x => x; -let test : Array64 ((3 : U64) - (1 : U64)) () -> Array64 2 () = fun x => x; +let test : Array8 3 () -> Array8 3 () = fun x => x; +let test : Array16 3 () -> Array16 3 () = fun x => x; +let test : Array32 3 () -> Array32 3 () = fun x => x; +let test : Array64 3 () -> Array64 3 () = fun x => x; +let test : Array8 2 () -> Array8 2 () = fun x => x; +let test : Array16 2 () -> Array16 2 () = fun x => x; +let test : Array32 2 () -> Array32 2 () = fun x => x; +let test : Array64 2 () -> Array64 2 () = fun x => x; Type : Type ''' stderr = '' diff --git a/tests/succeed/record-patterns/fun-type-generic-pair.fathom b/tests/succeed/record-patterns/fun-type-generic-pair.fathom new file mode 100644 index 000000000..b1dba36ee --- /dev/null +++ b/tests/succeed/record-patterns/fun-type-generic-pair.fathom @@ -0,0 +1,3 @@ +let FstType = fun ((A, B) : (Type, Type)) ((a, b) : (A, B)) -> A; +let SndType = fun ((A, B) : (Type, Type)) ((a, b) : (A, B)) -> B; +{} diff --git a/tests/succeed/record-patterns/fun-type-generic-pair.snap b/tests/succeed/record-patterns/fun-type-generic-pair.snap new file mode 100644 index 000000000..459b38818 --- /dev/null +++ b/tests/succeed/record-patterns/fun-type-generic-pair.snap @@ -0,0 +1,14 @@ +stdout = ''' +let FstType : Type = fun (a : (Type, Type)) -> (let A : Type = a._0; +let B : Type = a._1; +fun (b : (a._0, a._1)) -> (let a : a._0 = b._0; +let b : a._1 = b._1; +A)); +let SndType : Type = fun (a : (Type, Type)) -> (let A : Type = a._0; +let B : Type = a._1; +fun (b : (a._0, a._1)) -> (let a : a._0 = b._0; +let b : a._1 = b._1; +B)); +() : () +''' +stderr = '' diff --git a/tests/succeed/record-patterns/let-check.fathom b/tests/succeed/record-patterns/let-check.fathom new file mode 100644 index 000000000..6dc5f7354 --- /dev/null +++ b/tests/succeed/record-patterns/let-check.fathom @@ -0,0 +1,9 @@ +let () : () = (); +let _ : () = (); + +let (x, y) : (Bool, Bool) = (false, true); +let (a, _) : (Bool, Bool) = (false, true); +let (_, b) : (Bool, Bool) = (false, true); +let (_, _) : (Bool, Bool) = (false, true); +let _ : (Bool, Bool) = (false, true); +{} diff --git a/tests/succeed/record-patterns/let-check.snap b/tests/succeed/record-patterns/let-check.snap new file mode 100644 index 000000000..7256df5cb --- /dev/null +++ b/tests/succeed/record-patterns/let-check.snap @@ -0,0 +1,15 @@ +stdout = ''' +let _ : () = (); +let _ : () = (); +let a : (Bool, Bool) = (false, true); +let x : Bool = a._0; +let y : Bool = a._1; +let b : (Bool, Bool) = (false, true); +let a : Bool = b._0; +let c : (Bool, Bool) = (false, true); +let b : Bool = c._1; +let _ : (Bool, Bool) = (false, true); +let _ : (Bool, Bool) = (false, true); +() : () +''' +stderr = '' diff --git a/tests/succeed/record-patterns/let-generic-pair.fathom b/tests/succeed/record-patterns/let-generic-pair.fathom new file mode 100644 index 000000000..9317e7f4c --- /dev/null +++ b/tests/succeed/record-patterns/let-generic-pair.fathom @@ -0,0 +1,3 @@ +let fst = fun (A : Type) (B : Type) (p : (A, B)) => let (x, _) = p; x; +let snd = fun (A : Type) (B : Type) (p : (A, B)) => let (_, y) = p; y; +{} diff --git a/tests/succeed/record-patterns/let-generic-pair.snap b/tests/succeed/record-patterns/let-generic-pair.snap new file mode 100644 index 000000000..e9468fb1f --- /dev/null +++ b/tests/succeed/record-patterns/let-generic-pair.snap @@ -0,0 +1,10 @@ +stdout = ''' +let fst : fun (A : Type) (B : Type) -> (A, B) -> A = fun A B p => let x : A = +p._0; +x; +let snd : fun (A : Type) (B : Type) -> (A, B) -> B = fun A B p => let y : B = +p._1; +y; +() : () +''' +stderr = '' diff --git a/tests/succeed/record-patterns/let-synth.fathom b/tests/succeed/record-patterns/let-synth.fathom new file mode 100644 index 000000000..7e94184df --- /dev/null +++ b/tests/succeed/record-patterns/let-synth.fathom @@ -0,0 +1,9 @@ +let () = (); +let _ = (); + +let (x, y) = (false, true); +let (a, _) = (false, true); +let (_, b) = (false, true); +let (_, _) = (false, true); +let _ = (false, true); +{} diff --git a/tests/succeed/record-patterns/let-synth.snap b/tests/succeed/record-patterns/let-synth.snap new file mode 100644 index 000000000..7256df5cb --- /dev/null +++ b/tests/succeed/record-patterns/let-synth.snap @@ -0,0 +1,15 @@ +stdout = ''' +let _ : () = (); +let _ : () = (); +let a : (Bool, Bool) = (false, true); +let x : Bool = a._0; +let y : Bool = a._1; +let b : (Bool, Bool) = (false, true); +let a : Bool = b._0; +let c : (Bool, Bool) = (false, true); +let b : Bool = c._1; +let _ : (Bool, Bool) = (false, true); +let _ : (Bool, Bool) = (false, true); +() : () +''' +stderr = '' diff --git a/tests/succeed/record-patterns/match-bool-pairs.fathom b/tests/succeed/record-patterns/match-bool-pairs.fathom new file mode 100644 index 000000000..59947a7cc --- /dev/null +++ b/tests/succeed/record-patterns/match-bool-pairs.fathom @@ -0,0 +1,56 @@ +let and1 : Bool -> Bool -> Bool += fun x y => match (x, y) { + (true, true) => true, + _ => false, +}; +let and2 : Bool -> Bool -> Bool += fun x y => match (x, y) { + (true, true) => true, + (_, _) => false, +}; +let and3 : Bool -> Bool -> Bool += fun x y => match (x, y) { + (true, true) => true, + (false, true) => false, + (true, false) => false, + (false, false) => false, +}; + +let or1 : Bool -> Bool -> Bool += fun x y => match (x, y) { + (false, false) => false, + _ => true, +}; +let or2 : Bool -> Bool -> Bool += fun x y => match (x, y) { + (false, false) => false, + (_, _) => true, +}; +let or3 : Bool -> Bool -> Bool += fun x y => match (x, y) { + (false, false) => false, + (false, true) => true, + (true, false) => true, + (true, true) => true, +}; + +let xor1 : Bool -> Bool -> Bool += fun x y => match (x, y) { + (true, false) => true, + (false, true) => true, + _ => false, +}; +let xor2 : Bool -> Bool -> Bool += fun x y => match (x, y) { + (true, false) => true, + (false, true) => true, + (_, _) => false, +}; +let xor3 : Bool -> Bool -> Bool += fun x y => match (x, y) { + (true, false) => true, + (false, true) => true, + (false, false) => false, + (true, true) => false, +}; +{} diff --git a/tests/succeed/record-patterns/match-bool-pairs.snap b/tests/succeed/record-patterns/match-bool-pairs.snap new file mode 100644 index 000000000..7cadddac3 --- /dev/null +++ b/tests/succeed/record-patterns/match-bool-pairs.snap @@ -0,0 +1,22 @@ +stdout = ''' +let and1 : Bool -> Bool -> Bool = fun x y => let a : (Bool, Bool) = (x, y); +if a._0 then if a._1 then true else false else false; +let and2 : Bool -> Bool -> Bool = fun x y => let a : (Bool, Bool) = (x, y); +if a._0 then if a._1 then true else false else false; +let and3 : Bool -> Bool -> Bool = fun x y => let a : (Bool, Bool) = (x, y); +if a._0 then if a._1 then true else false else if a._1 then false else false; +let or1 : Bool -> Bool -> Bool = fun x y => let a : (Bool, Bool) = (x, y); +if a._0 then true else if a._1 then true else false; +let or2 : Bool -> Bool -> Bool = fun x y => let a : (Bool, Bool) = (x, y); +if a._0 then true else if a._1 then true else false; +let or3 : Bool -> Bool -> Bool = fun x y => let a : (Bool, Bool) = (x, y); +if a._0 then if a._1 then true else true else if a._1 then true else false; +let xor1 : Bool -> Bool -> Bool = fun x y => let a : (Bool, Bool) = (x, y); +if a._0 then if a._1 then false else true else if a._1 then true else false; +let xor2 : Bool -> Bool -> Bool = fun x y => let a : (Bool, Bool) = (x, y); +if a._0 then if a._1 then false else true else if a._1 then true else false; +let xor3 : Bool -> Bool -> Bool = fun x y => let a : (Bool, Bool) = (x, y); +if a._0 then if a._1 then false else true else if a._1 then true else false; +() : () +''' +stderr = '' diff --git a/tests/succeed/record-patterns/match-generic-pair.fathom b/tests/succeed/record-patterns/match-generic-pair.fathom new file mode 100644 index 000000000..3b5786e05 --- /dev/null +++ b/tests/succeed/record-patterns/match-generic-pair.fathom @@ -0,0 +1,3 @@ +let fst = fun (A : Type) (B : Type) (p : (A, B)) => match p { (x, _) => x }; +let snd = fun (A : Type) (B : Type) (p : (A, B)) => match p { (_, y) => y }; +{} diff --git a/tests/succeed/record-patterns/match-generic-pair.snap b/tests/succeed/record-patterns/match-generic-pair.snap new file mode 100644 index 000000000..e9468fb1f --- /dev/null +++ b/tests/succeed/record-patterns/match-generic-pair.snap @@ -0,0 +1,10 @@ +stdout = ''' +let fst : fun (A : Type) (B : Type) -> (A, B) -> A = fun A B p => let x : A = +p._0; +x; +let snd : fun (A : Type) (B : Type) -> (A, B) -> B = fun A B p => let y : B = +p._1; +y; +() : () +''' +stderr = '' diff --git a/tests/succeed/record-patterns/match-int-pairs.fathom b/tests/succeed/record-patterns/match-int-pairs.fathom new file mode 100644 index 000000000..76f708193 --- /dev/null +++ b/tests/succeed/record-patterns/match-int-pairs.fathom @@ -0,0 +1,11 @@ +let f : U32 -> U32 -> U32 += fun x y => +let p = (x, y); +match p { + (0, a) => a + (1 : U32), + (b, 0) => b + (2 : U32), + (1, c) => c + (3 : U32), + (d, 1) => d + (4 : U32), + (_, _) => (5 : U32), +}; +{} diff --git a/tests/succeed/record-patterns/match-int-pairs.snap b/tests/succeed/record-patterns/match-int-pairs.snap new file mode 100644 index 000000000..ab622529d --- /dev/null +++ b/tests/succeed/record-patterns/match-int-pairs.snap @@ -0,0 +1,24 @@ +stdout = ''' +let f : U32 -> U32 -> U32 = fun x y => let p : (U32, U32) = (x, y); +match p._0 { + 0 => let a : U32 = p._1; + a + (1 : U32), + 1 => match p._1 { + 0 => let b : U32 = p._0; + b + (2 : U32), + 1 => let c : U32 = p._1; + c + (3 : U32), + _ => let c : U32 = p._1; + c + (3 : U32), + }, + _ => match p._1 { + 0 => let b : U32 = p._0; + b + (2 : U32), + 1 => let d : U32 = p._0; + d + (4 : U32), + _ => 5, + }, +}; +() : () +''' +stderr = '' diff --git a/tests/succeed/record-patterns/synth-fun-lit-generic-pair.fathom b/tests/succeed/record-patterns/synth-fun-lit-generic-pair.fathom new file mode 100644 index 000000000..9b9b15e2e --- /dev/null +++ b/tests/succeed/record-patterns/synth-fun-lit-generic-pair.fathom @@ -0,0 +1 @@ +fun ((A, B) : (Type, Type)) ((x, y) : (A, B)) => x diff --git a/tests/succeed/record-patterns/synth-fun-lit-generic-pair.snap b/tests/succeed/record-patterns/synth-fun-lit-generic-pair.snap new file mode 100644 index 000000000..bcf52284e --- /dev/null +++ b/tests/succeed/record-patterns/synth-fun-lit-generic-pair.snap @@ -0,0 +1,8 @@ +stdout = ''' +fun a => let A : Type = a._0; +let B : Type = a._1; +fun b => let x : a._0 = b._0; +let y : a._1 = b._1; +x : fun (a : (Type, Type)) -> (a._0, a._1) -> a._0 +''' +stderr = '' diff --git a/tests/succeed/record-type/generic-point.snap b/tests/succeed/record-type/generic-point.snap index cf67a8938..49749aedc 100644 --- a/tests/succeed/record-type/generic-point.snap +++ b/tests/succeed/record-type/generic-point.snap @@ -1,6 +1,7 @@ stdout = ''' let Point : Type -> Type = fun A => { x : A, y : A }; -let test_point : fun (A : Type) -> Point A -> { x : A, y : A } = fun A p => p; +let test_point : fun (A : Type) -> { x : A, y : A } -> { x : A, y : A } = +fun A p => p; Type : Type ''' stderr = '' diff --git a/tests/succeed/record-type/generic-singleton.snap b/tests/succeed/record-type/generic-singleton.snap index df5327e5f..bba362493 100644 --- a/tests/succeed/record-type/generic-singleton.snap +++ b/tests/succeed/record-type/generic-singleton.snap @@ -1,6 +1,6 @@ stdout = ''' let Singleton : Type -> Type = fun A => { x : A }; -let test_point : fun (A : Type) -> Singleton A -> { x : A } = fun A p => p; +let test_point : fun (A : Type) -> { x : A } -> { x : A } = fun A p => p; Type : Type ''' stderr = '' diff --git a/tests/succeed/stress.snap b/tests/succeed/stress.snap index 303161fb1..84c877ded 100644 --- a/tests/succeed/stress.snap +++ b/tests/succeed/stress.snap @@ -68,12 +68,17 @@ Type) -> A -> A) id (fun (A : Type) -> A -> A) id (fun (A : Type) -> A -> A) id (fun (A : Type) -> A -> A) id (fun (A : Type) -> A -> A) id (fun (A : Type) -> A -> A) id; let Nat : Type = fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat; -let zero : Nat = fun Nat succ zero => zero; -let succ : Nat -> Nat = fun prev Nat succ zero => succ (prev Nat succ zero); -let add : Nat -> Nat -> Nat = -fun n0 n1 Nat succ zero => n0 Nat succ (n1 Nat succ zero); -let mul : Nat -> Nat -> Nat = -fun n0 n1 Nat succ zero => n0 Nat (n1 Nat succ) zero; +let zero : fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat = +fun Nat succ zero => zero; +let succ : (fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat) -> fun (Nat : +Type) -> (Nat -> Nat) -> Nat -> Nat = +fun prev Nat succ zero => succ (prev Nat succ zero); +let add : (fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat) -> (fun (Nat : +Type) -> (Nat -> Nat) -> Nat -> Nat) -> fun (Nat : Type) -> (Nat -> Nat) -> Nat +-> Nat = fun n0 n1 Nat succ zero => n0 Nat succ (n1 Nat succ zero); +let mul : (fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat) -> (fun (Nat : +Type) -> (Nat -> Nat) -> Nat -> Nat) -> fun (Nat : Type) -> (Nat -> Nat) -> Nat +-> Nat = fun n0 n1 Nat succ zero => n0 Nat (n1 Nat succ) zero; let n0 : fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat = zero; let n1 : fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat = succ n0; let n2 : fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat = succ n1; @@ -87,12 +92,26 @@ let n9 : fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat = succ n8; let n10 : fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat = succ n9; let n3000 : fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat = mul n10 (mul n10 (mul n10 n3)); -let Vec : Type -> Nat -> Type = fun Elem len => fun (Vec : Nat -> Type) -> -Vec zero -> (fun (len : fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat) -> Elem --> Vec len -> Vec (succ len)) -> Vec len; -let vnil : fun (Elem : Type) -> Vec Elem zero = fun Elem Vec nil cons => nil; +let Vec : Type -> (fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat) -> Type = +fun Elem len => fun (Vec : (fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat) -> +Type) -> Vec (fun Nat succ zero => zero) -> (fun (len : fun (Nat : Type) -> (Nat +-> Nat) -> Nat -> Nat) -> Elem -> Vec len -> +Vec (fun Nat succ zero => succ (len Nat succ zero))) -> Vec len; +let vnil : fun (Elem : Type) (Vec : (fun (Nat : Type) -> (Nat -> Nat) -> Nat -> +Nat) -> Type) -> Vec (fun Nat succ zero => zero) -> (fun (len : fun (Nat : +Type) -> (Nat -> Nat) -> Nat -> Nat) -> Elem -> Vec len -> +Vec (fun Nat succ zero => succ (len Nat succ zero))) -> +Vec (fun Nat succ zero => zero) = fun Elem Vec nil cons => nil; let vcons : fun (Elem : Type) (len : fun (Nat : Type) -> (Nat -> Nat) -> Nat -> -Nat) -> Elem -> Vec Elem len -> Vec Elem (succ len) = +Nat) -> Elem -> (fun (Vec : (fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat) -> +Type) -> Vec (fun Nat succ zero => zero) -> (fun (len : fun (Nat : Type) -> (Nat +-> Nat) -> Nat -> Nat) -> Elem -> Vec len -> +Vec (fun Nat succ zero => succ (len Nat succ zero))) -> Vec len) -> fun (Vec : +(fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat) -> Type) -> +Vec (fun Nat succ zero => zero) -> (fun (len : fun (Nat : Type) -> (Nat -> Nat) +-> Nat -> Nat) -> Elem -> Vec len -> +Vec (fun Nat succ zero => succ (len Nat succ zero))) -> +Vec (fun Nat succ zero => succ (len Nat succ zero)) = fun Elem len head tail Vec nil cons => cons len head (tail Vec nil cons); let vec1 : fun (Vec : (fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat) -> Type) -> Vec (fun Nat succ zero => zero) -> (fun (len : fun (Nat : Type) -> (Nat diff --git a/tests/succeed/tuple/check-term.snap b/tests/succeed/tuple/check-term.snap index c2ecc8ef3..28e27c989 100644 --- a/tests/succeed/tuple/check-term.snap +++ b/tests/succeed/tuple/check-term.snap @@ -2,9 +2,9 @@ stdout = ''' let Triple : Type = (U16, U16, U16); let Point : Type = { x : U16, y : U16, z : U16 }; let Any : Type = { A : Type, a : A }; -let triple : Triple = (0, 1, 2); -let point : Point = { x = 0, y = 1, z = 2 }; -let any : Any = { A = Bool, a = false }; +let triple : (U16, U16, U16) = (0, 1, 2); +let point : { x : U16, y : U16, z : U16 } = { x = 0, y = 1, z = 2 }; +let any : { A : Type, a : A } = { A = Bool, a = false }; () : () ''' stderr = ''