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