System.Object[]

040e9a33 · ComFreek · 8b4d1167 · 040e9a33 · 040e9a33 · 040e9a33
Commit 040e9a33 authored 4 years ago by ComFreek
--- a/content/http..mathhub.info/FrameIT/frameworld/$Angle$Sum.omdoc.xz
+++ b/content/http..mathhub.info/FrameIT/frameworld/$Angle$Sum.omdoc.xz
--- a/content/http..mathhub.info/FrameIT/frameworld/$Midpoint.omdoc.xz
+++ b/content/http..mathhub.info/FrameIT/frameworld/$Midpoint.omdoc.xz
--- a/content/http..mathhub.info/FrameIT/frameworld/$Opposite$Len.omdoc.xz
+++ b/content/http..mathhub.info/FrameIT/frameworld/$Opposite$Len.omdoc.xz
--- a/content/http..mathhub.info/FrameIT/frameworld/$Supplementary$Angles.omdoc.xz
+++ b/content/http..mathhub.info/FrameIT/frameworld/$Supplementary$Angles.omdoc.xz
--- a/narration/Scrolls/MiscScrolls.omdoc
+++ b/narration/Scrolls/MiscScrolls.omdoc
 <?xml version="1.0" encoding="UTF-8"?>
-<omdoc base="http://mathhub.info/FrameIT/frameworld/Scrolls/MiscScrolls.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/MiscScrolls.mmt#0.0.0:1248.35.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/MiscScrolls.mmt#0.0.0:84.0.84"/></metadata>Miscellaneous scrolls for playing around/testing that don't have a good home yet</opaque><instruction text="namespace http://mathhub.info/FrameIT/frameworld"/><instruction text="fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta"/><mref name="[http://mathhub.info/FrameIT/frameworld?Midpoint]" target="http://mathhub.info/FrameIT/frameworld?Midpoint"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/MiscScrolls.mmt#165.5.0:179.5.14"/></metadata></mref></omdoc>
\ No newline at end of file
+<omdoc base="http://mathhub.info/FrameIT/frameworld/Scrolls/MiscScrolls.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/MiscScrolls.mmt#0.0.0:1241.36.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/MiscScrolls.mmt#0.0.0:84.0.84"/></metadata>Miscellaneous scrolls for playing around/testing that don't have a good home yet</opaque><instruction text="namespace http://mathhub.info/FrameIT/frameworld"/><instruction text="fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta"/><mref name="[http://mathhub.info/FrameIT/frameworld?Midpoint]" target="http://mathhub.info/FrameIT/frameworld?Midpoint"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/MiscScrolls.mmt#165.5.0:179.5.14"/></metadata></mref></omdoc>
\ No newline at end of file
--- a/narration/Scrolls/SupplementaryAngles.omdoc
+++ b/narration/Scrolls/SupplementaryAngles.omdoc
 <?xml version="1.0" encoding="UTF-8"?>
-<omdoc base="http://mathhub.info/FrameIT/frameworld/Scrolls/SupplementaryAngles.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/SupplementaryAngles.mmt#0.0.0:1619.45.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><instruction text="namespace http://mathhub.info/FrameIT/frameworld"/><instruction text="fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta"/><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/SupplementaryAngles.mmt#78.3.0:245.11.0"/></metadata><scope>\
+<omdoc base="http://mathhub.info/FrameIT/frameworld/Scrolls/SupplementaryAngles.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/SupplementaryAngles.mmt#0.0.0:1612.46.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><instruction text="namespace http://mathhub.info/FrameIT/frameworld"/><instruction text="fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta"/><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/SupplementaryAngles.mmt#78.3.0:245.11.0"/></metadata><scope>\
       \ D
        \
 ________\_________

--- a/narration/Scrolls/TriangleScrolls.omdoc
+++ b/narration/Scrolls/TriangleScrolls.omdoc
 <?xml version="1.0" encoding="UTF-8"?>
-<omdoc base="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#0.0.0:4687.132.3"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#0.0.0:47.0.47"/></metadata>Modular scrolls having to do with triangles</opaque><instruction text="namespace http://mathhub.info/FrameIT/frameworld"/><instruction text="fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta"/><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#128.5.0:322.14.0"/></metadata>A blueprint problem theory for triangle scrolls
+<omdoc base="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#0.0.0:4666.135.3"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#0.0.0:47.0.47"/></metadata>Modular scrolls having to do with triangles</opaque><instruction text="namespace http://mathhub.info/FrameIT/frameworld"/><instruction text="fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta"/><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#128.5.0:322.14.0"/></metadata>A blueprint problem theory for triangle scrolls
       B
      /|
     / |
@@ -9,4 +9,4 @@

  (nicer image: https://en.wikipedia.org/wiki/Right_triangle#/media/File:Rtriangle.svg)</opaque><mref name="[http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem]" target="http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#324.15.0:359.15.35"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#511.21.0:667.23.77"/></metadata>A blueprint problem theory for triangle scrolls that require a right angle

-   We use ?TriangleScroll_GeneralProblem and demand the angle at C to be 90°</opaque><mref name="[http://mathhub.info/FrameIT/frameworld?TriangleScroll_RightAngledProblem]" target="http://mathhub.info/FrameIT/frameworld?TriangleScroll_RightAngledProblem"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#669.24.0:708.24.39"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?AngleSum]" target="http://mathhub.info/FrameIT/frameworld?AngleSum"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#941.33.0:955.33.14"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?OppositeLen]" target="http://mathhub.info/FrameIT/frameworld?OppositeLen"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#2247.67.0:2264.67.17"/></metadata></mref></omdoc>
\ No newline at end of file
+   We use ?TriangleScroll_GeneralProblem and demand the angle at C to be 90°</opaque><mref name="[http://mathhub.info/FrameIT/frameworld?TriangleScroll_RightAngledProblem]" target="http://mathhub.info/FrameIT/frameworld?TriangleScroll_RightAngledProblem"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#669.24.0:708.24.39"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?AngleSum]" target="http://mathhub.info/FrameIT/frameworld?AngleSum"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#941.33.0:955.33.14"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?OppositeLen]" target="http://mathhub.info/FrameIT/frameworld?OppositeLen"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#2240.68.0:2257.68.17"/></metadata></mref></omdoc>
\ No newline at end of file
--- a/source/Scrolls/MiscScrolls.mmt
+++ b/source/Scrolls/MiscScrolls.mmt
@@ -4,6 +4,9 @@ namespace http://mathhub.info/FrameIT/frameworld ❚
 fixmeta ?FrameworldMeta ❚

 theory Midpoint =
+    meta ?MetaAnnotations?problemTheory ?Midpoint/Problem ❙
+    meta ?MetaAnnotations?solutionTheory ?Midpoint/Solution ❙
+
    theory Problem =
        P
            : point ❘
@@ -22,8 +25,6 @@ theory Midpoint =
        include ?Midpoint/Problem ❙

        meta ?MetaAnnotations?label "MidPoint" ❙
-        meta ?MetaAnnotations?problemTheory ?Midpoint/Problem ❙
-        meta ?MetaAnnotations?solutionTheory ?Midpoint/Solution ❙
        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

--- a/source/Scrolls/README.md
+++ b/source/Scrolls/README.md
@@ -3,17 +3,23 @@
 ## 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.
+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.
+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 =
+    // 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 ❙
+           like a label and description. ❙

        P
            : point ❘
@@ -29,29 +35,25 @@ theory Midpoint =
    ❚

    theory Solution =
-        // note: include the problem theory before spelling out the meta annotations
-                 to have access to the facts formalized in the problem theory ❙
+        // A solution theory always starts with including the problem theory: ❙
        include ?Midpoint/Problem ❙

-        // the next meta annotations (to the theory) actually make this theory into a scroll: 
-           We specify the Problem and Solution theories  ❙
-
+        // Next, we can supply a label and a description to be used for the overall scroll:❙
        meta ?MetaAnnotations?label "MidPoint" ❙
-        meta ?MetaAnnotations?problemTheory ?Midpoint/Problem ❙
-        meta ?MetaAnnotations?solutionTheory ?Midpoint/Solution ❙
+        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 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.
+          In FrameIT, we use such string interpolation to give the scroll a more dynamic flavor:
          
-          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}." ❙
+          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 ❘

--- a/source/Scrolls/SupplementaryAngles.mmt
+++ b/source/Scrolls/SupplementaryAngles.mmt
@@ -11,6 +11,9 @@ A         B        C
 The scroll encodes "angle ABD + angle DBC = 180°", or rather, "angle DBC = 180° - angle ABD"
 ❚
 theory SupplementaryAngles =
+    meta ?MetaAnnotations?problemTheory ?SupplementaryAngles/Problem ❙
+    meta ?MetaAnnotations?solutionTheory ?SupplementaryAngles/Solution ❙
+
    theory Problem =
        A: point ❘ meta ?MetaAnnotations?label "A" ❙
        B: point ❘ meta ?MetaAnnotations?label "B" ❙
@@ -30,8 +33,6 @@ theory SupplementaryAngles =

    theory Solution =
        meta ?MetaAnnotations?label "AngleSum" ❙
-        meta ?MetaAnnotations?problemTheory ?SupplementaryAngles/Problem ❙
-        meta ?MetaAnnotations?solutionTheory ?SupplementaryAngles/Solution ❙
        meta ?MetaAnnotations?description "Supplementary angles add up to 180 degree " ❙

        include ?SupplementaryAngles/Problem ❙

--- a/source/Scrolls/TriangleScrolls.mmt
+++ b/source/Scrolls/TriangleScrolls.mmt
@@ -32,6 +32,9 @@ theory TriangleScroll_RightAngledProblem =
 ❚

 theory AngleSum =
+    meta ?MetaAnnotations?problemTheory ?AngleSum/Problem ❙
+    meta ?MetaAnnotations?solutionTheory ?AngleSum/Solution ❙
+
    theory Problem =
        include ?TriangleScroll_GeneralProblem ❙

@@ -52,8 +55,6 @@ theory AngleSum =
        include ?AngleSum/Problem ❙

        meta ?MetaAnnotations?label "AngleSum" ❙
-        meta ?MetaAnnotations?problemTheory ?AngleSum/Problem ❙
-        meta ?MetaAnnotations?solutionTheory ?AngleSum/Solution ❙
        meta ?MetaAnnotations?description s"Given a triangle ${lverb A B C} and two known angles, we can deduce the missing angle by the sum of interior angles in triangles always being 180°" ❙

        angleBCA
@@ -66,6 +67,9 @@ theory AngleSum =
 ❚

 theory OppositeLen =
+    meta ?MetaAnnotations?problemTheory ?OppositeLen/Problem ❙
+    meta ?MetaAnnotations?solutionTheory ?OppositeLen/Solution ❙
+
    theory Problem =
        include ?TriangleScroll_RightAngledProblem ❙
    
@@ -86,8 +90,6 @@ theory OppositeLen =
        include ?OppositeLen/Problem ❙

        meta ?MetaAnnotations?label "OppositeLen" ❙
-        meta ?MetaAnnotations?problemTheory ?OppositeLen/Problem ❙
-        meta ?MetaAnnotations?solutionTheory ?OppositeLen/Solution ❙
        meta ?MetaAnnotations?description s"Given a triangle ${lverb A B C} right angled at ${lverb C}, the distance ${lverb A B} can be computed from the angle at ${lverb B} and the distance ${lverb B C}" ❙
    
        deducedLineCA
@@ -101,6 +103,9 @@ theory OppositeLen =

 // Doesn't typecheck, not sure why ❚
 // theory Pythagoras =
+    meta ?MetaAnnotations?problemTheory ?Pythagoras/Problem ❙
+    meta ?MetaAnnotations?solutionTheory ?Pythagoras/Solution ❙
+
    theory Problem =
        include ?TriangleScroll_RightAngledProblem ❙
    
@@ -119,8 +124,6 @@ theory OppositeLen =
        include ?Pythagoras/Problem ❙

        meta ?MetaAnnotations?label "Pythagoras" ❙
-        meta ?MetaAnnotations?problemTheory ?Pythagoras/Problem ❙
-        meta ?MetaAnnotations?solutionTheory ?Pythagoras/Solution ❙
        meta ?MetaAnnotations?description "Given a ABC right-angled at C and lengths of both legs, we can compute the length of the hypotenuse via Pythagora's theorem" ❙

        deducedHypotenuse