Merge pull request #386 from brendanzab/cleanups-to-arrow-distillation

Cleanups to arrow distillation

Author: brendanzab

fathom/src/core.rs

@@ -215,6 +215,53 @@ impl<'arena> Term<'arena> {
             | Term::ConstMatch(span, _, _, _) => *span,
         }
     }
+
+    /// Returns `true` if the term contains an occurrence of the rigid variable.
+    pub fn binds_rigid_var(&self, mut var: LocalVar) -> bool {
+        match self {
+            Term::RigidVar(_, v) => *v == var,
+            Term::ItemVar(_, _)
+            | Term::FlexibleVar(_, _)
+            | Term::FlexibleInsertion(_, _, _)
+            | Term::Universe(_)
+            | Term::Prim(_, _)
+            | Term::ConstLit(_, _) => false,
+
+            Term::Ann(_, expr, r#type) => expr.binds_rigid_var(var) || r#type.binds_rigid_var(var),
+            Term::Let(_, _, def_type, def_expr, output_expr) => {
+                def_type.binds_rigid_var(var)
+                    || def_expr.binds_rigid_var(var)
+                    || output_expr.binds_rigid_var(var.prev())
+            }
+            Term::FunType(_, _, input_type, output_type) => {
+                input_type.binds_rigid_var(var) || output_type.binds_rigid_var(var.prev())
+            }
+            Term::FunLit(_, _, output_expr) => output_expr.binds_rigid_var(var.prev()),
+            Term::FunApp(_, head_expr, input_expr) => {
+                head_expr.binds_rigid_var(var) || input_expr.binds_rigid_var(var)
+            }
+            Term::RecordType(_, _, terms)
+            | Term::RecordLit(_, _, terms)
+            | Term::FormatRecord(_, _, terms)
+            | Term::FormatOverlap(_, _, terms) => terms.iter().any(|term| {
+                let result = term.binds_rigid_var(var);
+                var = var.prev();
+                result
+            }),
+            Term::RecordProj(_, head_expr, _) => head_expr.binds_rigid_var(var),
+            Term::ArrayLit(_, elem_exprs) => {
+                elem_exprs.iter().any(|term| term.binds_rigid_var(var))
+            }
+            Term::FormatCond(_, _, format, pred) => {
+                format.binds_rigid_var(var) || pred.binds_rigid_var(var.prev())
+            }
+            Term::ConstMatch(_, scrut, branches, default_expr) => {
+                scrut.binds_rigid_var(var)
+                    || branches.iter().any(|(_, term)| term.binds_rigid_var(var))
+                    || default_expr.map_or(false, |term| term.binds_rigid_var(var.prev()))
+            }
+        }
+    }
 }
 
 macro_rules! def_prims {
@@ -623,45 +670,3 @@ mod tests {
         assert!(!std::mem::needs_drop::<Term<'_>>());
     }
 }
-
-impl<'arena> Term<'arena> {
-    pub fn contains_free(&self, mut var: LocalVar) -> bool {
-        match self {
-            Term::RigidVar(_, v) => *v == var,
-            Term::ItemVar(_, _)
-            | Term::FlexibleVar(_, _)
-            | Term::FlexibleInsertion(_, _, _)
-            | Term::Universe(_)
-            | Term::Prim(_, _)
-            | Term::ConstLit(_, _) => false,
-
-            Term::Ann(_, term, r#type) => term.contains_free(var) || r#type.contains_free(var),
-            Term::Let(_, _, r#type, def, body) => {
-                r#type.contains_free(var)
-                    || def.contains_free(var)
-                    || body.contains_free(var.prev())
-            }
-            Term::FunType(_, _, input_type, output_type) => {
-                input_type.contains_free(var) || output_type.contains_free(var.prev())
-            }
-            Term::FunLit(_, _, body) => body.contains_free(var.prev()),
-            Term::FunApp(_, head, arg) => head.contains_free(var) || arg.contains_free(var),
-            Term::RecordType(_, _, terms)
-            | Term::RecordLit(_, _, terms)
-            | Term::FormatRecord(_, _, terms)
-            | Term::FormatOverlap(_, _, terms) => terms.iter().any(|term| {
-                let result = term.contains_free(var);
-                var = var.prev();
-                result
-            }),
-            Term::RecordProj(_, term, _) => term.contains_free(var),
-            Term::ArrayLit(_, terms) => terms.iter().any(|term| term.contains_free(var)),
-            Term::FormatCond(_, _, t1, t2) => t1.contains_free(var) || t2.contains_free(var.prev()),
-            Term::ConstMatch(_, scrut, branches, default) => {
-                scrut.contains_free(var)
-                    || branches.iter().any(|(_, term)| term.contains_free(var))
-                    || default.map_or(false, |term| term.contains_free(var.prev()))
-            }
-        }
-    }
-}

fathom/src/surface/distillation.rs

@@ -369,8 +369,11 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
                 )
             }
             core::Term::Universe(_span) => Term::Universe(()),
+
+            // Use arrow sugar if the the input binding is not referenced in the
+            // output type.
             core::Term::FunType(_span, _, input_type, output_type)
-                if !output_type.contains_free(LocalVar::last()) =>
+                if !output_type.binds_rigid_var(LocalVar::last()) =>
             {
                 let input_type = self.check(input_type);
 
@@ -384,6 +387,7 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
                     self.scope.to_scope(output_type),
                 )
             }
+            // Otherwise distill to a function type with an explicit parameter.
             core::Term::FunType(_span, input_name, input_type, output_type) => {
                 let input_type = self.check(input_type);
 
@@ -398,6 +402,7 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
                     self.scope.to_scope(output_type),
                 )
             }
+
             core::Term::FunLit(_span, input_name, output_expr) => {
                 let input_name = self.push_rigid(*input_name);
                 let output_expr = self.synth(output_expr);