文宇祥 hackwaly

This is the predecessor of Mazeppa.

Supercompilation is a deep program transformation technique due to V. F. Turchin, a prominent computer scientist, cybernetician, physicist, and Soviet dissident. He described the concept as follows [^supercompiler-concept]:

A supercompiler is a program transformer of a certain type. The usual way of thinking about program transformation is in terms of some set of rules which preserve the functional meaning of the program, and a step-by-step application of these rules to the initial program. ... The concept of a supercompiler is a product of cybernetic thinking. A program is seen as a machine. To make sense of it, one must observe its operation. So a supercompiler does not transform the program by steps; it controls and observes (SUPERvises) the running of the machine that is represented by th

A pattern for using GADTs to subset cases

Consider the following straightforward mutable queue implementation using two stacks:

type 'a adt_queue = {
  mutable head : 'a head;
  mutable tail : 'a tail;
}

	(* 这是我（预期，亦或是已经）在 ∞-type càfe summer school 上做的 talk，

	"从零教你手把手实现一个 MLTT 类型检查器"

	的内容稿。本 talk 计划以现场边讲解边手写代码的方式实现，
	所以虽然这份内容稿会尽量尝试还原 talk 的思路和逻辑，
	它的内容可能会与实际的 talk 有出入，建议有条件的人直接去听 talk 本身 *)

	(* 本次 talk 将会使用 OCaml 来实现一个 MLTT 类型检查器。
	你可能不会写 OCaml，但这没有关系。本次 talk 只会使用以下的功能：

	// Define the grammar
	const grammar = {
	nonTerminals: ['S', 'A'],
	terminals: ['a', 'b'],
	productions: [
	{ left: 'S', right: ['A', 'a'] },
	{ left: 'S', right: ['b'] },
	{ left: 'A', right: ['a', 'A'] },
	{ left: 'A', right: [] }
	]

	(menhir
	(modules parser))

	(ocamllex lexer)

	(executable
	(name ex))

	#!/usr/bin/env python3
	import re, string
	START_SYMBOL = '<start>'
	RE_NONTERMINAL = re.compile('(<[^<> ]*>)')
	EPSILON = ''

	def fixpoint(f):
	def helper(arg):
	while True:
	sarg = str(arg)

	// Copied from typescript playground - https://www.typescriptlang.org/play/

	class Vector {

	constructor(public x: number, public y: number, public z: number) { }

	static times(k: number, v: Vector) {
	return new Vector(k * v.x, k * v.y, k * v.z);
	}

	// This code demonstrates a simplified "stackification" algorithm to turn
	// instructions in a basic block back into a tree. This is useful when
	// generating WebAssembly code from assembly instructions in SSA form.
	//
	// It's the algorithm used by LLVM's WebAssembly backend, viewable here:
	// https://github.com/llvm-mirror/llvm/blob/master/lib/Target/WebAssembly/WebAssemblyRegStackify.cpp

	type InsKind =
	'Add' \|
	'LocalSet' \|

	import zipfile
	import xxtea
	import re
	import os

	# setXXTEAKeyAndSign

	apk = zipfile.ZipFile("xxxx.apk", "r")

	probe_file = []

	import struct

	_DELTA = 0x9E3779B9

	def _long2str(v, w):
	n = (len(v) - 1) << 2
	if w:
	m = v[-1]
	if (m < n - 3) or (m > n): return ''
	n = m