Compare commits
396 Commits
Author | SHA1 | Date | |
---|---|---|---|
7130c6bd11 | |||
c5aacc060a | |||
6048dc0b9c | |||
1f01c3caff | |||
bca44343eb | |||
3b9c2edcdd | |||
fa180ee24e | |||
5846dd5d04 | |||
f6b347eb05 | |||
c1b27a13ae | |||
147658ee89 | |||
4017c52fee | |||
65d290556f | |||
854dccd4d2 | |||
07859cd1af | |||
19be7eb1f5 | |||
5de2ae1203 | |||
595a1ad99b | |||
32ccfc76ae | |||
ae0d54e567 | |||
b774f0e088 | |||
e294bcb2d0 | |||
1322e0249c | |||
e40a05633c | |||
e5fb0a2929 | |||
3bd1f0c8a0 | |||
948759b7d4 | |||
f2e424944e | |||
8a471c6b45 | |||
9b93582d18 | |||
9fc2d16fb8 | |||
f00c69f02c | |||
4fc1191d13 | |||
951aafc90a | |||
ee13409b33 | |||
615aeb72da | |||
3be67ca4c8 | |||
b216581f2b | |||
1060198b01 | |||
0485917a20 | |||
37dd9ad6d4 | |||
77dade1d1d | |||
d140422225 | |||
2defe99c73 | |||
0766211d79 | |||
b854eade3c | |||
c6f34f8eaa | |||
0ba5799c75 | |||
324fa948e6 | |||
3e46ff8be6 | |||
18eb1da5ba | |||
dde7df4604 | |||
e4101f1396 | |||
d94ceeab2e | |||
697f083237 | |||
3e97fdcfea | |||
40007c427e | |||
5ab0d0d40e | |||
7c65afbc93 | |||
fb071e55aa | |||
406c934b7a | |||
292cf009e6 | |||
6bf7659b19 | |||
0a90e8da29 | |||
32fe8e5ee6 | |||
7ccbaa7829 | |||
7817c9a4ce | |||
bf9b0aedf9 | |||
21b2ff208e | |||
ecad4541f6 | |||
26a29865e7 | |||
ba287130d3 | |||
864276ea72 | |||
23eb36b911 | |||
51bcd116b3 | |||
928adbd594 | |||
e91b6f692f | |||
861dafef70 | |||
388c23c376 | |||
82d9196c90 | |||
826a16eb66 | |||
0b97eb85a1 | |||
a2132001e8 | |||
4fd6dd5606 | |||
7b71ec4402 | |||
07771117ac | |||
7fbc884e94 | |||
b40be72590 | |||
b3db25c470 | |||
6a7b6ffc1f | |||
c87bb90c48 | |||
a6225191d0 | |||
afb904a64c | |||
cbad391dcd | |||
0bf3facf6c | |||
a9da39b987 | |||
1071bdd35a | |||
8656985885 | |||
3be523b79e | |||
1fb7e5ff85 | |||
df75d6e017 | |||
29c9af4902 | |||
7b03183e75 | |||
4c70e61a14 | |||
b2b225f4ae | |||
c17142e648 | |||
8e4759bd2b | |||
d2807917d2 | |||
71c030b947 | |||
1f3ab5349a | |||
daaccb9b2f | |||
b66c58b68e | |||
13636a0d29 | |||
5232f0a6e2 | |||
6a168f2fe1 | |||
04f12b545d | |||
711b01175d | |||
272c2666c5 | |||
60ba43378a | |||
1da60b3b28 | |||
ee118b07e5 | |||
06ee998d54 | |||
c197a45540 | |||
4d23b45633 | |||
c027efa931 | |||
96c4d6fecc | |||
4e1fd54c58 | |||
d6db020e1c | |||
c0f4fe017f | |||
11d726a6ad | |||
37399afc68 | |||
5c19fc4208 | |||
00f0f13b93 | |||
54844fb954 | |||
6ffd3afeaa | |||
9d0dcd98bd | |||
f78f877e21 | |||
5d0b903c03 | |||
032411fe9c | |||
76b061d699 | |||
08d37c839c | |||
0a26230fe1 | |||
2e59beda0c | |||
ee8b1f5dc0 | |||
4938cdaecd | |||
84f28ae5ce | |||
58e7a1f2dc | |||
78bba7a0e9 | |||
9d31764073 | |||
d787548915 | |||
a29bca499f | |||
60d3b3025a | |||
c036041339 | |||
1df315612a | |||
15beddf96b | |||
20d8b18a9b | |||
53ff0c39e4 | |||
357a3bef09 | |||
81eef51e88 | |||
10dfb2fe49 | |||
ef76149112 | |||
a6a330a78e | |||
7f4d0df366 | |||
3eddac0a89 | |||
6e7ac1c1ca | |||
68d9cf1274 | |||
5eb0d1548c | |||
e543904995 | |||
ffda1d3235 | |||
b705aa217c | |||
6f20b17948 | |||
2fde7e5cf8 | |||
bee06b6731 | |||
d3fa7336a2 | |||
96545a899f | |||
6ef5ae2394 | |||
05a31dd4d4 | |||
d9d5c8bf14 | |||
291a1f0178 | |||
2547b53aa2 | |||
409f8b7186 | |||
189422bf1e | |||
74daeee140 | |||
befcd3cf98 | |||
e063ff6aa5 | |||
6179c86919 | |||
a20fe07a56 | |||
2b5dcf12d7 | |||
5873c1ca96 | |||
c6e2ecb996 | |||
2130b00752 | |||
474c3a8348 | |||
29a18b8b37 | |||
21ab4f0a8b | |||
7d2842fd64 | |||
cd4c121e07 | |||
d0570f876e | |||
8bf99a1ab0 | |||
fdcd4ddd60 | |||
c09fff455f | |||
0b3755c69a | |||
e90fb64946 | |||
d542a4790e | |||
bc5cb4009c | |||
6724533d0e | |||
0f0668b77b | |||
266bf9b4cf | |||
a6f3bccf64 | |||
2d640f2e6a | |||
d7d99205a1 | |||
9f437d5b9f | |||
0d3100ba33 | |||
72fb69d87b | |||
ed4fcf5e9d | |||
8742c6e7b9 | |||
d7d7254a7b | |||
7e8870de6c | |||
8f2b2addc2 | |||
e4743bbdef | |||
80cdea6932 | |||
645f2c5c9c | |||
85b81ffc98 | |||
fa5536f504 | |||
16086e79b0 | |||
b001bba3b8 | |||
0c895a2662 | |||
6f0641f315 | |||
dc9dbe8a0f | |||
0b8096f973 | |||
d58a2a9975 | |||
a83268a6e3 | |||
5c83f234c6 | |||
24abec4045 | |||
56ff56281e | |||
c25f9ad9ae | |||
5041c90ac0 | |||
2855675fa5 | |||
209689c5f4 | |||
3d64b0aa28 | |||
3bceab0606 | |||
c189da3671 | |||
dd232cedb5 | |||
88c5daa561 | |||
4f281ef108 | |||
12aca7ca58 | |||
77ec1aa969 | |||
8710a5554c | |||
6b24d67409 | |||
48c3105f42 | |||
032453c4d0 | |||
f093868da1 | |||
1f5e38190d | |||
250884c7bc | |||
8a2e91e65e | |||
5910ce7980 | |||
00bec06012 | |||
54dccdbc7d | |||
2bd776ec55 | |||
23cf7c9e8b | |||
384f5de765 | |||
9ae4798d80 | |||
850ccbdcee | |||
d8ab3f2226 | |||
9ddd2dd3bc | |||
f579641866 | |||
a71c0c4e74 | |||
d3921f9e20 | |||
e0d7332dea | |||
d6b8eb8548 | |||
2964b6c6fa | |||
a0cd1074e1 | |||
cc2b5ef918 | |||
d003fdf357 | |||
5384faf3ec | |||
a833cd84f3 | |||
7f1b9d31ea | |||
5bd8c11a86 | |||
846d85bb7a | |||
b492c2d0fb | |||
1a6f5e061b | |||
5c62107e3b | |||
0891c5da62 | |||
2d22f0b2f2 | |||
1961e545c0 | |||
7951fcc494 | |||
6bf0b37694 | |||
7a51132e69 | |||
98f071df6d | |||
9543296ffd | |||
16dd545c22 | |||
e7cb818f05 | |||
ed89ade5e3 | |||
80d2eec5ed | |||
8d980b0287 | |||
|
baa199c50f | ||
|
29a0d2e357 | ||
|
7ab72668e1 | ||
ca3345cb33 | |||
0ade4b2efb | |||
2439a02dbb | |||
a785c71c5f | |||
db852cab68 | |||
6a5718c45e | |||
c68dbdb8fe | |||
49e0e2eb67 | |||
7d5b39f130 | |||
dd8c846b3e | |||
392b103f38 | |||
347c818ab6 | |||
9192b870b6 | |||
c21757694e | |||
770c7d0663 | |||
bd8c9d8cdc | |||
10a4435760 | |||
bc52c2c685 | |||
81c8b2a903 | |||
5ef10238e3 | |||
d2e8f809d0 | |||
8e550dc982 | |||
ed81ca957b | |||
f8ab8257e7 | |||
2474804258 | |||
e23dc1c063 | |||
9b28528acc | |||
86fd460a7a | |||
609b8c76b6 | |||
57aecc46be | |||
ded50480a8 | |||
4043a5c1a3 | |||
b96d405270 | |||
85751ba294 | |||
6145d9e804 | |||
fe1c05fe46 | |||
dc3f086b9d | |||
e778b8710d | |||
20be96253c | |||
e6129dd01d | |||
1ce0e8903f | |||
b67c1ab615 | |||
f044082fa5 | |||
b2a02c5a9c | |||
3946fecd1d | |||
27f43d0ad0 | |||
684b3e0838 | |||
adc66d8605 | |||
58b831cd24 | |||
8cf0502492 | |||
a490514079 | |||
a658286776 | |||
7fb3c26633 | |||
21ca8e5e90 | |||
f719cedc37 | |||
22e70f7164 | |||
a573a0b765 | |||
ca1abf951f | |||
2efa3c4a42 | |||
f3fd177235 | |||
092f98c17a | |||
eec6174562 | |||
81efcea0e5 | |||
7ac85b5b1e | |||
1b35ca32ac | |||
97c989e465 | |||
b43b81cc02 | |||
c061e3e1b2 | |||
cd61c47e35 | |||
4f9b3669a2 | |||
7164140c15 | |||
d41973f1a8 | |||
8806f2862d | |||
36989c76ee | |||
13aef5b3c0 | |||
b8f9f93537 | |||
1c93d28441 | |||
2ce351f7ef | |||
826dde759f | |||
d1aa966737 | |||
4d24e7095b | |||
6c1940f5d2 | |||
30c395151d | |||
d72e64c7f9 | |||
abdc8e5056 | |||
bc754c7a7d | |||
84ad8d43b5 | |||
e440630497 | |||
71689fce79 | |||
e7185ff460 | |||
18f493675a | |||
0c004b2e85 | |||
c214d9ee37 | |||
72259c16a9 | |||
66b656ada5 | |||
46e4ca3948 | |||
f2bf2fb025 | |||
50d48deec1 | |||
3c905aa1d7 |
15
.gitmodules
vendored
15
.gitmodules
vendored
@ -1,9 +1,18 @@
|
|||||||
[submodule "code/aoc-2020"]
|
[submodule "code/aoc-2020"]
|
||||||
path = code/aoc-2020
|
path = code/aoc-2020
|
||||||
url = https://dev.danilafe.com/Advent-of-Code/AdventOfCode-2020.git
|
url = https://dev.danilafe.com/Advent-of-Code/AdventOfCode-2020.git
|
||||||
[submodule "code/libabacus"]
|
|
||||||
path = code/libabacus
|
|
||||||
url = https://dev.danilafe.com/Experiments/libabacus
|
|
||||||
[submodule "themes/vanilla"]
|
[submodule "themes/vanilla"]
|
||||||
path = themes/vanilla
|
path = themes/vanilla
|
||||||
url = https://dev.danilafe.com/Web-Projects/vanilla-hugo.git
|
url = https://dev.danilafe.com/Web-Projects/vanilla-hugo.git
|
||||||
|
[submodule "code/server-config"]
|
||||||
|
path = code/server-config
|
||||||
|
url = https://dev.danilafe.com/Nix-Configs/server-config
|
||||||
|
[submodule "code/blog-static-flake"]
|
||||||
|
path = code/blog-static-flake
|
||||||
|
url = https://dev.danilafe.com/Nix-Configs/blog-static-flake.git
|
||||||
|
[submodule "code/compiler"]
|
||||||
|
path = code/compiler
|
||||||
|
url = https://dev.danilafe.com/DanilaFe/bloglang.git
|
||||||
|
[submodule "code/agda-spa"]
|
||||||
|
path = code/agda-spa
|
||||||
|
url = https://dev.danilafe.com/DanilaFe/agda-spa.git
|
||||||
|
9
Gemfile
Normal file
9
Gemfile
Normal file
@ -0,0 +1,9 @@
|
|||||||
|
# frozen_string_literal: true
|
||||||
|
|
||||||
|
source "https://rubygems.org"
|
||||||
|
|
||||||
|
git_source(:github) {|repo_name| "https://github.com/#{repo_name}" }
|
||||||
|
|
||||||
|
gem 'nokogiri'
|
||||||
|
gem 'execjs'
|
||||||
|
gem 'duktape'
|
21
Gemfile.lock
Normal file
21
Gemfile.lock
Normal file
@ -0,0 +1,21 @@
|
|||||||
|
GEM
|
||||||
|
remote: https://rubygems.org/
|
||||||
|
specs:
|
||||||
|
duktape (2.7.0.0)
|
||||||
|
execjs (2.9.1)
|
||||||
|
mini_portile2 (2.8.6)
|
||||||
|
nokogiri (1.15.6)
|
||||||
|
mini_portile2 (~> 2.8.2)
|
||||||
|
racc (~> 1.4)
|
||||||
|
racc (1.8.0)
|
||||||
|
|
||||||
|
PLATFORMS
|
||||||
|
ruby
|
||||||
|
|
||||||
|
DEPENDENCIES
|
||||||
|
duktape
|
||||||
|
execjs
|
||||||
|
nokogiri
|
||||||
|
|
||||||
|
BUNDLED WITH
|
||||||
|
2.1.4
|
351
agda.rb
Normal file
351
agda.rb
Normal file
@ -0,0 +1,351 @@
|
|||||||
|
require "nokogiri"
|
||||||
|
require "pathname"
|
||||||
|
|
||||||
|
files = ARGV[0..-1]
|
||||||
|
|
||||||
|
class LineInfo
|
||||||
|
attr_accessor :links
|
||||||
|
|
||||||
|
def initialize
|
||||||
|
@links = []
|
||||||
|
end
|
||||||
|
end
|
||||||
|
|
||||||
|
class AgdaContext
|
||||||
|
def initialize
|
||||||
|
@file_infos = {}
|
||||||
|
end
|
||||||
|
|
||||||
|
# Traverse the preformatted Agda block in the given Agda HTML file
|
||||||
|
# and find which textual ranges have IDs and links to other ranges.
|
||||||
|
# Store this information in a hash, line => LineInfo.
|
||||||
|
def process_agda_html_file(file)
|
||||||
|
return @file_infos[file] if @file_infos.include? file
|
||||||
|
|
||||||
|
@file_infos[file] = line_infos = {}
|
||||||
|
unless File.exists?(file)
|
||||||
|
return line_infos
|
||||||
|
end
|
||||||
|
|
||||||
|
document = Nokogiri::HTML.parse(File.open(file))
|
||||||
|
pre_code = document.css("pre.Agda")[0]
|
||||||
|
|
||||||
|
# The traversal postorder; we always visit children before their
|
||||||
|
# parents, and we visit leaves in sequence.
|
||||||
|
offset = 0
|
||||||
|
line = 1
|
||||||
|
pre_code.traverse do |at|
|
||||||
|
# Text nodes are always leaves; visiting a new leaf means we've advanced
|
||||||
|
# in the text by the length of that text. However, if there are newlines
|
||||||
|
# -- since this is a preformatted block -- we also advanced by a line.
|
||||||
|
# At this time, do not support links that span multiple lines, but
|
||||||
|
# Agda doesn't produce those either.
|
||||||
|
if at.text?
|
||||||
|
if at.content.include? "\n"
|
||||||
|
# This textual leaf is at least part whitespace. The logic
|
||||||
|
# assumes that links can't span multiple pages, and that links
|
||||||
|
# aren't nested, so ensure that the parent of the textual node
|
||||||
|
# is the preformatted block itself.
|
||||||
|
raise "unsupported Agda HTML output" if at.parent.name != "pre"
|
||||||
|
|
||||||
|
# Increase the line and track the final offset. Written as a loop
|
||||||
|
# in case we eventually want to add some handling for the pieces
|
||||||
|
# sandwiched between newlines.
|
||||||
|
at.content.split("\n", -1).each_with_index do |bit, idx|
|
||||||
|
line += 1 unless idx == 0
|
||||||
|
offset = bit.length
|
||||||
|
end
|
||||||
|
else
|
||||||
|
# It's not a newline node, so it could be anywhere. All we need to
|
||||||
|
# do is adjust the offset within the full pre block's text.
|
||||||
|
offset += at.content.length
|
||||||
|
end
|
||||||
|
elsif at.name == "a"
|
||||||
|
# We found a link. Agda emits both links and "things to link to" as
|
||||||
|
# 'a' nodes, so check for either, and record them. Even if
|
||||||
|
# the link is nested, the .content.length accessor will only
|
||||||
|
# retrieve the textual content, and thus -- assuming the link
|
||||||
|
# isn't split across lines -- will find the proper from-to range.
|
||||||
|
|
||||||
|
line_info = line_infos.fetch(line) { line_infos[line] = LineInfo.new }
|
||||||
|
href = at.attribute("href")
|
||||||
|
id = at.attribute("id")
|
||||||
|
if href or id
|
||||||
|
new_node = { :from => offset-at.content.length, :to => offset }
|
||||||
|
new_node[:href] = href if href
|
||||||
|
new_node[:id] = id if id
|
||||||
|
|
||||||
|
line_info.links << new_node
|
||||||
|
end
|
||||||
|
end
|
||||||
|
end
|
||||||
|
return line_infos
|
||||||
|
end
|
||||||
|
end
|
||||||
|
|
||||||
|
class FileGroup
|
||||||
|
def initialize(agda_context)
|
||||||
|
@agda_context = agda_context
|
||||||
|
# Agda HTML href -> list of (file, Hugo HTML node that links to it)
|
||||||
|
@nodes_referencing_href = {}
|
||||||
|
# Agda HTML href -> (its new ID in Hugo-land, file in which it's defined)
|
||||||
|
# This supports cross-post linking within a seires.
|
||||||
|
@global_seen_hrefs = {}
|
||||||
|
# file name -> Agda HTML href -> its new ID in Hugo-land
|
||||||
|
# This supports linking within a particular post.
|
||||||
|
@local_seen_hrefs = Hash.new { {} }
|
||||||
|
# Global counter to generate fresh IDs. There's no reason for it to
|
||||||
|
# be global within a series (since IDs are namespaced by the file they're in),
|
||||||
|
# but it's just more convenient this way.
|
||||||
|
@id_counter = 0
|
||||||
|
end
|
||||||
|
|
||||||
|
def note_defined_href(file, href)
|
||||||
|
file_hrefs = @local_seen_hrefs.fetch(file) do
|
||||||
|
@local_seen_hrefs[file] = {}
|
||||||
|
end
|
||||||
|
|
||||||
|
uniq_id = file_hrefs.fetch(href) do
|
||||||
|
new_id = "agda-unique-ident-#{@id_counter}"
|
||||||
|
@id_counter += 1
|
||||||
|
file_hrefs[href] = new_id
|
||||||
|
end
|
||||||
|
|
||||||
|
unless @global_seen_hrefs.include? href
|
||||||
|
@global_seen_hrefs[href] = { :file => file, :id => uniq_id }
|
||||||
|
end
|
||||||
|
|
||||||
|
return uniq_id
|
||||||
|
end
|
||||||
|
|
||||||
|
def note_used_href(file, node, href)
|
||||||
|
ref_list = @nodes_referencing_href.fetch(href) { @nodes_referencing_href[href] = [] }
|
||||||
|
ref_list << { :file => file, :node => node }
|
||||||
|
return href
|
||||||
|
end
|
||||||
|
|
||||||
|
# Given a Hugo HTML file which references potentially several Agda modules
|
||||||
|
# in code blocks, insert links into the code blocks.
|
||||||
|
#
|
||||||
|
# There are several things we need to take care of:
|
||||||
|
# 1. Finding the HTML files associated with each referenced Agda module.
|
||||||
|
# For this, we make use of the data-base-path etc. attributes that
|
||||||
|
# the vanilla theme inserts.
|
||||||
|
# 2. "zipping together" the Agda and Hugo HTML representations. Each of
|
||||||
|
# them encode the code, but they use different HTML elements and structures.
|
||||||
|
# So, given a Hugo HTML code block, traverse its textual contents
|
||||||
|
# and find any that are covered by links in the related Agda HTML file.
|
||||||
|
# 3. Fixing up links: the Agda HTML links assume each module has its own HTML
|
||||||
|
# file. This isn't true for us: multiple modules are stitched into
|
||||||
|
# one Hugo HTML file. Also, we don't include the entire Agda HTML
|
||||||
|
# file in the Hugo HTML, so some links may be broken. So, find IDs
|
||||||
|
# that are visible in the Hugo file, rename them to be globally unique,
|
||||||
|
# and re-write cross-file links that reference these IDs to point
|
||||||
|
# inside the Hugo file.
|
||||||
|
def process_source_file(file, document)
|
||||||
|
# Process each highlight group that's been marked as an Agda file.
|
||||||
|
document.css('div[data-agda-block]').each do |t|
|
||||||
|
first_line, last_line = nil, nil
|
||||||
|
|
||||||
|
if first_line_attr = t.attribute("data-first-line")
|
||||||
|
first_line = first_line_attr.to_s.to_i
|
||||||
|
end
|
||||||
|
if last_line_attr = t.attribute("data-last-line")
|
||||||
|
last_line = last_line_attr.to_s.to_i
|
||||||
|
end
|
||||||
|
|
||||||
|
if first_line and last_line
|
||||||
|
line_range = first_line..last_line
|
||||||
|
else
|
||||||
|
line_range = 1..
|
||||||
|
end
|
||||||
|
|
||||||
|
# Sometimes, code is deeply nested in the source file, but we don't
|
||||||
|
# want to show the leading space. In that case, the generator sets
|
||||||
|
# data-source-offset with how much leading space was stripped off.
|
||||||
|
initial_offset = 0
|
||||||
|
if source_offset_attr = t.attribute("data-source-offset")
|
||||||
|
initial_offset = source_offset_attr.to_s.to_i
|
||||||
|
end
|
||||||
|
|
||||||
|
full_path = t.attribute("data-file-path").to_s
|
||||||
|
full_path_dirs = Pathname(full_path).each_filename.to_a
|
||||||
|
|
||||||
|
# The name of an Agda module is determined from its directory
|
||||||
|
# structure: A/B/C.agda creates A.B.C.html. Depending on where
|
||||||
|
# the code is included, there might be some additional folders
|
||||||
|
# that precede A that we want to ignore.
|
||||||
|
base_path = t.attribute("data-base-path").to_s
|
||||||
|
base_dir_depth = 0
|
||||||
|
if base_path.empty?
|
||||||
|
# No submodules were used. Assume code/<X> is the root, since
|
||||||
|
# that's the code layout of the blog right now.
|
||||||
|
base_dir_depth = 1
|
||||||
|
base_path = full_path_dirs[0]
|
||||||
|
else
|
||||||
|
# The code is in a submodule. Assume that the base path / submodule
|
||||||
|
# root is the Agda module root, ignore all folders before that.
|
||||||
|
base_path_dirs = Pathname(base_path).each_filename.to_a
|
||||||
|
base_dir_depth = base_path_dirs.length
|
||||||
|
end
|
||||||
|
|
||||||
|
dirs_in_base = full_path_dirs[base_dir_depth..-1]
|
||||||
|
html_file = dirs_in_base.join(".").gsub(/\.agda$/, ".html")
|
||||||
|
html_path = File.join(["code", base_path, "html", html_file])
|
||||||
|
|
||||||
|
agda_info = @agda_context.process_agda_html_file(html_path)
|
||||||
|
|
||||||
|
# Hugo conveniently generates a bunch of spans, each encoding a line
|
||||||
|
# of code output. We can iterate over these and match them up with
|
||||||
|
# the line numbers we got from reading the Agda HTML output.
|
||||||
|
lines = t.css("pre.chroma code[data-lang] .line")
|
||||||
|
lines.zip(line_range).each do |line, line_no|
|
||||||
|
line_info = agda_info[line_no]
|
||||||
|
next unless line_info
|
||||||
|
|
||||||
|
offset = initial_offset
|
||||||
|
line.traverse do |lt|
|
||||||
|
if lt.text?
|
||||||
|
content = lt.content
|
||||||
|
new_offset = offset + content.length
|
||||||
|
|
||||||
|
# The span/a/etc. structure of the Agda and Hugo HTML files
|
||||||
|
# need not line up; it's possible for there to be a single link
|
||||||
|
# in the Agda file that's broken up across multiple HTML nodes
|
||||||
|
# in the Hugo output. For now, just don't link those, since inserting
|
||||||
|
# such overlapping links is relatively complicated. Instead,
|
||||||
|
# require links to fit fully within a current text node (and thus,
|
||||||
|
# not overlap the boundaries of any HTML).
|
||||||
|
matching_links = line_info.links.filter do |link|
|
||||||
|
link[:from] >= offset and link[:to] <= new_offset
|
||||||
|
end
|
||||||
|
|
||||||
|
# A given text node can be broken into any number of sub-nodes,
|
||||||
|
# where some sub-nodes are still text, and others have been turned
|
||||||
|
# into links. Store the new pieces in replace_with. E.g.,
|
||||||
|
#
|
||||||
|
# Original:
|
||||||
|
# abc
|
||||||
|
#
|
||||||
|
# New:
|
||||||
|
# a<a href="..">b</a>c
|
||||||
|
#
|
||||||
|
# replace_with:
|
||||||
|
# ["a", <Nokogiri::XML::Node...>, "c"]
|
||||||
|
#
|
||||||
|
# match_offset represents how much of the original text we've
|
||||||
|
# already converted. The below iteration assumes that matching
|
||||||
|
# links are in order, and don't overlap.
|
||||||
|
replace_with = []
|
||||||
|
replace_offset = 0
|
||||||
|
matching_links.each do |match|
|
||||||
|
# The link's range is an offset from the beginning of the line,
|
||||||
|
# but the text piece we're splitting up might be partway into
|
||||||
|
# the line. Convert the link coordinates to piece-relative ones.
|
||||||
|
relative_from = match[:from] - offset
|
||||||
|
relative_to = match[:to] - offset
|
||||||
|
|
||||||
|
# If the previous link ended some time before the new link
|
||||||
|
# began (or if the current link is the first one, and is not
|
||||||
|
# at the beginning), ensure that the plain text "in between"
|
||||||
|
# is kept.
|
||||||
|
replace_with << content[replace_offset...relative_from]
|
||||||
|
|
||||||
|
tag = (match.include? :href) ? 'a' : 'span'
|
||||||
|
new_node = Nokogiri::XML::Node.new(tag, document)
|
||||||
|
if match.include? :href
|
||||||
|
# For nodes with links, note what they're referring to, so
|
||||||
|
# we can adjust their hrefs when we assign global IDs.
|
||||||
|
href = match[:href].to_s
|
||||||
|
new_node['href'] = note_used_href file, new_node, href
|
||||||
|
end
|
||||||
|
if match.include? :id
|
||||||
|
# For nodes with IDs visible in the current Hugo file, we'll
|
||||||
|
# want to redirect links that previously go to other Agda
|
||||||
|
# module HTML files. So, note the ID that we want to redirect,
|
||||||
|
# and pick a new unique ID to replace it with.
|
||||||
|
id = match[:id].to_s
|
||||||
|
new_node['id'] = note_defined_href file, "#{html_file}##{id}"
|
||||||
|
end
|
||||||
|
new_node.content = content[relative_from...relative_to]
|
||||||
|
|
||||||
|
replace_with << new_node
|
||||||
|
replace_offset = relative_to
|
||||||
|
end
|
||||||
|
replace_with << content[replace_offset..-1]
|
||||||
|
|
||||||
|
# Finally, replace the node under consideration with the new
|
||||||
|
# pieces.
|
||||||
|
replace_with.each do |replacement|
|
||||||
|
lt.add_previous_sibling replacement
|
||||||
|
end
|
||||||
|
lt.remove
|
||||||
|
|
||||||
|
offset = new_offset
|
||||||
|
end
|
||||||
|
end
|
||||||
|
end
|
||||||
|
end
|
||||||
|
end
|
||||||
|
|
||||||
|
def cross_link_files
|
||||||
|
# Now, we have a complete list of all the IDs visible in scope.
|
||||||
|
# Redirect relevant links to these IDs. This achieves within-post
|
||||||
|
# links.
|
||||||
|
@nodes_referencing_href.each do |href, references|
|
||||||
|
references.each do |reference|
|
||||||
|
file = reference[:file]
|
||||||
|
node = reference[:node]
|
||||||
|
|
||||||
|
local_targets = @local_seen_hrefs[file]
|
||||||
|
if local_targets.include? href
|
||||||
|
# A code block in this fine provides this href, create a local link.
|
||||||
|
node['href'] = "##{local_targets[href]}"
|
||||||
|
elsif @global_seen_hrefs.include? href
|
||||||
|
# A code block in this series, but not in this file, defines
|
||||||
|
# this href. Create a cross-file link.
|
||||||
|
target = @global_seen_hrefs[href]
|
||||||
|
other_file = target[:file]
|
||||||
|
id = target[:id]
|
||||||
|
|
||||||
|
relpath = Pathname.new(other_file).dirname.relative_path_from(Pathname.new(file).dirname)
|
||||||
|
node['href'] = "#{relpath}##{id}"
|
||||||
|
else
|
||||||
|
# No definitions in any blog page. For now, just delete the anchor.
|
||||||
|
node.replace node.content
|
||||||
|
end
|
||||||
|
end
|
||||||
|
end
|
||||||
|
end
|
||||||
|
end
|
||||||
|
|
||||||
|
agda_context = AgdaContext.new
|
||||||
|
|
||||||
|
file_documents = {}
|
||||||
|
series_groups = files.group_by do |file|
|
||||||
|
file_documents[file] = document = Nokogiri::HTML.parse(File.open(file))
|
||||||
|
document.css("meta[name=blog-series]")&.attribute("content")&.to_s
|
||||||
|
end
|
||||||
|
|
||||||
|
# For the 'nil' group, process individually.
|
||||||
|
if files_with_no_series = series_groups.delete(nil)
|
||||||
|
files_with_no_series.each do |file|
|
||||||
|
file_group = FileGroup.new agda_context
|
||||||
|
file_group.process_source_file file, file_documents[file]
|
||||||
|
file_group.cross_link_files
|
||||||
|
end
|
||||||
|
end
|
||||||
|
|
||||||
|
# For groups, process them together to allow cross-linking
|
||||||
|
series_groups.each do |_, files_in_series|
|
||||||
|
file_group = FileGroup.new agda_context
|
||||||
|
files_in_series.each do |file|
|
||||||
|
file_group.process_source_file file, file_documents[file]
|
||||||
|
end
|
||||||
|
file_group.cross_link_files
|
||||||
|
end
|
||||||
|
|
||||||
|
# Having modified all the HTML files, save them.
|
||||||
|
file_documents.each do |file, document|
|
||||||
|
File.write(file, document.to_html(encoding: 'UTF-8'))
|
||||||
|
end
|
110
analyze.rb
Normal file
110
analyze.rb
Normal file
@ -0,0 +1,110 @@
|
|||||||
|
require "pathname"
|
||||||
|
require "set"
|
||||||
|
require "json"
|
||||||
|
|
||||||
|
def resolve_path(bp, p)
|
||||||
|
path = nil
|
||||||
|
if bp.start_with? "."
|
||||||
|
path = Pathname.new(File.join(bp, p)).cleanpath.to_s
|
||||||
|
elsif p.start_with? "blog/"
|
||||||
|
path = File.join("content", p)
|
||||||
|
else
|
||||||
|
path = File.join("content", "blog", p)
|
||||||
|
end
|
||||||
|
if File.directory? path
|
||||||
|
path = File.join(path, "index.md")
|
||||||
|
elsif !path.end_with? ".md"
|
||||||
|
path += ".md"
|
||||||
|
end
|
||||||
|
path.gsub("blog/blog/", "blog/")
|
||||||
|
end
|
||||||
|
|
||||||
|
files = Set.new
|
||||||
|
refs = {}
|
||||||
|
Dir['content/blog/**/*.md'].each do |file|
|
||||||
|
file = file.chomp
|
||||||
|
files << file
|
||||||
|
arr = refs[file] || (refs[file] = [])
|
||||||
|
pattern = Regexp.union(/< relref "([^"]+)" >/, /< draftlink "[^"]+" "([^"]+)" >/)
|
||||||
|
File.open(file).read.scan(pattern) do |ref|
|
||||||
|
ref = resolve_path(File.dirname(file), ref[0] || ref[1])
|
||||||
|
arr << ref
|
||||||
|
files << ref
|
||||||
|
end
|
||||||
|
arr.uniq!
|
||||||
|
end
|
||||||
|
|
||||||
|
data = {}
|
||||||
|
id = 0
|
||||||
|
series = {}
|
||||||
|
files.each do |file|
|
||||||
|
id += 1
|
||||||
|
name = file
|
||||||
|
tags = []
|
||||||
|
group = 1
|
||||||
|
draft = false
|
||||||
|
next unless File.exists?(file)
|
||||||
|
value = File.size(file)
|
||||||
|
url = file.gsub(/^content/, "https://danilafe.com").delete_suffix("/index.md").delete_suffix(".md")
|
||||||
|
File.readlines(file).each do |l|
|
||||||
|
if l =~ /^title: (.+)$/
|
||||||
|
name = $~[1].delete_prefix('"').delete_suffix('"')
|
||||||
|
elsif l =~ /^draft: true$/
|
||||||
|
draft = true
|
||||||
|
elsif l =~ /^series: (.+)$/
|
||||||
|
this_series = $~[1]
|
||||||
|
series_list = series.fetch(this_series) do
|
||||||
|
series[this_series] = []
|
||||||
|
end
|
||||||
|
series_list << file
|
||||||
|
elsif l =~ /^tags: (.+)$/
|
||||||
|
tags = $~[1].delete_prefix("[").delete_suffix("]").split(/,\s?/).map { |it| it.gsub('"', '') }
|
||||||
|
if tags.include? "Compilers"
|
||||||
|
group = 2
|
||||||
|
elsif tags.include? "Coq"
|
||||||
|
group = 3
|
||||||
|
elsif tags.include? "Programming Languages"
|
||||||
|
group = 4
|
||||||
|
elsif tags.include? "Haskell"
|
||||||
|
group = 5
|
||||||
|
elsif tags.include? "Crystal"
|
||||||
|
group = 6
|
||||||
|
elsif tags.include? "Agda"
|
||||||
|
group = 7
|
||||||
|
elsif tags.include? "Hugo"
|
||||||
|
group = 8
|
||||||
|
end
|
||||||
|
end
|
||||||
|
end
|
||||||
|
next if draft
|
||||||
|
data[file] = { :id => id, :name => name, :group => group, :tags => tags, :url => url, :value => value }
|
||||||
|
end
|
||||||
|
|
||||||
|
edges = []
|
||||||
|
files.each do |file1|
|
||||||
|
# files.each do |file2|
|
||||||
|
# next if file1 == file2
|
||||||
|
# next unless data[file1][:tags].any? { |t| data[file2][:tags].include? t }
|
||||||
|
# edges << { :from => data[file1][:id], :to => data[file2][:id] }
|
||||||
|
# end
|
||||||
|
next unless frefs = refs[file1]
|
||||||
|
frefs.each do |ref|
|
||||||
|
next unless data[file1]
|
||||||
|
next unless data[ref]
|
||||||
|
edges << { :from => data[file1][:id], :to => data[ref][:id] }
|
||||||
|
end
|
||||||
|
end
|
||||||
|
series.each do |series, files|
|
||||||
|
files.sort.each_cons(2) do |file1, file2|
|
||||||
|
next unless data[file1]
|
||||||
|
next unless data[file2]
|
||||||
|
edges << { :from => data[file1][:id], :to => data[file2][:id] }
|
||||||
|
edges << { :from => data[file2][:id], :to => data[file1][:id] }
|
||||||
|
end
|
||||||
|
end
|
||||||
|
edges.uniq!
|
||||||
|
# edges.filter! { |e| e[:from] < e[:to] }
|
||||||
|
edges.map! { |e| { :from => [e[:from], e[:to]].min, :to => [e[:from], e[:to]].max } }.uniq!
|
||||||
|
|
||||||
|
puts ("export const nodes = " + JSON.pretty_unparse(data.values) + ";")
|
||||||
|
puts ("export const edges = " + JSON.pretty_unparse(edges) + ";")
|
65
assets/bergamot/rendering/imp.bergamot
Normal file
65
assets/bergamot/rendering/imp.bergamot
Normal file
@ -0,0 +1,65 @@
|
|||||||
|
LatexListNil @ latexlist(nil, nil) <-;
|
||||||
|
LatexListCons @ latexlist(cons(?x, ?xs), cons(?l_x, ?l_s)) <- latex(?x, ?l_x), latexlist(?xs, ?l_s);
|
||||||
|
|
||||||
|
IntercalateNil @ intercalate(?sep, nil, nil) <-;
|
||||||
|
IntercalateConsCons @ intercalate(?sep, cons(?x_1, cons(?x_2, ?xs)), cons(?x_1, cons(?sep, ?ys))) <- intercalate(?sep, cons(?x_2, ?xs), ?ys);
|
||||||
|
IntercalateConsNil @ intercalate(?sep, cons(?x, nil), cons(?x, nil)) <-;
|
||||||
|
|
||||||
|
NonEmpty @ nonempty(cons(?x, ?xs)) <-;
|
||||||
|
|
||||||
|
InListHere @ inlist(?e, cons(?e, ?es)) <-;
|
||||||
|
InListThere @ inlist(?e_1, cons(?e_2, ?es)) <- inlist(?e_1, ?es);
|
||||||
|
|
||||||
|
BasicParenLit @ paren(lit(?v), ?l) <- latex(lit(?v), ?l);
|
||||||
|
BasicParenVar @ paren(var(?x), ?l) <- latex(var(?x), ?l);
|
||||||
|
BasicParenVar @ paren(metavariable(?x), ?l) <- latex(metavariable(?x), ?l);
|
||||||
|
BasicParenOther @ paren(?t, ?l) <- latex(?t, ?l_t), join(["(", ?l_t, ")"], ?l);
|
||||||
|
|
||||||
|
LatexInt @ latex(?i, ?l) <- int(?i), tostring(?i, ?l);
|
||||||
|
LatexFloat @ latex(?f, ?l) <- float(?f), tostring(?f, ?l);
|
||||||
|
LatexStr @ latex(?s, ?l) <- str(?s), escapestring(?s, ?l_1), latexifystring(?s, ?l_2), join(["\\texttt{\"", ?l_2, "\"}"], ?l);
|
||||||
|
LatexMeta @ latex(metavariable(?l), ?l) <-;
|
||||||
|
LatexLit @ latex(lit(?i), ?l) <- latex(?i, ?l);
|
||||||
|
LatexVar @ latex(var(metavariable(?s)), ?l) <- latex(metavariable(?s), ?l);
|
||||||
|
LatexVar @ latex(var(?s), ?l) <- latex(?s, ?l_v), join(["\\texttt{", ?l_v, "}"], ?l);
|
||||||
|
LatexPlus @ latex(plus(?e_1, ?e_2), ?l) <-
|
||||||
|
paren(?e_1, ?l_1), paren(?e_2, ?l_2),
|
||||||
|
join([?l_1, " + ", ?l_2], ?l);
|
||||||
|
LatexMinus @ latex(minus(?e_1, ?e_2), ?l) <-
|
||||||
|
paren(?e_1, ?l_1), paren(?e_2, ?l_2),
|
||||||
|
join([?l_1, " - ", ?l_2], ?l);
|
||||||
|
|
||||||
|
EnvLiteralNil @ envlitrec(empty, "\\{", "", ?seen) <-;
|
||||||
|
EnvLiteralSingle @ envlitsingle(?pre, ?e, ?v, "", ?pre, ?seen) <- inlist(?e, ?seen);
|
||||||
|
EnvLiteralSingle @ envlitsingle(?pre, ?e, ?v, ?l, ", ", ?seen) <- latex(?e, ?l_e), latex(?v, ?l_v), join([?pre, "\\texttt{", ?l_e, "} \\mapsto", ?l_v], ?l);
|
||||||
|
EnvLiteralCons @ envlitrec(extend(empty, ?e, ?v), ?l, ?newnext, ?seen) <- envlitrec(?rho, ?l_rho, ?next, cons(?e, ?seen)), envlitsingle(?next, ?e, ?v, ?l_v, ?newnext, ?seen), join([?l_rho, ?l_v], ?l);
|
||||||
|
EnvLiteralCons @ envlitrec(extend(?rho, ?e, ?v), ?l, ?newnext, ?seen) <- envlitrec(?rho, ?l_rho, ?next, cons(?e, ?seen)), envlitsingle(?next, ?e, ?v, ?l_v, ?newnext, ?seen), join([?l_rho, ?l_v], ?l);
|
||||||
|
EnvLiteralOuter @ envlit(?rho, ?l) <- envlitrec(?rho, ?l_rho, ?rest, []), join([?l_rho, "\\}"], ?l);
|
||||||
|
|
||||||
|
LatexEnvLit @ latex(?rho, ?l) <- envlit(?rho, ?l);
|
||||||
|
LatexTypeEmpty @ latex(empty, "\\{\\}") <-;
|
||||||
|
LatexExtend @ latex(extend(?a, ?b, ?c), ?l) <- latex(?a, ?l_a), latex(?b, ?l_b), latex(?c, ?l_c), join([?l_a, "[", ?l_b, " \\mapsto ", ?l_c, "]"], ?l);
|
||||||
|
LatexInenv @ latex(inenv(?x, ?v, ?G), ?l) <-latex(?x, ?l_x), latex(?v, ?l_v), latex(?G, ?l_G), join([?l_G, "(", ?l_x, ") = ", ?l_v], ?l);
|
||||||
|
LatexEvalTer @ latex(eval(?G, ?e, ?t), ?l) <- latex(?G, ?l_G), latex(?e, ?l_e), latex(?t, ?l_t), join([?l_G, ",\\ ", ?l_e, " \\Downarrow ", ?l_t], ?l);
|
||||||
|
|
||||||
|
LatexAdd @ latex(add(?a, ?b, ?c), ?l) <- latex(?a, ?l_a), latex(?b, ?l_b), latex(?c, ?l_c), join([?l_a, "+", ?l_b, "=", ?l_c], ?l);
|
||||||
|
LatexSubtract @ latex(subtract(?a, ?b, ?c), ?l) <- latex(?a, ?l_a), latex(?b, ?l_b), latex(?c, ?l_c), join([?l_a, "-", ?l_b, "=", ?l_c], ?l);
|
||||||
|
LatexEvalTer @ latex(stepbasic(?G, ?e, ?H), ?l) <- latex(?G, ?l_G), latex(?e, ?l_e), latex(?H, ?l_H), join([?l_G, ",\\ ", ?l_e, " \\Rightarrow ", ?l_H], ?l);
|
||||||
|
LatexEvalTer @ latex(step(?G, ?e, ?H), ?l) <- latex(?G, ?l_G), latex(?e, ?l_e), latex(?H, ?l_H), join([?l_G, ",\\ ", ?l_e, " \\Rightarrow ", ?l_H], ?l);
|
||||||
|
|
||||||
|
LatexNoop @ latex(noop, "\\texttt{noop}") <-;
|
||||||
|
LatexAssign @ latex(assign(?x, ?e), ?l) <- latex(?x, ?l_x), latex(?e, ?l_e), join([?l_x, " = ", ?l_e], ?l);
|
||||||
|
LatexAssign @ latex(if(?e, ?s_1, ?s_2), ?l) <- latex(?e, ?l_e), latex(?s_1, ?l_1), latex(?s_2, ?l_2), join(["\\textbf{if}\\ ", ?l_e, "\\ \\{\\ ", ?l_1, "\\ \\}\\ \\textbf{else}\\ \\{\\ ", ?l_2, "\\ \\}"], ?l);
|
||||||
|
LatexAssign @ latex(while(?e, ?s), ?l) <- latex(?e, ?l_e), latex(?s, ?l_s), join(["\\textbf{while}\\ ", ?l_e, "\\ \\{\\ ", ?l_s, "\\ \\}"], ?l);
|
||||||
|
LatexAssign @ latex(seq(?s_1, ?s_2), ?l) <- latex(?s_1, ?l_1), latex(?s_2, ?l_2), join([?l_1, "; ", ?l_2], ?l);
|
||||||
|
|
||||||
|
LatexNumNeq @ latex(not(eq(?e_1, ?e_2)), ?l) <- latex(?e_1, ?l_1), latex(?e_2, ?l_2), join([?l_1, " \\neq ", ?l_2], ?l);
|
||||||
|
LatexNot @ latex(not(?e), ?l) <- latex(?e, ?l_e), join(["\\neg (", ?l_e, ")"], ?l);
|
||||||
|
LatexNumEq @ latex(eq(?e_1, ?e_2), ?l) <- latex(?e_1, ?l_1), latex(?e_2, ?l_2), join([?l_1, " = ", ?l_2], ?l);
|
||||||
|
|
||||||
|
LatexIsInt @ latex(int(?e), ?l) <- latex(?e, ?l_e), join([?l_e, " \\in \\texttt{Int}"], ?l);
|
||||||
|
LatexIsFloat @ latex(float(?e), ?l) <- latex(?e, ?l_e), join([?l_e, " \\in \\texttt{Float}"], ?l);
|
||||||
|
LatexIsNum @ latex(num(?e), ?l) <- latex(?e, ?l_e), join([?l_e, " \\in \\texttt{Num}"], ?l);
|
||||||
|
LatexIsStr @ latex(str(?e), ?l) <- latex(?e, ?l_e), join([?l_e, " \\in \\texttt{Str}"], ?l);
|
||||||
|
LatexSym @ latex(?s, ?l) <- sym(?s), tostring(?s, ?l_1), join(["\\text{", ?l_1,"}"], ?l);
|
||||||
|
LatexCall @ latex(?c, ?l) <- call(?c, ?n, ?ts), nonempty(?ts), latexlist(?ts, ?lts_1), intercalate(", ", ?lts_1, ?lts_2), join(?lts_2, ?lts_3), join(["\\text{", ?n, "}", "(", ?lts_3, ")"], ?l);
|
74
assets/bergamot/rendering/lc.bergamot
Normal file
74
assets/bergamot/rendering/lc.bergamot
Normal file
@ -0,0 +1,74 @@
|
|||||||
|
PrecApp @ prec(app(?l, ?r), 100, left) <-;
|
||||||
|
PrecPlus @ prec(plus(?l, ?r), 80, either) <-;
|
||||||
|
PrecAbs @ prec(abs(?x, ?t, ?e), 0, right) <-;
|
||||||
|
PrecArr @ prec(tarr(?l, ?r), 0, right) <-;
|
||||||
|
|
||||||
|
SelectHead @ select(cons([?t, ?v], ?rest), ?default, ?v) <- ?t;
|
||||||
|
SelectTail @ select(cons([?t, ?v], ?rest), ?default, ?found) <- not(?t), select(?rest, ?default, ?found);
|
||||||
|
SelectEmpty @ select(nil, ?default, ?default) <-;
|
||||||
|
|
||||||
|
Eq @ eq(?x, ?x) <-;
|
||||||
|
|
||||||
|
ParenthAssocLeft @ parenthassoc(?a_i, left, right) <-;
|
||||||
|
ParenthAssocRight @ parenthassoc(?a_i, right, left) <-;
|
||||||
|
ParenthAssocNone @ parenthassoc(?a_i, none, ?pos) <-;
|
||||||
|
ParenthAssocNeq @ parenthassoc(?a_i, ?a_o, ?pos) <- not(eq(?a_i, ?a_o));
|
||||||
|
|
||||||
|
Parenth @ parenth(?inner, ?outer, ?pos, ?strin, ?strout) <-
|
||||||
|
prec(?inner, ?p_i, ?a_i), prec(?outer, ?p_o, ?a_o),
|
||||||
|
join(["(", ?strin, ")"], ?strinparen),
|
||||||
|
select([ [less(?p_i, ?p_o), strinparen], [less(?p_o, ?p_i), ?strin], [ parenthassoc(?a_i, ?a_o, ?pos), ?strinparen ] ], ?strin, ?strout);
|
||||||
|
ParenthFallback @ parenth(?inner, ?outer, ?pos, ?strin, ?strin) <-;
|
||||||
|
|
||||||
|
LatexListNil @ latexlist(nil, nil) <-;
|
||||||
|
LatexListCons @ latexlist(cons(?x, ?xs), cons(?l_x, ?l_s)) <- latex(?x, ?l_x), latexlist(?xs, ?l_s);
|
||||||
|
|
||||||
|
IntercalateNil @ intercalate(?sep, nil, nil) <-;
|
||||||
|
IntercalateConsCons @ intercalate(?sep, cons(?x_1, cons(?x_2, ?xs)), cons(?x_1, cons(?sep, ?ys))) <- intercalate(?sep, cons(?x_2, ?xs), ?ys);
|
||||||
|
IntercalateConsNil @ intercalate(?sep, cons(?x, nil), cons(?x, nil)) <-;
|
||||||
|
|
||||||
|
NonEmpty @ nonempty(cons(?x, ?xs)) <-;
|
||||||
|
|
||||||
|
LatexInt @ latex(?i, ?l) <- int(?i), tostring(?i, ?l);
|
||||||
|
LatexFloat @ latex(?f, ?l) <- float(?f), tostring(?f, ?l);
|
||||||
|
LatexStr @ latex(?s, ?l) <- str(?s), escapestring(?s, ?l_1), latexifystring(?s, ?l_2), join(["\\texttt{\"", ?l_2, "\"}"], ?l);
|
||||||
|
LatexMeta @ latex(metavariable(?l), ?l) <-;
|
||||||
|
LatexLit @ latex(lit(?i), ?l) <- latex(?i, ?l);
|
||||||
|
LatexVar @ latex(var(?s), ?l) <- latex(?s, ?l);
|
||||||
|
LatexPlus @ latex(plus(?e_1, ?e_2), ?l) <-
|
||||||
|
latex(?e_1, ?l_1), latex(?e_2, ?l_2),
|
||||||
|
parenth(?e_1, plus(?e_1, ?e_2), left, ?l_1, ?lp_1),
|
||||||
|
parenth(?e_2, plus(?e_1, ?e_2), right, ?l_2, ?lp_2),
|
||||||
|
join([?lp_1, " + ", ?lp_2], ?l);
|
||||||
|
LatexPair @ latex(pair(?e_1, ?e_2), ?l) <- latex(?e_1, ?l_1), latex(?e_2, ?l_2), join(["(", ?l_1, ", ", ?l_2, ")"], ?l);
|
||||||
|
LatexAbs @ latex(abs(?x, ?t, ?e), ?l) <- latex(?e, ?l_e), latex(?t, ?l_t), latex(?x, ?l_x), join(["\\lambda ", ?l_x, " : ", ?l_t, " . ", ?l_e], ?l);
|
||||||
|
LatexApp @ latex(app(?e_1, ?e_2), ?l) <-
|
||||||
|
latex(?e_1, ?l_1), latex(?e_2, ?l_2),
|
||||||
|
parenth(?e_1, app(?e_1, ?e_2), left, ?l_1, ?lp_1),
|
||||||
|
parenth(?e_2, app(?e_1, ?e_2), right, ?l_2, ?lp_2),
|
||||||
|
join([?lp_1, " \\enspace ", ?lp_2], ?l);
|
||||||
|
|
||||||
|
LatexTInt @ latex(tint, "\\text{tint}") <-;
|
||||||
|
LatexTStr @ latex(tstr, "\\text{tstr}") <-;
|
||||||
|
LatexTArr @ latex(tarr(?t_1, ?t_2), ?l) <-
|
||||||
|
latex(?t_1, ?l_1), latex(?t_2, ?l_2),
|
||||||
|
parenth(?t_1, tarr(?t_1, ?t_2), left, ?l_1, ?lp_1),
|
||||||
|
parenth(?t_2, tarr(?t_1, ?t_2), right, ?l_2, ?lp_2),
|
||||||
|
join([?lp_1, " \\to ", ?lp_2], ?l);
|
||||||
|
LatexTPair @ latex(tpair(?t_1, ?t_2), ?l) <- latex(?t_1, ?l_1), latex(?t_2, ?l_2), join(["(", ?l_1, ", ", ?l_2, ")"], ?l);
|
||||||
|
|
||||||
|
LatexTypeEmpty @ latex(empty, "\\varnothing") <-;
|
||||||
|
LatexTypeExtend @ latex(extend(?a, ?b, ?c), ?l) <- latex(?a, ?l_a), latex(?b, ?l_b), latex(?c, ?l_c), join([?l_a, " , ", ?l_b, " : ", ?l_c], ?l);
|
||||||
|
LatexTypeInenv @ latex(inenv(?x, ?t, ?G), ?l) <-latex(?x, ?l_x), latex(?t, ?l_t), latex(?G, ?l_G), join([?l_x, " : ", ?l_t, " \\in ", ?l_G], ?l);
|
||||||
|
|
||||||
|
LatexTypeBin @ latex(type(?e, ?t), ?l) <- latex(?e, ?l_e), latex(?t, ?l_t), join([?l_e, " : ", ?l_t], ?l);
|
||||||
|
LatexTypeTer @ latex(type(?G, ?e, ?t), ?l) <- latex(?G, ?l_G), latex(?e, ?l_e), latex(?t, ?l_t), join([?l_G, " \\vdash ", ?l_e, " : ", ?l_t], ?l);
|
||||||
|
|
||||||
|
LatexConverts @ latex(converts(?f, ?t), ?l) <- latex(?f, ?l_f), latex(?t, ?l_t), join([?l_f, " \\preceq ", ?l_t], ?l);
|
||||||
|
|
||||||
|
LatexIsInt @ latex(int(?e), ?l) <- latex(?e, ?l_e), join([?l_e, " \\in \\texttt{Int}"], ?l);
|
||||||
|
LatexIsFloat @ latex(float(?e), ?l) <- latex(?e, ?l_e), join([?l_e, " \\in \\texttt{Float}"], ?l);
|
||||||
|
LatexIsNum @ latex(num(?e), ?l) <- latex(?e, ?l_e), join([?l_e, " \\in \\texttt{Num}"], ?l);
|
||||||
|
LatexIsStr @ latex(str(?e), ?l) <- latex(?e, ?l_e), join([?l_e, " \\in \\texttt{Str}"], ?l);
|
||||||
|
LatexSym @ latex(?s, ?l) <- sym(?s), tostring(?s, ?l_1), join(["\\text{", ?l_1,"}"], ?l);
|
||||||
|
LatexCall @ latex(?c, ?l) <- call(?c, ?n, ?ts), nonempty(?ts), latexlist(?ts, ?lts_1), intercalate(", ", ?lts_1, ?lts_2), join(?lts_2, ?lts_3), join(["\\text{", ?n, "}", "(", ?lts_3, ")"], ?l);
|
174
assets/scss/bergamot.scss
Normal file
174
assets/scss/bergamot.scss
Normal file
@ -0,0 +1,174 @@
|
|||||||
|
@import "variables.scss";
|
||||||
|
@import "mixins.scss";
|
||||||
|
|
||||||
|
.bergamot-exercise {
|
||||||
|
counter-increment: bergamot-exercise;
|
||||||
|
|
||||||
|
.bergamot-root {
|
||||||
|
border: none;
|
||||||
|
padding: 0;
|
||||||
|
margin-top: 1em;
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
.bergamot-exercise-label {
|
||||||
|
.bergamot-exercise-number::after {
|
||||||
|
content: "Exercise " counter(bergamot-exercise);
|
||||||
|
font-weight: bold;
|
||||||
|
text-decoration: underline;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
.bergamot-button {
|
||||||
|
@include bordered-block;
|
||||||
|
padding: 0.25em;
|
||||||
|
padding-left: 1em;
|
||||||
|
padding-right: 1em;
|
||||||
|
background-color: inherit;
|
||||||
|
display: inline-flex;
|
||||||
|
align-items: center;
|
||||||
|
justify-content: center;
|
||||||
|
transition: 0.25s;
|
||||||
|
font-family: $font-body;
|
||||||
|
@include var(color, text-color);
|
||||||
|
|
||||||
|
&.bergamot-hidden {
|
||||||
|
display: none;
|
||||||
|
}
|
||||||
|
|
||||||
|
.feather {
|
||||||
|
margin-right: 0.5em;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
.bergamot-play {
|
||||||
|
.feather { color: $primary-color; }
|
||||||
|
&:hover, &:focus {
|
||||||
|
.feather { color: lighten($primary-color, 20%); }
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
.bergamot-reset {
|
||||||
|
.feather { color: #0099CC; }
|
||||||
|
&:hover, &:focus {
|
||||||
|
.feather { color: lighten(#0099CC, 20%); }
|
||||||
|
}
|
||||||
|
|
||||||
|
svg {
|
||||||
|
fill: none;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
.bergamot-close {
|
||||||
|
.feather { color: tomato; }
|
||||||
|
&:hover, &:focus {
|
||||||
|
.feather { color: lighten(tomato, 20%); }
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
.bergamot-button-group {
|
||||||
|
margin-top: 1em;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
.bergamot-root {
|
||||||
|
@include bordered-block;
|
||||||
|
padding: 1em;
|
||||||
|
|
||||||
|
.bergamot-section-heading {
|
||||||
|
margin-bottom: 0.5em;
|
||||||
|
font-family: $font-body;
|
||||||
|
font-style: normal;
|
||||||
|
font-weight: bold;
|
||||||
|
font-size: 1.25em;
|
||||||
|
}
|
||||||
|
|
||||||
|
.bergamot-section {
|
||||||
|
margin-bottom: 1em;
|
||||||
|
}
|
||||||
|
|
||||||
|
textarea {
|
||||||
|
display: block;
|
||||||
|
width: 100%;
|
||||||
|
height: 10em;
|
||||||
|
resize: none;
|
||||||
|
}
|
||||||
|
|
||||||
|
input[type="text"] {
|
||||||
|
width: 100%;
|
||||||
|
@include textual-input;
|
||||||
|
}
|
||||||
|
|
||||||
|
.bergamot-rule-list {
|
||||||
|
display: flex;
|
||||||
|
flex-direction: row;
|
||||||
|
flex-wrap: wrap;
|
||||||
|
justify-content: center;
|
||||||
|
}
|
||||||
|
|
||||||
|
.bergamot-rule-list katex-expression {
|
||||||
|
margin-left: .5em;
|
||||||
|
margin-right: .5em;
|
||||||
|
flex-grow: 1;
|
||||||
|
flex-basis: 0;
|
||||||
|
}
|
||||||
|
|
||||||
|
.bergamot-rule-section {
|
||||||
|
.bergamot-rule-section-name {
|
||||||
|
text-align: center;
|
||||||
|
margin: 0.25em;
|
||||||
|
font-weight: bold;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
.bergamot-proof-tree {
|
||||||
|
overflow: auto;
|
||||||
|
}
|
||||||
|
|
||||||
|
.bergamot-error {
|
||||||
|
@include bordered-block;
|
||||||
|
padding: 0.5rem;
|
||||||
|
border-color: tomato;
|
||||||
|
background-color: rgba(tomato, 0.25);
|
||||||
|
margin-top: 1rem;
|
||||||
|
}
|
||||||
|
|
||||||
|
.bergamot-selector {
|
||||||
|
button {
|
||||||
|
@include var(background-color, background-color);
|
||||||
|
@include var(color, text-color);
|
||||||
|
@include bordered-block;
|
||||||
|
padding: 0.5rem;
|
||||||
|
font-family: $font-body;
|
||||||
|
border-style: dotted;
|
||||||
|
|
||||||
|
&.active {
|
||||||
|
border-color: $primary-color;
|
||||||
|
border-style: solid;
|
||||||
|
font-weight: bold;
|
||||||
|
}
|
||||||
|
|
||||||
|
&:not(:first-child) {
|
||||||
|
border-bottom-left-radius: 0;
|
||||||
|
border-top-left-radius: 0;
|
||||||
|
}
|
||||||
|
|
||||||
|
&:not(:last-child) {
|
||||||
|
border-bottom-right-radius: 0;
|
||||||
|
border-top-right-radius: 0;
|
||||||
|
border-right-width: 0;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
button.active + button {
|
||||||
|
border-left-color: $primary-color;
|
||||||
|
border-left-style: solid;
|
||||||
|
}
|
||||||
|
|
||||||
|
margin-bottom: 1rem;
|
||||||
|
}
|
||||||
|
|
||||||
|
.bergamot-no-proofs {
|
||||||
|
text-align: center;
|
||||||
|
}
|
||||||
|
}
|
@ -17,12 +17,32 @@
|
|||||||
border-bottom-right-radius: 0;
|
border-bottom-right-radius: 0;
|
||||||
padding-left: 0.5em;
|
padding-left: 0.5em;
|
||||||
padding-right: 0.5rem;
|
padding-right: 0.5rem;
|
||||||
|
|
||||||
|
@include below-container-width {
|
||||||
|
@include bordered-block;
|
||||||
|
text-align: center;
|
||||||
|
border-bottom: none;
|
||||||
|
border-bottom-left-radius: 0;
|
||||||
|
border-bottom-right-radius: 0;
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
&:last-child {
|
&:last-child {
|
||||||
@include bordered-block;
|
@include bordered-block;
|
||||||
border-top-left-radius: 0;
|
border-top-left-radius: 0;
|
||||||
border-bottom-left-radius: 0;
|
border-bottom-left-radius: 0;
|
||||||
|
|
||||||
|
@include below-container-width {
|
||||||
|
@include bordered-block;
|
||||||
|
border-top-left-radius: 0;
|
||||||
|
border-top-right-radius: 0;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
tr {
|
||||||
|
@include below-container-width {
|
||||||
|
margin-bottom: 0.5rem;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
430
assets/scss/thevoid.scss
Normal file
430
assets/scss/thevoid.scss
Normal file
@ -0,0 +1,430 @@
|
|||||||
|
@import "variables.scss";
|
||||||
|
|
||||||
|
body {
|
||||||
|
background-color: #1c1e26;
|
||||||
|
--text-color: white;
|
||||||
|
font-family: $font-code;
|
||||||
|
}
|
||||||
|
|
||||||
|
h1, h2, h3, h4, h5, h6 {
|
||||||
|
text-align: left;
|
||||||
|
font-family: $font-code;
|
||||||
|
}
|
||||||
|
|
||||||
|
h1::after {
|
||||||
|
content: "(writing)";
|
||||||
|
font-size: 1rem;
|
||||||
|
margin-left: 0.5em;
|
||||||
|
position: relative;
|
||||||
|
bottom: -0.5em;
|
||||||
|
color: $primary-color;
|
||||||
|
}
|
||||||
|
|
||||||
|
nav .container {
|
||||||
|
justify-content: flex-start;
|
||||||
|
|
||||||
|
a {
|
||||||
|
padding-left: 0;
|
||||||
|
margin-right: 1em;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
.header-divider {
|
||||||
|
visibility: hidden;
|
||||||
|
}
|
||||||
|
|
||||||
|
hr {
|
||||||
|
height: auto;
|
||||||
|
border: none;
|
||||||
|
|
||||||
|
&::after {
|
||||||
|
content: "* * *";
|
||||||
|
color: $primary-color;
|
||||||
|
font-size: 2rem;
|
||||||
|
display: block;
|
||||||
|
text-align: center;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
/* Code for the CSS glitch effect. Originally from: https://codepen.io/mattgrosswork/pen/VwprebG */
|
||||||
|
|
||||||
|
.glitch {
|
||||||
|
position: relative;
|
||||||
|
|
||||||
|
span {
|
||||||
|
animation: paths 5s step-end infinite;
|
||||||
|
font-weight: bold;
|
||||||
|
}
|
||||||
|
|
||||||
|
&::before, &::after {
|
||||||
|
content: attr(data-text);
|
||||||
|
position: absolute;
|
||||||
|
width: 110%;
|
||||||
|
z-index: -1;
|
||||||
|
}
|
||||||
|
|
||||||
|
&::before {
|
||||||
|
top: 10px;
|
||||||
|
left: 15px;
|
||||||
|
color: #e0287d;
|
||||||
|
|
||||||
|
animation: paths 5s step-end infinite, opacity 5s step-end infinite,
|
||||||
|
font 8s step-end infinite, movement 10s step-end infinite;
|
||||||
|
}
|
||||||
|
|
||||||
|
&::after {
|
||||||
|
top: 5px;
|
||||||
|
left: -10px;
|
||||||
|
color: #1bc7fb;
|
||||||
|
|
||||||
|
animation: paths 5s step-end infinite, opacity 5s step-end infinite,
|
||||||
|
font 7s step-end infinite, movement 8s step-end infinite;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
@keyframes paths {
|
||||||
|
0% {
|
||||||
|
clip-path: polygon(
|
||||||
|
0% 43%,
|
||||||
|
83% 43%,
|
||||||
|
83% 22%,
|
||||||
|
23% 22%,
|
||||||
|
23% 24%,
|
||||||
|
91% 24%,
|
||||||
|
91% 26%,
|
||||||
|
18% 26%,
|
||||||
|
18% 83%,
|
||||||
|
29% 83%,
|
||||||
|
29% 17%,
|
||||||
|
41% 17%,
|
||||||
|
41% 39%,
|
||||||
|
18% 39%,
|
||||||
|
18% 82%,
|
||||||
|
54% 82%,
|
||||||
|
54% 88%,
|
||||||
|
19% 88%,
|
||||||
|
19% 4%,
|
||||||
|
39% 4%,
|
||||||
|
39% 14%,
|
||||||
|
76% 14%,
|
||||||
|
76% 52%,
|
||||||
|
23% 52%,
|
||||||
|
23% 35%,
|
||||||
|
19% 35%,
|
||||||
|
19% 8%,
|
||||||
|
36% 8%,
|
||||||
|
36% 31%,
|
||||||
|
73% 31%,
|
||||||
|
73% 16%,
|
||||||
|
1% 16%,
|
||||||
|
1% 56%,
|
||||||
|
50% 56%,
|
||||||
|
50% 8%
|
||||||
|
);
|
||||||
|
}
|
||||||
|
|
||||||
|
5% {
|
||||||
|
clip-path: polygon(
|
||||||
|
0% 29%,
|
||||||
|
44% 29%,
|
||||||
|
44% 83%,
|
||||||
|
94% 83%,
|
||||||
|
94% 56%,
|
||||||
|
11% 56%,
|
||||||
|
11% 64%,
|
||||||
|
94% 64%,
|
||||||
|
94% 70%,
|
||||||
|
88% 70%,
|
||||||
|
88% 32%,
|
||||||
|
18% 32%,
|
||||||
|
18% 96%,
|
||||||
|
10% 96%,
|
||||||
|
10% 62%,
|
||||||
|
9% 62%,
|
||||||
|
9% 84%,
|
||||||
|
68% 84%,
|
||||||
|
68% 50%,
|
||||||
|
52% 50%,
|
||||||
|
52% 55%,
|
||||||
|
35% 55%,
|
||||||
|
35% 87%,
|
||||||
|
25% 87%,
|
||||||
|
25% 39%,
|
||||||
|
15% 39%,
|
||||||
|
15% 88%,
|
||||||
|
52% 88%
|
||||||
|
);
|
||||||
|
}
|
||||||
|
|
||||||
|
30% {
|
||||||
|
clip-path: polygon(
|
||||||
|
0% 53%,
|
||||||
|
93% 53%,
|
||||||
|
93% 62%,
|
||||||
|
68% 62%,
|
||||||
|
68% 37%,
|
||||||
|
97% 37%,
|
||||||
|
97% 89%,
|
||||||
|
13% 89%,
|
||||||
|
13% 45%,
|
||||||
|
51% 45%,
|
||||||
|
51% 88%,
|
||||||
|
17% 88%,
|
||||||
|
17% 54%,
|
||||||
|
81% 54%,
|
||||||
|
81% 75%,
|
||||||
|
79% 75%,
|
||||||
|
79% 76%,
|
||||||
|
38% 76%,
|
||||||
|
38% 28%,
|
||||||
|
61% 28%,
|
||||||
|
61% 12%,
|
||||||
|
55% 12%,
|
||||||
|
55% 62%,
|
||||||
|
68% 62%,
|
||||||
|
68% 51%,
|
||||||
|
0% 51%,
|
||||||
|
0% 92%,
|
||||||
|
63% 92%,
|
||||||
|
63% 4%,
|
||||||
|
65% 4%
|
||||||
|
);
|
||||||
|
}
|
||||||
|
|
||||||
|
45% {
|
||||||
|
clip-path: polygon(
|
||||||
|
0% 33%,
|
||||||
|
2% 33%,
|
||||||
|
2% 69%,
|
||||||
|
58% 69%,
|
||||||
|
58% 94%,
|
||||||
|
55% 94%,
|
||||||
|
55% 25%,
|
||||||
|
33% 25%,
|
||||||
|
33% 85%,
|
||||||
|
16% 85%,
|
||||||
|
16% 19%,
|
||||||
|
5% 19%,
|
||||||
|
5% 20%,
|
||||||
|
79% 20%,
|
||||||
|
79% 96%,
|
||||||
|
93% 96%,
|
||||||
|
93% 50%,
|
||||||
|
5% 50%,
|
||||||
|
5% 74%,
|
||||||
|
55% 74%,
|
||||||
|
55% 57%,
|
||||||
|
96% 57%,
|
||||||
|
96% 59%,
|
||||||
|
87% 59%,
|
||||||
|
87% 65%,
|
||||||
|
82% 65%,
|
||||||
|
82% 39%,
|
||||||
|
63% 39%,
|
||||||
|
63% 92%,
|
||||||
|
4% 92%,
|
||||||
|
4% 36%,
|
||||||
|
24% 36%,
|
||||||
|
24% 70%,
|
||||||
|
1% 70%,
|
||||||
|
1% 43%,
|
||||||
|
15% 43%,
|
||||||
|
15% 28%,
|
||||||
|
23% 28%,
|
||||||
|
23% 71%,
|
||||||
|
90% 71%,
|
||||||
|
90% 86%,
|
||||||
|
97% 86%,
|
||||||
|
97% 1%,
|
||||||
|
60% 1%,
|
||||||
|
60% 67%,
|
||||||
|
71% 67%,
|
||||||
|
71% 91%,
|
||||||
|
17% 91%,
|
||||||
|
17% 14%,
|
||||||
|
39% 14%,
|
||||||
|
39% 30%,
|
||||||
|
58% 30%,
|
||||||
|
58% 11%,
|
||||||
|
52% 11%,
|
||||||
|
52% 83%,
|
||||||
|
68% 83%
|
||||||
|
);
|
||||||
|
}
|
||||||
|
|
||||||
|
76% {
|
||||||
|
clip-path: polygon(
|
||||||
|
0% 26%,
|
||||||
|
15% 26%,
|
||||||
|
15% 73%,
|
||||||
|
72% 73%,
|
||||||
|
72% 70%,
|
||||||
|
77% 70%,
|
||||||
|
77% 75%,
|
||||||
|
8% 75%,
|
||||||
|
8% 42%,
|
||||||
|
4% 42%,
|
||||||
|
4% 61%,
|
||||||
|
17% 61%,
|
||||||
|
17% 12%,
|
||||||
|
26% 12%,
|
||||||
|
26% 63%,
|
||||||
|
73% 63%,
|
||||||
|
73% 43%,
|
||||||
|
90% 43%,
|
||||||
|
90% 67%,
|
||||||
|
50% 67%,
|
||||||
|
50% 41%,
|
||||||
|
42% 41%,
|
||||||
|
42% 46%,
|
||||||
|
50% 46%,
|
||||||
|
50% 84%,
|
||||||
|
96% 84%,
|
||||||
|
96% 78%,
|
||||||
|
49% 78%,
|
||||||
|
49% 25%,
|
||||||
|
63% 25%,
|
||||||
|
63% 14%
|
||||||
|
);
|
||||||
|
}
|
||||||
|
|
||||||
|
90% {
|
||||||
|
clip-path: polygon(
|
||||||
|
0% 41%,
|
||||||
|
13% 41%,
|
||||||
|
13% 6%,
|
||||||
|
87% 6%,
|
||||||
|
87% 93%,
|
||||||
|
10% 93%,
|
||||||
|
10% 13%,
|
||||||
|
89% 13%,
|
||||||
|
89% 6%,
|
||||||
|
3% 6%,
|
||||||
|
3% 8%,
|
||||||
|
16% 8%,
|
||||||
|
16% 79%,
|
||||||
|
0% 79%,
|
||||||
|
0% 99%,
|
||||||
|
92% 99%,
|
||||||
|
92% 90%,
|
||||||
|
5% 90%,
|
||||||
|
5% 60%,
|
||||||
|
0% 60%,
|
||||||
|
0% 48%,
|
||||||
|
89% 48%,
|
||||||
|
89% 13%,
|
||||||
|
80% 13%,
|
||||||
|
80% 43%,
|
||||||
|
95% 43%,
|
||||||
|
95% 19%,
|
||||||
|
80% 19%,
|
||||||
|
80% 85%,
|
||||||
|
38% 85%,
|
||||||
|
38% 62%
|
||||||
|
);
|
||||||
|
}
|
||||||
|
|
||||||
|
1%,
|
||||||
|
7%,
|
||||||
|
33%,
|
||||||
|
47%,
|
||||||
|
78%,
|
||||||
|
93% {
|
||||||
|
clip-path: none;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
@keyframes movement {
|
||||||
|
0% {
|
||||||
|
top: 0px;
|
||||||
|
left: -20px;
|
||||||
|
}
|
||||||
|
|
||||||
|
15% {
|
||||||
|
top: 10px;
|
||||||
|
left: 10px;
|
||||||
|
}
|
||||||
|
|
||||||
|
60% {
|
||||||
|
top: 5px;
|
||||||
|
left: -10px;
|
||||||
|
}
|
||||||
|
|
||||||
|
75% {
|
||||||
|
top: -5px;
|
||||||
|
left: 20px;
|
||||||
|
}
|
||||||
|
|
||||||
|
100% {
|
||||||
|
top: 10px;
|
||||||
|
left: 5px;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
@keyframes opacity {
|
||||||
|
0% {
|
||||||
|
opacity: 0.1;
|
||||||
|
}
|
||||||
|
|
||||||
|
5% {
|
||||||
|
opacity: 0.7;
|
||||||
|
}
|
||||||
|
|
||||||
|
30% {
|
||||||
|
opacity: 0.4;
|
||||||
|
}
|
||||||
|
|
||||||
|
45% {
|
||||||
|
opacity: 0.6;
|
||||||
|
}
|
||||||
|
|
||||||
|
76% {
|
||||||
|
opacity: 0.4;
|
||||||
|
}
|
||||||
|
|
||||||
|
90% {
|
||||||
|
opacity: 0.8;
|
||||||
|
}
|
||||||
|
|
||||||
|
1%,
|
||||||
|
7%,
|
||||||
|
33%,
|
||||||
|
47%,
|
||||||
|
78%,
|
||||||
|
93% {
|
||||||
|
opacity: 0;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
@keyframes font {
|
||||||
|
0% {
|
||||||
|
font-weight: 100;
|
||||||
|
color: #e0287d;
|
||||||
|
filter: blur(3px);
|
||||||
|
}
|
||||||
|
|
||||||
|
20% {
|
||||||
|
font-weight: 500;
|
||||||
|
color: #fff;
|
||||||
|
filter: blur(0);
|
||||||
|
}
|
||||||
|
|
||||||
|
50% {
|
||||||
|
font-weight: 300;
|
||||||
|
color: #1bc7fb;
|
||||||
|
filter: blur(2px);
|
||||||
|
}
|
||||||
|
|
||||||
|
60% {
|
||||||
|
font-weight: 700;
|
||||||
|
color: #fff;
|
||||||
|
filter: blur(0);
|
||||||
|
}
|
||||||
|
|
||||||
|
90% {
|
||||||
|
font-weight: 500;
|
||||||
|
color: #e0287d;
|
||||||
|
filter: blur(6px);
|
||||||
|
}
|
||||||
|
}
|
70
build-agda-html.rb
Normal file
70
build-agda-html.rb
Normal file
@ -0,0 +1,70 @@
|
|||||||
|
require "json"
|
||||||
|
require "set"
|
||||||
|
require "optparse"
|
||||||
|
require "fileutils"
|
||||||
|
|
||||||
|
# For target_dir, use absolute paths because when invoking Agda, we'll be
|
||||||
|
# using chdir.
|
||||||
|
root_path = "code"
|
||||||
|
target_dir = File.expand_path "code"
|
||||||
|
data_file = "data/submodules.json"
|
||||||
|
OptionParser.new do |opts|
|
||||||
|
opts.banner = "Usage: build-agda-html.rb [options]"
|
||||||
|
|
||||||
|
opts.on("--root-path=PATH", "Search for Agda project folders in the given location") do |f|
|
||||||
|
root_path = f
|
||||||
|
end
|
||||||
|
opts.on("--target-dir=PATH", "Generate HTML files into the given directory") do |f|
|
||||||
|
target_dir = File.expand_path f
|
||||||
|
end
|
||||||
|
opts.on("--data-file=FILE", "Specify the submodules.json that encodes nested submodule structure") do |f|
|
||||||
|
data_file = f
|
||||||
|
end
|
||||||
|
end.parse!
|
||||||
|
files = ARGV
|
||||||
|
|
||||||
|
code_paths = Dir.entries(root_path).select do |f|
|
||||||
|
File.directory?(File.join(root_path, f)) and f != '.' and f != '..'
|
||||||
|
end.to_set
|
||||||
|
code_paths += JSON.parse(File.read(data_file)).keys if File.exists? 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
|
87
code/agda-issomething/example.agda
Normal file
87
code/agda-issomething/example.agda
Normal file
@ -0,0 +1,87 @@
|
|||||||
|
open import Agda.Primitive using (Level; lsuc)
|
||||||
|
open import Relation.Binary.PropositionalEquality using (_≡_)
|
||||||
|
|
||||||
|
variable
|
||||||
|
a : Level
|
||||||
|
A : Set a
|
||||||
|
|
||||||
|
module FirstAttempt where
|
||||||
|
record Semigroup (A : Set a) : Set a where
|
||||||
|
field
|
||||||
|
_∙_ : A → A → A
|
||||||
|
|
||||||
|
isAssociative : ∀ (a₁ a₂ a₃ : A) → a₁ ∙ (a₂ ∙ a₃) ≡ (a₁ ∙ a₂) ∙ a₃
|
||||||
|
|
||||||
|
record Monoid (A : Set a) : Set a where
|
||||||
|
field semigroup : Semigroup A
|
||||||
|
|
||||||
|
open Semigroup semigroup public
|
||||||
|
|
||||||
|
field
|
||||||
|
zero : A
|
||||||
|
|
||||||
|
isIdentityLeft : ∀ (a : A) → zero ∙ a ≡ a
|
||||||
|
isIdentityRight : ∀ (a : A) → a ∙ zero ≡ a
|
||||||
|
|
||||||
|
record ContrivedExample (A : Set a) : Set a where
|
||||||
|
field
|
||||||
|
-- first property
|
||||||
|
monoid : Monoid A
|
||||||
|
|
||||||
|
-- second property; Semigroup is a stand-in.
|
||||||
|
semigroup : Semigroup A
|
||||||
|
|
||||||
|
operationsEqual : Monoid._∙_ monoid ≡ Semigroup._∙_ semigroup
|
||||||
|
|
||||||
|
module SecondAttempt where
|
||||||
|
record IsSemigroup {A : Set a} (_∙_ : A → A → A) : Set a where
|
||||||
|
field isAssociative : ∀ (a₁ a₂ a₃ : A) → a₁ ∙ (a₂ ∙ a₃) ≡ (a₁ ∙ a₂) ∙ a₃
|
||||||
|
|
||||||
|
record IsMonoid {A : Set a} (zero : A) (_∙_ : A → A → A) : Set a where
|
||||||
|
field
|
||||||
|
isSemigroup : IsSemigroup _∙_
|
||||||
|
|
||||||
|
isIdentityLeft : ∀ (a : A) → zero ∙ a ≡ a
|
||||||
|
isIdentityRight : ∀ (a : A) → a ∙ zero ≡ a
|
||||||
|
|
||||||
|
open IsSemigroup isSemigroup public
|
||||||
|
|
||||||
|
record IsContrivedExample {A : Set a} (zero : A) (_∙_ : A → A → A) : Set a where
|
||||||
|
field
|
||||||
|
-- first property
|
||||||
|
monoid : IsMonoid zero _∙_
|
||||||
|
|
||||||
|
-- second property; Semigroup is a stand-in.
|
||||||
|
semigroup : IsSemigroup _∙_
|
||||||
|
|
||||||
|
record Semigroup (A : Set a) : Set a where
|
||||||
|
field
|
||||||
|
_∙_ : A → A → A
|
||||||
|
isSemigroup : IsSemigroup _∙_
|
||||||
|
|
||||||
|
record Monoid (A : Set a) : Set a where
|
||||||
|
field
|
||||||
|
zero : A
|
||||||
|
_∙_ : A → A → A
|
||||||
|
isMonoid : IsMonoid zero _∙_
|
||||||
|
|
||||||
|
module ThirdAttempt {A : Set a} (_∙_ : A → A → A) where
|
||||||
|
record IsSemigroup : Set a where
|
||||||
|
field isAssociative : ∀ (a₁ a₂ a₃ : A) → a₁ ∙ (a₂ ∙ a₃) ≡ (a₁ ∙ a₂) ∙ a₃
|
||||||
|
|
||||||
|
record IsMonoid (zero : A) : Set a where
|
||||||
|
field
|
||||||
|
isSemigroup : IsSemigroup
|
||||||
|
|
||||||
|
isIdentityLeft : ∀ (a : A) → zero ∙ a ≡ a
|
||||||
|
isIdentityRight : ∀ (a : A) → a ∙ zero ≡ a
|
||||||
|
|
||||||
|
open IsSemigroup isSemigroup public
|
||||||
|
|
||||||
|
record IsContrivedExample (zero : A) : Set a where
|
||||||
|
field
|
||||||
|
-- first property
|
||||||
|
monoid : IsMonoid zero
|
||||||
|
|
||||||
|
-- second property; Semigroup is a stand-in.
|
||||||
|
semigroup : IsSemigroup
|
1
code/agda-spa
Submodule
1
code/agda-spa
Submodule
@ -0,0 +1 @@
|
|||||||
|
Subproject commit 913121488069a20cdfd40777a8777eb3744c415e
|
1
code/blog-static-flake
Submodule
1
code/blog-static-flake
Submodule
@ -0,0 +1 @@
|
|||||||
|
Subproject commit 67b47d9c298e7476c2ca211aac5c5fd961637b7b
|
112
code/catamorphisms/Cata.hs
Normal file
112
code/catamorphisms/Cata.hs
Normal file
@ -0,0 +1,112 @@
|
|||||||
|
{-# LANGUAGE LambdaCase, DeriveFunctor, DeriveFoldable, MultiParamTypeClasses #-}
|
||||||
|
import Prelude hiding (length, sum, fix)
|
||||||
|
|
||||||
|
length :: [a] -> Int
|
||||||
|
length [] = 0
|
||||||
|
length (_:xs) = 1 + length xs
|
||||||
|
|
||||||
|
lengthF :: ([a] -> Int) -> [a] -> Int
|
||||||
|
lengthF rec [] = 0
|
||||||
|
lengthF rec (_:xs) = 1 + rec xs
|
||||||
|
|
||||||
|
lengthF' = \rec -> \case
|
||||||
|
[] -> 0
|
||||||
|
_:xs -> 1 + rec xs
|
||||||
|
|
||||||
|
fix f = let x = f x in x
|
||||||
|
|
||||||
|
length' = fix lengthF
|
||||||
|
|
||||||
|
data MyList = MyNil | MyCons Int MyList
|
||||||
|
data MyListF a = MyNilF | MyConsF Int a
|
||||||
|
|
||||||
|
newtype Fix f = Fix { unFix :: f (Fix f) }
|
||||||
|
|
||||||
|
testList :: Fix MyListF
|
||||||
|
testList = Fix (MyConsF 1 (Fix (MyConsF 2 (Fix (MyConsF 3 (Fix MyNilF))))))
|
||||||
|
|
||||||
|
myOut :: MyList -> MyListF MyList
|
||||||
|
myOut MyNil = MyNilF
|
||||||
|
myOut (MyCons i xs) = MyConsF i xs
|
||||||
|
|
||||||
|
myIn :: MyListF MyList -> MyList
|
||||||
|
myIn MyNilF = MyNil
|
||||||
|
myIn (MyConsF i xs) = MyCons i xs
|
||||||
|
|
||||||
|
instance Functor MyListF where
|
||||||
|
fmap f MyNilF = MyNilF
|
||||||
|
fmap f (MyConsF i a) = MyConsF i (f a)
|
||||||
|
|
||||||
|
mySumF :: MyListF Int -> Int
|
||||||
|
mySumF MyNilF = 0
|
||||||
|
mySumF (MyConsF i rest) = i + rest
|
||||||
|
|
||||||
|
mySum :: MyList -> Int
|
||||||
|
mySum = mySumF . fmap mySum . myOut
|
||||||
|
|
||||||
|
myCata :: (MyListF a -> a) -> MyList -> a
|
||||||
|
myCata f = f . fmap (myCata f) . myOut
|
||||||
|
|
||||||
|
myLength = myCata $ \case
|
||||||
|
MyNilF -> 0
|
||||||
|
MyConsF _ l -> 1 + l
|
||||||
|
|
||||||
|
myMax = myCata $ \case
|
||||||
|
MyNilF -> 0
|
||||||
|
MyConsF x y -> max x y
|
||||||
|
|
||||||
|
myMin = myCata $ \case
|
||||||
|
MyNilF -> 0
|
||||||
|
MyConsF x y -> min x y
|
||||||
|
|
||||||
|
myTestList = MyCons 2 (MyCons 1 (MyCons 3 MyNil))
|
||||||
|
|
||||||
|
pack :: a -> (Int -> a -> a) -> MyListF a -> a
|
||||||
|
pack b f MyNilF = b
|
||||||
|
pack b f (MyConsF x y) = f x y
|
||||||
|
|
||||||
|
unpack :: (MyListF a -> a) -> (a, Int -> a -> a)
|
||||||
|
unpack f = (f MyNilF, \i a -> f (MyConsF i a))
|
||||||
|
|
||||||
|
class Functor f => Cata a f where
|
||||||
|
out :: a -> f a
|
||||||
|
|
||||||
|
cata :: Cata a f => (f b -> b) -> a -> b
|
||||||
|
cata f = f . fmap (cata f) . out
|
||||||
|
|
||||||
|
instance Cata MyList MyListF where
|
||||||
|
out = myOut
|
||||||
|
|
||||||
|
data ListF a b = Nil | Cons a b deriving Functor
|
||||||
|
|
||||||
|
instance Cata [a] (ListF a) where
|
||||||
|
out [] = Nil
|
||||||
|
out (x:xs) = Cons x xs
|
||||||
|
|
||||||
|
sum :: Num a => [a] -> a
|
||||||
|
sum = cata $ \case
|
||||||
|
Nil -> 0
|
||||||
|
Cons x xs -> x + xs
|
||||||
|
|
||||||
|
data BinaryTree a = Node a (BinaryTree a) (BinaryTree a) | Leaf deriving (Show, Foldable)
|
||||||
|
data BinaryTreeF a b = NodeF a b b | LeafF deriving Functor
|
||||||
|
|
||||||
|
instance Cata (BinaryTree a) (BinaryTreeF a) where
|
||||||
|
out (Node a l r) = NodeF a l r
|
||||||
|
out Leaf = LeafF
|
||||||
|
|
||||||
|
invert :: BinaryTree a -> BinaryTree a
|
||||||
|
invert = cata $ \case
|
||||||
|
LeafF -> Leaf
|
||||||
|
NodeF a l r -> Node a r l
|
||||||
|
|
||||||
|
data MaybeF a b = NothingF | JustF a deriving Functor
|
||||||
|
|
||||||
|
instance Cata (Maybe a) (MaybeF a) where
|
||||||
|
out Nothing = NothingF
|
||||||
|
out (Just x) = JustF x
|
||||||
|
|
||||||
|
getOrDefault :: a -> Maybe a -> a
|
||||||
|
getOrDefault d = cata $ \case
|
||||||
|
NothingF -> d
|
||||||
|
JustF a -> a
|
1
code/compiler
Submodule
1
code/compiler
Submodule
@ -0,0 +1 @@
|
|||||||
|
Subproject commit 137455b0f4365ba3fd11c45ce49781cdbe829ec3
|
@ -1,33 +0,0 @@
|
|||||||
%option noyywrap
|
|
||||||
|
|
||||||
%{
|
|
||||||
#include <iostream>
|
|
||||||
%}
|
|
||||||
|
|
||||||
%%
|
|
||||||
|
|
||||||
[ \n]+ {}
|
|
||||||
\+ { std::cout << "PLUS" << std::endl; }
|
|
||||||
\* { std::cout << "TIMES" << std::endl; }
|
|
||||||
- { std::cout << "MINUS" << std::endl; }
|
|
||||||
\/ { std::cout << "DIVIDE" << std::endl; }
|
|
||||||
[0-9]+ { std::cout << "NUMBER: " << yytext << std::endl; }
|
|
||||||
defn { std::cout << "KEYWORD: defn" << std::endl; }
|
|
||||||
data { std::cout << "KEYWORD: data" << std::endl; }
|
|
||||||
case { std::cout << "KEYWORD: case" << std::endl; }
|
|
||||||
of { std::cout << "KEYWORD: of" << std::endl; }
|
|
||||||
\{ { std::cout << "OPEN CURLY" << std::endl; }
|
|
||||||
\} { std::cout << "CLOSED CURLY" << std::endl; }
|
|
||||||
\( { std::cout << "OPEN PARENTH" << std::endl; }
|
|
||||||
\) { std::cout << "CLOSE PARENTH" << std::endl; }
|
|
||||||
, { std::cout << "COMMA" << std::endl; }
|
|
||||||
-> { std::cout << "PATTERN ARROW" << std::endl; }
|
|
||||||
= { std::cout << "EQUAL" << std::endl; }
|
|
||||||
[a-z][a-zA-Z]* { std::cout << "LOWERCASE IDENTIFIER: " << yytext << std::endl; }
|
|
||||||
[A-Z][a-zA-Z]* { std::cout << "UPPERCASE IDENTIFIER: " << yytext << std::endl; }
|
|
||||||
|
|
||||||
%%
|
|
||||||
|
|
||||||
int main() {
|
|
||||||
yylex();
|
|
||||||
}
|
|
@ -1,128 +0,0 @@
|
|||||||
#pragma once
|
|
||||||
#include <memory>
|
|
||||||
#include <vector>
|
|
||||||
|
|
||||||
struct ast {
|
|
||||||
virtual ~ast() = default;
|
|
||||||
};
|
|
||||||
|
|
||||||
using ast_ptr = std::unique_ptr<ast>;
|
|
||||||
|
|
||||||
struct pattern {
|
|
||||||
virtual ~pattern() = default;
|
|
||||||
};
|
|
||||||
|
|
||||||
using pattern_ptr = std::unique_ptr<pattern>;
|
|
||||||
|
|
||||||
struct branch {
|
|
||||||
pattern_ptr pat;
|
|
||||||
ast_ptr expr;
|
|
||||||
|
|
||||||
branch(pattern_ptr p, ast_ptr a)
|
|
||||||
: pat(std::move(p)), expr(std::move(a)) {}
|
|
||||||
};
|
|
||||||
|
|
||||||
using branch_ptr = std::unique_ptr<branch>;
|
|
||||||
|
|
||||||
struct constructor {
|
|
||||||
std::string name;
|
|
||||||
std::vector<std::string> types;
|
|
||||||
|
|
||||||
constructor(std::string n, std::vector<std::string> ts)
|
|
||||||
: name(std::move(n)), types(std::move(ts)) {}
|
|
||||||
};
|
|
||||||
|
|
||||||
using constructor_ptr = std::unique_ptr<constructor>;
|
|
||||||
|
|
||||||
struct definition {
|
|
||||||
virtual ~definition() = default;
|
|
||||||
};
|
|
||||||
|
|
||||||
using definition_ptr = std::unique_ptr<definition>;
|
|
||||||
|
|
||||||
enum binop {
|
|
||||||
PLUS,
|
|
||||||
MINUS,
|
|
||||||
TIMES,
|
|
||||||
DIVIDE
|
|
||||||
};
|
|
||||||
|
|
||||||
struct ast_int : public ast {
|
|
||||||
int value;
|
|
||||||
|
|
||||||
explicit ast_int(int v)
|
|
||||||
: value(v) {}
|
|
||||||
};
|
|
||||||
|
|
||||||
struct ast_lid : public ast {
|
|
||||||
std::string id;
|
|
||||||
|
|
||||||
explicit ast_lid(std::string i)
|
|
||||||
: id(std::move(i)) {}
|
|
||||||
};
|
|
||||||
|
|
||||||
struct ast_uid : public ast {
|
|
||||||
std::string id;
|
|
||||||
|
|
||||||
explicit ast_uid(std::string i)
|
|
||||||
: id(std::move(i)) {}
|
|
||||||
};
|
|
||||||
|
|
||||||
struct ast_binop : public ast {
|
|
||||||
binop op;
|
|
||||||
ast_ptr left;
|
|
||||||
ast_ptr right;
|
|
||||||
|
|
||||||
ast_binop(binop o, ast_ptr l, ast_ptr r)
|
|
||||||
: op(o), left(std::move(l)), right(std::move(r)) {}
|
|
||||||
};
|
|
||||||
|
|
||||||
struct ast_app : public ast {
|
|
||||||
ast_ptr left;
|
|
||||||
ast_ptr right;
|
|
||||||
|
|
||||||
ast_app(ast_ptr l, ast_ptr r)
|
|
||||||
: left(std::move(l)), right(std::move(r)) {}
|
|
||||||
};
|
|
||||||
|
|
||||||
struct ast_case : public ast {
|
|
||||||
ast_ptr of;
|
|
||||||
std::vector<branch_ptr> branches;
|
|
||||||
|
|
||||||
ast_case(ast_ptr o, std::vector<branch_ptr> b)
|
|
||||||
: of(std::move(o)), branches(std::move(b)) {}
|
|
||||||
};
|
|
||||||
|
|
||||||
struct pattern_var : public pattern {
|
|
||||||
std::string var;
|
|
||||||
|
|
||||||
pattern_var(std::string v)
|
|
||||||
: var(std::move(v)) {}
|
|
||||||
};
|
|
||||||
|
|
||||||
struct pattern_constr : public pattern {
|
|
||||||
std::string constr;
|
|
||||||
std::vector<std::string> params;
|
|
||||||
|
|
||||||
pattern_constr(std::string c, std::vector<std::string> p)
|
|
||||||
: constr(std::move(c)), params(std::move(p)) {}
|
|
||||||
};
|
|
||||||
|
|
||||||
struct definition_defn : public definition {
|
|
||||||
std::string name;
|
|
||||||
std::vector<std::string> params;
|
|
||||||
ast_ptr body;
|
|
||||||
|
|
||||||
definition_defn(std::string n, std::vector<std::string> p, ast_ptr b)
|
|
||||||
: name(std::move(n)), params(std::move(p)), body(std::move(b)) {
|
|
||||||
|
|
||||||
}
|
|
||||||
};
|
|
||||||
|
|
||||||
struct definition_data : public definition {
|
|
||||||
std::string name;
|
|
||||||
std::vector<constructor_ptr> constructors;
|
|
||||||
|
|
||||||
definition_data(std::string n, std::vector<constructor_ptr> cs)
|
|
||||||
: name(std::move(n)), constructors(std::move(cs)) {}
|
|
||||||
};
|
|
@ -1 +0,0 @@
|
|||||||
rm -f parser.o parser.cpp parser.hpp stack.hh scanner.cpp scanner.o a.out
|
|
@ -1,5 +0,0 @@
|
|||||||
bison -o parser.cpp -d parser.y
|
|
||||||
flex -o scanner.cpp scanner.l
|
|
||||||
g++ -c -o scanner.o scanner.cpp
|
|
||||||
g++ -c -o parser.o parser.cpp
|
|
||||||
g++ main.cpp parser.o scanner.o
|
|
@ -1,14 +0,0 @@
|
|||||||
#include "ast.hpp"
|
|
||||||
#include "parser.hpp"
|
|
||||||
|
|
||||||
void yy::parser::error(const std::string& msg) {
|
|
||||||
std::cout << "An error occured: " << msg << std::endl;
|
|
||||||
}
|
|
||||||
|
|
||||||
extern std::vector<definition_ptr> program;
|
|
||||||
|
|
||||||
int main() {
|
|
||||||
yy::parser parser;
|
|
||||||
parser.parse();
|
|
||||||
std::cout << program.size() << std::endl;
|
|
||||||
}
|
|
@ -1,140 +0,0 @@
|
|||||||
%{
|
|
||||||
#include <string>
|
|
||||||
#include <iostream>
|
|
||||||
#include "ast.hpp"
|
|
||||||
#include "parser.hpp"
|
|
||||||
|
|
||||||
std::vector<definition_ptr> program;
|
|
||||||
extern yy::parser::symbol_type yylex();
|
|
||||||
|
|
||||||
%}
|
|
||||||
|
|
||||||
%token PLUS
|
|
||||||
%token TIMES
|
|
||||||
%token MINUS
|
|
||||||
%token DIVIDE
|
|
||||||
%token <int> INT
|
|
||||||
%token DEFN
|
|
||||||
%token DATA
|
|
||||||
%token CASE
|
|
||||||
%token OF
|
|
||||||
%token OCURLY
|
|
||||||
%token CCURLY
|
|
||||||
%token OPAREN
|
|
||||||
%token CPAREN
|
|
||||||
%token COMMA
|
|
||||||
%token ARROW
|
|
||||||
%token EQUAL
|
|
||||||
%token <std::string> LID
|
|
||||||
%token <std::string> UID
|
|
||||||
|
|
||||||
%language "c++"
|
|
||||||
%define api.value.type variant
|
|
||||||
%define api.token.constructor
|
|
||||||
|
|
||||||
%type <std::vector<std::string>> lowercaseParams uppercaseParams
|
|
||||||
%type <std::vector<definition_ptr>> program definitions
|
|
||||||
%type <std::vector<branch_ptr>> branches
|
|
||||||
%type <std::vector<constructor_ptr>> constructors
|
|
||||||
%type <ast_ptr> aAdd aMul case app appBase
|
|
||||||
%type <definition_ptr> definition defn data
|
|
||||||
%type <branch_ptr> branch
|
|
||||||
%type <pattern_ptr> pattern
|
|
||||||
%type <constructor_ptr> constructor
|
|
||||||
|
|
||||||
%start program
|
|
||||||
|
|
||||||
%%
|
|
||||||
|
|
||||||
program
|
|
||||||
: definitions { program = std::move($1); }
|
|
||||||
;
|
|
||||||
|
|
||||||
definitions
|
|
||||||
: definitions definition { $$ = std::move($1); $$.push_back(std::move($2)); }
|
|
||||||
| definition { $$ = std::vector<definition_ptr>(); $$.push_back(std::move($1)); }
|
|
||||||
;
|
|
||||||
|
|
||||||
definition
|
|
||||||
: defn { $$ = std::move($1); }
|
|
||||||
| data { $$ = std::move($1); }
|
|
||||||
;
|
|
||||||
|
|
||||||
defn
|
|
||||||
: DEFN LID lowercaseParams EQUAL OCURLY aAdd CCURLY
|
|
||||||
{ $$ = definition_ptr(
|
|
||||||
new definition_defn(std::move($2), std::move($3), std::move($6))); }
|
|
||||||
;
|
|
||||||
|
|
||||||
lowercaseParams
|
|
||||||
: %empty { $$ = std::vector<std::string>(); }
|
|
||||||
| lowercaseParams LID { $$ = std::move($1); $$.push_back(std::move($2)); }
|
|
||||||
;
|
|
||||||
|
|
||||||
uppercaseParams
|
|
||||||
: %empty { $$ = std::vector<std::string>(); }
|
|
||||||
| uppercaseParams UID { $$ = std::move($1); $$.push_back(std::move($2)); }
|
|
||||||
;
|
|
||||||
|
|
||||||
aAdd
|
|
||||||
: aAdd PLUS aMul { $$ = ast_ptr(new ast_binop(PLUS, std::move($1), std::move($3))); }
|
|
||||||
| aAdd MINUS aMul { $$ = ast_ptr(new ast_binop(MINUS, std::move($1), std::move($3))); }
|
|
||||||
| aMul { $$ = std::move($1); }
|
|
||||||
;
|
|
||||||
|
|
||||||
aMul
|
|
||||||
: aMul TIMES app { $$ = ast_ptr(new ast_binop(TIMES, std::move($1), std::move($3))); }
|
|
||||||
| aMul DIVIDE app { $$ = ast_ptr(new ast_binop(DIVIDE, std::move($1), std::move($3))); }
|
|
||||||
| app { $$ = std::move($1); }
|
|
||||||
;
|
|
||||||
|
|
||||||
app
|
|
||||||
: app appBase { $$ = ast_ptr(new ast_app(std::move($1), std::move($2))); }
|
|
||||||
| appBase { $$ = std::move($1); }
|
|
||||||
;
|
|
||||||
|
|
||||||
appBase
|
|
||||||
: INT { $$ = ast_ptr(new ast_int($1)); }
|
|
||||||
| LID { $$ = ast_ptr(new ast_lid(std::move($1))); }
|
|
||||||
| UID { $$ = ast_ptr(new ast_uid(std::move($1))); }
|
|
||||||
| OPAREN aAdd CPAREN { $$ = std::move($2); }
|
|
||||||
| case { $$ = std::move($1); }
|
|
||||||
;
|
|
||||||
|
|
||||||
case
|
|
||||||
: CASE aAdd OF OCURLY branches CCURLY
|
|
||||||
{ $$ = ast_ptr(new ast_case(std::move($2), std::move($5))); }
|
|
||||||
;
|
|
||||||
|
|
||||||
branches
|
|
||||||
: branches branch { $$ = std::move($1); $1.push_back(std::move($2)); }
|
|
||||||
| branch { $$ = std::vector<branch_ptr>(); $$.push_back(std::move($1));}
|
|
||||||
;
|
|
||||||
|
|
||||||
branch
|
|
||||||
: pattern ARROW OCURLY aAdd CCURLY
|
|
||||||
{ $$ = branch_ptr(new branch(std::move($1), std::move($4))); }
|
|
||||||
;
|
|
||||||
|
|
||||||
pattern
|
|
||||||
: LID { $$ = pattern_ptr(new pattern_var(std::move($1))); }
|
|
||||||
| UID lowercaseParams
|
|
||||||
{ $$ = pattern_ptr(new pattern_constr(std::move($1), std::move($2))); }
|
|
||||||
;
|
|
||||||
|
|
||||||
data
|
|
||||||
: DATA UID EQUAL OCURLY constructors CCURLY
|
|
||||||
{ $$ = definition_ptr(new definition_data(std::move($2), std::move($5))); }
|
|
||||||
;
|
|
||||||
|
|
||||||
constructors
|
|
||||||
: constructors COMMA constructor { $$ = std::move($1); $$.push_back(std::move($3)); }
|
|
||||||
| constructor
|
|
||||||
{ $$ = std::vector<constructor_ptr>(); $$.push_back(std::move($1)); }
|
|
||||||
;
|
|
||||||
|
|
||||||
constructor
|
|
||||||
: UID uppercaseParams
|
|
||||||
{ $$ = constructor_ptr(new constructor(std::move($1), std::move($2))); }
|
|
||||||
;
|
|
||||||
|
|
@ -1,34 +0,0 @@
|
|||||||
%option noyywrap
|
|
||||||
|
|
||||||
%{
|
|
||||||
#include <iostream>
|
|
||||||
#include "ast.hpp"
|
|
||||||
#include "parser.hpp"
|
|
||||||
|
|
||||||
#define YY_DECL yy::parser::symbol_type yylex()
|
|
||||||
|
|
||||||
%}
|
|
||||||
|
|
||||||
%%
|
|
||||||
|
|
||||||
[ \n]+ {}
|
|
||||||
\+ { return yy::parser::make_PLUS(); }
|
|
||||||
\* { return yy::parser::make_TIMES(); }
|
|
||||||
- { return yy::parser::make_MINUS(); }
|
|
||||||
\/ { return yy::parser::make_DIVIDE(); }
|
|
||||||
[0-9]+ { return yy::parser::make_INT(atoi(yytext)); }
|
|
||||||
defn { return yy::parser::make_DEFN(); }
|
|
||||||
data { return yy::parser::make_DATA(); }
|
|
||||||
case { return yy::parser::make_CASE(); }
|
|
||||||
of { return yy::parser::make_OF(); }
|
|
||||||
\{ { return yy::parser::make_OCURLY(); }
|
|
||||||
\} { return yy::parser::make_CCURLY(); }
|
|
||||||
\( { return yy::parser::make_OPAREN(); }
|
|
||||||
\) { return yy::parser::make_CPAREN(); }
|
|
||||||
, { return yy::parser::make_COMMA(); }
|
|
||||||
-> { return yy::parser::make_ARROW(); }
|
|
||||||
= { return yy::parser::make_EQUAL(); }
|
|
||||||
[a-z][a-zA-Z]* { return yy::parser::make_LID(std::string(yytext)); }
|
|
||||||
[A-Z][a-zA-Z]* { return yy::parser::make_UID(std::string(yytext)); }
|
|
||||||
|
|
||||||
%%
|
|
@ -1,82 +0,0 @@
|
|||||||
#include "ast.hpp"
|
|
||||||
|
|
||||||
std::string op_name(binop op) {
|
|
||||||
switch(op) {
|
|
||||||
case PLUS: return "+";
|
|
||||||
case MINUS: return "-";
|
|
||||||
case TIMES: return "*";
|
|
||||||
case DIVIDE: return "/";
|
|
||||||
}
|
|
||||||
throw 0;
|
|
||||||
}
|
|
||||||
|
|
||||||
type_ptr ast_int::typecheck(type_mgr& mgr, const type_env& env) const {
|
|
||||||
return type_ptr(new type_base("Int"));
|
|
||||||
}
|
|
||||||
|
|
||||||
type_ptr ast_lid::typecheck(type_mgr& mgr, const type_env& env) const {
|
|
||||||
return env.lookup(id);
|
|
||||||
}
|
|
||||||
|
|
||||||
type_ptr ast_uid::typecheck(type_mgr& mgr, const type_env& env) const {
|
|
||||||
return env.lookup(id);
|
|
||||||
}
|
|
||||||
|
|
||||||
type_ptr ast_binop::typecheck(type_mgr& mgr, const type_env& env) const {
|
|
||||||
type_ptr ltype = left->typecheck(mgr, env);
|
|
||||||
type_ptr rtype = right->typecheck(mgr, env);
|
|
||||||
type_ptr ftype = env.lookup(op_name(op));
|
|
||||||
if(!ftype) throw 0;
|
|
||||||
|
|
||||||
type_ptr return_type = mgr.new_type();
|
|
||||||
type_ptr arrow_one = type_ptr(new type_arr(rtype, return_type));
|
|
||||||
type_ptr arrow_two = type_ptr(new type_arr(ltype, arrow_one));
|
|
||||||
|
|
||||||
mgr.unify(arrow_two, ftype);
|
|
||||||
return return_type;
|
|
||||||
}
|
|
||||||
|
|
||||||
type_ptr ast_app::typecheck(type_mgr& mgr, const type_env& env) const {
|
|
||||||
type_ptr ltype = left->typecheck(mgr, env);
|
|
||||||
type_ptr rtype = right->typecheck(mgr, env);
|
|
||||||
|
|
||||||
type_ptr return_type = mgr.new_type();
|
|
||||||
type_ptr arrow = type_ptr(new type_arr(rtype, return_type));
|
|
||||||
mgr.unify(arrow, ltype);
|
|
||||||
return return_type;
|
|
||||||
}
|
|
||||||
|
|
||||||
type_ptr ast_case::typecheck(type_mgr& mgr, const type_env& env) const {
|
|
||||||
type_ptr case_type = of->typecheck(mgr, env);
|
|
||||||
type_ptr branch_type = mgr.new_type();
|
|
||||||
|
|
||||||
for(auto& branch : branches) {
|
|
||||||
type_env new_env = env.scope();
|
|
||||||
branch->pat->match(case_type, mgr, new_env);
|
|
||||||
type_ptr curr_branch_type = branch->expr->typecheck(mgr, new_env);
|
|
||||||
mgr.unify(branch_type, curr_branch_type);
|
|
||||||
}
|
|
||||||
|
|
||||||
return branch_type;
|
|
||||||
}
|
|
||||||
|
|
||||||
void pattern_var::match(type_ptr t, type_mgr& mgr, type_env& env) const {
|
|
||||||
env.bind(var, t);
|
|
||||||
}
|
|
||||||
|
|
||||||
void pattern_constr::match(type_ptr t, type_mgr& mgr, type_env& env) const {
|
|
||||||
type_ptr constructor_type = env.lookup(constr);
|
|
||||||
if(!constructor_type) throw 0;
|
|
||||||
|
|
||||||
for(int i = 0; i < params.size(); i++) {
|
|
||||||
type_arr* arr = dynamic_cast<type_arr*>(constructor_type.get());
|
|
||||||
if(!arr) throw 0;
|
|
||||||
|
|
||||||
env.bind(params[i], arr->left);
|
|
||||||
constructor_type = arr->right;
|
|
||||||
}
|
|
||||||
|
|
||||||
mgr.unify(t, constructor_type);
|
|
||||||
type_base* result_type = dynamic_cast<type_base*>(constructor_type.get());
|
|
||||||
if(!result_type) throw 0;
|
|
||||||
}
|
|
@ -1,162 +0,0 @@
|
|||||||
#pragma once
|
|
||||||
#include <memory>
|
|
||||||
#include <vector>
|
|
||||||
#include "type.hpp"
|
|
||||||
#include "env.hpp"
|
|
||||||
|
|
||||||
struct ast {
|
|
||||||
virtual ~ast() = default;
|
|
||||||
|
|
||||||
virtual type_ptr typecheck(type_mgr& mgr, const type_env& env) const = 0;
|
|
||||||
};
|
|
||||||
|
|
||||||
using ast_ptr = std::unique_ptr<ast>;
|
|
||||||
|
|
||||||
struct pattern {
|
|
||||||
virtual ~pattern() = default;
|
|
||||||
|
|
||||||
virtual void match(type_ptr t, type_mgr& mgr, type_env& env) const = 0;
|
|
||||||
};
|
|
||||||
|
|
||||||
using pattern_ptr = std::unique_ptr<pattern>;
|
|
||||||
|
|
||||||
struct branch {
|
|
||||||
pattern_ptr pat;
|
|
||||||
ast_ptr expr;
|
|
||||||
|
|
||||||
branch(pattern_ptr p, ast_ptr a)
|
|
||||||
: pat(std::move(p)), expr(std::move(a)) {}
|
|
||||||
};
|
|
||||||
|
|
||||||
using branch_ptr = std::unique_ptr<branch>;
|
|
||||||
|
|
||||||
struct constructor {
|
|
||||||
std::string name;
|
|
||||||
std::vector<std::string> types;
|
|
||||||
|
|
||||||
constructor(std::string n, std::vector<std::string> ts)
|
|
||||||
: name(std::move(n)), types(std::move(ts)) {}
|
|
||||||
};
|
|
||||||
|
|
||||||
using constructor_ptr = std::unique_ptr<constructor>;
|
|
||||||
|
|
||||||
struct definition {
|
|
||||||
virtual ~definition() = default;
|
|
||||||
|
|
||||||
virtual void typecheck_first(type_mgr& mgr, type_env& env) = 0;
|
|
||||||
virtual void typecheck_second(type_mgr& mgr, const type_env& env) const = 0;
|
|
||||||
};
|
|
||||||
|
|
||||||
using definition_ptr = std::unique_ptr<definition>;
|
|
||||||
|
|
||||||
enum binop {
|
|
||||||
PLUS,
|
|
||||||
MINUS,
|
|
||||||
TIMES,
|
|
||||||
DIVIDE
|
|
||||||
};
|
|
||||||
|
|
||||||
struct ast_int : public ast {
|
|
||||||
int value;
|
|
||||||
|
|
||||||
explicit ast_int(int v)
|
|
||||||
: value(v) {}
|
|
||||||
|
|
||||||
type_ptr typecheck(type_mgr& mgr, const type_env& env) const;
|
|
||||||
};
|
|
||||||
|
|
||||||
struct ast_lid : public ast {
|
|
||||||
std::string id;
|
|
||||||
|
|
||||||
explicit ast_lid(std::string i)
|
|
||||||
: id(std::move(i)) {}
|
|
||||||
|
|
||||||
type_ptr typecheck(type_mgr& mgr, const type_env& env) const;
|
|
||||||
};
|
|
||||||
|
|
||||||
struct ast_uid : public ast {
|
|
||||||
std::string id;
|
|
||||||
|
|
||||||
explicit ast_uid(std::string i)
|
|
||||||
: id(std::move(i)) {}
|
|
||||||
|
|
||||||
type_ptr typecheck(type_mgr& mgr, const type_env& env) const;
|
|
||||||
};
|
|
||||||
|
|
||||||
struct ast_binop : public ast {
|
|
||||||
binop op;
|
|
||||||
ast_ptr left;
|
|
||||||
ast_ptr right;
|
|
||||||
|
|
||||||
ast_binop(binop o, ast_ptr l, ast_ptr r)
|
|
||||||
: op(o), left(std::move(l)), right(std::move(r)) {}
|
|
||||||
|
|
||||||
type_ptr typecheck(type_mgr& mgr, const type_env& env) const;
|
|
||||||
};
|
|
||||||
|
|
||||||
struct ast_app : public ast {
|
|
||||||
ast_ptr left;
|
|
||||||
ast_ptr right;
|
|
||||||
|
|
||||||
ast_app(ast_ptr l, ast_ptr r)
|
|
||||||
: left(std::move(l)), right(std::move(r)) {}
|
|
||||||
|
|
||||||
type_ptr typecheck(type_mgr& mgr, const type_env& env) const;
|
|
||||||
};
|
|
||||||
|
|
||||||
struct ast_case : public ast {
|
|
||||||
ast_ptr of;
|
|
||||||
std::vector<branch_ptr> branches;
|
|
||||||
|
|
||||||
ast_case(ast_ptr o, std::vector<branch_ptr> b)
|
|
||||||
: of(std::move(o)), branches(std::move(b)) {}
|
|
||||||
|
|
||||||
type_ptr typecheck(type_mgr& mgr, const type_env& env) const;
|
|
||||||
};
|
|
||||||
|
|
||||||
struct pattern_var : public pattern {
|
|
||||||
std::string var;
|
|
||||||
|
|
||||||
pattern_var(std::string v)
|
|
||||||
: var(std::move(v)) {}
|
|
||||||
|
|
||||||
void match(type_ptr t, type_mgr& mgr, type_env& env) const;
|
|
||||||
};
|
|
||||||
|
|
||||||
struct pattern_constr : public pattern {
|
|
||||||
std::string constr;
|
|
||||||
std::vector<std::string> params;
|
|
||||||
|
|
||||||
pattern_constr(std::string c, std::vector<std::string> p)
|
|
||||||
: constr(std::move(c)), params(std::move(p)) {}
|
|
||||||
|
|
||||||
void match(type_ptr t, type_mgr&, type_env& env) const;
|
|
||||||
};
|
|
||||||
|
|
||||||
struct definition_defn : public definition {
|
|
||||||
std::string name;
|
|
||||||
std::vector<std::string> params;
|
|
||||||
ast_ptr body;
|
|
||||||
|
|
||||||
type_ptr return_type;
|
|
||||||
std::vector<type_ptr> param_types;
|
|
||||||
|
|
||||||
definition_defn(std::string n, std::vector<std::string> p, ast_ptr b)
|
|
||||||
: name(std::move(n)), params(std::move(p)), body(std::move(b)) {
|
|
||||||
|
|
||||||
}
|
|
||||||
|
|
||||||
void typecheck_first(type_mgr& mgr, type_env& env);
|
|
||||||
void typecheck_second(type_mgr& mgr, const type_env& env) const;
|
|
||||||
};
|
|
||||||
|
|
||||||
struct definition_data : public definition {
|
|
||||||
std::string name;
|
|
||||||
std::vector<constructor_ptr> constructors;
|
|
||||||
|
|
||||||
definition_data(std::string n, std::vector<constructor_ptr> cs)
|
|
||||||
: name(std::move(n)), constructors(std::move(cs)) {}
|
|
||||||
|
|
||||||
void typecheck_first(type_mgr& mgr, type_env& env);
|
|
||||||
void typecheck_second(type_mgr& mgr, const type_env& env) const;
|
|
||||||
};
|
|
@ -1,2 +0,0 @@
|
|||||||
data Bool = { True, False }
|
|
||||||
defn main = { 3 + True }
|
|
@ -1 +0,0 @@
|
|||||||
defn main = { 1 2 3 4 5 }
|
|
@ -1 +0,0 @@
|
|||||||
rm -f parser.o parser.cpp parser.hpp stack.hh scanner.cpp scanner.o type.o env.o ast.o definition.o a.out
|
|
@ -1,9 +0,0 @@
|
|||||||
bison -o parser.cpp -d parser.y
|
|
||||||
flex -o scanner.cpp scanner.l
|
|
||||||
g++ -g -c -o scanner.o scanner.cpp
|
|
||||||
g++ -g -c -o parser.o parser.cpp
|
|
||||||
g++ -g -c -o type.o type.cpp
|
|
||||||
g++ -g -c -o env.o env.cpp
|
|
||||||
g++ -g -c -o ast.o ast.cpp
|
|
||||||
g++ -g -c -o definition.o definition.cpp
|
|
||||||
g++ -g main.cpp parser.o scanner.o type.o env.o ast.o definition.o
|
|
@ -1,48 +0,0 @@
|
|||||||
#include "ast.hpp"
|
|
||||||
|
|
||||||
void definition_defn::typecheck_first(type_mgr& mgr, type_env& env) {
|
|
||||||
return_type = mgr.new_type();
|
|
||||||
type_ptr full_type = return_type;
|
|
||||||
|
|
||||||
for(auto it = params.rbegin(); it != params.rend(); it++) {
|
|
||||||
type_ptr param_type = mgr.new_type();
|
|
||||||
full_type = type_ptr(new type_arr(param_type, full_type));
|
|
||||||
param_types.push_back(param_type);
|
|
||||||
}
|
|
||||||
|
|
||||||
env.bind(name, full_type);
|
|
||||||
}
|
|
||||||
|
|
||||||
void definition_defn::typecheck_second(type_mgr& mgr, const type_env& env) const {
|
|
||||||
type_env new_env = env.scope();
|
|
||||||
auto param_it = params.begin();
|
|
||||||
auto type_it = param_types.rbegin();
|
|
||||||
|
|
||||||
while(param_it != params.end() && type_it != param_types.rend()) {
|
|
||||||
new_env.bind(*param_it, *type_it);
|
|
||||||
param_it++;
|
|
||||||
type_it++;
|
|
||||||
}
|
|
||||||
|
|
||||||
type_ptr body_type = body->typecheck(mgr, new_env);
|
|
||||||
mgr.unify(return_type, body_type);
|
|
||||||
}
|
|
||||||
|
|
||||||
void definition_data::typecheck_first(type_mgr& mgr, type_env& env) {
|
|
||||||
type_ptr return_type = type_ptr(new type_base(name));
|
|
||||||
|
|
||||||
for(auto& constructor : constructors) {
|
|
||||||
type_ptr full_type = return_type;
|
|
||||||
|
|
||||||
for(auto& type_name : constructor->types) {
|
|
||||||
type_ptr type = type_ptr(new type_base(type_name));
|
|
||||||
full_type = type_ptr(new type_arr(type, full_type));
|
|
||||||
}
|
|
||||||
|
|
||||||
env.bind(constructor->name, full_type);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
void definition_data::typecheck_second(type_mgr& mgr, const type_env& env) const {
|
|
||||||
// Nothing
|
|
||||||
}
|
|
@ -1,16 +0,0 @@
|
|||||||
#include "env.hpp"
|
|
||||||
|
|
||||||
type_ptr type_env::lookup(const std::string& name) const {
|
|
||||||
auto it = names.find(name);
|
|
||||||
if(it != names.end()) return it->second;
|
|
||||||
if(parent) return parent->lookup(name);
|
|
||||||
return nullptr;
|
|
||||||
}
|
|
||||||
|
|
||||||
void type_env::bind(const std::string& name, type_ptr t) {
|
|
||||||
names[name] = t;
|
|
||||||
}
|
|
||||||
|
|
||||||
type_env type_env::scope() const {
|
|
||||||
return type_env(this);
|
|
||||||
}
|
|
@ -1,16 +0,0 @@
|
|||||||
#pragma once
|
|
||||||
#include <map>
|
|
||||||
#include "type.hpp"
|
|
||||||
|
|
||||||
struct type_env {
|
|
||||||
std::map<std::string, type_ptr> names;
|
|
||||||
type_env const* parent = nullptr;
|
|
||||||
|
|
||||||
type_env(type_env const* p)
|
|
||||||
: parent(p) {}
|
|
||||||
type_env() : type_env(nullptr) {}
|
|
||||||
|
|
||||||
type_ptr lookup(const std::string& name) const;
|
|
||||||
void bind(const std::string& name, type_ptr t);
|
|
||||||
type_env scope() const;
|
|
||||||
};
|
|
@ -1,39 +0,0 @@
|
|||||||
#include "ast.hpp"
|
|
||||||
#include "parser.hpp"
|
|
||||||
#include "type.hpp"
|
|
||||||
|
|
||||||
void yy::parser::error(const std::string& msg) {
|
|
||||||
std::cout << "An error occured: " << msg << std::endl;
|
|
||||||
}
|
|
||||||
|
|
||||||
extern std::vector<definition_ptr> program;
|
|
||||||
|
|
||||||
void typecheck_program(const std::vector<definition_ptr>& prog) {
|
|
||||||
type_mgr mgr;
|
|
||||||
type_env env;
|
|
||||||
|
|
||||||
type_ptr int_type = type_ptr(new type_base("Int"));
|
|
||||||
type_ptr binop_type = type_ptr(new type_arr(
|
|
||||||
int_type,
|
|
||||||
type_ptr(new type_arr(int_type, int_type))));
|
|
||||||
|
|
||||||
env.bind("+", binop_type);
|
|
||||||
env.bind("-", binop_type);
|
|
||||||
env.bind("*", binop_type);
|
|
||||||
env.bind("/", binop_type);
|
|
||||||
|
|
||||||
for(auto& def : prog) {
|
|
||||||
def->typecheck_first(mgr, env);
|
|
||||||
}
|
|
||||||
|
|
||||||
for(auto& def : prog) {
|
|
||||||
def->typecheck_second(mgr, env);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
int main() {
|
|
||||||
yy::parser parser;
|
|
||||||
parser.parse();
|
|
||||||
typecheck_program(program);
|
|
||||||
std::cout << program.size() << std::endl;
|
|
||||||
}
|
|
@ -1,140 +0,0 @@
|
|||||||
%{
|
|
||||||
#include <string>
|
|
||||||
#include <iostream>
|
|
||||||
#include "ast.hpp"
|
|
||||||
#include "parser.hpp"
|
|
||||||
|
|
||||||
std::vector<definition_ptr> program;
|
|
||||||
extern yy::parser::symbol_type yylex();
|
|
||||||
|
|
||||||
%}
|
|
||||||
|
|
||||||
%token PLUS
|
|
||||||
%token TIMES
|
|
||||||
%token MINUS
|
|
||||||
%token DIVIDE
|
|
||||||
%token <int> INT
|
|
||||||
%token DEFN
|
|
||||||
%token DATA
|
|
||||||
%token CASE
|
|
||||||
%token OF
|
|
||||||
%token OCURLY
|
|
||||||
%token CCURLY
|
|
||||||
%token OPAREN
|
|
||||||
%token CPAREN
|
|
||||||
%token COMMA
|
|
||||||
%token ARROW
|
|
||||||
%token EQUAL
|
|
||||||
%token <std::string> LID
|
|
||||||
%token <std::string> UID
|
|
||||||
|
|
||||||
%language "c++"
|
|
||||||
%define api.value.type variant
|
|
||||||
%define api.token.constructor
|
|
||||||
|
|
||||||
%type <std::vector<std::string>> lowercaseParams uppercaseParams
|
|
||||||
%type <std::vector<definition_ptr>> program definitions
|
|
||||||
%type <std::vector<branch_ptr>> branches
|
|
||||||
%type <std::vector<constructor_ptr>> constructors
|
|
||||||
%type <ast_ptr> aAdd aMul case app appBase
|
|
||||||
%type <definition_ptr> definition defn data
|
|
||||||
%type <branch_ptr> branch
|
|
||||||
%type <pattern_ptr> pattern
|
|
||||||
%type <constructor_ptr> constructor
|
|
||||||
|
|
||||||
%start program
|
|
||||||
|
|
||||||
%%
|
|
||||||
|
|
||||||
program
|
|
||||||
: definitions { program = std::move($1); }
|
|
||||||
;
|
|
||||||
|
|
||||||
definitions
|
|
||||||
: definitions definition { $$ = std::move($1); $$.push_back(std::move($2)); }
|
|
||||||
| definition { $$ = std::vector<definition_ptr>(); $$.push_back(std::move($1)); }
|
|
||||||
;
|
|
||||||
|
|
||||||
definition
|
|
||||||
: defn { $$ = std::move($1); }
|
|
||||||
| data { $$ = std::move($1); }
|
|
||||||
;
|
|
||||||
|
|
||||||
defn
|
|
||||||
: DEFN LID lowercaseParams EQUAL OCURLY aAdd CCURLY
|
|
||||||
{ $$ = definition_ptr(
|
|
||||||
new definition_defn(std::move($2), std::move($3), std::move($6))); }
|
|
||||||
;
|
|
||||||
|
|
||||||
lowercaseParams
|
|
||||||
: %empty { $$ = std::vector<std::string>(); }
|
|
||||||
| lowercaseParams LID { $$ = std::move($1); $$.push_back(std::move($2)); }
|
|
||||||
;
|
|
||||||
|
|
||||||
uppercaseParams
|
|
||||||
: %empty { $$ = std::vector<std::string>(); }
|
|
||||||
| uppercaseParams UID { $$ = std::move($1); $$.push_back(std::move($2)); }
|
|
||||||
;
|
|
||||||
|
|
||||||
aAdd
|
|
||||||
: aAdd PLUS aMul { $$ = ast_ptr(new ast_binop(PLUS, std::move($1), std::move($3))); }
|
|
||||||
| aAdd MINUS aMul { $$ = ast_ptr(new ast_binop(MINUS, std::move($1), std::move($3))); }
|
|
||||||
| aMul { $$ = std::move($1); }
|
|
||||||
;
|
|
||||||
|
|
||||||
aMul
|
|
||||||
: aMul TIMES app { $$ = ast_ptr(new ast_binop(TIMES, std::move($1), std::move($3))); }
|
|
||||||
| aMul DIVIDE app { $$ = ast_ptr(new ast_binop(DIVIDE, std::move($1), std::move($3))); }
|
|
||||||
| app { $$ = std::move($1); }
|
|
||||||
;
|
|
||||||
|
|
||||||
app
|
|
||||||
: app appBase { $$ = ast_ptr(new ast_app(std::move($1), std::move($2))); }
|
|
||||||
| appBase { $$ = std::move($1); }
|
|
||||||
;
|
|
||||||
|
|
||||||
appBase
|
|
||||||
: INT { $$ = ast_ptr(new ast_int($1)); }
|
|
||||||
| LID { $$ = ast_ptr(new ast_lid(std::move($1))); }
|
|
||||||
| UID { $$ = ast_ptr(new ast_uid(std::move($1))); }
|
|
||||||
| OPAREN aAdd CPAREN { $$ = std::move($2); }
|
|
||||||
| case { $$ = std::move($1); }
|
|
||||||
;
|
|
||||||
|
|
||||||
case
|
|
||||||
: CASE aAdd OF OCURLY branches CCURLY
|
|
||||||
{ $$ = ast_ptr(new ast_case(std::move($2), std::move($5))); }
|
|
||||||
;
|
|
||||||
|
|
||||||
branches
|
|
||||||
: branches branch { $$ = std::move($1); $1.push_back(std::move($2)); }
|
|
||||||
| branch { $$ = std::vector<branch_ptr>(); $$.push_back(std::move($1));}
|
|
||||||
;
|
|
||||||
|
|
||||||
branch
|
|
||||||
: pattern ARROW OCURLY aAdd CCURLY
|
|
||||||
{ $$ = branch_ptr(new branch(std::move($1), std::move($4))); }
|
|
||||||
;
|
|
||||||
|
|
||||||
pattern
|
|
||||||
: LID { $$ = pattern_ptr(new pattern_var(std::move($1))); }
|
|
||||||
| UID lowercaseParams
|
|
||||||
{ $$ = pattern_ptr(new pattern_constr(std::move($1), std::move($2))); }
|
|
||||||
;
|
|
||||||
|
|
||||||
data
|
|
||||||
: DATA UID EQUAL OCURLY constructors CCURLY
|
|
||||||
{ $$ = definition_ptr(new definition_data(std::move($2), std::move($5))); }
|
|
||||||
;
|
|
||||||
|
|
||||||
constructors
|
|
||||||
: constructors COMMA constructor { $$ = std::move($1); $$.push_back(std::move($3)); }
|
|
||||||
| constructor
|
|
||||||
{ $$ = std::vector<constructor_ptr>(); $$.push_back(std::move($1)); }
|
|
||||||
;
|
|
||||||
|
|
||||||
constructor
|
|
||||||
: UID uppercaseParams
|
|
||||||
{ $$ = constructor_ptr(new constructor(std::move($1), std::move($2))); }
|
|
||||||
;
|
|
||||||
|
|
@ -1,34 +0,0 @@
|
|||||||
%option noyywrap
|
|
||||||
|
|
||||||
%{
|
|
||||||
#include <iostream>
|
|
||||||
#include "ast.hpp"
|
|
||||||
#include "parser.hpp"
|
|
||||||
|
|
||||||
#define YY_DECL yy::parser::symbol_type yylex()
|
|
||||||
|
|
||||||
%}
|
|
||||||
|
|
||||||
%%
|
|
||||||
|
|
||||||
[ \n]+ {}
|
|
||||||
\+ { return yy::parser::make_PLUS(); }
|
|
||||||
\* { return yy::parser::make_TIMES(); }
|
|
||||||
- { return yy::parser::make_MINUS(); }
|
|
||||||
\/ { return yy::parser::make_DIVIDE(); }
|
|
||||||
[0-9]+ { return yy::parser::make_INT(atoi(yytext)); }
|
|
||||||
defn { return yy::parser::make_DEFN(); }
|
|
||||||
data { return yy::parser::make_DATA(); }
|
|
||||||
case { return yy::parser::make_CASE(); }
|
|
||||||
of { return yy::parser::make_OF(); }
|
|
||||||
\{ { return yy::parser::make_OCURLY(); }
|
|
||||||
\} { return yy::parser::make_CCURLY(); }
|
|
||||||
\( { return yy::parser::make_OPAREN(); }
|
|
||||||
\) { return yy::parser::make_CPAREN(); }
|
|
||||||
, { return yy::parser::make_COMMA(); }
|
|
||||||
-> { return yy::parser::make_ARROW(); }
|
|
||||||
= { return yy::parser::make_EQUAL(); }
|
|
||||||
[a-z][a-zA-Z]* { return yy::parser::make_LID(std::string(yytext)); }
|
|
||||||
[A-Z][a-zA-Z]* { return yy::parser::make_UID(std::string(yytext)); }
|
|
||||||
|
|
||||||
%%
|
|
@ -1,78 +0,0 @@
|
|||||||
#include "type.hpp"
|
|
||||||
#include <sstream>
|
|
||||||
#include <algorithm>
|
|
||||||
|
|
||||||
std::string type_mgr::new_type_name() {
|
|
||||||
int temp = last_id++;
|
|
||||||
std::string str = "";
|
|
||||||
|
|
||||||
while(temp != -1) {
|
|
||||||
str += (char) ('a' + (temp % 26));
|
|
||||||
temp = temp / 26 - 1;
|
|
||||||
}
|
|
||||||
|
|
||||||
std::reverse(str.begin(), str.end());
|
|
||||||
return str;
|
|
||||||
}
|
|
||||||
|
|
||||||
type_ptr type_mgr::new_type() {
|
|
||||||
return type_ptr(new type_var(new_type_name()));
|
|
||||||
}
|
|
||||||
|
|
||||||
type_ptr type_mgr::new_arrow_type() {
|
|
||||||
return type_ptr(new type_arr(new_type(), new_type()));
|
|
||||||
}
|
|
||||||
|
|
||||||
type_ptr type_mgr::resolve(type_ptr t, type_var*& var) {
|
|
||||||
type_var* cast;
|
|
||||||
|
|
||||||
var = nullptr;
|
|
||||||
while((cast = dynamic_cast<type_var*>(t.get()))) {
|
|
||||||
auto it = types.find(cast->name);
|
|
||||||
|
|
||||||
if(it == types.end()) {
|
|
||||||
var = cast;
|
|
||||||
break;
|
|
||||||
}
|
|
||||||
t = it->second;
|
|
||||||
}
|
|
||||||
|
|
||||||
return t;
|
|
||||||
}
|
|
||||||
|
|
||||||
void type_mgr::unify(type_ptr l, type_ptr r) {
|
|
||||||
type_var* lvar;
|
|
||||||
type_var* rvar;
|
|
||||||
type_arr* larr;
|
|
||||||
type_arr* rarr;
|
|
||||||
type_base* lid;
|
|
||||||
type_base* rid;
|
|
||||||
|
|
||||||
l = resolve(l, lvar);
|
|
||||||
r = resolve(r, rvar);
|
|
||||||
|
|
||||||
if(lvar) {
|
|
||||||
bind(lvar->name, r);
|
|
||||||
return;
|
|
||||||
} else if(rvar) {
|
|
||||||
bind(rvar->name, l);
|
|
||||||
return;
|
|
||||||
} else if((larr = dynamic_cast<type_arr*>(l.get())) &&
|
|
||||||
(rarr = dynamic_cast<type_arr*>(r.get()))) {
|
|
||||||
unify(larr->left, rarr->left);
|
|
||||||
unify(larr->right, rarr->right);
|
|
||||||
return;
|
|
||||||
} else if((lid = dynamic_cast<type_base*>(l.get())) &&
|
|
||||||
(rid = dynamic_cast<type_base*>(r.get()))) {
|
|
||||||
if(lid->name == rid->name) return;
|
|
||||||
}
|
|
||||||
|
|
||||||
throw 0;
|
|
||||||
}
|
|
||||||
|
|
||||||
void type_mgr::bind(const std::string& s, type_ptr t) {
|
|
||||||
type_var* other = dynamic_cast<type_var*>(t.get());
|
|
||||||
|
|
||||||
if(other && other->name == s) return;
|
|
||||||
types[s] = t;
|
|
||||||
}
|
|
@ -1,44 +0,0 @@
|
|||||||
#pragma once
|
|
||||||
#include <memory>
|
|
||||||
#include <map>
|
|
||||||
|
|
||||||
struct type {
|
|
||||||
virtual ~type() = default;
|
|
||||||
};
|
|
||||||
|
|
||||||
using type_ptr = std::shared_ptr<type>;
|
|
||||||
|
|
||||||
struct type_var : public type {
|
|
||||||
std::string name;
|
|
||||||
|
|
||||||
type_var(std::string n)
|
|
||||||
: name(std::move(n)) {}
|
|
||||||
};
|
|
||||||
|
|
||||||
struct type_base : public type {
|
|
||||||
std::string name;
|
|
||||||
|
|
||||||
type_base(std::string n)
|
|
||||||
: name(std::move(n)) {}
|
|
||||||
};
|
|
||||||
|
|
||||||
struct type_arr : public type {
|
|
||||||
type_ptr left;
|
|
||||||
type_ptr right;
|
|
||||||
|
|
||||||
type_arr(type_ptr l, type_ptr r)
|
|
||||||
: left(std::move(l)), right(std::move(r)) {}
|
|
||||||
};
|
|
||||||
|
|
||||||
struct type_mgr {
|
|
||||||
int last_id = 0;
|
|
||||||
std::map<std::string, type_ptr> types;
|
|
||||||
|
|
||||||
std::string new_type_name();
|
|
||||||
type_ptr new_type();
|
|
||||||
type_ptr new_arrow_type();
|
|
||||||
|
|
||||||
void unify(type_ptr l, type_ptr r);
|
|
||||||
type_ptr resolve(type_ptr t, type_var*& var);
|
|
||||||
void bind(const std::string& s, type_ptr t);
|
|
||||||
};
|
|
@ -1,2 +0,0 @@
|
|||||||
defn main = { plus 320 6 }
|
|
||||||
defn plus x y = { x + y }
|
|
@ -1,3 +0,0 @@
|
|||||||
defn add x y = { x + y }
|
|
||||||
defn double x = { add x x }
|
|
||||||
defn main = { double 163 }
|
|
@ -1,7 +0,0 @@
|
|||||||
data List = { Nil, Cons Int List }
|
|
||||||
defn length l = {
|
|
||||||
case l of {
|
|
||||||
Nil -> { 0 }
|
|
||||||
Cons x xs -> { 1 + length xs }
|
|
||||||
}
|
|
||||||
}
|
|
@ -1,25 +0,0 @@
|
|||||||
cmake_minimum_required(VERSION 3.1)
|
|
||||||
project(compiler)
|
|
||||||
|
|
||||||
find_package(BISON)
|
|
||||||
find_package(FLEX)
|
|
||||||
bison_target(parser
|
|
||||||
${CMAKE_CURRENT_SOURCE_DIR}/parser.y
|
|
||||||
${CMAKE_CURRENT_BINARY_DIR}/parser.cpp
|
|
||||||
COMPILE_FLAGS "-d")
|
|
||||||
flex_target(scanner
|
|
||||||
${CMAKE_CURRENT_SOURCE_DIR}/scanner.l
|
|
||||||
${CMAKE_CURRENT_BINARY_DIR}/scanner.cpp)
|
|
||||||
add_flex_bison_dependency(scanner parser)
|
|
||||||
|
|
||||||
add_executable(compiler
|
|
||||||
ast.cpp ast.hpp definition.cpp
|
|
||||||
env.cpp env.hpp
|
|
||||||
type.cpp type.hpp
|
|
||||||
error.cpp error.hpp
|
|
||||||
${BISON_parser_OUTPUTS}
|
|
||||||
${FLEX_scanner_OUTPUTS}
|
|
||||||
main.cpp
|
|
||||||
)
|
|
||||||
target_include_directories(compiler PUBLIC ${CMAKE_CURRENT_SOURCE_DIR})
|
|
||||||
target_include_directories(compiler PUBLIC ${CMAKE_CURRENT_BINARY_DIR})
|
|
@ -1,145 +0,0 @@
|
|||||||
#include "ast.hpp"
|
|
||||||
#include <ostream>
|
|
||||||
#include "error.hpp"
|
|
||||||
|
|
||||||
std::string op_name(binop op) {
|
|
||||||
switch(op) {
|
|
||||||
case PLUS: return "+";
|
|
||||||
case MINUS: return "-";
|
|
||||||
case TIMES: return "*";
|
|
||||||
case DIVIDE: return "/";
|
|
||||||
}
|
|
||||||
return "??";
|
|
||||||
}
|
|
||||||
|
|
||||||
void print_indent(int n, std::ostream& to) {
|
|
||||||
while(n--) to << " ";
|
|
||||||
}
|
|
||||||
|
|
||||||
void ast_int::print(int indent, std::ostream& to) const {
|
|
||||||
print_indent(indent, to);
|
|
||||||
to << "INT: " << value << std::endl;
|
|
||||||
}
|
|
||||||
|
|
||||||
type_ptr ast_int::typecheck(type_mgr& mgr, const type_env& env) const {
|
|
||||||
return type_ptr(new type_base("Int"));
|
|
||||||
}
|
|
||||||
|
|
||||||
void ast_lid::print(int indent, std::ostream& to) const {
|
|
||||||
print_indent(indent, to);
|
|
||||||
to << "LID: " << id << std::endl;
|
|
||||||
}
|
|
||||||
|
|
||||||
type_ptr ast_lid::typecheck(type_mgr& mgr, const type_env& env) const {
|
|
||||||
return env.lookup(id);
|
|
||||||
}
|
|
||||||
|
|
||||||
void ast_uid::print(int indent, std::ostream& to) const {
|
|
||||||
print_indent(indent, to);
|
|
||||||
to << "UID: " << id << std::endl;
|
|
||||||
}
|
|
||||||
|
|
||||||
type_ptr ast_uid::typecheck(type_mgr& mgr, const type_env& env) const {
|
|
||||||
return env.lookup(id);
|
|
||||||
}
|
|
||||||
|
|
||||||
void ast_binop::print(int indent, std::ostream& to) const {
|
|
||||||
print_indent(indent, to);
|
|
||||||
to << "BINOP: " << op_name(op) << std::endl;
|
|
||||||
left->print(indent + 1, to);
|
|
||||||
right->print(indent + 1, to);
|
|
||||||
}
|
|
||||||
|
|
||||||
type_ptr ast_binop::typecheck(type_mgr& mgr, const type_env& env) const {
|
|
||||||
type_ptr ltype = left->typecheck(mgr, env);
|
|
||||||
type_ptr rtype = right->typecheck(mgr, env);
|
|
||||||
type_ptr ftype = env.lookup(op_name(op));
|
|
||||||
if(!ftype) throw type_error(std::string("unknown binary operator ") + op_name(op));
|
|
||||||
|
|
||||||
type_ptr return_type = mgr.new_type();
|
|
||||||
type_ptr arrow_one = type_ptr(new type_arr(rtype, return_type));
|
|
||||||
type_ptr arrow_two = type_ptr(new type_arr(ltype, arrow_one));
|
|
||||||
|
|
||||||
mgr.unify(arrow_two, ftype);
|
|
||||||
return return_type;
|
|
||||||
}
|
|
||||||
|
|
||||||
void ast_app::print(int indent, std::ostream& to) const {
|
|
||||||
print_indent(indent, to);
|
|
||||||
to << "APP:" << std::endl;
|
|
||||||
left->print(indent + 1, to);
|
|
||||||
right->print(indent + 1, to);
|
|
||||||
}
|
|
||||||
|
|
||||||
type_ptr ast_app::typecheck(type_mgr& mgr, const type_env& env) const {
|
|
||||||
type_ptr ltype = left->typecheck(mgr, env);
|
|
||||||
type_ptr rtype = right->typecheck(mgr, env);
|
|
||||||
|
|
||||||
type_ptr return_type = mgr.new_type();
|
|
||||||
type_ptr arrow = type_ptr(new type_arr(rtype, return_type));
|
|
||||||
mgr.unify(arrow, ltype);
|
|
||||||
return return_type;
|
|
||||||
}
|
|
||||||
|
|
||||||
void ast_case::print(int indent, std::ostream& to) const {
|
|
||||||
print_indent(indent, to);
|
|
||||||
to << "CASE: " << std::endl;
|
|
||||||
for(auto& branch : branches) {
|
|
||||||
print_indent(indent + 1, to);
|
|
||||||
branch->pat->print(to);
|
|
||||||
to << std::endl;
|
|
||||||
branch->expr->print(indent + 2, to);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
type_ptr ast_case::typecheck(type_mgr& mgr, const type_env& env) const {
|
|
||||||
type_var* var;
|
|
||||||
type_ptr case_type = mgr.resolve(of->typecheck(mgr, env), var);
|
|
||||||
type_ptr branch_type = mgr.new_type();
|
|
||||||
|
|
||||||
for(auto& branch : branches) {
|
|
||||||
type_env new_env = env.scope();
|
|
||||||
branch->pat->match(case_type, mgr, new_env);
|
|
||||||
type_ptr curr_branch_type = branch->expr->typecheck(mgr, new_env);
|
|
||||||
mgr.unify(branch_type, curr_branch_type);
|
|
||||||
}
|
|
||||||
|
|
||||||
case_type = mgr.resolve(case_type, var);
|
|
||||||
if(!dynamic_cast<type_base*>(case_type.get())) {
|
|
||||||
throw type_error("attempting case analysis of non-data type");
|
|
||||||
}
|
|
||||||
|
|
||||||
return branch_type;
|
|
||||||
}
|
|
||||||
|
|
||||||
void pattern_var::print(std::ostream& to) const {
|
|
||||||
to << var;
|
|
||||||
}
|
|
||||||
|
|
||||||
void pattern_var::match(type_ptr t, type_mgr& mgr, type_env& env) const {
|
|
||||||
env.bind(var, t);
|
|
||||||
}
|
|
||||||
|
|
||||||
void pattern_constr::print(std::ostream& to) const {
|
|
||||||
to << constr;
|
|
||||||
for(auto& param : params) {
|
|
||||||
to << " " << param;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
void pattern_constr::match(type_ptr t, type_mgr& mgr, type_env& env) const {
|
|
||||||
type_ptr constructor_type = env.lookup(constr);
|
|
||||||
if(!constructor_type) {
|
|
||||||
throw type_error(std::string("pattern using unknown constructor ") + constr);
|
|
||||||
}
|
|
||||||
|
|
||||||
for(int i = 0; i < params.size(); i++) {
|
|
||||||
type_arr* arr = dynamic_cast<type_arr*>(constructor_type.get());
|
|
||||||
if(!arr) throw type_error("too many parameters in constructor pattern");
|
|
||||||
|
|
||||||
env.bind(params[i], arr->left);
|
|
||||||
constructor_type = arr->right;
|
|
||||||
}
|
|
||||||
|
|
||||||
mgr.unify(t, constructor_type);
|
|
||||||
}
|
|
@ -1,172 +0,0 @@
|
|||||||
#pragma once
|
|
||||||
#include <memory>
|
|
||||||
#include <vector>
|
|
||||||
#include "type.hpp"
|
|
||||||
#include "env.hpp"
|
|
||||||
|
|
||||||
struct ast {
|
|
||||||
virtual ~ast() = default;
|
|
||||||
|
|
||||||
virtual void print(int indent, std::ostream& to) const = 0;
|
|
||||||
virtual type_ptr typecheck(type_mgr& mgr, const type_env& env) const = 0;
|
|
||||||
};
|
|
||||||
|
|
||||||
using ast_ptr = std::unique_ptr<ast>;
|
|
||||||
|
|
||||||
struct pattern {
|
|
||||||
virtual ~pattern() = default;
|
|
||||||
|
|
||||||
virtual void print(std::ostream& to) const = 0;
|
|
||||||
virtual void match(type_ptr t, type_mgr& mgr, type_env& env) const = 0;
|
|
||||||
};
|
|
||||||
|
|
||||||
using pattern_ptr = std::unique_ptr<pattern>;
|
|
||||||
|
|
||||||
struct branch {
|
|
||||||
pattern_ptr pat;
|
|
||||||
ast_ptr expr;
|
|
||||||
|
|
||||||
branch(pattern_ptr p, ast_ptr a)
|
|
||||||
: pat(std::move(p)), expr(std::move(a)) {}
|
|
||||||
};
|
|
||||||
|
|
||||||
using branch_ptr = std::unique_ptr<branch>;
|
|
||||||
|
|
||||||
struct constructor {
|
|
||||||
std::string name;
|
|
||||||
std::vector<std::string> types;
|
|
||||||
|
|
||||||
constructor(std::string n, std::vector<std::string> ts)
|
|
||||||
: name(std::move(n)), types(std::move(ts)) {}
|
|
||||||
};
|
|
||||||
|
|
||||||
using constructor_ptr = std::unique_ptr<constructor>;
|
|
||||||
|
|
||||||
struct definition {
|
|
||||||
virtual ~definition() = default;
|
|
||||||
|
|
||||||
virtual void typecheck_first(type_mgr& mgr, type_env& env) = 0;
|
|
||||||
virtual void typecheck_second(type_mgr& mgr, const type_env& env) const = 0;
|
|
||||||
};
|
|
||||||
|
|
||||||
using definition_ptr = std::unique_ptr<definition>;
|
|
||||||
|
|
||||||
enum binop {
|
|
||||||
PLUS,
|
|
||||||
MINUS,
|
|
||||||
TIMES,
|
|
||||||
DIVIDE
|
|
||||||
};
|
|
||||||
|
|
||||||
struct ast_int : public ast {
|
|
||||||
int value;
|
|
||||||
|
|
||||||
explicit ast_int(int v)
|
|
||||||
: value(v) {}
|
|
||||||
|
|
||||||
void print(int indent, std::ostream& to) const;
|
|
||||||
type_ptr typecheck(type_mgr& mgr, const type_env& env) const;
|
|
||||||
};
|
|
||||||
|
|
||||||
struct ast_lid : public ast {
|
|
||||||
std::string id;
|
|
||||||
|
|
||||||
explicit ast_lid(std::string i)
|
|
||||||
: id(std::move(i)) {}
|
|
||||||
|
|
||||||
void print(int indent, std::ostream& to) const;
|
|
||||||
type_ptr typecheck(type_mgr& mgr, const type_env& env) const;
|
|
||||||
};
|
|
||||||
|
|
||||||
struct ast_uid : public ast {
|
|
||||||
std::string id;
|
|
||||||
|
|
||||||
explicit ast_uid(std::string i)
|
|
||||||
: id(std::move(i)) {}
|
|
||||||
|
|
||||||
void print(int indent, std::ostream& to) const;
|
|
||||||
type_ptr typecheck(type_mgr& mgr, const type_env& env) const;
|
|
||||||
};
|
|
||||||
|
|
||||||
struct ast_binop : public ast {
|
|
||||||
binop op;
|
|
||||||
ast_ptr left;
|
|
||||||
ast_ptr right;
|
|
||||||
|
|
||||||
ast_binop(binop o, ast_ptr l, ast_ptr r)
|
|
||||||
: op(o), left(std::move(l)), right(std::move(r)) {}
|
|
||||||
|
|
||||||
void print(int indent, std::ostream& to) const;
|
|
||||||
type_ptr typecheck(type_mgr& mgr, const type_env& env) const;
|
|
||||||
};
|
|
||||||
|
|
||||||
struct ast_app : public ast {
|
|
||||||
ast_ptr left;
|
|
||||||
ast_ptr right;
|
|
||||||
|
|
||||||
ast_app(ast_ptr l, ast_ptr r)
|
|
||||||
: left(std::move(l)), right(std::move(r)) {}
|
|
||||||
|
|
||||||
void print(int indent, std::ostream& to) const;
|
|
||||||
type_ptr typecheck(type_mgr& mgr, const type_env& env) const;
|
|
||||||
};
|
|
||||||
|
|
||||||
struct ast_case : public ast {
|
|
||||||
ast_ptr of;
|
|
||||||
std::vector<branch_ptr> branches;
|
|
||||||
|
|
||||||
ast_case(ast_ptr o, std::vector<branch_ptr> b)
|
|
||||||
: of(std::move(o)), branches(std::move(b)) {}
|
|
||||||
|
|
||||||
void print(int indent, std::ostream& to) const;
|
|
||||||
type_ptr typecheck(type_mgr& mgr, const type_env& env) const;
|
|
||||||
};
|
|
||||||
|
|
||||||
struct pattern_var : public pattern {
|
|
||||||
std::string var;
|
|
||||||
|
|
||||||
pattern_var(std::string v)
|
|
||||||
: var(std::move(v)) {}
|
|
||||||
|
|
||||||
void print(std::ostream &to) const;
|
|
||||||
void match(type_ptr t, type_mgr& mgr, type_env& env) const;
|
|
||||||
};
|
|
||||||
|
|
||||||
struct pattern_constr : public pattern {
|
|
||||||
std::string constr;
|
|
||||||
std::vector<std::string> params;
|
|
||||||
|
|
||||||
pattern_constr(std::string c, std::vector<std::string> p)
|
|
||||||
: constr(std::move(c)), params(std::move(p)) {}
|
|
||||||
|
|
||||||
void print(std::ostream &to) const;
|
|
||||||
void match(type_ptr t, type_mgr&, type_env& env) const;
|
|
||||||
};
|
|
||||||
|
|
||||||
struct definition_defn : public definition {
|
|
||||||
std::string name;
|
|
||||||
std::vector<std::string> params;
|
|
||||||
ast_ptr body;
|
|
||||||
|
|
||||||
type_ptr return_type;
|
|
||||||
std::vector<type_ptr> param_types;
|
|
||||||
|
|
||||||
definition_defn(std::string n, std::vector<std::string> p, ast_ptr b)
|
|
||||||
: name(std::move(n)), params(std::move(p)), body(std::move(b)) {
|
|
||||||
|
|
||||||
}
|
|
||||||
|
|
||||||
void typecheck_first(type_mgr& mgr, type_env& env);
|
|
||||||
void typecheck_second(type_mgr& mgr, const type_env& env) const;
|
|
||||||
};
|
|
||||||
|
|
||||||
struct definition_data : public definition {
|
|
||||||
std::string name;
|
|
||||||
std::vector<constructor_ptr> constructors;
|
|
||||||
|
|
||||||
definition_data(std::string n, std::vector<constructor_ptr> cs)
|
|
||||||
: name(std::move(n)), constructors(std::move(cs)) {}
|
|
||||||
|
|
||||||
void typecheck_first(type_mgr& mgr, type_env& env);
|
|
||||||
void typecheck_second(type_mgr& mgr, const type_env& env) const;
|
|
||||||
};
|
|
@ -1,48 +0,0 @@
|
|||||||
#include "ast.hpp"
|
|
||||||
|
|
||||||
void definition_defn::typecheck_first(type_mgr& mgr, type_env& env) {
|
|
||||||
return_type = mgr.new_type();
|
|
||||||
type_ptr full_type = return_type;
|
|
||||||
|
|
||||||
for(auto it = params.rbegin(); it != params.rend(); it++) {
|
|
||||||
type_ptr param_type = mgr.new_type();
|
|
||||||
full_type = type_ptr(new type_arr(param_type, full_type));
|
|
||||||
param_types.push_back(param_type);
|
|
||||||
}
|
|
||||||
|
|
||||||
env.bind(name, full_type);
|
|
||||||
}
|
|
||||||
|
|
||||||
void definition_defn::typecheck_second(type_mgr& mgr, const type_env& env) const {
|
|
||||||
type_env new_env = env.scope();
|
|
||||||
auto param_it = params.begin();
|
|
||||||
auto type_it = param_types.rbegin();
|
|
||||||
|
|
||||||
while(param_it != params.end() && type_it != param_types.rend()) {
|
|
||||||
new_env.bind(*param_it, *type_it);
|
|
||||||
param_it++;
|
|
||||||
type_it++;
|
|
||||||
}
|
|
||||||
|
|
||||||
type_ptr body_type = body->typecheck(mgr, new_env);
|
|
||||||
mgr.unify(return_type, body_type);
|
|
||||||
}
|
|
||||||
|
|
||||||
void definition_data::typecheck_first(type_mgr& mgr, type_env& env) {
|
|
||||||
type_ptr return_type = type_ptr(new type_base(name));
|
|
||||||
|
|
||||||
for(auto& constructor : constructors) {
|
|
||||||
type_ptr full_type = return_type;
|
|
||||||
|
|
||||||
for(auto it = constructor->types.rbegin(); it != constructor->types.rend(); it++) {
|
|
||||||
type_ptr type = type_ptr(new type_base(*it));
|
|
||||||
full_type = type_ptr(new type_arr(type, full_type));
|
|
||||||
}
|
|
||||||
|
|
||||||
env.bind(constructor->name, full_type);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
void definition_data::typecheck_second(type_mgr& mgr, const type_env& env) const {
|
|
||||||
// Nothing
|
|
||||||
}
|
|
@ -1,16 +0,0 @@
|
|||||||
#include "env.hpp"
|
|
||||||
|
|
||||||
type_ptr type_env::lookup(const std::string& name) const {
|
|
||||||
auto it = names.find(name);
|
|
||||||
if(it != names.end()) return it->second;
|
|
||||||
if(parent) return parent->lookup(name);
|
|
||||||
return nullptr;
|
|
||||||
}
|
|
||||||
|
|
||||||
void type_env::bind(const std::string& name, type_ptr t) {
|
|
||||||
names[name] = t;
|
|
||||||
}
|
|
||||||
|
|
||||||
type_env type_env::scope() const {
|
|
||||||
return type_env(this);
|
|
||||||
}
|
|
@ -1,16 +0,0 @@
|
|||||||
#pragma once
|
|
||||||
#include <map>
|
|
||||||
#include "type.hpp"
|
|
||||||
|
|
||||||
struct type_env {
|
|
||||||
std::map<std::string, type_ptr> names;
|
|
||||||
type_env const* parent = nullptr;
|
|
||||||
|
|
||||||
type_env(type_env const* p)
|
|
||||||
: parent(p) {}
|
|
||||||
type_env() : type_env(nullptr) {}
|
|
||||||
|
|
||||||
type_ptr lookup(const std::string& name) const;
|
|
||||||
void bind(const std::string& name, type_ptr t);
|
|
||||||
type_env scope() const;
|
|
||||||
};
|
|
@ -1,5 +0,0 @@
|
|||||||
#include "error.hpp"
|
|
||||||
|
|
||||||
const char* type_error::what() const noexcept {
|
|
||||||
return "an error occured while checking the types of the program";
|
|
||||||
}
|
|
@ -1,21 +0,0 @@
|
|||||||
#pragma once
|
|
||||||
#include <exception>
|
|
||||||
#include "type.hpp"
|
|
||||||
|
|
||||||
struct type_error : std::exception {
|
|
||||||
std::string description;
|
|
||||||
|
|
||||||
type_error(std::string d)
|
|
||||||
: description(std::move(d)) {}
|
|
||||||
|
|
||||||
const char* what() const noexcept override;
|
|
||||||
};
|
|
||||||
|
|
||||||
struct unification_error : public type_error {
|
|
||||||
type_ptr left;
|
|
||||||
type_ptr right;
|
|
||||||
|
|
||||||
unification_error(type_ptr l, type_ptr r)
|
|
||||||
: left(std::move(l)), right(std::move(r)),
|
|
||||||
type_error("failed to unify types") {}
|
|
||||||
};
|
|
@ -1,2 +0,0 @@
|
|||||||
data Bool = { True, False }
|
|
||||||
defn main = { 3 + True }
|
|
@ -1 +0,0 @@
|
|||||||
defn main = { 1 2 3 4 5 }
|
|
@ -1,2 +0,0 @@
|
|||||||
defn main = { plus 320 6 }
|
|
||||||
defn plus x y = { x + y }
|
|
@ -1,3 +0,0 @@
|
|||||||
defn add x y = { x + y }
|
|
||||||
defn double x = { add x x }
|
|
||||||
defn main = { double 163 }
|
|
@ -1,7 +0,0 @@
|
|||||||
data List = { Nil, Cons Int List }
|
|
||||||
defn length l = {
|
|
||||||
case l of {
|
|
||||||
Nil -> { 0 }
|
|
||||||
Cons x xs -> { 1 + length xs }
|
|
||||||
}
|
|
||||||
}
|
|
@ -1,70 +0,0 @@
|
|||||||
#include "ast.hpp"
|
|
||||||
#include <iostream>
|
|
||||||
#include "parser.hpp"
|
|
||||||
#include "error.hpp"
|
|
||||||
#include "type.hpp"
|
|
||||||
|
|
||||||
void yy::parser::error(const std::string& msg) {
|
|
||||||
std::cout << "An error occured: " << msg << std::endl;
|
|
||||||
}
|
|
||||||
|
|
||||||
extern std::vector<definition_ptr> program;
|
|
||||||
|
|
||||||
void typecheck_program(
|
|
||||||
const std::vector<definition_ptr>& prog,
|
|
||||||
type_mgr& mgr, type_env& env) {
|
|
||||||
type_ptr int_type = type_ptr(new type_base("Int"));
|
|
||||||
type_ptr binop_type = type_ptr(new type_arr(
|
|
||||||
int_type,
|
|
||||||
type_ptr(new type_arr(int_type, int_type))));
|
|
||||||
|
|
||||||
env.bind("+", binop_type);
|
|
||||||
env.bind("-", binop_type);
|
|
||||||
env.bind("*", binop_type);
|
|
||||||
env.bind("/", binop_type);
|
|
||||||
|
|
||||||
for(auto& def : prog) {
|
|
||||||
def->typecheck_first(mgr, env);
|
|
||||||
}
|
|
||||||
|
|
||||||
for(auto& def : prog) {
|
|
||||||
def->typecheck_second(mgr, env);
|
|
||||||
}
|
|
||||||
|
|
||||||
for(auto& pair : env.names) {
|
|
||||||
std::cout << pair.first << ": ";
|
|
||||||
pair.second->print(mgr, std::cout);
|
|
||||||
std::cout << std::endl;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
int main() {
|
|
||||||
yy::parser parser;
|
|
||||||
type_mgr mgr;
|
|
||||||
type_env env;
|
|
||||||
|
|
||||||
parser.parse();
|
|
||||||
for(auto& definition : program) {
|
|
||||||
definition_defn* def = dynamic_cast<definition_defn*>(definition.get());
|
|
||||||
if(!def) continue;
|
|
||||||
|
|
||||||
std::cout << def->name;
|
|
||||||
for(auto& param : def->params) std::cout << " " << param;
|
|
||||||
std::cout << ":" << std::endl;
|
|
||||||
|
|
||||||
def->body->print(1, std::cout);
|
|
||||||
}
|
|
||||||
try {
|
|
||||||
typecheck_program(program, mgr, env);
|
|
||||||
} catch(unification_error& err) {
|
|
||||||
std::cout << "failed to unify types: " << std::endl;
|
|
||||||
std::cout << " (1) \033[34m";
|
|
||||||
err.left->print(mgr, std::cout);
|
|
||||||
std::cout << "\033[0m" << std::endl;
|
|
||||||
std::cout << " (2) \033[32m";
|
|
||||||
err.right->print(mgr, std::cout);
|
|
||||||
std::cout << "\033[0m" << std::endl;
|
|
||||||
} catch(type_error& err) {
|
|
||||||
std::cout << "failed to type check program: " << err.description << std::endl;
|
|
||||||
}
|
|
||||||
}
|
|
@ -1,140 +0,0 @@
|
|||||||
%{
|
|
||||||
#include <string>
|
|
||||||
#include <iostream>
|
|
||||||
#include "ast.hpp"
|
|
||||||
#include "parser.hpp"
|
|
||||||
|
|
||||||
std::vector<definition_ptr> program;
|
|
||||||
extern yy::parser::symbol_type yylex();
|
|
||||||
|
|
||||||
%}
|
|
||||||
|
|
||||||
%token PLUS
|
|
||||||
%token TIMES
|
|
||||||
%token MINUS
|
|
||||||
%token DIVIDE
|
|
||||||
%token <int> INT
|
|
||||||
%token DEFN
|
|
||||||
%token DATA
|
|
||||||
%token CASE
|
|
||||||
%token OF
|
|
||||||
%token OCURLY
|
|
||||||
%token CCURLY
|
|
||||||
%token OPAREN
|
|
||||||
%token CPAREN
|
|
||||||
%token COMMA
|
|
||||||
%token ARROW
|
|
||||||
%token EQUAL
|
|
||||||
%token <std::string> LID
|
|
||||||
%token <std::string> UID
|
|
||||||
|
|
||||||
%language "c++"
|
|
||||||
%define api.value.type variant
|
|
||||||
%define api.token.constructor
|
|
||||||
|
|
||||||
%type <std::vector<std::string>> lowercaseParams uppercaseParams
|
|
||||||
%type <std::vector<definition_ptr>> program definitions
|
|
||||||
%type <std::vector<branch_ptr>> branches
|
|
||||||
%type <std::vector<constructor_ptr>> constructors
|
|
||||||
%type <ast_ptr> aAdd aMul case app appBase
|
|
||||||
%type <definition_ptr> definition defn data
|
|
||||||
%type <branch_ptr> branch
|
|
||||||
%type <pattern_ptr> pattern
|
|
||||||
%type <constructor_ptr> constructor
|
|
||||||
|
|
||||||
%start program
|
|
||||||
|
|
||||||
%%
|
|
||||||
|
|
||||||
program
|
|
||||||
: definitions { program = std::move($1); }
|
|
||||||
;
|
|
||||||
|
|
||||||
definitions
|
|
||||||
: definitions definition { $$ = std::move($1); $$.push_back(std::move($2)); }
|
|
||||||
| definition { $$ = std::vector<definition_ptr>(); $$.push_back(std::move($1)); }
|
|
||||||
;
|
|
||||||
|
|
||||||
definition
|
|
||||||
: defn { $$ = std::move($1); }
|
|
||||||
| data { $$ = std::move($1); }
|
|
||||||
;
|
|
||||||
|
|
||||||
defn
|
|
||||||
: DEFN LID lowercaseParams EQUAL OCURLY aAdd CCURLY
|
|
||||||
{ $$ = definition_ptr(
|
|
||||||
new definition_defn(std::move($2), std::move($3), std::move($6))); }
|
|
||||||
;
|
|
||||||
|
|
||||||
lowercaseParams
|
|
||||||
: %empty { $$ = std::vector<std::string>(); }
|
|
||||||
| lowercaseParams LID { $$ = std::move($1); $$.push_back(std::move($2)); }
|
|
||||||
;
|
|
||||||
|
|
||||||
uppercaseParams
|
|
||||||
: %empty { $$ = std::vector<std::string>(); }
|
|
||||||
| uppercaseParams UID { $$ = std::move($1); $$.push_back(std::move($2)); }
|
|
||||||
;
|
|
||||||
|
|
||||||
aAdd
|
|
||||||
: aAdd PLUS aMul { $$ = ast_ptr(new ast_binop(PLUS, std::move($1), std::move($3))); }
|
|
||||||
| aAdd MINUS aMul { $$ = ast_ptr(new ast_binop(MINUS, std::move($1), std::move($3))); }
|
|
||||||
| aMul { $$ = std::move($1); }
|
|
||||||
;
|
|
||||||
|
|
||||||
aMul
|
|
||||||
: aMul TIMES app { $$ = ast_ptr(new ast_binop(TIMES, std::move($1), std::move($3))); }
|
|
||||||
| aMul DIVIDE app { $$ = ast_ptr(new ast_binop(DIVIDE, std::move($1), std::move($3))); }
|
|
||||||
| app { $$ = std::move($1); }
|
|
||||||
;
|
|
||||||
|
|
||||||
app
|
|
||||||
: app appBase { $$ = ast_ptr(new ast_app(std::move($1), std::move($2))); }
|
|
||||||
| appBase { $$ = std::move($1); }
|
|
||||||
;
|
|
||||||
|
|
||||||
appBase
|
|
||||||
: INT { $$ = ast_ptr(new ast_int($1)); }
|
|
||||||
| LID { $$ = ast_ptr(new ast_lid(std::move($1))); }
|
|
||||||
| UID { $$ = ast_ptr(new ast_uid(std::move($1))); }
|
|
||||||
| OPAREN aAdd CPAREN { $$ = std::move($2); }
|
|
||||||
| case { $$ = std::move($1); }
|
|
||||||
;
|
|
||||||
|
|
||||||
case
|
|
||||||
: CASE aAdd OF OCURLY branches CCURLY
|
|
||||||
{ $$ = ast_ptr(new ast_case(std::move($2), std::move($5))); }
|
|
||||||
;
|
|
||||||
|
|
||||||
branches
|
|
||||||
: branches branch { $$ = std::move($1); $$.push_back(std::move($2)); }
|
|
||||||
| branch { $$ = std::vector<branch_ptr>(); $$.push_back(std::move($1));}
|
|
||||||
;
|
|
||||||
|
|
||||||
branch
|
|
||||||
: pattern ARROW OCURLY aAdd CCURLY
|
|
||||||
{ $$ = branch_ptr(new branch(std::move($1), std::move($4))); }
|
|
||||||
;
|
|
||||||
|
|
||||||
pattern
|
|
||||||
: LID { $$ = pattern_ptr(new pattern_var(std::move($1))); }
|
|
||||||
| UID lowercaseParams
|
|
||||||
{ $$ = pattern_ptr(new pattern_constr(std::move($1), std::move($2))); }
|
|
||||||
;
|
|
||||||
|
|
||||||
data
|
|
||||||
: DATA UID EQUAL OCURLY constructors CCURLY
|
|
||||||
{ $$ = definition_ptr(new definition_data(std::move($2), std::move($5))); }
|
|
||||||
;
|
|
||||||
|
|
||||||
constructors
|
|
||||||
: constructors COMMA constructor { $$ = std::move($1); $$.push_back(std::move($3)); }
|
|
||||||
| constructor
|
|
||||||
{ $$ = std::vector<constructor_ptr>(); $$.push_back(std::move($1)); }
|
|
||||||
;
|
|
||||||
|
|
||||||
constructor
|
|
||||||
: UID uppercaseParams
|
|
||||||
{ $$ = constructor_ptr(new constructor(std::move($1), std::move($2))); }
|
|
||||||
;
|
|
||||||
|
|
@ -1,34 +0,0 @@
|
|||||||
%option noyywrap
|
|
||||||
|
|
||||||
%{
|
|
||||||
#include <iostream>
|
|
||||||
#include "ast.hpp"
|
|
||||||
#include "parser.hpp"
|
|
||||||
|
|
||||||
#define YY_DECL yy::parser::symbol_type yylex()
|
|
||||||
|
|
||||||
%}
|
|
||||||
|
|
||||||
%%
|
|
||||||
|
|
||||||
[ \n]+ {}
|
|
||||||
\+ { return yy::parser::make_PLUS(); }
|
|
||||||
\* { return yy::parser::make_TIMES(); }
|
|
||||||
- { return yy::parser::make_MINUS(); }
|
|
||||||
\/ { return yy::parser::make_DIVIDE(); }
|
|
||||||
[0-9]+ { return yy::parser::make_INT(atoi(yytext)); }
|
|
||||||
defn { return yy::parser::make_DEFN(); }
|
|
||||||
data { return yy::parser::make_DATA(); }
|
|
||||||
case { return yy::parser::make_CASE(); }
|
|
||||||
of { return yy::parser::make_OF(); }
|
|
||||||
\{ { return yy::parser::make_OCURLY(); }
|
|
||||||
\} { return yy::parser::make_CCURLY(); }
|
|
||||||
\( { return yy::parser::make_OPAREN(); }
|
|
||||||
\) { return yy::parser::make_CPAREN(); }
|
|
||||||
, { return yy::parser::make_COMMA(); }
|
|
||||||
-> { return yy::parser::make_ARROW(); }
|
|
||||||
= { return yy::parser::make_EQUAL(); }
|
|
||||||
[a-z][a-zA-Z]* { return yy::parser::make_LID(std::string(yytext)); }
|
|
||||||
[A-Z][a-zA-Z]* { return yy::parser::make_UID(std::string(yytext)); }
|
|
||||||
|
|
||||||
%%
|
|
@ -1,99 +0,0 @@
|
|||||||
#include "type.hpp"
|
|
||||||
#include <sstream>
|
|
||||||
#include <algorithm>
|
|
||||||
#include "error.hpp"
|
|
||||||
|
|
||||||
void type_var::print(const type_mgr& mgr, std::ostream& to) const {
|
|
||||||
auto it = mgr.types.find(name);
|
|
||||||
if(it != mgr.types.end()) {
|
|
||||||
it->second->print(mgr, to);
|
|
||||||
} else {
|
|
||||||
to << name;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
void type_base::print(const type_mgr& mgr, std::ostream& to) const {
|
|
||||||
to << name;
|
|
||||||
}
|
|
||||||
|
|
||||||
void type_arr::print(const type_mgr& mgr, std::ostream& to) const {
|
|
||||||
left->print(mgr, to);
|
|
||||||
to << " -> (";
|
|
||||||
right->print(mgr, to);
|
|
||||||
to << ")";
|
|
||||||
}
|
|
||||||
|
|
||||||
std::string type_mgr::new_type_name() {
|
|
||||||
int temp = last_id++;
|
|
||||||
std::string str = "";
|
|
||||||
|
|
||||||
while(temp != -1) {
|
|
||||||
str += (char) ('a' + (temp % 26));
|
|
||||||
temp = temp / 26 - 1;
|
|
||||||
}
|
|
||||||
|
|
||||||
std::reverse(str.begin(), str.end());
|
|
||||||
return str;
|
|
||||||
}
|
|
||||||
|
|
||||||
type_ptr type_mgr::new_type() {
|
|
||||||
return type_ptr(new type_var(new_type_name()));
|
|
||||||
}
|
|
||||||
|
|
||||||
type_ptr type_mgr::new_arrow_type() {
|
|
||||||
return type_ptr(new type_arr(new_type(), new_type()));
|
|
||||||
}
|
|
||||||
|
|
||||||
type_ptr type_mgr::resolve(type_ptr t, type_var*& var) {
|
|
||||||
type_var* cast;
|
|
||||||
|
|
||||||
var = nullptr;
|
|
||||||
while((cast = dynamic_cast<type_var*>(t.get()))) {
|
|
||||||
auto it = types.find(cast->name);
|
|
||||||
|
|
||||||
if(it == types.end()) {
|
|
||||||
var = cast;
|
|
||||||
break;
|
|
||||||
}
|
|
||||||
t = it->second;
|
|
||||||
}
|
|
||||||
|
|
||||||
return t;
|
|
||||||
}
|
|
||||||
|
|
||||||
void type_mgr::unify(type_ptr l, type_ptr r) {
|
|
||||||
type_var* lvar;
|
|
||||||
type_var* rvar;
|
|
||||||
type_arr* larr;
|
|
||||||
type_arr* rarr;
|
|
||||||
type_base* lid;
|
|
||||||
type_base* rid;
|
|
||||||
|
|
||||||
l = resolve(l, lvar);
|
|
||||||
r = resolve(r, rvar);
|
|
||||||
|
|
||||||
if(lvar) {
|
|
||||||
bind(lvar->name, r);
|
|
||||||
return;
|
|
||||||
} else if(rvar) {
|
|
||||||
bind(rvar->name, l);
|
|
||||||
return;
|
|
||||||
} else if((larr = dynamic_cast<type_arr*>(l.get())) &&
|
|
||||||
(rarr = dynamic_cast<type_arr*>(r.get()))) {
|
|
||||||
unify(larr->left, rarr->left);
|
|
||||||
unify(larr->right, rarr->right);
|
|
||||||
return;
|
|
||||||
} else if((lid = dynamic_cast<type_base*>(l.get())) &&
|
|
||||||
(rid = dynamic_cast<type_base*>(r.get()))) {
|
|
||||||
if(lid->name == rid->name) return;
|
|
||||||
}
|
|
||||||
|
|
||||||
throw unification_error(l, r);
|
|
||||||
}
|
|
||||||
|
|
||||||
void type_mgr::bind(const std::string& s, type_ptr t) {
|
|
||||||
type_var* other = dynamic_cast<type_var*>(t.get());
|
|
||||||
|
|
||||||
if(other && other->name == s) return;
|
|
||||||
types[s] = t;
|
|
||||||
}
|
|
@ -1,54 +0,0 @@
|
|||||||
#pragma once
|
|
||||||
#include <memory>
|
|
||||||
#include <map>
|
|
||||||
|
|
||||||
struct type_mgr;
|
|
||||||
|
|
||||||
struct type {
|
|
||||||
virtual ~type() = default;
|
|
||||||
|
|
||||||
virtual void print(const type_mgr& mgr, std::ostream& to) const = 0;
|
|
||||||
};
|
|
||||||
|
|
||||||
using type_ptr = std::shared_ptr<type>;
|
|
||||||
|
|
||||||
struct type_var : public type {
|
|
||||||
std::string name;
|
|
||||||
|
|
||||||
type_var(std::string n)
|
|
||||||
: name(std::move(n)) {}
|
|
||||||
|
|
||||||
void print(const type_mgr& mgr, std::ostream& to) const;
|
|
||||||
};
|
|
||||||
|
|
||||||
struct type_base : public type {
|
|
||||||
std::string name;
|
|
||||||
|
|
||||||
type_base(std::string n)
|
|
||||||
: name(std::move(n)) {}
|
|
||||||
|
|
||||||
void print(const type_mgr& mgr, std::ostream& to) const;
|
|
||||||
};
|
|
||||||
|
|
||||||
struct type_arr : public type {
|
|
||||||
type_ptr left;
|
|
||||||
type_ptr right;
|
|
||||||
|
|
||||||
type_arr(type_ptr l, type_ptr r)
|
|
||||||
: left(std::move(l)), right(std::move(r)) {}
|
|
||||||
|
|
||||||
void print(const type_mgr& mgr, std::ostream& to) const;
|
|
||||||
};
|
|
||||||
|
|
||||||
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);
|
|
||||||
};
|
|
@ -1,28 +0,0 @@
|
|||||||
cmake_minimum_required(VERSION 3.1)
|
|
||||||
project(compiler)
|
|
||||||
|
|
||||||
find_package(BISON)
|
|
||||||
find_package(FLEX)
|
|
||||||
bison_target(parser
|
|
||||||
${CMAKE_CURRENT_SOURCE_DIR}/parser.y
|
|
||||||
${CMAKE_CURRENT_BINARY_DIR}/parser.cpp
|
|
||||||
COMPILE_FLAGS "-d")
|
|
||||||
flex_target(scanner
|
|
||||||
${CMAKE_CURRENT_SOURCE_DIR}/scanner.l
|
|
||||||
${CMAKE_CURRENT_BINARY_DIR}/scanner.cpp)
|
|
||||||
add_flex_bison_dependency(scanner parser)
|
|
||||||
|
|
||||||
add_executable(compiler
|
|
||||||
ast.cpp ast.hpp definition.cpp
|
|
||||||
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})
|
|
@ -1,262 +0,0 @@
|
|||||||
#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);
|
|
||||||
}
|
|
@ -1,197 +0,0 @@
|
|||||||
#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();
|
|
||||||
};
|
|
@ -1,21 +0,0 @@
|
|||||||
#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 "??";
|
|
||||||
}
|
|
@ -1,12 +0,0 @@
|
|||||||
#pragma once
|
|
||||||
#include <string>
|
|
||||||
|
|
||||||
enum binop {
|
|
||||||
PLUS,
|
|
||||||
MINUS,
|
|
||||||
TIMES,
|
|
||||||
DIVIDE
|
|
||||||
};
|
|
||||||
|
|
||||||
std::string op_name(binop op);
|
|
||||||
std::string op_action(binop op);
|
|
@ -1,83 +0,0 @@
|
|||||||
#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() {
|
|
||||||
|
|
||||||
}
|
|
@ -1,23 +0,0 @@
|
|||||||
#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;
|
|
||||||
}
|
|
@ -1,34 +0,0 @@
|
|||||||
#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;
|
|
||||||
};
|
|
@ -1,5 +0,0 @@
|
|||||||
#include "error.hpp"
|
|
||||||
|
|
||||||
const char* type_error::what() const noexcept {
|
|
||||||
return "an error occured while checking the types of the program";
|
|
||||||
}
|
|
@ -1,21 +0,0 @@
|
|||||||
#pragma once
|
|
||||||
#include <exception>
|
|
||||||
#include "type.hpp"
|
|
||||||
|
|
||||||
struct type_error : std::exception {
|
|
||||||
std::string description;
|
|
||||||
|
|
||||||
type_error(std::string d)
|
|
||||||
: description(std::move(d)) {}
|
|
||||||
|
|
||||||
const char* what() const noexcept override;
|
|
||||||
};
|
|
||||||
|
|
||||||
struct unification_error : public type_error {
|
|
||||||
type_ptr left;
|
|
||||||
type_ptr right;
|
|
||||||
|
|
||||||
unification_error(type_ptr l, type_ptr r)
|
|
||||||
: left(std::move(l)), right(std::move(r)),
|
|
||||||
type_error("failed to unify types") {}
|
|
||||||
};
|
|
@ -1,2 +0,0 @@
|
|||||||
data Bool = { True, False }
|
|
||||||
defn main = { 3 + True }
|
|
@ -1 +0,0 @@
|
|||||||
defn main = { 1 2 3 4 5 }
|
|
@ -1,8 +0,0 @@
|
|||||||
data List = { Nil, Cons Int List }
|
|
||||||
|
|
||||||
defn head l = {
|
|
||||||
case l of {
|
|
||||||
Nil -> { 0 }
|
|
||||||
Cons x y z -> { x }
|
|
||||||
}
|
|
||||||
}
|
|
@ -1,2 +0,0 @@
|
|||||||
defn main = { plus 320 6 }
|
|
||||||
defn plus x y = { x + y }
|
|
@ -1,3 +0,0 @@
|
|||||||
defn add x y = { x + y }
|
|
||||||
defn double x = { add x x }
|
|
||||||
defn main = { double 163 }
|
|
@ -1,7 +0,0 @@
|
|||||||
data List = { Nil, Cons Int List }
|
|
||||||
defn length l = {
|
|
||||||
case l of {
|
|
||||||
Nil -> { 0 }
|
|
||||||
Cons x xs -> { 1 + length xs }
|
|
||||||
}
|
|
||||||
}
|
|
@ -1,83 +0,0 @@
|
|||||||
#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;
|
|
||||||
}
|
|
@ -1,120 +0,0 @@
|
|||||||
#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;
|
|
||||||
};
|
|
@ -1,88 +0,0 @@
|
|||||||
#include "ast.hpp"
|
|
||||||
#include <iostream>
|
|
||||||
#include "parser.hpp"
|
|
||||||
#include "error.hpp"
|
|
||||||
#include "type.hpp"
|
|
||||||
|
|
||||||
void yy::parser::error(const std::string& msg) {
|
|
||||||
std::cout << "An error occured: " << msg << std::endl;
|
|
||||||
}
|
|
||||||
|
|
||||||
extern std::vector<definition_ptr> program;
|
|
||||||
|
|
||||||
void typecheck_program(
|
|
||||||
const std::vector<definition_ptr>& prog,
|
|
||||||
type_mgr& mgr, type_env& env) {
|
|
||||||
type_ptr int_type = type_ptr(new type_base("Int"));
|
|
||||||
type_ptr binop_type = type_ptr(new type_arr(
|
|
||||||
int_type,
|
|
||||||
type_ptr(new type_arr(int_type, int_type))));
|
|
||||||
|
|
||||||
env.bind("+", binop_type);
|
|
||||||
env.bind("-", binop_type);
|
|
||||||
env.bind("*", binop_type);
|
|
||||||
env.bind("/", binop_type);
|
|
||||||
|
|
||||||
for(auto& def : prog) {
|
|
||||||
def->typecheck_first(mgr, env);
|
|
||||||
}
|
|
||||||
|
|
||||||
for(auto& def : prog) {
|
|
||||||
def->typecheck_second(mgr, env);
|
|
||||||
}
|
|
||||||
|
|
||||||
for(auto& pair : env.names) {
|
|
||||||
std::cout << pair.first << ": ";
|
|
||||||
pair.second->print(mgr, std::cout);
|
|
||||||
std::cout << std::endl;
|
|
||||||
}
|
|
||||||
|
|
||||||
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;
|
|
||||||
}
|
|
||||||
}
|
|
@ -1,140 +0,0 @@
|
|||||||
%{
|
|
||||||
#include <string>
|
|
||||||
#include <iostream>
|
|
||||||
#include "ast.hpp"
|
|
||||||
#include "parser.hpp"
|
|
||||||
|
|
||||||
std::vector<definition_ptr> program;
|
|
||||||
extern yy::parser::symbol_type yylex();
|
|
||||||
|
|
||||||
%}
|
|
||||||
|
|
||||||
%token PLUS
|
|
||||||
%token TIMES
|
|
||||||
%token MINUS
|
|
||||||
%token DIVIDE
|
|
||||||
%token <int> INT
|
|
||||||
%token DEFN
|
|
||||||
%token DATA
|
|
||||||
%token CASE
|
|
||||||
%token OF
|
|
||||||
%token OCURLY
|
|
||||||
%token CCURLY
|
|
||||||
%token OPAREN
|
|
||||||
%token CPAREN
|
|
||||||
%token COMMA
|
|
||||||
%token ARROW
|
|
||||||
%token EQUAL
|
|
||||||
%token <std::string> LID
|
|
||||||
%token <std::string> UID
|
|
||||||
|
|
||||||
%language "c++"
|
|
||||||
%define api.value.type variant
|
|
||||||
%define api.token.constructor
|
|
||||||
|
|
||||||
%type <std::vector<std::string>> lowercaseParams uppercaseParams
|
|
||||||
%type <std::vector<definition_ptr>> program definitions
|
|
||||||
%type <std::vector<branch_ptr>> branches
|
|
||||||
%type <std::vector<constructor_ptr>> constructors
|
|
||||||
%type <ast_ptr> aAdd aMul case app appBase
|
|
||||||
%type <definition_ptr> definition defn data
|
|
||||||
%type <branch_ptr> branch
|
|
||||||
%type <pattern_ptr> pattern
|
|
||||||
%type <constructor_ptr> constructor
|
|
||||||
|
|
||||||
%start program
|
|
||||||
|
|
||||||
%%
|
|
||||||
|
|
||||||
program
|
|
||||||
: definitions { program = std::move($1); }
|
|
||||||
;
|
|
||||||
|
|
||||||
definitions
|
|
||||||
: definitions definition { $$ = std::move($1); $$.push_back(std::move($2)); }
|
|
||||||
| definition { $$ = std::vector<definition_ptr>(); $$.push_back(std::move($1)); }
|
|
||||||
;
|
|
||||||
|
|
||||||
definition
|
|
||||||
: defn { $$ = std::move($1); }
|
|
||||||
| data { $$ = std::move($1); }
|
|
||||||
;
|
|
||||||
|
|
||||||
defn
|
|
||||||
: DEFN LID lowercaseParams EQUAL OCURLY aAdd CCURLY
|
|
||||||
{ $$ = definition_ptr(
|
|
||||||
new definition_defn(std::move($2), std::move($3), std::move($6))); }
|
|
||||||
;
|
|
||||||
|
|
||||||
lowercaseParams
|
|
||||||
: %empty { $$ = std::vector<std::string>(); }
|
|
||||||
| lowercaseParams LID { $$ = std::move($1); $$.push_back(std::move($2)); }
|
|
||||||
;
|
|
||||||
|
|
||||||
uppercaseParams
|
|
||||||
: %empty { $$ = std::vector<std::string>(); }
|
|
||||||
| uppercaseParams UID { $$ = std::move($1); $$.push_back(std::move($2)); }
|
|
||||||
;
|
|
||||||
|
|
||||||
aAdd
|
|
||||||
: aAdd PLUS aMul { $$ = ast_ptr(new ast_binop(PLUS, std::move($1), std::move($3))); }
|
|
||||||
| aAdd MINUS aMul { $$ = ast_ptr(new ast_binop(MINUS, std::move($1), std::move($3))); }
|
|
||||||
| aMul { $$ = std::move($1); }
|
|
||||||
;
|
|
||||||
|
|
||||||
aMul
|
|
||||||
: aMul TIMES app { $$ = ast_ptr(new ast_binop(TIMES, std::move($1), std::move($3))); }
|
|
||||||
| aMul DIVIDE app { $$ = ast_ptr(new ast_binop(DIVIDE, std::move($1), std::move($3))); }
|
|
||||||
| app { $$ = std::move($1); }
|
|
||||||
;
|
|
||||||
|
|
||||||
app
|
|
||||||
: app appBase { $$ = ast_ptr(new ast_app(std::move($1), std::move($2))); }
|
|
||||||
| appBase { $$ = std::move($1); }
|
|
||||||
;
|
|
||||||
|
|
||||||
appBase
|
|
||||||
: INT { $$ = ast_ptr(new ast_int($1)); }
|
|
||||||
| LID { $$ = ast_ptr(new ast_lid(std::move($1))); }
|
|
||||||
| UID { $$ = ast_ptr(new ast_uid(std::move($1))); }
|
|
||||||
| OPAREN aAdd CPAREN { $$ = std::move($2); }
|
|
||||||
| case { $$ = std::move($1); }
|
|
||||||
;
|
|
||||||
|
|
||||||
case
|
|
||||||
: CASE aAdd OF OCURLY branches CCURLY
|
|
||||||
{ $$ = ast_ptr(new ast_case(std::move($2), std::move($5))); }
|
|
||||||
;
|
|
||||||
|
|
||||||
branches
|
|
||||||
: branches branch { $$ = std::move($1); $$.push_back(std::move($2)); }
|
|
||||||
| branch { $$ = std::vector<branch_ptr>(); $$.push_back(std::move($1));}
|
|
||||||
;
|
|
||||||
|
|
||||||
branch
|
|
||||||
: pattern ARROW OCURLY aAdd CCURLY
|
|
||||||
{ $$ = branch_ptr(new branch(std::move($1), std::move($4))); }
|
|
||||||
;
|
|
||||||
|
|
||||||
pattern
|
|
||||||
: LID { $$ = pattern_ptr(new pattern_var(std::move($1))); }
|
|
||||||
| UID lowercaseParams
|
|
||||||
{ $$ = pattern_ptr(new pattern_constr(std::move($1), std::move($2))); }
|
|
||||||
;
|
|
||||||
|
|
||||||
data
|
|
||||||
: DATA UID EQUAL OCURLY constructors CCURLY
|
|
||||||
{ $$ = definition_ptr(new definition_data(std::move($2), std::move($5))); }
|
|
||||||
;
|
|
||||||
|
|
||||||
constructors
|
|
||||||
: constructors COMMA constructor { $$ = std::move($1); $$.push_back(std::move($3)); }
|
|
||||||
| constructor
|
|
||||||
{ $$ = std::vector<constructor_ptr>(); $$.push_back(std::move($1)); }
|
|
||||||
;
|
|
||||||
|
|
||||||
constructor
|
|
||||||
: UID uppercaseParams
|
|
||||||
{ $$ = constructor_ptr(new constructor(std::move($1), std::move($2))); }
|
|
||||||
;
|
|
||||||
|
|
@ -1,34 +0,0 @@
|
|||||||
%option noyywrap
|
|
||||||
|
|
||||||
%{
|
|
||||||
#include <iostream>
|
|
||||||
#include "ast.hpp"
|
|
||||||
#include "parser.hpp"
|
|
||||||
|
|
||||||
#define YY_DECL yy::parser::symbol_type yylex()
|
|
||||||
|
|
||||||
%}
|
|
||||||
|
|
||||||
%%
|
|
||||||
|
|
||||||
[ \n]+ {}
|
|
||||||
\+ { return yy::parser::make_PLUS(); }
|
|
||||||
\* { return yy::parser::make_TIMES(); }
|
|
||||||
- { return yy::parser::make_MINUS(); }
|
|
||||||
\/ { return yy::parser::make_DIVIDE(); }
|
|
||||||
[0-9]+ { return yy::parser::make_INT(atoi(yytext)); }
|
|
||||||
defn { return yy::parser::make_DEFN(); }
|
|
||||||
data { return yy::parser::make_DATA(); }
|
|
||||||
case { return yy::parser::make_CASE(); }
|
|
||||||
of { return yy::parser::make_OF(); }
|
|
||||||
\{ { return yy::parser::make_OCURLY(); }
|
|
||||||
\} { return yy::parser::make_CCURLY(); }
|
|
||||||
\( { return yy::parser::make_OPAREN(); }
|
|
||||||
\) { return yy::parser::make_CPAREN(); }
|
|
||||||
, { return yy::parser::make_COMMA(); }
|
|
||||||
-> { return yy::parser::make_ARROW(); }
|
|
||||||
= { return yy::parser::make_EQUAL(); }
|
|
||||||
[a-z][a-zA-Z]* { return yy::parser::make_LID(std::string(yytext)); }
|
|
||||||
[A-Z][a-zA-Z]* { return yy::parser::make_UID(std::string(yytext)); }
|
|
||||||
|
|
||||||
%%
|
|
@ -1,99 +0,0 @@
|
|||||||
#include "type.hpp"
|
|
||||||
#include <sstream>
|
|
||||||
#include <algorithm>
|
|
||||||
#include "error.hpp"
|
|
||||||
|
|
||||||
void type_var::print(const type_mgr& mgr, std::ostream& to) const {
|
|
||||||
auto it = mgr.types.find(name);
|
|
||||||
if(it != mgr.types.end()) {
|
|
||||||
it->second->print(mgr, to);
|
|
||||||
} else {
|
|
||||||
to << name;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
void type_base::print(const type_mgr& mgr, std::ostream& to) const {
|
|
||||||
to << name;
|
|
||||||
}
|
|
||||||
|
|
||||||
void type_arr::print(const type_mgr& mgr, std::ostream& to) const {
|
|
||||||
left->print(mgr, to);
|
|
||||||
to << " -> (";
|
|
||||||
right->print(mgr, to);
|
|
||||||
to << ")";
|
|
||||||
}
|
|
||||||
|
|
||||||
std::string type_mgr::new_type_name() {
|
|
||||||
int temp = last_id++;
|
|
||||||
std::string str = "";
|
|
||||||
|
|
||||||
while(temp != -1) {
|
|
||||||
str += (char) ('a' + (temp % 26));
|
|
||||||
temp = temp / 26 - 1;
|
|
||||||
}
|
|
||||||
|
|
||||||
std::reverse(str.begin(), str.end());
|
|
||||||
return str;
|
|
||||||
}
|
|
||||||
|
|
||||||
type_ptr type_mgr::new_type() {
|
|
||||||
return type_ptr(new type_var(new_type_name()));
|
|
||||||
}
|
|
||||||
|
|
||||||
type_ptr type_mgr::new_arrow_type() {
|
|
||||||
return type_ptr(new type_arr(new_type(), new_type()));
|
|
||||||
}
|
|
||||||
|
|
||||||
type_ptr type_mgr::resolve(type_ptr t, type_var*& var) 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;
|
|
||||||
}
|
|
@ -1,65 +0,0 @@
|
|||||||
#pragma once
|
|
||||||
#include <memory>
|
|
||||||
#include <map>
|
|
||||||
|
|
||||||
struct type_mgr;
|
|
||||||
|
|
||||||
struct type {
|
|
||||||
virtual ~type() = default;
|
|
||||||
|
|
||||||
virtual void print(const type_mgr& mgr, std::ostream& to) const = 0;
|
|
||||||
};
|
|
||||||
|
|
||||||
using type_ptr = std::shared_ptr<type>;
|
|
||||||
|
|
||||||
struct type_var : public type {
|
|
||||||
std::string name;
|
|
||||||
|
|
||||||
type_var(std::string n)
|
|
||||||
: name(std::move(n)) {}
|
|
||||||
|
|
||||||
void print(const type_mgr& mgr, std::ostream& to) const;
|
|
||||||
};
|
|
||||||
|
|
||||||
struct type_base : public type {
|
|
||||||
std::string name;
|
|
||||||
|
|
||||||
type_base(std::string n)
|
|
||||||
: name(std::move(n)) {}
|
|
||||||
|
|
||||||
void print(const type_mgr& mgr, std::ostream& to) const;
|
|
||||||
};
|
|
||||||
|
|
||||||
struct type_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);
|
|
||||||
};
|
|
@ -1,16 +0,0 @@
|
|||||||
#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);
|
|
||||||
}
|
|
@ -1,16 +0,0 @@
|
|||||||
#pragma once
|
|
||||||
#include <map>
|
|
||||||
#include "type.hpp"
|
|
||||||
|
|
||||||
struct type_env {
|
|
||||||
std::map<std::string, type_ptr> names;
|
|
||||||
type_env const* parent = nullptr;
|
|
||||||
|
|
||||||
type_env(type_env const* p)
|
|
||||||
: parent(p) {}
|
|
||||||
type_env() : type_env(nullptr) {}
|
|
||||||
|
|
||||||
type_ptr lookup(const std::string& name) const;
|
|
||||||
void bind(const std::string& name, type_ptr t);
|
|
||||||
type_env scope() const;
|
|
||||||
};
|
|
@ -1,28 +0,0 @@
|
|||||||
cmake_minimum_required(VERSION 3.1)
|
|
||||||
project(compiler)
|
|
||||||
|
|
||||||
find_package(BISON)
|
|
||||||
find_package(FLEX)
|
|
||||||
bison_target(parser
|
|
||||||
${CMAKE_CURRENT_SOURCE_DIR}/parser.y
|
|
||||||
${CMAKE_CURRENT_BINARY_DIR}/parser.cpp
|
|
||||||
COMPILE_FLAGS "-d")
|
|
||||||
flex_target(scanner
|
|
||||||
${CMAKE_CURRENT_SOURCE_DIR}/scanner.l
|
|
||||||
${CMAKE_CURRENT_BINARY_DIR}/scanner.cpp)
|
|
||||||
add_flex_bison_dependency(scanner parser)
|
|
||||||
|
|
||||||
add_executable(compiler
|
|
||||||
ast.cpp ast.hpp definition.cpp
|
|
||||||
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})
|
|
@ -1,262 +0,0 @@
|
|||||||
#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);
|
|
||||||
}
|
|
@ -1,197 +0,0 @@
|
|||||||
#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();
|
|
||||||
};
|
|
@ -1,21 +0,0 @@
|
|||||||
#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 "??";
|
|
||||||
}
|
|
@ -1,12 +0,0 @@
|
|||||||
#pragma once
|
|
||||||
#include <string>
|
|
||||||
|
|
||||||
enum binop {
|
|
||||||
PLUS,
|
|
||||||
MINUS,
|
|
||||||
TIMES,
|
|
||||||
DIVIDE
|
|
||||||
};
|
|
||||||
|
|
||||||
std::string op_name(binop op);
|
|
||||||
std::string op_action(binop op);
|
|
@ -1,83 +0,0 @@
|
|||||||
#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() {
|
|
||||||
|
|
||||||
}
|
|
@ -1,23 +0,0 @@
|
|||||||
#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;
|
|
||||||
}
|
|
@ -1,34 +0,0 @@
|
|||||||
#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;
|
|
||||||
};
|
|
@ -1,5 +0,0 @@
|
|||||||
#include "error.hpp"
|
|
||||||
|
|
||||||
const char* type_error::what() const noexcept {
|
|
||||||
return "an error occured while checking the types of the program";
|
|
||||||
}
|
|
@ -1,21 +0,0 @@
|
|||||||
#pragma once
|
|
||||||
#include <exception>
|
|
||||||
#include "type.hpp"
|
|
||||||
|
|
||||||
struct type_error : std::exception {
|
|
||||||
std::string description;
|
|
||||||
|
|
||||||
type_error(std::string d)
|
|
||||||
: description(std::move(d)) {}
|
|
||||||
|
|
||||||
const char* what() const noexcept override;
|
|
||||||
};
|
|
||||||
|
|
||||||
struct unification_error : public type_error {
|
|
||||||
type_ptr left;
|
|
||||||
type_ptr right;
|
|
||||||
|
|
||||||
unification_error(type_ptr l, type_ptr r)
|
|
||||||
: left(std::move(l)), right(std::move(r)),
|
|
||||||
type_error("failed to unify types") {}
|
|
||||||
};
|
|
@ -1,2 +0,0 @@
|
|||||||
data Bool = { True, False }
|
|
||||||
defn main = { 3 + True }
|
|
@ -1 +0,0 @@
|
|||||||
defn main = { 1 2 3 4 5 }
|
|
@ -1,8 +0,0 @@
|
|||||||
data List = { Nil, Cons Int List }
|
|
||||||
|
|
||||||
defn head l = {
|
|
||||||
case l of {
|
|
||||||
Nil -> { 0 }
|
|
||||||
Cons x y z -> { x }
|
|
||||||
}
|
|
||||||
}
|
|
@ -1,31 +0,0 @@
|
|||||||
#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));
|
|
||||||
}
|
|
@ -1,2 +0,0 @@
|
|||||||
defn main = { plus 320 6 }
|
|
||||||
defn plus x y = { x + y }
|
|
@ -1,3 +0,0 @@
|
|||||||
defn add x y = { x + y }
|
|
||||||
defn double x = { add x x }
|
|
||||||
defn main = { double 163 }
|
|
@ -1,7 +0,0 @@
|
|||||||
data List = { Nil, Cons Int List }
|
|
||||||
defn length l = {
|
|
||||||
case l of {
|
|
||||||
Nil -> { 0 }
|
|
||||||
Cons x xs -> { 1 + length xs }
|
|
||||||
}
|
|
||||||
}
|
|
Some files were not shown because too many files have changed in this diff Show More
Loading…
Reference in New Issue
Block a user