ikedaisuke’s gists

ikedaisuke / gist:1408300

Created November 30, 2011 07:05

Yet another program in Haskell to pretty-print and parse files

	module Main where

	-- see also Shugo's blog
	-- http://shugo.net/jit/20111129.html#p01

	import Control.Applicative
	import Data.List
	import System.Environment
	import System.IO
	import qualified Text.ParserCombinators.Parsec as PC

ikedaisuke / gist:1376024

Created November 18, 2011 09:47

TPPmark 写経途中

	module Half where

	-- http://staff.aist.go.jp/reynald.affeldt/tpp2011/garrigue_candy.v

	open import Data.Nat
	open import Data.Nat.Properties
	open import Relation.Binary.Core
	open import Relation.Binary.PropositionalEquality

	half : ℕ -> ℕ

ikedaisuke / gist:1344227

Created November 7, 2011 05:12

Thierry's proof of the principle of infinite descent (a part) in Agda2

	infiniteDescent : ∀ {a l} -> (A : Set a) -> (R : Rel A l) ->
	(P : Pred A l) -> Noether A R ->
	((x : A) -> P x -> ∃ (λ y -> R y x × P y)) ->
	(z : A) -> ¬ (P z)
	infiniteDescent A R P noe f
	= noe (λ w → ¬ P w) g
	where g : (x : A) → ((y : A) → R y x → ¬ P y) → ¬ P x
	g x h px with f x px
	... \| (v , k) = h v (proj₁ k) (proj₂ k)

ikedaisuke / gist:1344224

Created November 7, 2011 05:10

Thierry's proof of the principle of infinite descent (a part) in Agda1/Alfa

ikedaisuke / gist:1305738

Created October 22, 2011 07:20

dart (bleeding_edge rev. 623) の型検査バグ? ではなく、型検査オプションが必要だという話でした

	foo() {
	List<List<int>> arr;
	arr[0] = 0; // no error nor warning
	arr = 0; // ditto
	}
	main() {}

	// % dart foo.dart
	// %
	// % dart --enable_type_chekcs foo.dart

ikedaisuke / gist:1211203

Created September 12, 2011 13:03

Peano axioms of natural numbers in Agda

	module Peano where

	open import Data.Nat using (ℕ; zero; suc)
	open import Relation.Binary.Core using (_≢_; refl)

	{-
	already defined:
	data ℕ : Set where
	zero : ℕ -- axiom 1
	suc : (n : ℕ) -> ℕ -- axiom 2

ikedaisuke / gist:1087586

Created July 17, 2011 13:23

CoPL Nat Derivation Rules

	module Nat where

	data Nat : Set where
	Z : Nat
	S : Nat -> Nat

	data _plus_is_ : Nat -> Nat -> Nat -> Set where
	P-Zero : (m n : Nat) -> Z plus m is n
	P-Succ : (l m n : Nat) -> l plus m is n -> (S l) plus m is (S n)

ikedaisuke / gist:918522

Created April 13, 2011 21:59

Render particles in Gloss

	module Main where

	-- http://www.f13g.com/%A5%D7%A5%ED%A5%B0%A5%E9%A5%DF%A5%F3%A5%B0/Haskell/GLUT/#content_1_7

	import System.Random
	import Graphics.Gloss
	import Graphics.Gloss.Interface.Simulate

	data Particle
	= Particle { position :: Point

ikedaisuke / gist:916931

Created April 13, 2011 03:52

Rotate a square in Gloss (with key event (DOWN-key))

	module Main where

	-- http://www.f13g.com/%A5%D7%A5%ED%A5%B0%A5%E9%A5%DF%A5%F3%A5%B0/Haskell/GLUT/#content_1_4

	import Graphics.Gloss.Interface.Game

	data State
	= State { angle :: Float
	, isPositive :: Bool
	, picture :: Picture }

ikedaisuke / gist:915964

Created April 12, 2011 17:22

Rotate a square in Haskell GLUT

	module Main where

	-- http://www.f13g.com/%A5%D7%A5%ED%A5%B0%A5%E9%A5%DF%A5%F3%A5%B0/Haskell/GLUT/#content_1_0

	import qualified Control.Monad.State as S
	import Graphics.UI.GLUT

	type AngleState a = S.StateT GLdouble IO a

	timeOut :: Timeout

Ikegami Daisuke ikedaisuke