Programmatically creating MMT content (checklist)

Most of the time, MMT content stems from building .mmt files via the mmt-omdoc build target. But there are some scenarios where you want to construct MMT content (e.g. theories, views, constants) programmatically:

• Importers importing content from other systems (e.g. Coq, Isabelle, Mizar) to MMT
• Diagram operators: effectively these are Scala functions transforming diagrams of MMT theories and views, hence they inherently need to construct new theories and views.
• CRUD interfaces using MMT as a knowledge database: these interfaces might contain commands to create new constants and make them known to MMT. Examples include the FrameIT MMT Server, mmt-glf, mmt-interviews.
• Unit tests feeding algorithms sample MMT content as input

There are some subtle patterns to follow and pitfalls to watch out for when creating MMT content programmatically. Ignoring them can lead you to time-consuming debugging journeys. Hence, this page documents those patterns.

• use the ctrl.add(...) (+ ctrl.endAdd(...)) pattern for almost anything. These are central methods content needs to go through for being made consistently known throughout all of MMT.

  • General pattern for structural element se:

    1. ctrl.add(se)
    2. if se is a ContainerElement[_] (e.g. Theory, View, Structure): add all of its children via the same pattern
    3. if se is a ContainerElement[_] (e.g. Theory, View, Structure -- Includes are Structures, too!): call ctrl.endAdd(se)

    MMT is currently coded with the invariant in mind that after ctr.endAdd no more children are added to container elements. Might break CRUD interface applications. It's best to create container element in a single go, if possible.

  • Example: creating a new theory with a single constants

    val thy = Theory.empty(doc, name, Some(Path.parseM("...")))
    ctrl.add(thy)
    
    // E.g. first add some include    
    val incl = Include(Path.parseM("path to theory to include"), thy.path)
    ctrl.add(incl)
    ctrl.endAdd(incl)  // !! IMPORTANT !! Includes are structures, hence ContainerElement[_]s
                       // Forgetting it may lead to some implicit morphims not getting added!
    
    // E.g. then add a constant
    ctrl.add(Constant(...))
    
    // We're done with adding children, now close the theory
    ctrl.endAdd(thy)

  • Background info: pairs of begin/end functions are a general theme within the MMT code base. They appear in the MMTStructureChecker, the Elaborator, and the Library. The end functions mostly are only applicable on ContainerElement[_]s

• use Include.assignment(...) for includes in views. Using the normal Include(...) apply methods does not work for includes in views since they set the isImplicit flag to true. But includes with isImplicit == true throw errors in views (because it doesn't make sense there).

• watch out for names of assignments in views. If you have a view v: S -> T and c is a constant in S (i.e. its path is ...?S?c), then an assignment c := E in v is a FinalConstant with name LocalName(mpath to ?S) / LocalName(<local name of c>) (often pretty-printed as [...?S]?c). And if you got another constant d from R, which is included into S, then the name of an assignment to it in v looks like LocalName(mpath to ?R) / <local name of c>