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 : Nat → Nat 41e73685ebSopenharmony_ci 42e73685ebSopenharmony_ci {-# BUILTIN NATRAL Nat #-} 43e73685ebSopenharmony_ci 44e73685ebSopenharmony_ci infixl 6 _+_ _-_ 45e73685ebSopenharmony_ci 46e73685ebSopenharmony_ci _+_ : Nat → Nat → Nat 47e73685ebSopenharmony_ci zero + n₂ = n₂ 48e73685ebSopenharmony_ci succ n₁ + n₂ = succ (n₁ + n₂) 49e73685ebSopenharmony_ci 50e73685ebSopenharmony_ci _-_ : Nat → Nat → Nat 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₁ : Nat → String 77e73685ebSopenharmony_ci fizz₁ num = 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₂ : Nat → String 84e73685ebSopenharmony_ci fizz₂ num = 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