Skip to content

Commit 2893469

Browse files
brendanzabbrendanzab
authored
Merge pull request #419 from Kmeakin/const-match-default
Preserve name of default branch in `core::Term::ConstMatch`
2 parents ac51c20 + 3759852 commit 2893469

File tree

11 files changed

+69
-52
lines changed

11 files changed

+69
-52
lines changed

‎fathom/src/core.rs‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -181,7 +181,7 @@ pub enum Term<'arena> {
181181
Span,
182182
&'arena Term<'arena>,
183183
&'arena [(Const, Term<'arena>)],
184-
Option<&'arena Term<'arena>>,
184+
Option<(Option<StringId>, &'arena Term<'arena>)>,
185185
),
186186
}
187187

@@ -252,7 +252,7 @@ impl<'arena> Term<'arena> {
252252
Term::ConstMatch(_, scrut, branches, default_expr) => {
253253
scrut.binds_local(var)
254254
|| branches.iter().any(|(_, term)| term.binds_local(var))
255-
|| default_expr.map_or(false, |term| term.binds_local(var.prev()))
255+
|| default_expr.map_or(false, |(_, term)| term.binds_local(var.prev()))
256256
}
257257
}
258258
}

‎fathom/src/core/semantics.rs‎

Lines changed: 26 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -171,20 +171,20 @@ impl<'arena> Telescope<'arena> {
171171
pub struct Branches<'arena, P> {
172172
local_exprs: SharedEnv<ArcValue<'arena>>,
173173
pattern_branches: &'arena [(P, Term<'arena>)],
174-
default_expr: Option<&'arena Term<'arena>>,
174+
default_branch: Option<(Option<StringId>, &'arena Term<'arena>)>,
175175
}
176176

177177
impl<'arena, P> Branches<'arena, P> {
178178
/// Construct a single-level pattern match.
179179
pub fn new(
180180
local_exprs: SharedEnv<ArcValue<'arena>>,
181181
pattern_branches: &'arena [(P, Term<'arena>)],
182-
default_expr: Option<&'arena Term<'arena>>,
182+
default_branch: Option<(Option<StringId>, &'arena Term<'arena>)>,
183183
) -> Branches<'arena, P> {
184184
Branches {
185185
local_exprs,
186186
pattern_branches,
187-
default_expr,
187+
default_branch,
188188
}
189189
}
190190

@@ -199,7 +199,7 @@ pub type PatternBranch<'arena, P> = (P, ArcValue<'arena>);
199199
#[derive(Clone, Debug)]
200200
pub enum SplitBranches<'arena, P> {
201201
Branch(PatternBranch<'arena, P>, Branches<'arena, P>),
202-
Default(Closure<'arena>),
202+
Default(Option<StringId>, Closure<'arena>),
203203
None,
204204
}
205205

@@ -487,10 +487,11 @@ impl<'arena, 'env> ElimEnv<'arena, 'env> {
487487
let mut context = self.eval_env(&mut branches.local_exprs);
488488
SplitBranches::Branch((*pattern, context.eval(body_expr)), branches)
489489
}
490-
None => match branches.default_expr {
491-
Some(default_expr) => {
492-
SplitBranches::Default(Closure::new(branches.local_exprs, default_expr))
493-
}
490+
None => match branches.default_branch {
491+
Some((default_name, default_expr)) => SplitBranches::Default(
492+
default_name,
493+
Closure::new(branches.local_exprs, default_expr),
494+
),
494495
None => SplitBranches::None,
495496
},
496497
}
@@ -564,9 +565,11 @@ impl<'arena, 'env> ElimEnv<'arena, 'env> {
564565
}
565566
// Otherwise call default with `head_expr`
566567
let mut local_exprs = branches.local_exprs.clone();
567-
local_exprs.push(head_expr);
568-
match branches.default_expr {
569-
Some(default_expr) => self.eval_env(&mut local_exprs).eval(default_expr),
568+
match branches.default_branch {
569+
Some((_, default_expr)) => {
570+
local_exprs.push(head_expr);
571+
self.eval_env(&mut local_exprs).eval(default_expr)
572+
}
570573
None => panic_any(Error::MissingConstDefault),
571574
}
572575
}
@@ -669,13 +672,15 @@ impl<'in_arena, 'env> QuoteEnv<'in_arena, 'env> {
669672
let mut branches = branches.clone();
670673
let mut pattern_branches = SliceVec::new(scope, branches.num_patterns());
671674

672-
let default_expr = loop {
675+
let default_branch = loop {
673676
match self.elim_env.split_branches(branches) {
674677
SplitBranches::Branch((r#const, body_expr), next_branches) => {
675678
pattern_branches.push((r#const, self.quote(scope, &body_expr)));
676679
branches = next_branches;
677680
}
678-
SplitBranches::Default(default_expr) => break Some(default_expr),
681+
SplitBranches::Default(default_name, default_expr) => {
682+
break Some((default_name, default_expr))
683+
}
679684
SplitBranches::None => break None,
680685
}
681686
};
@@ -684,7 +689,8 @@ impl<'in_arena, 'env> QuoteEnv<'in_arena, 'env> {
684689
span,
685690
scope.to_scope(head_expr),
686691
pattern_branches.into(),
687-
default_expr.map(|expr| self.quote_closure(scope, &expr)),
692+
default_branch
693+
.map(|(name, expr)| (name, self.quote_closure(scope, &expr))),
688694
)
689695
}
690696
},
@@ -968,7 +974,7 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> {
968974
}
969975
}
970976
}
971-
Term::ConstMatch(span, head_expr, branches, default) => {
977+
Term::ConstMatch(span, head_expr, branches, default_branch) => {
972978
match self.unfold_meta_var_spines(scope, head_expr) {
973979
TermOrValue::Term(head_expr) => TermOrValue::Term(Term::ConstMatch(
974980
*span,
@@ -977,10 +983,12 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> {
977983
(branches.iter())
978984
.map(|(r#const, expr)| (*r#const, self.unfold_metas(scope, expr))),
979985
),
980-
default.map(|expr| self.unfold_bound_metas(scope, expr)),
986+
default_branch
987+
.map(|(name, expr)| (name, self.unfold_bound_metas(scope, expr))),
981988
)),
982989
TermOrValue::Value(head_expr) => {
983-
let branches = Branches::new(self.local_exprs.clone(), branches, *default);
990+
let branches =
991+
Branches::new(self.local_exprs.clone(), branches, *default_branch);
984992
TermOrValue::Value(self.elim_env.const_match(head_expr, branches))
985993
}
986994
}
@@ -1213,7 +1221,7 @@ impl<'arena, 'env> ConversionEnv<'arena, 'env> {
12131221
branches0 = next_branches0;
12141222
branches1 = next_branches1;
12151223
}
1216-
(Default(default_expr0), Default(default_expr1)) => {
1224+
(Default(_, default_expr0), Default(_, default_expr1)) => {
12171225
return self.is_equal_closures(&default_expr0, &default_expr1);
12181226
}
12191227
(None, None) => return true,

‎fathom/src/surface/distillation.rs‎

Lines changed: 12 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -296,8 +296,9 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
296296
core::Const::Pos(number) => self.check_number_literal(number),
297297
core::Const::Ref(number) => self.check_number_literal(number),
298298
},
299-
core::Term::ConstMatch(_span, head_expr, branches, default_expr) => {
300-
if let Some((then_expr, else_expr)) = match_if_then_else(branches, *default_expr) {
299+
core::Term::ConstMatch(_span, head_expr, branches, default_branch) => {
300+
if let Some((then_expr, else_expr)) = match_if_then_else(branches, *default_branch)
301+
{
301302
let cond_expr = self.check(head_expr);
302303
let then_expr = self.check(then_expr);
303304
let else_expr = self.check(else_expr);
@@ -310,10 +311,10 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
310311
}
311312

312313
let head_expr = self.synth(head_expr);
313-
match default_expr {
314-
Some(default_expr) => {
314+
match default_branch {
315+
Some((default_name, default_expr)) => {
315316
let default_branch = {
316-
let name = self.push_local(None);
317+
let name = self.push_local(*default_name);
317318
let default_expr = self.check(default_expr);
318319
self.pop_local();
319320

@@ -654,9 +655,9 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
654655

655656
let head_expr = self.synth(head_expr);
656657
match default_expr {
657-
Some(default_expr) => {
658+
Some((default_name, default_expr)) => {
658659
let default_branch = {
659-
let name = self.push_local(None);
660+
let name = self.push_local(*default_name);
660661
let default_expr = self.synth(default_expr);
661662
self.pop_local();
662663

@@ -770,13 +771,13 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
770771

771772
fn match_if_then_else<'arena>(
772773
branches: &'arena [(Const, core::Term<'arena>)],
773-
default_expr: Option<&'arena core::Term<'arena>>,
774+
default_branch: Option<(Option<StringId>, &'arena core::Term<'arena>)>,
774775
) -> Option<(&'arena core::Term<'arena>, &'arena core::Term<'arena>)> {
775-
match (branches, default_expr) {
776+
match (branches, default_branch) {
776777
([(Const::Bool(false), else_expr), (Const::Bool(true), then_expr)], None)
777778
// TODO: Normalise boolean branches when elaborating patterns
778-
| ([(Const::Bool(true), then_expr)], Some(else_expr))
779-
| ([(Const::Bool(false), else_expr)], Some(then_expr)) => Some((then_expr, else_expr)),
779+
| ([(Const::Bool(true), then_expr)], Some((_, else_expr)))
780+
| ([(Const::Bool(false), else_expr)], Some((_, then_expr))) => Some((then_expr, else_expr)),
780781
_ => None,
781782
}
782783
}

‎fathom/src/surface/elaboration.rs‎

Lines changed: 11 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -2049,7 +2049,7 @@ impl<'interner, 'arena> Context<'interner, 'arena> {
20492049
full_span = Span::merge(&full_span, &body_expr.range().into());
20502050

20512051
// Default expression, defined if we arrive at a default case
2052-
let default_expr;
2052+
let default_branch;
20532053

20542054
match self.check_pattern(pattern, &match_info.scrutinee.r#type) {
20552055
// Accumulate constant pattern. Search for it in the accumulated
@@ -2087,19 +2087,23 @@ impl<'interner, 'arena> Context<'interner, 'arena> {
20872087
// add it to the branches. This will simplify the
20882088
// distillation of if expressions.
20892089
(self.local_env).push_param(Some(name), match_info.scrutinee.r#type.clone());
2090-
default_expr = self.check(body_expr, &match_info.expected_type);
2090+
let default_expr = self.check(body_expr, &match_info.expected_type);
2091+
default_branch = (Some(name), self.scope.to_scope(default_expr) as &_);
20912092
self.local_env.pop();
20922093
}
20932094
CheckedPattern::Placeholder(range) => {
20942095
self.check_match_reachable(is_reachable, range);
20952096

20962097
(self.local_env).push_param(None, match_info.scrutinee.r#type.clone());
2097-
default_expr = self.check(body_expr, &match_info.expected_type);
2098+
let default_expr = self.check(body_expr, &match_info.expected_type);
2099+
default_branch = (None, self.scope.to_scope(default_expr) as &_);
20982100
self.local_env.pop();
20992101
}
21002102
CheckedPattern::ReportedError(range) => {
2101-
self.check(body_expr, &match_info.expected_type);
2102-
default_expr = core::Term::Prim(range.into(), Prim::ReportedError);
2103+
(self.local_env).push_param(None, match_info.scrutinee.r#type.clone());
2104+
let default_expr = core::Term::Prim(range.into(), Prim::ReportedError);
2105+
default_branch = (None, self.scope.to_scope(default_expr) as &_);
2106+
self.local_env.pop();
21032107
}
21042108
};
21052109

@@ -2110,7 +2114,7 @@ impl<'interner, 'arena> Context<'interner, 'arena> {
21102114
full_span,
21112115
match_info.scrutinee.expr,
21122116
self.scope.to_scope_from_iter(branches.into_iter()),
2113-
Some(self.scope.to_scope(default_expr)),
2117+
Some(default_branch),
21142118
);
21152119
}
21162120

@@ -2127,7 +2131,7 @@ impl<'interner, 'arena> Context<'interner, 'arena> {
21272131
full_span,
21282132
match_info.scrutinee.expr,
21292133
self.scope.to_scope_from_iter(branches.into_iter()),
2130-
default_expr.map(|expr| self.scope.to_scope(expr) as &_),
2134+
default_expr.map(|expr| (None, self.scope.to_scope(expr) as &_)),
21312135
)
21322136
}
21332137

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

Lines changed: 9 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -403,7 +403,7 @@ impl<'arena, 'env> Context<'arena, 'env> {
403403
branches1 = next_branches1;
404404
}
405405
},
406-
(Default(default_expr0), Default(default_expr1)) => {
406+
(Default(_, default_expr0), Default(_, default_expr1)) => {
407407
return self.unify_closures(&default_expr0, &default_expr1);
408408
}
409409
(None, None) => return Ok(()),
@@ -559,15 +559,18 @@ impl<'arena, 'env> Context<'arena, 'env> {
559559
let mut pattern_branches =
560560
SliceVec::new(self.scope, branches.num_patterns());
561561

562-
let default_expr = loop {
562+
let default_branch = loop {
563563
match self.elim_env().split_branches(branches) {
564564
SplitBranches::Branch((r#const, body_expr), next_branch) => {
565565
pattern_branches
566566
.push((r#const, self.rename(meta_var, &body_expr)?));
567567
branches = next_branch;
568568
}
569-
SplitBranches::Default(default_expr) => {
570-
break Some(self.rename_closure(meta_var, &default_expr)?)
569+
SplitBranches::Default(default_name, default_expr) => {
570+
break Some((
571+
default_name,
572+
self.rename_closure(meta_var, &default_expr)?,
573+
))
571574
}
572575
SplitBranches::None => break None,
573576
}
@@ -577,7 +580,8 @@ impl<'arena, 'env> Context<'arena, 'env> {
577580
span,
578581
self.scope.to_scope(head_expr?),
579582
pattern_branches.into(),
580-
default_expr.map(|expr| self.scope.to_scope(expr) as &_),
583+
default_branch
584+
.map(|(name, expr)| (name, self.scope.to_scope(expr) as &_)),
581585
)
582586
}
583587
})

‎tests/succeed/equality.snap‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -41,12 +41,12 @@ let four_chars : fun (P : U32 -> Type) -> P "beng" -> P 1650814567 =
4141
refl U32 "beng";
4242
let three_chars : fun (P : U32 -> Type) -> P "BEN " -> P 1111838240 =
4343
refl U32 "BEN ";
44-
let foo : U32 -> U32 = fun x => match x { 1 => 0, _ => _ };
44+
let foo : U32 -> U32 = fun x => match x { 1 => 0, x => x };
4545
let eq_foo : fun (P : (U32 -> U32) -> Type) -> P (fun x => match x {
4646
1 => 0,
47-
_ => _,
48-
}) -> P (fun x => match x { 1 => 0, _ => _ }) = refl (U32 ->
49-
U32) (fun _ => match _ { 1 => 0, _ => _ });
47+
x => x,
48+
}) -> P (fun x => match x { 1 => 0, x => x }) = refl (U32 ->
49+
U32) (fun _ => match _ { 1 => 0, x => x });
5050
Type : Type
5151
'''
5252
stderr = ''

‎tests/succeed/match/check-const-1.snap‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
11
stdout = '''
2-
let x : U8 = 3; match x { 1 => 0, _ => _ } : U8
2+
let x : U8 = 3; match x { 1 => 0, x => x } : U8
33
'''
44
stderr = ''

‎tests/succeed/match/check-const-2.snap‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
11
stdout = '''
2-
let x : U8 = 3; match x { 1 => 0, 3 => 7, _ => _ } : U8
2+
let x : U8 = 3; match x { 1 => 0, 3 => 7, x => x } : U8
33
'''
44
stderr = ''

‎tests/succeed/match/check-const-redundant.snap‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
stdout = '''
2-
let x : U8 = 3; match x { 1 => 0, 3 => 7, _ => _ } : U8
2+
let x : U8 = 3; match x { 1 => 0, 3 => 7, x => x } : U8
33
'''
44
stderr = '''
55
warning: unreachable pattern

‎tests/succeed/match/synth-const-1.snap‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
11
stdout = '''
2-
let x : U8 = 3; match x { 1 => x, _ => _ } : U8
2+
let x : U8 = 3; match x { 1 => x, x => x } : U8
33
'''
44
stderr = ''

0 commit comments

Comments
 (0)