2025-05-14 11:42:19 +02:00
|
|
|
use std::str::FromStr;
|
|
|
|
|
use lalrpop_util::ParseError;
|
2025-05-14 12:14:13 +02:00
|
|
|
use crate::rsprocess::{RSset, RSprocess, RSenvironment, RSassert, RSassertOp, RSBHML};
|
2025-05-14 11:42:19 +02:00
|
|
|
|
|
|
|
|
grammar;
|
|
|
|
|
|
2025-05-14 12:14:13 +02:00
|
|
|
// matches words (letter followed by numbers, letters or _)
|
2025-05-14 11:42:19 +02:00
|
|
|
Literal = { r"[[:alpha:]][[:word:]]*" };
|
|
|
|
|
|
2025-05-14 12:14:13 +02:00
|
|
|
// all numbers are i64
|
2025-05-14 11:42:19 +02:00
|
|
|
Num: i64 = {
|
|
|
|
|
r"[0-9]+" =>? i64::from_str(<>)
|
|
|
|
|
.map_err(|_| ParseError::User { error: "Number is too big" })
|
|
|
|
|
};
|
|
|
|
|
|
2025-05-14 12:14:13 +02:00
|
|
|
// macro for matching sequence of patterns with C as separator
|
|
|
|
|
Separeted<T, C>: Vec<T> = {
|
2025-05-14 11:42:19 +02:00
|
|
|
<mut v:(<T> C)+> <e:T?> => match e {
|
|
|
|
|
None => v,
|
|
|
|
|
Some(e) => {
|
|
|
|
|
v.push(e);
|
|
|
|
|
v
|
|
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
};
|
|
|
|
|
|
2025-05-14 12:14:13 +02:00
|
|
|
// ----- SetParser -----
|
|
|
|
|
pub Set: RSset<'input> = {
|
2025-05-14 11:42:19 +02:00
|
|
|
<s: Set_of_entities> => s
|
|
|
|
|
};
|
|
|
|
|
|
2025-05-14 12:14:13 +02:00
|
|
|
// ----- ContextParser -----
|
2025-05-14 11:42:19 +02:00
|
|
|
pub Context: Box<RSprocess<'input>> = {
|
|
|
|
|
"[" "]" => Box::new(RSprocess::Nill),
|
|
|
|
|
"[" <t: CTX_process> "]" => Box::new(t),
|
2025-05-14 12:14:13 +02:00
|
|
|
"[" <t: Separeted<CTX_process, ",">> "]" => Box::new(RSprocess::NondeterministicChoice{children: t})
|
2025-05-14 11:42:19 +02:00
|
|
|
};
|
|
|
|
|
|
|
|
|
|
CTX_process: RSprocess<'input> = {
|
|
|
|
|
<c: Set_of_entities> "." <k: CTX_process> => RSprocess::EntitySet{entities: c, next_process: Box::new(k)},
|
|
|
|
|
"(" <k: CTX_process> ")" => k,
|
2025-05-14 12:14:13 +02:00
|
|
|
"(" <k: Separeted<CTX_process, "+">> ")" => RSprocess::Summation{children: k},
|
2025-05-14 11:42:19 +02:00
|
|
|
"<" <n: Num> <k1: CTX_process> ">" "." <k: CTX_process> => RSprocess::WaitEntity{repeat: n, repeated_process: Box::new(k1), next_process: Box::new(k)},
|
|
|
|
|
"nil" => RSprocess::Nill,
|
|
|
|
|
<identifier: Literal> => RSprocess::ConstantIdentifier{identifier: identifier}
|
|
|
|
|
};
|
|
|
|
|
|
2025-05-14 12:14:13 +02:00
|
|
|
Set_of_entities: RSset<'input> = {
|
|
|
|
|
"{" "}" => RSset::from(vec![]),
|
|
|
|
|
"{" <t: Literal> "}" => RSset::from(vec![t]),
|
|
|
|
|
"{" <t: Separeted<Literal, ",">> "}" => RSset::from(t)
|
2025-05-14 11:42:19 +02:00
|
|
|
};
|
|
|
|
|
|
2025-05-14 12:14:13 +02:00
|
|
|
// ----- EnvironmentParser -----
|
2025-05-14 11:42:19 +02:00
|
|
|
pub Environment: Box<RSenvironment<'input>> = {
|
|
|
|
|
"[" "]" => Box::new(RSenvironment::new()),
|
2025-05-14 12:14:13 +02:00
|
|
|
"[" <t: Separeted<Env_term, ",">> "]" => Box::new(RSenvironment::from(t))
|
2025-05-14 11:42:19 +02:00
|
|
|
};
|
|
|
|
|
|
|
|
|
|
Env_term: (&'input str, Box<RSprocess<'input>>) = {
|
|
|
|
|
<identifier: Literal> "=" <k: CTX_process> => (identifier, Box::new(k))
|
|
|
|
|
};
|
|
|
|
|
|
2025-05-14 12:14:13 +02:00
|
|
|
// ----- AssertParser -----
|
2025-05-14 11:42:19 +02:00
|
|
|
pub Assert: Box<RSassert<'input>> = {
|
|
|
|
|
<f: Formula_Assert> => Box::new(f)
|
|
|
|
|
};
|
|
|
|
|
|
|
|
|
|
Formula_Assert: RSassert<'input> = {
|
|
|
|
|
"-" <f: Formula_Assert> => RSassert::Not(Box::new(f)),
|
|
|
|
|
"(" <f1: Formula_Assert> "^" <f2: Formula_Assert> ")" => RSassert::Xor(Box::new(f1), Box::new(f2)),
|
2025-05-14 12:14:13 +02:00
|
|
|
"(" <f: Separeted<Formula_Assert, "\\/">> ")" => RSassert::Or(f),
|
|
|
|
|
"(" <f: Separeted<Formula_Assert, "/\\">> ")" => RSassert::And(f),
|
2025-05-14 11:42:19 +02:00
|
|
|
<c: Set_of_entities> "inW" => RSassert::Sub(c, RSassertOp::InW),
|
|
|
|
|
<c: Set_of_entities> "inR" => RSassert::Sub(c, RSassertOp::InR),
|
|
|
|
|
<c: Set_of_entities> "inI" => RSassert::Sub(c, RSassertOp::InI),
|
|
|
|
|
<c: Set_of_entities> "inP" => RSassert::Sub(c, RSassertOp::InP),
|
|
|
|
|
"?" "inW" => RSassert::NonEmpty(RSassertOp::InW),
|
|
|
|
|
"?" "inR" => RSassert::NonEmpty(RSassertOp::InR),
|
|
|
|
|
"?" "inI" => RSassert::NonEmpty(RSassertOp::InI),
|
|
|
|
|
"?" "inP" => RSassert::NonEmpty(RSassertOp::InP),
|
|
|
|
|
};
|
|
|
|
|
|
2025-05-14 12:14:13 +02:00
|
|
|
// ----- BHMLParser -----
|
2025-05-14 11:42:19 +02:00
|
|
|
pub BHML: Box<RSBHML<'input>> = {
|
|
|
|
|
<g: Formula_BHML> => Box::new(g)
|
|
|
|
|
};
|
|
|
|
|
|
|
|
|
|
Formula_BHML: RSBHML<'input> = {
|
|
|
|
|
"true" => RSBHML::True,
|
|
|
|
|
"false" => RSBHML::False,
|
2025-05-14 12:14:13 +02:00
|
|
|
"(" <g: Separeted<Formula_BHML, "\\/">> ")" => RSBHML::Or(g),
|
|
|
|
|
"(" <g: Separeted<Formula_BHML, "/\\">> ")" => RSBHML::And(g),
|
2025-05-14 11:42:19 +02:00
|
|
|
"<" <f: Formula_Assert> ">" <g: Formula_BHML> => RSBHML::Diamond(Box::new(f), Box::new(g)),
|
|
|
|
|
"[" <f: Formula_Assert> "]" <g: Formula_BHML> => RSBHML::Box(Box::new(f), Box::new(g)),
|
|
|
|
|
};
|