1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
|
//! 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(())
}
|
