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
8 use codespan_reporting::diagnostic::{Diagnostic, Label};
9 use codespan_reporting::files::SimpleFiles;
10 use codespan_reporting::term::termcolor::StandardStream;
11 use codespan_reporting::term::{self, ColorArg};
12 use structopt::StructOpt;
13
14 #[derive(Debug, StructOpt)]
15 #[structopt(name = "emit")]
16 pub 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
main() -> anyhow::Result<()>28 fn 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