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

module ErrorReflectionDemo

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

%language ErrorReflection

data Col = BOOL | STRING | INT

david-christiansen

module SExpParse

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

%default total

data MessageFmt = KWD String
                | STRING

david-christiansen

module Test

import Provider

import Database
import Queries

%language TypeProviders

%link C "sqlite3api.o"

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

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

module ErrorTest

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

%language ErrorReflection

data Ty = TUnit | TFun Ty Ty

david-christiansen

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!

david-christiansen

module PreOrderReasoning


-- QED is first to get the precedence to work out. It's just refl with an explicit argument.
syntax [expr] "QED" = qed expr
-- foo ={ prf }= bar ={ prf' }= fnord QED
-- is a proof that foo is related to fnord, with the intermediate step being bar, justified by prf and prf'
syntax [from] "={" [prf] "}=" [to] = step from prf to

--These are the components for using the syntax with equality

david-christiansen

module JSON

import Data.HVect

import Control.Monad.Identity

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