Skip to content

Commit

Permalink
Make it easier to distill/pretty print values
Browse files Browse the repository at this point in the history 
This reduces the gymnasics 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.
  • Loading branch information
@brendanzab
brendanzab committed Feb 9, 2023
1 parent 505176a commit 8446cb2
Show file tree
Hide file tree
Showing 2 changed files with 22 additions and 51 deletions.
4 changes: 2 additions & 2 deletions fathom/src/surface/distillation.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -41,7 +41,7 @@ pub struct Context<'arena, 'env> {
/// Item name environment.
item_names: &'env UniqueEnv<Symbol>,
/// Local name environment.
local_names: &'env mut UniqueEnv<Option<Symbol>>,
local_names: UniqueEnv<Option<Symbol>>,
/// Metavariable sources.
meta_sources: &'env UniqueEnv<MetaSource>,
}
Expand All @@ -51,7 +51,7 @@ impl<'arena, 'env> Context<'arena, 'env> {
pub fn new(
scope: &'arena Scope<'arena>,
item_names: &'env UniqueEnv<Symbol>,
local_names: &'env mut UniqueEnv<Option<Symbol>>,
local_names: UniqueEnv<Option<Symbol>>,
meta_sources: &'env UniqueEnv<MetaSource>,
) -> Context<'arena, 'env> {
Context {
Expand Down
69 changes: 20 additions & 49 deletions fathom/src/surface/elaboration.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -375,19 +375,7 @@ impl<'arena> Context<'arena> {
(None, source) => on_message(Message::UnsolvedMetaVar { source }),
// Yield messages of solved named holes
(Some(expr), MetaSource::HoleExpr(range, name)) => {
let term = self.quote_env().quote(self.scope, expr);
let surface_term = distillation::Context::new(
self.scope,
&self.item_env.names,
&mut self.local_env.names,
&self.meta_env.sources,
)
.check(&term);

let pretty_context = pretty::Context::new(self.scope);
let doc = pretty_context.term(&surface_term).into_doc();
let expr = doc.pretty(usize::MAX).to_string();

let expr = self.pretty_value(expr);
on_message(Message::HoleSolution { range, name, expr });
}
// Ignore solutions of anything else
Expand Down Expand Up @@ -420,18 +408,18 @@ impl<'arena> Context<'arena> {
}

pub fn distillation_context<'out_arena>(
&mut self,
&self,
scope: &'out_arena Scope<'out_arena>,
) -> distillation::Context<'out_arena, '_> {
distillation::Context::new(
scope,
&self.item_env.names,
&mut self.local_env.names,
self.local_env.names.clone(),
&self.meta_env.sources,
)
}

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

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

let from = self.pretty_print_value(&from);
let to = self.pretty_print_value(&to);
self.push_message(Message::FailedToUnify {
range,
found: from,
expected: to,
found: self.pretty_value(&from),
expected: self.pretty_value(&to),
error,
});
core::Term::Prim(span, Prim::ReportedError)
Expand Down Expand Up @@ -757,10 +743,9 @@ impl<'arena> Context<'arena> {
// Some((Prim::Array64Type, [len, _])) => todo!(),
Some((Prim::ReportedError, _)) => None,
_ => {
let expected_type = self.pretty_print_value(expected_type);
self.push_message(Message::StringLiteralNotSupported {
range: file_range,
expected_type,
expected_type: self.pretty_value(expected_type),
});
None
}
Expand All @@ -785,10 +770,9 @@ impl<'arena> Context<'arena> {
Some((Prim::F64Type, [])) => self.parse_number(*range, *lit, Const::F64),
Some((Prim::ReportedError, _)) => None,
_ => {
let expected_type = self.pretty_print_value(expected_type);
self.push_message(Message::NumericLiteralNotSupported {
range: file_range,
expected_type,
expected_type: self.pretty_value(expected_type),
});
None
}
Expand Down Expand Up @@ -875,12 +859,10 @@ impl<'arena> Context<'arena> {
match self.unification_context().unify(&r#type, expected_type) {
Ok(()) => self.check_pattern(pattern, &r#type),
Err(error) => {
let lhs = self.pretty_print_value(&r#type);
let rhs = self.pretty_print_value(expected_type);
self.push_message(Message::FailedToUnify {
range: file_range,
found: lhs,
expected: rhs,
found: self.pretty_value(&r#type),
expected: self.pretty_value(expected_type),
error,
});
CheckedPattern::ReportedError(file_range)
Expand Down Expand Up @@ -1178,10 +1160,9 @@ impl<'arena> Context<'arena> {
return core::Term::Prim(file_range.into(), Prim::ReportedError)
}
_ => {
let expected_type = self.pretty_print_value(&expected_type);
self.push_message(Message::ArrayLiteralNotSupported {
range: file_range,
expected_type,
expected_type: self.pretty_value(&expected_type),
});
return core::Term::Prim(file_range.into(), Prim::ReportedError);
}
Expand Down Expand Up @@ -1213,11 +1194,10 @@ impl<'arena> Context<'arena> {
self.check(elem_expr, elem_type);
}

let expected_len = self.pretty_print_value(len_value.unwrap());
self.push_message(Message::MismatchedArrayLength {
range: file_range,
found_len: elem_exprs.len(),
expected_len,
expected_len: self.pretty_value(len_value.unwrap()),
});

core::Term::Prim(file_range.into(), Prim::ReportedError)
Expand All @@ -1236,10 +1216,9 @@ impl<'arena> Context<'arena> {
// Some((Prim::Array64Type, [len, _])) => todo!(),
Some((Prim::ReportedError, _)) => None,
_ => {
let expected_type = self.pretty_print_value(&expected_type);
self.push_message(Message::StringLiteralNotSupported {
range: file_range,
expected_type,
expected_type: self.pretty_value(&expected_type),
});
None
}
Expand All @@ -1264,10 +1243,9 @@ impl<'arena> Context<'arena> {
Some((Prim::F64Type, [])) => self.parse_number(*range, *lit, Const::F64),
Some((Prim::ReportedError, _)) => None,
_ => {
let expected_type = self.pretty_print_value(&expected_type);
self.push_message(Message::NumericLiteralNotSupported {
range: file_range,
expected_type,
expected_type: self.pretty_value(&expected_type),
});
return core::Term::Prim(file_range.into(), Prim::ReportedError);
}
Expand Down Expand Up @@ -1521,11 +1499,10 @@ impl<'arena> Context<'arena> {
if arg.plicity == *plicity {
(param_type, body_type)
} else {
let head_type = self.pretty_print_value(&head_type);
self.messages.push(Message::PlicityArgumentMismatch {
head_range: self.file_range(head_range),
head_plicity: Plicity::Explicit,
head_type,
head_type: self.pretty_value(&head_type),
arg_range: self.file_range(arg.term.range()),
arg_plicity: arg.plicity,
});
Expand All @@ -1542,10 +1519,9 @@ impl<'arena> Context<'arena> {
_ => {
// NOTE: We could try to infer that this is a function type,
// but this takes more work to prevent cascading type errors
let head_type = self.pretty_print_value(&head_type);
self.push_message(Message::UnexpectedArgument {
head_range: self.file_range(head_range),
head_type,
head_type: self.pretty_value(&head_type),
arg_range: self.file_range(arg.term.range()),
});
return self.synth_reported_error(*range);
Expand Down Expand Up @@ -1681,15 +1657,12 @@ impl<'arena> Context<'arena> {
_ => {}
}

let head_type = self.pretty_print_value(&head_type);
let suggestion =
suggest_name(*proj_label, labels.iter().map(|(_, label)| *label));
self.push_message(Message::UnknownField {
head_range: self.file_range(head_range),
head_type,
head_type: self.pretty_value(&head_type),
label_range: self.file_range(*label_range),
label: *proj_label,
suggestion,
suggestion: suggest_name(*proj_label, labels.iter().map(|(_, l)| *l)),
});
return self.synth_reported_error(*range);
}
Expand Down Expand Up @@ -2005,15 +1978,13 @@ impl<'arena> Context<'arena> {
(Gte(_), Some(((S64Type, []), (S64Type, [])))) => (S64Gte, BoolType),

_ => {
let lhs_pretty = self.pretty_print_value(&lhs_type);
let rhs_pretty = self.pretty_print_value(&rhs_type);
self.push_message(Message::BinOpMismatchedTypes {
range: self.file_range(range),
lhs_range: self.file_range(lhs.range()),
rhs_range: self.file_range(rhs.range()),
op: op.map_range(|range| self.file_range(range)),
lhs: lhs_pretty,
rhs: rhs_pretty,
lhs: self.pretty_value(&lhs_type),
rhs: self.pretty_value(&rhs_type),
});
return self.synth_reported_error(range);
}
Expand Down

0 comments on commit 8446cb2

Please sign in to comment.