948759b7d4
Update the SPA repo
...
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-11-16 14:44:02 -08:00
32fe8e5ee6
Update the referenced Agda submodule
...
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-08-18 10:30:21 -10: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
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
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
250884c7bc
Edit and publish Alloy article
2023-06-04 21:56:45 -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
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
846d85bb7a
Add missing source file to typeclasses-are-logic post
2023-01-29 21:12:10 -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
bd8c9d8cdc
Add draft of compiler article
2022-08-10 19:26:04 -07:00
57aecc46be
Update and publish catamorphism article
2022-04-24 01:09:34 -07:00
4043a5c1a3
Add a draft of the catmorphisms post
2022-04-22 17:20:32 -07:00
dc3f086b9d
Update the blog flake submodule and Nix Blog post
2022-04-09 15:55:21 -07:00
b67c1ab615
Add some more to the Nix Blog post
2022-04-09 02:50:04 -07:00
97c989e465
Add a draft about digit sum patterns.
2021-12-31 00:14:31 -08:00
d41973f1a8
Add server configuration as submodule
2021-12-03 19:38:16 -08:00
826dde759f
Finish a draft of the UCC evaluator article
2021-11-28 16:50:28 -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
c214d9ee37
Add the initial version of the Dawn article.
2021-11-20 23:21:03 -08:00
3c905aa1d7
Add draft of TypeScript typesafe event emitter post
2021-09-04 18:32:08 -07: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
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
06014eade9
Add AoC submodule.
2021-01-01 18:40:43 -08:00
234b795157
Add Coq advent of code post.
2020-12-02 01:14:32 -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
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
5db864881a
Fix use of wrong environment for name mangling.
2020-09-17 22:55:27 -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
