Skip to content

Instantly share code, notes, and snippets.

Avatar
🍌
semper φ

Greg Pfeil sellout

🍌
semper φ
View GitHub Profile
View broken-scanl.idr
scanl : (b -> a -> b) -> b -> Vect n a -> Vect (S n) b
scanl f q ls = q :: (case ls of
[] => []
x::xs => scanl f (f q x) xs)
-- When elaborating left hand side of Main.case block in scanl:
-- When elaborating argument ls to Main.case block in scanl:
-- Can't unify
-- Vect 0 a
-- with
@sellout
sellout / gist:10744574
Last active Aug 29, 2015
very confused, as usual
View gist:10744574
import Data.Bits
trim : Bits (1 + n) -> Bits n
trim b = truncate b
BoundedInt : Integer -> Nat -> Type
BoundedInt min max = (x : Integer ** so (min <= x && x < toIntegerNat max))
postulate bounds : (x : Integer) -> so (lower <= x && x < toIntegerNat upper) -> so (lower <= x && 1+2*x < pow 2 upper)
@sellout
sellout / gist:11119737
Last active Aug 29, 2015
How can I define Ord for integralTy?
View gist:11119737
integralTy : (signed : Bool) -> Nat -> Type
integralTy False 0 = Bits8
integralTy False 1 = Bits16
integralTy False 2 = Bits32
integralTy False 3 = Bits64
integralTy _ _ = Integer
inRange : Ord (integralTy m n) => integralTy m n -> integralTy m n -> integralTy m n -> Bool
inRange x lower upper = lower <= x && x < upper
View gist:11242089
(defun ansi-color-insertion-filter (proc string)
(when (buffer-live-p (process-buffer proc))
(with-current-buffer (process-buffer proc)
(save-excursion
;; Insert the text, advancing the process marker.
(goto-char (process-mark proc))
(insert (ansi-color-apply string))
(set-marker (process-mark proc) (point)))
(goto-char (process-mark proc)))))
View gist:11242603
append : Bits m -> Bits n -> Bits (m + n)
append {n=n} a b = shiftLeft (cast n) (zeroExtend a) `or` zeroExtend b
View gist:11269679
(defun ansi-color-insertion-filter (proc string)
(when (buffer-live-p (process-buffer proc))
(with-current-buffer (process-buffer proc)
(save-excursion
;; Insert the text, advancing the process marker.
(goto-char (process-mark proc))
(insert (ansi-color-apply string))
(set-marker (process-mark proc) (point)))
(goto-char (process-mark proc)))))
View gist:11299585
partition : Bits (m * n) -> Vect m (Bits n)
partition {m=Z} _ = Prelude.Vect.Nil
partition {m=S m} {n=n} bits =
truncate (replace (plusCommutative n (m*n)) bits)
:: partition (truncate (shiftRightLogical (cast n) bits))
View gist:11356985
KeySize : Type
KeySize = Fin 256 -- should actually be [1-256], not [0-256]
public
ARC4Key : KeySize -> Type
ARC4Key n = Vect (finToNat n) (Mod 256) -- should be Byte, but can’t convert yet
public
data AllegedRivestCipher4 : KeySize -> Type where
ARC4 : ARC4Key n -> AllegedRivestCipher4 n
@sellout
sellout / gist:11373682
Created Apr 28, 2014
My crazy git remotes
View gist:11373682
$ git remote -v
origin git@github.com:idris-lang/Idris-dev.git (fetch)
origin git@github.com:sellout/Idris-dev.git (push)
reverse git@github.com:sellout/Idris-dev.git (fetch)
reverse git@github.com:idris-lang/Idris-dev.git (push)
View gist:11390058
confoundMessage : (StreamCipher k, Serializable i, Serializable o) =>
k -> i -> o
confoundMessage key message =
let encodedMsg = encode message
in decode (zipWith xor
(Prelude.Stream.take (length encodedMsg)
(generateKeystream key))
encodedMsg)
-- When elaborating an application of function Prelude.Vect.zipWith:
You can’t perform that action at this time.