david-christiansen

  %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

module Test

import Provider

import Database
import Queries

%language TypeProviders

%link C "sqlite3api.o"

david-christiansen

module SExpParse

import Lightyear.Core
import Lightyear.Combinators
import Lightyear.Strings

%default total

data MessageFmt = KWD String
                | STRING

david-christiansen

module ErrorReflectionDemo

import Language.Reflection
import Language.Reflection.Errors
import Language.Reflection.Utils

%language ErrorReflection

data Col = BOOL | STRING | INT

david-christiansen

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

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

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

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

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

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