Skip to content

Instantly share code, notes, and snippets.

@petermarks
petermarks / folds.hs
Created June 14, 2012 22:47
Folds and unfolds
{-# LANGUAGE ViewPatterns, GADTs, KindSignatures, ScopedTypeVariables #-}
import Data.List
foldr2 :: (a -> b -> b) -> b -> [a] -> b
foldr2 f b [] = b
foldr2 f b (x:xs) = f x (foldr2 f b xs)
foldr3 :: ((a,b)->b,()->b) -> [a] -> b
foldr3 (f,b) [] = b ()
foldr3 (f,b) (x:xs) = f (x, foldr3 (f,b) xs)
@petermarks
petermarks / gpretty.hs
Created August 7, 2012 14:46
Generic pretty printing
{-# language TypeSynonymInstances, FlexibleInstances, DeriveDataTypeable #-}
module GPretty where
import Data.Data
import Data.Typeable
import Data.Generics.Aliases
data Tree a = Node a [Tree a]
deriving (Show, Data, Typeable)
@petermarks
petermarks / Bot.hs
Created December 16, 2012 12:21
Sketch of Bot interface
module Bot where
import Control.Monad.Reader
import Control.Monad.Cont
import Data.List
data Command
= NoAction
| Fire
| Accelerate
@petermarks
petermarks / Alloc.hs
Created December 20, 2012 19:51
Room allocations
module Alloc where
import Data.List
import Control.Arrow
data Allocs = Allocs {checkouts :: [Int], checkins :: [Int]} deriving (Eq, Show)
allocs :: [[Int]] -> (Int, [Allocs])
allocs = first length . mapAccumL f []
{ stdenv }:
stdenv.mkDerivation
{ name = "website";
src = ../code;
phases = [ "installPhase" ];
installPhase = ''
mkdir -p $out
cp -r * $out/
ln -s /data/files $out
#{ stdenv, fetchurl, qtbase, qtmultimedia, qttools, alsa-lib, libusb }:
with import <nixpkgs> {};
# TODO: disable some plugins
stdenv.mkDerivation {
name = "qlcplus-4.11.0";
src = ./qlcplus-QLC-_4.11.0;
buildInputs = [ qt5.qtbase qt5.qtscript qt5.qtmultimedia qt5.qttools alsaLib libusb libudev qt5.qmakeHook ];
nativeBuildInputs = [ pkgconfig ];
@petermarks
petermarks / record.idr
Created July 4, 2018 10:06
Proving record field get and set are an identity for the field value
record R where
constructor MkR
foo : Nat
foo_identity : (foo (set_foo x r)) = x
foo_identity {x} {r} with (foo (set_foo x r))
foo_identity {x} | y = ?rhs