Skip to content

Instantly share code, notes, and snippets.

@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
#{ 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 ];
{ stdenv }:
stdenv.mkDerivation
{ name = "website";
src = ../code;
phases = [ "installPhase" ];
installPhase = ''
mkdir -p $out
cp -r * $out/
ln -s /data/files $out
@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 []
@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 / 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 / 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 / Puzzle.hs
Created April 29, 2012 10:22
Logic Puzzle Solver
{-# LANGUAGE ExistentialQuantification, MultiParamTypeClasses #-}
module Puzzle where
import Data.List
--------------------------------------------------------------------------------
-- Specific to this puzzle
main :: IO ()
module Main where
import Control.Monad
import Control.Monad.Logic
import Control.Monad.State.Strict
import qualified Data.Map as M
type BindingT k v = StateT (M.Map k v)
bind :: (Ord k, Eq v, Monad m) => k -> v -> BindingT k v m ()
@petermarks
petermarks / Coded.hs
Created March 17, 2012 15:34
Coded (dead end)
{-# LANGUAGE DeriveFunctor, DeriveTraversable, DeriveFoldable #-}
module Coded where
import Control.Unification
import Control.Unification.IntVar
import Control.Monad.Logic
import Data.Functor.Fixedpoint
import Data.List
import Data.Foldable
import Data.Traversable