Skip to content

Commit d9a0246

Browse files
brendanzabbrendanzab
committed
Make it easier to distill/pretty print values
This reduces the qymnasics we’ve needed to do whenever we want to pretty print something by cloning the name environment as opposed to taking it by mutable reference when constructing a distillation environment. This means we can no longer reuse the existing allocation when temporarily pushing local names, but I think the savings we got from this was probably minor, and the increase in clarity is worth it.
1 parent 505176a commit d9a0246

File tree

2 files changed

+22
-51
lines changed

2 files changed

+22
-51
lines changed

‎fathom/src/surface/distillation.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -41,7 +41,7 @@ pub struct Context<'arena, 'env> {
4141
/// Item name environment.
4242
item_names: &'env UniqueEnv<Symbol>,
4343
/// Local name environment.
44-
local_names: &'env mut UniqueEnv<Option<Symbol>>,
44+
local_names: UniqueEnv<Option<Symbol>>,
4545
/// Metavariable sources.
4646
meta_sources: &'env UniqueEnv<MetaSource>,
4747
}
@@ -51,7 +51,7 @@ impl<'arena, 'env> Context<'arena, 'env> {
5151
pub fn new(
5252
scope: &'arena Scope<'arena>,
5353
item_names: &'env UniqueEnv<Symbol>,
54-
local_names: &'env mut UniqueEnv<Option<Symbol>>,
54+
local_names: UniqueEnv<Option<Symbol>>,
5555
meta_sources: &'env UniqueEnv<MetaSource>,
5656
) -> Context<'arena, 'env> {
5757
Context {

‎fathom/src/surface/elaboration.rs

Lines changed: 20 additions & 49 deletions
Original file line numberDiff line numberDiff line change
@@ -375,19 +375,7 @@ impl<'arena> Context<'arena> {
375375
(None, source) => on_message(Message::UnsolvedMetaVar { source }),
376376
// Yield messages of solved named holes
377377
(Some(expr), MetaSource::HoleExpr(range, name)) => {
378-
let term = self.quote_env().quote(self.scope, expr);
379-
let surface_term = distillation::Context::new(
380-
self.scope,
381-
&self.item_env.names,
382-
&mut self.local_env.names,
383-
&self.meta_env.sources,
384-
)
385-
.check(&term);
386-
387-
let pretty_context = pretty::Context::new(self.scope);
388-
let doc = pretty_context.term(&surface_term).into_doc();
389-
let expr = doc.pretty(usize::MAX).to_string();
390-
378+
let expr = self.pretty_value(expr);
391379
on_message(Message::HoleSolution { range, name, expr });
392380
}
393381
// Ignore solutions of anything else
@@ -420,18 +408,18 @@ impl<'arena> Context<'arena> {
420408
}
421409

422410
pub fn distillation_context<'out_arena>(
423-
&mut self,
411+
&self,
424412
scope: &'out_arena Scope<'out_arena>,
425413
) -> distillation::Context<'out_arena, '_> {
426414
distillation::Context::new(
427415
scope,
428416
&self.item_env.names,
429-
&mut self.local_env.names,
417+
self.local_env.names.clone(),
430418
&self.meta_env.sources,
431419
)
432420
}
433421

434-
fn pretty_print_value(&mut self, value: &ArcValue<'_>) -> String {
422+
fn pretty_value(&self, value: &ArcValue<'_>) -> String {
435423
let scope = self.scope;
436424

437425
let term = self.quote_env().unfolding_metas().quote(scope, value);
@@ -625,12 +613,10 @@ impl<'arena> Context<'arena> {
625613
}
626614
};
627615

628-
let from = self.pretty_print_value(&from);
629-
let to = self.pretty_print_value(&to);
630616
self.push_message(Message::FailedToUnify {
631617
range,
632-
found: from,
633-
expected: to,
618+
found: self.pretty_value(&from),
619+
expected: self.pretty_value(&to),
634620
error,
635621
});
636622
core::Term::Prim(span, Prim::ReportedError)
@@ -757,10 +743,9 @@ impl<'arena> Context<'arena> {
757743
// Some((Prim::Array64Type, [len, _])) => todo!(),
758744
Some((Prim::ReportedError, _)) => None,
759745
_ => {
760-
let expected_type = self.pretty_print_value(expected_type);
761746
self.push_message(Message::StringLiteralNotSupported {
762747
range: file_range,
763-
expected_type,
748+
expected_type: self.pretty_value(expected_type),
764749
});
765750
None
766751
}
@@ -785,10 +770,9 @@ impl<'arena> Context<'arena> {
785770
Some((Prim::F64Type, [])) => self.parse_number(*range, *lit, Const::F64),
786771
Some((Prim::ReportedError, _)) => None,
787772
_ => {
788-
let expected_type = self.pretty_print_value(expected_type);
789773
self.push_message(Message::NumericLiteralNotSupported {
790774
range: file_range,
791-
expected_type,
775+
expected_type: self.pretty_value(expected_type),
792776
});
793777
None
794778
}
@@ -875,12 +859,10 @@ impl<'arena> Context<'arena> {
875859
match self.unification_context().unify(&r#type, expected_type) {
876860
Ok(()) => self.check_pattern(pattern, &r#type),
877861
Err(error) => {
878-
let lhs = self.pretty_print_value(&r#type);
879-
let rhs = self.pretty_print_value(expected_type);
880862
self.push_message(Message::FailedToUnify {
881863
range: file_range,
882-
found: lhs,
883-
expected: rhs,
864+
found: self.pretty_value(&r#type),
865+
expected: self.pretty_value(expected_type),
884866
error,
885867
});
886868
CheckedPattern::ReportedError(file_range)
@@ -1178,10 +1160,9 @@ impl<'arena> Context<'arena> {
11781160
return core::Term::Prim(file_range.into(), Prim::ReportedError)
11791161
}
11801162
_ => {
1181-
let expected_type = self.pretty_print_value(&expected_type);
11821163
self.push_message(Message::ArrayLiteralNotSupported {
11831164
range: file_range,
1184-
expected_type,
1165+
expected_type: self.pretty_value(&expected_type),
11851166
});
11861167
return core::Term::Prim(file_range.into(), Prim::ReportedError);
11871168
}
@@ -1213,11 +1194,10 @@ impl<'arena> Context<'arena> {
12131194
self.check(elem_expr, elem_type);
12141195
}
12151196

1216-
let expected_len = self.pretty_print_value(len_value.unwrap());
12171197
self.push_message(Message::MismatchedArrayLength {
12181198
range: file_range,
12191199
found_len: elem_exprs.len(),
1220-
expected_len,
1200+
expected_len: self.pretty_value(len_value.unwrap()),
12211201
});
12221202

12231203
core::Term::Prim(file_range.into(), Prim::ReportedError)
@@ -1236,10 +1216,9 @@ impl<'arena> Context<'arena> {
12361216
// Some((Prim::Array64Type, [len, _])) => todo!(),
12371217
Some((Prim::ReportedError, _)) => None,
12381218
_ => {
1239-
let expected_type = self.pretty_print_value(&expected_type);
12401219
self.push_message(Message::StringLiteralNotSupported {
12411220
range: file_range,
1242-
expected_type,
1221+
expected_type: self.pretty_value(&expected_type),
12431222
});
12441223
None
12451224
}
@@ -1264,10 +1243,9 @@ impl<'arena> Context<'arena> {
12641243
Some((Prim::F64Type, [])) => self.parse_number(*range, *lit, Const::F64),
12651244
Some((Prim::ReportedError, _)) => None,
12661245
_ => {
1267-
let expected_type = self.pretty_print_value(&expected_type);
12681246
self.push_message(Message::NumericLiteralNotSupported {
12691247
range: file_range,
1270-
expected_type,
1248+
expected_type: self.pretty_value(&expected_type),
12711249
});
12721250
return core::Term::Prim(file_range.into(), Prim::ReportedError);
12731251
}
@@ -1521,11 +1499,10 @@ impl<'arena> Context<'arena> {
15211499
if arg.plicity == *plicity {
15221500
(param_type, body_type)
15231501
} else {
1524-
let head_type = self.pretty_print_value(&head_type);
15251502
self.messages.push(Message::PlicityArgumentMismatch {
15261503
head_range: self.file_range(head_range),
15271504
head_plicity: Plicity::Explicit,
1528-
head_type,
1505+
head_type: self.pretty_value(&head_type),
15291506
arg_range: self.file_range(arg.term.range()),
15301507
arg_plicity: arg.plicity,
15311508
});
@@ -1542,10 +1519,9 @@ impl<'arena> Context<'arena> {
15421519
_ => {
15431520
// NOTE: We could try to infer that this is a function type,
15441521
// but this takes more work to prevent cascading type errors
1545-
let head_type = self.pretty_print_value(&head_type);
15461522
self.push_message(Message::UnexpectedArgument {
15471523
head_range: self.file_range(head_range),
1548-
head_type,
1524+
head_type: self.pretty_value(&head_type),
15491525
arg_range: self.file_range(arg.term.range()),
15501526
});
15511527
return self.synth_reported_error(*range);
@@ -1681,15 +1657,12 @@ impl<'arena> Context<'arena> {
16811657
_ => {}
16821658
}
16831659

1684-
let head_type = self.pretty_print_value(&head_type);
1685-
let suggestion =
1686-
suggest_name(*proj_label, labels.iter().map(|(_, label)| *label));
16871660
self.push_message(Message::UnknownField {
16881661
head_range: self.file_range(head_range),
1689-
head_type,
1662+
head_type: self.pretty_value(&head_type),
16901663
label_range: self.file_range(*label_range),
16911664
label: *proj_label,
1692-
suggestion,
1665+
suggestion: suggest_name(*proj_label, labels.iter().map(|(_, l)| *l)),
16931666
});
16941667
return self.synth_reported_error(*range);
16951668
}
@@ -2005,15 +1978,13 @@ impl<'arena> Context<'arena> {
20051978
(Gte(_), Some(((S64Type, []), (S64Type, [])))) => (S64Gte, BoolType),
20061979

20071980
_ => {
2008-
let lhs_pretty = self.pretty_print_value(&lhs_type);
2009-
let rhs_pretty = self.pretty_print_value(&rhs_type);
20101981
self.push_message(Message::BinOpMismatchedTypes {
20111982
range: self.file_range(range),
20121983
lhs_range: self.file_range(lhs.range()),
20131984
rhs_range: self.file_range(rhs.range()),
20141985
op: op.map_range(|range| self.file_range(range)),
2015-
lhs: lhs_pretty,
2016-
rhs: rhs_pretty,
1986+
lhs: self.pretty_value(&lhs_type),
1987+
rhs: self.pretty_value(&rhs_type),
20171988
});
20181989
return self.synth_reported_error(range);
20191990
}

0 commit comments

Comments
 (0)