Skip to content

Instantly share code, notes, and snippets.

Avatar

David Thrane Christiansen david-christiansen

View GitHub Profile
View VeryFun.idr
module VeryFun
class VeryFun (f : Type -> Type) (dict : Functor f) | f where
funIdentity : {a : Type} -> (x : f a) ->
map @{dict} id x = id x
funComposition : {a : Type} -> {b : Type} ->
(x : f a) -> (g1 : a -> b) -> (g2 : b -> c) ->
map @{dict} (g2 . g1) x = (map @{dict} g2 . map @{dict} g1) x
instance VeryFun List %instance where
View MkMonoid.idr
module MkMonoid
import Language.Reflection.Elab
||| Generate a Monoid dictionary
total
mkMonoid : Semigroup a => (neutral : a) -> Monoid a
mkMonoid @{semigroup} neutral = mkMonoid' _ semigroup neutral
where
mkMonoid' : (a : Type) -> (constr : Semigroup a) -> a -> Monoid a
@david-christiansen
david-christiansen / MkShow.idr
Last active Oct 26, 2017
Generating a "Show" instance
View MkShow.idr
module MkShow
import Language.Reflection.Elab
mkShow : (a : Type) -> (a -> String) -> Show a
mkShow = %runElab (fill (Var (SN (InstanceCtorN `{Show}))) *> solve)
shower : Show Float
shower = mkShow _ (const "oops")
@david-christiansen
david-christiansen / fix-audio.sh
Last active May 15, 2017
How to fix the audio on the current crop of OPLSS videos
View fix-audio.sh
#!/bin/bash
for i in *.mp4; do
if [ ! -a "${i%.mp4}-fixed.mp4" ]; then
ffmpeg -i "$i" -vcodec copy -ac 1 "${i%.mp4}-fixed.mp4"
fi
done
@david-christiansen
david-christiansen / PlusRewrite.idr
Last active Aug 8, 2016
Simplifying "plus" expressions with rewrite-rule combinators and quasiquotes in Idris
View PlusRewrite.idr
module PlusRewrite
import Language.Reflection
import Language.Reflection.Utils
rewrite_plusSuccRightSucc : TT -> Maybe Tactic
rewrite_plusSuccRightSucc `(plus ~n (S ~m)) = Just $ Rewrite `(plusSuccRightSucc ~n ~m)
rewrite_plusSuccRightSucc `(S ~n) = rewrite_plusSuccRightSucc n
rewrite_plusSuccRightSucc `(plus ~n ~m) = rewrite_plusSuccRightSucc n <|> rewrite_plusSuccRightSucc m
rewrite_plusSuccRightSucc _ = Nothing
@david-christiansen
david-christiansen / monad-notation.rkt
Created Mar 23, 2016
Monad notation for Typed Racket
View monad-notation.rkt
#lang typed/racket
(require (for-syntax racket syntax/parse) racket/stxparam)
(provide do-impl define-do pure)
(module+ test (require typed/rackunit))
(define-syntax (<- stx) (raise-syntax-error '<- "used outside of do"))
View Main.idr
module Main
import Data.Vect
import Data.Fin
%default total
||| If a value is neither at the head of a Vect nor in the tail of
||| that Vect, then it is not in the Vect.
notHeadNotTail : Not (x = y) -> Not (Elem x xs) -> Not (Elem x (y :: xs))
@david-christiansen
david-christiansen / FunErrTest.idr
Created Jan 23, 2014
Error reflection now supports specific function arguments
View FunErrTest.idr
import Language.Reflection.Errors
import Language.Reflection.Utils
%language ErrorReflection
total
cadr : (xs : List a)
-> {auto cons1 : isCons xs = True}
-> {auto cons2 : isCons (tail xs cons1) = True}
-> a
@david-christiansen
david-christiansen / gist:8336956
Created Jan 9, 2014
First reflected error in Idris
View gist:8336956
drc@drc:~/Documents/Code/Idris/error-reflection-test$ idris ErrorTest.idr
____ __ _
/ _/___/ /____(_)____
/ // __ / ___/ / ___/ Version 0.9.10.1-git:5361547
_/ // /_/ / / / (__ ) http://www.idris-lang.org/
/___/\__,_/_/ /_/____/ Type :? for help
Type checking ./ErrorTest.idr
*ErrorTest> the Nat ""
ERROR HAPPENED!
View Bugfind.idr
module Bugfind
import Language.Reflection
import Language.Reflection.Util
foo : TT
foo = Erased