-
1
-
2
-
3
-
4
-
5
-
6
-
7
-
8
-
9
-
10
-
11
-
12
-
13
-
14
-
15
-
16
-
17
-
18
-
19
-
20
-
21
-
22
-
23
-
24
-
25
-
26
-
27
-
28
-
29
-
30
-
31
-
32
-
33
-
34
-
35
-
36
-
37
-
38
-
39
-
40
-
41
-
42
-
43
-
44
-
45
-
46
-
47
-
48
-
49
-
50
-
51
-
52
-
53
-
54
-
55
-
56
-
57
-
58
-
59
-
60
-
61
-
62
-
63
-
64
-
65
-
66
-
67
-
68
-
69
-
70
-
71
-
72
-
73
-
74
-
75
-
76
-
77
-
78
-
79
-
80
-
81
-
82
-
83
-
84
-
85
-
86
-
87
-
88
-
89
-
90
-
91
-
92
-
93
-
94
-
95
-
96
-
97
-
98
-
99
-
100
-
101
-
102
-
103
-
104
-
105
-
106
-
107
-
108
-
109
-
110
-
111
-
112
-
113
-
114
-
115
-
116
-
117
-
118
-
119
-
120
-
121
-
122
-
123
-
124
-
125
-
126
-
127
-
128
-
129
-
130
-
131
-
132
-
133
-
134
-
135
-
136
-
137
-
138
-
139
-
140
-
141
-
142
-
143
-
144
-
145
-
146
-
147
-
148
-
149
-
150
-
151
-
152
-
153
-
154
-
155
-
156
-
157
-
158
-
159
-
160
-
161
-
162
-
163
-
164
-
165
-
166
-
167
-
168
-
169
-
170
-
171
-
172
-
173
-
174
-
175
-
176
-
177
-
178
-
179
-
180
-
181
-
182
-
183
-
184
-
185
-
186
-
187
-
188
-
189
-
190
-
191
-
192
-
193
-
194
-
195
-
196
-
197
-
198
-
199
-
200
-
201
-
202
-
203
-
204
-
205
-
206
-
207
-
208
-
209
-
210
-
211
-
212
-
213
-
214
-
215
-
216
-
217
-
218
-
219
-
220
-
221
-
222
-
223
-
224
-
225
-
226
-
227
-
228
-
229
-
230
-
231
-
232
-
233
-
234
-
235
-
236
-
237
-
238
-
239
-
240
-
241
-
242
-
243
-
244
-
245
-
246
-
247
-
248
-
249
-
250
-
251
-
252
-
253
-
254
-
255
-
256
-
257
-
258
-
259
-
260
-
261
-
262
-
263
-
264
-
265
-
266
-
267
-
268
-
269
-
270
-
271
-
272
-
273
-
274
-
275
-
276
-
277
-
278
-
279
-
280
-
281
-
282
-
283
-
284
-
285
-
286
-
287
-
288
-
289
-
290
-
291
-
292
-
293
-
294
-
295
-
296
-
297
-
298
-
299
-
300
-
301
-
302
-
303
-
304
-
305
-
306
-
307
-
308
-
309
-
310
-
311
-
312
-
313
-
314
-
315
-
316
-
317
-
318
-
319
-
320
-
321
-
322
-
323
-
324
-
325
-
326
-
327
-
328
-
329
-
330
-
331
-
332
-
333
-
334
-
335
-
336
-
337
-
338
-
339
-
340
-
341
-
342
-
343
-
344
-
345
-
346
-
347
-
348
-
349
-
350
-
351
-
352
-
353
-
354
-
355
-
356
-
357
-
358
-
359
-
360
-
361
-
362
-
363
-
364
-
365
-
366
-
367
-
368
-
369
-
370
-
371
-
372
-
373
-
374
-
375
-
376
-
377
-
378
-
379
-
380
-
381
-
382
-
383
-
384
-
385
-
386
-
387
-
388
-
389
-
390
-
391
-
392
-
393
-
394
-
395
-
396
-
397
-
398
-
399
-
400
-
401
-
402
-
403
-
404
-
405
-
406
-
407
-
408
-
409
-
410
-
411
-
412
-
413
-
414
-
415
-
416
-
417
-
418
-
419
-
420
-
421
-
422
-
423
-
424
-
425
-
426
-
427
-
428
-
429
-
430
-
431
-
432
-
433
-
434
-
435
-
436
-
437
-
438
-
439
-
440
-
441
-
442
-
443
-
444
-
445
-
446
-
447
-
448
-
449
-
450
-
451
-
452
-
453
-
454
-
455
-
456
-
457
-
458
-
459
-
460
-
461
-
462
-
463
-
464
-
465
-
466
-
467
-
468
-
469
-
470
-
471
-
472
-
473
-
474
-
475
-
476
-
477
-
478
-
479
-
480
-
481
-
482
-
483
-
484
-
485
-
486
-
487
-
488
-
489
-
490
-
491
-
492
-
493
-
494
-
495
-
496
-
497
-
498
-
499
-
500
-
501
-
502
-
503
-
504
-
505
-
506
-
507
-
508
-
509
-
510
-
511
-
512
-
513
-
514
-
515
-
516
-
517
-
518
-
519
-
520
-
521
-
522
-
523
-
524
-
525
-
526
-
527
-
528
-
529
-
530
-
531
-
532
-
533
-
534
-
535
-
536
-
537
-
538
-
539
-
540
-
541
-
542
-
543
-
544
-
545
-
546
-
547
-
548
-
549
-
550
-
551
-
552
-
553
-
554
-
555
-
556
-
557
-
558
-
559
-
560
-
561
-
562
-
563
-
564
-
565
-
566
-
567
-
568
-
569
-
570
-
571
-
572
-
573
-
574
-
575
-
576
-
577
-
578
-
579
-
580
-
581
-
582
-
583
-
584
-
585
-
586
-
587
-
588
-
589
-
590
-
591
-
592
-
593
-
594
-
595
-
596
-
597
-
598
-
599
-
600
-
601
-
602
-
603
-
604
-
605
-
606
-
607
-
608
-
609
-
610
-
611
-
612
-
613
-
614
-
615
-
616
-
617
-
618
-
619
-
620
-
621
-
622
-
623
-
624
-
625
-
626
-
627
-
628
-
629
-
630
-
631
-
632
-
633
-
634
-
635
-
636
-
637
-
638
-
639
-
640
-
641
-
642
-
643
-
644
-
645
-
646
-
647
-
648
-
649
-
650
-
651
-
652
-
653
-
654
-
655
-
656
-
657
-
658
-
659
-
660
-
661
-
662
-
663
-
664
-
665
-
666
-
667
-
668
-
669
-
670
-
671
-
672
-
673
-
674
-
675
-
676
-
677
-
678
-
679
-
680
-
681
-
682
-
683
-
684
-
685
-
686
-
687
-
688
-
689
-
690
-
691
-
692
-
693
-
694
-
695
-
696
-
697
-
698
-
699
-
700
-
701
-
702
-
703
-
704
-
705
-
706
-
707
-
708
-
709
-
710
-
711
-
712
-
713
-
714
-
715
-
716
-
717
-
718
-
719
-
720
-
721
-
722
-
723
-
724
-
725
-
726
-
727
-
728
-
729
-
730
-
731
-
732
-
733
-
734
-
735
-
736
-
737
-
738
-
739
-
740
-
741
-
742
-
743
-
744
-
745
-
746
-
747
-
748
-
749
-
750
-
751
-
752
-
753
-
754
-
755
-
756
-
757
-
758
-
759
-
760
-
761
-
762
-
763
-
764
-
765
-
766
-
767
-
768
-
769
-
770
-
771
-
772
-
773
-
774
-
775
-
776
-
777
-
778
-
779
-
780
-
781
-
782
-
783
-
784
-
785
-
786
-
787
-
788
-
789
-
790
-
791
-
792
-
793
-
794
-
795
-
796
-
797
-
798
-
799
-
800
-
801
-
802
-
803
-
804
-
805
-
806
-
807
-
808
-
809
-
810
-
811
-
812
-
813
-
814
-
815
-
816
-
817
-
818
-
819
-
820
-
821
-
822
-
823
-
824
-
825
-
826
-
827
-
828
-
829
-
830
-
831
-
832
-
833
-
834
-
835
-
836
-
837
-
838
-
839
-
840
-
841
-
842
-
843
-
844
-
845
-
846
-
847
-
848
-
849
-
850
-
851
-
852
-
853
-
854
-
855
-
856
-
857
-
858
-
859
-
860
-
861
-
862
-
863
-
864
-
865
-
866
-
867
-
868
-
869
-
870
-
871
-
872
-
873
-
874
-
875
-
876
-
877
-
878
-
879
-
880
-
881
-
882
-
883
-
884
-
885
-
886
-
887
-
888
-
889
-
890
-
891
-
892
-
893
-
894
-
895
-
896
-
897
-
898
-
899
-
900
-
901
-
902
-
903
-
904
-
905
-
906
-
907
-
908
-
909
-
910
-
911
-
912
-
913
-
914
-
915
-
916
-
917
-
918
-
919
-
920
-
921
-
922
-
923
-
924
-
925
-
926
-
927
-
928
-
929
-
930
-
931
-
932
-
933
-
934
-
935
-
936
-
937
-
938
-
939
-
940
-
941
-
942
-
943
-
944
-
945
-
946
-
947
-
948
-
949
-
950
-
951
-
952
-
953
-
954
-
955
-
956
-
957
-
958
-
959
-
960
-
961
-
962
-
963
-
964
-
965
-
966
-
967
-
968
-
969
-
970
-
971
-
972
-
973
-
974
-
975
-
976
-
977
-
978
-
979
-
980
-
981
-
982
-
983
-
984
-
985
-
986
-
987
-
988
-
989
-
990
-
991
-
992
-
993
-
994
-
995
-
996
-
997
-
998
-
999
-
1000
-
1001
-
1002
-
1003
-
1004
-
1005
-
1006
-
1007
-
1008
-
1009
-
1010
-
1011
-
1012
-
1013
-
1014
-
1015
-
1016
-
1017
-
1018
-
1019
-
1020
-
1021
-
1022
-
1023
-
1024
-
1025
-
1026
-
1027
-
1028
-
1029
-
1030
-
1031
-
1032
-
1033
-
1034
-
1035
-
1036
-
1037
-
1038
-
1039
-
1040
-
1041
-
1042
-
1043
-
1044
-
1045
-
1046
-
1047
-
1048
-
1049
-
1050
-
1051
-
1052
-
1053
-
1054
-
1055
-
1056
-
1057
-
1058
-
1059
-
1060
-
1061
-
1062
-
1063
-
1064
-
1065
-
1066
-
1067
-
1068
-
1069
-
1070
-
1071
-
1072
-
1073
-
1074
-
1075
-
1076
-
1077
-
1078
-
1079
-
1080
-
1081
-
1082
-
1083
-
1084
-
1085
-
1086
-
1087
-
1088
-
1089
-
1090
-
1091
-
1092
-
1093
-
1094
-
1095
-
1096
-
1097
-
1098
-
1099
-
1100
-
1101
-
1102
-
1103
-
1104
-
1105
-
1106
-
1107
-
1108
-
1109
-
1110
-
1111
-
1112
-
1113
-
1114
-
1115
-
1116
-
1117
-
1118
-
1119
-
1120
-
1121
-
1122
-
1123
-
1124
-
1125
-
1126
-
1127
-
1128
-
1129
-
1130
-
1131
-
1132
-
1133
-
1134
-
1135
-
1136
-
1137
-
1138
-
1139
-
1140
-
1141
-
1142
-
1143
-
1144
-
1145
-
1146
-
1147
-
1148
-
1149
-
1150
-
1151
-
1152
-
1153
-
1154
-
1155
-
1156
-
1157
-
1158
-
1159
-
1160
-
1161
-
1162
-
1163
-
1164
-
1165
-
1166
-
1167
-
1168
-
1169
-
1170
-
1171
-
1172
-
1173
-
1174
-
1175
-
1176
-
1177
-
1178
-
1179
-
1180
-
1181
-
1182
-
1183
-
1184
-
1185
-
1186
-
1187
-
1188
-
1189
-
1190
-
1191
-
1192
-
1193
-
1194
-
1195
-
1196
-
1197
-
1198
-
1199
-
1200
-
1201
-
1202
-
1203
-
1204
-
1205
-
1206
-
1207
-
1208
-
1209
-
1210
-
1211
-
1212
-
1213
-
1214
-
1215
-
1216
-
1217
-
1218
-
1219
-
1220
-
1221
-
1222
-
1223
-
1224
-
1225
-
1226
-
1227
-
1228
-
1229
-
1230
-
1231
-
1232
-
1233
-
1234
-
1235
-
1236
-
1237
-
1238
-
1239
-
1240
-
1241
-
1242
-
1243
-
1244
-
1245
-
1246
-
1247
-
1248
-
1249
-
1250
-
1251
-
1252
-
1253
-
1254
-
1255
-
1256
-
1257
-
1258
-
1259
-
1260
-
1261
-
1262
-
1263
-
1264
-
1265
-
1266
-
1267
-
1268
-
1269
-
1270
-
1271
-
1272
-
1273
-
1274
-
1275
-
1276
-
1277
-
1278
-
1279
-
1280
-
1281
-
1282
-
1283
-
1284
-
1285
-
1286
-
1287
-
1288
-
1289
-
1290
-
1291
-
1292
-
1293
-
1294
-
1295
-
1296
-
1297
-
1298
-
1299
-
1300
-
1301
-
1302
-
1303
-
1304
-
1305
-
1306
-
1307
-
1308
-
1309
-
1310
-
1311
-
1312
-
1313
-
1314
-
1315
-
1316
-
1317
-
1318
-
1319
-
1320
-
1321
-
1322
-
1323
-
1324
-
1325
-
1326
-
1327
-
1328
-
1329
-
1330
-
1331
-
1332
-
1333
-
1334
-
1335
-
1336
-
1337
-
1338
-
1339
-
1340
-
1341
-
1342
-
1343
-
1344
-
1345
-
1346
-
1347
-
1348
-
1349
-
1350
-
1351
-
1352
-
1353
-
1354
-
1355
-
1356
-
1357
-
1358
-
1359
-
1360
-
1361
-
1362
-
1363
-
1364
-
1365
-
1366
-
1367
-
1368
-
1369
-
1370
-
1371
-
1372
-
1373
-
1374
-
1375
-
1376
-
1377
-
1378
-
1379
-
1380
-
1381
-
1382
-
1383
-
1384
-
1385
-
1386
-
1387
-
1388
-
1389
-
1390
-
1391
-
1392
-
1393
-
1394
-
1395
-
1396
-
1397
-
1398
-
1399
-
1400
-
1401
-
1402
-
1403
-
1404
-
1405
-
1406
-
1407
-
1408
-
1409
-
1410
-
1411
-
1412
-
1413
-
1414
-
1415
-
1416
-
1417
-
1418
-
1419
-
1420
-
1421
-
1422
-
1423
-
1424
-
1425
-
1426
-
1427
-
1428
-
1429
-
1430
-
1431
-
1432
-
1433
-
1434
-
1435
-
1436
-
1437
-
1438
-
1439
-
1440
-
1441
-
1442
-
1443
-
1444
-
1445
-
1446
-
1447
-
1448
-
1449
-
1450
-
1451
-
1452
-
1453
-
1454
-
1455
-
1456
-
1457
-
1458
-
1459
-
1460
-
1461
-
1462
-
1463
-
1464
-
1465
-
1466
-
1467
-
1468
-
1469
-
1470
-
1471
-
1472
-
1473
-
1474
-
1475
-
1476
-
1477
-
1478
-
1479
-
1480
-
1481
-
1482
-
1483
-
1484
-
1485
-
1486
-
1487
-
1488
-
1489
-
1490
-
1491
-
1492
-
1493
-
1494
-
1495
-
1496
-
1497
-
1498
-
1499
-
1500
-
1501
-
1502
-
1503
-
1504
-
1505
-
1506
-
1507
-
1508
-
1509
-
1510
-
1511
-
1512
-
1513
-
1514
-
1515
-
1516
-
1517
-
1518
-
1519
-
1520
-
1521
-
1522
-
1523
-
1524
-
1525
-
1526
-
1527
-
1528
-
1529
-
1530
-
1531
-
1532
-
1533
-
1534
-
1535
-
1536
-
1537
-
1538
-
1539
-
1540
import Lean.Data.Json
import Raylean
-- See https://github.com/funexists/raylean/ PRs #61, #62, #63 for the stuff that I upstreamed to Raylean
open Raylean Types
-- Random stuff that should be in the Lean standard library but isn't?
def Float.pi := 4 * Float.atan 1
def Float.hypot (x y : Float) := Float.sqrt <| x ^ 2 + y ^ 2
def Vector.modify (V : Vector α n) (i : Nat) (f : α → α) : Vector α n := by
have : (V.toArray.modify i f).size = n := by grind
exact this ▸ (V.toArray.modify i f |>.toVector)
/-
## Basic utilities
-/
/-- Scale factor for grid to Raylib coordinates
The purpose of this is ~~to give me headaches~~ because the Raylib third-person camera has a fixed speed -/
def scaleN := 10
def scale := scaleN.toFloat
def fps := 60
-- Each cell of the grid corresponds to 5m, so peeps move at 15m/s (≈33 mph)
def ticksPerSecond := 3
/-- Keyboard sensitivity -/
def sensitivity := 5
/-- A point in the 3D grid -/
structure Nat3 where
x : Nat
y : Nat
z : Nat
deriving Inhabited, BEq, Hashable, Lean.ToJson, Lean.FromJson
-- Helpful for debugging
instance : ToString Nat3 := ⟨fun a ↦ s!"({a.x}, {a.y}, {a.z})"⟩
instance : Add Nat3 where
add a b := ⟨a.x + b.x, a.y + b.y, a.z + b.z⟩
instance : Sub Nat3 where
sub a b := ⟨a.x - b.x, a.y - b.y, a.z - b.z⟩
instance : HMul Nat Nat3 Nat3 where
hMul c a := ⟨a.x * c, a.y * c, a.z * c⟩
instance : HMul Nat3 Nat Nat3 where
hMul a c := ⟨a.x * c, a.y * c, a.z * c⟩
instance : HDiv Nat3 Nat Nat3 where
hDiv a c := ⟨a.x / c, a.y / c, a.z / c⟩
def Nat3.swizzle (a : Nat3) : Nat3 := ⟨a.z, a.y, a.x⟩
/-
## MonotoniCity types
-/
inductive BuildingVariant
| house
| apartment
| office
| park
| farm
| groceryStore
| mine
| industrialPlant
| factory
| shop
| bank
deriving Inhabited, BEq, DecidableEq, Lean.ToJson, Lean.FromJson
instance : ToString BuildingVariant where
toString
| .house => "house"
| .apartment => "apartment"
| .office => "office"
| .park => "park"
| .farm => "farm"
| .groceryStore => "grocery store"
| .mine => "mine"
| .industrialPlant => "industrial plant"
| .factory => "factory"
| .shop => "shop"
| .bank => "bank"
/-- For the console -/
def BuildingVariant.ofString? : String → Option BuildingVariant
| "h" => some .house
| "a" => some .apartment
| "o" => some .office
| "p" => some .park
| "r" => some .farm
| "g" => some .groceryStore
| "m" => some .mine
| "i" => some .industrialPlant
| "f" => some .factory
| "s" => some .shop
| "b" => some .bank
| _ => none
/-- OpenTTD-style industry chains -/
def BuildingVariant.deliverTo : BuildingVariant → Option BuildingVariant
| .farm => some .groceryStore
| .mine => some .industrialPlant
| .industrialPlant => some .factory
| .factory => some .shop
| .bank => some .bank
| _ => none
instance [BEq α] [Hashable α] [Lean.ToJson α] : Lean.ToJson (Std.HashSet α) where
toJson := List.toJson ∘ Std.HashSet.toList
instance [BEq α] [Hashable α] [Lean.FromJson α] : Lean.FromJson (Std.HashSet α) where
fromJson? j := .ofList <$> List.fromJson? j
instance [BEq α] [Hashable α] [Lean.ToJson α] [Lean.ToJson β] : Lean.ToJson (Std.HashMap α β) where
toJson := List.toJson ∘ Std.HashMap.toList
instance [BEq α] [Hashable α] [Lean.FromJson α] [Lean.FromJson β] : Lean.FromJson (Std.HashMap α β) where
fromJson? j := .ofList <$> List.fromJson? j
structure Building where
variant : BuildingVariant
pos : Nat3
size : Nat3
entrance : Nat3
exit : Nat3
spots : Nat
production : Nat
dist : Std.HashMap Nat3 Nat
isDeleted : Bool
deriving Inhabited, Lean.ToJson, Lean.FromJson
namespace Building
def capacity (size : Nat3) : BuildingVariant → Nat
| .house => 2
| .office => size.x * size.y * size.z
| .apartment => size.x * size.y * size.z / 2
| .groceryStore | .shop => size.x * size.y * size.z / 4
| .bank => size.x * size.y * size.z / 8
| .factory => size.x * size.y * size.z / 16
| .industrialPlant => size.x * size.y * size.z / 32
| .mine | .park | .farm => size.x * size.z / 64
def isResidential (b : Building) :=
match b.variant with
| .house | .apartment => true
| _ => false
/-- These buildings are at the start of industry chains -/
def isProducer (b : Building) :=
match b.variant with
| .farm | .mine | .bank => true
| _ => false
/-- This is the multiplier for both production and monetary payout -/
def payout (b : Building) :=
match b.variant with
| .groceryStore => 3
| .industrialPlant => 1
| .factory => 2
| .shop => 3
| .bank => 1
| _ => 0
def color (b : Building) :=
match b.variant with
| .house => Color.Raylean.red
| .apartment => Color.Raylean.orange
| .office => Color.Raylean.blue
| .park => Color.Raylean.green
| .farm => Color.Raylean.lime
| .groceryStore => Color.Raylean.purple
| .mine => Color.Raylean.brown
| .industrialPlant => Color.Raylean.darkgray
| .factory => Color.Raylean.beige
| .shop => Color.Raylean.pink
| .bank => Color.Raylean.gold
def cost (b : Building) :=
-- Make taller buildings slightly more expensive
100 * b.size.x * b.size.y * (b.size.y.log2 + 1) * b.size.z *
match b.variant with
-- Factory and industrial plant both have a min height of 4 so we don't need a large scale factor here
| .house | .park | .farm => 1
| .apartment | .office | .factory => 2
| .groceryStore | .shop | .industrialPlant => 5
| .mine => 10
| .bank => 500
/-- This is used in some random places but NOT when placing buildings -/
def checkCollide (pos size pos' size' : Nat3) :=
-- 1D collision
let f (a b c d : Nat) := !(b ≤ c || d ≤ a)
-- Do it for all 3 dimensions
(f pos.x (pos.x + size.x) pos'.x (pos'.x + size'.x) && f pos.y (pos.y + size.y) pos'.y (pos'.y + size'.y) && f pos.z (pos.z + size.z) pos'.z (pos'.z + size'.z))
#guard checkCollide ⟨10, 10, 10⟩ ⟨5, 5, 5⟩ ⟨12, 8, 14⟩ ⟨5, 5, 5⟩
-- Being flush against is not a collision (but you can't place buildings flush)
#guard !checkCollide ⟨10, 10, 10⟩ ⟨5, 5, 5⟩ ⟨15, 10, 10⟩ ⟨5, 5, 5⟩
#guard !checkCollide ⟨10, 10, 10⟩ ⟨5, 5, 5⟩ ⟨0, 8, 14⟩ ⟨5, 5, 5⟩
end Building
structure Peep where
home : Nat
work : Nat
pos : Nat3
dest : Nat
dir : Option Nat
brokenDown : Bool
isDelivery : Bool
deriving BEq, Lean.ToJson, Lean.FromJson
/-- Grid helper functions -/
def dx (i : Nat) := Int.ofNat (i / 9 % 3) - 1
def dy (i : Nat) := Int.ofNat (i % 3) - 1
def dz (i : Nat) := Int.ofNat (i / 3 % 3) - 1
def di (x y z : Int) := 9 * x + y + 3 * z + 13 |>.toNat
/-- These functions are inverses kinda -/
example : di (dx i) (dy i) (dz i) = i % 27 := by
simp [di, dx, dy, dz]
grind
-- `i` and `26 - i` should be in opposite directions
#guard (List.range 27 |>.map fun i ↦ dx i == -(dx (26 - i)) && dy i == -(dy (26 - i)) && dz i == -(dz (26 - i))).and
def Nat3.appdk (p : Nat3) (i k : Nat) : Nat3 :=
⟨p.x + k * dx i |>.toNat, p.y + k * dy i |>.toNat, p.z + k * dz i |>.toNat⟩
def Nat3.appd (p : Nat3) (i : Nat) : Nat3 :=
appdk p i 1
def Nat3.appd2 (p : Nat3) : Fin 4 → Nat3
| 0 => ⟨p.x + 1, p.y, p.z⟩
| 1 => ⟨p.x, p.y, p.z + 1⟩
| 2 => ⟨p.x - 1, p.y, p.z⟩
| 3 => ⟨p.x, p.y, p.z - 1⟩
structure TrafficLight where
greenLen : Nat
redLen : Nat
shift : Nat
deriving BEq, Lean.ToJson, Lean.FromJson
instance : ToString TrafficLight where
toString t := s!"Green: {t.greenLen}, Red: {t.redLen}, Shift: {t.shift}"
def TrafficLight.isGreen (t : TrafficLight) (ticks : Nat) : Bool :=
(ticks / ticksPerSecond + t.redLen + t.greenLen - t.shift) % (t.redLen + t.greenLen) < t.greenLen
inductive Road
| none
| low
| high
deriving Inhabited, BEq, Lean.ToJson, Lean.FromJson
def Road.cost (r : Road) (y y' : Nat) :=
(if y == 0 && y' == 0 then 1 else 10 * (y ^ 2 + y' ^ 2)) *
match r with
| none => 0
| low => 10
| high => 50
instance [Lean.ToJson α] : Lean.ToJson (Vector α n) where
toJson := Array.toJson ∘ Vector.toArray
instance [Lean.FromJson α] : Lean.FromJson (Vector α n) where
fromJson? j := do
let A ← Array.fromJson? j
if h : A.size = n then
return h ▸ A.toVector
else
throw s!"expected size {n}, got {A.size}"
inductive Control
| none
| yield
| trafficLight (t : TrafficLight)
deriving Inhabited, BEq, Lean.ToJson, Lean.FromJson
instance : ToString Control where
toString
| .none => ""
| .yield => "Yield"
| .trafficLight t => toString t
def Control.isRed (ticks : Nat)
| trafficLight t => !t.isGreen ticks
| _ => false
-- Bitmasks!
structure Point where
name : String
control : Control
/-- These point in the direction of the edge -/
e : UInt64
/-- These point in the OPPOSITE direction as the edge -/
ein : UInt64
deriving Inhabited, Lean.ToJson, Lean.FromJson
def getRoad (e : UInt64) (i : Nat) : Road :=
if e >>> i.toUInt64 &&& 1 == 0 then
.none
else if e >>> (i.toUInt64 + 27) &&& 1 == 0 then
.low
else
.high
def setRoad (e : UInt64) (i : Nat) : Road → UInt64
| .none => e
| .low => (e &&& ~~~(1 <<< (i.toUInt64 + 27))) ||| (1 <<< i.toUInt64)
| .high => e ||| (1 <<< i.toUInt64) ||| (1 <<< (i.toUInt64 + 27))
def unset (e : UInt64) (i : Nat) :=
e &&& ~~~(1 <<< (i.toUInt64 + 27) ||| (1 <<< i.toUInt64))
/-- Crazy bit magic -/
def iter (e : UInt64) : Array (Nat × Road) := Id.run do
-- Mask out higher bits
let mut e' := e &&& (1 <<< (27 : UInt64) - 1)
let mut ret := #[]
while e' != 0 do
let i := e'.ctz
ret := ret.push (i.toNat, if e >>> (i + 27) &&& 1 == 0 then .low else .high)
e' := e' &&& ~~~(1 <<< i)
return ret
instance : Lean.ToJson StdGen where
toJson x := Lean.toJson (x.1, x.2)
instance : Lean.FromJson StdGen where
fromJson? j := do
let (x : Nat × Nat) ← Lean.fromJson? j
return ⟨x.1, x.2⟩
/-- The entire game state, which is persisted to save files -/
structure State where
rng : StdGen
ticks : Nat
speed : Nat
money : Nat
origin : Nat3
grid : Std.HashMap Nat3 Point
buildings : Array Building
occupiedByBuilding : Std.HashSet Nat3
portals : Std.HashSet Nat3
unfull : Vector (Array Nat) 2
buildingVariants : Vector (Array Nat) ((BuildingVariant.ofNat 100).ctorIdx + 1)
peeps : Array Peep
occupied : Std.HashSet Nat3
deriving Lean.ToJson, Lean.FromJson
/-
## doTick and friends
-/
/-- Lift vanilla `StateM` into `StateT` (state monad wrapped around something else) -/
instance [Monad m] : MonadLift (StateM σ) (StateT σ m) where
monadLift x := modifyGet <| StateT.run x
/-- Lift exception throwing into the IO monad -/
instance : MonadLift (Except String) IO where
monadLift x := .ofExcept x
/-- For lifting `StateT State (Except String)` to `StateT State IO` -/
instance [MonadLift m n] [Monad n] : MonadLift (StateT σ m) (StateT σ n) where
monadLift x s := monadLift (x s)
/-- Macro for easily updating a specific field of the state -/
macro "modifyf" field:ident fn:term : term =>
let lval := ⟨.node .none `Lean.Parser.Term.structInstLVal #[field.raw, Lean.mkNullNode]⟩
`(modify fun s ↦ { s with $lval := $fn s.$field })
/-- Macro for easily setting a specific field of the state -/
macro "setf" field:ident val:term : term =>
let lval := ⟨.node .none `Lean.Parser.Term.structInstLVal #[field.raw, Lean.mkNullNode]⟩
`(modify fun s ↦ { s with $lval := $val })
-- For some reason `notation "setf" field val => modifyf field (fun _ ↦ val)` doesn't work
/-- Generate array of street names at compile time -/
elab "get_street_names" : term => do
return Lean.toExpr <|
(← IO.FS.readFile "street-names.txt").split '\n' |>.toStringArray
def street_names := get_street_names
theorem queue_dequeue_isSome_if_not_isEmpty {q : Std.Queue α} (h : ¬q.isEmpty) : q.dequeue?.isSome := by
rw [Std.Queue.dequeue?]
by_cases q.dList = []
· have : q.eList ≠ [] := by grind [Std.Queue.isEmpty]
have : q.eList.reverse ≠ [] := by simp [this]
grind
· grind
/-- Precompute distances to `start` using BFS -/
def mkDist (g : Std.HashMap Nat3 Point) (start : Nat3) := Id.run do
let mut q := Std.Queue.enqueue start .empty
let mut dist := Std.HashMap.ofList [(start, 0)]
while hq : ¬q.isEmpty do
let uq := q.dequeue?.get (queue_dequeue_isSome_if_not_isEmpty hq)
let u := uq.1
q := uq.2
let d := dist[u]!
if hg : g.contains u then
for (i, road) in iter g[u].ein do
let v := u.appd i
if hg : g.contains v then
match road with
| .low =>
if !dist.contains v then
dist := dist.insert v (d + 1)
q := q.enqueue v
| .high =>
if !dist.contains v then
dist := dist.insert v (d + 1)
q := q.enqueue v
-- Try traveling another unit in direction `i`
let v' := v.appd i
if hg : g.contains v' then
match getRoad g[v'].e (26 - i) with
| .high =>
if !dist.contains v' then
dist := dist.insert v' (d + 1)
q := q.enqueue v'
| _ =>
pure ()
| .none =>
pure ()
return dist
/-- Precompute all distances -/
def mkDists : StateM State Unit := do
let g := (← get).grid
modifyf buildings (·.map fun b ↦
if !b.isDeleted then { b with dist := mkDist g b.entrance } else b)
/-- Generate a random nat in [0, n) (with a slight bias towards smaller numbers)
`randNat` is more sophisticated but doesn't bundle a bounds proof, so let's just use modulo for simplicity
-/
def rand (n : Nat) (hn : 0 < n := by grind) : StateM State (Fin n) := do
let (ret, rng) := stdNext (← get).rng
setf rng rng
return ⟨ret % n, Nat.mod_lt ret hn⟩
/-- Shuffle an array using the Fisher-Yates algorithm -/
def Array.shuffle (A : Array α) : StateM State (Array α) := do
let mut A' := A.toVector
for hi : i in [1:A'.size] do
let j ← rand (i + 1)
A' := A'.swap i j
return A'.toArray
-- These are all per-tick, not per-second
abbrev productionProb := 200
abbrev homeToWorkProb := 5000
abbrev homeToGroceryStoreProb := 10000
abbrev homeToShopProb := 10000
abbrev homeToBankProb := 50000
abbrev deliveryProb := 200
abbrev workToHomeProb := 10000
abbrev consumerToHomeProb := 5000
abbrev breakdownProb := 50000
abbrev repairProb := 25
/-- Run one iteration of the game
This is a huge incomprehensible mess I know -/
def doTick : StateM State Unit := do
-- Produce resources
let newProd := if (← rand productionProb) == 0 then 1 else 0
modifyf buildings (·.map fun b ↦
if b.isProducer then
{ b with production := min (b.production + newProd) 20 }
else
b)
-- Now let's move the peeps!
let mut peeps := #[]
-- Occupied after this tick
let mut occupied : Std.HashSet Nat3 := .ofList []
-- Occupied after half this tick (all coordinates multiplied by 2)
-- This is to prevent peeps from crossing each other diagonally
let mut occupiedMid : Std.HashSet Nat3 := .ofList []
let origPeeps :=
let g := (← get).grid
(← (← get).peeps.shuffle).partition (fun p ↦
if h : g.contains p.pos then g[p.pos].control != .yield else true)
for p in origPeeps.1 ++ origPeeps.2 do
let u := p.pos
let bvs := (← get).buildingVariants
let g := (← get).grid
let ticks := (← get).ticks
if u == (← get).buildings[p.dest]!.entrance then
let doProb (p : Peep) (bv : BuildingVariant) (prob : Nat) (isDelivery : Bool) (hprob : 0 < prob := by grind) : StateM State Peep := do
if h : (← rand prob) == ⟨0, hprob⟩ && !bvs[bv.ctorIdx]!.isEmpty then
let idx ← rand bvs[bv.ctorIdx]!.size
if idx == p.dest || !(← get).buildings[bvs[bv.ctorIdx]![idx]]!.dist.contains (← get).buildings[p.dest]!.exit then
-- Unreachable or delivering to same building
return p
if isDelivery then
modifyf buildings (·.modify p.work fun b ↦ { b with production := b.production - 1 })
return { p with dest := bvs[bv.ctorIdx]![idx], isDelivery }
else
return p
if p.dir.isSome then
-- Newly arrived at building
let payout := (← get).buildings[p.dest]!.payout
modifyf money (· + (if p.isDelivery then 1000 * payout else 100))
if p.isDelivery then
modifyf buildings (·.modify p.dest fun b ↦ { b with production := min (b.production + payout) 100 })
let mut p' := { p with dir := none }
if p.dest == p.home then
-- At home, go to work or consumer buildings
if (← rand homeToWorkProb) == 0 then
p' := { p' with dest := p.work, isDelivery := false }
else
p' ← doProb p' .groceryStore homeToGroceryStoreProb false
p' ← doProb p' .shop homeToShopProb false
p' ← doProb p' .bank homeToBankProb false
else if p.dest == p.work then
-- At work, go home or do delivery
if (← rand workToHomeProb) == 0 then
p' := { p' with dest := p.home, isDelivery := false }
else if (← get).buildings[p.work]!.production > 0 then
match (← get).buildings[p.work]!.variant.deliverTo with
| some bv => p' ← doProb p' bv deliveryProb true
| none => pure ()
else if p.isDelivery then
-- Doing delivery, go back to work
p' := { p' with dest := p.work, isDelivery := false }
else
-- At consumer building (hopefully?), go home
if (← rand consumerToHomeProb) == 0 then
if 0 < (← get).buildings[p.dest]!.production then
-- Make some money if building has stuff
modifyf money (· + 5000)
modifyf buildings (·.modify p.dest fun b ↦ { b with production := b.production - 1 })
p' := { p' with dest := p.home, isDelivery := false }
-- Start the journey!
if p'.dest != p.dest then
p' := { p' with pos := (← get).buildings[p.dest]!.exit }
peeps := peeps.push p'
else if (if h : g.contains u then g[u].control.isRed ticks else false) then
-- Traffic light
occupied := occupied.insert u
peeps := peeps.push ({ p with dir := none })
else if p.brokenDown then
occupied := occupied.insert u
peeps := peeps.push ({ p with dir := none, brokenDown := (← rand repairProb) != 0 })
else
-- Find unoccupied move with lowest dist
let dist := (← get).buildings[p.dest]!.dist
let mut neighbors := #[]
if hs : g.contains u then
for (i, road) in iter g[u].e do
let v := u.appd i
if hd : dist.contains v then
match road with
| .none =>
pure ()
| .low =>
neighbors := neighbors.push (dist[v], i)
| .high =>
neighbors := neighbors.push (dist[v], i)
if hv : g.contains v then
let v' := v.appd i
if hd : dist.contains v' then
match getRoad g[v].e i with
| .high =>
neighbors := neighbors.push (dist[v'], i + 27)
| _ =>
pure ()
neighbors := neighbors.qsort (fun a b ↦ a.1 < b.1 || (a.1 == b.1 && a.2 < b.2))
let mut p' := p
for (d, i) in neighbors do
if d > neighbors[0]!.1 + 100 || d > 5 * neighbors[0]!.1 then
-- Don't move if this makes us take a really long detour
-- TODO: better heuristic since this one can cause really bad deadlocks
break
let v := u.appd i
if i < 27 then
if (← get).occupied.contains v || occupied.contains v || occupiedMid.contains (u + v) then
continue
occupied := occupied.insert v
occupiedMid := occupiedMid.insert (u + v)
p' := { p with pos := v, dir := some i }
else
let v':= u.appdk i 2
if (← get).occupied.contains v || occupied.contains v || occupiedMid.contains (u + v) || (← get).occupied.contains v' || occupied.contains v' || occupiedMid.contains (v + v') then
continue
occupied := occupied.insert v
occupiedMid := occupiedMid.insert (u + v)
occupied := occupied.insert v'
occupiedMid := occupiedMid.insert (v + v')
p' := { p with pos := v', dir := some i }
break
if p' == p then
occupied := occupied.insert u
p' := { p with pos := u, dir := none }
peeps := peeps.push { p' with brokenDown := (← rand breakdownProb) == 0 }
setf peeps peeps
setf occupied occupied
modifyf ticks (· + 1)
/-
## Commands
-/
/-- Load game state from file -/
def loadState (path : String) : IO State := do
let serialized ← IO.FS.readFile path
let json ← .ofExcept <| Lean.Json.parse serialized
.ofExcept <| Lean.fromJson? json
/-- Save game state to file -/
def saveState (path : String) (s : State) := do
IO.FS.writeFile path <| Lean.toJson s |>.compress
def endPointsToCorners (start stop : Nat3) : Nat3 × Nat3 :=
(⟨min start.x stop.x, min start.y stop.y, min start.z stop.z⟩, ⟨max start.x stop.x, max start.y stop.y, max start.z stop.z⟩)
def shell (pos size : Nat3) : Array Nat3 := Id.run do
let mut ret := #[]
for x in [pos.x:pos.x + size.x + 1] do
for z in [pos.z:pos.z + size.z + 1] do
ret := ret.push ⟨x, pos.y, z⟩
ret := ret.push ⟨x, pos.y + size.y, z⟩
for x in [pos.x:pos.x + size.x + 1] do
for y in [pos.y + 1:pos.y + size.y] do
ret := ret.push ⟨x, y, pos.z⟩
ret := ret.push ⟨x, y, pos.z + size.z⟩
for y in [pos.y + 1:pos.y + size.y] do
for z in [pos.z + 1:pos.z + size.z] do
ret := ret.push ⟨pos.x, y, z⟩
ret := ret.push ⟨pos.x + size.x, y, z⟩
return ret
/-- Delete roads in a region (yeah this is surprisingly complicated) -/
def delete (start stop : Nat3) : StateM State Unit := do
let (start, stop) := endPointsToCorners start stop
-- Delete roads
-- Make sure ein immediately outside the deleted region is consistent
-- This does a bit of redundant work but oh well let's keep it simple
for p in shell start (stop - start) do
if (← get).grid.contains p then
for (i, _) in iter (← get).grid[p]!.e do
let p' := p.appd i
modifyf grid (·.modify p' fun pt ↦ { pt with ein := unset pt.ein (26 - i) })
for (i, _) in iter (← get).grid[p]!.ein do
let p' := p.appd i
modifyf grid (·.modify p' fun pt ↦ { pt with e := unset pt.e (26 - i) })
-- Delete the deleted region
for x in [start.x:stop.x + 1] do
for y in [start.y:stop.y + 1] do
for z in [start.z:stop.z + 1] do
modifyf grid (·.erase ⟨x, y, z⟩)
-- Delete buildings
for (b, idx) in (← get).buildings.zip (Array.range (← get).buildings.size) do
-- Only delete if overlapping center at ground floor
if !b.isDeleted && Building.checkCollide { b.pos + b.size / 2 with y := b.pos.y } ⟨1, 1, 1⟩ start { stop - start with y := 1 } then
for pos in shell b.pos b.size do
modifyf occupiedByBuilding (·.erase pos)
modifyf portals (·.erase b.entrance)
modifyf portals (·.erase b.exit)
for i in List.finRange 4 do
modifyf portals (·.erase <| b.entrance.appd2 i)
modifyf portals (·.erase <| b.exit.appd2 i)
modifyf buildings (·.set! idx { b with isDeleted := true })
let buildings := (← get).buildings
-- Note that we don't add back spots, this is because ~~I'm lazy~~ to penalize deleting buildings
modifyf peeps (·.filterMap fun p ↦
if !buildings[p.home]!.isDeleted && !buildings[p.work]!.isDeleted then
some (if buildings[p.dest]!.isDeleted then { p with dest := p.home } else p)
else
none)
modifyf buildingVariants (·.map (·.filter fun idx ↦ !buildings[idx]!.isDeleted))
modifyf unfull (fun uf ↦ #v[uf[0].filter fun idx ↦ !buildings[idx]!.isDeleted, uf[1].filter fun idx ↦ !buildings[idx]!.isDeleted])
/-- Spend some money! -/
def spend (cost : Nat) : StateT State (Except String) Unit := do
if cost > (← get).money then
throw s!"Need ${cost}, only have ${(← get).money}"
modifyf money (· - cost)
/-- Add a building to the state -/
def addBuilding (variant : BuildingVariant) (pos size entrance exit : Nat3) : StateT State (Except String) Unit := do
if entrance == exit then
throw "Building entrance cannot be in same position as exit"
let onSide (p : Nat3) :=
pos.x ≤ p.x && p.x ≤ pos.x + size.x && pos.z ≤ p.z && p.z ≤ pos.z + size.z && (p.x == pos.x || p.x == pos.x + size.x || p.z == pos.z || p.z == pos.z + size.z)
if !onSide entrance || !onSide exit then
throw "Building entrance or exit not on side of building"
let bIdx := (← get).buildings.size
let size' :=
if (variant == .factory || variant == .industrialPlant) && size.y < 4 then
{ size with y := 4 }
else if variant == .park || variant == .farm || variant == .mine then
{ size with y := 1 }
else
size
-- Check for collisions
for p in shell pos size' do
if (← get).grid.contains p then
throw "Building collides with existing road"
if (← get).occupiedByBuilding.contains p then
throw "Building collides with existing building"
if (← get).portals.contains p then
throw "Building collides with existing entrance or exit"
for i in List.finRange 4 do
if (← get).occupiedByBuilding.contains <| entrance.appd2 i then
throw "Entrance collides with existing building"
if (← get).occupiedByBuilding.contains <| exit.appd2 i then
throw "Exit collides with existing building"
-- Update the collision sets
for p in shell pos size' do
if p != entrance && p != exit then
modifyf occupiedByBuilding (·.insert p)
modifyf portals (·.insert entrance)
modifyf portals (·.insert exit)
for i in List.finRange 4 do
modifyf portals (·.insert <| entrance.appd2 i)
modifyf portals (·.insert <| exit.appd2 i)
let b : Building := {
variant
pos
size := size'
entrance
exit
spots := Building.capacity size variant
production := 0
dist := mkDist (← get).grid entrance
isDeleted := false
}
spend b.cost
-- Randomly iterate through empty spots in buildings of the opposite kind and create new peeps
-- TODO: Does this have bugs? (most likely yes)
let mut spots := b.spots
while spots > 0 do
let choices := ((← get).unfull[b.isResidential.toNat]'(by grind [Bool.toNat_lt]))
if h : !choices.isEmpty then
let choiceIdx ← rand choices.size
let idx := choices[choiceIdx]
if b.isResidential then
modifyf peeps (·.push {
home := (← get).buildings.size
work := idx
pos := b.entrance
dest := bIdx
dir := none
brokenDown := false
isDelivery := false
})
else
modifyf peeps (·.push {
home := idx
work := bIdx
pos := (← get).buildings[idx]!.entrance
dest := idx
dir := none
brokenDown := false
isDelivery := false
})
spots := spots - 1
modifyf buildings (·.modify idx (fun b ↦ { b with spots := b.spots - 1 }))
if (← get).buildings[idx]!.spots == 0 then
modifyf unfull (·.modify b.isResidential.toNat (·.eraseIdx! choiceIdx))
else
break
modifyf buildings (·.push { b with spots })
if spots > 0 then
modifyf unfull (·.modify (!b.isResidential).toNat (·.push bIdx))
modifyf buildingVariants (·.modify variant.ctorIdx (·.push bIdx))
def max3 (a b c : Nat) := max a (max b c)
def diff (a b : Nat) := if a < b then b - a else a - b
/-- Snap `a` to the nearest small `b` multiple -/
def snap (a : Int) (b : Nat) :=
if a ≤ -b / 2 then
-1
else if a ≤ b / 2 then
0
else 1
/-- Get direction and length between two endpoints -/
def endpointsToRoad (start stop : Nat3) :=
let length := max3 (diff start.x stop.x) (diff start.y stop.y) (diff start.z stop.z)
let dir := di (snap (Int.ofNat stop.x - start.x) length) (snap (Int.ofNat stop.y - start.y) length) (snap (Int.ofNat stop.z - start.z) length)
(length, dir)
-- Sanity check
#guard endpointsToRoad ⟨5, 5, 5⟩ ⟨1, 5, 2⟩ == (4, di (-1) 0 (-1))
/-- Add roads to the state
Note that this DOES NOT call `mkDists` so it's your responsibility to do that! -/
def addRoad (start stop : Nat3) (isHigh : Bool) : StateT State (Except String) Unit := do
let (length, dir) := endpointsToRoad start stop
if dir == di 0 0 0 || dir == di 0 1 0 || dir == di 0 (-1) 0 then
throw "Road cannot go straight up or down"
let road : Road := if isHigh then .high else .low
let originy := (← get).origin.y
spend <| length * road.cost (diff start.y originy) (diff stop.y originy)
-- TODO: Better heuristic here
let mut name := ""
let stop := start.appdk dir length
for u in [start, stop, { start with x := start.x + 1 }, { start with z := start.z + 1 }, { start with x := start.x - 1 }, { start with z := start.z - 1 }] do
if (← get).grid.contains u then
-- Yeah this is not ideal but Lean doesn't know the two `← get`s are the same
name := (← get).grid[u]!.name
if name == "" then
if isHigh then
name := s!"Highway {(← rand 998) + 1}"
else
have : 0 < street_names.size := by native_decide
name := s!"{street_names[← rand street_names.size]} Street"
for i in List.range (length + 1) do
let v := start.appdk dir i
if h : (← get).occupiedByBuilding.contains v then
throw "Road collides with existing building"
modifyf grid fun g ↦ Id.run do
let mut g := g
if h : !g.contains v then
g := g.insert v ⟨name, .none, 0, 0⟩
g.modify v fun p ↦ Id.run do
let mut p' := p
if i < length then
p' := { p' with e := setRoad p.e dir road }
if i > 0 then
p' := { p' with ein := setRoad p.ein (26 - dir) road }
return p'
def addMultiRoad (start stop : Nat3) (isHigh : Bool) : StateT State (Except String) Unit := do
if start.y != stop.y then
throw "Multilane road must remain at same level"
-- We can't overwrite `start` and `stop` here since we need to preserve the direction of the road
let y := start.y
let swizzled := diff start.x stop.x < diff start.z stop.z
let (start', stop') :=
if swizzled then
let (start', stop') := endPointsToCorners start stop
(start'.swizzle, stop'.swizzle)
else
endPointsToCorners start stop
let addRoad' p p' :=
(if swizzled then
if start.z < stop.z then addRoad p.swizzle p'.swizzle else addRoad p'.swizzle p.swizzle
else
if start.x < stop.x then addRoad p p' else addRoad p' p) isHigh
for i in [start'.z:stop'.z + 1] do
-- Straight lines
addRoad' ⟨start'.x, y, i⟩ ⟨stop'.x, y, i⟩
-- Diagonal segments
let d := stop'.z - start'.z
for i in [start'.x:stop'.x + d] do
if i < start'.x + d then
addRoad' ⟨start'.x, y, start'.z + i - start'.x⟩ ⟨i, y, start'.z⟩
addRoad' ⟨start'.x, y, stop'.z + start'.x - i⟩ ⟨i, y, stop'.z⟩
else if i > stop'.x then
addRoad' ⟨i - d, y, start'.z⟩ ⟨stop'.x, y, start'.z + stop'.x + d - i⟩
addRoad' ⟨i - d, y, stop'.z⟩ ⟨stop'.x, y, stop'.z + i - stop'.x - d⟩
else
addRoad' ⟨i - d, y, start'.z⟩ ⟨i, y, stop'.z⟩
addRoad' ⟨i - d, y, stop'.z⟩ ⟨i, y, start'.z⟩
def addYield (pos : Nat3) : StateT State (Except String) Unit := do
spend 10
if !(← get).grid.contains pos then
throw s!"Could not place yield at {pos}"
modifyf grid (·.modify pos fun p ↦ { p with control := .yield })
def addTrafficLight (pos : Nat3) (t : TrafficLight) : StateT State (Except String) Unit := do
spend 100
if !(← get).grid.contains pos then
throw s!"Could not place traffic light at {pos}"
modifyf grid (·.modify pos fun p ↦ { p with control := .trafficLight t })
def deleteControl (pos : Nat3) : StateT State (Except String) Unit := do
if !(← get).grid.contains pos then
throw s!"Could not delete control signal at {pos}"
modifyf grid (·.modify pos fun p ↦ { p with control := .none })
-- TODO: Highway interchanges
inductive IntersectionVariant
| _1x1
| _1x2
| _2x1
| _2x2
| roundabout
deriving DecidableEq
instance : ToString IntersectionVariant where
toString
| .roundabout => "roundabout"
| ._1x1 => "1x1"
| ._1x2 => "1x2"
| ._2x1 => "2x1"
| ._2x2 => "2x2"
def addRoundabout (pos : Nat3) : StateT State (Except String) Unit := do
-- Note that the X-Z plane is mirrored!
-- Octagon
let verts : Array Nat3 := #[⟨1, 0, 2⟩, ⟨1, 0, 3⟩, ⟨2, 0, 4⟩, ⟨3, 0, 4⟩, ⟨4, 0, 3⟩, ⟨4, 0, 2⟩, ⟨3, 0, 1⟩, ⟨2, 0, 1⟩]
for hi : i in [:8] do
addRoad (pos + verts[i]) (pos + verts[(i + 1) % 8]'(by simp [verts]; grind)) false
-- Entry and exit roads
addRoad (pos + ⟨0, 0, 3⟩) (pos + ⟨1, 0, 3⟩) false
addRoad (pos + ⟨1, 0, 2⟩) (pos + ⟨0, 0, 2⟩) false
addRoad (pos + ⟨3, 0, 5⟩) (pos + ⟨3, 0, 4⟩) false
addRoad (pos + ⟨2, 0, 4⟩) (pos + ⟨2, 0, 5⟩) false
addRoad (pos + ⟨5, 0, 2⟩) (pos + ⟨4, 0, 2⟩) false
addRoad (pos + ⟨4, 0, 3⟩) (pos + ⟨5, 0, 3⟩) false
addRoad (pos + ⟨2, 0, 0⟩) (pos + ⟨2, 0, 1⟩) false
addRoad (pos + ⟨3, 0, 1⟩) (pos + ⟨3, 0, 0⟩) false
-- Yields
addYield (pos + ⟨0, 0, 3⟩)
addYield (pos + ⟨3, 0, 5⟩)
addYield (pos + ⟨5, 0, 2⟩)
addYield (pos + ⟨2, 0, 0⟩)
def addIntersection1x1 (pos : Nat3) : StateT State (Except String) Unit := do
-- Main roads
addRoad (pos + ⟨0, 0, 2⟩) (pos + ⟨3, 0, 2⟩) false
addRoad (pos + ⟨3, 0, 1⟩) (pos + ⟨0, 0, 1⟩) false
addRoad (pos + ⟨1, 0, 0⟩) (pos + ⟨1, 0, 3⟩) false
addRoad (pos + ⟨2, 0, 3⟩) (pos + ⟨2, 0, 0⟩) false
-- Left turns
addRoad (pos + ⟨1, 0, 1⟩) (pos + ⟨2, 0, 2⟩) false
addRoad (pos + ⟨2, 0, 2⟩) (pos + ⟨1, 0, 1⟩) false
addRoad (pos + ⟨1, 0, 2⟩) (pos + ⟨2, 0, 1⟩) false
addRoad (pos + ⟨2, 0, 1⟩) (pos + ⟨1, 0, 2⟩) false
-- Traffic lights
addTrafficLight (pos + ⟨0, 0, 2⟩) ⟨10, 10, 0⟩
addTrafficLight (pos + ⟨3, 0, 1⟩) ⟨10, 10, 0⟩
addTrafficLight (pos + ⟨2, 0, 3⟩) ⟨10, 10, 10⟩
addTrafficLight (pos + ⟨1, 0, 0⟩) ⟨10, 10, 10⟩
def addIntersectionComplex (pos : Nat3) : StateT State (Except String) Unit := do
-- Clear out center
delete (pos + ⟨1, 0, 1⟩) (pos + ⟨4, 0, 4⟩)
-- Main roads
addRoad (pos + ⟨0, 0, 3⟩) (pos + ⟨5, 0, 3⟩) false
addRoad (pos + ⟨5, 0, 2⟩) (pos + ⟨0, 0, 2⟩) false
addRoad (pos + ⟨2, 0, 0⟩) (pos + ⟨2, 0, 5⟩) false
addRoad (pos + ⟨3, 0, 5⟩) (pos + ⟨3, 0, 0⟩) false
-- Left turns
addRoad (pos + ⟨1, 0, 3⟩) (pos + ⟨3, 0, 1⟩) false
addRoad (pos + ⟨4, 0, 2⟩) (pos + ⟨2, 0, 4⟩) false
addRoad (pos + ⟨2, 0, 1⟩) (pos + ⟨4, 0, 3⟩) false
addRoad (pos + ⟨3, 0, 4⟩) (pos + ⟨1, 0, 2⟩) false
def addIntersection1x2 (pos : Nat3) : StateT State (Except String) Unit := do
addIntersectionComplex pos
addRoad (pos + ⟨0, 0, 4⟩) (pos + ⟨5, 0, 4⟩) false
addRoad (pos + ⟨5, 0, 1⟩) (pos + ⟨0, 0, 1⟩) false
-- Straight traffic lights
addTrafficLight (pos + ⟨1, 0, 4⟩) ⟨15, 15, 0⟩
addTrafficLight (pos + ⟨4, 0, 1⟩) ⟨15, 15, 0⟩
addTrafficLight (pos + ⟨3, 0, 5⟩) ⟨10, 20, 20⟩
addTrafficLight (pos + ⟨2, 0, 0⟩) ⟨10, 20, 20⟩
-- Left turn lights
addTrafficLight (pos + ⟨1, 0, 3⟩) ⟨20, 10, 0⟩
addTrafficLight (pos + ⟨4, 0, 2⟩) ⟨20, 10, 0⟩
def addIntersection2x1 (pos : Nat3) : StateT State (Except String) Unit := do
addIntersectionComplex pos
addRoad (pos + ⟨1, 0, 0⟩) (pos + ⟨1, 0, 5⟩) false
addRoad (pos + ⟨4, 0, 5⟩) (pos + ⟨4, 0, 0⟩) false
-- Straight traffic lights
addTrafficLight (pos + ⟨0, 0, 3⟩) ⟨10, 20, 20⟩
addTrafficLight (pos + ⟨5, 0, 2⟩) ⟨10, 20, 20⟩
addTrafficLight (pos + ⟨4, 0, 4⟩) ⟨15, 15, 0⟩
addTrafficLight (pos + ⟨1, 0, 1⟩) ⟨15, 15, 0⟩
-- Left turn lights
addTrafficLight (pos + ⟨2, 0, 1⟩) ⟨20, 10, 0⟩
addTrafficLight (pos + ⟨3, 0, 4⟩) ⟨20, 10, 0⟩
def addIntersection2x2 (pos : Nat3) : StateT State (Except String) Unit := do
addIntersectionComplex pos
addRoad (pos + ⟨0, 0, 4⟩) (pos + ⟨5, 0, 4⟩) false
addRoad (pos + ⟨5, 0, 1⟩) (pos + ⟨0, 0, 1⟩) false
addRoad (pos + ⟨1, 0, 0⟩) (pos + ⟨1, 0, 5⟩) false
addRoad (pos + ⟨4, 0, 5⟩) (pos + ⟨4, 0, 0⟩) false
-- Straight traffic lights
addTrafficLight (pos + ⟨0, 0, 4⟩) ⟨15, 25, 0⟩
addTrafficLight (pos + ⟨5, 0, 1⟩) ⟨15, 25, 0⟩
addTrafficLight (pos + ⟨4, 0, 5⟩) ⟨15, 25, 20⟩
addTrafficLight (pos + ⟨1, 0, 0⟩) ⟨15, 25, 20⟩
-- Left turn lights
addTrafficLight (pos + ⟨0, 0, 3⟩) ⟨20, 20, 0⟩
addTrafficLight (pos + ⟨5, 0, 2⟩) ⟨20, 20, 0⟩
addTrafficLight (pos + ⟨2, 0, 0⟩) ⟨20, 20, 20⟩
addTrafficLight (pos + ⟨3, 0, 5⟩) ⟨20, 20, 20⟩
def addIntersection (pos : Nat3) (iv : IntersectionVariant) : StateT State (Except String) Unit := do
match iv with
| .roundabout => addRoundabout pos
| ._1x1 => addIntersection1x1 pos
| ._1x2 => addIntersection1x2 pos
| ._2x1 => addIntersection2x1 pos
| ._2x2 => addIntersection2x2 pos
mkDists
/-- Currently unused -/
def addIntersection' (pos : Nat3) : StateT State (Except String) Unit := do
-- Main roads
addRoad (pos + ⟨0, 0, 3⟩) (pos + ⟨5, 0, 3⟩) false
addRoad (pos + ⟨5, 0, 2⟩) (pos + ⟨0, 0, 2⟩) false
addRoad (pos + ⟨2, 0, 0⟩) (pos + ⟨2, 0, 5⟩) false
addRoad (pos + ⟨3, 0, 5⟩) (pos + ⟨3, 0, 0⟩) false
-- Right turns
addRoad (pos + ⟨2, 0, 0⟩) (pos + ⟨0, 0, 2⟩) false
addRoad (pos + ⟨0, 0, 3⟩) (pos + ⟨2, 0, 5⟩) false
addRoad (pos + ⟨3, 0, 5⟩) (pos + ⟨5, 0, 3⟩) false
addRoad (pos + ⟨5, 0, 2⟩) (pos + ⟨3, 0, 0⟩) false
-- Left turns
addRoad (pos + ⟨2, 0, 2⟩) (pos + ⟨3, 0, 3⟩) false
addRoad (pos + ⟨3, 0, 3⟩) (pos + ⟨2, 0, 2⟩) false
addRoad (pos + ⟨2, 0, 3⟩) (pos + ⟨3, 0, 2⟩) false
addRoad (pos + ⟨3, 0, 2⟩) (pos + ⟨2, 0, 3⟩) false
-- Traffic lights
addTrafficLight (pos + ⟨1, 0, 3⟩) ⟨10, 10, 0⟩
addTrafficLight (pos + ⟨4, 0, 2⟩) ⟨10, 10, 0⟩
addTrafficLight (pos + ⟨2, 0, 1⟩) ⟨10, 10, 10⟩
addTrafficLight (pos + ⟨3, 0, 4⟩) ⟨10, 10, 10⟩
-- Yields
addYield (pos + ⟨1, 0, 1⟩)
addYield (pos + ⟨4, 0, 1⟩)
addYield (pos + ⟨1, 0, 4⟩)
addYield (pos + ⟨4, 0, 4⟩)
mkDists
/-- Rename roads in a region -/
def rename (src : Nat3) (start stop : Nat3) : StateT State (Except String) Unit := do
if !(← get).grid.contains src then
throw s!"Grid does not contain {src}"
let newName := (← get).grid[src]!.name
let (start, stop) := endPointsToCorners start stop
for x in [start.x:stop.x + 1] do
for y in [start.y:stop.y + 1] do
for z in [start.z:stop.z + 1] do
if (← get).grid.contains ⟨x, y, z⟩ then
modifyf grid (·.modify ⟨x, y, z⟩ fun pt ↦ { pt with name := newName })
inductive Action
| delete
| road (isHigh : Bool)
| multiRoad (isHigh : Bool)
| building (bv : BuildingVariant)
| yield
| trafficLight (phase : Bool)
| deleteControl
| intersection (iv : IntersectionVariant)
| rename
instance : ToString Action where
toString
| .delete => "Delete"
| .road isHigh => s!"Build {if isHigh then "highway" else "road"}"
| .multiRoad isHigh => s!"Build multilane {if isHigh then "highway" else "road"}"
| .building bv => s!"Build {bv}"
| .yield => "Build yield"
| .trafficLight phase => s!"Build traffic light (phase {if phase then 2 else 1})"
| .deleteControl => "Delete control signal"
| .intersection iv => s!"Build intersection {iv}"
| .rename => "Rename street"
def keyAction : List (Char × Action) := [
('0', .delete),
('1', .road false),
('2', .road true),
('3', .multiRoad false),
('4', .multiRoad true),
('5', .yield),
('6', .trafficLight false),
('7', .trafficLight true),
('8', .deleteControl),
('9', .rename),
('R', .building .house),
('T', .building .apartment),
('Y', .building .office),
('U', .building .park),
('I', .building .farm),
('O', .building .groceryStore),
('P', .building .mine),
('F', .building .industrialPlant),
('G', .building .factory),
('H', .building .shop),
('J', .building .bank),
('Z', .intersection .roundabout),
('X', .intersection ._1x1),
('C', .intersection ._1x2),
('V', .intersection ._2x1),
('B', .intersection ._2x2),
]
def endpointsToPosSize (pos pos' : Nat3) : Nat3 × Nat3 :=
(⟨min pos.x pos'.x, min pos.y pos'.y, min pos.z pos'.z⟩, ⟨diff pos.x pos'.x, diff pos.y pos'.y, diff pos.z pos'.z⟩)
def doAction (curAction : Action) (actionState : List Nat3) (mousePos : Nat3) (newHeight : Nat) : StateT State IO (List Nat3) := do
match actionState, curAction with
| pos :: _, .delete =>
delete pos mousePos
mkDists
| pos :: _, .road isHigh =>
addRoad pos mousePos isHigh
mkDists
| pos :: _, .multiRoad isHigh =>
addMultiRoad pos mousePos isHigh
mkDists
| pos :: pos' :: entrance :: _, .building variant =>
let (pos, size) := endpointsToPosSize pos { pos' with y := pos.y + newHeight / sensitivity }
addBuilding variant pos size entrance mousePos
| _, .yield =>
addYield mousePos
| _, .trafficLight phase =>
addTrafficLight mousePos ⟨10, 10, if phase then 10 else 0⟩
| _, .deleteControl =>
deleteControl mousePos
| _, .intersection iv =>
addIntersection mousePos iv
| src :: pos :: _, .rename =>
rename src pos mousePos
| _, _ =>
return actionState ++ [mousePos]
return []
-- TODO: Add height to existing building
def handleCmd (cmd : String) : StateT State IO Unit := do
match cmd.split ' ' |>.toStringList with
| "h" :: _ | "help" :: _ | "?" :: _ =>
IO.println "HOTKEYS
Left click: Invoke action at location
Right click: Cancel action
ESC: Quit
WASD: Move around
←: Decrease speed
→: Increase speed
↓: Decrement inspect height
↑: Increment inspect height
-: Decrement add building height
=: Increment add building height
[: Fixed pointer mode
]: Free pointer mode"
IO.println <| "\n".intercalate <| keyAction.map fun (c, a) ↦ s!"{c}: {a}"
| "save" :: path :: _ =>
saveState path (← get)
| "load" :: path :: _ =>
set <| ← loadState path
| "speed" :: speed :: _ =>
setf speed (sensitivity * String.toNat! speed)
| "prod" :: _ =>
for b in (← get).buildings do
if b.production > 0 then
IO.println s!"Building {b.variant} at {b.pos}: {b.production}"
-- | "cheat" :: _ =>
-- let b := (← get).buildings
-- modifyf peeps (·.map fun p ↦ { p with pos := b[p.dest]!.entrance })
| "tl" :: A =>
if h : A.length ≥ 6 then
let A := A.map String.toNat!
have : A.length ≥ 6 := by grind
addTrafficLight ⟨A[0], A[1], A[2]⟩ ⟨A[3], A[4], A[5]⟩
else
throw <| .userError "Failed to parse add traffic light command"
| A =>
match A.drop 1, keyAction.find? (·.1 == A[0]!.front) with
| actionStateStr :: mousePosStr :: newHeightStr :: _, some (_, action) =>
let actionState ← .ofExcept <| Lean.fromJson? (← .ofExcept <| Lean.Json.parse actionStateStr)
let mousePos ← .ofExcept <| Lean.fromJson? (← .ofExcept <| Lean.Json.parse mousePosStr)
_ ← doAction action actionState mousePos newHeightStr.toNat!
| _, _ =>
throw <| .userError "Command not found or malformed command"
/-
## Rendering and UI
-/
def Nat3.toVector3 (pos : Nat3) : Vector3 :=
⟨pos.x.toFloat / scale, pos.y.toFloat / scale, pos.z.toFloat / scale⟩
def Nat3.toVector3Shift (pos : Nat3) (s : State) : Vector3 :=
pos.toVector3 - s.origin.toVector3
/-- Low `speed` means paused -/
def maxFrames (speed : Nat) :=
if speed < sensitivity then 2 ^ 32 else fps / ticksPerSecond / (speed / sensitivity)
/-- Draw the game state -/
def render (s : State) (camera : Camera3D) (frames : Nat) : IO Unit := do
let screenWidth := (← getScreenWidth).toFloat
let screenHeight := (← getScreenHeight).toFloat
-- Render buildings
for b in s.buildings do
if !b.isDeleted then
let sizeV3 :=
if b.variant == .park || b.variant == .farm || b.variant == .mine then
{ b.size.toVector3 with y := 0 }
else
b.size.toVector3
let posV3 := b.pos.toVector3Shift s + sizeV3 / 2.0
let entranceV3 := b.entrance.toVector3Shift s + ⟨0, 0.05, 0⟩
let exitV3 := b.exit.toVector3Shift s + ⟨0, 0.05, 0⟩
drawCubeV posV3 sizeV3 b.color
drawCubeWiresV posV3 sizeV3 .black
drawCubeV entranceV3 ⟨0.1, 0.1, 0.1⟩ .green
drawCubeV exitV3 ⟨0.1, 0.1, 0.1⟩ .red
-- Render roads
for (pos, pt) in s.grid do
let posV3 := pos.toVector3Shift s
for (i, road) in iter pt.e do
if road == .none then
continue
let stop := pos.appd i
let stopV3 := stop.toVector3Shift s
drawCylinderEx posV3 stopV3 0.01 0 1 (if road == .low then Color.Raylean.gray else Color.Raylean.gold)
-- Fake shadows
if pos.y != s.origin.y || stop.y != s.origin.y then
drawLine3D { posV3 with y := 0 } { stopV3 with y := 0 } Color.Raylean.lightgray
match pt.control with
| .yield =>
drawCubeV (posV3 + ⟨0, 0.075, 0⟩) ⟨0.02, 0.02, 0.02⟩ .yellow
| .trafficLight t =>
drawCubeV (posV3 + ⟨0, 0.075, 0⟩) ⟨0.02, 0.02, 0.02⟩ (if t.isGreen s.ticks then .green else .red)
| .none =>
pure ()
-- Render peeps
for peep in s.peeps do
-- Unfortunately we can't use `Nat3.toVector3` here because they're `Int`s
if peep.pos == s.buildings[peep.dest]!.entrance && peep.dir.isNone then
continue
let posV3 :=
match peep.dir with
| none =>
peep.pos.toVector3Shift s
| some i =>
let m := (maxFrames s.speed).toFloat
let ivec : Vector3 := ⟨.ofInt (dx i) / scale, .ofInt (dy i) / scale, .ofInt (dz i) / scale⟩
peep.pos.toVector3Shift s - (m - frames.toFloat - 1) / m * (if i < 27 then 1 else 2) * ivec
let color := if peep.brokenDown then .black else s.buildings[peep.work]!.color
drawCube (posV3 + ⟨0, 0.035, 0⟩) 0.075 0.075 0.075 color
drawCubeWires (posV3 + ⟨0, 0.035, 0⟩) 0.075 0.075 0.075 .black
-- Render building names
endMode3D
for b in s.buildings do
if !b.isDeleted then
let name :=
if h : s.grid.contains b.entrance then
s!"{if b.entrance.x == b.pos.x || b.entrance.x == b.pos.x + b.size.x then b.entrance.z else b.entrance.x} {s.grid[b.entrance].name} ({b.variant})"
else
s!"Unnamed {b.variant}"
let sizeV3 := b.size.toVector3
let posV3 := b.pos.toVector3Shift s + sizeV3 / 2.0
let pos2D ← getWorldToScreen (posV3 + ⟨0, 0.2, 0⟩) camera
if pos2D.x < 0 || pos2D.x > screenWidth || pos2D.y < 0 || pos2D.y > screenHeight then
continue
drawText name pos2D.x.toUInt64.toNat pos2D.y.toUInt64.toNat 10 Color.black
beginMode3D camera
/-- Get 3D coordinates at level `y` of 2D screen position
This assumes `up = ⟨0, 1, 0⟩ ∧ projection = .perspective` -/
def project (p : Vector2) (camera : Camera3D) (y width height : Float) : Vector3 :=
let hor := (p.x - width / 2) / (height / 2)
let vert := (p.y - height / 2) / (height / 2)
let focal := 1 / .tan (camera.fovy * .pi / 360)
-- Horizontal angle
let hora := Float.atan2 hor focal
-- Vertical angle
let verta := Float.atan2 vert focal
-- Compute current radial angle
let r := (camera.position.x - camera.target.x).hypot (camera.position.z - camera.target.z)
let h := camera.position.y - camera.target.y
let θ := Float.atan2 r h
-- Compute multiplier for radial move based on `θ - verta`
let mul := .tan (θ - verta) * h / r
-- Radial move
let dradial := mul * Vector3.mk (camera.target.x - camera.position.x) 0 (camera.target.z - camera.position.z)
-- Now compute the tangential move
let d := camera.position - camera.target |>.length
-- The term `h / (h + r * .tan verta)` is intuitively how much horizontal lines get squished or stretched
let mul := d * .tan hora / r * h / (h + r * .tan verta)
-- Tangential move
let dtang := mul * Vector3.mk (camera.target.z - camera.position.z) 0 (camera.position.x - camera.target.x)
-- Now scale to level `y`
(dradial - dtang) * (camera.position.y - y) / (camera.position.y - camera.target.y) + ⟨camera.position.x, y, camera.position.z⟩
/-- Inverse of `Nat3.toVector3Shift` -/
def Raylean.Types.Vector3.toNat3Shift (posV3 : Vector3) (s : State) : Nat3 :=
let posV3 := posV3 + s.origin.toVector3
let round (f : Float) := ((scale * f).round + 1e-9).toUInt64.toNat
⟨round posV3.x, round posV3.y, round posV3.z⟩
/-- Get position of mouse at level `y` (relative to origin) -/
def getMouse3D (y : Int) (camera : Camera3D) (fixedPointer : Bool) : IO Vector3 := do
let yf := Float.ofInt (y / sensitivity) / scale
if fixedPointer then
return camera.position - (camera.position - camera.target) * (camera.position.y - yf) / camera.position.y
let pos2 ← getMousePosition
let windowScale ← getWindowScaleDPI
-- `.dot` is just element-wise product, not the dot product!
return project (pos2.dot windowScale) camera yf (← getScreenWidth).toFloat (← getScreenHeight).toFloat
def spawnInitBuildings : StateT State IO Unit := do
let randPos (gap : Nat) : StateM State Nat3 := do
repeat
let x ← rand (100 + gap)
let z ← rand (100 + gap)
if 50 < x && x < gap + 50 && 50 < z && z < gap + 50 then
continue
return ⟨(← get).origin.x - 50 - gap / 2 + x, 10, (← get).origin.z - 50 - gap / 2 + z⟩
let sideToPos (pos size : Nat3) (side : Fin 4) (offset : Nat) :=
pos +
(match side with
| 0 => ⟨offset, 0, 0⟩
| 1 => ⟨size.x, 0, offset⟩
| 2 => ⟨size.x - offset, 0, size.z⟩
| 3 => ⟨0, 0, size.z - offset⟩)
let randBuilding (variant : BuildingVariant) (size : Nat3) (offset : Nat) (gap : Nat) : StateT State IO Unit := do
let pos ← randPos gap
let size := if (← rand 2) == 0 then size else size.swizzle
let side ← rand 4
try
addBuilding variant pos size (sideToPos pos size side offset) (sideToPos pos size side (offset + 1))
catch e =>
IO.println e
-- Spawn the commercial buildings first so peeps' workplaces get evenly distributed among them
for i in [:2] do
randBuilding .park ⟨6, 1, 12⟩ 3 0
for i in [:3] do
randBuilding .office ⟨8, 2, 4⟩ 2 0
for i in [:7] do
randBuilding .groceryStore ⟨6, 1, 4⟩ 2 0
for i in [:10] do
randBuilding .shop ⟨8, 1, 5⟩ 3 0
for i in [:5] do
randBuilding .factory ⟨10, 5, 10⟩ 5 100
for i in [:2] do
randBuilding .mine ⟨15, 1, 30⟩ 5 200
for i in [:3] do
randBuilding .industrialPlant ⟨10, 5, 10⟩ 5 200
for i in [:10] do
randBuilding .farm ⟨15, 1, 30⟩ 5 200
for i in [:40] do
randBuilding .house ⟨4, 1, 3⟩ 1 100
for i in [:12] do
randBuilding .apartment ⟨8, 4, 5⟩ 1 0
-- Place all peeps at exits
let b := (← get).buildings
modifyf peeps (·.map fun p ↦ { p with pos := b[p.home]!.exit, dest := p.work })
setf money 100000
def renderAction (actionState : List Nat3) (curAction : Action) (mousePos : Nat3) (s : State) (newHeight : Nat) : StateT State IO Unit := do
let mousePosV3 := mousePos.toVector3Shift s
match actionState, curAction with
| pos :: _, .delete =>
let posV3 := pos.toVector3Shift s
drawCubeV ((posV3 + mousePosV3) / 2.0) (mousePosV3 - posV3) Color.Raylean.maroon
| pos :: _, .road isHigh =>
let (length, dir) := endpointsToRoad pos mousePos
let stop := pos.appdk dir length
let posV3 := pos.toVector3Shift s
let stopV3 := stop.toVector3Shift s
drawLine3D posV3 stopV3 (if isHigh then Color.Raylean.orange else Color.Raylean.pink)
-- Fake shadows
if pos.y != s.origin.y || stop.y != s.origin.y then
drawLine3D { posV3 with y := 0 } { stopV3 with y := 0 } Color.Raylean.lightgray
| pos :: _, .multiRoad isHigh =>
let posV3 := pos.toVector3Shift s
drawCubeV ((posV3 + mousePosV3) / 2.0) (mousePosV3 - posV3) (if isHigh then Color.Raylean.orange else Color.Raylean.pink)
| poses, .building _ =>
let poses := poses ++ [mousePos]
if h : poses.length > 1 then
let (pos, size) := endpointsToPosSize poses[0] { poses[1] with y := poses[0].y + newHeight / sensitivity }
let posV3 := pos.toVector3Shift s
drawCubeV (posV3 + size.toVector3 / 2.0) size.toVector3 Color.Raylean.lightgray
drawCubeWiresV (posV3 + size.toVector3 / 2.0) size.toVector3 .black
if h : poses.length > 2 then
drawCubeV (poses[2].toVector3Shift s + ⟨0, 0.05, 0⟩) ⟨0.1, 0.1, 0.1⟩ .green
if h : poses.length > 3 then
drawCubeV (poses[3].toVector3Shift s + ⟨0, 0.05, 0⟩) ⟨0.1, 0.1, 0.1⟩ .red
| _, .yield | _, .trafficLight _ | _, .deleteControl =>
drawCubeV (mousePosV3 + ⟨0, 0.075, 0⟩) ⟨0.02, 0.02, 0.02⟩ Color.Raylean.lightgray
| _, .intersection iv =>
match iv with
| ._1x1 =>
drawCubeV (mousePosV3 + ⟨0.15, 0, 0.15⟩) ⟨0.3, 0, 0.3⟩ Color.Raylean.gray
| _ =>
drawCubeV (mousePosV3 + ⟨0.25, 0, 0.25⟩) ⟨0.5, 0, 0.5⟩ Color.Raylean.gray
| _ :: pos :: _, .rename =>
let posV3 := pos.toVector3Shift s
drawCubeV ((posV3 + mousePosV3) / 2.0) (mousePosV3 - posV3) Color.Raylean.skyblue
| _, _ =>
pure ()
def getInput (stdin : IO.FS.Stream) := do
IO.print "> "
return (← stdin.getLine).trimAsciiEnd.toString
def padTime (n : Nat) :=
if n < 10 then s!"0{n}" else s!"{n}"
def gameLoop (needSpawn : Bool) : StateT State IO Unit := do
if needSpawn then
spawnInitBuildings
let mut camera : Camera3D := {
position := ⟨scale, scale, scale⟩
target := ⟨0, 0, 0⟩
up := ⟨0, 1, 0⟩
fovy := 45
projection := .perspective
}
let stdin ← IO.getStdin
let mut task ← IO.asTask <| getInput stdin
let mut actionState : List Nat3 := []
let mut curAction := .road false
let mut y : Int := 0
let mut newHeight : Nat := sensitivity
let mut frames := 0
let mut err := none
let mut fixedPointer := false
while !(← windowShouldClose) do
-- Fix `up` to prevent the Q and E keys from messing it up
camera := { ← updateCamera camera .thirdPerson with up := ⟨0, 1, 0⟩ }
if ← isKeyDown Key.up then
y := y + 1
if ← isKeyDown Key.down then
y := y - 1
if (← isMouseButtonPressed MouseButton.left) then do
let mousePos := (← getMouse3D y camera fixedPointer).toNat3Shift (← get)
try
actionState ← doAction curAction actionState mousePos newHeight
catch e =>
IO.println e
err := some (e.toString, 5 * fps)
if (← isMouseButtonPressed MouseButton.right) then do
actionState := []
if (← isKeyDown Key.left) then do
modifyf speed (· - 1)
if (← isKeyDown Key.right) then do
modifyf speed (· + 1)
if (← isKeyDown '-'.toNat) then do
newHeight := newHeight - 1
if (← isKeyDown '='.toNat) then do
newHeight := newHeight + 1
if (← isKeyDown '['.toNat) then do
fixedPointer := true
if (← isKeyDown ']'.toNat) then do
fixedPointer := false
for (key, action) in keyAction do
if (← isKeyDown key.toNat) then do
curAction := action
if ← IO.hasFinished task then
let cmd ← (.ofExcept task.get)
try
handleCmd cmd
catch e =>
IO.println e
err := some (e.toString, 5 * fps)
task ← IO.asTask <| getInput stdin
if frames ≥ maxFrames (← get).speed then
doTick
frames := 0
else
frames := frames + 1
err :=
match err with
| some (e, frames) => if frames == 0 then none else some (e, frames - 1)
| none => none
let s ← get
renderFrame do
clearBackground Color.white
let mousePosV3 ← getMouse3D y camera fixedPointer
let mousePos := mousePosV3.toNat3Shift s
renderWithCamera camera do
render s camera frames
drawGrid (s.origin.x / scaleN * 2) 1
renderAction actionState curAction mousePos s newHeight
drawText s!"Active action: {curAction}" 10 10 20 .black
drawText s!"Time: {s.ticks / ticksPerSecond / 60 / 60}:{padTime <| s.ticks / ticksPerSecond / 60 % 60}:{padTime <| s.ticks / ticksPerSecond % 60}" 10 40 20 .black
drawText s!"Money: ${s.money}" 10 70 20 .black
drawText s!"Population: {s.peeps.size}" 10 100 20 .black
drawText s!"Speed: {s.speed / sensitivity}" 10 130 20 .black
drawText s!"{mousePos}" 10 160 20 .black
if hs : s.grid.contains mousePos then
drawText s!"{s.grid[mousePos].name} {s.grid[mousePos].control}" 10 190 20 .black
drawFPS ((← getScreenWidth) - 100) 10
if he : err.isSome then
drawText (err.get he).1 10 ((← getScreenHeight) - 30) 20 Color.Raylean.maroon
if fixedPointer then
let center : Vector2 := ⟨(← getScreenWidth).toFloat / 2, (← getScreenHeight).toFloat / 2⟩
drawLineV (center - ⟨0, 10⟩) (center + ⟨0, 10⟩) .black
drawLineV (center - ⟨10, 0⟩) (center + ⟨10, 0⟩) .black
closeWindow
saveState "save.auto" (← get)
def main (args : List String) : IO Unit := do
setConfigFlags <| Flags.windowResizable ||| Flags.windowHighdpi
initWindow 960 640 "MonotoniCity"
-- The initial dimensions don't matter since we immediately resize the window to work around a HiDPI bug
maximizeWindow
setTargetFPS fps
let mut needSpawn := true
let mut s := {
rng := mkStdGen (← IO.rand 0 (2 ^ 32))
ticks := 0
speed := sensitivity
money := 2 ^ 32 -- The initial value doesn't matter since we spawn a bunch of buildings first
origin := ⟨500, 10, 500⟩
grid := .ofList []
buildings := #[]
occupiedByBuilding := .ofList []
portals := .ofList []
unfull := #v[#[], #[]]
buildingVariants := .replicate _ #[]
occupied := .ofList []
peeps := #[]
}
if h : args.length > 0 then
try
s ← loadState args[0]
needSpawn := false
catch e =>
IO.println s!"Failed to load save {args[0]} with error {e}"
gameLoop needSpawn |>.run' s
-- We can't use `exit` because that won't kill the `getInput` task
IO.Process.forceExit 0