Compare commits

..

508 Commits

Author SHA1 Message Date
f2e424944e Start working on the control flow graphs post
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-11-13 19:57:08 -08:00
8a471c6b45 Add missing imp.bergamot file for rendering imperative programs
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-11-06 10:43:47 -08:00
9b93582d18 Fix meta description on part 4 of SPA 2024-11-03 17:59:37 -08:00
9fc2d16fb8 Adjust dates of part 4 and part 5 to match real publication dates
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-11-03 17:51:13 -08:00
f00c69f02c Edit and publish SPA part 5 2024-11-03 17:50:11 -08:00
4fc1191d13 Proofread and publish part 4
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-11-03 17:37:44 -08:00
951aafc90a Stop using 'symeq'
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-11-03 17:12:39 -08:00
ee13409b33 Add a visualization of two ASTs
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-11-03 17:06:19 -08:00
615aeb72da Finish most of part 5 of SPA series
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-11-03 16:58:06 -08:00
3be67ca4c8 Use unification-based 'eq' for numbers and symbols
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-11-03 16:05:04 -08:00
37dd9ad6d4 Write the semantics section using Bergamot
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-10-13 13:31:47 -07:00
77dade1d1d Move all bergamot partials and shortcodes into theme
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-09-15 20:10:04 -07:00
d140422225 Update theme
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-09-15 20:05:46 -07:00
2defe99c73 Update theme w/ more Bergamot affordances
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-09-15 19:49:37 -07:00
0766211d79 Turn semantics post into page bundle
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-09-15 18:47:32 -07:00
b854eade3c Remove configs from website that are now defined in theme
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-09-15 18:46:23 -07:00
c6f34f8eaa Delete unused shortcodes
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-09-15 17:46:13 -07:00
0ba5799c75 Update theme with missing file
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-09-15 16:39:17 -07:00
324fa948e6 Bring in more theme updates
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-09-15 16:28:07 -07:00
3e46ff8be6 Update vanilla theme to handle loading Bergamot
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-09-15 15:47:26 -07:00
18eb1da5ba Allow render rules to be customized using render presets
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-09-15 13:49:57 -07:00
dde7df4604 Update to new Bergamot version
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-09-15 10:33:40 -07:00
e4101f1396 Fix missing paren
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-09-01 15:19:47 -07:00
d94ceeab2e Make minor edits to part 5 of SPA
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-08-31 11:37:28 -07:00
697f083237 Reference more future posts in SPA intro
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-08-18 15:05:55 -10:00
3e97fdcfea Start work on the draft about semantics
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-08-18 15:05:39 -10:00
40007c427e Avoid using a non-greedy match and just avoid $ in {{< latex >}}
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-08-18 14:16:42 -10:00
5ab0d0d40e Use a non-greedy match for the double-dollar-sign escaping
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-08-18 14:07:16 -10:00
7c65afbc93 Fix more line numbers
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-08-18 13:31:08 -10:00
fb071e55aa Update 'submodules.json' with new submodule
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-08-18 13:23:20 -10:00
406c934b7a Update code in blog post to match new line numbers
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-08-18 13:22:28 -10:00
292cf009e6 Remove --local-interfaces as it is no longer needed
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-08-18 12:29:35 -10:00
6bf7659b19 Fix line numbering issues due to updating Agda
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-08-18 11:14:09 -10:00
0a90e8da29 Write a draft of the fixed point algorithm article
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-08-18 11:05:51 -10:00
32fe8e5ee6 Update the referenced Agda submodule
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-08-18 10:30:21 -10:00
7ccbaa7829 Make sure all links are consistent
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-08-09 06:48:26 -07:00
7817c9a4ce Add draft link support to analyze.rb
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-08-08 17:54:25 -07:00
bf9b0aedf9 Edit and publish part 3
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-08-08 17:30:17 -07:00
21b2ff208e Edit and publish part 2
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-08-08 16:45:13 -07:00
ecad4541f6 Add a (not-yet-valid) link to part 4
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-08-08 16:44:48 -07:00
864276ea72 Delete .DS_Store file
No idea how I managed to commit it.

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-08-01 21:23:13 -07:00
23eb36b911 Update theme
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-07-16 14:31:06 -07:00
51bcd116b3 Update other dates on lattice drafts
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-07-06 17:52:17 -07:00
928adbd594 Publish Agda SPA post about lattices
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-07-06 17:46:54 -07:00
e91b6f692f Publish introducton to SPA in Agda
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-07-06 17:42:44 -07:00
861dafef70 Finish up draft about lattices of finite height.
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-07-05 20:43:26 -07:00
388c23c376 Write more on finite height lattices
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-07-05 12:09:29 -07:00
82d9196c90 Update theme with bugfix
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-06-27 22:32:13 -07:00
826a16eb66 Start working on part 3
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-06-27 22:26:01 -07:00
0b97eb85a1 Update theme
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-06-26 19:49:24 -07:00
a2132001e8 Update theme
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-06-26 19:25:32 -07:00
4fd6dd5606 Make minor edits to article and update theme
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-06-24 19:59:51 -07:00
7b71ec4402 Update theme some more
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-06-24 19:49:05 -07:00
07771117ac Update theme
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-06-24 19:28:41 -07:00
7fbc884e94 Actually disable new tab external links
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-06-24 18:48:13 -07:00
b40be72590 Disable opening external links in new tab
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-06-24 17:52:14 -07:00
b3db25c470 Fix some typos and publish the microfeatures post
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-06-23 18:02:13 -07:00
6a7b6ffc1f Write an article about microfeatures
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-06-23 17:59:03 -07:00
c87bb90c48 Update theme
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-06-23 17:57:06 -07:00
a6225191d0 Update theme
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-06-19 22:44:53 -07:00
afb904a64c Update theme
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-06-19 22:29:09 -07:00
cbad391dcd Update theme
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-06-19 22:18:19 -07:00
0bf3facf6c Add series navigation before appendix
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-06-19 22:04:01 -07:00
a9da39b987 Update theme
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-06-19 22:03:54 -07:00
1071bdd35a Update theme
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-06-19 17:31:34 -07:00
8656985885 Introduce "join" and "meet" as terms
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-06-16 20:12:39 -07:00
3be523b79e Update theme
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-06-16 19:45:29 -07:00
1fb7e5ff85 Finish draft of part 2, combining lattices
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-06-16 18:09:56 -07:00
df75d6e017 Slightly expand the draft.
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-06-09 19:39:00 -07:00
29c9af4902 Update theme to generate links to file ranges where possible
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-06-09 18:52:01 -07:00
7b03183e75 Continue expanding on the map draft
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-06-09 18:02:04 -07:00
4c70e61a14 Write some more in combining lattices
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-30 22:41:15 -07:00
b2b225f4ae Create only undirected edges from smaller node ID to higher node ID
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-30 21:07:23 -07:00
c17142e648 Fix the call to 'uniq' in analyze.rb
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-30 20:58:03 -07:00
8e4759bd2b Start on the navigation links in Agda SPA intro
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-30 20:52:33 -07:00
d2807917d2 Insert sequential links for series in analyze.rb
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-30 20:52:14 -07:00
71c030b947 Slightly tweak wording and front matter in Agda SPA posts
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-30 20:02:49 -07:00
1f3ab5349a Restore the dates in 'learning emulation' to their proper ones.
I found the original dates using the Wayback machine.

https://web.archive.org/web/20161022053013/https://danilafe.com/

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-30 18:58:38 -07:00
daaccb9b2f Add new groups to content graph script
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-30 00:38:27 -07:00
b66c58b68e Lightly edit and publish the Agda+Hugo post
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-30 00:30:05 -07:00
13636a0d29 Write more about Agda+Hugo
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-30 00:13:48 -07:00
5232f0a6e2 Update theme with new code highlighting
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-27 18:58:20 -07:00
6a168f2fe1 Start on a draft about Agda and Hugo
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-25 23:28:18 -07:00
04f12b545d Minor edits to 'lattices 2'
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-25 20:45:19 -07:00
711b01175d Put the number back to what it was
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-24 23:12:27 -07:00
272c2666c5 Inconsequential tweak to test Agda caching in build system
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-24 13:44:34 -07:00
60ba43378a Make the destination folders
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-24 13:21:33 -07:00
1da60b3b28 Print result of executing command
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-24 13:17:44 -07:00
ee118b07e5 Make build-agda-html.rb more configurable
This should use it from Nix, and cache the Agda compilations

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-24 12:31:26 -07:00
06ee998d54 Allow executing non-remote JS for KaTeX
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-23 21:14:49 -07:00
c197a45540 Port over the HTML conversion script to execute JS
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-23 21:03:03 -07:00
4d23b45633 Update theme
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-23 00:57:07 -07:00
c027efa931 Stop crashing on failed Agda invocation
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-23 00:31:36 -07:00
96c4d6fecc Fail if couldn't build Agda
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-23 00:04:13 -07:00
4e1fd54c58 Add Gemfile and lock for nokogiri since a script now uses it
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-22 23:14:51 -07:00
d6db020e1c Adjust build script to accept Agda invocation
This might come in useful from NixOS

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-22 23:05:36 -07:00
c0f4fe017f Replace absolute links with relrefs
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-22 23:05:11 -07:00
11d726a6ad Fix absolute link in favor of relref
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-22 23:01:26 -07:00
37399afc68 Update theme to generate series meta
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-22 22:42:04 -07:00
5c19fc4208 Automatically group files using the series meta
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-22 22:41:32 -07:00
00f0f13b93 Support cross-file linking
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-22 22:29:26 -07:00
54844fb954 Add script to generate HTML for all Agda files appropriately
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-22 17:34:32 -07:00
6ffd3afeaa Update theme
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-22 17:07:37 -07:00
9d0dcd98bd Improve support when code occurrs multiple times
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-22 17:05:38 -07:00
f78f877e21 Support blocks that are the entire file
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-22 16:50:45 -07:00
5d0b903c03 Support non-submodule code
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-22 16:47:42 -07:00
032411fe9c Add a script to generate links using Agda's HTML output
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-22 16:28:00 -07:00
76b061d699 Update theme
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-22 16:23:47 -07:00
08d37c839c Update theme
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-21 23:51:08 -07:00
0a26230fe1 Remove unused shortcodes
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-21 20:09:48 -07:00
2e59beda0c Update theme 2024-05-21 19:05:07 -07:00
ee8b1f5dc0 Write a bit more, enable support for paragraph links
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-21 19:04:08 -07:00
4938cdaecd Work some more on lattices 2
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-20 22:46:18 -07:00
84f28ae5ce Add tags to Agda articles
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-20 21:46:14 -07:00
58e7a1f2dc Start on a draft of 'combining lattices'
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-20 21:39:03 -07:00
78bba7a0e9 Update the blog for series navigation
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-20 00:37:16 -07:00
9d31764073 Tie up Lattices (1), and plan to write Lattices (2)
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-19 22:29:24 -07:00
d787548915 Update theme
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-16 16:17:01 -07:00
a29bca499f Switch to using data/ for submodule information
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-16 15:52:33 -07:00
60d3b3025a Flesh out the Lattices post some more
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-14 21:43:12 -07:00
c036041339 Update theme
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-14 20:32:37 -07:00
1df315612a Update "typesafe interpreter" article to new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-13 19:08:17 -07:00
15beddf96b Update btree article with new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-13 19:07:44 -07:00
20d8b18a9b Update 'stack language recursion' article to new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-13 19:07:01 -07:00
53ff0c39e4 Update "search as polynomial" article to new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-13 19:06:33 -07:00
357a3bef09 Update the modulo patterns article to use new delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-13 19:04:08 -07:00
81eef51e88 Update 'math rendering is wrong' to new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-13 19:02:14 -07:00
10dfb2fe49 Update "church encoding" article to new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-13 19:01:42 -07:00
ef76149112 Update 'newtype' article to new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-13 19:01:08 -07:00
a6a330a78e Update Haskell LSP article to new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-13 19:00:23 -07:00
7f4d0df366 Update "catemorphisms" article to new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-13 18:59:54 -07:00
3eddac0a89 Update "proving my compiler incorrect" to new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-13 18:58:50 -07:00
6e7ac1c1ca Update "I don't like Coq's docs" article to new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-13 18:58:15 -07:00
68d9cf1274 Update 'evaluator for Dawn in Coq' article to new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-13 18:57:15 -07:00
5eb0d1548c Update dawn-in-coq to new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-13 18:55:59 -07:00
e543904995 Update boolean values article to new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-13 18:54:11 -07:00
ffda1d3235 Moved the bergamot article to new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-13 18:52:21 -07:00
b705aa217c Update "expr pattern in agda" to new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-13 18:50:56 -07:00
6f20b17948 Update "compiler: polymorphic data types" to new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-13 18:50:05 -07:00
2fde7e5cf8 Update "compiler: polymorphism" to new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-13 18:48:34 -07:00
bee06b6731 Update "compiler: compilation" to use new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-13 18:43:14 -07:00
d3fa7336a2 Update "compiler: execution" to new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-13 18:38:05 -07:00
96545a899f Update "compiler: typechecking" to new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-13 18:33:30 -07:00
6ef5ae2394 Update "types: variables" to new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-13 18:31:52 -07:00
05a31dd4d4 Update 'compiler: parsing' article to new string literals
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-13 18:30:27 -07:00
d9d5c8bf14 Switch 'types: basics' to new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-13 18:28:36 -07:00
291a1f0178 Update SPA article on Lattices with new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-13 18:22:21 -07:00
2547b53aa2 Switch "Homework for an assignment" post 2 to new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-13 18:20:54 -07:00
409f8b7186 Switch tokenizing article to new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-13 18:20:04 -07:00
189422bf1e Convert AoC Coq article to new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-13 18:16:20 -07:00
74daeee140 Enable goldmark passthrough
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-13 17:47:52 -07:00
befcd3cf98 Add a sidenote about land and lor.
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-13 15:41:50 -07:00
e063ff6aa5 Update the vanilla theme
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-12 18:58:44 -07:00
6179c86919 Show the basic Nat lattice.
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-12 18:52:26 -07:00
a20fe07a56 Move original 'monotone function' text into new post and heavily rework it
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-12 18:28:44 -07:00
2b5dcf12d7 Rename the SPA intro to have a specific name
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-12 13:50:29 -07:00
5873c1ca96 Write a high-level introduction for the SPA series
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-12 13:49:21 -07:00
c6e2ecb996 Add first section of Agda program analysis article
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-03-14 22:25:17 -07:00
2130b00752 Narrow some of the tags
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-03-13 15:59:46 -07:00
474c3a8348 Switch bracket types in Agda expression pattern post
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-03-13 15:05:37 -07:00
29a18b8b37 Add description to expr_pattern
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-03-11 23:26:07 -07:00
21ab4f0a8b Update theme 2024-03-11 23:21:08 -07:00
7d2842fd64 Add article about the 'deeply embedded expression' pattern 2024-03-11 23:15:56 -07:00
cd4c121e07 Update the theme
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-03-11 15:50:40 -07:00
d0570f876e Add the SPA code as a submodule
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-03-11 14:34:35 -07:00
8bf99a1ab0 Update theme
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-02-02 21:05:48 -08:00
fdcd4ddd60 Defer loading of KaTeX JS and Bergamot support code 2023-12-30 19:56:14 -08:00
c09fff455f Update theme. 2023-12-30 19:40:10 -08:00
0b3755c69a Use a shim instead of the real katex-expression because it hardcodes too much.
We don't need a second bundle of KaTeX, or all of the fonts a second time, served
from a CDN we don't control.

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2023-12-30 19:38:37 -08:00
e90fb64946 Update theme
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2023-12-30 16:31:46 -08:00
d542a4790e Update theme 2023-12-30 16:16:10 -08:00
bc5cb4009c Update theme 2023-12-30 16:02:52 -08:00
6724533d0e Update theme and change config.toml to match 2023-12-30 14:48:16 -08:00
0f0668b77b Make use of theme's support for Plausible. 2023-12-30 13:13:00 -08:00
266bf9b4cf Add an exercise about conversions to types: basics
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2023-12-29 12:47:58 -08:00
a6f3bccf64 Use markdown for exercises, since it works fine out of the box.
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2023-12-28 16:05:15 -08:00
2d640f2e6a Center the 'no proofs' message 2023-12-28 13:20:19 -08:00
d7d99205a1 Properly escape < in HTML content. 2023-12-28 00:36:58 -08:00
9f437d5b9f Add a couple of exercises to types: basics.
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2023-12-28 00:13:13 -08:00
0d3100ba33 Make exercises into details (so they can be collapsed) 2023-12-28 00:12:51 -08:00
72fb69d87b Make minor changes to types: basics.
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2023-12-27 23:31:45 -08:00
ed4fcf5e9d Start explaining exercises in types intro.
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2023-12-27 23:31:28 -08:00
8742c6e7b9 Add a Bergamot exercise shortcode to give exercises.
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2023-12-27 23:31:00 -08:00
d7d7254a7b Extract loading and closing bergamot into a helper script.
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2023-12-27 23:30:16 -08:00
7e8870de6c Factor launching bergamot into a helper function 2023-12-27 13:27:20 -08:00
8f2b2addc2 Rename the widget IDs to not include numbers. 2023-12-27 13:16:20 -08:00
e4743bbdef Make some edits to 'types' part 1. 2023-12-26 14:02:48 -08:00
80cdea6932 Update rendering rules for changes to Bergamot. 2023-12-26 13:22:38 -08:00
645f2c5c9c Update inference rules to match new Bergamot's single-literal output
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2023-12-26 13:21:37 -08:00
85b81ffc98 Modify rendering rules to handle precedence
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2023-12-25 18:42:43 -08:00
fa5536f504 Add special styling for bergamot error messages
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2023-12-25 18:42:29 -08:00
16086e79b0 Proofread and publish bergamot post
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2023-12-22 22:15:17 -08:00
b001bba3b8 Tweak rendering rules to support int(x) and str(x).
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2023-12-22 22:00:46 -08:00
0c895a2662 Add an initial draft of the Bergamot post.
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2023-12-22 22:00:06 -08:00
6f0641f315 Render variables better
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2023-12-22 16:04:47 -08:00
dc9dbe8a0f Update for bergamot requiring an 'input program' too
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2023-12-22 16:04:33 -08:00
0b8096f973 Tweak the menu selector style
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2023-12-22 16:04:04 -08:00
d58a2a9975 Add overflow scroll to proof tree view.
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2023-12-21 21:27:39 -08:00
a83268a6e3 Update use of the bergamot widget
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2023-12-21 17:26:19 -08:00
5c83f234c6 Include rendering rules in Bergamot widget.
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2023-12-03 00:03:08 -08:00
24abec4045 Add some more CSS for the updates to the bergamot widget
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2023-12-03 00:01:49 -08:00
56ff56281e Add missing SCSS file for bergamot. 2023-11-29 23:26:09 -08:00
c25f9ad9ae Add the work-in-progress Bergamot widget to the basics page. 2023-11-29 23:21:15 -08:00
5041c90ac0 Add some partials to load and create a Bergamot widget.
I've set up some infrastructure to build and host a bergamot JS
file using Nix on static.danilafe.com.

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2023-11-29 22:29:14 -08:00
2855675fa5 Update theme
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2023-11-29 22:28:31 -08:00
209689c5f4 Update the theme
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2023-11-27 22:18:15 -08:00
3d64b0aa28 Update the 'vanilla' theme
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2023-11-24 11:04:42 -08:00
3bceab0606 Fix dates
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2023-10-14 15:58:20 -07:00
c189da3671 Finalize the X Macro article
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2023-10-14 15:38:54 -07:00
dd232cedb5 Fixup links and add description to X Macros article. 2023-10-09 20:33:21 -07:00
88c5daa561 Add the 'chapel' tag to the alloy article
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2023-10-09 20:24:19 -07:00
4f281ef108 Add a draft article about X Macros 2023-10-09 20:23:57 -07:00
12aca7ca58 Update the Alloy blogpost to point to the GitHub files.
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2023-10-09 14:41:03 -07:00
77ec1aa969 Update the 'vanilla' theme
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2023-10-09 14:40:45 -07:00
8710a5554c Fix mistakes in the example.agda file for IsSomething.
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2023-09-03 11:38:00 -07:00
6b24d67409 Minor wording updates to the Agda post. 2023-08-31 22:30:36 -07:00
48c3105f42 Finish and publish the IsSomething article 2023-08-31 22:16:26 -07:00
032453c4d0 Add a first draft of the IsSomething article 2023-08-28 23:04:39 -07:00
f093868da1 Add the missing general-base pattern drawing code 2023-08-28 20:46:29 -07:00
1f5e38190d Fix DeMorgan's link 2023-06-04 22:03:38 -07:00
250884c7bc Edit and publish Alloy article 2023-06-04 21:56:45 -07:00
8a2e91e65e Update theme 2023-06-04 21:54:19 -07:00
5910ce7980 Say screw it and publish polynomial article 2023-05-22 21:42:32 -07:00
00bec06012 Make some edits to the polynomial draft
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2023-05-22 20:44:50 -07:00
54dccdbc7d Fix accidentally lowercased shortcode 2023-05-14 21:23:22 -07:00
2bd776ec55 Add a description and disclaimer to the Alloy draft. 2023-05-14 21:18:23 -07:00
23cf7c9e8b Finish initial draft of the Alloy article. 2023-05-14 21:13:23 -07:00
384f5de765 Make some more progress on the Alloy article. 2023-05-14 16:00:55 -07:00
9ae4798d80 Hide Alloy article even from draft side 2023-05-04 21:03:37 -07:00
850ccbdcee Update theme 2023-05-04 21:02:07 -07:00
d8ab3f2226 Continue working on the Alloy blog post 2023-05-04 21:01:31 -07:00
9ddd2dd3bc Add initial draft of alloy article 2023-05-04 01:03:58 -07:00
f579641866 Add support for discussion rooms and add one to polynomial article 2023-04-15 15:09:06 -07:00
a71c0c4e74 Update theme 2023-04-09 22:52:37 -07:00
d3921f9e20 Update the theme to better deal with dark mode 2023-04-09 22:39:47 -07:00
e0d7332dea Update theme 2023-03-11 14:57:12 -08:00
d6b8eb8548 Update theme with CSS variable fallbacks 2023-03-11 14:08:26 -08:00
2964b6c6fa Tweak some wording in the variables article 2023-03-11 12:15:21 -08:00
a0cd1074e1 Update the theme with dark mode support 2023-03-11 12:14:57 -08:00
cc2b5ef918 Remove the resume, as it's now auto-built 2023-02-19 22:49:55 -08:00
d003fdf357 Update theme 2023-02-19 15:11:03 -08:00
5384faf3ec Update theme with support for series 2023-01-31 18:54:57 -08:00
a833cd84f3 Add series tags to relevant articles 2023-01-31 18:53:30 -08:00
7f1b9d31ea Add all the series pages 2023-01-31 18:53:02 -08:00
5bd8c11a86 Tag the more rough articles as expired to make sure they don't show up 2023-01-29 21:23:59 -08:00
846d85bb7a Add missing source file to typeclasses-are-logic post 2023-01-29 21:12:10 -08:00
b492c2d0fb Add more drafts 2023-01-29 21:08:31 -08:00
1a6f5e061b Add a very rough draft of the idris catemorphisms article I found lying around 2023-01-29 21:00:22 -08:00
5c62107e3b Put language code back into config.toml 2023-01-01 20:52:55 -08:00
0891c5da62 Update theme 2023-01-01 19:37:08 -08:00
2d22f0b2f2 Remove the code for the linear multistep article, too 2023-01-01 15:27:27 -08:00
1961e545c0 Extract compiler into its own repo 2023-01-01 15:09:41 -08:00
7951fcc494 Update theme 2023-01-01 14:32:42 -08:00
6bf0b37694 Move the content graph layout into theme 2023-01-01 13:21:10 -08:00
7a51132e69 Add back the tags page content via Markdown 2023-01-01 13:00:41 -08:00
98f071df6d Update theme 2023-01-01 12:59:45 -08:00
9543296ffd Delete some generated files in favor of generating them at build time 2023-01-01 12:30:49 -08:00
16dd545c22 Make use of the theme's supported i18n features 2023-01-01 12:30:49 -08:00
e7cb818f05 Merge branch 'master' of https://dev.danilafe.com/Web-Projects/blog-static 2022-12-30 13:35:00 -08:00
ed89ade5e3 Update theme 2022-12-30 13:34:56 -08:00
80d2eec5ed Update theme 2022-12-30 13:29:03 -08:00
8d980b0287 Fix typo in equation for search-as-polynomial article 2022-12-30 13:27:47 -08:00
Danila Fedorin
baa199c50f Prevent overlap in polynomial search article 2022-12-09 15:42:48 -08:00
Danila Fedorin
29a0d2e357 Remove linear multistep article (transferred to Chapel blog) 2022-12-09 15:42:29 -08:00
Danila Fedorin
7ab72668e1 Update the theme 2022-12-09 15:41:27 -08:00
ca3345cb33 Edit and improve the polynomial search post 2022-10-26 21:26:27 -07:00
0ade4b2efb Add a tiny section about the tropical semiring to polynomial post 2022-10-25 22:46:05 -07:00
2439a02dbb Add draft of first part of polynomials article 2022-10-23 17:27:30 -07:00
a785c71c5f Update theme with new KaTeX version 2022-10-18 19:32:50 -07:00
db852cab68 Update about page 2022-10-18 18:09:40 -07:00
6a5718c45e Remove donation info 2022-10-18 18:09:40 -07:00
c68dbdb8fe Fix line range in linear multistep solver post 2022-10-04 13:20:56 -07:00
49e0e2eb67 Make some edits to the variables article 2022-09-11 12:35:23 -07:00
7d5b39f130 Make most tables not wrap on small screens 2022-09-10 23:56:08 -07:00
dd8c846b3e Fix typo in the polymorphism article 2022-09-10 17:20:09 -07:00
392b103f38 Fix a mental typo in part 2 of types series 2022-09-10 12:33:43 -07:00
347c818ab6 Add a summary to the end of part 1 of types series 2022-09-10 12:33:07 -07:00
9192b870b6 Add a draft of the variables post in the types series 2022-08-29 21:45:53 -07:00
c21757694e Update the theme 2022-08-28 19:10:27 -07:00
770c7d0663 Finish draft of Type Theory post 2022-08-28 19:05:59 -07:00
bd8c9d8cdc Add draft of compiler article 2022-08-10 19:26:04 -07:00
10a4435760 Continue work on the type theory draft 2022-07-02 17:30:31 -07:00
bc52c2c685 Use the new dialog environment to discuss the meaning of n 2022-07-02 16:16:26 -07:00
81c8b2a903 Update theme 2022-07-02 16:16:08 -07:00
5ef10238e3 Start working on the basics part of the type systems articles 2022-06-30 21:58:57 -07:00
d2e8f809d0 Write some more for types series' intro. 2022-06-27 21:34:31 -07:00
8e550dc982 Start working on types series? 2022-06-27 19:38:58 -07:00
ed81ca957b Add missing backslashes to post 2022-06-26 18:35:47 -07:00
f8ab8257e7 Remove phone number 2022-05-15 11:44:04 -07:00
2474804258 Update the resume to fix link typo 2022-04-30 15:24:53 -07:00
e23dc1c063 Fix invalid KaTeX escape characters 2022-04-28 22:46:22 -07:00
9b28528acc Update generated files 2022-04-26 13:19:04 -07:00
86fd460a7a Revert "Remove generated files"
This reverts commit 609b8c76b6.
2022-04-26 13:15:56 -07:00
609b8c76b6 Remove generated files 2022-04-26 20:04:51 -07:00
57aecc46be Update and publish catamorphism article 2022-04-24 01:09:34 -07:00
ded50480a8 Update resume 2022-04-22 18:54:05 -07:00
4043a5c1a3 Add a draft of the catmorphisms post 2022-04-22 17:20:32 -07:00
b96d405270 Change tags on Nix Blog article 2022-04-10 13:11:50 -07:00
85751ba294 Update the search index and graph view 2022-04-10 13:07:06 -07:00
6145d9e804 Edit and public Nix Blog article 2022-04-10 13:04:03 -07:00
fe1c05fe46 Finih up draft of the Nix Blog article 2022-04-10 00:53:35 -07:00
dc3f086b9d Update the blog flake submodule and Nix Blog post 2022-04-09 15:55:21 -07:00
e778b8710d Add some more content to Nix Blog post 2022-04-09 15:35:52 -07:00
20be96253c Fix analyzer script and update graph JSON 2022-04-09 03:24:15 -07:00
e6129dd01d Fix SSH-based git remote breaking links 2022-04-09 03:14:21 -07:00
1ce0e8903f Update submodule configuration 2022-04-09 02:54:08 -07:00
b67c1ab615 Add some more to the Nix Blog post 2022-04-09 02:50:04 -07:00
f044082fa5 Update theme to escape HTML 2022-03-28 15:56:55 -07:00
b2a02c5a9c Update theme 2022-03-27 21:24:24 -07:00
3946fecd1d Update theme 2022-03-27 19:34:57 -07:00
27f43d0ad0 Update theme 2022-03-27 19:22:07 -07:00
684b3e0838 Update theme 2022-03-27 18:56:02 -07:00
adc66d8605 Update index? 2022-03-23 19:17:07 -07:00
58b831cd24 Fix typo in graph page 2022-03-15 17:27:33 -07:00
8cf0502492 Upate theme 2022-03-15 17:15:15 -07:00
a490514079 Add a graph visualization page based on the analyze script 2022-03-15 17:15:15 -07:00
a658286776 Make analyze.rb find its own files and generate JS 2022-03-15 15:08:46 -07:00
7fb3c26633 Add a file to create file dependency graph 2022-03-10 01:29:52 -08:00
21ca8e5e90 Replace all of the ref with relrefs 2022-03-09 22:03:33 -08:00
f719cedc37 Update index 2022-02-23 21:58:27 -08:00
22e70f7164 Add a thank you to Arthur in the conclusion 2022-01-08 17:49:46 -08:00
a573a0b765 Update and publish digit sum patterns article 2022-01-08 17:42:33 -08:00
ca1abf951f Finish up a draft of the modulo patterns article 2022-01-07 16:56:22 -08:00
2efa3c4a42 Replace sine/cosine math with visualizations. 2022-01-03 01:13:29 -08:00
f3fd177235 Add missing images 2022-01-01 20:16:15 -08:00
092f98c17a Update theme 2022-01-01 20:13:09 -08:00
eec6174562 Try moving some proofs into an appendix 2022-01-01 20:12:30 -08:00
81efcea0e5 Give initial stabs at Arthur's suggestions 2022-01-01 14:45:11 -08:00
7ac85b5b1e Add some more to the generalization sections. 2022-01-01 03:36:20 -08:00
1b35ca32ac Fix a few typos (thanks, Arthur) 2021-12-31 19:32:37 -08:00
97c989e465 Add a draft about digit sum patterns. 2021-12-31 00:14:31 -08:00
b43b81cc02 Update theme 2021-12-15 13:31:16 -08:00
c061e3e1b2 Publish matrix highlight 2021-12-13 21:19:23 -08:00
cd61c47e35 Remove quote from Matrix website 2021-12-13 20:16:37 -08:00
4f9b3669a2 Write a little article about Matrix Highlight 2021-12-13 18:25:12 -08:00
7164140c15 Add another (unpublished) draft 2021-12-04 00:41:01 -08:00
d41973f1a8 Add server configuration as submodule 2021-12-03 19:38:16 -08:00
8806f2862d Update index 2021-12-03 00:39:29 -08:00
36989c76ee Update theme 2021-12-03 00:35:28 -08:00
13aef5b3c0 Edit and publish second Coq Dawn article 2021-12-02 18:29:47 -08:00
b8f9f93537 Add illustrations about evaluation chains 2021-12-02 17:41:36 -08:00
1c93d28441 Remove undercore from refl constructor to avoid KaTeX errors 2021-11-28 19:34:57 -08:00
2ce351f7ef Actually push the rest of the new article 2021-11-28 17:33:04 -08:00
826dde759f Finish a draft of the UCC evaluator article 2021-11-28 16:50:28 -08:00
d1aa966737 Temporarily hide the Coq documentation article, even from drafts. 2021-11-28 16:46:56 -08:00
4d24e7095b Make some more progress on the UCC evaluator article 2021-11-28 01:48:01 -08:00
6c1940f5d2 Get started on a post about a UCC evaluator 2021-11-28 01:09:26 -08:00
30c395151d Use a different representation of values and prove equivalence of UCC evalutor 2021-11-28 01:08:56 -08:00
d72e64c7f9 Fix Ltac2 bug in Dawn file 2021-11-27 23:13:08 -08:00
abdc8e5056 Cleanup DawnEval.v 2021-11-27 14:17:09 -08:00
bc754c7a7d Start working on a verified UCC evaluator. 2021-11-26 01:40:04 -08:00
84ad8d43b5 Start on a draft for rant about Coq documentation 2021-11-25 00:33:54 -08:00
e440630497 Re-generate Stork index 2021-11-21 16:38:48 -08:00
71689fce79 Update tags 2021-11-21 16:20:18 -08:00
e7185ff460 Fix calling UCC Dawn 2021-11-21 12:38:19 -08:00
18f493675a Publish the dawn post 2021-11-20 23:36:57 -08:00
0c004b2e85 Edit the Dawn post a bit 2021-11-20 23:36:45 -08:00
c214d9ee37 Add the initial version of the Dawn article. 2021-11-20 23:21:03 -08:00
72259c16a9 Update resume 2021-10-03 20:36:54 -07:00
66b656ada5 Published TypeScript article 2021-09-19 12:34:40 -07:00
46e4ca3948 Fix typos in TypeScript article 2021-09-19 12:30:44 -07:00
f2bf2fb025 Fix up donation styles on smaller screens 2021-09-19 12:18:00 -07:00
50d48deec1 Update resume 2021-09-04 19:24:40 -07:00
3c905aa1d7 Add draft of TypeScript typesafe event emitter post 2021-09-04 18:32:08 -07:00
d5f478b3c6 Add donations 2021-08-23 18:41:46 -07:00
0f96b93532 Fix broken link in about page 2021-08-01 12:02:30 -07:00
5449affbc8 Update theme. 2021-06-28 12:04:15 -07:00
2cf19900db Update resume 2021-06-25 01:18:29 -07:00
efe5d08430 Update index. 2021-06-23 20:06:23 -07:00
994e9ed8d2 Update resume. 2021-06-20 19:01:48 -07:00
72af5cb7f0 Update resume. 2021-06-09 19:43:53 -07:00
308ee34025 Extract theme into submodule. 2021-04-15 01:44:07 -07:00
9839befdf1 Update resume. 2021-02-28 13:10:38 -08:00
d688df6c92 Update about page. 2021-02-24 22:03:29 -08:00
24eef25984 Add contact email to footer. 2021-02-24 17:54:22 -08:00
77ae0be899 Add search and links to it. 2021-02-22 17:21:27 -08:00
ca939da28e Add hugo functions post. 2021-01-18 00:55:31 -08:00
5d0920cb6d Extract code groups into a partial and display them for entire files and raw files. 2021-01-17 18:23:43 -08:00
d1ea7b5364 Add Hugo codelines post. 2021-01-13 21:39:35 -08:00
ebdb986e2a Remove useless sidenotes partial 2021-01-13 16:35:01 -08:00
4bb6695c2e Move margin include into TOC 2021-01-13 16:34:30 -08:00
a6c5a42c1d Split generated and handwritten configuration. 2021-01-11 17:07:18 -08:00
c44c718d06 Remove accidentally commited test submodule. 2021-01-11 16:58:33 -08:00
5e4097453b Update submodule script to properly gather submodule paths. 2021-01-11 12:39:41 -08:00
bfeae89ab5 Update codelines to use submodule link information 2021-01-10 22:51:10 -08:00
755364c0df Publish second Coq post. 2021-01-10 22:49:10 -08:00
dcb1e9a736 Finish up draft of Coq post. 2021-01-10 22:48:31 -08:00
c8543961af Add generated section of configuration. 2021-01-10 20:26:11 -08:00
cbad3b76eb Add script to generate submodule links. 2021-01-10 20:24:22 -08:00
b3ff2fe135 Add more text to draft. 2021-01-02 21:23:47 -08:00
6a6f25547e Update post with tactic-based proof. 2021-01-02 18:33:02 -08:00
43dfee56cc More progress on Coq post. 2021-01-01 21:35:46 -08:00
6f9a2ce092 Switch day 1 Coq post to use submodule'd code. 2021-01-01 18:46:35 -08:00
06014eade9 Add AoC submodule. 2021-01-01 18:40:43 -08:00
6f92a50c83 Make more progress on Coq post. 2021-01-01 18:39:30 -08:00
60eb50737d Add draft of the first portion of day 8 Coq writeup. 2020-12-31 21:51:43 -08:00
250746e686 Test commit to see if blog updating script works. 2020-12-30 18:36:02 -08:00
3bac151b08 Make the fooder divider a container. 2020-12-30 18:06:38 -08:00
c61d9ccb99 Adjust footer divider style. 2020-12-30 18:00:44 -08:00
56ad03b833 Remove index, since it's currently unused. 2020-12-30 16:47:01 -08:00
2f9e6278ba Use feather for starts. 2020-12-30 16:42:19 -08:00
17e0fbc6fb Remove search for now, since it screws with page load times. 2020-12-30 15:50:00 -08:00
7ee7feadf3 Link to favorite posts from footer. 2020-12-30 14:45:30 -08:00
b36ea558a3 Update index. 2020-12-30 14:43:55 -08:00
17d6a75465 Remove double toml extension from index. 2020-12-30 14:42:39 -08:00
d5541bc985 Add favorites page. 2020-12-30 14:41:29 -08:00
98a46e9fd4 Display star near favorite posts. 2020-12-30 14:27:42 -08:00
2e3074df00 Add favorite posts 2020-12-30 14:27:22 -08:00
b3dc3e690b Update search index. 2020-12-30 13:41:29 -08:00
b1943ede2f Add internship footer to posts (sorry) 2020-12-30 13:41:03 -08:00
0467e4e12f Disable progress bar in Stork. 2020-12-28 22:44:34 -08:00
8164624cee Remove useless paragraph element and fix CSS. 2020-12-28 22:41:15 -08:00
e0451d026c Update index. 2020-12-28 22:32:24 -08:00
1f1345477f Use Hugo's plaintext instead of file path for Stork index. 2020-12-28 22:32:17 -08:00
44529e872f Fix wrong path name for index file. 2020-12-28 22:23:29 -08:00
a10996954e Redirect search index. 2020-12-28 22:22:37 -08:00
4d1dfb5f66 Generate initial index. This will not be static indefinitely; I just need to find a way to build it in Nix. 2020-12-28 22:22:19 -08:00
f97b624688 Tweak search styles a little bit. 2020-12-28 22:03:04 -08:00
8215c59122 Change search highlight color. 2020-12-27 22:24:43 -08:00
eb97bd9c3e Add search box to main page. 2020-12-27 20:09:05 -08:00
d2e100fe4b Add search CSS. 2020-12-27 20:08:40 -08:00
de09a1f6bd Enable TOML output. 2020-12-27 20:08:27 -08:00
c40672e762 Add a way to generate TOML template for Stork. 2020-12-27 20:08:18 -08:00
565d4a6955 Update resume. 2020-12-14 18:03:31 -08:00
8f0f2eb35e Finish up the Coq Advent of Code post. 2020-12-02 18:45:28 -08:00
234b795157 Add Coq advent of code post. 2020-12-02 01:14:32 -08:00
e317c56c99 Add some shortcodes for making the game theory post nicer. 2020-11-08 21:22:51 -08:00
29d12a9914 Publish new Idris post. 2020-11-02 01:08:41 -08:00
b459e9cbfe Update typesafe imperative language post draft. 2020-11-01 23:56:55 -08:00
52abe73ef7 Make the typesafe imperative language work properly. 2020-10-31 01:34:23 -07:00
f0fe481bcf Add post about the typesafe imperative language. 2020-10-30 19:07:30 -07:00
222446a937 Add non-color indication to highlighted lines. 2020-10-10 17:12:40 -07:00
e7edd43034 Add draft warning. 2020-09-27 16:22:29 -07:00
2bc2c282e1 Revert "Experimentally enable shortcodes"
This reverts commit 5cc92d3a9d.
2020-09-27 14:47:25 -07:00
5cc92d3a9d Experimentally enable shortcodes 2020-09-27 14:42:35 -07:00
4be8a25699 Add a label to codelines that includes the source file. 2020-09-27 14:41:56 -07:00
d3421733e1 Update resume. 2020-09-25 22:52:07 -07:00
4c099a54e8 Publish part 13. 2020-09-19 16:27:41 -07:00
9f77f07ed2 Finish 13th part of the compiler series. 2020-09-19 16:14:07 -07:00
04ab1a137c Mark 13th post as draft 2020-09-19 11:59:54 -07:00
53744ac772 Fix wording 2020-09-18 15:14:34 -07:00
50a1c33adb Adjust code lines. 2020-09-18 14:42:50 -07:00
d153af5212 Get rid of more constructors and make mangled names optional. 2020-09-18 14:09:03 -07:00
a336b27b6c Remove unneeded explicit calls to std::string 2020-09-18 12:27:57 -07:00
97eb4b6e3e Fix silent error in set_mangled_name 2020-09-18 12:02:37 -07:00
430768eac5 Add a TODO to part 13. 2020-09-17 22:56:08 -07:00
5db864881a Fix use of wrong environment for name mangling. 2020-09-17 22:55:27 -07:00
d3b1047d37 Renamed the file since we have no optimization. 2020-09-17 22:36:43 -07:00
98cac103c4 Update blog post, switching away from two sections. 2020-09-17 22:35:40 -07:00
7226d66f67 Remove the parent method from type_env. 2020-09-17 22:35:12 -07:00
8a352ed3ea Roll back optimization changes. 2020-09-17 20:45:24 -07:00
02f8306c7b Use an instruction instead of a special-case boolean instruction. 2020-09-17 18:33:52 -07:00
cf6f353f20 Change tagging to assume sign extension.
ARM and x86_64 require "real" pointers to be
sign-extended in their top bits. This means
a working pointer is guaranteed to have either "11"
as leading bits, or "00". So, to tag a "fake" pointer
which is an unboxed 32-bit integer, we simply toggle
the leading bit.
2020-09-17 18:30:55 -07:00
7a631b3557 Make a few more things classes. 2020-09-17 18:30:41 -07:00
5e13047846 Make global scope a class. 2020-09-15 19:45:05 -07:00
c17d532802 Make type_mgr a class. 2020-09-15 19:19:58 -07:00
55e4e61906 Make mangler a class and reformat graph. 2020-09-15 19:13:48 -07:00
f2f88ab9ca Make env a class. 2020-09-15 19:12:12 -07:00
ba418d357f Make type_env a class. 2020-09-15 19:10:36 -07:00
0e3f16139d Make llvm_context a class. 2020-09-15 19:08:00 -07:00
55486d511f Make some refactors for name mangling and encapsulation. 2020-09-15 18:51:28 -07:00
6080094c41 Require mangled names for global variables. 2020-09-15 14:39:31 -07:00
6b8d3b0f8a Refactor errors and update post draft. 2020-09-11 21:29:49 -07:00
725958137a Factor type into case strategy constructor. 2020-09-11 13:03:00 -07:00
1f6b4bef74 Start working on part 13 of compiler series. 2020-09-11 02:16:57 -07:00
fe1e0a6de0 Switch to using FILE* and default YY_INPUT. 2020-09-11 02:16:29 -07:00
1f3c42fc44 Change constructor visibility to global.
Constructors are always effectively global.
2020-09-10 20:11:55 -07:00
8bf67c7dc3 Merge branch 'master' of https://dev.danilafe.com/Web-Projects/blog-static into master 2020-09-10 18:47:55 -07:00
13214cee96 Try out unboxing integers. 2020-09-10 17:32:16 -07:00
579c7bad92 Enable more syntax. 2020-09-10 16:04:44 -07:00
f00a6a7783 Actually use the environment for binop functions. 2020-09-10 16:03:56 -07:00
2a81fdd9fb Stop using mangled names for local variables. 2020-09-10 15:14:19 -07:00
17c59e595c Add assertion regarding local name mangling. 2020-09-10 15:05:02 -07:00
ad2576eae2 Move common code into loops. 2020-09-10 14:50:03 -07:00
72d8179cc5 Add compile-time flag to disable output. 2020-09-10 14:07:28 -07:00
dbabec0db6 Tweak parsed type error warning. 2020-09-10 14:04:06 -07:00
76675fbc9b Make make_case_for throw from the second time on.
Also clean up the errors thrown a little bit.
2020-09-10 14:03:04 -07:00
ca395b5c09 Add programs to trigger error cases. 2020-09-10 14:02:19 -07:00
1a05d5ff7a Add type errors to identifier nodes. 2020-09-10 12:59:26 -07:00
56f0dbd02f Prevent case compilation from crashing and burning. 2020-09-10 12:53:55 -07:00
9fc0ff961d Add more built-in boolean-specific instructions. 2020-09-10 12:44:41 -07:00
73441dc93b Register booleans as internal types. 2020-09-10 00:54:35 -07:00
df5f5eba1c Make sure to delete LLVM target machine. 2020-09-09 23:45:48 -07:00
d950b8dc90 Initialize graph indegree. 2020-09-09 23:44:53 -07:00
85394b185d Add prototype impl of case specialization.
Boolean cases could be translated to ifs, and
integer cases to jumps. That's still in progress.
2020-09-09 22:49:35 -07:00
86b49f9cc3 Add 'internal' types. 2020-09-09 18:08:38 -07:00
9769b3e396 Replace throw 0 with real exceptions or assertions. 2020-09-09 17:19:23 -07:00
e337992410 Add sources for unification type errors. 2020-09-09 15:26:18 -07:00
d5c3a44041 Add extra line after code fence. 2020-09-09 15:25:48 -07:00
eade42be49 Print locations in non-unification type errors. 2020-09-09 15:15:25 -07:00
d0fac50cfd Add locations to patterns. 2020-09-09 15:15:09 -07:00
dd4aa6fb9d Require C++17 for optionals 2020-09-09 15:14:37 -07:00
aa867b2e5f Add locations to error reporting. 2020-09-09 15:08:43 -07:00
2fa2be4b9e Add a method to print location. 2020-09-09 14:41:16 -07:00
d5536467f6 Touch up source index code. 2020-09-09 14:20:10 -07:00
67cb61c93f Keep track of locations in definitions. 2020-09-09 14:19:46 -07:00
578d580683 Make driver keep track of line numbers and locations. 2020-09-09 13:57:01 -07:00
789f277780 Update ASTs to actually take in locations.
Didn't realize I broke the build by leaving this out.
2020-09-09 13:29:28 -07:00
308ec615b9 Start using driver, and switch to file IO. 2020-09-09 13:28:43 -07:00
0e40c9e216 Enable locations. 2020-09-09 12:21:50 -07:00
5dbf75b5e4 Fork off version 13 of the compiler. 2020-09-08 18:38:05 -07:00
b921ddfc8d Update resume. 2020-09-02 13:47:55 -07:00
bf3c81fe24 Fix invalid property for flexbox. 2020-08-29 00:08:16 -07:00
06cbd93f05 Publish boolean values post. 2020-08-21 23:06:26 -07:00
6c3780d9ea Finish up the draft of the boolean values post. 2020-08-21 17:37:22 -07:00
6f0667bb28 Add draft of boolean values post. 2020-08-20 21:19:47 -07:00
8368283a3e Add warning about evaluation model. 2020-08-15 01:37:57 -07:00
18ee3a1526 Add margins to code tables. 2020-08-15 01:18:01 -07:00
536 changed files with 19241 additions and 20579 deletions

18
.gitmodules vendored Normal file
View File

@ -0,0 +1,18 @@
[submodule "code/aoc-2020"]
path = code/aoc-2020
url = https://dev.danilafe.com/Advent-of-Code/AdventOfCode-2020.git
[submodule "themes/vanilla"]
path = themes/vanilla
url = https://dev.danilafe.com/Web-Projects/vanilla-hugo.git
[submodule "code/server-config"]
path = code/server-config
url = https://dev.danilafe.com/Nix-Configs/server-config
[submodule "code/blog-static-flake"]
path = code/blog-static-flake
url = https://dev.danilafe.com/Nix-Configs/blog-static-flake.git
[submodule "code/compiler"]
path = code/compiler
url = https://dev.danilafe.com/DanilaFe/bloglang.git
[submodule "code/agda-spa"]
path = code/agda-spa
url = https://dev.danilafe.com/DanilaFe/agda-spa.git

9
Gemfile Normal file
View 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
View 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

343
agda.rb Normal file
View File

@ -0,0 +1,343 @@
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
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 = 0
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
View 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) + ";")

View 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);

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

56
assets/scss/donate.scss Normal file
View File

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

View File

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

70
build-agda-html.rb Normal file
View 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

View 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

@ -0,0 +1 @@
Subproject commit 828b652d3b9266e27ef7cf5a8a7fb82e3fd3133f

1
code/aoc-2020 Submodule

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

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

112
code/catamorphisms/Cata.hs Normal file
View 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

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

View File

@ -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();
}

View File

@ -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)) {}
};

View File

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

View File

@ -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

View File

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

View File

@ -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))); }
;

View File

@ -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)); }
%%

View File

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

View File

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

View File

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

View File

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

View File

@ -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

View File

@ -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

View File

@ -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
}

View File

@ -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);
}

View File

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

View File

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

View File

@ -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))); }
;

View File

@ -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)); }
%%

View File

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

View File

@ -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);
};

View File

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

View File

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

View File

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

View File

@ -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})

View File

@ -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);
}

View File

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

View File

@ -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
}

View File

@ -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);
}

View File

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

View File

@ -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";
}

View File

@ -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") {}
};

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

@ -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))); }
;

View File

@ -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)); }
%%

View File

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

View File

@ -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);
};

View File

@ -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})

View File

@ -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);
}

View File

@ -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();
};

View File

@ -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 "??";
}

View File

@ -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);

View File

@ -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() {
}

View File

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

View File

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

View File

@ -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";
}

View File

@ -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") {}
};

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

@ -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))); }
;

View File

@ -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)); }
%%

View File

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

View File

@ -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);
};

View File

@ -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);
}

View File

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

View File

@ -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})

View File

@ -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);
}

View File

@ -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();
};

View File

@ -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 "??";
}

View File

@ -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);

View File

@ -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() {
}

View File

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

View File

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

View File

@ -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";
}

View File

@ -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") {}
};

View File

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

View File

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

View File

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

View File

@ -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));
}

View File

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

View File

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

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