CoderPuppy

(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)

CoderPuppy

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

{-# OPTIONS_GHC -Wno-tabs #-}

module LamCo2 where

import Numeric.Natural

data Term
	= Var Int
	| Lam Term
	| App Term Term

CoderPuppy

{-# OPTIONS_GHC -Wno-tabs #-}

module LamCo where

import Debug.Trace

data Term
	= TVar Int
	| TLam Term
	| TAp Term Term

CoderPuppy

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

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

CoderPuppy

Keybase proof

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:

CoderPuppy

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

This is a tool for generating .defs (and then .libs) from .dlls I created while helping @hbomb79

Usage

batch:

dumpbin -exports <lib>.dll > <lib>.dll.exports

shell:

{echo LIBRARY .dll; echo EXPORTS; lua manip.lua .dll.exports.txt} > .def

CoderPuppy

data Type = TName TypeName          -- Foo
          | TVar TypeVar            -- a
          | TLambda TypeVar Type    -- \(a : Type) => b -- not strictly necessary
          | TForAll TypeVar Type    -- \{a : Type) => b
          | TExists TypeVar Type    -- (a : Type ** b)
          | TFunc Type Type         -- a -> b
          | TArrow Constraint Type  -- a => b
          | TInst Type Type         -- a b

type Nat f g = forall a. f a -> g a