diff --git a/src/ast.rs b/src/ast.rs index b75d806..3c99087 100644 --- a/src/ast.rs +++ b/src/ast.rs @@ -1,6 +1,6 @@ // Operators -#[derive(Clone, Copy, Eq, PartialEq)] +#[derive(Clone, Copy, Eq, Hash, Ord, PartialEq, PartialOrd)] pub enum BinaryOperator { Add, @@ -11,7 +11,7 @@ pub enum BinaryOperator Exponentiate, } -#[derive(Clone, Copy, Eq, PartialEq)] +#[derive(Clone, Copy, Eq, Hash, Ord, PartialEq, PartialOrd)] pub enum ComparisonOperator { Greater, @@ -22,7 +22,7 @@ pub enum ComparisonOperator Equal, } -#[derive(Clone, Copy, Eq, PartialEq)] +#[derive(Clone, Copy, Eq, Hash, Ord, PartialEq, PartialOrd)] pub enum UnaryOperator { AbsoluteValue, @@ -118,6 +118,17 @@ impl std::cmp::Ord for VariableDeclaration } } +impl std::hash::Hash for VariableDeclaration +{ + #[inline(always)] + fn hash(&self, state: &mut H) + { + let p = self as *const VariableDeclaration; + + p.hash(state); + } +} + impl VariableDeclaration { pub fn new(name: String) -> Self @@ -133,6 +144,7 @@ pub type VariableDeclarations = Vec>; // Terms +#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)] pub struct BinaryOperation { pub operator: BinaryOperator, @@ -153,6 +165,7 @@ impl BinaryOperation } } +#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)] pub struct Function { pub declaration: std::rc::Rc, @@ -174,13 +187,14 @@ impl Function } } -#[derive(Clone, Copy, Eq, PartialEq)] +#[derive(Clone, Copy, Eq, Hash, Ord, PartialEq, PartialOrd)] pub enum SpecialInteger { Infimum, Supremum, } +#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)] pub struct UnaryOperation { pub operator: UnaryOperator, @@ -199,6 +213,7 @@ impl UnaryOperation } } +#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)] pub struct Variable { pub declaration: std::rc::Rc, @@ -217,6 +232,7 @@ impl Variable // Formulas +#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)] pub struct Compare { pub operator: ComparisonOperator, @@ -237,6 +253,7 @@ impl Compare } } +#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)] pub struct Exists { pub parameters: std::rc::Rc, @@ -255,6 +272,7 @@ impl Exists } } +#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)] pub struct ForAll { pub parameters: std::rc::Rc, @@ -273,6 +291,7 @@ impl ForAll } } +#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)] pub struct IfAndOnlyIf { pub left: Box, @@ -291,6 +310,7 @@ impl IfAndOnlyIf } } +#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)] pub struct Implies { pub antecedent: Box, @@ -309,6 +329,7 @@ impl Implies } } +#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)] pub struct Predicate { pub declaration: std::rc::Rc, @@ -332,6 +353,7 @@ impl Predicate // Variants +#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)] pub enum Term { BinaryOperation(BinaryOperation), @@ -450,6 +472,7 @@ impl Term } } +#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)] pub enum Formula { And(Formulas), diff --git a/src/parse.rs b/src/parse.rs index 6538ac0..55fdea6 100644 --- a/src/parse.rs +++ b/src/parse.rs @@ -1,6 +1,8 @@ mod names; +mod terms; pub use names::{function_name, predicate_name, variable_name}; +pub use terms::{integer, special_integer}; /* use nom:: diff --git a/src/parse/terms.rs b/src/parse/terms.rs new file mode 100644 index 0000000..a0e1ddd --- /dev/null +++ b/src/parse/terms.rs @@ -0,0 +1,170 @@ +use nom:: +{ + IResult, + branch::alt, + bytes::complete::tag, + character::complete::digit1, + combinator::{map, map_res, opt, recognize}, + sequence::pair, +}; + +pub fn integer(i: &str) -> IResult<&str, crate::Term> +{ + map + ( + map_res + ( + recognize + ( + pair + ( + opt + ( + alt + (( + tag("-"), + tag("+"), + )) + ), + digit1, + ) + ), + std::str::FromStr::from_str, + ), + crate::Term::integer, + )(i) +} + +fn infimum(i: &str) -> IResult<&str, crate::Term> +{ + map + ( + tag("#inf"), + |_| crate::Term::infimum(), + )(i) +} + +fn supremum(i: &str) -> IResult<&str, crate::Term> +{ + map + ( + tag("#sup"), + |_| crate::Term::supremum(), + )(i) +} + +pub fn special_integer(i: &str) -> IResult<&str, crate::Term> +{ + alt + (( + infimum, + supremum, + ))(i) +} + +/* +fn string<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term> +{ + map + ( + delimited + ( + multispace0, + delimited + ( + tag("\""), + is_not("\""), + tag("\""), + ), + multispace0 + ), + |s: &str| crate::Term::String(s.to_string()) + )(i) +} + + +fn function<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula> +{ + alt + (( + function_n_ary, + function_0_ary + ))(i) +} + +fn function_0_ary<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term> +{ + map + ( + delimited(multispace0, function_identifier, multispace0), + |name| crate::Formula::function( + crate::FunctionDeclaration + { + name: name, + arity: 0, + }, + vec![]) + )(i) +} + +fn function_n_ary<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term> +{ + map + ( + pair + ( + delimited(multispace0, function_identifier, multispace0), + delimited + ( + multispace0, + delimited + ( + tag("("), + separated_list(tag(","), term), + tag(")") + ), + multispace0 + ) + ), + |(name, arguments)| crate::Formula::function( + crate::PredicateDeclaration + { + name: name, + arity: arguments.len(), + }, + arguments) + )(i) +} + +*/ + +#[cfg(test)] +mod tests +{ + use crate::parse::*; + + #[test] + fn parse_integer() + { + assert_eq!(integer("0"), Ok(("", crate::Term::integer(0)))); + assert_eq!(integer("10000"), Ok(("", crate::Term::integer(10000)))); + assert_eq!(integer("-10000"), Ok(("", crate::Term::integer(-10000)))); + assert_eq!(integer("1.5"), Ok((".5", crate::Term::integer(1)))); + assert!(integer("a").is_err()); + assert!(integer("-").is_err()); + assert!(integer(" ").is_err()); + } + + #[test] + fn parse_special_integer() + { + assert_eq!(special_integer("#inf"), Ok(("", crate::Term::infimum()))); + assert_eq!(special_integer("#sup"), Ok(("", crate::Term::supremum()))); + assert!(special_integer("inf").is_err()); + assert!(special_integer("sup").is_err()); + assert!(special_integer("0").is_err()); + assert!(special_integer("10000").is_err()); + assert!(special_integer("-10000").is_err()); + assert!(special_integer(" ").is_err()); + } +}