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
85. 85
86. 86
87. 87
88. 88
89. 89
90. 90
91. 91
92. 92
93. 93
94. 94
95. 95
96. 96
97. 97
98. 98
99. 99
100. 100
101. 101
102. 102
103. 103
104. 104
105. 105

import Lean.Data.Json
import Raylean

open Raylean Types

def fps := 60
def screenWidth := 960
def screenHeight := 640

structure Nat3 where
  x : Nat
  y : Nat
  z : Nat

def initialBallPosition : Vector3 := ⟨0, 0, 0⟩

structure Move where
  up : Bool
  down : Bool
  left : Bool
  right : Bool

def updateBallPosition (d : Move) (p : Vector3) := Id.run do
  let mut p := p
  if d.up then
    p := { p with z := p.z - 0.1 }
  if d.down then
    p := { p with z := p.z + 0.1 }
  if d.left then
    p := { p with x := p.x - 0.1 }
  if d.right then
    p := { p with x := p.x + 0.1 }
  return p

def getMove : IO Move := do
  return {
    up := ← isKeyDown Key.up,
    down := ← isKeyDown Key.down,
    left := ← isKeyDown Key.left,
    right := ← isKeyDown Key.right
  }


structure Vehicle where
  pos : Nat3
  dest : Nat3


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
  -- This constant is FLAG_WINDOW_HIGHDPI || FLAG_WINDOW_RESIZABLE
  -- https://github.com/raysan5/raylib/blob/aaacda6e147031f2af0cfb6c1fd7e64d761ddb1f/src/raylib.h#L567
  setConfigFlags 0x00002004
  initWindow screenWidth screenHeight "LeanTTD"
  setTargetFPS fps
  let mut camera : Camera3D := {
    position := ⟨10, 10, 10⟩
    target := ⟨0, 0, 0⟩
    up := ⟨0, 1, 0⟩
    fovy := 45
    projection := .perspective
  }
  let mut ballPosition := initialBallPosition
  while not (← windowShouldClose) do
    camera ← updateCamera camera .thridPerson
    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
      renderWithCamera camera do
        drawCube ballPosition 2 2 2 Color.red
        drawCubeWires ballPosition 2 2 2 Color.blue
        drawGrid 100 1
  closeWindow