Skip to content
Snippets Groups Projects
Commit 891df920 authored by ComFreek's avatar ComFreek
Browse files

document situation spaces

parent 2c32b722
No related branches found
No related tags found
1 merge request!1Added new Scrolls and new Theories
Hide whitespace changes
Inline Side-by-side
Showing
with 285 additions and 83 deletions
README.md
+ 3
− 2
View file @ 891df920
......@@ -16,9 +16,10 @@ Besides that, there is also
- [`IntegrationTests/`](./source/IntegrationTests): contains some integration tests run by the unit tests in the frameit-mmt submodule of the UniFormal/MMT project
## Contributing
## Documentation
See [`Scrolls/README.md`](./source/Scrolls) for how to write scrolls.
- [`./source/Scrolls/README.md`](./source/Scrolls) for a guide on how to write scrolls.
- [`./situation-space.md`](./situation-space.md) for an overview how a situation space and theory looks like over the course of playing.
## Authors
......
errors/mmt-omdoc/IntegrationTests/SituationTheory.mmt.err
+ 0
− 2
View file @ 891df920
<errors>
</errors>
narration/IntegrationTests/SituationTheory.omdoc
+ 1
− 1
View file @ 891df920
<?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:2102.84.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
<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:1753.61.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/space_typechecking_test"/><instruction text="rule scala://parser.api.mmt.kwarc.info?MMTURILexer"/><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/space_typechecking_test?SituationSpace]" target="http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.mmt#271.7.0:291.7.20"/></metadata></mref></omdoc>
\ No newline at end of file
relational/IntegrationTests/SituationTheory.rel
+ 1
− 3
View file @ 891df920
document http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.omdoc
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
Declares http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.omdoc http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace
relational/http..mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test/$Situation$Space.rel 0 → 100644
+ 139
− 0
View file @ 891df920
theory http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace
HasMeta http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace http://mathhub.info/FrameIT/frameworld?FrameworldMeta
Declares http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace?Root
theory http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root
HasMeta http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root http://mathhub.info/FrameIT/frameworld?FrameworldMeta
Includes http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root http://mathhub.info/FrameIT/frameworld?OppositeLen
Includes http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root http://mathhub.info/FrameIT/frameworld?AngleSum
Declares http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?A
constant http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?A
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?A?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?A?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?A?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?A?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
Declares http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?B
constant http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?B
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?B?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?B?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?B?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?B?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
Declares http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?C
constant http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?C
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?C?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?C?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?C?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?C?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
Declares http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC
constant http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?type http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?C?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?type http://mathhub.info/MitM/Foundation?Logic?eq?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?type http://mathhub.info/MitM/core/geometry?Geometry/Common?metric?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?type http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?B?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?type http://mathhub.info/MitM/Foundation?Logic?prop?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?type http://mathhub.info/MitM/Foundation?Logic?ded?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?definition http://cds.omdoc.org/urtheories?Strings?string?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?definition http://mathhub.info/MitM/Foundation?Logic?eq?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?definition http://mathhub.info/MitM/core/geometry?Geometry/Common?metric?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?definition http://cds.omdoc.org/urtheories?Bool?BOOL?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?definition http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?definition http://mathhub.info/MitM/Foundation?Logic?ded?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?definition http://cds.omdoc.org/urtheories?Ded?DED?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?C?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?B?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?definition http://mathhub.info/MitM/Foundation?Logic?prop?type
Declares http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC
constant http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?type http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?A?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?type http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?C?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?type http://mathhub.info/MitM/Foundation?Logic?eq?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?type http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?B?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?type http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?type http://mathhub.info/MitM/Foundation?Logic?prop?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?type http://mathhub.info/MitM/Foundation?Logic?ded?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?definition http://cds.omdoc.org/urtheories?Strings?string?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?definition http://mathhub.info/MitM/Foundation?Logic?eq?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?definition http://cds.omdoc.org/urtheories?Bool?BOOL?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?definition http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?definition http://mathhub.info/MitM/Foundation?Logic?ded?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?A?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?definition http://cds.omdoc.org/urtheories?Ded?DED?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?C?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?B?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?definition http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?definition http://mathhub.info/MitM/Foundation?Logic?prop?type
Declares http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC
constant http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?type http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?A?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?type http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?C?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?type http://mathhub.info/MitM/Foundation?Logic?eq?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?type http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?B?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?type http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?type http://mathhub.info/MitM/Foundation?Logic?prop?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?type http://mathhub.info/MitM/Foundation?Logic?ded?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?definition http://cds.omdoc.org/urtheories?Strings?string?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?definition http://mathhub.info/MitM/Foundation?Logic?eq?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?definition http://cds.omdoc.org/urtheories?Bool?BOOL?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?definition http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?definition http://mathhub.info/MitM/Foundation?Logic?ded?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?A?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?definition http://cds.omdoc.org/urtheories?Ded?DED?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?C?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?B?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?definition http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?definition http://mathhub.info/MitM/Foundation?Logic?prop?type
Declares http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC
constant http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?type http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?A?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?type http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?C?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?type http://mathhub.info/MitM/Foundation?Logic?eq?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?type http://mathhub.info/MitM/Foundation?Logic?ded?definition
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?type http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?B?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?type http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?type http://mathhub.info/MitM/Foundation?Logic?prop?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?type http://mathhub.info/MitM/Foundation?Logic?ded?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?definition http://cds.omdoc.org/urtheories?Strings?string?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?definition http://mathhub.info/MitM/Foundation?Logic?eq?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?definition http://cds.omdoc.org/urtheories?Bool?BOOL?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?definition http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?definition http://mathhub.info/MitM/Foundation?Logic?ded?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?A?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?definition http://cds.omdoc.org/urtheories?Ded?DED?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?C?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?B?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?definition http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?definition http://mathhub.info/MitM/Foundation?Logic?prop?type
Declares http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?first_view
HasDomain http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view ☞frameworld:?OppositeLen/Problem
HasCodomain http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root
view http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view
HasViewFrom http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root ☞frameworld:?OppositeLen/Problem
Declares http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?A
constant http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?A
Declares http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?B
constant http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?B
Declares http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?C
constant http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?C
situation-space.md 0 → 100644
+ 67
− 0
View file @ 891df920
## The Evolution of a Situation Space
This is an overview of how a situation space and theory looks like over the course of playing.
Read from top to bottom; the comments indicate the "current" action that led to the creation of the respective module or declaration.
```mmt
fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta ❚
theory SituationSpace =
// Player starts with situation_theory_1 below that includes this root situation theory,
providing access to scrolls that are available by default ❙
theory Root =
include ☞http://mathhub.info/FrameIT/frameworld?OppositeLen ❙
include ☞http://mathhub.info/FrameIT/frameworld?AngleSum ❙
include ☞http://mathhub.info/FrameIT/frameworld?Midpoint ❙
❚
// Player starts with this situation theory. ❙
theory situation_theory_1 =
include ?DefaultSituationSpace/Root ❙
// The player collects some facts about the world. ❙
fact1: ... ❙
fact2: ... ❙
fact3: ... ❙
// The player formulates a scroll view... (continued below) ❙
view scroll_view_1 : ?OppositeLen/Problem -> ?SituationSpace/situation_theory_1 =
factslot1 = fact1 ❙
factslot2 = fact2 ❙
factslot3 = fact3 ❙
❚
❚
// (continued)... and applies the scroll and thus lands in a new derived situation theory. ❙
theory situation_theory_2 =
include ?SituationSpace/situation_theory_1 ❙
// The player gets access to facts obtained by the scroll (these are precisely the ones pushed out
from ?OppositeLen/Solution over ?SituationSpace?situation_theory_1?scroll_view_1). ❙
out_fact1: ... ❙
out_fact2: ... ❙
out_fact3: ... ❙
// The player goes on collecting more facts. ❙
fact4: ... ❙
fact5: ... ❙
// The player again formulates a scroll, now being able to combine facts they measured themselves
and facts they previously obtained via scroll application. ❙
view scroll_view_2 : ?OppositeLen/Problem -> ?SituationSpace/situation_theory_2 =
factslot1 = out_fact1 ❙
factslot2 = fact4 ❙
factslot3 = out_fact3 ❙
❚
❚
theory SituationSpace/situation_theory_3 =
include ?SituationSpace/situation_theory_2 ❙
out_fact4: ... ❙
// and so on and so forth ❙
❚
❚
```
\ No newline at end of file
source/IntegrationTests/SituationTheory.mmt
+ 32
− 33
View file @ 891df920
namespace http://mathhub.info/FrameIT/frameworld/integrationtests ❚
namespace http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test ❚
import frameworld http://mathhub.info/FrameIT/frameworld ❚
rule scala://parser.api.mmt.kwarc.info?MMTURILexer ❚
import frameworld http://mathhub.info/FrameIT/frameworld ❚
fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta ❚
theory SampleSituationSpace =
theory SituationSpace =
theory Root =
// planar triangle in R^2 ❙
include ☞frameworld:?OppositeLen ❙
......@@ -34,52 +35,50 @@ theory SampleSituationSpace =
meta frameworld:?MetaAnnotations?label "𝔹ℂ"
❙
angleABC
angleB
: Σ β:ℝ. ⊦ ( ∠ A,B,C ) ≐ β ❘
= ⟨45.0, sketch "calculated by ComFreek by hand"⟩ ❘
meta frameworld:?MetaAnnotations?label "∠𝔸𝔹ℂ"
❙
angleBAC
angleA
: Σ β:ℝ. ⊦ ( ∠ B,A,C ) ≐ β ❘
= ⟨45.0, sketch "calculated by ComFreek by hand"⟩ ❘
meta frameworld:?MetaAnnotations?label "∠ℬ𝔸ℂ"
❙
rightAngledC
rightAngleC
: ⊦ ( ∠ 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 ❙
p : point ❘ = ⟨0.0, 0.0, 0.0⟩ ❙
view v : ?MyScroll/Problem -> ?SituationSpace/RootSituationTheory =
a = b ❙
view first_view : frameworld:?OppositeLen/Problem -> ?SituationSpace/Root =
A = A ❙
B = B ❙
C = C ❙
distanceBC = distanceBC ❙
angleB = angleB ❙
rightAngleC = rightAngleC ❙
❚
❚
❚
theory PushedOutSituationTheory =
include ?SituationSpace/RootSituationTheory ❙
c: type ❙
q = p ❙
theory Derived1 =
include ?SituationSpace/Root ❙
deducedLineCA : Σ x:ℝ . ⊦ (d- C A) ≐ x ❘ = ⟨(tan (πl angleB)) ⋅ (πl distanceBC), sketch "OppositeLen Scroll"⟩ ❙
view w : ?MyScroll/Problem -> ?SituationSpace/PushedOutSituationTheory =
a = c ❙
view first_pushout_view : frameworld:?OppositeLen/Solution -> ?SituationSpace/Derived1 =
include ?SituationSpace/Root/first_view ❙
deducedLineCA = deducedLineCA ❙
❚
view second_view : frameworld:?OppositeLen/Problem -> ?SituationSpace/Derived1 =
A = A ❙
B = B ❙
C = C ❙
distanceBC = distanceBC ❙
angleB = angleB ❙
rightAngleC = rightAngleC ❙
❚
❚
❚
❚
\ No newline at end of file
❚
source/Scrolls/README.md
+ 42
− 42
View file @ 891df920
......@@ -9,58 +9,58 @@ Let us write a scroll "Midpoint" that requires two points `P` and `Q` as input,
```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 ❙
// 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. ❙
// 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.
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. ❙
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"
❙
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"
❙
❚
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 ❙
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}." ❙
// 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.
// 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). ❙
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: ❙
// 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}."
❙
❚
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}."
❙
❚
❚
```
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment