Skip to content

Instantly share code, notes, and snippets.

Avatar

Louis Warren louisswarren

View GitHub Profile
@louisswarren
louisswarren / mfwpp
Last active Nov 25, 2020
Mutex files with preprocessing
View mfwpp
#!/bin/sh
# Generate all .m4 file outputs - being lazy and just re-running the script
# with an argument. To be safe AND lazy, add a useless argument just to make
# sure this doesn't fork bomb me some day if I change how this is done.
if [ -z "$1" ]; then
exec find $(dirname -- "$0") -name '*.m4' -exec "./$0" '{}' 'safety' \;
fi
# Generate $1 from its .m4 file.
@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 $< $@
You can’t perform that action at this time.