use crate::prelude::*;
impl Runtime {
pub fn parse_fact(&mut self, tb: &mut TokenBlock) -> Result<Fact, RuntimeError> {
match tb.current()? {
FORALL => self.parse_forall_or_forall_with_iff(tb),
_ => {
let or_and_spec_fact = self.parse_exist_or_and_chain_atomic_fact(tb)?;
Ok(or_and_spec_fact.to_fact())
}
}
}
fn parse_forall_or_forall_with_iff(
&mut self,
tb: &mut TokenBlock,
) -> Result<Fact, RuntimeError> {
self.run_in_local_parsing_time_name_scope(|this| {
tb.skip_token(FORALL)?;
let mut param_def: Vec<ParamGroupWithParamType> = vec![];
while tb.current()? != COLON {
param_def.push(this.parse_param_def_with_param_type_and_skip_comma(tb)?);
}
let forall_param_names = ParamGroupWithParamType::collect_param_names(¶m_def);
this.register_collected_param_names_for_def_parse(
&forall_param_names,
tb.line_file.clone(),
)?;
tb.skip_token(COLON)?;
let last_body = tb.body.last().ok_or_else(|| {
RuntimeError::new_parse_error_with_msg_position_previous_error(
"Expected body".to_string(),
tb.line_file.clone(),
None,
)
})?;
if last_body.current()? == EQUIVALENT_SIGN {
this.parse_forall_with_iff(tb, param_def)
} else {
this.parse_forall(tb, param_def)
}
})
}
fn parse_forall_with_iff(
&mut self,
tb: &mut TokenBlock,
param_def: Vec<ParamGroupWithParamType>,
) -> Result<Fact, RuntimeError> {
if tb.body.len() < 2 {
return Err(
RuntimeError::new_parse_error_with_msg_position_previous_error(
"Expected at least 2 body blocks".to_string(),
tb.line_file.clone(),
None,
),
);
}
let mut dom_facts: Vec<ExistOrAndChainAtomicFact> = Vec::new();
let mut then_facts: Vec<ExistOrAndChainAtomicFact> = Vec::new();
let mut iff_facts: Vec<ExistOrAndChainAtomicFact> = Vec::new();
let body_len = tb.body.len();
let iff_block = tb.body.get_mut(body_len - 1).ok_or_else(|| {
RuntimeError::new_parse_error_with_msg_position_previous_error(
"Expected <=>: block in forall body".to_string(),
tb.line_file.clone(),
None,
)
})?;
iff_block.skip_token_and_colon_and_exceed_end_of_head(EQUIVALENT_SIGN)?;
for block in iff_block.body.iter_mut() {
iff_facts.push(self.parse_exist_or_and_chain_atomic_fact(block)?);
}
let then_block = tb.body.get_mut(body_len - 2).ok_or_else(|| {
RuntimeError::new_parse_error_with_msg_position_previous_error(
"Expected =>: block in forall body".to_string(),
tb.line_file.clone(),
None,
)
})?;
then_block.skip_token_and_colon_and_exceed_end_of_head(RIGHT_ARROW)?;
for block in then_block.body.iter_mut() {
then_facts.push(self.parse_exist_or_and_chain_atomic_fact(block)?);
}
for block in tb.body.iter_mut().take(body_len - 2) {
dom_facts.push(self.parse_exist_or_and_chain_atomic_fact(block)?);
}
let forall_fact = ForallFact::new(param_def, dom_facts, then_facts, tb.line_file.clone());
Ok(Fact::ForallFactWithIff(ForallFactWithIff::new(
forall_fact,
iff_facts,
tb.line_file.clone(),
)))
}
fn parse_forall(
&mut self,
tb: &mut TokenBlock,
param_def: Vec<ParamGroupWithParamType>,
) -> Result<Fact, RuntimeError> {
let last_body = tb.body.last().ok_or_else(|| {
RuntimeError::new_parse_error_with_msg_position_previous_error(
"Expected body".to_string(),
tb.line_file.clone(),
None,
)
})?;
if last_body.current()? == RIGHT_ARROW {
let mut dom_facts: Vec<ExistOrAndChainAtomicFact> = vec![];
let n = tb.body.len();
for block in tb.body.iter_mut().take(n - 1) {
dom_facts.push(self.parse_exist_or_and_chain_atomic_fact(block)?);
}
let last = tb.body.last_mut().ok_or_else(|| {
RuntimeError::new_parse_error_with_msg_position_previous_error(
"Expected body".to_string(),
tb.line_file.clone(),
None,
)
})?;
last.skip_token_and_colon_and_exceed_end_of_head(RIGHT_ARROW)?;
let mut then_facts: Vec<ExistOrAndChainAtomicFact> = Vec::new();
for block in last.body.iter_mut() {
then_facts.push(self.parse_exist_or_and_chain_atomic_fact(block)?);
}
Ok(Fact::ForallFact(ForallFact::new(
param_def,
dom_facts,
then_facts,
tb.line_file.clone(),
)))
} else {
let mut then_facts: Vec<ExistOrAndChainAtomicFact> = Vec::new();
for block in tb.body.iter_mut() {
then_facts.push(self.parse_exist_or_and_chain_atomic_fact(block)?);
}
Ok(Fact::ForallFact(ForallFact::new(
param_def,
vec![],
then_facts,
tb.line_file.clone(),
)))
}
}
pub fn parse_and_chain_atomic_fact(
&mut self,
tb: &mut TokenBlock,
) -> Result<AndChainAtomicFact, RuntimeError> {
let first = self.parse_chain_atomic(tb, true)?;
match first {
ChainAtomicFact::ChainFact(c) => return Ok(AndChainAtomicFact::ChainFact(c)),
ChainAtomicFact::AtomicFact(a) => {
let mut collected: Vec<AtomicFact> = vec![a];
while !tb.exceed_end_of_head() && tb.current()? == AND {
tb.skip_token(AND)?;
let next = self.parse_atomic_fact(tb, true)?;
collected.push(next);
}
if collected.len() == 1 {
return Ok(AndChainAtomicFact::AtomicFact(collected.remove(0)));
}
Ok(AndChainAtomicFact::AndFact(AndFact::new(
collected,
tb.line_file.clone(),
)))
}
}
}
pub fn parse_exist_fact(&mut self, tb: &mut TokenBlock) -> Result<ExistFact, RuntimeError> {
self.run_in_local_parsing_time_name_scope(|this| {
tb.skip_token(EXIST)?;
let mut param_def: Vec<ParamGroupWithParamType> = vec![];
while tb.current()? != ST {
param_def.push(this.parse_param_def_with_param_type_and_skip_comma(tb)?);
}
let exist_param_names = ParamGroupWithParamType::collect_param_names(¶m_def);
this.run_in_local_parsing_time_name_scope(move |inner| {
inner.register_collected_param_names_for_def_parse(
&exist_param_names,
tb.line_file.clone(),
)?;
tb.skip_token(ST)?;
tb.skip_token(LEFT_CURLY_BRACE)?;
let mut facts: Vec<OrAndChainAtomicFact> = vec![];
loop {
facts.push(inner.parse_or_and_chain_atomic_fact(tb)?);
if tb.current()? != RIGHT_CURLY_BRACE {
tb.skip_token(COMMA)?;
} else {
break;
}
}
tb.skip_token(RIGHT_CURLY_BRACE)?;
let line_file = tb.line_file.clone();
Ok(ExistFact::new(param_def, facts, line_file))
})
})
}
pub fn parse_facts_in_body(&mut self, tb: &mut TokenBlock) -> Result<Vec<Fact>, RuntimeError> {
let mut facts: Vec<Fact> = vec![];
for block in tb.body.iter_mut() {
facts.push(self.parse_fact(block)?);
}
Ok(facts)
}
pub fn parse_exist_or_and_chain_atomic_fact(
&mut self,
tb: &mut TokenBlock,
) -> Result<ExistOrAndChainAtomicFact, RuntimeError> {
match tb.current()? {
EXIST => {
let exist_fact = self.parse_exist_fact(tb)?;
Ok(ExistOrAndChainAtomicFact::ExistFact(exist_fact))
}
NOT => {
tb.skip_token(NOT)?;
Ok(self
.parse_atomic_fact(tb, false)
.map(|a| ExistOrAndChainAtomicFact::AtomicFact(a))?)
}
_ => Ok(self
.parse_or_and_chain_atomic_fact(tb)?
.to_exist_or_and_chain_atomic_fact()),
}
}
pub fn parse_atomic_fact(
&mut self,
tb: &mut TokenBlock,
is_true: bool,
) -> Result<AtomicFact, RuntimeError> {
if tb.current()? == NOT {
tb.skip_token(NOT)?;
return Ok(self.parse_atomic_fact(tb, !is_true)?);
}
let line_file = tb.line_file.clone();
if tb.current()? == FACT_PREFIX {
tb.skip_token(FACT_PREFIX)?;
let prop = self.parse_identifier_or_identifier_with_mod(tb)?;
let args = self.parse_braced_objs(tb)?;
let atomic = AtomicFact::to_atomic_fact(prop, is_true, args, line_file).map_err(
|e: RuntimeErrorStruct| {
RuntimeError::new_parse_error_with_msg_position_previous_error(
e.msg.clone(),
tb.line_file.clone(),
None,
)
},
)?;
return Ok(atomic);
}
let first_obj = self.parse_obj(tb)?;
if tb.exceed_end_of_head() {
return Err(
RuntimeError::new_parse_error_with_msg_position_previous_error(
"Expected operator or $prop in atomic fact".to_string(),
tb.line_file.clone(),
None,
),
);
}
let tok = tb.current()?.to_string();
let prop = if is_comparison_str(&tok) {
tb.advance()?;
IdentifierOrIdentifierWithMod::Identifier(Identifier::new(tok.clone()))
} else if tok == FACT_PREFIX {
tb.skip_token(FACT_PREFIX)?;
self.parse_identifier_or_identifier_with_mod(tb)?
} else {
return Err(
RuntimeError::new_parse_error_with_msg_position_previous_error(
"Expected operator or $prop in atomic fact".to_string(),
tb.line_file.clone(),
None,
),
);
};
let next_obj = self.parse_obj(tb)?;
let args = vec![first_obj, next_obj];
let atomic = AtomicFact::to_atomic_fact(prop, is_true, args, line_file).map_err(
|e: RuntimeErrorStruct| {
RuntimeError::new_parse_error_with_msg_position_previous_error(
e.msg.clone(),
tb.line_file.clone(),
None,
)
},
)?;
Ok(atomic)
}
pub fn parse_or_and_chain_atomic_fact(
&mut self,
tb: &mut TokenBlock,
) -> Result<OrAndChainAtomicFact, RuntimeError> {
let first = self.parse_and_chain_atomic_fact(tb)?;
let mut list: Vec<AndChainAtomicFact> = vec![first];
while !tb.exceed_end_of_head() && tb.current()? == OR {
tb.skip_token(OR)?;
list.push(self.parse_and_chain_atomic_fact(tb)?);
}
if list.len() == 1 {
return Ok(match list.remove(0) {
AndChainAtomicFact::AtomicFact(a) => OrAndChainAtomicFact::AtomicFact(a),
AndChainAtomicFact::AndFact(a) => OrAndChainAtomicFact::AndFact(a),
AndChainAtomicFact::ChainFact(c) => OrAndChainAtomicFact::ChainFact(c),
});
}
Ok(OrAndChainAtomicFact::OrFact(OrFact::new(
list,
tb.line_file.clone(),
)))
}
pub fn parse_chain_atomic(
&mut self,
tb: &mut TokenBlock,
is_true: bool,
) -> Result<ChainAtomicFact, RuntimeError> {
let line_file = tb.line_file.clone();
if tb.current()? == FACT_PREFIX {
tb.skip_token(FACT_PREFIX)?;
let prop = self.parse_identifier_or_identifier_with_mod(tb)?;
let args = self.parse_braced_objs(tb)?;
let atomic = AtomicFact::to_atomic_fact(prop, is_true, args, line_file).map_err(
|e: RuntimeErrorStruct| {
RuntimeError::new_parse_error_with_msg_position_previous_error(
e.msg.clone(),
tb.line_file.clone(),
None,
)
},
)?;
return Ok(ChainAtomicFact::AtomicFact(atomic));
}
let first_obj = self.parse_obj(tb)?;
let mut objs: Vec<crate::obj::Obj> = vec![first_obj];
let mut prop_names: Vec<IdentifierOrIdentifierWithMod> = vec![];
while !tb.exceed_end_of_head() {
let tok = tb.current()?.to_string();
let prop = if is_comparison_str(&tok) {
tb.advance()?;
IdentifierOrIdentifierWithMod::Identifier(Identifier::new(tok.clone()))
} else if tok == FACT_PREFIX {
tb.skip_token(FACT_PREFIX)?;
self.parse_identifier_or_identifier_with_mod(tb)?
} else {
break;
};
let next_obj = self.parse_obj(tb)?;
prop_names.push(prop);
objs.push(next_obj);
}
if prop_names.is_empty() {
return Err(
RuntimeError::new_parse_error_with_msg_position_previous_error(
"Expected operator or $prop in fact".to_string(),
tb.line_file.clone(),
None,
),
);
}
if !is_true && (objs.len() > 2 || prop_names.len() > 1) {
return Err(
RuntimeError::new_parse_error_with_msg_position_previous_error(
"Negated fact must be single atomic (one operator)".to_string(),
tb.line_file.clone(),
None,
),
);
}
if objs.len() == 2 && prop_names.len() == 1 {
let prop = prop_names.remove(0);
let args = objs;
let atomic = AtomicFact::to_atomic_fact(prop, is_true, args, line_file).map_err(
|e: RuntimeErrorStruct| {
RuntimeError::new_parse_error_with_msg_position_previous_error(
e.msg.clone(),
tb.line_file.clone(),
None,
)
},
)?;
return Ok(ChainAtomicFact::AtomicFact(atomic));
}
Ok(ChainAtomicFact::ChainFact(ChainFact::new(
objs, prop_names, line_file,
)))
}
}