Skip to content

Commit 88c7337

Browse files
brendanzabbrendanzab
committed
Switch to an explicitly typed core language
1 parent 8b4b9e8 commit 88c7337

File tree

83 files changed

+1088
-1011
lines changed

Some content is hidden

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

83 files changed

+1088
-1011
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

+19-26
Original file line numberDiff line numberDiff line change
@@ -245,12 +245,7 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
245245
/// Distill a core term into a surface term, in a 'checkable' context.
246246
pub fn check(&mut self, core_term: &core::Term<'_>) -> Term<'arena, ()> {
247247
match core_term {
248-
core::Term::Ann(_span, expr, _) => {
249-
// Avoid adding extraneous type annotations!
250-
self.check(expr)
251-
}
252-
core::Term::Let(_span, def_name, def_type, def_expr, body_expr) => {
253-
let def_type = self.check(def_type);
248+
core::Term::Let(_, def_name, def_expr, body_expr) => {
254249
let def_expr = self.check(def_expr);
255250

256251
let def_name = self.freshen_name(*def_name, body_expr);
@@ -261,28 +256,31 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
261256
Term::Let(
262257
(),
263258
Pattern::Name((), def_name),
264-
Some(self.scope.to_scope(def_type)),
259+
None,
265260
self.scope.to_scope(def_expr),
266261
self.scope.to_scope(body_expr),
267262
)
268263
}
269264
core::Term::FunLit(..) => {
270265
let initial_local_len = self.local_len();
266+
271267
let mut params = Vec::new();
272268
let mut body_expr = core_term;
273-
while let core::Term::FunLit(_, plicity, param_name, next_body_expr) = body_expr {
274-
let param_name = self.freshen_name(*param_name, next_body_expr);
275-
params.push((*plicity, self.push_local(param_name)));
269+
270+
while let core::Term::FunLit(_, plicity, name, r#type, next_body_expr) = body_expr {
271+
let r#type = self.check(r#type);
272+
let name = self.freshen_name(*name, next_body_expr);
273+
params.push((*plicity, self.push_local(name), r#type));
276274
body_expr = next_body_expr;
277275
}
278276

279277
let body_expr = self.check(body_expr);
280278
self.truncate_local(initial_local_len);
281279

282-
let params = params.into_iter().map(|(plicity, name)| Param {
280+
let params = params.into_iter().map(|(plicity, name, r#type)| Param {
283281
plicity,
284282
pattern: Pattern::Name((), name),
285-
r#type: None,
283+
r#type: Some(r#type),
286284
});
287285

288286
Term::FunLiteral(
@@ -442,14 +440,7 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
442440
Term::App((), head_expr, args.into())
443441
}
444442
}
445-
core::Term::Ann(_span, expr, r#type) => {
446-
let r#type = self.check(r#type);
447-
let expr = self.check(expr);
448-
449-
Term::Ann((), self.scope.to_scope(expr), self.scope.to_scope(r#type))
450-
}
451-
core::Term::Let(_span, def_name, def_type, def_expr, body_expr) => {
452-
let def_type = self.check(def_type);
443+
core::Term::Let(_, def_name, def_expr, body_expr) => {
453444
let def_expr = self.check(def_expr);
454445

455446
let def_name = self.freshen_name(*def_name, body_expr);
@@ -460,7 +451,7 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
460451
Term::Let(
461452
(),
462453
Pattern::Name((), def_name),
463-
Some(self.scope.to_scope(def_type)),
454+
None,
464455
self.scope.to_scope(def_expr),
465456
self.scope.to_scope(body_expr),
466457
)
@@ -522,22 +513,24 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
522513
}
523514
core::Term::FunLit(..) => {
524515
let initial_local_len = self.local_len();
516+
525517
let mut params = Vec::new();
526518
let mut body_expr = core_term;
527519

528-
while let core::Term::FunLit(_, plicity, param_name, next_body_expr) = body_expr {
529-
let param_name = self.freshen_name(*param_name, next_body_expr);
530-
params.push((*plicity, self.push_local(param_name)));
520+
while let core::Term::FunLit(_, plicity, name, r#type, next_body_expr) = body_expr {
521+
let r#type = self.check(r#type);
522+
let name = self.freshen_name(*name, next_body_expr);
523+
params.push((*plicity, self.push_local(name), r#type));
531524
body_expr = next_body_expr;
532525
}
533526

534527
let body_expr = self.synth(body_expr);
535528
self.truncate_local(initial_local_len);
536529

537-
let params = params.into_iter().map(|(plicity, name)| Param {
530+
let params = params.into_iter().map(|(plicity, name, r#type)| Param {
538531
plicity,
539532
pattern: Pattern::Name((), name),
540-
r#type: None,
533+
r#type: Some(r#type),
541534
});
542535

543536
Term::FunLiteral(

0 commit comments

Comments
 (0)