diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Angle$Sum.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Angle$Sum.omdoc.xz index d98c98eecc4aeb98be81d644f463265ff986bcb2..1e4fe2b8b8cc5f46ea58940a11bc138e79e3f1f3 100644 Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Angle$Sum.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Angle$Sum.omdoc.xz differ diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Midpoint.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Midpoint.omdoc.xz index e08aec6cdbc4697c1a763635ad859889a7c3d7dd..48d3d35101ce8452f38170f7c4f430c0858b4d32 100644 Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Midpoint.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Midpoint.omdoc.xz differ diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Opposite$Len.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Opposite$Len.omdoc.xz index 24d2ddbb478e139f3bb73cfbd87ebbaffd5b3ecd..da09733b6672b342a04775053ba91cb1395538a0 100644 Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Opposite$Len.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Opposite$Len.omdoc.xz differ diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Supplementary$Angles.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Supplementary$Angles.omdoc.xz index b5d7c29c08a210200354b371cb7f1eb9964ad72e..158099d7784d33707b4c1a4a0754e097a3f9526c 100644 Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Supplementary$Angles.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Supplementary$Angles.omdoc.xz differ diff --git a/narration/Scrolls/MiscScrolls.omdoc b/narration/Scrolls/MiscScrolls.omdoc index 5cfc39fc9e597b8fa2336297a87eac1266b4f031..d967130bcf8c7289799ef1b9b055a69f05bdc9db 100644 --- a/narration/Scrolls/MiscScrolls.omdoc +++ b/narration/Scrolls/MiscScrolls.omdoc @@ -1,2 +1,2 @@ <?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 diff --git a/narration/Scrolls/SupplementaryAngles.omdoc b/narration/Scrolls/SupplementaryAngles.omdoc index add781f09c93c48fc58f4ec910848aeb563b160a..aa05b40c5c058594fad7a795c2ec04cccaf1edd8 100644 --- a/narration/Scrolls/SupplementaryAngles.omdoc +++ b/narration/Scrolls/SupplementaryAngles.omdoc @@ -1,5 +1,5 @@ <?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 \ ________\_________ diff --git a/narration/Scrolls/TriangleScrolls.omdoc b/narration/Scrolls/TriangleScrolls.omdoc index 9c97eca948588c8bd16462045f8aed90f98df203..9f6f7d5711365e02fedd14dcf72757cc90fa538c 100644 --- a/narration/Scrolls/TriangleScrolls.omdoc +++ b/narration/Scrolls/TriangleScrolls.omdoc @@ -1,5 +1,5 @@ <?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 diff --git a/source/Scrolls/MiscScrolls.mmt b/source/Scrolls/MiscScrolls.mmt index 412444a5fea73789f717dadf70a47d23d782e0ac..19a535dc34f0f9cb1cb3e3f655f32d88d9cff829 100644 --- 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 diff --git a/source/Scrolls/README.md b/source/Scrolls/README.md index 95e8ed120b3fd9198eb22bae7c15dc95316d35bf..df4a964df9bde9872445f442af2398f69dd695ff 100644 --- 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 ☠diff --git a/source/Scrolls/SupplementaryAngles.mmt b/source/Scrolls/SupplementaryAngles.mmt index e64358543c69f3feca94940fb7322983e4940e79..ebadc26333279d11a0643114ca5189773e589fa8 100644 --- 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 ♠diff --git a/source/Scrolls/TriangleScrolls.mmt b/source/Scrolls/TriangleScrolls.mmt index 74768140fc297724f4258b4b8fd2eb2bd113a1f3..94a9ec00fb2cd1f0bf3ad0121fde9d7060366b51 100644 --- 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