Skip to content

Instantly share code, notes, and snippets.

Jaden Geller JadenGeller

Block or report user

Report or block JadenGeller

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
@JadenGeller
JadenGeller / rotate.py
Last active Jun 14, 2018
Rotate in place
View rotate.py
def transpose_matrix(size, matrix):
for y in range(size):
for x in range(y):
matrix[y][x], matrix[x][y] = matrix[x][y], matrix[y][x]
def flip_y_matrix(size, matrix):
for y in range(size // 2):
flip_y = size - y - 1
for x in range(size):
matrix[x][y], matrix[x][flip_y] = matrix[x][flip_y], matrix[x][y]
@JadenGeller
JadenGeller / Constructive.idr
Created Apr 27, 2018
Are constructive programs better?
View Constructive.idr
import Data.List
import Data.List.Views
import Data.Vect
import Data.Vect.Views
%default total
-- Constructive
rotate : Vect len elem -> Vect len elem
@JadenGeller
JadenGeller / checking.py
Created Apr 2, 2018
Dynamic Type Checking
View checking.py
#!/usr/bin/python
import inspect
def typeAsserting(f):
signature = inspect.signature(f)
def wrapper(*args, **kwargs):
bound_args = signature.bind(*args, **kwargs)
for name, parameter_value in bound_args.arguments.items():
expected_type = signature.parameters[name].annotation
@JadenGeller
JadenGeller / join_quoted_strs.py
Created Jan 24, 2018
A gross simple state machine
View join_quoted_strs.py
def join_quoted_strs(s):
r = ''
within_quotes = False
is_escaped = False
for c in s:
if within_quotes:
if is_escaped:
r += c
is_escaped = False
else:
View TypeDictionary.swift
private struct TypeDescriptor: Hashable, CustomStringConvertible {
private let type: Any.Type
internal init(_ type: Any.Type) {
self.type = type
}
public var hashValue: Int {
return String(describing: type).hashValue
}
public static func ==(lhs: TypeDescriptor, rhs: TypeDescriptor) -> Bool {
View Advent1.swift
public struct RotatingIterator<Base: IteratorProtocol>: Sequence, IteratorProtocol {
private var skippedElements: [Base.Element] = []
private var base: Base
internal init(_ base: Base, count: Int) {
self.base = base
for _ in 0..<count {
guard let element = self.base.next() else { break }
self.skippedElements.append(element)
}
View Advent.idr
import SignedNat
import Data.Vect
step : (Fin n, Vect n SignedNat) -> (SignedNat, Vect n SignedNat)
step (i, xs) = let delta = index i xs in
let xs' = updateAt i succ xs in
let i' = (toSignedNatNat (finToNat i)) + delta in
(i', xs')
signedNatToFin : SignedNat -> (m : Nat) -> Maybe (Fin m)
@JadenGeller
JadenGeller / SignedNat.idr
Created Dec 17, 2017
Signed Natural Numbers
View SignedNat.idr
module SignedNat
import Control.Isomorphism
%access public export
%default total
||| Signed natural numbers: unbounded, signed integers which can be pattern
||| matched.
data SignedNat : Type where
@JadenGeller
JadenGeller / captcha.idr
Created Dec 12, 2017
Advent 2017 Day 1
View captcha.idr
import Data.Vect
import Data.Vect.Views
%default total
infixl 1 &
(&) : a -> (a -> b) -> b
x & f = f x
rotate : Vect len elem -> Vect len elem
@JadenGeller
JadenGeller / LEM.idr
Last active Mar 29, 2018
Derivation of Law of the Excluded Middle from call/cc
View LEM.idr
%default total
postulate callCC : ((a -> Void) -> a) -> a
peirce : ((a -> b) -> a) -> a
peirce f = callCC (f . (void .))
notExcludedMiddleImpliesExcludedMiddle : Not (Dec p) -> Dec p
notExcludedMiddleImpliesExcludedMiddle notExcludedMiddle = No (notExcludedMiddle . Yes)
You can’t perform that action at this time.