Skip to content

Instantly share code, notes, and snippets.

View louisswarren's full-sized avatar

Louis Warren louisswarren

View GitHub Profile
@louisswarren
louisswarren / .gitignore
Last active November 22, 2020 05:53
cat
*.vim
*.agdai
@louisswarren
louisswarren / bench.py
Created October 14, 2020 07:52
Python benchmarker
from time import time, sleep
def runtime(f, retcont):
t = time()
r = f()
tt = time()
if retcont == []:
retcont.append(r)
elif retcont is not None:
assert(r == retcont[0])
@louisswarren
louisswarren / lexer.py
Last active September 27, 2020 10:14
BNF
from collections import namedtuple
import re
# Literal patterns only match themselves, but quack like regular expressions
class LiteralPattern(str):
def match(self, other):
if other.startswith(self):
return LiteralMatch(str(self))
return None
@louisswarren
louisswarren / Makefile
Last active September 27, 2020 05:40 — forked from skeeto/Makefile
C Object Oriented Programming Example
CFLAGS = -std=c99 -Wall
main : main.o
.PHONY : test clean
test : main
./$^ "*regex*" "*vtable*" < main.c
clean :
@louisswarren
louisswarren / threeand.c
Created September 19, 2020 23:24
Find non-intersecting binary triplets
#include <stdio.h>
#include <stdlib.h>
#include <stdint.h>
void print_bin(uint32_t x)
{
int i;
for (i = 31; i >= 0; --i)
putchar(x & (1 << i) ? '1' : '0');
}
@louisswarren
louisswarren / natded.agda
Created September 8, 2020 05:43
Natural deduction rules directly in Agda
arrowelim : {A B : Set} → (A → B) → A → B
arrowelim f a = f a
data _⊎_ (A B : Set) : Set where
inl : A → A ⊎ B
inr : B → A ⊎ B
disjintro₁ : {A : Set} → A → (X : Set) → A ⊎ X
disjintro₁ a X = inl a
@louisswarren
louisswarren / agda.agda
Created August 20, 2020 10:39
agda.agda
data ℕ : Set where
zero : ℕ
suc : (n : ℕ) → ℕ
{-# BUILTIN NATURAL ℕ #-}
infixl 6 _+_
_+_ : (n m : ℕ) → ℕ
n + zero = n
n + suc m = suc (n + m)
@louisswarren
louisswarren / natded.tex
Last active March 11, 2021 22:59
Natural deduction with handy latex commands
\documentclass[a4paper]{article}
\usepackage{bussproofs}
\usepackage{savetrees}
\usepackage{amsmath}
\newcommand{\using}[2]{\AxiomC{}\RightLabel{#1}\UnaryInfC{#2}}
\newcommand{\assume}[1]{\AxiomC{#1}}
\newcommand{\closed}[2]{\AxiomC{$\left[\text{#2}\right]^\text{#1}$}}
@louisswarren
louisswarren / Makefile
Last active December 30, 2022 08:10
Tiny library for PPM output
.PHONY: default
default: spectrum.png
.PHONY: waves-video
waves-video: waves
./$< | mpv --no-correct-pts --fps=30 --scale=oversample -
.PHONY: test test-video
test: nz.png
sxiv $^
@louisswarren
louisswarren / Makefile
Last active August 12, 2020 03:20
Conway's game of life with pbm files
CC = gcc
CFLAGS = -O3 -std=c99
.PHONY: test
test: life
./life < gosper.pbm | mpv --no-correct-pts --fps=20 --scale=oversample -
.PHONY: time
time: life-limited
time ./$< < pulsar.pbm > /dev/null