Skip to content

Instantly share code, notes, and snippets.

View dannypsnl's full-sized avatar

Lîm Tsú-thuàn dannypsnl

346 followers · 150 following
View GitHub Profile
@dannypsnl
dannypsnl / EasierIndices.agda
Created September 29, 2025 18:49 — forked from yangzhixuan/EasierIndices.agda
Making working with de Brujin indices easier
{-
This file demonstrates a technique for making working with de Bruijn-indexed
terms easier that I learnt from the paper /The Linearity Monad/ by Jennifer
Paykin and Steve Zdancewic. After defining well-typed terms `Γ ⊢ τ` using de Bruijn
indices, we define an auxiliary function `lam` that takes in the variable term explicitly:
> lam : {V : Type} {Γ : Cxt V} {τ σ : Ty V}
> → (({Δ : Cxt V} → {{IsExt Δ (Γ , τ)}} → Δ ⊢ τ)
> → (Γ , τ) ⊢ σ)
> → Γ ⊢ τ ⇒ σ
@dannypsnl
dannypsnl / tuple.agda
Created March 23, 2024 08:47 — forked from bobatkey/tuple.agda
"A Quick Introduction to Denotational Semantics using Agda" notes for talk given at TUPLE 2024 (https://typesig.comp-soc.com/tuple/)
{-# OPTIONS --postfix-projections #-}
module tuple where
------------------------------------------------------------------------------
--
@dannypsnl
dannypsnl / NbEUnitEta.hs
Created October 24, 2023 15:13 — forked from AndrasKovacs/NbEUnitEta.hs
{-# language
BlockArguments
, ImplicitParams
, LambdaCase
, OverloadedStrings
, PatternSynonyms
, Strict
, UnicodeSyntax
#-}
{-# options_ghc -Wincomplete-patterns -Wunused-imports #-}
@dannypsnl
dannypsnl / pcomb.ml
Created August 7, 2023 15:29 — forked from neel-krishnaswami/pcomb.ml
A linear-time parser combinator library in Ocaml
module C : sig
type t
val empty : t
val one : char -> t
val union : t -> t -> t
val inter : t -> t -> t
val top : t
val mem : char -> t -> bool
val make : (char -> bool) -> t
val equal : t -> t -> bool
@dannypsnl
dannypsnl / natmod.agda
Created July 19, 2023 06:33 — forked from Trebor-Huang/natmod.agda
Free natural model as an HIIT
{-# OPTIONS --cubical #-}
module natmod where
open import Cubical.Foundations.Prelude
data Ctx : Type
data _⊢_ : Ctx → Ctx → Type
data Ty : Ctx → Type
data Tm : Ctx → Type
-- This is halfway between EAT and GAT.
-- GAT is hard! Why is EAT so easy?
@dannypsnl
dannypsnl / SPropSketch.hs
Created June 15, 2022 05:34 — forked from atennapel/SPropSketch.hs
SProp sketch
{-# LANGUAGE PatternSynonyms #-}
type Ix = Int
type Lvl = Int
type ULvl = Int
data Sort = Type ULvl | Prop
deriving (Show, Eq)
data SortType = SType | SProp
@dannypsnl
dannypsnl / octal_x86.txt
Created February 18, 2022 15:45 — forked from seanjensengrey/octal_x86.txt
x86 is an octal machine
# source:http://reocities.com/SiliconValley/heights/7052/opcode.txt
From: [email protected] (Mark Hopkins)
Newsgroups: alt.lang.asm
Subject: A Summary of the 80486 Opcodes and Instructions
(1) The 80x86 is an Octal Machine
This is a follow-up and revision of an article posted in alt.lang.asm on
7-5-92 concerning the 80x86 instruction encoding.
The only proper way to understand 80x86 coding is to realize that ALL 80x86
@dannypsnl
dannypsnl / macro-expanders.rkt
Created April 8, 2021 12:01 — forked from wilbowma/macro-expanders.rkt
#lang racket
(require cpsc411/compiler-lib)
(module+ a
;; Compiler style
(define (expand e)
(define (expand-expr e)
(match e
[`(and ,e1 ,e2)
@dannypsnl
dannypsnl / 0-env.rkt
Created February 18, 2021 13:07 — forked from shhyou/0-env.rkt
Compilation-time Environment
;; Exporting free identifier table operations that close over a global map
#lang racket/base
(require racket/list
syntax/id-table)
(provide env-ref env-has-id? env-add!)
(define id-table (make-free-id-table))
@dannypsnl
dannypsnl / PrettyParseError.hs
Created October 12, 2020 04:41 — forked from lynn/PrettyParseError.hs
Pretty ParseErrors for Text.Parsec
module PrettyParseError (
prettyParseError,
PrettyParseErrorOptions(PrettyParseErrorOptions),
prettyParseErrorDefaults
) where
import Data.List (intercalate, nub)
import Text.Parsec
import Text.Parsec.Error
import Text.Parsec.Pos