rewrite API

rewrite 包在项的某一个位置应用一条重写规则，并准确报告发生了什么：之前与之后的项、规则名，以及从根到被重写位置的路径。有界范式化与轨迹都是通过重复这样的单步构建的。每个函数都有 Term[T] 版本，并在注明处提供适用于任意 @syntax.BindingSyntax AST 的版本。

import {
  "Luna-Flow/type_theory/syntax",
  "Luna-Flow/type_theory/rewrite",
}

规则是一个函数 (Term[T]) -> Term[T]?，当它作为整体适用于某个项时返回 Some(result)，否则返回 None。遍历函数决定在何处尝试规则。相关理论见 rewrite 设计。

规则名

`RuleName`

RuleName 是归约规则的非空标识符。

pub struct RuleName {
  value : String
} derive(Compare, Eq, Hash, @debug.Debug)

规则名用于在结果和轨迹中标记步骤。它们按文本进行比较、排序和哈希；顺序为 String 的顺序：较短的文本在前，然后按 UTF-16 码元比较。

`RuleName::new`

RuleName::new 验证并创建一个规则名。

pub fn RuleName::new(String) -> Result[Self, RuleNameError]

对空字符串返回 Err(RuleNameError::Empty)，否则返回 Ok(name)。

`RuleName::unsafe_new`

RuleName::unsafe_new 从已知非空的字符串创建规则名。

pub fn RuleName::unsafe_new(String) -> Self

遇到空字符串时中止。对 "beta" 这类不变式显而易见的字面量使用它；对来自输入的名字使用 RuleName::new。

`RuleName::value`

RuleName::value 返回规则名的文本。

pub fn RuleName::value(Self) -> String

`RuleName::equal`, `RuleName::compare`, `RuleName::hash`

这些方法是提升的 Eq、Compare 和 Hash 实现。

pub fn RuleName::equal(Self, Self) -> Bool
pub fn RuleName::compare(Self, Self) -> Int
pub fn RuleName::hash(Self) -> Int

test "rule names" {
  assert_eq(@rewrite.RuleName::new(""), Err(@rewrite.RuleNameError::Empty))
  match @rewrite.RuleName::new("beta") {
    Ok(name) => inspect(name.value(), content="beta")
    Err(_) => fail("non-empty name rejected")
  }
  // shortlex order: shorter names first
  let eta = @rewrite.RuleName::unsafe_new("eta")
  assert_true(eta < @rewrite.RuleName::unsafe_new("beta"))
}

`RuleNameError`

RuleNameError 列出规则名无效的原因。

pub(all) enum RuleNameError {
  Empty
} derive(Eq, @debug.Debug)
pub fn RuleNameError::equal(Self, Self) -> Bool

Empty 是唯一的情形：规则名不得为空。

位置

`ReductionFrame`

ReductionFrame 是从一个节点到其某个子节点的一步。

pub(all) enum ReductionFrame {
  BinderBody
  ApplyHead
  ApplyArgument(Int)
} derive(Eq, @debug.Debug)
pub fn ReductionFrame::equal(Self, Self) -> Bool

BinderBody 进入 Bind 的体，ApplyHead 进入 Apply 的头部，ApplyArgument(i) 进入其第 i 个参数（从 0 开始计数）。

`ReductionPath`

ReductionPath 是从根到某个位置的帧序列。

pub struct ReductionPath {
  frames : Array[ReductionFrame]
} derive(Eq, @debug.Debug)

空路径即根。

`ReductionPath::root`, `ReductionPath::prepend`, `ReductionPath::to_array`

这些函数构造和读取路径。

pub fn ReductionPath::root() -> Self
pub fn ReductionPath::prepend(Self, ReductionFrame) -> Self
pub fn ReductionPath::to_array(Self) -> Array[ReductionFrame]

prepend(frame) 在根端添加一帧，遍历正是借此把子节点中某一步的路径提升到父节点。to_array 返回以根开头的帧。

`ReductionPath::equal`

ReductionPath::equal 逐帧比较两条路径。

pub fn ReductionPath::equal(Self, Self) -> Bool

test "paths are built from the redex up" {
  let path = @rewrite.ReductionPath::root()
    .prepend(@rewrite.ApplyArgument(1))
    .prepend(@rewrite.BinderBody)
  assert_eq(path.to_array(), [@rewrite.BinderBody, @rewrite.ApplyArgument(1)])
  assert_eq(@rewrite.ReductionPath::root().to_array(), [])
}

`Term` 上的单步

`StepResult`

StepResult[T] 是一次归约尝试的结果。

pub(all) enum StepResult[T] {
  NoStep
  Reduced(before~ : @syntax.Term[T], after~ : @syntax.Term[T], rule~ : RuleName, path~ : ReductionPath)
} derive(Eq, @debug.Debug)
pub fn[T : Eq] StepResult::equal(Self[T], Self[T]) -> Bool

NoStep 表示遍历没有找到规则适用的位置。Reduced 记录整个项 before、整个项 after、规则以及被重写位置的路径。恰好有一个位置被重写：before 在 path 处的子项是该规则的可约式，而 after 是将该子项替换为规则结果后的 before。

`top_down_once`

top_down_once 按前序重写规则适用的第一个位置。

pub fn[T] top_down_once(@syntax.Term[T], RuleName, (@syntax.Term[T]) -> @syntax.Term[T]?) -> StepResult[T]

规则先在节点本身上尝试，再在其子节点上尝试；子节点的访问顺序是先头部，再从左到右依次访问参数，并且会进入绑定子的体。所选位置是最左最外的可约式。NoStep 表示该规则在项中任何位置都不适用。

`bottom_up_once`

bottom_up_once 按后序遍历，改写规则适用的第一个位置。

pub fn[T] bottom_up_once(@syntax.Term[T], RuleName, (@syntax.Term[T]) -> @syntax.Term[T]?) -> StepResult[T]

子节点先于其父节点尝试，顺序同样是从左到右。所选位置是最左最内的可约式。NoStep 同样表示该规则在任何位置都不适用。

fn drop_zero(t : @syntax.Term[String]) -> @syntax.Term[String]? {
  match t {
    Apply(Value("+"), [Value("0"), other]) => Some(other)
    _ => None
  }
}

test "outermost versus innermost" {
  let rule = @rewrite.RuleName::unsafe_new("drop_zero")
  let inner : @syntax.Term[String] = Apply(Value("+"), [Value("0"), Value("1")])
  let outer : @syntax.Term[String] = Apply(Value("+"), [Value("0"), inner])
  match @rewrite.top_down_once(outer, rule, drop_zero) {
    Reduced(after~, path~, ..) => {
      assert_eq(after, inner)
      assert_eq(path.to_array(), [])
    }
    NoStep => fail("expected a step")
  }
  match @rewrite.bottom_up_once(outer, rule, drop_zero) {
    Reduced(after~, path~, ..) => {
      assert_eq(after, Apply(Value("+"), [Value("0"), Value("1")]))
      assert_eq(path.to_array(), [@rewrite.ApplyArgument(1)])
    }
    NoStep => fail("expected a step")
  }
}

在 `Term` 上重复执行步骤

`NormalizationResult`

NormalizationResult[T] 是对步进函数进行有界重复的结果。

pub(all) enum NormalizationResult[T] {
  NormalForm(term~ : @syntax.Term[T], steps~ : Int)
  StepLimitReached(term~ : @syntax.Term[T], steps~ : Int)
} derive(Eq, @debug.Debug)
pub fn[T : Eq] NormalizationResult::equal(Self[T], Self[T]) -> Bool

NormalForm(term, steps)：步进函数在 term 上返回 NoStep，该项是经过 steps 步得到的。StepLimitReached(term, steps)：steps 步的上限已用尽，且 term 仍可继续归约。

`normalize`

normalize 反复应用步进函数，直到它返回 NoStep 或达到步数上限。

pub fn[T] normalize(@syntax.Term[T], (@syntax.Term[T]) -> StepResult[T], Int) -> NormalizationResult[T]

normalize(term, step, max_steps) 至多执行 max_steps 个成功步骤，并且至多调用 step max_steps + 1 次：在最后一个允许的步骤之后，它会再调用一次 step，以判定结果是 NormalForm 还是 StepLimitReached。当 max_steps <= 0 时，它不执行任何步骤，只对 term 进行分类。归约策略由步进函数决定；现成的步进函数见 eval。

`ReductionTrace`

ReductionTrace[T] 记录一次有界运行：初始项、每个成功的步骤以及最终结果。

pub struct ReductionTrace[T] {
  initial : @syntax.Term[T]
  steps : Array[StepResult[T]]
  result : NormalizationResult[T]
} derive(Eq, @debug.Debug)
pub fn[T] ReductionTrace::initial(Self[T]) -> @syntax.Term[T]
pub fn[T] ReductionTrace::steps(Self[T]) -> Array[StepResult[T]]
pub fn[T] ReductionTrace::result(Self[T]) -> NormalizationResult[T]
pub fn[T : Eq] ReductionTrace::equal(Self[T], Self[T]) -> Bool

steps 中的每个元素都是一个 Reduced 值；相邻步骤首尾相接，前一步的 after 即后一步的 before。steps().length() 等于 result 中的 steps 计数。steps() 返回一个副本。

`trace`

trace 运行与 normalize 相同的循环，并记录每一步。

pub fn[T] trace(@syntax.Term[T], (@syntax.Term[T]) -> StepResult[T], Int) -> ReductionTrace[T]

fn decrement(t : @syntax.Term[Int]) -> @syntax.Term[Int]? {
  match t {
    Value(n) if n > 0 => Some(Value(n - 1))
    _ => None
  }
}

test "normalize and trace" {
  let rule = @rewrite.RuleName::unsafe_new("decrement")
  let step = (t : @syntax.Term[Int]) => @rewrite.top_down_once(t, rule, decrement)
  assert_eq(
    @rewrite.normalize(Value(3), step, 10),
    NormalForm(term=Value(0), steps=3),
  )
  let run = @rewrite.trace(Value(3), step, 2)
  assert_eq(run.steps().length(), 2)
  assert_eq(run.result(), StepLimitReached(term=Value(1), steps=2))
  assert_eq(run.initial(), Value(3))
}

感知绑定的 AST

`GenericStepResult`

GenericStepResult[N] 是针对下游 AST N 的 StepResult。

pub(all) enum GenericStepResult[N] {
  NoStep
  Reduced(before~ : N, after~ : N, rule~ : RuleName, path~ : ReductionPath)
} derive(Eq, @debug.Debug)
pub fn[N : Eq] GenericStepResult::equal(Self[N], Self[N]) -> Bool

`generic_top_down_once`

generic_top_down_once 是适用于任意 BindingSyntax AST 的 top_down_once。

pub fn[N : @syntax.BindingSyntax] generic_top_down_once(N, RuleName, (N) -> N?) -> GenericStepResult[N]

遍历使用 BindingSyntax::project 查找子节点，并使用 trait 的构造函数重建被改写节点的各级父节点。Opaque 节点和变量节点没有子节点；规则仍会在它们上面尝试。

`GenericNormalizationResult`

GenericNormalizationResult[N] 是针对下游 AST 的 NormalizationResult。

pub(all) enum GenericNormalizationResult[N] {
  NormalForm(term~ : N, steps~ : Int)
  StepLimitReached(term~ : N, steps~ : Int)
} derive(Eq, @debug.Debug)
pub fn[N : Eq] GenericNormalizationResult::equal(Self[N], Self[N]) -> Bool

`generic_normalize`

generic_normalize 使用同一条规则重复执行 generic_top_down_once，直到没有步骤可用或达到步数上限。

pub fn[N : @syntax.BindingSyntax] generic_normalize(N, RuleName, (N) -> N?, Int) -> GenericNormalizationResult[N]

它与 normalize 遵循相同的步数约定，只是策略固定为自顶向下。

test "generic rewriting on Term" {
  let rule = @rewrite.RuleName::unsafe_new("drop_zero")
  let inner : @syntax.Term[String] = Apply(Value("+"), [Value("0"), Value("1")])
  let outer : @syntax.Term[String] = Apply(Value("+"), [Value("0"), inner])
  assert_eq(
    @rewrite.generic_normalize(outer, rule, drop_zero, 10),
    NormalForm(term=Value("1"), steps=2),
  )
}

关于下游 AST，请参阅适配器教程。

rewrite API

规则名

RuleName

RuleName::new

RuleName::unsafe_new

RuleName::value

RuleName::equal, RuleName::compare, RuleName::hash

RuleNameError

位置

ReductionFrame

ReductionPath

ReductionPath::root, ReductionPath::prepend, ReductionPath::to_array

ReductionPath::equal

Term 上的单步

StepResult

top_down_once

bottom_up_once

在 Term 上重复执行步骤

NormalizationResult

normalize

ReductionTrace

trace