1. 1
2. 2
3. 3
4. 4
5. 5
6. 6
7. 7
8. 8
9. 9
10. 10
11. 11
12. 12
13. 13
14. 14
15. 15
16. 16
17. 17
18. 18
19. 19
20. 20
21. 21
22. 22
23. 23
24. 24
25. 25
26. 26
27. 27
28. 28
29. 29
30. 30
31. 31
32. 32
33. 33
34. 34
35. 35
36. 36
37. 37
38. 38
39. 39
40. 40
41. 41
42. 42
43. 43
44. 44
45. 45
46. 46
47. 47
48. 48
49. 49
50. 50
51. 51
52. 52
53. 53
54. 54
55. 55
56. 56
57. 57
58. 58
59. 59
60. 60
61. 61
62. 62
63. 63
64. 64
65. 65
66. 66
67. 67
68. 68
69. 69
70. 70
71. 71
72. 72
73. 73
74. 74
75. 75
76. 76
77. 77
78. 78
79. 79
80. 80
81. 81
82. 82
83. 83
84. 84

import Lean.Data.Json
import Raylean

open Raylean Types

def screenWidth := 800
def screenHeight := 450

private def initialBallPosition : Vector2 := { x := screenWidth.toFloat / 2, y := screenHeight.toFloat / 2 }

inductive Move where
  | up
  | down
  | left
  | right
  | stay

def updateBallPosition (d : Move) (p : Vector2) : Vector2 := match d with
  | Move.right => { p with x := p.x + 2.0 }
  | Move.left => { p with x := p.x - 2.0 }
  | Move.up => { p with y := p.y - 2.0 }
  | Move.down => { p with y := p.y + 2.0 }
  | Move.stay => p

def getMove : IO Move := do
  if (← isKeyDown Key.right) then return Move.right
     else if (← isKeyDown Key.left) then return Move.left
     else if (← isKeyDown Key.up) then return Move.up
     else if (← isKeyDown Key.down) then return Move.down
     else return Move.stay

def doRender : IO Unit := do
  let mut ballPosition := initialBallPosition
  while not (← windowShouldClose) do
    let d ← getMove
    ballPosition := updateBallPosition d ballPosition
    renderFrame do
      drawFPS (screenWidth - 100) 10
      clearBackground Color.white
      drawText "Move the ball with arrow keys" 10 10 20 Color.blue
      drawCircleV ballPosition 50 Color.red
  closeWindow


structure Vehicle where
  pos : Nat × Nat
  dest : Nat × Nat


inductive Road
  | none
  | low
  | high
deriving Lean.ToJson, Lean.FromJson

structure Point where
  roads : Vector Road 24
  occupant : Option Nat

def Grid h w := Vector (Vector Point w) h

def Tick (g : Grid h w) : Grid h w := Id.run do
  return g


structure State where
  datetime : Std.Time.PlainDateTime
  height : Nat
  width : Nat
  grid : Grid height width
-- deriving Lean.ToJson, Lean.FromJson


def myroad : Road := .low

def serialized := Lean.toJson myroad |>.compress

def blah : Except String Road := Lean.Json.parse serialized >>= Lean.fromJson?


def main : IO Unit := do
  initWindow 1280 720 "LeanTTD"
  setTargetFPS 60
  doRender