Skip to content

Instantly share code, notes, and snippets.

View AdamBrouwersHarries's full-sized avatar
🎼
Music, Dance & Maths

Adam Brouwers-Harries AdamBrouwersHarries

🎼
Music, Dance & Maths
View GitHub Profile
@AdamBrouwersHarries
AdamBrouwersHarries / isort.idr
Created October 20, 2023 18:01
A short gist showing how we can encode the correctness of a sorting algorithm through Idris2's type system. We define a structure to track the correct ordering of the output, and use lienarity to ensure that the output is a permutation of the input.
module ISort
import Data.Linear.Interface
import Data.Linear.Notation
import Data.Linear.LNat
import Data.Linear.LEither
import Data.Linear.LMaybe
import Data.Linear.LVect
-- Some useful things defined for LNats
@AdamBrouwersHarries
AdamBrouwersHarries / Reproduction.idr
Created October 19, 2023 21:44
A partial attempt at writing a constructively sorted vector, where sorting ensures that the output is a permutation of the input
module Linear.Reproduction
import Data.Linear.Interface
import Data.Linear.Notation
import Data.Linear.LNat
import Data.Linear.LEither
import Data.Linear.LMaybe
-- Some useful things defined for LNats
@AdamBrouwersHarries
AdamBrouwersHarries / Treemember.idr
Created March 12, 2021 21:58
A demonstration of "full" searching for logging contexts. Note, this currently hangs Idris2 with an infinite loop.
module Treemember
import Data.List
import Data.List1
import Data.String
import Data.These
import Data.Maybe
import Data.So
import Libraries.Data.StringTrie
import Libraries.Data.StringMap
module Treemember
import Data.List1
import Data.String
import Data.These
import Data.Maybe
import Libraries.Data.StringTrie
import Libraries.Data.StringMap
-- Take a path through the trie, and return a node's name (if there is one).
module SpecD
-- Provide a placeholder type for a spectrogram
SpectTy : Type
SpectTy = Nat
-- Datatype to track whether we should be returning a residual
data ResidualTy = Residual | Pair
-- Transform ResidualTy to a type that we can return
@AdamBrouwersHarries
AdamBrouwersHarries / bpm.rs
Created December 22, 2019 01:05
Simple terminal based BPM detection/reporting in Rust uing tui
/// Based on code from tui-rs/examples, adapted to support bpm calculation by beats.
/// A simple example demonstrating how to handle user input. This is
/// a bit out of the scope of the library as it does not provide any
/// input handling out of the box. However, it may helps some to get
/// started.
///
/// This is a very simple example:
/// * A input box always focused. Every character you type is registered
/// here
@AdamBrouwersHarries
AdamBrouwersHarries / Raphael.hs
Created October 4, 2018 11:25
Utterly nerd sniped.
module Main where
import Control.Monad
import Data.List
import Data.Function
-- Define a name - i.e. just a variable
data Name = MkName Char deriving (Eq, Show)
-- Define a context - a mapping from variabels to values
object Tree {
class PrintBuilder(var content: String, var indent: Int) {
def +=(line: String) = {
content = content + "\n" + (" " * indent) + line
}
def in : Unit = {
indent = indent + 1
}
@AdamBrouwersHarries
AdamBrouwersHarries / analyse.sh
Created July 5, 2017 15:48
Analysis tool for profiling information
#!/bin/sh
resultfile=$1
profilefile=$(echo $resultfile | sed -e "s/result/profiling_data/g")
summaryfile=$(echo $resultfile | sed -e "s/result/profile_summary/g")
readablesummary=$(echo $resultfile | sed -e "s/result/profile_summary_readable/g")
touch $profilefile
/**
* Created by adam on 31/05/17.
*/
package profiler
import scala.collection.mutable
import com.github.nscala_time.time.Imports._
class CheckPoint(val checkpointName: String, val startTime: org.joda.time.DateTime) {}
// NOT THREADSAFE