catlog/tt/
modelgen.rs

1//! Generate catlog models from doublett types.
2
3use std::fmt;
4
5use crate::dbl::model::DiscreteDblModel;
6use crate::dbl::model::MutDblModel;
7use crate::dbl::model::{DblModel, FgDblModel};
8use crate::one::category::FgCategory;
9use crate::tt::stx::MorphismType;
10use crate::tt::{eval::*, prelude::*, toplevel::*, val::*};
11use crate::zero::QualifiedLabel;
12use crate::zero::QualifiedName;
13
14/// Generate a discrete double model from a type.
15///
16/// Precondition: `ty` must be valid in the empty context.
17pub fn generate(
18    toplevel: &Toplevel,
19    theory: &Theory,
20    ty: &TyV,
21) -> (DiscreteDblModel, HashMap<QualifiedName, QualifiedLabel>) {
22    let eval = Evaluator::new(toplevel, Env::Nil, 0);
23    let (elt, eval) = eval.bind_self(ty.clone());
24    let elt = eval.eta_neu(&elt, ty);
25    let mut out = DiscreteDblModel::new(theory.definition.clone());
26    let mut name_translation = HashMap::new();
27    extract_to(&eval, &mut out, &mut name_translation, vec![], vec![], &elt, ty);
28    (out, name_translation)
29}
30
31// val must be an eta-expanded element of an object type
32fn name_of(val: &TmV) -> QualifiedName {
33    let mut out = Vec::new();
34    let mut n = val.as_neu();
35    while let TmN_::Proj(n1, f, _) = &*n.clone() {
36        n = n1.clone();
37        out.push(*f);
38    }
39    out.reverse();
40    out.into()
41}
42
43fn extract_to(
44    eval: &Evaluator,
45    out: &mut DiscreteDblModel,
46    name_translation: &mut HashMap<QualifiedName, QualifiedLabel>,
47    prefix: Vec<NameSegment>,
48    label_prefix: Vec<LabelSegment>,
49    val: &TmV,
50    ty: &TyV,
51) {
52    match &**ty {
53        TyV_::Object(ot) => {
54            out.add_ob(prefix.clone().into(), ot.clone());
55            name_translation.insert(prefix.into(), label_prefix.into());
56        }
57        TyV_::Morphism(mt, dom, cod) => {
58            out.add_mor(prefix.clone().into(), name_of(dom), name_of(cod), mt.0.clone());
59            name_translation.insert(prefix.into(), label_prefix.into());
60        }
61        TyV_::Record(r) => {
62            for (name, (label, _)) in r.fields1.iter() {
63                let mut prefix = prefix.clone();
64                prefix.push(*name);
65                let mut label_prefix = label_prefix.clone();
66                label_prefix.push(*label);
67                extract_to(
68                    eval,
69                    out,
70                    name_translation,
71                    prefix,
72                    label_prefix,
73                    &eval.proj(val, *name, *label),
74                    &eval.field_ty(ty, val, *name),
75                )
76            }
77        }
78        TyV_::Sing(_, _) => {}
79        TyV_::Unit => {}
80    }
81}
82
83/// Display model output nicely
84pub fn model_output(
85    prefix: &str,
86    out: &mut impl fmt::Write,
87    model: &DiscreteDblModel,
88    name_translation: &HashMap<QualifiedName, QualifiedLabel>,
89) -> fmt::Result {
90    writeln!(out, "{prefix}object generators:")?;
91    for obgen in model.ob_generators() {
92        writeln!(
93            out,
94            "{prefix}  {} : {}",
95            name_translation.get(&obgen).unwrap(),
96            model.ob_type(&obgen)
97        )?;
98    }
99    writeln!(out, "{prefix}morphism generators:")?;
100    for morgen in model.mor_generators() {
101        writeln!(
102            out,
103            "{prefix}  {} : {} -> {} ({})",
104            name_translation.get(&morgen).unwrap(),
105            name_translation.get(&model.mor_generator_dom(&morgen)).unwrap(),
106            name_translation.get(&model.mor_generator_cod(&morgen)).unwrap(),
107            MorphismType(model.mor_generator_type(&morgen))
108        )?;
109    }
110    Ok(())
111}
catlog/tt/modelgen.rs

catlog/tt/
modelgen.rs
