use omena_cascade::{
BoxLonghandInputV0, LayerFlattenInputV0, ScopeFlattenInputV0, StaticSupportsAssumptionV0,
StaticSupportsEvalVerdictV0, evaluate_static_supports_condition,
prove_box_shorthand_combination, prove_layer_flatten_candidate, prove_scope_flatten_candidate,
};
use crate::{
CanonicalSmtInputV0, CascadeSMTProofV0, SmtBackendV0, canonical_smt_input_v0,
proof::cascade_smt_proof_v0,
};
pub fn smt_prove_box_shorthand_combination_v0<B: SmtBackendV0>(
shorthand_property: &str,
longhands: &[BoxLonghandInputV0],
backend: &B,
) -> CascadeSMTProofV0 {
let proof = prove_box_shorthand_combination(shorthand_property, longhands);
let canonical_input =
canonical_box_shorthand_combination_input_v0(shorthand_property, longhands);
cascade_smt_proof_v0(
canonical_input,
backend,
"prove_box_shorthand_combination",
Some(proof.accepted),
)
}
pub fn smt_prove_scope_flatten_candidate_v0<B: SmtBackendV0>(
input: ScopeFlattenInputV0,
backend: &B,
) -> CascadeSMTProofV0 {
let canonical_input = canonical_scope_flatten_candidate_input_v0(&input);
let proof = prove_scope_flatten_candidate(input);
cascade_smt_proof_v0(
canonical_input,
backend,
"prove_scope_flatten_candidate",
Some(proof.accepted),
)
}
pub fn smt_prove_layer_flatten_candidate_v0<B: SmtBackendV0>(
input: LayerFlattenInputV0,
backend: &B,
) -> CascadeSMTProofV0 {
let canonical_input = canonical_layer_flatten_candidate_input_v0(&input);
let proof = prove_layer_flatten_candidate(input);
cascade_smt_proof_v0(
canonical_input,
backend,
"prove_layer_flatten_candidate",
Some(proof.accepted),
)
}
pub fn smt_evaluate_static_supports_condition_v0<B: SmtBackendV0>(
condition: &str,
assumption: StaticSupportsAssumptionV0,
backend: &B,
) -> CascadeSMTProofV0 {
let witness = evaluate_static_supports_condition(condition, assumption);
let l1_accepted = match witness.verdict {
StaticSupportsEvalVerdictV0::AlwaysTrue => Some(true),
StaticSupportsEvalVerdictV0::AlwaysFalse => Some(false),
StaticSupportsEvalVerdictV0::Unknown => None,
};
cascade_smt_proof_v0(
canonical_static_supports_condition_input_v0(&witness.verdict),
backend,
"evaluate_static_supports_condition",
l1_accepted,
)
}
fn canonical_box_shorthand_combination_input_v0(
shorthand_property: &str,
longhands: &[BoxLonghandInputV0],
) -> CanonicalSmtInputV0 {
let expected = smt_box_shorthand_longhands_v0(shorthand_property);
let canonical_order = expected.is_some_and(|expected| {
longhands.len() == expected.len()
&& longhands
.iter()
.zip(expected.iter())
.all(|(actual, expected)| actual.property == *expected)
});
canonical_smt_input_v0(
"box-shorthand-combination",
"prove_box_shorthand_combination",
vec![
smt_require_term_v0("supported-shorthand-property", expected.is_some()),
smt_require_term_v0("canonical-longhand-quartet", canonical_order),
smt_require_term_v0(
"no-important-longhand",
longhands.iter().all(|longhand| !longhand.important),
),
smt_require_term_v0(
"no-empty-longhand-value",
longhands.iter().all(|longhand| !longhand.value.is_empty()),
),
smt_require_term_v0(
"adjacent-source-order",
longhands
.windows(2)
.all(|pair| pair[1].source_order == pair[0].source_order + 1),
),
],
)
}
fn canonical_scope_flatten_candidate_input_v0(input: &ScopeFlattenInputV0) -> CanonicalSmtInputV0 {
canonical_smt_input_v0(
"scope-flatten-candidate",
"prove_scope_flatten_candidate",
vec![
smt_require_term_v0("no-limit-selector", input.limit_selector.is_none()),
smt_require_term_v0("root-scope", input.root_selector.trim() == ":root"),
smt_require_term_v0("no-peer-scope", input.peer_scope_count == 0),
smt_require_term_v0(
"no-competing-unscoped-rule",
input.competing_unscoped_rule_count == 0,
),
smt_require_term_v0("not-inside-layer", !input.inside_layer),
],
)
}
fn canonical_layer_flatten_candidate_input_v0(input: &LayerFlattenInputV0) -> CanonicalSmtInputV0 {
canonical_smt_input_v0(
"layer-flatten-candidate",
"prove_layer_flatten_candidate",
vec![
smt_require_term_v0("closed-bundle", input.closed_bundle),
smt_require_term_v0("no-peer-layer", input.peer_layer_count == 0),
smt_require_term_v0("no-unlayered-rule", input.unlayered_rule_count == 0),
smt_require_term_v0(
"no-important-declaration",
input.important_declaration_count == 0,
),
],
)
}
fn canonical_static_supports_condition_input_v0(
verdict: &StaticSupportsEvalVerdictV0,
) -> CanonicalSmtInputV0 {
let canonical_terms = match verdict {
StaticSupportsEvalVerdictV0::AlwaysTrue => {
vec![smt_require_term_v0("supports-condition-known-true", true)]
}
StaticSupportsEvalVerdictV0::AlwaysFalse => {
vec![smt_require_term_v0("supports-condition-known-true", false)]
}
StaticSupportsEvalVerdictV0::Unknown => vec!["unknown:supports-condition".to_string()],
};
canonical_smt_input_v0(
"static-supports-condition",
"evaluate_static_supports_condition",
canonical_terms,
)
}
fn smt_require_term_v0(name: &str, value: bool) -> String {
format!("require:{name}={value}")
}
fn smt_box_shorthand_longhands_v0(shorthand_property: &str) -> Option<[&'static str; 4]> {
match shorthand_property {
"margin" => Some(["margin-top", "margin-right", "margin-bottom", "margin-left"]),
"padding" => Some([
"padding-top",
"padding-right",
"padding-bottom",
"padding-left",
]),
"border-color" => Some([
"border-top-color",
"border-right-color",
"border-bottom-color",
"border-left-color",
]),
"border-style" => Some([
"border-top-style",
"border-right-style",
"border-bottom-style",
"border-left-style",
]),
"border-width" => Some([
"border-top-width",
"border-right-width",
"border-bottom-width",
"border-left-width",
]),
"scroll-margin" => Some([
"scroll-margin-top",
"scroll-margin-right",
"scroll-margin-bottom",
"scroll-margin-left",
]),
"scroll-padding" => Some([
"scroll-padding-top",
"scroll-padding-right",
"scroll-padding-bottom",
"scroll-padding-left",
]),
_ => None,
}
}