Project Serpent: Day 3

Yesterday I spent some time improving my MenuInput data type. I realized I haven’t mentioned that at all in this series of posts, so I’ll talk about it a little.

A MenuInput basically describes an editable entry in an options menu. Simple menu inputs might be things like NatBox "Number of heads" 3. This represents an input box that can contain a natural number, labeled “Number of heads”, and whose default value is 3. Similarly, FloatBox "Game speed" 1 is a box called “Game speed” that contains a floating point number defaulting to 1. There are also selection boxes, like Options "Hair color" ["blue", "green", "red"] "green", which means that there are three choices for hair color defaulting to green. And finally, there are toggle options with additional configuration available if they’re toggled “on”: Toggle "Gravity" [FloatBox "Strength" 9.8, Options "Direction" ["up", "down", "left", "right"] "down"] means that gravity can be either on or off, and if it’s on you can also configure its strength and select one of the four cardinal directions for it.

Every kind of menu input has a type of values that it accepts. A NatBox accepts natural numbers, a FloatBox accepts floating point numbers, an Option accepts one of the available strings from the list of choices1, and a Toggle can either be “off” or it can be “on” with a list of values for the extra configuration options. Because Idris is a dependently typed language, we can actually encode this statement as a function from MenuInputs to Types, and that’s exactly what valueFor does in Spec.idr.

So part of my time yesterday was spent writing additional utilities for working with lists of menu inputs and the values they can take. For example, I have a function to apply an update2 to a particular entry in a menu, or to get the value of a certain entry.

Anyway, that is one system I have developed that I hope to get a lot of use out of when I get to programming the menus. So far, I’m not there yet, but I’m getting there: the other thing I spent time on yesterday was my skeleton implementation of the game state, with a focus on states in the “in-game” phase. Right now I’m working on what you might call the meat of the game: stepping a game state by moving the snake, doing collision detection, and possibly growing it or ending the game.

Today I’ll finish writing functions for stepping the game state, and hopefully by tomorrow I’ll be ready to start hooking those functions up to some kind of UI!


  1. we represent these in Idris as strings paired with proofs that they’re in the list of available options. 
  2. I also have a function mapping MenuInputs to the kinds of updates you can perform on them: for example, a Toggle can be toggled and a NatBox can be incremented or decremented, and any input can be set to an exact value. See updateFor in Spec.idr for details. 
Advertisements

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s