This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module ErrorTest | |
import Language.Reflection | |
import Language.Reflection.Errors | |
import Language.Reflection.Utils | |
%language ErrorReflection | |
data Ty = TUnit | TFun Ty Ty |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module ErrorReflectionDemo | |
import Language.Reflection | |
import Language.Reflection.Errors | |
import Language.Reflection.Utils | |
%language ErrorReflection | |
data Col = BOOL | STRING | INT |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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") |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#!/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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#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")) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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! |