catlog/tt/
batch.rs

1//! Batch elaboration for doublett
2use std::cell::{Ref, RefCell, RefMut};
3use std::fmt::Write;
4use std::ops::DerefMut;
5use std::time::{Duration, Instant};
6use std::{fs, io};
7
8use crate::tt::*;
9use crate::zero::NameSegment;
10
11use fnotation::parser::Prec;
12use fnotation::{FNtnTop, ParseConfig};
13use scopeguard::guard;
14use tattle::display::SourceInfo;
15use tattle::{Reporter, declare_error};
16use text_elab::*;
17use toplevel::*;
18
19const PARSE_CONFIG: ParseConfig = ParseConfig::new(
20    &[
21        (":", Prec::nonassoc(20)),
22        (":=", Prec::nonassoc(10)),
23        ("&", Prec::lassoc(40)),
24        ("*", Prec::lassoc(60)),
25    ],
26    &[":", ":=", "&", "Unit", "Id", "*"],
27    &["type", "def", "syn", "chk", "norm", "generate", "set_theory"],
28);
29
30declare_error!(TOP_ERROR, "top", "an error at the top-level");
31
32/// An enum to configure the output of batch processing
33pub enum BatchOutput {
34    /// Snapshot mode: save to string
35    Snapshot(RefCell<String>),
36    /// Interactive mode: print to console
37    Interactive,
38}
39
40impl BatchOutput {
41    fn report(&self, reporter: &Reporter, source_info: &SourceInfo) {
42        match self {
43            BatchOutput::Snapshot(out) => source_info
44                .extract_report_to(
45                    RefMut::deref_mut(&mut out.borrow_mut()),
46                    reporter.clone(),
47                    tattle::display::DisplayOptions::String,
48                )
49                .unwrap(),
50            BatchOutput::Interactive => {
51                source_info
52                    .extract_report_to_io(
53                        &mut io::stdout(),
54                        reporter.clone(),
55                        tattle::display::DisplayOptions::Terminal,
56                    )
57                    .unwrap();
58            }
59        }
60    }
61
62    fn log_input(&self, src: &str, decl: &FNtnTop) {
63        match self {
64            BatchOutput::Snapshot(out) => {
65                writeln!(out.borrow_mut(), "{}", decl.loc.slice(src)).unwrap();
66            }
67            BatchOutput::Interactive => {}
68        }
69    }
70
71    fn declared(&self, name: NameSegment) {
72        match self {
73            BatchOutput::Snapshot(out) => {
74                writeln!(out.borrow_mut(), "#/ declared: {}", name).unwrap();
75            }
76            BatchOutput::Interactive => {}
77        }
78    }
79
80    fn got_result(&self, result: &str) {
81        match self {
82            BatchOutput::Snapshot(out) => {
83                writeln!(out.borrow_mut(), "#/ result: {}", result).unwrap();
84            }
85            BatchOutput::Interactive => {
86                println!("{}", result);
87            }
88        }
89    }
90
91    fn display_errors(&self, should_fail: bool, reporter: &Reporter, source_info: &SourceInfo) {
92        match self {
93            BatchOutput::Snapshot(out) => {
94                let mut out = out.borrow_mut();
95                if reporter.errored() {
96                    if should_fail {
97                        writeln!(out, "#/ expected errors:").unwrap();
98                    } else {
99                        writeln!(out, "#/ unexpected errors:").unwrap();
100                    }
101                    let mut errors = String::new();
102                    source_info
103                        .extract_report_to(
104                            &mut errors,
105                            reporter.clone(),
106                            tattle::display::DisplayOptions::String,
107                        )
108                        .unwrap();
109                    for l in errors.lines() {
110                        writeln!(out, "#/ {l}").unwrap();
111                    }
112                }
113                writeln!(out).unwrap();
114            }
115            BatchOutput::Interactive => {
116                if should_fail {
117                    reporter.poll();
118                } else {
119                    self.report(reporter, source_info);
120                }
121            }
122        }
123    }
124
125    fn record_time(&self, path: &str, elapsed_t: Duration) {
126        match self {
127            BatchOutput::Snapshot(_) => {}
128            BatchOutput::Interactive => {
129                println!(
130                    "finished elaborating {} in {}ms",
131                    path,
132                    elapsed_t.as_micros() as f64 / 1000.0
133                );
134            }
135        }
136    }
137
138    #[allow(unused)]
139    /// Get the result of a snapshot test
140    pub fn result<'a>(&'a self) -> Ref<'a, String> {
141        match self {
142            BatchOutput::Snapshot(out) => out.borrow(),
143            _ => panic!("cannot get result of interactive session"),
144        }
145    }
146}
147
148/// Read from path and elaborate
149pub fn run(path: &str, output: &BatchOutput) -> io::Result<bool> {
150    let src = match fs::read_to_string(path) {
151        Ok(s) => s,
152        Err(e) => {
153            eprintln!("Could not read {}: {}", &path, e);
154            return Ok(false);
155        }
156    };
157    elaborate(&src, path, output)
158}
159
160/// Run the doublett elaborator in batch mode
161pub fn elaborate(src: &str, path: &str, output: &BatchOutput) -> io::Result<bool> {
162    let reporter = Reporter::new();
163    let source_info = SourceInfo::new(Some(path), src);
164    let start_t = Instant::now();
165    let _unwind_guard = guard((), |_| {
166        output.report(&reporter, &source_info);
167    });
168    let mut succeeded = true;
169    let _ = PARSE_CONFIG.with_parsed_top(src, reporter.clone(), |topntns| {
170        let mut toplevel = Toplevel::new(std_theories());
171        let mut topelab = TopElaborator::new(reporter.clone());
172        for topntn in topntns.iter() {
173            output.log_input(src, topntn);
174            let mut should_fail = false;
175            for annot in topntn.annotations {
176                // We allow single_match here because in the future we might want
177                // more annotations
178                #[allow(clippy::single_match)]
179                match annot.ast0() {
180                    fnotation::Var("should_fail") => {
181                        should_fail = true;
182                    }
183                    _ => {}
184                }
185            }
186            if let Some(d) = topelab.elab(&toplevel, topntn) {
187                if should_fail {
188                    reporter.error(
189                        topntn.loc,
190                        TOP_ERROR,
191                        "expected a failure to elaborate".to_string(),
192                    );
193                } else {
194                    match d {
195                        TopElabResult::Declaration(name_segment, top_decl) => {
196                            toplevel.declarations.insert(name_segment, top_decl);
197                            output.declared(name_segment);
198                        }
199                        TopElabResult::Output(s) => {
200                            output.got_result(&s);
201                        }
202                    }
203                }
204            } else if !should_fail {
205                succeeded = false;
206            }
207            output.display_errors(should_fail, &reporter, &source_info);
208        }
209        Some(())
210    });
211    output.record_time(path, Instant::now() - start_t);
212    Ok(succeeded)
213}
214
215#[test]
216fn snapshot_examples() {
217    use similar::{ChangeTag, TextDiff};
218    let mut succeeded = true;
219    for f in fs::read_dir("examples").unwrap() {
220        let Ok(f) = f else {
221            continue;
222        };
223        let os_fname = f.file_name();
224        let fname = os_fname.to_str().unwrap();
225        if !fname.ends_with(".dbltt") {
226            continue;
227        }
228        let output = BatchOutput::Snapshot(RefCell::new(String::new()));
229        succeeded = run(f.path().to_str().unwrap(), &output).unwrap() && succeeded;
230        let golden_path = format!("examples/{}.snapshot", fname);
231        if matches!(std::env::var("UPDATE_SNAPSHOT"), Ok(s) if &s == "1") {
232            fs::write(&golden_path, output.result().as_str()).unwrap();
233        } else {
234            let golden = fs::read_to_string(&golden_path).unwrap_or_default();
235            let result = output.result();
236            let result_str = result.as_str();
237            if &golden != result_str {
238                succeeded = false;
239                println!("failed snapshot test for examples/{fname}:");
240                let diff = TextDiff::from_lines(golden.as_str(), result_str);
241
242                for change in diff.iter_all_changes() {
243                    match change.tag() {
244                        ChangeTag::Delete => {
245                            print!("- {}", change);
246                        }
247                        ChangeTag::Insert => {
248                            print!("+ {}", change);
249                        }
250                        ChangeTag::Equal => {}
251                    };
252                }
253            }
254        }
255    }
256    assert!(succeeded);
257}
catlog/tt/batch.rs

catlog/tt/
batch.rs
