Skip to content

Commit e007327

Browse files
KmeakinKmeakin
committed
Parse letrec terms
1 parent 289c397 commit e007327

File tree

7 files changed

+74
-53
lines changed

7 files changed

+74
-53
lines changed

‎fathom/src/surface.rs‎

Lines changed: 15 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -199,9 +199,13 @@ pub enum Term<'arena, Range> {
199199
/// Let expressions.
200200
Let(
201201
Range,
202-
Pattern<Range>,
203-
Option<&'arena Term<'arena, Range>>,
202+
&'arena LetDef<'arena, Range>,
204203
&'arena Term<'arena, Range>,
204+
),
205+
/// Letrec expressions.
206+
Letrec(
207+
Range,
208+
&'arena [LetDef<'arena, Range>],
205209
&'arena Term<'arena, Range>,
206210
),
207211
/// If expressions
@@ -291,6 +295,13 @@ pub enum Term<'arena, Range> {
291295
ReportedError(Range),
292296
}
293297

298+
#[derive(Debug, Clone)]
299+
pub struct LetDef<'arena, Range> {
300+
pub pattern: Pattern<Range>,
301+
pub r#type: Option<Term<'arena, Range>>,
302+
pub expr: Term<'arena, Range>,
303+
}
304+
294305
impl<'arena, Range: Clone> Term<'arena, Range> {
295306
/// Get the source range of the term.
296307
pub fn range(&self) -> Range {
@@ -300,7 +311,8 @@ impl<'arena, Range: Clone> Term<'arena, Range> {
300311
| Term::Hole(range, _)
301312
| Term::Placeholder(range)
302313
| Term::Ann(range, _, _)
303-
| Term::Let(range, _, _, _, _)
314+
| Term::Let(range, ..)
315+
| Term::Letrec(range, ..)
304316
| Term::If(range, _, _, _)
305317
| Term::Match(range, _, _)
306318
| Term::Universe(range)

‎fathom/src/surface/distillation.rs‎

Lines changed: 17 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -10,9 +10,7 @@ use crate::core::{Const, Plicity, UIntStyle};
1010
use crate::env::{self, EnvLen, Index, Level, UniqueEnv};
1111
use crate::source::{Span, StringId, StringInterner};
1212
use crate::surface::elaboration::MetaSource;
13-
use crate::surface::{
14-
Arg, BinOp, ExprField, FormatField, Item, ItemDef, Module, Param, Pattern, Term, TypeField,
15-
};
13+
use crate::surface::*;
1614

1715
/// Term precedences
1816
#[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord)]
@@ -286,19 +284,17 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
286284

287285
let def_name = self.freshen_name(*def_name, body_expr);
288286
let def_name = self.push_local(def_name);
289-
let def_pattern = name_to_pattern(def_name);
290287
let body_expr = self.check_prec(Prec::Let, body_expr);
291288
self.pop_local();
292289

293-
self.paren(
294-
prec > Prec::Let,
295-
Term::Let(
296-
(),
297-
def_pattern,
298-
Some(self.scope.to_scope(def_type)),
299-
self.scope.to_scope(def_expr),
300-
self.scope.to_scope(body_expr),
301-
),
290+
Term::Let(
291+
(),
292+
self.scope.to_scope(LetDef {
293+
pattern: name_to_pattern(def_name),
294+
r#type: Some(def_type),
295+
expr: def_expr,
296+
}),
297+
self.scope.to_scope(body_expr),
302298
)
303299
}
304300
core::Term::FunLit(..) => {
@@ -510,15 +506,14 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
510506
let body_expr = self.synth_prec(Prec::Let, body_expr);
511507
self.pop_local();
512508

513-
self.paren(
514-
prec > Prec::Let,
515-
Term::Let(
516-
(),
517-
name_to_pattern(def_name),
518-
Some(self.scope.to_scope(def_type)),
519-
self.scope.to_scope(def_expr),
520-
self.scope.to_scope(body_expr),
521-
),
509+
Term::Let(
510+
(),
511+
self.scope.to_scope(LetDef {
512+
pattern: name_to_pattern(def_name),
513+
r#type: Some(def_type),
514+
expr: def_expr,
515+
}),
516+
self.scope.to_scope(body_expr),
522517
)
523518
}
524519
core::Term::Universe(_span) => Term::Universe(()),

‎fathom/src/surface/elaboration.rs‎

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1012,11 +1012,10 @@ impl<'interner, 'arena> Context<'interner, 'arena> {
10121012
let expected_type = self.elim_env().force(expected_type);
10131013

10141014
match (surface_term, expected_type.as_ref()) {
1015-
(Term::Paren(_, term), _) => self.check(term, &expected_type),
1016-
(Term::Let(_, def_pattern, def_type, def_expr, body_expr), _) => {
1015+
(Term::Let(_, def, body_expr), _) => {
10171016
let (def_pattern, def_type, def_type_value) =
1018-
self.synth_ann_pattern(def_pattern, *def_type);
1019-
let def_expr = self.check(def_expr, &def_type_value);
1017+
self.synth_ann_pattern(&def.pattern, def.r#type.as_ref());
1018+
let def_expr = self.check(&def.expr, &def_type_value);
10201019
let def_expr_value = self.eval_env().eval(&def_expr);
10211020

10221021
let def_name = self.push_local_def(def_pattern, def_expr_value, def_type_value); // TODO: split on constants
@@ -1420,10 +1419,10 @@ impl<'interner, 'arena> Context<'interner, 'arena> {
14201419

14211420
(ann_expr, type_value)
14221421
}
1423-
Term::Let(_, def_pattern, def_type, def_expr, body_expr) => {
1422+
Term::Let(_, def, body_expr) => {
14241423
let (def_pattern, def_type, def_type_value) =
1425-
self.synth_ann_pattern(def_pattern, *def_type);
1426-
let def_expr = self.check(def_expr, &def_type_value);
1424+
self.synth_ann_pattern(&def.pattern, def.r#type.as_ref());
1425+
let def_expr = self.check(&def.expr, &def_type_value);
14271426
let def_expr_value = self.eval_env().eval(&def_expr);
14281427

14291428
let def_name = self.push_local_def(def_pattern, def_expr_value, def_type_value);
@@ -1440,6 +1439,7 @@ impl<'interner, 'arena> Context<'interner, 'arena> {
14401439

14411440
(let_expr, body_type)
14421441
}
1442+
Term::Letrec(_, _, _) => todo!(),
14431443
Term::If(_, cond_expr, then_expr, else_expr) => {
14441444
let cond_expr = self.check(cond_expr, &self.bool_type.clone());
14451445
let (then_expr, r#type) = self.synth(then_expr);

‎fathom/src/surface/elaboration/order.rs‎

Lines changed: 6 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -181,15 +181,16 @@ fn term_deps(
181181
term_deps(expr, item_names, local_names, deps);
182182
term_deps(r#type, item_names, local_names, deps);
183183
}
184-
Term::Let(_, pattern, r#type, def_expr, body_expr) => {
185-
push_pattern(pattern, local_names);
186-
if let Some(r#type) = r#type {
184+
Term::Let(_, def, body_expr) => {
185+
push_pattern(&def.pattern, local_names);
186+
if let Some(r#type) = def.r#type.as_ref() {
187187
term_deps(r#type, item_names, local_names, deps);
188188
}
189-
term_deps(def_expr, item_names, local_names, deps);
189+
term_deps(&def.expr, item_names, local_names, deps);
190190
term_deps(body_expr, item_names, local_names, deps);
191-
pop_pattern(pattern, local_names);
191+
pop_pattern(&def.pattern, local_names);
192192
}
193+
Term::Letrec(_, _, _) => todo!(),
193194
Term::If(_, cond_expr, then_expr, else_expr) => {
194195
term_deps(cond_expr, item_names, local_names, deps);
195196
term_deps(then_expr, item_names, local_names, deps);

‎fathom/src/surface/grammar.lalrpop‎

Lines changed: 11 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -2,10 +2,7 @@ use scoped_arena::Scope;
22
use std::cell::RefCell;
33

44
use crate::source::{ByteRange, BytePos, StringId, StringInterner};
5-
use crate::surface::{
6-
Arg, BinOp, ExprField, FormatField, Item, ItemDef, Module, ParseMessage,
7-
Pattern, Param, Plicity, Term, TypeField,
8-
};
5+
use crate::surface::*;
96
use crate::surface::lexer::{Error as LexerError, Token};
107

118
grammar<'arena, 'source>(
@@ -29,6 +26,7 @@ extern {
2926
"fun" => Token::KeywordFun,
3027
"if" => Token::KeywordIf,
3128
"let" => Token::KeywordLet,
29+
"letrec" => Token::KeywordLetrec,
3230
"match" => Token::KeywordMatch,
3331
"overlap" => Token::KeywordOverlap,
3432
"Type" => Token::KeywordType,
@@ -113,20 +111,21 @@ pub Term: Term<'arena, ByteRange> = {
113111

114112
LetTerm: Term<'arena, ByteRange> = {
115113
FunTerm,
116-
<start: @L> "let" <def_pattern: Pattern> <def_type: (":" <LetTerm>)?> "=" <def_expr: Term> ";" <body_expr: LetTerm> <end: @R> => {
117-
Term::Let(
118-
ByteRange::new(start, end),
119-
def_pattern,
120-
def_type.map(|def_type| scope.to_scope(def_type) as &_),
121-
scope.to_scope(def_expr),
122-
scope.to_scope(body_expr),
123-
)
114+
<start: @L> "let" <def: LetDef> ";" <body_expr: LetTerm> <end: @R> => {
115+
Term::Let(ByteRange::new(start, end), scope.to_scope(def), scope.to_scope(body_expr))
116+
},
117+
<start: @L> "letrec" <defs: Seq1<LetDef, ",">> ";" <body_expr: LetTerm> <end: @R> => {
118+
Term::Letrec(ByteRange::new(start, end), defs, scope.to_scope(body_expr))
124119
},
125120
<start: @L> "if" <cond_expr: FunTerm> "then" <then_expr: LetTerm> "else" <else_expr: LetTerm> <end: @R> => {
126121
Term::If(ByteRange::new(start, end), scope.to_scope(cond_expr), scope.to_scope(then_expr), scope.to_scope(else_expr))
127122
},
128123
};
129124

125+
LetDef: LetDef<'arena, ByteRange> = {
126+
<pattern: Pattern> <r#type: (":" <LetTerm>)?> "=" <expr: Term> => LetDef {pattern, r#type, expr},
127+
};
128+
130129
FunTerm: Term<'arena, ByteRange> = {
131130
EqExpr,
132131
<start: @L> <plicity: Plicity> <param_type: AppTerm> "->" <body_type: FunTerm> <end: @R> => {

‎fathom/src/surface/lexer.rs‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -37,6 +37,8 @@ pub enum Token<'source> {
3737
KeywordIf,
3838
#[token("let")]
3939
KeywordLet,
40+
#[token("letrec")]
41+
KeywordLetrec,
4042
#[token("match")]
4143
KeywordMatch,
4244
#[token("overlap")]
@@ -235,6 +237,7 @@ impl<'source> Token<'source> {
235237
Token::KeywordFun => "fun",
236238
Token::KeywordIf => "if",
237239
Token::KeywordLet => "let",
240+
Token::KeywordLetrec => "letrec",
238241
Token::KeywordMatch => "match",
239242
Token::KeywordOverlap => "overlap",
240243
Token::KeywordThen => "then",

‎fathom/src/surface/pretty.rs‎

Lines changed: 15 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ use scoped_arena::Scope;
55

66
use crate::source::{StringId, StringInterner};
77
use crate::surface::lexer::is_keyword;
8-
use crate::surface::{Arg, FormatField, Item, Module, Param, Pattern, Plicity, Term};
8+
use crate::surface::{Arg, FormatField, Item, LetDef, Module, Param, Pattern, Plicity, Term};
99

1010
const INDENT: isize = 4;
1111

@@ -156,21 +156,22 @@ impl<'interner, 'arena> Context<'interner, 'arena> {
156156
self.softline(),
157157
self.term(r#type),
158158
]),
159-
Term::Let(_, def_pattern, def_type, def_expr, body_expr) => self.concat([
159+
Term::Let(_, def, body_expr) => self.concat([
160160
self.concat([
161161
self.text("let"),
162162
self.space(),
163-
self.ann_pattern(def_pattern, *def_type),
163+
self.ann_pattern(&def.pattern, def.r#type.as_ref()),
164164
self.space(),
165165
self.text("="),
166166
self.softline(),
167-
self.term(def_expr),
167+
self.term(&def.expr),
168168
self.text(";"),
169169
])
170170
.group(),
171171
self.line(),
172172
self.term(body_expr),
173173
]),
174+
Term::Letrec(_, _, _) => todo!(),
174175
Term::If(_, cond_expr, then_expr, mut else_expr) => {
175176
let mut branches = Vec::new();
176177

@@ -346,6 +347,16 @@ impl<'interner, 'arena> Context<'interner, 'arena> {
346347
}
347348
}
348349

350+
fn let_def<Range>(&'arena self, def: &LetDef<'_, Range>) -> DocBuilder<'arena, Self> {
351+
self.concat([
352+
self.ann_pattern(&def.pattern, def.r#type.as_ref()),
353+
self.space(),
354+
self.text("="),
355+
self.softline(),
356+
self.term(&def.expr),
357+
])
358+
}
359+
349360
fn format_field<Range>(
350361
&'arena self,
351362
format_field: &FormatField<'_, Range>,

0 commit comments

Comments
 (0)