andrejbauer

(*
   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 *)

AndrasKovacs

Garbage collection with zero cost at non-GC time

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

Hirrolot

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

Hirrolot

(* 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

lemmy

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

Gadgetoid

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

racerxdl

jtag newtap ecp5 tap -irlen 8 -expected-id 0x41111043

rxwei

See the official Differentiable Programming Manifesto instead.

fay59

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.

1. Combined type and variable/field declaration, inside a struct scope [https://godbolt.org/g/Rh94Go]

struct foo {
   struct bar {
 int x;

agrif

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