Skip to content

Instantly share code, notes, and snippets.

Avatar

Louis Warren louisswarren

View GitHub Profile
@louisswarren
louisswarren / bench.py
Created Oct 14, 2020
Python benchmarker
View bench.py
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])
View lexer.py
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 Sep 27, 2020 — forked from skeeto/Makefile
C Object Oriented Programming Example
View Makefile
CFLAGS = -std=c99 -Wall
main : main.o
.PHONY : test clean
test : main
./$^ "*regex*" "*vtable*" < main.c
clean :
@louisswarren
louisswarren / threeand.c
Created Sep 19, 2020
Find non-intersecting binary triplets
View threeand.c
#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 Sep 8, 2020
Natural deduction rules directly in Agda
View natded.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
View 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
Created Aug 17, 2020
Natural deduction with handy latex commands
View natded.tex
\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 Oct 23, 2020
Tiny library for PPM output
View Makefile
.PHONY: test test-video
test: nz.png
sxiv $^
test-video: fire
./fire | mpv --no-correct-pts --fps=30 --scale=oversample -
%.png: %.ppm
convert $< $@
@louisswarren
louisswarren / Makefile
Last active Aug 12, 2020
Conway's game of life with pbm files
View Makefile
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
@louisswarren
louisswarren / spiral.py
Last active Aug 8, 2020
Spirals of numbers
View spiral.py
class Turtle:
directions = [( 0, 1),
(-1, 0),
( 0, -1),
( 1, 0)]
def __init__(self, x=0, y=0, d=0, boundary=lambda x, y: True):
self.x = x
self.y = y
self.d = d
You can’t perform that action at this time.