README.md

# UFrameIT Scrolls

## How to write one

Let's walk through an example of writing a scroll.
The scroll we will be writing can be found in `MiscScrolls.mmt` at time of writing, albeit without the documentary comments we will be making here.

Let us write a scroll "Midpoint" that requires two points `P` and `Q` as input, and that gives you upon application the midpoint between those points.

```mmt
theory Midpoint =
    theory Problem =
        // Declare all required fact inputs here.

           For every fact, you may (but are not required to) give some meta information
           like a label and description ❙

        P
            : point ❘
            meta ?MetaAnnotations?label "P" ❘
            meta ?MetaAnnotations?description "Some arbitrary input point"
        ❙

        Q
            : point ❘
            meta ?MetaAnnotations?label "Q" ❘
            meta ?MetaAnnotations?description "Some other arbitrary input point"
        ❙
    ❚

    theory Solution =
        // note: include the problem theory before spelling out the meta annotations
                 to have access to the facts formalized in the problem theory ❙
        include ?Midpoint/Problem ❙

        meta ?MetaAnnotations?label "MidPoint" ❙
        meta ?MetaAnnotations?problemTheory ?Midpoint/Problem ❙
        meta ?MetaAnnotations?solutionTheory ?Midpoint/Solution ❙


       // In the next meta datum string we prefix the double quotes by an "s"
          to be able to make use of string interpolation. Concretely, this makes
          the scroll dynamic: if the user fills the first P fact slot by a point
          with label A, then the scroll description should also talk about A, not P.
          
          Hence, we use "${lverb P}", where by P we refer to the fact constant of P
          as included by the problem theory. Read this as "label verbalization of P".
          
          And "${lverb P Q}" is syntactic sugar for "${lverb P}${lverb Q}", i.e., the mere
          concatenation (without whitespace). ❙
        meta ?MetaAnnotations?description s"Our MidPoint scroll that given two points ${lverb P} and ${lverb Q} computes the midpoint of the line ${lverb P Q}." ❙

        midpoint
            : point ❘
            = ⟨0.5 ⋅ (P_x + Q_x), 0.5 ⋅ (P_x + Q_x), 0.5 ⋅ (P_x + Q_x)⟩ ❘
            meta ?MetaAnnotations?label s"Mid[${lverb P Q}]" ❘
            meta ?MetaAnnotations?description s"The midpoint between points ${lverb P} and ${lverb Q}."
        ❙
    ❚
❚
```