Skip to content

Instantly share code, notes, and snippets.

Avatar

Carter Tazio Schonwald cartazio

View GitHub Profile
@cartazio
cartazio / finitary.agda
Created Jan 4, 2022 — forked from atennapel/finitary.agda
Finitary non-indexed datatype signatures
View finitary.agda
{-# OPTIONS --type-in-type #-}
open import Agda.Builtin.Unit
open import Agda.Builtin.Sigma
open import Data.Product
data Ty : Set where
U : Ty
Pi : (A : Set) -> (A -> Ty) -> Ty
PiInd : Ty -> Ty
@cartazio
cartazio / howto grep hackage.md
Last active Sep 7, 2021
how to grep all of hackage!
View howto grep hackage.md

first decide where to place your local copy of stuff

cd $YOURPLACE

how to get the most recent version of everything

cabal list --simple | awk '{print ($1)}' | uniq | time xargs -P20 -n1 cabal get

then use grep/ ripgrep or whatever to find where code exists/is used/ is defined

then look at the matches

View examples-fromListN.hs
$ rg -e fromListN -t haskell ./
./network-topic-models-0.2.0.1/RunLDA.hs
139: let termCounts = V.fromListN (M.size nodeItems)
./network-topic-models-0.2.0.1/RunCI.hs
174: let termCounts = V.fromListN (M.size nodeItems)
./network-topic-models-0.2.0.1/RunST.hs
171: let termCounts = V.fromListN (M.size nodeItems)
View babyCalculusEqations.hs
d/dx (x ^ a) == d/dx (a -> x )
we never consider a ^ x === x -> a ()
log_x(\nu Y -> T) == \mu Z -> log_X T , where Z == log_X Y
(translation: every time we see log_X Y , in T, replace taht with Z )
View Sadd.hs
module Main where
import Data.Word
import Data.Int
import Foreign.Ptr
import Foreign.C.Types
main = c_MD5Final `seq` print "yay"
@cartazio
cartazio / StructExample.hs
Created Jun 6, 2019
hacky unfinished scribblings about how to do fancy struct instances
View StructExample.hs
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE ExplicitForAll#-}
module Main where
import Data.Struct
--import Data.Struct.TH
--import qualified Data.Coerce as Crc
import Data.Coerce (coerce)
View chordCorrect.als
/* ========================================================================
A MODEL IN ALLOY
OF A CORRECT VERSION OF THE CHORD RING-MAINTENANCE PROTOCOL
Pamela Zave, August 2016.
Copyright AT&T Labs, Inc., 2016, 2018.
======================================================================== */
open util/ordering[Time] as trace
open util/ordering[Node] as ring
@cartazio
cartazio / packagesize.txt
Last active Feb 19, 2019
rounded up to the nearest megabyte, generated with du -hm -d1 ./ | sort -rn
View packagesize.txt
143 .//sugarhaskell-0.1
122 .//morfette-0.4.7
53 .//http2-1.6.4
40 .//cjk-0.1.0.1
39 .//qt-1.1.6.1
37 .//uhc-light-1.1.10.0
37 .//cld2-0.1.1.1
33 .//texmath-0.11.2
33 .//happstack-yui-7373.5.3
32 .//scholdoc-texmath-0.1.0.1
@cartazio
cartazio / fixYoMath.r
Last active Feb 11, 2019
NAN NAN you cant get the undefined float value man
View fixYoMath.r
install("inline")# not needed after the first time
library("inline")
nanBoom <- cfunction(c(dummy="ANY"),body="
fenv_t fenv;
unsigned int new_excepts = FE_DIVBYZERO | FE_INVALID ;
fegetenv(&fenv);
fenv.__mxcsr &= ~(new_excepts << 7);
fesetenv(&fenv);
return dummy;
",includes="#include <fenv.h>",language="C")
@cartazio
cartazio / simplemat.c
Created Jan 29, 2019
old matrix mat code
View simplemat.c
// #include <emmintrin.h>
#include <immintrin.h>
// #if defined (__SSE4_2__) || defined (__SSE4_1__)
// for some reason i can't get anything newer than sse4.2 work with both gcc-clang and clang
// #include <smmintrin.h>
// #endif
#include <memory.h>