implies：用于逻辑公式的Pybound Rust包

implies 是一个 Rust 包，用于将逻辑公式存储为解析树并在其上进行复杂操作，如替换、旋转、转换为合取范式等。命题逻辑已预先实现，但此包在通用的 struct Formula<B,U,A> 上运行，该 struct 可以轻松地与您自己的 Binary 和 Unary 操作符以及 Atomic 公式类型一起使用：如果您可以为您的首选逻辑（模态、时态、谓词等）实现这些类型，则可以为此语言使用此包的完整功能。有关此包的更多信息，请参阅文档。

存在命题逻辑的Python绑定，但使用Python API提供的控制性和灵活性要小得多。如果需要，可以通过在编译时启用"python"功能来使用Rust的Python API，这将添加"pyo3"作为依赖项。

以下是一个使用implies实现基本模态逻辑的简单示例，以便您了解如何轻松地使用implies为您的逻辑语言

use crate::formula::*;
use crate::parser::Match;
use crate::prop::*;
use crate::symbol::{Atom, Symbolic};

/// The usual unary operators for modal logic: negation,
/// box and diamond. Most of the traits you need to get your
/// symbol types to work with implies are derivable.
///
/// Pro tip:
/// Write operator enums like this in the ascending precedence order
/// want for your operators, so that deriving Ord freely gives you the
/// precedence you expect. In the case of unary operators like these,
/// it doesn't matter, but it's useful for binary operators.
#[derive(PartialEq, Eq, Ord, PartialOrd, Copy, Clone, Default, Hash)]
enum ModalUnary {
    Box,
    Diamond,
    // Give any value as the default, it just allows
    // fast swap operations under the hood without
    // unsafe Rust.
    #[default]
    Not,
}

/// Specify how your type should be pretty-printed.
impl std::fmt::Display for ModalUnary {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            ModalUnary::Box => write!(f, "◻"),
            ModalUnary::Diamond => write!(f, "◊"),
            ModalUnary::Not => write!(f, "¬"),
        }
    }
}

/// This marker trait shows you've covered all the bases.
impl Symbolic for ModalUnary {}

/// Implement this simple trait (whose methods are partial inverses)
/// for immediate access to parsing formulae from strings.
impl Match for ModalUnary {
    fn match_str(s: &str) -> Option<Self> {
        match s {
            "◻" => Some(ModalUnary::Box),
            "◊" => Some(ModalUnary::Diamond),
            "¬" | "not" | "~" => Some(ModalUnary::Not),
            _ => None,
        }
    }

    fn get_matches(&self) -> Vec<String> {
        match self {
            ModalUnary::Box => vec!["◻".to_owned()],
            ModalUnary::Diamond => vec!["◊".to_owned()],
            ModalUnary::Not => vec!["¬".to_owned(), "not".to_owned(), "~".to_owned()],
        }
    }
}

/// The binary operators for modal logic are the same as those for propositional.
type ModalBinary = PropBinary;

/// Just write a type alias and that's it, all of implies' functionality for free.
type ModalFormula = Formula<ModalBinary, ModalUnary, Atom>;

一旦设置了类似 ModalFormula 的类型，就可以免费使用Formula struct中提供的所有方法。要初始化公式，您可以从原子开始

let mut f = ModalFormula::new(Atom("p"))  // p

或使用级联宏进行构建器语法

let mut f = cascade! {
  let f = ModalFormula::new(Atom("p"))   // p
  ..unify(ModalUnary::Box)               // ◻p
  ..left_combine(PropBinary::Implies, ModalFormula::new(Atom("q"))) // q -> ◻p
}

或如果您的类型实现了 Match，则可以使用字符串！

use implies::parser::build_formula;

let mut f: ModalFormula = build_formula("q -> ◻p")?;