work

b9aadd59 · ComFreek · 4ed9b3d9 · b9aadd59 · b9aadd59 · b9aadd59
Commit b9aadd59 authored 4 years ago by ComFreek
--- a/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$My$Scroll.omdoc.xz
+++ b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$My$Scroll.omdoc.xz
--- a/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Sample$Situation$Space.omdoc.xz
+++ b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Sample$Situation$Space.omdoc.xz
--- a/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Sample$Situation$Theory.omdoc.xz
+++ b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Sample$Situation$Theory.omdoc.xz
--- a/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Situation$Space.omdoc.xz
+++ b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Situation$Space.omdoc.xz
--- a/errors/mmt-omdoc/IntegrationTests/SituationTheory.mmt.err
+++ b/errors/mmt-omdoc/IntegrationTests/SituationTheory.mmt.err
-<errors>
-</errors>
--- a/narration/IntegrationTests/SituationTheory.omdoc
+++ b/narration/IntegrationTests/SituationTheory.omdoc
 <?xml version="1.0" encoding="UTF-8"?>
-<omdoc base="http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.mmt#0.0.0:1087.44.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/integrationtests"/><instruction text="import frameworld http://mathhub.info/FrameIT/frameworld"/><instruction text="fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta"/><mref name="[http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory]" target="http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.mmt#194.6.0:221.6.27"/></metadata></mref></omdoc>
\ No newline at end of file
+<omdoc base="http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.mmt#0.0.0:1966.78.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/integrationtests"/><instruction text="import frameworld http://mathhub.info/FrameIT/frameworld"/><instruction text="fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta"/><mref name="[http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace]" target="http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.mmt#194.6.0:220.6.26"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll]" target="http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.mmt#1535.56.0:1549.56.14"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace]" target="http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.mmt#1661.64.0:1681.64.20"/></metadata></mref></omdoc>
\ No newline at end of file
--- a/relational/IntegrationTests/SituationTheory.rel
+++ b/relational/IntegrationTests/SituationTheory.rel
 document http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.omdoc
-Declares http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.omdoc http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory
+Declares http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.omdoc http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace
+Declares http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.omdoc http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll
+Declares http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.omdoc http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace
--- a/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$My$Scroll.rel
+++ b/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$My$Scroll.rel
+theory http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll
+HasMeta http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll http://mathhub.info/FrameIT/frameworld?FrameworldMeta
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll?Problem
+theory http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll/Problem
+HasMeta http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll/Problem http://mathhub.info/FrameIT/frameworld?FrameworldMeta
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll/Problem http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll/Problem?a
+constant http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll/Problem?a
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll?Solution
+theory http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll/Solution
+HasMeta http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll/Solution http://mathhub.info/FrameIT/frameworld?FrameworldMeta
+Includes http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll/Solution http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll/Problem
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll/Solution http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll/Solution?c
+constant http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll/Solution?c
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll/Solution?c?definition http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll/Problem?a?type
--- a/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Sample$Situation$Space.rel
+++ b/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Sample$Situation$Space.rel
--- a/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Sample$Situation$Theory.rel
+++ b/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Sample$Situation$Theory.rel
@@ -6,6 +6,8 @@ dataconstructor http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSi
 dataconstructor http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?angleBAC
 theory http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory
 HasMeta http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory http://mathhub.info/FrameIT/frameworld?FrameworldMeta
+Includes http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory http://mathhub.info/FrameIT/frameworld?OppositeLen
+Includes http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory http://mathhub.info/FrameIT/frameworld?AngleSum
 Declares http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?A
 constant http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?A
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?A?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type

--- a/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Situation$Space.rel
+++ b/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Situation$Space.rel
+theory http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace
+HasMeta http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace http://mathhub.info/FrameIT/frameworld?FrameworldMeta
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace?RootSituationTheory
+theory http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/RootSituationTheory
+HasMeta http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/RootSituationTheory http://mathhub.info/FrameIT/frameworld?FrameworldMeta
+Includes http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/RootSituationTheory http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/RootSituationTheory http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/RootSituationTheory?b
+constant http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/RootSituationTheory?b
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/RootSituationTheory http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/RootSituationTheory?v
+HasDomain http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/RootSituationTheory/v http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll/Problem
+HasCodomain http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/RootSituationTheory/v http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/RootSituationTheory
+view http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/RootSituationTheory/v
+HasViewFrom http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/RootSituationTheory http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll/Problem
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/RootSituationTheory/v http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/RootSituationTheory/v?[http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll/Problem]/a
+constant http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/RootSituationTheory/v?[http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll/Problem]/a
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/RootSituationTheory/v?[http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll/Problem]/a?definition http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/RootSituationTheory?b?type
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace?PushedOutSituationTheory
+theory http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/PushedOutSituationTheory
+HasMeta http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/PushedOutSituationTheory http://mathhub.info/FrameIT/frameworld?FrameworldMeta
+Includes http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/PushedOutSituationTheory http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/RootSituationTheory
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/PushedOutSituationTheory http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/PushedOutSituationTheory?c
+constant http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/PushedOutSituationTheory?c
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/PushedOutSituationTheory?c?definition http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/RootSituationTheory?b?type
--- a/source/IntegrationTests/SituationTheory.mmt
+++ b/source/IntegrationTests/SituationTheory.mmt
@@ -4,42 +4,76 @@ import frameworld http://mathhub.info/FrameIT/frameworld ❚

 fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta ❚

-theory SampleSituationTheory =
-    // planar triangle in R^2 ❙
-
-    A
-        : point ❘
-        = ⟨0.0, 0.0, 0.0⟩ ❘
-        meta frameworld:?MetaAnnotations?label "A"
-   ❙
-
-    B
-        : point ❘
-        = ⟨3.0, 3.0, 0.0⟩ ❘
-        meta frameworld:?MetaAnnotations?label "B"
-   ❙
-
-    C
-        : point ❘
-        = ⟨0.0, 3.0, 0.0⟩ ❘
-        meta frameworld:?MetaAnnotations?label "C"
-   ❙
-
-   distanceBC
-        : Σ x:ℝ. ⊦ (d- B C ≐ x) ❘
-        = ⟨3.0, sketch "calculated by ComFreek by hand"⟩ ❘
-        meta frameworld:?MetaAnnotations?label "BC"
-   ❙
-
-   angleABC
-        : Σ β:ℝ. ⊦ ( ∠ A,B,C ) ≐ β ❘
-        = ⟨45.0, sketch "calculated by ComFreek by hand"⟩ ❘
-        meta frameworld:?MetaAnnotations?label "∠ABC"
-   ❙
-
-   angleBAC
-        : Σ β:ℝ. ⊦ ( ∠ A,B,C ) ≐ β ❘
-        = ⟨45.0, sketch "calculated by ComFreek by hand"⟩ ❘
-        meta frameworld:?MetaAnnotations?label "∠BAC"
-   ❙
+theory SampleSituationSpace =
+    theory Root =
+        // planar triangle in R^2 ❙
+        include ☞frameworld:?OppositeLen ❙
+        include ☞frameworld:?AngleSum ❙
+
+        A
+            : point ❘
+            = ⟨0.0, 0.0, 0.0⟩ ❘
+            meta frameworld:?MetaAnnotations?label "𝔸"
+        ❙
+
+        B
+            : point ❘
+            = ⟨3.0, 3.0, 0.0⟩ ❘
+            meta frameworld:?MetaAnnotations?label "𝔹"
+        ❙
+
+        C
+            : point ❘
+            = ⟨0.0, 3.0, 0.0⟩ ❘
+            meta frameworld:?MetaAnnotations?label "ℂ"
+        ❙
+
+        distanceBC
+            : Σ x:ℝ. ⊦ (d- B C ≐ x) ❘
+            = ⟨3.0, sketch "calculated by ComFreek by hand"⟩ ❘
+            meta frameworld:?MetaAnnotations?label "𝔹ℂ"
+        ❙
+
+        angleABC
+            : Σ β:ℝ. ⊦ ( ∠ A,B,C ) ≐ β ❘
+            = ⟨45.0, sketch "calculated by ComFreek by hand"⟩ ❘
+            meta frameworld:?MetaAnnotations?label "∠𝔸𝔹ℂ"
+        ❙
+
+        angleBAC
+            : Σ β:ℝ. ⊦ ( ∠ B,A,C ) ≐ β ❘
+            = ⟨45.0, sketch "calculated by ComFreek by hand"⟩ ❘
+            meta frameworld:?MetaAnnotations?label "∠ℬ𝔸ℂ"
+        ❙
+
+        rightAngledC
+            : ⊦ ( ∠ B,C,A ) ≐ 90.0 ❘
+            = sketch "calculated by ComFreek by hand, hopefully correct" ❘
+            meta frameworld:?MetaAnnotations?label "∟ℂ"
+        ❙
+    ❚
+❚
+
+theory MyScroll =
+  theory Problem = a: type ❙❚
+  theory Solution =
+    include ?MyScroll/Problem ❙
+    c: type ❘ = a❙
+  ❚
 ❚
+
+theory SituationSpace =
+  theory RootSituationTheory =
+    include ?MyScroll ❙
+    b: type ❙
+
+    view v : ?MyScroll/Problem -> ?SituationSpace/RootSituationTheory =
+      a = b ❙
+    ❚
+  ❚
+
+  theory PushedOutSituationTheory =
+    include ?SituationSpace/RootSituationTheory ❙
+    c: type ❘ = b ❙
+  ❚
+❚
\ No newline at end of file