Path-Iter

基于路径语义的 cocategory 枚举库

基于论文 Cocategory Enumeration 的实现。

有关路径语义的介绍，请参阅 此论文。

路径语义中的子类型

在正常的路径语义中，在定理证明中使用 正常路径。正常路径是从具有子类型的函数中派生出来的。

此库专注于子类型，而不是更一般的正常路径的情况。

路径语义中的子类型写成以下形式

x : [f] a

其中 x 是某个输入，f 是一个函数，a 是 f 的输出。

此库用于高效地枚举此类子类型。

示例：AND

使用 path! 宏以路径语义的标准表示法进行编写。它使用实现 IntoIterator 的 Path 构造一个类型。

use path_iter::*;

fn main() {
    for a in path!([And] true) {
        // Prints `(true, true)`
        println!("{:?}", a);
    }
}

它打印 (true, true)，因为这是 And 的唯一输入值，产生 true 作为输出。

示例：AND 2

您可以在运行时决定输出值

use path_iter::*;

fn main() {
    for &b in &[false, true] {
        for a in path!([And] b) {
            println!("{:?}", a);
        }
        println!("");
    }
}

这将打印

(false, false)
(false, true)
(true, false)

(true, true)

示例：AND-NOT

您可以连接路径子类型

use path_iter::*;

fn main() {
    for a in path!([And] [Not] true) {
        println!("{:?}", a);
    }
}

示例：偏应用

偏应用是一种技术，当调用时使用比签名 fewer 的参数时，函数减少到另一个函数。

例如，And(true) 减少到 Idb。

use path_iter::*;

fn main() {
   for a in path!([And(true)] true) {
        println!("{:?}", a);
    }
}

use path_iter::*;

fn main() {
    for a in path!([((And, And), (And, And)), (And, And), And] true) {
        println!("{:?}", a);
    }
}