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 supplying 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:
theory Midpoint =
// A scroll is a theory with two special meta datums referencing a problem and a solution theory: ❙
meta ?MetaAnnotations?problemTheory ?Midpoint/Problem ❙
meta ?MetaAnnotations?solutionTheory ?Midpoint/Solution ❙
// You can specify those theories as nested theories of the scroll theory as such, but this is not required at all; it is just convention. ❙
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 =
// A solution theory always starts with including the problem theory: ❙
include ?Midpoint/Problem ❙
// Next, we can supply a label and a description to be used for the overall scroll:❙
meta ?MetaAnnotations?label "MidPoint" ❙
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}." ❙
// Here, the description uses MMT's interpolation feature by prefixing the double quotes with an "s".
This allows embedding arbitrary MMT terms within the string via ${...} where ... is an MMT term.
In FrameIT, we use such string interpolation to give the scroll a more dynamic flavor:
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.
For that we can use the MMT term `lverb P` that stands for "label verbalization" of P embedded into the description string via "${lverb P}".
Whenever the user reassigns the fact slot for P, the label verbalization will kick in again and adjust the result of "${lverb P}" to the label of the actually assigned fact.
And "${lverb P Q}" is syntactic sugar for "${lverb P}${lverb Q}", i.e., the mere concatenation (without whitespace). ❙
// Next, solution theories declare all facts that are acquired upon successful application: ❙
midpoint
: point ❘
= ⟨0.5 ⋅ (P _x + Q _x), 0.5 ⋅ (P _y + Q _y), 0.5 ⋅ (P _z + Q _z)⟩ ❘
meta ?MetaAnnotations?label s"Mid[${lverb P Q}]" ❘
meta ?MetaAnnotations?description s"The midpoint between points ${lverb P} and ${lverb Q}."
❙
❚
❚