Skip to content

Commit cff2b4c

Browse files
brendanzabbrendanzab
committed
Switch to an explicitly typed core language
1 parent 289c397 commit cff2b4c

File tree

84 files changed

+1096
-1020
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

84 files changed

+1096
-1020
lines changed

‎fathom/src/core.rs

+26-25
Original file line numberDiff line numberDiff line change
@@ -140,15 +140,12 @@ pub enum Term<'arena> {
140140
// - https://lib.rs/crates/smallbitvec
141141
// - https://lib.rs/crates/bit-vec
142142
InsertedMeta(Span, Level, &'arena [LocalInfo]),
143-
/// Annotated expressions.
144-
Ann(Span, &'arena Term<'arena>, &'arena Term<'arena>),
145143
/// Let expressions.
146144
Let(
147145
Span,
148146
Option<StringId>,
149147
&'arena Term<'arena>,
150148
&'arena Term<'arena>,
151-
&'arena Term<'arena>,
152149
),
153150

154151
/// The type of types.
@@ -167,7 +164,13 @@ pub enum Term<'arena> {
167164
/// Function literals.
168165
///
169166
/// Also known as: lambda expressions, anonymous functions.
170-
FunLit(Span, Plicity, Option<StringId>, &'arena Term<'arena>),
167+
FunLit(
168+
Span,
169+
Plicity,
170+
Option<StringId>,
171+
&'arena Term<'arena>,
172+
&'arena Term<'arena>,
173+
),
171174
/// Function applications.
172175
FunApp(Span, Plicity, &'arena Term<'arena>, &'arena Term<'arena>),
173176

@@ -208,26 +211,25 @@ impl<'arena> Term<'arena> {
208211
/// Get the source span of the term.
209212
pub fn span(&self) -> Span {
210213
match self {
211-
Term::ItemVar(span, _)
212-
| Term::LocalVar(span, _)
213-
| Term::MetaVar(span, _)
214-
| Term::InsertedMeta(span, _, _)
215-
| Term::Ann(span, _, _)
216-
| Term::Let(span, _, _, _, _)
214+
Term::ItemVar(span, ..)
215+
| Term::LocalVar(span, ..)
216+
| Term::MetaVar(span, ..)
217+
| Term::InsertedMeta(span, ..)
218+
| Term::Let(span, ..)
217219
| Term::Universe(span)
218220
| Term::FunType(span, ..)
219221
| Term::FunLit(span, ..)
220222
| Term::FunApp(span, ..)
221-
| Term::RecordType(span, _, _)
222-
| Term::RecordLit(span, _, _)
223-
| Term::RecordProj(span, _, _)
223+
| Term::RecordType(span, ..)
224+
| Term::RecordLit(span, ..)
225+
| Term::RecordProj(span, ..)
224226
| Term::ArrayLit(span, _)
225-
| Term::FormatRecord(span, _, _)
226-
| Term::FormatCond(span, _, _, _)
227-
| Term::FormatOverlap(span, _, _)
228-
| Term::Prim(span, _)
229-
| Term::ConstLit(span, _)
230-
| Term::ConstMatch(span, _, _, _) => *span,
227+
| Term::FormatRecord(span, ..)
228+
| Term::FormatCond(span, ..)
229+
| Term::FormatOverlap(span, ..)
230+
| Term::Prim(span, ..)
231+
| Term::ConstLit(span, ..)
232+
| Term::ConstMatch(span, ..) => *span,
231233
}
232234
}
233235

@@ -242,16 +244,15 @@ impl<'arena> Term<'arena> {
242244
| Term::Prim(_, _)
243245
| Term::ConstLit(_, _) => false,
244246

245-
Term::Ann(_, expr, r#type) => expr.binds_local(var) || r#type.binds_local(var),
246-
Term::Let(_, _, def_type, def_expr, body_expr) => {
247-
def_type.binds_local(var)
248-
|| def_expr.binds_local(var)
249-
|| body_expr.binds_local(var.prev())
247+
Term::Let(_, _, def_expr, body_expr) => {
248+
def_expr.binds_local(var) || body_expr.binds_local(var.prev())
250249
}
251250
Term::FunType(.., param_type, body_type) => {
252251
param_type.binds_local(var) || body_type.binds_local(var.prev())
253252
}
254-
Term::FunLit(.., body_expr) => body_expr.binds_local(var.prev()),
253+
Term::FunLit(.., param_type, body_expr) => {
254+
param_type.binds_local(var) || body_expr.binds_local(var.prev())
255+
}
255256
Term::FunApp(.., head_expr, arg_expr) => {
256257
head_expr.binds_local(var) || arg_expr.binds_local(var)
257258
}

‎fathom/src/core/pretty.rs

+20-21
Original file line numberDiff line numberDiff line change
@@ -137,26 +137,13 @@ impl<'interner, 'arena> Context<'interner> {
137137
Term::InsertedMeta(_, level, info) => {
138138
RcDoc::text(format!("InsertedMeta({level:?}, {info:?})"))
139139
}
140-
Term::Ann(_, expr, r#type) => self.paren(
141-
prec > Prec::Top,
142-
RcDoc::concat([
143-
RcDoc::concat([
144-
self.term_prec(Prec::Let, expr),
145-
RcDoc::space(),
146-
RcDoc::text(":"),
147-
])
148-
.group(),
149-
RcDoc::softline(),
150-
self.term_prec(Prec::Top, r#type),
151-
]),
152-
),
153-
Term::Let(_, def_pattern, def_type, def_expr, body_expr) => self.paren(
140+
Term::Let(_, def_pattern, def_expr, body_expr) => self.paren(
154141
prec > Prec::Let,
155142
RcDoc::concat([
156143
RcDoc::concat([
157144
RcDoc::text("let"),
158145
RcDoc::space(),
159-
self.ann_pattern(Prec::Top, *def_pattern, def_type),
146+
self.pattern(*def_pattern),
160147
RcDoc::space(),
161148
RcDoc::text("="),
162149
RcDoc::softline(),
@@ -201,17 +188,29 @@ impl<'interner, 'arena> Context<'interner> {
201188
self.term_prec(Prec::Fun, body_type),
202189
]),
203190
),
204-
Term::FunLit(_, plicity, param_name, body_expr) => self.paren(
191+
Term::FunLit(_, plicity, param_name, param_type, body_expr) => self.paren(
205192
prec > Prec::Fun,
206193
RcDoc::concat([
207194
RcDoc::concat([
208195
RcDoc::text("fun"),
209196
RcDoc::space(),
210-
self.plicity(*plicity),
211-
match param_name {
212-
Some(name) => self.string_id(*name),
213-
None => RcDoc::text("_"),
214-
},
197+
self.paren(
198+
prec > Prec::Top,
199+
RcDoc::concat([
200+
RcDoc::concat([
201+
self.plicity(*plicity),
202+
match param_name {
203+
Some(name) => self.string_id(*name),
204+
None => RcDoc::text("_"),
205+
},
206+
RcDoc::space(),
207+
RcDoc::text(":"),
208+
])
209+
.group(),
210+
RcDoc::softline(),
211+
self.term_prec(Prec::Top, param_type),
212+
]),
213+
),
215214
RcDoc::space(),
216215
RcDoc::text("=>"),
217216
])

‎fathom/src/core/semantics.rs

+19-18
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,7 @@ pub enum Value<'arena> {
3030
/// Dependent function types.
3131
FunType(Plicity, Option<StringId>, ArcValue<'arena>, Closure<'arena>),
3232
/// Function literals.
33-
FunLit(Plicity, Option<StringId>, Closure<'arena>),
33+
FunLit(Plicity, Option<StringId>, ArcValue<'arena>, Closure<'arena>),
3434

3535
/// Record types.
3636
RecordType(&'arena [StringId], Telescope<'arena>),
@@ -298,8 +298,7 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> {
298298
let head_expr = self.eval(&Term::MetaVar(*span, *var));
299299
self.apply_local_infos(head_expr, local_infos)
300300
}
301-
Term::Ann(span, expr, _) => Spanned::merge(*span, self.eval(expr)),
302-
Term::Let(span, _, _, def_expr, body_expr) => {
301+
Term::Let(span, _, def_expr, body_expr) => {
303302
let def_expr = self.eval(def_expr);
304303
self.local_exprs.push(def_expr);
305304
let body_expr = self.eval(body_expr);
@@ -318,11 +317,12 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> {
318317
Closure::new(self.local_exprs.clone(), body_type),
319318
)),
320319
),
321-
Term::FunLit(span, plicity, param_name, body_expr) => Spanned::new(
320+
Term::FunLit(span, plicity, param_name, param_type, body_expr) => Spanned::new(
322321
*span,
323322
Arc::new(Value::FunLit(
324323
*plicity,
325324
*param_name,
325+
self.eval(param_type),
326326
Closure::new(self.local_exprs.clone(), body_expr),
327327
)),
328328
),
@@ -521,7 +521,7 @@ impl<'arena, 'env> ElimEnv<'arena, 'env> {
521521
) -> ArcValue<'arena> {
522522
match Arc::make_mut(&mut head_expr) {
523523
// Beta-reduction
524-
Value::FunLit(fun_plicity, _, body_expr) => {
524+
Value::FunLit(fun_plicity, _, _, body_expr) => {
525525
assert_eq!(arg_plicity, *fun_plicity, "Plicities must be equal");
526526
// FIXME: use span from head/arg exprs?
527527
self.apply_closure(body_expr, arg_expr)
@@ -722,10 +722,11 @@ impl<'in_arena, 'env> QuoteEnv<'in_arena, 'env> {
722722
scope.to_scope(self.quote(scope, param_type)),
723723
self.quote_closure(scope, body_type),
724724
),
725-
Value::FunLit(plicity, param_name, body_expr) => Term::FunLit(
725+
Value::FunLit(plicity, param_name, param_type, body_expr) => Term::FunLit(
726726
span,
727727
*plicity,
728728
*param_name,
729+
scope.to_scope(self.quote(scope, param_type)),
729730
self.quote_closure(scope, body_expr),
730731
),
731732

@@ -874,15 +875,9 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> {
874875
Term::InsertedMeta(*span, *var, infos)
875876
}
876877
},
877-
Term::Ann(span, expr, r#type) => Term::Ann(
878-
*span,
879-
scope.to_scope(self.unfold_metas(scope, expr)),
880-
scope.to_scope(self.unfold_metas(scope, r#type)),
881-
),
882-
Term::Let(span, def_name, def_type, def_expr, body_expr) => Term::Let(
878+
Term::Let(span, def_name, def_expr, body_expr) => Term::Let(
883879
*span,
884880
*def_name,
885-
scope.to_scope(self.unfold_metas(scope, def_type)),
886881
scope.to_scope(self.unfold_metas(scope, def_expr)),
887882
self.unfold_bound_metas(scope, body_expr),
888883
),
@@ -896,10 +891,11 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> {
896891
scope.to_scope(self.unfold_metas(scope, param_type)),
897892
self.unfold_bound_metas(scope, body_type),
898893
),
899-
Term::FunLit(span, plicity, param_name, body_expr) => Term::FunLit(
894+
Term::FunLit(span, plicity, param_name, param_type, body_expr) => Term::FunLit(
900895
*span,
901896
*plicity,
902897
*param_name,
898+
scope.to_scope(self.unfold_metas(scope, param_type)),
903899
self.unfold_bound_metas(scope, body_expr),
904900
),
905901

@@ -1117,13 +1113,18 @@ impl<'arena, 'env> ConversionEnv<'arena, 'env> {
11171113
&& self.is_equal(param_type0, param_type1)
11181114
&& self.is_equal_closures(body_type0, body_type1)
11191115
}
1120-
(Value::FunLit(plicity0, _, body_expr0), Value::FunLit(plicity1, _, body_expr1)) => {
1121-
plicity0 == plicity1 && self.is_equal_closures(body_expr0, body_expr1)
1116+
(
1117+
Value::FunLit(plicity0, _, param_type0, body_expr0),
1118+
Value::FunLit(plicity1, _, param_type1, body_expr1),
1119+
) => {
1120+
plicity0 == plicity1
1121+
&& self.is_equal(param_type0, param_type1)
1122+
&& self.is_equal_closures(body_expr0, body_expr1)
11221123
}
1123-
(Value::FunLit(plicity, _, body_expr), _) => {
1124+
(Value::FunLit(plicity, .., body_expr), _) => {
11241125
self.is_equal_fun_lit(*plicity, body_expr, &value1)
11251126
}
1126-
(_, Value::FunLit(plicity, _, body_expr)) => {
1127+
(_, Value::FunLit(plicity, .., body_expr)) => {
11271128
self.is_equal_fun_lit(*plicity, body_expr, &value0)
11281129
}
11291130

‎fathom/src/surface/distillation.rs

+23-34
Original file line numberDiff line numberDiff line change
@@ -276,14 +276,8 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
276276

277277
fn check_prec(&mut self, prec: Prec, core_term: &core::Term<'_>) -> Term<'arena, ()> {
278278
match core_term {
279-
core::Term::Ann(_span, expr, _) => {
280-
// Avoid adding extraneous type annotations!
281-
self.check_prec(prec, expr)
282-
}
283-
core::Term::Let(_span, def_name, def_type, def_expr, body_expr) => {
284-
let def_type = self.check_prec(Prec::Top, def_type);
285-
let def_expr = self.check_prec(Prec::Let, def_expr);
286-
279+
core::Term::Let(_, def_name, def_expr, body_expr) => {
280+
let def_expr = self.check_prec(Prec::Top, def_expr);
287281
let def_name = self.freshen_name(*def_name, body_expr);
288282
let def_name = self.push_local(def_name);
289283
let def_pattern = name_to_pattern(def_name);
@@ -295,29 +289,32 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
295289
Term::Let(
296290
(),
297291
def_pattern,
298-
Some(self.scope.to_scope(def_type)),
292+
None,
299293
self.scope.to_scope(def_expr),
300294
self.scope.to_scope(body_expr),
301295
),
302296
)
303297
}
304298
core::Term::FunLit(..) => {
305299
let initial_local_len = self.local_len();
300+
306301
let mut params = Vec::new();
307302
let mut body_expr = core_term;
308-
while let core::Term::FunLit(_, plicity, param_name, next_body_expr) = body_expr {
309-
let param_name = self.freshen_name(*param_name, next_body_expr);
310-
params.push((*plicity, self.push_local(param_name)));
303+
304+
while let core::Term::FunLit(_, plicity, name, r#type, next_body_expr) = body_expr {
305+
let r#type = self.check(r#type);
306+
let name = self.freshen_name(*name, next_body_expr);
307+
params.push((*plicity, self.push_local(name), r#type));
311308
body_expr = next_body_expr;
312309
}
313310

314311
let body_expr = self.check_prec(Prec::Let, body_expr);
315312
self.truncate_local(initial_local_len);
316313

317-
let params = params.into_iter().map(|(plicity, name)| Param {
314+
let params = params.into_iter().map(|(plicity, name, r#type)| Param {
318315
plicity,
319316
pattern: name_to_pattern(name),
320-
r#type: None,
317+
r#type: Some(r#type),
321318
});
322319

323320
self.paren(
@@ -492,30 +489,20 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
492489
self.paren(prec > Prec::App, Term::App((), head_expr, args.into()))
493490
}
494491
}
495-
core::Term::Ann(_span, expr, r#type) => {
496-
let expr = self.check_prec(Prec::Let, expr);
497-
let r#type = self.check_prec(Prec::Top, r#type);
498-
499-
self.paren(
500-
prec > Prec::Top,
501-
Term::Ann((), self.scope.to_scope(expr), self.scope.to_scope(r#type)),
502-
)
503-
}
504-
core::Term::Let(_span, def_name, def_type, def_expr, body_expr) => {
505-
let def_type = self.check_prec(Prec::Top, def_type);
506-
let def_expr = self.check_prec(Prec::Let, def_expr);
507-
492+
core::Term::Let(_, def_name, def_expr, body_expr) => {
493+
let def_expr = self.check_prec(Prec::Top, def_expr);
508494
let def_name = self.freshen_name(*def_name, body_expr);
509495
let def_name = self.push_local(def_name);
496+
let def_pattern = name_to_pattern(def_name);
510497
let body_expr = self.synth_prec(Prec::Let, body_expr);
511498
self.pop_local();
512499

513500
self.paren(
514501
prec > Prec::Let,
515502
Term::Let(
516503
(),
517-
name_to_pattern(def_name),
518-
Some(self.scope.to_scope(def_type)),
504+
def_pattern,
505+
None,
519506
self.scope.to_scope(def_expr),
520507
self.scope.to_scope(body_expr),
521508
),
@@ -581,22 +568,24 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
581568
}
582569
core::Term::FunLit(..) => {
583570
let initial_local_len = self.local_len();
571+
584572
let mut params = Vec::new();
585573
let mut body_expr = core_term;
586574

587-
while let core::Term::FunLit(_, plicity, param_name, next_body_expr) = body_expr {
588-
let param_name = self.freshen_name(*param_name, next_body_expr);
589-
params.push((*plicity, self.push_local(param_name)));
575+
while let core::Term::FunLit(_, plicity, name, r#type, next_body_expr) = body_expr {
576+
let r#type = self.check(r#type);
577+
let name = self.freshen_name(*name, next_body_expr);
578+
params.push((*plicity, self.push_local(name), r#type));
590579
body_expr = next_body_expr;
591580
}
592581

593582
let body_expr = self.synth_prec(Prec::Let, body_expr);
594583
self.truncate_local(initial_local_len);
595584

596-
let params = params.into_iter().map(|(plicity, name)| Param {
585+
let params = params.into_iter().map(|(plicity, name, r#type)| Param {
597586
plicity,
598587
pattern: name_to_pattern(name),
599-
r#type: None,
588+
r#type: Some(r#type),
600589
});
601590

602591
self.paren(

0 commit comments

Comments
 (0)