Skip to content

Instantly share code, notes, and snippets.

Jaden Geller JadenGeller

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.