From f19f1a3eb13fd03203afad77d47fab05b9b5a81d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Fri, 24 Jan 2020 18:43:42 +0100 Subject: [PATCH] Work in progress --- src/ast.rs | 196 +++++++++++++++++++++++++++++++++---------------- src/format.rs | 192 +++++++++++++++++++++++++++++++++--------------- src/lib.rs | 6 +- src/parse.rs | 199 ++++++++++++++++++++++++++++---------------------- 4 files changed, 383 insertions(+), 210 deletions(-) diff --git a/src/ast.rs b/src/ast.rs index 9f81d17..7f764c3 100644 --- a/src/ast.rs +++ b/src/ast.rs @@ -1,76 +1,150 @@ -#[derive(Eq, Hash, PartialEq)] +// Operators + +pub enum BinaryOperator +{ + Addition, + Subtraction, + Multiplication, + Division, + Modulo, + Exponentiation, +} + +pub enum ComparisonOperator +{ + Greater, + Less, + LessOrEqual, + GreaterOrEqual, + NotEqual, + Equal, +} + +pub enum UnaryOperator +{ + AbsoluteValue, + Negation, +} + +// Primitives + +pub struct FunctionDeclaration +{ + pub name: String, + pub arity: usize, +} + pub struct PredicateDeclaration { pub name: String, pub arity: usize, } -#[derive(PartialEq)] -pub struct Predicate -{ - pub declaration: PredicateDeclaration, - pub arguments: Vec, -} - -#[derive(PartialEq)] -pub struct Exists -{ - pub parameters: Vec, - pub argument: Box, -} - -#[derive(PartialEq)] -pub struct ForAll -{ - pub parameters: Vec, - pub argument: Box, -} - -#[derive(PartialEq)] -pub enum Formula -{ - Exists(Exists), - ForAll(ForAll), - Not(Box), - And(Vec>), - Or(Vec>), - Implies(Box, Box), - Biconditional(Box, Box), - Less(Term, Term), - LessOrEqual(Term, Term), - Greater(Term, Term), - GreaterOrEqual(Term, Term), - Equal(Term, Term), - NotEqual(Term, Term), - Boolean(bool), - Predicate(Predicate), -} - -#[derive(PartialEq)] -pub enum Domain -{ - Program, - Integer, -} - -#[derive(PartialEq)] pub struct VariableDeclaration { pub name: String, - pub domain: Domain, } -#[derive(PartialEq)] -pub enum Term +// Terms + +pub struct BinaryOperation +{ + pub operator: BinaryOperator, + pub left: Box, + pub right: Box, +} + +pub struct Function +{ + pub declaration: std::rc::Rc, + pub arguments: Vec>, +} + +pub enum SpecialInteger { Infimum, Supremum, - Integer(i64), - Symbolic(String), - String(String), - Variable(VariableDeclaration), - Add(Box, Box), - Subtract(Box, Box), - Multiply(Box, Box), - Negative(Box), } + +pub struct UnaryOperation +{ + pub operator: UnaryOperator, + pub argument: Box, +} + +pub struct Variable +{ + pub declaration: std::rc::Rc, +} + +// Formulas + +pub struct Biconditional +{ + pub left: Box, + pub right: Box, +} + +pub struct Comparison +{ + pub operator: ComparisonOperator, + pub left: Box, + pub right: Box, +} + +pub struct Exists +{ + pub parameters: Vec>, + pub argument: Box, +} + +pub struct ForAll +{ + pub parameters: Vec>, + pub argument: Box, +} + +pub struct Implies +{ + pub antecedent: Box, + pub implication: Box, +} + +pub struct Predicate +{ + pub declaration: std::rc::Rc, + pub arguments: Vec>, +} + +// Variants + +pub enum Term +{ + BinaryOperation(BinaryOperation), + Boolean(bool), + Function(Function), + Integer(i32), + SpecialInteger(SpecialInteger), + String(String), + Symbolic(String), + UnaryOperation(UnaryOperation), + Variable(Variable), +} + +pub type Terms = Vec>; + +pub enum Formula +{ + And(Formulas), + Biconditional(Biconditional), + Boolean(bool), + Comparison(Comparison), + Exists(Exists), + ForAll(ForAll), + Implies(Implies), + Not(Box), + Or(Formulas), + Predicate(Predicate), +} + +pub type Formulas = Vec>; diff --git a/src/format.rs b/src/format.rs index 5189259..f749f78 100644 --- a/src/format.rs +++ b/src/format.rs @@ -1,16 +1,16 @@ struct TermDisplay<'term> { - parent_precedence: u64, + parent_precedence: i32, term: &'term crate::Term, } struct FormulaDisplay<'formula> { - parent_precedence: u64, + parent_precedence: i32, formula: &'formula crate::Formula, } -fn display_term<'term>(term: &'term crate::Term, parent_precedence: u64) -> TermDisplay<'term> +fn display_term<'term>(term: &'term crate::Term, parent_precedence: i32) -> TermDisplay<'term> { TermDisplay { @@ -19,7 +19,7 @@ fn display_term<'term>(term: &'term crate::Term, parent_precedence: u64) -> Term } } -fn display_formula<'formula>(formula: &'formula crate::Formula, parent_precedence: u64) +fn display_formula<'formula>(formula: &'formula crate::Formula, parent_precedence: i32) -> FormulaDisplay<'formula> { FormulaDisplay @@ -29,28 +29,66 @@ fn display_formula<'formula>(formula: &'formula crate::Formula, parent_precedenc } } -fn term_precedence(term: &crate::Term) -> u64 +trait Precedence { - match term + fn precedence(&self) -> i32; +} + +impl Precedence for crate::Term +{ + fn precedence(&self) -> i32 { - crate::Term::Infimum | crate::Term::Supremum | crate::Term::Integer(_) | crate::Term::Symbolic(_) | crate::Term::String(_) | crate::Term::Variable(_) => 0, - crate::Term::Negative(_) => 1, - crate::Term::Multiply(_, _) => 2, - crate::Term::Add(_, _) | crate::Term::Subtract(_, _) => 3, + match &self + { + Self::Boolean(_) + | Self::Function(_) + | Self::SpecialInteger(_) + | Self::Integer(_) + | Self::Symbolic(_) + | Self::String(_) + | Self::Variable(_) + => 0, + Self::UnaryOperation(crate::UnaryOperation{operator: crate::UnaryOperator::Negation, ..}) + => 1, + Self::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Exponentiation, ..}) + => 2, + Self::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Multiplication, ..}) + | Self::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Division, ..}) + | Self::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Modulo, ..}) + => 3, + Self::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Addition, ..}) + | Self::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Subtraction, ..}) + => 4, + Self::UnaryOperation(crate::UnaryOperation{operator: crate::UnaryOperator::AbsoluteValue, ..}) + => 5, + } } } -fn formula_precedence(formula: &crate::Formula) -> u64 +impl Precedence for crate::Formula { - match formula + fn precedence(&self) -> i32 { - crate::Formula::Predicate(_) | crate::Formula::Boolean(_) | crate::Formula::Less(_, _) | crate::Formula::LessOrEqual(_, _) | crate::Formula::Greater(_, _) | crate::Formula::GreaterOrEqual(_, _) | crate::Formula::Equal(_, _) | crate::Formula::NotEqual(_, _) => 0, - crate::Formula::Exists(_) | crate::Formula::ForAll(_) => 1, - crate::Formula::Not(_) => 2, - crate::Formula::And(_) => 3, - crate::Formula::Or(_) => 4, - crate::Formula::Implies(_, _) => 5, - crate::Formula::Biconditional(_, _) => 6, + match &self + { + Self::Predicate(_) + | Self::Boolean(_) + | Self::Comparison(_) + => 0, + Self::Exists(_) + | Self::ForAll(_) + => 1, + Self::Not(_) + => 2, + Self::And(_) + => 3, + Self::Or(_) + => 4, + Self::Implies(_) + => 5, + Self::Biconditional(_) + => 6, + } } } @@ -58,12 +96,6 @@ impl std::fmt::Debug for crate::VariableDeclaration { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result { - match &self.domain - { - crate::Domain::Program => write!(format, "X")?, - crate::Domain::Integer => write!(format, "N")?, - }; - write!(format, "{}", &self.name) } } @@ -80,7 +112,7 @@ impl<'term> std::fmt::Debug for TermDisplay<'term> { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result { - let precedence = term_precedence(self.term); + let precedence = self.term.precedence(); let requires_parentheses = precedence > self.parent_precedence; if requires_parentheses @@ -88,18 +120,58 @@ impl<'term> std::fmt::Debug for TermDisplay<'term> write!(format, "(")?; } - match self.term + match &self.term { - crate::Term::Infimum => write!(format, "#inf"), - crate::Term::Supremum => write!(format, "#sup"), + crate::Term::Boolean(true) => write!(format, "true"), + crate::Term::Boolean(false) => write!(format, "false"), + crate::Term::SpecialInteger(crate::SpecialInteger::Infimum) => write!(format, "#inf"), + crate::Term::SpecialInteger(crate::SpecialInteger::Supremum) => write!(format, "#sup"), crate::Term::Integer(value) => write!(format, "{}", value), - crate::Term::Symbolic(ref value) => write!(format, "{}", value), - crate::Term::String(ref value) => write!(format, "\"{}\"", value), - crate::Term::Variable(ref declaration) => write!(format, "{:?}", declaration), - crate::Term::Add(ref left, ref right) => write!(format, "{:?} + {:?}", display_term(left, precedence), display_term(right, precedence)), - crate::Term::Subtract(ref left, ref right) => write!(format, "{:?} - {:?}", display_term(left, precedence), display_term(right, precedence)), - crate::Term::Multiply(ref left, ref right) => write!(format, "{:?} * {:?}", display_term(left, precedence), display_term(right, precedence)), - crate::Term::Negative(ref argument) => write!(format, "-{:?}", display_term(argument, precedence)), + crate::Term::Symbolic(value) => write!(format, "{}", value), + crate::Term::String(value) => write!(format, "\"{}\"", value), + crate::Term::Variable(variable) => write!(format, "{:?}", variable.declaration), + crate::Term::Function(function) => + { + write!(format, "{}", function.declaration.name)?; + + assert!(function.declaration.arity == function.arguments.len(), + "function has a different number of arguments than declared (expected {}, got {})", + function.declaration.arity, function.arguments.len()); + + if function.arguments.len() > 0 + { + write!(format, "{}(", function.declaration.name)?; + + let mut separator = ""; + + for argument in &function.arguments + { + write!(format, "{}{:?}", separator, display_term(&argument, 1000))?; + + separator = ", "; + } + + write!(format, ")")?; + } + + Ok(()) + }, + crate::Term::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Addition, left, right}) + => write!(format, "{:?} + {:?}", display_term(left, precedence), display_term(right, precedence)), + crate::Term::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Subtraction, left, right}) + => write!(format, "{:?} - {:?}", display_term(left, precedence), display_term(right, precedence)), + crate::Term::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Multiplication, left, right}) + => write!(format, "{:?} * {:?}", display_term(left, precedence), display_term(right, precedence)), + crate::Term::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Division, left, right}) + => write!(format, "{:?} / {:?}", display_term(left, precedence), display_term(right, precedence)), + crate::Term::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Modulo, left, right}) + => write!(format, "{:?} % {:?}", display_term(left, precedence), display_term(right, precedence)), + crate::Term::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Exponentiation, left, right}) + => write!(format, "{:?} ** {:?}", display_term(left, precedence), display_term(right, precedence)), + crate::Term::UnaryOperation(crate::UnaryOperation{operator: crate::UnaryOperator::Negation, argument}) + => write!(format, "-{:?}", display_term(argument, precedence)), + crate::Term::UnaryOperation(crate::UnaryOperation{operator: crate::UnaryOperator::AbsoluteValue, argument}) + => write!(format, "|{:?}|", display_term(argument, precedence)), }?; if requires_parentheses @@ -123,7 +195,7 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula> { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result { - let precedence = formula_precedence(self.formula); + let precedence = self.formula.precedence(); let requires_parentheses = precedence > self.parent_precedence; if requires_parentheses @@ -131,9 +203,9 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula> write!(format, "(")?; } - match self.formula + match &self.formula { - crate::Formula::Exists(ref exists) => + crate::Formula::Exists(exists) => { write!(format, "exists")?; @@ -148,7 +220,7 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula> write!(format, " {:?}", display_formula(&exists.argument, precedence))?; }, - crate::Formula::ForAll(ref for_all) => + crate::Formula::ForAll(for_all) => { write!(format, "forall")?; @@ -163,8 +235,8 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula> write!(format, " {:?}", display_formula(&for_all.argument, precedence))?; }, - crate::Formula::Not(ref argument) => write!(format, "not {:?}", display_formula(argument, precedence))?, - crate::Formula::And(ref arguments) => + crate::Formula::Not(argument) => write!(format, "not {:?}", display_formula(argument, precedence))?, + crate::Formula::And(arguments) => { let mut separator = ""; @@ -175,7 +247,7 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula> separator = " and " } }, - crate::Formula::Or(ref arguments) => + crate::Formula::Or(arguments) => { let mut separator = ""; @@ -186,21 +258,25 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula> separator = " or " } }, - crate::Formula::Implies(ref left, ref right) => write!(format, "{:?} -> {:?}", display_formula(left, precedence), display_formula(right, precedence))?, - crate::Formula::Biconditional(ref left, ref right) => write!(format, "{:?} <-> {:?}", display_formula(left, precedence), display_formula(right, precedence))?, - crate::Formula::Less(ref left, ref right) => write!(format, "{:?} < {:?}", display_term(left, 1000), display_term(right, 1000))?, - crate::Formula::LessOrEqual(ref left, ref right) => write!(format, "{:?} <= {:?}", display_term(left, 1000), display_term(right, 1000))?, - crate::Formula::Greater(ref left, ref right) => write!(format, "{:?} > {:?}", display_term(left, 1000), display_term(right, 1000))?, - crate::Formula::GreaterOrEqual(ref left, ref right) => write!(format, "{:?} >= {:?}", display_term(left, 1000), display_term(right, 1000))?, - crate::Formula::Equal(ref left, ref right) => write!(format, "{:?} = {:?}", display_term(left, 1000), display_term(right, 1000))?, - crate::Formula::NotEqual(ref left, ref right) => write!(format, "{:?} != {:?}", display_term(left, 1000), display_term(right, 1000))?, - crate::Formula::Boolean(value) => - match value - { - true => write!(format, "#true")?, - false => write!(format, "#false")?, - }, - crate::Formula::Predicate(ref predicate) => + crate::Formula::Implies(crate::Implies{antecedent, implication}) + => write!(format, "{:?} -> {:?}", display_formula(antecedent, precedence), display_formula(implication, precedence))?, + crate::Formula::Biconditional(crate::Biconditional{left, right}) + => write!(format, "{:?} <-> {:?}", display_formula(left, precedence), display_formula(right, precedence))?, + crate::Formula::Comparison(crate::Comparison{operator: crate::ComparisonOperator::Less, left, right}) + => write!(format, "{:?} < {:?}", display_term(left, 1000), display_term(right, 1000))?, + crate::Formula::Comparison(crate::Comparison{operator: crate::ComparisonOperator::LessOrEqual, left, right}) + => write!(format, "{:?} <= {:?}", display_term(left, 1000), display_term(right, 1000))?, + crate::Formula::Comparison(crate::Comparison{operator: crate::ComparisonOperator::Greater, left, right}) + => write!(format, "{:?} > {:?}", display_term(left, 1000), display_term(right, 1000))?, + crate::Formula::Comparison(crate::Comparison{operator: crate::ComparisonOperator::GreaterOrEqual, left, right}) + => write!(format, "{:?} >= {:?}", display_term(left, 1000), display_term(right, 1000))?, + crate::Formula::Comparison(crate::Comparison{operator: crate::ComparisonOperator::Equal, left, right}) + => write!(format, "{:?} = {:?}", display_term(left, 1000), display_term(right, 1000))?, + crate::Formula::Comparison(crate::Comparison{operator: crate::ComparisonOperator::NotEqual, left, right}) + => write!(format, "{:?} != {:?}", display_term(left, 1000), display_term(right, 1000))?, + crate::Formula::Boolean(true) => write!(format, "#true")?, + crate::Formula::Boolean(false) => write!(format, "#false")?, + crate::Formula::Predicate(predicate) => { write!(format, "{}", predicate.declaration.name)?; diff --git a/src/lib.rs b/src/lib.rs index be744e7..db4cb95 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -1,6 +1,6 @@ mod ast; pub mod format; -mod parse; +//mod parse; -pub use ast::{Domain, Exists, Formula, ForAll, Predicate, PredicateDeclaration, VariableDeclaration, Term}; -pub use parse::{formula, formulas, term}; +pub use ast::*; +//pub use parse::{formula, formulas, term}; diff --git a/src/parse.rs b/src/parse.rs index 0cc40c4..603141b 100644 --- a/src/parse.rs +++ b/src/parse.rs @@ -10,6 +10,60 @@ use nom:: bytes::complete::tag, }; +type VariableDeclarations = std::collections::HashSet>; + +struct VariableDeclarationStack +{ + free_variable_declarations: VariableDeclarations, + bound_variable_declarations: Vec>, +} + +impl VariableDeclarationStack +{ + fn find(&self, variable_name: &str) -> Option> + { + for variable_declarations in self.iter().rev() + { + if let Some(variable_declaration) = variable_declarations.iter().find(|x| x.name == variable_name) + { + return Some(std::rc::Rc::clone(&variable_declaration)); + } + } + + if let Some(variable_declaration) = self.free_variable_declarations.iter().find(|x| x.name == variable_name) + { + return Some(std::rc::Rc::clone(&variable_declaration)); + } + + None + } + + pub(crate) fn find_or_create(&mut self, variable_name: &str) -> std::rc::Rc + { + if let Some(variable_declaration) = self.find(variable_name) + { + return variable_declaration; + } + + let variable_declaration = crate::VariableDeclaration + { + name: variable_name.to_owned(), + }; + let variable_declaration = std::rc::Rc::new(variable_declaration); + + self.free_variable_declarations.insert(std::rc::Rc::clone(&variable_declaration)); + + variable_declaration + } +} + +struct Declarations +{ + //function_declarations:, + //predicate_declarations:, + variable_declaration_stack: VariableDeclarationStack, +} + enum TermOperator { Add, @@ -17,25 +71,25 @@ enum TermOperator Multiply, } -fn infimum(i: &str) -> IResult<&str, crate::Term> +fn infimum<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term> { map ( delimited(multispace0, tag("#inf"), multispace0), - |_| crate::Term::Infimum + |_| crate::Term::SpecialInteger(crate::SpecialInteger::Infimum) )(i) } -fn supremum(i: &str) -> IResult<&str, crate::Term> +fn supremum<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term> { map ( delimited(multispace0, tag("#sup"), multispace0), - |_| crate::Term::Supremum + |_| crate::Term::SpecialInteger(crate::SpecialInteger::Supremum) )(i) } -fn integer(i: &str) -> IResult<&str, crate::Term> +fn integer<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term> { map ( @@ -53,7 +107,7 @@ fn is_lowercase_alphanumeric(c: char) -> bool c.is_alphanumeric() && c.is_lowercase() } -fn symbolic_identifier(i: &str) -> IResult<&str, String> +fn symbolic_identifier<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, String> { let (i, symbolic_identifier) = map ( @@ -68,16 +122,16 @@ fn symbolic_identifier(i: &str) -> IResult<&str, String> Ok((i, symbolic_identifier)) } -fn symbolic(i: &str) -> IResult<&str, crate::Term> +fn symbolic<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term> { map ( - delimited(multispace0, symbolic_identifier, multispace0), + delimited(multispace0, |i| symbolic_identifier(i, declarations), multispace0), crate::Term::Symbolic )(i) } -fn string(i: &str) -> IResult<&str, crate::Term> +fn string<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term> { map ( @@ -96,7 +150,7 @@ fn string(i: &str) -> IResult<&str, crate::Term> )(i) } -fn program_variable_identifier(i: &str) -> IResult<&str, String> +fn variable_identifier<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, String> { map ( @@ -105,7 +159,7 @@ fn program_variable_identifier(i: &str) -> IResult<&str, String> multispace0, preceded ( - tag("X"), + take_while_m_n(1, 1, |c| char::is_alphabetic(c) && char::is_uppercase(c)), take_while(char::is_alphanumeric) ), multispace0 @@ -114,79 +168,48 @@ fn program_variable_identifier(i: &str) -> IResult<&str, String> )(i) } -fn integer_variable_identifier(i: &str) -> IResult<&str, String> +fn variable_declaration<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::VariableDeclaration> { map ( - delimited - ( - multispace0, - preceded - ( - tag("N"), - take_while(char::is_alphanumeric) - ), - multispace0 - ), - |s: &str| s.to_string() + |i| variable_identifier(i, declarations), + |s| crate::VariableDeclaration{name: s}, )(i) } -fn program_variable_declaration(i: &str) -> IResult<&str, crate::VariableDeclaration> +fn program_variable<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term> { map ( - program_variable_identifier, - |s| crate::VariableDeclaration{name: s, domain: crate::Domain::Program} + |i| program_variable_identifier(i, declarations), + |s| + { + let declaration = declarations.variable_declaration_stack.get(s.as_ref()); + + crate::Term::Variable(crate::VariableDeclaration{name: s, domain: crate::Domain::Program}) + }, )(i) } -fn integer_variable_declaration(i: &str) -> IResult<&str, crate::VariableDeclaration> +fn integer_variable<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term> { map ( - integer_variable_identifier, - |s| crate::VariableDeclaration{name: s, domain: crate::Domain::Integer} + |i| integer_variable_identifier, + |s| crate::Term::Variable(crate::VariableDeclaration{name: s, domain: crate::Domain::Integer}), )(i) } -fn variable_declaration(i: &str) -> IResult<&str, crate::VariableDeclaration> +fn variable<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term> { alt (( - program_variable_declaration, - integer_variable_declaration + |i| program_variable(i, declarations), + |i| integer_variable(i, declarations), ))(i) } -fn program_variable(i: &str) -> IResult<&str, crate::Term> -{ - map - ( - program_variable_identifier, - |s| crate::Term::Variable(crate::VariableDeclaration{name: s, domain: crate::Domain::Program}) - )(i) -} - -fn integer_variable(i: &str) -> IResult<&str, crate::Term> -{ - map - ( - integer_variable_identifier, - |s| crate::Term::Variable(crate::VariableDeclaration{name: s, domain: crate::Domain::Integer}) - )(i) -} - -fn variable(i: &str) -> IResult<&str, crate::Term> -{ - alt - (( - program_variable, - integer_variable - ))(i) -} - -fn predicate_0_ary(i: &str) -> IResult<&str, crate::Formula> +fn predicate_0_ary<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula> { map ( @@ -205,7 +228,7 @@ fn predicate_0_ary(i: &str) -> IResult<&str, crate::Formula> )(i) } -fn predicate_n_ary(i: &str) -> IResult<&str, crate::Formula> +fn predicate_n_ary<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula> { map ( @@ -238,7 +261,7 @@ fn predicate_n_ary(i: &str) -> IResult<&str, crate::Formula> )(i) } -fn predicate(i: &str) -> IResult<&str, crate::Formula> +fn predicate<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula> { alt (( @@ -247,7 +270,7 @@ fn predicate(i: &str) -> IResult<&str, crate::Formula> ))(i) } -fn boolean(i: &str) -> IResult<&str, crate::Formula> +fn boolean<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula> { map ( @@ -265,7 +288,7 @@ fn boolean(i: &str) -> IResult<&str, crate::Formula> )(i) } -fn less(i: &str) -> IResult<&str, crate::Formula> +fn less<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula> { map ( @@ -278,7 +301,7 @@ fn less(i: &str) -> IResult<&str, crate::Formula> )(i) } -fn less_or_equal(i: &str) -> IResult<&str, crate::Formula> +fn less_or_equal<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula> { map ( @@ -291,7 +314,7 @@ fn less_or_equal(i: &str) -> IResult<&str, crate::Formula> )(i) } -fn greater(i: &str) -> IResult<&str, crate::Formula> +fn greater<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula> { map ( @@ -304,7 +327,7 @@ fn greater(i: &str) -> IResult<&str, crate::Formula> )(i) } -fn greater_or_equal(i: &str) -> IResult<&str, crate::Formula> +fn greater_or_equal<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula> { map ( @@ -317,7 +340,7 @@ fn greater_or_equal(i: &str) -> IResult<&str, crate::Formula> )(i) } -fn equal(i: &str) -> IResult<&str, crate::Formula> +fn equal<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula> { map ( @@ -330,7 +353,7 @@ fn equal(i: &str) -> IResult<&str, crate::Formula> )(i) } -fn not_equal(i: &str) -> IResult<&str, crate::Formula> +fn not_equal<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula> { map ( @@ -343,7 +366,7 @@ fn not_equal(i: &str) -> IResult<&str, crate::Formula> )(i) } -fn comparison(i: &str) -> IResult<&str, crate::Formula> +fn comparison<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula> { alt (( @@ -356,7 +379,7 @@ fn comparison(i: &str) -> IResult<&str, crate::Formula> ))(i) } -fn term_parenthesized(i: &str) -> IResult<&str, crate::Term> +fn term_parenthesized<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term> { delimited ( @@ -387,7 +410,7 @@ fn fold_terms(initial: crate::Term, remainder: Vec<(TermOperator, crate::Term)>) }) } -fn term_precedence_0(i: &str) -> IResult<&str, crate::Term> +fn term_precedence_0<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term> { alt (( @@ -401,7 +424,7 @@ fn term_precedence_0(i: &str) -> IResult<&str, crate::Term> ))(i) } -fn term_precedence_1(i: &str) -> IResult<&str, crate::Term> +fn term_precedence_1<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term> { alt (( @@ -419,7 +442,7 @@ fn term_precedence_1(i: &str) -> IResult<&str, crate::Term> ))(i) } -fn term_precedence_2(i: &str) -> IResult<&str, crate::Term> +fn term_precedence_2<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term> { let (i, initial) = term_precedence_1(i)?; let (i, remainder) = @@ -435,7 +458,7 @@ fn term_precedence_2(i: &str) -> IResult<&str, crate::Term> Ok((i, fold_terms(initial, remainder))) } -fn term_precedence_3(i: &str) -> IResult<&str, crate::Term> +fn term_precedence_3<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term> { let (i, initial) = term_precedence_2(i)?; let (i, remainder) = @@ -459,12 +482,12 @@ fn term_precedence_3(i: &str) -> IResult<&str, crate::Term> Ok((i, fold_terms(initial, remainder))) } -pub fn term(i: &str) -> IResult<&str, crate::Term> +pub fn term<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term> { term_precedence_3(i) } -fn formula_parenthesized(i: &str) -> IResult<&str, crate::Formula> +fn formula_parenthesized<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula> { delimited ( @@ -479,7 +502,7 @@ fn formula_parenthesized(i: &str) -> IResult<&str, crate::Formula> )(i) } -fn formula_precedence_0(i: &str) -> IResult<&str, crate::Formula> +fn formula_precedence_0<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula> { alt (( @@ -490,7 +513,7 @@ fn formula_precedence_0(i: &str) -> IResult<&str, crate::Formula> ))(i) } -fn exists(i: &str) -> IResult<&str, crate::Formula> +fn exists<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula> { map ( @@ -521,7 +544,7 @@ fn exists(i: &str) -> IResult<&str, crate::Formula> )(i) } -fn for_all(i: &str) -> IResult<&str, crate::Formula> +fn for_all<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula> { map ( @@ -552,7 +575,7 @@ fn for_all(i: &str) -> IResult<&str, crate::Formula> )(i) } -fn formula_precedence_1(i: &str) -> IResult<&str, crate::Formula> +fn formula_precedence_1<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula> { alt (( @@ -562,7 +585,7 @@ fn formula_precedence_1(i: &str) -> IResult<&str, crate::Formula> ))(i) } -fn formula_precedence_2(i: &str) -> IResult<&str, crate::Formula> +fn formula_precedence_2<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula> { alt (( @@ -580,7 +603,7 @@ fn formula_precedence_2(i: &str) -> IResult<&str, crate::Formula> ))(i) } -fn formula_precedence_3(i: &str) -> IResult<&str, crate::Formula> +fn formula_precedence_3<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula> { alt (( @@ -599,7 +622,7 @@ fn formula_precedence_3(i: &str) -> IResult<&str, crate::Formula> ))(i) } -fn formula_precedence_4(i: &str) -> IResult<&str, crate::Formula> +fn formula_precedence_4<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula> { alt (( @@ -618,7 +641,7 @@ fn formula_precedence_4(i: &str) -> IResult<&str, crate::Formula> ))(i) } -fn formula_precedence_5(i: &str) -> IResult<&str, crate::Formula> +fn formula_precedence_5<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula> { let (i, left) = formula_precedence_4(i)?; @@ -629,7 +652,7 @@ fn formula_precedence_5(i: &str) -> IResult<&str, crate::Formula> } } -fn formula_precedence_6(i: &str) -> IResult<&str, crate::Formula> +fn formula_precedence_6<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula> { let (i, left) = formula_precedence_5(i)?; @@ -640,12 +663,12 @@ fn formula_precedence_6(i: &str) -> IResult<&str, crate::Formula> } } -pub fn formula(i: &str) -> IResult<&str, crate::Formula> +pub fn formula<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula> { formula_precedence_6(i) } -pub fn formulas(i: &str) -> IResult<&str, Vec> +pub fn formulas<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, Vec> { many0(formula)(i) }