dunhamsteve

#!/usr/bin/env python3

# Show process memory usage via ncdu

import json, subprocess, time, tempfile
from collections import defaultdict
from itertools import dropwhile

def psize(s): return int(s[0:-1])*{'K':2**10, 'M':2**20, 'G':2**30}[s[-1]]
def runcmd(cmd):

dunhamsteve

<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE plist PUBLIC "-//Apple//DTD PLIST 1.0//EN" "http://www.apple.com/DTDs/PropertyList-1.0.dtd">
<plist version="1.0">
<dict>
	<key>BBEditDocumentType</key>
	<string>CodelessLanguageModule</string>
	<key>BBLMLanguageCode</key>
	<string>IDR2</string>
	<key>BBLMLanguageDisplayName</key>
	<string>Idris2</string>

dunhamsteve

// Normalization by evaluation
//
// 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.
//
// In this version, instead of passing in each branch as an argument, we pass
// a single object with a named function for each constructor.  The case statements

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