Skip to content

Commit ff2cfa4

Browse files
brendanzabbrendanzab
committed
Break the dependency between surface and core
1 parent 941aa50 commit ff2cfa4

File tree

8 files changed

+137
-129
lines changed

8 files changed

+137
-129
lines changed

‎fathom/src/surface.rs‎

Lines changed: 6 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,6 @@ use codespan_reporting::diagnostic::{Diagnostic, Label};
77
use lalrpop_util::lalrpop_mod;
88
use scoped_arena::Scope;
99

10-
use crate::core::Plicity;
1110
use crate::files::FileId;
1211
use crate::source::{BytePos, ByteRange, StringId, StringInterner};
1312

@@ -205,7 +204,6 @@ pub enum Term<'arena, Range> {
205204
/// Arrow types.
206205
Arrow(
207206
Range,
208-
Plicity,
209207
&'arena Term<'arena, Range>,
210208
&'arena Term<'arena, Range>,
211209
),
@@ -333,16 +331,15 @@ impl<'arena> Term<'arena, ByteRange> {
333331
}
334332

335333
#[derive(Debug, Clone)]
336-
pub struct Param<'arena, Range> {
337-
pub plicity: Plicity,
338-
pub pattern: Pattern<Range>,
339-
pub r#type: Option<Term<'arena, Range>>,
334+
pub enum Param<'arena, Range> {
335+
Explicit(Pattern<Range>, Option<Term<'arena, Range>>),
336+
Implicit(Pattern<Range>, Option<Term<'arena, Range>>),
340337
}
341338

342339
#[derive(Debug, Clone)]
343-
pub struct Arg<'arena, Range> {
344-
pub plicity: Plicity,
345-
pub term: Term<'arena, Range>,
340+
pub enum Arg<'arena, Range> {
341+
Explicit(Term<'arena, Range>),
342+
Implicit(Term<'arena, Range>),
346343
}
347344

348345
/// A field declaration in a record and offset format

‎fathom/src/surface/distillation.rs‎

Lines changed: 31 additions & 31 deletions
Original file line numberDiff line numberDiff line change
@@ -274,10 +274,9 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
274274
let body_expr = self.check(body_expr);
275275
self.truncate_local(initial_local_len);
276276

277-
let params = params.into_iter().map(|(plicity, name)| Param {
278-
plicity,
279-
pattern: Pattern::Name((), name),
280-
r#type: None,
277+
let params = params.into_iter().map(|(plicity, name)| match plicity {
278+
Plicity::Explicit => Param::Explicit(Pattern::Name((), name), None),
279+
Plicity::Implicit => Param::Implicit(Pattern::Name((), name), None),
281280
});
282281

283282
Term::FunLiteral(
@@ -426,10 +425,9 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
426425
core::LocalInfo::Def => {}
427426
core::LocalInfo::Param => {
428427
let var = self.local_len().level_to_index(var).unwrap();
429-
args.push(Arg {
430-
plicity: Plicity::Explicit,
431-
term: self.check(&core::Term::LocalVar(Span::Empty, var)),
432-
});
428+
args.push(Arg::Explicit(
429+
self.check(&core::Term::LocalVar(Span::Empty, var)),
430+
));
433431
}
434432
}
435433
}
@@ -470,35 +468,38 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
470468

471469
let body_type = loop {
472470
match body_type {
473-
// Use an explicit parameter if it is referenced in the body
474-
core::Term::FunType(_, plicity, param_name, param_type, next_body_type)
475-
if next_body_type.binds_local(Index::last()) =>
471+
// Use arrow sugar if the parameter is explicit and is
472+
// not referenced in the body type.
473+
core::Term::FunType(_, Plicity::Explicit, _, param_type, body_type)
474+
if !body_type.binds_local(Index::last()) =>
476475
{
477476
let param_type = self.check(param_type);
478-
let param_name = self.freshen_name(*param_name, next_body_type);
479-
let param_name = self.push_local(param_name);
480-
params.push(Param {
481-
plicity: *plicity,
482-
pattern: Pattern::Name((), param_name),
483-
r#type: Some(param_type),
484-
});
485-
body_type = next_body_type;
486-
}
487-
// Use arrow sugar if the parameter is not referenced in the body type.
488-
core::Term::FunType(_, plicity, _, param_type, body_type) => {
489-
let param_type = self.check(param_type);
490477

491478
self.push_local(None);
492479
let body_type = self.check(body_type);
493480
self.pop_local();
494481

495482
break Term::Arrow(
496483
(),
497-
*plicity,
498484
self.scope.to_scope(param_type),
499485
self.scope.to_scope(body_type),
500486
);
501487
}
488+
// Use a parameter if it is referenced in the body
489+
core::Term::FunType(_, plicity, param_name, param_type, next_body_type) => {
490+
let param_type = self.check(param_type);
491+
let param_name = self.freshen_name(*param_name, next_body_type);
492+
let param_name = self.push_local(param_name);
493+
params.push(match plicity {
494+
Plicity::Explicit => {
495+
Param::Explicit(Pattern::Name((), param_name), Some(param_type))
496+
}
497+
Plicity::Implicit => {
498+
Param::Implicit(Pattern::Name((), param_name), Some(param_type))
499+
}
500+
});
501+
body_type = next_body_type;
502+
}
502503
body_type => break self.check(body_type),
503504
}
504505
};
@@ -529,10 +530,9 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
529530
let body_expr = self.synth(body_expr);
530531
self.truncate_local(initial_local_len);
531532

532-
let params = params.into_iter().map(|(plicity, name)| Param {
533-
plicity,
534-
pattern: Pattern::Name((), name),
535-
r#type: None,
533+
let params = params.into_iter().map(|(plicity, name)| match plicity {
534+
Plicity::Explicit => Param::Explicit(Pattern::Name((), name), None),
535+
Plicity::Implicit => Param::Implicit(Pattern::Name((), name), None),
536536
});
537537

538538
Term::FunLiteral(
@@ -565,9 +565,9 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
565565
(),
566566
self.scope.to_scope(self.synth(head_expr)),
567567
self.scope.to_scope_from_iter(args.into_iter().rev().map(
568-
|(plicity, arg_expr)| Arg {
569-
plicity,
570-
term: self.check(arg_expr),
568+
|(plicity, arg_expr)| match plicity {
569+
Plicity::Explicit => Arg::Explicit(self.check(arg_expr)),
570+
Plicity::Implicit => Arg::Implicit(self.check(arg_expr)),
571571
},
572572
)),
573573
)

‎fathom/src/surface/elaboration.rs‎

Lines changed: 55 additions & 50 deletions
Original file line numberDiff line numberDiff line change
@@ -33,7 +33,7 @@ use crate::env::{self, EnvLen, Level, SharedEnv, UniqueEnv};
3333
use crate::source::{BytePos, ByteRange, Span, Spanned, StringId, StringInterner};
3434
use crate::surface::elaboration::reporting::Message;
3535
use crate::surface::{
36-
distillation, pretty, BinOp, FormatField, Item, Module, Param, Pattern, Term,
36+
distillation, pretty, Arg, BinOp, FormatField, Item, Module, Param, Pattern, Term,
3737
};
3838

3939
mod order;
@@ -934,13 +934,17 @@ impl<'interner, 'arena> Context<'interner, 'arena> {
934934
self.local_env.reserve(params.len());
935935

936936
Vec::from_iter(params.iter().map(|param| {
937-
let range = param.pattern.range();
938-
let (pattern, type_value) =
939-
self.synth_ann_pattern(&param.pattern, param.r#type.as_ref());
937+
let (plicity, pattern, r#type) = match param {
938+
Param::Explicit(pattern, r#type) => (Plicity::Explicit, pattern, r#type),
939+
Param::Implicit(pattern, r#type) => (Plicity::Implicit, pattern, r#type),
940+
};
941+
942+
let range = pattern.range();
943+
let (pattern, type_value) = self.synth_ann_pattern(pattern, r#type.as_ref());
940944
let r#type = self.quote_env().quote(self.scope, &type_value);
941945
let (name, _) = self.push_local_param(pattern, type_value);
942946

943-
(range, param.plicity, name, r#type)
947+
(range, plicity, name, r#type)
944948
}))
945949
}
946950

@@ -1393,7 +1397,7 @@ impl<'interner, 'arena> Context<'interner, 'arena> {
13931397
(expr, r#type)
13941398
}
13951399
Term::Universe(range) => (core::Term::Universe(range.into()), self.universe.clone()),
1396-
Term::Arrow(range, plicity, param_type, body_type) => {
1400+
Term::Arrow(range, param_type, body_type) => {
13971401
let universe = self.universe.clone();
13981402
let param_type = self.check(param_type, &universe);
13991403
let param_type_value = self.eval_env().eval(&param_type);
@@ -1404,7 +1408,7 @@ impl<'interner, 'arena> Context<'interner, 'arena> {
14041408

14051409
let fun_type = core::Term::FunType(
14061410
range.into(),
1407-
*plicity,
1411+
Plicity::Explicit,
14081412
None,
14091413
self.scope.to_scope(param_type),
14101414
self.scope.to_scope(body_type),
@@ -1447,28 +1451,29 @@ impl<'interner, 'arena> Context<'interner, 'arena> {
14471451
let (mut head_expr, mut head_type) = self.synth(head_expr);
14481452

14491453
for arg in *args {
1450-
head_type = self.elim_env().force(&head_type);
1451-
1452-
match arg.plicity {
1453-
Plicity::Implicit => {}
1454-
Plicity::Explicit => {
1454+
let (arg_plicity, arg_term) = match arg {
1455+
Arg::Explicit(arg_term) => {
14551456
(head_expr, head_type) =
14561457
self.insert_implicit_apps(head_range, head_expr, head_type);
1458+
(Plicity::Explicit, arg_term)
14571459
}
1458-
}
1460+
Arg::Implicit(arg_term) => (Plicity::Implicit, arg_term),
1461+
};
1462+
1463+
head_type = self.elim_env().force(&head_type);
14591464

14601465
let (param_type, body_type) = match head_type.as_ref() {
1461-
Value::FunType(plicity, _, param_type, body_type) => {
1462-
if arg.plicity == *plicity {
1466+
Value::FunType(param_plicity, _, param_type, body_type) => {
1467+
if arg_plicity == *param_plicity {
14631468
(param_type, body_type)
14641469
} else {
14651470
let head_type = self.pretty_print_value(&head_type);
14661471
self.messages.push(Message::PlicityArgumentMismatch {
14671472
head_range,
1468-
head_plicity: Plicity::Explicit,
1473+
head_plicity: *param_plicity,
14691474
head_type,
1470-
arg_range: arg.term.range(),
1471-
arg_plicity: arg.plicity,
1475+
arg_range: arg_term.range(),
1476+
arg_plicity,
14721477
});
14731478
return self.synth_reported_error(*range);
14741479
}
@@ -1487,21 +1492,20 @@ impl<'interner, 'arena> Context<'interner, 'arena> {
14871492
self.push_message(Message::UnexpectedArgument {
14881493
head_range,
14891494
head_type,
1490-
arg_range: arg.term.range(),
1495+
arg_range: arg_term.range(),
14911496
});
14921497
return self.synth_reported_error(*range);
14931498
}
14941499
};
14951500

1496-
let arg_range = arg.term.range();
1497-
head_range = ByteRange::merge(&head_range, &arg_range).unwrap();
1498-
1499-
let arg_expr = self.check(&arg.term, param_type);
1501+
let arg_range = arg_term.range();
1502+
let arg_expr = self.check(arg_term, param_type);
15001503
let arg_expr_value = self.eval_env().eval(&arg_expr);
15011504

1505+
head_range = ByteRange::merge(&head_range, &arg_range).unwrap();
15021506
head_expr = core::Term::FunApp(
15031507
head_range.into(),
1504-
arg.plicity,
1508+
arg_plicity,
15051509
self.scope.to_scope(head_expr),
15061510
self.scope.to_scope(arg_expr),
15071511
);
@@ -1695,37 +1699,39 @@ impl<'interner, 'arena> Context<'interner, 'arena> {
16951699
) -> core::Term<'arena> {
16961700
match params.split_first() {
16971701
Some((param, next_params)) => {
1702+
let (param_plicity, pattern, pattern_type) = match param {
1703+
Param::Explicit(pattern, r#type) => (Plicity::Explicit, pattern, r#type),
1704+
Param::Implicit(pattern, r#type) => (Plicity::Implicit, pattern, r#type),
1705+
};
1706+
16981707
let body_type = self.elim_env().force(expected_type);
1699-
match body_type.as_ref() {
1700-
Value::FunType(param_plicity, _, param_type, next_body_type)
1701-
if param.plicity == *param_plicity =>
1708+
match (param_plicity, body_type.as_ref()) {
1709+
(param_plicity, Value::FunType(next_plicity, _, param_type, body_type))
1710+
if param_plicity == *next_plicity =>
17021711
{
1703-
let range =
1704-
ByteRange::merge(&param.pattern.range(), &body_expr.range()).unwrap();
1705-
let pattern = self.check_ann_pattern(
1706-
&param.pattern,
1707-
param.r#type.as_ref(),
1708-
param_type,
1709-
);
1712+
let range = ByteRange::merge(&pattern.range(), &body_expr.range()).unwrap();
1713+
let pattern =
1714+
self.check_ann_pattern(pattern, pattern_type.as_ref(), param_type);
17101715
let (name, arg_expr) = self.push_local_param(pattern, param_type.clone());
17111716

1712-
let body_type = self.elim_env().apply_closure(next_body_type, arg_expr);
1717+
let body_type = self.elim_env().apply_closure(body_type, arg_expr);
17131718
let body_expr =
17141719
self.check_fun_lit(range, next_params, body_expr, &body_type);
17151720
self.local_env.pop();
17161721

17171722
core::Term::FunLit(
17181723
range.into(),
1719-
param.plicity,
1724+
param_plicity,
17201725
name,
17211726
self.scope.to_scope(body_expr),
17221727
)
17231728
}
1724-
// If an implicit function is expected, try to generalise the
1725-
// function literal by wrapping it in an implicit function
1726-
Value::FunType(Plicity::Implicit, param_name, param_type, next_body_type)
1727-
if param.plicity == Plicity::Explicit =>
1728-
{
1729+
// If an implicit function is expected, generalise the
1730+
// function literal by it in an implicit function
1731+
(
1732+
Plicity::Explicit,
1733+
Value::FunType(Plicity::Implicit, param_name, param_type, next_body_type),
1734+
) => {
17291735
let arg_expr = self.local_env.push_param(*param_name, param_type.clone());
17301736
let body_type = self.elim_env().apply_closure(next_body_type, arg_expr);
17311737
let body_expr = self.check_fun_lit(range, params, body_expr, &body_type);
@@ -1737,20 +1743,20 @@ impl<'interner, 'arena> Context<'interner, 'arena> {
17371743
self.scope.to_scope(body_expr),
17381744
)
17391745
}
1740-
// Attempt to elaborate the the body of the function in synthesis
1741-
// mode if we are checking against a metavariable.
1742-
Value::Stuck(Head::MetaVar(_), _) => {
1743-
let range =
1744-
ByteRange::merge(&param.pattern.range(), &body_expr.range()).unwrap();
1746+
// Attempt to elaborate the the body of the function in
1747+
// synthesis mode if we are checking against a metavariable.
1748+
(_, Value::Stuck(Head::MetaVar(_), _)) => {
1749+
let range = ByteRange::merge(&pattern.range(), &body_expr.range()).unwrap();
17451750
let (expr, r#type) = self.synth_fun_lit(range, params, body_expr, None);
17461751
self.convert(range, expr, &r#type, expected_type)
17471752
}
1748-
Value::Stuck(Head::Prim(Prim::ReportedError), _) => {
1753+
// Propagate reported errors
1754+
(_, Value::Stuck(Head::Prim(Prim::ReportedError), _)) => {
17491755
core::Term::Prim(range.into(), Prim::ReportedError)
17501756
}
1751-
_ => {
1757+
(_, _) => {
17521758
self.push_message(Message::UnexpectedParameter {
1753-
param_range: param.pattern.range(),
1759+
param_range: pattern.range(),
17541760
});
17551761
// TODO: For improved error recovery, bind the rest of
17561762
// the parameters, and check the body of the function
@@ -1770,7 +1776,6 @@ impl<'interner, 'arena> Context<'interner, 'arena> {
17701776
body_expr: &Term<'_, ByteRange>,
17711777
body_type: Option<&Term<'_, ByteRange>>,
17721778
) -> (core::Term<'arena>, ArcValue<'arena>) {
1773-
self.local_env.reserve(params.len());
17741779
let initial_local_len = self.local_env.len();
17751780

17761781
let params = self.synth_and_push_params(params);

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

Lines changed: 13 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,7 @@ use fxhash::{FxHashMap, FxHashSet};
2222

2323
use crate::source::{ByteRange, StringId};
2424
use crate::surface::elaboration::reporting::Message;
25-
use crate::surface::{elaboration, FormatField, Item, Module, Param, Pattern, Term};
25+
use crate::surface::{elaboration, Arg, FormatField, Item, Module, Param, Pattern, Term};
2626

2727
enum Error {
2828
CycleDetected,
@@ -222,7 +222,11 @@ fn term_deps(
222222
Term::App(_, head_expr, args) => {
223223
term_deps(head_expr, item_names, local_names, deps);
224224
for arg in *args {
225-
term_deps(&arg.term, item_names, local_names, deps);
225+
match arg {
226+
Arg::Explicit(term) | Arg::Implicit(term) => {
227+
term_deps(term, item_names, local_names, deps);
228+
}
229+
}
226230
}
227231
}
228232
Term::RecordType(_, type_fields) => {
@@ -285,10 +289,14 @@ fn push_param_deps(
285289
deps: &mut Vec<StringId>,
286290
) {
287291
for param in params {
288-
if let Some(r#type) = &param.r#type {
289-
term_deps(r#type, item_names, local_names, deps);
292+
match param {
293+
Param::Explicit(pattern, r#type) | Param::Implicit(pattern, r#type) => {
294+
if let Some(r#type) = r#type {
295+
term_deps(r#type, item_names, local_names, deps);
296+
}
297+
push_pattern(pattern, local_names);
298+
}
290299
}
291-
push_pattern(&param.pattern, local_names);
292300
}
293301
}
294302

0 commit comments

Comments
 (0)