Skip to content

Instantly share code, notes, and snippets.

Avatar

David Thrane Christiansen david-christiansen

View GitHub Profile
View New proof automation
%reflection
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
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"
@david-christiansen
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
| STRING
@david-christiansen
david-christiansen / ErrorReflectionDemo.idr
Created May 1, 2014
Error reflection demo from today
View ErrorReflectionDemo.idr
module ErrorReflectionDemo
import Language.Reflection
import Language.Reflection.Errors
import Language.Reflection.Utils
%language ErrorReflection
data Col = BOOL | STRING | INT
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
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
david-christiansen / Output
Created Jun 25, 2014
Beginning of quasiquotes for proof automation
View Output
drc@drc:~/tmp$ idris Quasiquote.idr
____ __ _
/ _/___/ /____(_)____
/ // __ / ___/ / ___/ Version 0.9.13.1-git:f8ec244
_/ // /_/ / / / (__ ) http://www.idris-lang.org/
/___/\__,_/_/ /_/____/ Type :? for help
Idris is free software with ABSOLUTELY NO WARRANTY.
For details type :warranty.
Type checking ./Quasiquote.idr
@david-christiansen
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
david-christiansen / FizzBuzzC.idr
Last active Jan 25, 2018
Dependently typed FizzBuzz, now with 30% more constructive thinking
View FizzBuzzC.idr
module FizzBuzzC
%default total
-- Dependently typed FizzBuzz, constructively
-- A number is fizzy if it is evenly divisible by 3
data Fizzy : Nat -> Type where
ZeroFizzy : Fizzy 0
Fizz : Fizzy n -> Fizzy (3 + n)
@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
You can’t perform that action at this time.