Skip to content

Commit de9ccea

Browse files
brendanzabbrendanzab
committed
Switch to an explicitly typed core language
1 parent 9d75e85 commit de9ccea

Some content is hidden

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

52 files changed

+694
-503
lines changed

‎fathom/src/core.rs

Lines changed: 27 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -122,8 +122,6 @@ pub enum Term<'arena> {
122122
// - https://lib.rs/crates/smallbitvec
123123
// - https://lib.rs/crates/bit-vec
124124
InsertedMeta(Span, Level, &'arena [LocalInfo]),
125-
/// Annotated expressions.
126-
Ann(Span, &'arena Term<'arena>, &'arena Term<'arena>),
127125
/// Let expressions.
128126
Let(
129127
Span,
@@ -148,7 +146,12 @@ pub enum Term<'arena> {
148146
/// Function literals.
149147
///
150148
/// Also known as: lambda expressions, anonymous functions.
151-
FunLit(Span, Option<StringId>, &'arena Term<'arena>),
149+
FunLit(
150+
Span,
151+
Option<StringId>,
152+
&'arena Term<'arena>,
153+
&'arena Term<'arena>,
154+
),
152155
/// Function applications.
153156
FunApp(Span, &'arena Term<'arena>, &'arena Term<'arena>),
154157

@@ -190,26 +193,25 @@ impl<'arena> Term<'arena> {
190193
/// Get the source span of the term.
191194
pub fn span(&self) -> Span {
192195
match self {
193-
Term::ItemVar(span, _)
194-
| Term::LocalVar(span, _)
195-
| Term::MetaVar(span, _)
196-
| Term::InsertedMeta(span, _, _)
197-
| Term::Ann(span, _, _)
198-
| Term::Let(span, _, _, _, _)
196+
Term::ItemVar(span, ..)
197+
| Term::LocalVar(span, ..)
198+
| Term::MetaVar(span, ..)
199+
| Term::InsertedMeta(span, ..)
200+
| Term::Let(span, ..)
199201
| Term::Universe(span)
200-
| Term::FunType(span, _, _, _)
201-
| Term::FunLit(span, _, _)
202-
| Term::FunApp(span, _, _)
203-
| Term::RecordType(span, _, _)
204-
| Term::RecordLit(span, _, _)
205-
| Term::RecordProj(span, _, _)
206-
| Term::ArrayLit(span, _)
207-
| Term::FormatRecord(span, _, _)
208-
| Term::FormatCond(span, _, _, _)
209-
| Term::FormatOverlap(span, _, _)
210-
| Term::Prim(span, _)
211-
| Term::ConstLit(span, _)
212-
| Term::ConstMatch(span, _, _, _) => *span,
202+
| Term::FunType(span, ..)
203+
| Term::FunLit(span, ..)
204+
| Term::FunApp(span, ..)
205+
| Term::RecordType(span, ..)
206+
| Term::RecordLit(span, ..)
207+
| Term::RecordProj(span, ..)
208+
| Term::ArrayLit(span, ..)
209+
| Term::FormatRecord(span, ..)
210+
| Term::FormatCond(span, ..)
211+
| Term::FormatOverlap(span, ..)
212+
| Term::Prim(span, ..)
213+
| Term::ConstLit(span, ..)
214+
| Term::ConstMatch(span, ..) => *span,
213215
}
214216
}
215217

@@ -224,7 +226,6 @@ impl<'arena> Term<'arena> {
224226
| Term::Prim(_, _)
225227
| Term::ConstLit(_, _) => false,
226228

227-
Term::Ann(_, expr, r#type) => expr.binds_local(var) || r#type.binds_local(var),
228229
Term::Let(_, _, def_type, def_expr, body_expr) => {
229230
def_type.binds_local(var)
230231
|| def_expr.binds_local(var)
@@ -233,7 +234,9 @@ impl<'arena> Term<'arena> {
233234
Term::FunType(_, _, param_type, body_type) => {
234235
param_type.binds_local(var) || body_type.binds_local(var.prev())
235236
}
236-
Term::FunLit(_, _, body_expr) => body_expr.binds_local(var.prev()),
237+
Term::FunLit(_, _, param_type, body_expr) => {
238+
param_type.binds_local(var) || body_expr.binds_local(var.prev())
239+
}
237240
Term::FunApp(_, head_expr, arg_expr) => {
238241
head_expr.binds_local(var) || arg_expr.binds_local(var)
239242
}

‎fathom/src/core/binary.rs

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -380,12 +380,12 @@ impl<'arena, 'data> Context<'arena, 'data> {
380380
Value::Stuck(Head::LocalVar(_), _)
381381
| Value::Stuck(Head::MetaVar(_), _)
382382
| Value::Universe
383-
| Value::FunType(_, _, _)
384-
| Value::FunLit(_, _)
385-
| Value::RecordType(_, _)
386-
| Value::RecordLit(_, _)
387-
| Value::ArrayLit(_)
388-
| Value::ConstLit(_) => Err(ReadError::InvalidFormat(format.span())),
383+
| Value::FunType(..)
384+
| Value::FunLit(..)
385+
| Value::RecordType(..)
386+
| Value::RecordLit(..)
387+
| Value::ArrayLit(..)
388+
| Value::ConstLit(..) => Err(ReadError::InvalidFormat(format.span())),
389389
}
390390
}
391391

‎fathom/src/core/semantics.rs

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

3535
/// Record types.
3636
RecordType(&'arena [StringId], Telescope<'arena>),
@@ -291,7 +291,6 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> {
291291
let head_expr = self.eval(&Term::MetaVar(*span, *var));
292292
self.apply_local_infos(head_expr, local_infos)
293293
}
294-
Term::Ann(span, expr, _) => Spanned::merge(*span, self.eval(expr)),
295294
Term::Let(span, _, _, def_expr, body_expr) => {
296295
let def_expr = self.eval(def_expr);
297296
self.local_exprs.push(def_expr);
@@ -310,10 +309,11 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> {
310309
Closure::new(self.local_exprs.clone(), body_type),
311310
)),
312311
),
313-
Term::FunLit(span, param_name, body_expr) => Spanned::new(
312+
Term::FunLit(span, param_name, param_type, body_expr) => Spanned::new(
314313
*span,
315314
Arc::new(Value::FunLit(
316315
*param_name,
316+
self.eval(param_type),
317317
Closure::new(self.local_exprs.clone(), body_expr),
318318
)),
319319
),
@@ -498,7 +498,7 @@ impl<'arena, 'env> ElimEnv<'arena, 'env> {
498498
) -> ArcValue<'arena> {
499499
match Arc::make_mut(&mut head_expr) {
500500
// Beta-reduction
501-
Value::FunLit(_, body_expr) => self.apply_closure(body_expr, arg_expr), // FIXME: use span from head/arg exprs?
501+
Value::FunLit(_, _, body_expr) => self.apply_closure(body_expr, arg_expr), // FIXME: use span from head/arg exprs?
502502
// The computation is stuck, preventing further reduction
503503
Value::Stuck(head, spine) => {
504504
spine.push(Elim::FunApp(arg_expr));
@@ -689,9 +689,12 @@ impl<'in_arena, 'env> QuoteEnv<'in_arena, 'env> {
689689
scope.to_scope(self.quote(scope, param_type)),
690690
self.quote_closure(scope, body_type),
691691
),
692-
Value::FunLit(param_name, body_expr) => {
693-
Term::FunLit(span, *param_name, self.quote_closure(scope, body_expr))
694-
}
692+
Value::FunLit(param_name, param_type, body_expr) => Term::FunLit(
693+
span,
694+
*param_name,
695+
scope.to_scope(self.quote(scope, param_type)),
696+
self.quote_closure(scope, body_expr),
697+
),
695698

696699
Value::RecordType(labels, types) => Term::RecordType(
697700
span,
@@ -842,11 +845,6 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> {
842845
None => panic_any(Error::UnboundMetaVar),
843846
}
844847
}
845-
Term::Ann(span, expr, r#type) => Term::Ann(
846-
*span,
847-
scope.to_scope(self.unfold_metas(scope, expr)),
848-
scope.to_scope(self.unfold_metas(scope, r#type)),
849-
),
850848
Term::Let(span, def_name, def_type, def_expr, body_expr) => Term::Let(
851849
*span,
852850
*def_name,
@@ -863,9 +861,10 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> {
863861
scope.to_scope(self.unfold_metas(scope, param_type)),
864862
self.unfold_bound_metas(scope, body_type),
865863
),
866-
Term::FunLit(span, param_name, body_expr) => Term::FunLit(
864+
Term::FunLit(span, param_name, param_type, body_expr) => Term::FunLit(
867865
*span,
868866
*param_name,
867+
scope.to_scope(self.unfold_metas(scope, param_type)),
869868
self.unfold_bound_metas(scope, body_expr),
870869
),
871870

@@ -1095,11 +1094,15 @@ impl<'arena, 'env> ConversionEnv<'arena, 'env> {
10951094
self.is_equal(param_type0, param_type1)
10961095
&& self.is_equal_closures(body_type0, body_type1)
10971096
}
1098-
(Value::FunLit(_, body_expr0), Value::FunLit(_, body_expr1)) => {
1099-
self.is_equal_closures(body_expr0, body_expr1)
1097+
(
1098+
Value::FunLit(_, param_type0, body_expr0),
1099+
Value::FunLit(_, param_type1, body_expr1),
1100+
) => {
1101+
self.is_equal(param_type0, param_type1)
1102+
&& self.is_equal_closures(body_expr0, body_expr1)
11001103
}
1101-
(Value::FunLit(_, body_expr), _) => self.is_equal_fun_lit(body_expr, &value1),
1102-
(_, Value::FunLit(_, body_expr)) => self.is_equal_fun_lit(body_expr, &value0),
1104+
(Value::FunLit(_, _, body_expr), _) => self.is_equal_fun_lit(body_expr, &value1),
1105+
(_, Value::FunLit(_, _, body_expr)) => self.is_equal_fun_lit(body_expr, &value0),
11031106

11041107
(Value::RecordType(labels0, types0), Value::RecordType(labels1, types1)) => {
11051108
labels0 == labels1 && self.is_equal_telescopes(types0, types1)
@@ -1275,7 +1278,7 @@ mod tests {
12751278
Value::Stuck(_, _) => {}
12761279
Value::Universe => {}
12771280
Value::FunType(_, _, _) => {}
1278-
Value::FunLit(_, _) => {}
1281+
Value::FunLit(_, _, _) => {}
12791282
Value::RecordType(_, _) => {}
12801283
Value::RecordLit(_, _) => {}
12811284
Value::ArrayLit(_) => {}

‎fathom/src/surface/distillation.rs

Lines changed: 20 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -203,10 +203,6 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
203203
/// Distill a core term into a surface term, in a 'checkable' context.
204204
pub fn check(&mut self, core_term: &core::Term<'_>) -> Term<'arena, ()> {
205205
match core_term {
206-
core::Term::Ann(_span, expr, _) => {
207-
// Avoid adding extraneous type annotations!
208-
self.check(expr)
209-
}
210206
core::Term::Let(_span, def_name, def_type, def_expr, body_expr) => {
211207
let def_type = self.check(def_type);
212208
let def_expr = self.check(def_expr);
@@ -223,20 +219,25 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
223219
self.scope.to_scope(body_expr),
224220
)
225221
}
226-
core::Term::FunLit(_, param_name, mut body_expr) => {
222+
core::Term::FunLit(..) => {
227223
let initial_local_len = self.local_len();
228-
let mut param_names = vec![self.push_local(*param_name)];
229-
while let core::Term::FunLit(_, param_name, next_body_expr) = body_expr {
230-
param_names.push(self.push_local(*param_name));
224+
let mut param_names = Vec::new();
225+
let mut body_expr = core_term;
226+
227+
while let core::Term::FunLit(_, param_name, param_type, next_body_expr) = body_expr
228+
{
229+
let param_type = self.check(param_type);
230+
param_names.push((self.push_local(*param_name), param_type));
231231
body_expr = next_body_expr;
232232
}
233233

234234
let body_expr = self.check(body_expr);
235235
self.truncate_local(initial_local_len);
236236

237-
let patterns = param_names
238-
.into_iter()
239-
.map(|name| (Pattern::Name((), name), None));
237+
let patterns = param_names.into_iter().map(|(name, r#type)| {
238+
let r#type = self.scope.to_scope(r#type) as &_;
239+
(Pattern::Name((), name), Some(r#type))
240+
});
240241

241242
Term::FunLiteral(
242243
(),
@@ -394,12 +395,6 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
394395
Term::App((), head_expr, arg_exprs.into())
395396
}
396397
}
397-
core::Term::Ann(_span, expr, r#type) => {
398-
let r#type = self.check(r#type);
399-
let expr = self.check(expr);
400-
401-
Term::Ann((), self.scope.to_scope(expr), self.scope.to_scope(r#type))
402-
}
403398
core::Term::Let(_span, def_name, def_type, def_expr, body_expr) => {
404399
let def_type = self.check(def_type);
405400
let def_expr = self.check(def_expr);
@@ -474,17 +469,20 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
474469
let mut param_names = Vec::new();
475470
let mut body_expr = core_term;
476471

477-
while let core::Term::FunLit(_, param_name, next_body_expr) = body_expr {
478-
param_names.push(self.push_local(*param_name));
472+
while let core::Term::FunLit(_, param_name, param_type, next_body_expr) = body_expr
473+
{
474+
let param_type = self.check(param_type);
475+
param_names.push((self.push_local(*param_name), param_type));
479476
body_expr = next_body_expr;
480477
}
481478

482479
let body_expr = self.synth(body_expr);
483480
self.truncate_local(initial_local_len);
484481

485-
let patterns = param_names
486-
.into_iter()
487-
.map(|name| (Pattern::Name((), name), None));
482+
let patterns = param_names.into_iter().map(|(name, r#type)| {
483+
let r#type = self.scope.to_scope(r#type) as &_;
484+
(Pattern::Name((), name), Some(r#type))
485+
});
488486

489487
Term::FunLiteral(
490488
(),

‎fathom/src/surface/elaboration.rs

Lines changed: 17 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -1239,18 +1239,11 @@ impl<'interner, 'arena> Context<'interner, 'arena> {
12391239

12401240
(expr, r#type)
12411241
}
1242-
Term::Ann(range, expr, r#type) => {
1242+
Term::Ann(_, expr, r#type) => {
12431243
let r#type = self.check(r#type, &self.universe.clone());
12441244
let type_value = self.eval_env().eval(&r#type);
1245-
let expr = self.check(expr, &type_value);
12461245

1247-
let ann_expr = core::Term::Ann(
1248-
range.into(),
1249-
self.scope.to_scope(expr),
1250-
self.scope.to_scope(r#type),
1251-
);
1252-
1253-
(ann_expr, type_value)
1246+
(self.check(expr, &type_value), type_value)
12541247
}
12551248
Term::Let(range, def_pattern, def_type, def_expr, body_expr) => {
12561249
let (def_pattern, def_type_value) = self.synth_ann_pattern(def_pattern, *def_type);
@@ -1579,17 +1572,24 @@ impl<'interner, 'arena> Context<'interner, 'arena> {
15791572
Some(((pattern, r#type), next_patterns)) => {
15801573
let body_type = self.elim_env().force(expected_type);
15811574
match body_type.as_ref() {
1582-
Value::FunType(_, param_type, next_body_type) => {
1575+
Value::FunType(_, param_type_value, next_body_type) => {
15831576
let range = ByteRange::merge(&pattern.range(), &body_expr.range()).unwrap();
1584-
let pattern = self.check_ann_pattern(pattern, *r#type, param_type);
1585-
let (name, arg_expr) = self.push_local_param(pattern, param_type.clone());
1577+
let pattern = self.check_ann_pattern(pattern, *r#type, param_type_value);
1578+
let param_type = self.quote_env().quote(self.scope, param_type_value);
1579+
let (name, arg_expr) =
1580+
self.push_local_param(pattern, param_type_value.clone());
15861581

15871582
let body_type = self.elim_env().apply_closure(next_body_type, arg_expr);
15881583
let body_expr =
15891584
self.check_fun_lit(range, next_patterns, body_expr, &body_type);
15901585
self.local_env.pop();
15911586

1592-
core::Term::FunLit(range.into(), name, self.scope.to_scope(body_expr))
1587+
core::Term::FunLit(
1588+
range.into(),
1589+
name,
1590+
self.scope.to_scope(param_type),
1591+
self.scope.to_scope(body_expr),
1592+
)
15931593
}
15941594
// Attempt to elaborate the the body of the function in synthesis
15951595
// mode if we are checking against a metavariable.
@@ -1654,13 +1654,10 @@ impl<'interner, 'arena> Context<'interner, 'arena> {
16541654

16551655
// Construct the function literal and type from the parameters in reverse
16561656
for (range, name, r#type) in params.into_iter().rev() {
1657-
fun_lit = core::Term::FunLit(range.into(), name, self.scope.to_scope(fun_lit));
1658-
fun_type = core::Term::FunType(
1659-
Span::Empty,
1660-
name,
1661-
self.scope.to_scope(r#type),
1662-
self.scope.to_scope(fun_type),
1663-
);
1657+
let r#type = self.scope.to_scope(r#type);
1658+
fun_lit = core::Term::FunLit(range.into(), name, r#type, self.scope.to_scope(fun_lit));
1659+
fun_type =
1660+
core::Term::FunType(Span::Empty, name, r#type, self.scope.to_scope(fun_type));
16641661
}
16651662

16661663
(fun_lit, self.eval_env().eval(&fun_type))

0 commit comments

Comments
 (0)