Skip to content

Instantly share code, notes, and snippets.

@mb64
mb64 / DerivingEq.idr
Created July 10, 2020 03:34
Deriving equality with Idris 2's new reflection -- strange bug where it doesn't work from a different module
module DerivingEq
import Language.Reflection
%language ElabReflection
public export
countArgs : (ty : TTImp) -> Nat
countArgs (IPi _ _ ExplicitArg _ _ retTy) = 1 + countArgs retTy
countArgs (IPi _ _ _ _ _ retTy) = countArgs retTy
@mb64
mb64 / Bidir.idr
Created August 6, 2020 06:39
An attempt at a well-typed implementation of Complete+Easy. Needless to say, it does not work.
module Bidir
Ident : Type
Ident = String
mutual
BaseCtx' : Type
Ctx' : BaseCtx' -> Type
CtxItem' : (b : BaseCtx') -> (c : Ctx' b) -> Type
@mb64
mb64 / Nat.agda
Created October 5, 2020 05:52
An attempt to prove that the free semigroup on one generator is commutative.
{-# OPTIONS --cubical --safe #-}
open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism using (Iso; isoToPath)
data N : Set where
one : N
_+_ : N → N → N
assoc : (a b c : N) → (a + b) + c ≡ a + (b + c)
@mb64
mb64 / Makefile
Created October 17, 2020 23:59
GCC vs repne scasl: wstrlen bench
.PHONY: all bench
all: bench
bench: main_c main_asm
@echo "Running the C version..."
@bash -c 'time ./main_c'
@echo
@echo "Running the asm version..."
@bash -c 'time ./main_asm'
@mb64
mb64 / flat_tree.c
Created October 31, 2020 08:42
Flat trees in ATS and C
/* A flat representation of
* data Tree = Leaf Int | Node Tree Tree
*
* Either:
* - *ft is LEAF and a single int follows
* - *ft is NODE and two subtrees follow
*/
#define LEAF 0
#define NODE 1
@mb64
mb64 / example.idr
Created November 25, 2020 00:29
All the polymorphism in Idris 2
f : {a : Type} -> a -> a
f {a=Int} x = 2 * x
f {a=String} x = "twice " ++ x
f {a=_} x = x
main : IO ()
main = do
-- Ad-hoc polymorphism type 1: type-based overloading
-- Also in: C++, Java
printLn $ "hi " ++ "there" -- uses the ++ for String
@mb64
mb64 / .bashrc
Created December 9, 2020 07:10
reMarkable 2 dotfiles
umask 022
declare -x PAGER='less'
declare -x EDITOR='vim'
declare -x VISUAL="${EDITOR}"
declare -x FCEDIT="${EDITOR}"
declare -x LS_COLORS='no=01;37:fi=01;37:di=01;34:ln=01;36:pi=01;32:so=01;35:do=01;35:bd=01;33:cd=01;33:ex=01;31:mi=00;37:or=00;36:'
declare -x HISTCONTROL=ignoreboth:erasedups
@mb64
mb64 / Prolog.hs
Created January 31, 2021 02:17
A simple, readable Prolog interpreter in Haskell
{-# LANGUAGE ImportQualifiedPost, BlockArguments #-}
module Main where
import Control.Applicative
import Control.Monad
import Control.Monad.RWS
import Data.Char
import Data.Foldable
import Data.List
import Data.Set qualified as Set
@mb64
mb64 / heap_bench.sml
Created March 13, 2021 00:27
Heap benchmarks in MLton
(** A small benchmark for heap implementations
*
* Task: (mutably) sort an array, using heap sort
* Implementations:
* - BinaryHeap, a simple binary heap implemented with mutable array operations
* - PairingHeap, Okazaki's strict amortized pairing heap
* - SplayHeap, Okazaki's strict amortized splay heap
* - BinomialHeap, Okazaki's strict amortized binomial heap
* - LeftistHeap, Okazaki's strict rank-based leftist heap
*
@mb64
mb64 / PowerSeries.agda
Last active April 7, 2021 23:00
A proof that formal power series over an arbitrary commutative ring form a commutative ring, formalized in Agda using guarded coinduction.
{-# OPTIONS --guardedness --safe #-}
open import Data.Product
open import Function using (_$_)
open import Relation.Binary using (IsEquivalence)
open import Algebra
open import Relation.Binary.Definitions
import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
open import Tactic.RingSolver using (solve-∀)