Merge pull request #459 from Kmeakin/pretty-metavars

Distill metavariables to named terms

Author: brendanzab

fathom/src/surface/distillation.rs

@@ -85,7 +85,7 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
     fn get_hole_name(&self, var: Level) -> Option<StringId> {
         match self.meta_sources.get_level(var)? {
             MetaSource::HoleExpr(_, name) => Some(*name),
-            _ => None,
+            _ => Some(self.interner.borrow_mut().get_or_intern(var.to_string())),
         }
     }
 

fathom/tests/source_tests.rs

@@ -39,6 +39,8 @@ impl TestMode {
 #[serde(deny_unknown_fields)]
 #[serde(rename_all = "kebab-case")]
 struct Config {
+    #[serde(default = "DEFAULT_ALLOW_ERRORS")]
+    allow_errors: bool,
     mode: Option<TestMode>,
     #[serde(default = "DEFAULT_IGNORE")]
     ignore: bool,
@@ -54,6 +56,7 @@ struct Config {
     test_normalisation: bool,
 }
 
+const DEFAULT_ALLOW_ERRORS: fn() -> bool = || false;
 const DEFAULT_IGNORE: fn() -> bool = || false;
 const DEFAULT_EXIT_CODE: fn() -> i32 = || 0;
 const DEFAULT_EXAMPLE_DATA: fn() -> Vec<String> = Vec::new;
@@ -296,6 +299,9 @@ impl<'a> TestCommand<'a> {
         let mut failures = Vec::new();
         let mut command = process::Command::from(self.command);
         command.arg(self.input_file);
+        if self.config.allow_errors {
+            command.arg("--allow-errors");
+        }
 
         match command.output() {
             Ok(output) => {

tests/fail/elaboration/unsolved/fun-literal-param-type.fathom

@@ -1,3 +1,3 @@
-//~ exit-code = 1
+//~ allow-errors = true
 
 fun a => a

tests/fail/elaboration/unsolved/fun-literal-param-type.snap

@@ -1,4 +1,6 @@
-stdout = ''
+stdout = '''
+fun a => a : ?0 -> ?0
+'''
 stderr = '''
 error: failed to infer named pattern type
   ┌─ tests/fail/elaboration/unsolved/fun-literal-param-type.fathom:3:5

tests/fail/elaboration/unsolved/fun-literal-placeholder-body-type.fathom

@@ -1,3 +1,3 @@
-//~ exit-code = 1
+//~ allow-errors = true
 
 fun (A : Type) a (b : A) => a : fun (A : Type) -> _

tests/fail/elaboration/unsolved/fun-literal-placeholder-body-type.snap

@@ -1,4 +1,6 @@
-stdout = ''
+stdout = '''
+fun A a b => a : fun (A : Type) -> ?2 A -> A -> ?2 A
+'''
 stderr = '''
 error: failed to infer named pattern type
   ┌─ tests/fail/elaboration/unsolved/fun-literal-placeholder-body-type.fathom:3:16

tests/fail/elaboration/unsolved/hole-ann.fathom

@@ -1,3 +1,3 @@
-//~ exit-code = 1
+//~ allow-errors = true
 
 ?woopsie : Type

tests/fail/elaboration/unsolved/hole-ann.snap

@@ -1,4 +1,6 @@
-stdout = ''
+stdout = '''
+?woopsie : Type
+'''
 stderr = '''
 error: failed to infer hole expression
   ┌─ tests/fail/elaboration/unsolved/hole-ann.fathom:3:1

tests/fail/elaboration/unsolved/hole.fathom

@@ -1,3 +1,3 @@
-//~ exit-code = 1
+//~ allow-errors = true
 
 ?woopsie

tests/fail/elaboration/unsolved/hole.snap

@@ -1,4 +1,6 @@
-stdout = ''
+stdout = '''
+?woopsie : ?0
+'''
 stderr = '''
 error: failed to infer hole expression
   ┌─ tests/fail/elaboration/unsolved/hole.fathom:3:1