Start parsing terms
This commit is contained in:
parent
0c057211ed
commit
896af02120
31
src/ast.rs
31
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<H: std::hash::Hasher>(&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<std::rc::Rc<VariableDeclaration>>;
|
||||
|
||||
// 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<FunctionDeclaration>,
|
||||
@ -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<VariableDeclaration>,
|
||||
@ -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<VariableDeclarations>,
|
||||
@ -255,6 +272,7 @@ impl Exists
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
|
||||
pub struct ForAll
|
||||
{
|
||||
pub parameters: std::rc::Rc<VariableDeclarations>,
|
||||
@ -273,6 +291,7 @@ impl ForAll
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
|
||||
pub struct IfAndOnlyIf
|
||||
{
|
||||
pub left: Box<Formula>,
|
||||
@ -291,6 +310,7 @@ impl IfAndOnlyIf
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
|
||||
pub struct Implies
|
||||
{
|
||||
pub antecedent: Box<Formula>,
|
||||
@ -309,6 +329,7 @@ impl Implies
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
|
||||
pub struct Predicate
|
||||
{
|
||||
pub declaration: std::rc::Rc<PredicateDeclaration>,
|
||||
@ -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),
|
||||
|
@ -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::
|
||||
|
170
src/parse/terms.rs
Normal file
170
src/parse/terms.rs
Normal file
@ -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());
|
||||
}
|
||||
}
|
Loading…
Reference in New Issue
Block a user