Update theme with syntax highlighting fix

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>

.drone.yml

@@ -0,0 +1,38 @@
+kind: pipeline
+type: docker
+name: default
+
+volumes:
+  - name: live-output
+    temp: {}
+
+steps:
+  - name: test-compiler
+    image: archlinux
+    commands:
+    - pacman -Sy cmake gcc make llvm bison flex gettext libffi --noconfirm
+    - cd code/compiler
+    - ./test.sh
+  - name: build-live
+    image: klakegg/hugo:ext-alpine
+    commands:
+    - hugo -D --baseUrl "http://danilafe.com:8080"
+    volumes:
+    - name: live-output
+      path: /live-output
+    environment:
+      HUGO_DESTINATION: /live-output
+# - name: upload-live
+#   image: eeacms/rsync
+#   commands:
+#   - eval `ssh-agent -s`
+#   - echo "$CUSTOM_KEY" | ssh-add -
+#   - mkdir -p ~/.ssh
+#   - echo -e "Host *\n\tStrictHostKeyChecking no\n\n" > ~/.ssh/config
+#   - rsync -rv -e "ssh -p 22" /live-output/ blog-live@danilafe.com:/var/www/blog-live/ --checksum
+#   environment:
+#     CUSTOM_KEY:
+#       from_secret: live_ssh_key
+#   volumes:
+#   - name: live-output
+#     path: /live-output

.gitmodules

@@ -0,0 +1,18 @@
+[submodule "code/aoc-2020"]
+	path = code/aoc-2020
+	url = https://dev.danilafe.com/Advent-of-Code/AdventOfCode-2020.git
+[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
+[submodule "code/blog-static-flake"]
+	path = code/blog-static-flake
+	url = https://dev.danilafe.com/Nix-Configs/blog-static-flake.git
+[submodule "code/compiler"]
+	path = code/compiler
+	url = https://dev.danilafe.com/DanilaFe/bloglang.git
+[submodule "code/agda-spa"]
+	path = code/agda-spa
+	url = https://dev.danilafe.com/DanilaFe/agda-spa.git

Gemfile

@@ -0,0 +1,9 @@
+# frozen_string_literal: true
+
+source "https://rubygems.org"
+
+git_source(:github) {|repo_name| "https://github.com/#{repo_name}" }
+
+gem 'nokogiri'
+gem 'execjs'
+gem 'duktape'

Gemfile.lock

@@ -0,0 +1,21 @@
+GEM
+  remote: https://rubygems.org/
+  specs:
+    duktape (2.7.0.0)
+    execjs (2.9.1)
+    mini_portile2 (2.8.8)
+    nokogiri (1.18.3)
+      mini_portile2 (~> 2.8.2)
+      racc (~> 1.4)
+    racc (1.8.1)
+
+PLATFORMS
+  ruby
+
+DEPENDENCIES
+  duktape
+  execjs
+  nokogiri
+
+BUNDLED WITH
+   2.1.4

agda.rb

@@ -0,0 +1,351 @@
+require "nokogiri"
+require "pathname"
+
+files = ARGV[0..-1]
+
+class LineInfo
+  attr_accessor :links
+
+  def initialize
+    @links = []
+  end
+end
+
+class AgdaContext
+  def initialize
+    @file_infos = {}
+  end
+
+  # Traverse the preformatted Agda block in the given Agda HTML file
+  # and find which textual ranges have IDs and links to other ranges.
+  # Store this information in a hash, line => LineInfo.
+  def process_agda_html_file(file)
+    return @file_infos[file] if @file_infos.include? file
+
+    @file_infos[file] = line_infos = {}
+    unless File.exist?(file)
+      return line_infos
+    end
+
+    document = Nokogiri::HTML.parse(File.open(file))
+    pre_code = document.css("pre.Agda")[0]
+
+    # The traversal postorder; we always visit children before their
+    # parents, and we visit leaves in sequence.
+    offset = 0
+    line = 1
+    pre_code.traverse do |at|
+      # Text nodes are always leaves; visiting a new leaf means we've advanced
+      # in the text by the length of that text. However, if there are newlines
+      # -- since this is a preformatted block -- we also advanced by a line.
+      # At this time, do not support links that span multiple lines, but
+      # Agda doesn't produce those either.
+      if at.text?
+        if at.content.include? "\n"
+          # This textual leaf is at least part whitespace. The logic
+          # assumes that links can't span multiple pages, and that links
+          # aren't nested, so ensure that the parent of the textual node
+          # is the preformatted block itself.
+          raise "unsupported Agda HTML output" if at.parent.name != "pre"
+
+          # Increase the line and track the final offset. Written as a loop
+          # in case we eventually want to add some handling for the pieces
+          # sandwiched between newlines.
+          at.content.split("\n", -1).each_with_index do |bit, idx|
+            line += 1 unless idx == 0
+            offset = bit.length
+          end
+        else
+          # It's not a newline node, so it could be anywhere. All we need to
+          # do is adjust the offset within the full pre block's text.
+          offset += at.content.length
+        end
+      elsif at.name == "a"
+        # We found a link. Agda emits both links and "things to link to" as
+        # 'a' nodes, so check for either, and record them. Even if
+        # the link is nested, the .content.length accessor will only
+        # retrieve the textual content, and thus -- assuming the link
+        # isn't split across lines -- will find the proper from-to range.
+
+        line_info = line_infos.fetch(line) { line_infos[line] = LineInfo.new }
+        href = at.attribute("href")
+        id = at.attribute("id")
+        if href or id
+          new_node = { :from => offset-at.content.length, :to => offset }
+          new_node[:href] = href if href
+          new_node[:id] = id if id
+
+          line_info.links << new_node
+        end
+      end
+    end
+    return line_infos
+  end
+end
+
+class FileGroup
+  def initialize(agda_context)
+    @agda_context = agda_context
+    # Agda HTML href -> list of (file, Hugo HTML node that links to it)
+    @nodes_referencing_href = {}
+    # Agda HTML href -> (its new ID in Hugo-land, file in which it's defined)
+    # This supports cross-post linking within a seires.
+    @global_seen_hrefs = {}
+    # file name -> Agda HTML href -> its new ID in Hugo-land
+    # This supports linking within a particular post.
+    @local_seen_hrefs = Hash.new { {} }
+    # Global counter to generate fresh IDs. There's no reason for it to
+    # be global within a series (since IDs are namespaced by the file they're in),
+    # but it's just more convenient this way.
+    @id_counter = 0
+  end
+
+  def note_defined_href(file, href)
+    file_hrefs = @local_seen_hrefs.fetch(file) do
+      @local_seen_hrefs[file] = {}
+    end
+
+    uniq_id = file_hrefs.fetch(href) do
+      new_id = "agda-unique-ident-#{@id_counter}"
+      @id_counter += 1
+      file_hrefs[href] = new_id
+    end
+
+    unless @global_seen_hrefs.include? href
+      @global_seen_hrefs[href] = { :file => file, :id => uniq_id }
+    end
+
+    return uniq_id
+  end
+
+  def note_used_href(file, node, href)
+    ref_list = @nodes_referencing_href.fetch(href) { @nodes_referencing_href[href] = [] }
+    ref_list << { :file => file, :node => node }
+    return href
+  end
+
+  # Given a Hugo HTML file which references potentially several Agda modules
+  # in code blocks, insert links into the code blocks.
+  #
+  # There are several things we need to take care of:
+  # 1. Finding the HTML files associated with each referenced Agda module.
+  #    For this, we make use of the data-base-path etc. attributes that
+  #    the vanilla theme inserts.
+  # 2. "zipping together" the Agda and Hugo HTML representations. Each of
+  #    them encode the code, but they use different HTML elements and structures.
+  #    So, given a Hugo HTML code block, traverse its textual contents
+  #    and find any that are covered by links in the related Agda HTML file.
+  # 3. Fixing up links: the Agda HTML links assume each module has its own HTML
+  #    file. This isn't true for us: multiple modules are stitched into
+  #    one Hugo HTML file. Also, we don't include the entire Agda HTML
+  #    file in the Hugo HTML, so some links may be broken. So, find IDs
+  #    that are visible in the Hugo file, rename them to be globally unique,
+  #    and re-write cross-file links that reference these IDs to point
+  #    inside the Hugo file.
+  def process_source_file(file, document)
+    # Process each highlight group that's been marked as an Agda file.
+    document.css('div[data-agda-block]').each do |t|
+      first_line, last_line = nil, nil
+
+      if first_line_attr = t.attribute("data-first-line")
+        first_line = first_line_attr.to_s.to_i
+      end
+      if last_line_attr = t.attribute("data-last-line")
+        last_line = last_line_attr.to_s.to_i
+      end
+
+      if first_line and last_line
+        line_range = first_line..last_line
+      else
+        line_range = 1..
+      end
+
+      # Sometimes, code is deeply nested in the source file, but we don't
+      # want to show the leading space. In that case, the generator sets
+      # data-source-offset with how much leading space was stripped off.
+      initial_offset = 0
+      if source_offset_attr = t.attribute("data-source-offset")
+        initial_offset = source_offset_attr.to_s.to_i
+      end
+
+      full_path = t.attribute("data-file-path").to_s
+      full_path_dirs = Pathname(full_path).each_filename.to_a
+
+      # The name of an Agda module is determined from its directory
+      # structure: A/B/C.agda creates A.B.C.html. Depending on where
+      # the code is included, there might be some additional folders
+      # that precede A that we want to ignore.
+      base_path = t.attribute("data-base-path").to_s
+      base_dir_depth = 0
+      if base_path.empty?
+        # No submodules were used. Assume code/<X> is the root, since
+        # that's the code layout of the blog right now.
+        base_dir_depth = 1
+        base_path = full_path_dirs[0]
+      else
+        # The code is in a submodule. Assume that the base path / submodule
+        # root is the Agda module root, ignore all folders before that.
+        base_path_dirs = Pathname(base_path).each_filename.to_a
+        base_dir_depth = base_path_dirs.length
+      end
+
+      dirs_in_base = full_path_dirs[base_dir_depth..-1]
+      html_file = dirs_in_base.join(".").gsub(/\.agda$/, ".html")
+      html_path = File.join(["code", base_path, "html", html_file])
+
+      agda_info = @agda_context.process_agda_html_file(html_path)
+
+      # Hugo conveniently generates a bunch of spans, each encoding a line
+      # of code output. We can iterate over these and match them up with
+      # the line numbers we got from reading the Agda HTML output.
+      lines = t.css("pre.chroma code[data-lang] .line")
+      lines.zip(line_range).each do |line, line_no|
+        line_info = agda_info[line_no]
+        next unless line_info
+
+        offset = initial_offset
+        line.traverse do |lt|
+          if lt.text?
+            content = lt.content
+            new_offset = offset + content.length
+
+            # The span/a/etc. structure of the Agda and Hugo HTML files
+            # need not line up; it's possible for there to be a single link
+            # in the Agda file that's broken up across multiple HTML nodes
+            # in the Hugo output. For now, just don't link those, since inserting
+            # such overlapping links is relatively complicated. Instead,
+            # require links to fit fully within a current text node (and thus,
+            # not overlap the boundaries of any HTML).
+            matching_links = line_info.links.filter do |link|
+              link[:from] >= offset and link[:to] <= new_offset
+            end
+
+            # A given text node can be broken into any number of sub-nodes,
+            # where some sub-nodes are still text, and others have been turned
+            # into links. Store the new pieces in replace_with. E.g.,
+            #
+            # Original:
+            #   abc
+            #
+            # New:
+            #   a<a href="..">b</a>c
+            #
+            # replace_with:
+            #   ["a", <Nokogiri::XML::Node...>, "c"]
+            #
+            # match_offset represents how much of the original text we've
+            # already converted. The below iteration assumes that matching
+            # links are in order, and don't overlap.
+            replace_with = []
+            replace_offset = 0
+            matching_links.each do |match|
+              # The link's range is an offset from the beginning of the line,
+              # but the text piece we're splitting up might be partway into
+              # the line. Convert the link coordinates to piece-relative ones.
+              relative_from = match[:from] - offset
+              relative_to = match[:to] - offset
+
+              # If the previous link ended some time before the new link
+              # began (or if the current link is the first one, and is not
+              # at the beginning), ensure that the plain text "in between"
+              # is kept.
+              replace_with << content[replace_offset...relative_from]
+
+              tag = (match.include? :href) ? 'a' : 'span'
+              new_node = Nokogiri::XML::Node.new(tag, document)
+              if match.include? :href
+                # For nodes with links, note what they're referring to, so
+                # we can adjust their hrefs when we assign global IDs.
+                href = match[:href].to_s
+                new_node['href'] = note_used_href file, new_node, href
+              end
+              if match.include? :id
+                # For nodes with IDs visible in the current Hugo file, we'll
+                # want to redirect links that previously go to other Agda
+                # module HTML files. So, note the ID that we want to redirect,
+                # and pick a new unique ID to replace it with.
+                id = match[:id].to_s
+                new_node['id'] = note_defined_href file, "#{html_file}##{id}"
+              end
+              new_node.content = content[relative_from...relative_to]
+
+              replace_with << new_node
+              replace_offset = relative_to
+            end
+            replace_with << content[replace_offset..-1]
+
+            # Finally, replace the node under consideration with the new
+            # pieces.
+            replace_with.each do |replacement|
+              lt.add_previous_sibling replacement
+            end
+            lt.remove
+
+            offset = new_offset
+          end
+        end
+      end
+    end
+  end
+
+  def cross_link_files
+    # Now, we have a complete list of all the IDs visible in scope.
+    # Redirect relevant links to these IDs. This achieves within-post
+    # links.
+    @nodes_referencing_href.each do |href, references|
+      references.each do |reference|
+        file = reference[:file]
+        node = reference[:node]
+
+        local_targets = @local_seen_hrefs[file]
+        if local_targets.include? href
+          # A code block in this fine provides this href, create a local link.
+          node['href'] = "##{local_targets[href]}"
+        elsif @global_seen_hrefs.include? href
+          # A code block in this series, but not in this file, defines
+          # this href. Create a cross-file link.
+          target = @global_seen_hrefs[href]
+          other_file = target[:file]
+          id = target[:id]
+
+          relpath = Pathname.new(other_file).dirname.relative_path_from(Pathname.new(file).dirname)
+          node['href'] = "#{relpath}##{id}"
+        else
+          # No definitions in any blog page. For now, just delete the anchor.
+          node.replace node.content
+        end
+      end
+    end
+  end
+end
+
+agda_context = AgdaContext.new
+
+file_documents = {}
+series_groups = files.group_by do |file|
+  file_documents[file] = document = Nokogiri::HTML.parse(File.open(file))
+  document.css("meta[name=blog-series]")&.attribute("content")&.to_s
+end
+
+# For the 'nil' group, process individually.
+if files_with_no_series = series_groups.delete(nil)
+  files_with_no_series.each do |file|
+    file_group = FileGroup.new agda_context
+    file_group.process_source_file file, file_documents[file]
+    file_group.cross_link_files
+  end
+end
+
+# For groups, process them together to allow cross-linking
+series_groups.each do |_, files_in_series|
+  file_group = FileGroup.new agda_context
+  files_in_series.each do |file|
+    file_group.process_source_file file, file_documents[file]
+  end
+  file_group.cross_link_files
+end
+
+# Having modified all the HTML files, save them.
+file_documents.each do |file, document|
+  File.write(file, document.to_html(encoding: 'UTF-8'))
+end

analyze.rb

@@ -0,0 +1,110 @@
+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 = {}
+Dir['content/blog/**/*.md'].each do |file|
+  file = file.chomp
+  files << file
+  arr = refs[file] || (refs[file] = [])
+  pattern = Regexp.union(/< relref "([^"]+)" >/, /< draftlink "[^"]+" "([^"]+)" >/)
+  File.open(file).read.scan(pattern) do |ref|
+    ref = resolve_path(File.dirname(file), ref[0] || ref[1])
+    arr << ref
+    files << ref
+  end
+  arr.uniq!
+end
+
+data = {}
+id = 0
+series = {}
+files.each do |file|
+  id += 1
+  name = file
+  tags = []
+  group = 1
+  draft = false
+  next unless File.exist?(file)
+  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 =~ /^draft: true$/
+      draft = true
+    elsif l =~ /^series: (.+)$/
+      this_series = $~[1]
+      series_list = series.fetch(this_series) do
+        series[this_series] = []
+      end
+      series_list << file
+    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
+      elsif tags.include? "Agda"
+        group = 7
+      elsif tags.include? "Hugo"
+        group = 8
+      end
+    end
+  end
+  next if draft
+  data[file] = { :id => id, :name => 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|
+    next unless data[file1]
+    next unless data[ref]
+    edges << { :from => data[file1][:id], :to => data[ref][:id] }
+  end
+end
+series.each do |series, files|
+  files.sort.each_cons(2) do |file1, file2|
+    next unless data[file1]
+    next unless data[file2]
+    edges << { :from => data[file1][:id], :to => data[file2][:id] }
+    edges << { :from => data[file2][:id], :to => data[file1][:id] }
+  end
+end
+edges.uniq!
+# edges.filter! { |e| e[:from] < e[:to] }
+edges.map! { |e| { :from => [e[:from], e[:to]].min, :to => [e[:from], e[:to]].max } }.uniq!
+
+puts ("export const nodes = " + JSON.pretty_unparse(data.values) + ";")
+puts ("export const edges = " + JSON.pretty_unparse(edges) + ";")

assets/bergamot/rendering/imp.bergamot

@@ -0,0 +1,65 @@
+LatexListNil @ latexlist(nil, nil) <-;
+LatexListCons @ latexlist(cons(?x, ?xs), cons(?l_x, ?l_s)) <- latex(?x, ?l_x), latexlist(?xs, ?l_s);
+
+IntercalateNil @ intercalate(?sep, nil, nil) <-;
+IntercalateConsCons @ intercalate(?sep, cons(?x_1, cons(?x_2, ?xs)), cons(?x_1, cons(?sep, ?ys))) <- intercalate(?sep, cons(?x_2, ?xs), ?ys);
+IntercalateConsNil @ intercalate(?sep, cons(?x, nil), cons(?x, nil)) <-;
+
+NonEmpty @ nonempty(cons(?x, ?xs)) <-;
+
+InListHere @ inlist(?e, cons(?e, ?es)) <-;
+InListThere @ inlist(?e_1, cons(?e_2, ?es)) <- inlist(?e_1, ?es);
+
+BasicParenLit @ paren(lit(?v), ?l) <- latex(lit(?v), ?l);
+BasicParenVar @ paren(var(?x), ?l) <- latex(var(?x), ?l);
+BasicParenVar @ paren(metavariable(?x), ?l) <- latex(metavariable(?x), ?l);
+BasicParenOther @ paren(?t, ?l) <- latex(?t, ?l_t), join(["(", ?l_t, ")"], ?l);
+
+LatexInt @ latex(?i, ?l) <- int(?i), tostring(?i, ?l);
+LatexFloat @ latex(?f, ?l) <- float(?f), tostring(?f, ?l);
+LatexStr @ latex(?s, ?l) <- str(?s), escapestring(?s, ?l_1), latexifystring(?s, ?l_2), join(["\\texttt{\"", ?l_2, "\"}"], ?l);
+LatexMeta @ latex(metavariable(?l), ?l) <-;
+LatexLit @ latex(lit(?i), ?l) <- latex(?i, ?l);
+LatexVar @ latex(var(metavariable(?s)), ?l) <- latex(metavariable(?s), ?l);
+LatexVar @ latex(var(?s), ?l) <- latex(?s, ?l_v), join(["\\texttt{", ?l_v, "}"], ?l);
+LatexPlus @ latex(plus(?e_1, ?e_2), ?l) <-
+    paren(?e_1, ?l_1), paren(?e_2, ?l_2),
+    join([?l_1, " + ", ?l_2], ?l);
+LatexMinus @ latex(minus(?e_1, ?e_2), ?l) <-
+    paren(?e_1, ?l_1), paren(?e_2, ?l_2),
+    join([?l_1, " - ", ?l_2], ?l);
+
+EnvLiteralNil @ envlitrec(empty, "\\{", "", ?seen) <-;
+EnvLiteralSingle @ envlitsingle(?pre, ?e, ?v, "", ?pre, ?seen) <- inlist(?e, ?seen);
+EnvLiteralSingle @ envlitsingle(?pre, ?e, ?v, ?l, ", ", ?seen) <- latex(?e, ?l_e), latex(?v, ?l_v), join([?pre, "\\texttt{", ?l_e, "} \\mapsto", ?l_v], ?l);
+EnvLiteralCons @ envlitrec(extend(empty, ?e, ?v), ?l, ?newnext, ?seen) <- envlitrec(?rho, ?l_rho, ?next, cons(?e, ?seen)), envlitsingle(?next, ?e, ?v, ?l_v, ?newnext, ?seen), join([?l_rho, ?l_v], ?l);
+EnvLiteralCons @ envlitrec(extend(?rho, ?e, ?v), ?l, ?newnext, ?seen) <- envlitrec(?rho, ?l_rho, ?next, cons(?e, ?seen)), envlitsingle(?next, ?e, ?v, ?l_v, ?newnext, ?seen), join([?l_rho, ?l_v], ?l);
+EnvLiteralOuter @ envlit(?rho, ?l) <- envlitrec(?rho, ?l_rho, ?rest, []), join([?l_rho, "\\}"], ?l);
+
+LatexEnvLit @ latex(?rho, ?l) <- envlit(?rho, ?l);
+LatexTypeEmpty @ latex(empty, "\\{\\}") <-;
+LatexExtend @ latex(extend(?a, ?b, ?c), ?l) <- latex(?a, ?l_a), latex(?b, ?l_b), latex(?c, ?l_c), join([?l_a, "[", ?l_b, " \\mapsto ", ?l_c, "]"], ?l);
+LatexInenv @ latex(inenv(?x, ?v, ?G), ?l) <-latex(?x, ?l_x), latex(?v, ?l_v), latex(?G, ?l_G), join([?l_G, "(", ?l_x, ") = ", ?l_v], ?l);
+LatexEvalTer @ latex(eval(?G, ?e, ?t), ?l) <- latex(?G, ?l_G), latex(?e, ?l_e), latex(?t, ?l_t), join([?l_G, ",\\  ", ?l_e, " \\Downarrow ", ?l_t], ?l);
+
+LatexAdd @ latex(add(?a, ?b, ?c), ?l) <- latex(?a, ?l_a), latex(?b, ?l_b), latex(?c, ?l_c), join([?l_a, "+", ?l_b, "=", ?l_c], ?l);
+LatexSubtract @ latex(subtract(?a, ?b, ?c), ?l) <- latex(?a, ?l_a), latex(?b, ?l_b), latex(?c, ?l_c), join([?l_a, "-", ?l_b, "=", ?l_c], ?l);
+LatexEvalTer @ latex(stepbasic(?G, ?e, ?H), ?l) <- latex(?G, ?l_G), latex(?e, ?l_e), latex(?H, ?l_H), join([?l_G, ",\\  ", ?l_e, " \\Rightarrow ", ?l_H], ?l);
+LatexEvalTer @ latex(step(?G, ?e, ?H), ?l) <- latex(?G, ?l_G), latex(?e, ?l_e), latex(?H, ?l_H), join([?l_G, ",\\  ", ?l_e, " \\Rightarrow ", ?l_H], ?l);
+
+LatexNoop @ latex(noop, "\\texttt{noop}") <-;
+LatexAssign @ latex(assign(?x, ?e), ?l) <- latex(?x, ?l_x), latex(?e, ?l_e), join([?l_x, " = ", ?l_e], ?l);
+LatexAssign @ latex(if(?e, ?s_1, ?s_2), ?l) <- latex(?e, ?l_e), latex(?s_1, ?l_1), latex(?s_2, ?l_2), join(["\\textbf{if}\\ ", ?l_e, "\\ \\{\\ ", ?l_1, "\\ \\}\\ \\textbf{else}\\ \\{\\ ", ?l_2, "\\ \\}"], ?l);
+LatexAssign @ latex(while(?e, ?s), ?l) <- latex(?e, ?l_e), latex(?s, ?l_s), join(["\\textbf{while}\\ ", ?l_e, "\\ \\{\\ ", ?l_s, "\\ \\}"], ?l);
+LatexAssign @ latex(seq(?s_1, ?s_2), ?l) <- latex(?s_1, ?l_1), latex(?s_2, ?l_2), join([?l_1, "; ", ?l_2], ?l);
+
+LatexNumNeq @ latex(not(eq(?e_1, ?e_2)), ?l) <- latex(?e_1, ?l_1), latex(?e_2, ?l_2), join([?l_1, " \\neq ", ?l_2], ?l);
+LatexNot @ latex(not(?e), ?l) <- latex(?e, ?l_e), join(["\\neg (", ?l_e, ")"], ?l);
+LatexNumEq @ latex(eq(?e_1, ?e_2), ?l) <- latex(?e_1, ?l_1), latex(?e_2, ?l_2), join([?l_1, " = ", ?l_2], ?l);
+
+LatexIsInt @ latex(int(?e), ?l) <- latex(?e, ?l_e), join([?l_e, " \\in \\texttt{Int}"], ?l);
+LatexIsFloat @ latex(float(?e), ?l) <- latex(?e, ?l_e), join([?l_e, " \\in \\texttt{Float}"], ?l);
+LatexIsNum @ latex(num(?e), ?l) <- latex(?e, ?l_e), join([?l_e, " \\in \\texttt{Num}"], ?l);
+LatexIsStr @ latex(str(?e), ?l) <- latex(?e, ?l_e), join([?l_e, " \\in \\texttt{Str}"], ?l);
+LatexSym @ latex(?s, ?l) <- sym(?s), tostring(?s, ?l_1), join(["\\text{", ?l_1,"}"], ?l);
+LatexCall @ latex(?c, ?l) <- call(?c, ?n, ?ts), nonempty(?ts), latexlist(?ts, ?lts_1), intercalate(", ", ?lts_1, ?lts_2), join(?lts_2, ?lts_3), join(["\\text{", ?n, "}", "(", ?lts_3, ")"], ?l);

assets/bergamot/rendering/lc.bergamot

@@ -0,0 +1,74 @@
+PrecApp @ prec(app(?l, ?r), 100, left) <-;
+PrecPlus @ prec(plus(?l, ?r), 80, either) <-;
+PrecAbs @ prec(abs(?x, ?t, ?e), 0, right) <-;
+PrecArr @ prec(tarr(?l, ?r), 0, right) <-;
+
+SelectHead @ select(cons([?t, ?v], ?rest), ?default, ?v) <- ?t;
+SelectTail @ select(cons([?t, ?v], ?rest), ?default, ?found) <- not(?t), select(?rest, ?default, ?found);
+SelectEmpty @ select(nil, ?default, ?default) <-;
+
+Eq @ eq(?x, ?x) <-;
+
+ParenthAssocLeft @ parenthassoc(?a_i, left, right) <-;
+ParenthAssocRight @ parenthassoc(?a_i, right, left) <-;
+ParenthAssocNone @ parenthassoc(?a_i, none, ?pos) <-;
+ParenthAssocNeq @ parenthassoc(?a_i, ?a_o, ?pos) <- not(eq(?a_i, ?a_o));
+
+Parenth @ parenth(?inner, ?outer, ?pos, ?strin, ?strout) <-
+    prec(?inner, ?p_i, ?a_i), prec(?outer, ?p_o, ?a_o),
+    join(["(", ?strin, ")"], ?strinparen),
+    select([ [less(?p_i, ?p_o), strinparen], [less(?p_o, ?p_i), ?strin], [ parenthassoc(?a_i, ?a_o, ?pos), ?strinparen ] ], ?strin, ?strout);
+ParenthFallback @ parenth(?inner, ?outer, ?pos, ?strin, ?strin) <-;
+
+LatexListNil @ latexlist(nil, nil) <-;
+LatexListCons @ latexlist(cons(?x, ?xs), cons(?l_x, ?l_s)) <- latex(?x, ?l_x), latexlist(?xs, ?l_s);
+
+IntercalateNil @ intercalate(?sep, nil, nil) <-;
+IntercalateConsCons @ intercalate(?sep, cons(?x_1, cons(?x_2, ?xs)), cons(?x_1, cons(?sep, ?ys))) <- intercalate(?sep, cons(?x_2, ?xs), ?ys);
+IntercalateConsNil @ intercalate(?sep, cons(?x, nil), cons(?x, nil)) <-;
+
+NonEmpty @ nonempty(cons(?x, ?xs)) <-;
+
+LatexInt @ latex(?i, ?l) <- int(?i), tostring(?i, ?l);
+LatexFloat @ latex(?f, ?l) <- float(?f), tostring(?f, ?l);
+LatexStr @ latex(?s, ?l) <- str(?s), escapestring(?s, ?l_1), latexifystring(?s, ?l_2), join(["\\texttt{\"", ?l_2, "\"}"], ?l);
+LatexMeta @ latex(metavariable(?l), ?l) <-;
+LatexLit @ latex(lit(?i), ?l) <- latex(?i, ?l);
+LatexVar @ latex(var(?s), ?l) <- latex(?s, ?l);
+LatexPlus @ latex(plus(?e_1, ?e_2), ?l) <-
+    latex(?e_1, ?l_1), latex(?e_2, ?l_2),
+    parenth(?e_1, plus(?e_1, ?e_2), left, ?l_1, ?lp_1),
+    parenth(?e_2, plus(?e_1, ?e_2), right, ?l_2, ?lp_2),
+    join([?lp_1, " + ", ?lp_2], ?l);
+LatexPair @ latex(pair(?e_1, ?e_2), ?l) <- latex(?e_1, ?l_1), latex(?e_2, ?l_2), join(["(", ?l_1, ",  ", ?l_2, ")"], ?l);
+LatexAbs @ latex(abs(?x, ?t, ?e), ?l) <- latex(?e, ?l_e), latex(?t, ?l_t), latex(?x, ?l_x), join(["\\lambda ", ?l_x, " : ", ?l_t, " . ", ?l_e], ?l);
+LatexApp @ latex(app(?e_1, ?e_2), ?l) <-
+    latex(?e_1, ?l_1), latex(?e_2, ?l_2),
+    parenth(?e_1, app(?e_1, ?e_2), left, ?l_1, ?lp_1),
+    parenth(?e_2, app(?e_1, ?e_2), right, ?l_2, ?lp_2),
+    join([?lp_1, " \\enspace ", ?lp_2], ?l);
+
+LatexTInt @ latex(tint, "\\text{tint}") <-;
+LatexTStr @ latex(tstr, "\\text{tstr}") <-;
+LatexTArr @ latex(tarr(?t_1, ?t_2), ?l) <-
+    latex(?t_1, ?l_1), latex(?t_2, ?l_2),
+    parenth(?t_1, tarr(?t_1, ?t_2), left, ?l_1, ?lp_1),
+    parenth(?t_2, tarr(?t_1, ?t_2), right, ?l_2, ?lp_2),
+    join([?lp_1, " \\to ", ?lp_2], ?l);
+LatexTPair @ latex(tpair(?t_1, ?t_2), ?l) <- latex(?t_1, ?l_1), latex(?t_2, ?l_2), join(["(", ?l_1, ", ", ?l_2, ")"], ?l);
+
+LatexTypeEmpty @ latex(empty, "\\varnothing") <-;
+LatexTypeExtend @ latex(extend(?a, ?b, ?c), ?l) <- latex(?a, ?l_a), latex(?b, ?l_b), latex(?c, ?l_c), join([?l_a, " , ", ?l_b, " : ", ?l_c], ?l);
+LatexTypeInenv @ latex(inenv(?x, ?t, ?G), ?l) <-latex(?x, ?l_x), latex(?t, ?l_t), latex(?G, ?l_G), join([?l_x, " : ", ?l_t, " \\in ", ?l_G], ?l);
+
+LatexTypeBin @ latex(type(?e, ?t), ?l) <- latex(?e, ?l_e), latex(?t, ?l_t), join([?l_e, " : ", ?l_t], ?l);
+LatexTypeTer @ latex(type(?G, ?e, ?t), ?l) <- latex(?G, ?l_G), latex(?e, ?l_e), latex(?t, ?l_t), join([?l_G, " \\vdash ", ?l_e, " : ", ?l_t], ?l);
+
+LatexConverts @ latex(converts(?f, ?t), ?l) <- latex(?f, ?l_f), latex(?t, ?l_t), join([?l_f, " \\preceq ", ?l_t], ?l);
+
+LatexIsInt @ latex(int(?e), ?l) <- latex(?e, ?l_e), join([?l_e, " \\in \\texttt{Int}"], ?l);
+LatexIsFloat @ latex(float(?e), ?l) <- latex(?e, ?l_e), join([?l_e, " \\in \\texttt{Float}"], ?l);
+LatexIsNum @ latex(num(?e), ?l) <- latex(?e, ?l_e), join([?l_e, " \\in \\texttt{Num}"], ?l);
+LatexIsStr @ latex(str(?e), ?l) <- latex(?e, ?l_e), join([?l_e, " \\in \\texttt{Str}"], ?l);
+LatexSym @ latex(?s, ?l) <- sym(?s), tostring(?s, ?l_1), join(["\\text{", ?l_1,"}"], ?l);
+LatexCall @ latex(?c, ?l) <- call(?c, ?n, ?ts), nonempty(?ts), latexlist(?ts, ?lts_1), intercalate(", ", ?lts_1, ?lts_2), join(?lts_2, ?lts_3), join(["\\text{", ?n, "}", "(", ?lts_3, ")"], ?l);

assets/scss/bergamot.scss

@@ -0,0 +1,174 @@
+@import "variables.scss";
+@import "mixins.scss";
+
+.bergamot-exercise {
+    counter-increment: bergamot-exercise;
+
+    .bergamot-root {
+        border: none;
+        padding: 0;
+        margin-top: 1em;
+    }
+
+
+    .bergamot-exercise-label {
+        .bergamot-exercise-number::after {
+            content: "Exercise " counter(bergamot-exercise);
+            font-weight: bold;
+            text-decoration: underline;
+        }
+    }
+
+    .bergamot-button {
+        @include bordered-block;
+        padding: 0.25em;
+        padding-left: 1em;
+        padding-right: 1em;
+        background-color: inherit;
+        display: inline-flex;
+        align-items: center;
+        justify-content: center;
+        transition: 0.25s;
+        font-family: $font-body;
+        @include var(color, text-color);
+
+        &.bergamot-hidden {
+            display: none;
+        }
+
+        .feather {
+            margin-right: 0.5em;
+        }
+    }
+
+    .bergamot-play {
+        .feather { color: $primary-color; }
+        &:hover, &:focus {
+            .feather { color: lighten($primary-color, 20%); }
+        }
+    }
+
+    .bergamot-reset {
+        .feather { color: #0099CC; }
+        &:hover, &:focus {
+            .feather { color: lighten(#0099CC, 20%); }
+        }
+
+        svg {
+            fill: none;
+        }
+    }
+
+    .bergamot-close {
+        .feather { color: tomato; }
+        &:hover, &:focus {
+            .feather { color: lighten(tomato, 20%); }
+        }
+    }
+
+    .bergamot-button-group {
+        margin-top: 1em;
+    }
+}
+
+.bergamot-root {
+    @include bordered-block;
+    padding: 1em;
+
+    .bergamot-section-heading {
+        margin-bottom: 0.5em;
+        font-family: $font-body;
+        font-style: normal;
+        font-weight: bold;
+        font-size: 1.25em;
+    }
+
+    .bergamot-section {
+        margin-bottom: 1em;
+    }
+
+    textarea {
+        display: block;
+        width: 100%;
+        height: 10em;
+        resize: none;
+    }
+
+    input[type="text"] {
+        width: 100%;
+        @include textual-input;
+    }
+
+    .bergamot-rule-list {
+        display: flex;
+        flex-direction: row;
+        flex-wrap: wrap;
+        justify-content: center;
+    }
+
+    .bergamot-rule-list katex-expression {
+        margin-left: .5em;
+        margin-right: .5em;
+        flex-grow: 1;
+        flex-basis: 0;
+    }
+
+    .bergamot-rule-section {
+        .bergamot-rule-section-name {
+            text-align: center;
+            margin: 0.25em;
+            font-weight: bold;
+        }
+    }
+
+    .bergamot-proof-tree {
+        overflow: auto;
+    }
+
+    .bergamot-error {
+        @include bordered-block;
+        padding: 0.5rem;
+        border-color: tomato;
+        background-color: rgba(tomato, 0.25);
+        margin-top: 1rem;
+    }
+
+    .bergamot-selector {
+        button {
+            @include var(background-color, background-color);
+            @include var(color, text-color);
+            @include bordered-block;
+            padding: 0.5rem;
+            font-family: $font-body;
+            border-style: dotted;
+
+            &.active {
+                border-color: $primary-color;
+                border-style: solid;
+                font-weight: bold;
+            }
+
+            &:not(:first-child) {
+                border-bottom-left-radius: 0;
+                border-top-left-radius: 0;
+            }
+
+            &:not(:last-child) {
+                border-bottom-right-radius: 0;
+                border-top-right-radius: 0;
+                border-right-width: 0;
+            }
+        }
+
+        button.active + button {
+            border-left-color: $primary-color;
+            border-left-style: solid;
+        }
+
+        margin-bottom: 1rem;
+    }
+
+    .bergamot-no-proofs {
+        text-align: center;
+    }
+}

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;
+}

assets/scss/gmachine.scss

@@ -1,4 +1,5 @@
-@import "style.scss";
+@import "variables.scss";
+@import "mixins.scss";
 
 .gmachine-instruction {
     display: flex;
@@ -6,7 +7,7 @@
 }
 
 .gmachine-instruction-name {
-    padding: 10px;
+    padding: .8rem;
     border-right: $standard-border;
     flex-grow: 1;
     flex-basis: 20%;
@@ -28,12 +29,12 @@
 }
 
 .gmachine-inner-label {
-    padding: 10px;
+    padding: .8rem;
     font-weight: bold;
 }
 
 .gmachine-inner-text {
-    padding: 10px;
+    padding: .8rem;
     text-align: right;
     flex-grow: 1;
 }

assets/scss/stack.scss

@@ -0,0 +1,19 @@
+@import "variables.scss";
+@import "mixins.scss";
+
+.stack {
+    display: flex;
+    flex-direction: column;
+    max-width: 10rem;
+    margin: auto;
+    @include bordered-block;
+}
+
+.stack-element {
+    text-align: center;
+    min-height: 1.5rem;
+
+    &:not(:last-child) {
+        border-bottom: $standard-border;
+    }
+}

assets/scss/thevoid.scss

@@ -0,0 +1,430 @@
+@import "variables.scss";
+
+body {
+  background-color: #1c1e26;
+  --text-color: white;
+  font-family: $font-code;
+}
+
+h1, h2, h3, h4, h5, h6 {
+  text-align: left;
+  font-family: $font-code;
+}
+
+h1::after {
+  content: "(writing)";
+  font-size: 1rem;
+  margin-left: 0.5em;
+  position: relative;
+  bottom: -0.5em;
+  color: $primary-color;
+}
+
+nav .container {
+  justify-content: flex-start;
+
+  a {
+    padding-left: 0;
+    margin-right: 1em;
+  }
+}
+
+.header-divider {
+  visibility: hidden;
+}
+
+hr {
+  height: auto;
+  border: none;
+
+  &::after {
+    content: "* * *";
+    color: $primary-color;
+    font-size: 2rem;
+    display: block;
+    text-align: center;
+  }
+}
+
+/* Code for the CSS glitch effect. Originally from: https://codepen.io/mattgrosswork/pen/VwprebG */
+
+.glitch {
+  position: relative;
+
+  span {
+    animation: paths 5s step-end infinite;
+    font-weight: bold;
+  }
+
+  &::before, &::after {
+    content: attr(data-text);
+    position: absolute;
+    width: 110%;
+    z-index: -1;
+  }
+
+  &::before {
+    top: 10px;
+    left: 15px;
+    color: #e0287d;
+
+    animation: paths 5s step-end infinite, opacity 5s step-end infinite,
+               font 8s step-end infinite, movement 10s step-end infinite;
+  }
+
+  &::after {
+    top: 5px;
+    left: -10px;
+    color: #1bc7fb;
+
+    animation: paths 5s step-end infinite, opacity 5s step-end infinite,
+               font 7s step-end infinite, movement 8s step-end infinite;
+  }
+}
+
+@keyframes paths {
+  0% {
+    clip-path: polygon(
+      0% 43%,
+      83% 43%,
+      83% 22%,
+      23% 22%,
+      23% 24%,
+      91% 24%,
+      91% 26%,
+      18% 26%,
+      18% 83%,
+      29% 83%,
+      29% 17%,
+      41% 17%,
+      41% 39%,
+      18% 39%,
+      18% 82%,
+      54% 82%,
+      54% 88%,
+      19% 88%,
+      19% 4%,
+      39% 4%,
+      39% 14%,
+      76% 14%,
+      76% 52%,
+      23% 52%,
+      23% 35%,
+      19% 35%,
+      19% 8%,
+      36% 8%,
+      36% 31%,
+      73% 31%,
+      73% 16%,
+      1% 16%,
+      1% 56%,
+      50% 56%,
+      50% 8%
+    );
+  }
+
+  5% {
+    clip-path: polygon(
+      0% 29%,
+      44% 29%,
+      44% 83%,
+      94% 83%,
+      94% 56%,
+      11% 56%,
+      11% 64%,
+      94% 64%,
+      94% 70%,
+      88% 70%,
+      88% 32%,
+      18% 32%,
+      18% 96%,
+      10% 96%,
+      10% 62%,
+      9% 62%,
+      9% 84%,
+      68% 84%,
+      68% 50%,
+      52% 50%,
+      52% 55%,
+      35% 55%,
+      35% 87%,
+      25% 87%,
+      25% 39%,
+      15% 39%,
+      15% 88%,
+      52% 88%
+    );
+  }
+
+  30% {
+    clip-path: polygon(
+      0% 53%,
+      93% 53%,
+      93% 62%,
+      68% 62%,
+      68% 37%,
+      97% 37%,
+      97% 89%,
+      13% 89%,
+      13% 45%,
+      51% 45%,
+      51% 88%,
+      17% 88%,
+      17% 54%,
+      81% 54%,
+      81% 75%,
+      79% 75%,
+      79% 76%,
+      38% 76%,
+      38% 28%,
+      61% 28%,
+      61% 12%,
+      55% 12%,
+      55% 62%,
+      68% 62%,
+      68% 51%,
+      0% 51%,
+      0% 92%,
+      63% 92%,
+      63% 4%,
+      65% 4%
+    );
+  }
+
+  45% {
+    clip-path: polygon(
+      0% 33%,
+      2% 33%,
+      2% 69%,
+      58% 69%,
+      58% 94%,
+      55% 94%,
+      55% 25%,
+      33% 25%,
+      33% 85%,
+      16% 85%,
+      16% 19%,
+      5% 19%,
+      5% 20%,
+      79% 20%,
+      79% 96%,
+      93% 96%,
+      93% 50%,
+      5% 50%,
+      5% 74%,
+      55% 74%,
+      55% 57%,
+      96% 57%,
+      96% 59%,
+      87% 59%,
+      87% 65%,
+      82% 65%,
+      82% 39%,
+      63% 39%,
+      63% 92%,
+      4% 92%,
+      4% 36%,
+      24% 36%,
+      24% 70%,
+      1% 70%,
+      1% 43%,
+      15% 43%,
+      15% 28%,
+      23% 28%,
+      23% 71%,
+      90% 71%,
+      90% 86%,
+      97% 86%,
+      97% 1%,
+      60% 1%,
+      60% 67%,
+      71% 67%,
+      71% 91%,
+      17% 91%,
+      17% 14%,
+      39% 14%,
+      39% 30%,
+      58% 30%,
+      58% 11%,
+      52% 11%,
+      52% 83%,
+      68% 83%
+    );
+  }
+
+  76% {
+    clip-path: polygon(
+      0% 26%,
+      15% 26%,
+      15% 73%,
+      72% 73%,
+      72% 70%,
+      77% 70%,
+      77% 75%,
+      8% 75%,
+      8% 42%,
+      4% 42%,
+      4% 61%,
+      17% 61%,
+      17% 12%,
+      26% 12%,
+      26% 63%,
+      73% 63%,
+      73% 43%,
+      90% 43%,
+      90% 67%,
+      50% 67%,
+      50% 41%,
+      42% 41%,
+      42% 46%,
+      50% 46%,
+      50% 84%,
+      96% 84%,
+      96% 78%,
+      49% 78%,
+      49% 25%,
+      63% 25%,
+      63% 14%
+    );
+  }
+
+  90% {
+    clip-path: polygon(
+      0% 41%,
+      13% 41%,
+      13% 6%,
+      87% 6%,
+      87% 93%,
+      10% 93%,
+      10% 13%,
+      89% 13%,
+      89% 6%,
+      3% 6%,
+      3% 8%,
+      16% 8%,
+      16% 79%,
+      0% 79%,
+      0% 99%,
+      92% 99%,
+      92% 90%,
+      5% 90%,
+      5% 60%,
+      0% 60%,
+      0% 48%,
+      89% 48%,
+      89% 13%,
+      80% 13%,
+      80% 43%,
+      95% 43%,
+      95% 19%,
+      80% 19%,
+      80% 85%,
+      38% 85%,
+      38% 62%
+    );
+  }
+
+  1%,
+  7%,
+  33%,
+  47%,
+  78%,
+  93% {
+    clip-path: none;
+  }
+}
+
+@keyframes movement {
+  0% {
+    top: 0px;
+    left: -20px;
+  }
+
+  15% {
+    top: 10px;
+    left: 10px;
+  }
+
+  60% {
+    top: 5px;
+    left: -10px;
+  }
+
+  75% {
+    top: -5px;
+    left: 20px;
+  }
+
+  100% {
+    top: 10px;
+    left: 5px;
+  }
+}
+
+@keyframes opacity {
+  0% {
+    opacity: 0.1;
+  }
+
+  5% {
+    opacity: 0.7;
+  }
+
+  30% {
+    opacity: 0.4;
+  }
+
+  45% {
+    opacity: 0.6;
+  }
+
+  76% {
+    opacity: 0.4;
+  }
+
+  90% {
+    opacity: 0.8;
+  }
+
+  1%,
+  7%,
+  33%,
+  47%,
+  78%,
+  93% {
+    opacity: 0;
+  }
+}
+
+
+@keyframes font {
+  0% {
+    font-weight: 100;
+    color: #e0287d;
+    filter: blur(3px);
+  }
+
+  20% {
+    font-weight: 500;
+    color: #fff;
+    filter: blur(0);
+  }
+
+  50% {
+    font-weight: 300;
+    color: #1bc7fb;
+    filter: blur(2px);
+  }
+
+  60% {
+    font-weight: 700;
+    color: #fff;
+    filter: blur(0);
+  }
+
+  90% {
+    font-weight: 500;
+    color: #e0287d;
+    filter: blur(6px);
+  }
+}

build-agda-html.rb

@@ -0,0 +1,70 @@
+require "json"
+require "set"
+require "optparse"
+require "fileutils"
+
+# For target_dir, use absolute paths because when invoking Agda, we'll be
+# using chdir.
+root_path = "code"
+target_dir = File.expand_path "code"
+data_file = "data/submodules.json"
+OptionParser.new do |opts|
+  opts.banner = "Usage: build-agda-html.rb [options]"
+
+  opts.on("--root-path=PATH", "Search for Agda project folders in the given location") do |f|
+    root_path = f
+  end
+  opts.on("--target-dir=PATH", "Generate HTML files into the given directory") do |f|
+    target_dir = File.expand_path f
+  end
+  opts.on("--data-file=FILE", "Specify the submodules.json that encodes nested submodule structure") do |f|
+    data_file = f
+  end
+end.parse!
+files = ARGV
+
+code_paths = Dir.entries(root_path).select do |f|
+  File.directory?(File.join(root_path, f)) and f != '.' and f != '..'
+end.to_set
+code_paths += JSON.parse(File.read(data_file)).keys if File.exist? data_file
+# Extending code_paths from submodules.json means that nested Agda modules
+# have their root dir correctly set.
+
+max_path = ->(path) {
+  code_paths.max_by do |code_path|
+    count = 0
+    path.chars.zip(code_path.chars) do |c1, c2|
+      break unless c1 == c2
+      count += 1
+    end
+
+    next count
+  end
+}
+
+files_for_paths = {}
+Dir.glob("**/*.agda", base: root_path) do |agda_file|
+  best_path = max_path.call(agda_file)
+  files_for_path = files_for_paths.fetch(best_path) do
+    files_for_paths[best_path] = []
+  end
+
+  files_for_path << agda_file[best_path.length + File::SEPARATOR.length..-1]
+end
+
+original_wd = Dir.getwd
+files_for_paths.each do |path, files|
+  Dir.chdir(original_wd)
+  Dir.chdir(File.join(root_path, path))
+  html_dir = File.join [target_dir, path, "html"]
+  FileUtils.mkdir_p html_dir
+
+  files.each do |file|
+    command = "#{ARGV[0]} #{file} --html --html-dir=#{html_dir}"
+    puts command
+    puts `#{command}`
+
+    # Allow some programs to fail (e.g., IO.agda in SPA without --guardedness)
+    # fail unless $? == 0
+  end
+end

chatgpt-subset-feather-icon.rb

@@ -0,0 +1,49 @@
+#!/usr/bin/env ruby
+# frozen_string_literal: true
+
+require 'nokogiri'
+require 'set'
+
+# 1) Process all files passed in from the command line
+svgpath = ARGV[0]
+files = ARGV[1..]
+
+# 2) Extract used Feather icons
+used_icons = Set.new
+
+files.each do |file|
+  # Parse each HTML file
+  doc = File.open(file, "r:UTF-8") { |f| Nokogiri::HTML(f) }
+
+  # Look for <use xlink:href="/feather-sprite.svg#iconName">
+  doc.css("use").each do |use_tag|
+    href = use_tag["xlink:href"] || use_tag["href"]
+    if href && href.start_with?("/feather-sprite.svg#")
+      icon_name = href.split("#").last
+      used_icons << icon_name
+    end
+  end
+end
+
+puts "Found #{used_icons.size} unique icons: #{used_icons.to_a.join(', ')}"
+
+# 3) Load the full feather-sprite.svg as XML
+sprite_doc = File.open(svgpath, "r:UTF-8") { |f| Nokogiri::XML(f) }
+
+# 4) Create a new SVG with only the required symbols
+new_svg = Nokogiri::XML::Document.new
+svg_tag = Nokogiri::XML::Node.new("svg", new_svg)
+svg_tag["xmlns"] = "http://www.w3.org/2000/svg"
+new_svg.add_child(svg_tag)
+
+sprite_doc.css("symbol").each do |symbol_node|
+  if used_icons.include?(symbol_node["id"])
+    # Duplicate the symbol node (so it can be inserted in the new document)
+    svg_tag.add_child(symbol_node.dup)
+  end
+end
+
+# 5) Save the subset sprite
+File.open(svgpath, "w:UTF-8") do |f|
+  f.write(new_svg.to_xml)
+end

chatgpt-subset-one-go.py

@@ -0,0 +1,69 @@
+import os
+import sys
+from bs4 import BeautifulSoup
+from fontTools.subset import Subsetter, Options
+from fontTools.ttLib import TTFont
+
+FONT_EXTENSIONS = (".ttf", ".woff", ".woff2", ".otf")  # Font file types
+
+def extract_text_from_html(file_path):
+    """Extract text content from a single HTML file."""
+    with open(file_path, "r", encoding="utf-8") as f:
+        soup = BeautifulSoup(f.read(), "html.parser")
+        return soup.get_text()
+
+def get_used_characters(files):
+    """Collect unique characters from all .html files in the given directory."""
+    char_set = set()
+    for file in files:
+        text = extract_text_from_html(file)
+        char_set.update(text)
+    return "".join(sorted(char_set))
+
+def find_font_files(directory):
+    """Find all font files in the given directory, recursively."""
+    font_files = []
+    for root, _, files in os.walk(directory):
+        for file in files:
+            if file.endswith(FONT_EXTENSIONS):
+                font_files.append(os.path.join(root, file))
+    return font_files
+
+def subset_font_in_place(font_path, characters):
+    """Subsets the given font file to include only the specified characters."""
+    # Convert characters to their integer code points
+    unicode_set = {ord(c) for c in characters}
+
+    font = TTFont(font_path)
+    options = Options()
+    options.drop_tables += ["DSIG"]
+    options.drop_tables += ["LTSH", "VDMX", "hdmx", "gasp"]
+    options.unicodes = unicode_set
+    options.variations = False
+    options.drop_variations = True
+    options.layout_features = ["*"]  # keep all OT features
+    options.hinting = False
+
+    # Preserve original format if it was WOFF/WOFF2
+    if font_path.endswith(".woff2"):
+        options.flavor = "woff2"
+    elif font_path.endswith(".woff"):
+        options.flavor = "woff"
+
+    subsetter = Subsetter(options)
+    subsetter.populate(unicodes=unicode_set)
+    subsetter.subset(font)
+
+    # Overwrite the original font file
+    font.save(font_path)
+    print(f"Subsetted font in place: {font_path}")
+
+if __name__ == "__main__":
+    used_chars = get_used_characters(sys.argv[2:])
+    print(f"Extracted {len(used_chars)} unique characters from {len(sys.argv[2:])} HTML files.")
+
+    font_files = find_font_files(sys.argv[1])
+    print(f"Found {len(font_files)} font files to subset.")
+
+    for font_file in font_files:
+        subset_font_in_place(font_file, used_chars)

code/agda-issomething/example.agda

@@ -0,0 +1,87 @@
+open import Agda.Primitive using (Level; lsuc)
+open import Relation.Binary.PropositionalEquality using (_≡_)
+
+variable
+    a : Level
+    A : Set a
+
+module FirstAttempt where
+    record Semigroup (A : Set a) : Set a where
+        field
+            _∙_ : A → A → A
+
+            isAssociative : ∀ (a₁ a₂ a₃ : A) → a₁ ∙ (a₂ ∙ a₃) ≡ (a₁ ∙ a₂) ∙ a₃
+
+    record Monoid (A : Set a) : Set a where
+        field semigroup : Semigroup A
+
+        open Semigroup semigroup public
+
+        field
+            zero : A
+
+            isIdentityLeft : ∀ (a : A) → zero ∙ a ≡ a
+            isIdentityRight : ∀ (a : A) → a ∙ zero ≡ a
+
+    record ContrivedExample (A : Set a) : Set a where
+        field
+            -- first property
+            monoid : Monoid A
+
+            -- second property; Semigroup is a stand-in.
+            semigroup : Semigroup A
+
+            operationsEqual : Monoid._∙_ monoid ≡ Semigroup._∙_ semigroup
+
+module SecondAttempt where
+    record IsSemigroup {A : Set a} (_∙_ : A → A → A) : Set a where
+        field isAssociative : ∀ (a₁ a₂ a₃ : A) → a₁ ∙ (a₂ ∙ a₃) ≡ (a₁ ∙ a₂) ∙ a₃
+
+    record IsMonoid {A : Set a} (zero : A) (_∙_ : A → A → A) : Set a where
+        field
+            isSemigroup : IsSemigroup _∙_
+
+            isIdentityLeft : ∀ (a : A) → zero ∙ a ≡ a
+            isIdentityRight : ∀ (a : A) → a ∙ zero ≡ a
+
+        open IsSemigroup isSemigroup public
+
+    record IsContrivedExample {A : Set a} (zero : A) (_∙_ : A → A → A) : Set a where
+        field
+            -- first property
+            monoid : IsMonoid zero _∙_
+
+            -- second property; Semigroup is a stand-in.
+            semigroup : IsSemigroup _∙_
+
+    record Semigroup (A : Set a) : Set a where
+        field
+            _∙_ : A → A → A
+            isSemigroup : IsSemigroup _∙_
+
+    record Monoid (A : Set a) : Set a where
+        field
+            zero : A
+            _∙_ : A → A → A
+            isMonoid : IsMonoid zero _∙_
+
+module ThirdAttempt {A : Set a} (_∙_ : A → A → A) where
+    record IsSemigroup : Set a where
+        field isAssociative : ∀ (a₁ a₂ a₃ : A) → a₁ ∙ (a₂ ∙ a₃) ≡ (a₁ ∙ a₂) ∙ a₃
+
+    record IsMonoid (zero : A) : Set a where
+        field
+            isSemigroup : IsSemigroup
+
+            isIdentityLeft : ∀ (a : A) → zero ∙ a ≡ a
+            isIdentityRight : ∀ (a : A) → a ∙ zero ≡ a
+
+        open IsSemigroup isSemigroup public
+
+    record IsContrivedExample (zero : A) : Set a where
+        field
+            -- first property
+            monoid : IsMonoid zero
+
+            -- second property; Semigroup is a stand-in.
+            semigroup : IsSemigroup

code/agda-spa

@@ -0,0 +1 @@
+Subproject commit 913121488069a20cdfd40777a8777eb3744c415e

code/aoc-2020

@@ -0,0 +1 @@
+Subproject commit 7a8503c3fe1aa7e624e4d8672aa9b56d24b4ba82

code/blog-static-flake

@@ -0,0 +1 @@
+Subproject commit 67b47d9c298e7476c2ca211aac5c5fd961637b7b

code/catamorphisms/Cata.hs

@@ -0,0 +1,112 @@
+{-# LANGUAGE LambdaCase, DeriveFunctor, DeriveFoldable, MultiParamTypeClasses #-}
+import Prelude hiding (length, sum, fix)
+
+length :: [a] -> Int
+length [] = 0
+length (_:xs) = 1 + length xs
+
+lengthF :: ([a] -> Int) -> [a] -> Int
+lengthF rec [] = 0
+lengthF rec (_:xs) = 1 + rec xs
+
+lengthF' = \rec -> \case
+    [] -> 0
+    _:xs -> 1 + rec xs
+
+fix f = let x = f x in x
+
+length' = fix lengthF
+
+data MyList = MyNil | MyCons Int MyList
+data MyListF a = MyNilF | MyConsF Int a 
+
+newtype Fix f = Fix { unFix :: f (Fix f) }
+
+testList :: Fix MyListF
+testList = Fix (MyConsF 1 (Fix (MyConsF 2 (Fix (MyConsF 3 (Fix MyNilF))))))
+
+myOut :: MyList -> MyListF MyList
+myOut MyNil = MyNilF
+myOut (MyCons i xs) = MyConsF i xs
+
+myIn :: MyListF MyList -> MyList 
+myIn MyNilF = MyNil
+myIn (MyConsF i xs) = MyCons i xs
+
+instance Functor MyListF where
+    fmap f MyNilF = MyNilF
+    fmap f (MyConsF i a) = MyConsF i (f a)
+
+mySumF :: MyListF Int -> Int
+mySumF MyNilF = 0
+mySumF (MyConsF i rest) = i + rest
+
+mySum :: MyList -> Int
+mySum = mySumF . fmap mySum . myOut
+
+myCata :: (MyListF a -> a) -> MyList -> a
+myCata f = f . fmap (myCata f) . myOut
+
+myLength = myCata $ \case
+    MyNilF -> 0
+    MyConsF _ l -> 1 + l
+
+myMax = myCata $ \case
+    MyNilF -> 0
+    MyConsF x y -> max x y
+
+myMin = myCata $ \case
+    MyNilF -> 0
+    MyConsF x y -> min x y
+
+myTestList = MyCons 2 (MyCons 1 (MyCons 3 MyNil))
+
+pack :: a -> (Int -> a -> a) -> MyListF a -> a
+pack b f MyNilF = b
+pack b f (MyConsF x y) = f x y
+
+unpack :: (MyListF a -> a) -> (a, Int -> a -> a)
+unpack f = (f MyNilF, \i a -> f (MyConsF i a))
+
+class Functor f => Cata a f where
+    out :: a -> f a
+
+cata :: Cata a f => (f b -> b) -> a -> b
+cata f = f . fmap (cata f) . out
+
+instance Cata MyList MyListF where
+    out = myOut
+
+data ListF a b = Nil | Cons a b deriving Functor
+
+instance Cata [a] (ListF a) where
+    out [] = Nil
+    out (x:xs) = Cons x xs
+
+sum :: Num a => [a] -> a
+sum = cata $ \case
+    Nil -> 0
+    Cons x xs -> x + xs
+
+data BinaryTree a = Node a (BinaryTree a) (BinaryTree a) | Leaf deriving (Show, Foldable)
+data BinaryTreeF a b = NodeF a b b | LeafF deriving Functor
+
+instance Cata (BinaryTree a) (BinaryTreeF a) where
+    out (Node a l r) = NodeF a l r
+    out Leaf = LeafF
+
+invert :: BinaryTree a -> BinaryTree a
+invert = cata $ \case
+    LeafF -> Leaf
+    NodeF a l r -> Node a r l
+
+data MaybeF a b = NothingF | JustF a deriving Functor
+
+instance Cata (Maybe a) (MaybeF a) where
+    out Nothing = NothingF
+    out (Just x) = JustF x
+
+getOrDefault :: a -> Maybe a -> a
+getOrDefault d = cata $ \case
+    NothingF -> d
+    JustF a -> a

code/compiler

@@ -0,0 +1 @@
+Subproject commit 137455b0f4365ba3fd11c45ce49781cdbe829ec3

code/compiler/01/scanner.l

@@ -1,33 +0,0 @@
-%option noyywrap
-
-%{
-#include <iostream>
-%}
-
-%%
-
-[ \n]+ {}
-\+ { std::cout << "PLUS" << std::endl; }
-\* { std::cout << "TIMES" << std::endl; }
-- { std::cout << "MINUS" << std::endl; }
-\/ { std::cout << "DIVIDE" << std::endl; }
-[0-9]+ { std::cout << "NUMBER: " << yytext << std::endl; }
-defn { std::cout << "KEYWORD: defn" << std::endl; }
-data { std::cout << "KEYWORD: data" << std::endl; }
-case { std::cout << "KEYWORD: case" << std::endl; }
-of { std::cout << "KEYWORD: of" << std::endl; }
-\{ { std::cout << "OPEN CURLY" << std::endl; }
-\} { std::cout << "CLOSED CURLY" << std::endl; }
-\( { std::cout << "OPEN PARENTH" << std::endl; }
-\) { std::cout << "CLOSE PARENTH" << std::endl; }
-,  { std::cout << "COMMA" << std::endl; }
--> { std::cout << "PATTERN ARROW" << std::endl; }
-= { std::cout << "EQUAL" << std::endl; }
-[a-z][a-zA-Z]* { std::cout << "LOWERCASE IDENTIFIER: " << yytext << std::endl; }
-[A-Z][a-zA-Z]* { std::cout << "UPPERCASE IDENTIFIER: " << yytext << std::endl; }
-
-%%
-
-int main() {
-    yylex();
-}

code/compiler/02/ast.hpp

@@ -1,128 +0,0 @@
-#pragma once
-#include <memory>
-#include <vector>
-
-struct ast {
-    virtual ~ast() = default;
-};
-
-using ast_ptr = std::unique_ptr<ast>;
-
-struct pattern {
-    virtual ~pattern() = default;
-};
-
-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 constructor {
-    std::string name;
-    std::vector<std::string> types;
-
-    constructor(std::string n, std::vector<std::string> ts)
-        : name(std::move(n)), types(std::move(ts)) {}
-};
-
-using constructor_ptr = std::unique_ptr<constructor>;
-
-struct definition {
-    virtual ~definition() = default;
-};
-
-using definition_ptr = std::unique_ptr<definition>;
-
-enum binop {
-    PLUS,
-    MINUS,
-    TIMES,
-    DIVIDE
-};
-
-struct ast_int : public ast {
-    int value;
-
-    explicit ast_int(int v)
-        : value(v) {}
-};
-
-struct ast_lid : public ast {
-    std::string id;
-
-    explicit ast_lid(std::string i)
-        : id(std::move(i)) {}
-};
-
-struct ast_uid : public ast {
-    std::string id;
-
-    explicit ast_uid(std::string i)
-        : id(std::move(i)) {}
-};
-
-struct ast_binop : public ast {
-    binop op;  
-    ast_ptr left;
-    ast_ptr right;
-
-    ast_binop(binop o, ast_ptr l, ast_ptr r)
-        : op(o), left(std::move(l)), right(std::move(r)) {}
-};
-
-struct ast_app : public ast {
-    ast_ptr left;
-    ast_ptr right;
-
-    ast_app(ast_ptr l, ast_ptr r)
-        : left(std::move(l)), right(std::move(r)) {}
-};
-
-struct ast_case : public ast {
-    ast_ptr of;
-    std::vector<branch_ptr> branches;
-
-    ast_case(ast_ptr o, std::vector<branch_ptr> b)
-        : of(std::move(o)), branches(std::move(b)) {}
-};
-
-struct pattern_var : public pattern {
-    std::string var;
-
-    pattern_var(std::string v)
-        : var(std::move(v)) {}
-};
-
-struct pattern_constr : public pattern {
-    std::string constr;
-    std::vector<std::string> params;
-
-    pattern_constr(std::string c, std::vector<std::string> p)
-        : constr(std::move(c)), params(std::move(p)) {}
-};
-
-struct definition_defn : public definition {
-    std::string name;
-    std::vector<std::string> params;
-    ast_ptr body;
-
-    definition_defn(std::string n, std::vector<std::string> p, ast_ptr b)
-        : name(std::move(n)), params(std::move(p)), body(std::move(b)) {
-
-    }
-};
-
-struct definition_data : public definition {
-    std::string name;
-    std::vector<constructor_ptr> constructors;
-
-    definition_data(std::string n, std::vector<constructor_ptr> cs)
-        : name(std::move(n)), constructors(std::move(cs)) {}
-};

code/compiler/02/clean.sh

@@ -1 +0,0 @@
-rm -f parser.o parser.cpp parser.hpp stack.hh scanner.cpp scanner.o a.out

code/compiler/02/compile.sh

@@ -1,5 +0,0 @@
-bison -o parser.cpp -d parser.y
-flex -o scanner.cpp scanner.l
-g++ -c -o scanner.o scanner.cpp
-g++ -c -o parser.o parser.cpp
-g++ main.cpp parser.o scanner.o

code/compiler/02/main.cpp

@@ -1,14 +0,0 @@
-#include "ast.hpp"
-#include "parser.hpp"
-
-void yy::parser::error(const std::string& msg) {
-    std::cout << "An error occured: " << msg << std::endl;
-}
-
-extern std::vector<definition_ptr> program;
-
-int main() {
-    yy::parser parser;
-    parser.parse();
-    std::cout << program.size() << std::endl;
-}

code/compiler/02/parser.y

@@ -1,140 +0,0 @@
-%{
-#include <string>
-#include <iostream>
-#include "ast.hpp"
-#include "parser.hpp"
-
-std::vector<definition_ptr> program;
-extern yy::parser::symbol_type yylex();
-
-%}
-
-%token PLUS
-%token TIMES
-%token MINUS
-%token DIVIDE
-%token <int> INT
-%token DEFN
-%token DATA
-%token CASE
-%token OF
-%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
-
-%type <std::vector<std::string>> lowercaseParams uppercaseParams
-%type <std::vector<definition_ptr>> program definitions
-%type <std::vector<branch_ptr>> branches
-%type <std::vector<constructor_ptr>> constructors
-%type <ast_ptr> aAdd aMul case app appBase
-%type <definition_ptr> definition defn data 
-%type <branch_ptr> branch
-%type <pattern_ptr> pattern
-%type <constructor_ptr> constructor
-
-%start program
-
-%%
-
-program
-    : definitions { program = std::move($1); }
-    ;
-
-definitions
-    : definitions definition { $$ = std::move($1); $$.push_back(std::move($2)); }
-    | definition { $$ = std::vector<definition_ptr>(); $$.push_back(std::move($1)); }
-    ;
-
-definition
-    : defn { $$ = std::move($1); }
-    | data { $$ = std::move($1); }
-    ;
-
-defn
-    : DEFN LID lowercaseParams EQUAL OCURLY aAdd CCURLY
-        { $$ = definition_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)); }
-    ;
-
-uppercaseParams
-    : %empty { $$ = std::vector<std::string>(); }
-    | uppercaseParams UID { $$ = 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); }
-    ;
-
-case
-    : CASE aAdd OF OCURLY branches CCURLY 
-        { $$ = ast_ptr(new ast_case(std::move($2), std::move($5))); }
-    ;
-
-branches
-    : branches branch { $$ = std::move($1); $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 EQUAL OCURLY constructors CCURLY
-        { $$ = definition_ptr(new definition_data(std::move($2), std::move($5))); }
-    ;
-
-constructors
-    : constructors COMMA constructor { $$ = std::move($1); $$.push_back(std::move($3)); }
-    | constructor
-        { $$ = std::vector<constructor_ptr>(); $$.push_back(std::move($1)); }
-    ;
-
-constructor
-    : UID uppercaseParams
-        { $$ = constructor_ptr(new constructor(std::move($1), std::move($2))); }
-    ;
-

code/compiler/02/scanner.l

@@ -1,34 +0,0 @@
-%option noyywrap
-
-%{
-#include <iostream>
-#include "ast.hpp"
-#include "parser.hpp"
-
-#define YY_DECL yy::parser::symbol_type yylex()
-
-%}
-
-%%
-
-[ \n]+ {}
-\+ { return yy::parser::make_PLUS(); }
-\* { return yy::parser::make_TIMES(); }
-- { return yy::parser::make_MINUS(); }
-\/ { return yy::parser::make_DIVIDE(); }
-[0-9]+ { return yy::parser::make_INT(atoi(yytext)); }
-defn { return yy::parser::make_DEFN(); }
-data { return yy::parser::make_DATA(); }
-case { return yy::parser::make_CASE(); }
-of { return yy::parser::make_OF(); }
-\{ { return yy::parser::make_OCURLY(); }
-\} { return yy::parser::make_CCURLY(); }
-\( { return yy::parser::make_OPAREN(); }
-\) { return yy::parser::make_CPAREN(); }
-,  { return yy::parser::make_COMMA(); }
--> { return yy::parser::make_ARROW(); }
-= { return yy::parser::make_EQUAL(); }
-[a-z][a-zA-Z]* { return yy::parser::make_LID(std::string(yytext)); }
-[A-Z][a-zA-Z]* { return yy::parser::make_UID(std::string(yytext)); }
-
-%%

code/compiler/03/ast.cpp

@@ -1,82 +0,0 @@
-#include "ast.hpp"
-
-std::string op_name(binop op) {
-    switch(op) {
-        case PLUS: return "+";
-        case MINUS: return "-";
-        case TIMES: return "*";
-        case DIVIDE: return "/";
-    }
-    throw 0;
-}
-
-type_ptr ast_int::typecheck(type_mgr& mgr, const type_env& env) const {
-    return type_ptr(new type_base("Int"));
-}
-
-type_ptr ast_lid::typecheck(type_mgr& mgr, const type_env& env) const {
-    return env.lookup(id);
-}
-
-type_ptr ast_uid::typecheck(type_mgr& mgr, const type_env& env) const {
-    return env.lookup(id);
-}
-
-type_ptr ast_binop::typecheck(type_mgr& mgr, const type_env& env) const {
-    type_ptr ltype = left->typecheck(mgr, env);
-    type_ptr rtype = right->typecheck(mgr, env);
-    type_ptr ftype = env.lookup(op_name(op));
-    if(!ftype) throw 0;
-
-    type_ptr return_type = mgr.new_type();
-    type_ptr arrow_one = type_ptr(new type_arr(rtype, return_type));
-    type_ptr arrow_two = type_ptr(new type_arr(ltype, arrow_one));
-
-    mgr.unify(arrow_two, ftype);
-    return return_type;
-}
-
-type_ptr ast_app::typecheck(type_mgr& mgr, const type_env& env) const {
-    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);
-    return return_type;
-}
-
-type_ptr ast_case::typecheck(type_mgr& mgr, const type_env& env) const {
-    type_ptr case_type = of->typecheck(mgr, env);
-    type_ptr branch_type = mgr.new_type();
-
-    for(auto& branch : branches) {
-        type_env new_env = env.scope();
-        branch->pat->match(case_type, mgr, new_env);
-        type_ptr curr_branch_type = branch->expr->typecheck(mgr, new_env);
-        mgr.unify(branch_type, curr_branch_type);
-    }
-
-    return branch_type;
-}
-
-void pattern_var::match(type_ptr t, type_mgr& mgr, type_env& env) const {
-    env.bind(var, t);
-}
-
-void pattern_constr::match(type_ptr t, type_mgr& mgr, type_env& env) const {
-    type_ptr constructor_type = env.lookup(constr);
-    if(!constructor_type) throw 0;
-
-    for(int i = 0; i < params.size(); i++) {
-        type_arr* arr = dynamic_cast<type_arr*>(constructor_type.get());
-        if(!arr) throw 0;
-
-        env.bind(params[i], arr->left);
-        constructor_type = arr->right;
-    }
-
-    mgr.unify(t, constructor_type);
-    type_base* result_type = dynamic_cast<type_base*>(constructor_type.get());
-    if(!result_type) throw 0;
-}

code/compiler/03/ast.hpp

@@ -1,162 +0,0 @@
-#pragma once
-#include <memory>
-#include <vector>
-#include "type.hpp"
-#include "env.hpp"
-
-struct ast {
-    virtual ~ast() = default;
-
-    virtual type_ptr typecheck(type_mgr& mgr, const type_env& env) const = 0;
-};
-
-using ast_ptr = std::unique_ptr<ast>;
-
-struct pattern {
-    virtual ~pattern() = default;
-
-    virtual void match(type_ptr t, type_mgr& mgr, type_env& 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 constructor {
-    std::string name;
-    std::vector<std::string> types;
-
-    constructor(std::string n, std::vector<std::string> ts)
-        : name(std::move(n)), types(std::move(ts)) {}
-};
-
-using constructor_ptr = std::unique_ptr<constructor>;
-
-struct definition {
-    virtual ~definition() = default;
-    
-    virtual void typecheck_first(type_mgr& mgr, type_env& env) = 0;
-    virtual void typecheck_second(type_mgr& mgr, const type_env& env) const = 0;
-};
-
-using definition_ptr = std::unique_ptr<definition>;
-
-enum binop {
-    PLUS,
-    MINUS,
-    TIMES,
-    DIVIDE
-};
-
-struct ast_int : public ast {
-    int value;
-
-    explicit ast_int(int v)
-        : value(v) {}
-
-    type_ptr typecheck(type_mgr& mgr, const type_env& env) const;
-};
-
-struct ast_lid : public ast {
-    std::string id;
-
-    explicit ast_lid(std::string i)
-        : id(std::move(i)) {}
-
-    type_ptr typecheck(type_mgr& mgr, const type_env& env) const;
-};
-
-struct ast_uid : public ast {
-    std::string id;
-
-    explicit ast_uid(std::string i)
-        : id(std::move(i)) {}
-
-    type_ptr typecheck(type_mgr& mgr, const type_env& env) const;
-};
-
-struct ast_binop : public ast {
-    binop op;  
-    ast_ptr left;
-    ast_ptr right;
-
-    ast_binop(binop o, ast_ptr l, ast_ptr r)
-        : op(o), left(std::move(l)), right(std::move(r)) {}
-
-    type_ptr typecheck(type_mgr& mgr, const type_env& env) const;
-};
-
-struct ast_app : public ast {
-    ast_ptr left;
-    ast_ptr right;
-
-    ast_app(ast_ptr l, ast_ptr r)
-        : left(std::move(l)), right(std::move(r)) {}
-
-    type_ptr typecheck(type_mgr& mgr, const type_env& env) const;
-};
-
-struct ast_case : public ast {
-    ast_ptr of;
-    std::vector<branch_ptr> branches;
-
-    ast_case(ast_ptr o, std::vector<branch_ptr> b)
-        : of(std::move(o)), branches(std::move(b)) {}
-
-    type_ptr typecheck(type_mgr& mgr, const type_env& env) const;
-};
-
-struct pattern_var : public pattern {
-    std::string var;
-
-    pattern_var(std::string v)
-        : var(std::move(v)) {}
-
-    void match(type_ptr t, type_mgr& mgr, type_env& 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)
-        : constr(std::move(c)), params(std::move(p)) {}
-
-    void match(type_ptr t, type_mgr&, type_env& env) const;
-};
-
-struct definition_defn : public definition {
-    std::string name;
-    std::vector<std::string> params;
-    ast_ptr body;
-
-    type_ptr return_type;
-    std::vector<type_ptr> param_types;
-
-    definition_defn(std::string n, std::vector<std::string> p, ast_ptr b)
-        : name(std::move(n)), params(std::move(p)), body(std::move(b)) {
-
-    }
-
-    void typecheck_first(type_mgr& mgr, type_env& env);
-    void typecheck_second(type_mgr& mgr, const type_env& env) const;
-};
-
-struct definition_data : public definition {
-    std::string name;
-    std::vector<constructor_ptr> constructors;
-
-    definition_data(std::string n, std::vector<constructor_ptr> cs)
-        : name(std::move(n)), constructors(std::move(cs)) {}
-
-    void typecheck_first(type_mgr& mgr, type_env& env);
-    void typecheck_second(type_mgr& mgr, const type_env& env) const;
-};

code/compiler/03/bad1.txt

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

code/compiler/03/bad2.txt

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

code/compiler/03/clean.sh

@@ -1 +0,0 @@
-rm -f parser.o parser.cpp parser.hpp stack.hh scanner.cpp scanner.o type.o env.o ast.o definition.o a.out

code/compiler/03/compile.sh

@@ -1,9 +0,0 @@
-bison -o parser.cpp -d parser.y
-flex -o scanner.cpp scanner.l
-g++ -g -c -o scanner.o scanner.cpp
-g++ -g -c -o parser.o parser.cpp
-g++ -g -c -o type.o type.cpp
-g++ -g -c -o env.o env.cpp
-g++ -g -c -o ast.o ast.cpp
-g++ -g -c -o definition.o definition.cpp
-g++ -g main.cpp parser.o scanner.o type.o env.o ast.o definition.o

code/compiler/03/definition.cpp

@@ -1,48 +0,0 @@
-#include "ast.hpp"
-
-void definition_defn::typecheck_first(type_mgr& mgr, type_env& env) {
-    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();
-        full_type = type_ptr(new type_arr(param_type, full_type));
-        param_types.push_back(param_type);
-    }
-
-    env.bind(name, full_type);
-}
-
-void definition_defn::typecheck_second(type_mgr& mgr, const type_env& env) const {
-    type_env new_env = env.scope();
-    auto param_it = params.begin();
-    auto type_it = param_types.rbegin();
-
-    while(param_it != params.end() && type_it != param_types.rend()) {
-        new_env.bind(*param_it, *type_it);
-        param_it++;
-        type_it++;
-    }
-
-    type_ptr body_type = body->typecheck(mgr, new_env);
-    mgr.unify(return_type, body_type);
-}
-
-void definition_data::typecheck_first(type_mgr& mgr, type_env& env) {
-    type_ptr return_type = type_ptr(new type_base(name));
-
-    for(auto& constructor : constructors) {
-        type_ptr full_type = return_type;
-
-        for(auto& type_name : constructor->types) {
-            type_ptr type = type_ptr(new type_base(type_name));
-            full_type = type_ptr(new type_arr(type, full_type));
-        }
-
-        env.bind(constructor->name, full_type);
-    }
-}
-
-void definition_data::typecheck_second(type_mgr& mgr, const type_env& env) const {
-    // Nothing
-}

code/compiler/03/env.cpp

@@ -1,16 +0,0 @@
-#include "env.hpp"
-
-type_ptr type_env::lookup(const std::string& name) const {
-    auto it = names.find(name);
-    if(it != names.end()) return it->second;
-    if(parent) return parent->lookup(name);
-    return nullptr;
-}
-
-void type_env::bind(const std::string& name, type_ptr t) {
-    names[name] = t;
-}
-
-type_env type_env::scope() const {
-    return type_env(this);
-}

code/compiler/03/env.hpp

@@ -1,16 +0,0 @@
-#pragma once
-#include <map>
-#include "type.hpp"
-
-struct type_env {
-    std::map<std::string, type_ptr> names;
-    type_env const* parent = nullptr;
-
-    type_env(type_env const* p)
-        : parent(p) {}
-    type_env() : type_env(nullptr) {}
-
-    type_ptr lookup(const std::string& name) const;
-    void bind(const std::string& name, type_ptr t);
-    type_env scope() const;
-};

code/compiler/03/main.cpp

@@ -1,39 +0,0 @@
-#include "ast.hpp"
-#include "parser.hpp"
-#include "type.hpp"
-
-void yy::parser::error(const std::string& msg) {
-    std::cout << "An error occured: " << msg << std::endl;
-}
-
-extern std::vector<definition_ptr> program;
-
-void typecheck_program(const std::vector<definition_ptr>& prog) {
-    type_mgr mgr;
-    type_env env;
-
-    type_ptr int_type = type_ptr(new type_base("Int")); 
-    type_ptr binop_type = type_ptr(new type_arr(
-                int_type,
-                type_ptr(new type_arr(int_type, int_type))));
-
-    env.bind("+", binop_type);
-    env.bind("-", binop_type);
-    env.bind("*", binop_type);
-    env.bind("/", binop_type);
-
-    for(auto& def : prog) {
-        def->typecheck_first(mgr, env);
-    }
-
-    for(auto& def : prog) {
-        def->typecheck_second(mgr, env);
-    }
-}
-
-int main() {
-    yy::parser parser;
-    parser.parse();
-    typecheck_program(program);
-    std::cout << program.size() << std::endl;
-}

code/compiler/03/parser.y

@@ -1,140 +0,0 @@
-%{
-#include <string>
-#include <iostream>
-#include "ast.hpp"
-#include "parser.hpp"
-
-std::vector<definition_ptr> program;
-extern yy::parser::symbol_type yylex();
-
-%}
-
-%token PLUS
-%token TIMES
-%token MINUS
-%token DIVIDE
-%token <int> INT
-%token DEFN
-%token DATA
-%token CASE
-%token OF
-%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
-
-%type <std::vector<std::string>> lowercaseParams uppercaseParams
-%type <std::vector<definition_ptr>> program definitions
-%type <std::vector<branch_ptr>> branches
-%type <std::vector<constructor_ptr>> constructors
-%type <ast_ptr> aAdd aMul case app appBase
-%type <definition_ptr> definition defn data 
-%type <branch_ptr> branch
-%type <pattern_ptr> pattern
-%type <constructor_ptr> constructor
-
-%start program
-
-%%
-
-program
-    : definitions { program = std::move($1); }
-    ;
-
-definitions
-    : definitions definition { $$ = std::move($1); $$.push_back(std::move($2)); }
-    | definition { $$ = std::vector<definition_ptr>(); $$.push_back(std::move($1)); }
-    ;
-
-definition
-    : defn { $$ = std::move($1); }
-    | data { $$ = std::move($1); }
-    ;
-
-defn
-    : DEFN LID lowercaseParams EQUAL OCURLY aAdd CCURLY
-        { $$ = definition_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)); }
-    ;
-
-uppercaseParams
-    : %empty { $$ = std::vector<std::string>(); }
-    | uppercaseParams UID { $$ = 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); }
-    ;
-
-case
-    : CASE aAdd OF OCURLY branches CCURLY 
-        { $$ = ast_ptr(new ast_case(std::move($2), std::move($5))); }
-    ;
-
-branches
-    : branches branch { $$ = std::move($1); $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 EQUAL OCURLY constructors CCURLY
-        { $$ = definition_ptr(new definition_data(std::move($2), std::move($5))); }
-    ;
-
-constructors
-    : constructors COMMA constructor { $$ = std::move($1); $$.push_back(std::move($3)); }
-    | constructor
-        { $$ = std::vector<constructor_ptr>(); $$.push_back(std::move($1)); }
-    ;
-
-constructor
-    : UID uppercaseParams
-        { $$ = constructor_ptr(new constructor(std::move($1), std::move($2))); }
-    ;
-

code/compiler/03/scanner.l

@@ -1,34 +0,0 @@
-%option noyywrap
-
-%{
-#include <iostream>
-#include "ast.hpp"
-#include "parser.hpp"
-
-#define YY_DECL yy::parser::symbol_type yylex()
-
-%}
-
-%%
-
-[ \n]+ {}
-\+ { return yy::parser::make_PLUS(); }
-\* { return yy::parser::make_TIMES(); }
-- { return yy::parser::make_MINUS(); }
-\/ { return yy::parser::make_DIVIDE(); }
-[0-9]+ { return yy::parser::make_INT(atoi(yytext)); }
-defn { return yy::parser::make_DEFN(); }
-data { return yy::parser::make_DATA(); }
-case { return yy::parser::make_CASE(); }
-of { return yy::parser::make_OF(); }
-\{ { return yy::parser::make_OCURLY(); }
-\} { return yy::parser::make_CCURLY(); }
-\( { return yy::parser::make_OPAREN(); }
-\) { return yy::parser::make_CPAREN(); }
-,  { return yy::parser::make_COMMA(); }
--> { return yy::parser::make_ARROW(); }
-= { return yy::parser::make_EQUAL(); }
-[a-z][a-zA-Z]* { return yy::parser::make_LID(std::string(yytext)); }
-[A-Z][a-zA-Z]* { return yy::parser::make_UID(std::string(yytext)); }
-
-%%

code/compiler/03/type.cpp

@@ -1,78 +0,0 @@
-#include "type.hpp"
-#include <sstream>
-#include <algorithm>
-
-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::resolve(type_ptr t, type_var*& var) {
-    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) {
-    type_var* lvar;
-    type_var* rvar;
-    type_arr* larr;
-    type_arr* rarr;
-    type_base* lid;
-    type_base* rid;
-
-    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);
-        unify(larr->right, rarr->right);
-        return;
-    } else if((lid = dynamic_cast<type_base*>(l.get())) &&
-            (rid = dynamic_cast<type_base*>(r.get()))) {
-        if(lid->name == rid->name) return;
-    }
-
-    throw 0;
-}
-
-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;
-}

code/compiler/03/type.hpp

@@ -1,44 +0,0 @@
-#pragma once
-#include <memory>
-#include <map>
-
-struct type {
-    virtual ~type() = default;
-};
-
-using type_ptr = std::shared_ptr<type>;
-
-struct type_var : public type {
-    std::string name;
-
-    type_var(std::string n)
-        : name(std::move(n)) {}
-};
-
-struct type_base : public type {
-    std::string name;
-
-    type_base(std::string n) 
-        : name(std::move(n)) {}
-};
-
-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)) {}
-};
-
-struct type_mgr {
-    int last_id = 0;
-    std::map<std::string, type_ptr> types;
-
-    std::string new_type_name();
-    type_ptr new_type();
-    type_ptr new_arrow_type();
-
-    void unify(type_ptr l, type_ptr r);
-    type_ptr resolve(type_ptr t, type_var*& var);
-    void bind(const std::string& s, type_ptr t);
-};

code/compiler/03/works1.txt

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

code/compiler/03/works2.txt

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

code/compiler/03/works3.txt

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

code/compiler/04/CMakeLists.txt

@@ -1,25 +0,0 @@
-cmake_minimum_required(VERSION 3.1)
-project(compiler)
-
-find_package(BISON)
-find_package(FLEX)
-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)
-
-add_executable(compiler
-    ast.cpp ast.hpp definition.cpp
-    env.cpp env.hpp
-    type.cpp type.hpp
-    error.cpp error.hpp
-    ${BISON_parser_OUTPUTS}
-    ${FLEX_scanner_OUTPUTS}
-    main.cpp
-)
-target_include_directories(compiler PUBLIC ${CMAKE_CURRENT_SOURCE_DIR})
-target_include_directories(compiler PUBLIC ${CMAKE_CURRENT_BINARY_DIR})

code/compiler/04/ast.cpp

@@ -1,145 +0,0 @@
-#include "ast.hpp"
-#include <ostream>
-#include "error.hpp"
-
-std::string op_name(binop op) {
-    switch(op) {
-        case PLUS: return "+";
-        case MINUS: return "-";
-        case TIMES: return "*";
-        case DIVIDE: return "/";
-    }
-    return "??";
-}
-
-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;
-}
-
-type_ptr ast_int::typecheck(type_mgr& mgr, const type_env& env) const {
-    return type_ptr(new type_base("Int"));
-}
-
-void ast_lid::print(int indent, std::ostream& to) const {
-    print_indent(indent, to);
-    to << "LID: " << id << std::endl;
-}
-
-type_ptr ast_lid::typecheck(type_mgr& mgr, const type_env& env) const {
-    return env.lookup(id);
-}
-
-void ast_uid::print(int indent, std::ostream& to) const {
-    print_indent(indent, to);
-    to << "UID: " << id << std::endl;
-}
-
-type_ptr ast_uid::typecheck(type_mgr& mgr, const type_env& env) const {
-    return env.lookup(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);
-}
-
-type_ptr ast_binop::typecheck(type_mgr& mgr, const type_env& env) const {
-    type_ptr ltype = left->typecheck(mgr, env);
-    type_ptr rtype = right->typecheck(mgr, env);
-    type_ptr ftype = env.lookup(op_name(op));
-    if(!ftype) throw type_error(std::string("unknown binary operator ") + op_name(op));
-
-    type_ptr return_type = mgr.new_type();
-    type_ptr arrow_one = type_ptr(new type_arr(rtype, return_type));
-    type_ptr arrow_two = type_ptr(new type_arr(ltype, arrow_one));
-
-    mgr.unify(arrow_two, ftype);
-    return return_type;
-}
-
-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);
-}
-
-type_ptr ast_app::typecheck(type_mgr& mgr, const type_env& env) const {
-    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);
-    return return_type;
-}
-
-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);
-    }
-}
-
-type_ptr ast_case::typecheck(type_mgr& mgr, const type_env& env) const {
-    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 new_env = env.scope();
-        branch->pat->match(case_type, mgr, new_env);
-        type_ptr curr_branch_type = branch->expr->typecheck(mgr, new_env);
-        mgr.unify(branch_type, curr_branch_type);
-    }
-
-    case_type = mgr.resolve(case_type, var);
-    if(!dynamic_cast<type_base*>(case_type.get())) {
-        throw type_error("attempting case analysis of non-data type");
-    }
-
-    return branch_type;
-}
-
-void pattern_var::print(std::ostream& to) const {
-    to << var;
-}
-
-void pattern_var::match(type_ptr t, type_mgr& mgr, type_env& 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::match(type_ptr t, type_mgr& mgr, type_env& env) const {
-    type_ptr constructor_type = env.lookup(constr);
-    if(!constructor_type) {
-        throw type_error(std::string("pattern using unknown constructor ") + constr);
-    }
-
-    for(int i = 0; i < params.size(); i++) {
-        type_arr* arr = dynamic_cast<type_arr*>(constructor_type.get());
-        if(!arr) throw type_error("too many parameters in constructor pattern");
-
-        env.bind(params[i], arr->left);
-        constructor_type = arr->right;
-    }
-
-    mgr.unify(t, constructor_type);
-}

code/compiler/04/ast.hpp

@@ -1,172 +0,0 @@
-#pragma once
-#include <memory>
-#include <vector>
-#include "type.hpp"
-#include "env.hpp"
-
-struct ast {
-    virtual ~ast() = default;
-
-    virtual void print(int indent, std::ostream& to) const = 0;
-    virtual type_ptr typecheck(type_mgr& mgr, const type_env& env) const = 0;
-};
-
-using ast_ptr = std::unique_ptr<ast>;
-
-struct pattern {
-    virtual ~pattern() = default;
-
-    virtual void print(std::ostream& to) const = 0;
-    virtual void match(type_ptr t, type_mgr& mgr, type_env& 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 constructor {
-    std::string name;
-    std::vector<std::string> types;
-
-    constructor(std::string n, std::vector<std::string> ts)
-        : name(std::move(n)), types(std::move(ts)) {}
-};
-
-using constructor_ptr = std::unique_ptr<constructor>;
-
-struct definition {
-    virtual ~definition() = default;
-    
-    virtual void typecheck_first(type_mgr& mgr, type_env& env) = 0;
-    virtual void typecheck_second(type_mgr& mgr, const type_env& env) const = 0;
-};
-
-using definition_ptr = std::unique_ptr<definition>;
-
-enum binop {
-    PLUS,
-    MINUS,
-    TIMES,
-    DIVIDE
-};
-
-struct ast_int : public ast {
-    int value;
-
-    explicit ast_int(int v)
-        : value(v) {}
-
-    void print(int indent, std::ostream& to) const;
-    type_ptr typecheck(type_mgr& mgr, const type_env& env) const;
-};
-
-struct ast_lid : public ast {
-    std::string id;
-
-    explicit ast_lid(std::string i)
-        : id(std::move(i)) {}
-
-    void print(int indent, std::ostream& to) const;
-    type_ptr typecheck(type_mgr& mgr, const type_env& env) const;
-};
-
-struct ast_uid : public ast {
-    std::string id;
-
-    explicit ast_uid(std::string i)
-        : id(std::move(i)) {}
-
-    void print(int indent, std::ostream& to) const;
-    type_ptr typecheck(type_mgr& mgr, const type_env& env) const;
-};
-
-struct ast_binop : public ast {
-    binop op;  
-    ast_ptr left;
-    ast_ptr right;
-
-    ast_binop(binop o, ast_ptr l, ast_ptr r)
-        : op(o), left(std::move(l)), right(std::move(r)) {}
-
-    void print(int indent, std::ostream& to) const;
-    type_ptr typecheck(type_mgr& mgr, const type_env& env) const;
-};
-
-struct ast_app : public ast {
-    ast_ptr left;
-    ast_ptr right;
-
-    ast_app(ast_ptr l, ast_ptr r)
-        : left(std::move(l)), right(std::move(r)) {}
-
-    void print(int indent, std::ostream& to) const;
-    type_ptr typecheck(type_mgr& mgr, const type_env& env) const;
-};
-
-struct ast_case : public ast {
-    ast_ptr of;
-    std::vector<branch_ptr> branches;
-
-    ast_case(ast_ptr o, std::vector<branch_ptr> b)
-        : of(std::move(o)), branches(std::move(b)) {}
-
-    void print(int indent, std::ostream& to) const;
-    type_ptr typecheck(type_mgr& mgr, const type_env& env) const;
-};
-
-struct pattern_var : public pattern {
-    std::string var;
-
-    pattern_var(std::string v)
-        : var(std::move(v)) {}
-
-    void print(std::ostream &to) const;
-    void match(type_ptr t, type_mgr& mgr, type_env& 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)
-        : constr(std::move(c)), params(std::move(p)) {}
-
-    void print(std::ostream &to) const;
-    void match(type_ptr t, type_mgr&, type_env& env) const;
-};
-
-struct definition_defn : public definition {
-    std::string name;
-    std::vector<std::string> params;
-    ast_ptr body;
-
-    type_ptr return_type;
-    std::vector<type_ptr> param_types;
-
-    definition_defn(std::string n, std::vector<std::string> p, ast_ptr b)
-        : name(std::move(n)), params(std::move(p)), body(std::move(b)) {
-
-    }
-
-    void typecheck_first(type_mgr& mgr, type_env& env);
-    void typecheck_second(type_mgr& mgr, const type_env& env) const;
-};
-
-struct definition_data : public definition {
-    std::string name;
-    std::vector<constructor_ptr> constructors;
-
-    definition_data(std::string n, std::vector<constructor_ptr> cs)
-        : name(std::move(n)), constructors(std::move(cs)) {}
-
-    void typecheck_first(type_mgr& mgr, type_env& env);
-    void typecheck_second(type_mgr& mgr, const type_env& env) const;
-};

code/compiler/04/definition.cpp

@@ -1,48 +0,0 @@
-#include "ast.hpp"
-
-void definition_defn::typecheck_first(type_mgr& mgr, type_env& env) {
-    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();
-        full_type = type_ptr(new type_arr(param_type, full_type));
-        param_types.push_back(param_type);
-    }
-
-    env.bind(name, full_type);
-}
-
-void definition_defn::typecheck_second(type_mgr& mgr, const type_env& env) const {
-    type_env new_env = env.scope();
-    auto param_it = params.begin();
-    auto type_it = param_types.rbegin();
-
-    while(param_it != params.end() && type_it != param_types.rend()) {
-        new_env.bind(*param_it, *type_it);
-        param_it++;
-        type_it++;
-    }
-
-    type_ptr body_type = body->typecheck(mgr, new_env);
-    mgr.unify(return_type, body_type);
-}
-
-void definition_data::typecheck_first(type_mgr& mgr, type_env& env) {
-    type_ptr return_type = type_ptr(new type_base(name));
-
-    for(auto& constructor : constructors) {
-        type_ptr full_type = return_type;
-
-        for(auto it = constructor->types.rbegin(); it != constructor->types.rend(); it++) {
-            type_ptr type = type_ptr(new type_base(*it));
-            full_type = type_ptr(new type_arr(type, full_type));
-        }
-
-        env.bind(constructor->name, full_type);
-    }
-}
-
-void definition_data::typecheck_second(type_mgr& mgr, const type_env& env) const {
-    // Nothing
-}

code/compiler/04/env.cpp

@@ -1,16 +0,0 @@
-#include "env.hpp"
-
-type_ptr type_env::lookup(const std::string& name) const {
-    auto it = names.find(name);
-    if(it != names.end()) return it->second;
-    if(parent) return parent->lookup(name);
-    return nullptr;
-}
-
-void type_env::bind(const std::string& name, type_ptr t) {
-    names[name] = t;
-}
-
-type_env type_env::scope() const {
-    return type_env(this);
-}

code/compiler/04/env.hpp

@@ -1,16 +0,0 @@
-#pragma once
-#include <map>
-#include "type.hpp"
-
-struct type_env {
-    std::map<std::string, type_ptr> names;
-    type_env const* parent = nullptr;
-
-    type_env(type_env const* p)
-        : parent(p) {}
-    type_env() : type_env(nullptr) {}
-
-    type_ptr lookup(const std::string& name) const;
-    void bind(const std::string& name, type_ptr t);
-    type_env scope() const;
-};

code/compiler/04/error.cpp

@@ -1,5 +0,0 @@
-#include "error.hpp"
-
-const char* type_error::what() const noexcept {
-    return "an error occured while checking the types of the program";
-}

code/compiler/04/error.hpp

@@ -1,21 +0,0 @@
-#pragma once
-#include <exception>
-#include "type.hpp"
-
-struct type_error : std::exception {
-    std::string description;
-
-    type_error(std::string d)
-        : description(std::move(d)) {}
-
-    const char* what() const noexcept override;
-};
-
-struct unification_error : public type_error {
-    type_ptr left;
-    type_ptr right;
-
-    unification_error(type_ptr l, type_ptr r)
-        : left(std::move(l)), right(std::move(r)), 
-            type_error("failed to unify types") {}
-};

code/compiler/04/examples/bad1.txt

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

code/compiler/04/examples/bad2.txt

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

code/compiler/04/examples/works1.txt

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

code/compiler/04/examples/works2.txt

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

code/compiler/04/examples/works3.txt

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

code/compiler/04/main.cpp

@@ -1,70 +0,0 @@
-#include "ast.hpp"
-#include <iostream>
-#include "parser.hpp"
-#include "error.hpp"
-#include "type.hpp"
-
-void yy::parser::error(const std::string& msg) {
-    std::cout << "An error occured: " << msg << std::endl;
-}
-
-extern std::vector<definition_ptr> program;
-
-void typecheck_program(
-        const std::vector<definition_ptr>& prog,
-        type_mgr& mgr, type_env& env) {
-    type_ptr int_type = type_ptr(new type_base("Int")); 
-    type_ptr binop_type = type_ptr(new type_arr(
-                int_type,
-                type_ptr(new type_arr(int_type, int_type))));
-
-    env.bind("+", binop_type);
-    env.bind("-", binop_type);
-    env.bind("*", binop_type);
-    env.bind("/", binop_type);
-
-    for(auto& def : prog) {
-        def->typecheck_first(mgr, env);
-    }
-
-    for(auto& def : prog) {
-        def->typecheck_second(mgr, env);
-    }
-
-    for(auto& pair : env.names) {
-        std::cout << pair.first << ": ";
-        pair.second->print(mgr, std::cout);
-        std::cout << std::endl;
-    }
-}
-
-int main() {
-    yy::parser parser;
-    type_mgr mgr;
-    type_env env;
-
-    parser.parse();
-    for(auto& definition : program) {
-        definition_defn* def = dynamic_cast<definition_defn*>(definition.get());
-        if(!def) continue;
-
-        std::cout << def->name;
-        for(auto& param : def->params) std::cout << " " << param;
-        std::cout << ":" << std::endl;
-
-        def->body->print(1, std::cout);
-    }
-    try {
-        typecheck_program(program, mgr, env);
-    } catch(unification_error& err) {
-        std::cout << "failed to unify types: " << std::endl;
-        std::cout << "  (1) \033[34m";
-        err.left->print(mgr, std::cout);
-        std::cout << "\033[0m" << std::endl;
-        std::cout << "  (2) \033[32m";
-        err.right->print(mgr, std::cout);
-        std::cout << "\033[0m" << std::endl;
-    } catch(type_error& err) {
-        std::cout << "failed to type check program: " << err.description << std::endl;
-    }
-}

code/compiler/04/parser.y

@@ -1,140 +0,0 @@
-%{
-#include <string>
-#include <iostream>
-#include "ast.hpp"
-#include "parser.hpp"
-
-std::vector<definition_ptr> program;
-extern yy::parser::symbol_type yylex();
-
-%}
-
-%token PLUS
-%token TIMES
-%token MINUS
-%token DIVIDE
-%token <int> INT
-%token DEFN
-%token DATA
-%token CASE
-%token OF
-%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
-
-%type <std::vector<std::string>> lowercaseParams uppercaseParams
-%type <std::vector<definition_ptr>> program definitions
-%type <std::vector<branch_ptr>> branches
-%type <std::vector<constructor_ptr>> constructors
-%type <ast_ptr> aAdd aMul case app appBase
-%type <definition_ptr> definition defn data 
-%type <branch_ptr> branch
-%type <pattern_ptr> pattern
-%type <constructor_ptr> constructor
-
-%start program
-
-%%
-
-program
-    : definitions { program = std::move($1); }
-    ;
-
-definitions
-    : definitions definition { $$ = std::move($1); $$.push_back(std::move($2)); }
-    | definition { $$ = std::vector<definition_ptr>(); $$.push_back(std::move($1)); }
-    ;
-
-definition
-    : defn { $$ = std::move($1); }
-    | data { $$ = std::move($1); }
-    ;
-
-defn
-    : DEFN LID lowercaseParams EQUAL OCURLY aAdd CCURLY
-        { $$ = definition_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)); }
-    ;
-
-uppercaseParams
-    : %empty { $$ = std::vector<std::string>(); }
-    | uppercaseParams UID { $$ = 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); }
-    ;
-
-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 EQUAL OCURLY constructors CCURLY
-        { $$ = definition_ptr(new definition_data(std::move($2), std::move($5))); }
-    ;
-
-constructors
-    : constructors COMMA constructor { $$ = std::move($1); $$.push_back(std::move($3)); }
-    | constructor
-        { $$ = std::vector<constructor_ptr>(); $$.push_back(std::move($1)); }
-    ;
-
-constructor
-    : UID uppercaseParams
-        { $$ = constructor_ptr(new constructor(std::move($1), std::move($2))); }
-    ;
-

code/compiler/04/scanner.l

@@ -1,34 +0,0 @@
-%option noyywrap
-
-%{
-#include <iostream>
-#include "ast.hpp"
-#include "parser.hpp"
-
-#define YY_DECL yy::parser::symbol_type yylex()
-
-%}
-
-%%
-
-[ \n]+ {}
-\+ { return yy::parser::make_PLUS(); }
-\* { return yy::parser::make_TIMES(); }
-- { return yy::parser::make_MINUS(); }
-\/ { return yy::parser::make_DIVIDE(); }
-[0-9]+ { return yy::parser::make_INT(atoi(yytext)); }
-defn { return yy::parser::make_DEFN(); }
-data { return yy::parser::make_DATA(); }
-case { return yy::parser::make_CASE(); }
-of { return yy::parser::make_OF(); }
-\{ { return yy::parser::make_OCURLY(); }
-\} { return yy::parser::make_CCURLY(); }
-\( { return yy::parser::make_OPAREN(); }
-\) { return yy::parser::make_CPAREN(); }
-,  { return yy::parser::make_COMMA(); }
--> { return yy::parser::make_ARROW(); }
-= { return yy::parser::make_EQUAL(); }
-[a-z][a-zA-Z]* { return yy::parser::make_LID(std::string(yytext)); }
-[A-Z][a-zA-Z]* { return yy::parser::make_UID(std::string(yytext)); }
-
-%%

code/compiler/04/type.cpp

@@ -1,99 +0,0 @@
-#include "type.hpp"
-#include <sstream>
-#include <algorithm>
-#include "error.hpp"
-
-void type_var::print(const type_mgr& mgr, std::ostream& to) const {
-    auto it = mgr.types.find(name);
-    if(it != mgr.types.end()) {
-        it->second->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 {
-    left->print(mgr, to);
-    to << " -> (";
-    right->print(mgr, to);
-    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::resolve(type_ptr t, type_var*& var) {
-    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) {
-    type_var* lvar;
-    type_var* rvar;
-    type_arr* larr;
-    type_arr* rarr;
-    type_base* lid;
-    type_base* rid;
-
-    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);
-        unify(larr->right, rarr->right);
-        return;
-    } else if((lid = dynamic_cast<type_base*>(l.get())) &&
-            (rid = dynamic_cast<type_base*>(r.get()))) {
-        if(lid->name == rid->name) return;
-    }
-
-    throw unification_error(l, r);
-}
-
-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;
-}

code/compiler/04/type.hpp

@@ -1,54 +0,0 @@
-#pragma once
-#include <memory>
-#include <map>
-
-struct 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_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;
-
-    type_base(std::string n) 
-        : name(std::move(n)) {}
-
-    void print(const type_mgr& mgr, std::ostream& to) const;
-};
-
-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;
-};