Scott Fleischman scott-fleischman

2016

2015

KSSU splits timer GUI challenge

This document presents an informal “GUI framework benchmark” along the lines of [TodoMVC][]: it is a relatively simple, well-defined problem that can be used to illustrate the strengths and weaknesses of different GUI paradigms. However, unlike TodoMVC, this problem is specifically designed to stress test state management in multi-stage modal flows, where modifications to the application state can be complex but must not be committed immediately.

The problem in question is to write a speedrunning timer for [Kirby Super Star Ultra][kssu]’s [True Arena boss rush mode][kssu-true-arena]. This is a completely meaningless problem to most people, but that’s okay—this document does not assume any familiarity with KSSU or with speedrunning timers more generally. However, I do want to go over a couple basics to provide some context on the problem being solved:

The True Arena is a videogame boss rush mode where the objective is to beat a series of bosses as quickly as possible.

Papers I like Pt. 1 Papers I like Pt. 2

Let's start meta:

Lamport - State the Problem Before Describing the Solution (1978). … 1-page memo. Read it.
Herlihy - Wait-free synchronization (1991) … Truly seminal. Lucid + enough good ideas for 4 papers easily.
Cook - How complex systems fail (1998) … 4 pages that anyone working on/with complex systems should read.

	module Prime where

	open import Coinduction

	open import Data.Empty
	open import Data.Nat
	open import Data.Nat.Properties
	open import Data.Nat.Divisibility
	open import Data.Fin hiding (pred; _+_; _<_; _≤_; compare)
	open import Data.Fin.Props hiding (_≟_)

	;SMBDIS.ASM - A COMPREHENSIVE SUPER MARIO BROS. DISASSEMBLY
	;by doppelganger ([email protected])

	;This file is provided for your own use as-is. It will require the character rom data
	;and an iNES file header to get it to work.

	;There are so many people I have to thank for this, that taking all the credit for
	;myself would be an unforgivable act of arrogance. Without their help this would
	;probably not be possible. So I thank all the peeps in the nesdev scene whose insight into
	;the 6502 and the NES helped me learn how it works (you guys know who you are, there's no

	(* -- mode: ocaml; -- *)

	module type FUNCTOR = sig
	type 'a t
	val map : ('a -> 'b) -> 'a t -> 'b t
	end

	type 'a monoid = {unit : 'a ; join : 'a -> 'a -> 'a}

	type var = string

	(* An initial attempt at universal algebra in Coq.
	Author: Andrej Bauer <[email protected]>

	If someone knows of a less painful way of doing this, please let me know.

	We would like to define the notion of an algebra with given operations satisfying given
	equations. For example, a group has of three operations (unit, multiplication, inverse)
	and five equations (associativity, unit left, unit right, inverse left, inverse right).
	*)

	S ::= S S S
	\| S S
	\| 'a'


	aaaaaaaaaaaaaaaaaaaaaaaaaaaaa

	O(n^3)

	-- A simply-typed lambda calculus, and a definition of normalisation by
	-- evaluation for it.
	--
	-- The NBE implementation is based on a presentation by Sam Lindley from 2016:
	-- http://homepages.inf.ed.ac.uk/slindley/nbe/nbe-cambridge2016.pdf
	--
	-- Adapted to handle terms with explicitly typed contexts (Sam's slides only
	-- consider open terms with the environments left implicit/untyped). This was a
	-- pain in the ass to figure out.

	{-# OPTIONS --without-K #-}

	{-
	Claim: finitary inductive types are constructible from Π,Σ,Uᵢ,_≡_ and ℕ, without
	quotients. Sketch in two parts.

	1. First, construction of finitary inductive types from Π, Σ, Uᵢ, _≡_ and binary trees.
	Here I only show this for really simple, single-sorted closed inductive types,
	but it should work for indexed inductive types as well.