add integration tests

df7dcdd8 · ComFreek · 0057987c · df7dcdd8 · df7dcdd8 · df7dcdd8
Commit df7dcdd8 authored 4 years ago by ComFreek
--- a/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Close$Gap$Test_$Codomain.omdoc.xz
+++ b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Close$Gap$Test_$Codomain.omdoc.xz
--- a/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Expected$Type$Test_$Codomain.omdoc.xz
+++ b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Expected$Type$Test_$Codomain.omdoc.xz
--- a/errors/mmt-omdoc/IntegrationTests/.err
+++ b/errors/mmt-omdoc/IntegrationTests/.err
+<errors>
+</errors>
--- a/errors/mmt-omdoc/IntegrationTests/CloseGapTests.mmt.err
+++ b/errors/mmt-omdoc/IntegrationTests/CloseGapTests.mmt.err
+<errors>
+</errors>
--- a/errors/mmt-omdoc/IntegrationTests/ExpectedTypeTests.mmt.err
+++ b/errors/mmt-omdoc/IntegrationTests/ExpectedTypeTests.mmt.err
+<errors>
+</errors>
--- a/narration/IntegrationTests/CloseGapTests.omdoc
+++ b/narration/IntegrationTests/CloseGapTests.omdoc
+<?xml version="1.0" encoding="UTF-8"?>
+<omdoc base="http://mathhub.info/FrameIT/frameworld/IntegrationTests/CloseGapTests.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/IntegrationTests/CloseGapTests.mmt#0.0.0:295.9.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="fixmeta http://mathhub.info/FrameIT/frameworld?FactCollection"/><mref name="[http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapTest_Codomain]" target="http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapTest_Codomain"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/IntegrationTests/CloseGapTests.mmt#134.4.0:161.4.27"/></metadata></mref></omdoc>
\ No newline at end of file
--- a/narration/IntegrationTests/ExpectedTypeTests.omdoc
+++ b/narration/IntegrationTests/ExpectedTypeTests.omdoc
+<?xml version="1.0" encoding="UTF-8"?>
+<omdoc base="http://mathhub.info/FrameIT/frameworld/IntegrationTests/ExpectedTypeTests.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/IntegrationTests/ExpectedTypeTests.mmt#0.0.0:327.15.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="fixmeta http://mathhub.info/FrameIT/frameworld?FactCollection"/><mref name="[http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain]" target="http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/IntegrationTests/ExpectedTypeTests.mmt#134.4.0:165.4.31"/></metadata></mref></omdoc>
\ No newline at end of file
--- a/relational/IntegrationTests/.rel
+++ b/relational/IntegrationTests/.rel
+document http://mathhub.info/FrameIT/frameworld/IntegrationTests
+Declares http://mathhub.info/FrameIT/frameworld/IntegrationTests http://mathhub.info/FrameIT/frameworld/IntegrationTests/CloseGapTests.omdoc
+Declares http://mathhub.info/FrameIT/frameworld/IntegrationTests http://mathhub.info/FrameIT/frameworld/IntegrationTests/ExpectedTypeTests.omdoc
--- a/relational/IntegrationTests/CloseGapTests.rel
+++ b/relational/IntegrationTests/CloseGapTests.rel
+document http://mathhub.info/FrameIT/frameworld/IntegrationTests/CloseGapTests.omdoc
+Declares http://mathhub.info/FrameIT/frameworld/IntegrationTests/CloseGapTests.omdoc http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapTest_Codomain
--- a/relational/IntegrationTests/ExpectedTypeTests.rel
+++ b/relational/IntegrationTests/ExpectedTypeTests.rel
+document http://mathhub.info/FrameIT/frameworld/IntegrationTests/ExpectedTypeTests.omdoc
+Declares http://mathhub.info/FrameIT/frameworld/IntegrationTests/ExpectedTypeTests.omdoc http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain
--- a/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Close$Gap$Test_$Codomain.rel
+++ b/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Close$Gap$Test_$Codomain.rel
+dataconstructor http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapTest_Codomain?a
+dataconstructor http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapTest_Codomain?b
+datatypeconstructor http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapTest_Codomain?complexAngleFact
+theory http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapTest_Codomain
+HasMeta http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapTest_Codomain http://mathhub.info/FrameIT/frameworld?FactCollection
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapTest_Codomain http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapTest_Codomain?a
+constant http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapTest_Codomain?a
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapTest_Codomain?a?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapTest_Codomain?a?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapTest_Codomain http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapTest_Codomain?b
+constant http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapTest_Codomain?b
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapTest_Codomain?b?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapTest_Codomain?b?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapTest_Codomain http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapTest_Codomain?complexAngleFact
+constant http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapTest_Codomain?complexAngleFact
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapTest_Codomain?complexAngleFact?definition http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapTest_Codomain?b?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapTest_Codomain?complexAngleFact?definition http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapTest_Codomain?a?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapTest_Codomain?complexAngleFact?definition http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapTest_Codomain?b?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapTest_Codomain?complexAngleFact?definition http://mathhub.info/FrameIT/frameworld?AngleFact?angleFact?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapTest_Codomain?complexAngleFact?definition http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapTest_Codomain?a?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapTest_Codomain?complexAngleFact?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapTest_Codomain?complexAngleFact?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
--- a/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Expected$Type$Test_$Codomain.rel
+++ b/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Expected$Type$Test_$Codomain.rel
+dataconstructor http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?pA
+dataconstructor http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?pB
+dataconstructor http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?pC
+dataconstructor http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?pangleABC_v
+dataconstructor http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?arcsin
+dataconstructor http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?one_half
+dataconstructor http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?pangleComplexExpression
+theory http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain
+HasMeta http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain http://mathhub.info/FrameIT/frameworld?FactCollection
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?pA
+constant http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?pA
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?pA?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?pA?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?pB
+constant http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?pB
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?pB?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?pB?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?pC
+constant http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?pC
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?pC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?pC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?pangleABC_v
+constant http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?pangleABC_v
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?pangleABC_v?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?arcsin
+constant http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?arcsin
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?arcsin?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?one_half
+constant http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?one_half
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?one_half?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?pangleComplexExpression
+constant http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?pangleComplexExpression
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?pangleComplexExpression?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?pangleComplexExpression?definition http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?arcsin?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?pangleComplexExpression?definition http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?one_half?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?pangleComplexExpression?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
--- a/source/IntegrationTests/CloseGapTests.mmt
+++ b/source/IntegrationTests/CloseGapTests.mmt
+namespace http://mathhub.info/FrameIT/frameworld/integrationtests ❚
+
+fixmeta http://mathhub.info/FrameIT/frameworld?FactCollection ❚
+
+theory CloseGapTest_Codomain =
+    a: ℝ ❘ = 42.0 ❙
+    b: ℝ ❘ = 4242.0 ❙
+    complexAngleFact = angleFact ⟨1.0, 2.0, 3.0⟩ ⟨4.0, 5.0, 6.0⟩ ⟨a, b, 0.0⟩ (90.0) ❙
+❚
--- a/source/IntegrationTests/ExpectedTypeTests.mmt
+++ b/source/IntegrationTests/ExpectedTypeTests.mmt
+namespace http://mathhub.info/FrameIT/frameworld/integrationtests ❚
+
+fixmeta http://mathhub.info/FrameIT/frameworld?FactCollection ❚
+
+theory ExpectedTypeTest_Codomain =
+    pA: point ❙
+    pB: point ❙
+    pC: point ❙
+
+    pangleABC_v: ℝ ❙
+
+    arcsin: ℝ ⟶ ℝ ❙
+    one_half: ℝ ❙
+    pangleComplexExpression = arcsin one_half❙
+❚