Skip to content

Instantly share code, notes, and snippets.

@aspiwack
aspiwack / Cdcl.hs
Last active September 28, 2023 06:42
Functional CDCL
module Cdcl where
import Data.Foldable
import Data.Maybe
import Data.Monoid
type Atom = Int
type Literal = (Bool, Atom)
@aspiwack
aspiwack / catlist.ml
Created June 17, 2022 14:55
An implementation of “programmed laziness” for list concatenation
module CatList : sig
(** “Lazy” lists with O(1) concatenation. *)
type +'a t
type (+'a, +'l) view =
| Nil
| Cons of 'a * 'l
val view : 'a t -> ('a, 'a t) view
@aspiwack
aspiwack / pipewire.org
Created May 9, 2021 15:52
Notes on Pipewire on Ubuntu in 2021-05

Replace Pulseaudio

Ubuntu 21.04 comes with Pipewire pre-installed. A pipewire service is running, but it’s doesn’t handle audio by default. For this you need to install a pipewire-pulse service. The (preinstalled) pipewire package provides such a service as documentation. First let’s copy it in Systemd’s space.

$ cp /usr/share/doc/pipewire/examples/systemd/user/pipewire-pulse.* /usr/lib/systemd/user/
@aspiwack
aspiwack / lhs2tex-mode.el
Created November 19, 2020 13:08
An Emacs configuration to colour Haskell code blocks in lhs2tex
;; I wrote a bit of Emacs configuration (which can be added to your
;; init.el) so that an lhs2tex file can be syntax-highlighted as a
;; Latex file but the Haskell code is highlighted as Haskell code. In
;; fact it's a little more than this, as the code blocks are
;; interpreted with the haskell-mode, so you can use your haskell
;; commands there.
;;
;; I don't recommend opening all `.lhs' file in this mode, as they
;; don't need to be Latex files. Literate Haskell is really agnostic
;; about its surrounding language.

Keybase proof

I hereby claim:

  • I am aspiwack on github.
  • I am aspiwack (https://keybase.io/aspiwack) on keybase.
  • I have a public key ASAdUTbPKE_sXn1PUR6IItRsYY6oaQki2LSvqSdZsCkntgo

To claim this, I am signing this object:

@aspiwack
aspiwack / stg.ml
Created December 12, 2016 07:59
A small STG-like lazy abstract machine
(** A small STG-like lazy abstract machine. What I take from the STG
is that constructors are responsible for choosing a branch in a
pattern-matching (the T in STG) and for updating themselves (by
pushing an update frame). Apart from that it's not very different
from a simple KAM. Note that the current implementation in GHC is
not actually tagless anymore, as it proved to be slower than a
tagged mechanism. But since it's a simpler design, (and the
difference doesn't matter much unless actual machine code is
emitted).
@aspiwack
aspiwack / .merlin
Last active October 21, 2020 20:11
Heap: benchmarking pairing heaps vs braun trees
PKG core_bench
PKG qcheck
B _build
@aspiwack
aspiwack / wem.coq
Created January 2, 2016 20:49
A proof of ∀ A, A∨¬A explained with continuation
(** To give a direct proof of the constructive result that [forall
A:Prop, ~~(A\/~A)], it is useful to see [~A] as meaning a
"continuation of [A]". That is, [~A] is a computation that takes an
[A] and "returns".*)
(** Here is a first proof by forward chaining. *)
Lemma Proof₁ : forall A:Prop, ~~(A\/~A).
Proof.
intros A k₀.
(** We have [k₀:~(A\/~A)]. That is [k₀] is a continuation of either
@aspiwack
aspiwack / Diff.scala
Created September 22, 2015 15:33
Simple, naïve, generic diff implementation
package util
import scala.reflect.ClassTag
sealed abstract class Diffed[+A]
final case class Unchanged[+A](x: A) extends Diffed[A] {
override def toString: String = "Unchanged(" + x + ")"
}
final case class Changed[+A](x: A) extends Diffed[A] {
override def toString: String = "Changed(" + x + ")"
@aspiwack
aspiwack / BoundedHeightDomain.coq
Created July 30, 2015 16:50
Mostly for my own benefit: some results about bounded height domains. Double-checking [calculations for an article](https://github.com/aspiwack/topocircuit)
Require Coq.Setoids.Setoid.
Require Import Coq.Classes.RelationClasses.
Require Import Coq.Classes.Morphisms.
Require Import Coq.micromega.Psatz.
(** Chains of finite length *)
Definition Chain {A} (R:A->A->Prop) (n:nat) : Type :=
{ c:{ k | k <= n } -> A |
forall k₁ k₂, proj1_sig k₁ <= proj1_sig k₂ -> R (c k₁) (c k₂) }