Skip to content

Commit 31e36af

Browse files
KmeakinKmeakin
committed
Replace all used occurances of _ of fresh names
1 parent a74f45e commit 31e36af

File tree

4 files changed

+121
-76
lines changed

4 files changed

+121
-76
lines changed

‎fathom/src/surface/distillation.rs‎

Lines changed: 54 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -86,6 +86,42 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
8686
}
8787
}
8888

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

232-
let def_name = self.push_local(*def_name);
268+
let def_name = self.freshen_name(*def_name, body_expr);
269+
let def_name = self.push_local(def_name);
233270
let body_expr = self.check(body_expr);
234271
self.pop_local();
235272

@@ -241,11 +278,14 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
241278
self.scope.to_scope(body_expr),
242279
)
243280
}
244-
core::Term::FunLit(_, param_name, mut body_expr) => {
281+
core::Term::FunLit(..) => {
245282
let initial_local_len = self.local_len();
246-
let mut param_names = vec![self.push_local(*param_name)];
283+
let mut param_names = Vec::new();
284+
let mut body_expr = core_term;
285+
247286
while let core::Term::FunLit(_, param_name, next_body_expr) = body_expr {
248-
param_names.push(self.push_local(*param_name));
287+
let param_name = self.freshen_name(*param_name, next_body_expr);
288+
param_names.push(self.push_local(param_name));
249289
body_expr = next_body_expr;
250290
}
251291

@@ -328,7 +368,8 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
328368
match default_branch {
329369
Some((default_name, default_expr)) => {
330370
let default_branch = {
331-
let name = self.push_local(*default_name);
371+
let name = self.freshen_name(*default_name, default_expr);
372+
let name = self.push_local(name);
332373
let default_expr = self.check(default_expr);
333374
self.pop_local();
334375

@@ -419,7 +460,8 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
419460
let def_type = self.check(def_type);
420461
let def_expr = self.check(def_expr);
421462

422-
let def_name = self.push_local(*def_name);
463+
let def_name = self.freshen_name(*def_name, body_expr);
464+
let def_name = self.push_local(def_name);
423465
let body_expr = self.synth(body_expr);
424466
self.pop_local();
425467

@@ -446,7 +488,8 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
446488
if next_body_type.binds_local(Index::last()) =>
447489
{
448490
let param_type = self.check(param_type);
449-
let param_name = self.push_local(*param_name);
491+
let param_name = self.freshen_name(*param_name, next_body_type);
492+
let param_name = self.push_local(param_name);
450493
patterns.push((
451494
Pattern::Name((), param_name),
452495
Some(self.scope.to_scope(param_type) as &_),
@@ -490,7 +533,8 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
490533
let mut body_expr = core_term;
491534

492535
while let core::Term::FunLit(_, param_name, next_body_expr) = body_expr {
493-
param_names.push(self.push_local(*param_name));
536+
let param_name = self.freshen_name(*param_name, next_body_expr);
537+
param_names.push(self.push_local(param_name));
494538
body_expr = next_body_expr;
495539
}
496540

@@ -659,7 +703,8 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
659703
match default_expr {
660704
Some((default_name, default_expr)) => {
661705
let default_branch = {
662-
let name = self.push_local(*default_name);
706+
let name = self.freshen_name(*default_name, default_expr);
707+
let name = self.push_local(name);
663708
let default_expr = self.synth(default_expr);
664709
self.pop_local();
665710

‎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)