use crate::{
AbstractClassValueProvenanceNodeV0, AbstractClassValueProvenanceTreeV0,
AbstractClassValueProvenanceV0, AbstractClassValueV0, abstract_class_value_kind, automaton_key,
};
use omena_evidence_graph::{
EvidenceDemandEdgeV0, EvidenceGraphBuildErrorV0, EvidenceGraphV0, EvidenceNodeKeyV0,
EvidenceNodeSeedV0, GuaranteeKindV0, build_evidence_graph_from_edges_v0,
};
const ABSTRACT_VALUE_PROVENANCE_EDGE_KIND_V0: &str = "abstract-value-provenance";
pub fn summarize_abstract_class_value_provenance_tree(
value: &AbstractClassValueV0,
) -> AbstractClassValueProvenanceTreeV0 {
let value_kind = abstract_class_value_kind(value);
let value_provenance = abstract_class_value_provenance(value);
AbstractClassValueProvenanceTreeV0 {
schema_version: "0",
product: "omena-abstract-value.provenance-tree",
value_kind,
value: value.clone(),
value_provenance,
root: AbstractClassValueProvenanceNodeV0 {
operation: root_operation(value, value_provenance),
result_kind: value_kind,
result_provenance: value_provenance,
detail: root_detail(value),
reason: root_reason(value, value_provenance),
children: constraint_children(value),
},
}
}
impl AbstractClassValueProvenanceTreeV0 {
pub fn evidence_node_key(&self) -> EvidenceNodeKeyV0 {
EvidenceNodeKeyV0::new(
self.product,
format!(
"{}:{}:{}",
self.value_kind,
self.root.operation,
self.root.detail.as_deref().unwrap_or("no-detail")
),
)
}
pub fn evidence_node_seed(&self) -> EvidenceNodeSeedV0 {
let mut provenance = vec![
self.product.to_string(),
self.value_kind.to_string(),
self.root.operation.to_string(),
];
if let Some(result_provenance) = self.root.result_provenance {
provenance.push(format!("{result_provenance:?}"));
}
EvidenceNodeSeedV0::new(
self.evidence_node_key(),
provenance,
GuaranteeKindV0::for_label_less_family(),
)
}
pub fn evidence_demand_edge(&self) -> EvidenceDemandEdgeV0 {
EvidenceDemandEdgeV0::new(
self.product,
self.evidence_node_key(),
ABSTRACT_VALUE_PROVENANCE_EDGE_KIND_V0,
)
}
pub fn evidence_graph(&self) -> Result<EvidenceGraphV0, EvidenceGraphBuildErrorV0> {
build_evidence_graph_from_edges_v0(
[self.evidence_node_seed()],
[self.evidence_demand_edge()],
)
}
}
fn abstract_class_value_provenance(
value: &AbstractClassValueV0,
) -> Option<AbstractClassValueProvenanceV0> {
match value {
AbstractClassValueV0::Prefix { provenance, .. }
| AbstractClassValueV0::Suffix { provenance, .. }
| AbstractClassValueV0::PrefixSuffix { provenance, .. }
| AbstractClassValueV0::CharInclusion { provenance, .. }
| AbstractClassValueV0::Composite { provenance, .. }
| AbstractClassValueV0::Automaton { provenance, .. }
| AbstractClassValueV0::Top { provenance } => *provenance,
_ => None,
}
}
fn root_operation(
value: &AbstractClassValueV0,
provenance: Option<AbstractClassValueProvenanceV0>,
) -> &'static str {
match provenance {
Some(AbstractClassValueProvenanceV0::FiniteSetWideningChars)
| Some(AbstractClassValueProvenanceV0::FiniteSetWideningComposite)
| Some(AbstractClassValueProvenanceV0::FiniteSetWideningAutomaton) => "finiteSetWidening",
Some(AbstractClassValueProvenanceV0::AutomatonJoin) => "automatonJoin",
Some(AbstractClassValueProvenanceV0::AutomatonConcat) => "automatonConcat",
Some(AbstractClassValueProvenanceV0::PrefixJoinLcp) => "prefixJoinLongestCommonPrefix",
Some(AbstractClassValueProvenanceV0::SuffixJoinLcs) => "suffixJoinLongestCommonSuffix",
Some(AbstractClassValueProvenanceV0::PrefixSuffixJoin)
| Some(AbstractClassValueProvenanceV0::CompositeJoin) => "reducedProductJoin",
Some(AbstractClassValueProvenanceV0::CompositeConcat) => "reducedProductConcat",
Some(AbstractClassValueProvenanceV0::UnconstrainedInput) => "unconstrainedInput",
Some(AbstractClassValueProvenanceV0::AutomatonStateLimit) => "automatonStateWidening",
Some(AbstractClassValueProvenanceV0::FlowIterationLimit) => "flowIterationWidening",
Some(AbstractClassValueProvenanceV0::MissingFlowPredecessor) => "missingFlowPredecessor",
Some(AbstractClassValueProvenanceV0::JoinUnrepresentable) => "unrepresentableJoin",
Some(AbstractClassValueProvenanceV0::ConcatenationUnrepresentable) => {
"unrepresentableConcatenation"
}
Some(AbstractClassValueProvenanceV0::ReducedProductUnconstrained) => {
"reducedProductUnconstrained"
}
None => match value {
AbstractClassValueV0::Bottom => "bottomDomain",
AbstractClassValueV0::Exact { .. } => "exactLiteral",
AbstractClassValueV0::FiniteSet { .. } => "finiteSetDomain",
AbstractClassValueV0::Automaton { .. } => "automatonDomain",
AbstractClassValueV0::Prefix { .. }
| AbstractClassValueV0::Suffix { .. }
| AbstractClassValueV0::PrefixSuffix { .. }
| AbstractClassValueV0::CharInclusion { .. }
| AbstractClassValueV0::Composite { .. } => "constraintDomain",
AbstractClassValueV0::Top { .. } => "topDomain",
},
}
}
fn root_reason(
value: &AbstractClassValueV0,
provenance: Option<AbstractClassValueProvenanceV0>,
) -> &'static str {
match provenance {
Some(AbstractClassValueProvenanceV0::FiniteSetWideningChars) => {
"large finite set widened to character constraints"
}
Some(AbstractClassValueProvenanceV0::FiniteSetWideningComposite) => {
"large finite set widened to preserved edge and character constraints"
}
Some(AbstractClassValueProvenanceV0::FiniteSetWideningAutomaton) => {
"large finite set widened to a bounded deterministic string automaton"
}
Some(AbstractClassValueProvenanceV0::AutomatonJoin) => {
"finite string languages were merged through automaton union"
}
Some(AbstractClassValueProvenanceV0::AutomatonConcat) => {
"finite string languages were concatenated through automaton composition"
}
Some(AbstractClassValueProvenanceV0::PrefixJoinLcp) => {
"branch merge retained the meaningful longest common prefix"
}
Some(AbstractClassValueProvenanceV0::SuffixJoinLcs) => {
"branch merge retained the meaningful longest common suffix"
}
Some(AbstractClassValueProvenanceV0::PrefixSuffixJoin)
| Some(AbstractClassValueProvenanceV0::CompositeJoin) => {
"reduced product combined compatible constraints from multiple domains"
}
Some(AbstractClassValueProvenanceV0::CompositeConcat) => {
"reduced product concatenated compatible constraints without widening to top"
}
Some(AbstractClassValueProvenanceV0::UnconstrainedInput) => {
"the producing input did not provide a finite class-value constraint"
}
Some(AbstractClassValueProvenanceV0::AutomatonStateLimit) => {
"the finite language exceeded the bounded automaton state limit"
}
Some(AbstractClassValueProvenanceV0::FlowIterationLimit) => {
"the class-value flow did not converge within its iteration limit"
}
Some(AbstractClassValueProvenanceV0::MissingFlowPredecessor) => {
"a referenced flow predecessor was unavailable"
}
Some(AbstractClassValueProvenanceV0::JoinUnrepresentable) => {
"the joined class-value constraints had no sound bounded representation"
}
Some(AbstractClassValueProvenanceV0::ConcatenationUnrepresentable) => {
"the concatenated class-value constraints had no sound bounded representation"
}
Some(AbstractClassValueProvenanceV0::ReducedProductUnconstrained) => {
"the reduced product retained no constraining axis"
}
None => match value {
AbstractClassValueV0::Bottom => "no class value can satisfy the current constraints",
AbstractClassValueV0::Exact { .. } => "the class value is known exactly",
AbstractClassValueV0::FiniteSet { .. } => "the class value is one of a bounded set",
AbstractClassValueV0::Automaton { .. } => {
"the class value is represented by a bounded deterministic string automaton"
}
AbstractClassValueV0::Prefix { .. }
| AbstractClassValueV0::Suffix { .. }
| AbstractClassValueV0::PrefixSuffix { .. }
| AbstractClassValueV0::CharInclusion { .. }
| AbstractClassValueV0::Composite { .. } => {
"the class value is represented by explicit domain constraints"
}
AbstractClassValueV0::Top { .. } => "the class value is unconstrained",
},
}
}
fn root_detail(value: &AbstractClassValueV0) -> Option<String> {
match value {
AbstractClassValueV0::Exact { value } => Some(format!("value={value}")),
AbstractClassValueV0::FiniteSet { values } => Some(format!("valueCount={}", values.len())),
AbstractClassValueV0::Automaton { automaton, .. } => Some(format!(
"stateCount={},transitionCount={},key={}",
automaton.state_count,
automaton.transitions.len(),
automaton_key(automaton)
)),
_ => None,
}
}
fn constraint_children(value: &AbstractClassValueV0) -> Vec<AbstractClassValueProvenanceNodeV0> {
let mut children = Vec::new();
match value {
AbstractClassValueV0::Prefix { prefix, .. } => {
children.push(constraint_node(
"prefixConstraint",
"prefix",
prefix.clone(),
));
}
AbstractClassValueV0::Suffix { suffix, .. } => {
children.push(constraint_node(
"suffixConstraint",
"suffix",
suffix.clone(),
));
}
AbstractClassValueV0::PrefixSuffix {
prefix,
suffix,
min_length,
..
} => {
children.push(constraint_node(
"prefixConstraint",
"prefix",
prefix.clone(),
));
children.push(constraint_node(
"suffixConstraint",
"suffix",
suffix.clone(),
));
children.push(constraint_node(
"lengthConstraint",
"minLength",
min_length.to_string(),
));
}
AbstractClassValueV0::CharInclusion {
must_chars,
may_chars,
may_include_other_chars,
..
} => {
push_char_constraint_children(
&mut children,
must_chars,
may_chars,
*may_include_other_chars,
);
}
AbstractClassValueV0::Composite {
prefix,
suffix,
min_length,
must_chars,
may_chars,
may_include_other_chars,
..
} => {
if let Some(prefix) = prefix {
children.push(constraint_node(
"prefixConstraint",
"prefix",
prefix.clone(),
));
}
if let Some(suffix) = suffix {
children.push(constraint_node(
"suffixConstraint",
"suffix",
suffix.clone(),
));
}
if let Some(min_length) = min_length {
children.push(constraint_node(
"lengthConstraint",
"minLength",
min_length.to_string(),
));
}
push_char_constraint_children(
&mut children,
must_chars,
may_chars,
*may_include_other_chars,
);
}
AbstractClassValueV0::Bottom
| AbstractClassValueV0::Exact { .. }
| AbstractClassValueV0::FiniteSet { .. }
| AbstractClassValueV0::Automaton { .. }
| AbstractClassValueV0::Top { .. } => {}
}
children
}
fn push_char_constraint_children(
children: &mut Vec<AbstractClassValueProvenanceNodeV0>,
must_chars: &str,
may_chars: &str,
may_include_other_chars: bool,
) {
if !must_chars.is_empty() {
children.push(constraint_node(
"characterMustConstraint",
"mustChars",
must_chars.to_string(),
));
}
if !may_include_other_chars {
children.push(constraint_node(
"characterMayConstraint",
"mayChars",
may_chars.to_string(),
));
}
}
fn constraint_node(
operation: &'static str,
label: &'static str,
value: String,
) -> AbstractClassValueProvenanceNodeV0 {
AbstractClassValueProvenanceNodeV0 {
operation,
result_kind: "constraint",
result_provenance: None,
detail: Some(format!("{label}={value}")),
reason: "constraint retained by the abstract value domain",
children: Vec::new(),
}
}