catlog_wasm/

theory.rs

//! Wasm bindings for double theories.

use std::collections::HashMap;
use std::rc::Rc;

use all_the_same::all_the_same;
use derive_more::{From, TryInto};
use ustr::Ustr;

use wasm_bindgen::prelude::*;

use catlog::dbl::theory::{
    self, DblTheory as _, ModalMorType, ModalObOp, ModalObType, ModeApp, TabMorType, TabObOp,
    TabObType,
};
use catlog::one::{Path, QualifiedPath, ShortPath};
use catlog::tt::{
    self,
    notebook_elab::{demote_modality, promote_modality},
};
use catlog::zero::{NameSegment, QualifiedName};
use notebook_types::current::theory::*;

use super::notation::*;

/// Elaborates into object type in a discrete double theory.
impl CanElaborate<ObType, QualifiedName> for Elaborator {
    fn elab(&self, ob_type: &ObType) -> Result<QualifiedName, String> {
        match ob_type {
            ObType::Basic(id) => Ok((*id).into()),
            _ => Err(format!("Cannot use object type in discrete double theory: {ob_type:#?}")),
        }
    }
}

/// Elaborates into morphism type in a discrete double theory.
impl CanElaborate<MorType, QualifiedPath> for Elaborator {
    fn elab(&self, mor_type: &MorType) -> Result<QualifiedPath, String> {
        match mor_type {
            MorType::Basic(id) => Ok(Path::single((*id).into())),
            MorType::Composite(fs) => {
                let fs: Result<Vec<_>, _> = fs.iter().map(|f| self.elab(f)).collect();
                let path = Path::from_vec(fs?).ok_or("Composite should not be empty")?;
                Ok(path.flatten())
            }
            MorType::Hom(ob_type) => Ok(Path::Id(self.elab(ob_type.as_ref())?)),
            _ => Err(format!("Cannot use morphsim type in discrete double theory: {mor_type:#?}")),
        }
    }
}

/// Elaborates into object operation in a discrete double theory.
impl CanElaborate<ObOp, QualifiedName> for Elaborator {
    fn elab(&self, op: &ObOp) -> Result<QualifiedName, String> {
        Err(format!("Cannot use operation in discrete double theory: {op:#?}"))
    }
}

/// Elaborates into object type in a discrete tabulator theory.
impl CanElaborate<ObType, TabObType> for Elaborator {
    fn elab(&self, ob_type: &ObType) -> Result<TabObType, String> {
        match ob_type {
            ObType::Basic(id) => Ok(TabObType::Basic((*id).into())),
            ObType::Tabulator(mor_type) => {
                Ok(TabObType::Tabulator(Box::new(self.elab(mor_type.as_ref())?)))
            }
            _ => Err(format!("Cannot use object type in discrete tabulator theory: {ob_type:#?}")),
        }
    }
}

/// Elaborates into morphism type in a discrete tabulator theory.
impl CanElaborate<MorType, TabMorType> for Elaborator {
    fn elab(&self, mor_type: &MorType) -> Result<TabMorType, String> {
        match mor_type {
            MorType::Basic(id) => Ok(TabMorType::Basic((*id).into())),
            MorType::Composite(_) => {
                Err("Composites not yet implemented for tabulator theories".into())
            }
            MorType::Hom(ob_type) => Ok(TabMorType::Hom(Box::new(self.elab(ob_type.as_ref())?))),
            _ => {
                Err(format!("Cannot use morphism type in discrete tabulator theory: {mor_type:#?}"))
            }
        }
    }
}

/// Elaborates into object operation in a discrete tabulator theory.
impl CanElaborate<ObOp, TabObOp> for Elaborator {
    fn elab(&self, op: &ObOp) -> Result<TabObOp, String> {
        Err(format!("Cannot use operation in discrete tabulator theory: {op:#?}"))
    }
}

/// Elaborates into object type in a modal double theory.
impl CanElaborate<ObType, ModalObType> for Elaborator {
    fn elab(&self, ob_type: &ObType) -> Result<ModalObType, String> {
        match ob_type {
            ObType::Basic(id) => Ok(ModeApp::new((*id).into())),
            ObType::ModeApp { modality, ob_type } => Ok({
                let ob_type: ModalObType = self.elab(ob_type.as_ref())?;
                ob_type.apply(promote_modality(*modality))
            }),
            _ => Err(format!("Cannot use object type in modal theory: {ob_type:#?}")),
        }
    }
}

/// Elaborates into morphism type in a modal double theory.
impl CanElaborate<MorType, ModalMorType> for Elaborator {
    fn elab(&self, mor_type: &MorType) -> Result<ModalMorType, String> {
        match mor_type {
            MorType::Basic(id) => Ok(ModeApp::new((*id).into()).into()),
            MorType::Hom(ob_type) => Ok(ShortPath::Zero(self.elab(ob_type.as_ref())?)),
            MorType::ModeApp { modality, mor_type } => Ok({
                let mor_type: ModalMorType = self.elab(mor_type.as_ref())?;
                mor_type.apply(promote_modality(*modality))
            }),
            _ => Err(format!("Cannot use morphism type in modal theory: {mor_type:#?}")),
        }
    }
}

/// Elaborates into an object operation in a modal double theory.
impl CanElaborate<ObOp, ModalObOp> for Elaborator {
    fn elab(&self, op: &ObOp) -> Result<ModalObOp, String> {
        match op {
            ObOp::Basic(id) => Ok(ModalObOp::generator((*id).into())),
        }
    }
}

pub(crate) fn expect_single_name(name: &QualifiedName) -> Ustr {
    match name.only() {
        Some(NameSegment::Text(text)) => text,
        _ => panic!("Only singleton names are currently supported in notebook types"),
    }
}

/// Quotes an object type in a discrete double theory.
impl CanQuote<QualifiedName, ObType> for Quoter {
    fn quote(&self, name: &QualifiedName) -> ObType {
        ObType::Basic(expect_single_name(name))
    }
}

/// Quotes a morphism type in a discrete double theory.
impl CanQuote<QualifiedPath, MorType> for Quoter {
    fn quote(&self, path: &QualifiedPath) -> MorType {
        match path {
            Path::Id(v) => MorType::Hom(Box::new(ObType::Basic(expect_single_name(v)))),
            Path::Seq(edges) => {
                if edges.len() == 1 {
                    MorType::Basic(expect_single_name(&edges.head))
                } else {
                    MorType::Composite(
                        edges.iter().map(|e| MorType::Basic(expect_single_name(e))).collect(),
                    )
                }
            }
        }
    }
}

/// Quotes an object type in a discrete tabulator theory.
impl CanQuote<TabObType, ObType> for Quoter {
    fn quote(&self, ob_type: &TabObType) -> ObType {
        match ob_type {
            TabObType::Basic(name) => ObType::Basic(expect_single_name(name)),
            TabObType::Tabulator(mor_type) => {
                ObType::Tabulator(Box::new(self.quote(mor_type.as_ref())))
            }
        }
    }
}

/// Quotes a morphism type in a discrete tabulator theory.
impl CanQuote<TabMorType, MorType> for Quoter {
    fn quote(&self, mor_type: &TabMorType) -> MorType {
        match mor_type {
            TabMorType::Basic(name) => MorType::Basic(expect_single_name(name)),
            TabMorType::Hom(ob_type) => MorType::Hom(Box::new(self.quote(ob_type.as_ref()))),
        }
    }
}

/// Quotes an object type in a modal theory.
impl CanQuote<ModalObType, ObType> for Quoter {
    fn quote(&self, app: &ModalObType) -> ObType {
        let mut quoted = ObType::Basic(expect_single_name(&app.arg));
        for modality in &app.modalities {
            quoted = ObType::ModeApp {
                modality: demote_modality(*modality),
                ob_type: quoted.into(),
            }
        }
        quoted
    }
}

/// Quotes a morphism type in a modal theory.
impl CanQuote<ModalMorType, MorType> for Quoter {
    fn quote(&self, mor_type: &ModalMorType) -> MorType {
        match mor_type {
            ShortPath::Zero(ob_type) => MorType::Hom(Box::new(self.quote(ob_type))),
            ShortPath::One(app) => {
                let mut quoted = MorType::Basic(expect_single_name(&app.arg));
                for modality in &app.modalities {
                    quoted = MorType::ModeApp {
                        modality: demote_modality(*modality),
                        mor_type: quoted.into(),
                    }
                }
                quoted
            }
        }
    }
}

/// A box containing a double theory of any kind.
///
/// Ideally the Wasm-bound [`DblTheory`] would just have a type parameter for the
/// underlying double theory, but `wasm-bindgen` does not support
/// [generics](https://github.com/rustwasm/wasm-bindgen/issues/3309). Instead, we
/// explicitly enumerate the supported kinds of double theories in this enum.
#[derive(From, TryInto)]
#[try_into(ref)]
pub enum DblTheoryBox {
    /// A discrete double theory.
    Discrete(Rc<theory::DiscreteDblTheory>),
    /// A discrete tabulator theory.
    DiscreteTab(Rc<theory::DiscreteTabTheory>),
    /// A modal double theory.
    Modal(Rc<theory::ModalDblTheory>),
}

/// Wasm binding for a double theory.
#[wasm_bindgen]
pub struct DblTheory(#[wasm_bindgen(skip)] pub DblTheoryBox);

impl DblTheory {
    /// Tries to get a discrete double theory.
    pub fn discrete(&self) -> Result<&Rc<theory::DiscreteDblTheory>, String> {
        (&self.0).try_into().map_err(|_| "Theory should be discrete".into())
    }

    /// Tries to convert into a theory usable by DoubleTT.
    pub fn try_into_tt(&self) -> Option<tt::theory::TheoryDef> {
        match &self.0 {
            DblTheoryBox::Discrete(th) => Some(tt::theory::TheoryDef::Discrete(th.clone())),
            DblTheoryBox::Modal(th) => Some(tt::theory::TheoryDef::Modal(th.clone())),
            _ => None,
        }
    }
}

#[wasm_bindgen]
impl DblTheory {
    /// Returns whether the theory contains the object type.
    #[wasm_bindgen(js_name = "hasObType")]
    pub fn has_ob_type(&self, ob_type: ObType) -> Result<bool, String> {
        all_the_same!(match &self.0 {
            DblTheoryBox::[Discrete, DiscreteTab, Modal](th) => {
                Ok(th.has_ob_type(&Elaborator.elab(&ob_type)?))
            }
        })
    }

    /// Returns whether the theory contains the morphism type.
    #[wasm_bindgen(js_name = "hasMorType")]
    pub fn has_mor_type(&self, mor_type: MorType) -> Result<bool, String> {
        all_the_same!(match &self.0 {
            DblTheoryBox::[Discrete, DiscreteTab, Modal](th) => {
                Ok(th.has_mor_type(&Elaborator.elab(&mor_type)?))
            }
        })
    }

    /// Gets the source of a morphism type.
    #[wasm_bindgen]
    pub fn src(&self, mor_type: MorType) -> Result<ObType, String> {
        all_the_same!(match &self.0 {
            DblTheoryBox::[Discrete, DiscreteTab, Modal](th) => {
                let mor_type = Elaborator.elab(&mor_type)?;
                Ok(Quoter.quote(&th.src_type(&mor_type)))
            }
        })
    }

    /// Gets the target of a morphism type.
    #[wasm_bindgen]
    pub fn tgt(&self, mor_type: MorType) -> Result<ObType, String> {
        all_the_same!(match &self.0 {
            DblTheoryBox::[Discrete, DiscreteTab, Modal](th) => {
                let mor_type = Elaborator.elab(&mor_type)?;
                Ok(Quoter.quote(&th.tgt_type(&mor_type)))
            }
        })
    }

    /// Gets the domain of an object operation.
    #[wasm_bindgen]
    pub fn dom(&self, op: ObOp) -> Result<ObType, String> {
        all_the_same!(match &self.0 {
            DblTheoryBox::[Discrete, DiscreteTab, Modal](th) => {
                let op = Elaborator.elab(&op)?;
                Ok(Quoter.quote(&th.ob_op_dom(&op)))
            }
        })
    }

    /// Gets the codomain of an object operation.
    #[wasm_bindgen]
    pub fn cod(&self, op: ObOp) -> Result<ObType, String> {
        all_the_same!(match &self.0 {
            DblTheoryBox::[Discrete, DiscreteTab, Modal](th) => {
                let op = Elaborator.elab(&op)?;
                Ok(Quoter.quote(&th.ob_op_cod(&op)))
            }
        })
    }

    /// Does the theory support instantiating models in other models?
    ///
    /// Eventually instantiation should be supported for every double doctrine
    /// and then this method can be removed.
    #[wasm_bindgen(js_name = "canInstantiateModels")]
    pub fn can_instantiate_models(&self) -> bool {
        !matches!(&self.0, DblTheoryBox::DiscreteTab(_))
    }
}

/// Mapping from object types to numerical indices.
///
/// Like [`MorTypeIndex`], this struct just compensates for the lack of hash maps
/// with arbitrary keys in JavaScript.
#[wasm_bindgen]
#[derive(Clone, Default)]
pub struct ObTypeIndex(HashMap<ObType, usize>);

#[wasm_bindgen]
impl ObTypeIndex {
    /// Creates a new object type index.
    #[wasm_bindgen(constructor)]
    pub fn new() -> Self {
        Default::default()
    }

    /// Returns whether the object type is set.
    #[wasm_bindgen(js_name = "has")]
    pub fn contains_key(&self, x: &ObType) -> bool {
        self.0.contains_key(x)
    }

    /// Gets the index of an object type, if set.
    #[wasm_bindgen]
    pub fn get(&self, x: &ObType) -> Option<usize> {
        self.0.get(x).copied()
    }

    /// Sets the index of an object type.
    #[wasm_bindgen(js_name = "set")]
    pub fn insert(&mut self, x: ObType, i: usize) {
        self.0.insert(x, i);
    }
}

/// Mapping from morphism types to numerical indices.
///
/// Like [`ObTypeIndex`], this struct just compensates for the lack of hash maps
/// with arbitrary keys in JavaScript.
#[wasm_bindgen]
#[derive(Clone, Default)]
pub struct MorTypeIndex(HashMap<MorType, usize>);

#[wasm_bindgen]
impl MorTypeIndex {
    /// Creates a new morphism type index.
    #[wasm_bindgen(constructor)]
    pub fn new() -> Self {
        Default::default()
    }

    /// Returns whether the morphism type is set.
    #[wasm_bindgen(js_name = "has")]
    pub fn contains_key(&self, m: &MorType) -> bool {
        self.0.contains_key(m)
    }

    /// Gets the index of a morphism type, if set.
    #[wasm_bindgen]
    pub fn get(&self, m: &MorType) -> Option<usize> {
        self.0.get(m).copied()
    }

    /// Sets the index of a morphism type.
    #[wasm_bindgen(js_name = "set")]
    pub fn insert(&mut self, m: MorType, i: usize) {
        self.0.insert(m, i);
    }
}