Skip to content

Instantly share code, notes, and snippets.

View pedrominicz's full-sized avatar

Pedro Minicz pedrominicz

View GitHub Profile
@pedrominicz
pedrominicz / Eval.hs
Created June 2, 2023 16:55
Crégut's strongly reducing Krivine abstract machine
{-# LANGUAGE PatternSynonyms #-}
module Eval (eval) where
data Expr
= Var {-# UNPACK #-} !Int
| Lam Expr
| App Expr Expr
type Level = Int
@pedrominicz
pedrominicz / main.c
Created June 1, 2023 20:20
Create an OpenGL context using Xlib and EGL
#include <stdio.h>
#include <stdlib.h>
#include <EGL/egl.h>
#include <GL/gl.h>
#include <X11/Xlib.h>
static struct {
Display* display;
Window root_window;
@pedrominicz
pedrominicz / merge.sh
Created May 26, 2023 18:54
Merge completely different Git repositories
#!/usr/bin/env bash
# https://stackoverflow.com/questions/1425892/how-do-you-merge-two-git-repositories
# https://stackoverflow.com/questions/2949738/git-merge-different-repositories
# https://git-scm.com/docs/git-filter-branch
# https://gist.github.com/msrose/2feacb303035d11d2d05
set -e
repos=(comp fun karen kvm learn logic m8080 mios mm study sugar tt)
@pedrominicz
pedrominicz / STLC.hs
Last active May 9, 2023 12:35
Type-check STLC into a GADT
{-# LANGUAGE BlockArguments, DataKinds, LambdaCase, MonoLocalBinds #-}
module STLC where
-- https://gist.github.com/pedrominicz/656cbe1a8309af8ef3226b40093bf409
-- https://github.com/goldfirere/glambda/blob/master/src/Language/Glambda/Check.hs
-- https://github.com/goldfirere/glambda/blob/master/src/Language/Glambda/Type.hs
-- https://stackoverflow.com/questions/11104536/how-to-parse-strings-to-syntax-tree-using-gadts
import Data.Type.Equality
@pedrominicz
pedrominicz / Main.x
Last active March 10, 2023 19:16
Alex: indentation-sensitive lexer
{
module Main (main) where
import Control.Applicative
import Control.Monad.State
import Data.Foldable
import Data.Maybe
import Data.Word
import System.Exit
@pedrominicz
pedrominicz / config.h
Last active April 9, 2023 14:56
dmenu config
/* See LICENSE file for copyright and license details. */
/* Default settings; can be overriden by command line. */
static int topbar = 1; /* -b option; if 0, dmenu appears at bottom */
/* -fn option overrides fonts[0]; default X11 font or font set */
static const char *fonts[] = {
"Source Code Pro:style=Bold:pixelsize=16:antialias=true:autohint=true"
};
static const char *prompt = NULL; /* -p option; prompt to the left of input field */
static const char *colors[SchemeLast][2] = {
@pedrominicz
pedrominicz / ANF.hs
Last active November 24, 2022 22:54
A-normalization (administrative normal form, ANF)
module ANF where
-- https://www.researchgate.net/publication/2392886_The_Essence_of_Compiling_with_Continuations
-- https://matt.might.net/articles/a-normalization/
-- https://gist.github.com/siraben/447c419508b460afc99a232d5df8063f
import Control.Monad.State
type Name = String
@pedrominicz
pedrominicz / gnome-terminal.md
Created August 12, 2022 13:28
Gnome terminal config with fallback fonts

How to use this config

Because the people behind Gnome are geniuses, they decided to the end the long tradition of having config files somewhere in $HOME/.config and instead store settings in "some binary file optimized for quick reading" that is located "somewhere".

Thanks, loading small plain text config files was terrible a bottleneck. I am glad the dozen custom settings I have can now load blazingly fast. Parsing simple plain text config files is a very computationally intensive process. Also, I am so glad I have no idea where this binary file is located, I always felt anxious knowing my config files where ominously sitting somewhere in $HOME/.config, watching my every move.

Sarcasm aside, there is a way of interacting with said binary file as if it where a plain text config file using dconf dump and dconf load.

$ dconf load /org/gnome/terminal/ <<EOF
@pedrominicz
pedrominicz / ipl.lean
Last active August 12, 2022 11:52
The admissibility of structural rules for the negative fragment of intuitionistic propositional logic
import tactic.basic
-- Lean version 3.45.0
@[derive decidable_eq] inductive prop : Type
| and : prop → prop → prop
| true : prop
| impl : prop → prop → prop
| other : ℕ → prop
@pedrominicz
pedrominicz / sk_boltzmann.pl
Last active August 9, 2022 11:57
Randomly generate typable SK-combinator calculus terms using Boltzmann samplers
:- ensure_loaded(library(apply)).
:- ensure_loaded(library(random)).
:- set_prolog_flag(optimise, true).
:- set_prolog_flag(optimise_unify, true).
% Randomly generate typable SK-combinator calculus terms using Boltzmann
% samplers.
%
% Based on the paper Random generation of closed simply-typed λ-terms: a