diff --git a/lean/Examples/Orbital.lean b/lean/Examples/Orbital.lean index b0027aa..f4ec07f 100644 --- a/lean/Examples/Orbital.lean +++ b/lean/Examples/Orbital.lean @@ -79,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 diff --git a/lean/Examples/Window.lean b/lean/Examples/Window.lean index 2137239..44eadee 100644 --- a/lean/Examples/Window.lean +++ b/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 diff --git a/lean/Raylean/Graphics2D/Render.lean b/lean/Raylean/Graphics2D/Render.lean index 09336c8..57997f3 100644 --- a/lean/Raylean/Graphics2D/Render.lean +++ b/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'