Luna Flow
简体中文

适配器教程

本教程将你自己的表达式类型接入 type_theory。你将为一个小型 AST 实现 @syntax.BindingSyntax，然后直接在其上使用泛型的自由变量计算、避免捕获的代换和改写，而无需转换为 Term[T]。最后你将测试适配器定律。

快速入门

moon add Luna-Flow/type_theory@0.2.0
import {
  "Luna-Flow/type_theory/core",
  "Luna-Flow/type_theory/syntax",
  "Luna-Flow/type_theory/substitution",
  "Luna-Flow/type_theory/rewrite",
}

下面是一个包含数字、运算符符号、变量、调用和绑定子 Fun(x, body) 的表达式语言，以及它的适配器：

priv enum Expr {
  Num(Int)
  Sym(String)
  Var(@core.Name)
  Call(Expr, Array[Expr])
  Fun(@core.Name, Expr)
} derive(Eq, Debug)

impl @syntax.BindingSyntax for Expr with fn project(self) {
  match self {
    Num(_) | Sym(_) => Opaque
    Var(x) => Variable(x)
    Call(f, args) => Apply(f, args)
    Fun(x, body) => Bind(x, body)
  }
}

impl @syntax.BindingSyntax for Expr with fn variable(x) {
  Var(x)
}

impl @syntax.BindingSyntax for Expr with fn apply(f, args) {
  Call(f, args)
}

impl @syntax.BindingSyntax for Expr with fn bind(x, body) {
  Fun(x, body)
}

test "quick start: free variables of an Expr" {
  let x = @core.Name::new("x")
  let y = @core.Name::new("y")
  let e = Fun(x, Call(Sym("+"), [Var(x), Var(y)]))
  let fv = @syntax.generic_free_variables(e)
  assert_true(fv.contains(y))
  assert_false(fv.contains(x))
}

数字和运算符符号投影为 Opaque，因为它们不含变量。该类型是 priv 的，因为这个示例只存在于单个包中；导出其 AST 的库应将它设为 pub(all)，并用 pub extend 声明它所提升的方法。调用的运算符就是它的头部，因此重建调用时会保留运算符。

日常任务

无捕获地代换

GenericSubstitution::apply_once 替换自由变量，并在必要时重命名 Fun 绑定子：

test "capture-avoiding substitution on Expr" {
  let x = @core.Name::new("x")
  let y = @core.Name::new("y")
  let e = Fun(y, Call(Sym("+"), [Var(x), Var(y)]))
  let s = @substitution.GenericSubstitution::singleton(x, Var(y))
  let y1 = @core.Name::new("y_1")
  assert_eq(s.apply_once(e), Fun(y1, Call(Sym("+"), [Var(y), Var(y1)])))
}

部分求值

代入已知的值，其余部分保持符号形式：

test "partial evaluation on Expr" {
  let x = @core.Name::new("x")
  let y = @core.Name::new("y")
  let e = Call(Sym("*"), [Var(x), Var(y)])
  let known = @substitution.GenericSubstitution::singleton(x, Num(3))
  assert_eq(known.apply_once(e), Call(Sym("*"), [Num(3), Var(y)]))
}

用改写规则化简

针对你自己的类型编写规则，让泛型遍历找出它们适用的位置：

fn fold_add(e : Expr) -> Expr? {
  match e {
    Call(Sym("+"), [Num(a), Num(b)]) => Some(Num(a + b))
    _ => None
  }
}

test "constant folding on Expr" {
  let x = @core.Name::new("x")
  let e = Call(Sym("*"), [Var(x), Call(Sym("+"), [Num(1), Call(Sym("+"), [Num(2), Num(3)])])])
  let rule = @rewrite.RuleName::unsafe_new("fold_add")
  assert_eq(
    @rewrite.generic_normalize(e, rule, fold_add, 10),
    NormalForm(term=Call(Sym("*"), [Var(x), Num(6)]), steps=2),
  )
  match @rewrite.generic_top_down_once(e, rule, fold_add) {
    Reduced(path~, ..) =>
      assert_eq(path.to_array(), [@rewrite.ApplyArgument(1), @rewrite.ApplyArgument(1)])
    NoStep => fail("expected a step")
  }
}

该路径表示：* 的第二个参数，然后是外层 + 的第二个参数。

重命名绑定子

generic_alpha_rename_bound 重命名绑定子体中的变量，并拒绝已被使用的名字：

test "rename a Fun parameter" {
  let x = @core.Name::new("x")
  let y = @core.Name::new("y")
  let z = @core.Name::new("z")
  let body = Call(Sym("+"), [Var(x), Var(y)])
  assert_true(@syntax.generic_alpha_rename_bound(body, x, y) is None)
  assert_eq(
    @syntax.generic_alpha_rename_bound(body, x, z),
    Some(Call(Sym("+"), [Var(z), Var(y)])),
  )
}

进阶

测试适配器定律

只有当 project 与构造器保持一致（即适配器设计中的视图定律）时，泛型算法才是正确的。请在有代表性的节点上测试它们：

fn rebuild(e : Expr) -> Expr {
  match @syntax.BindingSyntax::project(e) {
    Opaque => e
    Variable(x) => @syntax.BindingSyntax::variable(x)
    Apply(f, args) => @syntax.BindingSyntax::apply(f, args)
    Bind(x, body) => @syntax.BindingSyntax::bind(x, body)
  }
}

test "view laws" {
  let x = @core.Name::new("x")
  let samples = [
    Num(1),
    Sym("+"),
    Var(x),
    Call(Sym("+"), [Var(x), Num(2)]),
    Fun(x, Var(x)),
  ]
  for e in samples {
    assert_eq(rebuild(e), e)
    if @syntax.BindingSyntax::project(e) is Opaque {
      assert_eq(@syntax.generic_free_variables(e).length(), 0)
    }
  }
}

一个视图情形下的多个运算符

所有调用都投影为 Apply，运算符随头部一起传递，因此 apply(head, args) 可以重建任何调用。如果你的 AST 有 Add(a, b) 和 Mul(a, b) 这样彼此独立的节点种类，就给它们一个能标识种类的头部（就像这里的 Sym）；否则 apply 无法知道应重建哪种节点。

桥接你的变量类型

如果你的 AST 有自己的变量类型，请在 project 中将其单射地映射到 @core.Name（不同的变量对应不同的名字），并在 variable 中映射回来。

常见陷阱

  • 不透明节点中的变量。 投影为 Opaque 的节点从不被搜索。如果其中含有变量，代换会遗漏它们。
  • 用点语法调用 trait 方法。 请写成 @syntax.BindingSyntax::project(e)；这些方法形式没有被提升。
  • 在 apply 中丢失节点种类。 如果两种节点都投影为 Apply，而头部又不能区分它们，重建就会改变 AST。
  • 期望重复代换。 apply_once 只代换一次；如果替换项中提到了定义域中的名字，请自行迭代。

后续步骤