Add a file to create file dependency graph

This reverts commit 5cc92d3a9d.

.gitmodules

@@ -0,0 +1,12 @@
+[submodule "code/aoc-2020"]
+	path = code/aoc-2020
+	url = https://dev.danilafe.com/Advent-of-Code/AdventOfCode-2020.git
+[submodule "code/libabacus"]
+	path = code/libabacus
+	url = https://dev.danilafe.com/Experiments/libabacus
+[submodule "themes/vanilla"]
+	path = themes/vanilla
+	url = https://dev.danilafe.com/Web-Projects/vanilla-hugo.git
+[submodule "code/server-config"]
+	path = code/server-config
+	url = https://dev.danilafe.com/Nix-Configs/server-config

analyze.rb

@@ -0,0 +1,82 @@
+require "pathname"
+require "set"
+require "json"
+
+def resolve_path(bp, p)
+  path = nil
+  if bp.start_with? "."
+    path = Pathname.new(File.join(bp, p)).cleanpath.to_s
+  elsif p.start_with? "blog/"
+    path = File.join("content", p)
+  else
+    path = File.join("content", "blog", p)
+  end
+  if File.directory? path
+    path = File.join(path, "index.md") 
+  elsif !path.end_with? ".md"
+    path += ".md"
+  end
+  path.gsub("blog/blog/", "blog/")
+end
+
+files = Set.new
+refs = {}
+ARGF.each do |file|
+  file = file.chomp
+  files << file
+  arr = refs[file] || (refs[file] = [])
+  File.open(file).read.scan(/< relref "([^"]+)" >/) do |ref|
+    ref = resolve_path(File.dirname(file), ref[0])
+    arr << ref
+    files << ref
+  end
+  arr.uniq!
+end
+
+data = {}
+id = 0
+files.each do |file|
+  id += 1
+  name = file
+  tags = []
+  group = 1
+  value = File.size(file)
+  url = file.gsub(/^content/, "https://danilafe.com").delete_suffix("/index.md").delete_suffix(".md")
+  File.readlines(file).each do |l|
+    if l =~ /^title: (.+)$/
+      name = $~[1].delete_prefix('"').delete_suffix('"')
+    elsif l =~ /^tags: (.+)$/
+      tags = $~[1].delete_prefix("[").delete_suffix("]").split(/,\s?/).map { |it| it.gsub('"', '') }
+      if tags.include? "Compilers"
+        group = 2
+      elsif tags.include? "Coq"
+        group = 3
+      elsif tags.include? "Programming Languages"
+        group = 4
+      elsif tags.include? "Haskell"
+        group = 5
+      elsif tags.include? "Crystal"
+        group = 6
+      end
+    end
+  end
+  data[file] = { :id => id, :label => name, :group => group, :tags => tags, :url => url, :value => value }
+end
+
+edges = []
+files.each do |file1|
+  # files.each do |file2|
+  #   next if file1 == file2
+  #   next unless data[file1][:tags].any? { |t| data[file2][:tags].include? t }
+  #   edges << { :from => data[file1][:id], :to => data[file2][:id] }
+  # end
+  next unless frefs = refs[file1]
+  frefs.each do |ref|
+    edges << { :from => data[file1][:id], :to => data[ref][:id] }
+  end
+end
+edges.uniq
+# edges.filter! { |e| e[:from] < e[:to] }
+
+puts ("const nodes = " + JSON.pretty_unparse(data.values) + ";")
+puts ("const edges = " + JSON.pretty_unparse(edges) + ";")

assets/scss/donate.scss

@@ -0,0 +1,56 @@
+@import "../../themes/vanilla/assets/scss/mixins.scss";
+
+.donation-methods {
+    padding: 0;
+    border: none;
+    border-spacing: 0 0.5rem;
+
+    td {
+        padding: 0;
+        overflow: hidden;
+
+        &:first-child {
+            @include bordered-block;
+            text-align: right;
+            border-right: none;
+            border-top-right-radius: 0;
+            border-bottom-right-radius: 0;
+            padding-left: 0.5em;
+            padding-right: 0.5rem;
+
+            @include below-container-width {
+                @include bordered-block;
+                text-align: center;
+                border-bottom: none;
+                border-bottom-left-radius: 0;
+                border-bottom-right-radius: 0;
+            }
+        }
+
+        &:last-child {
+            @include bordered-block;
+            border-top-left-radius: 0;
+            border-bottom-left-radius: 0;
+
+            @include below-container-width {
+                @include bordered-block;
+                border-top-left-radius: 0;
+                border-top-right-radius: 0;
+            }
+        }
+    }
+
+    tr {
+        @include below-container-width {
+            margin-bottom: 0.5rem;
+        }
+    }
+
+    code {
+        width: 100%;
+        box-sizing: border-box;
+        border: none;
+        display: inline-block;
+        padding: 0.25rem;
+    }
+}

assets/scss/gametheory.scss

@@ -0,0 +1,11 @@
+@import "variables.scss";
+@import "mixins.scss";
+
+.assumption-number {
+    font-weight: bold;
+}
+
+.assumption {
+    @include bordered-block;
+    padding: 0.8rem;
+}

code/compiler/13/CMakeLists.txt

@@ -0,0 +1,53 @@
+cmake_minimum_required(VERSION 3.1)
+project(compiler)
+
+# We want C++17 for std::optional
+set(CMAKE_CXX_STANDARD 17)
+set(CMAKE_CXX_STANDARD_REQUIRED ON)
+
+# Find all the required packages
+find_package(BISON)
+find_package(FLEX)
+find_package(LLVM REQUIRED CONFIG)
+
+# Set up the flex and bison targets
+bison_target(parser
+    ${CMAKE_CURRENT_SOURCE_DIR}/parser.y
+    ${CMAKE_CURRENT_BINARY_DIR}/parser.cpp
+    COMPILE_FLAGS "-d")
+flex_target(scanner
+    ${CMAKE_CURRENT_SOURCE_DIR}/scanner.l
+    ${CMAKE_CURRENT_BINARY_DIR}/scanner.cpp)
+add_flex_bison_dependency(scanner parser)
+
+# Find all the relevant LLVM components
+llvm_map_components_to_libnames(LLVM_LIBS core x86asmparser x86codegen)
+
+# Create compiler executable
+add_executable(compiler
+    definition.cpp definition.hpp
+    parsed_type.cpp parsed_type.hpp
+    ast.cpp ast.hpp
+    llvm_context.cpp llvm_context.hpp
+    type_env.cpp type_env.hpp
+    env.cpp env.hpp
+    type.cpp type.hpp
+    error.cpp error.hpp
+    binop.cpp binop.hpp
+    instruction.cpp instruction.hpp
+    graph.cpp graph.hpp
+    global_scope.cpp global_scope.hpp
+    parse_driver.cpp parse_driver.hpp
+    mangler.cpp mangler.hpp
+    compiler.cpp compiler.hpp
+    ${BISON_parser_OUTPUTS}
+    ${FLEX_scanner_OUTPUTS}
+    main.cpp
+)
+
+# Configure compiler executable
+target_include_directories(compiler PUBLIC ${CMAKE_CURRENT_SOURCE_DIR})
+target_include_directories(compiler PUBLIC ${CMAKE_CURRENT_BINARY_DIR})
+target_include_directories(compiler PUBLIC ${LLVM_INCLUDE_DIRS})
+target_compile_definitions(compiler PUBLIC ${LLVM_DEFINITIONS})
+target_link_libraries(compiler ${LLVM_LIBS})

code/compiler/13/ast.cpp

@@ -0,0 +1,454 @@
+#include "ast.hpp"
+#include <ostream>
+#include <type_traits>
+#include "binop.hpp"
+#include "error.hpp"
+#include "instruction.hpp"
+#include "type.hpp"
+#include "type_env.hpp"
+#include "env.hpp"
+
+static void print_indent(int n, std::ostream& to) {
+    while(n--) to << "  ";
+}
+
+void ast_int::print(int indent, std::ostream& to) const {
+    print_indent(indent, to);
+    to << "INT: " << value << std::endl;
+}
+
+void ast_int::find_free(std::set<std::string>& into) {
+
+}
+
+type_ptr ast_int::typecheck(type_mgr& mgr, type_env_ptr& env) {
+    this->env = env;
+    return type_ptr(new type_app(env->lookup_type("Int")));
+}
+
+void ast_int::translate(global_scope& scope) {
+
+}
+
+void ast_int::compile(const env_ptr& env, std::vector<instruction_ptr>& into) const {
+    into.push_back(instruction_ptr(new instruction_pushint(value)));
+}
+
+void ast_lid::print(int indent, std::ostream& to) const {
+    print_indent(indent, to);
+    to << "LID: " << id << std::endl;
+}
+
+void ast_lid::find_free(std::set<std::string>& into) {
+    into.insert(id);
+}
+
+type_ptr ast_lid::typecheck(type_mgr& mgr, type_env_ptr& env) {
+    this->env = env;
+    type_scheme_ptr lid_type = env->lookup(id);
+    if(!lid_type)
+        throw type_error("unknown identifier " + id, loc);
+    return lid_type->instantiate(mgr);
+}
+
+void ast_lid::translate(global_scope& scope) {
+
+}
+
+void ast_lid::compile(const env_ptr& env, std::vector<instruction_ptr>& into) const {
+    into.push_back(instruction_ptr(
+        (this->env->is_global(id)) ?
+            (instruction*) new instruction_pushglobal(this->env->get_mangled_name(id)) :
+            (instruction*) new instruction_push(env->get_offset(id))));
+}
+
+void ast_uid::print(int indent, std::ostream& to) const {
+    print_indent(indent, to);
+    to << "UID: " << id << std::endl;
+}
+
+void ast_uid::find_free(std::set<std::string>& into) {
+
+}
+
+type_ptr ast_uid::typecheck(type_mgr& mgr, type_env_ptr& env) {
+    this->env = env;
+    type_scheme_ptr uid_type = env->lookup(id);
+    if(!uid_type)
+        throw type_error("unknown constructor " + id, loc);
+    return uid_type->instantiate(mgr);
+}
+
+void ast_uid::translate(global_scope& scope) {
+
+}
+
+void ast_uid::compile(const env_ptr& env, std::vector<instruction_ptr>& into) const {
+    into.push_back(instruction_ptr(
+                new instruction_pushglobal(this->env->get_mangled_name(id))));
+}
+
+void ast_binop::print(int indent, std::ostream& to) const {
+    print_indent(indent, to);
+    to << "BINOP: " << op_name(op) << std::endl;
+    left->print(indent + 1, to);
+    right->print(indent + 1, to);
+}
+
+void ast_binop::find_free(std::set<std::string>& into) {
+    left->find_free(into);
+    right->find_free(into);
+}
+
+type_ptr ast_binop::typecheck(type_mgr& mgr, type_env_ptr& env) {
+    this->env = env;
+    type_ptr ltype = left->typecheck(mgr, env);
+    type_ptr rtype = right->typecheck(mgr, env);
+    type_ptr ftype = env->lookup(op_name(op))->instantiate(mgr);
+    if(!ftype) throw type_error("unknown binary operator " + op_name(op), loc);
+
+    // For better type errors, we first require binary function,
+    // and only then unify each argument. This way, we can
+    // precisely point out which argument is "wrong".
+
+    type_ptr return_type = mgr.new_type();
+    type_ptr second_type = mgr.new_type();
+    type_ptr first_type = mgr.new_type();
+    type_ptr arrow_one = type_ptr(new type_arr(second_type, return_type));
+    type_ptr arrow_two = type_ptr(new type_arr(first_type, arrow_one));
+
+    mgr.unify(ftype, arrow_two, loc);
+    mgr.unify(first_type, ltype, left->loc);
+    mgr.unify(second_type, rtype, right->loc);
+    return return_type;
+}
+
+void ast_binop::translate(global_scope& scope) {
+    left->translate(scope);
+    right->translate(scope);
+}
+
+void ast_binop::compile(const env_ptr& env, std::vector<instruction_ptr>& into) const {
+    right->compile(env, into);
+    left->compile(env_ptr(new env_offset(1, env)), into);
+
+    auto mangled_name = this->env->get_mangled_name(op_name(op));
+    into.push_back(instruction_ptr(new instruction_pushglobal(mangled_name)));
+    into.push_back(instruction_ptr(new instruction_mkapp()));
+    into.push_back(instruction_ptr(new instruction_mkapp()));
+}
+
+void ast_app::print(int indent, std::ostream& to) const {
+    print_indent(indent, to);
+    to << "APP:" << std::endl;
+    left->print(indent + 1, to);
+    right->print(indent + 1, to);
+}
+
+void ast_app::find_free(std::set<std::string>& into) {
+    left->find_free(into);
+    right->find_free(into);
+}
+
+type_ptr ast_app::typecheck(type_mgr& mgr, type_env_ptr& env) {
+    this->env = env;
+    type_ptr ltype = left->typecheck(mgr, env);
+    type_ptr rtype = right->typecheck(mgr, env);
+
+    type_ptr return_type = mgr.new_type();
+    type_ptr arrow = type_ptr(new type_arr(rtype, return_type));
+    mgr.unify(arrow, ltype, left->loc);
+    return return_type;
+}
+
+void ast_app::translate(global_scope& scope) {
+    left->translate(scope);
+    right->translate(scope);
+}
+
+void ast_app::compile(const env_ptr& env, std::vector<instruction_ptr>& into) const {
+    right->compile(env, into);
+    left->compile(env_ptr(new env_offset(1, env)), into);
+    into.push_back(instruction_ptr(new instruction_mkapp()));
+}
+
+void ast_case::print(int indent, std::ostream& to) const {
+    print_indent(indent, to);
+    to << "CASE: " << std::endl;
+    for(auto& branch : branches) {
+        print_indent(indent + 1, to);
+        branch->pat->print(to);
+        to << std::endl;
+        branch->expr->print(indent + 2, to);
+    }
+}
+
+void ast_case::find_free(std::set<std::string>& into) {
+    of->find_free(into);
+    for(auto& branch : branches) {
+        std::set<std::string> free_in_branch;
+        std::set<std::string> pattern_variables;
+        branch->pat->find_variables(pattern_variables);
+        branch->expr->find_free(free_in_branch);
+        for(auto& free : free_in_branch) {
+            if(pattern_variables.find(free) == pattern_variables.end())
+                into.insert(free);
+        }
+    }
+}
+
+type_ptr ast_case::typecheck(type_mgr& mgr, type_env_ptr& env) {
+    this->env = env;
+    type_var* var;
+    type_ptr case_type = mgr.resolve(of->typecheck(mgr, env), var);
+    type_ptr branch_type = mgr.new_type();
+
+    for(auto& branch : branches) {
+        type_env_ptr new_env = type_scope(env);
+        branch->pat->typecheck(case_type, mgr, new_env);
+        type_ptr curr_branch_type = branch->expr->typecheck(mgr, new_env);
+        mgr.unify(curr_branch_type, branch_type, branch->expr->loc);
+    }
+
+    input_type = mgr.resolve(case_type, var);
+    type_app* app_type;
+    if(!(app_type = dynamic_cast<type_app*>(input_type.get())) ||
+            !dynamic_cast<type_data*>(app_type->constructor.get())) {
+        throw type_error("attempting case analysis of non-data type");
+    }
+
+    return branch_type;
+}
+
+void ast_case::translate(global_scope& scope) {
+    of->translate(scope);
+    for(auto& branch : branches) {
+        branch->expr->translate(scope);
+    }
+}
+
+void ast_case::compile(const env_ptr& env, std::vector<instruction_ptr>& into) const {
+    type_app* app_type = dynamic_cast<type_app*>(input_type.get());
+    type_data* type = dynamic_cast<type_data*>(app_type->constructor.get());
+
+    of->compile(env, into);
+    into.push_back(instruction_ptr(new instruction_eval()));
+
+    instruction_jump* jump_instruction = new instruction_jump();
+    into.push_back(instruction_ptr(jump_instruction));
+    for(auto& branch : branches) {
+        std::vector<instruction_ptr> branch_instructions;
+        pattern_var* vpat;
+        pattern_constr* cpat;
+
+        if((vpat = dynamic_cast<pattern_var*>(branch->pat.get()))) {
+            branch->expr->compile(env_ptr(new env_offset(1, env)), branch_instructions);
+
+            for(auto& constr_pair : type->constructors) {
+                if(jump_instruction->tag_mappings.find(constr_pair.second.tag) !=
+                        jump_instruction->tag_mappings.end())
+                    break;
+
+                jump_instruction->tag_mappings[constr_pair.second.tag] =
+                    jump_instruction->branches.size();
+            }
+            jump_instruction->branches.push_back(std::move(branch_instructions));
+        } else if((cpat = dynamic_cast<pattern_constr*>(branch->pat.get()))) {
+            env_ptr new_env = env;
+            for(auto it = cpat->params.rbegin(); it != cpat->params.rend(); it++) {
+                new_env = env_ptr(new env_var(*it, new_env));
+            }
+
+            branch_instructions.push_back(instruction_ptr(new instruction_split(
+                            cpat->params.size())));
+            branch->expr->compile(new_env, branch_instructions);
+            branch_instructions.push_back(instruction_ptr(new instruction_slide(
+                            cpat->params.size())));
+
+            int new_tag = type->constructors[cpat->constr].tag;
+            if(jump_instruction->tag_mappings.find(new_tag) !=
+                    jump_instruction->tag_mappings.end())
+                throw type_error("technically not a type error: duplicate pattern");
+
+            jump_instruction->tag_mappings[new_tag] =
+                jump_instruction->branches.size();
+            jump_instruction->branches.push_back(std::move(branch_instructions));
+        }
+    }
+
+    for(auto& constr_pair : type->constructors) {
+        if(jump_instruction->tag_mappings.find(constr_pair.second.tag) ==
+                jump_instruction->tag_mappings.end())
+            throw type_error("non-total pattern");
+    }
+}
+
+void ast_let::print(int indent, std::ostream& to) const {
+    print_indent(indent, to);
+    to << "LET: " << std::endl;
+    in->print(indent + 1, to);
+}
+
+void ast_let::find_free(std::set<std::string>& into) {
+    definitions.find_free(into);
+    std::set<std::string> all_free;
+    in->find_free(all_free);
+    for(auto& free_var : all_free) {
+        if(definitions.defs_defn.find(free_var) == definitions.defs_defn.end())
+            into.insert(free_var);
+    }
+}
+
+type_ptr ast_let::typecheck(type_mgr& mgr, type_env_ptr& env) {
+    this->env = env;
+    definitions.typecheck(mgr, env);
+    return in->typecheck(mgr, definitions.env);
+}
+
+void ast_let::translate(global_scope& scope) {
+    for(auto& def : definitions.defs_data) {
+        def.second->into_globals(scope);
+    }
+    for(auto& def : definitions.defs_defn) {
+        size_t original_params = def.second->params.size();
+        std::string original_name = def.second->name;
+        auto& global_definition = def.second->into_global(scope);
+        size_t captured = global_definition.params.size() - original_params;
+
+        type_env_ptr mangled_env = type_scope(env);
+        mangled_env->bind(def.first, env->lookup(def.first), visibility::global);
+        mangled_env->set_mangled_name(def.first, global_definition.name);
+
+        ast_ptr global_app(new ast_lid(original_name));
+        global_app->env = mangled_env;
+        for(auto& param : global_definition.params) {
+            if(!(captured--)) break;
+            ast_ptr new_arg(new ast_lid(param));
+            new_arg->env = env;
+            global_app = ast_ptr(new ast_app(std::move(global_app), std::move(new_arg)));
+            global_app->env = env;
+        }
+        translated_definitions.push_back({ def.first, std::move(global_app) });
+    }
+    in->translate(scope);
+}
+
+void ast_let::compile(const env_ptr& env, std::vector<instruction_ptr>& into) const {
+    into.push_back(instruction_ptr(new instruction_alloc(translated_definitions.size())));
+    env_ptr new_env = env;
+    for(auto& def : translated_definitions) {
+        new_env = env_ptr(new env_var(def.first, std::move(new_env)));
+    }
+    int offset = translated_definitions.size() - 1;
+    for(auto& def : translated_definitions) {
+        def.second->compile(new_env, into);
+        into.push_back(instruction_ptr(new instruction_update(offset--)));
+    }
+    in->compile(new_env, into);
+    into.push_back(instruction_ptr(new instruction_slide(translated_definitions.size())));
+}
+
+void ast_lambda::print(int indent, std::ostream&  to) const {
+    print_indent(indent, to);
+    to << "LAMBDA";
+    for(auto& param : params) {
+        to << " " << param;
+    }
+    to << std::endl;
+    body->print(indent+1, to);
+}
+
+void ast_lambda::find_free(std::set<std::string>& into) {
+    body->find_free(free_variables);
+    for(auto& param : params) {
+        free_variables.erase(param);
+    }
+    into.insert(free_variables.begin(), free_variables.end());
+}
+
+type_ptr ast_lambda::typecheck(type_mgr& mgr, type_env_ptr& env) {
+    this->env = env;
+    var_env = type_scope(env);
+    type_ptr return_type = mgr.new_type();
+    type_ptr full_type = return_type;
+
+    for(auto it = params.rbegin(); it != params.rend(); it++) {
+        type_ptr param_type = mgr.new_type();
+        var_env->bind(*it, param_type);
+        full_type = type_ptr(new type_arr(std::move(param_type), full_type));
+    }
+
+    mgr.unify(return_type, body->typecheck(mgr, var_env), body->loc);
+    return full_type;
+}
+
+void ast_lambda::translate(global_scope& scope) {
+    std::vector<std::string> function_params;
+    for(auto& free_variable : free_variables) {
+        if(env->is_global(free_variable)) continue;
+        function_params.push_back(free_variable);
+    }
+    size_t captured_count = function_params.size();
+    function_params.insert(function_params.end(), params.begin(), params.end());
+
+    auto& new_function = scope.add_function("lambda", std::move(function_params), std::move(body));
+    type_env_ptr mangled_env = type_scope(env);
+    mangled_env->bind("lambda", type_scheme_ptr(nullptr), visibility::global);
+    mangled_env->set_mangled_name("lambda", new_function.name);
+    ast_ptr new_application = ast_ptr(new ast_lid("lambda"));
+    new_application->env = mangled_env;
+
+    for(auto& param : new_function.params) {
+        if(!(captured_count--)) break;
+        ast_ptr new_arg = ast_ptr(new ast_lid(param));
+        new_arg->env = env;
+        new_application = ast_ptr(new ast_app(std::move(new_application), std::move(new_arg)));
+        new_application->env = env;
+    }
+    translated = std::move(new_application);
+}
+
+void ast_lambda::compile(const env_ptr& env, std::vector<instruction_ptr>& into) const {
+    translated->compile(env, into);
+}
+
+void pattern_var::print(std::ostream& to) const {
+    to << var;
+}
+
+void pattern_var::find_variables(std::set<std::string>& into) const {
+    into.insert(var);
+}
+
+void pattern_var::typecheck(type_ptr t, type_mgr& mgr, type_env_ptr& env) const {
+    env->bind(var, t);
+}
+
+void pattern_constr::print(std::ostream& to) const {
+    to << constr;
+    for(auto& param : params) {
+        to << " " << param;
+    }
+}
+
+void pattern_constr::find_variables(std::set<std::string>& into) const {
+    into.insert(params.begin(), params.end());
+}
+
+void pattern_constr::typecheck(type_ptr t, type_mgr& mgr, type_env_ptr& env) const {
+    type_scheme_ptr constructor_type_scheme = env->lookup(constr);
+    if(!constructor_type_scheme) {
+        throw type_error("pattern using unknown constructor " + constr, loc);
+    }
+    type_ptr constructor_type = constructor_type_scheme->instantiate(mgr);
+
+    for(auto& param : params) {
+        type_arr* arr = dynamic_cast<type_arr*>(constructor_type.get());
+        if(!arr) throw type_error("too many parameters in constructor pattern", loc);
+
+        env->bind(param, arr->left);
+        constructor_type = arr->right;
+    }
+
+    mgr.unify(t, constructor_type, loc);
+}

code/compiler/13/ast.hpp

@@ -0,0 +1,195 @@
+#pragma once
+#include <memory>
+#include <vector>
+#include <set>
+#include "type.hpp"
+#include "type_env.hpp"
+#include "binop.hpp"
+#include "instruction.hpp"
+#include "env.hpp"
+#include "definition.hpp"
+#include "location.hh"
+#include "global_scope.hpp"
+
+struct ast {
+    type_env_ptr env;
+    yy::location loc;
+
+    ast(yy::location l) : env(nullptr), loc(std::move(l)) {}
+    virtual ~ast() = default;
+
+    virtual void print(int indent, std::ostream& to) const = 0;
+    virtual void find_free(std::set<std::string>& into) = 0;
+    virtual type_ptr typecheck(type_mgr& mgr, type_env_ptr& env) = 0;
+    virtual void translate(global_scope& scope) = 0;
+    virtual void compile(const env_ptr& env,
+        std::vector<instruction_ptr>& into) const = 0;
+};
+
+using ast_ptr = std::unique_ptr<ast>;
+
+struct pattern {
+    yy::location loc;
+
+    pattern(yy::location l) : loc(std::move(l)) {}
+    virtual ~pattern() = default;
+
+    virtual void print(std::ostream& to) const = 0;
+    virtual void find_variables(std::set<std::string>& into) const = 0;
+    virtual void typecheck(type_ptr t, type_mgr& mgr, type_env_ptr& env) const = 0;
+};
+
+using pattern_ptr = std::unique_ptr<pattern>;
+
+struct branch {
+    pattern_ptr pat;
+    ast_ptr expr;
+
+    branch(pattern_ptr p, ast_ptr a)
+        : pat(std::move(p)), expr(std::move(a)) {}
+};
+
+using branch_ptr = std::unique_ptr<branch>;
+
+struct ast_int : public ast {
+    int value;
+
+    explicit ast_int(int v, yy::location l = yy::location())
+        : ast(std::move(l)), value(v) {}
+
+    void print(int indent, std::ostream& to) const;
+    void find_free(std::set<std::string>& into);
+    type_ptr typecheck(type_mgr& mgr, type_env_ptr& env);
+    void translate(global_scope& scope);
+    void compile(const env_ptr& env, std::vector<instruction_ptr>& into) const;
+};
+
+struct ast_lid : public ast {
+    std::string id;
+
+    explicit ast_lid(std::string i, yy::location l = yy::location())
+        : ast(std::move(l)), id(std::move(i)) {}
+
+    void print(int indent, std::ostream& to) const;
+    void find_free(std::set<std::string>& into);
+    type_ptr typecheck(type_mgr& mgr, type_env_ptr& env);
+    void translate(global_scope& scope);
+    void compile(const env_ptr& env, std::vector<instruction_ptr>& into) const;
+};
+
+struct ast_uid : public ast {
+    std::string id;
+
+    explicit ast_uid(std::string i, yy::location l = yy::location())
+        : ast(std::move(l)), id(std::move(i)) {}
+
+    void print(int indent, std::ostream& to) const;
+    void find_free(std::set<std::string>& into);
+    type_ptr typecheck(type_mgr& mgr, type_env_ptr& env);
+    void translate(global_scope& scope);
+    void compile(const env_ptr& env, std::vector<instruction_ptr>& into) const;
+};
+
+struct ast_binop : public ast {
+    binop op;  
+    ast_ptr left;
+    ast_ptr right;
+
+    ast_binop(binop o, ast_ptr l, ast_ptr r, yy::location lc = yy::location())
+        : ast(std::move(lc)), op(o), left(std::move(l)), right(std::move(r)) {}
+
+    void print(int indent, std::ostream& to) const;
+    void find_free(std::set<std::string>& into);
+    type_ptr typecheck(type_mgr& mgr, type_env_ptr& env);
+    void translate(global_scope& scope);
+    void compile(const env_ptr& env, std::vector<instruction_ptr>& into) const;
+};
+
+struct ast_app : public ast {
+    ast_ptr left;
+    ast_ptr right;
+
+    ast_app(ast_ptr l, ast_ptr r, yy::location lc = yy::location())
+        : ast(std::move(lc)), left(std::move(l)), right(std::move(r)) {}
+
+    void print(int indent, std::ostream& to) const;
+    void find_free(std::set<std::string>& into);
+    type_ptr typecheck(type_mgr& mgr, type_env_ptr& env);
+    void translate(global_scope& scope);
+    void compile(const env_ptr& env, std::vector<instruction_ptr>& into) const;
+};
+
+struct ast_case : public ast {
+    ast_ptr of;
+    type_ptr input_type;
+    std::vector<branch_ptr> branches;
+
+    ast_case(ast_ptr o, std::vector<branch_ptr> b, yy::location l = yy::location())
+        : ast(std::move(l)), of(std::move(o)), branches(std::move(b)) {}
+
+    void print(int indent, std::ostream& to) const;
+    void find_free(std::set<std::string>& into);
+    type_ptr typecheck(type_mgr& mgr, type_env_ptr& env);
+    void translate(global_scope& scope);
+    void compile(const env_ptr& env, std::vector<instruction_ptr>& into) const;
+};
+
+struct ast_let : public ast {
+    using basic_definition = std::pair<std::string, ast_ptr>;
+
+    definition_group definitions;
+    ast_ptr in;
+
+    std::vector<basic_definition> translated_definitions;
+
+    ast_let(definition_group g, ast_ptr i, yy::location l = yy::location())
+        : ast(std::move(l)), definitions(std::move(g)), in(std::move(i)) {}
+
+    void print(int indent, std::ostream& to) const;
+    void find_free(std::set<std::string>& into);
+    type_ptr typecheck(type_mgr& mgr, type_env_ptr& env);
+    void translate(global_scope& scope);
+    void compile(const env_ptr& env, std::vector<instruction_ptr>& into) const;
+};
+
+struct ast_lambda : public ast {
+    std::vector<std::string> params;
+    ast_ptr body;
+
+    type_env_ptr var_env;
+
+    std::set<std::string> free_variables;
+    ast_ptr translated;
+
+    ast_lambda(std::vector<std::string> ps, ast_ptr b, yy::location l = yy::location())
+        : ast(std::move(l)), params(std::move(ps)), body(std::move(b)) {}
+
+    void print(int indent, std::ostream& to) const;
+    void find_free(std::set<std::string>& into);
+    type_ptr typecheck(type_mgr& mgr, type_env_ptr& env);
+    void translate(global_scope& scope);
+    void compile(const env_ptr& env, std::vector<instruction_ptr>& into) const;
+};
+
+struct pattern_var : public pattern {
+    std::string var;
+
+    pattern_var(std::string v, yy::location l = yy::location())
+        : pattern(std::move(l)), var(std::move(v)) {}
+
+    void print(std::ostream &to) const;
+    void find_variables(std::set<std::string>& into) const;
+    void typecheck(type_ptr t, type_mgr& mgr, type_env_ptr& env) const;
+};
+
+struct pattern_constr : public pattern {
+    std::string constr;
+    std::vector<std::string> params;
+
+    pattern_constr(std::string c, std::vector<std::string> p, yy::location l = yy::location())
+        : pattern(std::move(l)), constr(std::move(c)), params(std::move(p)) {}
+
+    void print(std::ostream &to) const;
+    void find_variables(std::set<std::string>& into) const;
+    virtual void typecheck(type_ptr t, type_mgr& mgr, type_env_ptr& env) const;
+};

code/compiler/13/binop.cpp

@@ -0,0 +1,21 @@
+#include "binop.hpp"
+
+std::string op_name(binop op) {
+    switch(op) {
+        case PLUS: return "+";
+        case MINUS: return "-";
+        case TIMES: return "*";
+        case DIVIDE: return "/";
+    }
+    return "??";
+}
+
+std::string op_action(binop op) {
+    switch(op) {
+        case PLUS: return "plus";
+        case MINUS: return "minus";
+        case TIMES: return "times";
+        case DIVIDE: return "divide";
+    }
+    return "??";
+}

code/compiler/13/binop.hpp

@@ -0,0 +1,17 @@
+#pragma once
+#include <array>
+#include <string>
+
+enum binop {
+    PLUS,
+    MINUS,
+    TIMES,
+    DIVIDE
+};
+
+constexpr binop all_binops[] = {
+    PLUS, MINUS, TIMES, DIVIDE
+};
+
+std::string op_name(binop op);
+std::string op_action(binop op);

code/compiler/13/compiler.cpp

@@ -0,0 +1,153 @@
+#include "compiler.hpp"
+#include "binop.hpp"
+#include "error.hpp"
+#include "global_scope.hpp"
+#include "parse_driver.hpp"
+#include "type.hpp"
+#include "type_env.hpp"
+
+#include "llvm/IR/LegacyPassManager.h"
+#include "llvm/IR/Verifier.h"
+#include "llvm/Support/TargetSelect.h"
+#include "llvm/Support/TargetRegistry.h"
+#include "llvm/Support/raw_ostream.h"
+#include "llvm/Support/FileSystem.h"
+#include "llvm/Target/TargetOptions.h"
+#include "llvm/Target/TargetMachine.h"
+
+void compiler::add_default_types() {
+    global_env->bind_type("Int", type_ptr(new type_base("Int")));
+}
+
+void compiler::add_binop_type(binop op, type_ptr type) {
+    auto name = mng.new_mangled_name(op_action(op));
+    global_env->bind(op_name(op), std::move(type), visibility::global);
+    global_env->set_mangled_name(op_name(op), name);
+}
+
+void compiler::add_default_function_types() {
+    type_ptr int_type = global_env->lookup_type("Int");
+    assert(int_type != nullptr);
+    type_ptr int_type_app = type_ptr(new type_app(int_type));
+
+    type_ptr closed_int_op_type(
+            new type_arr(int_type_app, type_ptr(new type_arr(int_type_app, int_type_app))));
+
+    constexpr binop closed_ops[] = { PLUS, MINUS, TIMES, DIVIDE };
+    for(auto& op : closed_ops) add_binop_type(op, closed_int_op_type);
+}
+
+void compiler::parse() {
+    if(!driver())
+        throw compiler_error("failed to open file");
+}
+
+void compiler::typecheck() {
+    std::set<std::string> free_variables;
+    global_defs.find_free(free_variables);
+    global_defs.typecheck(type_m, global_env);
+}
+
+void compiler::translate() {
+    for(auto& data : global_defs.defs_data) {
+        data.second->into_globals(global_scp);
+    }
+    for(auto& defn : global_defs.defs_defn) {
+        auto& function = defn.second->into_global(global_scp);
+        defn.second->env->set_mangled_name(defn.first, function.name);
+    }
+}
+
+void compiler::compile() {
+    global_scp.compile();
+}
+
+void compiler::create_llvm_binop(binop op) {
+    auto new_function =
+        ctx.create_custom_function(global_env->get_mangled_name(op_name(op)), 2);
+    std::vector<instruction_ptr> instructions;
+    instructions.push_back(instruction_ptr(new instruction_push(1)));
+    instructions.push_back(instruction_ptr(new instruction_eval()));
+    instructions.push_back(instruction_ptr(new instruction_push(1)));
+    instructions.push_back(instruction_ptr(new instruction_eval()));
+    instructions.push_back(instruction_ptr(new instruction_binop(op)));
+    instructions.push_back(instruction_ptr(new instruction_update(2)));
+    instructions.push_back(instruction_ptr(new instruction_pop(2)));
+    ctx.get_builder().SetInsertPoint(&new_function->getEntryBlock());
+    for(auto& instruction : instructions) {
+        instruction->gen_llvm(ctx, new_function);
+    }
+    ctx.get_builder().CreateRetVoid();
+}
+
+void compiler::generate_llvm() {
+    for(auto op : all_binops) {
+        create_llvm_binop(op);
+    }
+
+    global_scp.generate_llvm(ctx);
+}
+
+void compiler::output_llvm(const std::string& into) {
+    std::string targetTriple = llvm::sys::getDefaultTargetTriple();
+
+    llvm::InitializeNativeTarget();
+    llvm::InitializeNativeTargetAsmParser();
+    llvm::InitializeNativeTargetAsmPrinter();
+
+    std::string error;
+    const llvm::Target* target =
+        llvm::TargetRegistry::lookupTarget(targetTriple, error);
+    if (!target) {
+        std::cerr << error << std::endl;
+    } else {
+        std::string cpu = "generic";
+        std::string features = "";
+        llvm::TargetOptions options;
+        std::unique_ptr<llvm::TargetMachine> targetMachine(
+                target->createTargetMachine(targetTriple, cpu, features,
+                    options, llvm::Optional<llvm::Reloc::Model>()));
+
+        ctx.get_module().setDataLayout(targetMachine->createDataLayout());
+        ctx.get_module().setTargetTriple(targetTriple);
+
+        std::error_code ec;
+        llvm::raw_fd_ostream file(into, ec, llvm::sys::fs::F_None);
+        if (ec) {
+            throw compiler_error("failed to open object file for writing");
+        } else {
+            llvm::CodeGenFileType type = llvm::CGFT_ObjectFile;
+            llvm::legacy::PassManager pm;
+            if (targetMachine->addPassesToEmitFile(pm, file, NULL, type)) {
+                throw compiler_error("failed to add passes to pass manager");
+            } else {
+                pm.run(ctx.get_module());
+                file.close();
+            }
+        }
+    }
+}
+
+compiler::compiler(const std::string& filename)
+    : file_m(), global_defs(), driver(file_m, global_defs, filename),
+      global_env(new type_env), type_m(), mng(), global_scp(mng), ctx() {
+    add_default_types();
+    add_default_function_types();
+}
+
+void compiler::operator()(const std::string& into) {
+    parse();
+    typecheck();
+    translate();
+    compile();
+    generate_llvm();
+    output_llvm(into);
+}
+
+file_mgr& compiler::get_file_manager() {
+    return file_m;
+}
+
+type_mgr& compiler::get_type_manager() {
+    return type_m;
+}

code/compiler/13/compiler.hpp

@@ -0,0 +1,37 @@
+#pragma once
+#include "binop.hpp"
+#include "parse_driver.hpp" 
+#include "definition.hpp" 
+#include "type_env.hpp" 
+#include "type.hpp"
+#include "global_scope.hpp"
+#include "mangler.hpp" 
+#include "llvm_context.hpp"
+
+class compiler {
+    private:
+        file_mgr file_m;
+        definition_group global_defs;
+        parse_driver driver;
+        type_env_ptr global_env;
+        type_mgr type_m;
+        mangler mng;
+        global_scope global_scp;
+        llvm_context ctx;
+
+        void add_default_types();
+        void add_binop_type(binop op, type_ptr type);
+        void add_default_function_types();
+        void parse();
+        void typecheck();
+        void translate();
+        void compile();
+        void create_llvm_binop(binop op);
+        void generate_llvm();
+        void output_llvm(const std::string& into);
+    public:
+        compiler(const std::string& filename);
+        void operator()(const std::string& into);
+        file_mgr& get_file_manager();
+        type_mgr& get_type_manager();
+};

code/compiler/13/definition.cpp

@@ -0,0 +1,148 @@
+#include "definition.hpp"
+#include <cassert>
+#include "error.hpp"
+#include "ast.hpp"
+#include "instruction.hpp"
+#include "llvm_context.hpp"
+#include "type.hpp"
+#include "type_env.hpp"
+#include "graph.hpp"
+#include <llvm/IR/DerivedTypes.h>
+#include <llvm/IR/Function.h>
+#include <llvm/IR/Type.h>
+
+void definition_defn::find_free() {
+    body->find_free(free_variables);
+    for(auto& param : params) {
+        free_variables.erase(param);
+    }
+}
+
+void definition_defn::insert_types(type_mgr& mgr, type_env_ptr& env, visibility v) {
+    this->env = env;
+    var_env = type_scope(env);
+    return_type = mgr.new_type();
+    full_type = return_type;
+
+    for(auto it = params.rbegin(); it != params.rend(); it++) {
+        type_ptr param_type = mgr.new_type();
+        full_type = type_ptr(new type_arr(param_type, full_type));
+        var_env->bind(*it, param_type);
+    }
+    env->bind(name, full_type, v);
+}
+
+void definition_defn::typecheck(type_mgr& mgr) {
+    type_ptr body_type = body->typecheck(mgr, var_env);
+    mgr.unify(return_type, body_type);
+}
+
+
+global_function& definition_defn::into_global(global_scope& scope) {
+    std::vector<std::string> all_params;
+    for(auto& free : free_variables) {
+        if(env->is_global(free)) continue;
+        all_params.push_back(free);
+    }
+    all_params.insert(all_params.end(), params.begin(), params.end());
+    body->translate(scope);
+    return scope.add_function(name, std::move(all_params), std::move(body));
+}
+
+void definition_data::insert_types(type_env_ptr& env) {
+    this->env = env;
+    env->bind_type(name, type_ptr(new type_data(name, vars.size())));
+}
+
+void definition_data::insert_constructors() const {
+    type_ptr this_type_ptr = env->lookup_type(name);
+    type_data* this_type = static_cast<type_data*>(this_type_ptr.get());
+    int next_tag = 0;
+
+    std::set<std::string> var_set;
+    type_app* return_app = new type_app(std::move(this_type_ptr));
+    type_ptr return_type(return_app);
+    for(auto& var : vars) {
+        if(var_set.find(var) != var_set.end())
+            throw compiler_error(
+                    "type variable " + var +
+                    " used twice in data type definition.", loc);
+        var_set.insert(var);
+        return_app->arguments.push_back(type_ptr(new type_var(var)));
+    }
+
+    for(auto& constructor : constructors) {
+        constructor->tag = next_tag;
+        this_type->constructors[constructor->name] = { next_tag++ };
+
+        type_ptr full_type = return_type;
+        for(auto it = constructor->types.rbegin(); it != constructor->types.rend(); it++) {
+            type_ptr type = (*it)->to_type(var_set, env);
+            full_type = type_ptr(new type_arr(type, full_type));
+        }
+
+        type_scheme_ptr full_scheme(new type_scheme(std::move(full_type)));
+        full_scheme->forall.insert(full_scheme->forall.begin(), vars.begin(), vars.end());
+        env->bind(constructor->name, full_scheme, visibility::global);
+    }
+}
+
+void definition_data::into_globals(global_scope& scope) {
+    for(auto& constructor : constructors) {
+        global_constructor& c = scope.add_constructor(
+                constructor->name, constructor->tag, constructor->types.size());
+        env->set_mangled_name(constructor->name, c.name);
+    }
+}
+
+void definition_group::find_free(std::set<std::string>& into) {
+    for(auto& def_pair : defs_defn) {
+        def_pair.second->find_free();
+        for(auto& free_var : def_pair.second->free_variables) {
+            if(defs_defn.find(free_var) == defs_defn.end()) {
+                into.insert(free_var);
+            } else {
+                def_pair.second->nearby_variables.insert(free_var);
+            }
+        }
+    }
+}
+
+void definition_group::typecheck(type_mgr& mgr, type_env_ptr& env) {
+    this->env = type_scope(env);
+
+    for(auto& def_data : defs_data) {
+        def_data.second->insert_types(this->env);
+    }
+    for(auto& def_data : defs_data) {
+        def_data.second->insert_constructors();
+    }
+
+    function_graph dependency_graph;
+
+    for(auto& def_defn : defs_defn) {
+        def_defn.second->find_free();
+        dependency_graph.add_function(def_defn.second->name);
+
+        for(auto& dependency : def_defn.second->nearby_variables) {
+            assert(defs_defn.find(dependency) != defs_defn.end());
+            dependency_graph.add_edge(def_defn.second->name, dependency);
+        }
+    }
+
+    std::vector<group_ptr> groups = dependency_graph.compute_order();
+    for(auto it = groups.rbegin(); it != groups.rend(); it++) {
+        auto& group = *it;
+        for(auto& def_defnn_name : group->members) {
+            auto& def_defn = defs_defn.find(def_defnn_name)->second;
+            def_defn->insert_types(mgr, this->env, vis);
+        }
+        for(auto& def_defnn_name : group->members) {
+            auto& def_defn = defs_defn.find(def_defnn_name)->second;
+            def_defn->typecheck(mgr);
+        }
+        for(auto& def_defnn_name : group->members) {
+            this->env->generalize(def_defnn_name, *group, mgr);
+        }
+    }
+}

code/compiler/13/definition.hpp

@@ -0,0 +1,91 @@
+#pragma once
+#include <memory>
+#include <vector>
+#include <map>
+#include <set>
+#include "instruction.hpp"
+#include "llvm_context.hpp"
+#include "parsed_type.hpp"
+#include "type_env.hpp"
+#include "location.hh"
+#include "global_scope.hpp"
+
+struct ast;
+using ast_ptr = std::unique_ptr<ast>;
+
+struct constructor {
+    std::string name;
+    std::vector<parsed_type_ptr> types;
+    int8_t tag;
+
+    constructor(std::string n, std::vector<parsed_type_ptr> ts)
+        : name(std::move(n)), types(std::move(ts)) {}
+};
+
+using constructor_ptr = std::unique_ptr<constructor>;
+
+struct definition_defn {
+    std::string name;
+    std::vector<std::string> params;
+    ast_ptr body;
+    yy::location loc;
+
+    type_env_ptr env;
+    type_env_ptr var_env;
+    std::set<std::string> free_variables;
+    std::set<std::string> nearby_variables;
+    type_ptr full_type;
+    type_ptr return_type;
+
+    definition_defn(
+            std::string n,
+            std::vector<std::string> p,
+            ast_ptr b,
+            yy::location l = yy::location())
+        : name(std::move(n)), params(std::move(p)), body(std::move(b)), loc(std::move(l)) {
+
+    }
+
+    void find_free();
+    void insert_types(type_mgr& mgr, type_env_ptr& env, visibility v);
+    void typecheck(type_mgr& mgr);
+
+    global_function& into_global(global_scope& scope);
+};
+
+using definition_defn_ptr = std::unique_ptr<definition_defn>;
+
+struct definition_data {
+    std::string name;
+    std::vector<std::string> vars;
+    std::vector<constructor_ptr> constructors;
+    yy::location loc;
+
+    type_env_ptr env;
+
+    definition_data(
+            std::string n,
+            std::vector<std::string> vs,
+            std::vector<constructor_ptr> cs,
+            yy::location l = yy::location())
+        : name(std::move(n)), vars(std::move(vs)), constructors(std::move(cs)), loc(std::move(l)) {}
+
+    void insert_types(type_env_ptr& env);
+    void insert_constructors() const;
+
+    void into_globals(global_scope& scope);
+};
+
+using definition_data_ptr = std::unique_ptr<definition_data>;
+
+struct definition_group {
+    std::map<std::string, definition_data_ptr> defs_data;
+    std::map<std::string, definition_defn_ptr> defs_defn;
+    visibility vis;
+    type_env_ptr env;
+
+    definition_group(visibility v = visibility::local) : vis(v) {}
+
+    void find_free(std::set<std::string>& into);
+    void typecheck(type_mgr& mgr, type_env_ptr& env);
+};

code/compiler/13/env.cpp

@@ -0,0 +1,24 @@
+#include "env.hpp"
+#include <cassert>
+
+int env_var::get_offset(const std::string& name) const {
+    if(name == this->name) return 0;
+    assert(parent != nullptr);
+    return parent->get_offset(name) + 1;
+}
+
+bool env_var::has_variable(const std::string& name) const {
+    if(name == this->name) return true;
+    if(parent) return parent->has_variable(name);
+    return false;
+}
+
+int env_offset::get_offset(const std::string& name) const {
+    assert(parent != nullptr);
+    return parent->get_offset(name) + offset;
+}
+
+bool env_offset::has_variable(const std::string& name) const {
+    if(parent) return parent->has_variable(name);
+    return false;
+}

code/compiler/13/env.hpp

@@ -0,0 +1,39 @@
+#pragma once
+#include <memory>
+#include <string>
+
+class env {
+    public:
+        virtual ~env() = default;
+
+        virtual int get_offset(const std::string& name) const = 0;
+        virtual bool has_variable(const std::string& name) const = 0;
+};
+
+using env_ptr = std::shared_ptr<env>;
+
+class env_var : public env {
+    private:
+        std::string name;
+        env_ptr parent;
+
+    public:
+        env_var(std::string n, env_ptr p)
+            : name(std::move(n)), parent(std::move(p)) {}
+
+        int get_offset(const std::string& name) const;
+        bool has_variable(const std::string& name) const;
+};
+
+class env_offset : public env {
+    private:
+        int offset;
+        env_ptr parent;
+
+    public:
+        env_offset(int o, env_ptr p)
+            : offset(o), parent(std::move(p)) {}
+
+        int get_offset(const std::string& name) const;
+        bool has_variable(const std::string& name) const;
+};

code/compiler/13/error.cpp

@@ -0,0 +1,41 @@
+#include "error.hpp"
+
+const char* compiler_error::what() const noexcept {
+    return "an error occured while compiling the program";
+}
+
+void compiler_error::print_about(std::ostream& to) {
+    to << what() << ": ";
+    to << description << std::endl;
+}
+
+void compiler_error::print_location(std::ostream& to, file_mgr& fm, bool highlight) {
+    if(!loc) return;
+    to << "occuring on line " << loc->begin.line << ":" << std::endl;
+    fm.print_location(to, *loc, highlight);
+}
+
+void compiler_error::pretty_print(std::ostream& to, file_mgr& fm) {
+    print_about(to);
+    print_location(to, fm);
+}
+
+const char* type_error::what() const noexcept {
+    return "an error occured while checking the types of the program";
+}
+
+void type_error::pretty_print(std::ostream& to, file_mgr& fm) {
+    print_about(to);
+    print_location(to, fm, true);
+}
+
+void unification_error::pretty_print(std::ostream& to, file_mgr& fm, type_mgr& mgr) {
+    type_error::pretty_print(to, fm);
+    to << "the expected type was:" << std::endl;
+    to << "  \033[34m";
+    left->print(mgr, to);
+    to << std::endl << "\033[0mwhile the actual type was:" << std::endl;
+    to << "  \033[32m";
+    right->print(mgr, to);
+    to << "\033[0m" << std::endl;
+}

code/compiler/13/error.hpp

@@ -0,0 +1,49 @@
+#pragma once
+#include <exception>
+#include <optional>
+#include "type.hpp"
+#include "location.hh"
+#include "parse_driver.hpp"
+
+using maybe_location = std::optional<yy::location>;
+
+class compiler_error : std::exception {
+    private:
+        std::string description;
+        maybe_location loc;
+
+    public:
+        compiler_error(std::string d, maybe_location l = std::nullopt)
+            : description(std::move(d)), loc(std::move(l)) {}
+
+        const char* what() const noexcept override;
+
+        void print_about(std::ostream& to);
+        void print_location(std::ostream& to, file_mgr& fm, bool highlight = false);
+
+        void pretty_print(std::ostream& to, file_mgr& fm);
+};
+
+class type_error : compiler_error {
+    private:
+
+    public:
+        type_error(std::string d, maybe_location l = std::nullopt)
+            : compiler_error(std::move(d), std::move(l)) {}
+
+        const char* what() const noexcept override;
+        void pretty_print(std::ostream& to, file_mgr& fm);
+};
+
+class unification_error : public type_error {
+    private:
+        type_ptr left;
+        type_ptr right;
+
+    public:
+        unification_error(type_ptr l, type_ptr r, maybe_location loc = std::nullopt)
+            : left(std::move(l)), right(std::move(r)), 
+            type_error("failed to unify types", std::move(loc)) {}
+
+        void pretty_print(std::ostream& to, file_mgr& fm, type_mgr& mgr);
+};

code/compiler/13/examples/bad1.txt

@@ -0,0 +1,2 @@
+data Bool = { True, False }
+defn main = { 3 + True }

code/compiler/13/examples/bad2.txt

@@ -0,0 +1 @@
+defn main = { 1 2 3 4 5 }

code/compiler/13/examples/bad3.txt

@@ -0,0 +1,8 @@
+data List = { Nil, Cons Int List }
+
+defn head l = {
+    case l of {
+        Nil -> { 0 }
+        Cons x y z -> { x }
+    }
+}

code/compiler/13/examples/errors/double_catchall.txt

@@ -0,0 +1,6 @@
+defn main = {
+    case True of {
+        n -> { 2 }
+        n -> { 1 }
+    }
+}

code/compiler/13/examples/errors/duplicate_type_param.txt

@@ -0,0 +1 @@
+data Pair a a = { MkPair a a }

code/compiler/13/examples/errors/exhausted_patterns.txt

@@ -0,0 +1,7 @@
+defn main = {
+    case True of {
+        True -> { 1 }
+        False -> { 0 }
+        n -> { 2 }
+    }
+}

code/compiler/13/examples/errors/incomplete_patterns.txt

@@ -0,0 +1,5 @@
+defn main = {
+    case True of {
+        True -> { 1 }
+    }
+}

code/compiler/13/examples/errors/invalid_case_analysis.txt

@@ -0,0 +1,7 @@
+defn add x y = { x + y }
+
+defn main = {
+    case add of {
+        n -> { 1 }
+    }
+}

code/compiler/13/examples/errors/match_after_catchall.txt

@@ -0,0 +1,7 @@
+defn main = {
+    case True of {
+        n -> { 2 }
+        True -> { 1 }
+        False -> { 0 }
+    }
+}

code/compiler/13/examples/errors/pattern_too_few_args.txt

@@ -0,0 +1,8 @@
+data List = { Nil, Cons Int List }
+
+defn head l = {
+    case l of {
+        Nil -> { 0 }
+        Cons x -> { x }
+    }
+}

code/compiler/13/examples/errors/pattern_too_many_args.txt

@@ -0,0 +1,8 @@
+data List = { Nil, Cons Int List }
+
+defn head l = {
+    case l of {
+        Nil -> { 0 }
+        Cons x y z -> { x }
+    }
+}

code/compiler/13/examples/errors/pattern_unknown_constructor.txt

@@ -0,0 +1,6 @@
+defn main = {
+    case True of {
+        NotBool -> { 1 }
+        True -> { 2 }
+    }
+}

code/compiler/13/examples/errors/type_redefinition.txt

@@ -0,0 +1 @@
+data Bool = { True, False }

code/compiler/13/examples/errors/unknown_lid.txt

@@ -0,0 +1,3 @@
+defn main = {
+    weird 1
+}

code/compiler/13/examples/errors/unknown_type.txt

@@ -0,0 +1 @@
+data Wrapper = { Wrap Weird }

code/compiler/13/examples/errors/unknown_type_param.txt

@@ -0,0 +1 @@
+data Wrapper = { Wrap a }

code/compiler/13/examples/errors/unknown_uid.txt

@@ -0,0 +1,3 @@
+defn main = {
+    Weird 1
+}

code/compiler/13/examples/errors/wrong_type_kind.txt

@@ -0,0 +1 @@
+data Wrapper = { Wrap (Int Bool) }

code/compiler/13/examples/fixpoint.txt

@@ -0,0 +1,17 @@
+data List a = { Nil, Cons a (List a) }
+
+defn fix f = { let { defn x = { f x } } in { x } }
+defn fixpointOnes fo = { Cons 1 fo }
+defn sumTwo l = {
+    case l of {
+        Nil -> { 0 }
+        Cons x xs -> {
+            x + case xs of {
+                Nil -> { 0 }
+                Cons y ys -> { y }
+            }
+        }
+    }
+}
+
+defn main = { sumTwo (fix fixpointOnes) }

code/compiler/13/examples/if.txt

@@ -0,0 +1,8 @@
+data Bool = { True, False }
+defn if c t e = {
+    case c of {
+        True -> { t }
+        False -> { e }
+    }
+}
+defn main = { if (if True False True) 11 3 }

code/compiler/13/examples/lambda.txt

@@ -0,0 +1,19 @@
+data List a = { Nil, Cons a (List a) }
+
+defn sum l = {
+    case l of {
+        Nil -> { 0 }
+        Cons x xs -> { x + sum xs}
+    }
+}
+
+defn map f l = {
+    case l of {
+        Nil -> { Nil }
+        Cons x xs -> { Cons (f x) (map f xs) }
+    }
+}
+
+defn main = {
+    sum (map \x -> { x * x } (map (\x -> { x + x }) (Cons 1 (Cons 2 (Cons 3 Nil)))))
+}

code/compiler/13/examples/letin.txt

@@ -0,0 +1,47 @@
+data Bool = { True, False }
+
+data List a = { Nil, Cons a (List a) }
+
+defn if c t e = {
+    case c of {
+        True -> { t }
+        False -> { e }
+    }
+}
+
+defn mergeUntil l r p = {
+    let {
+        defn mergeLeft nl nr = {
+            case nl of {
+                Nil -> { Nil }
+                Cons x xs -> { if (p x) (Cons x (mergeRight xs nr)) Nil }
+            }
+        }
+        defn mergeRight nl nr = {
+            case nr of {
+                Nil -> { Nil }
+                Cons x xs -> { if (p x) (Cons x (mergeLeft nl xs)) Nil }
+            }
+        }
+    } in {
+        mergeLeft l r
+    }
+}
+
+defn const x y = { x }
+
+defn sum l = {
+    case l of {
+        Nil -> { 0 }
+        Cons x xs -> { x + sum xs }
+    }
+}
+
+defn main = {
+    let {
+        defn firstList = { Cons 1 (Cons 3 (Cons 5 Nil)) }
+        defn secondList = { Cons 2 (Cons 4 (Cons 6 Nil)) }
+    } in {
+        sum (mergeUntil firstList secondList (const True))
+    }
+}

code/compiler/13/examples/list.txt

@@ -0,0 +1,32 @@
+data List a = { Nil, Cons a (List a) }
+
+defn map f l = {
+    case l of {
+        Nil -> { Nil }
+        Cons x xs -> { Cons (f x) (map f xs) }
+    }
+}
+
+defn foldl f b l = {
+    case l of {
+        Nil -> { b }
+        Cons x xs -> { foldl f (f b x) xs }
+    }
+}
+
+defn foldr f b l = {
+    case l of {
+        Nil -> { b }
+        Cons x xs -> { f x (foldr f b xs) }
+    }
+}
+
+defn list = { Cons 1 (Cons 2 (Cons 3 (Cons 4 Nil))) }
+
+defn add x y = { x + y }
+defn sum l = { foldr add 0 l }
+
+defn skipAdd x y = { y + 1 }
+defn length l = { foldr skipAdd 0 l }
+
+defn main = { sum list + length list }

code/compiler/13/examples/mutual_recursion.txt

@@ -0,0 +1,25 @@
+data Bool = { True, False }
+data List = { Nil, Cons Int List }
+
+defn if c t e = {
+    case c of {
+        True -> { t }
+        False -> { e }
+    }
+}
+
+defn oddEven l e = {
+    case l of {
+        Nil -> { e }
+        Cons x xs -> { evenOdd xs e }
+    }
+}
+
+defn evenOdd l e = {
+    case l of {
+        Nil -> { e }
+        Cons x xs -> { oddEven xs e }
+    }
+}
+
+defn main = { if (oddEven (Cons 1 (Cons 2 (Cons 3 Nil))) True) (oddEven (Cons 1 (Cons 2 (Cons 3 Nil))) 1) 3 }

code/compiler/13/examples/packed.txt

@@ -0,0 +1,23 @@
+data Pair a b = { Pair a b }
+
+defn packer = {
+    let {
+        data Packed a = { Packed a }
+        defn pack a = { Packed a }
+        defn unpack p = {
+            case p of {
+                Packed a -> { a }
+            }
+        }
+    } in {
+        Pair pack unpack
+    }
+}
+
+defn main = { 
+    case packer of {
+        Pair pack unpack -> {
+            unpack (pack 3)
+        }
+    }
+}

code/compiler/13/examples/pair.txt

@@ -0,0 +1,17 @@
+data Pair a b = { MkPair a b }
+
+defn fst p = {
+    case p of {
+        MkPair a b -> { a }
+    }
+}
+
+defn snd p = {
+    case p of {
+        MkPair a b -> { b }
+    }
+}
+
+defn pair = { MkPair 1 (MkPair 2 3) }
+
+defn main = { fst pair + snd (snd pair) }

code/compiler/13/examples/primes.txt

@@ -0,0 +1,122 @@
+data List = { Nil, Cons Nat List }
+data Bool = { True, False }
+data Nat = { O, S Nat }
+
+defn if c t e = {
+    case c of {
+        True -> { t }
+        False -> { e }
+    }
+}
+
+defn toInt n = {
+    case n of {
+        O -> { 0 }
+        S np -> { 1 + toInt np }
+    }
+}
+
+defn lte n m = {
+    case m of {
+        O -> {
+            case n of {
+                O -> { True }
+                S np -> { False }
+            }
+        }
+        S mp -> {
+            case n of {
+                O -> { True }
+                S np -> { lte np mp }
+            }
+        }
+    }
+}
+
+defn minus n m = {
+    case m of {
+        O -> { n }
+        S mp -> { 
+            case n of {
+                O -> { O }
+                S np -> {
+                    minus np mp
+                }
+            }
+        }
+    }
+}
+
+defn mod n m = {
+    if (lte m n) (mod (minus n m) m) n
+}
+
+defn notDivisibleBy n m = {
+    case (mod m n) of {
+        O -> { False }
+        S mp -> { True }
+    }
+}
+
+defn filter f l = {
+    case l of {
+        Nil -> { Nil }
+        Cons x xs -> { if (f x) (Cons x (filter f xs)) (filter f xs) }
+    }
+}
+
+defn map f l = {
+    case l of {
+        Nil -> { Nil }
+        Cons x xs -> { Cons (f x) (map f xs) }
+    }
+}
+
+defn nats = {
+    Cons (S (S O)) (map S nats)
+}
+
+defn primesRec l = {
+    case l of {
+        Nil -> { Nil }
+        Cons p xs -> { Cons p (primesRec (filter (notDivisibleBy p) xs)) }
+    }
+}
+
+defn primes = {
+    primesRec nats
+}
+
+defn take n l = {
+    case l of {
+        Nil -> { Nil }
+        Cons x xs -> {
+            case n of {
+                O -> { Nil }
+                S np -> { Cons x (take np xs) }
+            }
+        }
+    }
+}
+
+defn head l = {
+    case l of {
+        Nil -> { O }
+        Cons x xs -> { x }
+    }
+}
+
+defn reverseAcc a l = {
+    case l of {
+        Nil -> { a }
+        Cons x xs -> { reverseAcc (Cons x a) xs }
+    }
+}
+
+defn reverse l = {
+    reverseAcc Nil l
+}
+
+defn main = {
+    toInt (head (reverse (take ((S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) primes)))
+}

code/compiler/13/examples/runtime1.c

@@ -0,0 +1,31 @@
+#include "../runtime.h"
+
+void f_add(struct stack* s) {
+    struct node_num* left = (struct node_num*) eval(stack_peek(s, 0));
+    struct node_num* right = (struct node_num*) eval(stack_peek(s, 1));
+    stack_push(s, (struct node_base*) alloc_num(left->value + right->value));
+}
+
+void f_main(struct stack* s) {
+    // PushInt 320
+    stack_push(s, (struct node_base*) alloc_num(320));
+
+    // PushInt 6
+    stack_push(s, (struct node_base*) alloc_num(6));
+
+    // PushGlobal f_add (the function for +)
+    stack_push(s, (struct node_base*) alloc_global(f_add, 2));
+
+    struct node_base* left;
+    struct node_base* right;
+    
+    // MkApp
+    left = stack_pop(s);
+    right = stack_pop(s);
+    stack_push(s, (struct node_base*) alloc_app(left, right));
+    
+    // MkApp
+    left = stack_pop(s);
+    right = stack_pop(s);
+    stack_push(s, (struct node_base*) alloc_app(left, right));
+}

code/compiler/13/examples/works1.txt

@@ -0,0 +1,2 @@
+defn main = { sum 320 6 }
+defn sum x y = { x + y }

code/compiler/13/examples/works2.txt

@@ -0,0 +1,3 @@
+defn add x y = { x + y }
+defn double x = { add x x }
+defn main = { double 163 }

code/compiler/13/examples/works3.txt

@@ -0,0 +1,9 @@
+data List a = { Nil, Cons a (List a) }
+data Bool = { True, False }
+defn length l = {
+    case l of {
+        Nil -> { 0 }
+        Cons x xs -> { 1 + length xs }
+    }
+}
+defn main = { length (Cons 1 (Cons 2 (Cons 3 Nil))) + length (Cons True (Cons False (Cons True Nil))) }

code/compiler/13/examples/works4.txt

@@ -0,0 +1,16 @@
+data List = { Nil, Cons Int List }
+
+defn add x y = { x + y }
+defn mul x y = { x * y }
+
+defn foldr f b l = {
+    case l of {
+        Nil -> { b }
+        Cons x xs -> { f x (foldr f b xs) }
+    }
+}
+
+defn main = {
+    foldr add 0 (Cons 1 (Cons 2 (Cons 3 (Cons 4 Nil)))) +
+    foldr mul 1 (Cons 1 (Cons 2 (Cons 3 (Cons 4 Nil))))
+}

code/compiler/13/examples/works5.txt

@@ -0,0 +1,17 @@
+data List = { Nil, Cons Int List }
+
+defn sumZip l m = {
+    case l of {
+        Nil -> { 0 }
+        Cons x xs -> {
+            case m of {
+                Nil -> { 0 }
+                Cons y ys -> { x + y + sumZip xs ys }
+            }
+        }
+    }
+}
+
+defn ones = { Cons 1 ones }
+
+defn main = { sumZip ones (Cons 1 (Cons 2 (Cons 3 Nil))) }

code/compiler/13/global_scope.cpp

@@ -0,0 +1,76 @@
+#include "global_scope.hpp"
+#include "ast.hpp"
+
+void global_function::compile() {
+    env_ptr new_env = env_ptr(new env_offset(0, nullptr));
+    for(auto it = params.rbegin(); it != params.rend(); it++) {
+        new_env = env_ptr(new env_var(*it, new_env));
+    }
+    body->compile(new_env, instructions);
+    instructions.push_back(instruction_ptr(new instruction_update(params.size())));
+    instructions.push_back(instruction_ptr(new instruction_pop(params.size())));
+}
+
+void global_function::declare_llvm(llvm_context& ctx) {
+    generated_function = ctx.create_custom_function(name, params.size());
+}
+
+void global_function::generate_llvm(llvm_context& ctx) {
+    ctx.get_builder().SetInsertPoint(&generated_function->getEntryBlock());
+    for(auto& instruction : instructions) {
+        instruction->gen_llvm(ctx, generated_function);
+    }
+    ctx.get_builder().CreateRetVoid();
+}
+
+void global_constructor::generate_llvm(llvm_context& ctx) {
+    auto new_function =
+        ctx.create_custom_function(name, arity);
+    std::vector<instruction_ptr> instructions;
+    instructions.push_back(instruction_ptr(new instruction_pack(tag, arity)));
+    instructions.push_back(instruction_ptr(new instruction_update(0)));
+    ctx.get_builder().SetInsertPoint(&new_function->getEntryBlock());
+    for (auto& instruction : instructions) {
+        instruction->gen_llvm(ctx, new_function);
+    }
+    ctx.get_builder().CreateRetVoid();
+}
+
+global_function& global_scope::add_function(
+        const std::string& n,
+        std::vector<std::string> ps,
+        ast_ptr b) {
+    auto name = mng->new_mangled_name(n);
+    global_function* new_function =
+        new global_function(std::move(name), std::move(ps), std::move(b));
+    functions.push_back(global_function_ptr(new_function));
+    return *new_function;
+}
+
+global_constructor& global_scope::add_constructor(
+        const std::string& n,
+        int8_t t,
+        size_t a) {
+    auto name = mng->new_mangled_name(n);
+    global_constructor* new_constructor = new global_constructor(name, t, a);
+    constructors.push_back(global_constructor_ptr(new_constructor));
+    return *new_constructor;
+}
+
+void global_scope::compile() {
+    for(auto& function : functions) {
+        function->compile();
+    }
+}
+
+void global_scope::generate_llvm(llvm_context& ctx) {
+    for(auto& constructor : constructors) {
+        constructor->generate_llvm(ctx);
+    }
+    for(auto& function : functions) {
+        function->declare_llvm(ctx);
+    }
+    for(auto& function : functions) {
+        function->generate_llvm(ctx);
+    }
+}

code/compiler/13/global_scope.hpp

@@ -0,0 +1,60 @@
+#pragma once
+#include <memory>
+#include <string>
+#include <vector>
+#include <llvm/IR/Function.h>
+#include "instruction.hpp"
+#include "mangler.hpp"
+
+struct ast;
+using ast_ptr = std::unique_ptr<ast>;
+
+struct global_function {
+    std::string name;
+    std::vector<std::string> params;
+    ast_ptr body;
+
+    std::vector<instruction_ptr> instructions;
+    llvm::Function* generated_function;
+
+    global_function(std::string n, std::vector<std::string> ps, ast_ptr b)
+        : name(std::move(n)), params(std::move(ps)), body(std::move(b)) {}
+
+    void compile();
+    void declare_llvm(llvm_context& ctx);
+    void generate_llvm(llvm_context& ctx);
+};
+
+using global_function_ptr = std::unique_ptr<global_function>;
+
+struct global_constructor {
+    std::string name;
+    int8_t tag;
+    size_t arity;
+
+    global_constructor(std::string n, int8_t t, size_t a)
+        : name(std::move(n)), tag(t), arity(a) {}
+
+    void generate_llvm(llvm_context& ctx);
+};
+
+using global_constructor_ptr = std::unique_ptr<global_constructor>;
+
+class global_scope {
+    private:
+        std::vector<global_function_ptr> functions;
+        std::vector<global_constructor_ptr> constructors;
+        mangler* mng;
+
+    public:
+        global_scope(mangler& m) : mng(&m) {}
+
+        global_function& add_function(
+                const std::string& n, 
+                std::vector<std::string> ps, 
+                ast_ptr b);
+        global_constructor& add_constructor(const std::string& n, int8_t t, size_t a);
+
+        void compile();
+        void generate_llvm(llvm_context& ctx);
+};

code/compiler/13/graph.cpp

@@ -0,0 +1,114 @@
+#include "graph.hpp"
+
+std::set<function_graph::edge> function_graph::compute_transitive_edges() {
+    std::set<edge> transitive_edges;
+    transitive_edges.insert(edges.begin(), edges.end());
+    for(auto& connector : adjacency_lists) {
+        for(auto& from : adjacency_lists) {
+            edge to_connector { from.first, connector.first };
+            for(auto& to : adjacency_lists) {
+                edge full_jump { from.first, to.first };
+                if(transitive_edges.find(full_jump) != transitive_edges.end()) continue;
+
+                edge from_connector { connector.first, to.first };
+                if(transitive_edges.find(to_connector) != transitive_edges.end() &&
+                        transitive_edges.find(from_connector) != transitive_edges.end())
+                    transitive_edges.insert(std::move(full_jump));
+            }
+        }
+    }
+    return transitive_edges;
+}
+
+void function_graph::create_groups(
+        const std::set<edge>& transitive_edges,
+        std::map<function, group_id>& group_ids,
+        std::map<group_id, data_ptr>& group_data_map) {
+    group_id id_counter = 0;
+    for(auto& vertex : adjacency_lists) {
+        if(group_ids.find(vertex.first) != group_ids.end())
+            continue;
+        data_ptr new_group(new group_data);
+        new_group->functions.insert(vertex.first);
+        group_data_map[id_counter] = new_group;
+        group_ids[vertex.first] = id_counter;
+        for(auto& other_vertex : adjacency_lists) {
+            if(transitive_edges.find({vertex.first, other_vertex.first}) != transitive_edges.end() &&
+                    transitive_edges.find({other_vertex.first, vertex.first}) != transitive_edges.end()) {
+                group_ids[other_vertex.first] = id_counter;
+                new_group->functions.insert(other_vertex.first);
+            }
+        }
+        id_counter++;
+    }
+}
+
+void function_graph::create_edges(
+        std::map<function, group_id>& group_ids,
+        std::map<group_id, data_ptr>& group_data_map) {
+    std::set<std::pair<group_id, group_id>> group_edges;
+    for(auto& vertex : adjacency_lists) {
+        auto vertex_id = group_ids[vertex.first];
+        auto& vertex_data = group_data_map[vertex_id];
+        for(auto& other_vertex : vertex.second) {
+            auto other_id = group_ids[other_vertex];
+            if(vertex_id == other_id) continue;
+            if(group_edges.find({vertex_id, other_id}) != group_edges.end())
+                continue;
+            group_edges.insert({vertex_id, other_id});
+            vertex_data->adjacency_list.insert(other_id);
+            group_data_map[other_id]->indegree++;
+        }
+    }
+}
+
+std::vector<group_ptr> function_graph::generate_order(
+        std::map<function, group_id>& group_ids,
+        std::map<group_id, data_ptr>& group_data_map) {
+    std::queue<group_id> id_queue;
+    std::vector<group_ptr> output;
+    for(auto& group : group_data_map) {
+        if(group.second->indegree == 0) id_queue.push(group.first);
+    }
+
+    while(!id_queue.empty()) {
+        auto new_id = id_queue.front();
+        auto& group_data = group_data_map[new_id];
+        group_ptr output_group(new group);
+        output_group->members = std::move(group_data->functions);
+        id_queue.pop();
+
+        for(auto& adjacent_group : group_data->adjacency_list) {
+            if(--group_data_map[adjacent_group]->indegree == 0)
+                id_queue.push(adjacent_group);
+        }
+
+        output.push_back(std::move(output_group));
+    }
+
+    return output;
+}
+
+std::set<function>& function_graph::add_function(const function& f) {
+    auto adjacency_list_it = adjacency_lists.find(f);
+    if(adjacency_list_it != adjacency_lists.end()) {
+        return adjacency_list_it->second;
+    } else {
+        return adjacency_lists[f] = { };
+    }
+}
+
+void function_graph::add_edge(const function& from, const function& to) {
+    add_function(from).insert(to);
+    edges.insert({ from, to });
+}
+
+std::vector<group_ptr> function_graph::compute_order() {
+    std::set<edge> transitive_edges = compute_transitive_edges();
+    std::map<function, group_id> group_ids;
+    std::map<group_id, data_ptr> group_data_map;
+
+    create_groups(transitive_edges, group_ids, group_data_map);
+    create_edges(group_ids, group_data_map);
+    return generate_order(group_ids, group_data_map);
+}

code/compiler/13/graph.hpp

@@ -0,0 +1,54 @@
+#pragma once
+#include <algorithm>
+#include <cstddef>
+#include <queue>
+#include <set>
+#include <string>
+#include <map>
+#include <memory>
+#include <vector>
+
+using function = std::string;
+
+struct group {
+    std::set<function> members;
+};
+
+using group_ptr = std::unique_ptr<group>;
+
+class function_graph {
+    private:
+        using group_id = size_t;
+
+        struct group_data {
+            std::set<function> functions;
+            std::set<group_id> adjacency_list;
+            size_t indegree;
+
+            group_data() : indegree(0) {}
+        };
+
+        using data_ptr = std::shared_ptr<group_data>;
+        using edge = std::pair<function, function>;
+        using group_edge = std::pair<group_id, group_id>;
+
+        std::map<function, std::set<function>> adjacency_lists;
+        std::set<edge> edges;
+
+        std::set<edge> compute_transitive_edges();
+        void create_groups(
+                const std::set<edge>&,
+                std::map<function, group_id>&,
+                std::map<group_id, data_ptr>&);
+        void create_edges(
+                std::map<function, group_id>&,
+                std::map<group_id, data_ptr>&);
+        std::vector<group_ptr> generate_order(
+                std::map<function, group_id>&,
+                std::map<group_id, data_ptr>&);
+    
+    public:
+        std::set<function>& add_function(const function& f);
+        void add_edge(const function& from, const function& to);
+        std::vector<group_ptr> compute_order();
+};

code/compiler/13/instruction.cpp

@@ -0,0 +1,177 @@
+#include "instruction.hpp"
+#include "llvm_context.hpp"
+#include <llvm/IR/BasicBlock.h>
+#include <llvm/IR/Function.h>
+
+using namespace llvm;
+
+static void print_indent(int n, std::ostream& to) {
+    while(n--) to << "  ";
+}
+
+void instruction_pushint::print(int indent, std::ostream& to) const {
+    print_indent(indent, to);
+    to << "PushInt(" << value << ")" << std::endl;
+}
+
+void instruction_pushint::gen_llvm(llvm_context& ctx, Function* f) const {
+    ctx.create_push(f, ctx.create_num(f, ctx.create_i32(value)));
+}
+
+void instruction_pushglobal::print(int indent, std::ostream& to) const {
+    print_indent(indent, to);
+    to << "PushGlobal(" << name << ")" << std::endl;
+}
+
+void instruction_pushglobal::gen_llvm(llvm_context& ctx, Function* f) const {
+    auto& global_f = ctx.get_custom_function(name);
+    auto arity = ctx.create_i32(global_f.arity);
+    ctx.create_push(f, ctx.create_global(f, global_f.function, arity));
+}
+
+void instruction_push::print(int indent, std::ostream& to) const {
+    print_indent(indent, to);
+    to << "Push(" << offset << ")" << std::endl;
+}
+
+void instruction_push::gen_llvm(llvm_context& ctx, Function* f) const {
+    ctx.create_push(f, ctx.create_peek(f, ctx.create_size(offset)));
+}
+
+void instruction_pop::print(int indent, std::ostream& to) const {
+    print_indent(indent, to);
+    to << "Pop(" << count << ")" << std::endl;
+}
+
+void instruction_pop::gen_llvm(llvm_context& ctx, Function* f) const {
+    ctx.create_popn(f, ctx.create_size(count));
+}
+
+void instruction_mkapp::print(int indent, std::ostream& to) const {
+    print_indent(indent, to);
+    to << "MkApp()" << std::endl;
+}
+
+void instruction_mkapp::gen_llvm(llvm_context& ctx, Function* f) const {
+    auto left = ctx.create_pop(f);
+    auto right = ctx.create_pop(f);
+    ctx.create_push(f, ctx.create_app(f, left, right));
+}
+
+void instruction_update::print(int indent, std::ostream& to) const {
+    print_indent(indent, to);
+    to << "Update(" << offset << ")" << std::endl;
+}
+
+void instruction_update::gen_llvm(llvm_context& ctx, Function* f) const {
+    ctx.create_update(f, ctx.create_size(offset));
+}
+
+void instruction_pack::print(int indent, std::ostream& to) const {
+    print_indent(indent, to);
+    to << "Pack(" << tag << ", " << size << ")" << std::endl;
+}
+
+void instruction_pack::gen_llvm(llvm_context& ctx, Function* f) const {
+    ctx.create_pack(f, ctx.create_size(size), ctx.create_i8(tag));
+}
+
+void instruction_split::print(int indent, std::ostream& to) const {
+    print_indent(indent, to);
+    to << "Split()" << std::endl;
+}
+
+void instruction_split::gen_llvm(llvm_context& ctx, Function* f) const {
+    ctx.create_split(f, ctx.create_size(size));
+}
+
+void instruction_jump::print(int indent, std::ostream& to) const {
+    print_indent(indent, to);
+    to << "Jump(" << std::endl;
+    for(auto& instruction_set : branches) {
+        for(auto& instruction : instruction_set) {
+            instruction->print(indent + 2, to);
+        }
+        to << std::endl;
+    }
+    print_indent(indent, to);
+    to << ")" << std::endl;
+}
+
+void instruction_jump::gen_llvm(llvm_context& ctx, Function* f) const {
+    auto top_node = ctx.create_peek(f, ctx.create_size(0));
+    auto tag = ctx.unwrap_data_tag(top_node);
+    auto safety_block = ctx.create_basic_block("safety", f);
+    auto switch_op = ctx.get_builder().CreateSwitch(tag, safety_block, tag_mappings.size());
+    std::vector<BasicBlock*> blocks;
+
+    for(auto& branch : branches) {
+        auto branch_block = ctx.create_basic_block("branch", f);
+        ctx.get_builder().SetInsertPoint(branch_block);
+        for(auto& instruction : branch) {
+            instruction->gen_llvm(ctx, f);
+        }
+        ctx.get_builder().CreateBr(safety_block);
+        blocks.push_back(branch_block);
+    }
+
+    for(auto& mapping : tag_mappings) {
+        switch_op->addCase(ctx.create_i8(mapping.first), blocks[mapping.second]);
+    }
+
+    ctx.get_builder().SetInsertPoint(safety_block);
+}
+
+void instruction_slide::print(int indent, std::ostream& to) const {
+    print_indent(indent, to);
+    to << "Slide(" << offset << ")" << std::endl;
+}
+
+void instruction_slide::gen_llvm(llvm_context& ctx, Function* f) const {
+    ctx.create_slide(f, ctx.create_size(offset));
+}
+
+void instruction_binop::print(int indent, std::ostream& to) const {
+    print_indent(indent, to);
+    to << "BinOp(" << op_action(op) << ")" << std::endl;
+}
+
+void instruction_binop::gen_llvm(llvm_context& ctx, Function* f) const {
+    auto left_int = ctx.unwrap_num(ctx.create_pop(f));
+    auto right_int = ctx.unwrap_num(ctx.create_pop(f));
+    llvm::Value* result;
+    switch(op) {
+        case PLUS: result = ctx.get_builder().CreateAdd(left_int, right_int); break;
+        case MINUS: result = ctx.get_builder().CreateSub(left_int, right_int); break;
+        case TIMES: result = ctx.get_builder().CreateMul(left_int, right_int); break;
+        case DIVIDE: result = ctx.get_builder().CreateSDiv(left_int, right_int); break;
+    }
+    ctx.create_push(f, ctx.create_num(f, result));
+}
+
+void instruction_eval::print(int indent, std::ostream& to) const {
+    print_indent(indent, to);
+    to << "Eval()" << std::endl;
+}
+
+void instruction_eval::gen_llvm(llvm_context& ctx, Function* f) const {
+    ctx.create_unwind(f);
+}
+
+void instruction_alloc::print(int indent, std::ostream& to) const {
+    print_indent(indent, to);
+    to << "Alloc(" << amount << ")" << std::endl;
+}
+
+void instruction_alloc::gen_llvm(llvm_context& ctx, Function* f) const {
+    ctx.create_alloc(f, ctx.create_size(amount));
+}
+
+void instruction_unwind::print(int indent, std::ostream& to) const {
+    print_indent(indent, to);
+    to << "Unwind()" << std::endl;
+}
+
+void instruction_unwind::gen_llvm(llvm_context& ctx, Function* f) const {
+    // Nothing
+}

code/compiler/13/instruction.hpp

@@ -0,0 +1,142 @@
+#pragma once
+#include <llvm/IR/Function.h>
+#include <string>
+#include <memory>
+#include <vector>
+#include <map>
+#include <ostream>
+#include "binop.hpp"
+#include "llvm_context.hpp"
+
+struct instruction {
+    virtual ~instruction() = default;
+
+    virtual void print(int indent, std::ostream& to) const = 0;
+    virtual void gen_llvm(llvm_context& ctx, llvm::Function* f) const = 0;
+};
+
+using instruction_ptr = std::unique_ptr<instruction>;
+
+struct instruction_pushint : public instruction {
+    int value;
+
+    instruction_pushint(int v)
+        : value(v) {}
+
+    void print(int indent, std::ostream& to) const;
+    void gen_llvm(llvm_context& ctx, llvm::Function* f) const;
+};
+
+struct instruction_pushglobal : public instruction {
+    std::string name;
+
+    instruction_pushglobal(std::string n)
+        : name(std::move(n)) {}
+
+    void print(int indent, std::ostream& to) const;
+    void gen_llvm(llvm_context& ctx, llvm::Function* f) const;
+};
+
+struct instruction_push : public instruction {
+    int offset;
+
+    instruction_push(int o)
+        : offset(o) {}
+
+    void print(int indent, std::ostream& to) const;
+    void gen_llvm(llvm_context& ctx, llvm::Function* f) const;
+};
+
+struct instruction_pop : public instruction {
+    int count;
+
+    instruction_pop(int c)
+        : count(c) {}
+
+    void print(int indent, std::ostream& to) const;
+    void gen_llvm(llvm_context& ctx, llvm::Function* f) const;
+};
+
+struct instruction_mkapp : public instruction {
+    void print(int indent, std::ostream& to) const;
+    void gen_llvm(llvm_context& ctx, llvm::Function* f) const;
+};
+
+struct instruction_update : public instruction {
+    int offset;
+
+    instruction_update(int o)
+        : offset(o) {}
+
+    void print(int indent, std::ostream& to) const;
+    void gen_llvm(llvm_context& ctx, llvm::Function* f) const;
+};
+
+struct instruction_pack : public instruction {
+    int tag;
+    int size;
+
+    instruction_pack(int t, int s)
+        : tag(t), size(s) {}
+
+    void print(int indent, std::ostream& to) const;
+    void gen_llvm(llvm_context& ctx, llvm::Function* f) const;
+};
+
+struct instruction_split : public instruction {
+    int size;
+
+    instruction_split(int s)
+        : size(s) {}
+
+    void print(int indent, std::ostream& to) const;
+    void gen_llvm(llvm_context& ctx, llvm::Function* f) const;
+};
+
+struct instruction_jump : public instruction {
+    std::vector<std::vector<instruction_ptr>> branches;
+    std::map<int, int> tag_mappings;
+
+    void print(int indent, std::ostream& to) const;
+    void gen_llvm(llvm_context& ctx, llvm::Function* f) const;
+};
+
+struct instruction_slide : public instruction {
+    int offset;
+
+    instruction_slide(int o)
+        : offset(o) {}
+
+    void print(int indent, std::ostream& to) const;
+    void gen_llvm(llvm_context& ctx, llvm::Function* f) const;
+};
+
+struct instruction_binop : public instruction {
+    binop op;
+
+    instruction_binop(binop o)
+        : op(o) {}
+
+    void print(int indent, std::ostream& to) const;
+    void gen_llvm(llvm_context& ctx, llvm::Function* f) const;
+};
+
+struct instruction_eval : public instruction {
+    void print(int indent, std::ostream& to) const;
+    void gen_llvm(llvm_context& ctx, llvm::Function* f) const;
+};
+
+struct instruction_alloc : public instruction {
+    int amount;
+
+    instruction_alloc(int a)
+        : amount(a) {}
+
+    void print(int indent, std::ostream& to) const;
+    void gen_llvm(llvm_context& ctx, llvm::Function* f) const;
+};
+
+struct instruction_unwind : public instruction {
+    void print(int indent, std::ostream& to) const;
+    void gen_llvm(llvm_context& ctx, llvm::Function* f) const;
+};

code/compiler/13/llvm_context.cpp

@@ -0,0 +1,294 @@
+#include "llvm_context.hpp"
+#include <llvm/IR/DerivedTypes.h>
+
+using namespace llvm;
+
+void llvm_context::create_types() {
+    stack_type = StructType::create(ctx, "stack");
+    gmachine_type = StructType::create(ctx, "gmachine");
+    stack_ptr_type = PointerType::getUnqual(stack_type);
+    gmachine_ptr_type = PointerType::getUnqual(gmachine_type);
+    tag_type = IntegerType::getInt8Ty(ctx);
+    struct_types["node_base"] = StructType::create(ctx, "node_base");
+    struct_types["node_app"] = StructType::create(ctx, "node_app");
+    struct_types["node_num"] = StructType::create(ctx, "node_num");
+    struct_types["node_global"] = StructType::create(ctx, "node_global");
+    struct_types["node_ind"] = StructType::create(ctx, "node_ind");
+    struct_types["node_data"] = StructType::create(ctx, "node_data");
+    node_ptr_type = PointerType::getUnqual(struct_types.at("node_base"));
+    function_type = FunctionType::get(Type::getVoidTy(ctx), { gmachine_ptr_type }, false);
+
+    gmachine_type->setBody(
+            stack_ptr_type,
+            node_ptr_type,
+            IntegerType::getInt64Ty(ctx),
+            IntegerType::getInt64Ty(ctx)
+    );
+    struct_types.at("node_base")->setBody(
+            IntegerType::getInt32Ty(ctx),
+            IntegerType::getInt8Ty(ctx),
+            node_ptr_type
+    );
+    struct_types.at("node_app")->setBody(
+            struct_types.at("node_base"),
+            node_ptr_type,
+            node_ptr_type
+    );
+    struct_types.at("node_num")->setBody(
+            struct_types.at("node_base"),
+            IntegerType::getInt32Ty(ctx)
+    );
+    struct_types.at("node_global")->setBody(
+            struct_types.at("node_base"),
+            FunctionType::get(Type::getVoidTy(ctx), { stack_ptr_type }, false)
+    );
+    struct_types.at("node_ind")->setBody(
+            struct_types.at("node_base"),
+            node_ptr_type
+    );
+    struct_types.at("node_data")->setBody(
+            struct_types.at("node_base"),
+            IntegerType::getInt8Ty(ctx),
+            PointerType::getUnqual(node_ptr_type)
+    );
+}
+
+void llvm_context::create_functions() {
+    auto void_type = Type::getVoidTy(ctx);
+    auto sizet_type = IntegerType::get(ctx, sizeof(size_t) * 8);
+    functions["stack_init"] = Function::Create(
+            FunctionType::get(void_type, { stack_ptr_type }, false),
+            Function::LinkageTypes::ExternalLinkage,
+            "stack_init",
+            &module
+    );
+    functions["stack_free"] = Function::Create(
+            FunctionType::get(void_type, { stack_ptr_type }, false),
+            Function::LinkageTypes::ExternalLinkage,
+            "stack_free",
+            &module
+    );
+    functions["stack_push"] = Function::Create(
+            FunctionType::get(void_type, { stack_ptr_type, node_ptr_type }, false),
+            Function::LinkageTypes::ExternalLinkage,
+            "stack_push",
+            &module
+    );
+    functions["stack_pop"] = Function::Create(
+            FunctionType::get(node_ptr_type, { stack_ptr_type }, false),
+            Function::LinkageTypes::ExternalLinkage,
+            "stack_pop",
+            &module
+    );
+    functions["stack_peek"] = Function::Create(
+            FunctionType::get(node_ptr_type, { stack_ptr_type, sizet_type }, false),
+            Function::LinkageTypes::ExternalLinkage,
+            "stack_peek",
+            &module
+    );
+    functions["stack_popn"] = Function::Create(
+            FunctionType::get(void_type, { stack_ptr_type, sizet_type }, false),
+            Function::LinkageTypes::ExternalLinkage,
+            "stack_popn",
+            &module
+    );
+    functions["gmachine_slide"] = Function::Create(
+            FunctionType::get(void_type, { gmachine_ptr_type, sizet_type }, false),
+            Function::LinkageTypes::ExternalLinkage,
+            "gmachine_slide",
+            &module
+    );
+    functions["gmachine_update"] = Function::Create(
+            FunctionType::get(void_type, { gmachine_ptr_type, sizet_type }, false),
+            Function::LinkageTypes::ExternalLinkage,
+            "gmachine_update",
+            &module
+    );
+    functions["gmachine_alloc"] = Function::Create(
+            FunctionType::get(void_type, { gmachine_ptr_type, sizet_type }, false),
+            Function::LinkageTypes::ExternalLinkage,
+            "gmachine_alloc",
+            &module
+    );
+    functions["gmachine_pack"] = Function::Create(
+            FunctionType::get(void_type, { gmachine_ptr_type, sizet_type, tag_type }, false),
+            Function::LinkageTypes::ExternalLinkage,
+            "gmachine_pack",
+            &module
+    );
+    functions["gmachine_split"] = Function::Create(
+            FunctionType::get(void_type, { gmachine_ptr_type, sizet_type }, false),
+            Function::LinkageTypes::ExternalLinkage,
+            "gmachine_split",
+            &module
+    );
+    functions["gmachine_track"] = Function::Create(
+            FunctionType::get(node_ptr_type, { gmachine_ptr_type, node_ptr_type }, false),
+            Function::LinkageTypes::ExternalLinkage,
+            "gmachine_track",
+            &module
+    );
+
+    auto int32_type = IntegerType::getInt32Ty(ctx);
+    functions["alloc_app"] = Function::Create(
+            FunctionType::get(node_ptr_type, { node_ptr_type, node_ptr_type }, false),
+            Function::LinkageTypes::ExternalLinkage,
+            "alloc_app",
+            &module
+    );
+    functions["alloc_num"] = Function::Create(
+            FunctionType::get(node_ptr_type, { int32_type }, false),
+            Function::LinkageTypes::ExternalLinkage,
+            "alloc_num",
+            &module
+    );
+    functions["alloc_global"] = Function::Create(
+            FunctionType::get(node_ptr_type, { function_type, int32_type }, false),
+            Function::LinkageTypes::ExternalLinkage,
+            "alloc_global",
+            &module
+    );
+    functions["alloc_ind"] = Function::Create(
+            FunctionType::get(node_ptr_type, { node_ptr_type }, false),
+            Function::LinkageTypes::ExternalLinkage,
+            "alloc_ind",
+            &module
+    );
+
+    functions["unwind"] = Function::Create(
+            FunctionType::get(void_type, { gmachine_ptr_type }, false),
+            Function::LinkageTypes::ExternalLinkage,
+            "unwind",
+            &module
+    );
+}
+
+IRBuilder<>& llvm_context::get_builder() {
+    return builder;
+}
+
+Module& llvm_context::get_module() {
+    return module;
+}
+
+BasicBlock* llvm_context::create_basic_block(const std::string& name, llvm::Function* f) {
+    return BasicBlock::Create(ctx, name, f);
+}
+
+ConstantInt* llvm_context::create_i8(int8_t i) {
+    return ConstantInt::get(ctx, APInt(8, i));
+}
+ConstantInt* llvm_context::create_i32(int32_t i) {
+    return ConstantInt::get(ctx, APInt(32, i));
+}
+ConstantInt* llvm_context::create_size(size_t i) {
+    return ConstantInt::get(ctx, APInt(sizeof(size_t) * 8, i));
+}
+
+Value* llvm_context::create_pop(Function* f) {
+    auto pop_f = functions.at("stack_pop");
+    return builder.CreateCall(pop_f, { unwrap_gmachine_stack_ptr(f->arg_begin()) });
+}
+Value* llvm_context::create_peek(Function* f, Value* off) {
+    auto peek_f = functions.at("stack_peek");
+    return builder.CreateCall(peek_f, { unwrap_gmachine_stack_ptr(f->arg_begin()), off });
+}
+void llvm_context::create_push(Function* f, Value* v) {
+    auto push_f = functions.at("stack_push");
+    builder.CreateCall(push_f, { unwrap_gmachine_stack_ptr(f->arg_begin()), v });
+}
+void llvm_context::create_popn(Function* f, Value* off) {
+    auto popn_f = functions.at("stack_popn");
+    builder.CreateCall(popn_f, { unwrap_gmachine_stack_ptr(f->arg_begin()), off });
+}
+void llvm_context::create_update(Function* f, Value* off) {
+    auto update_f = functions.at("gmachine_update");
+    builder.CreateCall(update_f, { f->arg_begin(), off });
+}
+void llvm_context::create_pack(Function* f, Value* c, Value* t) {
+    auto pack_f = functions.at("gmachine_pack");
+    builder.CreateCall(pack_f, { f->arg_begin(), c, t });
+}
+void llvm_context::create_split(Function* f, Value* c) {
+    auto split_f = functions.at("gmachine_split");
+    builder.CreateCall(split_f, { f->arg_begin(), c });
+}
+void llvm_context::create_slide(Function* f, Value* off) {
+    auto slide_f = functions.at("gmachine_slide");
+    builder.CreateCall(slide_f, { f->arg_begin(), off });
+}
+void llvm_context::create_alloc(Function* f, Value* n) {
+    auto alloc_f = functions.at("gmachine_alloc");
+    builder.CreateCall(alloc_f, { f->arg_begin(), n });
+}
+Value* llvm_context::create_track(Function* f, Value* v) {
+    auto track_f = functions.at("gmachine_track");
+    return builder.CreateCall(track_f, { f->arg_begin(), v });
+}
+
+void llvm_context::create_unwind(Function* f) {
+    auto unwind_f = functions.at("unwind");
+    builder.CreateCall(unwind_f, { f->args().begin() });
+}
+
+Value* llvm_context::unwrap_gmachine_stack_ptr(Value* g) {
+    auto offset_0 = create_i32(0);
+    return builder.CreateGEP(g, { offset_0, offset_0 });
+}
+
+Value* llvm_context::unwrap_num(Value* v) {
+    auto num_ptr_type = PointerType::getUnqual(struct_types.at("node_num"));
+    auto cast = builder.CreatePointerCast(v, num_ptr_type);
+    auto offset_0 = create_i32(0);
+    auto offset_1 = create_i32(1);
+    auto int_ptr = builder.CreateGEP(cast, { offset_0, offset_1 });
+    return builder.CreateLoad(int_ptr);
+}
+Value* llvm_context::create_num(Function* f, Value* v) {
+    auto alloc_num_f = functions.at("alloc_num");
+    auto alloc_num_call = builder.CreateCall(alloc_num_f, { v });
+    return create_track(f, alloc_num_call);
+}
+
+Value* llvm_context::unwrap_data_tag(Value* v) {
+    auto data_ptr_type = PointerType::getUnqual(struct_types.at("node_data"));
+    auto cast = builder.CreatePointerCast(v, data_ptr_type);
+    auto offset_0 = create_i32(0);
+    auto offset_1 = create_i32(1);
+    auto tag_ptr = builder.CreateGEP(cast, { offset_0, offset_1 });
+    return builder.CreateLoad(tag_ptr);
+}
+
+Value* llvm_context::create_global(Function* f, Value* gf, Value* a) {
+    auto alloc_global_f = functions.at("alloc_global");
+    auto alloc_global_call = builder.CreateCall(alloc_global_f, { gf, a });
+    return create_track(f, alloc_global_call);
+}
+
+Value* llvm_context::create_app(Function* f, Value* l, Value* r) {
+    auto alloc_app_f = functions.at("alloc_app");
+    auto alloc_app_call = builder.CreateCall(alloc_app_f, { l, r });
+    return create_track(f, alloc_app_call);
+}
+
+llvm::Function* llvm_context::create_custom_function(const std::string& name, int32_t arity) {
+    auto void_type = llvm::Type::getVoidTy(ctx);
+    auto new_function = llvm::Function::Create(
+            function_type,
+            llvm::Function::LinkageTypes::ExternalLinkage,
+            "f_" + name,
+            &module
+    );
+    auto start_block = llvm::BasicBlock::Create(ctx, "entry", new_function);
+
+    auto new_custom_f = custom_function_ptr(new custom_function());
+    new_custom_f->arity = arity;
+    new_custom_f->function = new_function;
+    custom_functions["f_" + name] = std::move(new_custom_f);
+
+    return new_function;
+}
+
+llvm_context::custom_function& llvm_context::get_custom_function(const std::string& name) {
+    return *custom_functions.at("f_" + name);
+}

code/compiler/13/llvm_context.hpp

@@ -0,0 +1,81 @@
+#pragma once
+#include <llvm/IR/DerivedTypes.h>
+#include <llvm/IR/Function.h>
+#include <llvm/IR/LLVMContext.h>
+#include <llvm/IR/IRBuilder.h>
+#include <llvm/IR/Module.h>
+#include <llvm/IR/Value.h>
+#include <map>
+
+class llvm_context {
+    public:
+        struct custom_function {
+            llvm::Function* function;
+            int32_t arity;
+        };
+
+        using custom_function_ptr = std::unique_ptr<custom_function>;
+
+    private:
+        llvm::LLVMContext ctx;
+        llvm::IRBuilder<> builder;
+        llvm::Module module;
+
+        std::map<std::string, custom_function_ptr> custom_functions;
+        std::map<std::string, llvm::Function*> functions;
+        std::map<std::string, llvm::StructType*> struct_types;
+
+        llvm::StructType* stack_type;
+        llvm::StructType* gmachine_type;
+        llvm::PointerType* stack_ptr_type;
+        llvm::PointerType* gmachine_ptr_type;
+        llvm::PointerType* node_ptr_type;
+        llvm::IntegerType* tag_type;
+        llvm::FunctionType* function_type;
+
+        void create_types();
+        void create_functions();
+
+    public:
+        llvm_context()
+            : builder(ctx), module("bloglang", ctx) {
+                create_types();
+                create_functions();
+            }
+
+        llvm::IRBuilder<>& get_builder();
+        llvm::Module& get_module();
+
+        llvm::BasicBlock* create_basic_block(const std::string& name, llvm::Function* f);
+
+        llvm::ConstantInt* create_i8(int8_t);
+        llvm::ConstantInt* create_i32(int32_t);
+        llvm::ConstantInt* create_size(size_t);
+
+        llvm::Value* create_pop(llvm::Function*);
+        llvm::Value* create_peek(llvm::Function*, llvm::Value*);
+        void create_push(llvm::Function*, llvm::Value*);
+        void create_popn(llvm::Function*, llvm::Value*);
+        void create_update(llvm::Function*, llvm::Value*);
+        void create_pack(llvm::Function*, llvm::Value*, llvm::Value*);
+        void create_split(llvm::Function*, llvm::Value*);
+        void create_slide(llvm::Function*, llvm::Value*);
+        void create_alloc(llvm::Function*, llvm::Value*);
+        llvm::Value* create_track(llvm::Function*, llvm::Value*);
+
+        void create_unwind(llvm::Function*);
+
+        llvm::Value* unwrap_gmachine_stack_ptr(llvm::Value*);
+
+        llvm::Value* unwrap_num(llvm::Value*);
+        llvm::Value* create_num(llvm::Function*, llvm::Value*);
+
+        llvm::Value* unwrap_data_tag(llvm::Value*);
+
+        llvm::Value* create_global(llvm::Function*, llvm::Value*, llvm::Value*);
+
+        llvm::Value* create_app(llvm::Function*, llvm::Value*, llvm::Value*);
+
+        llvm::Function* create_custom_function(const std::string& name, int32_t arity);
+        custom_function& get_custom_function(const std::string& name);
+};

code/compiler/13/main.cpp

@@ -0,0 +1,27 @@
+#include "ast.hpp"
+#include <iostream>
+#include "parser.hpp"
+#include "compiler.hpp"
+#include "error.hpp"
+
+void yy::parser::error(const yy::location& loc, const std::string& msg) {
+    std::cerr << "An error occured: " << msg << std::endl;
+}
+
+int main(int argc, char** argv) {
+    if(argc != 2) {
+        std::cerr << "please enter a file to compile." << std::endl;
+        exit(1);
+    }
+    compiler cmp(argv[1]);
+
+    try {
+        cmp("program.o");
+    } catch(unification_error& err) {
+        err.pretty_print(std::cerr, cmp.get_file_manager(), cmp.get_type_manager());
+    } catch(type_error& err) {
+        err.pretty_print(std::cerr, cmp.get_file_manager());
+    } catch (compiler_error& err) {
+        err.pretty_print(std::cerr, cmp.get_file_manager());
+    }
+}

code/compiler/13/mangler.cpp

@@ -0,0 +1,17 @@
+#include "mangler.hpp"
+
+std::string mangler::new_mangled_name(const std::string& n) {
+    auto occurence_it = occurence_count.find(n);
+    int occurence = 0;
+    if(occurence_it != occurence_count.end()) {
+        occurence = occurence_it->second + 1;
+    }
+    occurence_count[n] = occurence;
+
+    std::string final_name = n;
+    if (occurence != 0) {
+        final_name += "_";
+        final_name += std::to_string(occurence);
+    }
+    return final_name;
+}

code/compiler/13/mangler.hpp

@@ -0,0 +1,11 @@
+#pragma once
+#include <string>
+#include <map>
+
+class mangler {
+    private:
+        std::map<std::string, int> occurence_count;
+
+    public:
+        std::string new_mangled_name(const std::string& str);
+};

code/compiler/13/parse_driver.cpp

@@ -0,0 +1,72 @@
+#include "parse_driver.hpp"
+#include "scanner.hpp"
+#include <sstream>
+
+file_mgr::file_mgr() : file_offset(0) {
+    line_offsets.push_back(0);
+}
+
+void file_mgr::write(const char* buf, size_t len) {
+    string_stream.write(buf, len);
+    file_offset += len;
+}
+
+void file_mgr::mark_line() {
+    line_offsets.push_back(file_offset);
+}
+
+void file_mgr::finalize() {
+    file_contents = string_stream.str();
+}
+
+size_t file_mgr::get_index(int line, int column) const {
+    assert(line > 0 && line <= line_offsets.size());
+    return line_offsets.at(line-1) + column - 1;
+}
+
+size_t file_mgr::get_line_end(int line) const {
+    if(line == line_offsets.size()) return file_contents.size();
+    return get_index(line+1, 1);
+}
+
+void file_mgr::print_location(
+        std::ostream& stream,
+        const yy::location& loc,
+        bool highlight) const {
+    size_t print_start = get_index(loc.begin.line, 1);
+    size_t highlight_start = get_index(loc.begin.line, loc.begin.column);
+    size_t highlight_end = get_index(loc.end.line, loc.end.column);
+    size_t print_end = get_line_end(loc.end.line);
+    const char* content = file_contents.c_str();
+    stream.write(content + print_start, highlight_start - print_start);
+    if(highlight) stream << "\033[4;31m";
+    stream.write(content + highlight_start, highlight_end - highlight_start);
+    if(highlight) stream << "\033[0m";
+    stream.write(content + highlight_end, print_end - highlight_end);
+}
+
+bool parse_driver::operator()() {
+    FILE* stream = fopen(file_name.c_str(), "r");
+    if(!stream) return false;
+    yyscan_t scanner;
+    yylex_init(&scanner);
+    yyset_in(stream, scanner);
+    yy::parser parser(scanner, *this);
+    parser();
+    yylex_destroy(scanner);
+    fclose(stream);
+    file_m->finalize();
+    return true;
+}
+
+yy::location& parse_driver::get_current_location() {
+    return location;
+}
+
+file_mgr& parse_driver::get_file_manager() const {
+    return *file_m;
+}
+
+definition_group& parse_driver::get_global_defs() const {
+    return *global_defs;
+}

code/compiler/13/parse_driver.hpp

@@ -0,0 +1,58 @@
+#pragma once
+#include <string>
+#include <fstream>
+#include <sstream>
+#include "definition.hpp"
+#include "location.hh"
+#include "parser.hpp"
+
+struct parse_driver;
+
+void scanner_init(parse_driver* d, yyscan_t* scanner);
+void scanner_destroy(yyscan_t* scanner);
+
+class file_mgr {
+    private:
+        std::ostringstream string_stream;
+        std::string file_contents;
+
+        size_t file_offset;
+        std::vector<size_t> line_offsets;
+    public:
+        file_mgr();
+
+        void write(const char* buffer, size_t len);
+        void mark_line();
+        void finalize();
+
+        size_t get_index(int line, int column) const;
+        size_t get_line_end(int line) const;
+        void print_location(
+                std::ostream& stream,
+                const yy::location& loc,
+                bool highlight = true) const;
+};
+
+class parse_driver {
+    private:
+        std::string file_name;
+        yy::location location;
+        definition_group* global_defs;
+        file_mgr* file_m;
+
+    public:
+        parse_driver(
+                file_mgr& mgr,
+                definition_group& defs,
+                const std::string& file)
+            : file_name(file), file_m(&mgr), global_defs(&defs) {}
+
+        bool operator()();
+        yy::location& get_current_location();
+        file_mgr& get_file_manager() const;
+        definition_group& get_global_defs() const;
+};
+
+#define YY_DECL yy::parser::symbol_type yylex(yyscan_t yyscanner, parse_driver& drv)
+
+YY_DECL;

code/compiler/13/parsed_type.cpp

@@ -0,0 +1,48 @@
+#include "parsed_type.hpp"
+#include <sstream>
+#include "type.hpp"
+#include "type_env.hpp"
+#include "error.hpp"
+
+type_ptr parsed_type_app::to_type(
+        const std::set<std::string>& vars,
+        const type_env& e) const {
+    auto parent_type = e.lookup_type(name);
+    if(parent_type == nullptr)
+        throw type_error("no such type or type constructor " + name);
+    type_base* base_type;
+    if(!(base_type = dynamic_cast<type_base*>(parent_type.get())))
+        throw type_error("invalid type " + name);
+    if(base_type->arity != arguments.size()) {
+        std::ostringstream error_stream;
+        error_stream << "invalid application of type ";
+        error_stream << name;
+        error_stream << " (" << base_type->arity << " argument(s) expected, ";
+        error_stream << "but " << arguments.size() << " provided)";
+        throw type_error(error_stream.str());
+    }
+
+    type_app* new_app = new type_app(std::move(parent_type));
+    type_ptr to_return(new_app);
+    for(auto& arg : arguments) {
+        new_app->arguments.push_back(arg->to_type(vars, e));
+    }
+    return to_return;
+}
+
+type_ptr parsed_type_var::to_type(
+        const std::set<std::string>& vars,
+        const type_env& e) const {
+    if(vars.find(var) == vars.end())
+        throw type_error("the type variable " + var + " was not explicitly declared.");
+    return type_ptr(new type_var(var));
+}
+
+
+type_ptr parsed_type_arr::to_type(
+        const std::set<std::string>& vars,
+        const type_env& env) const {
+    auto new_left = left->to_type(vars, env);
+    auto new_right = right->to_type(vars, env);
+    return type_ptr(new type_arr(std::move(new_left), std::move(new_right)));
+}

code/compiler/13/parsed_type.hpp

@@ -0,0 +1,43 @@
+#pragma once
+#include <memory>
+#include <set>
+#include <string>
+#include "type_env.hpp"
+
+struct parsed_type {
+    virtual type_ptr to_type(
+            const std::set<std::string>& vars,
+            const type_env& env) const = 0;
+};
+
+using parsed_type_ptr = std::unique_ptr<parsed_type>;
+
+struct parsed_type_app : parsed_type {
+    std::string name;
+    std::vector<parsed_type_ptr> arguments;
+
+    parsed_type_app(
+            std::string n,
+            std::vector<parsed_type_ptr> as)
+        : name(std::move(n)), arguments(std::move(as)) {}
+
+    type_ptr to_type(const std::set<std::string>& vars, const type_env& env) const;
+};
+
+struct parsed_type_var : parsed_type {
+    std::string var;
+
+    parsed_type_var(std::string v) : var(std::move(v)) {}
+
+    type_ptr to_type(const std::set<std::string>& vars, const type_env& env) const;
+};
+
+struct parsed_type_arr : parsed_type {
+    parsed_type_ptr left;
+    parsed_type_ptr right;
+
+    parsed_type_arr(parsed_type_ptr l, parsed_type_ptr r)
+        : left(std::move(l)), right(std::move(r)) {}
+
+    type_ptr to_type(const std::set<std::string>& vars, const type_env& env) const;
+};

code/compiler/13/parser.y

@@ -0,0 +1,180 @@
+%code requires {
+#include <string>
+#include <vector>
+#include "ast.hpp"
+#include "definition.hpp"
+#include "parser.hpp"
+#include "parsed_type.hpp"
+
+class parse_driver;
+using yyscan_t = void*;
+}
+
+%param { yyscan_t scanner }
+%param { parse_driver& drv }
+
+%code {
+#include "parse_driver.hpp"
+}
+
+%token BACKSLASH
+%token PLUS
+%token TIMES
+%token MINUS
+%token DIVIDE
+%token <int> INT
+%token DEFN
+%token DATA
+%token CASE
+%token OF
+%token LET
+%token IN
+%token OCURLY
+%token CCURLY
+%token OPAREN
+%token CPAREN
+%token COMMA
+%token ARROW
+%token EQUAL
+%token <std::string> LID
+%token <std::string> UID
+
+%language "c++"
+%define api.value.type variant
+%define api.token.constructor
+
+%locations
+
+%type <std::vector<std::string>> lowercaseParams
+%type <std::vector<branch_ptr>> branches
+%type <std::vector<constructor_ptr>> constructors
+%type <std::vector<parsed_type_ptr>> typeList
+%type <definition_group> definitions
+%type <parsed_type_ptr> type nonArrowType typeListElement
+%type <ast_ptr> aAdd aMul case let lambda app appBase
+%type <definition_data_ptr> data 
+%type <definition_defn_ptr> defn
+%type <branch_ptr> branch
+%type <pattern_ptr> pattern
+%type <constructor_ptr> constructor
+
+%start program
+
+%%
+
+program
+    : definitions { $1.vis = visibility::global; std::swap(drv.get_global_defs(), $1); }
+    ;
+
+definitions
+    : definitions defn { $$ = std::move($1); auto name = $2->name; $$.defs_defn[name] = std::move($2); }
+    | definitions data { $$ = std::move($1); auto name = $2->name; $$.defs_data[name] = std::move($2); }
+    | %empty { $$ = definition_group(); }
+    ;
+
+defn
+    : DEFN LID lowercaseParams EQUAL OCURLY aAdd CCURLY
+        { $$ = definition_defn_ptr(
+            new definition_defn(std::move($2), std::move($3), std::move($6), @$)); }
+    ;
+
+lowercaseParams
+    : %empty { $$ = std::vector<std::string>(); }
+    | lowercaseParams LID { $$ = std::move($1); $$.push_back(std::move($2)); }
+    ;
+
+aAdd
+    : aAdd PLUS aMul { $$ = ast_ptr(new ast_binop(PLUS, std::move($1), std::move($3), @$)); }
+    | aAdd MINUS aMul { $$ = ast_ptr(new ast_binop(MINUS, std::move($1), std::move($3), @$)); }
+    | aMul { $$ = std::move($1); }
+    ;
+
+aMul
+    : aMul TIMES app { $$ = ast_ptr(new ast_binop(TIMES, std::move($1), std::move($3), @$)); }
+    | aMul DIVIDE app { $$ = ast_ptr(new ast_binop(DIVIDE, std::move($1), std::move($3), @$)); }
+    | app { $$ = std::move($1); }
+    ;
+
+app
+    : app appBase { $$ = ast_ptr(new ast_app(std::move($1), std::move($2), @$)); }
+    | appBase { $$ = std::move($1); }
+    ;
+
+appBase
+    : INT { $$ = ast_ptr(new ast_int($1, @$)); }
+    | LID { $$ = ast_ptr(new ast_lid(std::move($1), @$)); }
+    | UID { $$ = ast_ptr(new ast_uid(std::move($1), @$)); }
+    | OPAREN aAdd CPAREN { $$ = std::move($2); }
+    | case { $$ = std::move($1); }
+    | let { $$ = std::move($1); }
+    | lambda { $$ = std::move($1); }
+    ;
+
+let
+    : LET OCURLY definitions CCURLY IN OCURLY aAdd CCURLY
+        { $$ = ast_ptr(new ast_let(std::move($3), std::move($7), @$)); }
+    ;
+
+lambda
+    : BACKSLASH lowercaseParams ARROW OCURLY aAdd CCURLY
+        { $$ = ast_ptr(new ast_lambda(std::move($2), std::move($5), @$)); }
+    ;
+
+case
+    : CASE aAdd OF OCURLY branches CCURLY 
+        { $$ = ast_ptr(new ast_case(std::move($2), std::move($5), @$)); }
+    ;
+
+branches
+    : branches branch { $$ = std::move($1); $$.push_back(std::move($2)); }
+    | branch { $$ = std::vector<branch_ptr>(); $$.push_back(std::move($1));}
+    ;
+
+branch
+    : pattern ARROW OCURLY aAdd CCURLY
+        { $$ = branch_ptr(new branch(std::move($1), std::move($4))); }
+    ;
+
+pattern
+    : LID { $$ = pattern_ptr(new pattern_var(std::move($1), @$)); }
+    | UID lowercaseParams
+        { $$ = pattern_ptr(new pattern_constr(std::move($1), std::move($2), @$)); }
+    ;
+
+data
+    : DATA UID lowercaseParams EQUAL OCURLY constructors CCURLY
+        { $$ = definition_data_ptr(new definition_data(std::move($2), std::move($3), std::move($6), @$)); }
+    ;
+
+constructors
+    : constructors COMMA constructor { $$ = std::move($1); $$.push_back(std::move($3)); }
+    | constructor
+        { $$ = std::vector<constructor_ptr>(); $$.push_back(std::move($1)); }
+    ;
+
+constructor
+    : UID typeList
+        { $$ = constructor_ptr(new constructor(std::move($1), std::move($2))); }
+    ;
+
+type
+    : nonArrowType ARROW type { $$ = parsed_type_ptr(new parsed_type_arr(std::move($1), std::move($3))); }
+    | nonArrowType { $$ = std::move($1); }
+    ;
+
+nonArrowType
+    : UID typeList { $$ = parsed_type_ptr(new parsed_type_app(std::move($1), std::move($2))); }
+    | LID { $$ = parsed_type_ptr(new parsed_type_var(std::move($1))); }
+    | OPAREN type CPAREN { $$ = std::move($2); }
+    ;
+
+typeListElement
+    : OPAREN type CPAREN { $$ = std::move($2); }
+    | UID { $$ = parsed_type_ptr(new parsed_type_app(std::move($1), {})); }
+    | LID { $$ = parsed_type_ptr(new parsed_type_var(std::move($1))); }
+    ;
+
+typeList
+    : %empty { $$ = std::vector<parsed_type_ptr>(); }
+    | typeList typeListElement { $$ = std::move($1); $$.push_back(std::move($2)); }
+    ;

code/compiler/13/runtime.c

@@ -0,0 +1,269 @@
+#include <stdint.h>
+#include <assert.h>
+#include <memory.h>
+#include <stdio.h>
+#include "runtime.h"
+
+struct node_base* alloc_node() {
+    struct node_base* new_node = malloc(sizeof(struct node_app));
+    new_node->gc_next = NULL;
+    new_node->gc_reachable = 0;
+    assert(new_node != NULL);
+    return new_node;
+}
+
+struct node_app* alloc_app(struct node_base* l, struct node_base* r) {
+    struct node_app* node = (struct node_app*) alloc_node();
+    node->base.tag = NODE_APP;
+    node->left = l;
+    node->right = r;
+    return node;
+}
+
+struct node_num* alloc_num(int32_t n) {
+    struct node_num* node = (struct node_num*) alloc_node();
+    node->base.tag = NODE_NUM;
+    node->value = n;
+    return node;
+}
+
+struct node_global* alloc_global(void (*f)(struct gmachine*), int32_t a) {
+    struct node_global* node = (struct node_global*) alloc_node();
+    node->base.tag = NODE_GLOBAL;
+    node->arity = a;
+    node->function = f;
+    return node;
+}
+
+struct node_ind* alloc_ind(struct node_base* n) {
+    struct node_ind* node = (struct node_ind*) alloc_node();
+    node->base.tag = NODE_IND;
+    node->next = n;
+    return node;
+}
+
+void free_node_direct(struct node_base* n) {
+    if(n->tag == NODE_DATA) {
+        free(((struct node_data*) n)->array);
+    }
+}
+
+void gc_visit_node(struct node_base* n) {
+    if(n->gc_reachable) return;
+    n->gc_reachable = 1;
+
+    if(n->tag == NODE_APP) {
+        struct node_app* app = (struct node_app*) n;
+        gc_visit_node(app->left);
+        gc_visit_node(app->right);
+    } if(n->tag == NODE_IND) {
+        struct node_ind* ind = (struct node_ind*) n;
+        gc_visit_node(ind->next);
+    } if(n->tag == NODE_DATA) {
+        struct node_data* data = (struct node_data*) n;
+        struct node_base** to_visit = data->array;
+        while(*to_visit) {
+            gc_visit_node(*to_visit);
+            to_visit++;
+        }
+    }
+}
+
+void stack_init(struct stack* s) {
+    s->size = 4;
+    s->count = 0;
+    s->data = malloc(sizeof(*s->data) * s->size);
+    assert(s->data != NULL);
+}
+
+void stack_free(struct stack* s) {
+    free(s->data);
+}
+
+void stack_push(struct stack* s, struct node_base* n) {
+    while(s->count >= s->size) {
+        s->data = realloc(s->data, sizeof(*s->data) * (s->size *= 2));
+        assert(s->data != NULL);
+    }
+    s->data[s->count++] = n;
+}
+
+struct node_base* stack_pop(struct stack* s) {
+    assert(s->count > 0);
+    return s->data[--s->count];
+}
+
+struct node_base* stack_peek(struct stack* s, size_t o) {
+    assert(s->count > o);
+    return s->data[s->count - o - 1];
+}
+
+void stack_popn(struct stack* s, size_t n) {
+    assert(s->count >= n);
+    s->count -= n;
+}
+
+void gmachine_init(struct gmachine* g) {
+    stack_init(&g->stack);
+    g->gc_nodes = NULL;
+    g->gc_node_count = 0;
+    g->gc_node_threshold = 128;
+}
+
+void gmachine_free(struct gmachine* g) {
+    stack_free(&g->stack);
+    struct node_base* to_free = g->gc_nodes;
+    struct node_base* next;
+
+    while(to_free) {
+        next = to_free->gc_next;
+        free_node_direct(to_free);
+        free(to_free);
+        to_free = next;
+    }
+}
+
+void gmachine_slide(struct gmachine* g, size_t n) {
+    assert(g->stack.count > n);
+    g->stack.data[g->stack.count - n - 1] = g->stack.data[g->stack.count - 1];
+    g->stack.count -= n;
+}
+
+void gmachine_update(struct gmachine* g, size_t o) {
+    assert(g->stack.count > o + 1);
+    struct node_ind* ind =
+        (struct node_ind*) g->stack.data[g->stack.count - o - 2];
+    ind->base.tag = NODE_IND;
+    ind->next = g->stack.data[g->stack.count -= 1];
+}
+
+void gmachine_alloc(struct gmachine* g, size_t o) {
+    while(o--) {
+        stack_push(&g->stack,
+                gmachine_track(g, (struct node_base*) alloc_ind(NULL)));
+    }
+}
+
+void gmachine_pack(struct gmachine* g, size_t n, int8_t t) {
+    assert(g->stack.count >= n);
+
+    struct node_base** data = malloc(sizeof(*data) * (n + 1));
+    assert(data != NULL);
+    memcpy(data, &g->stack.data[g->stack.count - n], n * sizeof(*data));
+    data[n] = NULL;
+
+    struct node_data* new_node = (struct node_data*) alloc_node();
+    new_node->array = data;
+    new_node->base.tag = NODE_DATA;
+    new_node->tag = t;
+
+    stack_popn(&g->stack, n);
+    stack_push(&g->stack, gmachine_track(g, (struct node_base*) new_node));
+}
+
+void gmachine_split(struct gmachine* g, size_t n) {
+    struct node_data* node = (struct node_data*) stack_pop(&g->stack);
+    for(size_t i = 0; i < n; i++) {
+        stack_push(&g->stack, node->array[i]);
+    }
+}
+
+struct node_base* gmachine_track(struct gmachine* g, struct node_base* b) {
+    g->gc_node_count++;
+    b->gc_next = g->gc_nodes;
+    g->gc_nodes = b;
+
+    if(g->gc_node_count >= g->gc_node_threshold) {
+        uint64_t nodes_before = g->gc_node_count;
+        gc_visit_node(b);
+        gmachine_gc(g);
+        g->gc_node_threshold = g->gc_node_count * 2;
+    }
+
+    return b;
+}
+
+void gmachine_gc(struct gmachine* g) {
+    for(size_t i = 0; i < g->stack.count; i++) {
+        gc_visit_node(g->stack.data[i]);
+    }
+
+    struct node_base** head_ptr = &g->gc_nodes;
+    while(*head_ptr) {
+        if((*head_ptr)->gc_reachable) {
+            (*head_ptr)->gc_reachable = 0;
+            head_ptr = &(*head_ptr)->gc_next;
+        } else {
+            struct node_base* to_free = *head_ptr;
+            *head_ptr = to_free->gc_next;
+            free_node_direct(to_free);
+            free(to_free);
+            g->gc_node_count--;
+        }
+    }
+}
+
+void unwind(struct gmachine* g) {
+    struct stack* s = &g->stack;
+
+    while(1) {
+        struct node_base* peek = stack_peek(s, 0);
+        if(peek->tag == NODE_APP) {
+            struct node_app* n = (struct node_app*) peek;
+            stack_push(s, n->left);
+        } else if(peek->tag == NODE_GLOBAL) {
+            struct node_global* n = (struct node_global*) peek;
+            assert(s->count > n->arity);
+
+            for(size_t i = 1; i <= n->arity; i++) {
+                s->data[s->count - i]
+                    = ((struct node_app*) s->data[s->count - i - 1])->right;
+            }
+
+            n->function(g);
+        } else if(peek->tag == NODE_IND) {
+            struct node_ind* n = (struct node_ind*) peek;
+            stack_pop(s);
+            stack_push(s, n->next);
+        } else {
+            break;
+        }
+    }
+}
+
+extern void f_main(struct gmachine* s);
+
+void print_node(struct node_base* n) {
+    if(n->tag == NODE_APP) {
+        struct node_app* app = (struct node_app*) n;
+        print_node(app->left);
+        putchar(' ');
+        print_node(app->right);
+    } else if(n->tag == NODE_DATA) {
+        printf("(Packed)");
+    } else if(n->tag == NODE_GLOBAL) {
+        struct node_global* global = (struct node_global*) n;
+        printf("(Global: %p)", global->function);
+    } else if(n->tag == NODE_IND) {
+        print_node(((struct node_ind*) n)->next);
+    } else if(n->tag == NODE_NUM) {
+        struct node_num* num = (struct node_num*) n;
+        printf("%d", num->value);
+    }
+}
+
+int main(int argc, char** argv) {
+    struct gmachine gmachine;
+    struct node_global* first_node = alloc_global(f_main, 0);
+    struct node_base* result;
+
+    gmachine_init(&gmachine);
+    gmachine_track(&gmachine, (struct node_base*) first_node);
+    stack_push(&gmachine.stack, (struct node_base*) first_node);
+    unwind(&gmachine);
+    result = stack_pop(&gmachine.stack);
+    printf("Result: ");
+    print_node(result);
+    putchar('\n');
+    gmachine_free(&gmachine);
+}

code/compiler/13/runtime.h

@@ -0,0 +1,84 @@
+#pragma once
+#include <stdlib.h>
+
+struct gmachine;
+
+enum node_tag {
+    NODE_APP,
+    NODE_NUM,
+    NODE_GLOBAL,
+    NODE_IND,
+    NODE_DATA
+};
+
+struct node_base {
+    enum node_tag tag;
+    int8_t gc_reachable;
+    struct node_base* gc_next;
+};
+
+struct node_app {
+    struct node_base base;
+    struct node_base* left;
+    struct node_base* right;
+};
+
+struct node_num {
+    struct node_base base;
+    int32_t value;
+};
+
+struct node_global {
+    struct node_base base;
+    int32_t arity;
+    void (*function)(struct gmachine*);
+};
+
+struct node_ind {
+    struct node_base base;
+    struct node_base* next;
+};
+
+struct node_data {
+    struct node_base base;
+    int8_t tag;
+    struct node_base** array;
+};
+
+struct node_base* alloc_node();
+struct node_app* alloc_app(struct node_base* l, struct node_base* r);
+struct node_num* alloc_num(int32_t n);
+struct node_global* alloc_global(void (*f)(struct gmachine*), int32_t a);
+struct node_ind* alloc_ind(struct node_base* n);
+void free_node_direct(struct node_base*);
+void gc_visit_node(struct node_base*);
+
+struct stack {
+    size_t size;
+    size_t count;
+    struct node_base** data;
+};
+
+void stack_init(struct stack* s);
+void stack_free(struct stack* s);
+void stack_push(struct stack* s, struct node_base* n);
+struct node_base* stack_pop(struct stack* s);
+struct node_base* stack_peek(struct stack* s, size_t o);
+void stack_popn(struct stack* s, size_t n);
+
+struct gmachine {
+    struct stack stack;
+    struct node_base* gc_nodes;
+    int64_t gc_node_count;
+    int64_t gc_node_threshold;
+};
+
+void gmachine_init(struct gmachine* g);
+void gmachine_free(struct gmachine* g);
+void gmachine_slide(struct gmachine* g, size_t n);
+void gmachine_update(struct gmachine* g, size_t o);
+void gmachine_alloc(struct gmachine* g, size_t o);
+void gmachine_pack(struct gmachine* g, size_t n, int8_t t);
+void gmachine_split(struct gmachine* g, size_t n);
+struct node_base* gmachine_track(struct gmachine* g, struct node_base* b);
+void gmachine_gc(struct gmachine* g);

code/compiler/13/scanner.l

@@ -0,0 +1,45 @@
+%option noyywrap
+%option reentrant
+%option header-file="scanner.hpp"
+
+%{
+#include <iostream>
+#include "ast.hpp"
+#include "definition.hpp"
+#include "parse_driver.hpp"
+#include "parser.hpp"
+
+#define YY_USER_ACTION \
+    drv.get_file_manager().write(yytext, yyleng); \
+    LOC.step(); LOC.columns(yyleng); 
+#define LOC drv.get_current_location()
+%}
+
+%%
+
+\n { drv.get_current_location().lines(); drv.get_file_manager().mark_line(); }
+[ ]+ {}
+\\ { return yy::parser::make_BACKSLASH(LOC); }
+\+ { return yy::parser::make_PLUS(LOC); }
+\* { return yy::parser::make_TIMES(LOC); }
+- { return yy::parser::make_MINUS(LOC); }
+\/ { return yy::parser::make_DIVIDE(LOC); }
+[0-9]+ { return yy::parser::make_INT(atoi(yytext), LOC); }
+defn { return yy::parser::make_DEFN(LOC); }
+data { return yy::parser::make_DATA(LOC); }
+case { return yy::parser::make_CASE(LOC); }
+of { return yy::parser::make_OF(LOC); }
+let { return yy::parser::make_LET(LOC); }
+in { return yy::parser::make_IN(LOC); }
+\{ { return yy::parser::make_OCURLY(LOC); }
+\} { return yy::parser::make_CCURLY(LOC); }
+\( { return yy::parser::make_OPAREN(LOC); }
+\) { return yy::parser::make_CPAREN(LOC); }
+,  { return yy::parser::make_COMMA(LOC); }
+-> { return yy::parser::make_ARROW(LOC); }
+= { return yy::parser::make_EQUAL(LOC); }
+[a-z][a-zA-Z]* { return yy::parser::make_LID(std::string(yytext), LOC); }
+[A-Z][a-zA-Z]* { return yy::parser::make_UID(std::string(yytext), LOC); }
+<<EOF>> { return yy::parser::make_YYEOF(LOC); }
+
+%%

code/compiler/13/test.cpp

@@ -0,0 +1,23 @@
+#include "graph.hpp"
+
+int main() {
+    function_graph graph;
+    graph.add_edge("f", "g");
+    graph.add_edge("g", "h");
+    graph.add_edge("h", "f");
+
+    graph.add_edge("i", "j");
+    graph.add_edge("j", "i");
+
+    graph.add_edge("j", "f");
+
+    graph.add_edge("x", "f");
+    graph.add_edge("x", "i");
+
+    for(auto& group : graph.compute_order()) {
+        std::cout << "Group: " << std::endl;
+        for(auto& member : group->members) {
+            std::cout << member << std::endl;
+        }
+    }
+}

code/compiler/13/type.cpp

@@ -0,0 +1,213 @@
+#include "type.hpp"
+#include <ostream>
+#include <sstream>
+#include <algorithm>
+#include <vector>
+#include "error.hpp"
+
+void type_scheme::print(const type_mgr& mgr, std::ostream& to) const {
+    if(forall.size() != 0) {
+        to << "forall ";
+        for(auto& var : forall) {
+            to << var << " ";
+        }
+        to << ". ";
+    }
+    monotype->print(mgr, to);
+}
+
+type_ptr type_scheme::instantiate(type_mgr& mgr) const {
+    if(forall.size() == 0) return monotype;
+    std::map<std::string, type_ptr> subst;
+    for(auto& var : forall) {
+        subst[var] = mgr.new_type();
+    }
+    return mgr.substitute(subst, monotype);
+}
+
+void type_var::print(const type_mgr& mgr, std::ostream& to) const {
+    auto type = mgr.lookup(name);
+    if(type) {
+        type->print(mgr, to);
+    } else {
+        to << name;
+    }
+}
+
+void type_base::print(const type_mgr& mgr, std::ostream& to) const {
+    to << name;
+}
+
+void type_arr::print(const type_mgr& mgr, std::ostream& to) const {
+    type_var* var;
+    bool print_parenths = dynamic_cast<type_arr*>(mgr.resolve(left, var).get()) != nullptr;
+    if(print_parenths) to << "(";
+    left->print(mgr, to);
+    if(print_parenths) to << ")";
+    to << " -> ";
+    right->print(mgr, to);
+}
+
+void type_app::print(const type_mgr& mgr, std::ostream& to) const {
+    constructor->print(mgr, to);
+    to << "*";
+    for(auto& arg : arguments) {
+        to << " ";
+        arg->print(mgr, to);
+    }
+}
+
+std::string type_mgr::new_type_name() {
+    int temp = last_id++;
+    std::string str = "";
+
+    while(temp != -1) {
+        str += (char) ('a' + (temp % 26));
+        temp = temp / 26 - 1;
+    }
+
+    std::reverse(str.begin(), str.end());
+    return str;
+}
+
+type_ptr type_mgr::new_type() {
+    return type_ptr(new type_var(new_type_name()));
+}
+
+type_ptr type_mgr::new_arrow_type() {
+    return type_ptr(new type_arr(new_type(), new_type()));
+}
+
+type_ptr type_mgr::lookup(const std::string& var) const {
+    auto types_it = types.find(var);
+    if(types_it != types.end()) return types_it->second;
+    return nullptr;
+}
+
+type_ptr type_mgr::resolve(type_ptr t, type_var*& var) const {
+    type_var* cast;
+
+    var = nullptr;
+    while((cast = dynamic_cast<type_var*>(t.get()))) {
+        auto it = types.find(cast->name);
+
+        if(it == types.end()) {
+            var = cast;
+            break;
+        }
+        t = it->second;
+    }
+
+    return t;
+}
+
+void type_mgr::unify(type_ptr l, type_ptr r, const std::optional<yy::location>& loc) {
+    type_var *lvar, *rvar;
+    type_arr *larr, *rarr;
+    type_base *lid, *rid;
+    type_app *lapp, *rapp;
+
+    l = resolve(l, lvar);
+    r = resolve(r, rvar);
+
+    if(lvar) {
+        bind(lvar->name, r);
+        return;
+    } else if(rvar) {
+        bind(rvar->name, l);
+        return;
+    } else if((larr = dynamic_cast<type_arr*>(l.get())) &&
+            (rarr = dynamic_cast<type_arr*>(r.get()))) {
+        unify(larr->left, rarr->left, loc);
+        unify(larr->right, rarr->right, loc);
+        return;
+    } else if((lid = dynamic_cast<type_base*>(l.get())) &&
+            (rid = dynamic_cast<type_base*>(r.get()))) {
+        if(lid->name == rid->name &&
+                lid->arity == rid->arity)
+            return;
+    } else if((lapp = dynamic_cast<type_app*>(l.get())) &&
+            (rapp = dynamic_cast<type_app*>(r.get()))) {
+        unify(lapp->constructor, rapp->constructor, loc);
+        auto left_it = lapp->arguments.begin();
+        auto right_it = rapp->arguments.begin();
+        while(left_it != lapp->arguments.end() &&
+                right_it != rapp->arguments.end()) {
+            unify(*left_it, *right_it, loc);
+            left_it++, right_it++;
+        }
+        return;
+    }
+
+    throw unification_error(l, r, loc);
+}
+
+type_ptr type_mgr::substitute(const std::map<std::string, type_ptr>& subst, const type_ptr& t) const {
+    type_ptr temp = t;
+    while(type_var* var = dynamic_cast<type_var*>(temp.get())) {
+        auto subst_it = subst.find(var->name);
+        if(subst_it != subst.end()) return subst_it->second;
+        auto var_it = types.find(var->name);
+        if(var_it == types.end()) return t;
+        temp = var_it->second;
+    }
+
+    if(type_arr* arr = dynamic_cast<type_arr*>(temp.get())) {
+        auto left_result = substitute(subst, arr->left);
+        auto right_result = substitute(subst, arr->right);
+        if(left_result == arr->left && right_result == arr->right) return t;
+        return type_ptr(new type_arr(left_result, right_result));
+    } else if(type_app* app = dynamic_cast<type_app*>(temp.get())) {
+        auto constructor_result = substitute(subst, app->constructor);
+        bool arg_changed = false;
+        std::vector<type_ptr> new_args;
+        for(auto& arg : app->arguments) {
+            auto arg_result = substitute(subst, arg);
+            arg_changed |= arg_result != arg;
+            new_args.push_back(std::move(arg_result));
+        }
+
+        if(constructor_result == app->constructor && !arg_changed) return t;
+        type_app* new_app = new type_app(std::move(constructor_result));
+        std::swap(new_app->arguments, new_args);
+        return type_ptr(new_app);
+    }
+    return t;
+}
+
+void type_mgr::bind(const std::string& s, type_ptr t) {
+    type_var* other = dynamic_cast<type_var*>(t.get());
+    
+    if(other && other->name == s) return;
+    types[s] = t;
+}
+
+void type_mgr::find_free(const type_ptr& t, std::set<std::string>& into) const {
+    type_var* var;
+    type_ptr resolved = resolve(t, var);
+
+    if(var) {
+        into.insert(var->name);
+    } else if(type_arr* arr = dynamic_cast<type_arr*>(resolved.get())) {
+        find_free(arr->left, into);
+        find_free(arr->right, into);
+    } else if(type_app* app = dynamic_cast<type_app*>(resolved.get())) {
+        find_free(app->constructor, into);
+        for(auto& arg : app->arguments) find_free(arg, into);
+    }
+}
+
+void type_mgr::find_free(const type_scheme_ptr& t, std::set<std::string>& into) const {
+    std::set<std::string> monotype_free;
+    type_mgr limited_mgr;
+    for(auto& binding : types) {
+        auto existing_position = std::find(t->forall.begin(), t->forall.end(), binding.first);
+        if(existing_position != t->forall.end()) continue;
+        limited_mgr.types[binding.first] = binding.second;
+    }
+    limited_mgr.find_free(t->monotype, monotype_free);
+    for(auto& not_free : t->forall) {
+        monotype_free.erase(not_free);
+    }
+    into.insert(monotype_free.begin(), monotype_free.end());
+}

code/compiler/13/type.hpp

@@ -0,0 +1,101 @@
+#pragma once
+#include <memory>
+#include <map>
+#include <string>
+#include <vector>
+#include <set>
+#include <optional>
+#include "location.hh"
+
+class type_mgr;
+
+struct type {
+    virtual ~type() = default;
+
+    virtual void print(const type_mgr& mgr, std::ostream& to) const = 0;
+};
+
+using type_ptr = std::shared_ptr<type>;
+
+struct type_scheme {
+    std::vector<std::string> forall;
+    type_ptr monotype;
+
+    type_scheme(type_ptr type) : forall(), monotype(std::move(type)) {}
+
+    void print(const type_mgr& mgr, std::ostream& to) const;
+    type_ptr instantiate(type_mgr& mgr) const;
+};
+
+using type_scheme_ptr = std::shared_ptr<type_scheme>;
+
+struct type_var : public type {
+    std::string name;
+
+    type_var(std::string n)
+        : name(std::move(n)) {}
+
+    void print(const type_mgr& mgr, std::ostream& to) const;
+};
+
+struct type_base : public type {
+    std::string name;
+    int32_t arity;
+
+    type_base(std::string n, int32_t a = 0) 
+        : name(std::move(n)), arity(a) {}
+
+    void print(const type_mgr& mgr, std::ostream& to) const;
+};
+
+struct type_data : public type_base {
+    struct constructor {
+        int tag;
+    };
+
+    std::map<std::string, constructor> constructors;
+
+    type_data(std::string n, int32_t a = 0)
+        : type_base(std::move(n), a) {}
+};
+
+struct type_arr : public type {
+    type_ptr left;
+    type_ptr right;
+
+    type_arr(type_ptr l, type_ptr r)
+        : left(std::move(l)), right(std::move(r)) {}
+
+    void print(const type_mgr& mgr, std::ostream& to) const;
+};
+
+struct type_app : public type {
+    type_ptr constructor;
+    std::vector<type_ptr> arguments;
+
+    type_app(type_ptr c)
+        : constructor(std::move(c)) {}
+
+    void print(const type_mgr& mgr, std::ostream& to) const;
+};
+
+class type_mgr {
+    private:
+        int last_id = 0;
+        std::map<std::string, type_ptr> types;
+
+    public:
+        std::string new_type_name();
+        type_ptr new_type();
+        type_ptr new_arrow_type();
+
+        void unify(type_ptr l, type_ptr r, const std::optional<yy::location>& loc = std::nullopt);
+        type_ptr substitute(
+                const std::map<std::string, type_ptr>& subst,
+                const type_ptr& t) const;
+        type_ptr lookup(const std::string& var) const;
+        type_ptr resolve(type_ptr t, type_var*& var) const;
+        void bind(const std::string& s, type_ptr t);
+        void find_free(const type_ptr& t, std::set<std::string>& into) const;
+        void find_free(const type_scheme_ptr& t, std::set<std::string>& into) const;
+};

code/compiler/13/type_env.cpp

@@ -0,0 +1,96 @@
+#include "type_env.hpp"
+#include "type.hpp"
+#include "error.hpp"
+#include <cassert>
+
+void type_env::find_free(const type_mgr& mgr, std::set<std::string>& into) const {
+    if(parent != nullptr) parent->find_free(mgr, into);
+    for(auto& binding : names) {
+        mgr.find_free(binding.second.type, into);
+    }
+}
+
+void type_env::find_free_except(const type_mgr& mgr, const group& avoid,
+        std::set<std::string>& into) const {
+    if(parent != nullptr) parent->find_free(mgr, into);
+    for(auto& binding : names) {
+        if(avoid.members.find(binding.first) != avoid.members.end()) continue;
+        mgr.find_free(binding.second.type, into);
+    }
+}
+
+type_scheme_ptr type_env::lookup(const std::string& name) const {
+    auto it = names.find(name);
+    if(it != names.end()) return it->second.type;
+    if(parent) return parent->lookup(name);
+    return nullptr;
+}
+
+bool type_env::is_global(const std::string& name) const {
+    auto it = names.find(name);
+    if(it != names.end()) return it->second.vis == visibility::global;
+    if(parent) return parent->is_global(name);
+    return false;
+}
+
+void type_env::set_mangled_name(const std::string& name, const std::string& mangled) {
+    auto it = names.find(name);
+
+    // Can't set mangled name for non-existent variable.
+    assert(it != names.end());
+    // Local names shouldn't need mangling.
+    assert(it->second.vis == visibility::global);
+
+    it->second.mangled_name = mangled;
+}
+
+const std::string& type_env::get_mangled_name(const std::string& name) const {
+    auto it = names.find(name);
+    if(it != names.end()) {
+        assert(it->second.mangled_name);
+        return *it->second.mangled_name;
+    }
+    assert(parent != nullptr);
+    return parent->get_mangled_name(name);
+}
+
+type_ptr type_env::lookup_type(const std::string& name) const {
+    auto it = type_names.find(name);
+    if(it != type_names.end()) return it->second;
+    if(parent) return parent->lookup_type(name);
+    return nullptr;
+}
+
+void type_env::bind(const std::string& name, type_ptr t, visibility v) {
+    type_scheme_ptr new_scheme(new type_scheme(std::move(t)));
+    names[name] = variable_data(std::move(new_scheme), v, std::nullopt);
+}
+
+void type_env::bind(const std::string& name, type_scheme_ptr t, visibility v) {
+    names[name] = variable_data(std::move(t), v, "");
+}
+
+void type_env::bind_type(const std::string& type_name, type_ptr t) {
+    if(lookup_type(type_name) != nullptr)
+        throw type_error("redefinition of type");
+    type_names[type_name] = t;
+}
+
+void type_env::generalize(const std::string& name, const group& grp, type_mgr& mgr) {
+    auto names_it = names.find(name);
+    assert(names_it != names.end());
+    assert(names_it->second.type->forall.size() == 0);
+
+    std::set<std::string> free_in_type;
+    std::set<std::string> free_in_env;
+    mgr.find_free(names_it->second.type->monotype, free_in_type);
+    find_free_except(mgr, grp, free_in_env);
+    for(auto& free : free_in_type) {
+        if(free_in_env.find(free) != free_in_env.end()) continue;
+        names_it->second.type->forall.push_back(free);
+    }
+}
+
+type_env_ptr type_scope(type_env_ptr parent) {
+    return type_env_ptr(new type_env(std::move(parent)));
+}

code/compiler/13/type_env.hpp

@@ -0,0 +1,52 @@
+#pragma once
+#include <map>
+#include <string>
+#include <set>
+#include <optional>
+#include "graph.hpp"
+#include "type.hpp"
+
+struct type_env;
+using type_env_ptr = std::shared_ptr<type_env>;
+
+enum class visibility { global,local };
+
+class type_env {
+    private:
+        struct variable_data {
+            type_scheme_ptr type;
+            visibility vis;
+            std::optional<std::string> mangled_name;
+
+            variable_data()
+                : variable_data(nullptr, visibility::local, std::nullopt) {}
+            variable_data(type_scheme_ptr t, visibility v, std::optional<std::string> n)
+                : type(std::move(t)), vis(v), mangled_name(std::move(n)) {}
+        };
+
+        type_env_ptr parent;
+        std::map<std::string, variable_data> names;
+        std::map<std::string, type_ptr> type_names;
+
+    public:
+        type_env(type_env_ptr p) : parent(std::move(p)) {}
+        type_env() : type_env(nullptr) {}
+
+        void find_free(const type_mgr& mgr, std::set<std::string>& into) const;
+        void find_free_except(const type_mgr& mgr, const group& avoid,
+                std::set<std::string>& into) const;
+        type_scheme_ptr lookup(const std::string& name) const;
+        bool is_global(const std::string& name) const;
+        void set_mangled_name(const std::string& name, const std::string& mangled);
+        const std::string& get_mangled_name(const std::string& name) const;
+        type_ptr lookup_type(const std::string& name) const;
+        void bind(const std::string& name, type_ptr t,
+                visibility v = visibility::local);
+        void bind(const std::string& name, type_scheme_ptr t,
+                visibility v = visibility::local);
+        void bind_type(const std::string& type_name, type_ptr t);
+        void generalize(const std::string& name, const group& grp, type_mgr& mgr);
+};
+
+
+type_env_ptr type_scope(type_env_ptr parent);

code/dawn/Dawn.v

@@ -0,0 +1,179 @@
+Require Import Coq.Lists.List.
+From Ltac2 Require Import Ltac2.
+
+Inductive intrinsic :=
+  | swap
+  | clone
+  | drop
+  | quote
+  | compose
+  | apply.
+
+Inductive expr :=
+  | e_int (i : intrinsic)
+  | e_quote (e : expr)
+  | e_comp (e1 e2 : expr).
+
+Definition e_compose (e : expr) (es : list expr) := fold_left e_comp es e.
+
+Inductive IsValue : expr -> Prop :=
+  | Val_quote : forall {e : expr}, IsValue (e_quote e).
+
+Definition value := { v : expr & IsValue v }.
+Definition value_stack := list value.
+
+Definition v_quote (e : expr) := existT IsValue (e_quote e) Val_quote.
+
+Inductive Sem_int : value_stack -> intrinsic -> value_stack -> Prop :=
+  | Sem_swap : forall (v v' : value) (vs : value_stack), Sem_int (v' :: v :: vs) swap (v :: v' :: vs)
+  | Sem_clone : forall (v : value) (vs : value_stack), Sem_int (v :: vs) clone (v :: v :: vs)
+  | Sem_drop : forall (v : value) (vs : value_stack), Sem_int (v :: vs) drop vs
+  | Sem_quote : forall (v : value) (vs : value_stack), Sem_int (v :: vs) quote ((v_quote (projT1 v)) :: vs)
+  | Sem_compose : forall (e e' : expr) (vs : value_stack), Sem_int (v_quote e' :: v_quote e :: vs) compose (v_quote (e_comp e e') :: vs)
+  | Sem_apply : forall (e : expr) (vs vs': value_stack), Sem_expr vs e vs' -> Sem_int (v_quote e :: vs) apply vs'
+
+with Sem_expr : value_stack -> expr -> value_stack -> Prop :=
+  | Sem_e_int : forall (i : intrinsic) (vs vs' : value_stack), Sem_int vs i vs' -> Sem_expr vs (e_int i) vs'
+  | Sem_e_quote : forall (e : expr) (vs : value_stack), Sem_expr vs (e_quote e) (v_quote e :: vs)
+  | Sem_e_comp : forall (e1 e2 : expr) (vs1 vs2 vs3 : value_stack),
+      Sem_expr vs1 e1 vs2 -> Sem_expr vs2 e2 vs3 -> Sem_expr vs1 (e_comp e1 e2) vs3.
+
+Definition false : expr := e_quote (e_int drop).
+Definition false_v : value := v_quote (e_int drop).
+
+Definition true : expr := e_quote (e_comp (e_int swap) (e_int drop)).
+Definition true_v : value := v_quote (e_comp (e_int swap) (e_int drop)).
+
+Theorem false_correct : forall (v v' : value) (vs : value_stack), Sem_expr (v' :: v :: vs) (e_comp false (e_int apply)) (v :: vs).
+Proof.
+  intros v v' vs.
+  eapply Sem_e_comp.
+  - apply Sem_e_quote.
+  - apply Sem_e_int. apply Sem_apply. apply Sem_e_int. apply Sem_drop.
+Qed.
+
+Theorem true_correct : forall (v v' : value) (vs : value_stack), Sem_expr (v' :: v :: vs) (e_comp true (e_int apply)) (v' :: vs).
+Proof.
+  intros v v' vs.
+  eapply Sem_e_comp.
+  - apply Sem_e_quote.
+  - apply Sem_e_int. apply Sem_apply. eapply Sem_e_comp.
+    * apply Sem_e_int. apply Sem_swap.
+    * apply Sem_e_int. apply Sem_drop.
+Qed.
+
+Definition or : expr := e_comp (e_int clone) (e_int apply).
+
+Theorem or_false_v : forall (v : value) (vs : value_stack), Sem_expr (false_v :: v :: vs) or (v :: vs).
+Proof with apply Sem_e_int.
+  intros v vs.
+  eapply Sem_e_comp...
+  - apply Sem_clone.
+  - apply Sem_apply... apply Sem_drop.
+Qed.
+
+Theorem or_true : forall (v : value) (vs : value_stack), Sem_expr (true_v :: v :: vs) or (true_v :: vs).
+Proof with apply Sem_e_int.
+  intros v vs.
+  eapply Sem_e_comp...
+  - apply Sem_clone...
+  - apply Sem_apply. eapply Sem_e_comp...
+    * apply Sem_swap.
+    * apply Sem_drop.
+Qed.
+
+Definition or_false_false := or_false_v false_v.
+Definition or_false_true := or_false_v true_v.
+Definition or_true_false := or_true false_v.
+Definition or_true_true := or_true true_v.
+
+Fixpoint quote_n (n : nat) :=
+  match n with
+  | O => e_int quote
+  | S n' => e_compose (quote_n n') (e_int swap :: e_int quote :: e_int swap :: e_int compose :: nil)
+  end.
+
+Theorem quote_2_correct : forall (v1 v2 : value) (vs : value_stack),
+    Sem_expr (v2 :: v1 :: vs) (quote_n 1) (v_quote (e_comp (projT1 v1) (projT1 v2)) :: vs).
+Proof with apply Sem_e_int.
+  intros v1 v2 vs. simpl.
+  repeat (eapply Sem_e_comp)...
+  - apply Sem_quote.
+  - apply Sem_swap.
+  - apply Sem_quote.
+  - apply Sem_swap.
+  - apply Sem_compose.
+Qed.
+
+Theorem quote_3_correct : forall (v1 v2 v3 : value) (vs : value_stack),
+  Sem_expr (v3 :: v2 :: v1 :: vs) (quote_n 2) (v_quote (e_comp (projT1 v1) (e_comp (projT1 v2) (projT1 v3))) :: vs).
+Proof with apply Sem_e_int.
+  intros v1 v2 v3 vs. simpl.
+  repeat (eapply Sem_e_comp)...
+  - apply Sem_quote.
+  - apply Sem_swap.
+  - apply Sem_quote.
+  - apply Sem_swap.
+  - apply Sem_compose.
+  - apply Sem_swap.
+  - apply Sem_quote.
+  - apply Sem_swap.
+  - apply Sem_compose.
+Qed.
+
+Ltac2 rec solve_basic () := Control.enter (fun _ =>
+  match! goal with
+  | [|- Sem_int ?vs1 swap ?vs2] => apply Sem_swap
+  | [|- Sem_int ?vs1 clone ?vs2] => apply Sem_clone
+  | [|- Sem_int ?vs1 drop ?vs2] => apply Sem_drop
+  | [|- Sem_int ?vs1 quote ?vs2] => apply Sem_quote
+  | [|- Sem_int ?vs1 compose ?vs2] => apply Sem_compose
+  | [|- Sem_int ?vs1 apply ?vs2] => apply Sem_apply
+  | [|- Sem_expr ?vs1 (e_comp ?e1 ?e2) ?vs2] => eapply Sem_e_comp; solve_basic ()
+  | [|- Sem_expr ?vs1 (e_int ?e) ?vs2] => apply Sem_e_int; solve_basic ()
+  | [|- Sem_expr ?vs1 (e_quote ?e) ?vs2] => apply Sem_e_quote
+  | [_ : _ |- _] => ()
+  end).
+
+Theorem quote_2_correct' : forall (v1 v2 : value) (vs : value_stack),
+    Sem_expr (v2 :: v1 :: vs) (quote_n 1) (v_quote (e_comp (projT1 v1) (projT1 v2)) :: vs).
+Proof. intros. simpl. solve_basic (). Qed.
+
+Theorem quote_3_correct' : forall (v1 v2 v3 : value) (vs : value_stack),
+  Sem_expr (v3 :: v2 :: v1 :: vs) (quote_n 2) (v_quote (e_comp (projT1 v1) (e_comp (projT1 v2) (projT1 v3))) :: vs).
+Proof. intros. simpl. solve_basic (). Qed.
+
+Definition rotate_n (n : nat) := e_compose (quote_n n) (e_int swap :: e_int quote :: e_int compose :: e_int apply :: nil).
+
+Lemma eval_value : forall (v : value) (vs : value_stack),
+  Sem_expr vs (projT1 v) (v :: vs).
+Proof.
+  intros v vs.
+  destruct v. destruct i.
+  simpl. apply Sem_e_quote.
+Qed.
+
+Theorem rotate_3_correct : forall (v1 v2 v3 : value) (vs : value_stack),
+  Sem_expr (v3 :: v2 :: v1 :: vs) (rotate_n 1) (v1 :: v3 :: v2 :: vs).
+Proof.
+  intros. unfold rotate_n. simpl. solve_basic ().
+  repeat (eapply Sem_e_comp); apply eval_value.
+Qed.
+
+Theorem rotate_4_correct : forall (v1 v2 v3 v4 : value) (vs : value_stack),
+  Sem_expr (v4 :: v3 :: v2 :: v1 :: vs) (rotate_n 2) (v1 :: v4 :: v3 :: v2 :: vs).
+Proof.
+  intros. unfold rotate_n. simpl. solve_basic ().
+  repeat (eapply Sem_e_comp); apply eval_value.
+Qed.
+
+Theorem e_comp_assoc : forall (e1 e2 e3 : expr) (vs vs' : value_stack),
+  Sem_expr vs (e_comp e1 (e_comp e2 e3)) vs' <-> Sem_expr vs (e_comp (e_comp e1 e2) e3) vs'.
+Proof.
+  intros e1 e2 e3 vs vs'.
+  split; intros Heval.
+  - inversion Heval; subst. inversion H4; subst.
+    eapply Sem_e_comp. eapply Sem_e_comp. apply H2. apply H3. apply H6.
+  - inversion Heval; subst. inversion H2; subst.
+    eapply Sem_e_comp. apply H3. eapply Sem_e_comp. apply H6. apply H4.
+Qed.

code/dawn/DawnEval.v

@@ -0,0 +1,254 @@
+Require Import Coq.Lists.List.
+Require Import DawnV2.
+Require Import Coq.Program.Equality.
+From Ltac2 Require Import Ltac2.
+
+Inductive step_result :=
+  | err
+  | middle (e : expr) (s : value_stack)
+  | final (s : value_stack).
+
+Fixpoint eval_step (s : value_stack) (e : expr) : step_result :=
+  match e, s with
+  | e_int swap, v' :: v :: vs => final (v :: v' :: vs)
+  | e_int clone, v :: vs => final (v :: v :: vs)
+  | e_int drop, v :: vs => final vs
+  | e_int quote, v :: vs => final (v_quote (value_to_expr v) :: vs)
+  | e_int compose, (v_quote v2) :: (v_quote v1) :: vs => final (v_quote (e_comp v1 v2) :: vs)
+  | e_int apply, (v_quote v1) :: vs => middle v1 vs
+  | e_quote e', vs => final (v_quote e' :: vs)
+  | e_comp e1 e2, vs =>
+      match eval_step vs e1 with
+      | final vs' => middle e2 vs'
+      | middle e1' vs' => middle (e_comp e1' e2) vs'
+      | err => err
+      end
+  | _, _ => err
+  end.
+
+Theorem eval_step_correct : forall (e : expr) (vs vs' : value_stack), Sem_expr vs e vs' ->
+  (eval_step vs e = final vs') \/
+  (exists (ei : expr) (vsi : value_stack),
+    eval_step vs e = middle ei vsi /\
+    Sem_expr vsi ei vs').
+Proof.
+  intros e vs vs' Hsem.
+  (* Proceed by induction on the semantics. *)
+  induction Hsem.
+  - inversion H; (* The expression is just an intrnsic. *)
+    (* Dismiss all the straightforward "final" cases,
+       of which most intrinsics are. *)
+    try (left; reflexivity).
+    (* Only apply remains; We are in an intermediate / middle case. *)
+    right.
+    (* The semantics guarantee that the expression in the
+       quote evaluates to the final state. *)
+    exists e, vs0. auto.
+  - (* The expression is a quote. This is yet another final case. *)
+    left; reflexivity.
+  - (* The composition is never a final step, since we have to evaluate both
+       branches to "finish up". *)
+    destruct IHHsem1; right.
+    + (* If the left branch finihed, only the right branch needs to be evaluted. *)
+      simpl. rewrite H. exists e2, vs2. auto.
+    + (* Otherwise, the left branch has an intermediate evaluation, guaranteed
+         by induction to be consitent. *)
+      destruct H as [ei [vsi [Heval Hsem']]].
+      (* We compose the remaining part of the left branch with the right branch. *)
+      exists (e_comp ei e2), vsi. simpl.
+      (* The evaluation is trivially to a "middle" state. *)
+      rewrite Heval. split. auto.
+      eapply Sem_e_comp. apply Hsem'. apply Hsem2.
+Qed.
+
+Inductive eval_chain (vs : value_stack) (e : expr) (vs' : value_stack) : Prop :=
+  | chain_final (P : eval_step vs e = final vs')
+  | chain_middle (ei : expr) (vsi : value_stack)
+      (P : eval_step vs e = middle ei vsi) (rest : eval_chain vsi ei vs').
+
+Lemma eval_chain_merge : forall (e1 e2 : expr) (vs vs' vs'' : value_stack),
+  eval_chain vs e1 vs' -> eval_chain vs' e2 vs'' -> eval_chain vs (e_comp e1 e2) vs''.
+Proof.
+  intros e1 e2 vs vs' vs'' ch1 ch2.
+  induction ch1;
+  eapply chain_middle; simpl; try (rewrite P); auto.
+Qed.
+
+Lemma eval_chain_split : forall (e1 e2 : expr) (vs vs'' : value_stack),
+  eval_chain vs (e_comp e1 e2) vs'' -> exists vs', (eval_chain vs e1 vs') /\ (eval_chain vs' e2 vs'').
+Proof.
+  intros e1 e2 vs vss'' ch.
+  ltac1:(dependent induction ch).
+  - simpl in P. destruct (eval_step vs e1); inversion P.
+  - simpl in P. destruct (eval_step vs e1) eqn:Hval; try (inversion P).
+    + injection P as Hinj; subst. specialize (IHch e e2 H0) as [s'0 [ch1 ch2]].
+      eexists. split.
+      * eapply chain_middle. apply Hval. apply ch1.
+      * apply ch2.
+    + subst. eexists. split.
+      * eapply chain_final. apply Hval.
+      * apply ch.
+Qed.
+
+Theorem val_step_sem : forall (e : expr) (vs vs' : value_stack),
+  Sem_expr vs e vs' -> eval_chain vs e vs'
+with eval_step_int : forall (i : intrinsic) (vs vs' : value_stack),
+  Sem_int vs i vs' -> eval_chain vs (e_int i) vs'.
+Proof.
+  - intros e vs vs' Hsem.
+    induction Hsem.
+    + (* This is an intrinsic, which is handled by the second
+         theorem, eval_step_int. This lemma is used here. *)
+      auto.
+    + (* A quote doesn't have a next step, and so is final. *)
+      apply chain_final. auto.
+    + (* In composition, by induction, we know that the two sub-expressions produce
+         proper evaluation chains. Chains can be composed (via eval_chain_merge). *)
+      eapply eval_chain_merge; eauto.
+  - intros i vs vs' Hsem.
+    (* The evaluation chain depends on the specific intrinsic in use. *)
+    inversion Hsem; subst;
+    (* Most intrinsics produce a final value, and the evaluation chain is trivial. *)
+    try (apply chain_final; auto; fail).
+    (* Only apply is non-final. The first step is popping the quote from the stack,
+       and the rest of the steps are given by the evaluation of the code in the quote. *)
+    apply chain_middle with e vs0; auto.
+Qed.
+
+Ltac2 Type exn ::= [ | Not_intrinsic ].
+
+Ltac2 rec destruct_n (n : int) (vs : constr) : unit :=
+  if Int.le n 0 then () else
+    let v := Fresh.in_goal @v in
+    let vs' := Fresh.in_goal @vs in
+    destruct $vs as [|$v $vs']; Control.enter (fun () =>
+      try (destruct_n (Int.sub n 1) (Control.hyp vs'))
+    ).
+
+Ltac2 int_arity (int : constr) : int :=
+  match! int with
+  | swap => 2
+  | clone => 1
+  | drop => 1
+  | quote => 1
+  | compose => 2
+  | apply => 1
+  | _ => Control.throw Not_intrinsic
+  end.
+
+Ltac2 destruct_int_stack (int : constr) (va: constr) := destruct_n (int_arity int) va.
+
+Ltac2 ensure_valid_stack () := Control.enter (fun () =>
+  match! goal with
+  | [h : eval_step ?a (e_int ?b) = ?c |- _] =>
+      let h := Control.hyp h in
+      destruct_int_stack b a;
+      try (inversion $h; fail)
+  | [|- _ ] => ()
+  end).
+
+Theorem test : forall (vs vs': value_stack), eval_step vs (e_int swap) = final vs' ->
+  exists v1 v2 vs'', vs = v1 :: v2 :: vs'' /\ vs' = v2 :: v1 :: vs''.
+Proof.
+  intros s s' Heq.
+  ensure_valid_stack ().
+  simpl in Heq. injection Heq as Hinj. subst. eauto.
+Qed.
+
+Theorem eval_step_final_sem : forall (e : expr) (vs vs' : value_stack),
+  eval_step vs e = final vs' -> Sem_expr vs e vs'.
+Proof.
+  intros e vs vs' Hev. destruct e.
+  - destruct i; ensure_valid_stack ();
+    (* Get rid of trivial cases that match one-to-one. *)
+    simpl in Hev; try (injection Hev as Hinj; subst; solve_basic ()).
+    + (* compose with one quoted value is not final, but an error. *)
+      destruct v. inversion Hev.
+    + (* compose with two quoted values. *)
+      destruct v; destruct v0.
+      injection Hev as Hinj; subst; solve_basic ().
+    + (* Apply is not final. *) destruct v. inversion Hev.
+  - (* Quote is always final, trivially, and the semantics match easily. *)
+    simpl in Hev. injection Hev as Hinj; subst. solve_basic ().
+  - (* Compose is never final, so we don't need to handle it here. *)
+    simpl in Hev. destruct (eval_step vs e1); inversion Hev.
+Qed.
+
+Theorem eval_step_middle_sem : forall (e ei: expr) (vs vsi vs' : value_stack),
+  eval_step vs e = middle ei vsi ->
+  Sem_expr vsi ei vs' ->
+  Sem_expr vs e vs'.
+Proof.
+  intros e. induction e; intros ei vs vsi vs' Hev Hsem.
+  - destruct i; ensure_valid_stack ().
+    + (* compose with one quoted value; invalid. *)
+      destruct v. inversion Hev.
+    + (* compose with two quoted values; not a middle step. *)
+      destruct v; destruct v0. inversion Hev.
+    + (* Apply *)
+      destruct v. injection Hev as Hinj; subst.
+      solve_basic (). auto.
+  - (* quoting an expression is not middle. *)
+    inversion Hev.
+  - simpl in Hev.
+    destruct (eval_step vs e1) eqn:Hev1.
+    + (* Step led to an error, which can't happen in a chain. *)
+      inversion Hev.
+    + (* Left expression makes a non-final step. Milk this for equalities first. *)
+      injection Hev as Hinj; subst.
+      (* The rest of the program (e_comp e e2) evaluates using our semantics,
+         which means that both e and e2 evaluate using our semantics. *)
+      inversion Hsem; subst.
+      (* By induction, e1 evaluates using our semantics if e does, which we just confirmed. *)
+      specialize (IHe1 e vs vsi vs2 Hev1 H2).
+      (* The composition rule can now be applied. *)
+      eapply Sem_e_comp; eauto.
+    + (* Left expression makes a final step. Milk this for equalities first. *)
+      injection Hev as Hinj; subst.
+      (* Using eval_step_final, we know that e1 evaluates to the intermediate
+         state given our semantics. *)
+      specialize (eval_step_final_sem e1 vs vsi Hev1) as Hsem1.
+      (* The composition rule can now be applied. *)
+      eapply Sem_e_comp; eauto.
+Qed.
+
+Theorem eval_step_sem_back : forall (e : expr) (vs vs' : value_stack),
+  eval_chain vs e vs' -> Sem_expr vs e vs'.
+Proof.
+  intros e vs vs' ch.
+  ltac1:(dependent induction ch).
+  - apply eval_step_final_sem. auto.
+  - specialize (eval_step_middle_sem e ei vs vsi vs' P IHch). auto.
+Qed.
+
+Corollary eval_step_no_sem : forall (e : expr) (vs vs' : value_stack),
+  ~(Sem_expr vs e vs') -> ~(eval_chain vs e vs').
+Proof.
+  intros e vs vs' Hnsem Hch.
+  specialize (eval_step_sem_back _ _ _ Hch). auto.
+Qed.
+
+Require Extraction.
+Require Import ExtrHaskellBasic.
+Extraction Language Haskell.
+Set Extraction KeepSingleton.
+Extraction "UccGen.hs" expr eval_step true false or.
+
+Remark eval_swap_two_values : forall (vs vs' : value_stack),
+  eval_step vs (e_int swap) = final vs' -> exists v1 v2 vst, vs = v1 :: v2 :: vst /\ vs' = v2 :: v1 :: vst.
+Proof.
+  intros vs vs' Hev.
+  (* Can't proceed until we know more about the stack. *)
+  destruct vs as [|v1 [|v2 vs]].
+  - (* Invalid case; empty stack. *) inversion Hev.
+  - (* Invalid case; stack only has one value. *) inversion Hev.
+  - (* Valid case: the stack has two values. *) injection Hev. eauto.
+Qed.
+
+Remark eval_swap_two_values' : forall (vs vs' : value_stack),
+  eval_step vs (e_int swap) = final vs' -> exists v1 v2 vst, vs = v1 :: v2 :: vst /\ vs' = v2 :: v1 :: vst.
+Proof.
+  intros vs vs' Hev.
+  ensure_valid_stack ().
+  injection Hev. eauto.
+Qed.

code/dawn/DawnV2.v

@@ -0,0 +1,179 @@
+Require Import Coq.Lists.List.
+From Ltac2 Require Import Ltac2.
+
+Inductive intrinsic :=
+  | swap
+  | clone
+  | drop
+  | quote
+  | compose
+  | apply.
+
+Inductive expr :=
+  | e_int (i : intrinsic)
+  | e_quote (e : expr)
+  | e_comp (e1 e2 : expr).
+
+Definition e_compose (e : expr) (es : list expr) := fold_left e_comp es e.
+
+Inductive value := v_quote (e : expr).
+Definition value_stack := list value.
+
+Definition value_to_expr (v : value) : expr :=
+  match v with
+  | v_quote e => e_quote e
+  end.
+
+Inductive Sem_int : value_stack -> intrinsic -> value_stack -> Prop :=
+  | Sem_swap : forall (v v' : value) (vs : value_stack), Sem_int (v' :: v :: vs) swap (v :: v' :: vs)
+  | Sem_clone : forall (v : value) (vs : value_stack), Sem_int (v :: vs) clone (v :: v :: vs)
+  | Sem_drop : forall (v : value) (vs : value_stack), Sem_int (v :: vs) drop vs
+  | Sem_quote : forall (v : value) (vs : value_stack), Sem_int (v :: vs) quote ((v_quote (value_to_expr v)) :: vs)
+  | Sem_compose : forall (e e' : expr) (vs : value_stack), Sem_int (v_quote e' :: v_quote e :: vs) compose (v_quote (e_comp e e') :: vs)
+  | Sem_apply : forall (e : expr) (vs vs': value_stack), Sem_expr vs e vs' -> Sem_int (v_quote e :: vs) apply vs'
+
+with Sem_expr : value_stack -> expr -> value_stack -> Prop :=
+  | Sem_e_int : forall (i : intrinsic) (vs vs' : value_stack), Sem_int vs i vs' -> Sem_expr vs (e_int i) vs'
+  | Sem_e_quote : forall (e : expr) (vs : value_stack), Sem_expr vs (e_quote e) (v_quote e :: vs)
+  | Sem_e_comp : forall (e1 e2 : expr) (vs1 vs2 vs3 : value_stack),
+      Sem_expr vs1 e1 vs2 -> Sem_expr vs2 e2 vs3 -> Sem_expr vs1 (e_comp e1 e2) vs3.
+
+Definition false : expr := e_quote (e_int drop).
+Definition false_v : value := v_quote (e_int drop).
+
+Definition true : expr := e_quote (e_comp (e_int swap) (e_int drop)).
+Definition true_v : value := v_quote (e_comp (e_int swap) (e_int drop)).
+
+Theorem false_correct : forall (v v' : value) (vs : value_stack), Sem_expr (v' :: v :: vs) (e_comp false (e_int apply)) (v :: vs).
+Proof.
+  intros v v' vs.
+  eapply Sem_e_comp.
+  - apply Sem_e_quote.
+  - apply Sem_e_int. apply Sem_apply. apply Sem_e_int. apply Sem_drop.
+Qed.
+
+Theorem true_correct : forall (v v' : value) (vs : value_stack), Sem_expr (v' :: v :: vs) (e_comp true (e_int apply)) (v' :: vs).
+Proof.
+  intros v v' vs.
+  eapply Sem_e_comp.
+  - apply Sem_e_quote.
+  - apply Sem_e_int. apply Sem_apply. eapply Sem_e_comp.
+    * apply Sem_e_int. apply Sem_swap.
+    * apply Sem_e_int. apply Sem_drop.
+Qed.
+
+Definition or : expr := e_comp (e_int clone) (e_int apply).
+
+Theorem or_false_v : forall (v : value) (vs : value_stack), Sem_expr (false_v :: v :: vs) or (v :: vs).
+Proof with apply Sem_e_int.
+  intros v vs.
+  eapply Sem_e_comp...
+  - apply Sem_clone.
+  - apply Sem_apply... apply Sem_drop.
+Qed.
+
+Theorem or_true : forall (v : value) (vs : value_stack), Sem_expr (true_v :: v :: vs) or (true_v :: vs).
+Proof with apply Sem_e_int.
+  intros v vs.
+  eapply Sem_e_comp...
+  - apply Sem_clone...
+  - apply Sem_apply. eapply Sem_e_comp...
+    * apply Sem_swap.
+    * apply Sem_drop.
+Qed.
+
+Definition or_false_false := or_false_v false_v.
+Definition or_false_true := or_false_v true_v.
+Definition or_true_false := or_true false_v.
+Definition or_true_true := or_true true_v.
+
+Fixpoint quote_n (n : nat) :=
+  match n with
+  | O => e_int quote
+  | S n' => e_compose (quote_n n') (e_int swap :: e_int quote :: e_int swap :: e_int compose :: nil)
+  end.
+
+Theorem quote_2_correct : forall (v1 v2 : value) (vs : value_stack),
+    Sem_expr (v2 :: v1 :: vs) (quote_n 1) (v_quote (e_comp (value_to_expr v1) (value_to_expr v2)) :: vs).
+Proof with apply Sem_e_int.
+  intros v1 v2 vs. simpl.
+  repeat (eapply Sem_e_comp)...
+  - apply Sem_quote.
+  - apply Sem_swap.
+  - apply Sem_quote.
+  - apply Sem_swap.
+  - apply Sem_compose.
+Qed.
+
+Theorem quote_3_correct : forall (v1 v2 v3 : value) (vs : value_stack),
+  Sem_expr (v3 :: v2 :: v1 :: vs) (quote_n 2) (v_quote (e_comp (value_to_expr v1) (e_comp (value_to_expr v2) (value_to_expr v3))) :: vs).
+Proof with apply Sem_e_int.
+  intros v1 v2 v3 vs. simpl.
+  repeat (eapply Sem_e_comp)...
+  - apply Sem_quote.
+  - apply Sem_swap.
+  - apply Sem_quote.
+  - apply Sem_swap.
+  - apply Sem_compose.
+  - apply Sem_swap.
+  - apply Sem_quote.
+  - apply Sem_swap.
+  - apply Sem_compose.
+Qed.
+
+Ltac2 rec solve_basic () := Control.enter (fun _ =>
+  match! goal with
+  | [|- Sem_int ?vs1 swap ?vs2] => apply Sem_swap
+  | [|- Sem_int ?vs1 clone ?vs2] => apply Sem_clone
+  | [|- Sem_int ?vs1 drop ?vs2] => apply Sem_drop
+  | [|- Sem_int ?vs1 quote ?vs2] => apply Sem_quote
+  | [|- Sem_int ?vs1 compose ?vs2] => apply Sem_compose
+  | [|- Sem_int ?vs1 apply ?vs2] => apply Sem_apply
+  | [|- Sem_expr ?vs1 (e_comp ?e1 ?e2) ?vs2] => eapply Sem_e_comp; solve_basic ()
+  | [|- Sem_expr ?vs1 (e_int ?e) ?vs2] => apply Sem_e_int; solve_basic ()
+  | [|- Sem_expr ?vs1 (e_quote ?e) ?vs2] => apply Sem_e_quote
+  | [_ : _ |- _] => ()
+  end).
+
+Theorem quote_2_correct' : forall (v1 v2 : value) (vs : value_stack),
+    Sem_expr (v2 :: v1 :: vs) (quote_n 1) (v_quote (e_comp (value_to_expr v1) (value_to_expr v2)) :: vs).
+Proof. intros. simpl. solve_basic (). Qed.
+
+Theorem quote_3_correct' : forall (v1 v2 v3 : value) (vs : value_stack),
+  Sem_expr (v3 :: v2 :: v1 :: vs) (quote_n 2) (v_quote (e_comp (value_to_expr v1) (e_comp (value_to_expr v2) (value_to_expr v3))) :: vs).
+Proof. intros. simpl. solve_basic (). Qed.
+
+Definition rotate_n (n : nat) := e_compose (quote_n n) (e_int swap :: e_int quote :: e_int compose :: e_int apply :: nil).
+
+Lemma eval_value : forall (v : value) (vs : value_stack),
+  Sem_expr vs (value_to_expr v) (v :: vs).
+Proof.
+  intros v vs.
+  destruct v. 
+  simpl. apply Sem_e_quote.
+Qed.
+
+Theorem rotate_3_correct : forall (v1 v2 v3 : value) (vs : value_stack),
+  Sem_expr (v3 :: v2 :: v1 :: vs) (rotate_n 1) (v1 :: v3 :: v2 :: vs).
+Proof.
+  intros. unfold rotate_n. simpl. solve_basic ().
+  repeat (eapply Sem_e_comp); apply eval_value.
+Qed.
+
+Theorem rotate_4_correct : forall (v1 v2 v3 v4 : value) (vs : value_stack),
+  Sem_expr (v4 :: v3 :: v2 :: v1 :: vs) (rotate_n 2) (v1 :: v4 :: v3 :: v2 :: vs).
+Proof.
+  intros. unfold rotate_n. simpl. solve_basic ().
+  repeat (eapply Sem_e_comp); apply eval_value.
+Qed.
+
+Theorem e_comp_assoc : forall (e1 e2 e3 : expr) (vs vs' : value_stack),
+  Sem_expr vs (e_comp e1 (e_comp e2 e3)) vs' <-> Sem_expr vs (e_comp (e_comp e1 e2) e3) vs'.
+Proof.
+  intros e1 e2 e3 vs vs'.
+  split; intros Heval.
+  - inversion Heval; subst. inversion H4; subst.
+    eapply Sem_e_comp. eapply Sem_e_comp. apply H2. apply H3. apply H6.
+  - inversion Heval; subst. inversion H2; subst.
+    eapply Sem_e_comp. apply H3. eapply Sem_e_comp. apply H6. apply H4.
+Qed.

code/dawn/Ucc.hs

@@ -0,0 +1,64 @@
+module Ucc where
+import UccGen
+import Text.Parsec
+import Data.Functor.Identity
+import Control.Applicative hiding ((<|>))
+import System.IO
+
+instance Show Intrinsic where
+    show Swap = "swap"
+    show Clone = "clone"
+    show Drop = "drop"
+    show Quote = "quote"
+    show Compose = "compose"
+    show Apply = "apply"
+
+instance Show Expr where
+    show (E_int i) = show i
+    show (E_quote e) = "[" ++ show e ++ "]"
+    show (E_comp e1 e2) = show e1 ++ " " ++ show e2
+
+instance Show Value where
+    show (V_quote e) = show (E_quote e)
+
+type Parser a = ParsecT String () Identity a
+
+intrinsic :: Parser Intrinsic
+intrinsic = (<* spaces) $ foldl1 (<|>) $ map (\(s, i) -> try (string s >> return i))
+    [ ("swap", Swap)
+    , ("clone", Clone)
+    , ("drop", Drop)
+    , ("quote", Quote)
+    , ("compose", Compose)
+    , ("apply", Apply)
+    ]
+
+expression :: Parser Expr
+expression = foldl1 E_comp <$> many1 single
+    where
+        single
+            = (E_int <$> intrinsic)
+            <|> (fmap E_quote $ char '[' *> spaces *> expression <* char ']' <* spaces)
+
+parseExpression :: String -> Either ParseError Expr
+parseExpression = runParser expression () "<inline>"
+
+eval :: [Value] -> Expr -> Maybe [Value]
+eval s e =
+    case eval_step s e of
+        Err -> Nothing
+        Final s' -> Just s'
+        Middle e' s' -> eval s' e'
+
+main :: IO ()
+main = do
+    putStr "> "
+    hFlush stdout
+    str <- getLine
+    case parseExpression str of
+        Right e ->
+            case eval [] e of
+                Just st -> putStrLn $ show st
+                _ -> putStrLn "Evaluation error"
+        _ -> putStrLn "Parse error"
+    main

code/patterns/patterns.rb

@@ -0,0 +1,68 @@
+require 'victor'
+
+def sum_digits(n)
+  while n > 9
+    n = n.to_s.chars.map(&:to_i).sum
+  end
+  n
+end
+
+def step(x, y, n, dir)
+  case dir
+  when :top
+    return [x,y+n,:right]
+  when :right
+    return [x+n,y,:bottom]
+  when :bottom
+    return [x,y-n,:left]
+  when :left
+    return [x-n,y,:top]
+  end
+end
+
+def run_number(number)
+  counter = 1
+  x, y, dir = 0, 0, :top
+  line_stack = [[0,0]]
+
+  loop do
+    x, y, dir = step(x,y, sum_digits(counter*number), dir)
+    line_stack << [x,y]
+    counter += 1
+    break if x == 0 && y == 0
+  end
+  return make_svg(line_stack)
+end
+
+def make_svg(line_stack)
+  line_length = 20
+  xs = line_stack.map { |c| c[0] }
+  ys = line_stack.map { |c| c[1] }
+  
+  x_offset = -xs.min
+  y_offset = -ys.min
+  svg_coords = ->(p) {
+    nx, ny = p
+    [(nx+x_offset)*line_length + line_length/2, (ny+y_offset)*line_length + line_length/2]
+  }
+  
+  max_width = (xs.max - xs.min).abs * line_length + line_length
+  max_height = (ys.max - ys.min).abs * line_length + line_length
+  svg = Victor::SVG.new width: max_width, height: max_height
+  
+  style = { stroke: 'black', stroke_width: 5 }
+  svg.build do
+    line_stack.each_cons(2) do |pair|
+      p1, p2 = pair
+      x1, y1 = svg_coords.call(p1)
+      x2, y2 = svg_coords.call(p2)
+      line x1: x1, y1: y1, x2: x2, y2: y2, style: style
+      circle cx: x2, cy: y2, r: line_length/6, style: style, fill: 'black'
+    end
+  end
+  return svg
+end
+
+(1..9).each do |i|
+  run_number(i).save "pattern_#{i}"
+end

code/typesafe-imperative/TypesafeImp.idr

@@ -0,0 +1,102 @@
+data Reg = A | B | R
+
+data Ty = IntTy | BoolTy
+
+TypeState : Type
+TypeState = (Ty, Ty, Ty)
+
+getRegTy : Reg -> TypeState -> Ty
+getRegTy A (a, _, _) = a
+getRegTy B (_, b, _) = b
+getRegTy R (_, _, r) = r
+
+setRegTy : Reg -> Ty -> TypeState -> TypeState
+setRegTy A a (_, b, r) = (a, b, r)
+setRegTy B b (a, _, r) = (a, b, r)
+setRegTy R r (a, b, _) = (a, b, r)
+
+data Expr : TypeState -> Ty -> Type where
+  Lit : Int -> Expr s IntTy
+  Load : (r : Reg) -> Expr s (getRegTy r s)
+  Add : Expr s IntTy -> Expr s IntTy -> Expr s IntTy
+  Leq : Expr s IntTy -> Expr s IntTy -> Expr s BoolTy
+  Not : Expr s BoolTy -> Expr s BoolTy
+
+mutual
+  data Stmt : TypeState -> TypeState -> TypeState -> Type where
+    Store : (r : Reg) -> Expr s t -> Stmt l s (setRegTy r t s)
+    If : Expr s BoolTy -> Prog l s n -> Prog l s n -> Stmt l s n
+    Loop : Prog s s s -> Stmt l s s
+    Break : Stmt s s s
+
+  data Prog : TypeState -> TypeState -> TypeState -> Type where
+    Nil : Prog l s s
+    (::) : Stmt l s n -> Prog l n m -> Prog l s m
+
+initialState : TypeState
+initialState = (IntTy, IntTy, IntTy)
+
+testProg : Prog Main.initialState Main.initialState Main.initialState
+testProg =
+  [ Store A (Lit 1 `Leq` Lit 2)
+  , If (Load A)
+    [ Store A (Lit 1) ]
+    [ Store A (Lit 2) ]
+  , Store B (Lit 2)
+  , Store R (Add (Load A) (Load B))
+  ]
+
+prodProg : Prog Main.initialState Main.initialState Main.initialState
+prodProg =
+  [ Store A (Lit 7)
+  , Store B (Lit 9)
+  , Store R (Lit 0)
+  , Loop
+    [ If (Load A `Leq` Lit 0)
+      [ Break ]
+      [ Store R (Load R `Add` Load B)
+      , Store A (Load A `Add` Lit (-1))
+      ]
+    ]
+  ]
+
+repr : Ty -> Type
+repr IntTy = Int
+repr BoolTy = Bool
+
+data State : TypeState -> Type where
+  MkState : (repr a, repr b, repr c) -> State (a, b, c)
+
+getReg : (r : Reg) -> State s -> repr (getRegTy r s)
+getReg A (MkState (a, _, _)) = a
+getReg B (MkState (_, b, _)) = b
+getReg R (MkState (_, _, r)) = r
+
+setReg : (r : Reg) -> repr t -> State s -> State (setRegTy r t s)
+setReg A a (MkState (_, b, r)) = MkState (a, b, r)
+setReg B b (MkState (a, _, r)) = MkState (a, b, r)
+setReg R r (MkState (a, b, _)) = MkState (a, b, r)
+
+expr : Expr s t -> State s -> repr t
+expr (Lit i) _ = i
+expr (Load r) s = getReg r s
+expr (Add l r) s = expr l s + expr r s
+expr (Leq l r) s = expr l s <= expr r s
+expr (Not e) s = not $ expr e s
+
+mutual
+  stmt : Stmt l s n -> State s -> Either (State l) (State n)
+  stmt (Store r e) s = Right $ setReg r (expr e s) s
+  stmt (If c t e) s = if expr c s then prog t s else prog e s
+  stmt (Loop p) s =
+    case prog p s >>= stmt (Loop p) of
+      Right s => Right s
+      Left s => Right s
+  stmt Break s = Left s
+
+  prog : Prog l s n -> State s -> Either (State l) (State n)
+  prog Nil s = Right s
+  prog (st::p) s = stmt st s >>= prog p
+
+run : Prog l s l -> State s -> State l
+run p s = either id id $ prog p s

code/typescript-emitter/js1.js

@@ -0,0 +1,23 @@
+class EventEmitter {
+    constructor() {
+        this.handlers = {}
+    }
+
+    emit(event) {
+        this.handlers[event]?.forEach(h => h());
+    }
+
+    addHandler(event, handler) {
+        if(!this.handlers[event]) {
+            this.handlers[event] = [handler];
+        } else {
+            this.handlers[event].push(handler);
+        }
+    }
+}
+
+const emitter = new EventEmitter();
+emitter.addHandler("start", () => console.log("Started!"));
+emitter.addHandler("end", () => console.log("Ended!"));
+emitter.emit("end");
+emitter.emit("start");

code/typescript-emitter/js2.js

@@ -0,0 +1,23 @@
+class EventEmitter {
+    constructor() {
+        this.handlers = {}
+    }
+
+    emit(event, value) {
+        this.handlers[event]?.forEach(h => h(value));
+    }
+
+    addHandler(event, handler) {
+        if(!this.handlers[event]) {
+            this.handlers[event] = [handler];
+        } else {
+            this.handlers[event].push(handler);
+        }
+    }
+}
+
+const emitter = new EventEmitter();
+emitter.addHandler("numberChange", n => console.log("New number value is: ", n));
+emitter.addHandler("stringChange", s => console.log("New string value is: ", s));
+emitter.emit("numberChange", 1);
+emitter.emit("stringChange", "3");

code/typescript-emitter/ts.ts

@@ -0,0 +1,27 @@
+class EventEmitter<T> {
+    private handlers: { [eventName in keyof T]?: ((value: T[eventName]) => void)[] }
+
+    constructor() {
+        this.handlers = {}
+    }
+
+    emit<K extends keyof T>(event: K, value: T[K]): void {
+        this.handlers[event]?.forEach(h => h(value));
+    }
+
+    addHandler<K extends keyof T>(event: K, handler: (value: T[K]) => void): void {
+        if(!this.handlers[event]) {
+            this.handlers[event] = [handler];
+        } else {
+            this.handlers[event].push(handler);
+        }
+    }
+}
+
+const emitter = new EventEmitter<{ numberChange: number, stringChange: string }>();
+emitter.addHandler("numberChange", n => console.log("New number value is: ", n));
+emitter.addHandler("stringChange", s => console.log("New string value is: ", s));
+emitter.emit("numberChange", 1);
+emitter.emit("stringChange", "3");
+emitter.emit("numberChange", "1");
+emitter.emit("stringChange", 3);

config-gen.toml

@@ -0,0 +1,8 @@
+[params]
+  [params.submoduleLinks]
+    [params.submoduleLinks.aoc2020]
+      url = "https://dev.danilafe.com/Advent-of-Code/AdventOfCode-2020/src/commit/7a8503c3fe1aa7e624e4d8672aa9b56d24b4ba82"
+      path = "aoc-2020"
+    [params.submoduleLinks.serverconfig]
+      url = "https://dev.danilafe.com/Nix-Configs/server-config/src/commit/98cffe09546aee1678f7baebdea5eb5fef288935"
+      path = "server-config"

config.toml

@@ -1,18 +1,22 @@
-languageCode = "en"
+baseURL = "https://danilafe.com"
+languageCode = "en-us"
 title = "Daniel's Blog"
 theme = "vanilla"
 pygmentsCodeFences = true
 pygmentsUseClasses = true
 summaryLength = 20
 
+[outputFormats]
+  [outputFormats.Toml]
+    name = "toml"
+    mediaType = "application/toml"
+    isHTML = false
+
+[outputs]
+  home = ["html","rss","toml"]
+
 [markup]
   [markup.tableOfContents]
     endLevel = 4
     ordered = false
     startLevel = 3
-
-[languages]
-  [languages.en]
-    baseURL = "https://danilafe.com"
-  [languages.ru]
-    baseURL = "https://ru.danilafe.com"

content/_index.ru.md

@@ -1,8 +0,0 @@
----
-title: Daniel's Blog
-description: Персональный блог Данилы Федорина о функциональном программировании, дизайне компиляторов, и многом другом! 
----
-## Привет!
-Добро пожаловать на мой сайт. Здесь, я пишу на многие темы, включая фунциональное программирование, дизайн компилляторов, теорию языков программирования, и иногда компьютерные игры. Я надеюсь, что здесь вы найдете что-нибуть интересное!
-
-Вы читаете русскою версию моего сайта. Я только недавно занялся его переводом, и до этого времени редко писал на русском. Я заранеее извиняюсь за присутствие орфографических или грамматических ошибок.

content/about.md

@@ -1,6 +1,8 @@
 ---
 title: About
 ---
+{{< donate_css >}}
+
 I'm Daniel, a Computer Science student currently working towards my Master's Degree at Oregon State University.
 Due to my initial interest in calculators and compilers, I got involved in the Programming Language Theory research
 group, gaining same experience in formal verification, domain specific language, and explainable computing.
@@ -8,3 +10,34 @@ group, gaining same experience in formal verification, domain specific language,
 For work, school, and hobby projects, I use a variety of programming languages, most commonly C/C++,
 Haskell, [Crystal](https://crystal-lang.org/), and [Elm](https://elm-lang.org/). I also have experience
 with Java, Python, Haxe, and JavaScript.
+
+A few notes about me or this site:
+* __Correctness__: I mostly write technical content. Even though I proofread my articles, there's
+always a fairly good chance that I'm wrong. You should always use your best judgement when reading
+anything on this site -- if something seems wrong, it may very well be. I'm far from an expert.
+* __Schedule__: I do not have a set post schedule. There are many reasons for this:
+schoolwork, personal life, lack of inspiration. It also takes a _very_ long time for
+me to write a single article. My article on [polymorphic type checking]({{< relref "/blog/10_compiler_polymorphism.md" >}})
+is around 8,000 words long; besides writing it, I have to edit it, link up all the code
+references, and proofread the final result. And of course, I need to write the code and
+occasionally do some research.
+* __Design__: I am doing my best to keep this website accessible and easy on the eyes.
+I'm also doing my best to avoid any and all uses of JavaScript. I used to use a lot of
+uMatrix, and most of the websites I browsed during this time were broken. Similarly,
+a lot of websites were unusable on my weaker machines. So, I'm doing my part and
+making this site usable without any JavaScript, and, as it seems to me, even
+without any CSS.
+* __Source code__: This blog is open source, but not on GitHub. Instead,
+you can find the code on my [Gitea instance](https://dev.danilafe.com/Web-Projects/blog-static).
+If you use this code for your own site, I would prefer that you don't copy the theme.
+
+### Donate
+I don't run ads, nor do I profit from writing anything on here. I have no trouble paying for hosting,
+and I write my articles voluntarily, for my own enjoyment. However, if you found something particularly
+helpful on here, and would like to buy me a cup of coffee or help host the site, you can donate using
+the method(s) below.
+
+{{< donation_methods >}}
+{{< donation_method "Bitcoin" "1BbXPZhdzv4xHq5LYhme3xBiUsHw5fmafd" >}}
+{{< donation_method "Ethereum" "0xd111E49344bEC80570e68EE0A00b87B1EFcb5D56" >}}
+{{< /donation_methods >}}

content/blog/00_aoc_coq.md

@@ -0,0 +1,351 @@
+---
+title: "Advent of Code in Coq - Day 1"
+date: 2020-12-02T18:44:56-08:00
+tags: ["Advent of Code", "Coq"]
+favorite: true
+---
+
+The first puzzle of this year's [Advent of Code](https://adventofcode.com) was quite
+simple, which gave me a thought: "Hey, this feels within reach for me to formally verify!"
+At first, I wanted to formalize and prove the correctness of the [two-pointer solution](https://www.geeksforgeeks.org/two-pointers-technique/).
+However, I didn't have the time to mess around with the various properties of sorted
+lists and their traversals. So, I settled for the brute force solution. Despite
+the simplicity of its implementation, there is plenty to talk about when proving
+its correctness using Coq. Let's get right into it!
+
+Before we start, in the interest of keeping the post self-contained, here's the (paraphrased)
+problem statement:
+
+> Given an unsorted list of numbers, find two distinct numbers that add up to 2020.
+
+With this in mind, we can move on to writing some Coq!
+
+### Defining the Functions
+The first step to proving our code correct is to actually write the code! To start with,
+let's write a helper function that, given a number `x`, tries to find another number
+`y` such that `x + y = 2020`. In fact, rather than hardcoding the desired
+sum to `2020`, let's just use another argument called `total`. The code is quite simple:
+
+{{< codelines "Coq" "aoc-2020/day1.v" 11 18 >}}
+
+Here, `is` is the list of numbers that we want to search.
+We proceed by case analysis: if the list is empty, we can't
+find a match, so we return `None` (the Coq equivalent of Haskell's `Nothing`).
+On the other hand, if the list has at least one element `y`, we see if it adds
+up to `total`, and return `Some y` (equivalent to `Just y` in Haskell) if it does.
+If it doesn't, we continue our search into the rest of the list.
+
+It's somewhat unusual, in my experience, to put the list argument first when writing
+functions in a language with [currying](https://wiki.haskell.org/Currying). However,
+it seems as though Coq's `simpl` tactic, which we will use later, works better
+for our purposes when the argument being case analyzed is given first.
+
+We can now use `find_matching` to define our `find_sum` function, which solves part 1.
+Here's the code:
+
+{{< codelines "Coq" "aoc-2020/day1.v" 20 28 >}}
+
+For every `x` that we encounter in our input list `is`, we want to check if there's
+a matching number in the rest of the list. We only search the remainder of the list
+because we can't use `x` twice: the `x` and `y` we return that add up to `total`
+must be different elements. We use `find_matching` to try find a complementary number
+for `x`. If we don't find it, this `x` isn't it, so we recursively move on to `xs`.
+On the other hand, if we _do_ find a matching `y`, we're done! We return `(x,y)`,
+wrapped in `Some` to indicate that we found something useful.
+
+What about that `(* Was buggy! *)` line? Well, it so happens that my initial
+implementation had a bug on this line, one that came up as I was proving
+the correctness of my function. When I wasn't able to prove a particular
+behavior in one of the cases, I realized something was wrong. In short,
+my proof actually helped me find and fix a bug!
+
+This is all the code we'll need to get our solution. Next, let's talk about some
+properties of our two functions.
+
+### Our First Lemma
+When we call `find_matching`, we want to be sure that if we get a number, 
+it does indeed add up to our expected total. We can state it a little bit more
+formally as follows:
+
+> For any numbers `k` and `x`, and for any list of number `is`,
+> if `find_matching is k x` returns a number `y`, then `x + y = k`.
+
+And this is how we write it in Coq:
+
+{{< codelines "Coq" "aoc-2020/day1.v" 30 31 >}}
+
+The arrow, `->`, reads "implies". Other than that, I think this
+property reads pretty well. The proof, unfortunately, is a little bit more involved.
+Here are the first few lines:
+
+{{< codelines "Coq" "aoc-2020/day1.v" 32 35 >}}
+
+We start with the `intros is` tactic, which is akin to saying
+"consider a particular list of integers `is`". We do this without losing
+generality: by simply examining a concrete list, we've said nothing about
+what that list is like. We then proceed by induction on `is`.
+
+To prove something by induction for a list, we need to prove two things:
+
+* The __base case__. Whatever property we want to hold, it must
+hold for the empty list, which is the simplest possible list.
+In our case, this means `find_matching` searching an empty list.
+* The __inductive case__. Assuming that a property holds for any list
+`[b, c, ...]`, we want to show that the property also holds for 
+the list `[a, b, c, ...]`. That is, the property must remain true if we
+prepend an element to a list for which this property holds.
+
+These two things combined give us a proof for _all_ lists, which is exactly
+what we want! If you don't belive me, here's how it works. Suppose you want
+to prove that some property `P` holds for `[1,2,3,4]`. Given the base
+case, we know that `P []` holds. Next, by the inductive case, since
+`P []` holds, we can prepend `4` to the list, and the property will
+still hold. Thus, `P [4]`. Now that `P [4]` holds, we can again prepend
+an element to the list, this time a `3`, and conclude that `P [3,4]`.
+Repeating this twice more, we arrive at our desired fact: `P [1,2,3,4]`.
+
+When we write `induction is`, Coq will generate two proof goals for us,
+one for the base case, and one for the inductive case. We will have to prove
+each of them separately. Since we have
+not yet introduced the variables `k`, `x`, and `y`, they remain
+inside a `forall` quantifier at that time. To be able to refer
+to them, we want to use `intros`. We want to do this in both the
+base and the inductive case. To quickly do this, we use Coq's `;`
+operator. When we write `a; b`, Coq runs the tactic `a`, and then
+runs the tactic `b` in every proof goal generated by `a`. This is
+exactly what we want.
+
+There's one more variable inside our second `intros`: `Hev`.
+This variable refers to the hypothesis of our statement:
+that is, the part on the left of the `->`. To prove that `A`
+implies `B`, we assume that `A` holds, and try to argue `B` from there.
+Here is no different: when we use `intros Hev`, we say, "suppose that you have
+a proof that `find_matching` evaluates to `Some y`, called `Hev`". The thing
+on the right of `->` becomes our proof goal.
+
+Now, it's time to look at the cases. To focus on one case at a time,
+we use `-`. The first case is our base case. Here's what Coq prints
+out at this time:
+
+```
+k, x, y : nat
+Hev : find_matching nil k x = Some y
+
+========================= (1 / 1)
+
+x + y = k
+```
+
+All the stuff above the `===` line are our hypotheses. We know
+that we have some `k`, `x`, and `y`, all of which are numbers.
+We also have the assumption that `find_matching` returns `Some y`.
+In the base case, `is` is just `[]`, and this is reflected in the
+type for `Hev`. To make this more clear, we'll simplify the call to `find_matching`
+in `Hev`, using `simpl in Hev`. Now, here's what Coq has to say about `Hev`:
+
+```
+Hev : None = Some y
+```
+
+Well, this doesn't make any sense. How can something be equal to nothing?
+We ask Coq this question using `inversion Hev`. Effectively, the question
+that `inversion` asks is: what are the possible ways we could have acquired `Hev`?
+Coq generates a proof goal for each of these possible ways. Alas, there are
+no ways to arrive at this contradictory assumption: the number of proof sub-goals
+is zero. This means we're done with the base case!
+
+The inductive case is the meat of this proof. Here's the corresponding part
+of the Coq source file:
+
+{{< codelines "Coq" "aoc-2020/day1.v" 36 40 >}}
+
+This time, the proof state is more complicated:
+
+```
+a : nat
+is : list nat
+IHis : forall k x y : nat, find_matching is k x = Some y -> x + y = k
+k, x, y : nat
+Hev : find_matching (a :: is) k x = Some y
+
+========================= (1 / 1)
+
+x + y = k
+```
+
+Following the footsteps of our informal description of the inductive case,
+Coq has us prove our property for `(a :: is)`, or the list `is` to which
+`a` is being prepended. Like before, we assume that our property holds for `is`.
+This is represented in the __induction hypothesis__ `IHis`. It states that if
+`find_matching` finds a `y` in `is`, it must add up to `k`. However, `IHis`
+doesn't tell us anything about `a :: is`: that's our job. We also still have
+`Hev`, which is our assumption that `find_matching` finds a `y` in `(a :: is)`.
+Running `simpl in Hev` gives us the following:
+
+```
+Hev : (if x + a =? k then Some a else find_matching is k x) = Some y
+```
+
+The result of `find_matching` now depends on whether or not the new element `a`
+adds up to `k`. If it does, then `find_matching` will return `a`, which means
+that `y` is the same as `a`. If not, it must be that `find_matching` finds
+the `y` in the rest of the list, `is`. We're not sure which of the possibilities
+is the case. Fortunately, we don't need to be!
+If we can prove that the `y` that `find_matching` finds is correct regardless
+of whether `a` adds up to `k` or not, we're good to go! To do this,
+we perform case analysis using `destruct`.
+
+Our particular use of `destruct` says: check any possible value for `x + a ?= k`,
+and create an equation `Heq` that tells us what that value is. `?=` returns a boolean
+value, and so `destruct` generates two new goals: one where the function returns `true`,
+and one where it returns `false`. We start with the former. Here's the proof state:
+
+```
+a : nat
+is : list nat
+IHis : forall k x y : nat, find_matching is k x = Some y -> x + y = k
+k, x, y : nat
+Heq : (x + a =? k) = true
+Hev : Some a = Some y
+
+========================= (1 / 1)
+
+x + y = k
+```
+
+There is a new hypothesis: `Heq`. It tells us that we're currently
+considering the case where `?=` evaluates to `true`. Also,
+`Hev` has been considerably simplified: now that we know the condition
+of the `if` expression, we can just replace it with the `then` branch.
+
+Looking at `Hev`, we can see that our prediction was right: `a` is equal to `y`. After all,
+if they weren't, `Some a` wouldn't equal to `Some y`. To make Coq
+take this information into account, we use `injection`. This will create
+a new hypothesis, `a = y`. But if one is equal to the other, why don't we
+just use only one of these variables everywhere? We do exactly that by using
+`subst`, which replaces `a` with `y` everywhere in our proof.
+
+The proof state is now:
+
+```
+is : list nat
+IHis : forall k x y : nat, find_matching is k x = Some y -> x + y = k
+k, x, y : nat
+Heq : (x + y =? k) = true
+
+========================= (1 / 1)
+
+x + y = k
+```
+
+We're close, but there's one more detail to keep in mind. Our goal, `x + y = k`,
+is the __proposition__ that `x + y` is equal to `k`. However, `Heq` tells us
+that the __function__ `?=` evaluates to `true`. These are fundamentally different.
+One talks about mathematical equality, while the other about some function `?=`
+defined somewhere in Coq's standard library. Who knows - maybe there's a bug in
+Coq's implementation! Fortunately, Coq comes with a proof that if two numbers
+are equal according to `?=`, they are mathematically equal. This proof is
+called `eqb_nat_eq`. We tell Coq to use this with `apply`. Our proof goal changes to:
+
+```
+true = (x + y =? k)
+```
+
+This is _almost_ like `Heq`, but flipped. Instead of manually flipping it and using `apply`
+with `Heq`, I let Coq do the rest of the work using `auto`.
+
+Phew! All this for the `true` case of `?=`. Next, what happens if `x + a` does not equal `k`?
+Here's the proof state at this time:
+
+```
+a : nat
+is : list nat
+IHis : forall k x y : nat, find_matching is k x = Some y -> x + y = k
+k, x, y : nat
+Heq : (x + a =? k) = false
+Hev : find_matching is k x = Some y
+
+========================= (1 / 1)
+
+x + y = k
+```
+
+Since `a` was not what it was looking for, `find_matching` moved on to `is`. But hey,
+we're in the inductive case! We are assuming that `find_matching` will work properly
+with the list `is`. Since `find_matching` found its `y` in `is`, this should be all we need!
+We use our induction hypothesis `IHis` with `apply`. `IHis` itself does not know that
+`find_matching` moved on to `is`, so it asks us to prove it. Fortunately, `Hev` tells us
+exactly that, so we use `assumption`, and the proof is complete! Quod erat demonstrandum, QED!
+
+### The Rest of the Owl
+Here are a couple of other properties of `find_matching`. For brevity's sake, I will
+not go through their proofs step-by-step. I find that the best way to understand
+Coq proofs is to actually step through them in the IDE!
+
+First on the list is `find_matching_skip`. Here's the type:
+
+{{< codelines "Coq" "aoc-2020/day1.v" 42 43 >}}
+
+It reads: if we correctly find a number in a small list `is`, we can find that same number
+even if another number is prepended to `is`. That makes sense: _adding_ a number to
+a list doesn't remove whatever we found in it! I used this lemma to prove another,
+`find_matching_works`:
+
+{{< codelines "Coq" "aoc-2020/day1.v" 53 54 >}}
+
+This reads, if there _is_ an element `y` in `is` that adds up to `k` with `x`, then
+`find_matching` will find it. This is an important property. After all, if it didn't
+hold, it would mean that `find_matching` would occasionally fail to find a matching
+number, even though it's there! We can't have that.
+
+Finally, we want to specify what it means for `find_sum`, our solution function, to actually
+work. The naive definition would be:
+
+> Given a list of integers, `find_sum` always finds a pair of numbers that add up to `k`.
+
+Unfortunately, this is not true. What if, for instance, we give `find_sum` an empty list?
+There are no numbers from that list to find and add together. Even a non-empty list
+may not include such a pair! We need a way to characterize valid input lists. I claim
+that all lists from this Advent of Code puzzle are guaranteed to have two numbers that
+add up to our goal, and that these numbers are not equal to each other. In Coq,
+we state this as follows:
+
+{{< codelines "Coq" "aoc-2020/day1.v" 8 9 >}}
+
+This defines a new property, `has_pair t is` (read "`is` has a pair of numbers that add to `t`"),
+which means:
+
+> There are two numbers `n1` and `n2` such that, they are not equal to each other (`n1<>n2`) __and__
+> the number `n1` is an element of `is` (`In n1 is`) __and__
+> the number `n2` is an element of `is` (`In n2 is`) __and__
+> the two numbers add up to `t` (`n1 + n2 = t`).
+
+When making claims about the correctness of our algorithm, we will assume that this
+property holds. Finally, here's the theorem we want to prove:
+
+{{< codelines "Coq" "aoc-2020/day1.v" 68 70 >}}
+
+It reads, "for any total `k` and list `is`, if `is` has a pair of numbers that add to `k`,
+then `find_sum` will return a pair of numbers `x` and `y` that add to `k`".
+There's some nuance here. We hardly reference the `has_pair` property in this definition,
+and for good reason. Our `has_pair` hypothesis only says that there is _at least one_
+pair of numbers in `is` that meets our criteria. However, this pair need not be the only
+one, nor does it need to be the one returned by `find_sum`! However, if we have many pairs,
+we want to confirm that `find_sum` will find one of them. Finally, here is the proof.
+I will not be able to go through it in detail in this post, but I did comment it to
+make it easier to read:
+
+{{< codelines "Coq" "aoc-2020/day1.v" 71 106 >}}
+
+Coq seems happy with it, and so am I! The bug I mentioned earlier popped up on line 96.
+I had accidentally made `find_sum` return `None` if it couldn't find a complement
+for the `x` it encountered. This meant that it never recursed into the remaining
+list `xs`, and thus, the pair was never found at all! It this became impossible
+to prove that `find_some` will return `Some y`, and I had to double back
+and check my definitions.
+
+I hope you enjoyed this post! If you're interested to learn more about Coq, I strongly recommend
+checking out [Software Foundations](https://softwarefoundations.cis.upenn.edu/), a series
+of books on Coq written as comments in a Coq source file! In particular, check out
+[Logical Foundations](https://softwarefoundations.cis.upenn.edu/lf-current/index.html)
+for an introduction to using Coq. Thanks for reading!

content/blog/00_compiler_intro.md

@@ -145,4 +145,5 @@ Here are the posts that I've written so far for this series:
 * [Polymorphism]({{< relref "10_compiler_polymorphism.md" >}})
 * [Polymorphic Data Types]({{< relref "11_compiler_polymorphic_data_types.md" >}})
 * [Let/In and Lambdas]({{< relref "12_compiler_let_in_lambda/index.md" >}})
+* [Cleanup]({{< relref "13_compiler_cleanup/index.md" >}})
 

content/blog/00_compiler_intro.ru.md

@@ -1,97 +0,0 @@
----
-title: Пишем Компилятор Для Функционального Языка на С++, Часть 0 - Вступление
-date: 2019-08-03T01:02:30-07:00
-tags: ["C and C++", "Functional Languages", "Compilers"]
-description: "todo"
----
-Год назад, я был записан на курс по компиляторам. Я ждал этого момента почти два учебных года: еще со времени школы меня интересовало создание языков программирования. Однако я был разочарован - заданный нам финальный проект полностью состоял из склеивания вместе написанных профессором кусочков кода. Склеив себе такой грустный компилятор, я не почувствовал бы никакой гордости. А я хотел бы гордиться всеми своими проектами.
-
-Вместо стандартного задания, я решил -- с разрешением профессора -- написать компилятор для ленивого функционального языка, используя отличную книгу Саймона Пейтона Джоунса, _Implementing functional languages: a tutorial_. На курсе мы пользовались С++, и мой проект не был исключением. Получился прикольный маленький язык, и теперь я хочу рассказать вам, как вы тоже можете создать ваш собственный функциональный язык.  
-
-### Примечание к Русской Версии
-Вы читаете русскою версию этой статьи. Оригинал ее был написан год назад, и с тех пор объем всей серии немного изменился. Я планировал описать только те части компилятора, которые я успел закончить и сдать профессору: лексический анализ, синтаксический разбор, мономорфную проверку типов, и компиляцию простых выражений с помощью LLVM. Закончив и описав все эти части, я решил продолжать разрабатывать компилятор, и описал сборку мусора, полиморфную проверку типов, полиморфные структуры данных, а также компиляцию более сложных выражений. Вместо того чтобы писать наивный перевод английской версии -- притворяясь что я не знаю о перемене моих планов -- я буду вносить в эту версию изменения соответствующие сегодняшнему состоянию компилятора. Части статей не затронутые этими изменениями я тоже не буду переводить слово в слово, иначе они будут звучать ненатурально. Тем не менее техническое содержание каждой статьи будет аналогично содержанию ее английской версии, и код будет тот же самый. 
-
-### Мотивация
-Начать эту серию меня подтолкнули две причины. 
-
-Во-первых, почти все учебники и вступления к созданию компиляторов, с которыми я сталкивался, были написаны об императивных языках, часто похожих на C, C++, Python, или JavaScript. Я считаю, что в компиляции функциональных языков -- особенно ленивых -- есть много чего интересного, и все это относительно редко упоминается. 
-
-Во-вторых, меня вдохновили книги, как Software Foundations. Все содержание Software Foundations, например, написано в форме комментариев языка Coq. Таким образом, можно не только читать саму книгу, но и сразу же запускать находящийся рядом с комментариями код. Когда описываемый код под рукой, легче экспериментировать и интереснее читать. Принимая это во внимание, я выкладываю вместе с каждой статьей соответствующую версию компилятора; в самой статье описывается код именно из этой версии. Все части написанной мною программы полностью доступны. 
-
-### Обзор
-Прежде чем начинать наш проект, давайте обсудим, чего мы будем добиваться, и какими способами. 
-
-#### “Классические” Стадии Компилятора
-Части большинства компиляторов достаточно независимы друг от друга (по крайней мере в теории). Мы можем разделить их на следующие шаги:
-
-* Лексический анализ
-* Синтаксический разбор
-* Анализ и оптимизация
-* Генерация кода
-
-Не все вышеописанные шаги встречаются в каждом компиляторе. Например, компилятор в моих статьях совсем не оптимизирует код. Также, в некоторых компиляторах присутствуют шаги не упомянутые в этом списке. Язык Idris  -- как и многие другие функциональные языки -- переводится сначала в упрощённый язык “TT”, и только после этого проходит через анализ. Иногда, с целью ускорить компиляцию, несколько шагов производятся одновременно. В целом, все эти стадии помогут нам сориентироваться, но никаким образом нас не ограничат.  
-
-#### Темы, Которые Мы Рассмотрим
-Мы начнем с нуля, и пошагово построим компилятор состоящий из следующих частей:
-
-* Лексического анализа с помощью программы Flex.
-* Синтаксического разбора с помощью программы Bison.
-* Сначала мономорфной, а позже полиморфной проверки типов.
-* Вычисления программ используя абстрактную машину G-machine.
-* Компиляции абстрактных инструкций G-machine используя LLVM.
-* Простого сбора мусора.
-
-Наша цель - создать ленивый, функциональный язык.
-
-#### Темы, Которые Мы Не Рассмотрим
-Для того, чтобы создать любую нетривиальную программу, нужно иметь значительный объем опыта и знаний; одному человеку было бы сложно научить всему этому. У меня буквально не хватило бы на это времени, да и исход такой попытки был бы неблагоприятным: опытным читателям было бы труднее извлечь из статей новую информацию, а неопытным читателям все равно было бы недостаточно подробно. Вместо того, чтобы портить таким образом свои статьи, я буду полагаться на то, что вы достаточно комфортно себя чувствуете с некоторыми темами. В число этих тем входят:
-
-* [Теория алгоритмов](https://ru.wikipedia.org/wiki/%D0%A2%D0%B5%D0%BE%D1%80%D0%B8%D1%8F_%D0%B0%D0%BB%D0%B3%D0%BE%D1%80%D0%B8%D1%82%D0%BC%D0%BE%D0%B2),
-более конкретно [теория автоматов](https://ru.wikipedia.org/wiki/%D0%A2%D0%B5%D0%BE%D1%80%D0%B8%D1%8F_%D0%B0%D0%B2%D1%82%D0%BE%D0%BC%D0%B0%D1%82%D0%BE%D0%B2).
-Детерминированные и недетерминированные автоматы кратко упоминаются в первой статье во время лексического анализа, a синтаксический разбор мы выполним используя контекстно-свободную грамматику.
-* [Функциональное программирование](https://ru.wikipedia.org/wiki/%D0%A4%D1%83%D0%BD%D0%BA%D1%86%D0%B8%D0%BE%D0%BD%D0%B0%D0%BB%D1%8C%D0%BD%D0%BE%D0%B5_%D0%BF%D1%80%D0%BE%D0%B3%D1%80%D0%B0%D0%BC%D0%BC%D0%B8%D1%80%D0%BE%D0%B2%D0%B0%D0%BD%D0%B8%D0%B5), с легкой примесью [лямбда-исчисления](https://ru.wikipedia.org/wiki/%D0%9B%D1%8F%D0%BC%D0%B1%D0%B4%D0%B0-%D0%B8%D1%81%D1%87%D0%B8%D1%81%D0%BB%D0%B5%D0%BD%D0%B8%D0%B5).
-Мы будем пользоваться лямбда-функциями, каррированием, и системой типов Хиндли-Мильнер, которая часто встречается в языках семейства ML.
-* С++. Я стараюсь писать код правильно и по последним стандартам, но я не эксперт. Я не буду объяснять синтаксис или правила С++, но разумеется буду описывать что именно делает мой код с точки зрения компиляторов.
-
-#### Синтаксис Нашего Языка
-Саймон Пейтон Джоунс, в одном из своих [~~двух~~ многочисленных](https://www.reddit.com/r/ProgrammingLanguages/comments/dsu115/compiling_a_functional_language_using_c/f6t52mh?utm_source=share&utm_medium=web2x&context=3) трудов на тему функциональных языков, отметил что большинство из этих языков по сути очень похожи друг на друга; часто, главная разница состоит именно в их синтаксисе. На данный момент, выбор синтаксиса - наша главная степень свободы. Нам точно нужно предоставить доступ к следующим вещам:
-
-* Декларациям функций
-* Вызову функций
-* Арифметике
-* Aлгебраическим типам данных
-* Сопоставлению с образцом
-
-Позже, мы добавим к этому списку выражения let/in и лямбда-функции. С арифметикой разобраться не сложно - числа будут писаться просто как `3`, значения выражений как `1+2*3` будут высчитываться по обычным математическим правилам. Вызов функций ненамного сложнее. Выражение `f x` будет значить “вызов функции `f` с параметром `x`”, а `f x + g y` - “сумма значений `f x` и `g y`”. Заметьте, что вызов функций имеет приоритет выше приоритета арифметических операций.
-
-Теперь давайте придумаем синтаксис для деклараций функций. Я предлогаю следующий вариант:
-
-```
-defn f x = { x + x }
-```
-
-А для типов данных:
-
-```
-data List = { Nil, Cons Int List }
-```
-
-Заметьте, что мы пока пользуемся мономорфными декларациями типов данных. Позже, в одиннадцатой части, мы добавим синтаксис для полиморфных деклараций.
-
-В последнюю очередь, давайте определимся с синтаксисом сопоставления с образцом:
-
-```
-case l of {
-    Nil -> { 0 }
-    Cons x xs -> { x }
-}
-```
-
-Представленная выше распечатка читается как: “если лист `l` сопоставим с `Nil`, то все выражение возвращает значение `0`; иначе, если лист сопоставим с `Cons x xs` (что, опираясь на декларацию `List`, означает, что лист состоит из значений `x`, с типом `Int`, и `xs`, с типом `List`), то выражение возвращает `x`”.   
-
-Вот и конец нашего обзора! В следующей статье, мы начнем с лексического анализа, что является первым шагом в процессе трансформации программного текста в исполняемые файлы.
-
-### Список Статей
-* Ой! Тут как-то пусто.
-* Вы, наверно, читаете черновик.
-* Если нет, то пожалуйста напишите мне об этом!

content/blog/00_cs325_languages_hw1.md

@@ -1,7 +1,7 @@
 ---
 title: A Language for an Assignment - Homework 1
 date: 2019-12-27T23:27:09-08:00
-tags: ["Haskell", "Python", "Algorithms"]
+tags: ["Haskell", "Python", "Algorithms", "Programming Languages"]
 ---
 
 On a rainy Oregon day, I was walking between classes with a group of friends.

content/blog/01_aoc_coq.md

@@ -0,0 +1,940 @@
+---
+title: "Advent of Code in Coq - Day 8"
+date: 2021-01-10T22:48:39-08:00
+tags: ["Advent of Code", "Coq"]
+---
+
+Huh? We're on day 8? What happened to days 2 through 7?
+
+Well, for the most part, I didn't think they were that interesting from the Coq point of view.
+Day 7 got close, but not close enough to inspire me to create a formalization. Day 8, on the other
+hand, is
+{{< sidenote "right" "pl-note" "quite interesting," >}}
+Especially to someone like me who's interested in programming languages!
+{{< /sidenote >}} and took quite some time to formalize.
+
+As before, here's an (abridged) description of the problem:
+
+> Given a tiny assembly-like language, determine the state of its accumulator
+> when the same instruction is executed twice.
+
+Before we start on the Coq formalization, let's talk about an idea from
+Programming Language Theory (PLT), _big step operational semantics_.
+
+### Big Step Operational Semantics
+What we have in Advent of Code's Day 8 is, undeniably, a small programming language.
+We are tasked with executing this language, or, in PLT lingo, defining its _semantics_.
+There are many ways of doing this - at university, I've been taught of [denotational](https://en.wikipedia.org/wiki/Denotational_semantics), [axiomatic](https://en.wikipedia.org/wiki/Axiomatic_semantics), 
+and [operational](https://en.wikipedia.org/wiki/Operational_semantics) semantics.
+I believe that Coq's mechanism of inductive definitions lends itself very well
+to operational semantics, so we'll take that route. But even "operational semantics"
+doesn't refer to a concrete technique - we have a choice between small-step (structural) and
+big-step (natural) operational semantics. The former describe the minimal "steps" a program
+takes as it's being evaluated, while the latter define the final results of evaluating a program.
+I decided to go with big-step operational semantics, since they're more intutive (natural!).
+
+So, how does one go about "[defining] the final results of evaluating a program?" Most commonly,
+we go about using _inference rules_. Let's talk about those next.
+
+#### Inference Rules
+Inference rules are a very general notion. The describe how we can determine (infer) a conclusion
+from a set of assumptions. It helps to look at an example. Here's a silly little inference rule:
+
+{{< latex >}}
+\frac
+{\text{I'm allergic to cats} \quad \text{My friend has a cat}}
+{\text{I will not visit my friend very much}}
+{{< /latex >}}
+
+It reads, "if I'm allergic to cats, and if my friend has a cat, then I will not visit my friend very much".
+Here, "I'm allergic to cats" and "my friend has a cat" are _premises_, and "I will not visit my friend very much" is
+a _conclusion_. An inference rule states that if all its premises are true, then its conclusion must be true.
+Here's another inference rule, this time with some mathematical notation instead of words:
+
+{{< latex >}}
+\frac
+{n < m}
+{n + 1 < m + 1}
+{{< /latex >}}
+
+This one reads, "if \\(n\\) is less than \\(m\\), then \\(n+1\\) is less than \\(m+1\\)". We can use inference
+rules to define various constructs. As an example, let's define what it means for a natural number to be even.
+It takes two rules:
+
+{{< latex >}}
+\frac
+{}
+{0 \; \text{is even}}
+\quad
+\frac
+{n \; \text{is even}}
+{n+2 \; \text{is even}}
+{{< /latex >}}
+
+First of all, zero is even. We take this as fact - there are no premises for the first rule, so they
+are all trivially true. Next, if a number is even, then adding 2 to that number results in another
+even number. Using the two of these rules together, we can correctly determine whether any number
+is or isn't even. We start knowing that 0 is even. Adding 2 we learn that 2 is even, and adding 2
+again we see that 4 is even, as well. We can continue this to determine that 6, 8, 10, and so on
+are even too. Never in this process will we visit the numbers 1 or 3 or 5, and that's good - they're not even!
+
+Let's now extend this notion to programming languages, starting with a simple arithmetic language.
+This language is made up of natural numbers and the \\(\square\\) operation, which represents the addition
+of two numbers. Again, we need two rules:
+
+{{< latex >}}
+\frac
+{n \in \mathbb{N}}
+{n \; \text{evaluates to} \; n}
+\quad
+\frac
+{e_1 \; \text{evaluates to} \; n_1 \quad e_2 \; \text{evaluates to} \; n_2}
+{e_1 \square e_2 \; \text{evaluates to} \; n_1 + n_2}
+{{< /latex >}}
+
+First, let me explain myself. I used \\(\square\\) to demonstrate two important points. First, languages can be made of
+any kind of characters we want; it's the rules that we define that give these languages meaning.
+Second, while \\(\square\\) is the addition operation _in our language_, \\(+\\) is the _mathematical addition operator_.
+They are not the same - we use the latter to define how the former works.
+
+Finally, writing "evaluates to" gets quite tedious, especially for complex languages. Instead,
+PLT people use notation to make their semantics more concise. The symbol \\(\Downarrow\\) is commonly
+used to mean "evaluates to"; thus, \\(e \Downarrow v\\) reads "the expression \\(e\\) evaluates to the value \\(v\\).
+Using this notation, our rules start to look like the following:
+
+{{< latex >}}
+\frac
+{n \in \mathbb{N}}
+{n \Downarrow n}
+\quad
+\frac
+{e_1 \Downarrow n_1 \quad e_2 \Downarrow n_2}
+{e_1 \square e_2 \Downarrow n_1 + n_2}
+{{< /latex >}}
+
+If nothing else, these are way more compact! Though these may look intimidating at first, it helps to
+simply read each symbol as its English meaning.
+
+#### Encoding Inference Rules in Coq
+Now that we've seen what inference rules are, we can take a look at how they can be represented in Coq.
+We can use Coq's `Inductive` mechanism to define the rules. Let's start with our "is even" property.
+
+```Coq
+Inductive is_even : nat -> Prop :=
+    | zero_even : is_even 0
+    | plustwo_even : is_even n -> is_even (n+2).
+```
+
+The first line declares the property `is_even`, which, given a natural number, returns proposition.
+This means that `is_even` is not a proposition itself, but `is_even 0`, `is_even 1`, and `is_even 2`
+are all propositions.
+
+The following two lines each encode one of our aforementioned inference rules. The first rule, `zero_even`,
+is of type `is_even 0`. The `zero_even` rule doesn't require any arguments, and we can use it to create
+a proof that 0 is even. On the other hand, the `plustwo_even` rule _does_ require an argument, `is_even n`.
+To construct a proof that a number `n+2` is even using `plustwo_even`, we need to provide a proof
+that `n` itself is even. From this definition we can see a general principle: we encode each inference
+rule as constructor of an inductive Coq type. Each rule encoded in this manner takes as arguments
+the proofs of its premises, and returns a proof of its conclusion.
+
+For another example, let's encode our simple addition language. First, we have to define the language
+itself:
+
+```Coq
+Inductive tinylang : Type :=
+    | number (n : nat) : tinylang
+    | box (e1 e2 : tinylang) : tinylang.
+```
+
+This defines the two elements of our example language: `number n` corresponds to \\(n\\), and `box e1 e2` corresponds
+to \\(e_1 \square e_2\\). Finally, we define the inference rules:
+
+```Coq {linenos=true}
+Inductive tinylang_sem : tinylang -> nat -> Prop :=
+    | number_sem : forall (n : nat), tinylang_sem (number n) n
+    | box_sem : forall (e1 e2 : tinylang) (n1 n2 : nat),
+        tinylang_sem e1 n1 -> tinylang_sem e2 n2 ->
+        tinylang_sem (box e1 e2) (n1 + n2).
+```
+
+When we wrote our rules earlier, by using arbitrary variables like \\(e_1\\) and \\(n_1\\), we implicitly meant
+that our rules work for _any_ number or expression. When writing Coq we have to make this assumption explicit
+by using `forall`. For instance, the rule on line 2 reads, "for any number `n`, the expression `n` evaluates to `n`".
+
+#### Semantics of Our Language
+
+We've now written some example big-step operational semantics, both "on paper" and in Coq. Now, it's time to take a look at
+the specific semantics of the language from Day 8! Our language consists of a few parts.
+
+First, there are three opcodes: \\(\texttt{jmp}\\), \\(\\texttt{nop}\\), and \\(\\texttt{add}\\). Opcodes, combined
+with an integer, make up an instruction. For example, the instruction \\(\\texttt{add} \\; 3\\) will increase the
+content of the accumulator by three. Finally, a program consists of a sequence of instructions; They're separated
+by newlines in the puzzle input, but we'll instead separate them by semicolons. For example, here's a complete program.
+
+{{< latex >}}
+\texttt{add} \; 0; \; \texttt{nop} \; 2; \; \texttt{jmp} \; -2
+{{< /latex >}}
+
+Now, let's try evaluating this program. Starting at the beginning and with 0 in the accumulator,
+it will add 0 to the accumulator (keeping it the same),
+do nothing, and finally jump back to the beginning. At this point, it will try to run the addition instruction again,
+which is not allowed; thus, the program will terminate.
+
+Did you catch that? The semantics of this language will require more information than just our program itself (which we'll denote by \\(p\\)).
+* First, to evaluate the program we will need a program counter, \\(\\textit{c}\\). This program counter
+will tell us the position of the instruction to be executed next. It can also point past the last instruction,
+which means our program terminated successfully. 
+* Next, we'll need the accumulator \\(a\\). Addition instructions can change the accumulator, and we will be interested
+in the number that ends up in the accumulator when our program finishes executing.
+* Finally, and more subtly, we'll need to keep track of the states we visited. For instance,
+in the course of evaluating our program above, we encounter the \\((c, a)\\) pair of \\((0, 0)\\) twice: once
+at the beginning, and once at the end. However, whereas at the beginning we have not yet encountered the addition
+instruction, at the end we have, so the evaluation behaves differently. To make the proofs work better in Coq,
+we'll use a set \\(v\\) of
+{{< sidenote "right" "allowed-note" "allowed (valid) program counters (as opposed to visited program counters)." >}}
+Whereas the set of "visited" program counters keeps growing as our evaluation continues,
+the set of "allowed" program counters keeps shrinking. Because the "allowed" set never stops shrinking,
+assuming we're starting with a finite set, our execution will eventually terminate.
+{{< /sidenote >}}
+
+Now we have all the elements of our evaluation. Let's define some notation. A program starts at some state,
+and terminates in another, possibly different state. In the course of a regular evaluation, the program
+never changes; only the state does. So I propose this (rather unorthodox) notation:
+
+{{< latex >}}
+(c, a, v) \Rightarrow_p (c', a', v')
+{{< /latex >}}
+
+This reads, "after starting at program counter \\(c\\), accumulator \\(a\\), and set of valid addresses \\(v\\),
+the program \\(p\\) terminates with program counter \\(c'\\), accumulator \\(a'\\), and set of valid addresses \\(v'\\)".
+Before creating the inference rules for this evaluation relation, let's define the effect of evaluating a single
+instruction, using notation \\((c, a) \rightarrow_i (c', a')\\). An addition instruction changes the accumulator,
+and increases the program counter by 1.
+
+{{< latex >}}
+\frac{}
+{(c, a) \rightarrow_{\texttt{add} \; n} (c+1, a+n)}
+{{< /latex >}}
+
+A no-op instruction does even less. All it does is increment the program counter.
+
+{{< latex >}}
+\frac{}
+{(c, a) \rightarrow_{\texttt{nop} \; n} (c+1, a)}
+{{< /latex >}}
+
+Finally, a jump instruction leaves the accumulator intact, but adds a number to the program counter itself!
+
+{{< latex >}}
+\frac{}
+{(c, a) \rightarrow_{\texttt{jmp} \; n} (c+n, a)}
+{{< /latex >}}
+
+None of these rules have any premises, and they really are quite simple. Now, let's define the rules
+for evaluating a program. First of all, a program starting in a state that is not considered "valid"
+is done evaluating, and is in a "failed" state.
+
+{{< latex >}}
+\frac{c \not \in v \quad c \not= \text{length}(p)}
+{(c, a, v) \Rightarrow_{p} (c, a, v)}
+{{< /latex >}}
+
+We use \\(\\text{length}(p)\\) to represent the number of instructions in \\(p\\). Note the second premise:
+even if our program counter \\(c\\) is not included in the valid set, if it's "past the end of the program",
+the program terminates in an "ok" state.
+{{< sidenote "left" "avoid-c-note" "Here's a rule for terminating in the \"ok\" state:" >}}
+In the presented rule, we don't use the variable <code>c</code> all that much, and we know its concrete
+value (from the equality premise). We could thus avoid introducing the name \(c\) by
+replacing it with said known value:
+
+{{< latex >}}
+\frac{}
+{(\text{length}(p), a, v) \Rightarrow_{p} (\text{length}(p), a, v)}
+{{< /latex >}}
+
+This introduces some duplication, but that is really because all "base case" evaluation rules
+start and stop in the same state. To work around this, we could define a separate proposition
+to mean "program \(p\) is done in state \(s\)", then \(s\) will really only need to occur once,
+and so will \(\text{length}(p)\). This is, in fact, what we will do later on,
+since being able to talk abut "programs being done" will help us with
+components of our proof.
+{{< /sidenote >}}
+
+{{< latex >}}
+\frac{c = \text{length}(p)}
+{(c, a, v) \Rightarrow_{p} (c, a, v)}
+{{< /latex >}}
+
+When our program counter reaches the end of the program, we are also done evaluating it. Even though
+both rules {{< sidenote "right" "redundant-note" "lead to the same conclusion," >}}
+In fact, if the end of the program is never included in the valid set, the second rule is completely redundant.
+{{< /sidenote >}}
+it helps to distinguish the two possible outcomes. Finally, if neither of the termination conditions are met,
+our program can take a step, and continue evaluating from there.
+
+{{< latex >}}
+\frac{c \in v \quad p[c] = i \quad (c, a) \rightarrow_i (c', a') \quad (c', a', v - \{c\}) \Rightarrow_p (c'', a'', v'')}
+{(c, a, v) \Rightarrow_{p} (c'', a'', v'')}
+{{< /latex >}}
+
+This is quite a rule. A lot of things need to work out for a program to evauate from a state that isn't
+currently the final state:
+
+* The current program counter \\(c\\) must be valid. That is, it must be an element of \\(v\\).
+* This program counter must correspond to an instruction \\(i\\) in \\(p\\), which we write as \\(p[c] = i\\).
+* This instruction must be executed, changing our program counter from \\(c\\) to \\(c'\\) and our
+accumulator from \\(a\\) to \\(a'\\). The set of valid instructions will no longer include \\(c\\),
+and will become \\(v - \\{c\\}\\).
+* Our program must then finish executing, starting at state
+\\((c', a', v - \\{c\\})\\), and ending in some (unknown) state \\((c'', a'', v'')\\).
+
+If all of these conditions are met, our program, starting at \\((c, a, v)\\), will terminate in the state \\((c'', a'', v'')\\). This third rule completes our semantics; a program being executed will keep running instructions using the third rule, until it finally
+hits an invalid program counter (terminating with the first rule) or gets to the end of the program (terminating with the second rule).
+
+#### Aside: Vectors and Finite \\(\mathbb{N}\\)
+We'll be getting to the Coq implementation of our semantics soon, but before we do:
+what type should \\(c\\) be? It's entirely possible for an instruction like \\(\\texttt{jmp} \\; -10000\\)
+to throw our program counter way before the first instruction of our program, so at first, it seems
+as though we should use an integer. But the prompt doesn't even specify what should happen in this
+case - it only says an instruction shouldn't be run twice. The "valid set", although it may help resolve
+this debate, is our invention, and isn't part of the original specification.
+
+There is, however, something we can infer from this problem. Since the problem of jumping "too far behind" or
+"too far ahead" is never mentioned, we can assume that _all jumps will lead either to an instruction,
+or right to the end of a program_. This means that \\(c\\) is a natural number, with
+
+{{< latex >}}
+0 \leq c \leq \text{length}(p)
+{{< /latex >}}
+
+In a language like Coq, it's possible to represent such a number. Since we've gotten familliar with
+inference rules, let's present two rules that define such a number:
+
+{{< latex >}}
+\frac
+{n \in \mathbb{N}^+}
+{Z : \text{Fin} \; n}
+\quad
+\frac
+{f : \text{Fin} \; n}
+{S f : \text{Fin} \; (n+1)}
+{{< /latex >}}
+
+This is a variation of the [Peano encoding](https://wiki.haskell.org/Peano_numbers) of natural numbers.
+It reads as follows: zero (\\(Z\\)) is a finite natural number less than any positive natural number \\(n\\). Then, if a finite natural number
+\\(f\\) is less than \\(n\\), then adding one to that number (using the successor function \\(S\\))
+will create a natural number less than \\(n+1\\). We encode this in Coq as follows
+([originally from here](https://coq.inria.fr/library/Coq.Vectors.Fin.html#t)):
+
+```Coq
+Inductive t : nat -> Set :=
+    | F1 : forall {n}, t (S n)
+    | FS : forall {n}, t n -> t (S n).
+```
+
+The `F1` constructor here is equivalent to our \\(Z\\), and `FS` is equivalent to our \\(S\\).
+To represent positive natural numbers \\(\\mathbb{N}^+\\), we simply take a regular natural
+number from \\(\mathbb{N}\\) and find its successor using `S` (simply adding 1). Again, we have
+to explicitly use `forall` in our type signatures.
+
+We can use a similar technique to represent a list with a known number of elements, known
+in the Idris and Coq world as a vector. Again, we only need two inference rules to define such
+a vector:
+
+{{< latex >}}
+\frac
+{t : \text{Type}}
+{[] : \text{Vec} \; t \; 0}
+\quad
+\frac
+{x : \text{t} \quad \textit{xs} : \text{Vec} \; t \; n}
+{(x::\textit{xs}) : \text{Vec} \; t \; (n+1)}
+{{< /latex >}}
+
+These rules read: the empty list \\([]\\) is zero-length vector of any type \\(t\\). Then,
+if we take an element \\(x\\) of type \\(t\\), and an \\(n\\)-long vector \\(\textit{xs}\\) of \\(t\\),
+then we can prepend \\(x\\) to \\(\textit{xs}\\) and get an \\((n+1)\\)-long vector of \\(t\\).
+In Coq, we write this as follows ([originally from here](https://coq.inria.fr/library/Coq.Vectors.VectorDef.html#t)):
+
+```Coq
+Inductive t A : nat -> Type :=
+    | nil : t A 0
+    | cons : forall (h:A) (n:nat), t A n -> t A (S n).
+```
+
+The `nil` constructor represents the empty list \\([]\\), and `cons` represents
+the operation of prepending an element (called `h` in the code and \\(x\\) in our inference rules)
+to another vector of length \\(n\\), which remains unnamed in the code but is called \\(\\textit{xs}\\) in our rules.
+
+These two definitions work together quite well. For instance, suppose we have a vector of length \\(n\\).
+If we were to access its elements by indices starting at 0, we'd be allowed to access indices 0 through \\(n-1\\).
+These are precisely the values of the finite natural numbers less than \\(n\\), \\(\\text{Fin} \\; n \\).
+Thus, given such an index \\(\\text{Fin} \\; n\\) and a vector \\(\\text{Vec} \\; t \\; n\\), we are guaranteed
+to be able to retrieve the element at the given index! In our code, we will not have to worry about bounds checking.
+
+Of course, if our program has \\(n\\) elements, our program counter will be a finite number less than \\(n+1\\),
+since there's always the possibility of it pointing past the instructions, indicating that we've finished
+running the program. This leads to some minor complications: we can't safely access the program instruction
+at index \\(\\text{Fin} \\; (n+1)\\). We can solve this problem by considering two cases:
+either our index points one past the end of the program (in which case its value is exactly the finite
+representation of \\(n\\)), or it's less than \\(n\\), in which case we can "tighten" the upper bound,
+and convert that index into a \\(\\text{Fin} \\; n\\). We formalize it in a lemma:
+
+{{< codelines "Coq" "aoc-2020/day8.v" 80 82 >}}
+
+There's a little bit of a gotcha here. Instead of translating our above statement literally,
+and returning a value that's the result of "tightening" our input `f`, we return a value
+`f'` that can be "weakened" to `f`. This is because "tightening" is not a total function - 
+it's not always possible to convert a \\(\\text{Fin} \\; (n+1)\\) into a \\(\\text{Fin} \\; n\\).
+However, "weakening" \\(\\text{Fin} \\; n\\) _is_ a total function, since a number less than \\(n\\)
+is, by the transitive property of a total order, also less than \\(n+1\\).
+
+The Coq proof for this claim is as follows:
+
+{{< codelines "Coq" "aoc-2020/day8.v" 88 97 >}}
+
+The `Fin.rectS` function is a convenient way to perform inductive proofs over
+our finite natural numbers. Informally, our proof proceeds as follows:
+
+* If the current finite natural number is zero, take a look at the "bound" (which
+we assume is nonzero, since there isn't a natural number less than zero).
+    * If this "bounding number" is one, our `f` can't be tightened any further,
+    since doing so would create a number less than zero. Fortunately, in this case,
+    `n` must be `0`, so `f` is the finite representation of `n`.
+    * Otherwise, `f` is most definitely a weakened version of another `f'`,
+    since the tightest possible type for zero has a "bounding number" of one, and
+    our "bounding number" is greater than that. We return a tighter version of our finite zero.
+* If our number is a successor of another finite number, we check if that other number
+can itself be tightened.
+    * If it can't be tightened, then our smaller number is a finite representation of
+    `n-1`. This, in turn, means that adding one to it will be the finite representation
+    of `n` (if \\(x\\) is equal to \\(n-1\\), then \\(x+1\\) is equal to \\(n\\)).
+    * If it _can_ be tightened, then so can the successor (if \\(x\\) is less
+    than \\(n-1\\), then \\(x+1\\) is less than \\(n\\)).
+
+Next, let's talk about addition, specifically the kind of addition done by the \\(\\texttt{jmp}\\) instruction.
+We can always add an integer to a natural number, but we can at best guarantee that the result
+will be an integer. For instance, we can add `-1000` to `1`, and get `-999`, which is _not_ a natural
+number. We implement this kind of addition in a function called `jump_t`:
+
+{{< codelines "Coq" "aoc-2020/day8.v" 56 56 >}}
+
+At the moment, its definition is not particularly important. What is important, though,
+is that it takes a bounded natural number `pc` (our program counter), an integer `off`
+(the offset provided by the jump instruction) and returns another integer representing
+the final offset. Why are integers of type `t`? Well, it so happens
+that Coq provides facilities for working with arbitrary implementations of integers,
+without relying on how they are implemented under the hood. This can be seen in its
+[`Coq.ZArith.Int`](https://coq.inria.fr/library/Coq.ZArith.Int.html) module,
+which describes what functions and types an implementation of integers should provide.
+Among those is `t`, the type of an integer in such an arbitrary implementation. We too
+will not make an assumption about how the integers are implemented, and simply
+use this generic `t` from now on.
+
+Now, suppose we wanted to write a function that _does_ return a valid program
+counter after adding the offset to it. Since it's possible for this function to fail
+(for instance, if the offset is very negative), it has to return `option (fin (S n))`.
+That is, this function may either fail (returning `None`) or succeed, returning
+`Some f`, where `f` is of type `fin (S n)`, aka \\(\\text{Fin} \\; (n + 1)\\). Here's
+the function in Coq (again, don't worry too much about the definition):
+
+{{< codelines "Coq" "aoc-2020/day8.v" 61 61 >}}
+
+We will make use of this function when we define and verify our semantics.
+Let's take a look at that next.
+
+#### Semantics in Coq
+
+Now that we've seen finite sets and vectors, it's time to use them to
+encode our semantics in Coq. Before we do anything else, we need
+to provide Coq definitions for the various components of our
+language, much like what we did with `tinylang`. We can start with opcodes:
+
+{{< codelines "Coq" "aoc-2020/day8.v" 20 23 >}}
+
+Now we can define a few other parts of our language and semantics, namely
+states, instructions and programs (which I called "inputs" since, we'll, they're
+our puzzle input). A state is simply the 3-tuple of the program counter, the set
+of valid program counters, and the accumulator. We write it as follows:
+
+{{< codelines "Coq" "aoc-2020/day8.v" 33 33 >}}
+
+The star `*` is used here to represent a [product type](https://en.wikipedia.org/wiki/Product_type)
+rather than arithmetic multiplication. Our state type accepts an argument,
+`n`, much like a finite natural number or a vector. In fact, this `n` is passed on
+to the state's program counter and set types. Rightly, a state for a program
+of length \\(n\\) will not be of the same type as a state for a program of length \\(n+1\\).
+
+An instruction is also a tuple, but this time containing only two elements: the opcode and
+the number. We write this as follows:
+
+{{< codelines "Coq" "aoc-2020/day8.v" 36 36 >}}
+
+Finally, we have to define the type of a program. This type will also be
+indexed by `n`, the program's length. A program of length `n` is simply a
+vector of instructions `inst` of length `n`. This leads to the following
+definition:
+
+{{< codelines "Coq" "aoc-2020/day8.v" 38 38 >}}
+
+So far, so good! Finally, it's time to get started on the semantics themselves.
+We begin with the inductive definition of \\((\\rightarrow_i)\\).
+I think this is fairly straightforward. However, we do use
+`t` instead of \\(n\\) from the rules, and we use `FS`
+instead of \\(+1\\). Also, we make the formerly implicit
+assumption that \\(c+n\\) is valid explicit, by
+providing a proof that `valid_jump_t pc t = Some pc'`.
+
+{{< codelines "Coq" "aoc-2020/day8.v" 103 110 >}}
+
+Next, it will help us to combine the premises for
+"failed" and "ok" terminations into Coq data types.
+This will make it easier for us to formulate a lemma later on.
+Here are the definitions:
+
+{{< codelines "Coq" "aoc-2020/day8.v" 112 117 >}}
+
+Since all of out "termination" rules start and
+end in the same state, there's no reason to
+write that state twice. Thus, both `done`
+and `stuck` only take the input `inp`,
+and the state, which includes the accumulator
+`acc`, the set of allowed program counters `v`, and
+the program counter at which the program came to an end.
+When the program terminates successfully, this program
+counter will be equal to the length of the program `n`,
+so we use `nat_to_fin n`. On the other hand, if the program
+terminates in as stuck state, it must be that it terminated
+at a program counter that points to an instruction. Thus, this
+program counter is actually a \\(\\text{Fin} \\; n\\), and not
+a \\(\\text{Fin} \\ (n+1)\\), and is not in the set of allowed program counters.
+We use the same "weakening" trick we saw earlier to represent
+this.
+
+Finally, we encode the three inference rules we came up with:
+
+{{< codelines "Coq" "aoc-2020/day8.v" 119 126 >}}
+
+Notice that we fused two of the premises in the last rule.
+Instead of naming the instruction at the current program
+counter (by writing \\(p[c] = i\\)) and using it in another premise, we simply use
+`nth inp pc`, which corresponds to \\(p[c]\\) in our
+"paper" semantics.
+
+Before we go on writing some actual proofs, we have
+one more thing we have to address. Earlier, we said:
+
+> All jumps will lead either to an instruction, or right to the end of a program.
+
+To make Coq aware of this constraint, we'll have to formalize it. To
+start off, we'll define the notion of a "valid instruction", which is guaranteed
+to keep the program counter in the correct range.
+There are a couple of ways to do this, but we'll use yet another definition based
+on inference rules. First, though, observe that the same instruction may be valid
+for one program, and invalid for another. For instance, \\(\\texttt{jmp} \\; 100\\)
+is perfectly valid for a program with thousands of instructions, but if it occurs
+in a program with only 3 instructions, it will certainly lead to disaster. Specifically,
+the validity of an instruction depends on the length of the program in which it resides,
+and the program counter at which it's encountered.
+Thus, we refine our idea of validity to "being valid for a program of length \\(n\\) at program counter \\(f\\)".
+For this, we can use the following two inference rules:
+
+{{< latex >}}
+\frac
+{c : \text{Fin} \; n}
+{\texttt{add} \; t \; \text{valid for} \; n, c }
+\quad
+\frac
+{c : \text{Fin} \; n \quad o \in \{\texttt{nop}, \texttt{jmp}\} \quad J_v(c, t) = \text{Some} \; c' }
+{o \; t \; \text{valid for} \; n, c }
+{{< /latex >}}
+
+The first rule states that if a program has length \\(n\\), then \\(\\texttt{add}\\) is valid
+at any program counter whose value is less than \\(n\\). This is because running
+\\(\\texttt{add}\\) will increment the program counter \\(c\\) by 1,
+and thus, create a new program counter that's less than \\(n+1\\),
+which, as we discussed above, is perfectly valid.
+
+The second rule works for the other two instructions. It has an extra premise:
+the result of `jump_valid_t` (written as \\(J_v\\)) has to be \\(\\text{Some} \\; c'\\),
+that is, `jump_valid_t` must succeed. Note that we require this even for no-ops,
+since it later turns out that one of the them may be a jump after all.
+
+We now have our validity rules. If an instruction satisfies them for a given program
+and at a given program counter, evaluating it will always result in a program counter that has a proper value.
+We encode the rules in Coq as follows:
+
+{{< codelines "Coq" "aoc-2020/day8.v" 152 157 >}}
+
+Note that we have three rules instead of two. This is because we "unfolded"
+\\(o\\) from our second rule: rather than using set notation (or "or"), we
+just generated two rules that vary in nothing but the operation involved.
+
+Of course, we must have that every instruction in a program is valid.
+We don't really need inference rules for this, as much as a "forall" quantifier.
+A program \\(p\\) of length \\(n\\) is valid if the following holds:
+
+{{< latex >}}
+\forall (c : \text{Fin} \; n). p[c] \; \text{valid for} \; n, c
+{{< /latex >}}
+
+That is, for every possible in-bounds program counter \\(c\\),
+the instruction at the program counter is valid. We can now
+encode this in Coq, too:
+
+{{< codelines "Coq" "aoc-2020/day8.v" 160 161 >}}
+
+In the above, `n` is made implicit where possible.
+Since \\(c\\) (called `pc` in the code) is of type \\(\\text{Fin} \\; n\\), there's no
+need to write \\(n\\) _again_. The curly braces tell Coq to infer that
+argument where possible.
+
+### Proving Termination
+Here we go! It's finally time to make some claims about our
+definitions. Who knows - maybe we wrote down total garbage!
+We will be creating several related lemmas and theorems.
+All of them share two common assumptions:
+
+* We have some valid program `inp` of length `n`.
+* This program is a valid input, that is, `valid_input` holds for it.
+There's no sense in arguing based on an invalid input program.
+
+We represent these grouped assumptions by opening a Coq
+`Section`, which we call `ValidInput`, and listing our assumptions:
+
+{{< codelines "Coq" "aoc-2020/day8.v" 163 166 >}}
+
+We had to also explicitly mention the length `n` of our program.
+From now on, the variables `n`, `inp`, and `Hv` will be
+available to all of the proofs we write in this section.
+The first proof is rather simple. The claim is:
+
+> For our valid program, at any program counter `pc`
+and accumulator `acc`, there must exist another program
+counter `pc'` and accumulator `acc'` such that the
+instruction evaluation relation \\((\rightarrow_i)\\)
+connects the two. That is, valid addresses aside,
+we can always make a step.
+
+Here is this claim encoded in Coq:
+
+{{< codelines "Coq" "aoc-2020/day8.v" 168 169 >}}
+
+We start our proof by introducing all the relevant variables into
+the global context. I've mentioned this when I wrote about
+day 1, but here's the gist: the `intros` keyword takes
+variables from a `forall`, and makes them concrete.
+In short, `intros x` is very much like saying "suppose
+we have an `x`", and going on with the proof.
+
+{{< codelines "Coq" "aoc-2020/day8.v" 170 171 >}}
+
+Here, we said "take any program counter `pc` and any
+accumulator `acc`". Now what? Well, first of all,
+we want to take a look at the instruction at the current
+`pc`. We know that this instruction is a combination
+of an opcode and a number, so we use `destruct` to get
+access to both of these parts:
+
+{{< codelines "Coq" "aoc-2020/day8.v" 172 172 >}}
+
+Now, Coq reports the following proof state:
+
+```
+1 subgoal
+
+n : nat
+inp : input n
+Hv : valid_input inp
+pc : Fin.t n
+acc : t
+o : opcode
+t0 : t
+Hop : nth inp pc = (o, t0)
+
+========================= (1 / 1)
+
+exists (pc' : fin (S n)) (acc' : t),
+  step_noswap (o, t0) (pc, acc) (pc', acc')
+```
+
+We have some opcode `o`, and some associated number
+`t0`, and we must show that there exist a `pc'`
+and `acc'` to which we can move on. To prove
+that something exists in Coq, we must provide
+an instance of that "something". If we claim
+that there exists a dog that's not a good boy,
+we better have this elusive creature in hand.
+In other words, proofs in Coq are [constructive](https://en.wikipedia.org/wiki/Constructive_proof).
+Without knowing the kind of operation we're dealing with, we can't
+say for sure how the step will proceed. Thus, we proceed by
+case analysis on `o`.
+
+{{< codelines "Coq" "aoc-2020/day8.v" 173 173 >}}
+
+There are three possible cases we have to consider,
+one for each type of instruction.
+
+* If the instruction is \\(\\texttt{add}\\), we know
+that `pc' = pc + 1` and `acc' = acc + t0`. That is,
+the program counter is simply incremented, and the accumulator
+is modified with the number part of the instruction.
+* If the instruction is \\(\\texttt{nop}\\), the program
+coutner will again be incremented (`pc' = pc + 1`),
+but the accumulator will stay the same, so `acc' = acc`.
+* If the instruction is \\(\\texttt{jmp}\\), things are
+more complicated. We must rely on the assumption
+that our input is valid, which tells us that adding
+`t0` to our `pc` will result in `Some f`, and not `None`.
+Given this, we have `pc' = f`, and `acc' = acc`.
+
+This is how these three cases are translated to Coq:
+
+{{< codelines "Coq" "aoc-2020/day8.v" 174 177 >}}
+
+For the first two cases, we simply provide the
+values we expect for `pc'` and `acc'`, and
+apply the corresponding inference rule that
+is satisfied by these values. For the third case, we have
+to invoke `Hv`, the hypothesis that our input is valid.
+In particular, we care about the instruction at `pc`,
+so we use `specialize` to plug `pc` into the more general
+hypothesis. We then replace `nth inp pc` with its known
+value, `(jmp, t0)`. This tells us the following, in Coq's words:
+
+```
+Hv : valid_inst (jmp, t0) pc
+```
+
+That is, `(jmp, t0)` is a valid instruction at `pc`. Then, using
+Coq's `inversion` tactic, we ask: how is this possible? There is
+only one inference rule that gives us such a conclusion, and it is named `valid_inst_jmp`
+in our Coq code. Since we have a proof that our `jmp` is valid,
+it must mean that this rule was used. Furthermore, since this
+rule requires that `valid_jump_t` evaluates to `Some f'`, we know
+that this must be the case here! Coq now has adds the following
+two lines to our proof state:
+
+```
+f' : fin (S n)
+H0 : valid_jump_t pc t0 = Some f'
+```
+
+Finally, we specify, as mentioned earlier, that `pc' = f'` and `acc' = acc`.
+As before, we apply the corresponding step rule for `jmp`. When it asks
+for a proof that `valid_jump_t` produces a valid program counter,
+we hand it `H0` using `apply H0`. And with that, Coq is happy!
+
+Next, we prove a claim that a valid program can always do _something_,
+and that something is one of three things:
+
+* It can terminate in the "ok" state if the program counter
+reaches the programs' end.
+* It can terminate with an error if it's currently at a program
+counter that is not included in the valid set.
+* Otherwise, it can run the current instruction and advance
+to a "next" state.
+
+Alternatively, we could say that one of the inference rules
+for \\((\\Rightarrow_p)\\) must apply. This is not the case if the input
+is not valid, since, as I said
+before, an arbitrary input program can lead us to jump
+to a negative address (or to an address _way_ past the end of the program).
+Here's the claim, translated to Coq:
+
+{{< codelines "Coq" "aoc-2020/day8.v" 181 186 >}}
+
+Informally, we can prove this as follows:
+
+* If the current program counter is equal to the length
+of the program, we've reached the end. Thus, the program
+can terminate in the "ok" state.
+* Otherwise, the current program counter must be
+less than the length of the program.
+    * If we've already encountered this program counter (that is,
+    if it's gone from the set of valid program counters),
+    then the program will terminate in the "error" state.
+    * Otherwise, the program counter is in the set of
+    valid instructions. By our earlier theorem, in a valid
+    program, the instruction at any program counter can be correctly
+    executed, taking us to the next state. Now too
+    our program can move to this next state.
+
+Below is the Coq translation of the above.
+
+{{< codelines "Coq" "aoc-2020/day8.v" 187 203 >}}
+
+It doesn't seem like we're that far from being done now.
+A program can always take a step, and each time it does,
+the set of valid program counters decreases in size. Eventually,
+this set will become empty, so if nothing else, our program will
+eventually terminate in an "error" state. Thus, it will stop
+running no matter what. 
+
+This seems like a task for induction, in this case on the size
+of the valid set. In particular, strong mathematical induction
+{{< sidenote "right" "strong-induction-note" "seem to work best." >}}
+Why strong induction? If we remove a single element from a set,
+its size should decrease strictly by 1. Thus, why would we need
+to care about sets of <em>all</em> sizes less than the current
+set's size?<br>
+<br>
+Unfortunately, we're not working with purely mathematical sets.
+Coq's default facility for sets is simply a layer on top
+of good old lists, and makes no effort to be "correct by construction".
+It is thus perfectly possible to have a "set" which inlcudes an element
+twice. Depending on the implementation of <code>set_remove</code>,
+we may end up removing the repeated element multiple times, thereby
+shrinking the length of our list by more than 1. I'd rather
+not worry about implementation details like that.
+{{< /sidenote >}}
+Someone on StackOverflow [implemented this](https://stackoverflow.com/questions/45872719/how-to-do-induction-on-the-length-of-a-list-in-coq),
+so I'll just use it. The Coq theorem corresonding to strong induction
+on the length of a list is as follows:
+
+{{< codelines "Coq" "aoc-2020/day8.v" 205 207 >}}
+
+It reads,
+
+> If for some list `l`, the property `P` holding for all lists
+shorter than `l` means that it also holds for `l` itself, then
+`P` holds for all lists.
+
+This is perhaps not particularly elucidating. We can alternatively
+think of this as trying to prove some property for all lists `l`.
+We start with all empty lists. Here, we have nothing else to rely
+on; there are no lists shorter than the empty list, and our property
+must hold for all empty lists. Then, we move on to proving
+the property for all lists of length 1, already knowing that it holds
+for all empty lists. Once we're done there, we move on to proving
+that `P` holds for all lists of length 2, now knowing that it holds
+for all empty lists _and_ all lists of length 1. We continue
+doing this, eventually covering lists of any length.
+
+Before proving termination, there's one last thing we have to
+take care off. Coq's standard library does not come with
+a proof that removing an element from a set makes it smaller;
+we have to provide it ourselves. Here's the claim encoded
+in Coq:
+
+{{< codelines "Coq" "aoc-2020/day8.v" 217 219 >}}
+
+This reads, "if a set `s` contains a finite natural
+number `f`, removing `f` from `s` reduces the set's size".
+The details of the proof are not particularly interesting,
+and I hope that you understand intuitively why this is true.
+Finally, we make our termination claim.
+
+{{< codelines "Coq" "aoc-2020/day8.v" 230 231 >}}
+
+It's quite a strong claim - given _any_ program counter,
+set of valid addresses, and accumulator, a valid input program
+will terminate. Let's take a look at the proof.
+
+{{< codelines "Coq" "aoc-2020/day8.v" 232 234 >}}
+
+We use `intros` again. However, it brings in variables
+in order, and we really only care about the _second_ variable.
+We thus `intros` the first two, and then "put back" the first
+one using `generalize dependent`. Then, we proceed by
+induction on length, as seen above.
+
+{{< codelines "Coq" "aoc-2020/day8.v" 235 236>}}
+
+Now we're in the "inductive step". Our inductive hypothesis
+is that any set of valid addresses smaller than the current one will
+guarantee that the program will terminate. We must show
+that using our set, too, will guarantee termination. We already
+know that a valid input, given a state, can have one of three
+possible outcomes: "ok" termination, "failed" termination,
+or a "step". We use `destruct` to take a look at each of these
+in turn. The first two cases ("ok" termination and "failed" termination)
+are fairly trivial:
+
+{{< codelines "Coq" "aoc-2020/day8.v" 237 240 >}}
+
+We basically connect the dots between the premises (in a form like `done`)
+and the corresponding inference rule (`run_noswap_ok`). The more
+interesting case is when we can take a step.
+
+{{< codelines "Coq" "aoc-2020/day8.v" 241 253 >}}
+
+Since we know we can take a step, we know that we'll be removing
+the current program counter from the set of valid addresses. This
+set must currently contain the present program counter (since otherwise
+we'd have "failed"), and thus will shrink when we remove it. This,
+in turn, lets us use the inductive hypothesis: it tells us that no matter the
+program counter or accumulator, if we start with this new "shrunk"
+set, we will terminate in some state. Coq's constructive
+nature helps us here: it doesn't just tells us that there is some state
+in which we terminate - it gives us that state! We use `edestruct` to get
+a handle on this final state, which Coq automatically names `x`. At this
+time Coq still isn't convinced that our new set is smaller, so we invoke
+our earlier `set_remove_length` theorem to placate it.
+
+We now have all the pieces: we know that we can take a step, removing
+the current program counter from our current set. We also know that
+with that newly shrunken set, we'll terminate in some final state `x`.
+Thus, all that's left to say is to apply our "step" rule. It asks
+us for three things:
+
+1. That the current program counter is in the set. We've long since
+established this, and `auto` takes care of that.
+2. That a step is possible. We've already established this, too,
+since we're in the "can take a step" case. We apply `Hst`,
+the hypothesis that confirms that we can, indeed, step.
+3. That we terminate after this. The `x` we got
+from our induction hypothesis came with a proof that
+running with the "next" program counter and accumulator
+will result in termination. We apply this proof, automatically
+named `H0` by Coq.
+
+And that's it! We've proved that a program terminates no matter what.
+This has also (almost!) given us a solution to part 1. Consider the case
+in which we start with program counter 0, accumulator 0, and the "full"
+set of allowed program counters. Since our proof works for _all_ configurations,
+it will also work for this one. Furthermore, since Coq proofs are constructive,
+this proof will __return to us the final program counter and accumulator!__
+This is precisely what we'd need to solve part 1.
+
+But wait, almost? What's missing? We're missing a few implementation details:
+* We've not provided a concrete impelmentation of integers. The simplest
+thing to do here would be to use [`Coq.ZArith.BinInt`](https://coq.inria.fr/library/Coq.ZArith.BinInt.html),
+for which there is a module [`Z_as_Int`](https://coq.inria.fr/library/Coq.ZArith.Int.html#Z_as_Int)
+that provides `t` and friends.
+* We assumed (reasonably, I would say) that it's possible to convert a natural
+number to an integer. If we're using the aforementioned `BinInt` module,
+we can use [`Z.of_nat`](https://coq.inria.fr/library/Coq.ZArith.BinIntDef.html#Z.of_nat).
+* We also assumed (still reasonably) that we can try convert an integer
+back to a finite natural number, failing if it's too small or too large.
+There's no built-in function for this, but `Z`, for one, distinguishes
+between the "positive", "zero", and "negative" cases, and we have
+`Pos.to_nat` for the positive case.
+
+Well, I seem to have covered all the implementation details. Why not just
+go ahead and solve the problem? I tried, and ran into two issues:
+
+* Although this is "given", we assumed that our input program will be
+valid. For us to use the result of our Coq proof, we need to provide it
+a constructive proof that our program is valid. Creating this proof is tedious
+in theory, and quite difficult in practice: I've run into a
+strange issue trying to pattern match on finite naturals.
+* Even supposing we _do_ have a proof of validity, I'm not certain
+if it's possible to actually extract an answer from it. It seems
+that Coq distinguishes between proofs (things of type `Prop`) and
+values (things of type `Set`). things of types `Prop` are supposed
+to be _erased_. This means that when you convert Coq code,
+to, say, Haskell, you will see no trace of any `Prop`s in that generated
+code. Unfortunately, this also means we
+[can't use our proofs to construct values](https://stackoverflow.com/questions/27322979/why-coq-doesnt-allow-inversion-destruct-etc-when-the-goal-is-a-type),
+even though our proof objects do indeed contain them.
+
+So, we "theoretically" have a solution to part 1, down to the algorithm
+used to compute it and a proof that our algorithm works. In "reality", though, we
+can't actually use this solution to procure an answer. Like we did with day 1, we'll have
+to settle for only a proof.
+
+Let's wrap up for this post. It would be more interesting to devise and
+formally verify an algorithm for part 2, but this post has already gotten
+quite long and contains a lot of information. Perhaps I will revisit this
+at a later time. Thanks for reading!

content/blog/01_cs325_languages_hw2.md

@@ -1,7 +1,7 @@
 ---
 title: A Language for an Assignment - Homework 2
 date: 2019-12-30T20:05:10-08:00
-tags: ["Haskell", "Python", "Algorithms"]
+tags: ["Haskell", "Python", "Algorithms", "Programming Languages"]
 ---
 
 After the madness of the

content/blog/02_cs325_languages_hw3.md

@@ -1,7 +1,7 @@
 ---
 title: A Language for an Assignment - Homework 3
 date: 2020-01-02T22:17:43-08:00
-tags: ["Haskell", "Python", "Algorithms"]
+tags: ["Haskell", "Python", "Algorithms", "Programming Languages"]
 ---
 
 It rained in Sunriver on New Year's Eve, and it continued to rain

content/blog/02_learning_emulation.md

@@ -3,7 +3,7 @@ title: Learning Emulation, Part 2
 date: 2016-11-23 23:23:18.664038
 tags: ["C and C++", "Emulation"]
 ---
-_This is the second post in a series I'm writing about Chip-8 emulation. If you want to see the first one, head [here]({{< ref "/blog/01_learning_emulation.md" >}})._
+_This is the second post in a series I'm writing about Chip-8 emulation. If you want to see the first one, head [here]({{< relref "/blog/01_learning_emulation.md" >}})._
 
 Now that we have an understanding of the physical capabilities of a Chip-8 system, we can write code that will represent such a system on our computer. In this post we'll start writing some basic code - be prepared.
 

content/blog/03_learning_emulation.md

@@ -3,7 +3,7 @@ title: Learning Emulation, Part 2.5 - Implementation
 date: 2016-11-23 23:23:56.633942
 tags: ["C and C++", "Emulation"]
 ---
-_This is the third post in a series I'm writing about Chip-8 emulation. If you want to see the first one, head [here]({{< ref "/blog/01_learning_emulation.md" >}})._
+_This is the third post in a series I'm writing about Chip-8 emulation. If you want to see the first one, head [here]({{< relref "/blog/01_learning_emulation.md" >}})._
 
 In the previous part of this tutorial, we created a type to represent a basic Chip-8 machine. However, we've done nothing to make it behave like one! Let's start working on that.
 

content/blog/10_compiler_polymorphism.md

@@ -3,6 +3,7 @@ title: Compiling a Functional Language Using C++, Part 10 - Polymorphism
 date: 2020-03-25T17:14:20-07:00
 tags: ["C and C++", "Functional Languages", "Compilers"]
 description: "In this post, we extend our compiler's typechecking algorithm to implement the Hindley-Milner type system, allowing for polymorphic functions."
+favorite: true
 ---
 
 [In part 8]({{< relref "08_compiler_llvm.md" >}}), we wrote some pretty interesting programs in our little language.

content/blog/12_compiler_let_in_lambda/index.md

@@ -984,5 +984,6 @@ Before either of those things, though, I think that I want to go through
 the compiler and perform another round of improvements, similarly to
 [part 4]({{< relref "04_compiler_improvements" >}}). It's hard to do a lot
 of refactoring while covering new content, since major changes need to
-be explained and presented for the post to make sense. I hope to see
+be explained and presented for the post to make sense.
-you in these future posts!
+I do this in [part 13]({{< relref "13_compiler_cleanup/index.md" >}}) - cleanup.
+I hope to see you there!