I hereby claim:
- I am coderpuppy on github.
- I am coderpuppy (https://keybase.io/coderpuppy) on keybase.
- I have a public key ASBpYyLjaXIPLMFePGVJVj9_5IehALYXrFDAO0sDXe-UQAo
To claim this, I am signing this object:
Drew CoderPuppy
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| local fill_i | |
| local fill_left = 0 | |
| local function place_fill(f) | |
| if fill_left <= 0 then | |
| local is = {} | |
| for i = 1, 16 do | |
| local d = turtle.getItemDetail(i) | |
| if d then | |
| is[d.name] = is[d.name] or i | |
| end |
CoderPuppy
/ guix-idris.scm
Created
October 2, 2020 15:29
Guix packages for Idris 2, bootstrapping all the way
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| (use-modules | |
| (guix profiles) | |
| (gnu packages idris) | |
| (guix packages) | |
| (guix git-download) | |
| (guix download) | |
| (guix build-system gnu) | |
| ((guix licenses) #:prefix license:) | |
| (gnu packages multiprecision) | |
| (gnu packages llvm) |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| local function refuel(n) | |
| local sel = turtle.getSelectedSlot() | |
| local slot = 1 | |
| while turtle.getFuelLevel() < n do | |
| if slot > 16 then | |
| error 'no fuel' | |
| end | |
| turtle.select(slot) | |
| if not turtle.refuel(1) then | |
| slot = slot + 1 |
CoderPuppy
/ LamCo2.hs
Created
January 30, 2019 15:49
Applying "Functional Derivation of a Virtual Machine for Delimited Continuations" to an evaluator with multi-prompt delimited continuations
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| {-# OPTIONS_GHC -Wno-tabs #-} | |
| module LamCo2 where | |
| import Numeric.Natural | |
| data Term | |
| = Var Int | |
| | Lam Term | |
| | App Term Term |
CoderPuppy
/ LamCo.hs
Created
January 29, 2019 04:37
Sketch of a virtual machine supporting multi-prompt delimited continuations in Haskell
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| {-# OPTIONS_GHC -Wno-tabs #-} | |
| module LamCo where | |
| import Debug.Trace | |
| data Term | |
| = TVar Int | |
| | TLam Term | |
| | TAp Term Term |
CoderPuppy
/ DelimCont3.idr
Last active
January 30, 2019 15:45
Multi-prompt Delimited Continuations in Idris
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| import Control.Lens | |
| mutual | |
| record Frame sfd dfd r (sd : sfd) (ps : List (sfd, Type, Type)) rt jt where | |
| constructor MkFrame | |
| dd : dfd | |
| ret : rt -> Frames sfd dfd r ps -> r | |
| jmp : jt -> Frames sfd dfd r ps -> r | |
| data Frames : (sfd : Type) -> (dfd : Type) -> (r : Type) -> (ps : List (sfd, Type, Type)) -> Type where | |
| Nil : Frames sfd dfd r [] |
CoderPuppy
/ data-fun.agda
Last active
March 3, 2018 03:59
Fun with theoretical primitive data structures
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| makeRecord : | |
| (ks : Set) (o : Relation.Binary ks) → | |
| {¬refl : ¬ Relation.Reflexive o} {asym : Relation.Asymmetric o} {trans : Relation.Transitive o} → | |
| {τs : Record ks o $ makeRecord ks o $ λ k τs → Record o τs → Type} → | |
| ((k : ks) → Record (filter (o k) ks) o (fst $ _≅_.l⇒r joinSplitRecord τs) → get τs k) → | |
| Record ks o τs | |
| Record : | |
| (ks : Set) → (o : Relation.Binary ks) → | |
| {¬refl : ¬ Relation.Reflexive o} {asym : Relation.Asymmetric o} {trans : Relation.Transitive o} → | |
| Record ks o (makeRecord ks o $ λ k τs → Record o τs → Type) → Type |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| reverseT : List a -> List a -> List a | |
| reverseT r [] = r | |
| reverseT r (a::as) = reverseT (a::r) as | |
| reverse : List a -> List a | |
| reverse = reverseT [] | |
| total | |
| reverseT_ends_ts : Proofs.reverseT ts as = Proofs.reverse as ++ ts | |
| reverseT_ends_ts {ts} {as=[]} = Refl |
CoderPuppy
/ README.md
Created
October 4, 2016 02:54
A tool for generating .defs (and then .libs) from .dlls