| (* | |
| A formalization of first-order logic, theories and their models. | |
| As an example we formalize the language of ZF set theory and a a small fragment of ZF. | |
| *) | |
| (* A signature is given by function symbols, relation symbols, and their arities. *) | |
| Structure Signature := | |
| { funSym : Type (* names of function symbols *) | |
| ; funArity : funSym -> Type (* arities of function symbols *) | |
| ; relSym : Type (* names of relation symbols *) |
Every once in a while I investigate low-level backend options for PL-s, although so far I haven't actually written any such backend for my projects. Recently I've been looking at precise garbage collection in popular backends, and I've been (like on previous occasions) annoyed by limitations and compromises.
I was compelled to think about a system which accommodates precise relocating GC as much as possible. In one extreme configuration, described in this note, there
| type cps_var = | |
| (* Taken from the lambda term during CPS conversion. *) | |
| | CLamVar of string | |
| (* Generated uniquely during CPS conversion. *) | |
| | CGenVar of int | |
| type cps_term = | |
| | CFix of (cps_var * cps_var list * cps_term) list * cps_term | |
| | CAppl of cps_var * cps_var list | |
| | CRecord of cps_var list * binder |
| (* A variable identifier of the lambda language [term]. *) | |
| type var = string [@@deriving eq] | |
| (* The lambda language; direct style. *) | |
| type term = | |
| | Var of var | |
| | Fix of (var * var list * term) list * term | |
| | Appl of term * term list | |
| | Record of term list | |
| | Select of term * int |
| --------------------------- MODULE TLAPlus2Grammar --------------------------- | |
| EXTENDS Naturals, Sequences, BNFGrammars | |
| CommaList(L) == L & (tok(",") & L)^* | |
| AtLeast4(s) == Tok({s \o s \o s} & {s}^+) | |
| ReservedWord == | |
| { "ASSUME", "ELSE", "LOCAL", "UNION", | |
| "ASSUMPTION", "ENABLED", "MODULE", "VARIABLE", | |
| "AXIOM", "EXCEPT", "OTHER", "VARIABLES", |
| CFLAGS_ALL=-I../libusbgx/build/include -I../bcm2835-1.68/build/include -L../bcm2835-1.68/build/lib -I../lua-5.4.0/src -L../libusbgx/build/lib -L../libserialport/build/lib -L../lua-5.4.0/src -lpng -lz -lpthread -llua -lm -lbcm2835 -ldl | |
| pi400: CFLAGS+=-static $(CFLAGS_ALL) -lusbgx -lconfig -DPI400_USB | |
| pi400: pi400.c gadget-hid.c | |
| $(CC) $^ $(CFLAGS) -o $@ | |
| pi400test: CFLAGS+=-static $(CFLAGS_ALL) -lusbgx -lconfig | |
| pi400test: pi400.c gadget-hid.c | |
| $(CC) $^ $(CFLAGS) -o $@ |
| jtag newtap ecp5 tap -irlen 8 -expected-id 0x41111043 |
Here's a list of mildly interesting things about the C language that I learned mostly by consuming Clang's ASTs. Although surprises are getting sparser, I might continue to update this document over time.
There are many more mildly interesting features of C++, but the language is literally known for being weird, whereas C is usually considered smaller and simpler, so this is (almost) only about C.
struct foo {
struct bar {
int x;
| -- Exercise: prove Peirce’s law <=> law of excluded middle in Haskell | |
| {-# LANGUAGE Rank2Types #-} | |
| import Data.Void | |
| import Data.Bifunctor | |
| import Data.Functor.Identity | |
| type Not a = a -> Void |