dunhamsteve

// Normalization by evaluation
//
// I was playing around with mogensen-scott encoding of the STLC and got carried away.
//
// Inspired Andras Kovacs' by elaboration-zoo  typecheck-HOAS-names
//
// By inspired, I mean that I wrote this after studing Kovacs' stuff and then
// cheated and looked up some of the answers when I got to the infer/check bit.
// Any bugs are mine, though.

dunhamsteve

from yaml import Loader, load
# I got the idea from:
#   https://github.com/Granitosaurus/macos-compose/tree/master
# in Karabiner, assign right_control to non_us_backslash (which somehow is §)
#
# in keys.yaml, lines like:
# §to: →
# §in: ∈
# §ni: ∋
# §all: ∀

dunhamsteve

#!/usr/bin/env python3

# Scans the chrome service worker caches and prints url  and size for each directory
# Add -v to the command line for more details

import struct, os, functools, sys

def uvarint(data,pos):
    x = s = 0
    while True:

dunhamsteve

module WellTyped

import Data.Vect

data Ty = TyInt | TyBool | TyFun Ty Ty

interpTy : Ty -> Type
interpTy TyInt = Integer
interpTy TyBool = Bool
interpTy (TyFun x y) = interpTy x -> interpTy y

dunhamsteve

#!/bin/bash

# This script generates a treemap of the current memory usage (RSS)

awkcode='
$1 == "PID" { next }
/.*/ {
    cmd = substr($0,index($0,$4));
    sub(/.*\//,"",cmd);
    gsub(/\//,"_",cmd);

dunhamsteve

\   
\!! ‼
\! ¡
\!? ⁉
\"' “
\"< «
\"> »
\" ̈
\"A Ä
\"E Ë

dunhamsteve

-- https://www.cs.nott.ac.uk/~psymp4/files/dependently-typed-compilers.pdf

data Exp : Type -> Type where
  Val : t -> Exp t
  Add : Exp Nat -> Exp Nat -> Exp Nat
  If  : Eq t => Exp Bool -> Exp t -> Exp t -> Exp t

eval : Exp t -> t
eval (Val x) = x
eval (Add x y) = eval x + eval y

dunhamsteve

#!/usr/bin/env python3

# This script creates Idris2.docset for use in Dash.app
# It expects idris to be in ~/.idris2 and is hardcoded to 0.5.1 at the moment.

import os, sqlite3, html5lib, re

oj = os.path.join

debug = lambda *x: None

dunhamsteve

#!/usr/bin/env python3

# pip3 install pyobjc requests

from AppKit import NSPasteboard
import json, requests, re, sys

def rewrite(url):
  m = re.match(r'https://www.craft.do/s/(\w+)',url)
  if not m:

dunhamsteve

#!/usr/bin/env node

// Placed in the public domain

// Dump craft database as json

// This is intended as a sample of how to extract craft raw data for
// playing around with. It has no dependencies aside from node.

// The top section reads the Craft DB into memory (takes about 380ms for 50k blocks)