Quelle  term.rs

//! 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(())
}