Skip to content

Instantly share code, notes, and snippets.

oplaxity cell

Greg Pfeil sellout

oplaxity cell
Block or report user

Report or block sellout

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
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.