Lîm Tsú-thuàn dannypsnl

Grope

A grope is a set $G$ together with a binary operation $\circ$, in which the identity

$$ x \circ (y \circ x) = y $$

is satisfied for all $x, y \in G$.

	#lang racket
	(require (for-syntax syntax/parse))
	(require data/queue)
	(require graphviz)

	(struct e-class (e-nodes))
	(struct e-graph (e-classes) #:transparent)
	#\|
	The rewriter is a function that takes
	1. a callback (to add result into same e-class), and

	#lang racket

	(define (split-list lst n)
	(for/list ([i (in-range 0 (length lst) n)])
	(take (drop lst i) (min n (- (length lst) i)))))

	(define P (make-parallel-thread-pool (processor-count)))

	(define JOBS (split-list (range 1 10000000) 100000))

	{-
	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 Δ (Γ , τ)}} → Δ ⊢ τ)
	> → (Γ , τ) ⊢ σ)
	> → Γ ⊢ τ ⇒ σ

	#lang racket
	(require (for-syntax syntax/parse))

	(define (reify-name n)
	(string->symbol
	(string-append "_" (number->string n))))
	(struct fresh (value count)
	#:methods gen:custom-write
	[(define (write-proc self out mode)
	(if (fresh-value self)

	#lang racket
	(require (for-syntax syntax/parse))

	(define-syntax (math stx)
	(syntax-parse stx
	#:datum-literals (+ *)
	[(_ (o ...) op o* ...)
	#'(let ([k (math o ...)])
	(math k op o* ...))]
	[(_ (o ...)) #'(math o ...)]