Skip to content

Commit db5c996

Browse files
brendanzabbrendanzab
authored
Merge pull request #435 from Kmeakin/fresh-names
Replace all used occurances of `_` with fresh names
2 parents 64e4f3c + 5962f10 commit db5c996

File tree

5 files changed

+122
-77
lines changed

5 files changed

+122
-77
lines changed

‎doc/roadmap.md‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -73,7 +73,7 @@
7373
- [x] unification
7474
- [x] zonking
7575
- [x] distiller
76-
- [ ] improve binder names
76+
- [x] improve binder names
7777
- [ ] improve hole names
7878
- [ ] core language validation
7979
- [x] binary format interpreter

‎fathom/src/surface/distillation.rs‎

Lines changed: 54 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -82,6 +82,42 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
8282
}
8383
}
8484

85+
/// Generate a fresh name that does not appear in `self.local_names`
86+
fn gen_fresh_name(&mut self) -> StringId {
87+
fn to_str(x: u32) -> String {
88+
let base = x / 26;
89+
let letter = x % 26;
90+
let letter = (letter as u8 + b'a') as char;
91+
if base == 0 {
92+
format!("{letter}")
93+
} else {
94+
format!("{letter}{base}")
95+
}
96+
}
97+
98+
let mut counter = 0;
99+
loop {
100+
let name = to_str(counter);
101+
let name = self.interner.borrow_mut().get_or_intern(name);
102+
match self.local_names.iter().any(|symbol| *symbol == Some(name)) {
103+
true => {}
104+
false => return name,
105+
}
106+
counter += 1;
107+
}
108+
}
109+
110+
/// Replace `name` with a fresh name if it is `_` and occurs in `body`
111+
fn freshen_name(&mut self, name: Option<StringId>, body: &core::Term<'_>) -> Option<StringId> {
112+
match name {
113+
Some(name) => Some(name),
114+
None => match body.binds_local(Index::last()) {
115+
false => None,
116+
true => Some(self.gen_fresh_name()),
117+
},
118+
}
119+
}
120+
85121
fn check_number_literal_styled<T: core::UIntStyled<N>, const N: usize>(
86122
&mut self,
87123
number: T,
@@ -224,7 +260,8 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
224260
let def_type = self.check(def_type);
225261
let def_expr = self.check(def_expr);
226262

227-
let def_name = self.push_local(*def_name);
263+
let def_name = self.freshen_name(*def_name, body_expr);
264+
let def_name = self.push_local(def_name);
228265
let body_expr = self.check(body_expr);
229266
self.pop_local();
230267

@@ -236,11 +273,14 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
236273
self.scope.to_scope(body_expr),
237274
)
238275
}
239-
core::Term::FunLit(_, param_name, mut body_expr) => {
276+
core::Term::FunLit(..) => {
240277
let initial_local_len = self.local_len();
241-
let mut param_names = vec![self.push_local(*param_name)];
278+
let mut param_names = Vec::new();
279+
let mut body_expr = core_term;
280+
242281
while let core::Term::FunLit(_, param_name, next_body_expr) = body_expr {
243-
param_names.push(self.push_local(*param_name));
282+
let param_name = self.freshen_name(*param_name, next_body_expr);
283+
param_names.push(self.push_local(param_name));
244284
body_expr = next_body_expr;
245285
}
246286

@@ -323,7 +363,8 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
323363
match default_branch {
324364
Some((default_name, default_expr)) => {
325365
let default_branch = {
326-
let name = self.push_local(*default_name);
366+
let name = self.freshen_name(*default_name, default_expr);
367+
let name = self.push_local(name);
327368
let default_expr = self.check(default_expr);
328369
self.pop_local();
329370

@@ -414,7 +455,8 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
414455
let def_type = self.check(def_type);
415456
let def_expr = self.check(def_expr);
416457

417-
let def_name = self.push_local(*def_name);
458+
let def_name = self.freshen_name(*def_name, body_expr);
459+
let def_name = self.push_local(def_name);
418460
let body_expr = self.synth(body_expr);
419461
self.pop_local();
420462

@@ -441,7 +483,8 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
441483
if next_body_type.binds_local(Index::last()) =>
442484
{
443485
let param_type = self.check(param_type);
444-
let param_name = self.push_local(*param_name);
486+
let param_name = self.freshen_name(*param_name, next_body_type);
487+
let param_name = self.push_local(param_name);
445488
patterns.push((
446489
Pattern::Name((), param_name),
447490
Some(self.scope.to_scope(param_type) as &_),
@@ -485,7 +528,8 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
485528
let mut body_expr = core_term;
486529

487530
while let core::Term::FunLit(_, param_name, next_body_expr) = body_expr {
488-
param_names.push(self.push_local(*param_name));
531+
let param_name = self.freshen_name(*param_name, next_body_expr);
532+
param_names.push(self.push_local(param_name));
489533
body_expr = next_body_expr;
490534
}
491535

@@ -654,7 +698,8 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
654698
match default_expr {
655699
Some((default_name, default_expr)) => {
656700
let default_branch = {
657-
let name = self.push_local(*default_name);
701+
let name = self.freshen_name(*default_name, default_expr);
702+
let name = self.push_local(name);
658703
let default_expr = self.synth(default_expr);
659704
self.pop_local();
660705

‎tests/succeed/equality.snap‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -46,7 +46,7 @@ let eq_foo : fun (P : (U32 -> U32) -> Type) -> P (fun x => match x {
4646
1 => 0,
4747
x => x,
4848
}) -> P (fun x => match x { 1 => 0, x => x }) = refl (U32 ->
49-
U32) (fun _ => match _ { 1 => 0, x => x });
49+
U32) (fun a => match a { 1 => 0, x => x });
5050
Type : Type
5151
'''
5252
stderr = ''

‎tests/succeed/prelude.snap‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -58,7 +58,7 @@ P a0 -> P a2 =
5858
fun _ a0 a1 a2 p0 p1 P => compose (P a0) (P a1) (P a2) (p0 P) (p1 P);
5959
let sym : fun (A : Type) (a0 : A) (a1 : A) -> (fun (P : A -> Type) -> P a0 ->
6060
P a1) -> fun (P : A -> Type) -> P a1 -> P a0 =
61-
fun _ a0 a1 p => p (fun a1 => Eq _ a1 a0) (refl _ a0);
61+
fun a a0 a1 p => p (fun a1 => Eq a a1 a0) (refl a a0);
6262
let id_apply_type : Type = (fun a => a) Type;
6363
let list1 : fun (List : Type) -> List -> (Bool -> List -> List) -> List =
6464
cons Bool (id Bool true) (nil Bool);
@@ -73,7 +73,7 @@ P (fun Nat succ zero => succ (succ (succ (succ (succ (succ (succ (succ (succ (su
7373
->
7474
P (fun Nat succ zero => succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) =
7575
refl (fun (Nat : Type) -> (Nat -> Nat) -> Nat ->
76-
Nat) (fun _ _ _ => _ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ _))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))));
76+
Nat) (fun _ a b => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))));
7777
let eq_id_apply_type : fun (P : Type -> Type) -> P Type -> P Type =
7878
refl Type Type;
7979
let eq_id_apply_true : fun (P : Bool -> Type) -> P true -> P true =

0 commit comments

Comments
 (0)