graphics2d: scale now modifies a translation within a picture

lean/Examples/Orbital.lean

@@ -46,7 +46,8 @@ def updateWithStatic (dt : Float) (staticBodies : Array (Mass × Position)) : Po
       -- p is the vector pointing from the oribiting body (po) to the static body (ps)
       let p := ps.sub po
       let pMag := p.length
-      let a := p |>.mul (m / pMag^3)
+      let softenedDistance := (pMag^2 + 0.25^2).sqrt
+      let a := p |>.mul (m / softenedDistance^3)
       vNew := vNew.add (a.mul dt)
     let pNew := po.add (vNew.mul dt)
     let oNew := o.push pNew
@@ -78,30 +79,27 @@ def update : System World Unit := do
   if (← isKeyDown Key.r) then cmap resetPlayer
   updateOrbitingBody (← getFrameTime)
 
-def translateScale (v : Vector2) : Vector2 :=
-  v.mul 100
-
-def bodyScale (mass : Mass) : Float := mass.val * 30
+def bodyScale (mass : Mass) : Float := mass.val * 0.3
 
 def staticBody (mass : Mass) (p : Position) : Picture :=
   .circle (bodyScale mass) |>
   .color .red |>
-  .translate (translateScale p.val)
+  .translate p.val
 
 def orbitingBody (p : Position) (c : Color) : Picture :=
-  .circle 10 |>
+  .circle 0.1 |>
   .color c |>
-  .translate (translateScale p.val)
+  .translate p.val
 
 def orbitPath (o : OrbitPath) : Picture :=
-  .line (o.val.map (translateScale ·)) |> .color .white
+  .line o.val |> .color .white
 
 def gamePicture : System World Picture := do
   let staticBodies ← collect (cx := Mass × Position × Not Velocity) <| fun (m, p, _) => staticBody m p |> some
   let playerOrbitingBody ← collect (cx := Player × Position × Velocity) <| fun (_, p, _) => orbitingBody p .green |> some
   let orbitingBodies ← collect (cx := Position × Velocity × Not Player) <| fun (p, _, _) => orbitingBody p .blue |> some
-  let orbitPaths ← collect <| fun o => orbitPath o |> some
-  return (.pictures (staticBodies ++ playerOrbitingBody ++ orbitingBodies ++ orbitPaths))
+  let orbitPaths ← collect <| some ∘ orbitPath
+  return (.scale ⟨100, 100⟩ <| .pictures (staticBodies ++ playerOrbitingBody ++ orbitingBodies ++ orbitPaths))
 
 def render : System World Unit :=
   renderFrame do

lean/Examples/Window.lean

@@ -26,9 +26,9 @@ def render : IO Unit := do
   let origin : Vector2 := ⟨0, 0⟩
   let rotation : Float := 0
   let rectangle := .rectangle 10 10 |> .color Color.red |> .scale ⟨20,20⟩
-  let circle := (.circle 100 |> .color Color.blue |> .scale ⟨0.5, 0.5⟩)
+  let circle := .circle 100 |> .color Color.blue |> .scale ⟨0.5, 0.5⟩
   let line :=  .line #[⟨100, 100⟩, ⟨200, 200⟩] |> .color Color.black
-  let p : Picture := line ++ (rectangle ++ circle |> .translate ⟨250, -50⟩ |> .scale ⟨1, 2⟩)
+  let p : Picture := line ++ (rectangle ++ circle |> .translate ⟨250, -40⟩ |> .scale ⟨1, 2⟩)
 
   while not (← windowShouldClose) do
     renderFrame do

lean/Raylean/Graphics2D/Render.lean

@@ -16,13 +16,11 @@ structure RenderContext where
   translate : Vector2
   center : Vector2
 
-/-- Translate a point in screen coordinates -/
-def RenderContext.screenTranslate (s : RenderContext) (v : Vector2) : Vector2 :=
-  ⟨v.x + s.translate.x, v.y - s.translate.y⟩
-
 /-- Convert a point in Picture coordinates to a point in screen coordinates -/
 def RenderContext.toScreen (s : RenderContext) (v : Vector2) : Vector2 :=
-  s.screenTranslate ⟨s.center.x + s.scale.x * v.x, s.center.y - s.scale.y * v.y⟩
+  let translateScreen := s.translate.dot ⟨1, -1⟩
+  let vScreen := v.dot ⟨1, -1⟩
+  vScreen |>.dot s.scale |>.add translateScreen |>.add s.center
 
 abbrev getContext : ReaderT RenderContext IO RenderContext := read
 
@@ -36,7 +34,7 @@ def renderLine (points : Array Vector2) : ReaderT RenderContext IO Unit := do
 
 def renderCircle (radius : Float) : ReaderT RenderContext IO Unit := do
   let ctx ← getContext
-  drawCircleV (ctx.screenTranslate ctx.center) (radius * (max 0 (max ctx.scale.x ctx.scale.y))) ctx.color
+  drawCircleV (ctx.toScreen ⟨0, 0⟩) (radius * (max 0 (max ctx.scale.x ctx.scale.y))) ctx.color
 
 def renderRectangle (width height : Float) : ReaderT RenderContext IO Unit := do
   let ctx ← getContext
@@ -52,7 +50,9 @@ partial def renderPicture' : (picture : Picture) → ReaderT RenderContext IO Un
   | .circle radius => renderCircle radius
   | .rectangle width height => renderRectangle width height
   | .color c p  => renderPicture' p |>.local (set color c)
-  | .translate v p => renderPicture' p |>.local (over translate (·.add v))
+  | .translate v p => renderPicture' p |>.local (fun s =>
+    over translate (·.add (v.dot s.scale)) s
+  )
   | .scale v p => renderPicture'  p |>.local (over scale (·.dot v))
   | .pictures ps => (fun _ => ()) <$> ps.mapM renderPicture'