david-christiansen

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

david-christiansen

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

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

#!/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

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

#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"))

david-christiansen

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

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

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 Bugfind



import Language.Reflection
import Language.Reflection.Util

foo : TT
foo = Erased