| //! To run this example, execute the following command from the top level of |
| //! this repository: |
| //! |
| //! ```sh |
| //! cargo run --example term |
| //! ``` |
| |
| use codespan_reporting::diagnostic::{Diagnostic, Label}; |
| use codespan_reporting::files::SimpleFiles; |
| use codespan_reporting::term::termcolor::StandardStream; |
| use codespan_reporting::term::{self, ColorArg}; |
| use structopt::StructOpt; |
| |
| #[derive(Debug, StructOpt)] |
| #[structopt(name = "emit")] |
| pub struct Opts { |
| /// Configure coloring of output |
| #[structopt( |
| long = "color", |
| parse(try_from_str), |
| default_value = "auto", |
| possible_values = ColorArg::VARIANTS, |
| case_insensitive = true |
| )] |
| pub color: ColorArg, |
| } |
| |
| fn main() -> anyhow::Result<()> { |
| let opts = Opts::from_args(); |
| let mut files = SimpleFiles::new(); |
| |
| let file_id1 = files.add( |
| "Data/Nat.fun", |
| unindent::unindent( |
| " |
| module Data.Nat where |
| |
| data Nat : Type where |
| zero : Nat |
| succ : Nat → Nat |
| |
| {-# BUILTIN NATRAL Nat #-} |
| |
| infixl 6 _+_ _-_ |
| |
| _+_ : Nat → Nat → Nat |
| zero + n₂ = n₂ |
| succ n₁ + n₂ = succ (n₁ + n₂) |
| |
| _-_ : Nat → Nat → Nat |
| n₁ - zero = n₁ |
| zero - succ n₂ = zero |
| succ n₁ - succ n₂ = n₁ - n₂ |
| ", |
| ), |
| ); |
| |
| let file_id2 = files.add( |
| "Test.fun", |
| unindent::unindent( |
| r#" |
| module Test where |
| |
| _ : Nat |
| _ = 123 + "hello" |
| "#, |
| ), |
| ); |
| |
| let file_id3 = files.add( |
| "FizzBuzz.fun", |
| unindent::unindent( |
| r#" |
| module FizzBuzz where |
| |
| fizz₁ : Nat → String |
| fizz₁ num = case (mod num 5) (mod num 3) of |
| 0 0 => "FizzBuzz" |
| 0 _ => "Fizz" |
| _ 0 => "Buzz" |
| _ _ => num |
| |
| fizz₂ : Nat → String |
| fizz₂ num = |
| case (mod num 5) (mod num 3) of |
| 0 0 => "FizzBuzz" |
| 0 _ => "Fizz" |
| _ 0 => "Buzz" |
| _ _ => num |
| "#, |
| ), |
| ); |
| |
| let diagnostics = [ |
| // Unknown builtin error |
| Diagnostic::error() |
| .with_message("unknown builtin: `NATRAL`") |
| .with_labels(vec![ |
| Label::primary(file_id1, 96..102).with_message("unknown builtin") |
| ]) |
| .with_notes(vec![ |
| "there is a builtin with a similar name: `NATURAL`".to_owned() |
| ]), |
| // Unused parameter warning |
| Diagnostic::warning() |
| .with_message("unused parameter pattern: `n₂`") |
| .with_labels(vec![ |
| Label::primary(file_id1, 285..289).with_message("unused parameter") |
| ]) |
| .with_notes(vec!["consider using a wildcard pattern: `_`".to_owned()]), |
| // Unexpected type error |
| Diagnostic::error() |
| .with_message("unexpected type in application of `_+_`") |
| .with_code("E0001") |
| .with_labels(vec![ |
| Label::primary(file_id2, 37..44).with_message("expected `Nat`, found `String`"), |
| Label::secondary(file_id1, 130..155) |
| .with_message("based on the definition of `_+_`"), |
| ]) |
| .with_notes(vec![unindent::unindent( |
| " |
| expected type `Nat` |
| found type `String` |
| ", |
| )]), |
| // Incompatible match clause error |
| Diagnostic::error() |
| .with_message("`case` clauses have incompatible types") |
| .with_code("E0308") |
| .with_labels(vec![ |
| Label::primary(file_id3, 163..166).with_message("expected `String`, found `Nat`"), |
| Label::secondary(file_id3, 62..166) |
| .with_message("`case` clauses have incompatible types"), |
| Label::secondary(file_id3, 41..47) |
| .with_message("expected type `String` found here"), |
| ]) |
| .with_notes(vec![unindent::unindent( |
| " |
| expected type `String` |
| found type `Nat` |
| ", |
| )]), |
| // Incompatible match clause error |
| Diagnostic::error() |
| .with_message("`case` clauses have incompatible types") |
| .with_code("E0308") |
| .with_labels(vec![ |
| Label::primary(file_id3, 328..331).with_message("expected `String`, found `Nat`"), |
| Label::secondary(file_id3, 211..331) |
| .with_message("`case` clauses have incompatible types"), |
| Label::secondary(file_id3, 258..268) |
| .with_message("this is found to be of type `String`"), |
| Label::secondary(file_id3, 284..290) |
| .with_message("this is found to be of type `String`"), |
| Label::secondary(file_id3, 306..312) |
| .with_message("this is found to be of type `String`"), |
| Label::secondary(file_id3, 186..192) |
| .with_message("expected type `String` found here"), |
| ]) |
| .with_notes(vec![unindent::unindent( |
| " |
| expected type `String` |
| found type `Nat` |
| ", |
| )]), |
| ]; |
| |
| let writer = StandardStream::stderr(opts.color.into()); |
| let config = codespan_reporting::term::Config::default(); |
| for diagnostic in &diagnostics { |
| term::emit(&mut writer.lock(), &config, &files, &diagnostic)?; |
| } |
| |
| Ok(()) |
| } |