1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183
//! A [Rust][0] library for representing, parsing, and computing with first-order [term rewriting systems][1]. //! //! # Usage //! //! ```toml //! [dependencies] //! term_rewriting = "0.7" //! ``` //! //! # Example //! //! ``` //! use term_rewriting::{Signature, Term, parse_trs, parse_term}; //! //! // We can parse a string representation of SK combinatory logic, //! let mut sig = Signature::default(); //! let sk_rules = "S x_ y_ z_ = (x_ z_) (y_ z_); K x_ y_ = x_;"; //! let trs = parse_trs(&mut sig, sk_rules).expect("parsed TRS"); //! //! // and we can also parse an arbitrary term. //! let mut sig = Signature::default(); //! let term = "S K K (K S K)"; //! let parsed_term = parse_term(&mut sig, term).expect("parsed term"); //! //! // These can also be constructed by hand. //! let mut sig = Signature::default(); //! let s = sig.new_op(0, Some("S".to_string())); //! let k = sig.new_op(0, Some("K".to_string())); //! let app = sig.new_op(2, Some(".".to_string())); //! //! let constructed_term = Term::Application { //! op: app.clone(), //! args: vec![ //! Term::Application { //! op: app.clone(), //! args: vec![ //! Term::Application { //! op: app.clone(), //! args: vec![ //! Term::Application { op: s.clone(), args: vec![] }, //! Term::Application { op: k.clone(), args: vec![] }, //! ] //! }, //! Term::Application { op: k.clone(), args: vec![] } //! ] //! }, //! Term::Application { //! op: app.clone(), //! args: vec![ //! Term::Application { //! op: app.clone(), //! args: vec![ //! Term::Application { op: k.clone(), args: vec![] }, //! Term::Application { op: s.clone(), args: vec![] }, //! ] //! }, //! Term::Application { op: k.clone(), args: vec![] } //! ] //! } //! ] //! }; //! //! // This is the same output the parser produces. //! assert_eq!(parsed_term, constructed_term); //! ``` //! //! # TRS syntax //! //! Several functions are available which parse TRS-related data structures //! according to the following grammar (defined in [augmented Backus-Naur form]): //! //! - [`parse`]: a [`TRS`] and list of [`Term`s] (`program`) //! - [`parse_trs`]: a [`TRS`] (`trs`) //! - [`parse_term`]: a [`Term`] (`top-level-term`) //! - [`parse_rule`]: a [`Rule`] (`rule`) //! - [`parse_context`]: a [`Context`] (`top-level-context`) //! - [`parse_rulecontext`]: a [`RuleContext`] (`rulecontext`) //! //! ```text //! program = *wsp *( *comment statement ";" *comment ) *wsp //! //! statement = rule / top-level-term //! //! rule = top-level-term *wsp "=" *wsp top-level-term //! rule /= rule *wsp "|" *wsp top-level-term //! //! top-level-term = term //! top-level-term /= top-level-term 1*wsp top-level-term //! //! term = variable //! term /= application //! term /= "(" *wsp top-level-term *wsp ")" //! //! rulecontext = top-level-term *wsp "=" *wsp top-level-term //! rulecontext /= rule *wsp "|" *wsp top-level-term //! //! top-level-context = context //! top-level-context /= top-level-context 1*wsp top-level-context //! //! context = variable //! context /= application //! context /= hole //! context /= "(" *wsp top-level-context *wsp ")" //! //! hole = "[!]" //! //! variable = identifier"_" //! //! application = identifier "(" [ term *( 1*wsp term ) ] ")" //! application /= identifier //! application /= binary-application //! //! ; binary application is the '.' operator with arity 2. //! binary-application = "(" *wsp term *wsp term *wsp ")" //! //! identifier = 1*( ALPHA / DIGIT ) //! //! comment = "#" *any-char-but-newline "\n" //! //! wsp = SP / TAB / CR / LF //! ``` //! //! # Term Rewriting Systems //! //! Term Rewriting Systems (TRS) are a simple formalism from theoretical //! computer science used to model the behavior and evolution of tree-based //! structures like natural langauge parse trees or abstract syntax trees. //! //! A TRS is defined as a pair _(S, R)_. _S_ is a set of symbols called the //! signature and together with a disjoint and countably infinite set of //! variables, defines the set of all possible trees, or terms, which the system //! can consider. _R_ is a set of rewrite rules. A rewrite rule is an equation, //! _s = t_, and is interpreted as follows: any term matching the pattern //! described by _s_ can be rewritten according to the pattern described by _t_. //! Together _S_ and _R_ define a TRS that describes a system of computation, //! which can be considered as a sort of programming language. //! `term_rewriting` provides a way to describe arbitrary first-order TRSs //! (i.e. no lambda-binding in rules). //! //! ### Further Reading //! //! - Baader & Nipkow (1999). [Term rewriting and all that][2]. Cambridge University Press. //! - Bezem, Klop, & de Vrijer (Eds.) (2003). [Term Rewriting Systems][3]. Cambridge University Press. //! - [Rewriting][4]. (2017). Wikipedia. //! //! [0]: https://www.rust-lang.org //! "The Rust Programming Language" //! [1]: https://en.wikipedia.org/wiki/Rewriting#Term_rewriting_systems //! "Wikipedia - Term Rewriting Systems" //! [2]: http://www.cambridge.org/us/academic/subjects/computer-science/programming-languages-and-applied-logic/term-rewriting-and-all //! "Term Rewriting and All That" //! [3]: http://www.cambridge.org/us/academic/subjects/computer-science/programming-languages-and-applied-logic/term-rewriting-systems //! "Term Rewriting Systems" //! [4]: https://en.wikipedia.org/wiki/Rewriting //! "Wikipedia - Rewriting" //! [augmented Backus-Naur form]: https://en.wikipedia.org/wiki/Augmented_Backus–Naur_form //! [`parse`]: fn.parse.html //! [`parse_trs`]: fn.parse_trs.html //! [`parse_term`]: fn.parse_term.html //! [`parse_rule`]: fn.parse_rule.html //! [`parse_context`]: fn.parse_context.html //! [`parse_rulecontext`]: fn.parse_rulecontext.html //! [`TRS`]: struct.TRS.html //! [`Term`s]: enum.Term.html //! [`Term`]: enum.Term.html //! [`Rule`]: struct.Rule.html //! [`Context`]: enum.Context.html //! [`RuleContext`]: struct.RuleContext.html extern crate itertools; #[macro_use] extern crate nom; extern crate rand; mod parser; mod pretty; pub mod trace; mod types; pub use parser::{ parse, parse_context, parse_rule, parse_rulecontext, parse_term, parse_trs, ParseError, }; pub use types::*;