nvanderw

FROM alpine:latest

RUN ["apk", "add", "bash"]
COPY "sieve.sh" "$WORKDIR"
ENTRYPOINT ["./sieve.sh"]

nvanderw

# Moved: https://github.com/nvanderw/voting/blob/main/proportional.py

nvanderw

(i:=__import__,n:=255,p:=lambda a:print(a,end='',flush=True),t:=i('blessed').Terminal(),H:=0,w:=t.width,h:=t.height,p(t.clear+t.home),x:=1,y:=1,X:=1,Y:=1,u:=lambda v,p,m:v if 0<p<m-1else -v,p(t.hide_cursor),all((x:=x+X,y:=y+Y,X:=u(X,x,w),Y:=u(Y,y,h),R:=i('colorsys').hsv_to_rgb(H/n,1,1),p(t.move_xy(x,y)+t.bold+t.color_rgb(*map(lambda m:int(m*n),R))+"☻"),H:=H+7&n,i('time').sleep(.01))for _ in iter(int,1)))

nvanderw

import os
import signal
import sys
import time
import random

NUM_ITERATIONS = 10000000
NUM_WORKERS = 20

def unpack_bits(bs):

nvanderw

from blessed import Terminal
from colorsys import hsv_to_rgb
from time import sleep
from random import randrange, choice
from sys import stdout

# Print with no trailing newline
def printn(*args, **kwargs):
    kwargs['end'] = ''
    print(*args, **kwargs)

nvanderw

# For finding the best wordle starting word

import argparse
import itertools
import math
import random

from dataclasses import dataclass
from multiprocessing import Pool
from typing import Any

nvanderw

newtype Fix f = Fix (f (Fix f))

-- Define List as the fixed point of a type operator
data ListR a t = Nil | Cons a t
type List a = Fix (ListR a)

-- The type operator ListR represents "one layer" of the structure
-- of List. We can do something fold-like with it.
-- My question is, is there a name for f? It's like a catamorphism
-- but doesn't recurse into the data.

nvanderw

module Main

data Literal : Type where
    float : Float -> Literal

-- A PostScript program which takes a stack of one size to a stack of
-- another size.
-- (PostScript m n) takes a stack of size m and returns a stack of size n.
data PostScript : Nat -> Nat -> Type where
    nop : PostScript n n

nvanderw

{-# LANGUAGE DataKinds, KindSignatures, GADTs #-}

data Nat = Zero | Succ Nat

data Even :: Nat -> * where
    Even_base :: Even Zero
    Even_induct :: Even k -> Even (Succ (Succ k))

data Odd :: Nat -> * where
    Odd_base :: Odd (Succ Zero)

nvanderw

{-# LANGUAGE DataKinds, KindSignatures, GADTs #-}

data Nat = Zero | Succ Nat

-- Bounded naturals
data Fin :: Nat -> * where
    FZ :: Fin (Succ n)
    FS :: Fin n -> Fin (Succ n)

data Vect (n :: Nat) a where