diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Frameworld$Meta.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Frameworld$Meta.omdoc.xz index f58dd1ac5451c19fd0e55f5fdb1830515be3f6b9..96aad98e857b18138e7a2af7caba74d23cf24813 100644 Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Frameworld$Meta.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Frameworld$Meta.omdoc.xz differ diff --git a/narration/MetaTheories.omdoc b/narration/MetaTheories.omdoc index 34be72d83c4920796d703191a93355e36eccee11..ff67f80de510a6fbfa551bc01cc1b8f9f1c8ca83 100644 --- a/narration/MetaTheories.omdoc +++ b/narration/MetaTheories.omdoc @@ -1,2 +1,2 @@ <?xml version="1.0" encoding="UTF-8"?> -<omdoc base="http://mathhub.info/FrameIT/frameworld/MetaTheories.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#0.0.0:20521.388.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://cds.omdoc.org/urtheories?LF"/><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#125.5.0:253.5.128"/></metadata>MMT meta keys and value constructors for meta annotations of facts in situation theories and (input/output) facts in scrolls</opaque><mref name="[http://mathhub.info/FrameIT/frameworld?MetaAnnotations]" target="http://mathhub.info/FrameIT/frameworld?MetaAnnotations"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#255.6.0:276.6.21"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?2DPoints]" target="http://mathhub.info/FrameIT/frameworld?2DPoints"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#685.24.1:699.24.15"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?FrameITBasics]" target="http://mathhub.info/FrameIT/frameworld?FrameITBasics"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#1094.48.0:1113.48.19"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?FrameITRectangles]" target="http://mathhub.info/FrameIT/frameworld?FrameITRectangles"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#4340.108.0:4363.108.23"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?FrameITTriangles]" target="http://mathhub.info/FrameIT/frameworld?FrameITTriangles"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#7437.158.0:7459.158.22"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?FrameITCircle]" target="http://mathhub.info/FrameIT/frameworld?FrameITCircle"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#10771.202.0:10790.202.19"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?FrameITCone]" target="http://mathhub.info/FrameIT/frameworld?FrameITCone"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#12754.240.0:12771.240.17"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?FrameITCylinder]" target="http://mathhub.info/FrameIT/frameworld?FrameITCylinder"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#16111.295.0:16132.295.21"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?FrameITTheories]" target="http://mathhub.info/FrameIT/frameworld?FrameITTheories"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#17019.318.0:17040.318.21"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#19961.370.0:20056.370.95"/></metadata>The meta theory to use for situation theories, scroll problem, and scroll solution theories</opaque><mref name="[http://mathhub.info/FrameIT/frameworld?FrameworldMeta]" target="http://mathhub.info/FrameIT/frameworld?FrameworldMeta"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#20058.371.0:20078.371.20"/></metadata></mref></omdoc> \ No newline at end of file +<omdoc base="http://mathhub.info/FrameIT/frameworld/MetaTheories.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#0.0.0:20627.388.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://cds.omdoc.org/urtheories?LF"/><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#125.5.0:253.5.128"/></metadata>MMT meta keys and value constructors for meta annotations of facts in situation theories and (input/output) facts in scrolls</opaque><mref name="[http://mathhub.info/FrameIT/frameworld?MetaAnnotations]" target="http://mathhub.info/FrameIT/frameworld?MetaAnnotations"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#255.6.0:276.6.21"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?2DPoints]" target="http://mathhub.info/FrameIT/frameworld?2DPoints"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#685.24.1:699.24.15"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?FrameITBasics]" target="http://mathhub.info/FrameIT/frameworld?FrameITBasics"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#1094.48.0:1113.48.19"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?FrameITRectangles]" target="http://mathhub.info/FrameIT/frameworld?FrameITRectangles"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#4442.108.0:4465.108.23"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?FrameITTriangles]" target="http://mathhub.info/FrameIT/frameworld?FrameITTriangles"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#7539.158.0:7561.158.22"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?FrameITCircle]" target="http://mathhub.info/FrameIT/frameworld?FrameITCircle"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#10873.202.0:10892.202.19"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?FrameITCone]" target="http://mathhub.info/FrameIT/frameworld?FrameITCone"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#12860.240.0:12877.240.17"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?FrameITCylinder]" target="http://mathhub.info/FrameIT/frameworld?FrameITCylinder"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#16217.295.0:16238.295.21"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?FrameITTheories]" target="http://mathhub.info/FrameIT/frameworld?FrameITTheories"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#17125.318.0:17146.318.21"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#20067.370.0:20162.370.95"/></metadata>The meta theory to use for situation theories, scroll problem, and scroll solution theories</opaque><mref name="[http://mathhub.info/FrameIT/frameworld?FrameworldMeta]" target="http://mathhub.info/FrameIT/frameworld?FrameworldMeta"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#20164.371.0:20184.371.20"/></metadata></mref></omdoc> \ No newline at end of file diff --git a/source/MetaTheories.mmt b/source/MetaTheories.mmt index 39ae590e5d6432951e2e52ef98b4fa5c8a2e0501..4d2c522119aae85c7998f5b8c7ced67dcfa1ac25 100644 --- a/source/MetaTheories.mmt +++ b/source/MetaTheories.mmt @@ -88,10 +88,10 @@ theory FrameITBasics = // projection and distance function for planes â™ helperFunctionForProjection : plane ⟶ point ⟶ ℠☠= [e, p] ( < ( Pnormal e ) , ( planeBase e ) > - < ( Pnormal e ) , p > ) / ( < ( Pnormal e ) , ( Pnormal e ) > ) ☠# helperT 1 2 prec 1 â™ orthogonalProjectionPointToPlane : plane ⟶ point ⟶ point ☠= [e,p] p p+p ( ( helperT e p ) rdotp( Pnormal e ) ) ☠# orthogProjPointToPlane 1 2 prec 1 â™ - distancePlanePoint : plane ⟶ point ⟶ ℠☠= [e,p] ( doAbs ( < Pnormal e , p > - < Pnormal e , Pbase e > ) ) / ( | Pnormal e | ) ☠# distPlP 1 2 prec 1 â™ + distancePlanePoint : plane ⟶ point ⟶ ℠☠= [e,p] ( doAbs ( < Pnormal e , p > - < Pnormal e , Pbase e > ) ) / ( | Pnormal e | + epsi ) ☠# distPlP 1 2 prec 1 â™ // functions to calculate the angle between a plane and a line â™ - anglePlaneLineCalc : point ⟶ point ⟶ ℠☠= [v,w] asin ( < v,w > / (|v| â‹… |w|)) ☠# plcalc 1 2 prec 1 â™ + anglePlaneLineCalc : point ⟶ point ⟶ ℠☠= [v,w] asin ( < v,w > / ( (|v| â‹… |w|) + epsi )) ☠# plcalc 1 2 prec 1 â™ anglePlaneLine : plane ⟶ line ⟶ ℠☠= [e,l] plcalc ( Pnormal e ) ( directionL l ) ☠# ∠pl 1 2 prec 1 â™ radToDegree : ℠⟶ ℠☠= [r] ( r / pi_num ) â‹… 180.0 ☠# radToDegree 1 prec 1 â™ @@ -100,7 +100,7 @@ theory FrameITBasics = lineOnProofFrom: {l } ⊦ ( from l ) on l ☠# fromOnProofLine 1 â™ lineOnProofTo: {l } ⊦ ( to l ) on l ☠# toOnProofLine 1 â™ - + normalizeSafe: point ⟶ point ☠= [v] (1.0 / ( | v | + epsi )) â‹…â‹… v ☠# normS 1 â™ âš @@ -228,7 +228,7 @@ theory FrameITCircle = angleCircleLine : circle ⟶ line ⟶ ℠☠= [c,l] radToDegree ( plcalc ( Pnormal ( planeCircle c ) ) ( directionL l ) ) ☠# ∠cl 1 2 prec 1 â™ orthogonalCircleLine : circle ⟶ line ⟶ bool ☠# orthogCL 1 2 â™ - pointsToPlaneNormal : point ⟶ point ⟶ point ⟶ plane ☠= [p1,p2,p3] Ppn p1 ( normalize ( (p2 p-p p1 ) Vcross ( p3 p-p p1) ) ) ☠# pToPlane 1 2 3 â™ + pointsToPlaneNormal : point ⟶ point ⟶ point ⟶ plane ☠= [p1,p2,p3] Ppn p1 ( normalizeSafe ( (p2 p-p p1 ) Vcross ( p3 p-p p1) ) ) ☠# pToPlane 1 2 3 â™ wrap3EdgePointsToPlaneParametric : point ⟶ point ⟶ point ⟶ plane ☠= [p1,p2,p3 ] Ppara p1 (p2 p-p p1 ) ( p3 p-p p1) ☠# pointsToPlanePara 1 2 3 â™ parallelCircles: circle ⟶ circle ⟶ bool ☠# paraCirc 1 2 â™