Changes
3 changed files (+1163/-32)
-
-
@@ -10,10 +10,23 @@ namespace Raylean-- Helpful for debugging instance : ToString Vector3 := ⟨fun v ↦ s!"({v.1}, {v.2}, {v.3})"⟩ instance : Add Vector3 where add a b := ⟨a.x + b.x, a.y + b.y, a.z + b.z⟩ instance : Sub Vector3 where sub a b := ⟨a.x - b.x, a.y - b.y, a.z - b.z⟩ instance : HMul Vector3 Float Vector3 where hMul a c := ⟨a.x * c, a.y * c, a.z * c⟩ instance : HDiv Vector3 Float Vector3 where hDiv a c := ⟨a.x / c, a.y / c, a.z / c⟩ /-- This is in Raylib but not Raylean so let's just define it ourselves -/ def drawCubeV (pos size : Vector3) (color : Color) := drawCube pos size.x size.y size.z color /-- Same as above -/ def drawCubeWiresV (pos size : Vector3) (color : Color) := drawCubeWires pos size.x size.y size.z color
-
@@ -23,28 +36,11 @@ def fps := 60def screenWidth := 960 def screenHeight := 640 /-- Grid side length (each cell is 5m by 5m) -/ def N := 200 /-- Grid height -/ def M := 20 def origin : Vector3 := ⟨N.toFloat / 20, M.toFloat / 20, N.toFloat / 20⟩ instance : Add Vector3 where add a b := ⟨a.x + b.x, a.y + b.y, a.z + b.z⟩ instance : Sub Vector3 where sub a b := ⟨a.x - b.x, a.y - b.y, a.z - b.z⟩ instance : HDiv Vector3 Float Vector3 where hDiv a b := ⟨a.x / b, a.y / b, a.z / b⟩ structure Nat3 where x : Nat y : Nat z : Nat deriving Lean.ToJson, Lean.FromJson deriving BEq, Hashable, Lean.ToJson, Lean.FromJson inductive BuildingVariant | house
-
@@ -65,10 +61,13 @@ def BuildingVariant.ofString? : String → Option BuildingVariantstructure Building where pos : Nat3 size : Nat3 entrance : Nat3 exit : Nat3 variant : BuildingVariant occupants : Nat deriving Lean.ToJson, Lean.FromJson def Building.occupants (b : Building) := def Building.capacity (b : Building) := match b.variant with | .house => 1 | .apartment => b.size.x * b.size.y * b.size.z / 2
-
@@ -84,10 +83,13 @@ def Building.color (b : Building) :=| .shop => Color.Raylean.purple | .factory => Color.Raylean.green /-- Vehicle is synonymous with person in this game -/ structure Vehicle where home : Nat work : Nat pos : Nat3 dest : Nat3 deriving Lean.ToJson, Lean.FromJson inductive Road | none
-
@@ -100,36 +102,130 @@ instance [Lean.ToJson α] : Lean.ToJson (Vector α n) whereinstance [Lean.FromJson α] : Lean.FromJson (Vector α n) where fromJson? j := do let A : Array α ← Array.fromJson? j let A ← Array.fromJson? j if h : A.size = n then return h ▸ A.toVector else throw s!"expected size {n}, got {A.size}" structure Point where roads : Vector Road 24 occupant : Option Nat name : String ein : Vector Road 24 eout : Vector Road 24 deriving Lean.ToJson, Lean.FromJson def dx : Vector Int 24 := List.replicate 9 (-1) ++ List.replicate 6 0 ++ List.replicate 9 1 |>.toArray.toVector def dy : Vector Int 24 := List.replicate 8 [-1, 0, 1] |>.flatten.toArray.toVector def dz : Vector Int 24 := #v[-1, -1, -1, 0, 0, 0, 1, 1, 1, -1, -1, -1, 1, 1, 1, -1, -1, -1, 0, 0, 0, 1, 1, 1] -- Roads should not go straight up or straight down #guard (List.range 24 |>.mapFinIdx fun i _ hi ↦ dx[i] != 0 || dz[i] != 0).and -- `i` and `23 - i` should be in opposite directions #guard (List.range 24 |>.mapFinIdx fun i _ hi ↦ dx[i] == (-dx[23 - i]) && dy[i] == (-dy[23 - i]) && dz[i] == (-dz[23 - i])).and def appd (p : Nat3) (i : Nat) (hi : i < 24 := by grind) : Nat3 := ⟨p.x + dx[i] |>.toNat, p.y + dy[i] |>.toNat, p.z + dz[i] |>.toNat⟩ def Point.empty : Point := ⟨.replicate 24 .none, none⟩ ⟨.replicate 24 .none, .replicate 24 .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 abbrev Grid := Vector (Vector (Vector Point (M + 1)) (N + 1)) (N + 1) instance [BEq α] [Hashable α] [Lean.FromJson α] [Lean.FromJson β] : Lean.FromJson (Std.HashMap α β) where fromJson? j := .ofList <$> List.fromJson? j -- TODO: routing table for each building, reverse grid structure State where rng : Nat speed : Nat day : Nat time : Nat grid : Grid origin : Nat3 grid : Std.HashMap Nat3 Point buildings : Array Building dists : Array (Std.HashMap Nat3 Nat) occupied : Std.HashSet Nat3 vehicles : Array Vehicle deriving Lean.ToJson, Lean.FromJson makeLenses State -- TODO open that namespace? /-- 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 each destination using BFS -/ def mkDist : StateM State Unit := do let mut dists : Array (Std.HashMap Nat3 Nat) := #[] let s ← get for building in s.buildings do -- TODO refactor this into its own func let mut q : Std.Queue Nat3 := .enqueue building.entrance .empty let mut dist : Std.HashMap Nat3 Nat := .ofList [(building.entrance, 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 hs : s.grid.contains u then for hi : i in List.range 24 do let v := appd u i match (s.grid[u]'hs).ein[i]'(by grind) with | .low => if !dist.contains v then dist := dist.insert u (d + 1) q := q.enqueue v | .high => if !dist.contains v then dist := dist.insert v (d + 1) q := q.enqueue v if hs : s.grid.contains v then match (s.grid[v]'hs).ein[i]'(by grind) with | .high => let v' := appd u i if !dist.contains v' then dist := dist.insert v' (d + 1) q := q.enqueue v' | _ => pure () | .none => pure () dists := dists.push dist -- TODO update dists in state -- TODO def tick : StateM State Unit := do modify <| over State.Lens.rng (· + 2) -- Randomize list of vehicles using Fisher-Yates -- For each vehicle, if has dest then look at dist table and iterate through all possible moves -- Cannot do a move if occupied currently or after this tick -- Do that move -- Set the new list of vehicles with the new position and direction (for animating) modify <| over State.Lens.time (· + 1) def Nat3.toVector3 (p : Nat3) : Vector3 := ⟨p.x.toFloat / 10, p.y.toFloat / 10, p.z.toFloat / 10⟩
-
@@ -138,7 +234,7 @@ def render (s : State) : IO Unit := dofor b in s.buildings do let p := b.pos.toVector3 let s := b.size.toVector3 let o := p - origin + s / 2.0 let o := p - s.origin.toVector3 + s / 2.0 drawCubeV o s b.color drawCubeWiresV o s .black
-
@@ -159,12 +255,14 @@ def handleCmd (cmd : String) : StateT State IO Unit := doIO.FS.writeFile path <| Lean.toJson (← get) |>.compress | ["l", path] => set <| ← loadState path | ["v", speed] => modify <| set State.Lens.speed <| String.toNat! speed | "b" :: variant :: dims => let variant := BuildingVariant.ofString? variant if h : dims.length = 6 && variant.isSome then let dims := dims.map String.toNat! have : dims.length = 6 := by grind modify <| over State.Lens.buildings (·.push ⟨⟨dims[0], dims[1], dims[2]⟩, ⟨dims[3], dims[4], dims[5]⟩, variant.get (by grind)⟩) modify <| over State.Lens.buildings (·.push ⟨⟨dims[0], dims[1], dims[2]⟩, ⟨dims[3], dims[4], dims[5]⟩, variant.get (by grind), 0⟩) else throw <| .userError "Failed to parse build command" | _ =>
-
@@ -193,8 +291,9 @@ def gameLoop : StateT State IO Unit := dodrawFPS (screenWidth - 100) 10 clearBackground Color.white renderWithCamera camera do drawGrid (N / 20) 1 render (← get) let s ← get drawGrid (s.origin.x / 10) 1 render s closeWindow def main : IO Unit := do
-
@@ -205,8 +304,13 @@ def main : IO Unit := dosetTargetFPS fps _ ← gameLoop.run { rng := 0 speed := 1 day := 0 time := 0 grid := Vector.replicate _ (Vector.replicate _ (Vector.replicate _ .empty)) origin := ⟨200, 10, 200⟩ grid := .ofList [] dists := #[] buildings := #[] occupied := .ofList [] vehicles := #[] }
-
-
-
@@ -70,3 +70,6 @@ INFO: TIMER: Target time per frame: 16.667 millisecondshttps://www.raylib.com/cheatsheet/cheatsheet.html The street names are from https://github.com/rossburton/barnum/blob/master/source-data/street-names.txt
-
-
street-names.txt (new)
-
@@ -0,0 +1,1024 @@Abbott Abercrombie Adair Bridge Addicks Howell Adeline Ainsworth Akerswood Alchester Alder Aldwych Amundson Anchorage Anderson Anniston Anns Apahon Appaloosa Apple Tree Apple Valley Arcola Arden Walk Arthur Ashbrook Ashford Forest Ashmont Ashstone Ashworth Aspen Aspen Pine Atwood Autumn Autumn Oaks Barkers Barkers Landing Barkers Point Barons Barryknoll Bateswood Bauxhall Bavarian Bayberry Bayou Knoll Bayou River Baytown Beach Beaufort Beaux Bridge Beaverwood Bekah Belfort Belgrave Bell Manor Bellville Benson Bensonwood Bent Creek Bergmann Billy Cross Birch Post Birchtree Birchwood Birnam Wood Bison Blackberry Blackberry Farm Blackberry Ridge Blackhaw Black Springs Bluebird Blue Grass Bobwood Boheme Bolling Brook Boom Boulinwood Boutwell Bow String Bradford Bramblewood Branford Breezy Creek Brenley Brenner Creek Brewers Briar Knoll Briar Path Brick Bridge Forest Brierbrook Britoak Brittmoore Broadgreen Broadway Brook Bridge Brookline Brooksedge Brookside Brooxie Brownleaf Brush Creek Bryn Mawr Bubbling Brook Buckingham Buck Ram Burfordi Burlington Burntwood Burrows Farm Butterfly Calumet Camara Cambury Camelback Cane Creek Canella Canon Gate Cape Charles Capital Captains Cardinal Carlingford Carnelian Carnton Carolcrest Carrick Carters Grove Cattail Cavershamwood Caylors Wood Cedarcrest Cedar Lake Cedar Lane Cedar Ridge Cedarville Cedarwood Center Center Hill Centre Oak Chadbourne Charstone Chatham Chatsworth Cherry Cherrybark Cherryfield Chertsy Chesley Chestnut Chico Churchill Churchill Downs Cindywood Cinnamon Oak Circle Gate Circleshade Circle Trees Claiborne Claiborne Farm Clarington Clear Spring Cliffrose Cloverbrook Coachmans Cobblestone Comely Commercial Commodore Conifer Conner Coppershire Cordie Lee Cordova Cornuta Cornwall Corporate Center Corporate Edge Corporate Gardens Corsica Cottage Cottage Glen Cotton Boll Cotton Cross Cotton Plant Cottonwood Country Country Place Countryside Cranberry Hill Cranbrook Creathwood Creek Bridge Creekside Crestwood Crestwyn Croixwood Crooked Creek Crooked Oak Crossbow Cross Country Crossflower Cross Pike Cross Ridge Crossroads Cross Village Crye Crest Currywood Curve Crest Dairy Ashford Dallager Danbury Danforth Darby Dan Daria Darrel Deauville Deep Valley Deer Deerfield Deer Path Delano Dellwood Deodara Dewhurst Diamond Leaf Dian Dogwood Dogwood Crest Dogwood Grove Dogwood Villa Donnington Donnybrook Doral Dove Field Dovie Dragonfly Drayton Driftwood Driving Park Dubuque Duckhorn Duncaster Dundee Dunedin Durley Eagle Branch Eagle Ridge Ealing Eastern Eben Echo Edenfield Edgewood Effingham Egerton Eldor Eldridge Electra Elk Run Elm Elmhurst Elm Leaf Elm Ridge Enterprise Everett Evergreen Eversholt Everwood Exeter Fair Harbor Fairlawn Fairmeadows Fairport Fairy Falls Falling Leaf Farindon Farm Hill Farmingdale Farmington Farnifold Fawnlake Featherleigh Fern Fernspring Fernwood Fiddlers Elbow Fireside Fischer Flaghoist Fleetwood Oaks Fleetwood Place Flowers Oak Fords Station Forest Forest Bend Forest Downs Forest Hill Forest Hill Irene Forestwood Foster Dale Foster Ridge Fountainside Fox Creek Fox Fern Foxgate Fox Grape Frontage Gadient Gainesway Gallery Garden Arbor Gayle Gaywood Germantown Germantown Village Germanwood Gershwin Gilbert Glenchester Glen Meadow Golden Chance Golden Fields Goringwood Goswell Grand Oak Grasshopper Gray Ridge Great Oaks Greeley Greenbelt Green Clover Green Downs Green Forest Green Holly Green Knoll Greenmeadow Green Orchard Greenpark Green Pastures Greensprings Green Twig Greenwood Grenville Grisby Grist Mill Grove Grove Brook Grove Lake Grove Meadow Grove Mill Groveshire Grovewood Gumleaf Hacks Cross Hampton Grove Hancock Hanson Hapano Harding Harriet Harrod Harvest Haseley Havenhill Havenhurst Havershire Hawksprings Hawthorne Hayden Hayley Hazel Hazelton Heatherbrook Heatherfield Heatherglen Heatherly Heathmore Heathstone Heifort Hemlock Herdsman Heritage Hermitage Hickory Hickory Glen Hickory Post Hidden Hidden Harbor Hidden Oaks Hidden Valley Highgate Highland Highwood Hill Creek Hillcrest Hillside Hobbits Glen Holcombe Hollow Creek Hollow Fork Holly Heath Holly Hill Hollyhock Holly Spring Homestead Homeward Honeye Honey Hill Honey Tree Howard Hudson Huntcliff Hunters Hunters Creek Hunters Den Hunters Forest Hunters Grove Hunters Hill Hunters Horn Hunters Run Huntleigh Icerose Ilo Imperial Indian Creek Industrial Ingberg Innsbruck Interlachen Inwood Irish Ironwood Island Grove Isleton Itasca Ivy Ivy Leaf Ivy Wall Jamaca Jarvis Jasmine Jeffrey Jenna Jermyn Jewell Jocelyn Jody Johnson Joliet Judd Judicial Julianne Juno Justen Kahlden Kallie Katy Keats Kelchner Kellywood Kelman Kelvin Kersh Keswick Keystone Kickerillo Kimberley Kimbro Kimbrook Kimbrough Kimbrough Grove Kimbrough Park Kimdale Kimforest Kimridge Kinderhill Kingcastle Kingsride Kinship Kirby Kirkwood Kismet Knoll Knollwood Krueger La Costa Lake Lakemere Lakeside Lakespur Lancashire Landfair Langwood Lansing La Quinta Lasso Last Arrow Laurel Laurel Ridge Laurie Laurinburg Leaning Ash Lecuyer Leesburg Lee Shore Leeward Legend Leighton Creek Lennox Liberty Linden Linson Lockridge Locust Lofton Londonderry Long Lake Long Oak Lookout Lost Meadow Lydia Mac Macey Magnolia Ridge Magnolia Tree Main Maize Malabar Malcolm Mallard Mandeville Manning Manning Trail Manor Woods Maple Maple Shadow Mardite Marine Market Marsh Martha Marthas Martin Grove Maryknoll Marylane Marywood Chase Masters Matisse May Mayfield May Woods Mcclellan Mcdonald Mcdougal Mchenry Mckusick Mcvay Meadow Meadow Creek Bridge Meadow Glen Meadow Hill Meadowlark Meadow Run Meadowview Meadow Wood Melville Memorial Memorial Mews Mendel Merchants Merenerm Mer Rouge Mid Oaks Mikeyair Mill Miller Farms Millstone Mimosa Mimosa Tree Minar Misty Creek Misty Hollow Misty Meadow Mistywood Monarda Mont Blanc Monte Vallo Moonlight Bay Moore Morgan Morning Dove Morningside Moss Tree Mossy Creek Muir Mulberry Mustang Myeron Myrtle Myrtlea Myrtlewood Mystic Ridge Neal Nelson Nena Neshoba Neshoba Trace Newberry Newell New England Newgate Newman New Riverdale Newsum Nightingale Nikerton Nohapa Nolan Norcrest Nordic Norell Norman Normandale Normandy North Northbrook Northland Northridge Northwestern Norwich Norwood Nottingham Oaks Novak Nova Scotia Oak Oak Bend Oakes Oak Glen Oakgreen Oakhill Oak Hill Oakland Oakleigh Oak Manor Oak Park Oakridge Oak Run Oaksedge Oakville Oarman Oasis Obrien Odegard Odell Ojib Old Bridge Old Deer Old Elm Oldfield Old Katy Old Mill Old Post Oldridge Old Stone Old Village Olene Ole Pike Olinda Olive Olney Oak Omaha Omar Orchard Grove Orchard Hill Oren Oriole Orleans Orwell Oryan Osgood Osman Osprey Otchipwe Ottawa Otter Ottumwa Overhill Overlook Owens Oxboro Oxen Oxford Ozark Paddock Painters Palisade Palomino Panama Pangbourne Panoha Panorama Parade Paradise Paragon Paris Park Parker Park Ridge Parkwood Partridge Patchester Paul Pawnee Peabody Peacan Pebblebrook Pecan Trees Peller Penbrook Penfield Penmont Penrose Pepper Periwinkle Perkins Perthshire Pete Mitchell Pickett Pike Wood Pine Pinecroft Pine Hollow Pinehurst Pineridge Pinerock Pinesap Pine Tree Pine Valley Pioneer Pittsfield Plainwood Plantation Planting Pond View Poplar Poplar Estates Poplar Lake Poplar Woods Port Charlotte Pridalea Primrose Professional Pyron Oaks Quail Quail Grove Quant Quarry Queens Queensbury Queensmill Quinlan Quirt Radbrook Rainbow Rainwood Ramblewood Ramsey Rancho Bauer Ravencliff Ravenhill Ravensdale Ravine Redfield Redhaw Redwood Place Regents Regentview Renoir Reunion Rhineland Rice Rich Hill Rico Ridge Ridgetown Riggs Rivard Riverain River Bend Rivercrest Riverdale River Forest River Heights Riverlace River Reach River Roads River Valley Riverview Riverwind Riverwood Robin Rock Rocky Hollow Rolling Valley Rosehaven Round Hill Rowan Rowlock Roxbury Rubyshade Rummel Creek Rustleaf Rutherford Saddle Saddlegait Saddle Ridge Saint Croix Saint Francis Saint George Saint Louis Saint Marys San Augustine Sanders Hill Sanders Ridge Sandy Sandy Berry Sandy Creek Sandy Port Savannah Sawyer School Schulenberg Scruggs Sea Smoke Seeley Settlers Shadeley Shadowmoss Shady Creek Shannon Oaks Shelton Shepherdwood Sherburne Sibelius Silkwood Silverbark Silvergate Sister Tagg Siward Skyview Sleepy Hollow Soboda Somerset Sonning Southchester Southern Southmoore Sparkling Lake Spear Point Splinter Oak Square Lake Stafford Stagecoach Stags Leap Staloch Stamford Staples Station Hill Steamboat Steeplegate Sterling Stillbrook Still Meadow Stillwater St Ives Stonebridge Stone Creek Stone Farm Stonegate Stoneleigh Stone Mill Stone Walk Stonewyck Stout Summer Fields Sundance Sunny Creek Sunny Slope Sunrise Sunset Surrey Sweet Oaks Sweetwood Swenson Sycamore Tagg Tall Pine Tallwood Talmage Tamarack Tamerlane Tanoak Tanya Taylorcrest Teddington Tending Thicket Thistlewood Thorene Thornbranch Thornbrook Thorncroft Thornvine Thornwick Threadneedle Three Chimneys Timber Toro Tosca Tower Towering Pines Towne Trademark Trail Hollow Trailville Trailwood Trotter Trowbridge Tuenge Tully Turkey Turkey Creek Turkey Trail Turpins Glen Tuscany Twisted Oak Union Valley Crest Val Verde Van Tassel Vicherne Victoria Vienna Village Shops Vineyard Walking Horse Walkwood Walnut Walnut Creek Walworth Wargate Washington Water Waterleaf Watkins Waverly Waxlander Wax Myrtle Webster Weeping Willow Wellton West Westcott Western Westlake Park Westminster Weston Westport Wethersfield Wheatley Wheatstone Whipper Whitemarsh Whitewater White Wing Wickchester Wickshire Wilchester Wilcrest Wildcrest Wild Oak Wildpines Wildwood Wilkins Willard Willey William Willow Willowbend Willow Brook Winchester Windbreak Windham Winding Creek Winding Oak Windstone Way Winged Foot Winners Winnton Winterberry Winter Oaks Woffington Wolf Bend Wolf Park Wolf River Woodbend Wood Branch Park Wood Briar Wood Creek Woodford Woodgate Woodhall Woodlane Woodleaf Woodridge Woodruff Woodside Woodsong Woodthorpe Wren Wycliffe Wyndhurst Wynterhall Yorkchester Zurich
-