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

Added StepUntil.scala and changed BouncingScroll

parent c4ea3dc9
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/StepUntil.scala 0 → 100644
+ 105
− 0
View file @ 19f9d797
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, Arrow, OfType, Pi}
import info.kwarc.mmt.LFX.datatypes.{Listtype, Ls}
import info.kwarc.mmt.api.utils.URI
object StepUntil {
val ns: DPath = DPath(URI.http colon "mathhub.info") / "FrameIT" / "frameworld"
val path: GlobalName = ns ? "StepUntilWrap" ? "stepUntil"
val term: OMID = OMS(path)
def apply(iv: Term, f: Term, tC: Term): Term = OMA(this.term, List(iv, f, tC))
def unapply(tm : Term) : Option[(Term,Term,Term)] = tm match {
case OMA(this.term, List(iv, f, tC)) => Some((iv, f, tC))
case _ => None
}
}
object StepUntilRule 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(StepUntilComp(truetm), StepUntilInfTypingRule(truetm))
case _ =>
???
}
case class StepUntilComp(truetm: Term) extends ComputationRule(StepUntil.path) {
override def apply(check: CheckingCallback)(tm: Term, covered: Boolean)(implicit stack: Stack, history: History): Simplifiability = tm match {
case StepUntil(iv, f, tC) =>
var values = Seq[Term]()
var iter = 0
var cur = iv
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 : _*))
case Some(false) | None =>
values = values :+ cur
cur = Apply(f, cur)
}
}
// todo: try to log something via stack, history, check, or this
Simplify(Ls(values : _*))
case _ => Simplifiability.NoRecurse
}
}
case class StepUntilInfTypingRule(truetm: Term) extends InferenceAndTypingRule(StepUntil.path, OfType.path) {
override def apply(solver: Solver, tm: Term, tp: Option[Term], covered: Boolean)(implicit stack: Stack, history: History)
: (Option[Term], Option[Boolean]) = tm match {
case StepUntil(iv, _, _) =>
solver.inferType(iv) match {
case Some(tpA) =>
(Some(Listtype(tpA)),Some(true))
case _ =>
(None, None)
}
case _ =>
(None, None)
}
/**val (p, tpA) = (tm, tp) match {
case (StepUntil(iv, f, tC), Some(Listtype(tp1))) =>
solver.check(Typing(stack, iv, tp1, None))
solver.inferType(f).map(solver.safeSimplifyUntil(_)(Arrow.unapply)._1) match {
case Some(Pi(x,tpA1,tpB1)) if !tpB1.freeVars.contains(x) =>
if (!covered) {
solver.check(Subtyping(stack, iv, tpA1))
solver.check(Typing(stack, iv, tpB1))
}
(tC, tp1)
case _ =>
return (None,None)
}
case (StepUntil(iv, f, tC), _) =>
solver.inferType(f).map(solver.safeSimplifyUntil(_)(Arrow.unapply)._1) match {
case Some(Pi(x,tpA1,tpB1)) if !tpB1.freeVars.contains(x) =>
solver.check(Subtyping(stack, iv, tpA1))
solver.check(Typing(stack, iv, tpB1))
(tC, iv)
case _ =>
return (None,None)
}
case _ =>
return (None, None)
}
if (!covered) {
val proptp = solver.inferType(truetm) match {
case Some(t) => t
case _ => return (None, None)
}
val (name, _) = Context.pickFresh((stack ++ solver.constantContext ++ solver.outerContext).context, LocalName("ls"))
solver.check(Typing(stack++name%tpA,Apply(p,OMV(name)),proptp))
}
(Some(Listtype(tpA)),Some(true))*/
}
}
\ No newline at end of file
source/Scrolls/BouncingScroll.mmt
+ 60
− 62
View file @ 19f9d797
......@@ -2,86 +2,84 @@ 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 ❚
//import rules scala://datatypes.LFX.mmt.kwarc.info ❚
import rules scala://rules.frameit.mmt.kwarc.info ❚
//fixmeta base:?Logic ❚
fixmeta ?FrameworldMeta ❚
theory BouncingScrollMeta : ?FrameworldMeta =
if_then_elsex : {A : 𝒰 100, P : bool, a : A, b : A}A ❘ # ifx 2 thenx 3 elsex 4 ❙
simplify_ifelse1: {A: 𝒰 100, a: A, b: A} ⊦ ifx true thenx a elsex b ≐ a ❘ role Simplify ❙
simplify_ifelse2: {A: 𝒰 100, a: A, b: A} ⊦ ifx false thenx a elsex b ≐ b ❘ role Simplify ❙
theory StepUntilWrap =
stepUntil : ℝ ⟶ (ℝ ⟶ ℝ) ⟶ (ℝ ⟶ bool) ⟶ List[ℝ] ❘ # stepUntil 1 2 3 ❙
rule rules?StepUntilRule (true) ❙
❚
fixmeta ?BouncingScrollMeta ❚
theory BouncingScroll =
meta ?MetaAnnotations?problemTheory ?BouncingScroll/Problem ❙
meta ?MetaAnnotations?solutionTheory ?BouncingScroll/Solution ❙
rule rules?FilterRule (true) ❙
include ?StepUntilWrap ❙
theory funcs =
//get_ht : ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ❘ =
[z,zv,g] times_real_lit (minus_real_lit (plus_real_lit zv (sqrt (plus_real_lit (times_real_lit zv zv) (minus_real_lit (times_real_lit (times_real_lit 2.0 g) z)))))) (inv_real_lit g) ❙
//new_ht : ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ❘ =
[zv,g,ht,bo] times_real_lit (times_real_lit (minus_real_lit 2.0) (times_real_lit (minus_real_lit bo) (plus_real_lit (times_real_lit g ht) zv))) (inv_real_lit g) ❙
//prep : ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ((ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ)) ❘ =
[x,y,z,xv,yv,zv,g,bo] ⟨⟨x, y, z⟩, ⟨xv, yv, zv⟩, ⟨g, get_ht z zv g, bo⟩⟩ ❙
//vals order: (x,y,z),(xv,yv,zv),(g,ht,bo) ❙
//edit : ((ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ)) ⟶ ((ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ)) ❘ =
[vals] ⟨⟨plus_real_lit (πl (πl vals)) (times_real_lit (πl (πr (πr (πr vals)))) (πl (πl (πr vals)))),
plus_real_lit (πl (πr (πl vals))) (times_real_lit (πl (πr (πr (πr vals)))) (πl (πr (πl (πr vals))))),
0.0⟩,
⟨times_real_lit (πr (πr (πr (πr vals)))) (πl (πl (πr vals))),
times_real_lit (πr (πr (πr (πr vals)))) (πl (πr (πl (πr vals)))),
times_real_lit (minus_real_lit (πr (πr (πr (πr vals))))) (plus_real_lit (times_real_lit (πl (πr (πr vals))) (πl (πr (πr (πr vals))))) (πr (πr (πl (πr vals)))))⟩,
⟨(πl (πr (πr vals))),
new_ht (πr (πr (πl (πr vals)))) (πl (πr (πr vals))) (πl (πr (πr (πr vals)))) (πr (πr (πr (πr vals)))),
(πr (πr (πr (πr vals))))⟩⟩ ❙
//fun0 : ((ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ)) ⟶ List[(ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ)] ❘ =
[vals] cons vals nil ❙
//fun1 : ((ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ)) ⟶ List[(ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ)] ❘ =
[vals] cons vals (fun0 (edit vals)) ❙
//fun2 : ((ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ)) ⟶ List[(ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ)] ❘ =
[vals] cons vals (fun1 (edit vals)) ❙
//fun3 : ((ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ)) ⟶ List[(ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ)] ❘ =
[vals] cons vals (fun2 (edit vals)) ❙
//red_ht_helper : ((ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ)) ⟶ ℝ ❘ =
[cele] πl (πr (πr (πr cele))) ❙
//red_ht : List[(ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ)] ⟶ List[ℝ] ❘ =
[clsele] clsele map ([xele] red_ht_helper xele) ❙
//red_vals_helper : ((ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ)) ⟶ ((ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ)) ❘ =
[cel] ⟨πl cel, πl (πr cel)⟩ ❙
//red_vals : List[(ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ)] ⟶ List[(ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ)] ❘ =
[cls] (cls map ([x1] red_vals_helper x1)) ++ nil ❙
//get_pos_fun: ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ (ℝ ⟶ (ℝ × ℝ × ℝ)) ❘ =
[x,y,z,xv,yv,zv,g] ([t] ⟨plus_real_lit x (times_real_lit xv t), plus_real_lit y (times_real_lit yv t), plus_real_lit (times_real_lit (times_real_lit 0.5 g) (times_real_lit t t)) (plus_real_lit z (times_real_lit zv t))⟩ ) ❙
//red_funcs : List[(ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ)] ⟶ List[ℝ ⟶ (ℝ × ℝ × ℝ)] ❘ =
[cls] (cls map ([x] get_pos_fun (πl (πl vals)) (πl (πr (πl vals))) (πr (πr (πl vals))) (πl (πl (πr vals))) (πl (πr (πl (πr vals)))) (πr (πr (πl (πr vals)))) (πl (πr (πr vals))))) ++ nil ❙
❚
// start position and velocity ❙
theory Problem =
include ?BouncingScroll/funcs ❙
xposition: ℝ ❘ meta ?MetaAnnotations?label "X" ❙
yposition: ℝ ❘ meta ?MetaAnnotations?label "Y" ❙
zposition: ℝ ❘ meta ?MetaAnnotations?label "Z" ❙
xvelocity: ℝ ❘ meta ?MetaAnnotations?label "XV" ❙
yvelocity: ℝ ❘ meta ?MetaAnnotations?label "YV" ❙
zvelocity: ℝ ❘ meta ?MetaAnnotations?label "ZV" ❙
g_base: ℝ ❘ meta ?MetaAnnotations?label "G" ❙
walls: List[(ℝ × ℝ) × (ℝ × ℝ)] ❘ meta ?MetaAnnotations?label "Walls" ❙
bounce: ℝ ❘ meta ?MetaAnnotations?label "BO" ❙
❚
// the output of the scroll ❙
theory Solution =
include ?BouncingScroll/Problem ❙
//fold_func : (((ℝ × ℝ) × (ℝ × ℝ)) × ℝ) ⟶ (ℝ × ℝ) ⟶ (ℝ × ℝ) ❘ =
[cur][acc] if (leq_real_lit (πl acc) (πr (πl (πl cur)))) then acc else ⟨πr (πl (πl cur)), πr cur⟩ ❙
//check_hit : ((ℝ × ℝ) × (ℝ × ℝ)) ⟶ bool ❘ =
[p] leq_real_lit 0.000001 (πr (πl p)) ❙
//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)⟩⟩ ❙
//get_mc_list : List[(ℝ × ℝ) × (ℝ × ℝ)] ⟶ List[(ℝ × ℝ) × (ℝ × ℝ)] ❘ = [wl] wl map ([x] get_mc x) ❙
//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)) ❙
//get_hit_time : ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ❘ =
[y, yv, g] times_real_lit (minus_real_lit (plus_real_lit yv (sqrt (plus_real_lit (times_real_lit yv yv) (minus_real_lit (times_real_lit (times_real_lit 2.0 g) y)))))) (inv_real_lit g) ❙
//mcws : List[(ℝ × ℝ) × (ℝ × ℝ)] ❘ = get_mc_list walls ❙
//list_ht_pos : List[((ℝ × ℝ) × (ℝ × ℝ)) × ℝ] ❘ = reduce_list_ht_pos mcws xposition yposition xvelocity yvelocity g_base ❙
//list_ht_neg : List[((ℝ × ℝ) × (ℝ × ℝ)) × ℝ] ❘ = reduce_list_ht_neg mcws xposition yposition xvelocity yvelocity g_base ❙
//hit_time : ℝ ❘ = get_hit_time yposition yvelocity g_base ❙
fold_func : (ℝ × ℝ) ⟶ ℝ ⟶ ℝ ❘ =
[cur][acc] plus_real_lit acc (πl cur) ❙
fold_func2 : (ℝ × ℝ) ⟶ (ℝ × ℝ) ⟶ (ℝ × ℝ) ❘ =
[cur][acc] ifx (leq_real_lit (πl acc) (πl cur)) thenx acc elsex cur ❙
l1 : List[(ℝ × ℝ)] ❘ = cons ⟨xposition, 1.0⟩ (cons ⟨yposition, 2.0⟩ (cons ⟨xvelocity, 3.0⟩ (cons ⟨yvelocity, 4.0⟩ (cons ⟨g_base, 5.0⟩ nil)))) ❙
l2 : List[(ℝ × ℝ)] ❘ = cons ⟨xposition, 1.0⟩ (cons ⟨yposition, 2.0⟩ (cons ⟨xvelocity, 3.0⟩ (cons ⟨yvelocity, 4.0⟩ (cons ⟨g_base, 5.0⟩ nil)))) ❙
l3 : List[(ℝ × ℝ)] ❘ = l1 ++ l2 ❙
mh : ℝ ❘ = l3 fold 0.0 fold_func ❙
//mh2 : (ℝ × ℝ) ❘ = l3 fold ⟨99999.9, -1.0⟩ fold_func2 ❙
mh3 : ℝ ❘ = (cons 4.0 (cons 5.0 nil)) fold 9.0 ([cur][acc] ifx (leq_real_lit acc cur) thenx acc elsex cur) ❙
mh4 : ℝ ❘ = (cons 4.0 (cons 5.0 nil)) fold 0.0 ([cur][acc] plus_real_lit acc cur) ❙
//full_list: List[(ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ)] ❘ =
fun3 (prep xposition yposition zposition xvelocity yvelocity zvelocity g_base bounce) ❙
//ht_list: List[ℝ] ❘ = red_ht full_list ❙
//val_list: List[(ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ)] ❘ = red_vals full_list ❙
test_func : ℝ ⟶ ℝ ❘ =
[x] plus_real_lit x 1.0 ❙
test_bool : ℝ ⟶ bool ❘ =
[x] leq_real_lit 10.0 x ❙
out_list: List[ℝ] ❘ = stepUntil 0.0 test_func test_bool ❙
meta ?MetaAnnotations?label "BouncingScroll" ❙
meta ?MetaAnnotations?description s"Bouncing " ❙
❚
......
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