catlog/tt/
batch.rs

1//! Batch elaboration for DoubleTT.
2
3use std::cell::{Ref, RefCell, RefMut};
4use std::fmt::Write;
5use std::ops::DerefMut;
6use std::time::{Duration, Instant};
7use std::{fs, io};
8
9use fnotation::FNtnTop;
10use scopeguard::guard;
11use tattle::display::SourceInfo;
12use tattle::{Reporter, declare_error};
13
14use super::{
15    modelgen::{ModelInstance, instance_from_def},
16    text_elab::*,
17    theory::std_theories,
18    toplevel::*,
19};
20use crate::dbl::discrete::DiscreteInstanceTerm;
21use crate::dbl::modal::{
22    ModalInstanceBase, ModalInstanceTerm, ModalMor, ModalOb, modal_mor_as_identity,
23};
24use crate::dbl::model_instance::{DblModelInstance, HasInstanceTerm};
25use crate::one::path::Path;
26use crate::zero::{NameSegment, Namespace};
27
28declare_error!(TOP_ERROR, "top", "an error at the top-level");
29
30/// An enum to configure the output of batch processing.
31pub enum BatchOutput {
32    /// Snapshot mode: save to string.
33    Snapshot(RefCell<String>),
34    /// Interactive mode: print to console.
35    Interactive,
36}
37
38impl BatchOutput {
39    fn report(&self, reporter: &Reporter, source_info: &SourceInfo) {
40        match self {
41            BatchOutput::Snapshot(out) => source_info
42                .extract_report_to(
43                    RefMut::deref_mut(&mut out.borrow_mut()),
44                    reporter.clone(),
45                    tattle::display::DisplayOptions::String,
46                )
47                .unwrap(),
48            BatchOutput::Interactive => {
49                source_info
50                    .extract_report_to_io(
51                        &mut io::stdout(),
52                        reporter.clone(),
53                        tattle::display::DisplayOptions::Terminal,
54                    )
55                    .unwrap();
56            }
57        }
58    }
59
60    fn log_input(&self, src: &str, decl: &FNtnTop) {
61        match self {
62            BatchOutput::Snapshot(out) => {
63                writeln!(out.borrow_mut(), "{}", decl.loc.slice(src)).unwrap();
64            }
65            BatchOutput::Interactive => {}
66        }
67    }
68
69    fn declared(&self, name: NameSegment) {
70        match self {
71            BatchOutput::Snapshot(out) => {
72                writeln!(out.borrow_mut(), "#/ declared: {}", name).unwrap();
73            }
74            BatchOutput::Interactive => {}
75        }
76    }
77
78    fn instance_summary(&self, instance: &ModelInstance, ns: &Namespace) {
79        if let BatchOutput::Snapshot(out) = self {
80            let mut out = out.borrow_mut();
81            match instance {
82                ModelInstance::Discrete(instance) => write_instance_summary(
83                    &mut out,
84                    instance,
85                    ns,
86                    |fiber| ns.label_string(fiber),
87                    |tm| format_instance_term(tm, ns),
88                ),
89                ModelInstance::ModalUnital(instance) => write_instance_summary(
90                    &mut out,
91                    instance,
92                    ns,
93                    |ob| format_modal_ob(ob, ns),
94                    |tm| format_modal_instance_term(tm, ns),
95                ),
96                ModelInstance::ModalNonUnital(instance) => write_instance_summary(
97                    &mut out,
98                    instance,
99                    ns,
100                    |ob| format_modal_ob(ob, ns),
101                    |tm| format_modal_instance_term(tm, ns),
102                ),
103            }
104        }
105    }
106
107    fn instance_error(&self, msg: &str) {
108        if let BatchOutput::Snapshot(out) = self {
109            writeln!(out.borrow_mut(), "#/ instance generation failed: {msg}").unwrap();
110        }
111    }
112
113    fn got_result(&self, result: &str) {
114        match self {
115            BatchOutput::Snapshot(out) => {
116                writeln!(out.borrow_mut(), "#/ result: {}", result).unwrap();
117            }
118            BatchOutput::Interactive => {
119                println!("{}", result);
120            }
121        }
122    }
123
124    fn display_errors(&self, should_fail: bool, reporter: &Reporter, source_info: &SourceInfo) {
125        match self {
126            BatchOutput::Snapshot(out) => {
127                let mut out = out.borrow_mut();
128                if reporter.errored() {
129                    if should_fail {
130                        writeln!(out, "#/ expected errors:").unwrap();
131                    } else {
132                        writeln!(out, "#/ unexpected errors:").unwrap();
133                    }
134                    let mut errors = String::new();
135                    source_info
136                        .extract_report_to(
137                            &mut errors,
138                            reporter.clone(),
139                            tattle::display::DisplayOptions::String,
140                        )
141                        .unwrap();
142                    for l in errors.lines() {
143                        writeln!(out, "#/ {l}").unwrap();
144                    }
145                }
146                writeln!(out).unwrap();
147            }
148            BatchOutput::Interactive => {
149                if should_fail {
150                    reporter.poll();
151                } else {
152                    self.report(reporter, source_info);
153                }
154            }
155        }
156    }
157
158    fn record_time(&self, path: &str, elapsed_t: Duration) {
159        match self {
160            BatchOutput::Snapshot(_) => {}
161            BatchOutput::Interactive => {
162                println!(
163                    "finished elaborating {} in {}ms",
164                    path,
165                    elapsed_t.as_micros() as f64 / 1000.0
166                );
167            }
168        }
169    }
170
171    /// Get the result of a snapshot test.
172    pub fn result<'a>(&'a self) -> Ref<'a, String> {
173        match self {
174            BatchOutput::Snapshot(out) => out.borrow(),
175            _ => panic!("cannot get result of interactive session"),
176        }
177    }
178}
179
180/// Read from path and elaborate.
181pub fn run(path: &str, output: &BatchOutput) -> io::Result<bool> {
182    let src = match fs::read_to_string(path) {
183        Ok(s) => s,
184        Err(e) => {
185            eprintln!("Could not read {}: {}", &path, e);
186            return Ok(false);
187        }
188    };
189    elaborate(&src, path, output)
190}
191
192/// Run the DoubleTT elaborator in batch mode.
193pub fn elaborate(src: &str, path: &str, output: &BatchOutput) -> io::Result<bool> {
194    let reporter = Reporter::new();
195    let source_info = SourceInfo::new(Some(path), src);
196    let start_t = Instant::now();
197    let _unwind_guard = guard((), |_| {
198        output.report(&reporter, &source_info);
199    });
200    let mut succeeded = true;
201    let _ = TT_PARSE_CONFIG.with_parsed_top(src, reporter.clone(), |topntns| {
202        let mut toplevel = Toplevel::new(std_theories());
203        let mut topelab = TopElaborator::new(reporter.clone());
204        for topntn in topntns.iter() {
205            output.log_input(src, topntn);
206            let mut should_fail = false;
207            for annot in topntn.annotations {
208                // We allow single_match here because in the future we might want
209                // more annotations
210                #[allow(clippy::single_match)]
211                match annot.ast0() {
212                    fnotation::Var("should_fail") => {
213                        should_fail = true;
214                    }
215                    _ => {}
216                }
217            }
218            if let Some(d) = topelab.elab(&toplevel, topntn) {
219                if should_fail && !reporter.errored() {
220                    reporter.error(
221                        topntn.loc,
222                        TOP_ERROR,
223                        "expected a failure to elaborate".to_string(),
224                    );
225                } else {
226                    match d {
227                        TopElabResult::Declaration(name_segment, top_decl) => {
228                            let is_instance = matches!(&top_decl, TopDecl::Instance(_));
229                            toplevel.declarations.insert(name_segment, top_decl);
230                            output.declared(name_segment);
231                            if is_instance
232                                && let Some(TopDecl::Instance(def)) =
233                                    toplevel.declarations.get(&name_segment)
234                            {
235                                match instance_from_def(&toplevel, &def.theory.definition, def) {
236                                    Ok((instance, ns)) => output.instance_summary(&instance, &ns),
237                                    Err(msg) => output.instance_error(&msg),
238                                }
239                            }
240                        }
241                        TopElabResult::Output(s) => {
242                            output.got_result(&s);
243                        }
244                    }
245                }
246            } else if !should_fail {
247                succeeded = false;
248            }
249            output.display_errors(should_fail, &reporter, &source_info);
250        }
251        Some(())
252    });
253    output.record_time(path, Instant::now() - start_t);
254    Ok(succeeded)
255}
256
257#[test]
258fn snapshot_examples() {
259    use similar::{ChangeTag, TextDiff};
260    let mut succeeded = true;
261    let base_path = std::path::Path::new("examples/tt/text");
262    for f in fs::read_dir(base_path).unwrap() {
263        let Ok(f) = f else {
264            continue;
265        };
266        let os_fname = f.file_name();
267        let fname = os_fname.to_str().unwrap();
268        if !fname.ends_with(".dbltt") {
269            continue;
270        }
271        let output = BatchOutput::Snapshot(RefCell::new(String::new()));
272        succeeded = run(f.path().to_str().unwrap(), &output).unwrap() && succeeded;
273        let golden_path = base_path.join(format!("{fname}.snapshot"));
274        if matches!(std::env::var("UPDATE_SNAPSHOT"), Ok(s) if &s == "1") {
275            fs::write(&golden_path, output.result().as_str()).unwrap();
276        } else {
277            let golden = fs::read_to_string(&golden_path).unwrap_or_default();
278            let result = output.result();
279            let result_str = result.as_str();
280            if golden != result_str {
281                succeeded = false;
282                println!("failed snapshot test for {}:", base_path.join(fname).display());
283                let diff = TextDiff::from_lines(golden.as_str(), result_str);
284
285                for change in diff.iter_all_changes() {
286                    match change.tag() {
287                        ChangeTag::Delete => {
288                            print!("- {}", change);
289                        }
290                        ChangeTag::Insert => {
291                            print!("+ {}", change);
292                        }
293                        ChangeTag::Equal => {}
294                    };
295                }
296            }
297        }
298    }
299    assert!(succeeded);
300}
301
302/// Render an instance term for snapshot output as `f(g(base))`, with
303/// `f` the outermost (last-applied) model morphism in the path.
304pub(in crate::tt) fn format_instance_term(tm: &DiscreteInstanceTerm, ns: &Namespace) -> String {
305    let mut s = ns.label_string(&tm.base);
306    if let Path::Seq(edges) = &tm.path {
307        for mor in edges.iter() {
308            s = format!("{}({})", ns.label_string(mor), s);
309        }
310    }
311    s
312}
313
314/// Writes the generators and equations of an instance, using the given
315/// per-doctrine formatters for fibers and equation terms.
316pub(in crate::tt) fn write_instance_summary<M: HasInstanceTerm>(
317    out: &mut String,
318    instance: &DblModelInstance<M>,
319    ns: &Namespace,
320    fmt_ob: impl Fn(&M::Ob) -> String,
321    fmt_term: impl Fn(&M::Term) -> String,
322) {
323    let gens: Vec<_> = instance.generators().collect();
324    let eqns: Vec<_> = instance.equations().collect();
325    if gens.is_empty() && eqns.is_empty() {
326        writeln!(out, "#/ instance has no generators or equations").unwrap();
327        return;
328    }
329    if !gens.is_empty() {
330        writeln!(out, "#/ instance generators:").unwrap();
331        for (name, fiber) in &gens {
332            writeln!(out, "#/   {} : {}", ns.label_string(name), fmt_ob(fiber)).unwrap();
333        }
334    }
335    if !eqns.is_empty() {
336        writeln!(out, "#/ instance equations:").unwrap();
337        for (lhs, rhs) in &eqns {
338            writeln!(out, "#/   {} == {}", fmt_term(lhs), fmt_term(rhs)).unwrap();
339        }
340    }
341}
342
343/// Renders a modal object for snapshot output: generators by name, object
344/// operations as `op(inner)`, and lists as `[a, b, …]`.
345pub(in crate::tt) fn format_modal_ob(ob: &ModalOb, ns: &Namespace) -> String {
346    match ob {
347        ModalOb::Generator(name) => ns.label_string(name),
348        ModalOb::App(inner, op) => format!("{op}({})", format_modal_ob(inner, ns)),
349        ModalOb::List(_, obs) => {
350            let inner: Vec<_> = obs.iter().map(|ob| format_modal_ob(ob, ns)).collect();
351            format!("[{}]", inner.join(", "))
352        }
353    }
354}
355
356/// An applicative rendering of a modal instance term, reconstructed from its
357/// flat `(mor, base)` normal form so it prints back in surface syntax.
358enum Rendered {
359    Gen(String),
360    App(String, Box<Rendered>),
361    ObApp(String, Box<Rendered>),
362    List(Vec<Rendered>),
363}
364
365impl Rendered {
366    fn render(&self) -> String {
367        match self {
368            Rendered::Gen(name) => name.clone(),
369            Rendered::App(name, inner) => format!("{name}({})", inner.render()),
370            Rendered::ObApp(op, inner) => format!("@{op} {}", inner.render()),
371            Rendered::List(items) => {
372                let inner: Vec<_> = items.iter().map(Rendered::render).collect();
373                format!("[{}]", inner.join(", "))
374            }
375        }
376    }
377}
378
379/// Renders a modal instance term as e.g. `op([x, unit([])])`, re-interleaving
380/// the morphism with its base (the inverse of the flattening done during
381/// extraction).
382pub(in crate::tt) fn format_modal_instance_term(tm: &ModalInstanceTerm, ns: &Namespace) -> String {
383    apply_mor(&tm.mor, base_rendered(&tm.base, ns), ns).render()
384}
385
386fn base_rendered(base: &ModalInstanceBase, ns: &Namespace) -> Rendered {
387    match base {
388        ModalInstanceBase::Generator(name) => Rendered::Gen(ns.label_string(name)),
389        ModalInstanceBase::List(_, bases) => {
390            Rendered::List(bases.iter().map(|b| base_rendered(b, ns)).collect())
391        }
392        ModalInstanceBase::ObApp(op, inner) => {
393            Rendered::ObApp(format!("{op}"), Box::new(base_rendered(inner, ns)))
394        }
395    }
396}
397
398/// Applies a model morphism to an already-rendered argument, undoing the
399/// `Composite`/`List` tupling introduced by normalization: a `Composite` path
400/// folds its morphisms outermost-last, and a list morphism zips into a list
401/// argument.
402fn apply_mor(mor: &ModalMor, arg: Rendered, ns: &Namespace) -> Rendered {
403    if modal_mor_as_identity(mor).is_some() {
404        return arg;
405    }
406    match mor {
407        ModalMor::Generator(name) => Rendered::App(ns.label_string(name), Box::new(arg)),
408        ModalMor::App(_, op) => Rendered::App(format!("{op}"), Box::new(arg)),
409        // The functorial action of an object operation: it applies to an
410        // `@op [..]` base, and the lifted morphisms act on the operation's
411        // content, so we push them inside the existing wrapper rather than
412        // adding another.
413        ModalMor::HomApp(path, _op) => match arg {
414            Rendered::ObApp(op_name, inner) => {
415                Rendered::ObApp(op_name, Box::new(apply_path(path, *inner, ns)))
416            }
417            // Should not arise: a hom operation applies to an object-op base.
418            other => other,
419        },
420        ModalMor::Composite(path) => apply_path(path, arg, ns),
421        ModalMor::List(_, mors) => match arg {
422            Rendered::List(items) if items.len() == mors.len() => {
423                Rendered::List(mors.iter().zip(items).map(|(m, a)| apply_mor(m, a, ns)).collect())
424            }
425            // Should not arise: a list morphism always applies to a list base.
426            other => other,
427        },
428    }
429}
430
431/// Applies a path of morphisms to a rendered argument, folding outermost-last
432/// (so `[m1, m2]` renders as `m2(m1(arg))`).
433fn apply_path(path: &Path<ModalOb, ModalMor>, arg: Rendered, ns: &Namespace) -> Rendered {
434    match path {
435        Path::Id(_) => arg,
436        Path::Seq(edges) => edges.iter().fold(arg, |acc, mor| apply_mor(mor, acc, ns)),
437    }
438}
catlog/tt/batch.rs

catlog/tt/
batch.rs
