| module Graph where | |
| open import Agda.Builtin.List | |
| open import Agda.Builtin.Nat renaming (Nat to ℕ) | |
| data Fin : ℕ → Set where | |
| zero : ∀{n} → Fin (suc n) | |
| suc : ∀{n} → Fin n → Fin (suc n) | |
| len : {A : Set} → List A → ℕ |
| def run(G, n): | |
| for _ in range(n): | |
| i = len(G[0]) - 1 | |
| for j in range(len(G)): | |
| s = 0 | |
| if 0 <= j - 1: | |
| s += G[j - 1][i] | |
| if j + 1 < len(G): | |
| s += G[j + 1][i] | |
| G[j] += (s, ) |
| def obviously(v, msg=''): | |
| def outer(f): | |
| def inner(*args, **kwargs): | |
| r = f(*args, **kwargs) | |
| if not v(r): | |
| if msg: | |
| errmsg = f.__name__ + ': ' + msg | |
| else: | |
| errmsg = f.__name__ + ': obviously not true' | |
| raise Exception(errmsg) |
Keywords: logging, programming, overcast
I made a simple script for writing daily logs. This could be useful for taking notes regarding daily progress. This could have been valuable while doing my PhD. Oh well.
The weather isn't great today. Not terrible, just not great.
| import sys | |
| def openstd(file, mode='r', *args, **kwargs): | |
| if file == '-': | |
| if 'r' in mode: | |
| return sys.stdin | |
| elif any(w in mode for w in 'wxa'): | |
| return sys.stdout | |
| else: | |
| raise Exception("Mode not supported") |
| open import Agda.Primitive | |
| Pred : ∀{a} → Set a → Set _ | |
| Pred A = A → Set | |
| _∈_ : ∀{a} {A : Set a} → A → Pred A → Set | |
| x ∈ α = α x | |
| _⊂_ : ∀{a} {A : Set a} → Pred A → Pred A → Set a | |
| α ⊂ β = ∀ x → x ∈ α → x ∈ β |
| open import Agda.Builtin.Equality | |
| open import Agda.Primitive | |
| Π : ∀{a b} → (A : Set a) → (B : A → Set b) → Set (a ⊔ b) | |
| Π A B = (x : A) → B x | |
| syntax Π A (λ x → B) = Π[ x ∶ A ] B | |
| record _×_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where |
| open import Agda.Builtin.Equality public | |
| data ⊥ : Set where | |
| ¬_ : (A : Set) → Set | |
| ¬ A = A → ⊥ | |
| infix 4 _≢_ | |
| _≢_ : {A : Set} → A → A → Set | |
| x ≢ y = ¬(x ≡ y) |
| # Idea suggested by Michael Cowie | |
| import itertools | |
| class BloomHeap: | |
| def __init__(self, *values): | |
| self.tape = [] | |
| if len(values) == 1 and not isinstance(values[0], int): | |
| self += values[0] | |
| elif values: |