Skip to content

Instantly share code, notes, and snippets.

View msmorgan's full-sized avatar

Michael Morgan msmorgan

23 followers · 12 following
View GitHub Profile
@msmorgan
msmorgan / datediff.py
Last active May 4, 2021 23:30
from itertools import accumulate
MONTH_NAMES = ['Jan', 'Feb', 'Mar', 'Apr', 'May', 'Jun', 'Jul', 'Aug', 'Sep', 'Oct', 'Nov', 'Dec']
MONTH_LENGTHS = [31, 28, 31, 30, 31, 30, 31, 31, 30, 31, 30, 31]
MONTH_STARTS = list(accumulate([0] + MONTH_LENGTHS[:-1])) # [0, 31, 31+28, 31+28+31, ...]
def is_leap_year(year: int) -> bool:
return year % 4 == 0 and (year % 100 != 0 or year % 400 == 0)
@msmorgan
msmorgan / main.dart
Created April 25, 2020 15:49
class A {
final name = 'A';
void printName() {
print(name);
}
}
class B extends A {
@override
@msmorgan
msmorgan / main.rs
Created February 12, 2019 21:27
using typetag to do fancy stuff
use std::collections::HashSet;
use serde::{Deserialize, Serialize};
struct Context {
applications: HashSet<String>,
}
impl Context {
pub fn new() -> Self {
@msmorgan
msmorgan / counters.txt
Created November 14, 2018 19:42
All the counter types mentioned on non-silver-border Magic: The Gathering cards.
-0/-1
-0/-2
-1/-0
-1/-1
-2/-1
-2/-2
+0/+1
+0/+2
+1/+0
+1/+1
@msmorgan
msmorgan / SParser.idr
Created January 4, 2018 19:31
term : MRule Expr
term = pure $ let (x, xs) = !multChain in
foldl (Binary Mul) x xs
where
multChain : MRule (Expr, List Expr)
multChain = do x <- factor
xs <- (do let op = match (Op Mul)
op
commit
sepBy1 op factor) <|> pure []
@msmorgan
msmorgan / SParser.idr
Created January 4, 2018 19:00
module SParser
import Text.Lexer
import Text.Parser
data SParser : Type -> Type -> Bool -> Type -> Type where
MkSParser : (s -> Grammar t c (a, s)) -> SParser s t c a
Functor (SParser s t b) where
map f (MkSParser g) = MkSParser $ \s => map (\(v,s) => (f v, s)) (g s)
@msmorgan
msmorgan / Ter.idr
Created November 20, 2017 03:34
data CloserToZero : Integer -> Integer -> Type where
CTZ : So (x * x < y * y) -> CloserToZero x y
CTZInj : CloserToZero x y -> So (x * x < y * y)
CTZInj (CTZ oh) = oh
closerToZero : (x, y : Integer) -> Dec (CloserToZero x y)
closerToZero x y with (x * x < y * y) proof prf
closerToZero x y | True = Yes (CTZ (rewrite sym prf in Oh))
closerToZero x y | False = No (absurd . the (So False) . rewrite prf in CTZInj)
@msmorgan
msmorgan / ToggleList.idr
Last active November 10, 2017 06:21
module Data.ToggleList
%access public export
%default total
data Next = A | B
next : Next -> Type -> Type -> Type
next A a _ = a
next B _ b = b
@msmorgan
msmorgan / AltList.idr
Created November 10, 2017 05:48
module Data.AltList
%access public export
%default total
data AltList : (a : Type) -> (b : Type) -> Type where
Nil : AltList a b
ConsB : b -> AltList a b -> AltList a b
ConsAB : a -> b -> AltList a b -> AltList a b
@msmorgan
msmorgan / MapToken.idr
Last active November 7, 2017 00:43
module Text.Parser.Core
{-
...
-}
-- what to name this?
mapToken : (tokB -> tokA) -> Grammar tokA c a -> Grammar tokB c a
mapToken f (Empty val) = Empty val
mapToken f (Terminal g) = Terminal (g . f)