1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
use crate::prelude::*;
impl Runtime {
/// If the fact string is in the known-facts cache, return the cached verification result.
pub fn verify_fact_from_cache_using_display_string(&self, fact: &Fact) -> Option<StmtResult> {
let key = fact.to_string();
let (cache_ok, cache_line_file) = self.cache_known_facts_contains(&key);
if cache_ok {
Some(
(FactualStmtSuccess::new_with_verified_by_known_fact_source_recording_facts(
fact.clone(),
key,
None,
Some(cache_line_file),
Vec::new(),
))
.into(),
)
} else {
None
}
}
/// If check_type_nonempty is true and param_type is Obj(set), verifies that the set is nonempty and stores the fact.
pub fn verify_param_type_nonempty_if_required(
&mut self,
param_type: &ParamType,
check_type_nonempty: bool,
) -> Result<(), RuntimeError> {
if !check_type_nonempty {
return Ok(());
}
match param_type {
ParamType::Set(_) | ParamType::NonemptySet(_) | ParamType::FiniteSet(_) => Ok(()),
ParamType::Obj(param_set) => match param_set {
Obj::FnSet(fn_set) => {
let ret_nonempty = IsNonemptySetFact::new(
fn_set.ret_set.as_ref().clone(),
default_line_file(),
)
.into();
self.verify_fact_well_defined_and_store_and_infer(
ret_nonempty,
&VerifyState::new(2, false),
)?;
Ok(())
}
Obj::SetBuilder(_) => Err(RuntimeError::ExecStmtError(RuntimeErrorStruct::new(
None,
"set builder param type is not supported yet in verify_param_type_nonempty_if_required"
.to_string(),
default_line_file(),
None,
vec![],
))),
_ => {
let nonempty_fact =
IsNonemptySetFact::new(param_set.clone(), default_line_file());
let ret= self.verify_fact(
&nonempty_fact.into(),
&VerifyState::new(0, false),
)?;
if ret.is_unknown() {
return Err(RuntimeError::from(VerifyRuntimeError(RuntimeErrorStruct::new(
None,
"param type is not nonempty".to_string(),
default_line_file(),
None,
vec![],
))));
}
Ok(())
}
},
}
}
}