Comments

Signed-off-by: Anqur <[email protected]>

lyzh/__main__.py

@@ -1,3 +1,5 @@
+"""命令行入口."""
+
 import sys
 import typing
 
@@ -15,13 +17,15 @@ def fatal(m: str | Exception) -> typing.Never:
 
 
 ids = core.IDs()
-defs: core.Defs[cst.Expr] = []
+defs: core.Defs[cst.Expr] = []  # 尚未检查类型的定义
 
+# 获取文件名.
 try:
     _, file, *_ = sys.argv
 except ValueError:
     fatal("usage: lyzh FILE")
 
+# 加载源文件, 并解析出所有定义.
 try:
     with open(file) as f:
         grammar.prog(defs)(parsec.Source(f.read(), ids))
@@ -30,6 +34,7 @@ def fatal(m: str | Exception) -> typing.Never:
 except parsec.Error as e:
     fatal(f"{file}:{e}")
 
+# 解析所有定义中的引用, 并开始类型检查.
 try:
     well_typed = elab.Elaborator(ids).elaborate(resolve.Resolver().resolve(defs))
     print("\n\n".join(str(d) for d in well_typed))

lyzh/abstract/data.py

@@ -1,3 +1,5 @@
+"""Abstract syntax, 这个层级的值能够被深度求值, 但也可能是没法继续求值的形式, 即 normal form."""
+
 import dataclasses
 import typing
 
@@ -6,11 +8,15 @@
 
 @dataclasses.dataclass
 class Term:
+    """数值父类."""
+
     pass
 
 
 @dataclasses.dataclass
 class Ref(Term):
+    """变量引用."""
+
     v: core.Var
 
     def __str__(self):
@@ -19,6 +25,8 @@ def __str__(self):
 
 @dataclasses.dataclass
 class Univ(Term):
+    """类型宇宙."""
+
     pass
 
     def __str__(self):
@@ -27,6 +35,8 @@ def __str__(self):
 
 @dataclasses.dataclass
 class FnType(Term):
+    """函数类型."""
+
     p: core.Param[Term]
     body: Term
 
@@ -36,7 +46,9 @@ def __str__(self):
 
 @dataclasses.dataclass
 class Fn(Term):
-    p: core.Param[Term]
+    """函数."""
+
+    p: core.Param[Term]  # 此时函数的参数类型确定
     body: Term
 
     def __str__(self):
@@ -45,6 +57,8 @@ def __str__(self):
 
 @dataclasses.dataclass
 class App(Term):
+    """函数应用."""
+
     f: Term
     x: Term
 
@@ -53,5 +67,9 @@ def __str__(self):
 
 
 type Globals = typing.Dict[core.ID, core.Def[Term]]
+"""全局变量定义, 在学术中叫做 Sigma, ∑, 其实就是 global context."""
 
 type Locals = typing.Dict[core.ID, Term]
+"""本地变量定义, 在学术中叫做 Gamma, Γ (对, 论文里最常出现的那个), 其实就是 local context,
+注意这里的映射值的结构是 Term, 但实际上它只能是该变量的类型 (type term), 不能是一个值 (value
+term)."""

lyzh/abstract/normalize.py

@@ -1,3 +1,6 @@
+"""求值器, 将一个值转换为它的 normal form, 所谓 NbE (normalized by evaluation)
+就是在编译期间将可以计算的表达式通过求值 (evaluation) 转换为 normal form, 以供后续类型检查使用的算法理念."""
+
 import dataclasses
 import typing
 
@@ -10,12 +13,20 @@
 class Normalizer:
     ids: core.IDs
     globals: ast.Globals
+    # env 在学术里又叫做 rho, ρ, evaluation context, evaluation environment 等等,
+    # 要时刻注意这里的映射值的结构是 ast.Term, 和 ast.Locals 不同, 它可以是类型 (type term),
+    # 也可以是值 (value term), 因为这里要做的事情无非就是变量替换 (substitution).
+    #
+    # 所以, 根据惯例, 变量到变量类型的映射 (也就是 locals, Gamma, Γ) 我们习惯叫 context,
+    # 变量到值的映射 (也就是 env, pho, ρ) 我们叫 environment.
     env: typing.Dict[core.ID, ast.Term] = dataclasses.field(default_factory=dict)
 
     def term(self, tm: ast.Term) -> ast.Term:
+        """对单个值进行求值."""
         match tm:
             case ast.Ref(v):
                 try:
+                    # 进行变量替换, 并且刷新内部变量的引用.
                     return self.term(rename.Renamer(self.ids).rename(self.env[v.id]))
                 except KeyError:
                     return tm
@@ -24,26 +35,32 @@ def term(self, tm: ast.Term) -> ast.Term:
                 x = self.term(x)
                 match f:
                     case ast.Fn(p, b):
+                        # 将 b 里面 p.name 出现的地方替换为 x.
                         return self.subst((p.name, x), b)
                     case _:
                         return ast.App(f, x)
             case ast.Fn(p, b):
+                # 对参数类型和函数体求值, 并保持原样.
                 return ast.Fn(self.param(p), self.term(b))
             case ast.FnType(p, b):
+                # 对参数类型和函数类型体求值, 并保持原样.
                 return ast.FnType(self.param(p), self.term(b))
             case ast.Univ():
                 return tm
         raise AssertionError("impossible")
 
     def param(self, p: core.Param[ast.Term]) -> core.Param[ast.Term]:
+        """对参数类型求值."""
         return core.Param[ast.Term](p.name, self.term(p.type))
 
     def subst(self, m: typing.Tuple[core.Var, ast.Term], tm: ast.Term) -> ast.Term:
+        """提供一组映射, 并对 tm 进行求值."""
         (v, x) = m
         self.env[v.id] = x
         return self.term(tm)
 
     def apply(self, f: ast.Term, *args: ast.Term) -> ast.Term:
+        """模拟函数调用, 如果 f 是函数, 则不断用它的函数体进行变量替换."""
         ret = f
         for x in args:
             match f:
@@ -55,14 +72,16 @@ def apply(self, f: ast.Term, *args: ast.Term) -> ast.Term:
 
 
 def to_value(d: core.Def[ast.Term]) -> ast.Term:
+    """将一个定义转换为它的值形式."""
     ret = d.body
     for p in reversed(d.params):
-        ret = ast.Fn(p, ret)
+        ret = ast.Fn(p, ret)  # 参数不为空, 转成函数
     return ret
 
 
 def to_type(d: core.Def[ast.Term]) -> ast.Term:
+    """将一个定义转换为它的类型形式."""
     ret = d.ret
     for p in reversed(d.params):
-        ret = ast.FnType(p, ret)
+        ret = ast.FnType(p, ret)  # 参数不为空, 转成函数类型
     return ret

lyzh/abstract/rename.py

@@ -1,3 +1,8 @@
+"""数值内部引用刷新器, 这是因为, 我们使用了 capture-avoiding substitution 的技术,
+所有的定义检查完毕类型之后, 它就像一个 "模板" 存在于 global context 当中, 如果后续有其他定义引用,
+则我们应该把这个 "模板" 生成出来的数值内部的所有 ID 重新刷新, 不然的话, 引用会指向 "模板" 中去,
+造成严重错误 (比如程序陷入死循环)."""
+
 import dataclasses
 import typing
 
@@ -7,13 +12,17 @@
 
 @dataclasses.dataclass
 class Renamer:
+    """数值内部引用刷新器."""
+
     ids: core.IDs
     m: typing.Dict[core.ID, core.ID] = dataclasses.field(default_factory=dict)
 
     def rename(self, tm: ast.Term) -> ast.Term:
+        """刷新数值内部引用."""
         match tm:
             case ast.Ref(v):
                 try:
+                    # 用旧的 ID 替换成新的 ID.
                     return ast.Ref(core.Var(v.text, self.m[v.id]))
                 except KeyError:
                     return tm
@@ -28,6 +37,7 @@ def rename(self, tm: ast.Term) -> ast.Term:
         raise AssertionError("impossible")
 
     def param(self, p: core.Param[ast.Term]) -> core.Param[ast.Term]:
+        """将参数赋予新的 ID 放入映射, 并刷新参数类型."""
         name = self.ids.rename(p.name)
-        self.m[p.name.id] = name.id
+        self.m[p.name.id] = name.id  # 后续遇到旧的 ID 会被替换成新的 ID
         return core.Param[ast.Term](name, self.rename(p.type))

lyzh/abstract/unify.py

@@ -1,3 +1,5 @@
+"""相等检查器, 即执行 unification 算法, 又叫做 conversion checking."""
+
 import dataclasses
 
 import lyzh.abstract.data as ast
@@ -7,6 +9,8 @@
 
 @dataclasses.dataclass
 class Unifier:
+    """相等检查器."""
+
     ids: core.IDs
     globals: ast.Globals
 
@@ -17,10 +21,12 @@ def unify(self, lhs: ast.Term, rhs: ast.Term) -> bool:
             case ast.App(f, x), ast.App(g, y):
                 return self.unify(f, g) and self.unify(x, y)
             case ast.Fn(p, b), ast.Fn(q, c):
+                # 将 c 内部的 q 替换成 p 后和 b 检查是否相等.
                 return self.unify(b, self.nf().subst((q.name, ast.Ref(p.name)), c))
             case ast.FnType(p, b), ast.FnType(q, c):
                 if not self.unify(p.type, q.type):
                     return False
+                # 将 c 内部的 q 替换成 p 后和 b 检查是否相等.
                 return self.unify(b, self.nf().subst((q.name, ast.Ref(p.name)), c))
             case ast.Univ(), ast.Univ():
                 return True

lyzh/concrete/data.py

@@ -1,41 +1,57 @@
+"""Concrete syntax, 这里的定义携带了位置信息, 并且可以用于深入求值计算."""
+
 import dataclasses
 
 import lyzh.core as core
 
 
 @dataclasses.dataclass
 class Expr:
+    """表达式父类."""
+
     loc: core.Loc
 
 
 @dataclasses.dataclass
 class Fn(Expr):
-    v: core.Var
+    """Function, 函数表达式, 也就是 lambda 表达式."""
+
+    v: core.Var  # 只有名字, 不需要标明类型
     body: Expr
 
 
 @dataclasses.dataclass
 class App(Expr):
+    """Function application, 函数应用表达式."""
+
     f: Expr
     x: Expr
 
 
 @dataclasses.dataclass
 class FnType(Expr):
+    """Function type, 函数类型表达式, 也就是学术里的 Pi type 和 dependent function type."""
+
     p: core.Param
     body: Expr
 
 
 @dataclasses.dataclass
 class Univ(Expr):
+    """Universe, 类型宇宙表达式, 也就是学术里的 type of type, 类型的类型."""
+
     pass
 
 
 @dataclasses.dataclass
 class Unresolved(Expr):
+    """未进行作用域检查的变量引用表达式."""
+
     v: core.Var
 
 
 @dataclasses.dataclass
 class Resolved(Expr):
+    """通过作用域检查后的变量引用表达式."""
+
     v: core.Var