855 Commits

Author SHA1 Message Date
7a088d6739 Edit, finish, and publish post on PL
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2025-12-31 21:27:55 -08:00
626baefd76 Do some aggressive trimming and editing.
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2025-12-30 00:06:17 -08:00
4602d02720 [WIP] 2/3 draft
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2025-12-29 23:07:55 -08:00
7fbd4ea9f8 Update theme with syntax highlighting fix
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2025-04-12 17:56:44 -07:00
6fd1e1962b Update theme
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2025-03-30 23:15:54 -07:00
62c338e382 Add a post on Chapel's runtime types
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2025-03-02 22:56:10 -08:00
40ea9ec637 Update theme for newer Hugo
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2025-03-02 19:00:05 -08:00
787e194d41 Update theme with new Hugo support
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2025-03-02 13:42:42 -08:00
71162e2db9 Update nokogiri more
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2025-03-02 13:36:08 -08:00
43debc65e4 Update nokogiri
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2025-03-02 13:27:09 -08:00
b07ea85b70 Update ruby scripts to use 'File.exist?'
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2025-03-02 11:32:55 -08:00
06e8b8e022 Keep KaTeX css files
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2025-02-23 17:01:49 -08:00
647f47a5f3 Remove KaTeX CSS includes if we don't need them.
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2025-02-23 14:43:49 -08:00
36e4feb668 Update theme
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2025-02-23 14:14:15 -08:00
11be991946 Print number of files processed 2025-02-23 13:25:18 -08:00
a8c2b1d05a Fix bug in subsetting script
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2025-02-23 13:16:33 -08:00
fb46142e9d Remove incorrect print
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2025-02-23 12:45:24 -08:00
0b33d03b73 Pass the font folder as part of argv
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2025-02-23 12:35:45 -08:00
804147caef Read SVG path from the command line
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2025-02-23 12:34:44 -08:00
d847d20666 Adjust Python script to also just accept HTML files as args
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2025-02-23 12:28:19 -08:00
07408d01a9 Use ARGV like other ruby post-processing scripts
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2025-02-23 12:22:06 -08:00
816a473913 Add a (ChatGPT-provided) script to perform subsetting
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2025-02-23 12:05:02 -08:00
ce8f8fb872 Add a (ChatGPT-provided) script to subset feather icons
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2025-02-23 11:58:41 -08:00
2f60004241 Update theme with instanced fonts
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2025-02-23 11:43:38 -08:00
7130c6bd11 Fix cross-linking in whitespace-trimmed files
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-12-26 12:35:03 -08:00
c5aacc060a Update theme with font improvements
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-12-26 11:53:29 -08:00
6048dc0b9c Mark SPA series as completed
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-12-25 19:07:26 -08:00
1f01c3caff Publish the last two posts in the SPA series
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-12-25 19:05:28 -08:00
bca44343eb Update theme with required shortcodes
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-12-25 19:04:10 -08:00
3b9c2edcdd Write up the "verified" portion of the forward analysis
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-12-25 19:03:51 -08:00
fa180ee24e Fix thevoid theme on light mode devices
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-12-04 13:58:32 -08:00
5846dd5d04 Fix typos
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-12-01 22:19:45 -08:00
f6b347eb05 Fix slugs and add example of constant propagation
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-12-01 22:19:08 -08:00
c1b27a13ae Add a draft post on forward analysis
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-12-01 22:16:02 -08:00
147658ee89 Update theme
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-11-28 20:41:21 -08:00
4017c52fee Add a link to the future (not-yet-written) forward analysis post
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-11-28 20:38:18 -08:00
65d290556f Write a new post about proving the connection between semantics and CFGs
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-11-28 20:33:08 -08:00
854dccd4d2 Update caption / description of SPA part 6
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-11-27 16:34:03 -08:00
07859cd1af Publish SPA part 6, for real this time
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-11-27 16:30:13 -08:00
19be7eb1f5 Edit and publish post on control flow graphs
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-11-27 16:27:26 -08:00
5de2ae1203 Publish 'the void'
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-11-27 15:13:34 -08:00
595a1ad99b More edits
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-11-27 12:27:56 -08:00
32ccfc76ae Merge branch 'thevoid' 2024-11-27 00:41:05 -08:00
ae0d54e567 Add draft warning to the void
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-11-27 00:40:44 -08:00
b774f0e088 More minor edits
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-11-27 00:40:32 -08:00
e294bcb2d0 Add conclusion and make some edits
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-11-27 00:21:47 -08:00
1322e0249c Update theme
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-11-26 19:52:02 -08:00
e40a05633c Update theme
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-11-25 19:17:13 -08:00
e5fb0a2929 Write more
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-11-16 15:25:26 -08:00
3bd1f0c8a0 Update Agda SPA imp 2024-11-16 15:16:57 -08:00
948759b7d4 Update the SPA repo
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-11-16 14:44:02 -08:00
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
b216581f2b Editing pass
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-11-03 15:54:18 -08:00
1060198b01 Finish draft-sans-ending 2024-11-02 20:43:22 -07:00
0485917a20 Transcribe more writing
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-10-31 23:47:29 -07: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
26a29865e7 Write some more 2024-08-08 16:13:57 -07:00
ba287130d3 Start working on "The Void" 2024-08-04 19:37:29 -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
b0e501f086 Publish the new typesafe interpreter post. 2020-08-12 15:48:53 -07:00
385ae59133 Merge branch 'colors' into master 2020-08-12 15:43:42 -07:00
49469bdf12 Fix issues in typesafe interpreter article. 2020-08-12 15:43:22 -07:00
020417e971 Add draft of new Idris typechecking post.
This one uses line highlights!
2020-08-12 01:38:38 -07:00
eff0de5330 Allow the codelines shortcode to use hl_lines. 2020-08-12 01:37:55 -07:00
b219f6855e Change highlight color for code. 2020-08-12 01:37:39 -07:00
068d0218b0 Fix typesafe interpreter post. 2020-08-11 19:54:45 -07:00
65215ccdd6 Start working on improving color handling in code. 2020-08-11 19:29:55 -07:00
3e9f6a14f2 Fix single-line scroll bug 2020-08-11 17:43:59 -07:00
7623787b1c Mention Kai's help in time traveling article. 2020-07-30 02:05:43 -07:00
e15daa8f6d Make the detailed time traveling example a subsection. 2020-07-30 01:09:30 -07:00
298cf6599c Publish time traveling post. 2020-07-30 00:58:48 -07:00
841930a8ef Add time traveling code. 2020-07-30 00:57:47 -07:00
9b37e496cb Add figure size classes to global CSS. 2020-07-30 00:57:27 -07:00
58e6ad9e79 Update lazy evaluation post with images and more. 2020-07-30 00:49:35 -07:00
3aa2a6783e Add images to time traveling post. 2020-07-29 20:09:32 -07:00
d64a0d1fcd Add version of typesafe interpreter with tuples. 2020-07-23 16:38:54 -07:00
ba141031dd Remove the tweet shortcode. 2020-07-23 13:50:09 -07:00
ebdc63f5a0 Make small edit to DELL post. 2020-07-23 13:45:24 -07:00
5af0a09714 Publish DELL post. 2020-07-23 13:41:33 -07:00
8a2bc2660c Update date on typesafe interpreter. 2020-07-22 14:38:01 -07:00
e59b8cf403 Edit and publish typesafe interpreter. 2020-07-22 14:35:19 -07:00
b078ef9a22 Remove implicit arguments from TypsafeIntrV2. 2020-07-22 14:30:47 -07:00
fdaec6d5a9 Make small adjustments to backend math post. 2020-07-21 15:34:46 -07:00
b631346379 Publish the mathematics post. 2020-07-21 14:55:52 -07:00
e9f2378b47 Resume working on the draft of time traveling. 2020-07-20 22:32:14 -07:00
7d2f78d25c Add links and make small clarifications. 2020-07-20 13:56:07 -07:00
1f734a613c Add the second part of the typechecking post. 2020-07-19 22:56:44 -07:00
a3c299b057 Start working on the improved type-safe interpreter. 2020-07-19 17:16:31 -07:00
12aedfce92 Make small fixes to math rendering code. 2020-07-19 14:09:24 -07:00
65645346a2 Adjust title in DELL post. 2020-07-18 20:47:38 -07:00
cb65e89e53 Add math rendering draft. 2020-07-18 20:47:16 -07:00
6a2fec8ef4 Update the about page. 2020-07-17 19:39:43 -07:00
aa59c90810 Add the draft of the DELL post. 2020-07-17 19:39:35 -07:00
2b317930a0 Add resume link. 2020-07-15 15:09:37 -07:00
e7d56dd4bd Clean up some styles. 2020-07-15 13:56:03 -07:00
a4fedb276d Adjust margin spacing. 2020-07-15 13:18:34 -07:00
277c0a2ce6 Rework sidenote spacing and TOC. 2020-07-15 13:13:47 -07:00
ef3c61e9e6 Make table of contents dark. 2020-06-30 22:15:22 -07:00
1908126607 Add border to code. 2020-06-30 21:31:16 -07:00
2d77f8489f Move hiding code into margin SCSS. 2020-06-30 21:22:19 -07:00
0371651fdd Fix headings on Starbound post. 2020-06-24 23:01:35 -07:00
01734d24f7 Get started on tables of contents. 2020-06-24 22:46:22 -07:00
71fc0546e0 Move move code into common 'margin node' mixin. 2020-06-24 22:06:08 -07:00
871a745702 Extract margin variables and mixins into separate file. 2020-06-24 14:21:56 -07:00
3f0df8ae0d Add links for 12th part of compiler series. 2020-06-21 22:21:43 -07:00
1746011c16 Publish 12th part of compiler series. 2020-06-21 00:51:04 -07:00
7c4cfbf3d4 Fix typechecking of mutually recursive functions. 2020-06-21 00:47:26 -07:00
8524e098a8 Make proofreading-based fixes. 2020-06-20 23:50:26 -07:00
971f58da9b Finish draft of part 12 of compiler series. 2020-06-20 22:03:57 -07:00
c496be1031 Finish implementation description in part 12. 2020-06-20 20:46:54 -07:00
21851e3a9c Add more content to part 12. 2020-06-19 02:22:08 -07:00
600d5b91ea Remove unneeded parent class. 2020-06-18 23:06:13 -07:00
09b90c3bbc Add line numbers to codelines shortode. 2020-06-18 22:30:01 -07:00
f6ca13d6dc Add more implementation content to part 12. 2020-06-18 22:29:38 -07:00
9c4d7c514f Add more content to post 12 draft. 2020-06-16 23:32:09 -07:00
ad1946e9fb Add first draft of lambdas. 2020-06-14 02:00:20 -07:00
68910458e8 Properly handle null types in pattern typechecking. 2020-06-14 00:43:39 -07:00
240e87eca4 Use mangled names in variable environments. 2020-06-13 23:43:52 -07:00
6b5f7e25b7 Maybe finish the let/in code? 2020-06-01 00:23:41 -07:00
e7229e644f Start working on translation. 2020-05-31 18:52:52 -07:00
08c8aca144 Start working on a lifted version of a definition. 2020-05-31 14:37:33 -07:00
7f8dae74ac Adjust type output. 2020-05-31 00:50:58 -07:00
08503116ff Mark some definitions as global, so as not to capture them. 2020-05-31 00:34:12 -07:00
a1d679a59d No longer destroy the list of free variables.
It so happens that this list will tell us which variables
need to be captured.
2020-05-30 23:29:36 -07:00
4586bd0188 Check for free variables in the environment before generalizing. 2020-05-30 16:40:27 -07:00
a97b50f497 Add parsing of let/in. 2020-05-28 14:44:12 -07:00
c84ff11d0d Add typechecking to let/in expressions. 2020-05-26 00:52:54 -07:00
e966e74487 Extract ordering functionality into definition group. 2020-05-25 23:58:56 -07:00
3865abfb4d Add a struct to contain groups of mutually recursive definitions. 2020-05-25 22:11:45 -07:00
1905601aaa Fork off the 12th version of the compiler. 2020-05-25 21:20:41 -07:00
aacb9e2874 Prefer invisible text to unstyled text. 2020-05-25 20:55:20 -07:00
78f3b18969 Increase padding in post lists. 2020-05-17 22:00:10 -07:00
9f73ca2950 Remove bold font weight on post lists.
Some checks failed
continuous-integration/drone/push Build is failing
2020-05-09 17:53:55 -07:00
035b98a602 Start using description meta.
Some checks failed
continuous-integration/drone/push Build is failing
2020-05-09 17:29:57 -07:00
17f4ebc297 Add media screen to all stylesheets. 2020-05-09 17:02:13 -07:00
906e15674e Make minor edits to the content 2020-05-09 16:52:05 -07:00
85bd0b6c9c Switch to left-alignment on small screens to prevent ugly gaps.
Some checks failed
continuous-integration/drone/push Build is failing
2020-05-09 01:48:22 -07:00
b19e8713e0 Center post titles and word counters. 2020-05-09 01:45:53 -07:00
68fb78e765 Only left-justify post titles 2020-05-09 01:41:10 -07:00
be8a0a4a3a Left jusify text in links to prevent random variation
Some checks failed
continuous-integration/drone/push Build is failing
2020-05-04 19:55:48 -07:00
e883e3c60e Update link lists to visually indicate they're links.
Some checks failed
continuous-integration/drone/push Build is failing
2020-05-04 19:25:03 -07:00
4ede62b39a Stop displaying links in bold.
Some checks failed
continuous-integration/drone/push Build is failing
2020-05-04 03:56:21 -07:00
7d9f487a78 Stop using revert due to Chrome issues
Some checks failed
continuous-integration/drone/push Build is failing
2020-05-04 03:47:53 -07:00
9da584ded4 Make page lists bold
Some checks failed
continuous-integration/drone/push Build is failing
2020-05-04 03:36:23 -07:00
9452c90cf3 Switch back to Raleway 2020-05-04 03:35:24 -07:00
a80064f40a Merge branch 'master' of https://dev.danilafe.com/Web-Projects/blog-static 2020-05-04 03:29:48 -07:00
49691803cc Stop displaying links as inline-block 2020-05-04 03:28:17 -07:00
ee4738b245 Add redesign CSS 2020-05-04 03:23:55 -07:00
b270fa78da Add draft of lazy evaluation post 2020-05-04 01:58:25 -07:00
18339d7e4d Build and test version 11 of the compiler instead of 10.
Some checks failed
continuous-integration/drone/push Build is failing
2020-04-26 21:28:34 -07:00
78563448fb Update to LLVM 10.
Some checks failed
continuous-integration/drone/push Build is failing
2020-04-26 21:24:24 -07:00
144d5f3324 Try to fix compiler build failure
Some checks failed
continuous-integration/drone/push Build is failing
2020-04-26 21:05:28 -07:00
0fb315ec47 Prevent single-column tables in the case of highlighting
Some checks failed
continuous-integration/drone/push Build is failing
2020-04-26 20:47:51 -07:00
1ff67341a1 Disable live uploading while the new server doesn't accept the files.
Some checks failed
continuous-integration/drone/push Build is failing
2020-04-26 19:57:50 -07:00
a441280812 Add article about Crystal and Nix with OpenSSL.
Some checks failed
continuous-integration/drone/push Build is failing
2020-04-26 19:56:15 -07:00
eda9bbb191 Add more to part 12 of compiler series 2020-04-25 18:07:32 -07:00
2d9da2899f Switch to no line breaks (for Ghostwriter support) 2020-04-25 15:45:15 -07:00
a95490d9d4 Add more content to part 12 of compiler series
Some checks failed
continuous-integration/drone/push Build is failing
2020-04-22 00:30:42 -07:00
44135b1824 Add experimental figure-based styles 2020-04-22 00:30:22 -07:00
4a0367b401 Start work on part 12 of compiler series
Some checks failed
continuous-integration/drone/push Build is failing
2020-04-21 20:44:02 -07:00
c1f0104edb Add missing arity checks to compiler series
Some checks failed
continuous-integration/drone/push Build is failing
2020-04-14 19:21:33 -07:00
c9a7fbf6dd Finalize part 10 of compiler series
Some checks failed
continuous-integration/drone/push Build is failing
2020-04-14 19:06:29 -07:00
1f00b6a3f8 Make compiler check for arity in part 11 of compiler series.
Some checks failed
continuous-integration/drone/push Build is failing
2020-04-14 16:20:12 -07:00
acb22c4119 Finish draft of part 11 of compiler series 2020-04-14 16:19:54 -07:00
be2b855ffe Rename inaccurately named rule 2020-04-14 15:58:25 -07:00
88c9418350 Update example to include polymorphism 2020-04-14 15:58:13 -07:00
2255543d94 Add more work on part 11 of compiler series
Some checks failed
continuous-integration/drone/push Build is failing
2020-04-14 00:15:32 -07:00
b4c91d2dd4 Adjust grammar to allow for broader range of type inputs. 2020-04-13 23:17:34 -07:00
98c1b5a3b2 Make substitution replace types at every lookup step 2020-04-13 17:59:57 -07:00
122a1d73d3 Integrate new types into the rest of the project 2020-04-13 17:12:43 -07:00
74e6dba914 Add parsed type data structure, type application and arity. 2020-04-13 17:08:03 -07:00
d7846e0b32 Fork off code for part 11 of compiler series.
Some checks failed
continuous-integration/drone/push Build is failing
2020-04-09 23:48:53 -07:00
902ffc0bc0 Add missing backslashes
Some checks failed
continuous-integration/drone/push Build is failing
2020-04-09 22:55:02 -07:00
8c1168d818 Add seemingly missing string includes. 2020-04-09 16:26:10 -07:00
fd77fe078a Disable Google Analytics
Some checks failed
continuous-integration/drone/push Build is failing
2020-04-08 21:50:44 -07:00
7f3883fb39 Remove KaTeX JavaScript from page.
All checks were successful
continuous-integration/drone/push Build is passing
2020-04-07 15:30:04 -07:00
6a2698e911 Fix weird typo in part 11 of compiler series 2020-04-07 15:28:40 -07:00
569fea74a7 Make some progress on part 11 of compiler series 2020-04-04 23:16:01 -07:00
b04d82f0b3 Make small fixes to compiler series posts
All checks were successful
continuous-integration/drone/push Build is passing
2020-03-30 19:59:40 -07:00
33cd4f5f68 Start working on part 11 of compiler series
All checks were successful
continuous-integration/drone/push Build is passing
2020-03-28 22:26:47 -07:00
49cf8e3e08 Add links to the article everywhere else
All checks were successful
continuous-integration/drone/push Build is passing
2020-03-25 17:40:40 -07:00
c53a8ba68e Finish and publish part 10 of compiler series
All checks were successful
continuous-integration/drone/push Build is passing
2020-03-25 17:15:53 -07:00
5cccb97ede Add missing source file
All checks were successful
continuous-integration/drone/push Build is passing
2020-03-25 03:36:17 -07:00
493419f324 Remove debug output
Some checks failed
continuous-integration/drone/push Build is failing
2020-03-25 03:35:30 -07:00
577e0ad930 Finalize draft of polymorphism post
Some checks failed
continuous-integration/drone/push Build is failing
2020-03-25 03:22:21 -07:00
2a12f7f31e Switch to using type schemes and implement polymorphism in compiler series 2020-03-24 23:04:51 -07:00
ae3e661d7a Implement new ordered typing in compiler series 2020-03-24 22:00:11 -07:00
0efa05142f Separate definitions in compiler series 2020-03-24 21:08:06 -07:00
6714e18e7c Switch type environment to using pointers 2020-03-24 18:04:01 -07:00
5d53678e83 Only store type in case expression
All checks were successful
continuous-integration/drone/push Build is passing
2020-03-24 17:53:06 -07:00
3cb66a606d Make MathJax post public
All checks were successful
continuous-integration/drone/push Build is passing
2020-03-24 16:41:11 -07:00
074db07275 Add 'math rendering is wrong' draft
All checks were successful
continuous-integration/drone/push Build is passing
2020-03-15 18:43:28 -07:00
e3834ed6ea Explain graph code
All checks were successful
continuous-integration/drone/push Build is passing
2020-03-14 21:04:13 -07:00
1bdb4a650e Start work on algorithms in compiler post 10
All checks were successful
continuous-integration/drone/push Build is passing
2020-03-14 17:18:06 -07:00
6966973497 Set up script to test latest compiler version
All checks were successful
continuous-integration/drone/push Build is passing
2020-03-10 22:26:02 -07:00
8ee016e189 Fork into version 10 of the compiler for blog series 2020-03-10 20:58:26 -07:00
fa0a96f057 Remove horizontal scroll because it adds vertical scroll (?).
All checks were successful
continuous-integration/drone/push Build is passing
2020-03-10 18:46:35 -07:00
a2c84f5c40 Make KaTeX scrollable
All checks were successful
continuous-integration/drone/push Build is passing
2020-03-10 18:39:56 -07:00
768c43df2d Write up the instantiation rule and the new type checking algorithm in compiler series.
All checks were successful
continuous-integration/drone/push Build is passing
2020-03-10 18:36:26 -07:00
579d988f4a Remove lambda abstraction rule from part 10 of compiler series.
All checks were successful
continuous-integration/drone/push Build is passing
2020-03-09 22:55:12 -07:00
45bc113e3f Add some more text to polymorphism post
All checks were successful
continuous-integration/drone/push Build is passing
2020-03-09 22:30:27 -07:00
1abc13b20f Allow stack cells to be bigger
All checks were successful
continuous-integration/drone/push Build is passing
2020-03-08 00:38:19 -08:00
cdc9e28c90 Remove sidenote from stack post 2020-03-08 00:38:05 -08:00
8a48a110ff Avoid duplicating generated CSS by splitting SASS into separate files 2020-03-08 00:35:11 -08:00
0eb1abd26d Add note about n being zero to stack post
All checks were successful
continuous-integration/drone/push Build is passing
2020-03-08 00:23:28 -08:00
a7a6d7ff13 Stop using images and use HTML/CSS to render stacks 2020-03-08 00:20:30 -08:00
fb544e0545 Fix missing argument to slide in stack recursion post
All checks were successful
continuous-integration/drone/push Build is passing
2020-03-07 14:22:56 -08:00
84029fbc5b Finalize stack/recursion post
All checks were successful
continuous-integration/drone/push Build is passing
2020-03-06 23:06:45 -08:00
8039e459fa Finalize stack draft writeup
All checks were successful
continuous-integration/drone/push Build is passing
2020-03-06 22:50:30 -08:00
f202c8ea44 Start on the recursion tutorial post
All checks were successful
continuous-integration/drone/push Build is passing
2020-03-06 21:28:09 -08:00
d8d1aa66e6 Start working on explanations in Part 10 of Compiler series 2020-03-06 17:54:22 -08:00
79ef221820 Make KaTeX not break inside math, and clean up container code 2020-03-06 17:54:00 -08:00
67ecc741d0 Switch more posts to work with KaTeX and the latex macro
All checks were successful
continuous-integration/drone/push Build is passing
2020-03-04 14:07:05 -08:00
80d722568e Begin switching towards KaTeX
All checks were successful
continuous-integration/drone/push Build is passing
2020-03-02 23:50:49 -08:00
b9fcac974d Use the new latex shortcode to remove backslashes 2020-03-02 23:50:28 -08:00
31e9e58304 Fix typo in part 2 of compiler series
All checks were successful
continuous-integration/drone/push Build is passing
2020-03-02 21:56:47 -08:00
8f09b518ba Add sidenote delimiters to make the site not look bad with CSS off 2020-03-02 21:30:23 -08:00
2d6aab6b71 Add special table style and factor out media queries
All checks were successful
continuous-integration/drone/push Build is passing
2020-03-01 16:07:38 -08:00
6712c0064a Finalize new Drone configuration
All checks were successful
continuous-integration/drone/push Build is passing
2020-02-29 23:16:49 -08:00
5e6d97ab36 Add drone fix 15/?: try to control Hugo through environment variable
All checks were successful
continuous-integration/drone/push Build is passing
2020-02-29 23:13:59 -08:00
ea753fdfe7 Add drone fix 14/?: even more uses of ls
All checks were successful
continuous-integration/drone/push Build is passing
2020-02-29 23:12:06 -08:00
1db8a24b4d Add drone fix 13/?: try to figure out where Hugo puts files
All checks were successful
continuous-integration/drone/push Build is passing
2020-02-29 23:10:13 -08:00
f8adac8b76 Add drone fix 12/?: unset HUGO_TARGET
All checks were successful
continuous-integration/drone/push Build is passing
2020-02-29 23:04:40 -08:00
4bae586e36 Add drone fix 11/?: make hugo generate verbose output
Some checks failed
continuous-integration/drone/push Build is failing
2020-02-29 23:00:45 -08:00
3522c34adf Add drone fix 10/?: remove broken echo command
Some checks failed
continuous-integration/drone/push Build is failing
2020-02-29 22:57:49 -08:00
96fc519b3c Add drone fix 9/?: remove volume use and try use another output directory
Some checks failed
continuous-integration/drone/push Build is failing
2020-02-29 22:56:49 -08:00
28f686eb80 Add drone fix 8/?: add more debug output
All checks were successful
continuous-integration/drone/push Build is passing
2020-02-29 22:50:03 -08:00
6f0c95e49c Add drone fix 7/?: add = to Hugo commands
All checks were successful
continuous-integration/drone/push Build is passing
2020-02-29 22:47:58 -08:00
130086db00 Add drone fix 6/?: add more debug output
All checks were successful
continuous-integration/drone/push Build is passing
2020-02-29 22:44:21 -08:00
2a1ad171c0 Add drone fix 5/?: add debug output and skip compiler build
All checks were successful
continuous-integration/drone/push Build is passing
2020-02-29 22:42:19 -08:00
db8a050bdf Add drone fix 4/?: use Drone volume in rsync step
All checks were successful
continuous-integration/drone/push Build is passing
2020-02-29 22:32:42 -08:00
3ff5ce4dec Add drone fix 4/?: Use a drone volume to preserve storage
Some checks failed
continuous-integration/drone/push Build is failing
2020-02-29 22:29:26 -08:00
9f8855a4d3 Add drone fix 3/?: Split build and upload into steps
Some checks failed
continuous-integration/drone/push Build is failing
2020-02-29 22:18:33 -08:00
d3515d3fa5 Add drone fix 2/?: switch to an image with hugo-ext
Some checks failed
continuous-integration/drone/push Build is failing
2020-02-29 22:03:03 -08:00
277427af57 Add drone fix 1/?: set up ssh-agent
Some checks failed
continuous-integration/drone/push Build is failing
2020-02-29 21:52:01 -08:00
f6c1079bda Try to set up drone for live CI uploads
Some checks failed
continuous-integration/drone/push Build is failing
2020-02-29 21:48:08 -08:00
252d82469c Add a latex macro to help escape and write multiline latex 2020-02-29 20:42:36 -08:00
1879ba2c2b Add styling for tables. 2020-02-29 20:16:57 -08:00
fc444c1986 Resume work on polymorphism post 2020-02-29 20:15:37 -08:00
ae9805e4f2 Finish draft of Idris post
All checks were successful
continuous-integration/drone/push Build is passing
2020-02-29 17:52:45 -08:00
33b1457e91 Add first draft of Idris post 2020-02-29 16:12:12 -08:00
9e399ebe3c Add initial draft of typesafe interpreter post
All checks were successful
continuous-integration/drone/push Build is passing
2020-02-27 23:09:51 -08:00
eac1151616 Do not attribute G-machine to SPJ specifically
All checks were successful
continuous-integration/drone/push Build is passing
2020-02-23 21:29:21 -08:00
f7a7100fea Reword explanation of Update + Pop 2020-02-23 21:26:56 -08:00
c207d1dfcf Remove unused line at the end of works1.txt 2020-02-23 21:26:37 -08:00
df051fd643 Fix n vs n-1 mistake 2020-02-23 21:20:32 -08:00
419ab937b6 Switch to full text RSS 2020-02-23 21:01:41 -08:00
7ff919c31b Make the shortcodes HTML-specific 2020-02-23 20:24:40 -08:00
ee90351c17 Add Crystal Nix post
All checks were successful
continuous-integration/drone/push Build is passing
2020-02-16 22:55:25 -08:00
fbdbf67ce3 Add gettext to build requirements to satisfy flex
All checks were successful
continuous-integration/drone/push Build is passing
2020-02-11 19:28:24 -08:00
a7e32d300a Add bison and flex to build requirements
Some checks failed
continuous-integration/drone/push Build is failing
2020-02-11 19:17:31 -08:00
56387cb936 Add make to pacman command
Some checks failed
continuous-integration/drone/push Build is failing
2020-02-11 18:56:55 -08:00
df965816ac Update pacman command to download database files.
Some checks failed
continuous-integration/drone/push Build is failing
2020-02-11 18:53:39 -08:00
c7341c9b15 Try again to include all the required tooling
Some checks failed
continuous-integration/drone/push Build is failing
2020-02-11 18:52:06 -08:00
00322d7e9f Try switch to an image with CMake.
Some checks failed
continuous-integration/drone/push Build is failing
2020-02-11 18:47:40 -08:00
ef93632130 Add garbage collection post to main link
Some checks failed
continuous-integration/drone/push Build is failing
2020-02-11 18:40:59 -08:00
0f744888ef Move testing code into a script 2020-02-11 18:37:21 -08:00
a5b84bab69 Revert to YAML 2020-02-11 14:25:44 -08:00
12725500a8 Try wrap pipeline in array 2020-02-11 14:20:47 -08:00
1917c08e51 Messing around to try get the syntax right, part 2 2020-02-11 14:03:24 -08:00
b304057560 Messing around to try get the syntax right 2020-02-11 14:02:13 -08:00
e5a39d8dfb Replace ints with strings 2020-02-11 13:50:05 -08:00
54ccef9c72 Remove string interpolation for a bit 2020-02-11 13:48:30 -08:00
c103c6acbf Try to build multiple compiler versions 2020-02-11 13:40:00 -08:00
d6f53076c0 Switch to jsonnet syntax
All checks were successful
continuous-integration/drone/push Build is passing
2020-02-11 13:35:36 -08:00
b07ea8fe9c Add initial drone configuration file
All checks were successful
continuous-integration/drone/push Build is passing
2020-02-11 13:25:10 -08:00
9a7441779f Fix typo in compiler series 2020-02-10 19:38:46 -08:00
a6f27e446d Remove draft flag and update date on 9th compiler post 2020-02-10 19:23:15 -08:00
e7f0ccfa16 Finish compiler series 2020-02-10 19:18:55 -08:00
e5d01a4e19 Add the primes program from compiler series 2020-02-10 18:13:04 -08:00
b7d72f2fbf Implement garbage collection in runtime 2020-02-06 11:32:19 -08:00
281dbbd174 Track allocated nodes using a G-machine struct in compiler series. 2020-02-06 10:05:26 -08:00
153349f3d5 Add intermediate style to fit right sidenotes 2020-02-03 13:38:21 -08:00
8d22acfe78 Switch to single stack in runtime for Compiler Series 2020-01-31 15:29:12 -08:00
c1b030ee97 Bump polymorphism compiler post up one spot 2020-01-27 20:34:04 -08:00
803f52b2d0 Update the compiler to leave the stack clean 2020-01-27 20:29:01 -08:00
2f96abeef6 Instantiate compiler for garbage collection 2020-01-27 14:52:25 -08:00
163fcd2b2e Revert "Update style to use inches". It sucks!
This reverts commit 133979218a.
2020-01-15 18:32:34 -08:00
9ddcb1b3f2 Merge branch 'master' of dev.danilafe.com:Web-Projects/blog-static 2020-01-15 13:06:23 -08:00
133979218a Update style to use inches 2020-01-15 13:05:03 -08:00
ef545be03c Fix warnings from Hugo 2020-01-06 19:19:55 -08:00
c534dc7508 Remove draft tag from GHC IDE post 2020-01-06 18:49:28 -08:00
263ffe2b8c Add GHC IDE instructions for Haskell 2020-01-06 18:38:44 -08:00
67181fb033 Finish third post in CS325 series. 2020-01-03 23:47:36 -08:00
a026e67a3b Add first draft of Homework 3 (CS325) 2020-01-03 21:09:15 -08:00
d9544398b9 Add homework 3 solution for CS325 2020-01-02 21:20:32 -08:00
1c4bb29fdd Fix minor grammar mistake 2020-01-01 11:18:49 -08:00
765d497724 Address missing problem and make some other improvements in CS325HW2 2020-01-01 11:12:44 -08:00
80410c9200 Extract common parsing code 2019-12-31 21:59:13 -08:00
4e918db5cb Add the post for the second homework assignment. 2019-12-30 23:28:22 -08:00
382102f071 Add solution to CS325 hw2 2019-12-30 20:04:39 -08:00
6e88780f8b Add favicon to HTML 2019-12-30 14:56:09 -08:00
e3035b9d66 Make G-machine CSS use rem 2019-12-30 14:50:00 -08:00
8765626898 Fix typo on index page 2019-12-30 14:42:36 -08:00
c38247df9e Add ID to broken sidenote 2019-12-30 14:32:09 -08:00
baf44f8627 Fix todo 2019-12-29 22:51:59 -08:00
19aa126025 Add the first post in CS325 series 2019-12-29 22:47:36 -08:00
a406fb0846 Add first draft of Language 1 for CS325 2019-12-28 23:12:15 -08:00
75664e90bb Add solutions for HW1 for CS325 madness 2019-12-27 23:20:37 -08:00
f74209c970 Add common code for CS325 madness 2019-12-27 23:20:18 -08:00
c7ce8a3107 Add homework assignments 2019-12-27 23:18:00 -08:00
b3b906dd90 Add polymorphism draft 2019-12-27 23:13:23 -08:00
b8e0e0b4ce Change CSS to use rems 2019-12-27 23:12:35 -08:00
eb02e1e6b0 Fix broken link 2019-12-24 15:30:12 -08:00
b2fc6ea5a8 Add numbered sidenotes 2019-12-09 23:11:28 -08:00
f75a47e273 Add post about sidenotes 2019-12-08 23:47:52 -08:00
9eae560cae Make sidenotes mobile-friendly 2019-12-07 00:16:59 -08:00
b0529a9124 Add initial implementation of sidenotes 2019-12-06 00:10:26 -08:00
3df9c57482 Fix naming issue (this is really a compiler bug) 2019-12-05 19:36:47 -08:00
cb5163e1d9 Add gitignore file 2019-12-04 14:35:23 -08:00
c309ac4c14 Rename page and add pop instruction to part 5 of compiler series 2019-11-14 11:05:17 -08:00
58c9d5f982 Fix another typo in compiler series 2019-11-13 13:51:32 -08:00
dc9a68ad10 Fix mistakes in blog posts 2019-11-13 13:49:47 -08:00
db16dbda18 Fix incorrect CMakeLists.txt 2019-11-13 13:47:04 -08:00
172630c2ee Stop justifying titles and add lang attribute 2019-11-11 15:36:59 -08:00
6dc7734c70 Remove more draft labels 2019-11-06 22:32:57 -08:00
19a1ffbc98 Remove draft label 2019-11-06 22:32:21 -08:00
2cce2859bb Fix some typos 2019-11-06 22:27:52 -08:00
654239e29f Fix last sentence of compiler post 2019-11-06 21:34:29 -08:00
50fbe3e196 Finish draft of post 8 in compiler series 2019-11-06 21:10:53 -08:00
1a8a1c3052 Work on writing up the rest of part 8 in compiler series 2019-11-06 14:44:53 -08:00
2994f8983d Add the push operation in code in compiler series 2019-11-06 13:23:59 -08:00
64227f2873 Finish implementation of compiler 2019-11-06 12:52:42 -08:00
9aef499deb Factor out definition into separate file in compiler series 2019-11-05 10:40:51 -08:00
c79b5a4120 Start writing actual compillation code in compiler series 2019-11-05 00:42:33 -08:00
81ee50d0d4 Implement function and type creation, add text to blog in compiler series 2019-11-04 18:25:54 -08:00
43b140285f Fix missing line in runtime header in compiler series 2019-11-04 13:30:18 -08:00
adb894869e Remove code border. 2019-11-02 17:53:31 -07:00
1f6032a30e Start work on chapter 8 code for compilers 2019-11-02 17:53:15 -07:00
9531f4d8e3 Add chapter 8 starting code for compiler series 2019-11-02 16:38:11 -07:00
37097d3a40 Change SCSS to use darken, and remove input styles. 2019-10-31 14:41:52 -07:00
3aa468c2f6 Remove debug printf 2019-10-31 14:38:06 -07:00
c704187012 Use darken to specify link color 2019-10-31 14:32:34 -07:00
a834fd578e Finish initial draft of runtime posts. 2019-10-30 14:21:13 -07:00
4b5e2f4454 Write some more about runetime 2019-10-30 00:19:56 -07:00
7812b1064b Make progress on compiler posts 2019-10-26 20:30:29 -07:00
65b9f385cf Start working on runtime chapter 2019-10-15 11:13:13 -07:00
ed88d54aa6 Add post about LSP idea 2019-10-12 13:12:18 -07:00
d1b515ec5b Make max width higher 2019-10-12 00:31:43 -07:00
1ffc43af98 Link compiler posts together 2019-10-10 18:15:37 -07:00
b27dc19e57 Finish draft of part 6 of compiler series 2019-10-10 18:00:13 -07:00
df0b819b0e Fix bug from small improvements 2019-10-10 17:59:44 -07:00
21f90d85c5 Add finishing touches to code for part 6 of compiler series 2019-10-10 13:14:00 -07:00
18e3f2af55 Fix definition to resolve its own types 2019-10-09 22:51:19 -07:00
3901c9b115 Add print methods to instructions 2019-10-09 22:46:17 -07:00
d9486d08ae Fix type in compiler blog 2019-10-08 23:50:21 -07:00
d90993a93c Implement ast_case::compile for compiler series and reference code 2019-10-08 23:46:35 -07:00
7e9bd95846 Write explanations of AST refactor in compiler series 2019-10-08 21:42:25 -07:00
d3d73e0e9c Fix up compile in compiler blog part 6, and add more text. 2019-10-08 14:10:05 -07:00
d9c151d774 Continue implementation of compilation 2019-10-01 23:23:52 -07:00
384 changed files with 34188 additions and 3746 deletions

38
.drone.yml Normal file
View File

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

1
.gitignore vendored Normal file
View File

@@ -0,0 +1 @@
**/build/*

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.8)
nokogiri (1.18.3)
mini_portile2 (~> 2.8.2)
racc (~> 1.4)
racc (1.8.1)
PLATFORMS
ruby
DEPENDENCIES
duktape
execjs
nokogiri
BUNDLED WITH
2.1.4

351
agda.rb Normal file
View File

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

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.exist?(file)
value = File.size(file)
url = file.gsub(/^content/, "https://danilafe.com").delete_suffix("/index.md").delete_suffix(".md")
File.readlines(file).each do |l|
if l =~ /^title: (.+)$/
name = $~[1].delete_prefix('"').delete_suffix('"')
elsif l =~ /^draft: true$/
draft = true
elsif l =~ /^series: (.+)$/
this_series = $~[1]
series_list = series.fetch(this_series) do
series[this_series] = []
end
series_list << file
elsif l =~ /^tags: (.+)$/
tags = $~[1].delete_prefix("[").delete_suffix("]").split(/,\s?/).map { |it| it.gsub('"', '') }
if tags.include? "Compilers"
group = 2
elsif tags.include? "Coq"
group = 3
elsif tags.include? "Programming Languages"
group = 4
elsif tags.include? "Haskell"
group = 5
elsif tags.include? "Crystal"
group = 6
elsif tags.include? "Agda"
group = 7
elsif tags.include? "Hugo"
group = 8
end
end
end
next if draft
data[file] = { :id => id, :name => name, :group => group, :tags => tags, :url => url, :value => value }
end
edges = []
files.each do |file1|
# files.each do |file2|
# next if file1 == file2
# next unless data[file1][:tags].any? { |t| data[file2][:tags].include? t }
# edges << { :from => data[file1][:id], :to => data[file2][:id] }
# end
next unless frefs = refs[file1]
frefs.each do |ref|
next unless data[file1]
next unless data[ref]
edges << { :from => data[file1][:id], :to => data[ref][:id] }
end
end
series.each do |series, files|
files.sort.each_cons(2) do |file1, file2|
next unless data[file1]
next unless data[file2]
edges << { :from => data[file1][:id], :to => data[file2][:id] }
edges << { :from => data[file2][:id], :to => data[file1][:id] }
end
end
edges.uniq!
# edges.filter! { |e| e[:from] < e[:to] }
edges.map! { |e| { :from => [e[:from], e[:to]].min, :to => [e[:from], e[:to]].max } }.uniq!
puts ("export const nodes = " + JSON.pretty_unparse(data.values) + ";")
puts ("export const edges = " + JSON.pretty_unparse(edges) + ";")

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

View File

@@ -1,14 +1,14 @@
$basic-border: 1px solid #bfbfbf; @import "variables.scss";
@import "mixins.scss";
.gmachine-instruction { .gmachine-instruction {
display: flex; display: flex;
border: $basic-border; @include bordered-block;
border-radius: 2px;
} }
.gmachine-instruction-name { .gmachine-instruction-name {
padding: 10px; padding: .8rem;
border-right: $basic-border; border-right: $standard-border;
flex-grow: 1; flex-grow: 1;
flex-basis: 20%; flex-basis: 20%;
text-align: center; text-align: center;
@@ -20,7 +20,7 @@ $basic-border: 1px solid #bfbfbf;
} }
.gmachine-inner { .gmachine-inner {
border-bottom: $basic-border; border-bottom: $standard-border;
width: 100%; width: 100%;
&:last-child { &:last-child {
@@ -29,12 +29,12 @@ $basic-border: 1px solid #bfbfbf;
} }
.gmachine-inner-label { .gmachine-inner-label {
padding: 10px; padding: .8rem;
font-weight: bold; font-weight: bold;
} }
.gmachine-inner-text { .gmachine-inner-text {
padding: 10px; padding: .8rem;
text-align: right; text-align: right;
flex-grow: 1; flex-grow: 1;
} }

19
assets/scss/stack.scss Normal file
View File

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

430
assets/scss/thevoid.scss Normal file
View File

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

70
build-agda-html.rb Normal file
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.exist? data_file
# Extending code_paths from submodules.json means that nested Agda modules
# have their root dir correctly set.
max_path = ->(path) {
code_paths.max_by do |code_path|
count = 0
path.chars.zip(code_path.chars) do |c1, c2|
break unless c1 == c2
count += 1
end
next count
end
}
files_for_paths = {}
Dir.glob("**/*.agda", base: root_path) do |agda_file|
best_path = max_path.call(agda_file)
files_for_path = files_for_paths.fetch(best_path) do
files_for_paths[best_path] = []
end
files_for_path << agda_file[best_path.length + File::SEPARATOR.length..-1]
end
original_wd = Dir.getwd
files_for_paths.each do |path, files|
Dir.chdir(original_wd)
Dir.chdir(File.join(root_path, path))
html_dir = File.join [target_dir, path, "html"]
FileUtils.mkdir_p html_dir
files.each do |file|
command = "#{ARGV[0]} #{file} --html --html-dir=#{html_dir}"
puts command
puts `#{command}`
# Allow some programs to fail (e.g., IO.agda in SPA without --guardedness)
# fail unless $? == 0
end
end

View File

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

69
chatgpt-subset-one-go.py Normal file
View File

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

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

Submodule code/agda-spa added at 9131214880

1
code/aoc-2020 Submodule

Submodule code/aoc-2020 added at 7a8503c3fe

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

Submodule code/compiler added at 137455b0f4

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,144 +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();
if(!dynamic_cast<type_base*>(case_type.get())) {
throw type_error("attempting case analysis of non-data 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::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,26 +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
${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,144 +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();
if(!dynamic_cast<type_base*>(case_type.get())) {
throw type_error("attempting case analysis of non-data 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::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,170 +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 {
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 compile(const env_ptr env,
std::vector<instruction>& into) const;
};
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>;
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,9 +0,0 @@
#pragma once
enum binop {
PLUS,
MINUS,
TIMES,
DIVIDE
};

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,31 +0,0 @@
#pragma once
#include <memory>
#include <string>
struct env {
virtual ~env() = default;
virtual int get_offset(const std::string& name) const = 0;
};
using env_ptr = std::shared_ptr<env>;
struct env_var {
std::string name;
env_ptr parent;
env_var(std::string& n, env_ptr p)
: name(std::move(n)), parent(std::move(p)) {}
virtual int get_offset(const std::string& name) const;
};
struct env_offset {
int offset;
env_ptr parent;
env_offset(int o, env_ptr p)
: offset(o), parent(std::move(p)) {}
virtual int get_offset(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 @@
#pragma once
#include <string>
#include <memory>
#include "binop.hpp"
struct instruction {
virtual ~instruction() = default;
};
using instruction_ptr = std::unique_ptr<instruction>;
struct instruction_pushint : public instruction {
int value;
instruction_pushint(int v)
: value(v) {}
};
struct instruction_pushglobal : public instruction {
std::string name;
instruction_pushglobal(std::string n)
: name(std::move(n)) {}
};
struct instruction_push : public instruction {
int offset;
instruction_push(int o)
: offset(o) {}
};
struct instruction_mkapp : public instruction {
};
struct instruction_update : public instruction {
int offset;
instruction_update(int o)
: offset(o) {}
};
struct instruction_pack : public instruction {
int tag;
int size;
instruction_pack(int t, int s)
: tag(t), size(s) {}
};
struct instruction_split : public instruction {
};
struct instruction_slide : public instruction {
int offset;
instruction_slide(int o)
: offset(o) {}
};
struct instruction_binop : public instruction {
binop op;
instruction_binop(binop o)
: op(o) {}
};
struct instruction_eval : public instruction {
};
struct instruction_alloc : public instruction {
int amount;
instruction_alloc(int a)
: amount(a) {}
};
struct instruction_unwind : public instruction {
};

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

@@ -0,0 +1,119 @@
CS 325-001, Analysis of Algorithms, Fall 2019
HW1 - Python 3, qsort, BST, and qselect
Due electronically on flip on Monday 9/30 at 11:59pm.
No late submission will be accepted.
Need to submit on flip: report.txt, qsort.py, and qselect.py.
qselect.py will be automatically graded for correctness (1%).
flip $ /nfs/farm/classes/eecs/fall2019/cs325-001/submit hw1 qselect.py qsort.py report.txt
Note:
1. You can ssh to flip machines from your own machine by:
$ ssh access.engr.oregonstate.edu
2. You can add /nfs/farm/classes/eecs/fall2019/cs325-001/ to your $PATH:
$ export PATH=$PATH:/nfs/farm/classes/eecs/fall2019/cs325-001/
and add the above command to your ~/.bash_profile,
so that you don't need to type it every time.
(alternatively, you can use symbolic links or aliases to avoid typing the long path)
3. You can choose to submit each file separately, or submit them together.
Textbooks for References:
[1] CLRS Ch. 9.2 and Ch. 12
0. Q: What's the best-case, worst-case, and average-case time complexities of quicksort.
Briefly explain each case.
1. [WILL BE GRADED]
Quickselect with Randomized Pivot (CLRS Ch. 9.2).
>>> from qselect import *
>>> qselect(2, [3, 10, 4, 7, 19])
4
>>> qselect(4, [11, 2, 8, 3])
11
Q: What's the best-case, worst-case, and average-case time complexities? Briefly explain.
Filename: qselect.py
2. Buggy Qsort Revisited
In the slides we showed a buggy version of qsort which is weird in an interesting way:
it actually returns a binary search tree for the given array, rooted at the pivot:
>>> from qsort import *
>>> tree = sort([4,2,6,3,5,7,1,9])
>>> tree
[[[[], 1, []], 2, [[], 3, []]], 4, [[[], 5, []], 6, [[], 7, [[], 9, []]]]]
which encodes a binary search tree:
4
/ \
2 6
/ \ / \
1 3 5 7
\
9
Now on top of that piece of code, add three functions:
* sorted(t): returns the sorted order (infix traversal)
* search(t, x): returns whether x is in t
* insert(t, x): inserts x into t (in-place) if it is missing, otherwise does nothing.
>>> sorted(tree)
[1, 2, 3, 4, 5, 6, 7, 9]
>>> search(tree, 6)
True
>>> search(tree, 6.5)
False
>>> insert(tree, 6.5)
>>> tree
[[[[], 1, []], 2, [[], 3, []]], 4, [[[], 5, []], 6, [[[], 6.5, []], 7, [[], 9, []]]]]
>>> insert(tree, 3)
>>> tree
[[[[], 1, []], 2, [[], 3, []]], 4, [[[], 5, []], 6, [[[], 6.5, []], 7, [[], 9, []]]]]
Hint: both search and insert should depend on a helper function _search(tree, x) which
returns the subtree (a list) rooted at x when x is found, or the [] where x should
be inserted.
e.g.,
>>> tree = sort([4,2,6,3,5,7,1,9]) # starting from the initial tree
>>> _search(tree, 3)
[[], 3, []]
>>> _search(tree, 0)
[]
>>> _search(tree, 6.5)
[]
>>> _search(tree, 0) is _search(tree, 6.5)
False
>>> _search(tree, 0) == _search(tree, 6.5)
True
Note the last two []'s are different nodes (with different memory addresses):
the first one is the left child of 1, while the second one is the left child of 7
(so that insert is very easy).
Filename: qsort.py
Q: What are the time complexities for the operations implemented?
Debriefing (required!): --------------------------
1. Approximately how many hours did you spend on this assignment?
2. Would you rate it as easy, moderate, or difficult?
3. Did you work on it mostly alone, or mostly with other people?
4. How deeply do you feel you understand the material it covers (0%100%)?
5. Any other comments?
This section is intended to help us calibrate the homework assignments.
Your answers to this section will *not* affect your grade; however, skipping it
will certainly do.

View File

@@ -0,0 +1,170 @@
CS 325, Algorithms (MS/MEng-level), Fall 2019
HW10 - Challenge Problem - RNA Structure Prediction (6%)
This problem combines dynamic programming and priority queues.
Due Wednesday 12/4, 11:59pm.
No late submission will be accepted.
Include in your submission: report.txt, rna.py.
Grading:
* report.txt -- 1%
* 1-best structure -- 2%
* number of structures -- 1%
* k-best structures -- 2%
Textbooks for References:
[1] KT Ch. 6.5 (DP over intervals -- RNA structure)
[2] KT slides: DP I (RNA section)
http://www.cs.princeton.edu/~wayne/kleinberg-tardos/
***Please analyze time/space complexities for each problem in report.txt.
1. Given an RNA sequence, such as ACAGU, we can predict its secondary structure
by tagging each nucleotide as (, ., or ). Each matching pair of () must be
AU, GC, or GU (or their mirror symmetries: UA, CG, UG).
We also assume pairs can _not_ cross each other.
The following are valid structures for ACAGU:
ACAGU
.....
...()
..(.)
.(.).
(...)
((.))
We want to find the structure with the maximum number of matching pairs.
In the above example, the last structure is optimal (2 pairs).
>>> best("ACAGU")
(2, '((.))')
Tie-breaking: arbitrary. Don't worry as long as your structure
is one of the correct best structures.
some other cases (more cases at the bottom):
GCACG
(2, '().()')
UUCAGGA
(3, '(((.)))')
GUUAGAGUCU
(4, '(.()((.)))')
AUAACCUUAUAGGGCUCUG
(8, '.(((..)()()((()))))')
AACCGCUGUGUCAAGCCCAUCCUGCCUUGUU
(11, '(((.(..(.((.)((...().))()))))))')
GAUGCCGUGUAGUCCAAAGACUUCACCGUUGG
(14, '.()()(()(()())(((.((.)(.))()))))')
CAUCGGGGUCUGAGAUGGCCAUGAAGGGCACGUACUGUUU
(18, '(()())(((((.)))()(((())(.(.().()()))))))')
ACGGCCAGUAAAGGUCAUAUACGCGGAAUGACAGGUCUAUCUAC
(19, '.()(((.)(..))(((.()()(())))(((.)((())))))())')
AGGCAUCAAACCCUGCAUGGGAGCACCGCCACUGGCGAUUUUGGUA
(20, '.(()())...((((()()))((()(.()(((.)))()())))))()')
2. Total number of all possible structures
>>> total("ACAGU")
6
3. k-best structures: output the 1-best, 2nd-best, ... kth-best structures.
>>> kbest("ACAGU", 3)
[(2, '((.))'), (1, '(...)'), (1, '.(.).')]
The list must be sorted.
Tie-breaking: arbitrary.
In case the input k is bigger than the number of possible structures, output all.
Sanity check: kbest(s, 1)[0][0] == best(s)[0] for each RNA sequence s.
All three functions should be in one file: rna.py.
See more testcases at the end.
Debriefing (required!): --------------------------
0. What's your name?
1. Approximately how many hours did you spend on this assignment?
2. Would you rate it as easy, moderate, or difficult?
3. Did you work on it mostly alone, or mostly with other people?
4. How deeply do you feel you understand the material it covers (0%-100%)?
5. Any other comments?
This section is intended to help us calibrate the homework assignments.
Your answers to this section will *not* affect your grade; however, skipping it
will certainly do.
TESTCASES:
for each sequence s, we list three lines:
best(s)
total(s)
kbest(s, 10)
ACAGU
(2, '((.))')
6
[(2, '((.))'), (1, '.(.).'), (1, '..(.)'), (1, '...()'), (1, '(...)'), (0, '.....')]
------
AC
(0, '..')
1
[(0, '..')]
------
GUAC
(2, '(())')
5
[(2, '(())'), (1, '()..'), (1, '.().'), (1, '(..)'), (0, '....')]
------
GCACG
(2, '().()')
6
[(2, '().()'), (1, '(..).'), (1, '()...'), (1, '.(..)'), (1, '...()'), (0, '.....')]
------
CCGG
(2, '(())')
6
[(2, '(())'), (1, '(.).'), (1, '.().'), (1, '.(.)'), (1, '(..)'), (0, '....')]
------
CCCGGG
(3, '((()))')
20
[(3, '((()))'), (2, '((.)).'), (2, '(.()).'), (2, '.(()).'), (2, '.(().)'), (2, '.((.))'), (2, '((.).)'), (2, '(.(.))'), (2, '(.().)'), (2, '((..))')]
------
UUCAGGA
(3, '(((.)))')
24
[(3, '(((.)))'), (2, '((.).).'), (2, '((..)).'), (2, '(.(.)).'), (2, '((.))..'), (2, '.((.)).'), (2, '.((.).)'), (2, '.((..))'), (2, '((..).)'), (2, '((.)..)')]
------
AUAACCUA
(2, '.((...))')
19
[(2, '((.)..).'), (2, '(()...).'), (2, '()(...).'), (2, '().(..).'), (2, '()....()'), (2, '.()(..).'), (2, '.()...()'), (2, '.(.)..()'), (2, '.((...))'), (2, '.(.(..))')]
------
UUGGACUUG
(4, '(()((.)))')
129
[(4, '(())(.)()'), (4, '(()((.)))'), (3, '(().)..()'), (3, '(().).(.)'), (3, '(().)(..)'), (3, '((.))..()'), (3, '((.)).(.)'), (3, '((.))(..)'), (3, '(())(..).'), (3, '(())(.)..')]
------
UUUGGCACUA
(4, '(.()()(.))')
179
[(4, '((()).).()'), (4, '((.)()).()'), (4, '(.()()).()'), (4, '.(()()).()'), (4, '.(()()(.))'), (4, '((()).(.))'), (4, '((.)()(.))'), (4, '((()())..)'), (4, '(.()()(.))'), (3, '((()).)...')]
------
GAUGCCGUGUAGUCCAAAGACUUC
(11, '(((()()((()(.))))((.))))')
2977987
[(11, '(()())(((()().))(((.))))'), (11, '(()())(((()()).)(((.))))'), (11, '(()())(((()(.)))(((.))))'), (11, '(()()()((()(.)))(((.))))'), (11, '(((()()((()().)))((.))))'), (11, '(((()()((()(.))))((.))))'), (11, '(()()()((()()).)(((.))))'), (11, '(()()()((()().))(((.))))'), (11, '(((()()((()()).))((.))))'), (10, '(()()()((()().).)((.))).')]
------
AGGCAUCAAACCCUGCAUGGGAGCG
(10, '.(()())...((((()()))).())')
560580
[(10, '.(()())...((((())())).)()'), (10, '.(()())...((((()()))).)()'), (10, '.(()())...(((()(()))).)()'), (10, '.(()())...(((()(()))).())'), (10, '.(()())...((((())())).())'), (10, '.(()())...((((()()))).())'), (9, '((.).)(...(.((()()))).)()'), (9, '((.).)(...(((.)(()))).)()'), (9, '((.).)(...(.(()(()))).)()'), (9, '((.).)(...((.(()()))).)()')]
------

View File

@@ -0,0 +1,42 @@
HW11 -- OPTIONAL (for your practice only -- solutions will be released on Tuesday)
Edit Distance (see updated final review solutions)
flip $ /nfs/farm/classes/eecs/fall2019/cs325-001/submit hw11 edit.py
Implement two functions:
* distance1(s, t): Viterbi-style (either top-down or bottom-up)
* distance2(s, t): Dijkstra-style (best-first)
For Dijkstra, you can use either heapdict or heapq (see review problem 7).
Given that this graph is extremely sparse (why?), heapq (ElogE) might be faster than heapdict (ElogV)
because the latter has overhead for hash.
They should return the same result (just return the edit distance).
We have 10 testcases (listed below); the first 5 test distance1(),
and the second 5 test distance2() on the same 5 string pairs.
My solutions (on flip2):
Testing Case 1 (open)... 0.001 s, Correct
Testing Case 2 (open)... 0.000 s, Correct
Testing Case 3 (open)... 0.012 s, Correct
Testing Case 4 (open)... 0.155 s, Correct
Testing Case 5 (open)... 0.112 s, Correct
Testing Case 6 (hidden)... 0.000 s, Correct
Testing Case 7 (hidden)... 0.000 s, Correct
Testing Case 8 (hidden)... 0.004 s, Correct
Testing Case 9 (hidden)... 0.009 s, Correct
Testing Case 10 (hidden)... 0.021 s, Correct
Total Time: 0.316 s
distance1("abcdefh", "abbcdfg") == 3
distance1("pretty", "prettier") == 3
distance1("aaaaaaadaaaaaaaaaaaaaaaaacaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa", "aaaaaaaaaaaabaaaaaaaaaaaaaaaaaaaaaaaaaaaaaxaaaaaaaaaaaaaaaaaaaaaa") == 5
distance1('cpuyedzrwcbritzclzhwwabmlyresvewkdxwkamyzbxtwiqzvokqpkecyywrbvhlqgxzutdjfmvlhsezfbhfjbllmfhzlqlcwibubyyjupbwhztskyksfthkptxqlmhivfjbgclwsombvytdztapwpzmdqfwwrhqsgztobeuiatcwmrzfbwhfnpzzasomrhotoqiwvexlgxsnafiagfewmopdzwanxswfsmbxsmsczbwsgnwy', 'cpuyedzrwcbritzclzhwwabmlyresvewkdxwkamyzbtwiqzvokqpkecyywrbvhlqgxzutdjfmvlhsezfbhfjbllmfhzlqlcwibubyyjupbwhztskyksfthkptxqlmhivfbgclwsombvytdztapwpzmdqfwwrhqsgztobeuiatcwmrzfbwhfnpzzasonrhotoqiwvexlgxsnafiagfewmopdzwanxswfsmbxsmsczbwsgnwy') == 3
distance1('cpuyedzrwcbritzclzhwwabmlyresvewkdxwkamyzbtwiqzvokqpasdfkecyywrbvhlqgxzutdjfmvlhsezfbhbllmfhzlqlcwibubyyjupbwhztsxyksfthkptxqlmhivfjbgclhombvytdztapwpzmdqfwwrhqsgztobeuiatcwmrzfbwhfnpzzasomrttoqiwvexlgxsnafiagfewmopdzwanxswfsmbxsmsczbwsgnwydmbihjkvziitusmkjljrsbafytsinql', 'cpuyedzrwcbritzclzhwwabmlyresvewkdxwkamyzbtwiqzvokqpkecyywrbvhlqgxzutdjfmvlhsezfbhfjbllmfhzlqlcwibubyyjupbwhztskyksfthkptxqlmhivfjbgclwsombvytdztapwpzmdqfwwrhqsgztobeuiatcwmrzfbwhfnpzzasomrhotoqiwvexlgxsnafiagfewmopdzwanxswfsmbxsmsczbwsgnwydmbihjkvziitusmkjljrsbafytsinql') == 11
distance2("abcdefh", "abbcdfg") == 3
distance2("pretty", "prettier") == 3
distance2("aaaaaaadaaaaaaaaaaaaaaaaacaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa", "aaaaaaaaaaaabaaaaaaaaaaaaaaaaaaaaaaaaaaaaaxaaaaaaaaaaaaaaaaaaaaaa") == 5
distance2('cpuyedzrwcbritzclzhwwabmlyresvewkdxwkamyzbxtwiqzvokqpkecyywrbvhlqgxzutdjfmvlhsezfbhfjbllmfhzlqlcwibubyyjupbwhztskyksfthkptxqlmhivfjbgclwsombvytdztapwpzmdqfwwrhqsgztobeuiatcwmrzfbwhfnpzzasomrhotoqiwvexlgxsnafiagfewmopdzwanxswfsmbxsmsczbwsgnwy', 'cpuyedzrwcbritzclzhwwabmlyresvewkdxwkamyzbtwiqzvokqpkecyywrbvhlqgxzutdjfmvlhsezfbhfjbllmfhzlqlcwibubyyjupbwhztskyksfthkptxqlmhivfbgclwsombvytdztapwpzmdqfwwrhqsgztobeuiatcwmrzfbwhfnpzzasonrhotoqiwvexlgxsnafiagfewmopdzwanxswfsmbxsmsczbwsgnwy') == 3
distance2('cpuyedzrwcbritzclzhwwabmlyresvewkdxwkamyzbtwiqzvokqpasdfkecyywrbvhlqgxzutdjfmvlhsezfbhbllmfhzlqlcwibubyyjupbwhztsxyksfthkptxqlmhivfjbgclhombvytdztapwpzmdqfwwrhqsgztobeuiatcwmrzfbwhfnpzzasomrttoqiwvexlgxsnafiagfewmopdzwanxswfsmbxsmsczbwsgnwydmbihjkvziitusmkjljrsbafytsinql', 'cpuyedzrwcbritzclzhwwabmlyresvewkdxwkamyzbtwiqzvokqpkecyywrbvhlqgxzutdjfmvlhsezfbhfjbllmfhzlqlcwibubyyjupbwhztskyksfthkptxqlmhivfjbgclwsombvytdztapwpzmdqfwwrhqsgztobeuiatcwmrzfbwhfnpzzasomrhotoqiwvexlgxsnafiagfewmopdzwanxswfsmbxsmsczbwsgnwydmbihjkvziitusmkjljrsbafytsinql') == 11

View File

@@ -0,0 +1,80 @@
CS 325-001, Analysis of Algorithms, Fall 2019
HW2 - Divide-n-conquer: mergesort, number of inversions, longest path
Due Monday Oct 7, 11:59pm (same submission instructions as HW1).
No late submission will be accepted.
Need to submit: report.txt, msort.py, inversions.py, and longest.py.
longest.py will be graded for correctness (1%).
To submit:
flip $ /nfs/farm/classes/eecs/fall2019/cs325-001/submit hw2 report.txt {msort,inversions,longest}.py
(You can submit each file separately, or submit them together.)
To see your best results so far:
flip $ /nfs/farm/classes/eecs/fall2019/cs325-001/query hw2
Textbooks for References:
[1] CLRS Ch. 2
0. Which of the following sorting algorithms are (or can be made) stable?
(a) mergesort
(b) quicksort with the first element as pivot
(c) quicksort with randomized pivot
(d) selection sort
(e) insertion sort
(f) heap sort --- not covered yet (see CLRS Ch. 6)
1. Implement mergesort.
>>> mergesort([4, 2, 5, 1, 6, 3])
[1, 2, 3, 4, 5, 6]
Filename: msort.py
2. Calculate the number of inversions in a list.
>>> num_inversions([4, 1, 3, 2])
4
>>> num_inversions([2, 4, 1, 3])
3
Filename: inversions.py
Must run in O(nlogn) time.
3. [WILL BE GRADED]
Length of the longest path in a binary tree (number of edges).
We will use the "buggy qsort" representation of binary trees from HW1:
[left_subtree, root, right_subtree]
>>> longest([[], 1, []])
0
>>> longest([[[], 1, []], 2, [[], 3, []]])
2
>>> longest([[[[], 1, []], 2, [[], 3, []]], 4, [[[], 5, []], 6, [[], 7, [[], 9, []]]]])
5
Note the answer is 5 because the longest path is 1-2-4-6-7-9.
Filename: longest.py
Must run in O(n) time.
Debriefing (required!): --------------------------
1. Approximately how many hours did you spend on this assignment?
2. Would you rate it as easy, moderate, or difficult?
3. Did you work on it mostly alone, or mostly with other people?
Note you are encouraged to discuss with your classmates,
but each students should submit his/her own code.
4. How deeply do you feel you understand the material it covers (0%100%)?
5. Any other comments?
This section is intended to help us calibrate the homework assignments.
Your answers to this section will *not* affect your grade; however, skipping it
will certainly do.

View File

@@ -0,0 +1,83 @@
CS 325, Algorithms, Fall 2019
HW3 - K closest numbers; Two Pointers
Due Monday Oct 14, 11:59pm. (same submission instructions as HW1-2).
No late submission will be accepted.
Need to submit: report.txt, closest_unsorted.py, closest_sorted.py, xyz.py.
closest_sorted.py will be graded for correctness (1%).
To submit:
flip $ /nfs/farm/classes/eecs/fall2019/cs325-001/submit hw3 report.txt {closest*,xyz}.py
(You can submit each file separately, or submit them together.)
To see your best results so far:
flip $ /nfs/farm/classes/eecs/fall2019/cs325-001/query hw3
1. Given an array A of n numbers, a query x, and a number k,
find the k numbers in A that are closest (in value) to x.
For example:
find([4,1,3,2,7,4], 5.2, 2) returns [4,4]
find([4,1,3,2,7,4], 6.5, 3) returns [4,7,4]
find([5,3,4,1,6,3], 3.5, 2) returns [3,4]
Filename: closest_unsorted.py
Must run in O(n) time.
The elements in the returned list must be in the original order.
In case two numbers are equally close to x, choose the earlier one.
2. [WILL BE GRADED]
Now what if the input array is sorted? Can you do it faster?
find([1,2,3,4,4,7], 5.2, 2) returns [4,4]
find([1,2,3,4,4,7], 6.5, 3) returns [4,4,7]
Filename: closest_sorted.py
Must run in O(logn + k) time.
The elements in the returned list must be in the original order.
Note: in case two numbers are equally close to x, choose the smaller one:
find([1,2,3,4,4,6,6], 5, 3) returns [4,4,6]
find([1,2,3,4,4,5,6], 4, 5) returns [2,3,4,4,5]
Hint: you can use Python's bisect.bisect for binary search.
3. For a given array A of n *distinct* numbers, find all triples (x,y,z)
s.t. x + y = z. (x, y, z are distinct numbers)
e.g.,
find([1, 4, 2, 3, 5]) returns [(1,3,4), (1,2,3), (1,4,5), (2,3,5)]
Note that:
1) no duplicates in the input array
2) you can choose any arbitrary order for triples in the returned list.
Filename: xyz.py
Must run in O(n^2) time.
Hint: you can use any built-in sort in Python.
Debriefing (required!): --------------------------
0. What's your name?
1. Approximately how many hours did you spend on this assignment?
2. Would you rate it as easy, moderate, or difficult?
3. Did you work on it mostly alone, or mostly with other people?
Note you are encouraged to discuss with your classmates,
but each students should submit his/her own code.
4. How deeply do you feel you understand the material it covers (0%-100%)?
5. Which part(s) of the course you like the most so far?
6. Which part(s) of the course you dislike the most so far?
This section is intended to help us calibrate the homework assignments.
Your answers to this section will *not* affect your grade; however, skipping it
will certainly do.

View File

@@ -0,0 +1,114 @@
CS 325-001, Algorithms, Fall 2019
HW4 - Priority Queue and Heaps
Due via the submit program on Monday Oct 21, 11:59pm.
No late submission will be accepted.
Need to submit: report.txt, nbest.py, kmergesort.py, datastream.py.
datastream.py will be graded for correctness (1%).
To submit:
flip $ /nfs/farm/classes/eecs/fall2019/cs325-001/submit hw4 report.txt {nbest,kmergesort,datastream}.py
(You can submit each file separately, or submit them together.)
To see your best results so far:
flip $ /nfs/farm/classes/eecs/fall2019/cs325-001/query hw4
Textbooks for References:
[1] CLRS Ch. 6
[2] KT slides for binary heaps (only read the first 20 pages!):
https://www.cs.princeton.edu/~wayne/kleinberg-tardos/pdf/BinomialHeaps.pdf
[3] Python heapq module
0. There are two methods for building a heap from an unsorted array:
(1) insert each element into the heap --- O(nlogn) -- heapq.heappush()
(2) heapify (top-down) --- O(n) -- heapq.heapify()
(a) Derive these time complexities.
(b) Use a long list of random numbers to show the difference in time. (Hint: random.shuffle or random.sample)
(c) What about sorted or reversely-sorted numbers?
1. Given two lists A and B, each with n integers, return
a sorted list C that contains the smallest n elements from AxB:
AxB = { (x, y) | x in A, y in B }
i.e., AxB is the Cartesian Product of A and B.
ordering: (x,y) < (x',y') iff. x+y < x'+y' or (x+y==x'+y' and y<y')
You need to implement three algorithms and compare:
(a) enumerate all n^2 pairs, sort, and take top n.
(b) enumerate all n^2 pairs, but use qselect from hw1.
(c) Dijkstra-style best-first, only enumerate O(n) (at most 2n) pairs.
Hint: you can use Python's heapq module for priority queue.
Q: What are the time complexities of these algorithms?
>>> a, b = [4, 1, 5, 3], [2, 6, 3, 4]
>>> nbesta(a, b) # algorithm (a), slowest
[(1, 2), (1, 3), (3, 2), (1, 4)]
>>> nbestb(a, b) # algorithm (b), slow
[(1, 2), (1, 3), (3, 2), (1, 4)]
>>> nbestc(a, b) # algorithm (c), fast
[(1, 2), (1, 3), (3, 2), (1, 4)]
Filename: nbest.py
2. k-way mergesort (the classical mergesort is a special case where k=2).
>>> kmergesort([4,1,5,2,6,3,7,0], 3) # k=3
[0,1,2,3,4,5,6,7]
Q: What is the complexity? Write down the detailed analysis in report.txt.
Filename: kmergesort.py
3. [WILL BE GRADED]
Find the k smallest numbers in a data stream of length n (k<<n),
using only O(k) space (the stream itself might be too big to fit in memory).
>>> ksmallest(4, [10, 2, 9, 3, 7, 8, 11, 5, 7])
[2, 3, 5, 7]
>>> ksmallest(3, range(1000000, 0, -1))
[1, 2, 3]
Note:
a) it should work with both lists and lazy lists
b) the output list should be sorted
Q: What is your complexity? Write down the detailed analysis in report.txt.
Filename: datastream.py
[UPDATE] The built-in function heapq.nsmallest() is _not_ allowed for this problem.
The whole point is to implement it yourself. :)
4. (optional) Summarize the time complexities of the basic operations (push, pop-min, peak, heapify) for these implementations of priority queue:
(a) unsorted array
(b) sorted array (highest priority first)
(c) reversly sorted array (lowest priority first)
(d) linked list
(e) binary heap
Debriefing (required!): --------------------------
0. What's your name?
1. Approximately how many hours did you spend on this assignment?
2. Would you rate it as easy, moderate, or difficult?
3. Did you work on it mostly alone, or mostly with other people?
Note you are encouraged to discuss with your classmates,
but each students should submit his/her own code.
4. How deeply do you feel you understand the material it covers (0%-100%)?
5. Which part(s) of the course you like the most so far?
6. Which part(s) of the course you dislike the most so far?
This section is intended to help us calibrate the homework assignments.
Your answers to this section will *not* affect your grade; however, skipping it
will certainly do.

View File

@@ -0,0 +1,130 @@
CS 532-001, Algorithms, Fall 2019
HW5 - DP (part 1: simple)
HWs 5-7 are all on DPs.
Due Monday Oct 28, 11:59pm.
No late submission will be accepted.
Need to submit report.txt, mis.py, bsts.py, bitstrings.py.
mis.py will be graded for correctness (1%).
To submit:
flip $ /nfs/farm/classes/eecs/fall2019/cs325-001/submit hw5 report.txt {mis,bsts,bitstrings}.py
(You can submit each file separately, or submit them together.)
To see your best results so far:
flip $ /nfs/farm/classes/eecs/fall2019/cs325-001/query hw5
Textbooks for References:
[1] CLRS Ch. 15
[2] KT Ch. 6
or Ch. 5 in a previous version:
http://cs.furman.edu/~chealy/cs361/kleinbergbook.pdf
Hint: Among the three coding questions, p3 is the easiest, and p1 is similar to p3.
You'll realize that both are very similar to p0 (Fibonacci).
p2 is slightly different from these, but still very easy.
0. (Optional) Is Fibonacci REALLY O(n)?
Hint: the value of f(n) itself grows exponentially.
1. [WILL BE GRADED]
Maximum Weighted Independent Set
[HINT] independent set is a set where no two numbers are neighbors in the original list.
see also https://en.wikipedia.org/wiki/Independent_set_(graph_theory)
input: a list of numbers (could be negative)
output: a pair of the max sum and the list of numbers chosen
>>> max_wis([7,8,5])
(12, [7,5])
>>> max_wis([-1,8,10])
(10, [10])
>>> max_wis([])
(0, [])
[HINT] if all numbers are negative, the optimal solution is 0,
since [] is an independent set according to the definition above.
>>> max_wis([-5, -1, -4])
(0, [])
Q: What's the complexity?
Include both top-down (max_wis()) and bottom-up (max_wis2()) solutions,
and make sure they produce exact same results.
We'll only grade the top-down version.
Tie-breaking: any best solution is considered correct.
Filename: mis.py
[HINT] you can also use the naive O(2^n) exhaustive search method to verify your answer.
2. Number of n-node BSTs
input: n
output: number of n-node BSTs
>>> bsts(2)
2
>>> bsts(3)
5
>>> bsts(5)
42
[HINT] There are two 2-node BSTs:
2 1
/ \
1 2
Note that all other 2-node BSTs are *isomorphic* to either one.
Qa: What's the complexity of this DP?
Qb: What's the name of this famous number series?
Feel free to use any implementation style.
Filename: bsts.py
3. Number of bit strings of length n that has
1) no two consecutive 0s.
2) two consecutive 0s.
>>> num_no(3)
5
>>> num_yes(3)
3
[HINT] There are three 3-bit 0/1-strings that have two consecutive 0s.
001 100 000
The other five 3-bit 0/1-strings have no two consecutive 0s:
010 011 101 110 111
Feel free to choose any implementation style.
Filename: bitstrings.py
[HINT] Like problem 1, you can also use the O(2^n) exhaustive search method to verify your answer.
Debriefing (required!): --------------------------
0. What's your name?
1. Approximately how many hours did you spend on this assignment?
2. Would you rate it as easy, moderate, or difficult?
3. Did you work on it mostly alone, or mostly with other people?
4. How deeply do you feel you understand the material it covers (0%-100%)?
5. Which part(s) of the course you like the most so far?
6. Which part(s) of the course you dislike the most so far?
This section is intended to help us calibrate the homework assignments.
Your answers to this section will *not* affect your grade; however, skipping it
will certainly do.

View File

@@ -0,0 +1,114 @@
CS 325-001, Algorithms, Fall 2019
HW6 - DP (part 2)
Due on Monday Nov 4, 11:59pm.
No late submission will be accepted.
Need to submit: report.txt, knapsack_unbounded.py, knapsack_bounded.py.
knapsack_bounded.py will be graded for correctness (1%).
To submit:
flip $ /nfs/farm/classes/eecs/fall2019/cs325-001/submit hw6 report.txt knapsack*.py
(You can submit each file separately, or submit them together.)
To see your best results so far:
flip $ /nfs/farm/classes/eecs/fall2019/cs325-001/query hw6
Textbooks for References:
[1] KT Ch. 6.4
or Ch. 5.3 in a previous version:
http://cs.furman.edu/~chealy/cs361/kleinbergbook.pdf
[2] KT slides for DP (pages 1-37):
https://www.cs.princeton.edu/~wayne/kleinberg-tardos/pdf/06DynamicProgrammingI.pdf
[3] Wikipedia: Knapsack (unbounded and 0/1)
[4] CLRS Ch. 15
Please answer time/space complexities for each problem in report.txt.
0. For each of the coding problems below:
(a) Describe a greedy solution.
(b) Show a counterexample to the greedy solution.
(c) Define the DP subproblem
(d) Write the recurrence relations
(e) Do not forget base cases
(f) Analyze the space and time complexities
1. Unbounded Knapsack
You have n items, each with weight w_i and value v_i, and each has infinite copies.
**All numbers are positive integers.**
What's the best value for a bag of W?
>>> best(3, [(2, 4), (3, 5)])
(5, [0, 1])
the input to the best() function is W and a list of pairs (w_i, v_i).
this output means to take 0 copies of item 1 and 1 copy of item 2.
tie-breaking: *reverse* lexicographical: i.e., [1, 0] is better than [0, 1]:
(i.e., take as many copies from the first item as possible, etc.)
>>> best(3, [(1, 5), (1, 5)])
(15, [3, 0])
>>> best(3, [(1, 2), (1, 5)])
(15, [0, 3])
>>> best(3, [(1, 2), (2, 5)])
(7, [1, 1])
>>> best(58, [(5, 9), (9, 18), (6, 12)])
(114, [2, 4, 2])
>>> best(92, [(8, 9), (9, 10), (10, 12), (5, 6)])
(109, [1, 1, 7, 1])
Q: What are the time and space complexities?
filename: knapsack_unbounded.py
2. [WILL BE GRADED]
Bounded Knapsack
You have n items, each with weight w_i and value v_i, and has c_i copies.
**All numbers are positive integers.**
What's the best value for a bag of W?
>>> best(3, [(2, 4, 2), (3, 5, 3)])
(5, [0, 1])
the input to the best() function is W and a list of triples (w_i, v_i, c_i).
tie-breaking: same as in p1:
>>> best(3, [(1, 5, 2), (1, 5, 3)])
(15, [2, 1])
>>> best(3, [(1, 5, 1), (1, 5, 3)])
(15, [1, 2])
>>> best(20, [(1, 10, 6), (3, 15, 4), (2, 10, 3)])
(130, [6, 4, 1])
>>> best(92, [(1, 6, 6), (6, 15, 7), (8, 9, 8), (2, 4, 7), (2, 20, 2)])
(236, [6, 7, 3, 7, 2])
Q: What are the time and space complexities?
filename: knapsack_bounded.py
You are encouraged to come up with a few other testcases yourself to test your code!
Debriefing (required!): --------------------------
0. What's your name?
1. Approximately how many hours did you spend on this assignment?
2. Would you rate it as easy, moderate, or difficult?
3. Did you work on it mostly alone, or mostly with other people?
4. How deeply do you feel you understand the material it covers (0%-100%)?
5. Which part(s) of the course you like the most so far?
6. Which part(s) of the course you dislike the most so far?
This section is intended to help us calibrate the homework assignments.
Your answers to this section will *not* affect your grade; however, skipping it
will certainly do.

View File

@@ -0,0 +1,147 @@
CS 325-001, Algorithms, Fall 2019
HW8 - Graphs (part I); DP (part III)
Due on Monday November 18, 11:59pm.
No late submission will be accepted.
Include in your submission: report.txt, topol.py, viterbi.py.
viterbi.py will be graded for correctness (1%).
To submit:
flip $ /nfs/farm/classes/eecs/fall2019/cs325-001/submit hw8 report.txt {topol,viterbi}.py
(You can submit each file separately, or submit them together.)
To see your best results so far:
flip $ /nfs/farm/classes/eecs/fall2019/cs325-001/query hw8
Textbooks for References:
[1] CLRS Ch. 23 (Elementary Graph Algorithms)
[2] KT Ch. 3 (graphs), or Ch. 2 in this earlier version:
http://cs.furman.edu/~chealy/cs361/kleinbergbook.pdf
[3] KT slides (highly recommend!):
https://www.cs.princeton.edu/~wayne/kleinberg-tardos/pdf/03Graphs.pdf
[4] Jeff Erickson: Ch. 5 (Basic Graph Algorithms):
http://jeffe.cs.illinois.edu/teaching/algorithms/book/05-graphs.pdf
[5] DPV Ch. 3, 4.2, 4.4, 4.7 (Dasgupta, Papadimitriou, Vazirani)
https://www.cs.berkeley.edu/~vazirani/algorithms/chap3.pdf (decomposition of graphs)
https://www.cs.berkeley.edu/~vazirani/algorithms/chap4.pdf (paths, shortest paths)
[6] my advanced DP tutorial (up to page 16):
http://web.engr.oregonstate.edu/~huanlian/slides/COLING-tutorial-anim.pdf
Please answer non-coding questions in report.txt.
0. For the following graphs, decide whether they are
(1) directed or undirected, (2) dense or sparse, and (3) cyclic or acyclic:
(a) Facebook
(b) Twitter
(c) a family
(d) V=airports, E=direct_flights
(e) a mesh
(f) V=courses, E=prerequisites
(g) a tree
(h) V=linux_software_packages, E=dependencies
(i) DP subproblems for 0-1 knapsack
Can you name a very big dense graph?
1. Topological Sort
For a given directed graph, output a topological order if it exists.
Tie-breaking: ARBITRARY tie-breaking. This will make the code
and time complexity analysis a lot easier.
e.g., for the following example:
0 --> 2 --> 3 --> 5 --> 6
/ \ | / \
/ \ v / \
1 > 4 > 7
>>> order(8, [(0,2), (1,2), (2,3), (2,4), (3,4), (3,5), (4,5), (5,6), (5,7)])
[0, 1, 2, 3, 4, 5, 6, 7]
Note that order() takes two arguments, n and list_of_edges,
where n specifies that the nodes are named 0..(n-1).
If we flip the (3,4) edge:
>>> order(8, [(0,2), (1,2), (2,3), (2,4), (4,3), (3,5), (4,5), (5,6), (5,7)])
[0, 1, 2, 4, 3, 5, 6, 7]
If there is a cycle, return None
>>> order(4, [(0,1), (1,2), (2,1), (2,3)])
None
Other cases:
>>> order(5, [(0,1), (1,2), (2,3), (3,4)])
[0, 1, 2, 3, 4]
>>> order(5, [])
[0, 1, 2, 3, 4] # could be any order
>>> order(3, [(1,2), (2,1)])
None
>>> order(1, [(0,0)]) # self-loop
None
Tie-breaking: arbitrary (any valid topological order is fine).
filename: topol.py
questions:
(a) did you realize that bottom-up implementations of DP use (implicit) topological orderings?
e.g., what is the topological ordering in your (or my) bottom-up bounded knapsack code?
(b) what about top-down implementations? what order do they use to traverse the graph?
(c) does that suggest there is a top-down solution for topological sort as well?
2. [WILL BE GRADED]
Viterbi Algorithm For Longest Path in DAG (see DPV 4.7, [2], CLRS problem 15-1)
Recall that the Viterbi algorithm has just two steps:
a) get a topological order (use problem 1 above)
b) follow that order, and do either forward or backward updates
This algorithm captures all DP problems on DAGs, for example,
longest path, shortest path, number of paths, etc.
In this problem, given a DAG (guaranteed acyclic!), output a pair (l, p)
where l is the length of the longest path (number of edges), and p is the path. (you can think of each edge being unit cost)
e.g., for the above example:
>>> longest(8, [(0,2), (1,2), (2,3), (2,4), (3,4), (3,5), (4,5), (5,6), (5,7)])
(5, [0, 2, 3, 4, 5, 6])
>>> longest(8, [(0,2), (1,2), (2,3), (2,4), (4,3), (3,5), (4,5), (5,6), (5,7)])
(5, [0, 2, 4, 3, 5, 6])
>>> longest(8, [(0,1), (0,2), (1,2), (2,3), (2,4), (4,3), (3,5), (4,5), (5,6), (5,7), (6,7)])
(7, [0, 1, 2, 4, 3, 5, 6, 7]) # unique answer
Note that longest() takes two arguments, n and list_of_edges,
where n specifies that the nodes are named 0..(n-1).
Tie-breaking: arbitrary. any longest path is fine.
Filename: viterbi.py
Note: you can use this program to solve MIS, knapsacks, coins, etc.
Debriefing (required!): --------------------------
0. What's your name?
1. Approximately how many hours did you spend on this assignment?
2. Would you rate it as easy, moderate, or difficult?
3. Did you work on it mostly alone, or mostly with other people?
4. How deeply do you feel you understand the material it covers (0%-100%)?
5. Any other comments?
This section is intended to help us calibrate the homework assignments.
Your answers to this section will *not* affect your grade; however, skipping it
will certainly do.

View File

@@ -0,0 +1,166 @@
CS 325, Algorithms, Fall 2019
HW9 - Graphs (part 2), DP (part 4)
Due Monday Nov 25, 11:59pm.
No late submission will be accepted.
Include in your submission: report.txt, dijkstra.py, nbest.py.
dijkstra.py will be graded for correctness (1%).
Textbooks for References:
[1] CLRS Ch. 22 (graph)
[2] my DP tutorial (up to page 16):
http://web.engr.oregonstate.edu/~huanlian/slides/COLING-tutorial-anim.pdf
[3] DPV Ch. 3, 4.2, 4.4, 4.7, 6 (Dasgupta, Papadimitriou, Vazirani)
https://www.cs.berkeley.edu/~vazirani/algorithms/chap3.pdf
https://www.cs.berkeley.edu/~vazirani/algorithms/chap4.pdf
https://www.cs.berkeley.edu/~vazirani/algorithms/chap6.pdf
[4] KT Ch. 6 (DP)
http://www.aw-bc.com/info/kleinberg/assets/downloads/ch6.pdf
[5] KT slides: Greedy II (Dijkstra)
http://www.cs.princeton.edu/~wayne/kleinberg-tardos/
***Please answer time/space complexities for each problem in report.txt.
1. [WILL BE GRADED]
Dijkstra (see CLRS 24.3 and DPV 4.4)
Given an undirected graph, find the shortest path from source (node 0)
to target (node n-1).
Edge weights are guaranteed to be non-negative, since Dijkstra doesn't work
with negative weights, e.g.
3
0 ------ 1
\ /
2 \ / -2
\/
2
in this example, Dijkstra would return length 2 (path 0-2),
but path 0-1-2 is better (length 1).
For example (return a pair of shortest-distance and shortest-path):
1
0 ------ 1
\ / \
5 \ /1 \6
\/ 2 \
2 ------ 3
>>> shortest(4, [(0,1,1), (0,2,5), (1,2,1), (2,3,2), (1,3,6)])
(4, [0,1,2,3])
If the target node (n-1) is unreachable from the source (0),
return None:
>>> shortest(5, [(0,1,1), (0,2,5), (1,2,1), (2,3,2), (1,3,6)])
None
Another example:
1 1
0-----1 2-----3
>>> shortest(4, [(0,1,1), (2,3,1)])
None
Tiebreaking: arbitrary. Any shortest path would do.
Filename: dijkstra.py
Hint: please use heapdict from here:
https://raw.githubusercontent.com/DanielStutzbach/heapdict/master/heapdict.py
>>> from heapdict import heapdict
>>> h = heapdict()
>>> h['a'] = 3
>>> h['b'] = 1
>>> h.peekitem()
('b', 1)
>>> h['a'] = 0
>>> h.peekitem()
('a', 0)
>>> h.popitem()
('a', 0)
>>> len(h)
1
>>> 'a' in h
False
>>> 'b' in h
True
You don't need to submit heapdict.py; we have it in our grader.
2. [Redo the nbest question from Midterm, preparing for HW10 part 3]
Given k pairs of lists A_i and B_i (0 <= i < k), each with n sorted numbers,
find the n smallest pairs in all the (k n^2) pairs.
We say (x,y) < (x', y') if and only if x+y < x'+y'.
Tie-breaking: lexicographical (i.e., prefer smaller x).
You can base your code on the skeleton from the Midterm:
from heapq import heappush, heappop
def nbest(ABs): # no need to pass in k or n
k = len(ABs)
n = len(ABs[0][0])
def trypush(i, p, q): # push pair (A_i,p, B_i,q) if possible
A, B = ABs[i] # A_i, B_i
if p < n and q < n and ______________________________:
heappush(h, (________________, i, p, q, (A[p],B[q])))
used.add((i, p, q))
h, used = ___________________ # initialize
for i in range(k): # NEED TO OPTIMIZE
trypush(______________)
for _ in range(n):
_, i, p, q, pair = ________________
yield pair # return the next pair (in a lazy list)
_______________________
_______________________
But recall we had two optimizations to speed up the first for-loop (queue initialization):
(1) using heapify instead of k initial pushes. You need to implement this (very easy).
(2) using qselect to choose top n out of the k bests. This one is OPTIONAL.
Analyze the time complexity for the version you implemented.
>>> list(nbest([([1,2,4], [2,3,5]), ([0,2,4], [3,4,5])]))
[(0, 3), (1, 2), (0, 4)]
>>> list(nbest([([-1,2],[1,4]), ([0,2],[3,4]), ([0,1],[4,6]), ([-1,2],[1,5])]))
[(-1, 1), (-1, 1)]
>>> list(nbest([([5,6,10,14],[3,5,10,14]),([2,7,9,11],[3,8,12,16]),([1,3,8,10],[5,9,10,11]),([1,2,3,5],[3,4,9,10]),([4,5,9,10],[2,4,6,11]),([4,6,10,13],[2,3,5,9]),([3,7,10,12],[1,2,5,10]),([5,9,14,15],[4,8,13,14])]))
[(1, 3), (3, 1), (1, 4), (2, 3)]
>>> list(nbest([([1,6,8,13],[5,8,11,12]),([1,2,3,5],[5,9,11,13]),([3,5,7,10],[4,6,7,11]),([1,4,7,8],[4,9,11,15]),([4,8,10,13],[4,6,10,11]),([4,8,12,15],[5,10,11,13]),([2,3,4,8],[4,7,11,15]),([4,5,10,15],[5,6,7,8])]))
[(1, 4), (1, 5), (1, 5), (2, 4)]
This problem prepares you for the hardest question in HW10 (part 3).
Filename: nbest.py
Debriefing (required!): --------------------------
0. What's your name?
1. Approximately how many hours did you spend on this assignment?
2. Would you rate it as easy, moderate, or difficult?
3. Did you work on it mostly alone, or mostly with other people?
4. How deeply do you feel you understand the material it covers (0%-100%)?
5. Any other comments?
This section is intended to help us calibrate the homework assignments.
Your answers to this section will *not* affect your grade; however, skipping it
will certainly do.

View File

@@ -0,0 +1,19 @@
qselect(xs,k) =
~xs -> {
pivot <- xs[0]!
left <- xs[#0 <= pivot]
right <- xs[#0 > pivot]
} ->
if k > |left| + 1 then qselect(right, k - |left| - 1)
else if k == |left| + 1 then [pivot]
else qselect(left, k);
_search(xs, k) =
if xs[1] == k then xs
else if xs[1] > k then _search(xs[0], k)
else _search(xs[2], k);
sorted(xs) = sorted(xs[0]) ++ [xs[1]] ++ sorted(xs[2]);
search(xs, k) = |_search(xs, k)| != 0;
insert(xs, k) = _insert(k, _search(xs, k));
_insert(k, xs) = if |xs| == 0 then xs << [] << k << [] else xs

View File

@@ -0,0 +1,11 @@
state 0;
effect {
if(SOURCE == R) {
STATE = STATE + |LEFT|;
}
}
combine {
STATE = STATE + LSTATE + RSTATE;
}

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