Skip to content

Instantly share code, notes, and snippets.


David Thrane Christiansen david-christiansen

View GitHub Profile
david-christiansen / Test.idr
Created Feb 6, 2014
Statically checked embedded subset of SQL in Idris
View Test.idr
module Test
import Provider
import Database
import Queries
%language TypeProviders
%link C "sqlite3api.o"
View New proof automation
solveHasTable : Type -> Tactic
solveHasTable (HasTable (_::tl) name s) =
Try (Refine "Here" `Seq` Solve)
(Refine "There" `Seq` (Solve `Seq` solveHasTable (HasTable tl name s)))
solveHasTable (HasTable (a++b) _ _) = Refine "Here" `Seq` Solve
solveHasTable (HasTable _ name s) = Refine "Here" `Seq` Solve
david-christiansen / SExpParse.idr
Created Mar 25, 2014
Prototype parser for Idris's machine-readable interaction syntax
View SExpParse.idr
module SExpParse
import Lightyear.Core
import Lightyear.Combinators
import Lightyear.Strings
%default total
data MessageFmt = KWD String
View Test.idr
module Main
import System.Random.TF.Gen
genNums : Int -> TFGen -> IO TFGen
genNums i gen = if i > 0 then
let (n, gen') = tfGenNext gen in
do putStrLn (show i ++"\t0x"++show n)
genNums (i-1) (fst (split gen'))
else return gen
david-christiansen / Prov.idr
Created May 15, 2014
Compile-time QuickCheck as a type provider in Idris
View Prov.idr
import QuickCheck
import Providers
%language TypeProviders
prop_RevRev : Eq a => List a -> Bool
prop_RevRev xs = reverse (reverse xs) == xs
stupid : List a -> List a
david-christiansen / Output
Created Jun 25, 2014
Beginning of quasiquotes for proof automation
View Output
drc@drc:~/tmp$ idris Quasiquote.idr
____ __ _
/ _/___/ /____(_)____
/ // __ / ___/ / ___/ Version
_/ // /_/ / / / (__ )
/___/\__,_/_/ /_/____/ Type :? for help
Idris is free software with ABSOLUTELY NO WARRANTY.
For details type :warranty.
Type checking ./Quasiquote.idr
david-christiansen / FizzBuzz.idr
Last active Aug 29, 2015
Dependently typed FizzBuzz, about 5 years late to the party
View FizzBuzz.idr
module FizzBuzz
-- Dependently-typed FizzBuzz, about 5 years late to the party.
-- A specification of the problem. Each constructor tells the conditions
-- under which it can be applied, and the "auto" keyword means that proof
-- search will be used in the context where they are applied to fill them
-- out. For instance, applying `N` to some Nat fails unless there's a proof in
-- scope that the argument meets the criteria.
data FB : Nat -> Type where
david-christiansen / gist:a463bdb0086dab60c72b
Created Nov 4, 2014
ghc-mod error annotations as Helm data source
View gist:a463bdb0086dab60c72b
(defun helm-ghc-errors-in-buffer ()
(with-current-buffer helm-current-buffer
(remove-if-not #'(lambda (o) (overlay-get o 'ghc-check))
(overlays-in (point-min) (point-max)))))
(defun helm-ghc-describe-overlay (o)
(cl-flet ((abbreviate (str)
(if (> (length str) fill-column)
(concat (substring str 0 (- fill-column 3)) "...")
View gist:2ba5e03910666ae27203
;;; Helm support for finding my stuff
(defvar helm-david-christiansen-git-repo-list nil
"The Git repos found for my Helm launcher.")
(defvar helm-david-christiansen-git-repo-finder-process nil
"The process finding Git repos for my Helm launcher.")
(defun helm-david-christiansen-git-repo-finder-output-filter (proc string)
(when (buffer-live-p (process-buffer proc))
(with-current-buffer (process-buffer proc)
(let ((moving (= (point) (process-mark proc))))
View Snoc.idr
module Snoc
data SnocList : List a -> Type where
SnocNil : SnocList []
Snoc : (xs : List a) -> (x : a) -> SnocList (xs ++ [x])
snocList : (xs : List a) -> SnocList xs
snocList [] = SnocNil
snocList (x :: xs) with (snocList xs)
snocList (x :: []) | SnocNil = Snoc [] x
You can’t perform that action at this time.