jesyspa

// Copyright 2018 Google LLC.
// SPDX-License-Identifier: Apache-2.0
// Solution to part 2 of www.adventofcode.com/2018/day/1
#include <algorithm>
#include <cassert>
#include <iostream>
#include <iterator>
#include <unordered_map>
#include <vector>

jesyspa

module imonad where

postulate
  -- Whatever the monad is indexed over
  Ix : Set₁
  
infixr 3 _:→_
_:→_ : (Ix -> Set) -> (Ix -> Set) -> Set₁
a :→ b = ∀{x : Ix} -> a x -> b x

jesyspa

#include <iostream>
#include <vector>
#include <array>
#include <string>
#include <variant>
#include <stdexcept>
#include <iomanip>

struct StoreTag {};
struct LoadTag {};

jesyspa

#include "Application.h"
#include <string>
#include <iostream>
LRESULT CALLBACK WndProc(HWND hWnd, UINT message, WPARAM wParam, LPARAM lParam)
{
	AllocConsole();
	freopen("CONOUT$", "w", stdout);
	PAINTSTRUCT ps;
	HDC hdc;

jesyspa

/*
 * Idea: sometimes, you want a pair (a : A, B a), where the first element determines the type of the second element.
 * By the product-exponent adjunction, a map (a : A, B a) -> C is equivalent to a map (a : A) -> B a -> C.
 * Furthermore, if we perform a full double negation translation of our program, we can replace terms of type
 * (a : A, B a) with terms of type forall R. ((a : A, B a) -> R) -> R and thus with terms of type
 * forall R. ((a : A) -> B a -> R) -> R.  These are considerably easier to model in C++ than what we started with.
 *
 * We model a term x of type (a : A) -> B a -> R using a C++-term of a C++-type of the form
 *  struct x_dfun {
 *      template<A a>

jesyspa

#pragma once

#include <blaze/Blaze.h>
#include <random>

namespace bz=blaze;

namespace blazegen {
    // Generates a uniform random matrix of type T using a (P)RNG
    // of class Generator.

jesyspa

#include <chrono>
#include <cmath>
#include <iostream>

template<typename F>
auto timeit(F f) {
    int const ITERS = 1'000;
    using namespace std::chrono;
    auto b = system_clock::now();
    volatile int dummy;

jesyspa

from random import choice
from functools import cmp_to_key

# i.e. a <= b
def is_le(priorities, a, b):
    return a == b or any(is_le(priorities, c, b) for (a2, c) in priorities if a == a2)

def is_ordered(priorities, a, b):
    return is_le(priorities, a, b) or is_le(priorities, b, a)

jesyspa

#include <iostream>
 
int main() {
	std::cerr << "[C++] Launched" << std::endl;
	int total = 0;
	int tmp;
	while (std::cin >> tmp) {
		std::cerr << "[C++] Read " << tmp << std::endl;
		total += tmp;
	}

jesyspa

Mathematics is driven by curiosity, and a good question is one of the most valuable
things you can have.  With this book, we hope to give you a basic familiarity with
several fields of mathematics, and inspire you to ask your own questions about them.

Let's start with an example: suppose you have a rectangle.  Can you cut it into squares
that are all the same size?

If you're used to mathematics as it is taught at school, this might not seem like much
of a mathematical question at all; we're not calculating anything, and we're not
solving any equations.  It turns out that questions like this, where we explore what