From 214edf7089642041f9da7ee14980f6a0a8805525 Mon Sep 17 00:00:00 2001 From: Karl Meakin Date: Thu, 19 Jan 2023 05:54:01 +0000 Subject: [PATCH 1/3] Parse letrec terms --- fathom/src/surface.rs | 20 ++++++++++++++++---- fathom/src/surface/distillation.rs | 12 ++++++------ fathom/src/surface/elaboration.rs | 13 +++++++------ fathom/src/surface/elaboration/order.rs | 11 ++++++----- fathom/src/surface/grammar.lalrpop | 23 +++++++++++------------ fathom/src/surface/lexer.rs | 3 +++ fathom/src/surface/pretty.rs | 19 +++++++++++++++---- 7 files changed, 64 insertions(+), 37 deletions(-) diff --git a/fathom/src/surface.rs b/fathom/src/surface.rs index 7d9e2defd..dbdc5a3c8 100644 --- a/fathom/src/surface.rs +++ b/fathom/src/surface.rs @@ -199,9 +199,13 @@ pub enum Term<'arena, Range> { /// Let expressions. Let( Range, - Pattern, - Option<&'arena Term<'arena, Range>>, + &'arena LetDef<'arena, Range>, &'arena Term<'arena, Range>, + ), + /// Letrec expressions. + Letrec( + Range, + &'arena [LetDef<'arena, Range>], &'arena Term<'arena, Range>, ), /// If expressions @@ -291,6 +295,13 @@ pub enum Term<'arena, Range> { ReportedError(Range), } +#[derive(Debug, Clone)] +pub struct LetDef<'arena, Range> { + pub pattern: Pattern, + pub r#type: Option>, + pub expr: Term<'arena, Range>, +} + impl<'arena, Range: Clone> Term<'arena, Range> { /// Get the source range of the term. pub fn range(&self) -> Range { @@ -300,7 +311,8 @@ impl<'arena, Range: Clone> Term<'arena, Range> { | Term::Hole(range, _) | Term::Placeholder(range) | Term::Ann(range, _, _) - | Term::Let(range, _, _, _, _) + | Term::Let(range, ..) + | Term::Letrec(range, ..) | Term::If(range, _, _, _) | Term::Match(range, _, _) | Term::Universe(range) @@ -530,7 +542,7 @@ mod tests { #[cfg(target_pointer_width = "64")] fn term_size() { assert_eq!(std::mem::size_of::>(), 32); - assert_eq!(std::mem::size_of::>(), 48); + assert_eq!(std::mem::size_of::>(), 40); } #[test] diff --git a/fathom/src/surface/distillation.rs b/fathom/src/surface/distillation.rs index 548c26797..fc32be8b2 100644 --- a/fathom/src/surface/distillation.rs +++ b/fathom/src/surface/distillation.rs @@ -10,9 +10,7 @@ use crate::core::{Const, Plicity, UIntStyle}; use crate::env::{self, EnvLen, Index, Level, UniqueEnv}; use crate::source::{Span, StringId, StringInterner}; use crate::surface::elaboration::MetaSource; -use crate::surface::{ - Arg, BinOp, ExprField, FormatField, Item, ItemDef, Module, Param, Pattern, Term, TypeField, -}; +use crate::surface::*; /// Term precedences #[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord)] @@ -395,9 +393,11 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> { prec > Prec::Let, Term::Let( (), - pattern, - Some(self.scope.to_scope(r#type)), - self.scope.to_scope(expr), + self.scope.to_scope(LetDef { + pattern, + r#type: Some(r#type), + expr, + }), self.scope.to_scope(body), ), ) diff --git a/fathom/src/surface/elaboration.rs b/fathom/src/surface/elaboration.rs index 799c7fbc9..1c04c8a64 100644 --- a/fathom/src/surface/elaboration.rs +++ b/fathom/src/surface/elaboration.rs @@ -1013,10 +1013,10 @@ 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), _) => { + (Term::Let(_, def, body_expr), _) => { let (def_pattern, def_type, def_type_value) = - self.synth_ann_pattern(def_pattern, *def_type); - let def_expr = self.check(def_expr, &def_type_value); + self.synth_ann_pattern(&def.pattern, def.r#type.as_ref()); + let def_expr = self.check(&def.expr, &def_type_value); let def_expr_value = self.eval_env().eval(&def_expr); let def_name = self.push_local_def(def_pattern, def_expr_value, def_type_value); // TODO: split on constants @@ -1423,10 +1423,10 @@ impl<'interner, 'arena> Context<'interner, 'arena> { (ann_expr, type_value) } - Term::Let(_, def_pattern, def_type, def_expr, body_expr) => { + Term::Let(_, def, body_expr) => { let (def_pattern, def_type, def_type_value) = - self.synth_ann_pattern(def_pattern, *def_type); - let def_expr = self.check(def_expr, &def_type_value); + self.synth_ann_pattern(&def.pattern, def.r#type.as_ref()); + let def_expr = self.check(&def.expr, &def_type_value); let def_expr_value = self.eval_env().eval(&def_expr); let def_name = self.push_local_def(def_pattern, def_expr_value, def_type_value); @@ -1443,6 +1443,7 @@ impl<'interner, 'arena> Context<'interner, 'arena> { (let_expr, body_type) } + Term::Letrec(_, _, _) => todo!(), Term::If(_, cond_expr, then_expr, else_expr) => { let cond_expr = self.check(cond_expr, &self.bool_type.clone()); let (then_expr, r#type) = self.synth(then_expr); diff --git a/fathom/src/surface/elaboration/order.rs b/fathom/src/surface/elaboration/order.rs index aa7827580..2978590e2 100644 --- a/fathom/src/surface/elaboration/order.rs +++ b/fathom/src/surface/elaboration/order.rs @@ -183,15 +183,16 @@ fn term_deps( term_deps(expr, item_names, local_names, deps); term_deps(r#type, item_names, local_names, deps); } - Term::Let(_, pattern, r#type, def_expr, body_expr) => { - push_pattern(pattern, local_names); - if let Some(r#type) = r#type { + Term::Let(_, def, body_expr) => { + push_pattern(&def.pattern, local_names); + if let Some(r#type) = def.r#type.as_ref() { term_deps(r#type, item_names, local_names, deps); } - term_deps(def_expr, item_names, local_names, deps); + term_deps(&def.expr, item_names, local_names, deps); term_deps(body_expr, item_names, local_names, deps); - pop_pattern(pattern, local_names); + pop_pattern(&def.pattern, local_names); } + Term::Letrec(_, _, _) => todo!(), Term::If(_, cond_expr, then_expr, else_expr) => { term_deps(cond_expr, item_names, local_names, deps); term_deps(then_expr, item_names, local_names, deps); diff --git a/fathom/src/surface/grammar.lalrpop b/fathom/src/surface/grammar.lalrpop index 26d35046b..01d829234 100644 --- a/fathom/src/surface/grammar.lalrpop +++ b/fathom/src/surface/grammar.lalrpop @@ -2,10 +2,7 @@ use scoped_arena::Scope; 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, -}; +use crate::surface::*; use crate::surface::lexer::{Error as LexerError, Token}; grammar<'arena, 'source>( @@ -29,6 +26,7 @@ extern { "fun" => Token::KeywordFun, "if" => Token::KeywordIf, "let" => Token::KeywordLet, + "letrec" => Token::KeywordLetrec, "match" => Token::KeywordMatch, "overlap" => Token::KeywordOverlap, "Type" => Token::KeywordType, @@ -113,20 +111,21 @@ pub Term: Term<'arena, ByteRange> = { LetTerm: Term<'arena, ByteRange> = { FunTerm, - "let" )?> "=" ";" => { - Term::Let( - ByteRange::new(start, end), - def_pattern, - def_type.map(|def_type| scope.to_scope(def_type) as &_), - scope.to_scope(def_expr), - scope.to_scope(body_expr), - ) + "let" ";" => { + Term::Let(ByteRange::new(start, end), scope.to_scope(def), scope.to_scope(body_expr)) + }, + "letrec" > ";" => { + Term::Letrec(ByteRange::new(start, end), defs, scope.to_scope(body_expr)) }, "if" "then" "else" => { Term::If(ByteRange::new(start, end), scope.to_scope(cond_expr), scope.to_scope(then_expr), scope.to_scope(else_expr)) }, }; +LetDef: LetDef<'arena, ByteRange> = { + )?> "=" => LetDef {pattern, r#type, expr}, +}; + FunTerm: Term<'arena, ByteRange> = { EqExpr, "->" => { diff --git a/fathom/src/surface/lexer.rs b/fathom/src/surface/lexer.rs index 444284092..d69082de4 100644 --- a/fathom/src/surface/lexer.rs +++ b/fathom/src/surface/lexer.rs @@ -37,6 +37,8 @@ pub enum Token<'source> { KeywordIf, #[token("let")] KeywordLet, + #[token("letrec")] + KeywordLetrec, #[token("match")] KeywordMatch, #[token("overlap")] @@ -235,6 +237,7 @@ impl<'source> Token<'source> { Token::KeywordFun => "fun", Token::KeywordIf => "if", Token::KeywordLet => "let", + Token::KeywordLetrec => "letrec", Token::KeywordMatch => "match", Token::KeywordOverlap => "overlap", Token::KeywordThen => "then", diff --git a/fathom/src/surface/pretty.rs b/fathom/src/surface/pretty.rs index 225faf085..24e66fb7d 100644 --- a/fathom/src/surface/pretty.rs +++ b/fathom/src/surface/pretty.rs @@ -5,7 +5,7 @@ use scoped_arena::Scope; use crate::source::{StringId, StringInterner}; use crate::surface::lexer::is_keyword; -use crate::surface::{Arg, FormatField, Item, Module, Param, Pattern, Plicity, Term}; +use crate::surface::{Arg, FormatField, Item, LetDef, Module, Param, Pattern, Plicity, Term}; const INDENT: isize = 4; @@ -161,21 +161,22 @@ impl<'interner, 'arena> Context<'interner, 'arena> { self.softline(), self.term(r#type), ]), - Term::Let(_, def_pattern, def_type, def_expr, body_expr) => self.concat([ + Term::Let(_, def, body_expr) => self.concat([ self.concat([ self.text("let"), self.space(), - self.ann_pattern(def_pattern, *def_type), + self.ann_pattern(&def.pattern, def.r#type.as_ref()), self.space(), self.text("="), self.softline(), - self.term(def_expr), + self.term(&def.expr), self.text(";"), ]) .group(), self.line(), self.term(body_expr), ]), + Term::Letrec(_, _, _) => todo!(), Term::If(_, cond_expr, then_expr, mut else_expr) => { let mut branches = Vec::new(); @@ -339,6 +340,16 @@ impl<'interner, 'arena> Context<'interner, 'arena> { } } + fn let_def(&'arena self, def: &LetDef<'_, Range>) -> DocBuilder<'interner, 'arena> { + self.concat([ + self.ann_pattern(&def.pattern, def.r#type.as_ref()), + self.space(), + self.text("="), + self.softline(), + self.term(&def.expr), + ]) + } + fn format_field( &'arena self, format_field: &FormatField<'_, Range>, From d2e1f7b76b89b0dfa42b716cb04d5531d4fa259c Mon Sep 17 00:00:00 2001 From: Karl Meakin Date: Thu, 19 Jan 2023 06:01:12 +0000 Subject: [PATCH 2/3] Pretty print letrec --- fathom/src/surface/pretty.rs | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/fathom/src/surface/pretty.rs b/fathom/src/surface/pretty.rs index 24e66fb7d..178a7c95b 100644 --- a/fathom/src/surface/pretty.rs +++ b/fathom/src/surface/pretty.rs @@ -165,18 +165,20 @@ impl<'interner, 'arena> Context<'interner, 'arena> { self.concat([ self.text("let"), self.space(), - self.ann_pattern(&def.pattern, def.r#type.as_ref()), - self.space(), - self.text("="), - self.softline(), - self.term(&def.expr), + self.let_def(def), self.text(";"), ]) .group(), self.line(), self.term(body_expr), ]), - Term::Letrec(_, _, _) => todo!(), + Term::Letrec(_, defs, body_expr) => self.sequence( + false, + self.text("letrec "), + defs.iter().map(|def| self.let_def(def)), + self.text(","), + self.concat([self.text(";"), self.line(), self.term(body_expr)]), + ), Term::If(_, cond_expr, then_expr, mut else_expr) => { let mut branches = Vec::new(); From 07e8de5982884ddb781c8133726d6f095001c42f Mon Sep 17 00:00:00 2001 From: Karl Meakin Date: Thu, 19 Jan 2023 06:32:45 +0000 Subject: [PATCH 3/3] Elaborate letrec terms --- fathom/src/core.rs | 37 +++++--- fathom/src/core/pretty.rs | 33 +++++-- fathom/src/core/semantics.rs | 56 ++++++++++-- fathom/src/env.rs | 4 + fathom/src/surface.rs | 9 ++ fathom/src/surface/distillation.rs | 32 ++++++- fathom/src/surface/elaboration.rs | 98 ++++++++++++++++----- fathom/src/surface/elaboration/order.rs | 18 +++- fathom/src/surface/elaboration/reporting.rs | 1 + tests/succeed/letrec/factorial.fathom | 12 +++ tests/succeed/letrec/factorial.snap | 14 +++ tests/succeed/letrec/fibonacci.fathom | 8 ++ tests/succeed/letrec/fibonacci.snap | 11 +++ tests/succeed/letrec/parity.fathom | 14 +++ tests/succeed/letrec/parity.snap | 14 +++ 15 files changed, 307 insertions(+), 54 deletions(-) create mode 100644 tests/succeed/letrec/factorial.fathom create mode 100644 tests/succeed/letrec/factorial.snap create mode 100644 tests/succeed/letrec/fibonacci.fathom create mode 100644 tests/succeed/letrec/fibonacci.snap create mode 100644 tests/succeed/letrec/parity.fathom create mode 100644 tests/succeed/letrec/parity.snap diff --git a/fathom/src/core.rs b/fathom/src/core.rs index 49f1b8622..00c48dfd7 100644 --- a/fathom/src/core.rs +++ b/fathom/src/core.rs @@ -143,13 +143,8 @@ pub enum Term<'arena> { /// Annotated expressions. Ann(Span, &'arena Term<'arena>, &'arena Term<'arena>), /// Let expressions. - Let( - Span, - Option, - &'arena Term<'arena>, - &'arena Term<'arena>, - &'arena Term<'arena>, - ), + Let(Span, &'arena LetDef<'arena>, &'arena Term<'arena>), + Letrec(Span, &'arena [LetDef<'arena>], &'arena Term<'arena>), /// The type of types. Universe(Span), @@ -204,6 +199,13 @@ pub enum Term<'arena> { ), } +#[derive(Debug, Clone)] +pub struct LetDef<'arena> { + pub name: Option, + pub r#type: Term<'arena>, + pub expr: Term<'arena>, +} + impl<'arena> Term<'arena> { /// Get the source span of the term. pub fn span(&self) -> Span { @@ -213,7 +215,8 @@ impl<'arena> Term<'arena> { | Term::MetaVar(span, _) | Term::InsertedMeta(span, _, _) | Term::Ann(span, _, _) - | Term::Let(span, _, _, _, _) + | Term::Let(span, ..) + | Term::Letrec(span, ..) | Term::Universe(span) | Term::FunType(span, ..) | Term::FunLit(span, ..) @@ -243,11 +246,23 @@ impl<'arena> Term<'arena> { | Term::ConstLit(_, _) => false, Term::Ann(_, expr, r#type) => expr.binds_local(var) || r#type.binds_local(var), - Term::Let(_, _, def_type, def_expr, body_expr) => { - def_type.binds_local(var) - || def_expr.binds_local(var) + Term::Let(_, def, body_expr) => { + def.r#type.binds_local(var) + || def.expr.binds_local(var) || body_expr.binds_local(var.prev()) } + Term::Letrec(_, defs, body_expr) => { + for _def in defs.iter() { + var = var.prev(); + } + + if (defs.iter()).any(|def| def.r#type.binds_local(var) || def.expr.binds_local(var)) + { + return true; + } + + body_expr.binds_local(var) + } Term::FunType(.., param_type, body_type) => { param_type.binds_local(var) || body_type.binds_local(var.prev()) } diff --git a/fathom/src/core/pretty.rs b/fathom/src/core/pretty.rs index 8ce508db4..5cdd24b14 100644 --- a/fathom/src/core/pretty.rs +++ b/fathom/src/core/pretty.rs @@ -30,7 +30,7 @@ use std::cell::RefCell; use pretty::RcDoc; -use crate::core::{Item, Module, Plicity, Term}; +use crate::core::{Item, LetDef, Module, Plicity, Term}; use crate::source::{StringId, StringInterner}; use crate::surface::lexer::is_keyword; @@ -150,17 +150,13 @@ impl<'interner, 'arena> Context<'interner> { self.term_prec(Prec::Top, r#type), ]), ), - Term::Let(_, def_pattern, def_type, def_expr, body_expr) => self.paren( + Term::Let(_, def, body_expr) => self.paren( prec > Prec::Let, RcDoc::concat([ RcDoc::concat([ RcDoc::text("let"), RcDoc::space(), - self.ann_pattern(Prec::Top, *def_pattern, def_type), - RcDoc::space(), - RcDoc::text("="), - RcDoc::softline(), - self.term_prec(Prec::Let, def_expr), + self.let_def(def), RcDoc::text(";"), ]) .group(), @@ -168,6 +164,19 @@ impl<'interner, 'arena> Context<'interner> { self.term_prec(Prec::Let, body_expr), ]), ), + Term::Letrec(_, defs, body_expr) => self.paren( + prec > Prec::Let, + self.sequence( + RcDoc::concat([RcDoc::text("let")]), + defs.iter().map(|def| self.let_def(def)), + RcDoc::text(","), + RcDoc::concat([ + RcDoc::text(";"), + RcDoc::line(), + self.term_prec(Prec::Let, body_expr), + ]), + ), + ), Term::Universe(_) => RcDoc::text("Type"), Term::FunType(_, plicity, param_name, param_type, body_type) => self.paren( prec > Prec::Fun, @@ -341,6 +350,16 @@ impl<'interner, 'arena> Context<'interner> { } } + fn let_def(&'arena self, def: &LetDef<'arena>) -> RcDoc { + RcDoc::concat([ + self.ann_pattern(Prec::Top, def.name, &def.r#type), + RcDoc::space(), + RcDoc::text("="), + RcDoc::softline(), + self.term_prec(Prec::Let, &def.expr), + ]) + } + fn format_field(&'arena self, label: StringId, format: &Term<'arena>) -> RcDoc { RcDoc::concat([ self.ident(label), diff --git a/fathom/src/core/semantics.rs b/fathom/src/core/semantics.rs index 8623e5aaf..560d43431 100644 --- a/fathom/src/core/semantics.rs +++ b/fathom/src/core/semantics.rs @@ -7,8 +7,8 @@ use std::sync::Arc; use scoped_arena::Scope; use crate::alloc::SliceVec; -use crate::core::{prim, Const, LocalInfo, Plicity, Prim, Term}; -use crate::env::{EnvLen, Index, Level, SharedEnv, SliceEnv}; +use crate::core::*; +use crate::env::{self, EnvLen, Index, Level, SharedEnv, SliceEnv}; use crate::source::{Span, Spanned, StringId}; /// Atomically reference counted values. We use reference counting to increase @@ -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() @@ -299,13 +301,29 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> { self.apply_local_infos(head_expr, local_infos) } Term::Ann(span, expr, _) => Spanned::merge(*span, self.eval(expr)), - Term::Let(span, _, _, def_expr, body_expr) => { - let def_expr = self.eval(def_expr); + Term::Let(span, def, body_expr) => { + let def_expr = self.eval(&def.expr); self.local_exprs.push(def_expr); let body_expr = self.eval(body_expr); self.local_exprs.pop(); Spanned::merge(*span, body_expr) } + Term::Letrec(span, defs, body_expr) => { + let initial_len = self.local_exprs.len(); + + for _def in defs.iter() { + // TODO: lazy evaluation? + (self.local_exprs).push(Spanned::empty(Arc::new(Value::ERROR))); + } + for (level, def) in Iterator::zip(env::levels(), defs.iter()) { + let def_expr = self.eval(&def.expr); + self.local_exprs.set_level(level, def_expr); + } + + let body_expr = self.eval(body_expr); + self.local_exprs.truncate(initial_len); + Spanned::merge(*span, body_expr) + } Term::Universe(span) => Spanned::new(*span, Arc::new(Value::Universe)), @@ -879,13 +897,35 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> { scope.to_scope(self.unfold_metas(scope, expr)), scope.to_scope(self.unfold_metas(scope, r#type)), ), - Term::Let(span, def_name, def_type, def_expr, body_expr) => Term::Let( + Term::Let(span, def, body_expr) => Term::Let( *span, - *def_name, - scope.to_scope(self.unfold_metas(scope, def_type)), - scope.to_scope(self.unfold_metas(scope, def_expr)), + scope.to_scope(LetDef { + name: def.name, + r#type: self.unfold_metas(scope, &def.r#type), + expr: self.unfold_metas(scope, &def.expr), + }), self.unfold_bound_metas(scope, body_expr), ), + Term::Letrec(span, defs, body_expr) => { + let initial_len = self.local_exprs.len(); + + for _def in defs.iter() { + let var = Arc::new(Value::local_var(self.local_exprs.len().next_level())); + self.local_exprs.push(Spanned::empty(var)); + } + + let defs = scope.to_scope_from_iter(defs.iter().map(|def| { + let name = def.name; + let r#type = self.unfold_metas(scope, &def.r#type); + let expr = self.unfold_metas(scope, &def.expr); + LetDef { name, r#type, expr } + })); + + let body_expr = self.unfold_metas(scope, body_expr); + self.local_exprs.truncate(initial_len); + + Term::Letrec(*span, defs, scope.to_scope(body_expr)) + } Term::Universe(span) => Term::Universe(*span), diff --git a/fathom/src/env.rs b/fathom/src/env.rs index 2f62a6032..489592c09 100644 --- a/fathom/src/env.rs +++ b/fathom/src/env.rs @@ -337,6 +337,10 @@ impl SharedEnv { self.get_level(self.len().index_to_level(index)?) } + pub fn set_level(&mut self, level: Level, entry: Entry) { + self.entries.set_mut(level.0 as usize, entry); + } + /// Push an entry onto the environment. pub fn push(&mut self, entry: Entry) { assert!(self.entries.len() < usize::from(u16::MAX)); diff --git a/fathom/src/surface.rs b/fathom/src/surface.rs index dbdc5a3c8..7537323f5 100644 --- a/fathom/src/surface.rs +++ b/fathom/src/surface.rs @@ -179,6 +179,15 @@ impl Pattern { } } +impl Pattern { + pub fn name(&self) -> Option { + match self { + Pattern::Name(_, name) => Some(*name), + _ => None, + } + } +} + /// Surface terms. #[derive(Debug, Clone)] pub enum Term<'arena, Range> { diff --git a/fathom/src/surface/distillation.rs b/fathom/src/surface/distillation.rs index fc32be8b2..3e4f7bce5 100644 --- a/fathom/src/surface/distillation.rs +++ b/fathom/src/surface/distillation.rs @@ -380,10 +380,10 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> { Term::Ann((), self.scope.to_scope(expr), self.scope.to_scope(r#type)), ) } - (core::Term::Let(_, name, r#type, expr, body), _) => { - let r#type = self.term_prec(mode, Prec::Top, r#type); - let expr = self.term_prec(mode, Prec::Let, expr); - let name = self.freshen_name(*name, body); + (core::Term::Let(_, def, body), _) => { + let r#type = self.term_prec(mode, Prec::Top, &def.r#type); + let expr = self.term_prec(mode, Prec::Let, &def.expr); + let name = self.freshen_name(def.name, body); let name = self.push_local(name); let pattern = name_to_pattern(name); let body = self.term_prec(mode, Prec::Top, body); @@ -402,6 +402,30 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> { ), ) } + (core::Term::Letrec(_, defs, body_expr), _) => { + let initial_len = self.local_len(); + + // TODO: freshen names + let def_names: Vec<_> = defs.iter().map(|def| self.push_local(def.name)).collect(); + + let defs = self.scope.to_scope_from_iter( + Iterator::zip(def_names.iter(), defs.iter()).map(|(name, def)| { + let r#type = self.check(&def.r#type); + let expr = self.check(&def.expr); + + LetDef { + pattern: name_to_pattern(*name), + r#type: Some(r#type), + expr, + } + }), + ); + + let body_expr = self.check(body_expr); + self.truncate_local(initial_len); + + Term::Letrec((), defs, self.scope.to_scope(body_expr)) + } (core::Term::Universe(_), _) => Term::Universe(()), (core::Term::FunType(..), _) => { let initial_local_len = self.local_len(); diff --git a/fathom/src/surface/elaboration.rs b/fathom/src/surface/elaboration.rs index 1c04c8a64..24ee54a89 100644 --- a/fathom/src/surface/elaboration.rs +++ b/fathom/src/surface/elaboration.rs @@ -26,7 +26,7 @@ use std::sync::Arc; use scoped_arena::Scope; -use super::ExprField; +use super::{ExprField, LetDef}; use crate::alloc::SliceVec; use crate::core::semantics::{self, ArcValue, Head, Telescope, Value}; use crate::core::{self, prim, Const, Plicity, Prim, UIntStyle}; @@ -177,6 +177,8 @@ impl<'arena> LocalEnv<'arena> { #[derive(Debug, Copy, Clone)] pub enum MetaSource { ImplicitArg(FileRange, Option), + /// The type of a letrec definition + LetrecType(FileRange, Option), /// The type of a hole. HoleType(FileRange, StringId), /// The expression of a hole. @@ -199,6 +201,7 @@ impl MetaSource { pub fn range(&self) -> FileRange { match self { MetaSource::ImplicitArg(range, _) + | MetaSource::LetrecType(range, ..) | MetaSource::HoleType(range, _) | MetaSource::HoleExpr(range, _) | MetaSource::PlaceholderType(range) @@ -1000,6 +1003,51 @@ impl<'interner, 'arena> Context<'interner, 'arena> { })) } + fn synth_let_def(&mut self, def: &LetDef<'_, ByteRange>) -> core::LetDef<'arena> { + let (def_pattern, def_type, def_type_value) = + self.synth_ann_pattern(&def.pattern, def.r#type.as_ref()); + let def_expr = self.check(&def.expr, &def_type_value); + let def_expr_value = self.eval_env().eval(&def_expr); + let def_name = self.push_local_def(def_pattern, def_expr_value, def_type_value); // TODO: split on constants + core::LetDef { + name: def_name, + r#type: def_type, + expr: def_expr, + } + } + + fn synth_letrec_defs( + &mut self, + defs: &[LetDef<'_, ByteRange>], + ) -> &'arena [core::LetDef<'arena>] { + // Insert a fresh type variable for each definition + let types: Vec<_> = (defs.iter()) + .map(|def| { + let name = def.pattern.name(); + let source = MetaSource::LetrecType(self.file_range(def.pattern.range()), name); + let r#type = self.push_unsolved_type(source); + let expr = Spanned::empty(Arc::new(Value::ERROR)); // TODO: lazy evaluation? + self.local_env.push_def(name, expr, r#type.clone()); + r#type + }) + .collect(); + + // Check each definition's pattern against its type variable + for (r#type, def) in Iterator::zip(types.iter(), defs.iter()) { + let _pattern = self.check_ann_pattern(&def.pattern, def.r#type.as_ref(), r#type); + } + + // Check each definition's rhs against its type variable + (self.scope).to_scope_from_iter(Iterator::zip(types.iter(), defs.iter()).map( + |(type_value, def)| { + let name = def.pattern.name(); + let r#type = self.quote_env().quote(self.scope, type_value); + let expr = self.check(&def.expr, type_value); + core::LetDef { name, r#type, expr } + }, + )) + } + /// Check that a surface term conforms to the given type. /// /// Returns the elaborated term in the core language. @@ -1014,23 +1062,24 @@ impl<'interner, 'arena> Context<'interner, 'arena> { match (surface_term, expected_type.as_ref()) { (Term::Paren(_, term), _) => self.check(term, &expected_type), (Term::Let(_, def, body_expr), _) => { - let (def_pattern, def_type, def_type_value) = - self.synth_ann_pattern(&def.pattern, def.r#type.as_ref()); - let def_expr = self.check(&def.expr, &def_type_value); - let def_expr_value = self.eval_env().eval(&def_expr); - - let def_name = self.push_local_def(def_pattern, def_expr_value, def_type_value); // TODO: split on constants + let def = self.synth_let_def(def); 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(def), self.scope.to_scope(body_expr), ) } + (Term::Letrec(_, defs, body_expr), _) => { + let initial_len = self.local_env.len(); + let defs = self.synth_letrec_defs(defs); + let body_expr = self.check(body_expr, &expected_type); + self.local_env.truncate(initial_len); + core::Term::Letrec(file_range.into(), defs, self.scope.to_scope(body_expr)) + } + (Term::If(_, cond_expr, then_expr, else_expr), _) => { let cond_expr = self.check(cond_expr, &self.bool_type.clone()); let then_expr = self.check(then_expr, &expected_type); @@ -1424,26 +1473,27 @@ impl<'interner, 'arena> Context<'interner, 'arena> { (ann_expr, type_value) } Term::Let(_, def, body_expr) => { - let (def_pattern, def_type, def_type_value) = - self.synth_ann_pattern(&def.pattern, def.r#type.as_ref()); - let def_expr = self.check(&def.expr, &def_type_value); - let def_expr_value = self.eval_env().eval(&def_expr); - - let def_name = self.push_local_def(def_pattern, def_expr_value, def_type_value); + let def = self.synth_let_def(def); 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(def), self.scope.to_scope(body_expr), ); (let_expr, body_type) } - Term::Letrec(_, _, _) => todo!(), + Term::Letrec(_, defs, body_expr) => { + let initial_len = self.local_env.len(); + let defs = self.synth_letrec_defs(defs); + let (body_expr, body_type) = self.synth(body_expr); + self.local_env.truncate(initial_len); + let letrec_expr = + core::Term::Letrec(file_range.into(), defs, self.scope.to_scope(body_expr)); + (letrec_expr, body_type) + } Term::If(_, cond_expr, then_expr, else_expr) => { let cond_expr = self.check(cond_expr, &self.bool_type.clone()); let (then_expr, r#type) = self.synth(then_expr); @@ -2311,9 +2361,11 @@ impl<'interner, 'arena> Context<'interner, 'arena> { 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(core::LetDef { + name: def_name, + r#type: def_type, + expr: match_info.scrutinee.expr.clone(), + }), self.scope.to_scope(body_expr), ) } diff --git a/fathom/src/surface/elaboration/order.rs b/fathom/src/surface/elaboration/order.rs index 2978590e2..864f8e4c6 100644 --- a/fathom/src/surface/elaboration/order.rs +++ b/fathom/src/surface/elaboration/order.rs @@ -192,7 +192,23 @@ fn term_deps( term_deps(body_expr, item_names, local_names, deps); pop_pattern(&def.pattern, local_names); } - Term::Letrec(_, _, _) => todo!(), + Term::Letrec(_, defs, body_expr) => { + for def in defs.iter() { + push_pattern(&def.pattern, local_names); + } + + for def in defs.iter() { + if let Some(r#type) = def.r#type.as_ref() { + term_deps(r#type, item_names, local_names, deps); + } + term_deps(&def.expr, item_names, local_names, deps); + } + + term_deps(body_expr, item_names, local_names, deps); + for def in defs.iter() { + pop_pattern(&def.pattern, local_names); + } + } Term::If(_, cond_expr, then_expr, else_expr) => { term_deps(cond_expr, item_names, local_names, deps); term_deps(then_expr, item_names, local_names, deps); diff --git a/fathom/src/surface/elaboration/reporting.rs b/fathom/src/surface/elaboration/reporting.rs index ed429af47..01f3d54d4 100644 --- a/fathom/src/surface/elaboration/reporting.rs +++ b/fathom/src/surface/elaboration/reporting.rs @@ -479,6 +479,7 @@ impl Message { Message::UnsolvedMetaVar { source } => { let (range, source_name) = match source { MetaSource::ImplicitArg(range, _) => (range, "implicit argument"), + MetaSource::LetrecType(range, _) => (range, "letrec definition"), MetaSource::HoleExpr(range, _) => (range, "hole expression"), MetaSource::PlaceholderExpr(range) => (range, "placeholder expression"), MetaSource::PlaceholderPatternType(range) => { diff --git a/tests/succeed/letrec/factorial.fathom b/tests/succeed/letrec/factorial.fathom new file mode 100644 index 000000000..5f4b0b492 --- /dev/null +++ b/tests/succeed/letrec/factorial.fathom @@ -0,0 +1,12 @@ +letrec + factorial : U32 -> U32 + = fun (x : U32) => match x { + 0 => 1, + _ => x * factorial (x - 1), + }, + factorial_iter : U32 -> U32 -> U32 + = fun (acc: U32) (x : U32) => match x { + 0 => acc, + _ => factorial_iter (acc * x) (x - 1), + }; +(factorial, factorial_iter) diff --git a/tests/succeed/letrec/factorial.snap b/tests/succeed/letrec/factorial.snap new file mode 100644 index 000000000..0ef71fe95 --- /dev/null +++ b/tests/succeed/letrec/factorial.snap @@ -0,0 +1,14 @@ +stdout = ''' +letrec + factorial : U32 -> U32 = fun x => match x { + 0 => 1, + _ => x * factorial (x - (1 : U32)), + }, + factorial_iter : U32 -> U32 -> U32 = fun acc x => match x { + 0 => acc, + _ => factorial_iter (acc * x) (x - (1 : U32)), + }, +; +(factorial, factorial_iter) : (U32 -> U32, U32 -> U32 -> U32) +''' +stderr = '' diff --git a/tests/succeed/letrec/fibonacci.fathom b/tests/succeed/letrec/fibonacci.fathom new file mode 100644 index 000000000..63d18a5ba --- /dev/null +++ b/tests/succeed/letrec/fibonacci.fathom @@ -0,0 +1,8 @@ +letrec + fibonacci : U32 -> U32 + = fun (x : U32) => match x { + 0 => 0, + 1 => 1, + _ => (fibonacci (x - 1)) + (fibonacci (x - 2)), + }; +fibonacci diff --git a/tests/succeed/letrec/fibonacci.snap b/tests/succeed/letrec/fibonacci.snap new file mode 100644 index 000000000..6690c6f87 --- /dev/null +++ b/tests/succeed/letrec/fibonacci.snap @@ -0,0 +1,11 @@ +stdout = ''' +letrec + fibonacci : U32 -> U32 = fun x => match x { + 0 => 0, + 1 => 1, + _ => fibonacci (x - (1 : U32)) + fibonacci (x - (2 : U32)), + }, +; +fibonacci : U32 -> U32 +''' +stderr = '' diff --git a/tests/succeed/letrec/parity.fathom b/tests/succeed/letrec/parity.fathom new file mode 100644 index 000000000..4682b6095 --- /dev/null +++ b/tests/succeed/letrec/parity.fathom @@ -0,0 +1,14 @@ +letrec + is_even : U32 -> Bool + = fun (x : U32) => match x { + 0 => true, + _ => is_odd (x - 1), + }, + + is_odd : U32 -> Bool + = fun (x : U32) => match x { + 0 => false, + _ => is_even (x - 1), + }, +; +(is_even, is_odd) diff --git a/tests/succeed/letrec/parity.snap b/tests/succeed/letrec/parity.snap new file mode 100644 index 000000000..edcb12866 --- /dev/null +++ b/tests/succeed/letrec/parity.snap @@ -0,0 +1,14 @@ +stdout = ''' +letrec + is_even : U32 -> Bool = fun x => match x { + 0 => true, + _ => is_odd (x - (1 : U32)), + }, + is_odd : U32 -> Bool = fun x => match x { + 0 => false, + _ => is_even (x - (1 : U32)), + }, +; +(is_even, is_odd) : (U32 -> Bool, U32 -> Bool) +''' +stderr = ''