From 35649e850ead603f2269c125cb3036f099f1e8ed Mon Sep 17 00:00:00 2001
From: Lucas <lucas.heublein@t-online.de>
Date: Thu, 7 Sep 2023 20:29:38 +0200
Subject: [PATCH] Added a mmt file for 3D bouncing. (And a python File to call
the Scroll). And changed the 2d bouncing scroll to only use stepUntil instead
of stepUntilX
---
connect_to_mmt_W3Bounce.py | 273 ++++++++++++++++++
.../kwarc/mmt/frameit/rules/StepUntil.scala | 2 +-
source/DefaultSituationSpace.mmt | 1 +
source/IntegrationTests/DynamicsDebug.mmt | 19 +-
source/Scrolls/W3DBouncingScroll.mmt | 98 +++++++
source/Scrolls/WBouncingScroll.mmt | 6 +-
source/dynamics.mmt | 42 +++
7 files changed, 437 insertions(+), 4 deletions(-)
create mode 100644 connect_to_mmt_W3Bounce.py
create mode 100644 source/Scrolls/W3DBouncingScroll.mmt
diff --git a/connect_to_mmt_W3Bounce.py b/connect_to_mmt_W3Bounce.py
new file mode 100644
index 0000000..a74414c
--- /dev/null
+++ b/connect_to_mmt_W3Bounce.py
@@ -0,0 +1,273 @@
+import http.client
+import json
+import time
+
+HOST = 'localhost' #'127.0.0.1'
+PORT = 8085
+headers = {'Content-type': 'application/json'}
+
+bouncing_scroll = 'http://mathhub.info/FrameIT/frameworld?W3DBouncingScroll'
+pos_ref = {'uri': 'http://mathhub.info/FrameIT/frameworld?W3DBouncingScroll/Problem?position'}
+vel_ref = {'uri': 'http://mathhub.info/FrameIT/frameworld?W3DBouncingScroll/Problem?velocity'}
+G_ref = {'uri': 'http://mathhub.info/FrameIT/frameworld?W3DBouncingScroll/Problem?g_base'}
+B_ref = {'uri': 'http://mathhub.info/FrameIT/frameworld?W3DBouncingScroll/Problem?bounce'}
+W_ref = {'uri': 'http://mathhub.info/FrameIT/frameworld?W3DBouncingScroll/Problem?wallsr'}
+
+real_list = 'http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace/SituationTheory2?real_list'
+list_type = 'http://gl.mathhub.info/MMT/LFX/Datatypes?ListSymbols?ListType'
+product = 'http://gl.mathhub.info/MMT/LFX/Sigma?Symbols?Product'
+real_lit = 'http://mathhub.info/MitM/Foundation?RealLiterals?real_lit'
+cons = 'http://gl.mathhub.info/MMT/LFX/Datatypes?ListSymbols?cons'
+cons_nil = 'http://gl.mathhub.info/MMT/LFX/Datatypes?ListSymbols?nil_constant'
+tuple_mmt = 'http://gl.mathhub.info/MMT/LFX/Sigma?Symbols?Tuple'
+point_mmt = 'http://mathhub.info/MitM/core/geometry?3DGeometry?point'
+
+
+def list_element_4point(p1, p2, p3, p4):
+ return {'applicant': {'uri': tuple_mmt, 'kind': 'OMS'},
+ 'arguments': [{'applicant': {'uri': tuple_mmt, 'kind': 'OMS'},
+ 'arguments': [{'float': p1[0], 'kind': 'OMF'},
+ {'float': p1[1], 'kind': 'OMF'},
+ {'float': p1[2], 'kind': 'OMF'}],
+ 'kind': 'OMA'},
+ {'applicant': {'uri': tuple_mmt, 'kind': 'OMS'},
+ 'arguments': [{'float': p2[0], 'kind': 'OMF'},
+ {'float': p2[1], 'kind': 'OMF'},
+ {'float': p2[2], 'kind': 'OMF'}],
+ 'kind': 'OMA'},
+ {'applicant': {'uri': tuple_mmt, 'kind': 'OMS'},
+ 'arguments': [{'float': p3[0], 'kind': 'OMF'},
+ {'float': p3[1], 'kind': 'OMF'},
+ {'float': p3[2], 'kind': 'OMF'}],
+ 'kind': 'OMA'},
+ {'applicant': {'uri': tuple_mmt, 'kind': 'OMS'},
+ 'arguments': [{'float': p4[0], 'kind': 'OMF'},
+ {'float': p4[1], 'kind': 'OMF'},
+ {'float': p4[2], 'kind': 'OMF'}],
+ 'kind': 'OMA'}],
+ 'kind': 'OMA'}
+
+def list_element_4point_plus_nil(p1, p2, p3, p4):
+ return {'applicant': {'uri': cons, 'kind': 'OMS'},
+ 'arguments': [{'applicant': {'uri': cons_nil, 'kind': 'OMS'},
+ 'arguments': [{'applicant': {'uri': product, 'kind': 'OMS'},
+ 'arguments': [{'applicant': {'uri': product, 'kind': 'OMS'},
+ 'arguments': [{'uri': real_lit, 'kind': 'OMS'},
+ {'uri': real_lit, 'kind': 'OMS'},
+ {'uri': real_lit, 'kind': 'OMS'}],
+ 'kind': 'OMA'},
+ {'applicant': {'uri': product, 'kind': 'OMS'},
+ 'arguments': [{'uri': real_lit, 'kind': 'OMS'},
+ {'uri': real_lit, 'kind': 'OMS'},
+ {'uri': real_lit, 'kind': 'OMS'}],
+ 'kind': 'OMA'},
+ {'applicant': {'uri': product, 'kind': 'OMS'},
+ 'arguments': [{'uri': real_lit, 'kind': 'OMS'},
+ {'uri': real_lit, 'kind': 'OMS'},
+ {'uri': real_lit, 'kind': 'OMS'}],
+ 'kind': 'OMA'},
+ {'applicant': {'uri': product, 'kind': 'OMS'},
+ 'arguments': [{'uri': real_lit, 'kind': 'OMS'},
+ {'uri': real_lit, 'kind': 'OMS'},
+ {'uri': real_lit, 'kind': 'OMS'}],
+ 'kind': 'OMA'}],
+ 'kind': 'OMA'}],
+ 'kind': 'OMA'},
+ {'applicant': {'uri': tuple_mmt, 'kind': 'OMS'},
+ 'arguments': [{'applicant': {'uri': tuple_mmt, 'kind': 'OMS'},
+ 'arguments': [{'float': p1[0], 'kind': 'OMF'},
+ {'float': p1[1], 'kind': 'OMF'},
+ {'float': p1[2], 'kind': 'OMF'}],
+ 'kind': 'OMA'},
+ {'applicant': {'uri': tuple_mmt, 'kind': 'OMS'},
+ 'arguments': [{'float': p2[0], 'kind': 'OMF'},
+ {'float': p2[1], 'kind': 'OMF'},
+ {'float': p2[2], 'kind': 'OMF'}],
+ 'kind': 'OMA'},
+ {'applicant': {'uri': tuple_mmt, 'kind': 'OMS'},
+ 'arguments': [{'float': p3[0], 'kind': 'OMF'},
+ {'float': p3[1], 'kind': 'OMF'},
+ {'float': p3[2], 'kind': 'OMF'}],
+ 'kind': 'OMA'},
+ {'applicant': {'uri': tuple_mmt, 'kind': 'OMS'},
+ 'arguments': [{'float': p4[0], 'kind': 'OMF'},
+ {'float': p4[1], 'kind': 'OMF'},
+ {'float': p4[2], 'kind': 'OMF'}],
+ 'kind': 'OMA'}],
+ 'kind': 'OMA'}],
+ 'kind': 'OMA'}
+
+def cons_2elements(e1, e2):
+ return {'applicant': {'uri': cons, 'kind': 'OMS'},
+ 'arguments': [e1, e2],
+ 'kind': 'OMA'}
+
+def construct_list_4point_df(values):
+ # Values needs to be of the form [[[x1, y1, z1], [x2, y2, z2], [x3, y3, z3], [x4, y4, z4]], ...]
+ prev_ele = {}
+ for ci, cv in enumerate(values[::-1]):
+ if ci == 0:
+ prev_ele = list_element_4point_plus_nil(cv[0], cv[1], cv[2], cv[3])
+ else:
+ cur_ele = list_element_4point(cv[0], cv[1], cv[2], cv[3])
+ prev_ele = cons_2elements(prev_ele, cur_ele)
+ return prev_ele
+
+def create_walls_fact(values):
+ # Values needs to be of the form [[x1, y1, x2, y2], [x1, y1, x2, y2], ...]
+ return {'ref': W_ref,
+ 'label': 'Wallsr',
+ 'tp': {'applicant': {'uri': list_type, 'kind': 'OMS'},
+ 'arguments': [{'applicant': {'uri': product, 'kind': 'OMS'},
+ 'arguments': [{'uri': point_mmt, 'kind': 'OMS'},
+ {'uri': point_mmt, 'kind': 'OMS'},
+ {'uri': point_mmt, 'kind': 'OMS'},
+ {'uri': point_mmt, 'kind': 'OMS'}],
+ 'kind': 'OMA'}],
+ 'kind': 'OMA'},
+ 'kind': 'general',
+ 'df': construct_list_4point_df(values)
+ }
+
+def create_R_fact(val, ref):
+ return {"ref": ref,
+ "label": "X",
+ "kind": "general",
+ "tp": {'uri': real_lit,
+ 'kind': 'OMS'},
+ "df": {"kind": "OMF", "float": val}
+ }
+
+def create_point_fact(val, ref):
+ return {"ref": ref,
+ "label": "P",
+ "kind": "general",
+ "tp": {"kind": "OMS", "uri": point_mmt},
+ "df": {"kind": "OMA", "applicant": {"kind": "OMS", "uri": tuple_mmt},
+ "arguments": [{"kind": "OMF", "float": val[0]},
+ {"kind": "OMF", "float": val[1]},
+ {"kind": "OMF", "float": val[2]}]}}
+
+g = -200.0
+pos_fact = create_point_fact([380.0, 0.0, 300.0], pos_ref)
+vel_fact = create_point_fact([-490.0, 100.0, 150.0], vel_ref)
+G_fact = create_point_fact([0.0, g, 0.0], G_ref)
+B_fact = create_R_fact(0.8, B_ref)
+#wallsr_list = [[[-400.0, -400.0, 0.0], [400.0, -400.0, 0.0], [400.0, 400.0, 0.0], [-400.0, 400.0, 0.0]]]
+wallsr_list = [[[0.0, 0.0, 0.0], [400.0, 0.0, 0.0], [400.0, 0.0, 400.0], [0.0, 0.0, 400.0]],
+ [[0.0, 400.0, 0.0], [400.0, 400.0, 0.0], [400.0, 400.0, 400.0], [0.0, 400.0, 400.0]],
+ [[0.0, 0.0, 0.0], [0.0, 0.0, 400.0], [0.0, 400.0, 400.0], [0.0, 400.0, 0.0]],
+ [[400.0, 0.0, 0.0], [400.0, 0.0, 400.0], [400.0, 400.0, 400.0], [400.0, 400.0, 0.0]],
+ [[0.0, 0.0, 400.0], [400.0, 0.0, 400.0], [400.0, 400.0, 400.0], [0.0, 400.0, 400.0]],
+ [[0.0, 0.0, 0.0], [400.0, 0.0, 0.0], [400.0, 400.0, 0.0], [0.0, 400.0, 0.0]],
+ [[50.0, 0.0, 200.0], [120.7, 0.0, 270.7], [120.7, 200.0, 270.7], [50.0, 200.0, 200.0]],
+ [[150.0, 0.0, 100.0], [200.0, 0.0, 100.0], [200.0, 200.0, 100.0], [150.0, 200.0, 100.0]],
+ [[150.0, 0.0, 286.6], [200.0, 0.0, 200.0], [200.0, 200.0, 200.0], [150.0, 200.0, 286.6]],
+ [[230.7, 0.0, 340.0], [300.0, 0.0, 300.0], [300.0, 200.0, 300.0], [230.7, 200.0, 340.0]],
+ [[300.0, 0.0, 100.0], [386.6, 0.0, 150.0], [386.6, 200.0, 150.0], [300.0, 200.0, 100.0]],
+ [[50.0, 0.0, 50.0], [100.0, 0.0, 136.6], [100.0, 200.0, 136.6], [50.0, 200.0, 50.0]]]
+wallsr_fact = create_walls_fact(wallsr_list)
+fact_list = [pos_fact, vel_fact, G_fact, B_fact, wallsr_fact]
+fact_list_encoded = json.dumps(fact_list).encode('utf-8')
+
+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')
+
+t1 = time.time()
+conn = http.client.HTTPConnection(HOST, port=PORT)
+conn.request("POST", "/fact/bulkadd", headers=headers, body=fact_list_encoded)
+response = conn.getresponse()
+data = response.read()
+print(response.status, response.reason)
+print(time.time() - t1)
+
+data_dict = json.loads(data.decode('utf-8'))
+
+t2 = time.time()
+conn = http.client.HTTPConnection(HOST, port=PORT)
+conn.request("POST", "/scroll/apply", headers=headers, body=scroll_encoded)
+response = conn.getresponse()
+data = response.read()
+print(response.status, response.reason)
+print(time.time() - t2)
+
+
+data_dict = json.loads(data.decode('utf-8'))
+for i in range(len(data_dict["acquiredFacts"])):
+ print(data_dict["acquiredFacts"][i])
+
+rel_fact = data_dict['acquiredFacts'][0]["df"]["arguments"]
+values = []
+for rf in rel_fact:
+ rfa = rf["arguments"]
+ cvals = []
+ for ri2, rrf in enumerate(rfa):
+ if ri2 == len(rfa) - 1:
+ cvals.extend([x["float"] for x in rrf["arguments"][0]["arguments"]])
+ cvals.append(rrf["arguments"][1]["float"])
+ else:
+ cvals.extend([x["float"] for x in rrf["arguments"]])
+ values.append(cvals)
+print("Step\tX\tY\tZ\tXv\tYv\tZv\tht\tnx\tny\tnz")
+for i, v in enumerate(values):
+ print("%d\t%.2f\t%.2f\t%.2f\t%.2f\t%.2f\t%.2f\t%.2f\t%.2f\t%.2f\t%.2f" % (i, v[0], v[1], v[2], v[3], v[4], v[5], v[9], v[6], v[7], v[8]))
+
+
+import matplotlib.pyplot as plt
+import numpy as np
+
+def get_xyz_wrap(xs, ys, zs, xv, yv, zv):
+ def get_xyz(ct):
+ rx = xs + ct * xv
+ ry = ys + ct * yv
+ rz = zs + ct * zv + 0.5 * g * ct**2
+ return np.array([rx, ry, rz])
+ return get_xyz
+
+# plot ---------------------------------------------------- #
+def floatRgb(mag, cmin, cmax):
+ """ Return a tuple of floats between 0 and 1 for R, G, and B. """
+ # Normalize to 0-1
+ x = float(mag - cmin) / (cmax - cmin)
+ blue = np.minimum(np.maximum(4*(0.75-x), 0.), 1.)
+ red = np.minimum(np.maximum(4*(x-0.25), 0.), 1.)
+ green = np.minimum(np.maximum(4*np.abs(x-0.5)-1., 0.), 1.)
+ return red, green, blue
+
+def rgb(mag, cmin, cmax):
+ """ Return a tuple of integers, as used in AWT/Java plots. """
+ red, green, blue = floatRgb(mag, cmin, cmax)
+ return int(red*255), int(green*255), int(blue*255)
+
+def strRgb(mag, cmin, cmax):
+ """ Return a hex string, as used in Tk plots. """
+ return "#%02x%02x%02x" % rgb(mag, cmin, cmax)
+
+plt.figure()
+ax = plt.axes(projection ="3d")
+
+pos3ds = []
+colors = []
+for w in wallsr_list:
+ spos = np.array(w[0])
+ in1 = np.array(w[1]) -np.array( w[0])
+ in2 = np.array(w[3]) - np.array(w[0])
+ for i1 in np.arange(0, 1.01, 0.1):
+ for i2 in np.arange(0, 1.01, 0.1):
+ cur_pos = spos + i1 * in1 + i2 * in2
+ pos3ds.append([cur_pos[0], cur_pos[1], cur_pos[2]])
+ colors.append(strRgb(cur_pos[1], 0, 400))
+for mii, mi in enumerate(values):
+ xyz_func = get_xyz_wrap(mi[0], mi[1], mi[2], mi[3], mi[4], mi[5])
+ pos3ds.extend([xyz_func(ct) for ct in np.arange(0, mi[9], 0.01)])
+ colors.extend([strRgb(xyz_func(ct)[1], 0, 400) for ct in np.arange(0, mi[9], 0.01)])
+pos3ds = np.array(pos3ds)
+ax.scatter3D(pos3ds[:, 0], pos3ds[:, 1], pos3ds[:, 2], color=colors)
+plt.show()
+# plot ---------------------------------------------------- #
diff --git a/scala/info/kwarc/mmt/frameit/rules/StepUntil.scala b/scala/info/kwarc/mmt/frameit/rules/StepUntil.scala
index 826333d..d2463b3 100644
--- a/scala/info/kwarc/mmt/frameit/rules/StepUntil.scala
+++ b/scala/info/kwarc/mmt/frameit/rules/StepUntil.scala
@@ -44,7 +44,7 @@ object StepUntilRule extends ParametricRule {
case StepUntil(_, iv, f, tC) =>
val values = mutable.ListBuffer[Term]()
var iter = 0
- var cur = iv
+ var cur = check.simplify(iv)
while (iter < DEBUG_MAX_ITER_COUNT) {
iter += 1
check.tryToCheckWithoutDelay(Equality(stack, Apply(tC, cur), truetm, None)) match {
diff --git a/source/DefaultSituationSpace.mmt b/source/DefaultSituationSpace.mmt
index 2c66635..5dc2f2a 100644
--- a/source/DefaultSituationSpace.mmt
+++ b/source/DefaultSituationSpace.mmt
@@ -17,6 +17,7 @@ theory DefaultSituationSpace =
include ?CircleScroll â™
include ?BouncingScroll â™
include ?WBouncingScroll â™
+ include ?W3DBouncingScroll â™
// include ?SinOppositeLeg â™
include ?CircleLineAngleScroll â™
include ?CircleAreaScroll â™
diff --git a/source/IntegrationTests/DynamicsDebug.mmt b/source/IntegrationTests/DynamicsDebug.mmt
index b75c102..c8ffd6f 100644
--- a/source/IntegrationTests/DynamicsDebug.mmt
+++ b/source/IntegrationTests/DynamicsDebug.mmt
@@ -8,7 +8,7 @@ fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta âš
theory IfElseDebug =
include ☞http://mathhub.info/FrameIT/frameworld?IfThenElseX â™
- c: ℠☠= â„ ifx (leq_real_lit 20.0 10.0) thenx 1.0 elsex 0.0 â™
+ c: ℠☠= â„ ifx (leq_real_lit 20.0 30.0) thenx 1.0 elsex 0.0 â™
âš
theory StepUntilDebug =
@@ -24,7 +24,22 @@ theory StepUntilXDebug =
my_list: List[â„] ☠= stepUntilX â„ List[â„] (℠× â„) (cons 1.0 nil) ⟨2.0, 1.0⟩ 0.0 ([x: List[â„], y: ℠× â„, z: â„] times_real_lit (plus_real_lit (x fold 0.0 ([curr: â„][acc: â„] plus_real_lit curr acc)) z) (Ï€l y)) ([x: â„] leq_real_lit 50.0 x) â™
//my_list: ℠☠= stepUntil â„ 0.0 ([x: â„] plus_real_lit x 1.0) ([x: â„] leq_real_lit 10.0 x) â™
âš
-theory StepUntilX2Debug =
+
+theory W3Debug =
+ map_func : ℠⟶ (℠× â„) ☠=
+ [ca] ⟨ca, ca⟩ â™
+ add_map_func : ℠⟶ ℠☠=
+ [wi] plus_real_lit 1.0 wi â™
+ add_fold_func : (℠× â„) ⟶ (℠× â„) ⟶ (℠× â„) ☠=
+ [cur][acc] ⟨plus_real_lit (Ï€l acc) (Ï€l cur), plus_real_lit (Ï€r acc) (Ï€r cur)⟩ â™
+ add_one : List[â„] ⟶ List[â„] ☠=
+ [w] w map add_map_func â™
+ duplicate : List[â„] ⟶ (℠× â„) ☠=
+ [a] (a map map_func) fold ⟨1.0, 1.0⟩ add_fold_func â™
+ test_fold4 : List[â„] ⟶ (℠× â„) ☠=
+ [rl] duplicate (add_one rl) â™
+âš
+//theory StepUntilX2Debug =
include ☞http://mathhub.info/FrameIT/frameworld?StepUntilX â™
include ☞http://mathhub.info/FrameIT/frameworld?IfThenElseX â™
rule rules?FilterRule (true) â™
diff --git a/source/Scrolls/W3DBouncingScroll.mmt b/source/Scrolls/W3DBouncingScroll.mmt
new file mode 100644
index 0000000..6055c0a
--- /dev/null
+++ b/source/Scrolls/W3DBouncingScroll.mmt
@@ -0,0 +1,98 @@
+namespace http://mathhub.info/FrameIT/frameworld âš
+
+import base http://mathhub.info/MitM/Foundation âš
+import arith http://mathhub.info/MitM/core/arithmetics âš
+import rules scala://datatypes.LFX.mmt.kwarc.info âš
+
+fixmeta ?FrameworldMeta âš
+
+theory W3DBouncingScroll =
+ meta ?MetaAnnotations?problemTheory ?W3DBouncingScroll/Problem â™
+ meta ?MetaAnnotations?solutionTheory ?W3DBouncingScroll/Solution â™
+ rule rules?FilterRule (true) â™
+ include ?IfThenElseX â™
+ include ?StepUntil â™
+ include ?Walls â™
+
+ theory funcs =
+ eq_zero : ℠⟶ bool ☠=
+ [val] (bool) ifx (leq_real_lit val 0.000001)
+ thenx ((bool) ifx (leq_real_lit (minus_real_lit 0.000001) val)
+ thenx true
+ elsex false)
+ elsex false â™
+ get_abcs : List[wall] ⟶ point ⟶ point ⟶ ℠⟶ List[point × wall] ☠=
+ [w, p, v, g] w map ([wi : wall] ⟨⟨(times_real_lit (wi.c) g),
+ (plus_real_lit (plus_real_lit (times_real_lit (wi.a) (v _x)) (times_real_lit (wi.b) (v _y))) (times_real_lit (wi.c) (v _z))),
+ (plus_real_lit (plus_real_lit (plus_real_lit (times_real_lit (wi.a) (p _x)) (times_real_lit (wi.b) (p _y))) (times_real_lit (wi.c) (p _z))) (minus_real_lit (wi.d)))⟩,
+ wi⟩) â™
+ mget_hts : (point × wall) ⟶ (℠× ℠× wall) ☠=
+ [cabc] (℠× ℠× wall) ifx (eq_zero ((πl cabc) _x))
+ thenx ((℠× ℠× wall) ifx (eq_zero ((πl cabc) _y))
+ thenx (⟨-1.0, -1.0, (πr cabc)⟩)
+ elsex (⟨minus_real_lit (times_real_lit ((πl cabc) _z) (inv_real_lit ((πl cabc) _y))),
+ minus_real_lit (times_real_lit ((πl cabc) _z) (inv_real_lit ((πl cabc) _y))), (πr cabc)⟩))
+ elsex ((℠× ℠× wall) ifx (leq_real_lit 0.0 (plus_real_lit (times_real_lit ((πl cabc) _y) ((πl cabc) _y)) (minus_real_lit (times_real_lit 2.0 (times_real_lit ((πl cabc) _x) ((πl cabc) _z))))))
+ thenx (⟨times_real_lit (plus_real_lit (minus_real_lit ((πl cabc) _y)) (sqrt (plus_real_lit (times_real_lit ((πl cabc) _y) ((πl cabc) _y)) (minus_real_lit (times_real_lit 2.0 (times_real_lit ((πl cabc) _x) ((πl cabc) _z))))))) (inv_real_lit ((πl cabc) _x)),
+ times_real_lit (plus_real_lit (minus_real_lit ((πl cabc) _y)) (minus_real_lit (sqrt (plus_real_lit (times_real_lit ((πl cabc) _y) ((πl cabc) _y)) (minus_real_lit (times_real_lit 2.0 (times_real_lit ((πl cabc) _x) ((πl cabc) _z)))))))) (inv_real_lit ((πl cabc) _x)), (πr cabc)⟩)
+ elsex (⟨-1.0, -1.0, (Ï€r cabc)⟩)) â™
+ get_pt : ℠⟶ point ⟶ point ⟶ ℠⟶ point ☠=
+ [rht, rp, rv, rg] ⟨plus_real_lit (rp _x) (times_real_lit (rv _x) rht),
+ plus_real_lit (rp _y) (times_real_lit (rv _y) rht),
+ plus_real_lit (plus_real_lit (rp _z) (times_real_lit (rv _z) rht)) (times_real_lit (times_real_lit 0.5 rg) (times_real_lit rht rht))⟩ â™
+ check_hit : (℠× wall) ⟶ point ⟶ point ⟶ ℠⟶ bool ☠=
+ [rw, rp, rv, rg] ([np : point] (bool) ifx (leq_real_lit (scalar_productI ((Ï€r rw).point1) ((Ï€r rw).u)) (scalar_productI np ((Ï€r rw).u)))
+ thenx ((bool) ifx (leq_real_lit (scalar_productI np ((Ï€r rw).u)) (scalar_productI ((Ï€r rw).point2) ((Ï€r rw).u)))
+ thenx ((bool) ifx (leq_real_lit (scalar_productI ((Ï€r rw).point1) (point_subtractI ((Ï€r rw).point4) ((Ï€r rw).point1))) (scalar_productI np (point_subtractI ((Ï€r rw).point4) ((Ï€r rw).point1))))
+ thenx (leq_real_lit (scalar_productI np (point_subtractI ((Ï€r rw).point4) ((Ï€r rw).point1))) (scalar_productI ((Ï€r rw).point4) (point_subtractI ((Ï€r rw).point4) ((Ï€r rw).point1))))
+ elsex false)
+ elsex false)
+ elsex false) (get_pt (Ï€l rw) rp rv rg) â™
+ fold_func : (℠× wall) ⟶ (point × â„) ⟶ (point × â„) ☠=
+ [cur][acc] (point × â„) ifx (leq_real_lit (Ï€l cur) (Ï€r acc)) thenx (⟨(Ï€r cur).norm_vec, (Ï€l cur)⟩) elsex acc â™
+ calc_new_vals : (point × point × (point × â„)) ⟶ (℠× â„) ⟶ (point × point) ☠=
+ [v, bv] ⟨get_pt (Ï€r (Ï€r (Ï€r v))) (Ï€l v) (Ï€l (Ï€r v)) (Ï€l bv), ([d : point] vec_multI (Ï€r bv) (point_subtractI d (vec_multI (times_real_lit 2.0 (scalar_productI d (Ï€l (Ï€r (Ï€r v))))) (Ï€l (Ï€r (Ï€r v)))))) (⟨(Ï€l (Ï€r v)) _x, (Ï€l (Ï€r v)) _y, plus_real_lit ((Ï€l (Ï€r v)) _z) (times_real_lit (Ï€r (Ï€r (Ï€r v))) (Ï€l bv))⟩)⟩ â™
+ end_cond : (point × point × (point × â„)) ⟶ bool ☠=
+ [vals] leq_real_lit (Ï€r (Ï€r (Ï€r vals))) 0.1 â™
+ map_reduce_hts : (℠× ℠× wall) ⟶ (℠× wall) ☠=
+ [wsi] (℠× wall) ifx (leq_real_lit (πl wsi) 0.000001)
+ thenx ((℠× wall) ifx (leq_real_lit (πl (πr wsi)) 0.000001)
+ thenx (⟨-1.0, πr (πr wsi)⟩)
+ elsex (⟨πl (πr wsi), πr (πr wsi)⟩))
+ elsex ((℠× wall) ifx (leq_real_lit (πl (πr wsi)) 0.000001)
+ thenx (⟨πl wsi, πr (πr wsi)⟩)
+ elsex ((℠× wall) ifx (leq_real_lit (πl wsi) (πl (πr wsi)))
+ thenx (⟨πl wsi, πr (πr wsi)⟩)
+ elsex (⟨πl (Ï€r wsi), Ï€r (Ï€r wsi)⟩))) â™
+ get_next_vals : List[wall] ⟶ (℠× â„) ⟶ ((point × point × (point × â„)) ⟶ (point × point × (point × â„))) ☠=
+ [aw, abv] ([v : point × point × (point × â„)] ([x : point × point] ⟨πl x, Ï€r x, ((((((get_abcs aw (Ï€l x) (Ï€r x) (Ï€l abv)) map mget_hts) map map_reduce_hts) filter ([wsj : ℠× wall] leq_real_lit 0.000001 (Ï€l wsj))) filter ([wsk : ℠× wall] check_hit wsk (Ï€l x) (Ï€r x) (Ï€l abv))) fold ⟨⟨-1.0, -1.0, -1.0⟩, 99999.9⟩ fold_func)⟩) (calc_new_vals v abv)) â™
+ prep : List[wall] ⟶ point ⟶ point ⟶ ℠⟶ (point × point × (point × â„)) ☠=
+ [awi, p, v, g] ⟨p, v, ((((((get_abcs awi p v g) map mget_hts) map map_reduce_hts) filter ([wsj : ℠× wall] leq_real_lit 0.000001 (Ï€l wsj))) filter ([wsk : ℠× wall] check_hit wsk p v g)) fold ⟨⟨-1.0, -1.0, -1.0⟩, 99999.9⟩ fold_func)⟩ â™
+ get_pos_fun: point ⟶ point ⟶ ℠⟶ (℠⟶ point) ☠=
+ [p, v, g] ([t] ⟨plus_real_lit (p _x) (times_real_lit (v _x) t), plus_real_lit (p _y) (times_real_lit (v _y) t), plus_real_lit (times_real_lit (times_real_lit 0.5 g) (times_real_lit t t)) (plus_real_lit (p _z) (times_real_lit (v _z) t))⟩) â™
+ red_ht : (point × point × (point × â„)) ⟶ ℠☠=
+ [cele] Ï€r (Ï€r (Ï€r cele)) â™
+ âš
+ // start position and velocity â™
+ theory Problem =
+ include ?W3DBouncingScroll/funcs â™
+ position: point ☠meta ?MetaAnnotations?label "Pos" â™
+ velocity: point ☠meta ?MetaAnnotations?label "Vel" â™
+ g_base: point ☠meta ?MetaAnnotations?label "G" â™
+ bounce: ℠☠meta ?MetaAnnotations?label "BO" â™
+ wallsr: List[point × point × point × point] ☠meta ?MetaAnnotations?label "WallsR" â™
+ âš
+
+ // the output of the scroll â™
+
+ theory Solution =
+ include ?W3DBouncingScroll/Problem â™
+ //testw : List[point × point × point × point] ☠= cons (⟨⟨0.0, 0.0, 0.0⟩, ⟨1.0, 0.0, 0.0⟩, ⟨2.0, 0.0, 0.0⟩, ⟨3.0, 0.0, 0.0⟩⟩) (cons (⟨⟨0.0, 1.0, 0.0⟩, ⟨1.0, 1.0, 0.0⟩, ⟨2.0, 1.0, 0.0⟩, ⟨3.0, 1.0, 0.0⟩⟩) nil) â™
+ //wallse : List[wall] ☠= wallsr map ([cw] create_wall (Ï€l cw) (Ï€l (Ï€r cw)) (Ï€l (Ï€r (Ï€r cw))) (Ï€r (Ï€r (Ï€r cw)))) â™
+ full_list: List[point × point × (point × â„)] ☠= stepUntil (point × point × (point × â„)) (prep (wallsr map ([cw] create_wall (Ï€l cw) (Ï€l (Ï€r cw)) (Ï€l (Ï€r (Ï€r cw))) (Ï€r (Ï€r (Ï€r cw))))) position velocity (g_base _y)) (get_next_vals (wallsr map ([cw] create_wall (Ï€l cw) (Ï€l (Ï€r cw)) (Ï€l (Ï€r (Ï€r cw))) (Ï€r (Ï€r (Ï€r cw))))) ⟨(g_base _y), bounce⟩) end_cond â™
+ ht_list: List[â„] ☠= full_list map red_ht â™
+ fun_list : List[℠⟶ point] ☠= full_list map ([vals] get_pos_fun (Ï€l vals) (Ï€l (Ï€r vals)) (g_base _y)) â™
+ meta ?MetaAnnotations?label "W3DBouncingScroll" â™
+ meta ?MetaAnnotations?description s"Bouncing " â™
+ âš
+âš
\ No newline at end of file
diff --git a/source/Scrolls/WBouncingScroll.mmt b/source/Scrolls/WBouncingScroll.mmt
index 7da8ea0..8e1317b 100644
--- a/source/Scrolls/WBouncingScroll.mmt
+++ b/source/Scrolls/WBouncingScroll.mmt
@@ -12,6 +12,7 @@ theory WBouncingScroll =
rule rules?FilterRule (true) â™
include ?IfThenElseX â™
include ?StepUntilX â™
+ include ?StepUntil â™
theory funcs =
calc_new_vals : (℠× â„) ⟶ ((℠× â„) × (℠× â„) × (℠× â„)) ⟶ ((℠× â„) × (℠× â„)) ☠=
@@ -47,6 +48,8 @@ theory WBouncingScroll =
[wsi, x, y, xv, yv, g] ⟨⟨x, y⟩, ⟨xv, yv⟩, (reduce_list_ht_pos wsi x y xv yv g) fold ((reduce_list_ht_neg wsi x y xv yv g) fold ⟨99999.9, -1.0⟩ fold_func) fold_func ⟩ â™
get_next_vals : List[(℠× â„) × (℠× â„)] ⟶ (℠× â„) ⟶ ((℠× â„) × (℠× â„) × (℠× â„)) ⟶ ((℠× â„) × (℠× â„) × (℠× â„)) ☠=
[wsi, bv, v] ([x : ((℠× â„) × (℠× â„))] ⟨⟨πl (Ï€l x), Ï€r (Ï€l x)⟩, ⟨πl (Ï€r x), Ï€r (Ï€r x)⟩, (reduce_list_ht_pos wsi (Ï€l (Ï€l x)) (Ï€r (Ï€l x)) (Ï€l (Ï€r x)) (Ï€r (Ï€r x)) (Ï€l bv)) fold ((reduce_list_ht_neg wsi (Ï€l (Ï€l x)) (Ï€r (Ï€l x)) (Ï€l (Ï€r x)) (Ï€r (Ï€r x)) (Ï€l bv)) fold ⟨99999.9, -1.0⟩ fold_func) fold_func ⟩) (calc_new_vals bv v) â™
+ get_next_vals_extra : List[(℠× â„) × (℠× â„)] ⟶ (℠× â„) ⟶ (((℠× â„) × (℠× â„) × (℠× â„)) ⟶ ((℠× â„) × (℠× â„) × (℠× â„))) ☠=
+ [wsi, bv] ([v : ((℠× â„) × (℠× â„) × (℠× â„))] ([x : ((℠× â„) × (℠× â„))] ⟨⟨πl (Ï€l x), Ï€r (Ï€l x)⟩, ⟨πl (Ï€r x), Ï€r (Ï€r x)⟩, (reduce_list_ht_pos wsi (Ï€l (Ï€l x)) (Ï€r (Ï€l x)) (Ï€l (Ï€r x)) (Ï€r (Ï€r x)) (Ï€l bv)) fold ((reduce_list_ht_neg wsi (Ï€l (Ï€l x)) (Ï€r (Ï€l x)) (Ï€l (Ï€r x)) (Ï€r (Ï€r x)) (Ï€l bv)) fold ⟨99999.9, -1.0⟩ fold_func) fold_func ⟩) (calc_new_vals bv v)) â™
end_cond : ((℠× â„) × (℠× â„) × (℠× â„)) ⟶ bool ☠=
[vals] leq_real_lit (Ï€l (Ï€r (Ï€r vals))) 0.1 â™
red_ht : ((℠× â„) × (℠× â„) × (℠× â„)) ⟶ ℠☠=
@@ -77,7 +80,8 @@ 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 _y), bounce⟩ (prep (walls map get_mc) (position _z) (position _y) (velocity _z) (velocity _y) (g_base _y)) get_next_vals end_cond â™
+ full_list: List[(℠× â„) × (℠× â„) × (℠× â„)] ☠= stepUntil ((℠× â„) × (℠× â„) × (℠× â„)) (prep (walls map get_mc) (position _z) (position _y) (velocity _z) (velocity _y) (g_base _y)) (get_next_vals_extra (walls map get_mc) ⟨(g_base _y), bounce⟩) 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 _y)) â™
meta ?MetaAnnotations?label "WBouncingScroll" â™
diff --git a/source/dynamics.mmt b/source/dynamics.mmt
index 48c12aa..d3dfc04 100644
--- a/source/dynamics.mmt
+++ b/source/dynamics.mmt
@@ -19,3 +19,45 @@ theory IfThenElseX =
ifthenelsex : {X: type} bool ⟶ X ⟶ X ⟶ X ☠# 1 ifx 2 thenx 3 elsex 4 â™
rule rules?IfThenElseRuleX (true) (false) â™
âš
+theory Walls =
+ //wall : type ☠= {'
+ point1 : point,
+ point2 : point,
+ point3 : point,
+ point4 : point,
+ u : point := point_subtractI point2 point1,
+ v : point := point_subtractI point3 point1,
+ vc : point := vec_cross u v,
+ a : â„ := vc _x,
+ b : â„ := vc _y,
+ c : â„ := vc _z,
+ d : â„ := plus_real_lit (plus_real_lit (times_real_lit a (point1 _x)) (times_real_lit b (point1 _y))) (times_real_lit c (point1 _z)),
+ length : â„ := sqrt (plus_real_lit (plus_real_lit (times_real_lit a a) (times_real_lit b b)) (times_real_lit c c)),
+ norm_vec : point := ⟨times_real_lit a (inv_real_lit length), times_real_lit b (inv_real_lit length), times_real_lit c (inv_real_lit length)⟩
+ '} â™
+ wall : type ☠= {'
+ point1 : point,
+ point2 : point,
+ point3 : point,
+ point4 : point,
+ u : point,
+ v : point,
+ vc : point,
+ a : â„,
+ b : â„,
+ c : â„,
+ d : â„,
+ length : â„,
+ norm_vec : point
+ '} â™
+ create_wall : point ⟶ point ⟶ point ⟶ point ⟶ wall ☠= [p1, p2, p3, p4] ([vcc : point] ['point1 := p1, point2 := p2, point3 := p3, point4 := p4,
+ u := point_subtractI p2 p1,
+ v := point_subtractI p3 p1,
+ vc := vcc, a := vcc _x, b := vcc _y, c := vcc _z,
+ d := plus_real_lit (plus_real_lit (times_real_lit (vcc _x) (p1 _x)) (times_real_lit (vcc _y) (p1 _y))) (times_real_lit (vcc _z) (p1 _z)),
+ length := sqrt (plus_real_lit (plus_real_lit (times_real_lit (vcc _x) (vcc _x)) (times_real_lit (vcc _y) (vcc _y))) (times_real_lit (vcc _z) (vcc _z))),
+ norm_vec := (⟨ times_real_lit (vcc _x) (inv_real_lit (sqrt (plus_real_lit (plus_real_lit (times_real_lit (vcc _x) (vcc _x)) (times_real_lit (vcc _y) (vcc _y))) (times_real_lit (vcc _z) (vcc _z))))),
+ times_real_lit (vcc _y) (inv_real_lit (sqrt (plus_real_lit (plus_real_lit (times_real_lit (vcc _x) (vcc _x)) (times_real_lit (vcc _y) (vcc _y))) (times_real_lit (vcc _z) (vcc _z))))),
+ times_real_lit (vcc _z) (inv_real_lit (sqrt (plus_real_lit (plus_real_lit (times_real_lit (vcc _x) (vcc _x)) (times_real_lit (vcc _y) (vcc _y))) (times_real_lit (vcc _z) (vcc _z)))))⟩) ']
+ ) (vec_cross (point_subtractI p2 p1) (point_subtractI p3 p1)) â™
+âš
\ No newline at end of file
--
GitLab