3 Commits

524 changed files with 24360 additions and 12792 deletions

6
.gitmodules vendored
View File

@@ -10,9 +10,3 @@
[submodule "code/blog-static-flake"] [submodule "code/blog-static-flake"]
path = code/blog-static-flake path = code/blog-static-flake
url = https://dev.danilafe.com/Nix-Configs/blog-static-flake.git 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

View File

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

View File

@@ -1,21 +0,0 @@
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

361
agda.rb
View File

@@ -1,361 +0,0 @@
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.
if at.parent.name != "pre"
# Costmetic highlight warnings are sometimes applied to newlines.
# If they don't have content, treat them as normal newlines at the
# top level.
#
# This is an <a class="CosmeticProblem">\n</a> node.
unless at.parent.name == "a" and at.parent['class'] == "CosmeticProblem" and at.content.strip.empty?
raise "unsupported Agda HTML output in file #{file} at line #{line} (content #{at.content.inspect})"
end
end
# 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

View File

@@ -25,9 +25,8 @@ Dir['content/blog/**/*.md'].each do |file|
file = file.chomp file = file.chomp
files << file files << file
arr = refs[file] || (refs[file] = []) arr = refs[file] || (refs[file] = [])
pattern = Regexp.union(/< relref "([^"]+)" >/, /< draftlink "[^"]+" "([^"]+)" >/) File.open(file).read.scan(/< relref "([^"]+)" >/) do |ref|
File.open(file).read.scan(pattern) do |ref| ref = resolve_path(File.dirname(file), ref[0])
ref = resolve_path(File.dirname(file), ref[0] || ref[1])
arr << ref arr << ref
files << ref files << ref
end end
@@ -36,14 +35,13 @@ end
data = {} data = {}
id = 0 id = 0
series = {}
files.each do |file| files.each do |file|
id += 1 id += 1
name = file name = file
tags = [] tags = []
group = 1 group = 1
draft = false draft = false
next unless File.exist?(file) next unless File.exists?(file)
value = File.size(file) value = File.size(file)
url = file.gsub(/^content/, "https://danilafe.com").delete_suffix("/index.md").delete_suffix(".md") url = file.gsub(/^content/, "https://danilafe.com").delete_suffix("/index.md").delete_suffix(".md")
File.readlines(file).each do |l| File.readlines(file).each do |l|
@@ -51,12 +49,6 @@ files.each do |file|
name = $~[1].delete_prefix('"').delete_suffix('"') name = $~[1].delete_prefix('"').delete_suffix('"')
elsif l =~ /^draft: true$/ elsif l =~ /^draft: true$/
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: (.+)$/ elsif l =~ /^tags: (.+)$/
tags = $~[1].delete_prefix("[").delete_suffix("]").split(/,\s?/).map { |it| it.gsub('"', '') } tags = $~[1].delete_prefix("[").delete_suffix("]").split(/,\s?/).map { |it| it.gsub('"', '') }
if tags.include? "Compilers" if tags.include? "Compilers"
@@ -69,10 +61,6 @@ files.each do |file|
group = 5 group = 5
elsif tags.include? "Crystal" elsif tags.include? "Crystal"
group = 6 group = 6
elsif tags.include? "Agda"
group = 7
elsif tags.include? "Hugo"
group = 8
end end
end end
end end
@@ -94,17 +82,8 @@ files.each do |file1|
edges << { :from => data[file1][:id], :to => data[ref][:id] } edges << { :from => data[file1][:id], :to => data[ref][:id] }
end end
end end
series.each do |series, files| edges.uniq
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.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 nodes = " + JSON.pretty_unparse(data.values) + ";")
puts ("export const edges = " + JSON.pretty_unparse(edges) + ";") puts ("export const edges = " + JSON.pretty_unparse(edges) + ";")

View File

@@ -1,65 +0,0 @@
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);

View File

@@ -1,74 +0,0 @@
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);

View File

@@ -1,174 +0,0 @@
@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;
}
}

View File

@@ -1,19 +0,0 @@
@import "variables.scss";
@import "mixins.scss";
.spiderweb {
position: fixed;
top: 0;
right: 0;
opacity: 0.25;
max-width: 900px;
@include below-container-width {
width: $container-width-threshold;
}
}
code {
background: none;
border: none;
}

View File

@@ -1,382 +0,0 @@
/* 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);
}
}

View File

@@ -1,47 +0,0 @@
@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;
}
}

View File

@@ -1,718 +0,0 @@
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!-- Created with Inkscape (http://www.inkscape.org/) -->
<svg
width="197.21727mm"
height="106.16592mm"
viewBox="0 0 197.21727 106.16592"
version="1.1"
id="svg1"
xml:space="preserve"
inkscape:version="1.4.2 (ebf0e940, 2025-05-08)"
sodipodi:docname="spiderweb.svg"
xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape"
xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd"
xmlns="http://www.w3.org/2000/svg"
xmlns:svg="http://www.w3.org/2000/svg"><sodipodi:namedview
id="namedview1"
pagecolor="#000000"
bordercolor="#000000"
borderopacity="0.25"
inkscape:showpageshadow="2"
inkscape:pageopacity="0.0"
inkscape:pagecheckerboard="0"
inkscape:deskcolor="#d1d1d1"
inkscape:document-units="mm"
inkscape:zoom="1.2119635"
inkscape:cx="292.91312"
inkscape:cy="235.56816"
inkscape:window-width="1728"
inkscape:window-height="996"
inkscape:window-x="0"
inkscape:window-y="38"
inkscape:window-maximized="1"
inkscape:current-layer="mainlayer" /><defs
id="defs1" /><g
inkscape:groupmode="layer"
id="mainlayer"
inkscape:label="Main Layer"
transform="translate(-12.908849,0.44133637)"><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 107.50107,0.48134806 -4.01124,4.49258204 c 0,0 5.61573,31.9294199 14.28,37.0637999 8.66426,5.134379 7.54112,5.294828 7.54112,5.294828"
id="path2"
sodipodi:nodetypes="ccsc" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="M 173.22006,0.15397339 85.91715,39.263214"
id="path3" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 183.22833,-0.15397339 c 0,0 -49.11751,32.33441039 -64.66882,56.50823339"
id="path4" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 185.53793,-0.30794677 c 0,0 -48.80956,45.57612277 -56.50823,61.43538277"
id="path5" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 184.76806,4.1572814 c 0,0 -42.1887,53.8906846 -31.41057,70.2118646"
id="path6" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 190.46508,0 c 0,0 -31.10262,53.428764 -18.93873,84.99331"
id="path7" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 191.85084,-0.15397339 c 0,0 -17.55297,60.81948839 -3.23344,92.69197939"
id="path8" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 193.54455,-0.15397339 c 0,0 -6.62086,54.50657839 16.32117,86.53304339"
id="path9" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 196.31607,-0.30794677 c 0,0 6.00496,36.33771977 13.54965,48.19366877"
id="path10" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="M 197.39388,0.15397339 209.86572,26.483423"
id="path11" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="M 198.62567,0.30794677 209.55778,15.551312"
id="path12" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 115.28177,0.20224871 c 0,0 -2.52811,22.24735829 -0.30337,25.68558729"
id="path13" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 120.33799,1.415741 0.30337,11.932674 v 0 c 0,0 -1.21349,6.269711 -1.21349,10.213561"
id="path14" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 120.64136,13.752913 c 0,0 1.92136,7.584327 2.02249,8.59557"
id="path15" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 125.89983,0.80899486 c 0,0 0,9.50569014 5.05621,17.79788714"
id="path16" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 126.91107,10.112436 c 0,0 -0.4045,5.865213 0.70787,10.314684"
id="path17" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="M 128.63018,0.20224871 134.39427,17.494514"
id="path18" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 135.30439,0.30337307 c 0,0 0.60675,9.91018693 2.42698,15.57315093"
id="path19" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 139.75386,0.7078705 c 0,0 -1.41574,3.94385 1.61799,13.7529125"
id="path20" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 143.09097,1.1123679 c 0,0 1.82024,8.3933216 3.84272,11.2248041"
id="path21" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 144.30446,6.0674614 c 0,0 -0.809,2.9326065 -0.30337,6.7753316"
id="path22" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="M 147.54044,0.40449743 148.75393,10.618058"
id="path23" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 150.87754,0.20224871 3.43823,7.78657559"
id="path24" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 153.2034,0.10112436 3.3371,6.37083444"
id="path25" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 155.52926,0.20224871 3.33711,5.66296389"
id="path26" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="M 159.06861,0.50562179 161.4956,4.7528448"
id="path27" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="M 162.00122,0.40449743 164.02371,3.94385"
id="path28" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 164.4282,-0.30337307 1.92137,3.33710377"
id="path29" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 115.28177,26.797955 c 0,0 -2.02249,11.427052 11.93267,16.786643"
id="path30" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 120.03461,24.269846 c 0,0 3.84273,11.022554 12.74167,14.86528"
id="path31" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 126.30432,21.33724 c 0,0 0.4045,9.404565 9.00007,15.067529"
id="path32" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 134.69765,17.797887 c 0,0 -4.85397,8.494446 5.15734,14.460782"
id="path33" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 137.428,16.078773 c 0,0 0.30337,6.26971 5.05622,13.95516"
id="path34" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 140.15836,14.15741 c 0,0 -1.01124,6.370835 4.75285,13.854038"
id="path35" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 143.29321,13.045042 c 0,0 -0.91011,7.584327 4.34835,12.640545"
id="path36" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 146.32695,12.842793 c 0,0 -2.32586,4.044975 3.13485,11.325928"
id="path37" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 147.54044,11.427052 c 0,0 0.20225,7.17983 4.75284,10.820307"
id="path38" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 149.76517,9.9101872 c 0,0 1.41574,8.4944458 3.94385,10.3146838"
id="path39" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 151.58541,9.7079384 c 0,0 2.02249,6.4719586 5.25847,8.5955706"
id="path40" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 153.2034,9.0000679 c 0,0 2.12361,5.9663371 4.85397,7.8877001"
id="path41" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 154.31577,8.2921974 5.86521,7.0787046"
id="path42" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="M 209.52546,105.56381 12.995207,0"
id="path43" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 158.24027,7.5068802 4.05133,6.7919388"
id="path44" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 160.24291,5.8928883 3.88494,7.1587677"
id="path45" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 162.81832,4.4087534 3.71034,6.8968616"
id="path46" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 165.48103,3.666686 3.01192,6.416701"
id="path47" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 167.88184,2.4008064 2.79367,5.9365392"
id="path48" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 171.19932,0.52381229 2.1389,5.98019051"
id="path49" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 173.42552,0.43651024 1.70239,4.62700856"
id="path50" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 176.17554,0.43651024 1.30953,3.14287386"
id="path51" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 176.52474,4.6270087 1.39684,1.7460409"
id="path52" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 174.56045,5.9365393 1.83334,1.920645"
id="path53" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 171.85408,7.8571843 2.70637,2.0952494"
id="path54" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 170.23899,9.4286212 2.09526,2.4881088"
id="path55" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 167.00882,11.654823 3.49208,2.051599"
id="path56" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 165.00087,12.702448 3.44843,2.793666"
id="path57" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 163.25483,14.317536 3.31748,3.011921"
id="path58" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 161.02863,15.32151 4.23415,3.797639"
id="path59" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 158.80243,17.89692 3.75399,3.579384"
id="path60" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 155.6159,18.900894 5.84924,4.103196"
id="path61" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 154.48098,21.432653 5.10717,3.317478"
id="path62" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 151.94922,22.698533 4.58335,4.845264"
id="path63" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 149.06825,25.361245 6.19844,4.190498"
id="path64" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 148.23888,26.539822 c 0,0 1.74604,3.492082 4.71431,5.674635"
id="path65" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 144.57219,28.635073 c 0,0 2.35716,2.575409 6.54766,4.583356"
id="path66" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 142.6952,30.992228 c 0,0 3.66669,4.365101 6.2421,5.019868"
id="path67" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 138.63565,33.916847 c 0,0 4.23415,3.186523 8.25005,4.059544"
id="path68" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 137.10787,35.008121 c 0,0 4.1905,5.89289 7.15877,6.023843"
id="path69" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 134.88167,37.758137 c 0,0 2.79366,4.32145 6.72225,5.500028"
id="path70" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 132.69912,39.373225 c 0,0 3.53573,5.325425 7.50797,6.111142"
id="path71" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 130.77847,41.512124 c 0,0 3.66669,6.02384 7.20242,7.289721"
id="path72" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 128.42131,43.781977 c 0,0 2.44446,5.369076 7.07147,6.984164"
id="path73" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 127.06813,45.528018 c 0,0 2.70637,7.420676 6.11115,8.555601"
id="path74" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 124.49272,48.452637 c 0,0 2.92462,6.373051 6.94051,7.988139"
id="path75" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 182.0798,2.2845037 2.38172,2.0414713"
id="path76" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 183.92685,5.4925301 2.2845,1.7498327 2.81918,2.0900778"
id="path77" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 188.7875,10.110144 4.03433,-0.729097 4.71483,-1.3123744"
id="path78" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 197.68248,7.8256402 2.38171,-0.8749163"
id="path79" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 200.55026,5.055072 1.60401,-1.0693422"
id="path80" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="M 201.6196,3.8399103 204.29296,0"
id="path81" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 203.32083,6.9021176 c 0,0 3.35384,-2.7219619 4.18015,-6.65908529"
id="path82" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 204.92484,8.4089178 c 0,0 3.45106,-2.2358971 4.61761,-7.3881821"
id="path83" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 180.76743,4.4717943 1.84705,2.6247489"
id="path84" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 182.46866,7.1451498 2.57614,2.7219619"
id="path85" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 184.80176,10.547602 3.49967,1.992865"
id="path86" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 188.44725,13.220958 4.37458,-0.194426"
id="path87" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 192.67601,13.804235 5.88138,-1.992865"
id="path88" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 198.55739,10.742028 3.0136,-1.0693422"
id="path89" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 203.51525,7.5340016 -1.94426,1.6526195"
id="path90" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 205.11927,9.4782599 -2.57615,2.0414711"
id="path91" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 177.65661,7.5340016 2.43033,2.0900776"
id="path92" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 180.23276,10.450389 3.0622,2.770569"
id="path93" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 183.10054,14.14448 4.27737,2.381717"
id="path94" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 188.39864,15.748494 4.13155,0.09721"
id="path95" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 193.3079,15.991526 5.44392,-1.360981"
id="path96" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 199.57813,15.408248 4.76343,-0.243032"
id="path97" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 204.04992,13.220958 2.77057,-1.360981"
id="path98" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 206.62607,10.596209 2.96499,-3.7913043"
id="path99" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 207.74402,12.929319 1.70122,-2.284504"
id="path100" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 175.71236,9.5754729 2.81917,2.3331101"
id="path101" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 178.04547,13.609809 4.13155,2.867781"
id="path102" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 182.37144,16.428984 4.81204,2.235897 5.2495,0.09721"
id="path103" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 192.28716,18.713488 7.4854,-0.82631"
id="path104" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 200.21001,19.296765 4.95786,-1.701226"
id="path105" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 205.4109,15.311035 2.77057,-1.5068"
id="path106" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 200.8419,20.852172 -7.97146,1.5068"
id="path107" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 186.50299,22.164546 6.85351,0.194426"
id="path108" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 180.71882,19.393978 5.83278,2.770568"
id="path109" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 176.49006,15.408248 4.71483,3.499665"
id="path110" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 173.96252,11.568338 2.91639,3.208026"
id="path111" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 171.62941,13.46399 3.30524,3.15942"
id="path112" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 174.88605,18.178817 4.76343,3.062207"
id="path113" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 179.40645,23.039463 7.14515,2.18729"
id="path114" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 185.87111,26.150276 6.70769,-0.534671"
id="path115" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 200.79329,23.428314 -8.2631,2.187291"
id="path116" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 207.74402,22.504792 c 0,0 -5.00647,2.867781 -5.88139,3.062207"
id="path117" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 168.42139,16.185952 5.2981,2.624749"
id="path118" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 166.91459,17.692752 4.76343,3.888517"
id="path119" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 172.65015,20.657746 5.63835,3.402452"
id="path120" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 178.48292,26.053063 7.04794,1.652619"
id="path121" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 185.28783,28.726418 7.63121,-0.68049"
id="path122" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 201.71681,26.393308 -8.79777,1.604014"
id="path123" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="M 202.49452,29.066664 193.3565,31.74002"
id="path124" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 185.23922,31.399773 8.2145,-0.14582"
id="path125" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 176.68449,29.455514 8.65195,1.166556"
id="path126" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 169.9768,25.858637 6.41605,3.256634"
id="path127" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 171.09474,23.379708 c 0,0 3.93713,3.353845 6.41605,3.645484"
id="path128" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 165.16475,20.074469 c 0,0 3.30524,3.645484 5.34672,3.985729"
id="path129" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 162.88025,21.678482 c 0,0 4.4718,4.325975 6.56187,4.569007"
id="path130" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 160.49853,23.914379 c 0,0 4.90926,3.791303 7.14515,4.131549"
id="path131" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 175.42072,31.691413 c 0,0 -4.61762,-0.388853 -7.77704,-3.499665"
id="path132" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 184.80176,33.100999 c 0,0 -7.14515,-0.194424 -9.13801,-1.604013"
id="path133" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 184.65594,35.142471 8.79778,-1.263769"
id="path134" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 203.32083,31.5942 -10.20736,2.478929"
id="path135" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 166.91459,29.892974 c 0,0 -5.58975,-1.020736 -8.06868,-4.180156"
id="path136" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 166.37992,30.524857 c 0,0 6.12441,3.548272 8.84637,3.839911"
id="path137" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 184.51013,36.114601 c 0,0 -9.33244,-2.041472 -9.67269,-2.624749"
id="path138" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 184.36431,37.47558 c 0,0 8.36031,-0.437457 9.0408,-0.729096"
id="path139" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 204.34156,33.975915 c 0,0 -10.01293,3.402455 -10.83924,3.402455"
id="path140" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 204.6332,36.211814 -11.13088,3.305238"
id="path141" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 183.73242,41.023854 9.96433,-1.701228"
id="path142" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 173.52507,38.544923 10.20735,2.478931"
id="path143" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 174.4972,36.697877 9.86711,1.992866"
id="path144" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 164.97033,33.635672 9.13801,2.867781"
id="path145" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 156.36699,29.018058 8.94358,3.353845"
id="path146" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 164.24123,34.899438 c 0,0 -8.3117,-2.916385 -9.18662,-5.152284"
id="path147" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 173.71949,38.787956 c 0,0 -7.97146,-2.138685 -9.96432,-4.714827"
id="path148" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 206.33443,38.593529 -12.20022,2.867782"
id="path149" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 183.97545,42.530654 9.7213,-1.166556"
id="path150" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 172.74736,42.093194 c 0,0 9.04081,1.798439 10.5476,0.923523"
id="path151" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 162.58861,37.864433 c 0,0 7.19376,4.034338 10.15875,3.694091"
id="path152" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 153.20756,32.12887 c 0,0 6.22163,5.881383 9.08941,5.686956"
id="path153" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 150.72864,34.559195 c 0,0 8.11727,5.443923 10.20735,5.395317"
id="path154" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 149.31905,35.725748 c 0,0 6.70769,7.290969 10.79063,6.075809"
id="path155" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 171.58081,46.516382 c 0,0 -4.76344,1.749835 -11.66555,-4.277368"
id="path156" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 183.00333,48.071791 c 0,0 -4.81204,1.117949 -11.2767,-1.701226"
id="path157" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 194.91191,46.710808 c 0,0 -9.42965,2.819176 -11.47113,1.749833"
id="path158" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 194.37724,43.94024 -10.74203,0.729099"
id="path159" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 160.64435,41.995981 11.13088,2.527538"
id="path160" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="M 183.19775,46.224745 171.82384,44.572126"
id="path161" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="M 206.43164,41.169672 194.23142,44.08606"
id="path162" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 207.35516,43.11393 -12.73489,3.694092"
id="path163" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="M 208.08426,45.301222 195.54379,49.57859"
id="path164" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 147.28059,37.851884 c 0,0 7.4801,7.80252 11.22015,6.448364"
id="path165" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 145.41056,39.850877 c 0,0 5.28766,7.99597 11.86499,7.480102"
id="path166" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 142.44432,43.139542 c 0,0 6.38387,6.899749 13.41259,7.738033"
id="path167" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 141.15465,44.751632 c 0,0 3.09521,8.576321 12.70327,12.058439"
id="path168" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 139.67152,46.621657 c 0,0 4.51385,13.283626 12.63879,15.991938"
id="path169" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 137.35011,49.00755 c 0,0 8.18942,11.607054 15.41159,9.93048"
id="path170" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 135.86699,51.071028 c 0,0 -3.67557,8.124936 15.02468,15.218135"
id="path171" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 131.74004,56.874552 2.64383,8.124936"
id="path172" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 146.76472,71.641302 4.57834,-2.192443"
id="path173" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 131.4821,56.229718 5.28766,0.709318"
id="path174" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 157.72694,45.58992 13.15465,4.320402"
id="path175" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 157.27555,47.00856 c 0,0 9.60806,5.739043 13.15466,4.642821"
id="path176" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 156.56623,49.00755 c 0,0 6.19043,5.739043 12.83224,5.15869"
id="path177" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 154.88966,53.198987 14.63778,4.062468"
id="path178" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 168.94708,63.387398 c 0,0 -13.67052,-6.319393 -14.31536,-11.284633"
id="path179" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="M 169.14053,59.840799 161.85389,59.32493"
id="path180" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 153.5355,56.874552 c 0,0 3.35315,5.094208 14.89572,9.479092"
id="path181" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 151.66548,63.838785 c 0,0 13.79949,6.254911 16.83022,5.287655"
id="path182" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 168.68915,72.28614 c 0,0 -17.41058,-2.127962 -17.99093,-4.126953"
id="path183" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 170.62366,49.910322 c 0,0 11.60705,2.450378 13.02569,1.354156"
id="path184" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 170.04331,55.971783 c 0,0 6.83526,-1.289674 12.70327,0.902769"
id="path185" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 183.52038,55.907299 c 0,0 12.18741,-0.644837 12.63879,-1.547606"
id="path186" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 182.87555,49.587903 c 0,0 12.76775,1.998994 13.15465,3.095215"
id="path187" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 170.23676,51.457928 c 0,0 4.3204,-0.19345 5.22317,0.902772 0.90277,1.096221 6.06146,2.063475 7.22217,0.902771"
id="path188" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 183.32693,52.038281 4.25592,-1.547606"
id="path189" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 190.87151,50.619641 4.19144,-1.354156"
id="path190" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 196.61056,54.295209 c 0,0 12.50982,-5.868011 13.34811,-3.933503"
id="path191" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 195.12744,52.16725 c 0,0 14.18639,-0.515869 14.63778,-3.997987"
id="path192" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 169.72089,57.841808 c 0,0 11.67153,3.159696 13.15466,1.547606"
id="path193" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 197.31988,56.939036 -14.37985,3.288665"
id="path194" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 197.77126,60.356667 c 0,0 -9.4146,-0.451384 -9.67254,-1.354156"
id="path195" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 169.2695,61.517373 c 0,0 13.28363,0 13.67053,1.22519"
id="path196" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 168.81812,64.161201 c 0,0 5.93249,-0.902769 14.37985,1.354156"
id="path197" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 168.36673,67.965735 14.89572,0.967255"
id="path198" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 169.39847,73.769261 13.7995,-2.192443"
id="path199" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 168.23777,71.641302 c 0,0 1.48312,5.674559 15.92745,2.643828"
id="path200" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 169.33399,76.735508 c 0,0 7.0932,-0.773803 14.31536,10.833248"
id="path201" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 184.74557,76.671024 -8.96322,2.192443"
id="path202" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="M 184.55212,79.766238 177.26547,79.44382"
id="path203" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 162.11182,80.346591 7.35113,-2.966246"
id="path204" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 165.27152,82.023166 4.12695,-2.256928"
id="path205" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 171.07504,82.539035 c 0,0 14.25089,-0.128969 14.63779,1.870024"
id="path206" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 180.74759,89.890168 c 0,0 4.90075,-3.417634 5.99698,-2.256928"
id="path207" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 182.87555,67.901253 15.60503,-4.642821"
id="path208" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 199.44784,65.773294 c 0,0 -15.21814,2.837278 -15.66952,2.837278"
id="path209" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 182.94003,71.899237 17.3461,-3.224181"
id="path210" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="M 183.52038,73.640296 201.5758,70.996465"
id="path211" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="M 183.71383,77.444827 202.3496,73.575811"
id="path212" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 185.06799,80.153141 c 0,0 19.47405,-2.063477 21.08614,-0.128968"
id="path213" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 203.70376,77.057926 -7.02872,2.385894"
id="path214" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 186.35766,85.440797 c 0,0 9.67254,2.450377 13.54156,1.80554"
id="path215" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="M 188.1632,90.470518 209.37831,86.02115"
id="path216" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 186.6156,87.568756 c 0,0 17.34609,-2.127959 20.44131,-3.804534"
id="path217" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 197.70678,57.068005 12.25189,-2.966246"
id="path218" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 198.09368,60.55012 11.86499,-3.804534"
id="path219" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 199.06094,62.613595 10.63979,-2.643828"
id="path220" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 199.77026,65.773294 c 0,0 8.83425,-4.255921 9.8015,-3.546599"
id="path221" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 200.86648,68.610572 c 0,0 4.38488,1.354156 8.83425,-1.483122"
id="path222" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 201.70476,71.060949 2.32141,-2.063474"
id="path223" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 202.99444,74.220646 6.96423,-3.030728"
id="path224" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 205.1224,79.314854 4.64282,-2.64383"
id="path225" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="m 208.34658,83.635256 1.41864,-0.838287"
id="path226" /><path
style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
d="M 29.690113,9.1690057 175.30265,0"
id="path227" /></g></svg>

Before

Width:  |  Height:  |  Size: 43 KiB

View File

@@ -1,70 +0,0 @@
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

View File

@@ -1,49 +0,0 @@
#!/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

View File

@@ -1,69 +0,0 @@
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)

View File

@@ -1,87 +0,0 @@
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

Submodule code/agda-spa deleted from 9131214880

Submodule code/compiler deleted from 137455b0f4

View File

@@ -0,0 +1,33 @@
%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();
}

128
code/compiler/02/ast.hpp Normal file
View File

@@ -0,0 +1,128 @@
#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)) {}
};

1
code/compiler/02/clean.sh Executable file
View File

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

5
code/compiler/02/compile.sh Executable file
View File

@@ -0,0 +1,5 @@
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

14
code/compiler/02/main.cpp Normal file
View File

@@ -0,0 +1,14 @@
#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;
}

140
code/compiler/02/parser.y Normal file
View File

@@ -0,0 +1,140 @@
%{
#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))); }
;

View File

@@ -0,0 +1,34 @@
%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)); }
%%

82
code/compiler/03/ast.cpp Normal file
View File

@@ -0,0 +1,82 @@
#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;
}

162
code/compiler/03/ast.hpp Normal file
View File

@@ -0,0 +1,162 @@
#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;
};

View File

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

View File

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

1
code/compiler/03/clean.sh Executable file
View File

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

9
code/compiler/03/compile.sh Executable file
View File

@@ -0,0 +1,9 @@
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

View File

@@ -0,0 +1,48 @@
#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
}

16
code/compiler/03/env.cpp Normal file
View File

@@ -0,0 +1,16 @@
#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);
}

16
code/compiler/03/env.hpp Normal file
View File

@@ -0,0 +1,16 @@
#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;
};

39
code/compiler/03/main.cpp Normal file
View File

@@ -0,0 +1,39 @@
#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;
}

140
code/compiler/03/parser.y Normal file
View File

@@ -0,0 +1,140 @@
%{
#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))); }
;

View File

@@ -0,0 +1,34 @@
%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)); }
%%

78
code/compiler/03/type.cpp Normal file
View File

@@ -0,0 +1,78 @@
#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;
}

44
code/compiler/03/type.hpp Normal file
View File

@@ -0,0 +1,44 @@
#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);
};

View File

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

View File

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

View File

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

View File

@@ -0,0 +1,25 @@
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})

145
code/compiler/04/ast.cpp Normal file
View File

@@ -0,0 +1,145 @@
#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);
}

172
code/compiler/04/ast.hpp Normal file
View File

@@ -0,0 +1,172 @@
#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;
};

View File

@@ -0,0 +1,48 @@
#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
}

16
code/compiler/04/env.cpp Normal file
View File

@@ -0,0 +1,16 @@
#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);
}

16
code/compiler/04/env.hpp Normal file
View File

@@ -0,0 +1,16 @@
#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;
};

View File

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

View File

@@ -0,0 +1,21 @@
#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") {}
};

View File

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

View File

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

View File

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

View File

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

View File

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

70
code/compiler/04/main.cpp Normal file
View File

@@ -0,0 +1,70 @@
#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;
}
}

140
code/compiler/04/parser.y Normal file
View File

@@ -0,0 +1,140 @@
%{
#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))); }
;

View File

@@ -0,0 +1,34 @@
%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)); }
%%

99
code/compiler/04/type.cpp Normal file
View File

@@ -0,0 +1,99 @@
#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;
}

54
code/compiler/04/type.hpp Normal file
View File

@@ -0,0 +1,54 @@
#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;
};
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);
};

View File

@@ -0,0 +1,28 @@
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
type_env.cpp type_env.hpp
env.cpp env.hpp
type.cpp type.hpp
error.cpp error.hpp
binop.cpp binop.hpp
instruction.cpp instruction.hpp
${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})

262
code/compiler/06/ast.cpp Normal file
View File

@@ -0,0 +1,262 @@
#include "ast.hpp"
#include <ostream>
#include "error.hpp"
static void print_indent(int n, std::ostream& to) {
while(n--) to << " ";
}
type_ptr ast::typecheck_common(type_mgr& mgr, const type_env& env) {
node_type = typecheck(mgr, env);
return node_type;
}
void ast::resolve_common(const type_mgr& mgr) {
type_var* var;
type_ptr resolved_type = mgr.resolve(node_type, var);
if(var) throw type_error("ambiguously typed program");
resolve(mgr);
node_type = std::move(resolved_type);
}
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_int::resolve(const type_mgr& mgr) const {
}
void ast_int::compile(const env_ptr& env, std::vector<instruction_ptr>& into) const {
into.push_back(instruction_ptr(new instruction_pushint(value)));
}
void ast_lid::print(int indent, std::ostream& to) const {
print_indent(indent, to);
to << "LID: " << id << std::endl;
}
type_ptr ast_lid::typecheck(type_mgr& mgr, const type_env& env) const {
return env.lookup(id);
}
void ast_lid::resolve(const type_mgr& mgr) const {
}
void ast_lid::compile(const env_ptr& env, std::vector<instruction_ptr>& into) const {
into.push_back(instruction_ptr(
env->has_variable(id) ?
(instruction*) new instruction_push(env->get_offset(id)) :
(instruction*) new instruction_pushglobal(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_uid::resolve(const type_mgr& mgr) const {
}
void ast_uid::compile(const env_ptr& env, std::vector<instruction_ptr>& into) const {
into.push_back(instruction_ptr(new instruction_pushglobal(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_common(mgr, env);
type_ptr rtype = right->typecheck_common(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_binop::resolve(const type_mgr& mgr) const {
left->resolve_common(mgr);
right->resolve_common(mgr);
}
void ast_binop::compile(const env_ptr& env, std::vector<instruction_ptr>& into) const {
right->compile(env, into);
left->compile(env_ptr(new env_offset(1, env)), into);
into.push_back(instruction_ptr(new instruction_pushglobal(op_action(op))));
into.push_back(instruction_ptr(new instruction_mkapp()));
into.push_back(instruction_ptr(new instruction_mkapp()));
}
void ast_app::print(int indent, std::ostream& to) const {
print_indent(indent, to);
to << "APP:" << std::endl;
left->print(indent + 1, to);
right->print(indent + 1, to);
}
type_ptr ast_app::typecheck(type_mgr& mgr, const type_env& env) const {
type_ptr ltype = left->typecheck_common(mgr, env);
type_ptr rtype = right->typecheck_common(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_app::resolve(const type_mgr& mgr) const {
left->resolve_common(mgr);
right->resolve_common(mgr);
}
void ast_app::compile(const env_ptr& env, std::vector<instruction_ptr>& into) const {
right->compile(env, into);
left->compile(env_ptr(new env_offset(1, env)), into);
into.push_back(instruction_ptr(new instruction_mkapp()));
}
void ast_case::print(int indent, std::ostream& to) const {
print_indent(indent, to);
to << "CASE: " << std::endl;
for(auto& branch : branches) {
print_indent(indent + 1, to);
branch->pat->print(to);
to << std::endl;
branch->expr->print(indent + 2, to);
}
}
type_ptr ast_case::typecheck(type_mgr& mgr, const type_env& env) const {
type_var* var;
type_ptr case_type = mgr.resolve(of->typecheck_common(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_common(mgr, new_env);
mgr.unify(branch_type, curr_branch_type);
}
case_type = mgr.resolve(case_type, var);
if(!dynamic_cast<type_data*>(case_type.get())) {
throw type_error("attempting case analysis of non-data type");
}
return branch_type;
}
void ast_case::resolve(const type_mgr& mgr) const {
of->resolve_common(mgr);
for(auto& branch : branches) {
branch->expr->resolve_common(mgr);
}
}
void ast_case::compile(const env_ptr& env, std::vector<instruction_ptr>& into) const {
type_data* type = dynamic_cast<type_data*>(of->node_type.get());
of->compile(env, into);
into.push_back(instruction_ptr(new instruction_eval()));
instruction_jump* jump_instruction = new instruction_jump();
into.push_back(instruction_ptr(jump_instruction));
for(auto& branch : branches) {
std::vector<instruction_ptr> branch_instructions;
pattern_var* vpat;
pattern_constr* cpat;
if((vpat = dynamic_cast<pattern_var*>(branch->pat.get()))) {
branch->expr->compile(env_ptr(new env_offset(1, env)), branch_instructions);
for(auto& constr_pair : type->constructors) {
if(jump_instruction->tag_mappings.find(constr_pair.second.tag) !=
jump_instruction->tag_mappings.end())
break;
jump_instruction->tag_mappings[constr_pair.second.tag] =
jump_instruction->branches.size();
}
jump_instruction->branches.push_back(std::move(branch_instructions));
} else if((cpat = dynamic_cast<pattern_constr*>(branch->pat.get()))) {
env_ptr new_env = env;
for(auto it = cpat->params.rbegin(); it != cpat->params.rend(); it++) {
new_env = env_ptr(new env_var(*it, new_env));
}
branch_instructions.push_back(instruction_ptr(new instruction_split()));
branch->expr->compile(new_env, branch_instructions);
branch_instructions.push_back(instruction_ptr(new instruction_slide(
cpat->params.size())));
int new_tag = type->constructors[cpat->constr].tag;
if(jump_instruction->tag_mappings.find(new_tag) !=
jump_instruction->tag_mappings.end())
throw type_error("technically not a type error: duplicate pattern");
jump_instruction->tag_mappings[new_tag] =
jump_instruction->branches.size();
jump_instruction->branches.push_back(std::move(branch_instructions));
}
}
for(auto& constr_pair : type->constructors) {
if(jump_instruction->tag_mappings.find(constr_pair.second.tag) ==
jump_instruction->tag_mappings.end())
throw type_error("non-total pattern");
}
}
void 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);
}

197
code/compiler/06/ast.hpp Normal file
View File

@@ -0,0 +1,197 @@
#pragma once
#include <memory>
#include <vector>
#include "type.hpp"
#include "type_env.hpp"
#include "binop.hpp"
#include "instruction.hpp"
#include "env.hpp"
struct ast {
type_ptr node_type;
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;
virtual void resolve(const type_mgr& mgr) const = 0;
virtual void compile(const env_ptr& env,
std::vector<instruction_ptr>& into) const = 0;
type_ptr typecheck_common(type_mgr& mgr, const type_env& env);
void resolve_common(const type_mgr& mgr);
};
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;
int8_t tag;
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;
virtual void resolve(const type_mgr& mgr) = 0;
virtual void compile() = 0;
};
using definition_ptr = std::unique_ptr<definition>;
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;
void resolve(const type_mgr& mgr) const;
void compile(const env_ptr& env, std::vector<instruction_ptr>& into) const;
};
struct ast_lid : public ast {
std::string id;
explicit ast_lid(std::string i)
: id(std::move(i)) {}
void print(int indent, std::ostream& to) const;
type_ptr typecheck(type_mgr& mgr, const type_env& env) const;
void resolve(const type_mgr& mgr) const;
void compile(const env_ptr& env, std::vector<instruction_ptr>& into) const;
};
struct ast_uid : public ast {
std::string id;
explicit ast_uid(std::string i)
: id(std::move(i)) {}
void print(int indent, std::ostream& to) const;
type_ptr typecheck(type_mgr& mgr, const type_env& env) const;
void resolve(const type_mgr& mgr) const;
void compile(const env_ptr& env, std::vector<instruction_ptr>& into) const;
};
struct ast_binop : public ast {
binop op;
ast_ptr left;
ast_ptr right;
ast_binop(binop o, ast_ptr l, ast_ptr r)
: 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;
void resolve(const type_mgr& mgr) const;
void compile(const env_ptr& env, std::vector<instruction_ptr>& into) const;
};
struct ast_app : public ast {
ast_ptr left;
ast_ptr right;
ast_app(ast_ptr l, ast_ptr r)
: 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;
void resolve(const type_mgr& mgr) const;
void compile(const env_ptr& env, std::vector<instruction_ptr>& into) 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;
void resolve(const type_mgr& mgr) const;
void compile(const env_ptr& env, std::vector<instruction_ptr>& into) const;
};
struct pattern_var : public pattern {
std::string var;
pattern_var(std::string v)
: 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;
std::vector<instruction_ptr> instructions;
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;
void resolve(const type_mgr& mgr);
void compile();
};
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;
void resolve(const type_mgr& mgr);
void compile();
};

View File

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

View File

@@ -0,0 +1,12 @@
#pragma once
#include <string>
enum binop {
PLUS,
MINUS,
TIMES,
DIVIDE
};
std::string op_name(binop op);
std::string op_action(binop op);

View File

@@ -0,0 +1,83 @@
#include "ast.hpp"
#include "error.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_common(mgr, new_env);
mgr.unify(return_type, body_type);
}
void definition_defn::resolve(const type_mgr& mgr) {
type_var* var;
body->resolve_common(mgr);
return_type = mgr.resolve(return_type, var);
if(var) throw type_error("ambiguously typed program");
for(auto& param_type : param_types) {
param_type = mgr.resolve(param_type, var);
if(var) throw type_error("ambiguously typed program");
}
}
void definition_defn::compile() {
env_ptr new_env = env_ptr(new env_offset(0, nullptr));
for(auto it = params.rbegin(); it != params.rend(); it++) {
new_env = env_ptr(new env_var(*it, new_env));
}
body->compile(new_env, instructions);
instructions.push_back(instruction_ptr(new instruction_update(params.size())));
instructions.push_back(instruction_ptr(new instruction_pop(params.size())));
}
void definition_data::typecheck_first(type_mgr& mgr, type_env& env) {
type_data* this_type = new type_data(name);
type_ptr return_type = type_ptr(this_type);
int next_tag = 0;
for(auto& constructor : constructors) {
constructor->tag = next_tag;
this_type->constructors[constructor->name] = { next_tag++ };
type_ptr full_type = return_type;
for(auto it = constructor->types.rbegin(); it != constructor->types.rend(); it++) {
type_ptr type = 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
}
void definition_data::resolve(const type_mgr& mgr) {
// Nothing
}
void definition_data::compile() {
}

23
code/compiler/06/env.cpp Normal file
View File

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

34
code/compiler/06/env.hpp Normal file
View File

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

View File

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

View File

@@ -0,0 +1,21 @@
#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") {}
};

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

@@ -0,0 +1,83 @@
#include "instruction.hpp"
static void print_indent(int n, std::ostream& to) {
while(n--) to << " ";
}
void instruction_pushint::print(int indent, std::ostream& to) const {
print_indent(indent, to);
to << "PushInt(" << value << ")" << std::endl;
}
void instruction_pushglobal::print(int indent, std::ostream& to) const {
print_indent(indent, to);
to << "PushGlobal(" << name << ")" << std::endl;
}
void instruction_push::print(int indent, std::ostream& to) const {
print_indent(indent, to);
to << "Push(" << offset << ")" << std::endl;
}
void instruction_pop::print(int indent, std::ostream& to) const {
print_indent(indent, to);
to << "Pop(" << count << ")" << std::endl;
}
void instruction_mkapp::print(int indent, std::ostream& to) const {
print_indent(indent, to);
to << "MkApp()" << std::endl;
}
void instruction_update::print(int indent, std::ostream& to) const {
print_indent(indent, to);
to << "Update(" << offset << ")" << std::endl;
}
void instruction_pack::print(int indent, std::ostream& to) const {
print_indent(indent, to);
to << "Pack(" << tag << ", " << size << ")" << std::endl;
}
void instruction_split::print(int indent, std::ostream& to) const {
print_indent(indent, to);
to << "Split()" << std::endl;
}
void instruction_jump::print(int indent, std::ostream& to) const {
print_indent(indent, to);
to << "Jump(" << std::endl;
for(auto& instruction_set : branches) {
for(auto& instruction : instruction_set) {
instruction->print(indent + 2, to);
}
to << std::endl;
}
print_indent(indent, to);
to << ")" << std::endl;
}
void instruction_slide::print(int indent, std::ostream& to) const {
print_indent(indent, to);
to << "Slide(" << offset << ")" << std::endl;
}
void instruction_binop::print(int indent, std::ostream& to) const {
print_indent(indent, to);
to << "BinOp(" << op_action(op) << ")" << std::endl;
}
void instruction_eval::print(int indent, std::ostream& to) const {
print_indent(indent, to);
to << "Eval()" << std::endl;
}
void instruction_alloc::print(int indent, std::ostream& to) const {
print_indent(indent, to);
to << "Alloc(" << amount << ")" << std::endl;
}
void instruction_unwind::print(int indent, std::ostream& to) const {
print_indent(indent, to);
to << "Unwind()" << std::endl;
}

View File

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

88
code/compiler/06/main.cpp Normal file
View File

@@ -0,0 +1,88 @@
#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;
}
for(auto& def : prog) {
def->resolve(mgr);
}
}
void compile_program(const std::vector<definition_ptr>& prog) {
for(auto& def : prog) {
def->compile();
definition_defn* defn = dynamic_cast<definition_defn*>(def.get());
if(!defn) continue;
for(auto& instruction : defn->instructions) {
instruction->print(0, 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);
compile_program(program);
} 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;
}
}

140
code/compiler/06/parser.y Normal file
View File

@@ -0,0 +1,140 @@
%{
#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))); }
;

View File

@@ -0,0 +1,34 @@
%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)); }
%%

99
code/compiler/06/type.cpp Normal file
View File

@@ -0,0 +1,99 @@
#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) const {
type_var* cast;
var = nullptr;
while((cast = dynamic_cast<type_var*>(t.get()))) {
auto it = types.find(cast->name);
if(it == types.end()) {
var = cast;
break;
}
t = it->second;
}
return t;
}
void type_mgr::unify(type_ptr l, type_ptr r) {
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;
}

65
code/compiler/06/type.hpp Normal file
View File

@@ -0,0 +1,65 @@
#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_data : public type_base {
struct constructor {
int tag;
};
std::map<std::string, constructor> constructors;
type_data(std::string n)
: type_base(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)) {}
void print(const type_mgr& mgr, std::ostream& to) const;
};
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) const;
void bind(const std::string& s, type_ptr t);
};

View File

@@ -0,0 +1,16 @@
#include "type_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);
}

View File

@@ -0,0 +1,16 @@
#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;
};

View File

@@ -0,0 +1,28 @@
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
type_env.cpp type_env.hpp
env.cpp env.hpp
type.cpp type.hpp
error.cpp error.hpp
binop.cpp binop.hpp
instruction.cpp instruction.hpp
${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})

262
code/compiler/07/ast.cpp Normal file
View File

@@ -0,0 +1,262 @@
#include "ast.hpp"
#include <ostream>
#include "error.hpp"
static void print_indent(int n, std::ostream& to) {
while(n--) to << " ";
}
type_ptr ast::typecheck_common(type_mgr& mgr, const type_env& env) {
node_type = typecheck(mgr, env);
return node_type;
}
void ast::resolve_common(const type_mgr& mgr) {
type_var* var;
type_ptr resolved_type = mgr.resolve(node_type, var);
if(var) throw type_error("ambiguously typed program");
resolve(mgr);
node_type = std::move(resolved_type);
}
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_int::resolve(const type_mgr& mgr) const {
}
void ast_int::compile(const env_ptr& env, std::vector<instruction_ptr>& into) const {
into.push_back(instruction_ptr(new instruction_pushint(value)));
}
void ast_lid::print(int indent, std::ostream& to) const {
print_indent(indent, to);
to << "LID: " << id << std::endl;
}
type_ptr ast_lid::typecheck(type_mgr& mgr, const type_env& env) const {
return env.lookup(id);
}
void ast_lid::resolve(const type_mgr& mgr) const {
}
void ast_lid::compile(const env_ptr& env, std::vector<instruction_ptr>& into) const {
into.push_back(instruction_ptr(
env->has_variable(id) ?
(instruction*) new instruction_push(env->get_offset(id)) :
(instruction*) new instruction_pushglobal(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_uid::resolve(const type_mgr& mgr) const {
}
void ast_uid::compile(const env_ptr& env, std::vector<instruction_ptr>& into) const {
into.push_back(instruction_ptr(new instruction_pushglobal(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_common(mgr, env);
type_ptr rtype = right->typecheck_common(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_binop::resolve(const type_mgr& mgr) const {
left->resolve_common(mgr);
right->resolve_common(mgr);
}
void ast_binop::compile(const env_ptr& env, std::vector<instruction_ptr>& into) const {
right->compile(env, into);
left->compile(env_ptr(new env_offset(1, env)), into);
into.push_back(instruction_ptr(new instruction_pushglobal(op_action(op))));
into.push_back(instruction_ptr(new instruction_mkapp()));
into.push_back(instruction_ptr(new instruction_mkapp()));
}
void ast_app::print(int indent, std::ostream& to) const {
print_indent(indent, to);
to << "APP:" << std::endl;
left->print(indent + 1, to);
right->print(indent + 1, to);
}
type_ptr ast_app::typecheck(type_mgr& mgr, const type_env& env) const {
type_ptr ltype = left->typecheck_common(mgr, env);
type_ptr rtype = right->typecheck_common(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_app::resolve(const type_mgr& mgr) const {
left->resolve_common(mgr);
right->resolve_common(mgr);
}
void ast_app::compile(const env_ptr& env, std::vector<instruction_ptr>& into) const {
right->compile(env, into);
left->compile(env_ptr(new env_offset(1, env)), into);
into.push_back(instruction_ptr(new instruction_mkapp()));
}
void ast_case::print(int indent, std::ostream& to) const {
print_indent(indent, to);
to << "CASE: " << std::endl;
for(auto& branch : branches) {
print_indent(indent + 1, to);
branch->pat->print(to);
to << std::endl;
branch->expr->print(indent + 2, to);
}
}
type_ptr ast_case::typecheck(type_mgr& mgr, const type_env& env) const {
type_var* var;
type_ptr case_type = mgr.resolve(of->typecheck_common(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_common(mgr, new_env);
mgr.unify(branch_type, curr_branch_type);
}
case_type = mgr.resolve(case_type, var);
if(!dynamic_cast<type_data*>(case_type.get())) {
throw type_error("attempting case analysis of non-data type");
}
return branch_type;
}
void ast_case::resolve(const type_mgr& mgr) const {
of->resolve_common(mgr);
for(auto& branch : branches) {
branch->expr->resolve_common(mgr);
}
}
void ast_case::compile(const env_ptr& env, std::vector<instruction_ptr>& into) const {
type_data* type = dynamic_cast<type_data*>(of->node_type.get());
of->compile(env, into);
into.push_back(instruction_ptr(new instruction_eval()));
instruction_jump* jump_instruction = new instruction_jump();
into.push_back(instruction_ptr(jump_instruction));
for(auto& branch : branches) {
std::vector<instruction_ptr> branch_instructions;
pattern_var* vpat;
pattern_constr* cpat;
if((vpat = dynamic_cast<pattern_var*>(branch->pat.get()))) {
branch->expr->compile(env_ptr(new env_offset(1, env)), branch_instructions);
for(auto& constr_pair : type->constructors) {
if(jump_instruction->tag_mappings.find(constr_pair.second.tag) !=
jump_instruction->tag_mappings.end())
break;
jump_instruction->tag_mappings[constr_pair.second.tag] =
jump_instruction->branches.size();
}
jump_instruction->branches.push_back(std::move(branch_instructions));
} else if((cpat = dynamic_cast<pattern_constr*>(branch->pat.get()))) {
env_ptr new_env = env;
for(auto it = cpat->params.rbegin(); it != cpat->params.rend(); it++) {
new_env = env_ptr(new env_var(*it, new_env));
}
branch_instructions.push_back(instruction_ptr(new instruction_split()));
branch->expr->compile(new_env, branch_instructions);
branch_instructions.push_back(instruction_ptr(new instruction_slide(
cpat->params.size())));
int new_tag = type->constructors[cpat->constr].tag;
if(jump_instruction->tag_mappings.find(new_tag) !=
jump_instruction->tag_mappings.end())
throw type_error("technically not a type error: duplicate pattern");
jump_instruction->tag_mappings[new_tag] =
jump_instruction->branches.size();
jump_instruction->branches.push_back(std::move(branch_instructions));
}
}
for(auto& constr_pair : type->constructors) {
if(jump_instruction->tag_mappings.find(constr_pair.second.tag) ==
jump_instruction->tag_mappings.end())
throw type_error("non-total pattern");
}
}
void 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);
}

197
code/compiler/07/ast.hpp Normal file
View File

@@ -0,0 +1,197 @@
#pragma once
#include <memory>
#include <vector>
#include "type.hpp"
#include "type_env.hpp"
#include "binop.hpp"
#include "instruction.hpp"
#include "env.hpp"
struct ast {
type_ptr node_type;
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;
virtual void resolve(const type_mgr& mgr) const = 0;
virtual void compile(const env_ptr& env,
std::vector<instruction_ptr>& into) const = 0;
type_ptr typecheck_common(type_mgr& mgr, const type_env& env);
void resolve_common(const type_mgr& mgr);
};
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;
int8_t tag;
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;
virtual void resolve(const type_mgr& mgr) = 0;
virtual void compile() = 0;
};
using definition_ptr = std::unique_ptr<definition>;
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;
void resolve(const type_mgr& mgr) const;
void compile(const env_ptr& env, std::vector<instruction_ptr>& into) const;
};
struct ast_lid : public ast {
std::string id;
explicit ast_lid(std::string i)
: id(std::move(i)) {}
void print(int indent, std::ostream& to) const;
type_ptr typecheck(type_mgr& mgr, const type_env& env) const;
void resolve(const type_mgr& mgr) const;
void compile(const env_ptr& env, std::vector<instruction_ptr>& into) const;
};
struct ast_uid : public ast {
std::string id;
explicit ast_uid(std::string i)
: id(std::move(i)) {}
void print(int indent, std::ostream& to) const;
type_ptr typecheck(type_mgr& mgr, const type_env& env) const;
void resolve(const type_mgr& mgr) const;
void compile(const env_ptr& env, std::vector<instruction_ptr>& into) const;
};
struct ast_binop : public ast {
binop op;
ast_ptr left;
ast_ptr right;
ast_binop(binop o, ast_ptr l, ast_ptr r)
: 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;
void resolve(const type_mgr& mgr) const;
void compile(const env_ptr& env, std::vector<instruction_ptr>& into) const;
};
struct ast_app : public ast {
ast_ptr left;
ast_ptr right;
ast_app(ast_ptr l, ast_ptr r)
: 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;
void resolve(const type_mgr& mgr) const;
void compile(const env_ptr& env, std::vector<instruction_ptr>& into) 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;
void resolve(const type_mgr& mgr) const;
void compile(const env_ptr& env, std::vector<instruction_ptr>& into) const;
};
struct pattern_var : public pattern {
std::string var;
pattern_var(std::string v)
: 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;
std::vector<instruction_ptr> instructions;
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;
void resolve(const type_mgr& mgr);
void compile();
};
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;
void resolve(const type_mgr& mgr);
void compile();
};

View File

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

View File

@@ -0,0 +1,12 @@
#pragma once
#include <string>
enum binop {
PLUS,
MINUS,
TIMES,
DIVIDE
};
std::string op_name(binop op);
std::string op_action(binop op);

View File

@@ -0,0 +1,83 @@
#include "ast.hpp"
#include "error.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_common(mgr, new_env);
mgr.unify(return_type, body_type);
}
void definition_defn::resolve(const type_mgr& mgr) {
type_var* var;
body->resolve_common(mgr);
return_type = mgr.resolve(return_type, var);
if(var) throw type_error("ambiguously typed program");
for(auto& param_type : param_types) {
param_type = mgr.resolve(param_type, var);
if(var) throw type_error("ambiguously typed program");
}
}
void definition_defn::compile() {
env_ptr new_env = env_ptr(new env_offset(0, nullptr));
for(auto it = params.rbegin(); it != params.rend(); it++) {
new_env = env_ptr(new env_var(*it, new_env));
}
body->compile(new_env, instructions);
instructions.push_back(instruction_ptr(new instruction_update(params.size())));
instructions.push_back(instruction_ptr(new instruction_pop(params.size())));
}
void definition_data::typecheck_first(type_mgr& mgr, type_env& env) {
type_data* this_type = new type_data(name);
type_ptr return_type = type_ptr(this_type);
int next_tag = 0;
for(auto& constructor : constructors) {
constructor->tag = next_tag;
this_type->constructors[constructor->name] = { next_tag++ };
type_ptr full_type = return_type;
for(auto it = constructor->types.rbegin(); it != constructor->types.rend(); it++) {
type_ptr type = 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
}
void definition_data::resolve(const type_mgr& mgr) {
// Nothing
}
void definition_data::compile() {
}

23
code/compiler/07/env.cpp Normal file
View File

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

34
code/compiler/07/env.hpp Normal file
View File

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

View File

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

View File

@@ -0,0 +1,21 @@
#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") {}
};

View File

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

View File

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

View File

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

View File

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

View File

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

Some files were not shown because too many files have changed in this diff Show More