索引

• 概览
• 设计
• 抽象机器
• 数据表示
• 编译、链接和运行
• 垃圾收集
• 其他
• Js_of_ocaml和Emscripten实现在线编译运行

代码

编译器的设计和实现大量参考了 @Zinc 和Caml Light 0.75，因此取名Caml Featherweight了……实现方面更接近于 @Zinc ，Caml Light有些晦涩复杂的地方我换成自己乱想的实现了。

tl;dr的话可以直接读源码：https://github.com/MaskRay/CamlFeatherweight

Read More

抽象机器

抽象机器(abstract machine)一步一步执行程序，但比起具体的机器(如x86)省略了大量的硬件细节。与抽象机器经常混用的一个概念是虚拟机(virtual machine)。但virtual machine这个词被广泛用于操作系统的各层抽象中，因此报告中我们用“抽象机器”这个词以与这些概念相区分。

@Diehl00abstractmachines对抽象机器做了分类。

Strict functional language的抽象机器

• SECD machine(1964) call-by-value
• Functional Abstract Machine(1983)是一个扩展、优化的SECD
• Zinc Abstrace Machine(1990)可以看作是Krivine machine的call-by-value版本。

Lazy functional language的抽象机器

• G-machine(1984)
• Krivine machine(1985)
• Three Instruction Machine(1986)
• Spineless-Tagless G-machine(1989)，用于Glasgow Haskell Compiler

Krivine machine

采用de Bruijn index表示的\(\lambda\)-calculus的项形式如下：

\[M\;::=\; n \;|\; (M N) \;|\; \lambda M\]

Krivine machine仅有三条指令：Access、Push和Grab，把call-by-name的\(\lambda\)-calculus规约为weak head normal form，它的翻译方案如下：

\[\begin{aligned} \llbracket n\rrbracket &=& \text{Access}(n) \\ \llbracket (M N) \rrbracket &=& \text{Push}(\llbracket N\rrbracket); \llbracket M\rrbracket \\ \llbracket \lambda M \rrbracket &=& \text{Grab}; \llbracket M\rrbracket \\\end{aligned}\]

机器有一个代码指针、环境(一个闭包列表)、栈(闭包列表)，状态转移方案如下：

Three Instruction Machine

@Implementing是描述Three Instruction Machine (TIM)的一个很好的材料。我们据此实现了一个简单lazy functional language的编译器。TIM是spineless的抽象机器，有三条主要的指令：Take、Push和Enter，因此被称为Three Instruction Machine，可以实现pure \(\lambda\)-calculus的call-by-name计算。每条指令其实还有多种地址模式。为了实现算术操作等更多需求，还需要更多的指令。@Notes-TIM提供了更多的描述。我们对TIM的实验并未集成到项目中。

Logic programming language的抽象机器

常用Warren Abstract Machine及其变体。

Zinc抽象机器

Caml Light采用了执行方式是编译到Zinc抽象机器。

类似于Krivine machine，Zinc有代码指针和环境。Zinc不仅要处理闭包，还要处理其他的值类型，因而引入了一个累加器存放临时结果。Krivine machine中的栈被拆分成两个栈，参数栈和返回栈。如果不作拆分，翻译方案中将会多出一些交换栈顶元素的操作，会带来性能损失。

处于tail call位置的表达式指的是计算完当前表达式后就会执行Return，这样的表达式可能会有优化的翻译方案。下面用\(C\)表示一般的翻译方案，\(T\)表示处于tail call位置的表达式的翻译方案。

访问局部变量

\(n\)为de Bruijn index，翻译方案如下：

\[T\llbracket n\rrbracket =C\llbracket n\rrbracket = \text{Access}(n)\]

lllll|lllll Code & Acc & Env & Arg stack & Ret stack
\(\text{Access}(n);c\) & a & \(e=v_0\cdots v_n\cdots\) & \(s\) & \(r\)
\(c\) & \(v_n\) & \(e\) & \(s\) & \(r\)

应用和\(\lambda\)抽象

先来看一下Zinc的前驱CAM是如何翻译函数应用的：

\[\begin{aligned} C\llbracket n\rrbracket &=& \text{Access}(n) \\ C\llbracket \lambda M\rrbracket &=& \text{Closure}(C\llbracket M\rrbracket;\text{Return}) \\ C\llbracket M\; N\rrbracket &=& C\llbracket M\rrbracket;C\llbracket N\rrbracket;\text{Apply} \\\end{aligned}\]

对于一个\(n\)参数的函数应用，用curry的观点看就是有\(n\)次单参数的函数应用，将会产生\(n-1\)个临时闭包。

Zinc做了一个改进，把所有参数从右到左求值并压入参数栈，把函数放在累加器中，再使用Apply指令应用到全部\(n\)个参数上。考虑如下代码：

1
2
3
4

let id x = x in
let f x = id in
let g f x = x in
g (f 3) 4

4压入参数栈后对f 3求值，3压栈后应用f，此时栈上的元素是3和4，但提供给f的参数只有一个。因此我们需要一种机制让f知道它的参数只有一个。一种做法是把参数栈的元素分割开，区分不同函数应用的参数。Zinc采取的做法是使用Pushmark指令，在参数栈上压入记号\(\epsilon\)。

再考虑一个情况，执行Return时参数栈顶不一定是\(\epsilon\)，可能是其他值，那是和partial application相对的情况，即函数应用结果是新函数，新函数要作用在余下的参数上。此时累加器是一个函数，需要把它应用到余下的参数上。

\[C\llbracket M \; N_1 \; N_2 \cdots N_k\rrbracket = \text{Pushmark};C\llbracket N_k\rrbracket;\text{Push};\cdots;C\llbracket N_1\rrbracket;\text{Push};C\llbracket M\rrbracket;\text{Apply}\]

\(\lambda\)抽象作为first-class值，在传递时应该使用其闭包表示。它除了被传递外，唯一能做的就是应用到参数上，在函数体执行完之后需要返回到caller，因此是个tail call。因为Apply指令已经把参数栈上的第一个参数移动到环境中了，翻译\(\lambda\)抽象时可以免去这个操作。结合上述考虑，可以采用如下翻译方案：

\[C\llbracket \lambda M\rrbracket = \text{Cur}(T\llbracket M\rrbracket;\text{Return})\]

Cur的作用是构建一个闭包。

Tail call翻译方案的优化

再考虑如何优化处于tail call位置的应用和\(\lambda\)抽象的翻译方案。

Tail call位置的函数应用允许接受过量的参数，此时可看作是接受原本需要数目的参数后返回了一个新函数，新函数应用在了余下的参数上。因此我们不需要用\(\epsilon\)分割参数。翻译\(\lambda\)抽象时，也不同生成一个闭包等待之后被应用到余下的参数上，可以直接从参数栈上取一个参数移动到环境中，再执行函数体；如果取到\(\epsilon\)，就说明参数不够，此时再生成闭包。

\[\begin{aligned} T\llbracket \lambda M\rrbracket &=& \text{Grab};T\llbracket M\rrbracket \\ T\llbracket M \; N_1 \; N_2 \cdots N_k\rrbracket &=& C\llbracket N_k\rrbracket;\text{Push};\cdots;C\llbracket N_1\rrbracket;\text{Push};C\llbracket M\rrbracket;\text{Termapply} \\\end{aligned}\]

let绑定

\(\text{let}\; x=N\;\text{in}\; M\)可以变换为\((\lambda M)\; N\)以消除let，但这么做会引入闭包，更好的方法是直接计算\(N\)再放到环境中。若有and引入了多个绑定，只要依次放到环境中即可。对于非tail call的情况，let表达式计算完后应该把环境中引入的绑定清除，用Endlet指令实现。

\[\begin{aligned} C\llbracket \text{let}\; x_1=N_1\;\text{and}\ldots\text{and}\; x_k=N_k\; \text{in}\; M\rrbracket &=& C\llbracket N_1\rrbracket;\text{Let};\ldots C\llbracket N_k\rrbracket;\text{Let};C\llbracket M\rrbracket;\text{Endlet k} \\ T\llbracket \text{let}\; x_1=N_1\;\text{and}\ldots\text{and}\; x_k=N_k\; \text{in}\; M\rrbracket &=& C\llbracket N_1\rrbracket;\text{Let};\ldots C\llbracket N_k\rrbracket;\text{Let};C\llbracket M\rrbracket \\ C\llbracket \text{let rec}\; x_1=N_1\;\text{and}\ldots\text{and}\; x_k=N_k\; \text{in}\; M\rrbracket &=& \text{Dummy}\; k;C\llbracket N_1\rrbracket;\text{Update}\; k-1;\ldots \\ & & C\llbracket N_k\rrbracket;\text{Update}\; 0;C\llbracket M\rrbracket;\text{Endlet k} \\ T\llbracket \text{let rec}\; x_1=N_1\;\text{and}\ldots\text{and}\; x_k=N_k\; \text{in}\; M\rrbracket &=& \text{Dummy}\; k;C\llbracket N_1\rrbracket;\text{Update}\; k-1;\ldots \\ & & C\llbracket N_k\rrbracket;\text{Update}\; 0;C\llbracket M\rrbracket \\\end{aligned}\]

指令集

下面解释一些主要指令的含义：

• ACCESS \(n\) 获取环境中第\(n\)个槽位，放在累加器中。

• CONSTINT8 \(n\) 把int8_t类型的整数\(n\)放在累加器中。

• GETGLOBAL \(s\) 把槽位为\(s\)的全局值放在累加器中。

• SETGLOBAL \(s\) 把累加器中的值存入槽位\(s\)。

• APPLY 函数应用，根据返回地址和当前环境构建闭包压入返回栈，同时把参数栈顶弹出添加到环境中。

• POP 弹出参数栈。

• PUSH 把累加器的值压入参数栈。

• PUSHMARK 把\(\epsilon\)压入参数栈。

• CUR \(l\)，用标签\(l\)指向的代码和当前环境构建闭包，放入累加器中。

• GRAB 若参数栈顶为值，则弹出添加到环境中，否则构建闭包放入累加器并返回。

• TERMAPPLY 函数应用，同时把参数栈顶弹出添加到环境中。

• DUMMY \(n\) 在环境中压入\(n\)个任意值(内容无关紧要)。

• ENDLET \(n\) 在环境中弹出\(n\)个元素。

• LET 把累加器压入环境。

• UPDATE \(n\) 用累加器更新环境的第\(n\)个值。

• GETFIELD \(n\) 累加器更新为其表示的block的第\(n\)个域。

• MAKEBLOCK \(tag,size\) 根据tag和size域创建block。

• SETFIELD 累加器表示的block的第\(n\)个域更新为参数栈中弹出的元素。

• BRANCH \(l\) 跳转。

• SWITCH 根据累加器表示的block的tag和跳转表跳转。

• CCALL1 累加器标示解释器中定义的原语函数，执行该函数。

• RAISE 抛出异常。

• RETURN 若参数栈顶为\(\epsilon\)则弹出并返回，否则执行累加器中的闭包。

数据表示

不同类型语言的实现使用了截然不同的数据表示方式。

对于Scheme这样的动态类型语言的实现，数据在运行时需要标志以区分不同类型，所有类型的数据通常需要适配某一种通用的格式，通常是一个字的指针，指向一个block，block里存储具体的数据，这种存储方式称为boxed，记录类型、数组等都是boxed类型。对于双精度浮点数，因为占64位，而机器字长不足以同时表示指针和所有可能的浮点数，因此浮点数也必须采用boxed类型。

因为整数使用的普遍性及性能考虑，整数通常不存储在block中并用指针标识，而是用左移一位且最低位置1的方式表示。因为指针通常要满足一定的对齐条件，最低位为0，这种表示方法不会引起歧义。

对于C、Pascal这样的monomorphic静态类型语言的实现，因为无需进行运行时类型测试，各数据类型不必有统一的格式，因此往往可以有不同的大小。单精度、双精度浮点数可以采取格子的unboxed表示，可以有各种大小的整数类型，比如int8_t、int64_t等。不同类型的函数也可以采取不同的调用约定，比如参数为浮点数或整数时，很多架构下在调用函数时会把参数放在不同的寄存器中。

引入parametric polymorphism后，问题变得复杂，有三类解决方案：

• 限制polymorphism的形式，比如Modula中规定抽象类型必须是指针类型，Java中不允许unboxed类型如int转换为Object。这种方式的缺点是不够直观，并且对语言表现力有较大的牺牲。

• 为不同类型生成多份代码。C++模板通常采取这种方式，为不同类型生成不同的代码。缺点是代码大小膨胀，链接复杂性增加，可能需要链接代码生成等。

• 采用Scheme式样的处理方式。普遍采用boxed类型。缺点是性能损失。

这方面有一些研究成果，比如采取C和Scheme结合的方法、在polymorphic代码中引入类型大小信息等。

Block和整数的区分

我们采取boxed类型的方式，多数类型如元组、数组、float等，它们的实际内容都用堆上分配的一块内存表示，使用指针来标识它们，参数传递和变量存储时都使用表示它们的指针。整数则用低位为1的值表示。

整数

一个整数\(i\)表示为\(2i+1\)，在一个字长为32位的机器上(下面都假定采用32位机)，能表示的int范围不再是\([-2^{31},2^{31})\)，丢失了一位变为\([-2^{30},2^{30})\)。相应地，整数运算需要做一些修改，比如取反实现为\(2-x\)、加法实现为\(x+y-1\)等。

Block

一个block由记录元数据的首部和实际存储的数据两部分组成。字符串、数组和闭包的格式有些特殊，其他block采用统一的格式，元数据占两个字，第一个字记录tag、block的大小和用于垃圾收集的字段color。第二个字是一个XOR链表指针，堆上所有分配的block都串在一个XOR链表里。

bits  31  20 19    8 7   0   31                 0
     +------+-------+-----+ +--------------------+
     | size | color | tag | | xor of prev & next |
     +------+-------+-----+ +--------------------+

Tag占据一个字节，标识了该block的类型，可用于区分内置类型float(表示为一个双精度浮点数)、string、array和sum类型采用了哪一个构造器。注意经过类型检查后，我们不需要区分不同代数数据类型，只需要标识特定代数数据类型采用了哪一个构造器。

若tag值大于或等于No_scan_tag(251)，就表示这个block存储的数据都是不透明的字节信息，不应该把它们解释为指向其他block的指针。一个代数数据类型的各个构造器，分别用tag值0、1、2等表示。unit类型的构造器()的tag值为1，bool类型的构造器false的tag值为0，true的tag值为1。

size域代表block的指针域数目，对于true这类不包含子域的值，其size为0。

color域用于垃圾收集，对于我们采用的Schorr-Waite graph marking算法，color域需要\(\max\lceil\log_2{n+1}\rceil\)个bit，其中\(n\)是该节点的指针域数目。如果color域和size域使用相同的长度，如我们的实现中所选取的，size域最大可以为\(2^{12}-1=4095\)。元组很难有超过4095项，一个类型的构造器数目也很难超过4095，因此这种方式对于这些类型都是合适的。但是对于字符串长度和数组大小，4095还是相对较小，因此这两个类型要采取特殊的表示方式，把color域的bit也作为size使用，但这样就需要其他地方存储color域，我们选择了在XOR指针域后再加一个字编码color。

下表整理了一些常见类型值的表示方式：

|l|l| 值 & 表示
3 & 3*2+1=7
’a’ & 97*2+1=195
true & 指向一个tag为1，size为0的块的指针
false & 指向一个tag为0，size为0的块的指针
[] & 指向一个tag为0，size为0的块的指针
3::[] & 指向一个tag为1，size为2的块的指针，该块的两个域分别为2*3+1=7和一个表示[]的块

字符串的表示

字符串的block的tag大于No_scan_tag，但元数据存储格式略有区别。因为字符串不包含指向其他节点的指针域，采用Schorr-Waite graph marking算法垃圾收集时只需要区分是否被标记过，color域被缩短为只有一个bit，其余bit都被size域占用，size域共23个bit，最多可以表示长度为\(2^{23}-1\)的字符串。

bits  31  9  8     8 7   0   31                 0
     +------+-----+-+-----+ +--------------------+
     | size | color | tag | | xor of prev & next |
     +------+-------+-----+ +--------------------+

数组的表示

数组的block的tag大于No_scan_tag。原来第一个字的color域全部都被size域占用，因此最大长度是\(2^{24}-1\)，color域被移动到XOR链表指针域的下一个字。

bits  31           8 7   0   31                 0   31                 0
     +--------------+-----+ +--------------------+ +--------------------+
     |     size     | tag | | xor of prev & next | |        color       |
     +--------------+-----+ +--------------------+ +--------------------+

闭包的表示

闭包的block的tag小于No_scan_tag，size域固定为2，两个域分别为代码指针和表示环境的闭包。

环境的表示

为了一致性，环境也用block表示，但因为它不会作为值传递，tag值无关紧要，size域的值就是环境中存储的变量数。

Block中的XOR指针域

使用mark-sweep方式的垃圾收集器需要能追踪分配过的堆对象，我们在首部的XOR指针域中维护了所有分配对象的双链表。对于简单的收集所有对象并标记扫除的垃圾收集器，单链表足矣。但考虑到拓展性，我们采用了双链表，以方便未来可能需要支持的操作。因为两个指针域空间开销有点大，我们使用了XOR链表，即每个节点的指针域为其前驱和后继节点地址的XOR。根据XOR链表头或尾节点的地址即可遍历整个链表。

编译、链接和运行

流程概览

整个编译、链接和运行过程拆分为若干阶段：

• 解析。包括词法分析和语法分析，使用工具ocamllex和menhir。

• 类型检查。检查程序是否合法，类型推导也在这一步进行。

• 把语法树翻译成一种中间表示：扩充的\(\lambda-calculus\)

• 把扩充的\(\lambda-calculus\)编译为Zinc抽象机器字节码。每个源文件会生成一个目标文件。

• 链接各目标文件得到可被运行时系统执行的字节码文件。

• 运行时系统解释执行。

下面分别介绍各个阶段。

解析

使用ocamllex进行词法分析，menhir进行语法分析得到抽象语法树。

多数yacc实现都采用了操作符优先级来解决移入/规约冲突，在实现中我们碰到一些典型问题并得以解决。

词法分析错误信息

解析逗号分割的列表

考虑表示表达式的非终结符expr，它的其中两个产生式是逗号分割的表达式和分号分割的表达式，约定逗号(COMMA)优先级高于分号(SEMI)，可以如下实现：

expr:
  | ...
  | expr_comma_list %prec below_COMMA { Pexpr_tuple($1) }
  | expr SEMI expr { Pexpr_seq($1,$3) }
  | ...

expr_comma_list:
  | expr COMMA expr_comma_list { $1 :: $3 }
  | expr COMMA expr { [$1; $3] }

其中%prec below_COMMA是指定第一条产生式的优先级，从而在栈为expr_comma_list且向前看符号为COMMA时，menhir选择移入而不是规约expr_comma_list -> expr。

但这种语法描述还有一个问题。当栈内当前为expr COMMA expr_comma_list且向前看符号为SEMI时，规约expr_comma_list -> expr和规约expr COMMA expr_comma_list -> expr的优先级均大于SEMI，因此无法确定采取哪一个规约，产生规约/规约冲突。

解决方案是用右递归重新描述expr_comma_list：

expr_comma_list:
  | expr_comma_list COMMA expr { $3 :: $1 }
  | expr COMMA expr { [$3; $1] }

在使用expr_comma_list要注意把列表反转。考虑到函数式语言中在列表头部添加元素比较容易，描述文法时通常用左递归而非右递归，但在上述情形下就不得已采用右递归。在更为复杂的OCaml的parsing/parser.mly中也能看到一些这样的例子。

解析标识符，区分构造器和变量

Caml Light的语法分析文件中把实现文件划分为用双分号分割的多个phrase，解析完一个phrase后立即进行类型检查、代码生成等工作，并导入全局的值、类型、构造器信息。在解析模式匹配的地方遇到一个标识符时，通过查询之前是否定义过该标识符的构造器来区分该标识符是构造器还是变量。Caml Light把部分变量是否定义的工作糅合到了解析阶段。

我们希望能完整解析源文件后再进行变量定义判断的工作，因此借鉴了OCaml的解析器实现，区分大小写两种标识符，大写视为构造器，小写视为变量。

在这里也能一窥语言实现的考量，了解为什么很多支持模式匹配的语言规定构造器使用大写、变量使用小写。

这里也能看到为了语言的一致性，false和true应该看作构造器，使用大写，实现中如果要摈弃Caml Light中解析阶段判断是否定义的做法，比较好的方式是在词法分析中把false和true也作为词法单元。

类型检查

解析得到抽象语法树后，进行类型检查判断程序是否合法。项目中使用Damas-Hindley-Milner类型系统的algorithm W进行类型推导。

Algorithm W中使用unification来判断两个类型是否可能相等，为此需要适配两个类型的形状。比如如果要unify函数类型int -> a和另一个类型b -> char，需要把类型变量b变为具体类型int、类型变量b变为具体类型int。

实现unification时有两种方法：

• 使用一个类型映射表，记录各个类型变量被映射为什么类型(具体类型、其他类型变量、或generic类型)

• 每个类型变量维护一个可修改的域，表示不相交的集合，类型变量可以是尚未确定与其他类型的关系(自身为一个集合)，或者被确定与某些类型相同(与它们在一个集合中)。这里的可变域表示为并查集算法的父节点。

使用可变域性能较高，因此我们的实现中也采用了这一方法。

类型的generalization

Damas-Hindley-Milner类型系统中的let-polymorphism阶段，需要把尚未和外部类型联系起来的类型变量generalize成generic类型。

原始的实现方式是遍历类型(表示为一棵树)，访问其中所有类型变量，判断是否和外部类型unify过，如果没有则generalize。http://okmij.org/ftp/ML/generalization.html中提到的Rémy’s level-based generalization采取了一种剪枝策略，也是Caml Light实现所采用的。我们的项目也实现了这一方法。另外文章中还提到了一种惰性实现，可以优化occur check，并加速整个类型推导过程的时间复杂度到近似线性。我们实现了该方法，但考虑到多数情况下类型树不会很大，occur check和遍历类型树的代价不会很大，并且惰性方法要引入额外的空间需求，以及实现的复杂性，未在项目中引入。

实例化generic类型

Caml Light在实例化generic类型时采用了一种技巧(cl75/src/compiler/types.ml)，把实例化分成两个阶段：copy_type和cleanup_type。

copy_type把原来的类型复制了一份，修改了类型树中generic类型变量的可变域，指向一个该变量的实例(不再为generic)，返回的副本与原本的类型共享那些非generic的部分。当原来的类型被复制第二遍的时候，新的副本会与第一份副本共用新生成的非generic类型变量。因此对于相同的generic类型变量，它的各个副本都会是相同的类型实例。

之后经过cleanup_type，原来的类型被还原成copy_type前的形态。

copy_type的特性在产生相关联的类型实例时很方便，比如两棵类型树共享一个generic的类型变量。那么实例化时希望得到的两个类型树实例的对应类型实例也是相同的。可以这样做：先分别对两棵树进行copy_type，再分别cleanup_type，得到的两个副本保证共用了相同的类型实例。

扩充的\(\lambda\)-calculus

ML的语法比较复杂，在编译到字节码需要进行一些简化，为此Caml Light采用了一个扩充的\(\lambda\)-calculus作为中间表示，我们也实现了类似的、但更加简化的扩充\(\lambda\)-calculus。

原始的无类型\(\lambda\)-calculus中唯一的值类型是\(\lambda\)抽象，另外也只有变量和应用两种项形式。经过de-Bruijn index的变换后，可以引入环境这一元素(若干嵌套的\(\lambda\)抽象中的值的列表)，变量指向环境中特定位置项，因此可以用一个索引值替代，由此我们就把Lvar of string换成了Lvar of int，这里之所以能做这样的变换还得感谢静态作用域。

比如在fun x -> fun y -> x中，x和y都在环境中，x可以用de Bruijn index 1代替。

在ML中，值类型还可以是像int这样的基本类型，因此我们需要一个额外的构造器Lconst of constant。原始的无类型\(\lambda\)-calculus也无法表示加法这样的运算，只能采用Church encoding。在ML这样的实际语言中需要有办法表示这些运算，以及其他很多操作如数组取元素、比较两数、根据构造器和参数创建代数数据类型等，因此我们添加了构造器Lprim of prim * lambda list，可以看作prim表示的原语函数应用在一些参数上。

抛开let-polymorphism，let可以等价变形为\(\lambda\)抽象和应用的一个简单组合(let x=... in y变换为(fun x -> y) (...))。而在类型检查通过后，如果把所有值看作是boxed类型，并且使用无类型的\(\lambda\)-calculus，那么我们可以不忽略let-polymorphism的影响。但实现为函数应用会有一定的性能开销，因此尽管不是必须有的，我们还是提供了构造器Llet of lambda list * lambda。

利用call-by-value的求值策略顺序，可以用\(\lambda\)抽象和应用实现表示顺序执行的;(x; y变换为(fun _ -> y) x)，但为了性能考虑设立了Lsequence of lambda * lambda构造器，它会先执行第一项，再执行第二项。通过使用这种方式，实现了对C中语句和表达式的统一。

模式匹配引入了更多的复杂性。当没有模式匹配时，环境中的项(函数的形式参数)只有一种引用方式，即视为一个整体引用。但涉及模式匹配后，考虑fun ((x,y) as a) ->，作为整体的参数可以用a引用，但模式匹配又引入了构成二元组a的两个成分x、y，它们也可以被函数体引用，所以该如何表示它们呢？另外代数数据类型的构造器可以有多个参数，也可以在模式匹配中出现，需要提供一种办法引用它们的参数。

就像代数数据类型的描述那样(元组可以看成是提供了语法支持的特殊代数数据类型)，参数可以看成是它们的子域，我们使用原语Pfield of int来引用某个子域。用于de Bruijn index的环境不再是简单变量的列表，列表中的每一项不仅要提供引用参数自身的方法，也要提供方法引用出现在模式匹配中的所有变量。因此我们把环境表示为一个列表的列表，每个内层列表代替的原来的简单参数，其中包含所有变量的引用方式。

项目源文件front.ml实现了抽象语法树到扩充的\(\lambda\)-calculus的翻译。很多节点的翻译很直观：

1
2
3
4
5
6
7
8
9
10

| Pexpr_apply(e,es) ->
    Lapply(go e, List.map go es)
| Pexpr_array es ->
    Lprim(Pmakeblock(0,0), List.map go es)
| Pexpr_constant c ->
    Lconst c
| Pexpr_sequence(e1,e2) ->
    Lsequence(go e1, go e2)
| Pexpr_tuple es ->
    Lprim(Pmakeblock(1,0), List.map go es)

比如代表函数应用的Pexpr_apply，代表字面量的Pexpr_constant等。元组稍复杂一些，可以看作是使用原语Pmakeblock创建了一个新的block，其各个域是元组的各个成分。

构造器较为复杂，需要判断在代数数据类型定义中该构造器是否带参数(Constr_constant或Constr_regular，以及在表达式中是否带参数，选择翻译成一个创建新block的原语，或者是个\(\lambda\)抽象：接受参数以创建block。

1
2
3
4
5
6
7
8
9
10
11
12
13

| Pexpr_constr(id,arg) ->
    let cd = find_constr_desc id in
    begin match arg with
    | None ->
        begin match cd.info.cs_kind with
        | Constr_constant ->
            Lprim(Pmakeblock cd.info.cs_tag, [])
        | _ ->
            Labstract(Lprim(Pmakeblock cd.info.cs_tag, [Lvar 0]))
        end
    | Some arg ->
        Lprim(Pmakeblock cd.info.cs_tag, [go arg])
    end

全局值

处于顶层的let会产生一个全局值(如基本类型值、函数等)，可以被之后的代码引用。用通常的静态作用域观点看，这样产生的值不在之后代码的作用域内。当然我们可以把在顶层并列放置的let绑定视为是嵌套的，但这种模型无法解决多文件全局值的引用问题，因此不可行。

解决这个问题需要引入全局值的概念，设置原语Pgetglobal of long_ident和Psetglobal of long_ident用于表示读取和写入全局值。

翻译模式匹配

模式匹配是最复杂的部分，允许匹配多个代数数据类型复合的结构，混合字面量、变量和构造器，各个匹配项还有顺序要求，因为如果多个模式都能匹配，那么根据语义应该选取最靠前的匹配项。@slpj的Chapter 5，Philip Wadler提供了详细的描述。@Zinc的5.2.4 Compiling pattern matching提供了Caml Light中的实现方法。在项目中我们又进行了进一步的简化。

对于复杂的模式匹配，比如：

1
2
3

match false, false with
| false, true -> ()
| false, false -> ()

设想一个按顺序匹配元组的各个项的扩充\(\lambda\)-calculus表示，第一个匹配项的false匹配成功后，true会匹配失败，此时应该跳转到第二个匹配项。如何实现这样的逻辑呢？

当涉及多个匹配项时，翻译器会把它们组织成Lstaticcatch(p1,Lstaticcatch(p2,Lstaticcatch(...)))，p1、p2是各模式匹配项翻译得到的代码，执行p1时，若发现后续的模式匹配失败了，就会执行Lstaticraise。其效果相当于抛出了一个异常，该异常会被嵌套它的最内层的Lstaticcatch捕获，尝试执行作为替代的第二条指令。这一机制可以看成是一个静态作用域的异常处理，因此使用了这样的名字：Lstaticcatch和Lstaticraise。

if可以看作是模式匹配的特例，即匹配true和false，但为了性能考虑，设立了Lif这一构造器。

翻译异常处理

Lcatch of lambda * lambda的第一个参数是try的代码体，如果抛出异常则把控制权交给模式匹配部分，即第二个参数。

扩充\(\lambda\)-calculus定义

lambda.ml中的定义：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15

type lambda =
  | Labstract of lambda
  | Lapply of lambda * lambda list
  | Lcatch of lambda * lambda
  | Lcond of lambda * (constant * lambda) list
  | Lconst of constant
  | Lif of lambda * lambda * lambda
  | Llet of lambda list * lambda
  | Lletrec of lambda list * lambda
  | Lprim of prim * lambda list
  | Lsequence of lambda * lambda
  | Lstaticcatch of lambda * lambda
  | Lstaticraise
  | Lswitch of int * lambda * (constr_tag * lambda) list
  | Lvar of int

扩充\(\lambda\)-calculus翻译成Zinc抽象机器的linear code

接下来把中间表示翻译成Zinc抽象机器的linear code。字节码相当于机器码，而linear code就相当于汇编代码。Linear code的定义在文件instruction.ml中：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26

type zinc_instruction =
  | Kaccess of int
  | Kapply
  | Kbranch of int
  | Kbranchif of int
  | Kbranchifnot of int
  | Kcur of int
  | Kdummy of int
  | Kendlet of int
  | Kgetglobal of long_ident
  | Kgrab
  | Klabel of int
  | Klet
  | Kmakeblock of constr_tag * int
  | Kpoptrap
  | Kprim of prim
  | Kpush
  | Kpushmark
  | Kpushtrap of int
  | Kquote of struct_constant
  | Kreturn
  | Ksetglobal of long_ident
  | Kswitch of int array
  | Ktermapply
  | Ktest of bool_test * int
  | Kupdate of int

type zinc_instruction的多数构造器都和字节码有直观的对应关系，比如构造器Kaccess of int翻译成字节码时，会额外输出一个uint8_t类型的操作数。表示的标号构造器Klabel of int不会生成字节码，但能作为一个标签供其他指令引用。

中间表示翻译成linear code的实现在文件back.ml中，采用了compile with continuation的编译方法。其中的主要函数是compile_lambda中的compile_expr : int -> lambda -> instruction list -> instruction list，第一个参数表示模式匹配失败后需要跳转到的代码，第二个参数是待编译的扩充\(\lambda\)-calculus，第三个参数代表该指令执行完后需要执行的continuation，返回Zinc指令的列表(需要包含continuation)。

很多结构的翻译是直观的：

1
2
3
4
5
6
7
8

| Lvar i ->
    Kaccess i :: cont
| Lconst c ->
    Kquote c :: cont
| Lprim(Pdummy n, []) ->
    Kdummy n::cont
| Lprim(Pgetglobal id, []) ->
    Kgetglobal id::cont

模式匹配失败后会执行Lstaticraise，翻译的方式是跳转到嵌套该代码的最靠近的Lstaticcatch。

1
2

| Lstaticraise ->
    Kbranch staticraise::cont

有部分结构比如Lif，代码执行路径可能有多条，需要引入一些分支指令。

Lswitch根据参数(必须是block)的tag值及跳转表进行跳转。

Lcatch的翻译方案是压入一个异常处理栈帧，执行try代码体时若发生异常，控制权会交给最近的异常处理栈帧，如果它匹配失败就把控制权交给外层的异常处理栈帧。若未发生异常则弹出异常处理栈帧。

全局值

扩充\(\lambda\)-calculus中对全局值的处理可以直接翻译成相应的抽象机器指令，同样需要用于处理读取和写入全局值的指令。读取和写入相同名称的指令应该访问同一个内存地址。为了性能的考虑，我们不希望在运行时维护一个名称到具体内存地址的映射表。再考虑到一个文件访问另一个文件定义的全局值，我们在生成代码后还需要一个过程把这些名字解析到合适的槽位，因此需要下一个阶段——链接。

1
2
3
4

| Lprim(Pgetglobal id, []) ->
    Kgetglobal id::cont
| Lprim(Psetglobal id, [e]) ->
    c_expr e (Ksetglobal id::cont)

Linear code翻译为字节码，生成目标文件

这一阶段的实现在文件emit.ml中。我们使用了一个简单的翻译方案。每个指令拆分为操作码和参数两部分，操作码占据一个字节，参数则有多种形式：uint8_t、int16_t、标签等。

因为标签定义和引用都是在当前源文件里局部的，生成代码时可以把这些标签引用都解析为字节码中的相对地址。

链接器

正如之前所提到的，这一过程并非必须，但基于性能的考虑需要在编译流程中引入这一阶段。读取各个源文件编译得到的目标文件(需要重定位)，梳理其中全局值定义和引用的关系，把各条Ksetglobal、Kgetglobal指令解析到正确的槽位是这一阶段的主要目标。

在我们的实现中这一部分的代码在ld.ml中，ld是传统的链接器的名字，我们借用了这一名字来贴切地表示这段代码需要完成的任务。

ld.ml使用了一个两遍扫描过程，先扫描各目标文件得到所有的全局值定义，再扫描各目标文件，解析其中的全局值定义和引用，把指令写入可执行文件中。该文件实际上还处理了原语操作。

运行时系统和字节码解释器

运行时系统和字节码解释器用C实现，在目录runtime/中。

初始化共享的size域为0的构造器

因为构造器的域不可变，且size域为0的block经常被使用，我们可以把tag值为0到255的256个block缓存起来，供所有size域为0的block共享。Caml Light的cl75/src/runtime/mlvalues.h中声明了extern header_t first_atoms[];，()、true等就用这些first_atoms元素的指针表示。我们的运行时也采用了这一技巧。

全局值初始化

字节码文件中有一些float、string常量，执行时需要一个加载过程，把这些常量分配为block供代码使用。另外还有一些Psetglobal需要引用的槽位，初始化为整数0(bit pattern是1)。

指令解码和派发

解释器的主要部分是runtime/main.c中的一个取指令并解释的循环。常规解释器实现方法是在循环里放置一个switch实现指令的解码和派发：

1
2
3
4
5
6
7
8
9
10
11

for(;;) {
  switch (*pc++) {
    case ACCESS:
      ...
      break;
    case ADDFLOAT:
      ...
      break;
    ...
  }
}

但这样做，指令一条抽象机器指令会引入至少两条CPU的跳转指令，即break引入的跳转到switch处的指令和switch跳到某一个标签处的指令。

我们可以让break实现解码下一条指令并跳转到相应标签处的功能，这样就可以节省一条跳转指令。GCC提供了computed goto特性，可以获取可以获取标签所指代码的地址(void*类型)，从而可以手工实现一个跳转表：

1
2
3
4
5
6
7
8
9
10

void *jumptable[] = {&&ACCESS, &&ADDFLOAT, ...};
goto *jumptable[*pc++];

ACCESS:
  ...
  goto *jumptable[*pc++];
ADDFLOAT:
  ...
  goto *jumptable[*pc++];
...

垃圾收集

Caml Light使用的垃圾收集算法可以参考@Sestoft94，结合了stop-and-copy和分代mark-sweep。我们的实现则使用了一个非常简单的方法，基于Schorr-Waite graph marking算法。该算法不使用栈，只需要在节点上分配极少量信息(\(\lceil\log_2{n+1}\rceil\) bits，其中\(n\)是该节点的指针域数目)。在一些资料中被称为pointer reversal。基本思想是在节点信息里维护一个域\(s\)，表示遍历过程中的访问次数，并把遍历过程中祖先节点下溯的指针翻转，再设置一个表示当前节点父节点的指针\(p\)以把祖先节点组织为一个链。

其他

项目中我们还实现了一些辅助工具。

Pretty printer

Pretty-print指的是对文本文件(特别是标记语言和程序代码)采用语法高亮、调整换行空格、调整字体等手段使之易于阅读。项目中实现了一个pretty printer，用于生成进行换行空格排版调整后的代码和调试信息。

下面只考虑进行换行空格排版调整的pretty printer。Haskell中的pretty printer主要有两大流派，其一是John Hughes设计，由Simon Peyton Jones修改的，跟随GHC一起发行，称为Hughes-PJ库；其二是Philip Wadler在The Fun of Programming中设计的pretty printer@Wadler，后由Leijen修改，添加了对齐等扩展得到的，称为Wadler-Leijen库。

@prettiest-printer提出了另一种方法，是对Wadler/Leijen的一种改良。原始的Hughes-PJ和Wadler/Leijen对于并集文档，为了注重性能，使用了贪心算法进行选择。但这样得到的文档不一定是最短的。这一方法以行为单位搜索最短表示。我对它进行了改良，使得能保证返回适应宽度的文档。

@Swierstra04提出了一种线性算法，@Swierstra09提供了该算法的不依赖lazy evaluation的版本。我实现并扩展了这种方法，引入了对齐操作。

h=5;a=let b=4;c=5 in (case 4 of <3> a -> 5;<4>->6;<4>-> case 3 of <2> A->2 * (let g = (let h = 5 in 5) + 8 in h)); h=6

收获

通过一个比较完整的字节码编译器实现，对编译器的流程有了更深入的理解，也更能体会ML/SML/OCaml语言设计的一些取舍，有些点也许未必是语言设计者的考虑因素，但确实是从文献和代码中得到的理解。

• SML库函数较少使用curry，而大量使用元组组合各个参数。因为Zinc之前的很多抽象机器实现curry时会产生大量闭包，有性能损失。
• 构造器和变量用大小写区分。这样在模式匹配时可以区分构造器和变量。
• 构造器只接受不超过一个元素，如果超过一个元素则用元组把参数组合起来，且带参数的构造器如果不跟参数单独出现是不合法的，因为它不能被视为函数。Caml Light的数据表示中接受元组参数的构造器实际上被看作\(n\)元构造器，对于A(x,y,z)，x,y,z是和A的tag在同一个block的，而不是存放一个指针域指向x,y,z形成的元组。
• Caml Light链接过程中要按依赖顺序指定各个目标文件。如果Caml Light在Pset_global定义符号前先看到了Pget_global引用，那么将会产生未定义错误。如果要支持向前引用，那么需要进行两边扫描或者为每个符号维护一个引用列表。
• Caml Light按phrase解析并进行代码生成。每一个phrase经过了解析、类型检查、添加到全局表、生成代码的完整过程，因此之前的类型定义给之后阶段的解析提供信息，语法树中可以使用一些语义更丰富的表示，比如出现构造器时可以使用其具体语义信息，而不仅仅是标识符信息。

编译、链接和运行

流程概览

整个编译、链接和运行过程拆分为若干阶段：

• 解析。包括词法分析和语法分析，使用工具ocamllex和menhir。

• 类型检查。检查程序是否合法，类型推导也在这一步进行。

• 把语法树翻译成一种中间表示：扩充的\(\lambda-calculus\)

• 把扩充的\(\lambda-calculus\)编译为Zinc抽象机器字节码。每个源文件会生成一个目标文件。

• 链接各目标文件得到可被运行时系统执行的字节码文件。

• 运行时系统解释执行。

下面分别介绍各个阶段。

解析

使用ocamllex进行词法分析，menhir进行语法分析得到抽象语法树。

多数yacc实现都采用了操作符优先级来解决移入/规约冲突，在实现中我们碰到一些典型问题并得以解决。

词法分析错误信息

解析逗号分割的列表

考虑表示表达式的非终结符expr，它的其中两个产生式是逗号分割的表达式和分号分割的表达式，约定逗号(COMMA)优先级高于分号(SEMI)，可以如下实现：

expr:
  | ...
  | expr_comma_list %prec below_COMMA { Pexpr_tuple($1) }
  | expr SEMI expr { Pexpr_seq($1,$3) }
  | ...

expr_comma_list:
  | expr COMMA expr_comma_list { $1 :: $3 }
  | expr COMMA expr { [$1; $3] }

其中%prec below_COMMA是指定第一条产生式的优先级，从而在栈为expr_comma_list且向前看符号为COMMA时，menhir选择移入而不是规约expr_comma_list -> expr。

但这种语法描述还有一个问题。当栈内当前为expr COMMA expr_comma_list且向前看符号为SEMI时，规约expr_comma_list -> expr和规约expr COMMA expr_comma_list -> expr的优先级均大于SEMI，因此无法确定采取哪一个规约，产生规约/规约冲突。

解决方案是用右递归重新描述expr_comma_list：

expr_comma_list:
  | expr_comma_list COMMA expr { $3 :: $1 }
  | expr COMMA expr { [$3; $1] }

在使用expr_comma_list要注意把列表反转。考虑到函数式语言中在列表头部添加元素比较容易，描述文法时通常用左递归而非右递归，但在上述情形下就不得已采用右递归。在更为复杂的OCaml的parsing/parser.mly中也能看到一些这样的例子。

解析标识符，区分构造器和变量

Caml Light的语法分析文件中把实现文件划分为用双分号分割的多个phrase，解析完一个phrase后立即进行类型检查、代码生成等工作，并导入全局的值、类型、构造器信息。在解析模式匹配的地方遇到一个标识符时，通过查询之前是否定义过该标识符的构造器来区分该标识符是构造器还是变量。Caml Light把部分变量是否定义的工作糅合到了解析阶段。

我们希望能完整解析源文件后再进行变量定义判断的工作，因此借鉴了OCaml的解析器实现，区分大小写两种标识符，大写视为构造器，小写视为变量。

在这里也能一窥语言实现的考量，了解为什么很多支持模式匹配的语言规定构造器使用大写、变量使用小写。

这里也能看到为了语言的一致性，false和true应该看作构造器，使用大写，实现中如果要摈弃Caml Light中解析阶段判断是否定义的做法，比较好的方式是在词法分析中把false和true也作为词法单元。

类型检查

解析得到抽象语法树后，进行类型检查判断程序是否合法。项目中使用Damas-Hindley-Milner类型系统的algorithm W进行类型推导。

Algorithm W中使用unification来判断两个类型是否可能相等，为此需要适配两个类型的形状。比如如果要unify函数类型int -> a和另一个类型b -> char，需要把类型变量b变为具体类型int、类型变量b变为具体类型int。

实现unification时有两种方法：

• 使用一个类型映射表，记录各个类型变量被映射为什么类型(具体类型、其他类型变量、或generic类型)

• 每个类型变量维护一个可修改的域，表示不相交的集合，类型变量可以是尚未确定与其他类型的关系(自身为一个集合)，或者被确定与某些类型相同(与它们在一个集合中)。这里的可变域表示为并查集算法的父节点。

使用可变域性能较高，因此我们的实现中也采用了这一方法。

类型的generalization

Damas-Hindley-Milner类型系统中的let-polymorphism阶段，需要把尚未和外部类型联系起来的类型变量generalize成generic类型。

原始的实现方式是遍历类型(表示为一棵树)，访问其中所有类型变量，判断是否和外部类型unify过，如果没有则generalize。http://okmij.org/ftp/ML/generalization.html中提到的Rémy’s level-based generalization采取了一种剪枝策略，也是Caml Light实现所采用的。我们的项目也实现了这一方法。另外文章中还提到了一种惰性实现，可以优化occur check，并加速整个类型推导过程的时间复杂度到近似线性。我们实现了该方法，但考虑到多数情况下类型树不会很大，occur check和遍历类型树的代价不会很大，并且惰性方法要引入额外的空间需求，以及实现的复杂性，未在项目中引入。

实例化generic类型

Caml Light在实例化generic类型时采用了一种技巧(cl75/src/compiler/types.ml)，把实例化分成两个阶段：copy_type和cleanup_type。

copy_type把原来的类型复制了一份，修改了类型树中generic类型变量的可变域，指向一个该变量的实例(不再为generic)，返回的副本与原本的类型共享那些非generic的部分。当原来的类型被复制第二遍的时候，新的副本会与第一份副本共用新生成的非generic类型变量。因此对于相同的generic类型变量，它的各个副本都会是相同的类型实例。

之后经过cleanup_type，原来的类型被还原成copy_type前的形态。

copy_type的特性在产生相关联的类型实例时很方便，比如两棵类型树共享一个generic的类型变量。那么实例化时希望得到的两个类型树实例的对应类型实例也是相同的。可以这样做：先分别对两棵树进行copy_type，再分别cleanup_type，得到的两个副本保证共用了相同的类型实例。

扩充的\(\lambda\)-calculus

ML的语法比较复杂，在编译到字节码需要进行一些简化，为此Caml Light采用了一个扩充的\(\lambda\)-calculus作为中间表示，我们也实现了类似的、但更加简化的扩充\(\lambda\)-calculus。

原始的无类型\(\lambda\)-calculus中唯一的值类型是\(\lambda\)抽象，另外也只有变量和应用两种项形式。经过de-Bruijn index的变换后，可以引入环境这一元素(若干嵌套的\(\lambda\)抽象中的值的列表)，变量指向环境中特定位置项，因此可以用一个索引值替代，由此我们就把Lvar of string换成了Lvar of int，这里之所以能做这样的变换还得感谢静态作用域。

比如在fun x -> fun y -> x中，x和y都在环境中，x可以用de Bruijn index 1代替。

在ML中，值类型还可以是像int这样的基本类型，因此我们需要一个额外的构造器Lconst of constant。原始的无类型\(\lambda\)-calculus也无法表示加法这样的运算，只能采用Church encoding。在ML这样的实际语言中需要有办法表示这些运算，以及其他很多操作如数组取元素、比较两数、根据构造器和参数创建代数数据类型等，因此我们添加了构造器Lprim of prim * lambda list，可以看作prim表示的原语函数应用在一些参数上。

抛开let-polymorphism，let可以等价变形为\(\lambda\)抽象和应用的一个简单组合(let x=... in y变换为(fun x -> y) (...))。而在类型检查通过后，如果把所有值看作是boxed类型，并且使用无类型的\(\lambda\)-calculus，那么我们可以不忽略let-polymorphism的影响。但实现为函数应用会有一定的性能开销，因此尽管不是必须有的，我们还是提供了构造器Llet of lambda list * lambda。

利用call-by-value的求值策略顺序，可以用\(\lambda\)抽象和应用实现表示顺序执行的;(x; y变换为(fun _ -> y) x)，但为了性能考虑设立了Lsequence of lambda * lambda构造器，它会先执行第一项，再执行第二项。通过使用这种方式，实现了对C中语句和表达式的统一。

模式匹配引入了更多的复杂性。当没有模式匹配时，环境中的项(函数的形式参数)只有一种引用方式，即视为一个整体引用。但涉及模式匹配后，考虑fun ((x,y) as a) ->，作为整体的参数可以用a引用，但模式匹配又引入了构成二元组a的两个成分x、y，它们也可以被函数体引用，所以该如何表示它们呢？另外代数数据类型的构造器可以有多个参数，也可以在模式匹配中出现，需要提供一种办法引用它们的参数。

就像代数数据类型的描述那样(元组可以看成是提供了语法支持的特殊代数数据类型)，参数可以看成是它们的子域，我们使用原语Pfield of int来引用某个子域。用于de Bruijn index的环境不再是简单变量的列表，列表中的每一项不仅要提供引用参数自身的方法，也要提供方法引用出现在模式匹配中的所有变量。因此我们把环境表示为一个列表的列表，每个内层列表代替的原来的简单参数，其中包含所有变量的引用方式。

项目源文件front.ml实现了抽象语法树到扩充的\(\lambda\)-calculus的翻译。很多节点的翻译很直观：

1
2
3
4
5
6
7
8
9
10

| Pexpr_apply(e,es) ->
    Lapply(go e, List.map go es)
| Pexpr_array es ->
    Lprim(Pmakeblock(0,0), List.map go es)
| Pexpr_constant c ->
    Lconst c
| Pexpr_sequence(e1,e2) ->
    Lsequence(go e1, go e2)
| Pexpr_tuple es ->
    Lprim(Pmakeblock(1,0), List.map go es)

比如代表函数应用的Pexpr_apply，代表字面量的Pexpr_constant等。元组稍复杂一些，可以看作是使用原语Pmakeblock创建了一个新的block，其各个域是元组的各个成分。

构造器较为复杂，需要判断在代数数据类型定义中该构造器是否带参数(Constr_constant或Constr_regular，以及在表达式中是否带参数，选择翻译成一个创建新block的原语，或者是个\(\lambda\)抽象：接受参数以创建block。

1
2
3
4
5
6
7
8
9
10
11
12
13

| Pexpr_constr(id,arg) ->
    let cd = find_constr_desc id in
    begin match arg with
    | None ->
        begin match cd.info.cs_kind with
        | Constr_constant ->
            Lprim(Pmakeblock cd.info.cs_tag, [])
        | _ ->
            Labstract(Lprim(Pmakeblock cd.info.cs_tag, [Lvar 0]))
        end
    | Some arg ->
        Lprim(Pmakeblock cd.info.cs_tag, [go arg])
    end

全局值

处于顶层的let会产生一个全局值(如基本类型值、函数等)，可以被之后的代码引用。用通常的静态作用域观点看，这样产生的值不在之后代码的作用域内。当然我们可以把在顶层并列放置的let绑定视为是嵌套的，但这种模型无法解决多文件全局值的引用问题，因此不可行。

解决这个问题需要引入全局值的概念，设置原语Pgetglobal of long_ident和Psetglobal of long_ident用于表示读取和写入全局值。

翻译模式匹配

模式匹配是最复杂的部分，允许匹配多个代数数据类型复合的结构，混合字面量、变量和构造器，各个匹配项还有顺序要求，因为如果多个模式都能匹配，那么根据语义应该选取最靠前的匹配项。@slpj的Chapter 5，Philip Wadler提供了详细的描述。@Zinc的5.2.4 Compiling pattern matching提供了Caml Light中的实现方法。在项目中我们又进行了进一步的简化。

对于复杂的模式匹配，比如：

1
2
3

match false, false with
| false, true -> ()
| false, false -> ()

设想一个按顺序匹配元组的各个项的扩充\(\lambda\)-calculus表示，第一个匹配项的false匹配成功后，true会匹配失败，此时应该跳转到第二个匹配项。如何实现这样的逻辑呢？

当涉及多个匹配项时，翻译器会把它们组织成Lstaticcatch(p1,Lstaticcatch(p2,Lstaticcatch(...)))，p1、p2是各模式匹配项翻译得到的代码，执行p1时，若发现后续的模式匹配失败了，就会执行Lstaticraise。其效果相当于抛出了一个异常，该异常会被嵌套它的最内层的Lstaticcatch捕获，尝试执行作为替代的第二条指令。这一机制可以看成是一个静态作用域的异常处理，因此使用了这样的名字：Lstaticcatch和Lstaticraise。

if可以看作是模式匹配的特例，即匹配true和false，但为了性能考虑，设立了Lif这一构造器。

翻译异常处理

Lcatch of lambda * lambda的第一个参数是try的代码体，如果抛出异常则把控制权交给模式匹配部分，即第二个参数。

扩充\(\lambda\)-calculus定义

lambda.ml中的定义：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15

type lambda =
  | Labstract of lambda
  | Lapply of lambda * lambda list
  | Lcatch of lambda * lambda
  | Lcond of lambda * (constant * lambda) list
  | Lconst of constant
  | Lif of lambda * lambda * lambda
  | Llet of lambda list * lambda
  | Lletrec of lambda list * lambda
  | Lprim of prim * lambda list
  | Lsequence of lambda * lambda
  | Lstaticcatch of lambda * lambda
  | Lstaticraise
  | Lswitch of int * lambda * (constr_tag * lambda) list
  | Lvar of int

扩充\(\lambda\)-calculus翻译成Zinc抽象机器的linear code

接下来把中间表示翻译成Zinc抽象机器的linear code。字节码相当于机器码，而linear code就相当于汇编代码。Linear code的定义在文件instruction.ml中：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26

type zinc_instruction =
  | Kaccess of int
  | Kapply
  | Kbranch of int
  | Kbranchif of int
  | Kbranchifnot of int
  | Kcur of int
  | Kdummy of int
  | Kendlet of int
  | Kgetglobal of long_ident
  | Kgrab
  | Klabel of int
  | Klet
  | Kmakeblock of constr_tag * int
  | Kpoptrap
  | Kprim of prim
  | Kpush
  | Kpushmark
  | Kpushtrap of int
  | Kquote of struct_constant
  | Kreturn
  | Ksetglobal of long_ident
  | Kswitch of int array
  | Ktermapply
  | Ktest of bool_test * int
  | Kupdate of int

type zinc_instruction的多数构造器都和字节码有直观的对应关系，比如构造器Kaccess of int翻译成字节码时，会额外输出一个uint8_t类型的操作数。表示的标号构造器Klabel of int不会生成字节码，但能作为一个标签供其他指令引用。

中间表示翻译成linear code的实现在文件back.ml中，采用了compile with continuation的编译方法。其中的主要函数是compile_lambda中的compile_expr : int -> lambda -> instruction list -> instruction list，第一个参数表示模式匹配失败后需要跳转到的代码，第二个参数是待编译的扩充\(\lambda\)-calculus，第三个参数代表该指令执行完后需要执行的continuation，返回Zinc指令的列表(需要包含continuation)。

很多结构的翻译是直观的：

1
2
3
4
5
6
7
8

| Lvar i ->
    Kaccess i :: cont
| Lconst c ->
    Kquote c :: cont
| Lprim(Pdummy n, []) ->
    Kdummy n::cont
| Lprim(Pgetglobal id, []) ->
    Kgetglobal id::cont

模式匹配失败后会执行Lstaticraise，翻译的方式是跳转到嵌套该代码的最靠近的Lstaticcatch。

1
2

| Lstaticraise ->
    Kbranch staticraise::cont

有部分结构比如Lif，代码执行路径可能有多条，需要引入一些分支指令。

Lswitch根据参数(必须是block)的tag值及跳转表进行跳转。

Lcatch的翻译方案是压入一个异常处理栈帧，执行try代码体时若发生异常，控制权会交给最近的异常处理栈帧，如果它匹配失败就把控制权交给外层的异常处理栈帧。若未发生异常则弹出异常处理栈帧。

全局值

扩充\(\lambda\)-calculus中对全局值的处理可以直接翻译成相应的抽象机器指令，同样需要用于处理读取和写入全局值的指令。读取和写入相同名称的指令应该访问同一个内存地址。为了性能的考虑，我们不希望在运行时维护一个名称到具体内存地址的映射表。再考虑到一个文件访问另一个文件定义的全局值，我们在生成代码后还需要一个过程把这些名字解析到合适的槽位，因此需要下一个阶段——链接。

1
2
3
4

| Lprim(Pgetglobal id, []) ->
    Kgetglobal id::cont
| Lprim(Psetglobal id, [e]) ->
    c_expr e (Ksetglobal id::cont)

Linear code翻译为字节码，生成目标文件

这一阶段的实现在文件emit.ml中。我们使用了一个简单的翻译方案。每个指令拆分为操作码和参数两部分，操作码占据一个字节，参数则有多种形式：uint8_t、int16_t、标签等。

因为标签定义和引用都是在当前源文件里局部的，生成代码时可以把这些标签引用都解析为字节码中的相对地址。

链接器

正如之前所提到的，这一过程并非必须，但基于性能的考虑需要在编译流程中引入这一阶段。读取各个源文件编译得到的目标文件(需要重定位)，梳理其中全局值定义和引用的关系，把各条Ksetglobal、Kgetglobal指令解析到正确的槽位是这一阶段的主要目标。

在我们的实现中这一部分的代码在ld.ml中，ld是传统的链接器的名字，我们借用了这一名字来贴切地表示这段代码需要完成的任务。

ld.ml使用了一个两遍扫描过程，先扫描各目标文件得到所有的全局值定义，再扫描各目标文件，解析其中的全局值定义和引用，把指令写入可执行文件中。该文件实际上还处理了原语操作。

运行时系统和字节码解释器

运行时系统和字节码解释器用C实现，在目录runtime/中。

初始化共享的size域为0的构造器

因为构造器的域不可变，且size域为0的block经常被使用，我们可以把tag值为0到255的256个block缓存起来，供所有size域为0的block共享。Caml Light的cl75/src/runtime/mlvalues.h中声明了extern header_t first_atoms[];，()、true等就用这些first_atoms元素的指针表示。我们的运行时也采用了这一技巧。

全局值初始化

字节码文件中有一些float、string常量，执行时需要一个加载过程，把这些常量分配为block供代码使用。另外还有一些Psetglobal需要引用的槽位，初始化为整数0(bit pattern是1)。

指令解码和派发

解释器的主要部分是runtime/main.c中的一个取指令并解释的循环。常规解释器实现方法是在循环里放置一个switch实现指令的解码和派发：

1
2
3
4
5
6
7
8
9
10
11

for(;;) {
  switch (*pc++) {
    case ACCESS:
      ...
      break;
    case ADDFLOAT:
      ...
      break;
    ...
  }
}

但这样做，指令一条抽象机器指令会引入至少两条CPU的跳转指令，即break引入的跳转到switch处的指令和switch跳到某一个标签处的指令。

我们可以让break实现解码下一条指令并跳转到相应标签处的功能，这样就可以节省一条跳转指令。GCC提供了computed goto特性，可以获取可以获取标签所指代码的地址(void*类型)，从而可以手工实现一个跳转表：

1
2
3
4
5
6
7
8
9
10

void *jumptable[] = {&&ACCESS, &&ADDFLOAT, ...};
goto *jumptable[*pc++];

ACCESS:
  ...
  goto *jumptable[*pc++];
ADDFLOAT:
  ...
  goto *jumptable[*pc++];
...

垃圾收集

Caml Light使用的垃圾收集算法可以参考@Sestoft94，结合了stop-and-copy和分代mark-sweep。我们的实现则使用了一个非常简单的方法，基于Schorr-Waite graph marking算法。该算法不使用栈，只需要在节点上分配极少量信息(\(\lceil\log_2{n+1}\rceil\) bits，其中\(n\)是该节点的指针域数目)。在一些资料中被称为pointer reversal。基本思想是在节点信息里维护一个域\(s\)，表示遍历过程中的访问次数，并把遍历过程中祖先节点下溯的指针翻转，再设置一个表示当前节点父节点的指针\(p\)以把祖先节点组织为一个链。

数据表示

不同类型语言的实现使用了截然不同的数据表示方式。

对于Scheme这样的动态类型语言的实现，数据在运行时需要标志以区分不同类型，所有类型的数据通常需要适配某一种通用的格式，通常是一个字的指针，指向一个block，block里存储具体的数据，这种存储方式称为boxed，记录类型、数组等都是boxed类型。对于双精度浮点数，因为占64位，而机器字长不足以同时表示指针和所有可能的浮点数，因此浮点数也必须采用boxed类型。

因为整数使用的普遍性及性能考虑，整数通常不存储在block中并用指针标识，而是用左移一位且最低位置1的方式表示。因为指针通常要满足一定的对齐条件，最低位为0，这种表示方法不会引起歧义。

对于C、Pascal这样的monomorphic静态类型语言的实现，因为无需进行运行时类型测试，各数据类型不必有统一的格式，因此往往可以有不同的大小。单精度、双精度浮点数可以采取格子的unboxed表示，可以有各种大小的整数类型，比如int8_t、int64_t等。不同类型的函数也可以采取不同的调用约定，比如参数为浮点数或整数时，很多架构下在调用函数时会把参数放在不同的寄存器中。

引入parametric polymorphism后，问题变得复杂，有三类解决方案：

• 限制polymorphism的形式，比如Modula中规定抽象类型必须是指针类型，Java中不允许unboxed类型如int转换为Object。这种方式的缺点是不够直观，并且对语言表现力有较大的牺牲。

• 为不同类型生成多份代码。C++模板通常采取这种方式，为不同类型生成不同的代码。缺点是代码大小膨胀，链接复杂性增加，可能需要链接代码生成等。

• 采用Scheme式样的处理方式。普遍采用boxed类型。缺点是性能损失。

这方面有一些研究成果，比如采取C和Scheme结合的方法、在polymorphic代码中引入类型大小信息等。

Block和整数的区分

我们采取boxed类型的方式，多数类型如元组、数组、float等，它们的实际内容都用堆上分配的一块内存表示，使用指针来标识它们，参数传递和变量存储时都使用表示它们的指针。整数则用低位为1的值表示。

整数

一个整数\(i\)表示为\(2i+1\)，在一个字长为32位的机器上(下面都假定采用32位机)，能表示的int范围不再是\([-2^{31},2^{31})\)，丢失了一位变为\([-2^{30},2^{30})\)。相应地，整数运算需要做一些修改，比如取反实现为\(2-x\)、加法实现为\(x+y-1\)等。

Block

一个block由记录元数据的首部和实际存储的数据两部分组成。字符串、数组和闭包的格式有些特殊，其他block采用统一的格式，元数据占两个字，第一个字记录tag、block的大小和用于垃圾收集的字段color。第二个字是一个XOR链表指针，堆上所有分配的block都串在一个XOR链表里。

bits  31  20 19    8 7   0   31                 0
     +------+-------+-----+ +--------------------+
     | size | color | tag | | xor of prev & next |
     +------+-------+-----+ +--------------------+

Tag占据一个字节，标识了该block的类型，可用于区分内置类型float(表示为一个双精度浮点数)、string、array和sum类型采用了哪一个构造器。注意经过类型检查后，我们不需要区分不同代数数据类型，只需要标识特定代数数据类型采用了哪一个构造器。

若tag值大于或等于No_scan_tag(251)，就表示这个block存储的数据都是不透明的字节信息，不应该把它们解释为指向其他block的指针。一个代数数据类型的各个构造器，分别用tag值0、1、2等表示。unit类型的构造器()的tag值为1，bool类型的构造器false的tag值为0，true的tag值为1。

size域代表block的指针域数目，对于true这类不包含子域的值，其size为0。

color域用于垃圾收集，对于我们采用的Schorr-Waite graph marking算法，color域需要\(\max\lceil\log_2{n+1}\rceil\)个bit，其中\(n\)是该节点的指针域数目。如果color域和size域使用相同的长度，如我们的实现中所选取的，size域最大可以为\(2^{12}-1=4095\)。元组很难有超过4095项，一个类型的构造器数目也很难超过4095，因此这种方式对于这些类型都是合适的。但是对于字符串长度和数组大小，4095还是相对较小，因此这两个类型要采取特殊的表示方式，把color域的bit也作为size使用，但这样就需要其他地方存储color域，我们选择了在XOR指针域后再加一个字编码color。

下表整理了一些常见类型值的表示方式：

|l|l| 值 & 表示
3 & 3*2+1=7
’a’ & 97*2+1=195
true & 指向一个tag为1，size为0的块的指针
false & 指向一个tag为0，size为0的块的指针
[] & 指向一个tag为0，size为0的块的指针
3::[] & 指向一个tag为1，size为2的块的指针，该块的两个域分别为2*3+1=7和一个表示[]的块

字符串的表示

字符串的block的tag大于No_scan_tag，但元数据存储格式略有区别。因为字符串不包含指向其他节点的指针域，采用Schorr-Waite graph marking算法垃圾收集时只需要区分是否被标记过，color域被缩短为只有一个bit，其余bit都被size域占用，size域共23个bit，最多可以表示长度为\(2^{23}-1\)的字符串。

bits  31  9  8     8 7   0   31                 0
     +------+-----+-+-----+ +--------------------+
     | size | color | tag | | xor of prev & next |
     +------+-------+-----+ +--------------------+

数组的表示

数组的block的tag大于No_scan_tag。原来第一个字的color域全部都被size域占用，因此最大长度是\(2^{24}-1\)，color域被移动到XOR链表指针域的下一个字。

bits  31           8 7   0   31                 0   31                 0
     +--------------+-----+ +--------------------+ +--------------------+
     |     size     | tag | | xor of prev & next | |        color       |
     +--------------+-----+ +--------------------+ +--------------------+

闭包的表示

闭包的block的tag小于No_scan_tag，size域固定为2，两个域分别为代码指针和表示环境的闭包。

环境的表示

为了一致性，环境也用block表示，但因为它不会作为值传递，tag值无关紧要，size域的值就是环境中存储的变量数。

Block中的XOR指针域

使用mark-sweep方式的垃圾收集器需要能追踪分配过的堆对象，我们在首部的XOR指针域中维护了所有分配对象的双链表。对于简单的收集所有对象并标记扫除的垃圾收集器，单链表足矣。但考虑到拓展性，我们采用了双链表，以方便未来可能需要支持的操作。因为两个指针域空间开销有点大，我们使用了XOR链表，即每个节点的指针域为其前驱和后继节点地址的XOR。根据XOR链表头或尾节点的地址即可遍历整个链表。

垃圾收集

Caml Light使用的垃圾收集算法可以参考@Sestoft94，结合了stop-and-copy和分代mark-sweep。我们的实现则使用了一个非常简单的方法，基于Schorr-Waite graph marking算法。该算法不使用栈，只需要在节点上分配极少量信息(\(\lceil\log_2{n+1}\rceil\) bits，其中\(n\)是该节点的指针域数目)。在一些资料中被称为pointer reversal。基本思想是在节点信息里维护一个域\(s\)，表示遍历过程中的访问次数，并把遍历过程中祖先节点下溯的指针翻转，再设置一个表示当前节点父节点的指针\(p\)以把祖先节点组织为一个链。

其他

项目中我们还实现了一些辅助工具。

Pretty printer

Pretty-print指的是对文本文件(特别是标记语言和程序代码)采用语法高亮、调整换行空格、调整字体等手段使之易于阅读。项目中实现了一个pretty printer，用于生成进行换行空格排版调整后的代码和调试信息。

下面只考虑进行换行空格排版调整的pretty printer。Haskell中的pretty printer主要有两大流派，其一是John Hughes设计，由Simon Peyton Jones修改的，跟随GHC一起发行，称为Hughes-PJ库；其二是Philip Wadler在The Fun of Programming中设计的pretty printer@Wadler，后由Leijen修改，添加了对齐等扩展得到的，称为Wadler-Leijen库。

@prettiest-printer提出了另一种方法，是对Wadler/Leijen的一种改良。原始的Hughes-PJ和Wadler/Leijen对于并集文档，为了注重性能，使用了贪心算法进行选择。但这样得到的文档不一定是最短的。这一方法以行为单位搜索最短表示。我对它进行了改良，使得能保证返回适应宽度的文档。

@Swierstra04提出了一种线性算法，@Swierstra09提供了该算法的不依赖lazy evaluation的版本。我实现并扩展了这种方法，引入了对齐操作。

h=5;a=let b=4;c=5 in (case 4 of <3> a -> 5;<4>->6;<4>-> case 3 of <2> A->2 * (let g = (let h = 5 in 5) + 8 in h)); h=6

11月21日，比赛前一天

20日晚还在赶第二天编译原理课的展示，21日上午才开始搞江苏信安竞赛初赛的运维。网站还没有用户和队伍信息，信息要从一个csv文件中导入。也没有题目信息，需要从一个.docx文件里导入，我用的办法是unoconv -f txt a.docx转成文本文件a.txt后用awk处理得到csv格式的文件，之后在Rails项目的lib/tasks目录里创建了一个导入csv格式题目信息的task。在BCTF初赛平台的基础上，还有很多页面、路由和模型等需要调整。

Read More

Generate String from Regex

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115

let is_lower c =
  'a' <= c && c <= 'z'

type ast =
  | Lit of char
  | Star of ast
  | Cat of ast*ast
  | Or of ast*ast

module Parser = struct
  type state = Ret of ast | Cont of char list * ast list

  let parse re =
    let isp_tbl = Hashtbl.create 10 in
    let icp_tbl = Hashtbl.create 10 in
    List.iter (fun (c,x) -> Hashtbl.replace isp_tbl c x)
      ['\x00',0; '(',1; '|',3; '%',5; '*',7; ')',7];
    List.iter (fun (c,x) -> Hashtbl.replace icp_tbl c x)
      ['\x00',0; ')',1; '|',2; '%',4; '*',6; '(',6];

    let n = String.length re in
    let rec go ops vs i =
      let implicit_cat = 0 < i && i < n && (re.[i] = '(' || is_lower re.[i]) &&
        (re.[i-1] <> '(' && re.[i-1] <> '|') in
      let incoming implicit_cat ops vs =
        let ic = if implicit_cat then '%' else if i = n then '\x00' else re.[i] in
        if is_lower ic then
          Cont (ops, Lit ic::vs)
        else
          let icp = Hashtbl.find icp_tbl ic in
          let rec pop_go (op::ops' as ops) vs =
            if Hashtbl.find isp_tbl op > icp then
              match op with
              | '*' ->
                  let x::vs' = vs in
                  pop_go ops' (Star x::vs')
              | '%' ->
                  let y::x::vs' = vs in
                  pop_go ops' (Cat (x,y)::vs')
              | '|' ->
                  let y::x::vs' = vs in
                  pop_go ops' (Or (x,y)::vs')
              | c ->
                  Printf.printf "+ c: %c %c\n" op ic;
                  ops ,vs
            else
              ops, vs
          in
          let (op::ops' as ops), vs = pop_go ops vs in
          if Hashtbl.find isp_tbl op = icp then (
            if ic = '\x00' then
              Ret (List.hd vs)
            else
              Cont (ops', vs)
          ) else
            Cont (ic::ops, vs)
      in
      match incoming implicit_cat ops vs with
      | Ret _ as ret -> ret
      | Cont (ops,vs) ->
          if not implicit_cat then
            go ops vs (i+1)
          else
            let Cont (ops,vs) = incoming false ops vs in
            go ops vs (i+1)
    in
    let Ret ret = go ['\x00'] [] 0 in
    ret
end

let generate len =
  let rec go = function
    | Lit lit ->
        let a = Array.make (len+1) "#" in
        a.(1) <- String.make 1 lit;
        a
    | Star x ->
        let b = go x in
        let a = Array.make (len+1) "#" in
        a.(0) <- "";
        for i = 1 to len do
          let rec fill j =
            if j > 0 then
              if b.(j) <> "#" && a.(i-j) <> "#" then
                a.(i) <- a.(i-j) ^ b.(j)
              else
                fill (j-1)
          in
          fill i
        done;
        a
    | Cat (x,y) ->
        let b = go x and c = go y in
        let a = Array.make (len+1) "#" in
        for i = 0 to len do
          for j = 0 to len-i do
            if a.(i+j) = "#" && b.(i) <> "#" && c.(j) <> "#" then
              a.(i+j) <- b.(i) ^ c.(j)
          done
        done;
        a
    | Or (x,y) ->
        let b = go x in
        let c = go y in
        Array.init (len+1) (fun i -> if b.(i) <> "#" then b.(i) else c.(i))
  in
  go

let () =
  let len = read_int () in
  let re = read_line () in
  let ast = Parser.parse re in
  let a = generate len ast in
  let s = a.(len) in
  print_endline (if s <> "#" then s else "NIL")

While Language

生成AST后进入求值阶段，可以用state monad处理求值部分。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249

module Str = struct
  let implode l =
    let s = String.make (List.length l) ' ' in
    let rec go i = function
      | [] -> s
      | h::t -> s.[i] <- h; go (i+1) t
    in
    go 0 l

  let explode s =
    let rec go acc i =
      if i = String.length s then
        List.rev acc
      else
        go (s.[i]::acc) (i+1)
    in
    go [] 0
end

module LazyList = struct
  type 'a node = Nil  | Cons of 'a * 'a t and 'a t = 'a node Lazy.t
  let empty = lazy Nil
  let singleton x = lazy (Cons (x, empty))
  let cons h t = lazy (Cons (h, t))
  let force = Lazy.force
  let rec map f l = lazy (
    match force l with
    | Nil -> Nil
    | Cons (h, t) -> Cons (f h, map f t)
    )
  let rec append l1 l2 = lazy (
    match force l1 with
    | Nil -> force l2
    | Cons (h, t) -> Cons (h, append t l2)
    )
  let rec concat ll = lazy (
    match force ll with
    | Nil -> Nil
    | Cons (h, t) -> append h (concat t) |> force
    )
  let is_empty l =
    match force l with
    | Nil -> true
    | Cons _ -> false
end

module ParserCombinators = struct
  type input = { s: string; pos: int }
  type 'a t = input -> ('a * input) LazyList.node Lazy.t

  let unit x s = LazyList.singleton (x, s)
  let zero = unit []
  let (>>=) (type a) (type b) (x : a t) (f : a -> b t) s = LazyList.map (fun (a,s') -> f a s') (x s) |> LazyList.concat
  let (>>) x y = x >>= fun _ -> y
  let (<<) x y = x >>= fun b -> y >> unit b
  let (<|>) x y s = let r = x s in if LazyList.is_empty r then y s else r
  let fail s = LazyList.empty
  let (<$>) f x = x >>= fun b -> unit (f b)
  let (<$) b x = x >> unit b
  let (<*>) f x = f >>= fun g -> x >>= fun b -> unit (g b)
  let (<**>) x f = x >>= fun b -> f >>= fun g -> unit (g b)

  let rec many x =
    let go = x >>= fun b ->
      many x >>= fun bs ->
      unit (b::bs)
    in
    go <|> zero

  let many1 x =
    x >>= fun b ->
    many x >>= fun bs ->
    unit (b::bs)

  let next s =
    if s.pos = String.length s.s then
      None
    else
      Some (s.s.[s.pos], { s with pos = s.pos + 1 })

  let pred f = (fun s -> match next s with
    | None -> LazyList.empty
    | Some x -> LazyList.singleton x) >>= fun b ->
        if f b then unit b else fail

  let char c = pred (fun c' -> c = c')
  let str s =
    let rec go = function
      | [] -> zero
      | h::t -> char h >>= fun b -> go t >>= fun bs -> unit (b::bs)
    in
    Str.explode s |> go
  let digit = pred (fun c -> '0' <= c && c <= '9')
  let lower = pred (fun c -> 'a' <= c && c <= 'z')
  let drop x = x >> zero
  let space = pred (fun c -> c = ' ' || c = '\t' || c = '\r' || c = '\n')
  let token x = x << drop (many space)
  let char_ c = char c |> token
  let str_ s = str s |> token

  let sep_by x sep =
    let go = x >>= fun b ->
      many (drop sep >> x) >>= fun bs ->
      unit (b::bs)
    in
    go <|> zero

  let chainl1 x op =
    let rec go a =
      (op >>= fun f ->
      x >>= fun b ->
      go (f a b)) <|> unit a
    in
    x >>= go

  let parse x s =
    match LazyList.force ((drop (many space) >> x) { s; pos = 0 }) with
    | LazyList.Nil -> None
    | LazyList.Cons ((x, _), _) -> Some x
end

type aexpr =
  | Num of int64
  | Var of string
  | Add of aexpr * aexpr
  | Sub of aexpr * aexpr
  | Mul of aexpr * aexpr
  | Div of aexpr * aexpr

type bexpr =
  | Bool of bool
  | Not of bexpr
  | And of bexpr * bexpr
  | Or of bexpr * bexpr
  | Lt of aexpr * aexpr
  | Gt of aexpr * aexpr

type stmt =
  | Chain of stmt list
  | Assign of string * aexpr
  | If of bexpr * stmt * stmt
  | While of bexpr * stmt

module Parser = struct
  include ParserCombinators

  let add x y = Add (x,y)
  let sub x y = Sub (x,y)
  let mul x y = Mul (x,y)
  let div x y = Div (x,y)
  let num l = Num (Str.implode l |> Int64.of_string)
  let var l = Var (Str.implode l)
  let chain xs = Chain xs
  let if_ b t e = If (b,t,e)
  let while_ b t = While (b,t)
  let assign x y = Assign (x,y)
  let and_ x y = And (x,y)
  let or_ x y = Or (x,y)
  let lt x y = Lt (x,y)
  let gt x y = Gt (x,y)

  let rec aexpr =
    let rec e0 = lazy ((num <$> token (many1 digit)) <|> (var <$> token (many1 lower)) <|> (fun s -> (char_ '(' >> Lazy.force e2 << char_ ')') s))
    and e1 = lazy (chainl1 (Lazy.force e0) ((mul <$ char_ '*') <|> (div <$ char_ '/')))
    and e2 = lazy (chainl1 (Lazy.force e1) ((add <$ char_ '+') <|> (sub <$ char_ '-')))
    in
    Lazy.force e2

  let rec bexpr =
    let rec e0 = lazy ((Bool false <$ str_ "false") <|> (Bool true <$ str_ "true") <|>
      (fun s -> (char_ '(' >> Lazy.force e3 << char_ ')') s)
      )
    and e1 = lazy ((aexpr <**> ((lt <$ char_ '<') <|> (gt <$ char_ '>')) <*> aexpr) <|> Lazy.force e0)
    and e2 = lazy (chainl1 (Lazy.force e1) ((and_ <$ str_ "and")))
    and e3 = lazy (chainl1 (Lazy.force e2) ((or_ <$ str_ "or")))
    in
    Lazy.force e3

  let rec stmt =
    let rec sassign = lazy (Str.implode <$> token (many1 lower) <**> (assign <$ str_ ":=") <*> aexpr)
    and sif = lazy ((if_ <$ str_ "if") <*> bexpr << str_ "then" <*> Lazy.force sb << str_ "else" <*> Lazy.force sb)
    and sb = lazy (char_ '{' >> (fun s -> Lazy.force s1 s) << char_ '}')
    and swhile = lazy ((while_ <$ str_ "while") <*> bexpr << str_ "do" <*> Lazy.force sb)
    and s0 = lazy (Lazy.force sif <|> Lazy.force swhile <|> Lazy.force sb <|> Lazy.force sassign)
    and s1 = lazy (chain <$> sep_by (Lazy.force s0) (char_ ';'))
    in
    Lazy.force s1
end

module Eval = struct
  type store = (string, int64) Hashtbl.t
  type 'a t = store -> 'a

  let unit a s = a
  let (>>=) x f s = f (x s) s
  let (>>) x y = x >>= fun _ -> y
  let (<$>) f x s = x s |> f
  let rec map_ f = function
    | [] -> unit ()
    | h::t -> f h >> map_ f t
  let liftM2 f x y s =
    let x' = x s in
    let y' = y s in
    f x' y'

  let rec eval_a = function
    | Num n -> unit n
    | Var v -> fun tbl -> Hashtbl.find tbl v
    | Add (x,y) -> liftM2 Int64.add (eval_a x) (eval_a y)
    | Sub (x,y) -> liftM2 Int64.sub (eval_a x) (eval_a y)
    | Mul (x,y) -> liftM2 Int64.mul (eval_a x) (eval_a y)
    | Div (x,y) -> liftM2 Int64.div (eval_a x) (eval_a y)

  let rec eval_b = function
    | Bool b -> unit b
    | Not x -> not <$> eval_b x
    | And (x,y) -> liftM2 (&&) (eval_b x) (eval_b y)
    | Or (x,y) -> liftM2 (||) (eval_b x) (eval_b y)
    | Lt (x,y) -> liftM2 (<) (eval_a x) (eval_a y)
    | Gt (x,y) -> liftM2 (>) (eval_a x) (eval_a y)

  let rec eval_s = function
    | Assign (v,x) -> fun tbl -> Hashtbl.replace tbl v (eval_a x tbl)
    | Chain xs -> map_ eval_s xs
    | If (b,t,e) -> eval_b b >>= fun b' -> eval_s (if b' then t else e)
    | While (b,t) as w -> eval_b b >>= fun b' -> if b' then eval_s t >> eval_s w else unit ()

  let interpret ast =
    let tbl = Hashtbl.create 13 in
    eval_s ast tbl;
    Hashtbl.fold (fun k v xs -> (k,v)::xs) tbl [] |> List.sort compare |> List.iter (fun (k,v) ->
      Printf.printf "%s %Ld\n" k v
    )
end

let read _ =
  let rec go acc =
    try
      let s = read_line () in
      go (s::acc)
    with End_of_file ->
      String.concat "\n" (List.rev acc)
  in
  go []

let () =
  match Parser.parse Parser.stmt (read 0) with
  | None -> ()
  | Some ast -> Eval.interpret ast

Down With Abstractions

https://www.hackerrank.com/challenges/down-with-abstractions

要求把lambda calculus转化为SKIBC组合子，Wikipedia给出了一个算法进行这种转换。我尝试用De Bruijn index表示的lambda calculus实现。算法中有一个子程序是判断某个子calculus内是否有一个变量为free的，如果用朴素的实现方式(遍历取出所有变量，一一判断是否存在free的)，会增大时间复杂度。如果calculus的形态不发生改变，那么可以Inversion of Control：对于每个lambda abstraction找自由变量的要求，转换为把所有变量涉及的lambda abstraction标记出来。考虑到算子的形态会发生改变，我最终采用对于每个子calculus设置一个persistent heap来表示。

下面是实现代码，其中还结合state monad和lazy list实现了一个parser monad，用parsing expression grammar的方式来处理。 mutually recursive函数，目前理解得尚不清楚，用了一个比较麻烦的方式tying-the-knot：各function都表示为lazy的，这样所有的引用都需要表示为Lazy.force referenced的形式，另外对于引用链上所有back reference的地方都要使用eta expansion。如果不这么做会报运行时错误。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338

module Str = struct
  let implode l =
    let s = String.make (List.length l) ' ' in
    let rec go i = function
      | [] -> s
      | h::t -> s.[i] <- h; go (i+1) t
    in
    go 0 l

  let explode s =
    let rec go acc i =
      if i = String.length s then
        List.rev acc
      else
        go (s.[i]::acc) (i+1)
    in
    go [] 0
end

module LazyList = struct
  type 'a node = Nil  | Cons of 'a * 'a t and 'a t = 'a node Lazy.t
  let empty = lazy Nil
  let singleton x = lazy (Cons (x, empty))
  let cons h t = lazy (Cons (h, t))
  let force = Lazy.force
  let rec map f l = lazy (
    match force l with
    | Nil -> Nil
    | Cons (h, t) -> Cons (f h, map f t)
    )
  let rec append l1 l2 = lazy (
    match force l1 with
    | Nil -> force l2
    | Cons (h, t) -> Cons (h, append t l2)
    )
  let rec concat ll = lazy (
    match force ll with
    | Nil -> Nil
    | Cons (h, t) -> append h (concat t) |> force
    )
  let is_empty l =
    match force l with
    | Nil -> true
    | Cons _ -> false
end

module ParserCombinators(S : sig type store end) = struct
  type store = S.store
  type input = { s: string; pos: int; store: store }
  type 'a t = input -> ('a * input) LazyList.node Lazy.t

  let unit x s = LazyList.singleton (x, s)
  let zero = unit []
  let (>>=) (type a) (type b) (x : a t) (f : a -> b t) s = LazyList.map (fun (a,s') -> f a s') (x s) |> LazyList.concat
  let (>>) x y = x >>= fun _ -> y
  let (<<) x y = x >>= fun b -> y >> unit b
  let (<|>) x y s = let r = x s in if LazyList.is_empty r then y s else r
  let fail s = LazyList.empty
  let (<$>) f x = x >>= fun b -> unit (f b)
  let (<$) b x = x >> unit b
  let (<*>) f x = f >>= fun g -> x >>= fun b -> unit (g b)
  let (<**>) x f = x >>= fun b -> f >>= fun g -> unit (g b)

  let rec many x =
    let go = x >>= fun b ->
      many x >>= fun bs ->
      unit (b::bs)
    in
    go <|> zero

  let many1 x =
    x >>= fun b ->
    many x >>= fun bs ->
    unit (b::bs)

  let next s =
    if s.pos = String.length s.s then
      None
    else
      Some (s.s.[s.pos], { s with pos = s.pos + 1 })

  let pred f = (fun s -> match next s with
    | None -> LazyList.empty
    | Some x -> LazyList.singleton x) >>= fun b ->
        if f b then unit b else fail

  let char c = pred (fun c' -> c = c')
  let str s =
    let rec go = function
      | [] -> zero
      | h::t -> char h >>= fun b -> go t >>= fun bs -> unit (b::bs)
    in
    Str.explode s |> go
  let drop x = x >> zero
  let space = pred (fun c -> c = ' ' || c = '\t' || c = '\r' || c = '\n')
  let ident = Str.implode <$> many1 (pred (fun c -> 'a' <= c && c <= 'z' || 'A' <= c && c <= 'Z' || '0' <= c && c <= '9' || c = '_'))

  let token x = x << drop (many space)
  let char_ c = char c |> token
  let ident_ = token ident

  let (>>::) x y =
    x >>= fun a ->
    y >>= fun b ->
    unit (a::b)

  let sep_by x sep =
    let go = x >>= fun b ->
      many (drop sep >> x) >>= fun bs ->
      unit (b::bs)
    in
    go <|> zero

  let chainl1 x op =
    let rec go a =
      (op >>= fun f ->
      x >>= fun b ->
      go (f a b)) <|> unit a
    in
    x >>= go

  let rec chainr1 x op =
    let go a =
      (op >>= fun f ->
      chainr1 x op >>= fun b ->
      unit (f a b)) <|> unit a
    in
    x >>= go

  let parse x store s =
    match LazyList.force ((drop (many space) >> x) { s; pos = 0; store }) with
    | LazyList.Nil -> None
    | LazyList.Cons ((x, _), _) -> Some x
end

module LeftistHeap = struct
  type t = E | N of int * int * int * t * t

  let empty = E

  let is_empty = function
    | E -> true
    | _ -> false

  let singleton x = N (x,0,0,E,E)

  let rank = function
    | E -> -1
    | N (_,_,rk,_,_) -> rk

  let make x l r =
    if rank l >= rank r then
      N (x,0,rank r+1,l,r)
    else
      N (x,0,rank l+1,r,l)

  let add i = function
    | E -> E
    | N (x,d,rk,l,r) -> N (x+i,d+i,rk,l,r)

  let rec merge h1 h2 = match h1, h2 with
    | E, _ -> h2
    | _, E -> h1
    | N (x,d1,_,l1,r1), N (y,d2,_,l2,r2) ->
        if x < y then
          make x (add d1 l1) (merge (add d1 r1) h2)
        else
          make y (add d2 l2) (merge (add d2 r2) h1)

  let top = function
    | E -> invalid_arg "empty"
    | N (x,_,_,_,_) -> x

  let pop = function
    | E -> invalid_arg "empty"
    | N (_,d,_,l,r) -> merge (add d l) (add d r)

  let push h x = merge h (N (x,0,0,E,E))
end

type term =
  | Var of LeftistHeap.t * int
  | Abs of LeftistHeap.t * term
  | App of LeftistHeap.t * term * term
  | S
  | K
  | I
  | B
  | C

module List = struct
  include List

  let fold_left1 f xs =
    List.fold_left f (List.hd xs) (List.tl xs)

  let rec drop c = function
    | [] -> []
    | _::xs' as xs ->
        if c = 0 then
          xs
        else
          drop (c-1) xs'
end

let get_dh = function
  | Var (dh,_) -> dh
  | App (dh,_,_) -> dh
  | Abs (dh,_) -> dh
  | _ -> LeftistHeap.empty

let rec cut dh =
  if LeftistHeap.is_empty dh then
    dh
  else if LeftistHeap.top dh < 0 then
    cut (LeftistHeap.pop dh)
  else
    dh

(*let rec free l = function*)
  (*| Var (dh, c) -> c = l*)
  (*| App (dh,x,y) -> free l x || free l y*)
  (*| Abs (dh,x) -> free (l+1) x*)
  (*| _ -> false*)

let free x = match x with
  | Var (_,_)
  | App (_,_,_)
  | Abs (_,_) ->
      let dh = get_dh x in
      not (LeftistHeap.is_empty dh) && LeftistHeap.top dh = 0
  | _ -> false

let rec shift = function
  | Var (dh,c) as v -> Var (LeftistHeap.add (-1) dh |> cut, c-1)
  | App (dh,x,y) -> App (LeftistHeap.add (-1) dh |> cut, shift x, shift y)
  | Abs _ -> assert false
  | c -> c

let var x = Var (LeftistHeap.singleton x, x)

let abstract x = Abs (LeftistHeap.add (-1) (get_dh x) |> cut, x)

let app x y = App (LeftistHeap.merge (get_dh x) (get_dh y), x, y)

let rec nest lv t =
  if lv = 0 then
    t
  else
    nest (lv-1) (abstract t)

let print t =
  let rec go r = function
  | Var (_,c) ->
      Printf.printf "%d" c
  | Abs _ ->
      assert false
  | App (_,x,y) ->
      if r then print_char '(';
      go false x;
      go true y;
      if r then print_char ')'
  | S -> print_char 'S'
  | K -> print_char 'K'
  | I -> print_char 'I'
  | B -> print_char 'B'
  | C -> print_char 'C'
  in
  go false t

let rec tr =
  let e = LeftistHeap.empty in function
  | App (_,x,y) -> app (tr x) (tr y)
  | Abs (_, Var (_, 0)) -> I
  | Abs (_, App (_, x, Var (_, 0))) when not (free x) ->
      tr x |> shift
  | Abs (_, x) ->
      if not (free x) then
        app K (tr x |> shift)
      else (
        match x with
        | Abs (_, y) ->
            tr (abstract (tr x))
        | App (_,x,y) ->
            (*App (App (S, tr (Abs x)), tr (Abs y))*)
            let f1 = free x
            and f2 = free y in
            if not f1 then
              app (app B (tr x |> shift)) (tr (abstract y))
            else if not f2 then
              app (app C (tr (abstract x))) (tr y |> shift)
            else
              app (app S (tr (abstract x))) (tr (abstract y))
        | _ ->
            assert false
      )
  | t -> t

module Parser = struct
  include ParserCombinators(struct type store = string list end)

  let update f = fun s -> LazyList.singleton ((), { s with store = f s.store })

  let lookup v =
    let rec find i = function
      | [] -> failwith "not found"
      | v'::t ->
          if v = v' then
            i
          else
            find (i+1) t
    in
    fun s -> LazyList.singleton (find 0 s.store, s)

  let term =
    let rec pvar = lazy (ident_ >>= fun v -> var <$> lookup v)
    and pabstract = lazy (
      char_ '\\' >> many1 ident_ >>= fun vs ->
      let l = List.length vs in
      char_ '.' >>
      update (fun ctx -> List.fold_left (fun ctx v -> v::ctx) ctx vs) >>
      (nest l <$> Lazy.force term) <<
      update (List.drop l)
    )
    and term0 = lazy ((char_ '(' >> (fun s -> Lazy.force term s) << char_ ')' <|> Lazy.force pabstract <|> Lazy.force pvar))
    and term = lazy (List.fold_left1 app <$> many1 (Lazy.force term0))
    in
    Lazy.force term
end

let () =
  let n = read_int () in
  for i = 1 to n do
    let s = read_line () in
    match Parser.parse Parser.term [] s with
    | None -> ()
    | Some t -> tr t |> print; print_endline ""
  done

Infer

https://www.hackerrank.com/challenges/infer

http://okmij.org/ftp/ML/generalization.html Didier Rémy提出的加速generalization的算法。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472

module Str = struct
  let implode l =
    let s = Bytes.make (List.length l) ' ' in
    List.iteri (fun i c -> Bytes.set s i c) l;
    s
end

module LazyList = struct
  type 'a node = Nil | Cons of 'a * 'a t
  and 'a t = 'a node Lazy.t
  let empty = lazy Nil
  let singleton x = lazy (Cons (x, empty))
  let force = Lazy.force
  let rec map f l = lazy (
    match force l with
    | Nil -> Nil
    | Cons (h, t) -> Cons (f h, map f t)
  )
  let rec append l1 l2 = lazy (
    match force l1 with
    | Nil -> force l2
    | Cons (h, t) -> Cons (h, append t l2)
  )
  let rec concat ll = lazy (
    match force ll with
    | Nil -> Nil
    | Cons (h, t) -> append h (concat t) |> force
  )
  let is_empty l = force l = Nil
end

module ParserCombinators = struct
  type input = { s: bytes; pos: int }
  type 'a t = input -> ('a * input) LazyList.t
  let unit a s = LazyList.singleton (a, s)
  let zero = unit []
  let (>>=) (type a) (type b) (x : a t) (f : a -> b t) s =
    LazyList.map (fun (a,s) -> f a s) (x s) |> LazyList.concat
  let (>>) x y = x >>= fun _ -> y
  let (<<) x y = x >>= fun a -> y >> unit a
  let (<|>) x y s = let r = x s in if LazyList.is_empty r then y s else r
  let (<$>) f x = x >>= fun a -> unit (f a)
  let rec many x = many1 x <|> zero
  and many1 x = x >>= fun b -> many x >>= fun bs -> unit (b::bs)
  let sep_by x sep =
    let go = x >>= fun b ->
      many (sep >> x) >>= fun bs ->
      unit (b::bs)
    in
    go <|> zero
  let pred f s =
    if s.pos = Bytes.length s.s then
      LazyList.empty
    else
      let c = s.s.[s.pos] in
      if f c then unit c { s with pos = s.pos + 1 } else LazyList.empty
  let ident = Str.implode <$> many1 (pred (fun c ->
    'a'<=c&&c<='z' || 'A'<=c&&c<='Z' || '0'<=c&&c<='9' || c = '_'))
  let space = pred (fun c -> c = ' ' || c = '\t' || c = '\r' || c = '\n')
  let token x = x >>= fun a -> many space >> unit a
  let char c = pred ((=) c)
  let str cs =
    let rec go i =
      if i = Bytes.length cs then
        zero
      else
        char cs.[i] >> go (i+1)
    in
    go 0
  let ident_ = token ident
  let char_ c = token (char c)
  let str_ cs = token (str cs)
end

type expr =
  | Var of string
  | Fun of string list * expr
  | App of expr * expr list
  | Let of string * expr * expr
type level = int
type typ =
  | TConst of string
  | TVar of tv ref
  | TArrow of typ list * typ * levels
  | TApp of typ * typ list * levels
and tv = Unbound of int * level | Link of typ
and levels = { mutable level_old : level; mutable level_new : level }
let gray_level = -1
let generic_level = 19921213

let rec djs_find = function
  | TVar ({contents = Link t} as tv) ->
      let t = djs_find t in
      tv := Link t;
      t
  | t -> t

let get_level t =
  match djs_find t with
  | TConst _ -> 0
  | TVar ({contents = Unbound (_, l)}) -> l
  | TApp (_, _, ls)
  | TArrow (_, _, ls) -> ls.level_new
  | _ -> assert false

module Parser = struct
  include ParserCombinators
  let force = Lazy.force
  let generic_ctr = ref 0
  let tapp f args =
    let l = List.fold_left (fun acc a ->
      max acc (get_level a)) (get_level f) args in
    TApp (f, args, { level_old = l; level_new = l })
  let tarrow args r =
    let l = List.fold_left (fun acc a ->
      max acc (get_level a)) (get_level r) args in
    TArrow (args, r, { level_old = l; level_new = l })
  let typ () =
    let univ = Hashtbl.create 0 in
    let rec parse_ident =
      ident_ >>= fun n ->
      unit @@
        try TVar (ref @@ Link (Hashtbl.find univ n))
        with Not_found -> TConst n
    and parse_tys s = sep_by parse_ty (char_ ',') s
    and parse_ty s = (
      let t1 =
        let rec bracket f =
          (char_ '[' >> parse_tys << char_ ']' >>= fun args ->
          bracket (tapp f args)) <|> unit f
        in
        parse_ident >>= bracket >>= fun f ->
        (str_ "->" >> (fun s -> parse_ty s) >>= fun r ->
        unit @@ tarrow [f] r) <|> unit f
      in
      let t2 =
        char_ '(' >> parse_tys << char_ ')' >>= fun args ->
        (str_ "->" >> parse_ty >>= fun r ->
        unit @@ tarrow args r) <|> unit (List.hd args)
      in
      t1 <|> t2
    ) s
    and parse_top s = (
      (str_ "forall[" >> many ident_ << char_ ']' >>= fun vs ->
      List.iteri (fun i v ->
        decr generic_ctr;
        Hashtbl.replace univ v (TVar (Unbound (!generic_ctr, generic_level) |> ref))) vs;
      parse_ty) <|> parse_ty
    ) s
    in
    parse_top
  let expr =
    let rec parse_let s = (
      str_ "let" >> ident_ >>= fun n ->
      char_ '=' >> parse_expr >>= fun e ->
      str_ "in" >>
      parse_expr >>= fun b ->
      unit @@ Let (n, e, b)
    ) s
    and parse_fun s = (
      str_ "fun" >> many ident_ >>= fun args ->
      str_ "->" >> parse_expr >>= fun b ->
      unit @@ Fun (args, b)
    ) s
    and parse_simple_expr s = (
      let first = (char_ '(' >> parse_expr << char_ ')') <|>
        (ident_ >>= fun n -> unit @@ Var n)
      in
      let rec go a =
        (char_ '(' >> sep_by parse_expr (char_ ',') << char_ ')' >>= fun b ->
        go @@ App (a, b)) <|> unit a
      in
      first >>= go
    ) s
    and parse_expr s = (
      parse_let <|>
      parse_fun <|>
      parse_simple_expr
    ) s
    in
    parse_expr
  let eof s =
    if s.pos = Bytes.length s.s then
      LazyList.singleton ((), s)
    else
      LazyList.empty
  let parse x s =
    match force ((many space >> x << eof) { s; pos = 0 }) with
    | LazyList.Nil -> None
    | LazyList.Cons ((x, _), _) -> Some x
end

exception Cycle
exception Fail
exception Length
let gensym_ctr = ref 0
let gensym () =
  let n = !gensym_ctr in
  incr gensym_ctr;
  n
let reset_gensym () = gensym_ctr := 0
let cur_level = ref 0
let reset_level () = cur_level := 0
let enter_level () = incr cur_level
let leave_level () = decr cur_level
let new_var () = TVar (ref (Unbound (gensym (), !cur_level)))
let new_app f args = TApp (f, args, { level_new = !cur_level; level_old = !cur_level })
let new_arrow args r = TArrow (args, r, { level_new = !cur_level; level_old = !cur_level })

let adj_q = ref []
let reset_adj_q () = adj_q := []
let force_adj_q () =
  let rec go l acc t =
    match djs_find t with
    | TVar ({contents = Unbound (n, l')} as tv) ->
        if l < l' then
          tv := Unbound (n, l);
        acc
    | TApp (_, _, ls)
    | TArrow (_, _, ls) as t ->
        if ls.level_new = gray_level then
          raise Cycle;
        if l < ls.level_new then
          ls.level_new <- l;
        one acc t
    | _ -> acc
  and one acc = function
    | TApp (r, args, ls)
    | TArrow (args, r, ls) as t ->
        if ls.level_old <= !cur_level then
          t::acc
        else if ls.level_old = ls.level_new then
          acc
        else (
          let lvl = ls.level_new in
          ls.level_new <- gray_level;
          let acc = List.fold_left (go lvl) acc args in
          let acc = go lvl acc r in
          ls.level_new <- lvl;
          ls.level_old <- lvl;
          acc
        )
    | _ -> assert false
  in
  adj_q := List.fold_left one [] !adj_q

let rec update_level l = function
  | TConst _ ->
      ()
  | TVar ({contents = Unbound (n, l')} as tv) ->
      if l < l' then
        tv := Unbound (n, l)
  | TApp (_, _, ls)
  | TArrow (_, _, ls) as t ->
      if ls.level_new = gray_level then
        raise Cycle;
      if l < ls.level_new then (
        if ls.level_new = ls.level_old then
          adj_q := t :: !adj_q;
        ls.level_new <- l
      )
  | _ -> assert false

let rec unify t1 t2 =
  let t1 = djs_find t1 in
  let t2 = djs_find t2 in
  if t1 != t2 then
    match t1, t2 with
    | TConst t1, TConst t2 when t1 = t2 ->
        ()
    | TVar ({contents = Unbound (_, l)} as tv), t'
    | t', TVar ({contents = Unbound (_, l)} as tv) ->
        update_level l t';
        tv := Link t'
    | TApp (r1, args1, l1), TApp (r2, args2, l2)
    | TArrow (args1, r1, l1), TArrow (args2, r2, l2) ->
        if l1.level_new = gray_level || l2.level_new = gray_level then
          raise Cycle;
        if List.length args1 <> List.length args2 then
          raise Length;
        let lvl = min l1.level_new l2.level_new in
        l1.level_new <- gray_level;
        l2.level_new <- gray_level;
        List.iter2 (unify_level lvl) args1 args2;
        unify_level lvl r1 r2;
        l1.level_new <- lvl;
        l2.level_new <- lvl
    | _ -> raise Fail

and unify_level l t1 t2 =
  let t1 = djs_find t1 in
  update_level l t1;
  unify t1 t2

let gen t =
  let rec go t =
    match djs_find t with
    | TConst _ ->
        ()
    | TVar ({contents = Unbound (n, l)} as tv) ->
        if l > !cur_level then
          tv := Unbound (n, generic_level)
    | TApp (r, args, ls)
    | TArrow (args, r, ls) ->
        if ls.level_new > !cur_level then (
          List.iter go args;
          go r;
          let lvl = List.fold_left (fun acc a -> max acc (get_level a)) (get_level r) args in
          ls.level_new <- lvl;
          ls.level_old <- lvl
        )
    | _ -> assert false
  in
  force_adj_q ();
  go t

let inst t =
  let subst = Hashtbl.create 0 in
  let rec go = function
    | TVar {contents = Unbound (n, l)} when l = generic_level ->
        (try
          Hashtbl.find subst n
        with Not_found ->
          let tv = new_var () in
          Hashtbl.replace subst n tv;
          tv)
    | TVar {contents = Link t} ->
        go t
    | TApp (f, args, ls) when ls.level_new = generic_level ->
        new_app (go f) (List.map go args)
    | TArrow (args, r, ls) when ls.level_new = generic_level ->
        new_arrow (List.map go args) (go r)
    | t -> t
  in
  go t

let rec typeof env e =
  let rec go = function
    | Var x -> Hashtbl.find env x |> inst
    | Fun (args, e) ->
        let ty_args = List.map (fun x -> new_var ()) args in
        List.iter2 (Hashtbl.add env) args ty_args;
        let ty_e = go e in
        let r = new_arrow ty_args ty_e in
        List.iter (Hashtbl.remove env) args;
        r
    | App (e, args) ->
        let ty_fun = go e in
        let ty_args = List.map go args in
        let ty_res = new_var () in
        unify ty_fun (new_arrow ty_args ty_res);
        ty_res
    | Let (x, e1, e2) ->
        enter_level ();
        let ty_e1 = go e1 in
        leave_level ();
        gen ty_e1;
        Hashtbl.add env x ty_e1;
        let r = go e2 in
        Hashtbl.remove env x;
        r
  in
  go e

let rec check_cycle = function
  | TVar {contents = Link t} ->
      check_cycle t
  | TApp (r, args, ls)
  | TArrow (args, r, ls) ->
      if ls.level_new = gray_level then
        raise Cycle;
      let lvl = ls.level_new in
      ls.level_new <- gray_level;
      List.iter check_cycle args;
      check_cycle r;
      ls.level_new <- lvl
  | _ -> ()

let rec top_typeof env e =
  reset_gensym ();
  reset_level ();
  reset_adj_q ();
  let t = typeof env e in
  check_cycle t;
  t

let rec show t =
  let open Printf in
  let id2name = Hashtbl.create 0 in
  let rec go t =
    match djs_find t with
    | TConst n -> n
    | TVar ({contents = Unbound (n, _)}) ->
        (try
          Hashtbl.find id2name n
        with _ ->
          let i = Hashtbl.length id2name in
          let name = Char.chr (Char.code 'a' + i) |> String.make 1 in
          Hashtbl.replace id2name n name;
          name)
    | TApp (f, args, _) ->
        let u = go f in
        let v = String.concat ", " (List.map go args) in
        sprintf "%s[%s]" u v
    | TArrow (args, r, _) ->
        let f = function
          | TArrow _ -> false
          | _ -> true
        in
        let u = String.concat ", " (List.map go args) in
        let v = go r in
        if List.length args = 1 && f @@ djs_find (List.hd args) then
          sprintf "%s -> %s" u v
        else
          sprintf "(%s) -> %s" u v
    | _ -> assert false
  in
  let s = go t in
  let l = Hashtbl.length id2name in
  if l > 0 then (
    let vs = Hashtbl.fold (fun _ v l -> v::l) id2name [] |> List.sort compare in
    sprintf "forall[%s] %s" (String.concat " " vs) s
  ) else
    s

let extract = function
  | Some x -> x
  | None -> assert false

let core =
  [ "head", "forall[a] list[a] -> a"
  ; "tail", "forall[a] list[a] -> list[a]"
  ; "nil", "forall[a] list[a]"
  ; "cons", "forall[a] (a, list[a]) -> list[a]"
  ; "cons_curry", "forall[a] a -> list[a] -> list[a]"
  ; "map", "forall[a b] (a -> b, list[a]) -> list[b]"
  ; "map_curry", "forall[a b] (a -> b) -> list[a] -> list[b]"
  ; "one", "int"
  ; "zero", "int"
  ; "succ", "int -> int"
  ; "plus", "(int, int) -> int"
  ; "eq", "forall[a] (a, a) -> bool"
  ; "eq_curry", "forall[a] a -> a -> bool"
  ; "not", "bool -> bool"
  ; "true", "bool"
  ; "false", "bool"
  ; "pair", "forall[a b] (a, b) -> pair[a, b]"
  ; "pair_curry", "forall[a b] a -> b -> pair[a, b]"
  ; "first", "forall[a b] pair[a, b] -> a"
  ; "second", "forall[a b] pair[a, b] -> b"
  ; "id", "forall[a] a -> a"
  ; "const", "forall[a b] a -> b -> a"
  ; "apply", "forall[a b] (a -> b, a) -> b"
  ; "apply_curry", "forall[a b] (a -> b) -> a -> b"
  ; "choose", "forall[a] (a, a) -> a"
  ; "choose_curry", "forall[a] a -> a -> a"
  ]

let core_env =
  let env = Hashtbl.create 0 in
  List.iter (fun (var, typ) ->
    let t = Parser.parse (Parser.typ ()) typ |> extract in
    Hashtbl.replace env var t
  ) core;
  env

let type_check line =
  let env = Hashtbl.copy core_env in
  Parser.parse Parser.expr line |> extract |> top_typeof env

let () =
  read_line () |> type_check |> show |> print_endline