Skip to content
Snippets Groups Projects
Commit 35649e85 authored by Lucas-He's avatar Lucas-He
Browse files

Added a mmt file for 3D bouncing. (And a python File to call the Scroll). And... 

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
parent a536fd32
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
connect_to_mmt_W3Bounce.py 0 → 100644
+ 273
− 0
View file @ 35649e85
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 ---------------------------------------------------- #
scala/info/kwarc/mmt/frameit/rules/StepUntil.scala
+ 1
− 1
View file @ 35649e85
......@@ -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 {
......
source/DefaultSituationSpace.mmt
+ 1
− 0
View file @ 35649e85
......@@ -17,6 +17,7 @@ theory DefaultSituationSpace =
include ?CircleScroll ❙
include ?BouncingScroll ❙
include ?WBouncingScroll ❙
include ?W3DBouncingScroll ❙
// include ?SinOppositeLeg ❙
include ?CircleLineAngleScroll ❙
include ?CircleAreaScroll ❙
......
source/IntegrationTests/DynamicsDebug.mmt
+ 17
− 2
View file @ 35649e85
......@@ -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) ❙
......
source/Scrolls/W3DBouncingScroll.mmt 0 → 100644
+ 98
− 0
View file @ 35649e85
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
source/Scrolls/WBouncingScroll.mmt
+ 5
− 1
View file @ 35649e85
......@@ -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" ❙
......
source/dynamics.mmt
+ 42
− 0
View file @ 35649e85
......@@ -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
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