1//! To run this example, execute the following command from the top level of
2//! this repository:
3//!
4//! ```sh
5//! cargo run --example term
6//! ```
7
8use codespan_reporting::diagnostic::{Diagnostic, Label};
9use codespan_reporting::files::SimpleFiles;
10use codespan_reporting::term::termcolor::StandardStream;
11use codespan_reporting::term::{self, ColorArg};
12use structopt::StructOpt;
13
14#[derive(Debug, StructOpt)]
15#[structopt(name = "emit")]
16pub struct Opts {
17    /// Configure coloring of output
18    #[structopt(
19        long = "color",
20        parse(try_from_str),
21        default_value = "auto",
22        possible_values = ColorArg::VARIANTS,
23        case_insensitive = true
24    )]
25    pub color: ColorArg,
26}
27
28fn main() -> anyhow::Result<()> {
29    let opts = Opts::from_args();
30    let mut files = SimpleFiles::new();
31
32    let file_id1 = files.add(
33        "Data/Nat.fun",
34        unindent::unindent(
35            "
36                module Data.Nat where
37
38                data Nat : Type where
39                    zero : Nat
40                    succ : Nat → Nat
41
42                {-# BUILTIN NATRAL Nat #-}
43
44                infixl 6 _+_ _-_
45
46                _+_ : Nat → Nat → Nat
47                zero    + n₂ = n₂
48                succ n₁ + n₂ = succ (n₁ + n₂)
49
50                _-_ : Nat → Nat → Nat
51                n₁      - zero    = n₁
52                zero    - succ n₂ = zero
53                succ n₁ - succ n₂ = n₁ - n₂
54            ",
55        ),
56    );
57
58    let file_id2 = files.add(
59        "Test.fun",
60        unindent::unindent(
61            r#"
62                module Test where
63
64                _ : Nat
65                _ = 123 + "hello"
66            "#,
67        ),
68    );
69
70    let file_id3 = files.add(
71        "FizzBuzz.fun",
72        unindent::unindent(
73            r#"
74                module FizzBuzz where
75
76                fizz₁ : Nat → String
77                fizz₁ num = case (mod num 5) (mod num 3) of
78                    0 0 => "FizzBuzz"
79                    0 _ => "Fizz"
80                    _ 0 => "Buzz"
81                    _ _ => num
82
83                fizz₂ : Nat → String
84                fizz₂ num =
85                    case (mod num 5) (mod num 3) of
86                        0 0 => "FizzBuzz"
87                        0 _ => "Fizz"
88                        _ 0 => "Buzz"
89                        _ _ => num
90            "#,
91        ),
92    );
93
94    let diagnostics = [
95        // Unknown builtin error
96        Diagnostic::error()
97            .with_message("unknown builtin: `NATRAL`")
98            .with_labels(vec![
99                Label::primary(file_id1, 96..102).with_message("unknown builtin")
100            ])
101            .with_notes(vec![
102                "there is a builtin with a similar name: `NATURAL`".to_owned()
103            ]),
104        // Unused parameter warning
105        Diagnostic::warning()
106            .with_message("unused parameter pattern: `n₂`")
107            .with_labels(vec![
108                Label::primary(file_id1, 285..289).with_message("unused parameter")
109            ])
110            .with_notes(vec!["consider using a wildcard pattern: `_`".to_owned()]),
111        // Unexpected type error
112        Diagnostic::error()
113            .with_message("unexpected type in application of `_+_`")
114            .with_code("E0001")
115            .with_labels(vec![
116                Label::primary(file_id2, 37..44).with_message("expected `Nat`, found `String`"),
117                Label::secondary(file_id1, 130..155)
118                    .with_message("based on the definition of `_+_`"),
119            ])
120            .with_notes(vec![unindent::unindent(
121                "
122                    expected type `Nat`
123                       found type `String`
124                ",
125            )]),
126        // Incompatible match clause error
127        Diagnostic::error()
128            .with_message("`case` clauses have incompatible types")
129            .with_code("E0308")
130            .with_labels(vec![
131                Label::primary(file_id3, 163..166).with_message("expected `String`, found `Nat`"),
132                Label::secondary(file_id3, 62..166)
133                    .with_message("`case` clauses have incompatible types"),
134                Label::secondary(file_id3, 41..47)
135                    .with_message("expected type `String` found here"),
136            ])
137            .with_notes(vec![unindent::unindent(
138                "
139                    expected type `String`
140                       found type `Nat`
141                ",
142            )]),
143        // Incompatible match clause error
144        Diagnostic::error()
145            .with_message("`case` clauses have incompatible types")
146            .with_code("E0308")
147            .with_labels(vec![
148                Label::primary(file_id3, 328..331).with_message("expected `String`, found `Nat`"),
149                Label::secondary(file_id3, 211..331)
150                    .with_message("`case` clauses have incompatible types"),
151                Label::secondary(file_id3, 258..268)
152                    .with_message("this is found to be of type `String`"),
153                Label::secondary(file_id3, 284..290)
154                    .with_message("this is found to be of type `String`"),
155                Label::secondary(file_id3, 306..312)
156                    .with_message("this is found to be of type `String`"),
157                Label::secondary(file_id3, 186..192)
158                    .with_message("expected type `String` found here"),
159            ])
160            .with_notes(vec![unindent::unindent(
161                "
162                    expected type `String`
163                       found type `Nat`
164                ",
165            )]),
166    ];
167
168    let writer = StandardStream::stderr(opts.color.into());
169    let config = codespan_reporting::term::Config::default();
170    for diagnostic in &diagnostics {
171        term::emit(&mut writer.lock(), &config, &files, &diagnostic)?;
172    }
173
174    Ok(())
175}
176