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

Added the 2D wall Bouncing Scroll (WBouncingScroll) and a new StepUntil... 

Added the 2D wall Bouncing Scroll (WBouncingScroll) and a new StepUntil Function that also takes constant values
parent dca7782c
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
scala/info/kwarc/mmt/frameit/rules/StepUntilX.scala 0 → 100644
+ 65
− 0
View file @ a2e6a7c3
package info.kwarc.mmt.frameit.rules
import info.kwarc.mmt.api.checking._
import info.kwarc.mmt.api.{DPath, GlobalName, LocalName, ParametricRule, Rule, RuleSet}
import info.kwarc.mmt.api.frontend.Controller
import info.kwarc.mmt.api.objects._
import Conversions._
import info.kwarc.mmt.api.uom.{Simplifiability, Simplify}
import info.kwarc.mmt.lf.{Apply, ApplySpine, Arrow, OfType, Pi}
import info.kwarc.mmt.LFX.datatypes.{Listtype, Ls}
import info.kwarc.mmt.api.utils.URI
import scala.collection.mutable
object StepUntilX {
val ns: DPath = DPath(URI.http colon "mathhub.info") / "FrameIT" / "frameworld"
val path: GlobalName = ns ? "StepUntilX" ? "stepUntilX"
val rawhead: OMID = OMS(path)
def apply(tpA: Term, tpB: Term, tpC: Term, vB: Term, vC: Term, vA: Term, f: Term, tC: Term): Term =
ApplySpine(this.rawhead, tpA, tpB, tpC, vB, vC, vA, f, tC)
def unapply(tm : Term) : Option[(Term, Term, Term, Term, Term, Term, Term, Term)] = tm match {
case ApplySpine(this.rawhead, List(tpA, tpB, tpC, vB, vC, vA, f, tC)) => Some((tpA, tpB, tpC, vB, vC, vA, f, tC))
case _ => None
}
}
object StepUntilXRule extends ParametricRule {
// todo: document
private val DEBUG_MAX_ITER_COUNT = 100
override def apply(controller: Controller, home: Term, args: List[Term]): Rule = args match {
case List(truetm) =>
RuleSet(StepUntilXComp(truetm))
case _ =>
???
}
case class StepUntilXComp(truetm: Term) extends ComputationRule(StepUntilX.path) {
override def applicable(t: Term): Boolean = t match {
case StepUntilX(_, _, _, _, _, _, _, _) => true
case _ => false
}
override def apply(check: CheckingCallback)(tm: Term, covered: Boolean)(implicit stack: Stack, history: History): Simplifiability = tm match {
case StepUntilX(_, _, _, vB, vC, vA, f, tC) =>
val values = mutable.ListBuffer[Term]()
val valB = check.simplify(vB)
val valC = check.simplify(vC)
var iter = 0
var cur = check.simplify(vA)
while (iter < DEBUG_MAX_ITER_COUNT) {
iter += 1
check.tryToCheckWithoutDelay(Equality(stack, Apply(tC, cur), truetm, None)) match {
case Some(true) =>
return Simplify(Ls(values.toSeq : _*))
case Some(false) | None =>
values += cur
cur = check.simplify(ApplySpine(f, valB, valC, cur))
}
}
// todo: try to log something via stack, history, check, or this
Simplify(Ls(values.toSeq : _*))
case _ => Simplifiability.NoRecurse
}
}
}
\ No newline at end of file
source/DefaultSituationSpace.mmt
+ 1
− 0
View file @ a2e6a7c3
......@@ -16,6 +16,7 @@ theory DefaultSituationSpace =
include ?Midpoint ❙
include ?CircleScroll ❙
include ?BouncingScroll ❙
include ?WBouncingScroll ❙
// include ?SinOppositeLeg ❙
include ?CircleLineAngleScroll ❙
include ?CircleAreaScroll ❙
......
source/IntegrationTests/DynamicsDebug.mmt
+ 64
− 1
View file @ a2e6a7c3
......@@ -2,12 +2,13 @@ namespace http://mathhub.info/FrameIT/frameworld/integrationtests/dynamicsdebug
rule scala://parser.api.mmt.kwarc.info?MMTURILexer ❚
import rules scala://datatypes.LFX.mmt.kwarc.info ❚
import frameworld http://mathhub.info/FrameIT/frameworld ❚
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 10.0) thenx 1.0 elsex 0.0 ❙
❚
theory StepUntilDebug =
......@@ -16,3 +17,65 @@ theory StepUntilDebug =
my_list: List[ℝ] ❘ = stepUntil ℝ 0.0 ([x: ℝ] plus_real_lit x 1.0) ([x: ℝ] leq_real_lit 10.0 x) ❙
//my_list: ℝ ❘ = stepUntil ℝ 0.0 ([x: ℝ] plus_real_lit x 1.0) ([x: ℝ] leq_real_lit 10.0 x) ❙
❚
theory StepUntilXDebug =
include ☞http://mathhub.info/FrameIT/frameworld?StepUntilX ❙
//my_list: List[ℝ] ❘ = (cons 0.0 (cons 2.0 nil)) map ([x: ℝ] plus_real_lit x 1.0) ❙
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 =
include ☞http://mathhub.info/FrameIT/frameworld?StepUntilX ❙
include ☞http://mathhub.info/FrameIT/frameworld?IfThenElseX ❙
rule rules?FilterRule (true) ❙
calc_new_vals : (ℝ × ℝ) ⟶ ((ℝ × ℝ) × (ℝ × ℝ) × (ℝ × ℝ)) ⟶ ((ℝ × ℝ) × (ℝ × ℝ)) ❘ =
[bv, v] ⟨⟨plus_real_lit (πl (πl v)) (times_real_lit (πl (πl (πr v))) (πl (πr (πr v)))), plus_real_lit (plus_real_lit (πr (πl v)) (times_real_lit (πr (πl (πr v))) (πl (πr (πr v))))) (times_real_lit (times_real_lit 0.5 (πl bv)) (times_real_lit (πl (πr (πr v))) (πl (πr (πr v)))))⟩, ⟨ times_real_lit (πr bv) (plus_real_lit (πl (πl (πr v))) (times_real_lit (times_real_lit (times_real_lit 2.0 (πr (πr (πr v)))) (plus_real_lit (πr (πl (πr v))) (minus_real_lit (times_real_lit (πr (πr (πr v))) (πl (πl (πr v))))))) (inv_real_lit (plus_real_lit 1.0 (times_real_lit (πr (πr (πr v))) (πr (πr (πr v)))))))), times_real_lit (πr bv) (plus_real_lit (plus_real_lit (πr (πl (πr v))) (times_real_lit (πl bv) (πl (πr (πr v))))) (minus_real_lit (times_real_lit (times_real_lit 2.0 (plus_real_lit (plus_real_lit (πr (πl (πr v))) (times_real_lit (πl bv) (πl (πr (πr v))))) (minus_real_lit (times_real_lit (πr (πr (πr v))) (πl (πl (πr v))))))) (inv_real_lit (plus_real_lit 1.0 (times_real_lit (πr (πr (πr v))) (πr (πr (πr v)))))))))⟩⟩ ❙
fold_func : (((ℝ × ℝ) × (ℝ × ℝ)) × ℝ) ⟶ (ℝ × ℝ) ⟶ (ℝ × ℝ) ❘ =
[cur][acc] (ℝ × ℝ) ifx (leq_real_lit (πl acc) (πr (πl (πl cur)))) thenx acc elsex ⟨πr (πl (πl cur)), πr cur⟩ ❙
check_hit : ((ℝ × ℝ) × (ℝ × ℝ)) ⟶ bool ❘ =
[p] leq_real_lit 0.000001 (πr (πl p)) ❙
check_hit2 : ((ℝ × ℝ) × (ℝ × ℝ)) ⟶ bool ❘ =
[p] leq_real_lit (πl (πr p)) (πl (πl p)) ❙
check_hit3 : ((ℝ × ℝ) × (ℝ × ℝ)) ⟶ bool ❘ =
[p] leq_real_lit (πl (πl p)) (πr (πr p)) ❙
get_hit_time_pos : ((ℝ × ℝ) × (ℝ × ℝ)) ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ❘ =
[wi, x, y, xv, yv, g] times_real_lit (inv_real_lit g) (plus_real_lit (plus_real_lit (times_real_lit (πl (πl wi)) xv) (minus_real_lit yv)) (sqrt ( plus_real_lit (times_real_lit (plus_real_lit yv (minus_real_lit (times_real_lit (πl (πl wi)) xv))) (plus_real_lit yv (minus_real_lit (times_real_lit (πl (πl wi)) xv)))) (minus_real_lit (times_real_lit (times_real_lit 2.0 g) (plus_real_lit (plus_real_lit y (minus_real_lit (times_real_lit (πl (πl wi)) x))) (minus_real_lit (πr (πl wi))))))))) ❙
get_hit_time_neg : ((ℝ × ℝ) × (ℝ × ℝ)) ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ❘ =
[wi, x, y, xv, yv, g] times_real_lit (inv_real_lit g) (plus_real_lit (plus_real_lit (times_real_lit (πl (πl wi)) xv) (minus_real_lit yv)) (minus_real_lit (sqrt ( plus_real_lit (times_real_lit (plus_real_lit yv (minus_real_lit (times_real_lit (πl (πl wi)) xv))) (plus_real_lit yv (minus_real_lit (times_real_lit (πl (πl wi)) xv)))) (minus_real_lit (times_real_lit (times_real_lit 2.0 g) (plus_real_lit (plus_real_lit y (minus_real_lit (times_real_lit (πl (πl wi)) x))) (minus_real_lit (πr (πl wi)))))))))) ❙
get_x_ht : ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ❘ = [x, xv, ht] plus_real_lit x (times_real_lit xv ht) ❙
combine_ht_info_pos : ((ℝ × ℝ) × (ℝ × ℝ)) ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ (((ℝ × ℝ) × (ℝ × ℝ)) × ℝ) ❘ =
[wi, x, y, xv, yv, g] ⟨⟨⟨get_x_ht x xv (get_hit_time_pos wi x y xv yv g), get_hit_time_pos wi x y xv yv g⟩, ⟨(πl (πr wi)), (πr (πr wi))⟩⟩, (πl (πl wi))⟩ ❙
combine_ht_info_neg : ((ℝ × ℝ) × (ℝ × ℝ)) ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ (((ℝ × ℝ) × (ℝ × ℝ)) × ℝ) ❘ =
[wi, x, y, xv, yv, g] ⟨⟨⟨get_x_ht x xv (get_hit_time_neg wi x y xv yv g), get_hit_time_neg wi x y xv yv g⟩, ⟨(πl (πr wi)), (πr (πr wi))⟩⟩, (πl (πl wi))⟩ ❙
get_m : ((ℝ × ℝ) × (ℝ × ℝ)) ⟶ ℝ ❘ = [w] times_real_lit (plus_real_lit (πr (πr w)) (minus_real_lit (πr (πl w)))) (inv_real_lit (plus_real_lit (πl (πr w)) (minus_real_lit (πl (πl w))))) ❙
get_c : (ℝ × ℝ) ⟶ ℝ ⟶ ℝ ❘ = [w][m] plus_real_lit (πr w) (minus_real_lit (times_real_lit (πl w) m)) ❙
get_mc : ((ℝ × ℝ) × (ℝ × ℝ)) ⟶ ((ℝ × ℝ) × (ℝ × ℝ)) ❘ = [w] ⟨⟨get_m w, get_c (πl w) (get_m w)⟩, ⟨πl (πl w), πl (πr w)⟩⟩ ❙
reduce_list_ht_pos : List[(ℝ × ℝ) × (ℝ × ℝ)] ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ List[((ℝ × ℝ) × (ℝ × ℝ)) × ℝ] ❘ =
[wsi, x, y, xv, yv, g] (((wsi map ([wi] combine_ht_info_pos wi x y xv yv g)) filter ([wib] check_hit (πl wib))) filter ([wib] check_hit2 (πl wib))) filter ([wib] check_hit3 (πl wib)) ❙
reduce_list_ht_neg : List[(ℝ × ℝ) × (ℝ × ℝ)] ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ List[((ℝ × ℝ) × (ℝ × ℝ)) × ℝ] ❘ =
[wsi, x, y, xv, yv, g] (((wsi map ([wi] combine_ht_info_neg wi x y xv yv g)) filter ([wib] check_hit (πl wib))) filter ([wib] check_hit2 (πl wib))) filter ([wib] check_hit3 (πl wib)) ❙
prep : List[(ℝ × ℝ) × (ℝ × ℝ)] ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ((ℝ × ℝ) × (ℝ × ℝ) × (ℝ × ℝ)) ❘ =
[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) ❙
end_cond : ((ℝ × ℝ) × (ℝ × ℝ) × (ℝ × ℝ)) ⟶ bool ❘ =
[vals] leq_real_lit (πl (πr (πr vals))) 0.1 ❙
red_ht : ((ℝ × ℝ) × (ℝ × ℝ) × (ℝ × ℝ)) ⟶ ℝ ❘ =
[cele] πl (πr (πr cele)) ❙
get_pos_fun: ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ (ℝ ⟶ (ℝ × ℝ)) ❘ =
[x,y,xv,yv,g] ([t] ⟨plus_real_lit x (times_real_lit xv t), plus_real_lit (times_real_lit (times_real_lit 0.5 g) (times_real_lit t t)) (plus_real_lit y (times_real_lit yv t))⟩ ) ❙
my_list: List[(ℝ × ℝ) × (ℝ × ℝ) × (ℝ × ℝ)] ❘ = stepUntilX ((ℝ × ℝ) × (ℝ × ℝ) × (ℝ × ℝ)) List[(ℝ × ℝ) × (ℝ × ℝ)] (ℝ × ℝ) ((cons ⟨⟨-10000.0, 0.0⟩, ⟨10000.0, 0.0⟩⟩ (cons ⟨⟨0.0, -1000.0⟩, ⟨0.1, 1000.0⟩⟩ (cons ⟨⟨50.0, -150.0⟩, ⟨50.1, 150.0⟩⟩ nil))) map get_mc) ⟨-200.0, 0.5⟩ (prep ((cons ⟨⟨-10000.0, 0.0⟩, ⟨10000.0, 0.0⟩⟩ (cons ⟨⟨0.0, -1000.0⟩, ⟨0.1, 1000.0⟩⟩ (cons ⟨⟨50.0, -150.0⟩, ⟨50.1, 150.0⟩⟩ nil))) map get_mc) 200.0 300.0 (-100.0) 100.0 (-200.0)) get_next_vals end_cond ❙
//my_list: ℝ ❘ = stepUntil ℝ 0.0 ([x: ℝ] plus_real_lit x 1.0) ([x: ℝ] leq_real_lit 10.0 x) ❙
// full_list
: List[ ℝ×ℝ×(ℝ×ℝ)×(ℝ×ℝ)]
= stepUntilX (ℝ×ℝ×(ℝ×ℝ)×(ℝ×ℝ)) List[ ℝ×ℝ×(ℝ×ℝ)] (ℝ×ℝ) cons ⟨⟨0.0,0.0⟩,⟨-10000.0,10000.0⟩⟩ nil ⟨-200.0,0.5⟩ ⟨⟨200.0,300.0⟩,⟨-100.0,100.0⟩,⟨2.302775638,0.0⟩⟩ [wsi,bv,v]([xt:ℝ×ℝ×(ℝ×ℝ)]⟨⟨πl πl xt,πr πl xt⟩,⟨πl πr xt,πr πr xt⟩,(([wsit,x,y,xv,yv,g]wsit map [wi]([wi,x,y,xv,yv,g]⟨⟨⟨([x,xv,ht]x+(xv×ht)) x xv (([wi,x,y,xv,yv,g]g⁻¹×((πl πl wi)×xv)+-yv+-(sqrt (yv+-((πl πl wi)×xv)×yv+-((πl πl wi)×xv))+-(2.0×g×y+-((πl πl wi)×x)+-πr πl wi))) wi x y xv yv g),([wi,x,y,xv,yv,g]g⁻¹×((πl πl wi)×xv)+-yv+-(sqrt (yv+-((πl πl wi)×xv)×yv+-((πl πl wi)×xv))+-(2.0×g×y+-((πl πl wi)×x)+-πr πl wi))) wi x y xv yv g⟩,⟨πl πr wi,πr πr wi⟩⟩,πl πl wi⟩) wi x y xv yv g) wsi (πl πl xt) (πr πl xt) (πl πr xt) (πr πr xt) πl bv) fold ⟨99999.9,-1.0⟩ [cur][acc](ℝ×ℝ) ifx (leq_real_lit (πl acc) πr πl πl cur) thenx acc elsex ⟨πr πl πl cur,πr cur⟩⟩) (([bv,v]⟨⟨(πl πl v)+((πl πl πr v)×πl πr πr v),(πr πl v)+((πr πl πr v)×πl πr πr v)+(0.5×πl bv×((πl πr πr v)×πl πr πr v))⟩,⟨(πr bv)×(πl πl πr v)+(2.0×πr πr πr v×(πr πl πr v)+-((πr πr πr v)×πl πl πr v)×(1.0+((πr πr πr v)×πr πr πr v))⁻¹),(πr bv)×(πr πl πr v)+((πl bv)×πl πr πr v)+-(2.0×(πr πl πr v)+((πl bv)×πl πr πr v)+-((πr πr πr v)×πl πl πr v)×(1.0+((πr πr πr v)×πr πr πr v))⁻¹)⟩⟩) bv v) [vals]leq_real_lit (πl πr πr vals) 0.1 ❙
//iterated_fun: List[ ℝ×ℝ×(ℝ×ℝ)] ⟶ (ℝ×ℝ) ⟶ (ℝ×ℝ×(ℝ×ℝ)×(ℝ×ℝ)) ⟶ (ℝ×ℝ×(ℝ×ℝ)) ⟶ (ℝ×ℝ×(ℝ×ℝ)×(ℝ×ℝ)) ❘
= [wsi,bv,v,xt] ⟨⟨πl πl xt,πr πl xt⟩,⟨πl πr xt,πr πr xt⟩,(([wsit: List[(ℝ × ℝ) × (ℝ × ℝ)],x: ℝ,y: ℝ,xv: ℝ,yv: ℝ,g: ℝ]wsit map [wi: (ℝ × ℝ) × (ℝ × ℝ)]([wi: (ℝ × ℝ) × (ℝ × ℝ), x: ℝ,y: ℝ, xv: ℝ, yv: ℝ, g: ℝ]⟨⟨⟨([x: ℝ,xv: ℝ,ht: ℝ]x+(xv×ht)) x xv (([wi: (ℝ × ℝ) × (ℝ × ℝ), x: ℝ,y: ℝ, xv: ℝ, yv: ℝ, g: ℝ]g⁻¹×((πl πl wi)×xv)+-yv+-(sqrt (yv+-((πl πl wi)×xv)×yv+-((πl πl wi)×xv))+-(2.0×g×y+-((πl πl wi)×x)+-πr πl wi))) wi x y xv yv g),([wi: (ℝ × ℝ) × (ℝ × ℝ), x: ℝ,y: ℝ, xv: ℝ, yv: ℝ, g: ℝ]g⁻¹×((πl πl wi)×xv)+-yv+-(sqrt (yv+-((πl πl wi)×xv)×yv+-((πl πl wi)×xv))+-(2.0×g×y+-((πl πl wi)×x)+-πr πl wi))) wi x y xv yv g⟩,⟨πl πr wi,πr πr wi⟩⟩,πl πl wi⟩) wi x y xv yv g) wsi (πl πl xt) (πr πl xt) (πl πr xt) (πr πr xt) πl bv) fold ⟨99999.9,-1.0⟩ [cur: ((ℝ × ℝ) × (ℝ × ℝ)) × ℝ][acc: ℝ × ℝ](ℝ×ℝ) ifx (leq_real_lit (πl acc) πr πl πl cur) thenx acc elsex ⟨πr πl πl cur,πr cur⟩⟩ ❙
// (([bv,v]⟨⟨(πl πl v)+((πl πl πr v)×πl πr πr v),(πr πl v)+((πr πl πr v)×πl πr πr v)+(0.5×πl bv×((πl πr πr v)×πl πr πr v))⟩,⟨(πr bv)×(πl πl πr v)+(2.0×πr πr πr v×(πr πl πr v)+-((πr πr πr v)×πl πl πr v)×(1.0+((πr πr πr v)×πr πr πr v))⁻¹),(πr bv)×(πr πl πr v)+((πl bv)×πl πr πr v)+-(2.0×(πr πl πr v)+((πl bv)×πl πr πr v)+-((πr πr πr v)×πl πl πr v)×(1.0+((πr πr πr v)×πr πr πr v))⁻¹)⟩⟩) bv v) ❙
❚
source/Scrolls/WBouncingScroll.mmt 0 → 100644
+ 83
− 0
View file @ a2e6a7c3
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 WBouncingScroll =
meta ?MetaAnnotations?problemTheory ?WBouncingScroll/Problem ❙
meta ?MetaAnnotations?solutionTheory ?WBouncingScroll/Solution ❙
rule rules?FilterRule (true) ❙
include ?IfThenElseX ❙
include ?StepUntilX ❙
theory funcs =
calc_new_vals : (ℝ × ℝ) ⟶ ((ℝ × ℝ) × (ℝ × ℝ) × (ℝ × ℝ)) ⟶ ((ℝ × ℝ) × (ℝ × ℝ)) ❘ =
[bv, v] ⟨⟨plus_real_lit (πl (πl v)) (times_real_lit (πl (πl (πr v))) (πl (πr (πr v)))), plus_real_lit (plus_real_lit (πr (πl v)) (times_real_lit (πr (πl (πr v))) (πl (πr (πr v))))) (times_real_lit (times_real_lit 0.5 (πl bv)) (times_real_lit (πl (πr (πr v))) (πl (πr (πr v)))))⟩, ⟨ times_real_lit (πr bv) (plus_real_lit (πl (πl (πr v))) (times_real_lit (times_real_lit (times_real_lit 2.0 (πr (πr (πr v)))) (plus_real_lit (plus_real_lit (πr (πl (πr v))) (times_real_lit (πl bv) (πl (πr (πr v))))) (minus_real_lit (times_real_lit (πr (πr (πr v))) (πl (πl (πr v))))))) (inv_real_lit (plus_real_lit 1.0 (times_real_lit (πr (πr (πr v))) (πr (πr (πr v)))))))), times_real_lit (πr bv) (plus_real_lit (plus_real_lit (πr (πl (πr v))) (times_real_lit (πl bv) (πl (πr (πr v))))) (minus_real_lit (times_real_lit (times_real_lit 2.0 (plus_real_lit (plus_real_lit (πr (πl (πr v))) (times_real_lit (πl bv) (πl (πr (πr v))))) (minus_real_lit (times_real_lit (πr (πr (πr v))) (πl (πl (πr v))))))) (inv_real_lit (plus_real_lit 1.0 (times_real_lit (πr (πr (πr v))) (πr (πr (πr v)))))))))⟩⟩ ❙
fold_func : (((ℝ × ℝ) × (ℝ × ℝ)) × ℝ) ⟶ (ℝ × ℝ) ⟶ (ℝ × ℝ) ❘ =
[cur][acc] (ℝ × ℝ) ifx (leq_real_lit (πl acc) (πr (πl (πl cur)))) thenx acc elsex ⟨πr (πl (πl cur)), πr cur⟩ ❙
check_hit : ((ℝ × ℝ) × (ℝ × ℝ)) ⟶ bool ❘ =
[p] leq_real_lit 0.000001 (πr (πl p)) ❙
check_hit2 : ((ℝ × ℝ) × (ℝ × ℝ)) ⟶ bool ❘ =
[p] leq_real_lit (πl (πr p)) (πl (πl p)) ❙
check_hit3 : ((ℝ × ℝ) × (ℝ × ℝ)) ⟶ bool ❘ =
[p] leq_real_lit (πl (πl p)) (πr (πr p)) ❙
get_hit_time_pos : ((ℝ × ℝ) × (ℝ × ℝ)) ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ❘ =
[wi, x, y, xv, yv, g] times_real_lit (inv_real_lit g) (plus_real_lit (plus_real_lit (times_real_lit (πl (πl wi)) xv) (minus_real_lit yv)) (sqrt ( plus_real_lit (times_real_lit (plus_real_lit yv (minus_real_lit (times_real_lit (πl (πl wi)) xv))) (plus_real_lit yv (minus_real_lit (times_real_lit (πl (πl wi)) xv)))) (minus_real_lit (times_real_lit (times_real_lit 2.0 g) (plus_real_lit (plus_real_lit y (minus_real_lit (times_real_lit (πl (πl wi)) x))) (minus_real_lit (πr (πl wi))))))))) ❙
get_hit_time_neg : ((ℝ × ℝ) × (ℝ × ℝ)) ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ❘ =
[wi, x, y, xv, yv, g] times_real_lit (inv_real_lit g) (plus_real_lit (plus_real_lit (times_real_lit (πl (πl wi)) xv) (minus_real_lit yv)) (minus_real_lit (sqrt ( plus_real_lit (times_real_lit (plus_real_lit yv (minus_real_lit (times_real_lit (πl (πl wi)) xv))) (plus_real_lit yv (minus_real_lit (times_real_lit (πl (πl wi)) xv)))) (minus_real_lit (times_real_lit (times_real_lit 2.0 g) (plus_real_lit (plus_real_lit y (minus_real_lit (times_real_lit (πl (πl wi)) x))) (minus_real_lit (πr (πl wi)))))))))) ❙
get_x_ht : ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ❘ = [x, xv, ht] plus_real_lit x (times_real_lit xv ht) ❙
combine_ht_info_pos : ((ℝ × ℝ) × (ℝ × ℝ)) ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ (((ℝ × ℝ) × (ℝ × ℝ)) × ℝ) ❘ =
[wi, x, y, xv, yv, g] ⟨⟨⟨get_x_ht x xv (get_hit_time_pos wi x y xv yv g), get_hit_time_pos wi x y xv yv g⟩, ⟨(πl (πr wi)), (πr (πr wi))⟩⟩, (πl (πl wi))⟩ ❙
combine_ht_info_neg : ((ℝ × ℝ) × (ℝ × ℝ)) ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ (((ℝ × ℝ) × (ℝ × ℝ)) × ℝ) ❘ =
[wi, x, y, xv, yv, g] ⟨⟨⟨get_x_ht x xv (get_hit_time_neg wi x y xv yv g), get_hit_time_neg wi x y xv yv g⟩, ⟨(πl (πr wi)), (πr (πr wi))⟩⟩, (πl (πl wi))⟩ ❙
get_m : ((ℝ × ℝ) × (ℝ × ℝ)) ⟶ ℝ ❘ = [w] times_real_lit (plus_real_lit (πr (πr w)) (minus_real_lit (πr (πl w)))) (inv_real_lit (plus_real_lit (πl (πr w)) (minus_real_lit (πl (πl w))))) ❙
get_c : (ℝ × ℝ) ⟶ ℝ ⟶ ℝ ❘ = [w][m] plus_real_lit (πr w) (minus_real_lit (times_real_lit (πl w) m)) ❙
get_mc : ((ℝ × ℝ) × (ℝ × ℝ)) ⟶ ((ℝ × ℝ) × (ℝ × ℝ)) ❘ = [w] ⟨⟨get_m w, get_c (πl w) (get_m w)⟩, ⟨πl (πl w), πl (πr w)⟩⟩ ❙
reduce_list_ht_pos : List[(ℝ × ℝ) × (ℝ × ℝ)] ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ List[((ℝ × ℝ) × (ℝ × ℝ)) × ℝ] ❘ =
[wsi, x, y, xv, yv, g] (((wsi map ([wi] combine_ht_info_pos wi x y xv yv g)) filter ([wib] check_hit (πl wib))) filter ([wib] check_hit2 (πl wib))) filter ([wib] check_hit3 (πl wib)) ❙
reduce_list_ht_neg : List[(ℝ × ℝ) × (ℝ × ℝ)] ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ List[((ℝ × ℝ) × (ℝ × ℝ)) × ℝ] ❘ =
[wsi, x, y, xv, yv, g] (((wsi map ([wi] combine_ht_info_neg wi x y xv yv g)) filter ([wib] check_hit (πl wib))) filter ([wib] check_hit2 (πl wib))) filter ([wib] check_hit3 (πl wib)) ❙
prep : List[(ℝ × ℝ) × (ℝ × ℝ)] ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ((ℝ × ℝ) × (ℝ × ℝ) × (ℝ × ℝ)) ❘ =
[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) ❙
end_cond : ((ℝ × ℝ) × (ℝ × ℝ) × (ℝ × ℝ)) ⟶ bool ❘ =
[vals] leq_real_lit (πl (πr (πr vals))) 0.1 ❙
red_ht : ((ℝ × ℝ) × (ℝ × ℝ) × (ℝ × ℝ)) ⟶ ℝ ❘ =
[cele] πl (πr (πr cele)) ❙
get_pos_fun: ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ (ℝ ⟶ (ℝ × ℝ)) ❘ =
[x,y,xv,yv,g] ([t] ⟨plus_real_lit x (times_real_lit xv t), plus_real_lit (times_real_lit (times_real_lit 0.5 g) (times_real_lit t t)) (plus_real_lit y (times_real_lit yv t))⟩ ) ❙
❚
// 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" ❙
bounce: ℝ ❘ meta ?MetaAnnotations?label "BO" ❙
walls: List[(ℝ × ℝ) × (ℝ × ℝ)] ❘ meta ?MetaAnnotations?label "Walls" ❙
❚
// the output of the scroll ❙
theory Solution =
include ?WBouncingScroll/Problem ❙
//mcws : List[(ℝ × ℝ) × (ℝ × ℝ)] ❘ = get_mc_list walls ❙
//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 ❙
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) ❙
meta ?MetaAnnotations?label "WBouncingScroll" ❙
meta ?MetaAnnotations?description s"Bouncing " ❙
❚
❚
\ No newline at end of file
source/dynamics.mmt
+ 5
− 1
View file @ a2e6a7c3
......@@ -10,8 +10,12 @@ theory StepUntil =
//stepUntil : {X: type} X ⟶ (X ⟶ X) ⟶ (X ⟶ bool) ⟶ X ❘ # stepUntil 1 2 3 4 ❙
rule rules?StepUntilRule (true) ❙
❚
theory StepUntilX =
stepUntilX : {A: type}{B: type}{C: type} B ⟶ C ⟶ A ⟶ (B ⟶ C ⟶ A ⟶ A) ⟶ (A ⟶ bool) ⟶ List[A] ❘ # stepUntilX 1 2 3 4 5 6 7 8 ❙
rule rules?StepUntilXRule (true) ❙
❚
theory IfThenElseX =
// {X: type} X ⟶ (X ⟶ X) ⟶ (X ⟶ bool) ⟶ List[X] ❙
ifthenelsex : {X: type} bool ⟶ X ⟶ X ⟶ X ❘ # ifx 2 thenx 3 elsex 4 ❙
ifthenelsex : {X: type} bool ⟶ X ⟶ X ⟶ X ❘ # 1 ifx 2 thenx 3 elsex 4 ❙
rule rules?IfThenElseRuleX (true) (false) ❙
❚
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