cop/
tptp.rs

1//! TPTP parsing.
2use crate::fof::{Fof, FofAtom, Op, OpA, Quantifier};
3use crate::role::{Role, RoleMap};
4use crate::szs::NoSuccessKind;
5use crate::term::{Args, Term};
6use alloc::string::ToString;
7use alloc::{boxed::Box, string::String, vec::Vec};
8use tptp::{cnf, common, fof, top, TPTPIterator};
9
10/// String term.
11pub type STerm = Term<String, String>;
12/// String arguments.
13pub type SArgs = Args<String, String>;
14/// String formula.
15pub type SFof = Fof<FofAtom<String, String, String>, String>;
16
17/// Parse TPTP file and add formulas to role map, call `f` on include statements.
18pub fn parse<F>(bytes: &[u8], forms: &mut RoleMap<Vec<SFof>>, f: F) -> Result<(), NoSuccessKind>
19where
20    F: Fn(&str, &mut RoleMap<Vec<SFof>>) -> Result<(), NoSuccessKind>,
21{
22    let mut parser = TPTPIterator::<()>::new(bytes);
23    for input in &mut parser {
24        let input = input.map_err(|_| NoSuccessKind::SyntaxError)?;
25        match input {
26            top::TPTPInput::Include(include) => f(include.file_name.0 .0, forms)?,
27            top::TPTPInput::Annotated(ann) => {
28                let (role, formula) = get_role_formula(*ann);
29                log::info!("formula: {}", formula);
30                forms.get_mut(role).push(formula);
31            }
32        };
33    }
34    if parser.remaining.is_empty() {
35        Ok(())
36    } else {
37        Err(NoSuccessKind::SyntaxError)
38    }
39}
40
41fn get_role_formula(annotated: top::AnnotatedFormula) -> (Role, SFof) {
42    use top::AnnotatedFormula::*;
43    match annotated {
44        Fof(fof) => (Role::from(fof.0.role), SFof::from(*fof.0.formula)),
45        Cnf(cnf) => {
46            // quantify all variables in the formula
47            let role = Role::from(cnf.0.role);
48            let fm = SFof::from(*cnf.0.formula);
49            let mut vars: Vec<_> = fm.atoms().flat_map(|a| a.vars()).cloned().collect();
50            vars.sort();
51            vars.dedup();
52            let q = role.quantifier();
53            let fm = vars.into_iter().fold(fm, |fm, v| SFof::quant(q, v, fm));
54            (role, fm)
55        }
56        Tfx(_) => todo!(),
57    }
58}
59
60impl From<fof::FunctionTerm<'_>> for STerm {
61    fn from(tm: fof::FunctionTerm) -> Self {
62        use fof::FunctionTerm::*;
63        match tm {
64            Plain(p) => Self::from(p),
65            Defined(d) => Self::from(d),
66            System(_) => todo!(),
67        }
68    }
69}
70
71impl From<fof::DefinedTerm<'_>> for STerm {
72    fn from(tm: fof::DefinedTerm) -> Self {
73        use fof::DefinedTerm::*;
74        match tm {
75            Defined(d) => Self::from(d),
76            Atomic(_) => todo!(),
77        }
78    }
79}
80
81impl From<tptp::common::DefinedTerm<'_>> for STerm {
82    fn from(tm: tptp::common::DefinedTerm) -> Self {
83        use tptp::common::DefinedTerm::*;
84        match tm {
85            Number(n) => Self::C(n.to_string(), Args::new()),
86            Distinct(_) => todo!(),
87        }
88    }
89}
90
91impl From<fof::Term<'_>> for STerm {
92    fn from(tm: fof::Term) -> Self {
93        use fof::Term::*;
94        match tm {
95            Variable(v) => Self::V(v.to_string()),
96            Function(f) => Self::from(*f),
97        }
98    }
99}
100
101impl From<fof::Arguments<'_>> for SArgs {
102    fn from(args: fof::Arguments) -> Self {
103        args.0.into_iter().map(Term::from).collect()
104    }
105}
106
107impl From<fof::PlainTerm<'_>> for STerm {
108    fn from(tm: fof::PlainTerm) -> Self {
109        use fof::PlainTerm::*;
110        match tm {
111            Constant(c) => Self::C(c.to_string(), Args::new()),
112            Function(f, args) => Self::C(f.to_string(), Args::from(*args)),
113        }
114    }
115}
116
117impl From<fof::LogicFormula<'_>> for SFof {
118    fn from(frm: fof::LogicFormula) -> Self {
119        use fof::LogicFormula::*;
120        match frm {
121            Binary(b) => Self::from(b),
122            Unary(u) => Self::from(u),
123            Unitary(u) => Self::from(u),
124        }
125    }
126}
127
128impl From<fof::QuantifiedFormula<'_>> for SFof {
129    fn from(frm: fof::QuantifiedFormula) -> Self {
130        let q = Quantifier::from(frm.quantifier);
131        let vs = frm.bound.0.iter().rev().map(|v| v.to_string());
132        vs.fold(Self::from(*frm.formula), |fm, v| {
133            Self::Quant(q, v, Box::new(fm))
134        })
135    }
136}
137
138impl From<fof::UnitFormula<'_>> for SFof {
139    fn from(frm: fof::UnitFormula) -> Self {
140        use fof::UnitFormula::*;
141        match frm {
142            Unitary(u) => Self::from(u),
143            Unary(u) => Self::from(u),
144        }
145    }
146}
147
148impl From<fof::InfixUnary<'_>> for SFof {
149    fn from(frm: fof::InfixUnary) -> Self {
150        let _: common::InfixInequality = frm.op;
151        -Self::eqtm(Term::from(*frm.left), Term::from(*frm.right))
152    }
153}
154
155impl From<fof::UnaryFormula<'_>> for SFof {
156    fn from(frm: fof::UnaryFormula) -> Self {
157        use fof::UnaryFormula::*;
158        match frm {
159            // negation
160            Unary(_negation, fuf) => -Self::from(*fuf),
161            // term inequality
162            InfixUnary(i) => Self::from(i),
163        }
164    }
165}
166
167impl From<fof::BinaryFormula<'_>> for SFof {
168    fn from(frm: fof::BinaryFormula) -> Self {
169        use fof::BinaryFormula::*;
170        match frm {
171            Nonassoc(fbn) => Self::from(fbn),
172            Assoc(fba) => Self::from(fba),
173        }
174    }
175}
176
177impl From<fof::BinaryNonassoc<'_>> for SFof {
178    fn from(frm: fof::BinaryNonassoc) -> Self {
179        let left = Box::new(Self::from(*frm.left));
180        let right = Box::new(Self::from(*frm.right));
181        use common::NonassocConnective::*;
182        match frm.op {
183            LRImplies => Self::Bin(left, Op::Impl, right),
184            RLImplies => Self::Bin(right, Op::Impl, left),
185            Equivalent => Self::Bin(left, Op::EqFm, right),
186            NotEquivalent => -Self::Bin(left, Op::EqFm, right),
187            NotOr => -(*left | *right),
188            NotAnd => -(*left & *right),
189        }
190    }
191}
192
193impl From<fof::BinaryAssoc<'_>> for SFof {
194    fn from(fm: fof::BinaryAssoc) -> Self {
195        use fof::BinaryAssoc::*;
196        let (op, fms) = match fm {
197            Or(fms) => (OpA::Disj, fms.0),
198            And(fms) => (OpA::Conj, fms.0),
199        };
200        Self::BinA(op, fms.into_iter().map(Self::from).collect())
201    }
202}
203
204impl From<fof::Quantifier> for Quantifier {
205    fn from(q: fof::Quantifier) -> Self {
206        use fof::Quantifier::*;
207        match q {
208            Forall => Self::Forall,
209            Exists => Self::Exists,
210        }
211    }
212}
213
214impl From<fof::UnitaryFormula<'_>> for SFof {
215    fn from(frm: fof::UnitaryFormula) -> Self {
216        use fof::UnitaryFormula::*;
217        match frm {
218            Parenthesised(flf) => Self::from(*flf),
219            Quantified(fqf) => Self::from(fqf),
220            Atomic(a) => Self::from(*a),
221        }
222    }
223}
224
225impl From<fof::PlainAtomicFormula<'_>> for SFof {
226    fn from(frm: fof::PlainAtomicFormula) -> Self {
227        use fof::PlainTerm::*;
228        match frm.0 {
229            Constant(c) => Self::atom(c.to_string(), Args::new()),
230            Function(f, args) => Self::atom(f.to_string(), Args::from(*args)),
231        }
232    }
233}
234
235impl From<fof::DefinedAtomicFormula<'_>> for SFof {
236    fn from(frm: fof::DefinedAtomicFormula) -> Self {
237        use fof::DefinedAtomicFormula::*;
238        match frm {
239            Plain(p) => Self::from(p),
240            Infix(i) => Self::eqtm(Term::from(*i.left), Term::from(*i.right)),
241        }
242    }
243}
244
245impl From<fof::DefinedPlainFormula<'_>> for SFof {
246    fn from(fm: fof::DefinedPlainFormula) -> Self {
247        use fof::DefinedPlainTerm::Constant;
248        match fm.0 {
249            Constant(c) if c.0 .0 .0 .0 .0 == "true" => {
250                let p = Self::atom("$true".to_string(), Args::new());
251                Self::imp(p.clone(), p)
252            }
253            Constant(c) if c.0 .0 .0 .0 .0 == "false" => {
254                let p = Self::atom("$false".to_string(), Args::new());
255                p.clone() & -p
256            }
257            _ => todo!(),
258        }
259    }
260}
261
262impl From<fof::AtomicFormula<'_>> for SFof {
263    fn from(frm: fof::AtomicFormula) -> Self {
264        use fof::AtomicFormula::*;
265        match frm {
266            Plain(p) => Self::from(p),
267            Defined(d) => Self::from(d),
268            System(_) => todo!(),
269        }
270    }
271}
272
273impl From<fof::Formula<'_>> for SFof {
274    fn from(frm: fof::Formula) -> Self {
275        Self::from(frm.0)
276    }
277}
278
279impl From<cnf::Literal<'_>> for SFof {
280    fn from(lit: cnf::Literal) -> Self {
281        use cnf::Literal::*;
282        match lit {
283            Atomic(a) => Self::from(a),
284            NegatedAtomic(a) => -Self::from(a),
285            Infix(i) => Self::from(i),
286        }
287    }
288}
289
290impl From<cnf::Disjunction<'_>> for SFof {
291    fn from(frm: cnf::Disjunction) -> Self {
292        Self::BinA(OpA::Disj, frm.0.into_iter().map(Self::from).collect())
293    }
294}
295
296impl From<cnf::Formula<'_>> for SFof {
297    fn from(frm: cnf::Formula) -> Self {
298        use cnf::Formula::*;
299        match frm {
300            Disjunction(d) | Parenthesised(d) => Self::from(d),
301        }
302    }
303}
304
305impl From<top::FormulaRole<'_>> for Role {
306    fn from(role: top::FormulaRole<'_>) -> Self {
307        match role.0 .0 {
308            "conjecture" => Self::Conjecture,
309            "negated_conjecture" => Self::NegatedConjecture,
310            _ => Self::Other,
311        }
312    }
313}
cop/tptp.rs

cop/
tptp.rs
