Merge pull request #458 from brendanzab/avoid-item-names

Avoid item names

Author: brendanzab

fathom/src/surface/distillation.rs

@@ -45,6 +45,11 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
         }
     }
 
+    fn is_bound(&self, name: StringId) -> bool {
+        (self.local_names.iter()).any(|local_name| *local_name == Some(name))
+            || self.item_names.iter().any(|item_name| *item_name == name)
+    }
+
     fn local_len(&mut self) -> EnvLen {
         self.local_names.len()
     }
@@ -84,12 +89,12 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
         }
     }
 
-    /// Generate a fresh name that does not appear in `self.local_names`
+    /// Generate a fresh name that is not currently bound in the context
     fn gen_fresh_name(&mut self) -> StringId {
         let mut counter = 0;
         loop {
             let name = self.interner.borrow_mut().get_alphabetic_name(counter);
-            match self.local_names.iter().any(|symbol| *symbol == Some(name)) {
+            match self.is_bound(name) {
                 true => counter += 1,
                 false => return name,
             }
@@ -125,7 +130,7 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
                 r#type,
                 expr,
             } => {
-                let r#type = scope.to_scope(self.synth(r#type));
+                let r#type = scope.to_scope(self.check(r#type));
                 let expr = scope.to_scope(self.check(expr));
 
                 Item::Def(ItemDef {

tests/succeed/distillation/fresh-names.fathom

@@ -0,0 +1,31 @@
+//~ mode = "module"
+
+// An item to throw off fresh name generation
+def a = {};
+
+def const1 : fun (@A : _) (@B : _) -> A -> B -> A =
+  // The binders in the distilled term should use fresh names (starting with
+  // `a`, `b`, ...), avoiding the binding from the let expression and the
+  // top-level item
+  fun @_ @_ x y =>
+    // The following let bindings will force the type parameters to be
+    // referenced in the type annotation of the let expressions:
+    let x1 = x;
+    let y1 = y;
+
+    x;
+
+def const2 : fun (@A : _) (@B : _) -> A -> B -> A =
+  // A let expression to throw off fresh name generation
+  let b = {};
+
+  // The binders in the distilled term should use fresh names (starting with
+  // `a`, `b`, ...), avoiding the binding from the let expression and the
+  // top-level item
+  fun @_ @_ x y =>
+    // The following let bindings will force the type parameters to be
+    // referenced in the type annotation of the let expressions:
+    let x1 = x;
+    let y1 = y;
+
+    x;

tests/succeed/distillation/fresh-names.snap

@@ -0,0 +1,12 @@
+stdout = '''
+def a : () = ();
+def const1 : fun (@A : Type) (@B : Type) -> A -> B -> A =
+fun @b @c x y => let x1 : b = x;
+let y1 : c = y;
+x;
+def const2 : fun (@A : Type) (@B : Type) -> A -> B -> A = let b : () = ();
+fun @c @d x y => let x1 : c = x;
+let y1 : d = y;
+x;
+'''
+stderr = ''