From a536fd32368f3f9bdff9188f1eb888cf9a0e6dda Mon Sep 17 00:00:00 2001
From: Lucas <lucas.heublein@t-online.de>
Date: Thu, 24 Aug 2023 16:01:49 +0200
Subject: [PATCH] Changed the WBouncingScroll to take Point facts for the
 position, velocity and g instead of R facts

---
 connect_to_mmt_WBounce.py          | 38 +++++++++++++++++-------------
 source/Scrolls/WBouncingScroll.mmt | 17 +++++++------
 2 files changed, 31 insertions(+), 24 deletions(-)

diff --git a/connect_to_mmt_WBounce.py b/connect_to_mmt_WBounce.py
index 5e7d0c3..1b6e00b 100644
--- a/connect_to_mmt_WBounce.py
+++ b/connect_to_mmt_WBounce.py
@@ -7,10 +7,8 @@ PORT = 8085
 headers = {'Content-type': 'application/json'}
 
 bouncing_scroll = 'http://mathhub.info/FrameIT/frameworld?WBouncingScroll'
-X_ref = {'uri': 'http://mathhub.info/FrameIT/frameworld?WBouncingScroll/Problem?xposition'}
-Y_ref = {'uri': 'http://mathhub.info/FrameIT/frameworld?WBouncingScroll/Problem?yposition'}
-Xv_ref = {'uri': 'http://mathhub.info/FrameIT/frameworld?WBouncingScroll/Problem?xvelocity'}
-Yv_ref = {'uri': 'http://mathhub.info/FrameIT/frameworld?WBouncingScroll/Problem?yvelocity'}
+pos_ref = {'uri': 'http://mathhub.info/FrameIT/frameworld?WBouncingScroll/Problem?position'}
+vel_ref = {'uri': 'http://mathhub.info/FrameIT/frameworld?WBouncingScroll/Problem?velocity'}
 G_ref = {'uri': 'http://mathhub.info/FrameIT/frameworld?WBouncingScroll/Problem?g_base'}
 B_ref = {'uri': 'http://mathhub.info/FrameIT/frameworld?WBouncingScroll/Problem?bounce'}
 W_ref = {'uri': 'http://mathhub.info/FrameIT/frameworld?WBouncingScroll/Problem?walls'}
@@ -106,13 +104,21 @@ def create_R_fact(val, ref):
                    'kind': 'OMS'},
             "df": {"kind": "OMF", "float": val}
             }
+            
+def create_point_fact(val, ref):
+    return {"ref": ref,
+            "label": "P",
+            "kind": "general",
+            "tp": {"kind": "OMS", "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point"},
+            "df": {"kind": "OMA", "applicant": {"kind": "OMS", "uri": "http://gl.mathhub.info/MMT/LFX/Sigma?Symbols?Tuple"},
+                   "arguments": [{"kind": "OMF", "float": val[0]},
+                                 {"kind": "OMF", "float": val[1]},
+                                 {"kind": "OMF", "float": val[2]}]}}
 
 g = -200.0
-X_fact = create_R_fact(380.0, X_ref)
-Y_fact = create_R_fact(300.0, Y_ref)
-Xv_fact = create_R_fact(-490.0, Xv_ref)
-Yv_fact = create_R_fact(150.0, Yv_ref)
-G_fact = create_R_fact(g, G_ref)
+pos_fact = create_point_fact([0.0, 300.0, 380.0], pos_ref)
+vel_fact = create_point_fact([0.0, 150.0, -490.0], vel_ref)
+G_fact = create_point_fact([0.0, g, 0.0], G_ref)
 B_fact = create_R_fact(0.8, B_ref)
 #walls_fact = create_walls_fact([[-10000.0, 0.0, 10000.0, 0.0]])
 walls_list = [[-1.0, 0.0, 401.0, 0.0],
@@ -126,16 +132,14 @@ walls_list = [[-1.0, 0.0, 401.0, 0.0],
               [300.0, 100.0, 385.0, 150.0],
               [50.0, 50.0, 100.0, 135.0]]
 walls_fact = create_walls_fact(walls_list)
-fact_list = [X_fact, Y_fact, Xv_fact, Yv_fact, G_fact, B_fact, walls_fact]
+fact_list = [pos_fact, vel_fact, G_fact, B_fact, walls_fact]
 fact_list_encoded = json.dumps(fact_list).encode('utf-8')
 
-scroll_assignment_list = [{"fact": X_ref, "assignment": {"kind": "OMS", "uri": 'http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace/SituationTheory1?fact1'}},
-                          {"fact": Y_ref, "assignment": {"kind": "OMS", "uri": 'http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace/SituationTheory1?fact2'}},
-                          {"fact": Xv_ref, "assignment": {"kind": "OMS", "uri": 'http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace/SituationTheory1?fact3'}}, 
-                          {"fact": Yv_ref, "assignment": {"kind": "OMS", "uri": 'http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace/SituationTheory1?fact4'}}, 
-                          {"fact": G_ref, "assignment": {"kind": "OMS", "uri": 'http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace/SituationTheory1?fact5'}},
-                          {"fact": B_ref, "assignment": {"kind": "OMS", "uri": 'http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace/SituationTheory1?fact6'}},
-                          {"fact": W_ref, "assignment": {"kind": "OMS", "uri": 'http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace/SituationTheory1?fact7'}}]
+scroll_assignment_list = [{"fact": pos_ref, "assignment": {"kind": "OMS", "uri": 'http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace/SituationTheory1?fact1'}},
+                          {"fact": vel_ref, "assignment": {"kind": "OMS", "uri": 'http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace/SituationTheory1?fact2'}}, 
+                          {"fact": G_ref, "assignment": {"kind": "OMS", "uri": 'http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace/SituationTheory1?fact3'}},
+                          {"fact": B_ref, "assignment": {"kind": "OMS", "uri": 'http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace/SituationTheory1?fact4'}},
+                          {"fact": W_ref, "assignment": {"kind": "OMS", "uri": 'http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace/SituationTheory1?fact5'}}]
 scroll_application = {"scroll": bouncing_scroll,
                       "assignments": scroll_assignment_list}
 scroll_encoded = json.dumps(scroll_application).encode('utf-8')
diff --git a/source/Scrolls/WBouncingScroll.mmt b/source/Scrolls/WBouncingScroll.mmt
index 6c645cd..7da8ea0 100644
--- a/source/Scrolls/WBouncingScroll.mmt
+++ b/source/Scrolls/WBouncingScroll.mmt
@@ -57,11 +57,14 @@ theory WBouncingScroll =
     // start position and velocity ❙
     theory Problem =
 	    include ?WBouncingScroll/funcs ❙
-        xposition: ℝ ❘ meta ?MetaAnnotations?label "X" ❙
-        yposition: ℝ ❘ meta ?MetaAnnotations?label "Y" ❙
-        xvelocity: ℝ ❘ meta ?MetaAnnotations?label "XV" ❙
-	    yvelocity: ℝ ❘ meta ?MetaAnnotations?label "YV" ❙
-	    g_base: ℝ ❘ meta ?MetaAnnotations?label "G" ❙
+        position: point ❘ meta ?MetaAnnotations?label "Pos" ❙
+        velocity: point ❘ meta ?MetaAnnotations?label "Vel" ❙
+        g_base: point ❘ meta ?MetaAnnotations?label "G" ❙
+        //xposition: ℝ ❘ meta ?MetaAnnotations?label "X" ❙
+        //yposition: ℝ ❘ meta ?MetaAnnotations?label "Y" ❙
+        //xvelocity: ℝ ❘ meta ?MetaAnnotations?label "XV" ❙
+	    //yvelocity: ℝ ❘ meta ?MetaAnnotations?label "YV" ❙
+	    //g_base: ℝ ❘ meta ?MetaAnnotations?label "G" ❙
 		bounce: ℝ ❘ meta ?MetaAnnotations?label "BO" ❙
         walls: List[(ℝ × ℝ) × (ℝ × ℝ)] ❘ meta ?MetaAnnotations?label "Walls" ❙
     ❚
@@ -74,9 +77,9 @@ theory WBouncingScroll =
 		//basev : ((ℝ × ℝ) × (ℝ × ℝ) × (ℝ × ℝ)) ❘ = prep (walls map get_mc) xposition yposition xvelocity yvelocity g_base ❙
 		//nextv : ((ℝ × ℝ) × (ℝ × ℝ) × (ℝ × ℝ)) ❘ = get_next_vals (walls map get_mc ) ⟨g_base, bounce⟩ basev ❙
 		//nextv2 : ((ℝ × ℝ) × (ℝ × ℝ) × (ℝ × ℝ)) ❘ = get_next_vals (walls map get_mc ) ⟨g_base, bounce⟩ nextv ❙
-		full_list: List[(ℝ × ℝ) × (ℝ × ℝ) × (ℝ × ℝ)] ❘ = stepUntilX ((ℝ × ℝ) × (ℝ × ℝ) × (ℝ × ℝ)) List[(ℝ × ℝ) × (ℝ × ℝ)] (ℝ × ℝ) (walls map get_mc) ⟨g_base, bounce⟩ (prep (walls map get_mc) xposition yposition xvelocity yvelocity g_base) get_next_vals end_cond ❙
+		full_list: List[(ℝ × ℝ) × (ℝ × ℝ) × (ℝ × ℝ)] ❘ = stepUntilX ((ℝ × ℝ) × (ℝ × ℝ) × (ℝ × ℝ)) List[(ℝ × ℝ) × (ℝ × ℝ)] (ℝ × ℝ) (walls map get_mc) ⟨(g_base _y), bounce⟩ (prep (walls map get_mc) (position _z) (position _y) (velocity _z) (velocity _y) (g_base _y)) get_next_vals end_cond ❙
 		ht_list: List[ℝ] ❘ = full_list map ([xele] red_ht xele) ❙
-		fun_list : List[ℝ ⟶ (ℝ × ℝ)] ❘ = full_list map ([vals] get_pos_fun (πl (πl vals)) (πr (πl vals)) (πl (πl (πr vals))) (πr (πl (πr vals))) g_base) ❙
+		fun_list : List[ℝ ⟶ (ℝ × ℝ)] ❘ = full_list map ([vals] get_pos_fun (πl (πl vals)) (πr (πl vals)) (πl (πl (πr vals))) (πr (πl (πr vals))) (g_base _y)) ❙
         meta ?MetaAnnotations?label "WBouncingScroll" ❙
         meta ?MetaAnnotations?description s"Bouncing " ❙
     ❚
-- 
GitLab