Commit Graph

201 Commits

Author SHA1 Message Date
Danila Fedorin 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
Danila Fedorin 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
Danila Fedorin 48c3105f42 Finish and publish the IsSomething article 2023-08-31 22:16:26 -07:00
Danila Fedorin 032453c4d0 Add a first draft of the IsSomething article 2023-08-28 23:04:39 -07:00
Danila Fedorin f093868da1 Add the missing general-base pattern drawing code 2023-08-28 20:46:29 -07:00
Danila Fedorin 250884c7bc Edit and publish Alloy article 2023-06-04 21:56:45 -07:00
Danila Fedorin 23cf7c9e8b Finish initial draft of the Alloy article. 2023-05-14 21:13:23 -07:00
Danila Fedorin 384f5de765 Make some more progress on the Alloy article. 2023-05-14 16:00:55 -07:00
Danila Fedorin d8ab3f2226 Continue working on the Alloy blog post 2023-05-04 21:01:31 -07:00
Danila Fedorin 9ddd2dd3bc Add initial draft of alloy article 2023-05-04 01:03:58 -07:00
Danila Fedorin 846d85bb7a Add missing source file to typeclasses-are-logic post 2023-01-29 21:12:10 -08:00
Danila Fedorin 2d22f0b2f2 Remove the code for the linear multistep article, too 2023-01-01 15:27:27 -08:00
Danila Fedorin 1961e545c0 Extract compiler into its own repo 2023-01-01 15:09:41 -08:00
Danila Fedorin bd8c9d8cdc Add draft of compiler article 2022-08-10 19:26:04 -07:00
Danila Fedorin 57aecc46be Update and publish catamorphism article 2022-04-24 01:09:34 -07:00
Danila Fedorin 4043a5c1a3 Add a draft of the catmorphisms post 2022-04-22 17:20:32 -07:00
Danila Fedorin dc3f086b9d Update the blog flake submodule and Nix Blog post 2022-04-09 15:55:21 -07:00
Danila Fedorin b67c1ab615 Add some more to the Nix Blog post 2022-04-09 02:50:04 -07:00
Danila Fedorin 97c989e465 Add a draft about digit sum patterns. 2021-12-31 00:14:31 -08:00
Danila Fedorin d41973f1a8 Add server configuration as submodule 2021-12-03 19:38:16 -08:00
Danila Fedorin 826dde759f Finish a draft of the UCC evaluator article 2021-11-28 16:50:28 -08:00
Danila Fedorin 30c395151d Use a different representation of values and prove equivalence of UCC evalutor 2021-11-28 01:08:56 -08:00
Danila Fedorin d72e64c7f9 Fix Ltac2 bug in Dawn file 2021-11-27 23:13:08 -08:00
Danila Fedorin abdc8e5056 Cleanup DawnEval.v 2021-11-27 14:17:09 -08:00
Danila Fedorin bc754c7a7d Start working on a verified UCC evaluator. 2021-11-26 01:40:04 -08:00
Danila Fedorin c214d9ee37 Add the initial version of the Dawn article. 2021-11-20 23:21:03 -08:00
Danila Fedorin 3c905aa1d7 Add draft of TypeScript typesafe event emitter post 2021-09-04 18:32:08 -07:00
Danila Fedorin c44c718d06 Remove accidentally commited test submodule. 2021-01-11 16:58:33 -08:00
Danila Fedorin 5e4097453b Update submodule script to properly gather submodule paths. 2021-01-11 12:39:41 -08:00
Danila Fedorin b3ff2fe135 Add more text to draft. 2021-01-02 21:23:47 -08:00
Danila Fedorin 6a6f25547e Update post with tactic-based proof. 2021-01-02 18:33:02 -08:00
Danila Fedorin 06014eade9 Add AoC submodule. 2021-01-01 18:40:43 -08:00
Danila Fedorin 234b795157 Add Coq advent of code post. 2020-12-02 01:14:32 -08:00
Danila Fedorin b459e9cbfe Update typesafe imperative language post draft. 2020-11-01 23:56:55 -08:00
Danila Fedorin 52abe73ef7 Make the typesafe imperative language work properly. 2020-10-31 01:34:23 -07:00
Danila Fedorin f0fe481bcf Add post about the typesafe imperative language. 2020-10-30 19:07:30 -07:00
Danila Fedorin d153af5212 Get rid of more constructors and make mangled names optional. 2020-09-18 14:09:03 -07:00
Danila Fedorin a336b27b6c Remove unneeded explicit calls to std::string 2020-09-18 12:27:57 -07:00
Danila Fedorin 97eb4b6e3e Fix silent error in set_mangled_name 2020-09-18 12:02:37 -07:00
Danila Fedorin 5db864881a Fix use of wrong environment for name mangling. 2020-09-17 22:55:27 -07:00
Danila Fedorin 7226d66f67 Remove the parent method from type_env. 2020-09-17 22:35:12 -07:00
Danila Fedorin 8a352ed3ea Roll back optimization changes. 2020-09-17 20:45:24 -07:00
Danila Fedorin 02f8306c7b Use an instruction instead of a special-case boolean instruction. 2020-09-17 18:33:52 -07:00
Danila Fedorin 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
Danila Fedorin 7a631b3557 Make a few more things classes. 2020-09-17 18:30:41 -07:00
Danila Fedorin 5e13047846 Make global scope a class. 2020-09-15 19:45:05 -07:00
Danila Fedorin c17d532802 Make type_mgr a class. 2020-09-15 19:19:58 -07:00
Danila Fedorin 55e4e61906 Make mangler a class and reformat graph. 2020-09-15 19:13:48 -07:00
Danila Fedorin f2f88ab9ca Make env a class. 2020-09-15 19:12:12 -07:00
Danila Fedorin ba418d357f Make type_env a class. 2020-09-15 19:10:36 -07:00