| Name | implies JSON |
| Version |
0.4.5
JSON |
| download |
| home_page | None |
| Summary | A parser for logical formulas |
| upload_time | 2024-01-26 21:50:28 |
| maintainer | None |
| docs_url | None |
| author | None |
| requires_python | |
| license | MIT |
| keywords |
logic
binary_tree
tree
graph
|
| VCS |
 |
| bugtrack_url |
|
| requirements |
No requirements were recorded.
|
| Travis-CI |
No Travis.
|
| coveralls test coverage |
No coveralls.
|
# implies: a Pybound Rust crate for logical formulas
**implies** is a Rust crate for storing logical formulas as parse trees and performing complex operations on them,
like substitution, rotation, conversion to conjunctive normal form, and more. Propositional logic comes pre-implemented,
but this crate operates on a generic struct `Formula<B,U,A>` which can easily be used with your own `B`inary and `U`nary
operators and `Atom`ic formula types: if you can implement those types for your own preferred logic (modal, temporal,
predicate, etc...) you can use the full functionality of this crate for your own language. A lot more information is in
the [docs](https://docs.rs/implies/0.2.1-alpha/implies) for this crate.
There are Python bindings for propositional logic, but using the API in Python gives much less control and flexibility.
You can use the Python APIs from Rust if you want by enabling the "python" feature when compiling, which will add "pyo3" as a dependency.
Here is a simple example of implementing a basic modal logic with implies, so you can see how easily you can use implies for your own logical language:
```rust
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>;
```
Once you have a type like `ModalFormula` set up, you can just use all the provided methods
in the Formula struct for free. To initialize a formula you can start with just an atom
```rust
let mut f = ModalFormula::new(Atom("p")) // p
```
or use the cascade macro for builder syntax
```rust
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
}
```
or if your type implements `Match` just use a string!
```rust
use implies::parser::build_formula;
let mut f: ModalFormula = build_formula("q -> ◻p")?;
```
Raw data
{
"_id": null,
"home_page": null,
"name": "implies",
"maintainer": null,
"docs_url": null,
"requires_python": "",
"maintainer_email": null,
"keywords": "logic,binary_tree,tree,graph",
"author": null,
"author_email": null,
"download_url": "https://files.pythonhosted.org/packages/56/5d/0e15947f489ae2daebac67488f102bc620551f507fe03b6319773c6102ef/implies-0.4.5.tar.gz",
"platform": null,
"description": "# implies: a Pybound Rust crate for logical formulas\n\n**implies** is a Rust crate for storing logical formulas as parse trees and performing complex operations on them,\nlike substitution, rotation, conversion to conjunctive normal form, and more. Propositional logic comes pre-implemented, \nbut this crate operates on a generic struct `Formula<B,U,A>` which can easily be used with your own `B`inary and `U`nary\noperators and `Atom`ic formula types: if you can implement those types for your own preferred logic (modal, temporal, \npredicate, etc...) you can use the full functionality of this crate for your own language. A lot more information is in\nthe [docs](https://docs.rs/implies/0.2.1-alpha/implies) for this crate.\n\nThere are Python bindings for propositional logic, but using the API in Python gives much less control and flexibility.\nYou can use the Python APIs from Rust if you want by enabling the \"python\" feature when compiling, which will add \"pyo3\" as a dependency.\n\nHere is a simple example of implementing a basic modal logic with implies, so you can see how easily you can use implies for your own logical language:\n\n```rust\nuse crate::formula::*;\nuse crate::parser::Match;\nuse crate::prop::*;\nuse crate::symbol::{Atom, Symbolic};\n\n/// The usual unary operators for modal logic: negation,\n/// box and diamond. Most of the traits you need to get your\n/// symbol types to work with implies are derivable.\n///\n/// Pro tip:\n/// Write operator enums like this in the ascending precedence order\n/// want for your operators, so that deriving Ord freely gives you the\n/// precedence you expect. In the case of unary operators like these,\n/// it doesn't matter, but it's useful for binary operators.\n#[derive(PartialEq, Eq, Ord, PartialOrd, Copy, Clone, Default, Hash)]\nenum ModalUnary {\n Box,\n Diamond,\n // Give any value as the default, it just allows\n // fast swap operations under the hood without\n // unsafe Rust.\n #[default]\n Not,\n}\n\n/// Specify how your type should be pretty-printed.\nimpl std::fmt::Display for ModalUnary {\n fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {\n match self {\n ModalUnary::Box => write!(f, \"\u25fb\"),\n ModalUnary::Diamond => write!(f, \"\u25ca\"),\n ModalUnary::Not => write!(f, \"\u00ac\"),\n }\n }\n}\n\n/// This marker trait shows you've covered all the bases.\nimpl Symbolic for ModalUnary {}\n\n/// Implement this simple trait (whose methods are partial inverses)\n/// for immediate access to parsing formulae from strings.\nimpl Match for ModalUnary {\n fn match_str(s: &str) -> Option<Self> {\n match s {\n \"\u25fb\" => Some(ModalUnary::Box),\n \"\u25ca\" => Some(ModalUnary::Diamond),\n \"\u00ac\" | \"not\" | \"~\" => Some(ModalUnary::Not),\n _ => None,\n }\n }\n\n fn get_matches(&self) -> Vec<String> {\n match self {\n ModalUnary::Box => vec![\"\u25fb\".to_owned()],\n ModalUnary::Diamond => vec![\"\u25ca\".to_owned()],\n ModalUnary::Not => vec![\"\u00ac\".to_owned(), \"not\".to_owned(), \"~\".to_owned()],\n }\n }\n}\n\n/// The binary operators for modal logic are the same as those for propositional.\ntype ModalBinary = PropBinary;\n\n/// Just write a type alias and that's it, all of implies' functionality for free.\ntype ModalFormula = Formula<ModalBinary, ModalUnary, Atom>;\n```\n\nOnce you have a type like `ModalFormula` set up, you can just use all the provided methods\nin the Formula struct for free. To initialize a formula you can start with just an atom\n\n```rust\nlet mut f = ModalFormula::new(Atom(\"p\")) // p\n```\n\nor use the cascade macro for builder syntax\n\n```rust\nlet mut f = cascade! {\n let f = ModalFormula::new(Atom(\"p\")) // p\n ..unify(ModalUnary::Box) // \u25fbp\n ..left_combine(PropBinary::Implies, ModalFormula::new(Atom(\"q\"))) // q -> \u25fbp\n}\n```\n\nor if your type implements `Match` just use a string!\n\n```rust\nuse implies::parser::build_formula;\n\nlet mut f: ModalFormula = build_formula(\"q -> \u25fbp\")?;\n```\n",
"bugtrack_url": null,
"license": "MIT",
"summary": "A parser for logical formulas",
"version": "0.4.5",
"project_urls": {
"Source Code": "https://github.com/armaan-rashid/implies"
},
"split_keywords": [
"logic",
"binary_tree",
"tree",
"graph"
],
"urls": [
{
"comment_text": null,
"digests": {
"blake2b_256": "f6f48a4906b04ddf4c36086728cdcc44a7faeaa0392cbdfd418496f6977fcd63",
"md5": "6c5bda9f7e9c93736b0f58f388d6fe8b",
"sha256": "2b73261ebf688006909c27c630493f50d0d1e6bd02153bf5135ffa64701c04c0"
},
"downloads": -1,
"filename": "implies-0.4.5-cp39-cp39-macosx_10_12_x86_64.whl",
"has_sig": false,
"md5_digest": "6c5bda9f7e9c93736b0f58f388d6fe8b",
"packagetype": "bdist_wheel",
"python_version": "cp39",
"requires_python": null,
"size": 250760,
"upload_time": "2024-01-26T21:50:26",
"upload_time_iso_8601": "2024-01-26T21:50:26.460826Z",
"url": "https://files.pythonhosted.org/packages/f6/f4/8a4906b04ddf4c36086728cdcc44a7faeaa0392cbdfd418496f6977fcd63/implies-0.4.5-cp39-cp39-macosx_10_12_x86_64.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": null,
"digests": {
"blake2b_256": "565d0e15947f489ae2daebac67488f102bc620551f507fe03b6319773c6102ef",
"md5": "fc5b4c88ccd1acf03511f38b1de844e3",
"sha256": "69a64240bf8acb916c547aded91af1786a97d4b216051051e652c71ae2038913"
},
"downloads": -1,
"filename": "implies-0.4.5.tar.gz",
"has_sig": false,
"md5_digest": "fc5b4c88ccd1acf03511f38b1de844e3",
"packagetype": "sdist",
"python_version": "source",
"requires_python": null,
"size": 26090,
"upload_time": "2024-01-26T21:50:28",
"upload_time_iso_8601": "2024-01-26T21:50:28.403223Z",
"url": "https://files.pythonhosted.org/packages/56/5d/0e15947f489ae2daebac67488f102bc620551f507fe03b6319773c6102ef/implies-0.4.5.tar.gz",
"yanked": false,
"yanked_reason": null
}
],
"upload_time": "2024-01-26 21:50:28",
"github": true,
"gitlab": false,
"bitbucket": false,
"codeberg": false,
"github_user": "armaan-rashid",
"github_project": "implies",
"travis_ci": false,
"coveralls": false,
"github_actions": false,
"lcname": "implies"
}
