catlog/tt/

modelgen.rs

//! Generate catlog models from DoubleTT types.

use all_the_same::all_the_same;
use derive_more::{From, TryInto};
use tattle::display::SourceInfo;

use std::rc::Rc;

use super::{eval::*, prelude::*, text_elab, theory::*, toplevel::*, val::*};
use crate::dbl::{
    discrete::{self, DiscreteDblModelInstance, DiscreteInstanceTerm},
    discrete_tabulator, modal,
    model::{DblModel, DblModelPrinter, FpDblModel, MutDblModel},
    theory::{DblTheory, DblTheoryKind, NonUnital, Unital},
};
use crate::one::{
    Category,
    path::{Path, PathEq},
};
use crate::zero::{Namespace, QualifiedName, SkelColumn};

/// A model generated by DoubleTT.
///
/// Similarly to [`TheoryDef`], this enum boxes the different types of models
/// that can be generated by DoubleTT.
pub enum Model {
    /// A model of a discrete double theory.
    Discrete(Box<discrete::DiscreteDblModel>),
    /// A model of a discrete tabulator theory.
    DiscreteTab(Box<discrete_tabulator::DiscreteTabModel>),
    /// A model of a unital modal double theory.
    ModalUnital(Box<modal::ModalDblModel<Unital>>),
    /// A model of a non-unital modal double theory.
    ModalNonUnital(Box<modal::ModalDblModel<NonUnital>>),
}

/// An object in a model generated by DoubleTT.
#[derive(Debug, From, TryInto)]
enum Ob {
    Discrete(QualifiedName),
    DiscreteTab(discrete_tabulator::TabOb),
    Modal(modal::ModalOb),
}

/// A morphism in a model generated by DoubleTT.
#[derive(Debug, From, TryInto)]
enum Mor {
    Discrete(Path<QualifiedName, QualifiedName>),
    DiscreteTab(discrete_tabulator::TabMor),
    Modal(modal::ModalMor),
}

impl Model {
    /// Constructs an empty model of a theory.
    pub fn new(theory: &TheoryDef) -> Self {
        match theory {
            TheoryDef::Discrete(theory) => {
                Model::Discrete(Box::new(discrete::DiscreteDblModel::new(theory.clone())))
            }
            TheoryDef::DiscreteTab(theory) => Model::DiscreteTab(Box::new(
                discrete_tabulator::DiscreteTabModel::new(theory.clone()),
            )),
            TheoryDef::ModalUnital(theory) => {
                Model::ModalUnital(Box::new(modal::ModalDblModel::new(theory.clone())))
            }
            TheoryDef::ModalNonUnital(theory) => {
                Model::ModalNonUnital(Box::new(modal::ModalDblModel::new(theory.clone())))
            }
        }
    }

    /// Parses and generates a model from plain text.
    ///
    /// If there is an error in parsing, an error message is returned.
    pub fn from_text(th: &TheoryDef, s: &str) -> Result<Self, String> {
        let theory = Theory::new("_".into(), th.clone());
        let reporter = Reporter::new();
        let toplevel: Toplevel = Default::default();
        let maybe_elab = text_elab::TT_PARSE_CONFIG.with_parsed(s, reporter.clone(), |fntn| {
            let mut elaborator = text_elab::Elaborator::new(theory, reporter.clone(), &toplevel);
            Some(elaborator.ty(fntn))
        });
        if let Some((_, ty_v)) = maybe_elab
            && !reporter.errored()
        {
            let (model, _) = Self::from_ty(&toplevel, th, &ty_v);
            Ok(model)
        } else {
            let source_info = SourceInfo::new(None, s);
            Err(source_info.extract_report_to_string(reporter))
        }
    }

    /// Generates a model from a type.
    ///
    /// Precondition: `ty` must be valid in the empty context.
    pub fn from_ty(toplevel: &Toplevel, th: &TheoryDef, ty: &BaseTyV) -> (Self, Namespace) {
        let mut generator = ModelGenerator::new(toplevel, th);
        let namespace = generator.generate(ty);
        (generator.model, namespace)
    }

    /// Tries to extract a model of a discrete theory.
    pub fn as_discrete(self) -> Option<discrete::DiscreteDblModel> {
        match self {
            Model::Discrete(model) => Some(*model),
            _ => None,
        }
    }

    /// Tries to extract a model of a unital modal theory.
    pub fn as_modal(self) -> Option<modal::ModalDblModel<Unital>> {
        match self {
            Model::ModalUnital(model) => Some(*model),
            _ => None,
        }
    }

    /// Tries to extract a model of a non-unital modal theory.
    pub fn as_modal_non_unital(self) -> Option<modal::ModalDblModel<NonUnital>> {
        match self {
            Model::ModalNonUnital(model) => Some(*model),
            _ => None,
        }
    }

    /// Constructs the identity morphism on an object.
    fn id(&self, ob: Ob) -> Mor {
        all_the_same!(match self {
            Model::[Discrete, ModalUnital, DiscreteTab, ModalNonUnital](model) => {
                model.id(ob.try_into().unwrap()).into()
            }
        })
    }

    /// Composes a pair of morphisms.
    fn compose2(&self, mor1: Mor, mor2: Mor) -> Mor {
        all_the_same!(match self {
            Model::[Discrete, DiscreteTab, ModalUnital, ModalNonUnital](model) => {
                model.compose2(mor1.try_into().unwrap(), mor2.try_into().unwrap()).into()
            }
        })
    }

    /// Tabulates a morphism, if possible.
    fn tabulated(&self, mor: Mor) -> Option<Ob> {
        match self {
            Model::Discrete(_) => None,
            Model::DiscreteTab(model) => Some(model.tabulated(mor.try_into().unwrap()).into()),
            Model::ModalUnital(_) | Model::ModalNonUnital(_) => None,
        }
    }

    /// Adds an object generator to the model.
    fn add_ob(&mut self, name: QualifiedName, ob_type: ObType) {
        all_the_same!(match self {
            Model::[Discrete, DiscreteTab, ModalUnital, ModalNonUnital](model) => {
                model.add_ob(name, ob_type.try_into().unwrap())
            }
        });
    }

    /// Adds a morphism generator to the model.
    fn add_mor(&mut self, name: QualifiedName, dom: Ob, cod: Ob, mor_type: MorType) {
        all_the_same!(match self {
            Model::[Discrete, DiscreteTab, ModalUnital, ModalNonUnital](model) => {
                model.add_mor(
                    name,
                    dom.try_into().unwrap(),
                    cod.try_into().unwrap(),
                    mor_type.try_into().unwrap()
                );
            }
        });
    }

    /// Adds an equation between two morphisms to the model.
    fn add_equation(&mut self, lhs: Mor, rhs: Mor) {
        match self {
            Model::Discrete(model) => {
                model.add_equation(PathEq::new(lhs.try_into().unwrap(), rhs.try_into().unwrap()));
            }
            Model::DiscreteTab(_) => {
                // Discrete tabulator models currently do not support equations, so we ignore them.
            }
            Model::ModalUnital(_) | Model::ModalNonUnital(_) => {
                // Modal models currently do not support equations, so we ignore them.
            }
        }
    }

    /// Pretty prints a summary of the model.
    pub fn summary(&self, printer: &DblModelPrinter) -> String {
        all_the_same!(match self {
            Model::[Discrete, DiscreteTab, ModalUnital, ModalNonUnital](model) => printer.summary(model.as_ref())
        })
    }

    /// Pretty prints the model in the given namespace.
    pub fn to_doc<'a>(&self, printer: &DblModelPrinter, ns: &Namespace) -> D<'a> {
        all_the_same!(match self {
            Model::[Discrete, DiscreteTab, ModalUnital, ModalNonUnital](model) => printer.namespaced_doc(model.as_ref(), ns, ns)
        })
    }
}

struct ModelGenerator<'a> {
    eval: Evaluator<'a>,
    theory: TheoryDef,
    model: Model,
}

impl<'a> ModelGenerator<'a> {
    fn new(toplevel: &'a Toplevel, theory: &TheoryDef) -> Self {
        let eval = Evaluator::empty(toplevel);
        let theory = theory.clone();
        let model = Model::new(&theory);
        Self { eval, theory, model }
    }

    fn generate(&mut self, ty: &BaseTyV) -> Namespace {
        let tm_n;
        (tm_n, self.eval) = self.eval.bind_self(ty.clone());
        let tm_v = self.eval.eta_neu(&tm_n, ty);
        self.extract(vec![], &tm_v, ty).unwrap_or_else(Namespace::new_for_uuid)
    }

    /// Constructs a generating morphism.
    fn mor_generator(&self, name: QualifiedName) -> Mor {
        match &self.model {
            Model::Discrete(_) => Mor::Discrete(Path::single(name)),
            Model::DiscreteTab(_) => Mor::DiscreteTab(name.into()),
            Model::ModalUnital(_) | Model::ModalNonUnital(_) => {
                Mor::Modal(modal::ModalMor::Generator(name))
            }
        }
    }

    /// Constructs an application of an object operation, if the theory is modal.
    ///
    /// Returns the constructed object along with the expected object type of the result.
    fn ob_app(&self, name: &NameSegment, tm_v: &BaseTmV) -> Option<(Ob, ObType)> {
        let name: QualifiedName = [*name].into();
        match &self.model {
            Model::Discrete(_) | Model::DiscreteTab(_) => None,
            Model::ModalUnital(model) => self.op_app_modal(model, name, tm_v),
            Model::ModalNonUnital(model) => self.op_app_modal(model, name, tm_v),
        }
    }

    fn op_app_modal<Kind: DblTheoryKind>(
        &self,
        model: &modal::ModalDblModel<Kind>,
        name: QualifiedName,
        tm_v: &BaseTmV,
    ) -> Option<(Ob, ObType)> {
        let theory = model.theory();
        let op = modal::ModalObOp::generator(name.clone());
        let ot: ObType = theory.ob_op_cod(&op).into();
        let ob = self.make_ob_check_type(tm_v, &theory.ob_op_dom(&op).into())?;
        let ob = ob.try_into().unwrap();
        Some((Ob::Modal(modal::ModalOb::App(Box::new(ob), name)), ot))
    }

    /// Constructs a list of objects, if allowed.
    fn ob_list(&self, elems: Vec<Ob>, ob_type: &ObType) -> Option<Ob> {
        match &self.model {
            Model::Discrete(_) | Model::DiscreteTab(_) => None,
            Model::ModalUnital(_) | Model::ModalNonUnital(_) => {
                let ob_type: &modal::ModalObType = ob_type.try_into().unwrap();
                let Some(modal::Modality::List(list_type)) = ob_type.modalities.last() else {
                    unreachable!() // We know this is a list modality from the call site.
                };
                Some(Ob::Modal(modal::ModalOb::List(
                    *list_type,
                    elems.into_iter().map(|ob| ob.try_into().unwrap()).collect(),
                )))
            }
        }
    }

    /// Attempts to make an object of a model from a term.
    ///
    /// Returns the object together with the appropriate type.
    fn make_ob_synth_type(&self, val: &BaseTmV) -> Option<(Ob, ObType)> {
        match &**val {
            BaseTmV_::Neu(n, ty_v) => {
                let BaseTyV_::Object(ob_type) = &**ty_v else {
                    return None;
                };
                let name = n.to_qualified_name();
                let ob = match &self.model {
                    Model::Discrete(_) => Ob::Discrete(name),
                    Model::DiscreteTab(_) => Ob::DiscreteTab(name.into()),
                    Model::ModalUnital(_) | Model::ModalNonUnital(_) => {
                        Ob::Modal(modal::ModalOb::Generator(name))
                    }
                };
                Some((ob, ob_type.clone()))
            }
            BaseTmV_::App(name, tm_v) => self.ob_app(name, tm_v),
            BaseTmV_::Tab(mor_tm_v) => {
                let (mor, mor_type) = self.synth_mor(mor_tm_v)?;
                Some((self.model.tabulated(mor)?, self.theory.tabulator(mor_type)?))
            }
            _ => None,
        }
    }

    /// Attempts to make an object of a model from a term.
    ///
    /// Also checks that the term constructs an object of the given type, returning only the object if successful.
    fn make_ob_check_type(&self, val: &BaseTmV, ob_type: &ObType) -> Option<Ob> {
        match &**val {
            // ob_type checked recursively.
            BaseTmV_::List(elems) => {
                let el_type = ob_type.clone().list_arg()?;
                let elems: Option<Vec<_>> =
                    elems.iter().map(|tm| self.make_ob_check_type(tm, &el_type)).collect();
                self.ob_list(elems?, ob_type)
            }
            _ => {
                let (ob, ot) = self.make_ob_synth_type(val)?;
                (ot == *ob_type).then_some(ob)
            }
        }
    }

    /// Attempts to make a morphism of a model from a term.
    ///
    /// Also returns the expected morphism type of the result.
    fn synth_mor(&self, val: &BaseTmV) -> Option<(Mor, MorType)> {
        match &**val {
            BaseTmV_::Neu(n, ty_v) => {
                let BaseTyV_::Morphism(mor_type, _, _) = &**ty_v else {
                    return None;
                };
                let name = n.to_qualified_name();
                Some((self.mor_generator(name), mor_type.clone()))
            }
            BaseTmV_::Id(x) => {
                let (dom, dom_type) = self.make_ob_synth_type(x)?;
                let mor_type = self.theory.hom_type(dom_type)?;
                Some((self.model.id(dom), mor_type))
            }
            BaseTmV_::Compose(f, g) => {
                let (mf, mtf) = self.synth_mor(f)?;
                let (mg, mtg) = self.synth_mor(g)?;
                Some((self.model.compose2(mf, mg), self.theory.compose_types2(mtf, mtg)?))
            }
            _ => None,
        }
    }

    /// Attempts to make a morphism from a term of the given morphism type.
    ///
    /// At this time, all morphism constructors allow for type synthesis, but
    /// eventually this will change.
    fn make_mor(&self, val: &BaseTmV, mor_type: &MorType) -> Option<Mor> {
        let (mor, mt) = self.synth_mor(val)?;
        (mt == *mor_type).then_some(mor)
    }

    fn extract(
        &mut self,
        prefix: Vec<NameSegment>,
        val: &BaseTmV,
        ty: &BaseTyV,
    ) -> Option<Namespace> {
        match &**ty {
            BaseTyV_::Object(ot) => {
                self.model.add_ob(prefix.into(), ot.clone());
                None
            }
            BaseTyV_::Morphism(mt, dom, cod) => {
                let dom = self.make_ob_check_type(dom, &self.theory.src_type(mt))?;
                let cod = self.make_ob_check_type(cod, &self.theory.tgt_type(mt))?;
                self.model.add_mor(prefix.into(), dom, cod, mt.clone());
                None
            }
            BaseTyV_::Record(r) => {
                let mut namespace = Namespace::new_for_uuid();
                for (name, (label, _)) in r.fields.iter() {
                    let mut prefix = prefix.clone();
                    prefix.push(*name);
                    if let NameSegment::Uuid(uuid) = name {
                        namespace.set_label(*uuid, *label);
                    }
                    let field_tm_v = self.eval.proj(val, *name, *label);
                    let field_ty_v = self.eval.field_ty(ty, val, *name);
                    if let Some(inner) = self.extract(prefix, &field_tm_v, &field_ty_v) {
                        namespace.add_inner(*name, inner);
                    };
                }
                Some(namespace)
            }
            BaseTyV_::Sing(_, _) => None,
            BaseTyV_::Id(mor_ty, lhs, rhs) => {
                let BaseTyV_::Morphism(mt, _, _) = &**mor_ty else {
                    return None;
                };
                if let (Some(lhs), Some(rhs)) = (self.make_mor(lhs, mt), self.make_mor(rhs, mt)) {
                    self.model.add_equation(lhs, rhs);
                }
                None
            }
            BaseTyV_::Meta(_) => None,
        }
    }

    /// Extracts a [`ModelInstance`] from the fiber record of an instance body,
    /// dispatching on the doctrine of the (already generated) codomain model.
    fn instance(
        &self,
        fields: &Row<FiberTyV>,
        namespace: &mut Namespace,
    ) -> Result<ModelInstance, String> {
        match &self.model {
            Model::Discrete(model) => {
                let mut instance = DiscreteDblModelInstance::new(Rc::new((**model).clone()));
                extract_instance_record(&mut instance, namespace, &[], fields)?;
                Ok(ModelInstance::Discrete(instance))
            }
            Model::DiscreteTab(_) => {
                Err("instance generation does not support discrete tabulator theories".into())
            }
            Model::ModalUnital(model) => {
                Ok(ModelInstance::ModalUnital(self.modal_instance(model, namespace, fields)?))
            }
            Model::ModalNonUnital(model) => {
                Ok(ModelInstance::ModalNonUnital(self.modal_instance(model, namespace, fields)?))
            }
        }
    }

    /// Builds a modal instance over the given codomain model by walking the
    /// fiber record.
    fn modal_instance<Kind: DblTheoryKind + Clone>(
        &self,
        model: &modal::ModalDblModel<Kind>,
        namespace: &mut Namespace,
        fields: &Row<FiberTyV>,
    ) -> Result<modal::ModalDblModelInstance<Kind>, String> {
        let mut instance = modal::ModalDblModelInstance::new(Rc::new(model.clone()));
        self.extract_modal_record(&mut instance, namespace, &[], fields)?;
        Ok(instance)
    }

    /// Registers the contents of an instance (a fiber record) into a modal
    /// model instance, recursing into sub-instance imports under their prefix.
    ///
    /// Two passes, matching [`extract_instance_record`]: generators and
    /// sub-instances first, then the equation ([`Id`](FiberTyV_::Id)) fields,
    /// so every generator a term may mention is already registered.
    fn extract_modal_record<Kind: DblTheoryKind>(
        &self,
        instance: &mut modal::ModalDblModelInstance<Kind>,
        namespace: &mut Namespace,
        prefix: &[NameSegment],
        fields: &Row<FiberTyV>,
    ) -> Result<(), String> {
        for (name, (label, field_ty)) in fields.iter() {
            match &**field_ty {
                FiberTyV_::Over(obj) => {
                    if let NameSegment::Uuid(uuid) = name {
                        namespace.set_label(*uuid, *label);
                    }
                    let mut qsegs = prefix.to_vec();
                    qsegs.push(*name);
                    let qname: QualifiedName = qsegs.into();
                    let fiber = self.modal_fiber_ob(obj)?;
                    instance.add_generator(qname, fiber);
                }
                FiberTyV_::Record(sub_fields) => {
                    if let NameSegment::Uuid(uuid) = name {
                        namespace.set_label(*uuid, *label);
                    }
                    // Labels of the sub-instance's own generators live in an
                    // inner namespace keyed by the import's name, mirroring
                    // the structure of the flattened qualified names.
                    let mut sub_ns = Namespace::new_for_uuid();
                    let mut sub_prefix = prefix.to_vec();
                    sub_prefix.push(*name);
                    self.extract_modal_record(instance, &mut sub_ns, &sub_prefix, sub_fields)?;
                    namespace.add_inner(*name, sub_ns);
                }
                FiberTyV_::Id(_, _, _) => {}
            }
        }
        for (_, (_, field_ty)) in fields.iter() {
            if let FiberTyV_::Id(eq_ty, lhs, rhs) = &**field_ty {
                let ob_type = self.modal_equation_ob_type(eq_ty)?;
                let lhs_t = self.modal_instance_term(&*instance, lhs, &ob_type, prefix)?;
                let rhs_t = self.modal_instance_term(&*instance, rhs, &ob_type, prefix)?;
                instance.add_equation(lhs_t, rhs_t);
            }
        }
        Ok(())
    }

    /// Converts the codomain object a generator lies over into a [`ModalOb`].
    fn modal_fiber_ob(&self, obj: &BaseTmV) -> Result<modal::ModalOb, String> {
        let (ob, _) = self.make_ob_synth_type(obj).ok_or_else(|| {
            "instance generator lies over an object this doctrine cannot yet extract".to_string()
        })?;
        ob.try_into()
            .map_err(|_| "expected a modal object as a generator's fiber".to_string())
    }

    /// The object type an equation lives over (its `Over` fiber type).
    fn modal_equation_ob_type(&self, eq_ty: &FiberTyV) -> Result<ObType, String> {
        let FiberTyV_::Over(obj) = &**eq_ty else {
            return Err("instance equation is not over an object".into());
        };
        let (_, ob_type) = self
            .make_ob_synth_type(obj)
            .ok_or_else(|| "cannot determine the type of an instance equation".to_string())?;
        Ok(ob_type)
    }

    /// Converts a fiber term into a [`ModalInstanceTerm`].
    fn modal_instance_term<Kind: DblTheoryKind>(
        &self,
        instance: &modal::ModalDblModelInstance<Kind>,
        tm: &FiberTmV,
        expected: &ObType,
        prefix: &[NameSegment],
    ) -> Result<modal::ModalInstanceTerm, String> {
        let (mor, base) = self.modal_mor_base(instance, tm, expected, prefix)?;
        Ok(modal::ModalInstanceTerm { mor, base })
    }

    /// The heart of modal term extraction: converts a fiber term into a
    /// morphism applied to a base of generators, threading the expected object
    /// type down so list modalities can be recovered.
    ///
    /// The returned morphism is an identity exactly when the term is a pure
    /// base (generators/lists with no applied morphisms), keeping terms in the
    /// flat normal form of [`ModalInstanceTerm`]: composition and list-tupling
    /// of morphisms encountered inside list elements are pushed into the
    /// morphism (via `Composite`/`List`) rather than nesting applications.
    fn modal_mor_base<Kind: DblTheoryKind>(
        &self,
        instance: &modal::ModalDblModelInstance<Kind>,
        tm: &FiberTmV,
        expected: &ObType,
        prefix: &[NameSegment],
    ) -> Result<(modal::ModalMor, modal::ModalInstanceBase), String> {
        use modal::{ModalInstanceBase, ModalMor, ModalOb, Modality, MorListData};
        match &**tm {
            FiberTmV_::Var(_, _, _) | FiberTmV_::Proj(_, _, _) => {
                let mut segs = prefix.to_vec();
                segs.extend(fiber_full_name(tm)?);
                let qname: QualifiedName = segs.into();
                let fiber = instance
                    .fiber_of(&qname)
                    .ok_or_else(|| format!("instance term mentions unknown generator {qname}"))?;
                let id = instance.model().id(fiber.clone());
                Ok((id, ModalInstanceBase::Generator(qname)))
            }
            FiberTmV_::List(elems) => {
                let (modality, el_type) = expected
                    .clone()
                    .mode_app()
                    .ok_or_else(|| "expected a modal list type for a list term".to_string())?;
                let Modality::List(list_ty) = modality else {
                    return Err("expected a list modality for a list term".into());
                };
                let mut mors = Vec::with_capacity(elems.len());
                let mut bases = Vec::with_capacity(elems.len());
                for elem in elems {
                    let (m, b) = self.modal_mor_base(instance, elem, &el_type, prefix)?;
                    mors.push(m);
                    bases.push(b);
                }
                let base = ModalInstanceBase::List(list_ty, bases);
                // If every element is a pure base, the whole list is too, and
                // the morphism is the identity on the list object.
                let identity_obs: Option<Vec<&ModalOb>> =
                    mors.iter().map(modal::modal_mor_as_identity).collect();
                if let Some(objs) = identity_obs {
                    let list_ob = ModalOb::List(list_ty, objs.into_iter().cloned().collect());
                    Ok((instance.model().id(list_ob), base))
                } else {
                    let data = match list_ty {
                        modal::List::Plain => MorListData::Plain(),
                        modal::List::Symmetric => {
                            MorListData::Symmetric(SkelColumn::new((0..mors.len()).collect()))
                        }
                        other => {
                            return Err(format!(
                                "instance terms do not yet support the {other:?} list modality"
                            ));
                        }
                    };
                    Ok((ModalMor::List(data, mors), base))
                }
            }
            FiberTmV_::OverApp(path, _cod, inner) => {
                let qname: QualifiedName =
                    path.iter().map(|(seg, _)| *seg).collect::<Vec<_>>().into();
                let mor = ModalMor::Generator(qname.clone());
                let mor_type = MorType::Modal(instance.model().mor_generator_type(&qname));
                let dom_ty = self.theory.src_type(&mor_type);
                let (inner_mor, base) = self.modal_mor_base(instance, inner, &dom_ty, prefix)?;
                let full = if modal::modal_mor_as_identity(&inner_mor).is_some() {
                    mor
                } else {
                    instance.model().compose2(inner_mor, mor)
                };
                Ok((full, base))
            }
            FiberTmV_::ObApp(op, inner) => {
                let op_name: QualifiedName = [*op].into();
                // Recurse into the argument at the object operation's domain
                // type, so a list argument recovers its modality.
                let ob_op = modal::ModalObOp::generator(op_name.clone());
                let dom_ty: ObType = instance.model().theory().ob_op_dom(&ob_op).into();
                let (inner_mor, inner_base) =
                    self.modal_mor_base(instance, inner, &dom_ty, prefix)?;
                // If the argument is a pure base (identity morphism), the
                // object operation lands on data and the morphism stays the
                // identity on the resulting `App` object. Otherwise the
                // operation acts functorially on the argument's morphism,
                // yielding a `HomApp`.
                let mor = match modal::modal_mor_as_identity(&inner_mor).cloned() {
                    Some(inner_ob) => {
                        let app_ob = ModalOb::App(Box::new(inner_ob), op_name.clone());
                        instance.model().id(app_ob)
                    }
                    None => ModalMor::HomApp(Box::new(inner_mor.into()), op_name.clone()),
                };
                let base = ModalInstanceBase::ObApp(op_name, Box::new(inner_base));
                Ok((mor, base))
            }
            FiberTmV_::Meta(_) => Err("instance term contains an unresolved metavariable".into()),
        }
    }
}

/// An instance of a model generated by DoubleTT.
///
/// Like [`Model`], this boxes the per-doctrine concrete instance types
/// behind one enum.
pub enum ModelInstance {
    /// An instance of a discrete double model.
    Discrete(DiscreteDblModelInstance),
    /// An instance of a unital modal double model.
    ModalUnital(modal::ModalDblModelInstance<Unital>),
    /// An instance of a non-unital modal double model.
    ModalNonUnital(modal::ModalDblModelInstance<NonUnital>),
}

/// Generates a [`ModelInstance`] from an elaborated [`Instance`] declaration.
///
/// Walks the instance's fiber [`Record`](FiberTyV_::Record), registering
/// each generator with its fiber, each equation as a pair of instance
/// terms, and each sub-instance's contents under the appropriate prefix.
///
/// The codomain model is built with a `ModelGenerator`, which is then
/// reused to type the instance's generators and equation terms (this is how
/// modal list modalities are recovered).
pub fn instance_from_def(
    toplevel: &Toplevel,
    th: &TheoryDef,
    inst: &Instance,
) -> Result<(ModelInstance, Namespace), String> {
    let mut generator = ModelGenerator::new(toplevel, th);
    // Seed the namespace with the codomain model's labels, so that names of
    // codomain objects and morphisms appearing in fibers and terms resolve
    // alongside the instance's own generators.
    let mut namespace = generator.generate(&inst.codomain);
    let FiberTyV_::Record(fields) = &*inst.val else {
        return Err("expected an instance (a fiber record)".into());
    };
    let instance = generator.instance(fields, &mut namespace)?;
    Ok((instance, namespace))
}

/// The flat normal form of a single instance term, as produced by
/// [`normalize_instance_term`]: a composite model morphism applied to a base
/// of generators. Doctrine-specific because each has its own term type.
pub enum NormalizedInstanceTerm {
    /// A term of an instance of a discrete double model.
    Discrete(DiscreteInstanceTerm),
    /// A term of an instance of a modal double model (unital or non-unital).
    Modal(modal::ModalInstanceTerm),
}

impl NormalizedInstanceTerm {
    /// Renders the term in its flat normal form `mor @ base`, exposing the
    /// single (composite) model morphism acting on a base of generators. A
    /// term whose morphism is the identity (a pure base) is rendered as just
    /// its base. This is deliberately distinct from the applicative
    /// reconstruction used in instance summaries: the point of `norm` is to
    /// *show* the composite, e.g. `t(@tensor [s(x0), s(x0)])` normalizing to
    /// `(@tensor [s, s] ; t) @ @tensor [x0, x0]`.
    pub fn render(&self) -> String {
        match self {
            NormalizedInstanceTerm::Discrete(t) => match &t.path {
                Path::Id(_) => format!("{}", t.base),
                Path::Seq(edges) => {
                    let parts: Vec<_> = edges.iter().map(|mor| format!("{mor}")).collect();
                    if parts.len() == 1 {
                        format!("{} @ {}", parts[0], t.base)
                    } else {
                        format!("({}) @ {}", parts.join(" ; "), t.base)
                    }
                }
            },
            NormalizedInstanceTerm::Modal(t) => {
                let base = render_modal_base(&t.base);
                match modal::modal_mor_as_identity(&t.mor) {
                    Some(_) => base,
                    None => format!("{} @ {}", render_modal_mor(&t.mor), base),
                }
            }
        }
    }
}

/// Renders the base of a flat modal term: generators by name, lists as
/// `[a, b, …]`, and object operations as `@op <base>`.
fn render_modal_base(base: &modal::ModalInstanceBase) -> String {
    match base {
        modal::ModalInstanceBase::Generator(name) => format!("{name}"),
        modal::ModalInstanceBase::List(_, bases) => {
            let inner: Vec<_> = bases.iter().map(render_modal_base).collect();
            format!("[{}]", inner.join(", "))
        }
        modal::ModalInstanceBase::ObApp(op, inner) => {
            format!("@{op} {}", render_modal_base(inner))
        }
    }
}

/// Renders a model morphism in a flat term. A composite of length ≥ 2 is
/// shown parenthesized as `(m1 ; m2 ; …)`, applied left-to-right; the
/// functorial `HomApp` of an object operation shows as `@op <path>`.
fn render_modal_mor(mor: &modal::ModalMor) -> String {
    match mor {
        modal::ModalMor::Generator(name) => format!("{name}"),
        modal::ModalMor::Composite(path) => {
            let parts = render_modal_mor_path(path);
            match parts.len() {
                0 => "id".to_string(),
                1 => parts.into_iter().next().unwrap(),
                _ => format!("({})", parts.join(" ; ")),
            }
        }
        modal::ModalMor::App(path, op) => {
            format!("{op}({})", render_modal_mor_path(path).join(" ; "))
        }
        modal::ModalMor::HomApp(path, op) => {
            format!("@{op} {}", render_modal_mor_path(path).join(" ; "))
        }
        modal::ModalMor::List(_, mors) => {
            let inner: Vec<_> = mors.iter().map(render_modal_mor).collect();
            format!("[{}]", inner.join(", "))
        }
    }
}

/// The morphisms along a path, each flat-rendered; empty for an identity path.
fn render_modal_mor_path(path: &Path<modal::ModalOb, modal::ModalMor>) -> Vec<String> {
    match path {
        Path::Id(_) => Vec::new(),
        Path::Seq(edges) => edges.iter().map(render_modal_mor).collect(),
    }
}

/// Normalizes a single already-elaborated fiber term `tm` (lying over the
/// codomain object `over`) in the context of the instance `inst`, returning
/// its flat normal form.
///
/// This is what backs `norm [inst] <term>`: the term is elaborated against
/// `inst`'s fiber scope elsewhere (in `text_elab`), then handed here to run
/// the same extraction that turns an instance body's equations into
/// [`modal::ModalInstanceTerm`]s — which is where nested morphism applications
/// get composed into a single (`Composite`/`List`) morphism.
pub fn normalize_instance_term(
    toplevel: &Toplevel,
    th: &TheoryDef,
    inst: &Instance,
    tm: &FiberTmV,
    over: &BaseTmV,
) -> Result<NormalizedInstanceTerm, String> {
    let mut generator = ModelGenerator::new(toplevel, th);
    generator.generate(&inst.codomain);
    let FiberTyV_::Record(fields) = &*inst.val else {
        return Err("expected an instance (a fiber record)".into());
    };
    // Build the instance first, so every generator the term may mention is
    // registered before we extract (extraction resolves generators by name).
    let mut namespace = Namespace::new_for_uuid();
    match generator.instance(fields, &mut namespace)? {
        ModelInstance::Discrete(instance) => {
            let term = fiber_tm_to_discrete_instance_term(&instance, tm, &[])?;
            Ok(NormalizedInstanceTerm::Discrete(term))
        }
        ModelInstance::ModalUnital(instance) => {
            let (_, ob_type) = generator
                .make_ob_synth_type(over)
                .ok_or_else(|| "cannot determine the object the term lies over".to_string())?;
            let term = generator.modal_instance_term(&instance, tm, &ob_type, &[])?;
            Ok(NormalizedInstanceTerm::Modal(term))
        }
        ModelInstance::ModalNonUnital(instance) => {
            let (_, ob_type) = generator
                .make_ob_synth_type(over)
                .ok_or_else(|| "cannot determine the object the term lies over".to_string())?;
            let term = generator.modal_instance_term(&instance, tm, &ob_type, &[])?;
            Ok(NormalizedInstanceTerm::Modal(term))
        }
    }
}

/// Register the contents of an instance (a fiber record) into the model
/// instance under construction, recursing into sub-instance imports under
/// their prefix.
///
/// Two passes so that every generator — including those of sub-instances
/// — is registered before any equation that may mention it: first the
/// [`Over`](FiberTyV_::Over) generator fields and [`Record`](FiberTyV_::Record)
/// sub-instances, then the [`Id`](FiberTyV_::Id) equation fields.
fn extract_instance_record(
    instance: &mut DiscreteDblModelInstance,
    namespace: &mut Namespace,
    prefix: &[NameSegment],
    fields: &Row<FiberTyV>,
) -> Result<(), String> {
    for (name, (label, field_ty)) in fields.iter() {
        match &**field_ty {
            FiberTyV_::Over(obj) => {
                if let NameSegment::Uuid(uuid) = name {
                    namespace.set_label(*uuid, *label);
                }
                let mut qsegs = prefix.to_vec();
                qsegs.push(*name);
                let qname: QualifiedName = qsegs.into();
                // The fiber is the codomain object the generator lies over.
                // For a plain generator that is a projection `self.V`, whose
                // qualified name is `V`. Modal objects (lists, tensors) are
                // not yet supported by discrete model generation.
                let BaseTmV_::Neu(n, _) = &**obj else {
                    return Err("model generation does not yet support generators over a modal \
                         object (list/tensor)"
                        .into());
                };
                instance.add_generator(qname, n.to_qualified_name());
            }
            FiberTyV_::Record(sub_fields) => {
                if let NameSegment::Uuid(uuid) = name {
                    namespace.set_label(*uuid, *label);
                }
                // Labels of the sub-instance's own generators live in an
                // inner namespace keyed by the import's name, mirroring the
                // structure of the flattened qualified names.
                let mut sub_ns = Namespace::new_for_uuid();
                let mut sub_prefix = prefix.to_vec();
                sub_prefix.push(*name);
                extract_instance_record(instance, &mut sub_ns, &sub_prefix, sub_fields)?;
                namespace.add_inner(*name, sub_ns);
            }
            FiberTyV_::Id(_, _, _) => {}
        }
    }
    for (_, (_, field_ty)) in fields.iter() {
        if let FiberTyV_::Id(_, lhs, rhs) = &**field_ty {
            let lhs_t = fiber_tm_to_discrete_instance_term(instance, lhs, prefix)?;
            let rhs_t = fiber_tm_to_discrete_instance_term(instance, rhs, prefix)?;
            instance.add_equation(lhs_t, rhs_t);
        }
    }
    Ok(())
}

/// Convert a fiber term into a [`DiscreteInstanceTerm`], prefixing each
/// generator name with the path into any enclosing sub-instances.
///
/// Nested [`OverApp`](FiberTmV_::OverApp)s are flattened into a single
/// morphism path applied to the generator at the leaf, matching the flat
/// canonical shape of [`DiscreteInstanceTerm`].
fn fiber_tm_to_discrete_instance_term(
    instance: &DiscreteDblModelInstance,
    tm: &FiberTmV,
    prefix: &[NameSegment],
) -> Result<DiscreteInstanceTerm, String> {
    // Walk outer-to-inner, recording each applied morphism.
    let mut mors_outer_first: Vec<QualifiedName> = Vec::new();
    let mut cur = tm;
    let base: QualifiedName = loop {
        match &**cur {
            FiberTmV_::OverApp(mor_path, _, inner) => {
                let name: QualifiedName =
                    mor_path.iter().map(|(seg, _)| *seg).collect::<Vec<_>>().into();
                mors_outer_first.push(name);
                cur = inner;
            }
            _ => {
                let mut segs = prefix.to_vec();
                segs.extend(fiber_full_name(cur)?);
                break segs.into();
            }
        }
    };
    // Path order is innermost-first (apply first goes first).
    mors_outer_first.reverse();
    let path = match Path::from_vec(mors_outer_first) {
        Some(p) => p,
        None => {
            let fiber = instance
                .fiber_of(&base)
                .ok_or_else(|| format!("instance term mentions unknown generator {base}"))?;
            Path::Id(fiber.clone())
        }
    };
    Ok(DiscreteInstanceTerm { path, base })
}

/// Read off the full name of a fiber term that is a generator or a chain
/// of projections out of a sub-instance import (e.g. `we.e`): the leading
/// variable contributes a segment (it is itself a generator/import name),
/// followed by each projected field.
fn fiber_full_name(tm: &FiberTmV) -> Result<Vec<NameSegment>, String> {
    let mut segments = Vec::new();
    let mut cur = tm;
    loop {
        match &**cur {
            FiberTmV_::Var(_, name, _) => {
                segments.push(*name);
                break;
            }
            FiberTmV_::Proj(inner, f, _) => {
                segments.push(*f);
                cur = inner;
            }
            _ => return Err("expected a fiber generator or projection".into()),
        }
    }
    segments.reverse();
    Ok(segments)
}

#[cfg(test)]
mod tests {
    use super::*;
    use crate::tt::text_elab::{TT_PARSE_CONFIG, TopElabResult, TopElaborator};
    use crate::tt::theory::std_theories;

    fn elaborate_to_toplevel(src: &str) -> Toplevel {
        let reporter = Reporter::new();
        let mut toplevel = Toplevel::new(std_theories());
        let _ = TT_PARSE_CONFIG.with_parsed_top(src, reporter.clone(), |topntns| {
            let mut topelab = TopElaborator::new(reporter.clone());
            for topntn in topntns.iter() {
                if let Some(TopElabResult::Declaration(name, decl)) =
                    topelab.elab(&toplevel, topntn)
                {
                    toplevel.declarations.insert(name, decl);
                }
            }
            Some(())
        });
        assert!(!reporter.errored(), "elaboration produced errors");
        toplevel
    }

    #[test]
    fn instance_over_weighted_graph() {
        let src = r#"
set_theory ThSchema

model WeightedGraph := [
  V : Entity,
  E : Entity,
  Weight : AttrType,
  src : (Hom Entity)[E, V],
  tgt : (Hom Entity)[E, V],
  weight : Attr[E, Weight]
]

instance I : WeightedGraph := [
    V := [v],
    E := [e],
    src(e) := v
]
"#;
        let toplevel = elaborate_to_toplevel(src);
        let def = match toplevel.declarations.get(&name_seg("I")) {
            Some(TopDecl::Instance(i)) => i.clone(),
            _ => panic!("expected I to be an instance declaration"),
        };
        let (instance, _ns) = instance_from_def(&toplevel, &def.theory.definition, &def).unwrap();
        let ModelInstance::Discrete(instance) = instance else {
            panic!("expected a discrete instance");
        };

        let e_qname: QualifiedName = vec![name_seg("e")].into();
        let e_fiber: QualifiedName = vec![name_seg("E")].into();
        assert_eq!(instance.fiber_of(&e_qname), Some(&e_fiber));
        assert_eq!(instance.equations().count(), 1);
    }

    /// An instance carrying fiber equations, imported as a sub-instance.
    ///
    /// `Loop` is itself a fiber record carrying an `Id`-typed field per
    /// fiber equation alongside its `e`/`v` generators, and extraction of
    /// the importer must recover both copies of the loop's structure.
    #[test]
    fn import_of_instance_with_fiber_equations() {
        let src = r#"
set_theory ThSchema

model WeightedGraph := [
  V : Entity,
  E : Entity,
  Weight : AttrType,
  src : (Hom Entity)[E, V],
  tgt : (Hom Entity)[E, V],
  weight : Attr[E, Weight]
]

instance Loop : WeightedGraph := [
    V := [v],
    E := [e],
    src(e) := v,
    tgt(e) := v
]

instance UseLoop : WeightedGraph := [
    l : Loop
]
"#;
        let toplevel = elaborate_to_toplevel(src);

        // `Loop` is a fiber record exposing its two fiber equations as
        // `Id`-typed fields alongside the `e`/`v` generators.
        let loop_def = match toplevel.declarations.get(&name_seg("Loop")) {
            Some(TopDecl::Instance(i)) => i.clone(),
            _ => panic!("expected Loop to be an instance declaration"),
        };
        let FiberTyV_::Record(r) = &*loop_def.val else {
            panic!("Loop should be a fiber record");
        };
        assert!(r.get(name_seg("e")).is_some(), "generator field e");
        assert!(r.get(name_seg("v")).is_some(), "generator field v");
        assert!(r.get(name_seg("_eq0")).is_some(), "first fiber equation");
        assert!(r.get(name_seg("_eq1")).is_some(), "second fiber equation");

        // The importer still extracts both generators and the imported
        // copy's two equations.
        let use_def = match toplevel.declarations.get(&name_seg("UseLoop")) {
            Some(TopDecl::Instance(i)) => i.clone(),
            _ => panic!("expected UseLoop to be an instance declaration"),
        };
        let (instance, _ns) =
            instance_from_def(&toplevel, &use_def.theory.definition, &use_def).unwrap();
        let ModelInstance::Discrete(instance) = instance else {
            panic!("expected a discrete instance");
        };
        let le_qname: QualifiedName = vec![name_seg("l"), name_seg("e")].into();
        let e_fiber: QualifiedName = vec![name_seg("E")].into();
        assert_eq!(instance.fiber_of(&le_qname), Some(&e_fiber));
        assert_eq!(instance.equations().count(), 2);
    }

    /// A modal (multicategory) instance: generators lie over plain objects and
    /// equations are list-domain morphism applications.
    #[test]
    fn instance_over_multicategory_monoid() {
        let src = r#"
set_theory ThMulticategory

model SigMonoid := [
  M : Object,
  op : Multihom[[M, M], M],
  unit : Multihom[[], M]
]

instance Z2 : SigMonoid := [
    M := [x],
    op([x,x]) := unit([]),
    op([x,unit([])]) := x
]
"#;
        let toplevel = elaborate_to_toplevel(src);
        let def = match toplevel.declarations.get(&name_seg("Z2")) {
            Some(TopDecl::Instance(i)) => i.clone(),
            _ => panic!("expected Z2 to be an instance declaration"),
        };
        let (instance, _ns) = instance_from_def(&toplevel, &def.theory.definition, &def).unwrap();
        let ModelInstance::ModalUnital(instance) = instance else {
            panic!("expected a unital modal instance");
        };

        let x_qname: QualifiedName = vec![name_seg("x")].into();
        let m_fiber = modal::ModalOb::Generator(vec![name_seg("M")].into());
        assert_eq!(instance.fiber_of(&x_qname), Some(&m_fiber));
        assert_eq!(instance.equations().count(), 2);
    }

    /// A symmetric-monoidal instance: equation terms feed generators through
    /// the `@tensor` object operation into unary homs between product objects.
    #[test]
    fn instance_over_symmetric_monoidal() {
        let src = r#"
set_theory ThSymMonoidalCategory

model AB := [
  A : Object,
  B : Object,
  f : (Hom Object)[@tensor [A, B], A]
]

instance i : AB := [
    A := [a],
    B := [b],
    f(@tensor [a, b]) := a
]
"#;
        let toplevel = elaborate_to_toplevel(src);
        let def = match toplevel.declarations.get(&name_seg("i")) {
            Some(TopDecl::Instance(i)) => i.clone(),
            _ => panic!("expected i to be an instance declaration"),
        };
        let (instance, _ns) = instance_from_def(&toplevel, &def.theory.definition, &def).unwrap();
        let ModelInstance::ModalUnital(instance) = instance else {
            panic!("expected a unital modal instance");
        };

        let a_qname: QualifiedName = vec![name_seg("a")].into();
        let a_fiber = modal::ModalOb::Generator(vec![name_seg("A")].into());
        assert_eq!(instance.fiber_of(&a_qname), Some(&a_fiber));
        assert_eq!(instance.equations().count(), 1);
    }

    /// A symmetric-monoidal instance whose equation feeds a *morphism*
    /// application through `@tensor`, exercising the functorial action of the
    /// object operation (a `HomApp`) rather than a pure object-op base.
    #[test]
    fn instance_over_symmetric_monoidal_functorial() {
        let src = r#"
set_theory ThSymMonoidalCategory

model Chain := [
  X : Object,
  Y : Object,
  s : (Hom Object)[X, Y],
  t : (Hom Object)[@tensor [Y, Y], X]
]

instance chain : Chain := [
    X := [x0],
    t(@tensor [s(x0), s(x0)]) := x0
]
"#;
        let toplevel = elaborate_to_toplevel(src);
        let def = match toplevel.declarations.get(&name_seg("chain")) {
            Some(TopDecl::Instance(i)) => i.clone(),
            _ => panic!("expected chain to be an instance declaration"),
        };
        let (instance, _ns) = instance_from_def(&toplevel, &def.theory.definition, &def).unwrap();
        let ModelInstance::ModalUnital(instance) = instance else {
            panic!("expected a unital modal instance");
        };
        assert_eq!(instance.equations().count(), 1);

        // The left-hand side's morphism is a HomApp: the object operation
        // `tensor` acting on the list morphism `[s, s]`.
        let (lhs, _) = instance.equations().next().unwrap();
        assert!(
            matches!(&lhs.mor, modal::ModalMor::Composite(_)),
            "expected the applied morphism to compose `t` after the tensor's HomApp"
        );
    }
}