pedrominicz

{-# LANGUAGE PatternSynonyms #-}

module Eval (eval) where

data Expr
  = Var {-# UNPACK #-} !Int
  | Lam Expr
  | App Expr Expr

type Level = Int

pedrominicz

#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

#!/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

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

{
module Main (main) where

import Control.Applicative
import Control.Monad.State
import Data.Foldable
import Data.Maybe
import Data.Word
import System.Exit

pedrominicz

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

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

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

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

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